# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1665672549 -3600
# Node ID b82ac7ef65ecfa97c2b73727cf73a2ea5376dd4c
# Parent  cdc14f94c7548b6f59652ccff03d3105bc172691
Removal of the "unfold" method in favour of "unfolding"

diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/Guard/Extensions.thy
--- 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"
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/Guard/Guard_NS_Public.thy
--- 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)"
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/Guard/Guard_OtwayRees.thy
--- 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)"
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/Guard/Guard_Yahalom.thy
--- 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)"
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/Guard/P1.thy
--- 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)"
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/Guard/P2.thy
--- 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)"
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/Guard/Proto.thy
--- 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>
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/KerberosIV.thy
--- 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>
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/KerberosIV_Gets.thy
--- 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>
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/Message.thy
--- 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>
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/Public.thy
--- 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>  
diff -r cdc14f94c754 -r b82ac7ef65ec src/HOL/Auth/Yahalom.thy
--- 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