src/HOLCF/Domain.thy
author haftmann
Tue Jul 10 17:30:50 2007 +0200 (2007-07-10)
changeset 23709 fd31da8f752a
parent 23376 53317a1ec8b2
child 25806 2b976fcee6e5
permissions -rw-r--r--
moved lfp_induct2 here
     1 (*  Title:      HOLCF/Domain.thy
     2     ID:         $Id$
     3     Author:     Brian Huffman
     4 *)
     5 
     6 header {* Domain package *}
     7 
     8 theory Domain
     9 imports Ssum Sprod Up One Tr Fixrec
    10 begin
    11 
    12 defaultsort pcpo
    13 
    14 
    15 subsection {* Continuous isomorphisms *}
    16 
    17 text {* A locale for continuous isomorphisms *}
    18 
    19 locale iso =
    20   fixes abs :: "'a \<rightarrow> 'b"
    21   fixes rep :: "'b \<rightarrow> 'a"
    22   assumes abs_iso [simp]: "rep\<cdot>(abs\<cdot>x) = x"
    23   assumes rep_iso [simp]: "abs\<cdot>(rep\<cdot>y) = y"
    24 begin
    25 
    26 lemma swap: "iso rep abs"
    27   by (rule iso.intro [OF rep_iso abs_iso])
    28 
    29 lemma abs_less: "(abs\<cdot>x \<sqsubseteq> abs\<cdot>y) = (x \<sqsubseteq> y)"
    30 proof
    31   assume "abs\<cdot>x \<sqsubseteq> abs\<cdot>y"
    32   then have "rep\<cdot>(abs\<cdot>x) \<sqsubseteq> rep\<cdot>(abs\<cdot>y)" by (rule monofun_cfun_arg)
    33   then show "x \<sqsubseteq> y" by simp
    34 next
    35   assume "x \<sqsubseteq> y"
    36   then show "abs\<cdot>x \<sqsubseteq> abs\<cdot>y" by (rule monofun_cfun_arg)
    37 qed
    38 
    39 lemma rep_less: "(rep\<cdot>x \<sqsubseteq> rep\<cdot>y) = (x \<sqsubseteq> y)"
    40   by (rule iso.abs_less [OF swap])
    41 
    42 lemma abs_eq: "(abs\<cdot>x = abs\<cdot>y) = (x = y)"
    43   by (simp add: po_eq_conv abs_less)
    44 
    45 lemma rep_eq: "(rep\<cdot>x = rep\<cdot>y) = (x = y)"
    46   by (rule iso.abs_eq [OF swap])
    47 
    48 lemma abs_strict: "abs\<cdot>\<bottom> = \<bottom>"
    49 proof -
    50   have "\<bottom> \<sqsubseteq> rep\<cdot>\<bottom>" ..
    51   then have "abs\<cdot>\<bottom> \<sqsubseteq> abs\<cdot>(rep\<cdot>\<bottom>)" by (rule monofun_cfun_arg)
    52   then have "abs\<cdot>\<bottom> \<sqsubseteq> \<bottom>" by simp
    53   then show ?thesis by (rule UU_I)
    54 qed
    55 
    56 lemma rep_strict: "rep\<cdot>\<bottom> = \<bottom>"
    57   by (rule iso.abs_strict [OF swap])
    58 
    59 lemma abs_defin': "abs\<cdot>x = \<bottom> \<Longrightarrow> x = \<bottom>"
    60 proof -
    61   have "x = rep\<cdot>(abs\<cdot>x)" by simp
    62   also assume "abs\<cdot>x = \<bottom>"
    63   also note rep_strict
    64   finally show "x = \<bottom>" .
    65 qed
    66 
    67 lemma rep_defin': "rep\<cdot>z = \<bottom> \<Longrightarrow> z = \<bottom>"
    68   by (rule iso.abs_defin' [OF swap])
    69 
    70 lemma abs_defined: "z \<noteq> \<bottom> \<Longrightarrow> abs\<cdot>z \<noteq> \<bottom>"
    71   by (erule contrapos_nn, erule abs_defin')
    72 
    73 lemma rep_defined: "z \<noteq> \<bottom> \<Longrightarrow> rep\<cdot>z \<noteq> \<bottom>"
    74   by (rule iso.abs_defined [OF iso.swap]) (rule iso_axioms)
    75 
    76 lemma abs_defined_iff: "(abs\<cdot>x = \<bottom>) = (x = \<bottom>)"
    77   by (auto elim: abs_defin' intro: abs_strict)
    78 
    79 lemma rep_defined_iff: "(rep\<cdot>x = \<bottom>) = (x = \<bottom>)"
    80   by (rule iso.abs_defined_iff [OF iso.swap]) (rule iso_axioms)
    81 
    82 lemma (in iso) compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
    83 proof (unfold compact_def)
    84   assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
    85   with cont_Rep_CFun2
    86   have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
    87   then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_less by simp
    88 qed
    89 
    90 lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"
    91   by (rule iso.compact_abs_rev [OF iso.swap]) (rule iso_axioms)
    92 
    93 lemma compact_abs: "compact x \<Longrightarrow> compact (abs\<cdot>x)"
    94   by (rule compact_rep_rev) simp
    95 
    96 lemma compact_rep: "compact x \<Longrightarrow> compact (rep\<cdot>x)"
    97   by (rule iso.compact_abs [OF iso.swap]) (rule iso_axioms)
    98 
    99 lemma iso_swap: "(x = abs\<cdot>y) = (rep\<cdot>x = y)"
   100 proof
   101   assume "x = abs\<cdot>y"
   102   then have "rep\<cdot>x = rep\<cdot>(abs\<cdot>y)" by simp
   103   then show "rep\<cdot>x = y" by simp
   104 next
   105   assume "rep\<cdot>x = y"
   106   then have "abs\<cdot>(rep\<cdot>x) = abs\<cdot>y" by simp
   107   then show "x = abs\<cdot>y" by simp
   108 qed
   109 
   110 end
   111 
   112 
   113 subsection {* Casedist *}
   114 
   115 lemma ex_one_defined_iff:
   116   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
   117  apply safe
   118   apply (rule_tac p=x in oneE)
   119    apply simp
   120   apply simp
   121  apply force
   122  done
   123 
   124 lemma ex_up_defined_iff:
   125   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
   126  apply safe
   127   apply (rule_tac p=x in upE)
   128    apply simp
   129   apply fast
   130  apply (force intro!: up_defined)
   131  done
   132 
   133 lemma ex_sprod_defined_iff:
   134  "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
   135   (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
   136  apply safe
   137   apply (rule_tac p=y in sprodE)
   138    apply simp
   139   apply fast
   140  apply (force intro!: spair_defined)
   141  done
   142 
   143 lemma ex_sprod_up_defined_iff:
   144  "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
   145   (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
   146  apply safe
   147   apply (rule_tac p=y in sprodE)
   148    apply simp
   149   apply (rule_tac p=x in upE)
   150    apply simp
   151   apply fast
   152  apply (force intro!: spair_defined)
   153  done
   154 
   155 lemma ex_ssum_defined_iff:
   156  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
   157  ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
   158   (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
   159  apply (rule iffI)
   160   apply (erule exE)
   161   apply (erule conjE)
   162   apply (rule_tac p=x in ssumE)
   163     apply simp
   164    apply (rule disjI1, fast)
   165   apply (rule disjI2, fast)
   166  apply (erule disjE)
   167   apply force
   168  apply force
   169  done
   170 
   171 lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
   172   by auto
   173 
   174 lemmas ex_defined_iffs =
   175    ex_ssum_defined_iff
   176    ex_sprod_up_defined_iff
   177    ex_sprod_defined_iff
   178    ex_up_defined_iff
   179    ex_one_defined_iff
   180 
   181 text {* Rules for turning exh into casedist *}
   182 
   183 lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)
   184   by auto
   185 
   186 lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)"
   187   by rule auto
   188 
   189 lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
   190   by rule auto
   191 
   192 lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
   193   by rule auto
   194 
   195 lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
   196 
   197 
   198 subsection {* Setting up the package *}
   199 
   200 ML {*
   201 val iso_intro       = thm "iso.intro";
   202 val iso_abs_iso     = thm "iso.abs_iso";
   203 val iso_rep_iso     = thm "iso.rep_iso";
   204 val iso_abs_strict  = thm "iso.abs_strict";
   205 val iso_rep_strict  = thm "iso.rep_strict";
   206 val iso_abs_defin'  = thm "iso.abs_defin'";
   207 val iso_rep_defin'  = thm "iso.rep_defin'";
   208 val iso_abs_defined = thm "iso.abs_defined";
   209 val iso_rep_defined = thm "iso.rep_defined";
   210 val iso_compact_abs = thm "iso.compact_abs";
   211 val iso_compact_rep = thm "iso.compact_rep";
   212 val iso_iso_swap    = thm "iso.iso_swap";
   213 
   214 val exh_start = thm "exh_start";
   215 val ex_defined_iffs = thms "ex_defined_iffs";
   216 val exh_casedist0 = thm "exh_casedist0";
   217 val exh_casedists = thms "exh_casedists";
   218 *}
   219 
   220 end