--- a/doc-src/TutorialI/Types/Numbers.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy Wed Dec 10 15:59:34 2003 +0100
@@ -206,17 +206,17 @@
@{thm[display] realpow_abs[no_vars]}
\rulename{realpow_abs}
-@{thm[display] real_times_divide1_eq[no_vars]}
-\rulename{real_times_divide1_eq}
+@{thm[display] times_divide_eq_right[no_vars]}
+\rulename{times_divide_eq_right}
-@{thm[display] real_times_divide2_eq[no_vars]}
-\rulename{real_times_divide2_eq}
+@{thm[display] times_divide_eq_left[no_vars]}
+\rulename{times_divide_eq_left}
-@{thm[display] real_divide_divide1_eq[no_vars]}
-\rulename{real_divide_divide1_eq}
+@{thm[display] divide_divide_eq_right[no_vars]}
+\rulename{divide_divide_eq_right}
-@{thm[display] real_divide_divide2_eq[no_vars]}
-\rulename{real_divide_divide2_eq}
+@{thm[display] divide_divide_eq_left[no_vars]}
+\rulename{divide_divide_eq_left}
@{thm[display] real_minus_divide_eq[no_vars]}
\rulename{real_minus_divide_eq}
--- a/doc-src/TutorialI/Types/document/Numbers.tex Wed Dec 10 14:29:44 2003 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Wed Dec 10 15:59:34 2003 +0100
@@ -335,24 +335,24 @@
\rulename{realpow_abs}
\begin{isabelle}%
-x\ {\isacharasterisk}\ {\isacharparenleft}y\ {\isacharslash}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isacharasterisk}\ y\ {\isacharslash}\ z%
+a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c%
\end{isabelle}
-\rulename{real_times_divide1_eq}
+\rulename{times_divide_eq_right}
\begin{isabelle}%
-y\ {\isacharslash}\ z\ {\isacharasterisk}\ x\ {\isacharequal}\ y\ {\isacharasterisk}\ x\ {\isacharslash}\ z%
+b\ {\isacharslash}\ c\ {\isacharasterisk}\ a\ {\isacharequal}\ b\ {\isacharasterisk}\ a\ {\isacharslash}\ c%
\end{isabelle}
-\rulename{real_times_divide2_eq}
+\rulename{times_divide_eq_left}
\begin{isabelle}%
-x\ {\isacharslash}\ {\isacharparenleft}y\ {\isacharslash}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isacharasterisk}\ z\ {\isacharslash}\ y%
+a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ c\ {\isacharslash}\ b%
\end{isabelle}
-\rulename{real_divide_divide1_eq}
+\rulename{divide_divide_eq_right}
\begin{isabelle}%
-x\ {\isacharslash}\ y\ {\isacharslash}\ z\ {\isacharequal}\ x\ {\isacharslash}\ {\isacharparenleft}y\ {\isacharasterisk}\ z{\isacharparenright}%
+a\ {\isacharslash}\ b\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}%
\end{isabelle}
-\rulename{real_divide_divide2_eq}
+\rulename{divide_divide_eq_left}
\begin{isabelle}%
{\isacharminus}\ x\ {\isacharslash}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}%
--- a/doc-src/TutorialI/Types/numerics.tex Wed Dec 10 14:29:44 2003 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Wed Dec 10 15:59:34 2003 +0100
@@ -404,14 +404,14 @@
are installed as default simplification rules in order to express
combinations of products and quotients as rational expressions:
\begin{isabelle}
-x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z
-\rulename{real_times_divide1_eq}\isanewline
-y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z
-\rulename{real_times_divide2_eq}\isanewline
-x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y
-\rulename{real_divide_divide1_eq}\isanewline
-x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)
-\rulename{real_divide_divide2_eq}
+a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c
+\rulename{times_divide_eq_right}\isanewline
+b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c
+\rulename{times_divide_eq_left}\isanewline
+a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b
+\rulename{divide_divide_eq_right}\isanewline
+a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)
+\rulename{divide_divide_eq_left}
\end{isabelle}
Signs are extracted from quotients in the hope that complementary terms can
--- a/src/HOL/Complex/ComplexArith0.ML Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Complex/ComplexArith0.ML Wed Dec 10 15:59:34 2003 +0100
@@ -5,11 +5,6 @@
Also, common factor cancellation (see e.g. HyperArith0)
*)
-Goal "x - - y = x + (y::complex)";
-by (Simp_tac 1);
-qed "real_diff_minus_eq";
-Addsimps [real_diff_minus_eq];
-
(** Division and inverse **)
Goal "0/x = (0::complex)";
--- a/src/HOL/Complex/ex/Sqrt_Script.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Complex/ex/Sqrt_Script.thy Wed Dec 10 15:59:34 2003 +0100
@@ -68,8 +68,7 @@
apply clarify
apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp)
apply (simp del: real_of_nat_mult
- add: real_divide_eq_eq prime_not_square
- real_of_nat_mult [symmetric])
+ add: divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
done
lemmas two_sqrt_irrational =
--- a/src/HOL/Hyperreal/Lim.ML Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Hyperreal/Lim.ML Wed Dec 10 15:59:34 2003 +0100
@@ -5,6 +5,8 @@
differentiation of real=>real functions
*)
+val times_divide_eq_right = thm"times_divide_eq_right";
+
fun ARITH_PROVE str = prove_goal thy str
(fn prems => [cut_facts_tac prems 1,arith_tac 1]);
@@ -1048,9 +1050,9 @@
Goal "NSDERIV f x :> D \
\ ==> NSDERIV (%x. c * f x) x :> c*D";
by (asm_full_simp_tac
- (simpset() addsimps [real_times_divide1_eq RS sym, NSDERIV_NSLIM_iff,
+ (simpset() addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff,
real_minus_mult_eq2, real_add_mult_distrib2 RS sym]
- delsimps [real_times_divide1_eq, real_mult_minus_eq2]) 1);
+ delsimps [times_divide_eq_right, real_mult_minus_eq2]) 1);
by (etac (NSLIM_const RS NSLIM_mult) 1);
qed "NSDERIV_cmult";
@@ -1061,9 +1063,9 @@
"DERIV f x :> D \
\ ==> DERIV (%x. c * f x) x :> c*D";
by (asm_full_simp_tac
- (simpset() addsimps [real_times_divide1_eq RS sym, NSDERIV_NSLIM_iff,
+ (simpset() addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff,
real_minus_mult_eq2, real_add_mult_distrib2 RS sym]
- delsimps [real_times_divide1_eq, real_mult_minus_eq2]) 1);
+ delsimps [times_divide_eq_right, real_mult_minus_eq2]) 1);
by (etac (LIM_const RS LIM_mult2) 1);
qed "DERIV_cmult";
--- a/src/HOL/Hyperreal/Series.ML Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Hyperreal/Series.ML Wed Dec 10 15:59:34 2003 +0100
@@ -431,7 +431,7 @@
simpset() addsimps [sumr_geometric ,sums_def,
real_diff_def, real_add_divide_distrib]));
by (subgoal_tac "1 / (1 + -x) = 0/(x - 1) + - 1/(x - 1)" 1);
-by (asm_full_simp_tac (simpset() addsimps [real_divide_eq_cancel1,
+by (asm_full_simp_tac (simpset() addsimps [
real_divide_minus_eq RS sym, real_diff_def]) 2);
by (etac ssubst 1);
by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_divide 1);
--- a/src/HOL/Hyperreal/Transcendental.ML Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Hyperreal/Transcendental.ML Wed Dec 10 15:59:34 2003 +0100
@@ -12,6 +12,8 @@
res_inst_tac [("z",x)] cancel_thm i
end;
+val mult_less_cancel_left = thm"mult_less_cancel_left";
+
Goalw [root_def] "root (Suc n) 0 = 0";
by (safe_tac (claset() addSIs [some_equality,realpow_zero]
addSEs [realpow_zero_zero]));
@@ -285,24 +287,24 @@
by (Step_tac 1);
by (cut_inst_tac [("x","r")] reals_Archimedean3 1);
by Auto_tac;
-by (dres_inst_tac [("x","abs x")] spec 1 THEN Step_tac 1);
+by (dres_inst_tac [("x","abs x")] spec 1 THEN Safe_tac);
by (res_inst_tac [("N","n"),("c","r")] ratio_test 1);
by (auto_tac (claset(),simpset() addsimps [abs_mult,real_mult_assoc RS sym]
delsimps [fact_Suc]));
by (rtac real_mult_le_le_mono2 1);
-by (res_inst_tac [("w1","abs x")] (real_mult_commute RS ssubst) 2);
+by (res_inst_tac [("b1","abs x")] (mult_commute RS ssubst) 2);
by (stac fact_Suc 2);
by (stac real_of_nat_mult 2);
by (auto_tac (claset(),simpset() addsimps [abs_mult,real_inverse_distrib]));
by (auto_tac (claset(), simpset() addsimps
- [real_mult_assoc RS sym, abs_eqI2, real_inverse_gt_0]));
-by (rtac (CLAIM "x < (y::real) ==> x <= y") 1);
+ [mult_assoc RS sym, abs_eqI2, real_inverse_gt_0]));
+by (rtac order_less_imp_le 1);
by (res_inst_tac [("z1","real (Suc na)")] (real_mult_less_iff1
RS iffD1) 1);
by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym,
- real_mult_assoc,abs_inverse]));
-by (rtac real_less_trans 1);
-by (auto_tac (claset(),simpset() addsimps real_mult_ac));
+ mult_assoc,abs_inverse]));
+by (etac order_less_trans 1);
+by (auto_tac (claset(),simpset() addsimps [mult_less_cancel_left]@mult_ac));
qed "summable_exp";
Addsimps [real_of_nat_fact_gt_zero,
@@ -636,9 +638,10 @@
by (res_inst_tac [("R2.0","K * e")] real_less_trans 2);
by (res_inst_tac [("z","inverse K")] (CLAIM_SIMP
"[|(0::real) <z; z*x<z*y |] ==> x<y" [real_mult_less_cancel1]) 3);
-by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 4);
-by Auto_tac;
-by (auto_tac (claset(),simpset() addsimps real_mult_ac));
+by (asm_full_simp_tac (simpset() addsimps [mult_assoc RS sym]) 4);
+by (Force_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [mult_less_cancel_left]) 1);
+by (auto_tac (claset(),simpset() addsimps mult_ac));
qed "lemma_termdiff4";
Goal "[| 0 < k; \
@@ -1577,11 +1580,12 @@
by (etac sums_summable 1);
by (case_tac "m=0" 1);
by (Asm_simp_tac 1);
-by (res_inst_tac [("z","real (Suc (Suc (Suc (Suc 2))))")]
- (CLAIM "[|(0::real)<z; z*x<z*y |] ==> x<y") 1);
-by (asm_simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym, real_mult_assoc RS sym]) 2);
-by (stac (CLAIM "6 = 2 * (3::real)") 2);
-by (rtac real_mult_less_mono 2);
+by (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x" 1);
+by (asm_full_simp_tac (HOL_ss addsimps [mult_less_cancel_left]) 1);
+by (asm_full_simp_tac (simpset() addsimps []) 1);
+by (asm_simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym, real_mult_assoc RS sym]) 1);
+by (stac (CLAIM "6 = 2 * (3::real)") 1);
+by (rtac real_mult_less_mono 1);
by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc] delsimps [fact_Suc]));
by (stac fact_Suc 1);
by (stac fact_Suc 1);
@@ -1599,13 +1603,14 @@
by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]
delsimps [fact_Suc]));
by (multr_by_tac "real (Suc (Suc (Suc (4*m))))" 1);
-by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]
+by (auto_tac (claset(),simpset() addsimps [mult_assoc,mult_less_cancel_left]
delsimps [fact_Suc]));
-by (auto_tac (claset(),simpset() addsimps [CLAIM
- "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * (x::real))"]
+by (auto_tac (claset(),simpset() addsimps [
+ CLAIM "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * (x::real))"]
delsimps [fact_Suc]));
-by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,realpow_gt_zero]
- delsimps [fact_Suc]));
+by (subgoal_tac "0 < x ^ (4 * m)" 1);
+by (asm_simp_tac (simpset() addsimps [realpow_gt_zero]) 2);
+by (asm_simp_tac (simpset() addsimps [mult_less_cancel_left]) 1);
by (rtac real_mult_less_mono 1);
by (ALLGOALS(Asm_simp_tac));
by (TRYALL(rtac real_less_trans));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/BinaryTree.thy Wed Dec 10 15:59:34 2003 +0100
@@ -0,0 +1,795 @@
+header {* Isar-style Reasoning for Binary Tree Operations *}
+theory BinaryTree = Main:
+
+text {* We prove correctness of operations on
+ binary search tree implementing a set.
+
+ This document is GPL.
+
+ Author: Viktor Kuncak, MIT CSAIL, November 2003 *}
+
+(*============================================================*)
+section {* Tree Definition *}
+(*============================================================*)
+
+datatype 'a Tree = Tip | T "'a Tree" 'a "'a Tree"
+
+consts
+ setOf :: "'a Tree => 'a set"
+ -- {* set abstraction of a tree *}
+primrec
+"setOf Tip = {}"
+"setOf (T t1 x t2) = (setOf t1) Un (setOf t2) Un {x}"
+
+types
+ -- {* we require index to have an irreflexive total order < *}
+ -- {* apart from that, we do not rely on index being int *}
+ index = int
+
+types -- {* hash function type *}
+ 'a hash = "'a => index"
+
+constdefs
+ eqs :: "'a hash => 'a => 'a set"
+ -- {* equivalence class of elements with the same hash code *}
+ "eqs h x == {y. h y = h x}"
+
+consts
+ sortedTree :: "'a hash => 'a Tree => bool"
+ -- {* check if a tree is sorted *}
+primrec
+"sortedTree h Tip = True"
+"sortedTree h (T t1 x t2) =
+ (sortedTree h t1 &
+ (ALL l: setOf t1. h l < h x) &
+ (ALL r: setOf t2. h x < h r) &
+ sortedTree h t2)"
+
+lemma sortLemmaL:
+ "sortedTree h (T t1 x t2) ==> sortedTree h t1" by simp
+lemma sortLemmaR:
+ "sortedTree h (T t1 x t2) ==> sortedTree h t2" by simp
+
+(*============================================================*)
+section {* Tree Lookup *}
+(*============================================================*)
+
+consts
+ tlookup :: "'a hash => index => 'a Tree => 'a option"
+primrec
+"tlookup h k Tip = None"
+"tlookup h k (T t1 x t2) =
+ (if k < h x then tlookup h k t1
+ else if h x < k then tlookup h k t2
+ else Some x)"
+
+lemma tlookup_none:
+"sortedTree h t & (tlookup h k t = None) -->
+ (ALL x:setOf t. h x ~= k)"
+apply (induct t)
+apply auto (* takes some time *)
+done
+
+lemma tlookup_some:
+"sortedTree h t & (tlookup h k t = Some x) -->
+ x:setOf t & h x = k"
+apply (induct t)
+apply auto (* takes some time *)
+done
+
+constdefs
+ sorted_distinct_pred :: "'a hash => 'a => 'a => 'a Tree => bool"
+ -- {* No two elements have the same hash code *}
+ "sorted_distinct_pred h a b t == sortedTree h t &
+ a:setOf t & b:setOf t & h a = h b -->
+ a = b"
+
+declare sorted_distinct_pred_def [simp]
+
+-- {* for case analysis on three cases *}
+lemma cases3: "[| C1 ==> G; C2 ==> G; C3 ==> G;
+ C1 | C2 | C3 |] ==> G"
+by auto
+
+text {* @{term sorted_distinct_pred} holds for out trees: *}
+
+lemma sorted_distinct: "sorted_distinct_pred h a b t" (is "?P t")
+proof (induct t)
+ show "?P Tip" by simp
+ fix t1 :: "'a Tree" assume h1: "?P t1"
+ fix t2 :: "'a Tree" assume h2: "?P t2"
+ fix x :: 'a
+ show "?P (T t1 x t2)"
+ proof (unfold sorted_distinct_pred_def, safe)
+ assume s: "sortedTree h (T t1 x t2)"
+ assume adef: "a : setOf (T t1 x t2)"
+ assume bdef: "b : setOf (T t1 x t2)"
+ assume hahb: "h a = h b"
+ from s have s1: "sortedTree h t1" by auto
+ from s have s2: "sortedTree h t2" by auto
+ show "a = b"
+ -- {* We consider 9 cases for the position of a and b are in the tree *}
+ proof -
+ -- {* three cases for a *}
+ from adef have "a : setOf t1 | a = x | a : setOf t2" by auto
+ moreover { assume adef1: "a : setOf t1"
+ have ?thesis
+ proof -
+ -- {* three cases for b *}
+ from bdef have "b : setOf t1 | b = x | b : setOf t2" by auto
+ moreover { assume bdef1: "b : setOf t1"
+ from s1 adef1 bdef1 hahb h1 have ?thesis by simp }
+ moreover { assume bdef1: "b = x"
+ from adef1 bdef1 s have "h a < h b" by auto
+ from this hahb have ?thesis by simp }
+ moreover { assume bdef1: "b : setOf t2"
+ from adef1 s have o1: "h a < h x" by auto
+ from bdef1 s have o2: "h x < h b" by auto
+ from o1 o2 have "h a < h b" by simp
+ from this hahb have ?thesis by simp } -- {* case impossible *}
+ ultimately show ?thesis by blast
+ qed
+ }
+ moreover { assume adef1: "a = x"
+ have ?thesis
+ proof -
+ -- {* three cases for b *}
+ from bdef have "b : setOf t1 | b = x | b : setOf t2" by auto
+ moreover { assume bdef1: "b : setOf t1"
+ from this s have "h b < h x" by auto
+ from this adef1 have "h b < h a" by auto
+ from hahb this have ?thesis by simp } -- {* case impossible *}
+ moreover { assume bdef1: "b = x"
+ from adef1 bdef1 have ?thesis by simp }
+ moreover { assume bdef1: "b : setOf t2"
+ from this s have "h x < h b" by auto
+ from this adef1 have "h a < h b" by simp
+ from hahb this have ?thesis by simp } -- {* case impossible *}
+ ultimately show ?thesis by blast
+ qed
+ }
+ moreover { assume adef1: "a : setOf t2"
+ have ?thesis
+ proof -
+ -- {* three cases for b *}
+ from bdef have "b : setOf t1 | b = x | b : setOf t2" by auto
+ moreover { assume bdef1: "b : setOf t1"
+ from bdef1 s have o1: "h b < h x" by auto
+ from adef1 s have o2: "h x < h a" by auto
+ from o1 o2 have "h b < h a" by simp
+ from this hahb have ?thesis by simp } -- {* case impossible *}
+ moreover { assume bdef1: "b = x"
+ from adef1 bdef1 s have "h b < h a" by auto
+ from this hahb have ?thesis by simp } -- {* case impossible *}
+ moreover { assume bdef1: "b : setOf t2"
+ from s2 adef1 bdef1 hahb h2 have ?thesis by simp }
+ ultimately show ?thesis by blast
+ qed
+ }
+ ultimately show ?thesis by blast
+ qed
+ qed
+qed
+
+lemma tlookup_finds: -- {* if a node is in the tree, lookup finds it *}
+"sortedTree h t & y:setOf t -->
+ tlookup h (h y) t = Some y"
+proof safe
+ assume s: "sortedTree h t"
+ assume yint: "y : setOf t"
+ show "tlookup h (h y) t = Some y"
+ proof (cases "tlookup h (h y) t")
+ case None note res = this
+ from s res have "sortedTree h t & (tlookup h (h y) t = None)" by simp
+ from this have o1: "ALL x:setOf t. h x ~= h y" by (simp add: tlookup_none)
+ from o1 yint have "h y ~= h y" by fastsimp (* auto does not work *)
+ from this show ?thesis by simp
+ next case (Some z) note res = this
+ have ls: "sortedTree h t & (tlookup h (h y) t = Some z) -->
+ z:setOf t & h z = h y" by (simp add: tlookup_some)
+ have sd: "sorted_distinct_pred h y z t"
+ by (insert sorted_distinct [of h y z t], simp)
+ (* for some reason simplifier would never guess this substitution *)
+ from s res ls have o1: "z:setOf t & h z = h y" by simp
+ from s yint o1 sd have "y = z" by auto
+ from this res show "tlookup h (h y) t = Some y" by simp
+ qed
+qed
+
+subsection {* Tree membership as a special case of lookup *}
+
+constdefs
+ memb :: "'a hash => 'a => 'a Tree => bool"
+ "memb h x t ==
+ (case (tlookup h (h x) t) of
+ None => False
+ | Some z => (x=z))"
+
+lemma assumes s: "sortedTree h t"
+ shows memb_spec: "memb h x t = (x : setOf t)"
+proof (cases "tlookup h (h x) t")
+case None note tNone = this
+ from tNone have res: "memb h x t = False" by (simp add: memb_def)
+ from s tNone tlookup_none have o1: "ALL y:setOf t. h y ~= h x" by fastsimp
+ have notIn: "x ~: setOf t"
+ proof
+ assume h: "x : setOf t"
+ from h o1 have "h x ~= h x" by fastsimp
+ from this show False by simp
+ qed
+ from res notIn show ?thesis by simp
+next case (Some z) note tSome = this
+ from s tSome tlookup_some have zin: "z : setOf t" by fastsimp
+ show ?thesis
+ proof (cases "x=z")
+ case True note xez = this
+ from tSome xez have res: "memb h x t" by (simp add: memb_def)
+ from res zin xez show ?thesis by simp
+ next case False note xnez = this
+ from tSome xnez have res: "~ memb h x t" by (simp add: memb_def)
+ have "x ~: setOf t"
+ proof
+ assume xin: "x : setOf t"
+ from s tSome tlookup_some have hzhx: "h x = h z" by fastsimp
+ have o1: "sorted_distinct_pred h x z t"
+ by (insert sorted_distinct [of h x z t], simp)
+ from s xin zin hzhx o1 have "x = z" by fastsimp
+ from this xnez show False by simp
+ qed
+ from this res show ?thesis by simp
+ qed
+qed
+
+declare sorted_distinct_pred_def [simp del]
+
+(*============================================================*)
+section {* Insertion into a Tree *}
+(*============================================================*)
+
+consts
+ binsert :: "'a hash => 'a => 'a Tree => 'a Tree"
+
+primrec
+"binsert h e Tip = (T Tip e Tip)"
+"binsert h e (T t1 x t2) = (if h e < h x then
+ (T (binsert h e t1) x t2)
+ else
+ (if h x < h e then
+ (T t1 x (binsert h e t2))
+ else (T t1 e t2)))"
+
+text {* A technique for proving disjointness of sets. *}
+lemma disjCond: "[| !! x. [| x:A; x:B |] ==> False |] ==> A Int B = {}"
+by fastsimp
+
+text {* The following is a proof that insertion correctly implements
+ the set interface.
+ Compared to @{text BinaryTree_TacticStyle}, the claim is more
+ difficult, and this time we need to assume as a hypothesis
+ that the tree is sorted. *}
+
+lemma binsert_set: "sortedTree h t -->
+ setOf (binsert h e t) = (setOf t) - (eqs h e) Un {e}"
+ (is "?P t")
+proof (induct t)
+ -- {* base case *}
+ show "?P Tip" by (simp add: eqs_def)
+ -- {* inductition step *}
+ fix t1 :: "'a Tree" assume h1: "?P t1"
+ fix t2 :: "'a Tree" assume h2: "?P t2"
+ fix x :: 'a
+ show "?P (T t1 x t2)"
+ proof
+ assume s: "sortedTree h (T t1 x t2)"
+ from s have s1: "sortedTree h t1" by (rule sortLemmaL)
+ from s1 and h1 have c1: "setOf (binsert h e t1) = setOf t1 - eqs h e Un {e}" by simp
+ from s have s2: "sortedTree h t2" by (rule sortLemmaR)
+ from s2 and h2 have c2: "setOf (binsert h e t2) = setOf t2 - eqs h e Un {e}" by simp
+ show "setOf (binsert h e (T t1 x t2)) =
+ setOf (T t1 x t2) - eqs h e Un {e}"
+ proof (cases "h e < h x")
+ case True note eLess = this
+ from eLess have res: "binsert h e (T t1 x t2) = (T (binsert h e t1) x t2)" by simp
+ show "setOf (binsert h e (T t1 x t2)) =
+ setOf (T t1 x t2) - eqs h e Un {e}"
+ proof (simp add: res eLess c1)
+ show "insert x (insert e (setOf t1 - eqs h e Un setOf t2)) =
+ insert e (insert x (setOf t1 Un setOf t2) - eqs h e)"
+ proof -
+ have eqsLessX: "ALL el: eqs h e. h el < h x" by (simp add: eqs_def eLess)
+ from this have eqsDisjX: "ALL el: eqs h e. h el ~= h x" by fastsimp
+ from s have xLessT2: "ALL r: setOf t2. h x < h r" by auto
+ have eqsLessT2: "ALL el: eqs h e. ALL r: setOf t2. h el < h r"
+ proof safe
+ fix el assume hel: "el : eqs h e"
+ from hel eqs_def have o1: "h el = h e" by fastsimp (* auto fails here! *)
+ fix r assume hr: "r : setOf t2"
+ from xLessT2 hr o1 eLess show "h el < h r" by auto
+ qed
+ from eqsLessT2 have eqsDisjT2: "ALL el: eqs h e. ALL r: setOf t2. h el ~= h r"
+ by fastsimp (* auto fails here *)
+ from eqsDisjX eqsDisjT2 show ?thesis by fastsimp
+ qed
+ qed
+ next case False note eNotLess = this
+ show "setOf (binsert h e (T t1 x t2)) = setOf (T t1 x t2) - eqs h e Un {e}"
+ proof (cases "h x < h e")
+ case True note xLess = this
+ from xLess have res: "binsert h e (T t1 x t2) = (T t1 x (binsert h e t2))" by simp
+ show "setOf (binsert h e (T t1 x t2)) =
+ setOf (T t1 x t2) - eqs h e Un {e}"
+ proof (simp add: res xLess eNotLess c2)
+ show "insert x (insert e (setOf t1 Un (setOf t2 - eqs h e))) =
+ insert e (insert x (setOf t1 Un setOf t2) - eqs h e)"
+ proof -
+ have XLessEqs: "ALL el: eqs h e. h x < h el" by (simp add: eqs_def xLess)
+ from this have eqsDisjX: "ALL el: eqs h e. h el ~= h x" by auto
+ from s have t1LessX: "ALL l: setOf t1. h l < h x" by auto
+ have T1lessEqs: "ALL el: eqs h e. ALL l: setOf t1. h l < h el"
+ proof safe
+ fix el assume hel: "el : eqs h e"
+ fix l assume hl: "l : setOf t1"
+ from hel eqs_def have o1: "h el = h e" by fastsimp (* auto fails here! *)
+ from t1LessX hl o1 xLess show "h l < h el" by auto
+ qed
+ from T1lessEqs have T1disjEqs: "ALL el: eqs h e. ALL l: setOf t1. h el ~= h l"
+ by fastsimp
+ from eqsDisjX T1lessEqs show ?thesis by auto
+ qed
+ qed
+ next case False note xNotLess = this
+ from xNotLess eNotLess have xeqe: "h x = h e" by simp
+ from xeqe have res: "binsert h e (T t1 x t2) = (T t1 e t2)" by simp
+ show "setOf (binsert h e (T t1 x t2)) =
+ setOf (T t1 x t2) - eqs h e Un {e}"
+ proof (simp add: res eNotLess xeqe)
+ show "insert e (setOf t1 Un setOf t2) =
+ insert e (insert x (setOf t1 Un setOf t2) - eqs h e)"
+ proof -
+ have "insert x (setOf t1 Un setOf t2) - eqs h e =
+ setOf t1 Un setOf t2"
+ proof -
+ have (* o1: *) "x : eqs h e" by (simp add: eqs_def xeqe)
+ moreover have (* o2: *) "(setOf t1) Int (eqs h e) = {}"
+ proof (rule disjCond)
+ fix w
+ assume whSet: "w : setOf t1"
+ assume whEq: "w : eqs h e"
+ from whSet s have o1: "h w < h x" by simp
+ from whEq eqs_def have o2: "h w = h e" by fastsimp
+ from o2 xeqe have o3: "~ h w < h x" by simp
+ from o1 o3 show False by contradiction
+ qed
+ moreover have (* o3: *) "(setOf t2) Int (eqs h e) = {}"
+ proof (rule disjCond)
+ fix w
+ assume whSet: "w : setOf t2"
+ assume whEq: "w : eqs h e"
+ from whSet s have o1: "h x < h w" by simp
+ from whEq eqs_def have o2: "h w = h e" by fastsimp
+ from o2 xeqe have o3: "~ h x < h w" by simp
+ from o1 o3 show False by contradiction
+ qed
+ ultimately show ?thesis by auto
+ qed
+ from this show ?thesis by simp
+ qed
+ qed
+ qed
+ qed
+ qed
+qed
+
+text {* Using the correctness of set implementation,
+ preserving sortedness is still simple. *}
+lemma binsert_sorted: "sortedTree h t --> sortedTree h (binsert h x t)"
+by (induct t) (auto simp add: binsert_set)
+
+text {* We summarize the specification of binsert as follows. *}
+corollary binsert_spec: "sortedTree h t -->
+ sortedTree h (binsert h x t) &
+ setOf (binsert h e t) = (setOf t) - (eqs h e) Un {e}"
+by (simp add: binsert_set binsert_sorted)
+
+(*============================================================*)
+section {* Removing an element from a tree *}
+(*============================================================*)
+
+text {* These proofs are influenced by those in @{text BinaryTree_Tactic} *}
+
+consts
+ rm :: "'a hash => 'a Tree => 'a"
+ -- {* rightmost element of a tree *}
+primrec
+"rm h (T t1 x t2) =
+ (if t2=Tip then x else rm h t2)"
+
+consts
+ wrm :: "'a hash => 'a Tree => 'a Tree"
+ -- {* tree without the rightmost element *}
+primrec
+"wrm h (T t1 x t2) =
+ (if t2=Tip then t1 else (T t1 x (wrm h t2)))"
+
+consts
+ wrmrm :: "'a hash => 'a Tree => 'a Tree * 'a"
+ -- {* computing rightmost and removal in one pass *}
+primrec
+"wrmrm h (T t1 x t2) =
+ (if t2=Tip then (t1,x)
+ else (T t1 x (fst (wrmrm h t2)),
+ snd (wrmrm h t2)))"
+
+consts
+ remove :: "'a hash => 'a => 'a Tree => 'a Tree"
+ -- {* removal of an element from the tree *}
+primrec
+"remove h e Tip = Tip"
+"remove h e (T t1 x t2) =
+ (if h e < h x then (T (remove h e t1) x t2)
+ else if h x < h e then (T t1 x (remove h e t2))
+ else (if t1=Tip then t2
+ else let (t1p,r) = wrmrm h t1
+ in (T t1p r t2)))"
+
+theorem wrmrm_decomp: "t ~= Tip --> wrmrm h t = (wrm h t, rm h t)"
+apply (induct_tac t)
+apply simp_all
+done
+
+lemma rm_set: "t ~= Tip & sortedTree h t --> rm h t : setOf t"
+apply (induct_tac t)
+apply simp_all
+done
+
+lemma wrm_set: "t ~= Tip & sortedTree h t -->
+ setOf (wrm h t) = setOf t - {rm h t}" (is "?P t")
+proof (induct t)
+ show "?P Tip" by simp
+ fix t1 :: "'a Tree" assume h1: "?P t1"
+ fix t2 :: "'a Tree" assume h2: "?P t2"
+ fix x :: 'a
+ show "?P (T t1 x t2)"
+ proof (rule impI, erule conjE)
+ assume s: "sortedTree h (T t1 x t2)"
+ show "setOf (wrm h (T t1 x t2)) =
+ setOf (T t1 x t2) - {rm h (T t1 x t2)}"
+ proof (cases "t2 = Tip")
+ case True note t2tip = this
+ from t2tip have rm_res: "rm h (T t1 x t2) = x" by simp
+ from t2tip have wrm_res: "wrm h (T t1 x t2) = t1" by simp
+ from s have "x ~: setOf t1" by auto
+ from this rm_res wrm_res t2tip show ?thesis by simp
+ next case False note t2nTip = this
+ from t2nTip have rm_res: "rm h (T t1 x t2) = rm h t2" by simp
+ from t2nTip have wrm_res: "wrm h (T t1 x t2) = T t1 x (wrm h t2)" by simp
+ from s have s2: "sortedTree h t2" by simp
+ from h2 t2nTip s2
+ have o1: "setOf (wrm h t2) = setOf t2 - {rm h t2}" by simp
+ show ?thesis
+ proof (simp add: rm_res wrm_res t2nTip h2 o1)
+ show "insert x (setOf t1 Un (setOf t2 - {rm h t2})) =
+ insert x (setOf t1 Un setOf t2) - {rm h t2}"
+ proof -
+ from s rm_set t2nTip have xOk: "h x < h (rm h t2)" by auto
+ have t1Ok: "ALL l:setOf t1. h l < h (rm h t2)"
+ proof safe
+ fix l :: 'a assume ldef: "l : setOf t1"
+ from ldef s have lx: "h l < h x" by auto
+ from lx xOk show "h l < h (rm h t2)" by auto
+ qed
+ from xOk t1Ok show ?thesis by auto
+ qed
+ qed
+ qed
+ qed
+qed
+
+lemma wrm_set1: "t ~= Tip & sortedTree h t --> setOf (wrm h t) <= setOf t"
+by (auto simp add: wrm_set)
+
+lemma wrm_sort: "t ~= Tip & sortedTree h t --> sortedTree h (wrm h t)" (is "?P t")
+proof (induct t)
+ show "?P Tip" by simp
+ fix t1 :: "'a Tree" assume h1: "?P t1"
+ fix t2 :: "'a Tree" assume h2: "?P t2"
+ fix x :: 'a
+ show "?P (T t1 x t2)"
+ proof safe
+ assume s: "sortedTree h (T t1 x t2)"
+ show "sortedTree h (wrm h (T t1 x t2))"
+ proof (cases "t2 = Tip")
+ case True note t2tip = this
+ from t2tip have res: "wrm h (T t1 x t2) = t1" by simp
+ from res s show ?thesis by simp
+ next case False note t2nTip = this
+ from t2nTip have res: "wrm h (T t1 x t2) = T t1 x (wrm h t2)" by simp
+ from s have s1: "sortedTree h t1" by simp
+ from s have s2: "sortedTree h t2" by simp
+ from s2 h2 t2nTip have o1: "sortedTree h (wrm h t2)" by simp
+ from s2 t2nTip wrm_set1 have o2: "setOf (wrm h t2) <= setOf t2" by auto
+ from s o2 have o3: "ALL r: setOf (wrm h t2). h x < h r" by auto
+ from s1 o1 o3 res s show "sortedTree h (wrm h (T t1 x t2))" by simp
+ qed
+ qed
+qed
+
+lemma wrm_less_rm:
+ "t ~= Tip & sortedTree h t -->
+ (ALL l:setOf (wrm h t). h l < h (rm h t))" (is "?P t")
+proof (induct t)
+ show "?P Tip" by simp
+ fix t1 :: "'a Tree" assume h1: "?P t1"
+ fix t2 :: "'a Tree" assume h2: "?P t2"
+ fix x :: 'a
+ show "?P (T t1 x t2)"
+ proof safe
+ fix l :: "'a" assume ldef: "l : setOf (wrm h (T t1 x t2))"
+ assume s: "sortedTree h (T t1 x t2)"
+ from s have s1: "sortedTree h t1" by simp
+ from s have s2: "sortedTree h t2" by simp
+ show "h l < h (rm h (T t1 x t2))"
+ proof (cases "t2 = Tip")
+ case True note t2tip = this
+ from t2tip have rm_res: "rm h (T t1 x t2) = x" by simp
+ from t2tip have wrm_res: "wrm h (T t1 x t2) = t1" by simp
+ from ldef wrm_res have o1: "l : setOf t1" by simp
+ from rm_res o1 s show ?thesis by simp
+ next case False note t2nTip = this
+ from t2nTip have rm_res: "rm h (T t1 x t2) = rm h t2" by simp
+ from t2nTip have wrm_res: "wrm h (T t1 x t2) = T t1 x (wrm h t2)" by simp
+ from ldef wrm_res
+ have l_scope: "l : {x} Un setOf t1 Un setOf (wrm h t2)" by simp
+ have hLess: "h l < h (rm h t2)"
+ proof (cases "l = x")
+ case True note lx = this
+ from s t2nTip rm_set s2 have o1: "h x < h (rm h t2)" by auto
+ from lx o1 show ?thesis by simp
+ next case False note lnx = this
+ show ?thesis
+ proof (cases "l : setOf t1")
+ case True note l_in_t1 = this
+ from s t2nTip rm_set s2 have o1: "h x < h (rm h t2)" by auto
+ from l_in_t1 s have o2: "h l < h x" by auto
+ from o1 o2 show ?thesis by simp
+ next case False note l_notin_t1 = this
+ from l_scope lnx l_notin_t1
+ have l_in_res: "l : setOf (wrm h t2)" by auto
+ from l_in_res h2 t2nTip s2 show ?thesis by auto
+ qed
+ qed
+ from rm_res hLess show ?thesis by simp
+ qed
+ qed
+qed
+
+lemma remove_set: "sortedTree h t -->
+ setOf (remove h e t) = setOf t - eqs h e" (is "?P t")
+proof (induct t)
+ show "?P Tip" by auto
+ fix t1 :: "'a Tree" assume h1: "?P t1"
+ fix t2 :: "'a Tree" assume h2: "?P t2"
+ fix x :: 'a
+ show "?P (T t1 x t2)"
+ proof
+ assume s: "sortedTree h (T t1 x t2)"
+ show "setOf (remove h e (T t1 x t2)) = setOf (T t1 x t2) - eqs h e"
+ proof (cases "h e < h x")
+ case True note elx = this
+ from elx have res: "remove h e (T t1 x t2) = T (remove h e t1) x t2"
+ by simp
+ from s have s1: "sortedTree h t1" by simp
+ from s1 h1 have o1: "setOf (remove h e t1) = setOf t1 - eqs h e" by simp
+ show ?thesis
+ proof (simp add: o1 elx)
+ show "insert x (setOf t1 - eqs h e Un setOf t2) =
+ insert x (setOf t1 Un setOf t2) - eqs h e"
+ proof -
+ have xOk: "x ~: eqs h e"
+ proof
+ assume h: "x : eqs h e"
+ from h have o1: "~ (h e < h x)" by (simp add: eqs_def)
+ from elx o1 show "False" by contradiction
+ qed
+ have t2Ok: "(setOf t2) Int (eqs h e) = {}"
+ proof (rule disjCond)
+ fix y :: 'a
+ assume y_in_t2: "y : setOf t2"
+ assume y_in_eq: "y : eqs h e"
+ from y_in_t2 s have xly: "h x < h y" by auto
+ from y_in_eq have eey: "h y = h e" by (simp add: eqs_def) (* must "add:" not "from" *)
+ from xly eey have nelx: "~ (h e < h x)" by simp
+ from nelx elx show False by contradiction
+ qed
+ from xOk t2Ok show ?thesis by auto
+ qed
+ qed
+ next case False note nelx = this
+ show ?thesis
+ proof (cases "h x < h e")
+ case True note xle = this
+ from xle have res: "remove h e (T t1 x t2) = T t1 x (remove h e t2)" by simp
+ from s have s2: "sortedTree h t2" by simp
+ from s2 h2 have o1: "setOf (remove h e t2) = setOf t2 - eqs h e" by simp
+ show ?thesis
+ proof (simp add: o1 xle nelx)
+ show "insert x (setOf t1 Un (setOf t2 - eqs h e)) =
+ insert x (setOf t1 Un setOf t2) - eqs h e"
+ proof -
+ have xOk: "x ~: eqs h e"
+ proof
+ assume h: "x : eqs h e"
+ from h have o1: "~ (h x < h e)" by (simp add: eqs_def)
+ from xle o1 show "False" by contradiction
+ qed
+ have t1Ok: "(setOf t1) Int (eqs h e) = {}"
+ proof (rule disjCond)
+ fix y :: 'a
+ assume y_in_t1: "y : setOf t1"
+ assume y_in_eq: "y : eqs h e"
+ from y_in_t1 s have ylx: "h y < h x" by auto
+ from y_in_eq have eey: "h y = h e" by (simp add: eqs_def)
+ from ylx eey have nxle: "~ (h x < h e)" by simp
+ from nxle xle show False by contradiction
+ qed
+ from xOk t1Ok show ?thesis by auto
+ qed
+ qed
+ next case False note nxle = this
+ from nelx nxle have ex: "h e = h x" by simp
+ have t2Ok: "(setOf t2) Int (eqs h e) = {}"
+ proof (rule disjCond)
+ fix y :: 'a
+ assume y_in_t2: "y : setOf t2"
+ assume y_in_eq: "y : eqs h e"
+ from y_in_t2 s have xly: "h x < h y" by auto
+ from y_in_eq have eey: "h y = h e" by (simp add: eqs_def)
+ from y_in_eq ex eey have nxly: "~ (h x < h y)" by simp
+ from nxly xly show False by contradiction
+ qed
+ show ?thesis
+ proof (cases "t1 = Tip")
+ case True note t1tip = this
+ from ex t1tip have res: "remove h e (T t1 x t2) = t2" by simp
+ show ?thesis
+ proof (simp add: res t1tip ex)
+ show "setOf t2 = insert x (setOf t2) - eqs h e"
+ proof -
+ from ex have x_in_eqs: "x : eqs h e" by (simp add: eqs_def)
+ from x_in_eqs t2Ok show ?thesis by auto
+ qed
+ qed
+ next case False note t1nTip = this
+ from nelx nxle ex t1nTip
+ have res: "remove h e (T t1 x t2) =
+ T (wrm h t1) (rm h t1) t2"
+ by (simp add: Let_def wrmrm_decomp)
+ from res show ?thesis
+ proof simp
+ from s have s1: "sortedTree h t1" by simp
+ show "insert (rm h t1) (setOf (wrm h t1) Un setOf t2) =
+ insert x (setOf t1 Un setOf t2) - eqs h e"
+ proof (simp add: t1nTip s1 rm_set wrm_set)
+ show "insert (rm h t1) (setOf t1 - {rm h t1} Un setOf t2) =
+ insert x (setOf t1 Un setOf t2) - eqs h e"
+ proof -
+ from t1nTip s1 rm_set
+ have o1: "insert (rm h t1) (setOf t1 - {rm h t1} Un setOf t2) =
+ setOf t1 Un setOf t2" by auto
+ have o2: "insert x (setOf t1 Un setOf t2) - eqs h e =
+ setOf t1 Un setOf t2"
+ proof -
+ from ex have xOk: "x : eqs h e" by (simp add: eqs_def)
+ have t1Ok: "(setOf t1) Int (eqs h e) = {}"
+ proof (rule disjCond)
+ fix y :: 'a
+ assume y_in_t1: "y : setOf t1"
+ assume y_in_eq: "y : eqs h e"
+ from y_in_t1 s ex have o1: "h y < h e" by auto
+ from y_in_eq have o2: "~ (h y < h e)" by (simp add: eqs_def)
+ from o1 o2 show False by contradiction
+ qed
+ from xOk t1Ok t2Ok show ?thesis by auto
+ qed
+ from o1 o2 show ?thesis by simp
+ qed
+ qed
+ qed
+ qed
+ qed
+ qed
+ qed
+qed
+
+lemma remove_sort: "sortedTree h t -->
+ sortedTree h (remove h e t)" (is "?P t")
+proof (induct t)
+ show "?P Tip" by auto
+ fix t1 :: "'a Tree" assume h1: "?P t1"
+ fix t2 :: "'a Tree" assume h2: "?P t2"
+ fix x :: 'a
+ show "?P (T t1 x t2)"
+ proof
+ assume s: "sortedTree h (T t1 x t2)"
+ from s have s1: "sortedTree h t1" by simp
+ from s have s2: "sortedTree h t2" by simp
+ from h1 s1 have sr1: "sortedTree h (remove h e t1)" by simp
+ from h2 s2 have sr2: "sortedTree h (remove h e t2)" by simp
+ show "sortedTree h (remove h e (T t1 x t2))"
+ proof (cases "h e < h x")
+ case True note elx = this
+ from elx have res: "remove h e (T t1 x t2) = T (remove h e t1) x t2"
+ by simp
+ show ?thesis
+ proof (simp add: s sr1 s2 elx res)
+ let ?C1 = "ALL l:setOf (remove h e t1). h l < h x"
+ let ?C2 = "ALL r:setOf t2. h x < h r"
+ have o1: "?C1"
+ proof -
+ from s1 have "setOf (remove h e t1) = setOf t1 - eqs h e" by (simp add: remove_set)
+ from s this show ?thesis by auto
+ qed
+ from o1 s show "?C1 & ?C2" by auto
+ qed
+ next case False note nelx = this
+ show ?thesis
+ proof (cases "h x < h e")
+ case True note xle = this
+ from xle have res: "remove h e (T t1 x t2) = T t1 x (remove h e t2)" by simp
+ show ?thesis
+ proof (simp add: s s1 sr2 xle nelx res)
+ let ?C1 = "ALL l:setOf t1. h l < h x"
+ let ?C2 = "ALL r:setOf (remove h e t2). h x < h r"
+ have o2: "?C2"
+ proof -
+ from s2 have "setOf (remove h e t2) = setOf t2 - eqs h e" by (simp add: remove_set)
+ from s this show ?thesis by auto
+ qed
+ from o2 s show "?C1 & ?C2" by auto
+ qed
+ next case False note nxle = this
+ from nelx nxle have ex: "h e = h x" by simp
+ show ?thesis
+ proof (cases "t1 = Tip")
+ case True note t1tip = this
+ from ex t1tip have res: "remove h e (T t1 x t2) = t2" by simp
+ show ?thesis by (simp add: res t1tip ex s2)
+ next case False note t1nTip = this
+ from nelx nxle ex t1nTip
+ have res: "remove h e (T t1 x t2) =
+ T (wrm h t1) (rm h t1) t2"
+ by (simp add: Let_def wrmrm_decomp)
+ from res show ?thesis
+ proof simp
+ let ?C1 = "sortedTree h (wrm h t1)"
+ let ?C2 = "ALL l:setOf (wrm h t1). h l < h (rm h t1)"
+ let ?C3 = "ALL r:setOf t2. h (rm h t1) < h r"
+ let ?C4 = "sortedTree h t2"
+ from s1 t1nTip have o1: ?C1 by (simp add: wrm_sort)
+ from s1 t1nTip have o2: ?C2 by (simp add: wrm_less_rm)
+ have o3: ?C3
+ proof
+ fix r :: 'a
+ assume rt2: "r : setOf t2"
+ from s rm_set s1 t1nTip have o1: "h (rm h t1) < h x" by auto
+ from rt2 s have o2: "h x < h r" by auto
+ from o1 o2 show "h (rm h t1) < h r" by simp
+ qed
+ from o1 o2 o3 s2 show "?C1 & ?C2 & ?C3 & ?C4" by simp
+ qed
+ qed
+ qed
+ qed
+ qed
+qed
+
+text {* We summarize the specification of remove as follows. *}
+corollary remove_spec: "sortedTree h t -->
+ sortedTree h (remove h e t) &
+ setOf (remove h e t) = setOf t - eqs h e"
+by (simp add: remove_sort remove_set)
+
+generate_code ("BinaryTree_Code.ML")
+ test = "tlookup id 4 (remove id 3 (binsert id 4 (binsert id 3 Tip)))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/BinaryTree_Map.thy Wed Dec 10 15:59:34 2003 +0100
@@ -0,0 +1,257 @@
+header {* Mostly Isar-style Reasoning for Binary Tree Operations *}
+theory BinaryTree_Map = BinaryTree:
+
+text {* We prove correctness of map operations
+ implemented using binary search trees from BinaryTree.
+
+ This document is GPL.
+
+ Author: Viktor Kuncak, MIT CSAIL, November 2003 *}
+
+
+(*============================================================*)
+section {* Map implementation and an abstraction function *}
+(*============================================================*)
+
+types
+ 'a tarray = "(index * 'a) Tree"
+
+constdefs
+ valid_tmap :: "'a tarray => bool"
+ "valid_tmap t == sortedTree fst t"
+
+declare valid_tmap_def [simp]
+
+constdefs
+ mapOf :: "'a tarray => index => 'a option"
+ -- {* the abstraction function from trees to maps *}
+ "mapOf t i ==
+ (case (tlookup fst i t) of
+ None => None
+ | Some ia => Some (snd ia))"
+
+(*============================================================*)
+section {* Auxiliary Properties of our Implementation *}
+(*============================================================*)
+
+lemma mapOf_lookup1: "tlookup fst i t = None ==> mapOf t i = None"
+by (simp add: mapOf_def)
+
+lemma mapOf_lookup2: "tlookup fst i t = Some (j,a) ==> mapOf t i = Some a"
+by (simp add: mapOf_def)
+
+lemma assumes h: "mapOf t i = None"
+ shows mapOf_lookup3: "tlookup fst i t = None"
+proof (cases "tlookup fst i t")
+case None from this show ?thesis by assumption
+next case (Some ia) note tsome = this
+ from this have o1: "tlookup fst i t = Some (fst ia, snd ia)" by simp
+ have "mapOf t i = Some (snd ia)"
+ by (insert mapOf_lookup2 [of i t "fst ia" "snd ia"], simp add: o1)
+ from this have "mapOf t i ~= None" by simp
+ from this h show ?thesis by simp -- {* contradiction *}
+qed
+
+lemma assumes v: "valid_tmap t"
+ assumes h: "mapOf t i = Some a"
+ shows mapOf_lookup4: "tlookup fst i t = Some (i,a)"
+proof (cases "tlookup fst i t")
+case None
+ from this mapOf_lookup1 have "mapOf t i = None" by auto
+ from this h show ?thesis by simp -- {* contradiction *}
+next case (Some ia) note tsome = this
+ have tlookup_some_inst: "sortedTree fst t & (tlookup fst i t = Some ia) -->
+ ia : setOf t & fst ia = i" by (simp add: tlookup_some)
+ from tlookup_some_inst tsome v have "ia : setOf t" by simp
+ from tsome have "mapOf t i = Some (snd ia)" by (simp add: mapOf_def)
+ from this h have o1: "snd ia = a" by simp
+ from tlookup_some_inst tsome v have o2: "fst ia = i" by simp
+ from o1 o2 have "ia = (i,a)" by auto
+ from this tsome show "tlookup fst i t = Some (i, a)" by simp
+qed
+
+subsection {* Lemmas @{text mapset_none} and @{text mapset_some} establish
+ a relation between the set and map abstraction of the tree *}
+
+lemma assumes v: "valid_tmap t"
+ shows mapset_none: "(mapOf t i = None) = (ALL a. (i,a) ~: setOf t)"
+proof
+ -- {* ==> *}
+ assume mapNone: "mapOf t i = None"
+ from v mapNone mapOf_lookup3 have lnone: "tlookup fst i t = None" by auto
+ show "ALL a. (i,a) ~: setOf t"
+ proof
+ fix a
+ show "(i,a) ~: setOf t"
+ proof
+ assume iain: "(i,a) : setOf t"
+ have tlookup_none_inst:
+ "sortedTree fst t & (tlookup fst i t = None) --> (ALL x:setOf t. fst x ~= i)"
+ by (insert tlookup_none [of "fst" "t" "i"], assumption)
+ from v lnone tlookup_none_inst have "ALL x : setOf t. fst x ~= i" by simp
+ from this iain have "fst (i,a) ~= i" by fastsimp
+ from this show False by simp
+ qed
+ qed
+ -- {* <== *}
+ next assume h: "ALL a. (i,a) ~: setOf t"
+ show "mapOf t i = None"
+ proof (cases "mapOf t i")
+ case None show ?thesis by assumption
+ next case (Some a) note mapsome = this
+ from v mapsome have o1: "tlookup fst i t = Some (i,a)" by (simp add: mapOf_lookup4)
+ (* moving mapOf_lookup4 to assumption does not work, although it uses
+ no == !! *)
+ from tlookup_some have tlookup_some_inst:
+ "sortedTree fst t & tlookup fst i t = Some (i,a) -->
+ (i,a) : setOf t & fst (i,a) = i"
+ by (insert tlookup_some [of fst t i "(i,a)"], assumption)
+ from v o1 this have "(i,a) : setOf t" by simp
+ from this h show ?thesis by auto -- {* contradiction *}
+ qed
+qed
+
+lemma assumes v: "valid_tmap t"
+ shows mapset_some: "(mapOf t i = Some a) = ((i,a) : setOf t)"
+proof
+ -- {* ==> *}
+ assume mapsome: "mapOf t i = Some a"
+ from v mapsome have o1: "tlookup fst i t = Some (i,a)" by (simp add: mapOf_lookup4)
+ from tlookup_some have tlookup_some_inst:
+ "sortedTree fst t & tlookup fst i t = Some (i,a) -->
+ (i,a) : setOf t & fst (i,a) = i"
+ by (insert tlookup_some [of fst t i "(i,a)"], assumption)
+ from v o1 this show "(i,a) : setOf t" by simp
+ -- {* <== *}
+ next assume iain: "(i,a) : setOf t"
+ from v iain tlookup_finds have "tlookup fst (fst (i,a)) t = Some (i,a)" by fastsimp
+ from this have "tlookup fst i t = Some (i,a)" by simp
+ from this show "mapOf t i = Some a" by (simp add: mapOf_def)
+qed
+
+(*============================================================*)
+section {* Empty Map *}
+(*============================================================*)
+
+lemma mnew_spec_valid: "valid_tmap Tip"
+by (simp add: mapOf_def)
+
+lemma mtip_spec_empty: "mapOf Tip k = None"
+by (simp add: mapOf_def)
+
+
+(*============================================================*)
+section {* Map Update Operation *}
+(*============================================================*)
+
+constdefs
+ mupdate :: "index => 'a => 'a tarray => 'a tarray"
+ "mupdate i a t == binsert fst (i,a) t"
+
+lemma assumes v: "valid_tmap t"
+ shows mupdate_map: "mapOf (mupdate i a t) = (mapOf t)(i |-> a)"
+proof
+ fix i2
+ let ?tr = "binsert fst (i,a) t"
+ have upres: "mupdate i a t = ?tr" by (simp add: mupdate_def)
+ from v binsert_set
+ have setSpec: "setOf ?tr = setOf t - eqs fst (i,a) Un {(i,a)}" by fastsimp
+ from v binsert_sorted have vr: "valid_tmap ?tr" by fastsimp
+ show "mapOf (mupdate i a t) i2 = ((mapOf t)(i |-> a)) i2"
+ proof (cases "i = i2")
+ case True note i2ei = this
+ from i2ei have rhs_res: "((mapOf t)(i |-> a)) i2 = Some a" by simp
+ have lhs_res: "mapOf (mupdate i a t) i = Some a"
+ proof -
+ have will_find: "tlookup fst i ?tr = Some (i,a)"
+ proof -
+ from setSpec have kvin: "(i,a) : setOf ?tr" by simp
+ have binsert_sorted_inst: "sortedTree fst t -->
+ sortedTree fst ?tr"
+ by (insert binsert_sorted [of "fst" "t" "(i,a)"], assumption)
+ from v binsert_sorted_inst have rs: "sortedTree fst ?tr" by simp
+ have tlookup_finds_inst: "sortedTree fst ?tr & (i,a) : setOf ?tr -->
+ tlookup fst i ?tr = Some (i,a)"
+ by (insert tlookup_finds [of "fst" "?tr" "(i,a)"], simp)
+ from rs kvin tlookup_finds_inst show ?thesis by simp
+ qed
+ from upres will_find show ?thesis by (simp add: mapOf_def)
+ qed
+ from lhs_res rhs_res i2ei show ?thesis by simp
+ next case False note i2nei = this
+ from i2nei have rhs_res: "((mapOf t)(i |-> a)) i2 = mapOf t i2" by auto
+ have lhs_res: "mapOf (mupdate i a t) i2 = mapOf t i2"
+ proof (cases "mapOf t i2")
+ case None from this have mapNone: "mapOf t i2 = None" by simp
+ from v mapNone mapset_none have i2nin: "ALL a. (i2,a) ~: setOf t" by fastsimp
+ have noneIn: "ALL b. (i2,b) ~: setOf ?tr"
+ proof
+ fix b
+ from v binsert_set
+ have "setOf ?tr = setOf t - eqs fst (i,a) Un {(i,a)}"
+ by fastsimp
+ from this i2nei i2nin show "(i2,b) ~: setOf ?tr" by fastsimp
+ qed
+ have mapset_none_inst:
+ "valid_tmap ?tr --> (mapOf ?tr i2 = None) = (ALL a. (i2, a) ~: setOf ?tr)"
+ by (insert mapset_none [of "?tr" i2], simp)
+ from vr noneIn mapset_none_inst have "mapOf ?tr i2 = None" by fastsimp
+ from this upres mapNone show ?thesis by simp
+ next case (Some z) from this have mapSome: "mapOf t i2 = Some z" by simp
+ from v mapSome mapset_some have "(i2,z) : setOf t" by fastsimp
+ from this setSpec i2nei have "(i2,z) : setOf ?tr" by (simp add: eqs_def)
+ from this vr mapset_some have "mapOf ?tr i2 = Some z" by fastsimp
+ from this upres mapSome show ?thesis by simp
+ qed
+ from lhs_res rhs_res show ?thesis by simp
+ qed
+qed
+
+lemma assumes v: "valid_tmap t"
+ shows mupdate_valid: "valid_tmap (mupdate i a t)"
+proof -
+ let ?tr = "binsert fst (i,a) t"
+ have upres: "mupdate i a t = ?tr" by (simp add: mupdate_def)
+ from v binsert_sorted have vr: "valid_tmap ?tr" by fastsimp
+ from vr upres show ?thesis by simp
+qed
+
+(*============================================================*)
+section {* Map Remove Operation *}
+(*============================================================*)
+
+constdefs
+ mremove :: "index => 'a tarray => 'a tarray"
+ "mremove i t == remove fst (i, arbitrary) t"
+
+lemma assumes v: "valid_tmap t"
+ shows mremove_valid: "valid_tmap (mremove i t)"
+proof (simp add: mremove_def)
+ from v remove_sort
+ show "sortedTree fst (remove fst (i,arbitrary) t)" by fastsimp
+qed
+
+lemma assumes v: "valid_tmap t"
+ shows mremove_map: "mapOf (mremove i t) i = None"
+proof (simp add: mremove_def)
+ let ?tr = "remove fst (i,arbitrary) t"
+ show "mapOf ?tr i = None"
+ proof -
+ from v remove_spec
+ have remSet: "setOf ?tr = setOf t - eqs fst (i,arbitrary)"
+ by fastsimp
+ have noneIn: "ALL a. (i,a) ~: setOf ?tr"
+ proof
+ fix a
+ from remSet show "(i,a) ~: setOf ?tr" by (simp add: eqs_def)
+ qed
+ from v remove_sort have vr: "valid_tmap ?tr" by fastsimp
+ have mapset_none_inst: "valid_tmap ?tr ==>
+ (mapOf ?tr i = None) = (ALL a. (i,a) ~: setOf ?tr)"
+ by (insert mapset_none [of "?tr" "i"], simp)
+ from vr this have "(mapOf ?tr i = None) = (ALL a. (i,a) ~: setOf ?tr)" by fastsimp
+ from this noneIn show "mapOf ?tr i = None" by simp
+ qed
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/BinaryTree_TacticStyle.thy Wed Dec 10 15:59:34 2003 +0100
@@ -0,0 +1,141 @@
+header {* Tactic-Style Reasoning for Binary Tree Operations *}
+theory BinaryTree_TacticStyle = Main:
+
+text {* This example theory illustrates automated proofs of correctness
+ for binary tree operations using tactic-style reasoning.
+ The current proofs for remove operation are by Tobias Nipkow,
+ some modifications and the remaining tree operations are
+ by Viktor Kuncak. *}
+
+(*============================================================*)
+section {* Definition of a sorted binary tree *}
+(*============================================================*)
+
+datatype tree = Tip | Nd tree nat tree
+
+consts set_of :: "tree => nat set"
+-- {* The set of nodes stored in a tree. *}
+primrec
+"set_of Tip = {}"
+"set_of(Nd l x r) = set_of l Un set_of r Un {x}"
+
+consts sorted :: "tree => bool"
+-- {* Tree is sorted *}
+primrec
+"sorted Tip = True"
+"sorted(Nd l y r) =
+ (sorted l & sorted r & (ALL x:set_of l. x < y) & (ALL z:set_of r. y < z))"
+
+(*============================================================*)
+section {* Tree Membership *}
+(*============================================================*)
+
+consts
+ memb :: "nat => tree => bool"
+primrec
+"memb e Tip = False"
+"memb e (Nd t1 x t2) =
+ (if e < x then memb e t1
+ else if x < e then memb e t2
+ else True)"
+
+lemma member_set: "sorted t --> memb e t = (e : set_of t)"
+by (induct t, auto)
+
+(*============================================================*)
+section {* Insertion operation *}
+(*============================================================*)
+
+consts binsert :: "nat => tree => tree"
+-- {* Insert a node into sorted tree. *}
+primrec
+"binsert x Tip = (Nd Tip x Tip)"
+"binsert x (Nd t1 y t2) = (if x < y then
+ (Nd (binsert x t1) y t2)
+ else
+ (if y < x then
+ (Nd t1 y (binsert x t2))
+ else (Nd t1 y t2)))"
+
+theorem set_of_binsert [simp]: "set_of (binsert x t) = set_of t Un {x}"
+by (induct_tac t, auto)
+
+theorem binsert_sorted: "sorted t --> sorted (binsert x t)"
+by (induct_tac t, auto simp add: set_of_binsert)
+
+corollary binsert_spec: (* summary specification of binsert *)
+"sorted t ==>
+ sorted (binsert x t) &
+ set_of (binsert x t) = set_of t Un {x}"
+by (simp add: binsert_sorted)
+
+(*============================================================*)
+section {* Remove operation *}
+(*============================================================*)
+
+consts
+ remove:: "nat => tree => tree" -- {* remove a node from sorted tree *}
+ -- {* auxiliary operations: *}
+ rm :: "tree => nat" -- {* find the rightmost element in the tree *}
+ rem :: "tree => tree" -- {* find the tree without the rightmost element *}
+primrec
+"rm(Nd l x r) = (if r = Tip then x else rm r)"
+primrec
+"rem(Nd l x r) = (if r=Tip then l else Nd l x (rem r))"
+primrec
+"remove x Tip = Tip"
+"remove x (Nd l y r) =
+ (if x < y then Nd (remove x l) y r else
+ if y < x then Nd l y (remove x r) else
+ if l = Tip then r
+ else Nd (rem l) (rm l) r)"
+
+lemma rm_in_set_of: "t ~= Tip ==> rm t : set_of t"
+by (induct t) auto
+
+lemma set_of_rem: "t ~= Tip ==> set_of t = set_of(rem t) Un {rm t}"
+by (induct t) auto
+
+lemma [simp]: "[| t ~= Tip; sorted t |] ==> sorted(rem t)"
+by (induct t) (auto simp add:set_of_rem)
+
+lemma sorted_rem: "[| t ~= Tip; x \<in> set_of(rem t); sorted t |] ==> x < rm t"
+by (induct t) (auto simp add:set_of_rem split:if_splits)
+
+theorem set_of_remove [simp]: "sorted t ==> set_of(remove x t) = set_of t - {x}"
+apply(induct t)
+ apply simp
+apply simp
+apply(rule conjI)
+ apply fastsimp
+apply(rule impI)
+apply(rule conjI)
+ apply fastsimp
+apply(fastsimp simp:set_of_rem)
+done
+
+theorem remove_sorted: "sorted t ==> sorted(remove x t)"
+by (induct t) (auto intro: less_trans rm_in_set_of sorted_rem)
+
+corollary remove_spec: -- {* summary specification of remove *}
+"sorted t ==>
+ sorted (remove x t) &
+ set_of (remove x t) = set_of t - {x}"
+by (simp add: remove_sorted)
+
+text {* Finally, note that rem and rm can be computed
+ using a single tree traversal given by remrm. *}
+
+consts remrm :: "tree => tree * nat"
+primrec
+"remrm(Nd l x r) = (if r=Tip then (l,x) else
+ let (r',y) = remrm r in (Nd l x r',y))"
+
+lemma "t ~= Tip ==> remrm t = (rem t, rm t)"
+by (induct t) (auto simp:Let_def)
+
+text {* We can test this implementation by generating code. *}
+generate_code ("BinaryTree_TacticStyle_Code.ML")
+ test = "memb 4 (remove (3::nat) (binsert 4 (binsert 3 Tip)))"
+
+end
--- a/src/HOL/Induct/ROOT.ML Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Induct/ROOT.ML Wed Dec 10 15:59:34 2003 +0100
@@ -9,3 +9,6 @@
time_use_thy "PropLog";
time_use_thy "SList";
time_use_thy "LFilter";
+
+time_use_thy "BinaryTree_Map";
+time_use_thy "BinaryTree_TacticStyle";
--- a/src/HOL/Integ/Bin.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Integ/Bin.thy Wed Dec 10 15:59:34 2003 +0100
@@ -226,55 +226,9 @@
lemma int_numeral_1_eq_1: "Numeral1 = (1::int)"
by (simp add: int_1 int_Suc0_eq_1)
-
-subsubsection{*Special Simplification for Constants*}
-
-text{*These distributive laws move literals inside sums and differences.*}
-declare left_distrib [of _ _ "number_of v", standard, simp]
-declare right_distrib [of "number_of v", standard, simp]
-
-declare left_diff_distrib [of _ _ "number_of v", standard, simp]
-declare right_diff_distrib [of "number_of v", standard, simp]
-
-text{*These are actually for fields, like real: but where else to put them?*}
-declare zero_less_divide_iff [of "number_of w", standard, simp]
-declare divide_less_0_iff [of "number_of w", standard, simp]
-declare zero_le_divide_iff [of "number_of w", standard, simp]
-declare divide_le_0_iff [of "number_of w", standard, simp]
-
-(*Replaces "inverse #nn" by 1/#nn *)
-declare inverse_eq_divide [of "number_of w", standard, simp]
-
-text{*These laws simplify inequalities, moving unary minus from a term
-into the literal.*}
-declare less_minus_iff [of "number_of v", standard, simp]
-declare le_minus_iff [of "number_of v", standard, simp]
-declare equation_minus_iff [of "number_of v", standard, simp]
-
-declare minus_less_iff [of _ "number_of v", standard, simp]
-declare minus_le_iff [of _ "number_of v", standard, simp]
-declare minus_equation_iff [of _ "number_of v", standard, simp]
-
-text{*These simplify inequalities where one side is the constant 1.*}
-declare less_minus_iff [of 1, simplified, simp]
-declare le_minus_iff [of 1, simplified, simp]
-declare equation_zminus [of 1, simplified, simp]
-
-declare minus_less_iff [of _ 1, simplified, simp]
-declare minus_le_iff [of _ 1, simplified, simp]
-declare minus_equation_iff [of _ 1, simplified, simp]
-
-
-(*Moving negation out of products*)
+(*Moving negation out of products: so far for type "int" only*)
declare zmult_zminus [simp] zmult_zminus_right [simp]
-(*Cancellation of constant factors in comparisons (< and \<le>) *)
-
-declare mult_less_cancel_left [of "number_of v", standard, simp]
-declare mult_less_cancel_right [of _ "number_of v", standard, simp]
-declare mult_le_cancel_left [of "number_of v", standard, simp]
-declare mult_le_cancel_right [of _ "number_of v", standard, simp]
-
(** Special-case simplification for small constants **)
--- a/src/HOL/Integ/IntDiv.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Integ/IntDiv.thy Wed Dec 10 15:59:34 2003 +0100
@@ -10,18 +10,18 @@
fun posDivAlg (a,b) =
if a<b then (0,a)
else let val (q,r) = posDivAlg(a, 2*b)
- in if 0<=r-b then (2*q+1, r-b) else (2*q, r)
+ in if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
end
fun negDivAlg (a,b) =
- if 0<=a+b then (~1,a+b)
+ if 0\<le>a+b then (~1,a+b)
else let val (q,r) = negDivAlg(a, 2*b)
- in if 0<=r-b then (2*q+1, r-b) else (2*q, r)
+ in if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
end;
fun negateSnd (q,r:int) = (q,~r);
- fun divAlg (a,b) = if 0<=a then
+ fun divAlg (a,b) = if 0\<le>a then
if b>0 then posDivAlg (a,b)
else if a=0 then (0,0)
else negateSnd (negDivAlg (~a,~b))
@@ -40,10 +40,10 @@
quorem :: "(int*int) * (int*int) => bool"
"quorem == %((a,b), (q,r)).
a = b*q + r &
- (if 0 < b then 0<=r & r<b else b<r & r <= 0)"
+ (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
adjust :: "[int, int*int] => int*int"
- "adjust b == %(q,r). if 0 <= r-b then (2*q + 1, r-b)
+ "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
else (2*q, r)"
(** the division algorithm **)
@@ -52,14 +52,14 @@
consts posDivAlg :: "int*int => int*int"
recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + 1))"
"posDivAlg (a,b) =
- (if (a<b | b<=0) then (0,a)
+ (if (a<b | b\<le>0) then (0,a)
else adjust b (posDivAlg(a, 2*b)))"
(*for the case a<0, b>0*)
consts negDivAlg :: "int*int => int*int"
recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
"negDivAlg (a,b) =
- (if (0<=a+b | b<=0) then (-1,a+b)
+ (if (0\<le>a+b | b\<le>0) then (-1,a+b)
else adjust b (negDivAlg(a, 2*b)))"
(*for the general case b~=0*)
@@ -72,8 +72,8 @@
including the special case a=0, b<0, because negDivAlg requires a<0*)
divAlg :: "int*int => int*int"
"divAlg ==
- %(a,b). if 0<=a then
- if 0<=b then posDivAlg (a,b)
+ %(a,b). if 0\<le>a then
+ if 0\<le>b then posDivAlg (a,b)
else if a=0 then (0,0)
else negateSnd (negDivAlg (-a,-b))
else
@@ -92,9 +92,9 @@
subsection{*Uniqueness and Monotonicity of Quotients and Remainders*}
lemma unique_quotient_lemma:
- "[| b*q' + r' <= b*q + r; 0 <= r'; 0 < b; r < b |]
- ==> q' <= (q::int)"
-apply (subgoal_tac "r' + b * (q'-q) <= r")
+ "[| b*q' + r' \<le> b*q + r; 0 \<le> r'; 0 < b; r < b |]
+ ==> q' \<le> (q::int)"
+apply (subgoal_tac "r' + b * (q'-q) \<le> r")
prefer 2 apply (simp add: zdiff_zmult_distrib2)
apply (subgoal_tac "0 < b * (1 + q - q') ")
apply (erule_tac [2] order_le_less_trans)
@@ -105,8 +105,8 @@
done
lemma unique_quotient_lemma_neg:
- "[| b*q' + r' <= b*q + r; r <= 0; b < 0; b < r' |]
- ==> q <= (q'::int)"
+ "[| b*q' + r' \<le> b*q + r; r \<le> 0; b < 0; b < r' |]
+ ==> q \<le> (q'::int)"
by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,
auto)
@@ -136,7 +136,7 @@
lemma adjust_eq [simp]:
"adjust b (q,r) =
(let diff = r-b in
- if 0 <= diff then (2*q + 1, diff)
+ if 0 \<le> diff then (2*q + 1, diff)
else (2*q, r))"
by (simp add: Let_def adjust_def)
@@ -150,7 +150,7 @@
(*Correctness of posDivAlg: it computes quotients correctly*)
lemma posDivAlg_correct [rule_format]:
- "0 <= a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))"
+ "0 \<le> a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))"
apply (induct_tac a b rule: posDivAlg.induct, auto)
apply (simp_all add: quorem_def)
(*base case: a<b*)
@@ -172,7 +172,7 @@
lemma negDivAlg_eqn:
"0 < b ==>
negDivAlg (a,b) =
- (if 0<=a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))"
+ (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))"
by (rule negDivAlg.simps [THEN trans], simp)
(*Correctness of negDivAlg: it computes quotients correctly
@@ -181,7 +181,7 @@
"a < 0 --> 0 < b --> quorem ((a, b), negDivAlg (a, b))"
apply (induct_tac a b rule: negDivAlg.induct, auto)
apply (simp_all add: quorem_def)
- (*base case: 0<=a+b*)
+ (*base case: 0\<le>a+b*)
apply (simp add: negDivAlg_eqn)
(*main argument*)
apply (subst negDivAlg_eqn, assumption)
@@ -234,7 +234,7 @@
use "IntDiv_setup.ML"
-lemma pos_mod_conj : "(0::int) < b ==> 0 <= a mod b & a mod b < b"
+lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
apply (cut_tac a = a and b = b in divAlg_correct)
apply (auto simp add: quorem_def mod_def)
done
@@ -242,7 +242,7 @@
lemmas pos_mod_sign[simp] = pos_mod_conj [THEN conjunct1, standard]
and pos_mod_bound[simp] = pos_mod_conj [THEN conjunct2, standard]
-lemma neg_mod_conj : "b < (0::int) ==> a mod b <= 0 & b < a mod b"
+lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
apply (cut_tac a = a and b = b in divAlg_correct)
apply (auto simp add: quorem_def div_def mod_def)
done
@@ -265,34 +265,34 @@
lemma quorem_mod: "[| quorem((a,b),(q,r)); b ~= 0 |] ==> a mod b = r"
by (simp add: quorem_div_mod [THEN unique_remainder])
-lemma div_pos_pos_trivial: "[| (0::int) <= a; a < b |] ==> a div b = 0"
+lemma div_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a div b = 0"
apply (rule quorem_div)
apply (auto simp add: quorem_def)
done
-lemma div_neg_neg_trivial: "[| a <= (0::int); b < a |] ==> a div b = 0"
+lemma div_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a div b = 0"
apply (rule quorem_div)
apply (auto simp add: quorem_def)
done
-lemma div_pos_neg_trivial: "[| (0::int) < a; a+b <= 0 |] ==> a div b = -1"
+lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a div b = -1"
apply (rule quorem_div)
apply (auto simp add: quorem_def)
done
(*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*)
-lemma mod_pos_pos_trivial: "[| (0::int) <= a; a < b |] ==> a mod b = a"
+lemma mod_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a mod b = a"
apply (rule_tac q = 0 in quorem_mod)
apply (auto simp add: quorem_def)
done
-lemma mod_neg_neg_trivial: "[| a <= (0::int); b < a |] ==> a mod b = a"
+lemma mod_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a mod b = a"
apply (rule_tac q = 0 in quorem_mod)
apply (auto simp add: quorem_def)
done
-lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b <= 0 |] ==> a mod b = a+b"
+lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a mod b = a+b"
apply (rule_tac q = "-1" in quorem_mod)
apply (auto simp add: quorem_def)
done
@@ -355,13 +355,13 @@
subsection{*Division of a Number by Itself*}
-lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
+lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
apply (subgoal_tac "0 < a*q")
apply (simp add: int_0_less_mult_iff, arith)
done
-lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
-apply (subgoal_tac "0 <= a* (1-q) ")
+lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1"
+apply (subgoal_tac "0 \<le> a* (1-q) ")
apply (simp add: int_0_le_mult_iff)
apply (simp add: zdiff_zmult_distrib2)
done
@@ -408,10 +408,10 @@
(** a positive, b positive **)
-lemma div_pos_pos: "[| 0 < a; 0 <= b |] ==> a div b = fst (posDivAlg(a,b))"
+lemma div_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a div b = fst (posDivAlg(a,b))"
by (simp add: div_def divAlg_def)
-lemma mod_pos_pos: "[| 0 < a; 0 <= b |] ==> a mod b = snd (posDivAlg(a,b))"
+lemma mod_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a mod b = snd (posDivAlg(a,b))"
by (simp add: mod_def divAlg_def)
(** a negative, b positive **)
@@ -435,11 +435,11 @@
(** a negative, b negative **)
lemma div_neg_neg:
- "[| a < 0; b <= 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"
+ "[| a < 0; b \<le> 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"
by (simp add: div_def divAlg_def)
lemma mod_neg_neg:
- "[| a < 0; b <= 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"
+ "[| a < 0; b \<le> 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"
by (simp add: mod_def divAlg_def)
text {*Simplify expresions in which div and mod combine numerical constants*}
@@ -492,7 +492,7 @@
subsection{*Monotonicity in the First Argument (Dividend)*}
-lemma zdiv_mono1: "[| a <= a'; 0 < (b::int) |] ==> a div b <= a' div b"
+lemma zdiv_mono1: "[| a \<le> a'; 0 < (b::int) |] ==> a div b \<le> a' div b"
apply (cut_tac a = a and b = b in zmod_zdiv_equality)
apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
apply (rule unique_quotient_lemma)
@@ -501,7 +501,7 @@
apply (simp_all)
done
-lemma zdiv_mono1_neg: "[| a <= a'; (b::int) < 0 |] ==> a' div b <= a div b"
+lemma zdiv_mono1_neg: "[| a \<le> a'; (b::int) < 0 |] ==> a' div b \<le> a div b"
apply (cut_tac a = a and b = b in zmod_zdiv_equality)
apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
apply (rule unique_quotient_lemma_neg)
@@ -514,16 +514,16 @@
subsection{*Monotonicity in the Second Argument (Divisor)*}
lemma q_pos_lemma:
- "[| 0 <= b'*q' + r'; r' < b'; 0 < b' |] ==> 0 <= (q'::int)"
+ "[| 0 \<le> b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \<le> (q'::int)"
apply (subgoal_tac "0 < b'* (q' + 1) ")
apply (simp add: int_0_less_mult_iff)
apply (simp add: zadd_zmult_distrib2)
done
lemma zdiv_mono2_lemma:
- "[| b*q + r = b'*q' + r'; 0 <= b'*q' + r';
- r' < b'; 0 <= r; 0 < b'; b' <= b |]
- ==> q <= (q'::int)"
+ "[| b*q + r = b'*q' + r'; 0 \<le> b'*q' + r';
+ r' < b'; 0 \<le> r; 0 < b'; b' \<le> b |]
+ ==> q \<le> (q'::int)"
apply (frule q_pos_lemma, assumption+)
apply (subgoal_tac "b*q < b* (q' + 1) ")
apply (simp add: zmult_zless_cancel1)
@@ -535,7 +535,7 @@
done
lemma zdiv_mono2:
- "[| (0::int) <= a; 0 < b'; b' <= b |] ==> a div b <= a div b'"
+ "[| (0::int) \<le> a; 0 < b'; b' \<le> b |] ==> a div b \<le> a div b'"
apply (subgoal_tac "b ~= 0")
prefer 2 apply arith
apply (cut_tac a = a and b = b in zmod_zdiv_equality)
@@ -547,20 +547,20 @@
done
lemma q_neg_lemma:
- "[| b'*q' + r' < 0; 0 <= r'; 0 < b' |] ==> q' <= (0::int)"
+ "[| b'*q' + r' < 0; 0 \<le> r'; 0 < b' |] ==> q' \<le> (0::int)"
apply (subgoal_tac "b'*q' < 0")
apply (simp add: zmult_less_0_iff, arith)
done
lemma zdiv_mono2_neg_lemma:
"[| b*q + r = b'*q' + r'; b'*q' + r' < 0;
- r < b; 0 <= r'; 0 < b'; b' <= b |]
- ==> q' <= (q::int)"
+ r < b; 0 \<le> r'; 0 < b'; b' \<le> b |]
+ ==> q' \<le> (q::int)"
apply (frule q_neg_lemma, assumption+)
apply (subgoal_tac "b*q' < b* (q + 1) ")
apply (simp add: zmult_zless_cancel1)
apply (simp add: zadd_zmult_distrib2)
-apply (subgoal_tac "b*q' <= b'*q'")
+apply (subgoal_tac "b*q' \<le> b'*q'")
prefer 2 apply (simp add: zmult_zle_mono1_neg)
apply (subgoal_tac "b'*q' < b + b*q")
apply arith
@@ -568,7 +568,7 @@
done
lemma zdiv_mono2_neg:
- "[| a < (0::int); 0 < b'; b' <= b |] ==> a div b' <= a div b"
+ "[| a < (0::int); 0 < b'; b' \<le> b |] ==> a div b' \<le> a div b"
apply (cut_tac a = a and b = b in zmod_zdiv_equality)
apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
apply (rule zdiv_mono2_neg_lemma)
@@ -698,7 +698,7 @@
(** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
-lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r <= 0 |] ==> b*c < b*(q mod c) + r"
+lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r \<le> 0 |] ==> b*c < b*(q mod c) + r"
apply (subgoal_tac "b * (c - q mod c) < r * 1")
apply (simp add: zdiff_zmult_distrib2)
apply (rule order_le_less_trans)
@@ -708,19 +708,19 @@
add1_zle_eq pos_mod_bound)
done
-lemma zmult2_lemma_aux2: "[| (0::int) < c; b < r; r <= 0 |] ==> b * (q mod c) + r <= 0"
-apply (subgoal_tac "b * (q mod c) <= 0")
+lemma zmult2_lemma_aux2: "[| (0::int) < c; b < r; r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
+apply (subgoal_tac "b * (q mod c) \<le> 0")
apply arith
apply (simp add: zmult_le_0_iff)
done
-lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 <= r; r < b |] ==> 0 <= b * (q mod c) + r"
-apply (subgoal_tac "0 <= b * (q mod c) ")
+lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 \<le> r; r < b |] ==> 0 \<le> b * (q mod c) + r"
+apply (subgoal_tac "0 \<le> b * (q mod c) ")
apply arith
apply (simp add: int_0_le_mult_iff)
done
-lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
+lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
apply (simp add: zdiff_zmult_distrib2)
apply (rule order_less_le_trans)
@@ -798,7 +798,7 @@
lemma split_pos_lemma:
"0<k ==>
- P(n div k :: int)(n mod k) = (\<forall>i j. 0<=j & j<k & n = k*i + j --> P i j)"
+ P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
apply (rule iffI)
apply clarify
apply (erule_tac P="P ?x ?y" in rev_mp)
@@ -813,7 +813,7 @@
lemma split_neg_lemma:
"k<0 ==>
- P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j<=0 & n = k*i + j --> P i j)"
+ P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
apply (rule iffI)
apply clarify
apply (erule_tac P="P ?x ?y" in rev_mp)
@@ -829,8 +829,8 @@
lemma split_zdiv:
"P(n div k :: int) =
((k = 0 --> P 0) &
- (0<k --> (\<forall>i j. 0<=j & j<k & n = k*i + j --> P i)) &
- (k<0 --> (\<forall>i j. k<j & j<=0 & n = k*i + j --> P i)))"
+ (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
+ (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
apply (case_tac "k=0")
apply (simp add: DIVISION_BY_ZERO)
apply (simp only: linorder_neq_iff)
@@ -842,8 +842,8 @@
lemma split_zmod:
"P(n mod k :: int) =
((k = 0 --> P n) &
- (0<k --> (\<forall>i j. 0<=j & j<k & n = k*i + j --> P j)) &
- (k<0 --> (\<forall>i j. k<j & j<=0 & n = k*i + j --> P j)))"
+ (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
+ (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
apply (case_tac "k=0")
apply (simp add: DIVISION_BY_ZERO)
apply (simp only: linorder_neq_iff)
@@ -861,29 +861,33 @@
(** computing div by shifting **)
-lemma pos_zdiv_mult_2: "(0::int) <= a ==> (1 + 2*b) div (2*a) = b div a"
-apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
-apply (subgoal_tac "1 <= a")
- prefer 2 apply arith
-apply (subgoal_tac "1 < a * 2")
- prefer 2 apply arith
-apply (subgoal_tac "2* (1 + b mod a) <= 2*a")
- apply (rule_tac [2] zmult_zle_mono2)
-apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq
- pos_mod_bound)
-apply (subst zdiv_zadd1_eq)
-apply (simp add: zdiv_zmult_zmult2 zmod_zmult_zmult2 div_pos_pos_trivial)
-apply (subst div_pos_pos_trivial)
-apply (auto simp add: mod_pos_pos_trivial)
-apply (subgoal_tac "0 <= b mod a", arith)
-apply (simp)
-done
+lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
+proof cases
+ assume "a=0"
+ thus ?thesis by simp
+next
+ assume "a\<noteq>0" and le_a: "0\<le>a"
+ hence a_pos: "1 \<le> a" by arith
+ hence one_less_a2: "1 < 2*a" by arith
+ hence le_2a: "2 * (1 + b mod a) \<le> 2 * a"
+ by (simp add: mult_le_cancel_left zadd_commute [of 1] add1_zle_eq)
+ with a_pos have "0 \<le> b mod a" by simp
+ hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)"
+ by (simp add: mod_pos_pos_trivial one_less_a2)
+ with le_2a
+ have "(1 mod (2*a) + 2*(b mod a)) div (2*a) = 0"
+ by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2
+ right_distrib)
+ thus ?thesis
+ by (subst zdiv_zadd1_eq,
+ simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2
+ div_pos_pos_trivial)
+qed
-
-lemma neg_zdiv_mult_2: "a <= (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"
+lemma neg_zdiv_mult_2: "a \<le> (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"
apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ")
apply (rule_tac [2] pos_zdiv_mult_2)
-apply (auto simp add: zmult_zminus_right)
+apply (auto simp add: zmult_zminus_right right_diff_distrib)
apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
apply (simp only: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric],
simp)
@@ -892,12 +896,12 @@
(*Not clear why this must be proved separately; probably number_of causes
simplification problems*)
-lemma not_0_le_lemma: "~ 0 <= x ==> x <= (0::int)"
+lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
by auto
lemma zdiv_number_of_BIT[simp]:
"number_of (v BIT b) div number_of (w BIT False) =
- (if ~b | (0::int) <= number_of w
+ (if ~b | (0::int) \<le> number_of w
then number_of v div (number_of w)
else (number_of v + (1::int)) div (number_of w))"
apply (simp only: zadd_assoc number_of_BIT)
@@ -911,31 +915,31 @@
(** computing mod by shifting (proofs resemble those for div) **)
lemma pos_zmod_mult_2:
- "(0::int) <= a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"
+ "(0::int) \<le> a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"
apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
-apply (subgoal_tac "1 <= a")
+apply (subgoal_tac "1 \<le> a")
prefer 2 apply arith
apply (subgoal_tac "1 < a * 2")
prefer 2 apply arith
-apply (subgoal_tac "2* (1 + b mod a) <= 2*a")
+apply (subgoal_tac "2* (1 + b mod a) \<le> 2*a")
apply (rule_tac [2] zmult_zle_mono2)
apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq
pos_mod_bound)
apply (subst zmod_zadd1_eq)
apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
apply (rule mod_pos_pos_trivial)
-apply (auto simp add: mod_pos_pos_trivial)
-apply (subgoal_tac "0 <= b mod a", arith)
+apply (auto simp add: mod_pos_pos_trivial left_distrib)
+apply (subgoal_tac "0 \<le> b mod a", arith)
apply (simp)
done
lemma neg_zmod_mult_2:
- "a <= (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1"
+ "a \<le> (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1"
apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) =
1 + 2* ((-b - 1) mod (-a))")
apply (rule_tac [2] pos_zmod_mult_2)
-apply (auto simp add: zmult_zminus_right)
+apply (auto simp add: zmult_zminus_right right_diff_distrib)
apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
prefer 2 apply simp
apply (simp only: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
@@ -944,7 +948,7 @@
lemma zmod_number_of_BIT [simp]:
"number_of (v BIT b) mod number_of (w BIT False) =
(if b then
- if (0::int) <= number_of w
+ if (0::int) \<le> number_of w
then 2 * (number_of v mod number_of w) + 1
else 2 * ((number_of v + (1::int)) mod number_of w) - 1
else 2 * (number_of v mod number_of w))"
@@ -958,16 +962,16 @@
(** Quotients of signs **)
lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0"
-apply (subgoal_tac "a div b <= -1", force)
+apply (subgoal_tac "a div b \<le> -1", force)
apply (rule order_trans)
apply (rule_tac a' = "-1" in zdiv_mono1)
apply (auto simp add: zdiv_minus1)
done
-lemma div_nonneg_neg_le0: "[| (0::int) <= a; b < 0 |] ==> a div b <= 0"
+lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
by (drule zdiv_mono1_neg, auto)
-lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 <= a div b) = (0 <= a)"
+lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
apply auto
apply (drule_tac [2] zdiv_mono1)
apply (auto simp add: linorder_neq_iff)
@@ -976,16 +980,16 @@
done
lemma neg_imp_zdiv_nonneg_iff:
- "b < (0::int) ==> (0 <= a div b) = (a <= (0::int))"
+ "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
apply (subst zdiv_zminus_zminus [symmetric])
apply (subst pos_imp_zdiv_nonneg_iff, auto)
done
-(*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*)
+(*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
-(*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*)
+(*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
@@ -1150,7 +1154,7 @@
apply (rule_tac [!] x = "-k" in exI, auto)
done
-lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z <= (n::int)"
+lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
apply (rule_tac z=n in int_cases)
apply (auto simp add: dvd_int_iff)
apply (rule_tac z=z in int_cases)
--- a/src/HOL/Integ/NatBin.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Integ/NatBin.thy Wed Dec 10 15:59:34 2003 +0100
@@ -425,7 +425,7 @@
"((number_of (v BIT x) ::int) = number_of (w BIT y)) =
(x=y & (((number_of v) ::int) = number_of w))"
by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute
- Ring_and_Field.add_left_cancel add_assoc left_zero
+ Ring_and_Field.add_left_cancel add_assoc Ring_and_Field.add_0
split add: split_if cong: imp_cong)
--- a/src/HOL/Integ/NatSimprocs.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Integ/NatSimprocs.thy Wed Dec 10 15:59:34 2003 +0100
@@ -132,4 +132,65 @@
declare Suc_div_eq_add3_div [of _ "number_of v", standard, simp]
declare Suc_mod_eq_add3_mod [of _ "number_of v", standard, simp]
+
+subsection{*Special Simplification for Constants*}
+
+text{*These belong here, late in the development of HOL, to prevent their
+interfering with proofs of abstract properties of instances of the function
+@{term number_of}*}
+
+text{*These distributive laws move literals inside sums and differences.*}
+declare left_distrib [of _ _ "number_of v", standard, simp]
+declare right_distrib [of "number_of v", standard, simp]
+
+declare left_diff_distrib [of _ _ "number_of v", standard, simp]
+declare right_diff_distrib [of "number_of v", standard, simp]
+
+text{*These are actually for fields, like real: but where else to put them?*}
+declare zero_less_divide_iff [of "number_of w", standard, simp]
+declare divide_less_0_iff [of "number_of w", standard, simp]
+declare zero_le_divide_iff [of "number_of w", standard, simp]
+declare divide_le_0_iff [of "number_of w", standard, simp]
+
+(*Replaces "inverse #nn" by 1/#nn *)
+declare inverse_eq_divide [of "number_of w", standard, simp]
+
+text{*These laws simplify inequalities, moving unary minus from a term
+into the literal.*}
+declare less_minus_iff [of "number_of v", standard, simp]
+declare le_minus_iff [of "number_of v", standard, simp]
+declare equation_minus_iff [of "number_of v", standard, simp]
+
+declare minus_less_iff [of _ "number_of v", standard, simp]
+declare minus_le_iff [of _ "number_of v", standard, simp]
+declare minus_equation_iff [of _ "number_of v", standard, simp]
+
+text{*These simplify inequalities where one side is the constant 1.*}
+declare less_minus_iff [of 1, simplified, simp]
+declare le_minus_iff [of 1, simplified, simp]
+declare equation_minus_iff [of 1, simplified, simp]
+
+declare minus_less_iff [of _ 1, simplified, simp]
+declare minus_le_iff [of _ 1, simplified, simp]
+declare minus_equation_iff [of _ 1, simplified, simp]
+
+
+(*Cancellation of constant factors in comparisons (< and \<le>) *)
+
+declare mult_less_cancel_left [of "number_of v", standard, simp]
+declare mult_less_cancel_right [of _ "number_of v", standard, simp]
+declare mult_le_cancel_left [of "number_of v", standard, simp]
+declare mult_le_cancel_right [of _ "number_of v", standard, simp]
+
+
+(*Multiplying out constant divisors in comparisons (< \<le> and =) *)
+
+declare le_divide_eq [of _ _ "number_of w", standard, simp]
+declare divide_le_eq [of _ "number_of w", standard, simp]
+declare less_divide_eq [of _ _ "number_of w", standard, simp]
+declare divide_less_eq [of _ "number_of w", standard, simp]
+declare eq_divide_eq [of _ _ "number_of w", standard, simp]
+declare divide_eq_eq [of _ "number_of w", standard, simp]
+
+
end
--- a/src/HOL/IsaMakefile Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/IsaMakefile Wed Dec 10 15:59:34 2003 +0100
@@ -224,6 +224,8 @@
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
$(LOG)/HOL-Induct.gz: $(OUT)/HOL \
+ Induct/BinaryTree.thy Induct/BinaryTree_Map.thy\
+ Induct/BinaryTree_TacticStyle.thy\
Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
Induct/PropLog.thy Induct/ROOT.ML \
--- a/src/HOL/Numeral.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Numeral.thy Wed Dec 10 15:59:34 2003 +0100
@@ -57,4 +57,5 @@
lemma Let_1 [simp]: "Let 1 f == f 1"
by (simp add: Let_def)
+
end
--- a/src/HOL/Real/RealArith.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Real/RealArith.thy Wed Dec 10 15:59:34 2003 +0100
@@ -1,10 +1,80 @@
theory RealArith = RealArith0
files ("real_arith.ML"):
+lemma real_divide_1: "(x::real)/1 = x"
+by (simp add: real_divide_def)
+
use "real_arith.ML"
setup real_arith_setup
+subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
+
+text{*Needed in this non-standard form by Hyperreal/Transcendental*}
+lemma real_0_le_divide_iff:
+ "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))"
+by (simp add: real_divide_def zero_le_mult_iff, auto)
+
+lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
+by arith
+
+lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)"
+by auto
+
+lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)"
+by auto
+
+lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)"
+by auto
+
+lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)"
+by auto
+
+lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)"
+by auto
+
+
+(** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc.,
+ in RealBin
+**)
+
+lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)"
+by auto
+
+lemma real_0_le_diff_iff [iff]: "((0::real) \<le> x-y) = (y \<le> x)"
+by auto
+
+(*
+FIXME: we should have this, as for type int, but many proofs would break.
+It replaces x+-y by x-y.
+Addsimps [symmetric real_diff_def]
+*)
+
+(** Division by 1, -1 **)
+
+lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)"
+by simp
+
+lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)"
+by (simp add: real_divide_def real_minus_inverse)
+
+lemma real_lbound_gt_zero:
+ "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
+apply (rule_tac x = " (min d1 d2) /2" in exI)
+apply (simp add: min_def)
+done
+
+(*** Density of the Reals ***)
+
+lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
+by auto
+
+lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
+by auto
+
+lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y"
+by (blast intro!: real_less_half_sum real_gt_half_sum)
+
subsection{*Absolute Value Function for the Reals*}
(** abs (absolute value) **)
@@ -214,8 +284,25 @@
apply (rule abs_triangle_ineq)
done
+
ML
{*
+val real_0_le_divide_iff = thm"real_0_le_divide_iff";
+val real_add_minus_iff = thm"real_add_minus_iff";
+val real_add_eq_0_iff = thm"real_add_eq_0_iff";
+val real_add_less_0_iff = thm"real_add_less_0_iff";
+val real_0_less_add_iff = thm"real_0_less_add_iff";
+val real_add_le_0_iff = thm"real_add_le_0_iff";
+val real_0_le_add_iff = thm"real_0_le_add_iff";
+val real_0_less_diff_iff = thm"real_0_less_diff_iff";
+val real_0_le_diff_iff = thm"real_0_le_diff_iff";
+val real_divide_minus1 = thm"real_divide_minus1";
+val real_minus1_divide = thm"real_minus1_divide";
+val real_lbound_gt_zero = thm"real_lbound_gt_zero";
+val real_less_half_sum = thm"real_less_half_sum";
+val real_gt_half_sum = thm"real_gt_half_sum";
+val real_dense = thm"real_dense";
+
val abs_nat_number_of = thm"abs_nat_number_of";
val abs_split = thm"abs_split";
val abs_iff = thm"abs_iff";
--- a/src/HOL/Real/RealArith0.ML Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Real/RealArith0.ML Wed Dec 10 15:59:34 2003 +0100
@@ -6,9 +6,7 @@
Common factor cancellation
*)
-val real_diff_minus_eq = thm"real_diff_minus_eq";
val real_inverse_eq_divide = thm"real_inverse_eq_divide";
-val real_0_le_divide_iff = thm"real_0_le_divide_iff";
val real_mult_less_cancel2 = thm"real_mult_less_cancel2";
val real_mult_le_cancel2 = thm"real_mult_le_cancel2";
val real_mult_less_cancel1 = thm"real_mult_less_cancel1";
@@ -207,33 +205,10 @@
test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z";
*)
-val real_add_minus_iff = thm"real_add_minus_iff";
-val real_add_eq_0_iff = thm"real_add_eq_0_iff";
-val real_add_less_0_iff = thm"real_add_less_0_iff";
-val real_0_less_add_iff = thm"real_0_less_add_iff";
-val real_add_le_0_iff = thm"real_add_le_0_iff";
-val real_0_le_add_iff = thm"real_0_le_add_iff";
-val real_0_less_diff_iff = thm"real_0_less_diff_iff";
-val real_0_le_diff_iff = thm"real_0_le_diff_iff";
-val real_divide_eq_cancel2 = thm"real_divide_eq_cancel2";
-val real_divide_eq_cancel1 = thm"real_divide_eq_cancel1";
val real_inverse_less_iff = thm"real_inverse_less_iff";
val real_inverse_le_iff = thm"real_inverse_le_iff";
-val real_divide_1 = thm"real_divide_1";
-val real_divide_minus1 = thm"real_divide_minus1";
-val real_minus1_divide = thm"real_minus1_divide";
-val real_lbound_gt_zero = thm"real_lbound_gt_zero";
-val real_less_half_sum = thm"real_less_half_sum";
-val real_gt_half_sum = thm"real_gt_half_sum";
-val real_dense = thm"real_dense";
-val pos_real_less_divide_eq = thm"pos_real_less_divide_eq";
-val neg_real_less_divide_eq = thm"neg_real_less_divide_eq";
-val pos_real_divide_less_eq = thm"pos_real_divide_less_eq";
-val neg_real_divide_less_eq = thm"neg_real_divide_less_eq";
-val pos_real_le_divide_eq = thm"pos_real_le_divide_eq";
-val neg_real_le_divide_eq = thm"neg_real_le_divide_eq";
-val pos_real_divide_le_eq = thm"pos_real_divide_le_eq";
-val neg_real_divide_le_eq = thm"neg_real_divide_le_eq";
-val real_eq_divide_eq = thm"real_eq_divide_eq";
-val real_divide_eq_eq = thm"real_divide_eq_eq";
+val pos_real_less_divide_eq = thm"pos_less_divide_eq";
+val pos_real_divide_less_eq = thm"pos_divide_less_eq";
+val pos_real_le_divide_eq = thm"pos_le_divide_eq";
+val pos_real_divide_le_eq = thm"pos_divide_le_eq";
--- a/src/HOL/Real/RealArith0.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Real/RealArith0.thy Wed Dec 10 15:59:34 2003 +0100
@@ -1,270 +1,6 @@
theory RealArith0 = RealBin
files "real_arith0.ML":
-(*FIXME: move results further down to Ring_and_Field*)
-
setup real_arith_setup
-subsection{*Facts that need the Arithmetic Decision Procedure*}
-
-lemma real_diff_minus_eq: "x - - y = x + (y::real)"
-by simp
-declare real_diff_minus_eq [simp]
-
-(** Division and inverse **)
-
-lemma real_inverse_eq_divide: "inverse (x::real) = 1/x"
- by (rule Ring_and_Field.inverse_eq_divide)
-
-text{*Needed in this non-standard form by Hyperreal/Transcendental*}
-lemma real_0_le_divide_iff:
- "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))"
-by (simp add: real_divide_def real_0_le_mult_iff, auto)
-
-
-(**** Factor cancellation theorems for "real" ****)
-
-(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
- but not (yet?) for k*m < n*k. **)
-
-lemma real_mult_less_cancel2:
- "(m*k < n*k) = (((0::real) < k & m<n) | (k < 0 & n<m))"
- by (rule Ring_and_Field.mult_less_cancel_right)
-
-lemma real_mult_le_cancel2:
- "(m*k <= n*k) = (((0::real) < k --> m<=n) & (k < 0 --> n<=m))"
- by (rule Ring_and_Field.mult_le_cancel_right)
-
-lemma real_mult_less_cancel1:
- "(k*m < k*n) = (((0::real) < k & m<n) | (k < 0 & n<m))"
- by (rule Ring_and_Field.mult_less_cancel_left)
-
-lemma real_mult_le_cancel1:
- "!!k::real. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))"
- by (rule Ring_and_Field.mult_le_cancel_left)
-
-lemma real_mult_eq_cancel1: "!!k::real. (k*m = k*n) = (k = 0 | m=n)"
- by (rule Ring_and_Field.mult_cancel_left)
-
-lemma real_mult_eq_cancel2: "!!k::real. (m*k = n*k) = (k = 0 | m=n)"
- by (rule Ring_and_Field.mult_cancel_right)
-
-lemma real_mult_div_cancel1: "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)"
- by (rule Ring_and_Field.mult_divide_cancel_left)
-
-lemma real_mult_div_cancel_disj:
- "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)"
- by (rule Ring_and_Field.mult_divide_cancel_eq_if)
-
-subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
-
-lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
-by arith
-
-lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)"
-by auto
-
-lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)"
-by auto
-
-lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)"
-by auto
-
-lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)"
-by auto
-
-lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)"
-by auto
-
-
-(** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc.,
- in RealBin
-**)
-
-lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)"
-by auto
-
-lemma real_0_le_diff_iff [iff]: "((0::real) \<le> x-y) = (y \<le> x)"
-by auto
-
-(*
-FIXME: we should have this, as for type int, but many proofs would break.
-It replaces x+-y by x-y.
-Addsimps [symmetric real_diff_def]
-*)
-
-
-(*FIXME: move most of these to Ring_and_Field*)
-
-subsection{*Simplification of Inequalities Involving Literal Divisors*}
-
-lemma pos_real_le_divide_eq: "0<z ==> ((x::real) \<le> y/z) = (x*z \<le> y)"
-apply (subgoal_tac " (x*z \<le> y) = (x*z \<le> (y/z) *z) ")
- prefer 2 apply (simp add: real_divide_def real_mult_assoc)
-apply (erule ssubst)
-apply (subst real_mult_le_cancel2, simp)
-done
-
-lemma neg_real_le_divide_eq: "z<0 ==> ((x::real) \<le> y/z) = (y \<le> x*z)"
-apply (subgoal_tac " (y \<le> x*z) = ((y/z) *z \<le> x*z) ")
- prefer 2 apply (simp add: real_divide_def real_mult_assoc)
-apply (erule ssubst)
-apply (subst real_mult_le_cancel2, simp)
-done
-
-lemma real_le_divide_eq:
- "((x::real) \<le> y/z) = (if 0<z then x*z \<le> y
- else if z<0 then y \<le> x*z
- else x\<le>0)"
-apply (case_tac "z=0", simp)
-apply (simp add: pos_real_le_divide_eq neg_real_le_divide_eq)
-done
-
-declare real_le_divide_eq [of _ _ "number_of w", standard, simp]
-
-lemma pos_real_divide_le_eq: "0<z ==> (y/z \<le> (x::real)) = (y \<le> x*z)"
-apply (subgoal_tac " (y \<le> x*z) = ((y/z) *z \<le> x*z) ")
- prefer 2 apply (simp add: real_divide_def real_mult_assoc)
-apply (erule ssubst)
-apply (subst real_mult_le_cancel2, simp)
-done
-
-lemma neg_real_divide_le_eq: "z<0 ==> (y/z \<le> (x::real)) = (x*z \<le> y)"
-apply (subgoal_tac " (x*z \<le> y) = (x*z \<le> (y/z) *z) ")
- prefer 2 apply (simp add: real_divide_def real_mult_assoc)
-apply (erule ssubst)
-apply (subst real_mult_le_cancel2, simp)
-done
-
-
-lemma real_divide_le_eq:
- "(y/z \<le> (x::real)) = (if 0<z then y \<le> x*z
- else if z<0 then x*z \<le> y
- else 0 \<le> x)"
-apply (case_tac "z=0", simp)
-apply (simp add: pos_real_divide_le_eq neg_real_divide_le_eq)
-done
-
-declare real_divide_le_eq [of _ "number_of w", standard, simp]
-
-
-lemma pos_real_less_divide_eq: "0<z ==> ((x::real) < y/z) = (x*z < y)"
-apply (subgoal_tac " (x*z < y) = (x*z < (y/z) *z) ")
- prefer 2 apply (simp add: real_divide_def real_mult_assoc)
-apply (erule ssubst)
-apply (subst real_mult_less_cancel2, simp)
-done
-
-lemma neg_real_less_divide_eq: "z<0 ==> ((x::real) < y/z) = (y < x*z)"
-apply (subgoal_tac " (y < x*z) = ((y/z) *z < x*z) ")
- prefer 2 apply (simp add: real_divide_def real_mult_assoc)
-apply (erule ssubst)
-apply (subst real_mult_less_cancel2, simp)
-done
-
-lemma real_less_divide_eq:
- "((x::real) < y/z) = (if 0<z then x*z < y
- else if z<0 then y < x*z
- else x<0)"
-apply (case_tac "z=0", simp)
-apply (simp add: pos_real_less_divide_eq neg_real_less_divide_eq)
-done
-
-declare real_less_divide_eq [of _ _ "number_of w", standard, simp]
-
-lemma pos_real_divide_less_eq: "0<z ==> (y/z < (x::real)) = (y < x*z)"
-apply (subgoal_tac " (y < x*z) = ((y/z) *z < x*z) ")
- prefer 2 apply (simp add: real_divide_def real_mult_assoc)
-apply (erule ssubst)
-apply (subst real_mult_less_cancel2, simp)
-done
-
-lemma neg_real_divide_less_eq: "z<0 ==> (y/z < (x::real)) = (x*z < y)"
-apply (subgoal_tac " (x*z < y) = (x*z < (y/z) *z) ")
- prefer 2 apply (simp add: real_divide_def real_mult_assoc)
-apply (erule ssubst)
-apply (subst real_mult_less_cancel2, simp)
-done
-
-lemma real_divide_less_eq:
- "(y/z < (x::real)) = (if 0<z then y < x*z
- else if z<0 then x*z < y
- else 0 < x)"
-apply (case_tac "z=0", simp)
-apply (simp add: pos_real_divide_less_eq neg_real_divide_less_eq)
-done
-
-declare real_divide_less_eq [of _ "number_of w", standard, simp]
-
-lemma nonzero_real_eq_divide_eq: "z\<noteq>0 ==> ((x::real) = y/z) = (x*z = y)"
-apply (subgoal_tac " (x*z = y) = (x*z = (y/z) *z) ")
- prefer 2 apply (simp add: real_divide_def real_mult_assoc)
-apply (erule ssubst)
-apply (subst real_mult_eq_cancel2, simp)
-done
-
-lemma real_eq_divide_eq:
- "((x::real) = y/z) = (if z\<noteq>0 then x*z = y else x=0)"
-by (simp add: nonzero_real_eq_divide_eq)
-
-declare real_eq_divide_eq [of _ _ "number_of w", standard, simp]
-
-lemma nonzero_real_divide_eq_eq: "z\<noteq>0 ==> (y/z = (x::real)) = (y = x*z)"
-apply (subgoal_tac " (y = x*z) = ((y/z) *z = x*z) ")
- prefer 2 apply (simp add: real_divide_def real_mult_assoc)
-apply (erule ssubst)
-apply (subst real_mult_eq_cancel2, simp)
-done
-
-lemma real_divide_eq_eq:
- "(y/z = (x::real)) = (if z\<noteq>0 then y = x*z else x=0)"
-by (simp add: nonzero_real_divide_eq_eq)
-
-declare real_divide_eq_eq [of _ "number_of w", standard, simp]
-
-lemma real_divide_eq_cancel2: "(m/k = n/k) = (k = 0 | m = (n::real))"
-apply (case_tac "k=0", simp)
-apply (simp add:divide_inverse)
-done
-
-lemma real_divide_eq_cancel1: "(k/m = k/n) = (k = 0 | m = (n::real))"
-by (force simp add: real_divide_eq_eq real_eq_divide_eq)
-
-lemma real_inverse_less_iff:
- "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)"
-by (rule Ring_and_Field.inverse_less_iff_less)
-
-lemma real_inverse_le_iff:
- "[| 0 < r; 0 < x|] ==> (inverse x \<le> inverse r) = (r \<le> (x::real))"
-by (rule Ring_and_Field.inverse_le_iff_le)
-
-
-(** Division by 1, -1 **)
-
-lemma real_divide_1: "(x::real)/1 = x"
-by (simp add: real_divide_def)
-
-lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)"
-by simp
-
-lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)"
-by (simp add: real_divide_def real_minus_inverse)
-
-lemma real_lbound_gt_zero:
- "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
-apply (rule_tac x = " (min d1 d2) /2" in exI)
-apply (simp add: min_def)
-done
-
-(*** Density of the Reals ***)
-
-lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
-by auto
-
-lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
-by auto
-
-lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y"
-by (blast intro!: real_less_half_sum real_gt_half_sum)
-
end
--- a/src/HOL/Real/RealOrd.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Real/RealOrd.thy Wed Dec 10 15:59:34 2003 +0100
@@ -280,6 +280,9 @@
lemma real_mult_not_zero: "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)"
by simp
+lemma real_inverse_eq_divide: "inverse (x::real) = 1/x"
+ by (rule Ring_and_Field.inverse_eq_divide)
+
lemma real_inverse_inverse: "inverse(inverse (x::real)) = x"
by (rule Ring_and_Field.inverse_inverse_eq)
@@ -292,22 +295,6 @@
lemma real_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::real)"
by (rule Ring_and_Field.inverse_mult_distrib)
-lemma real_times_divide1_eq: "(x::real) * (y/z) = (x*y)/z"
-by (simp add: real_divide_def real_mult_assoc)
-
-lemma real_times_divide2_eq: "(y/z) * (x::real) = (y*x)/z"
-by (simp add: real_divide_def real_mult_ac)
-
-declare real_times_divide1_eq [simp] real_times_divide2_eq [simp]
-
-lemma real_divide_divide1_eq: "(x::real) / (y/z) = (x*z)/y"
-by (simp add: real_divide_def real_inverse_distrib real_mult_ac)
-
-lemma real_divide_divide2_eq: "((x::real) / y) / z = x/(y*z)"
-by (simp add: real_divide_def real_inverse_distrib real_mult_assoc)
-
-declare real_divide_divide1_eq [simp] real_divide_divide2_eq [simp]
-
(** As with multiplication, pull minus signs OUT of the / operator **)
lemma real_minus_divide_eq: "(-x) / (y::real) = - (x/y)"
@@ -376,6 +363,38 @@
by (rule Ring_and_Field.add_le_cancel_left)
+subsection{*Factor Cancellation Theorems for Type @{text real}*}
+
+lemma real_mult_less_cancel2:
+ "(m*k < n*k) = (((0::real) < k & m<n) | (k < 0 & n<m))"
+ by (rule Ring_and_Field.mult_less_cancel_right)
+
+lemma real_mult_le_cancel2:
+ "(m*k <= n*k) = (((0::real) < k --> m<=n) & (k < 0 --> n<=m))"
+ by (rule Ring_and_Field.mult_le_cancel_right)
+
+lemma real_mult_less_cancel1:
+ "(k*m < k*n) = (((0::real) < k & m<n) | (k < 0 & n<m))"
+ by (rule Ring_and_Field.mult_less_cancel_left)
+
+lemma real_mult_le_cancel1:
+ "!!k::real. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))"
+ by (rule Ring_and_Field.mult_le_cancel_left)
+
+lemma real_mult_eq_cancel1: "!!k::real. (k*m = k*n) = (k = 0 | m=n)"
+ by (rule Ring_and_Field.mult_cancel_left)
+
+lemma real_mult_eq_cancel2: "!!k::real. (m*k = n*k) = (k = 0 | m=n)"
+ by (rule Ring_and_Field.mult_cancel_right)
+
+lemma real_mult_div_cancel1: "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)"
+ by (rule Ring_and_Field.mult_divide_cancel_left)
+
+lemma real_mult_div_cancel_disj:
+ "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)"
+ by (rule Ring_and_Field.mult_divide_cancel_eq_if)
+
+
subsection{*For the @{text abel_cancel} Simproc (DELETE)*}
lemma real_eq_eqI: "(x::real) - y = x' - y' ==> (x=y) = (x'=y')"
@@ -563,15 +582,6 @@
lemma real_inverse_less_0: "x < 0 ==> inverse (x::real) < 0"
by (rule Ring_and_Field.negative_imp_inverse_negative)
-lemma real_mult_less_cancel1: "[| (0::real) < z; x * z < y * z |] ==> x < y"
-by (force simp add: Ring_and_Field.mult_less_cancel_right
- elim: order_less_asym)
-
-lemma real_mult_less_cancel2: "[| (0::real) < z; z*x < z*y |] ==> x < y"
-apply (erule real_mult_less_cancel1)
-apply (simp add: real_mult_commute)
-done
-
lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
by (rule Ring_and_Field.mult_strict_right_mono)
@@ -580,17 +590,15 @@
by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
-by (blast intro: real_mult_less_mono1 real_mult_less_cancel1)
+ by (force elim: order_less_asym
+ simp add: Ring_and_Field.mult_less_cancel_right)
-lemma real_mult_less_iff2 [simp]: "(0::real) < z ==> (z*x < z*y) = (x < y)"
-by (blast intro: real_mult_less_mono2 real_mult_less_cancel2)
-
-(* 05/00 *)
lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
by (auto simp add: real_le_def)
lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
-by (auto simp add: real_le_def)
+ by (force elim: order_less_asym
+ simp add: Ring_and_Field.mult_le_cancel_left)
lemma real_mult_less_mono':
"[| x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x|] ==> r1 * x < r2 * y"
@@ -605,17 +613,23 @@
"[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
by (rule Ring_and_Field.less_imp_inverse_less)
+lemma real_inverse_less_iff:
+ "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)"
+by (rule Ring_and_Field.inverse_less_iff_less)
+
+lemma real_inverse_le_iff:
+ "[| 0 < r; 0 < x|] ==> (inverse x \<le> inverse r) = (r \<le> (x::real))"
+by (rule Ring_and_Field.inverse_le_iff_le)
+
+(*FIXME: remove the [iff], since the general theorem is already [simp]*)
lemma real_mult_is_0 [iff]: "(x*y = 0) = (x = 0 | y = (0::real))"
-by auto
+by (rule Ring_and_Field.mult_eq_0_iff)
lemma real_inverse_add: "[| x \<noteq> 0; y \<noteq> 0 |]
==> inverse x + inverse y = (x + y) * inverse (x * (y::real))"
-apply (simp add: real_inverse_distrib real_add_mult_distrib real_mult_assoc [symmetric])
-apply (subst real_mult_assoc)
-apply (rule real_mult_left_commute [THEN subst])
-apply (simp add: real_add_commute)
-done
+by (simp add: Ring_and_Field.inverse_add mult_assoc)
+text{*FIXME: delete or at least combine the next two lemmas*}
lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
apply (drule Ring_and_Field.equals_zero_I [THEN sym])
apply (cut_tac x = y in real_le_square)
@@ -657,13 +671,8 @@
apply (auto intro: real_add_order order_less_imp_le)
done
-(*One use in HahnBanach/Aux.thy*)
-lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
-apply (rule real_less_or_eq_imp_le)
-apply (drule order_le_imp_less_or_eq)
-apply (auto intro: real_mult_less_mono1)
-done
+subsection{*Results About @{term real_of_posnat}: to be Deleted*}
lemma real_of_posnat_gt_zero: "0 < real_of_posnat n"
apply (unfold real_of_posnat_def)
@@ -753,7 +762,8 @@
by auto
lemma real_mult_less_cancel4: "[| (0::real)<z; z*x<z*y |] ==> x<y"
-by auto
+ by (force elim: order_less_asym
+ simp add: Ring_and_Field.mult_less_cancel_left)
lemma real_of_posnat_less_inv_iff: "0 < u ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse(u))"
apply safe
@@ -773,6 +783,13 @@
apply (simp (no_asm) add: real_add_assoc real_of_posnat_inv_le_iff)
done
+(*Used just below and in HahnBanach/Aux.thy*)
+lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
+apply (rule real_less_or_eq_imp_le)
+apply (drule order_le_imp_less_or_eq)
+apply (auto intro: real_mult_less_mono1)
+done
+
lemma real_mult_add_one_minus_ge_zero: "0 < r ==> 0 <= r*(1 + -inverse(real_of_posnat n))"
by (drule real_add_one_minus_inv_ge_zero [THEN real_mult_le_less_mono1], auto)
@@ -953,10 +970,7 @@
val real_of_nat_neg_int = thm "real_of_nat_neg_int";
val real_inverse_gt_0 = thm "real_inverse_gt_0";
val real_inverse_less_0 = thm "real_inverse_less_0";
-val real_mult_less_cancel1 = thm "real_mult_less_cancel1";
-val real_mult_less_cancel2 = thm "real_mult_less_cancel2";
val real_mult_less_iff1 = thm "real_mult_less_iff1";
-val real_mult_less_iff2 = thm "real_mult_less_iff2";
val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
val real_mult_less_mono = thm "real_mult_less_mono";
@@ -986,8 +1000,6 @@
val real_of_posnat_inv_le_iff = thm "real_of_posnat_inv_le_iff";
val real_of_posnat_less_iff = thm "real_of_posnat_less_iff";
val real_of_posnat_le_iff = thm "real_of_posnat_le_iff";
-val real_mult_less_cancel3 = thm "real_mult_less_cancel3";
-val real_mult_less_cancel4 = thm "real_mult_less_cancel4";
val real_of_posnat_less_inv_iff = thm "real_of_posnat_less_inv_iff";
val real_of_posnat_inv_eq_iff = thm "real_of_posnat_inv_eq_iff";
val real_add_one_minus_inv_ge_zero = thm "real_add_one_minus_inv_ge_zero";
@@ -1012,10 +1024,6 @@
val real_inverse_1 = thm"real_inverse_1";
val real_minus_inverse = thm"real_minus_inverse";
val real_inverse_distrib = thm"real_inverse_distrib";
-val real_times_divide1_eq = thm"real_times_divide1_eq";
-val real_times_divide2_eq = thm"real_times_divide2_eq";
-val real_divide_divide1_eq = thm"real_divide_divide1_eq";
-val real_divide_divide2_eq = thm"real_divide_divide2_eq";
val real_minus_divide_eq = thm"real_minus_divide_eq";
val real_divide_minus_eq = thm"real_divide_minus_eq";
val real_add_divide_distrib = thm"real_add_divide_distrib";
--- a/src/HOL/Real/RealPow.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Real/RealPow.thy Wed Dec 10 15:59:34 2003 +0100
@@ -146,9 +146,10 @@
lemma realpow_Suc_less [rule_format]:
"(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
- by (induct_tac "n", auto)
+ by (induct_tac "n", auto simp add: mult_less_cancel_left)
-lemma realpow_Suc_le [rule_format]: "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
+lemma realpow_Suc_le [rule_format]:
+ "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
apply (induct_tac "n")
apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq)
done
@@ -188,7 +189,7 @@
by (induct_tac "n", auto)
lemma realpow_less_Suc [rule_format]: "(1::real) < r --> r ^ n < r ^ Suc n"
-by (induct_tac "n", auto)
+by (induct_tac "n", auto simp add: mult_less_cancel_left)
lemma realpow_le_Suc2 [rule_format]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
by (blast intro!: order_less_imp_le realpow_less_Suc)
--- a/src/HOL/Real/real_arith.ML Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Real/real_arith.ML Wed Dec 10 15:59:34 2003 +0100
@@ -6,11 +6,17 @@
Augmentation of real linear arithmetic with rational coefficient handling
*)
+val real_divide_1 = thm"real_divide_1";
+
local
+val times_divide_eq_left = thm"times_divide_eq_left";
+val times_divide_eq_right = thm"times_divide_eq_right";
+
(* reduce contradictory <= to False *)
-val simps = [True_implies_equals,inst "w" "number_of ?v" real_add_mult_distrib2,
- real_divide_1,real_times_divide1_eq,real_times_divide2_eq];
+val simps = [True_implies_equals,
+ inst "w" "number_of ?v" real_add_mult_distrib2,
+ real_divide_1,times_divide_eq_right,times_divide_eq_left];
val simprocs = [real_cancel_numeral_factors_divide];
--- a/src/HOL/Ring_and_Field.thy Wed Dec 10 14:29:44 2003 +0100
+++ b/src/HOL/Ring_and_Field.thy Wed Dec 10 15:59:34 2003 +0100
@@ -19,7 +19,7 @@
axclass semiring \<subseteq> zero, one, plus, times
add_assoc: "(a + b) + c = a + (b + c)"
add_commute: "a + b = b + a"
- left_zero [simp]: "0 + a = a"
+ add_0 [simp]: "0 + a = a"
mult_assoc: "(a * b) * c = a * (b * c)"
mult_commute: "a * b = b * a"
@@ -52,7 +52,7 @@
subsection {* Derived Rules for Addition *}
-lemma right_zero [simp]: "a + 0 = (a::'a::semiring)"
+lemma add_0_right [simp]: "a + 0 = (a::'a::semiring)"
proof -
have "a + 0 = 0 + a" by (simp only: add_commute)
also have "... = a" by simp
@@ -120,6 +120,9 @@
lemma diff_0_right [simp]: "a - (0::'a::ring) = a"
by (simp add: diff_minus)
+lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::ring)"
+by (simp add: diff_minus)
+
lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))"
proof
assume "- a = - b"
@@ -166,33 +169,6 @@
theorems mult_ac = mult_assoc mult_commute mult_left_commute
-lemma right_inverse [simp]:
- assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
-proof -
- have "a * inverse a = inverse a * a" by (simp add: mult_ac)
- also have "... = 1" using not0 by simp
- finally show ?thesis .
-qed
-
-lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
-proof
- assume neq: "b \<noteq> 0"
- {
- hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
- also assume "a / b = 1"
- finally show "a = b" by simp
- next
- assume "a = b"
- with neq show "a / b = 1" by (simp add: divide_inverse)
- }
-qed
-
-lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
-by (simp add: divide_inverse)
-
-lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
- by (simp add: divide_inverse)
-
lemma mult_left_zero [simp]: "0 * a = (0::'a::ring)"
proof -
have "0*a + 0*a = 0*a + 0"
@@ -690,6 +666,33 @@
subsection {* Fields *}
+lemma right_inverse [simp]:
+ assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
+proof -
+ have "a * inverse a = inverse a * a" by (simp add: mult_ac)
+ also have "... = 1" using not0 by simp
+ finally show ?thesis .
+qed
+
+lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
+proof
+ assume neq: "b \<noteq> 0"
+ {
+ hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
+ also assume "a / b = 1"
+ finally show "a = b" by simp
+ next
+ assume "a = b"
+ with neq show "a / b = 1" by (simp add: divide_inverse)
+ }
+qed
+
+lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
+by (simp add: divide_inverse)
+
+lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
+ by (simp add: divide_inverse)
+
lemma divide_inverse_zero: "a/b = a * inverse(b::'a::{field,division_by_zero})"
apply (case_tac "b = 0")
apply (simp_all add: divide_inverse)
@@ -904,6 +907,22 @@
lemma divide_1 [simp]: "a/1 = (a::'a::field)"
by (simp add: divide_inverse [OF not_sym])
+lemma times_divide_eq_right [simp]:
+ "a * (b/c) = (a*b) / (c::'a::{field,division_by_zero})"
+by (simp add: divide_inverse_zero mult_assoc)
+
+lemma times_divide_eq_left [simp]:
+ "(b/c) * a = (b*a) / (c::'a::{field,division_by_zero})"
+by (simp add: divide_inverse_zero mult_ac)
+
+lemma divide_divide_eq_right [simp]:
+ "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
+by (simp add: divide_inverse_zero mult_ac)
+
+lemma divide_divide_eq_left [simp]:
+ "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
+by (simp add: divide_inverse_zero mult_assoc)
+
subsection {* Ordered Fields *}
@@ -1084,11 +1103,180 @@
by (simp add: divide_inverse_zero zero_le_mult_iff)
lemma divide_le_0_iff:
- "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
+ "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
+ (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
by (simp add: divide_inverse_zero mult_le_0_iff)
lemma divide_eq_0_iff [simp]:
"(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
by (simp add: divide_inverse_zero field_mult_eq_0_iff)
+
+subsection{*Simplification of Inequalities Involving Literal Divisors*}
+
+lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
+proof -
+ assume less: "0<c"
+ hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
+ by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
+ also have "... = (a*c \<le> b)"
+ by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+
+lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
+proof -
+ assume less: "c<0"
+ hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
+ by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
+ also have "... = (b \<le> a*c)"
+ by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma le_divide_eq:
+ "(a \<le> b/c) =
+ (if 0 < c then a*c \<le> b
+ else if c < 0 then b \<le> a*c
+ else a \<le> (0::'a::{ordered_field,division_by_zero}))"
+apply (case_tac "c=0", simp)
+apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)
+done
+
+lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
+proof -
+ assume less: "0<c"
+ hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
+ by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
+ also have "... = (b \<le> a*c)"
+ by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
+proof -
+ assume less: "c<0"
+ hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
+ by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
+ also have "... = (a*c \<le> b)"
+ by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma divide_le_eq:
+ "(b/c \<le> a) =
+ (if 0 < c then b \<le> a*c
+ else if c < 0 then a*c \<le> b
+ else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
+apply (case_tac "c=0", simp)
+apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)
+done
+
+
+lemma pos_less_divide_eq:
+ "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
+proof -
+ assume less: "0<c"
+ hence "(a < b/c) = (a*c < (b/c)*c)"
+ by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+ also have "... = (a*c < b)"
+ by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma neg_less_divide_eq:
+ "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
+proof -
+ assume less: "c<0"
+ hence "(a < b/c) = ((b/c)*c < a*c)"
+ by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+ also have "... = (b < a*c)"
+ by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma less_divide_eq:
+ "(a < b/c) =
+ (if 0 < c then a*c < b
+ else if c < 0 then b < a*c
+ else a < (0::'a::{ordered_field,division_by_zero}))"
+apply (case_tac "c=0", simp)
+apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)
+done
+
+lemma pos_divide_less_eq:
+ "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
+proof -
+ assume less: "0<c"
+ hence "(b/c < a) = ((b/c)*c < a*c)"
+ by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+ also have "... = (b < a*c)"
+ by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma neg_divide_less_eq:
+ "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
+proof -
+ assume less: "c<0"
+ hence "(b/c < a) = (a*c < (b/c)*c)"
+ by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
+ also have "... = (a*c < b)"
+ by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma divide_less_eq:
+ "(b/c < a) =
+ (if 0 < c then b < a*c
+ else if c < 0 then a*c < b
+ else 0 < (a::'a::{ordered_field,division_by_zero}))"
+apply (case_tac "c=0", simp)
+apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)
+done
+
+lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
+proof -
+ assume [simp]: "c\<noteq>0"
+ have "(a = b/c) = (a*c = (b/c)*c)"
+ by (simp add: field_mult_cancel_right)
+ also have "... = (a*c = b)"
+ by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma eq_divide_eq:
+ "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
+by (simp add: nonzero_eq_divide_eq)
+
+lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
+proof -
+ assume [simp]: "c\<noteq>0"
+ have "(b/c = a) = ((b/c)*c = a*c)"
+ by (simp add: field_mult_cancel_right)
+ also have "... = (b = a*c)"
+ by (simp add: divide_inverse mult_assoc)
+ finally show ?thesis .
+qed
+
+lemma divide_eq_eq:
+ "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
+by (force simp add: nonzero_divide_eq_eq)
+
+subsection{*Cancellation Laws for Division*}
+
+lemma divide_cancel_right [simp]:
+ "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
+apply (case_tac "c=0", simp)
+apply (simp add: divide_inverse_zero field_mult_cancel_right)
+done
+
+lemma divide_cancel_left [simp]:
+ "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
+apply (case_tac "c=0", simp)
+apply (simp add: divide_inverse_zero field_mult_cancel_left)
+done
+
+
end