src/HOLCF/Cprod.thy
author huffman
Thu Oct 07 13:54:43 2010 -0700 (2010-10-07)
changeset 39985 310f98585107
parent 39974 b525988432e9
child 39986 38677db30cad
permissions -rw-r--r--
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
huffman@15600
     1
(*  Title:      HOLCF/Cprod.thy
huffman@15576
     2
    Author:     Franz Regensburger
huffman@15576
     3
*)
huffman@15576
     4
huffman@15576
     5
header {* The cpo of cartesian products *}
huffman@15576
     6
huffman@15577
     7
theory Cprod
huffman@39985
     8
imports Bifinite
huffman@15577
     9
begin
huffman@15576
    10
wenzelm@36452
    11
default_sort cpo
huffman@15576
    12
huffman@35900
    13
subsection {* Continuous case function for unit type *}
huffman@16008
    14
wenzelm@25131
    15
definition
wenzelm@25131
    16
  unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
wenzelm@25131
    17
  "unit_when = (\<Lambda> a _. a)"
huffman@16008
    18
huffman@18289
    19
translations
wenzelm@25131
    20
  "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
huffman@18289
    21
huffman@18289
    22
lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
huffman@18289
    23
by (simp add: unit_when_def)
huffman@18289
    24
huffman@35926
    25
subsection {* Continuous version of split function *}
huffman@17834
    26
wenzelm@25131
    27
definition
wenzelm@25131
    28
  csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
huffman@35922
    29
  "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
huffman@15576
    30
huffman@15576
    31
translations
huffman@35926
    32
  "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
huffman@17816
    33
huffman@15576
    34
huffman@15593
    35
subsection {* Convert all lemmas to the continuous versions *}
huffman@15576
    36
huffman@18077
    37
lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
huffman@18077
    38
by (simp add: csplit_def)
huffman@18077
    39
huffman@33399
    40
lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
huffman@35922
    41
by (simp add: csplit_def)
huffman@33399
    42
huffman@39985
    43
subsection {* Map operator for product type *}
huffman@39985
    44
huffman@39985
    45
definition
huffman@39985
    46
  cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
huffman@39985
    47
where
huffman@39985
    48
  "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
huffman@39985
    49
huffman@39985
    50
lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
huffman@39985
    51
unfolding cprod_map_def by simp
huffman@39985
    52
huffman@39985
    53
lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
huffman@39985
    54
unfolding expand_cfun_eq by auto
huffman@39985
    55
huffman@39985
    56
lemma cprod_map_map:
huffman@39985
    57
  "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
huffman@39985
    58
    cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
huffman@39985
    59
by (induct p) simp
huffman@39985
    60
huffman@39985
    61
lemma ep_pair_cprod_map:
huffman@39985
    62
  assumes "ep_pair e1 p1" and "ep_pair e2 p2"
huffman@39985
    63
  shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
huffman@39985
    64
proof
huffman@39985
    65
  interpret e1p1: ep_pair e1 p1 by fact
huffman@39985
    66
  interpret e2p2: ep_pair e2 p2 by fact
huffman@39985
    67
  fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
huffman@39985
    68
    by (induct x) simp
huffman@39985
    69
  fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
huffman@39985
    70
    by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
huffman@39985
    71
qed
huffman@39985
    72
huffman@39985
    73
lemma deflation_cprod_map:
huffman@39985
    74
  assumes "deflation d1" and "deflation d2"
huffman@39985
    75
  shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
huffman@39985
    76
proof
huffman@39985
    77
  interpret d1: deflation d1 by fact
huffman@39985
    78
  interpret d2: deflation d2 by fact
huffman@39985
    79
  fix x
huffman@39985
    80
  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>(cprod_map\<cdot>d1\<cdot>d2\<cdot>x) = cprod_map\<cdot>d1\<cdot>d2\<cdot>x"
huffman@39985
    81
    by (induct x) (simp add: d1.idem d2.idem)
huffman@39985
    82
  show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
huffman@39985
    83
    by (induct x) (simp add: d1.below d2.below)
huffman@39985
    84
qed
huffman@39985
    85
huffman@39985
    86
lemma finite_deflation_cprod_map:
huffman@39985
    87
  assumes "finite_deflation d1" and "finite_deflation d2"
huffman@39985
    88
  shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
huffman@39985
    89
proof (rule finite_deflation_intro)
huffman@39985
    90
  interpret d1: finite_deflation d1 by fact
huffman@39985
    91
  interpret d2: finite_deflation d2 by fact
huffman@39985
    92
  have "deflation d1" and "deflation d2" by fact+
huffman@39985
    93
  thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
huffman@39985
    94
  have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
huffman@39985
    95
    by clarsimp
huffman@39985
    96
  thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
huffman@39985
    97
    by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
huffman@39985
    98
qed
huffman@39985
    99
huffman@39974
   100
subsection {* Cartesian product is an SFP domain *}
huffman@39974
   101
huffman@39974
   102
definition
huffman@39974
   103
  prod_approx :: "nat \<Rightarrow> udom \<times> udom \<rightarrow> udom \<times> udom"
huffman@39974
   104
where
huffman@39974
   105
  "prod_approx = (\<lambda>i. cprod_map\<cdot>(udom_approx i)\<cdot>(udom_approx i))"
huffman@39974
   106
huffman@39974
   107
lemma prod_approx: "approx_chain prod_approx"
huffman@39974
   108
proof (rule approx_chain.intro)
huffman@39974
   109
  show "chain (\<lambda>i. prod_approx i)"
huffman@39974
   110
    unfolding prod_approx_def by simp
huffman@39974
   111
  show "(\<Squnion>i. prod_approx i) = ID"
huffman@39974
   112
    unfolding prod_approx_def
huffman@39974
   113
    by (simp add: lub_distribs cprod_map_ID)
huffman@39974
   114
  show "\<And>i. finite_deflation (prod_approx i)"
huffman@39974
   115
    unfolding prod_approx_def
huffman@39974
   116
    by (intro finite_deflation_cprod_map finite_deflation_udom_approx)
huffman@39974
   117
qed
huffman@39974
   118
huffman@39974
   119
definition prod_sfp :: "sfp \<rightarrow> sfp \<rightarrow> sfp"
huffman@39974
   120
where "prod_sfp = sfp_fun2 prod_approx cprod_map"
huffman@39974
   121
huffman@39974
   122
lemma cast_prod_sfp:
huffman@39974
   123
  "cast\<cdot>(prod_sfp\<cdot>A\<cdot>B) = udom_emb prod_approx oo
huffman@39974
   124
    cprod_map\<cdot>(cast\<cdot>A)\<cdot>(cast\<cdot>B) oo udom_prj prod_approx"
huffman@39974
   125
unfolding prod_sfp_def
huffman@39974
   126
apply (rule cast_sfp_fun2 [OF prod_approx])
huffman@39974
   127
apply (erule (1) finite_deflation_cprod_map)
huffman@39974
   128
done
huffman@39974
   129
huffman@39974
   130
instantiation prod :: (sfp, sfp) sfp
huffman@39974
   131
begin
huffman@39974
   132
huffman@39974
   133
definition
huffman@39974
   134
  "emb = udom_emb prod_approx oo cprod_map\<cdot>emb\<cdot>emb"
huffman@39974
   135
huffman@39974
   136
definition
huffman@39974
   137
  "prj = cprod_map\<cdot>prj\<cdot>prj oo udom_prj prod_approx"
huffman@39974
   138
huffman@39974
   139
definition
huffman@39974
   140
  "sfp (t::('a \<times> 'b) itself) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
huffman@39974
   141
huffman@39974
   142
instance proof
huffman@39974
   143
  show "ep_pair emb (prj :: udom \<rightarrow> 'a \<times> 'b)"
huffman@39974
   144
    unfolding emb_prod_def prj_prod_def
huffman@39974
   145
    using ep_pair_udom [OF prod_approx]
huffman@39974
   146
    by (intro ep_pair_comp ep_pair_cprod_map ep_pair_emb_prj)
huffman@39974
   147
next
huffman@39974
   148
  show "cast\<cdot>SFP('a \<times> 'b) = emb oo (prj :: udom \<rightarrow> 'a \<times> 'b)"
huffman@39974
   149
    unfolding emb_prod_def prj_prod_def sfp_prod_def cast_prod_sfp
huffman@39974
   150
    by (simp add: cast_SFP oo_def expand_cfun_eq cprod_map_map)
huffman@39974
   151
qed
huffman@39974
   152
huffman@15576
   153
end
huffman@39974
   154
huffman@39974
   155
lemma SFP_prod: "SFP('a::sfp \<times> 'b::sfp) = prod_sfp\<cdot>SFP('a)\<cdot>SFP('b)"
huffman@39974
   156
by (rule sfp_prod_def)
huffman@39974
   157
huffman@39974
   158
end