src/HOL/Basic_BNF_Least_Fixpoints.thy
changeset 58377 c6f93b8d2d8e
parent 58353 c9f374b64d99
child 58390 b74d8470b98e
     1.1 --- a/src/HOL/Basic_BNF_Least_Fixpoints.thy	Thu Sep 18 16:47:40 2014 +0200
     1.2 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy	Thu Sep 18 16:47:40 2014 +0200
     1.3 @@ -9,32 +9,6 @@
     1.4  imports BNF_Least_Fixpoint
     1.5  begin
     1.6  
     1.7 -subsection {* Size setup (TODO: Merge with rest of file) *}
     1.8 -
     1.9 -lemma size_bool[code]: "size (b\<Colon>bool) = 0"
    1.10 -  by (cases b) auto
    1.11 -
    1.12 -lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
    1.13 -  by (induct n) simp_all
    1.14 -
    1.15 -declare prod.size[no_atp]
    1.16 -
    1.17 -lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
    1.18 -  by (rule ext) (case_tac x, auto)
    1.19 -
    1.20 -lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
    1.21 -  by (rule ext) auto
    1.22 -
    1.23 -setup {*
    1.24 -BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
    1.25 -  @{thms size_sum_o_map}
    1.26 -#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
    1.27 -  @{thms size_prod_o_map}
    1.28 -*}
    1.29 -
    1.30 -
    1.31 -subsection {* FP sugar setup *}
    1.32 -
    1.33  definition xtor :: "'a \<Rightarrow> 'a" where
    1.34    "xtor x = x"
    1.35  
    1.36 @@ -55,15 +29,6 @@
    1.37  
    1.38  lemmas xtor_inject = xtor_rel[of "op ="]
    1.39  
    1.40 -definition ctor_rec :: "'a \<Rightarrow> 'a" where
    1.41 -  "ctor_rec x = x"
    1.42 -
    1.43 -lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
    1.44 -  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
    1.45 -
    1.46 -lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
    1.47 -  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    1.48 -
    1.49  lemma xtor_rel_induct: "(\<And>x y. vimage2p id_bnf id_bnf R x y \<Longrightarrow> IR (xtor x) (xtor y)) \<Longrightarrow> R \<le> IR"
    1.50    unfolding xtor_def vimage2p_def id_bnf_def by default
    1.51  
    1.52 @@ -76,12 +41,30 @@
    1.53  lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))"
    1.54    unfolding xtor_def id_bnf_def by (rule reflexive)
    1.55  
    1.56 +definition ctor_rec :: "'a \<Rightarrow> 'a" where
    1.57 +  "ctor_rec x = x"
    1.58 +
    1.59 +lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
    1.60 +  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
    1.61 +
    1.62 +lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)"
    1.63 +  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    1.64 +
    1.65 +lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
    1.66 +  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    1.67 +
    1.68  ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
    1.69  
    1.70 +thm sum.rec_o_map
    1.71 +thm sum.size_o_map
    1.72 +
    1.73 +thm prod.rec_o_map
    1.74 +thm prod.size_o_map
    1.75 +
    1.76  hide_const (open) xtor ctor_rec
    1.77  
    1.78  hide_fact (open)
    1.79    xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
    1.80 -  ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
    1.81 +  ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
    1.82  
    1.83  end