theory Exercise04 imports "HOL-IMP.ASM" begin section \Relational Addition\ (* your definitions & proofs here *) section \Avoiding Stack Underflow\ text \From the tutorial:\ fun exec1 :: "instr \ state \ stack \ stack option" where "exec1 (LOADI n) _ stk = Some (n # stk)" | "exec1 (LOAD x) s stk = Some (s(x) # stk)" | "exec1 ADD _ stk = ( case stk of a # b # c \ Some ((a + b) # c) | _ \ None)" fun exec :: "instr list \ state \ stack \ stack option" where "exec [] _ stk = Some stk" | "exec (i#is) s stk = (case exec1 i s stk of Some stk \ exec is s stk | None \ None)" lemma exec_append[simp]: "exec (is1@is2) s stk = (case exec is1 s stk of Some stk \ exec is2 s stk | None \ None)" by (induction is1 arbitrary: stk) (auto split: option.split) theorem exec_comp: "exec (comp a) s stk = Some (aval a s # stk)" by (induction a arbitrary: stk) auto (* your definitions & proofs here *) lemma "exec is s stk = Some stk \ can_execute (length stk) is" oops lemma exec1r_equiv1: "exec1r i s stk stk' \ exec1 i s stk = Some stk'" oops lemma exec1_equiv1: "execr is s stk stk' \ exec is s stk = Some stk'" oops lemma exec1r_equiv2: "exec1 i s stk = Some stk' \ exec1r i s stk stk'" oops lemma execr_equiv2: "exec is s stk = Some stk' \ execr is s stk stk'" oops end