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