src/HOLCF/Domain.thy
author huffman
Tue Oct 12 06:20:05 2010 -0700 (2010-10-12)
changeset 40006 116e94f9543b
parent 36452 d37c6eed8117
child 40026 8f8f18a88685
permissions -rw-r--r--
remove unneeded lemmas from Fun_Cpo.thy
     1 (*  Title:      HOLCF/Domain.thy
     2     Author:     Brian Huffman
     3 *)
     4 
     5 header {* Domain package *}
     6 
     7 theory Domain
     8 imports Ssum Sprod Up One Tr Fixrec Representable
     9 uses
    10   ("Tools/cont_consts.ML")
    11   ("Tools/cont_proc.ML")
    12   ("Tools/Domain/domain_constructors.ML")
    13   ("Tools/Domain/domain_library.ML")
    14   ("Tools/Domain/domain_axioms.ML")
    15   ("Tools/Domain/domain_theorems.ML")
    16   ("Tools/Domain/domain_extender.ML")
    17 begin
    18 
    19 default_sort pcpo
    20 
    21 
    22 subsection {* Casedist *}
    23 
    24 lemma ex_one_defined_iff:
    25   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
    26  apply safe
    27   apply (rule_tac p=x in oneE)
    28    apply simp
    29   apply simp
    30  apply force
    31  done
    32 
    33 lemma ex_up_defined_iff:
    34   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
    35  apply safe
    36   apply (rule_tac p=x in upE)
    37    apply simp
    38   apply fast
    39  apply (force intro!: up_defined)
    40  done
    41 
    42 lemma ex_sprod_defined_iff:
    43  "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
    44   (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
    45  apply safe
    46   apply (rule_tac p=y in sprodE)
    47    apply simp
    48   apply fast
    49  apply (force intro!: spair_defined)
    50  done
    51 
    52 lemma ex_sprod_up_defined_iff:
    53  "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
    54   (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
    55  apply safe
    56   apply (rule_tac p=y in sprodE)
    57    apply simp
    58   apply (rule_tac p=x in upE)
    59    apply simp
    60   apply fast
    61  apply (force intro!: spair_defined)
    62  done
    63 
    64 lemma ex_ssum_defined_iff:
    65  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
    66  ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
    67   (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
    68  apply (rule iffI)
    69   apply (erule exE)
    70   apply (erule conjE)
    71   apply (rule_tac p=x in ssumE)
    72     apply simp
    73    apply (rule disjI1, fast)
    74   apply (rule disjI2, fast)
    75  apply (erule disjE)
    76   apply force
    77  apply force
    78  done
    79 
    80 lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
    81   by auto
    82 
    83 lemmas ex_defined_iffs =
    84    ex_ssum_defined_iff
    85    ex_sprod_up_defined_iff
    86    ex_sprod_defined_iff
    87    ex_up_defined_iff
    88    ex_one_defined_iff
    89 
    90 text {* Rules for turning exh into casedist *}
    91 
    92 lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)
    93   by auto
    94 
    95 lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)"
    96   by rule auto
    97 
    98 lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
    99   by rule auto
   100 
   101 lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
   102   by rule auto
   103 
   104 lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
   105 
   106 
   107 subsection {* Combinators for building copy functions *}
   108 
   109 lemmas domain_map_stricts =
   110   ssum_map_strict sprod_map_strict u_map_strict
   111 
   112 lemmas domain_map_simps =
   113   ssum_map_sinl ssum_map_sinr sprod_map_spair u_map_up
   114 
   115 
   116 subsection {* Installing the domain package *}
   117 
   118 lemmas con_strict_rules =
   119   sinl_strict sinr_strict spair_strict1 spair_strict2
   120 
   121 lemmas con_defin_rules =
   122   sinl_defined sinr_defined spair_defined up_defined ONE_defined
   123 
   124 lemmas con_defined_iff_rules =
   125   sinl_defined_iff sinr_defined_iff spair_strict_iff up_defined ONE_defined
   126 
   127 lemmas con_below_iff_rules =
   128   sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_defined_iff_rules
   129 
   130 lemmas con_eq_iff_rules =
   131   sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_defined_iff_rules
   132 
   133 lemmas sel_strict_rules =
   134   cfcomp2 sscase1 sfst_strict ssnd_strict fup1
   135 
   136 lemma sel_app_extra_rules:
   137   "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinr\<cdot>x) = \<bottom>"
   138   "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinl\<cdot>x) = x"
   139   "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinl\<cdot>x) = \<bottom>"
   140   "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinr\<cdot>x) = x"
   141   "fup\<cdot>ID\<cdot>(up\<cdot>x) = x"
   142 by (cases "x = \<bottom>", simp, simp)+
   143 
   144 lemmas sel_app_rules =
   145   sel_strict_rules sel_app_extra_rules
   146   ssnd_spair sfst_spair up_defined spair_defined
   147 
   148 lemmas sel_defined_iff_rules =
   149   cfcomp2 sfst_defined_iff ssnd_defined_iff
   150 
   151 lemmas take_con_rules =
   152   ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
   153   deflation_strict deflation_ID ID1 cfcomp2
   154 
   155 use "Tools/cont_consts.ML"
   156 use "Tools/cont_proc.ML"
   157 use "Tools/Domain/domain_library.ML"
   158 use "Tools/Domain/domain_axioms.ML"
   159 use "Tools/Domain/domain_constructors.ML"
   160 use "Tools/Domain/domain_theorems.ML"
   161 use "Tools/Domain/domain_extender.ML"
   162 
   163 end