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