--- a/FSet.thy	Thu Nov 05 13:47:04 2009 +0100
+++ b/FSet.thy	Thu Nov 05 13:47:41 2009 +0100
@@ -324,7 +324,7 @@
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
-(*ML {* lift_thm_fset @{context} @{thm map_append} *}*)
+ML {* lift_thm_fset @{context} @{thm map_append} *}
 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
 ML {* lift_thm_fset @{context} @{thm list.induct} *}
 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
@@ -336,6 +336,8 @@
 where
   "fset_rec \<equiv> list_rec"
 
+(* ML {* Toplevel.program (fn () => lift_thm_fset @{context} @{thm list.recs(2)}) *} *)
+
 thm list.recs(2)
 thm list.cases
 
@@ -350,7 +352,22 @@
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *}
 
 
-ML {* val t_a = atomize_thm @{thm map_append} *}
+ML {* val t_a = atomize_thm @{thm list.recs(2)} *}
+ML {* val p_a = cprop_of t_a *}
+ML {* val pp = (snd o Thm.dest_abs NONE o snd o Thm.dest_comb o snd o Thm.dest_comb) p_a *}
+ML {* needs_lift @{typ "'a list"} @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} *}
+ML {* cterm_of @{theory} (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) *}
+
+
+ML {* val tt = (my_reg @{context} (@{term list_eq}) ( @{typ "'a list"}) (term_of pp)) *}
+ML {* val (_, [R, _]) = strip_comb tt *}
+ML {* val (_, [R]) = strip_comb R *}
+ML {* val (f, [R1, R2]) = strip_comb R *}
+ML {* val (f, [R1, R2]) = strip_comb R2 *}
+ML {* val (f, [R1, R2]) = strip_comb R2 *}
+
+ML {* cterm_of @{theory} R2 *}
+
 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
  ML_prf {*  fun tac ctxt = FIRST' [
       rtac rel_refl,
@@ -369,7 +386,7 @@
   apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
   done*)
 
-ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
+ML {* val t_r = Toplevel.program (fn () => regularize t_a rty rel rel_eqv rel_refl @{context}) *}
 ML {*
   val rt = build_repabs_term @{context} t_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
@@ -382,6 +399,11 @@
 apply(atomize(full))
 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
+
+"(op = ===> (op = ===> op \<approx> ===> op = ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
+"QUOTIENT op = (id ---> id) (id ---> id)"
+"(op = ===> op \<approx> ===> op =) x y"
+
 done
 ML {* val t_t =
   Toplevel.program (fn () =>
@@ -393,12 +415,11 @@
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
 ML {* val lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
-ML {* val app_prs_thms = map Thm.freezeT app_prs_thms *}
+ML {* val lam_prs_thms = map Thm.varifyT lam_prs_thms *}
 ML {* val t_l = repeat_eqsubst_thm @{context} (app_prs_thms @ lam_prs_thms) t_t *}
-ML {* val (alls, exs) = findallex rty qty (prop_of t_a); *}
+ML {* val (alls, exs) = findallex @{context} rty qty (prop_of t_a); *}
 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *}
-ML {* val allthmsv = map Thm.varifyT allthms *}
-ML {* val t_a = MetaSimplifier.rewrite_rule (allthmsv) t_l *}
+ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_l *}
 ML {* val defs_sym = add_lower_defs @{context} defs *}
 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *}
 ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_d *}

--- a/QuotMain.thy	Thu Nov 05 13:47:04 2009 +0100
+++ b/QuotMain.thy	Thu Nov 05 13:47:41 2009 +0100
@@ -239,11 +239,8 @@
 text {* tyRel takes a type and builds a relation that a quantifier over this
   type needs to respect. *}
 ML {*
-fun matches (ty1, ty2) =
-  Type.raw_instance (ty1, Logic.varifyT ty2);
-
 fun tyRel ty rty rel lthy =
-  if matches (rty, ty)
+  if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty)
   then rel
   else (case ty of
           Type (s, tys) =>
@@ -260,6 +257,8 @@
         | _ => HOLogic.eq_const ty)
 *}
 
+(* ML {* cterm_of @{theory} (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) *} *)
+
 definition
   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
@@ -407,26 +406,39 @@
 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
 by (simp add: id_def)
 
+(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
 ML {*
-fun old_exchange_ty rty qty ty =
-  if ty = rty
-  then qty
-  else
-     (case ty of
-        Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys)
-      | _ => ty
-     )
+fun exchange_ty lthy rty qty ty =
+  let
+    val thy = ProofContext.theory_of lthy
+  in
+    if Sign.typ_instance thy (ty, rty) then
+      let
+        val inst = Sign.typ_match thy (rty, ty) Vartab.empty
+      in
+        Envir.subst_type inst qty
+      end
+    else
+      let
+        val (s, tys) = dest_Type ty
+      in
+        Type (s, map (exchange_ty lthy rty qty) tys)
+      end
+  end
+  handle _ => ty (* for dest_Type *)
 *}
 
-(* 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
+(*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+axioms Rl_eq: "EQUIV Rl"
+
+quotient ql = "'a list" / "Rl"
+  by (rule Rl_eq)
+ML {* 
+  ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});
+  ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})
 *}
+*)
+
 
 ML {*
 fun negF absF = repF
@@ -458,9 +470,10 @@
     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
   end
 
+  val thy = ProofContext.theory_of lthy
+
   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
@@ -471,8 +484,8 @@
   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)))
+  if (Sign.typ_instance thy (ty, rty))
+  then (get_const flag (ty, (exchange_ty lthy rty qty ty)))
   else (case ty of
           TFree _ => (mk_identity ty, (ty, ty))
         | Type (_, []) => (mk_identity ty, (ty, ty)) 
@@ -501,8 +514,8 @@
 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
+    val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
+    val xchg_ty = exchange_ty lthy rty qty ty
   in
     get_fun flag qenv lthy xchg_ty
   end
@@ -875,13 +888,14 @@
     | _ => ([], []);
 *}
 ML {*
-  fun findallex rty qty tm =
+  fun findallex lthy rty qty tm =
     let
       val (a, e) = findallex_all rty qty tm;
       val (ad, ed) = (map domain_type a, map domain_type e);
-      val (au, eu) = (distinct (op =) ad, distinct (op =) ed)
+      val (au, eu) = (distinct (op =) ad, distinct (op =) ed);
+      val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty)
     in
-      (map (old_exchange_ty rty qty) au, map (old_exchange_ty rty qty) eu)
+      (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu)
     end
 *}
 
@@ -912,10 +926,10 @@
     val rty = Logic.varifyT rty;
     val qty = Logic.varifyT qty;
   fun absty ty =
-    exchange_ty rty qty ty
+    exchange_ty lthy rty qty ty
   fun mk_rep tm =
     let
-      val ty = exchange_ty qty rty (fastype_of tm)
+      val ty = exchange_ty lthy qty rty (fastype_of tm)
     in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ tm end;
   fun mk_abs tm =
     let
@@ -941,6 +955,9 @@
 *}
 
 ML {*
+fun matches (ty1, ty2) =
+  Type.raw_instance (ty1, Logic.varifyT ty2);
+
 fun lookup_quot_data lthy qty =
   let
     val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
@@ -986,7 +1003,7 @@
   val t_a = atomize_thm t;
   val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
   val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
-  val (alls, exs) = findallex rty qty (prop_of t_a);
+  val (alls, exs) = findallex lthy rty qty (prop_of t_a);
   val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
   val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
   val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
@@ -1000,11 +1017,13 @@
   val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l;
   val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
   val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
+  val t_rv = ObjectLogic.rulify t_r
 in
-  ObjectLogic.rulify t_r
+  Thm.varifyT t_rv
 end
 *}
 
+
 ML {*
   fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
     let