From f0d5e487d19583d69e0b17cc133a900f48fcf844 Mon Sep 17 00:00:00 2001 From: Tim Makarios Date: Fri, 8 May 2015 16:50:23 +1200 Subject: [PATCH] Named constructed_from cases --- Communication.thy | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Communication.thy b/Communication.thy index 75f4681..cf46050 100644 --- a/Communication.thy +++ b/Communication.thy @@ -41,10 +41,13 @@ inductive contains_message :: "message \ message \ bool" text {* If a particular message has been constructed, what other messages must also have been constructed? *} inductive constructed_from :: "message \ message \ bool" for M - where "constructed_from M M" - | "constructed_from M (Signature _ m) \ constructed_from M m" - | "constructed_from M (Encrypted _ _ m) \ constructed_from M m" - | "m \ set ms \ constructed_from M (MessageList ms) + where constructed_from_self: "constructed_from M M" + | constructed_from_signature: + "constructed_from M (Signature _ m) \ constructed_from M m" + | constructed_from_encrypted: + "constructed_from M (Encrypted _ _ m) \ constructed_from M m" + | constructed_from_list: + "m \ set ms \ constructed_from M (MessageList ms) \ constructed_from M m" lemma actor_name_constructed_from: -- 2.11.4.GIT