--- a/src/HOL/Divides.thy Thu Jan 13 14:56:37 2005 +0100
+++ b/src/HOL/Divides.thy Fri Jan 14 12:00:27 2005 +0100
@@ -77,7 +77,7 @@
lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
apply (case_tac "n=0", simp)
apply (rule mod_eq [THEN wf_less_trans])
-apply (simp add: diff_less cut_apply less_eq)
+apply (simp add: cut_apply less_eq)
done
(*Avoids the ugly ~m<n above*)
@@ -119,7 +119,7 @@
apply (case_tac "k=0", simp)
apply (induct "m" rule: nat_less_induct)
apply (subst mod_if, simp)
-apply (simp add: mod_geq diff_less diff_mult_distrib)
+apply (simp add: mod_geq diff_mult_distrib)
done
lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
@@ -144,7 +144,7 @@
lemma div_geq: "[| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)"
apply (rule div_eq [THEN wf_less_trans])
-apply (simp add: diff_less cut_apply less_eq)
+apply (simp add: cut_apply less_eq)
done
(*Avoids the ugly ~m<n above*)
@@ -160,7 +160,7 @@
apply (case_tac "n=0", simp)
apply (induct "m" rule: nat_less_induct)
apply (subst mod_if)
-apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse diff_less)
+apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse)
done
lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
@@ -222,7 +222,12 @@
apply (induct "m" rule: nat_less_induct)
apply (case_tac "na<n", simp)
txt{*case @{term "n \<le> na"}*}
-apply (simp add: mod_geq diff_less)
+apply (simp add: mod_geq)
+done
+
+lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
+apply(drule mod_less_divisor[where m = m])
+apply simp
done
lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
@@ -427,7 +432,7 @@
(* 2.1 case m<k *)
apply simp
(* 2.2 case m>=k *)
-apply (simp add: div_geq diff_less diff_le_mono)
+apply (simp add: div_geq diff_le_mono)
done
(* Antimonotonicity of div in second argument *)
@@ -444,7 +449,7 @@
prefer 2
apply (blast intro: div_le_mono diff_le_mono2)
apply (rule le_trans, simp)
-apply (simp add: diff_less)
+apply (simp)
done
lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
@@ -467,7 +472,7 @@
apply (subgoal_tac "(m-n) div n < (m-n) ")
apply (rule impI less_trans_Suc)+
apply assumption
- apply (simp_all add: diff_less)
+ apply (simp_all)
done
text{*A fact for the mutilated chess board*}
@@ -479,7 +484,7 @@
apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
(* case n \<le> Suc(na) *)
apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
-apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
+apply (auto simp add: Suc_diff_le le_mod_geq)
done
lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
--- a/src/HOL/Fun.thy Thu Jan 13 14:56:37 2005 +0100
+++ b/src/HOL/Fun.thy Fri Jan 14 12:00:27 2005 +0100
@@ -163,6 +163,12 @@
apply blast
done
+lemma inj_on_image_iff: "\<lbrakk> ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y);
+ inj_on f A \<rbrakk> \<Longrightarrow> inj_on g (f ` A) = inj_on g A"
+apply(unfold inj_on_def)
+apply blast
+done
+
lemma inj_on_contraD: "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"
by (unfold inj_on_def, blast)
--- a/src/HOL/Integ/NatBin.thy Thu Jan 13 14:56:37 2005 +0100
+++ b/src/HOL/Integ/NatBin.thy Fri Jan 14 12:00:27 2005 +0100
@@ -388,11 +388,6 @@
apply (simp_all add: numerals)
done
-lemma diff_less': "[| 0<n; 0<m |] ==> m - n < (m::nat)"
-by (simp add: diff_less numerals)
-
-declare diff_less' [of "number_of v", standard, simp]
-
subsection{*Comparisons involving (0::nat) *}
@@ -764,7 +759,6 @@
val add_eq_if = thm"add_eq_if";
val mult_eq_if = thm"mult_eq_if";
val power_eq_if = thm"power_eq_if";
-val diff_less' = thm"diff_less'";
val eq_number_of_0 = thm"eq_number_of_0";
val eq_0_number_of = thm"eq_0_number_of";
val less_0_number_of = thm"less_0_number_of";
--- a/src/HOL/Isar_examples/Fibonacci.thy Thu Jan 13 14:56:37 2005 +0100
+++ b/src/HOL/Isar_examples/Fibonacci.thy Fri Jan 14 12:00:27 2005 +0100
@@ -142,7 +142,7 @@
assume "n < m" thus ?thesis by simp
next
assume not_lt: "~ n < m" hence le: "m <= n" by simp
- have "n - m < n" by (simp! add: diff_less)
+ have "n - m < n" by (simp!)
with hyp have "gcd (fib m, fib ((n - m) mod m))
= gcd (fib m, fib (n - m))" by simp
also from le have "... = gcd (fib m, fib n)"
--- a/src/HOL/List.thy Thu Jan 13 14:56:37 2005 +0100
+++ b/src/HOL/List.thy Fri Jan 14 12:00:27 2005 +0100
@@ -28,6 +28,7 @@
set :: "'a list => 'a set"
list_all:: "('a => bool) => ('a list => bool)"
list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool"
+ list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
map :: "('a=>'b) => ('a list => 'b list)"
mem :: "'a => 'a list => bool" (infixl 55)
nth :: "'a list => nat => 'a" (infixl "!" 100)
@@ -130,6 +131,10 @@
list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)"
primrec
+"list_ex P [] = False"
+"list_ex P (x#xs) = (P x \<or> list_ex P xs)"
+
+primrec
"map f [] = []"
"map f (x#xs) = f(x)#map f xs"
@@ -572,6 +577,9 @@
apply (case_tac ys, simp, force)
done
+lemma inj_on_rev[iff]: "inj_on rev A"
+by(simp add:inj_on_def)
+
lemma rev_induct [case_names Nil snoc]:
"[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
apply(subst rev_rev_ident[symmetric])
@@ -650,18 +658,20 @@
by (induct xs) (auto simp add: card_insert_if)
-subsubsection {* @{text mem} *}
+subsubsection {* @{text mem}, @{text list_all} and @{text list_ex} *}
text{* Only use @{text mem} for generating executable code. Otherwise
-use @{prop"x : set xs"} instead --- it is much easier to reason
-about. *}
+use @{prop"x : set xs"} instead --- it is much easier to reason about.
+The same is true for @{text list_all} and @{text list_ex}: write
+@{text"\<forall>x\<in>set xs"} and @{text"\<exists>x\<in>set xs"} instead because the HOL
+quantifiers are aleady known to the automatic provers. For the purpose
+of generating executable code use the theorems @{text set_mem_eq},
+@{text list_all_conv} and @{text list_ex_iff} to get rid off or
+introduce the combinators. *}
lemma set_mem_eq: "(x mem xs) = (x : set xs)"
by (induct xs) auto
-
-subsubsection {* @{text list_all} *}
-
lemma list_all_conv: "list_all P xs = (\<forall>x \<in> set xs. P x)"
by (induct xs) auto
@@ -672,6 +682,8 @@
lemma list_all_rev [simp]: "list_all P (rev xs) = list_all P xs"
by (simp add: list_all_conv)
+lemma list_ex_iff: "list_ex P xs = (\<exists>x \<in> set xs. P x)"
+by (induct xs) simp_all
subsubsection {* @{text filter} *}
@@ -1725,6 +1737,16 @@
lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
by (induct n) (simp_all add:rotate_def)
+lemma rotate_rev:
+ "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
+apply(simp add:rotate_drop_take rev_drop rev_take)
+apply(cases "length xs = 0")
+ apply simp
+apply(cases "n mod length xs = 0")
+ apply simp
+apply(simp add:rotate_drop_take rev_drop rev_take)
+done
+
subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
--- a/src/HOL/NatArith.thy Thu Jan 13 14:56:37 2005 +0100
+++ b/src/HOL/NatArith.thy Fri Jan 14 12:00:27 2005 +0100
@@ -62,7 +62,7 @@
(*Replaces the previous diff_less and le_diff_less, which had the stronger
second premise n\<le>m*)
-lemma diff_less: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
+lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
by arith
--- a/src/HOL/NumberTheory/Fib.thy Thu Jan 13 14:56:37 2005 +0100
+++ b/src/HOL/NumberTheory/Fib.thy Fri Jan 14 12:00:27 2005 +0100
@@ -108,7 +108,7 @@
lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
apply (induct n rule: nat_less_induct)
apply (subst mod_if)
- apply (simp add: gcd_fib_diff mod_geq not_less_iff_le diff_less)
+ apply (simp add: gcd_fib_diff mod_geq not_less_iff_le)
done
lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" -- {* Law 6.111 *}