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.16 -  let fun add_hvars(tm,hvars) = case tm of
1.17 +  let fun add_hvars tm hvars = case tm of
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.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.33
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.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.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.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;
```