--- a/src/HOL/Auth/Guard/Proto.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy Thu Oct 13 16:09:31 2022 +0100
@@ -122,7 +122,7 @@
by (unfold has_only_Says'_def is_Says_def, blast)
lemma has_only_Says_tr [simp]: "has_only_Says' p \<Longrightarrow> has_only_Says (tr p)"
-apply (unfold has_only_Says_def)
+unfolding has_only_Says_def
apply (rule allI, rule allI, rule impI)
apply (erule tr.induct)
apply (auto simp: has_only_Says'_def ok_def)
@@ -354,7 +354,7 @@
by (unfold uniq'_def, blast)
lemma uniq'_imp_uniq: "\<lbrakk>uniq' p inff secret; ord p inff\<rbrakk> \<Longrightarrow> uniq p secret"
-apply (unfold uniq_def)
+unfolding uniq_def
apply (rule allI)+
apply (case_tac "inff R R'")
apply (blast dest: uniq'D)
@@ -442,7 +442,7 @@
subsection\<open>guardedness for NSL\<close>
lemma "uniq ns secret \<Longrightarrow> preserv ns keys n Ks"
-apply (unfold preserv_def)
+unfolding preserv_def
apply (rule allI)+
apply (rule impI, rule impI, rule impI, rule impI, rule impI)
apply (erule fresh_ruleD, simp, simp, simp, simp)
--- a/src/HOL/Auth/KerberosIV.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/KerberosIV.thy Thu Oct 13 16:09:31 2022 +0100
@@ -295,7 +295,7 @@
subsection\<open>Lemmas about \<^term>\<open>authKeys\<close>\<close>
lemma authKeys_empty: "authKeys [] = {}"
-apply (unfold authKeys_def)
+unfolding authKeys_def
apply (simp (no_asm))
done
@@ -478,7 +478,7 @@
Ta = CT (before
Says Kas A (Crypt K \<lbrace>Key authK, Agent Peer, Number Ta, authTicket\<rbrace>)
on evs)"
-apply (unfold before_def)
+unfolding before_def
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (simp_all (no_asm) add: authKeys_def authKeys_insert, blast, blast)
@@ -550,7 +550,7 @@
Ts = CT(before
Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, servTicket\<rbrace>)
on evs) "
-apply (unfold before_def)
+unfolding before_def
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (simp_all add: authKeys_insert authKeys_not_insert authKeys_empty authKeys_simp, blast)
@@ -1014,7 +1014,7 @@
lemma AKcryptSKI:
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) \<in> set evs;
evs \<in> kerbIV \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs"
-apply (unfold AKcryptSK_def)
+unfolding AKcryptSK_def
apply (blast dest: Says_Tgs_message_form)
done
@@ -1033,7 +1033,7 @@
lemma Auth_fresh_not_AKcryptSK:
"\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> \<not> AKcryptSK authK servK evs"
-apply (unfold AKcryptSK_def)
+unfolding AKcryptSK_def
apply (erule rev_mp)
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
@@ -1080,7 +1080,7 @@
text\<open>Long term keys are not issued as servKeys\<close>
lemma shrK_not_AKcryptSK:
"evs \<in> kerbIV \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs"
-apply (unfold AKcryptSK_def)
+unfolding AKcryptSK_def
apply (erule kerbIV.induct)
apply (frule_tac [7] K5_msg_in_parts_spies)
apply (frule_tac [5] K3_msg_in_parts_spies, auto)
@@ -1093,7 +1093,7 @@
\<in> set evs;
authK' \<noteq> authK; evs \<in> kerbIV \<rbrakk>
\<Longrightarrow> \<not> AKcryptSK authK' servK evs"
-apply (unfold AKcryptSK_def)
+unfolding AKcryptSK_def
apply (blast dest: unique_servKeys)
done
--- a/src/HOL/Auth/KerberosIV_Gets.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/KerberosIV_Gets.thy Thu Oct 13 16:09:31 2022 +0100
@@ -876,7 +876,7 @@
lemma AKcryptSKI:
"\<lbrakk> Says Tgs A (Crypt authK \<lbrace>Key servK, Agent B, Number Ts, X \<rbrace>) \<in> set evs;
evs \<in> kerbIV_gets \<rbrakk> \<Longrightarrow> AKcryptSK authK servK evs"
-apply (unfold AKcryptSK_def)
+unfolding AKcryptSK_def
apply (blast dest: Says_Tgs_message_form)
done
@@ -894,7 +894,7 @@
lemma Auth_fresh_not_AKcryptSK:
"\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> \<not> AKcryptSK authK servK evs"
-apply (unfold AKcryptSK_def)
+unfolding AKcryptSK_def
apply (erule rev_mp)
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
@@ -948,7 +948,7 @@
text\<open>Long term keys are not issued as servKeys\<close>
lemma shrK_not_AKcryptSK:
"evs \<in> kerbIV_gets \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs"
-apply (unfold AKcryptSK_def)
+unfolding AKcryptSK_def
apply (erule kerbIV_gets.induct)
apply (frule_tac [8] Gets_ticket_parts)
by (frule_tac [6] Gets_ticket_parts, auto)
@@ -960,7 +960,7 @@
\<in> set evs;
authK' \<noteq> authK; evs \<in> kerbIV_gets \<rbrakk>
\<Longrightarrow> \<not> AKcryptSK authK' servK evs"
-apply (unfold AKcryptSK_def)
+unfolding AKcryptSK_def
by (blast dest: unique_servKeys)
text\<open>Equivalently\<close>
--- a/src/HOL/Auth/KerberosV.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/KerberosV.thy Thu Oct 13 16:09:31 2022 +0100
@@ -778,7 +778,7 @@
lemma Auth_fresh_not_AKcryptSK:
"\<lbrakk> Key authK \<notin> used evs; evs \<in> kerbV \<rbrakk>
\<Longrightarrow> \<not> AKcryptSK authK servK evs"
-apply (unfold AKcryptSK_def)
+unfolding AKcryptSK_def
apply (erule rev_mp)
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
@@ -821,7 +821,7 @@
text\<open>Long term keys are not issued as servKeys\<close>
lemma shrK_not_AKcryptSK:
"evs \<in> kerbV \<Longrightarrow> \<not> AKcryptSK K (shrK A) evs"
-apply (unfold AKcryptSK_def)
+unfolding AKcryptSK_def
apply (erule kerbV.induct)
apply (frule_tac [7] Says_ticket_parts)
apply (frule_tac [5] Says_ticket_parts, auto)
--- a/src/HOL/Auth/Kerberos_BAN.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/Kerberos_BAN.thy Thu Oct 13 16:09:31 2022 +0100
@@ -295,7 +295,7 @@
Tk = CT(before
Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
on evs)"
-apply (unfold before_def)
+unfolding before_def
apply (erule rev_mp)
apply (erule bankerberos.induct, simp_all add: takeWhile_tail)
apply auto
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy Thu Oct 13 16:09:31 2022 +0100
@@ -283,7 +283,7 @@
Tk = CT(before
Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>)
on evs)"
-apply (unfold before_def)
+unfolding before_def
apply (erule rev_mp)
apply (erule bankerb_gets.induct, simp_all)
txt\<open>We need this simplification only for Message 2\<close>
--- a/src/HOL/Auth/Message.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/Message.thy Thu Oct 13 16:09:31 2022 +0100
@@ -340,48 +340,42 @@
text\<open>Monotonicity; Lemma 1 of Lowe's paper\<close>
+lemma analz_mono_aux: "\<lbrakk>G \<subseteq> H; X \<in> analz G\<rbrakk> \<Longrightarrow> X \<in> analz H"
+ by (erule analz.induct) (auto dest: analz.Fst analz.Snd)
+
lemma analz_mono: "G\<subseteq>H \<Longrightarrow> analz(G) \<subseteq> analz(H)"
- apply auto
- apply (erule analz.induct)
- apply (auto dest: analz.Fst analz.Snd)
- done
+ using analz_mono_aux by blast
text\<open>Making it safe speeds up proofs\<close>
lemma MPair_analz [elim!]:
"\<lbrakk>\<lbrace>X,Y\<rbrace> \<in> analz H;
- \<lbrakk>X \<in> analz H; Y \<in> analz H\<rbrakk> \<Longrightarrow> P
-\<rbrakk> \<Longrightarrow> P"
+ \<lbrakk>X \<in> analz H; Y \<in> analz H\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by (blast dest: analz.Fst analz.Snd)
lemma analz_increasing: "H \<subseteq> analz(H)"
by blast
+lemma analz_into_parts: "X \<in> analz H \<Longrightarrow> X \<in> parts H"
+ by (erule analz.induct) auto
+
lemma analz_subset_parts: "analz H \<subseteq> parts H"
- apply (rule subsetI)
- apply (erule analz.induct, blast+)
- done
+ using analz_into_parts by blast
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
+lemma analz_parts [simp]: "analz (parts H) = parts H"
+ using analz_subset_parts by blast
lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
lemma parts_analz [simp]: "parts (analz H) = parts H"
- by (metis analz_increasing analz_subset_parts equalityI parts_mono parts_subset_iff)
-
-lemma analz_parts [simp]: "analz (parts H) = parts H"
- apply auto
- apply (erule analz.induct, auto)
- done
+ by (metis analz_increasing analz_subset_parts parts_idem parts_mono subset_antisym)
lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
subsubsection\<open>General equational properties\<close>
lemma analz_empty [simp]: "analz{} = {}"
- apply safe
- apply (erule analz.induct, blast+)
- done
+ using analz_parts by fastforce
text\<open>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\<close>
@@ -423,7 +417,7 @@
lemma analz_insert_Key [simp]:
"K \<notin> keysFor (analz H) \<Longrightarrow>
analz (insert (Key K) H) = insert (Key K) (analz H)"
- apply (unfold keysFor_def)
+ unfolding keysFor_def
apply (rule analz_insert_eq_I)
apply (erule analz.induct, auto)
done
--- a/src/HOL/Auth/Public.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/Public.thy Thu Oct 13 16:09:31 2022 +0100
@@ -255,7 +255,7 @@
that expression is not in normal form.\<close>
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
-apply (unfold keysFor_def)
+unfolding keysFor_def
apply (induct_tac "C")
apply (auto intro: range_eqI)
done
--- a/src/HOL/Auth/Recur.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/Recur.thy Thu Oct 13 16:09:31 2022 +0100
@@ -445,7 +445,7 @@
"\<lbrakk>Hash \<lbrace>Key(shrK A), Agent A, Agent B, NA, P\<rbrace> \<in> parts(spies evs);
A \<notin> bad; evs \<in> recur\<rbrakk>
\<Longrightarrow> Says A B (Hash[Key(shrK A)] \<lbrace>Agent A, Agent B, NA, P\<rbrace>) \<in> set evs"
-apply (unfold HPair_def)
+unfolding HPair_def
apply (erule rev_mp)
apply (erule recur.induct,
drule_tac [6] RA4_parts_spies,
--- a/src/HOL/Auth/Shared.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/Shared.thy Thu Oct 13 16:09:31 2022 +0100
@@ -59,7 +59,7 @@
that expression is not in normal form.\<close>
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
-apply (unfold keysFor_def)
+unfolding keysFor_def
apply (induct_tac "C", auto)
done
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Thu Oct 13 16:00:22 2022 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Thu Oct 13 16:09:31 2022 +0100
@@ -118,7 +118,7 @@
by auto
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}"
-apply (unfold keysFor_def)
+unfolding keysFor_def
apply (induct_tac "C", auto)
done