merge
authorblanchet
Fri, 04 Jun 2010 16:55:25 +0200
changeset 37333 81f058f2d2ff
parent 37332 51d99ba6fc4d (diff)
parent 37317 5164c4ec787b (current diff)
child 37334 00bfa4276d9c
merge
--- a/src/HOL/Metis_Examples/BigO.thy	Fri Jun 04 16:42:26 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy	Fri Jun 04 16:55:25 2010 +0200
@@ -880,25 +880,18 @@
 (* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less
                 le_max_iff_disj min_max.le_supE min_max.sup_absorb2
                 min_max.sup_commute) *)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>A. k A \<le> f A"
-have 1: "\<And>(X1\<Colon>'b\<Colon>linordered_idom) X2. \<not> max X1 X2 < X1"
-  by (metis linorder_not_less le_maxI1)  (*sort inserted by hand*)
-assume 2: "(0\<Colon>'b) \<le> k x - g x"
-have 3: "\<not> k x - g x < (0\<Colon>'b)"
-  by (metis 2 linorder_not_less)
-have 4: "\<And>X1 X2. min X1 (k X2) \<le> f X2"
-  by (metis min_max.inf_le2 min_max.le_inf_iff min_max.le_iff_inf 0)
-have 5: "\<bar>g x - f x\<bar> = f x - g x"
-  by (metis abs_minus_commute combine_common_factor mult_zero_right minus_add_cancel minus_zero abs_if diff_less_eq min_max.inf_commute 4 linorder_not_le min_max.le_iff_inf 3 diff_less_0_iff_less linorder_not_less)
-have 6: "max (0\<Colon>'b) (k x - g x) = k x - g x"
-  by (metis min_max.le_iff_sup 2)
-assume 7: "\<not> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
-have 8: "\<not> k x - g x \<le> f x - g x"
-  by (metis 5 abs_minus_commute 7 min_max.sup_commute 6)
-show "False"
-  by (metis min_max.sup_commute min_max.inf_commute min_max.sup_inf_absorb min_max.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)
+proof -
+  fix x :: 'a
+  assume "\<forall>x\<Colon>'a. k x \<le> f x"
+  hence F1: "\<forall>x\<^isub>1\<Colon>'a. max (k x\<^isub>1) (f x\<^isub>1) = f x\<^isub>1" by (metis min_max.sup_absorb2)
+  assume "(0\<Colon>'b) \<le> k x - g x"
+  hence F2: "max (0\<Colon>'b) (k x - g x) = k x - g x" by (metis min_max.sup_absorb2)
+  have F3: "\<forall>x\<^isub>1\<Colon>'b. x\<^isub>1 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_le_iff le_less)
+  have "\<forall>(x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>2 \<or> max x\<^isub>1 x\<^isub>2 \<le> x\<^isub>1" by (metis le_less le_max_iff_disj)
+  hence "\<forall>(x\<^isub>3\<Colon>'b) (x\<^isub>2\<Colon>'b) x\<^isub>1\<Colon>'b. x\<^isub>1 - x\<^isub>2 \<le> x\<^isub>3 - x\<^isub>2 \<or> x\<^isub>3 \<le> x\<^isub>1" by (metis add_le_imp_le_right diff_minus min_max.le_supE)
+  hence "k x - g x \<le> f x - g x" by (metis F1 le_less min_max.sup_absorb2 min_max.sup_commute)
+  hence "k x - g x \<le> \<bar>f x - g x\<bar>" by (metis F3 le_max_iff_disj min_max.sup_absorb2)
+  thus "max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>" by (metis F2 min_max.sup_commute)
 next
   show "\<And>x\<Colon>'a.
        \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>
--- a/src/HOL/Metis_Examples/set.thy	Fri Jun 04 16:42:26 2010 +0200
+++ b/src/HOL/Metis_Examples/set.thy	Fri Jun 04 16:55:25 2010 +0200
@@ -21,242 +21,164 @@
 (*multiple versions of this example*)
 lemma (*equal_union: *)
    "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
-proof (neg_clausify)
-fix x
-assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
-assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
-assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
-have 6: "sup Y Z = X \<or> Y \<subseteq> X"
-  by (metis 0)
-have 7: "sup Y Z = X \<or> Z \<subseteq> X"
-  by (metis 1)
-have 8: "\<And>X3. sup Y Z = X \<or> X \<subseteq> X3 \<or> \<not> Y \<subseteq> X3 \<or> \<not> Z \<subseteq> X3"
-  by (metis 5)
-have 9: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 2)
-have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 3)
-have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 4)
-have 12: "Z \<subseteq> X"
-  by (metis Un_upper2 7)
-have 13: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
-  by (metis 8 Un_upper2)
-have 14: "Y \<subseteq> X"
-  by (metis Un_upper1 6)
-have 15: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 10 12)
-have 16: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 9 12)
-have 17: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
-  by (metis 11 12)
-have 18: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x"
-  by (metis 17 14)
-have 19: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 15 14)
-have 20: "Y \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 16 14)
-have 21: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
-  by (metis 13 Un_upper1)
-have 22: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
-  by (metis equalityI 21)
-have 23: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 22 Un_least)
-have 24: "sup Y Z = X \<or> \<not> Y \<subseteq> X"
-  by (metis 23 12)
-have 25: "sup Y Z = X"
-  by (metis 24 14)
-have 26: "\<And>X3. X \<subseteq> X3 \<or> \<not> Z \<subseteq> X3 \<or> \<not> Y \<subseteq> X3"
-  by (metis Un_least 25)
-have 27: "Y \<subseteq> x"
-  by (metis 20 25)
-have 28: "Z \<subseteq> x"
-  by (metis 19 25)
-have 29: "\<not> X \<subseteq> x"
-  by (metis 18 25)
-have 30: "X \<subseteq> x \<or> \<not> Y \<subseteq> x"
-  by (metis 26 28)
-have 31: "X \<subseteq> x"
-  by (metis 30 27)
-show "False"
-  by (metis 31 29)
+proof -
+  have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>1 \<union> x\<^isub>2" by (metis Un_commute Un_upper2)
+  have F2a: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq)
+  have F2: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis F2a subset_Un_eq)
+  { assume "\<not> Z \<subseteq> X"
+    hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+  moreover
+  { assume AA1: "Y \<union> Z \<noteq> X"
+    { assume "\<not> Y \<subseteq> X"
+      hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
+    moreover
+    { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
+      { assume "\<not> Z \<subseteq> X"
+        hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+      moreover
+      { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
+        hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff)
+        hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2)
+        hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1)
+        hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+      ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) }
+    ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1) }
+  moreover
+  { assume "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
+    { assume "\<not> Y \<subseteq> X"
+      hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
+    moreover
+    { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
+      { assume "\<not> Z \<subseteq> X"
+        hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+      moreover
+      { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
+        hence "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z" by (metis Un_subset_iff)
+        hence "Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> Y \<union> Z" by (metis F2)
+        hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1)
+        hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+      ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1) }
+    ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by blast }
+  moreover
+  { assume "\<not> Y \<subseteq> X"
+    hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1) }
+  ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
 qed
 
 sledgehammer_params [isar_proof, isar_shrink_factor = 2]
 
 lemma (*equal_union: *)
-   "(X = Y \<union> Z) =
-    (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
-proof (neg_clausify)
-fix x
-assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
-assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
-assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
-have 6: "sup Y Z = X \<or> Y \<subseteq> X"
-  by (metis 0)
-have 7: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 2)
-have 8: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 4)
-have 9: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
-  by (metis 5 Un_upper2)
-have 10: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 3 Un_upper2)
-have 11: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X"
-  by (metis 8 Un_upper2)
-have 12: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 10 Un_upper1)
-have 13: "sup Y Z = X \<or> X \<subseteq> sup Y Z"
-  by (metis 9 Un_upper1)
-have 14: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis equalityI 13 Un_least)
-have 15: "sup Y Z = X"
-  by (metis 14 1 6)
-have 16: "Y \<subseteq> x"
-  by (metis 7 Un_upper2 Un_upper1 15)
-have 17: "\<not> X \<subseteq> x"
-  by (metis 11 Un_upper1 15)
-have 18: "X \<subseteq> x"
-  by (metis Un_least 15 12 15 16)
-show "False"
-  by (metis 18 17)
+   "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
+proof -
+  have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq)
+  { assume AA1: "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
+    { assume AAA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
+      { assume "\<not> Z \<subseteq> X"
+        hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+      moreover
+      { assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z"
+        hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1 Un_commute Un_upper2)
+        hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+      ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AAA1 Un_subset_iff) }
+    moreover
+    { assume "\<not> Y \<subseteq> X"
+      hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
+    ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) }
+  moreover
+  { assume "\<not> Z \<subseteq> X"
+    hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+  moreover
+  { assume "\<not> Y \<subseteq> X"
+    hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
+  moreover
+  { assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
+    { assume "\<not> Z \<subseteq> X"
+      hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+    moreover
+    { assume "Y \<union> Z \<subseteq> X \<and> X \<noteq> Y \<union> Z"
+      hence "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z" by (metis F1 Un_commute Un_upper2)
+      hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+    ultimately have "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_subset_iff) }
+  ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by metis
 qed
 
 sledgehammer_params [isar_proof, isar_shrink_factor = 3]
 
 lemma (*equal_union: *)
-   "(X = Y \<union> Z) =
-    (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
-proof (neg_clausify)
-fix x
-assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
-assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
-assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
-have 6: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 3)
-have 7: "\<And>X3. sup Y Z = X \<or> X \<subseteq> sup X3 Z \<or> \<not> Y \<subseteq> sup X3 Z"
-  by (metis 5 Un_upper2)
-have 8: "Y \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 2 Un_upper2)
-have 9: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 6 Un_upper2 Un_upper1)
-have 10: "sup Y Z = X \<or> \<not> sup Y Z \<subseteq> X"
-  by (metis equalityI 7 Un_upper1)
-have 11: "sup Y Z = X"
-  by (metis 10 Un_least 1 0)
-have 12: "Z \<subseteq> x"
-  by (metis 9 11)
-have 13: "X \<subseteq> x"
-  by (metis Un_least 11 12 8 Un_upper1 11)
-show "False"
-  by (metis 13 4 Un_upper2 Un_upper1 11)
+   "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
+proof -
+  have F1a: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<longrightarrow> x\<^isub>2 = x\<^isub>2 \<union> x\<^isub>1" by (metis Un_commute subset_Un_eq)
+  have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis F1a subset_Un_eq)
+  { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
+    hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) }
+  moreover
+  { assume AA1: "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. (Z \<subseteq> x\<^isub>1 \<and> Y \<subseteq> x\<^isub>1) \<and> \<not> X \<subseteq> x\<^isub>1"
+    { assume "(Z \<subseteq> X \<and> Y \<subseteq> X) \<and> Y \<union> Z \<noteq> X"
+      hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis F1 Un_commute Un_subset_iff Un_upper2) }
+    hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 Un_commute Un_subset_iff Un_upper2) }
+  ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2)
 qed
 
-(*Example included in TPHOLs paper*)
-
 sledgehammer_params [isar_proof, isar_shrink_factor = 4]
 
 lemma (*equal_union: *)
-   "(X = Y \<union> Z) =
-    (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
-proof (neg_clausify)
-fix x
-assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
-assume 1: "Z \<subseteq> X \<or> X = Y \<union> Z"
-assume 2: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Y \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 3: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> Z \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 4: "(\<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X \<or> \<not> X \<subseteq> x) \<or> X \<noteq> Y \<union> Z"
-assume 5: "\<And>V. ((\<not> Y \<subseteq> V \<or> \<not> Z \<subseteq> V) \<or> X \<subseteq> V) \<or> X = Y \<union> Z"
-have 6: "sup Y Z \<noteq> X \<or> \<not> X \<subseteq> x \<or> \<not> Y \<subseteq> X \<or> \<not> Z \<subseteq> X"
-  by (metis 4)
-have 7: "Z \<subseteq> x \<or> sup Y Z \<noteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis 3 Un_upper2)
-have 8: "Z \<subseteq> x \<or> sup Y Z \<noteq> X"
-  by (metis 7 Un_upper1)
-have 9: "sup Y Z = X \<or> \<not> Z \<subseteq> X \<or> \<not> Y \<subseteq> X"
-  by (metis equalityI 5 Un_upper2 Un_upper1 Un_least)
-have 10: "Y \<subseteq> x"
-  by (metis 2 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
-have 11: "X \<subseteq> x"
-  by (metis Un_least 9 Un_upper2 1 Un_upper1 0 8 9 Un_upper2 1 Un_upper1 0 10)
-show "False"
-  by (metis 11 6 Un_upper2 1 Un_upper1 0 9 Un_upper2 1 Un_upper1 0)
-qed 
+   "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
+proof -
+  have F1: "\<forall>(x\<^isub>2\<Colon>'b \<Rightarrow> bool) x\<^isub>1\<Colon>'b \<Rightarrow> bool. x\<^isub>1 \<subseteq> x\<^isub>2 \<and> x\<^isub>2 \<subseteq> x\<^isub>1 \<longrightarrow> x\<^isub>1 = x\<^isub>2" by (metis Un_commute subset_Un_eq)
+  { assume "\<not> Y \<subseteq> X"
+    hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_commute Un_upper2) }
+  moreover
+  { assume AA1: "Y \<subseteq> X \<and> Y \<union> Z \<noteq> X"
+    { assume "\<exists>x\<^isub>1\<Colon>'a \<Rightarrow> bool. Y \<subseteq> x\<^isub>1 \<union> Z \<and> Y \<union> Z \<noteq> X \<and> \<not> X \<subseteq> x\<^isub>1 \<union> Z"
+      hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_upper2) }
+    hence "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis AA1 F1 Un_commute Un_subset_iff Un_upper2) }
+  ultimately show "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V\<Colon>'a \<Rightarrow> bool. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" by (metis Un_subset_iff Un_upper2)
+qed
 
-declare [[ atp_problem_prefix = "set__equal_union" ]]
+sledgehammer_params [isar_proof, isar_shrink_factor = 1]
+
 lemma (*equal_union: *)
-   "(X = Y \<union> Z) =
-    (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))" 
-(*One shot proof: hand-reduced. Metis can't do the full proof any more.*)
+   "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
 by (metis Un_least Un_upper1 Un_upper2 set_eq_subset)
 
+lemma "(X = Y \<inter> Z) = (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
+by (metis Int_greatest Int_lower1 Int_lower2 subset_antisym)
 
-declare [[ atp_problem_prefix = "set__equal_inter" ]]
-lemma "(X = Y \<inter> Z) =
-    (X \<subseteq> Y \<and> X \<subseteq> Z \<and> (\<forall>V. V \<subseteq> Y \<and> V \<subseteq> Z \<longrightarrow> V \<subseteq> X))"
-by (metis Int_greatest Int_lower1 Int_lower2 set_eq_subset)
-
-declare [[ atp_problem_prefix = "set__fixedpoint" ]]
-lemma fixedpoint:
-    "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
+lemma fixedpoint: "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
 by metis
 
-lemma (*fixedpoint:*)
-    "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
-proof (neg_clausify)
-fix x xa
-assume 0: "f (g x) = x"
-assume 1: "\<And>y. y = x \<or> f (g y) \<noteq> y"
-assume 2: "\<And>x. g (f (xa x)) = xa x \<or> g (f x) \<noteq> x"
-assume 3: "\<And>x. g (f x) \<noteq> x \<or> xa x \<noteq> x"
-have 4: "\<And>X1. g (f X1) \<noteq> X1 \<or> g x \<noteq> X1"
-  by (metis 3 1 2)
-show "False"
-  by (metis 4 0)
+lemma (* fixedpoint: *) "\<exists>!x. f (g x) = x \<Longrightarrow> \<exists>!y. g (f y) = y"
+proof -
+  assume "\<exists>!x\<Colon>'a. f (g x) = x"
+  thus "\<exists>!y\<Colon>'b. g (f y) = y" by metis
 qed
 
-declare [[ atp_problem_prefix = "set__singleton_example" ]]
-lemma (*singleton_example_2:*)
+lemma (* singleton_example_2: *)
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
 by (metis Set.subsetI Union_upper insertCI set_eq_subset)
-  --{*found by SPASS*}
 
-lemma (*singleton_example_2:*)
+lemma (* singleton_example_2: *)
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
 by (metis Set.subsetI Union_upper insert_iff set_eq_subset)
 
 lemma singleton_example_2:
      "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-proof (neg_clausify)
-assume 0: "\<And>x. \<not> S \<subseteq> {x}"
-assume 1: "\<And>x. x \<notin> S \<or> \<Union>S \<subseteq> x"
-have 2: "\<And>X3. X3 = \<Union>S \<or> \<not> X3 \<subseteq> \<Union>S \<or> X3 \<notin> S"
-  by (metis set_eq_subset 1)
-have 3: "\<And>X3. S \<subseteq> insert (\<Union>S) X3"
-  by (metis insert_iff Set.subsetI Union_upper 2 Set.subsetI)
-show "False"
-  by (metis 3 0)
+proof -
+  assume "\<forall>x \<in> S. \<Union>S \<subseteq> x"
+  hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> \<Union>S \<and> x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis set_eq_subset)
+  hence "\<forall>x\<^isub>1. x\<^isub>1 \<in> S \<longrightarrow> x\<^isub>1 = \<Union>S" by (metis Union_upper)
+  hence "\<forall>x\<^isub>1\<Colon>('a \<Rightarrow> bool) \<Rightarrow> bool. \<Union>S \<in> x\<^isub>1 \<longrightarrow> S \<subseteq> x\<^isub>1" by (metis subsetI)
+  hence "\<forall>x\<^isub>1\<Colon>('a \<Rightarrow> bool) \<Rightarrow> bool. S \<subseteq> insert (\<Union>S) x\<^isub>1" by (metis insert_iff)
+  thus "\<exists>z. S \<subseteq> {z}" by metis
 qed
 
-
-
 text {*
   From W. W. Bledsoe and Guohui Feng, SET-VAR. JAR 11 (3), 1993, pages
   293-314.
 *}
 
-declare [[ atp_problem_prefix = "set__Bledsoe_Fung" ]]
-(*Notes: 1, the numbering doesn't completely agree with the paper. 
-2, we must rename set variables to avoid type clashes.*)
+(* Notes: (1) The numbering doesn't completely agree with the paper.
+   (2) We must rename set variables to avoid type clashes. *)
 lemma "\<exists>B. (\<forall>x \<in> B. x \<le> (0::int))"
       "D \<in> F \<Longrightarrow> \<exists>G. \<forall>A \<in> G. \<exists>B \<in> F. A \<subseteq> B"
       "P a \<Longrightarrow> \<exists>A. (\<forall>x \<in> A. P x) \<and> (\<exists>y. y \<in> A)"
@@ -265,13 +187,13 @@
       "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
       "\<exists>A. a \<notin> A"
       "(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m"
-apply (metis all_not_in_conv)+
-apply (metis mem_def)
-apply (metis insertCI singletonE zless_le)
-apply (metis Collect_def Collect_mem_eq)
-apply (metis Collect_def Collect_mem_eq)
-apply (metis DiffE)
-apply (metis pair_in_Id_conv)
-done
+       apply (metis all_not_in_conv)
+      apply (metis all_not_in_conv)
+     apply (metis mem_def)
+    apply (metis less_int_def singleton_iff)
+   apply (metis mem_def)
+  apply (metis mem_def)
+ apply (metis all_not_in_conv)
+by (metis pair_in_Id_conv)
 
 end
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 04 16:42:26 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Jun 04 16:55:25 2010 +0200
@@ -275,6 +275,7 @@
       ("% SZS output start Refutation", "% SZS output end Refutation")],
    known_failures =
      [(Unprovable, "Satisfiability detected"),
+      (Unprovable, "UNPROVABLE"),
       (OutOfResources, "CANNOT PROVE"),
       (OutOfResources, "Refutation not found")],
    max_axiom_clauses = 60,
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 04 16:42:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Jun 04 16:55:25 2010 +0200
@@ -409,9 +409,10 @@
           (substs' |> map (fn (x, y) =>
             Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
             Syntax.string_of_term ctxt (term_of y)))));
-  in  cterm_instantiate substs' i_th
-      handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
-  end;
+  in  cterm_instantiate substs' i_th end
+  handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
+       | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
+                             "\n(Perhaps you want to try \"metisFT\".)")
 
 (* INFERENCE RULE: RESOLVE *)
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 04 16:42:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Fri Jun 04 16:55:25 2010 +0200
@@ -457,7 +457,7 @@
 
 end;
 
-val suppress_endtheory = Unsynchronized.ref false;
+val suppress_endtheory = Unsynchronized.ref false
 
 fun clause_cache_endtheory thy =
   if ! suppress_endtheory then NONE
@@ -478,21 +478,18 @@
 (*** Converting a subgoal into negated conjecture clauses. ***)
 
 fun neg_skolemize_tac ctxt =
-  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
-
-fun neg_skolemize_tac ctxt =
-  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
+  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
 
 val neg_clausify =
   single #> Meson.make_clauses_unsorted #> map combinators #> Meson.finish_cnf
 
 fun neg_conjecture_clauses ctxt st0 n =
   let
-    val st = Seq.hd (neg_skolemize_tac ctxt n st0)
-    val ({params, prems, ...}, _) = Subgoal.focus (Variable.set_body false ctxt) n st
-  in
-    (map neg_clausify prems, map (Term.dest_Free o Thm.term_of o #2) params)
-  end
+    (* "Option" is thrown if the assumptions contain schematic variables. *)
+    val st = Seq.hd (neg_skolemize_tac ctxt n st0) handle Option.Option => st0
+    val ({params, prems, ...}, _) =
+      Subgoal.focus (Variable.set_body false ctxt) n st
+  in (map neg_clausify prems, map (dest_Free o term_of o #2) params) end
 
 (*Conversion of a subgoal to conjecture clauses. Each clause has
   leading !!-bound universal variables, to express generality. *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 04 16:42:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 04 16:55:25 2010 +0200
@@ -28,8 +28,11 @@
 
 val neg_clausify_setup =
   Method.setup @{binding neg_clausify}
-               (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
-               "conversion of goal to negated conjecture clauses"
+               (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac)
+                o tap (fn _ => legacy_feature "Old 'neg_clausify' method -- \
+                                   \rerun Sledgehammer to obtain a direct \
+                                   \proof"))
+               "conversion of goal to negated conjecture clauses (legacy)"
 
 (** Attribute for converting a theorem into clauses **)
 
@@ -41,7 +44,9 @@
                   end))
 
 val clausify_setup =
-  Attrib.setup @{binding clausify} parse_clausify_attribute
+  Attrib.setup @{binding clausify}
+               (parse_clausify_attribute
+                o tap (fn _ => legacy_feature "Old 'clausify' attribute"))
                "conversion of theorem to clauses"
 
 (** Sledgehammer commands **)
@@ -226,7 +231,7 @@
       let
         val birth_time = Time.now ()
         val death_time = Time.+ (birth_time, timeout)
-        val _ = kill_atps ()  (* race w.r.t. other Sledgehammer invocations *)
+        val _ = kill_atps ()
         val _ = priority "Sledgehammering..."
         val _ = app (start_prover_thread params birth_time death_time i n
                                          relevance_override minimize_command
@@ -249,8 +254,10 @@
   in
     case subgoal_count state of
       0 => priority "No subgoal!"
-    | n => priority (#2 (minimize_theorems (get_params thy override_params) i n
-                                           state name_thms_pairs))
+    | n =>
+      (kill_atps ();
+       priority (#2 (minimize_theorems (get_params thy override_params) i n
+                                       state name_thms_pairs)))
   end
 
 val sledgehammerN = "sledgehammer"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jun 04 16:42:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Jun 04 16:55:25 2010 +0200
@@ -487,8 +487,8 @@
 fun decode_lines ctxt full_types tfrees lines =
   fst (fold_map (decode_line full_types tfrees) lines ctxt)
 
-fun aint_inference _ (Definition _) = true
-  | aint_inference t (Inference (_, t', _)) = not (t aconv t')
+fun aint_actual_inference _ (Definition _) = true
+  | aint_actual_inference t (Inference (_, t', _)) = not (t aconv t')
 
 (* No "real" literals means only type information (tfree_tcs, clsrel, or
    clsarity). *)
@@ -510,7 +510,7 @@
       if is_only_type_information t then
         map (replace_deps_in_line (num, [])) lines
       (* Is there a repetition? If so, replace later line by earlier one. *)
-      else case take_prefix (aint_inference t) lines of
+      else case take_prefix (aint_actual_inference t) lines of
         (_, []) => lines (*no repetition of proof line*)
       | (pre, Inference (num', _, _) :: post) =>
         pre @ map (replace_deps_in_line (num', [num])) post
@@ -523,7 +523,7 @@
     if is_only_type_information t then
       Inference (num, t, deps) :: lines
     (* Is there a repetition? If so, replace later line by earlier one. *)
-    else case take_prefix (aint_inference t) lines of
+    else case take_prefix (aint_actual_inference t) lines of
       (* FIXME: Doesn't this code risk conflating proofs involving different
          types?? *)
        (_, []) => Inference (num, t, deps) :: lines
@@ -539,8 +539,8 @@
 and delete_dep num lines =
   fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
 
-(* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly,
-   removing the offending lines often does the trick. *)
+(* ATPs sometimes reuse free variable names in the strangest ways. Removing
+   offending lines often does the trick. *)
 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   | is_bad_free _ _ = false
 
@@ -549,8 +549,8 @@
                                         $ t1 $ t2)) = (t1 aconv t2)
   | is_trivial_formula t = false
 
-fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
-    (j, line :: lines)
+fun add_desired_line _ _ _ _ _ (line as Definition (num, _, _)) (j, lines) =
+    (j, line :: map (replace_deps_in_line (num, [])) lines)
   | add_desired_line ctxt isar_shrink_factor conjecture_shape thm_names frees
                      (Inference (num, t, deps)) (j, lines) =
     (j + 1,
@@ -639,6 +639,9 @@
 fun smart_case_split [] facts = ByMetis facts
   | smart_case_split proofs facts = CaseSplit (proofs, facts)
 
+val indent_size = 2
+val no_label = ("", ~1)
+
 val raw_prefix = "X"
 val assum_prefix = "A"
 val fact_prefix = "F"
@@ -677,16 +680,12 @@
     map2 (step_for_line thm_names) (length lines downto 1) lines
   end
 
-val indent_size = 2
-val no_label = ("", ~1)
-
-fun no_show qs = not (member (op =) qs Show)
-
 (* When redirecting proofs, we keep information about the labels seen so far in
    the "backpatches" data structure. The first component indicates which facts
    should be associated with forthcoming proof steps. The second component is a
-   pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and
-   "drop_ls" are those that should be dropped in a case split. *)
+   pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should
+   become assumptions and "drop_ls" are the labels that should be dropped in a
+   case split. *)
 type backpatches = (label * facts) list * (label list * label list)
 
 fun used_labels_of_step (Have (_, _, _, by)) =
@@ -731,8 +730,15 @@
 
 fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
   let
+    (* The first pass outputs those steps that are independent of the negated
+       conjecture. The second pass flips the proof by contradiction to obtain a
+       direct proof, introducing case splits when an inference depends on
+       several facts that depend on the negated conjecture. *)
+    fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
     val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
-    fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
+    val canonicalize_labels =
+      map (fn l => if member (op =) concl_ls l then hd concl_ls else l)
+      #> distinct (op =)
     fun first_pass ([], contra) = ([], contra)
       | first_pass ((step as Fix _) :: proof, contra) =
         first_pass (proof, contra) |>> cons step
@@ -740,15 +746,19 @@
         first_pass (proof, contra) |>> cons step
       | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
         if member (op =) concl_ls l then
-          first_pass (proof, contra ||> cons step)
+          first_pass (proof, contra ||> l = hd concl_ls ? cons step)
         else
           first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
-      | first_pass ((step as Have (qs, l, t, ByMetis (ls, ss))) :: proof,
-                    contra) =
-        if exists (member (op =) (fst contra)) ls then
-          first_pass (proof, contra |>> cons l ||> cons step)
-        else
-          first_pass (proof, contra) |>> cons step
+      | first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) =
+        let
+          val ls = canonicalize_labels ls
+          val step = Have (qs, l, t, ByMetis (ls, ss))
+        in
+          if exists (member (op =) (fst contra)) ls then
+            first_pass (proof, contra |>> cons l ||> cons step)
+          else
+            first_pass (proof, contra) |>> cons step
+        end
       | first_pass _ = raise Fail "malformed proof"
     val (proof_top, (contra_ls, contra_proof)) =
       first_pass (proof, (concl_ls, []))
@@ -756,23 +766,23 @@
     fun backpatch_labels patches ls =
       fold merge_fact_sets (map (backpatch_label patches) ls) ([], [])
     fun second_pass end_qs ([], assums, patches) =
-        ([Have (end_qs, no_label,
-                if length assums < length concl_ls then
-                  clause_for_literals thy (map (negate_term thy o fst) assums)
-                else
-                  concl_t,
+        ([Have (end_qs, no_label, concl_t,
                 ByMetis (backpatch_labels patches (map snd assums)))], patches)
       | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
         second_pass end_qs (proof, (t, l) :: assums, patches)
       | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
                             patches) =
         if member (op =) (snd (snd patches)) l andalso
+           not (member (op =) (fst (snd patches)) l) andalso
            not (AList.defined (op =) (fst patches) l) then
           second_pass end_qs (proof, assums, patches ||> apsnd (append ls))
         else
           (case List.partition (member (op =) contra_ls) ls of
              ([contra_l], co_ls) =>
-             if no_show qs then
+             if member (op =) qs Show then
+               second_pass end_qs (proof, assums,
+                                   patches |>> cons (contra_l, (co_ls, ss)))
+             else
                second_pass end_qs
                            (proof, assums,
                             patches |>> cons (contra_l, (l :: co_ls, ss)))
@@ -781,9 +791,6 @@
                          else
                            Have (qs, l, negate_term thy t,
                                  ByMetis (backpatch_label patches l)))
-             else
-               second_pass end_qs (proof, assums,
-                                   patches |>> cons (contra_l, (co_ls, ss)))
            | (contra_ls as _ :: _, co_ls) =>
              let
                val proofs =
@@ -801,7 +808,11 @@
                                           ||> apsnd (union (op =) drop_ls))
                              |> fst |> SOME
                            end) contra_ls
-               val facts = (co_ls, [])
+               val (assumes, facts) =
+                 if member (op =) (fst (snd patches)) l then
+                   ([Assume (l, negate_term thy t)], (l :: co_ls, ss))
+                 else
+                   ([], (co_ls, ss))
              in
                (case join_proofs proofs of
                   SOME (l, t, proofs, proof_tail) =>
@@ -812,6 +823,7 @@
                   [Have (case_split_qualifiers proofs @ end_qs, no_label,
                          concl_t, smart_case_split proofs facts)],
                 patches)
+               |>> append assumes
              end
            | _ => raise Fail "malformed proof")
        | second_pass _ _ = raise Fail "malformed proof"
@@ -914,9 +926,11 @@
 
 fun string_for_proof ctxt i n =
   let
-    fun fix_print_mode f =
-      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
-                      (print_mode_value ())) f
+    fun fix_print_mode f x =
+      setmp_CRITICAL show_no_free_types true
+          (setmp_CRITICAL show_types true
+               (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+                                         (print_mode_value ())) f)) x
     fun do_indent ind = replicate_string (ind * indent_size) " "
     fun do_free (s, T) =
       maybe_quote s ^ " :: " ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jun 04 16:42:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jun 04 16:55:25 2010 +0200
@@ -91,7 +91,8 @@
     end
 
 val subscript = implode o map (prefix "\<^isub>") o explode
-val nat_subscript = subscript o string_of_int
+fun nat_subscript n =
+  n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
 
 fun plain_string_from_xml_tree t =
   Buffer.empty |> XML.add_content t |> Buffer.content
--- a/src/Pure/old_goals.ML	Fri Jun 04 16:42:26 2010 +0200
+++ b/src/Pure/old_goals.ML	Fri Jun 04 16:55:25 2010 +0200
@@ -189,28 +189,28 @@
 
 local
 
-fun print_vars_terms thy (n,thm) =
+fun print_vars_terms n thm =
   let
-    fun typed ty = " has type: " ^ Syntax.string_of_typ_global thy ty;
-    fun find_vars thy (Const (c, ty)) =
+    val thy = theory_of_thm thm
+    fun typed s ty =
+      "  " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty;
+    fun find_vars (Const (c, ty)) =
           if null (Term.add_tvarsT ty []) then I
-          else insert (op =) (c ^ typed ty)
-      | find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty)
-      | find_vars _ (Free _) = I
-      | find_vars _ (Bound _) = I
-      | find_vars thy (Abs (_, _, t)) = find_vars thy t
-      | find_vars thy (t1 $ t2) =
-          find_vars thy t1 #> find_vars thy t1;
+          else insert (op =) (typed c ty)
+      | find_vars (Var (xi, ty)) =
+          insert (op =) (typed (Term.string_of_vname xi) ty)
+      | find_vars (Free _) = I
+      | find_vars (Bound _) = I
+      | find_vars (Abs (_, _, t)) = find_vars t
+      | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2;
     val prem = Logic.nth_prem (n, Thm.prop_of thm)
-    val tms = find_vars thy prem []
-  in
-    (warning "Found schematic vars in assumptions:"; warning (cat_lines tms))
-  end;
+    val tms = find_vars prem []
+  in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end;
 
 in
 
 fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm
-  handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty)
+  handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty)
 
 end;