43141

1 
header "Arithmetic and Boolean Expressions"


2 


3 
theory AExp imports Main begin


4 


5 
subsection "Arithmetic Expressions"


6 

45212

7 
type_synonym vname = string

43141

8 
type_synonym val = int

45212

9 
type_synonym state = "vname \<Rightarrow> val"

43141

10 

45212

11 
datatype aexp = N int  V vname  Plus aexp aexp

43141

12 


13 
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where

45216

14 
"aval (N n) s = n" 

43141

15 
"aval (V x) s = s x" 


16 
"aval (Plus a1 a2) s = aval a1 s + aval a2 s"


17 


18 

44923

19 
value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"

43141

20 

43158

21 
text {* The same state more concisely: *}

44923

22 
value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))"

43158

23 


24 
text {* A little syntax magic to write larger states compactly: *}


25 

44923

26 
definition null_state ("<>") where


27 
"null_state \<equiv> \<lambda>x. 0"

44036

28 
syntax


29 
"_State" :: "updbinds => 'a" ("<_>")

43158

30 
translations

44923

31 
"_State ms" => "_Update <> ms"

43141

32 

43158

33 
text {*


34 
We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:


35 
*}

44923

36 
lemma "<a := Suc 0, b := 2> = (<> (a := Suc 0)) (b := 2)"

43158

37 
by (rule refl)


38 

44036

39 
value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"

43158

40 

44923

41 

43158

42 
text {* Variables that are not mentioned in the state are 0 by default in

44036

43 
the @{term "<a := b::int>"} syntax:

44923

44 
*}

44036

45 
value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"

43141

46 

44923

47 
text{* Note that this @{text"<\<dots>>"} syntax works for any function space


48 
@{text"\<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2"} where @{text "\<tau>\<^isub>2"} has a @{text 0}. *}


49 

43141

50 


51 
subsection "Optimization"


52 


53 
text{* Evaluate constant subsexpressions: *}


54 


55 
fun asimp_const :: "aexp \<Rightarrow> aexp" where


56 
"asimp_const (N n) = N n" 


57 
"asimp_const (V x) = V x" 


58 
"asimp_const (Plus a1 a2) =


59 
(case (asimp_const a1, asimp_const a2) of


60 
(N n1, N n2) \<Rightarrow> N(n1+n2) 


61 
(a1',a2') \<Rightarrow> Plus a1' a2')"


62 

45238

63 
theorem aval_asimp_const:

43141

64 
"aval (asimp_const a) s = aval a s"

45015

65 
apply(induction a)

43141

66 
apply (auto split: aexp.split)


67 
done


68 


69 
text{* Now we also eliminate all occurrences 0 in additions. The standard


70 
method: optimized versions of the constructors: *}


71 


72 
fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where


73 
"plus (N i1) (N i2) = N(i1+i2)" 


74 
"plus (N i) a = (if i=0 then a else Plus (N i) a)" 


75 
"plus a (N i) = (if i=0 then a else Plus a (N i))" 


76 
"plus a1 a2 = Plus a1 a2"


77 


78 
lemma aval_plus[simp]:


79 
"aval (plus a1 a2) s = aval a1 s + aval a2 s"

45015

80 
apply(induction a1 a2 rule: plus.induct)

43141

81 
apply simp_all (* just for a change from auto *)


82 
done


83 


84 
fun asimp :: "aexp \<Rightarrow> aexp" where


85 
"asimp (N n) = N n" 


86 
"asimp (V x) = V x" 


87 
"asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"


88 


89 
text{* Note that in @{const asimp_const} the optimized constructor was


90 
inlined. Making it a separate function @{const plus} improves modularity of


91 
the code and the proofs. *}


92 


93 
value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"


94 


95 
theorem aval_asimp[simp]:


96 
"aval (asimp a) s = aval a s"

45015

97 
apply(induction a)

43141

98 
apply simp_all


99 
done


100 


101 
end
