src/FOLP/simp.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/FOLP/simp.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/FOLP/simp.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -84,7 +84,7 @@
     1.4            biresolve_tac (Net.unify_term net
     1.5                         (lhs_of (strip_assums_concl prem))) i);
     1.6  
     1.7 -fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
     1.8 +fun nth_subgoal i thm = List.nth(prems_of thm,i-1);
     1.9  
    1.10  fun goal_concl i thm = strip_assums_concl(nth_subgoal i thm);
    1.11  
    1.12 @@ -161,7 +161,7 @@
    1.13                       in case f of
    1.14                              Const(c,T) => 
    1.15                                  if c mem ccs
    1.16 -                                then foldr add_hvars (args,hvars)
    1.17 +                                then Library.foldr add_hvars (args,hvars)
    1.18                                  else add_term_vars(tm,hvars)
    1.19                            | _ => add_term_vars(tm,hvars)
    1.20                       end
    1.21 @@ -173,7 +173,7 @@
    1.22                  if at then vars else add_term_vars(tm,vars)
    1.23          fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
    1.24                  in if length(tml)=length(al)
    1.25 -                   then foldr itf (tml~~al,vars)
    1.26 +                   then Library.foldr itf (tml~~al,vars)
    1.27                     else vars
    1.28                  end
    1.29          fun add_vars (tm,vars) = case tm of
    1.30 @@ -194,12 +194,12 @@
    1.31      val lhs = rhs_of_eq 1 thm'
    1.32      val rhs = lhs_of_eq nops thm'
    1.33      val asms = tl(rev(tl(prems_of thm')))
    1.34 -    val hvars = foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
    1.35 +    val hvars = Library.foldr (add_hidden_vars ccs) (lhs::rhs::asms,[])
    1.36      val hvars = add_new_asm_vars new_asms (rhs,hvars)
    1.37      fun it_asms (asm,hvars) =
    1.38          if atomic asm then add_new_asm_vars new_asms (asm,hvars)
    1.39          else add_term_frees(asm,hvars)
    1.40 -    val hvars = foldr it_asms (asms,hvars)
    1.41 +    val hvars = Library.foldr it_asms (asms,hvars)
    1.42      val hvs = map (#1 o dest_Var) hvars
    1.43      val refl1_tac = refl_tac 1
    1.44      fun norm_step_tac st = st |>
    1.45 @@ -216,7 +216,7 @@
    1.46  
    1.47  fun add_norm_tags congs =
    1.48      let val ccs = map cong_const congs
    1.49 -        val new_asms = filter (exists not o #2)
    1.50 +        val new_asms = List.filter (exists not o #2)
    1.51                  (ccs ~~ (map (map atomic o prems_of) congs));
    1.52      in add_norms(congs,ccs,new_asms) end;
    1.53  
    1.54 @@ -252,7 +252,7 @@
    1.55      (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
    1.56       net);
    1.57  
    1.58 -val insert_thms = foldr insert_thm_warn;
    1.59 +val insert_thms = Library.foldr insert_thm_warn;
    1.60  
    1.61  fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    1.62  let val thms = mk_simps thm
    1.63 @@ -260,7 +260,7 @@
    1.64        simps = (thm,thms)::simps, simp_net = insert_thms(thms,simp_net)}
    1.65  end;
    1.66  
    1.67 -val op addrews = foldl addrew;
    1.68 +val op addrews = Library.foldl addrew;
    1.69  
    1.70  fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
    1.71  let val congs' = thms @ congs;
    1.72 @@ -278,10 +278,10 @@
    1.73      (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
    1.74       net);
    1.75  
    1.76 -val delete_thms = foldr delete_thm_warn;
    1.77 +val delete_thms = Library.foldr delete_thm_warn;
    1.78  
    1.79  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
    1.80 -let val congs' = foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
    1.81 +let val congs' = Library.foldl (gen_rem Drule.eq_thm_prop) (congs,thms)
    1.82  in SS{auto_tac=auto_tac, congs= congs',
    1.83        cong_net= delete_thms(map mk_trans thms,cong_net),
    1.84        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
    1.85 @@ -298,7 +298,7 @@
    1.86        simps = simps', simp_net = delete_thms(thms,simp_net)}
    1.87  end;
    1.88  
    1.89 -val op delrews = foldl delrew;
    1.90 +val op delrews = Library.foldl delrew;
    1.91  
    1.92  
    1.93  fun op setauto(SS{congs,cong_net,mk_simps,simps,simp_net,...}, auto_tac) =
    1.94 @@ -426,9 +426,9 @@
    1.95              SOME(thm',_) =>
    1.96                      let val ps = prems_of thm and ps' = prems_of thm';
    1.97                          val n = length(ps')-length(ps);
    1.98 -                        val a = length(strip_assums_hyp(nth_elem(i-1,ps)))
    1.99 +                        val a = length(strip_assums_hyp(List.nth(ps,i-1)))
   1.100                          val l = map (fn p => length(strip_assums_hyp(p)))
   1.101 -                                    (take(n,drop(i-1,ps')));
   1.102 +                                    (Library.take(n,Library.drop(i-1,ps')));
   1.103                      in (simp_refl(rev(l),a,REW::ss),thm',anet,ats,cs) end
   1.104            | NONE => (REW::ss,thm,anet,ats,cs);
   1.105  
   1.106 @@ -437,9 +437,9 @@
   1.107  fun add_asms(ss,thm,a,anet,ats,cs) =
   1.108      let val As = strip_varify(nth_subgoal i thm, a, []);
   1.109          val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
   1.110 -        val new_rws = flat(map mk_rew_rules thms);
   1.111 -        val rwrls = map mk_trans (flat(map mk_rew_rules thms));
   1.112 -        val anet' = foldr lhs_insert_thm (rwrls,anet)
   1.113 +        val new_rws = List.concat(map mk_rew_rules thms);
   1.114 +        val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
   1.115 +        val anet' = Library.foldr lhs_insert_thm (rwrls,anet)
   1.116      in  if !tracing andalso not(null new_rws)
   1.117          then (writeln"Adding rewrites:";  prths new_rws;  ())
   1.118          else ();
   1.119 @@ -539,7 +539,7 @@
   1.120  fun Pinst(f,fT,(eq,eqT),k,i,T,yik,Ts) =
   1.121  let fun xn_list(x,n) =
   1.122          let val ixs = map (fn i => (x^(radixstring(26,"a",i)),0)) (0 upto n);
   1.123 -        in ListPair.map eta_Var (ixs, take(n+1,Ts)) end
   1.124 +        in ListPair.map eta_Var (ixs, Library.take(n+1,Ts)) end
   1.125      val lhs = list_comb(f,xn_list("X",k-1))
   1.126      val rhs = list_comb(f,xn_list("X",i-1) @ [Bound 0] @ yik)
   1.127  in Abs("", T, Const(eq,[fT,fT]--->eqT) $ lhs $ rhs) end;
   1.128 @@ -596,7 +596,7 @@
   1.129      val T' = incr_tvar 9 T;
   1.130  in mk_cong_type sg (Const(f,T'),T') end;
   1.131  
   1.132 -fun mk_congs thy = flat o map (mk_cong_thy thy);
   1.133 +fun mk_congs thy = List.concat o map (mk_cong_thy thy);
   1.134  
   1.135  fun mk_typed_congs thy =
   1.136  let val sg = sign_of thy;
   1.137 @@ -606,7 +606,7 @@
   1.138              val t = case Sign.const_type sg f of
   1.139                        SOME(_) => Const(f,T) | NONE => Free(f,T)
   1.140          in (t,T) end
   1.141 -in flat o map (mk_cong_type sg o readfT) end;
   1.142 +in List.concat o map (mk_cong_type sg o readfT) end;
   1.143  
   1.144  end (* local *)
   1.145  end (* SIMP *);