src/HOL/UNITY/Transformers.thy
changeset 13866 b42d7983a822
parent 13861 0c18f31d901a
child 13874 0da2141606c6
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Mon Mar 17 17:37:20 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Mon Mar 17 17:37:48 2003 +0100
     1.3 @@ -3,11 +3,15 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   2003  University of Cambridge
     1.6  
     1.7 -Predicate Transformers from 
     1.8 +Predicate Transformers.  From 
     1.9  
    1.10      David Meier and Beverly Sanders,
    1.11      Composing Leads-to Properties
    1.12      Theoretical Computer Science 243:1-2 (2000), 339-361.
    1.13 +
    1.14 +    David Meier,
    1.15 +    Progress Properties in Program Refinement and Parallel Composition
    1.16 +    Swiss Federal Institute of Technology Zurich (1997)
    1.17  *)
    1.18  
    1.19  header{*Predicate Transformers*}
    1.20 @@ -274,10 +278,10 @@
    1.21  apply (blast intro: wens_set.Union) 
    1.22  done
    1.23  
    1.24 -theorem leadsTo_Union:
    1.25 -  assumes awpF: "T-B \<subseteq> awp F T"
    1.26 +theorem leadsTo_Join:
    1.27 +  assumes leadsTo: "F \<in> A leadsTo B"
    1.28 +      and awpF: "T-B \<subseteq> awp F T"
    1.29        and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
    1.30 -      and leadsTo: "F \<in> A leadsTo B"
    1.31    shows "F\<squnion>G \<in> T\<inter>A leadsTo B"
    1.32  apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE]) 
    1.33  apply (rule wens_Union [THEN bexE]) 
    1.34 @@ -472,10 +476,10 @@
    1.35  
    1.36  text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}
    1.37  
    1.38 -lemma fp_leadsTo_Union:
    1.39 +lemma fp_leadsTo_Join:
    1.40      "[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B"
    1.41 -apply (rule leadsTo_Union, assumption)
    1.42 - apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast, assumption)
    1.43 +apply (rule leadsTo_Join, assumption, blast)
    1.44 +apply (simp add: FP_def awp_iff_constrains stable_def constrains_def, blast) 
    1.45  done
    1.46  
    1.47  end