# HG changeset patch # User oheimb # Date 856797144 -3600 # Node ID 3eac428cdd1bd8a94f0583a852fd849b98508d7a # Parent d5fe793293aca2fd7cd0772fe5a681fbc7ae215e removed explicit_domains/, which is now covered by ex/ diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/IsaMakefile --- 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 diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/Makefile --- 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 diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/ex/Coind.ML --- 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(); diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/ex/Coind.thy --- 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)) -*) - - diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/Dlist.ML --- 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)) - ]); - - - - diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/Dlist.thy --- 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 - - - - diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/Dnat.ML --- 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< - -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 diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/Dnat2.ML --- 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]; - - - diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/Dnat2.thy --- 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) -*) - diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/README --- 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. - diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/ROOT.ML --- 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"; diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/Stream.ML --- 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) - ]); - - diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/Stream.thy --- 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 - - - - diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/Stream2.ML --- 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]; diff -r d5fe793293ac -r 3eac428cdd1b src/HOLCF/explicit_domains/Stream2.thy --- 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) - -*) -