Examples are adopted to the changes from HOLCF.
authorslotosch
Mon Feb 17 11:04:00 1997 +0100 (1997-02-17)
changeset 26423c3a84cc85a9
parent 2641 533a84b3bedd
child 2643 a7f469c0ba59
Examples are adopted to the changes from HOLCF.
Classlib is reduced.
Classlib still uses arities, Classlib will change completely to new
classes of ADTs
src/HOLCF/ex/Classlib.ML
src/HOLCF/ex/Classlib.thy
src/HOLCF/ex/Hoare.ML
src/HOLCF/ex/Loop.ML
src/HOLCF/ex/Loop.thy
src/HOLCF/ex/Witness.ML
src/HOLCF/ex/Witness.thy
     1.1 --- a/src/HOLCF/ex/Classlib.ML	Mon Feb 17 11:01:10 1997 +0100
     1.2 +++ b/src/HOLCF/ex/Classlib.ML	Mon Feb 17 11:04:00 1997 +0100
     1.3 @@ -1,196 +1,2 @@
     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 --- a/src/HOLCF/ex/Classlib.thy	Mon Feb 17 11:01:10 1997 +0100
     2.2 +++ b/src/HOLCF/ex/Classlib.thy	Mon Feb 17 11:04:00 1997 +0100
     2.3 @@ -5,13 +5,14 @@
     2.4  
     2.5  Introduce various type classes
     2.6  
     2.7 -The 8bit package is needed for this theory
     2.8 -
     2.9 -The type void of HOLCF/Void.thy is a witness for all the introduced classes.
    2.10 +The type void of HOLCF/One.thy is a witness for all the introduced classes.
    2.11  Inspect theory Witness.thy for all the proofs. 
    2.12  
    2.13 -the trivial instance for ++ -- ** // is LAM x y.(UU::void) 
    2.14 -the trivial instance for .= and .<=  is LAM x y.(UU::tr)
    2.15 +!!! Witness and Claslib have to be adapted to axclasses !!!
    2.16 +------------------------------------------------------------
    2.17 +
    2.18 +the trivial instance for ++ -- ** // is circ
    2.19 +the trivial instance for .= and .<=  is bullet
    2.20  
    2.21  the class hierarchy is as follows
    2.22  
    2.23 @@ -42,7 +43,7 @@
    2.24   
    2.25  classes cplus < pcpo	
    2.26  
    2.27 -arities void :: cplus
    2.28 +arities lift :: (term)cplus
    2.29  
    2.30  ops curried 
    2.31  	"++"	:: "'a::cplus -> 'a -> 'a"		(cinfixl 65)
    2.32 @@ -56,7 +57,7 @@
    2.33   
    2.34  classes cminus < pcpo	
    2.35  
    2.36 -arities void :: cminus
    2.37 +arities lift :: (term)cminus
    2.38  
    2.39  ops curried 
    2.40  	"--"	:: "'a::cminus -> 'a -> 'a"		(cinfixl 65)
    2.41 @@ -69,7 +70,7 @@
    2.42   
    2.43  classes ctimes < pcpo	
    2.44  
    2.45 -arities void :: ctimes
    2.46 +arities lift :: (term)ctimes
    2.47  
    2.48  ops curried 
    2.49  	"**"	:: "'a::ctimes -> 'a -> 'a"		(cinfixl 70)
    2.50 @@ -82,7 +83,7 @@
    2.51   
    2.52  classes cdiv < pcpo	
    2.53  
    2.54 -arities void :: cdiv
    2.55 +arities lift :: (term)cdiv
    2.56  
    2.57  ops curried 
    2.58  	"//"	:: "'a::cdiv -> 'a -> 'a"		(cinfixl 70)
    2.59 @@ -95,7 +96,7 @@
    2.60   
    2.61  classes per < pcpo	
    2.62  
    2.63 -arities void :: per
    2.64 +arities lift :: (term)per
    2.65  
    2.66  ops curried 
    2.67  	".="	:: "'a::per -> 'a -> tr"	(cinfixl 55)
    2.68 @@ -106,7 +107,7 @@
    2.69  
    2.70  strict_per	"(UU .= x) = UU & (x .= UU) = UU"
    2.71  total_per	"[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU"
    2.72 -flat_per	"flat (UU::'a::per)"
    2.73 +flat_per	"flat (x::'a::per)"
    2.74  
    2.75  sym_per		"(x .= y) = (y .= x)"
    2.76  trans_per	"[| (x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT"
    2.77 @@ -118,7 +119,7 @@
    2.78   
    2.79  classes equiv < per 	
    2.80  
    2.81 -arities void :: equiv
    2.82 +arities lift :: (term)equiv
    2.83  
    2.84  rules 
    2.85  
    2.86 @@ -131,65 +132,11 @@
    2.87   
    2.88  classes eq < equiv  	
    2.89  
    2.90 -arities void :: eq
    2.91 +arities lift :: (term)eq
    2.92  
    2.93  rules 
    2.94  
    2.95  weq	"[| (x::'a::eq) ~= UU; y ~= UU |] ==> 
    2.96  	 (x = y --> (x .=y) = TT) & (x ~= y --> (x .= y)=FF)"
    2.97  
    2.98 -(* -------------------------------------------------------------------- *)
    2.99 -
   2.100 -(* -------------------------------------------------------------------- *)
   2.101 -(* class qpo with characteristic constant .<=                           *)
   2.102 -(*  .<= is a partial order wrt an equivalence                           *)
   2.103 - 
   2.104 -classes qpo < equiv	
   2.105 -
   2.106 -arities void :: qpo
   2.107 -
   2.108 -ops curried 
   2.109 -	".<="	:: "'a::qpo -> 'a -> tr"	(cinfixl 55)
   2.110 -syntax (symbols)
   2.111 -	"op .<=":: "'a::qpo => 'a => tr"	(infixl "\\<preceq>" 55)
   2.112 -rules 
   2.113 -
   2.114 -strict_qpo	"(UU .<= x) = UU & (x .<= UU) = UU"
   2.115 -total_qpo	"[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU"
   2.116 -
   2.117 -refl_qpo	"[|x ~= UU|] ==> (x .<= x)=TT"
   2.118 -antisym_qpo	"[| (x .<= y)=TT; (y .<= x)=TT |] ==> (x .=  y)=TT"
   2.119 -trans_qpo	"[| (x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT"
   2.120 -
   2.121 -antisym_qpo_rev	"(x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" 
   2.122 -
   2.123 -(* -------------------------------------------------------------------- *)
   2.124 -
   2.125 -(* -------------------------------------------------------------------- *)
   2.126 -(* irreflexive part .< defined via .<=                                  *)
   2.127 - 
   2.128 -ops curried 
   2.129 -	".<"	:: "'a::qpo -> 'a -> tr"	(cinfixl 55)
   2.130 -syntax (symbols)
   2.131 -	"op .<"	:: "'a::qpo => 'a => tr"	(infixl "\\<prec>" 55)
   2.132 -
   2.133 -defs
   2.134 -
   2.135 -qless_def	"(op .<)  LAM x y.If x .= y then FF else x .<= y fi"
   2.136 -
   2.137 -(* -------------------------------------------------------------------- *)
   2.138 -
   2.139 -(* -------------------------------------------------------------------- *)
   2.140 -(* class qlinear is a refinement of of class qpo                        *)
   2.141 - 
   2.142 -classes qlinear < qpo  	
   2.143 -
   2.144 -arities void :: qlinear
   2.145 -
   2.146 -rules 
   2.147 -
   2.148 -qlinear	"[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT  (y .<= x)=TT "
   2.149 -
   2.150 -(* -------------------------------------------------------------------- *)
   2.151 -
   2.152  end
     3.1 --- a/src/HOLCF/ex/Hoare.ML	Mon Feb 17 11:01:10 1997 +0100
     3.2 +++ b/src/HOLCF/ex/Hoare.ML	Mon Feb 17 11:04:00 1997 +0100
     3.3 @@ -95,7 +95,7 @@
     3.4   (fn prems =>
     3.5          [
     3.6          (cut_facts_tac prems 1),
     3.7 -        (etac (flat_tr RS flat_codom RS disjE) 1),
     3.8 +        (etac (flat_flat RS flat_codom RS disjE) 1),
     3.9          (atac 1),
    3.10          (etac spec 1)
    3.11          ]);
    3.12 @@ -323,7 +323,7 @@
    3.13   (fn prems =>
    3.14          [
    3.15          (cut_facts_tac prems 1),
    3.16 -        (rtac (flat_tr RS flat_codom) 1),
    3.17 +        (rtac (flat_flat RS flat_codom) 1),
    3.18          (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1),
    3.19          (etac spec 1)
    3.20          ]);
     4.1 --- a/src/HOLCF/ex/Loop.ML	Mon Feb 17 11:01:10 1997 +0100
     4.2 +++ b/src/HOLCF/ex/Loop.ML	Mon Feb 17 11:04:00 1997 +0100
     4.3 @@ -57,7 +57,7 @@
     4.4          (asm_simp_tac HOLCF_ss 1),
     4.5          (stac while_unfold 1),
     4.6          (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1),
     4.7 -        (etac (flat_tr RS flat_codom RS disjE) 1),
     4.8 +        (etac (flat_flat RS flat_codom RS disjE) 1),
     4.9          (atac 1),
    4.10          (etac spec 1),
    4.11          (simp_tac HOLCF_ss 1),
    4.12 @@ -92,7 +92,7 @@
    4.13          (rtac step_def2 1),
    4.14          (asm_simp_tac HOLCF_ss 1),
    4.15          (etac exE 1),
    4.16 -        (etac (flat_tr RS flat_codom RS disjE) 1),
    4.17 +        (etac (flat_flat RS flat_codom RS disjE) 1),
    4.18          (asm_simp_tac HOLCF_ss 1),
    4.19          (asm_simp_tac HOLCF_ss 1)
    4.20          ]);
     5.1 --- a/src/HOLCF/ex/Loop.thy	Mon Feb 17 11:01:10 1997 +0100
     5.2 +++ b/src/HOLCF/ex/Loop.thy	Mon Feb 17 11:04:00 1997 +0100
     5.3 @@ -6,10 +6,9 @@
     5.4  Theory for a loop primitive like while
     5.5  *)
     5.6  
     5.7 -Loop = Tr2 +
     5.8 +Loop = Tr +
     5.9  
    5.10  consts
    5.11 -
    5.12          step  :: "('a -> tr)->('a -> 'a)->'a->'a"
    5.13          while :: "('a -> tr)->('a -> 'a)->'a->'a"
    5.14  
     6.1 --- a/src/HOLCF/ex/Witness.ML	Mon Feb 17 11:01:10 1997 +0100
     6.2 +++ b/src/HOLCF/ex/Witness.ML	Mon Feb 17 11:04:00 1997 +0100
     6.3 @@ -4,7 +4,7 @@
     6.4  (* classes cplus, cminus, ctimes, cdiv introduce 
     6.5     characteristic constants  o+ o- o* o/
     6.6  
     6.7 -	"bullet":: "void -> void -> void"
     6.8 +	"circ":: "one -> one -> one"
     6.9  
    6.10     is the witness for o+ o- o* o/	
    6.11  
    6.12 @@ -18,9 +18,9 @@
    6.13  
    6.14     The witness for these is 
    6.15  
    6.16 -	"cric"	:: "void -> void -> tr"			(cinfixl 55)
    6.17 +	"bullet":: "one -> one -> tr"			(cinfixl 55)
    6.18  
    6.19 -   the classes equiv, eq, qlinear impose additional axioms
    6.20 +   the classes equiv, eq, impose additional axioms
    6.21  *)
    6.22  
    6.23  (* -------------------------------------------------------------------- *)
    6.24 @@ -45,88 +45,85 @@
    6.25  
    6.26  characteristic axioms of class eq:
    6.27  
    6.28 -weq	"[|(x::'a::eq) ~= UU; y ~= UU|] ==> (x = y --> (x .= y)=TT) & (x ~= y --> x .= y)"
    6.29 +weq	"[|(x::'a::eq)~=UU; y~=UU|] ==> (x=y --> (x.=y)=TT) & (x~=y --> x.=y)"
    6.30  
    6.31  
    6.32     --------------------------------------------------------------------
    6.33  
    6.34 -characteristic axioms of class qpo:
    6.35 -
    6.36 -strict_qpo	"(UU .<= x) = UU & (x .<= UU) = UU"
    6.37 -total_qpo	"[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU"
    6.38 -
    6.39 -refl_qpo	"[|x ~= UU|] ==> (x .<= x)=TT"
    6.40 -antisym_qpo	"[|(x .<= y)=TT; (y .<= x)=TT |] ==> (x .= y)=TT"
    6.41 -trans_qpo	"[|(x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT"
    6.42 -antisym_qpo_rev	" (x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" 
    6.43 -
    6.44 -   --------------------------------------------------------------------
    6.45 -
    6.46 -characteristic axioms of class qlinear:
    6.47 -
    6.48 -qlinear	"[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT | (y .<= x)=TT "
    6.49 -
    6.50  *)
    6.51  
    6.52  (* strict_per, strict_qpo *)
    6.53 -val prems = goal thy "(UU circ x) = UU & (x circ UU) = UU";
    6.54 -by (simp_tac (HOLCF_ss addsimps [circ_def]) 1);
    6.55 +goalw thy [bullet_def] "(UU bullet x) = UU & (x bullet UU) = UU";
    6.56 +by (simp_tac (!simpset addsimps [flift1_def,flift2_def,o_def]) 1);
    6.57 +by (lift.induct_tac "x" 1);
    6.58 +auto();
    6.59  result();
    6.60  
    6.61  (* total_per, total_qpo *)
    6.62 -val prems = goal thy "[|x ~= UU; y ~= UU|] ==> (x circ y) ~= UU";
    6.63 +val prems = goal thy "[|x~=UU; y~=UU|] ==> (x bullet y) ~= UU";
    6.64 +by (subgoal_tac "x~=UU&y~=UU-->(x bullet y) ~= UU" 1);
    6.65  by (cut_facts_tac prems 1);
    6.66 -by (etac notE 1);
    6.67 -by (rtac unique_void2 1);
    6.68 +by (fast_tac HOL_cs 1);
    6.69 +by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
    6.70 +by (lift.induct_tac "x" 1);
    6.71 +by (fast_tac HOL_cs 1);
    6.72 +by (lift.induct_tac "y" 1);
    6.73 +auto();
    6.74  result();
    6.75  
    6.76  (* flat_per *)
    6.77  
    6.78 -val prems = goal thy "flat (UU::void)";
    6.79 -by (rtac flat_void 1);
    6.80 +goal thy "flat (x::one)";
    6.81 +by (rtac flat_flat 1);
    6.82  result();
    6.83  
    6.84  (* sym_per *)  
    6.85 -val prems = goal thy "(x circ y) = (y circ x)";
    6.86 -by (simp_tac (HOLCF_ss addsimps [circ_def]) 1);
    6.87 +goalw thy [bullet_def] "(x bullet y) = (y bullet x)";
    6.88 +by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
    6.89 +by (lift.induct_tac "x" 1);
    6.90 +by (lift.induct_tac "y" 2);
    6.91 +by (lift.induct_tac "y" 1);
    6.92 +auto();
    6.93  result();
    6.94  
    6.95  (* trans_per, trans_qpo *)
    6.96 -val prems = goal thy "[|(x bullet y)=TT; (y bullet z)=TT |] ==> (x bullet z)=TT";
    6.97 +val prems = goal thy "[|(x bullet y)=TT; (y bullet z)=TT|] ==>(x bullet z)=TT";
    6.98 +by (subgoal_tac "(x bullet y)=TT&(y bullet z)=TT-->(x bullet z)=TT" 1);
    6.99  by (cut_facts_tac prems 1);
   6.100 -by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
   6.101 +by (fast_tac HOL_cs 1);
   6.102 +by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
   6.103 +by (lift.induct_tac "x" 1);
   6.104 +by (lift.induct_tac "y" 2);
   6.105 +by (lift.induct_tac "y" 1);
   6.106 +by (lift.induct_tac "z" 4);
   6.107 +by (lift.induct_tac "z" 3);
   6.108 +by (lift.induct_tac "z" 2);
   6.109 +by (lift.induct_tac "z" 1);
   6.110 +auto();
   6.111  result();
   6.112  
   6.113  (* refl_per *)
   6.114 -val prems = goal thy "[|(x::void) ~= UU|] ==> (x bullet x)=TT";
   6.115 +val prems = goal thy "x ~= UU ==> (x bullet x)=TT";
   6.116 +by (subgoal_tac "x ~= UU --> (x bullet x)=TT" 1);
   6.117  by (cut_facts_tac prems 1);
   6.118 -by (etac notE 1);
   6.119 -by (rtac unique_void2 1);
   6.120 -result();
   6.121 +by (fast_tac HOL_cs 1);
   6.122 +by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
   6.123 +by (lift.induct_tac "x" 1);
   6.124 +auto();
   6.125 +qed "refl_per_one";
   6.126  
   6.127  (* weq *)
   6.128  val prems = goal thy 
   6.129 -	"[|(x::void) ~= UU; y ~= UU|] ==> (x = y --> (x bullet y)=TT) & (x ~= y --> (x bullet y)=FF)";
   6.130 +	"[|x~=UU; y~=UU|]==>(x=y-->(x bullet y)=TT)&(x~=y-->(x bullet y)=FF)";
   6.131 +by(subgoal_tac"x~=UU&y~=UU-->(x=y-->(x bullet y)=TT)&(x~=y-->(x bullet y)=FF)"1);
   6.132  by (cut_facts_tac prems 1);
   6.133 -by (etac notE 1);
   6.134 -by (rtac unique_void2 1);
   6.135 -result();
   6.136 -
   6.137 -(* antisym_qpo *)
   6.138 -val prems = goal thy "[|(x bullet y)=TT; (y bullet x)=TT |] ==> (x bullet y)=TT";
   6.139 -by (cut_facts_tac prems 1);
   6.140 -by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
   6.141 +by (fast_tac HOL_cs 1);
   6.142 +by (lift.induct_tac "x" 1);
   6.143 +by (lift.induct_tac "y" 2);
   6.144 +by (lift.induct_tac "y" 1);
   6.145 +auto();
   6.146 +br refl_per_one 1;
   6.147 +auto();
   6.148 +by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1);
   6.149  result();
   6.150  
   6.151 -(* antisym_qpo_rev *)
   6.152 -val prems = goal thy "(x bullet y)=TT ==> (x bullet y)=TT & (y bullet x)=TT";
   6.153 -by (cut_facts_tac prems 1);
   6.154 -by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1);
   6.155 -
   6.156 -(* qlinear *)
   6.157 -val prems = goal thy 
   6.158 -	"[|(x::void) ~= UU; y ~= UU|] ==> (x bullet y)=TT | (y bullet x)=TT ";
   6.159 -by (cut_facts_tac prems 1);
   6.160 -by (etac notE 1);
   6.161 -by (rtac unique_void2 1);
   6.162 -result();
     7.1 --- a/src/HOLCF/ex/Witness.thy	Mon Feb 17 11:01:10 1997 +0100
     7.2 +++ b/src/HOLCF/ex/Witness.thy	Mon Feb 17 11:04:00 1997 +0100
     7.3 @@ -1,29 +1,24 @@
     7.4  (*  Title:      FOCUS/Witness.thy
     7.5 -    ID:         $ $
     7.6 +    ID:         $Id$
     7.7      Author:     Franz Regensburger
     7.8      Copyright   1995 Technical University Munich
     7.9  
    7.10  Witnesses for introduction of type cleasse in theory Classlib
    7.11  
    7.12 -The 8bit package is needed for this theory
    7.13 +The type one of HOLCF/One.thy is a witness for all the introduced classes.
    7.14  
    7.15 -The type void of HOLCF/Void.thy is a witness for all the introduced classes.
    7.16 -
    7.17 -the trivial instance for ++ -- ** // is LAM x y.(UU::void) 
    7.18 -the trivial instance for .= and .<=  is LAM x y.(UU::tr)
    7.19 +the trivial instance for ++ -- ** // is circ 
    7.20 +the trivial instance for .= and .<=  is bullet
    7.21  
    7.22  *)
    7.23  
    7.24  Witness = HOLCF +
    7.25  
    7.26  ops curried 
    7.27 -	"circ"	:: "void -> void -> void"		(cinfixl 65)
    7.28 -	"bullet":: "void -> void -> tr"			(cinfixl 55)
    7.29 +	"bullet":: "one -> one -> tr"			(cinfixl 55)
    7.30  
    7.31  defs 
    7.32  
    7.33 -circ_def	"(op circ)  (LAM x y.UU)"
    7.34 -
    7.35 -bullet_def	"(op bullet)  (LAM x y.UU)"
    7.36 +bullet_def	"(op bullet)  flift1(flift2 o (op =))"
    7.37  
    7.38  end