author | nipkow |
Mon, 20 Aug 2018 20:54:26 +0200 | |
changeset 68776 | 403dd13cf6e9 |
parent 67406 | 23307fd33906 |
child 69505 | cc2d676d5395 |
permissions | -rw-r--r-- |
58889 | 1 |
section "Arithmetic and Boolean Expressions" |
43141 | 2 |
|
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
3 |
subsection "Arithmetic Expressions" |
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
4 |
|
43141 | 5 |
theory AExp imports Main begin |
6 |
||
45212 | 7 |
type_synonym vname = string |
43141 | 8 |
type_synonym val = int |
45212 | 9 |
type_synonym state = "vname \<Rightarrow> val" |
43141 | 10 |
|
67406 | 11 |
text_raw\<open>\snip{AExpaexpdef}{2}{1}{%\<close> |
58310 | 12 |
datatype aexp = N int | V vname | Plus aexp aexp |
67406 | 13 |
text_raw\<open>}%endsnip\<close> |
43141 | 14 |
|
67406 | 15 |
text_raw\<open>\snip{AExpavaldef}{1}{2}{%\<close> |
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" | |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52460
diff
changeset
|
19 |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s" |
67406 | 20 |
text_raw\<open>}%endsnip\<close> |
43141 | 21 |
|
22 |
||
44923 | 23 |
value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)" |
43141 | 24 |
|
67406 | 25 |
text \<open>The same state more concisely:\<close> |
44923 | 26 |
value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))" |
43158 | 27 |
|
67406 | 28 |
text \<open>A little syntax magic to write larger states compactly:\<close> |
43158 | 29 |
|
44923 | 30 |
definition null_state ("<>") where |
31 |
"null_state \<equiv> \<lambda>x. 0" |
|
44036 | 32 |
syntax |
33 |
"_State" :: "updbinds => 'a" ("<_>") |
|
43158 | 34 |
translations |
51040 | 35 |
"_State ms" == "_Update <> ms" |
54289
5a1be63f32cf
Add output translation for <a := .., b := .., ..> state notation.
kleing
parents:
54252
diff
changeset
|
36 |
"_State (_updbinds b bs)" <= "_Update (_State b) bs" |
43141 | 37 |
|
67406 | 38 |
text \<open>\noindent |
43158 | 39 |
We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly: |
67406 | 40 |
\<close> |
54252
a4a00347e59f
use int example like in the rest of IMP (instead of nat)
kleing
parents:
53015
diff
changeset
|
41 |
lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))" |
43158 | 42 |
by (rule refl) |
43 |
||
44036 | 44 |
value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>" |
43158 | 45 |
|
44923 | 46 |
|
67406 | 47 |
text \<open>In the @{term[source] "<a := b>"} syntax, variables that are not mentioned are 0 by default: |
48 |
\<close> |
|
44036 | 49 |
value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>" |
43141 | 50 |
|
67406 | 51 |
text\<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> |
|
44923 | 53 |
|
43141 | 54 |
|
45255 | 55 |
subsection "Constant Folding" |
43141 | 56 |
|
67406 | 57 |
text\<open>Evaluate constant subsexpressions:\<close> |
43141 | 58 |
|
67406 | 59 |
text_raw\<open>\snip{AExpasimpconstdef}{0}{2}{%\<close> |
43141 | 60 |
fun asimp_const :: "aexp \<Rightarrow> aexp" where |
61 |
"asimp_const (N n) = N n" | |
|
62 |
"asimp_const (V x) = V x" | |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52460
diff
changeset
|
63 |
"asimp_const (Plus a\<^sub>1 a\<^sub>2) = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52460
diff
changeset
|
64 |
(case (asimp_const a\<^sub>1, asimp_const a\<^sub>2) of |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52460
diff
changeset
|
65 |
(N n\<^sub>1, N n\<^sub>2) \<Rightarrow> N(n\<^sub>1+n\<^sub>2) | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52460
diff
changeset
|
66 |
(b\<^sub>1,b\<^sub>2) \<Rightarrow> Plus b\<^sub>1 b\<^sub>2)" |
67406 | 67 |
text_raw\<open>}%endsnip\<close> |
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 |
||
67406 | 75 |
text\<open>Now we also eliminate all occurrences 0 in additions. The standard |
76 |
method: optimized versions of the constructors:\<close> |
|
43141 | 77 |
|
67406 | 78 |
text_raw\<open>\snip{AExpplusdef}{0}{2}{%\<close> |
43141 | 79 |
fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52460
diff
changeset
|
80 |
"plus (N i\<^sub>1) (N i\<^sub>2) = N(i\<^sub>1+i\<^sub>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))" | |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52460
diff
changeset
|
83 |
"plus a\<^sub>1 a\<^sub>2 = Plus a\<^sub>1 a\<^sub>2" |
67406 | 84 |
text_raw\<open>}%endsnip\<close> |
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 |
||
67406 | 92 |
text_raw\<open>\snip{AExpasimpdef}{2}{0}{%\<close> |
43141 | 93 |
fun asimp :: "aexp \<Rightarrow> aexp" where |
94 |
"asimp (N n) = N n" | |
|
95 |
"asimp (V x) = V x" | |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52460
diff
changeset
|
96 |
"asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)" |
67406 | 97 |
text_raw\<open>}%endsnip\<close> |
43141 | 98 |
|
67406 | 99 |
text\<open>Note that in @{const asimp_const} the optimized constructor was |
43141 | 100 |
inlined. Making it a separate function @{const plus} improves modularity of |
67406 | 101 |
the code and the proofs.\<close> |
43141 | 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 |