changes due to new neq_simproc in simpdata.ML
authornipkow
Fri Oct 07 20:41:10 2005 +0200 (2005-10-07)
changeset 1777893d7e524417a
parent 17777 05f5532a8289
child 17779 407bea05c2da
changes due to new neq_simproc in simpdata.ML
src/HOL/Auth/Guard/P1.thy
src/HOL/Auth/Guard/P2.thy
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_Bad.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Bali/Decl.thy
src/HOL/Hoare/Pointers0.thy
src/HOL/Library/Multiset.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/MicroJava/Comp/Index.thy
src/HOL/MicroJava/Comp/TypeInf.thy
src/HOL/ex/MT.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Auth/Guard/P1.thy	Fri Oct 07 18:49:20 2005 +0200
     1.2 +++ b/src/HOL/Auth/Guard/P1.thy	Fri Oct 07 20:41:10 2005 +0200
     1.3 @@ -398,7 +398,7 @@
     1.4        ==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)"
     1.5  apply (erule p1.induct)
     1.6  apply (simp_all add: initState.simps knows.simps pro_def prom_def
     1.7 -                req_def reqm_def anchor_def chain_def sign_def, blast) 
     1.8 +                req_def reqm_def anchor_def chain_def sign_def)
     1.9  apply (blast dest: no_Key_in_agl)
    1.10  apply (auto del: parts_invKey disjE  dest: parts_trans
    1.11              simp add: no_Key_in_appdel)
     2.1 --- a/src/HOL/Auth/Guard/P2.thy	Fri Oct 07 18:49:20 2005 +0200
     2.2 +++ b/src/HOL/Auth/Guard/P2.thy	Fri Oct 07 20:41:10 2005 +0200
     2.3 @@ -302,7 +302,7 @@
     2.4        ==> (Key (priK A):parts (knows (Friend B) evs)) --> (A:bad)"
     2.5  apply (erule p2.induct)
     2.6  apply (simp_all add: initState.simps knows.simps pro_def prom_def
     2.7 -                req_def reqm_def anchor_def chain_def sign_def, blast) 
     2.8 +                req_def reqm_def anchor_def chain_def sign_def) 
     2.9  apply (blast dest: no_Key_in_agl)
    2.10  apply (auto del: parts_invKey disjE  dest: parts_trans
    2.11              simp add: no_Key_in_appdel)
     3.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Oct 07 18:49:20 2005 +0200
     3.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Oct 07 20:41:10 2005 +0200
     3.3 @@ -308,8 +308,6 @@
     3.4  txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
     3.5      @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
     3.6  apply (force dest!: Crypt_imp_keysFor)
     3.7 -txt{*NS3*}
     3.8 -apply blast
     3.9  txt{*NS4*}
    3.10  apply (blast dest: B_trusts_NS3
    3.11  	           Says_imp_knows_Spy [THEN analz.Inj]
    3.12 @@ -339,8 +337,6 @@
    3.13  apply (simp_all add: ex_disj_distrib, blast)
    3.14  txt{*NS2*}
    3.15  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
    3.16 -txt{*NS3*}
    3.17 -apply blast
    3.18  txt{*NS4*}
    3.19  apply (blast dest: B_trusts_NS3
    3.20  	     dest: Says_imp_knows_Spy [THEN analz.Inj]
    3.21 @@ -359,8 +355,6 @@
    3.22  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)
    3.23  txt{*NS2*}
    3.24  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
    3.25 -txt{*NS3*}
    3.26 -apply (blast dest!: cert_A_form)
    3.27  txt{*NS5*}
    3.28  apply (blast dest!: A_trusts_NS2
    3.29  	     dest: Says_imp_knows_Spy [THEN analz.Inj]
     4.1 --- a/src/HOL/Auth/OtwayRees.thy	Fri Oct 07 18:49:20 2005 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees.thy	Fri Oct 07 20:41:10 2005 +0200
     4.3 @@ -156,7 +156,7 @@
     4.4       "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
     4.5           evs \<in> otway |]
     4.6        ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
     4.7 -by (erule rev_mp, erule otway.induct, simp_all, blast)
     4.8 +by (erule rev_mp, erule otway.induct, simp_all)
     4.9  
    4.10  
    4.11  (****
     5.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Fri Oct 07 18:49:20 2005 +0200
     5.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Fri Oct 07 20:41:10 2005 +0200
     5.3 @@ -161,7 +161,7 @@
     5.4           evs \<in> otway |]
     5.5        ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
     5.6  apply (erule rev_mp)
     5.7 -apply (erule otway.induct, simp_all, blast)
     5.8 +apply (erule otway.induct, simp_all)
     5.9  done
    5.10  
    5.11  
     6.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Oct 07 18:49:20 2005 +0200
     6.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Oct 07 20:41:10 2005 +0200
     6.3 @@ -176,7 +176,7 @@
     6.4       "[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}
     6.5             \<in> set evs;   evs \<in> yahalom |]
     6.6        ==> K \<notin> range shrK"
     6.7 -by (erule rev_mp, erule yahalom.induct, simp_all, blast)
     6.8 +by (erule rev_mp, erule yahalom.induct, simp_all)
     6.9  
    6.10  
    6.11  subsection{*Secrecy Theorems*}
     7.1 --- a/src/HOL/Bali/Decl.thy	Fri Oct 07 18:49:20 2005 +0200
     7.2 +++ b/src/HOL/Bali/Decl.thy	Fri Oct 07 20:41:10 2005 +0200
     7.3 @@ -385,9 +385,7 @@
     7.4  by (simp add: ObjectC_def SXcptC_def Object_def SXcpt_def)
     7.5  
     7.6  lemma SXcptC_inject [simp]: "(SXcptC xn = SXcptC xm) = (xn = xm)"
     7.7 -apply (simp add: SXcptC_def)
     7.8 -apply auto
     7.9 -done
    7.10 +by (simp add: SXcptC_def)
    7.11  
    7.12  constdefs standard_classes :: "cdecl list"
    7.13           "standard_classes \<equiv> [ObjectC, SXcptC Throwable,
     8.1 --- a/src/HOL/Hoare/Pointers0.thy	Fri Oct 07 18:49:20 2005 +0200
     8.2 +++ b/src/HOL/Hoare/Pointers0.thy	Fri Oct 07 20:41:10 2005 +0200
     8.3 @@ -296,9 +296,6 @@
     8.4    {p = X}"
     8.5  apply vcg_simp
     8.6    apply blast
     8.7 - apply clarsimp
     8.8 - apply(erule disjE)
     8.9 -  apply clarsimp
    8.10   apply fastsimp
    8.11  apply clarsimp
    8.12  done
     9.1 --- a/src/HOL/Library/Multiset.thy	Fri Oct 07 18:49:20 2005 +0200
     9.2 +++ b/src/HOL/Library/Multiset.thy	Fri Oct 07 20:41:10 2005 +0200
     9.3 @@ -235,6 +235,7 @@
     9.4    apply (blast dest: sym)
     9.5    done
     9.6  
     9.7 +ML"reset use_neq_simproc"
     9.8  lemma add_eq_conv_diff:
     9.9    "(M + {#a#} = N + {#b#}) =
    9.10     (M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#})"
    9.11 @@ -243,6 +244,7 @@
    9.12    apply (rule conjI, force, safe, simp_all)
    9.13    apply (simp add: eq_sym_conv)
    9.14    done
    9.15 +ML"set use_neq_simproc"
    9.16  
    9.17  declare Rep_multiset_inject [symmetric, simp del]
    9.18  
    10.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Oct 07 18:49:20 2005 +0200
    10.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Oct 07 20:41:10 2005 +0200
    10.3 @@ -112,23 +112,17 @@
    10.4    "\<forall> ks. (empty(rev ks[\<mapsto>]rev xs)) k = Some x \<longrightarrow> length ks = length xs \<longrightarrow>
    10.5      xs ! length (takeWhile (\<lambda>z. z \<noteq> k) ks) = x"
    10.6  apply (induct xs)
    10.7 -apply simp
    10.8 + apply simp
    10.9  apply (intro strip)
   10.10  apply (subgoal_tac "\<exists> k' kr. ks = k' # kr")
   10.11 -apply (clarify)
   10.12 -apply (drule_tac x=kr in spec)
   10.13 -apply (simp only: rev.simps)
   10.14 -apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
   10.15 -apply (simp only:)
   10.16 -apply (case_tac "k' = k")
   10.17 -apply simp
   10.18 -apply simp 
   10.19 -apply (case_tac "k = k'")
   10.20 -apply simp
   10.21 -apply (simp add: empty_def)
   10.22 -apply (simp add: map_upds_append [THEN sym])
   10.23 + apply (clarify)
   10.24 + apply (drule_tac x=kr in spec)
   10.25 + apply (simp only: rev.simps)
   10.26 + apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
   10.27 +  apply (simp split:split_if_asm)
   10.28 + apply (simp add: map_upds_append [THEN sym])
   10.29  apply (case_tac ks)
   10.30 -apply auto
   10.31 + apply auto
   10.32  done
   10.33  
   10.34  
    11.1 --- a/src/HOL/MicroJava/Comp/Index.thy	Fri Oct 07 18:49:20 2005 +0200
    11.2 +++ b/src/HOL/MicroJava/Comp/Index.thy	Fri Oct 07 20:41:10 2005 +0200
    11.3 @@ -5,7 +5,9 @@
    11.4  
    11.5  (* Index of variable in list of parameter names and local variables *)
    11.6  
    11.7 -theory Index imports  AuxLemmas DefsComp begin
    11.8 +theory Index
    11.9 +imports AuxLemmas DefsComp
   11.10 +begin
   11.11  
   11.12  (*indexing a variable name among all variable declarations in a method body*)
   11.13  constdefs
   11.14 @@ -76,7 +78,6 @@
   11.15  apply (case_tac b, simp)
   11.16  apply (rule conjI)
   11.17  apply (simp add: gl_def)
   11.18 -apply (intro strip, simp)
   11.19  apply (simp add: galldefs del: set_append map_append)
   11.20  done
   11.21  
    12.1 --- a/src/HOL/MicroJava/Comp/TypeInf.thy	Fri Oct 07 18:49:20 2005 +0200
    12.2 +++ b/src/HOL/MicroJava/Comp/TypeInf.thy	Fri Oct 07 20:41:10 2005 +0200
    12.3 @@ -4,7 +4,9 @@
    12.4  *)
    12.5  
    12.6  (* Exact position in theory hierarchy still to be determined *)
    12.7 -theory TypeInf imports  WellType begin
    12.8 +theory TypeInf
    12.9 +imports "../J/WellType"
   12.10 +begin
   12.11  
   12.12  
   12.13  
    13.1 --- a/src/HOL/ex/MT.ML	Fri Oct 07 18:49:20 2005 +0200
    13.2 +++ b/src/HOL/ex/MT.ML	Fri Oct 07 20:41:10 2005 +0200
    13.3 @@ -609,7 +609,6 @@
    13.4  by (safe_tac HOL_cs);
    13.5  by (excluded_middle_tac "ev=x" 1);
    13.6  by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
    13.7 -by (Blast_tac 1);
    13.8  by (asm_simp_tac (simpset() addsimps [ve_app_owr1, te_app_owr1]) 1);
    13.9  qed "hasty_env1";
   13.10  
   13.11 @@ -653,12 +652,9 @@
   13.12  by (safe_tac HOL_cs);
   13.13  by (excluded_middle_tac "ev2=ev1a" 1);
   13.14  by (asm_full_simp_tac (simpset() addsimps [ve_app_owr2, te_app_owr2]) 1);
   13.15 -by (Blast_tac 1);
   13.16  
   13.17  by (asm_simp_tac (simpset() delsimps mem_simps
   13.18                             addsimps [ve_app_owr1, te_app_owr1]) 1);
   13.19 -by (hyp_subst_tac 1);
   13.20 -by (etac subst 1);
   13.21  by (Blast_tac 1);
   13.22  qed "consistency_fix";
   13.23  
    14.1 --- a/src/HOL/simpdata.ML	Fri Oct 07 18:49:20 2005 +0200
    14.2 +++ b/src/HOL/simpdata.ML	Fri Oct 07 20:41:10 2005 +0200
    14.3 @@ -135,6 +135,39 @@
    14.4    Simplifier.simproc (Theory.sign_of (the_context ()))
    14.5      "defined ALL" ["ALL x. P x"] Quantifier1.rearrange_all;
    14.6  
    14.7 +
    14.8 +(*** simproc for proving "(y = x) == False" from prmise "~(x = y)" ***)
    14.9 +
   14.10 +val use_neq_simproc = ref true;
   14.11 +
   14.12 +local
   14.13 +
   14.14 +val neq_to_EQ_False = thm "not_sym" RS Eq_FalseI;
   14.15 +
   14.16 +fun neq_prover sg ss (eq $ lhs $ rhs) =
   14.17 +let
   14.18 +  fun test thm = (case #prop(rep_thm thm) of
   14.19 +                    _ $ (Not $ (eq' $ l' $ r')) =>
   14.20 +                      Not = HOLogic.Not andalso eq' = eq andalso
   14.21 +                      r' aconv lhs andalso l' aconv rhs
   14.22 +                  | _ => false)
   14.23 +in
   14.24 +  if !use_neq_simproc then
   14.25 +    case Library.find_first test (prems_of_ss ss) of NONE => NONE
   14.26 +    | SOME thm => SOME (thm RS neq_to_EQ_False)
   14.27 +  else NONE
   14.28 +end
   14.29 +
   14.30 +in
   14.31 +
   14.32 +val neq_simproc =
   14.33 +  Simplifier.simproc (the_context ()) "neq_simproc" ["x = y"] neq_prover;
   14.34 +
   14.35 +end;
   14.36 +
   14.37 +
   14.38 +
   14.39 +
   14.40  (*** Simproc for Let ***)
   14.41  
   14.42  val use_let_simproc = ref true;
   14.43 @@ -336,7 +369,7 @@
   14.44         disj_not1, not_all, not_ex, cases_simp,
   14.45         thm "the_eq_trivial", the_sym_eq_trivial]
   14.46       @ ex_simps @ all_simps @ simp_thms)
   14.47 -     addsimprocs [defALL_regroup,defEX_regroup,let_simproc]
   14.48 +     addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]
   14.49       addcongs [imp_cong, simp_implies_cong]
   14.50       addsplits [split_if];
   14.51