--- a/src/HOL/Quotient.thy Sat Jun 26 22:44:25 2010 +0200
+++ b/src/HOL/Quotient.thy Mon Jun 28 10:39:39 2010 +0200
@@ -768,7 +768,7 @@
{* lifts theorems to quotient types *}
method_setup lifting_setup =
- {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
+ {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
{* sets up the three goals for the quotient lifting procedure *}
method_setup regularize =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Jun 26 22:44:25 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Jun 28 10:39:39 2010 +0200
@@ -2535,8 +2535,8 @@
THEN (rtac pred_intro_rule
(* How to handle equality correctly? *)
THEN_ALL_NEW (K (print_tac options "state before assumption matching")
- THEN' (fn i => REPEAT (atac i ORELSE (CHANGED (asm_full_simp_tac split_ss i)
- THEN print_tac options "state after pre-simplification:")))
+ THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_ss) THEN' (TRY o atac)))
+ THEN' (K (print_tac options "state after pre-simplification:"))
THEN' (K (print_tac options "state after assumption matching:")))) 1)
| prove_prems2 out_ts ((p, deriv) :: ps) =
let
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sat Jun 26 22:44:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Mon Jun 28 10:39:39 2010 +0200
@@ -12,7 +12,7 @@
val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
local_theory -> Quotient_Info.qconsts_info * local_theory
- val lift_raw_const: typ list -> string * term -> local_theory ->
+ val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
Quotient_Info.qconsts_info * local_theory
end;
@@ -50,6 +50,7 @@
let
val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
+ val _ = if is_Const rhs then () else warning "The definiens is not a constant"
fun sanity_test NONE _ = true
| sanity_test (SOME bind) str =
@@ -88,13 +89,13 @@
end
(* a wrapper for automatically lifting a raw constant *)
-fun lift_raw_const qtys (qconst_name, rconst) ctxt =
+fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
let
val rty = fastype_of rconst
- val qty = derive_qtyp qtys rty ctxt
+ val qty = derive_qtyp qtys rty false ctxt
+ val lhs = Free (qconst_name, qty)
in
- quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
- (Free (qconst_name, qty), rconst))) ctxt
+ quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
end
(* parser and command *)
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Jun 26 22:44:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Jun 28 10:39:39 2010 +0200
@@ -11,7 +11,7 @@
val injection_tac: Proof.context -> int -> tactic
val all_injection_tac: Proof.context -> int -> tactic
val clean_tac: Proof.context -> int -> tactic
- val procedure_tac: Proof.context -> thm -> int -> tactic
+ val procedure_tac: Proof.context -> thm list -> int -> tactic
val lift_tac: Proof.context -> thm list -> int -> tactic
val quotient_tac: Proof.context -> int -> tactic
val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
@@ -620,12 +620,23 @@
Object_Logic.full_atomize_tac
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
- let
- val rthm' = atomize_thm rthm
- val rule = procedure_inst ctxt (prop_of rthm') goal
- in
- (rtac rule THEN' rtac rthm') i
- end)
+ case rthm of
+ [] =>
+ let
+ val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
+ val rtrm = derive_qtrm qtys goal true ctxt
+ val rule = procedure_inst ctxt rtrm goal
+ in
+ rtac rule i
+ end
+ | [rthm'] =>
+ let
+ val rthm'' = atomize_thm rthm'
+ val rule = procedure_inst ctxt (prop_of rthm'') goal
+ in
+ (rtac rule THEN' rtac rthm'') i
+ end
+ | _ => error "more than one raw theorem given")
(* Automatic Proofs *)
@@ -633,14 +644,24 @@
fun lift_tac ctxt rthms =
let
fun mk_tac rthm =
- procedure_tac ctxt rthm
+ procedure_tac ctxt [rthm]
THEN' RANGE
[regularize_tac ctxt,
all_injection_tac ctxt,
+ clean_tac ctxt];
+ val mk_tac_raw =
+ procedure_tac ctxt []
+ THEN' RANGE
+ [fn _ => all_tac,
+ regularize_tac ctxt,
+ all_injection_tac ctxt,
clean_tac ctxt]
in
simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
- THEN' RANGE (map mk_tac rthms)
+ THEN'
+ (case rthms of
+ [] => mk_tac_raw
+ | _ => RANGE (map mk_tac rthms))
end
fun lifted qtys ctxt thm =
@@ -649,13 +670,21 @@
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 = (quotient_lift_all qtys ctxt' o prop_of) thm''
+ val goal = derive_qtrm qtys (prop_of thm'') false ctxt'
in
Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
|> singleton (ProofContext.export ctxt' ctxt)
end;
-(* An Attribute which automatically constructs the qthm *)
-val lifted_attrib = Thm.rule_attribute (fn ctxt => lifted [] (Context.proof_of ctxt))
+(* An attribute which automatically constructs the qthm
+ using all quotients defined so far.
+*)
+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 qtys ctxt
+ end)
end; (* structure *)
--- a/src/HOL/Tools/Quotient/quotient_term.ML Sat Jun 26 22:44:25 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Mon Jun 28 10:39:39 2010 +0200
@@ -26,8 +26,8 @@
val inj_repabs_trm: Proof.context -> term * term -> term
val inj_repabs_trm_chk: Proof.context -> term * term -> term
- val derive_qtyp: typ list -> typ -> Proof.context -> typ
- val quotient_lift_all: typ list -> Proof.context -> term -> term
+ val derive_qtyp: typ list -> typ -> bool -> Proof.context -> typ
+ val derive_qtrm: typ list -> term -> bool -> Proof.context -> term
end;
structure Quotient_Term: QUOTIENT_TERM =
@@ -690,96 +690,90 @@
(*** Wrapper for automatically transforming an rthm into a qthm ***)
-(* subst_tys takes a list of (rty, qty) substitution pairs
+(* subst_rty takes a list of (rty, qty) substitution pairs
and replaces all occurences of rty in the given type
- by appropriate qty, with substitution *)
-fun subst_ty thy ty (rty, qty) r =
- if r <> NONE then r else
- case try (Sign.typ_match thy (rty, ty)) Vartab.empty of
- SOME inst => SOME (Envir.subst_type inst qty)
- | NONE => NONE
-fun subst_tys thy substs ty =
- case fold (subst_ty thy ty) substs NONE of
- SOME ty => ty
- | NONE =>
- (case ty of
- Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
- | x => x)
+ by an appropriate qty
+*)
+fun subst_rtyp ctxt ty_subst rty =
+ case rty of
+ Type (s, rtys) =>
+ let
+ val thy = ProofContext.theory_of ctxt
+ val rty' = Type (s, map (subst_rtyp ctxt ty_subst) rtys)
+
+ fun matches [] = rty'
+ | matches ((rty, qty)::tail) =
+ case try (Sign.typ_match thy (rty, rty')) Vartab.empty of
+ NONE => matches tail
+ | SOME inst => Envir.subst_type inst qty
+ in
+ matches ty_subst
+ end
+ | _ => rty
+
+(* subst_rtrm takes a list of (rconst, qconst) substitution pairs,
+ as well as (rty, qty) substitution pairs, and replaces all
+ occurences of rconst and rty by appropriate instances of
+ qconst and qty
+*)
+fun subst_rtrm ctxt ty_subst trm_subst rtrm =
+ case rtrm of
+ t1 $ t2 => (subst_rtrm ctxt ty_subst trm_subst t1) $ (subst_rtrm ctxt ty_subst trm_subst t2)
+ | Abs (x, ty, t) => Abs (x, subst_rtyp ctxt ty_subst ty, subst_rtrm ctxt ty_subst trm_subst t)
+ | Free(n, ty) => Free(n, subst_rtyp ctxt ty_subst ty)
+ | Var(n, ty) => Var(n, subst_rtyp ctxt ty_subst ty)
+ | Bound i => Bound i
+ | Const (a, ty) =>
+ let
+ val thy = ProofContext.theory_of ctxt
-(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
- and if the given term matches any of the raw terms it
- returns the appropriate qtrm instantiated. If none of
- them matched it returns NONE. *)
-fun subst_trm thy t (rtrm, qtrm) s =
- if s <> NONE then s else
- case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of
- SOME inst => SOME (Envir.subst_term inst qtrm)
- | NONE => NONE;
-fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
+ fun matches [] = Const (a, subst_rtyp ctxt ty_subst ty)
+ | matches ((rconst, qconst)::tail) =
+ case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of
+ NONE => matches tail
+ | SOME inst => Envir.subst_term inst qconst
+ in
+ matches trm_subst
+ end
+
+(* generates type substitutions out of the
+ types involved in a quotient
+*)
+fun get_ty_subst qtys reverse ctxt =
+ Quotient_Info.quotdata_dest ctxt
+ |> map (fn x => (#rtyp x, #qtyp x))
+ |> filter (fn (_, qty) => member (op =) qtys qty)
+ |> map (fn (x, y) => if reverse then (y, x) else (x, y))
-(* prepares type and term substitution pairs to be used by above
- functions that let replace all raw constructs by appropriate
- lifted counterparts. *)
-fun get_ty_trm_substs qtys ctxt =
+(* generates term substitutions out of the qconst
+ definitions and relations in a quotient
+*)
+fun get_trm_subst qtys reverse ctxt =
let
- val thy = ProofContext.theory_of ctxt
- val quot_infos = Quotient_Info.quotdata_dest ctxt
- val const_infos = Quotient_Info.qconsts_dest ctxt
- val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
- val ty_substs =
- if qtys = [] then all_ty_substs else
- filter (fn (_, qty) => member (op =) qtys qty) all_ty_substs
- val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
- fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
- val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
- fun valid_trm_subst (rt, qt) = (subst_tys thy ty_substs (fastype_of rt) = fastype_of qt)
- val all_trm_substs = const_substs @ rel_substs
+ val subst_rtyp' = subst_rtyp ctxt (get_ty_subst qtys reverse ctxt)
+ fun proper (rt, qt) = (subst_rtyp' (fastype_of rt) = fastype_of qt)
+
+ val const_substs =
+ Quotient_Info.qconsts_dest ctxt
+ |> map (fn x => (#rconst x, #qconst x))
+ |> map (fn (x, y) => if reverse then (y, x) else (x, y))
+
+ val rel_substs =
+ Quotient_Info.quotdata_dest ctxt
+ |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
+ |> map (fn (x, y) => if reverse then (y, x) else (x, y))
in
- (ty_substs, filter valid_trm_subst all_trm_substs)
+ filter proper (const_substs @ rel_substs)
end
-fun derive_qtyp qtys rty ctxt =
-let
- val thy = ProofContext.theory_of ctxt
- val (ty_substs, _) = get_ty_trm_substs qtys ctxt
-in
- subst_tys thy ty_substs rty
-end
-
-(*
-Takes a term and
-
-* replaces raw constants by the quotient constants
-
-* replaces equivalence relations by equalities
-
-* replaces raw types by the quotient types
-
+(* derives a qtyp and qtrm out of a rtyp and rtrm,
+ respectively
*)
+fun derive_qtyp qtys rty unlift ctxt =
+ subst_rtyp ctxt (get_ty_subst qtys unlift ctxt) rty
-fun quotient_lift_all qtys ctxt t =
-let
- val thy = ProofContext.theory_of ctxt
- val (ty_substs, substs) = get_ty_trm_substs qtys ctxt
- fun lift_aux t =
- case subst_trms thy substs t of
- SOME x => x
- | NONE =>
- (case t of
- a $ b => lift_aux a $ lift_aux b
- | Abs(a, ty, s) =>
- let
- val (y, s') = Term.dest_abs (a, ty, s)
- val nty = subst_tys thy ty_substs ty
- in
- Abs(y, nty, abstract_over (Free (y, nty), lift_aux s'))
- end
- | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
- | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
- | Bound i => Bound i
- | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
-in
- lift_aux t
-end
+fun derive_qtrm qtys rtrm unlift ctxt =
+ subst_rtrm ctxt (get_ty_subst qtys unlift ctxt) (get_trm_subst qtys unlift ctxt) rtrm
+
end; (* structure *)