src/HOLCF/Ssum0.ML
author wenzelm
Sat Nov 03 01:41:26 2001 +0100 (2001-11-03)
changeset 12030 46d57d0290a2
parent 10834 a7897aebbffc
child 14981 e73f8140af78
permissions -rw-r--r--
GPLed;
paulson@9169
     1
(*  Title:      HOLCF/Ssum0.ML
nipkow@243
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Franz Regensburger
wenzelm@12030
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
nipkow@243
     5
paulson@9169
     6
Strict sum with typedef
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
(* ------------------------------------------------------------------------ *)
nipkow@243
    10
(* A non-emptyness result for Sssum                                         *)
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
paulson@9248
    13
Goalw [Ssum_def] "Sinl_Rep(a):Ssum";
paulson@10230
    14
by (Blast_tac 1);
paulson@9245
    15
qed "SsumIl";
nipkow@243
    16
paulson@9248
    17
Goalw [Ssum_def] "Sinr_Rep(a):Ssum";
paulson@10230
    18
by (Blast_tac 1);
paulson@9245
    19
qed "SsumIr";
nipkow@243
    20
paulson@9169
    21
Goal "inj_on Abs_Ssum Ssum";
paulson@9169
    22
by (rtac inj_on_inverseI 1);
paulson@9169
    23
by (etac Abs_Ssum_inverse 1);
paulson@9169
    24
qed "inj_on_Abs_Ssum";
nipkow@243
    25
nipkow@243
    26
(* ------------------------------------------------------------------------ *)
nipkow@243
    27
(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr                        *)
nipkow@243
    28
(* ------------------------------------------------------------------------ *)
nipkow@243
    29
paulson@9248
    30
Goalw [Sinr_Rep_def,Sinl_Rep_def]
paulson@9245
    31
 "Sinl_Rep(UU) = Sinr_Rep(UU)";
paulson@9245
    32
by (rtac ext 1);
paulson@9245
    33
by (rtac ext 1);
paulson@9245
    34
by (rtac ext 1);
paulson@9245
    35
by (fast_tac HOL_cs 1);
paulson@9245
    36
qed "strict_SinlSinr_Rep";
nipkow@243
    37
paulson@9248
    38
Goalw [Isinl_def,Isinr_def]
paulson@9245
    39
 "Isinl(UU) = Isinr(UU)";
paulson@9245
    40
by (rtac (strict_SinlSinr_Rep RS arg_cong) 1);
paulson@9245
    41
qed "strict_IsinlIsinr";
nipkow@243
    42
nipkow@243
    43
nipkow@243
    44
(* ------------------------------------------------------------------------ *)
nipkow@243
    45
(* distinctness of  Sinl_Rep, Sinr_Rep and Isinl, Isinr                     *)
nipkow@243
    46
(* ------------------------------------------------------------------------ *)
nipkow@243
    47
paulson@9248
    48
Goalw [Sinl_Rep_def,Sinr_Rep_def]
paulson@9245
    49
        "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU";
paulson@9248
    50
by (blast_tac (claset() addSDs [fun_cong]) 1);
paulson@9245
    51
qed "noteq_SinlSinr_Rep";
nipkow@243
    52
nipkow@243
    53
paulson@9248
    54
Goalw [Isinl_def,Isinr_def]
paulson@9245
    55
        "Isinl(a)=Isinr(b) ==> a=UU & b=UU";
paulson@9245
    56
by (rtac noteq_SinlSinr_Rep 1);
paulson@9245
    57
by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
paulson@9245
    58
by (rtac SsumIl 1);
paulson@9245
    59
by (rtac SsumIr 1);
paulson@9245
    60
qed "noteq_IsinlIsinr";
nipkow@243
    61
nipkow@243
    62
nipkow@243
    63
nipkow@243
    64
(* ------------------------------------------------------------------------ *)
nipkow@243
    65
(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr                       *)
nipkow@243
    66
(* ------------------------------------------------------------------------ *)
nipkow@243
    67
paulson@9248
    68
Goalw [Sinl_Rep_def] "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU";
paulson@9248
    69
by (blast_tac (claset() addSDs [fun_cong]) 1);
paulson@9245
    70
qed "inject_Sinl_Rep1";
nipkow@243
    71
paulson@9248
    72
Goalw [Sinr_Rep_def] "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU";
paulson@9248
    73
by (blast_tac (claset() addSDs [fun_cong]) 1);
paulson@9245
    74
qed "inject_Sinr_Rep1";
nipkow@243
    75
paulson@9248
    76
Goalw [Sinl_Rep_def]
paulson@9245
    77
"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2";
paulson@9248
    78
by (blast_tac (claset() addSDs [fun_cong]) 1);
paulson@9245
    79
qed "inject_Sinl_Rep2";
nipkow@243
    80
paulson@9248
    81
Goalw [Sinr_Rep_def]
paulson@9245
    82
"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2";
paulson@9248
    83
by (blast_tac (claset() addSDs [fun_cong]) 1);
paulson@9245
    84
qed "inject_Sinr_Rep2";
nipkow@243
    85
paulson@9169
    86
Goal "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2";
paulson@9169
    87
by (case_tac "a1=UU" 1);
paulson@9169
    88
by (hyp_subst_tac 1);
paulson@9169
    89
by (rtac (inject_Sinl_Rep1 RS sym) 1);
paulson@9169
    90
by (etac sym 1);
paulson@9169
    91
by (case_tac "a2=UU" 1);
paulson@9169
    92
by (hyp_subst_tac 1);
paulson@9169
    93
by (etac inject_Sinl_Rep1 1);
paulson@9169
    94
by (etac inject_Sinl_Rep2 1);
paulson@9169
    95
by (atac 1);
paulson@9169
    96
by (atac 1);
paulson@9169
    97
qed "inject_Sinl_Rep";
nipkow@243
    98
paulson@9169
    99
Goal "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2";
paulson@9169
   100
by (case_tac "b1=UU" 1);
paulson@9169
   101
by (hyp_subst_tac 1);
paulson@9169
   102
by (rtac (inject_Sinr_Rep1 RS sym) 1);
paulson@9169
   103
by (etac sym 1);
paulson@9169
   104
by (case_tac "b2=UU" 1);
paulson@9169
   105
by (hyp_subst_tac 1);
paulson@9169
   106
by (etac inject_Sinr_Rep1 1);
paulson@9169
   107
by (etac inject_Sinr_Rep2 1);
paulson@9169
   108
by (atac 1);
paulson@9169
   109
by (atac 1);
paulson@9169
   110
qed "inject_Sinr_Rep";
nipkow@243
   111
paulson@9248
   112
Goalw [Isinl_def] "Isinl(a1)=Isinl(a2)==> a1=a2";
paulson@9245
   113
by (rtac inject_Sinl_Rep 1);
paulson@9245
   114
by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
paulson@9245
   115
by (rtac SsumIl 1);
paulson@9245
   116
by (rtac SsumIl 1);
paulson@9245
   117
qed "inject_Isinl";
nipkow@243
   118
paulson@9248
   119
Goalw [Isinr_def] "Isinr(b1)=Isinr(b2) ==> b1=b2";
paulson@9245
   120
by (rtac inject_Sinr_Rep 1);
paulson@9245
   121
by (etac (inj_on_Abs_Ssum  RS inj_onD) 1);
paulson@9245
   122
by (rtac SsumIr 1);
paulson@9245
   123
by (rtac SsumIr 1);
paulson@9245
   124
qed "inject_Isinr";
nipkow@243
   125
paulson@10230
   126
AddSDs [inject_Isinl, inject_Isinr];
paulson@10230
   127
paulson@9169
   128
Goal "a1~=a2 ==> Isinl(a1) ~= Isinl(a2)";
paulson@10230
   129
by (Blast_tac 1);
paulson@9169
   130
qed "inject_Isinl_rev";
nipkow@243
   131
paulson@9169
   132
Goal "b1~=b2 ==> Isinr(b1) ~= Isinr(b2)";
paulson@10230
   133
by (Blast_tac 1);
paulson@9169
   134
qed "inject_Isinr_rev";
nipkow@243
   135
nipkow@243
   136
(* ------------------------------------------------------------------------ *)
nipkow@243
   137
(* Exhaustion of the strict sum ++                                          *)
nipkow@243
   138
(* choice of the bottom representation is arbitrary                         *)
nipkow@243
   139
(* ------------------------------------------------------------------------ *)
nipkow@243
   140
paulson@9248
   141
Goalw [Isinl_def,Isinr_def]
paulson@9245
   142
        "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)";
paulson@9245
   143
by (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1);
paulson@9245
   144
by (etac disjE 1);
paulson@9245
   145
by (etac exE 1);
paulson@9245
   146
by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1);
paulson@9245
   147
by (etac disjI1 1);
paulson@9245
   148
by (rtac disjI2 1);
paulson@9245
   149
by (rtac disjI1 1);
paulson@9245
   150
by (rtac exI 1);
paulson@9245
   151
by (rtac conjI 1);
paulson@9245
   152
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
paulson@9245
   153
by (etac arg_cong 1);
paulson@10230
   154
by (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos_nn 1);
paulson@9245
   155
by (etac arg_cong 2);
paulson@10230
   156
by (etac contrapos_nn 1);
paulson@9245
   157
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
paulson@9245
   158
by (rtac trans 1);
paulson@9245
   159
by (etac arg_cong 1);
paulson@9245
   160
by (etac arg_cong 1);
paulson@9245
   161
by (etac exE 1);
paulson@9245
   162
by (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1);
paulson@9245
   163
by (etac disjI1 1);
paulson@9245
   164
by (rtac disjI2 1);
paulson@9245
   165
by (rtac disjI2 1);
paulson@9245
   166
by (rtac exI 1);
paulson@9245
   167
by (rtac conjI 1);
paulson@9245
   168
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
paulson@9245
   169
by (etac arg_cong 1);
paulson@10230
   170
by (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos_nn 1);
paulson@9245
   171
by (hyp_subst_tac 2);
paulson@9245
   172
by (rtac (strict_SinlSinr_Rep RS sym) 2);
paulson@10230
   173
by (etac contrapos_nn 1);
paulson@9245
   174
by (rtac (Rep_Ssum_inverse RS sym RS trans) 1);
paulson@9245
   175
by (rtac trans 1);
paulson@9245
   176
by (etac arg_cong 1);
paulson@9245
   177
by (etac arg_cong 1);
paulson@9245
   178
qed "Exh_Ssum";
nipkow@243
   179
nipkow@243
   180
(* ------------------------------------------------------------------------ *)
nipkow@243
   181
(* elimination rules for the strict sum ++                                  *)
nipkow@243
   182
(* ------------------------------------------------------------------------ *)
nipkow@243
   183
paulson@9169
   184
val prems = Goal
clasohm@1461
   185
        "[|p=Isinl(UU) ==> Q ;\
clasohm@1461
   186
\       !!x.[|p=Isinl(x); x~=UU |] ==> Q;\
paulson@9169
   187
\       !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q";
paulson@9169
   188
by (rtac (Exh_Ssum RS disjE) 1);
paulson@9169
   189
by (etac disjE 2);
paulson@9169
   190
by (eresolve_tac prems 1);
paulson@9169
   191
by (etac exE 1);
paulson@9169
   192
by (etac conjE 1);
paulson@9169
   193
by (eresolve_tac prems 1);
paulson@9169
   194
by (atac 1);
paulson@9169
   195
by (etac exE 1);
paulson@9169
   196
by (etac conjE 1);
paulson@9169
   197
by (eresolve_tac prems 1);
paulson@9169
   198
by (atac 1);
paulson@9169
   199
qed "IssumE";
nipkow@243
   200
paulson@9169
   201
val prems = Goal
paulson@9169
   202
"[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q";
paulson@9169
   203
by (rtac IssumE 1);
paulson@9169
   204
by (eresolve_tac prems 1);
paulson@9169
   205
by (eresolve_tac prems 1);
paulson@9169
   206
by (eresolve_tac prems 1);
paulson@9169
   207
qed "IssumE2";
nipkow@243
   208
nipkow@243
   209
nipkow@243
   210
nipkow@243
   211
nipkow@243
   212
(* ------------------------------------------------------------------------ *)
nipkow@243
   213
(* rewrites for Iwhen                                                       *)
nipkow@243
   214
(* ------------------------------------------------------------------------ *)
nipkow@243
   215
paulson@9248
   216
Goalw [Iwhen_def]
paulson@9245
   217
        "Iwhen f g (Isinl UU) = UU";
paulson@9969
   218
by (rtac some_equality 1);
paulson@9245
   219
by (rtac conjI 1);
paulson@9245
   220
by (fast_tac HOL_cs  1);
paulson@9245
   221
by (rtac conjI 1);
paulson@9245
   222
by (strip_tac 1);
paulson@9245
   223
by (res_inst_tac [("P","a=UU")] notE 1);
paulson@9245
   224
by (fast_tac HOL_cs  1);
paulson@9245
   225
by (rtac inject_Isinl 1);
paulson@9245
   226
by (rtac sym 1);
paulson@9245
   227
by (fast_tac HOL_cs  1);
paulson@9245
   228
by (strip_tac 1);
paulson@9245
   229
by (res_inst_tac [("P","b=UU")] notE 1);
paulson@9245
   230
by (fast_tac HOL_cs  1);
paulson@9245
   231
by (rtac inject_Isinr 1);
paulson@9245
   232
by (rtac sym 1);
paulson@9245
   233
by (rtac (strict_IsinlIsinr RS subst) 1);
paulson@9245
   234
by (fast_tac HOL_cs  1);
paulson@9245
   235
by (fast_tac HOL_cs  1);
paulson@9245
   236
qed "Iwhen1";
nipkow@243
   237
nipkow@243
   238
paulson@9248
   239
Goalw [Iwhen_def]
nipkow@10834
   240
        "x~=UU ==> Iwhen f g (Isinl x) = f$x";
paulson@9969
   241
by (rtac some_equality 1);
paulson@9245
   242
by (fast_tac HOL_cs  2);
paulson@9245
   243
by (rtac conjI 1);
paulson@9245
   244
by (strip_tac 1);
paulson@9245
   245
by (res_inst_tac [("P","x=UU")] notE 1);
paulson@9245
   246
by (atac 1);
paulson@9245
   247
by (rtac inject_Isinl 1);
paulson@9245
   248
by (atac 1);
paulson@9245
   249
by (rtac conjI 1);
paulson@9245
   250
by (strip_tac 1);
paulson@9245
   251
by (rtac cfun_arg_cong 1);
paulson@9245
   252
by (rtac inject_Isinl 1);
paulson@9245
   253
by (fast_tac HOL_cs  1);
paulson@9245
   254
by (strip_tac 1);
paulson@9245
   255
by (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1);
paulson@9245
   256
by (fast_tac HOL_cs  2);
paulson@10230
   257
by (rtac contrapos_nn 1);
paulson@9245
   258
by (etac noteq_IsinlIsinr 2);
paulson@9245
   259
by (fast_tac HOL_cs  1);
paulson@9245
   260
qed "Iwhen2";
nipkow@243
   261
paulson@9248
   262
Goalw [Iwhen_def]
nipkow@10834
   263
        "y~=UU ==> Iwhen f g (Isinr y) = g$y";
paulson@9969
   264
by (rtac some_equality 1);
paulson@9245
   265
by (fast_tac HOL_cs  2);
paulson@9245
   266
by (rtac conjI 1);
paulson@9245
   267
by (strip_tac 1);
paulson@9245
   268
by (res_inst_tac [("P","y=UU")] notE 1);
paulson@9245
   269
by (atac 1);
paulson@9245
   270
by (rtac inject_Isinr 1);
paulson@9245
   271
by (rtac (strict_IsinlIsinr RS subst) 1);
paulson@9245
   272
by (atac 1);
paulson@9245
   273
by (rtac conjI 1);
paulson@9245
   274
by (strip_tac 1);
paulson@9245
   275
by (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1);
paulson@9245
   276
by (fast_tac HOL_cs  2);
paulson@10230
   277
by (rtac contrapos_nn 1);
paulson@9245
   278
by (etac (sym RS noteq_IsinlIsinr) 2);
paulson@9245
   279
by (fast_tac HOL_cs  1);
paulson@9245
   280
by (strip_tac 1);
paulson@9245
   281
by (rtac cfun_arg_cong 1);
paulson@9245
   282
by (rtac inject_Isinr 1);
paulson@9245
   283
by (fast_tac HOL_cs  1);
paulson@9245
   284
qed "Iwhen3";
nipkow@243
   285
nipkow@243
   286
(* ------------------------------------------------------------------------ *)
nipkow@243
   287
(* instantiate the simplifier                                               *)
nipkow@243
   288
(* ------------------------------------------------------------------------ *)
nipkow@243
   289
oheimb@8161
   290
val Ssum0_ss = (simpset_of Cfun3.thy) delsimps [range_composition] addsimps 
regensbu@1277
   291
                [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
regensbu@1277
   292
paulson@9248
   293
Addsimps [strict_IsinlIsinr RS sym, Iwhen1, Iwhen2, Iwhen3];