src/HOLCF/Cprod.thy
author wenzelm
Wed May 25 09:44:34 2005 +0200 (2005-05-25)
changeset 16070 4a83dd540b88
parent 16057 e23a61b3406f
child 16081 81a4b4a245b0
permissions -rw-r--r--
removed LICENCE note -- everything is subject to Isabelle licence as
stated in COPYRIGHT file;
     1 (*  Title:      HOLCF/Cprod.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 
     5 Partial ordering for cartesian product of HOL products.
     6 *)
     7 
     8 header {* The cpo of cartesian products *}
     9 
    10 theory Cprod
    11 imports Cfun
    12 begin
    13 
    14 defaultsort cpo
    15 
    16 subsection {* Type @{typ unit} is a pcpo *}
    17 
    18 instance unit :: sq_ord ..
    19 
    20 defs (overloaded)
    21   less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
    22 
    23 instance unit :: po
    24 by intro_classes simp_all
    25 
    26 instance unit :: cpo
    27 by intro_classes (simp add: is_lub_def is_ub_def)
    28 
    29 instance unit :: pcpo
    30 by intro_classes simp
    31 
    32 
    33 subsection {* Ordering on @{typ "'a * 'b"} *}
    34 
    35 instance "*" :: (sq_ord, sq_ord) sq_ord ..
    36 
    37 defs (overloaded)
    38   less_cprod_def: "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
    39 
    40 subsection {* Type @{typ "'a * 'b"} is a partial order *}
    41 
    42 lemma refl_less_cprod: "(p::'a*'b) << p"
    43 apply (unfold less_cprod_def)
    44 apply simp
    45 done
    46 
    47 lemma antisym_less_cprod: "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
    48 apply (unfold less_cprod_def)
    49 apply (rule injective_fst_snd)
    50 apply (fast intro: antisym_less)
    51 apply (fast intro: antisym_less)
    52 done
    53 
    54 lemma trans_less_cprod: 
    55         "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
    56 apply (unfold less_cprod_def)
    57 apply (rule conjI)
    58 apply (fast intro: trans_less)
    59 apply (fast intro: trans_less)
    60 done
    61 
    62 defaultsort pcpo
    63 
    64 instance "*" :: (cpo, cpo) po
    65 by intro_classes
    66   (assumption | rule refl_less_cprod antisym_less_cprod trans_less_cprod)+
    67 
    68 text {* for compatibility with old HOLCF-Version *}
    69 lemma inst_cprod_po: "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
    70 apply (fold less_cprod_def)
    71 apply (rule refl)
    72 done
    73 
    74 lemma less_cprod4c: "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"
    75 apply (simp add: inst_cprod_po)
    76 done
    77 
    78 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    79 
    80 text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
    81 
    82 lemma monofun_pair1: "monofun Pair"
    83 by (simp add: monofun less_fun inst_cprod_po)
    84 
    85 lemma monofun_pair2: "monofun(Pair x)"
    86 by (simp add: monofun inst_cprod_po)
    87 
    88 lemma monofun_pair: "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
    89 by (simp add: inst_cprod_po)
    90 
    91 text {* @{term fst} and @{term snd} are monotone *}
    92 
    93 lemma monofun_fst: "monofun fst"
    94 by (simp add: monofun inst_cprod_po)
    95 
    96 lemma monofun_snd: "monofun snd"
    97 by (simp add: monofun inst_cprod_po)
    98 
    99 subsection {* Type @{typ "'a * 'b"} is a cpo *}
   100 
   101 lemma lub_cprod: 
   102 "chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
   103 apply (rule is_lubI)
   104 apply (rule ub_rangeI)
   105 apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
   106 apply (rule monofun_pair)
   107 apply (rule is_ub_thelub)
   108 apply (erule monofun_fst [THEN ch2ch_monofun])
   109 apply (rule is_ub_thelub)
   110 apply (erule monofun_snd [THEN ch2ch_monofun])
   111 apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
   112 apply (rule monofun_pair)
   113 apply (rule is_lub_thelub)
   114 apply (erule monofun_fst [THEN ch2ch_monofun])
   115 apply (erule monofun_fst [THEN ub2ub_monofun])
   116 apply (rule is_lub_thelub)
   117 apply (erule monofun_snd [THEN ch2ch_monofun])
   118 apply (erule monofun_snd [THEN ub2ub_monofun])
   119 done
   120 
   121 lemmas thelub_cprod = lub_cprod [THEN thelubI, standard]
   122 (*
   123 "chain ?S1 ==>
   124  lub (range ?S1) =
   125  (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
   126 
   127 *)
   128 
   129 lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x"
   130 by (rule exI, erule lub_cprod)
   131 
   132 instance "*" :: (cpo, cpo) cpo
   133 by intro_classes (rule cpo_cprod)
   134 
   135 subsection {* Type @{typ "'a * 'b"} is pointed *}
   136 
   137 lemma minimal_cprod: "(UU,UU)<<p"
   138 by (simp add: inst_cprod_po)
   139 
   140 lemmas UU_cprod_def = minimal_cprod [THEN minimal2UU, symmetric, standard]
   141 
   142 lemma least_cprod: "EX x::'a*'b. ALL y. x<<y"
   143 apply (rule_tac x = " (UU,UU) " in exI)
   144 apply (rule minimal_cprod [THEN allI])
   145 done
   146 
   147 instance "*" :: (pcpo, pcpo) pcpo
   148 by intro_classes (rule least_cprod)
   149 
   150 text {* for compatibility with old HOLCF-Version *}
   151 lemma inst_cprod_pcpo: "UU = (UU,UU)"
   152 apply (simp add: UU_cprod_def[folded UU_def])
   153 done
   154 
   155 subsection {* Continuity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
   156 
   157 lemma contlub_pair1: "contlub(Pair)"
   158 apply (rule contlubI [rule_format])
   159 apply (rule ext)
   160 apply (subst lub_fun [THEN thelubI])
   161 apply (erule monofun_pair1 [THEN ch2ch_monofun])
   162 apply (subst thelub_cprod)
   163 apply (rule ch2ch_fun)
   164 apply (erule monofun_pair1 [THEN ch2ch_monofun])
   165 apply (simp add: lub_const [THEN thelubI])
   166 done
   167 
   168 lemma contlub_pair2: "contlub(Pair(x))"
   169 apply (rule contlubI [rule_format])
   170 apply (subst thelub_cprod)
   171 apply (erule monofun_pair2 [THEN ch2ch_monofun])
   172 apply (simp add: lub_const [THEN thelubI])
   173 done
   174 
   175 lemma cont_pair1: "cont(Pair)"
   176 apply (rule monocontlub2cont)
   177 apply (rule monofun_pair1)
   178 apply (rule contlub_pair1)
   179 done
   180 
   181 lemma cont_pair2: "cont(Pair(x))"
   182 apply (rule monocontlub2cont)
   183 apply (rule monofun_pair2)
   184 apply (rule contlub_pair2)
   185 done
   186 
   187 lemma contlub_fst: "contlub(fst)"
   188 apply (rule contlubI [rule_format])
   189 apply (simp add: lub_cprod [THEN thelubI])
   190 done
   191 
   192 lemma contlub_snd: "contlub(snd)"
   193 apply (rule contlubI [rule_format])
   194 apply (simp add: lub_cprod [THEN thelubI])
   195 done
   196 
   197 lemma cont_fst: "cont(fst)"
   198 apply (rule monocontlub2cont)
   199 apply (rule monofun_fst)
   200 apply (rule contlub_fst)
   201 done
   202 
   203 lemma cont_snd: "cont(snd)"
   204 apply (rule monocontlub2cont)
   205 apply (rule monofun_snd)
   206 apply (rule contlub_snd)
   207 done
   208 
   209 subsection {* Continuous versions of constants *}
   210 
   211 consts
   212         cpair        :: "'a::cpo -> 'b::cpo -> ('a*'b)" (* continuous pairing *)
   213         cfst         :: "('a::cpo*'b::cpo)->'a"
   214         csnd         :: "('a::cpo*'b::cpo)->'b"
   215         csplit       :: "('a::cpo->'b::cpo->'c::cpo)->('a*'b)->'c"
   216 
   217 syntax
   218         "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
   219 
   220 translations
   221         "<x, y, z>"   == "<x, <y, z>>"
   222         "<x, y>"      == "cpair$x$y"
   223 
   224 defs
   225 cpair_def:       "cpair  == (LAM x y.(x,y))"
   226 cfst_def:        "cfst   == (LAM p. fst(p))"
   227 csnd_def:        "csnd   == (LAM p. snd(p))"      
   228 csplit_def:      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
   229 
   230 subsection {* Syntax *}
   231 
   232 text {* syntax for @{text "LAM <x,y,z>.e"} *}
   233 
   234 syntax
   235   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
   236 
   237 translations
   238   "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
   239   "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
   240   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
   241 
   242 syntax (xsymbols)
   243   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
   244 
   245 text {* syntax for Let *}
   246 
   247 constdefs
   248   CLet           :: "'a::cpo -> ('a -> 'b::cpo) -> 'b"
   249   "CLet == LAM s f. f$s"
   250 
   251 nonterminals
   252   Cletbinds  Cletbind
   253 
   254 syntax
   255   "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
   256   "_Cbindp" :: "[patterns, 'a] => Cletbind"          ("(2<_> =/ _)" 10)
   257   ""        :: "Cletbind => Cletbinds"               ("_")
   258   "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
   259   "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
   260 
   261 translations
   262   "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
   263   "Let x = a in LAM ys. e"  == "CLet$a$(LAM x ys. e)"
   264   "Let x = a in e"          == "CLet$a$(LAM x. e)"
   265   "Let <xs> = a in e"       == "CLet$a$(LAM <xs>. e)"
   266 
   267 subsection {* Convert all lemmas to the continuous versions *}
   268 
   269 lemma beta_cfun_cprod: 
   270         "(LAM x y.(x,y))$a$b = (a,b)"
   271 apply (subst beta_cfun)
   272 apply (simp add: cont_pair1 cont_pair2 cont2cont_CF1L)
   273 apply (subst beta_cfun)
   274 apply (rule cont_pair2)
   275 apply (rule refl)
   276 done
   277 
   278 lemma inject_cpair: 
   279         "<a,b> = <aa,ba>  ==> a=aa & b=ba"
   280 by (simp add: cpair_def beta_cfun_cprod)
   281 
   282 lemma cpair_eq [iff]: "(<a, b> = <a', b'>) = (a = a' & b = b')"
   283 by (blast dest!: inject_cpair)
   284 
   285 lemma inst_cprod_pcpo2: "UU = <UU,UU>"
   286 by (simp add: cpair_def beta_cfun_cprod inst_cprod_pcpo)
   287 
   288 lemma defined_cpair_rev: 
   289  "<a,b> = UU ==> a = UU & b = UU"
   290 apply (drule inst_cprod_pcpo2 [THEN subst])
   291 apply (erule inject_cpair)
   292 done
   293 
   294 lemma Exh_Cprod2: "? a b. z=<a,b>"
   295 apply (unfold cpair_def)
   296 apply (rule PairE)
   297 apply (rule exI)
   298 apply (rule exI)
   299 apply (erule beta_cfun_cprod [THEN ssubst])
   300 done
   301 
   302 lemma cprodE:
   303 assumes prems: "!!x y. [| p = <x,y> |] ==> Q"
   304 shows "Q"
   305 apply (rule PairE)
   306 apply (rule prems)
   307 apply (simp add: cpair_def beta_cfun_cprod)
   308 done
   309 
   310 lemma cfst2 [simp]: "cfst$<x,y> = x"
   311 by (simp add: cpair_def cfst_def beta_cfun_cprod cont_fst)
   312 
   313 lemma csnd2 [simp]: "csnd$<x,y> = y"
   314 by (simp add: cpair_def csnd_def beta_cfun_cprod cont_snd)
   315 
   316 lemma cfst_strict [simp]: "cfst$UU = UU"
   317 by (simp add: inst_cprod_pcpo2)
   318 
   319 lemma csnd_strict [simp]: "csnd$UU = UU"
   320 by (simp add: inst_cprod_pcpo2)
   321 
   322 lemma surjective_pairing_Cprod2: "<cfst$p, csnd$p> = p"
   323 apply (unfold cfst_def csnd_def cpair_def)
   324 apply (simp add: cont_fst cont_snd beta_cfun_cprod)
   325 done
   326 
   327 lemma less_cprod5c: 
   328  "<xa,ya> << <x,y> ==> xa<<x & ya << y"
   329 by (simp add: cpair_def beta_cfun_cprod inst_cprod_po)
   330 
   331 lemma lub_cprod2: 
   332 "[|chain(S)|] ==> range(S) <<|  
   333   <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>"
   334 apply (simp add: cpair_def beta_cfun_cprod)
   335 apply (simp add: cfst_def csnd_def cont_fst cont_snd)
   336 apply (erule lub_cprod)
   337 done
   338 
   339 lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard]
   340 (*
   341 chain ?S1 ==>
   342  lub (range ?S1) =
   343  <lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" 
   344 *)
   345 
   346 lemma csplit2 [simp]: "csplit$f$<x,y> = f$x$y"
   347 by (simp add: csplit_def)
   348 
   349 lemma csplit3: "csplit$cpair$z=z"
   350 by (simp add: csplit_def surjective_pairing_Cprod2)
   351 
   352 lemmas Cprod_rews = cfst2 csnd2 csplit2
   353 
   354 end