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