src/HOLCF/Sprod2.ML
author regensbu
Thu Jun 29 16:28:40 1995 +0200 (1995-06-29)
changeset 1168 74be52691d62
parent 892 d0dc8d057929
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
The curried version of HOLCF is now just called HOLCF. The old
uncurried version is no longer supported
     1 (*  Title: 	HOLCF/sprod2.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for sprod2.thy
     7 *)
     8 
     9 
    10 open Sprod2;
    11 
    12 (* ------------------------------------------------------------------------ *)
    13 (* access to less_sprod in class po                                         *)
    14 (* ------------------------------------------------------------------------ *)
    15 
    16 qed_goal "less_sprod3a" Sprod2.thy 
    17 	"p1=Ispair UU UU ==> p1 << p2"
    18 (fn prems =>
    19 	[
    20 	(cut_facts_tac prems 1),
    21 	(rtac (inst_sprod_po RS ssubst) 1),
    22 	(etac less_sprod1a 1)
    23 	]);
    24 
    25 
    26 qed_goal "less_sprod3b" Sprod2.thy
    27  "p1~=Ispair UU UU ==>\
    28 \	(p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))" 
    29 (fn prems =>
    30 	[
    31 	(cut_facts_tac prems 1),
    32 	(rtac (inst_sprod_po RS ssubst) 1),
    33 	(etac less_sprod1b 1)
    34 	]);
    35 
    36 qed_goal "less_sprod4b" Sprod2.thy 
    37 	"p << Ispair UU UU ==> p = Ispair UU UU"
    38 (fn prems =>
    39 	[
    40 	(cut_facts_tac prems 1),
    41 	(rtac less_sprod2b 1),
    42 	(etac (inst_sprod_po RS subst) 1)
    43 	]);
    44 
    45 val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
    46 (* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *)
    47 
    48 qed_goal "less_sprod4c" Sprod2.thy
    49  "[|Ispair xa ya << Ispair x y; xa~=UU; ya~=UU; x~=UU; y~=UU|] ==>\
    50 \		xa<<x & ya << y"
    51 (fn prems =>
    52 	[
    53 	(cut_facts_tac prems 1),
    54 	(rtac less_sprod2c 1),
    55 	(etac (inst_sprod_po RS subst) 1),
    56 	(REPEAT (atac 1))
    57 	]);
    58 
    59 (* ------------------------------------------------------------------------ *)
    60 (* type sprod is pointed                                                    *)
    61 (* ------------------------------------------------------------------------ *)
    62 
    63 qed_goal "minimal_sprod" Sprod2.thy  "Ispair UU UU << p"
    64 (fn prems =>
    65 	[
    66 	(rtac less_sprod3a 1),
    67 	(rtac refl 1)
    68 	]);
    69 
    70 (* ------------------------------------------------------------------------ *)
    71 (* Ispair is monotone in both arguments                                     *)
    72 (* ------------------------------------------------------------------------ *)
    73 
    74 qed_goalw "monofun_Ispair1" Sprod2.thy [monofun] "monofun(Ispair)"
    75 (fn prems =>
    76 	[
    77 	(strip_tac 1),
    78 	(rtac (less_fun RS iffD2) 1),
    79 	(strip_tac 1),
    80 	(res_inst_tac [("Q",
    81 	" Ispair y xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
    82 	(res_inst_tac [("Q",
    83 	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
    84 	(rtac (less_sprod3b RS iffD2) 1),
    85 	(atac 1),
    86 	(rtac conjI 1),
    87 	(rtac (Isfst RS ssubst) 1),
    88 	(etac (strict_Ispair_rev RS conjunct1) 1),
    89 	(etac (strict_Ispair_rev RS conjunct2) 1),
    90 	(rtac (Isfst RS ssubst) 1),
    91 	(etac (strict_Ispair_rev RS conjunct1) 1),
    92 	(etac (strict_Ispair_rev RS conjunct2) 1),
    93 	(atac 1),
    94 	(rtac (Issnd RS ssubst) 1),
    95 	(etac (strict_Ispair_rev RS conjunct1) 1),
    96 	(etac (strict_Ispair_rev RS conjunct2) 1),
    97 	(rtac (Issnd RS ssubst) 1),
    98 	(etac (strict_Ispair_rev RS conjunct1) 1),
    99 	(etac (strict_Ispair_rev RS conjunct2) 1),
   100 	(rtac refl_less 1),
   101 	(etac less_sprod3a 1),
   102 	(res_inst_tac [("Q",
   103 	" Ispair x xa  = Ispair UU UU")] (excluded_middle RS disjE) 1),
   104 	(etac less_sprod3a 2),
   105 	(res_inst_tac [("P","Ispair y xa = Ispair UU UU")] notE 1),
   106 	(atac 2),
   107 	(rtac defined_Ispair 1),
   108 	(etac notUU_I 1),
   109 	(etac (strict_Ispair_rev RS  conjunct1) 1),
   110 	(etac (strict_Ispair_rev RS  conjunct2) 1)
   111 	]);
   112 
   113 
   114 qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))"
   115 (fn prems =>
   116 	[
   117 	(strip_tac 1),
   118 	(res_inst_tac [("Q",
   119 	" Ispair x y = Ispair UU UU")] (excluded_middle RS disjE) 1),
   120 	(res_inst_tac [("Q",
   121 	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   122 	(rtac (less_sprod3b RS iffD2) 1),
   123 	(atac 1),
   124 	(rtac conjI 1),
   125 	(rtac (Isfst RS ssubst) 1),
   126 	(etac (strict_Ispair_rev RS conjunct1) 1),
   127 	(etac (strict_Ispair_rev RS conjunct2) 1),
   128 	(rtac (Isfst RS ssubst) 1),
   129 	(etac (strict_Ispair_rev RS conjunct1) 1),
   130 	(etac (strict_Ispair_rev RS conjunct2) 1),
   131 	(rtac refl_less 1),
   132 	(rtac (Issnd RS ssubst) 1),
   133 	(etac (strict_Ispair_rev RS conjunct1) 1),
   134 	(etac (strict_Ispair_rev RS conjunct2) 1),
   135 	(rtac (Issnd RS ssubst) 1),
   136 	(etac (strict_Ispair_rev RS conjunct1) 1),
   137 	(etac (strict_Ispair_rev RS conjunct2) 1),
   138 	(atac 1),
   139 	(etac less_sprod3a 1),
   140 	(res_inst_tac [("Q",
   141 	" Ispair x xa = Ispair UU UU")] (excluded_middle RS disjE) 1),
   142 	(etac less_sprod3a 2),
   143 	(res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
   144 	(atac 2),
   145 	(rtac defined_Ispair 1),
   146 	(etac (strict_Ispair_rev RS  conjunct1) 1),
   147 	(etac notUU_I 1),
   148 	(etac (strict_Ispair_rev RS  conjunct2) 1)
   149 	]);
   150 
   151 qed_goal " monofun_Ispair" Sprod2.thy 
   152  "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
   153 (fn prems =>
   154 	[
   155 	(cut_facts_tac prems 1),
   156 	(rtac trans_less 1),
   157 	(rtac (monofun_Ispair1 RS monofunE RS spec RS spec RS mp RS 
   158 	(less_fun RS iffD1 RS spec)) 1),
   159 	(rtac (monofun_Ispair2 RS monofunE RS spec RS spec RS mp) 2),
   160 	(atac 1),
   161 	(atac 1)
   162 	]);
   163 
   164 
   165 (* ------------------------------------------------------------------------ *)
   166 (* Isfst and Issnd are monotone                                             *)
   167 (* ------------------------------------------------------------------------ *)
   168 
   169 qed_goalw " monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
   170 (fn prems =>
   171 	[
   172 	(strip_tac 1),
   173 	(res_inst_tac [("p","x")] IsprodE 1),
   174 	(hyp_subst_tac 1),
   175 	(rtac trans_less 1),
   176 	(rtac minimal 2),
   177 	(rtac (strict_Isfst1 RS ssubst) 1),
   178 	(rtac refl_less 1),
   179 	(hyp_subst_tac 1),
   180 	(res_inst_tac [("p","y")] IsprodE 1),
   181 	(hyp_subst_tac 1),
   182 	(res_inst_tac [("t","Isfst(Ispair xa ya)")] subst 1),
   183 	(rtac refl_less 2),
   184 	(etac (less_sprod4b RS sym RS arg_cong) 1),
   185 	(hyp_subst_tac 1),
   186 	(rtac (Isfst RS ssubst) 1),
   187 	(atac 1),
   188 	(atac 1),
   189 	(rtac (Isfst RS ssubst) 1),
   190 	(atac 1),
   191 	(atac 1),
   192 	(etac (less_sprod4c RS  conjunct1) 1),
   193 	(REPEAT (atac 1))
   194 	]);
   195 
   196 qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)"
   197 (fn prems =>
   198 	[
   199 	(strip_tac 1),
   200 	(res_inst_tac [("p","x")] IsprodE 1),
   201 	(hyp_subst_tac 1),
   202 	(rtac trans_less 1),
   203 	(rtac minimal 2),
   204 	(rtac (strict_Issnd1 RS ssubst) 1),
   205 	(rtac refl_less 1),
   206 	(hyp_subst_tac 1),
   207 	(res_inst_tac [("p","y")] IsprodE 1),
   208 	(hyp_subst_tac 1),
   209 	(res_inst_tac [("t","Issnd(Ispair xa ya)")] subst 1),
   210 	(rtac refl_less 2),
   211 	(etac (less_sprod4b RS sym RS arg_cong) 1),
   212 	(hyp_subst_tac 1),
   213 	(rtac (Issnd RS ssubst) 1),
   214 	(atac 1),
   215 	(atac 1),
   216 	(rtac (Issnd RS ssubst) 1),
   217 	(atac 1),
   218 	(atac 1),
   219 	(etac (less_sprod4c RS  conjunct2) 1),
   220 	(REPEAT (atac 1))
   221 	]);
   222 
   223 
   224 (* ------------------------------------------------------------------------ *)
   225 (* the type 'a ** 'b is a cpo                                               *)
   226 (* ------------------------------------------------------------------------ *)
   227 
   228 qed_goal "lub_sprod" Sprod2.thy 
   229 "[|is_chain(S)|] ==> range(S) <<| \
   230 \ Ispair (lub(range(%i.Isfst(S i)))) (lub(range(%i.Issnd(S i))))"
   231 (fn prems =>
   232 	[
   233 	(cut_facts_tac prems 1),
   234 	(rtac is_lubI 1),
   235 	(rtac conjI 1),
   236 	(rtac ub_rangeI 1),
   237 	(rtac allI 1),
   238 	(res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1),
   239 	(rtac monofun_Ispair 1),
   240 	(rtac is_ub_thelub 1),
   241 	(etac (monofun_Isfst RS ch2ch_monofun) 1),
   242 	(rtac is_ub_thelub 1),
   243 	(etac (monofun_Issnd RS ch2ch_monofun) 1),
   244 	(strip_tac 1),
   245 	(res_inst_tac [("t","u")] (surjective_pairing_Sprod RS ssubst) 1),
   246 	(rtac monofun_Ispair 1),
   247 	(rtac is_lub_thelub 1),
   248 	(etac (monofun_Isfst RS ch2ch_monofun) 1),
   249 	(etac (monofun_Isfst RS ub2ub_monofun) 1),
   250 	(rtac is_lub_thelub 1),
   251 	(etac (monofun_Issnd RS ch2ch_monofun) 1),
   252 	(etac (monofun_Issnd RS ub2ub_monofun) 1)
   253 	]);
   254 
   255 val thelub_sprod = (lub_sprod RS thelubI);
   256 
   257 
   258 qed_goal "cpo_sprod" Sprod2.thy 
   259 	"is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
   260 (fn prems =>
   261 	[
   262 	(cut_facts_tac prems 1),
   263 	(rtac exI 1),
   264 	(etac lub_sprod 1)
   265 	]);
   266 
   267 
   268 
   269 
   270 
   271 
   272 
   273