# HG changeset patch # User blanchet # Date 1393847300 -3600 # Node ID 98ad5680173a3a7d5ca3aa0979a66e6ed34b3c1b # Parent ee270328a78193f60702487a4bc198823a61121e use same identity function for abs and rep (doesn't seem to confuse any proofs) diff -r ee270328a781 -r 98ad5680173a src/HOL/BNF_Comp.thy --- a/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/BNF_Comp.thy Mon Mar 03 12:48:20 2014 +0100 @@ -128,11 +128,10 @@ end -definition id_rep :: "'a \ 'a" where "id_rep = (\x. x)" -definition id_abs :: "'a \ 'a" where "id_abs = (\x. x)" +definition id_bnf_comp :: "'a \ 'a" where "id_bnf_comp = (\x. x)" -lemma type_definition_id_rep_abs_UNIV: "type_definition id_rep id_abs UNIV" - unfolding id_rep_def id_abs_def by unfold_locales auto +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 csum_dup: "cinfinite r \ Card_order r \ p +c p' =o r +c r \ p +c p' =o r" by (metis csum_absorb2' ordIso_transitive ordLeq_refl) @@ -143,7 +142,7 @@ ML_file "Tools/BNF/bnf_comp_tactics.ML" ML_file "Tools/BNF/bnf_comp.ML" -hide_const id_rep id_abs -hide_fact id_rep_def id_abs_def type_definition_id_rep_abs_UNIV +hide_const id_bnf_comp +hide_fact id_bnf_comp_def type_definition_id_bnf_comp_UNIV end diff -r ee270328a781 -r 98ad5680173a src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 03 12:48:20 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 03 12:48:20 2014 +0100 @@ -639,10 +639,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_abs}, _)) = - Const (@{const_name id_abs}, absU --> absU) - | mk_abs_or_rep _ absU (Const (@{const_name id_rep}, _)) = - Const (@{const_name id_rep}, absU --> absU) +fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf_comp}, _)) = + Const (@{const_name id_bnf_comp}, 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; @@ -659,9 +657,10 @@ in if inline then pair (repT, - (@{const_name id_rep}, @{const_name id_abs}, @{thm type_definition_id_rep_abs_UNIV}, - @{thm type_definition.Abs_inverse[OF type_definition_id_rep_abs_UNIV]}, - @{thm type_definition.Abs_inject[OF type_definition_id_rep_abs_UNIV]})) + (@{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]})) else typedef (b, As, mx) set opt_morphs tac #>> (fn (T_name, ({Rep_name, Abs_name, ...},