src/HOLCF/Sprod2.ML
changeset 2640 ee4dfce170a0
parent 2033 639de962ded4
child 3323 194ae2e0c193
     1.1 --- a/src/HOLCF/Sprod2.ML	Sat Feb 15 18:24:05 1997 +0100
     1.2 +++ b/src/HOLCF/Sprod2.ML	Mon Feb 17 10:57:11 1997 +0100
     1.3 @@ -1,70 +1,38 @@
     1.4 -(*  Title:      HOLCF/sprod2.ML
     1.5 +(*  Title:      HOLCF/Sprod2.ML
     1.6      ID:         $Id$
     1.7      Author:     Franz Regensburger
     1.8      Copyright   1993 Technische Universitaet Muenchen
     1.9  
    1.10 -Lemmas for sprod2.thy
    1.11 +Lemmas for Sprod2.thy
    1.12  *)
    1.13  
    1.14 -
    1.15  open Sprod2;
    1.16  
    1.17 -(* ------------------------------------------------------------------------ *)
    1.18 -(* access to less_sprod in class po                                         *)
    1.19 -(* ------------------------------------------------------------------------ *)
    1.20 -
    1.21 -qed_goal "less_sprod3a" Sprod2.thy 
    1.22 -        "p1=Ispair UU UU ==> p1 << p2"
    1.23 -(fn prems =>
    1.24 -        [
    1.25 -        (cut_facts_tac prems 1),
    1.26 -        (stac inst_sprod_po 1),
    1.27 -        (etac less_sprod1a 1)
    1.28 -        ]);
    1.29 -
    1.30 -
    1.31 -qed_goal "less_sprod3b" Sprod2.thy
    1.32 - "p1~=Ispair UU UU ==>\
    1.33 -\       (p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))" 
    1.34 -(fn prems =>
    1.35 +(* for compatibility with old HOLCF-Version *)
    1.36 +qed_goal "inst_sprod_po" thy "(op <<)=(%x y.Isfst x<<Isfst y&Issnd x<<Issnd y)"
    1.37 + (fn prems => 
    1.38          [
    1.39 -        (cut_facts_tac prems 1),
    1.40 -        (stac inst_sprod_po 1),
    1.41 -        (etac less_sprod1b 1)
    1.42 -        ]);
    1.43 -
    1.44 -qed_goal "less_sprod4b" Sprod2.thy 
    1.45 -        "p << Ispair UU UU ==> p = Ispair UU UU"
    1.46 -(fn prems =>
    1.47 -        [
    1.48 -        (cut_facts_tac prems 1),
    1.49 -        (rtac less_sprod2b 1),
    1.50 -        (etac (inst_sprod_po RS subst) 1)
    1.51 -        ]);
    1.52 -
    1.53 -bind_thm ("less_sprod4a", less_sprod4b RS defined_Ispair_rev);
    1.54 -(* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *)
    1.55 -
    1.56 -qed_goal "less_sprod4c" Sprod2.thy
    1.57 - "[|Ispair xa ya << Ispair x y; xa~=UU; ya~=UU; x~=UU; y~=UU|] ==>\
    1.58 -\               xa<<x & ya << y"
    1.59 -(fn prems =>
    1.60 -        [
    1.61 -        (cut_facts_tac prems 1),
    1.62 -        (rtac less_sprod2c 1),
    1.63 -        (etac (inst_sprod_po RS subst) 1),
    1.64 -        (REPEAT (atac 1))
    1.65 +	(fold_goals_tac [po_def,less_sprod_def]),
    1.66 +	(rtac refl 1)
    1.67          ]);
    1.68  
    1.69  (* ------------------------------------------------------------------------ *)
    1.70  (* type sprod is pointed                                                    *)
    1.71  (* ------------------------------------------------------------------------ *)
    1.72  
    1.73 -qed_goal "minimal_sprod" Sprod2.thy  "Ispair UU UU << p"
    1.74 +qed_goal "minimal_sprod" thy "Ispair UU UU << p"
    1.75  (fn prems =>
    1.76          [
    1.77 -        (rtac less_sprod3a 1),
    1.78 -        (rtac refl 1)
    1.79 +        (simp_tac(Sprod0_ss addsimps[inst_sprod_po,minimal])1)
    1.80 +        ]);
    1.81 +
    1.82 +bind_thm ("UU_sprod_def",minimal_sprod RS minimal2UU RS sym);
    1.83 +
    1.84 +qed_goal "least_sprod" thy "? x::'a**'b.!y.x<<y"
    1.85 +(fn prems =>
    1.86 +        [
    1.87 +        (res_inst_tac [("x","Ispair UU UU")] exI 1),
    1.88 +        (rtac (minimal_sprod RS allI) 1)
    1.89          ]);
    1.90  
    1.91  (* ------------------------------------------------------------------------ *)
    1.92 @@ -77,77 +45,27 @@
    1.93          (strip_tac 1),
    1.94          (rtac (less_fun RS iffD2) 1),
    1.95          (strip_tac 1),
    1.96 -        (res_inst_tac [("Q",
    1.97 -        " Ispair y xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
    1.98 -        (res_inst_tac [("Q",
    1.99 -        " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.100 -        (rtac (less_sprod3b RS iffD2) 1),
   1.101 -        (atac 1),
   1.102 -        (rtac conjI 1),
   1.103 -        (stac Isfst 1),
   1.104 -        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.105 -        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.106 -        (stac Isfst 1),
   1.107 -        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.108 -        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.109 +        (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
   1.110 +        (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   1.111 +        (forward_tac [notUU_I] 1),
   1.112          (atac 1),
   1.113 -        (stac Issnd 1),
   1.114 -        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.115 -        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.116 -        (stac Issnd 1),
   1.117 -        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.118 -        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.119 -        (rtac refl_less 1),
   1.120 -        (etac less_sprod3a 1),
   1.121 -        (res_inst_tac [("Q",
   1.122 -        " Ispair x xa  = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.123 -        (etac less_sprod3a 2),
   1.124 -        (res_inst_tac [("P","Ispair y xa = Ispair UU UU")] notE 1),
   1.125 -        (atac 2),
   1.126 -        (rtac defined_Ispair 1),
   1.127 -        (etac notUU_I 1),
   1.128 -        (etac (strict_Ispair_rev RS  conjunct1) 1),
   1.129 -        (etac (strict_Ispair_rev RS  conjunct2) 1)
   1.130 +        (REPEAT(asm_simp_tac(Sprod0_ss 
   1.131 +                addsimps[inst_sprod_po,refl_less,minimal]) 1))
   1.132          ]);
   1.133  
   1.134 -
   1.135  qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))"
   1.136  (fn prems =>
   1.137          [
   1.138          (strip_tac 1),
   1.139 -        (res_inst_tac [("Q",
   1.140 -        " Ispair x y = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.141 -        (res_inst_tac [("Q",
   1.142 -        " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.143 -        (rtac (less_sprod3b RS iffD2) 1),
   1.144 +        (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   1.145 +        (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
   1.146 +        (forward_tac [notUU_I] 1),
   1.147          (atac 1),
   1.148 -        (rtac conjI 1),
   1.149 -        (stac Isfst 1),
   1.150 -        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.151 -        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.152 -        (stac Isfst 1),
   1.153 -        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.154 -        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.155 -        (rtac refl_less 1),
   1.156 -        (stac Issnd 1),
   1.157 -        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.158 -        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.159 -        (stac Issnd 1),
   1.160 -        (etac (strict_Ispair_rev RS conjunct1) 1),
   1.161 -        (etac (strict_Ispair_rev RS conjunct2) 1),
   1.162 -        (atac 1),
   1.163 -        (etac less_sprod3a 1),
   1.164 -        (res_inst_tac [("Q",
   1.165 -        " Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   1.166 -        (etac less_sprod3a 2),
   1.167 -        (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
   1.168 -        (atac 2),
   1.169 -        (rtac defined_Ispair 1),
   1.170 -        (etac (strict_Ispair_rev RS  conjunct1) 1),
   1.171 -        (etac notUU_I 1),
   1.172 -        (etac (strict_Ispair_rev RS  conjunct2) 1)
   1.173 +        (REPEAT(asm_simp_tac(Sprod0_ss 
   1.174 +                addsimps[inst_sprod_po,refl_less,minimal]) 1))
   1.175          ]);
   1.176  
   1.177 +
   1.178  qed_goal " monofun_Ispair" Sprod2.thy 
   1.179   "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
   1.180  (fn prems =>
   1.181 @@ -166,60 +84,11 @@
   1.182  (* Isfst and Issnd are monotone                                             *)
   1.183  (* ------------------------------------------------------------------------ *)
   1.184  
   1.185 -qed_goalw " monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
   1.186 -(fn prems =>
   1.187 -        [
   1.188 -        (strip_tac 1),
   1.189 -        (res_inst_tac [("p","x")] IsprodE 1),
   1.190 -        (hyp_subst_tac 1),
   1.191 -        (rtac trans_less 1),
   1.192 -        (rtac minimal 2),
   1.193 -        (stac strict_Isfst1 1),
   1.194 -        (rtac refl_less 1),
   1.195 -        (hyp_subst_tac 1),
   1.196 -        (res_inst_tac [("p","y")] IsprodE 1),
   1.197 -        (hyp_subst_tac 1),
   1.198 -        (res_inst_tac [("t","Isfst(Ispair xa ya)")] subst 1),
   1.199 -        (rtac refl_less 2),
   1.200 -        (etac (less_sprod4b RS sym RS arg_cong) 1),
   1.201 -        (hyp_subst_tac 1),
   1.202 -        (stac Isfst 1),
   1.203 -        (atac 1),
   1.204 -        (atac 1),
   1.205 -        (stac Isfst 1),
   1.206 -        (atac 1),
   1.207 -        (atac 1),
   1.208 -        (etac (less_sprod4c RS  conjunct1) 1),
   1.209 -        (REPEAT (atac 1))
   1.210 -        ]);
   1.211 +qed_goalw "monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
   1.212 +(fn prems => [(simp_tac (HOL_ss addsimps [inst_sprod_po]) 1)]);
   1.213  
   1.214  qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)"
   1.215 -(fn prems =>
   1.216 -        [
   1.217 -        (strip_tac 1),
   1.218 -        (res_inst_tac [("p","x")] IsprodE 1),
   1.219 -        (hyp_subst_tac 1),
   1.220 -        (rtac trans_less 1),
   1.221 -        (rtac minimal 2),
   1.222 -        (stac strict_Issnd1 1),
   1.223 -        (rtac refl_less 1),
   1.224 -        (hyp_subst_tac 1),
   1.225 -        (res_inst_tac [("p","y")] IsprodE 1),
   1.226 -        (hyp_subst_tac 1),
   1.227 -        (res_inst_tac [("t","Issnd(Ispair xa ya)")] subst 1),
   1.228 -        (rtac refl_less 2),
   1.229 -        (etac (less_sprod4b RS sym RS arg_cong) 1),
   1.230 -        (hyp_subst_tac 1),
   1.231 -        (stac Issnd 1),
   1.232 -        (atac 1),
   1.233 -        (atac 1),
   1.234 -        (stac Issnd 1),
   1.235 -        (atac 1),
   1.236 -        (atac 1),
   1.237 -        (etac (less_sprod4c RS  conjunct2) 1),
   1.238 -        (REPEAT (atac 1))
   1.239 -        ]);
   1.240 -
   1.241 +(fn prems => [(simp_tac (HOL_ss addsimps [inst_sprod_po]) 1)]);
   1.242  
   1.243  (* ------------------------------------------------------------------------ *)
   1.244  (* the type 'a ** 'b is a cpo                                               *)
   1.245 @@ -231,10 +100,8 @@
   1.246  (fn prems =>
   1.247          [
   1.248          (cut_facts_tac prems 1),
   1.249 -        (rtac is_lubI 1),
   1.250 -        (rtac conjI 1),
   1.251 -        (rtac ub_rangeI 1),
   1.252 -        (rtac allI 1),
   1.253 +        (rtac (conjI RS is_lubI) 1),
   1.254 +        (rtac (allI RS ub_rangeI) 1),
   1.255          (res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1),
   1.256          (rtac monofun_Ispair 1),
   1.257          (rtac is_ub_thelub 1),