# HG changeset patch
# User wenzelm
# Date 1319046319 -7200
# Node ID fe8d0706a8aa2612350c320b19d86b63d51e9c5c
# Parent  2825ce94fd4d1d345d554c9064266c65f6170c25# Parent  42316b81ef49b5f905fa8201ee08c3be11d3e954
merged

diff -r 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Abs_Int0_const.thy
--- a/src/HOL/IMP/Abs_Int0_const.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Abs_Int0_const.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa 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 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/BExp.thy
--- a/src/HOL/IMP/BExp.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/BExp.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/C_like.thy
--- a/src/HOL/IMP/C_like.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/C_like.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Compiler.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Def_Ass_Exp.thy
--- a/src/HOL/IMP/Def_Ass_Exp.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Def_Ass_Exp.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Fold.thy
--- a/src/HOL/IMP/Fold.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Fold.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Poly_Types.thy
--- a/src/HOL/IMP/Poly_Types.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Poly_Types.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Sec_Type_Expr.thy
--- a/src/HOL/IMP/Sec_Type_Expr.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Sec_Type_Expr.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Sem_Equiv.thy
--- a/src/HOL/IMP/Sem_Equiv.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Sem_Equiv.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Types.thy
--- a/src/HOL/IMP/Types.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Types.thy	Wed Oct 19 19:45:19 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 42316b81ef49 -r fe8d0706a8aa src/HOL/IMP/Vars.thy
--- a/src/HOL/IMP/Vars.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/IMP/Vars.thy	Wed Oct 19 19:45:19 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"
diff -r 42316b81ef49 -r fe8d0706a8aa src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/Product_Type.thy	Wed Oct 19 19:45:19 2011 +0200
@@ -1135,4 +1135,6 @@
 
 lemmas Pair_fst_snd_eq = prod_eq_iff
 
+hide_const (open) prod
+
 end
diff -r 42316b81ef49 -r fe8d0706a8aa src/HOL/Sum_Type.thy
--- a/src/HOL/Sum_Type.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/Sum_Type.thy	Wed Oct 19 19:45:19 2011 +0200
@@ -209,4 +209,6 @@
 
 hide_const (open) Suml Sumr Projl Projr
 
+hide_const (open) sum
+
 end
diff -r 42316b81ef49 -r fe8d0706a8aa src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Oct 19 19:45:19 2011 +0200
@@ -467,13 +467,12 @@
                     map (swap o `(resolve_spass_num spass_names)) deps))
 
 (* Syntax: <name> *)
-fun parse_satallax_line problem =
-  scan_general_id --| Scan.option ($$ " ")
-  >> (fn s => Inference ((s, SOME [s]), dummy_phi, []))
+fun parse_satallax_line x =
+  (scan_general_id --| Scan.option ($$ " ")
+   >> (fn s => Inference ((s, SOME [s]), dummy_phi, []))) x
 
 fun parse_line problem spass_names =
-  parse_tstp_line problem || parse_spass_line spass_names
-  || parse_satallax_line problem
+  parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line
 fun parse_proof problem spass_names tstp =
   tstp |> strip_spaces_except_between_idents
        |> raw_explode
diff -r 42316b81ef49 -r fe8d0706a8aa src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Oct 19 19:45:19 2011 +0200
@@ -101,6 +101,24 @@
    (NoPerl, "env: perl"),
    (NoLibwwwPerl, "Can't locate HTTP")]
 
+fun known_szs_failures wrap =
+  [(Unprovable, wrap "CounterSatisfiable"),
+   (Unprovable, wrap "Satisfiable"),
+   (GaveUp, wrap "GaveUp"),
+   (GaveUp, wrap "Unknown"),
+   (GaveUp, wrap "Incomplete"),
+   (ProofMissing, wrap "Theorem"),
+   (ProofMissing, wrap "Unsatisfiable"),
+   (TimedOut, wrap "Timeout"),
+   (Inappropriate, wrap "Inappropriate"),
+   (OutOfResources, wrap "ResourceOut"),
+   (OutOfResources, wrap "MemoryOut"),
+   (Interrupted, wrap "Forced"),
+   (Interrupted, wrap "User")]
+
+val known_szs_status_failures = known_szs_failures (prefix "SZS status ")
+val known_says_failures = known_szs_failures (prefix " says ")
+
 (* named ATPs *)
 
 val eN = "e"
@@ -208,14 +226,10 @@
         " -tAutoDev --silent --cpu-limit=" ^ string_of_int (to_secs 2 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
-     [(Unprovable, "SZS status: CounterSatisfiable"),
-      (Unprovable, "SZS status CounterSatisfiable"),
-      (ProofMissing, "SZS status Theorem"),
-      (TimedOut, "Failure: Resource limit exceeded (time)"),
+     known_szs_status_failures @
+     [(TimedOut, "Failure: Resource limit exceeded (time)"),
       (TimedOut, "time limit exceeded"),
-      (OutOfResources, "# Cannot determine problem status"),
-      (OutOfResources, "SZS status: ResourceOut"),
-      (OutOfResources, "SZS status ResourceOut")],
+      (OutOfResources, "# Cannot determine problem status")],
    conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>
@@ -244,7 +258,7 @@
         "--proofoutput --timeout " ^ string_of_int (to_secs 1 timeout)
         |> sos = sosN ? prefix "--sos ",
    proof_delims = tstp_proof_delims,
-   known_failures = [],
+   known_failures = known_szs_status_failures,
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices = fn ctxt =>
@@ -269,7 +283,7 @@
         "-p hocore -t " ^ string_of_int (to_secs 1 timeout),
    proof_delims =
      [("% Higher-Order Unsat Core BEGIN", "% Higher-Order Unsat Core END")],
-   known_failures = [],
+   known_failures = known_szs_status_failures,
    conj_sym_kind = Axiom,
    prem_kind = Hypothesis,
    best_slices =
@@ -337,10 +351,9 @@
       ("% SZS output start Refutation", "% SZS output end Refutation"),
       ("% SZS output start Proof", "% SZS output end Proof")],
    known_failures =
+     known_szs_status_failures @
      [(GaveUp, "UNPROVABLE"),
       (GaveUp, "CANNOT PROVE"),
-      (GaveUp, "SZS status GaveUp"),
-      (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),
       (VampireTooOld, "not a valid option"),
@@ -373,13 +386,7 @@
    arguments = fn _ => fn _ => fn _ => fn timeout => fn _ =>
      "MBQI=true -tptp -t:" ^ string_of_int (to_secs 1 timeout),
    proof_delims = [],
-   known_failures =
-     [(GaveUp, "SZS status Satisfiable"),
-      (GaveUp, "SZS status CounterSatisfiable"),
-      (GaveUp, "SZS status GaveUp"),
-      (GaveUp, "SZS status Unknown"),
-      (ProofMissing, "SZS status Unsatisfiable"),
-      (ProofMissing, "SZS status Theorem")],
+   known_failures = known_szs_status_failures,
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices =
@@ -399,7 +406,7 @@
    required_execs = [],
    arguments = K (K (K (K (K "")))),
    proof_delims = [],
-   known_failures = [(GaveUp, "SZS status Unknown")],
+   known_failures = known_szs_status_failures,
    conj_sym_kind = Hypothesis,
    prem_kind = Hypothesis,
    best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
@@ -456,15 +463,7 @@
      "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout))
      ^ " -s " ^ the_system system_name system_versions,
    proof_delims = union (op =) tstp_proof_delims proof_delims,
-   known_failures = known_failures @ known_perl_failures @
-     [(Unprovable, "says Satisfiable"),
-      (Unprovable, "says CounterSatisfiable"),
-      (GaveUp, "says Unknown"),
-      (GaveUp, "says GaveUp"),
-      (ProofMissing, "says Theorem"),
-      (ProofMissing, "says Unsatisfiable"),
-      (TimedOut, "says Timeout"),
-      (Inappropriate, "says Inappropriate")],
+   known_failures = known_failures @ known_perl_failures @ known_says_failures,
    conj_sym_kind = conj_sym_kind,
    prem_kind = prem_kind,
    best_slices = fn ctxt =>
diff -r 42316b81ef49 -r fe8d0706a8aa src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Oct 19 19:45:19 2011 +0200
@@ -1165,20 +1165,22 @@
       | freeze t = t
   in t |> exists_subterm is_Var t ? freeze end
 
-fun presimp_prop ctxt presimp_consts t =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val t = t |> Envir.beta_eta_contract
-              |> transform_elim_prop
-              |> Object_Logic.atomize_term thy
-    val need_trueprop = (fastype_of t = @{typ bool})
-  in
-    t |> need_trueprop ? HOLogic.mk_Trueprop
-      |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
-      |> extensionalize_term ctxt
-      |> presimplify_term ctxt presimp_consts
-      |> perhaps (try (HOLogic.dest_Trueprop))
-  end
+fun presimp_prop ctxt presimp_consts role t =
+  (let
+     val thy = Proof_Context.theory_of ctxt
+     val t = t |> Envir.beta_eta_contract
+               |> transform_elim_prop
+               |> Object_Logic.atomize_term thy
+     val need_trueprop = (fastype_of t = @{typ bool})
+   in
+     t |> need_trueprop ? HOLogic.mk_Trueprop
+       |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
+       |> extensionalize_term ctxt
+       |> presimplify_term ctxt presimp_consts
+       |> HOLogic.dest_Trueprop
+   end
+   handle TERM _ => if role = Conjecture then @{term False} else @{term True})
+  |> pair role
 
 (* making fact and conjecture formulas *)
 fun make_formula ctxt format type_enc eq_as_iff name loc kind t =
@@ -1199,7 +1201,8 @@
   | formula => SOME formula
 
 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
-  | s_not_trueprop t = s_not t
+  | s_not_trueprop t =
+    if fastype_of t = @{typ bool} then s_not t else @{prop False} (* too meta *)
 
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, loc), (kind, t)) =>
@@ -1659,7 +1662,7 @@
     val ((conjs, facts), lambdas) =
       if preproc then
         conjs @ facts
-        |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
+        |> map (apsnd (uncurry (presimp_prop ctxt presimp_consts)))
         |> preprocess_abstractions_in_terms trans_lambdas
         |>> chop (length conjs)
       else
diff -r 42316b81ef49 -r fe8d0706a8aa src/HOL/ex/Meson_Test.thy
--- a/src/HOL/ex/Meson_Test.thy	Wed Oct 19 17:04:43 2011 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Wed Oct 19 19:45:19 2011 +0200
@@ -10,7 +10,7 @@
   below and constants declared in HOL!
 *}
 
-hide_const (open) implies union inter subset sum quotient
+hide_const (open) implies union inter subset quotient
 
 text {*
   Test data for the MESON proof procedure