371 induct_prove qtys props qinduct (K ss_tac) ctxt' |
375 induct_prove qtys props qinduct (K ss_tac) ctxt' |
372 |> ProofContext.export ctxt' ctxt |
376 |> ProofContext.export ctxt' ctxt |
373 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
377 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
374 end |
378 end |
375 |
379 |
|
380 |
|
381 (** proves strong exhauts theorems **) |
|
382 |
|
383 |
|
384 (* fixme: move into nominal_library *) |
|
385 fun abs_const bmode ty = |
|
386 let |
|
387 val (const_name, binder_ty, abs_ty) = |
|
388 case bmode of |
|
389 Lst => (@{const_name "Abs_lst"}, @{typ "atom list"}, @{type_name abs_lst}) |
|
390 | Set => (@{const_name "Abs_set"}, @{typ "atom set"}, @{type_name abs_set}) |
|
391 | Res => (@{const_name "Abs_res"}, @{typ "atom set"}, @{type_name abs_res}) |
|
392 in |
|
393 Const (const_name, [binder_ty, ty] ---> Type (abs_ty, [ty])) |
|
394 end |
|
395 |
|
396 fun mk_abs bmode trm1 trm2 = |
|
397 abs_const bmode (fastype_of trm2) $ trm1 $ trm2 |
|
398 |
|
399 fun is_abs_eq thm = |
|
400 let |
|
401 fun is_abs trm = |
|
402 case (head_of trm) of |
|
403 Const (@{const_name "Abs_set"}, _) => true |
|
404 | Const (@{const_name "Abs_lst"}, _) => true |
|
405 | Const (@{const_name "Abs_res"}, _) => true |
|
406 | _ => false |
|
407 in |
|
408 thm |> prop_of |
|
409 |> HOLogic.dest_Trueprop |
|
410 |> HOLogic.dest_eq |
|
411 |> fst |
|
412 |> is_abs |
|
413 end |
|
414 |
|
415 |
|
416 (* adds a freshness condition to the assumptions *) |
|
417 fun mk_ecase_prems lthy c (params, prems, concl) bclauses = |
|
418 let |
|
419 val tys = map snd params |
|
420 val binders = get_all_binders bclauses |
|
421 |
|
422 fun prep_binder (opt, i) = |
|
423 let |
|
424 val t = Bound (length tys - i - 1) |
|
425 in |
|
426 case opt of |
|
427 NONE => setify_ty lthy (nth tys i) t |
|
428 | SOME bn => to_set_ty (fastype_of1 (tys, bn $ t)) (bn $ t) |
|
429 end |
|
430 |
|
431 val prems' = |
|
432 case binders of |
|
433 [] => prems (* case: no binders *) |
|
434 | _ => binders (* case: binders *) |
|
435 |> map prep_binder |
|
436 |> fold_union_env tys |
|
437 |> (fn t => mk_fresh_star t c) |
|
438 |> (fn t => HOLogic.mk_Trueprop t :: prems) |
|
439 in |
|
440 mk_full_horn params prems' concl |
|
441 end |
|
442 |
|
443 |
|
444 (* derives the freshness theorem that there exists a p, such that |
|
445 (p o as) #* (c, t1,..., tn) *) |
|
446 fun fresh_thm ctxt c parms binders bn_finite_thms = |
|
447 let |
|
448 fun prep_binder (opt, i) = |
|
449 case opt of |
|
450 NONE => setify ctxt (nth parms i) |
|
451 | SOME bn => to_set (bn $ (nth parms i)) |
|
452 |
|
453 fun prep_binder2 (opt, i) = |
|
454 case opt of |
|
455 NONE => atomify ctxt (nth parms i) |
|
456 | SOME bn => bn $ (nth parms i) |
|
457 |
|
458 val rhs = HOLogic.mk_tuple ([c] @ parms @ (map prep_binder2 binders)) |
|
459 val lhs = binders |
|
460 |> map prep_binder |
|
461 |> fold_union |
|
462 |> mk_perm (Bound 0) |
|
463 |
|
464 val goal = mk_fresh_star lhs rhs |
|
465 |> (fn t => HOLogic.mk_exists ("p", @{typ perm}, t)) |
|
466 |> HOLogic.mk_Trueprop |
|
467 |
|
468 val ss = bn_finite_thms @ @{thms supp_Pair finite_supp finite_sets_supp} |
|
469 @ @{thms finite.intros finite_Un finite_set finite_fset} |
|
470 in |
|
471 Goal.prove ctxt [] [] goal |
|
472 (K (HEADGOAL (rtac @{thm at_set_avoiding1} |
|
473 THEN_ALL_NEW (simp_tac (HOL_ss addsimps ss))))) |
|
474 end |
|
475 |
|
476 |
|
477 (* derives an abs_eq theorem of the form |
|
478 |
|
479 Exists q. [as].x = [p o as].(q o x) for non-recursive binders |
|
480 Exists q. [as].x = [q o as].(q o x) for recursive binders |
|
481 *) |
|
482 fun abs_eq_thm ctxt fprops p parms bn_finite_thms bn_eqvt permute_bns |
|
483 (bclause as (BC (bmode, binders, bodies))) = |
|
484 case binders of |
|
485 [] => [] |
|
486 | _ => |
|
487 let |
|
488 val rec_flag = is_recursive_binder bclause |
|
489 val binder_trm = comb_binders ctxt bmode parms binders |
|
490 val body_trm = foldl1 HOLogic.mk_prod (map (nth parms) bodies) |
|
491 |
|
492 val abs_lhs = mk_abs bmode binder_trm body_trm |
|
493 val abs_rhs = |
|
494 if rec_flag |
|
495 then mk_abs bmode (mk_perm (Bound 0) binder_trm) (mk_perm (Bound 0) body_trm) |
|
496 else mk_abs bmode (mk_perm p binder_trm) (mk_perm (Bound 0) body_trm) |
|
497 |
|
498 val abs_eq = HOLogic.mk_eq (abs_lhs, abs_rhs) |
|
499 val peq = HOLogic.mk_eq (mk_perm (Bound 0) binder_trm, mk_perm p binder_trm) |
|
500 |
|
501 val goal = HOLogic.mk_conj (abs_eq, peq) |
|
502 |> (fn t => HOLogic.mk_exists ("q", @{typ "perm"}, t)) |
|
503 |> HOLogic.mk_Trueprop |
|
504 |
|
505 val ss = fprops @ bn_finite_thms @ @{thms set.simps set_append union_eqvt} |
|
506 @ @{thms fresh_star_Un fresh_star_Pair fresh_star_list fresh_star_singleton fresh_star_fset |
|
507 fresh_star_set} @ @{thms finite.intros finite_fset} |
|
508 |
|
509 val tac1 = |
|
510 if rec_flag |
|
511 then resolve_tac @{thms Abs_rename_set' Abs_rename_res' Abs_rename_lst'} |
|
512 else resolve_tac @{thms Abs_rename_set Abs_rename_res Abs_rename_lst} |
|
513 |
|
514 val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] |
|
515 in |
|
516 [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) |
|
517 |> (if rec_flag |
|
518 then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] |
|
519 else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ] |
|
520 end |
|
521 |
|
522 |
|
523 val setify = @{lemma "xs = ys ==> set xs = set ys" by simp} |
|
524 |
|
525 fun case_tac ctxt c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
|
526 prems bclausess qexhaust_thm = |
|
527 let |
|
528 fun aux_tac prem bclauses = |
|
529 case (get_all_binders bclauses) of |
|
530 [] => EVERY' [rtac prem, atac] |
|
531 | binders => Subgoal.SUBPROOF (fn {params, prems, concl, context = ctxt, ...} => |
|
532 let |
|
533 val parms = map (term_of o snd) params |
|
534 val fthm = fresh_thm ctxt c parms binders bn_finite_thms |
|
535 |
|
536 val ss = @{thms fresh_star_Pair union_eqvt fresh_star_Un} |
|
537 val (([(_, fperm)], fprops), ctxt') = Obtain.result |
|
538 (K (EVERY1 [etac exE, |
|
539 full_simp_tac (HOL_basic_ss addsimps ss), |
|
540 REPEAT o (etac @{thm conjE})])) [fthm] ctxt |
|
541 |
|
542 val abs_eq_thms = flat |
|
543 (map (abs_eq_thm ctxt fprops (term_of fperm) parms bn_finite_thms bn_eqvt permute_bns) bclauses) |
|
544 |
|
545 val ((_, eqs), ctxt'') = Obtain.result |
|
546 (K (EVERY1 |
|
547 [ REPEAT o (etac @{thm exE}), |
|
548 REPEAT o (etac @{thm conjE}), |
|
549 REPEAT o (dtac setify), |
|
550 full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' |
|
551 |
|
552 val (abs_eqs, peqs) = split_filter is_abs_eq eqs |
|
553 |
|
554 val fprops' = |
|
555 map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops |
|
556 @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops |
|
557 |
|
558 (* for freshness conditions *) |
|
559 val tac1 = SOLVED' (EVERY' |
|
560 [ simp_tac (HOL_basic_ss addsimps peqs), |
|
561 rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), |
|
562 conj_tac (DETERM o resolve_tac fprops') ]) |
|
563 |
|
564 (* for equalities between constructors *) |
|
565 val tac2 = SOLVED' (EVERY' |
|
566 [ rtac (@{thm ssubst} OF prems), |
|
567 rewrite_goal_tac (map safe_mk_equiv eq_iff_thms), |
|
568 rewrite_goal_tac (map safe_mk_equiv abs_eqs), |
|
569 conj_tac (DETERM o resolve_tac (@{thms refl} @ perm_bn_alphas)) ]) |
|
570 |
|
571 (* proves goal "P" *) |
|
572 val side_thm = Goal.prove ctxt'' [] [] (term_of concl) |
|
573 (K (EVERY1 [ rtac prem, RANGE [tac1, tac2] ])) |
|
574 |> singleton (ProofContext.export ctxt'' ctxt) |
|
575 in |
|
576 rtac side_thm 1 |
|
577 end) ctxt |
|
578 in |
|
579 EVERY1 [rtac qexhaust_thm, RANGE (map2 aux_tac prems bclausess)] |
|
580 end |
|
581 |
|
582 |
|
583 fun prove_strong_exhausts lthy exhausts bclausesss bn_finite_thms eq_iff_thms bn_eqvt permute_bns |
|
584 perm_bn_alphas = |
|
585 let |
|
586 val ((_, exhausts'), lthy') = Variable.import true exhausts lthy |
|
587 |
|
588 val ([c, a], lthy'') = Variable.variant_fixes ["c", "'a"] lthy' |
|
589 val c = Free (c, TFree (a, @{sort fs})) |
|
590 |
|
591 val (ecases, main_concls) = exhausts' (* ecases are of the form (params, prems, concl) *) |
|
592 |> map prop_of |
|
593 |> map Logic.strip_horn |
|
594 |> split_list |
|
595 |
|
596 val ecases' = (map o map) strip_full_horn ecases |
|
597 |
|
598 val premss = (map2 o map2) (mk_ecase_prems lthy'' c) ecases' bclausesss |
|
599 |
|
600 fun tac bclausess exhaust {prems, context} = |
|
601 case_tac context c bn_finite_thms eq_iff_thms bn_eqvt permute_bns perm_bn_alphas |
|
602 prems bclausess exhaust |
|
603 |
|
604 fun prove prems bclausess exhaust concl = |
|
605 Goal.prove lthy'' [] prems concl (tac bclausess exhaust) |
|
606 in |
|
607 map4 prove premss bclausesss exhausts' main_concls |
|
608 |> ProofContext.export lthy'' lthy |
|
609 end |
|
610 |
376 end (* structure *) |
611 end (* structure *) |
377 |
612 |