theory tut03 imports Main "~~/src/HOL/IMP/ASM" begin inductive odd :: "nat \ bool" where "odd 1" | "odd n \ odd (n+2)" thm odd.intros thm odd.cases thm odd.induct inductive is_aval :: "aexp \ state \ val \ bool" where "is_aval (N i) s i" | "is_aval (V x) s (s x)" | "\is_aval a1 s v1; is_aval a2 s v2\ \ is_aval (Plus a1 a2) s (v1+v2)" lemma "is_aval (Plus (N 2 ) (Plus (V x ) (N 3 ))) s (2 + (s x + 3 ))" by (rule is_aval.intros)+ lemma aux: "is_aval a s v \ v=v' \ is_aval a s v'" by simp lemma "is_aval (Plus (N 2 ) (Plus (V x ) (N 3 ))) s (2 + (s x + 3 ))" apply simp apply (rule aux) apply (rule is_aval.intros) apply (rule is_aval.intros) apply (rule is_aval.intros) apply (rule is_aval.intros) apply (rule is_aval.intros) apply simp done lemma aux1: "is_aval a s v \ aval a s = v" apply (induction rule: is_aval.induct) apply simp_all done lemma aux2: "aval a s = v \ is_aval a s v" apply (induction a arbitrary: v) apply (auto intro: is_aval.intros) done lemma "aval a s = v \ is_aval a s v" by (metis aux1 aux2) (*apply (rule iffI) apply (rule aux2) apply (assumption) apply (rule aux1) apply (assumption)*) (*using aux1 aux2 by blast*) term length 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 _ (x#y#xs) = Some ((x+y)#xs)" | "exec1 ADD _ _ = 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)" apply(induction is1 arbitrary: stk) apply (auto split: option.splits) done theorem exec_comp: "exec (comp a) s stk = Some (aval a s # stk)" apply(induction a arbitrary: stk) apply (auto) done context fixes maxsize :: nat begin definition push :: "val \ stack \ stack option" where "push i stk \ if length stk < maxsize then Some (i #stk ) else None" fun exec1' :: "instr \ state \ stack \ stack option" where "exec1' (LOADI n) _ stk = push n stk" | "exec1' (LOAD x) s stk = push (s(x)) stk" | "exec1' ADD _ (x#y#xs) = push (x+y) xs" | "exec1' ADD _ _ = 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)" apply(induction is1 arbitrary: stk) apply (auto split: option.splits) done end fun stacksize :: "aexp \ nat" where "stacksize (N _) = 1" | "stacksize (V _) = 1" | "stacksize (Plus a1 a2) = max (stacksize a1) (stacksize a2 + 1)" lemma exec_comp_aux: "stacksize a + length stk \ maxsize \ exec' maxsize (comp a) s stk = Some (aval a s#stk)" apply(induction a arbitrary: stk) apply (auto simp: push_def) done theorem exec_comp': "stacksize a \ maxsize \ exec' maxsize (comp a) s [] = Some ([aval a s])" using exec_comp_aux[of a "[]" maxsize] by simp thm exec_comp_aux[where a=a and stk ="[]" and maxsize = maxsize] end