# HG changeset patch # User paulson # Date 843495578 -7200 # Node ID 1b234f1fd9c74fd42ec3c0c3118b541813406ba2 # Parent d9af64c26be6c1f95c73b11d0b9ff8ceeadf8277 Removal of the Notes constructor diff -r d9af64c26be6 -r 1b234f1fd9c7 src/HOL/Auth/Shared.ML --- 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; + diff -r d9af64c26be6 -r 1b234f1fd9c7 src/HOL/Auth/Shared.thy --- 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