# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282998280 -28800
# Node ID 053c69cb4a0e1406b1fcbe763dc85534f9c09792
# Parent  1920158cfa17a84bffc6c4a7d789ecc755aee97e
quotient package: lemmas to be lifted and descended can be pre-simplified

diff -r 1920158cfa17 -r 053c69cb4a0e src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Sat Aug 28 11:42:33 2010 +0200
+++ b/src/HOL/Quotient.thy	Sat Aug 28 20:24:40 2010 +0800
@@ -773,20 +773,20 @@
 
 method_setup lifting =
   {* Attrib.thms >> (fn thms => fn ctxt => 
-       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
+       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
   {* lifts theorems to quotient types *}
 
 method_setup lifting_setup =
   {* Attrib.thm >> (fn thm => fn ctxt => 
-       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt thm))) *}
+       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
   {* sets up the three goals for the quotient lifting procedure *}
 
 method_setup descending =
-  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt))) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
   {* decends theorems to the raw level *}
 
 method_setup descending_setup =
-  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt))) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
   {* sets up the three goals for the decending theorems *}
 
 method_setup regularize =
diff -r 1920158cfa17 -r 053c69cb4a0e src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 28 11:42:33 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 28 20:24:40 2010 +0800
@@ -12,11 +12,11 @@
   val all_injection_tac: Proof.context -> int -> tactic
   val clean_tac: Proof.context -> int -> tactic
   
-  val descend_procedure_tac: Proof.context -> int -> tactic
-  val descend_tac: Proof.context -> int -> tactic
+  val descend_procedure_tac: Proof.context -> thm list -> int -> tactic
+  val descend_tac: Proof.context -> thm list -> int -> tactic
  
-  val lift_procedure_tac: Proof.context -> thm -> int -> tactic
-  val lift_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
 
   val lifted: Proof.context -> typ list -> thm list -> thm -> thm
   val lifted_attrib: attribute
@@ -606,9 +606,9 @@
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
   val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
-    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
+    handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
   val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
-    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
+    handle LIFT_MATCH msg => lift_match_error ctxt msg rtrm qtrm
 in
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),
@@ -620,8 +620,12 @@
 
 (** descending as tactic **)
 
-fun descend_procedure_tac ctxt =
-  Object_Logic.full_atomize_tac
+fun descend_procedure_tac ctxt simps =
+let
+  val ss = (mk_minimal_ss ctxt) addsimps simps
+in
+  full_simp_tac ss
+  THEN' Object_Logic.full_atomize_tac
   THEN' gen_frees_tac ctxt
   THEN' SUBGOAL (fn (goal, i) =>
         let
@@ -631,11 +635,12 @@
         in
           rtac rule i
         end)
+end
 
-fun descend_tac ctxt =
+fun descend_tac ctxt simps =
 let
   val mk_tac_raw =
-    descend_procedure_tac ctxt
+    descend_procedure_tac ctxt simps
     THEN' RANGE
       [Object_Logic.rulify_tac THEN' (K all_tac),
        regularize_tac ctxt,
@@ -650,15 +655,20 @@
 
 
 (* the tactic leaves three subgoals to be proved *)
-fun lift_procedure_tac ctxt rthm =
-  Object_Logic.full_atomize_tac
+fun lift_procedure_tac ctxt simps rthm =
+let
+  val ss = (mk_minimal_ss ctxt) addsimps simps
+in
+  full_simp_tac ss
+  THEN' Object_Logic.full_atomize_tac
   THEN' gen_frees_tac ctxt
   THEN' SUBGOAL (fn (goal, i) =>
     let
       (* full_atomize_tac contracts eta redexes,
          so we do it also in the original theorem *)
       val rthm' = 
-        rthm |> Drule.eta_contraction_rule 
+        rthm |> full_simplify ss
+             |> Drule.eta_contraction_rule 
              |> Thm.forall_intr_frees
              |> atomize_thm 
 
@@ -666,32 +676,29 @@
     in
       (rtac rule THEN' rtac rthm') i
     end)
-
+end
 
-fun lift_single_tac ctxt rthm = 
-  lift_procedure_tac ctxt rthm
+fun lift_single_tac ctxt simps rthm = 
+  lift_procedure_tac ctxt simps rthm
   THEN' RANGE
     [ regularize_tac ctxt,
       all_injection_tac ctxt,
       clean_tac ctxt ]
 
-fun lift_tac ctxt rthms =
+fun lift_tac ctxt simps rthms =
   Goal.conjunction_tac 
-  THEN' RANGE (map (lift_single_tac ctxt) rthms)
+  THEN' RANGE (map (lift_single_tac ctxt simps) rthms)
 
 
 (* automated lifting with pre-simplification of the theorems;
    for internal usage *)
 fun lifted ctxt qtys simps rthm =
 let
-  val ss = (mk_minimal_ss ctxt) addsimps simps
-  val rthm' = asm_full_simplify ss rthm
-
-  val ((_, [rthm'']), ctxt') = Variable.import true [rthm'] ctxt
-  val goal = derive_qtrm ctxt' qtys (prop_of rthm'')
+  val ((_, [rthm']), ctxt') = Variable.import true [rthm] ctxt
+  val goal = derive_qtrm ctxt' qtys (prop_of rthm')
 in
   Goal.prove ctxt' [] [] goal 
-    (K (EVERY1 [asm_full_simp_tac ss, lift_single_tac ctxt' rthm'']))
+    (K (HEADGOAL (lift_single_tac ctxt' simps rthm')))
   |> singleton (ProofContext.export ctxt' ctxt)
 end