# HG changeset patch # User paulson # Date 1045577354 -3600 # Node ID 0fd39aa770950e6da01c749183292af8d68f5b11 # Parent 87a8ab465b29612066222ac398ffe3d808629823 new theory Transformers: Meier-Sanders non-interference theory diff -r 87a8ab465b29 -r 0fd39aa77095 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Feb 17 17:16:07 2003 +0100 +++ b/src/HOL/IsaMakefile Tue Feb 18 15:09:14 2003 +0100 @@ -385,7 +385,7 @@ UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy \ UNITY/Guar.thy UNITY/Lift_prog.thy UNITY/ListOrder.thy \ - UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \ + UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy \ UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \ UNITY/Simple/Channel.thy UNITY/Simple/Common.thy \ UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \ diff -r 87a8ab465b29 -r 0fd39aa77095 src/HOL/UNITY/ROOT.ML --- a/src/HOL/UNITY/ROOT.ML Mon Feb 17 17:16:07 2003 +0100 +++ b/src/HOL/UNITY/ROOT.ML Tue Feb 18 15:09:14 2003 +0100 @@ -9,6 +9,9 @@ (*Basic meta-theory*) time_use_thy "UNITY_Main"; +(*New Meier/Sanders composition theory*) +time_use_thy "Transformers"; + (*Simple examples: no composition*) time_use_thy "Simple/Deadlock"; time_use_thy "Simple/Common"; diff -r 87a8ab465b29 -r 0fd39aa77095 src/HOL/UNITY/Transformers.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/UNITY/Transformers.thy Tue Feb 18 15:09:14 2003 +0100 @@ -0,0 +1,263 @@ +(* Title: HOL/UNITY/Transformers + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2003 University of Cambridge + +Predicate Transformers from + + David Meier and Beverly Sanders, + Composing Leads-to Properties + Theoretical Computer Science 243:1-2 (2000), 339-361. +*) + +header{*Predicate Transformers*} + +theory Transformers = Comp: + +subsection{*Defining the Predicate Transformers @{term wp}, + @{term awp} and @{term wens}*} + +constdefs + wp :: "[('a*'a) set, 'a set] => 'a set" + --{*Dijkstra's weakest-precondition operator*} + "wp act B == - (act^-1 `` (-B))" + + awp :: "[ 'a program, 'a set] => 'a set" + "awp F B == (\act \ Acts F. wp act B)" + + wens :: "[ 'a program, ('a*'a) set, 'a set] => 'a set" + "wens F act B == gfp(\X. (wp act B \ awp F (B \ X)) \ B)" + +text{*The fundamental theorem for wp*} +theorem wp_iff: "(A <= wp act B) = (act `` A <= B)" +by (force simp add: wp_def) + +lemma Compl_Domain_subset_wp: "- (Domain act) \ wp act B" +by (force simp add: wp_def) + +lemma awp_Int_eq: "awp F (A\B) = awp F A \ awp F B" +by (simp add: awp_def wp_def, blast) + +text{*The fundamental theorem for awp*} +theorem awp_iff: "(A <= awp F B) = (F \ A co B)" +by (simp add: awp_def constrains_def wp_iff INT_subset_iff) + +theorem stable_iff_awp: "(A \ awp F A) = (F \ stable A)" +by (simp add: awp_iff stable_def) + +lemma awp_mono: "(A \ B) ==> awp F A \ awp F B" +by (simp add: awp_def wp_def, blast) + +lemma wens_unfold: + "wens F act B = (wp act B \ awp F (B \ wens F act B)) \ B" +apply (simp add: wens_def) +apply (rule gfp_unfold) +apply (simp add: mono_def wp_def awp_def, blast) +done + +text{*These two theorems justify the claim that @{term wens} returns the +weakest assertion satisfying the ensures property*} +lemma ensures_imp_wens: "F \ A ensures B ==> \act \ Acts F. A \ wens F act B" +apply (simp add: wens_def ensures_def transient_def, clarify) +apply (rule rev_bexI, assumption) +apply (rule gfp_upperbound) +apply (simp add: constrains_def awp_def wp_def, blast) +done + +lemma wens_ensures: "act \ Acts F ==> F \ (wens F act B) ensures B" +by (simp add: wens_def gfp_def constrains_def awp_def wp_def + ensures_def transient_def, blast) + +text{*These two results constitute assertion (4.13) of the thesis*} +lemma wens_mono: "(A \ B) ==> wens F act A \ wens F act B" +apply (simp add: wens_def wp_def awp_def) +apply (rule gfp_mono, blast) +done + +lemma wens_weakening: "B \ wens F act B" +by (simp add: wens_def gfp_def, blast) + +text{*Assertion (6), or 4.16 in the thesis*} +lemma subset_wens: "A-B \ wp act B \ awp F (B \ A) ==> A \ wens F act B" +apply (simp add: wens_def wp_def awp_def) +apply (rule gfp_upperbound, blast) +done + +text{*Assertion 4.17 in the thesis*} +lemma Diff_wens_constrains: "F \ (wens F act A - A) co wens F act A" +by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast) + +text{*Assertion (7): 4.18 in the thesis. NOTE that many of these results +hold for an arbitrary action. We often do not require @{term "act \ Acts F"}*} +lemma stable_wens: "F \ stable A ==> F \ stable (wens F act A)" +apply (simp add: stable_def) +apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) +apply (simp add: Un_Int_distrib2 Compl_partition2) +apply (erule constrains_weaken) + apply blast +apply (simp add: Un_subset_iff wens_weakening) +done + +text{*Assertion 4.20 in the thesis.*} +lemma wens_Int_eq_lemma: + "[|T-B \ awp F T; act \ Acts F|] + ==> T \ wens F act B \ wens F act (T\B)" +apply (rule subset_wens) +apply (rule_tac P="\x. ?f x \ ?b" in ssubst [OF wens_unfold]) +apply (simp add: wp_def awp_def, blast) +done + +text{*Assertion (8): 4.21 in the thesis. Here we indeed require + @{term "act \ Acts F"}*} +lemma wens_Int_eq: + "[|T-B \ awp F T; act \ Acts F|] + ==> T \ wens F act B = T \ wens F act (T\B)" +apply (rule equalityI) + apply (simp_all add: Int_lower1 Int_subset_iff) + apply (rule wens_Int_eq_lemma, assumption+) +apply (rule subset_trans [OF _ wens_mono [of "T\B" B]], auto) +done + +subsection{*Defining the Weakest Ensures Set*} + +consts + wens_set :: "['a program, 'a set] => 'a set set" + +inductive "wens_set F B" + intros + + Basis: "B \ wens_set F B" + + Wens: "[|X \ wens_set F B; act \ Acts F|] ==> wens F act X \ wens_set F B" + + Union: "W \ {} ==> \U \ W. U \ wens_set F B ==> \W \ wens_set F B" + +lemma wens_set_imp_co: "A \ wens_set F B ==> F \ (A-B) co A" +apply (erule wens_set.induct) + apply (simp add: constrains_def) + apply (drule_tac act1=act and A1=X + in constrains_Un [OF Diff_wens_constrains]) + apply (erule constrains_weaken, blast) + apply (simp add: Un_subset_iff wens_weakening) +apply (rule constrains_weaken) +apply (rule_tac I=W and A="\v. v-B" and A'="\v. v" in constrains_UN, blast+) +done + +lemma wens_set_imp_leadsTo: "A \ wens_set F B ==> F \ A leadsTo B" +apply (erule wens_set.induct) + apply (rule leadsTo_refl) + apply (blast intro: wens_ensures leadsTo_Basis leadsTo_Trans ) +apply (blast intro: leadsTo_Union) +done + +(*????????????????Set.thy Set.all_not_in_conv*) +lemma ex_in_conv: "(\x. x \ A) = (A \ {})" +by blast + + +lemma leadsTo_imp_wens_set: "F \ A leadsTo B ==> \C \ wens_set F B. A \ C" +apply (erule leadsTo_induct_pre) + apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens) + apply clarify + apply (drule ensures_weaken_R, assumption) + apply (blast dest!: ensures_imp_wens intro: wens_set.Wens) +apply (case_tac "S={}") + apply (simp, blast intro: wens_set.Basis) +apply (clarsimp dest!: bchoice simp: ball_conj_distrib Bex_def) +apply (rule_tac x = "\{Z. \U\S. Z = f U}" in exI) +apply (blast intro: wens_set.Union) +done + +text{*Assertion (9): 4.27 in the thesis.*} + +lemma leadsTo_iff_wens_set: "(F \ A leadsTo B) = (\C \ wens_set F B. A \ C)" +by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) + +text{*This is the result that requires the definition of @{term wens_set} to +require @{term W} to be non-empty in the Unio case, for otherwise we should +always have @{term "{} \ wens_set F B"}.*} +lemma wens_set_imp_subset: "A \ wens_set F B ==> B \ A" +apply (erule wens_set.induct) + apply (blast intro: wens_weakening [THEN subsetD])+ +done + + +subsection{*Properties Involving Program Union*} + +text{*Assertion (4.30) of thesis, reoriented*} +lemma awp_Join_eq: "awp (F\G) B = awp F B \ awp G B" +by (simp add: awp_def wp_def, blast) + +lemma wens_subset: + "wens F act B - B \ wp act B \ awp F (B \ wens F act B)" +by (subst wens_unfold, fast) + +text{*Assertion (4.31)*} +lemma subset_wens_Join: + "[|A = T \ wens F act B; T-B \ awp F T; A-B \ awp G (A \ B)|] + ==> A \ wens (F\G) act B" +apply (subgoal_tac "(T \ wens F act B) - B \ + wp act B \ awp F (B \ wens F act B) \ awp F T") + apply (rule subset_wens) + apply (simp add: awp_Join_eq awp_Int_eq Int_subset_iff Un_commute) + apply (simp add: awp_def wp_def, blast) +apply (insert wens_subset [of F act B], blast) +done + +text{*Assertion (4.32)*} +lemma wens_Join_subset: "wens (F\G) act B \ wens F act B" +apply (simp add: wens_def) +apply (rule gfp_mono) +apply (auto simp add: awp_Join_eq) +done + +text{*Lemma, because the inductive step is just too messy.*} +lemma wens_Union_inductive_step: + assumes awpF: "T-B \ awp F T" + and awpG: "!!X. X \ wens_set F B ==> (T\X) - B \ awp G (T\X)" + shows "[|X \ wens_set F B; act \ Acts F; Y \ X; T\X = T\Y|] + ==> wens (F\G) act Y \ wens F act X \ + T \ wens F act X = T \ wens (F\G) act Y" +apply (subgoal_tac "wens (F\G) act Y \ wens F act X") + prefer 2 + apply (blast dest: wens_mono intro: wens_Join_subset [THEN subsetD], simp) +apply (rule equalityI) + prefer 2 apply blast +apply (simp add: Int_lower1 Int_subset_iff) +apply (frule wens_set_imp_subset) +apply (subgoal_tac "T-X \ awp F T") + prefer 2 apply (blast intro: awpF [THEN subsetD]) +apply (rule_tac B = "wens (F\G) act (T\X)" in subset_trans) + prefer 2 apply (blast intro!: wens_mono) +apply (subst wens_Int_eq, assumption+) +apply (rule subset_wens_Join [of _ T]) + apply simp + apply blast +apply (subgoal_tac "T \ wens F act (T\X) \ T\X = T \ wens F act X") + prefer 2 + apply (subst wens_Int_eq [symmetric], assumption+) + apply (blast intro: wens_weakening [THEN subsetD], simp) +apply (blast intro: awpG [THEN subsetD] wens_set.Wens) +done + +lemma wens_Union: + assumes awpF: "T-B \ awp F T" + and awpG: "!!X. X \ wens_set F B ==> (T\X) - B \ awp G (T\X)" + and major: "X \ wens_set F B" + shows "\Y \ wens_set (F\G) B. Y \ X & T\X = T\Y" +apply (rule wens_set.induct [OF major]) + txt{*Basis: trivial*} + apply (blast intro: wens_set.Basis) + txt{*Inductive step*} + apply clarify + apply (rule_tac x = "wens (F\G) act Y" in rev_bexI) + apply (force intro: wens_set.Wens) + apply (simp add: wens_Union_inductive_step [OF awpF awpG]) +txt{*Union: by Axiom of Choice*} +apply (simp add: ball_conj_distrib Bex_def) +apply (clarify dest!: bchoice) +apply (rule_tac x = "\{Z. \U\W. Z = f U}" in exI) +apply (blast intro: wens_set.Union) +done + +end