Now if_weak_cong is a standard congruence rule
authorpaulson
Thu Jul 08 13:38:41 1999 +0200 (1999-07-08)
changeset 69154ab8e31a8421
parent 6914 ad689270a265
child 6916 4957978b6f9e
Now if_weak_cong is a standard congruence rule
src/HOL/Auth/Message.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/Public.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/TLS.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Thu Jul 08 13:37:40 1999 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Thu Jul 08 13:38:41 1999 +0200
     1.3 @@ -906,7 +906,7 @@
     1.4  fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
     1.5                       assume_tac (i+1);
     1.6  
     1.7 -(*Apply the EX-ALL quantifification to prove uniqueness theorems in 
     1.8 +(*Apply the EX-ALL quantification to prove uniqueness theorems in 
     1.9    their standard form*)
    1.10  fun prove_unique_tac lemma = 
    1.11    EVERY' [dtac lemma,
     2.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jul 08 13:37:40 1999 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Jul 08 13:38:41 1999 +0200
     2.3 @@ -241,7 +241,7 @@
     2.4  by (etac otway.induct 1);
     2.5  by analz_knows_Spy_tac;
     2.6  by (ALLGOALS
     2.7 -    (asm_simp_tac (simpset() addcongs [conj_cong, if_weak_cong] 
     2.8 +    (asm_simp_tac (simpset() addcongs [conj_cong] 
     2.9                               addsimps [analz_insert_eq, analz_insert_freshK]
    2.10                                        @ pushes @ split_ifs)));
    2.11  (*Oops*)
     3.1 --- a/src/HOL/Auth/Public.ML	Thu Jul 08 13:37:40 1999 +0200
     3.2 +++ b/src/HOL/Auth/Public.ML	Thu Jul 08 13:38:41 1999 +0200
     3.3 @@ -168,11 +168,10 @@
     3.4  (*Reverse the normal simplification of "image" to build up (not break down)
     3.5    the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
     3.6  val analz_image_keys_ss = 
     3.7 -     simpset() addcongs [if_weak_cong]
     3.8 -	      delsimps [image_insert, image_Un]
     3.9 -              delsimps [imp_disjL]    (*reduces blow-up*)
    3.10 -              addsimps [image_insert RS sym, image_Un RS sym,
    3.11 -			rangeI, 
    3.12 -			insert_Key_singleton, 
    3.13 -			insert_Key_image, Un_assoc RS sym];
    3.14 +     simpset() delsimps [image_insert, image_Un]
    3.15 +	       delsimps [imp_disjL]    (*reduces blow-up*)
    3.16 +	       addsimps [image_insert RS sym, image_Un RS sym,
    3.17 +			 rangeI, 
    3.18 +			 insert_Key_singleton, 
    3.19 +			 insert_Key_image, Un_assoc RS sym];
    3.20  
     4.1 --- a/src/HOL/Auth/Shared.ML	Thu Jul 08 13:37:40 1999 +0200
     4.2 +++ b/src/HOL/Auth/Shared.ML	Thu Jul 08 13:38:41 1999 +0200
     4.3 @@ -235,14 +235,13 @@
     4.4    the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
     4.5    erase occurrences of forwarded message components (X).*)
     4.6  val analz_image_freshK_ss = 
     4.7 -     simpset() addcongs [if_weak_cong]
     4.8 -	      delsimps [image_insert, image_Un]
     4.9 -              delsimps [imp_disjL]    (*reduces blow-up*)
    4.10 -              addsimps [image_insert RS sym, image_Un RS sym,
    4.11 -			analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
    4.12 -			insert_Key_singleton, subset_Compl_range,
    4.13 -			Key_not_used, insert_Key_image, Un_assoc RS sym]
    4.14 -                       @disj_comms;
    4.15 +     simpset() delsimps [image_insert, image_Un]
    4.16 +	       delsimps [imp_disjL]    (*reduces blow-up*)
    4.17 +	       addsimps [image_insert RS sym, image_Un RS sym,
    4.18 +			 analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
    4.19 +			 insert_Key_singleton, subset_Compl_range,
    4.20 +			 Key_not_used, insert_Key_image, Un_assoc RS sym]
    4.21 +			@disj_comms;
    4.22  
    4.23  (*Lemma for the trivial direction of the if-and-only-if*)
    4.24  Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
     5.1 --- a/src/HOL/Auth/TLS.ML	Thu Jul 08 13:37:40 1999 +0200
     5.2 +++ b/src/HOL/Auth/TLS.ML	Thu Jul 08 13:38:41 1999 +0200
     5.3 @@ -176,14 +176,10 @@
     5.4  fun analz_induct_tac i = 
     5.5      etac tls.induct i   THEN
     5.6      ClientKeyExch_tac  (i+6)  THEN	(*ClientKeyExch*)
     5.7 -    ALLGOALS (asm_simp_tac 
     5.8 -              (simpset() addcongs [if_weak_cong]
     5.9 -                         addsimps split_ifs @ pushes))  THEN
    5.10 +    ALLGOALS (asm_simp_tac (simpset() addsimps split_ifs @ pushes))  THEN
    5.11      (*Remove instances of pubK B:  the Spy already knows all public keys.
    5.12        Combining the two simplifier calls makes them run extremely slowly.*)
    5.13 -    ALLGOALS (asm_simp_tac 
    5.14 -              (simpset() addcongs [if_weak_cong]
    5.15 -			 addsimps [insert_absorb]));
    5.16 +    ALLGOALS (asm_simp_tac (simpset() addsimps [insert_absorb]));
    5.17  
    5.18  
    5.19  (*** Properties of items found in Notes ***)
     6.1 --- a/src/HOL/simpdata.ML	Thu Jul 08 13:37:40 1999 +0200
     6.2 +++ b/src/HOL/simpdata.ML	Thu Jul 08 13:38:41 1999 +0200
     6.3 @@ -483,8 +483,7 @@
     6.4  
     6.5  (* install implicit simpset *)
     6.6  
     6.7 -simpset_ref() := HOL_ss;
     6.8 -
     6.9 +simpset_ref() := HOL_ss addcongs [if_weak_cong];
    6.10  
    6.11  
    6.12  (*** integration of simplifier with classical reasoner ***)