author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45255  ffc06165d272 
child 49191  3601bf546775 
permissions  rwrr 
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 

45255  11 
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpaexpdef}{% *} 
45212  12 
datatype aexp = N int  V vname  Plus aexp aexp 
45255  13 
text_raw{*}\end{isaverbatimwrite}*} 
43141  14 

45255  15 
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpavaldef}{% *} 
43141  16 
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where 
45216  17 
"aval (N n) s = n"  
43141  18 
"aval (V x) s = s x"  
19 
"aval (Plus a1 a2) s = aval a1 s + aval a2 s" 

45255  20 
text_raw{*}\end{isaverbatimwrite}*} 
43141  21 

22 

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

43158  25 
text {* The same state more concisely: *} 
44923  26 
value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))" 
43158  27 

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

29 

44923  30 
definition null_state ("<>") where 
31 
"null_state \<equiv> \<lambda>x. 0" 

44036  32 
syntax 
33 
"_State" :: "updbinds => 'a" ("<_>") 

43158  34 
translations 
44923  35 
"_State ms" => "_Update <> ms" 
43141  36 

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

39 
*} 

44923  40 
lemma "<a := Suc 0, b := 2> = (<> (a := Suc 0)) (b := 2)" 
43158  41 
by (rule refl) 
42 

44036  43 
value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>" 
43158  44 

44923  45 

43158  46 
text {* Variables that are not mentioned in the state are 0 by default in 
44036  47 
the @{term "<a := b::int>"} syntax: 
44923  48 
*} 
44036  49 
value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>" 
43141  50 

44923  51 
text{* Note that this @{text"<\<dots>>"} syntax works for any function space 
52 
@{text"\<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2"} where @{text "\<tau>\<^isub>2"} has a @{text 0}. *} 

53 

43141  54 

45255  55 
subsection "Constant Folding" 
43141  56 

57 
text{* Evaluate constant subsexpressions: *} 

58 

45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

59 
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpconstdef}{% *} 
43141  60 
fun asimp_const :: "aexp \<Rightarrow> aexp" where 
61 
"asimp_const (N n) = N n"  

62 
"asimp_const (V x) = V x"  

45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

63 
"asimp_const (Plus a\<^isub>1 a\<^isub>2) = 
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

64 
(case (asimp_const a\<^isub>1, asimp_const a\<^isub>2) of 
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

65 
(N n\<^isub>1, N n\<^isub>2) \<Rightarrow> N(n\<^isub>1+n\<^isub>2)  
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

66 
(b\<^isub>1,b\<^isub>2) \<Rightarrow> Plus b\<^isub>1 b\<^isub>2)" 
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

67 
text_raw{*}\end{isaverbatimwrite}*} 
43141  68 

45238  69 
theorem aval_asimp_const: 
43141  70 
"aval (asimp_const a) s = aval a s" 
45015  71 
apply(induction a) 
43141  72 
apply (auto split: aexp.split) 
73 
done 

74 

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

76 
method: optimized versions of the constructors: *} 

77 

45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

78 
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpplusdef}{% *} 
43141  79 
fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where 
45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

80 
"plus (N i\<^isub>1) (N i\<^isub>2) = N(i\<^isub>1+i\<^isub>2)"  
43141  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))"  

45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

83 
"plus a\<^isub>1 a\<^isub>2 = Plus a\<^isub>1 a\<^isub>2" 
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

84 
text_raw{*}\end{isaverbatimwrite}*} 
43141  85 

86 
lemma aval_plus[simp]: 

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

45015  88 
apply(induction a1 a2 rule: plus.induct) 
43141  89 
apply simp_all (* just for a change from auto *) 
90 
done 

91 

45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

92 
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpdef}{% *} 
43141  93 
fun asimp :: "aexp \<Rightarrow> aexp" where 
94 
"asimp (N n) = N n"  

95 
"asimp (V x) = V x"  

45246
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

96 
"asimp (Plus a\<^isub>1 a\<^isub>2) = plus (asimp a\<^isub>1) (asimp a\<^isub>2)" 
4fbeabee6487
added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents:
45238
diff
changeset

97 
text_raw{*}\end{isaverbatimwrite}*} 
43141  98 

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

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

101 
the code and the proofs. *} 

102 

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

104 

105 
theorem aval_asimp[simp]: 

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

45015  107 
apply(induction a) 
43141  108 
apply simp_all 
109 
done 

110 

111 
end 