211 |
211 |
212 lemma comp_transfer: |
212 lemma comp_transfer: |
213 "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)" |
213 "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)" |
214 unfolding rel_fun_def by simp |
214 unfolding rel_fun_def by simp |
215 |
215 |
|
216 lemma If_transfer: "rel_fun (op =) (rel_fun A (rel_fun A A)) If If" |
|
217 unfolding rel_fun_def by simp |
|
218 |
|
219 lemma Abs_transfer: |
|
220 assumes type_copy1: "type_definition Rep1 Abs1 UNIV" |
|
221 assumes type_copy2: "type_definition Rep2 Abs2 UNIV" |
|
222 shows "rel_fun R (vimage2p Rep1 Rep2 R) Abs1 Abs2" |
|
223 unfolding vimage2p_def rel_fun_def |
|
224 type_definition.Abs_inverse[OF type_copy1 UNIV_I] |
|
225 type_definition.Abs_inverse[OF type_copy2 UNIV_I] by simp |
|
226 |
|
227 lemma Inl_transfer: |
|
228 "rel_fun S (rel_sum S T) Inl Inl" |
|
229 by auto |
|
230 |
|
231 lemma Inr_transfer: |
|
232 "rel_fun T (rel_sum S T) Inr Inr" |
|
233 by auto |
|
234 |
|
235 lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair" |
|
236 unfolding rel_fun_def rel_prod_def by simp |
|
237 |
216 ML_file "Tools/BNF/bnf_fp_util.ML" |
238 ML_file "Tools/BNF/bnf_fp_util.ML" |
217 ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" |
239 ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" |
218 ML_file "Tools/BNF/bnf_fp_def_sugar.ML" |
240 ML_file "Tools/BNF/bnf_fp_def_sugar.ML" |
219 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" |
241 ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" |
220 ML_file "Tools/BNF/bnf_fp_n2m.ML" |
242 ML_file "Tools/BNF/bnf_fp_n2m.ML" |