src/HOLCF/sprod2.ML
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 243 c22b85994e17
permissions -rw-r--r--
tidying
     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 val less_sprod3a = prove_goal 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 val less_sprod3b = prove_goal 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 val less_sprod4b = prove_goal 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 val less_sprod4c = prove_goal 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 val minimal_sprod = prove_goal 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 val monofun_Ispair1 = prove_goalw 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 val monofun_Ispair2 = prove_goalw 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 val  monofun_Ispair = prove_goal 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 val  monofun_Isfst = prove_goalw 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 val monofun_Issnd = prove_goalw 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 val lub_sprod = prove_goal 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 (* is_chain(?S1) ==> lub(range(?S1)) =                                     *)
   257 (* Ispair(lub(range(%i. Isfst(?S1(i)))),lub(range(%i. Issnd(?S1(i)))))     *)
   258 
   259 val cpo_sprod = prove_goal Sprod2.thy 
   260 	"is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
   261 (fn prems =>
   262 	[
   263 	(cut_facts_tac prems 1),
   264 	(rtac exI 1),
   265 	(etac lub_sprod 1)
   266 	]);
   267 
   268 
   269 
   270 
   271 
   272 
   273 
   274