1 signature QUOTIENT_TACS = |
1 signature QUOTIENT_TACS = |
2 sig |
2 sig |
3 val regularize_tac: Proof.context -> int -> tactic |
3 val regularize_tac: Proof.context -> int -> tactic |
4 val injection_tac: Proof.context -> int -> tactic |
4 val injection_tac: Proof.context -> int -> tactic |
5 val all_injection_tac: Proof.context -> int -> tactic |
5 val all_injection_tac: Proof.context -> int -> tactic |
6 val clean_tac: Proof.context -> int -> tactic |
6 val clean_tac: Proof.context -> int -> tactic |
7 val procedure_tac: Proof.context -> thm -> int -> tactic |
7 val procedure_tac: Proof.context -> thm -> int -> tactic |
8 val lift_tac: Proof.context -> thm -> int -> tactic |
8 val lift_tac: Proof.context -> thm -> int -> tactic |
9 val quotient_tac: Proof.context -> int -> tactic |
9 val quotient_tac: Proof.context -> int -> tactic |
10 val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic |
10 val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic |
11 end; |
11 end; |
12 |
12 |
13 structure Quotient_Tacs: QUOTIENT_TACS = |
13 structure Quotient_Tacs: QUOTIENT_TACS = |
14 struct |
14 struct |
15 |
15 |
68 (REPEAT_ALL_NEW (FIRST' |
68 (REPEAT_ALL_NEW (FIRST' |
69 [rtac @{thm identity_quotient}, |
69 [rtac @{thm identity_quotient}, |
70 resolve_tac (quotient_rules_get ctxt)])) |
70 resolve_tac (quotient_rules_get ctxt)])) |
71 |
71 |
72 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
72 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
73 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
73 val quotient_solver = |
|
74 Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
74 |
75 |
75 fun solve_quotient_assm ctxt thm = |
76 fun solve_quotient_assm ctxt thm = |
76 case Seq.pull (quotient_tac ctxt 1 thm) of |
77 case Seq.pull (quotient_tac ctxt 1 thm) of |
77 SOME (t, _) => t |
78 SOME (t, _) => t |
78 | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing." |
79 | _ => error "Solve_quotient_assm failed. Possibly a quotient theorem is missing." |
85 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
86 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
86 |
87 |
87 fun get_match_inst thy pat trm = |
88 fun get_match_inst thy pat trm = |
88 let |
89 let |
89 val univ = Unify.matchers thy [(pat, trm)] |
90 val univ = Unify.matchers thy [(pat, trm)] |
90 val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) |
91 val SOME (env, _) = Seq.pull univ (* raises BIND, if no unifier *) |
91 val tenv = Vartab.dest (Envir.term_env env) |
92 val tenv = Vartab.dest (Envir.term_env env) |
92 val tyenv = Vartab.dest (Envir.type_env env) |
93 val tyenv = Vartab.dest (Envir.type_env env) |
93 in |
94 in |
94 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
95 (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) |
95 end |
96 end |
129 calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 |
130 calculate_inst ctxt @{thm bex_reg_eqv_range[THEN eq_reflection]} redex R1 R2 |
130 |
131 |
131 | _ => NONE |
132 | _ => NONE |
132 end |
133 end |
133 |
134 |
134 (* 0. preliminary simplification step according to *) |
135 (* |
135 (* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *) |
136 0. preliminary simplification step according to |
136 (* ball_reg_eqv_range bex_reg_eqv_range *) |
137 ball_reg_eqv bex_reg_eqv babs_reg_eqv ball_reg_eqv_range bex_reg_eqv_range |
137 (* *) |
138 |
138 (* 1. eliminating simple Ball/Bex instances *) |
139 1. eliminating simple Ball/Bex instances (ball_reg_right bex_reg_left) |
139 (* thm ball_reg_right bex_reg_left *) |
140 |
140 (* *) |
141 2. monos |
141 (* 2. monos *) |
142 |
142 (* *) |
143 3. commutation rules for ball and bex (ball_all_comm bex_ex_comm) |
143 (* 3. commutation rules for ball and bex *) |
144 |
144 (* thm ball_all_comm bex_ex_comm *) |
145 4. then rel-equalities, which need to be instantiated with 'eq_imp_rel' |
145 (* *) |
146 to avoid loops |
146 (* 4. then rel-equalities, which need to be *) |
147 |
147 (* instantiated with the followig theorem *) |
148 5. then simplification like 0 |
148 (* to avoid loops: *) |
149 |
149 (* thm eq_imp_rel *) |
150 finally jump back to 1 *) |
150 (* *) |
|
151 (* 5. then simplification like 0 *) |
|
152 (* *) |
|
153 (* finally jump back to 1 *) |
|
154 |
|
155 fun regularize_tac ctxt = |
151 fun regularize_tac ctxt = |
156 let |
152 let |
157 val thy = ProofContext.theory_of ctxt |
153 val thy = ProofContext.theory_of ctxt |
158 val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} |
154 val ball_pat = @{term "Ball (Respects (R1 ===> R2)) P"} |
159 val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} |
155 val bex_pat = @{term "Bex (Respects (R1 ===> R2)) P"} |
382 |
378 |
383 fun injection_step_tac ctxt rel_refl = |
379 fun injection_step_tac ctxt rel_refl = |
384 FIRST' [ |
380 FIRST' [ |
385 injection_match_tac ctxt, |
381 injection_match_tac ctxt, |
386 |
382 |
387 (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) |
383 (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) |
388 apply_rsp_tac ctxt THEN' |
384 apply_rsp_tac ctxt THEN' |
389 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
385 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
390 |
386 |
391 (* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *) |
387 (* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *) |
392 (* merge with previous tactic *) |
388 (* merge with previous tactic *) |
393 Cong_Tac.cong_tac @{thm cong} THEN' |
389 Cong_Tac.cong_tac @{thm cong} THEN' |
394 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
390 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], |
395 |
391 |
396 (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *) |
392 (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *) |
397 rtac @{thm ext} THEN' quot_true_tac ctxt unlam, |
393 rtac @{thm ext} THEN' quot_true_tac ctxt unlam, |
398 |
394 |
399 (* resolving with R x y assumptions *) |
395 (* resolving with R x y assumptions *) |
400 atac, |
396 atac, |
401 |
397 |
402 (* reflexivity of the basic relations *) |
398 (* reflexivity of the basic relations *) |
403 (* R ... ... *) |
399 (* R ... ... *) |
404 resolve_tac rel_refl] |
400 resolve_tac rel_refl] |
405 |
401 |
406 fun injection_tac ctxt = |
402 fun injection_tac ctxt = |
511 val thy = ProofContext.theory_of lthy; |
507 val thy = ProofContext.theory_of lthy; |
512 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
508 val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) |
513 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
509 (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) |
514 val prs = prs_rules_get lthy |
510 val prs = prs_rules_get lthy |
515 val ids = id_simps_get lthy |
511 val ids = id_simps_get lthy |
516 |
512 |
517 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
513 fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver |
518 val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs}) |
514 val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs}) |
519 val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) |
515 val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) |
520 in |
516 in |
521 EVERY' [simp_tac ss1, |
517 EVERY' [simp_tac ss1, |
522 fun_map_tac lthy, |
518 fun_map_tac lthy, |
523 lambda_prs_tac lthy, |
519 lambda_prs_tac lthy, |
524 simp_tac ss2, |
520 simp_tac ss2, |
525 TRY o rtac refl] |
521 TRY o rtac refl] |
526 end |
522 end |
527 |
523 |
528 |
524 |
529 |
525 |
530 (** Tactic for Generalising Free Variables in a Goal **) |
526 (** Tactic for Generalising Free Variables in a Goal **) |
541 |
537 |
542 fun apply_under_Trueprop f = |
538 fun apply_under_Trueprop f = |
543 HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop |
539 HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop |
544 |
540 |
545 fun gen_frees_tac ctxt = |
541 fun gen_frees_tac ctxt = |
546 SUBGOAL (fn (concl, i) => |
542 SUBGOAL (fn (concl, i) => |
547 let |
543 let |
548 val thy = ProofContext.theory_of ctxt |
544 val thy = ProofContext.theory_of ctxt |
549 val vrs = Term.add_frees concl [] |
545 val vrs = Term.add_frees concl [] |
550 val cvrs = map (cterm_of thy o Free) vrs |
546 val cvrs = map (cterm_of thy o Free) vrs |
551 val concl' = apply_under_Trueprop (all_list vrs) concl |
547 val concl' = apply_under_Trueprop (all_list vrs) concl |
552 val goal = Logic.mk_implies (concl', concl) |
548 val goal = Logic.mk_implies (concl', concl) |
553 val rule = Goal.prove ctxt [] [] goal |
549 val rule = Goal.prove ctxt [] [] goal |
554 (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
550 (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) |
555 in |
551 in |
556 rtac rule i |
552 rtac rule i |
557 end) |
553 end) |
558 |
554 |
559 |
555 |
560 (** The General Shape of the Lifting Procedure **) |
556 (** The General Shape of the Lifting Procedure **) |
561 |
557 |
562 |
558 |
568 - 1st prem is the regularization step |
564 - 1st prem is the regularization step |
569 - 2nd prem is the rep/abs injection step |
565 - 2nd prem is the rep/abs injection step |
570 - 3rd prem is the cleaning part |
566 - 3rd prem is the cleaning part |
571 |
567 |
572 the Quot_True premise in 2nd records the lifted theorem *) |
568 the Quot_True premise in 2nd records the lifted theorem *) |
573 val lifting_procedure_thm = |
569 val lifting_procedure_thm = |
574 @{lemma "[|A; |
570 @{lemma "[|A; |
575 A --> B; |
571 A --> B; |
576 Quot_True D ==> B = C; |
572 Quot_True D ==> B = C; |
577 C = D|] ==> D" |
573 C = D|] ==> D" |
578 by (simp add: Quot_True_def)} |
574 by (simp add: Quot_True_def)} |
579 |
575 |
580 fun lift_match_error ctxt str rtrm qtrm = |
576 fun lift_match_error ctxt str rtrm qtrm = |
581 let |
577 let |
582 val rtrm_str = Syntax.string_of_term ctxt rtrm |
578 val rtrm_str = Syntax.string_of_term ctxt rtrm |