--- a/src/HOL/Auth/Guard/P1.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Auth/Guard/P1.thy Fri Oct 07 20:41:10 2005 +0200
@@ -398,7 +398,7 @@
==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)"
apply (erule p1.induct)
apply (simp_all add: initState.simps knows.simps pro_def prom_def
- req_def reqm_def anchor_def chain_def sign_def, blast)
+ req_def reqm_def anchor_def chain_def sign_def)
apply (blast dest: no_Key_in_agl)
apply (auto del: parts_invKey disjE dest: parts_trans
simp add: no_Key_in_appdel)
--- a/src/HOL/Auth/Guard/P2.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Auth/Guard/P2.thy Fri Oct 07 20:41:10 2005 +0200
@@ -302,7 +302,7 @@
==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)"
apply (erule p2.induct)
apply (simp_all add: initState.simps knows.simps pro_def prom_def
- req_def reqm_def anchor_def chain_def sign_def, blast)
+ req_def reqm_def anchor_def chain_def sign_def)
apply (blast dest: no_Key_in_agl)
apply (auto del: parts_invKey disjE dest: parts_trans
simp add: no_Key_in_appdel)
--- a/src/HOL/Auth/NS_Shared.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Fri Oct 07 20:41:10 2005 +0200
@@ -308,8 +308,6 @@
txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
@{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *}
apply (force dest!: Crypt_imp_keysFor)
-txt{*NS3*}
-apply blast
txt{*NS4*}
apply (blast dest: B_trusts_NS3
Says_imp_knows_Spy [THEN analz.Inj]
@@ -339,8 +337,6 @@
apply (simp_all add: ex_disj_distrib, blast)
txt{*NS2*}
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
-txt{*NS3*}
-apply blast
txt{*NS4*}
apply (blast dest: B_trusts_NS3
dest: Says_imp_knows_Spy [THEN analz.Inj]
@@ -359,8 +355,6 @@
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)
txt{*NS2*}
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
-txt{*NS3*}
-apply (blast dest!: cert_A_form)
txt{*NS5*}
apply (blast dest!: A_trusts_NS2
dest: Says_imp_knows_Spy [THEN analz.Inj]
--- a/src/HOL/Auth/OtwayRees.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Fri Oct 07 20:41:10 2005 +0200
@@ -156,7 +156,7 @@
"[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
evs \<in> otway |]
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
-by (erule rev_mp, erule otway.induct, simp_all, blast)
+by (erule rev_mp, erule otway.induct, simp_all)
(****
--- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Fri Oct 07 20:41:10 2005 +0200
@@ -161,7 +161,7 @@
evs \<in> otway |]
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
apply (erule rev_mp)
-apply (erule otway.induct, simp_all, blast)
+apply (erule otway.induct, simp_all)
done
--- a/src/HOL/Auth/Yahalom.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Auth/Yahalom.thy Fri Oct 07 20:41:10 2005 +0200
@@ -176,7 +176,7 @@
"[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}
\<in> set evs; evs \<in> yahalom |]
==> K \<notin> range shrK"
-by (erule rev_mp, erule yahalom.induct, simp_all, blast)
+by (erule rev_mp, erule yahalom.induct, simp_all)
subsection{*Secrecy Theorems*}
--- a/src/HOL/Bali/Decl.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Bali/Decl.thy Fri Oct 07 20:41:10 2005 +0200
@@ -385,9 +385,7 @@
by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def)
lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
-apply (simp add: SXcptC_def)
-apply auto
-done
+by (simp add: SXcptC_def)
constdefs standard_classes :: "cdecl list"
"standard_classes \<equiv> [ObjectC, SXcptC Throwable,
--- a/src/HOL/Hoare/Pointers0.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Hoare/Pointers0.thy Fri Oct 07 20:41:10 2005 +0200
@@ -296,9 +296,6 @@
{p = X}"
apply vcg_simp
apply blast
- apply clarsimp
- apply(erule disjE)
- apply clarsimp
apply fastsimp
apply clarsimp
done
--- a/src/HOL/Library/Multiset.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/Library/Multiset.thy Fri Oct 07 20:41:10 2005 +0200
@@ -235,6 +235,7 @@
apply (blast dest: sym)
done
+ML"reset use_neq_simproc"
lemma add_eq_conv_diff:
"(M + {#a#} = N + {#b#}) =
(M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
@@ -243,6 +244,7 @@
apply (rule conjI, force, safe, simp_all)
apply (simp add: eq_sym_conv)
done
+ML"set use_neq_simproc"
declare Rep_multiset_inject [symmetric, simp del]
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Fri Oct 07 20:41:10 2005 +0200
@@ -112,23 +112,17 @@
"\<forall> ks. (empty(rev ks[\<mapsto>]rev xs)) k = Some x \<longrightarrow> length ks = length xs \<longrightarrow>
xs ! length (takeWhile (\<lambda>z. z \<noteq> k) ks) = x"
apply (induct xs)
-apply simp
+ apply simp
apply (intro strip)
apply (subgoal_tac "\<exists> k' kr. ks = k' # kr")
-apply (clarify)
-apply (drule_tac x=kr in spec)
-apply (simp only: rev.simps)
-apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
-apply (simp only:)
-apply (case_tac "k' = k")
-apply simp
-apply simp
-apply (case_tac "k = k'")
-apply simp
-apply (simp add: empty_def)
-apply (simp add: map_upds_append [THEN sym])
+ apply (clarify)
+ apply (drule_tac x=kr in spec)
+ apply (simp only: rev.simps)
+ apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
+ apply (simp split:split_if_asm)
+ apply (simp add: map_upds_append [THEN sym])
apply (case_tac ks)
-apply auto
+ apply auto
done
--- a/src/HOL/MicroJava/Comp/Index.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/MicroJava/Comp/Index.thy Fri Oct 07 20:41:10 2005 +0200
@@ -5,7 +5,9 @@
(* Index of variable in list of parameter names and local variables *)
-theory Index imports AuxLemmas DefsComp begin
+theory Index
+imports AuxLemmas DefsComp
+begin
(*indexing a variable name among all variable declarations in a method body*)
constdefs
@@ -76,7 +78,6 @@
apply (case_tac b, simp)
apply (rule conjI)
apply (simp add: gl_def)
-apply (intro strip, simp)
apply (simp add: galldefs del: set_append map_append)
done
--- a/src/HOL/MicroJava/Comp/TypeInf.thy Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/MicroJava/Comp/TypeInf.thy Fri Oct 07 20:41:10 2005 +0200
@@ -4,7 +4,9 @@
*)
(* Exact position in theory hierarchy still to be determined *)
-theory TypeInf imports WellType begin
+theory TypeInf
+imports "../J/WellType"
+begin
--- a/src/HOL/ex/MT.ML Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/ex/MT.ML Fri Oct 07 20:41:10 2005 +0200
@@ -609,7 +609,6 @@
by (safe_tac HOL_cs);
by (excluded_middle_tac "ev=x" 1);
by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (Blast_tac 1);
by (asm_simp_tac (simpset() addsimps [ve_app_owr1, te_app_owr1]) 1);
qed "hasty_env1";
@@ -653,12 +652,9 @@
by (safe_tac HOL_cs);
by (excluded_middle_tac "ev2=ev1a" 1);
by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
-by (Blast_tac 1);
by (asm_simp_tac (simpset() delsimps mem_simps
addsimps [ve_app_owr1, te_app_owr1]) 1);
-by (hyp_subst_tac 1);
-by (etac subst 1);
by (Blast_tac 1);
qed "consistency_fix";
--- a/src/HOL/simpdata.ML Fri Oct 07 18:49:20 2005 +0200
+++ b/src/HOL/simpdata.ML Fri Oct 07 20:41:10 2005 +0200
@@ -135,6 +135,39 @@
Simplifier.simproc (Theory.sign_of (the_context ()))
"defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
+
+(*** simproc for proving "(y = x) == False" from prmise "~(x = y)" ***)
+
+val use_neq_simproc = ref true;
+
+local
+
+val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI;
+
+fun neq_prover sg ss (eq $ lhs $ rhs) =
+let
+ fun test thm = (case #prop(rep_thm thm) of
+ _ $ (Not $ (eq' $ l' $ r')) =>
+ Not = HOLogic.Not andalso eq' = eq andalso
+ r' aconv lhs andalso l' aconv rhs
+ | _ => false)
+in
+ if !use_neq_simproc then
+ case Library.find_first test (prems_of_ss ss) of NONE => NONE
+ | SOME thm => SOME (thm RS neq_to_EQ_False)
+ else NONE
+end
+
+in
+
+val neq_simproc =
+ Simplifier.simproc (the_context ()) "neq_simproc" ["x = y"] neq_prover;
+
+end;
+
+
+
+
(*** Simproc for Let ***)
val use_let_simproc = ref true;
@@ -336,7 +369,7 @@
disj_not1, not_all, not_ex, cases_simp,
thm "the_eq_trivial", the_sym_eq_trivial]
@ ex_simps @ all_simps @ simp_thms)
- addsimprocs [defALL_regroup,defEX_regroup,let_simproc]
+ addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]
addcongs [imp_cong, simp_implies_cong]
addsplits [split_if];