src/HOLCF/Domain.thy
author huffman
Wed Nov 10 17:56:08 2010 -0800 (2010-11-10)
changeset 40502 8e92772bc0e8
parent 40321 d065b195ec89
child 40503 4094d788b904
permissions -rw-r--r--
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
     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_axioms.ML")
    14   ("Tools/Domain/domain_induction.ML")
    15   ("Tools/Domain/domain.ML")
    16 begin
    17 
    18 default_sort pcpo
    19 
    20 
    21 subsection {* Casedist *}
    22 
    23 text {* Lemmas for proving nchotomy rule: *}
    24 
    25 lemma ex_one_bottom_iff:
    26   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = P ONE"
    27 by simp
    28 
    29 lemma ex_up_bottom_iff:
    30   "(\<exists>x. P x \<and> x \<noteq> \<bottom>) = (\<exists>x. P (up\<cdot>x))"
    31 by (safe, case_tac x, auto)
    32 
    33 lemma ex_sprod_bottom_iff:
    34  "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
    35   (\<exists>x y. (P (:x, y:) \<and> x \<noteq> \<bottom>) \<and> y \<noteq> \<bottom>)"
    36 by (safe, case_tac y, auto)
    37 
    38 lemma ex_sprod_up_bottom_iff:
    39  "(\<exists>y. P y \<and> y \<noteq> \<bottom>) =
    40   (\<exists>x y. P (:up\<cdot>x, y:) \<and> y \<noteq> \<bottom>)"
    41 by (safe, case_tac y, simp, case_tac x, auto)
    42 
    43 lemma ex_ssum_bottom_iff:
    44  "(\<exists>x. P x \<and> x \<noteq> \<bottom>) =
    45  ((\<exists>x. P (sinl\<cdot>x) \<and> x \<noteq> \<bottom>) \<or>
    46   (\<exists>x. P (sinr\<cdot>x) \<and> x \<noteq> \<bottom>))"
    47 by (safe, case_tac x, auto)
    48 
    49 lemma exh_start: "p = \<bottom> \<or> (\<exists>x. p = x \<and> x \<noteq> \<bottom>)"
    50   by auto
    51 
    52 lemmas ex_bottom_iffs =
    53    ex_ssum_bottom_iff
    54    ex_sprod_up_bottom_iff
    55    ex_sprod_bottom_iff
    56    ex_up_bottom_iff
    57    ex_one_bottom_iff
    58 
    59 text {* Rules for turning nchotomy into exhaust: *}
    60 
    61 lemma exh_casedist0: "\<lbrakk>R; R \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" (* like make_elim *)
    62   by auto
    63 
    64 lemma exh_casedist1: "((P \<or> Q \<Longrightarrow> R) \<Longrightarrow> S) \<equiv> (\<lbrakk>P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> S)"
    65   by rule auto
    66 
    67 lemma exh_casedist2: "(\<exists>x. P x \<Longrightarrow> Q) \<equiv> (\<And>x. P x \<Longrightarrow> Q)"
    68   by rule auto
    69 
    70 lemma exh_casedist3: "(P \<and> Q \<Longrightarrow> R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> R)"
    71   by rule auto
    72 
    73 lemmas exh_casedists = exh_casedist1 exh_casedist2 exh_casedist3
    74 
    75 
    76 subsection {* Installing the domain package *}
    77 
    78 lemmas con_strict_rules =
    79   sinl_strict sinr_strict spair_strict1 spair_strict2
    80 
    81 lemmas con_bottom_iff_rules =
    82   sinl_bottom_iff sinr_bottom_iff spair_bottom_iff up_defined ONE_defined
    83 
    84 lemmas con_below_iff_rules =
    85   sinl_below sinr_below sinl_below_sinr sinr_below_sinl con_bottom_iff_rules
    86 
    87 lemmas con_eq_iff_rules =
    88   sinl_eq sinr_eq sinl_eq_sinr sinr_eq_sinl con_bottom_iff_rules
    89 
    90 lemmas sel_strict_rules =
    91   cfcomp2 sscase1 sfst_strict ssnd_strict fup1
    92 
    93 lemma sel_app_extra_rules:
    94   "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinr\<cdot>x) = \<bottom>"
    95   "sscase\<cdot>ID\<cdot>\<bottom>\<cdot>(sinl\<cdot>x) = x"
    96   "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinl\<cdot>x) = \<bottom>"
    97   "sscase\<cdot>\<bottom>\<cdot>ID\<cdot>(sinr\<cdot>x) = x"
    98   "fup\<cdot>ID\<cdot>(up\<cdot>x) = x"
    99 by (cases "x = \<bottom>", simp, simp)+
   100 
   101 lemmas sel_app_rules =
   102   sel_strict_rules sel_app_extra_rules
   103   ssnd_spair sfst_spair up_defined spair_defined
   104 
   105 lemmas sel_bottom_iff_rules =
   106   cfcomp2 sfst_bottom_iff ssnd_bottom_iff
   107 
   108 lemmas take_con_rules =
   109   ssum_map_sinl' ssum_map_sinr' sprod_map_spair' u_map_up
   110   deflation_strict deflation_ID ID1 cfcomp2
   111 
   112 use "Tools/cont_consts.ML"
   113 use "Tools/cont_proc.ML"
   114 use "Tools/Domain/domain_axioms.ML"
   115 use "Tools/Domain/domain_constructors.ML"
   116 use "Tools/Domain/domain_induction.ML"
   117 use "Tools/Domain/domain.ML"
   118 
   119 end