undoing previous change
authornipkow
Sat Sep 11 18:35:43 2004 +0200 (2004-09-11)
changeset 1519929ca1fe63e7b
parent 15198 44495334adcc
child 15200 09489fe6989f
undoing previous change
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Sat Sep 11 09:25:47 2004 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Sat Sep 11 18:35:43 2004 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  infix 4
     1.6    addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
     1.7 -  setmksimps setmksimps2 setmkcong setmksym setmkeqTrue settermless setsubgoaler
     1.8 +  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
     1.9    setloop addloop delloop setSSolver addSSolver setSolver addSolver;
    1.10  
    1.11  signature BASIC_META_SIMPLIFIER =
    1.12 @@ -30,7 +30,6 @@
    1.13      procs: proc Net.net,
    1.14      mk_rews:
    1.15       {mk: thm -> thm list,
    1.16 -      mk2: thm list -> thm -> thm list,
    1.17        mk_cong: thm -> thm,
    1.18        mk_sym: thm -> thm option,
    1.19        mk_eq_True: thm -> thm option},
    1.20 @@ -55,7 +54,6 @@
    1.21    val addsimprocs: simpset * simproc list -> simpset
    1.22    val delsimprocs: simpset * simproc list -> simpset
    1.23    val setmksimps: simpset * (thm -> thm list) -> simpset
    1.24 -  val setmksimps2: simpset * (thm list -> thm -> thm list) -> simpset
    1.25    val setmkcong: simpset * (thm -> thm) -> simpset
    1.26    val setmksym: simpset * (thm -> thm option) -> simpset
    1.27    val setmkeqTrue: simpset * (thm -> thm option) -> simpset
    1.28 @@ -205,7 +203,6 @@
    1.29        (functions that prove rewrite rules on the fly);
    1.30      mk_rews:
    1.31        mk: turn simplification thms into rewrite rules;
    1.32 -      mk2: like mk but may also depend on the other premises
    1.33        mk_cong: prepare congruence rules;
    1.34        mk_sym: turn == around;
    1.35        mk_eq_True: turn P into P == True;
    1.36 @@ -213,7 +210,6 @@
    1.37  
    1.38  type mk_rews =
    1.39   {mk: thm -> thm list,
    1.40 -  mk2: thm list -> thm -> thm list,
    1.41    mk_cong: thm -> thm,
    1.42    mk_sym: thm -> thm option,
    1.43    mk_eq_True: thm -> thm option};
    1.44 @@ -306,7 +302,6 @@
    1.45  
    1.46  val basic_mk_rews: mk_rews =
    1.47   {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
    1.48 -  mk2 = fn thms => fn thm => [],
    1.49    mk_cong = I,
    1.50    mk_sym = Some o Drule.symmetric_fun,
    1.51    mk_eq_True = K None};
    1.52 @@ -491,11 +486,8 @@
    1.53      else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
    1.54    end;
    1.55  
    1.56 -fun extract_rews (Simpset ({prems, ...}, {mk_rews = {mk, ...}, ...}), thms)
    1.57 -  = flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
    1.58 -
    1.59 -fun extract_rews2 (Simpset ({prems, ...}, {mk_rews = {mk2, ...}, ...}), thms)
    1.60 -  = flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk2 prems thm)) thms);
    1.61 +fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
    1.62 +  flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
    1.63  
    1.64  fun orient_comb_simps comb mk_rrule (ss, thms) =
    1.65    let
    1.66 @@ -506,20 +498,11 @@
    1.67  fun extract_safe_rrules (ss, thm) =
    1.68    flat (map (orient_rrule ss) (extract_rews (ss, [thm])));
    1.69  
    1.70 -fun extract_safe_rrules2 (ss, thm) =
    1.71 -  flat (map (orient_rrule ss) (extract_rews2 (ss, [thm])));
    1.72 -
    1.73  (*add rewrite rules explicitly; do not reorient!*)
    1.74  fun ss addsimps thms =
    1.75    orient_comb_simps (insert_rrule false) (mk_rrule ss) (ss, thms);
    1.76  
    1.77  
    1.78 -fun add_prem2(ss,thm) =
    1.79 -  foldl (insert_rrule true) (ss,extract_safe_rrules2(ss,thm))
    1.80 -  |> add_prems [thm];
    1.81 -
    1.82 -fun add_prems2 thms ss = foldl add_prem2 (ss,thms);
    1.83 -
    1.84  (* delsimps *)
    1.85  
    1.86  fun del_rrule (ss, rrule as {thm, elhs, ...}) =
    1.87 @@ -634,29 +617,26 @@
    1.88  
    1.89  local
    1.90  
    1.91 -fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk2, mk_cong, mk_sym, mk_eq_True},
    1.92 +fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True},
    1.93        termless, subgoal_tac, loop_tacs, solvers) =>
    1.94 -  let val (mk', mk2', mk_cong', mk_sym', mk_eq_True') = f (mk, mk2, mk_cong, mk_sym, mk_eq_True) in
    1.95 -    (congs, procs, {mk = mk', mk2 = mk2', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'},
    1.96 +  let val (mk', mk_cong', mk_sym', mk_eq_True') = f (mk, mk_cong, mk_sym, mk_eq_True) in
    1.97 +    (congs, procs, {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'},
    1.98        termless, subgoal_tac, loop_tacs, solvers)
    1.99    end);
   1.100  
   1.101  in
   1.102  
   1.103 -fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk2, mk_cong, mk_sym, mk_eq_True) =>
   1.104 -  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   1.105 +fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True) =>
   1.106 +  (mk, mk_cong, mk_sym, mk_eq_True));
   1.107  
   1.108 -fun ss setmksimps2 mk2 = ss |> map_mk_rews (fn (mk, _, mk_cong, mk_sym, mk_eq_True) =>
   1.109 -  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   1.110 +fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True) =>
   1.111 +  (mk, mk_cong, mk_sym, mk_eq_True));
   1.112  
   1.113 -fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, mk2, _, mk_sym, mk_eq_True) =>
   1.114 -  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   1.115 +fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True) =>
   1.116 +  (mk, mk_cong, mk_sym, mk_eq_True));
   1.117  
   1.118 -fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk2, mk_cong, _, mk_eq_True) =>
   1.119 -  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   1.120 -
   1.121 -fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk2, mk_cong, mk_sym, _) =>
   1.122 -  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   1.123 +fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _) =>
   1.124 +  (mk, mk_cong, mk_sym, mk_eq_True));
   1.125  
   1.126  end;
   1.127  
   1.128 @@ -1019,8 +999,7 @@
   1.129          in (extract_safe_rrules (ss, asm), Some asm) end
   1.130  
   1.131      and add_rrules (rrss, asms) ss =
   1.132 -      let val Asms = mapfilter I asms
   1.133 -      in foldl (insert_rrule true) (ss, flat rrss) |> add_prems2 Asms end
   1.134 +      foldl (insert_rrule true) (ss, flat rrss) |> add_prems (mapfilter I asms)
   1.135  
   1.136      and disch r (prem, eq) =
   1.137        let