# HG changeset patch # User Christian Urban # Date 1261512406 -3600 # Node ID b4ffb8826105819547f2d0af3c5a8d19c0fa6947 # Parent d6acae26d0270b0a5b0efb8d38e5a139168d8fcf moved get_fun into quotient_term; this simplifies the overall including structure of the package diff -r d6acae26d027 -r b4ffb8826105 Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Tue Dec 22 20:51:37 2009 +0100 +++ b/Quot/Examples/FSet.thy Tue Dec 22 21:06:46 2009 +0100 @@ -39,7 +39,7 @@ ML {* -open Quotient_Def; +open Quotient_Term; *} ML {* diff -r d6acae26d027 -r b4ffb8826105 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Tue Dec 22 20:51:37 2009 +0100 +++ b/Quot/QuotMain.thy Tue Dec 22 21:06:46 2009 +0100 @@ -110,6 +110,11 @@ id_o[THEN eq_reflection] o_id[THEN eq_reflection] + +(* The translation functions for the lifting process. *) +use "quotient_term.ML" + + (* Definition of the quotient types *) use "quotient_typ.ML" @@ -117,11 +122,6 @@ (* Definitions for quotient constants *) use "quotient_def.ML" - -(* The translation functions for the lifting process. *) -use "quotient_term.ML" - - (* Tactics for proving the lifted theorems *) lemma eq_imp_rel: diff -r d6acae26d027 -r b4ffb8826105 Quot/quotient_def.ML --- a/Quot/quotient_def.ML Tue Dec 22 20:51:37 2009 +0100 +++ b/Quot/quotient_def.ML Tue Dec 22 21:06:46 2009 +0100 @@ -1,9 +1,6 @@ signature QUOTIENT_DEF = -sig - datatype flag = absF | repF - val get_fun: flag -> Proof.context -> typ * typ -> term - +sig val quotient_def: mixfix -> Attrib.binding -> term -> term -> Proof.context -> (term * thm) * local_theory val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) -> @@ -14,7 +11,7 @@ struct open Quotient_Info; -open Quotient_Type; +open Quotient_Term; (* wrapper for define *) fun define name mx attr rhs lthy = @@ -25,72 +22,6 @@ ((rhs, thm), lthy') end -datatype flag = absF | repF - -fun negF absF = repF - | negF repF = absF - -fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) - -fun mk_compose flag (trm1, trm2) = - case flag of - absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 - | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 - -fun get_fun_aux lthy s fs = -let - val thy = ProofContext.theory_of lthy - val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) - val info = maps_lookup thy s handle NotFound => raise exc -in - list_comb (Const (#mapfun info, dummyT), fs) -end - -fun get_const flag lthy _ qty = -(* FIXME: check here that the type-constructors of _ and qty are related *) -let - val thy = ProofContext.theory_of lthy - val qty_name = Long_Name.base_name (fst (dest_Type qty)) -in - case flag of - absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) - | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) -end - - -(* calculates the aggregate abs and rep functions for a given type; - repF is for constants' arguments; absF is for constants; - function types need to be treated specially, since repF and absF - change *) - -fun get_fun flag lthy (rty, qty) = - if rty = qty then mk_identity qty else - case (rty, qty) of - (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => - let - val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') - val fs_ty2 = get_fun flag lthy (ty2, ty2') - in - get_fun_aux lthy "fun" [fs_ty1, fs_ty2] - end - | (Type (s, _), Type (s', [])) => - if s = s' - then mk_identity qty - else get_const flag lthy rty qty - | (Type (s, tys), Type (s', tys')) => - let - val args = map (get_fun flag lthy) (tys ~~ tys') - in - if s = s' - then get_fun_aux lthy s args - else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args) - end - | (TFree x, TFree x') => - if x = x' - then mk_identity qty - else raise (LIFT_MATCH "get_fun (frees)") - | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") - | _ => raise (LIFT_MATCH "get_fun (default)") (* interface and syntax setup *) diff -r d6acae26d027 -r b4ffb8826105 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Tue Dec 22 20:51:37 2009 +0100 +++ b/Quot/quotient_tacs.ML Tue Dec 22 21:06:46 2009 +0100 @@ -12,7 +12,6 @@ struct open Quotient_Info; -open Quotient_Type; open Quotient_Term; diff -r d6acae26d027 -r b4ffb8826105 Quot/quotient_term.ML --- a/Quot/quotient_term.ML Tue Dec 22 20:51:37 2009 +0100 +++ b/Quot/quotient_term.ML Tue Dec 22 21:06:46 2009 +0100 @@ -1,15 +1,87 @@ signature QUOTIENT_TERM = sig - val regularize_trm: Proof.context -> term -> term -> term - val inj_repabs_trm: Proof.context -> (term * term) -> term + exception LIFT_MATCH of string + + datatype flag = absF | repF + val get_fun: flag -> Proof.context -> typ * typ -> term + + val regularize_trm: Proof.context -> term -> term -> term + val inj_repabs_trm: Proof.context -> (term * term) -> term end; structure Quotient_Term: QUOTIENT_TERM = struct open Quotient_Info; -open Quotient_Type; -open Quotient_Def; + +exception LIFT_MATCH of string + +(* Calculates the aggregate abs and rep functions for a given type; *) +(* repF is for constants' arguments; absF is for constants; *) +(* function types need to be treated specially, since repF and absF *) +(* change *) + +datatype flag = absF | repF + +fun negF absF = repF + | negF repF = absF + +fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) + +fun mk_compose flag (trm1, trm2) = + case flag of + absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 + | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 + +fun get_fun_aux lthy s fs = +let + val thy = ProofContext.theory_of lthy + val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."]) + val info = maps_lookup thy s handle NotFound => raise exc +in + list_comb (Const (#mapfun info, dummyT), fs) +end + +fun get_const flag lthy _ qty = +(* FIXME: check here that the type-constructors of _ and qty are related *) +let + val thy = ProofContext.theory_of lthy + val qty_name = Long_Name.base_name (fst (dest_Type qty)) +in + case flag of + absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT) + | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT) +end + +fun get_fun flag lthy (rty, qty) = + if rty = qty then mk_identity qty else + case (rty, qty) of + (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => + let + val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1') + val fs_ty2 = get_fun flag lthy (ty2, ty2') + in + get_fun_aux lthy "fun" [fs_ty1, fs_ty2] + end + | (Type (s, _), Type (s', [])) => + if s = s' + then mk_identity qty + else get_const flag lthy rty qty + | (Type (s, tys), Type (s', tys')) => + let + val args = map (get_fun flag lthy) (tys ~~ tys') + in + if s = s' + then get_fun_aux lthy s args + else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args) + end + | (TFree x, TFree x') => + if x = x' + then mk_identity qty + else raise (LIFT_MATCH "get_fun (frees)") + | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)") + | _ => raise (LIFT_MATCH "get_fun (default)") + (* Regularizing an rtrm means: @@ -218,8 +290,7 @@ *) fun mk_repabs lthy (T, T') trm = - Quotient_Def.get_fun repF lthy (T, T') - $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) + get_fun repF lthy (T, T') $ (get_fun absF lthy (T, T') $ trm) (* bound variables need to be treated properly, *)