# HG changeset patch
# User wenzelm
# Date 1133387566 -3600
# Node ID f18a54840629e63901df2551a5fb746cf1a7bded
# Parent  92af40e5d7b7ee0ab52c38137db5245b7d337646
simulaneous 'def';

diff -r 92af40e5d7b7 -r f18a54840629 NEWS
--- a/NEWS	Wed Nov 30 21:51:23 2005 +0100
+++ b/NEWS	Wed Nov 30 22:52:46 2005 +0100
@@ -61,6 +61,10 @@
   have "!!x. P x ==> Q x" by fact  ==  note `!!x. P x ==> Q x`
   have "P a ==> Q a" by fact       ==  note `P a ==> Q a`
 
+* Isar: 'def' now admits simultaneous definitions, e.g.:
+
+  def x == "t" and y == "u"
+
 * Provers/induct: improved internal context management to support
 local fixes and defines on-the-fly.  Thus explicit meta-level
 connectives !! and ==> are rarely required anymore in inductive goals
diff -r 92af40e5d7b7 -r f18a54840629 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Wed Nov 30 21:51:23 2005 +0100
+++ b/doc-src/IsarRef/pure.tex	Wed Nov 30 22:52:46 2005 +0100
@@ -709,7 +709,9 @@
   ;
   ('assume' | 'presume') (props + 'and')
   ;
-  'def' thmdecl? \\ name ('==' | equiv) term termpat?
+  'def' (def + 'and')
+  ;
+  def: thmdecl? \\ name ('==' | equiv) term termpat?
   ;
 \end{rail}
 
@@ -733,7 +735,8 @@
   ``$\DEF{}{x \equiv t}$'' abbreviates ``$\FIX{x}~\ASSUME{}{x \equiv t}$'',
   with the resulting hypothetical equation solved by reflexivity.
   
-  The default name for the definitional equation is $x_def$.
+  The default name for the definitional equation is $x_def$.  Several
+  simultaneous definitions may be given at the same time.
 
 \end{descr}
 
diff -r 92af40e5d7b7 -r f18a54840629 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Nov 30 21:51:23 2005 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 30 22:52:46 2005 +0100
@@ -421,8 +421,9 @@
 val defP =
   OuterSyntax.command "def" "local definition"
     (K.tag_proof K.prf_asm)
-    (P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp))
-      >> (Toplevel.print oo (Toplevel.proof o uncurry Proof.def)));
+    (P.and_list1
+      (P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
+    >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
 
 val obtainP =
   OuterSyntax.command "obtain" "generalized existence"
diff -r 92af40e5d7b7 -r f18a54840629 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Nov 30 21:51:23 2005 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Nov 30 22:52:46 2005 +0100
@@ -58,8 +58,10 @@
     -> state -> state
   val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
-  val def: string * Attrib.src list -> string *  (string * string list) -> state -> state
-  val def_i: string * context attribute list -> string * (term * term list) -> state -> state
+  val def: ((string * Attrib.src list) * (string * (string * string list))) list ->
+    state -> state
+  val def_i: ((string * context attribute list) * (string * (term * term list))) list ->
+    state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
@@ -496,7 +498,7 @@
 fun gen_bind bind args state =
   state
   |> assert_forward
-  |> map_context (bind args)
+  |> map_context (bind args #> snd)
   |> put_facts NONE;
 
 in
@@ -552,29 +554,26 @@
 
 local
 
-fun gen_def fix prep_att prep_term prep_pats
-    (raw_name, raw_atts) (x, (raw_rhs, raw_pats)) state =
+fun gen_def fix prep_att prep_binds args state =
   let
     val _ = assert_forward state;
     val thy = theory_of state;
-    val ctxt = context_of state;
 
-    val rhs = prep_term ctxt raw_rhs;
-    val pats = prep_pats (Term.fastype_of rhs) (ProofContext.declare_term rhs ctxt) raw_pats;
-    val eq = ProofContext.mk_def ctxt (x, rhs);
-    val name = if raw_name = "" then Thm.def_name x else raw_name;
-    val atts = map (prep_att thy) raw_atts;
+    val ((raw_names, raw_atts), (xs, raw_rhss)) = args |> split_list |>> split_list ||> split_list;
+    val names = map (fn ("", x) => Thm.def_name x | (name, _) => name) (raw_names ~~ xs);
+    val atts = map (map (prep_att thy)) raw_atts;
+    val (rhss, state') = state |> map_context_result (prep_binds false (map swap raw_rhss));
+    val eqs = ProofContext.mk_def (context_of state') (xs ~~ rhss);
   in
-    state
-    |> fix [([x], NONE)]
-    |> match_bind_i [(pats, rhs)]
-    |> assm_i ProofContext.export_def [((name, atts), [(eq, ([], []))])]
+    state'
+    |> fix [(xs, NONE)]
+    |> assm_i ProofContext.export_def ((names ~~ atts) ~~ map (fn eq => [(eq, ([], []))]) eqs)
   end;
 
 in
 
-val def = gen_def fix Attrib.local_attribute ProofContext.read_term ProofContext.read_term_pats;
-val def_i = gen_def fix_i (K I) ProofContext.cert_term ProofContext.cert_term_pats;
+val def = gen_def fix Attrib.local_attribute ProofContext.match_bind;
+val def_i = gen_def fix_i (K I) ProofContext.match_bind_i;
 
 end;