Made proofs more concise by replacing calls to spy_analz_tac by uses of
authorpaulson
Thu Jun 19 11:31:14 1997 +0200 (1997-06-19)
changeset 3451d10f100676d8
parent 3450 cd73bc206d87
child 3452 fa14fb9a572c
Made proofs more concise by replacing calls to spy_analz_tac by uses of
analz_insert_eq in rewriting
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/Provers/blast.ML
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Thu Jun 19 11:28:55 1997 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Thu Jun 19 11:31:14 1997 +0200
     1.3 @@ -221,8 +221,8 @@
     1.4  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     1.5  (*Takes 24 secs*)
     1.6  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     1.7 -(*NS4, Fake*) 
     1.8 -by (EVERY (map spy_analz_tac [3,2]));
     1.9 +(*Fake*) 
    1.10 +by (spy_analz_tac 2);
    1.11  (*Base*)
    1.12  by (Blast_tac 1);
    1.13  qed_spec_mp "analz_image_freshK";
    1.14 @@ -283,15 +283,18 @@
    1.15  by analz_sees_tac;
    1.16  by (ALLGOALS 
    1.17      (asm_simp_tac 
    1.18 -     (!simpset addsimps ([not_parts_not_analz, analz_insert_freshK] @ pushes)
    1.19 +     (!simpset addsimps ([analz_insert_eq, not_parts_not_analz, 
    1.20 +			  analz_insert_freshK] @ pushes)
    1.21                 setloop split_tac [expand_if])));
    1.22 -(*NS4, Fake*) 
    1.23 -by (EVERY (map spy_analz_tac [4,1]));
    1.24 +(*Oops*)
    1.25 +by (blast_tac (!claset addDs [unique_session_keys]) 5);
    1.26 +(*NS4*) 
    1.27 +by (Blast_tac 4);
    1.28  (*NS2*)
    1.29  by (blast_tac (!claset addSEs sees_Spy_partsEs
    1.30 -                       addIs [parts_insertI, impOfSubs analz_subset_parts]) 1);
    1.31 -(*Oops*)
    1.32 -by (blast_tac (!claset addDs [unique_session_keys]) 2);
    1.33 +                       addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
    1.34 +(*Fake*) 
    1.35 +by (spy_analz_tac 1);
    1.36  (*NS3*) (**LEVEL 6 **)
    1.37  by (step_tac (!claset delrules [impCE]) 1);
    1.38  by (forward_tac [Says_imp_sees_Spy' RS parts.Inj RS A_trusts_NS2] 1);
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu Jun 19 11:28:55 1997 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu Jun 19 11:31:14 1997 +0200
     2.3 @@ -192,10 +192,10 @@
     2.4  by (REPEAT_FIRST (resolve_tac [allI, impI]));
     2.5  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     2.6  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     2.7 +(*Fake*) 
     2.8 +by (spy_analz_tac 2);
     2.9  (*Base*)
    2.10  by (Blast_tac 1);
    2.11 -(*Fake, OR2, OR4*) 
    2.12 -by (REPEAT (spy_analz_tac 1));
    2.13  qed_spec_mp "analz_image_freshK";
    2.14  
    2.15  
    2.16 @@ -365,16 +365,18 @@
    2.17  by analz_sees_tac;
    2.18  by (ALLGOALS
    2.19      (asm_simp_tac (!simpset addcongs [conj_cong] 
    2.20 -                            addsimps [not_parts_not_analz, analz_insert_freshK]
    2.21 +                            addsimps [analz_insert_eq, not_parts_not_analz, 
    2.22 +				      analz_insert_freshK]
    2.23                              setloop split_tac [expand_if])));
    2.24 +(*Oops*)
    2.25 +by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    2.26 +(*OR4*) 
    2.27 +by (Blast_tac 3);
    2.28  (*OR3*)
    2.29 -by (blast_tac (!claset delrules [impCE]
    2.30 -                       addSEs sees_Spy_partsEs
    2.31 -                       addIs [impOfSubs analz_subset_parts]) 3);
    2.32 -(*OR4, OR2, Fake*) 
    2.33 -by (REPEAT_FIRST spy_analz_tac);
    2.34 -(*Oops*) (** LEVEL 5 **)
    2.35 -by (blast_tac (!claset addSDs [unique_session_keys]) 1);
    2.36 +by (blast_tac (!claset addSEs sees_Spy_partsEs
    2.37 +                       addIs [impOfSubs analz_subset_parts]) 2);
    2.38 +(*Fake*) 
    2.39 +by (spy_analz_tac 1);
    2.40  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    2.41  
    2.42  goal thy 
     3.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 19 11:28:55 1997 +0200
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu Jun 19 11:31:14 1997 +0200
     3.3 @@ -179,10 +179,9 @@
     3.4  by analz_sees_tac;
     3.5  by (REPEAT_FIRST (resolve_tac [allI, impI]));
     3.6  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     3.7 -(*14 seconds*)
     3.8  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     3.9 -(*OR4, Fake*) 
    3.10 -by (EVERY (map spy_analz_tac [3,2]));
    3.11 +(*Fake*) 
    3.12 +by (spy_analz_tac 2);
    3.13  (*Base*)
    3.14  by (Blast_tac 1);
    3.15  qed_spec_mp "analz_image_freshK";
    3.16 @@ -285,16 +284,18 @@
    3.17  by analz_sees_tac;
    3.18  by (ALLGOALS
    3.19      (asm_simp_tac (!simpset addcongs [conj_cong] 
    3.20 -                            addsimps [not_parts_not_analz,
    3.21 -                                      analz_insert_freshK]
    3.22 +                            addsimps [analz_insert_eq, not_parts_not_analz, 
    3.23 +				      analz_insert_freshK]
    3.24                              setloop split_tac [expand_if])));
    3.25 +(*Oops*)
    3.26 +by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    3.27 +(*OR4*) 
    3.28 +by (Blast_tac 3);
    3.29  (*OR3*)
    3.30  by (blast_tac (!claset addSEs sees_Spy_partsEs
    3.31                         addIs [impOfSubs analz_subset_parts]) 2);
    3.32 -(*Oops*) 
    3.33 -by (blast_tac (!claset addDs [unique_session_keys]) 3);
    3.34 -(*OR4, Fake*) 
    3.35 -by (REPEAT_FIRST spy_analz_tac);
    3.36 +(*Fake*) 
    3.37 +by (spy_analz_tac 1);
    3.38  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    3.39  
    3.40  goal thy 
     4.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jun 19 11:28:55 1997 +0200
     4.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jun 19 11:31:14 1997 +0200
     4.3 @@ -181,10 +181,10 @@
     4.4  by (REPEAT_FIRST (resolve_tac [allI, impI]));
     4.5  by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
     4.6  by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
     4.7 +(*Fake*) 
     4.8 +by (spy_analz_tac 2);
     4.9  (*Base*)
    4.10  by (Blast_tac 1);
    4.11 -(*Fake, OR2, OR4*) 
    4.12 -by (REPEAT (spy_analz_tac 1));
    4.13  qed_spec_mp "analz_image_freshK";
    4.14  
    4.15  
    4.16 @@ -238,16 +238,18 @@
    4.17  by analz_sees_tac;
    4.18  by (ALLGOALS
    4.19      (asm_simp_tac (!simpset addcongs [conj_cong] 
    4.20 -                            addsimps [not_parts_not_analz, analz_insert_freshK]
    4.21 +                            addsimps [analz_insert_eq, not_parts_not_analz, 
    4.22 +				      analz_insert_freshK]
    4.23                              setloop split_tac [expand_if])));
    4.24 +(*Oops*)
    4.25 +by (blast_tac (!claset addSDs [unique_session_keys]) 4);
    4.26 +(*OR4*) 
    4.27 +by (Blast_tac 3);
    4.28  (*OR3*)
    4.29 -by (blast_tac (!claset delrules [impCE]
    4.30 -                      addSEs sees_Spy_partsEs
    4.31 -                      addIs [impOfSubs analz_subset_parts]) 3);
    4.32 -(*OR4, OR2, Fake*) 
    4.33 -by (REPEAT_FIRST spy_analz_tac);
    4.34 -(*Oops*) (** LEVEL 5 **)
    4.35 -by (blast_tac (!claset addSDs [unique_session_keys]) 1);
    4.36 +by (blast_tac (!claset addSEs sees_Spy_partsEs
    4.37 +                       addIs [impOfSubs analz_subset_parts]) 2);
    4.38 +(*Fake*) 
    4.39 +by (spy_analz_tac 1);
    4.40  val lemma = result() RS mp RS mp RSN(2,rev_notE);
    4.41  
    4.42  goal thy 
     5.1 --- a/src/HOL/Auth/Recur.ML	Thu Jun 19 11:28:55 1997 +0200
     5.2 +++ b/src/HOL/Auth/Recur.ML	Thu Jun 19 11:31:14 1997 +0200
     5.3 @@ -268,8 +268,8 @@
     5.4       (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
     5.5  (*Base*)
     5.6  by (Blast_tac 1);
     5.7 -(*RA4, RA2, Fake*) 
     5.8 -by (REPEAT (spy_analz_tac 1));
     5.9 +(*Fake*) 
    5.10 +by (spy_analz_tac 1);
    5.11  val raw_analz_image_freshK = result();
    5.12  qed_spec_mp "analz_image_freshK";
    5.13  
     6.1 --- a/src/HOL/Auth/Shared.ML	Thu Jun 19 11:28:55 1997 +0200
     6.2 +++ b/src/HOL/Auth/Shared.ML	Thu Jun 19 11:31:14 1997 +0200
     6.3 @@ -388,10 +388,14 @@
     6.4  by (Blast_tac 1);
     6.5  qed "insert_Key_image";
     6.6  
     6.7 +(*Reverse the normal simplification of "image" to build up (not break down)
     6.8 +  the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
     6.9 +  erase occurrences of forwarded message components (X).*)
    6.10  val analz_image_freshK_ss = 
    6.11       !simpset delsimps [image_insert, image_Un]
    6.12 -              addsimps ([image_insert RS sym, image_Un RS sym,
    6.13 -                         Key_not_used, 
    6.14 +              addsimps ([analz_insert_eq, Key_not_used, 
    6.15 +			 impOfSubs (Un_upper2 RS analz_mono),
    6.16 +                         image_insert RS sym, image_Un RS sym,
    6.17                           insert_Key_singleton, subset_Compl_range,
    6.18                           insert_Key_image, Un_assoc RS sym]
    6.19                          @disj_comms)
     7.1 --- a/src/Provers/blast.ML	Thu Jun 19 11:28:55 1997 +0200
     7.2 +++ b/src/Provers/blast.ML	Thu Jun 19 11:31:14 1997 +0200
     7.3 @@ -1112,8 +1112,7 @@
     7.4  		| cell => Sequence.seqof(fn()=> cell))
     7.5       in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
     7.6       end
     7.7 -     handle Subscript => Sequence.null
     7.8 -	  | PROVE     => Sequence.null);
     7.9 +     handle PROVE     => Sequence.null);
    7.10  
    7.11  fun blast_tac cs = (DEEPEN (1,20) (depth_tac cs) 0);
    7.12