src/HOL/Auth/NS_Public_Bad.ML
changeset 2516 4d68fbe6378b
parent 2497 47de509bdd55
child 2536 1e04eb7f7eb1
     1.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Fri Jan 17 11:50:09 1997 +0100
     1.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Fri Jan 17 12:49:31 1997 +0100
     1.3 @@ -15,7 +15,6 @@
     1.4  
     1.5  proof_timing:=true;
     1.6  HOL_quantifiers := false;
     1.7 -Pretty.setdepth 20;
     1.8  
     1.9  AddIffs [Spy_in_lost];
    1.10  
    1.11 @@ -30,10 +29,7 @@
    1.12  \                     Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs";
    1.13  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.14  by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
    1.15 -by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
    1.16 -by (REPEAT_FIRST (resolve_tac [refl, conjI]));
    1.17 -by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
    1.18 -				    addss (!simpset setsolver safe_solver))));
    1.19 +by possibility_tac;
    1.20  result();
    1.21  
    1.22  
    1.23 @@ -88,9 +84,9 @@
    1.24  
    1.25  
    1.26  fun analz_induct_tac i = 
    1.27 -    etac ns_public.induct i	THEN
    1.28 +    etac ns_public.induct i     THEN
    1.29      ALLGOALS (asm_simp_tac 
    1.30 -	      (!simpset addsimps [not_parts_not_analz]
    1.31 +              (!simpset addsimps [not_parts_not_analz]
    1.32                          setloop split_tac [expand_if]));
    1.33  
    1.34  
    1.35 @@ -110,9 +106,9 @@
    1.36  by (fast_tac (!claset addSEs partsEs) 3);
    1.37  (*Fake*)
    1.38  by (best_tac (!claset addIs [analz_insertI]
    1.39 -		      addDs [impOfSubs analz_subset_parts,
    1.40 -			     impOfSubs Fake_parts_insert]
    1.41 -	              addss (!simpset)) 2);
    1.42 +                      addDs [impOfSubs analz_subset_parts,
    1.43 +                             impOfSubs Fake_parts_insert]
    1.44 +                      addss (!simpset)) 2);
    1.45  (*Base*)
    1.46  by (fast_tac (!claset addss (!simpset)) 1);
    1.47  bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
    1.48 @@ -137,8 +133,8 @@
    1.49  by (step_tac (!claset addSIs [analz_insertI]) 1);
    1.50  by (ex_strip_tac 1);
    1.51  by (best_tac (!claset delrules [conjI]
    1.52 -		      addSDs [impOfSubs Fake_parts_insert]
    1.53 -	              addDs  [impOfSubs analz_subset_parts]
    1.54 +                      addSDs [impOfSubs Fake_parts_insert]
    1.55 +                      addDs  [impOfSubs analz_subset_parts]
    1.56                        addss (!simpset)) 1);
    1.57  val lemma = result();
    1.58  
    1.59 @@ -163,7 +159,7 @@
    1.60                        addEs  [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
    1.61  (*NS1*)
    1.62  by (fast_tac (!claset addSEs partsEs
    1.63 -		      addSDs [Says_imp_sees_Spy' RS parts.Inj]
    1.64 +                      addSDs [Says_imp_sees_Spy' RS parts.Inj]
    1.65                        addIs  [impOfSubs analz_subset_parts]) 2);
    1.66  (*Fake*)
    1.67  by (spy_analz_tac 1);
    1.68 @@ -193,9 +189,9 @@
    1.69  by (fast_tac (!claset addss (!simpset)) 1);
    1.70  by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
    1.71  by (best_tac (!claset addSIs [disjI2]
    1.72 -		      addSDs [impOfSubs Fake_parts_insert]
    1.73 -		      addDs  [impOfSubs analz_subset_parts]
    1.74 -	              addss (!simpset)) 1);
    1.75 +                      addSDs [impOfSubs Fake_parts_insert]
    1.76 +                      addDs  [impOfSubs analz_subset_parts]
    1.77 +                      addss (!simpset)) 1);
    1.78  (*NS2*)
    1.79  by (Step_tac 1);
    1.80  by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
    1.81 @@ -225,10 +221,10 @@
    1.82  by (analz_induct_tac 1);
    1.83  (*Fake*)
    1.84  by (best_tac (!claset addSIs [disjI2]
    1.85 -		      addSDs [impOfSubs Fake_parts_insert]
    1.86 -		      addIs  [analz_insertI]
    1.87 -		      addDs  [impOfSubs analz_subset_parts]
    1.88 -	              addss (!simpset)) 2);
    1.89 +                      addSDs [impOfSubs Fake_parts_insert]
    1.90 +                      addIs  [analz_insertI]
    1.91 +                      addDs  [impOfSubs analz_subset_parts]
    1.92 +                      addss (!simpset)) 2);
    1.93  (*Base*)
    1.94  by (fast_tac (!claset addss (!simpset)) 1);
    1.95  qed_spec_mp "B_trusts_NS1";
    1.96 @@ -257,9 +253,9 @@
    1.97  by (step_tac (!claset addSIs [analz_insertI]) 1);
    1.98  by (ex_strip_tac 1);
    1.99  by (best_tac (!claset delrules [conjI]
   1.100 -	              addSDs [impOfSubs Fake_parts_insert]
   1.101 -	              addDs  [impOfSubs analz_subset_parts] 
   1.102 -	              addss (!simpset)) 1);
   1.103 +                      addSDs [impOfSubs Fake_parts_insert]
   1.104 +                      addDs  [impOfSubs analz_subset_parts] 
   1.105 +                      addss (!simpset)) 1);
   1.106  val lemma = result();
   1.107  
   1.108  goal thy 
   1.109 @@ -316,18 +312,18 @@
   1.110  (*Fake*)
   1.111  by (REPEAT_FIRST (resolve_tac [impI, conjI]));
   1.112  by (fast_tac (!claset addss (!simpset)) 1);
   1.113 -br (ccontr RS disjI2) 1;
   1.114 +by (rtac (ccontr RS disjI2) 1);
   1.115  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1));
   1.116  by (Fast_tac 1);
   1.117  by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   1.118 -	              addDs  [impOfSubs analz_subset_parts] 
   1.119 -	              addss (!simpset)) 1);
   1.120 +                      addDs  [impOfSubs analz_subset_parts] 
   1.121 +                      addss (!simpset)) 1);
   1.122  (*NS3*)
   1.123  by (Step_tac 1);
   1.124  by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT1 (assume_tac 1));
   1.125  by (Fast_tac 1);
   1.126  by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.127 -	              addDs  [unique_NB]) 1);
   1.128 +                      addDs  [unique_NB]) 1);
   1.129  qed_spec_mp "NB_decrypt_imp_A_msg";
   1.130  
   1.131