src/HOLCF/Cprod.thy
author huffman
Fri Mar 04 23:12:36 2005 +0100 (2005-03-04)
changeset 15576 efb95d0d01f7
child 15577 e16da3068ad6
permissions -rw-r--r--
converted to new-style theories, and combined numbered files
huffman@15576
     1
(*  Title:      HOLCF/Cprod1.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
Partial ordering for cartesian product of HOL theory prod.thy
huffman@15576
     7
*)
huffman@15576
     8
huffman@15576
     9
header {* The cpo of cartesian products *}
huffman@15576
    10
huffman@15576
    11
theory Cprod = Cfun:
huffman@15576
    12
huffman@15576
    13
defaultsort cpo
huffman@15576
    14
huffman@15576
    15
instance "*"::(sq_ord,sq_ord)sq_ord ..
huffman@15576
    16
huffman@15576
    17
defs (overloaded)
huffman@15576
    18
huffman@15576
    19
  less_cprod_def: "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
huffman@15576
    20
huffman@15576
    21
(* ------------------------------------------------------------------------ *)
huffman@15576
    22
(* less_cprod is a partial order on 'a * 'b                                 *)
huffman@15576
    23
(* ------------------------------------------------------------------------ *)
huffman@15576
    24
huffman@15576
    25
lemma refl_less_cprod: "(p::'a*'b) << p"
huffman@15576
    26
apply (unfold less_cprod_def)
huffman@15576
    27
apply simp
huffman@15576
    28
done
huffman@15576
    29
huffman@15576
    30
lemma antisym_less_cprod: "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
huffman@15576
    31
apply (unfold less_cprod_def)
huffman@15576
    32
apply (rule injective_fst_snd)
huffman@15576
    33
apply (fast intro: antisym_less)
huffman@15576
    34
apply (fast intro: antisym_less)
huffman@15576
    35
done
huffman@15576
    36
huffman@15576
    37
lemma trans_less_cprod: 
huffman@15576
    38
        "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
huffman@15576
    39
apply (unfold less_cprod_def)
huffman@15576
    40
apply (rule conjI)
huffman@15576
    41
apply (fast intro: trans_less)
huffman@15576
    42
apply (fast intro: trans_less)
huffman@15576
    43
done
huffman@15576
    44
huffman@15576
    45
(* Class Instance *::(pcpo,pcpo)po *)
huffman@15576
    46
huffman@15576
    47
defaultsort pcpo
huffman@15576
    48
huffman@15576
    49
instance "*"::(cpo,cpo)po
huffman@15576
    50
apply (intro_classes)
huffman@15576
    51
apply (rule refl_less_cprod)
huffman@15576
    52
apply (rule antisym_less_cprod, assumption+)
huffman@15576
    53
apply (rule trans_less_cprod, assumption+)
huffman@15576
    54
done
huffman@15576
    55
huffman@15576
    56
(* for compatibility with old HOLCF-Version *)
huffman@15576
    57
lemma inst_cprod_po: "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
huffman@15576
    58
apply (fold less_cprod_def)
huffman@15576
    59
apply (rule refl)
huffman@15576
    60
done
huffman@15576
    61
huffman@15576
    62
lemma less_cprod4c: "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"
huffman@15576
    63
apply (simp add: inst_cprod_po)
huffman@15576
    64
done
huffman@15576
    65
huffman@15576
    66
(* ------------------------------------------------------------------------ *)
huffman@15576
    67
(* type cprod is pointed                                                    *)
huffman@15576
    68
(* ------------------------------------------------------------------------ *)
huffman@15576
    69
huffman@15576
    70
lemma minimal_cprod: "(UU,UU)<<p"
huffman@15576
    71
apply (simp (no_asm) add: inst_cprod_po)
huffman@15576
    72
done
huffman@15576
    73
huffman@15576
    74
lemmas UU_cprod_def = minimal_cprod [THEN minimal2UU, symmetric, standard]
huffman@15576
    75
huffman@15576
    76
lemma least_cprod: "EX x::'a*'b. ALL y. x<<y"
huffman@15576
    77
apply (rule_tac x = " (UU,UU) " in exI)
huffman@15576
    78
apply (rule minimal_cprod [THEN allI])
huffman@15576
    79
done
huffman@15576
    80
huffman@15576
    81
(* ------------------------------------------------------------------------ *)
huffman@15576
    82
(* Pair <_,_>  is monotone in both arguments                                *)
huffman@15576
    83
(* ------------------------------------------------------------------------ *)
huffman@15576
    84
huffman@15576
    85
lemma monofun_pair1: "monofun Pair"
huffman@15576
    86
huffman@15576
    87
apply (unfold monofun)
huffman@15576
    88
apply (intro strip)
huffman@15576
    89
apply (rule less_fun [THEN iffD2])
huffman@15576
    90
apply (intro strip)
huffman@15576
    91
apply (simp (no_asm_simp) add: inst_cprod_po)
huffman@15576
    92
done
huffman@15576
    93
huffman@15576
    94
lemma monofun_pair2: "monofun(Pair x)"
huffman@15576
    95
apply (unfold monofun)
huffman@15576
    96
apply (simp (no_asm_simp) add: inst_cprod_po)
huffman@15576
    97
done
huffman@15576
    98
huffman@15576
    99
lemma monofun_pair: "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
huffman@15576
   100
apply (rule trans_less)
huffman@15576
   101
apply (erule monofun_pair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
huffman@15576
   102
apply (erule monofun_pair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
huffman@15576
   103
done
huffman@15576
   104
huffman@15576
   105
(* ------------------------------------------------------------------------ *)
huffman@15576
   106
(* fst and snd are monotone                                                 *)
huffman@15576
   107
(* ------------------------------------------------------------------------ *)
huffman@15576
   108
huffman@15576
   109
lemma monofun_fst: "monofun fst"
huffman@15576
   110
apply (unfold monofun)
huffman@15576
   111
apply (intro strip)
huffman@15576
   112
apply (rule_tac p = "x" in PairE)
huffman@15576
   113
apply (rule_tac p = "y" in PairE)
huffman@15576
   114
apply simp
huffman@15576
   115
apply (erule less_cprod4c [THEN conjunct1])
huffman@15576
   116
done
huffman@15576
   117
huffman@15576
   118
lemma monofun_snd: "monofun snd"
huffman@15576
   119
apply (unfold monofun)
huffman@15576
   120
apply (intro strip)
huffman@15576
   121
apply (rule_tac p = "x" in PairE)
huffman@15576
   122
apply (rule_tac p = "y" in PairE)
huffman@15576
   123
apply simp
huffman@15576
   124
apply (erule less_cprod4c [THEN conjunct2])
huffman@15576
   125
done
huffman@15576
   126
huffman@15576
   127
(* ------------------------------------------------------------------------ *)
huffman@15576
   128
(* the type 'a * 'b is a cpo                                                *)
huffman@15576
   129
(* ------------------------------------------------------------------------ *)
huffman@15576
   130
huffman@15576
   131
lemma lub_cprod: 
huffman@15576
   132
"chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
huffman@15576
   133
apply (rule is_lubI)
huffman@15576
   134
apply (rule ub_rangeI)
huffman@15576
   135
apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
huffman@15576
   136
apply (rule monofun_pair)
huffman@15576
   137
apply (rule is_ub_thelub)
huffman@15576
   138
apply (erule monofun_fst [THEN ch2ch_monofun])
huffman@15576
   139
apply (rule is_ub_thelub)
huffman@15576
   140
apply (erule monofun_snd [THEN ch2ch_monofun])
huffman@15576
   141
apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
huffman@15576
   142
apply (rule monofun_pair)
huffman@15576
   143
apply (rule is_lub_thelub)
huffman@15576
   144
apply (erule monofun_fst [THEN ch2ch_monofun])
huffman@15576
   145
apply (erule monofun_fst [THEN ub2ub_monofun])
huffman@15576
   146
apply (rule is_lub_thelub)
huffman@15576
   147
apply (erule monofun_snd [THEN ch2ch_monofun])
huffman@15576
   148
apply (erule monofun_snd [THEN ub2ub_monofun])
huffman@15576
   149
done
huffman@15576
   150
huffman@15576
   151
lemmas thelub_cprod = lub_cprod [THEN thelubI, standard]
huffman@15576
   152
(*
huffman@15576
   153
"chain ?S1 ==>
huffman@15576
   154
 lub (range ?S1) =
huffman@15576
   155
 (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
huffman@15576
   156
huffman@15576
   157
*)
huffman@15576
   158
huffman@15576
   159
lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x"
huffman@15576
   160
apply (rule exI)
huffman@15576
   161
apply (erule lub_cprod)
huffman@15576
   162
done
huffman@15576
   163
huffman@15576
   164
(* Class instance of * for class pcpo and cpo. *)
huffman@15576
   165
huffman@15576
   166
instance "*" :: (cpo,cpo)cpo
huffman@15576
   167
by (intro_classes, rule cpo_cprod)
huffman@15576
   168
huffman@15576
   169
instance "*" :: (pcpo,pcpo)pcpo
huffman@15576
   170
by (intro_classes, rule least_cprod)
huffman@15576
   171
huffman@15576
   172
consts
huffman@15576
   173
        cpair        :: "'a::cpo -> 'b::cpo -> ('a*'b)" (* continuous pairing *)
huffman@15576
   174
        cfst         :: "('a::cpo*'b::cpo)->'a"
huffman@15576
   175
        csnd         :: "('a::cpo*'b::cpo)->'b"
huffman@15576
   176
        csplit       :: "('a::cpo->'b::cpo->'c::cpo)->('a*'b)->'c"
huffman@15576
   177
huffman@15576
   178
syntax
huffman@15576
   179
        "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
huffman@15576
   180
huffman@15576
   181
translations
huffman@15576
   182
        "<x, y, z>"   == "<x, <y, z>>"
huffman@15576
   183
        "<x, y>"      == "cpair$x$y"
huffman@15576
   184
huffman@15576
   185
defs
huffman@15576
   186
cpair_def:       "cpair  == (LAM x y.(x,y))"
huffman@15576
   187
cfst_def:        "cfst   == (LAM p. fst(p))"
huffman@15576
   188
csnd_def:        "csnd   == (LAM p. snd(p))"      
huffman@15576
   189
csplit_def:      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
huffman@15576
   190
huffman@15576
   191
huffman@15576
   192
huffman@15576
   193
(* introduce syntax for
huffman@15576
   194
huffman@15576
   195
   Let <x,y> = e1; z = E2 in E3
huffman@15576
   196
huffman@15576
   197
   and
huffman@15576
   198
huffman@15576
   199
   LAM <x,y,z>.e
huffman@15576
   200
*)
huffman@15576
   201
huffman@15576
   202
constdefs
huffman@15576
   203
  CLet           :: "'a -> ('a -> 'b) -> 'b"
huffman@15576
   204
  "CLet == LAM s f. f$s"
huffman@15576
   205
huffman@15576
   206
huffman@15576
   207
(* syntax for Let *)
huffman@15576
   208
huffman@15576
   209
nonterminals
huffman@15576
   210
  Cletbinds  Cletbind
huffman@15576
   211
huffman@15576
   212
syntax
huffman@15576
   213
  "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
huffman@15576
   214
  ""        :: "Cletbind => Cletbinds"               ("_")
huffman@15576
   215
  "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
huffman@15576
   216
  "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
huffman@15576
   217
huffman@15576
   218
translations
huffman@15576
   219
  "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
huffman@15576
   220
  "Let x = a in e"          == "CLet$a$(LAM x. e)"
huffman@15576
   221
huffman@15576
   222
huffman@15576
   223
(* syntax for LAM <x,y,z>.e *)
huffman@15576
   224
huffman@15576
   225
syntax
huffman@15576
   226
  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
huffman@15576
   227
huffman@15576
   228
translations
huffman@15576
   229
  "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
huffman@15576
   230
  "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
huffman@15576
   231
  "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
huffman@15576
   232
huffman@15576
   233
syntax (xsymbols)
huffman@15576
   234
  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
huffman@15576
   235
huffman@15576
   236
(* for compatibility with old HOLCF-Version *)
huffman@15576
   237
lemma inst_cprod_pcpo: "UU = (UU,UU)"
huffman@15576
   238
apply (simp add: UU_cprod_def[folded UU_def])
huffman@15576
   239
done
huffman@15576
   240
huffman@15576
   241
(* ------------------------------------------------------------------------ *)
huffman@15576
   242
(* continuity of (_,_) , fst, snd                                           *)
huffman@15576
   243
(* ------------------------------------------------------------------------ *)
huffman@15576
   244
huffman@15576
   245
lemma Cprod3_lemma1: 
huffman@15576
   246
"chain(Y::(nat=>'a::cpo)) ==> 
huffman@15576
   247
  (lub(range(Y)),(x::'b::cpo)) = 
huffman@15576
   248
  (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"
huffman@15576
   249
apply (rule_tac f1 = "Pair" in arg_cong [THEN cong])
huffman@15576
   250
apply (rule lub_equal)
huffman@15576
   251
apply assumption
huffman@15576
   252
apply (rule monofun_fst [THEN ch2ch_monofun])
huffman@15576
   253
apply (rule ch2ch_fun)
huffman@15576
   254
apply (rule monofun_pair1 [THEN ch2ch_monofun])
huffman@15576
   255
apply assumption
huffman@15576
   256
apply (rule allI)
huffman@15576
   257
apply (simp (no_asm))
huffman@15576
   258
apply (rule sym)
huffman@15576
   259
apply (simp (no_asm))
huffman@15576
   260
apply (rule lub_const [THEN thelubI])
huffman@15576
   261
done
huffman@15576
   262
huffman@15576
   263
lemma contlub_pair1: "contlub(Pair)"
huffman@15576
   264
apply (rule contlubI)
huffman@15576
   265
apply (intro strip)
huffman@15576
   266
apply (rule expand_fun_eq [THEN iffD2])
huffman@15576
   267
apply (intro strip)
huffman@15576
   268
apply (subst lub_fun [THEN thelubI])
huffman@15576
   269
apply (erule monofun_pair1 [THEN ch2ch_monofun])
huffman@15576
   270
apply (rule trans)
huffman@15576
   271
apply (rule_tac [2] thelub_cprod [symmetric])
huffman@15576
   272
apply (rule_tac [2] ch2ch_fun)
huffman@15576
   273
apply (erule_tac [2] monofun_pair1 [THEN ch2ch_monofun])
huffman@15576
   274
apply (erule Cprod3_lemma1)
huffman@15576
   275
done
huffman@15576
   276
huffman@15576
   277
lemma Cprod3_lemma2: 
huffman@15576
   278
"chain(Y::(nat=>'a::cpo)) ==> 
huffman@15576
   279
  ((x::'b::cpo),lub(range Y)) = 
huffman@15576
   280
  (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"
huffman@15576
   281
apply (rule_tac f1 = "Pair" in arg_cong [THEN cong])
huffman@15576
   282
apply (rule sym)
huffman@15576
   283
apply (simp (no_asm))
huffman@15576
   284
apply (rule lub_const [THEN thelubI])
huffman@15576
   285
apply (rule lub_equal)
huffman@15576
   286
apply assumption
huffman@15576
   287
apply (rule monofun_snd [THEN ch2ch_monofun])
huffman@15576
   288
apply (rule monofun_pair2 [THEN ch2ch_monofun])
huffman@15576
   289
apply assumption
huffman@15576
   290
apply (rule allI)
huffman@15576
   291
apply (simp (no_asm))
huffman@15576
   292
done
huffman@15576
   293
huffman@15576
   294
lemma contlub_pair2: "contlub(Pair(x))"
huffman@15576
   295
apply (rule contlubI)
huffman@15576
   296
apply (intro strip)
huffman@15576
   297
apply (rule trans)
huffman@15576
   298
apply (rule_tac [2] thelub_cprod [symmetric])
huffman@15576
   299
apply (erule_tac [2] monofun_pair2 [THEN ch2ch_monofun])
huffman@15576
   300
apply (erule Cprod3_lemma2)
huffman@15576
   301
done
huffman@15576
   302
huffman@15576
   303
lemma cont_pair1: "cont(Pair)"
huffman@15576
   304
apply (rule monocontlub2cont)
huffman@15576
   305
apply (rule monofun_pair1)
huffman@15576
   306
apply (rule contlub_pair1)
huffman@15576
   307
done
huffman@15576
   308
huffman@15576
   309
lemma cont_pair2: "cont(Pair(x))"
huffman@15576
   310
apply (rule monocontlub2cont)
huffman@15576
   311
apply (rule monofun_pair2)
huffman@15576
   312
apply (rule contlub_pair2)
huffman@15576
   313
done
huffman@15576
   314
huffman@15576
   315
lemma contlub_fst: "contlub(fst)"
huffman@15576
   316
apply (rule contlubI)
huffman@15576
   317
apply (intro strip)
huffman@15576
   318
apply (subst lub_cprod [THEN thelubI])
huffman@15576
   319
apply assumption
huffman@15576
   320
apply (simp (no_asm))
huffman@15576
   321
done
huffman@15576
   322
huffman@15576
   323
lemma contlub_snd: "contlub(snd)"
huffman@15576
   324
apply (rule contlubI)
huffman@15576
   325
apply (intro strip)
huffman@15576
   326
apply (subst lub_cprod [THEN thelubI])
huffman@15576
   327
apply assumption
huffman@15576
   328
apply (simp (no_asm))
huffman@15576
   329
done
huffman@15576
   330
huffman@15576
   331
lemma cont_fst: "cont(fst)"
huffman@15576
   332
apply (rule monocontlub2cont)
huffman@15576
   333
apply (rule monofun_fst)
huffman@15576
   334
apply (rule contlub_fst)
huffman@15576
   335
done
huffman@15576
   336
huffman@15576
   337
lemma cont_snd: "cont(snd)"
huffman@15576
   338
apply (rule monocontlub2cont)
huffman@15576
   339
apply (rule monofun_snd)
huffman@15576
   340
apply (rule contlub_snd)
huffman@15576
   341
done
huffman@15576
   342
huffman@15576
   343
(* 
huffman@15576
   344
 -------------------------------------------------------------------------- 
huffman@15576
   345
 more lemmas for Cprod3.thy 
huffman@15576
   346
 
huffman@15576
   347
 -------------------------------------------------------------------------- 
huffman@15576
   348
*)
huffman@15576
   349
huffman@15576
   350
(* ------------------------------------------------------------------------ *)
huffman@15576
   351
(* convert all lemmas to the continuous versions                            *)
huffman@15576
   352
(* ------------------------------------------------------------------------ *)
huffman@15576
   353
huffman@15576
   354
lemma beta_cfun_cprod: 
huffman@15576
   355
        "(LAM x y.(x,y))$a$b = (a,b)"
huffman@15576
   356
apply (subst beta_cfun)
huffman@15576
   357
apply (simp (no_asm) add: cont_pair1 cont_pair2 cont2cont_CF1L)
huffman@15576
   358
apply (subst beta_cfun)
huffman@15576
   359
apply (rule cont_pair2)
huffman@15576
   360
apply (rule refl)
huffman@15576
   361
done
huffman@15576
   362
huffman@15576
   363
lemma inject_cpair: 
huffman@15576
   364
        "<a,b> = <aa,ba>  ==> a=aa & b=ba"
huffman@15576
   365
apply (unfold cpair_def)
huffman@15576
   366
apply (drule beta_cfun_cprod [THEN subst])
huffman@15576
   367
apply (drule beta_cfun_cprod [THEN subst])
huffman@15576
   368
apply (erule Pair_inject)
huffman@15576
   369
apply fast
huffman@15576
   370
done
huffman@15576
   371
huffman@15576
   372
lemma inst_cprod_pcpo2: "UU = <UU,UU>"
huffman@15576
   373
apply (unfold cpair_def)
huffman@15576
   374
apply (rule sym)
huffman@15576
   375
apply (rule trans)
huffman@15576
   376
apply (rule beta_cfun_cprod)
huffman@15576
   377
apply (rule sym)
huffman@15576
   378
apply (rule inst_cprod_pcpo)
huffman@15576
   379
done
huffman@15576
   380
huffman@15576
   381
lemma defined_cpair_rev: 
huffman@15576
   382
 "<a,b> = UU ==> a = UU & b = UU"
huffman@15576
   383
apply (drule inst_cprod_pcpo2 [THEN subst])
huffman@15576
   384
apply (erule inject_cpair)
huffman@15576
   385
done
huffman@15576
   386
huffman@15576
   387
lemma Exh_Cprod2:
huffman@15576
   388
        "? a b. z=<a,b>"
huffman@15576
   389
apply (unfold cpair_def)
huffman@15576
   390
apply (rule PairE)
huffman@15576
   391
apply (rule exI)
huffman@15576
   392
apply (rule exI)
huffman@15576
   393
apply (erule beta_cfun_cprod [THEN ssubst])
huffman@15576
   394
done
huffman@15576
   395
huffman@15576
   396
lemma cprodE:
huffman@15576
   397
assumes prems: "!!x y. [| p = <x,y> |] ==> Q"
huffman@15576
   398
shows "Q"
huffman@15576
   399
apply (rule PairE)
huffman@15576
   400
apply (rule prems)
huffman@15576
   401
apply (unfold cpair_def)
huffman@15576
   402
apply (erule beta_cfun_cprod [THEN ssubst])
huffman@15576
   403
done
huffman@15576
   404
huffman@15576
   405
lemma cfst2: 
huffman@15576
   406
        "cfst$<x,y> = x"
huffman@15576
   407
apply (unfold cfst_def cpair_def)
huffman@15576
   408
apply (subst beta_cfun_cprod)
huffman@15576
   409
apply (subst beta_cfun)
huffman@15576
   410
apply (rule cont_fst)
huffman@15576
   411
apply (simp (no_asm))
huffman@15576
   412
done
huffman@15576
   413
huffman@15576
   414
lemma csnd2: 
huffman@15576
   415
        "csnd$<x,y> = y"
huffman@15576
   416
apply (unfold csnd_def cpair_def)
huffman@15576
   417
apply (subst beta_cfun_cprod)
huffman@15576
   418
apply (subst beta_cfun)
huffman@15576
   419
apply (rule cont_snd)
huffman@15576
   420
apply (simp (no_asm))
huffman@15576
   421
done
huffman@15576
   422
huffman@15576
   423
lemma cfst_strict: "cfst$UU = UU"
huffman@15576
   424
apply (simp add: inst_cprod_pcpo2 cfst2)
huffman@15576
   425
done
huffman@15576
   426
huffman@15576
   427
lemma csnd_strict: "csnd$UU = UU"
huffman@15576
   428
apply (simp add: inst_cprod_pcpo2 csnd2)
huffman@15576
   429
done
huffman@15576
   430
huffman@15576
   431
lemma surjective_pairing_Cprod2: "<cfst$p , csnd$p> = p"
huffman@15576
   432
apply (unfold cfst_def csnd_def cpair_def)
huffman@15576
   433
apply (subst beta_cfun_cprod)
huffman@15576
   434
apply (simplesubst beta_cfun)
huffman@15576
   435
apply (rule cont_snd)
huffman@15576
   436
apply (subst beta_cfun)
huffman@15576
   437
apply (rule cont_fst)
huffman@15576
   438
apply (rule surjective_pairing [symmetric])
huffman@15576
   439
done
huffman@15576
   440
huffman@15576
   441
lemma less_cprod5c: 
huffman@15576
   442
 "<xa,ya> << <x,y> ==> xa<<x & ya << y"
huffman@15576
   443
apply (unfold cfst_def csnd_def cpair_def)
huffman@15576
   444
apply (rule less_cprod4c)
huffman@15576
   445
apply (drule beta_cfun_cprod [THEN subst])
huffman@15576
   446
apply (drule beta_cfun_cprod [THEN subst])
huffman@15576
   447
apply assumption
huffman@15576
   448
done
huffman@15576
   449
huffman@15576
   450
lemma lub_cprod2: 
huffman@15576
   451
"[|chain(S)|] ==> range(S) <<|  
huffman@15576
   452
  <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>"
huffman@15576
   453
apply (unfold cfst_def csnd_def cpair_def)
huffman@15576
   454
apply (subst beta_cfun_cprod)
huffman@15576
   455
apply (simplesubst beta_cfun [THEN ext])
huffman@15576
   456
apply (rule cont_snd)
huffman@15576
   457
apply (subst beta_cfun [THEN ext])
huffman@15576
   458
apply (rule cont_fst)
huffman@15576
   459
apply (rule lub_cprod)
huffman@15576
   460
apply assumption
huffman@15576
   461
done
huffman@15576
   462
huffman@15576
   463
lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard]
huffman@15576
   464
(*
huffman@15576
   465
chain ?S1 ==>
huffman@15576
   466
 lub (range ?S1) =
huffman@15576
   467
 <lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" 
huffman@15576
   468
*)
huffman@15576
   469
lemma csplit2: 
huffman@15576
   470
        "csplit$f$<x,y> = f$x$y"
huffman@15576
   471
apply (unfold csplit_def)
huffman@15576
   472
apply (subst beta_cfun)
huffman@15576
   473
apply (simp (no_asm))
huffman@15576
   474
apply (simp (no_asm) add: cfst2 csnd2)
huffman@15576
   475
done
huffman@15576
   476
huffman@15576
   477
lemma csplit3: 
huffman@15576
   478
  "csplit$cpair$z=z"
huffman@15576
   479
apply (unfold csplit_def)
huffman@15576
   480
apply (subst beta_cfun)
huffman@15576
   481
apply (simp (no_asm))
huffman@15576
   482
apply (simp (no_asm) add: surjective_pairing_Cprod2)
huffman@15576
   483
done
huffman@15576
   484
huffman@15576
   485
(* ------------------------------------------------------------------------ *)
huffman@15576
   486
(* install simplifier for Cprod                                             *)
huffman@15576
   487
(* ------------------------------------------------------------------------ *)
huffman@15576
   488
huffman@15576
   489
declare cfst2 [simp] csnd2 [simp] csplit2 [simp]
huffman@15576
   490
huffman@15576
   491
lemmas Cprod_rews = cfst2 csnd2 csplit2
huffman@15576
   492
huffman@15576
   493
end