src/HOL/Auth/OtwayRees_AN.ML
changeset 2375 14539397fc04
parent 2331 d6a56ff0d94e
child 2417 95f275c8476e
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 13 10:18:48 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 13 10:20:55 1996 +0100
     1.3 @@ -151,16 +151,17 @@
     1.4  \                length evs <= length evs' --> \
     1.5  \                newK evs' ~: keysFor (parts (sees lost Spy evs))";
     1.6  by (parts_induct_tac 1);
     1.7 -(*OR1 and OR3*)
     1.8 -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
     1.9 -(*Fake, OR2, OR4: these messages send unknown (X) components*)
    1.10 -by (REPEAT
    1.11 -    (best_tac
    1.12 +(*Fake, OR4: these messages send unknown (X) components*)
    1.13 +by (EVERY
    1.14 +    (map 
    1.15 +     (best_tac
    1.16        (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.17                        impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    1.18                        Suc_leD]
    1.19                 addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
    1.20 -               addss (!simpset)) 1));
    1.21 +               addss (!simpset))) [5,1]));
    1.22 +(*Remaining subgoals*)
    1.23 +by (REPEAT (fast_tac (!claset addDs [Suc_leD] addss (!simpset)) 1));
    1.24  qed_spec_mp "new_keys_not_used";
    1.25  
    1.26  bind_thm ("new_keys_not_analzd",
    1.27 @@ -336,15 +337,14 @@
    1.28  by (etac otway.induct 1);
    1.29  by analz_Fake_tac;
    1.30  by (ALLGOALS
    1.31 -    (asm_full_simp_tac 
    1.32 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
    1.33 -                          analz_insert_Key_newK] @ pushes)
    1.34 -               setloop split_tac [expand_if])));
    1.35 +    (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
    1.36 +				       analz_insert_Key_newK] @ pushes)
    1.37 +		            setloop split_tac [expand_if])));
    1.38  (*OR3*)
    1.39  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    1.40                        addss (!simpset addsimps [parts_insert2])) 2);
    1.41  (*OR4, Fake*) 
    1.42 -by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
    1.43 +by (REPEAT_FIRST spy_analz_tac);
    1.44  (*Oops*) 
    1.45  by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
    1.46  val lemma = result() RS mp RS mp RSN(2,rev_notE);