Automated lifting can be restricted to specific quotient types
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Sat Mar 27 14:48:46 2010 +0100 (2010-03-27)
changeset 359905ceedb86aa9d
parent 35983 27e2fa7d4ce7
child 35991 6ba552658807
child 35992 78674c6018ca
Automated lifting can be restricted to specific quotient types
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_term.ML
     1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat Mar 27 02:10:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sat Mar 27 14:48:46 2010 +0100
     1.3 @@ -12,7 +12,8 @@
     1.4    val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
     1.5      local_theory -> (term * thm) * local_theory
     1.6  
     1.7 -  val quotient_lift_const: string * term -> local_theory -> (term * thm) * local_theory
     1.8 +  val quotient_lift_const: typ list -> string * term -> local_theory ->
     1.9 +    (term * thm) * local_theory
    1.10  end;
    1.11  
    1.12  structure Quotient_Def: QUOTIENT_DEF =
    1.13 @@ -86,9 +87,9 @@
    1.14    quotient_def (decl, (attr, (lhs, rhs))) lthy''
    1.15  end
    1.16  
    1.17 -fun quotient_lift_const (b, t) ctxt =
    1.18 +fun quotient_lift_const qtys (b, t) ctxt =
    1.19    quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
    1.20 -    (Quotient_Term.quotient_lift_const (b, t) ctxt, t))) ctxt
    1.21 +    (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt
    1.22  
    1.23  local
    1.24    structure P = OuterParse;
     2.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Mar 27 02:10:00 2010 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Mar 27 14:48:46 2010 +0100
     2.3 @@ -15,6 +15,7 @@
     2.4    val lift_tac: Proof.context -> thm list -> int -> tactic
     2.5    val quotient_tac: Proof.context -> int -> tactic
     2.6    val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
     2.7 +  val lifted: typ list -> Proof.context -> thm -> thm
     2.8    val lifted_attrib: attribute
     2.9  end;
    2.10  
    2.11 @@ -650,17 +651,16 @@
    2.12    THEN' RANGE (map mk_tac rthms)
    2.13  end
    2.14  
    2.15 -(* An Attribute which automatically constructs the qthm *)
    2.16 -fun lifted_attrib_aux context thm =
    2.17 +fun lifted qtys ctxt thm =
    2.18  let
    2.19 -  val ctxt = Context.proof_of context
    2.20    val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
    2.21 -  val goal = (quotient_lift_all ctxt' o prop_of) thm'
    2.22 +  val goal = (quotient_lift_all qtys ctxt' o prop_of) thm'
    2.23  in
    2.24    Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1))
    2.25    |> singleton (ProofContext.export ctxt' ctxt)
    2.26  end;
    2.27  
    2.28 -val lifted_attrib = Thm.rule_attribute lifted_attrib_aux
    2.29 +(* An Attribute which automatically constructs the qthm *)
    2.30 +val lifted_attrib = Thm.rule_attribute (fn ctxt => lifted [] (Context.proof_of ctxt))
    2.31  
    2.32  end; (* structure *)
     3.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Sat Mar 27 02:10:00 2010 +0100
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Sat Mar 27 14:48:46 2010 +0100
     3.3 @@ -26,8 +26,8 @@
     3.4    val inj_repabs_trm: Proof.context -> term * term -> term
     3.5    val inj_repabs_trm_chk: Proof.context -> term * term -> term
     3.6  
     3.7 -  val quotient_lift_const: string * term -> local_theory -> term
     3.8 -  val quotient_lift_all: Proof.context -> term -> term
     3.9 +  val quotient_lift_const: typ list -> string * term -> local_theory -> term
    3.10 +  val quotient_lift_all: typ list -> Proof.context -> term -> term
    3.11  end;
    3.12  
    3.13  structure Quotient_Term: QUOTIENT_TERM =
    3.14 @@ -720,23 +720,28 @@
    3.15  (* prepares type and term substitution pairs to be used by above
    3.16     functions that let replace all raw constructs by appropriate
    3.17     lifted counterparts. *)
    3.18 -fun get_ty_trm_substs ctxt =
    3.19 +fun get_ty_trm_substs qtys ctxt =
    3.20  let
    3.21    val thy = ProofContext.theory_of ctxt
    3.22    val quot_infos  = Quotient_Info.quotdata_dest ctxt
    3.23    val const_infos = Quotient_Info.qconsts_dest ctxt
    3.24 -  val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
    3.25 +  val all_ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
    3.26 +  val ty_substs =
    3.27 +    if qtys = [] then all_ty_substs else
    3.28 +    filter (fn (_, qty) => qty mem qtys) all_ty_substs
    3.29    val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
    3.30    fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
    3.31    val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
    3.32 +  fun valid_trm_subst (rt, qt) = (subst_tys thy ty_substs (fastype_of rt) = fastype_of qt)
    3.33 +  val all_trm_substs = const_substs @ rel_substs
    3.34  in
    3.35 -  (ty_substs, const_substs @ rel_substs)
    3.36 +  (ty_substs, filter valid_trm_subst all_trm_substs)
    3.37  end
    3.38  
    3.39 -fun quotient_lift_const (b, t) ctxt =
    3.40 +fun quotient_lift_const qtys (b, t) ctxt =
    3.41  let
    3.42    val thy = ProofContext.theory_of ctxt
    3.43 -  val (ty_substs, _) = get_ty_trm_substs ctxt;
    3.44 +  val (ty_substs, _) = get_ty_trm_substs qtys ctxt;
    3.45    val (_, ty) = dest_Const t;
    3.46    val nty = subst_tys thy ty_substs ty;
    3.47  in
    3.48 @@ -754,10 +759,10 @@
    3.49  
    3.50  *)
    3.51  
    3.52 -fun quotient_lift_all ctxt t =
    3.53 +fun quotient_lift_all qtys ctxt t =
    3.54  let
    3.55    val thy = ProofContext.theory_of ctxt
    3.56 -  val (ty_substs, substs) = get_ty_trm_substs ctxt
    3.57 +  val (ty_substs, substs) = get_ty_trm_substs qtys ctxt
    3.58    fun lift_aux t =
    3.59      case subst_trms thy substs t of
    3.60        SOME x => x