--- a/src/HOL/BNF_Composition.thy Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/BNF_Composition.thy Thu Sep 04 09:02:43 2014 +0200
@@ -146,29 +146,29 @@
rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
-definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
+definition id_bnf :: "'a \<Rightarrow> 'a" where "id_bnf \<equiv> (\<lambda>x. x)"
-lemma id_bnf_comp_apply: "id_bnf_comp x = x"
- unfolding id_bnf_comp_def by simp
+lemma id_bnf_apply: "id_bnf x = x"
+ unfolding id_bnf_def by simp
bnf ID: 'a
- map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+ map: "id_bnf :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
sets: "\<lambda>x. {x}"
bd: natLeq
- rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
- unfolding id_bnf_comp_def
+ rel: "id_bnf :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+ unfolding id_bnf_def
apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
done
-lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
- unfolding id_bnf_comp_def by unfold_locales auto
+lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV"
+ unfolding id_bnf_def by unfold_locales auto
ML_file "Tools/BNF/bnf_comp_tactics.ML"
ML_file "Tools/BNF/bnf_comp.ML"
-hide_const (open) id_bnf_comp
-hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
+hide_const (open) id_bnf
+hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
end
--- a/src/HOL/Tools/BNF/bnf_comp.ML Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Thu Sep 04 09:02:43 2014 +0200
@@ -115,9 +115,8 @@
val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
in Envir.expand_term get end;
-val id_bnf_comp_def = @{thm id_bnf_comp_def};
-val expand_id_bnf_comp_def =
- expand_term_const [Thm.prop_of id_bnf_comp_def |> Logic.dest_equals];
+val id_bnf_def = @{thm id_bnf_def};
+val expand_id_bnf_def = expand_term_const [Thm.prop_of id_bnf_def |> Logic.dest_equals];
fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
| is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
@@ -198,7 +197,7 @@
fun mk_simplified_set set =
let
val setT = fastype_of set;
- val var_set' = Const (@{const_name id_bnf_comp}, setT --> setT) $ Var ((Name.uu, 0), setT);
+ val var_set' = Const (@{const_name id_bnf}, setT --> setT) $ Var ((Name.uu, 0), setT);
val goal = mk_Trueprop_eq (var_set', set);
fun tac {context = ctxt, prems = _} =
mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer);
@@ -342,8 +341,8 @@
Binding.empty Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy;
val phi =
- Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def])
- $> Morphism.term_morphism "BNF" expand_id_bnf_comp_def;
+ Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_def])
+ $> Morphism.term_morphism "BNF" expand_id_bnf_def;
val bnf'' = morph_bnf phi bnf';
in
@@ -720,8 +719,8 @@
else raise Term.TYPE ("mk_repT", [absT, repT, absT], [])
| _ => raise Term.TYPE ("mk_repT", [absT, repT, absT], []));
-fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf_comp}, _)) =
- Const (@{const_name id_bnf_comp}, absU --> absU)
+fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf}, _)) =
+ Const (@{const_name id_bnf}, absU --> absU)
| mk_abs_or_rep getT (Type (_, Us)) abs =
let val Ts = snd (dest_Type (getT (fastype_of abs)))
in Term.subst_atomic_types (Ts ~~ Us) abs end;
@@ -738,11 +737,11 @@
in
if inline then
pair (repT,
- (@{const_name id_bnf_comp}, @{const_name id_bnf_comp},
- @{thm type_definition_id_bnf_comp_UNIV},
- @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_comp_UNIV]},
- @{thm type_definition.Abs_inject[OF type_definition_id_bnf_comp_UNIV]},
- @{thm type_definition.Abs_cases[OF type_definition_id_bnf_comp_UNIV]}))
+ (@{const_name id_bnf}, @{const_name id_bnf},
+ @{thm type_definition_id_bnf_UNIV},
+ @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV]},
+ @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV]},
+ @{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]}))
else
typedef (b, As, mx) set opt_morphs tac
#>> (fn (T_name, ({Rep_name, Abs_name, ...},
@@ -858,7 +857,7 @@
Binding.empty Binding.empty []
((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
- val unfolds = @{thm id_bnf_comp_apply} ::
+ val unfolds = @{thm id_bnf_apply} ::
(#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set);
val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds));
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Thu Sep 04 09:02:43 2014 +0200
@@ -240,7 +240,7 @@
val simplified_set_simps =
@{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left
- o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_comp_def};
+ o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_def};
fun mk_simplified_set_tac ctxt collect_set_map =
unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Sep 04 09:02:43 2014 +0200
@@ -290,7 +290,7 @@
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_comp_def rel_sum_simps rel_prod_apply vimage2p_def
+ @{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
REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
(rtac refl ORELSE' atac))))
@@ -305,7 +305,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_comp_def vimage2p_def}) THEN
+ @{thms BNF_Composition.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
@@ -354,7 +354,7 @@
Abs_pre_inverses =
let
val assms_ctor_defs =
- map (unfold_thms ctxt (@{thm BNF_Composition.id_bnf_comp_def} :: ctor_defs)) assms;
+ map (unfold_thms ctxt (@{thm BNF_Composition.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
@@ -364,7 +364,7 @@
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_comp_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert
+ @{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
REPEAT_DETERM (HEADGOAL
(TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN'
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 04 09:02:43 2014 +0200
@@ -64,7 +64,7 @@
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_comp_def};
+ BNF_Composition.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 =