--- a/FIXME-TODO	Sun Dec 20 00:53:35 2009 +0100
+++ b/FIXME-TODO	Mon Dec 21 22:36:31 2009 +0100
@@ -8,11 +8,9 @@
   finite sets (syntax should be \<lbrace> \<rbrace>,
   look at Set.thy how syntax is been introduced)
 
-- think about what happens if things go wrong (like
-  theorem cannot be lifted) / proper diagnostic 
-  messages for the user
-
-- Handle theorems that include Ball/Bex
+- Handle theorems that include Ball/Bex. Would it help 
+  if we introduced separate Bex and Ball constants for 
+  quotienting?
 
 - user should be able to give quotient_respects and 
   preserves theorems in a more natural form.
@@ -22,12 +20,15 @@
 Lower Priority
 ==============
 
+- Maybe a quotient_definition should already require
+  a proof of the respectfulness (in this way one
+  already excludes non-sensical definitions)
+
 - accept partial equvalence relations
 
-- what happens if the original theorem contains bounded
-  quantifiers? can such theorems be lifted? If not, would 
-  it help if we introduced separate Bex and Ball constants
-  for quotienting?
+- think about what happens if things go wrong (like
+  theorem cannot be lifted) / proper diagnostic 
+  messages for the user
 
 - inductions from the datatype package have a strange
   order of quantifiers in assumptions.
@@ -55,4 +56,18 @@
   [QuotList, QuotOption, QuotPair...] could be automatically
   proven?
 
-- Examples: Finite multiset.
\ No newline at end of file
+- Examples: Finite multiset.
+
+- The current syntax of the quotient_definition is
+
+      "qconst :: qty"
+      as "rconst"
+
+  Is it possible to have the more Isabelle-like
+  syntax
+   
+      qconst :: "qty"
+      as "rconst"
+
+  That means "qconst :: qty" is not read as a term, but
+  as two entities.
\ No newline at end of file

--- a/Quot/Examples/FSet.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/Examples/FSet.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -1,5 +1,5 @@
 theory FSet
-imports "../QuotMain" List
+imports "../QuotMain" "../QuotList" List
 begin
 
 inductive
@@ -26,6 +26,61 @@
   fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
+
+fun
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+  "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient_type int = "nat \<times> nat" / intrel
+  apply(unfold equivp_def)
+  apply(auto simp add: mem_def expand_fun_eq)
+  done
+
+
+ML {*
+open Quotient_Def;
+*}
+
+ML {*
+get_fun absF @{context} (@{typ "'a list"}, 
+                         @{typ "'a fset"})
+|> Syntax.check_term @{context}
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+term "map id"
+term "abs_fset o (map id)"
+
+ML {*
+get_fun absF @{context} (@{typ "(nat * nat) list"}, 
+                         @{typ "int fset"})
+|> Syntax.check_term @{context}
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+term "map abs_int"
+term "abs_fset o map abs_int"
+
+
+ML {*
+get_fun absF @{context} (@{typ "('a list) list"}, 
+                         @{typ "('a fset) fset"})
+|> Syntax.check_term @{context}
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
+ML {*
+get_fun absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, 
+                         @{typ "('a fset) fset \<Rightarrow> 'a"})
+|> Syntax.check_term @{context}
+|> Syntax.string_of_term @{context}
+|> writeln
+*}
+
 quotient_definition
    "EMPTY :: 'a fset"
 as
@@ -52,11 +107,19 @@
 as
   "card1"
 
-(* text {*
+quotient_definition
+  "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
+as
+  "concat"
+
+term concat
+term fconcat
+
+text {*
  Maybe make_const_def should require a theorem that says that the particular lifted function
  respects the relation. With it such a definition would be impossible:
- make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}*)
+ make_const_def CARD @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
+*}
 
 lemma card1_0:
   fixes a :: "'a list"
@@ -213,7 +276,8 @@
 done
 
 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)"
-by (lifting member.simps(2))
+apply (lifting member.simps(2))
+done
 
 lemma "INSERT a (INSERT a x) = INSERT a x"
 apply (lifting list_eq.intros(4))

--- a/Quot/Examples/FSet2.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/Examples/FSet2.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -1,5 +1,5 @@
 theory FSet2
-imports "../QuotMain" List
+imports "../QuotMain" "../QuotList" List
 begin
 
 inductive

--- a/Quot/Examples/FSet3.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -1,37 +1,342 @@
 theory FSet3
-imports "../QuotMain" List
+imports "../QuotMain" "../QuotList" List
 begin
 
 fun
   list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
 where
-  "list_eq xs ys = (\<forall>e. (e \<in> set xs) = (e \<in> set ys))"
+  "list_eq xs ys = (\<forall>x. x \<in> set xs \<longleftrightarrow> x \<in> set ys)"
 
 lemma list_eq_equivp:
   shows "equivp list_eq"
 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
 by auto
 
-quotient_type fset = "'a list" / "list_eq"
-  by (rule list_eq_equivp)
+quotient_type 
+  fset = "'a list" / "list_eq"
+by (rule list_eq_equivp)
+
+
+section {* empty fset, finsert and membership *} 
+
+quotient_definition
+  "fempty :: 'a fset" ("{||}")
+as "[]::'a list"
+
+quotient_definition
+  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
+as "op #"
+
+syntax
+  "@Finset"     :: "args => 'a fset"  ("{|(_)|}")
 
-lemma not_nil_equiv_cons: 
-  "\<not>[] \<approx> a # A" 
-by auto
+translations
+  "{|x, xs|}" == "CONST finsert x {|xs|}"
+  "{|x|}"     == "CONST finsert x {||}"
+
+definition 
+  memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+  "memb x xs \<equiv> x \<in> set xs"
+
+quotient_definition
+  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50)
+as "memb"
+
+abbreviation
+  fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<notin>| _" [50, 51] 50)
+where
+  "a |\<notin>| S \<equiv> \<not>(a |\<in>| S)"
+
+lemma memb_rsp[quot_respect]: 
+  shows "(op = ===> op \<approx> ===> op =) memb memb"
+by (auto simp add: memb_def)
 
 lemma nil_rsp[quot_respect]:
   shows "[] \<approx> []"
-  by simp
+by simp
 
 lemma cons_rsp[quot_respect]: 
   shows "(op = ===> op \<approx> ===> op \<approx>) op # op #"
-  by simp
+by simp
+
+
+section {* Augmenting a set -- @{const finsert} *}
+
+text {* raw section *}
+
+lemma nil_not_cons: 
+  shows "\<not>[] \<approx> x # xs" 
+by auto
+
+lemma memb_cons_iff:
+  shows "memb x (y # xs) = (x = y \<or> memb x xs)"
+by (induct xs) (auto simp add: memb_def)
+
+lemma memb_consI1:
+  shows "memb x (x # xs)"
+by (simp add: memb_def)
+
+lemma memb_consI2: 
+  shows "memb x xs \<Longrightarrow> memb x (y # xs)"
+  by (simp add: memb_def)
+
+lemma memb_absorb:
+  shows "memb x xs \<Longrightarrow> (x # xs) \<approx> xs"
+by (induct xs) (auto simp add: memb_def)
+
+text {* lifted section *}
+
+lemma fempty_not_finsert[simp]:
+  shows "{||} \<noteq> finsert x S"
+by (lifting nil_not_cons)
+
+lemma fin_finsert_iff[simp]:
+  "x |\<in>| finsert y S = (x = y \<or> x |\<in>| S)"
+by (lifting memb_cons_iff) 
+
+lemma
+  shows finsertI1: "x |\<in>| finsert x S"
+  and   finsertI2: "x |\<in>| S \<Longrightarrow> x |\<in>| finsert y S"
+  by (lifting memb_consI1, lifting memb_consI2)
+
+lemma finsert_absorb [simp]: 
+  shows "x |\<in>| S \<Longrightarrow> finsert x S = S"
+by (lifting memb_absorb)
+
+
+section {* Singletons *}
+
+text {* raw section *}
+
+lemma singleton_list_eq:
+  shows "[x] \<approx> [y] \<longleftrightarrow> x = y"
+by auto
+
+text {* lifted section *}
+
+lemma fsingleton_eq[simp]:
+  shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
+by (lifting singleton_list_eq)
+
+
+section {* Cardinality of finite sets *}
+
+fun
+  fcard_raw :: "'a list \<Rightarrow> nat"
+where
+  fcard_raw_nil:  "fcard_raw [] = 0"
+| fcard_raw_cons: "fcard_raw (x # xs) = (if memb x xs then fcard_raw xs else Suc (fcard_raw xs))"
+
+quotient_definition
+  "fcard :: 'a fset \<Rightarrow> nat" 
+as "fcard_raw"
+
+text {* raw section *}
+
+lemma fcard_raw_ge_0:
+  assumes a: "x \<in> set xs"
+  shows "0 < fcard_raw xs"
+using a
+by (induct xs) (auto simp add: memb_def)
+
+lemma fcard_raw_delete_one:
+  "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
+by (induct xs) (auto dest: fcard_raw_ge_0 simp add: memb_def)
+
+lemma fcard_raw_rsp_aux:
+  assumes a: "a \<approx> b"
+  shows "fcard_raw a = fcard_raw b"
+using a
+apply(induct a arbitrary: b)
+apply(auto simp add: memb_def)
+apply(metis)
+apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)
+apply(simp add: fcard_raw_delete_one)
+apply(metis Suc_pred' fcard_raw_ge_0 fcard_raw_delete_one memb_def)
+done
+
+lemma fcard_raw_rsp[quot_respect]:
+  "(op \<approx> ===> op =) fcard_raw fcard_raw"
+  by (simp add: fcard_raw_rsp_aux)
+
+text {* lifted section *}
+
+lemma fcard_fempty [simp]:
+  shows "fcard {||} = 0"
+by (lifting fcard_raw_nil)
+
+lemma fcard_finsert_if [simp]:
+  shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
+by (lifting fcard_raw_cons)
+
+
+section {* Induction and Cases rules for finite sets *}
+
+lemma fset_exhaust[case_names fempty finsert, cases type: fset]:
+  shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by (lifting list.exhaust)
+
+lemma fset_induct[case_names fempty finsert]:
+  shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
+by (lifting list.induct)
 
-(*
-lemma mem_rsp[quot_respect]:
-  "(op = ===> op \<approx> ===> op =) (op mem) (op mem)"
+lemma fset_induct2[case_names fempty finsert, induct type: fset]:
+  assumes prem1: "P {||}" 
+  and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
+  shows "P S"
+proof(induct S rule: fset_induct)
+  case fempty
+  show "P {||}" by (rule prem1)
+next
+  case (finsert x S)
+  have asm: "P S" by fact
+  show "P (finsert x S)"
+  proof(cases "x |\<in>| S")
+    case True
+    have "x |\<in>| S" by fact
+    then show "P (finsert x S)" using asm by simp
+  next
+    case False
+    have "x |\<notin>| S" by fact
+    then show "P (finsert x S)" using prem2 asm by simp
+  qed
+qed
+
+
+section {* fmap and fset comprehension *}
+
+quotient_definition
+  "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+as
+ "map"
+
+(* PROPBLEM
+quotient_definition
+  "fconcat :: ('a fset) fset => 'a fset"
+as
+ "concat"
+
+term concat
+term fconcat
 *)
 
+consts
+  fconcat :: "('a fset) fset => 'a fset"
+
+text {* raw section *}
+
+lemma map_rsp_aux:
+  assumes a: "a \<approx> b"
+  shows "map f a \<approx> map f b"
+  using a
+apply(induct a arbitrary: b)
+apply(auto)
+apply(metis rev_image_eqI)
+done
+
+lemma map_rsp[quot_respect]:
+  shows "(op = ===> op \<approx> ===> op \<approx>) map map"
+by (auto simp add: map_rsp_aux)
+
+
+text {* lifted section *}
+
+(* TBD *)
+
+text {* syntax for fset comprehensions (adapted from lists) *}
+
+nonterminals fsc_qual fsc_quals
+
+syntax
+"_fsetcompr" :: "'a \<Rightarrow> fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> 'a fset"  ("{|_ . __")
+"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ <- _")
+"_fsc_test" :: "bool \<Rightarrow> fsc_qual" ("_")
+"_fsc_end" :: "fsc_quals" ("|}")
+"_fsc_quals" :: "fsc_qual \<Rightarrow> fsc_quals \<Rightarrow> fsc_quals" (", __")
+"_fsc_abs" :: "'a => 'b fset => 'b fset"
+
+syntax (xsymbols)
+"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
+syntax (HTML output)
+"_fsc_gen" :: "'a \<Rightarrow> 'a fset \<Rightarrow> fsc_qual" ("_ \<leftarrow> _")
+
+parse_translation (advanced) {*
+let
+  val femptyC = Syntax.const @{const_name fempty};
+  val finsertC = Syntax.const @{const_name finsert};
+  val fmapC = Syntax.const @{const_name fmap};
+  val fconcatC = Syntax.const @{const_name fconcat};
+  val IfC = Syntax.const @{const_name If};
+  fun fsingl x = finsertC $ x $ femptyC;
+
+  fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
+    let
+      val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
+      val e = if opti then fsingl e else e;
+      val case1 = Syntax.const "_case1" $ p $ e;
+      val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
+                                        $ femptyC;
+      val cs = Syntax.const "_case2" $ case1 $ case2
+      val ft = Datatype_Case.case_tr false Datatype.info_of_constr
+                 ctxt [x, cs]
+    in lambda x ft end;
+
+  fun abs_tr ctxt (p as Free(s,T)) e opti =
+        let val thy = ProofContext.theory_of ctxt;
+            val s' = Sign.intern_const thy s
+        in if Sign.declared_const thy s'
+           then (pat_tr ctxt p e opti, false)
+           else (lambda p e, true)
+        end
+    | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
+
+  fun fsc_tr ctxt [e, Const("_fsc_test",_) $ b, qs] =
+        let 
+          val res = case qs of 
+                      Const("_fsc_end",_) => fsingl e
+                    | Const("_fsc_quals",_)$ q $ qs => fsc_tr ctxt [e, q, qs];
+        in 
+          IfC $ b $ res $ femptyC 
+        end
+
+    | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_end",_)] =
+         (case abs_tr ctxt p e true of
+            (f,true) => fmapC $ f $ es
+          | (f, false) => fconcatC $ (fmapC $ f $ es))
+       
+    | fsc_tr ctxt [e, Const("_fsc_gen",_) $ p $ es, Const("_fsc_quals",_) $ q $ qs] =
+        let
+          val e' = fsc_tr ctxt [e, q, qs];
+        in 
+          fconcatC $ (fmapC $ (fst (abs_tr ctxt p e' false)) $ es) 
+        end
+
+in [("_fsetcompr", fsc_tr)] end
+*}
+
+(* examles *)
+term "{|(x,y,z). b|}"
+term "{|x. x \<leftarrow> xs|}"
+term "{|(x,y,z). x\<leftarrow>xs|}"
+term "{|e x y. x\<leftarrow>xs, y\<leftarrow>ys|}"
+term "{|(x,y,z). x<a, x>b|}"
+term "{|(x,y,z). x\<leftarrow>xs, x>b|}"
+term "{|(x,y,z). x<a, x\<leftarrow>xs|}"
+term "{|(x,y). Cons True x \<leftarrow> xs|}"
+term "{|(x,y,z). Cons x [] \<leftarrow> xs|}"
+term "{|(x,y,z). x<a, x>b, x=d|}"
+term "{|(x,y,z). x<a, x>b, y\<leftarrow>ys|}"
+term "{|(x,y,z). x<a, x\<leftarrow>xs,y>b|}"
+term "{|(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys|}"
+term "{|(x,y,z). x\<leftarrow>xs, x>b, y<a|}"
+term "{|(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys|}"
+term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x|}"
+term "{|(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs|}"
+
+
+(* BELOW CONSTRUCTION SITE *)
+
 
 lemma no_mem_nil: 
   "(\<forall>a. a \<notin> set A) = (A = [])"
@@ -108,49 +413,9 @@
     "X = [] \<or> (\<exists>a. a mem X \<and> X \<approx> a # delete_raw X a)"
   by (induct X) (auto)
 
-fun
-  card_raw :: "'a list \<Rightarrow> nat"
-where
-  card_raw_nil: "card_raw [] = 0"
-| card_raw_cons: "card_raw (x # xs) = (if x \<in> set xs then card_raw xs else Suc (card_raw xs))"
 
-lemma not_mem_card_raw:
-  fixes x :: "'a"
-  fixes xs :: "'a list"
-  shows "(\<not>(x mem xs)) = (card_raw (x # xs) = Suc (card_raw xs))"
-  sorry
-
-lemma card_raw_suc:
-  assumes c: "card_raw xs = Suc n"
-  shows "\<exists>a ys. (a \<notin> set ys) \<and> xs \<approx> (a # ys)"
-  using c apply(induct xs)
-  apply(simp)
-  sorry
 
-lemma mem_card_raw_gt_0:
-  "a \<in> set A \<Longrightarrow> 0 < card_raw A"
-  by (induct A) (auto)
 
-lemma card_raw_cons_gt_0:
-  "0 < card_raw (a # A)"
-  by (induct A) (auto)
-
-lemma card_raw_delete_raw:
-  "card_raw (delete_raw A a) = (if a \<in> set A then card_raw A - 1 else card_raw A)"
-sorry
-
-lemma card_raw_rsp_aux:
-  assumes e: "a \<approx> b"
-  shows "card_raw a = card_raw b"
-  using e sorry
-
-lemma card_raw_rsp[quot_respect]:
-  "(op \<approx> ===> op =) card_raw card_raw"
-  by (simp add: card_raw_rsp_aux)
-
-lemma card_raw_0:
-  "(card_raw A = 0) = (A = [])"
-  by (induct A) (auto)
 
 lemma list2set_thm:
   shows "set [] = {}"
@@ -209,26 +474,6 @@
 
 section {* Constants on the Quotient Type *} 
 
-quotient_definition
-  "fempty :: 'a fset" 
-  as "[]::'a list"
-
-quotient_definition
-  "finsert :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" 
-  as "op #"
-
-quotient_definition
-  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
-  as "\<lambda>x X. x \<in> set X"
-
-abbreviation
-  fnotin :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)
-where
-  "a \<notin>f S \<equiv> \<not>(a \<in>f S)"
-
-quotient_definition
-  "fcard :: 'a fset \<Rightarrow> nat" 
-  as "card_raw"
 
 quotient_definition
   "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" 
@@ -271,20 +516,21 @@
 
 thm mem_cons
 thm finite_set_raw_strong_cases
-thm card_raw.simps
-thm not_mem_card_raw
-thm card_raw_suc
+(*thm card_raw.simps*)
+(*thm not_mem_card_raw*)
+(*thm card_raw_suc*)
 
 lemma "fcard X = Suc n \<Longrightarrow> (\<exists>a S. a \<notin>f S & X = finsert a S)"
 (*by (lifting card_raw_suc)*)
 sorry
 
-thm card_raw_cons_gt_0
+(*thm card_raw_cons_gt_0
 thm mem_card_raw_gt_0
 thm not_nil_equiv_cons
+*)
 thm delete_raw.simps
 (*thm mem_delete_raw*)
-thm card_raw_delete_raw
+(*thm card_raw_delete_raw*)
 thm cons_delete_raw
 thm mem_cons_delete_raw
 thm finite_set_raw_delete_raw_cases

--- a/Quot/Examples/IntEx.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -249,7 +249,10 @@
 apply(lifting lam_tst3a)
 apply(rule impI)
 apply(rule lam_tst3a_reg)
-done
+apply(injection)
+sorry
+(* PROBLEM 
+done*)
 
 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
 by auto
@@ -259,7 +262,10 @@
 apply(rule impI)
 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
 apply(simp add: id_rsp)
-done
+apply(injection)
+sorry
+(* PROBLEM 
+done*)
 
 term map
 

--- a/Quot/QuotList.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/QuotList.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -59,7 +59,7 @@
   apply(rule list_rel_rel[OF q])
   done
 
-lemma map_id: "map id \<equiv> id"
+lemma map_id[id_simps]: "map id \<equiv> id"
   apply (rule eq_reflection)
   apply (rule ext)
   apply (rule_tac list="x" in list.induct)

--- a/Quot/QuotMain.thy	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 21 22:36:31 2009 +0100
@@ -166,6 +166,9 @@
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection, symmetric]
+  id_o[THEN eq_reflection]
+  o_id[THEN eq_reflection] 
+
 
 section {* Methods / Interface *}
 

--- a/Quot/quotient_def.ML	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/quotient_def.ML	Mon Dec 21 22:36:31 2009 +0100
@@ -32,6 +32,11 @@
 
 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
@@ -42,7 +47,7 @@
 end
 
 fun get_const flag lthy _ qty =
-(* FIXME: check here that _ and qty are related *)
+(* 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))
@@ -68,14 +73,18 @@
      in
        get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
      end
-  | (Type (s, []), Type (s', [])) =>
+  | (Type (s, _), Type (s', [])) =>
      if s = s'
      then mk_identity qty
      else get_const flag lthy rty qty
   | (Type (s, tys), Type (s', tys')) =>
-     if s = s'
-     then get_fun_aux lthy s' (map (get_fun flag lthy) (tys ~~ tys'))
-     else get_const flag lthy rty qty
+     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

--- a/Quot/quotient_tacs.ML	Sun Dec 20 00:53:35 2009 +0100
+++ b/Quot/quotient_tacs.ML	Mon Dec 21 22:36:31 2009 +0100
@@ -389,7 +389,8 @@
 let
   val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
 in
-  inj_repabs_step_tac ctxt rel_refl
+  simp_tac ((mk_minimal_ss ctxt) addsimps (id_simps_get ctxt)) (* HACK? *) 
+  THEN' inj_repabs_step_tac ctxt rel_refl
 end
 
 fun all_inj_repabs_tac ctxt =
@@ -491,7 +492,7 @@
 (*                                                     *)
 (* 5. Test for refl                                    *)
 
-fun clean_tac lthy =
+fun clean_tac_aux lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
@@ -508,7 +509,7 @@
             TRY o rtac refl]
   end
 
-
+fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *)
 
 (* Tactic for Genralisation of Free Variables in a Goal *)