src/HOLCF/Cprod.thy
changeset 15576 efb95d0d01f7
child 15577 e16da3068ad6
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/Cprod.thy	Fri Mar 04 23:12:36 2005 +0100
     1.3 @@ -0,0 +1,493 @@
     1.4 +(*  Title:      HOLCF/Cprod1.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Franz Regensburger
     1.7 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.8 +
     1.9 +Partial ordering for cartesian product of HOL theory prod.thy
    1.10 +*)
    1.11 +
    1.12 +header {* The cpo of cartesian products *}
    1.13 +
    1.14 +theory Cprod = Cfun:
    1.15 +
    1.16 +defaultsort cpo
    1.17 +
    1.18 +instance "*"::(sq_ord,sq_ord)sq_ord ..
    1.19 +
    1.20 +defs (overloaded)
    1.21 +
    1.22 +  less_cprod_def: "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
    1.23 +
    1.24 +(* ------------------------------------------------------------------------ *)
    1.25 +(* less_cprod is a partial order on 'a * 'b                                 *)
    1.26 +(* ------------------------------------------------------------------------ *)
    1.27 +
    1.28 +lemma refl_less_cprod: "(p::'a*'b) << p"
    1.29 +apply (unfold less_cprod_def)
    1.30 +apply simp
    1.31 +done
    1.32 +
    1.33 +lemma antisym_less_cprod: "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
    1.34 +apply (unfold less_cprod_def)
    1.35 +apply (rule injective_fst_snd)
    1.36 +apply (fast intro: antisym_less)
    1.37 +apply (fast intro: antisym_less)
    1.38 +done
    1.39 +
    1.40 +lemma trans_less_cprod: 
    1.41 +        "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
    1.42 +apply (unfold less_cprod_def)
    1.43 +apply (rule conjI)
    1.44 +apply (fast intro: trans_less)
    1.45 +apply (fast intro: trans_less)
    1.46 +done
    1.47 +
    1.48 +(* Class Instance *::(pcpo,pcpo)po *)
    1.49 +
    1.50 +defaultsort pcpo
    1.51 +
    1.52 +instance "*"::(cpo,cpo)po
    1.53 +apply (intro_classes)
    1.54 +apply (rule refl_less_cprod)
    1.55 +apply (rule antisym_less_cprod, assumption+)
    1.56 +apply (rule trans_less_cprod, assumption+)
    1.57 +done
    1.58 +
    1.59 +(* for compatibility with old HOLCF-Version *)
    1.60 +lemma inst_cprod_po: "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
    1.61 +apply (fold less_cprod_def)
    1.62 +apply (rule refl)
    1.63 +done
    1.64 +
    1.65 +lemma less_cprod4c: "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"
    1.66 +apply (simp add: inst_cprod_po)
    1.67 +done
    1.68 +
    1.69 +(* ------------------------------------------------------------------------ *)
    1.70 +(* type cprod is pointed                                                    *)
    1.71 +(* ------------------------------------------------------------------------ *)
    1.72 +
    1.73 +lemma minimal_cprod: "(UU,UU)<<p"
    1.74 +apply (simp (no_asm) add: inst_cprod_po)
    1.75 +done
    1.76 +
    1.77 +lemmas UU_cprod_def = minimal_cprod [THEN minimal2UU, symmetric, standard]
    1.78 +
    1.79 +lemma least_cprod: "EX x::'a*'b. ALL y. x<<y"
    1.80 +apply (rule_tac x = " (UU,UU) " in exI)
    1.81 +apply (rule minimal_cprod [THEN allI])
    1.82 +done
    1.83 +
    1.84 +(* ------------------------------------------------------------------------ *)
    1.85 +(* Pair <_,_>  is monotone in both arguments                                *)
    1.86 +(* ------------------------------------------------------------------------ *)
    1.87 +
    1.88 +lemma monofun_pair1: "monofun Pair"
    1.89 +
    1.90 +apply (unfold monofun)
    1.91 +apply (intro strip)
    1.92 +apply (rule less_fun [THEN iffD2])
    1.93 +apply (intro strip)
    1.94 +apply (simp (no_asm_simp) add: inst_cprod_po)
    1.95 +done
    1.96 +
    1.97 +lemma monofun_pair2: "monofun(Pair x)"
    1.98 +apply (unfold monofun)
    1.99 +apply (simp (no_asm_simp) add: inst_cprod_po)
   1.100 +done
   1.101 +
   1.102 +lemma monofun_pair: "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
   1.103 +apply (rule trans_less)
   1.104 +apply (erule monofun_pair1 [THEN monofunE, THEN spec, THEN spec, THEN mp, THEN less_fun [THEN iffD1, THEN spec]])
   1.105 +apply (erule monofun_pair2 [THEN monofunE, THEN spec, THEN spec, THEN mp])
   1.106 +done
   1.107 +
   1.108 +(* ------------------------------------------------------------------------ *)
   1.109 +(* fst and snd are monotone                                                 *)
   1.110 +(* ------------------------------------------------------------------------ *)
   1.111 +
   1.112 +lemma monofun_fst: "monofun fst"
   1.113 +apply (unfold monofun)
   1.114 +apply (intro strip)
   1.115 +apply (rule_tac p = "x" in PairE)
   1.116 +apply (rule_tac p = "y" in PairE)
   1.117 +apply simp
   1.118 +apply (erule less_cprod4c [THEN conjunct1])
   1.119 +done
   1.120 +
   1.121 +lemma monofun_snd: "monofun snd"
   1.122 +apply (unfold monofun)
   1.123 +apply (intro strip)
   1.124 +apply (rule_tac p = "x" in PairE)
   1.125 +apply (rule_tac p = "y" in PairE)
   1.126 +apply simp
   1.127 +apply (erule less_cprod4c [THEN conjunct2])
   1.128 +done
   1.129 +
   1.130 +(* ------------------------------------------------------------------------ *)
   1.131 +(* the type 'a * 'b is a cpo                                                *)
   1.132 +(* ------------------------------------------------------------------------ *)
   1.133 +
   1.134 +lemma lub_cprod: 
   1.135 +"chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
   1.136 +apply (rule is_lubI)
   1.137 +apply (rule ub_rangeI)
   1.138 +apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
   1.139 +apply (rule monofun_pair)
   1.140 +apply (rule is_ub_thelub)
   1.141 +apply (erule monofun_fst [THEN ch2ch_monofun])
   1.142 +apply (rule is_ub_thelub)
   1.143 +apply (erule monofun_snd [THEN ch2ch_monofun])
   1.144 +apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
   1.145 +apply (rule monofun_pair)
   1.146 +apply (rule is_lub_thelub)
   1.147 +apply (erule monofun_fst [THEN ch2ch_monofun])
   1.148 +apply (erule monofun_fst [THEN ub2ub_monofun])
   1.149 +apply (rule is_lub_thelub)
   1.150 +apply (erule monofun_snd [THEN ch2ch_monofun])
   1.151 +apply (erule monofun_snd [THEN ub2ub_monofun])
   1.152 +done
   1.153 +
   1.154 +lemmas thelub_cprod = lub_cprod [THEN thelubI, standard]
   1.155 +(*
   1.156 +"chain ?S1 ==>
   1.157 + lub (range ?S1) =
   1.158 + (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
   1.159 +
   1.160 +*)
   1.161 +
   1.162 +lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x"
   1.163 +apply (rule exI)
   1.164 +apply (erule lub_cprod)
   1.165 +done
   1.166 +
   1.167 +(* Class instance of * for class pcpo and cpo. *)
   1.168 +
   1.169 +instance "*" :: (cpo,cpo)cpo
   1.170 +by (intro_classes, rule cpo_cprod)
   1.171 +
   1.172 +instance "*" :: (pcpo,pcpo)pcpo
   1.173 +by (intro_classes, rule least_cprod)
   1.174 +
   1.175 +consts
   1.176 +        cpair        :: "'a::cpo -> 'b::cpo -> ('a*'b)" (* continuous pairing *)
   1.177 +        cfst         :: "('a::cpo*'b::cpo)->'a"
   1.178 +        csnd         :: "('a::cpo*'b::cpo)->'b"
   1.179 +        csplit       :: "('a::cpo->'b::cpo->'c::cpo)->('a*'b)->'c"
   1.180 +
   1.181 +syntax
   1.182 +        "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
   1.183 +
   1.184 +translations
   1.185 +        "<x, y, z>"   == "<x, <y, z>>"
   1.186 +        "<x, y>"      == "cpair$x$y"
   1.187 +
   1.188 +defs
   1.189 +cpair_def:       "cpair  == (LAM x y.(x,y))"
   1.190 +cfst_def:        "cfst   == (LAM p. fst(p))"
   1.191 +csnd_def:        "csnd   == (LAM p. snd(p))"      
   1.192 +csplit_def:      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
   1.193 +
   1.194 +
   1.195 +
   1.196 +(* introduce syntax for
   1.197 +
   1.198 +   Let <x,y> = e1; z = E2 in E3
   1.199 +
   1.200 +   and
   1.201 +
   1.202 +   LAM <x,y,z>.e
   1.203 +*)
   1.204 +
   1.205 +constdefs
   1.206 +  CLet           :: "'a -> ('a -> 'b) -> 'b"
   1.207 +  "CLet == LAM s f. f$s"
   1.208 +
   1.209 +
   1.210 +(* syntax for Let *)
   1.211 +
   1.212 +nonterminals
   1.213 +  Cletbinds  Cletbind
   1.214 +
   1.215 +syntax
   1.216 +  "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
   1.217 +  ""        :: "Cletbind => Cletbinds"               ("_")
   1.218 +  "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
   1.219 +  "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
   1.220 +
   1.221 +translations
   1.222 +  "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
   1.223 +  "Let x = a in e"          == "CLet$a$(LAM x. e)"
   1.224 +
   1.225 +
   1.226 +(* syntax for LAM <x,y,z>.e *)
   1.227 +
   1.228 +syntax
   1.229 +  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
   1.230 +
   1.231 +translations
   1.232 +  "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
   1.233 +  "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
   1.234 +  "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
   1.235 +
   1.236 +syntax (xsymbols)
   1.237 +  "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\\<Lambda>()<_>./ _)" [0, 10] 10)
   1.238 +
   1.239 +(* for compatibility with old HOLCF-Version *)
   1.240 +lemma inst_cprod_pcpo: "UU = (UU,UU)"
   1.241 +apply (simp add: UU_cprod_def[folded UU_def])
   1.242 +done
   1.243 +
   1.244 +(* ------------------------------------------------------------------------ *)
   1.245 +(* continuity of (_,_) , fst, snd                                           *)
   1.246 +(* ------------------------------------------------------------------------ *)
   1.247 +
   1.248 +lemma Cprod3_lemma1: 
   1.249 +"chain(Y::(nat=>'a::cpo)) ==> 
   1.250 +  (lub(range(Y)),(x::'b::cpo)) = 
   1.251 +  (lub(range(%i. fst(Y i,x))),lub(range(%i. snd(Y i,x))))"
   1.252 +apply (rule_tac f1 = "Pair" in arg_cong [THEN cong])
   1.253 +apply (rule lub_equal)
   1.254 +apply assumption
   1.255 +apply (rule monofun_fst [THEN ch2ch_monofun])
   1.256 +apply (rule ch2ch_fun)
   1.257 +apply (rule monofun_pair1 [THEN ch2ch_monofun])
   1.258 +apply assumption
   1.259 +apply (rule allI)
   1.260 +apply (simp (no_asm))
   1.261 +apply (rule sym)
   1.262 +apply (simp (no_asm))
   1.263 +apply (rule lub_const [THEN thelubI])
   1.264 +done
   1.265 +
   1.266 +lemma contlub_pair1: "contlub(Pair)"
   1.267 +apply (rule contlubI)
   1.268 +apply (intro strip)
   1.269 +apply (rule expand_fun_eq [THEN iffD2])
   1.270 +apply (intro strip)
   1.271 +apply (subst lub_fun [THEN thelubI])
   1.272 +apply (erule monofun_pair1 [THEN ch2ch_monofun])
   1.273 +apply (rule trans)
   1.274 +apply (rule_tac [2] thelub_cprod [symmetric])
   1.275 +apply (rule_tac [2] ch2ch_fun)
   1.276 +apply (erule_tac [2] monofun_pair1 [THEN ch2ch_monofun])
   1.277 +apply (erule Cprod3_lemma1)
   1.278 +done
   1.279 +
   1.280 +lemma Cprod3_lemma2: 
   1.281 +"chain(Y::(nat=>'a::cpo)) ==> 
   1.282 +  ((x::'b::cpo),lub(range Y)) = 
   1.283 +  (lub(range(%i. fst(x,Y i))),lub(range(%i. snd(x, Y i))))"
   1.284 +apply (rule_tac f1 = "Pair" in arg_cong [THEN cong])
   1.285 +apply (rule sym)
   1.286 +apply (simp (no_asm))
   1.287 +apply (rule lub_const [THEN thelubI])
   1.288 +apply (rule lub_equal)
   1.289 +apply assumption
   1.290 +apply (rule monofun_snd [THEN ch2ch_monofun])
   1.291 +apply (rule monofun_pair2 [THEN ch2ch_monofun])
   1.292 +apply assumption
   1.293 +apply (rule allI)
   1.294 +apply (simp (no_asm))
   1.295 +done
   1.296 +
   1.297 +lemma contlub_pair2: "contlub(Pair(x))"
   1.298 +apply (rule contlubI)
   1.299 +apply (intro strip)
   1.300 +apply (rule trans)
   1.301 +apply (rule_tac [2] thelub_cprod [symmetric])
   1.302 +apply (erule_tac [2] monofun_pair2 [THEN ch2ch_monofun])
   1.303 +apply (erule Cprod3_lemma2)
   1.304 +done
   1.305 +
   1.306 +lemma cont_pair1: "cont(Pair)"
   1.307 +apply (rule monocontlub2cont)
   1.308 +apply (rule monofun_pair1)
   1.309 +apply (rule contlub_pair1)
   1.310 +done
   1.311 +
   1.312 +lemma cont_pair2: "cont(Pair(x))"
   1.313 +apply (rule monocontlub2cont)
   1.314 +apply (rule monofun_pair2)
   1.315 +apply (rule contlub_pair2)
   1.316 +done
   1.317 +
   1.318 +lemma contlub_fst: "contlub(fst)"
   1.319 +apply (rule contlubI)
   1.320 +apply (intro strip)
   1.321 +apply (subst lub_cprod [THEN thelubI])
   1.322 +apply assumption
   1.323 +apply (simp (no_asm))
   1.324 +done
   1.325 +
   1.326 +lemma contlub_snd: "contlub(snd)"
   1.327 +apply (rule contlubI)
   1.328 +apply (intro strip)
   1.329 +apply (subst lub_cprod [THEN thelubI])
   1.330 +apply assumption
   1.331 +apply (simp (no_asm))
   1.332 +done
   1.333 +
   1.334 +lemma cont_fst: "cont(fst)"
   1.335 +apply (rule monocontlub2cont)
   1.336 +apply (rule monofun_fst)
   1.337 +apply (rule contlub_fst)
   1.338 +done
   1.339 +
   1.340 +lemma cont_snd: "cont(snd)"
   1.341 +apply (rule monocontlub2cont)
   1.342 +apply (rule monofun_snd)
   1.343 +apply (rule contlub_snd)
   1.344 +done
   1.345 +
   1.346 +(* 
   1.347 + -------------------------------------------------------------------------- 
   1.348 + more lemmas for Cprod3.thy 
   1.349 + 
   1.350 + -------------------------------------------------------------------------- 
   1.351 +*)
   1.352 +
   1.353 +(* ------------------------------------------------------------------------ *)
   1.354 +(* convert all lemmas to the continuous versions                            *)
   1.355 +(* ------------------------------------------------------------------------ *)
   1.356 +
   1.357 +lemma beta_cfun_cprod: 
   1.358 +        "(LAM x y.(x,y))$a$b = (a,b)"
   1.359 +apply (subst beta_cfun)
   1.360 +apply (simp (no_asm) add: cont_pair1 cont_pair2 cont2cont_CF1L)
   1.361 +apply (subst beta_cfun)
   1.362 +apply (rule cont_pair2)
   1.363 +apply (rule refl)
   1.364 +done
   1.365 +
   1.366 +lemma inject_cpair: 
   1.367 +        "<a,b> = <aa,ba>  ==> a=aa & b=ba"
   1.368 +apply (unfold cpair_def)
   1.369 +apply (drule beta_cfun_cprod [THEN subst])
   1.370 +apply (drule beta_cfun_cprod [THEN subst])
   1.371 +apply (erule Pair_inject)
   1.372 +apply fast
   1.373 +done
   1.374 +
   1.375 +lemma inst_cprod_pcpo2: "UU = <UU,UU>"
   1.376 +apply (unfold cpair_def)
   1.377 +apply (rule sym)
   1.378 +apply (rule trans)
   1.379 +apply (rule beta_cfun_cprod)
   1.380 +apply (rule sym)
   1.381 +apply (rule inst_cprod_pcpo)
   1.382 +done
   1.383 +
   1.384 +lemma defined_cpair_rev: 
   1.385 + "<a,b> = UU ==> a = UU & b = UU"
   1.386 +apply (drule inst_cprod_pcpo2 [THEN subst])
   1.387 +apply (erule inject_cpair)
   1.388 +done
   1.389 +
   1.390 +lemma Exh_Cprod2:
   1.391 +        "? a b. z=<a,b>"
   1.392 +apply (unfold cpair_def)
   1.393 +apply (rule PairE)
   1.394 +apply (rule exI)
   1.395 +apply (rule exI)
   1.396 +apply (erule beta_cfun_cprod [THEN ssubst])
   1.397 +done
   1.398 +
   1.399 +lemma cprodE:
   1.400 +assumes prems: "!!x y. [| p = <x,y> |] ==> Q"
   1.401 +shows "Q"
   1.402 +apply (rule PairE)
   1.403 +apply (rule prems)
   1.404 +apply (unfold cpair_def)
   1.405 +apply (erule beta_cfun_cprod [THEN ssubst])
   1.406 +done
   1.407 +
   1.408 +lemma cfst2: 
   1.409 +        "cfst$<x,y> = x"
   1.410 +apply (unfold cfst_def cpair_def)
   1.411 +apply (subst beta_cfun_cprod)
   1.412 +apply (subst beta_cfun)
   1.413 +apply (rule cont_fst)
   1.414 +apply (simp (no_asm))
   1.415 +done
   1.416 +
   1.417 +lemma csnd2: 
   1.418 +        "csnd$<x,y> = y"
   1.419 +apply (unfold csnd_def cpair_def)
   1.420 +apply (subst beta_cfun_cprod)
   1.421 +apply (subst beta_cfun)
   1.422 +apply (rule cont_snd)
   1.423 +apply (simp (no_asm))
   1.424 +done
   1.425 +
   1.426 +lemma cfst_strict: "cfst$UU = UU"
   1.427 +apply (simp add: inst_cprod_pcpo2 cfst2)
   1.428 +done
   1.429 +
   1.430 +lemma csnd_strict: "csnd$UU = UU"
   1.431 +apply (simp add: inst_cprod_pcpo2 csnd2)
   1.432 +done
   1.433 +
   1.434 +lemma surjective_pairing_Cprod2: "<cfst$p , csnd$p> = p"
   1.435 +apply (unfold cfst_def csnd_def cpair_def)
   1.436 +apply (subst beta_cfun_cprod)
   1.437 +apply (simplesubst beta_cfun)
   1.438 +apply (rule cont_snd)
   1.439 +apply (subst beta_cfun)
   1.440 +apply (rule cont_fst)
   1.441 +apply (rule surjective_pairing [symmetric])
   1.442 +done
   1.443 +
   1.444 +lemma less_cprod5c: 
   1.445 + "<xa,ya> << <x,y> ==> xa<<x & ya << y"
   1.446 +apply (unfold cfst_def csnd_def cpair_def)
   1.447 +apply (rule less_cprod4c)
   1.448 +apply (drule beta_cfun_cprod [THEN subst])
   1.449 +apply (drule beta_cfun_cprod [THEN subst])
   1.450 +apply assumption
   1.451 +done
   1.452 +
   1.453 +lemma lub_cprod2: 
   1.454 +"[|chain(S)|] ==> range(S) <<|  
   1.455 +  <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>"
   1.456 +apply (unfold cfst_def csnd_def cpair_def)
   1.457 +apply (subst beta_cfun_cprod)
   1.458 +apply (simplesubst beta_cfun [THEN ext])
   1.459 +apply (rule cont_snd)
   1.460 +apply (subst beta_cfun [THEN ext])
   1.461 +apply (rule cont_fst)
   1.462 +apply (rule lub_cprod)
   1.463 +apply assumption
   1.464 +done
   1.465 +
   1.466 +lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard]
   1.467 +(*
   1.468 +chain ?S1 ==>
   1.469 + lub (range ?S1) =
   1.470 + <lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" 
   1.471 +*)
   1.472 +lemma csplit2: 
   1.473 +        "csplit$f$<x,y> = f$x$y"
   1.474 +apply (unfold csplit_def)
   1.475 +apply (subst beta_cfun)
   1.476 +apply (simp (no_asm))
   1.477 +apply (simp (no_asm) add: cfst2 csnd2)
   1.478 +done
   1.479 +
   1.480 +lemma csplit3: 
   1.481 +  "csplit$cpair$z=z"
   1.482 +apply (unfold csplit_def)
   1.483 +apply (subst beta_cfun)
   1.484 +apply (simp (no_asm))
   1.485 +apply (simp (no_asm) add: surjective_pairing_Cprod2)
   1.486 +done
   1.487 +
   1.488 +(* ------------------------------------------------------------------------ *)
   1.489 +(* install simplifier for Cprod                                             *)
   1.490 +(* ------------------------------------------------------------------------ *)
   1.491 +
   1.492 +declare cfst2 [simp] csnd2 [simp] csplit2 [simp]
   1.493 +
   1.494 +lemmas Cprod_rews = cfst2 csnd2 csplit2
   1.495 +
   1.496 +end