added Classlib.* and Witness.*,
authoroheimb
Fri Jan 31 16:56:32 1997 +0100 (1997-01-31)
changeset 257024d7e8fb8261
parent 2569 3a8604f408c9
child 2571 b9f641195b48
added Classlib.* and Witness.*,
moved (and updated) Coind.*, Dagstuhl.*, Dlist.*, Dnat.*, Focus_ex.*
and Stream.* from HOLCF/explicit_domains to here
adapted several proofs; now they work again.
Hope that the following strange errors (when committing) do not matter:
rlog error: RCS/Classlib.ML,v: No such file or directory
rlog error: RCS/Classlib.thy,v: No such file or directory
rlog error: RCS/Coind.ML,v: No such file or directory
rlog error: RCS/Coind.thy,v: No such file or directory
rlog error: RCS/Dagstuhl.ML,v: No such file or directory
rlog error: RCS/Dagstuhl.thy,v: No such file or directory
rlog error: RCS/Dlist.ML,v: No such file or directory
rlog error: RCS/Dlist.thy,v: No such file or directory
rlog error: RCS/Dnat.ML,v: No such file or directory
rlog error: RCS/Dnat.thy,v: No such file or directory
rlog error: RCS/Focus_ex.ML,v: No such file or directory
rlog error: RCS/Focus_ex.thy,v: No such file or directory
rlog error: RCS/Stream.ML,v: No such file or directory
rlog error: RCS/Stream.thy,v: No such file or directory
rlog error: RCS/Witness.ML,v: No such file or directory
rlog error: RCS/Witness.thy,v: No such file or directory
src/HOLCF/ex/Classlib.ML
src/HOLCF/ex/Classlib.thy
src/HOLCF/ex/Coind.ML
src/HOLCF/ex/Coind.thy
src/HOLCF/ex/Dagstuhl.ML
src/HOLCF/ex/Dagstuhl.thy
src/HOLCF/ex/Dlist.ML
src/HOLCF/ex/Dlist.thy
src/HOLCF/ex/Dnat.ML
src/HOLCF/ex/Dnat.thy
src/HOLCF/ex/Fix2.thy
src/HOLCF/ex/Focus_ex.ML
src/HOLCF/ex/Focus_ex.thy
src/HOLCF/ex/Hoare.ML
src/HOLCF/ex/ROOT.ML
src/HOLCF/ex/Stream.ML
src/HOLCF/ex/Stream.thy
src/HOLCF/ex/Witness.ML
src/HOLCF/ex/Witness.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/ex/Classlib.ML	Fri Jan 31 16:56:32 1997 +0100
     1.3 @@ -0,0 +1,196 @@
     1.4 +open Classlib;
     1.5 +
     1.6 +qed_goal "strict_qless" Classlib.thy "(UU .< x) = UU & (x .< UU) = UU"
     1.7 + (fn prems =>
     1.8 +	[
     1.9 +	(simp_tac (HOLCF_ss addsimps [strict_qpo,qless_def,strict_per]) 1)
    1.10 +	]);
    1.11 +
    1.12 +qed_goal "total_qless" Classlib.thy "[|x ~= UU; y ~= UU|] ==> (x .< y) ~= UU"
    1.13 + (fn prems =>
    1.14 +	[
    1.15 +	(cut_facts_tac prems 1),
    1.16 +	(asm_simp_tac (HOLCF_ss addsimps [qless_def]) 1),
    1.17 +	(res_inst_tac [("p","x .= y")] trE 1),
    1.18 +	(asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1),
    1.19 +	(res_inst_tac [("P","x .= y = UU")] notE 1),
    1.20 +	(etac total_per 1),
    1.21 +	(atac 1),
    1.22 +	(atac 1),
    1.23 +	(asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1),
    1.24 +	(asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1)
    1.25 +	]);
    1.26 +
    1.27 +qed_goal "irrefl_qless" Classlib.thy "[|x ~= UU|] ==> (x .< x)=FF"
    1.28 + (fn prems =>
    1.29 +	[
    1.30 +	(cut_facts_tac prems 1),
    1.31 +	(asm_simp_tac (HOLCF_ss addsimps [total_per,qless_def,refl_per]) 1)
    1.32 +	]);
    1.33 +
    1.34 +qed_goal "asym_qless" Classlib.thy "~((x .< y)=TT & (y .< x)=TT)"
    1.35 + (fn prems =>
    1.36 +	[
    1.37 +	(case_tac "x ~= UU & y ~= UU" 1),
    1.38 +	(etac conjE 1),
    1.39 +	(asm_simp_tac (HOLCF_ss addsimps [qless_def]) 1),
    1.40 +	(res_inst_tac [("p","x .= y")] trE 1),
    1.41 +	(asm_simp_tac HOLCF_ss 1),
    1.42 +	(asm_simp_tac HOLCF_ss 1),
    1.43 +	(asm_simp_tac HOLCF_ss 1),
    1.44 +	(rtac (sym_per RS subst) 1),
    1.45 +	(asm_simp_tac HOLCF_ss  1),
    1.46 +	(rtac (de_Morgan_conj RS iffD1) 1),
    1.47 +	(res_inst_tac [("Pa","(x .= y)=TT")] classical2 1),
    1.48 +	(asm_simp_tac (HOLCF_ss addsimps []) 1),
    1.49 +	(etac conjE 1),
    1.50 +	(rtac antisym_qpo 1),
    1.51 +	(atac 1),
    1.52 +	(atac 1),
    1.53 +	(subgoal_tac "x=UU  y=UU" 1),
    1.54 +	(etac disjE 1),
    1.55 +	(asm_simp_tac (HOLCF_ss addsimps [strict_qless]) 1),
    1.56 +	(asm_simp_tac (HOLCF_ss addsimps [strict_qless]) 1),
    1.57 +	(fast_tac HOL_cs 1)
    1.58 +	]);
    1.59 +
    1.60 +
    1.61 +qed_goal "qless_iff" Classlib.thy "((x .< y)=TT) = ((x.=y)=FF & (x .<= y)=TT)"
    1.62 + (fn prems =>
    1.63 +	[
    1.64 +	(rtac iffI 1),
    1.65 +	(asm_full_simp_tac (HOLCF_ss addsimps [qless_def]) 1),
    1.66 +	(res_inst_tac [("p","x .= y")] trE 1),
    1.67 +	(res_inst_tac [("P","TT=UU")] notE 1),
    1.68 +	(simp_tac (HOLCF_ss addsimps []) 1),
    1.69 +	(rtac trans 1),
    1.70 +	(etac sym 1),
    1.71 +	(asm_simp_tac (HOLCF_ss addsimps []) 1),
    1.72 +	(res_inst_tac [("P","TT=FF")] notE 1),
    1.73 +	(simp_tac (HOLCF_ss addsimps []) 1),
    1.74 +	(rtac trans 1),
    1.75 +	(etac sym 1),
    1.76 +	(asm_full_simp_tac (HOLCF_ss addsimps []) 1),
    1.77 +	(rtac conjI 1),
    1.78 +	(atac 1),
    1.79 +	(rtac trans 1),
    1.80 +	(atac 2),
    1.81 +	(asm_full_simp_tac (HOLCF_ss addsimps []) 1),
    1.82 +	(asm_full_simp_tac (HOLCF_ss addsimps [qless_def]) 1)
    1.83 +	]);
    1.84 +
    1.85 +qed_goal "trans_qless" Classlib.thy "[|(x .< y)=TT; (y .< z)=TT |] ==> (x .< z)=TT"
    1.86 + (fn prems =>
    1.87 +	[
    1.88 +	(cut_facts_tac prems 1),
    1.89 +	(rtac (qless_iff RS iffD2) 1),
    1.90 +	(rtac conjI 1),
    1.91 +	(dtac (qless_iff RS iffD1) 1),
    1.92 +	(dtac (qless_iff RS iffD1) 1),
    1.93 +	(REPEAT (etac conjE 1)),
    1.94 +	(case_tac "x~=UU & z~=UU" 1),
    1.95 +	(REPEAT (etac conjE 1)),
    1.96 +	(res_inst_tac [("p","x .= z")] trE 1),
    1.97 +	(res_inst_tac [("P","x .= z = UU")] notE 1),
    1.98 +	(rtac total_per 1),
    1.99 +	(atac 1),
   1.100 +	(atac 1),
   1.101 +	(atac 1),
   1.102 +	(res_inst_tac [("P","TT = FF")] notE 1),
   1.103 +	(simp_tac (HOLCF_ss addsimps []) 1),
   1.104 +	(subgoal_tac "(y.=z)=TT" 1),
   1.105 +	(rtac trans 1),
   1.106 +	(etac sym 1),
   1.107 +	(atac 1),
   1.108 +	(rtac antisym_qpo 1),
   1.109 +	(atac 1),
   1.110 +	(rtac trans_qpo 1),
   1.111 +	(atac 2),
   1.112 +	(etac (antisym_qpo_rev RS conjunct2) 1),
   1.113 +	(atac 1),
   1.114 +	(dtac (de_Morgan_conj RS iffD1) 1),
   1.115 +	(etac disjE 1),
   1.116 +	(dtac notnotD 1),
   1.117 +	(res_inst_tac [("P","FF=UU")] notE 1),
   1.118 +	(simp_tac (HOLCF_ss addsimps []) 1),
   1.119 +	(rtac trans 1),
   1.120 +	(etac sym 1),
   1.121 +	(asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1),
   1.122 +	(dtac notnotD 1),
   1.123 +	(res_inst_tac [("P","FF=UU")] notE 1),
   1.124 +	(simp_tac (HOLCF_ss addsimps []) 1),
   1.125 +	(rtac trans 1),
   1.126 +	(etac sym 1),
   1.127 +	(asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1),
   1.128 +	(dtac (qless_iff RS iffD1) 1),
   1.129 +	(dtac (qless_iff RS iffD1) 1),
   1.130 +	(REPEAT (etac conjE 1)),
   1.131 +	(rtac trans_qpo 1),
   1.132 +	(atac 1),
   1.133 +	(atac 1)
   1.134 +	]);
   1.135 +
   1.136 +(*
   1.137 +
   1.138 +proof for transitivity depends on property antisym_qpo_rev
   1.139 +the proof is a bit lengthy
   1.140 +
   1.141 +val prems = goal Classlib.thy "[|(x .< y)=TT; (y .< z)=TT |] ==> (x .< z)=TT";
   1.142 +by (cut_facts_tac prems 1);
   1.143 +by (rtac (qless_iff RS iffD2) 1);
   1.144 +by (rtac conjI 1);
   1.145 +
   1.146 +by (dtac (qless_iff RS iffD1) 1);
   1.147 +by (dtac (qless_iff RS iffD1) 1);
   1.148 +by (REPEAT (etac conjE 1));
   1.149 +by (case_tac "x~=UU & z~=UU" 1);
   1.150 +by (REPEAT (etac conjE 1));
   1.151 +by (res_inst_tac [("p","x .= z")] trE 1);
   1.152 +by (res_inst_tac [("P","x .= z = UU")] notE 1);
   1.153 +
   1.154 +by (rtac total_per 1);
   1.155 +by (atac 1);
   1.156 +by (atac 1);
   1.157 +by (atac 1);
   1.158 +
   1.159 +by (res_inst_tac [("P","TT = FF")] notE 1);
   1.160 +by (simp_tac (HOLCF_ss addsimps []) 1);
   1.161 +by (subgoal_tac "(y.=z)=TT" 1);
   1.162 +by (rtac trans 1);
   1.163 +by (etac sym 1);
   1.164 +back();
   1.165 +back();
   1.166 +back();
   1.167 +by (atac 1);
   1.168 +by (rtac antisym_qpo 1);
   1.169 +by (atac 1);
   1.170 +by (rtac trans_qpo 1);
   1.171 +by (atac 2);
   1.172 +by (etac (antisym_qpo_rev RS conjunct2) 1);
   1.173 +by (atac 1);
   1.174 +
   1.175 +by (dtac (de_Morgan_conj RS iffD1) 1);
   1.176 +by (etac disjE 1);
   1.177 +by (dtac notnotD 1);
   1.178 +by (res_inst_tac [("P","FF=UU")] notE 1);
   1.179 +by (simp_tac (HOLCF_ss addsimps []) 1);
   1.180 +by (rtac trans 1);
   1.181 +by (etac sym 1);
   1.182 +by (asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1);
   1.183 +
   1.184 +by (dtac notnotD 1);
   1.185 +by (res_inst_tac [("P","FF=UU")] notE 1);
   1.186 +by (simp_tac (HOLCF_ss addsimps []) 1);
   1.187 +by (rtac trans 1);
   1.188 +by (etac sym 1);
   1.189 +back();
   1.190 +by (asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1);
   1.191 +
   1.192 +by (dtac (qless_iff RS iffD1) 1);
   1.193 +by (dtac (qless_iff RS iffD1) 1);
   1.194 +by (REPEAT (etac conjE 1));
   1.195 +by (rtac trans_qpo 1);
   1.196 +by (atac 1);
   1.197 +by (atac 1);
   1.198 +val trans_qless = result();
   1.199 +*)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOLCF/ex/Classlib.thy	Fri Jan 31 16:56:32 1997 +0100
     2.3 @@ -0,0 +1,195 @@
     2.4 +(*  Title:      FOCUS/Classlib.thy
     2.5 +    ID:         $ $
     2.6 +    Author:     Franz Regensburger
     2.7 +    Copyright   1995 Technical University Munich
     2.8 +
     2.9 +Introduce various type classes
    2.10 +
    2.11 +The 8bit package is needed for this theory
    2.12 +
    2.13 +The type void of HOLCF/Void.thy is a witness for all the introduced classes.
    2.14 +Inspect theory Witness.thy for all the proofs. 
    2.15 +
    2.16 +the trivial instance for ++ -- ** // is LAM x y.(UU::void) 
    2.17 +the trivial instance for .= and .<=  is LAM x y.(UU::tr)
    2.18 +
    2.19 +the class hierarchy is as follows
    2.20 +
    2.21 +        pcpo 
    2.22 +         |        
    2.23 +          ----------------
    2.24 +         |               | 
    2.25 +         |      --------------------- 
    2.26 +         |      |       |      |    | 
    2.27 +        per   cplus  cminus ctimes cdvi
    2.28 +         |
    2.29 +       equiv
    2.30 +       /  \
    2.31 +      /    \
    2.32 +     |     |
    2.33 +    qpo    eq
    2.34 +     | 
    2.35 +     |    
    2.36 +  qlinear
    2.37 +
    2.38 +
    2.39 +*)
    2.40 +
    2.41 +Classlib = HOLCF +
    2.42 +
    2.43 +(* -------------------------------------------------------------------- *)
    2.44 +(* class cplus with characteristic constant  ++                         *)
    2.45 + 
    2.46 +classes cplus < pcpo	
    2.47 +
    2.48 +arities void :: cplus
    2.49 +
    2.50 +ops curried 
    2.51 +	"++"	:: "'a::cplus -> 'a -> 'a"		(cinfixl 65)
    2.52 +
    2.53 +
    2.54 +(* class cplus has no characteristic axioms                             *)
    2.55 +(* -------------------------------------------------------------------- *)
    2.56 +
    2.57 +(* -------------------------------------------------------------------- *)
    2.58 +(* class cminus with characteristic constant --                         *)
    2.59 + 
    2.60 +classes cminus < pcpo	
    2.61 +
    2.62 +arities void :: cminus
    2.63 +
    2.64 +ops curried 
    2.65 +	"--"	:: "'a::cminus -> 'a -> 'a"		(cinfixl 65)
    2.66 +
    2.67 +(* class cminus has no characteristic axioms                            *)
    2.68 +(* -------------------------------------------------------------------- *)
    2.69 +
    2.70 +(* -------------------------------------------------------------------- *)
    2.71 +(* class ctimes with characteristic constant **                         *)
    2.72 + 
    2.73 +classes ctimes < pcpo	
    2.74 +
    2.75 +arities void :: ctimes
    2.76 +
    2.77 +ops curried 
    2.78 +	"**"	:: "'a::ctimes -> 'a -> 'a"		(cinfixl 70)
    2.79 +
    2.80 +(* class ctimes has no characteristic axioms                            *)
    2.81 +(* -------------------------------------------------------------------- *)
    2.82 +
    2.83 +(* -------------------------------------------------------------------- *)
    2.84 +(* class cdiv with characteristic constant //                           *)
    2.85 + 
    2.86 +classes cdiv < pcpo	
    2.87 +
    2.88 +arities void :: cdiv
    2.89 +
    2.90 +ops curried 
    2.91 +	"//"	:: "'a::cdiv -> 'a -> 'a"		(cinfixl 70)
    2.92 +
    2.93 +(* class cdiv has no characteristic axioms                              *)
    2.94 +(* -------------------------------------------------------------------- *)
    2.95 +
    2.96 +(* -------------------------------------------------------------------- *)
    2.97 +(* class per with characteristic constant .=                            *)
    2.98 + 
    2.99 +classes per < pcpo	
   2.100 +
   2.101 +arities void :: per
   2.102 +
   2.103 +ops curried 
   2.104 +	".="	:: "'a::per -> 'a -> tr"	(cinfixl 55)
   2.105 +syntax (symbols)
   2.106 +	"op .=" :: "'a::per => 'a => tr"	(infixl "\\<doteq>" 55)
   2.107 +
   2.108 +rules 
   2.109 +
   2.110 +strict_per	"(UU .= x) = UU & (x .= UU) = UU"
   2.111 +total_per	"[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU"
   2.112 +flat_per	"flat (UU::'a::per)"
   2.113 +
   2.114 +sym_per		"(x .= y) = (y .= x)"
   2.115 +trans_per	"[| (x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT"
   2.116 +
   2.117 +(* -------------------------------------------------------------------- *)
   2.118 +
   2.119 +(* -------------------------------------------------------------------- *)
   2.120 +(* class equiv is a refinement of of class per                          *)
   2.121 + 
   2.122 +classes equiv < per 	
   2.123 +
   2.124 +arities void :: equiv
   2.125 +
   2.126 +rules 
   2.127 +
   2.128 +refl_per	"[|(x::'a::equiv) ~= UU|] ==> (x .= x)=TT"
   2.129 +
   2.130 +(* -------------------------------------------------------------------- *)
   2.131 +
   2.132 +(* -------------------------------------------------------------------- *)
   2.133 +(* class eq is a refinement of of class equiv                           *)
   2.134 + 
   2.135 +classes eq < equiv  	
   2.136 +
   2.137 +arities void :: eq
   2.138 +
   2.139 +rules 
   2.140 +
   2.141 +weq	"[| (x::'a::eq) ~= UU; y ~= UU |] ==> 
   2.142 +	 (x = y --> (x .=y) = TT) & (x ~= y --> (x .= y)=FF)"
   2.143 +
   2.144 +(* -------------------------------------------------------------------- *)
   2.145 +
   2.146 +(* -------------------------------------------------------------------- *)
   2.147 +(* class qpo with characteristic constant .<=                           *)
   2.148 +(*  .<= is a partial order wrt an equivalence                           *)
   2.149 + 
   2.150 +classes qpo < equiv	
   2.151 +
   2.152 +arities void :: qpo
   2.153 +
   2.154 +ops curried 
   2.155 +	".<="	:: "'a::qpo -> 'a -> tr"	(cinfixl 55)
   2.156 +syntax (symbols)
   2.157 +	"op .<=":: "'a::qpo => 'a => tr"	(infixl "\\<preceq>" 55)
   2.158 +rules 
   2.159 +
   2.160 +strict_qpo	"(UU .<= x) = UU & (x .<= UU) = UU"
   2.161 +total_qpo	"[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU"
   2.162 +
   2.163 +refl_qpo	"[|x ~= UU|] ==> (x .<= x)=TT"
   2.164 +antisym_qpo	"[| (x .<= y)=TT; (y .<= x)=TT |] ==> (x .=  y)=TT"
   2.165 +trans_qpo	"[| (x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT"
   2.166 +
   2.167 +antisym_qpo_rev	"(x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" 
   2.168 +
   2.169 +(* -------------------------------------------------------------------- *)
   2.170 +
   2.171 +(* -------------------------------------------------------------------- *)
   2.172 +(* irreflexive part .< defined via .<=                                  *)
   2.173 + 
   2.174 +ops curried 
   2.175 +	".<"	:: "'a::qpo -> 'a -> tr"	(cinfixl 55)
   2.176 +syntax (symbols)
   2.177 +	"op .<"	:: "'a::qpo => 'a => tr"	(infixl "\\<prec>" 55)
   2.178 +
   2.179 +defs
   2.180 +
   2.181 +qless_def	"(op .<)  LAM x y.If x .= y then FF else x .<= y fi"
   2.182 +
   2.183 +(* -------------------------------------------------------------------- *)
   2.184 +
   2.185 +(* -------------------------------------------------------------------- *)
   2.186 +(* class qlinear is a refinement of of class qpo                        *)
   2.187 + 
   2.188 +classes qlinear < qpo  	
   2.189 +
   2.190 +arities void :: qlinear
   2.191 +
   2.192 +rules 
   2.193 +
   2.194 +qlinear	"[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT  (y .<= x)=TT "
   2.195 +
   2.196 +(* -------------------------------------------------------------------- *)
   2.197 +
   2.198 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/ex/Coind.ML	Fri Jan 31 16:56:32 1997 +0100
     3.3 @@ -0,0 +1,126 @@
     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 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOLCF/ex/Coind.thy	Fri Jan 31 16:56:32 1997 +0100
     4.3 @@ -0,0 +1,33 @@
     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 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOLCF/ex/Dagstuhl.ML	Fri Jan 31 16:56:32 1997 +0100
     5.3 @@ -0,0 +1,71 @@
     5.4 +(* $Id$ *)
     5.5 +
     5.6 +open Dagstuhl;
     5.7 +
     5.8 +val YS_def2  = fix_prover2 Dagstuhl.thy  YS_def  "YS = y && YS";
     5.9 +val YYS_def2 = fix_prover2 Dagstuhl.thy YYS_def "YYS = y && y && YYS";
    5.10 +
    5.11 +
    5.12 +val prems = goal Dagstuhl.thy "YYS << y && YYS";
    5.13 +by (rtac (YYS_def RS def_fix_ind) 1);
    5.14 +by (Simp_tac 1);
    5.15 +by (cont_tacR 1);
    5.16 +by (stac beta_cfun 1);
    5.17 +by (cont_tacR 1);
    5.18 +by (rtac monofun_cfun_arg 1);
    5.19 +by (rtac monofun_cfun_arg 1);
    5.20 +by (atac 1);
    5.21 +val lemma3 = result();
    5.22 +
    5.23 +val prems = goal Dagstuhl.thy "y && YYS << YYS";
    5.24 +by (stac YYS_def2 1);
    5.25 +back();
    5.26 +by (rtac monofun_cfun_arg 1);
    5.27 +by (rtac lemma3 1);
    5.28 +val lemma4=result();
    5.29 +
    5.30 +(* val  lemma5 = lemma3 RS (lemma4 RS antisym_less) *)
    5.31 +
    5.32 +val prems = goal Dagstuhl.thy "y && YYS = YYS";
    5.33 +by (rtac antisym_less 1);
    5.34 +by (rtac lemma4 1);
    5.35 +by (rtac lemma3 1);
    5.36 +val lemma5=result();
    5.37 +
    5.38 +val prems = goal Dagstuhl.thy "YS = YYS";
    5.39 +by (rtac stream.take_lemma 1);
    5.40 +by (nat_ind_tac "n" 1);
    5.41 +by (simp_tac (!simpset addsimps stream.rews) 1);
    5.42 +by (stac YS_def2 1);
    5.43 +by (stac YYS_def2 1);
    5.44 +by (asm_simp_tac (!simpset addsimps stream.rews) 1);
    5.45 +by (rtac (lemma5 RS sym RS subst) 1);
    5.46 +by (rtac refl 1);
    5.47 +val wir_moel=result();
    5.48 +
    5.49 +(* ------------------------------------------------------------------------ *)
    5.50 +(* Zweite L"osung: Bernhard M"oller                                         *)
    5.51 +(* statt Beweis von  wir_moel "uber take_lemma beidseitige Inclusion        *)
    5.52 +(* verwendet lemma5                                                         *)
    5.53 +(* ------------------------------------------------------------------------ *)
    5.54 +
    5.55 +val prems = goal Dagstuhl.thy "YYS << YS";
    5.56 +by (rewtac YYS_def);
    5.57 +by (rtac fix_least 1);
    5.58 +by (stac beta_cfun 1);
    5.59 +by (cont_tacR 1);
    5.60 +by (simp_tac (!simpset addsimps [YS_def2 RS sym]) 1);
    5.61 +val lemma6=result();
    5.62 +
    5.63 +val prems = goal Dagstuhl.thy "YS << YYS";
    5.64 +by (rtac (YS_def RS def_fix_ind) 1);
    5.65 +by (Simp_tac 1);
    5.66 +by (cont_tacR 1);
    5.67 +by (stac beta_cfun 1);
    5.68 +by (cont_tacR 1);
    5.69 +by (stac (lemma5 RS sym) 1);
    5.70 +by (etac monofun_cfun_arg 1);
    5.71 +val lemma7 = result();
    5.72 +
    5.73 +val  wir_moel = lemma6 RS (lemma7 RS antisym_less);
    5.74 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOLCF/ex/Dagstuhl.thy	Fri Jan 31 16:56:32 1997 +0100
     6.3 @@ -0,0 +1,17 @@
     6.4 +(* $Id$ *)
     6.5 +
     6.6 +
     6.7 +Dagstuhl  =  Stream +
     6.8 +
     6.9 +consts
    6.10 +        y  :: "'a"
    6.11 +       YS  :: "'a stream"
    6.12 +       YYS :: "'a stream"
    6.13 +
    6.14 +defs
    6.15 +
    6.16 +YS_def    "YS  == fix`(LAM x. y && x)"
    6.17 +YYS_def   "YYS == fix`(LAM z. y && y && z)"
    6.18 +  
    6.19 +end
    6.20 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOLCF/ex/Dlist.ML	Fri Jan 31 16:56:32 1997 +0100
     7.3 @@ -0,0 +1,37 @@
     7.4 +open Dlist;
     7.5 +
     7.6 +(* ------------------------------------------------------------------------- *)
     7.7 +(* expand fixed point properties of lmap                                     *)
     7.8 +(* ------------------------------------------------------------------------- *)
     7.9 +
    7.10 +bind_thm ("lmap_def2", fix_prover2 Dlist.thy lmap_def 
    7.11 +        "lmap = (LAM f s.case s of dnil => dnil | x ## l => f`x ## lmap`f`l )");
    7.12 +
    7.13 +(* ------------------------------------------------------------------------- *)
    7.14 +(* recursive  properties   of lmap                                           *)
    7.15 +(* ------------------------------------------------------------------------- *)
    7.16 +
    7.17 +qed_goal "lmap1" Dlist.thy "lmap`f`UU = UU"
    7.18 + (fn prems =>
    7.19 +	[
    7.20 +	(rtac (lmap_def2 RS ssubst) 1),
    7.21 +	(simp_tac (HOLCF_ss addsimps dlist.when_rews) 1)
    7.22 +	]);
    7.23 +
    7.24 +qed_goal "lmap2" Dlist.thy "lmap`f`dnil = dnil"
    7.25 + (fn prems =>
    7.26 +	[
    7.27 +	(rtac (lmap_def2 RS ssubst) 1),
    7.28 +	(simp_tac (HOLCF_ss addsimps dlist.when_rews) 1)
    7.29 +	]);
    7.30 +
    7.31 +qed_goal "lmap3" Dlist.thy 
    7.32 +	"[|x~=UU; xs~=UU|] ==> lmap`f`(x##xs) = (f`x)##(lmap`f`xs)"
    7.33 + (fn prems =>
    7.34 +	[
    7.35 +	(cut_facts_tac prems 1),
    7.36 +	(rtac trans 1),
    7.37 +	(rtac (lmap_def2 RS ssubst) 1),
    7.38 +	(asm_simp_tac (HOLCF_ss addsimps dlist.rews) 1),
    7.39 +	(rtac refl 1)
    7.40 +	]);
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOLCF/ex/Dlist.thy	Fri Jan 31 16:56:32 1997 +0100
     8.3 @@ -0,0 +1,27 @@
     8.4 +(*  Title:      HOLCF/Dlist.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     Franz Regensburger
     8.7 +    Copyright   1993 Technische Universitaet Muenchen
     8.8 +
     8.9 +Theory for finite lists  'a dlist = one ++ ('a ** 'a dlist)
    8.10 +*)
    8.11 +
    8.12 +Dlist = Classlib +
    8.13 +
    8.14 +domain 'a dlist = dnil | "##" (dhd::'a) (dtl::'a dlist) (cinfixr 65)
    8.15 +
    8.16 +ops curried
    8.17 +
    8.18 +lmap	:: "('a -> 'b) -> 'a dlist -> 'b dlist"
    8.19 +lmem	:: "('a::eq)  -> 'a dlist -> tr"		(cinfixl 50)
    8.20 +
    8.21 +defs
    8.22 +
    8.23 +lmap_def "   lmap  fix`(LAM h f s. case s of dnil => dnil 
    8.24 +				      | x ## xs => f`x ## h`f`xs)"
    8.25 +
    8.26 +lmem_def "op lmem  fix`(LAM h e l. case l of dnil => FF
    8.27 +			 | x ## xs => If e  x then TT else h`e`xs fi)"
    8.28 +
    8.29 +end
    8.30 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOLCF/ex/Dnat.ML	Fri Jan 31 16:56:32 1997 +0100
     9.3 @@ -0,0 +1,74 @@
     9.4 +(*  Title:      HOLCF/Dnat.ML
     9.5 +    ID:         $Id$
     9.6 +    Author:     Franz Regensburger
     9.7 +    Copyright   1993, 1995 Technische Universitaet Muenchen
     9.8 +
     9.9 +*)
    9.10 +
    9.11 +open Dnat;
    9.12 +
    9.13 +(* ------------------------------------------------------------------------- *)
    9.14 +(* expand fixed point properties                                             *)
    9.15 +(* ------------------------------------------------------------------------- *)
    9.16 +
    9.17 +bind_thm ("iterator_def2", fix_prover2 Dnat.thy iterator_def 
    9.18 +	"iterator = (LAM n f x. case n of dzero => x | \
    9.19 +\                                     dsucc`m => f`(iterator`m`f`x))");
    9.20 +
    9.21 +(* ------------------------------------------------------------------------- *)
    9.22 +(* recursive  properties                                                     *)
    9.23 +(* ------------------------------------------------------------------------- *)
    9.24 +
    9.25 +qed_goal "iterator1" Dnat.thy "iterator`UU`f`x = UU"
    9.26 + (fn prems =>
    9.27 +	[
    9.28 +	(rtac (iterator_def2 RS ssubst) 1),
    9.29 +	(simp_tac (HOLCF_ss addsimps dnat.rews) 1)
    9.30 +	]);
    9.31 +
    9.32 +qed_goal "iterator2" Dnat.thy "iterator`dzero`f`x = x"
    9.33 + (fn prems =>
    9.34 +	[
    9.35 +	(rtac (iterator_def2 RS ssubst) 1),
    9.36 +	(simp_tac (HOLCF_ss addsimps dnat.rews) 1)
    9.37 +	]);
    9.38 +
    9.39 +qed_goal "iterator3" Dnat.thy 
    9.40 +"n~=UU ==> iterator`(dsucc`n)`f`x = f`(iterator`n`f`x)"
    9.41 + (fn prems =>
    9.42 +	[
    9.43 +	(cut_facts_tac prems 1),
    9.44 +	(rtac trans 1),
    9.45 +	(rtac (iterator_def2 RS ssubst) 1),
    9.46 +	(asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1),
    9.47 +	(rtac refl 1)
    9.48 +	]);
    9.49 +
    9.50 +val iterator_rews = 
    9.51 +	[iterator1, iterator2, iterator3];
    9.52 +
    9.53 +val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(x::dnat)" (fn _ => [
    9.54 +	(rtac allI 1),
    9.55 +	(res_inst_tac [("x","x")] dnat.ind 1),
    9.56 +	(fast_tac HOL_cs 1),
    9.57 +	(rtac allI 1),
    9.58 +	(res_inst_tac [("x","y")] dnat.cases 1),
    9.59 +	(fast_tac (HOL_cs addSIs [UU_I]) 1),
    9.60 +	(Asm_simp_tac 1),
    9.61 +	(asm_simp_tac (!simpset addsimps dnat.dists_le) 1),
    9.62 +	(rtac allI 1),
    9.63 +	(res_inst_tac [("x","y")] dnat.cases 1),
    9.64 +	(fast_tac (HOL_cs addSIs [UU_I]) 1),
    9.65 +	(asm_simp_tac (!simpset addsimps dnat.dists_le) 1),
    9.66 +	(asm_simp_tac (!simpset addsimps dnat.rews) 1),
    9.67 +	(strip_tac 1),
    9.68 +	(subgoal_tac "d<<da" 1),
    9.69 +	(etac allE 1),
    9.70 +	(dtac mp 1),
    9.71 +	(atac 1),
    9.72 +	(etac disjE 1),
    9.73 +	(contr_tac 1),
    9.74 +	(Asm_simp_tac 1),
    9.75 +	(resolve_tac  dnat.inverts 1),
    9.76 +	(REPEAT (atac 1))]);
    9.77 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOLCF/ex/Dnat.thy	Fri Jan 31 16:56:32 1997 +0100
    10.3 @@ -0,0 +1,19 @@
    10.4 +(*  Title:      HOLCF/Dnat.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Franz Regensburger
    10.7 +    Copyright   1993 Technische Universitaet Muenchen
    10.8 +
    10.9 +Theory for the domain of natural numbers  dnat = one ++ dnat
   10.10 +*)
   10.11 +
   10.12 +Dnat = HOLCF +
   10.13 +
   10.14 +domain dnat = dzero | dsucc (dpred :: dnat)
   10.15 +
   10.16 +constdefs
   10.17 +
   10.18 +iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a"
   10.19 +            "iterator == fix`(LAM h n f x . case n of dzero   => x
   10.20 +                                                    | dsucc`m => f`(h`m`f`x))"
   10.21 +
   10.22 +end
    11.1 --- a/src/HOLCF/ex/Fix2.thy	Fri Jan 31 16:51:58 1997 +0100
    11.2 +++ b/src/HOLCF/ex/Fix2.thy	Fri Jan 31 16:56:32 1997 +0100
    11.3 @@ -20,19 +20,3 @@
    11.4  gix2_def "F`y=y ==> gix`F << y"
    11.5  
    11.6  end
    11.7 -
    11.8 -
    11.9 -
   11.10 -
   11.11 -
   11.12 -
   11.13 -
   11.14 -
   11.15 -
   11.16 -
   11.17 -
   11.18 -
   11.19 -
   11.20 -
   11.21 -
   11.22 -
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOLCF/ex/Focus_ex.ML	Fri Jan 31 16:56:32 1997 +0100
    12.3 @@ -0,0 +1,148 @@
    12.4 +open Focus_ex;
    12.5 +
    12.6 +(* first some logical trading *)
    12.7 +
    12.8 +val prems = goal Focus_ex.thy
    12.9 +"is_g(g) = \ 
   12.10 +\ (? f. is_f(f) &  (!x.(? z. <g`x,z> = f`<x,z> &  \
   12.11 +\                  (! w y. <y,w> = f`<x,w>  --> z << w))))";
   12.12 +by (simp_tac (HOL_ss addsimps [is_g,is_net_g]) 1);
   12.13 +by (fast_tac HOL_cs 1);
   12.14 +val lemma1 = result();
   12.15 +
   12.16 +val prems = goal Focus_ex.thy
   12.17 +"(? f. is_f(f) &  (!x. (? z. <g`x,z> = f`<x,z> &  \
   12.18 +\                 (!w y. <y,w> = f`<x,w>  --> z << w)))) \
   12.19 +\ = \ 
   12.20 +\ (? f. is_f(f) &  (!x. ? z.\
   12.21 +\       g`x = cfst`(f`<x,z>) &  \
   12.22 +\         z = csnd`(f`<x,z>) &  \
   12.23 +\       (! w y.  <y,w> = f`<x,w> --> z << w)))";
   12.24 +by (rtac iffI 1);
   12.25 +by (etac exE 1);
   12.26 +by (res_inst_tac [("x","f")] exI 1);
   12.27 +by (REPEAT (etac conjE 1));
   12.28 +by (etac conjI 1);
   12.29 +by (strip_tac 1);
   12.30 +by (etac allE 1);
   12.31 +by (etac exE 1);
   12.32 +by (res_inst_tac [("x","z")] exI 1);
   12.33 +by (REPEAT (etac conjE 1));
   12.34 +by (rtac conjI 1);
   12.35 +by (rtac conjI 2);
   12.36 +by (atac 3);
   12.37 +by (dtac sym 1);
   12.38 +by (asm_simp_tac HOLCF_ss 1);
   12.39 +by (dtac sym 1);
   12.40 +by (asm_simp_tac HOLCF_ss 1);
   12.41 +by (etac exE 1);
   12.42 +by (res_inst_tac [("x","f")] exI 1);
   12.43 +by (REPEAT (etac conjE 1));
   12.44 +by (etac conjI 1);
   12.45 +by (strip_tac 1);
   12.46 +by (etac allE 1);
   12.47 +by (etac exE 1);
   12.48 +by (res_inst_tac [("x","z")] exI 1);
   12.49 +by (REPEAT (etac conjE 1));
   12.50 +by (rtac conjI 1);
   12.51 +by (atac 2);
   12.52 +by (rtac trans 1);
   12.53 +by (rtac (surjective_pairing_Cprod2) 2);
   12.54 +by (etac subst 1);
   12.55 +by (etac subst 1);
   12.56 +by (rtac refl 1);
   12.57 +val lemma2 = result();
   12.58 +
   12.59 +(* direction def_g(g) --> is_g(g) *)
   12.60 +
   12.61 +val prems = goal Focus_ex.thy "def_g(g) --> is_g(g)";
   12.62 +by (simp_tac (HOL_ss addsimps [def_g,lemma1, lemma2]) 1);
   12.63 +by (rtac impI 1);
   12.64 +by (etac exE 1);
   12.65 +by (res_inst_tac [("x","f")] exI 1);
   12.66 +by (REPEAT (etac conjE 1));
   12.67 +by (etac conjI 1);
   12.68 +by (strip_tac 1);
   12.69 +by (res_inst_tac [("x","fix`(LAM k.csnd`(f`<x,k>))")] exI 1);
   12.70 +by (rtac conjI 1);
   12.71 + by (asm_simp_tac HOLCF_ss 1);
   12.72 + by (rtac trans 1);
   12.73 +  by (rtac surjective_pairing_Cprod2 2);
   12.74 + by (rtac cfun_arg_cong 1);
   12.75 + by (rtac trans 1);
   12.76 +  by (rtac fix_eq 1);
   12.77 + by (Simp_tac 1);
   12.78 +by (strip_tac 1);
   12.79 +by (rtac fix_least 1);
   12.80 +by (Simp_tac 1);
   12.81 +by(etac exE 1);
   12.82 +by (dtac sym 1);
   12.83 +back();
   12.84 +by (asm_simp_tac HOLCF_ss 1);
   12.85 +val lemma3 = result();
   12.86 +
   12.87 +(* direction is_g(g) --> def_g(g) *)
   12.88 +val prems = goal Focus_ex.thy "is_g(g) --> def_g(g)";
   12.89 +by (simp_tac (HOL_ss delsimps (ex_simps @ all_simps)
   12.90 +		     addsimps [lemma1,lemma2,def_g]) 1);
   12.91 +by (rtac impI 1);
   12.92 +by (etac exE 1);
   12.93 +by (res_inst_tac [("x","f")] exI 1);
   12.94 +by (REPEAT (etac conjE 1));
   12.95 +by (etac conjI 1);
   12.96 +by (rtac ext_cfun 1);
   12.97 +by (eres_inst_tac [("x","x")] allE 1);
   12.98 +by (etac exE 1);
   12.99 +by (REPEAT (etac conjE 1));
  12.100 +by (subgoal_tac "fix`(LAM k. csnd`(f`<x, k>)) = z" 1);
  12.101 + by (asm_simp_tac HOLCF_ss 1);
  12.102 +by (subgoal_tac "! w y. f`<x, w> = <y, w>  --> z << w" 1);
  12.103 +by (rtac sym 1);
  12.104 +by (rtac fix_eqI 1);
  12.105 +by (asm_simp_tac HOLCF_ss 1);
  12.106 +by (etac sym 1);
  12.107 +by (rtac allI 1);
  12.108 +by (simp_tac HOLCF_ss 1);
  12.109 +by (strip_tac 1);
  12.110 +by (subgoal_tac "f`<x, za> = <cfst`(f`<x,za>),za>" 1);
  12.111 +by (fast_tac HOL_cs 1);
  12.112 +by (rtac trans 1);
  12.113 +by (rtac (surjective_pairing_Cprod2 RS sym) 1);
  12.114 +by (etac cfun_arg_cong 1);
  12.115 +by (strip_tac 1);
  12.116 +by (REPEAT (etac allE 1));
  12.117 +by (etac mp 1);
  12.118 +by (etac sym 1);
  12.119 +val lemma4 = result();
  12.120 +
  12.121 +(* now we assemble the result *)
  12.122 +
  12.123 +val prems = goal Focus_ex.thy "def_g = is_g";
  12.124 +by (rtac ext 1);
  12.125 +by (rtac iffI 1);
  12.126 +by (etac (lemma3 RS mp) 1);
  12.127 +by (etac (lemma4 RS mp) 1);
  12.128 +val loopback_eq = result();
  12.129 +
  12.130 +val prems = goal Focus_ex.thy 
  12.131 +"(? f.\
  12.132 +\ is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))\
  12.133 +\ -->\
  12.134 +\ (? g. def_g(g::'b stream -> 'c stream ))";
  12.135 +by (simp_tac (HOL_ss addsimps [def_g]) 1);
  12.136 +by (strip_tac 1);
  12.137 +by (etac exE 1);
  12.138 +by (rtac exI 1);
  12.139 +by (rtac exI 1);
  12.140 +by (etac conjI 1);
  12.141 +by (rtac refl 1);
  12.142 +val L2 = result();
  12.143 +
  12.144 +val prems = goal Focus_ex.thy 
  12.145 +"(? f.\
  12.146 +\ is_f(f::'b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream))\
  12.147 +\ -->\
  12.148 +\ (? g. is_g(g::'b stream -> 'c stream ))";
  12.149 +by (rtac (loopback_eq RS subst) 1);
  12.150 +by (rtac L2 1);
  12.151 +val conservative_loopback = result();
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOLCF/ex/Focus_ex.thy	Fri Jan 31 16:56:32 1997 +0100
    13.3 @@ -0,0 +1,136 @@
    13.4 +(* Specification of the following loop back device
    13.5 +
    13.6 +
    13.7 +          g 
    13.8 +           --------------------
    13.9 +          |      -------       |
   13.10 +       x  |     |       |      |  y
   13.11 +    ------|---->|       |------| ----->        
   13.12 +          |  z  |   f   | z    |
   13.13 +          |  -->|       |---   |
   13.14 +          | |   |       |   |  |
   13.15 +          | |    -------    |  |
   13.16 +          | |               |  |
   13.17 +          |  <--------------   |
   13.18 +          |                    | 
   13.19 +           --------------------
   13.20 +
   13.21 +
   13.22 +First step: Notation in Agent Network Description Language (ANDL)
   13.23 +-----------------------------------------------------------------
   13.24 +
   13.25 +agent f
   13.26 +	input  channel i1:'b i2: ('b,'c) tc
   13.27 +	output channel o1:'c o2: ('b,'c) tc
   13.28 +is
   13.29 +	Rf(i1,i2,o1,o2)  (left open in the example)
   13.30 +end f
   13.31 +
   13.32 +agent g
   13.33 +	input  channel x:'b 
   13.34 +	output channel y:'c 
   13.35 +is network
   13.36 +	<y,z> = f`<x,z>
   13.37 +end network
   13.38 +end g
   13.39 +
   13.40 +
   13.41 +Remark: the type of the feedback depends at most on the types of the input and
   13.42 +        output of g. (No type miracles inside g)
   13.43 +
   13.44 +Second step: Translation of ANDL specification to HOLCF Specification
   13.45 +---------------------------------------------------------------------
   13.46 +
   13.47 +Specification of agent f ist translated to predicate is_f
   13.48 +
   13.49 +is_f :: ('b stream * ('b,'c) tc stream -> 
   13.50 +		'c stream * ('b,'c) tc stream) => bool
   13.51 +
   13.52 +is_f f  = !i1 i2 o1 o2. 
   13.53 +	f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2)
   13.54 +
   13.55 +Specification of agent g is translated to predicate is_g which uses
   13.56 +predicate is_net_g
   13.57 +
   13.58 +is_net_g :: ('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
   13.59 +	    'b stream => 'c stream => bool
   13.60 +
   13.61 +is_net_g f x y = 
   13.62 +	? z. <y,z> = f`<x,z> & 
   13.63 +	!oy hz. <oy,hz> = f`<x,hz> --> z << hz 
   13.64 +
   13.65 +
   13.66 +is_g :: ('b stream -> 'c stream) => bool
   13.67 +
   13.68 +is_g g  = ? f. is_f f  & (!x y. g`x = y --> is_net_g f x y
   13.69 +	  
   13.70 +Third step: (show conservativity)
   13.71 +-----------
   13.72 +
   13.73 +Suppose we have a model for the theory TH1 which contains the axiom
   13.74 +
   13.75 +	? f. is_f f 
   13.76 +
   13.77 +In this case there is also a model for the theory TH2 that enriches TH1 by
   13.78 +axiom
   13.79 +
   13.80 +	? g. is_g g 
   13.81 +
   13.82 +The result is proved by showing that there is a definitional extension
   13.83 +that extends TH1 by a definition of g.
   13.84 +
   13.85 +
   13.86 +We define:
   13.87 +
   13.88 +def_g g  = 
   13.89 +         (? f. is_f f  & 
   13.90 +	      g = (LAM x. cfst`(f`<x,fix`(LAM k.csnd`(f`<x,k>))>)) )
   13.91 +	
   13.92 +Now we prove:
   13.93 +
   13.94 +	(? f. is_f f ) --> (? g. is_g g) 
   13.95 +
   13.96 +using the theorems
   13.97 +
   13.98 +loopback_eq)	def_g = is_g			(real work) 
   13.99 +
  13.100 +L1)		(? f. is_f f ) --> (? g. def_g g)  (trivial)
  13.101 +
  13.102 +*)
  13.103 +
  13.104 +Focus_ex = Stream +
  13.105 +
  13.106 +types  tc 2
  13.107 +
  13.108 +arities tc:: (pcpo,pcpo)pcpo
  13.109 +
  13.110 +consts
  13.111 +
  13.112 +is_f     ::
  13.113 + "('b stream * ('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) => bool"
  13.114 +is_net_g :: "('b stream *('b,'c) tc stream -> 'c stream * ('b,'c) tc stream) =>
  13.115 +	    'b stream => 'c stream => bool"
  13.116 +is_g     :: "('b stream -> 'c stream) => bool"
  13.117 +def_g    :: "('b stream -> 'c stream) => bool"
  13.118 +Rf	 :: 
  13.119 +"('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
  13.120 +
  13.121 +defs
  13.122 +
  13.123 +is_f		"is_f f == (!i1 i2 o1 o2.
  13.124 +			f`<i1,i2> = <o1,o2> --> Rf(i1,i2,o1,o2))"
  13.125 +
  13.126 +is_net_g	"is_net_g f x y == (? z. 
  13.127 +			<y,z> = f`<x,z> &
  13.128 +			(!oy hz. <oy,hz> = f`<x,hz> --> z << hz))" 
  13.129 +
  13.130 +is_g		"is_g g  == (? f.
  13.131 +			is_f f  & 
  13.132 +			(!x y. g`x = y --> is_net_g f x y))"
  13.133 +
  13.134 +
  13.135 +def_g		"def_g g == (? f.
  13.136 +			is_f f  & 
  13.137 +	      		g = (LAM x. cfst`(f`<x,fix`(LAM  k.csnd`(f`<x,k>))>)))" 
  13.138 +
  13.139 +end
    14.1 --- a/src/HOLCF/ex/Hoare.ML	Fri Jan 31 16:51:58 1997 +0100
    14.2 +++ b/src/HOLCF/ex/Hoare.ML	Fri Jan 31 16:56:32 1997 +0100
    14.3 @@ -103,22 +103,6 @@
    14.4  
    14.5  (* ----- access to definitions ----- *)
    14.6  
    14.7 -val p_def2 = prove_goalw Hoare.thy [p_def]
    14.8 -"p = fix`(LAM f x. If b1`x then f`(g`x) else x fi)"
    14.9 - (fn prems =>
   14.10 -        [
   14.11 -        (rtac refl 1)
   14.12 -        ]);
   14.13 -
   14.14 -val q_def2 = prove_goalw Hoare.thy [q_def]
   14.15 -"q = fix`(LAM f x. If b1`x orelse b2`x then \
   14.16 -\     f`(g`x) else x fi)"
   14.17 - (fn prems =>
   14.18 -        [
   14.19 -        (rtac refl 1)
   14.20 -        ]);
   14.21 -
   14.22 -
   14.23  val p_def3 = prove_goal Hoare.thy 
   14.24  "p`x = If b1`x then p`(g`x) else x fi"
   14.25   (fn prems =>
   14.26 @@ -275,8 +259,7 @@
   14.27   (fn prems =>
   14.28          [
   14.29          (cut_facts_tac prems 1),
   14.30 -        (stac p_def2 1),
   14.31 -        (rtac fix_ind 1),
   14.32 +        (rtac (p_def RS def_fix_ind) 1),
   14.33          (rtac adm_all 1),
   14.34          (rtac allI 1),
   14.35          (rtac adm_eq 1),
   14.36 @@ -309,8 +292,7 @@
   14.37   (fn prems =>
   14.38          [
   14.39          (cut_facts_tac prems 1),
   14.40 -        (stac q_def2 1),
   14.41 -        (rtac fix_ind 1),
   14.42 +        (rtac (q_def RS def_fix_ind) 1),
   14.43          (rtac adm_all 1),
   14.44          (rtac allI 1),
   14.45          (rtac adm_eq 1),
   14.46 @@ -351,8 +333,7 @@
   14.47   (fn prems =>
   14.48          [
   14.49          (cut_facts_tac prems 1),
   14.50 -        (stac q_def2 1),
   14.51 -        (rtac fix_ind 1),
   14.52 +        (rtac (q_def RS def_fix_ind) 1),
   14.53          (rtac adm_all 1),
   14.54          (rtac allI 1),
   14.55          (rtac adm_eq 1),
    15.1 --- a/src/HOLCF/ex/ROOT.ML	Fri Jan 31 16:51:58 1997 +0100
    15.2 +++ b/src/HOLCF/ex/ROOT.ML	Fri Jan 31 16:56:32 1997 +0100
    15.3 @@ -11,9 +11,16 @@
    15.4  writeln"Root file for HOLCF examples";
    15.5  proof_timing := true;
    15.6  
    15.7 +time_use_thy "Classlib";
    15.8 +time_use_thy "Witness";
    15.9 +time_use_thy "Dnat";
   15.10 +time_use_thy "Dlist";
   15.11 +time_use_thy "Stream";
   15.12 +time_use_thy "Dagstuhl";
   15.13 +time_use_thy "Focus_ex";
   15.14 +time_use_thy "Fix2";
   15.15  time_use_thy "Hoare";
   15.16  time_use_thy "Loop";
   15.17 -time_use_thy "Fix2";
   15.18  time_use "loeckx.ML";
   15.19  
   15.20  OS.FileSys.chDir "..";
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOLCF/ex/Stream.ML	Fri Jan 31 16:56:32 1997 +0100
    16.3 @@ -0,0 +1,370 @@
    16.4 +(*  Title: 	FOCUS/Stream.ML
    16.5 +    ID:         $ $
    16.6 +    Author: 	Franz Regensburger, David von Oheimb
    16.7 +    Copyright   1993, 1995 Technische Universitaet Muenchen
    16.8 +
    16.9 +Theorems for Stream.thy
   16.10 +*)
   16.11 +
   16.12 +open Stream;
   16.13 +
   16.14 +fun stream_case_tac s i = res_inst_tac [("x",s)] stream.cases i
   16.15 +			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
   16.16 +
   16.17 +
   16.18 +(* ----------------------------------------------------------------------- *)
   16.19 +(* theorems about scons                                                    *)
   16.20 +(* ----------------------------------------------------------------------- *)
   16.21 +
   16.22 +section "scons";
   16.23 +
   16.24 +qed_goal "scons_eq_UU" thy "a && s = UU = (a = UU)" (fn _ => [
   16.25 +	safe_tac HOL_cs,
   16.26 +	etac contrapos2 1,
   16.27 +	safe_tac (HOL_cs addSIs stream.con_rews)]);
   16.28 +
   16.29 +qed_goal "scons_not_empty" thy "[| a && x = UU; a ~= UU |] ==> R" (fn prems => [
   16.30 +	cut_facts_tac prems 1,
   16.31 +	dresolve_tac stream.con_rews 1,
   16.32 +	contr_tac 1]);
   16.33 +
   16.34 +qed_goal "stream_exhaust_eq" thy "x ~= UU = (? a y. a ~= UU &  x = a && y)" (fn _ =>[
   16.35 +	cut_facts_tac [stream.exhaust] 1,
   16.36 +	safe_tac HOL_cs,
   16.37 +	   contr_tac 1,
   16.38 +	  fast_tac (HOL_cs addDs (tl stream.con_rews)) 1,
   16.39 +	 fast_tac HOL_cs 1,
   16.40 +	fast_tac (HOL_cs addDs (tl stream.con_rews)) 1]);
   16.41 +
   16.42 +qed_goal "stream_prefix" thy 
   16.43 +"[| a && s << t; a ~= UU  |] ==> ? b tt. t = b && tt &  b ~= UU &  s << tt" (fn prems => [
   16.44 +	cut_facts_tac prems 1,
   16.45 +	stream_case_tac "t" 1,
   16.46 +	 fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2,hd (tl stream.con_rews)]) 1,
   16.47 +	fast_tac (HOL_cs addDs stream.inverts) 1]);
   16.48 +
   16.49 +qed_goal "stream_flat_prefix" thy 
   16.50 +"[| x && xs << y && ys; (x::'a) ~= UU; flat (z::'a) |] ==> x = y &  xs << ys"(fn prems=>[
   16.51 +	cut_facts_tac prems 1,
   16.52 +	(forward_tac stream.inverts 1),
   16.53 +	(safe_tac HOL_cs),
   16.54 +	(dtac (hd stream.con_rews RS subst) 1),
   16.55 +	(fast_tac (HOL_cs addDs ((eq_UU_iff RS iffD2)::stream.con_rews)) 1),
   16.56 +	(rewtac flat_def),
   16.57 +	(fast_tac HOL_cs 1)]);
   16.58 +
   16.59 +qed_goal "stream_prefix'" thy "b ~= UU ==> x << b && z = \
   16.60 +\(x = UU |  (? a y. x = a && y &  a ~= UU &  a << b &  y << z))" (fn prems => [
   16.61 +	cut_facts_tac prems 1,
   16.62 +	safe_tac HOL_cs,
   16.63 +	  stream_case_tac "x" 1,
   16.64 +	   safe_tac (HOL_cs addSDs stream.inverts 
   16.65 +			    addSIs [minimal, monofun_cfun, monofun_cfun_arg]),
   16.66 +	fast_tac HOL_cs 1]);
   16.67 +
   16.68 +qed_goal "stream_inject_eq" thy
   16.69 + "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b &  s = t)" (fn prems => [
   16.70 +	cut_facts_tac prems 1,
   16.71 +	safe_tac (HOL_cs addSEs stream.injects)]);	
   16.72 +
   16.73 +
   16.74 +(* ----------------------------------------------------------------------- *)
   16.75 +(* theorems about stream_when                                              *)
   16.76 +(* ----------------------------------------------------------------------- *)
   16.77 +
   16.78 +section "stream_when";
   16.79 +
   16.80 +qed_goal "stream_when_strictf" thy "stream_when`UU`s=UU" (fn _ => [
   16.81 +	stream_case_tac "s" 1,
   16.82 +	ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_fapp1::stream.when_rews))
   16.83 +	]);
   16.84 +	
   16.85 +
   16.86 +(* ----------------------------------------------------------------------- *)
   16.87 +(* theorems about ft and rt                                                *)
   16.88 +(* ----------------------------------------------------------------------- *)
   16.89 +
   16.90 +section "ft & rt";
   16.91 +
   16.92 +(*
   16.93 +qed_goal "stream_ft_lemma1" thy "ft`s=UU --> s=UU" (fn prems => [
   16.94 +	stream_case_tac "s" 1,
   16.95 +	REPEAT (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1)]);
   16.96 +*)
   16.97 +
   16.98 +qed_goal "ft_defin" thy "s~=UU ==> ft`s~=UU" (fn prems => [
   16.99 +	cut_facts_tac prems 1,
  16.100 +	stream_case_tac "s" 1,
  16.101 +	fast_tac HOL_cs 1,
  16.102 +	asm_simp_tac (HOLCF_ss addsimps stream.rews) 1]);
  16.103 +
  16.104 +qed_goal "rt_strict_rev" thy "rt`s~=UU ==> s~=UU" (fn prems => [
  16.105 +	cut_facts_tac prems 1,
  16.106 +	etac contrapos 1,
  16.107 +	asm_simp_tac (HOLCF_ss addsimps stream.sel_rews) 1]);
  16.108 +
  16.109 +qed_goal "surjectiv_scons" thy "(ft`s)&&(rt`s)=s"
  16.110 + (fn prems =>
  16.111 +	[
  16.112 +	stream_case_tac "s" 1,
  16.113 +	REPEAT (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1)
  16.114 +	]);
  16.115 +
  16.116 +qed_goal_spec_mp "monofun_rt_mult" thy 
  16.117 +"!x s. x << s --> iterate i rt x << iterate i rt s" (fn _ => [
  16.118 +	nat_ind_tac "i" 1,
  16.119 +	simp_tac (HOLCF_ss addsimps stream.take_rews) 1,
  16.120 +	strip_tac 1,
  16.121 +	stream_case_tac "x" 1,
  16.122 +	rtac (minimal RS (monofun_iterate2 RS monofunE RS spec RS spec RS mp))1,
  16.123 +	dtac stream_prefix 1,
  16.124 +	 safe_tac HOL_cs,
  16.125 +	asm_simp_tac (HOL_ss addsimps iterate_Suc2::stream.rews) 1]);
  16.126 +			
  16.127 +
  16.128 +(* ----------------------------------------------------------------------- *)
  16.129 +(* theorems about stream_take                                              *)
  16.130 +(* ----------------------------------------------------------------------- *)
  16.131 +
  16.132 +section "stream_take";
  16.133 +
  16.134 +qed_goal "stream_reach2" thy  "(LUB i. stream_take i`s) = s"
  16.135 + (fn prems =>
  16.136 +	[
  16.137 +	(res_inst_tac [("t","s")] (stream.reach RS subst) 1),
  16.138 +	(stac fix_def2 1),
  16.139 +	(rewrite_goals_tac [stream.take_def]),
  16.140 +	(stac contlub_cfun_fun 1),
  16.141 +	(rtac is_chain_iterate 1),
  16.142 +	(rtac refl 1)
  16.143 +	]);
  16.144 +
  16.145 +qed_goal "chain_stream_take" thy "is_chain (%i.stream_take i`s)" (fn _ => [
  16.146 +	rtac is_chainI 1,
  16.147 +	subgoal_tac "!i s. stream_take i`s << stream_take (Suc i)`s" 1,
  16.148 +	fast_tac HOL_cs 1,
  16.149 +	rtac allI 1,
  16.150 +	nat_ind_tac "i" 1,
  16.151 +	 simp_tac (HOLCF_ss addsimps stream.take_rews) 1,
  16.152 +	rtac allI 1,
  16.153 +	stream_case_tac "s" 1,
  16.154 +	 simp_tac (HOLCF_ss addsimps stream.take_rews) 1,
  16.155 +	asm_simp_tac (HOLCF_ss addsimps monofun_cfun_arg::stream.take_rews) 1]);
  16.156 +
  16.157 +qed_goalw "stream_take_more" thy [stream.take_def] 
  16.158 +	"stream_take n`x = x ==> stream_take (Suc n)`x = x" (fn prems => [
  16.159 +		cut_facts_tac prems 1,
  16.160 +		rtac antisym_less 1,
  16.161 +		rtac (stream.reach RS subst) 1, (* 1*back(); *)
  16.162 +		rtac monofun_cfun_fun 1,
  16.163 +		stac fix_def2 1,
  16.164 +		rtac is_ub_thelub 1,
  16.165 +		rtac is_chain_iterate 1,
  16.166 +		etac subst 1, (* 2*back(); *)
  16.167 +		rtac monofun_cfun_fun 1,
  16.168 +		rtac (rewrite_rule [is_chain] is_chain_iterate RS spec) 1]);
  16.169 +
  16.170 +(*
  16.171 +val stream_take_lemma2 = prove_goal thy 
  16.172 + "! s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2" (fn prems => [
  16.173 +	(nat_ind_tac "n" 1),
  16.174 +	(simp_tac (!simpset addsimps stream_rews) 1),
  16.175 +	(strip_tac 1),
  16.176 +	(hyp_subst_tac  1),
  16.177 +	(simp_tac (!simpset addsimps stream_rews) 1),
  16.178 +	(rtac allI 1),
  16.179 +	(res_inst_tac [("s","s2")] streamE 1),
  16.180 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  16.181 +	(asm_simp_tac (!simpset addsimps stream_rews) 1),
  16.182 +	(strip_tac 1 ),
  16.183 +	(subgoal_tac "stream_take n1`xs = xs" 1),
  16.184 +	(rtac ((hd stream_inject) RS conjunct2) 2),
  16.185 +	(atac 4),
  16.186 +	(atac 2),
  16.187 +	(atac 2),
  16.188 +	(rtac cfun_arg_cong 1),
  16.189 +	(fast_tac HOL_cs 1)
  16.190 +	]);
  16.191 +*)
  16.192 +
  16.193 +val stream_take_lemma3 = prove_goal thy 
  16.194 + "!x xs.x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs"
  16.195 + (fn prems => [
  16.196 +	(nat_ind_tac "n" 1),
  16.197 +	(asm_simp_tac (HOL_ss addsimps stream.take_rews) 1),
  16.198 +	(strip_tac 1),
  16.199 +	(res_inst_tac [("P","x && xs=UU")] notE 1),
  16.200 +	(eresolve_tac stream.con_rews 1),
  16.201 +	(etac sym 1),
  16.202 +	(strip_tac 1),
  16.203 +	(rtac stream_take_more 1),
  16.204 +	(res_inst_tac [("a1","x")] ((hd stream.injects) RS conjunct2) 1),
  16.205 +	(etac (hd(tl(tl(stream.take_rews))) RS subst) 1),
  16.206 +	(atac 1),
  16.207 +	(atac 1)]) RS spec RS spec RS mp RS mp;
  16.208 +
  16.209 +val stream_take_lemma4 = prove_goal thy 
  16.210 + "!x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs"
  16.211 + (fn _ => [
  16.212 +	(nat_ind_tac "n" 1),
  16.213 +	(simp_tac (HOL_ss addsimps stream.take_rews) 1),
  16.214 +	(simp_tac (HOL_ss addsimps stream.take_rews) 1)
  16.215 +	]) RS spec RS spec RS mp;
  16.216 +
  16.217 +
  16.218 +(* ------------------------------------------------------------------------- *)
  16.219 +(* special induction rules                                                   *)
  16.220 +(* ------------------------------------------------------------------------- *)
  16.221 +
  16.222 +section "induction";
  16.223 +
  16.224 +qed_goalw "stream_finite_ind" thy [stream.finite_def] 
  16.225 + "[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x" 
  16.226 + (fn prems => [
  16.227 +	(cut_facts_tac prems 1),
  16.228 +	(etac exE 1),
  16.229 +	(etac subst 1),
  16.230 +	(rtac stream.finite_ind 1),
  16.231 +	(atac 1),
  16.232 +	(eresolve_tac prems 1),
  16.233 +	(atac 1)]);
  16.234 +
  16.235 +qed_goal "stream_finite_ind2" thy
  16.236 +"[| P UU;\
  16.237 +\   !! x    .    x ~= UU                  ==> P (x      && UU); \
  16.238 +\   !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )  \
  16.239 +\   |] ==> !s. P (stream_take n`s)" (fn prems => [
  16.240 +	res_inst_tac [("n","n")] nat_induct2 1,
  16.241 +	  asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1,
  16.242 +	 rtac allI 1,
  16.243 +	 stream_case_tac "s" 1,
  16.244 +	  asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1,
  16.245 +	 asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1,
  16.246 +	rtac allI 1,
  16.247 +	stream_case_tac "s" 1,
  16.248 +	 asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1,
  16.249 +	res_inst_tac [("x","sa")] stream.cases 1,
  16.250 +	 asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1,
  16.251 +	asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1]);
  16.252 +
  16.253 +
  16.254 +qed_goal "stream_ind2" thy
  16.255 +"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); \
  16.256 +\   !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s)\
  16.257 +\ |] ==> P x" (fn prems => [
  16.258 +	rtac (stream.reach RS subst) 1,
  16.259 +	rtac (adm_impl_admw RS wfix_ind) 1,
  16.260 +	rtac adm_subst 1,
  16.261 +	cont_tacR 1,
  16.262 +	resolve_tac prems 1,
  16.263 +	rtac allI 1,
  16.264 +	rtac (rewrite_rule [stream.take_def] stream_finite_ind2 RS spec) 1,
  16.265 +	resolve_tac prems 1,
  16.266 +	eresolve_tac prems 1,
  16.267 +	eresolve_tac prems 1, atac 1, atac 1]);
  16.268 +
  16.269 +
  16.270 +(* ----------------------------------------------------------------------- *)
  16.271 +(* simplify use of coinduction                                             *)
  16.272 +(* ----------------------------------------------------------------------- *)
  16.273 +
  16.274 +section "coinduction";
  16.275 +
  16.276 +qed_goalw "stream_coind_lemma2" thy [stream.bisim_def]
  16.277 +"!s1 s2. R s1 s2 --> ft`s1 = ft`s2 &  R (rt`s1) (rt`s2) ==> stream_bisim R"
  16.278 + (fn prems =>
  16.279 +	[
  16.280 +	(cut_facts_tac prems 1),
  16.281 +	(strip_tac 1),
  16.282 +	(etac allE 1),
  16.283 +	(etac allE 1),
  16.284 +	(dtac mp 1),
  16.285 +	(atac 1),
  16.286 +	(etac conjE 1),
  16.287 +	(case_tac "x = UU & x' = UU" 1),
  16.288 +	(rtac disjI1 1),
  16.289 +	(fast_tac HOL_cs 1),
  16.290 +	(rtac disjI2 1),
  16.291 +	(rtac disjE 1),
  16.292 +	(etac (de_Morgan_conj RS subst) 1),
  16.293 +	(res_inst_tac [("x","ft`x")] exI 1),
  16.294 +	(res_inst_tac [("x","rt`x")] exI 1),
  16.295 +	(res_inst_tac [("x","rt`x'")] exI 1),
  16.296 +	(rtac conjI 1),
  16.297 +	(etac ft_defin 1),
  16.298 +	(asm_simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1),
  16.299 +	(eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1),
  16.300 +	(simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1),
  16.301 +	(res_inst_tac [("x","ft`x'")] exI 1),
  16.302 +	(res_inst_tac [("x","rt`x")] exI 1),
  16.303 +	(res_inst_tac [("x","rt`x'")] exI 1),
  16.304 +	(rtac conjI 1),
  16.305 +	(etac ft_defin 1),
  16.306 +	(asm_simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1),
  16.307 +	(res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1),
  16.308 +	(etac sym 1),
  16.309 +	(simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1)
  16.310 +	]);
  16.311 +
  16.312 +(* ----------------------------------------------------------------------- *)
  16.313 +(* theorems about stream_finite                                            *)
  16.314 +(* ----------------------------------------------------------------------- *)
  16.315 +
  16.316 +section "stream_finite";
  16.317 +
  16.318 +qed_goalw "stream_finite_UU" thy [stream.finite_def] "stream_finite UU" 
  16.319 +	(fn prems => [
  16.320 +	(rtac exI 1),
  16.321 +	(simp_tac (HOLCF_ss addsimps stream.rews) 1)]);
  16.322 +
  16.323 +qed_goal "stream_finite_UU_rev" thy  "~  stream_finite s ==> s ~= UU"  (fn prems =>
  16.324 +	[
  16.325 +	(cut_facts_tac prems 1),
  16.326 +	(etac contrapos 1),
  16.327 +	(hyp_subst_tac  1),
  16.328 +	(rtac stream_finite_UU 1)
  16.329 +	]);
  16.330 +
  16.331 +qed_goalw "stream_finite_lemma1" thy [stream.finite_def]
  16.332 + "stream_finite xs ==> stream_finite (x && xs)" (fn prems => [
  16.333 +	(cut_facts_tac prems 1),
  16.334 +	(etac exE 1),
  16.335 +	(rtac exI 1),
  16.336 +	(etac stream_take_lemma4 1)
  16.337 +	]);
  16.338 +
  16.339 +qed_goalw "stream_finite_lemma2" thy [stream.finite_def]
  16.340 + "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs" (fn prems =>
  16.341 +	[
  16.342 +	(cut_facts_tac prems 1),
  16.343 +	(etac exE 1),
  16.344 +	(rtac exI 1),
  16.345 +	(etac stream_take_lemma3 1),
  16.346 +	(atac 1)
  16.347 +	]);
  16.348 +
  16.349 +qed_goal "stream_finite_rt_eq" thy "stream_finite (rt`s) = stream_finite s"
  16.350 +	(fn _ => [
  16.351 +	stream_case_tac "s" 1,
  16.352 +	 simp_tac (HOL_ss addsimps stream_finite_UU::stream.sel_rews) 1,
  16.353 +	asm_simp_tac (HOL_ss addsimps stream.sel_rews) 1,
  16.354 +	fast_tac (HOL_cs addIs [stream_finite_lemma1] 
  16.355 +			 addDs [stream_finite_lemma2]) 1]);
  16.356 +
  16.357 +qed_goal_spec_mp "stream_finite_less" thy 
  16.358 + "stream_finite s ==> !t. t<<s --> stream_finite t" (fn prems => [
  16.359 +	cut_facts_tac prems 1,
  16.360 +	eres_inst_tac [("x","s")] stream_finite_ind 1,
  16.361 +	 strip_tac 1, dtac UU_I 1,
  16.362 +	 asm_simp_tac (HOLCF_ss addsimps [stream_finite_UU]) 1,
  16.363 +	strip_tac 1,
  16.364 +	asm_full_simp_tac (HOL_ss addsimps [stream_prefix']) 1,
  16.365 +	fast_tac (HOL_cs addSIs [stream_finite_UU, stream_finite_lemma1]) 1]);
  16.366 +
  16.367 +qed_goal "adm_not_stream_finite" thy "adm (%x. ~  stream_finite x)" (fn _ => [
  16.368 +	rtac admI 1,
  16.369 +	dtac spec 1,
  16.370 +	etac contrapos 1,
  16.371 +	dtac stream_finite_less 1,
  16.372 +	 etac is_ub_thelub 1,
  16.373 +	atac 1]);
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOLCF/ex/Stream.thy	Fri Jan 31 16:56:32 1997 +0100
    17.3 @@ -0,0 +1,15 @@
    17.4 +(*  Title: 	FOCUS/Stream.thy
    17.5 +    ID:         $ $
    17.6 +    Author: 	Franz Regensburger, David von Oheimb
    17.7 +    Copyright   1993, 1995 Technische Universitaet Muenchen
    17.8 +
    17.9 +general Stream domain
   17.10 +*)
   17.11 +
   17.12 +Stream = HOLCF + 
   17.13 +
   17.14 +domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (cinfixr 65)
   17.15 +
   17.16 +end
   17.17 +
   17.18 +
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOLCF/ex/Witness.ML	Fri Jan 31 16:56:32 1997 +0100
    18.3 @@ -0,0 +1,132 @@
    18.4 +open Witness;
    18.5 +
    18.6 +(* -------------------------------------------------------------------- *)
    18.7 +(* classes cplus, cminus, ctimes, cdiv introduce 
    18.8 +   characteristic constants  o+ o- o* o/
    18.9 +
   18.10 +	"bullet":: "void -> void -> void"
   18.11 +
   18.12 +   is the witness for o+ o- o* o/	
   18.13 +
   18.14 +   No characteristic axioms are to be checked
   18.15 +*)
   18.16 +
   18.17 +(* -------------------------------------------------------------------- *)
   18.18 +(* classes per and qpo introduce characteristic constants
   18.19 +	".="	:: "'a::per -> 'a -> tr"		(cinfixl 55)
   18.20 +	".<="	:: "'a::qpo -> 'a -> tr"		(cinfixl 55)
   18.21 +
   18.22 +   The witness for these is 
   18.23 +
   18.24 +	"cric"	:: "void -> void -> tr"			(cinfixl 55)
   18.25 +
   18.26 +   the classes equiv, eq, qlinear impose additional axioms
   18.27 +*)
   18.28 +
   18.29 +(* -------------------------------------------------------------------- *)
   18.30 +(* 
   18.31 +
   18.32 +characteristic axioms of class per:
   18.33 +
   18.34 +strict_per	"(UU .= x) = UU & (x .= UU) = UU"
   18.35 +total_per	"[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU"
   18.36 +flat_per	"flat (UU::'a::per)"
   18.37 +
   18.38 +sym_per		"(x .= y) = (y .= x)"
   18.39 +trans_per	"[|(x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT"
   18.40 +
   18.41 +   --------------------------------------------------------------------
   18.42 +
   18.43 +characteristic axioms of class equiv:
   18.44 +
   18.45 +refl_per	"[|(x::'a::equiv) ~= UU|] ==> (x .= x)=TT"
   18.46 +
   18.47 +   --------------------------------------------------------------------
   18.48 +
   18.49 +characteristic axioms of class eq:
   18.50 +
   18.51 +weq	"[|(x::'a::eq) ~= UU; y ~= UU|] ==> (x = y --> (x .= y)=TT) & (x ~= y --> x .= y)"
   18.52 +
   18.53 +
   18.54 +   --------------------------------------------------------------------
   18.55 +
   18.56 +characteristic axioms of class qpo:
   18.57 +
   18.58 +strict_qpo	"(UU .<= x) = UU & (x .<= UU) = UU"
   18.59 +total_qpo	"[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU"
   18.60 +
   18.61 +refl_qpo	"[|x ~= UU|] ==> (x .<= x)=TT"
   18.62 +antisym_qpo	"[|(x .<= y)=TT; (y .<= x)=TT |] ==> (x .= y)=TT"
   18.63 +trans_qpo	"[|(x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT"
   18.64 +antisym_qpo_rev	" (x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" 
   18.65 +
   18.66 +   --------------------------------------------------------------------
   18.67 +
   18.68 +characteristic axioms of class qlinear:
   18.69 +
   18.70 +qlinear	"[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT | (y .<= x)=TT "
   18.71 +
   18.72 +*)
   18.73 +
   18.74 +(* strict_per, strict_qpo *)
   18.75 +val prems = goal thy "(UU circ x) = UU & (x circ UU) = UU";
   18.76 +by (simp_tac (HOLCF_ss addsimps [circ_def]) 1);
   18.77 +result();
   18.78 +
   18.79 +(* total_per, total_qpo *)
   18.80 +val prems = goal thy "[|x ~= UU; y ~= UU|] ==> (x circ y) ~= UU";
   18.81 +by (cut_facts_tac prems 1);
   18.82 +by (etac notE 1);
   18.83 +by (rtac unique_void2 1);
   18.84 +result();
   18.85 +
   18.86 +(* flat_per *)
   18.87 +
   18.88 +val prems = goal thy "flat (UU::void)";
   18.89 +by (rtac flat_void 1);
   18.90 +result();
   18.91 +
   18.92 +(* sym_per *)  
   18.93 +val prems = goal thy "(x circ y) = (y circ x)";
   18.94 +by (simp_tac (HOLCF_ss addsimps [circ_def]) 1);
   18.95 +result();
   18.96 +
   18.97 +(* trans_per, trans_qpo *)
   18.98 +val prems = goal thy "[|(x bullet y)=TT; (y bullet z)=TT |] ==> (x bullet z)=TT";
   18.99 +by (cut_facts_tac prems 1);
  18.100 +by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
  18.101 +result();
  18.102 +
  18.103 +(* refl_per *)
  18.104 +val prems = goal thy "[|(x::void) ~= UU|] ==> (x bullet x)=TT";
  18.105 +by (cut_facts_tac prems 1);
  18.106 +by (etac notE 1);
  18.107 +by (rtac unique_void2 1);
  18.108 +result();
  18.109 +
  18.110 +(* weq *)
  18.111 +val prems = goal thy 
  18.112 +	"[|(x::void) ~= UU; y ~= UU|] ==> (x = y --> (x bullet y)=TT) & (x ~= y --> (x bullet y)=FF)";
  18.113 +by (cut_facts_tac prems 1);
  18.114 +by (etac notE 1);
  18.115 +by (rtac unique_void2 1);
  18.116 +result();
  18.117 +
  18.118 +(* antisym_qpo *)
  18.119 +val prems = goal thy "[|(x bullet y)=TT; (y bullet x)=TT |] ==> (x bullet y)=TT";
  18.120 +by (cut_facts_tac prems 1);
  18.121 +by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
  18.122 +result();
  18.123 +
  18.124 +(* antisym_qpo_rev *)
  18.125 +val prems = goal thy "(x bullet y)=TT ==> (x bullet y)=TT & (y bullet x)=TT";
  18.126 +by (cut_facts_tac prems 1);
  18.127 +by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
  18.128 +
  18.129 +(* qlinear *)
  18.130 +val prems = goal thy 
  18.131 +	"[|(x::void) ~= UU; y ~= UU|] ==> (x bullet y)=TT | (y bullet x)=TT ";
  18.132 +by (cut_facts_tac prems 1);
  18.133 +by (etac notE 1);
  18.134 +by (rtac unique_void2 1);
  18.135 +result();
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOLCF/ex/Witness.thy	Fri Jan 31 16:56:32 1997 +0100
    19.3 @@ -0,0 +1,29 @@
    19.4 +(*  Title:      FOCUS/Witness.thy
    19.5 +    ID:         $ $
    19.6 +    Author:     Franz Regensburger
    19.7 +    Copyright   1995 Technical University Munich
    19.8 +
    19.9 +Witnesses for introduction of type cleasse in theory Classlib
   19.10 +
   19.11 +The 8bit package is needed for this theory
   19.12 +
   19.13 +The type void of HOLCF/Void.thy is a witness for all the introduced classes.
   19.14 +
   19.15 +the trivial instance for ++ -- ** // is LAM x y.(UU::void) 
   19.16 +the trivial instance for .= and .<=  is LAM x y.(UU::tr)
   19.17 +
   19.18 +*)
   19.19 +
   19.20 +Witness = HOLCF +
   19.21 +
   19.22 +ops curried 
   19.23 +	"circ"	:: "void -> void -> void"		(cinfixl 65)
   19.24 +	"bullet":: "void -> void -> tr"			(cinfixl 55)
   19.25 +
   19.26 +defs 
   19.27 +
   19.28 +circ_def	"(op circ)  (LAM x y.UU)"
   19.29 +
   19.30 +bullet_def	"(op bullet)  (LAM x y.UU)"
   19.31 +
   19.32 +end