# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1266247687 -3600
# Node ID 689a18f9484cebbb5ebffbda73308ce0a969d2d4
# Parent  64d896cc16f8d8f837a5b521cbfc8a750262f567
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy

diff -r 64d896cc16f8 -r 689a18f9484c Quot/Examples/AbsRepTest.thy
--- a/Quot/Examples/AbsRepTest.thy	Mon Feb 15 14:58:03 2010 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Mon Feb 15 16:28:07 2010 +0100
@@ -8,49 +8,6 @@
 ML_command "ProofContext.verbose := false"
 *)
 
-ML {*
-val ctxt0 = @{context}
-val ty = Syntax.read_typ ctxt0 "bool"  
-val ctxt1 = Variable.declare_typ ty ctxt0 
-val trm = Syntax.parse_term ctxt1 "A \<and> B"
-val trm' = Syntax.type_constraint ty trm
-val trm'' = Syntax.check_term ctxt1 trm'
-val ctxt2 = Variable.declare_term trm'' ctxt1 
-*}
-
-term "split"
-
-term "Ex1 (\<lambda>(x, y). P x y)" 
-
-lemma "(Ex1 (\<lambda>(x, y). P x y)) \<Longrightarrow> (\<exists>! x. \<exists>! y. P x y)"
-apply(erule ex1E)
-apply(case_tac x)
-apply(clarify)
-apply(rule_tac a="aa" in ex1I)
-apply(rule ex1I)
-apply(assumption)
-apply(blast)
-apply(blast)
-done
-
-(*
-lemma "(\<exists>! x. \<exists>! y. P x y) \<Longrightarrow> (Ex1 (\<lambda>(x, y). P x y))"
-apply(erule ex1E)
-apply(erule ex1E)
-apply(rule_tac a="(x, y)" in ex1I)
-apply(clarify)
-apply(case_tac xa)
-apply(clarify)
-
-apply(rule ex1I)
-apply(assumption)
-apply(blast)
-apply(blast)
-done
-
-apply(metis)
-*)
-
 ML {* open Quotient_Term *}
 
 ML {*
diff -r 64d896cc16f8 -r 689a18f9484c Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Mon Feb 15 14:58:03 2010 +0100
+++ b/Quot/quotient_def.ML	Mon Feb 15 16:28:07 2010 +0100
@@ -7,10 +7,10 @@
 
 signature QUOTIENT_DEF =
 sig
-  val quotient_def: (binding * mixfix) option * (Attrib.binding * (term * term)) ->
+  val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) ->
     local_theory -> (term * thm) * local_theory
 
-  val quotdef_cmd: (binding * mixfix) option * (Attrib.binding * (string * string)) ->
+  val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
     local_theory -> (term * thm) * local_theory
 end;
 
@@ -25,34 +25,36 @@
 (* The ML-interface for a quotient definition takes
    as argument:
 
-    - the mixfix annotation
-    - name and attributes
+    - an optional binding and mixfix annotation
+    - attributes
     - the new constant as term
     - the rhs of the definition as term
 
    It returns the defined constant and its definition
    theorem; stores the data in the qconsts data slot.
 
-   Restriction: At the moment the right-hand side must
-   be a terms composed of constant. Similarly the
-   left-hand side must be a single constant.
+   Restriction: At the moment the right-hand side of the
+   definition must be a constant. Similarly the left-hand 
+   side must be a constant.
 *)
-fun quotient_def (bindmx, (attr, (lhs, rhs))) lthy =
+fun error_msg bind str = 
+  error ("Head of quotient_definition " ^ 
+    (quote str) ^ " differs from declaration " ^ (Binding.name_of bind) ^
+      Position.str_of (Binding.pos_of bind))
+
+fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy =
 let
   val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
   val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
-  val derived_bname = Binding.name lhs_str
-  val (qconst_bname, mx) =
-    case bindmx of
-      SOME (bname, mx) =>
-        let
-          val _ = (Name.of_binding bname = lhs_str) orelse error ("Head of quotient_definition " ^ 
-            (quote lhs_str) ^ " differs from declaration " ^ (Binding.name_of bname) ^
-            Position.str_of (Binding.pos_of bname))
-        in
-          (derived_bname, mx)
-        end
-      | NONE => (derived_bname, NoSyn)
+  
+  fun sanity_test NONE _ = true
+    | sanity_test (SOME bind) str =
+        if Name.of_binding bind = str then true
+        else error_msg bind str
+
+  val _ = sanity_test optbind lhs_str
+
+  val qconst_bname = Binding.name lhs_str
   val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
   val (_, prop') = LocalDefs.cert_def lthy prop
@@ -69,20 +71,26 @@
   ((trm, thm), lthy'')
 end
 
-fun quotdef_cmd (bindmx, (attr, (lhs_str, rhs_str))) lthy =
+fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy =
 let
   val lhs = Syntax.read_term lthy lhs_str
   val rhs = Syntax.read_term lthy rhs_str
   val lthy' = Variable.declare_term lhs lthy
   val lthy'' = Variable.declare_term rhs lthy'
 in
-  quotient_def (bindmx, (attr, (lhs, rhs))) lthy''
+  quotient_def (decl, (attr, (lhs, rhs))) lthy''
 end
 
-val binding_mixfix_parser = OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where"
+local
+  structure P = OuterParse;
+in
+
+val quotdef_decl = (P.binding >> SOME) -- P.opt_mixfix' --| P.$$$ "where"
+
 val quotdef_parser =
-  (Scan.option binding_mixfix_parser) --
-    OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term))
+  Scan.optional quotdef_decl (NONE, NoSyn) -- 
+    P.!!! (SpecParse.opt_thm_name ":" -- (P.term --| P.$$$ "is" -- P.term))
+end
 
 val _ =
   OuterSyntax.local_theory "quotient_definition"