--- a/FSet.thy	Wed Nov 04 16:10:39 2009 +0100
+++ b/FSet.thy	Thu Nov 05 09:38:34 2009 +0100
@@ -317,9 +317,6 @@
 ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *}
 
 (* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *)
-
-
-
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
@@ -351,49 +348,59 @@
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *}
 
 
-ML {* val ind_r_a = atomize_thm @{thm map_append} *}
- prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
- ML_prf {*  fun tac ctxt =
-     (FIRST' [
+ML {* val t_a = atomize_thm @{thm map_append} *}
+(* prove {* build_regularize_goal t_a rty rel @{context}  *}
+ ML_prf {*  fun tac ctxt = FIRST' [
       rtac rel_refl,
       atac,
-      rtac @{thm get_rid},
-      rtac @{thm get_rid2},
-      (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
+      rtac @{thm universal_twice},
+      (rtac @{thm impI} THEN' atac),
+      rtac @{thm implication_twice},
+      (*rtac @{thm equality_twice},*)
+      EqSubst.eqsubst_tac ctxt [0]
         [(@{thm equiv_res_forall} OF [rel_eqv]),
-         (@{thm equiv_res_exists} OF [rel_eqv])]) i)),
+         (@{thm equiv_res_exists} OF [rel_eqv])],
       (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl),
       (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-    ]);
- *}
+     ]; *}
   apply (atomize(full))
-  apply (tactic {* tac @{context} 1 *}) *)
-ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv rel_refl @{context} *}
+  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 rt = build_repabs_term @{context} ind_r_r consts rty qty
-  val rg = Logic.mk_equals ((Thm.prop_of ind_r_r), rt);
+  val rt = build_repabs_term @{context} t_r consts rty qty
+  val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 *}
+
+ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a list \<Rightarrow> ?'a list"})) *}
+ML {* old_get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} @{typ "'a list \<Rightarrow> 'a list"} *}
+
 prove rg
 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 *})
 done
-ML {* val ind_r_t =
+ML {* val t_t =
   Toplevel.program (fn () =>
-  repabs @{context} ind_r_r consts rty qty quot rel_refl trans2 rsp_thms
+  repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms
   )
 *}
 
 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm list.induct})) *}
 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
-ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
-ML {* val ind_r_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) ind_r_t *}
-ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]]} *}
-ML {* val ind_r_a = simp_allex_prs quot [thm] ind_r_l *}
+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 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 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 defs_sym = add_lower_defs @{context} defs *}
-ML {* val ind_r_d = repeat_eqsubst_thm @{context} defs_sym ind_r_a *}
-ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
-ML {* ObjectLogic.rulify ind_r_s *}
+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 *}
+ML {* ObjectLogic.rulify t_s *}
 
 ML {*
   fun lift_thm_fset_note name thm lthy =

--- a/LamEx.thy	Wed Nov 04 16:10:39 2009 +0100
+++ b/LamEx.thy	Thu Nov 05 09:38:34 2009 +0100
@@ -165,6 +165,12 @@
 lemma rfv_rsp: "(alpha ===> op =) rfv rfv"
   sorry
 
+lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
+apply (auto)
+apply (erule alpha.cases)
+apply (simp_all add: rlam.inject alpha_refl)
+done
+
 ML {* val qty = @{typ "lam"} *}
 ML {* val defs = @{thms Var_def App_def Lam_def perm_lam_def fv_def} *}
 ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} @
@@ -187,6 +193,8 @@
 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
 ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *}
 
+ML {* val var_inject = lift_thm_lam @{context} @{thm rvar_inject} *}
+
 local_setup {*
   Quotient.note (@{binding "pi_var"}, pi_var) #> snd #>
   Quotient.note (@{binding "pi_app"}, pi_app) #> snd #>
@@ -195,7 +203,8 @@
   Quotient.note (@{binding "a2"}, a2) #> snd #>
   Quotient.note (@{binding "a3"}, a3) #> snd #>
   Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd #>
-  Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd
+  Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd #>
+  Quotient.note (@{binding "var_inject"}, var_inject) #> snd
 *}
 
 thm alpha.cases
@@ -203,18 +212,6 @@
 thm alpha.induct
 thm alpha_induct
 
-lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
-apply (auto)
-apply (erule alpha.cases)
-apply (simp_all add: rlam.inject alpha_refl)
-done
-
-ML {* val var_inject = Toplevel.program (fn () => lift_thm_lam @{context} @{thm rvar_inject}) *}
-
-local_setup {*
-  Quotient.note (@{binding "var_inject"}, var_inject) #> snd
-*}
-
 lemma var_supp:
   shows "supp (Var a) = ((supp a)::name set)"
   apply(simp add: supp_def)

--- 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;

--- a/QuotTest.thy	Wed Nov 04 16:10:39 2009 +0100
+++ b/QuotTest.thy	Thu Nov 05 09:38:34 2009 +0100
@@ -120,25 +120,18 @@
 
 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 = snd (dest_Free (term_of @{cpat "f :: ?'a list \<Rightarrow> ?'a list"})) *}
+ML {* val ttt = snd (dest_Free (term_of @{cpat "f :: ?'a ql \<Rightarrow> ?'a ql"})) *}
 
 ML {*
-  get_fun absF [(al, aq)] @{context} ttt
-  |> fst
-  |> Syntax.pretty_term @{context}
-  |> Pretty.string_of
-  |> writeln
+  fst (get_fun absF [(aq, al)] @{context} ttt)
+  |> cterm_of @{theory}
 *}
 
-
-ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat list \<Rightarrow> nat list"})) *}
+ML {* val ttt2 = snd (dest_Free (term_of @{cpat "f :: nat ql \<Rightarrow> bool ql \<Rightarrow> 'a ql"})) *}
 
 ML {*
-  get_fun absF [(al, aq)] @{context} ttt2
-  |> fst
-  |> Syntax.pretty_term @{context}
-  |> Pretty.string_of
-  |> writeln
+  fst (get_fun absF [(aq, al), (@{typ "nat ql"}, @{typ "nat list"}), (@{typ "bool ql"}, @{typ "bool list"})] @{context} ttt2)
+  |> cterm_of @{theory}
 *}
 
 quotient_def (for qt)