From 23edf345237fcb562a69d1fd577fbb9bc554153f Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sun, 8 Jan 2017 20:03:39 +0000 Subject: [PATCH] Updated indentation. --- UPF/NormalisationTestSpecification.thy | 68 +++++++++++++------------- UPF/UPF.thy | 13 ++--- 2 files changed, 42 insertions(+), 39 deletions(-) diff --git a/UPF/NormalisationTestSpecification.thy b/UPF/NormalisationTestSpecification.thy index f25862f..70281c1 100644 --- a/UPF/NormalisationTestSpecification.thy +++ b/UPF/NormalisationTestSpecification.thy @@ -5,8 +5,9 @@ * This file is part of HOL-TestGen. * * Copyright (c) 2005-2012 ETH Zurich, Switzerland - * 2008-2014 Achim D. Brucker, Germany - * 2009-2014 Université Paris-Sud, France + * 2008-2015 Achim D. Brucker, Germany + * 2009-2017 Université Paris-Sud, France + * 2015-2017 The University of Sheffield, UK * * All rights reserved. * @@ -38,13 +39,12 @@ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. ******************************************************************************) -(* $Id: NormalisationTestSpecification.thy 10879 2014-10-26 11:35:31Z brucker $ *) section {* Policy Transformation for Testing *} theory NormalisationTestSpecification -imports - Normalisation + imports + Normalisation begin text{* @@ -72,41 +72,43 @@ fun PUTList :: "('a \ 'b) \ 'a \ ('a \ ' lemma distrPUTL1: "x \ dom P \ (list2policy PL) x = P x \ (PUTList PUT x PL \ (PUT x = P x))" apply (induct PL) - apply (auto simp: list2policy_def dom_def) -done + apply (auto simp: list2policy_def dom_def) + done lemma PUTList_None: "x \ dom (list2policy list) \ PUTList PUT x list" apply (induct list) - apply (auto simp: list2policy_def dom_def) -done + apply (auto simp: list2policy_def dom_def) + done lemma PUTList_DomMT: "(\y\set list. dom a \ dom y = {}) \ x \ (dom a) \ x \ dom (list2policy list)" apply (induct list) - apply (auto simp: dom_def list2policy_def) -done + apply (auto simp: dom_def list2policy_def) + done lemma distrPUTL2: "x \ dom P \ (list2policy PL) x = P x \ disjDom PL \ (PUT x = P x) \ PUTList PUT x PL " apply (induct PL) - apply (simp_all add: list2policy_def) - apply (auto) - apply (case_tac "x \ dom a") - apply (case_tac "list2policy PL x = P x") - apply (simp add: list2policy_def) - apply (rule PUTList_None) - apply (rule_tac a = a in PUTList_DomMT) - apply (simp_all add: list2policy_def dom_def) -done + apply (simp_all add: list2policy_def) + apply (auto)[1] + subgoal for a PL p + apply (case_tac "x \ dom a") + apply (case_tac "list2policy PL x = P x") + apply (simp add: list2policy_def) + apply (rule PUTList_None) + apply (rule_tac a = a in PUTList_DomMT) + apply (simp_all add: list2policy_def dom_def) + done + done lemma distrPUTL: "\x \ dom P; (list2policy PL) x = P x; disjDom PL\ \ (PUT x = P x) = PUTList PUT x PL " apply (rule iffI) - apply (rule distrPUTL2) - apply (simp_all) + apply (rule distrPUTL2) + apply (simp_all) apply (rule_tac PL = PL in distrPUTL1) - apply (auto) -done + apply (auto) + done text{* It makes sense to cater for the common special case where the normalisation returns a list @@ -115,7 +117,7 @@ text{* *} fun gatherDomain_aux where - "gatherDomain_aux (x#xs) = (dom x \ (gatherDomain_aux xs))" + "gatherDomain_aux (x#xs) = (dom x \ (gatherDomain_aux xs))" |"gatherDomain_aux [] = {}" definition gatherDomain where "gatherDomain p = (gatherDomain_aux (butlast p))" @@ -129,16 +131,16 @@ definition disjDomGD where "disjDomGD p = disjDom (butlast p)" lemma distrPUTLG1: "\x \ dom P; (list2policy PL) x = P x; PUTListGD PUT x PL\ \ PUT x = P x" apply (induct PL) - apply (simp_all add: domIff PUTListGD_def disjDomGD_def gatherDomain_def list2policy_def) + apply (simp_all add: domIff PUTListGD_def disjDomGD_def gatherDomain_def list2policy_def) apply (auto simp: dom_def domIff split: if_split_asm) -done + done lemma distrPUTLG2: "PL \ [] \ x \ dom P \ (list2policy (PL)) x = P x \ disjDomGD PL \ (PUT x = P x) \ PUTListGD PUT x (PL)" apply (simp add: PUTListGD_def disjDomGD_def gatherDomain_def list2policy_def) apply (induct PL) - apply (auto) + apply (auto) apply (metis PUTList_DomMT PUTList_None domI) done @@ -146,12 +148,12 @@ lemma distrPUTLG: "\x \ dom P; (list2policy PL) x = P x; disjDomGD PL; PL \ []\ \ (PUT x = P x) = PUTListGD PUT x PL " apply (rule iffI) - apply (rule distrPUTLG2) - apply (simp_all) + apply (rule distrPUTLG2) + apply (simp_all) apply (rule_tac PL = PL in distrPUTLG1) - apply (auto) -done - + apply (auto) + done + end diff --git a/UPF/UPF.thy b/UPF/UPF.thy index 7e0f232..42b4834 100644 --- a/UPF/UPF.thy +++ b/UPF/UPF.thy @@ -6,8 +6,9 @@ * This file is part of HOL-TestGen. * * Copyright (c) 2005-2012 ETH Zurich, Switzerland - * 2008-2014 Achim D. Brucker, Germany - * 2009-2014 Université Paris-Sud, France + * 2008-2015 Achim D. Brucker, Germany + * 2009-2017 Université Paris-Sud, France + * 2015-2017 The University of Sheffield, UK * * All rights reserved. * @@ -44,10 +45,10 @@ section {* Putting Everything Together: UPF *} theory UPF -imports - Normalisation - NormalisationTestSpecification - Analysis + imports + Normalisation + NormalisationTestSpecification + Analysis begin text{*