header "Arithmetic and Boolean Expressions" theory AExp imports Main begin subsection "Arithmetic Expressions" type_synonym vname = string type_synonym val = int type_synonym state = "vname \ val" datatype aexp = N int | V vname | Plus aexp aexp fun aval :: "aexp \ state \ val" where "aval (N n) s = n" | "aval (V x) s = s x" | "aval (Plus a1 a2) s = aval a1 s + aval a2 s" value "aval (Plus (V ''x'') (N 5)) (\x. if x = ''x'' then 7 else 0)" text {* The same state more concisely: *} value "aval (Plus (V ''x'') (N 5)) ((\x. 0) (''x'':= 7))" text {* A little syntax magic to write larger states compactly: *} definition null_state ("<>") where "null_state \ \x. 0" syntax "_State" :: "updbinds => 'a" ("<_>") translations "_State ms" => "_Update <> ms" text {* We can now write a series of updates to the function @{text "\x. 0"} compactly: *} lemma " = (<> (a := Suc 0)) (b := 2)" by (rule refl) value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>" text {* Variables that are not mentioned in the state are 0 by default in the @{term ""} syntax: *} value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>" text{* Note that this @{text"<\>"} syntax works for any function space @{text"\\<^isub>1 \ \\<^isub>2"} where @{text "\\<^isub>2"} has a @{text 0}. *} subsection "Constant Folding" text{* Evaluate constant subsexpressions: *} fun asimp_const :: "aexp \ aexp" where "asimp_const (N n) = N n" | "asimp_const (V x) = V x" | "asimp_const (Plus a\<^isub>1 a\<^isub>2) = (case (asimp_const a\<^isub>1, asimp_const a\<^isub>2) of (N n\<^isub>1, N n\<^isub>2) \ N(n\<^isub>1+n\<^isub>2) | (b\<^isub>1,b\<^isub>2) \ Plus b\<^isub>1 b\<^isub>2)" theorem aval_asimp_const: "aval (asimp_const a) s = aval a s" apply(induction a) apply (auto split: aexp.split) done text{* Now we also eliminate all occurrences 0 in additions. The standard method: optimized versions of the constructors: *} fun plus :: "aexp \ aexp \ aexp" where "plus (N i\<^isub>1) (N i\<^isub>2) = N(i\<^isub>1+i\<^isub>2)" | "plus (N i) a = (if i=0 then a else Plus (N i) a)" | "plus a (N i) = (if i=0 then a else Plus a (N i))" | "plus a\<^isub>1 a\<^isub>2 = Plus a\<^isub>1 a\<^isub>2" lemma aval_plus[simp]: "aval (plus a1 a2) s = aval a1 s + aval a2 s" apply(induction a1 a2 rule: plus.induct) apply simp_all (* just for a change from auto *) done fun asimp :: "aexp \ aexp" where "asimp (N n) = N n" | "asimp (V x) = V x" | "asimp (Plus a\<^isub>1 a\<^isub>2) = plus (asimp a\<^isub>1) (asimp a\<^isub>2)" text{* Note that in @{const asimp_const} the optimized constructor was inlined. Making it a separate function @{const plus} improves modularity of the code and the proofs. *} value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))" theorem aval_asimp[simp]: "aval (asimp a) s = aval a s" apply(induction a) apply simp_all done end