removed explicit_domains/, which is now covered by ex/
authoroheimb
Mon Feb 24 16:12:24 1997 +0100 (1997-02-24)
changeset 26793eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
removed explicit_domains/, which is now covered by ex/
src/HOLCF/IsaMakefile
src/HOLCF/Makefile
src/HOLCF/ex/Coind.ML
src/HOLCF/ex/Coind.thy
src/HOLCF/explicit_domains/Dlist.ML
src/HOLCF/explicit_domains/Dlist.thy
src/HOLCF/explicit_domains/Dnat.ML
src/HOLCF/explicit_domains/Dnat.thy
src/HOLCF/explicit_domains/Dnat2.ML
src/HOLCF/explicit_domains/Dnat2.thy
src/HOLCF/explicit_domains/README
src/HOLCF/explicit_domains/ROOT.ML
src/HOLCF/explicit_domains/Stream.ML
src/HOLCF/explicit_domains/Stream.thy
src/HOLCF/explicit_domains/Stream2.ML
src/HOLCF/explicit_domains/Stream2.thy
     1.1 --- a/src/HOLCF/IsaMakefile	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ b/src/HOLCF/IsaMakefile	Mon Feb 24 16:12:24 1997 +0100
     1.3 @@ -45,18 +45,4 @@
     1.4  test: ex/ROOT.ML $(OUT)/HOLCF $(EX_FILES)
     1.5  	@$(ISATOOL) testdir $(OUT)/HOLCF ex
     1.6  
     1.7 -
     1.8 -## Explicit domains
     1.9 -#
    1.10 -#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy\
    1.11 -#		 explicit_domains/Dlist.thy \
    1.12 -#		 explicit_domains/Stream.thy explicit_domains/Stream2.thy
    1.13 -
    1.14 -#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \
    1.15 -#			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
    1.16 -#
    1.17 -#test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES)
    1.18 -#	@$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains
    1.19 -
    1.20 -
    1.21  .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF
     2.1 --- a/src/HOLCF/Makefile	Mon Feb 24 09:46:12 1997 +0100
     2.2 +++ b/src/HOLCF/Makefile	Mon Feb 24 16:12:24 1997 +0100
     2.3 @@ -86,29 +86,5 @@
     2.4  			\"$(COMP)\" is not poly or sml;;\
     2.5  	esac
     2.6  
     2.7 -#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy \
     2.8 -#		explicit_domains/Dlist.thy \
     2.9 -#		explicit_domains/Stream.thy explicit_domains/Stream2.thy
    2.10 -
    2.11 -#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS)\
    2.12 -#			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
    2.13 -
    2.14 -#test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF	$(EXPLICIT_DOMAINS_FILES) 
    2.15 -#	@case `basename "$(COMP)"` in \
    2.16 -#	poly*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    2.17 -#		then echo 'make_html := true; exit_use_dir"explicit_domains";\
    2.18 -#			  quit();' | $(COMP) $(BIN)/HOLCF;\
    2.19 -#		else echo 'exit_use_dir"explicit_domains"; quit();' \
    2.20 -#		       | $(COMP) $(BIN)/HOLCF;\
    2.21 -#		fi;;\
    2.22 -#	sml*)	if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    2.23 -#		then echo 'make_html := true; exit_use_dir"exlicit_domains";' \
    2.24 -#		       | $(BIN)/HOLCF;\
    2.25 -#		else echo 'exit_use_dir"explicit_domains";' | $(BIN)/HOLCF;\
    2.26 -#		fi;;\
    2.27 -#	*)	echo Bad value for ISABELLECOMP: \
    2.28 -#			\"$(COMP)\" is not poly or sml;;\
    2.29 -#	esac
    2.30 -
    2.31  .PRECIOUS:  $(BIN)/HOL	$(BIN)/HOLCF 
    2.32  
     3.1 --- a/src/HOLCF/ex/Coind.ML	Mon Feb 24 09:46:12 1997 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,126 +0,0 @@
     3.4 -(*  Title: 	FOCUS/ex/coind.ML
     3.5 -    ID:         $ $
     3.6 -    Author: 	Franz Regensburger
     3.7 -    Copyright   1993, 1995 Technische Universitaet Muenchen
     3.8 -*)
     3.9 -
    3.10 -open Coind;
    3.11 -
    3.12 -(* ------------------------------------------------------------------------- *)
    3.13 -(* expand fixed point properties                                             *)
    3.14 -(* ------------------------------------------------------------------------- *)
    3.15 -
    3.16 -
    3.17 -val nats_def2 = fix_prover2 Coind.thy nats_def 
    3.18 -	"nats = dzero&&(smap`dsucc`nats)";
    3.19 -
    3.20 -val from_def2 = fix_prover2 Coind.thy from_def 
    3.21 -	"from = (n.n&&(from`(dsucc`n)))";
    3.22 -
    3.23 -
    3.24 -
    3.25 -(* ------------------------------------------------------------------------- *)
    3.26 -(* recursive  properties                                                     *)
    3.27 -(* ------------------------------------------------------------------------- *)
    3.28 -
    3.29 -
    3.30 -val from = prove_goal Coind.thy "from`n = n&&(from`(dsucc`n))"
    3.31 - (fn prems =>
    3.32 -	[
    3.33 -	(rtac trans 1),
    3.34 -	(rtac (from_def2 RS ssubst) 1),
    3.35 -	(simp_tac HOLCF_ss  1),
    3.36 -	(rtac refl 1)
    3.37 -	]);
    3.38 -
    3.39 -
    3.40 -val from1 = prove_goal Coind.thy "from` = "
    3.41 - (fn prems =>
    3.42 -	[
    3.43 -	(rtac trans 1),
    3.44 -	(rtac (from RS ssubst) 1),
    3.45 -	(resolve_tac  stream.con_rews 1),
    3.46 -	(rtac refl 1)
    3.47 -	]);
    3.48 -
    3.49 -val coind_rews = 
    3.50 -	[iterator1, iterator2, iterator3, smap1, smap2,from1];
    3.51 -
    3.52 -(* ------------------------------------------------------------------------- *)
    3.53 -(* the example                                                               *)
    3.54 -(* prove:        nats = from`dzero                                           *)
    3.55 -(* ------------------------------------------------------------------------- *)
    3.56 -
    3.57 -val prems = goal Coind.thy "iterator`n`(smap`dsucc)`nats =\
    3.58 -\		 n&&(iterator`(dsucc`n)`(smap`dsucc)`nats)";
    3.59 -by (res_inst_tac [("x","n")] dnat.ind 1);
    3.60 -by (simp_tac (HOLCF_ss addsimps (coind_rews @ stream.rews)) 1);
    3.61 -by (simp_tac (HOLCF_ss addsimps (coind_rews @ stream.rews)) 1);
    3.62 -by (rtac trans 1);
    3.63 -by (rtac nats_def2 1);
    3.64 -by (simp_tac (HOLCF_ss addsimps (coind_rews @ dnat.rews)) 1);
    3.65 -by (rtac trans 1);
    3.66 -by (etac iterator3 1);
    3.67 -by (rtac trans 1);
    3.68 -by (asm_simp_tac HOLCF_ss 1);
    3.69 -by (rtac trans 1);
    3.70 -by (etac smap2 1);
    3.71 -by (rtac cfun_arg_cong 1);
    3.72 -by (asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat.rews)) 1);
    3.73 -val coind_lemma1 = result();
    3.74 -
    3.75 -val prems = goal Coind.thy "nats = from`dzero";
    3.76 -by (res_inst_tac [("R","% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream.coind 1);
    3.77 -by (res_inst_tac [("x","dzero")] exI 2);
    3.78 -by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 2);
    3.79 -by (rewrite_goals_tac [stream.bisim_def]);
    3.80 -by (strip_tac 1);
    3.81 -by (etac exE 1);
    3.82 -by (etac conjE 1);
    3.83 -by (case_tac "n=" 1);
    3.84 -by (rtac disjI1 1);
    3.85 -by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
    3.86 -by (rtac disjI2 1);
    3.87 -by (hyp_subst_tac 1);
    3.88 -by (res_inst_tac [("x","n")] exI 1);
    3.89 -by (res_inst_tac [("x","iterator`(dsucc`n)`(smap`dsucc)`nats")] exI 1);
    3.90 -by (res_inst_tac [("x","from`(dsucc`n)")] exI 1);
    3.91 -by (etac conjI 1);
    3.92 -by (rtac conjI 1);
    3.93 -by (res_inst_tac [("x","dsucc`n")] exI 1);
    3.94 -by (fast_tac HOL_cs 1);
    3.95 -by (rtac conjI 1);
    3.96 -by (rtac coind_lemma1 1);
    3.97 -by (rtac from 1);
    3.98 -val nats_eq_from = result();
    3.99 -
   3.100 -(* another proof using stream_coind_lemma2 *)
   3.101 -
   3.102 -val prems = goal Coind.thy "nats = from`dzero";
   3.103 -by (res_inst_tac [("R","% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream.coind 1);
   3.104 -by (rtac stream_coind_lemma2 1);
   3.105 -by (strip_tac 1);
   3.106 -by (etac exE 1);
   3.107 -by (case_tac "n=" 1);
   3.108 -by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
   3.109 -by (res_inst_tac [("x","::dnat")] exI 1);
   3.110 -by (simp_tac (HOLCF_ss addsimps coind_rews addsimps stream.rews) 1);
   3.111 -by (etac conjE 1);
   3.112 -by (hyp_subst_tac 1);
   3.113 -by (rtac conjI 1);
   3.114 -by (rtac (coind_lemma1 RS ssubst) 1);
   3.115 -by (rtac (from RS ssubst) 1);
   3.116 -by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
   3.117 -by (res_inst_tac [("x","dsucc`n")] exI 1);
   3.118 -by (rtac conjI 1);
   3.119 -by (rtac trans 1);
   3.120 -by (rtac (coind_lemma1 RS ssubst) 1);
   3.121 -by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
   3.122 -by (rtac refl 1);
   3.123 -by (rtac trans 1);
   3.124 -by (rtac (from RS ssubst) 1);
   3.125 -by (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1);
   3.126 -by (rtac refl 1);
   3.127 -by (res_inst_tac [("x","dzero")] exI 1);
   3.128 -by (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1);
   3.129 -val nats_eq_from = result();
     4.1 --- a/src/HOLCF/ex/Coind.thy	Mon Feb 24 09:46:12 1997 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,33 +0,0 @@
     4.4 -(*  Title: 	FOCUS/ex/Coind.thy
     4.5 -    ID:         $ $
     4.6 -    Author: 	Franz Regensburger
     4.7 -    Copyright   1993 195 Technische Universitaet Muenchen
     4.8 -
     4.9 -Example for co-induction on streams
    4.10 -*)
    4.11 -
    4.12 -Coind = Stream + Dnat +
    4.13 -
    4.14 -
    4.15 -consts
    4.16 -
    4.17 -	nats		:: "dnat stream"
    4.18 -	from		:: "dnat  dnat stream"
    4.19 -
    4.20 -defs
    4.21 -	nats_def	"nats  fix`(h.dzero&&(smap`dsucc`h))"
    4.22 -
    4.23 -	from_def	"from  fix`(h n.n&&(h`(dsucc`n)))"
    4.24 -
    4.25 -end
    4.26 -
    4.27 -(*
    4.28 -		smap`f` = 
    4.29 -	x  smap`f`(x&&xs) = (f`x)&&(smap`f`xs)
    4.30 -
    4.31 -		nats = dzero&&(smap`dsucc`nats)
    4.32 -
    4.33 -		from`n = n&&(from`(dsucc`n))
    4.34 -*)
    4.35 -
    4.36 -
     5.1 --- a/src/HOLCF/explicit_domains/Dlist.ML	Mon Feb 24 09:46:12 1997 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,566 +0,0 @@
     5.4 -(*  Title:      HOLCF/Dlist.ML
     5.5 -    Author:     Franz Regensburger
     5.6 -    ID:         $ $
     5.7 -    Copyright   1994 Technische Universitaet Muenchen
     5.8 -
     5.9 -Lemmas for dlist.thy
    5.10 -*)
    5.11 -
    5.12 -open Dlist;
    5.13 -
    5.14 -Delsimps (ex_simps @ all_simps);
    5.15 -
    5.16 -(* ------------------------------------------------------------------------*)
    5.17 -(* The isomorphisms dlist_rep_iso and dlist_abs_iso are strict             *)
    5.18 -(* ------------------------------------------------------------------------*)
    5.19 -
    5.20 -val dlist_iso_strict= dlist_rep_iso RS (dlist_abs_iso RS 
    5.21 -        (allI  RSN (2,allI RS iso_strict)));
    5.22 -
    5.23 -val dlist_rews = [dlist_iso_strict RS conjunct1,
    5.24 -                dlist_iso_strict RS conjunct2];
    5.25 -
    5.26 -(* ------------------------------------------------------------------------*)
    5.27 -(* Properties of dlist_copy                                                *)
    5.28 -(* ------------------------------------------------------------------------*)
    5.29 -
    5.30 -val temp = prove_goalw Dlist.thy  [dlist_copy_def] "dlist_copy`f`UU=UU"
    5.31 - (fn prems =>
    5.32 -        [
    5.33 -        (asm_simp_tac (!simpset addsimps 
    5.34 -                (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
    5.35 -        ]);
    5.36 -
    5.37 -val dlist_copy = [temp];
    5.38 -
    5.39 -
    5.40 -val temp = prove_goalw Dlist.thy  [dlist_copy_def,dnil_def] 
    5.41 -    "dlist_copy`f`dnil=dnil"
    5.42 - (fn prems =>
    5.43 -        [
    5.44 -        (asm_simp_tac (!simpset addsimps 
    5.45 -                (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
    5.46 -        ]);
    5.47 -
    5.48 -val dlist_copy = temp :: dlist_copy;
    5.49 -
    5.50 -
    5.51 -val temp = prove_goalw Dlist.thy  [dlist_copy_def,dcons_def] 
    5.52 -        "xl~=UU ==> dlist_copy`f`(dcons`x`xl)= dcons`x`(f`xl)"
    5.53 - (fn prems =>
    5.54 -        [
    5.55 -        (cut_facts_tac prems 1),
    5.56 -        (asm_simp_tac (!simpset addsimps 
    5.57 -                (dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
    5.58 -        (case_tac "x=UU" 1),
    5.59 -        (Asm_simp_tac  1),
    5.60 -        (asm_simp_tac (!simpset addsimps [defined_spair]) 1)
    5.61 -        ]);
    5.62 -
    5.63 -val dlist_copy = temp :: dlist_copy;
    5.64 -
    5.65 -val dlist_rews =  dlist_copy @ dlist_rews; 
    5.66 -
    5.67 -(* ------------------------------------------------------------------------*)
    5.68 -(* Exhaustion and elimination for dlists                                   *)
    5.69 -(* ------------------------------------------------------------------------*)
    5.70 -
    5.71 -qed_goalw "Exh_dlist" Dlist.thy [dcons_def,dnil_def]
    5.72 -        "l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons`x`xl)"
    5.73 - (fn prems =>
    5.74 -        [
    5.75 -        (Simp_tac 1),
    5.76 -        (rtac (dlist_rep_iso RS subst) 1),
    5.77 -        (res_inst_tac [("p","dlist_rep`l")] ssumE 1),
    5.78 -        (rtac disjI1 1),
    5.79 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
    5.80 -        (rtac disjI2 1),
    5.81 -        (rtac disjI1 1),
    5.82 -        (res_inst_tac [("p","x")] oneE 1),
    5.83 -        (contr_tac 1),
    5.84 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
    5.85 -        (rtac disjI2 1),
    5.86 -        (rtac disjI2 1),
    5.87 -        (res_inst_tac [("p","y")] sprodE 1),
    5.88 -        (contr_tac 1),
    5.89 -        (rtac exI 1),
    5.90 -        (rtac exI 1),
    5.91 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
    5.92 -        (fast_tac HOL_cs 1)
    5.93 -        ]);
    5.94 -
    5.95 -
    5.96 -qed_goal "dlistE" Dlist.thy 
    5.97 -"[| l=UU ==> Q; l=dnil ==> Q;!!x xl.[|l=dcons`x`xl;x~=UU;xl~=UU|]==>Q|]==>Q"
    5.98 - (fn prems =>
    5.99 -        [
   5.100 -        (rtac (Exh_dlist RS disjE) 1),
   5.101 -        (eresolve_tac prems 1),
   5.102 -        (etac disjE 1),
   5.103 -        (eresolve_tac prems 1),
   5.104 -        (etac exE 1),
   5.105 -        (etac exE 1),
   5.106 -        (resolve_tac prems 1),
   5.107 -        (fast_tac HOL_cs 1),
   5.108 -        (fast_tac HOL_cs 1),
   5.109 -        (fast_tac HOL_cs 1)
   5.110 -        ]);
   5.111 -
   5.112 -(* ------------------------------------------------------------------------*)
   5.113 -(* Properties of dlist_when                                                *)
   5.114 -(* ------------------------------------------------------------------------*)
   5.115 -
   5.116 -val temp = prove_goalw  Dlist.thy  [dlist_when_def] "dlist_when`f1`f2`UU=UU"
   5.117 - (fn prems =>
   5.118 -        [
   5.119 -        (asm_simp_tac (!simpset addsimps [dlist_iso_strict]) 1)
   5.120 -        ]);
   5.121 -
   5.122 -val dlist_when = [temp];
   5.123 -
   5.124 -val temp = prove_goalw  Dlist.thy [dlist_when_def,dnil_def]
   5.125 - "dlist_when`f1`f2`dnil= f1"
   5.126 - (fn prems =>
   5.127 -        [
   5.128 -        (asm_simp_tac (!simpset addsimps [dlist_abs_iso]) 1)
   5.129 -        ]);
   5.130 -
   5.131 -val dlist_when = temp::dlist_when;
   5.132 -
   5.133 -val temp = prove_goalw  Dlist.thy [dlist_when_def,dcons_def]
   5.134 - "[|x~=UU;xl~=UU|] ==> dlist_when`f1`f2`(dcons`x`xl)= f2`x`xl"
   5.135 - (fn prems =>
   5.136 -        [
   5.137 -        (cut_facts_tac prems 1),
   5.138 -        (asm_simp_tac (!simpset addsimps [dlist_abs_iso,defined_spair]) 1)
   5.139 -        ]);
   5.140 -
   5.141 -val dlist_when = temp::dlist_when;
   5.142 -
   5.143 -val dlist_rews = dlist_when @ dlist_rews;
   5.144 -
   5.145 -(* ------------------------------------------------------------------------*)
   5.146 -(* Rewrites for  discriminators and  selectors                             *)
   5.147 -(* ------------------------------------------------------------------------*)
   5.148 -
   5.149 -fun prover defs thm = prove_goalw Dlist.thy defs thm
   5.150 - (fn prems =>
   5.151 -        [
   5.152 -        (simp_tac (!simpset addsimps dlist_rews) 1)
   5.153 -        ]);
   5.154 -
   5.155 -val dlist_discsel = [
   5.156 -        prover [is_dnil_def] "is_dnil`UU=UU",
   5.157 -        prover [is_dcons_def] "is_dcons`UU=UU",
   5.158 -        prover [dhd_def] "dhd`UU=UU",
   5.159 -        prover [dtl_def] "dtl`UU=UU"
   5.160 -        ];
   5.161 -
   5.162 -fun prover defs thm = prove_goalw Dlist.thy defs thm
   5.163 - (fn prems =>
   5.164 -        [
   5.165 -        (cut_facts_tac prems 1),
   5.166 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
   5.167 -        ]);
   5.168 -
   5.169 -val dlist_discsel = [
   5.170 -prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   5.171 -  "is_dnil`dnil=TT",
   5.172 -prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   5.173 -  "[|x~=UU;xl~=UU|] ==> is_dnil`(dcons`x`xl)=FF",
   5.174 -prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   5.175 -  "is_dcons`dnil=FF",
   5.176 -prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   5.177 -  "[|x~=UU;xl~=UU|] ==> is_dcons`(dcons`x`xl)=TT",
   5.178 -prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   5.179 -  "dhd`dnil=UU",
   5.180 -prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   5.181 -  "[|x~=UU;xl~=UU|] ==> dhd`(dcons`x`xl)=x",
   5.182 -prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   5.183 -  "dtl`dnil=UU",
   5.184 -prover [is_dnil_def,is_dcons_def,dhd_def,dtl_def]
   5.185 -  "[|x~=UU;xl~=UU|] ==> dtl`(dcons`x`xl)=xl"] @ dlist_discsel;
   5.186 -
   5.187 -val dlist_rews = dlist_discsel @ dlist_rews;
   5.188 -
   5.189 -(* ------------------------------------------------------------------------*)
   5.190 -(* Definedness and strictness                                              *)
   5.191 -(* ------------------------------------------------------------------------*)
   5.192 -
   5.193 -fun prover contr thm = prove_goal Dlist.thy thm
   5.194 - (fn prems =>
   5.195 -        [
   5.196 -        (res_inst_tac [("P1",contr)] classical2 1),
   5.197 -        (simp_tac (!simpset addsimps dlist_rews) 1),
   5.198 -        (dtac sym 1),
   5.199 -        (Asm_simp_tac  1),
   5.200 -        (simp_tac (!simpset addsimps (prems @ dlist_rews)) 1)
   5.201 -        ]);
   5.202 -
   5.203 -
   5.204 -val dlist_constrdef = [
   5.205 -prover "is_dnil`(UU::'a dlist) ~= UU" "dnil~=(UU::'a dlist)",
   5.206 -prover "is_dcons`(UU::'a dlist) ~= UU" 
   5.207 -        "[|x~=UU;xl~=UU|]==>dcons`(x::'a)`xl ~= UU"
   5.208 - ];
   5.209 -
   5.210 -
   5.211 -fun prover defs thm = prove_goalw Dlist.thy defs thm
   5.212 - (fn prems =>
   5.213 -        [
   5.214 -        (simp_tac (!simpset addsimps dlist_rews) 1)
   5.215 -        ]);
   5.216 -
   5.217 -val dlist_constrdef = [
   5.218 -        prover [dcons_def] "dcons`UU`xl=UU",
   5.219 -        prover [dcons_def] "dcons`x`UU=UU"
   5.220 -        ] @ dlist_constrdef;
   5.221 -
   5.222 -val dlist_rews = dlist_constrdef @ dlist_rews;
   5.223 -
   5.224 -
   5.225 -(* ------------------------------------------------------------------------*)
   5.226 -(* Distinctness wrt. << and =                                              *)
   5.227 -(* ------------------------------------------------------------------------*)
   5.228 -
   5.229 -val temp = prove_goal Dlist.thy  "~dnil << dcons`(x::'a)`xl"
   5.230 - (fn prems =>
   5.231 -        [
   5.232 -        (res_inst_tac [("P1","TT << FF")] classical2 1),
   5.233 -        (resolve_tac dist_less_tr 1),
   5.234 -        (dres_inst_tac [("fo","is_dnil")] monofun_cfun_arg 1),
   5.235 -        (etac box_less 1),
   5.236 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.237 -        (case_tac "(x::'a)=UU" 1),
   5.238 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.239 -        (case_tac "(xl ::'a dlist)=UU" 1),
   5.240 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.241 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
   5.242 -        ]);
   5.243 -
   5.244 -val dlist_dist_less = [temp];
   5.245 -
   5.246 -val temp = prove_goal Dlist.thy  "[|x~=UU;xl~=UU|]==>~ dcons`x`xl << dnil"
   5.247 - (fn prems =>
   5.248 -        [
   5.249 -        (cut_facts_tac prems 1),
   5.250 -        (res_inst_tac [("P1","TT << FF")] classical2 1),
   5.251 -        (resolve_tac dist_less_tr 1),
   5.252 -        (dres_inst_tac [("fo","is_dcons")] monofun_cfun_arg 1),
   5.253 -        (etac box_less 1),
   5.254 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.255 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
   5.256 -        ]);
   5.257 -
   5.258 -val dlist_dist_less = temp::dlist_dist_less;
   5.259 -
   5.260 -val temp = prove_goal Dlist.thy  "dnil ~= dcons`x`xl"
   5.261 - (fn prems =>
   5.262 -        [
   5.263 -        (case_tac "x=UU" 1),
   5.264 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.265 -        (case_tac "xl=UU" 1),
   5.266 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.267 -        (res_inst_tac [("P1","TT = FF")] classical2 1),
   5.268 -        (resolve_tac dist_eq_tr 1),
   5.269 -        (dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
   5.270 -        (etac box_equals 1),
   5.271 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.272 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
   5.273 -        ]);
   5.274 -
   5.275 -val dlist_dist_eq = [temp,temp RS not_sym];
   5.276 -
   5.277 -val dlist_rews = dlist_dist_less @ dlist_dist_eq @ dlist_rews;
   5.278 -
   5.279 -(* ------------------------------------------------------------------------*)
   5.280 -(* Invertibility                                                           *)
   5.281 -(* ------------------------------------------------------------------------*)
   5.282 -
   5.283 -val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
   5.284 -\ dcons`x1`x2 << dcons`y1`y2 |] ==> x1<< y1 & x2 << y2"
   5.285 - (fn prems =>
   5.286 -        [
   5.287 -        (cut_facts_tac prems 1),
   5.288 -        (rtac conjI 1),
   5.289 -        (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
   5.290 -        (etac box_less 1),
   5.291 -        (asm_simp_tac (!simpset addsimps dlist_when) 1),
   5.292 -        (asm_simp_tac (!simpset addsimps dlist_when) 1),
   5.293 -        (dres_inst_tac [("fo","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
   5.294 -        (etac box_less 1),
   5.295 -        (asm_simp_tac (!simpset addsimps dlist_when) 1),
   5.296 -        (asm_simp_tac (!simpset addsimps dlist_when) 1)
   5.297 -        ]);
   5.298 -
   5.299 -val dlist_invert =[temp];
   5.300 -
   5.301 -(* ------------------------------------------------------------------------*)
   5.302 -(* Injectivity                                                             *)
   5.303 -(* ------------------------------------------------------------------------*)
   5.304 -
   5.305 -val temp = prove_goal Dlist.thy "[|x1~=UU; y1~=UU;x2~=UU; y2~=UU;\
   5.306 -\ dcons`x1`x2 = dcons`y1`y2 |] ==> x1= y1 & x2 = y2"
   5.307 - (fn prems =>
   5.308 -        [
   5.309 -        (cut_facts_tac prems 1),
   5.310 -        (rtac conjI 1),
   5.311 -        (dres_inst_tac [("f","dlist_when`UU`(LAM x l.x)")] cfun_arg_cong 1),
   5.312 -        (etac box_equals 1),
   5.313 -        (asm_simp_tac (!simpset addsimps dlist_when) 1),
   5.314 -        (asm_simp_tac (!simpset addsimps dlist_when) 1),
   5.315 -        (dres_inst_tac [("f","dlist_when`UU`(LAM x l.l)")] cfun_arg_cong 1),
   5.316 -        (etac box_equals 1),
   5.317 -        (asm_simp_tac (!simpset addsimps dlist_when) 1),
   5.318 -        (asm_simp_tac (!simpset addsimps dlist_when) 1)
   5.319 -        ]);
   5.320 -
   5.321 -val dlist_inject = [temp];
   5.322 - 
   5.323 -
   5.324 -(* ------------------------------------------------------------------------*)
   5.325 -(* definedness for  discriminators and  selectors                          *)
   5.326 -(* ------------------------------------------------------------------------*)
   5.327 -
   5.328 -fun prover thm = prove_goal Dlist.thy thm
   5.329 - (fn prems =>
   5.330 -        [
   5.331 -        (cut_facts_tac prems 1),
   5.332 -        (rtac dlistE 1),
   5.333 -        (contr_tac 1),
   5.334 -        (REPEAT (asm_simp_tac (!simpset addsimps dlist_discsel) 1))
   5.335 -        ]);
   5.336 -
   5.337 -val dlist_discsel_def = 
   5.338 -        [
   5.339 -        prover "l~=UU ==> is_dnil`l~=UU", 
   5.340 -        prover "l~=UU ==> is_dcons`l~=UU" 
   5.341 -        ];
   5.342 -
   5.343 -val dlist_rews = dlist_discsel_def @ dlist_rews;
   5.344 -
   5.345 -(* ------------------------------------------------------------------------*)
   5.346 -(* enhance the simplifier                                                  *)
   5.347 -(* ------------------------------------------------------------------------*)
   5.348 -
   5.349 -qed_goal "dhd2" Dlist.thy "xl~=UU ==> dhd`(dcons`x`xl)=x"
   5.350 - (fn prems =>
   5.351 -        [
   5.352 -        (cut_facts_tac prems 1),
   5.353 -        (case_tac "x=UU" 1),
   5.354 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.355 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
   5.356 -        ]);
   5.357 -
   5.358 -qed_goal "dtl2" Dlist.thy "x~=UU ==> dtl`(dcons`x`xl)=xl"
   5.359 - (fn prems =>
   5.360 -        [
   5.361 -        (cut_facts_tac prems 1),
   5.362 -        (case_tac "xl=UU" 1),
   5.363 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.364 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
   5.365 -        ]);
   5.366 -
   5.367 -val dlist_rews = dhd2 :: dtl2 :: dlist_rews;
   5.368 -
   5.369 -(* ------------------------------------------------------------------------*)
   5.370 -(* Properties dlist_take                                                   *)
   5.371 -(* ------------------------------------------------------------------------*)
   5.372 -
   5.373 -val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take n`UU=UU"
   5.374 - (fn prems =>
   5.375 -        [
   5.376 -        (res_inst_tac [("n","n")] natE 1),
   5.377 -        (Asm_simp_tac 1),
   5.378 -        (Asm_simp_tac 1),
   5.379 -        (simp_tac (!simpset addsimps dlist_rews) 1)
   5.380 -        ]);
   5.381 -
   5.382 -val dlist_take = [temp];
   5.383 -
   5.384 -val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take 0`xs=UU"
   5.385 - (fn prems =>
   5.386 -        [
   5.387 -        (Asm_simp_tac 1)
   5.388 -        ]);
   5.389 -
   5.390 -val dlist_take = temp::dlist_take;
   5.391 -
   5.392 -val temp = prove_goalw Dlist.thy [dlist_take_def]
   5.393 -        "dlist_take (Suc n)`dnil=dnil"
   5.394 - (fn prems =>
   5.395 -        [
   5.396 -        (Asm_simp_tac 1),
   5.397 -        (simp_tac (!simpset addsimps dlist_rews) 1)
   5.398 -        ]);
   5.399 -
   5.400 -val dlist_take = temp::dlist_take;
   5.401 -
   5.402 -val temp = prove_goalw Dlist.thy [dlist_take_def]
   5.403 -  "dlist_take (Suc n)`(dcons`x`xl)= dcons`x`(dlist_take n`xl)"
   5.404 - (fn prems =>
   5.405 -        [
   5.406 -        (case_tac "x=UU" 1),
   5.407 -        (Asm_simp_tac 1),
   5.408 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.409 -        (case_tac "xl=UU" 1),
   5.410 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.411 -        (Asm_simp_tac 1),
   5.412 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.413 -        (res_inst_tac [("n","n")] natE 1),
   5.414 -        (Asm_simp_tac 1),
   5.415 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.416 -        (Asm_simp_tac 1),
   5.417 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.418 -        (Asm_simp_tac 1),
   5.419 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
   5.420 -        ]);
   5.421 -
   5.422 -val dlist_take = temp::dlist_take;
   5.423 -
   5.424 -val dlist_rews = dlist_take @ dlist_rews;
   5.425 -
   5.426 -(* ------------------------------------------------------------------------*)
   5.427 -(* take lemma for dlists                                                  *)
   5.428 -(* ------------------------------------------------------------------------*)
   5.429 -
   5.430 -fun prover reach defs thm  = prove_goalw Dlist.thy defs thm
   5.431 - (fn prems =>
   5.432 -        [
   5.433 -        (res_inst_tac [("t","l1")] (reach RS subst) 1),
   5.434 -        (res_inst_tac [("t","l2")] (reach RS subst) 1),
   5.435 -        (stac fix_def2 1),
   5.436 -        (stac contlub_cfun_fun 1),
   5.437 -        (rtac is_chain_iterate 1),
   5.438 -        (stac contlub_cfun_fun 1),
   5.439 -        (rtac is_chain_iterate 1),
   5.440 -        (rtac lub_equal 1),
   5.441 -        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
   5.442 -        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
   5.443 -        (rtac allI 1),
   5.444 -        (resolve_tac prems 1)
   5.445 -        ]);
   5.446 -
   5.447 -val dlist_take_lemma = prover dlist_reach  [dlist_take_def]
   5.448 -        "(!!n.dlist_take n`l1 = dlist_take n`l2) ==> l1=l2";
   5.449 -
   5.450 -
   5.451 -(* ------------------------------------------------------------------------*)
   5.452 -(* Co -induction for dlists                                               *)
   5.453 -(* ------------------------------------------------------------------------*)
   5.454 -
   5.455 -qed_goalw "dlist_coind_lemma" Dlist.thy [dlist_bisim_def] 
   5.456 -"dlist_bisim R ==> ! p q. R p q --> dlist_take n`p = dlist_take n`q"
   5.457 - (fn prems =>
   5.458 -        [
   5.459 -        (cut_facts_tac prems 1),
   5.460 -        (nat_ind_tac "n" 1),
   5.461 -        (simp_tac (!simpset addsimps dlist_rews) 1),
   5.462 -        (strip_tac 1),
   5.463 -        ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
   5.464 -        (atac 1),
   5.465 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.466 -        (etac disjE 1),
   5.467 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.468 -        (etac exE 1),
   5.469 -        (etac exE 1),
   5.470 -        (etac exE 1),
   5.471 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.472 -        (REPEAT (etac conjE 1)),
   5.473 -        (rtac cfun_arg_cong 1),
   5.474 -        (fast_tac HOL_cs 1)
   5.475 -        ]);
   5.476 -
   5.477 -qed_goal "dlist_coind" Dlist.thy "[|dlist_bisim R ; R p q |] ==> p = q"
   5.478 - (fn prems =>
   5.479 -        [
   5.480 -        (rtac dlist_take_lemma 1),
   5.481 -        (rtac (dlist_coind_lemma RS spec RS spec RS mp) 1),
   5.482 -        (resolve_tac prems 1),
   5.483 -        (resolve_tac prems 1)
   5.484 -        ]);
   5.485 -
   5.486 -(* ------------------------------------------------------------------------*)
   5.487 -(* structural induction                                                    *)
   5.488 -(* ------------------------------------------------------------------------*)
   5.489 -
   5.490 -qed_goal "dlist_finite_ind" Dlist.thy
   5.491 -"[|P(UU);P(dnil);\
   5.492 -\  !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons`x`l1)\
   5.493 -\  |] ==> !l.P(dlist_take n`l)"
   5.494 - (fn prems =>
   5.495 -        [
   5.496 -        (nat_ind_tac "n" 1),
   5.497 -        (simp_tac (!simpset addsimps dlist_rews) 1),
   5.498 -        (resolve_tac prems 1),
   5.499 -        (rtac allI 1),
   5.500 -        (res_inst_tac [("l","l")] dlistE 1),
   5.501 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.502 -        (resolve_tac prems 1),
   5.503 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.504 -        (resolve_tac prems 1),
   5.505 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.506 -        (case_tac "dlist_take n1`xl=UU" 1),
   5.507 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.508 -        (resolve_tac prems 1),
   5.509 -        (resolve_tac prems 1),
   5.510 -        (atac 1),
   5.511 -        (atac 1),
   5.512 -        (etac spec 1)
   5.513 -        ]);
   5.514 -
   5.515 -qed_goal "dlist_all_finite_lemma1" Dlist.thy
   5.516 -"!l.dlist_take n`l=UU |dlist_take n`l=l"
   5.517 - (fn prems =>
   5.518 -        [
   5.519 -        (nat_ind_tac "n" 1),
   5.520 -        (simp_tac (!simpset addsimps dlist_rews) 1),
   5.521 -        (rtac allI 1),
   5.522 -        (res_inst_tac [("l","l")] dlistE 1),
   5.523 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.524 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.525 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.526 -        (eres_inst_tac [("x","xl")] allE 1),
   5.527 -        (etac disjE 1),
   5.528 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.529 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1)
   5.530 -        ]);
   5.531 -
   5.532 -qed_goal "dlist_all_finite_lemma2" Dlist.thy "? n.dlist_take n`l=l"
   5.533 - (fn prems =>
   5.534 -        [
   5.535 -        (case_tac "l=UU" 1),
   5.536 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.537 -        (subgoal_tac "(!n.dlist_take n`l=UU) |(? n.dlist_take n`l = l)" 1),
   5.538 -        (etac disjE 1),
   5.539 -        (eres_inst_tac [("P","l=UU")] notE 1),
   5.540 -        (rtac dlist_take_lemma 1),
   5.541 -        (asm_simp_tac (!simpset addsimps dlist_rews) 1),
   5.542 -        (atac 1),
   5.543 -        (subgoal_tac "!n.!l.dlist_take n`l=UU |dlist_take n`l=l" 1),
   5.544 -        (fast_tac HOL_cs 1),
   5.545 -        (rtac allI 1),
   5.546 -        (rtac dlist_all_finite_lemma1 1)
   5.547 -        ]);
   5.548 -
   5.549 -qed_goalw "dlist_all_finite" Dlist.thy [dlist_finite_def] "dlist_finite(l)"
   5.550 - (fn prems =>
   5.551 -        [
   5.552 -        (rtac  dlist_all_finite_lemma2 1)
   5.553 -        ]);
   5.554 -
   5.555 -qed_goal "dlist_ind" Dlist.thy
   5.556 -"[|P(UU);P(dnil);\
   5.557 -\  !! x l1.[|x~=UU;l1~=UU;P(l1)|] ==> P(dcons`x`l1)|] ==> P(l)"
   5.558 - (fn prems =>
   5.559 -        [
   5.560 -        (rtac (dlist_all_finite_lemma2 RS exE) 1),
   5.561 -        (etac subst 1),
   5.562 -        (rtac (dlist_finite_ind RS spec) 1),
   5.563 -        (REPEAT (resolve_tac prems 1)),
   5.564 -        (REPEAT (atac 1))
   5.565 -        ]);
   5.566 -
   5.567 -
   5.568 -
   5.569 -
     6.1 --- a/src/HOLCF/explicit_domains/Dlist.thy	Mon Feb 24 09:46:12 1997 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,128 +0,0 @@
     6.4 -(*  Title:      HOLCF/Dlist.thy
     6.5 -
     6.6 -    Author:     Franz Regensburger
     6.7 -    ID:         $ $
     6.8 -    Copyright   1994 Technische Universitaet Muenchen
     6.9 -
    6.10 -NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dlist.thy INSTEAD.
    6.11 -
    6.12 -Theory for finite lists  'a dlist = one ++ ('a ** 'a dlist)
    6.13 -
    6.14 -The type is axiomatized as the least solution of the domain equation above.
    6.15 -The functor term that specifies the domain equation is: 
    6.16 -
    6.17 -  FT = <++,K_{one},<**,K_{'a},I>>
    6.18 -
    6.19 -For details see chapter 5 of:
    6.20 -
    6.21 -[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
    6.22 -                     Dissertation, Technische Universit"at M"unchen, 1994
    6.23 -
    6.24 -
    6.25 -*)
    6.26 -
    6.27 -Dlist = Stream2 +
    6.28 -
    6.29 -types dlist 1
    6.30 -
    6.31 -(* ----------------------------------------------------------------------- *)
    6.32 -(* arity axiom is validated by semantic reasoning                          *)
    6.33 -(* partial ordering is implicit in the isomorphism axioms and their cont.  *)
    6.34 -
    6.35 -arities dlist::(pcpo)pcpo
    6.36 -
    6.37 -consts
    6.38 -
    6.39 -(* ----------------------------------------------------------------------- *)
    6.40 -(* essential constants                                                     *)
    6.41 -
    6.42 -dlist_rep       :: "('a dlist) -> (one ++ 'a ** 'a dlist)"
    6.43 -dlist_abs       :: "(one ++ 'a ** 'a dlist) -> ('a dlist)"
    6.44 -
    6.45 -(* ----------------------------------------------------------------------- *)
    6.46 -(* abstract constants and auxiliary constants                              *)
    6.47 -
    6.48 -dlist_copy      :: "('a dlist -> 'a dlist) ->'a dlist -> 'a dlist"
    6.49 -
    6.50 -dnil            :: "'a dlist"
    6.51 -dcons           :: "'a -> 'a dlist -> 'a dlist"
    6.52 -dlist_when      :: " 'b -> ('a -> 'a dlist -> 'b) -> 'a dlist -> 'b"
    6.53 -is_dnil         :: "'a dlist -> tr"
    6.54 -is_dcons        :: "'a dlist -> tr"
    6.55 -dhd             :: "'a dlist -> 'a"
    6.56 -dtl             :: "'a dlist -> 'a dlist"
    6.57 -dlist_take      :: "nat => 'a dlist -> 'a dlist"
    6.58 -dlist_finite    :: "'a dlist => bool"
    6.59 -dlist_bisim     :: "('a dlist => 'a dlist => bool) => bool"
    6.60 -
    6.61 -rules
    6.62 -
    6.63 -(* ----------------------------------------------------------------------- *)
    6.64 -(* axiomatization of recursive type 'a dlist                               *)
    6.65 -(* ----------------------------------------------------------------------- *)
    6.66 -(* ('a dlist,dlist_abs) is the initial F-algebra where                     *)
    6.67 -(* F is the locally continuous functor determined by functor term FT.      *)
    6.68 -(* domain equation: 'a dlist = one ++ ('a ** 'a dlist)                     *)
    6.69 -(* functor term:    FT = <++,K_{one},<**,K_{'a},I>>                        *)
    6.70 -(* ----------------------------------------------------------------------- *)
    6.71 -(* dlist_abs is an isomorphism with inverse dlist_rep                      *)
    6.72 -(* identity is the least endomorphism on 'a dlist                          *)
    6.73 -
    6.74 -dlist_abs_iso   "dlist_rep`(dlist_abs`x) = x"
    6.75 -dlist_rep_iso   "dlist_abs`(dlist_rep`x) = x"
    6.76 -dlist_copy_def  "dlist_copy == (LAM f. dlist_abs oo \
    6.77 -\               (sswhen`sinl`(sinr oo (ssplit`(LAM x y. (|x,f`y|) ))))\
    6.78 -\                                oo dlist_rep)"
    6.79 -dlist_reach     "(fix`dlist_copy)`x=x"
    6.80 -
    6.81 -
    6.82 -defs
    6.83 -(* ----------------------------------------------------------------------- *)
    6.84 -(* properties of additional constants                                      *)
    6.85 -(* ----------------------------------------------------------------------- *)
    6.86 -(* constructors                                                            *)
    6.87 -
    6.88 -dnil_def        "dnil  == dlist_abs`(sinl`one)"
    6.89 -dcons_def       "dcons == (LAM x l. dlist_abs`(sinr`(|x,l|) ))"
    6.90 -
    6.91 -(* ----------------------------------------------------------------------- *)
    6.92 -(* discriminator functional                                                *)
    6.93 -
    6.94 -dlist_when_def 
    6.95 -"dlist_when == (LAM f1 f2 l.\
    6.96 -\   sswhen`(LAM x.f1) `(ssplit`(LAM x l.f2`x`l)) `(dlist_rep`l))"
    6.97 -
    6.98 -(* ----------------------------------------------------------------------- *)
    6.99 -(* discriminators and selectors                                            *)
   6.100 -
   6.101 -is_dnil_def     "is_dnil  == dlist_when`TT`(LAM x l.FF)"
   6.102 -is_dcons_def    "is_dcons == dlist_when`FF`(LAM x l.TT)"
   6.103 -dhd_def         "dhd == dlist_when`UU`(LAM x l.x)"
   6.104 -dtl_def         "dtl == dlist_when`UU`(LAM x l.l)"
   6.105 -
   6.106 -(* ----------------------------------------------------------------------- *)
   6.107 -(* the taker for dlists                                                   *)
   6.108 -
   6.109 -dlist_take_def "dlist_take == (%n.iterate n dlist_copy UU)"
   6.110 -
   6.111 -(* ----------------------------------------------------------------------- *)
   6.112 -
   6.113 -dlist_finite_def        "dlist_finite == (%s.? n.dlist_take n`s=s)"
   6.114 -
   6.115 -(* ----------------------------------------------------------------------- *)
   6.116 -(* definition of bisimulation is determined by domain equation             *)
   6.117 -(* simplification and rewriting for abstract constants yields def below    *)
   6.118 -
   6.119 -dlist_bisim_def "dlist_bisim ==
   6.120 - ( %R.!l1 l2.
   6.121 -        R l1 l2 -->
   6.122 -  ((l1=UU & l2=UU) |
   6.123 -   (l1=dnil & l2=dnil) |
   6.124 -   (? x l11 l21. x~=UU & l11~=UU & l21~=UU & 
   6.125 -               l1=dcons`x`l11 & l2 = dcons`x`l21 & R l11 l21)))"
   6.126 -
   6.127 -end
   6.128 -
   6.129 -
   6.130 -
   6.131 -
     7.1 --- a/src/HOLCF/explicit_domains/Dnat.ML	Mon Feb 24 09:46:12 1997 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,534 +0,0 @@
     7.4 -(*  Title:      HOLCF/Dnat.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Franz Regensburger
     7.7 -    Copyright   1993 Technische Universitaet Muenchen
     7.8 -
     7.9 -Lemmas for dnat.thy 
    7.10 -*)
    7.11 -
    7.12 -open Dnat;
    7.13 -
    7.14 -(* ------------------------------------------------------------------------*)
    7.15 -(* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict               *)
    7.16 -(* ------------------------------------------------------------------------*)
    7.17 -
    7.18 -val dnat_iso_strict = dnat_rep_iso RS (dnat_abs_iso RS 
    7.19 -        (allI  RSN (2,allI RS iso_strict)));
    7.20 -
    7.21 -val dnat_rews = [dnat_iso_strict RS conjunct1,
    7.22 -                dnat_iso_strict RS conjunct2];
    7.23 -
    7.24 -(* ------------------------------------------------------------------------*)
    7.25 -(* Properties of dnat_copy                                                 *)
    7.26 -(* ------------------------------------------------------------------------*)
    7.27 -
    7.28 -fun prover defs thm =  prove_goalw Dnat.thy defs thm
    7.29 - (fn prems =>
    7.30 -        [
    7.31 -        (cut_facts_tac prems 1),
    7.32 -        (asm_simp_tac (!simpset addsimps 
    7.33 -                (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
    7.34 -        ]);
    7.35 -
    7.36 -val dnat_copy = 
    7.37 -        [
    7.38 -        prover [dnat_copy_def] "dnat_copy`f`UU=UU",
    7.39 -        prover [dnat_copy_def,dzero_def] "dnat_copy`f`dzero= dzero",
    7.40 -        prover [dnat_copy_def,dsucc_def] 
    7.41 -                "n~=UU ==> dnat_copy`f`(dsucc`n) = dsucc`(f`n)"
    7.42 -        ];
    7.43 -
    7.44 -val dnat_rews =  dnat_copy @ dnat_rews; 
    7.45 -
    7.46 -(* ------------------------------------------------------------------------*)
    7.47 -(* Exhaustion and elimination for dnat                                     *)
    7.48 -(* ------------------------------------------------------------------------*)
    7.49 -
    7.50 -qed_goalw "Exh_dnat" Dnat.thy [dsucc_def,dzero_def]
    7.51 -        "n = UU | n = dzero | (? x . x~=UU & n = dsucc`x)"
    7.52 - (fn prems =>
    7.53 -        [
    7.54 -        (Simp_tac  1),
    7.55 -        (rtac (dnat_rep_iso RS subst) 1),
    7.56 -        (res_inst_tac [("p","dnat_rep`n")] ssumE 1),
    7.57 -        (rtac disjI1 1),
    7.58 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
    7.59 -        (rtac (disjI1 RS disjI2) 1),
    7.60 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
    7.61 -        (res_inst_tac [("p","x")] oneE 1),
    7.62 -        (contr_tac 1),
    7.63 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
    7.64 -        (rtac (disjI2 RS disjI2) 1),
    7.65 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
    7.66 -        (fast_tac HOL_cs 1)
    7.67 -        ]);
    7.68 -
    7.69 -qed_goal "dnatE" Dnat.thy 
    7.70 - "[| n=UU ==> Q; n=dzero ==> Q; !!x.[|n=dsucc`x;x~=UU|]==>Q|]==>Q"
    7.71 - (fn prems =>
    7.72 -        [
    7.73 -        (rtac (Exh_dnat RS disjE) 1),
    7.74 -        (eresolve_tac prems 1),
    7.75 -        (etac disjE 1),
    7.76 -        (eresolve_tac prems 1),
    7.77 -        (REPEAT (etac exE 1)),
    7.78 -        (resolve_tac prems 1),
    7.79 -        (fast_tac HOL_cs 1),
    7.80 -        (fast_tac HOL_cs 1)
    7.81 -        ]);
    7.82 -
    7.83 -(* ------------------------------------------------------------------------*)
    7.84 -(* Properties of dnat_when                                                 *)
    7.85 -(* ------------------------------------------------------------------------*)
    7.86 -
    7.87 -fun prover defs thm =  prove_goalw Dnat.thy defs thm
    7.88 - (fn prems =>
    7.89 -        [
    7.90 -        (cut_facts_tac prems 1),
    7.91 -        (asm_simp_tac (!simpset addsimps 
    7.92 -                (dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
    7.93 -        ]);
    7.94 -
    7.95 -
    7.96 -val dnat_when = [
    7.97 -        prover [dnat_when_def] "dnat_when`c`f`UU=UU",
    7.98 -        prover [dnat_when_def,dzero_def] "dnat_when`c`f`dzero=c",
    7.99 -        prover [dnat_when_def,dsucc_def] 
   7.100 -                "n~=UU ==> dnat_when`c`f`(dsucc`n)=f`n"
   7.101 -        ];
   7.102 -
   7.103 -val dnat_rews = dnat_when @ dnat_rews;
   7.104 -
   7.105 -(* ------------------------------------------------------------------------*)
   7.106 -(* Rewrites for  discriminators and  selectors                             *)
   7.107 -(* ------------------------------------------------------------------------*)
   7.108 -
   7.109 -fun prover defs thm = prove_goalw Dnat.thy defs thm
   7.110 - (fn prems =>
   7.111 -        [
   7.112 -        (simp_tac (!simpset addsimps dnat_rews) 1)
   7.113 -        ]);
   7.114 -
   7.115 -val dnat_discsel = [
   7.116 -        prover [is_dzero_def] "is_dzero`UU=UU",
   7.117 -        prover [is_dsucc_def] "is_dsucc`UU=UU",
   7.118 -        prover [dpred_def] "dpred`UU=UU"
   7.119 -        ];
   7.120 -
   7.121 -
   7.122 -fun prover defs thm = prove_goalw Dnat.thy defs thm
   7.123 - (fn prems =>
   7.124 -        [
   7.125 -        (cut_facts_tac prems 1),
   7.126 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.127 -        ]);
   7.128 -
   7.129 -val dnat_discsel = [
   7.130 -        prover [is_dzero_def] "is_dzero`dzero=TT",
   7.131 -        prover [is_dzero_def] "n~=UU ==>is_dzero`(dsucc`n)=FF",
   7.132 -        prover [is_dsucc_def] "is_dsucc`dzero=FF",
   7.133 -        prover [is_dsucc_def] "n~=UU ==> is_dsucc`(dsucc`n)=TT",
   7.134 -        prover [dpred_def] "dpred`dzero=UU",
   7.135 -        prover [dpred_def] "n~=UU ==> dpred`(dsucc`n)=n"
   7.136 -        ] @ dnat_discsel;
   7.137 -
   7.138 -val dnat_rews = dnat_discsel @ dnat_rews;
   7.139 -
   7.140 -(* ------------------------------------------------------------------------*)
   7.141 -(* Definedness and strictness                                              *)
   7.142 -(* ------------------------------------------------------------------------*)
   7.143 -
   7.144 -fun prover contr thm = prove_goal Dnat.thy thm
   7.145 - (fn prems =>
   7.146 -        [
   7.147 -        (res_inst_tac [("P1",contr)] classical2 1),
   7.148 -        (simp_tac (!simpset addsimps dnat_rews) 1),
   7.149 -        (dtac sym 1),
   7.150 -        (Asm_simp_tac  1),
   7.151 -        (simp_tac (!simpset addsimps (prems @ dnat_rews)) 1)
   7.152 -        ]);
   7.153 -
   7.154 -val dnat_constrdef = [
   7.155 -        prover "is_dzero`UU ~= UU" "dzero~=UU",
   7.156 -        prover "is_dsucc`UU ~= UU" "n~=UU ==> dsucc`n~=UU"
   7.157 -        ]; 
   7.158 -
   7.159 -
   7.160 -fun prover defs thm = prove_goalw Dnat.thy defs thm
   7.161 - (fn prems =>
   7.162 -        [
   7.163 -        (simp_tac (!simpset addsimps dnat_rews) 1)
   7.164 -        ]);
   7.165 -
   7.166 -val dnat_constrdef = [
   7.167 -        prover [dsucc_def] "dsucc`UU=UU"
   7.168 -        ] @ dnat_constrdef;
   7.169 -
   7.170 -val dnat_rews = dnat_constrdef @ dnat_rews;
   7.171 -
   7.172 -
   7.173 -(* ------------------------------------------------------------------------*)
   7.174 -(* Distinctness wrt. << and =                                              *)
   7.175 -(* ------------------------------------------------------------------------*)
   7.176 -
   7.177 -val temp = prove_goal Dnat.thy  "~dzero << dsucc`n"
   7.178 - (fn prems =>
   7.179 -        [
   7.180 -        (res_inst_tac [("P1","TT << FF")] classical2 1),
   7.181 -        (resolve_tac dist_less_tr 1),
   7.182 -        (dres_inst_tac [("fo","is_dzero")] monofun_cfun_arg 1),
   7.183 -        (etac box_less 1),
   7.184 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.185 -        (case_tac "n=UU" 1),
   7.186 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.187 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.188 -        ]);
   7.189 -
   7.190 -val dnat_dist_less = [temp];
   7.191 -
   7.192 -val temp = prove_goal Dnat.thy  "n~=UU ==> ~dsucc`n << dzero"
   7.193 - (fn prems =>
   7.194 -        [
   7.195 -        (cut_facts_tac prems 1),
   7.196 -        (res_inst_tac [("P1","TT << FF")] classical2 1),
   7.197 -        (resolve_tac dist_less_tr 1),
   7.198 -        (dres_inst_tac [("fo","is_dsucc")] monofun_cfun_arg 1),
   7.199 -        (etac box_less 1),
   7.200 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.201 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.202 -        ]);
   7.203 -
   7.204 -val dnat_dist_less = temp::dnat_dist_less;
   7.205 -
   7.206 -val temp = prove_goal Dnat.thy   "dzero ~= dsucc`n"
   7.207 - (fn prems =>
   7.208 -        [
   7.209 -        (case_tac "n=UU" 1),
   7.210 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.211 -        (res_inst_tac [("P1","TT = FF")] classical2 1),
   7.212 -        (resolve_tac dist_eq_tr 1),
   7.213 -        (dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
   7.214 -        (etac box_equals 1),
   7.215 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.216 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.217 -        ]);
   7.218 -
   7.219 -val dnat_dist_eq = [temp, temp RS not_sym];
   7.220 -
   7.221 -val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews;
   7.222 -
   7.223 -(* ------------------------------------------------------------------------*)
   7.224 -(* Invertibility                                                           *)
   7.225 -(* ------------------------------------------------------------------------*)
   7.226 -
   7.227 -val dnat_invert = 
   7.228 -        [
   7.229 -prove_goal Dnat.thy 
   7.230 -"[|x1~=UU; y1~=UU; dsucc`x1 << dsucc`y1 |] ==> x1<< y1"
   7.231 - (fn prems =>
   7.232 -        [
   7.233 -        (cut_facts_tac prems 1),
   7.234 -        (dres_inst_tac [("fo","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
   7.235 -        (etac box_less 1),
   7.236 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.237 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.238 -        ])
   7.239 -        ];
   7.240 -
   7.241 -(* ------------------------------------------------------------------------*)
   7.242 -(* Injectivity                                                             *)
   7.243 -(* ------------------------------------------------------------------------*)
   7.244 -
   7.245 -val dnat_inject = 
   7.246 -        [
   7.247 -prove_goal Dnat.thy 
   7.248 -"[|x1~=UU; y1~=UU; dsucc`x1 = dsucc`y1 |] ==> x1= y1"
   7.249 - (fn prems =>
   7.250 -        [
   7.251 -        (cut_facts_tac prems 1),
   7.252 -        (dres_inst_tac [("f","dnat_when`c`(LAM x.x)")] cfun_arg_cong 1),
   7.253 -        (etac box_equals 1),
   7.254 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.255 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.256 -        ])
   7.257 -        ];
   7.258 -
   7.259 -(* ------------------------------------------------------------------------*)
   7.260 -(* definedness for  discriminators and  selectors                          *)
   7.261 -(* ------------------------------------------------------------------------*)
   7.262 -
   7.263 -
   7.264 -fun prover thm = prove_goal Dnat.thy thm
   7.265 - (fn prems =>
   7.266 -        [
   7.267 -        (cut_facts_tac prems 1),
   7.268 -        (rtac dnatE 1),
   7.269 -        (contr_tac 1),
   7.270 -        (REPEAT (asm_simp_tac (!simpset addsimps dnat_rews) 1))
   7.271 -        ]);
   7.272 -
   7.273 -val dnat_discsel_def = 
   7.274 -        [
   7.275 -        prover  "n~=UU ==> is_dzero`n ~= UU",
   7.276 -        prover  "n~=UU ==> is_dsucc`n ~= UU"
   7.277 -        ];
   7.278 -
   7.279 -val dnat_rews = dnat_discsel_def @ dnat_rews;
   7.280 -
   7.281 - 
   7.282 -(* ------------------------------------------------------------------------*)
   7.283 -(* Properties dnat_take                                                    *)
   7.284 -(* ------------------------------------------------------------------------*)
   7.285 -val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take n`UU = UU"
   7.286 - (fn prems =>
   7.287 -        [
   7.288 -        (res_inst_tac [("n","n")] natE 1),
   7.289 -        (Asm_simp_tac 1),
   7.290 -        (Asm_simp_tac 1),
   7.291 -        (simp_tac (!simpset addsimps dnat_rews) 1)
   7.292 -        ]);
   7.293 -
   7.294 -val dnat_take = [temp];
   7.295 -
   7.296 -val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take 0`xs = UU"
   7.297 - (fn prems =>
   7.298 -        [
   7.299 -        (Asm_simp_tac 1)
   7.300 -        ]);
   7.301 -
   7.302 -val dnat_take = temp::dnat_take;
   7.303 -
   7.304 -val temp = prove_goalw Dnat.thy [dnat_take_def]
   7.305 -        "dnat_take (Suc n)`dzero=dzero"
   7.306 - (fn prems =>
   7.307 -        [
   7.308 -        (Asm_simp_tac 1),
   7.309 -        (simp_tac (!simpset addsimps dnat_rews) 1)
   7.310 -        ]);
   7.311 -
   7.312 -val dnat_take = temp::dnat_take;
   7.313 -
   7.314 -val temp = prove_goalw Dnat.thy [dnat_take_def]
   7.315 -  "dnat_take (Suc n)`(dsucc`xs)=dsucc`(dnat_take n ` xs)"
   7.316 - (fn prems =>
   7.317 -        [
   7.318 -        (case_tac "xs=UU" 1),
   7.319 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.320 -        (Asm_simp_tac 1),
   7.321 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.322 -        (res_inst_tac [("n","n")] natE 1),
   7.323 -        (Asm_simp_tac 1),
   7.324 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.325 -        (Asm_simp_tac 1),
   7.326 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.327 -        (Asm_simp_tac 1),
   7.328 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.329 -        ]);
   7.330 -
   7.331 -val dnat_take = temp::dnat_take;
   7.332 -
   7.333 -val dnat_rews = dnat_take @ dnat_rews;
   7.334 -
   7.335 -
   7.336 -(* ------------------------------------------------------------------------*)
   7.337 -(* take lemma for dnats                                                  *)
   7.338 -(* ------------------------------------------------------------------------*)
   7.339 -
   7.340 -fun prover reach defs thm  = prove_goalw Dnat.thy defs thm
   7.341 - (fn prems =>
   7.342 -        [
   7.343 -        (res_inst_tac [("t","s1")] (reach RS subst) 1),
   7.344 -        (res_inst_tac [("t","s2")] (reach RS subst) 1),
   7.345 -        (stac fix_def2 1),
   7.346 -        (stac contlub_cfun_fun 1),
   7.347 -        (rtac is_chain_iterate 1),
   7.348 -        (stac contlub_cfun_fun 1),
   7.349 -        (rtac is_chain_iterate 1),
   7.350 -        (rtac lub_equal 1),
   7.351 -        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
   7.352 -        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
   7.353 -        (rtac allI 1),
   7.354 -        (resolve_tac prems 1)
   7.355 -        ]);
   7.356 -
   7.357 -val dnat_take_lemma = prover dnat_reach  [dnat_take_def]
   7.358 -        "(!!n.dnat_take n`s1 = dnat_take n`s2) ==> s1=s2";
   7.359 -
   7.360 -
   7.361 -(* ------------------------------------------------------------------------*)
   7.362 -(* Co -induction for dnats                                                 *)
   7.363 -(* ------------------------------------------------------------------------*)
   7.364 -
   7.365 -qed_goalw "dnat_coind_lemma" Dnat.thy [dnat_bisim_def] 
   7.366 -"dnat_bisim R ==> ! p q. R p q --> dnat_take n`p = dnat_take n`q"
   7.367 - (fn prems =>
   7.368 -        [
   7.369 -        (cut_facts_tac prems 1),
   7.370 -        (nat_ind_tac "n" 1),
   7.371 -        (simp_tac (!simpset addsimps dnat_take) 1),
   7.372 -        (strip_tac 1),
   7.373 -        ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
   7.374 -        (atac 1),
   7.375 -        (asm_simp_tac (!simpset addsimps dnat_take) 1),
   7.376 -        (etac disjE 1),
   7.377 -        (asm_simp_tac (!simpset addsimps dnat_take) 1),
   7.378 -        (etac exE 1),
   7.379 -        (etac exE 1),
   7.380 -        (asm_simp_tac (!simpset addsimps dnat_take) 1),
   7.381 -        (REPEAT (etac conjE 1)),
   7.382 -        (rtac cfun_arg_cong 1),
   7.383 -        (fast_tac HOL_cs 1)
   7.384 -        ]);
   7.385 -
   7.386 -qed_goal "dnat_coind" Dnat.thy "[|dnat_bisim R;R p q|] ==> p = q"
   7.387 - (fn prems =>
   7.388 -        [
   7.389 -        (rtac dnat_take_lemma 1),
   7.390 -        (rtac (dnat_coind_lemma RS spec RS spec RS mp) 1),
   7.391 -        (resolve_tac prems 1),
   7.392 -        (resolve_tac prems 1)
   7.393 -        ]);
   7.394 -
   7.395 -
   7.396 -(* ------------------------------------------------------------------------*)
   7.397 -(* structural induction for admissible predicates                          *)
   7.398 -(* ------------------------------------------------------------------------*)
   7.399 -
   7.400 -(* not needed any longer
   7.401 -qed_goal "dnat_ind" Dnat.thy
   7.402 -"[| adm(P);\
   7.403 -\   P(UU);\
   7.404 -\   P(dzero);\
   7.405 -\   !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc`s1)|] ==> P(s)"
   7.406 - (fn prems =>
   7.407 -        [
   7.408 -        (rtac (dnat_reach RS subst) 1),
   7.409 -        (res_inst_tac [("x","s")] spec 1),
   7.410 -        (rtac fix_ind 1),
   7.411 -        (rtac adm_all2 1),
   7.412 -        (rtac adm_subst 1),
   7.413 -        (cont_tacR 1),
   7.414 -        (resolve_tac prems 1),
   7.415 -        (Simp_tac 1),
   7.416 -        (resolve_tac prems 1),
   7.417 -        (strip_tac 1),
   7.418 -        (res_inst_tac [("n","xa")] dnatE 1),
   7.419 -        (asm_simp_tac (!simpset addsimps dnat_copy) 1),
   7.420 -        (resolve_tac prems 1),
   7.421 -        (asm_simp_tac (!simpset addsimps dnat_copy) 1),
   7.422 -        (resolve_tac prems 1),
   7.423 -        (asm_simp_tac (!simpset addsimps dnat_copy) 1),
   7.424 -        (case_tac "x`xb=UU" 1),
   7.425 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.426 -        (resolve_tac prems 1),
   7.427 -        (eresolve_tac prems 1),
   7.428 -        (etac spec 1)
   7.429 -        ]);
   7.430 -*)
   7.431 -
   7.432 -qed_goal "dnat_finite_ind" Dnat.thy
   7.433 -"[|P(UU);P(dzero);\
   7.434 -\  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\
   7.435 -\  |] ==> !s.P(dnat_take n`s)"
   7.436 - (fn prems =>
   7.437 -        [
   7.438 -        (nat_ind_tac "n" 1),
   7.439 -        (simp_tac (!simpset addsimps dnat_rews) 1),
   7.440 -        (resolve_tac prems 1),
   7.441 -        (rtac allI 1),
   7.442 -        (res_inst_tac [("n","s")] dnatE 1),
   7.443 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.444 -        (resolve_tac prems 1),
   7.445 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.446 -        (resolve_tac prems 1),
   7.447 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.448 -        (case_tac "dnat_take n1`x=UU" 1),
   7.449 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.450 -        (resolve_tac prems 1),
   7.451 -        (resolve_tac prems 1),
   7.452 -        (atac 1),
   7.453 -        (etac spec 1)
   7.454 -        ]);
   7.455 -
   7.456 -qed_goal "dnat_all_finite_lemma1" Dnat.thy
   7.457 -"!s.dnat_take n`s=UU |dnat_take n`s=s"
   7.458 - (fn prems =>
   7.459 -        [
   7.460 -        (nat_ind_tac "n" 1),
   7.461 -        (simp_tac (!simpset addsimps dnat_rews) 1),
   7.462 -        (rtac allI 1),
   7.463 -        (res_inst_tac [("n","s")] dnatE 1),
   7.464 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.465 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.466 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.467 -        (eres_inst_tac [("x","x")] allE 1),
   7.468 -        (etac disjE 1),
   7.469 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.470 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1)
   7.471 -        ]);
   7.472 -
   7.473 -qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take n`s=s"
   7.474 - (fn prems =>
   7.475 -        [
   7.476 -        (case_tac "s=UU" 1),
   7.477 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.478 -        (subgoal_tac "(!n.dnat_take(n)`s=UU) |(? n.dnat_take(n)`s=s)" 1),
   7.479 -        (etac disjE 1),
   7.480 -        (eres_inst_tac [("P","s=UU")] notE 1),
   7.481 -        (rtac dnat_take_lemma 1),
   7.482 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.483 -        (atac 1),
   7.484 -        (subgoal_tac "!n.!s.dnat_take(n)`s=UU |dnat_take(n)`s=s" 1),
   7.485 -        (fast_tac HOL_cs 1),
   7.486 -        (rtac allI 1),
   7.487 -        (rtac dnat_all_finite_lemma1 1)
   7.488 -        ]);
   7.489 -
   7.490 -
   7.491 -qed_goal "dnat_ind" Dnat.thy
   7.492 -"[|P(UU);P(dzero);\
   7.493 -\  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc`s1)\
   7.494 -\  |] ==> P(s)"
   7.495 - (fn prems =>
   7.496 -        [
   7.497 -        (rtac (dnat_all_finite_lemma2 RS exE) 1),
   7.498 -        (etac subst 1),
   7.499 -        (rtac (dnat_finite_ind RS spec) 1),
   7.500 -        (REPEAT (resolve_tac prems 1)),
   7.501 -        (REPEAT (atac 1))
   7.502 -        ]);
   7.503 -
   7.504 -
   7.505 -qed_goalw "dnat_flat" Dnat.thy [flat_def] "flat(dzero)"
   7.506 - (fn prems =>
   7.507 -        [
   7.508 -        (rtac allI 1),
   7.509 -        (res_inst_tac [("s","x")] dnat_ind 1),
   7.510 -        (fast_tac HOL_cs 1),
   7.511 -        (rtac allI 1),
   7.512 -        (res_inst_tac [("n","y")] dnatE 1),
   7.513 -        (fast_tac (HOL_cs addSIs [UU_I]) 1),
   7.514 -        (Asm_simp_tac 1),
   7.515 -        (asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
   7.516 -        (rtac allI 1),
   7.517 -        (res_inst_tac [("n","y")] dnatE 1),
   7.518 -        (fast_tac (HOL_cs addSIs [UU_I]) 1),
   7.519 -        (asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
   7.520 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
   7.521 -        (strip_tac 1),
   7.522 -        (subgoal_tac "s1<<xa" 1),
   7.523 -        (etac allE 1),
   7.524 -        (dtac mp 1),
   7.525 -        (atac 1),
   7.526 -        (etac disjE 1),
   7.527 -        (contr_tac 1),
   7.528 -        (Asm_simp_tac 1),
   7.529 -        (resolve_tac  dnat_invert 1),
   7.530 -        (REPEAT (atac 1))
   7.531 -        ]);
   7.532 -
   7.533 -
   7.534 -
   7.535 -
   7.536 -
   7.537 -
     8.1 --- a/src/HOLCF/explicit_domains/Dnat.thy	Mon Feb 24 09:46:12 1997 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,112 +0,0 @@
     8.4 -(*  Title:      HOLCF/Dnat.thy
     8.5 -    ID:         $Id$
     8.6 -    Author:     Franz Regensburger
     8.7 -    Copyright   1993 Technische Universitaet Muenchen
     8.8 -
     8.9 -NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD.
    8.10 -
    8.11 -Theory for the domain of natural numbers  dnat = one ++ dnat
    8.12 -
    8.13 -The type is axiomatized as the least solution of the domain equation above.
    8.14 -The functor term that specifies the domain equation is: 
    8.15 -
    8.16 -  FT = <++,K_{one},I>
    8.17 -
    8.18 -For details see chapter 5 of:
    8.19 -
    8.20 -[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
    8.21 -                     Dissertation, Technische Universit"at M"unchen, 1994
    8.22 -
    8.23 -*)
    8.24 -
    8.25 -Dnat = HOLCF +
    8.26 -
    8.27 -types dnat 0
    8.28 -
    8.29 -(* ----------------------------------------------------------------------- *)
    8.30 -(* arrity axiom is valuated by semantical reasoning                        *)
    8.31 -
    8.32 -arities dnat::pcpo
    8.33 -
    8.34 -consts
    8.35 -
    8.36 -(* ----------------------------------------------------------------------- *)
    8.37 -(* essential constants                                                     *)
    8.38 -
    8.39 -dnat_rep        :: " dnat -> (one ++ dnat)"
    8.40 -dnat_abs        :: "(one ++ dnat) -> dnat"
    8.41 -
    8.42 -(* ----------------------------------------------------------------------- *)
    8.43 -(* abstract constants and auxiliary constants                              *)
    8.44 -
    8.45 -dnat_copy       :: "(dnat -> dnat) -> dnat -> dnat"
    8.46 -
    8.47 -dzero           :: "dnat"
    8.48 -dsucc           :: "dnat -> dnat"
    8.49 -dnat_when       :: "'b -> (dnat -> 'b) -> dnat -> 'b"
    8.50 -is_dzero        :: "dnat -> tr"
    8.51 -is_dsucc        :: "dnat -> tr"
    8.52 -dpred           :: "dnat -> dnat"
    8.53 -dnat_take       :: "nat => dnat -> dnat"
    8.54 -dnat_bisim      :: "(dnat => dnat => bool) => bool"
    8.55 -
    8.56 -rules
    8.57 -
    8.58 -(* ----------------------------------------------------------------------- *)
    8.59 -(* axiomatization of recursive type dnat                                   *)
    8.60 -(* ----------------------------------------------------------------------- *)
    8.61 -(* (dnat,dnat_abs) is the initial F-algebra where                          *)
    8.62 -(* F is the locally continuous functor determined by functor term FT.      *)
    8.63 -(* domain equation: dnat = one ++ dnat                                     *)
    8.64 -(* functor term:    FT = <++,K_{one},I>                                    *) 
    8.65 -(* ----------------------------------------------------------------------- *)
    8.66 -(* dnat_abs is an isomorphism with inverse dnat_rep                        *)
    8.67 -(* identity is the least endomorphism on dnat                              *)
    8.68 -
    8.69 -dnat_abs_iso    "dnat_rep`(dnat_abs`x) = x"
    8.70 -dnat_rep_iso    "dnat_abs`(dnat_rep`x) = x"
    8.71 -dnat_copy_def   "dnat_copy == (LAM f. dnat_abs oo 
    8.72 -                 (sswhen`sinl`(sinr oo f)) oo dnat_rep )"
    8.73 -dnat_reach      "(fix`dnat_copy)`x=x"
    8.74 -
    8.75 -
    8.76 -defs
    8.77 -(* ----------------------------------------------------------------------- *)
    8.78 -(* properties of additional constants                                      *)
    8.79 -(* ----------------------------------------------------------------------- *)
    8.80 -(* constructors                                                            *)
    8.81 -
    8.82 -dzero_def       "dzero == dnat_abs`(sinl`one)"
    8.83 -dsucc_def       "dsucc == (LAM n. dnat_abs`(sinr`n))"
    8.84 -
    8.85 -(* ----------------------------------------------------------------------- *)
    8.86 -(* discriminator functional                                                *)
    8.87 -
    8.88 -dnat_when_def   "dnat_when == (LAM f1 f2 n.sswhen`(LAM x.f1)`f2`(dnat_rep`n))"
    8.89 -
    8.90 -
    8.91 -(* ----------------------------------------------------------------------- *)
    8.92 -(* discriminators and selectors                                            *)
    8.93 -
    8.94 -is_dzero_def    "is_dzero == dnat_when`TT`(LAM x.FF)"
    8.95 -is_dsucc_def    "is_dsucc == dnat_when`FF`(LAM x.TT)"
    8.96 -dpred_def       "dpred == dnat_when`UU`(LAM x.x)"
    8.97 -
    8.98 -
    8.99 -(* ----------------------------------------------------------------------- *)
   8.100 -(* the taker for dnats                                                   *)
   8.101 -
   8.102 -dnat_take_def "dnat_take == (%n.iterate n dnat_copy UU)"
   8.103 -
   8.104 -(* ----------------------------------------------------------------------- *)
   8.105 -(* definition of bisimulation is determined by domain equation             *)
   8.106 -(* simplification and rewriting for abstract constants yields def below    *)
   8.107 -
   8.108 -dnat_bisim_def "dnat_bisim ==
   8.109 -(%R.!s1 s2.
   8.110 -        R s1 s2 -->
   8.111 -  ((s1=UU & s2=UU) |(s1=dzero & s2=dzero) |
   8.112 -  (? s11 s21. s11~=UU & s21~=UU & s1=dsucc`s11 &
   8.113 -                 s2 = dsucc`s21 & R s11 s21)))"
   8.114 -
   8.115 -end
     9.1 --- a/src/HOLCF/explicit_domains/Dnat2.ML	Mon Feb 24 09:46:12 1997 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,52 +0,0 @@
     9.4 -(*  Title:      HOLCF/Dnat2.ML
     9.5 -    ID:         $Id$
     9.6 -    Author:     Franz Regensburger
     9.7 -    Copyright   1993 Technische Universitaet Muenchen
     9.8 -
     9.9 -Lemmas for theory Dnat2.thy
    9.10 -*)
    9.11 -
    9.12 -open Dnat2;
    9.13 -
    9.14 -
    9.15 -(* ------------------------------------------------------------------------- *)
    9.16 -(* expand fixed point properties                                             *)
    9.17 -(* ------------------------------------------------------------------------- *)
    9.18 -
    9.19 -val iterator_def2 = fix_prover2 Dnat2.thy iterator_def 
    9.20 -        "iterator = (LAM n f x. dnat_when`x`(LAM m.f`(iterator`m`f`x)) `n)";
    9.21 -
    9.22 -(* ------------------------------------------------------------------------- *)
    9.23 -(* recursive  properties                                                     *)
    9.24 -(* ------------------------------------------------------------------------- *)
    9.25 -
    9.26 -qed_goal "iterator1" Dnat2.thy "iterator`UU`f`x = UU"
    9.27 - (fn prems =>
    9.28 -        [
    9.29 -        (stac iterator_def2 1),
    9.30 -        (simp_tac (!simpset addsimps dnat_when) 1)
    9.31 -        ]);
    9.32 -
    9.33 -qed_goal "iterator2" Dnat2.thy "iterator`dzero`f`x = x"
    9.34 - (fn prems =>
    9.35 -        [
    9.36 -        (stac iterator_def2 1),
    9.37 -        (simp_tac (!simpset addsimps dnat_when) 1)
    9.38 -        ]);
    9.39 -
    9.40 -qed_goal "iterator3" Dnat2.thy 
    9.41 -"n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)"
    9.42 - (fn prems =>
    9.43 -        [
    9.44 -        (cut_facts_tac prems 1),
    9.45 -        (rtac trans 1),
    9.46 -        (stac iterator_def2 1),
    9.47 -        (asm_simp_tac (!simpset addsimps dnat_rews) 1),
    9.48 -        (rtac refl 1)
    9.49 -        ]);
    9.50 -
    9.51 -val dnat2_rews = 
    9.52 -        [iterator1, iterator2, iterator3];
    9.53 -
    9.54 -
    9.55 -
    10.1 --- a/src/HOLCF/explicit_domains/Dnat2.thy	Mon Feb 24 09:46:12 1997 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,31 +0,0 @@
    10.4 -(*  Title:      HOLCF/Dnat2.thy
    10.5 -    ID:         $Id$
    10.6 -    Author:     Franz Regensburger
    10.7 -    Copyright   1993 Technische Universitaet Muenchen
    10.8 -
    10.9 -NOT SUPPORTED ANY MORE. USE HOLCF/ex/Dnat.thy INSTEAD.
   10.10 -
   10.11 -Additional constants for dnat
   10.12 -
   10.13 -*)
   10.14 -
   10.15 -Dnat2 = Dnat +
   10.16 -
   10.17 -consts
   10.18 -
   10.19 -iterator        :: "dnat -> ('a -> 'a) -> 'a -> 'a"
   10.20 -
   10.21 -
   10.22 -defs
   10.23 -
   10.24 -iterator_def    "iterator == fix`(LAM h n f x.
   10.25 -                        dnat_when `x `(LAM m.f`(h`m`f`x)) `n)"
   10.26 -end
   10.27 -
   10.28 -(*
   10.29 -
   10.30 -                iterator`UU`f`x = UU
   10.31 -                iterator`dzero`f`x = x
   10.32 -      n~=UU --> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)
   10.33 -*)
   10.34 -
    11.1 --- a/src/HOLCF/explicit_domains/README	Mon Feb 24 09:46:12 1997 +0100
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,22 +0,0 @@
    11.4 -(*
    11.5 -    ID:         $Id$
    11.6 -    Author: 	Franz Regensburger
    11.7 -    Copyright   1995 Technische Universitaet Muenchen
    11.8 -
    11.9 -*)
   11.10 -
   11.11 -The files contained in this directory are examples for the
   11.12 -explicit construction of domains. The technique used is described
   11.13 -in the thesis
   11.14 -
   11.15 -	HOLCF: Eine konservative Erweiterung von HOL um LCF
   11.16 -
   11.17 -The thesis is available via the web using URL
   11.18 -
   11.19 -	http://www4.informatik.tu-muenchen.de/~regensbu/papers.html
   11.20 -
   11.21 -
   11.22 -The same construction is automatically performed if you use the
   11.23 -type definition package of David Oheimb. See subdirectory HOLCF/domains
   11.24 -for more details.
   11.25 -
    12.1 --- a/src/HOLCF/explicit_domains/ROOT.ML	Mon Feb 24 09:46:12 1997 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,20 +0,0 @@
    12.4 -(*
    12.5 -    ID:         $Id$
    12.6 -    Author:     Franz Regensburger
    12.7 -    Copyright   1995 Technische Universitaet Muenchen
    12.8 -
    12.9 -*)
   12.10 -
   12.11 -HOLCF_build_completed;    (*Cause examples to fail if HOLCF did*)
   12.12 -
   12.13 -writeln"Root file for HOLCF examples: explicit domain axiomatisation";
   12.14 -proof_timing := true;
   12.15 -
   12.16 -time_use_thy "Dnat";
   12.17 -time_use_thy "Dnat2";
   12.18 -time_use_thy "Stream";
   12.19 -time_use_thy "Stream2";
   12.20 -time_use_thy "Dlist";
   12.21 -
   12.22 -OS.FileSys.chDir "..";
   12.23 -maketest "END: Root file for HOLCF examples: explicit domain axiomatization";
    13.1 --- a/src/HOLCF/explicit_domains/Stream.ML	Mon Feb 24 09:46:12 1997 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,838 +0,0 @@
    13.4 -(*  
    13.5 -    ID:         $Id$
    13.6 -    Author:     Franz Regensburger
    13.7 -    Copyright   1993 Technische Universitaet Muenchen
    13.8 -
    13.9 -Lemmas for stream.thy
   13.10 -*)
   13.11 -
   13.12 -open Stream;
   13.13 -
   13.14 -(* ------------------------------------------------------------------------*)
   13.15 -(* The isomorphisms stream_rep_iso and stream_abs_iso are strict           *)
   13.16 -(* ------------------------------------------------------------------------*)
   13.17 -
   13.18 -val stream_iso_strict= stream_rep_iso RS (stream_abs_iso RS 
   13.19 -        (allI  RSN (2,allI RS iso_strict)));
   13.20 -
   13.21 -val stream_rews = [stream_iso_strict RS conjunct1,
   13.22 -                stream_iso_strict RS conjunct2];
   13.23 -
   13.24 -(* ------------------------------------------------------------------------*)
   13.25 -(* Properties of stream_copy                                               *)
   13.26 -(* ------------------------------------------------------------------------*)
   13.27 -
   13.28 -fun prover defs thm =  prove_goalw Stream.thy defs thm
   13.29 - (fn prems =>
   13.30 -        [
   13.31 -        (cut_facts_tac prems 1),
   13.32 -        (asm_simp_tac (!simpset addsimps 
   13.33 -                (stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
   13.34 -        ]);
   13.35 -
   13.36 -val stream_copy = 
   13.37 -        [
   13.38 -        prover [stream_copy_def] "stream_copy`f`UU=UU",
   13.39 -        prover [stream_copy_def,scons_def] 
   13.40 -        "x~=UU ==> stream_copy`f`(scons`x`xs)= scons`x`(f`xs)"
   13.41 -        ];
   13.42 -
   13.43 -val stream_rews =  stream_copy @ stream_rews; 
   13.44 -
   13.45 -(* ------------------------------------------------------------------------*)
   13.46 -(* Exhaustion and elimination for streams                                  *)
   13.47 -(* ------------------------------------------------------------------------*)
   13.48 -
   13.49 -qed_goalw "Exh_stream" Stream.thy [scons_def]
   13.50 -        "s = UU | (? x xs. x~=UU & s = scons`x`xs)"
   13.51 - (fn prems =>
   13.52 -        [
   13.53 -        (Simp_tac 1),
   13.54 -        (rtac (stream_rep_iso RS subst) 1),
   13.55 -        (res_inst_tac [("p","stream_rep`s")] sprodE 1),
   13.56 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   13.57 -        (Asm_simp_tac  1),
   13.58 -        (res_inst_tac [("p","y")] upE1 1),
   13.59 -         (contr_tac 1),
   13.60 -        (rtac disjI2 1),
   13.61 -        (rtac exI 1),
   13.62 -        (etac conjI 1),
   13.63 -	(rtac exI 1),
   13.64 -        (Asm_simp_tac  1)
   13.65 -        ]);
   13.66 -
   13.67 -qed_goal "streamE" Stream.thy 
   13.68 -        "[| s=UU ==> Q; !!x xs.[|s=scons`x`xs;x~=UU|]==>Q|]==>Q"
   13.69 - (fn prems =>
   13.70 -        [
   13.71 -        (rtac (Exh_stream RS disjE) 1),
   13.72 -        (eresolve_tac prems 1),
   13.73 -        (etac exE 1),
   13.74 -        (etac exE 1),
   13.75 -        (resolve_tac prems 1),
   13.76 -        (fast_tac HOL_cs 1),
   13.77 -        (fast_tac HOL_cs 1)
   13.78 -        ]);
   13.79 -
   13.80 -(* ------------------------------------------------------------------------*)
   13.81 -(* Properties of stream_when                                               *)
   13.82 -(* ------------------------------------------------------------------------*)
   13.83 -
   13.84 -fun prover defs thm =  prove_goalw Stream.thy defs thm
   13.85 - (fn prems =>
   13.86 -        [
   13.87 -        (cut_facts_tac prems 1),
   13.88 -        (asm_simp_tac (!simpset addsimps 
   13.89 -                (stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
   13.90 -        ]);
   13.91 -
   13.92 -
   13.93 -val stream_when = [
   13.94 -        prover [stream_when_def] "stream_when`f`UU=UU",
   13.95 -        prover [stream_when_def,scons_def] 
   13.96 -                "x~=UU ==> stream_when`f`(scons`x`xs)= f`x`xs"
   13.97 -        ];
   13.98 -
   13.99 -val stream_rews = stream_when @ stream_rews;
  13.100 -
  13.101 -(* ------------------------------------------------------------------------*)
  13.102 -(* Rewrites for  discriminators and  selectors                             *)
  13.103 -(* ------------------------------------------------------------------------*)
  13.104 -
  13.105 -fun prover defs thm = prove_goalw Stream.thy defs thm
  13.106 - (fn prems =>
  13.107 -        [
  13.108 -        (simp_tac (!simpset addsimps stream_rews) 1)
  13.109 -        ]);
  13.110 -
  13.111 -val stream_discsel = [
  13.112 -        prover [is_scons_def] "is_scons`UU=UU",
  13.113 -        prover [shd_def] "shd`UU=UU",
  13.114 -        prover [stl_def] "stl`UU=UU"
  13.115 -        ];
  13.116 -
  13.117 -fun prover defs thm = prove_goalw Stream.thy defs thm
  13.118 - (fn prems =>
  13.119 -        [
  13.120 -        (cut_facts_tac prems 1),
  13.121 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
  13.122 -        ]);
  13.123 -
  13.124 -val stream_discsel = [
  13.125 -prover [is_scons_def,shd_def,stl_def] "x~=UU ==> is_scons`(scons`x`xs)=TT",
  13.126 -prover [is_scons_def,shd_def,stl_def] "x~=UU ==> shd`(scons`x`xs)=x",
  13.127 -prover [is_scons_def,shd_def,stl_def] "x~=UU ==> stl`(scons`x`xs)=xs"
  13.128 -        ] @ stream_discsel;
  13.129 -
  13.130 -val stream_rews = stream_discsel @ stream_rews;
  13.131 -
  13.132 -(* ------------------------------------------------------------------------*)
  13.133 -(* Definedness and strictness                                              *)
  13.134 -(* ------------------------------------------------------------------------*)
  13.135 -
  13.136 -fun prover contr thm = prove_goal Stream.thy thm
  13.137 - (fn prems =>
  13.138 -        [
  13.139 -        (res_inst_tac [("P1",contr)] classical2 1),
  13.140 -        (simp_tac (!simpset addsimps stream_rews) 1),
  13.141 -        (dtac sym 1),
  13.142 -        (Asm_simp_tac 1),
  13.143 -        (simp_tac (!simpset addsimps (prems @ stream_rews)) 1)
  13.144 -        ]);
  13.145 -
  13.146 -val stream_constrdef = [
  13.147 -        prover "is_scons`(UU::'a stream)~=UU" "x~=UU ==> scons`(x::'a)`xs~=UU"
  13.148 -        ]; 
  13.149 -
  13.150 -fun prover defs thm = prove_goalw Stream.thy defs thm
  13.151 - (fn prems =>
  13.152 -        [
  13.153 -        (simp_tac (!simpset addsimps stream_rews) 1)
  13.154 -        ]);
  13.155 -
  13.156 -val stream_constrdef = [
  13.157 -        prover [scons_def] "scons`UU`xs=UU"
  13.158 -        ] @ stream_constrdef;
  13.159 -
  13.160 -val stream_rews = stream_constrdef @ stream_rews;
  13.161 -
  13.162 -
  13.163 -(* ------------------------------------------------------------------------*)
  13.164 -(* Distinctness wrt. << and =                                              *)
  13.165 -(* ------------------------------------------------------------------------*)
  13.166 -
  13.167 -
  13.168 -(* ------------------------------------------------------------------------*)
  13.169 -(* Invertibility                                                           *)
  13.170 -(* ------------------------------------------------------------------------*)
  13.171 -
  13.172 -val stream_invert =
  13.173 -        [
  13.174 -prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
  13.175 -\ scons`x1`x2 << scons`y1`y2|] ==> x1<< y1 & x2 << y2"
  13.176 - (fn prems =>
  13.177 -        [
  13.178 -        (cut_facts_tac prems 1),
  13.179 -        (rtac conjI 1),
  13.180 -        (dres_inst_tac [("fo","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
  13.181 -        (etac box_less 1),
  13.182 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
  13.183 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
  13.184 -        (dres_inst_tac [("fo","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
  13.185 -        (etac box_less 1),
  13.186 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
  13.187 -        (asm_simp_tac (!simpset addsimps stream_when) 1)
  13.188 -        ])
  13.189 -        ];
  13.190 -
  13.191 -(* ------------------------------------------------------------------------*)
  13.192 -(* Injectivity                                                             *)
  13.193 -(* ------------------------------------------------------------------------*)
  13.194 -
  13.195 -val stream_inject = 
  13.196 -        [
  13.197 -prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
  13.198 -\ scons`x1`x2 = scons`y1`y2 |] ==> x1= y1 & x2 = y2"
  13.199 - (fn prems =>
  13.200 -        [
  13.201 -        (cut_facts_tac prems 1),
  13.202 -        (rtac conjI 1),
  13.203 -        (dres_inst_tac [("f","stream_when`(LAM x l.x)")] cfun_arg_cong 1),
  13.204 -        (etac box_equals 1),
  13.205 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
  13.206 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
  13.207 -        (dres_inst_tac [("f","stream_when`(LAM x l.l)")] cfun_arg_cong 1),
  13.208 -        (etac box_equals 1),
  13.209 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
  13.210 -        (asm_simp_tac (!simpset addsimps stream_when) 1)
  13.211 -        ])
  13.212 -        ];
  13.213 -
  13.214 -(* ------------------------------------------------------------------------*)
  13.215 -(* definedness for  discriminators and  selectors                          *)
  13.216 -(* ------------------------------------------------------------------------*)
  13.217 -
  13.218 -fun prover thm = prove_goal Stream.thy thm
  13.219 - (fn prems =>
  13.220 -        [
  13.221 -        (cut_facts_tac prems 1),
  13.222 -        (rtac streamE 1),
  13.223 -        (contr_tac 1),
  13.224 -        (REPEAT (asm_simp_tac (!simpset addsimps stream_discsel) 1))
  13.225 -        ]);
  13.226 -
  13.227 -val stream_discsel_def = 
  13.228 -        [
  13.229 -        prover "s~=UU ==> is_scons`s ~= UU", 
  13.230 -        prover "s~=UU ==> shd`s ~=UU" 
  13.231 -        ];
  13.232 -
  13.233 -val stream_rews = stream_discsel_def @ stream_rews;
  13.234 -
  13.235 -
  13.236 -(* ------------------------------------------------------------------------*)
  13.237 -(* Properties stream_take                                                  *)
  13.238 -(* ------------------------------------------------------------------------*)
  13.239 -
  13.240 -val stream_take =
  13.241 -        [
  13.242 -prove_goalw Stream.thy [stream_take_def] "stream_take n`UU = UU"
  13.243 - (fn prems =>
  13.244 -        [
  13.245 -        (res_inst_tac [("n","n")] natE 1),
  13.246 -        (Asm_simp_tac 1),
  13.247 -        (Asm_simp_tac 1),
  13.248 -        (simp_tac (!simpset addsimps stream_rews) 1)
  13.249 -        ]),
  13.250 -prove_goalw Stream.thy [stream_take_def] "stream_take 0`xs=UU"
  13.251 - (fn prems =>
  13.252 -        [
  13.253 -        (Asm_simp_tac 1)
  13.254 -        ])];
  13.255 -
  13.256 -fun prover thm = prove_goalw Stream.thy [stream_take_def] thm
  13.257 - (fn prems =>
  13.258 -        [
  13.259 -        (cut_facts_tac prems 1),
  13.260 -        (Simp_tac 1),
  13.261 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
  13.262 -        ]);
  13.263 -
  13.264 -val stream_take = [
  13.265 -prover 
  13.266 -  "x~=UU ==> stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
  13.267 -        ] @ stream_take;
  13.268 -
  13.269 -val stream_rews = stream_take @ stream_rews;
  13.270 -
  13.271 -(* ------------------------------------------------------------------------*)
  13.272 -(* enhance the simplifier                                                  *)
  13.273 -(* ------------------------------------------------------------------------*)
  13.274 -
  13.275 -qed_goal "stream_copy2" Stream.thy 
  13.276 -     "stream_copy`f`(scons`x`xs) = scons`x`(f`xs)"
  13.277 - (fn prems =>
  13.278 -        [
  13.279 -        (case_tac "x=UU" 1),
  13.280 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.281 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
  13.282 -        ]);
  13.283 -
  13.284 -qed_goal "shd2" Stream.thy "shd`(scons`x`xs) = x"
  13.285 - (fn prems =>
  13.286 -        [
  13.287 -        (case_tac "x=UU" 1),
  13.288 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.289 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
  13.290 -        ]);
  13.291 -
  13.292 -qed_goal "stream_take2" Stream.thy 
  13.293 - "stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
  13.294 - (fn prems =>
  13.295 -        [
  13.296 -        (case_tac "x=UU" 1),
  13.297 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.298 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
  13.299 -        ]);
  13.300 -
  13.301 -val stream_rews = [stream_iso_strict RS conjunct1,
  13.302 -                   stream_iso_strict RS conjunct2,
  13.303 -                   hd stream_copy, stream_copy2]
  13.304 -                  @ stream_when
  13.305 -                  @ [hd stream_discsel,shd2] @ (tl (tl stream_discsel))  
  13.306 -                  @ stream_constrdef
  13.307 -                  @ stream_discsel_def
  13.308 -                  @ [ stream_take2] @ (tl stream_take);
  13.309 -
  13.310 -
  13.311 -(* ------------------------------------------------------------------------*)
  13.312 -(* take lemma for streams                                                  *)
  13.313 -(* ------------------------------------------------------------------------*)
  13.314 -
  13.315 -fun prover reach defs thm  = prove_goalw Stream.thy defs thm
  13.316 - (fn prems =>
  13.317 -        [
  13.318 -        (res_inst_tac [("t","s1")] (reach RS subst) 1),
  13.319 -        (res_inst_tac [("t","s2")] (reach RS subst) 1),
  13.320 -        (stac fix_def2 1),
  13.321 -        (stac contlub_cfun_fun 1),
  13.322 -        (rtac is_chain_iterate 1),
  13.323 -        (stac contlub_cfun_fun 1),
  13.324 -        (rtac is_chain_iterate 1),
  13.325 -        (rtac lub_equal 1),
  13.326 -        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
  13.327 -        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
  13.328 -        (rtac allI 1),
  13.329 -        (resolve_tac prems 1)
  13.330 -        ]);
  13.331 -
  13.332 -val stream_take_lemma = prover stream_reach  [stream_take_def]
  13.333 -        "(!!n.stream_take n`s1 = stream_take n`s2) ==> s1=s2";
  13.334 -
  13.335 -
  13.336 -qed_goal "stream_reach2" Stream.thy  "lub(range(%i.stream_take i`s))=s"
  13.337 - (fn prems =>
  13.338 -        [
  13.339 -        (res_inst_tac [("t","s")] (stream_reach RS subst) 1),
  13.340 -        (stac fix_def2 1),
  13.341 -        (rewtac stream_take_def),
  13.342 -        (stac contlub_cfun_fun 1),
  13.343 -        (rtac is_chain_iterate 1),
  13.344 -        (rtac refl 1)
  13.345 -        ]);
  13.346 -
  13.347 -(* ------------------------------------------------------------------------*)
  13.348 -(* Co -induction for streams                                               *)
  13.349 -(* ------------------------------------------------------------------------*)
  13.350 -
  13.351 -qed_goalw "stream_coind_lemma" Stream.thy [stream_bisim_def] 
  13.352 -"stream_bisim R ==> ! p q. R p q --> stream_take n`p = stream_take n`q"
  13.353 - (fn prems =>
  13.354 -        [
  13.355 -        (cut_facts_tac prems 1),
  13.356 -        (nat_ind_tac "n" 1),
  13.357 -        (simp_tac (!simpset addsimps stream_rews) 1),
  13.358 -        (strip_tac 1),
  13.359 -        ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
  13.360 -        (atac 1),
  13.361 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.362 -        (etac exE 1),
  13.363 -        (etac exE 1),
  13.364 -        (etac exE 1),
  13.365 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.366 -        (REPEAT (etac conjE 1)),
  13.367 -        (rtac cfun_arg_cong 1),
  13.368 -        (fast_tac HOL_cs 1)
  13.369 -        ]);
  13.370 -
  13.371 -qed_goal "stream_coind" Stream.thy "[|stream_bisim R ;R p q|] ==> p = q"
  13.372 - (fn prems =>
  13.373 -        [
  13.374 -        (rtac stream_take_lemma 1),
  13.375 -        (rtac (stream_coind_lemma RS spec RS spec RS mp) 1),
  13.376 -        (resolve_tac prems 1),
  13.377 -        (resolve_tac prems 1)
  13.378 -        ]);
  13.379 -
  13.380 -(* ------------------------------------------------------------------------*)
  13.381 -(* structural induction for admissible predicates                          *)
  13.382 -(* ------------------------------------------------------------------------*)
  13.383 -
  13.384 -qed_goal "stream_finite_ind" Stream.thy
  13.385 -"[|P(UU);\
  13.386 -\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
  13.387 -\  |] ==> !s.P(stream_take n`s)"
  13.388 - (fn prems =>
  13.389 -        [
  13.390 -        (nat_ind_tac "n" 1),
  13.391 -        (simp_tac (!simpset addsimps stream_rews) 1),
  13.392 -        (resolve_tac prems 1),
  13.393 -        (rtac allI 1),
  13.394 -        (res_inst_tac [("s","s")] streamE 1),
  13.395 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.396 -        (resolve_tac prems 1),
  13.397 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.398 -        (resolve_tac prems 1),
  13.399 -        (atac 1),
  13.400 -        (etac spec 1)
  13.401 -        ]);
  13.402 -
  13.403 -qed_goalw "stream_finite_ind2" Stream.thy  [stream_finite_def]
  13.404 -"(!!n.P(stream_take n`s)) ==>  stream_finite(s) -->P(s)"
  13.405 - (fn prems =>
  13.406 -        [
  13.407 -        (strip_tac 1),
  13.408 -        (etac exE 1),
  13.409 -        (etac subst 1),
  13.410 -        (resolve_tac prems 1)
  13.411 -        ]);
  13.412 -
  13.413 -qed_goal "stream_finite_ind3" Stream.thy 
  13.414 -"[|P(UU);\
  13.415 -\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
  13.416 -\  |] ==> stream_finite(s) --> P(s)"
  13.417 - (fn prems =>
  13.418 -        [
  13.419 -        (rtac stream_finite_ind2 1),
  13.420 -        (rtac (stream_finite_ind RS spec) 1),
  13.421 -        (REPEAT (resolve_tac prems 1)),
  13.422 -        (REPEAT (atac 1))
  13.423 -        ]);
  13.424 -
  13.425 -(* prove induction using definition of admissibility 
  13.426 -   stream_reach rsp. stream_reach2 
  13.427 -   and finite induction stream_finite_ind *)
  13.428 -
  13.429 -qed_goal "stream_ind" Stream.thy
  13.430 -"[|adm(P);\
  13.431 -\  P(UU);\
  13.432 -\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
  13.433 -\  |] ==> P(s)"
  13.434 - (fn prems =>
  13.435 -        [
  13.436 -        (rtac (stream_reach2 RS subst) 1),
  13.437 -        (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
  13.438 -        (resolve_tac prems 1),
  13.439 -        (SELECT_GOAL (rewtac stream_take_def) 1),
  13.440 -        (rtac ch2ch_fappL 1),
  13.441 -        (rtac is_chain_iterate 1),
  13.442 -        (rtac allI 1),
  13.443 -        (rtac (stream_finite_ind RS spec) 1),
  13.444 -        (REPEAT (resolve_tac prems 1)),
  13.445 -        (REPEAT (atac 1))
  13.446 -        ]);
  13.447 -
  13.448 -(* prove induction with usual LCF-Method using fixed point induction *)
  13.449 -qed_goal "stream_ind" Stream.thy
  13.450 -"[|adm(P);\
  13.451 -\  P(UU);\
  13.452 -\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
  13.453 -\  |] ==> P(s)"
  13.454 - (fn prems =>
  13.455 -        [
  13.456 -        (rtac (stream_reach RS subst) 1),
  13.457 -        (res_inst_tac [("x","s")] spec 1),
  13.458 -        (rtac wfix_ind 1),
  13.459 -        (rtac adm_impl_admw 1),
  13.460 -        (REPEAT (resolve_tac adm_thms 1)),
  13.461 -        (rtac adm_subst 1),
  13.462 -        (cont_tacR 1),
  13.463 -        (resolve_tac prems 1),
  13.464 -        (rtac allI 1),
  13.465 -        (rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
  13.466 -        (REPEAT (resolve_tac prems 1)),
  13.467 -        (REPEAT (atac 1))
  13.468 -        ]);
  13.469 -
  13.470 -
  13.471 -(* ------------------------------------------------------------------------*)
  13.472 -(* simplify use of Co-induction                                            *)
  13.473 -(* ------------------------------------------------------------------------*)
  13.474 -
  13.475 -qed_goal "surjectiv_scons" Stream.thy "scons`(shd`s)`(stl`s)=s"
  13.476 - (fn prems =>
  13.477 -        [
  13.478 -        (res_inst_tac [("s","s")] streamE 1),
  13.479 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.480 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
  13.481 -        ]);
  13.482 -
  13.483 -
  13.484 -qed_goalw "stream_coind_lemma2" Stream.thy [stream_bisim_def]
  13.485 -"!s1 s2. R s1 s2 --> shd`s1 = shd`s2 & R (stl`s1) (stl`s2) ==> stream_bisim R"
  13.486 - (fn prems =>
  13.487 -        [
  13.488 -        (cut_facts_tac prems 1),
  13.489 -        (strip_tac 1),
  13.490 -        (etac allE 1),
  13.491 -        (etac allE 1),
  13.492 -        (dtac mp 1),
  13.493 -        (atac 1),
  13.494 -        (etac conjE 1),
  13.495 -        (case_tac "s1 = UU & s2 = UU" 1),
  13.496 -        (rtac disjI1 1),
  13.497 -        (fast_tac HOL_cs 1),
  13.498 -        (rtac disjI2 1),
  13.499 -        (rtac disjE 1),
  13.500 -        (etac (de_Morgan_conj RS subst) 1),
  13.501 -        (res_inst_tac [("x","shd`s1")] exI 1),
  13.502 -        (res_inst_tac [("x","stl`s1")] exI 1),
  13.503 -        (res_inst_tac [("x","stl`s2")] exI 1),
  13.504 -        (rtac conjI 1),
  13.505 -        (eresolve_tac stream_discsel_def 1),
  13.506 -        (asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
  13.507 -        (eres_inst_tac [("s","shd`s1"),("t","shd`s2")] subst 1),
  13.508 -        (simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
  13.509 -        (res_inst_tac [("x","shd`s2")] exI 1),
  13.510 -        (res_inst_tac [("x","stl`s1")] exI 1),
  13.511 -        (res_inst_tac [("x","stl`s2")] exI 1),
  13.512 -        (rtac conjI 1),
  13.513 -        (eresolve_tac stream_discsel_def 1),
  13.514 -        (asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
  13.515 -        (res_inst_tac [("s","shd`s1"),("t","shd`s2")] ssubst 1),
  13.516 -        (etac sym 1),
  13.517 -        (simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1)
  13.518 -        ]);
  13.519 -
  13.520 -
  13.521 -(* ------------------------------------------------------------------------*)
  13.522 -(* theorems about finite and infinite streams                              *)
  13.523 -(* ------------------------------------------------------------------------*)
  13.524 -
  13.525 -(* ----------------------------------------------------------------------- *)
  13.526 -(* 2 lemmas about stream_finite                                            *)
  13.527 -(* ----------------------------------------------------------------------- *)
  13.528 -
  13.529 -qed_goalw "stream_finite_UU" Stream.thy [stream_finite_def]
  13.530 -         "stream_finite(UU)"
  13.531 - (fn prems =>
  13.532 -        [
  13.533 -        (rtac exI 1),
  13.534 -        (simp_tac (!simpset addsimps stream_rews) 1)
  13.535 -        ]);
  13.536 -
  13.537 -qed_goal "inf_stream_not_UU" Stream.thy  "~stream_finite(s)  ==> s ~= UU"
  13.538 - (fn prems =>
  13.539 -        [
  13.540 -        (cut_facts_tac prems 1),
  13.541 -        (etac swap 1),
  13.542 -        (dtac notnotD 1),
  13.543 -        (hyp_subst_tac  1),
  13.544 -        (rtac stream_finite_UU 1)
  13.545 -        ]);
  13.546 -
  13.547 -(* ----------------------------------------------------------------------- *)
  13.548 -(* a lemma about shd                                                       *)
  13.549 -(* ----------------------------------------------------------------------- *)
  13.550 -
  13.551 -qed_goal "stream_shd_lemma1" Stream.thy "shd`s=UU --> s=UU"
  13.552 - (fn prems =>
  13.553 -        [
  13.554 -        (res_inst_tac [("s","s")] streamE 1),
  13.555 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.556 -        (hyp_subst_tac 1),
  13.557 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
  13.558 -        ]);
  13.559 -
  13.560 -
  13.561 -(* ----------------------------------------------------------------------- *)
  13.562 -(* lemmas about stream_take                                                *)
  13.563 -(* ----------------------------------------------------------------------- *)
  13.564 -
  13.565 -qed_goal "stream_take_lemma1" Stream.thy 
  13.566 - "!x xs.x~=UU --> \
  13.567 -\  stream_take (Suc n)`(scons`x`xs) = scons`x`xs --> stream_take n`xs=xs"
  13.568 - (fn prems =>
  13.569 -        [
  13.570 -        (rtac allI 1),
  13.571 -        (rtac allI 1),
  13.572 -        (rtac impI 1),
  13.573 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.574 -        (strip_tac 1),
  13.575 -        (rtac ((hd stream_inject) RS conjunct2) 1),
  13.576 -        (atac 1),
  13.577 -        (atac 1),
  13.578 -        (atac 1)
  13.579 -        ]);
  13.580 -
  13.581 -
  13.582 -qed_goal "stream_take_lemma2" Stream.thy 
  13.583 - "! s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2"
  13.584 - (fn prems =>
  13.585 -        [
  13.586 -        (nat_ind_tac "n" 1),
  13.587 -        (simp_tac (!simpset addsimps stream_rews) 1),
  13.588 -        (strip_tac 1),
  13.589 -        (res_inst_tac [("s","s2")] streamE 1),
  13.590 -         (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.591 -	(hyp_subst_tac 1),
  13.592 -	(rotate_tac ~1 1),
  13.593 -        (asm_full_simp_tac (!simpset addsimps stream_rews) 1),
  13.594 -        (subgoal_tac "stream_take n1`xs = xs" 1),
  13.595 -         (rtac ((hd stream_inject) RS conjunct2) 2),
  13.596 -           (atac 4),
  13.597 -          (atac 2),
  13.598 -         (atac 2),
  13.599 -        (rtac cfun_arg_cong 1),
  13.600 -        (fast_tac HOL_cs 1)
  13.601 -        ]);
  13.602 -
  13.603 -qed_goal "stream_take_lemma3" Stream.thy 
  13.604 - "!x xs.x~=UU --> \
  13.605 -\  stream_take n`(scons`x`xs) = scons`x`xs --> stream_take n`xs=xs"
  13.606 - (fn prems =>
  13.607 -        [
  13.608 -        (nat_ind_tac "n" 1),
  13.609 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.610 -        (strip_tac 1 ),
  13.611 -        (res_inst_tac [("P","scons`x`xs=UU")] notE 1),
  13.612 -        (eresolve_tac stream_constrdef 1),
  13.613 -        (etac sym 1),
  13.614 -        (strip_tac 1 ),
  13.615 -        (rtac (stream_take_lemma2 RS spec RS mp) 1),
  13.616 -        (res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
  13.617 -        (atac 1),
  13.618 -        (atac 1),
  13.619 -        (etac (stream_take2 RS subst) 1)
  13.620 -        ]);
  13.621 -
  13.622 -qed_goal "stream_take_lemma4" Stream.thy 
  13.623 - "!x xs.\
  13.624 -\stream_take n`xs=xs --> stream_take (Suc n)`(scons`x`xs) = scons`x`xs"
  13.625 - (fn prems =>
  13.626 -        [
  13.627 -        (nat_ind_tac "n" 1),
  13.628 -        (simp_tac (!simpset addsimps stream_rews) 1),
  13.629 -        (simp_tac (!simpset addsimps stream_rews) 1)
  13.630 -        ]);
  13.631 -
  13.632 -(* ---- *)
  13.633 -
  13.634 -qed_goal "stream_take_lemma5" Stream.thy 
  13.635 -"!s. stream_take n`s=s --> iterate n stl s=UU"
  13.636 - (fn prems =>
  13.637 -        [
  13.638 -        (nat_ind_tac "n" 1),
  13.639 -        (Simp_tac 1),
  13.640 -        (simp_tac (!simpset addsimps stream_rews) 1),
  13.641 -        (strip_tac 1),
  13.642 -        (res_inst_tac [("s","s")] streamE 1),
  13.643 -        (hyp_subst_tac 1),
  13.644 -        (stac iterate_Suc2 1),
  13.645 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.646 -        (stac iterate_Suc2 1),
  13.647 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.648 -        (etac allE 1),
  13.649 -        (etac mp 1),
  13.650 -        (hyp_subst_tac 1),
  13.651 -        (etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
  13.652 -        (atac 1)
  13.653 -        ]);
  13.654 -
  13.655 -qed_goal "stream_take_lemma6" Stream.thy 
  13.656 -"!s.iterate n stl s =UU --> stream_take n`s=s"
  13.657 - (fn prems =>
  13.658 -        [
  13.659 -        (nat_ind_tac "n" 1),
  13.660 -        (Simp_tac 1),
  13.661 -        (strip_tac 1),
  13.662 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.663 -        (rtac allI 1),
  13.664 -        (res_inst_tac [("s","s")] streamE 1),
  13.665 -        (hyp_subst_tac 1),
  13.666 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
  13.667 -        (hyp_subst_tac 1),
  13.668 -        (stac iterate_Suc2 1),
  13.669 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
  13.670 -        ]);
  13.671 -
  13.672 -qed_goal "stream_take_lemma7" Stream.thy 
  13.673 -"(iterate n stl s=UU) = (stream_take n`s=s)"
  13.674 - (fn prems =>
  13.675 -        [
  13.676 -        (rtac iffI 1),
  13.677 -        (etac (stream_take_lemma6 RS spec RS mp) 1),
  13.678 -        (etac (stream_take_lemma5 RS spec RS mp) 1)
  13.679 -        ]);
  13.680 -
  13.681 -
  13.682 -qed_goal "stream_take_lemma8" Stream.thy
  13.683 -"[|adm(P); !n. ? m. n < m & P (stream_take m`s)|] ==> P(s)"
  13.684 - (fn prems =>
  13.685 -        [
  13.686 -        (cut_facts_tac prems 1),
  13.687 -        (rtac (stream_reach2 RS subst) 1),
  13.688 -        (rtac adm_lemma11 1),
  13.689 -        (atac 1),
  13.690 -        (atac 2),
  13.691 -        (rewtac stream_take_def),
  13.692 -        (rtac ch2ch_fappL 1),
  13.693 -        (rtac is_chain_iterate 1)
  13.694 -        ]);
  13.695 -
  13.696 -(* ----------------------------------------------------------------------- *)
  13.697 -(* lemmas stream_finite                                                    *)
  13.698 -(* ----------------------------------------------------------------------- *)
  13.699 -
  13.700 -qed_goalw "stream_finite_lemma1" Stream.thy [stream_finite_def]
  13.701 - "stream_finite(xs) ==> stream_finite(scons`x`xs)"
  13.702 - (fn prems =>
  13.703 -        [
  13.704 -        (cut_facts_tac prems 1),
  13.705 -        (etac exE 1),
  13.706 -        (rtac exI 1),
  13.707 -        (etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
  13.708 -        ]);
  13.709 -
  13.710 -qed_goalw "stream_finite_lemma2" Stream.thy [stream_finite_def]
  13.711 - "[|x~=UU; stream_finite(scons`x`xs)|] ==> stream_finite(xs)"
  13.712 - (fn prems =>
  13.713 -        [
  13.714 -        (cut_facts_tac prems 1),
  13.715 -        (etac exE 1),
  13.716 -        (rtac exI 1),
  13.717 -        (etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
  13.718 -        (atac 1)
  13.719 -        ]);
  13.720 -
  13.721 -qed_goal "stream_finite_lemma3" Stream.thy 
  13.722 - "x~=UU ==> stream_finite(scons`x`xs) = stream_finite(xs)"
  13.723 - (fn prems =>
  13.724 -        [
  13.725 -        (cut_facts_tac prems 1),
  13.726 -        (rtac iffI 1),
  13.727 -        (etac stream_finite_lemma2 1),
  13.728 -        (atac 1),
  13.729 -        (etac stream_finite_lemma1 1)
  13.730 -        ]);
  13.731 -
  13.732 -
  13.733 -qed_goalw "stream_finite_lemma5" Stream.thy [stream_finite_def]
  13.734 - "(!n. s1 << s2  --> stream_take n`s2 = s2 --> stream_finite(s1))\
  13.735 -\=(s1 << s2  --> stream_finite(s2) --> stream_finite(s1))"
  13.736 - (fn prems =>
  13.737 -        [
  13.738 -        (rtac iffI 1),
  13.739 -        (fast_tac HOL_cs 1),
  13.740 -        (fast_tac HOL_cs 1)
  13.741 -        ]);
  13.742 -
  13.743 -qed_goal "stream_finite_lemma6" Stream.thy
  13.744 - "!s1 s2. s1 << s2  --> stream_take n`s2 = s2 --> stream_finite(s1)"
  13.745 - (fn prems =>
  13.746 -        [
  13.747 -        (nat_ind_tac "n" 1),
  13.748 -        (simp_tac (!simpset addsimps stream_rews) 1),
  13.749 -        (strip_tac 1 ),
  13.750 -        (hyp_subst_tac  1),
  13.751 -        (dtac UU_I 1),
  13.752 -        (hyp_subst_tac  1),
  13.753 -        (rtac stream_finite_UU 1),
  13.754 -        (rtac allI 1),
  13.755 -        (rtac allI 1),
  13.756 -        (res_inst_tac [("s","s1")] streamE 1),
  13.757 -        (hyp_subst_tac  1),
  13.758 -        (strip_tac 1 ),
  13.759 -        (rtac stream_finite_UU 1),
  13.760 -        (hyp_subst_tac  1),
  13.761 -        (res_inst_tac [("s","s2")] streamE 1),
  13.762 -        (hyp_subst_tac  1),
  13.763 -        (strip_tac 1 ),
  13.764 -        (dtac UU_I 1),
  13.765 -        (asm_simp_tac(!simpset addsimps (stream_rews @ [stream_finite_UU])) 1),
  13.766 -        (hyp_subst_tac  1),
  13.767 -        (simp_tac (!simpset addsimps stream_rews) 1),
  13.768 -        (strip_tac 1 ),
  13.769 -        (rtac stream_finite_lemma1 1),
  13.770 -        (subgoal_tac "xs << xsa" 1),
  13.771 -        (subgoal_tac "stream_take n1`xsa = xsa" 1),
  13.772 -        (fast_tac HOL_cs 1),
  13.773 -        (res_inst_tac  [("x1.1","xa"),("y1.1","xa")] 
  13.774 -                   ((hd stream_inject) RS conjunct2) 1),
  13.775 -        (atac 1),
  13.776 -        (atac 1),
  13.777 -        (atac 1),
  13.778 -        (res_inst_tac [("x1.1","x"),("y1.1","xa")]
  13.779 -         ((hd stream_invert) RS conjunct2) 1),
  13.780 -        (atac 1),
  13.781 -        (atac 1),
  13.782 -        (atac 1)
  13.783 -        ]);
  13.784 -
  13.785 -qed_goal "stream_finite_lemma7" Stream.thy 
  13.786 -"s1 << s2  --> stream_finite(s2) --> stream_finite(s1)"
  13.787 - (fn prems =>
  13.788 -        [
  13.789 -        (rtac (stream_finite_lemma5 RS iffD1) 1),
  13.790 -        (rtac allI 1),
  13.791 -        (rtac (stream_finite_lemma6 RS spec RS spec) 1)
  13.792 -        ]);
  13.793 -
  13.794 -qed_goalw "stream_finite_lemma8" Stream.thy [stream_finite_def]
  13.795 -"stream_finite(s) = (? n. iterate n stl s = UU)"
  13.796 - (fn prems =>
  13.797 -        [
  13.798 -        (simp_tac (!simpset addsimps [stream_take_lemma7]) 1)
  13.799 -        ]);
  13.800 -
  13.801 -
  13.802 -(* ----------------------------------------------------------------------- *)
  13.803 -(* admissibility of ~stream_finite                                         *)
  13.804 -(* ----------------------------------------------------------------------- *)
  13.805 -
  13.806 -qed_goalw "adm_not_stream_finite" Stream.thy [adm_def]
  13.807 - "adm(%s. ~ stream_finite(s))"
  13.808 - (fn prems =>
  13.809 -        [
  13.810 -        (strip_tac 1 ),
  13.811 -        (res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical2 1),
  13.812 -        (atac 2),
  13.813 -        (subgoal_tac "!i.stream_finite(Y(i))" 1),
  13.814 -        (fast_tac HOL_cs 1),
  13.815 -        (rtac allI 1),
  13.816 -        (rtac (stream_finite_lemma7 RS mp RS mp) 1),
  13.817 -        (etac is_ub_thelub 1),
  13.818 -        (atac 1)
  13.819 -        ]);
  13.820 -
  13.821 -(* ----------------------------------------------------------------------- *)
  13.822 -(* alternative prove for admissibility of ~stream_finite                   *)
  13.823 -(* show that stream_finite(s) = (? n. iterate n stl s = UU)                *)
  13.824 -(* and prove adm. of ~(? n. iterate n stl s = UU)                          *)
  13.825 -(* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8          *)
  13.826 -(* ----------------------------------------------------------------------- *)
  13.827 -
  13.828 -
  13.829 -qed_goal "adm_not_stream_finite" Stream.thy "adm(%s. ~ stream_finite(s))"
  13.830 - (fn prems =>
  13.831 -        [
  13.832 -        (subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate n stl s ~=UU))" 1),
  13.833 -        (etac (adm_cong RS iffD2)1),
  13.834 -        (REPEAT(resolve_tac adm_thms 1)),
  13.835 -        (rtac  cont_iterate2 1),
  13.836 -        (rtac allI 1),
  13.837 -        (stac stream_finite_lemma8 1),
  13.838 -        (fast_tac HOL_cs 1)
  13.839 -        ]);
  13.840 -
  13.841 -
    14.1 --- a/src/HOLCF/explicit_domains/Stream.thy	Mon Feb 24 09:46:12 1997 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,117 +0,0 @@
    14.4 -(* 
    14.5 -    ID:         $Id$
    14.6 -    Author:     Franz Regensburger
    14.7 -    Copyright   1993 Technische Universitaet Muenchen
    14.8 -
    14.9 -NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD.
   14.10 -
   14.11 -Theory for streams without defined empty stream 
   14.12 -  'a stream = 'a ** ('a stream)u
   14.13 -
   14.14 -The type is axiomatized as the least solution of the domain equation above.
   14.15 -The functor term that specifies the domain equation is: 
   14.16 -
   14.17 -  FT = <**,K_{'a},U>
   14.18 -
   14.19 -For details see chapter 5 of:
   14.20 -
   14.21 -[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
   14.22 -                     Dissertation, Technische Universit"at M"unchen, 1994
   14.23 -*)
   14.24 -
   14.25 -Stream = Dnat2 +
   14.26 -
   14.27 -types stream 1
   14.28 -
   14.29 -(* ----------------------------------------------------------------------- *)
   14.30 -(* arity axiom is validated by semantic reasoning                          *)
   14.31 -(* partial ordering is implicit in the isomorphism axioms and their cont.  *)
   14.32 -
   14.33 -arities stream::(pcpo)pcpo
   14.34 -
   14.35 -consts
   14.36 -
   14.37 -(* ----------------------------------------------------------------------- *)
   14.38 -(* essential constants                                                     *)
   14.39 -
   14.40 -stream_rep      :: "('a stream) -> ('a ** ('a stream)u)"
   14.41 -stream_abs      :: "('a ** ('a stream)u) -> ('a stream)"
   14.42 -
   14.43 -(* ----------------------------------------------------------------------- *)
   14.44 -(* abstract constants and auxiliary constants                              *)
   14.45 -
   14.46 -stream_copy     :: "('a stream -> 'a stream) ->'a stream -> 'a stream"
   14.47 -
   14.48 -scons           :: "'a -> 'a stream -> 'a stream"
   14.49 -stream_when     :: "('a -> 'a stream -> 'b) -> 'a stream -> 'b"
   14.50 -is_scons        :: "'a stream -> tr"
   14.51 -shd             :: "'a stream -> 'a"
   14.52 -stl             :: "'a stream -> 'a stream"
   14.53 -stream_take     :: "nat => 'a stream -> 'a stream"
   14.54 -stream_finite   :: "'a stream => bool"
   14.55 -stream_bisim    :: "('a stream => 'a stream => bool) => bool"
   14.56 -
   14.57 -rules
   14.58 -
   14.59 -(* ----------------------------------------------------------------------- *)
   14.60 -(* axiomatization of recursive type 'a stream                              *)
   14.61 -(* ----------------------------------------------------------------------- *)
   14.62 -(* ('a stream,stream_abs) is the initial F-algebra where                   *)
   14.63 -(* F is the locally continuous functor determined by functor term FT.      *)
   14.64 -(* domain equation: 'a stream = 'a ** ('a stream)u                         *)
   14.65 -(* functor term:    FT = <**,K_{'a},U>                                     *)
   14.66 -(* ----------------------------------------------------------------------- *)
   14.67 -(* stream_abs is an isomorphism with inverse stream_rep                    *)
   14.68 -(* identity is the least endomorphism on 'a stream                         *)
   14.69 -
   14.70 -stream_abs_iso  "stream_rep`(stream_abs`x) = x"
   14.71 -stream_rep_iso  "stream_abs`(stream_rep`x) = x"
   14.72 -stream_copy_def "stream_copy == (LAM f. stream_abs oo 
   14.73 -                (ssplit`(LAM x y. (|x , (fup`(up oo f))`y|) )) oo stream_rep)"
   14.74 -stream_reach    "(fix`stream_copy)`x = x"
   14.75 -
   14.76 -defs
   14.77 -(* ----------------------------------------------------------------------- *)
   14.78 -(* properties of additional constants                                      *)
   14.79 -(* ----------------------------------------------------------------------- *)
   14.80 -(* constructors                                                            *)
   14.81 -
   14.82 -scons_def       "scons == (LAM x l. stream_abs`(| x, up`l |))"
   14.83 -
   14.84 -(* ----------------------------------------------------------------------- *)
   14.85 -(* discriminator functional                                                *)
   14.86 -
   14.87 -stream_when_def 
   14.88 -"stream_when == (LAM f l.ssplit `(LAM x l.f`x`(fup`ID`l)) `(stream_rep`l))"
   14.89 -
   14.90 -(* ----------------------------------------------------------------------- *)
   14.91 -(* discriminators and selectors                                            *)
   14.92 -
   14.93 -is_scons_def    "is_scons == stream_when`(LAM x l.TT)"
   14.94 -shd_def         "shd == stream_when`(LAM x l.x)"
   14.95 -stl_def         "stl == stream_when`(LAM x l.l)"
   14.96 -
   14.97 -(* ----------------------------------------------------------------------- *)
   14.98 -(* the taker for streams                                                   *)
   14.99 -
  14.100 -stream_take_def "stream_take == (%n.iterate n stream_copy UU)"
  14.101 -
  14.102 -(* ----------------------------------------------------------------------- *)
  14.103 -
  14.104 -stream_finite_def       "stream_finite == (%s.? n.stream_take n `s=s)"
  14.105 -
  14.106 -(* ----------------------------------------------------------------------- *)
  14.107 -(* definition of bisimulation is determined by domain equation             *)
  14.108 -(* simplification and rewriting for abstract constants yields def below    *)
  14.109 -
  14.110 -stream_bisim_def "stream_bisim ==
  14.111 -(%R.!s1 s2.
  14.112 -        R s1 s2 -->
  14.113 -  ((s1=UU & s2=UU) |
  14.114 -  (? x s11 s21. x~=UU & s1=scons`x`s11 & s2 = scons`x`s21 & R s11 s21)))"
  14.115 -
  14.116 -end
  14.117 -
  14.118 -
  14.119 -
  14.120 -
    15.1 --- a/src/HOLCF/explicit_domains/Stream2.ML	Mon Feb 24 09:46:12 1997 +0100
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,43 +0,0 @@
    15.4 -(*
    15.5 -    ID:         $Id$
    15.6 -    Author:     Franz Regensburger
    15.7 -    Copyright   1993 Technische Universitaet Muenchen
    15.8 -
    15.9 -Lemmas for theory Stream2.thy
   15.10 -*)
   15.11 -
   15.12 -open Stream2;
   15.13 -
   15.14 -(* ------------------------------------------------------------------------- *)
   15.15 -(* expand fixed point properties                                             *)
   15.16 -(* ------------------------------------------------------------------------- *)
   15.17 -
   15.18 -val smap_def2 = fix_prover2 Stream2.thy smap_def 
   15.19 -        "smap = (LAM f s. stream_when`(LAM x l.scons`(f`x) `(smap`f`l)) `s)";
   15.20 -
   15.21 -
   15.22 -(* ------------------------------------------------------------------------- *)
   15.23 -(* recursive  properties                                                     *)
   15.24 -(* ------------------------------------------------------------------------- *)
   15.25 -
   15.26 -
   15.27 -qed_goal "smap1" Stream2.thy "smap`f`UU = UU"
   15.28 - (fn prems =>
   15.29 -        [
   15.30 -        (stac smap_def2 1),
   15.31 -        (simp_tac (!simpset addsimps stream_when) 1)
   15.32 -        ]);
   15.33 -
   15.34 -qed_goal "smap2" Stream2.thy 
   15.35 -        "x~=UU ==> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)"
   15.36 - (fn prems =>
   15.37 -        [
   15.38 -        (cut_facts_tac prems 1),
   15.39 -        (rtac trans 1),
   15.40 -        (stac smap_def2 1),
   15.41 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   15.42 -        (rtac refl 1)
   15.43 -        ]);
   15.44 -
   15.45 -
   15.46 -val stream2_rews = [smap1, smap2];
    16.1 --- a/src/HOLCF/explicit_domains/Stream2.thy	Mon Feb 24 09:46:12 1997 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,31 +0,0 @@
    16.4 -(* 
    16.5 -    ID:         $Id$
    16.6 -    Author:     Franz Regensburger
    16.7 -    Copyright   1993 Technische Universitaet Muenchen
    16.8 -
    16.9 -NOT SUPPORTED ANY MORE. USE HOLCF/ex/Stream.thy INSTEAD.
   16.10 -
   16.11 -Additional constants for stream
   16.12 -*)
   16.13 -
   16.14 -Stream2 = Stream +
   16.15 -
   16.16 -consts
   16.17 -
   16.18 -smap            :: "('a -> 'b) -> 'a stream -> 'b stream"
   16.19 -
   16.20 -defs
   16.21 -
   16.22 -smap_def
   16.23 -  "smap == fix`(LAM h f s. stream_when`(LAM x l.scons `(f`x) `(h`f`l)) `s)"
   16.24 -
   16.25 -
   16.26 -end
   16.27 -      
   16.28 -
   16.29 -(*
   16.30 -                smap`f`UU = UU
   16.31 -      x~=UU --> smap`f`(scons`x`xs) = scons `(f`x) `(smap`f`xs)
   16.32 -
   16.33 -*)
   16.34 -