# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266232514 -3600
# Node ID 538daee762e68e592ecec37836da9af984205500
# Parent  84a38acbf512051e6f9beaf2711e351da3e35f6b
Added a binding to the parser.

diff -r 84a38acbf512 -r 538daee762e6 Quot/Examples/FSet2.thy
--- a/Quot/Examples/FSet2.thy	Mon Feb 15 10:25:17 2010 +0100
+++ b/Quot/Examples/FSet2.thy	Mon Feb 15 12:15:14 2010 +0100
@@ -21,12 +21,14 @@
 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
 by (auto intro: list_eq.intros list_eq_refl)
 
-quotient_type 
+quotient_type
   'a fset = "'a list" / "list_eq"
   by (rule equivp_list_eq)
 
 quotient_definition
-  "fempty :: 'a fset" ("{||}")
+  fempty ("{||}")
+where
+  "fempty :: 'a fset"
 is
   "[]"
 
@@ -40,7 +42,9 @@
 by (auto intro: list_eq.intros)
 
 quotient_definition
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [65,66] 65)
+  funion ("_ \<union>f _" [65,66] 65)
+where
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "(op @)"
 
@@ -67,7 +71,9 @@
 
 
 quotient_definition
-  "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<in>f _" [50, 51] 50)
+  fmem ("_ \<in>f _" [50, 51] 50)
+where
+  "fmem :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 is
   "(op mem)"
 
@@ -80,7 +86,7 @@
   shows "(op = ===> (op \<approx> ===> op =)) (op mem) (op mem)"
   by (simp add: memb_rsp_aux)
 
-definition 
+definition
   fnot_mem :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ \<notin>f _" [50, 51] 50)
 where
   "x \<notin>f S \<equiv> \<not>(x \<in>f S)"
@@ -91,7 +97,9 @@
   "inter_list X Y \<equiv> [x \<leftarrow> X. x\<in>set Y]"
 
 quotient_definition
-  "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
+  finter ("_ \<inter>f _" [70, 71] 70)
+where
+  "finter::'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "inter_list"
 
diff -r 84a38acbf512 -r 538daee762e6 Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Mon Feb 15 10:25:17 2010 +0100
+++ b/Quot/Examples/FSet3.thy	Mon Feb 15 12:15:14 2010 +0100
@@ -32,7 +32,9 @@
 section {* empty fset, finsert and membership *} 
 
 quotient_definition
-  "fempty :: 'a fset" ("{||}")
+  fempty  ("{||}")
+where
+  "fempty :: 'a fset"
 is "[]::'a list"
 
 quotient_definition
@@ -52,7 +54,9 @@
   "memb x xs \<equiv> x \<in> set xs"
 
 quotient_definition
-  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" ("_ |\<in>| _" [50, 51] 50)
+  fin ("_ |\<in>| _" [50, 51] 50)
+where
+  "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool"
 is "memb"
 
 abbreviation
@@ -135,7 +139,9 @@
 section {* Union *}
 
 quotient_definition
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<union>|" 65)
+  funion  (infixl "|\<union>|" 65)
+where
+  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "op @"
 
@@ -622,7 +628,9 @@
   is "delete_raw"
 
 quotient_definition
-  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
+  finter ("_ \<inter>f _" [70, 71] 70)
+where
+  "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   is "inter_raw"
 
 quotient_definition
@@ -703,7 +711,4 @@
 apply (lifting list.cases(2))
 done
 
-thm quot_respect
-
-
 end
diff -r 84a38acbf512 -r 538daee762e6 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Mon Feb 15 10:25:17 2010 +0100
+++ b/Quot/quotient_def.ML	Mon Feb 15 12:15:14 2010 +0100
@@ -10,7 +10,7 @@
   val quotient_def: mixfix -> Attrib.binding -> term -> term ->
     local_theory -> (term * thm) * local_theory
 
-  val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
+  val quotdef_cmd: (Attrib.binding * mixfix) option * (Attrib.binding * (string * string)) ->
     local_theory -> local_theory
 end;
 
@@ -59,24 +59,25 @@
   ((trm, thm), lthy'')
 end
 
-fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
+fun quotdef_cmd (bindmx, (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 mx attr lhs rhs lthy'' |> snd
+  case bindmx of
+    SOME (b, mx) => quotient_def mx attr lhs rhs lthy'' |> snd
+  | _ => quotient_def NoSyn attr lhs rhs lthy'' |> snd
 end
 
 val quotdef_parser =
-  (SpecParse.opt_thm_name ":" --
-     OuterParse.term) --
-      (OuterParse.opt_mixfix' --| OuterParse.$$$ "is" --
-         OuterParse.term)
+  (Scan.option (OuterParse.binding -- OuterParse.opt_mixfix' --| OuterParse.$$$ "where")) --
+    OuterParse.!!! (SpecParse.opt_thm_name ":" -- ((OuterParse.term --| OuterParse.$$$ "is") -- OuterParse.term))
 
-val _ = OuterSyntax.local_theory "quotient_definition"
-	  "definition for constants over the quotient type"
-             OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
+val _ =
+  OuterSyntax.local_theory "quotient_definition"
+    "definition for constants over the quotient type"
+      OuterKeyword.thy_decl (quotdef_parser >> (quotdef_cmd))
 
 end; (* structure *)