--- a/src/HOL/datatype.ML Tue Jul 22 11:12:55 1997 +0200
+++ b/src/HOL/datatype.ML Tue Jul 22 11:14:18 1997 +0200
@@ -6,10 +6,11 @@
*)
(* should go into Pure *)
-fun ALLNEWSUBGOALS tac tacf i =
- STATE (fn state0 => tac i THEN
- STATE (fn state1 => let val d = nprems_of state1 - nprems_of state0
- in EVERY(map tacf ((i+d) downto i)) end));
+fun ALLNEWSUBGOALS tac tacf i st0 = st0 |>
+ (tac i THEN
+ (fn st1 => st1 |>
+ let val d = nprems_of st1 - nprems_of st0
+ in EVERY(map tacf ((i+d) downto i)) end));
(*used for constructor parameters*)
datatype dt_type = dtVar of string |
@@ -878,12 +879,11 @@
fun exhaust_tac a =
ALLNEWSUBGOALS (res_inst_tac [(exh_var,a)] exhaustion)
(rotate_tac ~1);
- fun induct_tac a i =
- STATE(fn st =>
+ fun induct_tac a i st = st |>
(if Datatype.occs_in_prems a i st
then warning "Induction variable occurs also among premises!"
else ();
- itac a i))
+ itac a i)
in
(ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
case_const = const (ty^"_case"),
--- a/src/HOL/simpdata.ML Tue Jul 22 11:12:55 1997 +0200
+++ b/src/HOL/simpdata.ML Tue Jul 22 11:14:18 1997 +0200
@@ -388,20 +388,20 @@
(* rot_eq_tac rotates the first equality premise of subgoal i to the front,
fails if there is no equaliy or if an equality is already at the front *)
-fun rot_eq_tac i =
- let fun is_eq (Const ("Trueprop", _) $ (Const("op =",_) $ _ $ _)) = true
- | is_eq _ = false;
- fun find_eq n [] = None
- | find_eq n (t :: ts) = if (is_eq t) then Some n
- else find_eq (n + 1) ts;
- fun rot_eq state =
- let val (_, _, Bi, _) = dest_state (state, i)
- in case find_eq 0 (Logic.strip_assums_hyp Bi) of
+local
+ fun is_eq (Const ("Trueprop", _) $ (Const("op =" ,_) $ _ $ _)) = true
+ | is_eq _ = false;
+ fun find_eq n [] = None
+ | find_eq n (t :: ts) = if (is_eq t) then Some n
+ else find_eq (n + 1) ts;
+in
+val rot_eq_tac =
+ SUBGOAL (fn (Bi,i) =>
+ case find_eq 0 (Logic.strip_assums_hyp Bi) of
None => no_tac
| Some 0 => no_tac
- | Some n => rotate_tac n i
- end;
- in STATE rot_eq end;
+ | Some n => rotate_tac n i)
+end;
(*an unsatisfactory fix for the incomplete asm_full_simp_tac!
better: asm_really_full_simp_tac, a yet to be implemented version of
--- a/src/HOL/thy_data.ML Tue Jul 22 11:12:55 1997 +0200
+++ b/src/HOL/thy_data.ML Tue Jul 22 11:14:18 1997 +0200
@@ -85,23 +85,19 @@
in
(* generic induction tactic for datatypes *)
-fun induct_tac var i =
- let fun induct state =
+fun induct_tac var i state = state |>
let val (_, _, Bi, _) = dest_state (state, i)
val sign = #sign(rep_thm state)
val tn = find_tname var Bi
val ind_tac = #induct_tac(get_dt_info sign tn)
- in ind_tac var i end
- in STATE induct end;
+ in ind_tac var i end;
(* generic exhaustion tactic for datatypes *)
-fun exhaust_tac aterm i =
- let fun exhaust state =
+fun exhaust_tac aterm i state = state |>
let val sign = #sign(rep_thm state)
val tn = infer_tname state sign i aterm
val exh_tac = #exhaust_tac(get_dt_info sign tn)
- in exh_tac aterm i end
- in STATE exhaust end;
+ in exh_tac aterm i end;
end;
--- a/src/Pure/search.ML Tue Jul 22 11:12:55 1997 +0200
+++ b/src/Pure/search.ML Tue Jul 22 11:14:18 1997 +0200
@@ -66,19 +66,17 @@
(*Execute tac1, but only execute tac2 if there are at least as many subgoals
as before. This ensures that tac2 is only applied to an outcome of tac1.*)
-fun tac1 THEN_MAYBE tac2 = STATE
- (fn st => tac1 THEN
- COND (has_fewer_prems (nprems_of st)) all_tac tac2);
+fun (tac1 THEN_MAYBE tac2) st =
+ (tac1 THEN COND (has_fewer_prems (nprems_of st)) all_tac tac2) st;
fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
(*Tactical to reduce the number of premises by 1.
If no subgoals then it must fail! *)
-fun DEPTH_SOLVE_1 tac = STATE
- (fn st =>
+fun DEPTH_SOLVE_1 tac st = st |>
(case nprems_of st of
0 => no_tac
- | n => DEPTH_FIRST (has_fewer_prems n) tac));
+ | n => DEPTH_FIRST (has_fewer_prems n) tac);
(*Uses depth-first search to solve ALL subgoals*)
val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
@@ -166,12 +164,11 @@
(*Simple iterative deepening tactical. It merely "deepens" any search tactic
using increment "inc" up to limit "lim". *)
fun DEEPEN (inc,lim) tacf m i =
- let fun dpn m = STATE(fn state =>
- if has_fewer_prems i state then no_tac
- else if m>lim then
- (writeln "Giving up..."; no_tac)
- else (writeln ("Depth = " ^ string_of_int m);
- tacf m i ORELSE dpn (m+inc)))
+ let fun dpn m st = st |> (if has_fewer_prems i st then no_tac
+ else if m>lim then
+ (writeln "Giving up..."; no_tac)
+ else (writeln ("Depth = " ^ string_of_int m);
+ tacf m i ORELSE dpn (m+inc)))
in dpn m end;
(*** Best-first search ***)
--- a/src/Pure/tactic.ML Tue Jul 22 11:12:55 1997 +0200
+++ b/src/Pure/tactic.ML Tue Jul 22 11:14:18 1997 +0200
@@ -269,12 +269,10 @@
subgoal. Fails if "i" is out of range. ***)
(*compose version: arguments are as for bicompose.*)
-fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i =
- STATE ( fn st =>
- compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule),
- nsubgoal) i
- handle TERM (msg,_) => (writeln msg; no_tac)
- | THM (msg,_,_) => (writeln msg; no_tac) );
+fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i st = st |>
+ (compose_tac (bires_flg, lift_inst_rule (st, i, sinsts, rule), nsubgoal) i
+ handle TERM (msg,_) => (writeln msg; no_tac)
+ | THM (msg,_,_) => (writeln msg; no_tac));
(*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the
terms that are substituted contain (term or type) unknowns from the
--- a/src/Sequents/prover.ML Tue Jul 22 11:12:55 1997 +0200
+++ b/src/Sequents/prover.ML Tue Jul 22 11:14:18 1997 +0200
@@ -85,13 +85,13 @@
fun RESOLVE_THEN rules =
let val [rls0,rls1,rls2] = partition_list has_prems 0 2 rules;
- fun tac nextac i = STATE (fn state =>
- filseq_resolve_tac rls0 9999 i
- ORELSE
- (DETERM(filseq_resolve_tac rls1 9999 i) THEN TRY(nextac i))
- ORELSE
- (DETERM(filseq_resolve_tac rls2 9999 i) THEN TRY(nextac(i+1))
- THEN TRY(nextac i)) )
+ fun tac nextac i state = state |>
+ (filseq_resolve_tac rls0 9999 i
+ ORELSE
+ (DETERM(filseq_resolve_tac rls1 9999 i) THEN TRY(nextac i))
+ ORELSE
+ (DETERM(filseq_resolve_tac rls2 9999 i) THEN TRY(nextac(i+1))
+ THEN TRY(nextac i)))
in tac end;
@@ -202,11 +202,11 @@
fun UPTOGOAL n tf = let fun tac i = if i<n then all_tac
else tf(i) THEN tac(i-1)
- in STATE(fn state=> tac(nprems_of state)) end;
+ in fn st => tac (nprems_of st) st end;
(* Depth first search bounded by d *)
-fun solven_tac d n = STATE (fn state =>
- if d<0 then no_tac
+fun solven_tac d n state = state |>
+ (if d<0 then no_tac
else if (nprems_of state = 0) then all_tac
else (DETERM(fres_safe_tac n) THEN UPTOGOAL n (solven_tac d)) ORELSE
((fres_unsafe_tac n THEN UPTOGOAL n (solven_tac d)) APPEND
@@ -214,10 +214,10 @@
fun solve_tac d = rewrite_goals_tac rewrite_rls THEN solven_tac d 1;
-fun step_tac n = STATE (fn state =>
- if (nprems_of state = 0) then all_tac
- else (DETERM(fres_safe_tac n)) ORELSE
- (fres_unsafe_tac n APPEND fres_bound_tac n));
+fun step_tac n =
+ COND (has_fewer_prems 1) all_tac
+ (DETERM(fres_safe_tac n) ORELSE
+ (fres_unsafe_tac n APPEND fres_bound_tac n));
end;
end;