Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/Cont.ML
changeset 625 119391dd1d59
parent 243 c22b85994e17
child 752 b89462f9d5f1 
--- a/src/HOLCF/Cont.ML	Tue Oct 04 13:02:16 1994 +0100
+++ b/src/HOLCF/Cont.ML	Thu Oct 06 18:40:18 1994 +0100
@@ -312,15 +312,12 @@
 (* in both arguments                                                        *)
 (* ------------------------------------------------------------------------ *)
 
-val diag_lubCF2_1 = prove_goal Cont.thy 
+val diag_lemma1 = prove_goal Cont.thy 
 "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
-\ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
-\ lub(range(%i. CF2(FY(i))(TY(i))))"
-(fn prems =>
+\ is_chain(%i. lub(range(%j. CF2(FY(j), TY(i)))))"
+ (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(rtac antisym_less 1),
-	(rtac is_lub_thelub 1),
 	(rtac ch2ch_lubMF2L 1),
 	(rtac contX2mono 1),
 	(atac 1),
@@ -328,109 +325,124 @@
 	(rtac contX2mono 1),
 	(etac spec 1),
 	(atac 1),
-	(atac 1),
-	(rtac ub_rangeI 1),
-	(strip_tac 1 ),
-	(rtac is_lub_thelub 1),
-	((rtac ch2ch_MF2L 1) THEN (rtac contX2mono 1) THEN (atac 1)),
-	(atac 1),
-	(rtac ub_rangeI 1),
-	(strip_tac 1 ),
-	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
-	(rtac trans_less 1),
-	(rtac is_ub_thelub 2),
-	(rtac (chain_mono RS mp) 1),
-	((rtac ch2ch_MF2R 1) THEN (rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
-	(atac 1),
-	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
+	(atac 1)
+	]);
+
+val diag_lemma2 = prove_goal Cont.thy 
+"[|contX(CF2);is_chain(FY); is_chain(TY) |] ==>\
+\ is_chain(%m. CF2(FY(m), TY(n::nat)))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac (contX2mono RS ch2ch_MF2L) 1),
+	(atac 1)
+	]);
+
+val diag_lemma3 = prove_goal Cont.thy 
+"[|!f.contX(CF2(f));is_chain(FY); is_chain(TY) |] ==>\
+\ is_chain(%m. CF2(FY(n), TY(m)))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac allE 1),
+	(etac (contX2mono RS ch2ch_MF2R) 1),
+	(atac 1)
+	]);
+
+val diag_lemma4 = prove_goal Cont.thy 
+"[|contX(CF2);!f.contX(CF2(f));is_chain(FY); is_chain(TY) |] ==>\
+\ is_chain(%m. CF2(FY(m), TY(m)))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac (contX2mono RS ch2ch_MF2LR) 1),
 	(rtac allI 1),
-	((rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
-	(atac 1),
-	(hyp_subst_tac 1),
-	(rtac is_ub_thelub 1),
-	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
-	(rtac allI 1),
-	((rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
+	(etac allE 1),
+	(etac contX2mono 1),
 	(atac 1),
-	(rtac trans_less 1),
-	(rtac is_ub_thelub 2),
-	(res_inst_tac [("x1","ia")] (chain_mono RS mp) 1),
-	((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
-	(atac 1),
-	(atac 1),
-	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
-	(rtac allI 1),
-	((rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
-	(atac 1),
-	(rtac lub_mono 1),
-	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
-	(rtac allI 1),
-	((rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
-	(atac 1),
-	(rtac ch2ch_lubMF2L 1),
-	(rtac contX2mono 1),
-	(atac 1),
-	(rtac allI 1),
-	((rtac contX2mono 1) THEN (etac spec 1)),
-	(atac 1),
-	(atac 1),
-	(strip_tac 1 ),
-	(rtac is_ub_thelub 1),
-	((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
 	(atac 1)
 	]);
 
 
+val diag_lubCF2_1 = prove_goal Cont.thy 
+"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
+\ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
+\ lub(range(%i. CF2(FY(i))(TY(i))))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(rtac antisym_less 1),
+	(rtac is_lub_thelub 1),
+	(etac diag_lemma1 1),
+	(REPEAT (atac 1)),
+	(rtac ub_rangeI 1),
+	(strip_tac 1 ),
+	(rtac lub_mono3 1),
+	(etac diag_lemma2 1),
+	(REPEAT (atac 1)),
+	(etac diag_lemma4 1),
+	(REPEAT (atac 1)),
+	(rtac allI 1),
+	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
+	(res_inst_tac [("x","ia")] exI 1),
+	(rtac (chain_mono RS mp) 1),
+	(etac diag_lemma3 1),
+	(REPEAT (atac 1)),
+	(hyp_subst_tac 1),
+	(res_inst_tac [("x","ia")] exI 1),
+	(rtac refl_less 1),
+	(res_inst_tac [("x","i")] exI 1),
+	(rtac (chain_mono RS mp) 1),
+	(etac diag_lemma2 1),
+	(REPEAT (atac 1)),
+	(rtac lub_mono 1),
+	(etac diag_lemma4 1),
+	(REPEAT (atac 1)),
+	(etac diag_lemma1 1),
+	(REPEAT (atac 1)),
+	(strip_tac 1 ),
+	(rtac is_ub_thelub 1),
+	(etac diag_lemma2 1),
+	(REPEAT (atac 1))
+	]);
+
 val diag_lubCF2_2 = prove_goal Cont.thy 
 "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
 \ lub(range(%j. lub(range(%i. CF2(FY(j))(TY(i)))))) =\
 \ lub(range(%i. CF2(FY(i))(TY(i))))"
-(fn prems =>
+ (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac trans 1),
 	(rtac ex_lubMF2 1),
-	(rtac ((hd prems) RS contX2mono) 1), 
+	(etac contX2mono 1),
 	(rtac allI 1),
-	(rtac (((hd (tl prems)) RS spec RS contX2mono)) 1),
-	(atac 1),
-	(atac 1),
+	(etac allE 1),
+	(etac contX2mono 1),
+	(REPEAT (atac 1)),
 	(rtac diag_lubCF2_1 1),
-	(atac 1),
-	(atac 1),
-	(atac 1),
-	(atac 1)
+	(REPEAT (atac 1))
 	]);
 
-
 val contlub_CF2 = prove_goal Cont.thy 
 "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
 \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
-(fn prems =>
+ (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(rtac ((hd prems) RS contX2contlub RS contlubE RS 
-		spec RS mp RS ssubst) 1),
+	(rtac ((hd prems) RS contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
 	(atac 1),
 	(rtac (thelub_fun RS ssubst) 1),
-	(rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1), 
+	(rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1),
 	(atac 1),
 	(rtac trans 1),
-	(rtac (((hd (tl prems)) RS spec RS contX2contlub) RS 
-	contlubE RS spec RS mp RS ext RS arg_cong RS arg_cong) 1),
+	(rtac (((hd (tl prems)) RS spec RS contX2contlub) RS contlubE RS 
+               spec RS mp RS ext RS arg_cong RS arg_cong) 1),
 	(atac 1),
 	(rtac diag_lubCF2_2 1),
-	(atac 1),
-	(atac 1),
-	(atac 1),
-	(atac 1)
+	(REPEAT (atac 1))
 	]);
-
+ 
 (* ------------------------------------------------------------------------ *)
 (* The following results are about application for functions in 'a=>'b      *)
 (* ------------------------------------------------------------------------ *)
@@ -574,24 +586,20 @@
 	(atac 1)
 	]);
 
+
 val contX2contlub_app = prove_goal Cont.thy 
-"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==>\
-\	 contlub(%x.(ft(x))(tt(x)))"
+"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac contlubI 1),
 	(strip_tac 1),
 	(res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1),
-	(rtac contX2contlub 1),
-	(resolve_tac prems 1),
+	(etac contX2contlub 1),
 	(atac 1),
 	(rtac contlub_CF2 1),
-	(resolve_tac prems 1),
-	(resolve_tac prems 1),
-	(atac 1),
-	(rtac (contX2mono RS ch2ch_monofun) 1),
-	(resolve_tac prems 1),
+	(REPEAT (atac 1)),
+	(etac (contX2mono RS ch2ch_monofun) 1),
 	(atac 1)
 	]);
isabelle