src/HOL/Basic_BNF_Least_Fixpoints.thy
changeset 58352 37745650a3f4
child 58353 c9f374b64d99
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy	Tue Sep 16 19:23:37 2014 +0200
     1.3 @@ -0,0 +1,81 @@
     1.4 +(*  Title:      HOL/Basic_BNF_Least_Fixpoints.thy
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +    Copyright   2014
     1.7 +
     1.8 +Registration of basic types as BNF least fixpoints (datatypes).
     1.9 +*)
    1.10 +
    1.11 +theory Basic_BNF_Least_Fixpoints
    1.12 +imports BNF_Least_Fixpoint
    1.13 +begin
    1.14 +
    1.15 +subsection {* Size setup (TODO: Merge with rest of file) *}
    1.16 +
    1.17 +lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    1.18 +  by (cases b) auto
    1.19 +
    1.20 +lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
    1.21 +  by (induct n) simp_all
    1.22 +
    1.23 +declare prod.size[no_atp]
    1.24 +
    1.25 +lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
    1.26 +  by (rule ext) (case_tac x, auto)
    1.27 +
    1.28 +lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
    1.29 +  by (rule ext) auto
    1.30 +
    1.31 +setup {*
    1.32 +BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
    1.33 +  @{thms size_sum_o_map}
    1.34 +#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
    1.35 +  @{thms size_prod_o_map}
    1.36 +*}
    1.37 +
    1.38 +
    1.39 +subsection {* FP sugar setup *}
    1.40 +
    1.41 +definition xtor :: "'a \<Rightarrow> 'a" where
    1.42 +  "xtor x = x"
    1.43 +
    1.44 +lemma xtor_map: "f (xtor x) = xtor (f x)"
    1.45 +  unfolding xtor_def by (rule refl)
    1.46 +
    1.47 +lemma xtor_set: "f (xtor x) = f x"
    1.48 +  unfolding xtor_def by (rule refl) 
    1.49 +
    1.50 +lemma xtor_rel: "R (xtor x) (xtor y) = R x y"
    1.51 +  unfolding xtor_def by (rule refl)
    1.52 +
    1.53 +lemma xtor_induct: "(\<And>x. P (xtor x)) \<Longrightarrow> P z"
    1.54 +  unfolding xtor_def by assumption
    1.55 +
    1.56 +lemma xtor_xtor: "xtor (xtor x) = x"
    1.57 +  unfolding xtor_def by (rule refl)
    1.58 +
    1.59 +lemmas xtor_inject = xtor_rel[of "op ="]
    1.60 +
    1.61 +definition ctor_rec :: "'a \<Rightarrow> 'a" where
    1.62 +  "ctor_rec x = x"
    1.63 +
    1.64 +lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((BNF_Composition.id_bnf \<circ> g \<circ> BNF_Composition.id_bnf) x)"
    1.65 +  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
    1.66 +
    1.67 +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))"
    1.68 +  unfolding ctor_rec_def BNF_Composition.id_bnf_def comp_def by (rule refl)
    1.69 +
    1.70 +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"
    1.71 +  unfolding xtor_def vimage2p_def BNF_Composition.id_bnf_def by default
    1.72 +
    1.73 +lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inl a)))"
    1.74 +  unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    1.75 +
    1.76 +lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inr a)))"
    1.77 +  unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    1.78 +
    1.79 +lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (BNF_Composition.id_bnf (a, b)))"
    1.80 +  unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    1.81 +
    1.82 +ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
    1.83 +
    1.84 +end