src/HOL/IMP/AExp.thy
 author paulson 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