# HG changeset patch # User blanchet # Date 1409814163 -7200 # Node ID 6d527272f7b2e39f50b3e06e6a8263c5f9539c64 # Parent 95397823f39eb0c93798020adf8e7d51ae93454f renamed internal constant diff -r 95397823f39e -r 6d527272f7b2 src/HOL/BNF_Composition.thy --- 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 \ 'a \ bool" by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite) -definition id_bnf_comp :: "'a \ 'a" where "id_bnf_comp \ (\x. x)" +definition id_bnf :: "'a \ 'a" where "id_bnf \ (\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 \ 'b) \ 'a \ 'b" + map: "id_bnf :: ('a \ 'b) \ 'a \ 'b" sets: "\x. {x}" bd: natLeq - rel: "id_bnf_comp :: ('a \ 'b \ bool) \ 'a \ 'b \ bool" - unfolding id_bnf_comp_def + rel: "id_bnf :: ('a \ 'b \ bool) \ 'a \ 'b \ 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 diff -r 95397823f39e -r 6d527272f7b2 src/HOL/Tools/BNF/bnf_comp.ML --- 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)); diff -r 95397823f39e -r 6d527272f7b2 src/HOL/Tools/BNF/bnf_comp_tactics.ML --- 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 diff -r 95397823f39e -r 6d527272f7b2 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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' diff -r 95397823f39e -r 6d527272f7b2 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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 =