src/HOLCF/Sprod0.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4833 2e53109d4bc8
child 9245 428385c4bc50
permissions -rw-r--r--
made tutorial first;
clasohm@1461
     1
(*  Title:      HOLCF/sprod0.thy
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 theory sprod0.thy
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Sprod0;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* A non-emptyness result for Sprod                                         *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
clasohm@892
    15
qed_goalw "SprodI" Sprod0.thy [Sprod_def]
clasohm@1461
    16
        "(Spair_Rep a b):Sprod"
nipkow@243
    17
(fn prems =>
clasohm@1461
    18
        [
clasohm@1461
    19
        (EVERY1 [rtac CollectI, rtac exI,rtac exI, rtac refl])
clasohm@1461
    20
        ]);
nipkow@243
    21
nipkow@4833
    22
qed_goal "inj_on_Abs_Sprod" Sprod0.thy 
nipkow@4833
    23
        "inj_on Abs_Sprod Sprod"
nipkow@243
    24
(fn prems =>
clasohm@1461
    25
        [
nipkow@4833
    26
        (rtac inj_on_inverseI 1),
clasohm@1461
    27
        (etac Abs_Sprod_inverse 1)
clasohm@1461
    28
        ]);
nipkow@243
    29
nipkow@243
    30
(* ------------------------------------------------------------------------ *)
nipkow@243
    31
(* Strictness and definedness of Spair_Rep                                  *)
nipkow@243
    32
(* ------------------------------------------------------------------------ *)
nipkow@243
    33
clasohm@892
    34
qed_goalw "strict_Spair_Rep" Sprod0.thy [Spair_Rep_def]
regensbu@1168
    35
 "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
nipkow@243
    36
 (fn prems =>
clasohm@1461
    37
        [
clasohm@1461
    38
        (cut_facts_tac prems 1),
clasohm@1461
    39
        (rtac ext 1),
clasohm@1461
    40
        (rtac ext 1),
clasohm@1461
    41
        (rtac iffI 1),
clasohm@1461
    42
        (fast_tac HOL_cs 1),
clasohm@1461
    43
        (fast_tac HOL_cs 1)
clasohm@1461
    44
        ]);
nipkow@243
    45
clasohm@892
    46
qed_goalw "defined_Spair_Rep_rev" Sprod0.thy [Spair_Rep_def]
regensbu@1168
    47
 "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
nipkow@243
    48
 (fn prems =>
clasohm@1461
    49
        [
oheimb@1675
    50
        (case_tac "a=UU|b=UU" 1),
clasohm@1461
    51
        (atac 1),
clasohm@1461
    52
        (rtac disjI1 1),
clasohm@1461
    53
        (rtac ((hd prems) RS fun_cong RS fun_cong RS iffD2 RS mp RS 
clasohm@1461
    54
        conjunct1 RS sym) 1),
clasohm@1461
    55
        (fast_tac HOL_cs 1),
clasohm@1461
    56
        (fast_tac HOL_cs 1)
clasohm@1461
    57
        ]);
nipkow@243
    58
nipkow@243
    59
nipkow@243
    60
(* ------------------------------------------------------------------------ *)
nipkow@243
    61
(* injectivity of Spair_Rep and Ispair                                      *)
nipkow@243
    62
(* ------------------------------------------------------------------------ *)
nipkow@243
    63
clasohm@892
    64
qed_goalw "inject_Spair_Rep" Sprod0.thy [Spair_Rep_def]
regensbu@1168
    65
"[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
nipkow@243
    66
 (fn prems =>
clasohm@1461
    67
        [
clasohm@1461
    68
        (cut_facts_tac prems 1),
clasohm@1461
    69
        (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong 
clasohm@1461
    70
                RS iffD1 RS mp) 1),
clasohm@1461
    71
        (fast_tac HOL_cs 1),
clasohm@1461
    72
        (fast_tac HOL_cs 1)
clasohm@1461
    73
        ]);
nipkow@243
    74
nipkow@243
    75
clasohm@892
    76
qed_goalw "inject_Ispair" Sprod0.thy [Ispair_def]
clasohm@1461
    77
        "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"
nipkow@243
    78
(fn prems =>
clasohm@1461
    79
        [
clasohm@1461
    80
        (cut_facts_tac prems 1),
clasohm@1461
    81
        (etac inject_Spair_Rep 1),
clasohm@1461
    82
        (atac 1),
nipkow@4833
    83
        (etac (inj_on_Abs_Sprod  RS inj_onD) 1),
clasohm@1461
    84
        (rtac SprodI 1),
clasohm@1461
    85
        (rtac SprodI 1)
clasohm@1461
    86
        ]);
nipkow@243
    87
nipkow@243
    88
nipkow@243
    89
(* ------------------------------------------------------------------------ *)
nipkow@243
    90
(* strictness and definedness of Ispair                                     *)
nipkow@243
    91
(* ------------------------------------------------------------------------ *)
nipkow@243
    92
clasohm@892
    93
qed_goalw "strict_Ispair" Sprod0.thy [Ispair_def] 
regensbu@1168
    94
 "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
nipkow@243
    95
(fn prems =>
clasohm@1461
    96
        [
clasohm@1461
    97
        (cut_facts_tac prems 1),
clasohm@1461
    98
        (etac (strict_Spair_Rep RS arg_cong) 1)
clasohm@1461
    99
        ]);
nipkow@243
   100
clasohm@892
   101
qed_goalw "strict_Ispair1" Sprod0.thy [Ispair_def]
clasohm@1461
   102
        "Ispair UU b  = Ispair UU UU"
nipkow@243
   103
(fn prems =>
clasohm@1461
   104
        [
clasohm@1461
   105
        (rtac (strict_Spair_Rep RS arg_cong) 1),
clasohm@1461
   106
        (rtac disjI1 1),
clasohm@1461
   107
        (rtac refl 1)
clasohm@1461
   108
        ]);
nipkow@243
   109
clasohm@892
   110
qed_goalw "strict_Ispair2" Sprod0.thy [Ispair_def]
clasohm@1461
   111
        "Ispair a UU = Ispair UU UU"
nipkow@243
   112
(fn prems =>
clasohm@1461
   113
        [
clasohm@1461
   114
        (rtac (strict_Spair_Rep RS arg_cong) 1),
clasohm@1461
   115
        (rtac disjI2 1),
clasohm@1461
   116
        (rtac refl 1)
clasohm@1461
   117
        ]);
nipkow@243
   118
clasohm@892
   119
qed_goal "strict_Ispair_rev" Sprod0.thy 
clasohm@1461
   120
        "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
nipkow@243
   121
(fn prems =>
clasohm@1461
   122
        [
clasohm@1461
   123
        (cut_facts_tac prems 1),
oheimb@1675
   124
        (rtac (de_Morgan_disj RS subst) 1),
clasohm@1461
   125
        (etac contrapos 1),
clasohm@1461
   126
        (etac strict_Ispair 1)
clasohm@1461
   127
        ]);
nipkow@243
   128
clasohm@892
   129
qed_goalw "defined_Ispair_rev" Sprod0.thy [Ispair_def]
clasohm@1461
   130
        "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)"
nipkow@243
   131
(fn prems =>
clasohm@1461
   132
        [
clasohm@1461
   133
        (cut_facts_tac prems 1),
clasohm@1461
   134
        (rtac defined_Spair_Rep_rev 1),
nipkow@4833
   135
        (rtac (inj_on_Abs_Sprod  RS inj_onD) 1),
clasohm@1461
   136
        (atac 1),
clasohm@1461
   137
        (rtac SprodI 1),
clasohm@1461
   138
        (rtac SprodI 1)
clasohm@1461
   139
        ]);
nipkow@243
   140
clasohm@892
   141
qed_goal "defined_Ispair" Sprod0.thy  
regensbu@1168
   142
"[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)" 
nipkow@243
   143
(fn prems =>
clasohm@1461
   144
        [
clasohm@1461
   145
        (cut_facts_tac prems 1),
clasohm@1461
   146
        (rtac contrapos 1),
clasohm@1461
   147
        (etac defined_Ispair_rev 2),
oheimb@1675
   148
        (rtac (de_Morgan_disj RS iffD2) 1),
clasohm@1461
   149
        (etac conjI 1),
clasohm@1461
   150
        (atac 1)
clasohm@1461
   151
        ]);
nipkow@243
   152
nipkow@243
   153
nipkow@243
   154
(* ------------------------------------------------------------------------ *)
nipkow@243
   155
(* Exhaustion of the strict product **                                      *)
nipkow@243
   156
(* ------------------------------------------------------------------------ *)
nipkow@243
   157
clasohm@892
   158
qed_goalw "Exh_Sprod" Sprod0.thy [Ispair_def]
clasohm@1461
   159
        "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
nipkow@243
   160
(fn prems =>
clasohm@1461
   161
        [
clasohm@1461
   162
        (rtac (rewrite_rule [Sprod_def] Rep_Sprod RS CollectE) 1),
clasohm@1461
   163
        (etac exE 1),
clasohm@1461
   164
        (etac exE 1),
clasohm@1461
   165
        (rtac (excluded_middle RS disjE) 1),
clasohm@1461
   166
        (rtac disjI2 1),
clasohm@1461
   167
        (rtac exI 1),
clasohm@1461
   168
        (rtac exI 1),
clasohm@1461
   169
        (rtac conjI 1),
clasohm@1461
   170
        (rtac (Rep_Sprod_inverse RS sym RS trans) 1),
clasohm@1461
   171
        (etac arg_cong 1),
oheimb@1675
   172
        (rtac (de_Morgan_disj RS subst) 1),
clasohm@1461
   173
        (atac 1),
clasohm@1461
   174
        (rtac disjI1 1),
clasohm@1461
   175
        (rtac (Rep_Sprod_inverse RS sym RS trans) 1),
clasohm@1461
   176
        (res_inst_tac [("f","Abs_Sprod")] arg_cong 1),
clasohm@1461
   177
        (etac trans 1),
clasohm@1461
   178
        (etac strict_Spair_Rep 1)
clasohm@1461
   179
        ]);
nipkow@243
   180
nipkow@243
   181
(* ------------------------------------------------------------------------ *)
nipkow@243
   182
(* general elimination rule for strict product                              *)
nipkow@243
   183
(* ------------------------------------------------------------------------ *)
nipkow@243
   184
clasohm@892
   185
qed_goal "IsprodE" Sprod0.thy
regensbu@1168
   186
"[|p=Ispair UU UU ==> Q ;!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q|] ==> Q"
nipkow@243
   187
(fn prems =>
clasohm@1461
   188
        [
clasohm@1461
   189
        (rtac (Exh_Sprod RS disjE) 1),
clasohm@1461
   190
        (etac (hd prems) 1),
clasohm@1461
   191
        (etac exE 1),
clasohm@1461
   192
        (etac exE 1),
clasohm@1461
   193
        (etac conjE 1),
clasohm@1461
   194
        (etac conjE 1),
clasohm@1461
   195
        (etac (hd (tl prems)) 1),
clasohm@1461
   196
        (atac 1),
clasohm@1461
   197
        (atac 1)
clasohm@1461
   198
        ]);
nipkow@243
   199
nipkow@243
   200
nipkow@243
   201
(* ------------------------------------------------------------------------ *)
nipkow@243
   202
(* some results about the selectors Isfst, Issnd                            *)
nipkow@243
   203
(* ------------------------------------------------------------------------ *)
nipkow@243
   204
clasohm@892
   205
qed_goalw "strict_Isfst" Sprod0.thy [Isfst_def] 
clasohm@1461
   206
        "p=Ispair UU UU ==> Isfst p = UU"
nipkow@243
   207
(fn prems =>
clasohm@1461
   208
        [
clasohm@1461
   209
        (cut_facts_tac prems 1),
oheimb@4535
   210
        (rtac select_equality 1),
clasohm@1461
   211
        (rtac conjI 1),
clasohm@1461
   212
        (fast_tac HOL_cs  1),
clasohm@1461
   213
        (strip_tac 1),
clasohm@1461
   214
        (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1),
clasohm@1461
   215
        (rtac not_sym 1),
clasohm@1461
   216
        (rtac defined_Ispair 1),
clasohm@1461
   217
        (REPEAT (fast_tac HOL_cs  1))
clasohm@1461
   218
        ]);
nipkow@243
   219
nipkow@243
   220
clasohm@892
   221
qed_goal "strict_Isfst1" Sprod0.thy
clasohm@1461
   222
        "Isfst(Ispair UU y) = UU"
nipkow@243
   223
(fn prems =>
clasohm@1461
   224
        [
paulson@2033
   225
        (stac strict_Ispair1 1),
clasohm@1461
   226
        (rtac strict_Isfst 1),
clasohm@1461
   227
        (rtac refl 1)
clasohm@1461
   228
        ]);
nipkow@243
   229
clasohm@892
   230
qed_goal "strict_Isfst2" Sprod0.thy
clasohm@1461
   231
        "Isfst(Ispair x UU) = UU"
nipkow@243
   232
(fn prems =>
clasohm@1461
   233
        [
paulson@2033
   234
        (stac strict_Ispair2 1),
clasohm@1461
   235
        (rtac strict_Isfst 1),
clasohm@1461
   236
        (rtac refl 1)
clasohm@1461
   237
        ]);
nipkow@243
   238
nipkow@243
   239
clasohm@892
   240
qed_goalw "strict_Issnd" Sprod0.thy [Issnd_def] 
clasohm@1461
   241
        "p=Ispair UU UU ==>Issnd p=UU"
nipkow@243
   242
(fn prems =>
clasohm@1461
   243
        [
clasohm@1461
   244
        (cut_facts_tac prems 1),
oheimb@4535
   245
        (rtac select_equality 1),
clasohm@1461
   246
        (rtac conjI 1),
clasohm@1461
   247
        (fast_tac HOL_cs  1),
clasohm@1461
   248
        (strip_tac 1),
clasohm@1461
   249
        (res_inst_tac [("P","Ispair UU UU = Ispair a b")] notE 1),
clasohm@1461
   250
        (rtac not_sym 1),
clasohm@1461
   251
        (rtac defined_Ispair 1),
clasohm@1461
   252
        (REPEAT (fast_tac HOL_cs  1))
clasohm@1461
   253
        ]);
nipkow@243
   254
clasohm@892
   255
qed_goal "strict_Issnd1" Sprod0.thy
clasohm@1461
   256
        "Issnd(Ispair UU y) = UU"
nipkow@243
   257
(fn prems =>
clasohm@1461
   258
        [
paulson@2033
   259
        (stac strict_Ispair1 1),
clasohm@1461
   260
        (rtac strict_Issnd 1),
clasohm@1461
   261
        (rtac refl 1)
clasohm@1461
   262
        ]);
nipkow@243
   263
clasohm@892
   264
qed_goal "strict_Issnd2" Sprod0.thy
clasohm@1461
   265
        "Issnd(Ispair x UU) = UU"
nipkow@243
   266
(fn prems =>
clasohm@1461
   267
        [
paulson@2033
   268
        (stac strict_Ispair2 1),
clasohm@1461
   269
        (rtac strict_Issnd 1),
clasohm@1461
   270
        (rtac refl 1)
clasohm@1461
   271
        ]);
nipkow@243
   272
clasohm@892
   273
qed_goalw "Isfst" Sprod0.thy [Isfst_def]
clasohm@1461
   274
        "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
nipkow@243
   275
(fn prems =>
clasohm@1461
   276
        [
clasohm@1461
   277
        (cut_facts_tac prems 1),
oheimb@4535
   278
        (rtac select_equality 1),
clasohm@1461
   279
        (rtac conjI 1),
clasohm@1461
   280
        (strip_tac 1),
clasohm@1461
   281
        (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
clasohm@1461
   282
        (etac defined_Ispair 1),
clasohm@1461
   283
        (atac 1),
clasohm@1461
   284
        (atac 1),
clasohm@1461
   285
        (strip_tac 1),
clasohm@1461
   286
        (rtac (inject_Ispair RS conjunct1) 1),
clasohm@1461
   287
        (fast_tac HOL_cs  3),
clasohm@1461
   288
        (fast_tac HOL_cs  1),
clasohm@1461
   289
        (fast_tac HOL_cs  1),
clasohm@1461
   290
        (fast_tac HOL_cs  1)
clasohm@1461
   291
        ]);
nipkow@243
   292
clasohm@892
   293
qed_goalw "Issnd" Sprod0.thy [Issnd_def]
clasohm@1461
   294
        "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
nipkow@243
   295
(fn prems =>
clasohm@1461
   296
        [
clasohm@1461
   297
        (cut_facts_tac prems 1),
oheimb@4535
   298
        (rtac select_equality 1),
clasohm@1461
   299
        (rtac conjI 1),
clasohm@1461
   300
        (strip_tac 1),
clasohm@1461
   301
        (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
clasohm@1461
   302
        (etac defined_Ispair 1),
clasohm@1461
   303
        (atac 1),
clasohm@1461
   304
        (atac 1),
clasohm@1461
   305
        (strip_tac 1),
clasohm@1461
   306
        (rtac (inject_Ispair RS conjunct2) 1),
clasohm@1461
   307
        (fast_tac HOL_cs  3),
clasohm@1461
   308
        (fast_tac HOL_cs  1),
clasohm@1461
   309
        (fast_tac HOL_cs  1),
clasohm@1461
   310
        (fast_tac HOL_cs  1)
clasohm@1461
   311
        ]);
nipkow@243
   312
regensbu@1168
   313
qed_goal "Isfst2" Sprod0.thy "y~=UU ==>Isfst(Ispair x y)=x"
nipkow@243
   314
(fn prems =>
clasohm@1461
   315
        [
clasohm@1461
   316
        (cut_facts_tac prems 1),
clasohm@1461
   317
        (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
clasohm@1461
   318
        (etac Isfst 1),
clasohm@1461
   319
        (atac 1),
clasohm@1461
   320
        (hyp_subst_tac 1),
clasohm@1461
   321
        (rtac strict_Isfst1 1)
clasohm@1461
   322
        ]);
nipkow@243
   323
regensbu@1168
   324
qed_goal "Issnd2" Sprod0.thy "~x=UU ==>Issnd(Ispair x y)=y"
nipkow@243
   325
(fn prems =>
clasohm@1461
   326
        [
clasohm@1461
   327
        (cut_facts_tac prems 1),
clasohm@1461
   328
        (res_inst_tac [("Q","y=UU")] (excluded_middle RS disjE) 1),
clasohm@1461
   329
        (etac Issnd 1),
clasohm@1461
   330
        (atac 1),
clasohm@1461
   331
        (hyp_subst_tac 1),
clasohm@1461
   332
        (rtac strict_Issnd2 1)
clasohm@1461
   333
        ]);
nipkow@243
   334
nipkow@243
   335
nipkow@243
   336
(* ------------------------------------------------------------------------ *)
nipkow@243
   337
(* instantiate the simplifier                                               *)
nipkow@243
   338
(* ------------------------------------------------------------------------ *)
nipkow@243
   339
regensbu@1277
   340
val Sprod0_ss = 
regensbu@1277
   341
        HOL_ss 
regensbu@1277
   342
        addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
regensbu@1277
   343
                 Isfst2,Issnd2];
nipkow@243
   344
clasohm@892
   345
qed_goal "defined_IsfstIssnd" Sprod0.thy 
clasohm@1461
   346
        "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
nipkow@243
   347
 (fn prems =>
clasohm@1461
   348
        [
clasohm@1461
   349
        (cut_facts_tac prems 1),
clasohm@1461
   350
        (res_inst_tac [("p","p")] IsprodE 1),
clasohm@1461
   351
        (contr_tac 1),
clasohm@1461
   352
        (hyp_subst_tac 1),
clasohm@1461
   353
        (rtac conjI 1),
regensbu@1277
   354
        (asm_simp_tac Sprod0_ss 1),
regensbu@1277
   355
        (asm_simp_tac Sprod0_ss 1)
clasohm@1461
   356
        ]);
nipkow@243
   357
nipkow@243
   358
nipkow@243
   359
(* ------------------------------------------------------------------------ *)
nipkow@243
   360
(* Surjective pairing: equivalent to Exh_Sprod                              *)
nipkow@243
   361
(* ------------------------------------------------------------------------ *)
nipkow@243
   362
clasohm@892
   363
qed_goal "surjective_pairing_Sprod" Sprod0.thy 
clasohm@1461
   364
        "z = Ispair(Isfst z)(Issnd z)"
nipkow@243
   365
(fn prems =>
clasohm@1461
   366
        [
clasohm@1461
   367
        (res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1),
regensbu@1277
   368
        (asm_simp_tac Sprod0_ss 1),
clasohm@1461
   369
        (etac exE 1),
clasohm@1461
   370
        (etac exE 1),
regensbu@1277
   371
        (asm_simp_tac Sprod0_ss 1)
clasohm@1461
   372
        ]);
nipkow@243
   373
slotosch@2640
   374
qed_goal "Sel_injective_Sprod" thy 
slotosch@2640
   375
        "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
slotosch@2640
   376
(fn prems =>
slotosch@2640
   377
        [
slotosch@2640
   378
        (cut_facts_tac prems 1),
slotosch@2640
   379
        (subgoal_tac "Ispair(Isfst x)(Issnd x)=Ispair(Isfst y)(Issnd y)" 1),
slotosch@2640
   380
        (rotate_tac ~1 1),
slotosch@2640
   381
        (asm_full_simp_tac(HOL_ss addsimps[surjective_pairing_Sprod RS sym])1),
slotosch@2640
   382
        (Asm_simp_tac 1)
slotosch@2640
   383
        ]);