--- a/src/HOL/Auth/Event_lemmas.ML Sat Apr 26 12:38:17 2003 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,232 +0,0 @@
-(* Title: HOL/Auth/Event_lemmas
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-*)
-
-
-val knows_Cons = thm "knows_Cons";
-val used_Nil = thm "used_Nil";
-val used_Cons = thm "used_Cons";
-
-
-(*Inserted by default but later removed. This declaration lets the file
- be re-loaded.*)
-Addsimps [knows_Cons, used_Nil, used_Cons];
-
-(**** Function "knows" ****)
-
-(** Simplifying parts (insert X (knows Spy evs))
- = parts {X} Un parts (knows Spy evs) -- since general case loops*)
-
-bind_thm ("parts_insert_knows_Spy",
- inst "H" "knows Spy evs" parts_insert);
-
-
-val expand_event_case = thm "event.split";
-
-Goal "knows Spy (Says A B X # evs) = insert X (knows Spy evs)";
-by (Simp_tac 1);
-qed "knows_Spy_Says";
-
-(*The point of letting the Spy see "bad" agents' notes is to prevent
- redundant case-splits on whether A=Spy and whether A:bad*)
-Goal "knows Spy (Notes A X # evs) = \
-\ (if A:bad then insert X (knows Spy evs) else knows Spy evs)";
-by (Simp_tac 1);
-qed "knows_Spy_Notes";
-
-Goal "knows Spy (Gets A X # evs) = knows Spy evs";
-by (Simp_tac 1);
-qed "knows_Spy_Gets";
-
-Goal "knows Spy evs <= knows Spy (Says A B X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_Spy_subset_knows_Spy_Says";
-
-Goal "knows Spy evs <= knows Spy (Notes A X # evs)";
-by (Simp_tac 1);
-by (Fast_tac 1);
-qed "knows_Spy_subset_knows_Spy_Notes";
-
-Goal "knows Spy evs <= knows Spy (Gets A X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_Spy_subset_knows_Spy_Gets";
-
-(*Spy sees what is sent on the traffic*)
-Goal "Says A B X : set evs --> X : knows Spy evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Says_imp_knows_Spy";
-
-Goal "Notes A X : set evs --> A: bad --> X : knows Spy evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Notes_imp_knows_Spy";
-
-
-(*Use with addSEs to derive contradictions from old Says events containing
- items known to be fresh*)
-bind_thms ("knows_Spy_partsEs",
- map make_elim [Says_imp_knows_Spy RS parts.Inj, parts.Body]);
-
-Addsimps [knows_Spy_Says, knows_Spy_Notes, knows_Spy_Gets];
-
-
-(*Begin lemmas about agents' knowledge*)
-
-Goal "knows A (Says A B X # evs) = insert X (knows A evs)";
-by (Simp_tac 1);
-qed "knows_Says";
-
-Goal "knows A (Notes A X # evs) = insert X (knows A evs)";
-by (Simp_tac 1);
-qed "knows_Notes";
-
-Goal "A ~= Spy --> knows A (Gets A X # evs) = insert X (knows A evs)";
-by (Simp_tac 1);
-qed "knows_Gets";
-
-
-Goal "knows A evs <= knows A (Says A' B X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_subset_knows_Says";
-
-Goal "knows A evs <= knows A (Notes A' X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_subset_knows_Notes";
-
-Goal "knows A evs <= knows A (Gets A' X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
-qed "knows_subset_knows_Gets";
-
-(*Agents know what they say*)
-Goal "Says A B X : set evs --> X : knows A evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "Says_imp_knows";
-
-(*Agents know what they note*)
-Goal "Notes A X : set evs --> X : knows A evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "Notes_imp_knows";
-
-(*Agents know what they receive*)
-Goal "A ~= Spy --> Gets A X : set evs --> X : knows A evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-qed_spec_mp "Gets_imp_knows_agents";
-
-
-(*What agents DIFFERENT FROM Spy know
- was either said, or noted, or got, or known initially*)
-Goal "[| X : knows A evs; A ~= Spy |] ==> EX B. \
-\ Says A B X : set evs | Gets A X : set evs | Notes A X : set evs | X : initState A";
-by (etac rev_mp 1);
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "knows_imp_Says_Gets_Notes_initState";
-
-(*What the Spy knows -- for the time being --
- was either said or noted, or known initially*)
-Goal "[| X : knows Spy evs |] ==> EX A B. \
-\ Says A B X : set evs | Notes A X : set evs | X : initState Spy";
-by (etac rev_mp 1);
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
-by (Blast_tac 1);
-qed_spec_mp "knows_Spy_imp_Says_Notes_initState";
-
-(*END lemmas about agents' knowledge*)
-
-
-
-(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
-Delsimps [knows_Cons];
-
-
-(*** Fresh nonces ***)
-
-Goal "parts (knows Spy evs) <= used evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [parts_insert_knows_Spy]
- addsplits [expand_event_case])));
-by (ALLGOALS Blast_tac);
-qed "parts_knows_Spy_subset_used";
-
-bind_thm ("usedI", impOfSubs parts_knows_Spy_subset_used);
-AddIs [usedI];
-
-Goal "parts (initState B) <= used evs";
-by (induct_tac "evs" 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [parts_insert_knows_Spy]
- addsplits [expand_event_case])));
-by (ALLGOALS Blast_tac);
-bind_thm ("initState_into_used", impOfSubs (result()));
-
-Goal "used (Says A B X # evs) = parts{X} Un used evs";
-by (Simp_tac 1);
-qed "used_Says";
-Addsimps [used_Says];
-
-Goal "used (Notes A X # evs) = parts{X} Un used evs";
-by (Simp_tac 1);
-qed "used_Notes";
-Addsimps [used_Notes];
-
-Goal "used (Gets A X # evs) = used evs";
-by (Simp_tac 1);
-qed "used_Gets";
-Addsimps [used_Gets];
-
-Goal "used [] <= used evs";
-by (Simp_tac 1);
-by (blast_tac (claset() addIs [initState_into_used]) 1);
-qed "used_nil_subset";
-
-(**** NOTE REMOVAL--laws above are cleaner, as they don't involve "case" ****)
-Delsimps [used_Nil, used_Cons];
-
-
-(*For proving theorems of the form X ~: analz (knows Spy evs) --> P
- New events added by induction to "evs" are discarded. Provided
- this information isn't needed, the proof will be much shorter, since
- it will omit complicated reasoning about analz.*)
-
-bind_thms ("analz_mono_contra",
- [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD,
- knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD,
- knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD]);
-
-val analz_mono_contra_tac =
- let val analz_impI = inst "P" "?Y ~: analz (knows Spy ?evs)" impI
- in
- rtac analz_impI THEN'
- REPEAT1 o
- (dresolve_tac
- [knows_Spy_subset_knows_Spy_Says RS analz_mono RS contra_subsetD,
- knows_Spy_subset_knows_Spy_Notes RS analz_mono RS contra_subsetD,
- knows_Spy_subset_knows_Spy_Gets RS analz_mono RS contra_subsetD])
- THEN'
- mp_tac
- end;
-
-fun Reception_tac i =
- blast_tac (claset() addDs [Says_imp_knows_Spy RS parts.Inj,
- impOfSubs (parts_insert RS equalityD1),
- parts_trans,
- Says_imp_knows_Spy RS analz.Inj,
- impOfSubs analz_mono, analz_cut]
- addIs [less_SucI]) i;
-
-
-(*Compatibility for the old "spies" function*)
-bind_thms ("spies_partsEs", knows_Spy_partsEs);
-bind_thm ("Says_imp_spies", Says_imp_knows_Spy);
-bind_thm ("parts_insert_spies", parts_insert_knows_Spy);