src/FOLP/simp.ML
changeset 21078 101aefd61aac
parent 20951 868120282837
child 21287 a713ae348e8a
     1.1 --- a/src/FOLP/simp.ML	Fri Oct 20 17:07:25 2006 +0200
     1.2 +++ b/src/FOLP/simp.ML	Fri Oct 20 17:07:26 2006 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4  
     1.5  (*** Indexing and filtering of theorems ***)
     1.6  
     1.7 -fun eq_brl ((b1,th1),(b2,th2)) = b1=b2 andalso Drule.eq_thm_prop (th1,th2);
     1.8 +fun eq_brl ((b1 : bool, th1), (b2, th2)) = b1 = b2 andalso Drule.eq_thm_prop (th1, th2);
     1.9  
    1.10  (*insert a thm in a discrimination net by its lhs*)
    1.11  fun lhs_insert_thm (th,net) =
    1.12 @@ -155,25 +155,25 @@
    1.13  
    1.14  (*ccs contains the names of the constants possessing congruence rules*)
    1.15  fun add_hidden_vars ccs =
    1.16 -  let fun add_hvars(tm,hvars) = case tm of
    1.17 +  let fun add_hvars tm hvars = case tm of
    1.18                Abs(_,_,body) => add_term_vars(body,hvars)
    1.19              | _$_ => let val (f,args) = strip_comb tm 
    1.20                       in case f of
    1.21                              Const(c,T) => 
    1.22 -                                if c mem ccs
    1.23 -                                then foldr add_hvars hvars args
    1.24 -                                else add_term_vars(tm,hvars)
    1.25 -                          | _ => add_term_vars(tm,hvars)
    1.26 +                                if member (op =) ccs c
    1.27 +                                then fold_rev add_hvars args hvars
    1.28 +                                else add_term_vars (tm, hvars)
    1.29 +                          | _ => add_term_vars (tm, hvars)
    1.30                       end
    1.31              | _ => hvars;
    1.32    in add_hvars end;
    1.33  
    1.34  fun add_new_asm_vars new_asms =
    1.35 -    let fun itf((tm,at),vars) =
    1.36 +    let fun itf (tm, at) vars =
    1.37                  if at then vars else add_term_vars(tm,vars)
    1.38          fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
    1.39                  in if length(tml)=length(al)
    1.40 -                   then foldr itf vars (tml~~al)
    1.41 +                   then fold_rev itf (tml ~~ al) vars
    1.42                     else vars
    1.43                  end
    1.44          fun add_vars (tm,vars) = case tm of
    1.45 @@ -194,12 +194,12 @@
    1.46      val lhs = rhs_of_eq 1 thm'
    1.47      val rhs = lhs_of_eq nops thm'
    1.48      val asms = tl(rev(tl(prems_of thm')))
    1.49 -    val hvars = foldr (add_hidden_vars ccs) [] (lhs::rhs::asms)
    1.50 +    val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) []
    1.51      val hvars = add_new_asm_vars new_asms (rhs,hvars)
    1.52 -    fun it_asms (asm,hvars) =
    1.53 +    fun it_asms asm hvars =
    1.54          if atomic asm then add_new_asm_vars new_asms (asm,hvars)
    1.55          else add_term_frees(asm,hvars)
    1.56 -    val hvars = foldr it_asms hvars asms
    1.57 +    val hvars = fold_rev it_asms asms hvars
    1.58      val hvs = map (#1 o dest_Var) hvars
    1.59      val refl1_tac = refl_tac 1
    1.60      fun norm_step_tac st = st |>
    1.61 @@ -247,18 +247,18 @@
    1.62  (** Insertion of congruences and rewrites **)
    1.63  
    1.64  (*insert a thm in a thm net*)
    1.65 -fun insert_thm_warn (th,net) = 
    1.66 +fun insert_thm_warn th net = 
    1.67    Net.insert_term Drule.eq_thm_prop (concl_of th, th) net
    1.68    handle Net.INSERT => 
    1.69      (writeln"\nDuplicate rewrite or congruence rule:"; print_thm th;
    1.70       net);
    1.71  
    1.72 -val insert_thms = foldr insert_thm_warn;
    1.73 +val insert_thms = fold_rev insert_thm_warn;
    1.74  
    1.75  fun addrew(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thm) =
    1.76  let val thms = mk_simps thm
    1.77  in SS{auto_tac=auto_tac,congs=congs, cong_net=cong_net, mk_simps=mk_simps,
    1.78 -      simps = (thm,thms)::simps, simp_net = insert_thms simp_net thms}
    1.79 +      simps = (thm,thms)::simps, simp_net = insert_thms thms simp_net}
    1.80  end;
    1.81  
    1.82  val op addrews = Library.foldl addrew;
    1.83 @@ -266,25 +266,25 @@
    1.84  fun op addcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
    1.85  let val congs' = thms @ congs;
    1.86  in SS{auto_tac=auto_tac, congs= congs',
    1.87 -      cong_net= insert_thms cong_net (map mk_trans thms),
    1.88 +      cong_net= insert_thms (map mk_trans thms) cong_net,
    1.89        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
    1.90  end;
    1.91  
    1.92  (** Deletion of congruences and rewrites **)
    1.93  
    1.94  (*delete a thm from a thm net*)
    1.95 -fun delete_thm_warn (th,net) = 
    1.96 +fun delete_thm_warn th net = 
    1.97    Net.delete_term Drule.eq_thm_prop (concl_of th, th) net
    1.98    handle Net.DELETE => 
    1.99      (writeln"\nNo such rewrite or congruence rule:";  print_thm th;
   1.100       net);
   1.101  
   1.102 -val delete_thms = foldr delete_thm_warn;
   1.103 +val delete_thms = fold_rev delete_thm_warn;
   1.104  
   1.105  fun op delcongs(SS{auto_tac,congs,cong_net,mk_simps,simps,simp_net}, thms) =
   1.106  let val congs' = fold (remove Drule.eq_thm_prop) thms congs
   1.107  in SS{auto_tac=auto_tac, congs= congs',
   1.108 -      cong_net= delete_thms cong_net (map mk_trans thms),
   1.109 +      cong_net= delete_thms (map mk_trans thms) cong_net,
   1.110        mk_simps= normed_rews congs', simps=simps, simp_net=simp_net}
   1.111  end;
   1.112  
   1.113 @@ -296,7 +296,7 @@
   1.114                             ([],simps'))
   1.115      val (thms,simps') = find(simps,[])
   1.116  in SS{auto_tac=auto_tac, congs=congs, cong_net=cong_net, mk_simps=mk_simps,
   1.117 -      simps = simps', simp_net = delete_thms simp_net thms}
   1.118 +      simps = simps', simp_net = delete_thms thms simp_net }
   1.119  end;
   1.120  
   1.121  val op delrews = Library.foldl delrew;