new forward deduction capability for simplifier
authornipkow
Fri Sep 10 00:19:15 2004 +0200 (2004-09-10)
changeset 15195197e00ce3f20
parent 15194 ddbbab501213
child 15196 c7d69df58482
new forward deduction capability for simplifier
src/HOL/Hyperreal/Lim.thy
src/HOL/arith_data.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/HOL/Hyperreal/Lim.thy	Thu Sep 09 11:10:16 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/Lim.thy	Fri Sep 10 00:19:15 2004 +0200
     1.3 @@ -1507,8 +1507,6 @@
     1.4  apply (simp_all add: abs_if)
     1.5  apply (drule_tac x = "aa-x" in spec)
     1.6  apply (case_tac "x \<le> aa", simp_all)
     1.7 -apply (drule_tac x = x and y = aa in order_antisym)
     1.8 -apply (assumption, simp)
     1.9  done
    1.10  
    1.11  lemma IVT2: "[| f(b) \<le> y; y \<le> f(a);
    1.12 @@ -1603,7 +1601,7 @@
    1.13      proof (rule ccontr)
    1.14        assume "\<not> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
    1.15        with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
    1.16 -        by (auto simp add: linorder_not_le [symmetric] intro: order_antisym)
    1.17 +        by (fastsimp simp add: linorder_not_le [symmetric])
    1.18        hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
    1.19          by (auto simp add: isCont_inverse isCont_diff con)
    1.20        from isCont_bounded [OF le this]
    1.21 @@ -1851,8 +1849,8 @@
    1.22          assume az: "a \<le> z" and zb: "z \<le> b"
    1.23          show "f z = f b"
    1.24          proof (rule order_antisym)
    1.25 -          show "f z \<le> f b" by (simp add: fb_eq_fx x_max az zb) 
    1.26 -          show "f b \<le> f z" by (simp add: fb_eq_fx' x'_min az zb) 
    1.27 +          show "f z \<le> f b" by (simp add: fb_eq_fx x_max az zb)
    1.28 +          show "f b \<le> f z" by (simp add: fb_eq_fx' x'_min az zb)
    1.29          qed
    1.30        qed
    1.31        have bound': "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> f r = f y"
     2.1 --- a/src/HOL/arith_data.ML	Thu Sep 09 11:10:16 2004 +0200
     2.2 +++ b/src/HOL/arith_data.ML	Fri Sep 10 00:19:15 2004 +0200
     2.3 @@ -481,11 +481,55 @@
     2.4  
     2.5  end;
     2.6  
     2.7 +(* antisymmetry:
     2.8 +   combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y *)
     2.9 +
    2.10 +local
    2.11 +val antisym = mk_meta_eq order_antisym
    2.12 +val not_lessD = linorder_not_less RS iffD1
    2.13 +fun prp t thm = (#prop(rep_thm thm) = t)
    2.14 +in
    2.15 +fun antisym_eq prems thm =
    2.16 +  let
    2.17 +    val r = #prop(rep_thm thm);
    2.18 +  in
    2.19 +    case r of
    2.20 +      Tr $ ((c as Const("op <=",T)) $ s $ t) =>
    2.21 +        let val r' = Tr $ (c $ t $ s)
    2.22 +        in
    2.23 +          case Library.find_first (prp r') prems of
    2.24 +            None =>
    2.25 +              let val r' = Tr $ (HOLogic.not_const $ (Const("op <",T) $ s $ t))
    2.26 +              in case Library.find_first (prp r') prems of
    2.27 +                   None => []
    2.28 +                 | Some thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
    2.29 +              end
    2.30 +          | Some thm' => [thm' RS (thm RS antisym)]
    2.31 +        end
    2.32 +    | Tr $ (Const("Not",_) $ (Const("op <",T) $ s $ t)) =>
    2.33 +        let val r' = Tr $ (Const("op <=",T) $ s $ t)
    2.34 +        in
    2.35 +          case Library.find_first (prp r') prems of
    2.36 +            None =>
    2.37 +              let val r' = Tr $ (HOLogic.not_const $ (Const("op <",T) $ t $ s))
    2.38 +              in case Library.find_first (prp r') prems of
    2.39 +                   None => []
    2.40 +                 | Some thm' =>
    2.41 +                     [(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)]
    2.42 +              end
    2.43 +          | Some thm' => [thm' RS ((thm RS not_lessD) RS antisym)]
    2.44 +        end
    2.45 +    | _ => []
    2.46 +  end
    2.47 +  handle THM _ => []
    2.48 +end;
    2.49 +
    2.50  
    2.51  (* theory setup *)
    2.52  
    2.53  val arith_setup =
    2.54 - [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
    2.55 + [Simplifier.change_simpset_of (op setmksimps2) antisym_eq,
    2.56 +  Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
    2.57    init_lin_arith_data @
    2.58    [Simplifier.change_simpset_of (op addSolver)
    2.59     (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
     3.1 --- a/src/Pure/meta_simplifier.ML	Thu Sep 09 11:10:16 2004 +0200
     3.2 +++ b/src/Pure/meta_simplifier.ML	Fri Sep 10 00:19:15 2004 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  infix 4
     3.6    addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
     3.7 -  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
     3.8 +  setmksimps setmksimps2 setmkcong setmksym setmkeqTrue settermless setsubgoaler
     3.9    setloop addloop delloop setSSolver addSSolver setSolver addSolver;
    3.10  
    3.11  signature BASIC_META_SIMPLIFIER =
    3.12 @@ -30,6 +30,7 @@
    3.13      procs: proc Net.net,
    3.14      mk_rews:
    3.15       {mk: thm -> thm list,
    3.16 +      mk2: thm list -> thm -> thm list,
    3.17        mk_cong: thm -> thm,
    3.18        mk_sym: thm -> thm option,
    3.19        mk_eq_True: thm -> thm option},
    3.20 @@ -54,6 +55,7 @@
    3.21    val addsimprocs: simpset * simproc list -> simpset
    3.22    val delsimprocs: simpset * simproc list -> simpset
    3.23    val setmksimps: simpset * (thm -> thm list) -> simpset
    3.24 +  val setmksimps2: simpset * (thm list -> thm -> thm list) -> simpset
    3.25    val setmkcong: simpset * (thm -> thm) -> simpset
    3.26    val setmksym: simpset * (thm -> thm option) -> simpset
    3.27    val setmkeqTrue: simpset * (thm -> thm option) -> simpset
    3.28 @@ -203,6 +205,7 @@
    3.29        (functions that prove rewrite rules on the fly);
    3.30      mk_rews:
    3.31        mk: turn simplification thms into rewrite rules;
    3.32 +      mk2: like mk but may also depend on the other premises
    3.33        mk_cong: prepare congruence rules;
    3.34        mk_sym: turn == around;
    3.35        mk_eq_True: turn P into P == True;
    3.36 @@ -210,6 +213,7 @@
    3.37  
    3.38  type mk_rews =
    3.39   {mk: thm -> thm list,
    3.40 +  mk2: thm list -> thm -> thm list,
    3.41    mk_cong: thm -> thm,
    3.42    mk_sym: thm -> thm option,
    3.43    mk_eq_True: thm -> thm option};
    3.44 @@ -302,6 +306,7 @@
    3.45  
    3.46  val basic_mk_rews: mk_rews =
    3.47   {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
    3.48 +  mk2 = fn thms => fn thm => [],
    3.49    mk_cong = I,
    3.50    mk_sym = Some o Drule.symmetric_fun,
    3.51    mk_eq_True = K None};
    3.52 @@ -486,8 +491,11 @@
    3.53      else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
    3.54    end;
    3.55  
    3.56 -fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
    3.57 -  flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
    3.58 +fun extract_rews (Simpset ({prems, ...}, {mk_rews = {mk, ...}, ...}), thms)
    3.59 +  = flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
    3.60 +
    3.61 +fun extract_rews2 (Simpset ({prems, ...}, {mk_rews = {mk2, ...}, ...}), thms)
    3.62 +  = flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk2 prems thm)) thms);
    3.63  
    3.64  fun orient_comb_simps comb mk_rrule (ss, thms) =
    3.65    let
    3.66 @@ -498,11 +506,20 @@
    3.67  fun extract_safe_rrules (ss, thm) =
    3.68    flat (map (orient_rrule ss) (extract_rews (ss, [thm])));
    3.69  
    3.70 +fun extract_safe_rrules2 (ss, thm) =
    3.71 +  flat (map (orient_rrule ss) (extract_rews2 (ss, [thm])));
    3.72 +
    3.73  (*add rewrite rules explicitly; do not reorient!*)
    3.74  fun ss addsimps thms =
    3.75    orient_comb_simps (insert_rrule false) (mk_rrule ss) (ss, thms);
    3.76  
    3.77  
    3.78 +fun add_prem2(ss,thm) =
    3.79 +  foldl (insert_rrule true) (ss,extract_safe_rrules2(ss,thm))
    3.80 +  |> add_prems [thm];
    3.81 +
    3.82 +fun add_prems2 thms ss = foldl add_prem2 (ss,thms);
    3.83 +
    3.84  (* delsimps *)
    3.85  
    3.86  fun del_rrule (ss, rrule as {thm, elhs, ...}) =
    3.87 @@ -617,26 +634,29 @@
    3.88  
    3.89  local
    3.90  
    3.91 -fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True},
    3.92 +fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk2, mk_cong, mk_sym, mk_eq_True},
    3.93        termless, subgoal_tac, loop_tacs, solvers) =>
    3.94 -  let val (mk', mk_cong', mk_sym', mk_eq_True') = f (mk, mk_cong, mk_sym, mk_eq_True) in
    3.95 -    (congs, procs, {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'},
    3.96 +  let val (mk', mk2', mk_cong', mk_sym', mk_eq_True') = f (mk, mk2, mk_cong, mk_sym, mk_eq_True) in
    3.97 +    (congs, procs, {mk = mk', mk2 = mk2', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'},
    3.98        termless, subgoal_tac, loop_tacs, solvers)
    3.99    end);
   3.100  
   3.101  in
   3.102  
   3.103 -fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True) =>
   3.104 -  (mk, mk_cong, mk_sym, mk_eq_True));
   3.105 +fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk2, mk_cong, mk_sym, mk_eq_True) =>
   3.106 +  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   3.107  
   3.108 -fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True) =>
   3.109 -  (mk, mk_cong, mk_sym, mk_eq_True));
   3.110 +fun ss setmksimps2 mk2 = ss |> map_mk_rews (fn (mk, _, mk_cong, mk_sym, mk_eq_True) =>
   3.111 +  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   3.112  
   3.113 -fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True) =>
   3.114 -  (mk, mk_cong, mk_sym, mk_eq_True));
   3.115 +fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, mk2, _, mk_sym, mk_eq_True) =>
   3.116 +  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   3.117  
   3.118 -fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _) =>
   3.119 -  (mk, mk_cong, mk_sym, mk_eq_True));
   3.120 +fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk2, mk_cong, _, mk_eq_True) =>
   3.121 +  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   3.122 +
   3.123 +fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk2, mk_cong, mk_sym, _) =>
   3.124 +  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
   3.125  
   3.126  end;
   3.127  
   3.128 @@ -999,7 +1019,8 @@
   3.129          in (extract_safe_rrules (ss, asm), Some asm) end
   3.130  
   3.131      and add_rrules (rrss, asms) ss =
   3.132 -      foldl (insert_rrule true) (ss, flat rrss) |> add_prems (mapfilter I asms)
   3.133 +      let val Asms = mapfilter I asms
   3.134 +      in foldl (insert_rrule true) (ss, flat rrss) |> add_prems2 Asms end
   3.135  
   3.136      and disch r (prem, eq) =
   3.137        let