theory tut02 imports "~~/src/HOL/IMP/AExp" "~~/src/HOL/Library/Monad_Syntax" (* For monad syntax *) begin fun subst :: "vname => aexp => aexp => aexp" where "subst n a' (N i) = N i" | "subst n a' (V x) = (if n=x then a' else V x)" | "subst n a' (Plus a1 a2) = Plus (subst n a' a1) (subst n a' a2)" lemma subst_lemma: "aval (subst n a' a) \ = aval a (\(n := aval a' \))" apply (induction a) apply auto done lemma comp: assumes "aval a1 s = aval a2 s" shows "aval (subst x a1 a) s = aval (subst x a2 a) s" apply (simp add: subst_lemma assms) done lemma comp_alt_proof: assumes "aval a1 s = aval a2 s" shows "aval (subst x a1 a) s = aval (subst x a2 a) s" apply (subst subst_lemma) apply (subst subst_lemma) apply (subst assms) by (rule refl) datatype aexp = N int | V vname | Plus aexp aexp | Inc vname | Div aexp aexp term "s(x := 6)" -- "Function update" term "Some 4" -- "Option: Some" term None -- "Option: None" value "fst (a,b)=a" value "snd (a,b)=b" typ "'a option" value "case a of None => x | Some v => y" value "let x=1; y=2 in x+y" typ "val * state" typ "val \ state" (* "\times"*) 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 = ( case (aval a1 s) of Some (v1,s) => ( case (aval a2 s) of Some (v2,s) => Some (v1+v2,s) | None => None ) | None => None )" | "aval (Inc x) s = Some (s x,s(x := s x + 1))" | "aval (Div a1 a2) s = ( case (aval a1 s) of Some (v1,s) => ( case (aval a2 s) of Some (v2,s) => ( if v2=0 then None else Some (v1 div v2,s)) | None => None ) | None => None )" text "Alternative definition with monads" fun aval_m :: "aexp => state => (val\state) option" where "aval_m (N i) s = Some (i,s)" | "aval_m (V x) s = Some (s x,s)" | "aval_m (Plus a1 a2) s = do { (v1,s) <- aval_m a1 s; (v2,s) <- aval_m a2 s; Some (v1+v2,s) }" | "aval_m (Inc x) s = Some (s x,s(x := s x + 1))" | "aval_m (Div a1 a2) s = ( do { (v1,s) <- aval_m a1 s; (v2,s) <- aval_m a2 s; if v2=0 then None else Some (v1 div v2,s) } )" lemma "aval_m a s = aval a s" apply (induct a arbitrary: s) apply (auto split: option.split) done lemma assumes "aval a s = Some (v,s')" shows "s x \ s' x" using assms apply (induction a arbitrary: s s' v) apply (fastforce split: option.split_asm split_if_asm)+ done end