diff -r 274fda8cca4b -r 78f5885b76a9 src/HOL/UNITY/Comp.thy --- a/src/HOL/UNITY/Comp.thy Sun Feb 16 12:16:07 2003 +0100 +++ b/src/HOL/UNITY/Comp.thy Sun Feb 16 12:17:40 2003 +0100 @@ -7,9 +7,9 @@ From Chandy and Sanders, "Reasoning About Program Composition", Technical Report 2000-003, University of Florida, 2000. -Revised by Sidi Ehmety on January 2001 +Revised by Sidi Ehmety on January 2001 -Added: a strong form of the \ relation (component_of) and localize +Added: a strong form of the \ relation (component_of) and localize *) @@ -20,19 +20,19 @@ instance program :: (type) ord .. defs - component_def: "F \ H == \G. F Join G = H" + component_def: "F \ H == \G. F\G = H" strict_component_def: "(F < (H::'a program)) == (F \ H & F \ H)" constdefs component_of :: "'a program =>'a program=> bool" (infixl "component'_of" 50) - "F component_of H == \G. F ok G & F Join G = H" + "F component_of H == \G. F ok G & F\G = H" strict_component_of :: "'a program\'a program=> bool" (infixl "strict'_component'_of" 50) "F strict_component_of H == F component_of H & F\H" - + preserves :: "('a=>'b) => 'a program set" "preserves v == \z. stable {s. v s = z}" @@ -45,15 +45,15 @@ subsection{*The component relation*} -lemma componentI: "H \ F | H \ G ==> H \ (F Join G)" +lemma componentI: "H \ F | H \ G ==> H \ (F\G)" apply (unfold component_def, auto) -apply (rule_tac x = "G Join Ga" in exI) -apply (rule_tac [2] x = "G Join F" in exI) +apply (rule_tac x = "G\Ga" in exI) +apply (rule_tac [2] x = "G\F" in exI) apply (auto simp add: Join_ac) done -lemma component_eq_subset: - "(F \ G) = +lemma component_eq_subset: + "(F \ G) = (Init G \ Init F & Acts F \ Acts G & AllowedActs G \ AllowedActs F)" apply (unfold component_def) apply (force intro!: exI program_equalityI) @@ -72,18 +72,18 @@ lemma SKIP_minimal: "F \ SKIP ==> F = SKIP" by (auto intro!: program_equalityI simp add: component_eq_subset) -lemma component_Join1: "F \ (F Join G)" +lemma component_Join1: "F \ (F\G)" by (unfold component_def, blast) -lemma component_Join2: "G \ (F Join G)" +lemma component_Join2: "G \ (F\G)" apply (unfold component_def) apply (simp add: Join_commute, blast) done -lemma Join_absorb1: "F \ G ==> F Join G = G" +lemma Join_absorb1: "F \ G ==> F\G = G" by (auto simp add: component_def Join_left_absorb) -lemma Join_absorb2: "G \ F ==> F Join G = F" +lemma Join_absorb2: "G \ F ==> F\G = F" by (auto simp add: Join_ac component_def) lemma JN_component_iff: "((JOIN I F) \ H) = (\i \ I. F i \ H)" @@ -104,7 +104,7 @@ apply (blast intro!: program_equalityI) done -lemma Join_component_iff: "((F Join G) \ H) = (F \ H & G \ H)" +lemma Join_component_iff: "((F\G) \ H) = (F \ H & G \ H)" by (simp add: component_eq_subset, blast) lemma component_constrains: "[| F \ G; G \ A co B |] ==> F \ A co B" @@ -119,20 +119,17 @@ lemma preservesI: "(!!z. F \ stable {s. v s = z}) ==> F \ preserves v" by (unfold preserves_def, blast) -lemma preserves_imp_eq: +lemma preserves_imp_eq: "[| F \ preserves v; act \ Acts F; (s,s') \ act |] ==> v s = v s'" -apply (unfold preserves_def stable_def constrains_def, force) -done +by (unfold preserves_def stable_def constrains_def, force) -lemma Join_preserves [iff]: - "(F Join G \ preserves v) = (F \ preserves v & G \ preserves v)" -apply (unfold preserves_def, auto) -done +lemma Join_preserves [iff]: + "(F\G \ preserves v) = (F \ preserves v & G \ preserves v)" +by (unfold preserves_def, auto) lemma JN_preserves [iff]: "(JOIN I F \ preserves v) = (\i \ I. F i \ preserves v)" -apply (simp add: JN_stable preserves_def, blast) -done +by (simp add: JN_stable preserves_def, blast) lemma SKIP_preserves [iff]: "SKIP \ preserves v" by (auto simp add: preserves_def) @@ -182,19 +179,19 @@ (** Some lemmas used only in Client.ML **) lemma stable_localTo_stable2: - "[| F \ stable {s. P (v s) (w s)}; - G \ preserves v; G \ preserves w |] - ==> F Join G \ stable {s. P (v s) (w s)}" + "[| F \ stable {s. P (v s) (w s)}; + G \ preserves v; G \ preserves w |] + ==> F\G \ stable {s. P (v s) (w s)}" apply simp apply (subgoal_tac "G \ preserves (funPair v w) ") - prefer 2 apply simp -apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto) + prefer 2 apply simp +apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], + auto) done lemma Increasing_preserves_Stable: - "[| F \ stable {s. v s \ w s}; G \ preserves v; - F Join G \ Increasing w |] - ==> F Join G \ Stable {s. v s \ w s}" + "[| F \ stable {s. v s \ w s}; G \ preserves v; F\G \ Increasing w |] + ==> F\G \ Stable {s. v s \ w s}" apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib) apply (blast intro: constrains_weaken) (*The G case remains*) @@ -204,8 +201,7 @@ apply (erule_tac V = "\act \ Acts F. ?P act" in thin_rl) apply (erule_tac V = "\z. \act \ Acts F. ?P z act" in thin_rl) apply (subgoal_tac "v x = v xa") -prefer 2 apply blast -apply auto + apply auto apply (erule order_trans, blast) done @@ -225,7 +221,7 @@ lemma component_of_SKIP [simp]: "SKIP component_of F" by (unfold component_of_def, auto) -lemma component_of_trans: +lemma component_of_trans: "[| F component_of G; G component_of H |] ==> F component_of H" apply (unfold component_of_def) apply (blast intro: Join_assoc [symmetric]) @@ -241,8 +237,8 @@ lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F" by (simp add: localize_def) -lemma localize_AllowedActs_eq [simp]: - "AllowedActs (localize v F) = AllowedActs F \ (\G \ preserves v. Acts G)" +lemma localize_AllowedActs_eq [simp]: + "AllowedActs (localize v F) = AllowedActs F \ (\G \ preserves v. Acts G)" by (unfold localize_def, auto) end