src/HOLCF/sprod3.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/sprod3.thy
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 Sprod3.thy 
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
open Sprod3;
nipkow@243
    10
nipkow@243
    11
(* ------------------------------------------------------------------------ *)
nipkow@243
    12
(* continuity of Ispair, Isfst, Issnd                                       *)
nipkow@243
    13
(* ------------------------------------------------------------------------ *)
nipkow@243
    14
nipkow@243
    15
val sprod3_lemma1 = prove_goal Sprod3.thy 
nipkow@243
    16
"[| is_chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==>\
nipkow@243
    17
\ Ispair(lub(range(Y)),x) =\
nipkow@243
    18
\ Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\
nipkow@243
    19
\        lub(range(%i. Issnd(Ispair(Y(i),x)))))"
nipkow@243
    20
 (fn prems =>
nipkow@243
    21
	[
nipkow@243
    22
	(cut_facts_tac prems 1),
nipkow@243
    23
	(res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
nipkow@243
    24
	(rtac lub_equal 1),
nipkow@243
    25
	(atac 1),
nipkow@243
    26
	(rtac (monofun_Isfst RS ch2ch_monofun) 1),
nipkow@243
    27
	(rtac ch2ch_fun 1),
nipkow@243
    28
	(rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
nipkow@243
    29
	(atac 1),
nipkow@243
    30
	(rtac allI 1),
nipkow@243
    31
	(asm_simp_tac Sprod_ss 1),
nipkow@243
    32
	(rtac sym 1),
nipkow@243
    33
	(rtac lub_chain_maxelem 1),
nipkow@243
    34
	(rtac (monofun_Issnd RS ch2ch_monofun) 1),
nipkow@243
    35
	(rtac ch2ch_fun 1),
nipkow@243
    36
	(rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
nipkow@243
    37
	(atac 1),
nipkow@243
    38
	(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
nipkow@243
    39
	(rtac (notall2ex RS iffD1) 1),
nipkow@243
    40
	(res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
nipkow@243
    41
	(atac 1),
nipkow@243
    42
	(rtac chain_UU_I_inverse 1),
nipkow@243
    43
	(atac 1),
nipkow@243
    44
	(rtac exI 1),
nipkow@243
    45
	(etac Issnd2 1),
nipkow@243
    46
	(rtac allI 1),
nipkow@243
    47
	(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
nipkow@243
    48
	(asm_simp_tac Sprod_ss  1),
nipkow@243
    49
	(rtac refl_less 1),
nipkow@243
    50
	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
nipkow@243
    51
	(etac sym 1),
nipkow@243
    52
	(asm_simp_tac Sprod_ss  1),
nipkow@243
    53
	(rtac minimal 1)
nipkow@243
    54
	]);
nipkow@243
    55
nipkow@243
    56
nipkow@243
    57
val sprod3_lemma2 = prove_goal Sprod3.thy 
nipkow@243
    58
"[| is_chain(Y); ~ x = UU; lub(range(Y)) = UU |] ==>\
nipkow@243
    59
\   Ispair(lub(range(Y)),x) =\
nipkow@243
    60
\   Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\
nipkow@243
    61
\          lub(range(%i. Issnd(Ispair(Y(i),x)))))"
nipkow@243
    62
 (fn prems =>
nipkow@243
    63
	[
nipkow@243
    64
	(cut_facts_tac prems 1),
nipkow@243
    65
	(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
nipkow@243
    66
	(atac 1),
nipkow@243
    67
	(rtac trans 1),
nipkow@243
    68
	(rtac strict_Ispair1 1),
nipkow@243
    69
	(rtac (strict_Ispair RS sym) 1),
nipkow@243
    70
	(rtac disjI1 1),
nipkow@243
    71
	(rtac chain_UU_I_inverse 1),
nipkow@243
    72
	(rtac allI 1),
nipkow@243
    73
	(asm_simp_tac Sprod_ss  1),
nipkow@243
    74
	(etac (chain_UU_I RS spec) 1),
nipkow@243
    75
	(atac 1)
nipkow@243
    76
	]);
nipkow@243
    77
nipkow@243
    78
nipkow@243
    79
val sprod3_lemma3 = prove_goal Sprod3.thy 
nipkow@243
    80
"[| is_chain(Y); x = UU |] ==>\
nipkow@243
    81
\          Ispair(lub(range(Y)),x) =\
nipkow@243
    82
\          Ispair(lub(range(%i. Isfst(Ispair(Y(i),x)))),\
nipkow@243
    83
\                  lub(range(%i. Issnd(Ispair(Y(i),x)))))"
nipkow@243
    84
 (fn prems =>
nipkow@243
    85
	[
nipkow@243
    86
	(cut_facts_tac prems 1),
nipkow@243
    87
	(res_inst_tac [("s","UU"),("t","x")] ssubst 1),
nipkow@243
    88
	(atac 1),
nipkow@243
    89
	(rtac trans 1),
nipkow@243
    90
	(rtac strict_Ispair2 1),
nipkow@243
    91
	(rtac (strict_Ispair RS sym) 1),
nipkow@243
    92
	(rtac disjI1 1),
nipkow@243
    93
	(rtac chain_UU_I_inverse 1),
nipkow@243
    94
	(rtac allI 1),
nipkow@243
    95
	(simp_tac Sprod_ss  1)
nipkow@243
    96
	]);
nipkow@243
    97
nipkow@243
    98
nipkow@243
    99
val contlub_Ispair1 = prove_goal Sprod3.thy "contlub(Ispair)"
nipkow@243
   100
(fn prems =>
nipkow@243
   101
	[
nipkow@243
   102
	(rtac contlubI 1),
nipkow@243
   103
	(strip_tac 1),
nipkow@243
   104
	(rtac (expand_fun_eq RS iffD2) 1),
nipkow@243
   105
	(strip_tac 1),
nipkow@243
   106
	(rtac (lub_fun RS thelubI RS ssubst) 1),
nipkow@243
   107
	(etac (monofun_Ispair1 RS ch2ch_monofun) 1),
nipkow@243
   108
	(rtac trans 1),
nipkow@243
   109
	(rtac (thelub_sprod RS sym) 2),
nipkow@243
   110
	(rtac ch2ch_fun 2),
nipkow@243
   111
	(etac (monofun_Ispair1 RS ch2ch_monofun) 2),
nipkow@243
   112
	(res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
nipkow@243
   113
	(res_inst_tac 
nipkow@243
   114
		[("Q","lub(range(Y))=UU")] (excluded_middle RS disjE) 1),
nipkow@243
   115
	(etac sprod3_lemma1 1),
nipkow@243
   116
	(atac 1),
nipkow@243
   117
	(atac 1),
nipkow@243
   118
	(etac sprod3_lemma2 1),
nipkow@243
   119
	(atac 1),
nipkow@243
   120
	(atac 1),
nipkow@243
   121
	(etac sprod3_lemma3 1),
nipkow@243
   122
	(atac 1)
nipkow@243
   123
	]);
nipkow@243
   124
nipkow@243
   125
val sprod3_lemma4 = prove_goal Sprod3.thy 
nipkow@243
   126
"[| is_chain(Y); ~ x = UU; ~ lub(range(Y)) = UU |] ==>\
nipkow@243
   127
\         Ispair(x,lub(range(Y))) =\
nipkow@243
   128
\         Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\
nipkow@243
   129
\                lub(range(%i. Issnd(Ispair(x,Y(i))))))"
nipkow@243
   130
(fn prems =>
nipkow@243
   131
	[
nipkow@243
   132
	(cut_facts_tac prems 1),
nipkow@243
   133
	(res_inst_tac [("f1","Ispair")] (arg_cong RS cong) 1),
nipkow@243
   134
	(rtac sym 1),
nipkow@243
   135
	(rtac lub_chain_maxelem 1),
nipkow@243
   136
	(rtac (monofun_Isfst RS ch2ch_monofun) 1),
nipkow@243
   137
	(rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
nipkow@243
   138
	(atac 1),
nipkow@243
   139
	(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
nipkow@243
   140
	(rtac (notall2ex RS iffD1) 1),
nipkow@243
   141
	(res_inst_tac [("Q","lub(range(Y)) = UU")] contrapos 1),
nipkow@243
   142
	(atac 1),
nipkow@243
   143
	(rtac chain_UU_I_inverse 1),
nipkow@243
   144
	(atac 1),
nipkow@243
   145
	(rtac exI 1),
nipkow@243
   146
	(etac Isfst2 1),
nipkow@243
   147
	(rtac allI 1),
nipkow@243
   148
	(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
nipkow@243
   149
	(asm_simp_tac Sprod_ss 1),
nipkow@243
   150
	(rtac refl_less 1),
nipkow@243
   151
	(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
nipkow@243
   152
	(etac sym 1),
nipkow@243
   153
	(asm_simp_tac Sprod_ss  1),
nipkow@243
   154
	(rtac minimal 1),
nipkow@243
   155
	(rtac lub_equal 1),
nipkow@243
   156
	(atac 1),
nipkow@243
   157
	(rtac (monofun_Issnd RS ch2ch_monofun) 1),
nipkow@243
   158
	(rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
nipkow@243
   159
	(atac 1),
nipkow@243
   160
	(rtac allI 1),
nipkow@243
   161
	(asm_simp_tac Sprod_ss 1)
nipkow@243
   162
	]);
nipkow@243
   163
nipkow@243
   164
val sprod3_lemma5 = prove_goal Sprod3.thy 
nipkow@243
   165
"[| is_chain(Y); ~ x = UU; lub(range(Y)) = UU |] ==>\
nipkow@243
   166
\         Ispair(x,lub(range(Y))) =\
nipkow@243
   167
\         Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\
nipkow@243
   168
\                lub(range(%i. Issnd(Ispair(x,Y(i))))))"
nipkow@243
   169
 (fn prems =>
nipkow@243
   170
	[
nipkow@243
   171
	(cut_facts_tac prems 1),
nipkow@243
   172
	(res_inst_tac [("s","UU"),("t","lub(range(Y))")] ssubst 1),
nipkow@243
   173
	(atac 1),
nipkow@243
   174
	(rtac trans 1),
nipkow@243
   175
	(rtac strict_Ispair2 1),
nipkow@243
   176
	(rtac (strict_Ispair RS sym) 1),
nipkow@243
   177
	(rtac disjI2 1),
nipkow@243
   178
	(rtac chain_UU_I_inverse 1),
nipkow@243
   179
	(rtac allI 1),
nipkow@243
   180
	(asm_simp_tac Sprod_ss  1),
nipkow@243
   181
	(etac (chain_UU_I RS spec) 1),
nipkow@243
   182
	(atac 1)
nipkow@243
   183
	]);
nipkow@243
   184
nipkow@243
   185
val sprod3_lemma6 = prove_goal Sprod3.thy 
nipkow@243
   186
"[| is_chain(Y); x = UU |] ==>\
nipkow@243
   187
\         Ispair(x,lub(range(Y))) =\
nipkow@243
   188
\         Ispair(lub(range(%i. Isfst(Ispair(x,Y(i))))),\
nipkow@243
   189
\                lub(range(%i. Issnd(Ispair(x,Y(i))))))"
nipkow@243
   190
(fn prems =>
nipkow@243
   191
	[
nipkow@243
   192
	(cut_facts_tac prems 1),
nipkow@243
   193
	(res_inst_tac [("s","UU"),("t","x")] ssubst 1),
nipkow@243
   194
	(atac 1),
nipkow@243
   195
	(rtac trans 1),
nipkow@243
   196
	(rtac strict_Ispair1 1),
nipkow@243
   197
	(rtac (strict_Ispair RS sym) 1),
nipkow@243
   198
	(rtac disjI1 1),
nipkow@243
   199
	(rtac chain_UU_I_inverse 1),
nipkow@243
   200
	(rtac allI 1),
nipkow@243
   201
	(simp_tac Sprod_ss  1)
nipkow@243
   202
	]);
nipkow@243
   203
nipkow@243
   204
val contlub_Ispair2 = prove_goal Sprod3.thy "contlub(Ispair(x))"
nipkow@243
   205
(fn prems =>
nipkow@243
   206
	[
nipkow@243
   207
	(rtac contlubI 1),
nipkow@243
   208
	(strip_tac 1),
nipkow@243
   209
	(rtac trans 1),
nipkow@243
   210
	(rtac (thelub_sprod RS sym) 2),
nipkow@243
   211
	(etac (monofun_Ispair2 RS ch2ch_monofun) 2),
nipkow@243
   212
	(res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
nipkow@243
   213
	(res_inst_tac [("Q","lub(range(Y))=UU")] 
nipkow@243
   214
		(excluded_middle RS disjE) 1),
nipkow@243
   215
	(etac sprod3_lemma4 1),
nipkow@243
   216
	(atac 1),
nipkow@243
   217
	(atac 1),
nipkow@243
   218
	(etac sprod3_lemma5 1),
nipkow@243
   219
	(atac 1),
nipkow@243
   220
	(atac 1),
nipkow@243
   221
	(etac sprod3_lemma6 1),
nipkow@243
   222
	(atac 1)
nipkow@243
   223
	]);
nipkow@243
   224
nipkow@243
   225
nipkow@243
   226
val contX_Ispair1 = prove_goal Sprod3.thy "contX(Ispair)"
nipkow@243
   227
(fn prems =>
nipkow@243
   228
	[
nipkow@243
   229
	(rtac monocontlub2contX 1),
nipkow@243
   230
	(rtac monofun_Ispair1 1),
nipkow@243
   231
	(rtac contlub_Ispair1 1)
nipkow@243
   232
	]);
nipkow@243
   233
nipkow@243
   234
nipkow@243
   235
val contX_Ispair2 = prove_goal Sprod3.thy "contX(Ispair(x))"
nipkow@243
   236
(fn prems =>
nipkow@243
   237
	[
nipkow@243
   238
	(rtac monocontlub2contX 1),
nipkow@243
   239
	(rtac monofun_Ispair2 1),
nipkow@243
   240
	(rtac contlub_Ispair2 1)
nipkow@243
   241
	]);
nipkow@243
   242
nipkow@243
   243
val contlub_Isfst = prove_goal Sprod3.thy "contlub(Isfst)"
nipkow@243
   244
 (fn prems =>
nipkow@243
   245
	[
nipkow@243
   246
	(rtac contlubI 1),
nipkow@243
   247
	(strip_tac 1),
nipkow@243
   248
	(rtac (lub_sprod RS thelubI RS ssubst) 1),
nipkow@243
   249
	(atac 1),
nipkow@243
   250
	(res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]	
nipkow@243
   251
		(excluded_middle RS disjE) 1),
nipkow@243
   252
	(asm_simp_tac Sprod_ss  1),
nipkow@243
   253
	(res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")]
nipkow@243
   254
		ssubst 1),
nipkow@243
   255
	(atac 1),
nipkow@243
   256
	(rtac trans 1),
nipkow@243
   257
	(asm_simp_tac Sprod_ss  1),
nipkow@243
   258
	(rtac sym 1),
nipkow@243
   259
	(rtac chain_UU_I_inverse 1),
nipkow@243
   260
	(rtac allI 1),
nipkow@243
   261
	(rtac strict_Isfst 1),
nipkow@243
   262
	(rtac swap 1),
nipkow@243
   263
	(etac (defined_IsfstIssnd RS conjunct2) 2),
nipkow@243
   264
	(rtac notnotI 1),
nipkow@243
   265
	(rtac (chain_UU_I RS spec) 1),
nipkow@243
   266
	(rtac (monofun_Issnd RS ch2ch_monofun) 1),
nipkow@243
   267
	(atac 1),
nipkow@243
   268
	(atac 1)
nipkow@243
   269
	]);
nipkow@243
   270
nipkow@243
   271
nipkow@243
   272
val contlub_Issnd = prove_goal Sprod3.thy "contlub(Issnd)"
nipkow@243
   273
(fn prems =>
nipkow@243
   274
	[
nipkow@243
   275
	(rtac contlubI 1),
nipkow@243
   276
	(strip_tac 1),
nipkow@243
   277
	(rtac (lub_sprod RS thelubI RS ssubst) 1),
nipkow@243
   278
	(atac 1),
nipkow@243
   279
	(res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
nipkow@243
   280
	 (excluded_middle RS disjE) 1),
nipkow@243
   281
	(asm_simp_tac Sprod_ss  1),
nipkow@243
   282
	(res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")] 
nipkow@243
   283
		ssubst 1),
nipkow@243
   284
	(atac 1),
nipkow@243
   285
	(asm_simp_tac Sprod_ss  1),
nipkow@243
   286
	(rtac sym 1),
nipkow@243
   287
	(rtac chain_UU_I_inverse 1),
nipkow@243
   288
	(rtac allI 1),
nipkow@243
   289
	(rtac strict_Issnd 1),
nipkow@243
   290
	(rtac swap 1),
nipkow@243
   291
	(etac (defined_IsfstIssnd RS conjunct1) 2),
nipkow@243
   292
	(rtac notnotI 1),
nipkow@243
   293
	(rtac (chain_UU_I RS spec) 1),
nipkow@243
   294
	(rtac (monofun_Isfst RS ch2ch_monofun) 1),
nipkow@243
   295
	(atac 1),
nipkow@243
   296
	(atac 1)
nipkow@243
   297
	]);
nipkow@243
   298
nipkow@243
   299
nipkow@243
   300
val contX_Isfst = prove_goal Sprod3.thy "contX(Isfst)"
nipkow@243
   301
(fn prems =>
nipkow@243
   302
	[
nipkow@243
   303
	(rtac monocontlub2contX 1),
nipkow@243
   304
	(rtac monofun_Isfst 1),
nipkow@243
   305
	(rtac contlub_Isfst 1)
nipkow@243
   306
	]);
nipkow@243
   307
nipkow@243
   308
val contX_Issnd = prove_goal Sprod3.thy "contX(Issnd)"
nipkow@243
   309
(fn prems =>
nipkow@243
   310
	[
nipkow@243
   311
	(rtac monocontlub2contX 1),
nipkow@243
   312
	(rtac monofun_Issnd 1),
nipkow@243
   313
	(rtac contlub_Issnd 1)
nipkow@243
   314
	]);
nipkow@243
   315
nipkow@243
   316
(* 
nipkow@243
   317
 -------------------------------------------------------------------------- 
nipkow@243
   318
 more lemmas for Sprod3.thy 
nipkow@243
   319
 
nipkow@243
   320
 -------------------------------------------------------------------------- 
nipkow@243
   321
*)
nipkow@243
   322
nipkow@243
   323
val spair_eq = prove_goal Sprod3.thy "[|x1=x2;y1=y2|] ==> x1##y1 = x2##y2"
nipkow@243
   324
 (fn prems =>
nipkow@243
   325
	[
nipkow@243
   326
	(cut_facts_tac prems 1),
nipkow@243
   327
	(fast_tac HOL_cs 1)
nipkow@243
   328
	]);
nipkow@243
   329
nipkow@243
   330
(* ------------------------------------------------------------------------ *)
nipkow@243
   331
(* convert all lemmas to the continuous versions                            *)
nipkow@243
   332
(* ------------------------------------------------------------------------ *)
nipkow@243
   333
nipkow@243
   334
val beta_cfun_sprod = prove_goalw Sprod3.thy [spair_def]
nipkow@243
   335
	"(LAM x y.Ispair(x,y))[a][b] = Ispair(a,b)"
nipkow@243
   336
 (fn prems =>
nipkow@243
   337
	[
nipkow@243
   338
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   339
	(contX_tac 1),
nipkow@243
   340
	(rtac contX_Ispair2 1),
nipkow@243
   341
	(rtac contX2contX_CF1L 1),
nipkow@243
   342
	(rtac contX_Ispair1 1),
nipkow@243
   343
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   344
	(rtac contX_Ispair2 1),
nipkow@243
   345
	(rtac refl 1)
nipkow@243
   346
	]);
nipkow@243
   347
nipkow@243
   348
val inject_spair = prove_goalw Sprod3.thy [spair_def]
nipkow@243
   349
	"[|~aa=UU ; ~ba=UU ; (a##b)=(aa##ba) |] ==> a=aa & b=ba"
nipkow@243
   350
 (fn prems =>
nipkow@243
   351
	[
nipkow@243
   352
	(cut_facts_tac prems 1),
nipkow@243
   353
	(etac inject_Ispair 1),
nipkow@243
   354
	(atac 1),
nipkow@243
   355
	(etac box_equals 1),
nipkow@243
   356
	(rtac beta_cfun_sprod 1),
nipkow@243
   357
	(rtac beta_cfun_sprod 1)
nipkow@243
   358
	]);
nipkow@243
   359
nipkow@243
   360
val inst_sprod_pcpo2 = prove_goalw Sprod3.thy [spair_def] "UU = (UU##UU)"
nipkow@243
   361
 (fn prems =>
nipkow@243
   362
	[
nipkow@243
   363
	(rtac sym 1),
nipkow@243
   364
	(rtac trans 1),
nipkow@243
   365
	(rtac beta_cfun_sprod 1),
nipkow@243
   366
	(rtac sym 1),
nipkow@243
   367
	(rtac inst_sprod_pcpo 1)
nipkow@243
   368
	]);
nipkow@243
   369
nipkow@243
   370
val strict_spair = prove_goalw Sprod3.thy [spair_def] 
nipkow@243
   371
	"(a=UU | b=UU) ==> (a##b)=UU"
nipkow@243
   372
 (fn prems =>
nipkow@243
   373
	[
nipkow@243
   374
	(cut_facts_tac prems 1),
nipkow@243
   375
	(rtac trans 1),
nipkow@243
   376
	(rtac beta_cfun_sprod 1),
nipkow@243
   377
	(rtac trans 1),
nipkow@243
   378
	(rtac (inst_sprod_pcpo RS sym) 2),
nipkow@243
   379
	(etac strict_Ispair 1)
nipkow@243
   380
	]);
nipkow@243
   381
nipkow@243
   382
val strict_spair1 = prove_goalw Sprod3.thy [spair_def] "(UU##b) = UU"
nipkow@243
   383
 (fn prems =>
nipkow@243
   384
	[
nipkow@243
   385
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   386
	(rtac trans 1),
nipkow@243
   387
	(rtac (inst_sprod_pcpo RS sym) 2),
nipkow@243
   388
	(rtac strict_Ispair1 1)
nipkow@243
   389
	]);
nipkow@243
   390
nipkow@243
   391
val strict_spair2 = prove_goalw Sprod3.thy [spair_def] "(a##UU) = UU"
nipkow@243
   392
 (fn prems =>
nipkow@243
   393
	[
nipkow@243
   394
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   395
	(rtac trans 1),
nipkow@243
   396
	(rtac (inst_sprod_pcpo RS sym) 2),
nipkow@243
   397
	(rtac strict_Ispair2 1)
nipkow@243
   398
	]);
nipkow@243
   399
nipkow@243
   400
val strict_spair_rev = prove_goalw Sprod3.thy [spair_def]
nipkow@243
   401
	"~(x##y)=UU ==> ~x=UU & ~y=UU"
nipkow@243
   402
 (fn prems =>
nipkow@243
   403
	[
nipkow@243
   404
	(cut_facts_tac prems 1),
nipkow@243
   405
	(rtac strict_Ispair_rev 1),
nipkow@243
   406
	(rtac (beta_cfun_sprod RS subst) 1),
nipkow@243
   407
	(rtac (inst_sprod_pcpo RS subst) 1),
nipkow@243
   408
	(atac 1)
nipkow@243
   409
	]);
nipkow@243
   410
nipkow@243
   411
val defined_spair_rev = prove_goalw Sprod3.thy [spair_def]
nipkow@243
   412
 "(a##b) = UU ==> (a = UU | b = UU)"
nipkow@243
   413
 (fn prems =>
nipkow@243
   414
	[
nipkow@243
   415
	(cut_facts_tac prems 1),
nipkow@243
   416
	(rtac defined_Ispair_rev 1),
nipkow@243
   417
	(rtac (beta_cfun_sprod RS subst) 1),
nipkow@243
   418
	(rtac (inst_sprod_pcpo RS subst) 1),
nipkow@243
   419
	(atac 1)
nipkow@243
   420
	]);
nipkow@243
   421
nipkow@243
   422
val defined_spair = prove_goalw Sprod3.thy [spair_def]
nipkow@243
   423
	"[|~a=UU; ~b=UU|] ==> ~(a##b) = UU"
nipkow@243
   424
 (fn prems =>
nipkow@243
   425
	[
nipkow@243
   426
	(cut_facts_tac prems 1),
nipkow@243
   427
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   428
	(rtac (inst_sprod_pcpo RS ssubst) 1),
nipkow@243
   429
	(etac defined_Ispair 1),
nipkow@243
   430
	(atac 1)
nipkow@243
   431
	]);
nipkow@243
   432
nipkow@243
   433
val Exh_Sprod2 = prove_goalw Sprod3.thy [spair_def]
nipkow@243
   434
	"z=UU | (? a b. z=(a##b) & ~a=UU & ~b=UU)"
nipkow@243
   435
 (fn prems =>
nipkow@243
   436
	[
nipkow@243
   437
	(rtac (Exh_Sprod RS disjE) 1),
nipkow@243
   438
	(rtac disjI1 1),
nipkow@243
   439
	(rtac (inst_sprod_pcpo RS ssubst) 1),
nipkow@243
   440
	(atac 1),
nipkow@243
   441
	(rtac disjI2 1),
nipkow@243
   442
	(etac exE 1),
nipkow@243
   443
	(etac exE 1),
nipkow@243
   444
	(rtac exI 1),
nipkow@243
   445
	(rtac exI 1),
nipkow@243
   446
	(rtac conjI 1),
nipkow@243
   447
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   448
	(fast_tac HOL_cs 1),
nipkow@243
   449
	(fast_tac HOL_cs 1)
nipkow@243
   450
	]);
nipkow@243
   451
nipkow@243
   452
nipkow@243
   453
val sprodE =  prove_goalw Sprod3.thy [spair_def]
nipkow@243
   454
"[|p=UU ==> Q;!!x y. [|p=(x##y);~x=UU ; ~y=UU|] ==> Q|] ==> Q"
nipkow@243
   455
(fn prems =>
nipkow@243
   456
	[
nipkow@243
   457
	(rtac IsprodE 1),
nipkow@243
   458
	(resolve_tac prems 1),
nipkow@243
   459
	(rtac (inst_sprod_pcpo RS ssubst) 1),
nipkow@243
   460
	(atac 1),
nipkow@243
   461
	(resolve_tac prems 1),
nipkow@243
   462
	(atac 2),
nipkow@243
   463
	(atac 2),
nipkow@243
   464
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   465
	(atac 1)
nipkow@243
   466
	]);
nipkow@243
   467
nipkow@243
   468
nipkow@243
   469
val strict_sfst = prove_goalw Sprod3.thy [sfst_def] 
nipkow@243
   470
	"p=UU==>sfst[p]=UU"
nipkow@243
   471
 (fn prems =>
nipkow@243
   472
	[
nipkow@243
   473
	(cut_facts_tac prems 1),
nipkow@243
   474
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   475
	(rtac contX_Isfst 1),
nipkow@243
   476
	(rtac strict_Isfst 1),
nipkow@243
   477
	(rtac (inst_sprod_pcpo RS subst) 1),
nipkow@243
   478
	(atac 1)
nipkow@243
   479
	]);
nipkow@243
   480
nipkow@243
   481
val strict_sfst1 = prove_goalw Sprod3.thy [sfst_def,spair_def] 
nipkow@243
   482
	"sfst[UU##y] = UU"
nipkow@243
   483
 (fn prems =>
nipkow@243
   484
	[
nipkow@243
   485
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   486
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   487
	(rtac contX_Isfst 1),
nipkow@243
   488
	(rtac strict_Isfst1 1)
nipkow@243
   489
	]);
nipkow@243
   490
 
nipkow@243
   491
val strict_sfst2 = prove_goalw Sprod3.thy [sfst_def,spair_def] 
nipkow@243
   492
	"sfst[x##UU] = UU"
nipkow@243
   493
 (fn prems =>
nipkow@243
   494
	[
nipkow@243
   495
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   496
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   497
	(rtac contX_Isfst 1),
nipkow@243
   498
	(rtac strict_Isfst2 1)
nipkow@243
   499
	]);
nipkow@243
   500
nipkow@243
   501
val strict_ssnd = prove_goalw Sprod3.thy [ssnd_def] 
nipkow@243
   502
	"p=UU==>ssnd[p]=UU"
nipkow@243
   503
 (fn prems =>
nipkow@243
   504
	[
nipkow@243
   505
	(cut_facts_tac prems 1),
nipkow@243
   506
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   507
	(rtac contX_Issnd 1),
nipkow@243
   508
	(rtac strict_Issnd 1),
nipkow@243
   509
	(rtac (inst_sprod_pcpo RS subst) 1),
nipkow@243
   510
	(atac 1)
nipkow@243
   511
	]);
nipkow@243
   512
nipkow@243
   513
val strict_ssnd1 = prove_goalw Sprod3.thy [ssnd_def,spair_def] 
nipkow@243
   514
	"ssnd[UU##y] = UU"
nipkow@243
   515
 (fn prems =>
nipkow@243
   516
	[
nipkow@243
   517
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   518
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   519
	(rtac contX_Issnd 1),
nipkow@243
   520
	(rtac strict_Issnd1 1)
nipkow@243
   521
	]);
nipkow@243
   522
nipkow@243
   523
val strict_ssnd2 = prove_goalw Sprod3.thy [ssnd_def,spair_def] 
nipkow@243
   524
	"ssnd[x##UU] = UU"
nipkow@243
   525
 (fn prems =>
nipkow@243
   526
	[
nipkow@243
   527
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   528
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   529
	(rtac contX_Issnd 1),
nipkow@243
   530
	(rtac strict_Issnd2 1)
nipkow@243
   531
	]);
nipkow@243
   532
nipkow@243
   533
val sfst2 = prove_goalw Sprod3.thy [sfst_def,spair_def] 
nipkow@243
   534
	"~y=UU ==>sfst[x##y]=x"
nipkow@243
   535
 (fn prems =>
nipkow@243
   536
	[
nipkow@243
   537
	(cut_facts_tac prems 1),
nipkow@243
   538
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   539
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   540
	(rtac contX_Isfst 1),
nipkow@243
   541
	(etac Isfst2 1)
nipkow@243
   542
	]);
nipkow@243
   543
nipkow@243
   544
val ssnd2 = prove_goalw Sprod3.thy [ssnd_def,spair_def] 
nipkow@243
   545
	"~x=UU ==>ssnd[x##y]=y"
nipkow@243
   546
 (fn prems =>
nipkow@243
   547
	[
nipkow@243
   548
	(cut_facts_tac prems 1),
nipkow@243
   549
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   550
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   551
	(rtac contX_Issnd 1),
nipkow@243
   552
	(etac Issnd2 1)
nipkow@243
   553
	]);
nipkow@243
   554
nipkow@243
   555
nipkow@243
   556
val defined_sfstssnd = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
nipkow@243
   557
	"~p=UU ==> ~sfst[p]=UU & ~ssnd[p]=UU"
nipkow@243
   558
 (fn prems =>
nipkow@243
   559
	[
nipkow@243
   560
	(cut_facts_tac prems 1),
nipkow@243
   561
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   562
	(rtac contX_Issnd 1),
nipkow@243
   563
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   564
	(rtac contX_Isfst 1),
nipkow@243
   565
	(rtac defined_IsfstIssnd 1),
nipkow@243
   566
	(rtac (inst_sprod_pcpo RS subst) 1),
nipkow@243
   567
	(atac 1)
nipkow@243
   568
	]);
nipkow@243
   569
 
nipkow@243
   570
nipkow@243
   571
val surjective_pairing_Sprod2 = prove_goalw Sprod3.thy 
nipkow@243
   572
	[sfst_def,ssnd_def,spair_def] "(sfst[p] ## ssnd[p]) = p"
nipkow@243
   573
 (fn prems =>
nipkow@243
   574
	[
nipkow@243
   575
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   576
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   577
	(rtac contX_Issnd 1),
nipkow@243
   578
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   579
	(rtac contX_Isfst 1),
nipkow@243
   580
	(rtac (surjective_pairing_Sprod RS sym) 1)
nipkow@243
   581
	]);
nipkow@243
   582
nipkow@243
   583
nipkow@243
   584
val less_sprod5b = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
nipkow@243
   585
 "~p1=UU ==> (p1<<p2) = (sfst[p1]<<sfst[p2] & ssnd[p1]<<ssnd[p2])"
nipkow@243
   586
 (fn prems =>
nipkow@243
   587
	[
nipkow@243
   588
	(cut_facts_tac prems 1),
nipkow@243
   589
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   590
	(rtac contX_Issnd 1),
nipkow@243
   591
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   592
	(rtac contX_Issnd 1),
nipkow@243
   593
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   594
	(rtac contX_Isfst 1),
nipkow@243
   595
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   596
	(rtac contX_Isfst 1),
nipkow@243
   597
	(rtac less_sprod3b 1),
nipkow@243
   598
	(rtac (inst_sprod_pcpo RS subst) 1),
nipkow@243
   599
	(atac 1)
nipkow@243
   600
	]);
nipkow@243
   601
nipkow@243
   602
 
nipkow@243
   603
val less_sprod5c = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
nipkow@243
   604
 "[|xa##ya<<x##y;~xa=UU;~ya=UU;~x=UU;~y=UU|] ==>xa<<x & ya << y"
nipkow@243
   605
 (fn prems =>
nipkow@243
   606
	[
nipkow@243
   607
	(cut_facts_tac prems 1),
nipkow@243
   608
	(rtac less_sprod4c 1),
nipkow@243
   609
	(REPEAT (atac 2)),
nipkow@243
   610
	(rtac (beta_cfun_sprod RS subst) 1),
nipkow@243
   611
	(rtac (beta_cfun_sprod RS subst) 1),
nipkow@243
   612
	(atac 1)
nipkow@243
   613
	]);
nipkow@243
   614
nipkow@243
   615
val lub_sprod2 = prove_goalw Sprod3.thy [sfst_def,ssnd_def,spair_def]
nipkow@243
   616
"[|is_chain(S)|] ==> range(S) <<| \
nipkow@243
   617
\ (lub(range(%i.sfst[S(i)])) ## lub(range(%i.ssnd[S(i)])))"
nipkow@243
   618
 (fn prems =>
nipkow@243
   619
	[
nipkow@243
   620
	(cut_facts_tac prems 1),
nipkow@243
   621
	(rtac (beta_cfun_sprod RS ssubst) 1),
nipkow@243
   622
	(rtac (beta_cfun RS ext RS ssubst) 1),
nipkow@243
   623
	(rtac contX_Issnd 1),
nipkow@243
   624
	(rtac (beta_cfun RS ext RS ssubst) 1),
nipkow@243
   625
	(rtac contX_Isfst 1),
nipkow@243
   626
	(rtac lub_sprod 1),
nipkow@243
   627
	(resolve_tac prems 1)
nipkow@243
   628
	]);
nipkow@243
   629
nipkow@243
   630
nipkow@243
   631
val thelub_sprod2 = (lub_sprod2 RS thelubI);
nipkow@243
   632
(* is_chain(?S1) ==> lub(range(?S1)) =                                    *) 
nipkow@243
   633
(*     (lub(range(%i. sfst[?S1(i)]))## lub(range(%i. ssnd[?S1(i)])))        *)
nipkow@243
   634
nipkow@243
   635
nipkow@243
   636
nipkow@243
   637
val ssplit1 = prove_goalw Sprod3.thy [ssplit_def]
nipkow@243
   638
	"ssplit[f][UU]=UU"
nipkow@243
   639
 (fn prems =>
nipkow@243
   640
	[
nipkow@243
   641
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   642
	(contX_tacR 1),
nipkow@243
   643
	(rtac (strictify1 RS ssubst) 1),
nipkow@243
   644
	(rtac refl 1)
nipkow@243
   645
	]);
nipkow@243
   646
nipkow@243
   647
val ssplit2 = prove_goalw Sprod3.thy [ssplit_def]
nipkow@243
   648
	"[|~x=UU;~y=UU|] ==> ssplit[f][x##y]=f[x][y]"
nipkow@243
   649
 (fn prems =>
nipkow@243
   650
	[
nipkow@243
   651
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   652
	(contX_tacR 1),
nipkow@243
   653
	(rtac (strictify2 RS ssubst) 1),
nipkow@243
   654
	(rtac defined_spair 1),
nipkow@243
   655
	(resolve_tac prems 1),
nipkow@243
   656
	(resolve_tac prems 1),
nipkow@243
   657
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   658
	(contX_tacR 1),
nipkow@243
   659
	(rtac (sfst2 RS ssubst) 1),
nipkow@243
   660
	(resolve_tac prems 1),
nipkow@243
   661
	(rtac (ssnd2 RS ssubst) 1),
nipkow@243
   662
	(resolve_tac prems 1),
nipkow@243
   663
	(rtac refl 1)
nipkow@243
   664
	]);
nipkow@243
   665
nipkow@243
   666
nipkow@243
   667
val ssplit3 = prove_goalw Sprod3.thy [ssplit_def]
nipkow@243
   668
  "ssplit[spair][z]=z"
nipkow@243
   669
 (fn prems =>
nipkow@243
   670
	[
nipkow@243
   671
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   672
	(contX_tacR 1),
nipkow@243
   673
	(res_inst_tac [("Q","z=UU")] classical2 1),
nipkow@243
   674
	(hyp_subst_tac 1),
nipkow@243
   675
	(rtac strictify1 1),
nipkow@243
   676
	(rtac trans 1),
nipkow@243
   677
	(rtac strictify2 1),
nipkow@243
   678
	(atac 1),
nipkow@243
   679
	(rtac (beta_cfun RS ssubst) 1),
nipkow@243
   680
	(contX_tacR 1),
nipkow@243
   681
	(rtac surjective_pairing_Sprod2 1)
nipkow@243
   682
	]);
nipkow@243
   683
nipkow@243
   684
nipkow@243
   685
(* ------------------------------------------------------------------------ *)
nipkow@243
   686
(* install simplifier for Sprod                                             *)
nipkow@243
   687
(* ------------------------------------------------------------------------ *)
nipkow@243
   688
nipkow@243
   689
val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
nipkow@243
   690
		strict_ssnd1,strict_ssnd2,sfst2,ssnd2,
nipkow@243
   691
		ssplit1,ssplit2];
nipkow@243
   692
nipkow@243
   693
val Sprod_ss = Cfun_ss addsimps Sprod_rews;
nipkow@243
   694
nipkow@243
   695