# HG changeset patch
# User wenzelm
# Date 1473188958 -7200
# Node ID 67b091896158d297c97fb05996e7e273730f48a3
# Parent  56670ab6f55e3f23171cbf8d241f50cf6064d86d
clarified proof: save 1-2s CPU time;

diff -r 56670ab6f55e -r 67b091896158 src/HOL/Complete_Partial_Order.thy
--- a/src/HOL/Complete_Partial_Order.thy	Tue Sep 06 15:02:22 2016 +0200
+++ b/src/HOL/Complete_Partial_Order.thy	Tue Sep 06 21:09:18 2016 +0200
@@ -80,7 +80,7 @@
   by (rule chainI) simp
 
 lemma ccpo_Sup_singleton [simp]: "\<Squnion>{x} = x"
-  by (rule antisym)(auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
+  by (rule antisym) (auto intro: ccpo_Sup_least ccpo_Sup_upper simp add: chain_singleton)
 
 
 subsection \<open>Transfinite iteration of a function\<close>
@@ -282,26 +282,6 @@
 context ccpo
 begin
 
-lemma admissible_disj_lemma:
-  assumes A: "chain (op \<le>)A"
-  assumes P: "\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y"
-  shows "Sup A = Sup {x \<in> A. P x}"
-proof (rule antisym)
-  have *: "chain (op \<le>) {x \<in> A. P x}"
-    by (rule chain_compr [OF A])
-  show "Sup A \<le> Sup {x \<in> A. P x}"
-    apply (rule ccpo_Sup_least [OF A])
-    apply (drule P [rule_format], clarify)
-    apply (erule order_trans)
-    apply (simp add: ccpo_Sup_upper [OF *])
-    done
-  show "Sup {x \<in> A. P x} \<le> Sup A"
-    apply (rule ccpo_Sup_least [OF *])
-    apply clarify
-    apply (simp add: ccpo_Sup_upper [OF A])
-    done
-qed
-
 lemma admissible_disj:
   fixes P Q :: "'a \<Rightarrow> bool"
   assumes P: "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x)"
@@ -309,23 +289,73 @@
   shows "ccpo.admissible Sup (op \<le>) (\<lambda>x. P x \<or> Q x)"
 proof (rule ccpo.admissibleI)
   fix A :: "'a set"
-  assume A: "chain (op \<le>) A"
-  assume "A \<noteq> {}" and "\<forall>x\<in>A. P x \<or> Q x"
-  then have "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
-    using chainD[OF A] by blast  (* slow *)
-  then have "(\<exists>x. x \<in> A \<and> P x) \<and> Sup A = Sup {x \<in> A. P x} \<or> (\<exists>x. x \<in> A \<and> Q x) \<and> Sup A = Sup {x \<in> A. Q x}"
-    using admissible_disj_lemma [OF A] by blast
+  assume chain: "chain (op \<le>) A"
+  assume A: "A \<noteq> {}" and P_Q: "\<forall>x\<in>A. P x \<or> Q x"
+  have "(\<exists>x\<in>A. P x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y) \<or> (\<exists>x\<in>A. Q x) \<and> (\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> Q y)"
+    (is "?P \<or> ?Q" is "?P1 \<and> ?P2 \<or> _")
+  proof (rule disjCI)
+    assume "\<not> ?Q"
+    then consider "\<forall>x\<in>A. \<not> Q x" | a where "a \<in> A" "\<forall>y\<in>A. a \<le> y \<longrightarrow> \<not> Q y"
+      by blast
+    then show ?P
+    proof cases
+      case 1
+      with P_Q have "\<forall>x\<in>A. P x" by blast
+      with A show ?P by blast
+    next
+      case 2
+      note a = \<open>a \<in> A\<close>
+      show ?P
+      proof
+        from P_Q 2 have *: "\<forall>y\<in>A. a \<le> y \<longrightarrow> P y" by blast
+        with a have "P a" by blast
+        with a show ?P1 by blast
+        show ?P2
+        proof
+          fix x
+          assume x: "x \<in> A"
+          with chain a show "\<exists>y\<in>A. x \<le> y \<and> P y"
+          proof (rule chainE)
+            assume le: "a \<le> x"
+            with * a x have "P x" by blast
+            with x le show ?thesis by blast
+          next
+            assume "a \<ge> x"
+            with a \<open>P a\<close> show ?thesis by blast
+          qed
+        qed
+      qed
+    qed
+  qed
+  moreover
+  have "Sup A = Sup {x \<in> A. P x}" if "\<forall>x\<in>A. \<exists>y\<in>A. x \<le> y \<and> P y" for P
+  proof (rule antisym)
+    have chain_P: "chain (op \<le>) {x \<in> A. P x}"
+      by (rule chain_compr [OF chain])
+    show "Sup A \<le> Sup {x \<in> A. P x}"
+      apply (rule ccpo_Sup_least [OF chain])
+      apply (drule that [rule_format])
+      apply clarify
+      apply (erule order_trans)
+      apply (simp add: ccpo_Sup_upper [OF chain_P])
+      done
+    show "Sup {x \<in> A. P x} \<le> Sup A"
+      apply (rule ccpo_Sup_least [OF chain_P])
+      apply clarify
+      apply (simp add: ccpo_Sup_upper [OF chain])
+      done
+  qed
+  ultimately
+  consider "\<exists>x. x \<in> A \<and> P x" "Sup A = Sup {x \<in> A. P x}"
+    | "\<exists>x. x \<in> A \<and> Q x" "Sup A = Sup {x \<in> A. Q x}"
+    by blast
   then show "P (Sup A) \<or> Q (Sup A)"
-    apply (rule disjE)
+    apply cases
      apply simp_all
      apply (rule disjI1)
-     apply (rule ccpo.admissibleD [OF P chain_compr [OF A]])
-      apply simp
-     apply simp
+     apply (rule ccpo.admissibleD [OF P chain_compr [OF chain]]; simp)
     apply (rule disjI2)
-    apply (rule ccpo.admissibleD [OF Q chain_compr [OF A]])
-     apply simp
-    apply simp
+    apply (rule ccpo.admissibleD [OF Q chain_compr [OF chain]]; simp)
     done
 qed