equal
deleted
inserted
replaced
156 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" *} |
156 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" *} |
157 (* ML {* val consts = [@{const_name my_plus}] *}*) |
157 (* ML {* val consts = [@{const_name my_plus}] *}*) |
158 ML {* val consts = lookup_quot_consts defs *} |
158 ML {* val consts = lookup_quot_consts defs *} |
159 ML {* val t_a = atomize_thm @{thm ho_tst} *} |
159 ML {* val t_a = atomize_thm @{thm ho_tst} *} |
160 |
160 |
161 (*prove t_r: {* build_regularize_goal t_a rty rel @{context} *} |
161 (* |
|
162 prove t_r: {* build_regularize_goal t_a rty rel @{context} *} |
162 ML_prf {* fun tac ctxt = |
163 ML_prf {* fun tac ctxt = |
163 (ObjectLogic.full_atomize_tac) THEN' |
164 (ObjectLogic.full_atomize_tac) THEN' |
164 REPEAT_ALL_NEW (FIRST' [ |
165 REPEAT_ALL_NEW (FIRST' [ |
165 rtac rel_refl, |
166 rtac rel_refl, |
166 atac, |
167 atac, |
181 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
182 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
182 ML {* |
183 ML {* |
183 val rt = build_repabs_term @{context} t_r consts rty qty |
184 val rt = build_repabs_term @{context} t_r consts rty qty |
184 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
185 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
185 *} |
186 *} |
|
187 *) |
186 |
188 |
187 lemma foldl_rsp: |
189 lemma foldl_rsp: |
188 "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===> |
190 "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===> |
189 IntEx.intrel ===> op = ===> IntEx.intrel) |
191 IntEx.intrel ===> op = ===> IntEx.intrel) |
190 foldl foldl" |
192 foldl foldl" |