renamed B to Bc
authornipkow
Wed Oct 19 16:32:12 2011 +0200 (2011-10-19)
changeset 452001f1897ac7877
parent 45191 d98a0388faab
child 45201 154242732ef8
renamed B to Bc
src/HOL/IMP/Abs_Int0_const.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
src/HOL/IMP/BExp.thy
src/HOL/IMP/C_like.thy
src/HOL/IMP/Comp_Rev.thy
src/HOL/IMP/Compiler.thy
src/HOL/IMP/Def_Ass_Exp.thy
src/HOL/IMP/Fold.thy
src/HOL/IMP/Poly_Types.thy
src/HOL/IMP/Sec_Type_Expr.thy
src/HOL/IMP/Sem_Equiv.thy
src/HOL/IMP/Types.thy
src/HOL/IMP/Vars.thy
     1.1 --- a/src/HOL/IMP/Abs_Int0_const.thy	Wed Oct 19 09:11:21 2011 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int0_const.thy	Wed Oct 19 16:32:12 2011 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4  
     1.5  text{* While: *}
     1.6  definition "test4_const =
     1.7 - ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
     1.8 + ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
     1.9  
    1.10  text{* While, test is ignored: *}
    1.11  definition "test5_const =
     2.1 --- a/src/HOL/IMP/Abs_Int1.thy	Wed Oct 19 09:11:21 2011 +0200
     2.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Wed Oct 19 16:32:12 2011 +0200
     2.3 @@ -101,7 +101,7 @@
     2.4  
     2.5  
     2.6  fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where
     2.7 -"bfilter (B bv) res S = (if bv=res then S else Bot)" |
     2.8 +"bfilter (Bc v) res S = (if v=res then S else Bot)" |
     2.9  "bfilter (Not b) res S = bfilter b (\<not> res) S" |
    2.10  "bfilter (And b1 b2) res S =
    2.11    (if res then bfilter b1 True (bfilter b2 True S)
    2.12 @@ -130,7 +130,7 @@
    2.13  
    2.14  lemma bfilter_sound: "s <:up S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:up bfilter b bv S"
    2.15  proof(induction b arbitrary: S bv)
    2.16 -  case B thus ?case by simp
    2.17 +  case Bc thus ?case by simp
    2.18  next
    2.19    case (Not b) thus ?case by simp
    2.20  next
     3.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Wed Oct 19 09:11:21 2011 +0200
     3.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Wed Oct 19 16:32:12 2011 +0200
     3.3 @@ -83,7 +83,7 @@
     3.4  
     3.5  text{* While: *}
     3.6  definition "test4_const =
     3.7 - ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
     3.8 + ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
     3.9  
    3.10  text{* While, test is ignored: *}
    3.11  definition "test5_const =
     4.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Wed Oct 19 09:11:21 2011 +0200
     4.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Wed Oct 19 16:32:12 2011 +0200
     4.3 @@ -131,7 +131,7 @@
     4.4  
     4.5  
     4.6  fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
     4.7 -"bfilter (B bv) res S = (if bv=res then S else bot)" |
     4.8 +"bfilter (Bc v) res S = (if v=res then S else bot)" |
     4.9  "bfilter (Not b) res S = bfilter b (\<not> res) S" |
    4.10  "bfilter (And b1 b2) res S =
    4.11    (if res then bfilter b1 True (bfilter b2 True S)
    4.12 @@ -159,7 +159,7 @@
    4.13  
    4.14  lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
    4.15  proof(induction b arbitrary: S bv)
    4.16 -  case B thus ?case by simp
    4.17 +  case Bc thus ?case by simp
    4.18  next
    4.19    case (Not b) thus ?case by simp
    4.20  next
     5.1 --- a/src/HOL/IMP/BExp.thy	Wed Oct 19 09:11:21 2011 +0200
     5.2 +++ b/src/HOL/IMP/BExp.thy	Wed Oct 19 16:32:12 2011 +0200
     5.3 @@ -2,10 +2,10 @@
     5.4  
     5.5  subsection "Boolean Expressions"
     5.6  
     5.7 -datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
     5.8 +datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
     5.9  
    5.10  fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
    5.11 -"bval (B bv) _ = bv" |
    5.12 +"bval (Bc v) _ = v" |
    5.13  "bval (Not b) s = (\<not> bval b s)" |
    5.14  "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" |
    5.15  "bval (Less a1 a2) s = (aval a1 s < aval a2 s)"
    5.16 @@ -19,7 +19,7 @@
    5.17  text{* Optimized constructors: *}
    5.18  
    5.19  fun less :: "aexp \<Rightarrow> aexp \<Rightarrow> bexp" where
    5.20 -"less (N n1) (N n2) = B(n1 < n2)" |
    5.21 +"less (N n1) (N n2) = Bc(n1 < n2)" |
    5.22  "less a1 a2 = Less a1 a2"
    5.23  
    5.24  lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
    5.25 @@ -28,10 +28,10 @@
    5.26  done
    5.27  
    5.28  fun "and" :: "bexp \<Rightarrow> bexp \<Rightarrow> bexp" where
    5.29 -"and (B True) b = b" |
    5.30 -"and b (B True) = b" |
    5.31 -"and (B False) b = B False" |
    5.32 -"and b (B False) = B False" |
    5.33 +"and (Bc True) b = b" |
    5.34 +"and b (Bc True) = b" |
    5.35 +"and (Bc False) b = Bc False" |
    5.36 +"and b (Bc False) = Bc False" |
    5.37  "and b1 b2 = And b1 b2"
    5.38  
    5.39  lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \<and> bval b2 s)"
    5.40 @@ -40,8 +40,8 @@
    5.41  done
    5.42  
    5.43  fun not :: "bexp \<Rightarrow> bexp" where
    5.44 -"not (B True) = B False" |
    5.45 -"not (B False) = B True" |
    5.46 +"not (Bc True) = Bc False" |
    5.47 +"not (Bc False) = Bc True" |
    5.48  "not b = Not b"
    5.49  
    5.50  lemma bval_not[simp]: "bval (not b) s = (~bval b s)"
    5.51 @@ -55,7 +55,7 @@
    5.52  "bsimp (Less a1 a2) = less (asimp a1) (asimp a2)" |
    5.53  "bsimp (And b1 b2) = and (bsimp b1) (bsimp b2)" |
    5.54  "bsimp (Not b) = not(bsimp b)" |
    5.55 -"bsimp (B bv) = B bv"
    5.56 +"bsimp (Bc v) = Bc v"
    5.57  
    5.58  value "bsimp (And (Less (N 0) (N 1)) b)"
    5.59  
     6.1 --- a/src/HOL/IMP/C_like.thy	Wed Oct 19 09:11:21 2011 +0200
     6.2 +++ b/src/HOL/IMP/C_like.thy	Wed Oct 19 16:32:12 2011 +0200
     6.3 @@ -11,10 +11,10 @@
     6.4  "aval (!a) s = s(aval a s)" |
     6.5  "aval (Plus a\<^isub>1 a\<^isub>2) s = aval a\<^isub>1 s + aval a\<^isub>2 s"
     6.6  
     6.7 -datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
     6.8 +datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
     6.9  
    6.10  primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
    6.11 -"bval (B bv) _ = bv" |
    6.12 +"bval (Bc v) _ = v" |
    6.13  "bval (Not b) s = (\<not> bval b s)" |
    6.14  "bval (And b\<^isub>1 b\<^isub>2) s = (if bval b\<^isub>1 s then bval b\<^isub>2 s else False)" |
    6.15  "bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)"
     7.1 --- a/src/HOL/IMP/Comp_Rev.thy	Wed Oct 19 09:11:21 2011 +0200
     7.2 +++ b/src/HOL/IMP/Comp_Rev.thy	Wed Oct 19 16:32:12 2011 +0200
     7.3 @@ -443,7 +443,7 @@
     7.4    shows "i = isize(bcomp b c j) + (if c = bval b s then j else 0) \<and>
     7.5           s' = s \<and> stk' = stk"
     7.6  using assms proof (induction b arbitrary: c j i n s' stk')
     7.7 -  case B thus ?case 
     7.8 +  case Bc thus ?case 
     7.9      by (simp split: split_if_asm add: exec_n_simps)
    7.10  next
    7.11    case (Not b) 
     8.1 --- a/src/HOL/IMP/Compiler.thy	Wed Oct 19 09:11:21 2011 +0200
     8.2 +++ b/src/HOL/IMP/Compiler.thy	Wed Oct 19 16:32:12 2011 +0200
     8.3 @@ -204,7 +204,7 @@
     8.4    by (induct a arbitrary: stk) fastforce+
     8.5  
     8.6  fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
     8.7 -"bcomp (B bv) c n = (if bv=c then [JMP n] else [])" |
     8.8 +"bcomp (Bc v) c n = (if v=c then [JMP n] else [])" |
     8.9  "bcomp (Not b) c n = bcomp b (\<not>c) n" |
    8.10  "bcomp (And b1 b2) c n =
    8.11   (let cb2 = bcomp b2 c n;
     9.1 --- a/src/HOL/IMP/Def_Ass_Exp.thy	Wed Oct 19 09:11:21 2011 +0200
     9.2 +++ b/src/HOL/IMP/Def_Ass_Exp.thy	Wed Oct 19 16:32:12 2011 +0200
     9.3 @@ -18,7 +18,7 @@
     9.4  
     9.5  
     9.6  fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where
     9.7 -"bval (B bv) s = Some bv" |
     9.8 +"bval (Bc v) s = Some v" |
     9.9  "bval (Not b) s = (case bval b s of None \<Rightarrow> None | Some bv \<Rightarrow> Some(\<not> bv))" |
    9.10  "bval (And b\<^isub>1 b\<^isub>2) s = (case (bval b\<^isub>1 s, bval b\<^isub>2 s) of
    9.11    (Some bv\<^isub>1, Some bv\<^isub>2) \<Rightarrow> Some(bv\<^isub>1 & bv\<^isub>2) | _ \<Rightarrow> None)" |
    10.1 --- a/src/HOL/IMP/Fold.thy	Wed Oct 19 09:11:21 2011 +0200
    10.2 +++ b/src/HOL/IMP/Fold.thy	Wed Oct 19 16:32:12 2011 +0200
    10.3 @@ -233,35 +233,35 @@
    10.4  "bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" |
    10.5  "bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" |
    10.6  "bsimp_const (Not b) t = not(bsimp_const b t)" |
    10.7 -"bsimp_const (B bv) _ = B bv"
    10.8 +"bsimp_const (Bc bc) _ = Bc bc"
    10.9  
   10.10  theorem bvalsimp_const [simp]:
   10.11    assumes "approx t s"
   10.12    shows "bval (bsimp_const b t) s = bval b s"
   10.13    using assms by (induct b) auto
   10.14  
   10.15 -lemma not_B [simp]: "not (B v) = B (\<not>v)"
   10.16 +lemma not_Bc [simp]: "not (Bc v) = Bc (\<not>v)"
   10.17    by (cases v) auto
   10.18  
   10.19 -lemma not_B_eq [simp]: "(not b = B v) = (b = B (\<not>v))"
   10.20 +lemma not_Bc_eq [simp]: "(not b = Bc v) = (b = Bc (\<not>v))"
   10.21    by (cases b) auto
   10.22  
   10.23 -lemma and_B_eq: 
   10.24 -  "(and a b = B v) = (a = B False \<and> \<not>v \<or> 
   10.25 -                      b = B False \<and> \<not>v \<or> 
   10.26 -                      (\<exists>v1 v2. a = B v1 \<and> b = B v2 \<and> v = v1 \<and> v2))"
   10.27 +lemma and_Bc_eq: 
   10.28 +  "(and a b = Bc v) =
   10.29 +   (a = Bc False \<and> \<not>v  \<or>  b = Bc False \<and> \<not>v \<or> 
   10.30 +    (\<exists>v1 v2. a = Bc v1 \<and> b = Bc v2 \<and> v = v1 \<and> v2))"
   10.31    by (rule and.induct) auto
   10.32  
   10.33 -lemma less_B_eq [simp]:
   10.34 -  "(less a b = B v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
   10.35 +lemma less_Bc_eq [simp]:
   10.36 +  "(less a b = Bc v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
   10.37    by (rule less.induct) auto
   10.38      
   10.39 -theorem bvalsimp_const_B:
   10.40 +theorem bvalsimp_const_Bc:
   10.41  assumes "approx t s"
   10.42 -shows "bsimp_const b t = B v \<Longrightarrow> bval b s = v"
   10.43 +shows "bsimp_const b t = Bc v \<Longrightarrow> bval b s = v"
   10.44    using assms
   10.45    by (induct b arbitrary: v)
   10.46 -     (auto simp: approx_def and_B_eq aval_simp_const_N 
   10.47 +     (auto simp: approx_def and_Bc_eq aval_simp_const_N 
   10.48             split: bexp.splits bool.splits)
   10.49  
   10.50  
   10.51 @@ -271,8 +271,8 @@
   10.52    (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
   10.53  "bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" |
   10.54  "bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
   10.55 -    B True \<Rightarrow> bdefs c1 t
   10.56 -  | B False \<Rightarrow> bdefs c2 t
   10.57 +    Bc True \<Rightarrow> bdefs c1 t
   10.58 +  | Bc False \<Rightarrow> bdefs c2 t
   10.59    | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
   10.60  "bdefs (WHILE b DO c) t = t |` (-lnames c)" 
   10.61  
   10.62 @@ -282,11 +282,11 @@
   10.63  "bfold (x ::= a) t = (x ::= (simp_const a t))" |
   10.64  "bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))" |
   10.65  "bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
   10.66 -    B True \<Rightarrow> bfold c1 t
   10.67 -  | B False \<Rightarrow> bfold c2 t
   10.68 +    Bc True \<Rightarrow> bfold c1 t
   10.69 +  | Bc False \<Rightarrow> bfold c2 t
   10.70    | _ \<Rightarrow> IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)" |
   10.71  "bfold (WHILE b DO c) t = (case bsimp_const b t of
   10.72 -    B False \<Rightarrow> SKIP
   10.73 +    Bc False \<Rightarrow> SKIP
   10.74    | _ \<Rightarrow> WHILE bsimp_const b (t |` (-lnames c)) DO bfold c (t |` (-lnames c)))"
   10.75  
   10.76  
   10.77 @@ -342,18 +342,18 @@
   10.78    case (IfTrue b s c1 s')
   10.79    hence "approx (bdefs c1 t) s'" by simp
   10.80    thus ?case using `bval b s` `approx t s`
   10.81 -    by (clarsimp simp: approx_merge bvalsimp_const_B 
   10.82 +    by (clarsimp simp: approx_merge bvalsimp_const_Bc
   10.83                   split: bexp.splits bool.splits)
   10.84  next
   10.85    case (IfFalse b s c2 s')
   10.86    hence "approx (bdefs c2 t) s'" by simp
   10.87    thus ?case using `\<not>bval b s` `approx t s`
   10.88 -    by (clarsimp simp: approx_merge bvalsimp_const_B 
   10.89 +    by (clarsimp simp: approx_merge bvalsimp_const_Bc
   10.90                   split: bexp.splits bool.splits)
   10.91  next
   10.92    case WhileFalse
   10.93    thus ?case 
   10.94 -    by (clarsimp simp: bvalsimp_const_B approx_def restrict_map_def
   10.95 +    by (clarsimp simp: bvalsimp_const_Bc approx_def restrict_map_def
   10.96                   split: bexp.splits bool.splits)
   10.97  next
   10.98    case (WhileTrue b s1 c s2 s3)
   10.99 @@ -385,7 +385,7 @@
  10.100                     IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
  10.101      by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) 
  10.102    thus ?case using If
  10.103 -    by (fastforce simp: bvalsimp_const_B split: bexp.splits bool.splits 
  10.104 +    by (fastforce simp: bvalsimp_const_Bc split: bexp.splits bool.splits 
  10.105                   intro: equiv_up_to_trans)
  10.106    next
  10.107    case (While b c)
  10.108 @@ -400,7 +400,7 @@
  10.109    thus ?case
  10.110      by (auto split: bexp.splits bool.splits 
  10.111               intro: equiv_up_to_while_False 
  10.112 -             simp: bvalsimp_const_B)
  10.113 +             simp: bvalsimp_const_Bc)
  10.114  qed
  10.115  
  10.116  
    11.1 --- a/src/HOL/IMP/Poly_Types.thy	Wed Oct 19 09:11:21 2011 +0200
    11.2 +++ b/src/HOL/IMP/Poly_Types.thy	Wed Oct 19 16:32:12 2011 +0200
    11.3 @@ -18,7 +18,7 @@
    11.4  
    11.5  inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>p" 50)
    11.6  where
    11.7 -"\<Gamma> \<turnstile>p B bv" |
    11.8 +"\<Gamma> \<turnstile>p Bc v" |
    11.9  "\<Gamma> \<turnstile>p b \<Longrightarrow> \<Gamma> \<turnstile>p Not b" |
   11.10  "\<Gamma> \<turnstile>p b1 \<Longrightarrow> \<Gamma> \<turnstile>p b2 \<Longrightarrow> \<Gamma> \<turnstile>p And b1 b2" |
   11.11  "\<Gamma> \<turnstile>p a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile>p Less a1 a2"
    12.1 --- a/src/HOL/IMP/Sec_Type_Expr.thy	Wed Oct 19 09:11:21 2011 +0200
    12.2 +++ b/src/HOL/IMP/Sec_Type_Expr.thy	Wed Oct 19 16:32:12 2011 +0200
    12.3 @@ -20,7 +20,7 @@
    12.4  "sec_aexp (Plus a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
    12.5  
    12.6  fun sec_bexp :: "bexp \<Rightarrow> level" where
    12.7 -"sec_bexp (B bv) = 0" |
    12.8 +"sec_bexp (Bc v) = 0" |
    12.9  "sec_bexp (Not b) = sec_bexp b" |
   12.10  "sec_bexp (And b\<^isub>1 b\<^isub>2) = max (sec_bexp b\<^isub>1) (sec_bexp b\<^isub>2)" |
   12.11  "sec_bexp (Less a\<^isub>1 a\<^isub>2) = max (sec_aexp a\<^isub>1) (sec_aexp a\<^isub>2)"
    13.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Wed Oct 19 09:11:21 2011 +0200
    13.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Wed Oct 19 16:32:12 2011 +0200
    13.3 @@ -152,11 +152,11 @@
    13.4    "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
    13.5    by (auto simp: equiv_up_to_def)
    13.6  
    13.7 -lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (B True) DO c'"
    13.8 +lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (Bc True) DO c'"
    13.9   by (induct rule: big_step_induct) auto
   13.10    
   13.11  lemma equiv_up_to_while_True [intro!,simp]:
   13.12 -  "P \<Turnstile> WHILE B True DO c \<sim> WHILE B True DO SKIP"
   13.13 +  "P \<Turnstile> WHILE Bc True DO c \<sim> WHILE Bc True DO SKIP"
   13.14    unfolding equiv_up_to_def
   13.15    by (blast dest: while_never)
   13.16  
    14.1 --- a/src/HOL/IMP/Types.thy	Wed Oct 19 09:11:21 2011 +0200
    14.2 +++ b/src/HOL/IMP/Types.thy	Wed Oct 19 16:32:12 2011 +0200
    14.3 @@ -27,10 +27,10 @@
    14.4  
    14.5  subsection "Boolean Expressions"
    14.6  
    14.7 -datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
    14.8 +datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
    14.9  
   14.10  inductive tbval :: "bexp \<Rightarrow> state \<Rightarrow> bool \<Rightarrow> bool" where
   14.11 -"tbval (B bv) s bv" |
   14.12 +"tbval (Bc v) s v" |
   14.13  "tbval b s bv \<Longrightarrow> tbval (Not b) s (\<not> bv)" |
   14.14  "tbval b1 s bv1 \<Longrightarrow> tbval b2 s bv2 \<Longrightarrow> tbval (And b1 b2) s (bv1 & bv2)" |
   14.15  "taval a1 s (Iv i1) \<Longrightarrow> taval a2 s (Iv i2) \<Longrightarrow> tbval (Less a1 a2) s (i1 < i2)" |
   14.16 @@ -85,7 +85,7 @@
   14.17  
   14.18  inductive btyping :: "tyenv \<Rightarrow> bexp \<Rightarrow> bool" (infix "\<turnstile>" 50)
   14.19  where
   14.20 -B_ty: "\<Gamma> \<turnstile> B bv" |
   14.21 +B_ty: "\<Gamma> \<turnstile> Bc v" |
   14.22  Not_ty: "\<Gamma> \<turnstile> b \<Longrightarrow> \<Gamma> \<turnstile> Not b" |
   14.23  And_ty: "\<Gamma> \<turnstile> b1 \<Longrightarrow> \<Gamma> \<turnstile> b2 \<Longrightarrow> \<Gamma> \<turnstile> And b1 b2" |
   14.24  Less_ty: "\<Gamma> \<turnstile> a1 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> a2 : \<tau> \<Longrightarrow> \<Gamma> \<turnstile> Less a1 a2"
    15.1 --- a/src/HOL/IMP/Vars.thy	Wed Oct 19 09:11:21 2011 +0200
    15.2 +++ b/src/HOL/IMP/Vars.thy	Wed Oct 19 16:32:12 2011 +0200
    15.3 @@ -41,7 +41,7 @@
    15.4  begin
    15.5  
    15.6  fun vars_bexp :: "bexp \<Rightarrow> name set" where
    15.7 -"vars_bexp (B bv) = {}" |
    15.8 +"vars_bexp (Bc v) = {}" |
    15.9  "vars_bexp (Not b) = vars_bexp b" |
   15.10  "vars_bexp (And b\<^isub>1 b\<^isub>2) = vars_bexp b\<^isub>1 \<union> vars_bexp b\<^isub>2" |
   15.11  "vars_bexp (Less a\<^isub>1 a\<^isub>2) = vars a\<^isub>1 \<union> vars a\<^isub>2"