quotient package: lemmas to be lifted and descended can be pre-simplified
authorChristian Urban <urbanc@in.tum.de>
Sat Aug 28 20:24:40 2010 +0800 (2010-08-28)
changeset 38859053c69cb4a0e
parent 38858 1920158cfa17
child 38860 749d09f52fde
child 38864 4abe644fcea5
quotient package: lemmas to be lifted and descended can be pre-simplified
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_tacs.ML
     1.1 --- a/src/HOL/Quotient.thy	Sat Aug 28 11:42:33 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Sat Aug 28 20:24:40 2010 +0800
     1.3 @@ -773,20 +773,20 @@
     1.4  
     1.5  method_setup lifting =
     1.6    {* Attrib.thms >> (fn thms => fn ctxt => 
     1.7 -       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
     1.8 +       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
     1.9    {* lifts theorems to quotient types *}
    1.10  
    1.11  method_setup lifting_setup =
    1.12    {* Attrib.thm >> (fn thm => fn ctxt => 
    1.13 -       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt thm))) *}
    1.14 +       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
    1.15    {* sets up the three goals for the quotient lifting procedure *}
    1.16  
    1.17  method_setup descending =
    1.18 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt))) *}
    1.19 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
    1.20    {* decends theorems to the raw level *}
    1.21  
    1.22  method_setup descending_setup =
    1.23 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt))) *}
    1.24 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
    1.25    {* sets up the three goals for the decending theorems *}
    1.26  
    1.27  method_setup regularize =
     2.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 28 11:42:33 2010 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 28 20:24:40 2010 +0800
     2.3 @@ -12,11 +12,11 @@
     2.4    val all_injection_tac: Proof.context -> int -> tactic
     2.5    val clean_tac: Proof.context -> int -> tactic
     2.6    
     2.7 -  val descend_procedure_tac: Proof.context -> int -> tactic
     2.8 -  val descend_tac: Proof.context -> int -> tactic
     2.9 +  val descend_procedure_tac: Proof.context -> thm list -> int -> tactic
    2.10 +  val descend_tac: Proof.context -> thm list -> int -> tactic
    2.11   
    2.12 -  val lift_procedure_tac: Proof.context -> thm -> int -> tactic
    2.13 -  val lift_tac: Proof.context -> thm list -> int -> tactic
    2.14 +  val lift_procedure_tac: Proof.context -> thm list -> thm -> int -> tactic
    2.15 +  val lift_tac: Proof.context -> thm list -> thm list -> int -> tactic
    2.16  
    2.17    val lifted: Proof.context -> typ list -> thm list -> thm -> thm
    2.18    val lifted_attrib: attribute
    2.19 @@ -606,9 +606,9 @@
    2.20    val rtrm' = HOLogic.dest_Trueprop rtrm
    2.21    val qtrm' = HOLogic.dest_Trueprop qtrm
    2.22    val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
    2.23 -    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
    2.24 +    handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
    2.25    val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
    2.26 -    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
    2.27 +    handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
    2.28  in
    2.29    Drule.instantiate' []
    2.30      [SOME (cterm_of thy rtrm'),
    2.31 @@ -620,8 +620,12 @@
    2.32  
    2.33  (** descending as tactic **)
    2.34  
    2.35 -fun descend_procedure_tac ctxt =
    2.36 -  Object_Logic.full_atomize_tac
    2.37 +fun descend_procedure_tac ctxt simps =
    2.38 +let
    2.39 +  val ss = (mk_minimal_ss ctxt) addsimps simps
    2.40 +in
    2.41 +  full_simp_tac ss
    2.42 +  THEN' Object_Logic.full_atomize_tac
    2.43    THEN' gen_frees_tac ctxt
    2.44    THEN' SUBGOAL (fn (goal, i) =>
    2.45          let
    2.46 @@ -631,11 +635,12 @@
    2.47          in
    2.48            rtac rule i
    2.49          end)
    2.50 +end
    2.51  
    2.52 -fun descend_tac ctxt =
    2.53 +fun descend_tac ctxt simps =
    2.54  let
    2.55    val mk_tac_raw =
    2.56 -    descend_procedure_tac ctxt
    2.57 +    descend_procedure_tac ctxt simps
    2.58      THEN' RANGE
    2.59        [Object_Logic.rulify_tac THEN' (K all_tac),
    2.60         regularize_tac ctxt,
    2.61 @@ -650,15 +655,20 @@
    2.62  
    2.63  
    2.64  (* the tactic leaves three subgoals to be proved *)
    2.65 -fun lift_procedure_tac ctxt rthm =
    2.66 -  Object_Logic.full_atomize_tac
    2.67 +fun lift_procedure_tac ctxt simps rthm =
    2.68 +let
    2.69 +  val ss = (mk_minimal_ss ctxt) addsimps simps
    2.70 +in
    2.71 +  full_simp_tac ss
    2.72 +  THEN' Object_Logic.full_atomize_tac
    2.73    THEN' gen_frees_tac ctxt
    2.74    THEN' SUBGOAL (fn (goal, i) =>
    2.75      let
    2.76        (* full_atomize_tac contracts eta redexes,
    2.77           so we do it also in the original theorem *)
    2.78        val rthm' = 
    2.79 -        rthm |> Drule.eta_contraction_rule 
    2.80 +        rthm |> full_simplify ss
    2.81 +             |> Drule.eta_contraction_rule 
    2.82               |> Thm.forall_intr_frees
    2.83               |> atomize_thm 
    2.84  
    2.85 @@ -666,32 +676,29 @@
    2.86      in
    2.87        (rtac rule THEN' rtac rthm') i
    2.88      end)
    2.89 -
    2.90 +end
    2.91  
    2.92 -fun lift_single_tac ctxt rthm = 
    2.93 -  lift_procedure_tac ctxt rthm
    2.94 +fun lift_single_tac ctxt simps rthm = 
    2.95 +  lift_procedure_tac ctxt simps rthm
    2.96    THEN' RANGE
    2.97      [ regularize_tac ctxt,
    2.98        all_injection_tac ctxt,
    2.99        clean_tac ctxt ]
   2.100  
   2.101 -fun lift_tac ctxt rthms =
   2.102 +fun lift_tac ctxt simps rthms =
   2.103    Goal.conjunction_tac 
   2.104 -  THEN' RANGE (map (lift_single_tac ctxt) rthms)
   2.105 +  THEN' RANGE (map (lift_single_tac ctxt simps) rthms)
   2.106  
   2.107  
   2.108  (* automated lifting with pre-simplification of the theorems;
   2.109     for internal usage *)
   2.110  fun lifted ctxt qtys simps rthm =
   2.111  let
   2.112 -  val ss = (mk_minimal_ss ctxt) addsimps simps
   2.113 -  val rthm' = asm_full_simplify ss rthm
   2.114 -
   2.115 -  val ((_, [rthm'']), ctxt') = Variable.import true [rthm'] ctxt
   2.116 -  val goal = derive_qtrm ctxt' qtys (prop_of rthm'')
   2.117 +  val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
   2.118 +  val goal = derive_qtrm ctxt' qtys (prop_of rthm')
   2.119  in
   2.120    Goal.prove ctxt' [] [] goal 
   2.121 -    (K (EVERY1 [asm_full_simp_tac ss, lift_single_tac ctxt' rthm'']))
   2.122 +    (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
   2.123    |> singleton (ProofContext.export ctxt' ctxt)
   2.124  end
   2.125