# HG changeset patch # User wenzelm # Date 1303830193 -7200 # Node ID 8b139b8ee3663b29d3b5008d61da3ba8a7346567 # Parent aca720fb393661d79c6594858fc0ea46aac96cfc simplified/modernized method setup; diff -r aca720fb3936 -r 8b139b8ee366 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Tue Apr 26 15:56:15 2011 +0200 +++ b/src/HOL/Auth/Message.thy Tue Apr 26 17:03:13 2011 +0200 @@ -814,16 +814,6 @@ subsection{*Tactics useful for many protocol proofs*} ML {* -structure Message = -struct - -(*Prove base case (subgoal i) and simplify others. A typical base case - concerns Crypt K X \ Key`shrK`bad and cannot be proved by rewriting - alone.*) -fun prove_simple_subgoals_tac (cs, ss) i = - force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN - ALLGOALS (asm_simp_tac ss) - (*Analysis of Fake cases. Also works for messages that forward unknown parts, but this application is no longer necessary if analz_insert_eq is used. Abstraction over i is ESSENTIAL: it delays the dereferencing of claset @@ -842,26 +832,29 @@ fun Fake_insert_simp_tac ss i = REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i; -fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL +fun atomic_spy_analz_tac ctxt = + let val ss = simpset_of ctxt and cs = claset_of ctxt in + SELECT_GOAL (Fake_insert_simp_tac ss 1 THEN IF_UNSOLVED (Blast.depth_tac (cs addIs [@{thm analz_insertI}, impOfSubs @{thm analz_subset_parts}]) 4 1)) + end; -fun spy_analz_tac (cs,ss) i = - DETERM - (SELECT_GOAL - (EVERY - [ (*push in occurrences of X...*) - (REPEAT o CHANGED) - (res_inst_tac (Simplifier.the_context ss) [(("x", 1), "X")] (insert_commute RS ssubst) 1), - (*...allowing further simplifications*) - simp_tac ss 1, - REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), - DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i) - -end +fun spy_analz_tac ctxt i = + let val ss = simpset_of ctxt and cs = claset_of ctxt in + DETERM + (SELECT_GOAL + (EVERY + [ (*push in occurrences of X...*) + (REPEAT o CHANGED) + (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), + (*...allowing further simplifications*) + simp_tac ss 1, + REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), + DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i) + end; *} text{*By default only @{text o_apply} is built-in. But in the presence of @@ -903,15 +896,15 @@ lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] method_setup spy_analz = {* - Scan.succeed (SIMPLE_METHOD' o Message.spy_analz_tac o clasimpset_of) *} + Scan.succeed (SIMPLE_METHOD' o spy_analz_tac) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* - Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o clasimpset_of) *} + Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* - Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o simpset_of) *} + Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o simpset_of) *} "for debugging spy_analz" end diff -r aca720fb3936 -r 8b139b8ee366 src/HOL/SET_Protocol/Message_SET.thy --- a/src/HOL/SET_Protocol/Message_SET.thy Tue Apr 26 15:56:15 2011 +0200 +++ b/src/HOL/SET_Protocol/Message_SET.thy Tue Apr 26 17:03:13 2011 +0200 @@ -837,16 +837,6 @@ (*<*) ML {* -structure MessageSET = -struct - -(*Prove base case (subgoal i) and simplify others. A typical base case - concerns Crypt K X \ Key`shrK`bad and cannot be proved by rewriting - alone.*) -fun prove_simple_subgoals_tac (cs, ss) i = - force_tac (cs, ss addsimps [@{thm image_eq_UN}]) i THEN - ALLGOALS (asm_simp_tac ss) - (*Analysis of Fake cases. Also works for messages that forward unknown parts, but this application is no longer necessary if analz_insert_eq is used. Abstraction over i is ESSENTIAL: it delays the dereferencing of claset @@ -865,27 +855,29 @@ fun Fake_insert_simp_tac ss i = REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i; -fun atomic_spy_analz_tac (cs,ss) = SELECT_GOAL +fun atomic_spy_analz_tac ctxt = + let val ss = simpset_of ctxt and cs = claset_of ctxt in + SELECT_GOAL (Fake_insert_simp_tac ss 1 THEN IF_UNSOLVED (Blast.depth_tac (cs addIs [@{thm analz_insertI}, impOfSubs @{thm analz_subset_parts}]) 4 1)) + end; -fun spy_analz_tac (cs,ss) i = - DETERM - (SELECT_GOAL - (EVERY - [ (*push in occurrences of X...*) - (REPEAT o CHANGED) - (res_inst_tac (Simplifier.the_context ss) - [(("x", 1), "X")] (insert_commute RS ssubst) 1), - (*...allowing further simplifications*) - simp_tac ss 1, - REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), - DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i) - -end +fun spy_analz_tac ctxt i = + let val ss = simpset_of ctxt and cs = claset_of ctxt in + DETERM + (SELECT_GOAL + (EVERY + [ (*push in occurrences of X...*) + (REPEAT o CHANGED) + (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), + (*...allowing further simplifications*) + simp_tac ss 1, + REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), + DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i) + end; *} (*>*) @@ -936,18 +928,15 @@ lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] method_setup spy_analz = {* - Scan.succeed (fn ctxt => - SIMPLE_METHOD' (MessageSET.spy_analz_tac (clasimpset_of ctxt))) *} + Scan.succeed (SIMPLE_METHOD' o spy_analz_tac) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* - Scan.succeed (fn ctxt => - SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (clasimpset_of ctxt))) *} + Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* - Scan.succeed (fn ctxt => - SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (simpset_of ctxt))) *} + Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o simpset_of) *} "for debugging spy_analz" end