New version
authornipkow
Thu Oct 06 18:40:18 1994 +0100 (1994-10-06)
changeset 625119391dd1d59
parent 624 33b9b5da3e6f
child 626 68fbcdba50d2
New version
src/HOLCF/Cfun3.ML
src/HOLCF/Cont.ML
src/HOLCF/Cprod3.thy
src/HOLCF/Dlist.thy
src/HOLCF/Dnat.ML
src/HOLCF/Dnat.thy
src/HOLCF/Fix.ML
src/HOLCF/Holcfb.ML
src/HOLCF/One.ML
src/HOLCF/One.thy
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.ML
src/HOLCF/ROOT.ML
src/HOLCF/Sprod3.thy
src/HOLCF/Stream.ML
src/HOLCF/Stream.thy
src/HOLCF/Tr1.thy
src/HOLCF/Tr2.thy
src/HOLCF/ccc1.thy
     1.1 --- a/src/HOLCF/Cfun3.ML	Tue Oct 04 13:02:16 1994 +0100
     1.2 +++ b/src/HOLCF/Cfun3.ML	Thu Oct 06 18:40:18 1994 +0100
     1.3 @@ -17,11 +17,11 @@
     1.4  	(strip_tac 1),
     1.5  	(rtac (expand_fun_eq RS iffD2) 1),
     1.6  	(strip_tac 1),
     1.7 -	(rtac (lub_cfun RS thelubI RS ssubst) 1),
     1.8 +	(rtac (thelub_cfun RS ssubst) 1),
     1.9  	(atac 1),
    1.10  	(rtac (Cfunapp2 RS ssubst) 1),
    1.11  	(etac contX_lubcfun 1),
    1.12 -	(rtac (lub_fun RS thelubI RS ssubst) 1),
    1.13 +	(rtac (thelub_fun RS ssubst) 1),
    1.14  	(etac (monofun_fapp1 RS ch2ch_monofun) 1),
    1.15  	(rtac refl 1)
    1.16  	]);
     2.1 --- a/src/HOLCF/Cont.ML	Tue Oct 04 13:02:16 1994 +0100
     2.2 +++ b/src/HOLCF/Cont.ML	Thu Oct 06 18:40:18 1994 +0100
     2.3 @@ -312,15 +312,12 @@
     2.4  (* in both arguments                                                        *)
     2.5  (* ------------------------------------------------------------------------ *)
     2.6  
     2.7 -val diag_lubCF2_1 = prove_goal Cont.thy 
     2.8 +val diag_lemma1 = prove_goal Cont.thy 
     2.9  "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
    2.10 -\ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
    2.11 -\ lub(range(%i. CF2(FY(i))(TY(i))))"
    2.12 -(fn prems =>
    2.13 +\ is_chain(%i. lub(range(%j. CF2(FY(j), TY(i)))))"
    2.14 + (fn prems =>
    2.15  	[
    2.16  	(cut_facts_tac prems 1),
    2.17 -	(rtac antisym_less 1),
    2.18 -	(rtac is_lub_thelub 1),
    2.19  	(rtac ch2ch_lubMF2L 1),
    2.20  	(rtac contX2mono 1),
    2.21  	(atac 1),
    2.22 @@ -328,109 +325,124 @@
    2.23  	(rtac contX2mono 1),
    2.24  	(etac spec 1),
    2.25  	(atac 1),
    2.26 -	(atac 1),
    2.27 -	(rtac ub_rangeI 1),
    2.28 -	(strip_tac 1 ),
    2.29 -	(rtac is_lub_thelub 1),
    2.30 -	((rtac ch2ch_MF2L 1) THEN (rtac contX2mono 1) THEN (atac 1)),
    2.31 -	(atac 1),
    2.32 -	(rtac ub_rangeI 1),
    2.33 -	(strip_tac 1 ),
    2.34 -	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
    2.35 -	(rtac trans_less 1),
    2.36 -	(rtac is_ub_thelub 2),
    2.37 -	(rtac (chain_mono RS mp) 1),
    2.38 -	((rtac ch2ch_MF2R 1) THEN (rtac contX2mono 1) THEN (etac spec 1)),
    2.39 -	(atac 1),
    2.40 -	(atac 1),
    2.41 -	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
    2.42 +	(atac 1)
    2.43 +	]);
    2.44 +
    2.45 +val diag_lemma2 = prove_goal Cont.thy 
    2.46 +"[|contX(CF2);is_chain(FY); is_chain(TY) |] ==>\
    2.47 +\ is_chain(%m. CF2(FY(m), TY(n::nat)))"
    2.48 + (fn prems =>
    2.49 +	[
    2.50 +	(cut_facts_tac prems 1),
    2.51 +	(etac (contX2mono RS ch2ch_MF2L) 1),
    2.52 +	(atac 1)
    2.53 +	]);
    2.54 +
    2.55 +val diag_lemma3 = prove_goal Cont.thy 
    2.56 +"[|!f.contX(CF2(f));is_chain(FY); is_chain(TY) |] ==>\
    2.57 +\ is_chain(%m. CF2(FY(n), TY(m)))"
    2.58 + (fn prems =>
    2.59 +	[
    2.60 +	(cut_facts_tac prems 1),
    2.61 +	(etac allE 1),
    2.62 +	(etac (contX2mono RS ch2ch_MF2R) 1),
    2.63 +	(atac 1)
    2.64 +	]);
    2.65 +
    2.66 +val diag_lemma4 = prove_goal Cont.thy 
    2.67 +"[|contX(CF2);!f.contX(CF2(f));is_chain(FY); is_chain(TY) |] ==>\
    2.68 +\ is_chain(%m. CF2(FY(m), TY(m)))"
    2.69 + (fn prems =>
    2.70 +	[
    2.71 +	(cut_facts_tac prems 1),
    2.72 +	(etac (contX2mono RS ch2ch_MF2LR) 1),
    2.73  	(rtac allI 1),
    2.74 -	((rtac contX2mono 1) THEN (etac spec 1)),
    2.75 -	(atac 1),
    2.76 -	(atac 1),
    2.77 -	(hyp_subst_tac 1),
    2.78 -	(rtac is_ub_thelub 1),
    2.79 -	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
    2.80 -	(rtac allI 1),
    2.81 -	((rtac contX2mono 1) THEN (etac spec 1)),
    2.82 -	(atac 1),
    2.83 +	(etac allE 1),
    2.84 +	(etac contX2mono 1),
    2.85  	(atac 1),
    2.86 -	(rtac trans_less 1),
    2.87 -	(rtac is_ub_thelub 2),
    2.88 -	(res_inst_tac [("x1","ia")] (chain_mono RS mp) 1),
    2.89 -	((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
    2.90 -	(atac 1),
    2.91 -	(atac 1),
    2.92 -	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
    2.93 -	(rtac allI 1),
    2.94 -	((rtac contX2mono 1) THEN (etac spec 1)),
    2.95 -	(atac 1),
    2.96 -	(atac 1),
    2.97 -	(rtac lub_mono 1),
    2.98 -	((rtac ch2ch_MF2LR 1) THEN (etac contX2mono 1)),
    2.99 -	(rtac allI 1),
   2.100 -	((rtac contX2mono 1) THEN (etac spec 1)),
   2.101 -	(atac 1),
   2.102 -	(atac 1),
   2.103 -	(rtac ch2ch_lubMF2L 1),
   2.104 -	(rtac contX2mono 1),
   2.105 -	(atac 1),
   2.106 -	(rtac allI 1),
   2.107 -	((rtac contX2mono 1) THEN (etac spec 1)),
   2.108 -	(atac 1),
   2.109 -	(atac 1),
   2.110 -	(strip_tac 1 ),
   2.111 -	(rtac is_ub_thelub 1),
   2.112 -	((rtac ch2ch_MF2L 1) THEN (etac contX2mono 1)),
   2.113  	(atac 1)
   2.114  	]);
   2.115  
   2.116  
   2.117 +val diag_lubCF2_1 = prove_goal Cont.thy 
   2.118 +"[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   2.119 +\ lub(range(%i. lub(range(%j. CF2(FY(j))(TY(i)))))) =\
   2.120 +\ lub(range(%i. CF2(FY(i))(TY(i))))"
   2.121 + (fn prems =>
   2.122 +	[
   2.123 +	(cut_facts_tac prems 1),
   2.124 +	(rtac antisym_less 1),
   2.125 +	(rtac is_lub_thelub 1),
   2.126 +	(etac diag_lemma1 1),
   2.127 +	(REPEAT (atac 1)),
   2.128 +	(rtac ub_rangeI 1),
   2.129 +	(strip_tac 1 ),
   2.130 +	(rtac lub_mono3 1),
   2.131 +	(etac diag_lemma2 1),
   2.132 +	(REPEAT (atac 1)),
   2.133 +	(etac diag_lemma4 1),
   2.134 +	(REPEAT (atac 1)),
   2.135 +	(rtac allI 1),
   2.136 +	(res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1),
   2.137 +	(res_inst_tac [("x","ia")] exI 1),
   2.138 +	(rtac (chain_mono RS mp) 1),
   2.139 +	(etac diag_lemma3 1),
   2.140 +	(REPEAT (atac 1)),
   2.141 +	(hyp_subst_tac 1),
   2.142 +	(res_inst_tac [("x","ia")] exI 1),
   2.143 +	(rtac refl_less 1),
   2.144 +	(res_inst_tac [("x","i")] exI 1),
   2.145 +	(rtac (chain_mono RS mp) 1),
   2.146 +	(etac diag_lemma2 1),
   2.147 +	(REPEAT (atac 1)),
   2.148 +	(rtac lub_mono 1),
   2.149 +	(etac diag_lemma4 1),
   2.150 +	(REPEAT (atac 1)),
   2.151 +	(etac diag_lemma1 1),
   2.152 +	(REPEAT (atac 1)),
   2.153 +	(strip_tac 1 ),
   2.154 +	(rtac is_ub_thelub 1),
   2.155 +	(etac diag_lemma2 1),
   2.156 +	(REPEAT (atac 1))
   2.157 +	]);
   2.158 +
   2.159  val diag_lubCF2_2 = prove_goal Cont.thy 
   2.160  "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   2.161  \ lub(range(%j. lub(range(%i. CF2(FY(j))(TY(i)))))) =\
   2.162  \ lub(range(%i. CF2(FY(i))(TY(i))))"
   2.163 -(fn prems =>
   2.164 + (fn prems =>
   2.165  	[
   2.166  	(cut_facts_tac prems 1),
   2.167  	(rtac trans 1),
   2.168  	(rtac ex_lubMF2 1),
   2.169 -	(rtac ((hd prems) RS contX2mono) 1), 
   2.170 +	(etac contX2mono 1),
   2.171  	(rtac allI 1),
   2.172 -	(rtac (((hd (tl prems)) RS spec RS contX2mono)) 1),
   2.173 -	(atac 1),
   2.174 -	(atac 1),
   2.175 +	(etac allE 1),
   2.176 +	(etac contX2mono 1),
   2.177 +	(REPEAT (atac 1)),
   2.178  	(rtac diag_lubCF2_1 1),
   2.179 -	(atac 1),
   2.180 -	(atac 1),
   2.181 -	(atac 1),
   2.182 -	(atac 1)
   2.183 +	(REPEAT (atac 1))
   2.184  	]);
   2.185  
   2.186 -
   2.187  val contlub_CF2 = prove_goal Cont.thy 
   2.188  "[|contX(CF2);!f.contX(CF2(f));is_chain(FY);is_chain(TY)|] ==>\
   2.189  \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))"
   2.190 -(fn prems =>
   2.191 + (fn prems =>
   2.192  	[
   2.193  	(cut_facts_tac prems 1),
   2.194 -	(rtac ((hd prems) RS contX2contlub RS contlubE RS 
   2.195 -		spec RS mp RS ssubst) 1),
   2.196 +	(rtac ((hd prems) RS contX2contlub RS contlubE RS spec RS mp RS ssubst) 1),
   2.197  	(atac 1),
   2.198  	(rtac (thelub_fun RS ssubst) 1),
   2.199 -	(rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1), 
   2.200 +	(rtac ((hd prems) RS contX2mono RS ch2ch_monofun) 1),
   2.201  	(atac 1),
   2.202  	(rtac trans 1),
   2.203 -	(rtac (((hd (tl prems)) RS spec RS contX2contlub) RS 
   2.204 -	contlubE RS spec RS mp RS ext RS arg_cong RS arg_cong) 1),
   2.205 +	(rtac (((hd (tl prems)) RS spec RS contX2contlub) RS contlubE RS 
   2.206 +               spec RS mp RS ext RS arg_cong RS arg_cong) 1),
   2.207  	(atac 1),
   2.208  	(rtac diag_lubCF2_2 1),
   2.209 -	(atac 1),
   2.210 -	(atac 1),
   2.211 -	(atac 1),
   2.212 -	(atac 1)
   2.213 +	(REPEAT (atac 1))
   2.214  	]);
   2.215 -
   2.216 + 
   2.217  (* ------------------------------------------------------------------------ *)
   2.218  (* The following results are about application for functions in 'a=>'b      *)
   2.219  (* ------------------------------------------------------------------------ *)
   2.220 @@ -574,24 +586,20 @@
   2.221  	(atac 1)
   2.222  	]);
   2.223  
   2.224 +
   2.225  val contX2contlub_app = prove_goal Cont.thy 
   2.226 -"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==>\
   2.227 -\	 contlub(%x.(ft(x))(tt(x)))"
   2.228 +"[|contX(ft);!x.contX(ft(x));contX(tt)|] ==> contlub(%x.(ft(x))(tt(x)))"
   2.229   (fn prems =>
   2.230  	[
   2.231  	(cut_facts_tac prems 1),
   2.232  	(rtac contlubI 1),
   2.233  	(strip_tac 1),
   2.234  	(res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1),
   2.235 -	(rtac contX2contlub 1),
   2.236 -	(resolve_tac prems 1),
   2.237 +	(etac contX2contlub 1),
   2.238  	(atac 1),
   2.239  	(rtac contlub_CF2 1),
   2.240 -	(resolve_tac prems 1),
   2.241 -	(resolve_tac prems 1),
   2.242 -	(atac 1),
   2.243 -	(rtac (contX2mono RS ch2ch_monofun) 1),
   2.244 -	(resolve_tac prems 1),
   2.245 +	(REPEAT (atac 1)),
   2.246 +	(etac (contX2mono RS ch2ch_monofun) 1),
   2.247  	(atac 1)
   2.248  	]);
   2.249  
     3.1 --- a/src/HOLCF/Cprod3.thy	Tue Oct 04 13:02:16 1994 +0100
     3.2 +++ b/src/HOLCF/Cprod3.thy	Thu Oct 06 18:40:18 1994 +0100
     3.3 @@ -20,6 +20,8 @@
     3.4  	csnd         :: "('a*'b)->'b"
     3.5  	csplit       :: "('a->'b->'c)->('a*'b)->'c"
     3.6  
     3.7 +translations "x#y" => "cpair[x][y]"
     3.8 +
     3.9  rules 
    3.10  
    3.11  inst_cprod_pcpo	"(UU::'a*'b) = <UU,UU>"
    3.12 @@ -31,13 +33,6 @@
    3.13  
    3.14  end
    3.15  
    3.16 -ML
    3.17 -
    3.18 -(* ----------------------------------------------------------------------*)
    3.19 -(* parse translations for the above mixfix                               *)
    3.20 -(* ----------------------------------------------------------------------*)
    3.21 -
    3.22 -val parse_translation = [("@cpair",mk_cinfixtr "@cpair")];
    3.23  
    3.24  
    3.25  
     4.1 --- a/src/HOLCF/Dlist.thy	Tue Oct 04 13:02:16 1994 +0100
     4.2 +++ b/src/HOLCF/Dlist.thy	Thu Oct 06 18:40:18 1994 +0100
     4.3 @@ -4,7 +4,19 @@
     4.4      ID:         $ $
     4.5      Copyright   1994 Technische Universitaet Muenchen
     4.6  
     4.7 -Theory for lists
     4.8 +Theory for finite lists  'a dlist = one ++ ('a ** 'a dlist)
     4.9 +
    4.10 +The type is axiomatized as the least solution of the domain equation above.
    4.11 +The functor term that specifies the domain equation is: 
    4.12 +
    4.13 +  FT = <++,K_{one},<**,K_{'a},I>>
    4.14 +
    4.15 +For details see chapter 5 of:
    4.16 +
    4.17 +[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
    4.18 +                     Dissertation, Technische Universit"at M"unchen, 1994
    4.19 +
    4.20 +
    4.21  *)
    4.22  
    4.23  Dlist = Stream2 +
    4.24 @@ -47,8 +59,9 @@
    4.25  (* axiomatization of recursive type 'a dlist                               *)
    4.26  (* ----------------------------------------------------------------------- *)
    4.27  (* ('a dlist,dlist_abs) is the initial F-algebra where                     *)
    4.28 -(* F is the locally continuous functor determined by domain equation       *)
    4.29 -(* X = one ++ 'a ** X                                                      *)
    4.30 +(* F is the locally continuous functor determined by functor term FT.      *)
    4.31 +(* domain equation: 'a dlist = one ++ ('a ** 'a dlist)                     *)
    4.32 +(* functor term:    FT = <++,K_{one},<**,K_{'a},I>>                        *)
    4.33  (* ----------------------------------------------------------------------- *)
    4.34  (* dlist_abs is an isomorphism with inverse dlist_rep                      *)
    4.35  (* identity is the least endomorphism on 'a dlist                          *)
     5.1 --- a/src/HOLCF/Dnat.ML	Tue Oct 04 13:02:16 1994 +0100
     5.2 +++ b/src/HOLCF/Dnat.ML	Thu Oct 06 18:40:18 1994 +0100
     5.3 @@ -12,7 +12,7 @@
     5.4  (* The isomorphisms dnat_rep_iso and dnat_abs_iso are strict               *)
     5.5  (* ------------------------------------------------------------------------*)
     5.6  
     5.7 -val dnat_iso_strict= dnat_rep_iso RS (dnat_abs_iso RS 
     5.8 +val dnat_iso_strict = dnat_rep_iso RS (dnat_abs_iso RS 
     5.9  	(allI  RSN (2,allI RS iso_strict)));
    5.10  
    5.11  val dnat_rews = [dnat_iso_strict RS conjunct1,
    5.12 @@ -530,3 +530,5 @@
    5.13  
    5.14  
    5.15  
    5.16 +
    5.17 +
     6.1 --- a/src/HOLCF/Dnat.thy	Tue Oct 04 13:02:16 1994 +0100
     6.2 +++ b/src/HOLCF/Dnat.thy	Thu Oct 06 18:40:18 1994 +0100
     6.3 @@ -3,7 +3,17 @@
     6.4      Author: 	Franz Regensburger
     6.5      Copyright   1993 Technische Universitaet Muenchen
     6.6  
     6.7 -Theory for the domain of natural numbers
     6.8 +Theory for the domain of natural numbers  dnat = one ++ dnat
     6.9 +
    6.10 +The type is axiomatized as the least solution of the domain equation above.
    6.11 +The functor term that specifies the domain equation is: 
    6.12 +
    6.13 +  FT = <++,K_{one},I>
    6.14 +
    6.15 +For details see chapter 5 of:
    6.16 +
    6.17 +[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
    6.18 +                     Dissertation, Technische Universit"at M"unchen, 1994
    6.19  
    6.20  *)
    6.21  
    6.22 @@ -44,8 +54,9 @@
    6.23  (* axiomatization of recursive type dnat                                   *)
    6.24  (* ----------------------------------------------------------------------- *)
    6.25  (* (dnat,dnat_abs) is the initial F-algebra where                          *)
    6.26 -(* F is the locally continuous functor determined by domain equation       *)
    6.27 -(* X = one ++ X                                                            *)
    6.28 +(* F is the locally continuous functor determined by functor term FT.      *)
    6.29 +(* domain equation: dnat = one ++ dnat                                     *)
    6.30 +(* functor term:    FT = <++,K_{one},I>                                    *) 
    6.31  (* ----------------------------------------------------------------------- *)
    6.32  (* dnat_abs is an isomorphism with inverse dnat_rep                        *)
    6.33  (* identity is the least endomorphism on dnat                              *)
     7.1 --- a/src/HOLCF/Fix.ML	Tue Oct 04 13:02:16 1994 +0100
     7.2 +++ b/src/HOLCF/Fix.ML	Thu Oct 06 18:40:18 1994 +0100
     7.3 @@ -688,6 +688,43 @@
     7.4  	(etac cfun_arg_cong 1)
     7.5  	]);
     7.6  
     7.7 +(* ------------------------------------------------------------------------- *)
     7.8 +(* a result about functions with flat codomain                               *)
     7.9 +(* ------------------------------------------------------------------------- *)
    7.10 +
    7.11 +val flat_codom = prove_goalw Fix.thy [flat_def]
    7.12 +"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
    7.13 + (fn prems =>
    7.14 +	[
    7.15 +	(cut_facts_tac prems 1),
    7.16 +	(res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1),
    7.17 +	(rtac disjI1 1),
    7.18 +	(rtac UU_I 1),
    7.19 +	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
    7.20 +	(atac 1),
    7.21 +	(rtac (minimal RS monofun_cfun_arg) 1),
    7.22 +	(res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
    7.23 +	(etac disjI1 1),
    7.24 +	(rtac disjI2 1),
    7.25 +	(rtac allI 1),
    7.26 +	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
    7.27 +	(atac 1),
    7.28 +	(res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
    7.29 +	(etac allE 1),(etac allE 1),
    7.30 +	(dtac mp 1),
    7.31 +	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
    7.32 +	(etac disjE 1),
    7.33 +	(contr_tac 1),
    7.34 +	(atac 1),
    7.35 +	(etac allE 1),
    7.36 +	(etac allE 1),
    7.37 +	(dtac mp 1),
    7.38 +	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
    7.39 +	(etac disjE 1),
    7.40 +	(contr_tac 1),
    7.41 +	(atac 1)
    7.42 +	]);
    7.43 +
    7.44  (* ------------------------------------------------------------------------ *)
    7.45  (* admissibility of special formulae and propagation                        *)
    7.46  (* ------------------------------------------------------------------------ *)
    7.47 @@ -777,6 +814,8 @@
    7.48  	(etac spec 1)
    7.49  	]);
    7.50  
    7.51 +val adm_all2 = (allI RS adm_all);
    7.52 +
    7.53  val adm_subst = prove_goal  Fix.thy  
    7.54  	"[|contX(t); adm(P)|] ==> adm(%x.P(t(x)))"
    7.55   (fn prems =>
    7.56 @@ -1127,45 +1166,8 @@
    7.57  	]);
    7.58  
    7.59  
    7.60 -val adm_all2 = (allI RS adm_all);
    7.61  
    7.62  val adm_thms = [adm_impl,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
    7.63  	adm_all2,adm_not_less,adm_not_free,adm_conj,adm_less
    7.64  	];
    7.65  
    7.66 -(* ------------------------------------------------------------------------- *)
    7.67 -(* a result about functions with flat codomain                               *)
    7.68 -(* ------------------------------------------------------------------------- *)
    7.69 -
    7.70 -val flat_codom = prove_goalw Fix.thy [flat_def]
    7.71 -"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=(UU::'b) | (!z.f[z::'a]=c)"
    7.72 - (fn prems =>
    7.73 -	[
    7.74 -	(cut_facts_tac prems 1),
    7.75 -	(res_inst_tac [("Q","f[x::'a]=(UU::'b)")] classical2 1),
    7.76 -	(rtac disjI1 1),
    7.77 -	(rtac UU_I 1),
    7.78 -	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
    7.79 -	(atac 1),
    7.80 -	(rtac (minimal RS monofun_cfun_arg) 1),
    7.81 -	(res_inst_tac [("Q","f[UU::'a]=(UU::'b)")] classical2 1),
    7.82 -	(etac disjI1 1),
    7.83 -	(rtac disjI2 1),
    7.84 -	(rtac allI 1),
    7.85 -	(res_inst_tac [("s","f[x]"),("t","c")] subst 1),
    7.86 -	(atac 1),
    7.87 -	(res_inst_tac [("a","f[UU::'a]")] (refl RS box_equals) 1),
    7.88 -	(etac allE 1),(etac allE 1),
    7.89 -	(dtac mp 1),
    7.90 -	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
    7.91 -	(etac disjE 1),
    7.92 -	(contr_tac 1),
    7.93 -	(atac 1),
    7.94 -	(etac allE 1),
    7.95 -	(etac allE 1),
    7.96 -	(dtac mp 1),
    7.97 -	(res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
    7.98 -	(etac disjE 1),
    7.99 -	(contr_tac 1),
   7.100 -	(atac 1)
   7.101 -	]);
     8.1 --- a/src/HOLCF/Holcfb.ML	Tue Oct 04 13:02:16 1994 +0100
     8.2 +++ b/src/HOLCF/Holcfb.ML	Thu Oct 06 18:40:18 1994 +0100
     8.3 @@ -9,10 +9,10 @@
     8.4  open Holcfb;
     8.5  
     8.6  (* ------------------------------------------------------------------------ *)
     8.7 -(* <::nat=>nat=>bool is well-founded                                        *)
     8.8 +(* <::nat=>nat=>bool is a well-ordering                                     *)
     8.9  (* ------------------------------------------------------------------------ *)
    8.10  
    8.11 -val well_founded_nat = prove_goal  Nat.thy 
    8.12 +val well_ordering_nat = prove_goal  Nat.thy 
    8.13  	"!P. P(x::nat) --> (? y. P(y) & (! x. P(x) --> y <= x))"
    8.14   (fn prems =>
    8.15  	[
    8.16 @@ -45,7 +45,7 @@
    8.17   (fn prems =>
    8.18  	[
    8.19  	(cut_facts_tac prems 1),
    8.20 -	(rtac (well_founded_nat RS spec RS mp RS exE) 1),
    8.21 +	(rtac (well_ordering_nat RS spec RS mp RS exE) 1),
    8.22  	(atac 1),
    8.23  	(rtac selectI 1),
    8.24  	(atac 1)
    8.25 @@ -150,3 +150,21 @@
    8.26  val classical3 = (notE RS notI);
    8.27  (* [| ?P ==> ~ ?P1; ?P ==> ?P1 |] ==> ~ ?P *)
    8.28  
    8.29 +
    8.30 +val nat_less_cases = prove_goal Nat.thy 
    8.31 +    "[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
    8.32 +( fn prems =>
    8.33 +	[
    8.34 +	(res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
    8.35 +	(etac disjE 2),
    8.36 +	(etac (hd (tl (tl prems))) 1),
    8.37 +	(etac (sym RS hd (tl prems)) 1),
    8.38 +	(etac (hd prems) 1)
    8.39 +	]);
    8.40 +
    8.41 +
    8.42 +
    8.43 +
    8.44 +
    8.45 +
    8.46 +
     9.1 --- a/src/HOLCF/One.ML	Tue Oct 04 13:02:16 1994 +0100
     9.2 +++ b/src/HOLCF/One.ML	Thu Oct 06 18:40:18 1994 +0100
     9.3 @@ -68,15 +68,17 @@
     9.4  (* one is flat                                                              *)
     9.5  (* ------------------------------------------------------------------------ *)
     9.6  
     9.7 -val prems = goalw One.thy [flat_def] "flat(one)";
     9.8 -by (rtac allI 1);
     9.9 -by (rtac allI 1);
    9.10 -by (res_inst_tac [("p","x")] oneE 1);
    9.11 -by (asm_simp_tac ccc1_ss  1);
    9.12 -by (res_inst_tac [("p","y")] oneE 1);
    9.13 -by (asm_simp_tac (ccc1_ss addsimps dist_less_one) 1);
    9.14 -by (asm_simp_tac ccc1_ss  1);
    9.15 -val flat_one = result();
    9.16 +val flat_one = prove_goalw One.thy [flat_def] "flat(one)"
    9.17 + (fn prems =>
    9.18 +	[
    9.19 +	(rtac allI 1),
    9.20 +	(rtac allI 1),
    9.21 +	(res_inst_tac [("p","x")] oneE 1),
    9.22 +	(asm_simp_tac ccc1_ss  1),
    9.23 +	(res_inst_tac [("p","y")] oneE 1),
    9.24 +	(asm_simp_tac (ccc1_ss addsimps dist_less_one) 1),
    9.25 +	(asm_simp_tac ccc1_ss  1)
    9.26 +	]);
    9.27  
    9.28  
    9.29  (* ------------------------------------------------------------------------ *)
    10.1 --- a/src/HOLCF/One.thy	Tue Oct 04 13:02:16 1994 +0100
    10.2 +++ b/src/HOLCF/One.thy	Thu Oct 06 18:40:18 1994 +0100
    10.3 @@ -3,27 +3,17 @@
    10.4      Author: 	Franz Regensburger
    10.5      Copyright   1993 Technische Universitaet Muenchen
    10.6  
    10.7 -Introduve atomic type one = (void)u
    10.8 +Introduce atomic type one = (void)u
    10.9  
   10.10 -This is the first type that is introduced using a domain isomorphism.
   10.11 -The type axiom 
   10.12 -
   10.13 -	arities one :: pcpo
   10.14 +The type is axiomatized as the least solution of a domain equation.
   10.15 +The functor term that specifies the domain equation is: 
   10.16  
   10.17 -and the continuity of the Isomorphisms are taken for granted. Since the
   10.18 -type is not recursive, it could be easily introduced in a purely conservative
   10.19 -style as it was used for the types sprod, ssum, lift. The definition of the 
   10.20 -ordering is canonical using abstraction and representation, but this would take
   10.21 -again a lot of internal constants. It can easily be seen that the axioms below
   10.22 -are consistent.
   10.23 +  FT = <U,K_{void}>
   10.24  
   10.25 -The partial ordering on type one is implicitly defined via the
   10.26 -isomorphism axioms and the continuity of abs_one and rep_one.
   10.27 +For details see chapter 5 of:
   10.28  
   10.29 -We could also introduce the function less_one with definition
   10.30 -
   10.31 -less_one(x,y) = rep_one[x] << rep_one[y]
   10.32 -
   10.33 +[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
   10.34 +                     Dissertation, Technische Universit"at M"unchen, 1994
   10.35  
   10.36  *)
   10.37  
    11.1 --- a/src/HOLCF/Pcpo.thy	Tue Oct 04 13:02:16 1994 +0100
    11.2 +++ b/src/HOLCF/Pcpo.thy	Thu Oct 06 18:40:18 1994 +0100
    11.3 @@ -1,38 +1,14 @@
    11.4 -(*  Title: 	HOLCF/pcpo.thy
    11.5 -    ID:         $Id$
    11.6 -    Author: 	Franz Regensburger
    11.7 -    Copyright   1993 Technische Universitaet Muenchen
    11.8 -
    11.9 -Definition of class pcpo (pointed complete partial order)
   11.10 -
   11.11 -The prototype theory for this class is porder.thy 
   11.12 -
   11.13 -*)
   11.14 -
   11.15  Pcpo = Porder +
   11.16  
   11.17 -(* Introduction of new class. The witness is type void. *)
   11.18 -
   11.19  classes pcpo < po
   11.20 -
   11.21 -(* default class is still term *)
   11.22 -(* void is the prototype in pcpo *)
   11.23 -
   11.24  arities void :: pcpo
   11.25  
   11.26  consts	
   11.27 -	UU	::	"'a::pcpo"		(* UU is the least element *)
   11.28 +	UU :: "'a::pcpo"	
   11.29  rules
   11.30  
   11.31 -(* class axioms: justification is theory Porder *)
   11.32 -
   11.33 -minimal		"UU << x"			(* witness is minimal_void *)
   11.34 -
   11.35 -cpo		"is_chain(S) ==> ? x. range(S) <<| (x::('a::pcpo))" 
   11.36 -						(* witness is cpo_void     *)
   11.37 -						(* needs explicit type     *)
   11.38 -
   11.39 -(* instance of UU for the prototype void *)
   11.40 +minimal	"UU << x"	
   11.41 +cpo	"is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)" 
   11.42  
   11.43  inst_void_pcpo	"(UU::void) = UU_void"
   11.44  
    12.1 --- a/src/HOLCF/Porder.ML	Tue Oct 04 13:02:16 1994 +0100
    12.2 +++ b/src/HOLCF/Porder.ML	Thu Oct 06 18:40:18 1994 +0100
    12.3 @@ -9,6 +9,21 @@
    12.4  open Porder0;
    12.5  open Porder;
    12.6  
    12.7 +
    12.8 +(* ------------------------------------------------------------------------ *)
    12.9 +(* the reverse law of anti--symmetrie of <<                                 *)
   12.10 +(* ------------------------------------------------------------------------ *)
   12.11 +
   12.12 +val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x"
   12.13 +(fn prems =>
   12.14 +	[
   12.15 +	(cut_facts_tac prems 1),
   12.16 +	(rtac conjI 1),
   12.17 +	((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
   12.18 +	((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
   12.19 +	]);
   12.20 +
   12.21 +
   12.22  val box_less = prove_goal Porder.thy 
   12.23  "[| a << b; c << a; b << d|] ==> c << d"
   12.24   (fn prems =>
   12.25 @@ -72,20 +87,6 @@
   12.26  	(rtac refl_less 1)
   12.27  	]);
   12.28  
   12.29 -(* ------------------------------------------------------------------------ *)
   12.30 -(* Lemma for reasoning by cases on the natural numbers                      *)
   12.31 -(* ------------------------------------------------------------------------ *)
   12.32 -
   12.33 -val nat_less_cases = prove_goal Porder.thy 
   12.34 -	"[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
   12.35 -( fn prems =>
   12.36 -	[
   12.37 -	(res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
   12.38 -	(etac disjE 2),
   12.39 -	(etac (hd (tl (tl prems))) 1),
   12.40 -	(etac (sym RS hd (tl prems)) 1),
   12.41 -	(etac (hd prems) 1)
   12.42 -	]);
   12.43  
   12.44  (* ------------------------------------------------------------------------ *)
   12.45  (* The range of a chain is a totaly ordered     <<                           *)
   12.46 @@ -123,7 +124,7 @@
   12.47  
   12.48  
   12.49  (* ------------------------------------------------------------------------ *)
   12.50 -(* technical lemmas about lub and is_lub, use above results about @         *)
   12.51 +(* technical lemmas about lub and is_lub                                    *)
   12.52  (* ------------------------------------------------------------------------ *)
   12.53  
   12.54  val lubI = prove_goal Porder.thy "(? x. M <<| x) ==> M <<| lub(M)"
   12.55 @@ -303,19 +304,6 @@
   12.56  
   12.57  
   12.58  (* ------------------------------------------------------------------------ *)
   12.59 -(* the reverse law of anti--symmetrie of <<                                 *)
   12.60 -(* ------------------------------------------------------------------------ *)
   12.61 -
   12.62 -val antisym_less_inverse = prove_goal Porder.thy "x=y ==> x << y & y << x"
   12.63 -(fn prems =>
   12.64 -	[
   12.65 -	(cut_facts_tac prems 1),
   12.66 -	(rtac conjI 1),
   12.67 -	((rtac subst 1) THEN (rtac refl_less 2) THEN (atac 1)),
   12.68 -	((rtac subst 1) THEN (rtac refl_less 2) THEN (etac sym 1))
   12.69 -	]);
   12.70 -
   12.71 -(* ------------------------------------------------------------------------ *)
   12.72  (* results about finite chains                                              *)
   12.73  (* ------------------------------------------------------------------------ *)
   12.74  
    13.1 --- a/src/HOLCF/ROOT.ML	Tue Oct 04 13:02:16 1994 +0100
    13.2 +++ b/src/HOLCF/ROOT.ML	Thu Oct 06 18:40:18 1994 +0100
    13.3 @@ -55,7 +55,7 @@
    13.4  use_thy "One";
    13.5  use_thy "Tr1";
    13.6  use_thy "Tr2";
    13.7 -
    13.8 + 
    13.9  use_thy "HOLCF";
   13.10  
   13.11  use_thy "Dnat";
   13.12 @@ -64,7 +64,6 @@
   13.13  use_thy "Stream2";
   13.14  use_thy "Dlist";
   13.15  
   13.16 -
   13.17  use "../Pure/install_pp.ML";
   13.18  print_depth 8;  
   13.19  
    14.1 --- a/src/HOLCF/Sprod3.thy	Tue Oct 04 13:02:16 1994 +0100
    14.2 +++ b/src/HOLCF/Sprod3.thy	Thu Oct 06 18:40:18 1994 +0100
    14.3 @@ -18,6 +18,8 @@
    14.4  	ssnd         :: "('a**'b)->'b"
    14.5  	ssplit       :: "('a->'b->'c)->('a**'b)->'c"
    14.6  
    14.7 +translations "x##y" => "spair[x][y]"
    14.8 +
    14.9  rules 
   14.10  
   14.11  inst_sprod_pcpo	"(UU::'a**'b) = Ispair(UU,UU)"
   14.12 @@ -28,12 +30,5 @@
   14.13  
   14.14  end
   14.15  
   14.16 -ML
   14.17 -
   14.18 -(* ----------------------------------------------------------------------*)
   14.19 -(* parse translations for the above mixfix                               *)
   14.20 -(* ----------------------------------------------------------------------*)
   14.21 -
   14.22 -val parse_translation = [("@spair",mk_cinfixtr "@spair")];
   14.23  
   14.24  
    15.1 --- a/src/HOLCF/Stream.ML	Tue Oct 04 13:02:16 1994 +0100
    15.2 +++ b/src/HOLCF/Stream.ML	Thu Oct 06 18:40:18 1994 +0100
    15.3 @@ -419,6 +419,30 @@
    15.4  	(REPEAT (atac 1))
    15.5  	]);
    15.6  
    15.7 +(* prove induction using definition of admissibility 
    15.8 +   stream_reach rsp. stream_reach2 
    15.9 +   and finite induction stream_finite_ind *)
   15.10 +
   15.11 +val stream_ind = prove_goal Stream.thy
   15.12 +"[|adm(P);\
   15.13 +\  P(UU);\
   15.14 +\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   15.15 +\  |] ==> P(s)"
   15.16 + (fn prems =>
   15.17 +	[
   15.18 +	(rtac (stream_reach2 RS subst) 1),
   15.19 +	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   15.20 +	(resolve_tac prems 1),
   15.21 +	(SELECT_GOAL (rewrite_goals_tac [stream_take_def]) 1),
   15.22 +	(rtac ch2ch_fappL 1),
   15.23 +	(rtac is_chain_iterate 1),
   15.24 +	(rtac allI 1),
   15.25 +	(rtac (stream_finite_ind RS spec) 1),
   15.26 +	(REPEAT (resolve_tac prems 1)),
   15.27 +	(REPEAT (atac 1))
   15.28 +	]);
   15.29 +
   15.30 +(* prove induction with usual LCF-Method using fixed point induction *)
   15.31  val stream_ind = prove_goal Stream.thy
   15.32  "[|adm(P);\
   15.33  \  P(UU);\
   15.34 @@ -440,6 +464,7 @@
   15.35  	(REPEAT (atac 1))
   15.36  	]);
   15.37  
   15.38 +
   15.39  (* ------------------------------------------------------------------------*)
   15.40  (* simplify use of Co-induction                                            *)
   15.41  (* ------------------------------------------------------------------------*)
    16.1 --- a/src/HOLCF/Stream.thy	Tue Oct 04 13:02:16 1994 +0100
    16.2 +++ b/src/HOLCF/Stream.thy	Thu Oct 06 18:40:18 1994 +0100
    16.3 @@ -3,7 +3,18 @@
    16.4      Author: 	Franz Regensburger
    16.5      Copyright   1993 Technische Universitaet Muenchen
    16.6  
    16.7 -Theory for streams without defined empty stream
    16.8 +Theory for streams without defined empty stream 
    16.9 +  'a stream = 'a ** ('a stream)u
   16.10 +
   16.11 +The type is axiomatized as the least solution of the domain equation above.
   16.12 +The functor term that specifies the domain equation is: 
   16.13 +
   16.14 +  FT = <**,K_{'a},U>
   16.15 +
   16.16 +For details see chapter 5 of:
   16.17 +
   16.18 +[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
   16.19 +                     Dissertation, Technische Universit"at M"unchen, 1994
   16.20  *)
   16.21  
   16.22  Stream = Dnat2 +
   16.23 @@ -44,8 +55,9 @@
   16.24  (* axiomatization of recursive type 'a stream                              *)
   16.25  (* ----------------------------------------------------------------------- *)
   16.26  (* ('a stream,stream_abs) is the initial F-algebra where                   *)
   16.27 -(* F is the locally continuous functor determined by domain equation       *)
   16.28 -(* X = 'a ** (X)u                                                          *)
   16.29 +(* F is the locally continuous functor determined by functor term FT.      *)
   16.30 +(* domain equation: 'a stream = 'a ** ('a stream)u                         *)
   16.31 +(* functor term:    FT = <**,K_{'a},U>                                     *)
   16.32  (* ----------------------------------------------------------------------- *)
   16.33  (* stream_abs is an isomorphism with inverse stream_rep                    *)
   16.34  (* identity is the least endomorphism on 'a stream                         *)
    17.1 --- a/src/HOLCF/Tr1.thy	Tue Oct 04 13:02:16 1994 +0100
    17.2 +++ b/src/HOLCF/Tr1.thy	Thu Oct 06 18:40:18 1994 +0100
    17.3 @@ -3,22 +3,17 @@
    17.4      Author: 	Franz Regensburger
    17.5      Copyright   1993 Technische Universitaet Muenchen
    17.6  
    17.7 -Introduve the domain of truth values tr = {UU,TT,FF}
    17.8 -
    17.9 -This type is introduced using a domain isomorphism.
   17.10 +Introduce the domain of truth values tr = one ++ one
   17.11  
   17.12 -The type axiom 
   17.13 -
   17.14 -	arities tr :: pcpo
   17.15 +The type is axiomatized as the least solution of a domain equation.
   17.16 +The functor term that specifies the domain equation is: 
   17.17  
   17.18 -and the continuity of the Isomorphisms are taken for granted. Since the
   17.19 -type is not recursive, it could be easily introduced in a purely conservative
   17.20 -style as it was used for the types sprod, ssum, lift. The definition of the 
   17.21 -ordering is canonical using abstraction and representation, but this would take
   17.22 -again a lot of internal constants. It can be easily seen that the axioms below
   17.23 -are consistent.
   17.24 +  FT = <++,K_{one},K_{one}>
   17.25  
   17.26 -Partial Ordering is implicit in isomorphims abs_tr,rep_tr and their continuity
   17.27 +For details see chapter 5 of:
   17.28 +
   17.29 +[Franz Regensburger] HOLCF: Eine konservative Erweiterung von HOL um LCF,
   17.30 +                     Dissertation, Technische Universit"at M"unchen, 1994
   17.31  
   17.32  *)
   17.33  
    18.1 --- a/src/HOLCF/Tr2.thy	Tue Oct 04 13:02:16 1994 +0100
    18.2 +++ b/src/HOLCF/Tr2.thy	Thu Oct 06 18:40:18 1994 +0100
    18.3 @@ -20,6 +20,10 @@
    18.4  
    18.5          "neg"           :: "tr -> tr"
    18.6  
    18.7 +translations "x andalso y" => "trand[x][y]"
    18.8 +             "x orelse y"  => "tror[x][y]"
    18.9 +             "If b then e1 else e2 fi" => "Icifte[b][e1][e2]"
   18.10 +              
   18.11  rules
   18.12  
   18.13    ifte_def    "Icifte == (LAM t e1 e2.tr_when[e1][e2][t])"
   18.14 @@ -29,29 +33,7 @@
   18.15  
   18.16  end
   18.17  
   18.18 -ML
   18.19 -
   18.20 -(* ----------------------------------------------------------------------*)
   18.21 -(* translations for the above mixfixes                                   *)
   18.22 -(* ----------------------------------------------------------------------*)
   18.23 -
   18.24 -fun ciftetr ts =
   18.25 -	let val Cfapp = Const("fapp",dummyT) in	
   18.26 -	Cfapp $ 
   18.27 -	   	(Cfapp $
   18.28 -			(Cfapp$Const("Icifte",dummyT)$(nth_elem (0,ts)))$
   18.29 -		(nth_elem (1,ts)))$
   18.30 -	(nth_elem (2,ts))
   18.31 -	end;
   18.32 -
   18.33 -
   18.34 -val parse_translation = [("@andalso",mk_cinfixtr "@andalso"),
   18.35 -			("@orelse",mk_cinfixtr "@orelse"),
   18.36 -			("@cifte",ciftetr)];
   18.37 -
   18.38 -val print_translation = [];
   18.39  
   18.40  
   18.41  
   18.42  
   18.43 -
    19.1 --- a/src/HOLCF/ccc1.thy	Tue Oct 04 13:02:16 1994 +0100
    19.2 +++ b/src/HOLCF/ccc1.thy	Thu Oct 06 18:40:18 1994 +0100
    19.3 @@ -16,6 +16,7 @@
    19.4  	"@oo"		:: "('b->'c)=>('a->'b)=>'a->'c" ("_ oo _" [101,100] 100)
    19.5  	"cop @oo"	:: "('b->'c)->('a->'b)->'a->'c" ("cfcomp")
    19.6  
    19.7 +translations "f1 oo f2" => "cfcomp[f1][f2]"
    19.8  
    19.9  rules
   19.10  
   19.11 @@ -24,15 +25,6 @@
   19.12  
   19.13  end
   19.14  
   19.15 -ML
   19.16 -
   19.17 -(* ----------------------------------------------------------------------*)
   19.18 -(* parse translations for the above mixfix  oo                           *)
   19.19 -(* ----------------------------------------------------------------------*)
   19.20 -
   19.21 -val parse_translation = [("@oo",mk_cinfixtr "@oo")];
   19.22 -val print_translation = [];
   19.23  
   19.24  
   19.25  
   19.26 -