# HG changeset patch # User paulson # Date 869562858 -7200 # Node ID ed9de44032e0427a2192fdc2ee55954d5b19c55f # Parent 79ac9b4756216a5f4f5c030546c7e05b5b0c4c61 Removal of the tactical STATE diff -r 79ac9b475621 -r ed9de44032e0 src/HOL/datatype.ML --- 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"), diff -r 79ac9b475621 -r ed9de44032e0 src/HOL/simpdata.ML --- 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 diff -r 79ac9b475621 -r ed9de44032e0 src/HOL/thy_data.ML --- 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; diff -r 79ac9b475621 -r ed9de44032e0 src/Pure/search.ML --- 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 ***) diff -r 79ac9b475621 -r ed9de44032e0 src/Pure/tactic.ML --- 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 diff -r 79ac9b475621 -r ed9de44032e0 src/Sequents/prover.ML --- 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 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;