--- a/src/HOL/Auth/Message.thy Thu Oct 13 16:09:31 2022 +0100
+++ b/src/HOL/Auth/Message.thy Thu Oct 13 17:19:50 2022 +0100
@@ -820,9 +820,11 @@
(*The key-free part of a set of messages can be removed from the scope of the analz operator.*)
lemma analz_keyfree_into_Un: "\<lbrakk>X \<in> analz (G \<union> H); G \<subseteq> keyfree\<rbrakk> \<Longrightarrow> X \<in> parts G \<union> analz H"
- apply (erule analz.induct, auto dest: parts.Body)
- apply (metis Un_absorb2 keyfree_KeyE parts_Un parts_keyfree UnI2)
- done
+proof (induction rule: analz.induct)
+ case (Decrypt K X)
+ then show ?case
+ by (metis Un_iff analz.Decrypt in_mono keyfree_KeyE parts.Body parts_keyfree parts_mono)
+qed (auto dest: parts.Body)
subsection\<open>Tactics useful for many protocol proofs\<close>
ML
@@ -890,12 +892,14 @@
"X \<in> analz H \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> analz (insert X G) = analz G"
by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
-lemma synth_analz_insert_eq [rule_format]:
- "X \<in> synth (analz H)
- \<Longrightarrow> \<forall>G. H \<subseteq> G \<longrightarrow> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
- apply (erule synth.induct)
- apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
- done
+lemma synth_analz_insert_eq:
+ "\<lbrakk>X \<in> synth (analz H); H \<subseteq> G\<rbrakk>
+ \<Longrightarrow> (Key K \<in> analz (insert X G)) \<longleftrightarrow> (Key K \<in> analz G)"
+proof (induction arbitrary: G rule: synth.induct)
+ case (Inj X)
+ then show ?case
+ using gen_analz_insert_eq by presburger
+qed (simp_all add: subset_eq)
lemma Fake_parts_sing:
"X \<in> synth (analz H) \<Longrightarrow> parts{X} \<subseteq> synth (analz H) \<union> parts H"
--- a/src/HOL/Auth/NS_Public_Bad.thy Thu Oct 13 16:09:31 2022 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Oct 13 17:19:50 2022 +0100
@@ -78,9 +78,7 @@
\<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies evs) \<longrightarrow>
Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
Nonce NA \<in> analz (spies evs)"
-apply (erule ns_public.induct, simp_all)
-apply (blast intro: analz_insertI)+
-done
+ by (induct rule: ns_public.induct) (auto intro: analz_insertI)
(*Unicity for NS1: nonce NA identifies agents A and B*)
@@ -90,9 +88,7 @@
Nonce NA \<notin> analz (spies evs); evs \<in> ns_public\<rbrakk>
\<Longrightarrow> A=A' \<and> B=B'"
apply (erule rev_mp, erule rev_mp, erule rev_mp)
-apply (erule ns_public.induct, simp_all)
-(*Fake, NS1*)
-apply (blast intro!: analz_insertI)+
+apply (erule ns_public.induct, auto intro: analz_insertI)
done
@@ -116,9 +112,7 @@
\<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow>
Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs"
-apply (erule ns_public.induct)
-apply (auto dest: Spy_not_see_NA unique_NA)
-done
+ by (erule ns_public.induct) (auto dest: Spy_not_see_NA unique_NA)
theorem A_trusts_NS2:
"\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs;
@@ -134,10 +128,7 @@
\<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow>
Nonce NA \<notin> analz (spies evs) \<longrightarrow>
Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs"
-apply (erule ns_public.induct, simp_all)
-(*Fake*)
-apply (blast intro!: analz_insertI)
-done
+ by (induction evs rule: ns_public.induct) (use analz_insertI in auto)