# HG changeset patch # User paulson # Date 1261675855 0 # Node ID 9316b8f56d83117f4d0277cd8c20811dd6bd9a37 # Parent 248e1fd702e955061c35b3a3aca210eecef07872 tidied proofs diff -r 248e1fd702e9 -r 9316b8f56d83 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Thu Dec 24 11:05:58 2009 +0100 +++ b/src/HOL/Auth/Message.thy Thu Dec 24 17:30:55 2009 +0000 @@ -197,17 +197,13 @@ by (intro equalityI parts_Un_subset1 parts_Un_subset2) lemma parts_insert: "parts (insert X H) = parts {X} \ parts H" -apply (subst insert_is_Un [of _ H]) -apply (simp only: parts_Un) -done +by (metis insert_is_Un parts_Un) text{*TWO inserts to avoid looping. This rewrite is better than nothing. Not suitable for Addsimps: its behaviour can be strange.*} lemma parts_insert2: "parts (insert X (insert Y H)) = parts {X} \ parts {Y} \ parts H" -apply (simp add: Un_assoc) -apply (simp add: parts_insert [symmetric]) -done +by (metis Un_commute Un_empty_right Un_insert_right insert_is_Un parts_Un) lemma parts_UN_subset1: "(\x\A. parts(H x)) \ parts(\x\A. H x)" by (intro UN_least parts_mono UN_upper) @@ -242,10 +238,7 @@ by blast lemma parts_subset_iff [simp]: "(parts G \ parts H) = (G \ parts H)" -apply (rule iffI) -apply (iprover intro: subset_trans parts_increasing) -apply (frule parts_mono, simp) -done +by (metis equalityE parts_idem parts_increasing parts_mono subset_trans) lemma parts_trans: "[| X\ parts G; G \ parts H |] ==> X\ parts H" by (drule parts_mono, blast) @@ -322,10 +315,10 @@ lemma msg_Nonce_supply: "\N. \n. N\n --> Nonce n \ parts {msg}" apply (induct msg) apply (simp_all (no_asm_simp) add: exI parts_insert2) - txt{*MPair case: blast works out the necessary sum itself!*} - prefer 2 apply auto apply (blast elim!: add_leE) txt{*Nonce case*} -apply (rule_tac x = "N + Suc nat" in exI, auto) +apply (metis Suc_n_not_le_n) +txt{*MPair case: metis works out the necessary sum itself!*} +apply (metis le_trans nat_le_linear) done @@ -374,10 +367,7 @@ lemma parts_analz [simp]: "parts (analz H) = parts H" -apply (rule equalityI) -apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp) -apply (blast intro: analz_increasing [THEN parts_mono, THEN subsetD]) -done +by (metis analz_increasing analz_subset_parts equalityI parts_mono parts_subset_iff) lemma analz_parts [simp]: "analz (parts H) = parts H" apply auto @@ -514,10 +504,7 @@ by blast lemma analz_subset_iff [simp]: "(analz G \ analz H) = (G \ analz H)" -apply (rule iffI) -apply (iprover intro: subset_trans analz_increasing) -apply (frule analz_mono, simp) -done +by (metis analz_idem analz_increasing analz_mono subset_trans) lemma analz_trans: "[| X\ analz G; G \ analz H |] ==> X\ analz H" by (drule analz_mono, blast) @@ -626,10 +613,7 @@ by blast lemma synth_subset_iff [simp]: "(synth G \ synth H) = (G \ synth H)" -apply (rule iffI) -apply (iprover intro: subset_trans synth_increasing) -apply (frule synth_mono, simp add: synth_idem) -done +by (metis equalityE subset_trans synth_idem synth_increasing synth_mono) lemma synth_trans: "[| X\ synth G; G \ synth H |] ==> X\ synth H" by (drule synth_mono, blast) @@ -684,30 +668,26 @@ done lemma analz_synth [simp]: "analz (synth H) = analz H \ synth H" -apply (cut_tac H = "{}" in analz_synth_Un) -apply (simp (no_asm_use)) -done +by (metis Un_empty_right analz_synth_Un) subsubsection{*For reasoning about the Fake rule in traces *} lemma parts_insert_subset_Un: "X\ G ==> parts(insert X H) \ parts G \ parts H" -by (rule subset_trans [OF parts_mono parts_Un_subset2], blast) +by (metis UnCI Un_upper2 insert_subset parts_Un parts_mono) text{*More specifically for Fake. Very occasionally we could do with a version of the form @{term"parts{X} \ synth (analz H) \ parts H"} *} lemma Fake_parts_insert: "X \ synth (analz H) ==> parts (insert X H) \ synth (analz H) \ parts H" -apply (drule parts_insert_subset_Un) -apply (simp (no_asm_use)) -apply blast -done +by (metis Un_commute analz_increasing insert_subset parts_analz parts_mono + parts_synth synth_mono synth_subset_iff) lemma Fake_parts_insert_in_Un: "[|Z \ parts (insert X H); X: synth (analz H)|] - ==> Z \ synth (analz H) \ parts H"; -by (blast dest: Fake_parts_insert [THEN subsetD, dest]) + ==> Z \ synth (analz H) \ parts H" +by (metis Fake_parts_insert set_mp) text{*@{term H} is sometimes @{term"Key ` KK \ spies evs"}, so can't put @{term "G=H"}.*} @@ -715,10 +695,8 @@ "X\ synth (analz G) ==> analz (insert X H) \ synth (analz G) \ analz (G \ H)" apply (rule subsetI) -apply (subgoal_tac "x \ analz (synth (analz G) \ H) ") -prefer 2 apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD]) -apply (simp (no_asm_use)) -apply blast +apply (subgoal_tac "x \ analz (synth (analz G) \ H)", force) +apply (blast intro: analz_mono [THEN [2] rev_subsetD] analz_mono [THEN synth_mono, THEN [2] rev_subsetD]) done lemma analz_conj_parts [simp]: @@ -908,14 +886,8 @@ lemma Fake_analz_eq [simp]: "X \ synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)" -apply (drule Fake_analz_insert[of _ _ "H"]) -apply (simp add: synth_increasing[THEN Un_absorb2]) -apply (drule synth_mono) -apply (simp add: synth_idem) -apply (rule equalityI) -apply (simp add: ); -apply (rule synth_analz_mono, blast) -done +by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute equalityI + subset_insertI synth_analz_mono synth_increasing synth_subset_iff) text{*Two generalizations of @{text analz_insert_eq}*} lemma gen_analz_insert_eq [rule_format]: @@ -930,11 +902,8 @@ done lemma Fake_parts_sing: - "X \ synth (analz H) ==> parts{X} \ synth (analz H) \ parts H"; -apply (rule subset_trans) - apply (erule_tac [2] Fake_parts_insert) -apply (rule parts_mono, blast) -done + "X \ synth (analz H) ==> parts{X} \ synth (analz H) \ parts H" +by (metis Fake_parts_insert empty_subsetI insert_mono parts_mono subset_trans) lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]