Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
----------------------------------------------------------------------
authorregensbu
Mon, 28 Nov 1994 19:48:30 +0100
changeset 752 b89462f9d5f1
parent 751 f0aacbcedb77
child 753 ec86863e87c8
---------------------------------------------------------------------- Committing in HOLCF Use new translation mechanism and keyword syntax, cinfix.ML no longer needed. Optimized proofs in Cont.ML Modified Files: Cfun1.ML Cfun2.thy Cont.ML Cprod3.thy Makefile README Sprod3.thy Tr2.thy ccc1.thy ----------------------------------------------------------------------
src/HOLCF/Cfun1.ML file | annotate | diff | comparison | revisions
src/HOLCF/Cfun2.thy file | annotate | diff | comparison | revisions
src/HOLCF/Cont.ML file | annotate | diff | comparison | revisions
src/HOLCF/Cprod3.thy file | annotate | diff | comparison | revisions
src/HOLCF/Makefile file | annotate | diff | comparison | revisions
src/HOLCF/README file | annotate | diff | comparison | revisions
src/HOLCF/Sprod3.thy file | annotate | diff | comparison | revisions
src/HOLCF/Tr2.thy file | annotate | diff | comparison | revisions
src/HOLCF/ccc1.thy file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Cfun1.ML	Fri Nov 25 11:13:55 1994 +0100
+++ b/src/HOLCF/Cfun1.ML	Mon Nov 28 19:48:30 1994 +0100
@@ -120,10 +120,3 @@
 	(atac 1)
 	]);
 
-(* ------------------------------------------------------------------------ *)
-(* load ML file cinfix.ML                                                   *)
-(* ------------------------------------------------------------------------ *)
-
-
- writeln "Reading file  cinfix.ML"; 
-use "cinfix.ML";
--- a/src/HOLCF/Cfun2.thy	Fri Nov 25 11:13:55 1994 +0100
+++ b/src/HOLCF/Cfun2.thy	Mon Nov 28 19:48:30 1994 +0100
@@ -28,12 +28,3 @@
 
 end
 
-ML
-
-(* ----------------------------------------------------------------------*)
-(* unique setup of print translation for fapp                            *)
-(* ----------------------------------------------------------------------*)
-
-val print_translation = [("fapp",fapptr')];
-
-
--- a/src/HOLCF/Cont.ML	Fri Nov 25 11:13:55 1994 +0100
+++ b/src/HOLCF/Cont.ML	Mon Nov 28 19:48:30 1994 +0100
@@ -172,8 +172,7 @@
 (* ------------------------------------------------------------------------ *)
 
 val ch2ch_MF2L = prove_goal Cont.thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::po));\
-\	is_chain(F)|] ==> is_chain(%i. MF2(F(i),x))"
+"[|monofun(MF2); is_chain(F)|] ==> is_chain(%i. MF2(F(i),x))"
 (fn prems =>
 	[
 	(cut_facts_tac prems 1),
@@ -182,8 +181,8 @@
 	]);
 
 
-val ch2ch_MF2R = prove_goal Cont.thy "[|monofun(MF2(f)::('b::po=>'c::po));\
-\	is_chain(Y)|] ==> is_chain(%i. MF2(f,Y(i)))"
+val ch2ch_MF2R = prove_goal Cont.thy 
+"[|monofun(MF2(f)); is_chain(Y)|] ==> is_chain(%i. MF2(f,Y(i)))"
 (fn prems =>
 	[
 	(cut_facts_tac prems 1),
@@ -192,11 +191,9 @@
 	]);
 
 val ch2ch_MF2LR = prove_goal Cont.thy 
-"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
-\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
-\	is_chain(F); is_chain(Y)|] ==> \
+"[|monofun(MF2); !f.monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \
 \  is_chain(%i. MF2(F(i))(Y(i)))"
-(fn prems =>
+ (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac is_chainI 1),
@@ -208,6 +205,7 @@
 	(etac (is_chainE RS spec) 1)
 	]);
 
+
 val ch2ch_lubMF2R = prove_goal Cont.thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
 \  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
@@ -268,162 +266,113 @@
 	(atac 1)
 	]);
 
-
 val ex_lubMF2 = prove_goal Cont.thy 
 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
 \  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
 \	is_chain(F); is_chain(Y)|] ==> \
 \		lub(range(%j. lub(range(%i. MF2(F(j),Y(i)))))) =\
 \		lub(range(%i. lub(range(%j. MF2(F(j),Y(i))))))"
-(fn prems =>
+ (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac antisym_less 1),
-	(rtac is_lub_thelub 1),
+	(rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
 	(etac ch2ch_lubMF2R 1),
-	(atac 1),(atac 1),(atac 1),
-	(rtac ub_rangeI 1),
+	(REPEAT (atac 1)),
 	(strip_tac 1),
 	(rtac lub_mono 1),
 	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
 	(atac 1),
 	(etac ch2ch_lubMF2L 1),
-	(atac 1),(atac 1),(atac 1),
+	(REPEAT (atac 1)),
 	(strip_tac 1),
 	(rtac is_ub_thelub 1),
-	(etac ch2ch_MF2L 1),(atac 1),
-	(rtac is_lub_thelub 1),
+	(etac ch2ch_MF2L 1),
+	(atac 1),
+	(rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
 	(etac ch2ch_lubMF2L 1),
-	(atac 1),(atac 1),(atac 1),
-	(rtac ub_rangeI 1),
+	(REPEAT (atac 1)),
 	(strip_tac 1),
 	(rtac lub_mono 1),
-	(etac ch2ch_MF2L 1),(atac 1),
+	(etac ch2ch_MF2L 1),
+	(atac 1),
 	(etac ch2ch_lubMF2R 1),
-	(atac 1),(atac 1),(atac 1),
+	(REPEAT (atac 1)),
 	(strip_tac 1),
 	(rtac is_ub_thelub 1),
 	((rtac ch2ch_MF2R 1) THEN (etac spec 1)),
 	(atac 1)
 	]);
 
-(* ------------------------------------------------------------------------ *)
-(* The following results are about a curried function that is continuous    *)
-(* in both arguments                                                        *)
-(* ------------------------------------------------------------------------ *)
 
-val diag_lemma1 = prove_goal Cont.thy 
-"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
-\ is_chain(%i. lub(range(%j. CF2(FY(j), TY(i)))))"
- (fn prems =>
-	[
-	(cut_facts_tac prems 1),
-	(rtac ch2ch_lubMF2L 1),
-	(rtac contX2mono 1),
-	(atac 1),
-	(rtac allI 1),
-	(rtac contX2mono 1),
-	(etac spec 1),
-	(atac 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),
-	(etac allE 1),
-	(etac contX2mono 1),
-	(atac 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))))"
+val diag_lubMF2_1 = prove_goal Cont.thy 
+"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+\  is_chain(FY);is_chain(TY)|] ==>\
+\ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\
+\ lub(range(%i. MF2(FY(i))(TY(i))))"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac antisym_less 1),
-	(rtac is_lub_thelub 1),
-	(etac diag_lemma1 1),
+	(rtac (ub_rangeI RSN (2,is_lub_thelub)) 1),
+	(etac ch2ch_lubMF2L 1),
 	(REPEAT (atac 1)),
-	(rtac ub_rangeI 1),
 	(strip_tac 1 ),
 	(rtac lub_mono3 1),
-	(etac diag_lemma2 1),
+	(etac ch2ch_MF2L 1),
 	(REPEAT (atac 1)),
-	(etac diag_lemma4 1),
+	(etac ch2ch_MF2LR 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),
+	(etac allE 1),
+	(etac ch2ch_MF2R 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),
+	(etac ch2ch_MF2L 1),
 	(REPEAT (atac 1)),
 	(rtac lub_mono 1),
-	(etac diag_lemma4 1),
-	(REPEAT (atac 1)),
-	(etac diag_lemma1 1),
+	(etac ch2ch_MF2LR 1),
+	(REPEAT(atac 1)),
+	(etac ch2ch_lubMF2L 1),
 	(REPEAT (atac 1)),
 	(strip_tac 1 ),
 	(rtac is_ub_thelub 1),
-	(etac diag_lemma2 1),
-	(REPEAT (atac 1))
+	(etac ch2ch_MF2L 1),
+	(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))))"
+val diag_lubMF2_2 = prove_goal Cont.thy 
+"[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\
+\  !f.monofun(MF2(f)::('b::po=>'c::pcpo));\
+\  is_chain(FY);is_chain(TY)|] ==>\
+\ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\
+\ lub(range(%i. MF2(FY(i))(TY(i))))"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
 	(rtac trans 1),
 	(rtac ex_lubMF2 1),
-	(etac contX2mono 1),
-	(rtac allI 1),
-	(etac allE 1),
-	(etac contX2mono 1),
 	(REPEAT (atac 1)),
-	(rtac diag_lubCF2_1 1),
+	(etac diag_lubMF2_1 1),
 	(REPEAT (atac 1))
 	]);
 
+
+
+
+(* ------------------------------------------------------------------------ *)
+(* The following results are about a curried function that is continuous    *)
+(* in both arguments                                                        *)
+(* ------------------------------------------------------------------------ *)
+
 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))))"
@@ -436,13 +385,16 @@
 	(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),
+	(rtac diag_lubMF2_2 1),
+	(etac contX2mono 1),
+	(rtac allI 1),
+	(etac allE 1),
+	(etac contX2mono 1),
 	(REPEAT (atac 1))
 	]);
- 
+
 (* ------------------------------------------------------------------------ *)
 (* The following results are about application for functions in 'a=>'b      *)
 (* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Cprod3.thy	Fri Nov 25 11:13:55 1994 +0100
+++ b/src/HOLCF/Cprod3.thy	Mon Nov 28 19:48:30 1994 +0100
@@ -13,14 +13,14 @@
 arities "*" :: (pcpo,pcpo)pcpo			(* Witness cprod2.ML *)
 
 consts  
-	"@cpair"     :: "'a => 'b => ('a*'b)" ("_#_" [101,100] 100)
-	"cop @cpair" :: "'a -> 'b -> ('a*'b)" ("cpair")
-					(* continuous  pairing *)
+	cpair        :: "'a -> 'b -> ('a*'b)" (* continuous  pairing *)
 	cfst         :: "('a*'b)->'a"
 	csnd         :: "('a*'b)->'b"
 	csplit       :: "('a->'b->'c)->('a*'b)->'c"
 
-translations "x#y" => "cpair[x][y]"
+syntax	"@cpair"     :: "'a => 'b => ('a*'b)" ("_#_" [101,100] 100)
+
+translations "x#y" == "cpair[x][y]"
 
 rules 
 
--- a/src/HOLCF/Makefile	Fri Nov 25 11:13:55 1994 +0100
+++ b/src/HOLCF/Makefile	Mon Nov 28 19:48:30 1994 +0100
@@ -20,7 +20,7 @@
 	Porder0.thy Porder.thy Porder.ML  Pcpo.thy \
 	Pcpo.ML Fun1.thy Fun1.ML Fun2.thy Fun2.ML Fun3.thy Fun3.ML \
 	Cfun1.thy Cfun1.ML Cfun2.thy Cfun2.ML Cfun3.thy Cfun3.ML \
-	Cont.thy Cont.ML cinfix.ML\
+	Cont.thy Cont.ML \
 	Cprod1.thy Cprod1.ML Cprod2.thy Cprod2.ML Cprod3.thy Cprod3.ML \
 	Sprod0.thy Sprod0.ML Sprod1.thy Sprod1.ML Sprod2.thy Sprod2.ML\
 	Sprod3.thy Sprod3.ML\
--- a/src/HOLCF/README	Fri Nov 25 11:13:55 1994 +0100
+++ b/src/HOLCF/README	Mon Nov 28 19:48:30 1994 +0100
@@ -4,12 +4,13 @@
 Author:     Franz Regensburger
 Copyright   1993,1994 Technische Universitaet Muenchen
 
-Version: 1.4
-Date: 06.10.94
+Version: 1.5
+Date: 14.10.94
 
 A detailed description of the entire development can be found in 
 
 [Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
                      Dissertation, Technische Universit"at M"unchen, 1994
 
-
+Changes:
+14.10. New translation mechanism for continuous infixes
--- a/src/HOLCF/Sprod3.thy	Fri Nov 25 11:13:55 1994 +0100
+++ b/src/HOLCF/Sprod3.thy	Mon Nov 28 19:48:30 1994 +0100
@@ -10,13 +10,14 @@
 
 arities "**" :: (pcpo,pcpo)pcpo			(* Witness sprod2.ML *)
 
-consts
+consts  
 	spair        :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
 	sfst         :: "('a**'b)->'a"
 	ssnd         :: "('a**'b)->'b"
 	ssplit       :: "('a->'b->'c)->('a**'b)->'c"
 
-syntax	"@spair"     :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
+syntax  "@spair"     :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
+
 translations "x##y" == "spair[x][y]"
 
 rules 
--- a/src/HOLCF/Tr2.thy	Fri Nov 25 11:13:55 1994 +0100
+++ b/src/HOLCF/Tr2.thy	Mon Nov 28 19:48:30 1994 +0100
@@ -9,20 +9,19 @@
 Tr2 = Tr1 +
 
 consts
-	"@cifte"	:: "tr=>'c=>'c=>'c"
+	Icifte		:: "tr -> 'c -> 'c -> 'c"
+	trand		:: "tr -> tr -> tr"
+	tror		:: "tr -> tr -> tr"
+        neg		:: "tr -> tr"
+
+syntax 	"@cifte"	:: "tr=>'c=>'c=>'c"
                              ("(3If _/ (then _/ else _) fi)" 60)
-	"Icifte"        :: "tr->'c->'c->'c"
-
 	"@andalso"	:: "tr => tr => tr" ("_ andalso _" [36,35] 35)
-	"cop @andalso"	:: "tr -> tr -> tr" ("trand")
 	"@orelse"	:: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
-	"cop @orelse"	:: "tr -> tr -> tr" ("tror")
-
-        "neg"           :: "tr -> tr"
-
-translations "x andalso y" => "trand[x][y]"
-             "x orelse y"  => "tror[x][y]"
-             "If b then e1 else e2 fi" => "Icifte[b][e1][e2]"
+ 
+translations "x andalso y" == "trand[x][y]"
+             "x orelse y"  == "tror[x][y]"
+             "If b then e1 else e2 fi" == "Icifte[b][e1][e2]"
               
 rules
 
--- a/src/HOLCF/ccc1.thy	Fri Nov 25 11:13:55 1994 +0100
+++ b/src/HOLCF/ccc1.thy	Mon Nov 28 19:48:30 1994 +0100
@@ -10,13 +10,12 @@
 ccc1 = Cprod3 + Sprod3 + Ssum3 + Lift3 + Fix +
 
 consts
-
-	ID 		:: "'a -> 'a"
+	ID 	:: "'a -> 'a"
+	cfcomp	:: "('b->'c)->('a->'b)->'a->'c"
 
-	"@oo"		:: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
-	"cop @oo"	:: "('b->'c)->('a->'b)->'a->'c" ("cfcomp")
-
-translations "f1 oo f2" => "cfcomp[f1][f2]"
+syntax	"@oo"	:: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
+     
+translations 	"f1 oo f2" == "cfcomp[f1][f2]"
 
 rules
isabelle