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