src/HOL/Basic_BNF_Least_Fixpoints.thy
changeset 58353 c9f374b64d99
parent 58352 37745650a3f4
child 58377 c6f93b8d2d8e
     1.1 --- a/src/HOL/Basic_BNF_Least_Fixpoints.thy	Tue Sep 16 19:23:37 2014 +0200
     1.2 +++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy	Tue Sep 16 19:23:37 2014 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4    unfolding xtor_def by (rule refl)
     1.5  
     1.6  lemma xtor_set: "f (xtor x) = f x"
     1.7 -  unfolding xtor_def by (rule refl) 
     1.8 +  unfolding xtor_def by (rule refl)
     1.9  
    1.10  lemma xtor_rel: "R (xtor x) (xtor y) = R x y"
    1.11    unfolding xtor_def by (rule refl)
    1.12 @@ -58,24 +58,30 @@
    1.13  definition ctor_rec :: "'a \<Rightarrow> 'a" where
    1.14    "ctor_rec x = x"
    1.15  
    1.16 -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.17 +lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
    1.18    unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
    1.19  
    1.20 -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.21 -  unfolding ctor_rec_def BNF_Composition.id_bnf_def comp_def by (rule refl)
    1.22 +lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
    1.23 +  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
    1.24  
    1.25 -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.26 -  unfolding xtor_def vimage2p_def BNF_Composition.id_bnf_def by default
    1.27 +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.28 +  unfolding xtor_def vimage2p_def id_bnf_def by default
    1.29  
    1.30 -lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inl a)))"
    1.31 -  unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    1.32 +lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))"
    1.33 +  unfolding xtor_def id_bnf_def by (rule reflexive)
    1.34  
    1.35 -lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inr a)))"
    1.36 -  unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    1.37 +lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (id_bnf (Inr a)))"
    1.38 +  unfolding xtor_def id_bnf_def by (rule reflexive)
    1.39  
    1.40 -lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (BNF_Composition.id_bnf (a, b)))"
    1.41 -  unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
    1.42 +lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))"
    1.43 +  unfolding xtor_def id_bnf_def by (rule reflexive)
    1.44  
    1.45  ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
    1.46  
    1.47 +hide_const (open) xtor ctor_rec
    1.48 +
    1.49 +hide_fact (open)
    1.50 +  xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
    1.51 +  ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
    1.52 +
    1.53  end