src/HOLCF/Sprod2.ML
changeset 1168 74be52691d62
parent 892 d0dc8d057929
child 1461 6bcb44e4d6e5
     1.1 --- a/src/HOLCF/Sprod2.ML	Thu Jun 29 16:16:24 1995 +0200
     1.2 +++ b/src/HOLCF/Sprod2.ML	Thu Jun 29 16:28:40 1995 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  (* ------------------------------------------------------------------------ *)
     1.5  
     1.6  qed_goal "less_sprod3a" Sprod2.thy 
     1.7 -	"p1=Ispair(UU,UU) ==> p1 << p2"
     1.8 +	"p1=Ispair UU UU ==> p1 << p2"
     1.9  (fn prems =>
    1.10  	[
    1.11  	(cut_facts_tac prems 1),
    1.12 @@ -24,7 +24,7 @@
    1.13  
    1.14  
    1.15  qed_goal "less_sprod3b" Sprod2.thy
    1.16 - "~p1=Ispair(UU,UU) ==>\
    1.17 + "p1~=Ispair UU UU ==>\
    1.18  \	(p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))" 
    1.19  (fn prems =>
    1.20  	[
    1.21 @@ -34,7 +34,7 @@
    1.22  	]);
    1.23  
    1.24  qed_goal "less_sprod4b" Sprod2.thy 
    1.25 -	"p << Ispair(UU,UU) ==> p = Ispair(UU,UU)"
    1.26 +	"p << Ispair UU UU ==> p = Ispair UU UU"
    1.27  (fn prems =>
    1.28  	[
    1.29  	(cut_facts_tac prems 1),
    1.30 @@ -43,10 +43,10 @@
    1.31  	]);
    1.32  
    1.33  val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
    1.34 -(* Ispair(?a,?b) << Ispair(UU,UU) ==> ?a = UU | ?b = UU *)
    1.35 +(* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *)
    1.36  
    1.37  qed_goal "less_sprod4c" Sprod2.thy
    1.38 - "[|Ispair(xa,ya)<<Ispair(x,y);~xa=UU;~ya=UU;~x=UU;~y=UU|] ==>\
    1.39 + "[|Ispair xa ya << Ispair x y; xa~=UU; ya~=UU; x~=UU; y~=UU|] ==>\
    1.40  \		xa<<x & ya << y"
    1.41  (fn prems =>
    1.42  	[
    1.43 @@ -60,7 +60,7 @@
    1.44  (* type sprod is pointed                                                    *)
    1.45  (* ------------------------------------------------------------------------ *)
    1.46  
    1.47 -qed_goal "minimal_sprod" Sprod2.thy  "Ispair(UU,UU)<<p"
    1.48 +qed_goal "minimal_sprod" Sprod2.thy  "Ispair UU UU << p"
    1.49  (fn prems =>
    1.50  	[
    1.51  	(rtac less_sprod3a 1),
    1.52 @@ -78,9 +78,9 @@
    1.53  	(rtac (less_fun RS iffD2) 1),
    1.54  	(strip_tac 1),
    1.55  	(res_inst_tac [("Q",
    1.56 -	" Ispair(y,xa) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
    1.57 +	" Ispair y xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
    1.58  	(res_inst_tac [("Q",
    1.59 -	" Ispair(x,xa) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
    1.60 +	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
    1.61  	(rtac (less_sprod3b RS iffD2) 1),
    1.62  	(atac 1),
    1.63  	(rtac conjI 1),
    1.64 @@ -100,9 +100,9 @@
    1.65  	(rtac refl_less 1),
    1.66  	(etac less_sprod3a 1),
    1.67  	(res_inst_tac [("Q",
    1.68 -	" Ispair(x,xa) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
    1.69 +	" Ispair x xa  = Ispair UU UU")] (excluded_middle RS disjE) 1),
    1.70  	(etac less_sprod3a 2),
    1.71 -	(res_inst_tac [("P","Ispair(y,xa) = Ispair(UU,UU)")] notE 1),
    1.72 +	(res_inst_tac [("P","Ispair y xa = Ispair UU UU")] notE 1),
    1.73  	(atac 2),
    1.74  	(rtac defined_Ispair 1),
    1.75  	(etac notUU_I 1),
    1.76 @@ -116,9 +116,9 @@
    1.77  	[
    1.78  	(strip_tac 1),
    1.79  	(res_inst_tac [("Q",
    1.80 -	" Ispair(x,y) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
    1.81 +	" Ispair x y = Ispair UU UU")] (excluded_middle RS disjE) 1),
    1.82  	(res_inst_tac [("Q",
    1.83 -	" Ispair(x,xa) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
    1.84 +	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
    1.85  	(rtac (less_sprod3b RS iffD2) 1),
    1.86  	(atac 1),
    1.87  	(rtac conjI 1),
    1.88 @@ -138,9 +138,9 @@
    1.89  	(atac 1),
    1.90  	(etac less_sprod3a 1),
    1.91  	(res_inst_tac [("Q",
    1.92 -	" Ispair(x,xa) =Ispair(UU,UU)")] (excluded_middle RS disjE) 1),
    1.93 +	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
    1.94  	(etac less_sprod3a 2),
    1.95 -	(res_inst_tac [("P","Ispair(x,y) = Ispair(UU,UU)")] notE 1),
    1.96 +	(res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
    1.97  	(atac 2),
    1.98  	(rtac defined_Ispair 1),
    1.99  	(etac (strict_Ispair_rev RS  conjunct1) 1),
   1.100 @@ -149,7 +149,7 @@
   1.101  	]);
   1.102  
   1.103  qed_goal " monofun_Ispair" Sprod2.thy 
   1.104 - "[|x1<<x2; y1<<y2|] ==> Ispair(x1,y1)<<Ispair(x2,y2)"
   1.105 + "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
   1.106  (fn prems =>
   1.107  	[
   1.108  	(cut_facts_tac prems 1),
   1.109 @@ -179,7 +179,7 @@
   1.110  	(hyp_subst_tac 1),
   1.111  	(res_inst_tac [("p","y")] IsprodE 1),
   1.112  	(hyp_subst_tac 1),
   1.113 -	(res_inst_tac [("t","Isfst(Ispair(xa,ya))")] subst 1),
   1.114 +	(res_inst_tac [("t","Isfst(Ispair xa ya)")] subst 1),
   1.115  	(rtac refl_less 2),
   1.116  	(etac (less_sprod4b RS sym RS arg_cong) 1),
   1.117  	(hyp_subst_tac 1),
   1.118 @@ -206,7 +206,7 @@
   1.119  	(hyp_subst_tac 1),
   1.120  	(res_inst_tac [("p","y")] IsprodE 1),
   1.121  	(hyp_subst_tac 1),
   1.122 -	(res_inst_tac [("t","Issnd(Ispair(xa,ya))")] subst 1),
   1.123 +	(res_inst_tac [("t","Issnd(Ispair xa ya)")] subst 1),
   1.124  	(rtac refl_less 2),
   1.125  	(etac (less_sprod4b RS sym RS arg_cong) 1),
   1.126  	(hyp_subst_tac 1),
   1.127 @@ -227,7 +227,7 @@
   1.128  
   1.129  qed_goal "lub_sprod" Sprod2.thy 
   1.130  "[|is_chain(S)|] ==> range(S) <<| \
   1.131 -\ Ispair(lub(range(%i.Isfst(S(i)))),lub(range(%i.Issnd(S(i)))))"
   1.132 +\ Ispair (lub(range(%i.Isfst(S i)))) (lub(range(%i.Issnd(S i))))"
   1.133  (fn prems =>
   1.134  	[
   1.135  	(cut_facts_tac prems 1),
   1.136 @@ -253,8 +253,7 @@
   1.137  	]);
   1.138  
   1.139  val thelub_sprod = (lub_sprod RS thelubI);
   1.140 -(* is_chain(?S1) ==> lub(range(?S1)) =                                     *)
   1.141 -(* Ispair(lub(range(%i. Isfst(?S1(i)))),lub(range(%i. Issnd(?S1(i)))))     *)
   1.142 +
   1.143  
   1.144  qed_goal "cpo_sprod" Sprod2.thy 
   1.145  	"is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"