--- a/Nominal/FSet.thy Sun Jun 13 14:39:55 2010 +0200
+++ b/Nominal/FSet.thy Sun Jun 13 17:01:15 2010 +0200
@@ -1417,4 +1417,223 @@
no_notation
list_eq (infix "\<approx>" 50)
+ML {*
+open Quotient_Info;
+
+exception LIFT_MATCH of string
+
+
+
+(*** Aggregate Rep/Abs Function ***)
+
+
+(* The flag RepF is for types in negative position; AbsF is for types
+ in positive position. Because of this, function types need to be
+ treated specially, since there the polarity changes.
+*)
+
+datatype flag = AbsF | RepF
+
+fun negF AbsF = RepF
+ | negF RepF = AbsF
+
+fun is_identity (Const (@{const_name "id"}, _)) = true
+ | is_identity _ = false
+
+fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
+
+fun mk_fun_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_mapfun ctxt s =
+let
+ val thy = ProofContext.theory_of ctxt
+ val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
+ val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
+in
+ Const (mapfun, dummyT)
end
+
+(* makes a Free out of a TVar *)
+fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
+
+(* produces an aggregate map function for the
+ rty-part of a quotient definition; abstracts
+ over all variables listed in vs (these variables
+ correspond to the type variables in rty)
+
+ for example for: (?'a list * ?'b)
+ it produces: %a b. prod_map (map a) b
+*)
+fun mk_mapfun ctxt vs rty =
+let
+ val vs' = map (mk_Free) vs
+
+ fun mk_mapfun_aux rty =
+ case rty of
+ TVar _ => mk_Free rty
+ | Type (_, []) => mk_identity rty
+ | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
+ | _ => raise LIFT_MATCH "mk_mapfun (default)"
+in
+ fold_rev Term.lambda vs' (mk_mapfun_aux rty)
+end
+
+(* looks up the (varified) rty and qty for
+ a quotient definition
+*)
+fun get_rty_qty ctxt s =
+let
+ val thy = ProofContext.theory_of ctxt
+ val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
+ val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
+in
+ (#rtyp qdata, #qtyp qdata)
+end
+
+(* takes two type-environments and looks
+ up in both of them the variable v, which
+ must be listed in the environment
+*)
+fun double_lookup rtyenv qtyenv v =
+let
+ val v' = fst (dest_TVar v)
+in
+ (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
+end
+
+(* matches a type pattern with a type *)
+fun match ctxt err ty_pat ty =
+let
+ val thy = ProofContext.theory_of ctxt
+in
+ Sign.typ_match thy (ty_pat, ty) Vartab.empty
+ handle MATCH_TYPE => err ctxt ty_pat ty
+end
+
+(* produces the rep or abs constant for a qty *)
+fun absrep_const flag ctxt qty_str =
+let
+ val qty_name = Long_Name.base_name qty_str
+ val qualifier = Long_Name.qualifier qty_str
+in
+ case flag of
+ AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT)
+ | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT)
+end
+
+(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
+fun absrep_const_chk flag ctxt qty_str =
+ Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
+
+fun absrep_match_err ctxt ty_pat ty =
+let
+ val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
+ val ty_str = Syntax.string_of_typ ctxt ty
+in
+ raise LIFT_MATCH (space_implode " "
+ ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
+end
+
+
+(** generation of an aggregate absrep function **)
+
+(* - In case of equal types we just return the identity.
+
+ - In case of TFrees we also return the identity.
+
+ - In case of function types we recurse taking
+ the polarity change into account.
+
+ - If the type constructors are equal, we recurse for the
+ arguments and build the appropriate map function.
+
+ - If the type constructors are unequal, there must be an
+ instance of quotient types:
+
+ - we first look up the corresponding rty_pat and qty_pat
+ from the quotient definition; the arguments of qty_pat
+ must be some distinct TVars
+ - we then match the rty_pat with rty and qty_pat with qty;
+ if matching fails the types do not correspond -> error
+ - the matching produces two environments; we look up the
+ assignments for the qty_pat variables and recurse on the
+ assignments
+ - we prefix the aggregate map function for the rty_pat,
+ which is an abstraction over all type variables
+ - finally we compose the result with the appropriate
+ absrep function in case at least one argument produced
+ a non-identity function /
+ otherwise we just return the appropriate absrep
+ function
+
+ The composition is necessary for types like
+
+ ('a list) list / ('a foo) foo
+
+ The matching is necessary for types like
+
+ ('a * 'a) list / 'a bar
+
+ The test is necessary in order to eliminate superfluous
+ identity maps.
+*)
+
+fun absrep_fun flag ctxt (rty, qty) =
+ if rty = qty
+ then mk_identity rty
+ else
+ case (rty, qty) of
+ (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
+ let
+ val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
+ val arg2 = absrep_fun flag ctxt (ty2, ty2')
+ in
+ list_comb (get_mapfun ctxt "fun", [arg1, arg2])
+ end
+ | (Type (s, tys), Type (s', tys')) =>
+ if s = s'
+ then
+ let
+ val args = map (absrep_fun flag ctxt) (tys ~~ tys')
+ in
+ list_comb (get_mapfun ctxt s, args)
+ end
+ else
+ let
+ val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
+ val rtyenv = match ctxt absrep_match_err rty_pat rty
+ val qtyenv = match ctxt absrep_match_err qty_pat qty
+ val args_aux = map (double_lookup rtyenv qtyenv) vs
+ val args = map (absrep_fun flag ctxt) args_aux
+ val map_fun = mk_mapfun ctxt vs rty_pat
+ val result = list_comb (map_fun, args)
+ in
+ (*if forall is_identity args
+ then absrep_const flag ctxt s'
+ else*) mk_fun_compose flag (absrep_const flag ctxt s', result)
+ end
+ | (TFree x, TFree x') =>
+ if x = x'
+ then mk_identity rty
+ else raise (LIFT_MATCH "absrep_fun (frees)")
+ | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
+ | _ => raise (LIFT_MATCH "absrep_fun (default)")
+
+
+*}
+
+ML {*
+ absrep_fun AbsF @{context} (@{typ "('a list) list \<Rightarrow> 'a list"}, @{typ "('a fset) fset \<Rightarrow> 'a fset"})
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
+
+lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}"
+apply(auto simp add: mem_def)
+done
+
+
+end