# HG changeset patch
# User nipkow
# Date 1094768355 -7200
# Node ID 197e00ce3f2080ea4da0ed242cfbb0650cbb41bf
# Parent  ddbbab501213e584e8acd3f1099ca7e3b7f53db4
new forward deduction capability for simplifier

diff -r ddbbab501213 -r 197e00ce3f20 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Thu Sep 09 11:10:16 2004 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Fri Sep 10 00:19:15 2004 +0200
@@ -1507,8 +1507,6 @@
 apply (simp_all add: abs_if)
 apply (drule_tac x = "aa-x" in spec)
 apply (case_tac "x \<le> aa", simp_all)
-apply (drule_tac x = x and y = aa in order_antisym)
-apply (assumption, simp)
 done
 
 lemma IVT2: "[| f(b) \<le> y; y \<le> f(a);
@@ -1603,7 +1601,7 @@
     proof (rule ccontr)
       assume "\<not> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
       with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
-        by (auto simp add: linorder_not_le [symmetric] intro: order_antisym)
+        by (fastsimp simp add: linorder_not_le [symmetric])
       hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
         by (auto simp add: isCont_inverse isCont_diff con)
       from isCont_bounded [OF le this]
@@ -1851,8 +1849,8 @@
         assume az: "a \<le> z" and zb: "z \<le> b"
         show "f z = f b"
         proof (rule order_antisym)
-          show "f z \<le> f b" by (simp add: fb_eq_fx x_max az zb) 
-          show "f b \<le> f z" by (simp add: fb_eq_fx' x'_min az zb) 
+          show "f z \<le> f b" by (simp add: fb_eq_fx x_max az zb)
+          show "f b \<le> f z" by (simp add: fb_eq_fx' x'_min az zb)
         qed
       qed
       have bound': "\<forall>y. \<bar>r-y\<bar> < d \<longrightarrow> f r = f y"
diff -r ddbbab501213 -r 197e00ce3f20 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Thu Sep 09 11:10:16 2004 +0200
+++ b/src/HOL/arith_data.ML	Fri Sep 10 00:19:15 2004 +0200
@@ -481,11 +481,55 @@
 
 end;
 
+(* antisymmetry:
+   combines x <= y (or ~(y < x)) and y <= x (or ~(x < y)) into x = y *)
+
+local
+val antisym = mk_meta_eq order_antisym
+val not_lessD = linorder_not_less RS iffD1
+fun prp t thm = (#prop(rep_thm thm) = t)
+in
+fun antisym_eq prems thm =
+  let
+    val r = #prop(rep_thm thm);
+  in
+    case r of
+      Tr $ ((c as Const("op <=",T)) $ s $ t) =>
+        let val r' = Tr $ (c $ t $ s)
+        in
+          case Library.find_first (prp r') prems of
+            None =>
+              let val r' = Tr $ (HOLogic.not_const $ (Const("op <",T) $ s $ t))
+              in case Library.find_first (prp r') prems of
+                   None => []
+                 | Some thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
+              end
+          | Some thm' => [thm' RS (thm RS antisym)]
+        end
+    | Tr $ (Const("Not",_) $ (Const("op <",T) $ s $ t)) =>
+        let val r' = Tr $ (Const("op <=",T) $ s $ t)
+        in
+          case Library.find_first (prp r') prems of
+            None =>
+              let val r' = Tr $ (HOLogic.not_const $ (Const("op <",T) $ t $ s))
+              in case Library.find_first (prp r') prems of
+                   None => []
+                 | Some thm' =>
+                     [(thm' RS not_lessD) RS ((thm RS not_lessD) RS antisym)]
+              end
+          | Some thm' => [thm' RS ((thm RS not_lessD) RS antisym)]
+        end
+    | _ => []
+  end
+  handle THM _ => []
+end;
+
 
 (* theory setup *)
 
 val arith_setup =
- [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
+ [Simplifier.change_simpset_of (op setmksimps2) antisym_eq,
+  Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
   init_lin_arith_data @
   [Simplifier.change_simpset_of (op addSolver)
    (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
diff -r ddbbab501213 -r 197e00ce3f20 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu Sep 09 11:10:16 2004 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Sep 10 00:19:15 2004 +0200
@@ -7,7 +7,7 @@
 
 infix 4
   addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
-  setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
+  setmksimps setmksimps2 setmkcong setmksym setmkeqTrue settermless setsubgoaler
   setloop addloop delloop setSSolver addSSolver setSolver addSolver;
 
 signature BASIC_META_SIMPLIFIER =
@@ -30,6 +30,7 @@
     procs: proc Net.net,
     mk_rews:
      {mk: thm -> thm list,
+      mk2: thm list -> thm -> thm list,
       mk_cong: thm -> thm,
       mk_sym: thm -> thm option,
       mk_eq_True: thm -> thm option},
@@ -54,6 +55,7 @@
   val addsimprocs: simpset * simproc list -> simpset
   val delsimprocs: simpset * simproc list -> simpset
   val setmksimps: simpset * (thm -> thm list) -> simpset
+  val setmksimps2: simpset * (thm list -> thm -> thm list) -> simpset
   val setmkcong: simpset * (thm -> thm) -> simpset
   val setmksym: simpset * (thm -> thm option) -> simpset
   val setmkeqTrue: simpset * (thm -> thm option) -> simpset
@@ -203,6 +205,7 @@
       (functions that prove rewrite rules on the fly);
     mk_rews:
       mk: turn simplification thms into rewrite rules;
+      mk2: like mk but may also depend on the other premises
       mk_cong: prepare congruence rules;
       mk_sym: turn == around;
       mk_eq_True: turn P into P == True;
@@ -210,6 +213,7 @@
 
 type mk_rews =
  {mk: thm -> thm list,
+  mk2: thm list -> thm -> thm list,
   mk_cong: thm -> thm,
   mk_sym: thm -> thm option,
   mk_eq_True: thm -> thm option};
@@ -302,6 +306,7 @@
 
 val basic_mk_rews: mk_rews =
  {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
+  mk2 = fn thms => fn thm => [],
   mk_cong = I,
   mk_sym = Some o Drule.symmetric_fun,
   mk_eq_True = K None};
@@ -486,8 +491,11 @@
     else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
   end;
 
-fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
-  flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
+fun extract_rews (Simpset ({prems, ...}, {mk_rews = {mk, ...}, ...}), thms)
+  = flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms);
+
+fun extract_rews2 (Simpset ({prems, ...}, {mk_rews = {mk2, ...}, ...}), thms)
+  = flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk2 prems thm)) thms);
 
 fun orient_comb_simps comb mk_rrule (ss, thms) =
   let
@@ -498,11 +506,20 @@
 fun extract_safe_rrules (ss, thm) =
   flat (map (orient_rrule ss) (extract_rews (ss, [thm])));
 
+fun extract_safe_rrules2 (ss, thm) =
+  flat (map (orient_rrule ss) (extract_rews2 (ss, [thm])));
+
 (*add rewrite rules explicitly; do not reorient!*)
 fun ss addsimps thms =
   orient_comb_simps (insert_rrule false) (mk_rrule ss) (ss, thms);
 
 
+fun add_prem2(ss,thm) =
+  foldl (insert_rrule true) (ss,extract_safe_rrules2(ss,thm))
+  |> add_prems [thm];
+
+fun add_prems2 thms ss = foldl add_prem2 (ss,thms);
+
 (* delsimps *)
 
 fun del_rrule (ss, rrule as {thm, elhs, ...}) =
@@ -617,26 +634,29 @@
 
 local
 
-fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True},
+fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk2, mk_cong, mk_sym, mk_eq_True},
       termless, subgoal_tac, loop_tacs, solvers) =>
-  let val (mk', mk_cong', mk_sym', mk_eq_True') = f (mk, mk_cong, mk_sym, mk_eq_True) in
-    (congs, procs, {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'},
+  let val (mk', mk2', mk_cong', mk_sym', mk_eq_True') = f (mk, mk2, mk_cong, mk_sym, mk_eq_True) in
+    (congs, procs, {mk = mk', mk2 = mk2', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'},
       termless, subgoal_tac, loop_tacs, solvers)
   end);
 
 in
 
-fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True) =>
-  (mk, mk_cong, mk_sym, mk_eq_True));
+fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk2, mk_cong, mk_sym, mk_eq_True) =>
+  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
 
-fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True) =>
-  (mk, mk_cong, mk_sym, mk_eq_True));
+fun ss setmksimps2 mk2 = ss |> map_mk_rews (fn (mk, _, mk_cong, mk_sym, mk_eq_True) =>
+  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
 
-fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True) =>
-  (mk, mk_cong, mk_sym, mk_eq_True));
+fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, mk2, _, mk_sym, mk_eq_True) =>
+  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
 
-fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _) =>
-  (mk, mk_cong, mk_sym, mk_eq_True));
+fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk2, mk_cong, _, mk_eq_True) =>
+  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
+
+fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk2, mk_cong, mk_sym, _) =>
+  (mk, mk2, mk_cong, mk_sym, mk_eq_True));
 
 end;
 
@@ -999,7 +1019,8 @@
         in (extract_safe_rrules (ss, asm), Some asm) end
 
     and add_rrules (rrss, asms) ss =
-      foldl (insert_rrule true) (ss, flat rrss) |> add_prems (mapfilter I asms)
+      let val Asms = mapfilter I asms
+      in foldl (insert_rrule true) (ss, flat rrss) |> add_prems2 Asms end
 
     and disch r (prem, eq) =
       let