# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID 0b3c3cf282181e48c45aaf7fd5ddcef1fd83fe9c
# Parent  8ea9c6fa8b53d8aee8717166f23cb87cf8aa7a10
prove one more lemma using Sledgehammer, with some guidance, and replace clumsy old proof that relied on old extensionality behavior

diff -r 8ea9c6fa8b53 -r 0b3c3cf28218 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy	Thu May 12 15:29:19 2011 +0200
@@ -106,7 +106,6 @@
   assumes f_cl:  "(cl,f) : CLF_set" (*was the equivalent "f : CLF``{cl}"*)
   defines P_def: "P == fix f A"
 
-
 locale Tarski = CLF +
   fixes Y     :: "'a set"
     and intY1 :: "'a set"
@@ -409,18 +408,20 @@
 
 declare (in CLF) f_cl [simp]
 
-(*never proved, 2007-01-22: Tarski__CLF_unnamed_lemma
-  NOT PROVABLE because of the conjunction used in the definition: we don't
-  allow reasoning with rules like conjE, which is essential here.*)
 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_unnamed_lemma" ]]
 lemma (in CLF) [simp]:
-    "f: pset cl -> pset cl & monotone f (pset cl) (order cl)" 
-apply (insert f_cl)
-apply (unfold CLF_set_def)
-apply (erule SigmaE2) 
-apply (erule CollectE) 
-apply assumption
-done
+    "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
+proof -
+  have "\<forall>u v. (v, u) \<in> CLF_set \<longrightarrow> u \<in> {R \<in> pset v \<rightarrow> pset v. monotone R (pset v) (order v)}"
+    unfolding CLF_set_def using SigmaE2 by blast
+  hence F1: "\<forall>u v. (v, u) \<in> CLF_set \<longrightarrow> u \<in> pset v \<rightarrow> pset v \<and> monotone u (pset v) (order v)"
+    using CollectE by blast
+  hence "Tarski.monotone f (pset cl) (order cl)" by (metis f_cl)
+  hence "(cl, f) \<in> CLF_set \<and> Tarski.monotone f (pset cl) (order cl)"
+    by (metis f_cl)
+  thus "f \<in> pset cl \<rightarrow> pset cl \<and> Tarski.monotone f (pset cl) (order cl)"
+    using F1 by metis
+qed
 
 lemma (in CLF) f_in_funcset: "f \<in> A -> A"
 by (simp add: A_def)
@@ -432,10 +433,10 @@
 declare [[ sledgehammer_problem_prefix = "Tarski__CLF_CLF_dual" ]]
 declare (in CLF) CLF_set_def [simp] CL_dualCL [simp] monotone_dual [simp] dualA_iff [simp]
 
-lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set" 
+lemma (in CLF) CLF_dual: "(dual cl, f) \<in> CLF_set"
 apply (simp del: dualA_iff)
 apply (simp)
-done
+done 
 
 declare (in CLF) CLF_set_def[simp del] CL_dualCL[simp del] monotone_dual[simp del]
           dualA_iff[simp del]
@@ -518,24 +519,12 @@
 apply (rule conjI)
 proof -
   assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}"
-  have F1: "\<forall>x\<^isub>2. (\<lambda>R. R \<in> x\<^isub>2) = x\<^isub>2" by (metis Collect_def Collect_mem_eq)
-  have F2: "\<forall>x\<^isub>1 x\<^isub>2. (\<lambda>R. x\<^isub>2 (x\<^isub>1 R)) = x\<^isub>1 -` x\<^isub>2"
-    by (metis Collect_def vimage_Collect_eq)
-  have F3: "\<forall>x\<^isub>2 x\<^isub>1. (\<lambda>R. x\<^isub>1 R \<in> x\<^isub>2) = x\<^isub>1 -` x\<^isub>2"
-    by (metis Collect_def vimage_def)
-  have F4: "\<forall>x\<^isub>3 x\<^isub>1. (\<lambda>R. x\<^isub>1 R \<and> x\<^isub>3 R) = x\<^isub>1 \<inter> x\<^isub>3"
-    by (metis Collect_def Collect_conj_eq)
-  have F5: "(\<lambda>R. (R, f R) \<in> r \<and> R \<in> A) = H" using A1 by (metis Collect_def)
-  have F6: "\<forall>x\<^isub>1\<subseteq>A. glb x\<^isub>1 (dual cl) \<in> A" by (metis lub_dual_glb lub_in_lattice)
-  have F7: "\<forall>x\<^isub>2 x\<^isub>1. (\<lambda>R. x\<^isub>1 R \<in> x\<^isub>2) = (\<lambda>R. x\<^isub>2 (x\<^isub>1 R))" by (metis F2 F3)
-  have "(\<lambda>R. (R, f R) \<in> r \<and> A R) = H" by (metis F1 F5)
-  hence "A \<inter> (\<lambda>R. r (R, f R)) = H" by (metis F4 F7 Int_commute)
-  hence "H \<subseteq> A" by (metis Int_lower1)
-  hence "H \<subseteq> A" by metis
-  hence "glb H (dual cl) \<in> A" using F6 by metis
-  hence "glb (\<lambda>R. (R, f R) \<in> r \<and> R \<in> A) (dual cl) \<in> A" using F5 by metis
-  hence "lub (\<lambda>R. (R, f R) \<in> r \<and> R \<in> A) cl \<in> A" by (metis lub_dual_glb)
-  thus "lub {x. (x, f x) \<in> r \<and> x \<in> A} cl \<in> A" by (metis Collect_def)
+  have F1: "\<forall>u v. v \<inter> u \<subseteq> u" by (metis Int_commute Int_lower1)
+  have "{R. (R, f R) \<in> r} \<inter> {R. R \<in> A} = H" using A1 by (metis Collect_conj_eq)
+  hence "H \<subseteq> {R. R \<in> A}" using F1 by metis
+  hence "H \<subseteq> A" by (metis Collect_mem_eq)
+  hence "lub H cl \<in> A" by (metis lub_in_lattice)
+  thus "lub {x. (x, f x) \<in> r \<and> x \<in> A} cl \<in> A" using A1 by metis
 next
   assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}"
   have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)