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