src/HOLCF/Cprod2.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4721 c8a8482a8124
child 9245 428385c4bc50
permissions -rw-r--r--
made tutorial first;
clasohm@1461
     1
(*  Title:      HOLCF/cprod2.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
Lemmas for cprod2.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Cprod2;
nipkow@243
    10
slotosch@2640
    11
(* for compatibility with old HOLCF-Version *)
wenzelm@3842
    12
qed_goal "inst_cprod_po" thy "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
slotosch@2640
    13
 (fn prems => 
slotosch@2640
    14
        [
slotosch@3323
    15
        (fold_goals_tac [less_cprod_def]),
slotosch@2640
    16
        (rtac refl 1)
slotosch@2640
    17
        ]);
slotosch@2640
    18
slotosch@2640
    19
qed_goalw "less_cprod4c" thy [inst_cprod_po RS eq_reflection]
slotosch@2640
    20
 "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"
nipkow@243
    21
 (fn prems =>
clasohm@1461
    22
        [
clasohm@1461
    23
        (cut_facts_tac prems 1),
slotosch@2640
    24
        (etac conjE 1),
slotosch@2640
    25
        (dtac (fst_conv RS subst) 1),
slotosch@2640
    26
        (dtac (fst_conv RS subst) 1),
slotosch@2640
    27
        (dtac (fst_conv RS subst) 1),
slotosch@2640
    28
        (dtac (snd_conv RS subst) 1),
slotosch@2640
    29
        (dtac (snd_conv RS subst) 1),
slotosch@2640
    30
        (dtac (snd_conv RS subst) 1),
slotosch@2640
    31
        (rtac conjI 1),
slotosch@2640
    32
        (atac 1),
slotosch@2640
    33
        (atac 1)
clasohm@1461
    34
        ]);
nipkow@243
    35
nipkow@243
    36
(* ------------------------------------------------------------------------ *)
nipkow@243
    37
(* type cprod is pointed                                                    *)
nipkow@243
    38
(* ------------------------------------------------------------------------ *)
nipkow@243
    39
slotosch@2640
    40
qed_goal "minimal_cprod" thy  "(UU,UU)<<p"
nipkow@243
    41
(fn prems =>
clasohm@1461
    42
        [
wenzelm@4098
    43
        (simp_tac(simpset() addsimps[inst_cprod_po])1)
slotosch@2640
    44
        ]);
slotosch@2640
    45
slotosch@2640
    46
bind_thm ("UU_cprod_def",minimal_cprod RS minimal2UU RS sym);
slotosch@2640
    47
wenzelm@3842
    48
qed_goal "least_cprod" thy "? x::'a*'b.!y. x<<y"
slotosch@2640
    49
(fn prems =>
slotosch@2640
    50
        [
slotosch@2640
    51
        (res_inst_tac [("x","(UU,UU)")] exI 1),
slotosch@2640
    52
        (rtac (minimal_cprod RS allI) 1)
clasohm@1461
    53
        ]);
nipkow@243
    54
nipkow@243
    55
(* ------------------------------------------------------------------------ *)
nipkow@243
    56
(* Pair <_,_>  is monotone in both arguments                                *)
nipkow@243
    57
(* ------------------------------------------------------------------------ *)
nipkow@243
    58
slotosch@2640
    59
qed_goalw "monofun_pair1" thy [monofun] "monofun Pair"
nipkow@243
    60
 (fn prems =>
clasohm@1461
    61
        [
clasohm@1461
    62
        (strip_tac 1),
clasohm@1461
    63
        (rtac (less_fun RS iffD2) 1),
clasohm@1461
    64
        (strip_tac 1),
wenzelm@4098
    65
        (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1)
clasohm@1461
    66
        ]);
nipkow@243
    67
slotosch@2640
    68
qed_goalw "monofun_pair2" thy [monofun] "monofun(Pair x)"
nipkow@243
    69
 (fn prems =>
clasohm@1461
    70
        [
wenzelm@4098
    71
        (asm_simp_tac (simpset() addsimps [inst_cprod_po]) 1)
clasohm@1461
    72
        ]);
nipkow@243
    73
slotosch@3323
    74
qed_goal "monofun_pair" thy "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
nipkow@243
    75
 (fn prems =>
clasohm@1461
    76
        [
clasohm@1461
    77
        (cut_facts_tac prems 1),
clasohm@1461
    78
        (rtac trans_less 1),
clasohm@1461
    79
        (rtac (monofun_pair1 RS monofunE RS spec RS spec RS mp RS 
clasohm@1461
    80
        (less_fun RS iffD1 RS spec)) 1),
clasohm@1461
    81
        (rtac (monofun_pair2 RS monofunE RS spec RS spec RS mp) 2),
clasohm@1461
    82
        (atac 1),
clasohm@1461
    83
        (atac 1)
clasohm@1461
    84
        ]);
nipkow@243
    85
nipkow@243
    86
(* ------------------------------------------------------------------------ *)
nipkow@243
    87
(* fst and snd are monotone                                                 *)
nipkow@243
    88
(* ------------------------------------------------------------------------ *)
nipkow@243
    89
slotosch@2640
    90
qed_goalw "monofun_fst" thy [monofun] "monofun fst"
nipkow@243
    91
 (fn prems =>
clasohm@1461
    92
        [
clasohm@1461
    93
        (strip_tac 1),
clasohm@1461
    94
        (res_inst_tac [("p","x")] PairE 1),
clasohm@1461
    95
        (hyp_subst_tac 1),
clasohm@1461
    96
        (res_inst_tac [("p","y")] PairE 1),
clasohm@1461
    97
        (hyp_subst_tac 1),
clasohm@1461
    98
        (Asm_simp_tac  1),
clasohm@1461
    99
        (etac (less_cprod4c RS conjunct1) 1)
clasohm@1461
   100
        ]);
nipkow@243
   101
slotosch@2640
   102
qed_goalw "monofun_snd" thy [monofun] "monofun snd"
nipkow@243
   103
 (fn prems =>
clasohm@1461
   104
        [
clasohm@1461
   105
        (strip_tac 1),
clasohm@1461
   106
        (res_inst_tac [("p","x")] PairE 1),
clasohm@1461
   107
        (hyp_subst_tac 1),
clasohm@1461
   108
        (res_inst_tac [("p","y")] PairE 1),
clasohm@1461
   109
        (hyp_subst_tac 1),
clasohm@1461
   110
        (Asm_simp_tac  1),
clasohm@1461
   111
        (etac (less_cprod4c RS conjunct2) 1)
clasohm@1461
   112
        ]);
nipkow@243
   113
nipkow@243
   114
(* ------------------------------------------------------------------------ *)
nipkow@243
   115
(* the type 'a * 'b is a cpo                                                *)
nipkow@243
   116
(* ------------------------------------------------------------------------ *)
nipkow@243
   117
slotosch@2640
   118
qed_goal "lub_cprod" thy 
oheimb@4721
   119
"chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
nipkow@243
   120
 (fn prems =>
clasohm@1461
   121
        [
clasohm@1461
   122
        (cut_facts_tac prems 1),
slotosch@2640
   123
        (rtac (conjI RS is_lubI) 1),
slotosch@2640
   124
        (rtac (allI RS ub_rangeI) 1),
slotosch@2640
   125
        (res_inst_tac [("t","S i")] (surjective_pairing RS ssubst) 1),
clasohm@1461
   126
        (rtac monofun_pair 1),
clasohm@1461
   127
        (rtac is_ub_thelub 1),
clasohm@1461
   128
        (etac (monofun_fst RS ch2ch_monofun) 1),
clasohm@1461
   129
        (rtac is_ub_thelub 1),
clasohm@1461
   130
        (etac (monofun_snd RS ch2ch_monofun) 1),
clasohm@1461
   131
        (strip_tac 1),
clasohm@1461
   132
        (res_inst_tac [("t","u")] (surjective_pairing RS ssubst) 1),
clasohm@1461
   133
        (rtac monofun_pair 1),
clasohm@1461
   134
        (rtac is_lub_thelub 1),
clasohm@1461
   135
        (etac (monofun_fst RS ch2ch_monofun) 1),
clasohm@1461
   136
        (etac (monofun_fst RS ub2ub_monofun) 1),
clasohm@1461
   137
        (rtac is_lub_thelub 1),
clasohm@1461
   138
        (etac (monofun_snd RS ch2ch_monofun) 1),
clasohm@1461
   139
        (etac (monofun_snd RS ub2ub_monofun) 1)
clasohm@1461
   140
        ]);
nipkow@243
   141
oheimb@1779
   142
bind_thm ("thelub_cprod", lub_cprod RS thelubI);
regensbu@1168
   143
(*
oheimb@4721
   144
"chain ?S1 ==>
regensbu@1168
   145
 lub (range ?S1) =
regensbu@1168
   146
 (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
nipkow@243
   147
regensbu@1168
   148
*)
nipkow@243
   149
oheimb@4721
   150
qed_goal "cpo_cprod" thy "chain(S::nat=>'a::cpo*'b::cpo)==>? x. range S<<| x"
nipkow@243
   151
(fn prems =>
clasohm@1461
   152
        [
clasohm@1461
   153
        (cut_facts_tac prems 1),
clasohm@1461
   154
        (rtac exI 1),
clasohm@1461
   155
        (etac lub_cprod 1)
clasohm@1461
   156
        ]);
nipkow@243
   157
regensbu@1168
   158