author Christian Urban Wed Dec 07 14:00:02 2011 +0000 (2011-12-07) changeset 45782 f82020ca3248 parent 45776 714100f5fda4 child 45783 3e8a2464f607
added a specific tactic and method that deal with partial equivalence relations
 src/HOL/Quotient.thy file | annotate | diff | revisions src/HOL/Tools/Quotient/quotient_tacs.ML file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Quotient.thy	Mon Dec 05 15:10:15 2011 +0100
1.2 +++ b/src/HOL/Quotient.thy	Wed Dec 07 14:00:02 2011 +0000
1.3 @@ -747,6 +747,15 @@
1.4    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
1.5    {* set up the three goals for the decending theorems *}
1.6
1.7 +method_setup partiality_descending =
1.8 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_tac ctxt []))) *}
1.9 +  {* decend theorems to the raw level *}
1.10 +
1.11 +method_setup partiality_descending_setup =
1.12 +  {* Scan.succeed (fn ctxt =>
1.13 +       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))) *}
1.14 +  {* set up the three goals for the decending theorems *}
1.15 +
1.16  method_setup regularize =
1.17    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
1.18    {* prove the regularization goals from the quotient lifting procedure *}
```
```     2.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Dec 05 15:10:15 2011 +0100
2.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Dec 07 14:00:02 2011 +0000
2.3 @@ -14,6 +14,9 @@
2.4
2.5    val descend_procedure_tac: Proof.context -> thm list -> int -> tactic
2.6    val descend_tac: Proof.context -> thm list -> int -> tactic
2.7 +  val partiality_descend_procedure_tac: Proof.context -> thm list -> int -> tactic
2.8 +  val partiality_descend_tac: Proof.context -> thm list -> int -> tactic
2.9 +
2.10
2.11    val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic
2.12    val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic
2.13 @@ -580,13 +583,22 @@
2.14
2.15     the Quot_True premise in 2nd records the lifted theorem
2.16  *)
2.17 -val lifting_procedure_thm =
2.18 +val procedure_thm =
2.19    @{lemma  "[|A;
2.20                A --> B;
2.21                Quot_True D ==> B = C;
2.22                C = D|] ==> D"
2.24
2.25 +(* in case of partial equivalence relations, this form of the
2.26 +   procedure theorem results in solvable proof obligations
2.27 +*)
2.28 +val partiality_procedure_thm =
2.29 +  @{lemma  "[|B;
2.30 +              Quot_True D ==> B = C;
2.31 +              C = D|] ==> D"
2.32 +      by (simp add: Quot_True_def)}
2.33 +
2.34  fun lift_match_error ctxt msg rtrm qtrm =
2.35    let
2.36      val rtrm_str = Syntax.string_of_term ctxt rtrm
2.37 @@ -611,7 +623,7 @@
2.38        [SOME (cterm_of thy rtrm'),
2.39         SOME (cterm_of thy reg_goal),
2.40         NONE,
2.41 -       SOME (cterm_of thy inj_goal)] lifting_procedure_thm
2.42 +       SOME (cterm_of thy inj_goal)] procedure_thm
2.43    end
2.44
2.45
2.46 @@ -655,6 +667,56 @@
2.47    end
2.48
2.49
2.50 +(** descending for partial equivalence relations **)
2.51 +
2.52 +fun partiality_procedure_inst ctxt rtrm qtrm =
2.53 +  let
2.54 +    val thy = Proof_Context.theory_of ctxt
2.55 +    val rtrm' = HOLogic.dest_Trueprop rtrm
2.56 +    val qtrm' = HOLogic.dest_Trueprop qtrm
2.57 +    val reg_goal = Quotient_Term.regularize_trm_chk ctxt (rtrm', qtrm')
2.58 +      handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
2.59 +    val inj_goal = Quotient_Term.inj_repabs_trm_chk ctxt (reg_goal, qtrm')
2.60 +      handle Quotient_Term.LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
2.61 +  in
2.62 +    Drule.instantiate' []
2.63 +      [SOME (cterm_of thy reg_goal),
2.64 +       NONE,
2.65 +       SOME (cterm_of thy inj_goal)] partiality_procedure_thm
2.66 +  end
2.67 +
2.68 +
2.69 +fun partiality_descend_procedure_tac ctxt simps =
2.70 +  let
2.71 +    val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
2.72 +  in
2.73 +    full_simp_tac ss
2.74 +    THEN' Object_Logic.full_atomize_tac
2.75 +    THEN' gen_frees_tac ctxt
2.76 +    THEN' SUBGOAL (fn (goal, i) =>
2.77 +      let
2.78 +        val qtys = map #qtyp (Quotient_Info.dest_quotients ctxt)
2.79 +        val rtrm = Quotient_Term.derive_rtrm ctxt qtys goal
2.80 +        val rule = partiality_procedure_inst ctxt rtrm  goal
2.81 +      in
2.82 +        rtac rule i
2.83 +      end)
2.84 +  end
2.85 +
2.86 +fun partiality_descend_tac ctxt simps =
2.87 +  let
2.88 +    val mk_tac_raw =
2.89 +      partiality_descend_procedure_tac ctxt simps
2.90 +      THEN' RANGE
2.91 +        [Object_Logic.rulify_tac THEN' (K all_tac),
2.92 +         all_injection_tac ctxt,
2.93 +         clean_tac ctxt]
2.94 +  in
2.95 +    Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
2.96 +  end
2.97 +
2.98 +
2.99 +
2.100  (** lifting as a tactic **)
2.101
2.102
```