removed duplicate lemmas;
authorwenzelm
Mon Mar 17 18:37:00 2008 +0100 (2008-03-17)
changeset 2630003def556e26e
parent 26299 2f387f5c0f52
child 26301 28193aedc718
removed duplicate lemmas;
src/HOL/Auth/KerberosV.thy
src/HOL/Divides.thy
src/HOL/Hoare/hoare_tac.ML
src/HOL/Int.thy
src/HOL/Library/Heap.thy
src/HOL/List.thy
src/HOL/Matrix/SparseMatrix.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Auth/KerberosV.thy	Mon Mar 17 18:36:04 2008 +0100
     1.2 +++ b/src/HOL/Auth/KerberosV.thy	Mon Mar 17 18:37:00 2008 +0100
     1.3 @@ -897,24 +897,6 @@
     1.4  apply (blast dest: unique_servKeys Says_Tgs_message_form)
     1.5  done
     1.6  
     1.7 -lemma AKcryptSK_not_AKcryptSK:
     1.8 -     "\<lbrakk> AKcryptSK authK servK evs;  evs \<in> kerbV \<rbrakk>
     1.9 -      \<Longrightarrow> \<not> AKcryptSK servK K evs"
    1.10 -apply (erule rev_mp)
    1.11 -apply (erule kerbV.induct)
    1.12 -apply (frule_tac [7] Says_ticket_parts)
    1.13 -apply (frule_tac [5] Says_ticket_parts, simp_all, safe)
    1.14 -txt{*K4 splits into subcases*}
    1.15 -apply simp_all
    1.16 -prefer 4 apply (blast dest!: authK_not_AKcryptSK)
    1.17 -txt{*servK is fresh and so could not have been used, by
    1.18 -   @{text new_keys_not_used}*}
    1.19 - prefer 2 
    1.20 - apply (force dest!: Crypt_imp_invKey_keysFor simp add: AKcryptSK_def)
    1.21 -txt{*Others by freshness*}
    1.22 -apply (blast+)
    1.23 -done
    1.24 -
    1.25  text{*The only session keys that can be found with the help of session keys are
    1.26    those sent by Tgs in step K4.  *}
    1.27  
     2.1 --- a/src/HOL/Divides.thy	Mon Mar 17 18:36:04 2008 +0100
     2.2 +++ b/src/HOL/Divides.thy	Mon Mar 17 18:37:00 2008 +0100
     2.3 @@ -316,7 +316,7 @@
     2.4    then show ?thesis using divmod_div_mod by simp
     2.5  qed
     2.6  
     2.7 -text {* The ''recursion┬┤┬┤ equations for @{const div} and @{const mod} *}
     2.8 +text {* The ''recursion'' equations for @{const div} and @{const mod} *}
     2.9  
    2.10  lemma div_less [simp]:
    2.11    fixes m n :: nat
    2.12 @@ -704,61 +704,6 @@
    2.13    by (cases "n = 0") auto
    2.14  
    2.15  
    2.16 -(* Antimonotonicity of div in second argument *)
    2.17 -lemma div_le_mono2: "!!m::nat. [| 0<m; m\<le>n |] ==> (k div n) \<le> (k div m)"
    2.18 -apply (subgoal_tac "0<n")
    2.19 - prefer 2 apply simp
    2.20 -apply (induct_tac k rule: nat_less_induct)
    2.21 -apply (rename_tac "k")
    2.22 -apply (case_tac "k<n", simp)
    2.23 -apply (subgoal_tac "~ (k<m) ")
    2.24 - prefer 2 apply simp
    2.25 -apply (simp add: div_geq)
    2.26 -apply (subgoal_tac "(k-n) div n \<le> (k-m) div n")
    2.27 - prefer 2
    2.28 - apply (blast intro: div_le_mono diff_le_mono2)
    2.29 -apply (rule le_trans, simp)
    2.30 -apply (simp)
    2.31 -done
    2.32 -
    2.33 -lemma div_le_dividend [simp]: "m div n \<le> (m::nat)"
    2.34 -apply (case_tac "n=0", simp)
    2.35 -apply (subgoal_tac "m div n \<le> m div 1", simp)
    2.36 -apply (rule div_le_mono2)
    2.37 -apply (simp_all (no_asm_simp))
    2.38 -done
    2.39 -
    2.40 -(* Similar for "less than" *)
    2.41 -lemma div_less_dividend [rule_format]:
    2.42 -     "!!n::nat. 1<n ==> 0 < m --> m div n < m"
    2.43 -apply (induct_tac m rule: nat_less_induct)
    2.44 -apply (rename_tac "m")
    2.45 -apply (case_tac "m<n", simp)
    2.46 -apply (subgoal_tac "0<n")
    2.47 - prefer 2 apply simp
    2.48 -apply (simp add: div_geq)
    2.49 -apply (case_tac "n<m")
    2.50 - apply (subgoal_tac "(m-n) div n < (m-n) ")
    2.51 -  apply (rule impI less_trans_Suc)+
    2.52 -apply assumption
    2.53 -  apply (simp_all)
    2.54 -done
    2.55 -
    2.56 -declare div_less_dividend [simp]
    2.57 -
    2.58 -text{*A fact for the mutilated chess board*}
    2.59 -lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"
    2.60 -apply (case_tac "n=0", simp)
    2.61 -apply (induct "m" rule: nat_less_induct)
    2.62 -apply (case_tac "Suc (na) <n")
    2.63 -(* case Suc(na) < n *)
    2.64 -apply (frule lessI [THEN less_trans], simp add: less_not_refl3)
    2.65 -(* case n \<le> Suc(na) *)
    2.66 -apply (simp add: linorder_not_less le_Suc_eq mod_geq)
    2.67 -apply (auto simp add: Suc_diff_le le_mod_geq)
    2.68 -done
    2.69 -
    2.70 -
    2.71  subsubsection{*The Divides Relation*}
    2.72  
    2.73  lemma dvdI [intro?]: "n = m * k ==> m dvd n"
     3.1 --- a/src/HOL/Hoare/hoare_tac.ML	Mon Mar 17 18:36:04 2008 +0100
     3.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Mon Mar 17 18:37:00 2008 +0100
     3.3 @@ -86,15 +86,10 @@
     3.4  (** input does not suffer any unexpected transformation                     **)
     3.5  (*****************************************************************************)
     3.6  
     3.7 -Goal "-(Collect b) = {x. ~(b x)}";
     3.8 -by (Fast_tac 1);
     3.9 -qed "Compl_Collect";
    3.10 -
    3.11 -
    3.12  (**Simp_tacs**)
    3.13  
    3.14  val before_set2pred_simp_tac =
    3.15 -  (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect]));
    3.16 +  (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym, @{thm Compl_Collect}]));
    3.17  
    3.18  val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
    3.19  
     4.1 --- a/src/HOL/Int.thy	Mon Mar 17 18:36:04 2008 +0100
     4.2 +++ b/src/HOL/Int.thy	Mon Mar 17 18:37:00 2008 +0100
     4.3 @@ -1911,10 +1911,6 @@
     4.4  lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
     4.5  lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
     4.6  
     4.7 -lemmas int_distrib =
     4.8 -  zadd_zmult_distrib zadd_zmult_distrib2
     4.9 -  zdiff_zmult_distrib zdiff_zmult_distrib2
    4.10 -
    4.11  lemmas zmult_1 = mult_1_left [of "z::int", standard]
    4.12  lemmas zmult_1_right = mult_1_right [of "z::int", standard]
    4.13  
     5.1 --- a/src/HOL/Library/Heap.thy	Mon Mar 17 18:36:04 2008 +0100
     5.2 +++ b/src/HOL/Library/Heap.thy	Mon Mar 17 18:37:00 2008 +0100
     5.3 @@ -414,12 +414,12 @@
     5.4  lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)"
     5.5    by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def  new_ref_def)
     5.6  
     5.7 -(*not actually true ???
     5.8 +text {*not actually true ???*}
     5.9  lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)"
    5.10  apply (case_tac a)
    5.11  apply (simp add: Let_def upd_def)
    5.12  apply auto
    5.13 -done*)
    5.14 +oops
    5.15  
    5.16  lemma length_new_ref[simp]: 
    5.17    "length a (snd (ref v h)) = length a h"
    5.18 @@ -429,10 +429,6 @@
    5.19    "get_array a (snd (ref v h)) = get_array a h"
    5.20    by (simp add: new_ref_def ref_def set_ref_def get_array_def Let_def)
    5.21  
    5.22 -lemma get_array_new_ref [simp]:
    5.23 -  "get_array a (snd (ref v h)) ! i = get_array a h ! i"
    5.24 -  by (simp add: get_array_def new_ref_def ref_def set_ref_def Let_def)
    5.25 -
    5.26  lemma ref_present_upd [simp]: 
    5.27    "ref_present r (upd a i v h) = ref_present r h"
    5.28    by (simp add: upd_def ref_present_def set_array_def get_array_def)
     6.1 --- a/src/HOL/List.thy	Mon Mar 17 18:36:04 2008 +0100
     6.2 +++ b/src/HOL/List.thy	Mon Mar 17 18:37:00 2008 +0100
     6.3 @@ -1220,10 +1220,6 @@
     6.4  lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
     6.5  by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
     6.6  
     6.7 -lemma list_update_overwrite [simp]:
     6.8 -"i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
     6.9 -by (induct xs arbitrary: i) (auto split: nat.split)
    6.10 -
    6.11  lemma list_update_id[simp]: "xs[i := xs!i] = xs"
    6.12  by (induct xs arbitrary: i) (simp_all split:nat.splits)
    6.13  
     7.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Mon Mar 17 18:36:04 2008 +0100
     7.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Mon Mar 17 18:37:00 2008 +0100
     7.3 @@ -143,14 +143,6 @@
     7.4    apply (simp add: sorted_spvec.simps split:list.split_asm)
     7.5    done
     7.6  
     7.7 -lemma sorted_spvec_minus_spvec:
     7.8 -  "sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)"
     7.9 -  apply (induct v)
    7.10 -  apply (simp)
    7.11 -  apply (frule sorted_spvec_cons1, simp)
    7.12 -  apply (simp add: sorted_spvec.simps split:list.split_asm)
    7.13 -  done
    7.14 -
    7.15  lemma sorted_spvec_abs_spvec:
    7.16    "sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)"
    7.17    apply (induct v)
     8.1 --- a/src/HOL/Nat.thy	Mon Mar 17 18:36:04 2008 +0100
     8.2 +++ b/src/HOL/Nat.thy	Mon Mar 17 18:37:00 2008 +0100
     8.3 @@ -855,9 +855,6 @@
     8.4  
     8.5  subsubsection {* More results about difference *}
     8.6  
     8.7 -lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
     8.8 -by (induct m) simp_all
     8.9 -
    8.10  text {* Addition is the inverse of subtraction:
    8.11    if @{term "n \<le> m"} then @{term "n + (m - n) = m"}. *}
    8.12  lemma add_diff_inverse: "~  m < n ==> n + (m - n) = (m::nat)"
     9.1 --- a/src/HOL/Orderings.thy	Mon Mar 17 18:36:04 2008 +0100
     9.2 +++ b/src/HOL/Orderings.thy	Mon Mar 17 18:37:00 2008 +0100
     9.3 @@ -39,9 +39,6 @@
     9.4  lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
     9.5  unfolding less_le by blast
     9.6  
     9.7 -lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
     9.8 -by (erule contrapos_pn, erule subst, rule less_irrefl)
     9.9 -
    9.10  
    9.11  text {* Useful for simplification, but too risky to include by default. *}
    9.12