# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256340809 -7200
# Node ID 2c83d04262f9b78b62676285b6fddad785509ad1
# Parent  4f00ca4f5ef487766386347e821cce2a632878be
fixed problem with incorrect ABS/REP name

diff -r 4f00ca4f5ef4 -r 2c83d04262f9 FSet.thy
--- a/FSet.thy	Fri Oct 23 18:20:06 2009 +0200
+++ b/FSet.thy	Sat Oct 24 01:33:29 2009 +0200
@@ -2,6 +2,49 @@
 imports QuotMain
 begin
 
+(* test for get_fun *)
+datatype t =
+   vr "string"
+ | ap "t list"
+ | lm "string" "t"
+
+consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
+axioms t_eq: "EQUIV Rt"
+
+quotient qt = "t" / "Rt"
+    by (rule t_eq)
+
+setup {*
+  maps_update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
+  maps_update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
+  maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
+*}
+
+
+ML {*
+get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
+ |> fst
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
+
+ML {*
+get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
+ |> fst
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
+
+ML {*
+get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
+ |> fst
+ |> Syntax.pretty_term @{context}
+ |> Pretty.string_of
+ |> writeln
+*}
+(* end test get_fun *)
+
+
 inductive
   list_eq (infix "\<approx>" 50)
 where
diff -r 4f00ca4f5ef4 -r 2c83d04262f9 QuotMain.thy
--- a/QuotMain.thy	Fri Oct 23 18:20:06 2009 +0200
+++ b/QuotMain.thy	Sat Oct 24 01:33:29 2009 +0200
@@ -3,8 +3,16 @@
 uses ("quotient.ML")
 begin
 
-ML {* Pretty.writeln *}
-ML {*  LocalTheory.theory_result *}
+definition 
+  EQ_TRUE 
+where
+  "EQ_TRUE X \<equiv> (X = True)"
+
+lemma test: "EQ_TRUE ?X"
+  unfolding EQ_TRUE_def
+  by (rule refl)
+
+thm test
 
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -150,12 +158,12 @@
 use "quotient.ML"
 
 (* mapfuns for some standard types *)
-setup {*
-  maps_update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
-  maps_update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
-  maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
-*}
 
+ML {* quotdata_lookup @{theory} *}
+setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*}
+ML {* quotdata_lookup @{theory} *}
+
+ML {* print_quotdata @{context} *}
 
 ML {* maps_lookup @{theory} @{type_name list} *}
 
@@ -208,8 +216,10 @@
     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
   end
 
-  fun get_const absF = (Const ("FSet.ABS_" ^ qty_name, rty --> qty), (rty, qty))
-    | get_const repF = (Const ("FSet.REP_" ^ qty_name, qty --> rty), (qty, rty))
+  val thy = ProofContext.theory_of lthy
+
+  fun get_const absF = (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty))
+    | get_const repF = (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty))
 
   fun mk_identity ty = Abs ("", ty, Bound 0)
 
diff -r 4f00ca4f5ef4 -r 2c83d04262f9 quotient.ML
--- a/quotient.ML	Fri Oct 23 18:20:06 2009 +0200
+++ b/quotient.ML	Sat Oct 24 01:33:29 2009 +0200
@@ -1,6 +1,7 @@
 signature QUOTIENT =
 sig
   type maps_info = {mapfun: string, relfun: string}
+  type quotient_info = {qtyp: typ, rtyp: typ, rel: term}
   val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
@@ -8,6 +9,9 @@
   val maps_lookup: theory -> string -> maps_info option
   val maps_update: string -> maps_info -> theory -> theory                                  
   val print_quotdata: Proof.context -> unit
+  val quotdata_lookup: theory -> quotient_info list
+  val quotdata_update_thy: (typ * typ * term) -> theory -> theory
+  val quotdata_update: (typ * typ * term) -> Proof.context -> Proof.context
 end;
 
 structure Quotient: QUOTIENT =
@@ -41,9 +45,11 @@
    fun merge _ = (op @))
 
 val quotdata_lookup = QuotData.get
-fun quotdata_update (qty, rty, rel) = 
+fun quotdata_update_thy (qty, rty, rel) = 
       QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls)
 
+fun quotdata_update (qty, rty, rel) = ProofContext.theory (quotdata_update_thy (qty, rty, rel))
+
 fun print_quotdata ctxt =
 let
   val quots = QuotData.get (ProofContext.theory_of ctxt)
@@ -174,7 +180,7 @@
   val rep = Const (rep_name, abs_ty --> rep_ty)
 
   (* storing the quot-info *)
-  val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy)
+  (*val _ = quotdata_update (abs_ty, rty, rel) (ProofContext.theory_of lthy)*)
 
   (* ABS and REP definitions *)
   val ABS_const = Const (@{const_name "QUOT_TYPE.ABS"}, dummyT )
@@ -211,11 +217,7 @@
   val mthdt = Method.Basic (fn _ => mthd)
   val bymt = Proof.global_terminal_proof (mthdt, NONE)
   val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
-    Expression.Named [
-     ("R", rel),
-     ("Abs", abs),
-     ("Rep", rep)
-    ]))]
+    Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
 in
   lthy4
   |> note (quot_thm_name, quot_thm)