src/FOLP/simp.ML
changeset 1512 ce37c64244c0
parent 1459 d12da312eff4
child 2266 82aef6857c5b
     1.1 --- a/src/FOLP/simp.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/FOLP/simp.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -135,7 +135,7 @@
     1.4  in mk trans_thms end;
     1.5  
     1.6  (*Applies tactic and returns the first resulting state, FAILS if none!*)
     1.7 -fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of
     1.8 +fun one_result(tac,thm) = case Sequence.pull(tac thm) of
     1.9          Some(thm',_) => thm'
    1.10        | None => raise THM("Simplifier: could not continue", 0, [thm]);
    1.11  
    1.12 @@ -211,7 +211,7 @@
    1.13                               resolve_tac congs 1 ORELSE refl1_tac
    1.14                  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    1.15                  | _ => refl1_tac))
    1.16 -    val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm'))
    1.17 +    val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
    1.18  in thm'' end;
    1.19  
    1.20  fun add_norm_tags congs =
    1.21 @@ -336,19 +336,19 @@
    1.22      in find_if(tm,0) end;
    1.23  
    1.24  fun IF1_TAC cong_tac i =
    1.25 -    let fun seq_try (ifth::ifths,ifc::ifcs) thm = tapply(
    1.26 -                COND (if_rewritable ifc i) (DETERM(rtac ifth i))
    1.27 -                        (Tactic(seq_try(ifths,ifcs))), thm)
    1.28 -              | seq_try([],_) thm = tapply(no_tac,thm)
    1.29 -        and try_rew thm = tapply(Tactic(seq_try(case_rews,case_consts))
    1.30 -                                 ORELSE Tactic one_subt, thm)
    1.31 +    let fun seq_try (ifth::ifths,ifc::ifcs) thm = 
    1.32 +                (COND (if_rewritable ifc i) (DETERM(rtac ifth i))
    1.33 +                        (seq_try(ifths,ifcs))) thm
    1.34 +              | seq_try([],_) thm = no_tac thm
    1.35 +        and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm
    1.36          and one_subt thm =
    1.37                  let val test = has_fewer_prems (nprems_of thm + 1)
    1.38 -                    fun loop thm = tapply(COND test no_tac
    1.39 -                        ((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
    1.40 -                         ORELSE (refl_tac i THEN Tactic loop)), thm)
    1.41 -                in tapply(cong_tac THEN Tactic loop, thm) end
    1.42 -    in COND (may_match(case_consts,i)) (Tactic try_rew) no_tac end;
    1.43 +                    fun loop thm = 
    1.44 +			COND test no_tac
    1.45 +                          ((try_rew THEN DEPTH_FIRST test (refl_tac i))
    1.46 +			   ORELSE (refl_tac i THEN loop)) thm
    1.47 +                in (cong_tac THEN loop) thm end
    1.48 +    in COND (may_match(case_consts,i)) try_rew no_tac end;
    1.49  
    1.50  fun CASE_TAC (SS{cong_net,...}) i =
    1.51  let val cong_tac = net_tac cong_net i
    1.52 @@ -422,7 +422,7 @@
    1.53  fun simp_lhs(thm,ss,anet,ats,cs) =
    1.54      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
    1.55      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
    1.56 -    else case Sequence.pull(tapply(cong_tac i,thm)) of
    1.57 +    else case Sequence.pull(cong_tac i thm) of
    1.58              Some(thm',_) =>
    1.59                      let val ps = prems_of thm and ps' = prems_of thm';
    1.60                          val n = length(ps')-length(ps);
    1.61 @@ -455,12 +455,12 @@
    1.62                       thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
    1.63              end
    1.64      | None => if more
    1.65 -            then rew(tapply(lhs_net_tac anet i THEN assume_tac i,thm),
    1.66 +            then rew((lhs_net_tac anet i THEN assume_tac i) thm,
    1.67                       thm,ss,anet,ats,cs,false)
    1.68              else (ss,thm,anet,ats,cs);
    1.69  
    1.70  fun try_true(thm,ss,anet,ats,cs) =
    1.71 -    case Sequence.pull(tapply(auto_tac i,thm)) of
    1.72 +    case Sequence.pull(auto_tac i thm) of
    1.73        Some(thm',_) => (ss,thm',anet,ats,cs)
    1.74      | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
    1.75                in if !tracing
    1.76 @@ -471,7 +471,7 @@
    1.77                end;
    1.78  
    1.79  fun if_exp(thm,ss,anet,ats,cs) =
    1.80 -        case Sequence.pull(tapply(IF1_TAC (cong_tac i) i,thm)) of
    1.81 +        case Sequence.pull (IF1_TAC (cong_tac i) i thm) of
    1.82                  Some(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
    1.83                | None => (ss,thm,anet,ats,cs);
    1.84  
    1.85 @@ -479,7 +479,7 @@
    1.86            MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
    1.87          | ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
    1.88          | SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
    1.89 -        | REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
    1.90 +        | REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true)
    1.91          | REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
    1.92          | TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
    1.93          | PROVE => (if if_fl then MK_EQ::SIMP_LHS::IF::TRUE::ss
    1.94 @@ -496,10 +496,11 @@
    1.95  
    1.96  fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
    1.97  let val cong_tac = net_tac cong_net
    1.98 -in fn i => Tactic(fn thm =>
    1.99 -        if i <= 0 orelse nprems_of thm < i then Sequence.null
   1.100 -        else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
   1.101 -           THEN TRY(auto_tac i)
   1.102 +in fn i => 
   1.103 +    (fn thm =>
   1.104 +     if i <= 0 orelse nprems_of thm < i then Sequence.null
   1.105 +     else Sequence.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
   1.106 +    THEN TRY(auto_tac i)
   1.107  end;
   1.108  
   1.109  val SIMP_TAC = EXEC_TAC([MK_EQ,SIMP_LHS,REFL,STOP],false);