--- a/src/Pure/Isar/method.ML Tue Feb 14 19:29:54 2012 +0100
+++ b/src/Pure/Isar/method.ML Tue Feb 14 19:51:39 2012 +0100
@@ -4,16 +4,8 @@
Isar proof methods.
*)
-signature BASIC_METHOD =
-sig
- val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
- val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
- val rule_trace: bool Config.T
-end;
-
signature METHOD =
sig
- include BASIC_METHOD
type method
val apply: (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
@@ -42,6 +34,7 @@
val all_assm_tac: Proof.context -> tactic
val assumption: Proof.context -> method
val close: bool -> Proof.context -> method
+ val rule_trace: bool Config.T
val trace: Proof.context -> thm list -> unit
val rule_tac: thm list -> thm list -> int -> tactic
val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
@@ -89,18 +82,6 @@
structure Method: METHOD =
struct
-(** generic tools **)
-
-(* goal addressing *)
-
-fun FINDGOAL tac st =
- 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;
-
-
-
(** proof methods **)
(* datatype method *)
@@ -483,9 +464,6 @@
end;
-structure Basic_Method: BASIC_METHOD = Method;
-open Basic_Method;
-
val RAW_METHOD_CASES = Method.RAW_METHOD_CASES;
val RAW_METHOD = Method.RAW_METHOD;
val METHOD_CASES = Method.METHOD_CASES;
--- a/src/Pure/Isar/proof.ML Tue Feb 14 19:29:54 2012 +0100
+++ b/src/Pure/Isar/proof.ML Tue Feb 14 19:51:39 2012 +0100
@@ -36,7 +36,6 @@
val refine: Method.text -> state -> state Seq.seq
val refine_end: Method.text -> state -> state Seq.seq
val refine_insert: thm list -> state -> state
- val goal_tac: thm -> int -> tactic
val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
val goal: state -> {context: context, facts: thm list, goal: thm}
@@ -444,6 +443,8 @@
(* refine via sub-proof *)
+local
+
fun finish_tac 0 = K all_tac
| finish_tac n =
Goal.norm_hhf_tac THEN'
@@ -457,6 +458,12 @@
Tactic.rtac rule THEN'
finish_tac (Thm.nprems_of rule);
+fun FINDGOAL tac st =
+ 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;
+
+in
+
fun refine_goals print_rule inner raw_rules state =
let
val (outer, (_, goal)) = get_goal state;
@@ -467,6 +474,8 @@
|> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
end;
+end;
+
(* conclude_goal *)
--- a/src/Pure/tactical.ML Tue Feb 14 19:29:54 2012 +0100
+++ b/src/Pure/tactical.ML Tue Feb 14 19:51:39 2012 +0100
@@ -48,6 +48,7 @@
val ALLGOALS: (int -> tactic) -> tactic
val SOMEGOAL: (int -> tactic) -> tactic
val FIRSTGOAL: (int -> tactic) -> tactic
+ val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
val REPEAT_SOME: (int -> tactic) -> tactic
val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
val REPEAT_FIRST: (int -> tactic) -> tactic
@@ -314,6 +315,9 @@
let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n)
in find(1, nprems_of st)st end;
+(*First subgoal only.*)
+fun HEADGOAL tac = tac 1;
+
(*Repeatedly solve some using tac. *)
fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac));
fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac));