src/HOL/IMP/BExp.thy

--- a/src/HOL/IMP/BExp.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/BExp.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -2,10 +2,10 @@
 
 subsection "Boolean Expressions"
 
-datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
 
 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
-"bval (B bv) _ = bv" |
+"bval (Bc v) _ = v" |
 "bval (Not b) s = (\<not> bval b s)" |
 "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" |
 "bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
@@ -19,7 +19,7 @@
 text{* Optimized constructors: *}
 
 fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
-"less (N n1) (N n2) = B(n1 < n2)" |
+"less (N n1) (N n2) = Bc(n1 < n2)" |
 "less a1 a2 = Less a1 a2"
 
 lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
@@ -28,10 +28,10 @@
 done
 
 fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
-"and (B True) b = b" |
-"and b (B True) = b" |
-"and (B False) b = B False" |
-"and b (B False) = B False" |
+"and (Bc True) b = b" |
+"and b (Bc True) = b" |
+"and (Bc False) b = Bc False" |
+"and b (Bc False) = Bc False" |
 "and b1 b2 = And b1 b2"
 
 lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
@@ -40,8 +40,8 @@
 done
 
 fun not :: "bexp \<Rightarrow> bexp" where
-"not (B True) = B False" |
-"not (B False) = B True" |
+"not (Bc True) = Bc False" |
+"not (Bc False) = Bc True" |
 "not b = Not b"
 
 lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
@@ -55,7 +55,7 @@
 "bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" |
 "bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" |
 "bsimp (Not b) = not(bsimp b)" |
-"bsimp (B bv) = B bv"
+"bsimp (Bc v) = Bc v"
 
 value "bsimp (And (Less (N 0) (N 1)) b)"