170 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
170 ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *} |
171 |
171 |
172 thm fun_map.simps |
172 thm fun_map.simps |
173 text {* Respectfullness *} |
173 text {* Respectfullness *} |
174 |
174 |
175 lemma mem_respects: |
175 lemma memb_rsp: |
176 fixes z |
176 fixes z |
177 assumes a: "list_eq x y" |
177 assumes a: "list_eq x y" |
178 shows "(z memb x) = (z memb y)" |
178 shows "(z memb x) = (z memb y)" |
179 using a by induct auto |
179 using a by induct auto |
|
180 |
|
181 lemma ho_memb_rsp: |
|
182 "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)" |
|
183 apply (simp add: FUN_REL.simps) |
|
184 apply (metis memb_rsp) |
|
185 done |
180 |
186 |
181 lemma card1_rsp: |
187 lemma card1_rsp: |
182 fixes a b :: "'a list" |
188 fixes a b :: "'a list" |
183 assumes e: "a \<approx> b" |
189 assumes e: "a \<approx> b" |
184 shows "card1 a = card1 b" |
190 shows "card1 a = card1 b" |
185 using e apply induct |
191 using e apply induct |
186 apply (simp_all add:mem_respects) |
192 apply (simp_all add:memb_rsp) |
187 done |
193 done |
188 |
194 |
189 lemma cons_preserves: |
195 lemma cons_rsp: |
190 fixes z |
196 fixes z |
191 assumes a: "xs \<approx> ys" |
197 assumes a: "xs \<approx> ys" |
192 shows "(z # xs) \<approx> (z # ys)" |
198 shows "(z # xs) \<approx> (z # ys)" |
193 using a by (rule list_eq.intros(5)) |
199 using a by (rule list_eq.intros(5)) |
|
200 |
|
201 lemma ho_cons_rsp: |
|
202 "op = ===> op \<approx> ===> op \<approx> op # op #" |
|
203 apply (simp add: FUN_REL.simps) |
|
204 apply (metis cons_rsp) |
|
205 done |
194 |
206 |
195 lemma append_respects_fst: |
207 lemma append_respects_fst: |
196 assumes a : "list_eq l1 l2" |
208 assumes a : "list_eq l1 l2" |
197 shows "list_eq (l1 @ s) (l2 @ s)" |
209 shows "list_eq (l1 @ s) (l2 @ s)" |
198 using a |
210 using a |
249 rtac @{thm IDENTITY_QUOTIENT} |
261 rtac @{thm IDENTITY_QUOTIENT} |
250 ]) |
262 ]) |
251 *} |
263 *} |
252 |
264 |
253 ML {* |
265 ML {* |
|
266 fun LAMBDA_RES_TAC ctxt = |
|
267 case (term_of o #concl o fst) (Subgoal.focus ctxt 1 (Isar.goal ())) of |
|
268 (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) => |
|
269 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
270 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
271 | _ => fn _ => no_tac |
|
272 *} |
|
273 |
|
274 |
|
275 ML {* |
254 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
276 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
255 (FIRST' [ |
277 (FIRST' [ |
256 rtac @{thm FUN_QUOTIENT}, |
278 rtac @{thm FUN_QUOTIENT}, |
257 rtac quot_thm, |
279 rtac quot_thm, |
258 rtac @{thm IDENTITY_QUOTIENT}, |
280 rtac @{thm IDENTITY_QUOTIENT}, |
259 rtac @{thm ext}, |
281 rtac @{thm ext}, |
260 rtac trans_thm, |
282 rtac trans_thm, |
|
283 LAMBDA_RES_TAC ctxt, |
261 res_forall_rsp_tac ctxt, |
284 res_forall_rsp_tac ctxt, |
262 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
285 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
|
286 rtac refl, |
263 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
287 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
264 rtac reflex_thm, |
288 rtac reflex_thm, |
265 atac, |
289 atac, |
266 ( |
290 ( |
267 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) |
291 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) |
268 THEN_ALL_NEW (fn _ => no_tac) |
292 THEN_ALL_NEW (fn _ => no_tac) |
269 ) |
293 ) |
278 |
302 |
279 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
303 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
280 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
304 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
281 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
305 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
282 |
306 |
|
307 |
283 prove list_induct_tr: trm_r |
308 prove list_induct_tr: trm_r |
284 apply (atomize(full)) |
309 apply (atomize(full)) |
285 (* APPLY_RSP_TAC *) |
310 (* APPLY_RSP_TAC *) |
286 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
311 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
287 (* LAMBDA_RES_TAC *) |
312 (* LAMBDA_RES_TAC *) |
288 apply (simp only: FUN_REL.simps) |
313 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
289 apply (rule allI) |
|
290 apply (rule allI) |
|
291 apply (rule impI) |
|
292 (* MK_COMB_TAC *) |
314 (* MK_COMB_TAC *) |
293 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
315 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
294 (* MK_COMB_TAC *) |
316 (* MK_COMB_TAC *) |
295 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
317 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
296 (* REFL_TAC *) |
318 (* REFL_TAC *) |
298 (* MK_COMB_TAC *) |
320 (* MK_COMB_TAC *) |
299 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
321 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
300 (* MK_COMB_TAC *) |
322 (* MK_COMB_TAC *) |
301 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
323 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
302 (* REFL_TAC *) |
324 (* REFL_TAC *) |
303 apply (simp) |
325 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
304 (* APPLY_RSP_TAC *) |
326 (* APPLY_RSP_TAC *) |
305 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
327 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
306 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
328 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
307 apply (simp only: FUN_REL.simps) |
329 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
308 apply (rule allI) |
|
309 apply (rule allI) |
|
310 apply (rule impI) |
|
311 (* MK_COMB_TAC *) |
330 (* MK_COMB_TAC *) |
312 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
331 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
313 (* MK_COMB_TAC *) |
332 (* MK_COMB_TAC *) |
314 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
333 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
315 (* REFL_TAC *) |
334 (* REFL_TAC *) |
317 (* APPLY_RSP *) |
336 (* APPLY_RSP *) |
318 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
337 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
319 (* MK_COMB_TAC *) |
338 (* MK_COMB_TAC *) |
320 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
339 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
321 (* REFL_TAC *) |
340 (* REFL_TAC *) |
322 apply (simp) |
341 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
323 (* W(C (curry op THEN) (G... *) |
342 (* W(C (curry op THEN) (G... *) |
|
343 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
324 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
344 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
325 (* CONS respects *) |
345 (* CONS respects *) |
326 apply (simp add: FUN_REL.simps) |
346 apply (rule ho_cons_rsp) |
327 apply (rule allI) |
347 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
328 apply (rule allI) |
348 apply (subst FUN_REL.simps) |
329 apply (rule allI) |
|
330 apply (rule impI) |
|
331 apply (rule cons_preserves) |
|
332 apply (assumption) |
|
333 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
334 apply (simp only: FUN_REL.simps) |
|
335 apply (rule allI) |
349 apply (rule allI) |
336 apply (rule allI) |
350 apply (rule allI) |
337 apply (rule impI) |
351 apply (rule impI) |
338 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
352 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
339 done |
353 done |
358 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
372 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
359 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
373 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
360 prove m2_t_p: m2_t_g |
374 prove m2_t_p: m2_t_g |
361 apply (atomize(full)) |
375 apply (atomize(full)) |
362 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
376 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
363 apply (simp add: FUN_REL.simps) |
|
364 prefer 2 |
377 prefer 2 |
365 apply (simp only: FUN_REL.simps) |
378 apply (subst FUN_REL.simps) |
366 apply (rule allI) |
379 apply (rule allI) |
367 apply (rule allI) |
380 apply (rule allI) |
368 apply (rule impI) |
381 apply (rule impI) |
369 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
382 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
370 prefer 2 |
383 prefer 2 |
371 apply (simp only: FUN_REL.simps) |
384 apply (subst FUN_REL.simps) |
372 apply (rule allI) |
385 apply (rule allI) |
373 apply (rule allI) |
386 apply (rule allI) |
374 apply (rule impI) |
387 apply (rule impI) |
375 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
388 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
376 apply (simp only: FUN_REL.simps) |
389 apply (subst FUN_REL.simps) |
377 apply (rule allI) |
390 apply (rule allI) |
378 apply (rule allI) |
391 apply (rule allI) |
379 apply (rule impI) |
392 apply (rule impI) |
380 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
393 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
381 apply (simp only: FUN_REL.simps) |
394 apply (rule ho_memb_rsp) |
382 apply (rule allI) |
395 apply (rule ho_cons_rsp) |
383 apply (rule allI) |
396 apply (rule ho_memb_rsp) |
384 apply (rule impI) |
|
385 apply (rule allI) |
|
386 apply (rule allI) |
|
387 apply (rule impI) |
|
388 apply (simp add:mem_respects) |
|
389 apply (simp only: FUN_REL.simps) |
|
390 apply (rule allI) |
|
391 apply (rule allI) |
|
392 apply (rule impI) |
|
393 apply (rule allI) |
|
394 apply (rule allI) |
|
395 apply (rule impI) |
|
396 apply (simp add:cons_preserves) |
|
397 apply (simp only: FUN_REL.simps) |
|
398 apply (rule allI) |
|
399 apply (rule allI) |
|
400 apply (rule impI) |
|
401 apply (rule allI) |
|
402 apply (rule allI) |
|
403 apply (rule impI) |
|
404 apply (simp add:mem_respects) |
|
405 apply (auto) |
397 apply (auto) |
406 done |
398 done |
407 |
399 |
408 prove m2_t: m2_t |
400 prove m2_t: m2_t |
409 apply (simp only: m2_t_p[symmetric]) |
401 apply (simp only: m2_t_p[symmetric]) |
410 apply (tactic {* rtac m2_r 1 *}) |
402 apply (tactic {* rtac m2_r 1 *}) |
411 done |
403 done |
412 |
404 |
413 lemma id_apply2 [simp]: "id x \<equiv> x" |
405 lemma id_apply2 [simp]: "id x \<equiv> x" |
414 by (simp add: id_def) |
406 by (simp add: id_def) |
415 |
|
416 |
407 |
417 thm LAMBDA_PRS |
408 thm LAMBDA_PRS |
418 ML {* |
409 ML {* |
419 val t = prop_of @{thm LAMBDA_PRS} |
410 val t = prop_of @{thm LAMBDA_PRS} |
420 val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS} |
411 val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS} |
441 end |
432 end |
442 *} |
433 *} |
443 ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *} |
434 ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *} |
444 ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *} |
435 ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *} |
445 ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *} |
436 ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *} |
446 ML {* rwrs; m2_t' *} |
437 ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *} |
447 ML {* eqsubst_thm @{context} [rwrs] m2_t' *} |
438 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
448 thm INSERT_def |
439 ML {* ObjectLogic.rulify rthm *} |
449 |
440 |
450 |
441 |
451 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
442 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
452 |
443 |
453 prove card1_suc_r: {* |
444 prove card1_suc_r: {* |
472 |
463 |
473 lemma yy: |
464 lemma yy: |
474 shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" |
465 shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" |
475 unfolding IN_def EMPTY_def |
466 unfolding IN_def EMPTY_def |
476 apply(rule_tac f="(op =) False" in arg_cong) |
467 apply(rule_tac f="(op =) False" in arg_cong) |
477 apply(rule mem_respects) |
468 apply(rule memb_rsp) |
478 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
469 apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp) |
479 apply(rule list_eq.intros) |
470 apply(rule list_eq.intros) |
480 done |
471 done |
481 |
472 |
482 lemma |
473 lemma |
491 shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) = |
482 shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) = |
492 ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))" |
483 ((x=y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))" |
493 unfolding IN_def INSERT_def |
484 unfolding IN_def INSERT_def |
494 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong) |
485 apply(rule_tac f="(op \<or>) (x=y)" in arg_cong) |
495 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) |
486 apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) |
496 apply(rule mem_respects) |
487 apply(rule memb_rsp) |
497 apply(rule list_eq.intros(3)) |
488 apply(rule list_eq.intros(3)) |
498 apply(unfold REP_fset_def ABS_fset_def) |
489 apply(unfold REP_fset_def ABS_fset_def) |
499 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
490 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) |
500 apply(rule list_eq_refl) |
491 apply(rule list_eq_refl) |
501 done |
492 done |
552 (LocalDefs.unfold_tac @{context} fset_defs) THEN |
543 (LocalDefs.unfold_tac @{context} fset_defs) THEN |
553 ObjectLogic.full_atomize_tac 1 THEN |
544 ObjectLogic.full_atomize_tac 1 THEN |
554 REPEAT_ALL_NEW (FIRST' [ |
545 REPEAT_ALL_NEW (FIRST' [ |
555 rtac @{thm list_eq_refl}, |
546 rtac @{thm list_eq_refl}, |
556 rtac @{thm cons_preserves}, |
547 rtac @{thm cons_preserves}, |
557 rtac @{thm mem_respects}, |
548 rtac @{thm memb_rsp}, |
558 rtac @{thm card1_rsp}, |
549 rtac @{thm card1_rsp}, |
559 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
550 rtac @{thm QUOT_TYPE_I_fset.R_trans2}, |
560 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
551 CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})), |
561 Cong_Tac.cong_tac @{thm cong}, |
552 Cong_Tac.cong_tac @{thm cong}, |
562 rtac @{thm ext} |
553 rtac @{thm ext} |