# HG changeset patch # User paulson # Date 1071068374 -3600 # Node ID d149e3cbdb39e5dea45ddc3af0b4c3d434d22ebc # Parent f630017ed01c902b7d3b0a2008653e5d50f9b9c5 Moving some theorems from Real/RealArith0.ML diff -r f630017ed01c -r d149e3cbdb39 doc-src/TutorialI/Types/Numbers.thy --- 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} diff -r f630017ed01c -r d149e3cbdb39 doc-src/TutorialI/Types/document/Numbers.tex --- 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}% diff -r f630017ed01c -r d149e3cbdb39 doc-src/TutorialI/Types/numerics.tex --- 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 diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Complex/ComplexArith0.ML --- 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)"; diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Complex/ex/Sqrt_Script.thy --- 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 = diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Hyperreal/Lim.ML --- 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"; diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Hyperreal/Series.ML --- 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); diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Hyperreal/Transcendental.ML --- 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) x x '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 diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Induct/BinaryTree_Map.thy --- /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 diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Induct/BinaryTree_TacticStyle.thy --- /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 \ 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 diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Induct/ROOT.ML --- 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"; diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Integ/Bin.thy --- 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 \) *) - -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 **) diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Integ/IntDiv.thy --- 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 ar-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\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\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\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 & rr & r 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 \ 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 (a0) 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\a+b | b\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\a then + if 0\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' \ b*q + r; 0 \ r'; 0 < b; r < b |] + ==> q' \ (q::int)" +apply (subgoal_tac "r' + b * (q'-q) \ 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' \ b*q + r; r \ 0; b < 0; b < r' |] + ==> q \ (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 \ 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 \ 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 negDivAlg (a,b) = - (if 0<=a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))" + (if 0\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\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 \ 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 \ 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) \ 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 \ (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 \ 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) \ 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 \ (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 \ 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 \ 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 \ r |] ==> q \ 1" +apply (subgoal_tac "0 \ 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 \ 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 \ 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 \ 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 \ 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 \ a'; 0 < (b::int) |] ==> a div b \ 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 \ a'; (b::int) < 0 |] ==> a' div b \ 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 \ b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \ (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 \ b'*q' + r'; + r' < b'; 0 \ r; 0 < b'; b' \ b |] + ==> q \ (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) \ a; 0 < b'; b' \ b |] ==> a div b \ 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 \ r'; 0 < b' |] ==> q' \ (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 \ r'; 0 < b'; b' \ b |] + ==> q' \ (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' \ 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' \ b |] ==> a div b' \ 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 \ 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 \ 0 |] ==> b * (q mod c) + r \ 0" +apply (subgoal_tac "b * (q mod c) \ 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 \ r; r < b |] ==> 0 \ b * (q mod c) + r" +apply (subgoal_tac "0 \ 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 \ 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 - P(n div k :: int)(n mod k) = (\i j. 0<=j & j P i j)" + P(n div k :: int)(n mod k) = (\i j. 0\j & 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) = (\i j. k P i j)" + P(n div k :: int)(n mod k) = (\i j. k0 & 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 (\i j. 0<=j & j P i)) & - (k<0 --> (\i j. k P i)))" + (0 (\i j. 0\j & j P i)) & + (k<0 --> (\i j. k0 & 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 (\i j. 0<=j & j P j)) & - (k<0 --> (\i j. k P j)))" + (0 (\i j. 0\j & j P j)) & + (k<0 --> (\i j. k0 & 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) \ a ==> (1 + 2*b) div (2*a) = b div a" +proof cases + assume "a=0" + thus ?thesis by simp +next + assume "a\0" and le_a: "0\a" + hence a_pos: "1 \ a" by arith + hence one_less_a2: "1 < 2*a" by arith + hence le_2a: "2 * (1 + b mod a) \ 2 * a" + by (simp add: mult_le_cancel_left zadd_commute [of 1] add1_zle_eq) + with a_pos have "0 \ b mod a" by simp + hence le_addm: "0 \ 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 \ (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 \ x ==> x \ (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) \ 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) \ 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 \ 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) \ 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 \ 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 \ (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) \ 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 \ -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) \ a; b < 0 |] ==> a div b \ 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 \ a div b) = (0 \ 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 \ a div b) = (a \ (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 \ 0 iff a\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 \: 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 \ (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) diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Integ/NatBin.thy --- 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) diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Integ/NatSimprocs.thy --- 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 \) *) + +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 (< \ 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 diff -r f630017ed01c -r d149e3cbdb39 src/HOL/IsaMakefile --- 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 \ diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Numeral.thy --- 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 diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Real/RealArith.thy --- 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 \ (0::real)) = (y \ -x)" +by auto + +lemma real_0_le_add_iff [iff]: "((0::real) \ x+y) = (-x \ 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) \ x-y) = (y \ 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 |] ==> \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 ==> \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"; diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Real/RealArith0.ML --- 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"; diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Real/RealArith0.thy --- 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 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 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 \ (0::real)) = (y \ -x)" -by auto - -lemma real_0_le_add_iff [iff]: "((0::real) \ x+y) = (-x \ 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) \ x-y) = (y \ 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 ((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_le_cancel2, simp) -done - -lemma neg_real_le_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_le_cancel2, simp) -done - -lemma real_le_divide_eq: - "((x::real) \ y/z) = (if 0 y - else if z<0 then y \ x*z - else x\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 (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_le_cancel2, simp) -done - -lemma neg_real_divide_le_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_le_cancel2, simp) -done - - -lemma real_divide_le_eq: - "(y/z \ (x::real)) = (if 0 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_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 ((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 (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 00 ==> ((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\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\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\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 \ inverse r) = (r \ (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 |] ==> \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 ==> \r::real. x < r & r < y" -by (blast intro!: real_less_half_sum real_gt_half_sum) - end diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Real/RealOrd.thy --- 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 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 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 \ y*z) = (x\y)" by (auto simp add: real_le_def) lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \ z*y) = (x\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) \ r1; 0 \ 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 \ inverse r) = (r \ (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 \ 0; y \ 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) \ z; x < y |] ==> x*z \ 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) x (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) \ z; x < y |] ==> x*z \ 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"; diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Real/RealPow.thy --- 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 \ r & r < (1::real) --> r ^ Suc n \ r ^ n" +lemma realpow_Suc_le [rule_format]: + "0 \ r & r < (1::real) --> r ^ Suc n \ 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 \ r ^ Suc n" by (blast intro!: order_less_imp_le realpow_less_Suc) diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Real/real_arith.ML --- 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]; diff -r f630017ed01c -r d149e3cbdb39 src/HOL/Ring_and_Field.thy --- 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 \ 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 \ 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 \ 0 ==> (a / b = 1) = (a = (b::'a::field))" -proof - assume neq: "b \ 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 \ 0 ==> inverse (a::'a::field) = 1/a" -by (simp add: divide_inverse) - -lemma divide_self [simp]: "a \ 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 \ 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 \ 0 ==> (a / b = 1) = (a = (b::'a::field))" +proof + assume neq: "b \ 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 \ 0 ==> inverse (a::'a::field) = 1/a" +by (simp add: divide_inverse) + +lemma divide_self [simp]: "a \ 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 \ (0::'a::{ordered_field,division_by_zero})) = (0 \ a & b \ 0 | a \ 0 & 0 \ b)" + "(a/b \ (0::'a::{ordered_field,division_by_zero})) = + (0 \ a & b \ 0 | a \ 0 & 0 \ 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 \ b/c) = (a*c \ b)" +proof - + assume less: "0 b/c) = (a*c \ (b/c)*c)" + by (simp add: mult_le_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_le_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_le_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 le_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_le_divide_eq neg_le_divide_eq linorder_neq_iff) +done + +lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \ a) = (b \ a*c)" +proof - + assume less: "0 a) = ((b/c)*c \ a*c)" + by (simp add: mult_le_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_le_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_le_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_le_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_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 (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 (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\0 ==> ((a::'a::field) = b/c) = (a*c = b)" +proof - + assume [simp]: "c\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\0 then a*c = b else a=0)" +by (simp add: nonzero_eq_divide_eq) + +lemma nonzero_divide_eq_eq: "c\0 ==> (b/c = (a::'a::field)) = (b = a*c)" +proof - + assume [simp]: "c\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\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