# HG changeset patch
# User paulson
# Date 849809018 -3600
# Node ID 00ac25b2791d225f8693eab00f18ad28a61543be
# Parent  6df4488339e4471ce992e003b7fb75f52a0d0a19
Moved much common material to Message.ML

diff -r 6df4488339e4 -r 00ac25b2791d src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Thu Dec 05 19:03:08 1996 +0100
+++ b/src/HOL/Auth/Message.ML	Thu Dec 05 19:03:38 1996 +0100
@@ -7,6 +7,27 @@
 Inductive relations "parts", "analz" and "synth"
 *)
 
+val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
+by (case_tac "P" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
+val expand_case = result();
+
+fun expand_case_tac P i =
+    res_inst_tac [("P",P)] expand_case i THEN
+    Simp_tac (i+1) THEN 
+    Simp_tac i;
+
+
+
+(*GOALS.ML??*)
+fun prlim n = (goals_limit:=n; pr());
+
+(*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
+goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
+by (fast_tac (!claset addEs [equalityE]) 1);
+val subset_range_iff = result();
+
+
 open Message;
 
 
@@ -706,3 +727,48 @@
 (*We do NOT want Crypt... messages broken up in protocols!!*)
 Delrules partsEs;
 
+
+(** Rewrites to push in Key and Crypt messages, so that other messages can
+    be pulled out using the analz_insert rules **)
+
+fun insComm thy x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
+                          insert_commute;
+
+val pushKeys = map (insComm thy "Key ?K") 
+                  ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"];
+
+val pushCrypts = map (insComm thy "Crypt ?X ?K") 
+                    ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"];
+
+(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
+val pushes = pushKeys@pushCrypts;
+
+
+(*No premature instantiation of variables.  For proving weak liveness.*)
+fun safe_solver prems =
+    match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
+    ORELSE' etac FalseE;
+
+(*Analysis of Fake cases and of messages that forward unknown parts
+  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
+  DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
+fun spy_analz_tac i =
+  SELECT_GOAL 
+   (EVERY [  (*push in occurrences of X...*)
+           (REPEAT o CHANGED)
+             (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
+             (*...allowing further simplifications*)
+           simp_tac (!simpset setloop split_tac [expand_if]) 1,
+           REPEAT (resolve_tac [allI,impI,notI] 1),
+           dtac (impOfSubs Fake_analz_insert) 1,
+           eresolve_tac [asm_rl, synth.Inj] 1,
+           Fast_tac 1,
+           Asm_full_simp_tac 1,
+           IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono]) 2 1)
+           ]) i;
+
+
+(*Useful in many uniqueness proofs*)
+fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
+                     assume_tac (i+1);
+