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