src/HOLCF/Sprod3.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5033 06f03dc5a1dc
child 9245 428385c4bc50
permissions -rw-r--r--
made tutorial first;
slotosch@2640
     1
(*  Title:      HOLCF/Sprod3.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
slotosch@2640
     6
Lemmas for Sprod.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Sprod3;
nipkow@243
    10
slotosch@2640
    11
(* for compatibility with old HOLCF-Version *)
slotosch@2640
    12
qed_goal "inst_sprod_pcpo" thy "UU = Ispair UU UU"
slotosch@2640
    13
 (fn prems => 
slotosch@2640
    14
        [
slotosch@2640
    15
        (simp_tac (HOL_ss addsimps [UU_def,UU_sprod_def]) 1)
slotosch@2640
    16
        ]);
nipkow@243
    17
(* ------------------------------------------------------------------------ *)
nipkow@243
    18
(* continuity of Ispair, Isfst, Issnd                                       *)
nipkow@243
    19
(* ------------------------------------------------------------------------ *)
nipkow@243
    20
slotosch@2640
    21
qed_goal "sprod3_lemma1" thy 
oheimb@4721
    22
"[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==>\
regensbu@1168
    23
\ Ispair (lub(range Y)) x =\
regensbu@1168
    24
\ Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) \
regensbu@1168
    25
\        (lub(range(%i. Issnd(Ispair(Y i) x))))"
nipkow@243
    26
 (fn prems =>
clasohm@1461
    27
        [
clasohm@1461
    28
        (cut_facts_tac prems 1),
clasohm@1461
    29
        (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
clasohm@1461
    30
        (rtac lub_equal 1),
clasohm@1461
    31
        (atac 1),
clasohm@1461
    32
        (rtac (monofun_Isfst RS ch2ch_monofun) 1),
clasohm@1461
    33
        (rtac ch2ch_fun 1),
clasohm@1461
    34
        (rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
clasohm@1461
    35
        (atac 1),
clasohm@1461
    36
        (rtac allI 1),
regensbu@1277
    37
        (asm_simp_tac Sprod0_ss 1),
clasohm@1461
    38
        (rtac sym 1),
clasohm@1461
    39
        (rtac lub_chain_maxelem 1),
clasohm@1461
    40
        (res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
oheimb@1675
    41
        (rtac (not_all RS iffD1) 1),
clasohm@1461
    42
        (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
clasohm@1461
    43
        (atac 1),
clasohm@1461
    44
        (rtac chain_UU_I_inverse 1),
clasohm@1461
    45
        (atac 1),
clasohm@1461
    46
        (rtac exI 1),
clasohm@1461
    47
        (etac Issnd2 1),
clasohm@1461
    48
        (rtac allI 1),
clasohm@1461
    49
        (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
regensbu@1277
    50
        (asm_simp_tac Sprod0_ss 1),
regensbu@1277
    51
        (rtac refl_less 1),
clasohm@1461
    52
        (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
clasohm@1461
    53
        (etac sym 1),
regensbu@1277
    54
        (asm_simp_tac Sprod0_ss  1),
regensbu@1277
    55
        (rtac minimal 1)
clasohm@1461
    56
        ]);
nipkow@243
    57
slotosch@2640
    58
qed_goal "sprod3_lemma2" thy 
oheimb@4721
    59
"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
regensbu@1168
    60
\   Ispair (lub(range Y)) x =\
regensbu@1168
    61
\   Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))\
regensbu@1168
    62
\          (lub(range(%i. Issnd(Ispair(Y i) x))))"
nipkow@243
    63
 (fn prems =>
clasohm@1461
    64
        [
clasohm@1461
    65
        (cut_facts_tac prems 1),
clasohm@1461
    66
        (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
clasohm@1461
    67
        (atac 1),
clasohm@1461
    68
        (rtac trans 1),
clasohm@1461
    69
        (rtac strict_Ispair1 1),
clasohm@1461
    70
        (rtac (strict_Ispair RS sym) 1),
clasohm@1461
    71
        (rtac disjI1 1),
clasohm@1461
    72
        (rtac chain_UU_I_inverse 1),
clasohm@1461
    73
        (rtac allI 1),
regensbu@1277
    74
        (asm_simp_tac Sprod0_ss  1),
clasohm@1461
    75
        (etac (chain_UU_I RS spec) 1),
clasohm@1461
    76
        (atac 1)
clasohm@1461
    77
        ]);
nipkow@243
    78
nipkow@243
    79
slotosch@2640
    80
qed_goal "sprod3_lemma3" thy 
oheimb@4721
    81
"[| chain(Y); x = UU |] ==>\
regensbu@1168
    82
\          Ispair (lub(range Y)) x =\
regensbu@1168
    83
\          Ispair (lub(range(%i. Isfst(Ispair (Y i) x))))\
regensbu@1168
    84
\                 (lub(range(%i. Issnd(Ispair (Y i) x))))"
nipkow@243
    85
 (fn prems =>
clasohm@1461
    86
        [
clasohm@1461
    87
        (cut_facts_tac prems 1),
clasohm@1461
    88
        (res_inst_tac [("s","UU"),("t","x")] ssubst 1),
clasohm@1461
    89
        (atac 1),
clasohm@1461
    90
        (rtac trans 1),
clasohm@1461
    91
        (rtac strict_Ispair2 1),
clasohm@1461
    92
        (rtac (strict_Ispair RS sym) 1),
clasohm@1461
    93
        (rtac disjI1 1),
clasohm@1461
    94
        (rtac chain_UU_I_inverse 1),
clasohm@1461
    95
        (rtac allI 1),
regensbu@1277
    96
        (simp_tac Sprod0_ss  1)
clasohm@1461
    97
        ]);
nipkow@243
    98
nipkow@243
    99
slotosch@2640
   100
qed_goal "contlub_Ispair1" thy "contlub(Ispair)"
nipkow@243
   101
(fn prems =>
clasohm@1461
   102
        [
clasohm@1461
   103
        (rtac contlubI 1),
clasohm@1461
   104
        (strip_tac 1),
clasohm@1461
   105
        (rtac (expand_fun_eq RS iffD2) 1),
clasohm@1461
   106
        (strip_tac 1),
paulson@2033
   107
        (stac (lub_fun RS thelubI) 1),
clasohm@1461
   108
        (etac (monofun_Ispair1 RS ch2ch_monofun) 1),
clasohm@1461
   109
        (rtac trans 1),
clasohm@1461
   110
        (rtac (thelub_sprod RS sym) 2),
clasohm@1461
   111
        (rtac ch2ch_fun 2),
clasohm@1461
   112
        (etac (monofun_Ispair1 RS ch2ch_monofun) 2),
clasohm@1461
   113
        (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
clasohm@1461
   114
        (res_inst_tac 
clasohm@1461
   115
                [("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1),
clasohm@1461
   116
        (etac sprod3_lemma1 1),
clasohm@1461
   117
        (atac 1),
clasohm@1461
   118
        (atac 1),
clasohm@1461
   119
        (etac sprod3_lemma2 1),
clasohm@1461
   120
        (atac 1),
clasohm@1461
   121
        (atac 1),
clasohm@1461
   122
        (etac sprod3_lemma3 1),
clasohm@1461
   123
        (atac 1)
clasohm@1461
   124
        ]);
nipkow@243
   125
slotosch@2640
   126
qed_goal "sprod3_lemma4" thy 
oheimb@4721
   127
"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==>\
regensbu@1168
   128
\         Ispair x (lub(range Y)) =\
regensbu@1168
   129
\         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
regensbu@1168
   130
\                (lub(range(%i. Issnd (Ispair x (Y i)))))"
regensbu@1043
   131
 (fn prems =>
clasohm@1461
   132
        [
clasohm@1461
   133
        (cut_facts_tac prems 1),
clasohm@1461
   134
        (res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
clasohm@1461
   135
        (rtac sym 1),
clasohm@1461
   136
        (rtac lub_chain_maxelem 1),
wenzelm@3842
   137
        (res_inst_tac [("P","%j. Y(j)~=UU")] exE 1),
oheimb@1675
   138
        (rtac (not_all RS iffD1) 1),
clasohm@1461
   139
        (res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
clasohm@1461
   140
        (atac 1),
clasohm@1461
   141
        (rtac chain_UU_I_inverse 1),
clasohm@1461
   142
        (atac 1),
clasohm@1461
   143
        (rtac exI 1),
clasohm@1461
   144
        (etac Isfst2 1),
clasohm@1461
   145
        (rtac allI 1),
clasohm@1461
   146
        (res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
regensbu@1277
   147
        (asm_simp_tac Sprod0_ss 1),
regensbu@1277
   148
        (rtac refl_less 1),
clasohm@1461
   149
        (res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
clasohm@1461
   150
        (etac sym 1),
regensbu@1277
   151
        (asm_simp_tac Sprod0_ss  1),
regensbu@1277
   152
        (rtac minimal 1),
clasohm@1461
   153
        (rtac lub_equal 1),
clasohm@1461
   154
        (atac 1),
clasohm@1461
   155
        (rtac (monofun_Issnd RS ch2ch_monofun) 1),
clasohm@1461
   156
        (rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
clasohm@1461
   157
        (atac 1),
clasohm@1461
   158
        (rtac allI 1),
regensbu@1277
   159
        (asm_simp_tac Sprod0_ss 1)
clasohm@1461
   160
        ]);
nipkow@243
   161
slotosch@2640
   162
qed_goal "sprod3_lemma5" thy 
oheimb@4721
   163
"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==>\
regensbu@1168
   164
\         Ispair x (lub(range Y)) =\
regensbu@1168
   165
\         Ispair (lub(range(%i. Isfst(Ispair x (Y i)))))\
regensbu@1168
   166
\                (lub(range(%i. Issnd(Ispair x (Y i)))))"
nipkow@243
   167
 (fn prems =>
clasohm@1461
   168
        [
clasohm@1461
   169
        (cut_facts_tac prems 1),
clasohm@1461
   170
        (res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
clasohm@1461
   171
        (atac 1),
clasohm@1461
   172
        (rtac trans 1),
clasohm@1461
   173
        (rtac strict_Ispair2 1),
clasohm@1461
   174
        (rtac (strict_Ispair RS sym) 1),
clasohm@1461
   175
        (rtac disjI2 1),
clasohm@1461
   176
        (rtac chain_UU_I_inverse 1),
clasohm@1461
   177
        (rtac allI 1),
regensbu@1277
   178
        (asm_simp_tac Sprod0_ss  1),
clasohm@1461
   179
        (etac (chain_UU_I RS spec) 1),
clasohm@1461
   180
        (atac 1)
clasohm@1461
   181
        ]);
nipkow@243
   182
slotosch@2640
   183
qed_goal "sprod3_lemma6" thy 
oheimb@4721
   184
"[| chain(Y); x = UU |] ==>\
regensbu@1168
   185
\         Ispair x (lub(range Y)) =\
regensbu@1168
   186
\         Ispair (lub(range(%i. Isfst (Ispair x (Y i)))))\
regensbu@1168
   187
\                (lub(range(%i. Issnd (Ispair x (Y i)))))"
nipkow@243
   188
(fn prems =>
clasohm@1461
   189
        [
clasohm@1461
   190
        (cut_facts_tac prems 1),
clasohm@1461
   191
        (res_inst_tac [("s","UU"),("t","x")] ssubst 1),
clasohm@1461
   192
        (atac 1),
clasohm@1461
   193
        (rtac trans 1),
clasohm@1461
   194
        (rtac strict_Ispair1 1),
clasohm@1461
   195
        (rtac (strict_Ispair RS sym) 1),
clasohm@1461
   196
        (rtac disjI1 1),
clasohm@1461
   197
        (rtac chain_UU_I_inverse 1),
clasohm@1461
   198
        (rtac allI 1),
regensbu@1277
   199
        (simp_tac Sprod0_ss  1)
clasohm@1461
   200
        ]);
nipkow@243
   201
slotosch@2640
   202
qed_goal "contlub_Ispair2" thy "contlub(Ispair(x))"
nipkow@243
   203
(fn prems =>
clasohm@1461
   204
        [
clasohm@1461
   205
        (rtac contlubI 1),
clasohm@1461
   206
        (strip_tac 1),
clasohm@1461
   207
        (rtac trans 1),
clasohm@1461
   208
        (rtac (thelub_sprod RS sym) 2),
clasohm@1461
   209
        (etac (monofun_Ispair2 RS ch2ch_monofun) 2),
clasohm@1461
   210
        (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
clasohm@1461
   211
        (res_inst_tac [("Q","lub(range(Y))=UU")] 
clasohm@1461
   212
                (excluded_middle RS disjE) 1),
clasohm@1461
   213
        (etac sprod3_lemma4 1),
clasohm@1461
   214
        (atac 1),
clasohm@1461
   215
        (atac 1),
clasohm@1461
   216
        (etac sprod3_lemma5 1),
clasohm@1461
   217
        (atac 1),
clasohm@1461
   218
        (atac 1),
clasohm@1461
   219
        (etac sprod3_lemma6 1),
clasohm@1461
   220
        (atac 1)
clasohm@1461
   221
        ]);
nipkow@243
   222
nipkow@243
   223
slotosch@2640
   224
qed_goal "cont_Ispair1" thy "cont(Ispair)"
nipkow@243
   225
(fn prems =>
clasohm@1461
   226
        [
clasohm@1461
   227
        (rtac monocontlub2cont 1),
clasohm@1461
   228
        (rtac monofun_Ispair1 1),
clasohm@1461
   229
        (rtac contlub_Ispair1 1)
clasohm@1461
   230
        ]);
nipkow@243
   231
nipkow@243
   232
slotosch@2640
   233
qed_goal "cont_Ispair2" thy "cont(Ispair(x))"
nipkow@243
   234
(fn prems =>
clasohm@1461
   235
        [
clasohm@1461
   236
        (rtac monocontlub2cont 1),
clasohm@1461
   237
        (rtac monofun_Ispair2 1),
clasohm@1461
   238
        (rtac contlub_Ispair2 1)
clasohm@1461
   239
        ]);
nipkow@243
   240
slotosch@2640
   241
qed_goal "contlub_Isfst" thy "contlub(Isfst)"
nipkow@243
   242
 (fn prems =>
clasohm@1461
   243
        [
clasohm@1461
   244
        (rtac contlubI 1),
clasohm@1461
   245
        (strip_tac 1),
paulson@2033
   246
        (stac (lub_sprod RS thelubI) 1),
clasohm@1461
   247
        (atac 1),
clasohm@1461
   248
        (res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]  
clasohm@1461
   249
                (excluded_middle RS disjE) 1),
regensbu@1277
   250
        (asm_simp_tac Sprod0_ss  1),
clasohm@1461
   251
        (res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")]
clasohm@1461
   252
                ssubst 1),
clasohm@1461
   253
        (atac 1),
clasohm@1461
   254
        (rtac trans 1),
regensbu@1277
   255
        (asm_simp_tac Sprod0_ss  1),
clasohm@1461
   256
        (rtac sym 1),
clasohm@1461
   257
        (rtac chain_UU_I_inverse 1),
clasohm@1461
   258
        (rtac allI 1),
clasohm@1461
   259
        (rtac strict_Isfst 1),
clasohm@1461
   260
        (rtac swap 1),
clasohm@1461
   261
        (etac (defined_IsfstIssnd RS conjunct2) 2),
paulson@2033
   262
        (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS 
paulson@2033
   263
                                  chain_UU_I RS spec]) 1)
paulson@2033
   264
        ]);
nipkow@243
   265
slotosch@2640
   266
qed_goal "contlub_Issnd" thy "contlub(Issnd)"
nipkow@243
   267
(fn prems =>
clasohm@1461
   268
        [
clasohm@1461
   269
        (rtac contlubI 1),
clasohm@1461
   270
        (strip_tac 1),
paulson@2033
   271
        (stac (lub_sprod RS thelubI) 1),
clasohm@1461
   272
        (atac 1),
clasohm@1461
   273
        (res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
clasohm@1461
   274
         (excluded_middle RS disjE) 1),
regensbu@1277
   275
        (asm_simp_tac Sprod0_ss  1),
clasohm@1461
   276
        (res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] 
clasohm@1461
   277
                ssubst 1),
clasohm@1461
   278
        (atac 1),
regensbu@1277
   279
        (asm_simp_tac Sprod0_ss  1),
clasohm@1461
   280
        (rtac sym 1),
clasohm@1461
   281
        (rtac chain_UU_I_inverse 1),
clasohm@1461
   282
        (rtac allI 1),
clasohm@1461
   283
        (rtac strict_Issnd 1),
clasohm@1461
   284
        (rtac swap 1),
clasohm@1461
   285
        (etac (defined_IsfstIssnd RS conjunct1) 2),
oheimb@1675
   286
        (fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS
paulson@2033
   287
                                  chain_UU_I RS spec]) 1)
paulson@2033
   288
        ]);
nipkow@243
   289
slotosch@2640
   290
qed_goal "cont_Isfst" thy "cont(Isfst)"
nipkow@243
   291
(fn prems =>
clasohm@1461
   292
        [
clasohm@1461
   293
        (rtac monocontlub2cont 1),
clasohm@1461
   294
        (rtac monofun_Isfst 1),
clasohm@1461
   295
        (rtac contlub_Isfst 1)
clasohm@1461
   296
        ]);
nipkow@243
   297
slotosch@2640
   298
qed_goal "cont_Issnd" thy "cont(Issnd)"
nipkow@243
   299
(fn prems =>
clasohm@1461
   300
        [
clasohm@1461
   301
        (rtac monocontlub2cont 1),
clasohm@1461
   302
        (rtac monofun_Issnd 1),
clasohm@1461
   303
        (rtac contlub_Issnd 1)
clasohm@1461
   304
        ]);
nipkow@243
   305
wenzelm@5033
   306
qed_goal "spair_eq" thy "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)"
nipkow@243
   307
 (fn prems =>
clasohm@1461
   308
        [
clasohm@1461
   309
        (cut_facts_tac prems 1),
clasohm@1461
   310
        (fast_tac HOL_cs 1)
clasohm@1461
   311
        ]);
nipkow@243
   312
nipkow@243
   313
(* ------------------------------------------------------------------------ *)
nipkow@243
   314
(* convert all lemmas to the continuous versions                            *)
nipkow@243
   315
(* ------------------------------------------------------------------------ *)
nipkow@243
   316
slotosch@2640
   317
qed_goalw "beta_cfun_sprod" thy [spair_def]
wenzelm@3842
   318
        "(LAM x y. Ispair x y)`a`b = Ispair a b"
nipkow@243
   319
 (fn prems =>
clasohm@1461
   320
        [
paulson@2033
   321
        (stac beta_cfun 1),
wenzelm@4098
   322
        (simp_tac (simpset() addsimps [cont_Ispair2, cont_Ispair1,
oheimb@2566
   323
					cont2cont_CF1L]) 1),
paulson@2033
   324
        (stac beta_cfun 1),
clasohm@1461
   325
        (rtac cont_Ispair2 1),
clasohm@1461
   326
        (rtac refl 1)
clasohm@1461
   327
        ]);
nipkow@243
   328
slotosch@2640
   329
qed_goalw "inject_spair" thy [spair_def]
wenzelm@5033
   330
        "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba"
nipkow@243
   331
 (fn prems =>
clasohm@1461
   332
        [
clasohm@1461
   333
        (cut_facts_tac prems 1),
clasohm@1461
   334
        (etac inject_Ispair 1),
clasohm@1461
   335
        (atac 1),
clasohm@1461
   336
        (etac box_equals 1),
clasohm@1461
   337
        (rtac beta_cfun_sprod 1),
clasohm@1461
   338
        (rtac beta_cfun_sprod 1)
clasohm@1461
   339
        ]);
nipkow@243
   340
wenzelm@5033
   341
qed_goalw "inst_sprod_pcpo2" thy [spair_def] "UU = (:UU,UU:)"
nipkow@243
   342
 (fn prems =>
clasohm@1461
   343
        [
clasohm@1461
   344
        (rtac sym 1),
clasohm@1461
   345
        (rtac trans 1),
clasohm@1461
   346
        (rtac beta_cfun_sprod 1),
clasohm@1461
   347
        (rtac sym 1),
clasohm@1461
   348
        (rtac inst_sprod_pcpo 1)
clasohm@1461
   349
        ]);
nipkow@243
   350
slotosch@2640
   351
qed_goalw "strict_spair" thy [spair_def] 
wenzelm@5033
   352
        "(a=UU | b=UU) ==> (:a,b:)=UU"
nipkow@243
   353
 (fn prems =>
clasohm@1461
   354
        [
clasohm@1461
   355
        (cut_facts_tac prems 1),
clasohm@1461
   356
        (rtac trans 1),
clasohm@1461
   357
        (rtac beta_cfun_sprod 1),
clasohm@1461
   358
        (rtac trans 1),
clasohm@1461
   359
        (rtac (inst_sprod_pcpo RS sym) 2),
clasohm@1461
   360
        (etac strict_Ispair 1)
clasohm@1461
   361
        ]);
nipkow@243
   362
wenzelm@5033
   363
qed_goalw "strict_spair1" thy [spair_def] "(:UU,b:) = UU"
nipkow@243
   364
 (fn prems =>
clasohm@1461
   365
        [
paulson@2033
   366
        (stac beta_cfun_sprod 1),
clasohm@1461
   367
        (rtac trans 1),
clasohm@1461
   368
        (rtac (inst_sprod_pcpo RS sym) 2),
clasohm@1461
   369
        (rtac strict_Ispair1 1)
clasohm@1461
   370
        ]);
nipkow@243
   371
wenzelm@5033
   372
qed_goalw "strict_spair2" thy [spair_def] "(:a,UU:) = UU"
nipkow@243
   373
 (fn prems =>
clasohm@1461
   374
        [
paulson@2033
   375
        (stac beta_cfun_sprod 1),
clasohm@1461
   376
        (rtac trans 1),
clasohm@1461
   377
        (rtac (inst_sprod_pcpo RS sym) 2),
clasohm@1461
   378
        (rtac strict_Ispair2 1)
clasohm@1461
   379
        ]);
nipkow@243
   380
slotosch@2640
   381
qed_goalw "strict_spair_rev" thy [spair_def]
wenzelm@5033
   382
        "(:x,y:)~=UU ==> ~x=UU & ~y=UU"
nipkow@243
   383
 (fn prems =>
clasohm@1461
   384
        [
clasohm@1461
   385
        (cut_facts_tac prems 1),
clasohm@1461
   386
        (rtac strict_Ispair_rev 1),
clasohm@1461
   387
        (rtac (beta_cfun_sprod RS subst) 1),
clasohm@1461
   388
        (rtac (inst_sprod_pcpo RS subst) 1),
clasohm@1461
   389
        (atac 1)
clasohm@1461
   390
        ]);
nipkow@243
   391
slotosch@2640
   392
qed_goalw "defined_spair_rev" thy [spair_def]
wenzelm@5033
   393
 "(:a,b:) = UU ==> (a = UU | b = UU)"
nipkow@243
   394
 (fn prems =>
clasohm@1461
   395
        [
clasohm@1461
   396
        (cut_facts_tac prems 1),
clasohm@1461
   397
        (rtac defined_Ispair_rev 1),
clasohm@1461
   398
        (rtac (beta_cfun_sprod RS subst) 1),
clasohm@1461
   399
        (rtac (inst_sprod_pcpo RS subst) 1),
clasohm@1461
   400
        (atac 1)
clasohm@1461
   401
        ]);
nipkow@243
   402
slotosch@2640
   403
qed_goalw "defined_spair" thy [spair_def]
wenzelm@5033
   404
        "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
nipkow@243
   405
 (fn prems =>
clasohm@1461
   406
        [
clasohm@1461
   407
        (cut_facts_tac prems 1),
paulson@2033
   408
        (stac beta_cfun_sprod 1),
paulson@2033
   409
        (stac inst_sprod_pcpo 1),
clasohm@1461
   410
        (etac defined_Ispair 1),
clasohm@1461
   411
        (atac 1)
clasohm@1461
   412
        ]);
nipkow@243
   413
slotosch@2640
   414
qed_goalw "Exh_Sprod2" thy [spair_def]
wenzelm@5033
   415
        "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)"
nipkow@243
   416
 (fn prems =>
clasohm@1461
   417
        [
clasohm@1461
   418
        (rtac (Exh_Sprod RS disjE) 1),
clasohm@1461
   419
        (rtac disjI1 1),
paulson@2033
   420
        (stac inst_sprod_pcpo 1),
clasohm@1461
   421
        (atac 1),
clasohm@1461
   422
        (rtac disjI2 1),
clasohm@1461
   423
        (etac exE 1),
clasohm@1461
   424
        (etac exE 1),
clasohm@1461
   425
        (rtac exI 1),
clasohm@1461
   426
        (rtac exI 1),
clasohm@1461
   427
        (rtac conjI 1),
paulson@2033
   428
        (stac beta_cfun_sprod 1),
clasohm@1461
   429
        (fast_tac HOL_cs 1),
clasohm@1461
   430
        (fast_tac HOL_cs 1)
clasohm@1461
   431
        ]);
nipkow@243
   432
nipkow@243
   433
slotosch@2640
   434
qed_goalw "sprodE" thy [spair_def]
wenzelm@5033
   435
"[|p=UU ==> Q;!!x y. [|p=(:x,y:);x~=UU ; y~=UU|] ==> Q|] ==> Q"
nipkow@243
   436
(fn prems =>
clasohm@1461
   437
        [
clasohm@1461
   438
        (rtac IsprodE 1),
clasohm@1461
   439
        (resolve_tac prems 1),
paulson@2033
   440
        (stac inst_sprod_pcpo 1),
clasohm@1461
   441
        (atac 1),
clasohm@1461
   442
        (resolve_tac prems 1),
clasohm@1461
   443
        (atac 2),
clasohm@1461
   444
        (atac 2),
paulson@2033
   445
        (stac beta_cfun_sprod 1),
clasohm@1461
   446
        (atac 1)
clasohm@1461
   447
        ]);
nipkow@243
   448
nipkow@243
   449
slotosch@2640
   450
qed_goalw "strict_sfst" thy [sfst_def] 
clasohm@1461
   451
        "p=UU==>sfst`p=UU"
nipkow@243
   452
 (fn prems =>
clasohm@1461
   453
        [
clasohm@1461
   454
        (cut_facts_tac prems 1),
paulson@2033
   455
        (stac beta_cfun 1),
clasohm@1461
   456
        (rtac cont_Isfst 1),
clasohm@1461
   457
        (rtac strict_Isfst 1),
clasohm@1461
   458
        (rtac (inst_sprod_pcpo RS subst) 1),
clasohm@1461
   459
        (atac 1)
clasohm@1461
   460
        ]);
nipkow@243
   461
slotosch@2640
   462
qed_goalw "strict_sfst1" thy [sfst_def,spair_def] 
wenzelm@5033
   463
        "sfst`(:UU,y:) = UU"
nipkow@243
   464
 (fn prems =>
clasohm@1461
   465
        [
paulson@2033
   466
        (stac beta_cfun_sprod 1),
paulson@2033
   467
        (stac beta_cfun 1),
clasohm@1461
   468
        (rtac cont_Isfst 1),
clasohm@1461
   469
        (rtac strict_Isfst1 1)
clasohm@1461
   470
        ]);
nipkow@243
   471
 
slotosch@2640
   472
qed_goalw "strict_sfst2" thy [sfst_def,spair_def] 
wenzelm@5033
   473
        "sfst`(:x,UU:) = UU"
nipkow@243
   474
 (fn prems =>
clasohm@1461
   475
        [
paulson@2033
   476
        (stac beta_cfun_sprod 1),
paulson@2033
   477
        (stac beta_cfun 1),
clasohm@1461
   478
        (rtac cont_Isfst 1),
clasohm@1461
   479
        (rtac strict_Isfst2 1)
clasohm@1461
   480
        ]);
nipkow@243
   481
slotosch@2640
   482
qed_goalw "strict_ssnd" thy [ssnd_def] 
clasohm@1461
   483
        "p=UU==>ssnd`p=UU"
nipkow@243
   484
 (fn prems =>
clasohm@1461
   485
        [
clasohm@1461
   486
        (cut_facts_tac prems 1),
paulson@2033
   487
        (stac beta_cfun 1),
clasohm@1461
   488
        (rtac cont_Issnd 1),
clasohm@1461
   489
        (rtac strict_Issnd 1),
clasohm@1461
   490
        (rtac (inst_sprod_pcpo RS subst) 1),
clasohm@1461
   491
        (atac 1)
clasohm@1461
   492
        ]);
nipkow@243
   493
slotosch@2640
   494
qed_goalw "strict_ssnd1" thy [ssnd_def,spair_def] 
wenzelm@5033
   495
        "ssnd`(:UU,y:) = UU"
nipkow@243
   496
 (fn prems =>
clasohm@1461
   497
        [
paulson@2033
   498
        (stac beta_cfun_sprod 1),
paulson@2033
   499
        (stac beta_cfun 1),
clasohm@1461
   500
        (rtac cont_Issnd 1),
clasohm@1461
   501
        (rtac strict_Issnd1 1)
clasohm@1461
   502
        ]);
nipkow@243
   503
slotosch@2640
   504
qed_goalw "strict_ssnd2" thy [ssnd_def,spair_def] 
wenzelm@5033
   505
        "ssnd`(:x,UU:) = UU"
nipkow@243
   506
 (fn prems =>
clasohm@1461
   507
        [
paulson@2033
   508
        (stac beta_cfun_sprod 1),
paulson@2033
   509
        (stac beta_cfun 1),
clasohm@1461
   510
        (rtac cont_Issnd 1),
clasohm@1461
   511
        (rtac strict_Issnd2 1)
clasohm@1461
   512
        ]);
nipkow@243
   513
slotosch@2640
   514
qed_goalw "sfst2" thy [sfst_def,spair_def] 
wenzelm@5033
   515
        "y~=UU ==>sfst`(:x,y:)=x"
nipkow@243
   516
 (fn prems =>
clasohm@1461
   517
        [
clasohm@1461
   518
        (cut_facts_tac prems 1),
paulson@2033
   519
        (stac beta_cfun_sprod 1),
paulson@2033
   520
        (stac beta_cfun 1),
clasohm@1461
   521
        (rtac cont_Isfst 1),
clasohm@1461
   522
        (etac Isfst2 1)
clasohm@1461
   523
        ]);
nipkow@243
   524
slotosch@2640
   525
qed_goalw "ssnd2" thy [ssnd_def,spair_def] 
wenzelm@5033
   526
        "x~=UU ==>ssnd`(:x,y:)=y"
nipkow@243
   527
 (fn prems =>
clasohm@1461
   528
        [
clasohm@1461
   529
        (cut_facts_tac prems 1),
paulson@2033
   530
        (stac beta_cfun_sprod 1),
paulson@2033
   531
        (stac beta_cfun 1),
clasohm@1461
   532
        (rtac cont_Issnd 1),
clasohm@1461
   533
        (etac Issnd2 1)
clasohm@1461
   534
        ]);
nipkow@243
   535
nipkow@243
   536
slotosch@2640
   537
qed_goalw "defined_sfstssnd" thy [sfst_def,ssnd_def,spair_def]
clasohm@1461
   538
        "p~=UU ==> sfst`p ~=UU & ssnd`p ~=UU"
nipkow@243
   539
 (fn prems =>
clasohm@1461
   540
        [
clasohm@1461
   541
        (cut_facts_tac prems 1),
paulson@2033
   542
        (stac beta_cfun 1),
clasohm@1461
   543
        (rtac cont_Issnd 1),
paulson@2033
   544
        (stac beta_cfun 1),
clasohm@1461
   545
        (rtac cont_Isfst 1),
clasohm@1461
   546
        (rtac defined_IsfstIssnd 1),
clasohm@1461
   547
        (rtac (inst_sprod_pcpo RS subst) 1),
clasohm@1461
   548
        (atac 1)
clasohm@1461
   549
        ]);
nipkow@243
   550
 
nipkow@243
   551
slotosch@2640
   552
qed_goalw "surjective_pairing_Sprod2" thy 
wenzelm@5033
   553
        [sfst_def,ssnd_def,spair_def] "(:sfst`p , ssnd`p:) = p"
nipkow@243
   554
 (fn prems =>
clasohm@1461
   555
        [
paulson@2033
   556
        (stac beta_cfun_sprod 1),
paulson@2033
   557
        (stac beta_cfun 1),
clasohm@1461
   558
        (rtac cont_Issnd 1),
paulson@2033
   559
        (stac beta_cfun 1),
clasohm@1461
   560
        (rtac cont_Isfst 1),
clasohm@1461
   561
        (rtac (surjective_pairing_Sprod RS sym) 1)
clasohm@1461
   562
        ]);
nipkow@243
   563
nipkow@243
   564
slotosch@2640
   565
qed_goalw "lub_sprod2" thy [sfst_def,ssnd_def,spair_def]
oheimb@4721
   566
"[|chain(S)|] ==> range(S) <<| \
wenzelm@5033
   567
\ (: lub(range(%i. sfst`(S i))), lub(range(%i. ssnd`(S i))) :)"
nipkow@243
   568
 (fn prems =>
clasohm@1461
   569
        [
clasohm@1461
   570
        (cut_facts_tac prems 1),
paulson@2033
   571
        (stac beta_cfun_sprod 1),
paulson@2033
   572
        (stac (beta_cfun RS ext) 1),
clasohm@1461
   573
        (rtac cont_Issnd 1),
paulson@2033
   574
        (stac (beta_cfun RS ext) 1),
clasohm@1461
   575
        (rtac cont_Isfst 1),
clasohm@1461
   576
        (rtac lub_sprod 1),
clasohm@1461
   577
        (resolve_tac prems 1)
clasohm@1461
   578
        ]);
nipkow@243
   579
nipkow@243
   580
oheimb@1779
   581
bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI);
regensbu@1168
   582
(*
oheimb@4721
   583
 "chain ?S1 ==>
regensbu@1168
   584
 lub (range ?S1) =
wenzelm@5033
   585
 (:lub (range (%i. sfst`(?S1 i))), lub (range (%i. ssnd`(?S1 i))):)" : thm
regensbu@1168
   586
*)
nipkow@243
   587
slotosch@2640
   588
qed_goalw "ssplit1" thy [ssplit_def]
clasohm@1461
   589
        "ssplit`f`UU=UU"
nipkow@243
   590
 (fn prems =>
clasohm@1461
   591
        [
paulson@2033
   592
        (stac beta_cfun 1),
oheimb@2566
   593
        (Simp_tac 1),
paulson@2033
   594
        (stac strictify1 1),
clasohm@1461
   595
        (rtac refl 1)
clasohm@1461
   596
        ]);
nipkow@243
   597
slotosch@2640
   598
qed_goalw "ssplit2" thy [ssplit_def]
wenzelm@5033
   599
        "[|x~=UU;y~=UU|] ==> ssplit`f`(:x,y:)= f`x`y"
nipkow@243
   600
 (fn prems =>
clasohm@1461
   601
        [
paulson@2033
   602
        (stac beta_cfun 1),
oheimb@2566
   603
        (Simp_tac 1),
paulson@2033
   604
        (stac strictify2 1),
clasohm@1461
   605
        (rtac defined_spair 1),
clasohm@1461
   606
        (resolve_tac prems 1),
clasohm@1461
   607
        (resolve_tac prems 1),
paulson@2033
   608
        (stac beta_cfun 1),
oheimb@2566
   609
        (Simp_tac 1),
paulson@2033
   610
        (stac sfst2 1),
clasohm@1461
   611
        (resolve_tac prems 1),
paulson@2033
   612
        (stac ssnd2 1),
clasohm@1461
   613
        (resolve_tac prems 1),
clasohm@1461
   614
        (rtac refl 1)
clasohm@1461
   615
        ]);
nipkow@243
   616
nipkow@243
   617
slotosch@2640
   618
qed_goalw "ssplit3" thy [ssplit_def]
regensbu@1168
   619
  "ssplit`spair`z=z"
nipkow@243
   620
 (fn prems =>
clasohm@1461
   621
        [
paulson@2033
   622
        (stac beta_cfun 1),
oheimb@2566
   623
        (Simp_tac 1),
oheimb@1675
   624
        (case_tac "z=UU" 1),
clasohm@1461
   625
        (hyp_subst_tac 1),
clasohm@1461
   626
        (rtac strictify1 1),
clasohm@1461
   627
        (rtac trans 1),
clasohm@1461
   628
        (rtac strictify2 1),
clasohm@1461
   629
        (atac 1),
paulson@2033
   630
        (stac beta_cfun 1),
oheimb@2566
   631
        (Simp_tac 1),
clasohm@1461
   632
        (rtac surjective_pairing_Sprod2 1)
clasohm@1461
   633
        ]);
nipkow@243
   634
nipkow@243
   635
(* ------------------------------------------------------------------------ *)
nipkow@243
   636
(* install simplifier for Sprod                                             *)
nipkow@243
   637
(* ------------------------------------------------------------------------ *)
nipkow@243
   638
regensbu@1274
   639
val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
clasohm@1461
   640
                strict_ssnd1,strict_ssnd2,sfst2,ssnd2,defined_spair,
clasohm@1461
   641
                ssplit1,ssplit2];
slotosch@2640
   642
Addsimps Sprod_rews;
regensbu@1274
   643