src/HOL/IMP/BExp.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45216 a51a70687517
child 45255 ffc06165d272
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
     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 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
     8 "bval (Bc v) s = v" |
     9 "bval (Not b) s = (\<not> bval b s)" |
    10 "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" |
    11 "bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
    12 
    13 value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
    14             <''x'' := 3, ''y'' := 1>"
    15 
    16 
    17 subsection "Optimization"
    18 
    19 text{* Optimized constructors: *}
    20 
    21 fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
    22 "less (N n1) (N n2) = Bc(n1 < n2)" |
    23 "less a1 a2 = Less a1 a2"
    24 
    25 lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
    26 apply(induction a1 a2 rule: less.induct)
    27 apply simp_all
    28 done
    29 
    30 fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
    31 "and (Bc True) b = b" |
    32 "and b (Bc True) = b" |
    33 "and (Bc False) b = Bc False" |
    34 "and b (Bc False) = Bc False" |
    35 "and b1 b2 = And b1 b2"
    36 
    37 lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
    38 apply(induction b1 b2 rule: and.induct)
    39 apply simp_all
    40 done
    41 
    42 fun not :: "bexp \<Rightarrow> bexp" where
    43 "not (Bc True) = Bc False" |
    44 "not (Bc False) = Bc True" |
    45 "not b = Not b"
    46 
    47 lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
    48 apply(induction b rule: not.induct)
    49 apply simp_all
    50 done
    51 
    52 text{* Now the overall optimizer: *}
    53 
    54 fun bsimp :: "bexp \<Rightarrow> bexp" where
    55 "bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" |
    56 "bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" |
    57 "bsimp (Not b) = not(bsimp b)" |
    58 "bsimp (Bc v) = Bc v"
    59 
    60 value "bsimp (And (Less (N 0) (N 1)) b)"
    61 
    62 value "bsimp (And (Less (N 1) (N 0)) (B True))"
    63 
    64 theorem "bval (bsimp b) s = bval b s"
    65 apply(induction b)
    66 apply simp_all
    67 done
    68 
    69 end