# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259845193 -3600
# Node ID d2c9a72e52e03b28d08e399346a9dcc781212fd2
# Parent  6b2f6e7e62cc4efeed90be48132c94629d5a4995
first version of internalised quotient theorems; added FIXME-TODO

diff -r 6b2f6e7e62cc -r d2c9a72e52e0 FIXME-TODO
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/FIXME-TODO	Thu Dec 03 13:59:53 2009 +0100
@@ -0,0 +1,30 @@
+Higher Priority
+===============
+
+- redoing Int.thy (problem at the moment with overloaded
+  definitions....Florian)
+
+- have FSet.thy to have a simple infrastructure for 
+  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
+
+- Ask Peter and Michael for challenging examples 
+
+
+
+
+
+
+
+
+Lower Priority
+==============
+
+- find clean ways how to write down the "mathematical"
+  procedure for a possible submission (Peter submitted 
+  his work only to TPHOLs 2005...we would have to go
+  maybe for the Journal of Formalised Mathematics)
\ No newline at end of file
diff -r 6b2f6e7e62cc -r d2c9a72e52e0 QuotMain.thy
--- a/QuotMain.thy	Thu Dec 03 11:40:10 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 13:59:53 2009 +0100
@@ -716,7 +716,7 @@
 section {* RepAbs Injection Tactic *}
 
 (* TODO: check if it still works with first_order_match *)
-(* FIXME/TODO: do not handle everything *)x
+(* FIXME/TODO: do not handle everything *)
 ML {*
 fun instantiate_tac thm = 
   Subgoal.FOCUS (fn {concl, ...} =>
diff -r 6b2f6e7e62cc -r d2c9a72e52e0 quotient.ML
--- a/quotient.ML	Thu Dec 03 11:40:10 2009 +0100
+++ b/quotient.ML	Thu Dec 03 13:59:53 2009 +0100
@@ -5,7 +5,6 @@
   val quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
   val quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
 
-  val note: binding * thm -> local_theory -> thm * local_theory
 end;
 
 structure Quotient: QUOTIENT =
@@ -22,9 +21,9 @@
   ((rhs, thm), lthy')
 end
 
-fun note (name, thm) lthy =
+fun note (name, thm, attrs) lthy =
 let
-  val ((_,[thm']), lthy') = Local_Theory.note ((name, []), [thm]) lthy
+  val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy
 in
   (thm', lthy')
 end
@@ -158,7 +157,7 @@
   (* FIXME: to recalculated in for example REGULARIZE *)
 
   (* storing of the equiv_thm under a name *)
-  val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm) lthy3
+  val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm, []) lthy3
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
@@ -179,8 +178,8 @@
     Expression.Named [("R", rel), ("Abs", abs), ("Rep", rep) ]))]
 in
   lthy6
-  |> note (quot_thm_name, quot_thm)
-  ||>> note (quotient_thm_name, quotient_thm)
+  |> note (quot_thm_name, quot_thm, [])
+  ||>> note (quotient_thm_name, quotient_thm, [Attrib.internal (K quotient_rules_add)])
   ||> Local_Theory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];
diff -r 6b2f6e7e62cc -r d2c9a72e52e0 quotient_info.ML
--- a/quotient_info.ML	Thu Dec 03 11:40:10 2009 +0100
+++ b/quotient_info.ML	Thu Dec 03 13:59:53 2009 +0100
@@ -21,6 +21,8 @@
   val print_qconstinfo: Proof.context -> unit
 
   val rsp_rules_get: Proof.context -> thm list  
+  val quotient_rules_get: Proof.context -> thm list
+  val quotient_rules_add: attribute
 end;
 
 structure Quotient_Info: QUOTIENT_INFO =
@@ -161,7 +163,18 @@
 
 val rsp_rules_get = RspRules.get
 
-val _ = Context.>> (Context.map_theory RspRules.setup)
+(* quotient lemmas *)
+structure QuotientRules = Named_Thms
+  (val name = "quotient"
+   val description = "Quotient theorems.")
+
+val quotient_rules_get = QuotientRules.get
+val quotient_rules_add = Thm.declaration_attribute QuotientRules.add_thm
+
+(* setup of the theorem lists *)
+val _ = Context.>> (Context.map_theory 
+    (RspRules.setup #>
+     QuotientRules.setup))
 
 end; (* structure *)