# HG changeset patch # User Christian Urban # Date 1323266402 0 # Node ID f82020ca32482c3be10d5f17dda2b31ac15e42cb # Parent 714100f5fda4949be68dcd0411771977cfae4bcc added a specific tactic and method that deal with partial equivalence relations diff -r 714100f5fda4 -r f82020ca3248 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Quotient.thy Wed Dec 07 14:00:02 2011 +0000 @@ -747,6 +747,15 @@ {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *} {* set up the three goals for the decending theorems *} +method_setup partiality_descending = + {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_tac ctxt []))) *} + {* decend theorems to the raw level *} + +method_setup partiality_descending_setup = + {* Scan.succeed (fn ctxt => + SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))) *} + {* set up the three goals for the decending theorems *} + method_setup regularize = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *} {* prove the regularization goals from the quotient lifting procedure *} diff -r 714100f5fda4 -r f82020ca3248 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Dec 05 15:10:15 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Dec 07 14:00:02 2011 +0000 @@ -14,6 +14,9 @@ val descend_procedure_tac: Proof.context -> thm list -> int -> tactic val descend_tac: Proof.context -> thm list -> int -> tactic + val partiality_descend_procedure_tac: Proof.context -> thm list -> int -> tactic + val partiality_descend_tac: Proof.context -> thm list -> int -> tactic + val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic @@ -580,13 +583,22 @@ the Quot_True premise in 2nd records the lifted theorem *) -val lifting_procedure_thm = +val procedure_thm = @{lemma "[|A; A --> B; Quot_True D ==> B = C; C = D|] ==> D" by (simp add: Quot_True_def)} +(* in case of partial equivalence relations, this form of the + procedure theorem results in solvable proof obligations +*) +val partiality_procedure_thm = + @{lemma "[|B; + Quot_True D ==> B = C; + C = D|] ==> D" + by (simp add: Quot_True_def)} + fun lift_match_error ctxt msg rtrm qtrm = let val rtrm_str = Syntax.string_of_term ctxt rtrm @@ -611,7 +623,7 @@ [SOME (cterm_of thy rtrm'), SOME (cterm_of thy reg_goal), NONE, - SOME (cterm_of thy inj_goal)] lifting_procedure_thm + SOME (cterm_of thy inj_goal)] procedure_thm end @@ -655,6 +667,56 @@ end +(** descending for partial equivalence relations **) + +fun partiality_procedure_inst ctxt rtrm qtrm = + let + val thy = Proof_Context.theory_of ctxt + val rtrm' = HOLogic.dest_Trueprop rtrm + val qtrm' = HOLogic.dest_Trueprop qtrm + val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm') + handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm + val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm') + handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm + in + Drule.instantiate' [] + [SOME (cterm_of thy reg_goal), + NONE, + SOME (cterm_of thy inj_goal)] partiality_procedure_thm + end + + +fun partiality_descend_procedure_tac ctxt simps = + let + val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds) + in + full_simp_tac ss + THEN' Object_Logic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' SUBGOAL (fn (goal, i) => + let + val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt) + val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal + val rule = partiality_procedure_inst ctxt rtrm goal + in + rtac rule i + end) + end + +fun partiality_descend_tac ctxt simps = + let + val mk_tac_raw = + partiality_descend_procedure_tac ctxt simps + THEN' RANGE + [Object_Logic.rulify_tac THEN' (K all_tac), + all_injection_tac ctxt, + clean_tac ctxt] + in + Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw + end + + + (** lifting as a tactic **)