src/Pure/Isar/proof.ML

--- a/src/Pure/Isar/proof.ML	Wed Mar 08 18:00:01 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Mar 08 18:02:36 2000 +0100
@@ -7,8 +7,8 @@
 
 signature BASIC_PROOF =
 sig
-  val FINDGOAL: (int -> tactic) -> tactic
-  val HEADGOAL: (int -> tactic) -> tactic
+  val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
+  val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
 end;
 
 signature PROOF =
@@ -41,6 +41,7 @@
   val level: state -> int
   type method
   val method: (thm list -> tactic) -> method
+  val method_cases: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> method
   val refine: (context -> method) -> state -> state Seq.seq
   val refine_end: (context -> method) -> state -> state Seq.seq
   val find_free: term -> string -> term option
@@ -66,6 +67,7 @@
     -> state -> state
   val presume_i: (string * context attribute list * (term * (term list * term list)) list) list
     -> state -> state
+  val invoke_case: string -> state -> state
   val theorem: bstring -> theory attribute list -> string * (string list * string list)
     -> theory -> state
   val theorem_i: bstring -> theory attribute list -> term * (term list * term list)
@@ -194,6 +196,7 @@
 val put_thmss = map_context o ProofContext.put_thmss;
 val reset_thms = map_context o ProofContext.reset_thms;
 val assumptions = ProofContext.assumptions o context_of;
+val get_case = ProofContext.get_case o context_of;
 
 
 (* facts *)
@@ -235,16 +238,16 @@
 
 fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
 
-fun map_goal f (State (Node {context, facts, mode, goal = Some goal}, nodes)) =
-      State (make_node (context, facts, mode, Some (f goal)), nodes)
-  | map_goal f (State (nd, node :: nodes)) =
-      let val State (node', nodes') = map_goal f (State (node, nodes))
-      in State (nd, node' :: nodes') end
-  | map_goal _ state = state;
+fun map_goal f g (State (Node {context, facts, mode, goal = Some goal}, nodes)) =
+      State (make_node (f context, facts, mode, Some (g goal)), nodes)
+  | map_goal f g (State (nd, node :: nodes)) =
+      let val State (node', nodes') = map_goal f g (State (node, nodes))
+      in map_context f (State (nd, node' :: nodes')) end
+  | map_goal _ _ state = state;
 
 fun goal_facts get state =
   state
-  |> map_goal (fn ((result, (_, thm)), f) => ((result, (get state, thm)), f));
+  |> map_goal I (fn ((result, (_, thm)), f) => ((result, (get state, thm)), f));
 
 fun use_facts state =
   state
@@ -341,8 +344,11 @@
 
 (* datatype method *)
 
-datatype method = Method of thm list -> tactic;
-val method = Method;
+datatype method =
+  Method of thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq;
+
+fun method tac = Method (fn facts => fn st => Seq.map (rpair []) (tac facts st));
+val method_cases = Method;
 
 
 (* refine goal *)
@@ -358,10 +364,10 @@
     val (goal_ctxt, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
     val Method meth = meth_fun (if current_context then context_of state else goal_ctxt);
 
-    fun refn thm' =
+    fun refn (thm', cases) =
       state
       |> check_sign (Thm.sign_of_thm thm')
-      |> map_goal (K ((result, (facts, thm')), f));
+      |> map_goal (ProofContext.add_cases cases) (K ((result, (facts, thm')), f));
   in Seq.map refn (meth facts thm) end;
 
 in
@@ -421,8 +427,8 @@
   | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
 
 fun FINDGOAL tac st =
-  let fun find (i, n) = if i > n then no_tac else tac i APPEND find (i + 1, n)
-  in find (1, nprems_of st) st end;
+  let fun find (i, n) = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1, n))
+  in find (1, Thm.nprems_of st) st end;
 
 fun HEADGOAL tac = tac 1;
 
@@ -433,7 +439,7 @@
     val rule = exp raw_rule;
     val _ = print_rule rule;
     val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm;
-  in Seq.map (fn th => map_goal (K ((result, (facts, th)), f)) state) thmq end;
+  in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end;
 
 
 fun export_thm inner thm =
@@ -553,6 +559,16 @@
 end;
 
 
+(* invoke_case *)
+
+fun invoke_case name state =
+  let val (vars, props) = get_case state name in
+    state
+    |> fix_i (map (fn (x, T) => ([x], Some T)) vars)
+    |> assume_i [("", [], map (fn t => (t, ([], []))) props)]
+  end;
+
+
 
 (** goals **)