Deleted the redundant simprule not_parts_not_analz
authorpaulson
Tue Sep 16 13:58:02 1997 +0200 (1997-09-16)
changeset 367465ec38fbb265
parent 3673 3b06747c3f37
child 3675 70dd312b70b2
Deleted the redundant simprule not_parts_not_analz
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Sep 16 13:54:41 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Tue Sep 16 13:58:02 1997 +0200
     1.3 @@ -344,8 +344,7 @@
     1.4  by analz_sees_tac;
     1.5  by (ALLGOALS
     1.6      (asm_simp_tac (!simpset addcongs [conj_cong] 
     1.7 -                            addsimps [analz_insert_eq, not_parts_not_analz, 
     1.8 -				      analz_insert_freshK]
     1.9 +                            addsimps [analz_insert_eq, analz_insert_freshK]
    1.10                              setloop split_tac [expand_if])));
    1.11  (*Oops*)
    1.12  by (blast_tac (!claset addSDs [unique_session_keys]) 4);
     2.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 16 13:54:41 1997 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Tue Sep 16 13:58:02 1997 +0200
     2.3 @@ -268,9 +268,8 @@
     2.4  by (etac otway.induct 1);
     2.5  by analz_sees_tac;
     2.6  by (ALLGOALS
     2.7 -    (asm_simp_tac (!simpset addcongs [conj_cong] 
     2.8 -                            addsimps [analz_insert_eq, not_parts_not_analz, 
     2.9 -				      analz_insert_freshK]
    2.10 +    (asm_simp_tac (!simpset addcongs [conj_cong, if_weak_cong] 
    2.11 +                            addsimps [analz_insert_eq, analz_insert_freshK]
    2.12                              setloop split_tac [expand_if])));
    2.13  (*Oops*)
    2.14  by (blast_tac (!claset addSDs [unique_session_keys]) 4);
     3.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 16 13:54:41 1997 +0200
     3.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Tue Sep 16 13:58:02 1997 +0200
     3.3 @@ -231,8 +231,7 @@
     3.4  by analz_sees_tac;
     3.5  by (ALLGOALS
     3.6      (asm_simp_tac (!simpset addcongs [conj_cong] 
     3.7 -                            addsimps [analz_insert_eq, not_parts_not_analz, 
     3.8 -				      analz_insert_freshK]
     3.9 +                            addsimps [analz_insert_eq, analz_insert_freshK]
    3.10                              setloop split_tac [expand_if])));
    3.11  (*Oops*)
    3.12  by (blast_tac (!claset addSDs [unique_session_keys]) 4);
     4.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Sep 16 13:54:41 1997 +0200
     4.2 +++ b/src/HOL/Auth/Yahalom.ML	Tue Sep 16 13:58:02 1997 +0200
     4.3 @@ -228,8 +228,7 @@
     4.4  by analz_sees_tac;
     4.5  by (ALLGOALS
     4.6      (asm_simp_tac 
     4.7 -     (!simpset addsimps [analz_insert_eq, not_parts_not_analz, 
     4.8 -			 analz_insert_freshK]
     4.9 +     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
    4.10                 setloop split_tac [expand_if])));
    4.11  (*Oops*)
    4.12  by (blast_tac (!claset addDs [unique_session_keys]) 3);
    4.13 @@ -387,7 +386,7 @@
    4.14  by (ALLGOALS  (*22 seconds*)
    4.15      (asm_simp_tac 
    4.16       (analz_image_freshK_ss addsimps
    4.17 -        ([all_conj_distrib, not_parts_not_analz, analz_image_freshK,
    4.18 +        ([all_conj_distrib, analz_image_freshK,
    4.19  	  KeyWithNonce_Says, fresh_not_KeyWithNonce, 
    4.20  	  imp_disj_not1,  (*Moves NBa~=NB to the front*)
    4.21  	  Says_Server_KeyWithNonce] 
    4.22 @@ -507,8 +506,7 @@
    4.23  by analz_sees_tac;
    4.24  by (ALLGOALS
    4.25      (asm_simp_tac 
    4.26 -     (!simpset addsimps ([analz_insert_eq, not_parts_not_analz,
    4.27 -                          analz_insert_freshK] @ pushes)
    4.28 +     (!simpset addsimps ([analz_insert_eq, analz_insert_freshK] @ pushes)
    4.29                 setloop split_tac [expand_if])));
    4.30  (*Prove YM3 by showing that no NB can also be an NA*)
    4.31  by (blast_tac (!claset addDs [Says_imp_sees_Spy RS parts.Inj]
     5.1 --- a/src/HOL/Auth/Yahalom2.ML	Tue Sep 16 13:54:41 1997 +0200
     5.2 +++ b/src/HOL/Auth/Yahalom2.ML	Tue Sep 16 13:58:02 1997 +0200
     5.3 @@ -232,8 +232,7 @@
     5.4  by analz_sees_tac;
     5.5  by (ALLGOALS
     5.6      (asm_simp_tac 
     5.7 -     (!simpset addsimps [analz_insert_eq, not_parts_not_analz, 
     5.8 -			 analz_insert_freshK]
     5.9 +     (!simpset addsimps [analz_insert_eq, analz_insert_freshK]
    5.10                 setloop split_tac [expand_if])));
    5.11  (*Oops*)
    5.12  by (blast_tac (!claset addDs [unique_session_keys]) 3);