# HG changeset patch
# User wenzelm
# Date 1205775420 -3600
# Node ID 03def556e26e81686f29a32c989c560e4629462c
# Parent  2f387f5c0f52a531c97fa788325557c3d57375e5
removed duplicate lemmas;

diff -r 2f387f5c0f52 -r 03def556e26e src/HOL/Auth/KerberosV.thy
--- a/src/HOL/Auth/KerberosV.thy	Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/Auth/KerberosV.thy	Mon Mar 17 18:37:00 2008 +0100
@@ -897,24 +897,6 @@
 apply (blast dest: unique_servKeys Says_Tgs_message_form)
 done
 
-lemma AKcryptSK_not_AKcryptSK:
-     "\<lbrakk> AKcryptSK authK servK evs;  evs \<in> kerbV \<rbrakk>
-      \<Longrightarrow> \<not> AKcryptSK servK K evs"
-apply (erule rev_mp)
-apply (erule kerbV.induct)
-apply (frule_tac [7] Says_ticket_parts)
-apply (frule_tac [5] Says_ticket_parts, simp_all, safe)
-txt{*K4 splits into subcases*}
-apply simp_all
-prefer 4 apply (blast dest!: authK_not_AKcryptSK)
-txt{*servK is fresh and so could not have been used, by
-   @{text new_keys_not_used}*}
- prefer 2 
- apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
-txt{*Others by freshness*}
-apply (blast+)
-done
-
 text{*The only session keys that can be found with the help of session keys are
   those sent by Tgs in step K4.  *}
 
diff -r 2f387f5c0f52 -r 03def556e26e src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/Divides.thy	Mon Mar 17 18:37:00 2008 +0100
@@ -316,7 +316,7 @@
   then show ?thesis using divmod_div_mod by simp
 qed
 
-text {* The ''recursion´´ equations for @{const div} and @{const mod} *}
+text {* The ''recursion'' equations for @{const div} and @{const mod} *}
 
 lemma div_less [simp]:
   fixes m n :: nat
@@ -704,61 +704,6 @@
   by (cases "n = 0") auto
 
 
-(* Antimonotonicity of div in second argument *)
-lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
-apply (subgoal_tac "0<n")
- prefer 2 apply simp
-apply (induct_tac k rule: nat_less_induct)
-apply (rename_tac "k")
-apply (case_tac "k<n", simp)
-apply (subgoal_tac "~ (k<m) ")
- prefer 2 apply simp
-apply (simp add: div_geq)
-apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
- prefer 2
- apply (blast intro: div_le_mono diff_le_mono2)
-apply (rule le_trans, simp)
-apply (simp)
-done
-
-lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
-apply (case_tac "n=0", simp)
-apply (subgoal_tac "m div n \<le> m div 1", simp)
-apply (rule div_le_mono2)
-apply (simp_all (no_asm_simp))
-done
-
-(* Similar for "less than" *)
-lemma div_less_dividend [rule_format]:
-     "!!n::nat. 1<n ==> 0 < m --> m div n < m"
-apply (induct_tac m rule: nat_less_induct)
-apply (rename_tac "m")
-apply (case_tac "m<n", simp)
-apply (subgoal_tac "0<n")
- prefer 2 apply simp
-apply (simp add: div_geq)
-apply (case_tac "n<m")
- apply (subgoal_tac "(m-n) div n < (m-n) ")
-  apply (rule impI less_trans_Suc)+
-apply assumption
-  apply (simp_all)
-done
-
-declare div_less_dividend [simp]
-
-text{*A fact for the mutilated chess board*}
-lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
-apply (case_tac "n=0", simp)
-apply (induct "m" rule: nat_less_induct)
-apply (case_tac "Suc (na) <n")
-(* case Suc(na) < n *)
-apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
-(* case n \<le> Suc(na) *)
-apply (simp add: linorder_not_less le_Suc_eq mod_geq)
-apply (auto simp add: Suc_diff_le le_mod_geq)
-done
-
-
 subsubsection{*The Divides Relation*}
 
 lemma dvdI [intro?]: "n = m * k ==> m dvd n"
diff -r 2f387f5c0f52 -r 03def556e26e src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/Hoare/hoare_tac.ML	Mon Mar 17 18:37:00 2008 +0100
@@ -86,15 +86,10 @@
 (** input does not suffer any unexpected transformation                     **)
 (*****************************************************************************)
 
-Goal "-(Collect b) = {x. ~(b x)}";
-by (Fast_tac 1);
-qed "Compl_Collect";
-
-
 (**Simp_tacs**)
 
 val before_set2pred_simp_tac =
-  (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect]));
+  (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]));
 
 val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
 
diff -r 2f387f5c0f52 -r 03def556e26e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/Int.thy	Mon Mar 17 18:37:00 2008 +0100
@@ -1911,10 +1911,6 @@
 lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
 lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
 
-lemmas int_distrib =
-  zadd_zmult_distrib zadd_zmult_distrib2
-  zdiff_zmult_distrib zdiff_zmult_distrib2
-
 lemmas zmult_1 = mult_1_left [of "z::int", standard]
 lemmas zmult_1_right = mult_1_right [of "z::int", standard]
 
diff -r 2f387f5c0f52 -r 03def556e26e src/HOL/Library/Heap.thy
--- a/src/HOL/Library/Heap.thy	Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/Library/Heap.thy	Mon Mar 17 18:37:00 2008 +0100
@@ -414,12 +414,12 @@
 lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)"
   by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def  new_ref_def)
 
-(*not actually true ???
+text {*not actually true ???*}
 lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)"
 apply (case_tac a)
 apply (simp add: Let_def upd_def)
 apply auto
-done*)
+oops
 
 lemma length_new_ref[simp]: 
   "length a (snd (ref v h)) = length a h"
@@ -429,10 +429,6 @@
   "get_array a (snd (ref v h)) = get_array a h"
   by (simp add: new_ref_def ref_def set_ref_def get_array_def Let_def)
 
-lemma get_array_new_ref [simp]:
-  "get_array a (snd (ref v h)) ! i = get_array a h ! i"
-  by (simp add: get_array_def new_ref_def ref_def set_ref_def Let_def)
-
 lemma ref_present_upd [simp]: 
   "ref_present r (upd a i v h) = ref_present r h"
   by (simp add: upd_def ref_present_def set_array_def get_array_def)
diff -r 2f387f5c0f52 -r 03def556e26e src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/List.thy	Mon Mar 17 18:37:00 2008 +0100
@@ -1220,10 +1220,6 @@
 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
 
-lemma list_update_overwrite [simp]:
-"i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
-by (induct xs arbitrary: i) (auto split: nat.split)
-
 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
 by (induct xs arbitrary: i) (simp_all split:nat.splits)
 
diff -r 2f387f5c0f52 -r 03def556e26e src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/Matrix/SparseMatrix.thy	Mon Mar 17 18:37:00 2008 +0100
@@ -143,14 +143,6 @@
   apply (simp add: sorted_spvec.simps split:list.split_asm)
   done
 
-lemma sorted_spvec_minus_spvec:
-  "sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)"
-  apply (induct v)
-  apply (simp)
-  apply (frule sorted_spvec_cons1, simp)
-  apply (simp add: sorted_spvec.simps split:list.split_asm)
-  done
-
 lemma sorted_spvec_abs_spvec:
   "sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)"
   apply (induct v)
diff -r 2f387f5c0f52 -r 03def556e26e src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/Nat.thy	Mon Mar 17 18:37:00 2008 +0100
@@ -855,9 +855,6 @@
 
 subsubsection {* More results about difference *}
 
-lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
-by (induct m) simp_all
-
 text {* Addition is the inverse of subtraction:
   if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
 lemma add_diff_inverse: "~  m < n ==> n + (m - n) = (m::nat)"
diff -r 2f387f5c0f52 -r 03def556e26e src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/Orderings.thy	Mon Mar 17 18:37:00 2008 +0100
@@ -39,9 +39,6 @@
 lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
 unfolding less_le by blast
 
-lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
-by (erule contrapos_pn, erule subst, rule less_irrefl)
-
 
 text {* Useful for simplification, but too risky to include by default. *}