src/HOL/IMP/AExp.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45216 a51a70687517
child 45238 ed2bb3b58cc4
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 header "Arithmetic and Boolean Expressions"
     2 
     3 theory AExp imports Main begin
     4 
     5 subsection "Arithmetic Expressions"
     6 
     7 type_synonym vname = string
     8 type_synonym val = int
     9 type_synonym state = "vname \<Rightarrow> val"
    10 
    11 datatype aexp = N int | V vname | Plus aexp aexp
    12 
    13 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
    14 "aval (N n) s = 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)) (\<lambda>x. if x = ''x'' then 7 else 0)"
    20 
    21 text {* The same state more concisely: *}
    22 value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))"
    23 
    24 text {* A little syntax magic to write larger states compactly: *}
    25 
    26 definition null_state ("<>") where
    27   "null_state \<equiv> \<lambda>x. 0"
    28 syntax 
    29   "_State" :: "updbinds => 'a" ("<_>")
    30 translations
    31   "_State ms" => "_Update <> 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> = (<> (a := Suc 0)) (b := 2)"
    37   by (rule refl)
    38 
    39 value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
    40 
    41 
    42 text {* Variables that are not mentioned in the state are 0 by default in 
    43   the @{term "<a := b::int>"} syntax: 
    44 *}
    45 value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
    46 
    47 text{* Note that this @{text"<\<dots>>"} syntax works for any function space
    48 @{text"\<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2"} where @{text "\<tau>\<^isub>2"} has a @{text 0}. *}
    49 
    50 
    51 subsection "Optimization"
    52 
    53 text{* Evaluate constant subsexpressions: *}
    54 
    55 fun asimp_const :: "aexp \<Rightarrow> aexp" where
    56 "asimp_const (N n) = N n" |
    57 "asimp_const (V x) = V x" |
    58 "asimp_const (Plus a1 a2) =
    59   (case (asimp_const a1, asimp_const a2) of
    60     (N n1, N n2) \<Rightarrow> N(n1+n2) |
    61     (a1',a2') \<Rightarrow> Plus a1' a2')"
    62 
    63 theorem aval_asimp_const[simp]:
    64   "aval (asimp_const a) s = aval a s"
    65 apply(induction a)
    66 apply (auto split: aexp.split)
    67 done
    68 
    69 text{* Now we also eliminate all occurrences 0 in additions. The standard
    70 method: optimized versions of the constructors: *}
    71 
    72 fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
    73 "plus (N i1) (N i2) = N(i1+i2)" |
    74 "plus (N i) a = (if i=0 then a else Plus (N i) a)" |
    75 "plus a (N i) = (if i=0 then a else Plus a (N i))" |
    76 "plus a1 a2 = Plus a1 a2"
    77 
    78 lemma aval_plus[simp]:
    79   "aval (plus a1 a2) s = aval a1 s + aval a2 s"
    80 apply(induction a1 a2 rule: plus.induct)
    81 apply simp_all (* just for a change from auto *)
    82 done
    83 
    84 fun asimp :: "aexp \<Rightarrow> aexp" where
    85 "asimp (N n) = N n" |
    86 "asimp (V x) = V x" |
    87 "asimp (Plus a1 a2) = plus (asimp a1) (asimp a2)"
    88 
    89 text{* Note that in @{const asimp_const} the optimized constructor was
    90 inlined. Making it a separate function @{const plus} improves modularity of
    91 the code and the proofs. *}
    92 
    93 value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
    94 
    95 theorem aval_asimp[simp]:
    96   "aval (asimp a) s = aval a s"
    97 apply(induction a)
    98 apply simp_all
    99 done
   100 
   101 end