# HG changeset patch # User wenzelm # Date 1277714379 -7200 # Node ID 8ac597d6f3716510dd937df72401a3c32e804665 # Parent a47bb386b2382fd4c9cf5a3106791b0e45be2e71# Parent 1ae272fd4082fe82eeb01fc3dac07caa01d3f24f merged diff -r 1ae272fd4082 -r 8ac597d6f371 src/HOL/Quotient.thy --- 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 = diff -r 1ae272fd4082 -r 8ac597d6f371 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 1ae272fd4082 -r 8ac597d6f371 src/HOL/Tools/Quotient/quotient_def.ML --- 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 *) diff -r 1ae272fd4082 -r 8ac597d6f371 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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 *) diff -r 1ae272fd4082 -r 8ac597d6f371 src/HOL/Tools/Quotient/quotient_term.ML --- 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 *)