9 |
9 |
10 quotient my_int = "nat \<times> nat" / intrel |
10 quotient my_int = "nat \<times> nat" / intrel |
11 apply(unfold EQUIV_def) |
11 apply(unfold EQUIV_def) |
12 apply(auto simp add: mem_def expand_fun_eq) |
12 apply(auto simp add: mem_def expand_fun_eq) |
13 done |
13 done |
|
14 |
|
15 print_theorems |
14 |
16 |
15 quotient_def (for my_int) |
17 quotient_def (for my_int) |
16 ZERO::"my_int" |
18 ZERO::"my_int" |
17 where |
19 where |
18 "ZERO \<equiv> (0::nat, 0::nat)" |
20 "ZERO \<equiv> (0::nat, 0::nat)" |
112 |
114 |
113 lemma ho_plus_rsp: |
115 lemma ho_plus_rsp: |
114 "(intrel ===> intrel ===> intrel) my_plus my_plus" |
116 "(intrel ===> intrel ===> intrel) my_plus my_plus" |
115 by (simp) |
117 by (simp) |
116 |
118 |
117 ML {* val consts = [@{const_name "my_plus"}] *} |
|
118 ML {* val rty = @{typ "nat \<times> nat"} *} |
|
119 ML {* val qty = @{typ "my_int"} *} |
119 ML {* val qty = @{typ "my_int"} *} |
120 ML {* val rel = @{term "intrel"} *} |
120 ML {* val ty_name = "my_int" *} |
121 ML {* val rel_eqv = (#equiv_thm o hd) (quotdata_lookup @{context}) *} |
|
122 ML {* val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] *} |
|
123 ML {* val quot = @{thm QUOTIENT_my_int} *} |
|
124 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
121 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
125 ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *} |
|
126 ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *} |
|
127 ML {* val t_defs = @{thms PLUS_def} *} |
122 ML {* val t_defs = @{thms PLUS_def} *} |
128 |
123 |
129 ML {* |
124 ML {* |
130 fun lift_thm_my_int lthy t = |
125 fun lift_thm_my_int lthy t = |
131 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t |
126 lift_thm lthy qty ty_name rsp_thms t_defs t |
|
127 *} |
|
128 |
|
129 ML {* |
|
130 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty; |
132 *} |
131 *} |
133 |
132 |
134 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *} |
133 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *} |
135 |
134 |
136 lemma plus_assoc_pre: |
135 lemma plus_assoc_pre: |