--- a/src/HOL/BNF_Composition.thy Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/BNF_Composition.thy Tue Sep 16 19:23:37 2014 +0200
@@ -146,7 +146,8 @@
rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
-definition id_bnf :: "'a \<Rightarrow> 'a" where "id_bnf \<equiv> (\<lambda>x. x)"
+definition id_bnf :: "'a \<Rightarrow> 'a" where
+ "id_bnf \<equiv> (\<lambda>x. x)"
lemma id_bnf_apply: "id_bnf x = x"
unfolding id_bnf_def by simp
@@ -177,7 +178,4 @@
ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep
ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer
-hide_const (open) id_bnf
-hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
-
end
--- a/src/HOL/Basic_BNF_Least_Fixpoints.thy Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Basic_BNF_Least_Fixpoints.thy Tue Sep 16 19:23:37 2014 +0200
@@ -42,7 +42,7 @@
unfolding xtor_def by (rule refl)
lemma xtor_set: "f (xtor x) = f x"
- unfolding xtor_def by (rule refl)
+ unfolding xtor_def by (rule refl)
lemma xtor_rel: "R (xtor x) (xtor y) = R x y"
unfolding xtor_def by (rule refl)
@@ -58,24 +58,30 @@
definition ctor_rec :: "'a \<Rightarrow> 'a" where
"ctor_rec x = x"
-lemma ctor_rec: "g = id \<Longrightarrow> ctor_rec f (xtor x) = f ((BNF_Composition.id_bnf \<circ> g \<circ> BNF_Composition.id_bnf) x)"
+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_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (BNF_Composition.id_bnf \<circ> g \<circ> BNF_Composition.id_bnf))"
- unfolding ctor_rec_def BNF_Composition.id_bnf_def comp_def by (rule refl)
+lemma ctor_rec_o_map: "ctor_rec f \<circ> g = ctor_rec (f \<circ> (id_bnf \<circ> g \<circ> id_bnf))"
+ unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)
-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"
- unfolding xtor_def vimage2p_def BNF_Composition.id_bnf_def by default
+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"
+ unfolding xtor_def vimage2p_def id_bnf_def by default
-lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inl a)))"
- unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
+lemma Inl_def_alt: "Inl \<equiv> (\<lambda>a. xtor (id_bnf (Inl a)))"
+ unfolding xtor_def id_bnf_def by (rule reflexive)
-lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (BNF_Composition.id_bnf (Inr a)))"
- unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
+lemma Inr_def_alt: "Inr \<equiv> (\<lambda>a. xtor (id_bnf (Inr a)))"
+ unfolding xtor_def id_bnf_def by (rule reflexive)
-lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (BNF_Composition.id_bnf (a, b)))"
- unfolding xtor_def BNF_Composition.id_bnf_def by (rule reflexive)
+lemma Pair_def_alt: "Pair \<equiv> (\<lambda>a b. xtor (id_bnf (a, b)))"
+ unfolding xtor_def id_bnf_def by (rule reflexive)
ML_file "Tools/BNF/bnf_lfp_basic_sugar.ML"
+hide_const (open) xtor ctor_rec
+
+hide_fact (open)
+ xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
+ ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt
+
end
--- a/src/HOL/Main.thy Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Main.thy Tue Sep 16 19:23:37 2014 +0200
@@ -32,7 +32,9 @@
hide_const (open)
czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
- shift proj
+ shift proj id_bnf
+
+hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
no_syntax (xsymbols)
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Sep 16 19:23:37 2014 +0200
@@ -293,8 +293,8 @@
unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN
unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @
- @{thms BNF_Composition.id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def
- Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
+ @{thms id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False
+ iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
(rtac refl ORELSE' atac))))
cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
@@ -308,7 +308,7 @@
(rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN
unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
- @{thms BNF_Composition.id_bnf_def vimage2p_def}) THEN
+ @{thms id_bnf_def vimage2p_def}) THEN
TRYALL (hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
Inr_Inl_False sum.inject prod.inject}) THEN
@@ -356,8 +356,7 @@
fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors
Abs_pre_inverses =
let
- val assms_ctor_defs =
- map (unfold_thms ctxt (@{thm BNF_Composition.id_bnf_def} :: ctor_defs)) assms;
+ val assms_ctor_defs = map (unfold_thms ctxt (@{thm id_bnf_def} :: ctor_defs)) assms;
val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
|> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts;
in
@@ -367,8 +366,8 @@
cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
THEN' atac THEN' hyp_subst_tac ctxt)) THEN
unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
- @{thms BNF_Composition.id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert
- Un_empty_left Un_empty_right empty_iff singleton_iff}) THEN
+ @{thms id_bnf_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert Un_empty_left
+ Un_empty_right empty_iff singleton_iff}) THEN
REPEAT_DETERM (HEADGOAL
(TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN'
REPEAT_DETERM o eresolve_tac @{thms UN_E UnE singletonE} THEN'
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Sep 16 19:23:37 2014 +0200
@@ -2,7 +2,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2014
-Sugared datatype and codatatype constructions.
+Registration of basic types as BNF least fixpoints (datatypes).
*)
structure BNF_LFP_Basic_Sugar : sig end =
@@ -20,13 +20,11 @@
fun trivial_absT_info_of fpT =
{absT = fpT,
repT = fpT,
- abs = Const (@{const_name BNF_Composition.id_bnf}, fpT --> fpT),
- rep = Const (@{const_name BNF_Composition.id_bnf}, fpT --> fpT),
- abs_inject = @{thm type_definition.Abs_inject
- [OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I UNIV_I]},
- abs_inverse = @{thm type_definition.Abs_inverse
- [OF BNF_Composition.type_definition_id_bnf_UNIV UNIV_I]},
- type_definition = @{thm BNF_Composition.type_definition_id_bnf_UNIV}};
+ abs = Const (@{const_name id_bnf}, fpT --> fpT),
+ rep = Const (@{const_name id_bnf}, fpT --> fpT),
+ abs_inject = @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV UNIV_I UNIV_I]},
+ abs_inverse = @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV UNIV_I]},
+ type_definition = @{thm type_definition_id_bnf_UNIV}};
fun the_frozen_ctr_sugar_of ctxt fpT_name =
the (ctr_sugar_of ctxt fpT_name)
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Sep 16 19:23:37 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Sep 16 19:23:37 2014 +0200
@@ -63,8 +63,7 @@
funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
val rec_o_map_simps =
- @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod
- BNF_Composition.id_bnf_def};
+ @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def};
fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
ctor_rec_o_map =