src/HOLCF/cprod2.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/cprod2.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for cprod2.thy 
     7 *)
     8 
     9 open Cprod2;
    10 
    11 val less_cprod3a = prove_goal Cprod2.thy 
    12 	"p1=<UU,UU> ==> p1 << p2"
    13  (fn prems =>
    14 	[
    15 	(cut_facts_tac prems 1),
    16 	(rtac (inst_cprod_po RS ssubst) 1),
    17 	(rtac (less_cprod1b RS ssubst) 1),
    18 	(hyp_subst_tac 1),
    19 	(asm_simp_tac pair_ss  1),
    20 	(rtac conjI 1),
    21 	(rtac minimal 1),
    22 	(rtac minimal 1)
    23 	]);
    24 
    25 val less_cprod3b = prove_goal Cprod2.thy
    26  "(p1 << p2) = (fst(p1)<<fst(p2) & snd(p1)<<snd(p2))"
    27  (fn prems =>
    28 	[
    29 	(rtac (inst_cprod_po RS ssubst) 1),
    30 	(rtac less_cprod1b 1)
    31 	]);
    32 
    33 val less_cprod4a = prove_goal Cprod2.thy 
    34 	"<x1,x2> << <UU,UU> ==> x1=UU & x2=UU"
    35  (fn prems =>
    36 	[
    37 	(cut_facts_tac prems 1),
    38 	(rtac less_cprod2a 1),
    39 	(etac (inst_cprod_po RS subst) 1)
    40 	]);
    41 
    42 val less_cprod4b = prove_goal Cprod2.thy 
    43 	"p << <UU,UU> ==> p = <UU,UU>"
    44 (fn prems =>
    45 	[
    46 	(cut_facts_tac prems 1),
    47 	(rtac less_cprod2b 1),
    48 	(etac (inst_cprod_po RS subst) 1)
    49 	]);
    50 
    51 val less_cprod4c = prove_goal Cprod2.thy
    52  " <xa,ya> << <x,y> ==> xa<<x & ya << y"
    53 (fn prems =>
    54 	[
    55 	(cut_facts_tac prems 1),
    56 	(rtac less_cprod2c 1),
    57 	(etac (inst_cprod_po RS subst) 1),
    58 	(REPEAT (atac 1))
    59 	]);
    60 
    61 (* ------------------------------------------------------------------------ *)
    62 (* type cprod is pointed                                                    *)
    63 (* ------------------------------------------------------------------------ *)
    64 
    65 val minimal_cprod = prove_goal Cprod2.thy  "<UU,UU><<p"
    66 (fn prems =>
    67 	[
    68 	(rtac less_cprod3a 1),
    69 	(rtac refl 1)
    70 	]);
    71 
    72 (* ------------------------------------------------------------------------ *)
    73 (* Pair <_,_>  is monotone in both arguments                                *)
    74 (* ------------------------------------------------------------------------ *)
    75 
    76 val monofun_pair1 = prove_goalw Cprod2.thy [monofun] "monofun(Pair)"
    77  (fn prems =>
    78 	[
    79 	(strip_tac 1),
    80 	(rtac (less_fun RS iffD2) 1),
    81 	(strip_tac 1),
    82 	(rtac (less_cprod3b RS iffD2) 1),
    83 	(simp_tac pair_ss 1),
    84 	(asm_simp_tac Cfun_ss 1)
    85 	]);
    86 
    87 val monofun_pair2 = prove_goalw Cprod2.thy [monofun] "monofun(Pair(x))"
    88  (fn prems =>
    89 	[
    90 	(strip_tac 1),
    91 	(rtac (less_cprod3b RS iffD2) 1),
    92 	(simp_tac pair_ss 1),
    93 	(asm_simp_tac Cfun_ss 1)
    94 	]);
    95 
    96 val monofun_pair = prove_goal Cprod2.thy 
    97  "[|x1<<x2; y1<<y2|] ==> <x1,y1> << <x2,y2>"
    98  (fn prems =>
    99 	[
   100 	(cut_facts_tac prems 1),
   101 	(rtac trans_less 1),
   102 	(rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS 
   103 	(less_fun RS iffD1 RS spec)) 1),
   104 	(rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2),
   105 	(atac 1),
   106 	(atac 1)
   107 	]);
   108 
   109 (* ------------------------------------------------------------------------ *)
   110 (* fst and snd are monotone                                                 *)
   111 (* ------------------------------------------------------------------------ *)
   112 
   113 val monofun_fst = prove_goalw Cprod2.thy [monofun] "monofun(fst)"
   114  (fn prems =>
   115 	[
   116 	(strip_tac 1),
   117 	(res_inst_tac [("p","x")] PairE 1),
   118 	(hyp_subst_tac 1),
   119 	(res_inst_tac [("p","y")] PairE 1),
   120 	(hyp_subst_tac 1),
   121 	(asm_simp_tac pair_ss  1),
   122 	(etac (less_cprod4c RS conjunct1) 1)
   123 	]);
   124 
   125 val monofun_snd = prove_goalw Cprod2.thy [monofun] "monofun(snd)"
   126  (fn prems =>
   127 	[
   128 	(strip_tac 1),
   129 	(res_inst_tac [("p","x")] PairE 1),
   130 	(hyp_subst_tac 1),
   131 	(res_inst_tac [("p","y")] PairE 1),
   132 	(hyp_subst_tac 1),
   133 	(asm_simp_tac pair_ss  1),
   134 	(etac (less_cprod4c RS conjunct2) 1)
   135 	]);
   136 
   137 (* ------------------------------------------------------------------------ *)
   138 (* the type 'a * 'b is a cpo                                                *)
   139 (* ------------------------------------------------------------------------ *)
   140 
   141 val lub_cprod = prove_goal Cprod2.thy 
   142 " is_chain(S) ==> range(S) <<| \
   143 \   < lub(range(%i.fst(S(i)))),lub(range(%i.snd(S(i))))> "
   144  (fn prems =>
   145 	[
   146 	(cut_facts_tac prems 1),
   147 	(rtac is_lubI 1),
   148 	(rtac conjI 1),
   149 	(rtac ub_rangeI 1),
   150 	(rtac allI 1),
   151 	(res_inst_tac [("t","S(i)")] (surjective_pairing RS ssubst) 1),
   152 	(rtac monofun_pair 1),
   153 	(rtac is_ub_thelub 1),
   154 	(etac (monofun_fst RS ch2ch_monofun) 1),
   155 	(rtac is_ub_thelub 1),
   156 	(etac (monofun_snd RS ch2ch_monofun) 1),
   157 	(strip_tac 1),
   158 	(res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1),
   159 	(rtac monofun_pair 1),
   160 	(rtac is_lub_thelub 1),
   161 	(etac (monofun_fst RS ch2ch_monofun) 1),
   162 	(etac (monofun_fst RS ub2ub_monofun) 1),
   163 	(rtac is_lub_thelub 1),
   164 	(etac (monofun_snd RS ch2ch_monofun) 1),
   165 	(etac (monofun_snd RS ub2ub_monofun) 1)
   166 	]);
   167 
   168 val thelub_cprod = (lub_cprod RS thelubI);
   169 (* "is_chain(?S1) ==> lub(range(?S1)) =                                *)
   170 (*  <lub(range(%i. fst(?S1(i)))), lub(range(%i. snd(?S1(i))))>"        *)
   171 
   172 
   173 val cpo_cprod = prove_goal Cprod2.thy 
   174 	"is_chain(S::nat=>'a*'b)==>? x.range(S)<<| x"
   175 (fn prems =>
   176 	[
   177 	(cut_facts_tac prems 1),
   178 	(rtac exI 1),
   179 	(etac lub_cprod 1)
   180 	]);
   181