126 unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def |
126 unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def |
127 by (auto simp: type_copy_ex_RepI) |
127 by (auto simp: type_copy_ex_RepI) |
128 |
128 |
129 end |
129 end |
130 |
130 |
131 definition id_rep :: "'a \<Rightarrow> 'a" where "id_rep = (\<lambda>x. x)" |
131 definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp = (\<lambda>x. x)" |
132 definition id_abs :: "'a \<Rightarrow> 'a" where "id_abs = (\<lambda>x. x)" |
|
133 |
132 |
134 lemma type_definition_id_rep_abs_UNIV: "type_definition id_rep id_abs UNIV" |
133 lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV" |
135 unfolding id_rep_def id_abs_def by unfold_locales auto |
134 unfolding id_bnf_comp_def by unfold_locales auto |
136 |
135 |
137 lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r" |
136 lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r" |
138 by (metis csum_absorb2' ordIso_transitive ordLeq_refl) |
137 by (metis csum_absorb2' ordIso_transitive ordLeq_refl) |
139 |
138 |
140 lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r" |
139 lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r" |
141 by (metis cprod_infinite ordIso_transitive) |
140 by (metis cprod_infinite ordIso_transitive) |
142 |
141 |
143 ML_file "Tools/BNF/bnf_comp_tactics.ML" |
142 ML_file "Tools/BNF/bnf_comp_tactics.ML" |
144 ML_file "Tools/BNF/bnf_comp.ML" |
143 ML_file "Tools/BNF/bnf_comp.ML" |
145 |
144 |
146 hide_const id_rep id_abs |
145 hide_const id_bnf_comp |
147 hide_fact id_rep_def id_abs_def type_definition_id_rep_abs_UNIV |
146 hide_fact id_bnf_comp_def type_definition_id_bnf_comp_UNIV |
148 |
147 |
149 end |
148 end |