# HG changeset patch
# User blanchet
# Date 1272496266 -7200
# Node ID 2673979cb54da14aaf0d9298be8b357042f1fbd9
# Parent  95bdfa572ceebae0aea4966451e84cc531d19d8f
more neg_clausify proofs that get replaced by direct proofs

diff -r 95bdfa572cee -r 2673979cb54d src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Wed Apr 28 22:36:39 2010 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy	Thu Apr 29 01:11:06 2010 +0200
@@ -514,67 +514,44 @@
      "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
 apply (simp add: fix_def)
 apply (rule conjI)
-proof (neg_clausify)
-assume 0: "H =
-Collect
- (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
-assume 1: "lub (Collect
-      (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
-        (COMBC op \<in> A)))
- cl
-\<notin> A"
-have 2: "lub H cl \<notin> A"
-  by (metis 1 0)
-have 3: "(lub H cl, f (lub H cl)) \<in> r"
-  by (metis lubH_le_flubH 0)
-have 4: "(f (lub H cl), lub H cl) \<in> r"
-  by (metis flubH_le_lubH 0)
-have 5: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
-  by (metis antisymE 4)
-have 6: "lub H cl = f (lub H cl)"
-  by (metis 5 3)
-have 7: "(lub H cl, lub H cl) \<in> r"
-  by (metis 6 4)
-have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl_on X1 r"
-  by (metis 7 refl_onD2)
-have 9: "\<not> refl_on A r"
-  by (metis 8 2)
-show "False"
-  by (metis CO_refl_on 9);
-next --{*apparently the way to insert a second structured proof*}
-  show "H = {x. (x, f x) \<in> r \<and> x \<in> A} \<Longrightarrow>
-  f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) = lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
-  proof (neg_clausify)
-  assume 0: "H =
-  Collect
-   (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
-  assume 1: "f (lub (Collect
-           (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
-             (COMBC op \<in> A)))
-      cl) \<noteq>
-  lub (Collect
-        (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
-          (COMBC op \<in> A)))
-   cl"
-  have 2: "f (lub H cl) \<noteq>
-  lub (Collect
-        (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
-          (COMBC op \<in> A)))
-   cl"
-    by (metis 1 0)
-  have 3: "f (lub H cl) \<noteq> lub H cl"
-    by (metis 2 0)
-  have 4: "(lub H cl, f (lub H cl)) \<in> r"
-    by (metis lubH_le_flubH 0)
-  have 5: "(f (lub H cl), lub H cl) \<in> r"
-    by (metis flubH_le_lubH 0)
-  have 6: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
-    by (metis antisymE 5)
-  have 7: "lub H cl = f (lub H cl)"
-    by (metis 6 4)
-  show "False"
-    by (metis 3 7)
-  qed
+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)
+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)
+  have F2: "\<forall>w u. (\<lambda>R. u R \<and> w R) = u \<inter> w"
+    by (metis Collect_conj_eq Collect_def)
+  have F3: "\<forall>x v. (\<lambda>R. v R \<in> x) = v -` x" by (metis vimage_def Collect_def)
+  hence F4: "A \<inter> (\<lambda>R. (R, f R)) -` r = H" using A1 by auto
+  hence F5: "(f (lub H cl), lub H cl) \<in> r"
+    by (metis F1 F3 F2 Int_commute flubH_le_lubH Collect_def)
+  have F6: "(lub H cl, f (lub H cl)) \<in> r"
+    by (metis F1 F3 F2 F4 Int_commute lubH_le_flubH Collect_def)
+  have "(lub H cl, f (lub H cl)) \<in> r \<longrightarrow> f (lub H cl) = lub H cl"
+    using F5 by (metis antisymE)
+  hence "f (lub H cl) = lub H cl" using F6 by metis
+  thus "H = {x. (x, f x) \<in> r \<and> x \<in> A}
+        \<Longrightarrow> f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) =
+           lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
+    by (metis F4 F2 F3 F1 Collect_def Int_commute)
 qed
 
 lemma (in CLF) (*lubH_is_fixp:*)
@@ -744,18 +721,13 @@
      "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
       ==> (| pset = interval r a b, order = induced (interval r a b) r |)
           \<in> PartialOrder"
-proof (neg_clausify)
-assume 0: "a \<in> A"
-assume 1: "b \<in> A"
-assume 2: "\<lparr>pset = interval r a b, order = induced (interval r a b) r\<rparr> \<notin> PartialOrder"
-have 3: "\<not> interval r a b \<subseteq> A"
-  by (metis 2 po_subset_po)
-have 4: "b \<notin> A \<or> a \<notin> A"
-  by (metis 3 interval_subset)
-have 5: "a \<notin> A"
-  by (metis 4 1)
-show "False"
-  by (metis 5 0)
+proof -
+  assume A1: "a \<in> A"
+  assume "b \<in> A"
+  hence "\<forall>u. u \<in> A \<longrightarrow> interval r u b \<subseteq> A" by (metis interval_subset)
+  hence "interval r a b \<subseteq> A" using A1 by metis
+  hence "interval r a b \<subseteq> A" by metis
+  thus ?thesis by (metis po_subset_po)
 qed
 
 lemma (in CLF) intv_CL_lub:
@@ -1096,9 +1068,9 @@
 apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro,
   OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl)
 done
-  declare (in CLF) fixf_po[rule del] P_def [simp del] A_def [simp del] r_def [simp del]
+
+declare (in CLF) fixf_po [rule del] P_def [simp del] A_def [simp del] r_def [simp del]
          Tarski.tarski_full_lemma [rule del] cl_po [rule del] cl_co [rule del]
          CompleteLatticeI_simp [rule del]
 
-
 end