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