1section "Arithmetic and Boolean Expressions" 2 3theory AExp imports Main begin 4 5subsection "Arithmetic Expressions" 6 7type_synonym vname = string 8type_synonym val = int 9type_synonym state = "vname \<Rightarrow> val" 10 11text_raw\<open>\snip{AExpaexpdef}{2}{1}{%\<close> 12datatype aexp = N int | V vname | Plus aexp aexp 13text_raw\<open>}%endsnip\<close> 14 15text_raw\<open>\snip{AExpavaldef}{1}{2}{%\<close> 16fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where 17"aval (N n) s = n" | 18"aval (V x) s = s x" | 19"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s" 20text_raw\<open>}%endsnip\<close> 21 22 23value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)" 24 25text \<open>The same state more concisely:\<close> 26value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))" 27 28text \<open>A little syntax magic to write larger states compactly:\<close> 29 30definition null_state ("<>") where 31 "null_state \<equiv> \<lambda>x. 0" 32syntax 33 "_State" :: "updbinds => 'a" ("<_>") 34translations 35 "_State ms" == "_Update <> ms" 36 "_State (_updbinds b bs)" <= "_Update (_State b) bs" 37 38text \<open>\noindent 39 We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly: 40\<close> 41lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))" 42 by (rule refl) 43 44value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>" 45 46 47text \<open>In the @{term[source] "<a := b>"} syntax, variables that are not mentioned are 0 by default: 48\<close> 49value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>" 50 51text\<open>Note that this @{text"<\<dots>>"} syntax works for any function space 52@{text"\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2"} where @{text "\<tau>\<^sub>2"} has a @{text 0}.\<close> 53 54 55subsection "Constant Folding" 56 57text\<open>Evaluate constant subsexpressions:\<close> 58 59text_raw\<open>\snip{AExpasimpconstdef}{0}{2}{%\<close> 60fun asimp_const :: "aexp \<Rightarrow> aexp" where 61"asimp_const (N n) = N n" | 62"asimp_const (V x) = V x" | 63"asimp_const (Plus a\<^sub>1 a\<^sub>2) = 64 (case (asimp_const a\<^sub>1, asimp_const a\<^sub>2) of 65 (N n\<^sub>1, N n\<^sub>2) \<Rightarrow> N(n\<^sub>1+n\<^sub>2) | 66 (b\<^sub>1,b\<^sub>2) \<Rightarrow> Plus b\<^sub>1 b\<^sub>2)" 67text_raw\<open>}%endsnip\<close> 68 69theorem aval_asimp_const: 70 "aval (asimp_const a) s = aval a s" 71apply(induction a) 72apply (auto split: aexp.split) 73done 74 75text\<open>Now we also eliminate all occurrences 0 in additions. The standard 76method: optimized versions of the constructors:\<close> 77 78text_raw\<open>\snip{AExpplusdef}{0}{2}{%\<close> 79fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where 80"plus (N i\<^sub>1) (N i\<^sub>2) = N(i\<^sub>1+i\<^sub>2)" | 81"plus (N i) a = (if i=0 then a else Plus (N i) a)" | 82"plus a (N i) = (if i=0 then a else Plus a (N i))" | 83"plus a\<^sub>1 a\<^sub>2 = Plus a\<^sub>1 a\<^sub>2" 84text_raw\<open>}%endsnip\<close> 85 86lemma aval_plus[simp]: 87 "aval (plus a1 a2) s = aval a1 s + aval a2 s" 88apply(induction a1 a2 rule: plus.induct) 89apply simp_all (* just for a change from auto *) 90done 91 92text_raw\<open>\snip{AExpasimpdef}{2}{0}{%\<close> 93fun asimp :: "aexp \<Rightarrow> aexp" where 94"asimp (N n) = N n" | 95"asimp (V x) = V x" | 96"asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)" 97text_raw\<open>}%endsnip\<close> 98 99text\<open>Note that in @{const asimp_const} the optimized constructor was 100inlined. Making it a separate function @{const plus} improves modularity of 101the code and the proofs.\<close> 102 103value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))" 104 105theorem aval_asimp[simp]: 106 "aval (asimp a) s = aval a s" 107apply(induction a) 108apply simp_all 109done 110 111end 112