Removal of the tactical STATE
authorpaulson
Tue Jul 22 11:12:55 1997 +0200 (1997-07-22 ago)
changeset 353779ac9b475621
parent 3536 8fb4150e2ad3
child 3538 ed9de44032e0
Removal of the tactical STATE
src/CCL/typecheck.ML
src/FOL/simpdata.ML
src/FOLP/hypsubst.ML
src/FOLP/simp.ML
src/HOL/Hoare/Hoare.ML
src/HOL/ex/meson.ML
src/Provers/classical.ML
src/Provers/hypsubst.ML
src/Provers/simp.ML
src/Provers/simplifier.ML
src/Provers/splitter.ML
     1.1 --- a/src/CCL/typecheck.ML	Fri Jul 18 14:06:54 1997 +0200
     1.2 +++ b/src/CCL/typecheck.ML	Tue Jul 22 11:12:55 1997 +0200
     1.3 @@ -83,9 +83,8 @@
     1.4                   could_unify(x,hd (prems_of rcall2T)) orelse
     1.5                   could_unify(x,hd (prems_of rcall3T));
     1.6  
     1.7 -fun IHinst tac rls i = STATE (fn state =>
     1.8 -  let val (_,_,Bi,_) = dest_state(state,i);
     1.9 -      val bvs = bvars Bi [];
    1.10 +fun IHinst tac rls = SUBGOAL (fn (Bi,i) =>
    1.11 +  let val bvs = bvars Bi [];
    1.12        val ihs = filter could_IH (Logic.strip_assums_hyp Bi);
    1.13        val rnames = map (fn x=>
    1.14                      let val (a,b) = get_bno [] 0 x
    1.15 @@ -113,12 +112,8 @@
    1.16                             ematch_tac [SubtypeE] i ORELSE
    1.17                             match_tac [SubtypeI] i;
    1.18  
    1.19 -fun tc_step_tac prems i = STATE(fn state =>
    1.20 -          if (i>length(prems_of state)) 
    1.21 -             then no_tac
    1.22 -             else let val (_,_,c,_) = dest_state(state,i)
    1.23 -                  in if is_rigid_prog c then raw_step_tac prems i else no_tac
    1.24 -                  end);
    1.25 +fun tc_step_tac prems = SUBGOAL (fn (Bi,i) =>
    1.26 +          if is_rigid_prog Bi then raw_step_tac prems i else no_tac);
    1.27  
    1.28  fun typechk_tac rls i = SELECT_GOAL (REPEAT_FIRST (tc_step_tac rls)) i;
    1.29  
     2.1 --- a/src/FOL/simpdata.ML	Fri Jul 18 14:06:54 1997 +0200
     2.2 +++ b/src/FOL/simpdata.ML	Tue Jul 22 11:12:55 1997 +0200
     2.3 @@ -257,18 +257,21 @@
     2.4  
     2.5  (* rot_eq_tac rotates the first equality premise of subgoal i to the front,
     2.6     fails if there is no equaliy or if an equality is already at the front *)
     2.7 -fun rot_eq_tac i = let
     2.8 +local
     2.9    fun is_eq (Const ("Trueprop", _) $ (Const("op ="  ,_) $ _ $ _)) = true
    2.10 -  |   is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
    2.11 -  |   is_eq _ = false;
    2.12 +    | is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
    2.13 +    | is_eq _ = false;
    2.14    fun find_eq n [] = None
    2.15 -  |   find_eq n (t :: ts) = if (is_eq t) then Some n else find_eq (n + 1) ts;
    2.16 -  fun rot_eq state = let val (_, _, Bi, _) = dest_state (state, i) in
    2.17 -	    (case find_eq 0 (Logic.strip_assums_hyp Bi) of
    2.18 -	      None   => no_tac
    2.19 -	    | Some 0 => no_tac
    2.20 -	    | Some n => rotate_tac n i) end;
    2.21 -in STATE rot_eq end;
    2.22 +    | find_eq n (t :: ts) = if (is_eq t) then Some n 
    2.23 +			    else find_eq (n + 1) ts;
    2.24 +in
    2.25 +val rot_eq_tac = 
    2.26 +     SUBGOAL (fn (Bi,i) => 
    2.27 +	      case find_eq 0 (Logic.strip_assums_hyp Bi) of
    2.28 +		  None   => no_tac
    2.29 +		| Some 0 => no_tac
    2.30 +		| Some n => rotate_tac n i)
    2.31 +end;
    2.32  
    2.33  
    2.34  fun safe_asm_more_full_simp_tac ss = TRY o rot_eq_tac THEN' 
     3.1 --- a/src/FOLP/hypsubst.ML	Fri Jul 18 14:06:54 1997 +0200
     3.2 +++ b/src/FOLP/hypsubst.ML	Tue Jul 22 11:12:55 1997 +0200
     3.3 @@ -67,18 +67,18 @@
     3.4  
     3.5  (*Select a suitable equality assumption and substitute throughout the subgoal
     3.6    Replaces only Bound variables if bnd is true*)
     3.7 -fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
     3.8 -      let val (_,_,Bi,_) = dest_state(state,i)
     3.9 -          val n = length(Logic.strip_assums_hyp Bi) - 1
    3.10 +fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
    3.11 +      let val n = length(Logic.strip_assums_hyp Bi) - 1
    3.12            val (k,symopt) = eq_var bnd Bi
    3.13        in 
    3.14 -         EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    3.15 -                etac revcut_rl i,
    3.16 -                REPEAT_DETERM_N (n-k) (etac rev_mp i),
    3.17 -                etac (symopt RS subst) i,
    3.18 -                REPEAT_DETERM_N n (rtac imp_intr i)]
    3.19 +         DETERM
    3.20 +           (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    3.21 +		   etac revcut_rl i,
    3.22 +		   REPEAT_DETERM_N (n-k) (etac rev_mp i),
    3.23 +		   etac (symopt RS subst) i,
    3.24 +		   REPEAT_DETERM_N n (rtac imp_intr i)])
    3.25        end
    3.26 -      handle THM _ => no_tac | EQ_VAR => no_tac));
    3.27 +      handle THM _ => no_tac | EQ_VAR => no_tac);
    3.28  
    3.29  (*Substitutes for Free or Bound variables*)
    3.30  val hyp_subst_tac = gen_hyp_subst_tac false;
     4.1 --- a/src/FOLP/simp.ML	Fri Jul 18 14:06:54 1997 +0200
     4.2 +++ b/src/FOLP/simp.ML	Tue Jul 22 11:12:55 1997 +0200
     4.3 @@ -202,15 +202,15 @@
     4.4      val hvars = foldr it_asms (asms,hvars)
     4.5      val hvs = map (#1 o dest_Var) hvars
     4.6      val refl1_tac = refl_tac 1
     4.7 -    val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops)
     4.8 -              (STATE(fn thm =>
     4.9 -                case head_of(rhs_of_eq 1 thm) of
    4.10 -                  Var(ixn,_) => if ixn mem hvs then refl1_tac
    4.11 -                                else resolve_tac normI_thms 1 ORELSE refl1_tac
    4.12 -                | Const _ => resolve_tac normI_thms 1 ORELSE
    4.13 -                             resolve_tac congs 1 ORELSE refl1_tac
    4.14 -                | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    4.15 -                | _ => refl1_tac))
    4.16 +    fun norm_step_tac st = st |>
    4.17 +	 (case head_of(rhs_of_eq 1 st) of
    4.18 +	    Var(ixn,_) => if ixn mem hvs then refl1_tac
    4.19 +			  else resolve_tac normI_thms 1 ORELSE refl1_tac
    4.20 +	  | Const _ => resolve_tac normI_thms 1 ORELSE
    4.21 +		       resolve_tac congs 1 ORELSE refl1_tac
    4.22 +	  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    4.23 +	  | _ => refl1_tac)
    4.24 +    val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
    4.25      val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
    4.26  in thm'' end;
    4.27  
     5.1 --- a/src/HOL/Hoare/Hoare.ML	Fri Jul 18 14:06:54 1997 +0200
     5.2 +++ b/src/HOL/Hoare/Hoare.ML	Tue Jul 22 11:12:55 1997 +0200
     5.3 @@ -68,9 +68,10 @@
     5.4  (* rename_abs:term (von:string,nach:string,trm:term) benennt in trm alle Lambda-Abstraktionen
     5.5     mit Namen von in nach um *)
     5.6  
     5.7 -fun rename_abs (von,nach,Abs (s,t,trm)) =if von=s
     5.8 -                                                then Abs (nach,t,rename_abs (von,nach,trm))
     5.9 -                                                else Abs (s,t,rename_abs (von,nach,trm))
    5.10 +fun rename_abs (von,nach,Abs (s,t,trm)) =
    5.11 +    if von=s
    5.12 +	then Abs (nach,t,rename_abs (von,nach,trm))
    5.13 +        else Abs (s,t,rename_abs (von,nach,trm))
    5.14    | rename_abs (von,nach,trm1 $ trm2)   =rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2)
    5.15    | rename_abs (_,_,trm)                =trm;
    5.16  
    5.17 @@ -85,41 +86,35 @@
    5.18  
    5.19  fun ren_abs_thm (von,nach,theorem)      =
    5.20          equal_elim
    5.21 -                (
    5.22 -                        reflexive (
    5.23 -                                cterm_of
    5.24 -                                        (#sign (rep_thm theorem))
    5.25 -                                        (rename_abs (von,nach,#prop (rep_thm theorem)))
    5.26 -                        )
    5.27 -                )
    5.28 +                (reflexive (cterm_of (#sign (rep_thm theorem))
    5.29 +			    (rename_abs (von,nach,#prop (rep_thm theorem)))))
    5.30                  theorem;
    5.31  
    5.32  
    5.33 -(**************************************************************************************************)
    5.34 -(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch                         ***)
    5.35 -(***  - Umbenennen von Lambda-Abstraktionen im Theorem                                          ***)
    5.36 -(***  - Instanziieren von freien Variablen im Theorem                                           ***)
    5.37 -(***  - Composing des Subgoals mit dem Theorem                                                  ***)
    5.38 -(**************************************************************************************************)
    5.39 +(****************************************************************************)
    5.40 +(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch   ***)
    5.41 +(***  - Umbenennen von Lambda-Abstraktionen im Theorem                    ***)
    5.42 +(***  - Instanziieren von freien Variablen im Theorem                     ***)
    5.43 +(***  - Composing des Subgoals mit dem Theorem                            ***)
    5.44 +(****************************************************************************)
    5.45  
    5.46  (* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden
    5.47     - insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *)
    5.48  
    5.49  fun comp_inst_ren_tac rens insts theorem i      =
    5.50 -        let
    5.51 -                fun compose_inst_ren_tac [] insts theorem i                     =
    5.52 -                        compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i
    5.53 -                  | compose_inst_ren_tac ((von,nach)::rl) insts theorem i       =
    5.54 -                        compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i
    5.55 -        in
    5.56 -                compose_inst_ren_tac rens insts theorem i
    5.57 -        end;
    5.58 +        let fun compose_inst_ren_tac [] insts theorem i                     =
    5.59 +	      compose_tac (false,
    5.60 +			   cterm_instantiate insts theorem,nprems_of theorem) i
    5.61 +	      | compose_inst_ren_tac ((von,nach)::rl) insts theorem i       =
    5.62 +                        compose_inst_ren_tac rl insts 
    5.63 +			  (ren_abs_thm (von,nach,theorem)) i
    5.64 +        in  compose_inst_ren_tac rens insts theorem i  end;
    5.65  
    5.66  
    5.67 -(**************************************************************************************************)
    5.68 +(***************************************************************    *********)
    5.69  (*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen                               ***)
    5.70  (***    Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1"               ***)
    5.71 -(**************************************************************************************************)
    5.72 +(****************************************************************************)
    5.73  
    5.74  (* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen
    5.75     aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an.
    5.76 @@ -127,97 +122,79 @@
    5.77                wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *)
    5.78  
    5.79  fun pvars_of_term (name,trm)    =
    5.80 -        let
    5.81 -                fun add_vars (name,Free (s,t) $ trm,vl) =if name=s
    5.82 -                                                                then if trm mem vl
    5.83 -                                                                        then vl
    5.84 -                                                                        else trm::vl
    5.85 -                                                                else add_vars (name,trm,vl)
    5.86 -                  | add_vars (name,Abs (s,t,trm),vl)    =add_vars (name,trm,vl)
    5.87 -                  | add_vars (name,trm1 $ trm2,vl)      =add_vars (name,trm2,add_vars (name,trm1,vl))
    5.88 -                  | add_vars (_,_,vl)                   =vl
    5.89 -        in
    5.90 -                add_vars (name,trm,[])
    5.91 -        end;
    5.92 +  let fun add_vars (name,Free (s,t) $ trm,vl) =
    5.93 +            if name=s then if trm mem vl then vl else trm::vl
    5.94 +                      else add_vars (name,trm,vl)
    5.95 +	| add_vars (name,Abs (s,t,trm),vl)    =add_vars (name,trm,vl)
    5.96 +	| add_vars (name,trm1 $ trm2,vl)      =add_vars (name,trm2,add_vars (name,trm1,vl))
    5.97 +	| add_vars (_,_,vl)                   =vl
    5.98 +  in add_vars (name,trm,[]) end;
    5.99 +
   5.100  
   5.101  (* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i
   5.102 -   - v::vl:(term) list  Liste der zu eliminierenden Programmvariablen
   5.103 -   - meta_spec:thm      Theorem, welches zur Entfernung der Variablen benutzt wird
   5.104 -                        z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
   5.105 -   - namexAll:string    Name von    ^                                  (hier "x")
   5.106 -   - varx:term          Term zu                                      ^ (hier Var(("x",0),...))
   5.107 -   - varP:term          Term zu                                  ^     (hier Var(("P",0),...))
   5.108 -   - type_pvar:typ      Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...)
   5.109 + - v::vl:(term) list  Liste der zu eliminierenden Programmvariablen
   5.110 + - meta_spec:thm      Theorem, welches zur Entfernung der Variablen benutzt wird
   5.111 +		      z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
   5.112 + - namexAll:string    Name von    ^                                  (hier "x")
   5.113 + - varx:term          Term zu                                      ^ (hier Var(("x",0),...))
   5.114 + - varP:term          Term zu                                  ^     (hier Var(("P",0),...))
   5.115 + - type_pvar:typ      Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...)
   5.116  
   5.117 -   Vorgehen:
   5.118 -        - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
   5.119 -        - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
   5.120 -          z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
   5.121 -                meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
   5.122 -        - Instanziierungen in meta_spec:
   5.123 -                varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
   5.124 -                varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
   5.125 -                 -      zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
   5.126 -                        trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
   5.127 -                 -      substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
   5.128 -                        trm1 = "s(Suc(0)) = xs ==> xs = 1"
   5.129 -                 -      abstrahiere ueber xs:
   5.130 -                        trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
   5.131 -                 -      abstrahiere ueber restliche Vorkommen von s:
   5.132 -                        trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
   5.133 -                 -      instanziiere varP mit trm3
   5.134 + Vorgehen:
   5.135 +      - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
   5.136 +      - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
   5.137 +	z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
   5.138 +	      meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
   5.139 +      - Instanziierungen in meta_spec:
   5.140 +	      varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
   5.141 +	      varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
   5.142 +	 - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
   5.143 +		trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
   5.144 +	 - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
   5.145 +		trm1 = "s(Suc(0)) = xs ==> xs = 1"
   5.146 +	 - abstrahiere ueber xs:
   5.147 +		trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
   5.148 +	 - abstrahiere ueber restliche Vorkommen von s:
   5.149 +		trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
   5.150 +	 - instanziiere varP mit trm3
   5.151  *)
   5.152  
   5.153 -fun VarsElimTac ([],_,_,_,_,_) i                                        =all_tac
   5.154 -  | VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i        =
   5.155 -        STATE (
   5.156 -                fn state =>
   5.157 -                comp_inst_ren_tac
   5.158 -                        [(namexAll,pvar2pvarID v)]
   5.159 -                        [(
   5.160 -                                cterm_of (#sign (rep_thm state)) varx,
   5.161 -                                cterm_of (#sign (rep_thm state)) (
   5.162 -                                        Abs  ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v)
   5.163 -                                )
   5.164 -                        ),(
   5.165 -                                cterm_of (#sign (rep_thm state)) varP,
   5.166 -                                cterm_of (#sign (rep_thm state)) (
   5.167 -                                        let
   5.168 -                                                val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i);
   5.169 -                                                val (sname,trm0) = variant_abs ("s",dummyT,trm);
   5.170 -                                                val xsname = variant_name ("xs",trm0);
   5.171 -                                                val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0)
   5.172 -                                                val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1))
   5.173 -                                        in
   5.174 -                                                Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2))
   5.175 -                                        end
   5.176 -                                )
   5.177 -                        )]
   5.178 -                        meta_spec i
   5.179 -        )
   5.180 -        THEN
   5.181 -        (VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i);
   5.182 -
   5.183 -(* StateElimTac: Taktik zum Eliminieren aller Programmvariablen aus dem Subgoal i
   5.184 -
   5.185 -   zur Erinnerung:
   5.186 -    -   das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)",
   5.187 -        d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_)
   5.188 -    -   meta_spec hat die Form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
   5.189 +(* StateElimTac: tactic to eliminate all program variable from subgoal i
   5.190 +    - applies to subgoals of the form "!!s:('a) state.P(s)",
   5.191 +        i.e. the term  Const("all",_) $ Abs ("s",pvar --> 'a,_)
   5.192 +    -   meta_spec has the form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
   5.193  *)
   5.194  
   5.195 -fun StateElimTac i      =
   5.196 -        STATE (
   5.197 -                fn state =>
   5.198 -                let
   5.199 -                        val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i);
   5.200 -                        val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $
   5.201 -                                (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec)
   5.202 -                in
   5.203 -                        VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i
   5.204 -                end
   5.205 -        );
   5.206 -
   5.207 +val StateElimTac = SUBGOAL (fn (Bi,i) =>
   5.208 +  let val Const _ $ Abs (_,Type ("fun",[_,type_pvar]),trm) = Bi
   5.209 +      val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $
   5.210 +			    (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = 
   5.211 +			    #prop (rep_thm meta_spec)
   5.212 +      fun vtac v i st = st |>
   5.213 +	  let val cterm = cterm_of (#sign (rep_thm st))
   5.214 +	      val (_,_,_ $ Abs (_,_,trm),_) = dest_state (st,i);
   5.215 +	      val (sname,trm0) = variant_abs ("s",dummyT,trm);
   5.216 +	      val xsname = variant_name ("xs",trm0);
   5.217 +	      val trm1 = subst_term (Free (sname,dummyT) $ v,
   5.218 +				     Syntax.free xsname,trm0)
   5.219 +	      val trm2 = Abs ("xs", type_pvar,
   5.220 +			      abstract_over (Syntax.free xsname,trm1))
   5.221 +	  in
   5.222 +	      comp_inst_ren_tac
   5.223 +		[(namexAll,pvar2pvarID v)]
   5.224 +		[(cterm varx,
   5.225 +		  cterm (Abs  ("s",Type ("nat",[]) --> type_pvar,
   5.226 +			       Bound 0 $ v))),
   5.227 +		 (cterm varP,
   5.228 +		  cterm (Abs ("s", Type ("nat",[]) --> type_pvar,
   5.229 +			      abstract_over (Free (sname,dummyT),trm2))))]
   5.230 +		meta_spec i
   5.231 +	  end
   5.232 +      fun vars_tac [] i      = all_tac
   5.233 +	| vars_tac (v::vl) i = vtac v i THEN vars_tac vl i
   5.234 +  in
   5.235 +      vars_tac (pvars_of_term (variant_abs ("s",dummyT,trm))) i
   5.236 +  end);
   5.237  
   5.238  
   5.239  (*** tactics for verification condition generation ***)
   5.240 @@ -228,25 +205,22 @@
   5.241     Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *)
   5.242  
   5.243  fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false)
   5.244 -and HoareRuleTac i pre_cond =
   5.245 -      STATE(fn state =>
   5.246 -                ((WlpTac i) THEN (HoareRuleTac i pre_cond))
   5.247 -                ORELSE
   5.248 -                (FIRST[rtac SkipRule i,
   5.249 -                       rtac AssignRule i,
   5.250 -                       EVERY[rtac IfRule i,
   5.251 -                             HoareRuleTac (i+2) false,
   5.252 -                             HoareRuleTac (i+1) false],
   5.253 -                       EVERY[rtac WhileRule i,
   5.254 -                             Asm_full_simp_tac (i+2),
   5.255 -                             HoareRuleTac (i+1) true]]
   5.256 -                 THEN
   5.257 -                 (if pre_cond then (Asm_full_simp_tac i) else (atac i))
   5.258 -                )
   5.259 -        );
   5.260 +and HoareRuleTac i pre_cond st = st |>  
   5.261 +	(*abstraction over st prevents looping*)
   5.262 +    ( (WlpTac i THEN HoareRuleTac i pre_cond)
   5.263 +      ORELSE
   5.264 +      (FIRST[rtac SkipRule i,
   5.265 +	     rtac AssignRule i,
   5.266 +	     EVERY[rtac IfRule i,
   5.267 +		   HoareRuleTac (i+2) false,
   5.268 +		   HoareRuleTac (i+1) false],
   5.269 +	     EVERY[rtac WhileRule i,
   5.270 +		   Asm_full_simp_tac (i+2),
   5.271 +		   HoareRuleTac (i+1) true]]
   5.272 +       THEN
   5.273 +       (if pre_cond then (Asm_full_simp_tac i) else (atac i))) );
   5.274  
   5.275 -val HoareTac1 =
   5.276 -  EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac];
   5.277 +val hoare_tac = 
   5.278 +  SELECT_GOAL
   5.279 +    (EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac]);
   5.280  
   5.281 -val hoare_tac = SELECT_GOAL (HoareTac1);
   5.282 -
     6.1 --- a/src/HOL/ex/meson.ML	Fri Jul 18 14:06:54 1997 +0200
     6.2 +++ b/src/HOL/ex/meson.ML	Tue Jul 22 11:12:55 1997 +0200
     6.3 @@ -245,8 +245,8 @@
     6.4    handle THM _ => (*disjunction?*)
     6.5      let val tac = 
     6.6          (METAHYPS (resop (cnf_nil seen)) 1) THEN
     6.7 -        (STATE (fn st' => 
     6.8 -                METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1))
     6.9 +        (fn st' => st' |>
    6.10 +                METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)
    6.11      in  Sequence.list_of_s (tac (th RS disj_forward)) @ ths  end
    6.12  and cnf_nil seen th = cnf_aux seen (th,[]);
    6.13  
     7.1 --- a/src/Provers/classical.ML	Fri Jul 18 14:06:54 1997 +0200
     7.2 +++ b/src/Provers/classical.ML	Tue Jul 22 11:12:55 1997 +0200
     7.3 @@ -595,7 +595,7 @@
     7.4    biresolve_from_nets_tac dup_netpair;
     7.5  
     7.6  (*Searching to depth m.*)
     7.7 -fun depth_tac cs m i = STATE(fn state => 
     7.8 +fun depth_tac cs m i state = 
     7.9    SELECT_GOAL 
    7.10     (getWrapper cs
    7.11      (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
    7.12 @@ -605,7 +605,7 @@
    7.13        COND (K(m=0)) no_tac
    7.14          ((instp_step_tac cs i APPEND dup_step_tac cs i)
    7.15  	 THEN DEPTH_SOLVE (depth_tac cs (m-1) i)))) 1)
    7.16 -  i);
    7.17 +  i state;
    7.18  
    7.19  (*Search, with depth bound m.  
    7.20    This is the "entry point", which does safe inferences first.*)
     8.1 --- a/src/Provers/hypsubst.ML	Fri Jul 18 14:06:54 1997 +0200
     8.2 +++ b/src/Provers/hypsubst.ML	Tue Jul 22 11:12:55 1997 +0200
     8.3 @@ -116,12 +116,11 @@
     8.4    since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality
     8.5    must NOT be deleted.  Tactic must rotate or delete m assumptions.
     8.6  *)
     8.7 -fun thin_leading_eqs_tac bnd m i = STATE(fn state =>
     8.8 +fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) =>
     8.9      let fun count []      = 0
    8.10  	  | count (A::Bs) = ((inspect_pair bnd true (dest_eq A);  
    8.11  			      1 + count Bs)
    8.12                               handle Match => 0)
    8.13 -	val (_,_,Bi,_) = dest_state(state,i)
    8.14          val j = Int.min(m, count (Logic.strip_assums_hyp Bi))
    8.15      in  REPEAT_DETERM_N j (etac thin_rl i)  THEN  rotate_tac (m-j) i
    8.16      end);
    8.17 @@ -141,17 +140,16 @@
    8.18  
    8.19    (*Select a suitable equality assumption and substitute throughout the subgoal
    8.20      Replaces only Bound variables if bnd is true*)
    8.21 -  fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
    8.22 -	let val (_,_,Bi,_) = dest_state(state,i)
    8.23 -	    val n = length(Logic.strip_assums_hyp Bi) - 1
    8.24 +  fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
    8.25 +	let val n = length(Logic.strip_assums_hyp Bi) - 1
    8.26  	    val (k,_) = eq_var bnd true Bi
    8.27  	in 
    8.28 -	   EVERY [rotate_tac k i,
    8.29 -		  asm_full_simp_tac hyp_subst_ss i,
    8.30 -		  etac thin_rl i,
    8.31 -		  thin_leading_eqs_tac bnd (n-k) i]
    8.32 +	   DETERM (EVERY [rotate_tac k i,
    8.33 +			  asm_full_simp_tac hyp_subst_ss i,
    8.34 +			  etac thin_rl i,
    8.35 +			  thin_leading_eqs_tac bnd (n-k) i])
    8.36  	end
    8.37 -	handle THM _ => no_tac | EQ_VAR => no_tac));
    8.38 +	handle THM _ => no_tac | EQ_VAR => no_tac);
    8.39  
    8.40  end;
    8.41  
    8.42 @@ -159,18 +157,18 @@
    8.43  
    8.44  (*Old version of the tactic above -- slower but the only way
    8.45    to handle equalities containing Vars.*)
    8.46 -fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state =>
    8.47 -      let val (_,_,Bi,_) = dest_state(state,i)
    8.48 -	  val n = length(Logic.strip_assums_hyp Bi) - 1
    8.49 +fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
    8.50 +      let val n = length(Logic.strip_assums_hyp Bi) - 1
    8.51  	  val (k,symopt) = eq_var bnd false Bi
    8.52        in 
    8.53 -	 EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    8.54 -		etac revcut_rl i,
    8.55 -		REPEAT_DETERM_N (n-k) (etac rev_mp i),
    8.56 -		etac (if symopt then ssubst else subst) i,
    8.57 -		REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]
    8.58 +	 DETERM
    8.59 +           (EVERY [REPEAT_DETERM_N k (etac rev_mp i),
    8.60 +		   etac revcut_rl i,
    8.61 +		   REPEAT_DETERM_N (n-k) (etac rev_mp i),
    8.62 +		   etac (if symopt then ssubst else subst) i,
    8.63 +		   REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)])
    8.64        end
    8.65 -      handle THM _ => no_tac | EQ_VAR => no_tac));
    8.66 +      handle THM _ => no_tac | EQ_VAR => no_tac);
    8.67  
    8.68  (*Substitutes for Free or Bound variables*)
    8.69  val hyp_subst_tac = 
     9.1 --- a/src/Provers/simp.ML	Fri Jul 18 14:06:54 1997 +0200
     9.2 +++ b/src/Provers/simp.ML	Tue Jul 22 11:12:55 1997 +0200
     9.3 @@ -196,15 +196,15 @@
     9.4      val hvars = foldr it_asms (asms,hvars)
     9.5      val hvs = map (#1 o dest_Var) hvars
     9.6      val refl1_tac = refl_tac 1
     9.7 -    val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops)
     9.8 -	      (STATE(fn thm =>
     9.9 -		case head_of(rhs_of_eq 1 thm) of
    9.10 -		  Var(ixn,_) => if ixn mem hvs then refl1_tac
    9.11 -				else resolve_tac normI_thms 1 ORELSE refl1_tac
    9.12 -		| Const _ => resolve_tac normI_thms 1 ORELSE
    9.13 -			     resolve_tac congs 1 ORELSE refl1_tac
    9.14 -		| Free _ => resolve_tac congs 1 ORELSE refl1_tac
    9.15 -		| _ => refl1_tac))
    9.16 +    fun norm_step_tac st = st |>
    9.17 +	 (case head_of(rhs_of_eq 1 st) of
    9.18 +	    Var(ixn,_) => if ixn mem hvs then refl1_tac
    9.19 +			  else resolve_tac normI_thms 1 ORELSE refl1_tac
    9.20 +	  | Const _ => resolve_tac normI_thms 1 ORELSE
    9.21 +		       resolve_tac congs 1 ORELSE refl1_tac
    9.22 +	  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    9.23 +	  | _ => refl1_tac))
    9.24 +    val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
    9.25      val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
    9.26  in thm'' end;
    9.27  
    10.1 --- a/src/Provers/simplifier.ML	Fri Jul 18 14:06:54 1997 +0200
    10.2 +++ b/src/Provers/simplifier.ML	Tue Jul 22 11:12:55 1997 +0200
    10.3 @@ -272,9 +272,8 @@
    10.4  
    10.5  (** simplification tactics **)
    10.6  
    10.7 -fun NEWSUBGOALS tac tacf =
    10.8 -  STATE (fn state0 =>
    10.9 -    tac THEN STATE (fn state1 => tacf (nprems_of state1 - nprems_of state0)));
   10.10 +fun NEWSUBGOALS tac tacf st0 = st0 |>
   10.11 +    (tac THEN (fn st1 => tacf (nprems_of st1 - nprems_of st0) st1));
   10.12  
   10.13  (*not totally safe: may instantiate unknowns that appear also in other subgoals*)
   10.14  fun basic_gen_simp_tac mode =
    11.1 --- a/src/Provers/splitter.ML	Fri Jul 18 14:06:54 1997 +0200
    11.2 +++ b/src/Provers/splitter.ML	Tue Jul 22 11:12:55 1997 +0200
    11.3 @@ -261,21 +261,21 @@
    11.4                             val (Const(a,_),args) = strip_comb lhs
    11.5                         in (a,(thm,fastype_of t,length args)) end
    11.6        val cmap = map const splits;
    11.7 -      fun lift Ts t p state = rtac (inst_lift Ts t p state trlift i) i
    11.8 -      fun lift_split state =
    11.9 -            let val (Ts,t,splits) = select cmap state i
   11.10 +      fun lift_tac Ts t p st = (rtac (inst_lift Ts t p st trlift i) i) st
   11.11 +      fun lift_split_tac st = st |>
   11.12 +            let val (Ts,t,splits) = select cmap st i
   11.13              in case splits of
   11.14                   [] => no_tac
   11.15                 | (thm,apsns,pos,TB,tt)::_ =>
   11.16                     (case apsns of
   11.17 -                      [] => STATE(fn state => rtac (inst_split Ts t tt thm TB state) i)
   11.18 -                    | p::_ => EVERY[STATE(lift Ts t p),
   11.19 +                      [] => (fn state => state |>
   11.20 +			           rtac (inst_split Ts t tt thm TB state) i)
   11.21 +                    | p::_ => EVERY[lift_tac Ts t p,
   11.22                                      rtac reflexive_thm (i+1),
   11.23 -                                    STATE lift_split])
   11.24 +                                    lift_split_tac])
   11.25              end
   11.26 -  in STATE(fn thm =>
   11.27 -       if i <= nprems_of thm then rtac iffD i THEN STATE lift_split
   11.28 -       else no_tac)
   11.29 +  in COND (has_fewer_prems i) no_tac 
   11.30 +          (rtac iffD i THEN lift_split_tac)
   11.31    end;
   11.32  
   11.33  in split_tac end;