src/HOL/Basic_BNF_Least_Fixpoints.thy
author blanchet
Tue Sep 16 19:23:37 2014 +0200 (2014-09-16)
changeset 58352 37745650a3f4
child 58353 c9f374b64d99
permissions -rw-r--r--
register 'prod' and 'sum' as datatypes, to allow N2M through them
     1 (*  Title:      HOL/Basic_BNF_Least_Fixpoints.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2014
     4 
     5 Registration of basic types as BNF least fixpoints (datatypes).
     6 *)
     7 
     8 theory Basic_BNF_Least_Fixpoints
     9 imports BNF_Least_Fixpoint
    10 begin
    11 
    12 subsection {* Size setup (TODO: Merge with rest of file) *}
    13 
    14 lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    15   by (cases b) auto
    16 
    17 lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
    18   by (induct n) simp_all
    19 
    20 declare prod.size[no_atp]
    21 
    22 lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
    23   by (rule ext) (case_tac x, auto)
    24 
    25 lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
    26   by (rule ext) auto
    27 
    28 setup {*
    29 BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
    30   @{thms size_sum_o_map}
    31 #> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
    32   @{thms size_prod_o_map}
    33 *}
    34 
    35 
    36 subsection {* FP sugar setup *}
    37 
    38 definition xtor :: "'a \<Rightarrow> 'a" where
    39   "xtor x = x"
    40 
    41 lemma xtor_map: "f (xtor x) = xtor (f x)"
    42   unfolding xtor_def by (rule refl)
    43 
    44 lemma xtor_set: "f (xtor x) = f x"
    45   unfolding xtor_def by (rule refl) 
    46 
    47 lemma xtor_rel: "R (xtor x) (xtor y) = R x y"
    48   unfolding xtor_def by (rule refl)
    49 
    50 lemma xtor_induct: "(\<And>x. P (xtor x)) \<Longrightarrow> P z"
    51   unfolding xtor_def by assumption
    52 
    53 lemma xtor_xtor: "xtor (xtor x) = x"
    54   unfolding xtor_def by (rule refl)
    55 
    56 lemmas xtor_inject = xtor_rel[of "op ="]
    57 
    58 definition ctor_rec :: "'a \<Rightarrow> 'a" where
    59   "ctor_rec x = x"
    60 
    61 lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((BNF_Composition.id_bnf \<circ> g \<circ> BNF_Composition.id_bnf) x)"
    62   unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
    63 
    64 lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (BNF_Composition.id_bnf \<circ> g \<circ> BNF_Composition.id_bnf))"
    65   unfolding ctor_rec_def BNF_Composition.id_bnf_def comp_def by (rule refl)
    66 
    67 lemma xtor_rel_induct: "(\<And>x y. vimage2p BNF_Composition.id_bnf BNF_Composition.id_bnf R x y \<Longrightarrow> IR (xtor x) (xtor y)) \<Longrightarrow> R \<le> IR"
    68   unfolding xtor_def vimage2p_def BNF_Composition.id_bnf_def by default
    69 
    70 lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inl a)))"
    71   unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    72 
    73 lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inr a)))"
    74   unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    75 
    76 lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (BNF_Composition.id_bnf (a, b)))"
    77   unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    78 
    79 ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
    80 
    81 end