theory ex02 imports "HOL-IMP.AExp" "HOL-IMP.BExp" begin fun deduplicate :: "'a list \ 'a list" value "deduplicate [1,1,2,3,2,2,1::nat] = [1,2,3,2,1]" lemma "length (deduplicate xs) \ length xs" fun subst :: "vname \ aexp \ aexp \ aexp" lemma subst_lemma: "aval (subst x a' a) s = aval a (s(x := aval a' s))" lemma comp: "aval a1 s = aval a2 s \ aval (subst x a1 a) s = aval (subst x a2 a) s" value "<>(x := 0)" value "aval' (Plus' (PI' ''x'') (V' ''x'')) <>" value "aval' (Plus' (Plus' (PI' ''x'') (PI' ''x'')) (PI' ''x'')) <>" lemma aval'_inc: "aval' a <> = (v, s') \ 0 \ s' x" fun vars :: "aexp \ vname set" where lemma ndep: "x \ vars e \ aval e (s(x:=v)) = aval e s" end