# HG changeset patch
# User huffman
# Date 1116452992 -7200
# Node ID 693dd363e0bf080e0556673cc3af43c65dce055c
# Parent  42f3f299ee687f1f612dace4d8f60d007d89f0a5
shortened proof of adm_disj

diff -r 42f3f299ee68 -r 693dd363e0bf src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Wed May 18 23:29:36 2005 +0200
+++ b/src/HOLCF/Fix.ML	Wed May 18 23:49:52 2005 +0200
@@ -64,11 +64,6 @@
 val adm_disj_lemma5 = thm "adm_disj_lemma5";
 val adm_disj_lemma6 = thm "adm_disj_lemma6";
 val adm_disj_lemma7 = thm "adm_disj_lemma7";
-val adm_disj_lemma8 = thm "adm_disj_lemma8";
-val adm_disj_lemma9 = thm "adm_disj_lemma9";
-val adm_disj_lemma10 = thm "adm_disj_lemma10";
-val adm_disj_lemma12 = thm "adm_disj_lemma12";
-val adm_lemma11 = thm "adm_lemma11";
 val adm_disj = thm "adm_disj";
 val adm_imp = thm "adm_imp";
 val adm_iff = thm "adm_iff";
diff -r 42f3f299ee68 -r 693dd363e0bf src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Wed May 18 23:29:36 2005 +0200
+++ b/src/HOLCF/Fix.thy	Wed May 18 23:49:52 2005 +0200
@@ -421,173 +421,106 @@
 lemma adm_eq: "[|cont u ; cont v|]==> adm(%x. u x = v x)"
 by (simp add: po_eq_conv)
 
-text {* admissibility for disjunction is hard to prove. It takes 10 Lemmas *}
-
-lemma adm_disj_lemma1: "!n. P(Y n)|Q(Y n) ==> (? i.!j. R i j --> Q(Y(j))) | (!i.? j. R i j & P(Y(j)))"
-by fast
-
-lemma adm_disj_lemma2: "[| adm(Q); ? X. chain(X) & (!n. Q(X(n))) & 
-      lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
-by (force elim: admD)
+text {* admissibility for disjunction is hard to prove. It takes 7 Lemmas *}
 
-lemma adm_disj_lemma3: "chain Y ==> chain (%m. if m < Suc i then Y (Suc i) else Y m)"
-apply (unfold chain_def)
-apply (simp)
-apply safe
-apply (subgoal_tac "ia = i")
-apply (simp_all)
-done
-
-lemma adm_disj_lemma4: "!j. i < j --> Q(Y(j))  ==> !n. Q( if n < Suc i then Y(Suc i) else Y n)"
-by (simp)
-
-lemma adm_disj_lemma5: 
-  "!!Y::nat=>'a::cpo. [| chain(Y); ! j. i < j --> Q(Y(j)) |] ==> 
-          lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
-apply (safe intro!: lub_equal2 adm_disj_lemma3)
-prefer 2 apply (assumption)
-apply (rule_tac x = "i" in exI)
-apply (simp)
+lemma adm_disj_lemma1:
+  "\<forall>n::nat. P n \<or> Q n \<Longrightarrow> (\<forall>i. \<exists>j\<ge>i. P j) \<or> (\<forall>i. \<exists>j\<ge>i. Q j)"
+apply (erule contrapos_pp)
+apply clarsimp
+apply (rule exI)
+apply (rule conjI)
+apply (drule spec, erule mp)
+apply (rule le_maxI1)
+apply (drule spec, erule mp)
+apply (rule le_maxI2)
 done
 
-lemma adm_disj_lemma6: 
-  "[| chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==> 
-            ? X. chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
-apply (erule exE)
-apply (rule_tac x = "%m. if m<Suc (i) then Y (Suc (i)) else Y m" in exI)
+lemma adm_disj_lemma2: "[| adm P; \<exists>X. chain X & (!n. P(X n)) & 
+      lub(range Y)=lub(range X)|] ==> P(lub(range Y))"
+by (force elim: admD)
+
+lemma adm_disj_lemma3: 
+  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P (Y j) |] ==> 
+            chain(%m. Y (LEAST j. m\<le>j \<and> P(Y j)))"
+apply (rule chainI)
+apply (erule chain_mono3)
+apply (rule Least_le)
 apply (rule conjI)
-apply (rule adm_disj_lemma3)
-apply assumption
-apply (rule conjI)
-apply (rule adm_disj_lemma4)
-apply assumption
-apply (rule adm_disj_lemma5)
-apply assumption
-apply assumption
+apply (rule Suc_leD)
+apply (erule allE)
+apply (erule exE)
+apply (erule LeastI [THEN conjunct1])
+apply (erule allE)
+apply (erule exE)
+apply (erule LeastI [THEN conjunct2])
 done
 
-lemma adm_disj_lemma7: 
-  "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j))  |] ==> 
-            chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
-apply (rule chainI)
-apply (rule chain_mono3)
-apply assumption
-apply (rule Least_le)
-apply (rule conjI)
-apply (rule Suc_lessD)
-apply (erule allE)
-apply (erule exE)
-apply (rule LeastI [THEN conjunct1])
-apply assumption
-apply (erule allE)
-apply (erule exE)
-apply (rule LeastI [THEN conjunct2])
-apply assumption
-done
-
-lemma adm_disj_lemma8: 
-  "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(LEAST j::nat. m<j & P(Y(j))))"
-apply (intro strip)
+lemma adm_disj_lemma4: 
+  "[| \<forall>i. \<exists>j\<ge>i. P (Y j) |] ==> ! m. P(Y(LEAST j::nat. m\<le>j & P(Y j)))"
+apply (rule allI)
 apply (erule allE)
 apply (erule exE)
 apply (erule LeastI [THEN conjunct2])
 done
 
-lemma adm_disj_lemma9: 
-  "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==> 
-            lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
-apply (rule antisym_less)
-apply (rule lub_mono)
-apply assumption
-apply (rule adm_disj_lemma7)
-apply assumption
-apply assumption
-apply (intro strip)
-apply (rule chain_mono)
-apply assumption
-apply (erule allE)
-apply (erule exE)
-apply (rule LeastI [THEN conjunct1])
-apply assumption
-apply (rule lub_mono3)
-apply (rule adm_disj_lemma7)
-apply assumption
-apply assumption
-apply assumption
-apply (intro strip)
-apply (rule exI)
-apply (rule chain_mono)
-apply assumption
-apply (rule lessI)
+lemma adm_disj_lemma5: 
+  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j) |] ==> 
+            lub(range(Y)) = (LUB m. Y(LEAST j. m\<le>j & P(Y j)))"
+ apply (rule antisym_less)
+  apply (rule lub_mono)
+    apply assumption
+   apply (erule adm_disj_lemma3)
+   apply assumption
+  apply (rule allI)
+  apply (erule chain_mono3)
+  apply (erule allE)
+  apply (erule exE)
+  apply (erule LeastI [THEN conjunct1])
+ apply (rule lub_mono3)
+   apply (erule adm_disj_lemma3)
+   apply assumption
+  apply assumption
+ apply (rule allI)
+ apply (rule exI)
+ apply (rule refl_less)
 done
 
-lemma adm_disj_lemma10: "[| chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==> 
-            ? X. chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
-apply (rule_tac x = "%m. Y (Least (%j. m<j & P (Y (j))))" in exI)
-apply (rule conjI)
-apply (rule adm_disj_lemma7)
-apply assumption
-apply assumption
-apply (rule conjI)
-apply (rule adm_disj_lemma8)
-apply assumption
-apply (rule adm_disj_lemma9)
-apply assumption
-apply assumption
+lemma adm_disj_lemma6:
+  "[| chain(Y::nat=>'a::cpo); \<forall>i. \<exists>j\<ge>i. P(Y j) |] ==> 
+            \<exists>X. chain X & (\<forall>n. P(X n)) & lub(range Y) = lub(range X)"
+apply (rule_tac x = "%m. Y (LEAST j. m\<le>j & P (Y j))" in exI)
+apply (fast intro!: adm_disj_lemma3 adm_disj_lemma4 adm_disj_lemma5)
 done
 
-lemma adm_disj_lemma12: "[| adm(P); chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
+lemma adm_disj_lemma7:
+"[| adm(P); chain(Y); \<forall>i. \<exists>j\<ge>i. P(Y j) |]==>P(lub(range(Y)))"
 apply (erule adm_disj_lemma2)
 apply (erule adm_disj_lemma6)
 apply assumption
 done
 
-lemma adm_lemma11: 
-"[| adm(P); chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
-apply (erule adm_disj_lemma2)
-apply (erule adm_disj_lemma10)
-apply assumption
-done
-
 lemma adm_disj: "[| adm P; adm Q |] ==> adm(%x. P x | Q x)"
 apply (rule admI)
-apply (rule adm_disj_lemma1 [THEN disjE])
+apply (erule adm_disj_lemma1 [THEN disjE])
+apply (rule disjI1)
+apply (erule adm_disj_lemma7)
+apply assumption
 apply assumption
 apply (rule disjI2)
-apply (erule adm_disj_lemma12)
-apply assumption
-apply assumption
-apply (rule disjI1)
-apply (erule adm_lemma11)
+apply (erule adm_disj_lemma7)
 apply assumption
 apply assumption
 done
 
 lemma adm_imp: "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)"
-apply (subgoal_tac " (%x. P x --> Q x) = (%x. ~P x | Q x) ")
-apply (erule ssubst)
-apply (erule adm_disj)
-apply assumption
-apply (simp)
-done
+by (subst imp_conv_disj, rule adm_disj)
 
 lemma adm_iff: "[| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |]  
             ==> adm (%x. P x = Q x)"
-apply (subgoal_tac " (%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))")
-apply (simp)
-apply (rule ext)
-apply fast
-done
-
+by (subst iff_conv_conj_imp, rule adm_conj)
 
 lemma adm_not_conj: "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"
-apply (subgoal_tac " (%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x) ")
-apply (rule_tac [2] ext)
-prefer 2 apply fast
-apply (erule ssubst)
-apply (erule adm_disj)
-apply assumption
-done
+by (subst de_Morgan_conj, rule adm_disj)
 
 lemmas adm_lemmas = adm_not_free adm_imp adm_disj adm_eq adm_not_UU
         adm_UU_not_less adm_all2 adm_not_less adm_not_conj adm_iff