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.AExp" 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])" 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)" type_synonym reg = nat datatype op = REG reg | VAL val datatype instr = LD reg vname | ADD reg op op datatype v_or_reg = Var vname | Reg reg type_synonym mstate = "v_or_reg \<Rightarrow> int" definition "is_N a = (case a of N _ \<Rightarrow> True | _ \<Rightarrow> False)" fun num_add :: "instr list \<Rightarrow> nat" where "num_add [] = 0" | "num_add (x#xs) = (case x of (ADD _ _ _) \<Rightarrow> 1 | _ \<Rightarrow> 0) + num_add xs" lemma num_add_append[simp]: "num_add (xs @ ys) = num_add xs + num_add ys" by (induct xs) auto fun num_plus :: "aexp \<Rightarrow> nat" where "num_plus (Plus a1 a2) = 1 + num_plus a1 + num_plus a2" | "num_plus _ = 0" consts T :: "paren list \<Rightarrow> bool" consts op_val :: "op \<Rightarrow> mstate \<Rightarrow> int" consts exec1 :: "instr \<Rightarrow> mstate \<Rightarrow> mstate" consts exec :: "instr list \<Rightarrow> mstate \<Rightarrow> mstate" consts cmp :: "aexp \<Rightarrow> reg \<Rightarrow> instr list" end

theory Submission imports Defs begin theorem S_count: "S xs \<Longrightarrow> count xs Open = count xs Close" sorry inductive T :: "paren list \<Rightarrow> bool" lemma example: "T [Open, Open]" sorry 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 fun op_val :: "op \<Rightarrow> mstate \<Rightarrow> int" where "op_val _ = undefined" fun exec1 :: "instr \<Rightarrow> mstate \<Rightarrow> mstate" where "exec1 _ = undefined" fun exec :: "instr list \<Rightarrow> mstate \<Rightarrow> mstate" where "exec _ = undefined" fun cmp :: "aexp \<Rightarrow> reg \<Rightarrow> instr list" where "cmp _ = undefined" theorem cmp_len: "\<not>is_N a \<Longrightarrow> num_add (cmp a r) \<le> num_plus a" sorry lemma reg_var[simp]: "s (Reg r := x) o Var = s o Var" by auto theorem cmp_correct: "exec (cmp a r) \<sigma> (Reg r) = aval a (\<sigma> o Var)" sorry end

theory Check imports Submission begin theorem S_count: "S xs \<Longrightarrow> count xs Open = count xs Close" by (rule Submission.S_count) lemma example: "T [Open, Open]" by (rule Submission.example) 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_len: "\<not>is_N a \<Longrightarrow> num_add (cmp a r) \<le> num_plus a" by (rule Submission.cmp_len) theorem cmp_correct: "exec (cmp a r) \<sigma> (Reg r) = aval a (\<sigma> o Var)" by (rule Submission.cmp_correct) end

Terms and Conditions