# HG changeset patch # User regensbu # Date 786048510 -3600 # Node ID b89462f9d5f1895db56b35540d8f1b79665420e4 # Parent f0aacbcedb777f2ad6d39263091a37d23215d842 ---------------------------------------------------------------------- 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 ---------------------------------------------------------------------- diff -r f0aacbcedb77 -r b89462f9d5f1 src/HOLCF/Cfun1.ML --- 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"; diff -r f0aacbcedb77 -r b89462f9d5f1 src/HOLCF/Cfun2.thy --- 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')]; - - diff -r f0aacbcedb77 -r b89462f9d5f1 src/HOLCF/Cont.ML --- 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 *) (* ------------------------------------------------------------------------ *) diff -r f0aacbcedb77 -r b89462f9d5f1 src/HOLCF/Cprod3.thy --- 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 diff -r f0aacbcedb77 -r b89462f9d5f1 src/HOLCF/Makefile --- 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\ diff -r f0aacbcedb77 -r b89462f9d5f1 src/HOLCF/README --- 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 diff -r f0aacbcedb77 -r b89462f9d5f1 src/HOLCF/Sprod3.thy --- 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 diff -r f0aacbcedb77 -r b89462f9d5f1 src/HOLCF/Tr2.thy --- 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 diff -r f0aacbcedb77 -r b89462f9d5f1 src/HOLCF/ccc1.thy --- 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