133 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
129 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
134 ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *} |
130 ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *} |
135 ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *} |
131 ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *} |
136 ML {* val t_defs = @{thms PLUS_def} *} |
132 ML {* val t_defs = @{thms PLUS_def} *} |
137 |
133 |
138 |
134 ML {* |
139 |
135 fun lift_thm_my_int lthy t = |
140 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
136 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t |
|
137 *} |
|
138 |
|
139 lemma plus_sym_pre: |
|
140 shows "intrel (my_plus a b) (my_plus b a)" |
|
141 apply (cases a) |
|
142 apply (cases b) |
|
143 apply (simp) |
|
144 done |
|
145 |
|
146 ML {* lift_thm_my_int @{context} @{thm plus_sym_pre} *} |
|
147 |
|
148 lemma plus_assoc_pre: |
|
149 shows "intrel (my_plus (my_plus i j) k) (my_plus i (my_plus j k))" |
|
150 apply (cases i) |
|
151 apply (cases j) |
|
152 apply (cases k) |
|
153 apply (simp add: intrel_refl) |
|
154 done |
|
155 |
|
156 ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *} |
|
157 |
|
158 |
|
159 |
|
160 |
|
161 |
|
162 |
|
163 |
|
164 |
|
165 text {* Below is the construction site code used if things do now work *} |
|
166 |
|
167 ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *} |
141 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
168 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
142 |
169 |
143 ML {* val (g, thm, othm) = |
170 ML {* val (g, thm, othm) = |
144 Toplevel.program (fn () => |
171 Toplevel.program (fn () => |
145 repabs_eq @{context} t_r consts rty qty |
172 repabs_eq @{context} t_r consts rty qty |
171 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
198 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
172 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |
199 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |
173 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
200 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
174 ML {* ObjectLogic.rulify t_r *} |
201 ML {* ObjectLogic.rulify t_r *} |
175 |
202 |
176 lemma |
203 |
177 fixes i j k::"my_int" |
204 |
178 shows "(PLUS (PLUS i j) k) = (PLUS i (PLUS j k))" |
|
179 apply(unfold PLUS_def) |
|
180 apply(simp add: expand_fun_eq) |
|
181 sorry |
|
182 |
|
183 |
|