theory tut03 imports Main "~~/src/HOL/IMP/AExp" begin fun subst :: "vname \ aexp \ aexp \ aexp" where "subst v a' (N i) = N i" | "subst v a' (V v') = (if v = v' then a' else V v')" | "subst v a' (Plus a1 a2) = Plus (subst v a' a1) (subst v a' a2)" value "subst ''x'' (N 3) (V ''x'')" value "subst ''x'' (N 3) (V ''y'')" lemma subst_lemma[simp]: "aval (subst x a' a) s = aval a (s(x := aval a' s))" apply (induction a) apply simp apply simp apply (simp only: subst.simps) apply (simp only: aval.simps) done lemma comp: "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 datatype aexp' = N' int | V' vname | Plus' aexp' aexp' | PI' vname | Div' aexp' aexp' fun aval' :: "aexp' \ state \ (val \ state) option" where "aval' (N' n) s = Some (n, s)" | "aval' (V' x) s = Some (s x, s)" | "aval' (Plus' a\<^sub>1 a\<^sub>2) s = (case aval' a\<^sub>1 s of Some (v1, s1) \ (case aval' a\<^sub>2 s1 of Some (v2, s2) \ Some (v1 + v2, s2) | None \ None) | None \ None )" | "aval' (Div' a\<^sub>1 a\<^sub>2) s = (case aval' a\<^sub>1 s of Some (v1, s1) \ (case aval' a\<^sub>2 s1 of Some (v2, s2) \ if v2 = 0 then None else Some (v1 div v2, s2) | None \ None) | None \ None )" | "aval' (PI' x) s = Some (s x, s(x := s x + 1))" lemma "aval' (Plus' a b) s = aval' (Plus' b a) s" nitpick oops lemma "aval' (Plus' (V' ''x'') (PI' ''x'')) s \ aval' (Plus' (PI' ''x'') (V' ''x'')) s" by simp value "aval' (Div' (N' 3) (N' 0)) <>" value "aval' (Plus' (Div' (N' 3) (N' 0)) (N' 1)) <>" value "aval' (Div' (N' 4) (N' 2)) <>" lemma aval'_inc: "aval' a s = Some (v,s') \ s x \ s' x" apply (induct a arbitrary: s s' v) apply simp apply simp apply simp (* Notice how the simplifier doesn't split the cases for None and Some in the assumption *) apply (fastforce split: option.splits if_splits) apply force apply (fastforce split: option.splits if_splits) done end