--- 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. *}
--- 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"
--- 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]));
--- 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]
--- 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)
--- 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)
--- 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)
--- 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)"
--- 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. *}