src/HOL/IMP/BExp.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 60170 031ec3d34d31
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 theory BExp imports AExp begin
     2 
     3 subsection "Boolean Expressions"
     4 
     5 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
     6 
     7 text_raw{*\snip{BExpbvaldef}{1}{2}{% *}
     8 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
     9 "bval (Bc v) s = v" |
    10 "bval (Not b) s = (\<not> bval b s)" |
    11 "bval (And b\<^sub>1 b\<^sub>2) s = (bval b\<^sub>1 s \<and> bval b\<^sub>2 s)" |
    12 "bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
    13 text_raw{*}%endsnip*}
    14 
    15 value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
    16             <''x'' := 3, ''y'' := 1>"
    17 
    18 
    19 subsection "Constant Folding"
    20 
    21 text{* Optimizing constructors: *}
    22 
    23 text_raw{*\snip{BExplessdef}{0}{2}{% *}
    24 fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
    25 "less (N n\<^sub>1) (N n\<^sub>2) = Bc(n\<^sub>1 < n\<^sub>2)" |
    26 "less a\<^sub>1 a\<^sub>2 = Less a\<^sub>1 a\<^sub>2"
    27 text_raw{*}%endsnip*}
    28 
    29 lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
    30 apply(induction a1 a2 rule: less.induct)
    31 apply simp_all
    32 done
    33 
    34 text_raw{*\snip{BExpanddef}{2}{2}{% *}
    35 fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
    36 "and (Bc True) b = b" |
    37 "and b (Bc True) = b" |
    38 "and (Bc False) b = Bc False" |
    39 "and b (Bc False) = Bc False" |
    40 "and b\<^sub>1 b\<^sub>2 = And b\<^sub>1 b\<^sub>2"
    41 text_raw{*}%endsnip*}
    42 
    43 lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
    44 apply(induction b1 b2 rule: and.induct)
    45 apply simp_all
    46 done
    47 
    48 text_raw{*\snip{BExpnotdef}{2}{2}{% *}
    49 fun not :: "bexp \<Rightarrow> bexp" where
    50 "not (Bc True) = Bc False" |
    51 "not (Bc False) = Bc True" |
    52 "not b = Not b"
    53 text_raw{*}%endsnip*}
    54 
    55 lemma bval_not[simp]: "bval (not b) s = (\<not> bval b s)"
    56 apply(induction b rule: not.induct)
    57 apply simp_all
    58 done
    59 
    60 text{* Now the overall optimizer: *}
    61 
    62 text_raw{*\snip{BExpbsimpdef}{0}{2}{% *}
    63 fun bsimp :: "bexp \<Rightarrow> bexp" where
    64 "bsimp (Bc v) = Bc v" |
    65 "bsimp (Not b) = not(bsimp b)" |
    66 "bsimp (And b\<^sub>1 b\<^sub>2) = and (bsimp b\<^sub>1) (bsimp b\<^sub>2)" |
    67 "bsimp (Less a\<^sub>1 a\<^sub>2) = less (asimp a\<^sub>1) (asimp a\<^sub>2)"
    68 text_raw{*}%endsnip*}
    69 
    70 value "bsimp (And (Less (N 0) (N 1)) b)"
    71 
    72 value "bsimp (And (Less (N 1) (N 0)) (Bc True))"
    73 
    74 theorem "bval (bsimp b) s = bval b s"
    75 apply(induction b)
    76 apply simp_all
    77 done
    78 
    79 end