src/FOLP/simp.ML
changeset 15531 08c8dad8e399
parent 14772 c52060b69a8c
child 15570 8d8c70b41bab
     1.1 --- a/src/FOLP/simp.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/FOLP/simp.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -136,8 +136,8 @@
     1.4  
     1.5  (*Applies tactic and returns the first resulting state, FAILS if none!*)
     1.6  fun one_result(tac,thm) = case Seq.pull(tac thm) of
     1.7 -        Some(thm',_) => thm'
     1.8 -      | None => raise THM("Simplifier: could not continue", 0, [thm]);
     1.9 +        SOME(thm',_) => thm'
    1.10 +      | NONE => raise THM("Simplifier: could not continue", 0, [thm]);
    1.11  
    1.12  fun res1(thm,thms,i) = one_result(resolve_tac thms i,thm);
    1.13  
    1.14 @@ -180,8 +180,8 @@
    1.15                    Abs (_,_,body) => add_vars(body,vars)
    1.16                  | r$s => (case head_of tm of
    1.17                            Const(c,T) => (case assoc(new_asms,c) of
    1.18 -                                  None => add_vars(r,add_vars(s,vars))
    1.19 -                                | Some(al) => add_list(tm,al,vars))
    1.20 +                                  NONE => add_vars(r,add_vars(s,vars))
    1.21 +                                | SOME(al) => add_list(tm,al,vars))
    1.22                          | _ => add_vars(r,add_vars(s,vars)))
    1.23                  | _ => vars
    1.24      in add_vars end;
    1.25 @@ -211,7 +211,7 @@
    1.26  	  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    1.27  	  | _ => refl1_tac)
    1.28      val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
    1.29 -    val Some(thm'',_) = Seq.pull(add_norm_tac thm')
    1.30 +    val SOME(thm'',_) = Seq.pull(add_norm_tac thm')
    1.31  in thm'' end;
    1.32  
    1.33  fun add_norm_tags congs =
    1.34 @@ -423,14 +423,14 @@
    1.35      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
    1.36      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
    1.37      else case Seq.pull(cong_tac i thm) of
    1.38 -            Some(thm',_) =>
    1.39 +            SOME(thm',_) =>
    1.40                      let val ps = prems_of thm and ps' = prems_of thm';
    1.41                          val n = length(ps')-length(ps);
    1.42                          val a = length(strip_assums_hyp(nth_elem(i-1,ps)))
    1.43                          val l = map (fn p => length(strip_assums_hyp(p)))
    1.44                                      (take(n,drop(i-1,ps')));
    1.45                      in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
    1.46 -          | None => (REW::ss,thm,anet,ats,cs);
    1.47 +          | NONE => (REW::ss,thm,anet,ats,cs);
    1.48  
    1.49  (*NB: the "Adding rewrites:" trace will look strange because assumptions
    1.50        are represented by rules, generalized over their parameters*)
    1.51 @@ -447,22 +447,22 @@
    1.52      end;
    1.53  
    1.54  fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
    1.55 -      Some(thm',seq') =>
    1.56 +      SOME(thm',seq') =>
    1.57              let val n = (nprems_of thm') - (nprems_of thm)
    1.58              in pr_rew(i,n,thm,thm',more);
    1.59                 if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)
    1.60                 else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),
    1.61                       thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs)
    1.62              end
    1.63 -    | None => if more
    1.64 +    | NONE => if more
    1.65              then rew((lhs_net_tac anet i THEN assume_tac i) thm,
    1.66                       thm,ss,anet,ats,cs,false)
    1.67              else (ss,thm,anet,ats,cs);
    1.68  
    1.69  fun try_true(thm,ss,anet,ats,cs) =
    1.70      case Seq.pull(auto_tac i thm) of
    1.71 -      Some(thm',_) => (ss,thm',anet,ats,cs)
    1.72 -    | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
    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                   then (writeln"*** Failed to prove precondition. Normal form:";
    1.77                         pr_goal_concl i thm;  writeln"")
    1.78 @@ -472,8 +472,8 @@
    1.79  
    1.80  fun if_exp(thm,ss,anet,ats,cs) =
    1.81          case Seq.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 +                SOME(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs)
    1.85 +              | NONE => (ss,thm,anet,ats,cs);
    1.86  
    1.87  fun step(s::ss, thm, anet, ats, cs) = case s of
    1.88            MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
    1.89 @@ -549,10 +549,10 @@
    1.90          let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
    1.91              val [P] = add_term_vars(concl_of thm,[]) \\ [va,vb]
    1.92              val eqT::_ = binder_types cT
    1.93 -        in if Type.typ_instance tsig (T,eqT) then Some(thm,va,vb,P)
    1.94 +        in if Type.typ_instance tsig (T,eqT) then SOME(thm,va,vb,P)
    1.95             else find thms
    1.96          end
    1.97 -      | find [] = None
    1.98 +      | find [] = NONE
    1.99  in find subst_thms end;
   1.100  
   1.101  fun mk_cong sg (f,aTs,rT) (refl,eq) =
   1.102 @@ -569,8 +569,8 @@
   1.103      fun mk(c,T::Ts,i,yik) =
   1.104          let val si = radixstring(26,"a",i)
   1.105          in case find_subst tsig T of
   1.106 -             None => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik)
   1.107 -           | Some s => let val c' = c RSN (2,ri(s,i,si,T,yik))
   1.108 +             NONE => mk(c,Ts,i-1,eta_Var(("X"^si,0),T)::yik)
   1.109 +           | SOME s => let val c' = c RSN (2,ri(s,i,si,T,yik))
   1.110                         in mk(c',Ts,i-1,eta_Var(("Y"^si,0),T)::yik) end
   1.111          end
   1.112        | mk(c,[],_,_) = c;
   1.113 @@ -582,17 +582,17 @@
   1.114      fun find_refl(r::rs) =
   1.115          let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
   1.116          in if Type.typ_instance tsig (rT, hd(binder_types eqT))
   1.117 -           then Some(r,(eq,body_type eqT)) else find_refl rs
   1.118 +           then SOME(r,(eq,body_type eqT)) else find_refl rs
   1.119          end
   1.120 -      | find_refl([]) = None;
   1.121 +      | find_refl([]) = NONE;
   1.122  in case find_refl refl_thms of
   1.123 -     None => []  |  Some(refl) => [mk_cong sg (f,aTs,rT) refl]
   1.124 +     NONE => []  |  SOME(refl) => [mk_cong sg (f,aTs,rT) refl]
   1.125  end;
   1.126  
   1.127  fun mk_cong_thy thy f =
   1.128  let val sg = sign_of thy;
   1.129      val T = case Sign.const_type sg f of
   1.130 -                None => error(f^" not declared") | Some(T) => T;
   1.131 +                NONE => error(f^" not declared") | SOME(T) => T;
   1.132      val T' = incr_tvar 9 T;
   1.133  in mk_cong_type sg (Const(f,T'),T') end;
   1.134  
   1.135 @@ -602,9 +602,9 @@
   1.136  let val sg = sign_of thy;
   1.137      val S0 = Sign.defaultS sg;
   1.138      fun readfT(f,s) =
   1.139 -        let val T = incr_tvar 9 (Sign.read_typ(sg,K(Some(S0))) s);
   1.140 +        let val T = incr_tvar 9 (Sign.read_typ(sg,K(SOME(S0))) s);
   1.141              val t = case Sign.const_type sg f of
   1.142 -                      Some(_) => Const(f,T) | None => Free(f,T)
   1.143 +                      SOME(_) => Const(f,T) | NONE => Free(f,T)
   1.144          in (t,T) end
   1.145  in flat o map (mk_cong_type sg o readfT) end;
   1.146