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