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