--- a/doc-src/TutorialI/Protocol/Event_lemmas.ML Wed Dec 13 16:26:45 2006 +0100
+++ b/doc-src/TutorialI/Protocol/Event_lemmas.ML Wed Dec 13 16:32:20 2006 +0100
@@ -41,7 +41,7 @@
qed "knows_Spy_Gets";
Goal "knows Spy evs <= knows Spy (Says A B X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
+by (simp_tac (simpset() addsimps [thm "subset_insertI"]) 1);
qed "knows_Spy_subset_knows_Spy_Says";
Goal "knows Spy evs <= knows Spy (Notes A X # evs)";
@@ -50,7 +50,7 @@
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);
+by (simp_tac (simpset() addsimps [thm "subset_insertI"]) 1);
qed "knows_Spy_subset_knows_Spy_Gets";
(*Spy sees what is sent on the traffic*)
@@ -89,15 +89,15 @@
Goal "knows A evs <= knows A (Says A B X # evs)";
-by (simp_tac (simpset() addsimps [subset_insertI]) 1);
+by (simp_tac (simpset() addsimps [thm "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);
+by (simp_tac (simpset() addsimps [thm "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);
+by (simp_tac (simpset() addsimps [thm "subset_insertI"]) 1);
qed "knows_subset_knows_Gets";
(*Agents know what they say*)
--- a/doc-src/TutorialI/Protocol/Message_lemmas.ML Wed Dec 13 16:26:45 2006 +0100
+++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML Wed Dec 13 16:32:20 2006 +0100
@@ -125,7 +125,7 @@
keysFor_insert_Number, keysFor_insert_Key,
keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
- keysFor_UN RS equalityD1 RS subsetD RS UN_E];
+ keysFor_UN RS equalityD1 RS subsetD RS thm "UN_E"];
Goalw [keysFor_def] "keysFor (Key`E) = {}";
by Auto_tac;
@@ -158,7 +158,7 @@
by (Blast_tac 1);
qed "parts_increasing";
-val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
+val parts_insertI = impOfSubs (thm "subset_insertI" RS parts_mono);
Goal "parts{} = {}";
by Safe_tac;
@@ -182,7 +182,7 @@
(** Unions **)
Goal "parts(G) Un parts(H) \\<subseteq> parts(G Un H)";
-by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
+by (REPEAT (ares_tac [thm "Un_least", parts_mono, thm "Un_upper1", thm "Un_upper2"] 1));
val parts_Un_subset1 = result();
Goal "parts(G Un H) \\<subseteq> parts(G) Un parts(H)";
@@ -196,19 +196,19 @@
qed "parts_Un";
Goal "parts (insert X H) = parts {X} Un parts H";
-by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
+by (stac (read_instantiate [("A","H")] (thm "insert_is_Un")) 1);
by (simp_tac (HOL_ss addsimps [parts_Un]) 1);
qed "parts_insert";
(*TWO inserts to avoid looping. This rewrite is better than nothing.
Not suitable for Addsimps: its behaviour can be strange.*)
Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
-by (simp_tac (simpset() addsimps [Un_assoc]) 1);
+by (simp_tac (simpset() addsimps [thm "Un_assoc"]) 1);
by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1);
qed "parts_insert2";
Goal "(\\<Union>x\\<in>A. parts(H x)) \\<subseteq> parts(\\<Union>x\\<in>A. H x)";
-by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
+by (REPEAT (ares_tac [thm "UN_least", parts_mono, thm "UN_upper"] 1));
val parts_UN_subset1 = result();
Goal "parts(\\<Union>x\\<in>A. H x) \\<subseteq> (\\<Union>x\\<in>A. parts(H x))";
@@ -225,7 +225,7 @@
NOTE: the UN versions are no longer used!*)
Addsimps [parts_Un, parts_UN];
AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
- parts_UN RS equalityD1 RS subsetD RS UN_E];
+ parts_UN RS equalityD1 RS subsetD RS thm "UN_E"];
Goal "insert X (parts H) \\<subseteq> parts(insert X H)";
by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1);
@@ -378,7 +378,7 @@
qed "analz_parts";
Addsimps [analz_parts];
-bind_thm ("analz_insertI", impOfSubs (subset_insertI RS analz_mono));
+bind_thm ("analz_insertI", impOfSubs (thm "subset_insertI" RS analz_mono));
(** General equational properties **)
@@ -392,7 +392,7 @@
(*Converse fails: we can analz more from the union than from the
separate parts, as a key in one might decrypt a message in the other*)
Goal "analz(G) Un analz(H) \\<subseteq> analz(G Un H)";
-by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
+by (REPEAT (ares_tac [thm "Un_least", analz_mono, thm "Un_upper1", thm "Un_upper2"] 1));
qed "analz_Un";
Goal "insert X (analz H) \\<subseteq> analz(insert X H)";
@@ -557,7 +557,7 @@
Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
-by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv]
+by (asm_simp_tac (simpset() addsimps [thm "insert_def"] delsimps [thm "singleton_conv"]
setloop (rtac analz_cong)) 1);
qed "analz_insert_cong";
@@ -591,7 +591,7 @@
(*Converse fails: we can synth more from the union than from the
separate parts, building a compound message using elements of each.*)
Goal "synth(G) Un synth(H) \\<subseteq> synth(G Un H)";
-by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
+by (REPEAT (ares_tac [thm "Un_least", synth_mono, thm "Un_upper1", thm "Un_upper2"] 1));
qed "synth_Un";
Goal "insert X (synth H) \\<subseteq> synth(insert X H)";
--- a/doc-src/TutorialI/Protocol/Public_lemmas.ML Wed Dec 13 16:26:45 2006 +0100
+++ b/doc-src/TutorialI/Protocol/Public_lemmas.ML Wed Dec 13 16:32:20 2006 +0100
@@ -162,9 +162,9 @@
the set of keys. Based on analz_image_freshK_ss, but simpler.*)
val analz_image_keys_ss =
simpset() delsimps [image_insert, image_Un]
- delsimps [imp_disjL] (*reduces blow-up*)
+ delsimps [thm "imp_disjL"] (*reduces blow-up*)
addsimps [image_insert RS sym, image_Un RS sym,
rangeI,
insert_Key_singleton,
- insert_Key_image, Un_assoc RS sym];
+ insert_Key_image, thm "Un_assoc" RS sym];