Streamlined some proofs
authorpaulson
Fri Dec 13 10:20:55 1996 +0100 (1996-12-13)
changeset 237514539397fc04
parent 2374 4148aa5b00a2
child 2376 f5c61fd9b9b6
Streamlined some proofs
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Fri Dec 13 10:18:48 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Fri Dec 13 10:20:55 1996 +0100
     1.3 @@ -165,8 +165,8 @@
     1.4  by (parts_induct_tac 1);
     1.5  by (REPEAT_FIRST (fast_tac (!claset 
     1.6                                addSEs partsEs
     1.7 -                              addSDs  [Says_imp_sees_Spy RS parts.Inj]
     1.8 -                              addEs [leD RS notE]
     1.9 +                              addSDs [Says_imp_sees_Spy RS parts.Inj]
    1.10 +                              addEs  [leD RS notE]
    1.11                                addDs  [impOfSubs analz_subset_parts,
    1.12                                        impOfSubs parts_insert_subset_Un,
    1.13                                        Suc_leD]
    1.14 @@ -257,7 +257,7 @@
    1.15  by (etac otway.induct 1);
    1.16  by analz_Fake_tac;
    1.17  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
    1.18 -by (ALLGOALS (*Takes 14 secs*)
    1.19 +by (ALLGOALS (*Takes 12 secs*)
    1.20      (asm_simp_tac 
    1.21       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
    1.22                           @ pushes)
    1.23 @@ -451,15 +451,14 @@
    1.24  by (etac otway.induct 1);
    1.25  by analz_Fake_tac;
    1.26  by (ALLGOALS
    1.27 -    (asm_full_simp_tac 
    1.28 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
    1.29 -                          analz_insert_Key_newK] @ pushes)
    1.30 -               setloop split_tac [expand_if])));
    1.31 +    (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
    1.32 +				       analz_insert_Key_newK] @ pushes)
    1.33 +		            setloop split_tac [expand_if])));
    1.34  (*OR3*)
    1.35  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    1.36                        addss (!simpset addsimps [parts_insert2])) 3);
    1.37  (*OR4, OR2, Fake*) 
    1.38 -by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
    1.39 +by (REPEAT_FIRST spy_analz_tac);
    1.40  (*Oops*) (** LEVEL 5 **)
    1.41  by (fast_tac (!claset delrules [disjE]
    1.42                        addDs [unique_session_keys] addss (!simpset)) 1);
     2.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 13 10:18:48 1996 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Dec 13 10:20:55 1996 +0100
     2.3 @@ -151,16 +151,17 @@
     2.4  \                length evs <= length evs' --> \
     2.5  \                newK evs' ~: keysFor (parts (sees lost Spy evs))";
     2.6  by (parts_induct_tac 1);
     2.7 -(*OR1 and OR3*)
     2.8 -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
     2.9 -(*Fake, OR2, OR4: these messages send unknown (X) components*)
    2.10 -by (REPEAT
    2.11 -    (best_tac
    2.12 +(*Fake, OR4: these messages send unknown (X) components*)
    2.13 +by (EVERY
    2.14 +    (map 
    2.15 +     (best_tac
    2.16        (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    2.17                        impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    2.18                        Suc_leD]
    2.19                 addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
    2.20 -               addss (!simpset)) 1));
    2.21 +               addss (!simpset))) [5,1]));
    2.22 +(*Remaining subgoals*)
    2.23 +by (REPEAT (fast_tac (!claset addDs [Suc_leD] addss (!simpset)) 1));
    2.24  qed_spec_mp "new_keys_not_used";
    2.25  
    2.26  bind_thm ("new_keys_not_analzd",
    2.27 @@ -336,15 +337,14 @@
    2.28  by (etac otway.induct 1);
    2.29  by analz_Fake_tac;
    2.30  by (ALLGOALS
    2.31 -    (asm_full_simp_tac 
    2.32 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
    2.33 -                          analz_insert_Key_newK] @ pushes)
    2.34 -               setloop split_tac [expand_if])));
    2.35 +    (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
    2.36 +				       analz_insert_Key_newK] @ pushes)
    2.37 +		            setloop split_tac [expand_if])));
    2.38  (*OR3*)
    2.39  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    2.40                        addss (!simpset addsimps [parts_insert2])) 2);
    2.41  (*OR4, Fake*) 
    2.42 -by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
    2.43 +by (REPEAT_FIRST spy_analz_tac);
    2.44  (*Oops*) 
    2.45  by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
    2.46  val lemma = result() RS mp RS mp RSN(2,rev_notE);
     3.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Fri Dec 13 10:18:48 1996 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Fri Dec 13 10:20:55 1996 +0100
     3.3 @@ -336,15 +336,14 @@
     3.4  by (etac otway.induct 1);
     3.5  by analz_Fake_tac;
     3.6  by (ALLGOALS
     3.7 -    (asm_full_simp_tac 
     3.8 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
     3.9 -                          analz_insert_Key_newK] @ pushes)
    3.10 -               setloop split_tac [expand_if])));
    3.11 +    (asm_simp_tac (!simpset addsimps ([not_parts_not_analz,
    3.12 +				       analz_insert_Key_newK] @ pushes)
    3.13 +		            setloop split_tac [expand_if])));
    3.14  (*OR3*)
    3.15  by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl]
    3.16                        addss (!simpset addsimps [parts_insert2])) 3);
    3.17  (*OR4, OR2, Fake*) 
    3.18 -by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
    3.19 +by (REPEAT_FIRST spy_analz_tac);
    3.20  (*Oops*) (** LEVEL 5 **)
    3.21  by (fast_tac (!claset delrules [disjE]
    3.22  		      addDs [unique_session_keys] addss (!simpset)) 1);