theory tut02 imports "~~/src/HOL/IMP/AExp" "~~/src/HOL/Library/Monad_Syntax" begin fun subst :: "vname \ aexp \ aexp \ aexp" where "subst x a' (N i) = N i" | "subst x a' (V y) = (if x=y then a' else V y)" | "subst x a' (Plus a1 a2) = Plus (subst x a' a1) (subst x a' a2)" value "subst ''x'' (Plus (V ''z'') (N 2)) (Plus (V ''x'') (Plus (V ''y'') (Plus (N 1) (V ''x''))))" lemma subst_lemma: "aval (subst x a' a) s = aval a (s(x:=aval a' s))" by (induction a) auto lemma "aval a1 s = aval a2 s \ aval (subst x a1 a) s = aval (subst x a2 a) s" apply (subst subst_lemma) apply (subst subst_lemma) apply (simp only:) done lemma "aval a1 s = aval a2 s \ aval (subst x a1 a) s = aval (subst x a2 a) s" by (simp add: subst_lemma) (* by (induction a) auto Also works, but should re-use subst-lemma here*) fun vars :: "aexp \ vname set" where "vars (N _) = {}" | "vars (V x) = {x}" | "vars (Plus a1 a2) = vars a1 \ vars a2" value "vars (Plus (V ''x'') (Plus (V ''y'') (Plus (N 1) (V ''x''))))" lemma "x\vars e \ aval e (s(x:=v1)) = aval e (s(x:=v2))" by (induction e) auto datatype aexp' = N' int | V' vname | Plus' aexp' aexp' | PI vname | DIV aexp' aexp' fun aval' :: "aexp' \ state \ (val\state) option" where "aval' (N' i) s = Some (i,s)" | "aval' (V' x) s = Some (s x,s)" | "aval' (Plus' a1 a2) s = do { (v1,s) \ aval' a1 s; (v2,s) \ aval' a2 s; Some (v1+v2,s) }" | "aval' (DIV a1 a2) s = do { (v1,s) \ aval' a1 s; (v2,s) \ aval' a2 s; if v2 = 0 then None else Some (v1 div v2,s) }" | "aval' (PI x) s = Some (s x, s(x:=(s x + 1)))" (* Just ignore the next two lemmas, they are to set up the splitter for Option.bind. I assumed these to be in standard Isabelle *) lemma option_bind_split: "P (bind m f) \ (m = None \ P None) \ (\v. m=Some v \ P (f v))" by (cases m) auto lemma option_bind_split_asm: "P (bind m f) = (\( m=None \ \P None \ (\x. m=Some x \ \P (f x))))" by (cases m) auto lemma "aval' a s = Some (v,s') \ s x \ s' x" apply (induction a arbitrary: s s' v) (* The + iterates the method until it fails, or all goals are solved *) apply (fastforce split: split_if_asm prod.splits option_bind_split_asm)+ done lemma "aval' (Plus' (PI x) (V' x)) s \ aval' (Plus' (V' x) (PI x)) s" by auto end