I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Download Files
### Definitions File

### Template File

### Check File

theory Defs imports "HOL-IMP.ASM" begin text \<open>The \<open>count\<close> function from sheet 1.\<close> fun count :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" where "count [] _ = 0" | "count (x # xs) y = (if x = y then Suc (count xs y) else count xs y)" end

theory Submission imports Defs begin datatype paren = Open | Close inductive S where S_empty: "S []" | S_append: "S xs \<Longrightarrow> S ys \<Longrightarrow> S (xs @ ys)" | S_paren: "S xs \<Longrightarrow> S (Open # xs @ [Close])" theorem S_T: "S xs \<Longrightarrow> T xs" sorry theorem T_S: "T xs \<Longrightarrow> count xs Open = count xs Close \<Longrightarrow> S xs" sorry type_synonym reg = nat datatype op = REG reg | VAL int \<comment> \<open>An operand is either a register or a constant.\<close> datatype instr = LD reg vname \<comment> \<open>Load a variable value in a register.\<close> | ADD reg op op \<comment> \<open>Add the contents of the two operands, placing the result in the register.\<close> datatype v_or_reg = Var vname | Reg reg type_synonym mstate = "v_or_reg \<Rightarrow> int" fun op_val :: "op \<Rightarrow> mstate \<Rightarrow> int" where "op_val (REG r) \<sigma> = \<sigma> (Reg r)" | "op_val (VAL n) _ = n" fun exec :: "instr \<Rightarrow> mstate \<Rightarrow> mstate" where "exec _ _ = undefined" fun execs :: "instr list \<Rightarrow> mstate \<Rightarrow> mstate" where "execs [] \<sigma> = \<sigma>" | \<comment> \<open>Add recursive case here\<close> "execs _ _ = undefined" fun cmp :: "aexp \<Rightarrow> reg \<Rightarrow> op \<times> instr list" where "cmp _ _ = undefined" lemma [simp]: "s (Reg r := x) o Var = s o Var" by auto theorem cmp_correct: "cmp a r = (x, prog) \<Longrightarrow> op_val x (execs prog \<sigma>) = aval a (\<sigma> o Var) \<and> execs prog \<sigma> o Var = \<sigma> o Var" \<comment> \<open>The first conjunct states that the resulting operand contains the correct value, and the second conjunct states that the variable state is unchanged.\<close> sorry definition "ex_split P xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ zs \<and> P ys zs)" fun has_split where "has_split _ _ _ = undefined" theorem ex_split_has_split[code]: "ex_split P xs \<longleftrightarrow> has_split P [] xs" sorry definition "ex_balanced_sum xs = (\<exists>ys zs. sum_list ys = sum_list zs \<and> xs = ys @ zs \<and> ys \<noteq> [] \<and> zs \<noteq> [])" value "ex_balanced_sum [1,2,3,3,2,1::nat]" definition "linear_split (xs :: int list) \<equiv> (undefined :: bool)" theorem linear_correct: "linear_split xs \<longleftrightarrow> ex_balanced_sum xs" sorry end

theory Check imports Submission begin theorem S_T: "S xs \<Longrightarrow> T xs" by (rule Submission.S_T) theorem T_S: "T xs \<Longrightarrow> count xs Open = count xs Close \<Longrightarrow> S xs" by (rule Submission.T_S) theorem cmp_correct: "cmp a r = (x, prog) \<Longrightarrow> op_val x (execs prog \<sigma>) = aval a (\<sigma> o Var) \<and> execs prog \<sigma> o Var = \<sigma> o Var" \<comment> \<open>The first conjunct states that the resulting operand contains the correct value, and the second conjunct states that the variable state is unchanged.\<close> by (rule Submission.cmp_correct) theorem ex_split_has_split[code]: "ex_split P xs \<longleftrightarrow> has_split P [] xs" by (rule Submission.ex_split_has_split) theorem linear_correct: "linear_split xs \<longleftrightarrow> ex_balanced_sum xs" by (rule Submission.linear_correct) end

Terms and Conditions