--- a/QuotMain.thy	Mon Oct 12 13:58:31 2009 +0200
+++ b/QuotMain.thy	Mon Oct 12 14:30:50 2009 +0200
@@ -3,6 +3,7 @@
 uses ("quotient.ML")
 begin
 
+
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -145,6 +146,7 @@
 
 use "quotient.ML"
 
+
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
   let
@@ -223,7 +225,7 @@
 
 text {* information about map-functions for type-constructor *}
 ML {*
-type typ_info = {mapfun: string}
+type typ_info = {mapfun: string, relfun: string}
 
 local
   structure Data = TheoryDataFun
@@ -240,9 +242,9 @@
 
 (* mapfuns for some standard types *)
 setup {*
-  update @{type_name "list"} {mapfun = @{const_name "map"}} #> 
-  update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}} #> 
-  update @{type_name "fun"}  {mapfun = @{const_name "fun_map"}}
+  update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #> 
+  update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = "???"} #> 
+  update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
 *}
 
 ML {* lookup @{theory} @{type_name list} *}
@@ -285,7 +287,7 @@
 *}
 
 ML {*
-  get_fun repF @{typ t} @{typ qt} @{context} @{typ "t * nat"}
+  get_fun repF @{typ t} @{typ qt} @{context} @{typ "((t \<Rightarrow> t) list) * nat"}
   |> fst
   |> Syntax.string_of_term @{context}
   |> writeln
@@ -298,6 +300,32 @@
   |> writeln
 *}
 
+(*
+ML {*
+fun tyRel ty rty rel lthy =
+  if ty = rty 
+  then rel
+  else (case ty of
+         Type (s, tys) => 
+            (case (lookup (ProofContext.theory_of lthy) s) of
+               SOME (info) => list_comb (Const (#relfun info, ?????), map (tyRel ???) tys)
+               NONE  => (op =):: tys
+            )
+        | _ => (op =):: ty)
+*}
+
+ML {*
+
+fun regularise trm \<Rightarrow> new_trm 
+  (case trm of
+     ??
+  )
+*}
+
+fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
+  trm == new_trm
+*)
+
 text {* produces the definition for a lifted constant *}
 ML {*
 fun get_const_def nconst oconst rty qty lthy =

--- a/quotient.ML	Mon Oct 12 13:58:31 2009 +0200
+++ b/quotient.ML	Mon Oct 12 14:30:50 2009 +0200
@@ -162,6 +162,26 @@
       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 end
 
+(* syntax setup *)
+local structure P = OuterParse in
+
+val quottype_parser = 
+    (P.type_args -- P.binding) -- 
+      P.opt_infix -- 
+       (P.$$$ "=" |-- P.term) -- 
+         (P.$$$ "/" |-- P.term)
+           
+(*
+val _ =
+  OuterSyntax.command "quotient" "quotient type definition (requires equivalence proof)"
+    OuterKeyword.thy_goal
+    (typedef_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef)));
+
+end;
+*)
+
+end;
+
 end;
 
 open Quotient
\ No newline at end of file