src/HOLCF/Sprod2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4721 c8a8482a8124
child 7499 23e090051cb8
permissions -rw-r--r--
made tutorial first;
     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 open Sprod2;
    10 
    11 (* for compatibility with old HOLCF-Version *)
    12 qed_goal "inst_sprod_po" thy "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
    13  (fn prems => 
    14         [
    15 	(fold_goals_tac [less_sprod_def]),
    16 	(rtac refl 1)
    17         ]);
    18 
    19 (* ------------------------------------------------------------------------ *)
    20 (* type sprod is pointed                                                    *)
    21 (* ------------------------------------------------------------------------ *)
    22 
    23 qed_goal "minimal_sprod" thy "Ispair UU UU << p"
    24 (fn prems =>
    25         [
    26         (simp_tac(Sprod0_ss addsimps[inst_sprod_po,minimal])1)
    27         ]);
    28 
    29 bind_thm ("UU_sprod_def",minimal_sprod RS minimal2UU RS sym);
    30 
    31 qed_goal "least_sprod" thy "? x::'a**'b.!y. x<<y"
    32 (fn prems =>
    33         [
    34         (res_inst_tac [("x","Ispair UU UU")] exI 1),
    35         (rtac (minimal_sprod RS allI) 1)
    36         ]);
    37 
    38 (* ------------------------------------------------------------------------ *)
    39 (* Ispair is monotone in both arguments                                     *)
    40 (* ------------------------------------------------------------------------ *)
    41 
    42 qed_goalw "monofun_Ispair1" Sprod2.thy [monofun] "monofun(Ispair)"
    43 (fn prems =>
    44         [
    45         (strip_tac 1),
    46         (rtac (less_fun RS iffD2) 1),
    47         (strip_tac 1),
    48         (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
    49         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
    50         (forward_tac [notUU_I] 1),
    51         (atac 1),
    52         (REPEAT(asm_simp_tac(Sprod0_ss 
    53                 addsimps[inst_sprod_po,refl_less,minimal]) 1))
    54         ]);
    55 
    56 qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))"
    57 (fn prems =>
    58         [
    59         (strip_tac 1),
    60         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
    61         (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
    62         (forward_tac [notUU_I] 1),
    63         (atac 1),
    64         (REPEAT(asm_simp_tac(Sprod0_ss 
    65                 addsimps[inst_sprod_po,refl_less,minimal]) 1))
    66         ]);
    67 
    68 
    69 qed_goal "monofun_Ispair" Sprod2.thy 
    70  "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
    71 (fn prems =>
    72         [
    73         (cut_facts_tac prems 1),
    74         (rtac trans_less 1),
    75         (rtac (monofun_Ispair1 RS monofunE RS spec RS spec RS mp RS 
    76         (less_fun RS iffD1 RS spec)) 1),
    77         (rtac (monofun_Ispair2 RS monofunE RS spec RS spec RS mp) 2),
    78         (atac 1),
    79         (atac 1)
    80         ]);
    81 
    82 
    83 (* ------------------------------------------------------------------------ *)
    84 (* Isfst and Issnd are monotone                                             *)
    85 (* ------------------------------------------------------------------------ *)
    86 
    87 qed_goalw "monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
    88 (fn prems => [(simp_tac (HOL_ss addsimps [inst_sprod_po]) 1)]);
    89 
    90 qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)"
    91 (fn prems => [(simp_tac (HOL_ss addsimps [inst_sprod_po]) 1)]);
    92 
    93 (* ------------------------------------------------------------------------ *)
    94 (* the type 'a ** 'b is a cpo                                               *)
    95 (* ------------------------------------------------------------------------ *)
    96 
    97 qed_goal "lub_sprod" Sprod2.thy 
    98 "[|chain(S)|] ==> range(S) <<| \
    99 \ Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
   100 (fn prems =>
   101         [
   102         (cut_facts_tac prems 1),
   103         (rtac (conjI RS is_lubI) 1),
   104         (rtac (allI RS ub_rangeI) 1),
   105         (res_inst_tac [("t","S(i)")] (surjective_pairing_Sprod RS ssubst) 1),
   106         (rtac monofun_Ispair 1),
   107         (rtac is_ub_thelub 1),
   108         (etac (monofun_Isfst RS ch2ch_monofun) 1),
   109         (rtac is_ub_thelub 1),
   110         (etac (monofun_Issnd RS ch2ch_monofun) 1),
   111         (strip_tac 1),
   112         (res_inst_tac [("t","u")] (surjective_pairing_Sprod RS ssubst) 1),
   113         (rtac monofun_Ispair 1),
   114         (rtac is_lub_thelub 1),
   115         (etac (monofun_Isfst RS ch2ch_monofun) 1),
   116         (etac (monofun_Isfst RS ub2ub_monofun) 1),
   117         (rtac is_lub_thelub 1),
   118         (etac (monofun_Issnd RS ch2ch_monofun) 1),
   119         (etac (monofun_Issnd RS ub2ub_monofun) 1)
   120         ]);
   121 
   122 bind_thm ("thelub_sprod", lub_sprod RS thelubI);
   123 
   124 
   125 qed_goal "cpo_sprod" Sprod2.thy 
   126         "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
   127 (fn prems =>
   128         [
   129         (cut_facts_tac prems 1),
   130         (rtac exI 1),
   131         (etac lub_sprod 1)
   132         ]);
   133 
   134 
   135 
   136 
   137 
   138 
   139 
   140