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