# HG changeset patch # User paulson # Date 869562775 -7200 # Node ID 79ac9b4756216a5f4f5c030546c7e05b5b0c4c61 # Parent 8fb4150e2ad35e31f557334dd0ac707fd3a0bf9d Removal of the tactical STATE diff -r 8fb4150e2ad3 -r 79ac9b475621 src/CCL/typecheck.ML --- a/src/CCL/typecheck.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/CCL/typecheck.ML Tue Jul 22 11:12:55 1997 +0200 @@ -83,9 +83,8 @@ could_unify(x,hd (prems_of rcall2T)) orelse could_unify(x,hd (prems_of rcall3T)); -fun IHinst tac rls i = STATE (fn state => - let val (_,_,Bi,_) = dest_state(state,i); - val bvs = bvars Bi []; +fun IHinst tac rls = SUBGOAL (fn (Bi,i) => + let val bvs = bvars Bi []; val ihs = filter could_IH (Logic.strip_assums_hyp Bi); val rnames = map (fn x=> let val (a,b) = get_bno [] 0 x @@ -113,12 +112,8 @@ ematch_tac [SubtypeE] i ORELSE match_tac [SubtypeI] i; -fun tc_step_tac prems i = STATE(fn state => - if (i>length(prems_of state)) - then no_tac - else let val (_,_,c,_) = dest_state(state,i) - in if is_rigid_prog c then raw_step_tac prems i else no_tac - end); +fun tc_step_tac prems = SUBGOAL (fn (Bi,i) => + if is_rigid_prog Bi then raw_step_tac prems i else no_tac); fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i; diff -r 8fb4150e2ad3 -r 79ac9b475621 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/FOL/simpdata.ML Tue Jul 22 11:12:55 1997 +0200 @@ -257,18 +257,21 @@ (* 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 +local fun is_eq (Const ("Trueprop", _) $ (Const("op =" ,_) $ _ $ _)) = true - | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true - | is_eq _ = false; + | 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 - None => no_tac - | Some 0 => no_tac - | Some n => rotate_tac n i) end; -in STATE rot_eq end; + | 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; fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' diff -r 8fb4150e2ad3 -r 79ac9b475621 src/FOLP/hypsubst.ML --- a/src/FOLP/hypsubst.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/FOLP/hypsubst.ML Tue Jul 22 11:12:55 1997 +0200 @@ -67,18 +67,18 @@ (*Select a suitable equality assumption and substitute throughout the subgoal Replaces only Bound variables if bnd is true*) -fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => - let val (_,_,Bi,_) = dest_state(state,i) - val n = length(Logic.strip_assums_hyp Bi) - 1 +fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => + let val n = length(Logic.strip_assums_hyp Bi) - 1 val (k,symopt) = eq_var bnd Bi in - EVERY [REPEAT_DETERM_N k (etac rev_mp i), - etac revcut_rl i, - REPEAT_DETERM_N (n-k) (etac rev_mp i), - etac (symopt RS subst) i, - REPEAT_DETERM_N n (rtac imp_intr i)] + DETERM + (EVERY [REPEAT_DETERM_N k (etac rev_mp i), + etac revcut_rl i, + REPEAT_DETERM_N (n-k) (etac rev_mp i), + etac (symopt RS subst) i, + REPEAT_DETERM_N n (rtac imp_intr i)]) end - handle THM _ => no_tac | EQ_VAR => no_tac)); + handle THM _ => no_tac | EQ_VAR => no_tac); (*Substitutes for Free or Bound variables*) val hyp_subst_tac = gen_hyp_subst_tac false; diff -r 8fb4150e2ad3 -r 79ac9b475621 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/FOLP/simp.ML Tue Jul 22 11:12:55 1997 +0200 @@ -202,15 +202,15 @@ val hvars = foldr it_asms (asms,hvars) val hvs = map (#1 o dest_Var) hvars val refl1_tac = refl_tac 1 - val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) - (STATE(fn thm => - case head_of(rhs_of_eq 1 thm) of - Var(ixn,_) => if ixn mem hvs then refl1_tac - else resolve_tac normI_thms 1 ORELSE refl1_tac - | Const _ => resolve_tac normI_thms 1 ORELSE - resolve_tac congs 1 ORELSE refl1_tac - | Free _ => resolve_tac congs 1 ORELSE refl1_tac - | _ => refl1_tac)) + fun norm_step_tac st = st |> + (case head_of(rhs_of_eq 1 st) of + Var(ixn,_) => if ixn mem hvs then refl1_tac + else resolve_tac normI_thms 1 ORELSE refl1_tac + | Const _ => resolve_tac normI_thms 1 ORELSE + resolve_tac congs 1 ORELSE refl1_tac + | Free _ => resolve_tac congs 1 ORELSE refl1_tac + | _ => refl1_tac) + val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac val Some(thm'',_) = Sequence.pull(add_norm_tac thm') in thm'' end; diff -r 8fb4150e2ad3 -r 79ac9b475621 src/HOL/Hoare/Hoare.ML --- a/src/HOL/Hoare/Hoare.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/HOL/Hoare/Hoare.ML Tue Jul 22 11:12:55 1997 +0200 @@ -68,9 +68,10 @@ (* rename_abs:term (von:string,nach:string,trm:term) benennt in trm alle Lambda-Abstraktionen mit Namen von in nach um *) -fun rename_abs (von,nach,Abs (s,t,trm)) =if von=s - then Abs (nach,t,rename_abs (von,nach,trm)) - else Abs (s,t,rename_abs (von,nach,trm)) +fun rename_abs (von,nach,Abs (s,t,trm)) = + if von=s + then Abs (nach,t,rename_abs (von,nach,trm)) + else Abs (s,t,rename_abs (von,nach,trm)) | rename_abs (von,nach,trm1 $ trm2) =rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2) | rename_abs (_,_,trm) =trm; @@ -85,41 +86,35 @@ fun ren_abs_thm (von,nach,theorem) = equal_elim - ( - reflexive ( - cterm_of - (#sign (rep_thm theorem)) - (rename_abs (von,nach,#prop (rep_thm theorem))) - ) - ) + (reflexive (cterm_of (#sign (rep_thm theorem)) + (rename_abs (von,nach,#prop (rep_thm theorem))))) theorem; -(**************************************************************************************************) -(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch ***) -(*** - Umbenennen von Lambda-Abstraktionen im Theorem ***) -(*** - Instanziieren von freien Variablen im Theorem ***) -(*** - Composing des Subgoals mit dem Theorem ***) -(**************************************************************************************************) +(****************************************************************************) +(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch ***) +(*** - Umbenennen von Lambda-Abstraktionen im Theorem ***) +(*** - Instanziieren von freien Variablen im Theorem ***) +(*** - Composing des Subgoals mit dem Theorem ***) +(****************************************************************************) (* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden - insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *) fun comp_inst_ren_tac rens insts theorem i = - let - fun compose_inst_ren_tac [] insts theorem i = - compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i - | compose_inst_ren_tac ((von,nach)::rl) insts theorem i = - compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i - in - compose_inst_ren_tac rens insts theorem i - end; + let fun compose_inst_ren_tac [] insts theorem i = + compose_tac (false, + cterm_instantiate insts theorem,nprems_of theorem) i + | compose_inst_ren_tac ((von,nach)::rl) insts theorem i = + compose_inst_ren_tac rl insts + (ren_abs_thm (von,nach,theorem)) i + in compose_inst_ren_tac rens insts theorem i end; -(**************************************************************************************************) +(*************************************************************** *********) (*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen ***) (*** Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1" ***) -(**************************************************************************************************) +(****************************************************************************) (* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an. @@ -127,97 +122,79 @@ wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *) fun pvars_of_term (name,trm) = - let - fun add_vars (name,Free (s,t) $ trm,vl) =if name=s - then if trm mem vl - then vl - else trm::vl - else add_vars (name,trm,vl) - | add_vars (name,Abs (s,t,trm),vl) =add_vars (name,trm,vl) - | add_vars (name,trm1 $ trm2,vl) =add_vars (name,trm2,add_vars (name,trm1,vl)) - | add_vars (_,_,vl) =vl - in - add_vars (name,trm,[]) - end; + let fun add_vars (name,Free (s,t) $ trm,vl) = + if name=s then if trm mem vl then vl else trm::vl + else add_vars (name,trm,vl) + | add_vars (name,Abs (s,t,trm),vl) =add_vars (name,trm,vl) + | add_vars (name,trm1 $ trm2,vl) =add_vars (name,trm2,add_vars (name,trm1,vl)) + | add_vars (_,_,vl) =vl + in add_vars (name,trm,[]) end; + (* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i - - v::vl:(term) list Liste der zu eliminierenden Programmvariablen - - meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird - z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" - - namexAll:string Name von ^ (hier "x") - - varx:term Term zu ^ (hier Var(("x",0),...)) - - varP:term Term zu ^ (hier Var(("P",0),...)) - - type_pvar:typ Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...) + - v::vl:(term) list Liste der zu eliminierenden Programmvariablen + - meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird + z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" + - namexAll:string Name von ^ (hier "x") + - varx:term Term zu ^ (hier Var(("x",0),...)) + - varP:term Term zu ^ (hier Var(("P",0),...)) + - type_pvar:typ Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...) - Vorgehen: - - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu: - - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt - z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich - meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))" - - Instanziierungen in meta_spec: - varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert - varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a": - - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.": - trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable) - - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs: - trm1 = "s(Suc(0)) = xs ==> xs = 1" - - abstrahiere ueber xs: - trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1" - - abstrahiere ueber restliche Vorkommen von s: - trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1" - - instanziiere varP mit trm3 + Vorgehen: + - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu: + - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt + z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich + meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))" + - Instanziierungen in meta_spec: + varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert + varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a": + - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.": + trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable) + - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs: + trm1 = "s(Suc(0)) = xs ==> xs = 1" + - abstrahiere ueber xs: + trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1" + - abstrahiere ueber restliche Vorkommen von s: + trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1" + - instanziiere varP mit trm3 *) -fun VarsElimTac ([],_,_,_,_,_) i =all_tac - | VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i = - STATE ( - fn state => - comp_inst_ren_tac - [(namexAll,pvar2pvarID v)] - [( - cterm_of (#sign (rep_thm state)) varx, - cterm_of (#sign (rep_thm state)) ( - Abs ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v) - ) - ),( - cterm_of (#sign (rep_thm state)) varP, - cterm_of (#sign (rep_thm state)) ( - let - val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i); - val (sname,trm0) = variant_abs ("s",dummyT,trm); - val xsname = variant_name ("xs",trm0); - val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0) - val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1)) - in - Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2)) - end - ) - )] - meta_spec i - ) - THEN - (VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i); - -(* StateElimTac: Taktik zum Eliminieren aller Programmvariablen aus dem Subgoal i - - zur Erinnerung: - - das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)", - d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_) - - meta_spec hat die Form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" +(* StateElimTac: tactic to eliminate all program variable from subgoal i + - applies to subgoals of the form "!!s:('a) state.P(s)", + i.e. the term Const("all",_) $ Abs ("s",pvar --> 'a,_) + - meta_spec has the form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" *) -fun StateElimTac i = - STATE ( - fn state => - let - val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i); - val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $ - (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec) - in - VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i - end - ); - +val StateElimTac = SUBGOAL (fn (Bi,i) => + let val Const _ $ Abs (_,Type ("fun",[_,type_pvar]),trm) = Bi + val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $ + (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = + #prop (rep_thm meta_spec) + fun vtac v i st = st |> + let val cterm = cterm_of (#sign (rep_thm st)) + val (_,_,_ $ Abs (_,_,trm),_) = dest_state (st,i); + val (sname,trm0) = variant_abs ("s",dummyT,trm); + val xsname = variant_name ("xs",trm0); + val trm1 = subst_term (Free (sname,dummyT) $ v, + Syntax.free xsname,trm0) + val trm2 = Abs ("xs", type_pvar, + abstract_over (Syntax.free xsname,trm1)) + in + comp_inst_ren_tac + [(namexAll,pvar2pvarID v)] + [(cterm varx, + cterm (Abs ("s",Type ("nat",[]) --> type_pvar, + Bound 0 $ v))), + (cterm varP, + cterm (Abs ("s", Type ("nat",[]) --> type_pvar, + abstract_over (Free (sname,dummyT),trm2))))] + meta_spec i + end + fun vars_tac [] i = all_tac + | vars_tac (v::vl) i = vtac v i THEN vars_tac vl i + in + vars_tac (pvars_of_term (variant_abs ("s",dummyT,trm))) i + end); (*** tactics for verification condition generation ***) @@ -228,25 +205,22 @@ Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *) fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false) -and HoareRuleTac i pre_cond = - STATE(fn state => - ((WlpTac i) THEN (HoareRuleTac i pre_cond)) - ORELSE - (FIRST[rtac SkipRule i, - rtac AssignRule i, - EVERY[rtac IfRule i, - HoareRuleTac (i+2) false, - HoareRuleTac (i+1) false], - EVERY[rtac WhileRule i, - Asm_full_simp_tac (i+2), - HoareRuleTac (i+1) true]] - THEN - (if pre_cond then (Asm_full_simp_tac i) else (atac i)) - ) - ); +and HoareRuleTac i pre_cond st = st |> + (*abstraction over st prevents looping*) + ( (WlpTac i THEN HoareRuleTac i pre_cond) + ORELSE + (FIRST[rtac SkipRule i, + rtac AssignRule i, + EVERY[rtac IfRule i, + HoareRuleTac (i+2) false, + HoareRuleTac (i+1) false], + EVERY[rtac WhileRule i, + Asm_full_simp_tac (i+2), + HoareRuleTac (i+1) true]] + THEN + (if pre_cond then (Asm_full_simp_tac i) else (atac i))) ); -val HoareTac1 = - EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac]; +val hoare_tac = + SELECT_GOAL + (EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac]); -val hoare_tac = SELECT_GOAL (HoareTac1); - diff -r 8fb4150e2ad3 -r 79ac9b475621 src/HOL/ex/meson.ML --- a/src/HOL/ex/meson.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/HOL/ex/meson.ML Tue Jul 22 11:12:55 1997 +0200 @@ -245,8 +245,8 @@ handle THM _ => (*disjunction?*) let val tac = (METAHYPS (resop (cnf_nil seen)) 1) THEN - (STATE (fn st' => - METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)) + (fn st' => st' |> + METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1) in Sequence.list_of_s (tac (th RS disj_forward)) @ ths end and cnf_nil seen th = cnf_aux seen (th,[]); diff -r 8fb4150e2ad3 -r 79ac9b475621 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/Provers/classical.ML Tue Jul 22 11:12:55 1997 +0200 @@ -595,7 +595,7 @@ biresolve_from_nets_tac dup_netpair; (*Searching to depth m.*) -fun depth_tac cs m i = STATE(fn state => +fun depth_tac cs m i state = SELECT_GOAL (getWrapper cs (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac @@ -605,7 +605,7 @@ COND (K(m=0)) no_tac ((instp_step_tac cs i APPEND dup_step_tac cs i) THEN DEPTH_SOLVE (depth_tac cs (m-1) i)))) 1) - i); + i state; (*Search, with depth bound m. This is the "entry point", which does safe inferences first.*) diff -r 8fb4150e2ad3 -r 79ac9b475621 src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/Provers/hypsubst.ML Tue Jul 22 11:12:55 1997 +0200 @@ -116,12 +116,11 @@ since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality must NOT be deleted. Tactic must rotate or delete m assumptions. *) -fun thin_leading_eqs_tac bnd m i = STATE(fn state => +fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) => let fun count [] = 0 | count (A::Bs) = ((inspect_pair bnd true (dest_eq A); 1 + count Bs) handle Match => 0) - val (_,_,Bi,_) = dest_state(state,i) val j = Int.min(m, count (Logic.strip_assums_hyp Bi)) in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (m-j) i end); @@ -141,17 +140,16 @@ (*Select a suitable equality assumption and substitute throughout the subgoal Replaces only Bound variables if bnd is true*) - fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => - let val (_,_,Bi,_) = dest_state(state,i) - val n = length(Logic.strip_assums_hyp Bi) - 1 + fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => + let val n = length(Logic.strip_assums_hyp Bi) - 1 val (k,_) = eq_var bnd true Bi in - EVERY [rotate_tac k i, - asm_full_simp_tac hyp_subst_ss i, - etac thin_rl i, - thin_leading_eqs_tac bnd (n-k) i] + DETERM (EVERY [rotate_tac k i, + asm_full_simp_tac hyp_subst_ss i, + etac thin_rl i, + thin_leading_eqs_tac bnd (n-k) i]) end - handle THM _ => no_tac | EQ_VAR => no_tac)); + handle THM _ => no_tac | EQ_VAR => no_tac); end; @@ -159,18 +157,18 @@ (*Old version of the tactic above -- slower but the only way to handle equalities containing Vars.*) -fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => - let val (_,_,Bi,_) = dest_state(state,i) - val n = length(Logic.strip_assums_hyp Bi) - 1 +fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => + let val n = length(Logic.strip_assums_hyp Bi) - 1 val (k,symopt) = eq_var bnd false Bi in - EVERY [REPEAT_DETERM_N k (etac rev_mp i), - etac revcut_rl i, - REPEAT_DETERM_N (n-k) (etac rev_mp i), - etac (if symopt then ssubst else subst) i, - REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)] + DETERM + (EVERY [REPEAT_DETERM_N k (etac rev_mp i), + etac revcut_rl i, + REPEAT_DETERM_N (n-k) (etac rev_mp i), + etac (if symopt then ssubst else subst) i, + REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]) end - handle THM _ => no_tac | EQ_VAR => no_tac)); + handle THM _ => no_tac | EQ_VAR => no_tac); (*Substitutes for Free or Bound variables*) val hyp_subst_tac = diff -r 8fb4150e2ad3 -r 79ac9b475621 src/Provers/simp.ML --- a/src/Provers/simp.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/Provers/simp.ML Tue Jul 22 11:12:55 1997 +0200 @@ -196,15 +196,15 @@ val hvars = foldr it_asms (asms,hvars) val hvs = map (#1 o dest_Var) hvars val refl1_tac = refl_tac 1 - val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) - (STATE(fn thm => - case head_of(rhs_of_eq 1 thm) of - Var(ixn,_) => if ixn mem hvs then refl1_tac - else resolve_tac normI_thms 1 ORELSE refl1_tac - | Const _ => resolve_tac normI_thms 1 ORELSE - resolve_tac congs 1 ORELSE refl1_tac - | Free _ => resolve_tac congs 1 ORELSE refl1_tac - | _ => refl1_tac)) + fun norm_step_tac st = st |> + (case head_of(rhs_of_eq 1 st) of + Var(ixn,_) => if ixn mem hvs then refl1_tac + else resolve_tac normI_thms 1 ORELSE refl1_tac + | Const _ => resolve_tac normI_thms 1 ORELSE + resolve_tac congs 1 ORELSE refl1_tac + | Free _ => resolve_tac congs 1 ORELSE refl1_tac + | _ => refl1_tac)) + val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac val Some(thm'',_) = Sequence.pull(add_norm_tac thm') in thm'' end; diff -r 8fb4150e2ad3 -r 79ac9b475621 src/Provers/simplifier.ML --- a/src/Provers/simplifier.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/Provers/simplifier.ML Tue Jul 22 11:12:55 1997 +0200 @@ -272,9 +272,8 @@ (** simplification tactics **) -fun NEWSUBGOALS tac tacf = - STATE (fn state0 => - tac THEN STATE (fn state1 => tacf (nprems_of state1 - nprems_of state0))); +fun NEWSUBGOALS tac tacf st0 = st0 |> + (tac THEN (fn st1 => tacf (nprems_of st1 - nprems_of st0) st1)); (*not totally safe: may instantiate unknowns that appear also in other subgoals*) fun basic_gen_simp_tac mode = diff -r 8fb4150e2ad3 -r 79ac9b475621 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/Provers/splitter.ML Tue Jul 22 11:12:55 1997 +0200 @@ -261,21 +261,21 @@ val (Const(a,_),args) = strip_comb lhs in (a,(thm,fastype_of t,length args)) end val cmap = map const splits; - fun lift Ts t p state = rtac (inst_lift Ts t p state trlift i) i - fun lift_split state = - let val (Ts,t,splits) = select cmap state i + fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st + fun lift_split_tac st = st |> + let val (Ts,t,splits) = select cmap st i in case splits of [] => no_tac | (thm,apsns,pos,TB,tt)::_ => (case apsns of - [] => STATE(fn state => rtac (inst_split Ts t tt thm TB state) i) - | p::_ => EVERY[STATE(lift Ts t p), + [] => (fn state => state |> + rtac (inst_split Ts t tt thm TB state) i) + | p::_ => EVERY[lift_tac Ts t p, rtac reflexive_thm (i+1), - STATE lift_split]) + lift_split_tac]) end - in STATE(fn thm => - if i <= nprems_of thm then rtac iffD i THEN STATE lift_split - else no_tac) + in COND (has_fewer_prems i) no_tac + (rtac iffD i THEN lift_split_tac) end; in split_tac end;