1.1 --- a/doc-src/TutorialI/Types/Numbers.thy Wed Dec 10 14:29:44 2003 +0100
1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy Wed Dec 10 15:59:34 2003 +0100
1.3 @@ -206,17 +206,17 @@
1.4 @{thm[display] realpow_abs[no_vars]}
1.5 \rulename{realpow_abs}
1.6
1.7 -@{thm[display] real_times_divide1_eq[no_vars]}
1.8 -\rulename{real_times_divide1_eq}
1.9 +@{thm[display] times_divide_eq_right[no_vars]}
1.10 +\rulename{times_divide_eq_right}
1.11
1.12 -@{thm[display] real_times_divide2_eq[no_vars]}
1.13 -\rulename{real_times_divide2_eq}
1.14 +@{thm[display] times_divide_eq_left[no_vars]}
1.15 +\rulename{times_divide_eq_left}
1.16
1.17 -@{thm[display] real_divide_divide1_eq[no_vars]}
1.18 -\rulename{real_divide_divide1_eq}
1.19 +@{thm[display] divide_divide_eq_right[no_vars]}
1.20 +\rulename{divide_divide_eq_right}
1.21
1.22 -@{thm[display] real_divide_divide2_eq[no_vars]}
1.23 -\rulename{real_divide_divide2_eq}
1.24 +@{thm[display] divide_divide_eq_left[no_vars]}
1.25 +\rulename{divide_divide_eq_left}
1.26
1.27 @{thm[display] real_minus_divide_eq[no_vars]}
1.28 \rulename{real_minus_divide_eq}
2.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex Wed Dec 10 14:29:44 2003 +0100
2.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Wed Dec 10 15:59:34 2003 +0100
2.3 @@ -335,24 +335,24 @@
2.4 \rulename{realpow_abs}
2.5
2.6 \begin{isabelle}%
2.7 -x\ {\isacharasterisk}\ {\isacharparenleft}y\ {\isacharslash}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isacharasterisk}\ y\ {\isacharslash}\ z%
2.8 +a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c%
2.9 \end{isabelle}
2.10 -\rulename{real_times_divide1_eq}
2.11 +\rulename{times_divide_eq_right}
2.12
2.13 \begin{isabelle}%
2.14 -y\ {\isacharslash}\ z\ {\isacharasterisk}\ x\ {\isacharequal}\ y\ {\isacharasterisk}\ x\ {\isacharslash}\ z%
2.15 +b\ {\isacharslash}\ c\ {\isacharasterisk}\ a\ {\isacharequal}\ b\ {\isacharasterisk}\ a\ {\isacharslash}\ c%
2.16 \end{isabelle}
2.17 -\rulename{real_times_divide2_eq}
2.18 +\rulename{times_divide_eq_left}
2.19
2.20 \begin{isabelle}%
2.21 -x\ {\isacharslash}\ {\isacharparenleft}y\ {\isacharslash}\ z{\isacharparenright}\ {\isacharequal}\ x\ {\isacharasterisk}\ z\ {\isacharslash}\ y%
2.22 +a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ c\ {\isacharslash}\ b%
2.23 \end{isabelle}
2.24 -\rulename{real_divide_divide1_eq}
2.25 +\rulename{divide_divide_eq_right}
2.26
2.27 \begin{isabelle}%
2.28 -x\ {\isacharslash}\ y\ {\isacharslash}\ z\ {\isacharequal}\ x\ {\isacharslash}\ {\isacharparenleft}y\ {\isacharasterisk}\ z{\isacharparenright}%
2.29 +a\ {\isacharslash}\ b\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}%
2.30 \end{isabelle}
2.31 -\rulename{real_divide_divide2_eq}
2.32 +\rulename{divide_divide_eq_left}
2.33
2.34 \begin{isabelle}%
2.35 {\isacharminus}\ x\ {\isacharslash}\ y\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}x\ {\isacharslash}\ y{\isacharparenright}%
3.1 --- a/doc-src/TutorialI/Types/numerics.tex Wed Dec 10 14:29:44 2003 +0100
3.2 +++ b/doc-src/TutorialI/Types/numerics.tex Wed Dec 10 15:59:34 2003 +0100
3.3 @@ -404,14 +404,14 @@
3.4 are installed as default simplification rules in order to express
3.5 combinations of products and quotients as rational expressions:
3.6 \begin{isabelle}
3.7 -x\ *\ (y\ /\ z)\ =\ x\ *\ y\ /\ z
3.8 -\rulename{real_times_divide1_eq}\isanewline
3.9 -y\ /\ z\ *\ x\ =\ y\ *\ x\ /\ z
3.10 -\rulename{real_times_divide2_eq}\isanewline
3.11 -x\ /\ (y\ /\ z)\ =\ x\ *\ z\ /\ y
3.12 -\rulename{real_divide_divide1_eq}\isanewline
3.13 -x\ /\ y\ /\ z\ =\ x\ /\ (y\ *\ z)
3.14 -\rulename{real_divide_divide2_eq}
3.15 +a\ *\ (b\ /\ c)\ =\ a\ *\ b\ /\ c
3.16 +\rulename{times_divide_eq_right}\isanewline
3.17 +b\ /\ c\ *\ a\ =\ b\ *\ a\ /\ c
3.18 +\rulename{times_divide_eq_left}\isanewline
3.19 +a\ /\ (b\ /\ c)\ =\ a\ *\ c\ /\ b
3.20 +\rulename{divide_divide_eq_right}\isanewline
3.21 +a\ /\ b\ /\ c\ =\ a\ /\ (b\ *\ c)
3.22 +\rulename{divide_divide_eq_left}
3.23 \end{isabelle}
3.24
3.25 Signs are extracted from quotients in the hope that complementary terms can
4.1 --- a/src/HOL/Complex/ComplexArith0.ML Wed Dec 10 14:29:44 2003 +0100
4.2 +++ b/src/HOL/Complex/ComplexArith0.ML Wed Dec 10 15:59:34 2003 +0100
4.3 @@ -5,11 +5,6 @@
4.4 Also, common factor cancellation (see e.g. HyperArith0)
4.5 *)
4.6
4.7 -Goal "x - - y = x + (y::complex)";
4.8 -by (Simp_tac 1);
4.9 -qed "real_diff_minus_eq";
4.10 -Addsimps [real_diff_minus_eq];
4.11 -
4.12 (** Division and inverse **)
4.13
4.14 Goal "0/x = (0::complex)";
5.1 --- a/src/HOL/Complex/ex/Sqrt_Script.thy Wed Dec 10 14:29:44 2003 +0100
5.2 +++ b/src/HOL/Complex/ex/Sqrt_Script.thy Wed Dec 10 15:59:34 2003 +0100
5.3 @@ -68,8 +68,7 @@
5.4 apply clarify
5.5 apply (erule_tac P = "real m / real n * ?x = ?y" in rev_mp)
5.6 apply (simp del: real_of_nat_mult
5.7 - add: real_divide_eq_eq prime_not_square
5.8 - real_of_nat_mult [symmetric])
5.9 + add: divide_eq_eq prime_not_square real_of_nat_mult [symmetric])
5.10 done
5.11
5.12 lemmas two_sqrt_irrational =
6.1 --- a/src/HOL/Hyperreal/Lim.ML Wed Dec 10 14:29:44 2003 +0100
6.2 +++ b/src/HOL/Hyperreal/Lim.ML Wed Dec 10 15:59:34 2003 +0100
6.3 @@ -5,6 +5,8 @@
6.4 differentiation of real=>real functions
6.5 *)
6.6
6.7 +val times_divide_eq_right = thm"times_divide_eq_right";
6.8 +
6.9 fun ARITH_PROVE str = prove_goal thy str
6.10 (fn prems => [cut_facts_tac prems 1,arith_tac 1]);
6.11
6.12 @@ -1048,9 +1050,9 @@
6.13 Goal "NSDERIV f x :> D \
6.14 \ ==> NSDERIV (%x. c * f x) x :> c*D";
6.15 by (asm_full_simp_tac
6.16 - (simpset() addsimps [real_times_divide1_eq RS sym, NSDERIV_NSLIM_iff,
6.17 + (simpset() addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff,
6.18 real_minus_mult_eq2, real_add_mult_distrib2 RS sym]
6.19 - delsimps [real_times_divide1_eq, real_mult_minus_eq2]) 1);
6.20 + delsimps [times_divide_eq_right, real_mult_minus_eq2]) 1);
6.21 by (etac (NSLIM_const RS NSLIM_mult) 1);
6.22 qed "NSDERIV_cmult";
6.23
6.24 @@ -1061,9 +1063,9 @@
6.25 "DERIV f x :> D \
6.26 \ ==> DERIV (%x. c * f x) x :> c*D";
6.27 by (asm_full_simp_tac
6.28 - (simpset() addsimps [real_times_divide1_eq RS sym, NSDERIV_NSLIM_iff,
6.29 + (simpset() addsimps [times_divide_eq_right RS sym, NSDERIV_NSLIM_iff,
6.30 real_minus_mult_eq2, real_add_mult_distrib2 RS sym]
6.31 - delsimps [real_times_divide1_eq, real_mult_minus_eq2]) 1);
6.32 + delsimps [times_divide_eq_right, real_mult_minus_eq2]) 1);
6.33 by (etac (LIM_const RS LIM_mult2) 1);
6.34 qed "DERIV_cmult";
6.35
7.1 --- a/src/HOL/Hyperreal/Series.ML Wed Dec 10 14:29:44 2003 +0100
7.2 +++ b/src/HOL/Hyperreal/Series.ML Wed Dec 10 15:59:34 2003 +0100
7.3 @@ -431,7 +431,7 @@
7.4 simpset() addsimps [sumr_geometric ,sums_def,
7.5 real_diff_def, real_add_divide_distrib]));
7.6 by (subgoal_tac "1 / (1 + -x) = 0/(x - 1) + - 1/(x - 1)" 1);
7.7 -by (asm_full_simp_tac (simpset() addsimps [real_divide_eq_cancel1,
7.8 +by (asm_full_simp_tac (simpset() addsimps [
7.9 real_divide_minus_eq RS sym, real_diff_def]) 2);
7.10 by (etac ssubst 1);
7.11 by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_divide 1);
8.1 --- a/src/HOL/Hyperreal/Transcendental.ML Wed Dec 10 14:29:44 2003 +0100
8.2 +++ b/src/HOL/Hyperreal/Transcendental.ML Wed Dec 10 15:59:34 2003 +0100
8.3 @@ -12,6 +12,8 @@
8.4 res_inst_tac [("z",x)] cancel_thm i
8.5 end;
8.6
8.7 +val mult_less_cancel_left = thm"mult_less_cancel_left";
8.8 +
8.9 Goalw [root_def] "root (Suc n) 0 = 0";
8.10 by (safe_tac (claset() addSIs [some_equality,realpow_zero]
8.11 addSEs [realpow_zero_zero]));
8.12 @@ -285,24 +287,24 @@
8.13 by (Step_tac 1);
8.14 by (cut_inst_tac [("x","r")] reals_Archimedean3 1);
8.15 by Auto_tac;
8.16 -by (dres_inst_tac [("x","abs x")] spec 1 THEN Step_tac 1);
8.17 +by (dres_inst_tac [("x","abs x")] spec 1 THEN Safe_tac);
8.18 by (res_inst_tac [("N","n"),("c","r")] ratio_test 1);
8.19 by (auto_tac (claset(),simpset() addsimps [abs_mult,real_mult_assoc RS sym]
8.20 delsimps [fact_Suc]));
8.21 by (rtac real_mult_le_le_mono2 1);
8.22 -by (res_inst_tac [("w1","abs x")] (real_mult_commute RS ssubst) 2);
8.23 +by (res_inst_tac [("b1","abs x")] (mult_commute RS ssubst) 2);
8.24 by (stac fact_Suc 2);
8.25 by (stac real_of_nat_mult 2);
8.26 by (auto_tac (claset(),simpset() addsimps [abs_mult,real_inverse_distrib]));
8.27 by (auto_tac (claset(), simpset() addsimps
8.28 - [real_mult_assoc RS sym, abs_eqI2, real_inverse_gt_0]));
8.29 -by (rtac (CLAIM "x < (y::real) ==> x <= y") 1);
8.30 + [mult_assoc RS sym, abs_eqI2, real_inverse_gt_0]));
8.31 +by (rtac order_less_imp_le 1);
8.32 by (res_inst_tac [("z1","real (Suc na)")] (real_mult_less_iff1
8.33 RS iffD1) 1);
8.34 by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym,
8.35 - real_mult_assoc,abs_inverse]));
8.36 -by (rtac real_less_trans 1);
8.37 -by (auto_tac (claset(),simpset() addsimps real_mult_ac));
8.38 + mult_assoc,abs_inverse]));
8.39 +by (etac order_less_trans 1);
8.40 +by (auto_tac (claset(),simpset() addsimps [mult_less_cancel_left]@mult_ac));
8.41 qed "summable_exp";
8.42
8.43 Addsimps [real_of_nat_fact_gt_zero,
8.44 @@ -636,9 +638,10 @@
8.45 by (res_inst_tac [("R2.0","K * e")] real_less_trans 2);
8.46 by (res_inst_tac [("z","inverse K")] (CLAIM_SIMP
8.47 "[|(0::real) <z; z*x<z*y |] ==> x<y" [real_mult_less_cancel1]) 3);
8.48 -by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 4);
8.49 -by Auto_tac;
8.50 -by (auto_tac (claset(),simpset() addsimps real_mult_ac));
8.51 +by (asm_full_simp_tac (simpset() addsimps [mult_assoc RS sym]) 4);
8.52 +by (Force_tac 1);
8.53 +by (asm_full_simp_tac (simpset() addsimps [mult_less_cancel_left]) 1);
8.54 +by (auto_tac (claset(),simpset() addsimps mult_ac));
8.55 qed "lemma_termdiff4";
8.56
8.57 Goal "[| 0 < k; \
8.58 @@ -1577,11 +1580,12 @@
8.59 by (etac sums_summable 1);
8.60 by (case_tac "m=0" 1);
8.61 by (Asm_simp_tac 1);
8.62 -by (res_inst_tac [("z","real (Suc (Suc (Suc (Suc 2))))")]
8.63 - (CLAIM "[|(0::real)<z; z*x<z*y |] ==> x<y") 1);
8.64 -by (asm_simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym, real_mult_assoc RS sym]) 2);
8.65 -by (stac (CLAIM "6 = 2 * (3::real)") 2);
8.66 -by (rtac real_mult_less_mono 2);
8.67 +by (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x" 1);
8.68 +by (asm_full_simp_tac (HOL_ss addsimps [mult_less_cancel_left]) 1);
8.69 +by (asm_full_simp_tac (simpset() addsimps []) 1);
8.70 +by (asm_simp_tac (simpset() addsimps [numeral_2_eq_2 RS sym, real_mult_assoc RS sym]) 1);
8.71 +by (stac (CLAIM "6 = 2 * (3::real)") 1);
8.72 +by (rtac real_mult_less_mono 1);
8.73 by (auto_tac (claset(),simpset() addsimps [real_of_nat_Suc] delsimps [fact_Suc]));
8.74 by (stac fact_Suc 1);
8.75 by (stac fact_Suc 1);
8.76 @@ -1599,13 +1603,14 @@
8.77 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]
8.78 delsimps [fact_Suc]));
8.79 by (multr_by_tac "real (Suc (Suc (Suc (4*m))))" 1);
8.80 -by (auto_tac (claset(),simpset() addsimps [real_mult_assoc]
8.81 +by (auto_tac (claset(),simpset() addsimps [mult_assoc,mult_less_cancel_left]
8.82 delsimps [fact_Suc]));
8.83 -by (auto_tac (claset(),simpset() addsimps [CLAIM
8.84 - "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * (x::real))"]
8.85 +by (auto_tac (claset(),simpset() addsimps [
8.86 + CLAIM "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * (x::real))"]
8.87 delsimps [fact_Suc]));
8.88 -by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,realpow_gt_zero]
8.89 - delsimps [fact_Suc]));
8.90 +by (subgoal_tac "0 < x ^ (4 * m)" 1);
8.91 +by (asm_simp_tac (simpset() addsimps [realpow_gt_zero]) 2);
8.92 +by (asm_simp_tac (simpset() addsimps [mult_less_cancel_left]) 1);
8.93 by (rtac real_mult_less_mono 1);
8.94 by (ALLGOALS(Asm_simp_tac));
8.95 by (TRYALL(rtac real_less_trans));
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/Induct/BinaryTree.thy Wed Dec 10 15:59:34 2003 +0100
9.3 @@ -0,0 +1,795 @@
9.4 +header {* Isar-style Reasoning for Binary Tree Operations *}
9.5 +theory BinaryTree = Main:
9.6 +
9.7 +text {* We prove correctness of operations on
9.8 + binary search tree implementing a set.
9.9 +
9.10 + This document is GPL.
9.11 +
9.12 + Author: Viktor Kuncak, MIT CSAIL, November 2003 *}
9.13 +
9.14 +(*============================================================*)
9.15 +section {* Tree Definition *}
9.16 +(*============================================================*)
9.17 +
9.18 +datatype 'a Tree = Tip | T "'a Tree" 'a "'a Tree"
9.19 +
9.20 +consts
9.21 + setOf :: "'a Tree => 'a set"
9.22 + -- {* set abstraction of a tree *}
9.23 +primrec
9.24 +"setOf Tip = {}"
9.25 +"setOf (T t1 x t2) = (setOf t1) Un (setOf t2) Un {x}"
9.26 +
9.27 +types
9.28 + -- {* we require index to have an irreflexive total order < *}
9.29 + -- {* apart from that, we do not rely on index being int *}
9.30 + index = int
9.31 +
9.32 +types -- {* hash function type *}
9.33 + 'a hash = "'a => index"
9.34 +
9.35 +constdefs
9.36 + eqs :: "'a hash => 'a => 'a set"
9.37 + -- {* equivalence class of elements with the same hash code *}
9.38 + "eqs h x == {y. h y = h x}"
9.39 +
9.40 +consts
9.41 + sortedTree :: "'a hash => 'a Tree => bool"
9.42 + -- {* check if a tree is sorted *}
9.43 +primrec
9.44 +"sortedTree h Tip = True"
9.45 +"sortedTree h (T t1 x t2) =
9.46 + (sortedTree h t1 &
9.47 + (ALL l: setOf t1. h l < h x) &
9.48 + (ALL r: setOf t2. h x < h r) &
9.49 + sortedTree h t2)"
9.50 +
9.51 +lemma sortLemmaL:
9.52 + "sortedTree h (T t1 x t2) ==> sortedTree h t1" by simp
9.53 +lemma sortLemmaR:
9.54 + "sortedTree h (T t1 x t2) ==> sortedTree h t2" by simp
9.55 +
9.56 +(*============================================================*)
9.57 +section {* Tree Lookup *}
9.58 +(*============================================================*)
9.59 +
9.60 +consts
9.61 + tlookup :: "'a hash => index => 'a Tree => 'a option"
9.62 +primrec
9.63 +"tlookup h k Tip = None"
9.64 +"tlookup h k (T t1 x t2) =
9.65 + (if k < h x then tlookup h k t1
9.66 + else if h x < k then tlookup h k t2
9.67 + else Some x)"
9.68 +
9.69 +lemma tlookup_none:
9.70 +"sortedTree h t & (tlookup h k t = None) -->
9.71 + (ALL x:setOf t. h x ~= k)"
9.72 +apply (induct t)
9.73 +apply auto (* takes some time *)
9.74 +done
9.75 +
9.76 +lemma tlookup_some:
9.77 +"sortedTree h t & (tlookup h k t = Some x) -->
9.78 + x:setOf t & h x = k"
9.79 +apply (induct t)
9.80 +apply auto (* takes some time *)
9.81 +done
9.82 +
9.83 +constdefs
9.84 + sorted_distinct_pred :: "'a hash => 'a => 'a => 'a Tree => bool"
9.85 + -- {* No two elements have the same hash code *}
9.86 + "sorted_distinct_pred h a b t == sortedTree h t &
9.87 + a:setOf t & b:setOf t & h a = h b -->
9.88 + a = b"
9.89 +
9.90 +declare sorted_distinct_pred_def [simp]
9.91 +
9.92 +-- {* for case analysis on three cases *}
9.93 +lemma cases3: "[| C1 ==> G; C2 ==> G; C3 ==> G;
9.94 + C1 | C2 | C3 |] ==> G"
9.95 +by auto
9.96 +
9.97 +text {* @{term sorted_distinct_pred} holds for out trees: *}
9.98 +
9.99 +lemma sorted_distinct: "sorted_distinct_pred h a b t" (is "?P t")
9.100 +proof (induct t)
9.101 + show "?P Tip" by simp
9.102 + fix t1 :: "'a Tree" assume h1: "?P t1"
9.103 + fix t2 :: "'a Tree" assume h2: "?P t2"
9.104 + fix x :: 'a
9.105 + show "?P (T t1 x t2)"
9.106 + proof (unfold sorted_distinct_pred_def, safe)
9.107 + assume s: "sortedTree h (T t1 x t2)"
9.108 + assume adef: "a : setOf (T t1 x t2)"
9.109 + assume bdef: "b : setOf (T t1 x t2)"
9.110 + assume hahb: "h a = h b"
9.111 + from s have s1: "sortedTree h t1" by auto
9.112 + from s have s2: "sortedTree h t2" by auto
9.113 + show "a = b"
9.114 + -- {* We consider 9 cases for the position of a and b are in the tree *}
9.115 + proof -
9.116 + -- {* three cases for a *}
9.117 + from adef have "a : setOf t1 | a = x | a : setOf t2" by auto
9.118 + moreover { assume adef1: "a : setOf t1"
9.119 + have ?thesis
9.120 + proof -
9.121 + -- {* three cases for b *}
9.122 + from bdef have "b : setOf t1 | b = x | b : setOf t2" by auto
9.123 + moreover { assume bdef1: "b : setOf t1"
9.124 + from s1 adef1 bdef1 hahb h1 have ?thesis by simp }
9.125 + moreover { assume bdef1: "b = x"
9.126 + from adef1 bdef1 s have "h a < h b" by auto
9.127 + from this hahb have ?thesis by simp }
9.128 + moreover { assume bdef1: "b : setOf t2"
9.129 + from adef1 s have o1: "h a < h x" by auto
9.130 + from bdef1 s have o2: "h x < h b" by auto
9.131 + from o1 o2 have "h a < h b" by simp
9.132 + from this hahb have ?thesis by simp } -- {* case impossible *}
9.133 + ultimately show ?thesis by blast
9.134 + qed
9.135 + }
9.136 + moreover { assume adef1: "a = x"
9.137 + have ?thesis
9.138 + proof -
9.139 + -- {* three cases for b *}
9.140 + from bdef have "b : setOf t1 | b = x | b : setOf t2" by auto
9.141 + moreover { assume bdef1: "b : setOf t1"
9.142 + from this s have "h b < h x" by auto
9.143 + from this adef1 have "h b < h a" by auto
9.144 + from hahb this have ?thesis by simp } -- {* case impossible *}
9.145 + moreover { assume bdef1: "b = x"
9.146 + from adef1 bdef1 have ?thesis by simp }
9.147 + moreover { assume bdef1: "b : setOf t2"
9.148 + from this s have "h x < h b" by auto
9.149 + from this adef1 have "h a < h b" by simp
9.150 + from hahb this have ?thesis by simp } -- {* case impossible *}
9.151 + ultimately show ?thesis by blast
9.152 + qed
9.153 + }
9.154 + moreover { assume adef1: "a : setOf t2"
9.155 + have ?thesis
9.156 + proof -
9.157 + -- {* three cases for b *}
9.158 + from bdef have "b : setOf t1 | b = x | b : setOf t2" by auto
9.159 + moreover { assume bdef1: "b : setOf t1"
9.160 + from bdef1 s have o1: "h b < h x" by auto
9.161 + from adef1 s have o2: "h x < h a" by auto
9.162 + from o1 o2 have "h b < h a" by simp
9.163 + from this hahb have ?thesis by simp } -- {* case impossible *}
9.164 + moreover { assume bdef1: "b = x"
9.165 + from adef1 bdef1 s have "h b < h a" by auto
9.166 + from this hahb have ?thesis by simp } -- {* case impossible *}
9.167 + moreover { assume bdef1: "b : setOf t2"
9.168 + from s2 adef1 bdef1 hahb h2 have ?thesis by simp }
9.169 + ultimately show ?thesis by blast
9.170 + qed
9.171 + }
9.172 + ultimately show ?thesis by blast
9.173 + qed
9.174 + qed
9.175 +qed
9.176 +
9.177 +lemma tlookup_finds: -- {* if a node is in the tree, lookup finds it *}
9.178 +"sortedTree h t & y:setOf t -->
9.179 + tlookup h (h y) t = Some y"
9.180 +proof safe
9.181 + assume s: "sortedTree h t"
9.182 + assume yint: "y : setOf t"
9.183 + show "tlookup h (h y) t = Some y"
9.184 + proof (cases "tlookup h (h y) t")
9.185 + case None note res = this
9.186 + from s res have "sortedTree h t & (tlookup h (h y) t = None)" by simp
9.187 + from this have o1: "ALL x:setOf t. h x ~= h y" by (simp add: tlookup_none)
9.188 + from o1 yint have "h y ~= h y" by fastsimp (* auto does not work *)
9.189 + from this show ?thesis by simp
9.190 + next case (Some z) note res = this
9.191 + have ls: "sortedTree h t & (tlookup h (h y) t = Some z) -->
9.192 + z:setOf t & h z = h y" by (simp add: tlookup_some)
9.193 + have sd: "sorted_distinct_pred h y z t"
9.194 + by (insert sorted_distinct [of h y z t], simp)
9.195 + (* for some reason simplifier would never guess this substitution *)
9.196 + from s res ls have o1: "z:setOf t & h z = h y" by simp
9.197 + from s yint o1 sd have "y = z" by auto
9.198 + from this res show "tlookup h (h y) t = Some y" by simp
9.199 + qed
9.200 +qed
9.201 +
9.202 +subsection {* Tree membership as a special case of lookup *}
9.203 +
9.204 +constdefs
9.205 + memb :: "'a hash => 'a => 'a Tree => bool"
9.206 + "memb h x t ==
9.207 + (case (tlookup h (h x) t) of
9.208 + None => False
9.209 + | Some z => (x=z))"
9.210 +
9.211 +lemma assumes s: "sortedTree h t"
9.212 + shows memb_spec: "memb h x t = (x : setOf t)"
9.213 +proof (cases "tlookup h (h x) t")
9.214 +case None note tNone = this
9.215 + from tNone have res: "memb h x t = False" by (simp add: memb_def)
9.216 + from s tNone tlookup_none have o1: "ALL y:setOf t. h y ~= h x" by fastsimp
9.217 + have notIn: "x ~: setOf t"
9.218 + proof
9.219 + assume h: "x : setOf t"
9.220 + from h o1 have "h x ~= h x" by fastsimp
9.221 + from this show False by simp
9.222 + qed
9.223 + from res notIn show ?thesis by simp
9.224 +next case (Some z) note tSome = this
9.225 + from s tSome tlookup_some have zin: "z : setOf t" by fastsimp
9.226 + show ?thesis
9.227 + proof (cases "x=z")
9.228 + case True note xez = this
9.229 + from tSome xez have res: "memb h x t" by (simp add: memb_def)
9.230 + from res zin xez show ?thesis by simp
9.231 + next case False note xnez = this
9.232 + from tSome xnez have res: "~ memb h x t" by (simp add: memb_def)
9.233 + have "x ~: setOf t"
9.234 + proof
9.235 + assume xin: "x : setOf t"
9.236 + from s tSome tlookup_some have hzhx: "h x = h z" by fastsimp
9.237 + have o1: "sorted_distinct_pred h x z t"
9.238 + by (insert sorted_distinct [of h x z t], simp)
9.239 + from s xin zin hzhx o1 have "x = z" by fastsimp
9.240 + from this xnez show False by simp
9.241 + qed
9.242 + from this res show ?thesis by simp
9.243 + qed
9.244 +qed
9.245 +
9.246 +declare sorted_distinct_pred_def [simp del]
9.247 +
9.248 +(*============================================================*)
9.249 +section {* Insertion into a Tree *}
9.250 +(*============================================================*)
9.251 +
9.252 +consts
9.253 + binsert :: "'a hash => 'a => 'a Tree => 'a Tree"
9.254 +
9.255 +primrec
9.256 +"binsert h e Tip = (T Tip e Tip)"
9.257 +"binsert h e (T t1 x t2) = (if h e < h x then
9.258 + (T (binsert h e t1) x t2)
9.259 + else
9.260 + (if h x < h e then
9.261 + (T t1 x (binsert h e t2))
9.262 + else (T t1 e t2)))"
9.263 +
9.264 +text {* A technique for proving disjointness of sets. *}
9.265 +lemma disjCond: "[| !! x. [| x:A; x:B |] ==> False |] ==> A Int B = {}"
9.266 +by fastsimp
9.267 +
9.268 +text {* The following is a proof that insertion correctly implements
9.269 + the set interface.
9.270 + Compared to @{text BinaryTree_TacticStyle}, the claim is more
9.271 + difficult, and this time we need to assume as a hypothesis
9.272 + that the tree is sorted. *}
9.273 +
9.274 +lemma binsert_set: "sortedTree h t -->
9.275 + setOf (binsert h e t) = (setOf t) - (eqs h e) Un {e}"
9.276 + (is "?P t")
9.277 +proof (induct t)
9.278 + -- {* base case *}
9.279 + show "?P Tip" by (simp add: eqs_def)
9.280 + -- {* inductition step *}
9.281 + fix t1 :: "'a Tree" assume h1: "?P t1"
9.282 + fix t2 :: "'a Tree" assume h2: "?P t2"
9.283 + fix x :: 'a
9.284 + show "?P (T t1 x t2)"
9.285 + proof
9.286 + assume s: "sortedTree h (T t1 x t2)"
9.287 + from s have s1: "sortedTree h t1" by (rule sortLemmaL)
9.288 + from s1 and h1 have c1: "setOf (binsert h e t1) = setOf t1 - eqs h e Un {e}" by simp
9.289 + from s have s2: "sortedTree h t2" by (rule sortLemmaR)
9.290 + from s2 and h2 have c2: "setOf (binsert h e t2) = setOf t2 - eqs h e Un {e}" by simp
9.291 + show "setOf (binsert h e (T t1 x t2)) =
9.292 + setOf (T t1 x t2) - eqs h e Un {e}"
9.293 + proof (cases "h e < h x")
9.294 + case True note eLess = this
9.295 + from eLess have res: "binsert h e (T t1 x t2) = (T (binsert h e t1) x t2)" by simp
9.296 + show "setOf (binsert h e (T t1 x t2)) =
9.297 + setOf (T t1 x t2) - eqs h e Un {e}"
9.298 + proof (simp add: res eLess c1)
9.299 + show "insert x (insert e (setOf t1 - eqs h e Un setOf t2)) =
9.300 + insert e (insert x (setOf t1 Un setOf t2) - eqs h e)"
9.301 + proof -
9.302 + have eqsLessX: "ALL el: eqs h e. h el < h x" by (simp add: eqs_def eLess)
9.303 + from this have eqsDisjX: "ALL el: eqs h e. h el ~= h x" by fastsimp
9.304 + from s have xLessT2: "ALL r: setOf t2. h x < h r" by auto
9.305 + have eqsLessT2: "ALL el: eqs h e. ALL r: setOf t2. h el < h r"
9.306 + proof safe
9.307 + fix el assume hel: "el : eqs h e"
9.308 + from hel eqs_def have o1: "h el = h e" by fastsimp (* auto fails here! *)
9.309 + fix r assume hr: "r : setOf t2"
9.310 + from xLessT2 hr o1 eLess show "h el < h r" by auto
9.311 + qed
9.312 + from eqsLessT2 have eqsDisjT2: "ALL el: eqs h e. ALL r: setOf t2. h el ~= h r"
9.313 + by fastsimp (* auto fails here *)
9.314 + from eqsDisjX eqsDisjT2 show ?thesis by fastsimp
9.315 + qed
9.316 + qed
9.317 + next case False note eNotLess = this
9.318 + show "setOf (binsert h e (T t1 x t2)) = setOf (T t1 x t2) - eqs h e Un {e}"
9.319 + proof (cases "h x < h e")
9.320 + case True note xLess = this
9.321 + from xLess have res: "binsert h e (T t1 x t2) = (T t1 x (binsert h e t2))" by simp
9.322 + show "setOf (binsert h e (T t1 x t2)) =
9.323 + setOf (T t1 x t2) - eqs h e Un {e}"
9.324 + proof (simp add: res xLess eNotLess c2)
9.325 + show "insert x (insert e (setOf t1 Un (setOf t2 - eqs h e))) =
9.326 + insert e (insert x (setOf t1 Un setOf t2) - eqs h e)"
9.327 + proof -
9.328 + have XLessEqs: "ALL el: eqs h e. h x < h el" by (simp add: eqs_def xLess)
9.329 + from this have eqsDisjX: "ALL el: eqs h e. h el ~= h x" by auto
9.330 + from s have t1LessX: "ALL l: setOf t1. h l < h x" by auto
9.331 + have T1lessEqs: "ALL el: eqs h e. ALL l: setOf t1. h l < h el"
9.332 + proof safe
9.333 + fix el assume hel: "el : eqs h e"
9.334 + fix l assume hl: "l : setOf t1"
9.335 + from hel eqs_def have o1: "h el = h e" by fastsimp (* auto fails here! *)
9.336 + from t1LessX hl o1 xLess show "h l < h el" by auto
9.337 + qed
9.338 + from T1lessEqs have T1disjEqs: "ALL el: eqs h e. ALL l: setOf t1. h el ~= h l"
9.339 + by fastsimp
9.340 + from eqsDisjX T1lessEqs show ?thesis by auto
9.341 + qed
9.342 + qed
9.343 + next case False note xNotLess = this
9.344 + from xNotLess eNotLess have xeqe: "h x = h e" by simp
9.345 + from xeqe have res: "binsert h e (T t1 x t2) = (T t1 e t2)" by simp
9.346 + show "setOf (binsert h e (T t1 x t2)) =
9.347 + setOf (T t1 x t2) - eqs h e Un {e}"
9.348 + proof (simp add: res eNotLess xeqe)
9.349 + show "insert e (setOf t1 Un setOf t2) =
9.350 + insert e (insert x (setOf t1 Un setOf t2) - eqs h e)"
9.351 + proof -
9.352 + have "insert x (setOf t1 Un setOf t2) - eqs h e =
9.353 + setOf t1 Un setOf t2"
9.354 + proof -
9.355 + have (* o1: *) "x : eqs h e" by (simp add: eqs_def xeqe)
9.356 + moreover have (* o2: *) "(setOf t1) Int (eqs h e) = {}"
9.357 + proof (rule disjCond)
9.358 + fix w
9.359 + assume whSet: "w : setOf t1"
9.360 + assume whEq: "w : eqs h e"
9.361 + from whSet s have o1: "h w < h x" by simp
9.362 + from whEq eqs_def have o2: "h w = h e" by fastsimp
9.363 + from o2 xeqe have o3: "~ h w < h x" by simp
9.364 + from o1 o3 show False by contradiction
9.365 + qed
9.366 + moreover have (* o3: *) "(setOf t2) Int (eqs h e) = {}"
9.367 + proof (rule disjCond)
9.368 + fix w
9.369 + assume whSet: "w : setOf t2"
9.370 + assume whEq: "w : eqs h e"
9.371 + from whSet s have o1: "h x < h w" by simp
9.372 + from whEq eqs_def have o2: "h w = h e" by fastsimp
9.373 + from o2 xeqe have o3: "~ h x < h w" by simp
9.374 + from o1 o3 show False by contradiction
9.375 + qed
9.376 + ultimately show ?thesis by auto
9.377 + qed
9.378 + from this show ?thesis by simp
9.379 + qed
9.380 + qed
9.381 + qed
9.382 + qed
9.383 + qed
9.384 +qed
9.385 +
9.386 +text {* Using the correctness of set implementation,
9.387 + preserving sortedness is still simple. *}
9.388 +lemma binsert_sorted: "sortedTree h t --> sortedTree h (binsert h x t)"
9.389 +by (induct t) (auto simp add: binsert_set)
9.390 +
9.391 +text {* We summarize the specification of binsert as follows. *}
9.392 +corollary binsert_spec: "sortedTree h t -->
9.393 + sortedTree h (binsert h x t) &
9.394 + setOf (binsert h e t) = (setOf t) - (eqs h e) Un {e}"
9.395 +by (simp add: binsert_set binsert_sorted)
9.396 +
9.397 +(*============================================================*)
9.398 +section {* Removing an element from a tree *}
9.399 +(*============================================================*)
9.400 +
9.401 +text {* These proofs are influenced by those in @{text BinaryTree_Tactic} *}
9.402 +
9.403 +consts
9.404 + rm :: "'a hash => 'a Tree => 'a"
9.405 + -- {* rightmost element of a tree *}
9.406 +primrec
9.407 +"rm h (T t1 x t2) =
9.408 + (if t2=Tip then x else rm h t2)"
9.409 +
9.410 +consts
9.411 + wrm :: "'a hash => 'a Tree => 'a Tree"
9.412 + -- {* tree without the rightmost element *}
9.413 +primrec
9.414 +"wrm h (T t1 x t2) =
9.415 + (if t2=Tip then t1 else (T t1 x (wrm h t2)))"
9.416 +
9.417 +consts
9.418 + wrmrm :: "'a hash => 'a Tree => 'a Tree * 'a"
9.419 + -- {* computing rightmost and removal in one pass *}
9.420 +primrec
9.421 +"wrmrm h (T t1 x t2) =
9.422 + (if t2=Tip then (t1,x)
9.423 + else (T t1 x (fst (wrmrm h t2)),
9.424 + snd (wrmrm h t2)))"
9.425 +
9.426 +consts
9.427 + remove :: "'a hash => 'a => 'a Tree => 'a Tree"
9.428 + -- {* removal of an element from the tree *}
9.429 +primrec
9.430 +"remove h e Tip = Tip"
9.431 +"remove h e (T t1 x t2) =
9.432 + (if h e < h x then (T (remove h e t1) x t2)
9.433 + else if h x < h e then (T t1 x (remove h e t2))
9.434 + else (if t1=Tip then t2
9.435 + else let (t1p,r) = wrmrm h t1
9.436 + in (T t1p r t2)))"
9.437 +
9.438 +theorem wrmrm_decomp: "t ~= Tip --> wrmrm h t = (wrm h t, rm h t)"
9.439 +apply (induct_tac t)
9.440 +apply simp_all
9.441 +done
9.442 +
9.443 +lemma rm_set: "t ~= Tip & sortedTree h t --> rm h t : setOf t"
9.444 +apply (induct_tac t)
9.445 +apply simp_all
9.446 +done
9.447 +
9.448 +lemma wrm_set: "t ~= Tip & sortedTree h t -->
9.449 + setOf (wrm h t) = setOf t - {rm h t}" (is "?P t")
9.450 +proof (induct t)
9.451 + show "?P Tip" by simp
9.452 + fix t1 :: "'a Tree" assume h1: "?P t1"
9.453 + fix t2 :: "'a Tree" assume h2: "?P t2"
9.454 + fix x :: 'a
9.455 + show "?P (T t1 x t2)"
9.456 + proof (rule impI, erule conjE)
9.457 + assume s: "sortedTree h (T t1 x t2)"
9.458 + show "setOf (wrm h (T t1 x t2)) =
9.459 + setOf (T t1 x t2) - {rm h (T t1 x t2)}"
9.460 + proof (cases "t2 = Tip")
9.461 + case True note t2tip = this
9.462 + from t2tip have rm_res: "rm h (T t1 x t2) = x" by simp
9.463 + from t2tip have wrm_res: "wrm h (T t1 x t2) = t1" by simp
9.464 + from s have "x ~: setOf t1" by auto
9.465 + from this rm_res wrm_res t2tip show ?thesis by simp
9.466 + next case False note t2nTip = this
9.467 + from t2nTip have rm_res: "rm h (T t1 x t2) = rm h t2" by simp
9.468 + from t2nTip have wrm_res: "wrm h (T t1 x t2) = T t1 x (wrm h t2)" by simp
9.469 + from s have s2: "sortedTree h t2" by simp
9.470 + from h2 t2nTip s2
9.471 + have o1: "setOf (wrm h t2) = setOf t2 - {rm h t2}" by simp
9.472 + show ?thesis
9.473 + proof (simp add: rm_res wrm_res t2nTip h2 o1)
9.474 + show "insert x (setOf t1 Un (setOf t2 - {rm h t2})) =
9.475 + insert x (setOf t1 Un setOf t2) - {rm h t2}"
9.476 + proof -
9.477 + from s rm_set t2nTip have xOk: "h x < h (rm h t2)" by auto
9.478 + have t1Ok: "ALL l:setOf t1. h l < h (rm h t2)"
9.479 + proof safe
9.480 + fix l :: 'a assume ldef: "l : setOf t1"
9.481 + from ldef s have lx: "h l < h x" by auto
9.482 + from lx xOk show "h l < h (rm h t2)" by auto
9.483 + qed
9.484 + from xOk t1Ok show ?thesis by auto
9.485 + qed
9.486 + qed
9.487 + qed
9.488 + qed
9.489 +qed
9.490 +
9.491 +lemma wrm_set1: "t ~= Tip & sortedTree h t --> setOf (wrm h t) <= setOf t"
9.492 +by (auto simp add: wrm_set)
9.493 +
9.494 +lemma wrm_sort: "t ~= Tip & sortedTree h t --> sortedTree h (wrm h t)" (is "?P t")
9.495 +proof (induct t)
9.496 + show "?P Tip" by simp
9.497 + fix t1 :: "'a Tree" assume h1: "?P t1"
9.498 + fix t2 :: "'a Tree" assume h2: "?P t2"
9.499 + fix x :: 'a
9.500 + show "?P (T t1 x t2)"
9.501 + proof safe
9.502 + assume s: "sortedTree h (T t1 x t2)"
9.503 + show "sortedTree h (wrm h (T t1 x t2))"
9.504 + proof (cases "t2 = Tip")
9.505 + case True note t2tip = this
9.506 + from t2tip have res: "wrm h (T t1 x t2) = t1" by simp
9.507 + from res s show ?thesis by simp
9.508 + next case False note t2nTip = this
9.509 + from t2nTip have res: "wrm h (T t1 x t2) = T t1 x (wrm h t2)" by simp
9.510 + from s have s1: "sortedTree h t1" by simp
9.511 + from s have s2: "sortedTree h t2" by simp
9.512 + from s2 h2 t2nTip have o1: "sortedTree h (wrm h t2)" by simp
9.513 + from s2 t2nTip wrm_set1 have o2: "setOf (wrm h t2) <= setOf t2" by auto
9.514 + from s o2 have o3: "ALL r: setOf (wrm h t2). h x < h r" by auto
9.515 + from s1 o1 o3 res s show "sortedTree h (wrm h (T t1 x t2))" by simp
9.516 + qed
9.517 + qed
9.518 +qed
9.519 +
9.520 +lemma wrm_less_rm:
9.521 + "t ~= Tip & sortedTree h t -->
9.522 + (ALL l:setOf (wrm h t). h l < h (rm h t))" (is "?P t")
9.523 +proof (induct t)
9.524 + show "?P Tip" by simp
9.525 + fix t1 :: "'a Tree" assume h1: "?P t1"
9.526 + fix t2 :: "'a Tree" assume h2: "?P t2"
9.527 + fix x :: 'a
9.528 + show "?P (T t1 x t2)"
9.529 + proof safe
9.530 + fix l :: "'a" assume ldef: "l : setOf (wrm h (T t1 x t2))"
9.531 + assume s: "sortedTree h (T t1 x t2)"
9.532 + from s have s1: "sortedTree h t1" by simp
9.533 + from s have s2: "sortedTree h t2" by simp
9.534 + show "h l < h (rm h (T t1 x t2))"
9.535 + proof (cases "t2 = Tip")
9.536 + case True note t2tip = this
9.537 + from t2tip have rm_res: "rm h (T t1 x t2) = x" by simp
9.538 + from t2tip have wrm_res: "wrm h (T t1 x t2) = t1" by simp
9.539 + from ldef wrm_res have o1: "l : setOf t1" by simp
9.540 + from rm_res o1 s show ?thesis by simp
9.541 + next case False note t2nTip = this
9.542 + from t2nTip have rm_res: "rm h (T t1 x t2) = rm h t2" by simp
9.543 + from t2nTip have wrm_res: "wrm h (T t1 x t2) = T t1 x (wrm h t2)" by simp
9.544 + from ldef wrm_res
9.545 + have l_scope: "l : {x} Un setOf t1 Un setOf (wrm h t2)" by simp
9.546 + have hLess: "h l < h (rm h t2)"
9.547 + proof (cases "l = x")
9.548 + case True note lx = this
9.549 + from s t2nTip rm_set s2 have o1: "h x < h (rm h t2)" by auto
9.550 + from lx o1 show ?thesis by simp
9.551 + next case False note lnx = this
9.552 + show ?thesis
9.553 + proof (cases "l : setOf t1")
9.554 + case True note l_in_t1 = this
9.555 + from s t2nTip rm_set s2 have o1: "h x < h (rm h t2)" by auto
9.556 + from l_in_t1 s have o2: "h l < h x" by auto
9.557 + from o1 o2 show ?thesis by simp
9.558 + next case False note l_notin_t1 = this
9.559 + from l_scope lnx l_notin_t1
9.560 + have l_in_res: "l : setOf (wrm h t2)" by auto
9.561 + from l_in_res h2 t2nTip s2 show ?thesis by auto
9.562 + qed
9.563 + qed
9.564 + from rm_res hLess show ?thesis by simp
9.565 + qed
9.566 + qed
9.567 +qed
9.568 +
9.569 +lemma remove_set: "sortedTree h t -->
9.570 + setOf (remove h e t) = setOf t - eqs h e" (is "?P t")
9.571 +proof (induct t)
9.572 + show "?P Tip" by auto
9.573 + fix t1 :: "'a Tree" assume h1: "?P t1"
9.574 + fix t2 :: "'a Tree" assume h2: "?P t2"
9.575 + fix x :: 'a
9.576 + show "?P (T t1 x t2)"
9.577 + proof
9.578 + assume s: "sortedTree h (T t1 x t2)"
9.579 + show "setOf (remove h e (T t1 x t2)) = setOf (T t1 x t2) - eqs h e"
9.580 + proof (cases "h e < h x")
9.581 + case True note elx = this
9.582 + from elx have res: "remove h e (T t1 x t2) = T (remove h e t1) x t2"
9.583 + by simp
9.584 + from s have s1: "sortedTree h t1" by simp
9.585 + from s1 h1 have o1: "setOf (remove h e t1) = setOf t1 - eqs h e" by simp
9.586 + show ?thesis
9.587 + proof (simp add: o1 elx)
9.588 + show "insert x (setOf t1 - eqs h e Un setOf t2) =
9.589 + insert x (setOf t1 Un setOf t2) - eqs h e"
9.590 + proof -
9.591 + have xOk: "x ~: eqs h e"
9.592 + proof
9.593 + assume h: "x : eqs h e"
9.594 + from h have o1: "~ (h e < h x)" by (simp add: eqs_def)
9.595 + from elx o1 show "False" by contradiction
9.596 + qed
9.597 + have t2Ok: "(setOf t2) Int (eqs h e) = {}"
9.598 + proof (rule disjCond)
9.599 + fix y :: 'a
9.600 + assume y_in_t2: "y : setOf t2"
9.601 + assume y_in_eq: "y : eqs h e"
9.602 + from y_in_t2 s have xly: "h x < h y" by auto
9.603 + from y_in_eq have eey: "h y = h e" by (simp add: eqs_def) (* must "add:" not "from" *)
9.604 + from xly eey have nelx: "~ (h e < h x)" by simp
9.605 + from nelx elx show False by contradiction
9.606 + qed
9.607 + from xOk t2Ok show ?thesis by auto
9.608 + qed
9.609 + qed
9.610 + next case False note nelx = this
9.611 + show ?thesis
9.612 + proof (cases "h x < h e")
9.613 + case True note xle = this
9.614 + from xle have res: "remove h e (T t1 x t2) = T t1 x (remove h e t2)" by simp
9.615 + from s have s2: "sortedTree h t2" by simp
9.616 + from s2 h2 have o1: "setOf (remove h e t2) = setOf t2 - eqs h e" by simp
9.617 + show ?thesis
9.618 + proof (simp add: o1 xle nelx)
9.619 + show "insert x (setOf t1 Un (setOf t2 - eqs h e)) =
9.620 + insert x (setOf t1 Un setOf t2) - eqs h e"
9.621 + proof -
9.622 + have xOk: "x ~: eqs h e"
9.623 + proof
9.624 + assume h: "x : eqs h e"
9.625 + from h have o1: "~ (h x < h e)" by (simp add: eqs_def)
9.626 + from xle o1 show "False" by contradiction
9.627 + qed
9.628 + have t1Ok: "(setOf t1) Int (eqs h e) = {}"
9.629 + proof (rule disjCond)
9.630 + fix y :: 'a
9.631 + assume y_in_t1: "y : setOf t1"
9.632 + assume y_in_eq: "y : eqs h e"
9.633 + from y_in_t1 s have ylx: "h y < h x" by auto
9.634 + from y_in_eq have eey: "h y = h e" by (simp add: eqs_def)
9.635 + from ylx eey have nxle: "~ (h x < h e)" by simp
9.636 + from nxle xle show False by contradiction
9.637 + qed
9.638 + from xOk t1Ok show ?thesis by auto
9.639 + qed
9.640 + qed
9.641 + next case False note nxle = this
9.642 + from nelx nxle have ex: "h e = h x" by simp
9.643 + have t2Ok: "(setOf t2) Int (eqs h e) = {}"
9.644 + proof (rule disjCond)
9.645 + fix y :: 'a
9.646 + assume y_in_t2: "y : setOf t2"
9.647 + assume y_in_eq: "y : eqs h e"
9.648 + from y_in_t2 s have xly: "h x < h y" by auto
9.649 + from y_in_eq have eey: "h y = h e" by (simp add: eqs_def)
9.650 + from y_in_eq ex eey have nxly: "~ (h x < h y)" by simp
9.651 + from nxly xly show False by contradiction
9.652 + qed
9.653 + show ?thesis
9.654 + proof (cases "t1 = Tip")
9.655 + case True note t1tip = this
9.656 + from ex t1tip have res: "remove h e (T t1 x t2) = t2" by simp
9.657 + show ?thesis
9.658 + proof (simp add: res t1tip ex)
9.659 + show "setOf t2 = insert x (setOf t2) - eqs h e"
9.660 + proof -
9.661 + from ex have x_in_eqs: "x : eqs h e" by (simp add: eqs_def)
9.662 + from x_in_eqs t2Ok show ?thesis by auto
9.663 + qed
9.664 + qed
9.665 + next case False note t1nTip = this
9.666 + from nelx nxle ex t1nTip
9.667 + have res: "remove h e (T t1 x t2) =
9.668 + T (wrm h t1) (rm h t1) t2"
9.669 + by (simp add: Let_def wrmrm_decomp)
9.670 + from res show ?thesis
9.671 + proof simp
9.672 + from s have s1: "sortedTree h t1" by simp
9.673 + show "insert (rm h t1) (setOf (wrm h t1) Un setOf t2) =
9.674 + insert x (setOf t1 Un setOf t2) - eqs h e"
9.675 + proof (simp add: t1nTip s1 rm_set wrm_set)
9.676 + show "insert (rm h t1) (setOf t1 - {rm h t1} Un setOf t2) =
9.677 + insert x (setOf t1 Un setOf t2) - eqs h e"
9.678 + proof -
9.679 + from t1nTip s1 rm_set
9.680 + have o1: "insert (rm h t1) (setOf t1 - {rm h t1} Un setOf t2) =
9.681 + setOf t1 Un setOf t2" by auto
9.682 + have o2: "insert x (setOf t1 Un setOf t2) - eqs h e =
9.683 + setOf t1 Un setOf t2"
9.684 + proof -
9.685 + from ex have xOk: "x : eqs h e" by (simp add: eqs_def)
9.686 + have t1Ok: "(setOf t1) Int (eqs h e) = {}"
9.687 + proof (rule disjCond)
9.688 + fix y :: 'a
9.689 + assume y_in_t1: "y : setOf t1"
9.690 + assume y_in_eq: "y : eqs h e"
9.691 + from y_in_t1 s ex have o1: "h y < h e" by auto
9.692 + from y_in_eq have o2: "~ (h y < h e)" by (simp add: eqs_def)
9.693 + from o1 o2 show False by contradiction
9.694 + qed
9.695 + from xOk t1Ok t2Ok show ?thesis by auto
9.696 + qed
9.697 + from o1 o2 show ?thesis by simp
9.698 + qed
9.699 + qed
9.700 + qed
9.701 + qed
9.702 + qed
9.703 + qed
9.704 + qed
9.705 +qed
9.706 +
9.707 +lemma remove_sort: "sortedTree h t -->
9.708 + sortedTree h (remove h e t)" (is "?P t")
9.709 +proof (induct t)
9.710 + show "?P Tip" by auto
9.711 + fix t1 :: "'a Tree" assume h1: "?P t1"
9.712 + fix t2 :: "'a Tree" assume h2: "?P t2"
9.713 + fix x :: 'a
9.714 + show "?P (T t1 x t2)"
9.715 + proof
9.716 + assume s: "sortedTree h (T t1 x t2)"
9.717 + from s have s1: "sortedTree h t1" by simp
9.718 + from s have s2: "sortedTree h t2" by simp
9.719 + from h1 s1 have sr1: "sortedTree h (remove h e t1)" by simp
9.720 + from h2 s2 have sr2: "sortedTree h (remove h e t2)" by simp
9.721 + show "sortedTree h (remove h e (T t1 x t2))"
9.722 + proof (cases "h e < h x")
9.723 + case True note elx = this
9.724 + from elx have res: "remove h e (T t1 x t2) = T (remove h e t1) x t2"
9.725 + by simp
9.726 + show ?thesis
9.727 + proof (simp add: s sr1 s2 elx res)
9.728 + let ?C1 = "ALL l:setOf (remove h e t1). h l < h x"
9.729 + let ?C2 = "ALL r:setOf t2. h x < h r"
9.730 + have o1: "?C1"
9.731 + proof -
9.732 + from s1 have "setOf (remove h e t1) = setOf t1 - eqs h e" by (simp add: remove_set)
9.733 + from s this show ?thesis by auto
9.734 + qed
9.735 + from o1 s show "?C1 & ?C2" by auto
9.736 + qed
9.737 + next case False note nelx = this
9.738 + show ?thesis
9.739 + proof (cases "h x < h e")
9.740 + case True note xle = this
9.741 + from xle have res: "remove h e (T t1 x t2) = T t1 x (remove h e t2)" by simp
9.742 + show ?thesis
9.743 + proof (simp add: s s1 sr2 xle nelx res)
9.744 + let ?C1 = "ALL l:setOf t1. h l < h x"
9.745 + let ?C2 = "ALL r:setOf (remove h e t2). h x < h r"
9.746 + have o2: "?C2"
9.747 + proof -
9.748 + from s2 have "setOf (remove h e t2) = setOf t2 - eqs h e" by (simp add: remove_set)
9.749 + from s this show ?thesis by auto
9.750 + qed
9.751 + from o2 s show "?C1 & ?C2" by auto
9.752 + qed
9.753 + next case False note nxle = this
9.754 + from nelx nxle have ex: "h e = h x" by simp
9.755 + show ?thesis
9.756 + proof (cases "t1 = Tip")
9.757 + case True note t1tip = this
9.758 + from ex t1tip have res: "remove h e (T t1 x t2) = t2" by simp
9.759 + show ?thesis by (simp add: res t1tip ex s2)
9.760 + next case False note t1nTip = this
9.761 + from nelx nxle ex t1nTip
9.762 + have res: "remove h e (T t1 x t2) =
9.763 + T (wrm h t1) (rm h t1) t2"
9.764 + by (simp add: Let_def wrmrm_decomp)
9.765 + from res show ?thesis
9.766 + proof simp
9.767 + let ?C1 = "sortedTree h (wrm h t1)"
9.768 + let ?C2 = "ALL l:setOf (wrm h t1). h l < h (rm h t1)"
9.769 + let ?C3 = "ALL r:setOf t2. h (rm h t1) < h r"
9.770 + let ?C4 = "sortedTree h t2"
9.771 + from s1 t1nTip have o1: ?C1 by (simp add: wrm_sort)
9.772 + from s1 t1nTip have o2: ?C2 by (simp add: wrm_less_rm)
9.773 + have o3: ?C3
9.774 + proof
9.775 + fix r :: 'a
9.776 + assume rt2: "r : setOf t2"
9.777 + from s rm_set s1 t1nTip have o1: "h (rm h t1) < h x" by auto
9.778 + from rt2 s have o2: "h x < h r" by auto
9.779 + from o1 o2 show "h (rm h t1) < h r" by simp
9.780 + qed
9.781 + from o1 o2 o3 s2 show "?C1 & ?C2 & ?C3 & ?C4" by simp
9.782 + qed
9.783 + qed
9.784 + qed
9.785 + qed
9.786 + qed
9.787 +qed
9.788 +
9.789 +text {* We summarize the specification of remove as follows. *}
9.790 +corollary remove_spec: "sortedTree h t -->
9.791 + sortedTree h (remove h e t) &
9.792 + setOf (remove h e t) = setOf t - eqs h e"
9.793 +by (simp add: remove_sort remove_set)
9.794 +
9.795 +generate_code ("BinaryTree_Code.ML")
9.796 + test = "tlookup id 4 (remove id 3 (binsert id 4 (binsert id 3 Tip)))"
9.797 +
9.798 +end
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/Induct/BinaryTree_Map.thy Wed Dec 10 15:59:34 2003 +0100
10.3 @@ -0,0 +1,257 @@
10.4 +header {* Mostly Isar-style Reasoning for Binary Tree Operations *}
10.5 +theory BinaryTree_Map = BinaryTree:
10.6 +
10.7 +text {* We prove correctness of map operations
10.8 + implemented using binary search trees from BinaryTree.
10.9 +
10.10 + This document is GPL.
10.11 +
10.12 + Author: Viktor Kuncak, MIT CSAIL, November 2003 *}
10.13 +
10.14 +
10.15 +(*============================================================*)
10.16 +section {* Map implementation and an abstraction function *}
10.17 +(*============================================================*)
10.18 +
10.19 +types
10.20 + 'a tarray = "(index * 'a) Tree"
10.21 +
10.22 +constdefs
10.23 + valid_tmap :: "'a tarray => bool"
10.24 + "valid_tmap t == sortedTree fst t"
10.25 +
10.26 +declare valid_tmap_def [simp]
10.27 +
10.28 +constdefs
10.29 + mapOf :: "'a tarray => index => 'a option"
10.30 + -- {* the abstraction function from trees to maps *}
10.31 + "mapOf t i ==
10.32 + (case (tlookup fst i t) of
10.33 + None => None
10.34 + | Some ia => Some (snd ia))"
10.35 +
10.36 +(*============================================================*)
10.37 +section {* Auxiliary Properties of our Implementation *}
10.38 +(*============================================================*)
10.39 +
10.40 +lemma mapOf_lookup1: "tlookup fst i t = None ==> mapOf t i = None"
10.41 +by (simp add: mapOf_def)
10.42 +
10.43 +lemma mapOf_lookup2: "tlookup fst i t = Some (j,a) ==> mapOf t i = Some a"
10.44 +by (simp add: mapOf_def)
10.45 +
10.46 +lemma assumes h: "mapOf t i = None"
10.47 + shows mapOf_lookup3: "tlookup fst i t = None"
10.48 +proof (cases "tlookup fst i t")
10.49 +case None from this show ?thesis by assumption
10.50 +next case (Some ia) note tsome = this
10.51 + from this have o1: "tlookup fst i t = Some (fst ia, snd ia)" by simp
10.52 + have "mapOf t i = Some (snd ia)"
10.53 + by (insert mapOf_lookup2 [of i t "fst ia" "snd ia"], simp add: o1)
10.54 + from this have "mapOf t i ~= None" by simp
10.55 + from this h show ?thesis by simp -- {* contradiction *}
10.56 +qed
10.57 +
10.58 +lemma assumes v: "valid_tmap t"
10.59 + assumes h: "mapOf t i = Some a"
10.60 + shows mapOf_lookup4: "tlookup fst i t = Some (i,a)"
10.61 +proof (cases "tlookup fst i t")
10.62 +case None
10.63 + from this mapOf_lookup1 have "mapOf t i = None" by auto
10.64 + from this h show ?thesis by simp -- {* contradiction *}
10.65 +next case (Some ia) note tsome = this
10.66 + have tlookup_some_inst: "sortedTree fst t & (tlookup fst i t = Some ia) -->
10.67 + ia : setOf t & fst ia = i" by (simp add: tlookup_some)
10.68 + from tlookup_some_inst tsome v have "ia : setOf t" by simp
10.69 + from tsome have "mapOf t i = Some (snd ia)" by (simp add: mapOf_def)
10.70 + from this h have o1: "snd ia = a" by simp
10.71 + from tlookup_some_inst tsome v have o2: "fst ia = i" by simp
10.72 + from o1 o2 have "ia = (i,a)" by auto
10.73 + from this tsome show "tlookup fst i t = Some (i, a)" by simp
10.74 +qed
10.75 +
10.76 +subsection {* Lemmas @{text mapset_none} and @{text mapset_some} establish
10.77 + a relation between the set and map abstraction of the tree *}
10.78 +
10.79 +lemma assumes v: "valid_tmap t"
10.80 + shows mapset_none: "(mapOf t i = None) = (ALL a. (i,a) ~: setOf t)"
10.81 +proof
10.82 + -- {* ==> *}
10.83 + assume mapNone: "mapOf t i = None"
10.84 + from v mapNone mapOf_lookup3 have lnone: "tlookup fst i t = None" by auto
10.85 + show "ALL a. (i,a) ~: setOf t"
10.86 + proof
10.87 + fix a
10.88 + show "(i,a) ~: setOf t"
10.89 + proof
10.90 + assume iain: "(i,a) : setOf t"
10.91 + have tlookup_none_inst:
10.92 + "sortedTree fst t & (tlookup fst i t = None) --> (ALL x:setOf t. fst x ~= i)"
10.93 + by (insert tlookup_none [of "fst" "t" "i"], assumption)
10.94 + from v lnone tlookup_none_inst have "ALL x : setOf t. fst x ~= i" by simp
10.95 + from this iain have "fst (i,a) ~= i" by fastsimp
10.96 + from this show False by simp
10.97 + qed
10.98 + qed
10.99 + -- {* <== *}
10.100 + next assume h: "ALL a. (i,a) ~: setOf t"
10.101 + show "mapOf t i = None"
10.102 + proof (cases "mapOf t i")
10.103 + case None show ?thesis by assumption
10.104 + next case (Some a) note mapsome = this
10.105 + from v mapsome have o1: "tlookup fst i t = Some (i,a)" by (simp add: mapOf_lookup4)
10.106 + (* moving mapOf_lookup4 to assumption does not work, although it uses
10.107 + no == !! *)
10.108 + from tlookup_some have tlookup_some_inst:
10.109 + "sortedTree fst t & tlookup fst i t = Some (i,a) -->
10.110 + (i,a) : setOf t & fst (i,a) = i"
10.111 + by (insert tlookup_some [of fst t i "(i,a)"], assumption)
10.112 + from v o1 this have "(i,a) : setOf t" by simp
10.113 + from this h show ?thesis by auto -- {* contradiction *}
10.114 + qed
10.115 +qed
10.116 +
10.117 +lemma assumes v: "valid_tmap t"
10.118 + shows mapset_some: "(mapOf t i = Some a) = ((i,a) : setOf t)"
10.119 +proof
10.120 + -- {* ==> *}
10.121 + assume mapsome: "mapOf t i = Some a"
10.122 + from v mapsome have o1: "tlookup fst i t = Some (i,a)" by (simp add: mapOf_lookup4)
10.123 + from tlookup_some have tlookup_some_inst:
10.124 + "sortedTree fst t & tlookup fst i t = Some (i,a) -->
10.125 + (i,a) : setOf t & fst (i,a) = i"
10.126 + by (insert tlookup_some [of fst t i "(i,a)"], assumption)
10.127 + from v o1 this show "(i,a) : setOf t" by simp
10.128 + -- {* <== *}
10.129 + next assume iain: "(i,a) : setOf t"
10.130 + from v iain tlookup_finds have "tlookup fst (fst (i,a)) t = Some (i,a)" by fastsimp
10.131 + from this have "tlookup fst i t = Some (i,a)" by simp
10.132 + from this show "mapOf t i = Some a" by (simp add: mapOf_def)
10.133 +qed
10.134 +
10.135 +(*============================================================*)
10.136 +section {* Empty Map *}
10.137 +(*============================================================*)
10.138 +
10.139 +lemma mnew_spec_valid: "valid_tmap Tip"
10.140 +by (simp add: mapOf_def)
10.141 +
10.142 +lemma mtip_spec_empty: "mapOf Tip k = None"
10.143 +by (simp add: mapOf_def)
10.144 +
10.145 +
10.146 +(*============================================================*)
10.147 +section {* Map Update Operation *}
10.148 +(*============================================================*)
10.149 +
10.150 +constdefs
10.151 + mupdate :: "index => 'a => 'a tarray => 'a tarray"
10.152 + "mupdate i a t == binsert fst (i,a) t"
10.153 +
10.154 +lemma assumes v: "valid_tmap t"
10.155 + shows mupdate_map: "mapOf (mupdate i a t) = (mapOf t)(i |-> a)"
10.156 +proof
10.157 + fix i2
10.158 + let ?tr = "binsert fst (i,a) t"
10.159 + have upres: "mupdate i a t = ?tr" by (simp add: mupdate_def)
10.160 + from v binsert_set
10.161 + have setSpec: "setOf ?tr = setOf t - eqs fst (i,a) Un {(i,a)}" by fastsimp
10.162 + from v binsert_sorted have vr: "valid_tmap ?tr" by fastsimp
10.163 + show "mapOf (mupdate i a t) i2 = ((mapOf t)(i |-> a)) i2"
10.164 + proof (cases "i = i2")
10.165 + case True note i2ei = this
10.166 + from i2ei have rhs_res: "((mapOf t)(i |-> a)) i2 = Some a" by simp
10.167 + have lhs_res: "mapOf (mupdate i a t) i = Some a"
10.168 + proof -
10.169 + have will_find: "tlookup fst i ?tr = Some (i,a)"
10.170 + proof -
10.171 + from setSpec have kvin: "(i,a) : setOf ?tr" by simp
10.172 + have binsert_sorted_inst: "sortedTree fst t -->
10.173 + sortedTree fst ?tr"
10.174 + by (insert binsert_sorted [of "fst" "t" "(i,a)"], assumption)
10.175 + from v binsert_sorted_inst have rs: "sortedTree fst ?tr" by simp
10.176 + have tlookup_finds_inst: "sortedTree fst ?tr & (i,a) : setOf ?tr -->
10.177 + tlookup fst i ?tr = Some (i,a)"
10.178 + by (insert tlookup_finds [of "fst" "?tr" "(i,a)"], simp)
10.179 + from rs kvin tlookup_finds_inst show ?thesis by simp
10.180 + qed
10.181 + from upres will_find show ?thesis by (simp add: mapOf_def)
10.182 + qed
10.183 + from lhs_res rhs_res i2ei show ?thesis by simp
10.184 + next case False note i2nei = this
10.185 + from i2nei have rhs_res: "((mapOf t)(i |-> a)) i2 = mapOf t i2" by auto
10.186 + have lhs_res: "mapOf (mupdate i a t) i2 = mapOf t i2"
10.187 + proof (cases "mapOf t i2")
10.188 + case None from this have mapNone: "mapOf t i2 = None" by simp
10.189 + from v mapNone mapset_none have i2nin: "ALL a. (i2,a) ~: setOf t" by fastsimp
10.190 + have noneIn: "ALL b. (i2,b) ~: setOf ?tr"
10.191 + proof
10.192 + fix b
10.193 + from v binsert_set
10.194 + have "setOf ?tr = setOf t - eqs fst (i,a) Un {(i,a)}"
10.195 + by fastsimp
10.196 + from this i2nei i2nin show "(i2,b) ~: setOf ?tr" by fastsimp
10.197 + qed
10.198 + have mapset_none_inst:
10.199 + "valid_tmap ?tr --> (mapOf ?tr i2 = None) = (ALL a. (i2, a) ~: setOf ?tr)"
10.200 + by (insert mapset_none [of "?tr" i2], simp)
10.201 + from vr noneIn mapset_none_inst have "mapOf ?tr i2 = None" by fastsimp
10.202 + from this upres mapNone show ?thesis by simp
10.203 + next case (Some z) from this have mapSome: "mapOf t i2 = Some z" by simp
10.204 + from v mapSome mapset_some have "(i2,z) : setOf t" by fastsimp
10.205 + from this setSpec i2nei have "(i2,z) : setOf ?tr" by (simp add: eqs_def)
10.206 + from this vr mapset_some have "mapOf ?tr i2 = Some z" by fastsimp
10.207 + from this upres mapSome show ?thesis by simp
10.208 + qed
10.209 + from lhs_res rhs_res show ?thesis by simp
10.210 + qed
10.211 +qed
10.212 +
10.213 +lemma assumes v: "valid_tmap t"
10.214 + shows mupdate_valid: "valid_tmap (mupdate i a t)"
10.215 +proof -
10.216 + let ?tr = "binsert fst (i,a) t"
10.217 + have upres: "mupdate i a t = ?tr" by (simp add: mupdate_def)
10.218 + from v binsert_sorted have vr: "valid_tmap ?tr" by fastsimp
10.219 + from vr upres show ?thesis by simp
10.220 +qed
10.221 +
10.222 +(*============================================================*)
10.223 +section {* Map Remove Operation *}
10.224 +(*============================================================*)
10.225 +
10.226 +constdefs
10.227 + mremove :: "index => 'a tarray => 'a tarray"
10.228 + "mremove i t == remove fst (i, arbitrary) t"
10.229 +
10.230 +lemma assumes v: "valid_tmap t"
10.231 + shows mremove_valid: "valid_tmap (mremove i t)"
10.232 +proof (simp add: mremove_def)
10.233 + from v remove_sort
10.234 + show "sortedTree fst (remove fst (i,arbitrary) t)" by fastsimp
10.235 +qed
10.236 +
10.237 +lemma assumes v: "valid_tmap t"
10.238 + shows mremove_map: "mapOf (mremove i t) i = None"
10.239 +proof (simp add: mremove_def)
10.240 + let ?tr = "remove fst (i,arbitrary) t"
10.241 + show "mapOf ?tr i = None"
10.242 + proof -
10.243 + from v remove_spec
10.244 + have remSet: "setOf ?tr = setOf t - eqs fst (i,arbitrary)"
10.245 + by fastsimp
10.246 + have noneIn: "ALL a. (i,a) ~: setOf ?tr"
10.247 + proof
10.248 + fix a
10.249 + from remSet show "(i,a) ~: setOf ?tr" by (simp add: eqs_def)
10.250 + qed
10.251 + from v remove_sort have vr: "valid_tmap ?tr" by fastsimp
10.252 + have mapset_none_inst: "valid_tmap ?tr ==>
10.253 + (mapOf ?tr i = None) = (ALL a. (i,a) ~: setOf ?tr)"
10.254 + by (insert mapset_none [of "?tr" "i"], simp)
10.255 + from vr this have "(mapOf ?tr i = None) = (ALL a. (i,a) ~: setOf ?tr)" by fastsimp
10.256 + from this noneIn show "mapOf ?tr i = None" by simp
10.257 + qed
10.258 +qed
10.259 +
10.260 +end
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/Induct/BinaryTree_TacticStyle.thy Wed Dec 10 15:59:34 2003 +0100
11.3 @@ -0,0 +1,141 @@
11.4 +header {* Tactic-Style Reasoning for Binary Tree Operations *}
11.5 +theory BinaryTree_TacticStyle = Main:
11.6 +
11.7 +text {* This example theory illustrates automated proofs of correctness
11.8 + for binary tree operations using tactic-style reasoning.
11.9 + The current proofs for remove operation are by Tobias Nipkow,
11.10 + some modifications and the remaining tree operations are
11.11 + by Viktor Kuncak. *}
11.12 +
11.13 +(*============================================================*)
11.14 +section {* Definition of a sorted binary tree *}
11.15 +(*============================================================*)
11.16 +
11.17 +datatype tree = Tip | Nd tree nat tree
11.18 +
11.19 +consts set_of :: "tree => nat set"
11.20 +-- {* The set of nodes stored in a tree. *}
11.21 +primrec
11.22 +"set_of Tip = {}"
11.23 +"set_of(Nd l x r) = set_of l Un set_of r Un {x}"
11.24 +
11.25 +consts sorted :: "tree => bool"
11.26 +-- {* Tree is sorted *}
11.27 +primrec
11.28 +"sorted Tip = True"
11.29 +"sorted(Nd l y r) =
11.30 + (sorted l & sorted r & (ALL x:set_of l. x < y) & (ALL z:set_of r. y < z))"
11.31 +
11.32 +(*============================================================*)
11.33 +section {* Tree Membership *}
11.34 +(*============================================================*)
11.35 +
11.36 +consts
11.37 + memb :: "nat => tree => bool"
11.38 +primrec
11.39 +"memb e Tip = False"
11.40 +"memb e (Nd t1 x t2) =
11.41 + (if e < x then memb e t1
11.42 + else if x < e then memb e t2
11.43 + else True)"
11.44 +
11.45 +lemma member_set: "sorted t --> memb e t = (e : set_of t)"
11.46 +by (induct t, auto)
11.47 +
11.48 +(*============================================================*)
11.49 +section {* Insertion operation *}
11.50 +(*============================================================*)
11.51 +
11.52 +consts binsert :: "nat => tree => tree"
11.53 +-- {* Insert a node into sorted tree. *}
11.54 +primrec
11.55 +"binsert x Tip = (Nd Tip x Tip)"
11.56 +"binsert x (Nd t1 y t2) = (if x < y then
11.57 + (Nd (binsert x t1) y t2)
11.58 + else
11.59 + (if y < x then
11.60 + (Nd t1 y (binsert x t2))
11.61 + else (Nd t1 y t2)))"
11.62 +
11.63 +theorem set_of_binsert [simp]: "set_of (binsert x t) = set_of t Un {x}"
11.64 +by (induct_tac t, auto)
11.65 +
11.66 +theorem binsert_sorted: "sorted t --> sorted (binsert x t)"
11.67 +by (induct_tac t, auto simp add: set_of_binsert)
11.68 +
11.69 +corollary binsert_spec: (* summary specification of binsert *)
11.70 +"sorted t ==>
11.71 + sorted (binsert x t) &
11.72 + set_of (binsert x t) = set_of t Un {x}"
11.73 +by (simp add: binsert_sorted)
11.74 +
11.75 +(*============================================================*)
11.76 +section {* Remove operation *}
11.77 +(*============================================================*)
11.78 +
11.79 +consts
11.80 + remove:: "nat => tree => tree" -- {* remove a node from sorted tree *}
11.81 + -- {* auxiliary operations: *}
11.82 + rm :: "tree => nat" -- {* find the rightmost element in the tree *}
11.83 + rem :: "tree => tree" -- {* find the tree without the rightmost element *}
11.84 +primrec
11.85 +"rm(Nd l x r) = (if r = Tip then x else rm r)"
11.86 +primrec
11.87 +"rem(Nd l x r) = (if r=Tip then l else Nd l x (rem r))"
11.88 +primrec
11.89 +"remove x Tip = Tip"
11.90 +"remove x (Nd l y r) =
11.91 + (if x < y then Nd (remove x l) y r else
11.92 + if y < x then Nd l y (remove x r) else
11.93 + if l = Tip then r
11.94 + else Nd (rem l) (rm l) r)"
11.95 +
11.96 +lemma rm_in_set_of: "t ~= Tip ==> rm t : set_of t"
11.97 +by (induct t) auto
11.98 +
11.99 +lemma set_of_rem: "t ~= Tip ==> set_of t = set_of(rem t) Un {rm t}"
11.100 +by (induct t) auto
11.101 +
11.102 +lemma [simp]: "[| t ~= Tip; sorted t |] ==> sorted(rem t)"
11.103 +by (induct t) (auto simp add:set_of_rem)
11.104 +
11.105 +lemma sorted_rem: "[| t ~= Tip; x \<in> set_of(rem t); sorted t |] ==> x < rm t"
11.106 +by (induct t) (auto simp add:set_of_rem split:if_splits)
11.107 +
11.108 +theorem set_of_remove [simp]: "sorted t ==> set_of(remove x t) = set_of t - {x}"
11.109 +apply(induct t)
11.110 + apply simp
11.111 +apply simp
11.112 +apply(rule conjI)
11.113 + apply fastsimp
11.114 +apply(rule impI)
11.115 +apply(rule conjI)
11.116 + apply fastsimp
11.117 +apply(fastsimp simp:set_of_rem)
11.118 +done
11.119 +
11.120 +theorem remove_sorted: "sorted t ==> sorted(remove x t)"
11.121 +by (induct t) (auto intro: less_trans rm_in_set_of sorted_rem)
11.122 +
11.123 +corollary remove_spec: -- {* summary specification of remove *}
11.124 +"sorted t ==>
11.125 + sorted (remove x t) &
11.126 + set_of (remove x t) = set_of t - {x}"
11.127 +by (simp add: remove_sorted)
11.128 +
11.129 +text {* Finally, note that rem and rm can be computed
11.130 + using a single tree traversal given by remrm. *}
11.131 +
11.132 +consts remrm :: "tree => tree * nat"
11.133 +primrec
11.134 +"remrm(Nd l x r) = (if r=Tip then (l,x) else
11.135 + let (r',y) = remrm r in (Nd l x r',y))"
11.136 +
11.137 +lemma "t ~= Tip ==> remrm t = (rem t, rm t)"
11.138 +by (induct t) (auto simp:Let_def)
11.139 +
11.140 +text {* We can test this implementation by generating code. *}
11.141 +generate_code ("BinaryTree_TacticStyle_Code.ML")
11.142 + test = "memb 4 (remove (3::nat) (binsert 4 (binsert 3 Tip)))"
11.143 +
11.144 +end
12.1 --- a/src/HOL/Induct/ROOT.ML Wed Dec 10 14:29:44 2003 +0100
12.2 +++ b/src/HOL/Induct/ROOT.ML Wed Dec 10 15:59:34 2003 +0100
12.3 @@ -9,3 +9,6 @@
12.4 time_use_thy "PropLog";
12.5 time_use_thy "SList";
12.6 time_use_thy "LFilter";
12.7 +
12.8 +time_use_thy "BinaryTree_Map";
12.9 +time_use_thy "BinaryTree_TacticStyle";
13.1 --- a/src/HOL/Integ/Bin.thy Wed Dec 10 14:29:44 2003 +0100
13.2 +++ b/src/HOL/Integ/Bin.thy Wed Dec 10 15:59:34 2003 +0100
13.3 @@ -226,55 +226,9 @@
13.4 lemma int_numeral_1_eq_1: "Numeral1 = (1::int)"
13.5 by (simp add: int_1 int_Suc0_eq_1)
13.6
13.7 -
13.8 -subsubsection{*Special Simplification for Constants*}
13.9 -
13.10 -text{*These distributive laws move literals inside sums and differences.*}
13.11 -declare left_distrib [of _ _ "number_of v", standard, simp]
13.12 -declare right_distrib [of "number_of v", standard, simp]
13.13 -
13.14 -declare left_diff_distrib [of _ _ "number_of v", standard, simp]
13.15 -declare right_diff_distrib [of "number_of v", standard, simp]
13.16 -
13.17 -text{*These are actually for fields, like real: but where else to put them?*}
13.18 -declare zero_less_divide_iff [of "number_of w", standard, simp]
13.19 -declare divide_less_0_iff [of "number_of w", standard, simp]
13.20 -declare zero_le_divide_iff [of "number_of w", standard, simp]
13.21 -declare divide_le_0_iff [of "number_of w", standard, simp]
13.22 -
13.23 -(*Replaces "inverse #nn" by 1/#nn *)
13.24 -declare inverse_eq_divide [of "number_of w", standard, simp]
13.25 -
13.26 -text{*These laws simplify inequalities, moving unary minus from a term
13.27 -into the literal.*}
13.28 -declare less_minus_iff [of "number_of v", standard, simp]
13.29 -declare le_minus_iff [of "number_of v", standard, simp]
13.30 -declare equation_minus_iff [of "number_of v", standard, simp]
13.31 -
13.32 -declare minus_less_iff [of _ "number_of v", standard, simp]
13.33 -declare minus_le_iff [of _ "number_of v", standard, simp]
13.34 -declare minus_equation_iff [of _ "number_of v", standard, simp]
13.35 -
13.36 -text{*These simplify inequalities where one side is the constant 1.*}
13.37 -declare less_minus_iff [of 1, simplified, simp]
13.38 -declare le_minus_iff [of 1, simplified, simp]
13.39 -declare equation_zminus [of 1, simplified, simp]
13.40 -
13.41 -declare minus_less_iff [of _ 1, simplified, simp]
13.42 -declare minus_le_iff [of _ 1, simplified, simp]
13.43 -declare minus_equation_iff [of _ 1, simplified, simp]
13.44 -
13.45 -
13.46 -(*Moving negation out of products*)
13.47 +(*Moving negation out of products: so far for type "int" only*)
13.48 declare zmult_zminus [simp] zmult_zminus_right [simp]
13.49
13.50 -(*Cancellation of constant factors in comparisons (< and \<le>) *)
13.51 -
13.52 -declare mult_less_cancel_left [of "number_of v", standard, simp]
13.53 -declare mult_less_cancel_right [of _ "number_of v", standard, simp]
13.54 -declare mult_le_cancel_left [of "number_of v", standard, simp]
13.55 -declare mult_le_cancel_right [of _ "number_of v", standard, simp]
13.56 -
13.57
13.58 (** Special-case simplification for small constants **)
13.59
14.1 --- a/src/HOL/Integ/IntDiv.thy Wed Dec 10 14:29:44 2003 +0100
14.2 +++ b/src/HOL/Integ/IntDiv.thy Wed Dec 10 15:59:34 2003 +0100
14.3 @@ -10,18 +10,18 @@
14.4 fun posDivAlg (a,b) =
14.5 if a<b then (0,a)
14.6 else let val (q,r) = posDivAlg(a, 2*b)
14.7 - in if 0<=r-b then (2*q+1, r-b) else (2*q, r)
14.8 + in if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
14.9 end
14.10
14.11 fun negDivAlg (a,b) =
14.12 - if 0<=a+b then (~1,a+b)
14.13 + if 0\<le>a+b then (~1,a+b)
14.14 else let val (q,r) = negDivAlg(a, 2*b)
14.15 - in if 0<=r-b then (2*q+1, r-b) else (2*q, r)
14.16 + in if 0\<le>r-b then (2*q+1, r-b) else (2*q, r)
14.17 end;
14.18
14.19 fun negateSnd (q,r:int) = (q,~r);
14.20
14.21 - fun divAlg (a,b) = if 0<=a then
14.22 + fun divAlg (a,b) = if 0\<le>a then
14.23 if b>0 then posDivAlg (a,b)
14.24 else if a=0 then (0,0)
14.25 else negateSnd (negDivAlg (~a,~b))
14.26 @@ -40,10 +40,10 @@
14.27 quorem :: "(int*int) * (int*int) => bool"
14.28 "quorem == %((a,b), (q,r)).
14.29 a = b*q + r &
14.30 - (if 0 < b then 0<=r & r<b else b<r & r <= 0)"
14.31 + (if 0 < b then 0\<le>r & r<b else b<r & r \<le> 0)"
14.32
14.33 adjust :: "[int, int*int] => int*int"
14.34 - "adjust b == %(q,r). if 0 <= r-b then (2*q + 1, r-b)
14.35 + "adjust b == %(q,r). if 0 \<le> r-b then (2*q + 1, r-b)
14.36 else (2*q, r)"
14.37
14.38 (** the division algorithm **)
14.39 @@ -52,14 +52,14 @@
14.40 consts posDivAlg :: "int*int => int*int"
14.41 recdef posDivAlg "inv_image less_than (%(a,b). nat(a - b + 1))"
14.42 "posDivAlg (a,b) =
14.43 - (if (a<b | b<=0) then (0,a)
14.44 + (if (a<b | b\<le>0) then (0,a)
14.45 else adjust b (posDivAlg(a, 2*b)))"
14.46
14.47 (*for the case a<0, b>0*)
14.48 consts negDivAlg :: "int*int => int*int"
14.49 recdef negDivAlg "inv_image less_than (%(a,b). nat(- a - b))"
14.50 "negDivAlg (a,b) =
14.51 - (if (0<=a+b | b<=0) then (-1,a+b)
14.52 + (if (0\<le>a+b | b\<le>0) then (-1,a+b)
14.53 else adjust b (negDivAlg(a, 2*b)))"
14.54
14.55 (*for the general case b~=0*)
14.56 @@ -72,8 +72,8 @@
14.57 including the special case a=0, b<0, because negDivAlg requires a<0*)
14.58 divAlg :: "int*int => int*int"
14.59 "divAlg ==
14.60 - %(a,b). if 0<=a then
14.61 - if 0<=b then posDivAlg (a,b)
14.62 + %(a,b). if 0\<le>a then
14.63 + if 0\<le>b then posDivAlg (a,b)
14.64 else if a=0 then (0,0)
14.65 else negateSnd (negDivAlg (-a,-b))
14.66 else
14.67 @@ -92,9 +92,9 @@
14.68 subsection{*Uniqueness and Monotonicity of Quotients and Remainders*}
14.69
14.70 lemma unique_quotient_lemma:
14.71 - "[| b*q' + r' <= b*q + r; 0 <= r'; 0 < b; r < b |]
14.72 - ==> q' <= (q::int)"
14.73 -apply (subgoal_tac "r' + b * (q'-q) <= r")
14.74 + "[| b*q' + r' \<le> b*q + r; 0 \<le> r'; 0 < b; r < b |]
14.75 + ==> q' \<le> (q::int)"
14.76 +apply (subgoal_tac "r' + b * (q'-q) \<le> r")
14.77 prefer 2 apply (simp add: zdiff_zmult_distrib2)
14.78 apply (subgoal_tac "0 < b * (1 + q - q') ")
14.79 apply (erule_tac [2] order_le_less_trans)
14.80 @@ -105,8 +105,8 @@
14.81 done
14.82
14.83 lemma unique_quotient_lemma_neg:
14.84 - "[| b*q' + r' <= b*q + r; r <= 0; b < 0; b < r' |]
14.85 - ==> q <= (q'::int)"
14.86 + "[| b*q' + r' \<le> b*q + r; r \<le> 0; b < 0; b < r' |]
14.87 + ==> q \<le> (q'::int)"
14.88 by (rule_tac b = "-b" and r = "-r'" and r' = "-r" in unique_quotient_lemma,
14.89 auto)
14.90
14.91 @@ -136,7 +136,7 @@
14.92 lemma adjust_eq [simp]:
14.93 "adjust b (q,r) =
14.94 (let diff = r-b in
14.95 - if 0 <= diff then (2*q + 1, diff)
14.96 + if 0 \<le> diff then (2*q + 1, diff)
14.97 else (2*q, r))"
14.98 by (simp add: Let_def adjust_def)
14.99
14.100 @@ -150,7 +150,7 @@
14.101
14.102 (*Correctness of posDivAlg: it computes quotients correctly*)
14.103 lemma posDivAlg_correct [rule_format]:
14.104 - "0 <= a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))"
14.105 + "0 \<le> a --> 0 < b --> quorem ((a, b), posDivAlg (a, b))"
14.106 apply (induct_tac a b rule: posDivAlg.induct, auto)
14.107 apply (simp_all add: quorem_def)
14.108 (*base case: a<b*)
14.109 @@ -172,7 +172,7 @@
14.110 lemma negDivAlg_eqn:
14.111 "0 < b ==>
14.112 negDivAlg (a,b) =
14.113 - (if 0<=a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))"
14.114 + (if 0\<le>a+b then (-1,a+b) else adjust b (negDivAlg(a, 2*b)))"
14.115 by (rule negDivAlg.simps [THEN trans], simp)
14.116
14.117 (*Correctness of negDivAlg: it computes quotients correctly
14.118 @@ -181,7 +181,7 @@
14.119 "a < 0 --> 0 < b --> quorem ((a, b), negDivAlg (a, b))"
14.120 apply (induct_tac a b rule: negDivAlg.induct, auto)
14.121 apply (simp_all add: quorem_def)
14.122 - (*base case: 0<=a+b*)
14.123 + (*base case: 0\<le>a+b*)
14.124 apply (simp add: negDivAlg_eqn)
14.125 (*main argument*)
14.126 apply (subst negDivAlg_eqn, assumption)
14.127 @@ -234,7 +234,7 @@
14.128
14.129 use "IntDiv_setup.ML"
14.130
14.131 -lemma pos_mod_conj : "(0::int) < b ==> 0 <= a mod b & a mod b < b"
14.132 +lemma pos_mod_conj : "(0::int) < b ==> 0 \<le> a mod b & a mod b < b"
14.133 apply (cut_tac a = a and b = b in divAlg_correct)
14.134 apply (auto simp add: quorem_def mod_def)
14.135 done
14.136 @@ -242,7 +242,7 @@
14.137 lemmas pos_mod_sign[simp] = pos_mod_conj [THEN conjunct1, standard]
14.138 and pos_mod_bound[simp] = pos_mod_conj [THEN conjunct2, standard]
14.139
14.140 -lemma neg_mod_conj : "b < (0::int) ==> a mod b <= 0 & b < a mod b"
14.141 +lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
14.142 apply (cut_tac a = a and b = b in divAlg_correct)
14.143 apply (auto simp add: quorem_def div_def mod_def)
14.144 done
14.145 @@ -265,34 +265,34 @@
14.146 lemma quorem_mod: "[| quorem((a,b),(q,r)); b ~= 0 |] ==> a mod b = r"
14.147 by (simp add: quorem_div_mod [THEN unique_remainder])
14.148
14.149 -lemma div_pos_pos_trivial: "[| (0::int) <= a; a < b |] ==> a div b = 0"
14.150 +lemma div_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a div b = 0"
14.151 apply (rule quorem_div)
14.152 apply (auto simp add: quorem_def)
14.153 done
14.154
14.155 -lemma div_neg_neg_trivial: "[| a <= (0::int); b < a |] ==> a div b = 0"
14.156 +lemma div_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a div b = 0"
14.157 apply (rule quorem_div)
14.158 apply (auto simp add: quorem_def)
14.159 done
14.160
14.161 -lemma div_pos_neg_trivial: "[| (0::int) < a; a+b <= 0 |] ==> a div b = -1"
14.162 +lemma div_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a div b = -1"
14.163 apply (rule quorem_div)
14.164 apply (auto simp add: quorem_def)
14.165 done
14.166
14.167 (*There is no div_neg_pos_trivial because 0 div b = 0 would supersede it*)
14.168
14.169 -lemma mod_pos_pos_trivial: "[| (0::int) <= a; a < b |] ==> a mod b = a"
14.170 +lemma mod_pos_pos_trivial: "[| (0::int) \<le> a; a < b |] ==> a mod b = a"
14.171 apply (rule_tac q = 0 in quorem_mod)
14.172 apply (auto simp add: quorem_def)
14.173 done
14.174
14.175 -lemma mod_neg_neg_trivial: "[| a <= (0::int); b < a |] ==> a mod b = a"
14.176 +lemma mod_neg_neg_trivial: "[| a \<le> (0::int); b < a |] ==> a mod b = a"
14.177 apply (rule_tac q = 0 in quorem_mod)
14.178 apply (auto simp add: quorem_def)
14.179 done
14.180
14.181 -lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b <= 0 |] ==> a mod b = a+b"
14.182 +lemma mod_pos_neg_trivial: "[| (0::int) < a; a+b \<le> 0 |] ==> a mod b = a+b"
14.183 apply (rule_tac q = "-1" in quorem_mod)
14.184 apply (auto simp add: quorem_def)
14.185 done
14.186 @@ -355,13 +355,13 @@
14.187
14.188 subsection{*Division of a Number by Itself*}
14.189
14.190 -lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 <= q"
14.191 +lemma self_quotient_aux1: "[| (0::int) < a; a = r + a*q; r < a |] ==> 1 \<le> q"
14.192 apply (subgoal_tac "0 < a*q")
14.193 apply (simp add: int_0_less_mult_iff, arith)
14.194 done
14.195
14.196 -lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 <= r |] ==> q <= 1"
14.197 -apply (subgoal_tac "0 <= a* (1-q) ")
14.198 +lemma self_quotient_aux2: "[| (0::int) < a; a = r + a*q; 0 \<le> r |] ==> q \<le> 1"
14.199 +apply (subgoal_tac "0 \<le> a* (1-q) ")
14.200 apply (simp add: int_0_le_mult_iff)
14.201 apply (simp add: zdiff_zmult_distrib2)
14.202 done
14.203 @@ -408,10 +408,10 @@
14.204
14.205 (** a positive, b positive **)
14.206
14.207 -lemma div_pos_pos: "[| 0 < a; 0 <= b |] ==> a div b = fst (posDivAlg(a,b))"
14.208 +lemma div_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a div b = fst (posDivAlg(a,b))"
14.209 by (simp add: div_def divAlg_def)
14.210
14.211 -lemma mod_pos_pos: "[| 0 < a; 0 <= b |] ==> a mod b = snd (posDivAlg(a,b))"
14.212 +lemma mod_pos_pos: "[| 0 < a; 0 \<le> b |] ==> a mod b = snd (posDivAlg(a,b))"
14.213 by (simp add: mod_def divAlg_def)
14.214
14.215 (** a negative, b positive **)
14.216 @@ -435,11 +435,11 @@
14.217 (** a negative, b negative **)
14.218
14.219 lemma div_neg_neg:
14.220 - "[| a < 0; b <= 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"
14.221 + "[| a < 0; b \<le> 0 |] ==> a div b = fst (negateSnd(posDivAlg(-a,-b)))"
14.222 by (simp add: div_def divAlg_def)
14.223
14.224 lemma mod_neg_neg:
14.225 - "[| a < 0; b <= 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"
14.226 + "[| a < 0; b \<le> 0 |] ==> a mod b = snd (negateSnd(posDivAlg(-a,-b)))"
14.227 by (simp add: mod_def divAlg_def)
14.228
14.229 text {*Simplify expresions in which div and mod combine numerical constants*}
14.230 @@ -492,7 +492,7 @@
14.231
14.232 subsection{*Monotonicity in the First Argument (Dividend)*}
14.233
14.234 -lemma zdiv_mono1: "[| a <= a'; 0 < (b::int) |] ==> a div b <= a' div b"
14.235 +lemma zdiv_mono1: "[| a \<le> a'; 0 < (b::int) |] ==> a div b \<le> a' div b"
14.236 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
14.237 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
14.238 apply (rule unique_quotient_lemma)
14.239 @@ -501,7 +501,7 @@
14.240 apply (simp_all)
14.241 done
14.242
14.243 -lemma zdiv_mono1_neg: "[| a <= a'; (b::int) < 0 |] ==> a' div b <= a div b"
14.244 +lemma zdiv_mono1_neg: "[| a \<le> a'; (b::int) < 0 |] ==> a' div b \<le> a div b"
14.245 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
14.246 apply (cut_tac a = a' and b = b in zmod_zdiv_equality)
14.247 apply (rule unique_quotient_lemma_neg)
14.248 @@ -514,16 +514,16 @@
14.249 subsection{*Monotonicity in the Second Argument (Divisor)*}
14.250
14.251 lemma q_pos_lemma:
14.252 - "[| 0 <= b'*q' + r'; r' < b'; 0 < b' |] ==> 0 <= (q'::int)"
14.253 + "[| 0 \<le> b'*q' + r'; r' < b'; 0 < b' |] ==> 0 \<le> (q'::int)"
14.254 apply (subgoal_tac "0 < b'* (q' + 1) ")
14.255 apply (simp add: int_0_less_mult_iff)
14.256 apply (simp add: zadd_zmult_distrib2)
14.257 done
14.258
14.259 lemma zdiv_mono2_lemma:
14.260 - "[| b*q + r = b'*q' + r'; 0 <= b'*q' + r';
14.261 - r' < b'; 0 <= r; 0 < b'; b' <= b |]
14.262 - ==> q <= (q'::int)"
14.263 + "[| b*q + r = b'*q' + r'; 0 \<le> b'*q' + r';
14.264 + r' < b'; 0 \<le> r; 0 < b'; b' \<le> b |]
14.265 + ==> q \<le> (q'::int)"
14.266 apply (frule q_pos_lemma, assumption+)
14.267 apply (subgoal_tac "b*q < b* (q' + 1) ")
14.268 apply (simp add: zmult_zless_cancel1)
14.269 @@ -535,7 +535,7 @@
14.270 done
14.271
14.272 lemma zdiv_mono2:
14.273 - "[| (0::int) <= a; 0 < b'; b' <= b |] ==> a div b <= a div b'"
14.274 + "[| (0::int) \<le> a; 0 < b'; b' \<le> b |] ==> a div b \<le> a div b'"
14.275 apply (subgoal_tac "b ~= 0")
14.276 prefer 2 apply arith
14.277 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
14.278 @@ -547,20 +547,20 @@
14.279 done
14.280
14.281 lemma q_neg_lemma:
14.282 - "[| b'*q' + r' < 0; 0 <= r'; 0 < b' |] ==> q' <= (0::int)"
14.283 + "[| b'*q' + r' < 0; 0 \<le> r'; 0 < b' |] ==> q' \<le> (0::int)"
14.284 apply (subgoal_tac "b'*q' < 0")
14.285 apply (simp add: zmult_less_0_iff, arith)
14.286 done
14.287
14.288 lemma zdiv_mono2_neg_lemma:
14.289 "[| b*q + r = b'*q' + r'; b'*q' + r' < 0;
14.290 - r < b; 0 <= r'; 0 < b'; b' <= b |]
14.291 - ==> q' <= (q::int)"
14.292 + r < b; 0 \<le> r'; 0 < b'; b' \<le> b |]
14.293 + ==> q' \<le> (q::int)"
14.294 apply (frule q_neg_lemma, assumption+)
14.295 apply (subgoal_tac "b*q' < b* (q + 1) ")
14.296 apply (simp add: zmult_zless_cancel1)
14.297 apply (simp add: zadd_zmult_distrib2)
14.298 -apply (subgoal_tac "b*q' <= b'*q'")
14.299 +apply (subgoal_tac "b*q' \<le> b'*q'")
14.300 prefer 2 apply (simp add: zmult_zle_mono1_neg)
14.301 apply (subgoal_tac "b'*q' < b + b*q")
14.302 apply arith
14.303 @@ -568,7 +568,7 @@
14.304 done
14.305
14.306 lemma zdiv_mono2_neg:
14.307 - "[| a < (0::int); 0 < b'; b' <= b |] ==> a div b' <= a div b"
14.308 + "[| a < (0::int); 0 < b'; b' \<le> b |] ==> a div b' \<le> a div b"
14.309 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
14.310 apply (cut_tac a = a and b = b' in zmod_zdiv_equality)
14.311 apply (rule zdiv_mono2_neg_lemma)
14.312 @@ -698,7 +698,7 @@
14.313
14.314 (** first, four lemmas to bound the remainder for the cases b<0 and b>0 **)
14.315
14.316 -lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r <= 0 |] ==> b*c < b*(q mod c) + r"
14.317 +lemma zmult2_lemma_aux1: "[| (0::int) < c; b < r; r \<le> 0 |] ==> b*c < b*(q mod c) + r"
14.318 apply (subgoal_tac "b * (c - q mod c) < r * 1")
14.319 apply (simp add: zdiff_zmult_distrib2)
14.320 apply (rule order_le_less_trans)
14.321 @@ -708,19 +708,19 @@
14.322 add1_zle_eq pos_mod_bound)
14.323 done
14.324
14.325 -lemma zmult2_lemma_aux2: "[| (0::int) < c; b < r; r <= 0 |] ==> b * (q mod c) + r <= 0"
14.326 -apply (subgoal_tac "b * (q mod c) <= 0")
14.327 +lemma zmult2_lemma_aux2: "[| (0::int) < c; b < r; r \<le> 0 |] ==> b * (q mod c) + r \<le> 0"
14.328 +apply (subgoal_tac "b * (q mod c) \<le> 0")
14.329 apply arith
14.330 apply (simp add: zmult_le_0_iff)
14.331 done
14.332
14.333 -lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 <= r; r < b |] ==> 0 <= b * (q mod c) + r"
14.334 -apply (subgoal_tac "0 <= b * (q mod c) ")
14.335 +lemma zmult2_lemma_aux3: "[| (0::int) < c; 0 \<le> r; r < b |] ==> 0 \<le> b * (q mod c) + r"
14.336 +apply (subgoal_tac "0 \<le> b * (q mod c) ")
14.337 apply arith
14.338 apply (simp add: int_0_le_mult_iff)
14.339 done
14.340
14.341 -lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
14.342 +lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 \<le> r; r < b |] ==> b * (q mod c) + r < b * c"
14.343 apply (subgoal_tac "r * 1 < b * (c - q mod c) ")
14.344 apply (simp add: zdiff_zmult_distrib2)
14.345 apply (rule order_less_le_trans)
14.346 @@ -798,7 +798,7 @@
14.347
14.348 lemma split_pos_lemma:
14.349 "0<k ==>
14.350 - P(n div k :: int)(n mod k) = (\<forall>i j. 0<=j & j<k & n = k*i + j --> P i j)"
14.351 + P(n div k :: int)(n mod k) = (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i j)"
14.352 apply (rule iffI)
14.353 apply clarify
14.354 apply (erule_tac P="P ?x ?y" in rev_mp)
14.355 @@ -813,7 +813,7 @@
14.356
14.357 lemma split_neg_lemma:
14.358 "k<0 ==>
14.359 - P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j<=0 & n = k*i + j --> P i j)"
14.360 + P(n div k :: int)(n mod k) = (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i j)"
14.361 apply (rule iffI)
14.362 apply clarify
14.363 apply (erule_tac P="P ?x ?y" in rev_mp)
14.364 @@ -829,8 +829,8 @@
14.365 lemma split_zdiv:
14.366 "P(n div k :: int) =
14.367 ((k = 0 --> P 0) &
14.368 - (0<k --> (\<forall>i j. 0<=j & j<k & n = k*i + j --> P i)) &
14.369 - (k<0 --> (\<forall>i j. k<j & j<=0 & n = k*i + j --> P i)))"
14.370 + (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) &
14.371 + (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
14.372 apply (case_tac "k=0")
14.373 apply (simp add: DIVISION_BY_ZERO)
14.374 apply (simp only: linorder_neq_iff)
14.375 @@ -842,8 +842,8 @@
14.376 lemma split_zmod:
14.377 "P(n mod k :: int) =
14.378 ((k = 0 --> P n) &
14.379 - (0<k --> (\<forall>i j. 0<=j & j<k & n = k*i + j --> P j)) &
14.380 - (k<0 --> (\<forall>i j. k<j & j<=0 & n = k*i + j --> P j)))"
14.381 + (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) &
14.382 + (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
14.383 apply (case_tac "k=0")
14.384 apply (simp add: DIVISION_BY_ZERO)
14.385 apply (simp only: linorder_neq_iff)
14.386 @@ -861,29 +861,33 @@
14.387
14.388 (** computing div by shifting **)
14.389
14.390 -lemma pos_zdiv_mult_2: "(0::int) <= a ==> (1 + 2*b) div (2*a) = b div a"
14.391 -apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
14.392 -apply (subgoal_tac "1 <= a")
14.393 - prefer 2 apply arith
14.394 -apply (subgoal_tac "1 < a * 2")
14.395 - prefer 2 apply arith
14.396 -apply (subgoal_tac "2* (1 + b mod a) <= 2*a")
14.397 - apply (rule_tac [2] zmult_zle_mono2)
14.398 -apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq
14.399 - pos_mod_bound)
14.400 -apply (subst zdiv_zadd1_eq)
14.401 -apply (simp add: zdiv_zmult_zmult2 zmod_zmult_zmult2 div_pos_pos_trivial)
14.402 -apply (subst div_pos_pos_trivial)
14.403 -apply (auto simp add: mod_pos_pos_trivial)
14.404 -apply (subgoal_tac "0 <= b mod a", arith)
14.405 -apply (simp)
14.406 -done
14.407 +lemma pos_zdiv_mult_2: "(0::int) \<le> a ==> (1 + 2*b) div (2*a) = b div a"
14.408 +proof cases
14.409 + assume "a=0"
14.410 + thus ?thesis by simp
14.411 +next
14.412 + assume "a\<noteq>0" and le_a: "0\<le>a"
14.413 + hence a_pos: "1 \<le> a" by arith
14.414 + hence one_less_a2: "1 < 2*a" by arith
14.415 + hence le_2a: "2 * (1 + b mod a) \<le> 2 * a"
14.416 + by (simp add: mult_le_cancel_left zadd_commute [of 1] add1_zle_eq)
14.417 + with a_pos have "0 \<le> b mod a" by simp
14.418 + hence le_addm: "0 \<le> 1 mod (2*a) + 2*(b mod a)"
14.419 + by (simp add: mod_pos_pos_trivial one_less_a2)
14.420 + with le_2a
14.421 + have "(1 mod (2*a) + 2*(b mod a)) div (2*a) = 0"
14.422 + by (simp add: div_pos_pos_trivial le_addm mod_pos_pos_trivial one_less_a2
14.423 + right_distrib)
14.424 + thus ?thesis
14.425 + by (subst zdiv_zadd1_eq,
14.426 + simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2
14.427 + div_pos_pos_trivial)
14.428 +qed
14.429
14.430 -
14.431 -lemma neg_zdiv_mult_2: "a <= (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"
14.432 +lemma neg_zdiv_mult_2: "a \<le> (0::int) ==> (1 + 2*b) div (2*a) = (b+1) div a"
14.433 apply (subgoal_tac " (1 + 2* (-b - 1)) div (2 * (-a)) = (-b - 1) div (-a) ")
14.434 apply (rule_tac [2] pos_zdiv_mult_2)
14.435 -apply (auto simp add: zmult_zminus_right)
14.436 +apply (auto simp add: zmult_zminus_right right_diff_distrib)
14.437 apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
14.438 apply (simp only: zdiv_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric],
14.439 simp)
14.440 @@ -892,12 +896,12 @@
14.441
14.442 (*Not clear why this must be proved separately; probably number_of causes
14.443 simplification problems*)
14.444 -lemma not_0_le_lemma: "~ 0 <= x ==> x <= (0::int)"
14.445 +lemma not_0_le_lemma: "~ 0 \<le> x ==> x \<le> (0::int)"
14.446 by auto
14.447
14.448 lemma zdiv_number_of_BIT[simp]:
14.449 "number_of (v BIT b) div number_of (w BIT False) =
14.450 - (if ~b | (0::int) <= number_of w
14.451 + (if ~b | (0::int) \<le> number_of w
14.452 then number_of v div (number_of w)
14.453 else (number_of v + (1::int)) div (number_of w))"
14.454 apply (simp only: zadd_assoc number_of_BIT)
14.455 @@ -911,31 +915,31 @@
14.456 (** computing mod by shifting (proofs resemble those for div) **)
14.457
14.458 lemma pos_zmod_mult_2:
14.459 - "(0::int) <= a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"
14.460 + "(0::int) \<le> a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"
14.461 apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
14.462 -apply (subgoal_tac "1 <= a")
14.463 +apply (subgoal_tac "1 \<le> a")
14.464 prefer 2 apply arith
14.465 apply (subgoal_tac "1 < a * 2")
14.466 prefer 2 apply arith
14.467 -apply (subgoal_tac "2* (1 + b mod a) <= 2*a")
14.468 +apply (subgoal_tac "2* (1 + b mod a) \<le> 2*a")
14.469 apply (rule_tac [2] zmult_zle_mono2)
14.470 apply (auto simp add: zadd_commute [of 1] zmult_commute add1_zle_eq
14.471 pos_mod_bound)
14.472 apply (subst zmod_zadd1_eq)
14.473 apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
14.474 apply (rule mod_pos_pos_trivial)
14.475 -apply (auto simp add: mod_pos_pos_trivial)
14.476 -apply (subgoal_tac "0 <= b mod a", arith)
14.477 +apply (auto simp add: mod_pos_pos_trivial left_distrib)
14.478 +apply (subgoal_tac "0 \<le> b mod a", arith)
14.479 apply (simp)
14.480 done
14.481
14.482
14.483 lemma neg_zmod_mult_2:
14.484 - "a <= (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1"
14.485 + "a \<le> (0::int) ==> (1 + 2*b) mod (2*a) = 2 * ((b+1) mod a) - 1"
14.486 apply (subgoal_tac "(1 + 2* (-b - 1)) mod (2* (-a)) =
14.487 1 + 2* ((-b - 1) mod (-a))")
14.488 apply (rule_tac [2] pos_zmod_mult_2)
14.489 -apply (auto simp add: zmult_zminus_right)
14.490 +apply (auto simp add: zmult_zminus_right right_diff_distrib)
14.491 apply (subgoal_tac " (-1 - (2 * b)) = - (1 + (2 * b))")
14.492 prefer 2 apply simp
14.493 apply (simp only: zmod_zminus_zminus zdiff_def zminus_zadd_distrib [symmetric])
14.494 @@ -944,7 +948,7 @@
14.495 lemma zmod_number_of_BIT [simp]:
14.496 "number_of (v BIT b) mod number_of (w BIT False) =
14.497 (if b then
14.498 - if (0::int) <= number_of w
14.499 + if (0::int) \<le> number_of w
14.500 then 2 * (number_of v mod number_of w) + 1
14.501 else 2 * ((number_of v + (1::int)) mod number_of w) - 1
14.502 else 2 * (number_of v mod number_of w))"
14.503 @@ -958,16 +962,16 @@
14.504 (** Quotients of signs **)
14.505
14.506 lemma div_neg_pos_less0: "[| a < (0::int); 0 < b |] ==> a div b < 0"
14.507 -apply (subgoal_tac "a div b <= -1", force)
14.508 +apply (subgoal_tac "a div b \<le> -1", force)
14.509 apply (rule order_trans)
14.510 apply (rule_tac a' = "-1" in zdiv_mono1)
14.511 apply (auto simp add: zdiv_minus1)
14.512 done
14.513
14.514 -lemma div_nonneg_neg_le0: "[| (0::int) <= a; b < 0 |] ==> a div b <= 0"
14.515 +lemma div_nonneg_neg_le0: "[| (0::int) \<le> a; b < 0 |] ==> a div b \<le> 0"
14.516 by (drule zdiv_mono1_neg, auto)
14.517
14.518 -lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 <= a div b) = (0 <= a)"
14.519 +lemma pos_imp_zdiv_nonneg_iff: "(0::int) < b ==> (0 \<le> a div b) = (0 \<le> a)"
14.520 apply auto
14.521 apply (drule_tac [2] zdiv_mono1)
14.522 apply (auto simp add: linorder_neq_iff)
14.523 @@ -976,16 +980,16 @@
14.524 done
14.525
14.526 lemma neg_imp_zdiv_nonneg_iff:
14.527 - "b < (0::int) ==> (0 <= a div b) = (a <= (0::int))"
14.528 + "b < (0::int) ==> (0 \<le> a div b) = (a \<le> (0::int))"
14.529 apply (subst zdiv_zminus_zminus [symmetric])
14.530 apply (subst pos_imp_zdiv_nonneg_iff, auto)
14.531 done
14.532
14.533 -(*But not (a div b <= 0 iff a<=0); consider a=1, b=2 when a div b = 0.*)
14.534 +(*But not (a div b \<le> 0 iff a\<le>0); consider a=1, b=2 when a div b = 0.*)
14.535 lemma pos_imp_zdiv_neg_iff: "(0::int) < b ==> (a div b < 0) = (a < 0)"
14.536 by (simp add: linorder_not_le [symmetric] pos_imp_zdiv_nonneg_iff)
14.537
14.538 -(*Again the law fails for <=: consider a = -1, b = -2 when a div b = 0*)
14.539 +(*Again the law fails for \<le>: consider a = -1, b = -2 when a div b = 0*)
14.540 lemma neg_imp_zdiv_neg_iff: "b < (0::int) ==> (a div b < 0) = (0 < a)"
14.541 by (simp add: linorder_not_le [symmetric] neg_imp_zdiv_nonneg_iff)
14.542
14.543 @@ -1150,7 +1154,7 @@
14.544 apply (rule_tac [!] x = "-k" in exI, auto)
14.545 done
14.546
14.547 -lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z <= (n::int)"
14.548 +lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
14.549 apply (rule_tac z=n in int_cases)
14.550 apply (auto simp add: dvd_int_iff)
14.551 apply (rule_tac z=z in int_cases)
15.1 --- a/src/HOL/Integ/NatBin.thy Wed Dec 10 14:29:44 2003 +0100
15.2 +++ b/src/HOL/Integ/NatBin.thy Wed Dec 10 15:59:34 2003 +0100
15.3 @@ -425,7 +425,7 @@
15.4 "((number_of (v BIT x) ::int) = number_of (w BIT y)) =
15.5 (x=y & (((number_of v) ::int) = number_of w))"
15.6 by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute
15.7 - Ring_and_Field.add_left_cancel add_assoc left_zero
15.8 + Ring_and_Field.add_left_cancel add_assoc Ring_and_Field.add_0
15.9 split add: split_if cong: imp_cong)
15.10
15.11
16.1 --- a/src/HOL/Integ/NatSimprocs.thy Wed Dec 10 14:29:44 2003 +0100
16.2 +++ b/src/HOL/Integ/NatSimprocs.thy Wed Dec 10 15:59:34 2003 +0100
16.3 @@ -132,4 +132,65 @@
16.4 declare Suc_div_eq_add3_div [of _ "number_of v", standard, simp]
16.5 declare Suc_mod_eq_add3_mod [of _ "number_of v", standard, simp]
16.6
16.7 +
16.8 +subsection{*Special Simplification for Constants*}
16.9 +
16.10 +text{*These belong here, late in the development of HOL, to prevent their
16.11 +interfering with proofs of abstract properties of instances of the function
16.12 +@{term number_of}*}
16.13 +
16.14 +text{*These distributive laws move literals inside sums and differences.*}
16.15 +declare left_distrib [of _ _ "number_of v", standard, simp]
16.16 +declare right_distrib [of "number_of v", standard, simp]
16.17 +
16.18 +declare left_diff_distrib [of _ _ "number_of v", standard, simp]
16.19 +declare right_diff_distrib [of "number_of v", standard, simp]
16.20 +
16.21 +text{*These are actually for fields, like real: but where else to put them?*}
16.22 +declare zero_less_divide_iff [of "number_of w", standard, simp]
16.23 +declare divide_less_0_iff [of "number_of w", standard, simp]
16.24 +declare zero_le_divide_iff [of "number_of w", standard, simp]
16.25 +declare divide_le_0_iff [of "number_of w", standard, simp]
16.26 +
16.27 +(*Replaces "inverse #nn" by 1/#nn *)
16.28 +declare inverse_eq_divide [of "number_of w", standard, simp]
16.29 +
16.30 +text{*These laws simplify inequalities, moving unary minus from a term
16.31 +into the literal.*}
16.32 +declare less_minus_iff [of "number_of v", standard, simp]
16.33 +declare le_minus_iff [of "number_of v", standard, simp]
16.34 +declare equation_minus_iff [of "number_of v", standard, simp]
16.35 +
16.36 +declare minus_less_iff [of _ "number_of v", standard, simp]
16.37 +declare minus_le_iff [of _ "number_of v", standard, simp]
16.38 +declare minus_equation_iff [of _ "number_of v", standard, simp]
16.39 +
16.40 +text{*These simplify inequalities where one side is the constant 1.*}
16.41 +declare less_minus_iff [of 1, simplified, simp]
16.42 +declare le_minus_iff [of 1, simplified, simp]
16.43 +declare equation_minus_iff [of 1, simplified, simp]
16.44 +
16.45 +declare minus_less_iff [of _ 1, simplified, simp]
16.46 +declare minus_le_iff [of _ 1, simplified, simp]
16.47 +declare minus_equation_iff [of _ 1, simplified, simp]
16.48 +
16.49 +
16.50 +(*Cancellation of constant factors in comparisons (< and \<le>) *)
16.51 +
16.52 +declare mult_less_cancel_left [of "number_of v", standard, simp]
16.53 +declare mult_less_cancel_right [of _ "number_of v", standard, simp]
16.54 +declare mult_le_cancel_left [of "number_of v", standard, simp]
16.55 +declare mult_le_cancel_right [of _ "number_of v", standard, simp]
16.56 +
16.57 +
16.58 +(*Multiplying out constant divisors in comparisons (< \<le> and =) *)
16.59 +
16.60 +declare le_divide_eq [of _ _ "number_of w", standard, simp]
16.61 +declare divide_le_eq [of _ "number_of w", standard, simp]
16.62 +declare less_divide_eq [of _ _ "number_of w", standard, simp]
16.63 +declare divide_less_eq [of _ "number_of w", standard, simp]
16.64 +declare eq_divide_eq [of _ _ "number_of w", standard, simp]
16.65 +declare divide_eq_eq [of _ "number_of w", standard, simp]
16.66 +
16.67 +
16.68 end
17.1 --- a/src/HOL/IsaMakefile Wed Dec 10 14:29:44 2003 +0100
17.2 +++ b/src/HOL/IsaMakefile Wed Dec 10 15:59:34 2003 +0100
17.3 @@ -224,6 +224,8 @@
17.4 HOL-Induct: HOL $(LOG)/HOL-Induct.gz
17.5
17.6 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
17.7 + Induct/BinaryTree.thy Induct/BinaryTree_Map.thy\
17.8 + Induct/BinaryTree_TacticStyle.thy\
17.9 Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
17.10 Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
17.11 Induct/PropLog.thy Induct/ROOT.ML \
18.1 --- a/src/HOL/Numeral.thy Wed Dec 10 14:29:44 2003 +0100
18.2 +++ b/src/HOL/Numeral.thy Wed Dec 10 15:59:34 2003 +0100
18.3 @@ -57,4 +57,5 @@
18.4 lemma Let_1 [simp]: "Let 1 f == f 1"
18.5 by (simp add: Let_def)
18.6
18.7 +
18.8 end
19.1 --- a/src/HOL/Real/RealArith.thy Wed Dec 10 14:29:44 2003 +0100
19.2 +++ b/src/HOL/Real/RealArith.thy Wed Dec 10 15:59:34 2003 +0100
19.3 @@ -1,10 +1,80 @@
19.4 theory RealArith = RealArith0
19.5 files ("real_arith.ML"):
19.6
19.7 +lemma real_divide_1: "(x::real)/1 = x"
19.8 +by (simp add: real_divide_def)
19.9 +
19.10 use "real_arith.ML"
19.11
19.12 setup real_arith_setup
19.13
19.14 +subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
19.15 +
19.16 +text{*Needed in this non-standard form by Hyperreal/Transcendental*}
19.17 +lemma real_0_le_divide_iff:
19.18 + "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))"
19.19 +by (simp add: real_divide_def zero_le_mult_iff, auto)
19.20 +
19.21 +lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
19.22 +by arith
19.23 +
19.24 +lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)"
19.25 +by auto
19.26 +
19.27 +lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)"
19.28 +by auto
19.29 +
19.30 +lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)"
19.31 +by auto
19.32 +
19.33 +lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)"
19.34 +by auto
19.35 +
19.36 +lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)"
19.37 +by auto
19.38 +
19.39 +
19.40 +(** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc.,
19.41 + in RealBin
19.42 +**)
19.43 +
19.44 +lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)"
19.45 +by auto
19.46 +
19.47 +lemma real_0_le_diff_iff [iff]: "((0::real) \<le> x-y) = (y \<le> x)"
19.48 +by auto
19.49 +
19.50 +(*
19.51 +FIXME: we should have this, as for type int, but many proofs would break.
19.52 +It replaces x+-y by x-y.
19.53 +Addsimps [symmetric real_diff_def]
19.54 +*)
19.55 +
19.56 +(** Division by 1, -1 **)
19.57 +
19.58 +lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)"
19.59 +by simp
19.60 +
19.61 +lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)"
19.62 +by (simp add: real_divide_def real_minus_inverse)
19.63 +
19.64 +lemma real_lbound_gt_zero:
19.65 + "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
19.66 +apply (rule_tac x = " (min d1 d2) /2" in exI)
19.67 +apply (simp add: min_def)
19.68 +done
19.69 +
19.70 +(*** Density of the Reals ***)
19.71 +
19.72 +lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
19.73 +by auto
19.74 +
19.75 +lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
19.76 +by auto
19.77 +
19.78 +lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y"
19.79 +by (blast intro!: real_less_half_sum real_gt_half_sum)
19.80 +
19.81 subsection{*Absolute Value Function for the Reals*}
19.82
19.83 (** abs (absolute value) **)
19.84 @@ -214,8 +284,25 @@
19.85 apply (rule abs_triangle_ineq)
19.86 done
19.87
19.88 +
19.89 ML
19.90 {*
19.91 +val real_0_le_divide_iff = thm"real_0_le_divide_iff";
19.92 +val real_add_minus_iff = thm"real_add_minus_iff";
19.93 +val real_add_eq_0_iff = thm"real_add_eq_0_iff";
19.94 +val real_add_less_0_iff = thm"real_add_less_0_iff";
19.95 +val real_0_less_add_iff = thm"real_0_less_add_iff";
19.96 +val real_add_le_0_iff = thm"real_add_le_0_iff";
19.97 +val real_0_le_add_iff = thm"real_0_le_add_iff";
19.98 +val real_0_less_diff_iff = thm"real_0_less_diff_iff";
19.99 +val real_0_le_diff_iff = thm"real_0_le_diff_iff";
19.100 +val real_divide_minus1 = thm"real_divide_minus1";
19.101 +val real_minus1_divide = thm"real_minus1_divide";
19.102 +val real_lbound_gt_zero = thm"real_lbound_gt_zero";
19.103 +val real_less_half_sum = thm"real_less_half_sum";
19.104 +val real_gt_half_sum = thm"real_gt_half_sum";
19.105 +val real_dense = thm"real_dense";
19.106 +
19.107 val abs_nat_number_of = thm"abs_nat_number_of";
19.108 val abs_split = thm"abs_split";
19.109 val abs_iff = thm"abs_iff";
20.1 --- a/src/HOL/Real/RealArith0.ML Wed Dec 10 14:29:44 2003 +0100
20.2 +++ b/src/HOL/Real/RealArith0.ML Wed Dec 10 15:59:34 2003 +0100
20.3 @@ -6,9 +6,7 @@
20.4 Common factor cancellation
20.5 *)
20.6
20.7 -val real_diff_minus_eq = thm"real_diff_minus_eq";
20.8 val real_inverse_eq_divide = thm"real_inverse_eq_divide";
20.9 -val real_0_le_divide_iff = thm"real_0_le_divide_iff";
20.10 val real_mult_less_cancel2 = thm"real_mult_less_cancel2";
20.11 val real_mult_le_cancel2 = thm"real_mult_le_cancel2";
20.12 val real_mult_less_cancel1 = thm"real_mult_less_cancel1";
20.13 @@ -207,33 +205,10 @@
20.14 test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z";
20.15 *)
20.16
20.17 -val real_add_minus_iff = thm"real_add_minus_iff";
20.18 -val real_add_eq_0_iff = thm"real_add_eq_0_iff";
20.19 -val real_add_less_0_iff = thm"real_add_less_0_iff";
20.20 -val real_0_less_add_iff = thm"real_0_less_add_iff";
20.21 -val real_add_le_0_iff = thm"real_add_le_0_iff";
20.22 -val real_0_le_add_iff = thm"real_0_le_add_iff";
20.23 -val real_0_less_diff_iff = thm"real_0_less_diff_iff";
20.24 -val real_0_le_diff_iff = thm"real_0_le_diff_iff";
20.25 -val real_divide_eq_cancel2 = thm"real_divide_eq_cancel2";
20.26 -val real_divide_eq_cancel1 = thm"real_divide_eq_cancel1";
20.27 val real_inverse_less_iff = thm"real_inverse_less_iff";
20.28 val real_inverse_le_iff = thm"real_inverse_le_iff";
20.29 -val real_divide_1 = thm"real_divide_1";
20.30 -val real_divide_minus1 = thm"real_divide_minus1";
20.31 -val real_minus1_divide = thm"real_minus1_divide";
20.32 -val real_lbound_gt_zero = thm"real_lbound_gt_zero";
20.33 -val real_less_half_sum = thm"real_less_half_sum";
20.34 -val real_gt_half_sum = thm"real_gt_half_sum";
20.35 -val real_dense = thm"real_dense";
20.36
20.37 -val pos_real_less_divide_eq = thm"pos_real_less_divide_eq";
20.38 -val neg_real_less_divide_eq = thm"neg_real_less_divide_eq";
20.39 -val pos_real_divide_less_eq = thm"pos_real_divide_less_eq";
20.40 -val neg_real_divide_less_eq = thm"neg_real_divide_less_eq";
20.41 -val pos_real_le_divide_eq = thm"pos_real_le_divide_eq";
20.42 -val neg_real_le_divide_eq = thm"neg_real_le_divide_eq";
20.43 -val pos_real_divide_le_eq = thm"pos_real_divide_le_eq";
20.44 -val neg_real_divide_le_eq = thm"neg_real_divide_le_eq";
20.45 -val real_eq_divide_eq = thm"real_eq_divide_eq";
20.46 -val real_divide_eq_eq = thm"real_divide_eq_eq";
20.47 +val pos_real_less_divide_eq = thm"pos_less_divide_eq";
20.48 +val pos_real_divide_less_eq = thm"pos_divide_less_eq";
20.49 +val pos_real_le_divide_eq = thm"pos_le_divide_eq";
20.50 +val pos_real_divide_le_eq = thm"pos_divide_le_eq";
21.1 --- a/src/HOL/Real/RealArith0.thy Wed Dec 10 14:29:44 2003 +0100
21.2 +++ b/src/HOL/Real/RealArith0.thy Wed Dec 10 15:59:34 2003 +0100
21.3 @@ -1,270 +1,6 @@
21.4 theory RealArith0 = RealBin
21.5 files "real_arith0.ML":
21.6
21.7 -(*FIXME: move results further down to Ring_and_Field*)
21.8 -
21.9 setup real_arith_setup
21.10
21.11 -subsection{*Facts that need the Arithmetic Decision Procedure*}
21.12 -
21.13 -lemma real_diff_minus_eq: "x - - y = x + (y::real)"
21.14 -by simp
21.15 -declare real_diff_minus_eq [simp]
21.16 -
21.17 -(** Division and inverse **)
21.18 -
21.19 -lemma real_inverse_eq_divide: "inverse (x::real) = 1/x"
21.20 - by (rule Ring_and_Field.inverse_eq_divide)
21.21 -
21.22 -text{*Needed in this non-standard form by Hyperreal/Transcendental*}
21.23 -lemma real_0_le_divide_iff:
21.24 - "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))"
21.25 -by (simp add: real_divide_def real_0_le_mult_iff, auto)
21.26 -
21.27 -
21.28 -(**** Factor cancellation theorems for "real" ****)
21.29 -
21.30 -(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =,
21.31 - but not (yet?) for k*m < n*k. **)
21.32 -
21.33 -lemma real_mult_less_cancel2:
21.34 - "(m*k < n*k) = (((0::real) < k & m<n) | (k < 0 & n<m))"
21.35 - by (rule Ring_and_Field.mult_less_cancel_right)
21.36 -
21.37 -lemma real_mult_le_cancel2:
21.38 - "(m*k <= n*k) = (((0::real) < k --> m<=n) & (k < 0 --> n<=m))"
21.39 - by (rule Ring_and_Field.mult_le_cancel_right)
21.40 -
21.41 -lemma real_mult_less_cancel1:
21.42 - "(k*m < k*n) = (((0::real) < k & m<n) | (k < 0 & n<m))"
21.43 - by (rule Ring_and_Field.mult_less_cancel_left)
21.44 -
21.45 -lemma real_mult_le_cancel1:
21.46 - "!!k::real. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))"
21.47 - by (rule Ring_and_Field.mult_le_cancel_left)
21.48 -
21.49 -lemma real_mult_eq_cancel1: "!!k::real. (k*m = k*n) = (k = 0 | m=n)"
21.50 - by (rule Ring_and_Field.mult_cancel_left)
21.51 -
21.52 -lemma real_mult_eq_cancel2: "!!k::real. (m*k = n*k) = (k = 0 | m=n)"
21.53 - by (rule Ring_and_Field.mult_cancel_right)
21.54 -
21.55 -lemma real_mult_div_cancel1: "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)"
21.56 - by (rule Ring_and_Field.mult_divide_cancel_left)
21.57 -
21.58 -lemma real_mult_div_cancel_disj:
21.59 - "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)"
21.60 - by (rule Ring_and_Field.mult_divide_cancel_eq_if)
21.61 -
21.62 -subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
21.63 -
21.64 -lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
21.65 -by arith
21.66 -
21.67 -lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)"
21.68 -by auto
21.69 -
21.70 -lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)"
21.71 -by auto
21.72 -
21.73 -lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)"
21.74 -by auto
21.75 -
21.76 -lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)"
21.77 -by auto
21.78 -
21.79 -lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)"
21.80 -by auto
21.81 -
21.82 -
21.83 -(** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc.,
21.84 - in RealBin
21.85 -**)
21.86 -
21.87 -lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)"
21.88 -by auto
21.89 -
21.90 -lemma real_0_le_diff_iff [iff]: "((0::real) \<le> x-y) = (y \<le> x)"
21.91 -by auto
21.92 -
21.93 -(*
21.94 -FIXME: we should have this, as for type int, but many proofs would break.
21.95 -It replaces x+-y by x-y.
21.96 -Addsimps [symmetric real_diff_def]
21.97 -*)
21.98 -
21.99 -
21.100 -(*FIXME: move most of these to Ring_and_Field*)
21.101 -
21.102 -subsection{*Simplification of Inequalities Involving Literal Divisors*}
21.103 -
21.104 -lemma pos_real_le_divide_eq: "0<z ==> ((x::real) \<le> y/z) = (x*z \<le> y)"
21.105 -apply (subgoal_tac " (x*z \<le> y) = (x*z \<le> (y/z) *z) ")
21.106 - prefer 2 apply (simp add: real_divide_def real_mult_assoc)
21.107 -apply (erule ssubst)
21.108 -apply (subst real_mult_le_cancel2, simp)
21.109 -done
21.110 -
21.111 -lemma neg_real_le_divide_eq: "z<0 ==> ((x::real) \<le> y/z) = (y \<le> x*z)"
21.112 -apply (subgoal_tac " (y \<le> x*z) = ((y/z) *z \<le> x*z) ")
21.113 - prefer 2 apply (simp add: real_divide_def real_mult_assoc)
21.114 -apply (erule ssubst)
21.115 -apply (subst real_mult_le_cancel2, simp)
21.116 -done
21.117 -
21.118 -lemma real_le_divide_eq:
21.119 - "((x::real) \<le> y/z) = (if 0<z then x*z \<le> y
21.120 - else if z<0 then y \<le> x*z
21.121 - else x\<le>0)"
21.122 -apply (case_tac "z=0", simp)
21.123 -apply (simp add: pos_real_le_divide_eq neg_real_le_divide_eq)
21.124 -done
21.125 -
21.126 -declare real_le_divide_eq [of _ _ "number_of w", standard, simp]
21.127 -
21.128 -lemma pos_real_divide_le_eq: "0<z ==> (y/z \<le> (x::real)) = (y \<le> x*z)"
21.129 -apply (subgoal_tac " (y \<le> x*z) = ((y/z) *z \<le> x*z) ")
21.130 - prefer 2 apply (simp add: real_divide_def real_mult_assoc)
21.131 -apply (erule ssubst)
21.132 -apply (subst real_mult_le_cancel2, simp)
21.133 -done
21.134 -
21.135 -lemma neg_real_divide_le_eq: "z<0 ==> (y/z \<le> (x::real)) = (x*z \<le> y)"
21.136 -apply (subgoal_tac " (x*z \<le> y) = (x*z \<le> (y/z) *z) ")
21.137 - prefer 2 apply (simp add: real_divide_def real_mult_assoc)
21.138 -apply (erule ssubst)
21.139 -apply (subst real_mult_le_cancel2, simp)
21.140 -done
21.141 -
21.142 -
21.143 -lemma real_divide_le_eq:
21.144 - "(y/z \<le> (x::real)) = (if 0<z then y \<le> x*z
21.145 - else if z<0 then x*z \<le> y
21.146 - else 0 \<le> x)"
21.147 -apply (case_tac "z=0", simp)
21.148 -apply (simp add: pos_real_divide_le_eq neg_real_divide_le_eq)
21.149 -done
21.150 -
21.151 -declare real_divide_le_eq [of _ "number_of w", standard, simp]
21.152 -
21.153 -
21.154 -lemma pos_real_less_divide_eq: "0<z ==> ((x::real) < y/z) = (x*z < y)"
21.155 -apply (subgoal_tac " (x*z < y) = (x*z < (y/z) *z) ")
21.156 - prefer 2 apply (simp add: real_divide_def real_mult_assoc)
21.157 -apply (erule ssubst)
21.158 -apply (subst real_mult_less_cancel2, simp)
21.159 -done
21.160 -
21.161 -lemma neg_real_less_divide_eq: "z<0 ==> ((x::real) < y/z) = (y < x*z)"
21.162 -apply (subgoal_tac " (y < x*z) = ((y/z) *z < x*z) ")
21.163 - prefer 2 apply (simp add: real_divide_def real_mult_assoc)
21.164 -apply (erule ssubst)
21.165 -apply (subst real_mult_less_cancel2, simp)
21.166 -done
21.167 -
21.168 -lemma real_less_divide_eq:
21.169 - "((x::real) < y/z) = (if 0<z then x*z < y
21.170 - else if z<0 then y < x*z
21.171 - else x<0)"
21.172 -apply (case_tac "z=0", simp)
21.173 -apply (simp add: pos_real_less_divide_eq neg_real_less_divide_eq)
21.174 -done
21.175 -
21.176 -declare real_less_divide_eq [of _ _ "number_of w", standard, simp]
21.177 -
21.178 -lemma pos_real_divide_less_eq: "0<z ==> (y/z < (x::real)) = (y < x*z)"
21.179 -apply (subgoal_tac " (y < x*z) = ((y/z) *z < x*z) ")
21.180 - prefer 2 apply (simp add: real_divide_def real_mult_assoc)
21.181 -apply (erule ssubst)
21.182 -apply (subst real_mult_less_cancel2, simp)
21.183 -done
21.184 -
21.185 -lemma neg_real_divide_less_eq: "z<0 ==> (y/z < (x::real)) = (x*z < y)"
21.186 -apply (subgoal_tac " (x*z < y) = (x*z < (y/z) *z) ")
21.187 - prefer 2 apply (simp add: real_divide_def real_mult_assoc)
21.188 -apply (erule ssubst)
21.189 -apply (subst real_mult_less_cancel2, simp)
21.190 -done
21.191 -
21.192 -lemma real_divide_less_eq:
21.193 - "(y/z < (x::real)) = (if 0<z then y < x*z
21.194 - else if z<0 then x*z < y
21.195 - else 0 < x)"
21.196 -apply (case_tac "z=0", simp)
21.197 -apply (simp add: pos_real_divide_less_eq neg_real_divide_less_eq)
21.198 -done
21.199 -
21.200 -declare real_divide_less_eq [of _ "number_of w", standard, simp]
21.201 -
21.202 -lemma nonzero_real_eq_divide_eq: "z\<noteq>0 ==> ((x::real) = y/z) = (x*z = y)"
21.203 -apply (subgoal_tac " (x*z = y) = (x*z = (y/z) *z) ")
21.204 - prefer 2 apply (simp add: real_divide_def real_mult_assoc)
21.205 -apply (erule ssubst)
21.206 -apply (subst real_mult_eq_cancel2, simp)
21.207 -done
21.208 -
21.209 -lemma real_eq_divide_eq:
21.210 - "((x::real) = y/z) = (if z\<noteq>0 then x*z = y else x=0)"
21.211 -by (simp add: nonzero_real_eq_divide_eq)
21.212 -
21.213 -declare real_eq_divide_eq [of _ _ "number_of w", standard, simp]
21.214 -
21.215 -lemma nonzero_real_divide_eq_eq: "z\<noteq>0 ==> (y/z = (x::real)) = (y = x*z)"
21.216 -apply (subgoal_tac " (y = x*z) = ((y/z) *z = x*z) ")
21.217 - prefer 2 apply (simp add: real_divide_def real_mult_assoc)
21.218 -apply (erule ssubst)
21.219 -apply (subst real_mult_eq_cancel2, simp)
21.220 -done
21.221 -
21.222 -lemma real_divide_eq_eq:
21.223 - "(y/z = (x::real)) = (if z\<noteq>0 then y = x*z else x=0)"
21.224 -by (simp add: nonzero_real_divide_eq_eq)
21.225 -
21.226 -declare real_divide_eq_eq [of _ "number_of w", standard, simp]
21.227 -
21.228 -lemma real_divide_eq_cancel2: "(m/k = n/k) = (k = 0 | m = (n::real))"
21.229 -apply (case_tac "k=0", simp)
21.230 -apply (simp add:divide_inverse)
21.231 -done
21.232 -
21.233 -lemma real_divide_eq_cancel1: "(k/m = k/n) = (k = 0 | m = (n::real))"
21.234 -by (force simp add: real_divide_eq_eq real_eq_divide_eq)
21.235 -
21.236 -lemma real_inverse_less_iff:
21.237 - "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)"
21.238 -by (rule Ring_and_Field.inverse_less_iff_less)
21.239 -
21.240 -lemma real_inverse_le_iff:
21.241 - "[| 0 < r; 0 < x|] ==> (inverse x \<le> inverse r) = (r \<le> (x::real))"
21.242 -by (rule Ring_and_Field.inverse_le_iff_le)
21.243 -
21.244 -
21.245 -(** Division by 1, -1 **)
21.246 -
21.247 -lemma real_divide_1: "(x::real)/1 = x"
21.248 -by (simp add: real_divide_def)
21.249 -
21.250 -lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)"
21.251 -by simp
21.252 -
21.253 -lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)"
21.254 -by (simp add: real_divide_def real_minus_inverse)
21.255 -
21.256 -lemma real_lbound_gt_zero:
21.257 - "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2"
21.258 -apply (rule_tac x = " (min d1 d2) /2" in exI)
21.259 -apply (simp add: min_def)
21.260 -done
21.261 -
21.262 -(*** Density of the Reals ***)
21.263 -
21.264 -lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"
21.265 -by auto
21.266 -
21.267 -lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
21.268 -by auto
21.269 -
21.270 -lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y"
21.271 -by (blast intro!: real_less_half_sum real_gt_half_sum)
21.272 -
21.273 end
22.1 --- a/src/HOL/Real/RealOrd.thy Wed Dec 10 14:29:44 2003 +0100
22.2 +++ b/src/HOL/Real/RealOrd.thy Wed Dec 10 15:59:34 2003 +0100
22.3 @@ -280,6 +280,9 @@
22.4 lemma real_mult_not_zero: "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::real)"
22.5 by simp
22.6
22.7 +lemma real_inverse_eq_divide: "inverse (x::real) = 1/x"
22.8 + by (rule Ring_and_Field.inverse_eq_divide)
22.9 +
22.10 lemma real_inverse_inverse: "inverse(inverse (x::real)) = x"
22.11 by (rule Ring_and_Field.inverse_inverse_eq)
22.12
22.13 @@ -292,22 +295,6 @@
22.14 lemma real_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::real)"
22.15 by (rule Ring_and_Field.inverse_mult_distrib)
22.16
22.17 -lemma real_times_divide1_eq: "(x::real) * (y/z) = (x*y)/z"
22.18 -by (simp add: real_divide_def real_mult_assoc)
22.19 -
22.20 -lemma real_times_divide2_eq: "(y/z) * (x::real) = (y*x)/z"
22.21 -by (simp add: real_divide_def real_mult_ac)
22.22 -
22.23 -declare real_times_divide1_eq [simp] real_times_divide2_eq [simp]
22.24 -
22.25 -lemma real_divide_divide1_eq: "(x::real) / (y/z) = (x*z)/y"
22.26 -by (simp add: real_divide_def real_inverse_distrib real_mult_ac)
22.27 -
22.28 -lemma real_divide_divide2_eq: "((x::real) / y) / z = x/(y*z)"
22.29 -by (simp add: real_divide_def real_inverse_distrib real_mult_assoc)
22.30 -
22.31 -declare real_divide_divide1_eq [simp] real_divide_divide2_eq [simp]
22.32 -
22.33 (** As with multiplication, pull minus signs OUT of the / operator **)
22.34
22.35 lemma real_minus_divide_eq: "(-x) / (y::real) = - (x/y)"
22.36 @@ -376,6 +363,38 @@
22.37 by (rule Ring_and_Field.add_le_cancel_left)
22.38
22.39
22.40 +subsection{*Factor Cancellation Theorems for Type @{text real}*}
22.41 +
22.42 +lemma real_mult_less_cancel2:
22.43 + "(m*k < n*k) = (((0::real) < k & m<n) | (k < 0 & n<m))"
22.44 + by (rule Ring_and_Field.mult_less_cancel_right)
22.45 +
22.46 +lemma real_mult_le_cancel2:
22.47 + "(m*k <= n*k) = (((0::real) < k --> m<=n) & (k < 0 --> n<=m))"
22.48 + by (rule Ring_and_Field.mult_le_cancel_right)
22.49 +
22.50 +lemma real_mult_less_cancel1:
22.51 + "(k*m < k*n) = (((0::real) < k & m<n) | (k < 0 & n<m))"
22.52 + by (rule Ring_and_Field.mult_less_cancel_left)
22.53 +
22.54 +lemma real_mult_le_cancel1:
22.55 + "!!k::real. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))"
22.56 + by (rule Ring_and_Field.mult_le_cancel_left)
22.57 +
22.58 +lemma real_mult_eq_cancel1: "!!k::real. (k*m = k*n) = (k = 0 | m=n)"
22.59 + by (rule Ring_and_Field.mult_cancel_left)
22.60 +
22.61 +lemma real_mult_eq_cancel2: "!!k::real. (m*k = n*k) = (k = 0 | m=n)"
22.62 + by (rule Ring_and_Field.mult_cancel_right)
22.63 +
22.64 +lemma real_mult_div_cancel1: "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)"
22.65 + by (rule Ring_and_Field.mult_divide_cancel_left)
22.66 +
22.67 +lemma real_mult_div_cancel_disj:
22.68 + "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)"
22.69 + by (rule Ring_and_Field.mult_divide_cancel_eq_if)
22.70 +
22.71 +
22.72 subsection{*For the @{text abel_cancel} Simproc (DELETE)*}
22.73
22.74 lemma real_eq_eqI: "(x::real) - y = x' - y' ==> (x=y) = (x'=y')"
22.75 @@ -563,15 +582,6 @@
22.76 lemma real_inverse_less_0: "x < 0 ==> inverse (x::real) < 0"
22.77 by (rule Ring_and_Field.negative_imp_inverse_negative)
22.78
22.79 -lemma real_mult_less_cancel1: "[| (0::real) < z; x * z < y * z |] ==> x < y"
22.80 -by (force simp add: Ring_and_Field.mult_less_cancel_right
22.81 - elim: order_less_asym)
22.82 -
22.83 -lemma real_mult_less_cancel2: "[| (0::real) < z; z*x < z*y |] ==> x < y"
22.84 -apply (erule real_mult_less_cancel1)
22.85 -apply (simp add: real_mult_commute)
22.86 -done
22.87 -
22.88 lemma real_mult_less_mono1: "[| (0::real) < z; x < y |] ==> x*z < y*z"
22.89 by (rule Ring_and_Field.mult_strict_right_mono)
22.90
22.91 @@ -580,17 +590,15 @@
22.92 by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le)
22.93
22.94 lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
22.95 -by (blast intro: real_mult_less_mono1 real_mult_less_cancel1)
22.96 + by (force elim: order_less_asym
22.97 + simp add: Ring_and_Field.mult_less_cancel_right)
22.98
22.99 -lemma real_mult_less_iff2 [simp]: "(0::real) < z ==> (z*x < z*y) = (x < y)"
22.100 -by (blast intro: real_mult_less_mono2 real_mult_less_cancel2)
22.101 -
22.102 -(* 05/00 *)
22.103 lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
22.104 by (auto simp add: real_le_def)
22.105
22.106 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
22.107 -by (auto simp add: real_le_def)
22.108 + by (force elim: order_less_asym
22.109 + simp add: Ring_and_Field.mult_le_cancel_left)
22.110
22.111 lemma real_mult_less_mono':
22.112 "[| x < y; r1 < r2; (0::real) \<le> r1; 0 \<le> x|] ==> r1 * x < r2 * y"
22.113 @@ -605,17 +613,23 @@
22.114 "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"
22.115 by (rule Ring_and_Field.less_imp_inverse_less)
22.116
22.117 +lemma real_inverse_less_iff:
22.118 + "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)"
22.119 +by (rule Ring_and_Field.inverse_less_iff_less)
22.120 +
22.121 +lemma real_inverse_le_iff:
22.122 + "[| 0 < r; 0 < x|] ==> (inverse x \<le> inverse r) = (r \<le> (x::real))"
22.123 +by (rule Ring_and_Field.inverse_le_iff_le)
22.124 +
22.125 +(*FIXME: remove the [iff], since the general theorem is already [simp]*)
22.126 lemma real_mult_is_0 [iff]: "(x*y = 0) = (x = 0 | y = (0::real))"
22.127 -by auto
22.128 +by (rule Ring_and_Field.mult_eq_0_iff)
22.129
22.130 lemma real_inverse_add: "[| x \<noteq> 0; y \<noteq> 0 |]
22.131 ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))"
22.132 -apply (simp add: real_inverse_distrib real_add_mult_distrib real_mult_assoc [symmetric])
22.133 -apply (subst real_mult_assoc)
22.134 -apply (rule real_mult_left_commute [THEN subst])
22.135 -apply (simp add: real_add_commute)
22.136 -done
22.137 +by (simp add: Ring_and_Field.inverse_add mult_assoc)
22.138
22.139 +text{*FIXME: delete or at least combine the next two lemmas*}
22.140 lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
22.141 apply (drule Ring_and_Field.equals_zero_I [THEN sym])
22.142 apply (cut_tac x = y in real_le_square)
22.143 @@ -657,13 +671,8 @@
22.144 apply (auto intro: real_add_order order_less_imp_le)
22.145 done
22.146
22.147 -(*One use in HahnBanach/Aux.thy*)
22.148 -lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
22.149 -apply (rule real_less_or_eq_imp_le)
22.150 -apply (drule order_le_imp_less_or_eq)
22.151 -apply (auto intro: real_mult_less_mono1)
22.152 -done
22.153
22.154 +subsection{*Results About @{term real_of_posnat}: to be Deleted*}
22.155
22.156 lemma real_of_posnat_gt_zero: "0 < real_of_posnat n"
22.157 apply (unfold real_of_posnat_def)
22.158 @@ -753,7 +762,8 @@
22.159 by auto
22.160
22.161 lemma real_mult_less_cancel4: "[| (0::real)<z; z*x<z*y |] ==> x<y"
22.162 -by auto
22.163 + by (force elim: order_less_asym
22.164 + simp add: Ring_and_Field.mult_less_cancel_left)
22.165
22.166 lemma real_of_posnat_less_inv_iff: "0 < u ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse(u))"
22.167 apply safe
22.168 @@ -773,6 +783,13 @@
22.169 apply (simp (no_asm) add: real_add_assoc real_of_posnat_inv_le_iff)
22.170 done
22.171
22.172 +(*Used just below and in HahnBanach/Aux.thy*)
22.173 +lemma real_mult_le_less_mono1: "[| (0::real) \<le> z; x < y |] ==> x*z \<le> y*z"
22.174 +apply (rule real_less_or_eq_imp_le)
22.175 +apply (drule order_le_imp_less_or_eq)
22.176 +apply (auto intro: real_mult_less_mono1)
22.177 +done
22.178 +
22.179 lemma real_mult_add_one_minus_ge_zero: "0 < r ==> 0 <= r*(1 + -inverse(real_of_posnat n))"
22.180 by (drule real_add_one_minus_inv_ge_zero [THEN real_mult_le_less_mono1], auto)
22.181
22.182 @@ -953,10 +970,7 @@
22.183 val real_of_nat_neg_int = thm "real_of_nat_neg_int";
22.184 val real_inverse_gt_0 = thm "real_inverse_gt_0";
22.185 val real_inverse_less_0 = thm "real_inverse_less_0";
22.186 -val real_mult_less_cancel1 = thm "real_mult_less_cancel1";
22.187 -val real_mult_less_cancel2 = thm "real_mult_less_cancel2";
22.188 val real_mult_less_iff1 = thm "real_mult_less_iff1";
22.189 -val real_mult_less_iff2 = thm "real_mult_less_iff2";
22.190 val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1";
22.191 val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2";
22.192 val real_mult_less_mono = thm "real_mult_less_mono";
22.193 @@ -986,8 +1000,6 @@
22.194 val real_of_posnat_inv_le_iff = thm "real_of_posnat_inv_le_iff";
22.195 val real_of_posnat_less_iff = thm "real_of_posnat_less_iff";
22.196 val real_of_posnat_le_iff = thm "real_of_posnat_le_iff";
22.197 -val real_mult_less_cancel3 = thm "real_mult_less_cancel3";
22.198 -val real_mult_less_cancel4 = thm "real_mult_less_cancel4";
22.199 val real_of_posnat_less_inv_iff = thm "real_of_posnat_less_inv_iff";
22.200 val real_of_posnat_inv_eq_iff = thm "real_of_posnat_inv_eq_iff";
22.201 val real_add_one_minus_inv_ge_zero = thm "real_add_one_minus_inv_ge_zero";
22.202 @@ -1012,10 +1024,6 @@
22.203 val real_inverse_1 = thm"real_inverse_1";
22.204 val real_minus_inverse = thm"real_minus_inverse";
22.205 val real_inverse_distrib = thm"real_inverse_distrib";
22.206 -val real_times_divide1_eq = thm"real_times_divide1_eq";
22.207 -val real_times_divide2_eq = thm"real_times_divide2_eq";
22.208 -val real_divide_divide1_eq = thm"real_divide_divide1_eq";
22.209 -val real_divide_divide2_eq = thm"real_divide_divide2_eq";
22.210 val real_minus_divide_eq = thm"real_minus_divide_eq";
22.211 val real_divide_minus_eq = thm"real_divide_minus_eq";
22.212 val real_add_divide_distrib = thm"real_add_divide_distrib";
23.1 --- a/src/HOL/Real/RealPow.thy Wed Dec 10 14:29:44 2003 +0100
23.2 +++ b/src/HOL/Real/RealPow.thy Wed Dec 10 15:59:34 2003 +0100
23.3 @@ -146,9 +146,10 @@
23.4
23.5 lemma realpow_Suc_less [rule_format]:
23.6 "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
23.7 - by (induct_tac "n", auto)
23.8 + by (induct_tac "n", auto simp add: mult_less_cancel_left)
23.9
23.10 -lemma realpow_Suc_le [rule_format]: "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
23.11 +lemma realpow_Suc_le [rule_format]:
23.12 + "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
23.13 apply (induct_tac "n")
23.14 apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq)
23.15 done
23.16 @@ -188,7 +189,7 @@
23.17 by (induct_tac "n", auto)
23.18
23.19 lemma realpow_less_Suc [rule_format]: "(1::real) < r --> r ^ n < r ^ Suc n"
23.20 -by (induct_tac "n", auto)
23.21 +by (induct_tac "n", auto simp add: mult_less_cancel_left)
23.22
23.23 lemma realpow_le_Suc2 [rule_format]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
23.24 by (blast intro!: order_less_imp_le realpow_less_Suc)
24.1 --- a/src/HOL/Real/real_arith.ML Wed Dec 10 14:29:44 2003 +0100
24.2 +++ b/src/HOL/Real/real_arith.ML Wed Dec 10 15:59:34 2003 +0100
24.3 @@ -6,11 +6,17 @@
24.4 Augmentation of real linear arithmetic with rational coefficient handling
24.5 *)
24.6
24.7 +val real_divide_1 = thm"real_divide_1";
24.8 +
24.9 local
24.10
24.11 +val times_divide_eq_left = thm"times_divide_eq_left";
24.12 +val times_divide_eq_right = thm"times_divide_eq_right";
24.13 +
24.14 (* reduce contradictory <= to False *)
24.15 -val simps = [True_implies_equals,inst "w" "number_of ?v" real_add_mult_distrib2,
24.16 - real_divide_1,real_times_divide1_eq,real_times_divide2_eq];
24.17 +val simps = [True_implies_equals,
24.18 + inst "w" "number_of ?v" real_add_mult_distrib2,
24.19 + real_divide_1,times_divide_eq_right,times_divide_eq_left];
24.20
24.21 val simprocs = [real_cancel_numeral_factors_divide];
24.22
25.1 --- a/src/HOL/Ring_and_Field.thy Wed Dec 10 14:29:44 2003 +0100
25.2 +++ b/src/HOL/Ring_and_Field.thy Wed Dec 10 15:59:34 2003 +0100
25.3 @@ -19,7 +19,7 @@
25.4 axclass semiring \<subseteq> zero, one, plus, times
25.5 add_assoc: "(a + b) + c = a + (b + c)"
25.6 add_commute: "a + b = b + a"
25.7 - left_zero [simp]: "0 + a = a"
25.8 + add_0 [simp]: "0 + a = a"
25.9
25.10 mult_assoc: "(a * b) * c = a * (b * c)"
25.11 mult_commute: "a * b = b * a"
25.12 @@ -52,7 +52,7 @@
25.13
25.14 subsection {* Derived Rules for Addition *}
25.15
25.16 -lemma right_zero [simp]: "a + 0 = (a::'a::semiring)"
25.17 +lemma add_0_right [simp]: "a + 0 = (a::'a::semiring)"
25.18 proof -
25.19 have "a + 0 = 0 + a" by (simp only: add_commute)
25.20 also have "... = a" by simp
25.21 @@ -120,6 +120,9 @@
25.22 lemma diff_0_right [simp]: "a - (0::'a::ring) = a"
25.23 by (simp add: diff_minus)
25.24
25.25 +lemma diff_minus_eq_add [simp]: "a - - b = a + (b::'a::ring)"
25.26 +by (simp add: diff_minus)
25.27 +
25.28 lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))"
25.29 proof
25.30 assume "- a = - b"
25.31 @@ -166,33 +169,6 @@
25.32
25.33 theorems mult_ac = mult_assoc mult_commute mult_left_commute
25.34
25.35 -lemma right_inverse [simp]:
25.36 - assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
25.37 -proof -
25.38 - have "a * inverse a = inverse a * a" by (simp add: mult_ac)
25.39 - also have "... = 1" using not0 by simp
25.40 - finally show ?thesis .
25.41 -qed
25.42 -
25.43 -lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
25.44 -proof
25.45 - assume neq: "b \<noteq> 0"
25.46 - {
25.47 - hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
25.48 - also assume "a / b = 1"
25.49 - finally show "a = b" by simp
25.50 - next
25.51 - assume "a = b"
25.52 - with neq show "a / b = 1" by (simp add: divide_inverse)
25.53 - }
25.54 -qed
25.55 -
25.56 -lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
25.57 -by (simp add: divide_inverse)
25.58 -
25.59 -lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
25.60 - by (simp add: divide_inverse)
25.61 -
25.62 lemma mult_left_zero [simp]: "0 * a = (0::'a::ring)"
25.63 proof -
25.64 have "0*a + 0*a = 0*a + 0"
25.65 @@ -690,6 +666,33 @@
25.66
25.67 subsection {* Fields *}
25.68
25.69 +lemma right_inverse [simp]:
25.70 + assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
25.71 +proof -
25.72 + have "a * inverse a = inverse a * a" by (simp add: mult_ac)
25.73 + also have "... = 1" using not0 by simp
25.74 + finally show ?thesis .
25.75 +qed
25.76 +
25.77 +lemma right_inverse_eq: "b \<noteq> 0 ==> (a / b = 1) = (a = (b::'a::field))"
25.78 +proof
25.79 + assume neq: "b \<noteq> 0"
25.80 + {
25.81 + hence "a = (a / b) * b" by (simp add: divide_inverse mult_ac)
25.82 + also assume "a / b = 1"
25.83 + finally show "a = b" by simp
25.84 + next
25.85 + assume "a = b"
25.86 + with neq show "a / b = 1" by (simp add: divide_inverse)
25.87 + }
25.88 +qed
25.89 +
25.90 +lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
25.91 +by (simp add: divide_inverse)
25.92 +
25.93 +lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
25.94 + by (simp add: divide_inverse)
25.95 +
25.96 lemma divide_inverse_zero: "a/b = a * inverse(b::'a::{field,division_by_zero})"
25.97 apply (case_tac "b = 0")
25.98 apply (simp_all add: divide_inverse)
25.99 @@ -904,6 +907,22 @@
25.100 lemma divide_1 [simp]: "a/1 = (a::'a::field)"
25.101 by (simp add: divide_inverse [OF not_sym])
25.102
25.103 +lemma times_divide_eq_right [simp]:
25.104 + "a * (b/c) = (a*b) / (c::'a::{field,division_by_zero})"
25.105 +by (simp add: divide_inverse_zero mult_assoc)
25.106 +
25.107 +lemma times_divide_eq_left [simp]:
25.108 + "(b/c) * a = (b*a) / (c::'a::{field,division_by_zero})"
25.109 +by (simp add: divide_inverse_zero mult_ac)
25.110 +
25.111 +lemma divide_divide_eq_right [simp]:
25.112 + "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
25.113 +by (simp add: divide_inverse_zero mult_ac)
25.114 +
25.115 +lemma divide_divide_eq_left [simp]:
25.116 + "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
25.117 +by (simp add: divide_inverse_zero mult_assoc)
25.118 +
25.119
25.120 subsection {* Ordered Fields *}
25.121
25.122 @@ -1084,11 +1103,180 @@
25.123 by (simp add: divide_inverse_zero zero_le_mult_iff)
25.124
25.125 lemma divide_le_0_iff:
25.126 - "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
25.127 + "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) =
25.128 + (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
25.129 by (simp add: divide_inverse_zero mult_le_0_iff)
25.130
25.131 lemma divide_eq_0_iff [simp]:
25.132 "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
25.133 by (simp add: divide_inverse_zero field_mult_eq_0_iff)
25.134
25.135 +
25.136 +subsection{*Simplification of Inequalities Involving Literal Divisors*}
25.137 +
25.138 +lemma pos_le_divide_eq: "0 < (c::'a::ordered_field) ==> (a \<le> b/c) = (a*c \<le> b)"
25.139 +proof -
25.140 + assume less: "0<c"
25.141 + hence "(a \<le> b/c) = (a*c \<le> (b/c)*c)"
25.142 + by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
25.143 + also have "... = (a*c \<le> b)"
25.144 + by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
25.145 + finally show ?thesis .
25.146 +qed
25.147 +
25.148 +
25.149 +lemma neg_le_divide_eq: "c < (0::'a::ordered_field) ==> (a \<le> b/c) = (b \<le> a*c)"
25.150 +proof -
25.151 + assume less: "c<0"
25.152 + hence "(a \<le> b/c) = ((b/c)*c \<le> a*c)"
25.153 + by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
25.154 + also have "... = (b \<le> a*c)"
25.155 + by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
25.156 + finally show ?thesis .
25.157 +qed
25.158 +
25.159 +lemma le_divide_eq:
25.160 + "(a \<le> b/c) =
25.161 + (if 0 < c then a*c \<le> b
25.162 + else if c < 0 then b \<le> a*c
25.163 + else a \<le> (0::'a::{ordered_field,division_by_zero}))"
25.164 +apply (case_tac "c=0", simp)
25.165 +apply (force simp add: pos_le_divide_eq neg_le_divide_eq linorder_neq_iff)
25.166 +done
25.167 +
25.168 +lemma pos_divide_le_eq: "0 < (c::'a::ordered_field) ==> (b/c \<le> a) = (b \<le> a*c)"
25.169 +proof -
25.170 + assume less: "0<c"
25.171 + hence "(b/c \<le> a) = ((b/c)*c \<le> a*c)"
25.172 + by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
25.173 + also have "... = (b \<le> a*c)"
25.174 + by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
25.175 + finally show ?thesis .
25.176 +qed
25.177 +
25.178 +lemma neg_divide_le_eq: "c < (0::'a::ordered_field) ==> (b/c \<le> a) = (a*c \<le> b)"
25.179 +proof -
25.180 + assume less: "c<0"
25.181 + hence "(b/c \<le> a) = (a*c \<le> (b/c)*c)"
25.182 + by (simp add: mult_le_cancel_right order_less_not_sym [OF less])
25.183 + also have "... = (a*c \<le> b)"
25.184 + by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
25.185 + finally show ?thesis .
25.186 +qed
25.187 +
25.188 +lemma divide_le_eq:
25.189 + "(b/c \<le> a) =
25.190 + (if 0 < c then b \<le> a*c
25.191 + else if c < 0 then a*c \<le> b
25.192 + else 0 \<le> (a::'a::{ordered_field,division_by_zero}))"
25.193 +apply (case_tac "c=0", simp)
25.194 +apply (force simp add: pos_divide_le_eq neg_divide_le_eq linorder_neq_iff)
25.195 +done
25.196 +
25.197 +
25.198 +lemma pos_less_divide_eq:
25.199 + "0 < (c::'a::ordered_field) ==> (a < b/c) = (a*c < b)"
25.200 +proof -
25.201 + assume less: "0<c"
25.202 + hence "(a < b/c) = (a*c < (b/c)*c)"
25.203 + by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
25.204 + also have "... = (a*c < b)"
25.205 + by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
25.206 + finally show ?thesis .
25.207 +qed
25.208 +
25.209 +lemma neg_less_divide_eq:
25.210 + "c < (0::'a::ordered_field) ==> (a < b/c) = (b < a*c)"
25.211 +proof -
25.212 + assume less: "c<0"
25.213 + hence "(a < b/c) = ((b/c)*c < a*c)"
25.214 + by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
25.215 + also have "... = (b < a*c)"
25.216 + by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
25.217 + finally show ?thesis .
25.218 +qed
25.219 +
25.220 +lemma less_divide_eq:
25.221 + "(a < b/c) =
25.222 + (if 0 < c then a*c < b
25.223 + else if c < 0 then b < a*c
25.224 + else a < (0::'a::{ordered_field,division_by_zero}))"
25.225 +apply (case_tac "c=0", simp)
25.226 +apply (force simp add: pos_less_divide_eq neg_less_divide_eq linorder_neq_iff)
25.227 +done
25.228 +
25.229 +lemma pos_divide_less_eq:
25.230 + "0 < (c::'a::ordered_field) ==> (b/c < a) = (b < a*c)"
25.231 +proof -
25.232 + assume less: "0<c"
25.233 + hence "(b/c < a) = ((b/c)*c < a*c)"
25.234 + by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
25.235 + also have "... = (b < a*c)"
25.236 + by (simp add: order_less_imp_not_eq2 [OF less] divide_inverse mult_assoc)
25.237 + finally show ?thesis .
25.238 +qed
25.239 +
25.240 +lemma neg_divide_less_eq:
25.241 + "c < (0::'a::ordered_field) ==> (b/c < a) = (a*c < b)"
25.242 +proof -
25.243 + assume less: "c<0"
25.244 + hence "(b/c < a) = (a*c < (b/c)*c)"
25.245 + by (simp add: mult_less_cancel_right order_less_not_sym [OF less])
25.246 + also have "... = (a*c < b)"
25.247 + by (simp add: order_less_imp_not_eq [OF less] divide_inverse mult_assoc)
25.248 + finally show ?thesis .
25.249 +qed
25.250 +
25.251 +lemma divide_less_eq:
25.252 + "(b/c < a) =
25.253 + (if 0 < c then b < a*c
25.254 + else if c < 0 then a*c < b
25.255 + else 0 < (a::'a::{ordered_field,division_by_zero}))"
25.256 +apply (case_tac "c=0", simp)
25.257 +apply (force simp add: pos_divide_less_eq neg_divide_less_eq linorder_neq_iff)
25.258 +done
25.259 +
25.260 +lemma nonzero_eq_divide_eq: "c\<noteq>0 ==> ((a::'a::field) = b/c) = (a*c = b)"
25.261 +proof -
25.262 + assume [simp]: "c\<noteq>0"
25.263 + have "(a = b/c) = (a*c = (b/c)*c)"
25.264 + by (simp add: field_mult_cancel_right)
25.265 + also have "... = (a*c = b)"
25.266 + by (simp add: divide_inverse mult_assoc)
25.267 + finally show ?thesis .
25.268 +qed
25.269 +
25.270 +lemma eq_divide_eq:
25.271 + "((a::'a::{field,division_by_zero}) = b/c) = (if c\<noteq>0 then a*c = b else a=0)"
25.272 +by (simp add: nonzero_eq_divide_eq)
25.273 +
25.274 +lemma nonzero_divide_eq_eq: "c\<noteq>0 ==> (b/c = (a::'a::field)) = (b = a*c)"
25.275 +proof -
25.276 + assume [simp]: "c\<noteq>0"
25.277 + have "(b/c = a) = ((b/c)*c = a*c)"
25.278 + by (simp add: field_mult_cancel_right)
25.279 + also have "... = (b = a*c)"
25.280 + by (simp add: divide_inverse mult_assoc)
25.281 + finally show ?thesis .
25.282 +qed
25.283 +
25.284 +lemma divide_eq_eq:
25.285 + "(b/c = (a::'a::{field,division_by_zero})) = (if c\<noteq>0 then b = a*c else a=0)"
25.286 +by (force simp add: nonzero_divide_eq_eq)
25.287 +
25.288 +subsection{*Cancellation Laws for Division*}
25.289 +
25.290 +lemma divide_cancel_right [simp]:
25.291 + "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
25.292 +apply (case_tac "c=0", simp)
25.293 +apply (simp add: divide_inverse_zero field_mult_cancel_right)
25.294 +done
25.295 +
25.296 +lemma divide_cancel_left [simp]:
25.297 + "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
25.298 +apply (case_tac "c=0", simp)
25.299 +apply (simp add: divide_inverse_zero field_mult_cancel_left)
25.300 +done
25.301 +
25.302 +
25.303 end