src/HOL/IMP/AExp.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 58889 5b7a9633cfa8
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 section "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 text_raw{*\snip{AExpaexpdef}{2}{1}{% *}
    12 datatype aexp = N int | V vname | Plus aexp aexp
    13 text_raw{*}%endsnip*}
    14 
    15 text_raw{*\snip{AExpavaldef}{1}{2}{% *}
    16 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
    17 "aval (N n) s = n" |
    18 "aval (V x) s = s x" |
    19 "aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
    20 text_raw{*}%endsnip*}
    21 
    22 
    23 value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)"
    24 
    25 text {* The same state more concisely: *}
    26 value "aval (Plus (V ''x'') (N 5)) ((\<lambda>x. 0) (''x'':= 7))"
    27 
    28 text {* A little syntax magic to write larger states compactly: *}
    29 
    30 definition null_state ("<>") where
    31   "null_state \<equiv> \<lambda>x. 0"
    32 syntax 
    33   "_State" :: "updbinds => 'a" ("<_>")
    34 translations
    35   "_State ms" == "_Update <> ms"
    36   "_State (_updbinds b bs)" <= "_Update (_State b) bs"
    37 
    38 text {* \noindent
    39   We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly:
    40 *}
    41 lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))"
    42   by (rule refl)
    43 
    44 value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>"
    45 
    46 
    47 text {* In  the @{term[source] "<a := b>"} syntax, variables that are not mentioned are 0 by default:
    48 *}
    49 value "aval (Plus (V ''x'') (N 5)) <''y'' := 7>"
    50 
    51 text{* Note that this @{text"<\<dots>>"} syntax works for any function space
    52 @{text"\<tau>\<^sub>1 \<Rightarrow> \<tau>\<^sub>2"} where @{text "\<tau>\<^sub>2"} has a @{text 0}. *}
    53 
    54 
    55 subsection "Constant Folding"
    56 
    57 text{* Evaluate constant subsexpressions: *}
    58 
    59 text_raw{*\snip{AExpasimpconstdef}{0}{2}{% *}
    60 fun asimp_const :: "aexp \<Rightarrow> aexp" where
    61 "asimp_const (N n) = N n" |
    62 "asimp_const (V x) = V x" |
    63 "asimp_const (Plus a\<^sub>1 a\<^sub>2) =
    64   (case (asimp_const a\<^sub>1, asimp_const a\<^sub>2) of
    65     (N n\<^sub>1, N n\<^sub>2) \<Rightarrow> N(n\<^sub>1+n\<^sub>2) |
    66     (b\<^sub>1,b\<^sub>2) \<Rightarrow> Plus b\<^sub>1 b\<^sub>2)"
    67 text_raw{*}%endsnip*}
    68 
    69 theorem aval_asimp_const:
    70   "aval (asimp_const a) s = aval a s"
    71 apply(induction a)
    72 apply (auto split: aexp.split)
    73 done
    74 
    75 text{* Now we also eliminate all occurrences 0 in additions. The standard
    76 method: optimized versions of the constructors: *}
    77 
    78 text_raw{*\snip{AExpplusdef}{0}{2}{% *}
    79 fun plus :: "aexp \<Rightarrow> aexp \<Rightarrow> aexp" where
    80 "plus (N i\<^sub>1) (N i\<^sub>2) = N(i\<^sub>1+i\<^sub>2)" |
    81 "plus (N i) a = (if i=0 then a else Plus (N i) a)" |
    82 "plus a (N i) = (if i=0 then a else Plus a (N i))" |
    83 "plus a\<^sub>1 a\<^sub>2 = Plus a\<^sub>1 a\<^sub>2"
    84 text_raw{*}%endsnip*}
    85 
    86 lemma aval_plus[simp]:
    87   "aval (plus a1 a2) s = aval a1 s + aval a2 s"
    88 apply(induction a1 a2 rule: plus.induct)
    89 apply simp_all (* just for a change from auto *)
    90 done
    91 
    92 text_raw{*\snip{AExpasimpdef}{2}{0}{% *}
    93 fun asimp :: "aexp \<Rightarrow> aexp" where
    94 "asimp (N n) = N n" |
    95 "asimp (V x) = V x" |
    96 "asimp (Plus a\<^sub>1 a\<^sub>2) = plus (asimp a\<^sub>1) (asimp a\<^sub>2)"
    97 text_raw{*}%endsnip*}
    98 
    99 text{* Note that in @{const asimp_const} the optimized constructor was
   100 inlined. Making it a separate function @{const plus} improves modularity of
   101 the code and the proofs. *}
   102 
   103 value "asimp (Plus (Plus (N 0) (N 0)) (Plus (V ''x'') (N 0)))"
   104 
   105 theorem aval_asimp[simp]:
   106   "aval (asimp a) s = aval a s"
   107 apply(induction a)
   108 apply simp_all
   109 done
   110 
   111 end