--- a/src/HOL/Auth/Shared.ML Mon Sep 23 18:19:02 1996 +0200
+++ b/src/HOL/Auth/Shared.ML Mon Sep 23 18:19:38 1996 +0200
@@ -145,11 +145,6 @@
by (Fast_tac 1);
qed "sees_Says_subset_insert";
-goal thy "sees A (Notes A' X # evs) <= insert X (sees A evs)";
-by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
-by (Fast_tac 1);
-qed "sees_Notes_subset_insert";
-
goal thy "sees A evs <= sees A (Says A' B X # evs)";
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
by (Fast_tac 1);
@@ -180,7 +175,6 @@
goal thy "X : sees C evs --> \
\ (EX A B. Says A B X : set_of_list evs) | \
-\ (EX A. Notes A X : set_of_list evs) | \
\ (EX A. X = Key (shrK A))";
by (list.induct_tac "evs" 1);
by (ALLGOALS Asm_simp_tac);
@@ -245,3 +239,10 @@
]) i;
+(** Simplifying parts (insert X (sees A evs))
+ = parts {X} Un parts (sees A evs) -- since general case loops*)
+
+val parts_insert_sees =
+ parts_insert |> read_instantiate_sg (sign_of thy) [("H", "sees A evs")]
+ |> standard;
+
--- a/src/HOL/Auth/Shared.thy Mon Sep 23 18:19:02 1996 +0200
+++ b/src/HOL/Auth/Shared.thy Mon Sep 23 18:19:38 1996 +0200
@@ -6,8 +6,6 @@
Theory of Shared Keys (common to all symmetric-key protocols)
Server keys; initial states of agents; new nonces and keys; function "sees"
-
-IS THE Notes constructor needed??
*)
Shared = Message + List +
@@ -33,7 +31,6 @@
datatype (*Messages, and components of agent stores*)
event = Says agent agent msg
- | Notes agent msg
consts
sees1 :: [agent, event] => msg set
@@ -43,7 +40,6 @@
that is sent to it; it must note such things if/when received*)
sees1_Says "sees1 A (Says A' B X) = (if A:{A',Enemy} then {X} else {})"
(*part of A's internal state*)
- sees1_Notes "sees1 A (Notes A' X) = (if A=A' then {X} else {})"
consts
sees :: [agent, event list] => msg set