added a specific tactic and method that deal with partial equivalence relations
authorChristian Urban <urbanc@in.tum.de>
Wed Dec 07 14:00:02 2011 +0000 (2011-12-07)
changeset 45782f82020ca3248
parent 45776 714100f5fda4
child 45783 3e8a2464f607
added a specific tactic and method that deal with partial equivalence relations
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_tacs.ML
     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.23        by (simp add: Quot_True_def)}
    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