# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1666183140 -3600
# Node ID e4fa45571bab69b8382d2207185d7098f39fb0e2
# Parent  b45c8e35231ee11f018b42017f8a77cc4a8965d4
A bit of tidying

diff -r b45c8e35231e -r e4fa45571bab src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Tue Oct 18 15:59:15 2022 +0100
+++ b/src/HOL/Auth/Message.thy	Wed Oct 19 13:39:00 2022 +0100
@@ -86,10 +86,10 @@
 
 
 text\<open>Equations hold because constructors are injective.\<close>
-lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x\<in>A)"
+lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x \<in>A)"
   by auto
 
-lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
+lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x \<in>A)"
   by auto
 
 lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
@@ -110,7 +110,7 @@
 lemma keysFor_Un [simp]: "keysFor (H \<union> H') = keysFor H \<union> keysFor H'"
     unfolding keysFor_def by blast
 
-lemma keysFor_UN [simp]: "keysFor (\<Union>i\<in>A. H i) = (\<Union>i\<in>A. keysFor (H i))"
+lemma keysFor_UN [simp]: "keysFor (\<Union>i \<in>A. H i) = (\<Union>i \<in>A. keysFor (H i))"
     unfolding keysFor_def by blast
 
 text\<open>Monotonicity\<close>
@@ -170,11 +170,11 @@
 lemma parts_empty [simp]: "parts{} = {}"
   using parts_empty_aux by blast
 
-lemma parts_emptyE [elim!]: "X\<in> parts{} \<Longrightarrow> P"
+lemma parts_emptyE [elim!]: "X \<in> parts{} \<Longrightarrow> P"
   by simp
 
 text\<open>WARNING: loops if H = {Y}, therefore must not be repeated!\<close>
-lemma parts_singleton: "X \<in> parts H \<Longrightarrow> \<exists>Y\<in>H. X \<in> parts {Y}"
+lemma parts_singleton: "X \<in> parts H \<Longrightarrow> \<exists>Y \<in>H. X \<in> parts {Y}"
   by (erule parts.induct, fast+)
 
 
@@ -200,20 +200,20 @@
   "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
   by (metis Un_commute Un_empty_right Un_insert_right insert_is_Un parts_Un)
 
-lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
+lemma parts_UN_subset1: "(\<Union>x \<in>A. parts(H x)) \<subseteq> parts(\<Union>x \<in>A. H x)"
   by (intro UN_least parts_mono UN_upper)
 
-lemma parts_UN_subset2: "parts(\<Union>x\<in>A. H x) \<subseteq> (\<Union>x\<in>A. parts(H x))"
+lemma parts_UN_subset2: "parts(\<Union>x \<in>A. H x) \<subseteq> (\<Union>x \<in>A. parts(H x))"
   apply (rule subsetI)
   apply (erule parts.induct, blast+)
   done
 
 lemma parts_UN [simp]:
-  "parts (\<Union>x\<in>A. H x) = (\<Union>x\<in>A. parts (H x))"
+  "parts (\<Union>x \<in>A. H x) = (\<Union>x \<in>A. parts (H x))"
   by (intro equalityI parts_UN_subset1 parts_UN_subset2)
 
 lemma parts_image [simp]:
-  "parts (f ` A) = (\<Union>x\<in>A. parts {f x})"
+  "parts (f ` A) = (\<Union>x \<in>A. parts {f x})"
   apply auto
    apply (metis (mono_tags, opaque_lifting) image_iff parts_singleton)
   apply (metis empty_subsetI image_eqI insert_absorb insert_subset parts_mono)
@@ -234,7 +234,7 @@
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
-lemma parts_partsD [dest!]: "X\<in> parts (parts H) \<Longrightarrow> X\<in> parts H"
+lemma parts_partsD [dest!]: "X \<in> parts (parts H) \<Longrightarrow> X \<in> parts H"
   by (erule parts.induct, blast+)
 
 lemma parts_idem [simp]: "parts (parts H) = parts H"
@@ -243,15 +243,15 @@
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
   by (metis parts_idem parts_increasing parts_mono subset_trans)
 
-lemma parts_trans: "\<lbrakk>X\<in> parts G;  G \<subseteq> parts H\<rbrakk> \<Longrightarrow> X\<in> parts H"
+lemma parts_trans: "\<lbrakk>X \<in> parts G;  G \<subseteq> parts H\<rbrakk> \<Longrightarrow> X \<in> parts H"
   by (metis parts_subset_iff subsetD)
 
 text\<open>Cut\<close>
 lemma parts_cut:
-  "\<lbrakk>Y\<in> parts (insert X G);  X\<in> parts H\<rbrakk> \<Longrightarrow> Y\<in> parts (G \<union> H)" 
+  "\<lbrakk>Y \<in> parts (insert X G);  X \<in> parts H\<rbrakk> \<Longrightarrow> Y \<in> parts (G \<union> H)" 
   by (blast intro: parts_trans) 
 
-lemma parts_cut_eq [simp]: "X\<in> parts H \<Longrightarrow> parts (insert X H) = parts H"
+lemma parts_cut_eq [simp]: "X \<in> parts H \<Longrightarrow> parts (insert X H) = parts H"
   by (metis insert_absorb parts_idem parts_insert)
 
 
@@ -491,7 +491,7 @@
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
-lemma analz_analzD [dest!]: "X\<in> analz (analz H) \<Longrightarrow> X\<in> analz H"
+lemma analz_analzD [dest!]: "X \<in> analz (analz H) \<Longrightarrow> X \<in> analz H"
   by (erule analz.induct, blast+)
 
 lemma analz_idem [simp]: "analz (analz H) = analz H"
@@ -500,11 +500,11 @@
 lemma analz_subset_iff [simp]: "(analz G \<subseteq> analz H) = (G \<subseteq> analz H)"
   by (metis analz_idem analz_increasing analz_mono subset_trans)
 
-lemma analz_trans: "\<lbrakk>X\<in> analz G;  G \<subseteq> analz H\<rbrakk> \<Longrightarrow> X\<in> analz H"
+lemma analz_trans: "\<lbrakk>X \<in> analz G;  G \<subseteq> analz H\<rbrakk> \<Longrightarrow> X \<in> analz H"
   by (drule analz_mono, blast)
 
 text\<open>Cut; Lemma 2 of Lowe\<close>
-lemma analz_cut: "\<lbrakk>Y\<in> analz (insert X H);  X\<in> analz H\<rbrakk> \<Longrightarrow> Y\<in> analz H"
+lemma analz_cut: "\<lbrakk>Y \<in> analz (insert X H);  X \<in> analz H\<rbrakk> \<Longrightarrow> Y \<in> analz H"
   by (erule analz_trans, blast)
 
 (*Cut can be proved easily by induction on
@@ -514,7 +514,7 @@
 text\<open>This rewrite rule helps in the simplification of messages that involve
   the forwarding of unknown components (X).  Without it, removing occurrences
   of X can be very complicated.\<close>
-lemma analz_insert_eq: "X\<in> analz H \<Longrightarrow> analz (insert X H) = analz H"
+lemma analz_insert_eq: "X \<in> analz H \<Longrightarrow> analz (insert X H) = analz H"
   by (metis analz_cut analz_insert_eq_I insert_absorb)
 
 
@@ -541,16 +541,6 @@
    apply (erule analz.induct, blast+)
   done
 
-text\<open>These two are obsolete (with a single Spy) but cost little to prove...\<close>
-lemma analz_UN_analz_lemma:
-  "X\<in> analz (\<Union>i\<in>A. analz (H i)) \<Longrightarrow> X\<in> analz (\<Union>i\<in>A. H i)"
-  apply (erule analz.induct)
-     apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
-  done
-
-lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
-  by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
-
 
 subsection\<open>Inductive relation "synth"\<close>
 
@@ -599,7 +589,7 @@
 
 subsubsection\<open>Idempotence and transitivity\<close>
 
-lemma synth_synthD [dest!]: "X\<in> synth (synth H) \<Longrightarrow> X\<in> synth H"
+lemma synth_synthD [dest!]: "X \<in> synth (synth H) \<Longrightarrow> X \<in> synth H"
   by (erule synth.induct, auto)
 
 lemma synth_idem: "synth (synth H) = synth H"
@@ -608,11 +598,11 @@
 lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
   by (metis subset_trans synth_idem synth_increasing synth_mono)
 
-lemma synth_trans: "\<lbrakk>X\<in> synth G;  G \<subseteq> synth H\<rbrakk> \<Longrightarrow> X\<in> synth H"
+lemma synth_trans: "\<lbrakk>X \<in> synth G;  G \<subseteq> synth H\<rbrakk> \<Longrightarrow> X \<in> synth H"
   by (drule synth_mono, blast)
 
 text\<open>Cut; Lemma 2 of Lowe\<close>
-lemma synth_cut: "\<lbrakk>Y\<in> synth (insert X H);  X\<in> synth H\<rbrakk> \<Longrightarrow> Y\<in> synth H"
+lemma synth_cut: "\<lbrakk>Y \<in> synth (insert X H);  X \<in> synth H\<rbrakk> \<Longrightarrow> Y \<in> synth H"
   by (erule synth_trans, blast)
 
 lemma Crypt_synth_eq [simp]:
@@ -628,25 +618,23 @@
 subsubsection\<open>Combinations of parts, analz and synth\<close>
 
 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
-  apply (rule equalityI)
-   apply (rule subsetI)
-   apply (erule parts.induct)
-      apply (blast intro: synth_increasing [THEN parts_mono, THEN subsetD] 
-      parts.Fst parts.Snd parts.Body)+
-  done
+proof -
+  have "X \<in> parts (synth H) \<Longrightarrow> X \<in> parts H \<union> synth H" for X
+    by (induction X rule: parts.induct) (auto intro: parts.intros)
+  then show ?thesis
+    by (meson parts_increasing parts_mono subsetI antisym sup_least synth_increasing)
+qed
 
 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
-  apply (intro equalityI analz_subset_cong)+
-     apply simp_all
-  done
+  using analz_cong by blast
 
 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
-  apply (rule equalityI)
-   apply (rule subsetI)
-   apply (erule analz.induct)
-      prefer 5 apply (blast intro: analz_mono [THEN [2] rev_subsetD])
-     apply (blast intro: analz.Fst analz.Snd analz.Decrypt)+
-  done
+proof -
+  have "X \<in> analz (synth G \<union> H) \<Longrightarrow> X \<in> analz (G \<union> H) \<union> synth G" for X
+    by (induction X rule: analz.induct) (auto intro: analz.intros)
+  then show ?thesis
+    by (metis analz_subset_iff le_sup_iff subsetI subset_antisym synth_subset_iff)
+qed
 
 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
   by (metis Un_empty_right analz_synth_Un)
@@ -654,7 +642,7 @@
 
 subsubsection\<open>For reasoning about the Fake rule in traces\<close>
 
-lemma parts_insert_subset_Un: "X\<in> G \<Longrightarrow> parts(insert X H) \<subseteq> parts G \<union> parts H"
+lemma parts_insert_subset_Un: "X \<in> G \<Longrightarrow> parts(insert X H) \<subseteq> parts G \<union> parts H"
   by (metis UnCI Un_upper2 insert_subset parts_Un parts_mono)
 
 text\<open>More specifically for Fake. See also \<open>Fake_parts_sing\<close> below\<close>
@@ -672,7 +660,7 @@
 text\<open>\<^term>\<open>H\<close> is sometimes \<^term>\<open>Key ` KK \<union> spies evs\<close>, so can't put 
   \<^term>\<open>G=H\<close>.\<close>
 lemma Fake_analz_insert:
-  "X\<in> synth (analz G) \<Longrightarrow>  
+  "X \<in> synth (analz G) \<Longrightarrow>  
       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
   by (metis UnCI Un_commute Un_upper1 analz_analz_Un analz_mono analz_synth_Un insert_subset)
 
diff -r b45c8e35231e -r e4fa45571bab src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Tue Oct 18 15:59:15 2022 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed Oct 19 13:39:00 2022 +0100
@@ -19,9 +19,9 @@
 by blast
 
 text\<open>Collapses redundant cases in the huge protocol proofs\<close>
-lemmas disj_simps = disj_comms disj_left_absorb disj_assoc 
+lemmas disj_simps = disj_comms disj_left_absorb disj_assoc
 
-text\<open>Effective with assumptions like \<^term>\<open>K \<notin> range pubK\<close> and 
+text\<open>Effective with assumptions like \<^term>\<open>K \<notin> range pubK\<close> and
    \<^term>\<open>K \<notin> invKey`range pubK\<close>\<close>
 lemma notin_image_iff: "(y \<notin> f`I) = (\<forall>i\<in>I. f i \<noteq> y)"
 by blast
@@ -85,7 +85,7 @@
 
 text\<open>The function is indeed injective\<close>
 lemma inj_nat_of_agent: "inj nat_of_agent"
-by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split) 
+by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split)
 
 
 definition
@@ -620,16 +620,6 @@
 apply (erule analz.induct, blast+)
 done
 
-(*These two are obsolete (with a single Spy) but cost little to prove...*)
-lemma analz_UN_analz_lemma:
-     "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
-apply (erule analz.induct)
-apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
-done
-
-lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
-by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
-
 
 subsection\<open>Inductive relation "synth"\<close>
 
@@ -760,7 +750,7 @@
 done
 
 lemma Fake_parts_insert_in_Un:
-     "[|Z \<in> parts (insert X H);  X \<in> synth (analz H)|] 
+     "[|Z \<in> parts (insert X H);  X \<in> synth (analz H)|]
       ==> Z \<in>  synth (analz H) \<union> parts H"
 by (blast dest: Fake_parts_insert [THEN subsetD, dest])