diff -r 78bc4d9d7975 -r 8ebdef196fd5 QuotMain.thy
--- a/QuotMain.thy Wed Nov 04 16:10:39 2009 +0100
+++ b/QuotMain.thy Thu Nov 05 09:38:34 2009 +0100
@@ -376,7 +376,7 @@
fun my_reg_inst lthy rel rty trm =
case rel of
Const (n, _) => Syntax.check_term lthy
- (my_reg lthy (Const (n, dummyT)) rty trm)
+ (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)
*}
(*ML {*
@@ -448,14 +448,127 @@
)
*}
+(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
+ML {* fun exchange_ty rty (qty as (Type (qtys, _))) ty =
+ let val (s, tys) = dest_Type ty in
+ if Type.raw_instance (Logic.varifyT ty, rty)
+ then Type (qtys, tys)
+ else Type (s, map (exchange_ty rty qty) tys)
+ end
+ handle _ => ty
+*}
+
+ML {*
+fun negF absF = repF
+ | negF repF = absF
+
+fun get_fun_noexchange flag (rty, qty) lthy ty =
+let
+ fun get_fun_aux s fs_tys =
+ let
+ val (fs, tys) = split_list fs_tys
+ val (otys, ntys) = split_list tys
+ val oty = Type (s, otys)
+ val nty = Type (s, ntys)
+ val ftys = map (op -->) tys
+ in
+ (case (maps_lookup (ProofContext.theory_of lthy) s) of
+ SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
+ | NONE => error ("no map association for type " ^ s))
+ end
+
+ fun get_fun_fun fs_tys =
+ let
+ val (fs, tys) = split_list fs_tys
+ val ([oty1, oty2], [nty1, nty2]) = split_list tys
+ val oty = nty1 --> oty2
+ val nty = oty1 --> nty2
+ val ftys = map (op -->) tys
+ in
+ (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
+ end
+
+ fun get_const flag (rty, qty) =
+ 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), rty --> qty), (rty, qty))
+ | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
+ end
+
+ fun mk_identity ty = Abs ("", ty, Bound 0)
+
+in
+ if (Type.raw_instance (Logic.varifyT ty, rty))
+ then (get_const flag (ty, (exchange_ty rty qty ty)))
+ else (case ty of
+ TFree _ => (mk_identity ty, (ty, ty))
+ | Type (_, []) => (mk_identity ty, (ty, ty))
+ | Type ("fun" , [ty1, ty2]) =>
+ get_fun_fun [get_fun_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2]
+ | Type (s, tys) => get_fun_aux s (map (get_fun_noexchange flag (rty, qty) lthy) tys)
+ | _ => raise ERROR ("no type variables"))
+end
+*}
ML {*
fun old_get_fun flag rty qty lthy ty =
- get_fun flag [(qty, rty)] lthy ty
+ get_fun_noexchange flag (rty, qty) lthy ty
+*}
+
+ML {*
+fun find_matching_types rty ty =
+ let val (s, tys) = dest_Type ty in
+ if Type.raw_instance (Logic.varifyT ty, rty)
+ then [ty]
+ else flat (map (find_matching_types rty) tys)
+ end
+*}
+
+ML {*
+fun get_fun_new flag rty qty lthy ty =
+ let
+ val tys = find_matching_types rty ty;
+ val qenv = map (fn t => (exchange_ty rty qty t, t)) tys;
+ val xchg_ty = exchange_ty rty qty ty
+ in
+ get_fun flag qenv lthy xchg_ty
+ end
+*}
+
+(*
+consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+axioms Rl_eq: "EQUIV Rl"
-fun old_make_const_def nconst_bname otrm mx rty qty lthy =
- make_def nconst_bname otrm qty mx Attrib.empty_binding [(qty, rty)] lthy
+quotient ql = "'a list" / "Rl"
+ by (rule Rl_eq)
+
+ML {* val al = snd (dest_Free (term_of @{cpat "f :: ?'a list"})) *}
+ML {* val aq = snd (dest_Free (term_of @{cpat "f :: ?'a ql"})) *}
+ML {* val ttt = term_of @{cterm "f :: bool list \<Rightarrow> nat list"} *}
+
+ML {*
+ fst (get_fun_noexchange absF (al, aq) @{context} (fastype_of ttt))
+*}
+ML {*
+ fst (get_fun_new absF al aq @{context} (fastype_of ttt))
*}
+ML {*
+ fun mk_abs tm =
+ let
+ val ty = fastype_of tm
+ in fst (get_fun_noexchange absF (al, aq) @{context} ty) $ tm end
+ fun mk_repabs tm =
+ let
+ val ty = fastype_of tm
+ in fst (get_fun_noexchange repF (al, aq) @{context} ty) $ (mk_abs tm) end
+*}
+ML {*
+ cterm_of @{theory} (mk_repabs ttt)
+*}
+*)
text {* Does the same as 'subst' in a given prop or theorem *}
ML {*
@@ -499,15 +612,17 @@
ML {*
fun build_repabs_term lthy thm constructors rty qty =
let
- fun mk_rep tm =
- let
- val ty = old_exchange_ty rty qty (fastype_of tm)
- in fst (old_get_fun repF rty qty lthy ty) $ tm end
+ val rty = Logic.varifyT rty;
+ val qty = Logic.varifyT qty;
- fun mk_abs tm =
- let
- val ty = old_exchange_ty rty qty (fastype_of tm) in
- fst (old_get_fun absF rty qty lthy ty) $ tm end
+ fun mk_abs tm =
+ let
+ val ty = fastype_of tm
+ in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end
+ fun mk_repabs tm =
+ let
+ val ty = fastype_of tm
+ in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ (mk_abs tm) end
fun is_constructor (Const (x, _)) = member (op =) constructors x
| is_constructor _ = false;
@@ -521,16 +636,16 @@
val t' = lambda v (build_aux lthy t)
in
if (not (needs_lift rty (fastype_of tm))) then t'
- else mk_rep (mk_abs (
+ else mk_repabs (
if not (needs_lift rty vty) then t'
else
let
- val v' = mk_rep (mk_abs v);
+ val v' = mk_repabs v;
val t1 = Envir.beta_norm (t' $ v')
in
lambda v t1
end
- ))
+ )
end
| x =>
let
@@ -541,9 +656,9 @@
if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
then (list_comb (opp, (hd tms0) :: (tl tms)))
else if (is_constructor opp andalso needs_lift rty ty) then
- mk_rep (mk_abs (list_comb (opp,tms)))
+ mk_repabs (list_comb (opp,tms))
else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
- mk_rep(mk_abs(list_comb(opp,tms)))
+ mk_repabs(list_comb(opp,tms))
else if tms = [] then opp
else list_comb(opp, tms)
end
@@ -824,16 +939,18 @@
ML {*
fun applic_prs lthy rty qty absrep ty =
let
+ val rty = Logic.varifyT rty;
+ val qty = Logic.varifyT qty;
fun absty ty =
- old_exchange_ty rty qty ty
+ exchange_ty rty qty ty
fun mk_rep tm =
let
- val ty = old_exchange_ty rty qty (fastype_of tm)
- in fst (old_get_fun repF rty qty lthy ty) $ tm end;
+ val ty = exchange_ty qty rty (fastype_of tm)
+ in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ tm end;
fun mk_abs tm =
- let
- val ty = old_exchange_ty rty qty (fastype_of tm) in
- fst (old_get_fun absF rty qty lthy ty) $ tm end;
+ let
+ val ty = fastype_of tm
+ in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end
val (l, ltl) = Term.strip_type ty;
val nl = map absty l;
val vs = map (fn _ => "x") l;