src/Pure/Isar/proof.ML
changeset 8374 ffb2eb084078
parent 8239 07f25f7d2218
child 8383 2dd4823c744f
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Mar 08 18:00:01 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Mar 08 18:02:36 2000 +0100
     1.3 @@ -7,8 +7,8 @@
     1.4  
     1.5  signature BASIC_PROOF =
     1.6  sig
     1.7 -  val FINDGOAL: (int -> tactic) -> tactic
     1.8 -  val HEADGOAL: (int -> tactic) -> tactic
     1.9 +  val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
    1.10 +  val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
    1.11  end;
    1.12  
    1.13  signature PROOF =
    1.14 @@ -41,6 +41,7 @@
    1.15    val level: state -> int
    1.16    type method
    1.17    val method: (thm list -> tactic) -> method
    1.18 +  val method_cases: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> method
    1.19    val refine: (context -> method) -> state -> state Seq.seq
    1.20    val refine_end: (context -> method) -> state -> state Seq.seq
    1.21    val find_free: term -> string -> term option
    1.22 @@ -66,6 +67,7 @@
    1.23      -> state -> state
    1.24    val presume_i: (string * context attribute list * (term * (term list * term list)) list) list
    1.25      -> state -> state
    1.26 +  val invoke_case: string -> state -> state
    1.27    val theorem: bstring -> theory attribute list -> string * (string list * string list)
    1.28      -> theory -> state
    1.29    val theorem_i: bstring -> theory attribute list -> term * (term list * term list)
    1.30 @@ -194,6 +196,7 @@
    1.31  val put_thmss = map_context o ProofContext.put_thmss;
    1.32  val reset_thms = map_context o ProofContext.reset_thms;
    1.33  val assumptions = ProofContext.assumptions o context_of;
    1.34 +val get_case = ProofContext.get_case o context_of;
    1.35  
    1.36  
    1.37  (* facts *)
    1.38 @@ -235,16 +238,16 @@
    1.39  
    1.40  fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
    1.41  
    1.42 -fun map_goal f (State (Node {context, facts, mode, goal = Some goal}, nodes)) =
    1.43 -      State (make_node (context, facts, mode, Some (f goal)), nodes)
    1.44 -  | map_goal f (State (nd, node :: nodes)) =
    1.45 -      let val State (node', nodes') = map_goal f (State (node, nodes))
    1.46 -      in State (nd, node' :: nodes') end
    1.47 -  | map_goal _ state = state;
    1.48 +fun map_goal f g (State (Node {context, facts, mode, goal = Some goal}, nodes)) =
    1.49 +      State (make_node (f context, facts, mode, Some (g goal)), nodes)
    1.50 +  | map_goal f g (State (nd, node :: nodes)) =
    1.51 +      let val State (node', nodes') = map_goal f g (State (node, nodes))
    1.52 +      in map_context f (State (nd, node' :: nodes')) end
    1.53 +  | map_goal _ _ state = state;
    1.54  
    1.55  fun goal_facts get state =
    1.56    state
    1.57 -  |> map_goal (fn ((result, (_, thm)), f) => ((result, (get state, thm)), f));
    1.58 +  |> map_goal I (fn ((result, (_, thm)), f) => ((result, (get state, thm)), f));
    1.59  
    1.60  fun use_facts state =
    1.61    state
    1.62 @@ -341,8 +344,11 @@
    1.63  
    1.64  (* datatype method *)
    1.65  
    1.66 -datatype method = Method of thm list -> tactic;
    1.67 -val method = Method;
    1.68 +datatype method =
    1.69 +  Method of thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq;
    1.70 +
    1.71 +fun method tac = Method (fn facts => fn st => Seq.map (rpair []) (tac facts st));
    1.72 +val method_cases = Method;
    1.73  
    1.74  
    1.75  (* refine goal *)
    1.76 @@ -358,10 +364,10 @@
    1.77      val (goal_ctxt, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
    1.78      val Method meth = meth_fun (if current_context then context_of state else goal_ctxt);
    1.79  
    1.80 -    fun refn thm' =
    1.81 +    fun refn (thm', cases) =
    1.82        state
    1.83        |> check_sign (Thm.sign_of_thm thm')
    1.84 -      |> map_goal (K ((result, (facts, thm')), f));
    1.85 +      |> map_goal (ProofContext.add_cases cases) (K ((result, (facts, thm')), f));
    1.86    in Seq.map refn (meth facts thm) end;
    1.87  
    1.88  in
    1.89 @@ -421,8 +427,8 @@
    1.90    | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
    1.91  
    1.92  fun FINDGOAL tac st =
    1.93 -  let fun find (i, n) = if i > n then no_tac else tac i APPEND find (i + 1, n)
    1.94 -  in find (1, nprems_of st) st end;
    1.95 +  let fun find (i, n) = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1, n))
    1.96 +  in find (1, Thm.nprems_of st) st end;
    1.97  
    1.98  fun HEADGOAL tac = tac 1;
    1.99  
   1.100 @@ -433,7 +439,7 @@
   1.101      val rule = exp raw_rule;
   1.102      val _ = print_rule rule;
   1.103      val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm;
   1.104 -  in Seq.map (fn th => map_goal (K ((result, (facts, th)), f)) state) thmq end;
   1.105 +  in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end;
   1.106  
   1.107  
   1.108  fun export_thm inner thm =
   1.109 @@ -553,6 +559,16 @@
   1.110  end;
   1.111  
   1.112  
   1.113 +(* invoke_case *)
   1.114 +
   1.115 +fun invoke_case name state =
   1.116 +  let val (vars, props) = get_case state name in
   1.117 +    state
   1.118 +    |> fix_i (map (fn (x, T) => ([x], Some T)) vars)
   1.119 +    |> assume_i [("", [], map (fn t => (t, ([], []))) props)]
   1.120 +  end;
   1.121 +
   1.122 +
   1.123  
   1.124  (** goals **)
   1.125