--- 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 *)