made diff_less a simp rule
authornipkow
Fri Jan 14 12:00:27 2005 +0100 (2005-01-14)
changeset 1543971c0f98e31f1
parent 15438 dfc7d2a824d6
child 15440 d0cd75f7a365
made diff_less a simp rule
src/HOL/Divides.thy
src/HOL/Fun.thy
src/HOL/Integ/NatBin.thy
src/HOL/Isar_examples/Fibonacci.thy
src/HOL/List.thy
src/HOL/NatArith.thy
src/HOL/NumberTheory/Fib.thy
     1.1 --- a/src/HOL/Divides.thy	Thu Jan 13 14:56:37 2005 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Jan 14 12:00:27 2005 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4  lemma mod_geq: "~ m < (n::nat) ==> m mod n = (m-n) mod n"
     1.5  apply (case_tac "n=0", simp) 
     1.6  apply (rule mod_eq [THEN wf_less_trans])
     1.7 -apply (simp add: diff_less cut_apply less_eq)
     1.8 +apply (simp add: cut_apply less_eq)
     1.9  done
    1.10  
    1.11  (*Avoids the ugly ~m<n above*)
    1.12 @@ -119,7 +119,7 @@
    1.13  apply (case_tac "k=0", simp)
    1.14  apply (induct "m" rule: nat_less_induct)
    1.15  apply (subst mod_if, simp)
    1.16 -apply (simp add: mod_geq diff_less diff_mult_distrib)
    1.17 +apply (simp add: mod_geq diff_mult_distrib)
    1.18  done
    1.19  
    1.20  lemma mod_mult_distrib2: "(k::nat) * (m mod n) = (k*m) mod (k*n)"
    1.21 @@ -144,7 +144,7 @@
    1.22  
    1.23  lemma div_geq: "[| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)"
    1.24  apply (rule div_eq [THEN wf_less_trans])
    1.25 -apply (simp add: diff_less cut_apply less_eq)
    1.26 +apply (simp add: cut_apply less_eq)
    1.27  done
    1.28  
    1.29  (*Avoids the ugly ~m<n above*)
    1.30 @@ -160,7 +160,7 @@
    1.31  apply (case_tac "n=0", simp)
    1.32  apply (induct "m" rule: nat_less_induct)
    1.33  apply (subst mod_if)
    1.34 -apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse diff_less)
    1.35 +apply (simp_all (no_asm_simp) add: add_assoc div_geq add_diff_inverse)
    1.36  done
    1.37  
    1.38  lemma mod_div_equality2: "n * (m div n) + m mod n = (m::nat)"
    1.39 @@ -222,7 +222,12 @@
    1.40  apply (induct "m" rule: nat_less_induct)
    1.41  apply (case_tac "na<n", simp) 
    1.42  txt{*case @{term "n \<le> na"}*}
    1.43 -apply (simp add: mod_geq diff_less)
    1.44 +apply (simp add: mod_geq)
    1.45 +done
    1.46 +
    1.47 +lemma mod_le_divisor[simp]: "0 < n \<Longrightarrow> m mod n \<le> (n::nat)"
    1.48 +apply(drule mod_less_divisor[where m = m])
    1.49 +apply simp
    1.50  done
    1.51  
    1.52  lemma div_mult_self_is_m [simp]: "0<n ==> (m*n) div n = (m::nat)"
    1.53 @@ -427,7 +432,7 @@
    1.54  (* 2.1  case m<k *)
    1.55  apply simp
    1.56  (* 2.2  case m>=k *)
    1.57 -apply (simp add: div_geq diff_less diff_le_mono)
    1.58 +apply (simp add: div_geq diff_le_mono)
    1.59  done
    1.60  
    1.61  (* Antimonotonicity of div in second argument *)
    1.62 @@ -444,7 +449,7 @@
    1.63   prefer 2
    1.64   apply (blast intro: div_le_mono diff_le_mono2)
    1.65  apply (rule le_trans, simp)
    1.66 -apply (simp add: diff_less)
    1.67 +apply (simp)
    1.68  done
    1.69  
    1.70  lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
    1.71 @@ -467,7 +472,7 @@
    1.72   apply (subgoal_tac "(m-n) div n < (m-n) ")
    1.73    apply (rule impI less_trans_Suc)+
    1.74  apply assumption
    1.75 -  apply (simp_all add: diff_less)
    1.76 +  apply (simp_all)
    1.77  done
    1.78  
    1.79  text{*A fact for the mutilated chess board*}
    1.80 @@ -479,7 +484,7 @@
    1.81  apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
    1.82  (* case n \<le> Suc(na) *)
    1.83  apply (simp add: not_less_iff_le le_Suc_eq mod_geq)
    1.84 -apply (auto simp add: Suc_diff_le diff_less le_mod_geq)
    1.85 +apply (auto simp add: Suc_diff_le le_mod_geq)
    1.86  done
    1.87  
    1.88  lemma nat_mod_div_trivial [simp]: "m mod n div n = (0 :: nat)"
     2.1 --- a/src/HOL/Fun.thy	Thu Jan 13 14:56:37 2005 +0100
     2.2 +++ b/src/HOL/Fun.thy	Fri Jan 14 12:00:27 2005 +0100
     2.3 @@ -163,6 +163,12 @@
     2.4  apply blast
     2.5  done
     2.6  
     2.7 +lemma inj_on_image_iff: "\<lbrakk> ALL x:A. ALL y:A. (g(f x) = g(f y)) = (g x = g y);
     2.8 +  inj_on f A \<rbrakk> \<Longrightarrow> inj_on g (f ` A) = inj_on g A"
     2.9 +apply(unfold inj_on_def)
    2.10 +apply blast
    2.11 +done
    2.12 +
    2.13  lemma inj_on_contraD: "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)"
    2.14  by (unfold inj_on_def, blast)
    2.15  
     3.1 --- a/src/HOL/Integ/NatBin.thy	Thu Jan 13 14:56:37 2005 +0100
     3.2 +++ b/src/HOL/Integ/NatBin.thy	Fri Jan 14 12:00:27 2005 +0100
     3.3 @@ -388,11 +388,6 @@
     3.4  apply (simp_all add: numerals)
     3.5  done
     3.6  
     3.7 -lemma diff_less': "[| 0<n; 0<m |] ==> m - n < (m::nat)"
     3.8 -by (simp add: diff_less numerals)
     3.9 -
    3.10 -declare diff_less' [of "number_of v", standard, simp]
    3.11 -
    3.12  
    3.13  subsection{*Comparisons involving (0::nat) *}
    3.14  
    3.15 @@ -764,7 +759,6 @@
    3.16  val add_eq_if = thm"add_eq_if";
    3.17  val mult_eq_if = thm"mult_eq_if";
    3.18  val power_eq_if = thm"power_eq_if";
    3.19 -val diff_less' = thm"diff_less'";
    3.20  val eq_number_of_0 = thm"eq_number_of_0";
    3.21  val eq_0_number_of = thm"eq_0_number_of";
    3.22  val less_0_number_of = thm"less_0_number_of";
     4.1 --- a/src/HOL/Isar_examples/Fibonacci.thy	Thu Jan 13 14:56:37 2005 +0100
     4.2 +++ b/src/HOL/Isar_examples/Fibonacci.thy	Fri Jan 14 12:00:27 2005 +0100
     4.3 @@ -142,7 +142,7 @@
     4.4  	assume "n < m" thus ?thesis by simp
     4.5        next
     4.6  	assume not_lt: "~ n < m" hence le: "m <= n" by simp
     4.7 -	have "n - m < n" by (simp! add: diff_less)
     4.8 +	have "n - m < n" by (simp!)
     4.9  	with hyp have "gcd (fib m, fib ((n - m) mod m))
    4.10  	  = gcd (fib m, fib (n - m))" by simp
    4.11  	also from le have "... = gcd (fib m, fib n)"
     5.1 --- a/src/HOL/List.thy	Thu Jan 13 14:56:37 2005 +0100
     5.2 +++ b/src/HOL/List.thy	Fri Jan 14 12:00:27 2005 +0100
     5.3 @@ -28,6 +28,7 @@
     5.4    set :: "'a list => 'a set"
     5.5    list_all:: "('a => bool) => ('a list => bool)"
     5.6    list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool"
     5.7 +  list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
     5.8    map :: "('a=>'b) => ('a list => 'b list)"
     5.9    mem :: "'a => 'a list => bool"    (infixl 55)
    5.10    nth :: "'a list => nat => 'a"    (infixl "!" 100)
    5.11 @@ -130,6 +131,10 @@
    5.12    list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)"
    5.13  
    5.14  primrec
    5.15 +"list_ex P [] = False"
    5.16 +"list_ex P (x#xs) = (P x \<or> list_ex P xs)"
    5.17 +
    5.18 +primrec
    5.19    "map f [] = []"
    5.20    "map f (x#xs) = f(x)#map f xs"
    5.21  
    5.22 @@ -572,6 +577,9 @@
    5.23  apply (case_tac ys, simp, force)
    5.24  done
    5.25  
    5.26 +lemma inj_on_rev[iff]: "inj_on rev A"
    5.27 +by(simp add:inj_on_def)
    5.28 +
    5.29  lemma rev_induct [case_names Nil snoc]:
    5.30    "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
    5.31  apply(subst rev_rev_ident[symmetric])
    5.32 @@ -650,18 +658,20 @@
    5.33  by (induct xs) (auto simp add: card_insert_if)
    5.34  
    5.35  
    5.36 -subsubsection {* @{text mem} *}
    5.37 +subsubsection {* @{text mem}, @{text list_all} and @{text list_ex} *}
    5.38  
    5.39  text{* Only use @{text mem} for generating executable code.  Otherwise
    5.40 -use @{prop"x : set xs"} instead --- it is much easier to reason
    5.41 -about. *}
    5.42 +use @{prop"x : set xs"} instead --- it is much easier to reason about.
    5.43 +The same is true for @{text list_all} and @{text list_ex}: write
    5.44 +@{text"\<forall>x\<in>set xs"} and @{text"\<exists>x\<in>set xs"} instead because the HOL
    5.45 +quantifiers are aleady known to the automatic provers. For the purpose
    5.46 +of generating executable code use the theorems @{text set_mem_eq},
    5.47 +@{text list_all_conv} and @{text list_ex_iff} to get rid off or
    5.48 +introduce the combinators. *}
    5.49  
    5.50  lemma set_mem_eq: "(x mem xs) = (x : set xs)"
    5.51  by (induct xs) auto
    5.52  
    5.53 -
    5.54 -subsubsection {* @{text list_all} *}
    5.55 -
    5.56  lemma list_all_conv: "list_all P xs = (\<forall>x \<in> set xs. P x)"
    5.57  by (induct xs) auto
    5.58  
    5.59 @@ -672,6 +682,8 @@
    5.60  lemma list_all_rev [simp]: "list_all P (rev xs) = list_all P xs"
    5.61  by (simp add: list_all_conv)
    5.62  
    5.63 +lemma list_ex_iff: "list_ex P xs = (\<exists>x \<in> set xs. P x)"
    5.64 +by (induct xs) simp_all
    5.65  
    5.66  
    5.67  subsubsection {* @{text filter} *}
    5.68 @@ -1725,6 +1737,16 @@
    5.69  lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
    5.70  by (induct n) (simp_all add:rotate_def)
    5.71  
    5.72 +lemma rotate_rev:
    5.73 +  "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
    5.74 +apply(simp add:rotate_drop_take rev_drop rev_take)
    5.75 +apply(cases "length xs = 0")
    5.76 + apply simp
    5.77 +apply(cases "n mod length xs = 0")
    5.78 + apply simp
    5.79 +apply(simp add:rotate_drop_take rev_drop rev_take)
    5.80 +done
    5.81 +
    5.82  
    5.83  subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
    5.84  
     6.1 --- a/src/HOL/NatArith.thy	Thu Jan 13 14:56:37 2005 +0100
     6.2 +++ b/src/HOL/NatArith.thy	Fri Jan 14 12:00:27 2005 +0100
     6.3 @@ -62,7 +62,7 @@
     6.4  
     6.5  (*Replaces the previous diff_less and le_diff_less, which had the stronger
     6.6    second premise n\<le>m*)
     6.7 -lemma diff_less: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
     6.8 +lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
     6.9  by arith
    6.10  
    6.11  
     7.1 --- a/src/HOL/NumberTheory/Fib.thy	Thu Jan 13 14:56:37 2005 +0100
     7.2 +++ b/src/HOL/NumberTheory/Fib.thy	Fri Jan 14 12:00:27 2005 +0100
     7.3 @@ -108,7 +108,7 @@
     7.4  lemma gcd_fib_mod: "0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
     7.5    apply (induct n rule: nat_less_induct)
     7.6    apply (subst mod_if)
     7.7 -  apply (simp add: gcd_fib_diff mod_geq not_less_iff_le diff_less)
     7.8 +  apply (simp add: gcd_fib_diff mod_geq not_less_iff_le)
     7.9    done
    7.10  
    7.11  lemma fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)"  -- {* Law 6.111 *}