Streamlined many proofs
authorpaulson
Fri Dec 13 10:18:48 1996 +0100 (1996-12-13)
changeset 23744148aa5b00a2
parent 2373 490ffa16952e
child 2375 14539397fc04
Streamlined many proofs
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Shared.ML
     1.1 --- a/src/HOL/Auth/NS_Public.ML	Fri Dec 13 10:17:35 1996 +0100
     1.2 +++ b/src/HOL/Auth/NS_Public.ML	Fri Dec 13 10:18:48 1996 +0100
     1.3 @@ -114,7 +114,7 @@
     1.4  by (etac ns_public.induct 1);
     1.5  by (ALLGOALS
     1.6      (asm_simp_tac 
     1.7 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
     1.8 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
     1.9                 setloop split_tac [expand_if])));
    1.10  (*NS3*)
    1.11  by (fast_tac (!claset addSEs partsEs
    1.12 @@ -123,13 +123,12 @@
    1.13  by (fast_tac (!claset addSEs partsEs
    1.14                        addEs  [nonce_not_seen_now]) 3);
    1.15  (*Fake*)
    1.16 -by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
    1.17 +by (best_tac (!claset addIs [analz_insertI]
    1.18  		      addDs [impOfSubs analz_subset_parts,
    1.19  			     impOfSubs Fake_parts_insert]
    1.20  	              addss (!simpset)) 2);
    1.21  (*Base*)
    1.22 -by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
    1.23 -                      addss (!simpset)) 1);
    1.24 +by (fast_tac (!claset addss (!simpset)) 1);
    1.25  bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
    1.26  
    1.27  
    1.28 @@ -143,7 +142,7 @@
    1.29  by (etac ns_public.induct 1);
    1.30  by (ALLGOALS 
    1.31      (asm_simp_tac 
    1.32 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
    1.33 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
    1.34                 setloop split_tac [expand_if])));
    1.35  (*NS1*)
    1.36  by (expand_case_tac "NA = ?y" 3 THEN
    1.37 @@ -152,7 +151,7 @@
    1.38  by (fast_tac (!claset addss (!simpset)) 1);
    1.39  (*Fake*)
    1.40  by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
    1.41 -by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
    1.42 +by (step_tac (!claset addSIs [analz_insertI]) 1);
    1.43  by (ex_strip_tac 1);
    1.44  by (best_tac (!claset delrules [conjI]
    1.45  		      addSDs [impOfSubs Fake_parts_insert]
    1.46 @@ -183,7 +182,7 @@
    1.47  by (etac ns_public.induct 1);
    1.48  by (ALLGOALS 
    1.49      (asm_simp_tac 
    1.50 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
    1.51 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
    1.52                 setloop split_tac [expand_if])));
    1.53  (*NS3*)
    1.54  by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
    1.55 @@ -193,7 +192,7 @@
    1.56                        addSDs [new_nonces_not_seen, 
    1.57  			      Says_imp_sees_Spy' RS parts.Inj]) 2);
    1.58  (*Fake*)
    1.59 -by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
    1.60 +by (REPEAT_FIRST spy_analz_tac);
    1.61  (*NS2*)
    1.62  by (Step_tac 1);
    1.63  by (fast_tac (!claset addSEs partsEs
    1.64 @@ -252,12 +251,12 @@
    1.65  by (etac ns_public.induct 1);
    1.66  by (ALLGOALS
    1.67      (asm_simp_tac 
    1.68 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
    1.69 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
    1.70                 setloop split_tac [expand_if])));
    1.71  (*Fake*)
    1.72  by (best_tac (!claset addSIs [disjI2]
    1.73  		      addSDs [impOfSubs Fake_parts_insert]
    1.74 -		      addIs  [impOfSubs (subset_insertI RS analz_mono)]
    1.75 +		      addIs  [analz_insertI]
    1.76  		      addDs  [impOfSubs analz_subset_parts]
    1.77  	              addss (!simpset)) 2);
    1.78  (*Base*)
    1.79 @@ -280,7 +279,7 @@
    1.80  by (etac ns_public.induct 1);
    1.81  by (ALLGOALS 
    1.82      (asm_simp_tac 
    1.83 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
    1.84 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
    1.85                 setloop split_tac [expand_if])));
    1.86  (*NS2*)
    1.87  by (expand_case_tac "NB = ?y" 3 THEN
    1.88 @@ -289,7 +288,7 @@
    1.89  by (fast_tac (!claset addss (!simpset)) 1);
    1.90  (*Fake*)
    1.91  by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
    1.92 -by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
    1.93 +by (step_tac (!claset addSIs [analz_insertI]) 1);
    1.94  by (ex_strip_tac 1);
    1.95  by (best_tac (!claset delrules [conjI]
    1.96  	              addSDs [impOfSubs Fake_parts_insert]
    1.97 @@ -323,7 +322,7 @@
    1.98  by (etac ns_public.induct 1);
    1.99  by (ALLGOALS 
   1.100      (asm_simp_tac 
   1.101 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   1.102 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
   1.103                 setloop split_tac [expand_if])));
   1.104  (*NS3*)
   1.105  by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
   1.106 @@ -333,7 +332,7 @@
   1.107                        addSDs [new_nonces_not_seen, 
   1.108  			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   1.109  (*Fake*)
   1.110 -by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
   1.111 +by (REPEAT_FIRST spy_analz_tac);
   1.112  (*NS2*)
   1.113  by (Step_tac 1);
   1.114  by (fast_tac (!claset addSEs partsEs
     2.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Fri Dec 13 10:17:35 1996 +0100
     2.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Fri Dec 13 10:18:48 1996 +0100
     2.3 @@ -119,7 +119,7 @@
     2.4  by (etac ns_public.induct 1);
     2.5  by (ALLGOALS
     2.6      (asm_simp_tac 
     2.7 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
     2.8 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
     2.9                 setloop split_tac [expand_if])));
    2.10  (*NS3*)
    2.11  by (fast_tac (!claset addSEs partsEs
    2.12 @@ -128,13 +128,12 @@
    2.13  by (fast_tac (!claset addSEs partsEs
    2.14                        addEs  [nonce_not_seen_now]) 3);
    2.15  (*Fake*)
    2.16 -by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
    2.17 +by (best_tac (!claset addIs [analz_insertI]
    2.18  		      addDs [impOfSubs analz_subset_parts,
    2.19  			     impOfSubs Fake_parts_insert]
    2.20  	              addss (!simpset)) 2);
    2.21  (*Base*)
    2.22 -by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]
    2.23 -                      addss (!simpset)) 1);
    2.24 +by (fast_tac (!claset addss (!simpset)) 1);
    2.25  bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp));
    2.26  
    2.27  
    2.28 @@ -148,7 +147,7 @@
    2.29  by (etac ns_public.induct 1);
    2.30  by (ALLGOALS 
    2.31      (asm_simp_tac 
    2.32 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
    2.33 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
    2.34                 setloop split_tac [expand_if])));
    2.35  (*NS1*)
    2.36  by (expand_case_tac "NA = ?y" 3 THEN
    2.37 @@ -157,7 +156,7 @@
    2.38  by (fast_tac (!claset addss (!simpset)) 1);
    2.39  (*Fake*)
    2.40  by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
    2.41 -by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
    2.42 +by (step_tac (!claset addSIs [analz_insertI]) 1);
    2.43  by (ex_strip_tac 1);
    2.44  by (best_tac (!claset delrules [conjI]
    2.45  		      addSDs [impOfSubs Fake_parts_insert]
    2.46 @@ -188,7 +187,7 @@
    2.47  by (etac ns_public.induct 1);
    2.48  by (ALLGOALS 
    2.49      (asm_simp_tac 
    2.50 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
    2.51 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
    2.52                 setloop split_tac [expand_if])));
    2.53  (*NS3*)
    2.54  by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
    2.55 @@ -198,7 +197,7 @@
    2.56                        addSDs [new_nonces_not_seen, 
    2.57  			      Says_imp_sees_Spy' RS parts.Inj]) 2);
    2.58  (*Fake*)
    2.59 -by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
    2.60 +by (REPEAT_FIRST spy_analz_tac);
    2.61  (*NS2*)
    2.62  by (Step_tac 1);
    2.63  by (fast_tac (!claset addSEs partsEs
    2.64 @@ -258,12 +257,12 @@
    2.65  by (etac ns_public.induct 1);
    2.66  by (ALLGOALS
    2.67      (asm_simp_tac 
    2.68 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
    2.69 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
    2.70                 setloop split_tac [expand_if])));
    2.71  (*Fake*)
    2.72  by (best_tac (!claset addSIs [disjI2]
    2.73  		      addSDs [impOfSubs Fake_parts_insert]
    2.74 -		      addIs  [impOfSubs (subset_insertI RS analz_mono)]
    2.75 +		      addIs  [analz_insertI]
    2.76  		      addDs  [impOfSubs analz_subset_parts]
    2.77  	              addss (!simpset)) 2);
    2.78  (*Base*)
    2.79 @@ -285,7 +284,7 @@
    2.80  by (etac ns_public.induct 1);
    2.81  by (ALLGOALS 
    2.82      (asm_simp_tac 
    2.83 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
    2.84 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
    2.85                 setloop split_tac [expand_if])));
    2.86  (*NS2*)
    2.87  by (expand_case_tac "NB = ?y" 3 THEN
    2.88 @@ -294,7 +293,7 @@
    2.89  by (fast_tac (!claset addss (!simpset)) 1);
    2.90  (*Fake*)
    2.91  by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
    2.92 -by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1);
    2.93 +by (step_tac (!claset addSIs [analz_insertI]) 1);
    2.94  by (ex_strip_tac 1);
    2.95  by (best_tac (!claset delrules [conjI]
    2.96  	              addSDs [impOfSubs Fake_parts_insert]
    2.97 @@ -326,14 +325,14 @@
    2.98  by (etac ns_public.induct 1);
    2.99  by (ALLGOALS 
   2.100      (asm_simp_tac 
   2.101 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   2.102 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
   2.103                 setloop split_tac [expand_if])));
   2.104  (*NS1*)
   2.105  by (fast_tac (!claset addSEs partsEs
   2.106                        addSDs [new_nonces_not_seen, 
   2.107  			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   2.108  (*Fake*)
   2.109 -by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
   2.110 +by (REPEAT_FIRST spy_analz_tac);
   2.111  (*NS2 and NS3*)
   2.112  by (Step_tac 1);
   2.113  (*NS2*)
   2.114 @@ -411,14 +410,14 @@
   2.115  by (etac ns_public.induct 1);
   2.116  by (ALLGOALS 
   2.117      (asm_simp_tac 
   2.118 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes)
   2.119 +     (!simpset addsimps ([not_parts_not_analz] @ pushes)
   2.120                 setloop split_tac [expand_if])));
   2.121  (*NS1*)
   2.122  by (fast_tac (!claset addSEs partsEs
   2.123                        addSDs [new_nonces_not_seen, 
   2.124  			      Says_imp_sees_Spy' RS parts.Inj]) 2);
   2.125  (*Fake*)
   2.126 -by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac));
   2.127 +by (REPEAT_FIRST spy_analz_tac);
   2.128  (*NS2 and NS3*)
   2.129  by (Step_tac 1);
   2.130  (*NS2*)
     3.1 --- a/src/HOL/Auth/NS_Shared.ML	Fri Dec 13 10:17:35 1996 +0100
     3.2 +++ b/src/HOL/Auth/NS_Shared.ML	Fri Dec 13 10:18:48 1996 +0100
     3.3 @@ -362,7 +362,7 @@
     3.4  by analz_Fake_tac;
     3.5  by (ALLGOALS 
     3.6      (asm_simp_tac 
     3.7 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
     3.8 +     (!simpset addsimps ([not_parts_not_analz,
     3.9                            analz_insert_Key_newK] @ pushes)
    3.10                 setloop split_tac [expand_if])));
    3.11  (*NS2*)
    3.12 @@ -370,7 +370,7 @@
    3.13                        addEs [Says_imp_old_keys RS less_irrefl]
    3.14                        addss (!simpset)) 2);
    3.15  (*OR4, OR2, Fake*) 
    3.16 -by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
    3.17 +by (REPEAT_FIRST spy_analz_tac);
    3.18  (*NS3 and Oops subcases*) (**LEVEL 7 **)
    3.19  by (step_tac (!claset delrules [impCE]) 1);
    3.20  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);