# HG changeset patch
# User nipkow
# Date 1105700427 -3600
# Node ID 71c0f98e31f15e8258777a083898ade81c2dd8c3
# Parent  dfc7d2a824d654ca28bbe4bc1f03454814164489
made diff_less a simp rule

diff -r dfc7d2a824d6 -r 71c0f98e31f1 src/HOL/Divides.thy
--- 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)"
diff -r dfc7d2a824d6 -r 71c0f98e31f1 src/HOL/Fun.thy
--- 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)
 
diff -r dfc7d2a824d6 -r 71c0f98e31f1 src/HOL/Integ/NatBin.thy
--- 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";
diff -r dfc7d2a824d6 -r 71c0f98e31f1 src/HOL/Isar_examples/Fibonacci.thy
--- 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)"
diff -r dfc7d2a824d6 -r 71c0f98e31f1 src/HOL/List.thy
--- 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 *}
 
diff -r dfc7d2a824d6 -r 71c0f98e31f1 src/HOL/NatArith.thy
--- 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
 
 
diff -r dfc7d2a824d6 -r 71c0f98e31f1 src/HOL/NumberTheory/Fib.thy
--- 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 *}