--- a/src/HOL/SET-Protocol/MessageSET.thy Wed Aug 01 20:25:16 2007 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy Wed Aug 01 21:10:36 2007 +0200
@@ -835,13 +835,8 @@
(*<*)
ML
{*
-val analz_increasing = thm "analz_increasing";
-val analz_subset_parts = thm "analz_subset_parts";
-val parts_analz = thm "parts_analz";
-val analz_parts = thm "analz_parts";
-val analz_insertI = thm "analz_insertI";
-val Fake_parts_insert = thm "Fake_parts_insert";
-val Fake_analz_insert = thm "Fake_analz_insert";
+structure MessageSET =
+struct
(*Prove base case (subgoal i) and simplify others. A typical base case
concerns Crypt K X \<notin> Key`shrK`bad and cannot be proved by rewriting
@@ -859,9 +854,9 @@
Y \<in> parts(insert X H) and Y \<in> analz(insert X H)
*)
val Fake_insert_tac =
- dresolve_tac [impOfSubs Fake_analz_insert,
- impOfSubs Fake_parts_insert] THEN'
- eresolve_tac [asm_rl, thm"synth.Inj"];
+ dresolve_tac [impOfSubs @{thm Fake_analz_insert},
+ impOfSubs @{thm Fake_parts_insert}] THEN'
+ eresolve_tac [asm_rl, @{thm synth.Inj}];
fun Fake_insert_simp_tac ss i =
REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
@@ -870,8 +865,8 @@
(Fake_insert_simp_tac ss 1
THEN
IF_UNSOLVED (Blast.depth_tac
- (cs addIs [analz_insertI,
- impOfSubs analz_subset_parts]) 4 1))
+ (cs addIs [@{thm analz_insertI},
+ impOfSubs @{thm analz_subset_parts}]) 4 1))
(*The explicit claset and simpset arguments help it work with Isar*)
fun gen_spy_analz_tac (cs,ss) i =
@@ -887,6 +882,8 @@
DEPTH_SOLVE (atomic_spy_analz_tac (cs,ss) 1)]) i)
fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
+
+end
*}
(*>*)
@@ -938,17 +935,17 @@
method_setup spy_analz = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
+ Method.SIMPLE_METHOD' (MessageSET.gen_spy_analz_tac (local_clasimpset_of ctxt))) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
+ Method.SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (Fake_insert_simp_tac (local_simpset_of ctxt))) *}
+ Method.SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
"for debugging spy_analz"
end