# HG changeset patch
# User nipkow
# Date 1319034732 -7200
# Node ID 1f1897ac78771e5b49633c2edcf0de58b20d8ba1
# Parent  d98a0388faab49ae47d3a9a810eb7d6c7fd6f833
renamed B to Bc

diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Abs_Int0_const.thy
--- a/src/HOL/IMP/Abs_Int0_const.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Abs_Int0_const.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -88,7 +88,7 @@
 
 text{* While: *}
 definition "test4_const =
- ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
+ ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
 
 text{* While, test is ignored: *}
 definition "test5_const =
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -101,7 +101,7 @@
 
 
 fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where
-"bfilter (B bv) res S = (if bv=res then S else Bot)" |
+"bfilter (Bc v) res S = (if v=res then S else Bot)" |
 "bfilter (Not b) res S = bfilter b (\<not> res) S" |
 "bfilter (And b1 b2) res S =
   (if res then bfilter b1 True (bfilter b2 True S)
@@ -130,7 +130,7 @@
 
 lemma bfilter_sound: "s <:up S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:up bfilter b bv S"
 proof(induction b arbitrary: S bv)
-  case B thus ?case by simp
+  case Bc thus ?case by simp
 next
   case (Not b) thus ?case by simp
 next
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -83,7 +83,7 @@
 
 text{* While: *}
 definition "test4_const =
- ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
+ ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
 
 text{* While, test is ignored: *}
 definition "test5_const =
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -131,7 +131,7 @@
 
 
 fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
-"bfilter (B bv) res S = (if bv=res then S else bot)" |
+"bfilter (Bc v) res S = (if v=res then S else bot)" |
 "bfilter (Not b) res S = bfilter b (\<not> res) S" |
 "bfilter (And b1 b2) res S =
   (if res then bfilter b1 True (bfilter b2 True S)
@@ -159,7 +159,7 @@
 
 lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
 proof(induction b arbitrary: S bv)
-  case B thus ?case by simp
+  case Bc thus ?case by simp
 next
   case (Not b) thus ?case by simp
 next
diff -r d98a0388faab -r 1f1897ac7877 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)"
 
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/C_like.thy
--- a/src/HOL/IMP/C_like.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/C_like.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -11,10 +11,10 @@
 "aval (!a) s = s(aval a s)" |
 "aval (Plus a\<^isub>1 a\<^isub>2) s = aval a\<^isub>1 s + aval a\<^isub>2 s"
 
-datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
+datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
 
 primrec 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 b\<^isub>1 b\<^isub>2) s = (if bval b\<^isub>1 s then bval b\<^isub>2 s else False)" |
 "bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)"
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -443,7 +443,7 @@
   shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
          s' = s \<and> stk' = stk"
 using assms proof (induction b arbitrary: c j i n s' stk')
-  case B thus ?case 
+  case Bc thus ?case 
     by (simp split: split_if_asm add: exec_n_simps)
 next
   case (Not b) 
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -204,7 +204,7 @@
   by (induct a arbitrary: stk) fastforce+
 
 fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
-"bcomp (B bv) c n = (if bv=c then [JMP n] else [])" |
+"bcomp (Bc v) c n = (if v=c then [JMP n] else [])" |
 "bcomp (Not b) c n = bcomp b (\<not>c) n" |
 "bcomp (And b1 b2) c n =
  (let cb2 = bcomp b2 c n;
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Def_Ass_Exp.thy
--- a/src/HOL/IMP/Def_Ass_Exp.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Def_Ass_Exp.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -18,7 +18,7 @@
 
 
 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where
-"bval (B bv) s = Some bv" |
+"bval (Bc v) s = Some v" |
 "bval (Not b) s = (case bval b s of None \<Rightarrow> None | Some bv \<Rightarrow> Some(\<not> bv))" |
 "bval (And b\<^isub>1 b\<^isub>2) s = (case (bval b\<^isub>1 s, bval b\<^isub>2 s) of
   (Some bv\<^isub>1, Some bv\<^isub>2) \<Rightarrow> Some(bv\<^isub>1 & bv\<^isub>2) | _ \<Rightarrow> None)" |
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Fold.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -233,35 +233,35 @@
 "bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" |
 "bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" |
 "bsimp_const (Not b) t = not(bsimp_const b t)" |
-"bsimp_const (B bv) _ = B bv"
+"bsimp_const (Bc bc) _ = Bc bc"
 
 theorem bvalsimp_const [simp]:
   assumes "approx t s"
   shows "bval (bsimp_const b t) s = bval b s"
   using assms by (induct b) auto
 
-lemma not_B [simp]: "not (B v) = B (\<not>v)"
+lemma not_Bc [simp]: "not (Bc v) = Bc (\<not>v)"
   by (cases v) auto
 
-lemma not_B_eq [simp]: "(not b = B v) = (b = B (\<not>v))"
+lemma not_Bc_eq [simp]: "(not b = Bc v) = (b = Bc (\<not>v))"
   by (cases b) auto
 
-lemma and_B_eq: 
-  "(and a b = B v) = (a = B False \<and> \<not>v \<or> 
-                      b = B False \<and> \<not>v \<or> 
-                      (\<exists>v1 v2. a = B v1 \<and> b = B v2 \<and> v = v1 \<and> v2))"
+lemma and_Bc_eq: 
+  "(and a b = Bc v) =
+   (a = Bc False \<and> \<not>v  \<or>  b = Bc False \<and> \<not>v \<or> 
+    (\<exists>v1 v2. a = Bc v1 \<and> b = Bc v2 \<and> v = v1 \<and> v2))"
   by (rule and.induct) auto
 
-lemma less_B_eq [simp]:
-  "(less a b = B v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
+lemma less_Bc_eq [simp]:
+  "(less a b = Bc v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
   by (rule less.induct) auto
     
-theorem bvalsimp_const_B:
+theorem bvalsimp_const_Bc:
 assumes "approx t s"
-shows "bsimp_const b t = B v \<Longrightarrow> bval b s = v"
+shows "bsimp_const b t = Bc v \<Longrightarrow> bval b s = v"
   using assms
   by (induct b arbitrary: v)
-     (auto simp: approx_def and_B_eq aval_simp_const_N 
+     (auto simp: approx_def and_Bc_eq aval_simp_const_N 
            split: bexp.splits bool.splits)
 
 
@@ -271,8 +271,8 @@
   (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
 "bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" |
 "bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
-    B True \<Rightarrow> bdefs c1 t
-  | B False \<Rightarrow> bdefs c2 t
+    Bc True \<Rightarrow> bdefs c1 t
+  | Bc False \<Rightarrow> bdefs c2 t
   | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
 "bdefs (WHILE b DO c) t = t |` (-lnames c)" 
 
@@ -282,11 +282,11 @@
 "bfold (x ::= a) t = (x ::= (simp_const a t))" |
 "bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))" |
 "bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
-    B True \<Rightarrow> bfold c1 t
-  | B False \<Rightarrow> bfold c2 t
+    Bc True \<Rightarrow> bfold c1 t
+  | Bc False \<Rightarrow> bfold c2 t
   | _ \<Rightarrow> IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)" |
 "bfold (WHILE b DO c) t = (case bsimp_const b t of
-    B False \<Rightarrow> SKIP
+    Bc False \<Rightarrow> SKIP
   | _ \<Rightarrow> WHILE bsimp_const b (t |` (-lnames c)) DO bfold c (t |` (-lnames c)))"
 
 
@@ -342,18 +342,18 @@
   case (IfTrue b s c1 s')
   hence "approx (bdefs c1 t) s'" by simp
   thus ?case using `bval b s` `approx t s`
-    by (clarsimp simp: approx_merge bvalsimp_const_B 
+    by (clarsimp simp: approx_merge bvalsimp_const_Bc
                  split: bexp.splits bool.splits)
 next
   case (IfFalse b s c2 s')
   hence "approx (bdefs c2 t) s'" by simp
   thus ?case using `\<not>bval b s` `approx t s`
-    by (clarsimp simp: approx_merge bvalsimp_const_B 
+    by (clarsimp simp: approx_merge bvalsimp_const_Bc
                  split: bexp.splits bool.splits)
 next
   case WhileFalse
   thus ?case 
-    by (clarsimp simp: bvalsimp_const_B approx_def restrict_map_def
+    by (clarsimp simp: bvalsimp_const_Bc approx_def restrict_map_def
                  split: bexp.splits bool.splits)
 next
   case (WhileTrue b s1 c s2 s3)
@@ -385,7 +385,7 @@
                    IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
     by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) 
   thus ?case using If
-    by (fastforce simp: bvalsimp_const_B split: bexp.splits bool.splits 
+    by (fastforce simp: bvalsimp_const_Bc split: bexp.splits bool.splits 
                  intro: equiv_up_to_trans)
   next
   case (While b c)
@@ -400,7 +400,7 @@
   thus ?case
     by (auto split: bexp.splits bool.splits 
              intro: equiv_up_to_while_False 
-             simp: bvalsimp_const_B)
+             simp: bvalsimp_const_Bc)
 qed
 
 
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Poly_Types.thy
--- a/src/HOL/IMP/Poly_Types.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Poly_Types.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -18,7 +18,7 @@
 
 inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>p" 50)
 where
-"\<Gamma> \<turnstile>p B bv" |
+"\<Gamma> \<turnstile>p Bc v" |
 "\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p Not b" |
 "\<Gamma> \<turnstile>p b1 \<Longrightarrow> \<Gamma> \<turnstile>p b2 \<Longrightarrow> \<Gamma> \<turnstile>p And b1 b2" |
 "\<Gamma> \<turnstile>p a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p Less a1 a2"
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Sec_Type_Expr.thy
--- a/src/HOL/IMP/Sec_Type_Expr.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Sec_Type_Expr.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -20,7 +20,7 @@
 "sec_aexp (Plus a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
 
 fun sec_bexp :: "bexp \<Rightarrow> level" where
-"sec_bexp (B bv) = 0" |
+"sec_bexp (Bc v) = 0" |
 "sec_bexp (Not b) = sec_bexp b" |
 "sec_bexp (And b\<^isub>1 b\<^isub>2) = max (sec_bexp b\<^isub>1) (sec_bexp b\<^isub>2)" |
 "sec_bexp (Less a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -152,11 +152,11 @@
   "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
   by (auto simp: equiv_up_to_def)
 
-lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (B True) DO c'"
+lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (Bc True) DO c'"
  by (induct rule: big_step_induct) auto
   
 lemma equiv_up_to_while_True [intro!,simp]:
-  "P \<Turnstile> WHILE B True DO c \<sim> WHILE B True DO SKIP"
+  "P \<Turnstile> WHILE Bc True DO c \<sim> WHILE Bc True DO SKIP"
   unfolding equiv_up_to_def
   by (blast dest: while_never)
 
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Types.thy
--- a/src/HOL/IMP/Types.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Types.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -27,10 +27,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
 
 inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
-"tbval (B bv) s bv" |
+"tbval (Bc v) s v" |
 "tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
 "tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
 "taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
@@ -85,7 +85,7 @@
 
 inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
 where
-B_ty: "\<Gamma> \<turnstile> B bv" |
+B_ty: "\<Gamma> \<turnstile> Bc v" |
 Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
 And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
 Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"
diff -r d98a0388faab -r 1f1897ac7877 src/HOL/IMP/Vars.thy
--- a/src/HOL/IMP/Vars.thy	Wed Oct 19 09:11:21 2011 +0200
+++ b/src/HOL/IMP/Vars.thy	Wed Oct 19 16:32:12 2011 +0200
@@ -41,7 +41,7 @@
 begin
 
 fun vars_bexp :: "bexp \<Rightarrow> name set" where
-"vars_bexp (B bv) = {}" |
+"vars_bexp (Bc v) = {}" |
 "vars_bexp (Not b) = vars_bexp b" |
 "vars_bexp (And b\<^isub>1 b\<^isub>2) = vars_bexp b\<^isub>1 \<union> vars_bexp b\<^isub>2" |
 "vars_bexp (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"