# HG changeset patch
# User paulson
# Date 849808649 -3600
# Node ID 41289907faedd1c2cd61f4a92ac4360e5912ea1f
# Parent  95f0d5243c85498247764ef141106e34c307cf85
Moved much common material to Message.ML

diff -r 95f0d5243c85 -r 41289907faed src/HOL/Auth/Shared.ML
--- a/src/HOL/Auth/Shared.ML	Thu Dec 05 18:56:18 1996 +0100
+++ b/src/HOL/Auth/Shared.ML	Thu Dec 05 18:57:29 1996 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Auth/Message
+(*  Title:      HOL/Auth/Shared
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
@@ -9,27 +9,6 @@
 *)
 
 
-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 Shared;
 
 (*Holds because Friend is injective: thus cannot prove for all f*)
@@ -59,11 +38,11 @@
 AddIffs [inj_shrK RS inj_eq];
 AddSDs  [newN_length, newK_length];
 
+Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
+
 (** Rewrites should not refer to  initState(Friend i) 
     -- not in normal form! **)
 
-Addsimps [newK_neq_shrK, newK_neq_shrK RS not_sym];
-
 goal thy "Key (newK evs) ~: parts (initState lost B)";
 by (agent.induct_tac "B" 1);
 by (Auto_tac ());
@@ -186,11 +165,13 @@
                       addss (!simpset)) 1);
 qed "Says_Crypt_not_lost";
 
+(*NEEDED??*)
 goal thy "initState lost C <= Key `` range shrK";
 by (agent.induct_tac "C" 1);
 by (Auto_tac ());
 qed "initState_subset";
 
+(*NEEDED??*)
 goal thy "X : sees lost C evs --> \
 \          (EX A B. Says A B X : set_of_list evs) | (EX A. X = Key (shrK A))";
 by (list.induct_tac "evs" 1);
@@ -226,48 +207,6 @@
 qed_spec_mp "sees_lost_agent_subset_sees_Spy";
 
 
-(** Rewrites to push in Key and Crypt messages, so that other messages can
-    be pulled out using the analz_insert rules **)
-
-fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
-                      insert_commute;
-
-val pushKeys = map (insComm "Key ?K") 
-                  ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"];
-
-val pushCrypts = map (insComm "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;
-
-val pushKey_newK = insComm "Key (newK ?evs)"  "Key (shrK ?C)";
-
-
-(*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;
-
-
 (** Simplifying   parts (insert X (sees lost A evs))
       = parts {X} Un parts (sees lost A evs) -- since general case loops*)
 
@@ -279,6 +218,9 @@
 
 (*** Specialized rewriting for analz_insert_Key_newK ***)
 
+(*Push newK applications in, allowing other keys to be pulled out*)
+val pushKey_newK = insComm thy "Key (newK ?evs)"  "Key (shrK ?C)";
+
 goal thy "!!K. newK evs = invKey K ==> newK evs = K";
 by (rtac (invKey_eq RS iffD1) 1);
 by (Simp_tac 1);
@@ -309,8 +251,3 @@
 \        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
 by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
 qed "analz_image_newK_lemma";
-
-
-(*Useful in many uniqueness proofs*)
-fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
-