Added expand_parts_element macro

Further simplified proofs in NS_public

InductiveVerification/Message.lean

@@ -1,5 +1,6 @@
 import Init.Data.Nat.Lemmas
 import Init.Prelude
+import Lean
 import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Dist
 import Mathlib.Data.Set.Basic
@@ -12,6 +13,8 @@ import Mathlib.Order.Lattice
 import Mathlib.Tactic.ApplyAt
 import Mathlib.Tactic.SimpIntro
 import Mathlib.Tactic.NthRewrite
+open Lean Elab Command Term Meta
+open Parser.Tactic
 
 -- Keys are integers
 abbrev Key := Nat
@@ -351,6 +354,14 @@ lemma parts_element:
   · intro h; apply_rules [ parts_subset_iff.mp, Set.singleton_subset_iff.mpr ]
   · intro h; aapply parts_subset_iff.mpr; simp
 
+/--
+A tactic that expands terms like `X ∈ parts H`
+-/
+syntax (name := expandPartsElement) "expand_parts_element" (ppSpace location) : tactic
+macro_rules
+  | `(tactic| expand_parts_element at $loc) =>
+  `(tactic| rw[parts_element, Set.subset_def] at $loc; simp at $loc)
+
 @[simp]
 lemma parts_insert_Agent {H : Set Msg} {agt : Agent} :
   parts (insert (Agent agt) H) = insert (Agent agt) (parts H) :=
@@ -593,6 +604,16 @@ by
   | snd h ih => exact analz.snd ih
   | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
 
+lemma analz_mono_neg [InvKey] { h : A ⊆ B } :
+  X ∉ analz B → X ∉ analz A
+:= by
+  intro h₁ h₂; apply h₁; aapply analz_mono;
+  
+lemma analz_insert_mono_neg [InvKey] :
+  X ∉ analz (insert Y H) → X ∉ analz H
+:= by
+  apply_rules [ analz_mono_neg, Set.subset_insert ]
+
 -- Making it safe speeds up proofs
 -- @[simp]
 lemma MPair_analz {H : Set Msg} {X Y : Msg} {P : Prop} [InvKey] :
@@ -1597,3 +1618,15 @@ by
   apply subset_trans (b := parts (insert X H))
   · apply parts_mono; simp
   · aapply Fake_parts_insert
+  
+-- Often the result of Fake_parts_sing needs to be applied to a term in a
+-- disjunction
+lemma Fake_parts_sing_helper {A B : Set Msg}
+{ h : A ⊆ B } :
+X ∈ A ∨ h₁ → X ∈ B ∨ h₁
+:= by
+  intro h; cases h <;> try simp_all
+  left; aapply h
+
+attribute [-simp] Key.injEq
+