src/HOL/IMP/AExp.thy
 author huffman Thu Aug 11 09:11:15 2011 -0700 (2011-08-11) changeset 44165 d26a45f3c835 parent 44036 d03f9f28d01d child 44923 b80108b346a9 permissions -rw-r--r--
remove lemma stupid_ext
```     1 header "Arithmetic and Boolean Expressions"
```
```     2
```
```     3 theory AExp imports Main begin
```
```     4
```
```     5 subsection "Arithmetic Expressions"
```
```     6
```
```     7 type_synonym name = string
```
```     8 type_synonym val = int
```
```     9 type_synonym state = "name \<Rightarrow> val"
```
```    10
```
```    11 datatype aexp = N int | V name | Plus aexp aexp
```
```    12
```
```    13 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
```
```    14 "aval (N n) _ = n" |
```
```    15 "aval (V x) s = s x" |
```
```    16 "aval (Plus a1 a2) s = aval a1 s + aval a2 s"
```
```    17
```
```    18
```
```    19 value "aval (Plus (V ''x'') (N 5)) (%x. if x = ''x'' then 7 else 0)"
```
```    20
```
```    21 text {* The same state more concisely: *}
```
```    22 value "aval (Plus (V ''x'') (N 5)) ((%x. 0) (''x'':= 7))"
```
```    23
```
```    24 text {* A little syntax magic to write larger states compactly: *}
```
```    25
```
```    26 definition
```
```    27   "null_heap \<equiv> \<lambda>x. 0"
```
```    28 syntax
```
```    29   "_State" :: "updbinds => 'a" ("<_>")
```
```    30 translations
```
```    31   "_State ms" => "_Update (CONST null_heap) ms"
```
```    32
```
```    33 text {*
```
```    34   We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
```
```    35 *}
```
```    36 lemma "<a := Suc 0, b := 2> = (null_heap (a := Suc 0)) (b := 2)"
```
```    37   by (rule refl)
```
```    38
```
```    39 value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
```
```    40
```
```    41 text {* Variables that are not mentioned in the state are 0 by default in
```
```    42   the @{term "<a := b::int>"} syntax:
```
```    43 *}
```
```    44 value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
```
```    45
```
```    46
```
```    47 subsection "Optimization"
```
```    48
```
```    49 text{* Evaluate constant subsexpressions: *}
```
```    50
```
```    51 fun asimp_const :: "aexp \<Rightarrow> aexp" where
```
```    52 "asimp_const (N n) = N n" |
```
```    53 "asimp_const (V x) = V x" |
```
```    54 "asimp_const (Plus a1 a2) =
```
```    55   (case (asimp_const a1, asimp_const a2) of
```
```    56     (N n1, N n2) \<Rightarrow> N(n1+n2) |
```
```    57     (a1',a2') \<Rightarrow> Plus a1' a2')"
```
```    58
```
```    59 theorem aval_asimp_const[simp]:
```
```    60   "aval (asimp_const a) s = aval a s"
```
```    61 apply(induct a)
```
```    62 apply (auto split: aexp.split)
```
```    63 done
```
```    64
```
```    65 text{* Now we also eliminate all occurrences 0 in additions. The standard
```
```    66 method: optimized versions of the constructors: *}
```
```    67
```
```    68 fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
```
```    69 "plus (N i1) (N i2) = N(i1+i2)" |
```
```    70 "plus (N i) a = (if i=0 then a else Plus (N i) a)" |
```
```    71 "plus a (N i) = (if i=0 then a else Plus a (N i))" |
```
```    72 "plus a1 a2 = Plus a1 a2"
```
```    73
```
```    74 code_thms plus
```
```    75 code_thms plus
```
```    76
```
```    77 (* FIXME: dropping subsumed code eqns?? *)
```
```    78 lemma aval_plus[simp]:
```
```    79   "aval (plus a1 a2) s = aval a1 s + aval a2 s"
```
```    80 apply(induct a1 a2 rule: plus.induct)
```
```    81 apply simp_all (* just for a change from auto *)
```
```    82 done
```
```    83 code_thms plus
```
```    84
```
```    85 fun asimp :: "aexp \<Rightarrow> aexp" where
```
```    86 "asimp (N n) = N n" |
```
```    87 "asimp (V x) = V x" |
```
```    88 "asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"
```
```    89
```
```    90 text{* Note that in @{const asimp_const} the optimized constructor was
```
```    91 inlined. Making it a separate function @{const plus} improves modularity of
```
```    92 the code and the proofs. *}
```
```    93
```
```    94 value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
```
```    95
```
```    96 theorem aval_asimp[simp]:
```
```    97   "aval (asimp a) s = aval a s"
```
```    98 apply(induct a)
```
```    99 apply simp_all
```
```   100 done
```
```   101
```
```   102 end
```