--- a/src/HOL/Basic_BNF_LFPs.thy Mon Apr 04 23:58:48 2016 +0200
+++ b/src/HOL/Basic_BNF_LFPs.thy Tue Apr 05 09:54:17 2016 +0200
@@ -15,6 +15,9 @@
lemma xtor_map: "f (xtor x) = xtor (f x)"
unfolding xtor_def by (rule refl)
+lemma xtor_map_unique: "u \<circ> xtor = xtor \<circ> f \<Longrightarrow> u = f"
+ unfolding o_def xtor_def .
+
lemma xtor_set: "f (xtor x) = f x"
unfolding xtor_def by (rule refl)
@@ -50,6 +53,9 @@
lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((id_bnf \<circ> g \<circ> id_bnf) x)"
unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
+lemma ctor_rec_unique: "g = id \<Longrightarrow> f \<circ> xtor = s \<circ> (id_bnf \<circ> g \<circ> id_bnf) \<Longrightarrow> f = ctor_rec s"
+ unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)
+
lemma ctor_rec_def_alt: "f = ctor_rec (f \<circ> id_bnf)"
unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)