From f80f1cfe895ccc9c0c7327150f3550e7243225b1 Mon Sep 17 00:00:00 2001
From: Tim Makarios <tjm1983@gmail.com>
Date: Wed, 17 Jun 2015 17:00:14 +1200
Subject: [PATCH] Proved list_constructed_from

---
 Communication.thy | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/Communication.thy b/Communication.thy
index fc5f50d..f1945df 100644
--- a/Communication.thy
+++ b/Communication.thy
@@ -124,6 +124,46 @@ next
   thus "m = Encrypted a b M \<or> constructed_from M m" ..
 qed
 
+lemma list_constructed_from:
+  "constructed_from (MessageList ms) m
+  \<Longrightarrow> m = MessageList ms \<or> (\<exists> M \<in> set ms. constructed_from M m)"
+proof (induction rule: constructed_from.induct)
+  case constructed_from_self
+  show "MessageList ms = MessageList ms
+        \<or> (\<exists> M \<in> set ms. constructed_from M (MessageList ms))"
+    by simp
+next
+  case (constructed_from_signature a m)
+  from constructed_from_signature.IH
+    have "\<exists> M \<in> set ms. constructed_from M (Signature a m)"
+      by simp
+  hence "\<exists> M \<in> set ms. constructed_from M m"
+    by (metis constructed_from.constructed_from_signature)
+  thus "m = MessageList ms \<or> (\<exists> M \<in> set ms. constructed_from M m)" ..
+next
+  case (constructed_from_encrypted a b m)
+  from constructed_from_encrypted.IH
+    have "\<exists> M \<in> set ms. constructed_from M (Encrypted a b m)"
+      by simp
+  hence "\<exists> M \<in> set ms. constructed_from M m"
+    by (metis constructed_from.constructed_from_encrypted)
+  thus "m = MessageList ms \<or> (\<exists> M \<in> set ms. constructed_from M m)" ..
+next
+  case (constructed_from_list m ms')
+  from constructed_from_list.IH have "\<exists> M \<in> set ms. constructed_from M m"
+  proof
+    assume "MessageList ms' = MessageList ms"
+    with `m \<in> set ms'` have "m \<in> set ms" by simp
+    with constructed_from_self show "\<exists> M \<in> set ms. constructed_from M m"
+      by blast
+  next
+    assume "\<exists> M \<in> set ms. constructed_from M (MessageList ms')"
+    with `m \<in> set ms'` show "\<exists> M \<in> set ms. constructed_from M m"
+      by (metis constructed_from.constructed_from_list)
+  qed
+  thus "m = MessageList ms \<or> (\<exists> M \<in> set ms. constructed_from M m)" ..
+qed
+
 lemma constructed_from_transitive:
   assumes "constructed_from M' M"
   shows "constructed_from M m \<Longrightarrow> constructed_from M' m"
-- 
2.11.4.GIT