Updated indentation.

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
+ *               2008-2015 Achim D. Brucker, Germany
- *               2009-2014 Université Paris-Sud, France
+ *               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 
+  imports 
-  Normalisation
+    Normalisation
 begin
 
 text{* 
@@ -72,41 +72,43 @@ fun PUTList :: "('a \<mapsto> 'b) \<Rightarrow> 'a \<Rightarrow> ('a \<mapsto> '
 lemma distrPUTL1: "x \<in> dom P \<Longrightarrow> (list2policy PL) x = P x  
                              \<Longrightarrow>  (PUTList PUT x PL \<Longrightarrow> (PUT x = P x))"
   apply (induct PL) 
-  apply (auto simp: list2policy_def dom_def)
+   apply (auto simp: list2policy_def dom_def)
-done
+  done
 
 lemma PUTList_None: "x \<notin> dom (list2policy list) \<Longrightarrow> PUTList PUT x list"
   apply (induct list)
-  apply (auto simp: list2policy_def dom_def)
+   apply (auto simp: list2policy_def dom_def)
-done
+  done
 
 lemma PUTList_DomMT:
   "(\<forall>y\<in>set list. dom a \<inter> dom y = {}) \<Longrightarrow> x \<in> (dom a) \<Longrightarrow> x \<notin> dom (list2policy list)"
   apply (induct list)
-  apply (auto simp: dom_def list2policy_def)
+   apply (auto simp: dom_def list2policy_def)
-done
+  done
 
 lemma distrPUTL2: 
   "x \<in> dom P \<Longrightarrow> (list2policy PL) x = P x  \<Longrightarrow> disjDom PL \<Longrightarrow> (PUT x = P x) \<Longrightarrow> PUTList PUT x PL "
   apply (induct PL) 
-  apply (simp_all add: list2policy_def)
+   apply (simp_all add: list2policy_def)
-  apply (auto)
+  apply (auto)[1]
-  apply (case_tac "x \<in> dom a")
+  subgoal for a PL p
-  apply (case_tac "list2policy PL x = P x")
+    apply (case_tac "x \<in> dom a")
-  apply (simp add: list2policy_def)
+     apply (case_tac "list2policy PL x = P x")
-  apply (rule PUTList_None) 
+      apply (simp add: list2policy_def)
-  apply (rule_tac a = a in PUTList_DomMT)
+     apply (rule PUTList_None) 
-  apply (simp_all add: list2policy_def dom_def)
+     apply (rule_tac a = a in PUTList_DomMT)
-done
+      apply (simp_all add: list2policy_def dom_def)
+    done
+  done
 
 lemma distrPUTL: 
   "\<lbrakk>x \<in> dom P; (list2policy PL) x = P x; disjDom PL\<rbrakk> \<Longrightarrow> (PUT x = P x) = PUTList PUT x PL "
   apply (rule iffI)
-  apply (rule distrPUTL2)
+   apply (rule distrPUTL2)
-  apply (simp_all)
+      apply (simp_all)
   apply (rule_tac PL = PL in distrPUTL1)
-  apply (auto)
+    apply (auto)
-done
+  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 \<union> (gatherDomain_aux xs))"
+  "gatherDomain_aux (x#xs) = (dom x \<union> (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: "\<lbrakk>x \<in> dom P; (list2policy PL) x = P x; PUTListGD PUT x PL\<rbrakk> \<Longrightarrow> 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 \<noteq> [] \<Longrightarrow> x \<in> dom P \<Longrightarrow> (list2policy (PL)) x = P x \<Longrightarrow> disjDomGD PL \<Longrightarrow> 
    (PUT x = P x) \<Longrightarrow> 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:
   "\<lbrakk>x \<in> dom P; (list2policy PL) x = P x; disjDomGD PL; PL \<noteq> []\<rbrakk> \<Longrightarrow>  
   (PUT x = P x) = PUTListGD PUT x PL "
   apply (rule iffI)
-  apply (rule distrPUTLG2) 
+   apply (rule distrPUTLG2) 
-  apply (simp_all)
+       apply (simp_all)
   apply (rule_tac PL = PL in distrPUTLG1)
-  apply (auto)
+    apply (auto)
-done
+  done
-
+    
 end
 
 

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
+ *               2008-2015 Achim D. Brucker, Germany
- *               2009-2014 Université Paris-Sud, France
+ *               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 
+  imports 
-  Normalisation
+    Normalisation
-  NormalisationTestSpecification
+    NormalisationTestSpecification
-  Analysis
+    Analysis
 begin
 
 text{*