author Christian Urban Sun, 22 Aug 2010 12:58:03 +0800 changeset 38625 b97bd93fb9e2 parent 38624 9bb0016f7e60 child 38626 0170e0dc5f96
allow for pre-simplification of lifted theorems
```--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Aug 22 10:45:53 2010 +0800
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Aug 22 12:58:03 2010 +0800
@@ -18,7 +18,7 @@
val lift_procedure_tac: Proof.context -> thm -> int -> tactic
val lift_tac: Proof.context -> thm list -> int -> tactic

-  val lifted: Proof.context -> typ list -> thm -> thm
+  val lifted: Proof.context -> typ list -> thm list -> thm -> thm
val lifted_attrib: attribute
end;

@@ -647,7 +647,7 @@
end

-(** lifting as tactic **)
+(** lifting as a tactic **)

(* the tactic leaves three subgoals to be proved *)
fun lift_procedure_tac ctxt rthm =
@@ -661,39 +661,47 @@
(rtac rule THEN' rtac rthm') i
end)

+
+fun lift_single_tac ctxt rthm =
+  lift_procedure_tac ctxt rthm
+  THEN' RANGE
+    [ regularize_tac ctxt,
+      all_injection_tac ctxt,
+      clean_tac ctxt ]
+
fun lift_tac ctxt rthms =
+  Goal.conjunction_tac
+  THEN' RANGE (map (lift_single_tac ctxt) rthms)
+
+
+(* automated lifting with pre-simplification of the theorems;
+   for internal usage *)
+fun lifted ctxt qtys simps rthm =
let
-  fun mk_tac rthm =
-    lift_procedure_tac ctxt rthm
-    THEN' RANGE
-      [ regularize_tac ctxt,
-        all_injection_tac ctxt,
-        clean_tac ctxt ]
+  (* When the theorem is atomized, eta redexes are contracted,
+     so we do it both in the original theorem *)
+  val rthm' =
+    rthm
+    |> asm_full_simplify (HOL_basic_ss addsimps simps)
+    |> Drule.eta_contraction_rule
+  val ((_, [rthm'']), ctxt') = Variable.import false [rthm'] ctxt
+  val goal = derive_qtrm ctxt qtys (prop_of rthm'')
in
-  Goal.conjunction_tac THEN' RANGE (map mk_tac rthms)
+  Goal.prove ctxt' [] [] goal
+    (K ((asm_full_simp_tac (HOL_basic_ss addsimps simps)
+         THEN' lift_single_tac ctxt' rthm') 1))
+  |> singleton (ProofContext.export ctxt' ctxt)
end

-(** lifting as an attribute **)
-
-fun lifted ctxt qtys thm =
-let
-  (* When the theorem is atomized, eta redexes are contracted,
-     so we do it both in the original theorem *)
-  val thm' = Drule.eta_contraction_rule thm
-  val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt
-  val goal = derive_qtrm ctxt qtys (prop_of thm'')
-in
-  Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
-  |> singleton (ProofContext.export ctxt' ctxt)
-end;
+(* lifting as an attribute *)

val lifted_attrib = Thm.rule_attribute (fn context =>
let
val ctxt = Context.proof_of context
val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
in
-    lifted ctxt qtys
+    lifted ctxt qtys []
end)

end; (* structure *)```