# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1665677990 -3600
# Node ID 61640505795152a7652e776be5fdc76f4745ef88
# Parent  64d29ebb7d3de3a97dcb3cfd042ccf1775d6dedd
Trying to clean up some messy proofs

diff -r 64d29ebb7d3d -r 616405057951 src/HOL/Auth/Message.thy
--- 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"
diff -r 64d29ebb7d3d -r 616405057951 src/HOL/Auth/NS_Public_Bad.thy
--- 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)