# HG changeset patch # User paulson # Date 1665673771 -3600 # Node ID 64d29ebb7d3de3a97dcb3cfd042ccf1775d6dedd # Parent a6cc15ec45b2f7a70bdef49e16bfb93bdf4f1586 Mostly, removing the unfold method diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/Guard/Proto.thy --- 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 \ 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: "\uniq' p inff secret; ord p inff\ \ 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\guardedness for NSL\ lemma "uniq ns secret \ 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) diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/KerberosIV.thy --- 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\Lemmas about \<^term>\authKeys\\ 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 \Key authK, Agent Peer, Number Ta, authTicket\) 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 \Key servK, Agent B, Number Ts, servTicket\) 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: "\ Says Tgs A (Crypt authK \Key servK, Agent B, Number Ts, X \) \ set evs; evs \ kerbIV \ \ 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: "\ Key authK \ used evs; evs \ kerbIV \ \ \ 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\Long term keys are not issued as servKeys\ lemma shrK_not_AKcryptSK: "evs \ kerbIV \ \ 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 @@ \ set evs; authK' \ authK; evs \ kerbIV \ \ \ AKcryptSK authK' servK evs" -apply (unfold AKcryptSK_def) +unfolding AKcryptSK_def apply (blast dest: unique_servKeys) done diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/KerberosIV_Gets.thy --- 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: "\ Says Tgs A (Crypt authK \Key servK, Agent B, Number Ts, X \) \ set evs; evs \ kerbIV_gets \ \ 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: "\ Key authK \ used evs; evs \ kerbIV_gets \ \ \ 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\Long term keys are not issued as servKeys\ lemma shrK_not_AKcryptSK: "evs \ kerbIV_gets \ \ 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 @@ \ set evs; authK' \ authK; evs \ kerbIV_gets \ \ \ AKcryptSK authK' servK evs" -apply (unfold AKcryptSK_def) +unfolding AKcryptSK_def by (blast dest: unique_servKeys) text\Equivalently\ diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/KerberosV.thy --- 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: "\ Key authK \ used evs; evs \ kerbV \ \ \ 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\Long term keys are not issued as servKeys\ lemma shrK_not_AKcryptSK: "evs \ kerbV \ \ 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) diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/Kerberos_BAN.thy --- 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' \Number Tk, Agent B, Key K, Ticket\) on evs)" -apply (unfold before_def) +unfolding before_def apply (erule rev_mp) apply (erule bankerberos.induct, simp_all add: takeWhile_tail) apply auto diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/Kerberos_BAN_Gets.thy --- 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' \Number Tk, Agent B, Key K, Ticket\) on evs)" -apply (unfold before_def) +unfolding before_def apply (erule rev_mp) apply (erule bankerb_gets.induct, simp_all) txt\We need this simplification only for Message 2\ diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/Message.thy --- 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\Monotonicity; Lemma 1 of Lowe's paper\ +lemma analz_mono_aux: "\G \ H; X \ analz G\ \ X \ analz H" + by (erule analz.induct) (auto dest: analz.Fst analz.Snd) + lemma analz_mono: "G\H \ analz(G) \ analz(H)" - apply auto - apply (erule analz.induct) - apply (auto dest: analz.Fst analz.Snd) - done + using analz_mono_aux by blast text\Making it safe speeds up proofs\ lemma MPair_analz [elim!]: "\\X,Y\ \ analz H; - \X \ analz H; Y \ analz H\ \ P -\ \ P" + \X \ analz H; Y \ analz H\ \ P\ \ P" by (blast dest: analz.Fst analz.Snd) lemma analz_increasing: "H \ analz(H)" by blast +lemma analz_into_parts: "X \ analz H \ X \ parts H" + by (erule analz.induct) auto + lemma analz_subset_parts: "analz H \ 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\General equational properties\ lemma analz_empty [simp]: "analz{} = {}" - apply safe - apply (erule analz.induct, blast+) - done + using analz_parts by fastforce text\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\ @@ -423,7 +417,7 @@ lemma analz_insert_Key [simp]: "K \ keysFor (analz H) \ 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 diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/Public.thy --- 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.\ 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 diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/Recur.thy --- 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 @@ "\Hash \Key(shrK A), Agent A, Agent B, NA, P\ \ parts(spies evs); A \ bad; evs \ recur\ \ Says A B (Hash[Key(shrK A)] \Agent A, Agent B, NA, P\) \ set evs" -apply (unfold HPair_def) +unfolding HPair_def apply (erule rev_mp) apply (erule recur.induct, drule_tac [6] RA4_parts_spies, diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/Shared.thy --- 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.\ lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" -apply (unfold keysFor_def) +unfolding keysFor_def apply (induct_tac "C", auto) done diff -r a6cc15ec45b2 -r 64d29ebb7d3d src/HOL/Auth/Smartcard/Smartcard.thy --- 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