src/HOLCF/Ssum0.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4833 2e53109d4bc8
child 8161 bde1391fd0a5
permissions -rw-r--r--
made tutorial first;
clasohm@1461
     1
(*  Title:      HOLCF/ssum0.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 theory ssum0.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Ssum0;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* A non-emptyness result for Sssum                                         *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
clasohm@892
    15
qed_goalw "SsumIl" Ssum0.thy [Ssum_def] "Sinl_Rep(a):Ssum"
nipkow@243
    16
 (fn prems =>
clasohm@1461
    17
        [
clasohm@1461
    18
        (rtac CollectI 1),
clasohm@1461
    19
        (rtac disjI1 1),
clasohm@1461
    20
        (rtac exI 1),
clasohm@1461
    21
        (rtac refl 1)
clasohm@1461
    22
        ]);
nipkow@243
    23
clasohm@892
    24
qed_goalw "SsumIr" Ssum0.thy [Ssum_def] "Sinr_Rep(a):Ssum"
nipkow@243
    25
 (fn prems =>
clasohm@1461
    26
        [
clasohm@1461
    27
        (rtac CollectI 1),
clasohm@1461
    28
        (rtac disjI2 1),
clasohm@1461
    29
        (rtac exI 1),
clasohm@1461
    30
        (rtac refl 1)
clasohm@1461
    31
        ]);
nipkow@243
    32
nipkow@4833
    33
qed_goal "inj_on_Abs_Ssum" Ssum0.thy "inj_on Abs_Ssum Ssum"
nipkow@243
    34
(fn prems =>
clasohm@1461
    35
        [
nipkow@4833
    36
        (rtac inj_on_inverseI 1),
clasohm@1461
    37
        (etac Abs_Ssum_inverse 1)
clasohm@1461
    38
        ]);
nipkow@243
    39
nipkow@243
    40
(* ------------------------------------------------------------------------ *)
nipkow@243
    41
(* Strictness of Sinr_Rep, Sinl_Rep and Isinl, Isinr                        *)
nipkow@243
    42
(* ------------------------------------------------------------------------ *)
nipkow@243
    43
clasohm@892
    44
qed_goalw "strict_SinlSinr_Rep" Ssum0.thy [Sinr_Rep_def,Sinl_Rep_def]
nipkow@243
    45
 "Sinl_Rep(UU) = Sinr_Rep(UU)"
nipkow@243
    46
 (fn prems =>
clasohm@1461
    47
        [
clasohm@1461
    48
        (rtac ext 1),
clasohm@1461
    49
        (rtac ext 1),
clasohm@1461
    50
        (rtac ext 1),
clasohm@1461
    51
        (fast_tac HOL_cs 1)
clasohm@1461
    52
        ]);
nipkow@243
    53
clasohm@892
    54
qed_goalw "strict_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
nipkow@243
    55
 "Isinl(UU) = Isinr(UU)"
nipkow@243
    56
 (fn prems =>
clasohm@1461
    57
        [
clasohm@1461
    58
        (rtac (strict_SinlSinr_Rep RS arg_cong) 1)
clasohm@1461
    59
        ]);
nipkow@243
    60
nipkow@243
    61
nipkow@243
    62
(* ------------------------------------------------------------------------ *)
nipkow@243
    63
(* distinctness of  Sinl_Rep, Sinr_Rep and Isinl, Isinr                     *)
nipkow@243
    64
(* ------------------------------------------------------------------------ *)
nipkow@243
    65
clasohm@892
    66
qed_goalw "noteq_SinlSinr_Rep" Ssum0.thy [Sinl_Rep_def,Sinr_Rep_def]
clasohm@1461
    67
        "(Sinl_Rep(a) = Sinr_Rep(b)) ==> a=UU & b=UU"
nipkow@243
    68
 (fn prems =>
clasohm@1461
    69
        [
clasohm@1461
    70
        (rtac conjI 1),
oheimb@1675
    71
        (case_tac "a=UU" 1),
clasohm@1461
    72
        (atac 1),
clasohm@1461
    73
        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD2 
clasohm@1461
    74
        RS mp RS conjunct1 RS sym) 1),
clasohm@1461
    75
        (fast_tac HOL_cs 1),
clasohm@1461
    76
        (atac 1),
oheimb@1675
    77
        (case_tac "b=UU" 1),
clasohm@1461
    78
        (atac 1),
clasohm@1461
    79
        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong RS iffD1 
clasohm@1461
    80
        RS mp RS conjunct1 RS sym) 1),
clasohm@1461
    81
        (fast_tac HOL_cs 1),
clasohm@1461
    82
        (atac 1)
clasohm@1461
    83
        ]);
nipkow@243
    84
nipkow@243
    85
clasohm@892
    86
qed_goalw "noteq_IsinlIsinr" Ssum0.thy [Isinl_def,Isinr_def]
clasohm@1461
    87
        "Isinl(a)=Isinr(b) ==> a=UU & b=UU"
nipkow@243
    88
 (fn prems =>
clasohm@1461
    89
        [
clasohm@1461
    90
        (cut_facts_tac prems 1),
clasohm@1461
    91
        (rtac noteq_SinlSinr_Rep 1),
nipkow@4833
    92
        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
clasohm@1461
    93
        (rtac SsumIl 1),
clasohm@1461
    94
        (rtac SsumIr 1)
clasohm@1461
    95
        ]);
nipkow@243
    96
nipkow@243
    97
nipkow@243
    98
nipkow@243
    99
(* ------------------------------------------------------------------------ *)
nipkow@243
   100
(* injectivity of Sinl_Rep, Sinr_Rep and Isinl, Isinr                       *)
nipkow@243
   101
(* ------------------------------------------------------------------------ *)
nipkow@243
   102
clasohm@892
   103
qed_goalw "inject_Sinl_Rep1" Ssum0.thy [Sinl_Rep_def]
nipkow@243
   104
 "(Sinl_Rep(a) = Sinl_Rep(UU)) ==> a=UU"
nipkow@243
   105
 (fn prems =>
clasohm@1461
   106
        [
oheimb@1675
   107
        (case_tac "a=UU" 1),
clasohm@1461
   108
        (atac 1),
clasohm@1461
   109
        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
clasohm@1461
   110
        RS iffD2 RS mp RS conjunct1 RS sym) 1),
clasohm@1461
   111
        (fast_tac HOL_cs 1),
clasohm@1461
   112
        (atac 1)
clasohm@1461
   113
        ]);
nipkow@243
   114
clasohm@892
   115
qed_goalw "inject_Sinr_Rep1" Ssum0.thy [Sinr_Rep_def]
nipkow@243
   116
 "(Sinr_Rep(b) = Sinr_Rep(UU)) ==> b=UU"
nipkow@243
   117
 (fn prems =>
clasohm@1461
   118
        [
oheimb@1675
   119
        (case_tac "b=UU" 1),
clasohm@1461
   120
        (atac 1),
clasohm@1461
   121
        (rtac ((hd prems) RS fun_cong RS fun_cong RS fun_cong 
clasohm@1461
   122
        RS iffD2 RS mp RS conjunct1 RS sym) 1),
clasohm@1461
   123
        (fast_tac HOL_cs 1),
clasohm@1461
   124
        (atac 1)
clasohm@1461
   125
        ]);
nipkow@243
   126
clasohm@892
   127
qed_goalw "inject_Sinl_Rep2" Ssum0.thy [Sinl_Rep_def]
regensbu@1168
   128
"[| a1~=UU ; a2~=UU ; Sinl_Rep(a1)=Sinl_Rep(a2) |] ==> a1=a2"
nipkow@243
   129
 (fn prems =>
clasohm@1461
   130
        [
clasohm@1461
   131
        (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong 
clasohm@1461
   132
        RS iffD1 RS mp RS conjunct1) 1),
clasohm@1461
   133
        (fast_tac HOL_cs 1),
clasohm@1461
   134
        (resolve_tac prems 1)
clasohm@1461
   135
        ]);
nipkow@243
   136
clasohm@892
   137
qed_goalw "inject_Sinr_Rep2" Ssum0.thy [Sinr_Rep_def]
regensbu@1168
   138
"[|b1~=UU ; b2~=UU ; Sinr_Rep(b1)=Sinr_Rep(b2) |] ==> b1=b2"
nipkow@243
   139
 (fn prems =>
clasohm@1461
   140
        [
clasohm@1461
   141
        (rtac ((nth_elem (2,prems)) RS fun_cong  RS fun_cong RS fun_cong 
clasohm@1461
   142
        RS iffD1 RS mp RS conjunct1) 1),
clasohm@1461
   143
        (fast_tac HOL_cs 1),
clasohm@1461
   144
        (resolve_tac prems 1)
clasohm@1461
   145
        ]);
nipkow@243
   146
clasohm@892
   147
qed_goal "inject_Sinl_Rep" Ssum0.thy 
clasohm@1461
   148
        "Sinl_Rep(a1)=Sinl_Rep(a2) ==> a1=a2"
nipkow@243
   149
 (fn prems =>
clasohm@1461
   150
        [
clasohm@1461
   151
        (cut_facts_tac prems 1),
oheimb@1675
   152
        (case_tac "a1=UU" 1),
clasohm@1461
   153
        (hyp_subst_tac 1),
clasohm@1461
   154
        (rtac (inject_Sinl_Rep1 RS sym) 1),
clasohm@1461
   155
        (etac sym 1),
oheimb@1675
   156
        (case_tac "a2=UU" 1),
clasohm@1461
   157
        (hyp_subst_tac 1),
clasohm@1461
   158
        (etac inject_Sinl_Rep1 1),
clasohm@1461
   159
        (etac inject_Sinl_Rep2 1),
clasohm@1461
   160
        (atac 1),
clasohm@1461
   161
        (atac 1)
clasohm@1461
   162
        ]);
nipkow@243
   163
clasohm@892
   164
qed_goal "inject_Sinr_Rep" Ssum0.thy 
clasohm@1461
   165
        "Sinr_Rep(b1)=Sinr_Rep(b2) ==> b1=b2"
nipkow@243
   166
 (fn prems =>
clasohm@1461
   167
        [
clasohm@1461
   168
        (cut_facts_tac prems 1),
oheimb@1675
   169
        (case_tac "b1=UU" 1),
clasohm@1461
   170
        (hyp_subst_tac 1),
clasohm@1461
   171
        (rtac (inject_Sinr_Rep1 RS sym) 1),
clasohm@1461
   172
        (etac sym 1),
oheimb@1675
   173
        (case_tac "b2=UU" 1),
clasohm@1461
   174
        (hyp_subst_tac 1),
clasohm@1461
   175
        (etac inject_Sinr_Rep1 1),
clasohm@1461
   176
        (etac inject_Sinr_Rep2 1),
clasohm@1461
   177
        (atac 1),
clasohm@1461
   178
        (atac 1)
clasohm@1461
   179
        ]);
nipkow@243
   180
clasohm@892
   181
qed_goalw "inject_Isinl" Ssum0.thy [Isinl_def]
nipkow@243
   182
"Isinl(a1)=Isinl(a2)==> a1=a2"
nipkow@243
   183
 (fn prems =>
clasohm@1461
   184
        [
clasohm@1461
   185
        (cut_facts_tac prems 1),
clasohm@1461
   186
        (rtac inject_Sinl_Rep 1),
nipkow@4833
   187
        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
clasohm@1461
   188
        (rtac SsumIl 1),
clasohm@1461
   189
        (rtac SsumIl 1)
clasohm@1461
   190
        ]);
nipkow@243
   191
clasohm@892
   192
qed_goalw "inject_Isinr" Ssum0.thy [Isinr_def]
nipkow@243
   193
"Isinr(b1)=Isinr(b2) ==> b1=b2"
nipkow@243
   194
 (fn prems =>
clasohm@1461
   195
        [
clasohm@1461
   196
        (cut_facts_tac prems 1),
clasohm@1461
   197
        (rtac inject_Sinr_Rep 1),
nipkow@4833
   198
        (etac (inj_on_Abs_Ssum  RS inj_onD) 1),
clasohm@1461
   199
        (rtac SsumIr 1),
clasohm@1461
   200
        (rtac SsumIr 1)
clasohm@1461
   201
        ]);
nipkow@243
   202
clasohm@892
   203
qed_goal "inject_Isinl_rev" Ssum0.thy  
regensbu@1168
   204
"a1~=a2 ==> Isinl(a1) ~= Isinl(a2)"
nipkow@243
   205
 (fn prems =>
clasohm@1461
   206
        [
clasohm@1461
   207
        (cut_facts_tac prems 1),
clasohm@1461
   208
        (rtac contrapos 1),
clasohm@1461
   209
        (etac inject_Isinl 2),
clasohm@1461
   210
        (atac 1)
clasohm@1461
   211
        ]);
nipkow@243
   212
clasohm@892
   213
qed_goal "inject_Isinr_rev" Ssum0.thy  
regensbu@1168
   214
"b1~=b2 ==> Isinr(b1) ~= Isinr(b2)"
nipkow@243
   215
 (fn prems =>
clasohm@1461
   216
        [
clasohm@1461
   217
        (cut_facts_tac prems 1),
clasohm@1461
   218
        (rtac contrapos 1),
clasohm@1461
   219
        (etac inject_Isinr 2),
clasohm@1461
   220
        (atac 1)
clasohm@1461
   221
        ]);
nipkow@243
   222
nipkow@243
   223
(* ------------------------------------------------------------------------ *)
nipkow@243
   224
(* Exhaustion of the strict sum ++                                          *)
nipkow@243
   225
(* choice of the bottom representation is arbitrary                         *)
nipkow@243
   226
(* ------------------------------------------------------------------------ *)
nipkow@243
   227
clasohm@892
   228
qed_goalw "Exh_Ssum" Ssum0.thy [Isinl_def,Isinr_def]
clasohm@1461
   229
        "z=Isinl(UU) | (? a. z=Isinl(a) & a~=UU) | (? b. z=Isinr(b) & b~=UU)"
nipkow@243
   230
 (fn prems =>
clasohm@1461
   231
        [
clasohm@1461
   232
        (rtac (rewrite_rule [Ssum_def] Rep_Ssum RS CollectE) 1),
clasohm@1461
   233
        (etac disjE 1),
clasohm@1461
   234
        (etac exE 1),
oheimb@1675
   235
        (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
clasohm@1461
   236
        (etac disjI1 1),
clasohm@1461
   237
        (rtac disjI2 1),
clasohm@1461
   238
        (rtac disjI1 1),
clasohm@1461
   239
        (rtac exI 1),
clasohm@1461
   240
        (rtac conjI 1),
clasohm@1461
   241
        (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
clasohm@1461
   242
        (etac arg_cong 1),
clasohm@1461
   243
        (res_inst_tac [("Q","Sinl_Rep(a)=Sinl_Rep(UU)")] contrapos 1),
clasohm@1461
   244
        (etac arg_cong 2),
clasohm@1461
   245
        (etac contrapos 1),
clasohm@1461
   246
        (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
clasohm@1461
   247
        (rtac trans 1),
clasohm@1461
   248
        (etac arg_cong 1),
clasohm@1461
   249
        (etac arg_cong 1),
clasohm@1461
   250
        (etac exE 1),
oheimb@1675
   251
        (case_tac "z= Abs_Ssum(Sinl_Rep(UU))" 1),
clasohm@1461
   252
        (etac disjI1 1),
clasohm@1461
   253
        (rtac disjI2 1),
clasohm@1461
   254
        (rtac disjI2 1),
clasohm@1461
   255
        (rtac exI 1),
clasohm@1461
   256
        (rtac conjI 1),
clasohm@1461
   257
        (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
clasohm@1461
   258
        (etac arg_cong 1),
clasohm@1461
   259
        (res_inst_tac [("Q","Sinr_Rep(b)=Sinl_Rep(UU)")] contrapos 1),
clasohm@1461
   260
        (hyp_subst_tac 2),
clasohm@1461
   261
        (rtac (strict_SinlSinr_Rep RS sym) 2),
clasohm@1461
   262
        (etac contrapos 1),
clasohm@1461
   263
        (rtac (Rep_Ssum_inverse RS sym RS trans) 1),
clasohm@1461
   264
        (rtac trans 1),
clasohm@1461
   265
        (etac arg_cong 1),
clasohm@1461
   266
        (etac arg_cong 1)
clasohm@1461
   267
        ]);
nipkow@243
   268
nipkow@243
   269
(* ------------------------------------------------------------------------ *)
nipkow@243
   270
(* elimination rules for the strict sum ++                                  *)
nipkow@243
   271
(* ------------------------------------------------------------------------ *)
nipkow@243
   272
clasohm@892
   273
qed_goal "IssumE" Ssum0.thy
clasohm@1461
   274
        "[|p=Isinl(UU) ==> Q ;\
clasohm@1461
   275
\       !!x.[|p=Isinl(x); x~=UU |] ==> Q;\
clasohm@1461
   276
\       !!y.[|p=Isinr(y); y~=UU |] ==> Q|] ==> Q"
nipkow@243
   277
 (fn prems =>
clasohm@1461
   278
        [
clasohm@1461
   279
        (rtac (Exh_Ssum RS disjE) 1),
clasohm@1461
   280
        (etac disjE 2),
clasohm@1461
   281
        (eresolve_tac prems 1),
clasohm@1461
   282
        (etac exE 1),
clasohm@1461
   283
        (etac conjE 1),
clasohm@1461
   284
        (eresolve_tac prems 1),
clasohm@1461
   285
        (atac 1),
clasohm@1461
   286
        (etac exE 1),
clasohm@1461
   287
        (etac conjE 1),
clasohm@1461
   288
        (eresolve_tac prems 1),
clasohm@1461
   289
        (atac 1)
clasohm@1461
   290
        ]);
nipkow@243
   291
clasohm@892
   292
qed_goal "IssumE2" Ssum0.thy 
nipkow@243
   293
"[| !!x. [| p = Isinl(x) |] ==> Q;   !!y. [| p = Isinr(y) |] ==> Q |] ==>Q"
nipkow@243
   294
 (fn prems =>
clasohm@1461
   295
        [
clasohm@1461
   296
        (rtac IssumE 1),
clasohm@1461
   297
        (eresolve_tac prems 1), 
clasohm@1461
   298
        (eresolve_tac prems 1), 
clasohm@1461
   299
        (eresolve_tac prems 1)
clasohm@1461
   300
        ]);
nipkow@243
   301
nipkow@243
   302
nipkow@243
   303
nipkow@243
   304
nipkow@243
   305
(* ------------------------------------------------------------------------ *)
nipkow@243
   306
(* rewrites for Iwhen                                                       *)
nipkow@243
   307
(* ------------------------------------------------------------------------ *)
nipkow@243
   308
clasohm@892
   309
qed_goalw "Iwhen1" Ssum0.thy [Iwhen_def]
clasohm@1461
   310
        "Iwhen f g (Isinl UU) = UU"
nipkow@243
   311
 (fn prems =>
clasohm@1461
   312
        [
oheimb@4535
   313
        (rtac select_equality 1),
clasohm@1461
   314
        (rtac conjI 1),
clasohm@1461
   315
        (fast_tac HOL_cs  1),
clasohm@1461
   316
        (rtac conjI 1),
clasohm@1461
   317
        (strip_tac 1),
clasohm@1461
   318
        (res_inst_tac [("P","a=UU")] notE 1),
clasohm@1461
   319
        (fast_tac HOL_cs  1),
clasohm@1461
   320
        (rtac inject_Isinl 1),
clasohm@1461
   321
        (rtac sym 1),
clasohm@1461
   322
        (fast_tac HOL_cs  1),
clasohm@1461
   323
        (strip_tac 1),
clasohm@1461
   324
        (res_inst_tac [("P","b=UU")] notE 1),
clasohm@1461
   325
        (fast_tac HOL_cs  1),
clasohm@1461
   326
        (rtac inject_Isinr 1),
clasohm@1461
   327
        (rtac sym 1),
clasohm@1461
   328
        (rtac (strict_IsinlIsinr RS subst) 1),
clasohm@1461
   329
        (fast_tac HOL_cs  1),
clasohm@1461
   330
        (fast_tac HOL_cs  1)
clasohm@1461
   331
        ]);
nipkow@243
   332
nipkow@243
   333
clasohm@892
   334
qed_goalw "Iwhen2" Ssum0.thy [Iwhen_def]
clasohm@1461
   335
        "x~=UU ==> Iwhen f g (Isinl x) = f`x"
nipkow@243
   336
 (fn prems =>
clasohm@1461
   337
        [
clasohm@1461
   338
        (cut_facts_tac prems 1),
oheimb@4535
   339
        (rtac select_equality 1),
clasohm@1461
   340
        (fast_tac HOL_cs  2),
clasohm@1461
   341
        (rtac conjI 1),
clasohm@1461
   342
        (strip_tac 1),
clasohm@1461
   343
        (res_inst_tac [("P","x=UU")] notE 1),
clasohm@1461
   344
        (atac 1),
clasohm@1461
   345
        (rtac inject_Isinl 1),
clasohm@1461
   346
        (atac 1),
clasohm@1461
   347
        (rtac conjI 1),
clasohm@1461
   348
        (strip_tac 1),
clasohm@1461
   349
        (rtac cfun_arg_cong 1),
clasohm@1461
   350
        (rtac inject_Isinl 1),
clasohm@1461
   351
        (fast_tac HOL_cs  1),
clasohm@1461
   352
        (strip_tac 1),
clasohm@1461
   353
        (res_inst_tac [("P","Isinl(x) = Isinr(b)")] notE 1),
clasohm@1461
   354
        (fast_tac HOL_cs  2),
clasohm@1461
   355
        (rtac contrapos 1),
clasohm@1461
   356
        (etac noteq_IsinlIsinr 2),
clasohm@1461
   357
        (fast_tac HOL_cs  1)
clasohm@1461
   358
        ]);
nipkow@243
   359
clasohm@892
   360
qed_goalw "Iwhen3" Ssum0.thy [Iwhen_def]
clasohm@1461
   361
        "y~=UU ==> Iwhen f g (Isinr y) = g`y"
nipkow@243
   362
 (fn prems =>
clasohm@1461
   363
        [
clasohm@1461
   364
        (cut_facts_tac prems 1),
oheimb@4535
   365
        (rtac select_equality 1),
clasohm@1461
   366
        (fast_tac HOL_cs  2),
clasohm@1461
   367
        (rtac conjI 1),
clasohm@1461
   368
        (strip_tac 1),
clasohm@1461
   369
        (res_inst_tac [("P","y=UU")] notE 1),
clasohm@1461
   370
        (atac 1),
clasohm@1461
   371
        (rtac inject_Isinr 1),
clasohm@1461
   372
        (rtac (strict_IsinlIsinr RS subst) 1),
clasohm@1461
   373
        (atac 1),
clasohm@1461
   374
        (rtac conjI 1),
clasohm@1461
   375
        (strip_tac 1),
clasohm@1461
   376
        (res_inst_tac [("P","Isinr(y) = Isinl(a)")] notE 1),
clasohm@1461
   377
        (fast_tac HOL_cs  2),
clasohm@1461
   378
        (rtac contrapos 1),
clasohm@1461
   379
        (etac (sym RS noteq_IsinlIsinr) 2),
clasohm@1461
   380
        (fast_tac HOL_cs  1),
clasohm@1461
   381
        (strip_tac 1),
clasohm@1461
   382
        (rtac cfun_arg_cong 1),
clasohm@1461
   383
        (rtac inject_Isinr 1),
clasohm@1461
   384
        (fast_tac HOL_cs  1)
clasohm@1461
   385
        ]);
nipkow@243
   386
nipkow@243
   387
(* ------------------------------------------------------------------------ *)
nipkow@243
   388
(* instantiate the simplifier                                               *)
nipkow@243
   389
(* ------------------------------------------------------------------------ *)
nipkow@243
   390
wenzelm@4098
   391
val Ssum0_ss = (simpset_of Cfun3.thy) addsimps 
regensbu@1277
   392
                [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
regensbu@1277
   393