# HG changeset patch
# User oheimb
# Date 842544729 -7200
# Node ID 0256c8b71ff1a44b68de174999748e15c5539a3d
# Parent  51935901c2396370ee37d652efef960df55d6588
added flat_eq,
renamed  adm_disj_lemma11 to adm_lemma11,
localized adm_disj_lemma1, ..., adm_disj_lemma10, adm_disj_lemma12,
modularized proof of admI

diff -r 51935901c239 -r 0256c8b71ff1 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Thu Sep 12 18:05:33 1996 +0200
+++ b/src/HOLCF/Fix.ML	Thu Sep 12 18:12:09 1996 +0200
@@ -537,7 +537,6 @@
         (etac spec 1)
         ]);
 
-
 qed_goalw "adm_chain_finite"  Fix.thy  [chain_finite_def]
         "chain_finite(x::'a) ==> adm(P::'a=>bool)"
  (fn prems =>
@@ -598,6 +597,51 @@
         (rtac unique_void2 1)
         ]);
 
+qed_goalw "flat_eq" Fix.thy [is_flat_def] 
+	"[| is_flat (x::'a); (a::'a) ~= UU |] ==> a << b = (a = b)" (fn prems=>[
+	(cut_facts_tac prems 1),
+	(fast_tac (HOL_cs addIs [refl_less]) 1)]);
+
+(* ------------------------------------------------------------------------ *)
+(* lemmata for improved admissibility introdution rule                      *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "infinite_chain_adm_lemma" Porder.thy 
+"[|is_chain Y; !i. P (Y i); \
+\  (!!Y. [| is_chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
+\ |] ==> P (lub (range Y))"
+ (fn prems => [
+	cut_facts_tac prems 1,
+	case_tac "finite_chain Y" 1,
+	 eresolve_tac prems 2, atac 2, atac 2,
+	rewtac finite_chain_def,
+	safe_tac HOL_cs,
+	etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]);
+
+qed_goal "increasing_chain_adm_lemma" Porder.thy 
+"[|is_chain Y; !i. P (Y i); \
+\  (!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
+\ ==> P (lub (range Y))) |] ==> P (lub (range Y))"
+ (fn prems => [
+	cut_facts_tac prems 1,
+	etac infinite_chain_adm_lemma 1, atac 1, etac thin_rl 1,
+	rewtac finite_chain_def,
+	safe_tac HOL_cs,
+	etac swap 1,
+	rewtac max_in_chain_def,
+	resolve_tac prems 1, atac 1, atac 1,
+	fast_tac (HOL_cs addDs [le_imp_less_or_eq] 
+			 addEs [chain_mono RS mp]) 1]);
+
+qed_goalw "admI" Fix.thy [adm_def]
+ "(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
+\ ==> P(lub (range Y))) ==> adm P" 
+ (fn prems => [
+	strip_tac 1,
+	etac increasing_chain_adm_lemma 1, atac 1,
+	eresolve_tac prems 1, atac 1, atac 1]);
+
+
 (* ------------------------------------------------------------------------ *)
 (* continuous isomorphisms are strict                                       *)
 (* a prove for embedding projection pairs is similar                        *)
@@ -900,18 +944,20 @@
 (* admissibility for disjunction is hard to prove. It takes 10 Lemmas       *)
 (* ------------------------------------------------------------------------ *)
 
-qed_goal "adm_disj_lemma1"  Pcpo.thy 
-"[| is_chain Y; !n.P (Y n) | Q(Y n)|]\
-\ ==> (? i.!j. i<j --> Q(Y(j))) | (!i.? j.i<j & P(Y(j)))"
+local
+
+  val adm_disj_lemma1 = prove_goal Pcpo.thy 
+  "[| is_chain Y; !n.P (Y n) | Q(Y n)|]\
+  \ ==> (? i.!j. i<j --> Q(Y(j))) | (!i.? j.i<j & P(Y(j)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (fast_tac HOL_cs 1)
         ]);
 
-qed_goal "adm_disj_lemma2"  Fix.thy  
-"[| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
-\   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
+  val adm_disj_lemma2 = prove_goal Fix.thy  
+  "[| adm(Q); ? X.is_chain(X) & (!n.Q(X(n))) &\
+  \   lub(range(Y))=lub(range(X))|] ==> Q(lub(range(Y)))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -926,9 +972,9 @@
         (atac 1)
         ]);
 
-qed_goal "adm_disj_lemma3"  Fix.thy
-"[| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
-\         is_chain(%m. if m < Suc i then Y(Suc i) else Y m)"
+  val adm_disj_lemma3 = prove_goal Fix.thy
+  "[| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
+  \         is_chain(%m. if m < Suc i then Y(Suc i) else Y m)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -957,28 +1003,31 @@
 	(asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1)
         ]);
 
-qed_goal "adm_disj_lemma4"  Fix.thy
-"[| ! j. i < j --> Q(Y(j)) |] ==>\
-\        ! n. Q( if n < Suc i then Y(Suc i) else Y n)"
+  val adm_disj_lemma4 = prove_goal Fix.thy
+  "[| ! j. i < j --> Q(Y(j)) |] ==>\
+  \        ! n. Q( if n < Suc i then Y(Suc i) else Y n)"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac allI 1),
         (res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1),
-        (res_inst_tac[("s","Y(Suc(i))"),("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1),
+        (res_inst_tac[("s","Y(Suc(i))"),
+		      ("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1),
         (Asm_simp_tac 1),
         (etac allE 1),
         (rtac mp 1),
         (atac 1),
         (Asm_simp_tac 1),
-        (res_inst_tac[("s","Y(n)"),("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
+        (res_inst_tac[("s","Y(n)"),
+		      ("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
         (Asm_simp_tac 1),
         (hyp_subst_tac 1),
         (dtac spec 1),
         (rtac mp 1),
         (atac 1),
         (Asm_simp_tac 1),
-        (res_inst_tac [("s","Y(n)"),("t","if n < Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
+        (res_inst_tac [("s","Y(n)"),
+		       ("t","if n < Suc(i) then Y(Suc(i)) else Y(n)")]ssubst 1),
         (res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
         (rtac iffI 1),
         (etac FalseE 2),
@@ -992,9 +1041,9 @@
         (etac Suc_lessD 1)
         ]);
 
-qed_goal "adm_disj_lemma5"  Fix.thy
-"[| is_chain(Y::nat=>'a); ! j. i < j --> Q(Y(j)) |] ==>\
-\         lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
+  val adm_disj_lemma5 = prove_goal Fix.thy
+  "[| is_chain(Y::nat=>'a); ! j. i < j --> Q(Y(j)) |] ==>\
+  \       lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -1016,9 +1065,9 @@
         (rtac refl 1)
         ]);
 
-qed_goal "adm_disj_lemma6"  Fix.thy
-"[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
-\         ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
+  val adm_disj_lemma6 = prove_goal Fix.thy
+  "[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
+  \         ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -1036,10 +1085,9 @@
         (atac 1)
         ]);
 
-
-qed_goal "adm_disj_lemma7"  Fix.thy 
-"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j))  |] ==>\
-\         is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
+  val adm_disj_lemma7 = prove_goal Fix.thy 
+  "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j))  |] ==>\
+  \         is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -1060,8 +1108,8 @@
         (atac 1)
         ]);
 
-qed_goal "adm_disj_lemma8"  Fix.thy 
-"[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(Least(%j. m<j & P(Y(j)))))"
+  val adm_disj_lemma8 = prove_goal Fix.thy 
+  "[| ! i. ? j. i < j & P(Y(j)) |] ==> ! m. P(Y(Least(%j. m<j & P(Y(j)))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -1071,9 +1119,9 @@
         (etac (LeastI RS conjunct2) 1)
         ]);
 
-qed_goal "adm_disj_lemma9"  Fix.thy
-"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
-\         lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
+  val adm_disj_lemma9 = prove_goal Fix.thy
+  "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
+  \         lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -1102,9 +1150,9 @@
         (rtac lessI 1)
         ]);
 
-qed_goal "adm_disj_lemma10"  Fix.thy
-"[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
-\         ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
+  val adm_disj_lemma10 = prove_goal Fix.thy
+  "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
+  \         ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
@@ -1121,8 +1169,19 @@
         (atac 1)
         ]);
 
+  val adm_disj_lemma12 = prove_goal Fix.thy
+  "[| adm(P); is_chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
+ (fn prems =>
+        [
+        (cut_facts_tac prems 1),
+        (etac adm_disj_lemma2 1),
+        (etac adm_disj_lemma6 1),
+        (atac 1)
+        ]);
 
-qed_goal "adm_disj_lemma11" Fix.thy
+in
+
+val adm_lemma11 = prove_goal Fix.thy
 "[| adm(P); is_chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
  (fn prems =>
         [
@@ -1132,17 +1191,7 @@
         (atac 1)
         ]);
 
-qed_goal "adm_disj_lemma12" Fix.thy
-"[| adm(P); is_chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
- (fn prems =>
-        [
-        (cut_facts_tac prems 1),
-        (etac adm_disj_lemma2 1),
-        (etac adm_disj_lemma6 1),
-        (atac 1)
-        ]);
-
-qed_goal "adm_disj"  Fix.thy  
+val adm_disj = prove_goal Fix.thy  
         "[| adm P; adm Q |] ==> adm(%x.P x | Q x)"
  (fn prems =>
         [
@@ -1157,11 +1206,15 @@
         (atac 1),
         (atac 1),
         (rtac disjI1 1),
-        (etac adm_disj_lemma11 1),
+        (etac adm_lemma11 1),
         (atac 1),
         (atac 1)
         ]);
 
+end;
+
+bind_thm("adm_lemma11",adm_lemma11);
+bind_thm("adm_disj",adm_disj);
 
 qed_goal "adm_imp"  Fix.thy  
         "[| adm(%x.~(P x)); adm Q |] ==> adm(%x.P x --> Q x)"
@@ -1175,7 +1228,6 @@
         (atac 1)
         ]);
 
-
 qed_goal "adm_not_conj"  Fix.thy  
 "[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"(fn prems=>[
 	cut_facts_tac prems 1,
@@ -1187,26 +1239,6 @@
 	etac adm_disj 1,
 	atac 1]);
 
-qed_goalw "admI" Fix.thy [adm_def]
- "(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
-\ ==> P(lub (range Y))) ==> adm P" 
- (fn prems => [
-	strip_tac 1,
-	case_tac "finite_chain Y" 1,
-	rewtac finite_chain_def,
-	safe_tac HOL_cs,
-	dtac lub_finch1 1,
-	atac 1,
-	dtac thelubI 1,
-	etac ssubst 1,
-	etac spec 1,
-	etac swap 1,
-	rewtac max_in_chain_def,
-	resolve_tac prems 1, atac 1, atac 1,
-	fast_tac (HOL_cs addDs [le_imp_less_or_eq] 
-			 addEs [chain_mono RS mp]) 1]);
+val adm_thms = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
+        adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less];
 
-val adm_thms = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
-        adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less
-        ];
-