--- 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 =
--- 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
--- 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 =
--- 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
--- 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)"
--- 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)"
--- 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)
--- 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;
--- 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)" |
--- 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
--- 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"
--- 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)"
--- 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)
--- 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"
--- 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"