src/HOL/IMP/AExp.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45255 ffc06165d272
child 49191 3601bf546775
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     1
header "Arithmetic and Boolean Expressions"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     2
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     3
theory AExp imports Main begin
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     4
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     5
subsection "Arithmetic Expressions"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     6
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45015
diff changeset
     7
type_synonym vname = string
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
     8
type_synonym val = int
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45015
diff changeset
     9
type_synonym state = "vname \<Rightarrow> val"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    10
45255
nipkow
parents: 45246
diff changeset
    11
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpaexpdef}{% *}
45212
e87feee00a4c renamed name -> vname
nipkow
parents: 45015
diff changeset
    12
datatype aexp = N int | V vname | Plus aexp aexp
45255
nipkow
parents: 45246
diff changeset
    13
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    14
45255
nipkow
parents: 45246
diff changeset
    15
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpavaldef}{% *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    16
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
45216
nipkow
parents: 45212
diff changeset
    17
"aval (N n) s = n" |
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    18
"aval (V x) s = s x" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    19
"aval (Plus a1 a2) s = aval a1 s + aval a2 s"
45255
nipkow
parents: 45246
diff changeset
    20
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    21
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    22
44923
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    23
value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    24
43158
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    25
text {* The same state more concisely: *}
44923
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    26
value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))"
43158
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    27
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    28
text {* A little syntax magic to write larger states compactly: *}
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    29
44923
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    30
definition null_state ("<>") where
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    31
  "null_state \<equiv> \<lambda>x. 0"
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 43250
diff changeset
    32
syntax 
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 43250
diff changeset
    33
  "_State" :: "updbinds => 'a" ("<_>")
43158
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    34
translations
44923
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    35
  "_State ms" => "_Update <> ms"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    36
43158
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    37
text {* 
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    38
  We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    39
*}
44923
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    40
lemma "<a := Suc 0, b := 2> = (<> (a := Suc 0)) (b := 2)"
43158
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    41
  by (rule refl)
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    42
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 43250
diff changeset
    43
value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
43158
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    44
44923
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    45
43158
686fa0a0696e imported rest of new IMP
kleing
parents: 43141
diff changeset
    46
text {* Variables that are not mentioned in the state are 0 by default in 
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 43250
diff changeset
    47
  the @{term "<a := b::int>"} syntax: 
44923
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    48
*}
44036
d03f9f28d01d new state syntax with less conflicts
kleing
parents: 43250
diff changeset
    49
value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    50
44923
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    51
text{* Note that this @{text"<\<dots>>"} syntax works for any function space
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    52
@{text"\<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2"} where @{text "\<tau>\<^isub>2"} has a @{text 0}. *}
b80108b346a9 cleand up AbsInt fixpoint iteration; tuned syntax
nipkow
parents: 44036
diff changeset
    53
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    54
45255
nipkow
parents: 45246
diff changeset
    55
subsection "Constant Folding"
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    56
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    57
text{* Evaluate constant subsexpressions: *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    58
45246
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    59
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpconstdef}{% *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    60
fun asimp_const :: "aexp \<Rightarrow> aexp" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    61
"asimp_const (N n) = N n" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    62
"asimp_const (V x) = V x" |
45246
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    63
"asimp_const (Plus a\<^isub>1 a\<^isub>2) =
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    64
  (case (asimp_const a\<^isub>1, asimp_const a\<^isub>2) of
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    65
    (N n\<^isub>1, N n\<^isub>2) \<Rightarrow> N(n\<^isub>1+n\<^isub>2) |
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    66
    (b\<^isub>1,b\<^isub>2) \<Rightarrow> Plus b\<^isub>1 b\<^isub>2)"
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    67
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    68
45238
nipkow
parents: 45216
diff changeset
    69
theorem aval_asimp_const:
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    70
  "aval (asimp_const a) s = aval a s"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
    71
apply(induction a)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    72
apply (auto split: aexp.split)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    73
done
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    74
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    75
text{* Now we also eliminate all occurrences 0 in additions. The standard
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    76
method: optimized versions of the constructors: *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    77
45246
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    78
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpplusdef}{% *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    79
fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
45246
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    80
"plus (N i\<^isub>1) (N i\<^isub>2) = N(i\<^isub>1+i\<^isub>2)" |
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    81
"plus (N i) a = (if i=0 then a else Plus (N i) a)" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    82
"plus a (N i) = (if i=0 then a else Plus a (N i))" |
45246
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    83
"plus a\<^isub>1 a\<^isub>2 = Plus a\<^isub>1 a\<^isub>2"
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    84
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    85
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    86
lemma aval_plus[simp]:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    87
  "aval (plus a1 a2) s = aval a1 s + aval a2 s"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
    88
apply(induction a1 a2 rule: plus.induct)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    89
apply simp_all (* just for a change from auto *)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    90
done
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    91
45246
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    92
text_raw{*\begin{isaverbatimwrite}\newcommand{\AExpasimpdef}{% *}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    93
fun asimp :: "aexp \<Rightarrow> aexp" where
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    94
"asimp (N n) = N n" |
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    95
"asimp (V x) = V x" |
45246
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    96
"asimp (Plus a\<^isub>1 a\<^isub>2) = plus (asimp a\<^isub>1) (asimp a\<^isub>2)"
4fbeabee6487 added isaverbatimwrite that allows to cut out snippets of thy files in their latex form and dump them in a file
nipkow
parents: 45238
diff changeset
    97
text_raw{*}\end{isaverbatimwrite}*}
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    98
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
    99
text{* Note that in @{const asimp_const} the optimized constructor was
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   100
inlined. Making it a separate function @{const plus} improves modularity of
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   101
the code and the proofs. *}
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   102
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   103
value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   104
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   105
theorem aval_asimp[simp]:
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   106
  "aval (asimp a) s = aval a s"
45015
fdac1e9880eb Updated IMP to use new induction method
nipkow
parents: 44923
diff changeset
   107
apply(induction a)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   108
apply simp_all
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   109
done
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   110
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents:
diff changeset
   111
end