simplified/modernized method setup;
authorwenzelm
Tue Apr 26 17:23:21 2011 +0200 (2011-04-26)
changeset 42475f830a72b27ed
parent 42474 8b139b8ee366
child 42476 d0bc1268ef09
simplified/modernized method setup;
doc-src/TutorialI/Protocol/Message.thy
     1.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Tue Apr 26 17:03:13 2011 +0200
     1.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Tue Apr 26 17:23:21 2011 +0200
     1.3 @@ -824,13 +824,6 @@
     1.4  val pushes = @{thms pushes};
     1.5  
     1.6  
     1.7 -(*Prove base case (subgoal i) and simplify others.  A typical base case
     1.8 -  concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
     1.9 -  alone.*)
    1.10 -fun prove_simple_subgoals_tac (cs, ss) i = 
    1.11 -    force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN
    1.12 -    ALLGOALS (asm_simp_tac ss)
    1.13 -
    1.14  (*Analysis of Fake cases.  Also works for messages that forward unknown parts,
    1.15    but this application is no longer necessary if analz_insert_eq is used.
    1.16    Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
    1.17 @@ -849,25 +842,29 @@
    1.18  fun Fake_insert_simp_tac ss i = 
    1.19      REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
    1.20  
    1.21 -fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL
    1.22 -    (Fake_insert_simp_tac ss 1
    1.23 -     THEN
    1.24 -     IF_UNSOLVED (Blast.depth_tac
    1.25 -                  (cs addIs [analz_insertI,
    1.26 -                                   impOfSubs analz_subset_parts]) 4 1))
    1.27 +fun atomic_spy_analz_tac ctxt =
    1.28 +  let val ss = simpset_of ctxt and cs = claset_of ctxt in
    1.29 +    SELECT_GOAL
    1.30 +      (Fake_insert_simp_tac ss 1
    1.31 +       THEN
    1.32 +       IF_UNSOLVED (Blast.depth_tac
    1.33 +                    (cs addIs [analz_insertI,
    1.34 +                                     impOfSubs analz_subset_parts]) 4 1))
    1.35 +  end;
    1.36  
    1.37 -fun spy_analz_tac (cs,ss) i =
    1.38 -  DETERM
    1.39 -   (SELECT_GOAL
    1.40 -     (EVERY 
    1.41 -      [  (*push in occurrences of X...*)
    1.42 -       (REPEAT o CHANGED)
    1.43 -           (res_inst_tac (Simplifier.the_context ss)
    1.44 -            [(("x", 1), "X")] (insert_commute RS ssubst) 1),
    1.45 -       (*...allowing further simplifications*)
    1.46 -       simp_tac ss 1,
    1.47 -       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    1.48 -       DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
    1.49 +fun spy_analz_tac ctxt i =
    1.50 +  let val ss = simpset_of ctxt and cs = claset_of ctxt in
    1.51 +    DETERM
    1.52 +     (SELECT_GOAL
    1.53 +       (EVERY 
    1.54 +        [  (*push in occurrences of X...*)
    1.55 +         (REPEAT o CHANGED)
    1.56 +             (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
    1.57 +         (*...allowing further simplifications*)
    1.58 +         simp_tac ss 1,
    1.59 +         REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
    1.60 +         DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i)
    1.61 +  end;
    1.62  *}
    1.63  
    1.64  text{*By default only @{text o_apply} is built-in.  But in the presence of
    1.65 @@ -915,11 +912,11 @@
    1.66  lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
    1.67  
    1.68  method_setup spy_analz = {*
    1.69 -    Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o clasimpset_of) *}
    1.70 +    Scan.succeed (SIMPLE_METHOD' o spy_analz_tac) *}
    1.71      "for proving the Fake case when analz is involved"
    1.72  
    1.73  method_setup atomic_spy_analz = {*
    1.74 -    Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o clasimpset_of) *}
    1.75 +    Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac) *}
    1.76      "for debugging spy_analz"
    1.77  
    1.78  method_setup Fake_insert_simp = {*