134 |
134 |
135 ML {* val qty = @{typ "my_int"} *} |
135 ML {* val qty = @{typ "my_int"} *} |
136 ML {* val ty_name = "my_int" *} |
136 ML {* val ty_name = "my_int" *} |
137 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
137 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
138 ML {* val defs = @{thms PLUS_def} *} |
138 ML {* val defs = @{thms PLUS_def} *} |
|
139 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
|
140 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} |
|
141 ML {* val consts = lookup_quot_consts defs *} |
139 |
142 |
140 ML {* |
143 ML {* |
141 fun lift_thm_my_int lthy t = |
144 fun lift_thm_my_int lthy t = |
142 lift_thm lthy qty ty_name rsp_thms defs t |
145 lift_thm lthy qty ty_name rsp_thms defs t |
143 *} |
|
144 |
|
145 ML {* |
|
146 fun lift_thm_g_my_int lthy t g = |
146 fun lift_thm_g_my_int lthy t g = |
147 lift_thm_goal lthy qty ty_name rsp_thms defs t g |
147 lift_thm_goal lthy qty ty_name rsp_thms defs t g |
148 *} |
148 fun lift_tac_fset lthy t = |
149 |
149 lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs |
150 print_quotients |
150 *} |
151 ML {* quotdata_lookup @{context} "IntEx.my_int" *} |
151 |
152 ML {* quotdata_lookup @{context} "my_int" *} |
152 lemma "PLUS a b = PLUS b a" |
153 |
153 by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *}) |
154 ML {* |
|
155 val test = lift_thm_my_int @{context} @{thm plus_sym_pre} |
|
156 *} |
|
157 |
|
158 ML {* |
|
159 lift_thm_g_my_int @{context} @{thm plus_sym_pre} @{term "PLUS a b = PLUS b a"} |
|
160 *} |
|
161 |
154 |
162 lemma plus_assoc_pre: |
155 lemma plus_assoc_pre: |
163 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
156 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
164 apply (cases i) |
157 apply (cases i) |
165 apply (cases j) |
158 apply (cases j) |
166 apply (cases k) |
159 apply (cases k) |
167 apply (simp) |
160 apply (simp) |
168 done |
161 done |
169 |
162 |
170 ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *} |
163 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" |
171 |
164 by (tactic {* lift_tac_fset @{context} @{thm plus_assoc_pre} 1 *}) |
172 ML {* lift_thm_g_my_int @{context} @{thm plus_assoc_pre} |
165 |
173 @{term "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"} *} |
|
174 |
166 |
175 ML {* |
167 ML {* |
176 mk_REGULARIZE_goal @{context} |
168 mk_REGULARIZE_goal @{context} |
177 @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"} |
169 @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"} |
178 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
170 @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"} |
284 val rt = build_repabs_term @{context} t_r consts rty qty |
276 val rt = build_repabs_term @{context} t_r consts rty qty |
285 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
277 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
286 *} |
278 *} |
287 |
279 |
288 |
280 |
289 lemma foldl_rsp: |
281 |
290 "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===> |
|
291 IntEx.intrel ===> op = ===> IntEx.intrel) |
|
292 foldl foldl" |
|
293 apply (simp only:FUN_REL.simps) |
|
294 apply (rule allI) |
|
295 apply (rule allI) |
|
296 apply (rule impI) |
|
297 apply (rule allI) |
|
298 apply (rule allI) |
|
299 apply (rule impI) |
|
300 apply (rule allI) |
|
301 apply (rule allI) |
|
302 apply (rule impI) |
|
303 apply (simp only:) |
|
304 apply (rule list.induct) |
|
305 apply (simp) |
|
306 apply (simp only: foldl.simps) |
|
307 sorry |
|
308 |
|
309 ML {* val rsp_thms = @{thm foldl_rsp} :: rsp_thms *} |
|
310 prove t_t: rg |
282 prove t_t: rg |
311 apply(atomize(full)) |
283 apply(atomize(full)) |
312 ML_prf {* fun r_mk_comb_tac_int lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
284 ML_prf {* fun r_mk_comb_tac_int lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
313 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_int @{context}) 1 *}) |
285 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_int @{context}) 1 *}) |
314 done |
286 done |