165 @{const_name "membship"}, @{const_name "card1"}, |
165 @{const_name "membship"}, @{const_name "card1"}, |
166 @{const_name "append"}, @{const_name "fold1"}]; |
166 @{const_name "append"}, @{const_name "fold1"}]; |
167 *} |
167 *} |
168 |
168 |
169 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
169 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *} |
170 text {* expects atomized definition *} |
170 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
171 ML {* |
|
172 fun add_lower_defs ctxt thm = |
|
173 let |
|
174 val e1 = @{thm fun_cong} OF [thm] |
|
175 val f = eqsubst_thm ctxt @{thms fun_map.simps} e1 |
|
176 in |
|
177 thm :: (add_lower_defs ctxt f) |
|
178 end |
|
179 handle _ => [thm] |
|
180 *} |
|
181 ML {* val fset_defs_pre_sym = map symmetric fset_defs *} |
|
182 ML {* val fset_defs_atom = map atomize_thm fset_defs_pre_sym *} |
|
183 ML {* val fset_defs_all = flat (map (add_lower_defs @{context}) fset_defs_atom) *} |
|
184 ML {* val fset_defs_sym = map (fn t => eq_reflection OF [t]) fset_defs_all *} |
|
185 ML {* val fset_defs_sym = map ObjectLogic.rulify fset_defs_sym *} |
|
186 ML {* val fset_defs_sym = map Thm.varifyT fset_defs_sym *} |
|
187 |
|
188 |
|
189 (* |
|
190 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
|
191 *) |
|
192 |
|
193 |
|
194 thm fun_map.simps |
|
195 text {* Respectfullness *} |
|
196 |
171 |
197 lemma memb_rsp: |
172 lemma memb_rsp: |
198 fixes z |
173 fixes z |
199 assumes a: "list_eq x y" |
174 assumes a: "list_eq x y" |
200 shows "(z memb x) = (z memb y)" |
175 shows "(z memb x) = (z memb y)" |
268 apply (rule RIGHT_RES_FORALL_REGULAR) |
243 apply (rule RIGHT_RES_FORALL_REGULAR) |
269 prefer 2 |
244 prefer 2 |
270 apply (assumption) |
245 apply (assumption) |
271 apply (metis) |
246 apply (metis) |
272 done |
247 done |
273 |
|
274 ML {* |
|
275 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
|
276 let |
|
277 val rt = build_repabs_term lthy thm constructors rty qty; |
|
278 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
|
279 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
|
280 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms)); |
|
281 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
|
282 in |
|
283 (rt, cthm, thm) |
|
284 end |
|
285 *} |
|
286 |
|
287 ML {* |
|
288 fun repabs_eq2 lthy (rt, thm, othm) = |
|
289 let |
|
290 fun tac2 ctxt = |
|
291 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |
|
292 THEN' (rtac othm); |
|
293 val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1); |
|
294 in |
|
295 cthm |
|
296 end |
|
297 *} |
|
298 |
248 |
299 (* The all_prs and ex_prs should be proved for the instance... *) |
249 (* The all_prs and ex_prs should be proved for the instance... *) |
300 ML {* |
250 ML {* |
301 fun r_mk_comb_tac_fset ctxt = |
251 fun r_mk_comb_tac_fset ctxt = |
302 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
252 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
418 |
368 |
419 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
369 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
420 ML {* ObjectLogic.rulify rthm *} |
370 ML {* ObjectLogic.rulify rthm *} |
421 |
371 |
422 |
372 |
423 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
373 ML {* val card1_suc_a = atomize_thm @{thm card1_suc} *} |
424 |
374 |
425 prove card1_suc_r_p: {* |
375 prove card1_suc_r_p: {* |
426 build_regularize_goal (atomize_thm @{thm card1_suc}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
376 build_regularize_goal (atomize_thm @{thm card1_suc}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
427 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) |
377 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) |
428 done |
378 done |