src/HOLCF/Sprod.thy
author huffman
Fri Mar 04 23:23:47 2005 +0100 (2005-03-04)
changeset 15577 e16da3068ad6
parent 15576 efb95d0d01f7
child 15591 50c3384ca6c4
permissions -rw-r--r--
fix headers
huffman@15576
     1
(*  Title:      HOLCF/Sprod0.thy
huffman@15576
     2
    ID:         $Id$
huffman@15576
     3
    Author:     Franz Regensburger
huffman@15576
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
huffman@15576
     5
huffman@15576
     6
Strict product with typedef.
huffman@15576
     7
*)
huffman@15576
     8
huffman@15576
     9
header {* The type of strict products *}
huffman@15576
    10
huffman@15577
    11
theory Sprod
huffman@15577
    12
imports Cfun
huffman@15577
    13
begin
huffman@15576
    14
huffman@15576
    15
constdefs
huffman@15576
    16
  Spair_Rep     :: "['a,'b] => ['a,'b] => bool"
huffman@15576
    17
 "Spair_Rep == (%a b. %x y.(~a=UU & ~b=UU --> x=a  & y=b ))"
huffman@15576
    18
huffman@15576
    19
typedef (Sprod)  ('a, 'b) "**" (infixr 20) = "{f. ? a b. f = Spair_Rep (a::'a) (b::'b)}"
huffman@15576
    20
by auto
huffman@15576
    21
huffman@15576
    22
syntax (xsymbols)
huffman@15576
    23
  "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
huffman@15576
    24
syntax (HTML output)
huffman@15576
    25
  "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
huffman@15576
    26
huffman@15576
    27
subsection {* @{term Ispair}, @{term Isfst}, and @{term Issnd} *}
huffman@15576
    28
huffman@15576
    29
consts
huffman@15576
    30
  Ispair        :: "['a,'b] => ('a ** 'b)"
huffman@15576
    31
  Isfst         :: "('a ** 'b) => 'a"
huffman@15576
    32
  Issnd         :: "('a ** 'b) => 'b"  
huffman@15576
    33
huffman@15576
    34
defs
huffman@15576
    35
   (*defining the abstract constants*)
huffman@15576
    36
huffman@15576
    37
  Ispair_def:    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
huffman@15576
    38
huffman@15576
    39
  Isfst_def:     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
huffman@15576
    40
                &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
huffman@15576
    41
huffman@15576
    42
  Issnd_def:     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
huffman@15576
    43
                &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
huffman@15576
    44
huffman@15576
    45
(* ------------------------------------------------------------------------ *)
huffman@15576
    46
(* A non-emptyness result for Sprod                                         *)
huffman@15576
    47
(* ------------------------------------------------------------------------ *)
huffman@15576
    48
huffman@15576
    49
lemma SprodI: "(Spair_Rep a b):Sprod"
huffman@15576
    50
apply (unfold Sprod_def)
huffman@15576
    51
apply (rule CollectI, rule exI, rule exI, rule refl)
huffman@15576
    52
done
huffman@15576
    53
huffman@15576
    54
lemma inj_on_Abs_Sprod: "inj_on Abs_Sprod Sprod"
huffman@15576
    55
apply (rule inj_on_inverseI)
huffman@15576
    56
apply (erule Abs_Sprod_inverse)
huffman@15576
    57
done
huffman@15576
    58
huffman@15576
    59
(* ------------------------------------------------------------------------ *)
huffman@15576
    60
(* Strictness and definedness of Spair_Rep                                  *)
huffman@15576
    61
(* ------------------------------------------------------------------------ *)
huffman@15576
    62
huffman@15576
    63
lemma strict_Spair_Rep: 
huffman@15576
    64
 "(a=UU | b=UU) ==> (Spair_Rep a b) = (Spair_Rep UU UU)"
huffman@15576
    65
apply (unfold Spair_Rep_def)
huffman@15576
    66
apply (rule ext)
huffman@15576
    67
apply (rule ext)
huffman@15576
    68
apply (rule iffI)
huffman@15576
    69
apply fast
huffman@15576
    70
apply fast
huffman@15576
    71
done
huffman@15576
    72
huffman@15576
    73
lemma defined_Spair_Rep_rev: 
huffman@15576
    74
 "(Spair_Rep a b) = (Spair_Rep UU UU) ==> (a=UU | b=UU)"
huffman@15576
    75
apply (unfold Spair_Rep_def)
huffman@15576
    76
apply (case_tac "a=UU|b=UU")
huffman@15576
    77
apply assumption
huffman@15576
    78
apply (fast dest: fun_cong)
huffman@15576
    79
done
huffman@15576
    80
huffman@15576
    81
(* ------------------------------------------------------------------------ *)
huffman@15576
    82
(* injectivity of Spair_Rep and Ispair                                      *)
huffman@15576
    83
(* ------------------------------------------------------------------------ *)
huffman@15576
    84
huffman@15576
    85
lemma inject_Spair_Rep: 
huffman@15576
    86
"[|~aa=UU ; ~ba=UU ; Spair_Rep a b = Spair_Rep aa ba |] ==> a=aa & b=ba"
huffman@15576
    87
huffman@15576
    88
apply (unfold Spair_Rep_def)
huffman@15576
    89
apply (drule fun_cong)
huffman@15576
    90
apply (drule fun_cong)
huffman@15576
    91
apply (erule iffD1 [THEN mp])
huffman@15576
    92
apply auto
huffman@15576
    93
done
huffman@15576
    94
huffman@15576
    95
lemma inject_Ispair: 
huffman@15576
    96
        "[|~aa=UU ; ~ba=UU ; Ispair a b = Ispair aa ba |] ==> a=aa & b=ba"
huffman@15576
    97
apply (unfold Ispair_def)
huffman@15576
    98
apply (erule inject_Spair_Rep)
huffman@15576
    99
apply assumption
huffman@15576
   100
apply (erule inj_on_Abs_Sprod [THEN inj_onD])
huffman@15576
   101
apply (rule SprodI)
huffman@15576
   102
apply (rule SprodI)
huffman@15576
   103
done
huffman@15576
   104
huffman@15576
   105
(* ------------------------------------------------------------------------ *)
huffman@15576
   106
(* strictness and definedness of Ispair                                     *)
huffman@15576
   107
(* ------------------------------------------------------------------------ *)
huffman@15576
   108
huffman@15576
   109
lemma strict_Ispair: 
huffman@15576
   110
 "(a=UU | b=UU) ==> Ispair a b = Ispair UU UU"
huffman@15576
   111
apply (unfold Ispair_def)
huffman@15576
   112
apply (erule strict_Spair_Rep [THEN arg_cong])
huffman@15576
   113
done
huffman@15576
   114
huffman@15576
   115
lemma strict_Ispair1: 
huffman@15576
   116
        "Ispair UU b  = Ispair UU UU"
huffman@15576
   117
apply (unfold Ispair_def)
huffman@15576
   118
apply (rule strict_Spair_Rep [THEN arg_cong])
huffman@15576
   119
apply (rule disjI1)
huffman@15576
   120
apply (rule refl)
huffman@15576
   121
done
huffman@15576
   122
huffman@15576
   123
lemma strict_Ispair2: 
huffman@15576
   124
        "Ispair a UU = Ispair UU UU"
huffman@15576
   125
apply (unfold Ispair_def)
huffman@15576
   126
apply (rule strict_Spair_Rep [THEN arg_cong])
huffman@15576
   127
apply (rule disjI2)
huffman@15576
   128
apply (rule refl)
huffman@15576
   129
done
huffman@15576
   130
huffman@15576
   131
lemma strict_Ispair_rev: "~Ispair x y = Ispair UU UU ==> ~x=UU & ~y=UU"
huffman@15576
   132
apply (rule de_Morgan_disj [THEN subst])
huffman@15576
   133
apply (erule contrapos_nn)
huffman@15576
   134
apply (erule strict_Ispair)
huffman@15576
   135
done
huffman@15576
   136
huffman@15576
   137
lemma defined_Ispair_rev: 
huffman@15576
   138
        "Ispair a b  = Ispair UU UU ==> (a = UU | b = UU)"
huffman@15576
   139
apply (unfold Ispair_def)
huffman@15576
   140
apply (rule defined_Spair_Rep_rev)
huffman@15576
   141
apply (rule inj_on_Abs_Sprod [THEN inj_onD])
huffman@15576
   142
apply assumption
huffman@15576
   143
apply (rule SprodI)
huffman@15576
   144
apply (rule SprodI)
huffman@15576
   145
done
huffman@15576
   146
huffman@15576
   147
lemma defined_Ispair: "[|a~=UU; b~=UU|] ==> (Ispair a b) ~= (Ispair UU UU)"
huffman@15576
   148
apply (rule contrapos_nn)
huffman@15576
   149
apply (erule_tac [2] defined_Ispair_rev)
huffman@15576
   150
apply (rule de_Morgan_disj [THEN iffD2])
huffman@15576
   151
apply (erule conjI)
huffman@15576
   152
apply assumption
huffman@15576
   153
done
huffman@15576
   154
huffman@15576
   155
huffman@15576
   156
(* ------------------------------------------------------------------------ *)
huffman@15576
   157
(* Exhaustion of the strict product **                                      *)
huffman@15576
   158
(* ------------------------------------------------------------------------ *)
huffman@15576
   159
huffman@15576
   160
lemma Exh_Sprod:
huffman@15576
   161
        "z=Ispair UU UU | (? a b. z=Ispair a b & a~=UU & b~=UU)"
huffman@15576
   162
apply (unfold Ispair_def)
huffman@15576
   163
apply (rule Rep_Sprod[unfolded Sprod_def, THEN CollectE])
huffman@15576
   164
apply (erule exE)
huffman@15576
   165
apply (erule exE)
huffman@15576
   166
apply (rule excluded_middle [THEN disjE])
huffman@15576
   167
apply (rule disjI2)
huffman@15576
   168
apply (rule exI)
huffman@15576
   169
apply (rule exI)
huffman@15576
   170
apply (rule conjI)
huffman@15576
   171
apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
huffman@15576
   172
apply (erule arg_cong)
huffman@15576
   173
apply (rule de_Morgan_disj [THEN subst])
huffman@15576
   174
apply assumption
huffman@15576
   175
apply (rule disjI1)
huffman@15576
   176
apply (rule Rep_Sprod_inverse [symmetric, THEN trans])
huffman@15576
   177
apply (rule_tac f = "Abs_Sprod" in arg_cong)
huffman@15576
   178
apply (erule trans)
huffman@15576
   179
apply (erule strict_Spair_Rep)
huffman@15576
   180
done
huffman@15576
   181
huffman@15576
   182
(* ------------------------------------------------------------------------ *)
huffman@15576
   183
(* general elimination rule for strict product                              *)
huffman@15576
   184
(* ------------------------------------------------------------------------ *)
huffman@15576
   185
huffman@15576
   186
lemma IsprodE:
huffman@15576
   187
assumes prem1: "p=Ispair UU UU ==> Q"
huffman@15576
   188
assumes prem2: "!!x y. [|p=Ispair x y; x~=UU ; y~=UU|] ==> Q"
huffman@15576
   189
shows "Q"
huffman@15576
   190
apply (rule Exh_Sprod [THEN disjE])
huffman@15576
   191
apply (erule prem1)
huffman@15576
   192
apply (erule exE)
huffman@15576
   193
apply (erule exE)
huffman@15576
   194
apply (erule conjE)
huffman@15576
   195
apply (erule conjE)
huffman@15576
   196
apply (erule prem2)
huffman@15576
   197
apply assumption
huffman@15576
   198
apply assumption
huffman@15576
   199
done
huffman@15576
   200
huffman@15576
   201
(* ------------------------------------------------------------------------ *)
huffman@15576
   202
(* some results about the selectors Isfst, Issnd                            *)
huffman@15576
   203
(* ------------------------------------------------------------------------ *)
huffman@15576
   204
huffman@15576
   205
lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
huffman@15576
   206
apply (unfold Isfst_def)
huffman@15576
   207
apply (rule some_equality)
huffman@15576
   208
apply (rule conjI)
huffman@15576
   209
apply fast
huffman@15576
   210
apply (intro strip)
huffman@15576
   211
apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
huffman@15576
   212
apply (rule not_sym)
huffman@15576
   213
apply (rule defined_Ispair)
huffman@15576
   214
apply (fast+)
huffman@15576
   215
done
huffman@15576
   216
huffman@15576
   217
lemma strict_Isfst1 [simp]: "Isfst(Ispair UU y) = UU"
huffman@15576
   218
apply (subst strict_Ispair1)
huffman@15576
   219
apply (rule strict_Isfst)
huffman@15576
   220
apply (rule refl)
huffman@15576
   221
done
huffman@15576
   222
huffman@15576
   223
lemma strict_Isfst2 [simp]: "Isfst(Ispair x UU) = UU"
huffman@15576
   224
apply (subst strict_Ispair2)
huffman@15576
   225
apply (rule strict_Isfst)
huffman@15576
   226
apply (rule refl)
huffman@15576
   227
done
huffman@15576
   228
huffman@15576
   229
lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU"
huffman@15576
   230
apply (unfold Issnd_def)
huffman@15576
   231
apply (rule some_equality)
huffman@15576
   232
apply (rule conjI)
huffman@15576
   233
apply fast
huffman@15576
   234
apply (intro strip)
huffman@15576
   235
apply (rule_tac P = "Ispair UU UU = Ispair a b" in notE)
huffman@15576
   236
apply (rule not_sym)
huffman@15576
   237
apply (rule defined_Ispair)
huffman@15576
   238
apply (fast+)
huffman@15576
   239
done
huffman@15576
   240
huffman@15576
   241
lemma strict_Issnd1 [simp]: "Issnd(Ispair UU y) = UU"
huffman@15576
   242
apply (subst strict_Ispair1)
huffman@15576
   243
apply (rule strict_Issnd)
huffman@15576
   244
apply (rule refl)
huffman@15576
   245
done
huffman@15576
   246
huffman@15576
   247
lemma strict_Issnd2 [simp]: "Issnd(Ispair x UU) = UU"
huffman@15576
   248
apply (subst strict_Ispair2)
huffman@15576
   249
apply (rule strict_Issnd)
huffman@15576
   250
apply (rule refl)
huffman@15576
   251
done
huffman@15576
   252
huffman@15576
   253
lemma Isfst: "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
huffman@15576
   254
apply (unfold Isfst_def)
huffman@15576
   255
apply (rule some_equality)
huffman@15576
   256
apply (rule conjI)
huffman@15576
   257
apply (intro strip)
huffman@15576
   258
apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
huffman@15576
   259
apply (erule defined_Ispair)
huffman@15576
   260
apply assumption
huffman@15576
   261
apply assumption
huffman@15576
   262
apply (intro strip)
huffman@15576
   263
apply (rule inject_Ispair [THEN conjunct1])
huffman@15576
   264
prefer 3 apply fast
huffman@15576
   265
apply (fast+)
huffman@15576
   266
done
huffman@15576
   267
huffman@15576
   268
lemma Issnd: "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
huffman@15576
   269
apply (unfold Issnd_def)
huffman@15576
   270
apply (rule some_equality)
huffman@15576
   271
apply (rule conjI)
huffman@15576
   272
apply (intro strip)
huffman@15576
   273
apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
huffman@15576
   274
apply (erule defined_Ispair)
huffman@15576
   275
apply assumption
huffman@15576
   276
apply assumption
huffman@15576
   277
apply (intro strip)
huffman@15576
   278
apply (rule inject_Ispair [THEN conjunct2])
huffman@15576
   279
prefer 3 apply fast
huffman@15576
   280
apply (fast+)
huffman@15576
   281
done
huffman@15576
   282
huffman@15576
   283
lemma Isfst2: "y~=UU ==>Isfst(Ispair x y)=x"
huffman@15576
   284
apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
huffman@15576
   285
apply (erule Isfst)
huffman@15576
   286
apply assumption
huffman@15576
   287
apply (erule ssubst)
huffman@15576
   288
apply (rule strict_Isfst1)
huffman@15576
   289
done
huffman@15576
   290
huffman@15576
   291
lemma Issnd2: "~x=UU ==>Issnd(Ispair x y)=y"
huffman@15576
   292
apply (rule_tac Q = "y=UU" in excluded_middle [THEN disjE])
huffman@15576
   293
apply (erule Issnd)
huffman@15576
   294
apply assumption
huffman@15576
   295
apply (erule ssubst)
huffman@15576
   296
apply (rule strict_Issnd2)
huffman@15576
   297
done
huffman@15576
   298
huffman@15576
   299
huffman@15576
   300
(* ------------------------------------------------------------------------ *)
huffman@15576
   301
(* instantiate the simplifier                                               *)
huffman@15576
   302
(* ------------------------------------------------------------------------ *)
huffman@15576
   303
huffman@15576
   304
lemmas Sprod0_ss = strict_Isfst1 strict_Isfst2 strict_Issnd1 strict_Issnd2
huffman@15576
   305
                 Isfst2 Issnd2
huffman@15576
   306
huffman@15576
   307
declare Isfst2 [simp] Issnd2 [simp]
huffman@15576
   308
huffman@15576
   309
lemma defined_IsfstIssnd: "p~=Ispair UU UU ==> Isfst p ~= UU & Issnd p ~= UU"
huffman@15576
   310
apply (rule_tac p = "p" in IsprodE)
huffman@15576
   311
apply simp
huffman@15576
   312
apply (erule ssubst)
huffman@15576
   313
apply (rule conjI)
huffman@15576
   314
apply (simp add: Sprod0_ss)
huffman@15576
   315
apply (simp add: Sprod0_ss)
huffman@15576
   316
done
huffman@15576
   317
huffman@15576
   318
huffman@15576
   319
(* ------------------------------------------------------------------------ *)
huffman@15576
   320
(* Surjective pairing: equivalent to Exh_Sprod                              *)
huffman@15576
   321
(* ------------------------------------------------------------------------ *)
huffman@15576
   322
huffman@15576
   323
lemma surjective_pairing_Sprod: "z = Ispair(Isfst z)(Issnd z)"
huffman@15576
   324
apply (rule_tac z1 = "z" in Exh_Sprod [THEN disjE])
huffman@15576
   325
apply (simp add: Sprod0_ss)
huffman@15576
   326
apply (erule exE)
huffman@15576
   327
apply (erule exE)
huffman@15576
   328
apply (simp add: Sprod0_ss)
huffman@15576
   329
done
huffman@15576
   330
huffman@15576
   331
lemma Sel_injective_Sprod: "[|Isfst x = Isfst y; Issnd x = Issnd y|] ==> x = y"
huffman@15576
   332
apply (subgoal_tac "Ispair (Isfst x) (Issnd x) =Ispair (Isfst y) (Issnd y) ")
huffman@15576
   333
apply (simp (no_asm_use) add: surjective_pairing_Sprod[symmetric])
huffman@15576
   334
apply simp
huffman@15576
   335
done
huffman@15576
   336
huffman@15576
   337
subsection {* The strict product is a partial order *}
huffman@15576
   338
huffman@15576
   339
instance "**"::(sq_ord,sq_ord)sq_ord ..
huffman@15576
   340
huffman@15576
   341
defs (overloaded)
huffman@15576
   342
  less_sprod_def: "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
huffman@15576
   343
huffman@15576
   344
(* ------------------------------------------------------------------------ *)
huffman@15576
   345
(* less_sprod is a partial order on Sprod                                   *)
huffman@15576
   346
(* ------------------------------------------------------------------------ *)
huffman@15576
   347
huffman@15576
   348
lemma refl_less_sprod: "(p::'a ** 'b) << p"
huffman@15576
   349
apply (unfold less_sprod_def)
huffman@15576
   350
apply (fast intro: refl_less)
huffman@15576
   351
done
huffman@15576
   352
huffman@15576
   353
lemma antisym_less_sprod: 
huffman@15576
   354
        "[|(p1::'a ** 'b) << p2;p2 << p1|] ==> p1=p2"
huffman@15576
   355
apply (unfold less_sprod_def)
huffman@15576
   356
apply (rule Sel_injective_Sprod)
huffman@15576
   357
apply (fast intro: antisym_less)
huffman@15576
   358
apply (fast intro: antisym_less)
huffman@15576
   359
done
huffman@15576
   360
huffman@15576
   361
lemma trans_less_sprod: 
huffman@15576
   362
        "[|(p1::'a**'b) << p2;p2 << p3|] ==> p1 << p3"
huffman@15576
   363
apply (unfold less_sprod_def)
huffman@15576
   364
apply (blast intro: trans_less)
huffman@15576
   365
done
huffman@15576
   366
huffman@15576
   367
instance "**"::(pcpo,pcpo)po
huffman@15576
   368
by intro_classes
huffman@15576
   369
  (assumption | rule refl_less_sprod antisym_less_sprod trans_less_sprod)+
huffman@15576
   370
huffman@15576
   371
(* for compatibility with old HOLCF-Version *)
huffman@15576
   372
lemma inst_sprod_po: "(op <<)=(%x y. Isfst x<<Isfst y&Issnd x<<Issnd y)"
huffman@15576
   373
apply (fold less_sprod_def)
huffman@15576
   374
apply (rule refl)
huffman@15576
   375
done
huffman@15576
   376
huffman@15576
   377
subsection {* The strict product is pointed *}
huffman@15576
   378
(* ------------------------------------------------------------------------ *)
huffman@15576
   379
(* type sprod is pointed                                                    *)
huffman@15576
   380
(* ------------------------------------------------------------------------ *)
huffman@15576
   381
(*
huffman@15576
   382
lemma minimal_sprod: "Ispair UU UU << p"
huffman@15576
   383
apply (simp add: inst_sprod_po minimal)
huffman@15576
   384
done
huffman@15576
   385
huffman@15576
   386
lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
huffman@15576
   387
huffman@15576
   388
lemma least_sprod: "? x::'a**'b.!y. x<<y"
huffman@15576
   389
apply (rule_tac x = "Ispair UU UU" in exI)
huffman@15576
   390
apply (rule minimal_sprod [THEN allI])
huffman@15576
   391
done
huffman@15576
   392
*)
huffman@15576
   393
(* ------------------------------------------------------------------------ *)
huffman@15576
   394
(* Ispair is monotone in both arguments                                     *)
huffman@15576
   395
(* ------------------------------------------------------------------------ *)
huffman@15576
   396
huffman@15576
   397
lemma monofun_Ispair1: "monofun(Ispair)"
huffman@15576
   398
apply (unfold monofun)
huffman@15576
   399
apply (intro strip)
huffman@15576
   400
apply (rule less_fun [THEN iffD2])
huffman@15576
   401
apply (intro strip)
huffman@15576
   402
apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
huffman@15576
   403
apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
huffman@15576
   404
apply (frule notUU_I)
huffman@15576
   405
apply assumption
huffman@15576
   406
apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
huffman@15576
   407
done
huffman@15576
   408
huffman@15576
   409
lemma monofun_Ispair2: "monofun(Ispair(x))"
huffman@15576
   410
apply (unfold monofun)
huffman@15576
   411
apply (intro strip)
huffman@15576
   412
apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
huffman@15576
   413
apply (rule_tac Q = "xa=UU" in excluded_middle [THEN disjE])
huffman@15576
   414
apply (frule notUU_I)
huffman@15576
   415
apply assumption
huffman@15576
   416
apply (simp_all add: Sprod0_ss inst_sprod_po refl_less minimal)
huffman@15576
   417
done
huffman@15576
   418
huffman@15576
   419
lemma monofun_Ispair: "[|x1<<x2; y1<<y2|] ==> Ispair x1 y1 << Ispair x2 y2"
huffman@15576
   420
apply (rule trans_less)
huffman@15576
   421
apply (rule monofun_Ispair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
huffman@15576
   422
prefer 2 apply (rule monofun_Ispair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
huffman@15576
   423
apply assumption
huffman@15576
   424
apply assumption
huffman@15576
   425
done
huffman@15576
   426
huffman@15576
   427
(* ------------------------------------------------------------------------ *)
huffman@15576
   428
(* Isfst and Issnd are monotone                                             *)
huffman@15576
   429
(* ------------------------------------------------------------------------ *)
huffman@15576
   430
huffman@15576
   431
lemma monofun_Isfst: "monofun(Isfst)"
huffman@15576
   432
apply (unfold monofun)
huffman@15576
   433
apply (simp add: inst_sprod_po)
huffman@15576
   434
done
huffman@15576
   435
huffman@15576
   436
lemma monofun_Issnd: "monofun(Issnd)"
huffman@15576
   437
apply (unfold monofun)
huffman@15576
   438
apply (simp add: inst_sprod_po)
huffman@15576
   439
done
huffman@15576
   440
huffman@15576
   441
subsection {* The strict product is a cpo *}
huffman@15576
   442
(* ------------------------------------------------------------------------ *)
huffman@15576
   443
(* the type 'a ** 'b is a cpo                                               *)
huffman@15576
   444
(* ------------------------------------------------------------------------ *)
huffman@15576
   445
huffman@15576
   446
lemma lub_sprod: 
huffman@15576
   447
"[|chain(S)|] ==> range(S) <<|  
huffman@15576
   448
  Ispair (lub(range(%i. Isfst(S i)))) (lub(range(%i. Issnd(S i))))"
huffman@15576
   449
apply (rule is_lubI)
huffman@15576
   450
apply (rule ub_rangeI)
huffman@15576
   451
apply (rule_tac t = "S (i) " in surjective_pairing_Sprod [THEN ssubst])
huffman@15576
   452
apply (rule monofun_Ispair)
huffman@15576
   453
apply (rule is_ub_thelub)
huffman@15576
   454
apply (erule monofun_Isfst [THEN ch2ch_monofun])
huffman@15576
   455
apply (rule is_ub_thelub)
huffman@15576
   456
apply (erule monofun_Issnd [THEN ch2ch_monofun])
huffman@15576
   457
apply (rule_tac t = "u" in surjective_pairing_Sprod [THEN ssubst])
huffman@15576
   458
apply (rule monofun_Ispair)
huffman@15576
   459
apply (rule is_lub_thelub)
huffman@15576
   460
apply (erule monofun_Isfst [THEN ch2ch_monofun])
huffman@15576
   461
apply (erule monofun_Isfst [THEN ub2ub_monofun])
huffman@15576
   462
apply (rule is_lub_thelub)
huffman@15576
   463
apply (erule monofun_Issnd [THEN ch2ch_monofun])
huffman@15576
   464
apply (erule monofun_Issnd [THEN ub2ub_monofun])
huffman@15576
   465
done
huffman@15576
   466
huffman@15576
   467
lemmas thelub_sprod = lub_sprod [THEN thelubI, standard]
huffman@15576
   468
huffman@15576
   469
lemma cpo_sprod: "chain(S::nat=>'a**'b)==>? x. range(S)<<| x"
huffman@15576
   470
apply (rule exI)
huffman@15576
   471
apply (erule lub_sprod)
huffman@15576
   472
done
huffman@15576
   473
huffman@15576
   474
instance "**" :: (pcpo, pcpo) cpo
huffman@15576
   475
by intro_classes (rule cpo_sprod)
huffman@15576
   476
huffman@15576
   477
huffman@15576
   478
subsection {* The strict product is a pcpo *}
huffman@15576
   479
huffman@15576
   480
lemma minimal_sprod: "Ispair UU UU << p"
huffman@15576
   481
apply (simp add: inst_sprod_po minimal)
huffman@15576
   482
done
huffman@15576
   483
huffman@15576
   484
lemmas UU_sprod_def = minimal_sprod [THEN minimal2UU, symmetric, standard]
huffman@15576
   485
huffman@15576
   486
lemma least_sprod: "? x::'a**'b.!y. x<<y"
huffman@15576
   487
apply (rule_tac x = "Ispair UU UU" in exI)
huffman@15576
   488
apply (rule minimal_sprod [THEN allI])
huffman@15576
   489
done
huffman@15576
   490
huffman@15576
   491
instance "**" :: (pcpo, pcpo) pcpo
huffman@15576
   492
by intro_classes (rule least_sprod)
huffman@15576
   493
huffman@15576
   494
huffman@15576
   495
subsection {* Other constants *}
huffman@15576
   496
huffman@15576
   497
consts  
huffman@15576
   498
  spair		:: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
huffman@15576
   499
  sfst		:: "('a**'b)->'a"
huffman@15576
   500
  ssnd		:: "('a**'b)->'b"
huffman@15576
   501
  ssplit	:: "('a->'b->'c)->('a**'b)->'c"
huffman@15576
   502
huffman@15576
   503
syntax  
huffman@15576
   504
  "@stuple"	:: "['a, args] => 'a ** 'b"	("(1'(:_,/ _:'))")
huffman@15576
   505
huffman@15576
   506
translations
huffman@15576
   507
        "(:x, y, z:)"   == "(:x, (:y, z:):)"
huffman@15576
   508
        "(:x, y:)"      == "spair$x$y"
huffman@15576
   509
huffman@15576
   510
defs
huffman@15576
   511
spair_def:       "spair  == (LAM x y. Ispair x y)"
huffman@15576
   512
sfst_def:        "sfst   == (LAM p. Isfst p)"
huffman@15576
   513
ssnd_def:        "ssnd   == (LAM p. Issnd p)"     
huffman@15576
   514
ssplit_def:      "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
huffman@15576
   515
huffman@15576
   516
(* for compatibility with old HOLCF-Version *)
huffman@15576
   517
lemma inst_sprod_pcpo: "UU = Ispair UU UU"
huffman@15576
   518
apply (simp add: UU_def UU_sprod_def)
huffman@15576
   519
done
huffman@15576
   520
huffman@15576
   521
declare inst_sprod_pcpo [symmetric, simp]
huffman@15576
   522
huffman@15576
   523
(* ------------------------------------------------------------------------ *)
huffman@15576
   524
(* continuity of Ispair, Isfst, Issnd                                       *)
huffman@15576
   525
(* ------------------------------------------------------------------------ *)
huffman@15576
   526
huffman@15576
   527
lemma sprod3_lemma1: 
huffman@15576
   528
"[| chain(Y);  x~= UU;  lub(range(Y))~= UU |] ==> 
huffman@15576
   529
  Ispair (lub(range Y)) x = 
huffman@15576
   530
  Ispair (lub(range(%i. Isfst(Ispair(Y i) x))))  
huffman@15576
   531
         (lub(range(%i. Issnd(Ispair(Y i) x))))"
huffman@15576
   532
apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
huffman@15576
   533
apply (rule lub_equal)
huffman@15576
   534
apply assumption
huffman@15576
   535
apply (rule monofun_Isfst [THEN ch2ch_monofun])
huffman@15576
   536
apply (rule ch2ch_fun)
huffman@15576
   537
apply (rule monofun_Ispair1 [THEN ch2ch_monofun])
huffman@15576
   538
apply assumption
huffman@15576
   539
apply (rule allI)
huffman@15576
   540
apply (simp (no_asm_simp))
huffman@15576
   541
apply (rule sym)
huffman@15576
   542
apply (drule chain_UU_I_inverse2)
huffman@15576
   543
apply (erule exE)
huffman@15576
   544
apply (rule lub_chain_maxelem)
huffman@15576
   545
apply (erule Issnd2)
huffman@15576
   546
apply (rule allI)
huffman@15576
   547
apply (rename_tac "j")
huffman@15576
   548
apply (case_tac "Y (j) =UU")
huffman@15576
   549
apply auto
huffman@15576
   550
done
huffman@15576
   551
huffman@15576
   552
lemma sprod3_lemma2: 
huffman@15576
   553
"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
huffman@15576
   554
    Ispair (lub(range Y)) x = 
huffman@15576
   555
    Ispair (lub(range(%i. Isfst(Ispair(Y i) x)))) 
huffman@15576
   556
           (lub(range(%i. Issnd(Ispair(Y i) x))))"
huffman@15576
   557
apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
huffman@15576
   558
apply assumption
huffman@15576
   559
apply (rule trans)
huffman@15576
   560
apply (rule strict_Ispair1)
huffman@15576
   561
apply (rule strict_Ispair [symmetric])
huffman@15576
   562
apply (rule disjI1)
huffman@15576
   563
apply (rule chain_UU_I_inverse)
huffman@15576
   564
apply auto
huffman@15576
   565
apply (erule chain_UU_I [THEN spec])
huffman@15576
   566
apply assumption
huffman@15576
   567
done
huffman@15576
   568
huffman@15576
   569
huffman@15576
   570
lemma sprod3_lemma3: 
huffman@15576
   571
"[| chain(Y); x = UU |] ==> 
huffman@15576
   572
           Ispair (lub(range Y)) x = 
huffman@15576
   573
           Ispair (lub(range(%i. Isfst(Ispair (Y i) x)))) 
huffman@15576
   574
                  (lub(range(%i. Issnd(Ispair (Y i) x))))"
huffman@15576
   575
apply (erule ssubst)
huffman@15576
   576
apply (rule trans)
huffman@15576
   577
apply (rule strict_Ispair2)
huffman@15576
   578
apply (rule strict_Ispair [symmetric])
huffman@15576
   579
apply (rule disjI1)
huffman@15576
   580
apply (rule chain_UU_I_inverse)
huffman@15576
   581
apply (rule allI)
huffman@15576
   582
apply (simp add: Sprod0_ss)
huffman@15576
   583
done
huffman@15576
   584
huffman@15576
   585
lemma contlub_Ispair1: "contlub(Ispair)"
huffman@15576
   586
apply (rule contlubI)
huffman@15576
   587
apply (intro strip)
huffman@15576
   588
apply (rule expand_fun_eq [THEN iffD2])
huffman@15576
   589
apply (intro strip)
huffman@15576
   590
apply (subst lub_fun [THEN thelubI])
huffman@15576
   591
apply (erule monofun_Ispair1 [THEN ch2ch_monofun])
huffman@15576
   592
apply (rule trans)
huffman@15576
   593
apply (rule_tac [2] thelub_sprod [symmetric])
huffman@15576
   594
apply (rule_tac [2] ch2ch_fun)
huffman@15576
   595
apply (erule_tac [2] monofun_Ispair1 [THEN ch2ch_monofun])
huffman@15576
   596
apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
huffman@15576
   597
apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
huffman@15576
   598
apply (erule sprod3_lemma1)
huffman@15576
   599
apply assumption
huffman@15576
   600
apply assumption
huffman@15576
   601
apply (erule sprod3_lemma2)
huffman@15576
   602
apply assumption
huffman@15576
   603
apply assumption
huffman@15576
   604
apply (erule sprod3_lemma3)
huffman@15576
   605
apply assumption
huffman@15576
   606
done
huffman@15576
   607
huffman@15576
   608
lemma sprod3_lemma4: 
huffman@15576
   609
"[| chain(Y); x ~= UU; lub(range(Y)) ~= UU |] ==> 
huffman@15576
   610
          Ispair x (lub(range Y)) = 
huffman@15576
   611
          Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
huffman@15576
   612
                 (lub(range(%i. Issnd (Ispair x (Y i)))))"
huffman@15576
   613
apply (rule_tac f1 = "Ispair" in arg_cong [THEN cong])
huffman@15576
   614
apply (rule sym)
huffman@15576
   615
apply (drule chain_UU_I_inverse2)
huffman@15576
   616
apply (erule exE)
huffman@15576
   617
apply (rule lub_chain_maxelem)
huffman@15576
   618
apply (erule Isfst2)
huffman@15576
   619
apply (rule allI)
huffman@15576
   620
apply (rename_tac "j")
huffman@15576
   621
apply (case_tac "Y (j) =UU")
huffman@15576
   622
apply auto
huffman@15576
   623
done
huffman@15576
   624
huffman@15576
   625
lemma sprod3_lemma5: 
huffman@15576
   626
"[| chain(Y); x ~= UU; lub(range(Y)) = UU |] ==> 
huffman@15576
   627
          Ispair x (lub(range Y)) = 
huffman@15576
   628
          Ispair (lub(range(%i. Isfst(Ispair x (Y i))))) 
huffman@15576
   629
                 (lub(range(%i. Issnd(Ispair x (Y i)))))"
huffman@15576
   630
apply (rule_tac s = "UU" and t = "lub (range (Y))" in ssubst)
huffman@15576
   631
apply assumption
huffman@15576
   632
apply (rule trans)
huffman@15576
   633
apply (rule strict_Ispair2)
huffman@15576
   634
apply (rule strict_Ispair [symmetric])
huffman@15576
   635
apply (rule disjI2)
huffman@15576
   636
apply (rule chain_UU_I_inverse)
huffman@15576
   637
apply (rule allI)
huffman@15576
   638
apply (simp add: Sprod0_ss)
huffman@15576
   639
apply (erule chain_UU_I [THEN spec])
huffman@15576
   640
apply assumption
huffman@15576
   641
done
huffman@15576
   642
huffman@15576
   643
lemma sprod3_lemma6: 
huffman@15576
   644
"[| chain(Y); x = UU |] ==> 
huffman@15576
   645
          Ispair x (lub(range Y)) = 
huffman@15576
   646
          Ispair (lub(range(%i. Isfst (Ispair x (Y i))))) 
huffman@15576
   647
                 (lub(range(%i. Issnd (Ispair x (Y i)))))"
huffman@15576
   648
apply (rule_tac s = "UU" and t = "x" in ssubst)
huffman@15576
   649
apply assumption
huffman@15576
   650
apply (rule trans)
huffman@15576
   651
apply (rule strict_Ispair1)
huffman@15576
   652
apply (rule strict_Ispair [symmetric])
huffman@15576
   653
apply (rule disjI1)
huffman@15576
   654
apply (rule chain_UU_I_inverse)
huffman@15576
   655
apply (rule allI)
huffman@15576
   656
apply (simp add: Sprod0_ss)
huffman@15576
   657
done
huffman@15576
   658
huffman@15576
   659
lemma contlub_Ispair2: "contlub(Ispair(x))"
huffman@15576
   660
apply (rule contlubI)
huffman@15576
   661
apply (intro strip)
huffman@15576
   662
apply (rule trans)
huffman@15576
   663
apply (rule_tac [2] thelub_sprod [symmetric])
huffman@15576
   664
apply (erule_tac [2] monofun_Ispair2 [THEN ch2ch_monofun])
huffman@15576
   665
apply (rule_tac Q = "x=UU" in excluded_middle [THEN disjE])
huffman@15576
   666
apply (rule_tac Q = "lub (range (Y))=UU" in excluded_middle [THEN disjE])
huffman@15576
   667
apply (erule sprod3_lemma4)
huffman@15576
   668
apply assumption
huffman@15576
   669
apply assumption
huffman@15576
   670
apply (erule sprod3_lemma5)
huffman@15576
   671
apply assumption
huffman@15576
   672
apply assumption
huffman@15576
   673
apply (erule sprod3_lemma6)
huffman@15576
   674
apply assumption
huffman@15576
   675
done
huffman@15576
   676
huffman@15576
   677
lemma cont_Ispair1: "cont(Ispair)"
huffman@15576
   678
apply (rule monocontlub2cont)
huffman@15576
   679
apply (rule monofun_Ispair1)
huffman@15576
   680
apply (rule contlub_Ispair1)
huffman@15576
   681
done
huffman@15576
   682
huffman@15576
   683
lemma cont_Ispair2: "cont(Ispair(x))"
huffman@15576
   684
apply (rule monocontlub2cont)
huffman@15576
   685
apply (rule monofun_Ispair2)
huffman@15576
   686
apply (rule contlub_Ispair2)
huffman@15576
   687
done
huffman@15576
   688
huffman@15576
   689
lemma contlub_Isfst: "contlub(Isfst)"
huffman@15576
   690
apply (rule contlubI)
huffman@15576
   691
apply (intro strip)
huffman@15576
   692
apply (subst lub_sprod [THEN thelubI])
huffman@15576
   693
apply assumption
huffman@15576
   694
apply (rule_tac Q = "lub (range (%i. Issnd (Y (i))))=UU" in excluded_middle [THEN disjE])
huffman@15576
   695
apply (simp add: Sprod0_ss)
huffman@15576
   696
apply (rule_tac s = "UU" and t = "lub (range (%i. Issnd (Y (i))))" in ssubst)
huffman@15576
   697
apply assumption
huffman@15576
   698
apply (rule trans)
huffman@15576
   699
apply (simp add: Sprod0_ss)
huffman@15576
   700
apply (rule sym)
huffman@15576
   701
apply (rule chain_UU_I_inverse)
huffman@15576
   702
apply (rule allI)
huffman@15576
   703
apply (rule strict_Isfst)
huffman@15576
   704
apply (rule contrapos_np)
huffman@15576
   705
apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct2])
huffman@15576
   706
apply (fast dest!: monofun_Issnd [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
huffman@15576
   707
done
huffman@15576
   708
huffman@15576
   709
lemma contlub_Issnd: "contlub(Issnd)"
huffman@15576
   710
apply (rule contlubI)
huffman@15576
   711
apply (intro strip)
huffman@15576
   712
apply (subst lub_sprod [THEN thelubI])
huffman@15576
   713
apply assumption
huffman@15576
   714
apply (rule_tac Q = "lub (range (%i. Isfst (Y (i))))=UU" in excluded_middle [THEN disjE])
huffman@15576
   715
apply (simp add: Sprod0_ss)
huffman@15576
   716
apply (rule_tac s = "UU" and t = "lub (range (%i. Isfst (Y (i))))" in ssubst)
huffman@15576
   717
apply assumption
huffman@15576
   718
apply (simp add: Sprod0_ss)
huffman@15576
   719
apply (rule sym)
huffman@15576
   720
apply (rule chain_UU_I_inverse)
huffman@15576
   721
apply (rule allI)
huffman@15576
   722
apply (rule strict_Issnd)
huffman@15576
   723
apply (rule contrapos_np)
huffman@15576
   724
apply (erule_tac [2] defined_IsfstIssnd [THEN conjunct1])
huffman@15576
   725
apply (fast dest!: monofun_Isfst [THEN ch2ch_monofun, THEN chain_UU_I, THEN spec])
huffman@15576
   726
done
huffman@15576
   727
huffman@15576
   728
lemma cont_Isfst: "cont(Isfst)"
huffman@15576
   729
apply (rule monocontlub2cont)
huffman@15576
   730
apply (rule monofun_Isfst)
huffman@15576
   731
apply (rule contlub_Isfst)
huffman@15576
   732
done
huffman@15576
   733
huffman@15576
   734
lemma cont_Issnd: "cont(Issnd)"
huffman@15576
   735
apply (rule monocontlub2cont)
huffman@15576
   736
apply (rule monofun_Issnd)
huffman@15576
   737
apply (rule contlub_Issnd)
huffman@15576
   738
done
huffman@15576
   739
huffman@15576
   740
lemma spair_eq: "[|x1=x2;y1=y2|] ==> (:x1,y1:) = (:x2,y2:)"
huffman@15576
   741
apply fast
huffman@15576
   742
done
huffman@15576
   743
huffman@15576
   744
(* ------------------------------------------------------------------------ *)
huffman@15576
   745
(* convert all lemmas to the continuous versions                            *)
huffman@15576
   746
(* ------------------------------------------------------------------------ *)
huffman@15576
   747
huffman@15576
   748
lemma beta_cfun_sprod [simp]: 
huffman@15576
   749
        "(LAM x y. Ispair x y)$a$b = Ispair a b"
huffman@15576
   750
apply (subst beta_cfun)
huffman@15576
   751
apply (simp (no_asm) add: cont_Ispair2 cont_Ispair1 cont2cont_CF1L)
huffman@15576
   752
apply (subst beta_cfun)
huffman@15576
   753
apply (rule cont_Ispair2)
huffman@15576
   754
apply (rule refl)
huffman@15576
   755
done
huffman@15576
   756
huffman@15576
   757
lemma inject_spair: 
huffman@15576
   758
        "[| aa~=UU ; ba~=UU ; (:a,b:)=(:aa,ba:) |] ==> a=aa & b=ba"
huffman@15576
   759
apply (unfold spair_def)
huffman@15576
   760
apply (erule inject_Ispair)
huffman@15576
   761
apply assumption
huffman@15576
   762
apply (erule box_equals)
huffman@15576
   763
apply (rule beta_cfun_sprod)
huffman@15576
   764
apply (rule beta_cfun_sprod)
huffman@15576
   765
done
huffman@15576
   766
huffman@15576
   767
lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
huffman@15576
   768
apply (unfold spair_def)
huffman@15576
   769
apply (rule sym)
huffman@15576
   770
apply (rule trans)
huffman@15576
   771
apply (rule beta_cfun_sprod)
huffman@15576
   772
apply (rule sym)
huffman@15576
   773
apply (rule inst_sprod_pcpo)
huffman@15576
   774
done
huffman@15576
   775
huffman@15576
   776
lemma strict_spair: 
huffman@15576
   777
        "(a=UU | b=UU) ==> (:a,b:)=UU"
huffman@15576
   778
apply (unfold spair_def)
huffman@15576
   779
apply (rule trans)
huffman@15576
   780
apply (rule beta_cfun_sprod)
huffman@15576
   781
apply (rule trans)
huffman@15576
   782
apply (rule_tac [2] inst_sprod_pcpo [symmetric])
huffman@15576
   783
apply (erule strict_Ispair)
huffman@15576
   784
done
huffman@15576
   785
huffman@15576
   786
lemma strict_spair1: "(:UU,b:) = UU"
huffman@15576
   787
apply (unfold spair_def)
huffman@15576
   788
apply (subst beta_cfun_sprod)
huffman@15576
   789
apply (rule trans)
huffman@15576
   790
apply (rule_tac [2] inst_sprod_pcpo [symmetric])
huffman@15576
   791
apply (rule strict_Ispair1)
huffman@15576
   792
done
huffman@15576
   793
huffman@15576
   794
lemma strict_spair2: "(:a,UU:) = UU"
huffman@15576
   795
apply (unfold spair_def)
huffman@15576
   796
apply (subst beta_cfun_sprod)
huffman@15576
   797
apply (rule trans)
huffman@15576
   798
apply (rule_tac [2] inst_sprod_pcpo [symmetric])
huffman@15576
   799
apply (rule strict_Ispair2)
huffman@15576
   800
done
huffman@15576
   801
huffman@15576
   802
declare strict_spair1 [simp] strict_spair2 [simp]
huffman@15576
   803
huffman@15576
   804
lemma strict_spair_rev: "(:x,y:)~=UU ==> ~x=UU & ~y=UU"
huffman@15576
   805
apply (unfold spair_def)
huffman@15576
   806
apply (rule strict_Ispair_rev)
huffman@15576
   807
apply auto
huffman@15576
   808
done
huffman@15576
   809
huffman@15576
   810
lemma defined_spair_rev: "(:a,b:) = UU ==> (a = UU | b = UU)"
huffman@15576
   811
apply (unfold spair_def)
huffman@15576
   812
apply (rule defined_Ispair_rev)
huffman@15576
   813
apply auto
huffman@15576
   814
done
huffman@15576
   815
huffman@15576
   816
lemma defined_spair: 
huffman@15576
   817
        "[|a~=UU; b~=UU|] ==> (:a,b:) ~= UU"
huffman@15576
   818
apply (unfold spair_def)
huffman@15576
   819
apply (subst beta_cfun_sprod)
huffman@15576
   820
apply (subst inst_sprod_pcpo)
huffman@15576
   821
apply (erule defined_Ispair)
huffman@15576
   822
apply assumption
huffman@15576
   823
done
huffman@15576
   824
huffman@15576
   825
lemma Exh_Sprod2:
huffman@15576
   826
        "z=UU | (? a b. z=(:a,b:) & a~=UU & b~=UU)"
huffman@15576
   827
apply (unfold spair_def)
huffman@15576
   828
apply (rule Exh_Sprod [THEN disjE])
huffman@15576
   829
apply (rule disjI1)
huffman@15576
   830
apply (subst inst_sprod_pcpo)
huffman@15576
   831
apply assumption
huffman@15576
   832
apply (rule disjI2)
huffman@15576
   833
apply (erule exE)
huffman@15576
   834
apply (erule exE)
huffman@15576
   835
apply (rule exI)
huffman@15576
   836
apply (rule exI)
huffman@15576
   837
apply (rule conjI)
huffman@15576
   838
apply (subst beta_cfun_sprod)
huffman@15576
   839
apply fast
huffman@15576
   840
apply fast
huffman@15576
   841
done
huffman@15576
   842
huffman@15576
   843
huffman@15576
   844
lemma sprodE:
huffman@15576
   845
assumes prem1: "p=UU ==> Q"
huffman@15576
   846
assumes prem2: "!!x y. [| p=(:x,y:); x~=UU; y~=UU|] ==> Q"
huffman@15576
   847
shows "Q"
huffman@15576
   848
apply (rule IsprodE)
huffman@15576
   849
apply (rule prem1)
huffman@15576
   850
apply (subst inst_sprod_pcpo)
huffman@15576
   851
apply assumption
huffman@15576
   852
apply (rule prem2)
huffman@15576
   853
prefer 2 apply (assumption)
huffman@15576
   854
prefer 2 apply (assumption)
huffman@15576
   855
apply (unfold spair_def)
huffman@15576
   856
apply (subst beta_cfun_sprod)
huffman@15576
   857
apply assumption
huffman@15576
   858
done
huffman@15576
   859
huffman@15576
   860
huffman@15576
   861
lemma strict_sfst: 
huffman@15576
   862
        "p=UU==>sfst$p=UU"
huffman@15576
   863
apply (unfold sfst_def)
huffman@15576
   864
apply (subst beta_cfun)
huffman@15576
   865
apply (rule cont_Isfst)
huffman@15576
   866
apply (rule strict_Isfst)
huffman@15576
   867
apply (rule inst_sprod_pcpo [THEN subst])
huffman@15576
   868
apply assumption
huffman@15576
   869
done
huffman@15576
   870
huffman@15576
   871
lemma strict_sfst1: 
huffman@15576
   872
        "sfst$(:UU,y:) = UU"
huffman@15576
   873
apply (unfold sfst_def spair_def)
huffman@15576
   874
apply (subst beta_cfun_sprod)
huffman@15576
   875
apply (subst beta_cfun)
huffman@15576
   876
apply (rule cont_Isfst)
huffman@15576
   877
apply (rule strict_Isfst1)
huffman@15576
   878
done
huffman@15576
   879
 
huffman@15576
   880
lemma strict_sfst2: 
huffman@15576
   881
        "sfst$(:x,UU:) = UU"
huffman@15576
   882
apply (unfold sfst_def spair_def)
huffman@15576
   883
apply (subst beta_cfun_sprod)
huffman@15576
   884
apply (subst beta_cfun)
huffman@15576
   885
apply (rule cont_Isfst)
huffman@15576
   886
apply (rule strict_Isfst2)
huffman@15576
   887
done
huffman@15576
   888
huffman@15576
   889
lemma strict_ssnd: 
huffman@15576
   890
        "p=UU==>ssnd$p=UU"
huffman@15576
   891
apply (unfold ssnd_def)
huffman@15576
   892
apply (subst beta_cfun)
huffman@15576
   893
apply (rule cont_Issnd)
huffman@15576
   894
apply (rule strict_Issnd)
huffman@15576
   895
apply (rule inst_sprod_pcpo [THEN subst])
huffman@15576
   896
apply assumption
huffman@15576
   897
done
huffman@15576
   898
huffman@15576
   899
lemma strict_ssnd1: 
huffman@15576
   900
        "ssnd$(:UU,y:) = UU"
huffman@15576
   901
apply (unfold ssnd_def spair_def)
huffman@15576
   902
apply (subst beta_cfun_sprod)
huffman@15576
   903
apply (subst beta_cfun)
huffman@15576
   904
apply (rule cont_Issnd)
huffman@15576
   905
apply (rule strict_Issnd1)
huffman@15576
   906
done
huffman@15576
   907
huffman@15576
   908
lemma strict_ssnd2: 
huffman@15576
   909
        "ssnd$(:x,UU:) = UU"
huffman@15576
   910
apply (unfold ssnd_def spair_def)
huffman@15576
   911
apply (subst beta_cfun_sprod)
huffman@15576
   912
apply (subst beta_cfun)
huffman@15576
   913
apply (rule cont_Issnd)
huffman@15576
   914
apply (rule strict_Issnd2)
huffman@15576
   915
done
huffman@15576
   916
huffman@15576
   917
lemma sfst2: 
huffman@15576
   918
        "y~=UU ==>sfst$(:x,y:)=x"
huffman@15576
   919
apply (unfold sfst_def spair_def)
huffman@15576
   920
apply (subst beta_cfun_sprod)
huffman@15576
   921
apply (subst beta_cfun)
huffman@15576
   922
apply (rule cont_Isfst)
huffman@15576
   923
apply (erule Isfst2)
huffman@15576
   924
done
huffman@15576
   925
huffman@15576
   926
lemma ssnd2: 
huffman@15576
   927
        "x~=UU ==>ssnd$(:x,y:)=y"
huffman@15576
   928
apply (unfold ssnd_def spair_def)
huffman@15576
   929
apply (subst beta_cfun_sprod)
huffman@15576
   930
apply (subst beta_cfun)
huffman@15576
   931
apply (rule cont_Issnd)
huffman@15576
   932
apply (erule Issnd2)
huffman@15576
   933
done
huffman@15576
   934
huffman@15576
   935
huffman@15576
   936
lemma defined_sfstssnd: 
huffman@15576
   937
        "p~=UU ==> sfst$p ~=UU & ssnd$p ~=UU"
huffman@15576
   938
apply (unfold sfst_def ssnd_def spair_def)
huffman@15576
   939
apply (simplesubst beta_cfun)
huffman@15576
   940
apply (rule cont_Issnd)
huffman@15576
   941
apply (subst beta_cfun)
huffman@15576
   942
apply (rule cont_Isfst)
huffman@15576
   943
apply (rule defined_IsfstIssnd)
huffman@15576
   944
apply (rule inst_sprod_pcpo [THEN subst])
huffman@15576
   945
apply assumption
huffman@15576
   946
done
huffman@15576
   947
 
huffman@15576
   948
lemma surjective_pairing_Sprod2: "(:sfst$p , ssnd$p:) = p"
huffman@15576
   949
apply (unfold sfst_def ssnd_def spair_def)
huffman@15576
   950
apply (subst beta_cfun_sprod)
huffman@15576
   951
apply (simplesubst beta_cfun)
huffman@15576
   952
apply (rule cont_Issnd)
huffman@15576
   953
apply (subst beta_cfun)
huffman@15576
   954
apply (rule cont_Isfst)
huffman@15576
   955
apply (rule surjective_pairing_Sprod [symmetric])
huffman@15576
   956
done
huffman@15576
   957
huffman@15576
   958
lemma lub_sprod2: 
huffman@15576
   959
"chain(S) ==> range(S) <<|  
huffman@15576
   960
               (: lub(range(%i. sfst$(S i))), lub(range(%i. ssnd$(S i))) :)"
huffman@15576
   961
apply (unfold sfst_def ssnd_def spair_def)
huffman@15576
   962
apply (subst beta_cfun_sprod)
huffman@15576
   963
apply (simplesubst beta_cfun [THEN ext])
huffman@15576
   964
apply (rule cont_Issnd)
huffman@15576
   965
apply (subst beta_cfun [THEN ext])
huffman@15576
   966
apply (rule cont_Isfst)
huffman@15576
   967
apply (erule lub_sprod)
huffman@15576
   968
done
huffman@15576
   969
huffman@15576
   970
huffman@15576
   971
lemmas thelub_sprod2 = lub_sprod2 [THEN thelubI, standard]
huffman@15576
   972
(*
huffman@15576
   973
 "chain ?S1 ==>
huffman@15576
   974
 lub (range ?S1) =
huffman@15576
   975
 (:lub (range (%i. sfst$(?S1 i))), lub (range (%i. ssnd$(?S1 i))):)" : thm
huffman@15576
   976
*)
huffman@15576
   977
huffman@15576
   978
lemma ssplit1: 
huffman@15576
   979
        "ssplit$f$UU=UU"
huffman@15576
   980
apply (unfold ssplit_def)
huffman@15576
   981
apply (subst beta_cfun)
huffman@15576
   982
apply (simp (no_asm))
huffman@15576
   983
apply (subst strictify1)
huffman@15576
   984
apply (rule refl)
huffman@15576
   985
done
huffman@15576
   986
huffman@15576
   987
lemma ssplit2: 
huffman@15576
   988
        "[|x~=UU;y~=UU|] ==> ssplit$f$(:x,y:)= f$x$y"
huffman@15576
   989
apply (unfold ssplit_def)
huffman@15576
   990
apply (subst beta_cfun)
huffman@15576
   991
apply (simp (no_asm))
huffman@15576
   992
apply (subst strictify2)
huffman@15576
   993
apply (rule defined_spair)
huffman@15576
   994
apply assumption
huffman@15576
   995
apply assumption
huffman@15576
   996
apply (subst beta_cfun)
huffman@15576
   997
apply (simp (no_asm))
huffman@15576
   998
apply (subst sfst2)
huffman@15576
   999
apply assumption
huffman@15576
  1000
apply (subst ssnd2)
huffman@15576
  1001
apply assumption
huffman@15576
  1002
apply (rule refl)
huffman@15576
  1003
done
huffman@15576
  1004
huffman@15576
  1005
huffman@15576
  1006
lemma ssplit3: 
huffman@15576
  1007
  "ssplit$spair$z=z"
huffman@15576
  1008
apply (unfold ssplit_def)
huffman@15576
  1009
apply (subst beta_cfun)
huffman@15576
  1010
apply (simp (no_asm))
huffman@15576
  1011
apply (case_tac "z=UU")
huffman@15576
  1012
apply (erule ssubst)
huffman@15576
  1013
apply (rule strictify1)
huffman@15576
  1014
apply (rule trans)
huffman@15576
  1015
apply (rule strictify2)
huffman@15576
  1016
apply assumption
huffman@15576
  1017
apply (subst beta_cfun)
huffman@15576
  1018
apply (simp (no_asm))
huffman@15576
  1019
apply (rule surjective_pairing_Sprod2)
huffman@15576
  1020
done
huffman@15576
  1021
huffman@15576
  1022
(* ------------------------------------------------------------------------ *)
huffman@15576
  1023
(* install simplifier for Sprod                                             *)
huffman@15576
  1024
(* ------------------------------------------------------------------------ *)
huffman@15576
  1025
huffman@15576
  1026
lemmas Sprod_rews = strict_sfst1 strict_sfst2
huffman@15576
  1027
                strict_ssnd1 strict_ssnd2 sfst2 ssnd2 defined_spair
huffman@15576
  1028
                ssplit1 ssplit2
huffman@15576
  1029
declare Sprod_rews [simp]
huffman@15576
  1030
huffman@15576
  1031
end