From af31651461702071ec32401b760252fb27b9048d Mon Sep 17 00:00:00 2001
From: Tim Makarios <tjm1983@gmail.com>
Date: Tue, 16 Jun 2015 16:51:00 +1200
Subject: [PATCH] Proved that "events_before h t" is monotonic in t

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

diff --git a/Communication.thy b/Communication.thy
index 11cedc8..f7a0f17 100644
--- a/Communication.thy
+++ b/Communication.thy
@@ -446,6 +446,18 @@ text {* What events occurred before a given time? *}
 definition events_before :: "history \<Rightarrow> time \<Rightarrow> event set" where
   "events_before h t = {e. \<exists> u < t. (e, u) \<in> h}"
 
+lemma events_before_monotonic:
+  assumes "t' \<le> t"
+  shows "events_before h t' \<subseteq> events_before h t"
+proof
+  fix e
+  assume "e \<in> events_before h t'"
+  then obtain t'' where t''t': "t'' < t'" and inh: "(e, t'') \<in> h"
+    by (unfold events_before_def) auto
+  from t''t' and assms have "t'' < t" by simp
+  with inh show "e \<in> events_before h t" by (unfold events_before_def) auto
+qed
+
 text {* What events occurred at a given time? *}
 definition events_at :: "history \<Rightarrow> time \<Rightarrow> event set" where
   "events_at h t = {e. (e, t) \<in> h}"
-- 
2.11.4.GIT