src/Pure/meta_simplifier.ML
changeset 15195 197e00ce3f20
parent 15088 b8a95eadbc14
child 15199 29ca1fe63e7b
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Sep 09 11:10:16 2004 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Fri Sep 10 00:19:15 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 setmkcong setmksym setmkeqTrue settermless setsubgoaler
     1.8 +  setmksimps setmksimps2 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,6 +30,7 @@
    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 @@ -54,6 +55,7 @@
    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 @@ -203,6 +205,7 @@
    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 @@ -210,6 +213,7 @@
    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 @@ -302,6 +306,7 @@
    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 @@ -486,8 +491,11 @@
    1.53      else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
    1.54    end;
    1.55  
    1.56 -fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
    1.57 -  flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
    1.58 +fun extract_rews (Simpset ({prems, ...}, {mk_rews = {mk, ...}, ...}), thms)
    1.59 +  = flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
    1.60 +
    1.61 +fun extract_rews2 (Simpset ({prems, ...}, {mk_rews = {mk2, ...}, ...}), thms)
    1.62 +  = flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk2 prems thm)) thms);
    1.63  
    1.64  fun orient_comb_simps comb mk_rrule (ss, thms) =
    1.65    let
    1.66 @@ -498,11 +506,20 @@
    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 @@ -617,26 +634,29 @@
    1.88  
    1.89  local
    1.90  
    1.91 -fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True},
    1.92 +fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk2, mk_cong, mk_sym, mk_eq_True},
    1.93        termless, subgoal_tac, loop_tacs, solvers) =>
    1.94 -  let val (mk', mk_cong', mk_sym', mk_eq_True') = f (mk, mk_cong, mk_sym, mk_eq_True) in
    1.95 -    (congs, procs, {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'},
    1.96 +  let val (mk', mk2', mk_cong', mk_sym', mk_eq_True') = f (mk, mk2, mk_cong, mk_sym, mk_eq_True) in
    1.97 +    (congs, procs, {mk = mk', mk2 = mk2', 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 (_, mk_cong, mk_sym, mk_eq_True) =>
   1.104 -  (mk, mk_cong, mk_sym, mk_eq_True));
   1.105 +fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk2, mk_cong, mk_sym, mk_eq_True) =>
   1.106 +  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   1.107  
   1.108 -fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True) =>
   1.109 -  (mk, mk_cong, mk_sym, mk_eq_True));
   1.110 +fun ss setmksimps2 mk2 = ss |> map_mk_rews (fn (mk, _, mk_cong, mk_sym, mk_eq_True) =>
   1.111 +  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   1.112  
   1.113 -fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True) =>
   1.114 -  (mk, mk_cong, mk_sym, mk_eq_True));
   1.115 +fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, mk2, _, mk_sym, mk_eq_True) =>
   1.116 +  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   1.117  
   1.118 -fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _) =>
   1.119 -  (mk, mk_cong, mk_sym, mk_eq_True));
   1.120 +fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk2, mk_cong, _, mk_eq_True) =>
   1.121 +  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   1.122 +
   1.123 +fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk2, mk_cong, mk_sym, _) =>
   1.124 +  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   1.125  
   1.126  end;
   1.127  
   1.128 @@ -999,7 +1019,8 @@
   1.129          in (extract_safe_rrules (ss, asm), Some asm) end
   1.130  
   1.131      and add_rrules (rrss, asms) ss =
   1.132 -      foldl (insert_rrule true) (ss, flat rrss) |> add_prems (mapfilter I asms)
   1.133 +      let val Asms = mapfilter I asms
   1.134 +      in foldl (insert_rrule true) (ss, flat rrss) |> add_prems2 Asms end
   1.135  
   1.136      and disch r (prem, eq) =
   1.137        let