--- a/src/HOLCF/IsaMakefile Mon Feb 24 09:46:12 1997 +0100
+++ b/src/HOLCF/IsaMakefile Mon Feb 24 16:12:24 1997 +0100
@@ -45,18 +45,4 @@
test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES)
@$(ISATOOL) testdir $(OUT)/HOLCF ex
-
-## Explicit domains
-#
-#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy\
-# explicit_domains/Dlist.thy \
-# explicit_domains/Stream.thy explicit_domains/Stream2.thy
-
-#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \
-# $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
-#
-#test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES)
-# @$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains
-
-
.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF
--- a/src/HOLCF/Makefile Mon Feb 24 09:46:12 1997 +0100
+++ b/src/HOLCF/Makefile Mon Feb 24 16:12:24 1997 +0100
@@ -86,29 +86,5 @@
\"$(COMP)\" is not poly or sml;;\
esac
-#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy \
-# explicit_domains/Dlist.thy \
-# explicit_domains/Stream.thy explicit_domains/Stream2.thy
-
-#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\
-# $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
-
-#test2: explicit_domains/ROOT.ML $(BIN)/HOLCF $(EXPLICIT_DOMAINS_FILES)
-# @case `basename "$(COMP)"` in \
-# poly*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-# then echo 'make_html := true; exit_use_dir"explicit_domains";\
-# quit();' | $(COMP) $(BIN)/HOLCF;\
-# else echo 'exit_use_dir"explicit_domains"; quit();' \
-# | $(COMP) $(BIN)/HOLCF;\
-# fi;;\
-# sml*) if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
-# then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
-# | $(BIN)/HOLCF;\
-# else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
-# fi;;\
-# *) echo Bad value for ISABELLECOMP: \
-# \"$(COMP)\" is not poly or sml;;\
-# esac
-
.PRECIOUS: $(BIN)/HOL $(BIN)/HOLCF
--- a/src/HOLCF/ex/Coind.ML Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,126 +0,0 @@
-(* Title: FOCUS/ex/coind.ML
- ID: $ $
- Author: Franz Regensburger
- Copyright 1993, 1995 Technische Universitaet Muenchen
-*)
-
-open Coind;
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties *)
-(* ------------------------------------------------------------------------- *)
-
-
-val nats_def2 = fix_prover2 Coind.thy nats_def
- "nats = dzero&&(smap`dsucc`nats)";
-
-val from_def2 = fix_prover2 Coind.thy from_def
- "from = (¤n.n&&(from`(dsucc`n)))";
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* recursive properties *)
-(* ------------------------------------------------------------------------- *)
-
-
-val from = prove_goal Coind.thy "from`n = n&&(from`(dsucc`n))"
- (fn prems =>
- [
- (rtac trans 1),
- (rtac (from_def2 RS ssubst) 1),
- (simp_tac HOLCF_ss 1),
- (rtac refl 1)
- ]);
-
-
-val from1 = prove_goal Coind.thy "from`Ø = Ø"
- (fn prems =>
- [
- (rtac trans 1),
- (rtac (from RS ssubst) 1),
- (resolve_tac stream.con_rews 1),
- (rtac refl 1)
- ]);
-
-val coind_rews =
- [iterator1, iterator2, iterator3, smap1, smap2,from1];
-
-(* ------------------------------------------------------------------------- *)
-(* the example *)
-(* prove: nats = from`dzero *)
-(* ------------------------------------------------------------------------- *)
-
-val prems = goal Coind.thy "iterator`n`(smap`dsucc)`nats =\
-\ n&&(iterator`(dsucc`n)`(smap`dsucc)`nats)";
-by (res_inst_tac [("x","n")] dnat.ind 1);
-by (simp_tac (HOLCF_ss addsimps (coind_rews @ stream.rews)) 1);
-by (simp_tac (HOLCF_ss addsimps (coind_rews @ stream.rews)) 1);
-by (rtac trans 1);
-by (rtac nats_def2 1);
-by (simp_tac (HOLCF_ss addsimps (coind_rews @ dnat.rews)) 1);
-by (rtac trans 1);
-by (etac iterator3 1);
-by (rtac trans 1);
-by (asm_simp_tac HOLCF_ss 1);
-by (rtac trans 1);
-by (etac smap2 1);
-by (rtac cfun_arg_cong 1);
-by (asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat.rews)) 1);
-val coind_lemma1 = result();
-
-val prems = goal Coind.thy "nats = from`dzero";
-by (res_inst_tac [("R","% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream.coind 1);
-by (res_inst_tac [("x","dzero")] exI 2);
-by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 2);
-by (rewrite_goals_tac [stream.bisim_def]);
-by (strip_tac 1);
-by (etac exE 1);
-by (etac conjE 1);
-by (case_tac "n=Ø" 1);
-by (rtac disjI1 1);
-by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
-by (rtac disjI2 1);
-by (hyp_subst_tac 1);
-by (res_inst_tac [("x","n")] exI 1);
-by (res_inst_tac [("x","iterator`(dsucc`n)`(smap`dsucc)`nats")] exI 1);
-by (res_inst_tac [("x","from`(dsucc`n)")] exI 1);
-by (etac conjI 1);
-by (rtac conjI 1);
-by (res_inst_tac [("x","dsucc`n")] exI 1);
-by (fast_tac HOL_cs 1);
-by (rtac conjI 1);
-by (rtac coind_lemma1 1);
-by (rtac from 1);
-val nats_eq_from = result();
-
-(* another proof using stream_coind_lemma2 *)
-
-val prems = goal Coind.thy "nats = from`dzero";
-by (res_inst_tac [("R","% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream.coind 1);
-by (rtac stream_coind_lemma2 1);
-by (strip_tac 1);
-by (etac exE 1);
-by (case_tac "n=Ø" 1);
-by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
-by (res_inst_tac [("x","Ø::dnat")] exI 1);
-by (simp_tac (HOLCF_ss addsimps coind_rews addsimps stream.rews) 1);
-by (etac conjE 1);
-by (hyp_subst_tac 1);
-by (rtac conjI 1);
-by (rtac (coind_lemma1 RS ssubst) 1);
-by (rtac (from RS ssubst) 1);
-by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
-by (res_inst_tac [("x","dsucc`n")] exI 1);
-by (rtac conjI 1);
-by (rtac trans 1);
-by (rtac (coind_lemma1 RS ssubst) 1);
-by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
-by (rtac refl 1);
-by (rtac trans 1);
-by (rtac (from RS ssubst) 1);
-by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
-by (rtac refl 1);
-by (res_inst_tac [("x","dzero")] exI 1);
-by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
-val nats_eq_from = result();
--- a/src/HOLCF/ex/Coind.thy Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: FOCUS/ex/Coind.thy
- ID: $ $
- Author: Franz Regensburger
- Copyright 1993 195 Technische Universitaet Muenchen
-
-Example for co-induction on streams
-*)
-
-Coind = Stream + Dnat +
-
-
-consts
-
- nats :: "dnat stream"
- from :: "dnat è dnat stream"
-
-defs
- nats_def "nats Ú fix`(¤h.dzero&&(smap`dsucc`h))"
-
- from_def "from Ú fix`(¤h n.n&&(h`(dsucc`n)))"
-
-end
-
-(*
- smap`f`Ø = Ø
- xÛØ çè smap`f`(x&&xs) = (f`x)&&(smap`f`xs)
-
- nats = dzero&&(smap`dsucc`nats)
-
- from`n = n&&(from`(dsucc`n))
-*)
-
-
--- a/src/HOLCF/explicit_domains/Dlist.ML Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,566 +0,0 @@
-(* Title: HOLCF/Dlist.ML
- Author: Franz Regensburger
- ID: $ $
- Copyright 1994 Technische Universitaet Muenchen
-
-Lemmas for dlist.thy
-*)
-
-open Dlist;
-
-Delsimps (ex_simps @ all_simps);
-
-(* ------------------------------------------------------------------------*)
-(* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict *)
-(* ------------------------------------------------------------------------*)
-
-val dlist_iso_strict= dlist_rep_iso RS (dlist_abs_iso RS
- (allI RSN (2,allI RS iso_strict)));
-
-val dlist_rews = [dlist_iso_strict RS conjunct1,
- dlist_iso_strict RS conjunct2];
-
-(* ------------------------------------------------------------------------*)
-(* Properties of dlist_copy *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goalw Dlist.thy [dlist_copy_def] "dlist_copy`f`UU=UU"
- (fn prems =>
- [
- (asm_simp_tac (!simpset addsimps
- (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
- ]);
-
-val dlist_copy = [temp];
-
-
-val temp = prove_goalw Dlist.thy [dlist_copy_def,dnil_def]
- "dlist_copy`f`dnil=dnil"
- (fn prems =>
- [
- (asm_simp_tac (!simpset addsimps
- (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
- ]);
-
-val dlist_copy = temp :: dlist_copy;
-
-
-val temp = prove_goalw Dlist.thy [dlist_copy_def,dcons_def]
- "xl~=UU ==> dlist_copy`f`(dcons`x`xl)= dcons`x`(f`xl)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac (!simpset addsimps
- (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
- (case_tac "x=UU" 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps [defined_spair]) 1)
- ]);
-
-val dlist_copy = temp :: dlist_copy;
-
-val dlist_rews = dlist_copy @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Exhaustion and elimination for dlists *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "Exh_dlist" Dlist.thy [dcons_def,dnil_def]
- "l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons`x`xl)"
- (fn prems =>
- [
- (Simp_tac 1),
- (rtac (dlist_rep_iso RS subst) 1),
- (res_inst_tac [("p","dlist_rep`l")] ssumE 1),
- (rtac disjI1 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (rtac disjI2 1),
- (rtac disjI1 1),
- (res_inst_tac [("p","x")] oneE 1),
- (contr_tac 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (rtac disjI2 1),
- (rtac disjI2 1),
- (res_inst_tac [("p","y")] sprodE 1),
- (contr_tac 1),
- (rtac exI 1),
- (rtac exI 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (fast_tac HOL_cs 1)
- ]);
-
-
-qed_goal "dlistE" Dlist.thy
-"[| l=UU ==> Q; l=dnil ==> Q;!!x xl.[|l=dcons`x`xl;x~=UU;xl~=UU|]==>Q|]==>Q"
- (fn prems =>
- [
- (rtac (Exh_dlist RS disjE) 1),
- (eresolve_tac prems 1),
- (etac disjE 1),
- (eresolve_tac prems 1),
- (etac exE 1),
- (etac exE 1),
- (resolve_tac prems 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1)
- ]);
-
-(* ------------------------------------------------------------------------*)
-(* Properties of dlist_when *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goalw Dlist.thy [dlist_when_def] "dlist_when`f1`f2`UU=UU"
- (fn prems =>
- [
- (asm_simp_tac (!simpset addsimps [dlist_iso_strict]) 1)
- ]);
-
-val dlist_when = [temp];
-
-val temp = prove_goalw Dlist.thy [dlist_when_def,dnil_def]
- "dlist_when`f1`f2`dnil= f1"
- (fn prems =>
- [
- (asm_simp_tac (!simpset addsimps [dlist_abs_iso]) 1)
- ]);
-
-val dlist_when = temp::dlist_when;
-
-val temp = prove_goalw Dlist.thy [dlist_when_def,dcons_def]
- "[|x~=UU;xl~=UU|] ==> dlist_when`f1`f2`(dcons`x`xl)= f2`x`xl"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac (!simpset addsimps [dlist_abs_iso,defined_spair]) 1)
- ]);
-
-val dlist_when = temp::dlist_when;
-
-val dlist_rews = dlist_when @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Rewrites for discriminators and selectors *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm = prove_goalw Dlist.thy defs thm
- (fn prems =>
- [
- (simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-val dlist_discsel = [
- prover [is_dnil_def] "is_dnil`UU=UU",
- prover [is_dcons_def] "is_dcons`UU=UU",
- prover [dhd_def] "dhd`UU=UU",
- prover [dtl_def] "dtl`UU=UU"
- ];
-
-fun prover defs thm = prove_goalw Dlist.thy defs thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-val dlist_discsel = [
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
- "is_dnil`dnil=TT",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
- "[|x~=UU;xl~=UU|] ==> is_dnil`(dcons`x`xl)=FF",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
- "is_dcons`dnil=FF",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
- "[|x~=UU;xl~=UU|] ==> is_dcons`(dcons`x`xl)=TT",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
- "dhd`dnil=UU",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
- "[|x~=UU;xl~=UU|] ==> dhd`(dcons`x`xl)=x",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
- "dtl`dnil=UU",
-prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
- "[|x~=UU;xl~=UU|] ==> dtl`(dcons`x`xl)=xl"] @ dlist_discsel;
-
-val dlist_rews = dlist_discsel @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Definedness and strictness *)
-(* ------------------------------------------------------------------------*)
-
-fun prover contr thm = prove_goal Dlist.thy thm
- (fn prems =>
- [
- (res_inst_tac [("P1",contr)] classical2 1),
- (simp_tac (!simpset addsimps dlist_rews) 1),
- (dtac sym 1),
- (Asm_simp_tac 1),
- (simp_tac (!simpset addsimps (prems @ dlist_rews)) 1)
- ]);
-
-
-val dlist_constrdef = [
-prover "is_dnil`(UU::'a dlist) ~= UU" "dnil~=(UU::'a dlist)",
-prover "is_dcons`(UU::'a dlist) ~= UU"
- "[|x~=UU;xl~=UU|]==>dcons`(x::'a)`xl ~= UU"
- ];
-
-
-fun prover defs thm = prove_goalw Dlist.thy defs thm
- (fn prems =>
- [
- (simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-val dlist_constrdef = [
- prover [dcons_def] "dcons`UU`xl=UU",
- prover [dcons_def] "dcons`x`UU=UU"
- ] @ dlist_constrdef;
-
-val dlist_rews = dlist_constrdef @ dlist_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* Distinctness wrt. << and = *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goal Dlist.thy "~dnil << dcons`(x::'a)`xl"
- (fn prems =>
- [
- (res_inst_tac [("P1","TT << FF")] classical2 1),
- (resolve_tac dist_less_tr 1),
- (dres_inst_tac [("fo","is_dnil")] monofun_cfun_arg 1),
- (etac box_less 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (case_tac "(x::'a)=UU" 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (case_tac "(xl ::'a dlist)=UU" 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-val dlist_dist_less = [temp];
-
-val temp = prove_goal Dlist.thy "[|x~=UU;xl~=UU|]==>~ dcons`x`xl << dnil"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("P1","TT << FF")] classical2 1),
- (resolve_tac dist_less_tr 1),
- (dres_inst_tac [("fo","is_dcons")] monofun_cfun_arg 1),
- (etac box_less 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-val dlist_dist_less = temp::dlist_dist_less;
-
-val temp = prove_goal Dlist.thy "dnil ~= dcons`x`xl"
- (fn prems =>
- [
- (case_tac "x=UU" 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (case_tac "xl=UU" 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (res_inst_tac [("P1","TT = FF")] classical2 1),
- (resolve_tac dist_eq_tr 1),
- (dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
- (etac box_equals 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-val dlist_dist_eq = [temp,temp RS not_sym];
-
-val dlist_rews = dlist_dist_less @ dlist_dist_eq @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Invertibility *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
-\ dcons`x1`x2 << dcons`y1`y2 |] ==> x1<< y1 & x2 << y2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac conjI 1),
- (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
- (etac box_less 1),
- (asm_simp_tac (!simpset addsimps dlist_when) 1),
- (asm_simp_tac (!simpset addsimps dlist_when) 1),
- (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
- (etac box_less 1),
- (asm_simp_tac (!simpset addsimps dlist_when) 1),
- (asm_simp_tac (!simpset addsimps dlist_when) 1)
- ]);
-
-val dlist_invert =[temp];
-
-(* ------------------------------------------------------------------------*)
-(* Injectivity *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
-\ dcons`x1`x2 = dcons`y1`y2 |] ==> x1= y1 & x2 = y2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac conjI 1),
- (dres_inst_tac [("f","dlist_when`UU`(LAM x l.x)")] cfun_arg_cong 1),
- (etac box_equals 1),
- (asm_simp_tac (!simpset addsimps dlist_when) 1),
- (asm_simp_tac (!simpset addsimps dlist_when) 1),
- (dres_inst_tac [("f","dlist_when`UU`(LAM x l.l)")] cfun_arg_cong 1),
- (etac box_equals 1),
- (asm_simp_tac (!simpset addsimps dlist_when) 1),
- (asm_simp_tac (!simpset addsimps dlist_when) 1)
- ]);
-
-val dlist_inject = [temp];
-
-
-(* ------------------------------------------------------------------------*)
-(* definedness for discriminators and selectors *)
-(* ------------------------------------------------------------------------*)
-
-fun prover thm = prove_goal Dlist.thy thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac dlistE 1),
- (contr_tac 1),
- (REPEAT (asm_simp_tac (!simpset addsimps dlist_discsel) 1))
- ]);
-
-val dlist_discsel_def =
- [
- prover "l~=UU ==> is_dnil`l~=UU",
- prover "l~=UU ==> is_dcons`l~=UU"
- ];
-
-val dlist_rews = dlist_discsel_def @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* enhance the simplifier *)
-(* ------------------------------------------------------------------------*)
-
-qed_goal "dhd2" Dlist.thy "xl~=UU ==> dhd`(dcons`x`xl)=x"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (case_tac "x=UU" 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-qed_goal "dtl2" Dlist.thy "x~=UU ==> dtl`(dcons`x`xl)=xl"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (case_tac "xl=UU" 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-val dlist_rews = dhd2 :: dtl2 :: dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Properties dlist_take *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take n`UU=UU"
- (fn prems =>
- [
- (res_inst_tac [("n","n")] natE 1),
- (Asm_simp_tac 1),
- (Asm_simp_tac 1),
- (simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-val dlist_take = [temp];
-
-val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take 0`xs=UU"
- (fn prems =>
- [
- (Asm_simp_tac 1)
- ]);
-
-val dlist_take = temp::dlist_take;
-
-val temp = prove_goalw Dlist.thy [dlist_take_def]
- "dlist_take (Suc n)`dnil=dnil"
- (fn prems =>
- [
- (Asm_simp_tac 1),
- (simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-val dlist_take = temp::dlist_take;
-
-val temp = prove_goalw Dlist.thy [dlist_take_def]
- "dlist_take (Suc n)`(dcons`x`xl)= dcons`x`(dlist_take n`xl)"
- (fn prems =>
- [
- (case_tac "x=UU" 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (case_tac "xl=UU" 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (res_inst_tac [("n","n")] natE 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-val dlist_take = temp::dlist_take;
-
-val dlist_rews = dlist_take @ dlist_rews;
-
-(* ------------------------------------------------------------------------*)
-(* take lemma for dlists *)
-(* ------------------------------------------------------------------------*)
-
-fun prover reach defs thm = prove_goalw Dlist.thy defs thm
- (fn prems =>
- [
- (res_inst_tac [("t","l1")] (reach RS subst) 1),
- (res_inst_tac [("t","l2")] (reach RS subst) 1),
- (stac fix_def2 1),
- (stac contlub_cfun_fun 1),
- (rtac is_chain_iterate 1),
- (stac contlub_cfun_fun 1),
- (rtac is_chain_iterate 1),
- (rtac lub_equal 1),
- (rtac (is_chain_iterate RS ch2ch_fappL) 1),
- (rtac (is_chain_iterate RS ch2ch_fappL) 1),
- (rtac allI 1),
- (resolve_tac prems 1)
- ]);
-
-val dlist_take_lemma = prover dlist_reach [dlist_take_def]
- "(!!n.dlist_take n`l1 = dlist_take n`l2) ==> l1=l2";
-
-
-(* ------------------------------------------------------------------------*)
-(* Co -induction for dlists *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "dlist_coind_lemma" Dlist.thy [dlist_bisim_def]
-"dlist_bisim R ==> ! p q. R p q --> dlist_take n`p = dlist_take n`q"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps dlist_rews) 1),
- (strip_tac 1),
- ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
- (atac 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (etac disjE 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (etac exE 1),
- (etac exE 1),
- (etac exE 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (REPEAT (etac conjE 1)),
- (rtac cfun_arg_cong 1),
- (fast_tac HOL_cs 1)
- ]);
-
-qed_goal "dlist_coind" Dlist.thy "[|dlist_bisim R ; R p q |] ==> p = q"
- (fn prems =>
- [
- (rtac dlist_take_lemma 1),
- (rtac (dlist_coind_lemma RS spec RS spec RS mp) 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1)
- ]);
-
-(* ------------------------------------------------------------------------*)
-(* structural induction *)
-(* ------------------------------------------------------------------------*)
-
-qed_goal "dlist_finite_ind" Dlist.thy
-"[|P(UU);P(dnil);\
-\ !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons`x`l1)\
-\ |] ==> !l.P(dlist_take n`l)"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps dlist_rews) 1),
- (resolve_tac prems 1),
- (rtac allI 1),
- (res_inst_tac [("l","l")] dlistE 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (case_tac "dlist_take n1`xl=UU" 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1),
- (atac 1),
- (atac 1),
- (etac spec 1)
- ]);
-
-qed_goal "dlist_all_finite_lemma1" Dlist.thy
-"!l.dlist_take n`l=UU |dlist_take n`l=l"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps dlist_rews) 1),
- (rtac allI 1),
- (res_inst_tac [("l","l")] dlistE 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (eres_inst_tac [("x","xl")] allE 1),
- (etac disjE 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1)
- ]);
-
-qed_goal "dlist_all_finite_lemma2" Dlist.thy "? n.dlist_take n`l=l"
- (fn prems =>
- [
- (case_tac "l=UU" 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (subgoal_tac "(!n.dlist_take n`l=UU) |(? n.dlist_take n`l = l)" 1),
- (etac disjE 1),
- (eres_inst_tac [("P","l=UU")] notE 1),
- (rtac dlist_take_lemma 1),
- (asm_simp_tac (!simpset addsimps dlist_rews) 1),
- (atac 1),
- (subgoal_tac "!n.!l.dlist_take n`l=UU |dlist_take n`l=l" 1),
- (fast_tac HOL_cs 1),
- (rtac allI 1),
- (rtac dlist_all_finite_lemma1 1)
- ]);
-
-qed_goalw "dlist_all_finite" Dlist.thy [dlist_finite_def] "dlist_finite(l)"
- (fn prems =>
- [
- (rtac dlist_all_finite_lemma2 1)
- ]);
-
-qed_goal "dlist_ind" Dlist.thy
-"[|P(UU);P(dnil);\
-\ !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons`x`l1)|] ==> P(l)"
- (fn prems =>
- [
- (rtac (dlist_all_finite_lemma2 RS exE) 1),
- (etac subst 1),
- (rtac (dlist_finite_ind RS spec) 1),
- (REPEAT (resolve_tac prems 1)),
- (REPEAT (atac 1))
- ]);
-
-
-
-
--- a/src/HOLCF/explicit_domains/Dlist.thy Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,128 +0,0 @@
-(* Title: HOLCF/Dlist.thy
-
- Author: Franz Regensburger
- ID: $ $
- Copyright 1994 Technische Universitaet Muenchen
-
-NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dlist.thy INSTEAD.
-
-Theory for finite lists 'a dlist = one ++ ('a ** 'a dlist)
-
-The type is axiomatized as the least solution of the domain equation above.
-The functor term that specifies the domain equation is:
-
- FT = <++,K_{one},<**,K_{'a},I>>
-
-For details see chapter 5 of:
-
-[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
- Dissertation, Technische Universit"at M"unchen, 1994
-
-
-*)
-
-Dlist = Stream2 +
-
-types dlist 1
-
-(* ----------------------------------------------------------------------- *)
-(* arity axiom is validated by semantic reasoning *)
-(* partial ordering is implicit in the isomorphism axioms and their cont. *)
-
-arities dlist::(pcpo)pcpo
-
-consts
-
-(* ----------------------------------------------------------------------- *)
-(* essential constants *)
-
-dlist_rep :: "('a dlist) -> (one ++ 'a ** 'a dlist)"
-dlist_abs :: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
-
-(* ----------------------------------------------------------------------- *)
-(* abstract constants and auxiliary constants *)
-
-dlist_copy :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
-
-dnil :: "'a dlist"
-dcons :: "'a -> 'a dlist -> 'a dlist"
-dlist_when :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
-is_dnil :: "'a dlist -> tr"
-is_dcons :: "'a dlist -> tr"
-dhd :: "'a dlist -> 'a"
-dtl :: "'a dlist -> 'a dlist"
-dlist_take :: "nat => 'a dlist -> 'a dlist"
-dlist_finite :: "'a dlist => bool"
-dlist_bisim :: "('a dlist => 'a dlist => bool) => bool"
-
-rules
-
-(* ----------------------------------------------------------------------- *)
-(* axiomatization of recursive type 'a dlist *)
-(* ----------------------------------------------------------------------- *)
-(* ('a dlist,dlist_abs) is the initial F-algebra where *)
-(* F is the locally continuous functor determined by functor term FT. *)
-(* domain equation: 'a dlist = one ++ ('a ** 'a dlist) *)
-(* functor term: FT = <++,K_{one},<**,K_{'a},I>> *)
-(* ----------------------------------------------------------------------- *)
-(* dlist_abs is an isomorphism with inverse dlist_rep *)
-(* identity is the least endomorphism on 'a dlist *)
-
-dlist_abs_iso "dlist_rep`(dlist_abs`x) = x"
-dlist_rep_iso "dlist_abs`(dlist_rep`x) = x"
-dlist_copy_def "dlist_copy == (LAM f. dlist_abs oo \
-\ (sswhen`sinl`(sinr oo (ssplit`(LAM x y. (|x,f`y|) ))))\
-\ oo dlist_rep)"
-dlist_reach "(fix`dlist_copy)`x=x"
-
-
-defs
-(* ----------------------------------------------------------------------- *)
-(* properties of additional constants *)
-(* ----------------------------------------------------------------------- *)
-(* constructors *)
-
-dnil_def "dnil == dlist_abs`(sinl`one)"
-dcons_def "dcons == (LAM x l. dlist_abs`(sinr`(|x,l|) ))"
-
-(* ----------------------------------------------------------------------- *)
-(* discriminator functional *)
-
-dlist_when_def
-"dlist_when == (LAM f1 f2 l.\
-\ sswhen`(LAM x.f1) `(ssplit`(LAM x l.f2`x`l)) `(dlist_rep`l))"
-
-(* ----------------------------------------------------------------------- *)
-(* discriminators and selectors *)
-
-is_dnil_def "is_dnil == dlist_when`TT`(LAM x l.FF)"
-is_dcons_def "is_dcons == dlist_when`FF`(LAM x l.TT)"
-dhd_def "dhd == dlist_when`UU`(LAM x l.x)"
-dtl_def "dtl == dlist_when`UU`(LAM x l.l)"
-
-(* ----------------------------------------------------------------------- *)
-(* the taker for dlists *)
-
-dlist_take_def "dlist_take == (%n.iterate n dlist_copy UU)"
-
-(* ----------------------------------------------------------------------- *)
-
-dlist_finite_def "dlist_finite == (%s.? n.dlist_take n`s=s)"
-
-(* ----------------------------------------------------------------------- *)
-(* definition of bisimulation is determined by domain equation *)
-(* simplification and rewriting for abstract constants yields def below *)
-
-dlist_bisim_def "dlist_bisim ==
- ( %R.!l1 l2.
- R l1 l2 -->
- ((l1=UU & l2=UU) |
- (l1=dnil & l2=dnil) |
- (? x l11 l21. x~=UU & l11~=UU & l21~=UU &
- l1=dcons`x`l11 & l2 = dcons`x`l21 & R l11 l21)))"
-
-end
-
-
-
-
--- a/src/HOLCF/explicit_domains/Dnat.ML Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,534 +0,0 @@
-(* Title: HOLCF/Dnat.ML
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Lemmas for dnat.thy
-*)
-
-open Dnat;
-
-(* ------------------------------------------------------------------------*)
-(* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict *)
-(* ------------------------------------------------------------------------*)
-
-val dnat_iso_strict = dnat_rep_iso RS (dnat_abs_iso RS
- (allI RSN (2,allI RS iso_strict)));
-
-val dnat_rews = [dnat_iso_strict RS conjunct1,
- dnat_iso_strict RS conjunct2];
-
-(* ------------------------------------------------------------------------*)
-(* Properties of dnat_copy *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm = prove_goalw Dnat.thy defs thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac (!simpset addsimps
- (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
- ]);
-
-val dnat_copy =
- [
- prover [dnat_copy_def] "dnat_copy`f`UU=UU",
- prover [dnat_copy_def,dzero_def] "dnat_copy`f`dzero= dzero",
- prover [dnat_copy_def,dsucc_def]
- "n~=UU ==> dnat_copy`f`(dsucc`n) = dsucc`(f`n)"
- ];
-
-val dnat_rews = dnat_copy @ dnat_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Exhaustion and elimination for dnat *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "Exh_dnat" Dnat.thy [dsucc_def,dzero_def]
- "n = UU | n = dzero | (? x . x~=UU & n = dsucc`x)"
- (fn prems =>
- [
- (Simp_tac 1),
- (rtac (dnat_rep_iso RS subst) 1),
- (res_inst_tac [("p","dnat_rep`n")] ssumE 1),
- (rtac disjI1 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (rtac (disjI1 RS disjI2) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (res_inst_tac [("p","x")] oneE 1),
- (contr_tac 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (rtac (disjI2 RS disjI2) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (fast_tac HOL_cs 1)
- ]);
-
-qed_goal "dnatE" Dnat.thy
- "[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc`x;x~=UU|]==>Q|]==>Q"
- (fn prems =>
- [
- (rtac (Exh_dnat RS disjE) 1),
- (eresolve_tac prems 1),
- (etac disjE 1),
- (eresolve_tac prems 1),
- (REPEAT (etac exE 1)),
- (resolve_tac prems 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1)
- ]);
-
-(* ------------------------------------------------------------------------*)
-(* Properties of dnat_when *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm = prove_goalw Dnat.thy defs thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac (!simpset addsimps
- (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
- ]);
-
-
-val dnat_when = [
- prover [dnat_when_def] "dnat_when`c`f`UU=UU",
- prover [dnat_when_def,dzero_def] "dnat_when`c`f`dzero=c",
- prover [dnat_when_def,dsucc_def]
- "n~=UU ==> dnat_when`c`f`(dsucc`n)=f`n"
- ];
-
-val dnat_rews = dnat_when @ dnat_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Rewrites for discriminators and selectors *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm = prove_goalw Dnat.thy defs thm
- (fn prems =>
- [
- (simp_tac (!simpset addsimps dnat_rews) 1)
- ]);
-
-val dnat_discsel = [
- prover [is_dzero_def] "is_dzero`UU=UU",
- prover [is_dsucc_def] "is_dsucc`UU=UU",
- prover [dpred_def] "dpred`UU=UU"
- ];
-
-
-fun prover defs thm = prove_goalw Dnat.thy defs thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1)
- ]);
-
-val dnat_discsel = [
- prover [is_dzero_def] "is_dzero`dzero=TT",
- prover [is_dzero_def] "n~=UU ==>is_dzero`(dsucc`n)=FF",
- prover [is_dsucc_def] "is_dsucc`dzero=FF",
- prover [is_dsucc_def] "n~=UU ==> is_dsucc`(dsucc`n)=TT",
- prover [dpred_def] "dpred`dzero=UU",
- prover [dpred_def] "n~=UU ==> dpred`(dsucc`n)=n"
- ] @ dnat_discsel;
-
-val dnat_rews = dnat_discsel @ dnat_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Definedness and strictness *)
-(* ------------------------------------------------------------------------*)
-
-fun prover contr thm = prove_goal Dnat.thy thm
- (fn prems =>
- [
- (res_inst_tac [("P1",contr)] classical2 1),
- (simp_tac (!simpset addsimps dnat_rews) 1),
- (dtac sym 1),
- (Asm_simp_tac 1),
- (simp_tac (!simpset addsimps (prems @ dnat_rews)) 1)
- ]);
-
-val dnat_constrdef = [
- prover "is_dzero`UU ~= UU" "dzero~=UU",
- prover "is_dsucc`UU ~= UU" "n~=UU ==> dsucc`n~=UU"
- ];
-
-
-fun prover defs thm = prove_goalw Dnat.thy defs thm
- (fn prems =>
- [
- (simp_tac (!simpset addsimps dnat_rews) 1)
- ]);
-
-val dnat_constrdef = [
- prover [dsucc_def] "dsucc`UU=UU"
- ] @ dnat_constrdef;
-
-val dnat_rews = dnat_constrdef @ dnat_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* Distinctness wrt. << and = *)
-(* ------------------------------------------------------------------------*)
-
-val temp = prove_goal Dnat.thy "~dzero << dsucc`n"
- (fn prems =>
- [
- (res_inst_tac [("P1","TT << FF")] classical2 1),
- (resolve_tac dist_less_tr 1),
- (dres_inst_tac [("fo","is_dzero")] monofun_cfun_arg 1),
- (etac box_less 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (case_tac "n=UU" 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1)
- ]);
-
-val dnat_dist_less = [temp];
-
-val temp = prove_goal Dnat.thy "n~=UU ==> ~dsucc`n << dzero"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (res_inst_tac [("P1","TT << FF")] classical2 1),
- (resolve_tac dist_less_tr 1),
- (dres_inst_tac [("fo","is_dsucc")] monofun_cfun_arg 1),
- (etac box_less 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1)
- ]);
-
-val dnat_dist_less = temp::dnat_dist_less;
-
-val temp = prove_goal Dnat.thy "dzero ~= dsucc`n"
- (fn prems =>
- [
- (case_tac "n=UU" 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (res_inst_tac [("P1","TT = FF")] classical2 1),
- (resolve_tac dist_eq_tr 1),
- (dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
- (etac box_equals 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1)
- ]);
-
-val dnat_dist_eq = [temp, temp RS not_sym];
-
-val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Invertibility *)
-(* ------------------------------------------------------------------------*)
-
-val dnat_invert =
- [
-prove_goal Dnat.thy
-"[|x1~=UU; y1~=UU; dsucc`x1 << dsucc`y1 |] ==> x1<< y1"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (dres_inst_tac [("fo","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
- (etac box_less 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1)
- ])
- ];
-
-(* ------------------------------------------------------------------------*)
-(* Injectivity *)
-(* ------------------------------------------------------------------------*)
-
-val dnat_inject =
- [
-prove_goal Dnat.thy
-"[|x1~=UU; y1~=UU; dsucc`x1 = dsucc`y1 |] ==> x1= y1"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (dres_inst_tac [("f","dnat_when`c`(LAM x.x)")] cfun_arg_cong 1),
- (etac box_equals 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1)
- ])
- ];
-
-(* ------------------------------------------------------------------------*)
-(* definedness for discriminators and selectors *)
-(* ------------------------------------------------------------------------*)
-
-
-fun prover thm = prove_goal Dnat.thy thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac dnatE 1),
- (contr_tac 1),
- (REPEAT (asm_simp_tac (!simpset addsimps dnat_rews) 1))
- ]);
-
-val dnat_discsel_def =
- [
- prover "n~=UU ==> is_dzero`n ~= UU",
- prover "n~=UU ==> is_dsucc`n ~= UU"
- ];
-
-val dnat_rews = dnat_discsel_def @ dnat_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* Properties dnat_take *)
-(* ------------------------------------------------------------------------*)
-val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take n`UU = UU"
- (fn prems =>
- [
- (res_inst_tac [("n","n")] natE 1),
- (Asm_simp_tac 1),
- (Asm_simp_tac 1),
- (simp_tac (!simpset addsimps dnat_rews) 1)
- ]);
-
-val dnat_take = [temp];
-
-val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take 0`xs = UU"
- (fn prems =>
- [
- (Asm_simp_tac 1)
- ]);
-
-val dnat_take = temp::dnat_take;
-
-val temp = prove_goalw Dnat.thy [dnat_take_def]
- "dnat_take (Suc n)`dzero=dzero"
- (fn prems =>
- [
- (Asm_simp_tac 1),
- (simp_tac (!simpset addsimps dnat_rews) 1)
- ]);
-
-val dnat_take = temp::dnat_take;
-
-val temp = prove_goalw Dnat.thy [dnat_take_def]
- "dnat_take (Suc n)`(dsucc`xs)=dsucc`(dnat_take n ` xs)"
- (fn prems =>
- [
- (case_tac "xs=UU" 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (res_inst_tac [("n","n")] natE 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1)
- ]);
-
-val dnat_take = temp::dnat_take;
-
-val dnat_rews = dnat_take @ dnat_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* take lemma for dnats *)
-(* ------------------------------------------------------------------------*)
-
-fun prover reach defs thm = prove_goalw Dnat.thy defs thm
- (fn prems =>
- [
- (res_inst_tac [("t","s1")] (reach RS subst) 1),
- (res_inst_tac [("t","s2")] (reach RS subst) 1),
- (stac fix_def2 1),
- (stac contlub_cfun_fun 1),
- (rtac is_chain_iterate 1),
- (stac contlub_cfun_fun 1),
- (rtac is_chain_iterate 1),
- (rtac lub_equal 1),
- (rtac (is_chain_iterate RS ch2ch_fappL) 1),
- (rtac (is_chain_iterate RS ch2ch_fappL) 1),
- (rtac allI 1),
- (resolve_tac prems 1)
- ]);
-
-val dnat_take_lemma = prover dnat_reach [dnat_take_def]
- "(!!n.dnat_take n`s1 = dnat_take n`s2) ==> s1=s2";
-
-
-(* ------------------------------------------------------------------------*)
-(* Co -induction for dnats *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "dnat_coind_lemma" Dnat.thy [dnat_bisim_def]
-"dnat_bisim R ==> ! p q. R p q --> dnat_take n`p = dnat_take n`q"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps dnat_take) 1),
- (strip_tac 1),
- ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
- (atac 1),
- (asm_simp_tac (!simpset addsimps dnat_take) 1),
- (etac disjE 1),
- (asm_simp_tac (!simpset addsimps dnat_take) 1),
- (etac exE 1),
- (etac exE 1),
- (asm_simp_tac (!simpset addsimps dnat_take) 1),
- (REPEAT (etac conjE 1)),
- (rtac cfun_arg_cong 1),
- (fast_tac HOL_cs 1)
- ]);
-
-qed_goal "dnat_coind" Dnat.thy "[|dnat_bisim R;R p q|] ==> p = q"
- (fn prems =>
- [
- (rtac dnat_take_lemma 1),
- (rtac (dnat_coind_lemma RS spec RS spec RS mp) 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1)
- ]);
-
-
-(* ------------------------------------------------------------------------*)
-(* structural induction for admissible predicates *)
-(* ------------------------------------------------------------------------*)
-
-(* not needed any longer
-qed_goal "dnat_ind" Dnat.thy
-"[| adm(P);\
-\ P(UU);\
-\ P(dzero);\
-\ !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc`s1)|] ==> P(s)"
- (fn prems =>
- [
- (rtac (dnat_reach RS subst) 1),
- (res_inst_tac [("x","s")] spec 1),
- (rtac fix_ind 1),
- (rtac adm_all2 1),
- (rtac adm_subst 1),
- (cont_tacR 1),
- (resolve_tac prems 1),
- (Simp_tac 1),
- (resolve_tac prems 1),
- (strip_tac 1),
- (res_inst_tac [("n","xa")] dnatE 1),
- (asm_simp_tac (!simpset addsimps dnat_copy) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (!simpset addsimps dnat_copy) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (!simpset addsimps dnat_copy) 1),
- (case_tac "x`xb=UU" 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (resolve_tac prems 1),
- (eresolve_tac prems 1),
- (etac spec 1)
- ]);
-*)
-
-qed_goal "dnat_finite_ind" Dnat.thy
-"[|P(UU);P(dzero);\
-\ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\
-\ |] ==> !s.P(dnat_take n`s)"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps dnat_rews) 1),
- (resolve_tac prems 1),
- (rtac allI 1),
- (res_inst_tac [("n","s")] dnatE 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (case_tac "dnat_take n1`x=UU" 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1),
- (atac 1),
- (etac spec 1)
- ]);
-
-qed_goal "dnat_all_finite_lemma1" Dnat.thy
-"!s.dnat_take n`s=UU |dnat_take n`s=s"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps dnat_rews) 1),
- (rtac allI 1),
- (res_inst_tac [("n","s")] dnatE 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (eres_inst_tac [("x","x")] allE 1),
- (etac disjE 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1)
- ]);
-
-qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take n`s=s"
- (fn prems =>
- [
- (case_tac "s=UU" 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (subgoal_tac "(!n.dnat_take(n)`s=UU) |(? n.dnat_take(n)`s=s)" 1),
- (etac disjE 1),
- (eres_inst_tac [("P","s=UU")] notE 1),
- (rtac dnat_take_lemma 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (atac 1),
- (subgoal_tac "!n.!s.dnat_take(n)`s=UU |dnat_take(n)`s=s" 1),
- (fast_tac HOL_cs 1),
- (rtac allI 1),
- (rtac dnat_all_finite_lemma1 1)
- ]);
-
-
-qed_goal "dnat_ind" Dnat.thy
-"[|P(UU);P(dzero);\
-\ !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\
-\ |] ==> P(s)"
- (fn prems =>
- [
- (rtac (dnat_all_finite_lemma2 RS exE) 1),
- (etac subst 1),
- (rtac (dnat_finite_ind RS spec) 1),
- (REPEAT (resolve_tac prems 1)),
- (REPEAT (atac 1))
- ]);
-
-
-qed_goalw "dnat_flat" Dnat.thy [flat_def] "flat(dzero)"
- (fn prems =>
- [
- (rtac allI 1),
- (res_inst_tac [("s","x")] dnat_ind 1),
- (fast_tac HOL_cs 1),
- (rtac allI 1),
- (res_inst_tac [("n","y")] dnatE 1),
- (fast_tac (HOL_cs addSIs [UU_I]) 1),
- (Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
- (rtac allI 1),
- (res_inst_tac [("n","y")] dnatE 1),
- (fast_tac (HOL_cs addSIs [UU_I]) 1),
- (asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (strip_tac 1),
- (subgoal_tac "s1<<xa" 1),
- (etac allE 1),
- (dtac mp 1),
- (atac 1),
- (etac disjE 1),
- (contr_tac 1),
- (Asm_simp_tac 1),
- (resolve_tac dnat_invert 1),
- (REPEAT (atac 1))
- ]);
-
-
-
-
-
-
--- a/src/HOLCF/explicit_domains/Dnat.thy Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,112 +0,0 @@
-(* Title: HOLCF/Dnat.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD.
-
-Theory for the domain of natural numbers dnat = one ++ dnat
-
-The type is axiomatized as the least solution of the domain equation above.
-The functor term that specifies the domain equation is:
-
- FT = <++,K_{one},I>
-
-For details see chapter 5 of:
-
-[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
- Dissertation, Technische Universit"at M"unchen, 1994
-
-*)
-
-Dnat = HOLCF +
-
-types dnat 0
-
-(* ----------------------------------------------------------------------- *)
-(* arrity axiom is valuated by semantical reasoning *)
-
-arities dnat::pcpo
-
-consts
-
-(* ----------------------------------------------------------------------- *)
-(* essential constants *)
-
-dnat_rep :: " dnat -> (one ++ dnat)"
-dnat_abs :: "(one ++ dnat) -> dnat"
-
-(* ----------------------------------------------------------------------- *)
-(* abstract constants and auxiliary constants *)
-
-dnat_copy :: "(dnat -> dnat) -> dnat -> dnat"
-
-dzero :: "dnat"
-dsucc :: "dnat -> dnat"
-dnat_when :: "'b -> (dnat -> 'b) -> dnat -> 'b"
-is_dzero :: "dnat -> tr"
-is_dsucc :: "dnat -> tr"
-dpred :: "dnat -> dnat"
-dnat_take :: "nat => dnat -> dnat"
-dnat_bisim :: "(dnat => dnat => bool) => bool"
-
-rules
-
-(* ----------------------------------------------------------------------- *)
-(* axiomatization of recursive type dnat *)
-(* ----------------------------------------------------------------------- *)
-(* (dnat,dnat_abs) is the initial F-algebra where *)
-(* F is the locally continuous functor determined by functor term FT. *)
-(* domain equation: dnat = one ++ dnat *)
-(* functor term: FT = <++,K_{one},I> *)
-(* ----------------------------------------------------------------------- *)
-(* dnat_abs is an isomorphism with inverse dnat_rep *)
-(* identity is the least endomorphism on dnat *)
-
-dnat_abs_iso "dnat_rep`(dnat_abs`x) = x"
-dnat_rep_iso "dnat_abs`(dnat_rep`x) = x"
-dnat_copy_def "dnat_copy == (LAM f. dnat_abs oo
- (sswhen`sinl`(sinr oo f)) oo dnat_rep )"
-dnat_reach "(fix`dnat_copy)`x=x"
-
-
-defs
-(* ----------------------------------------------------------------------- *)
-(* properties of additional constants *)
-(* ----------------------------------------------------------------------- *)
-(* constructors *)
-
-dzero_def "dzero == dnat_abs`(sinl`one)"
-dsucc_def "dsucc == (LAM n. dnat_abs`(sinr`n))"
-
-(* ----------------------------------------------------------------------- *)
-(* discriminator functional *)
-
-dnat_when_def "dnat_when == (LAM f1 f2 n.sswhen`(LAM x.f1)`f2`(dnat_rep`n))"
-
-
-(* ----------------------------------------------------------------------- *)
-(* discriminators and selectors *)
-
-is_dzero_def "is_dzero == dnat_when`TT`(LAM x.FF)"
-is_dsucc_def "is_dsucc == dnat_when`FF`(LAM x.TT)"
-dpred_def "dpred == dnat_when`UU`(LAM x.x)"
-
-
-(* ----------------------------------------------------------------------- *)
-(* the taker for dnats *)
-
-dnat_take_def "dnat_take == (%n.iterate n dnat_copy UU)"
-
-(* ----------------------------------------------------------------------- *)
-(* definition of bisimulation is determined by domain equation *)
-(* simplification and rewriting for abstract constants yields def below *)
-
-dnat_bisim_def "dnat_bisim ==
-(%R.!s1 s2.
- R s1 s2 -->
- ((s1=UU & s2=UU) |(s1=dzero & s2=dzero) |
- (? s11 s21. s11~=UU & s21~=UU & s1=dsucc`s11 &
- s2 = dsucc`s21 & R s11 s21)))"
-
-end
--- a/src/HOLCF/explicit_domains/Dnat2.ML Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-(* Title: HOLCF/Dnat2.ML
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Lemmas for theory Dnat2.thy
-*)
-
-open Dnat2;
-
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties *)
-(* ------------------------------------------------------------------------- *)
-
-val iterator_def2 = fix_prover2 Dnat2.thy iterator_def
- "iterator = (LAM n f x. dnat_when`x`(LAM m.f`(iterator`m`f`x)) `n)";
-
-(* ------------------------------------------------------------------------- *)
-(* recursive properties *)
-(* ------------------------------------------------------------------------- *)
-
-qed_goal "iterator1" Dnat2.thy "iterator`UU`f`x = UU"
- (fn prems =>
- [
- (stac iterator_def2 1),
- (simp_tac (!simpset addsimps dnat_when) 1)
- ]);
-
-qed_goal "iterator2" Dnat2.thy "iterator`dzero`f`x = x"
- (fn prems =>
- [
- (stac iterator_def2 1),
- (simp_tac (!simpset addsimps dnat_when) 1)
- ]);
-
-qed_goal "iterator3" Dnat2.thy
-"n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac trans 1),
- (stac iterator_def2 1),
- (asm_simp_tac (!simpset addsimps dnat_rews) 1),
- (rtac refl 1)
- ]);
-
-val dnat2_rews =
- [iterator1, iterator2, iterator3];
-
-
-
--- a/src/HOLCF/explicit_domains/Dnat2.thy Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(* Title: HOLCF/Dnat2.thy
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD.
-
-Additional constants for dnat
-
-*)
-
-Dnat2 = Dnat +
-
-consts
-
-iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
-
-
-defs
-
-iterator_def "iterator == fix`(LAM h n f x.
- dnat_when `x `(LAM m.f`(h`m`f`x)) `n)"
-end
-
-(*
-
- iterator`UU`f`x = UU
- iterator`dzero`f`x = x
- n~=UU --> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)
-*)
-
--- a/src/HOLCF/explicit_domains/README Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(*
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1995 Technische Universitaet Muenchen
-
-*)
-
-The files contained in this directory are examples for the
-explicit construction of domains. The technique used is described
-in the thesis
-
- HOLCF: Eine konservative Erweiterung von HOL um LCF
-
-The thesis is available via the web using URL
-
- http://www4.informatik.tu-muenchen.de/~regensbu/papers.html
-
-
-The same construction is automatically performed if you use the
-type definition package of David Oheimb. See subdirectory HOLCF/domains
-for more details.
-
--- a/src/HOLCF/explicit_domains/ROOT.ML Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1995 Technische Universitaet Muenchen
-
-*)
-
-HOLCF_build_completed; (*Cause examples to fail if HOLCF did*)
-
-writeln"Root file for HOLCF examples: explicit domain axiomatisation";
-proof_timing := true;
-
-time_use_thy "Dnat";
-time_use_thy "Dnat2";
-time_use_thy "Stream";
-time_use_thy "Stream2";
-time_use_thy "Dlist";
-
-OS.FileSys.chDir "..";
-maketest "END: Root file for HOLCF examples: explicit domain axiomatization";
--- a/src/HOLCF/explicit_domains/Stream.ML Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,838 +0,0 @@
-(*
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Lemmas for stream.thy
-*)
-
-open Stream;
-
-(* ------------------------------------------------------------------------*)
-(* The isomorphisms stream_rep_iso and stream_abs_iso are strict *)
-(* ------------------------------------------------------------------------*)
-
-val stream_iso_strict= stream_rep_iso RS (stream_abs_iso RS
- (allI RSN (2,allI RS iso_strict)));
-
-val stream_rews = [stream_iso_strict RS conjunct1,
- stream_iso_strict RS conjunct2];
-
-(* ------------------------------------------------------------------------*)
-(* Properties of stream_copy *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm = prove_goalw Stream.thy defs thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac (!simpset addsimps
- (stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
- ]);
-
-val stream_copy =
- [
- prover [stream_copy_def] "stream_copy`f`UU=UU",
- prover [stream_copy_def,scons_def]
- "x~=UU ==> stream_copy`f`(scons`x`xs)= scons`x`(f`xs)"
- ];
-
-val stream_rews = stream_copy @ stream_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Exhaustion and elimination for streams *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "Exh_stream" Stream.thy [scons_def]
- "s = UU | (? x xs. x~=UU & s = scons`x`xs)"
- (fn prems =>
- [
- (Simp_tac 1),
- (rtac (stream_rep_iso RS subst) 1),
- (res_inst_tac [("p","stream_rep`s")] sprodE 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (Asm_simp_tac 1),
- (res_inst_tac [("p","y")] upE1 1),
- (contr_tac 1),
- (rtac disjI2 1),
- (rtac exI 1),
- (etac conjI 1),
- (rtac exI 1),
- (Asm_simp_tac 1)
- ]);
-
-qed_goal "streamE" Stream.thy
- "[| s=UU ==> Q; !!x xs.[|s=scons`x`xs;x~=UU|]==>Q|]==>Q"
- (fn prems =>
- [
- (rtac (Exh_stream RS disjE) 1),
- (eresolve_tac prems 1),
- (etac exE 1),
- (etac exE 1),
- (resolve_tac prems 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1)
- ]);
-
-(* ------------------------------------------------------------------------*)
-(* Properties of stream_when *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm = prove_goalw Stream.thy defs thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac (!simpset addsimps
- (stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
- ]);
-
-
-val stream_when = [
- prover [stream_when_def] "stream_when`f`UU=UU",
- prover [stream_when_def,scons_def]
- "x~=UU ==> stream_when`f`(scons`x`xs)= f`x`xs"
- ];
-
-val stream_rews = stream_when @ stream_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Rewrites for discriminators and selectors *)
-(* ------------------------------------------------------------------------*)
-
-fun prover defs thm = prove_goalw Stream.thy defs thm
- (fn prems =>
- [
- (simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-val stream_discsel = [
- prover [is_scons_def] "is_scons`UU=UU",
- prover [shd_def] "shd`UU=UU",
- prover [stl_def] "stl`UU=UU"
- ];
-
-fun prover defs thm = prove_goalw Stream.thy defs thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-val stream_discsel = [
-prover [is_scons_def,shd_def,stl_def] "x~=UU ==> is_scons`(scons`x`xs)=TT",
-prover [is_scons_def,shd_def,stl_def] "x~=UU ==> shd`(scons`x`xs)=x",
-prover [is_scons_def,shd_def,stl_def] "x~=UU ==> stl`(scons`x`xs)=xs"
- ] @ stream_discsel;
-
-val stream_rews = stream_discsel @ stream_rews;
-
-(* ------------------------------------------------------------------------*)
-(* Definedness and strictness *)
-(* ------------------------------------------------------------------------*)
-
-fun prover contr thm = prove_goal Stream.thy thm
- (fn prems =>
- [
- (res_inst_tac [("P1",contr)] classical2 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
- (dtac sym 1),
- (Asm_simp_tac 1),
- (simp_tac (!simpset addsimps (prems @ stream_rews)) 1)
- ]);
-
-val stream_constrdef = [
- prover "is_scons`(UU::'a stream)~=UU" "x~=UU ==> scons`(x::'a)`xs~=UU"
- ];
-
-fun prover defs thm = prove_goalw Stream.thy defs thm
- (fn prems =>
- [
- (simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-val stream_constrdef = [
- prover [scons_def] "scons`UU`xs=UU"
- ] @ stream_constrdef;
-
-val stream_rews = stream_constrdef @ stream_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* Distinctness wrt. << and = *)
-(* ------------------------------------------------------------------------*)
-
-
-(* ------------------------------------------------------------------------*)
-(* Invertibility *)
-(* ------------------------------------------------------------------------*)
-
-val stream_invert =
- [
-prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
-\ scons`x1`x2 << scons`y1`y2|] ==> x1<< y1 & x2 << y2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac conjI 1),
- (dres_inst_tac [("fo","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
- (etac box_less 1),
- (asm_simp_tac (!simpset addsimps stream_when) 1),
- (asm_simp_tac (!simpset addsimps stream_when) 1),
- (dres_inst_tac [("fo","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
- (etac box_less 1),
- (asm_simp_tac (!simpset addsimps stream_when) 1),
- (asm_simp_tac (!simpset addsimps stream_when) 1)
- ])
- ];
-
-(* ------------------------------------------------------------------------*)
-(* Injectivity *)
-(* ------------------------------------------------------------------------*)
-
-val stream_inject =
- [
-prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
-\ scons`x1`x2 = scons`y1`y2 |] ==> x1= y1 & x2 = y2"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac conjI 1),
- (dres_inst_tac [("f","stream_when`(LAM x l.x)")] cfun_arg_cong 1),
- (etac box_equals 1),
- (asm_simp_tac (!simpset addsimps stream_when) 1),
- (asm_simp_tac (!simpset addsimps stream_when) 1),
- (dres_inst_tac [("f","stream_when`(LAM x l.l)")] cfun_arg_cong 1),
- (etac box_equals 1),
- (asm_simp_tac (!simpset addsimps stream_when) 1),
- (asm_simp_tac (!simpset addsimps stream_when) 1)
- ])
- ];
-
-(* ------------------------------------------------------------------------*)
-(* definedness for discriminators and selectors *)
-(* ------------------------------------------------------------------------*)
-
-fun prover thm = prove_goal Stream.thy thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac streamE 1),
- (contr_tac 1),
- (REPEAT (asm_simp_tac (!simpset addsimps stream_discsel) 1))
- ]);
-
-val stream_discsel_def =
- [
- prover "s~=UU ==> is_scons`s ~= UU",
- prover "s~=UU ==> shd`s ~=UU"
- ];
-
-val stream_rews = stream_discsel_def @ stream_rews;
-
-
-(* ------------------------------------------------------------------------*)
-(* Properties stream_take *)
-(* ------------------------------------------------------------------------*)
-
-val stream_take =
- [
-prove_goalw Stream.thy [stream_take_def] "stream_take n`UU = UU"
- (fn prems =>
- [
- (res_inst_tac [("n","n")] natE 1),
- (Asm_simp_tac 1),
- (Asm_simp_tac 1),
- (simp_tac (!simpset addsimps stream_rews) 1)
- ]),
-prove_goalw Stream.thy [stream_take_def] "stream_take 0`xs=UU"
- (fn prems =>
- [
- (Asm_simp_tac 1)
- ])];
-
-fun prover thm = prove_goalw Stream.thy [stream_take_def] thm
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (Simp_tac 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-val stream_take = [
-prover
- "x~=UU ==> stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
- ] @ stream_take;
-
-val stream_rews = stream_take @ stream_rews;
-
-(* ------------------------------------------------------------------------*)
-(* enhance the simplifier *)
-(* ------------------------------------------------------------------------*)
-
-qed_goal "stream_copy2" Stream.thy
- "stream_copy`f`(scons`x`xs) = scons`x`(f`xs)"
- (fn prems =>
- [
- (case_tac "x=UU" 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-qed_goal "shd2" Stream.thy "shd`(scons`x`xs) = x"
- (fn prems =>
- [
- (case_tac "x=UU" 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-qed_goal "stream_take2" Stream.thy
- "stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
- (fn prems =>
- [
- (case_tac "x=UU" 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-val stream_rews = [stream_iso_strict RS conjunct1,
- stream_iso_strict RS conjunct2,
- hd stream_copy, stream_copy2]
- @ stream_when
- @ [hd stream_discsel,shd2] @ (tl (tl stream_discsel))
- @ stream_constrdef
- @ stream_discsel_def
- @ [ stream_take2] @ (tl stream_take);
-
-
-(* ------------------------------------------------------------------------*)
-(* take lemma for streams *)
-(* ------------------------------------------------------------------------*)
-
-fun prover reach defs thm = prove_goalw Stream.thy defs thm
- (fn prems =>
- [
- (res_inst_tac [("t","s1")] (reach RS subst) 1),
- (res_inst_tac [("t","s2")] (reach RS subst) 1),
- (stac fix_def2 1),
- (stac contlub_cfun_fun 1),
- (rtac is_chain_iterate 1),
- (stac contlub_cfun_fun 1),
- (rtac is_chain_iterate 1),
- (rtac lub_equal 1),
- (rtac (is_chain_iterate RS ch2ch_fappL) 1),
- (rtac (is_chain_iterate RS ch2ch_fappL) 1),
- (rtac allI 1),
- (resolve_tac prems 1)
- ]);
-
-val stream_take_lemma = prover stream_reach [stream_take_def]
- "(!!n.stream_take n`s1 = stream_take n`s2) ==> s1=s2";
-
-
-qed_goal "stream_reach2" Stream.thy "lub(range(%i.stream_take i`s))=s"
- (fn prems =>
- [
- (res_inst_tac [("t","s")] (stream_reach RS subst) 1),
- (stac fix_def2 1),
- (rewtac stream_take_def),
- (stac contlub_cfun_fun 1),
- (rtac is_chain_iterate 1),
- (rtac refl 1)
- ]);
-
-(* ------------------------------------------------------------------------*)
-(* Co -induction for streams *)
-(* ------------------------------------------------------------------------*)
-
-qed_goalw "stream_coind_lemma" Stream.thy [stream_bisim_def]
-"stream_bisim R ==> ! p q. R p q --> stream_take n`p = stream_take n`q"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
- (strip_tac 1),
- ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
- (atac 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (etac exE 1),
- (etac exE 1),
- (etac exE 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (REPEAT (etac conjE 1)),
- (rtac cfun_arg_cong 1),
- (fast_tac HOL_cs 1)
- ]);
-
-qed_goal "stream_coind" Stream.thy "[|stream_bisim R ;R p q|] ==> p = q"
- (fn prems =>
- [
- (rtac stream_take_lemma 1),
- (rtac (stream_coind_lemma RS spec RS spec RS mp) 1),
- (resolve_tac prems 1),
- (resolve_tac prems 1)
- ]);
-
-(* ------------------------------------------------------------------------*)
-(* structural induction for admissible predicates *)
-(* ------------------------------------------------------------------------*)
-
-qed_goal "stream_finite_ind" Stream.thy
-"[|P(UU);\
-\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
-\ |] ==> !s.P(stream_take n`s)"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
- (resolve_tac prems 1),
- (rtac allI 1),
- (res_inst_tac [("s","s")] streamE 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (resolve_tac prems 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (resolve_tac prems 1),
- (atac 1),
- (etac spec 1)
- ]);
-
-qed_goalw "stream_finite_ind2" Stream.thy [stream_finite_def]
-"(!!n.P(stream_take n`s)) ==> stream_finite(s) -->P(s)"
- (fn prems =>
- [
- (strip_tac 1),
- (etac exE 1),
- (etac subst 1),
- (resolve_tac prems 1)
- ]);
-
-qed_goal "stream_finite_ind3" Stream.thy
-"[|P(UU);\
-\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
-\ |] ==> stream_finite(s) --> P(s)"
- (fn prems =>
- [
- (rtac stream_finite_ind2 1),
- (rtac (stream_finite_ind RS spec) 1),
- (REPEAT (resolve_tac prems 1)),
- (REPEAT (atac 1))
- ]);
-
-(* prove induction using definition of admissibility
- stream_reach rsp. stream_reach2
- and finite induction stream_finite_ind *)
-
-qed_goal "stream_ind" Stream.thy
-"[|adm(P);\
-\ P(UU);\
-\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
-\ |] ==> P(s)"
- (fn prems =>
- [
- (rtac (stream_reach2 RS subst) 1),
- (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
- (resolve_tac prems 1),
- (SELECT_GOAL (rewtac stream_take_def) 1),
- (rtac ch2ch_fappL 1),
- (rtac is_chain_iterate 1),
- (rtac allI 1),
- (rtac (stream_finite_ind RS spec) 1),
- (REPEAT (resolve_tac prems 1)),
- (REPEAT (atac 1))
- ]);
-
-(* prove induction with usual LCF-Method using fixed point induction *)
-qed_goal "stream_ind" Stream.thy
-"[|adm(P);\
-\ P(UU);\
-\ !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
-\ |] ==> P(s)"
- (fn prems =>
- [
- (rtac (stream_reach RS subst) 1),
- (res_inst_tac [("x","s")] spec 1),
- (rtac wfix_ind 1),
- (rtac adm_impl_admw 1),
- (REPEAT (resolve_tac adm_thms 1)),
- (rtac adm_subst 1),
- (cont_tacR 1),
- (resolve_tac prems 1),
- (rtac allI 1),
- (rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
- (REPEAT (resolve_tac prems 1)),
- (REPEAT (atac 1))
- ]);
-
-
-(* ------------------------------------------------------------------------*)
-(* simplify use of Co-induction *)
-(* ------------------------------------------------------------------------*)
-
-qed_goal "surjectiv_scons" Stream.thy "scons`(shd`s)`(stl`s)=s"
- (fn prems =>
- [
- (res_inst_tac [("s","s")] streamE 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-
-qed_goalw "stream_coind_lemma2" Stream.thy [stream_bisim_def]
-"!s1 s2. R s1 s2 --> shd`s1 = shd`s2 & R (stl`s1) (stl`s2) ==> stream_bisim R"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (strip_tac 1),
- (etac allE 1),
- (etac allE 1),
- (dtac mp 1),
- (atac 1),
- (etac conjE 1),
- (case_tac "s1 = UU & s2 = UU" 1),
- (rtac disjI1 1),
- (fast_tac HOL_cs 1),
- (rtac disjI2 1),
- (rtac disjE 1),
- (etac (de_Morgan_conj RS subst) 1),
- (res_inst_tac [("x","shd`s1")] exI 1),
- (res_inst_tac [("x","stl`s1")] exI 1),
- (res_inst_tac [("x","stl`s2")] exI 1),
- (rtac conjI 1),
- (eresolve_tac stream_discsel_def 1),
- (asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
- (eres_inst_tac [("s","shd`s1"),("t","shd`s2")] subst 1),
- (simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
- (res_inst_tac [("x","shd`s2")] exI 1),
- (res_inst_tac [("x","stl`s1")] exI 1),
- (res_inst_tac [("x","stl`s2")] exI 1),
- (rtac conjI 1),
- (eresolve_tac stream_discsel_def 1),
- (asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
- (res_inst_tac [("s","shd`s1"),("t","shd`s2")] ssubst 1),
- (etac sym 1),
- (simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1)
- ]);
-
-
-(* ------------------------------------------------------------------------*)
-(* theorems about finite and infinite streams *)
-(* ------------------------------------------------------------------------*)
-
-(* ----------------------------------------------------------------------- *)
-(* 2 lemmas about stream_finite *)
-(* ----------------------------------------------------------------------- *)
-
-qed_goalw "stream_finite_UU" Stream.thy [stream_finite_def]
- "stream_finite(UU)"
- (fn prems =>
- [
- (rtac exI 1),
- (simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-qed_goal "inf_stream_not_UU" Stream.thy "~stream_finite(s) ==> s ~= UU"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac swap 1),
- (dtac notnotD 1),
- (hyp_subst_tac 1),
- (rtac stream_finite_UU 1)
- ]);
-
-(* ----------------------------------------------------------------------- *)
-(* a lemma about shd *)
-(* ----------------------------------------------------------------------- *)
-
-qed_goal "stream_shd_lemma1" Stream.thy "shd`s=UU --> s=UU"
- (fn prems =>
- [
- (res_inst_tac [("s","s")] streamE 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (hyp_subst_tac 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-
-(* ----------------------------------------------------------------------- *)
-(* lemmas about stream_take *)
-(* ----------------------------------------------------------------------- *)
-
-qed_goal "stream_take_lemma1" Stream.thy
- "!x xs.x~=UU --> \
-\ stream_take (Suc n)`(scons`x`xs) = scons`x`xs --> stream_take n`xs=xs"
- (fn prems =>
- [
- (rtac allI 1),
- (rtac allI 1),
- (rtac impI 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (strip_tac 1),
- (rtac ((hd stream_inject) RS conjunct2) 1),
- (atac 1),
- (atac 1),
- (atac 1)
- ]);
-
-
-qed_goal "stream_take_lemma2" Stream.thy
- "! s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
- (strip_tac 1),
- (res_inst_tac [("s","s2")] streamE 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (hyp_subst_tac 1),
- (rotate_tac ~1 1),
- (asm_full_simp_tac (!simpset addsimps stream_rews) 1),
- (subgoal_tac "stream_take n1`xs = xs" 1),
- (rtac ((hd stream_inject) RS conjunct2) 2),
- (atac 4),
- (atac 2),
- (atac 2),
- (rtac cfun_arg_cong 1),
- (fast_tac HOL_cs 1)
- ]);
-
-qed_goal "stream_take_lemma3" Stream.thy
- "!x xs.x~=UU --> \
-\ stream_take n`(scons`x`xs) = scons`x`xs --> stream_take n`xs=xs"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (strip_tac 1 ),
- (res_inst_tac [("P","scons`x`xs=UU")] notE 1),
- (eresolve_tac stream_constrdef 1),
- (etac sym 1),
- (strip_tac 1 ),
- (rtac (stream_take_lemma2 RS spec RS mp) 1),
- (res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
- (atac 1),
- (atac 1),
- (etac (stream_take2 RS subst) 1)
- ]);
-
-qed_goal "stream_take_lemma4" Stream.thy
- "!x xs.\
-\stream_take n`xs=xs --> stream_take (Suc n)`(scons`x`xs) = scons`x`xs"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
- (simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-(* ---- *)
-
-qed_goal "stream_take_lemma5" Stream.thy
-"!s. stream_take n`s=s --> iterate n stl s=UU"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (Simp_tac 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
- (strip_tac 1),
- (res_inst_tac [("s","s")] streamE 1),
- (hyp_subst_tac 1),
- (stac iterate_Suc2 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (stac iterate_Suc2 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (etac allE 1),
- (etac mp 1),
- (hyp_subst_tac 1),
- (etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
- (atac 1)
- ]);
-
-qed_goal "stream_take_lemma6" Stream.thy
-"!s.iterate n stl s =UU --> stream_take n`s=s"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (Simp_tac 1),
- (strip_tac 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (rtac allI 1),
- (res_inst_tac [("s","s")] streamE 1),
- (hyp_subst_tac 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (hyp_subst_tac 1),
- (stac iterate_Suc2 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1)
- ]);
-
-qed_goal "stream_take_lemma7" Stream.thy
-"(iterate n stl s=UU) = (stream_take n`s=s)"
- (fn prems =>
- [
- (rtac iffI 1),
- (etac (stream_take_lemma6 RS spec RS mp) 1),
- (etac (stream_take_lemma5 RS spec RS mp) 1)
- ]);
-
-
-qed_goal "stream_take_lemma8" Stream.thy
-"[|adm(P); !n. ? m. n < m & P (stream_take m`s)|] ==> P(s)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac (stream_reach2 RS subst) 1),
- (rtac adm_lemma11 1),
- (atac 1),
- (atac 2),
- (rewtac stream_take_def),
- (rtac ch2ch_fappL 1),
- (rtac is_chain_iterate 1)
- ]);
-
-(* ----------------------------------------------------------------------- *)
-(* lemmas stream_finite *)
-(* ----------------------------------------------------------------------- *)
-
-qed_goalw "stream_finite_lemma1" Stream.thy [stream_finite_def]
- "stream_finite(xs) ==> stream_finite(scons`x`xs)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac exE 1),
- (rtac exI 1),
- (etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
- ]);
-
-qed_goalw "stream_finite_lemma2" Stream.thy [stream_finite_def]
- "[|x~=UU; stream_finite(scons`x`xs)|] ==> stream_finite(xs)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac exE 1),
- (rtac exI 1),
- (etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
- (atac 1)
- ]);
-
-qed_goal "stream_finite_lemma3" Stream.thy
- "x~=UU ==> stream_finite(scons`x`xs) = stream_finite(xs)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac iffI 1),
- (etac stream_finite_lemma2 1),
- (atac 1),
- (etac stream_finite_lemma1 1)
- ]);
-
-
-qed_goalw "stream_finite_lemma5" Stream.thy [stream_finite_def]
- "(!n. s1 << s2 --> stream_take n`s2 = s2 --> stream_finite(s1))\
-\=(s1 << s2 --> stream_finite(s2) --> stream_finite(s1))"
- (fn prems =>
- [
- (rtac iffI 1),
- (fast_tac HOL_cs 1),
- (fast_tac HOL_cs 1)
- ]);
-
-qed_goal "stream_finite_lemma6" Stream.thy
- "!s1 s2. s1 << s2 --> stream_take n`s2 = s2 --> stream_finite(s1)"
- (fn prems =>
- [
- (nat_ind_tac "n" 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
- (strip_tac 1 ),
- (hyp_subst_tac 1),
- (dtac UU_I 1),
- (hyp_subst_tac 1),
- (rtac stream_finite_UU 1),
- (rtac allI 1),
- (rtac allI 1),
- (res_inst_tac [("s","s1")] streamE 1),
- (hyp_subst_tac 1),
- (strip_tac 1 ),
- (rtac stream_finite_UU 1),
- (hyp_subst_tac 1),
- (res_inst_tac [("s","s2")] streamE 1),
- (hyp_subst_tac 1),
- (strip_tac 1 ),
- (dtac UU_I 1),
- (asm_simp_tac(!simpset addsimps (stream_rews @ [stream_finite_UU])) 1),
- (hyp_subst_tac 1),
- (simp_tac (!simpset addsimps stream_rews) 1),
- (strip_tac 1 ),
- (rtac stream_finite_lemma1 1),
- (subgoal_tac "xs << xsa" 1),
- (subgoal_tac "stream_take n1`xsa = xsa" 1),
- (fast_tac HOL_cs 1),
- (res_inst_tac [("x1.1","xa"),("y1.1","xa")]
- ((hd stream_inject) RS conjunct2) 1),
- (atac 1),
- (atac 1),
- (atac 1),
- (res_inst_tac [("x1.1","x"),("y1.1","xa")]
- ((hd stream_invert) RS conjunct2) 1),
- (atac 1),
- (atac 1),
- (atac 1)
- ]);
-
-qed_goal "stream_finite_lemma7" Stream.thy
-"s1 << s2 --> stream_finite(s2) --> stream_finite(s1)"
- (fn prems =>
- [
- (rtac (stream_finite_lemma5 RS iffD1) 1),
- (rtac allI 1),
- (rtac (stream_finite_lemma6 RS spec RS spec) 1)
- ]);
-
-qed_goalw "stream_finite_lemma8" Stream.thy [stream_finite_def]
-"stream_finite(s) = (? n. iterate n stl s = UU)"
- (fn prems =>
- [
- (simp_tac (!simpset addsimps [stream_take_lemma7]) 1)
- ]);
-
-
-(* ----------------------------------------------------------------------- *)
-(* admissibility of ~stream_finite *)
-(* ----------------------------------------------------------------------- *)
-
-qed_goalw "adm_not_stream_finite" Stream.thy [adm_def]
- "adm(%s. ~ stream_finite(s))"
- (fn prems =>
- [
- (strip_tac 1 ),
- (res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical2 1),
- (atac 2),
- (subgoal_tac "!i.stream_finite(Y(i))" 1),
- (fast_tac HOL_cs 1),
- (rtac allI 1),
- (rtac (stream_finite_lemma7 RS mp RS mp) 1),
- (etac is_ub_thelub 1),
- (atac 1)
- ]);
-
-(* ----------------------------------------------------------------------- *)
-(* alternative prove for admissibility of ~stream_finite *)
-(* show that stream_finite(s) = (? n. iterate n stl s = UU) *)
-(* and prove adm. of ~(? n. iterate n stl s = UU) *)
-(* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8 *)
-(* ----------------------------------------------------------------------- *)
-
-
-qed_goal "adm_not_stream_finite" Stream.thy "adm(%s. ~ stream_finite(s))"
- (fn prems =>
- [
- (subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate n stl s ~=UU))" 1),
- (etac (adm_cong RS iffD2)1),
- (REPEAT(resolve_tac adm_thms 1)),
- (rtac cont_iterate2 1),
- (rtac allI 1),
- (stac stream_finite_lemma8 1),
- (fast_tac HOL_cs 1)
- ]);
-
-
--- a/src/HOLCF/explicit_domains/Stream.thy Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-(*
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD.
-
-Theory for streams without defined empty stream
- 'a stream = 'a ** ('a stream)u
-
-The type is axiomatized as the least solution of the domain equation above.
-The functor term that specifies the domain equation is:
-
- FT = <**,K_{'a},U>
-
-For details see chapter 5 of:
-
-[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
- Dissertation, Technische Universit"at M"unchen, 1994
-*)
-
-Stream = Dnat2 +
-
-types stream 1
-
-(* ----------------------------------------------------------------------- *)
-(* arity axiom is validated by semantic reasoning *)
-(* partial ordering is implicit in the isomorphism axioms and their cont. *)
-
-arities stream::(pcpo)pcpo
-
-consts
-
-(* ----------------------------------------------------------------------- *)
-(* essential constants *)
-
-stream_rep :: "('a stream) -> ('a ** ('a stream)u)"
-stream_abs :: "('a ** ('a stream)u) -> ('a stream)"
-
-(* ----------------------------------------------------------------------- *)
-(* abstract constants and auxiliary constants *)
-
-stream_copy :: "('a stream -> 'a stream) ->'a stream -> 'a stream"
-
-scons :: "'a -> 'a stream -> 'a stream"
-stream_when :: "('a -> 'a stream -> 'b) -> 'a stream -> 'b"
-is_scons :: "'a stream -> tr"
-shd :: "'a stream -> 'a"
-stl :: "'a stream -> 'a stream"
-stream_take :: "nat => 'a stream -> 'a stream"
-stream_finite :: "'a stream => bool"
-stream_bisim :: "('a stream => 'a stream => bool) => bool"
-
-rules
-
-(* ----------------------------------------------------------------------- *)
-(* axiomatization of recursive type 'a stream *)
-(* ----------------------------------------------------------------------- *)
-(* ('a stream,stream_abs) is the initial F-algebra where *)
-(* F is the locally continuous functor determined by functor term FT. *)
-(* domain equation: 'a stream = 'a ** ('a stream)u *)
-(* functor term: FT = <**,K_{'a},U> *)
-(* ----------------------------------------------------------------------- *)
-(* stream_abs is an isomorphism with inverse stream_rep *)
-(* identity is the least endomorphism on 'a stream *)
-
-stream_abs_iso "stream_rep`(stream_abs`x) = x"
-stream_rep_iso "stream_abs`(stream_rep`x) = x"
-stream_copy_def "stream_copy == (LAM f. stream_abs oo
- (ssplit`(LAM x y. (|x , (fup`(up oo f))`y|) )) oo stream_rep)"
-stream_reach "(fix`stream_copy)`x = x"
-
-defs
-(* ----------------------------------------------------------------------- *)
-(* properties of additional constants *)
-(* ----------------------------------------------------------------------- *)
-(* constructors *)
-
-scons_def "scons == (LAM x l. stream_abs`(| x, up`l |))"
-
-(* ----------------------------------------------------------------------- *)
-(* discriminator functional *)
-
-stream_when_def
-"stream_when == (LAM f l.ssplit `(LAM x l.f`x`(fup`ID`l)) `(stream_rep`l))"
-
-(* ----------------------------------------------------------------------- *)
-(* discriminators and selectors *)
-
-is_scons_def "is_scons == stream_when`(LAM x l.TT)"
-shd_def "shd == stream_when`(LAM x l.x)"
-stl_def "stl == stream_when`(LAM x l.l)"
-
-(* ----------------------------------------------------------------------- *)
-(* the taker for streams *)
-
-stream_take_def "stream_take == (%n.iterate n stream_copy UU)"
-
-(* ----------------------------------------------------------------------- *)
-
-stream_finite_def "stream_finite == (%s.? n.stream_take n `s=s)"
-
-(* ----------------------------------------------------------------------- *)
-(* definition of bisimulation is determined by domain equation *)
-(* simplification and rewriting for abstract constants yields def below *)
-
-stream_bisim_def "stream_bisim ==
-(%R.!s1 s2.
- R s1 s2 -->
- ((s1=UU & s2=UU) |
- (? x s11 s21. x~=UU & s1=scons`x`s11 & s2 = scons`x`s21 & R s11 s21)))"
-
-end
-
-
-
-
--- a/src/HOLCF/explicit_domains/Stream2.ML Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(*
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-Lemmas for theory Stream2.thy
-*)
-
-open Stream2;
-
-(* ------------------------------------------------------------------------- *)
-(* expand fixed point properties *)
-(* ------------------------------------------------------------------------- *)
-
-val smap_def2 = fix_prover2 Stream2.thy smap_def
- "smap = (LAM f s. stream_when`(LAM x l.scons`(f`x) `(smap`f`l)) `s)";
-
-
-(* ------------------------------------------------------------------------- *)
-(* recursive properties *)
-(* ------------------------------------------------------------------------- *)
-
-
-qed_goal "smap1" Stream2.thy "smap`f`UU = UU"
- (fn prems =>
- [
- (stac smap_def2 1),
- (simp_tac (!simpset addsimps stream_when) 1)
- ]);
-
-qed_goal "smap2" Stream2.thy
- "x~=UU ==> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)"
- (fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac trans 1),
- (stac smap_def2 1),
- (asm_simp_tac (!simpset addsimps stream_rews) 1),
- (rtac refl 1)
- ]);
-
-
-val stream2_rews = [smap1, smap2];
--- a/src/HOLCF/explicit_domains/Stream2.thy Mon Feb 24 09:46:12 1997 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*
- ID: $Id$
- Author: Franz Regensburger
- Copyright 1993 Technische Universitaet Muenchen
-
-NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD.
-
-Additional constants for stream
-*)
-
-Stream2 = Stream +
-
-consts
-
-smap :: "('a -> 'b) -> 'a stream -> 'b stream"
-
-defs
-
-smap_def
- "smap == fix`(LAM h f s. stream_when`(LAM x l.scons `(f`x) `(h`f`l)) `s)"
-
-
-end
-
-
-(*
- smap`f`UU = UU
- x~=UU --> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)
-
-*)
-