src/HOL/Auth/Message.thy
changeset 24122 fc7f857d33c8
parent 23746 a455e69c31cc
child 26342 0f65fa163304
     1.1 --- a/src/HOL/Auth/Message.thy	Wed Aug 01 19:59:12 2007 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Wed Aug 01 20:25:16 2007 +0200
     1.3 @@ -840,21 +840,8 @@
     1.4  subsection{*Tactics useful for many protocol proofs*}
     1.5  ML
     1.6  {*
     1.7 -val invKey = thm "invKey"
     1.8 -val keysFor_def = thm "keysFor_def"
     1.9 -val HPair_def = thm "HPair_def"
    1.10 -val symKeys_def = thm "symKeys_def"
    1.11 -val parts_mono = thm "parts_mono";
    1.12 -val analz_mono = thm "analz_mono";
    1.13 -val synth_mono = thm "synth_mono";
    1.14 -val analz_increasing = thm "analz_increasing";
    1.15 -
    1.16 -val analz_insertI = thm "analz_insertI";
    1.17 -val analz_subset_parts = thm "analz_subset_parts";
    1.18 -val Fake_parts_insert = thm "Fake_parts_insert";
    1.19 -val Fake_analz_insert = thm "Fake_analz_insert";
    1.20 -val pushes = thms "pushes";
    1.21 -
    1.22 +structure Message =
    1.23 +struct
    1.24  
    1.25  (*Prove base case (subgoal i) and simplify others.  A typical base case
    1.26    concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
    1.27 @@ -872,9 +859,9 @@
    1.28    Y \<in> parts(insert X H)  and  Y \<in> analz(insert X H)
    1.29  *)
    1.30  val Fake_insert_tac = 
    1.31 -    dresolve_tac [impOfSubs Fake_analz_insert,
    1.32 -                  impOfSubs Fake_parts_insert] THEN'
    1.33 -    eresolve_tac [asm_rl, thm"synth.Inj"];
    1.34 +    dresolve_tac [impOfSubs @{thm Fake_analz_insert},
    1.35 +                  impOfSubs @{thm Fake_parts_insert}] THEN'
    1.36 +    eresolve_tac [asm_rl, @{thm synth.Inj}];
    1.37  
    1.38  fun Fake_insert_simp_tac ss i = 
    1.39      REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
    1.40 @@ -883,8 +870,8 @@
    1.41      (Fake_insert_simp_tac ss 1
    1.42       THEN
    1.43       IF_UNSOLVED (Blast.depth_tac
    1.44 -		  (cs addIs [analz_insertI,
    1.45 -				   impOfSubs analz_subset_parts]) 4 1))
    1.46 +		  (cs addIs [@{thm analz_insertI},
    1.47 +				   impOfSubs @{thm analz_subset_parts}]) 4 1))
    1.48  
    1.49  (*The explicit claset and simpset arguments help it work with Isar*)
    1.50  fun gen_spy_analz_tac (cs,ss) i =
    1.51 @@ -900,6 +887,8 @@
    1.52         DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
    1.53  
    1.54  fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
    1.55 +
    1.56 +end
    1.57  *}
    1.58  
    1.59  text{*By default only @{text o_apply} is built-in.  But in the presence of
    1.60 @@ -951,18 +940,17 @@
    1.61  
    1.62  method_setup spy_analz = {*
    1.63      Method.ctxt_args (fn ctxt =>
    1.64 -        Method.SIMPLE_METHOD (gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    1.65 +        Method.SIMPLE_METHOD (Message.gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    1.66      "for proving the Fake case when analz is involved"
    1.67  
    1.68  method_setup atomic_spy_analz = {*
    1.69      Method.ctxt_args (fn ctxt =>
    1.70 -        Method.SIMPLE_METHOD (atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    1.71 +        Method.SIMPLE_METHOD (Message.atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    1.72      "for debugging spy_analz"
    1.73  
    1.74  method_setup Fake_insert_simp = {*
    1.75      Method.ctxt_args (fn ctxt =>
    1.76 -        Method.SIMPLE_METHOD (Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
    1.77 +        Method.SIMPLE_METHOD (Message.Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
    1.78      "for debugging spy_analz"
    1.79  
    1.80 -
    1.81  end