--- a/src/HOL/Auth/Guard/Extensions.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Thu Oct 13 15:49:09 2022 +0100
@@ -306,7 +306,7 @@
"one_step p == \<forall>evs ev. ev#evs \<in> p \<longrightarrow> evs \<in> p"
lemma one_step_Cons [dest]: "\<lbrakk>one_step p; ev#evs \<in> p\<rbrakk> \<Longrightarrow> evs \<in> p"
-by (unfold one_step_def, blast)
+ unfolding one_step_def by (blast)
lemma one_step_app: "\<lbrakk>evs@evs' \<in> p; one_step p; [] \<in> p\<rbrakk> \<Longrightarrow> evs' \<in> p"
by (induct evs, auto)
@@ -320,7 +320,7 @@
lemma has_only_SaysD: "\<lbrakk>ev \<in> set evs; evs \<in> p; has_only_Says p\<rbrakk>
\<Longrightarrow> \<exists>A B X. ev = Says A B X"
-by (unfold has_only_Says_def, blast)
+ unfolding has_only_Says_def by (blast)
lemma in_has_only_Says [dest]: "\<lbrakk>has_only_Says p; evs \<in> p; ev \<in> set evs\<rbrakk>
\<Longrightarrow> \<exists>A B X. ev = Says A B X"
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy Thu Oct 13 15:49:09 2022 +0100
@@ -64,7 +64,7 @@
by (auto simp: Gets_correct_def dest: nsp_has_no_Gets)
lemma nsp_is_one_step [iff]: "one_step nsp"
-by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> nsp" for ev evs, auto)
+ unfolding one_step_def by (clarify, ind_cases "ev#evs \<in> nsp" for ev evs, auto)
lemma nsp_has_only_Says' [rule_format]: "evs \<in> nsp \<Longrightarrow>
ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)"
--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy Thu Oct 13 15:49:09 2022 +0100
@@ -89,7 +89,7 @@
by (auto simp: Gets_correct_def dest: or_has_no_Gets)
lemma or_is_one_step [iff]: "one_step or"
-by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> or" for ev evs, auto)
+ unfolding one_step_def by (clarify, ind_cases "ev#evs \<in> or" for ev evs, auto)
lemma or_has_only_Says' [rule_format]: "evs \<in> or \<Longrightarrow>
ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)"
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Thu Oct 13 15:49:09 2022 +0100
@@ -80,7 +80,7 @@
by (auto simp: Gets_correct_def dest: ya_has_no_Gets)
lemma ya_is_one_step [iff]: "one_step ya"
-by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> ya" for ev evs, auto)
+ unfolding one_step_def by (clarify, ind_cases "ev#evs \<in> ya" for ev evs, auto)
lemma ya_has_only_Says' [rule_format]: "evs \<in> ya \<Longrightarrow>
ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)"
--- a/src/HOL/Auth/Guard/P1.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Guard/P1.thy Thu Oct 13 15:49:09 2022 +0100
@@ -354,7 +354,7 @@
by (auto simp: Gets_correct_def dest: p1_has_no_Gets)
lemma p1_is_one_step [iff]: "one_step p1"
-by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> p1" for ev evs, auto)
+ unfolding one_step_def by (clarify, ind_cases "ev#evs \<in> p1" for ev evs, auto)
lemma p1_has_only_Says' [rule_format]: "evs \<in> p1 \<Longrightarrow>
ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)"
--- a/src/HOL/Auth/Guard/P2.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Guard/P2.thy Thu Oct 13 15:49:09 2022 +0100
@@ -265,7 +265,7 @@
by (auto simp: Gets_correct_def dest: p2_has_no_Gets)
lemma p2_is_one_step [iff]: "one_step p2"
-by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> p2" for ev evs, auto)
+ unfolding one_step_def by (clarify, ind_cases "ev#evs \<in> p2" for ev evs, auto)
lemma p2_has_only_Says' [rule_format]: "evs \<in> p2 \<Longrightarrow>
ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)"
--- a/src/HOL/Auth/Guard/Proto.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy Thu Oct 13 15:49:09 2022 +0100
@@ -164,12 +164,12 @@
lemma freshD: "fresh p R s n Ks evs \<Longrightarrow> (\<exists>evs1 evs2.
evs = evs2 @ ap' s R # evs1 \<and> Nonce n \<notin> used evs1 \<and> R \<in> p \<and> ok evs1 R s
\<and> Nonce n \<in> parts {apm' s R} \<and> apm' s R \<in> guard n Ks)"
-by (unfold fresh_def, blast)
+ unfolding fresh_def by (blast)
lemma freshI [intro]: "\<lbrakk>Nonce n \<notin> used evs1; R \<in> p; Nonce n \<in> parts {apm' s R};
ok evs1 R s; apm' s R \<in> guard n Ks\<rbrakk>
\<Longrightarrow> fresh p R s n Ks (list @ ap' s R # evs1)"
-by (unfold fresh_def, blast)
+ unfolding fresh_def by (blast)
lemma freshI': "\<lbrakk>Nonce n \<notin> used evs1; (l,r) \<in> p;
Nonce n \<in> parts {apm s (msg r)}; ok evs1 (l,r) s; apm s (msg r) \<in> guard n Ks\<rbrakk>
@@ -220,10 +220,10 @@
"safe Ks G \<equiv> \<forall>K. K \<in> Ks \<longrightarrow> Key K \<notin> analz G"
lemma safeD [dest]: "\<lbrakk>safe Ks G; K \<in> Ks\<rbrakk> \<Longrightarrow> Key K \<notin> analz G"
-by (unfold safe_def, blast)
+ unfolding safe_def by (blast)
lemma safe_insert: "safe Ks (insert X G) \<Longrightarrow> safe Ks G"
-by (unfold safe_def, blast)
+ unfolding safe_def by (blast)
lemma Guard_safe: "\<lbrakk>Guard n Ks G; safe Ks G\<rbrakk> \<Longrightarrow> Nonce n \<notin> analz G"
by (blast dest: Guard_invKey)
@@ -238,7 +238,7 @@
lemma preservD: "\<lbrakk>preserv p keys n Ks; evs \<in> tr p; Guard n Ks (spies evs);
safe Ks (spies evs); fresh p R' s' n Ks evs; R \<in> p; ok evs R s;
keys R' s' n evs \<subseteq> Ks\<rbrakk> \<Longrightarrow> apm' s R \<in> guard n Ks"
-by (unfold preserv_def, blast)
+ unfolding preserv_def by (blast)
lemma preservD': "\<lbrakk>preserv p keys n Ks; evs \<in> tr p; Guard n Ks (spies evs);
safe Ks (spies evs); fresh p R' s' n Ks evs; (l,Says A B X) \<in> p;
@@ -253,7 +253,7 @@
lemma monotonD [dest]: "\<lbrakk>keys R' s' n (ev # evs) \<subseteq> Ks; monoton p keys;
ev # evs \<in> tr p\<rbrakk> \<Longrightarrow> keys R' s' n evs \<subseteq> Ks"
-by (unfold monoton_def, blast)
+ unfolding monoton_def by (blast)
subsection\<open>guardedness theorem\<close>
@@ -328,13 +328,13 @@
secret R n s Ks \<in> parts (spies evs); secret R' n' s' Ks \<in> parts (spies evs);
apm' s R \<in> guard (nonce s n) Ks; apm' s' R' \<in> guard (nonce s n) Ks\<rbrakk> \<Longrightarrow>
secret R n s Ks = secret R' n' s' Ks"
-by (unfold uniq_def, blast)
+ unfolding uniq_def by (blast)
definition ord :: "proto \<Rightarrow> (rule \<Rightarrow> rule \<Rightarrow> bool) \<Rightarrow> bool" where
"ord p inff \<equiv> \<forall>R R'. R \<in> p \<longrightarrow> R' \<in> p \<longrightarrow> \<not> inff R R' \<longrightarrow> inff R' R"
lemma ordD: "\<lbrakk>ord p inff; \<not> inff R R'; R \<in> p; R' \<in> p\<rbrakk> \<Longrightarrow> inff R' R"
-by (unfold ord_def, blast)
+ unfolding ord_def by (blast)
definition uniq' :: "proto \<Rightarrow> (rule \<Rightarrow> rule \<Rightarrow> bool) \<Rightarrow> secfun \<Rightarrow> bool" where
"uniq' p inff secret \<equiv> \<forall>evs R R' n n' Ks s s'. R \<in> p \<longrightarrow> R' \<in> p \<longrightarrow>
--- a/src/HOL/Auth/KerberosIV.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/KerberosIV.thy Thu Oct 13 15:49:09 2022 +0100
@@ -304,27 +304,27 @@
ev \<noteq> Says Kas A (Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta,
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace>)\<rbrace>))
\<Longrightarrow> authKeys (ev # evs) = authKeys evs"
-by (unfold authKeys_def, auto)
+ unfolding authKeys_def by (auto)
lemma authKeys_insert:
"authKeys
(Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta,
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace>)\<rbrace>) # evs)
= insert K (authKeys evs)"
-by (unfold authKeys_def, auto)
+ unfolding authKeys_def by (auto)
lemma authKeys_simp:
"K \<in> authKeys
(Says Kas A (Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta,
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace>)\<rbrace>) # evs)
\<Longrightarrow> K = K' | K \<in> authKeys evs"
-by (unfold authKeys_def, auto)
+ unfolding authKeys_def by (auto)
lemma authKeysI:
"Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta,
(Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace>)\<rbrace>) \<in> set evs
\<Longrightarrow> K \<in> authKeys evs"
-by (unfold authKeys_def, auto)
+ unfolding authKeys_def by (auto)
lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs"
by (simp add: authKeys_def, blast)
@@ -1044,7 +1044,7 @@
(with respect to a given trace). *)
lemma Serv_fresh_not_AKcryptSK:
"Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
-by (unfold AKcryptSK_def, blast)
+ unfolding AKcryptSK_def by (blast)
lemma authK_not_AKcryptSK:
"\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
--- a/src/HOL/Auth/KerberosIV_Gets.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/KerberosIV_Gets.thy Thu Oct 13 15:49:09 2022 +0100
@@ -270,27 +270,27 @@
ev \<noteq> Says Kas A (Crypt (shrK A) \<lbrace>akey, Agent Peer, Ta,
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, akey, Ta\<rbrace>)\<rbrace>))
\<Longrightarrow> authKeys (ev # evs) = authKeys evs"
-by (unfold authKeys_def, auto)
+ unfolding authKeys_def by (auto)
lemma authKeys_insert:
"authKeys
(Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Peer, Number Ta,
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K, Number Ta\<rbrace>)\<rbrace>) # evs)
= insert K (authKeys evs)"
-by (unfold authKeys_def, auto)
+ unfolding authKeys_def by (auto)
lemma authKeys_simp:
"K \<in> authKeys
(Says Kas A (Crypt (shrK A) \<lbrace>Key K', Agent Peer, Number Ta,
(Crypt (shrK Peer) \<lbrace>Agent A, Agent Peer, Key K', Number Ta\<rbrace>)\<rbrace>) # evs)
\<Longrightarrow> K = K' | K \<in> authKeys evs"
-by (unfold authKeys_def, auto)
+ unfolding authKeys_def by (auto)
lemma authKeysI:
"Says Kas A (Crypt (shrK A) \<lbrace>Key K, Agent Tgs, Number Ta,
(Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key K, Number Ta\<rbrace>)\<rbrace>) \<in> set evs
\<Longrightarrow> K \<in> authKeys evs"
-by (unfold authKeys_def, auto)
+ unfolding authKeys_def by (auto)
lemma authKeys_used: "K \<in> authKeys evs \<Longrightarrow> Key K \<in> used evs"
by (simp add: authKeys_def, blast)
@@ -905,7 +905,7 @@
(with respect to a given trace). *)
lemma Serv_fresh_not_AKcryptSK:
"Key servK \<notin> used evs \<Longrightarrow> \<not> AKcryptSK authK servK evs"
-by (unfold AKcryptSK_def, blast)
+ unfolding AKcryptSK_def by (blast)
lemma authK_not_AKcryptSK:
"\<lbrakk> Crypt (shrK Tgs) \<lbrace>Agent A, Agent Tgs, Key authK, tk\<rbrace>
--- a/src/HOL/Auth/Message.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Message.thy Thu Oct 13 15:49:09 2022 +0100
@@ -14,7 +14,7 @@
(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
-by blast
+ by blast
type_synonym
key = nat
@@ -78,72 +78,72 @@
text\<open>Monotonicity\<close>
+lemma parts_mono_aux: "\<lbrakk>G \<subseteq> H; x \<in> parts G\<rbrakk> \<Longrightarrow> x \<in> parts H"
+ by (erule parts.induct) (auto dest: parts.Fst parts.Snd parts.Body)
+
lemma parts_mono: "G \<subseteq> H \<Longrightarrow> parts(G) \<subseteq> parts(H)"
-apply auto
-apply (erule parts.induct)
-apply (blast dest: parts.Fst parts.Snd parts.Body)+
-done
+ using parts_mono_aux by blast
text\<open>Equations hold because constructors are injective.\<close>
lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x\<in>A)"
-by auto
+ by auto
lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
-by auto
+ by auto
lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
-by auto
+ by auto
subsubsection\<open>Inverse of keys\<close>
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
-by (metis invKey)
+ by (metis invKey)
subsection\<open>keysFor operator\<close>
lemma keysFor_empty [simp]: "keysFor {} = {}"
-by (unfold keysFor_def, blast)
+ unfolding keysFor_def by (blast)
lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
-by (unfold keysFor_def, blast)
+ unfolding keysFor_def by (blast)
lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
-by (unfold keysFor_def, blast)
+ unfolding keysFor_def by (blast)
text\<open>Monotonicity\<close>
lemma keysFor_mono: "G \<subseteq> H \<Longrightarrow> keysFor(G) \<subseteq> keysFor(H)"
-by (unfold keysFor_def, blast)
+ unfolding keysFor_def by (blast)
lemma keysFor_insert_Agent [simp]: "keysFor (insert (Agent A) H) = keysFor H"
-by (unfold keysFor_def, auto)
+ unfolding keysFor_def by (auto)
lemma keysFor_insert_Nonce [simp]: "keysFor (insert (Nonce N) H) = keysFor H"
-by (unfold keysFor_def, auto)
+ unfolding keysFor_def by (auto)
lemma keysFor_insert_Number [simp]: "keysFor (insert (Number N) H) = keysFor H"
-by (unfold keysFor_def, auto)
+ unfolding keysFor_def by (auto)
lemma keysFor_insert_Key [simp]: "keysFor (insert (Key K) H) = keysFor H"
-by (unfold keysFor_def, auto)
+ unfolding keysFor_def by (auto)
lemma keysFor_insert_Hash [simp]: "keysFor (insert (Hash X) H) = keysFor H"
-by (unfold keysFor_def, auto)
+ unfolding keysFor_def by (auto)
lemma keysFor_insert_MPair [simp]: "keysFor (insert \<lbrace>X,Y\<rbrace> H) = keysFor H"
-by (unfold keysFor_def, auto)
+ unfolding keysFor_def by (auto)
lemma keysFor_insert_Crypt [simp]:
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"
-by (unfold keysFor_def, auto)
+ unfolding keysFor_def by (auto)
lemma keysFor_image_Key [simp]: "keysFor (Key`E) = {}"
-by (unfold keysFor_def, auto)
+ unfolding keysFor_def by (auto)
lemma Crypt_imp_invKey_keysFor: "Crypt K X \<in> H \<Longrightarrow> invKey K \<in> keysFor H"
-by (unfold keysFor_def, blast)
+ unfolding keysFor_def by (blast)
subsection\<open>Inductive relation "parts"\<close>
@@ -627,7 +627,7 @@
lemma keysFor_synth [simp]:
"keysFor (synth H) = keysFor H \<union> invKey`{K. Key K \<in> H}"
-by (unfold keysFor_def, blast)
+ unfolding keysFor_def by (blast)
subsubsection\<open>Combinations of parts, analz and synth\<close>
--- a/src/HOL/Auth/Public.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Public.thy Thu Oct 13 15:49:09 2022 +0100
@@ -95,7 +95,7 @@
by blast
lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)"
-by (unfold symKeys_def, auto)
+ unfolding symKeys_def by (auto)
lemma analz_symKeys_Decrypt:
"\<lbrakk>Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H\<rbrakk>
--- a/src/HOL/Auth/Yahalom.thy Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Yahalom.thy Thu Oct 13 15:49:09 2022 +0100
@@ -332,7 +332,7 @@
"Says Server A
\<lbrace>Crypt (shrK A) \<lbrace>Agent B, Key K, na, Nonce NB\<rbrace>, X\<rbrace>
\<in> set evs \<Longrightarrow> KeyWithNonce K NB evs"
-by (unfold KeyWithNonce_def, blast)
+ unfolding KeyWithNonce_def by (blast)
lemma KeyWithNonce_Says [simp]:
"KeyWithNonce K NB (Says S A X # evs) =
@@ -354,7 +354,7 @@
(with respect to a given trace).\<close>
lemma fresh_not_KeyWithNonce:
"Key K \<notin> used evs \<Longrightarrow> \<not> KeyWithNonce K NB evs"
-by (unfold KeyWithNonce_def, blast)
+ unfolding KeyWithNonce_def by (blast)
text\<open>The Server message associates K with NB' and therefore not with any
other nonce NB.\<close>
@@ -363,7 +363,7 @@
\<in> set evs;
NB \<noteq> NB'; evs \<in> yahalom\<rbrakk>
\<Longrightarrow> \<not> KeyWithNonce K NB evs"
-by (unfold KeyWithNonce_def, blast dest: unique_session_keys)
+ unfolding KeyWithNonce_def by (blast dest: unique_session_keys)
text\<open>The only nonces that can be found with the help of session keys are