better treatment of methods: uses Method.ctxt_args to refer to current
authorpaulson
Fri Apr 27 17:16:21 2001 +0200 (2001-04-27)
changeset 11270a315a3862bb4
parent 11269 4095353bd0d7
child 11271 b2a1d9c20df7
better treatment of methods: uses Method.ctxt_args to refer to current
simpset and claset. Needed to fix problems with Recur.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/Message_lemmas.ML
src/HOL/Auth/Public.thy
src/HOL/Auth/Public_lemmas.ML
src/HOL/Auth/Recur.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Shared_lemmas.ML
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Apr 25 10:31:39 2001 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Fri Apr 27 17:16:21 2001 +0200
     1.3 @@ -143,15 +143,23 @@
     1.4  by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
     1.5  
     1.6  method_setup spy_analz = {*
     1.7 -    Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *}
     1.8 +    Method.ctxt_args (fn ctxt =>
     1.9 +        Method.METHOD (fn facts => 
    1.10 +            gen_spy_analz_tac (Classical.get_local_claset ctxt,
    1.11 +                               Simplifier.get_local_simpset ctxt) 1)) *}
    1.12      "for proving the Fake case when analz is involved"
    1.13  
    1.14  method_setup atomic_spy_analz = {*
    1.15 -    Method.no_args (Method.METHOD (fn facts => atomic_spy_analz_tac 1)) *}
    1.16 +    Method.ctxt_args (fn ctxt =>
    1.17 +        Method.METHOD (fn facts => 
    1.18 +            atomic_spy_analz_tac (Classical.get_local_claset ctxt,
    1.19 +                                  Simplifier.get_local_simpset ctxt) 1)) *}
    1.20      "for debugging spy_analz"
    1.21  
    1.22  method_setup Fake_insert_simp = {*
    1.23 -    Method.no_args (Method.METHOD (fn facts => Fake_insert_simp_tac 1)) *}
    1.24 +    Method.ctxt_args (fn ctxt =>
    1.25 +        Method.METHOD (fn facts =>
    1.26 +            Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
    1.27      "for debugging spy_analz"
    1.28  
    1.29  end
     2.1 --- a/src/HOL/Auth/Message_lemmas.ML	Wed Apr 25 10:31:39 2001 +0200
     2.2 +++ b/src/HOL/Auth/Message_lemmas.ML	Fri Apr 27 17:16:21 2001 +0200
     2.3 @@ -865,8 +865,8 @@
     2.4                    impOfSubs Fake_parts_insert] THEN'
     2.5      eresolve_tac [asm_rl, synth.Inj];
     2.6  
     2.7 -fun Fake_insert_simp_tac i = 
     2.8 -    REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i;
     2.9 +fun Fake_insert_simp_tac ss i = 
    2.10 +    REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
    2.11  
    2.12  
    2.13  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
    2.14 @@ -874,14 +874,15 @@
    2.15    Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
    2.16    DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
    2.17  
    2.18 -val atomic_spy_analz_tac = SELECT_GOAL
    2.19 -    (Fake_insert_simp_tac 1
    2.20 +fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
    2.21 +    (Fake_insert_simp_tac ss 1
    2.22       THEN
    2.23       IF_UNSOLVED (Blast.depth_tac
    2.24 -		  (claset() addIs [analz_insertI,
    2.25 +		  (cs addIs [analz_insertI,
    2.26  				   impOfSubs analz_subset_parts]) 4 1));
    2.27  
    2.28 -fun spy_analz_tac i =
    2.29 +(*The explicit claset and simpset arguments help it work with Isar*)
    2.30 +fun gen_spy_analz_tac (cs,ss) i =
    2.31    DETERM
    2.32     (SELECT_GOAL
    2.33       (EVERY 
    2.34 @@ -889,9 +890,11 @@
    2.35         (REPEAT o CHANGED)
    2.36             (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
    2.37         (*...allowing further simplifications*)
    2.38 -       Simp_tac 1,
    2.39 +       simp_tac ss 1,
    2.40         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    2.41 -       DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i);
    2.42 +       DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i);
    2.43 +
    2.44 +fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i;
    2.45  
    2.46  (*By default only o_apply is built-in.  But in the presence of eta-expansion
    2.47    this means that some terms displayed as (f o g) will be rewritten, and others
     3.1 --- a/src/HOL/Auth/Public.thy	Wed Apr 25 10:31:39 2001 +0200
     3.2 +++ b/src/HOL/Auth/Public.thy	Fri Apr 27 17:16:21 2001 +0200
     3.3 @@ -40,7 +40,9 @@
     3.4  (*Specialized methods*)
     3.5  
     3.6  method_setup possibility = {*
     3.7 -    Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
     3.8 +    Method.ctxt_args (fn ctxt =>
     3.9 +        Method.METHOD (fn facts =>
    3.10 +            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
    3.11      "for proving possibility theorems"
    3.12  
    3.13  end
     4.1 --- a/src/HOL/Auth/Public_lemmas.ML	Wed Apr 25 10:31:39 2001 +0200
     4.2 +++ b/src/HOL/Auth/Public_lemmas.ML	Fri Apr 27 17:16:21 2001 +0200
     4.3 @@ -139,14 +139,16 @@
     4.4  by (Fast_tac 1);
     4.5  qed "Nonce_supply";
     4.6  
     4.7 -(*Tactic for possibility theorems*)
     4.8 -fun possibility_tac st = st |>
     4.9 +(*Tactic for possibility theorems (Isar interface)*)
    4.10 +fun gen_possibility_tac ss state = state |>
    4.11      REPEAT (*omit used_Says so that Nonces start from different traces!*)
    4.12 -    (ALLGOALS (simp_tac (simpset() delsimps [used_Says]))
    4.13 +    (ALLGOALS (simp_tac (ss delsimps [used_Says]))
    4.14       THEN
    4.15       REPEAT_FIRST (eq_assume_tac ORELSE' 
    4.16                     resolve_tac [refl, conjI, Nonce_supply]));
    4.17  
    4.18 +(*Tactic for possibility theorems (ML script version)*)
    4.19 +fun possibility_tac state = gen_possibility_tac (simpset()) state;
    4.20  
    4.21  (*** Specialized rewriting for the analz_image_... theorems ***)
    4.22  
     5.1 --- a/src/HOL/Auth/Recur.thy	Wed Apr 25 10:31:39 2001 +0200
     5.2 +++ b/src/HOL/Auth/Recur.thy	Fri Apr 27 17:16:21 2001 +0200
     5.3 @@ -127,38 +127,44 @@
     5.4  done
     5.5  
     5.6  
     5.7 -(*Case two: Alice, Bob and the server
     5.8 -WHY WON'T INSERT LET VARS REMAIN???
     5.9 +(*Case two: Alice, Bob and the server*)
    5.10  lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
    5.11          Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
    5.12                     END|}  \<in> set evs"
    5.13 -apply (insert Nonce_supply2 Key_supply2)
    5.14 +apply (tactic "cut_facts_tac [Nonce_supply2, Key_supply2] 1")
    5.15  apply clarify
    5.16  apply (intro exI bexI)
    5.17 -apply (rule_tac [2] recur.Nil [THEN recur.RA1, THEN recur.RA2,
    5.18 -                               THEN recur.RA3 [OF _ _ respond.One]])
    5.19 -apply possibility
    5.20 -apply (DEPTH_SOLVE (erule asm_rl less_not_refl2 less_not_refl3))
    5.21 +apply (rule_tac [2] 
    5.22 +          recur.Nil [THEN recur.RA1, 
    5.23 +                     THEN recur.RA2,
    5.24 +                     THEN recur.RA3 [OF _ _ respond.One [THEN respond.Cons]],
    5.25 +                     THEN recur.RA4])
    5.26 +apply (tactic "basic_possibility_tac")
    5.27 +apply (tactic
    5.28 +      "DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
    5.29  done
    5.30 -*)
    5.31  
    5.32  (*Case three: Alice, Bob, Charlie and the server
    5.33 -  TOO SLOW to run every time!
    5.34 -Goal "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
    5.35 +  Rather slow (16 seconds) to run every time...
    5.36 +lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
    5.37          Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
    5.38                     END|}  \<in> set evs"
    5.39 -by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
    5.40 -by (REPEAT (eresolve_tac [exE, conjE] 1));
    5.41 -by (REPEAT (resolve_tac [exI,bexI] 1));
    5.42 -by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS
    5.43 -          (respond.One RS respond.Cons RS respond.Cons RSN
    5.44 -           (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
    5.45 -by basic_possibility_tac;
    5.46 -by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1
    5.47 -		 ORELSE
    5.48 -		 eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1));
    5.49 -result();
    5.50 -****)
    5.51 +apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1")
    5.52 +apply clarify
    5.53 +apply (intro exI bexI)
    5.54 +apply (rule_tac [2] 
    5.55 +          recur.Nil [THEN recur.RA1, 
    5.56 +                     THEN recur.RA2, THEN recur.RA2,
    5.57 +                     THEN recur.RA3 
    5.58 +                          [OF _ _ respond.One 
    5.59 +                                  [THEN respond.Cons, THEN respond.Cons]],
    5.60 +                     THEN recur.RA4, THEN recur.RA4])
    5.61 +apply (tactic "basic_possibility_tac")
    5.62 +apply (tactic
    5.63 +      "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 ORELSE \
    5.64 +\                   eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)")
    5.65 +done
    5.66 +*)
    5.67  
    5.68  (**** Inductive proofs about recur ****)
    5.69  
    5.70 @@ -274,7 +280,8 @@
    5.71  
    5.72  
    5.73  (*Everything that's hashed is already in past traffic. *)
    5.74 -lemma Hash_imp_body: "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
    5.75 +lemma Hash_imp_body:
    5.76 +     "[| Hash {|Key(shrK A), X|} \<in> parts (spies evs);
    5.77           evs \<in> recur;  A \<notin> bad |] ==> X \<in> parts (spies evs)"
    5.78  apply (erule rev_mp)
    5.79  apply (erule recur.induct,
    5.80 @@ -405,11 +412,6 @@
    5.81  done
    5.82  
    5.83  
    5.84 -(*WHAT'S GOING ON??*)
    5.85 -method_setup newbla = {*
    5.86 -    Method.no_args (Method.METHOD (fn facts =>  Blast_tac 1)) *}
    5.87 -    "for debugging spy_analz"
    5.88 -
    5.89  lemma Spy_not_see_session_key:
    5.90       "[| Crypt (shrK A) {|Key K, Agent A', N|} \<in> parts (spies evs);
    5.91           A \<notin> bad;  A' \<notin> bad;  evs \<in> recur |]
    5.92 @@ -423,12 +425,7 @@
    5.93  (*Base*)
    5.94  apply force
    5.95  (*Fake*)
    5.96 -apply (intro allI impI notI conjI iffI)
    5.97 -apply Fake_insert_simp
    5.98 -apply (blast ); 
    5.99 -(*???ASK MARKUS WHY METHOD_SETUP DOESN'T WORK.  Should be just
   5.100  apply spy_analz
   5.101 -*)
   5.102  (*RA2*)
   5.103  apply blast 
   5.104  (*RA3 remains*)
   5.105 @@ -496,7 +493,8 @@
   5.106  apply blast
   5.107  (*RA2: it cannot be a new Nonce, contradiction.*)
   5.108  apply blast
   5.109 -(*RA3*)
   5.110 +(*RA3*) (*Pity that the proof is so brittle: this step requires the rewriting,
   5.111 +          which however would break all other steps.*)
   5.112  apply (simp add: parts_insert_spies, blast)
   5.113  (*RA4*)
   5.114  apply blast
     6.1 --- a/src/HOL/Auth/Shared.thy	Wed Apr 25 10:31:39 2001 +0200
     6.2 +++ b/src/HOL/Auth/Shared.thy	Fri Apr 27 17:16:21 2001 +0200
     6.3 @@ -15,7 +15,7 @@
     6.4    shrK    :: "agent => key"  (*symmetric keys*)
     6.5  
     6.6  axioms
     6.7 -  isSym_keys: "K \\<in> symKeys"	(*All keys are symmetric*)
     6.8 +  isSym_keys: "K \<in> symKeys"	(*All keys are symmetric*)
     6.9    inj_shrK:   "inj shrK"	(*No two agents have the same long-term key*)
    6.10  
    6.11  primrec
    6.12 @@ -38,7 +38,7 @@
    6.13  
    6.14  (*Lets blast_tac perform this step without needing the simplifier*)
    6.15  lemma invKey_shrK_iff [iff]:
    6.16 -     "(Key (invKey K) \\<in> X) = (Key K \\<in> X)"
    6.17 +     "(Key (invKey K) \<in> X) = (Key K \<in> X)"
    6.18  by auto;
    6.19  
    6.20  (*Specialized methods*)
    6.21 @@ -52,7 +52,9 @@
    6.22      "for proving the Session Key Compromise theorem"
    6.23  
    6.24  method_setup possibility = {*
    6.25 -    Method.no_args (Method.METHOD (fn facts => possibility_tac)) *}
    6.26 +    Method.ctxt_args (fn ctxt =>
    6.27 +        Method.METHOD (fn facts =>
    6.28 +            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
    6.29      "for proving possibility theorems"
    6.30  
    6.31  end
     7.1 --- a/src/HOL/Auth/Shared_lemmas.ML	Wed Apr 25 10:31:39 2001 +0200
     7.2 +++ b/src/HOL/Auth/Shared_lemmas.ML	Fri Apr 27 17:16:21 2001 +0200
     7.3 @@ -201,14 +201,17 @@
     7.4  
     7.5  (*Omitting used_Says makes the tactic much faster: it leaves expressions
     7.6      such as  Nonce ?N \\<notin> used evs that match Nonce_supply*)
     7.7 -fun possibility_tac st = st |>
     7.8 +fun gen_possibility_tac ss state = state |>
     7.9     (REPEAT 
    7.10 -    (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] 
    7.11 +    (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets] 
    7.12                           setSolver safe_solver))
    7.13       THEN
    7.14       REPEAT_FIRST (eq_assume_tac ORELSE' 
    7.15                     resolve_tac [refl, conjI, Nonce_supply, Key_supply])));
    7.16  
    7.17 +(*Tactic for possibility theorems (ML script version)*)
    7.18 +fun possibility_tac state = gen_possibility_tac (simpset()) state;
    7.19 +
    7.20  (*For harder protocols (such as Recur) where we have to set up some
    7.21    nonces and keys initially*)
    7.22  fun basic_possibility_tac st = st |>