# HG changeset patch
# User wenzelm
# Date 1003185274 -7200
# Node ID 5f0ab6f5c280f64995ddc03f9328e0359fb12cd4
# Parent  311eee3d63b64891a69f9815a394b707f5ac7c4d
support impromptu terminology of cases parameters;

diff -r 311eee3d63b6 -r 5f0ab6f5c280 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Oct 16 00:33:22 2001 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 16 00:34:34 2001 +0200
@@ -363,9 +363,13 @@
     (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
 
+val case_spec =
+  (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.underscore >> K None || P.name >> Some)
+    --| P.$$$ ")") || P.xname >> rpair []) -- P.opt_attribs >> P.triple1;
+
 val caseP =
   OuterSyntax.command "case" "invoke local context" K.prf_asm
-    (P.xthm -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
+    (case_spec -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
 
 
 (* proof structure *)
diff -r 311eee3d63b6 -r 5f0ab6f5c280 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Oct 16 00:33:22 2001 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Tue Oct 16 00:34:34 2001 +0200
@@ -87,8 +87,9 @@
   val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val let_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
   val let_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T
-  val invoke_case: (string * Args.src list) * Comment.text -> ProofHistory.T -> ProofHistory.T
-  val invoke_case_i: (string * Proof.context attribute list) * Comment.text
+  val invoke_case: (string * string option list * Args.src list) * Comment.text
+    -> ProofHistory.T -> ProofHistory.T
+  val invoke_case_i: (string * string option list * Proof.context attribute list) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
   val theorem: string -> ((bstring * Args.src list) * (string * (string list * string list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
@@ -342,8 +343,8 @@
 val let_bind = ProofHistory.apply o Proof.let_bind o map Comment.ignore;
 val let_bind_i = ProofHistory.apply o Proof.let_bind_i o map Comment.ignore;
 
-fun invoke_case ((name, src), comment_ignore) = ProofHistory.apply (fn state =>
-  Proof.invoke_case (name, map (Attrib.local_attribute (Proof.theory_of state)) src) state);
+fun invoke_case ((name, xs, src), comment_ignore) = ProofHistory.apply (fn state =>
+  Proof.invoke_case (name, xs, map (Attrib.local_attribute (Proof.theory_of state)) src) state);
 val invoke_case_i = ProofHistory.apply o Proof.invoke_case o Comment.ignore;
 
 
diff -r 311eee3d63b6 -r 5f0ab6f5c280 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Oct 16 00:33:22 2001 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 16 00:34:34 2001 +0200
@@ -80,7 +80,7 @@
     -> state -> state
   val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
-  val invoke_case: string * context attribute list -> state -> state
+  val invoke_case: string * string option list * context attribute list -> state -> state
   val theorem: string -> bstring -> theory attribute list -> string * (string list * string list)
     -> theory -> state
   val theorem_i: string -> bstring -> theory attribute list -> term * (term list * term list)
@@ -549,10 +549,10 @@
 
 (* invoke_case *)
 
-fun invoke_case (name, atts) state =
+fun invoke_case (name, xs, atts) state =
   let
     val (state', (lets, asms)) =
-      map_context_result (ProofContext.apply_case (get_case state name)) state;
+      map_context_result (ProofContext.apply_case (get_case state name xs)) state;
   in
     state'
     |> add_binds_i lets
diff -r 311eee3d63b6 -r 5f0ab6f5c280 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Oct 16 00:33:22 2001 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Oct 16 00:34:34 2001 +0200
@@ -88,7 +88,7 @@
   val fix: (string list * string option) list -> context -> context
   val fix_i: (string list * typ option) list -> context -> context
   val bind_skolem: context -> string list -> term -> term
-  val get_case: context -> string -> RuleCases.T
+  val get_case: context -> string -> string option list -> RuleCases.T
   val add_cases: (string * RuleCases.T) list -> context -> context
   val apply_case: RuleCases.T -> context -> context * ((indexname * term option) list * term list)
   val show_hyps: bool ref
@@ -953,16 +953,22 @@
 
 (** cases **)
 
-fun check_case ctxt name {fixes, assumes, binds} =
-  if null (foldr Term.add_typ_tvars (map snd fixes, [])) andalso
-    null (foldr Term.add_term_vars (assumes, [])) then
-      {fixes = fixes, assumes = assumes, binds = map drop_schematic binds}
-  else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt);
+fun prep_case ctxt name xs {fixes, assumes, binds} =
+  let
+    fun replace (opt_x :: xs) ((y, T) :: ys) = (if_none opt_x y, T) :: replace xs ys
+      | replace [] ys = ys
+      | replace (_ :: _) [] = raise CONTEXT ("Too many parameters for case " ^ quote name, ctxt);
+  in
+    if null (foldr Term.add_typ_tvars (map snd fixes, [])) andalso
+      null (foldr Term.add_term_vars (assumes, [])) then
+        {fixes = replace xs fixes, assumes = assumes, binds = map drop_schematic binds}
+    else raise CONTEXT ("Illegal schematic variable(s) in case " ^ quote name, ctxt)
+  end;
 
-fun get_case (ctxt as Context {cases, ...}) name =
+fun get_case (ctxt as Context {cases, ...}) name xs =
   (case assoc (cases, name) of
     None => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
-  | Some c => check_case ctxt name c);
+  | Some c => prep_case ctxt name xs c);
 
 
 fun add_cases xs = map_context (fn (thy, data, asms, binds, thms, cases, defs) =>