# HG changeset patch
# User cek@localhost.localdomain
# Date 1256365466 -7200
# Node ID c1e76f09db70e1712f8bde5d52406c9be200f25f
# Parent  3413aa899aa7fefe65af929c0846b9220465da69
Cleaning the mess

diff -r 3413aa899aa7 -r c1e76f09db70 FSet.thy
--- a/FSet.thy	Sat Oct 24 08:09:40 2009 +0200
+++ b/FSet.thy	Sat Oct 24 08:24:26 2009 +0200
@@ -326,7 +326,7 @@
     LAMBDA_RES_TAC ctxt,
     res_forall_rsp_tac ctxt,
     (
-     (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps res_thms))
+     (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps (res_thms @ @{thms ho_all_prs})))
      THEN_ALL_NEW (fn _ => no_tac)
     ),
     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
@@ -358,13 +358,11 @@
 ML_prf {* val ctxt = @{context} *}
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RES_TAC *)
-prefer 2
 apply (subst FUN_REL.simps)
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (auto)
 done
 
 prove list_induct_t: trm
@@ -389,7 +387,6 @@
 prove m2_t_p: m2_t_g
 apply (atomize(full))
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
-apply (auto)
 done
 
 prove m2_t: m2_t
diff -r 3413aa899aa7 -r c1e76f09db70 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 24 08:09:40 2009 +0200
+++ b/QuotMain.thy	Sat Oct 24 08:24:26 2009 +0200
@@ -3,16 +3,8 @@
 uses ("quotient.ML")
 begin
 
-definition 
-  EQ_TRUE 
-where
-  "EQ_TRUE X \<equiv> (X = True)"
-
-lemma test: "EQ_TRUE ?X"
-  unfolding EQ_TRUE_def
-  by (rule refl)
-
-thm test
+ML {* Pretty.writeln *}
+ML {*  LocalTheory.theory_result *}
 
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
@@ -158,12 +150,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} *}
 
@@ -216,10 +208,8 @@
     (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty))
   end
 
-  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 get_const absF = (Const ("FSet.ABS_" ^ qty_name, rty --> qty), (rty, qty))
+    | get_const repF = (Const ("FSet.REP_" ^ qty_name, qty --> rty), (qty, rty))
 
   fun mk_identity ty = Abs ("", ty, Bound 0)
 
diff -r 3413aa899aa7 -r c1e76f09db70 quotient.ML
--- a/quotient.ML	Sat Oct 24 08:09:40 2009 +0200
+++ b/quotient.ML	Sat Oct 24 08:24:26 2009 +0200
@@ -1,7 +1,6 @@
 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
@@ -9,9 +8,6 @@
   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 =
@@ -45,11 +41,9 @@
    fun merge _ = (op @))
 
 val quotdata_lookup = QuotData.get
-fun quotdata_update_thy (qty, rty, rel) = 
+fun quotdata_update (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)
@@ -180,7 +174,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 )
@@ -217,7 +211,11 @@
   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)