From 1779f6a685454b719146e78bedc4810b4d847d7d Mon Sep 17 00:00:00 2001 From: Tim Makarios Date: Fri, 12 Jun 2015 16:40:58 +1200 Subject: [PATCH] Proved that constructed_from is transitive --- Communication.thy | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Communication.thy b/Communication.thy index 4b7c1dc..11cedc8 100644 --- a/Communication.thy +++ b/Communication.thy @@ -91,6 +91,24 @@ next by blast qed +lemma constructed_from_transitive: + assumes "constructed_from M' M" + shows "constructed_from M m \ constructed_from M' m" +proof (induction rule: constructed_from.induct) + case constructed_from_self + from assms show "constructed_from M' M" . +next + case (constructed_from_signature a m) + from constructed_from_signature.IH show "constructed_from M' m" by rule +next + case (constructed_from_encrypted a b m) + from constructed_from_encrypted.IH show "constructed_from M' m" by rule +next + case (constructed_from_list m ms) + from constructed_from_list.hyps(1) and constructed_from_list.IH + show "constructed_from M' m" by rule +qed + text {* What can a particular actor learn from a particular message? *} inductive learnable :: "actor \ message \ message \ bool" for a M where identity_learnable: "learnable a M M" -- 2.11.4.GIT