# HG changeset patch # User oheimb # Date 833565319 -7200 # Node ID 1155c06fa9567c20cd9facabaaf401e161b21578 # Parent 6c942cf3bf68ddc2954c022ea349c752d105d33d introduced forgotten bind_thm calls diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cfun2.ML --- a/src/HOLCF/Cfun2.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Cfun2.ML Fri May 31 19:55:19 1996 +0200 @@ -48,11 +48,11 @@ (rtac Rep_Cfun 1) ]); -val monofun_fapp2 = cont_fapp2 RS cont2mono; +bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono); (* monofun(fapp(?fo1)) *) -val contlub_fapp2 = cont_fapp2 RS cont2contlub; +bind_thm ("contlub_fapp2", cont_fapp2 RS cont2contlub); (* contlub(fapp(?fo1)) *) (* ------------------------------------------------------------------------ *) @@ -60,10 +60,10 @@ (* looks nice with mixfix syntac *) (* ------------------------------------------------------------------------ *) -val cont_cfun_arg = (cont_fapp2 RS contE RS spec RS mp); +bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp)); (* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1)) *) -val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp); +bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp)); (* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *) @@ -93,7 +93,7 @@ ]); -val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp); +bind_thm ("monofun_cfun_arg", monofun_fapp2 RS monofunE RS spec RS spec RS mp); (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1 *) (* ------------------------------------------------------------------------ *) @@ -125,7 +125,7 @@ ]); -val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L); +bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L); (* is_chain(?F) ==> is_chain (%i. ?F i`?x) *) @@ -210,7 +210,7 @@ (etac (monofun_fapp1 RS ub2ub_monofun) 1) ]); -val thelub_cfun = (lub_cfun RS thelubI); +bind_thm ("thelub_cfun", lub_cfun RS thelubI); (* is_chain(?CCF1) ==> lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x))) *) diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cfun3.ML --- a/src/HOLCF/Cfun3.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Cfun3.ML Fri May 31 19:55:19 1996 +0200 @@ -183,7 +183,7 @@ (* lemma for the cont tactic *) (* ------------------------------------------------------------------------ *) -val cont2cont_LAM2 = (allI RSN (2,(allI RS cont2cont_LAM))); +bind_thm ("cont2cont_LAM2", allI RSN (2,(allI RS cont2cont_LAM))); (* [| !!x. cont (?c1.0 x); !!y. cont (%x. ?c1.0 x y) |] ==> cont (%x. LAM y. ?c1.0 x y) @@ -343,10 +343,10 @@ ]); -val cont_Istrictify1 = (contlub_Istrictify1 RS +bind_thm ("cont_Istrictify1", contlub_Istrictify1 RS (monofun_Istrictify1 RS monocontlub2cont)); -val cont_Istrictify2 = (contlub_Istrictify2 RS +bind_thm ("cont_Istrictify2", contlub_Istrictify2 RS (monofun_Istrictify2 RS monocontlub2cont)); diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cont.ML --- a/src/HOLCF/Cont.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Cont.ML Fri May 31 19:55:19 1996 +0200 @@ -578,7 +578,7 @@ ]); -val cont2cont_app2 = (allI RSN (2,cont2cont_app)); +bind_thm ("cont2cont_app2", allI RSN (2,cont2cont_app)); (* [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *) (* cont (%x. ?ft x (?tt x)) *) diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cprod2.ML --- a/src/HOLCF/Cprod2.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Cprod2.ML Fri May 31 19:55:19 1996 +0200 @@ -160,7 +160,7 @@ (etac (monofun_snd RS ub2ub_monofun) 1) ]); -val thelub_cprod = (lub_cprod RS thelubI); +bind_thm ("thelub_cprod", lub_cprod RS thelubI); (* "is_chain ?S1 ==> lub (range ?S1) = diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cprod3.ML --- a/src/HOLCF/Cprod3.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Cprod3.ML Fri May 31 19:55:19 1996 +0200 @@ -283,7 +283,7 @@ (atac 1) ]); -val thelub_cprod2 = (lub_cprod2 RS thelubI); +bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI); (* is_chain ?S1 ==> lub (range ?S1) = diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Fix.ML --- a/src/HOLCF/Fix.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Fix.ML Fri May 31 19:55:19 1996 +0200 @@ -587,7 +587,7 @@ ]); -val adm_flat = flat_imp_chain_finite RS adm_chain_finite; +bind_thm ("adm_flat", flat_imp_chain_finite RS adm_chain_finite); (* is_flat(?x::?'a) ==> adm(?P::?'a => bool) *) qed_goalw "flat_void" Fix.thy [is_flat_def] "is_flat(UU::void)" @@ -828,7 +828,7 @@ (etac spec 1) ]); -val adm_all2 = (allI RS adm_all); +bind_thm ("adm_all2", allI RS adm_all); qed_goal "adm_subst" Fix.thy "[|cont t; adm P|] ==> adm(%x. P (t x))" diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Fun2.ML --- a/src/HOLCF/Fun2.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Fun2.ML Fri May 31 19:55:19 1996 +0200 @@ -92,7 +92,7 @@ (etac ub2ub_fun 1) ]); -val thelub_fun = (lub_fun RS thelubI); +bind_thm ("thelub_fun", lub_fun RS thelubI); (* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *) qed_goal "cpo_fun" Fun2.thy diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Lift2.ML --- a/src/HOLCF/Lift2.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Lift2.ML Fri May 31 19:55:19 1996 +0200 @@ -154,13 +154,13 @@ (rtac minimal_lift 1) ]); -val thelub_lift1a = lub_lift1a RS thelubI; +bind_thm ("thelub_lift1a", lub_lift1a RS thelubI); (* [| is_chain ?Y1; ? i x. ?Y1 i = Iup x |] ==> lub (range ?Y1) = Iup (lub (range (%i. Ilift (LAM x. x) (?Y1 i)))) *) -val thelub_lift1b = lub_lift1b RS thelubI; +bind_thm ("thelub_lift1b", lub_lift1b RS thelubI); (* [| is_chain ?Y1; ! i x. ?Y1 i ~= Iup x |] ==> lub (range ?Y1) = UU_lift diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Pcpo.ML --- a/src/HOLCF/Pcpo.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Pcpo.ML Fri May 31 19:55:19 1996 +0200 @@ -27,10 +27,10 @@ (* ------------------------------------------------------------------------ *) -val is_ub_thelub = (cpo RS lubI RS is_ub_lub); +bind_thm ("is_ub_thelub", cpo RS lubI RS is_ub_lub); (* is_chain(?S1) ==> ?S1(?x) << lub(range(?S1)) *) -val is_lub_thelub = (cpo RS lubI RS is_lub_lub); +bind_thm ("is_lub_thelub", cpo RS lubI RS is_lub_lub); (* [| is_chain(?S5); range(?S5) <| ?x1 |] ==> lub(range(?S5)) << ?x1 *) diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Porder.ML --- a/src/HOLCF/Porder.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Porder.ML Fri May 31 19:55:19 1996 +0200 @@ -216,10 +216,10 @@ (etac spec 1) ]); -val is_ub_lub = (is_lubE RS conjunct1 RS ub_rangeE RS spec); +bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec); (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) -val is_lub_lub = (is_lubE RS conjunct2 RS spec RS mp); +bind_thm ("is_lub_lub", is_lubE RS conjunct2 RS spec RS mp); (* [| ?S3 <<| ?x3; ?S3 <| ?x1 |] ==> ?x3 << ?x1 *) (* ------------------------------------------------------------------------ *) @@ -276,7 +276,7 @@ (* lub(?M) = UU_void *) (* ------------------------------------------------------------------------ *) -val thelub_void = (lub_void RS thelubI); +bind_thm ("thelub_void", lub_void RS thelubI); (* ------------------------------------------------------------------------ *) (* void is a cpo wrt. countable chains *) diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/ROOT.ML --- a/src/HOLCF/ROOT.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/ROOT.ML Fri May 31 19:55:19 1996 +0200 @@ -11,6 +11,8 @@ init_thy_reader(); (* start 8bit 1 *) +val banner = + "HOLCF with sections axioms,ops,domain,generated and 8bit characters"; (* end 8bit 1 *) writeln banner; diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Sprod2.ML --- a/src/HOLCF/Sprod2.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Sprod2.ML Fri May 31 19:55:19 1996 +0200 @@ -42,7 +42,7 @@ (etac (inst_sprod_po RS subst) 1) ]); -val less_sprod4a = (less_sprod4b RS defined_Ispair_rev); +bind_thm ("less_sprod4a", less_sprod4b RS defined_Ispair_rev); (* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *) qed_goal "less_sprod4c" Sprod2.thy @@ -252,7 +252,7 @@ (etac (monofun_Issnd RS ub2ub_monofun) 1) ]); -val thelub_sprod = (lub_sprod RS thelubI); +bind_thm ("thelub_sprod", lub_sprod RS thelubI); qed_goal "cpo_sprod" Sprod2.thy diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Sprod3.ML --- a/src/HOLCF/Sprod3.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Sprod3.ML Fri May 31 19:55:19 1996 +0200 @@ -612,7 +612,7 @@ ]); -val thelub_sprod2 = (lub_sprod2 RS thelubI); +bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI); (* "is_chain ?S1 ==> lub (range ?S1) = diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Ssum2.ML --- a/src/HOLCF/Ssum2.ML Fri May 31 19:47:23 1996 +0200 +++ b/src/HOLCF/Ssum2.ML Fri May 31 19:55:19 1996 +0200 @@ -390,14 +390,14 @@ ]); -val thelub_ssum1a = lub_ssum1a RS thelubI; +bind_thm ("thelub_ssum1a", lub_ssum1a RS thelubI); (* [| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinl x |] ==> lub (range ?Y1) = Isinl (lub (range (%i. Iwhen (LAM x. x) (LAM y. UU) (?Y1 i)))) *) -val thelub_ssum1b = lub_ssum1b RS thelubI; +bind_thm ("thelub_ssum1b", lub_ssum1b RS thelubI); (* [| is_chain ?Y1; ! i. ? x. ?Y1 i = Isinr x |] ==> lub (range ?Y1) = Isinr