# HG changeset patch
# User nipkow
# Date 1128710470 -7200
# Node ID 93d7e524417a2174b788fcc891abbbb2ac786b51
# Parent  05f5532a8289bc84b6f2a9bdd13f9e04126259b7
changes due to new neq_simproc in simpdata.ML

diff -r 05f5532a8289 -r 93d7e524417a src/HOL/Auth/Guard/P1.thy
--- 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)
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/Auth/Guard/P2.thy
--- 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)
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/Auth/NS_Shared.thy
--- 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]
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/Auth/OtwayRees.thy
--- 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)
 
 
 (****
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/Auth/OtwayRees_Bad.thy
--- 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
 
 
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/Auth/Yahalom.thy
--- 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*}
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/Bali/Decl.thy
--- 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,
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/Hoare/Pointers0.thy
--- 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
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/Library/Multiset.thy
--- 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]
 
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/MicroJava/Comp/CorrCompTp.thy
--- 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
 
 
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/MicroJava/Comp/Index.thy
--- 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
 
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/MicroJava/Comp/TypeInf.thy
--- 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
 
 
 
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/ex/MT.ML
--- 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";
 
diff -r 05f5532a8289 -r 93d7e524417a src/HOL/simpdata.ML
--- 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];