src/HOLCF/Cprod.thy
author huffman
Mon Mar 14 20:30:43 2005 +0100 (2005-03-14)
changeset 15609 d12c459e2325
parent 15600 a59f07556a8d
child 16008 861a255cf1e7
permissions -rw-r--r--
fixed syntax for Let <x,y> = a in e
     1 (*  Title:      HOLCF/Cprod.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Partial ordering for cartesian product of HOL theory prod.thy
     7 *)
     8 
     9 header {* The cpo of cartesian products *}
    10 
    11 theory Cprod
    12 imports Cfun
    13 begin
    14 
    15 defaultsort cpo
    16 
    17 subsection {* Ordering on @{typ "'a * 'b"} *}
    18 
    19 instance "*" :: (sq_ord, sq_ord) sq_ord ..
    20 
    21 defs (overloaded)
    22   less_cprod_def: "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
    23 
    24 subsection {* Type @{typ "'a * 'b"} is a partial order *}
    25 
    26 lemma refl_less_cprod: "(p::'a*'b) << p"
    27 apply (unfold less_cprod_def)
    28 apply simp
    29 done
    30 
    31 lemma antisym_less_cprod: "[|(p1::'a * 'b) << p2;p2 << p1|] ==> p1=p2"
    32 apply (unfold less_cprod_def)
    33 apply (rule injective_fst_snd)
    34 apply (fast intro: antisym_less)
    35 apply (fast intro: antisym_less)
    36 done
    37 
    38 lemma trans_less_cprod: 
    39         "[|(p1::'a*'b) << p2;p2 << p3|] ==> p1 << p3"
    40 apply (unfold less_cprod_def)
    41 apply (rule conjI)
    42 apply (fast intro: trans_less)
    43 apply (fast intro: trans_less)
    44 done
    45 
    46 defaultsort pcpo
    47 
    48 instance "*" :: (cpo, cpo) po
    49 by intro_classes
    50   (assumption | rule refl_less_cprod antisym_less_cprod trans_less_cprod)+
    51 
    52 text {* for compatibility with old HOLCF-Version *}
    53 lemma inst_cprod_po: "(op <<)=(%x y. fst x<<fst y & snd x<<snd y)"
    54 apply (fold less_cprod_def)
    55 apply (rule refl)
    56 done
    57 
    58 lemma less_cprod4c: "(x1,y1) << (x2,y2) ==> x1 << x2 & y1 << y2"
    59 apply (simp add: inst_cprod_po)
    60 done
    61 
    62 subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    63 
    64 text {* Pair @{text "(_,_)"}  is monotone in both arguments *}
    65 
    66 lemma monofun_pair1: "monofun Pair"
    67 by (simp add: monofun less_fun inst_cprod_po)
    68 
    69 lemma monofun_pair2: "monofun(Pair x)"
    70 by (simp add: monofun inst_cprod_po)
    71 
    72 lemma monofun_pair: "[|x1<<x2; y1<<y2|] ==> (x1::'a::cpo,y1::'b::cpo)<<(x2,y2)"
    73 by (simp add: inst_cprod_po)
    74 
    75 text {* @{term fst} and @{term snd} are monotone *}
    76 
    77 lemma monofun_fst: "monofun fst"
    78 by (simp add: monofun inst_cprod_po)
    79 
    80 lemma monofun_snd: "monofun snd"
    81 by (simp add: monofun inst_cprod_po)
    82 
    83 subsection {* Type @{typ "'a * 'b"} is a cpo *}
    84 
    85 lemma lub_cprod: 
    86 "chain S ==> range S<<|(lub(range(%i. fst(S i))),lub(range(%i. snd(S i))))"
    87 apply (rule is_lubI)
    88 apply (rule ub_rangeI)
    89 apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
    90 apply (rule monofun_pair)
    91 apply (rule is_ub_thelub)
    92 apply (erule monofun_fst [THEN ch2ch_monofun])
    93 apply (rule is_ub_thelub)
    94 apply (erule monofun_snd [THEN ch2ch_monofun])
    95 apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
    96 apply (rule monofun_pair)
    97 apply (rule is_lub_thelub)
    98 apply (erule monofun_fst [THEN ch2ch_monofun])
    99 apply (erule monofun_fst [THEN ub2ub_monofun])
   100 apply (rule is_lub_thelub)
   101 apply (erule monofun_snd [THEN ch2ch_monofun])
   102 apply (erule monofun_snd [THEN ub2ub_monofun])
   103 done
   104 
   105 lemmas thelub_cprod = lub_cprod [THEN thelubI, standard]
   106 (*
   107 "chain ?S1 ==>
   108  lub (range ?S1) =
   109  (lub (range (%i. fst (?S1 i))), lub (range (%i. snd (?S1 i))))" : thm
   110 
   111 *)
   112 
   113 lemma cpo_cprod: "chain(S::nat=>'a::cpo*'b::cpo)==>EX x. range S<<| x"
   114 by (rule exI, erule lub_cprod)
   115 
   116 instance "*" :: (cpo, cpo) cpo
   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
   130 
   131 instance "*" :: (pcpo, pcpo) pcpo
   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 *}
   194 
   195 consts
   196         cpair        :: "'a::cpo -> 'b::cpo -> ('a*'b)" (* continuous pairing *)
   197         cfst         :: "('a::cpo*'b::cpo)->'a"
   198         csnd         :: "('a::cpo*'b::cpo)->'b"
   199         csplit       :: "('a::cpo->'b::cpo->'c::cpo)->('a*'b)->'c"
   200 
   201 syntax
   202         "@ctuple"    :: "['a, args] => 'a * 'b"         ("(1<_,/ _>)")
   203 
   204 translations
   205         "<x, y, z>"   == "<x, <y, z>>"
   206         "<x, y>"      == "cpair$x$y"
   207 
   208 defs
   209 cpair_def:       "cpair  == (LAM x y.(x,y))"
   210 cfst_def:        "cfst   == (LAM p. fst(p))"
   211 csnd_def:        "csnd   == (LAM p. snd(p))"      
   212 csplit_def:      "csplit == (LAM f p. f$(cfst$p)$(csnd$p))"
   213 
   214 subsection {* Syntax *}
   215 
   216 text {* syntax for @{text "LAM <x,y,z>.e"} *}
   217 
   218 syntax
   219   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3LAM <_>./ _)" [0, 10] 10)
   220 
   221 translations
   222   "LAM <x,y,zs>.b"        == "csplit$(LAM x. LAM <y,zs>.b)"
   223   "LAM <x,y>. LAM zs. b"  <= "csplit$(LAM x y zs. b)"
   224   "LAM <x,y>.b"           == "csplit$(LAM x y. b)"
   225 
   226 syntax (xsymbols)
   227   "_LAM"    :: "[patterns, 'a => 'b] => ('a -> 'b)"  ("(3\<Lambda>()<_>./ _)" [0, 10] 10)
   228 
   229 text {* syntax for Let *}
   230 
   231 constdefs
   232   CLet           :: "'a::cpo -> ('a -> 'b::cpo) -> 'b"
   233   "CLet == LAM s f. f$s"
   234 
   235 nonterminals
   236   Cletbinds  Cletbind
   237 
   238 syntax
   239   "_Cbind"  :: "[pttrn, 'a] => Cletbind"             ("(2_ =/ _)" 10)
   240   "_Cbindp" :: "[patterns, 'a] => Cletbind"          ("(2<_> =/ _)" 10)
   241   ""        :: "Cletbind => Cletbinds"               ("_")
   242   "_Cbinds" :: "[Cletbind, Cletbinds] => Cletbinds"  ("_;/ _")
   243   "_CLet"   :: "[Cletbinds, 'a] => 'a"               ("(Let (_)/ in (_))" 10)
   244 
   245 translations
   246   "_CLet (_Cbinds b bs) e"  == "_CLet b (_CLet bs e)"
   247   "Let x = a in LAM ys. e"  == "CLet$a$(LAM x ys. e)"
   248   "Let x = a in e"          == "CLet$a$(LAM x. e)"
   249   "Let <xs> = a in e"       == "CLet$a$(LAM <xs>. e)"
   250 
   251 subsection {* Convert all lemmas to the continuous versions *}
   252 
   253 lemma beta_cfun_cprod: 
   254         "(LAM x y.(x,y))$a$b = (a,b)"
   255 apply (subst beta_cfun)
   256 apply (simp add: cont_pair1 cont_pair2 cont2cont_CF1L)
   257 apply (subst beta_cfun)
   258 apply (rule cont_pair2)
   259 apply (rule refl)
   260 done
   261 
   262 lemma inject_cpair: 
   263         "<a,b> = <aa,ba>  ==> a=aa & b=ba"
   264 by (simp add: cpair_def beta_cfun_cprod)
   265 
   266 lemma inst_cprod_pcpo2: "UU = <UU,UU>"
   267 by (simp add: cpair_def beta_cfun_cprod inst_cprod_pcpo)
   268 
   269 lemma defined_cpair_rev: 
   270  "<a,b> = UU ==> a = UU & b = UU"
   271 apply (drule inst_cprod_pcpo2 [THEN subst])
   272 apply (erule inject_cpair)
   273 done
   274 
   275 lemma Exh_Cprod2: "? a b. z=<a,b>"
   276 apply (unfold cpair_def)
   277 apply (rule PairE)
   278 apply (rule exI)
   279 apply (rule exI)
   280 apply (erule beta_cfun_cprod [THEN ssubst])
   281 done
   282 
   283 lemma cprodE:
   284 assumes prems: "!!x y. [| p = <x,y> |] ==> Q"
   285 shows "Q"
   286 apply (rule PairE)
   287 apply (rule prems)
   288 apply (simp add: cpair_def beta_cfun_cprod)
   289 done
   290 
   291 lemma cfst2 [simp]: "cfst$<x,y> = x"
   292 by (simp add: cpair_def cfst_def beta_cfun_cprod cont_fst)
   293 
   294 lemma csnd2 [simp]: "csnd$<x,y> = y"
   295 by (simp add: cpair_def csnd_def beta_cfun_cprod cont_snd)
   296 
   297 lemma cfst_strict: "cfst$UU = UU"
   298 by (simp add: inst_cprod_pcpo2)
   299 
   300 lemma csnd_strict: "csnd$UU = UU"
   301 by (simp add: inst_cprod_pcpo2)
   302 
   303 lemma surjective_pairing_Cprod2: "<cfst$p, csnd$p> = p"
   304 apply (unfold cfst_def csnd_def cpair_def)
   305 apply (simp add: cont_fst cont_snd beta_cfun_cprod)
   306 done
   307 
   308 lemma less_cprod5c: 
   309  "<xa,ya> << <x,y> ==> xa<<x & ya << y"
   310 by (simp add: cpair_def beta_cfun_cprod inst_cprod_po)
   311 
   312 lemma lub_cprod2: 
   313 "[|chain(S)|] ==> range(S) <<|  
   314   <(lub(range(%i. cfst$(S i)))) , lub(range(%i. csnd$(S i)))>"
   315 apply (simp add: cpair_def beta_cfun_cprod)
   316 apply (simp add: cfst_def csnd_def cont_fst cont_snd)
   317 apply (erule lub_cprod)
   318 done
   319 
   320 lemmas thelub_cprod2 = lub_cprod2 [THEN thelubI, standard]
   321 (*
   322 chain ?S1 ==>
   323  lub (range ?S1) =
   324  <lub (range (%i. cfst$(?S1 i))), lub (range (%i. csnd$(?S1 i)))>" 
   325 *)
   326 
   327 lemma csplit2 [simp]: "csplit$f$<x,y> = f$x$y"
   328 by (simp add: csplit_def)
   329 
   330 lemma csplit3: "csplit$cpair$z=z"
   331 by (simp add: csplit_def surjective_pairing_Cprod2)
   332 
   333 lemmas Cprod_rews = cfst2 csnd2 csplit2
   334 
   335 end