src/HOLCF/Cprod.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 40002 c5b5f7a3a3b1
child 40502 8e92772bc0e8
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/Cprod.thy
     2     Author:     Franz Regensburger
     3 *)
     4 
     5 header {* The cpo of cartesian products *}
     6 
     7 theory Cprod
     8 imports Deflation
     9 begin
    10 
    11 default_sort cpo
    12 
    13 subsection {* Continuous case function for unit type *}
    14 
    15 definition
    16   unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where
    17   "unit_when = (\<Lambda> a _. a)"
    18 
    19 translations
    20   "\<Lambda>(). t" == "CONST unit_when\<cdot>t"
    21 
    22 lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    23 by (simp add: unit_when_def)
    24 
    25 subsection {* Continuous version of split function *}
    26 
    27 definition
    28   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
    29   "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
    30 
    31 translations
    32   "\<Lambda>(CONST Pair x y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
    33 
    34 
    35 subsection {* Convert all lemmas to the continuous versions *}
    36 
    37 lemma csplit1 [simp]: "csplit\<cdot>f\<cdot>\<bottom> = f\<cdot>\<bottom>\<cdot>\<bottom>"
    38 by (simp add: csplit_def)
    39 
    40 lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
    41 by (simp add: csplit_def)
    42 
    43 subsection {* Map operator for product type *}
    44 
    45 definition
    46   cprod_map :: "('a \<rightarrow> 'b) \<rightarrow> ('c \<rightarrow> 'd) \<rightarrow> 'a \<times> 'c \<rightarrow> 'b \<times> 'd"
    47 where
    48   "cprod_map = (\<Lambda> f g p. (f\<cdot>(fst p), g\<cdot>(snd p)))"
    49 
    50 lemma cprod_map_Pair [simp]: "cprod_map\<cdot>f\<cdot>g\<cdot>(x, y) = (f\<cdot>x, g\<cdot>y)"
    51 unfolding cprod_map_def by simp
    52 
    53 lemma cprod_map_ID: "cprod_map\<cdot>ID\<cdot>ID = ID"
    54 unfolding cfun_eq_iff by auto
    55 
    56 lemma cprod_map_map:
    57   "cprod_map\<cdot>f1\<cdot>g1\<cdot>(cprod_map\<cdot>f2\<cdot>g2\<cdot>p) =
    58     cprod_map\<cdot>(\<Lambda> x. f1\<cdot>(f2\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
    59 by (induct p) simp
    60 
    61 lemma ep_pair_cprod_map:
    62   assumes "ep_pair e1 p1" and "ep_pair e2 p2"
    63   shows "ep_pair (cprod_map\<cdot>e1\<cdot>e2) (cprod_map\<cdot>p1\<cdot>p2)"
    64 proof
    65   interpret e1p1: ep_pair e1 p1 by fact
    66   interpret e2p2: ep_pair e2 p2 by fact
    67   fix x show "cprod_map\<cdot>p1\<cdot>p2\<cdot>(cprod_map\<cdot>e1\<cdot>e2\<cdot>x) = x"
    68     by (induct x) simp
    69   fix y show "cprod_map\<cdot>e1\<cdot>e2\<cdot>(cprod_map\<cdot>p1\<cdot>p2\<cdot>y) \<sqsubseteq> y"
    70     by (induct y) (simp add: e1p1.e_p_below e2p2.e_p_below)
    71 qed
    72 
    73 lemma deflation_cprod_map:
    74   assumes "deflation d1" and "deflation d2"
    75   shows "deflation (cprod_map\<cdot>d1\<cdot>d2)"
    76 proof
    77   interpret d1: deflation d1 by fact
    78   interpret d2: deflation d2 by fact
    79   fix x
    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"
    81     by (induct x) (simp add: d1.idem d2.idem)
    82   show "cprod_map\<cdot>d1\<cdot>d2\<cdot>x \<sqsubseteq> x"
    83     by (induct x) (simp add: d1.below d2.below)
    84 qed
    85 
    86 lemma finite_deflation_cprod_map:
    87   assumes "finite_deflation d1" and "finite_deflation d2"
    88   shows "finite_deflation (cprod_map\<cdot>d1\<cdot>d2)"
    89 proof (rule finite_deflation_intro)
    90   interpret d1: finite_deflation d1 by fact
    91   interpret d2: finite_deflation d2 by fact
    92   have "deflation d1" and "deflation d2" by fact+
    93   thus "deflation (cprod_map\<cdot>d1\<cdot>d2)" by (rule deflation_cprod_map)
    94   have "{p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p} \<subseteq> {x. d1\<cdot>x = x} \<times> {y. d2\<cdot>y = y}"
    95     by clarsimp
    96   thus "finite {p. cprod_map\<cdot>d1\<cdot>d2\<cdot>p = p}"
    97     by (rule finite_subset, simp add: d1.finite_fixes d2.finite_fixes)
    98 qed
    99 
   100 end