# HG changeset patch # User paulson # Date 1043854491 -3600 # Node ID d1811693899c67a60a377b51ade1b16d84dd3811 # Parent 3b6ff7ceaf272c44a0814810ea7cc6d4558517bf converted more UNITY theories to new-style diff -r 3b6ff7ceaf27 -r d1811693899c src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jan 29 16:29:38 2003 +0100 +++ b/src/HOL/IsaMakefile Wed Jan 29 16:34:51 2003 +0100 @@ -382,13 +382,13 @@ $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \ - UNITY/Comp.ML UNITY/Comp.thy UNITY/Detects.thy UNITY/ELT.thy \ + UNITY/Comp.thy UNITY/Detects.thy UNITY/ELT.thy \ UNITY/Extend.thy UNITY/FP.ML UNITY/FP.thy UNITY/Follows.ML \ UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \ - UNITY/Guar.ML UNITY/Guar.thy UNITY/Lift_prog.thy UNITY/ListOrder.thy \ + UNITY/Guar.thy UNITY/Lift_prog.thy UNITY/ListOrder.thy \ UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \ UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML \ - UNITY/UNITY.thy UNITY/Union.ML UNITY/Union.thy UNITY/WFair.ML UNITY/WFair.thy \ + UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.ML UNITY/WFair.thy \ UNITY/Simple/Channel.thy UNITY/Simple/Common.thy \ UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \ UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy \ diff -r 3b6ff7ceaf27 -r d1811693899c src/HOL/UNITY/Comp.ML --- a/src/HOL/UNITY/Comp.ML Wed Jan 29 16:29:38 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,263 +0,0 @@ -(* Title: HOL/UNITY/Comp.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Composition -From Chandy and Sanders, "Reasoning About Program Composition" - -Revised by Sidi Ehmety on January 2001 - -*) -(*** component <= ***) -Goalw [component_def] - "H <= F | H <= G ==> H <= (F Join G)"; -by Auto_tac; -by (res_inst_tac [("x", "G Join Ga")] exI 1); -by (res_inst_tac [("x", "G Join F")] exI 2); -by (auto_tac (claset(), simpset() addsimps Join_ac)); -qed "componentI"; - -Goalw [component_def] - "(F <= G) = \ -\ (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)"; -by (force_tac (claset() addSIs [exI, program_equalityI], - simpset()) 1); -qed "component_eq_subset"; - -Goalw [component_def] "SKIP <= F"; -by (force_tac (claset() addIs [Join_SKIP_left], simpset()) 1); -qed "component_SKIP"; - -Goalw [component_def] "F <= (F :: 'a program)"; -by (blast_tac (claset() addIs [Join_SKIP_right]) 1); -qed "component_refl"; - -AddIffs [component_SKIP, component_refl]; - -Goal "F <= SKIP ==> F = SKIP"; -by (auto_tac (claset() addSIs [program_equalityI], - simpset() addsimps [component_eq_subset])); -qed "SKIP_minimal"; - -Goalw [component_def] "F <= (F Join G)"; -by (Blast_tac 1); -qed "component_Join1"; - -Goalw [component_def] "G <= (F Join G)"; -by (simp_tac (simpset() addsimps [Join_commute]) 1); -by (Blast_tac 1); -qed "component_Join2"; - -Goal "F<=G ==> F Join G = G"; -by (auto_tac (claset(), simpset() addsimps [component_def, Join_left_absorb])); -qed "Join_absorb1"; - -Goal "G<=F ==> F Join G = F"; -by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def])); -qed "Join_absorb2"; - -Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)"; -by (simp_tac (simpset() addsimps [component_eq_subset]) 1); -by (Blast_tac 1); -qed "JN_component_iff"; - -Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))"; -by (blast_tac (claset() addIs [JN_absorb]) 1); -qed "component_JN"; - -Goalw [component_def] "[| F <= G; G <= H |] ==> F <= (H :: 'a program)"; -by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); -qed "component_trans"; - -Goal "[| F <= G; G <= F |] ==> F = (G :: 'a program)"; -by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1); -by (blast_tac (claset() addSIs [program_equalityI]) 1); -qed "component_antisym"; - -Goal "((F Join G) <= H) = (F <= H & G <= H)"; -by (simp_tac (simpset() addsimps [component_eq_subset]) 1); -by (Blast_tac 1); -qed "Join_component_iff"; - -Goal "[| F <= G; G : A co B |] ==> F : A co B"; -by (auto_tac (claset(), - simpset() addsimps [constrains_def, component_eq_subset])); -qed "component_constrains"; - -(*Used in Guar.thy to show that programs are partially ordered*) -bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq); - - -(*** preserves ***) - -val prems = -Goalw [preserves_def] "(!!z. F : stable {s. v s = z}) ==> F : preserves v"; -by (blast_tac (claset() addIs prems) 1); -qed "preservesI"; - -Goalw [preserves_def, stable_def, constrains_def] - "[| F : preserves v; act : Acts F; (s,s') : act |] ==> v s = v s'"; -by (Force_tac 1); -qed "preserves_imp_eq"; - -Goalw [preserves_def] - "(F Join G : preserves v) = (F : preserves v & G : preserves v)"; -by Auto_tac; -qed "Join_preserves"; - -Goal "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"; -by (simp_tac (simpset() addsimps [JN_stable, preserves_def]) 1); -by (Blast_tac 1); -qed "JN_preserves"; - -Goal "SKIP : preserves v"; -by (auto_tac (claset(), simpset() addsimps [preserves_def])); -qed "SKIP_preserves"; - -AddIffs [Join_preserves, JN_preserves, SKIP_preserves]; - -Goalw [funPair_def] "(funPair f g) x = (f x, g x)"; -by (Simp_tac 1); -qed "funPair_apply"; -Addsimps [funPair_apply]; - -Goal "preserves (funPair v w) = preserves v Int preserves w"; -by (auto_tac (claset(), - simpset() addsimps [preserves_def, stable_def, constrains_def])); -by (Blast_tac 1); -qed "preserves_funPair"; - -(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *) -AddIffs [preserves_funPair RS eqset_imp_iff]; - - -Goal "(funPair f g) o h = funPair (f o h) (g o h)"; -by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1); -qed "funPair_o_distrib"; - -Goal "fst o (funPair f g) = f"; -by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1); -qed "fst_o_funPair"; - -Goal "snd o (funPair f g) = g"; -by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1); -qed "snd_o_funPair"; -Addsimps [fst_o_funPair, snd_o_funPair]; - -Goal "preserves v <= preserves (w o v)"; -by (force_tac (claset(), - simpset() addsimps [preserves_def, stable_def, constrains_def]) 1); -qed "subset_preserves_o"; - -Goal "preserves v <= stable {s. P (v s)}"; -by (auto_tac (claset(), - simpset() addsimps [preserves_def, stable_def, constrains_def])); -by (rename_tac "s' s" 1); -by (subgoal_tac "v s = v s'" 1); -by (ALLGOALS Force_tac); -qed "preserves_subset_stable"; - -Goal "preserves v <= increasing v"; -by (auto_tac (claset(), - simpset() addsimps [impOfSubs preserves_subset_stable, - increasing_def])); -qed "preserves_subset_increasing"; - -Goal "preserves id <= stable A"; -by (force_tac (claset(), - simpset() addsimps [preserves_def, stable_def, constrains_def]) 1); -qed "preserves_id_subset_stable"; - - -(** For use with def_UNION_ok_iff **) - -Goal "safety_prop (preserves v)"; -by (auto_tac (claset() addIs [safety_prop_INTER1], - simpset() addsimps [preserves_def])); -qed "safety_prop_preserves"; -AddIffs [safety_prop_preserves]; - - -(** Some lemmas used only in Client.ML **) - -Goal "[| F : stable {s. P (v s) (w s)}; \ -\ G : preserves v; G : preserves w |] \ -\ ==> F Join G : stable {s. P (v s) (w s)}"; -by (Asm_simp_tac 1); -by (subgoal_tac "G: preserves (funPair v w)" 1); -by (Asm_simp_tac 2); -by (dres_inst_tac [("P1", "split ?Q")] - (impOfSubs preserves_subset_stable) 1); -by Auto_tac; -qed "stable_localTo_stable2"; - -Goal "[| F : stable {s. v s <= w s}; G : preserves v; \ -\ F Join G : Increasing w |] \ -\ ==> F Join G : Stable {s. v s <= w s}"; -by (auto_tac (claset(), - simpset() addsimps [stable_def, Stable_def, Increasing_def, - Constrains_def, all_conj_distrib])); -by (blast_tac (claset() addIs [constrains_weaken]) 1); -(*The G case remains*) -by (auto_tac (claset(), - simpset() addsimps [preserves_def, stable_def, constrains_def])); -by (case_tac "act: Acts F" 1); -by (Blast_tac 1); -(*We have a G-action, so delete assumptions about F-actions*) -by (thin_tac "ALL act:Acts F. ?P act" 1); -by (thin_tac "ALL z. ALL act:Acts F. ?P z act" 1); -by (subgoal_tac "v x = v xa" 1); -by (Blast_tac 2); -by Auto_tac; -by (etac order_trans 1); -by (Blast_tac 1); -qed "Increasing_preserves_Stable"; - -(** component_of **) - -(* component_of is stronger than <= *) -Goalw [component_def, component_of_def] -"F component_of H ==> F <= H"; -by (Blast_tac 1); -qed "component_of_imp_component"; - - -(* component_of satisfies many of the <='s properties *) -Goalw [component_of_def] -"F component_of F"; -by (res_inst_tac [("x", "SKIP")] exI 1); -by Auto_tac; -qed "component_of_refl"; - -Goalw [component_of_def] -"SKIP component_of F"; -by Auto_tac; -qed "component_of_SKIP"; - -Addsimps [component_of_refl, component_of_SKIP]; - -Goalw [component_of_def] -"[| F component_of G; G component_of H |] ==> F component_of H"; -by (blast_tac (claset() addIs [Join_assoc RS sym]) 1); -qed "component_of_trans"; - -bind_thm ("strict_component_of_eq", strict_component_of_def RS meta_eq_to_obj_eq); - -(** localize **) -Goalw [localize_def] - "Init (localize v F) = Init F"; -by (Simp_tac 1); -qed "localize_Init_eq"; - -Goalw [localize_def] - "Acts (localize v F) = Acts F"; -by (Simp_tac 1); -qed "localize_Acts_eq"; - -Goalw [localize_def] - "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"; -by Auto_tac; -qed "localize_AllowedActs_eq"; - -Addsimps [localize_Init_eq, localize_Acts_eq, localize_AllowedActs_eq]; diff -r 3b6ff7ceaf27 -r d1811693899c src/HOL/UNITY/Comp.thy --- a/src/HOL/UNITY/Comp.thy Wed Jan 29 16:29:38 2003 +0100 +++ b/src/HOL/UNITY/Comp.thy Wed Jan 29 16:34:51 2003 +0100 @@ -13,14 +13,13 @@ *) -Comp = Union + +theory Comp = Union: -instance - program :: (type) ord +instance program :: (type) ord .. defs - component_def "F <= H == EX G. F Join G = H" - strict_component_def "(F < (H::'a program)) == (F <= H & F ~= H)" + component_def: "F <= H == EX G. F Join G = H" + strict_component_def: "(F < (H::'a program)) == (F <= H & F ~= H)" constdefs @@ -28,7 +27,7 @@ (infixl "component'_of" 50) "F component_of H == EX G. F ok G & F Join G = H" - strict_component_of :: "'a program\\'a program=> bool" + strict_component_of :: "'a program\'a program=> bool" (infixl "strict'_component'_of" 50) "F strict_component_of H == F component_of H & F~=H" @@ -41,4 +40,222 @@ funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c" "funPair f g == %x. (f x, g x)" + + +(*** component <= ***) +lemma componentI: + "H <= F | H <= G ==> H <= (F Join 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 (auto simp add: Join_ac) +done + +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) +done + +lemma component_SKIP [iff]: "SKIP <= F" +apply (unfold component_def) +apply (force intro: Join_SKIP_left) +done + +lemma component_refl [iff]: "F <= (F :: 'a program)" +apply (unfold component_def) +apply (blast intro: Join_SKIP_right) +done + +lemma SKIP_minimal: "F <= SKIP ==> F = SKIP" +by (auto intro!: program_equalityI simp add: component_eq_subset) + +lemma component_Join1: "F <= (F Join G)" +by (unfold component_def, blast) + +lemma component_Join2: "G <= (F Join G)" +apply (unfold component_def) +apply (simp (no_asm) add: Join_commute) +apply blast +done + +lemma Join_absorb1: "F<=G ==> F Join G = G" +by (auto simp add: component_def Join_left_absorb) + +lemma Join_absorb2: "G<=F ==> F Join G = F" +by (auto simp add: Join_ac component_def) + +lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)" +apply (simp (no_asm) add: component_eq_subset) +apply blast +done + +lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))" +apply (unfold component_def) +apply (blast intro: JN_absorb) +done + +lemma component_trans: "[| F <= G; G <= H |] ==> F <= (H :: 'a program)" +apply (unfold component_def) +apply (blast intro: Join_assoc [symmetric]) +done + +lemma component_antisym: "[| F <= G; G <= F |] ==> F = (G :: 'a program)" +apply (simp (no_asm_use) add: component_eq_subset) +apply (blast intro!: program_equalityI) +done + +lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)" +apply (simp (no_asm) add: component_eq_subset) +apply blast +done + +lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B" +by (auto simp add: constrains_def component_eq_subset) + +(*Used in Guar.thy to show that programs are partially ordered*) +lemmas program_less_le = strict_component_def [THEN meta_eq_to_obj_eq] + + +(*** preserves ***) + +lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v" +by (unfold preserves_def, blast) + +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 + +lemma Join_preserves [iff]: + "(F Join G : preserves v) = (F : preserves v & G : preserves v)" +apply (unfold preserves_def, auto) +done + +lemma JN_preserves [iff]: + "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)" +apply (simp (no_asm) add: JN_stable preserves_def) +apply blast +done + +lemma SKIP_preserves [iff]: "SKIP : preserves v" +by (auto simp add: preserves_def) + +lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)" +by (simp add: funPair_def) + +lemma preserves_funPair: "preserves (funPair v w) = preserves v Int preserves w" +by (auto simp add: preserves_def stable_def constrains_def, blast) + +(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *) +declare preserves_funPair [THEN eqset_imp_iff, iff] + + +lemma funPair_o_distrib: "(funPair f g) o h = funPair (f o h) (g o h)" +apply (simp (no_asm) add: funPair_def o_def) +done + +lemma fst_o_funPair [simp]: "fst o (funPair f g) = f" +apply (simp (no_asm) add: funPair_def o_def) +done + +lemma snd_o_funPair [simp]: "snd o (funPair f g) = g" +apply (simp (no_asm) add: funPair_def o_def) +done + +lemma subset_preserves_o: "preserves v <= preserves (w o v)" +by (force simp add: preserves_def stable_def constrains_def) + +lemma preserves_subset_stable: "preserves v <= stable {s. P (v s)}" +apply (auto simp add: preserves_def stable_def constrains_def) +apply (rename_tac s' s) +apply (subgoal_tac "v s = v s'") +apply (force+) +done + +lemma preserves_subset_increasing: "preserves v <= increasing v" +by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def) + +lemma preserves_id_subset_stable: "preserves id <= stable A" +by (force simp add: preserves_def stable_def constrains_def) + + +(** For use with def_UNION_ok_iff **) + +lemma safety_prop_preserves [iff]: "safety_prop (preserves v)" +by (auto intro: safety_prop_INTER1 simp add: preserves_def) + + +(** 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)}" +apply (simp (no_asm_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) +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}" +apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib) +apply (blast intro: constrains_weaken) +(*The G case remains*) +apply (auto simp add: preserves_def stable_def constrains_def) +apply (case_tac "act: Acts F", blast) +(*We have a G-action, so delete assumptions about F-actions*) +apply (erule_tac V = "ALL act:Acts F. ?P act" in thin_rl) +apply (erule_tac V = "ALL z. ALL act:Acts F. ?P z act" in thin_rl) +apply (subgoal_tac "v x = v xa") +prefer 2 apply blast +apply auto +apply (erule order_trans, blast) +done + +(** component_of **) + +(* component_of is stronger than <= *) +lemma component_of_imp_component: "F component_of H ==> F <= H" +by (unfold component_def component_of_def, blast) + + +(* component_of satisfies many of the <='s properties *) +lemma component_of_refl [simp]: "F component_of F" +apply (unfold component_of_def) +apply (rule_tac x = SKIP in exI, auto) +done + +lemma component_of_SKIP [simp]: "SKIP component_of F" +by (unfold component_of_def, auto) + +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]) +done + +lemmas strict_component_of_eq = + strict_component_of_def [THEN meta_eq_to_obj_eq, standard] + +(** localize **) +lemma localize_Init_eq [simp]: "Init (localize v F) = Init F" +apply (unfold localize_def) +apply (simp (no_asm)) +done + +lemma localize_Acts_eq [simp]: "Acts (localize v F) = Acts F" +apply (unfold localize_def) +apply (simp (no_asm)) +done + +lemma localize_AllowedActs_eq [simp]: + "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)" +apply (unfold localize_def, auto) +done + end diff -r 3b6ff7ceaf27 -r d1811693899c src/HOL/UNITY/Comp/Counter.thy --- a/src/HOL/UNITY/Comp/Counter.thy Wed Jan 29 16:29:38 2003 +0100 +++ b/src/HOL/UNITY/Comp/Counter.thy Wed Jan 29 16:34:51 2003 +0100 @@ -11,7 +11,8 @@ Spriner LNCS 1586 (1999), pages 1215-1227. *) -Counter = Comp + +Counter = UNITY_Main + + (* Variables are names *) datatype name = C | c nat types state = name=>int diff -r 3b6ff7ceaf27 -r d1811693899c src/HOL/UNITY/Comp/Counterc.thy --- a/src/HOL/UNITY/Comp/Counterc.thy Wed Jan 29 16:29:38 2003 +0100 +++ b/src/HOL/UNITY/Comp/Counterc.thy Wed Jan 29 16:34:51 2003 +0100 @@ -11,7 +11,8 @@ Spriner LNCS 1586 (1999), pages 1215-1227. *) -Counterc = Comp + +Counterc = UNITY_Main + + types state arities state :: type diff -r 3b6ff7ceaf27 -r d1811693899c src/HOL/UNITY/Guar.ML --- a/src/HOL/UNITY/Guar.ML Wed Jan 29 16:29:38 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,520 +0,0 @@ -(* Title: HOL/UNITY/Guar.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1999 University of Cambridge - -Guarantees, etc. - -From Chandy and Sanders, "Reasoning About Program Composition" -Revised by Sidi Ehmety on January 2001 -*) - -Goal "(OK (insert i I) F) = (if i:I then OK I F else OK I F & (F i ok JOIN I F))"; -by (auto_tac (claset() addIs [ok_sym], - simpset() addsimps [OK_iff_ok])); -qed "OK_insert_iff"; - - - -(*** existential properties ***) -Goalw [ex_prop_def] - "[| ex_prop X; finite GG |] ==> \ -\ GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X"; -by (etac finite_induct 1); -by (auto_tac (claset(), simpset() addsimps [OK_insert_iff,Int_insert_left])); -qed_spec_mp "ex1"; - - -Goalw [ex_prop_def] - "ALL GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X ==> ex_prop X"; -by (Clarify_tac 1); -by (dres_inst_tac [("x", "{F,G}")] spec 1); -by (auto_tac (claset() addDs [ok_sym], - simpset() addsimps [OK_iff_ok])); -qed "ex2"; - - -(*Chandy & Sanders take this as a definition*) -Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)"; -by (blast_tac (claset() addIs [ex1,ex2]) 1); -qed "ex_prop_finite"; - - -(*Their "equivalent definition" given at the end of section 3*) -Goal - "ex_prop X = (ALL G. G:X = (ALL H. (G component_of H) --> H: X))"; -by Auto_tac; -by (rewrite_goals_tac - [ex_prop_def, component_of_def]); -by Safe_tac; -by (stac Join_commute 3); -by (dtac ok_sym 3); -by (REPEAT(Blast_tac 1)); -qed "ex_prop_equiv"; - - -(*** universal properties ***) -Goalw [uv_prop_def] - "[| uv_prop X; finite GG |] ==> \ -\ GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X"; -by (etac finite_induct 1); -by (auto_tac (claset(), simpset() addsimps - [Int_insert_left, OK_insert_iff])); -qed_spec_mp "uv1"; - -Goalw [uv_prop_def] - "ALL GG. finite GG & GG <= X & OK GG (%G. G)-->(JN G:GG. G):X ==> uv_prop X"; -by (rtac conjI 1); -by (Clarify_tac 2); -by (dres_inst_tac [("x", "{F,G}")] spec 2); -by (dres_inst_tac [("x", "{}")] spec 1); -by (auto_tac (claset() addDs [ok_sym], simpset() addsimps [OK_iff_ok])); -qed "uv2"; - -(*Chandy & Sanders take this as a definition*) -Goal "uv_prop X = (ALL GG. finite GG & GG <= X & OK GG (%G. G)--> (JN G:GG. G): X)"; -by (blast_tac (claset() addIs [uv1,uv2]) 1); -qed "uv_prop_finite"; - -(*** guarantees ***) - -val prems = Goal - "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y) \ -\ ==> F : X guarantees Y"; -by (simp_tac (simpset() addsimps [guar_def, component_def]) 1); -by (blast_tac (claset() addIs prems) 1); -qed "guaranteesI"; - -Goalw [guar_def, component_def] - "[| F : X guarantees Y; F ok G; F Join G : X |] \ -\ ==> F Join G : Y"; -by (Blast_tac 1); -qed "guaranteesD"; - -(*This version of guaranteesD matches more easily in the conclusion - The major premise can no longer be F<=H since we need to reason about G*) -Goalw [guar_def] - "[| F : X guarantees Y; F Join G = H; H : X; F ok G |] \ -\ ==> H : Y"; -by (Blast_tac 1); -qed "component_guaranteesD"; - -Goalw [guar_def] - "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"; -by (Blast_tac 1); -qed "guarantees_weaken"; - -Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV"; -by (Blast_tac 1); -qed "subset_imp_guarantees_UNIV"; - -(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) -Goalw [guar_def] "X <= Y ==> F : X guarantees Y"; -by (Blast_tac 1); -qed "subset_imp_guarantees"; - -(*Remark at end of section 4.1 *) - -Goalw [guar_def] "ex_prop Y ==> (Y = UNIV guarantees Y)"; -by (full_simp_tac (simpset() addsimps [ex_prop_equiv]) 1); -by Safe_tac; -by (dres_inst_tac [("x", "x")] spec 1); -by (dres_inst_tac [("x", "x")] spec 2); -by (dtac sym 2); -by (ALLGOALS(etac iffE)); -by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def]))); -by (REPEAT(Blast_tac 1)); -qed "ex_prop_imp"; - -Goalw [guar_def] "(Y = UNIV guarantees Y) ==> ex_prop(Y)"; -by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); -by Safe_tac; -by (ALLGOALS(full_simp_tac (simpset() addsimps [component_of_def]))); -by (dtac sym 2); -by (ALLGOALS(etac equalityE)); -by (REPEAT(Blast_tac 1)); -qed "guarantees_imp"; - -Goal "(ex_prop Y) = (Y = UNIV guarantees Y)"; -by (rtac iffI 1); -by (rtac ex_prop_imp 1); -by (rtac guarantees_imp 2); -by (ALLGOALS(Asm_simp_tac)); -qed "ex_prop_equiv2"; - - -(** Distributive laws. Re-orient to perform miniscoping **) - -Goalw [guar_def] - "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)"; -by (Blast_tac 1); -qed "guarantees_UN_left"; - -Goalw [guar_def] - "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"; -by (Blast_tac 1); -qed "guarantees_Un_left"; - -Goalw [guar_def] - "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"; -by (Blast_tac 1); -qed "guarantees_INT_right"; - -Goalw [guar_def] - "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"; -by (Blast_tac 1); -qed "guarantees_Int_right"; - -Goal "[| F : Z guarantees X; F : Z guarantees Y |] \ -\ ==> F : Z guarantees (X Int Y)"; -by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); -qed "guarantees_Int_right_I"; - -Goal "(F : X guarantees (INTER I Y)) = \ -\ (ALL i:I. F : X guarantees (Y i))"; -by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1); -qed "guarantees_INT_right_iff"; - -Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))"; -by (Blast_tac 1); -qed "shunting"; - -Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X"; -by (Blast_tac 1); -qed "contrapositive"; - -(** The following two can be expressed using intersection and subset, which - is more faithful to the text but looks cryptic. -**) - -Goalw [guar_def] - "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\ -\ ==> F : (V Int Y) guarantees Z"; -by (Blast_tac 1); -qed "combining1"; - -Goalw [guar_def] - "[| F : V guarantees (X Un Y); F : Y guarantees Z |]\ -\ ==> F : V guarantees (X Un Z)"; -by (Blast_tac 1); -qed "combining2"; - -(** The following two follow Chandy-Sanders, but the use of object-quantifiers - does not suit Isabelle... **) - -(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *) -Goalw [guar_def] - "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"; -by (Blast_tac 1); -qed "all_guarantees"; - -(*Premises should be [| F: X guarantees Y i; i: I |] *) -Goalw [guar_def] - "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"; -by (Blast_tac 1); -qed "ex_guarantees"; - - -(*** Additional guarantees laws, by lcp ***) - -Goalw [guar_def] - "[| F: U guarantees V; G: X guarantees Y; F ok G |] \ -\ ==> F Join G: (U Int X) guarantees (V Int Y)"; -by (Simp_tac 1); -by Safe_tac; -by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); -by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); -by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); -by (asm_simp_tac (simpset() addsimps Join_ac) 1); -qed "guarantees_Join_Int"; - -Goalw [guar_def] - "[| F: U guarantees V; G: X guarantees Y; F ok G |] \ -\ ==> F Join G: (U Un X) guarantees (V Un Y)"; -by (Simp_tac 1); -by Safe_tac; -by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); -by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); -by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); -by (asm_simp_tac (simpset() addsimps Join_ac) 1); -qed "guarantees_Join_Un"; - -Goalw [guar_def] - "[| ALL i:I. F i : X i guarantees Y i; OK I F |] \ -\ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"; -by Auto_tac; -by (ball_tac 1); -by (rename_tac "i" 1); -by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1); -by (auto_tac - (claset() addIs [OK_imp_ok], - simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb])); -qed "guarantees_JN_INT"; - -Goalw [guar_def] - "[| ALL i:I. F i : X i guarantees Y i; OK I F |] \ -\ ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)"; -by Auto_tac; -by (ball_tac 1); -by (rename_tac "i" 1); -by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1); -by (auto_tac - (claset() addIs [OK_imp_ok], - simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb])); -qed "guarantees_JN_UN"; - - -(*** guarantees laws for breaking down the program, by lcp ***) - -Goalw [guar_def] - "[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"; -by (Simp_tac 1); -by Safe_tac; -by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); -qed "guarantees_Join_I1"; - -Goal "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"; -by (asm_full_simp_tac (simpset() addsimps [inst "G" "G" Join_commute, - inst "G" "G" ok_commute]) 1); -by (blast_tac (claset() addIs [guarantees_Join_I1]) 1); -qed "guarantees_Join_I2"; - -Goalw [guar_def] - "[| i : I; F i: X guarantees Y; OK I F |] \ -\ ==> (JN i:I. (F i)) : X guarantees Y"; -by (Clarify_tac 1); -by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1); -by (auto_tac (claset() addIs [OK_imp_ok], - simpset() addsimps [JN_Join_diff, JN_Join_diff, Join_assoc RS sym])); -qed "guarantees_JN_I"; - - -(*** well-definedness ***) - -Goalw [welldef_def] "F Join G: welldef ==> F: welldef"; -by Auto_tac; -qed "Join_welldef_D1"; - -Goalw [welldef_def] "F Join G: welldef ==> G: welldef"; -by Auto_tac; -qed "Join_welldef_D2"; - -(*** refinement ***) - -Goalw [refines_def] "F refines F wrt X"; -by (Blast_tac 1); -qed "refines_refl"; - -(* Goalw [refines_def] - "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X"; -by Auto_tac; -qed "refines_trans"; *) - - - -Goalw [strict_ex_prop_def] - "strict_ex_prop X \ -\ ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) \ -\ = (F:X --> G:X)"; -by Auto_tac; -qed "strict_ex_refine_lemma"; - -Goalw [strict_ex_prop_def] - "strict_ex_prop X \ -\ ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \ -\ (F: welldef Int X --> G:X)"; -by Safe_tac; -by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1); -by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], simpset())); -qed "strict_ex_refine_lemma_v"; - -Goal "[| strict_ex_prop X; \ -\ ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \ -\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; -by (res_inst_tac [("x","SKIP")] allE 1 - THEN assume_tac 1); -by (asm_full_simp_tac - (simpset() addsimps [refines_def, iso_refines_def, - strict_ex_refine_lemma_v]) 1); -qed "ex_refinement_thm"; - - -Goalw [strict_uv_prop_def] - "strict_uv_prop X \ -\ ==> (ALL H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)"; -by (Blast_tac 1); -qed "strict_uv_refine_lemma"; - -Goalw [strict_uv_prop_def] - "strict_uv_prop X \ -\ ==> (ALL H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = \ -\ (F: welldef Int X --> G:X)"; -by Safe_tac; -by (eres_inst_tac [("x","SKIP"), ("P", "%H. ?PP H --> ?RR H")] allE 1); -by (auto_tac (claset() addDs [Join_welldef_D1, Join_welldef_D2], - simpset())); -qed "strict_uv_refine_lemma_v"; - -Goal "[| strict_uv_prop X; \ -\ ALL H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] \ -\ ==> (G refines F wrt X) = (G iso_refines F wrt X)"; -by (res_inst_tac [("x","SKIP")] allE 1 - THEN assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps [refines_def, iso_refines_def, - strict_uv_refine_lemma_v]) 1); -qed "uv_refinement_thm"; - -(* Added by Sidi Ehmety from Chandy & Sander, section 6 *) -Goalw [guar_def, component_of_def] -"(F:X guarantees Y) = (ALL H. H:X \\ (F component_of H \\ H:Y))"; -by Auto_tac; -qed "guarantees_equiv"; - -Goalw [wg_def] "!!X. F:(X guarantees Y) ==> X <= (wg F Y)"; -by Auto_tac; -qed "wg_weakest"; - -Goalw [wg_def, guar_def] "F:((wg F Y) guarantees Y)"; -by (Blast_tac 1); -qed "wg_guarantees"; - -Goalw [wg_def] - "(H: wg F X) = (F component_of H --> H:X)"; -by (simp_tac (simpset() addsimps [guarantees_equiv]) 1); -by (rtac iffI 1); -by (res_inst_tac [("x", "{H}")] exI 2); -by (REPEAT(Blast_tac 1)); -qed "wg_equiv"; - - -Goal -"F component_of H ==> (H:wg F X) = (H:X)"; -by (asm_simp_tac (simpset() addsimps [wg_equiv]) 1); -qed "component_of_wg"; - - -Goal -"ALL FF. finite FF & FF Int X ~= {} --> OK FF (%F. F) \ -\ --> (ALL F:FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))"; -by (Clarify_tac 1); -by (subgoal_tac "F component_of (JN F:FF. F)" 1); -by (dres_inst_tac [("X", "X")] component_of_wg 1); -by (Asm_full_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [component_of_def]) 1); -by (res_inst_tac [("x", "JN F:(FF-{F}). F")] exI 1); -by (auto_tac (claset() addIs [JN_Join_diff] addDs [ok_sym], - simpset() addsimps [OK_iff_ok])); -qed "wg_finite"; - -Goal "ex_prop X ==> (F:X) = (ALL H. H : wg F X)"; -by (full_simp_tac (simpset() addsimps [ex_prop_equiv, wg_equiv]) 1); -by (Blast_tac 1); -qed "wg_ex_prop"; - -(** From Charpentier and Chandy "Theorems About Composition" **) -(* Proposition 2 *) -Goalw [wx_def] "(wx X)<=X"; -by Auto_tac; -qed "wx_subset"; - -Goalw [wx_def] -"ex_prop (wx X)"; -by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); -by Safe_tac; -by (Blast_tac 1); -by Auto_tac; -qed "wx_ex_prop"; - -Goalw [wx_def] -"ALL Z. Z<= X --> ex_prop Z --> Z <= wx X"; -by Auto_tac; -qed "wx_weakest"; - - -(* Proposition 6 *) -Goalw [ex_prop_def] - "ex_prop({F. ALL G. F ok G --> F Join G:X})"; -by Safe_tac; -by (dres_inst_tac [("x", "G Join Ga")] spec 1); -by (force_tac (claset(), simpset() addsimps [ok_Join_iff1, Join_assoc]) 1); -by (dres_inst_tac [("x", "F Join Ga")] spec 1); -by (full_simp_tac (simpset() addsimps [ok_Join_iff1]) 1); -by Safe_tac; -by (asm_simp_tac (simpset() addsimps [ok_commute]) 1); -by (subgoal_tac "F Join G = G Join F" 1); -by (asm_simp_tac (simpset() addsimps [Join_assoc]) 1); -by (simp_tac (simpset() addsimps [Join_commute]) 1); -qed "wx'_ex_prop"; - -(* Equivalence with the other definition of wx *) - -Goalw [wx_def] - "wx X = {F. ALL G. F ok G --> (F Join G):X}"; -by Safe_tac; -by (full_simp_tac (simpset() addsimps [ex_prop_def]) 1); -by (dres_inst_tac [("x", "x")] spec 1); -by (dres_inst_tac [("x", "G")] spec 1); -by (forw_inst_tac [("c", "x Join G")] subsetD 1); -by Safe_tac; -by (Simp_tac 1); -by (res_inst_tac [("x", "{F. ALL G. F ok G --> F Join G:X}")] exI 1); -by Safe_tac; -by (rtac wx'_ex_prop 2); -by (rotate_tac 1 1); -by (dres_inst_tac [("x", "SKIP")] spec 1); -by Auto_tac; -qed "wx_equiv"; - - -(* Propositions 7 to 11 are about this second definition of wx. And - they are the same as the ones proved for the first definition of wx by equivalence *) - -(* Proposition 12 *) -(* Main result of the paper *) -Goalw [guar_def] - "(X guarantees Y) = wx(-X Un Y)"; -by (simp_tac (simpset() addsimps [wx_equiv]) 1); -qed "guarantees_wx_eq"; - -(* {* Corollary, but this result has already been proved elsewhere *} - "ex_prop(X guarantees Y)"; - by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1); - qed "guarantees_ex_prop"; -*) - -(* Rules given in section 7 of Chandy and Sander's - Reasoning About Program composition paper *) - -Goal "Init F <= A ==> F:(stable A) guarantees (Always A)"; -by (rtac guaranteesI 1); -by (simp_tac (simpset() addsimps [Join_commute]) 1); -by (rtac stable_Join_Always1 1); -by (ALLGOALS(asm_full_simp_tac (simpset() - addsimps [invariant_def, Join_stable]))); -qed "stable_guarantees_Always"; - -(* To be moved to WFair.ML *) -Goal "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B"; -by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1); -by (dres_inst_tac [("B", "A-B")] transient_strengthen 2); -by (rtac (ensuresI RS leadsTo_Basis) 3); -by (ALLGOALS(Blast_tac)); -qed "leadsTo_Basis'"; - - - -Goal "F:transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"; -by (rtac guaranteesI 1); -by (rtac leadsTo_Basis' 1); -by (dtac constrains_weaken_R 1); -by (assume_tac 2); -by (Blast_tac 1); -by (blast_tac (claset() addIs [Join_transient_I1]) 1); -qed "constrains_guarantees_leadsTo"; - - - - - - - diff -r 3b6ff7ceaf27 -r d1811693899c src/HOL/UNITY/Guar.thy --- a/src/HOL/UNITY/Guar.thy Wed Jan 29 16:29:38 2003 +0100 +++ b/src/HOL/UNITY/Guar.thy Wed Jan 29 16:34:51 2003 +0100 @@ -18,36 +18,39 @@ *) -Guar = Comp + +theory Guar = Comp: instance program :: (type) order - (component_refl, component_trans, component_antisym, - program_less_le) + by (intro_classes, + (assumption | rule component_refl component_trans component_antisym + program_less_le)+) + constdefs (*Existential and Universal properties. I formalize the two-program case, proving equivalence with Chandy and Sanders's n-ary definitions*) - ex_prop :: 'a program set => bool - "ex_prop X == ALL F G. F ok G -->F:X | G: X --> (F Join G) : X" + ex_prop :: "'a program set => bool" + "ex_prop X == \F G. F ok G -->F:X | G: X --> (F Join G) : X" - strict_ex_prop :: 'a program set => bool - "strict_ex_prop X == ALL F G. F ok G --> (F:X | G: X) = (F Join G : X)" + strict_ex_prop :: "'a program set => bool" + "strict_ex_prop X == \F G. F ok G --> (F:X | G: X) = (F Join G : X)" - uv_prop :: 'a program set => bool - "uv_prop X == SKIP : X & (ALL F G. F ok G --> F:X & G: X --> (F Join G) : X)" + uv_prop :: "'a program set => bool" + "uv_prop X == SKIP : X & (\F G. F ok G --> F:X & G: X --> (F Join G) : X)" - strict_uv_prop :: 'a program set => bool - "strict_uv_prop X == SKIP : X & (ALL F G. F ok G -->(F:X & G: X) = (F Join G : X))" + strict_uv_prop :: "'a program set => bool" + "strict_uv_prop X == + SKIP : X & (\F G. F ok G --> (F:X & G: X) = (F Join G : X))" - guar :: ['a program set, 'a program set] => 'a program set + guar :: "['a program set, 'a program set] => 'a program set" (infixl "guarantees" 55) (*higher than membership, lower than Co*) - "X guarantees Y == {F. ALL G. F ok G --> F Join G : X --> F Join G : Y}" + "X guarantees Y == {F. \G. F ok G --> F Join G : X --> F Join G : Y}" (* Weakest guarantees *) - wg :: ['a program, 'a program set] => 'a program set + wg :: "['a program, 'a program set] => 'a program set" "wg F Y == Union({X. F:X guarantees Y})" (* Weakest existential property stronger than X *) @@ -55,17 +58,484 @@ "wx X == Union({Y. Y<=X & ex_prop Y})" (*Ill-defined programs can arise through "Join"*) - welldef :: 'a program set + welldef :: "'a program set" "welldef == {F. Init F ~= {}}" - refines :: ['a program, 'a program, 'a program set] => bool + refines :: "['a program, 'a program, 'a program set] => bool" ("(3_ refines _ wrt _)" [10,10,10] 10) "G refines F wrt X == - ALL H. (F ok H & G ok H & F Join H:welldef Int X) --> (G Join H:welldef Int X)" + \H. (F ok H & G ok H & F Join H : welldef Int X) --> + (G Join H : welldef Int X)" - iso_refines :: ['a program, 'a program, 'a program set] => bool + iso_refines :: "['a program, 'a program, 'a program set] => bool" ("(3_ iso'_refines _ wrt _)" [10,10,10] 10) "G iso_refines F wrt X == F : welldef Int X --> G : welldef Int X" + +lemma OK_insert_iff: + "(OK (insert i I) F) = + (if i:I then OK I F else OK I F & (F i ok JOIN I F))" +by (auto intro: ok_sym simp add: OK_iff_ok) + + +(*** existential properties ***) +lemma ex1 [rule_format (no_asm)]: + "[| ex_prop X; finite GG |] ==> + GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X" +apply (unfold ex_prop_def) +apply (erule finite_induct) +apply (auto simp add: OK_insert_iff Int_insert_left) +done + + +lemma ex2: + "\GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X + ==> ex_prop X" +apply (unfold ex_prop_def, clarify) +apply (drule_tac x = "{F,G}" in spec) +apply (auto dest: ok_sym simp add: OK_iff_ok) +done + + +(*Chandy & Sanders take this as a definition*) +lemma ex_prop_finite: + "ex_prop X = + (\GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)" +by (blast intro: ex1 ex2) + + +(*Their "equivalent definition" given at the end of section 3*) +lemma ex_prop_equiv: + "ex_prop X = (\G. G:X = (\H. (G component_of H) --> H: X))" +apply auto +apply (unfold ex_prop_def component_of_def, safe) +apply blast +apply blast +apply (subst Join_commute) +apply (drule ok_sym, blast) +done + + +(*** universal properties ***) +lemma uv1 [rule_format]: + "[| uv_prop X; finite GG |] + ==> GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X" +apply (unfold uv_prop_def) +apply (erule finite_induct) +apply (auto simp add: Int_insert_left OK_insert_iff) +done + +lemma uv2: + "\GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X + ==> uv_prop X" +apply (unfold uv_prop_def) +apply (rule conjI) + apply (drule_tac x = "{}" in spec) + prefer 2 + apply clarify + apply (drule_tac x = "{F,G}" in spec) +apply (auto dest: ok_sym simp add: OK_iff_ok) +done + +(*Chandy & Sanders take this as a definition*) +lemma uv_prop_finite: + "uv_prop X = + (\GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G): X)" +by (blast intro: uv1 uv2) + +(*** guarantees ***) + +lemma guaranteesI: + "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y) + ==> F : X guarantees Y" +by (simp add: guar_def component_def) + +lemma guaranteesD: + "[| F : X guarantees Y; F ok G; F Join G : X |] + ==> F Join G : Y" +by (unfold guar_def component_def, blast) + +(*This version of guaranteesD matches more easily in the conclusion + The major premise can no longer be F<=H since we need to reason about G*) +lemma component_guaranteesD: + "[| F : X guarantees Y; F Join G = H; H : X; F ok G |] + ==> H : Y" +by (unfold guar_def, blast) + +lemma guarantees_weaken: + "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'" +by (unfold guar_def, blast) + +lemma subset_imp_guarantees_UNIV: "X <= Y ==> X guarantees Y = UNIV" +by (unfold guar_def, blast) + +(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) +lemma subset_imp_guarantees: "X <= Y ==> F : X guarantees Y" +by (unfold guar_def, blast) + +(*Remark at end of section 4.1 *) + +lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)" +apply (simp (no_asm_use) add: guar_def ex_prop_equiv) +apply safe + apply (drule_tac x = x in spec) + apply (drule_tac [2] x = x in spec) + apply (drule_tac [2] sym) +apply (auto simp add: component_of_def) +done + +lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)" +apply (simp (no_asm_use) add: guar_def ex_prop_equiv) +apply safe +apply (auto simp add: component_of_def dest: sym) +done + +lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)" +apply (rule iffI) +apply (rule ex_prop_imp) +apply (auto simp add: guarantees_imp) +done + + +(** Distributive laws. Re-orient to perform miniscoping **) + +lemma guarantees_UN_left: + "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)" +by (unfold guar_def, blast) + +lemma guarantees_Un_left: + "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)" +by (unfold guar_def, blast) + +lemma guarantees_INT_right: + "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)" +by (unfold guar_def, blast) + +lemma guarantees_Int_right: + "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)" +by (unfold guar_def, blast) + +lemma guarantees_Int_right_I: + "[| F : Z guarantees X; F : Z guarantees Y |] + ==> F : Z guarantees (X Int Y)" +by (simp add: guarantees_Int_right) + +lemma guarantees_INT_right_iff: + "(F : X guarantees (INTER I Y)) = (\i\I. F : X guarantees (Y i))" +by (simp add: guarantees_INT_right) + +lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X Un Y))" +by (unfold guar_def, blast) + +lemma contrapositive: "(X guarantees Y) = -Y guarantees -X" +by (unfold guar_def, blast) + +(** The following two can be expressed using intersection and subset, which + is more faithful to the text but looks cryptic. +**) + +lemma combining1: + "[| F : V guarantees X; F : (X Int Y) guarantees Z |] + ==> F : (V Int Y) guarantees Z" + +by (unfold guar_def, blast) + +lemma combining2: + "[| F : V guarantees (X Un Y); F : Y guarantees Z |] + ==> F : V guarantees (X Un Z)" +by (unfold guar_def, blast) + +(** The following two follow Chandy-Sanders, but the use of object-quantifiers + does not suit Isabelle... **) + +(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *) +lemma all_guarantees: + "\i\I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)" +by (unfold guar_def, blast) + +(*Premises should be [| F: X guarantees Y i; i: I |] *) +lemma ex_guarantees: + "\i\I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)" +by (unfold guar_def, blast) + + +(*** Additional guarantees laws, by lcp ***) + +lemma guarantees_Join_Int: + "[| F: U guarantees V; G: X guarantees Y; F ok G |] + ==> F Join G: (U Int X) guarantees (V Int Y)" +apply (unfold guar_def) +apply (simp (no_asm)) +apply safe +apply (simp add: Join_assoc) +apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ") +apply (simp add: ok_commute) +apply (simp (no_asm_simp) add: Join_ac) +done + +lemma guarantees_Join_Un: + "[| F: U guarantees V; G: X guarantees Y; F ok G |] + ==> F Join G: (U Un X) guarantees (V Un Y)" +apply (unfold guar_def) +apply (simp (no_asm)) +apply safe +apply (simp add: Join_assoc) +apply (subgoal_tac "F Join G Join Ga = G Join (F Join Ga) ") +apply (simp add: ok_commute) +apply (simp (no_asm_simp) add: Join_ac) +done + +lemma guarantees_JN_INT: + "[| \i\I. F i : X i guarantees Y i; OK I F |] + ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)" +apply (unfold guar_def, auto) +apply (drule bspec, assumption) +apply (rename_tac "i") +apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec) +apply (auto intro: OK_imp_ok + simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) +done + +lemma guarantees_JN_UN: + "[| \i\I. F i : X i guarantees Y i; OK I F |] + ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)" +apply (unfold guar_def, auto) +apply (drule bspec, assumption) +apply (rename_tac "i") +apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec) +apply (auto intro: OK_imp_ok + simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb) +done + + +(*** guarantees laws for breaking down the program, by lcp ***) + +lemma guarantees_Join_I1: + "[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y" +apply (unfold guar_def) +apply (simp (no_asm)) +apply safe +apply (simp add: Join_assoc) +done + +lemma guarantees_Join_I2: + "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y" +apply (simp add: Join_commute [of _ G] ok_commute [of _ G]) +apply (blast intro: guarantees_Join_I1) +done + +lemma guarantees_JN_I: + "[| i : I; F i: X guarantees Y; OK I F |] + ==> (JN i:I. (F i)) : X guarantees Y" +apply (unfold guar_def, clarify) +apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec) +apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric]) +done + + +(*** well-definedness ***) + +lemma Join_welldef_D1: "F Join G: welldef ==> F: welldef" +by (unfold welldef_def, auto) + +lemma Join_welldef_D2: "F Join G: welldef ==> G: welldef" +by (unfold welldef_def, auto) + +(*** refinement ***) + +lemma refines_refl: "F refines F wrt X" +by (unfold refines_def, blast) + + +(* Goalw [refines_def] + "[| H refines G wrt X; G refines F wrt X |] ==> H refines F wrt X" +by Auto_tac +qed "refines_trans"; *) + + + +lemma strict_ex_refine_lemma: + "strict_ex_prop X + ==> (\H. F ok H & G ok H & F Join H : X --> G Join H : X) + = (F:X --> G:X)" +by (unfold strict_ex_prop_def, auto) + +lemma strict_ex_refine_lemma_v: + "strict_ex_prop X + ==> (\H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = + (F: welldef Int X --> G:X)" +apply (unfold strict_ex_prop_def, safe) +apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE) +apply (auto dest: Join_welldef_D1 Join_welldef_D2) +done + +lemma ex_refinement_thm: + "[| strict_ex_prop X; + \H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |] + ==> (G refines F wrt X) = (G iso_refines F wrt X)" +apply (rule_tac x = SKIP in allE, assumption) +apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v) +done + + +lemma strict_uv_refine_lemma: + "strict_uv_prop X ==> + (\H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)" +by (unfold strict_uv_prop_def, blast) + +lemma strict_uv_refine_lemma_v: + "strict_uv_prop X + ==> (\H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) = + (F: welldef Int X --> G:X)" +apply (unfold strict_uv_prop_def, safe) +apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE) +apply (auto dest: Join_welldef_D1 Join_welldef_D2) +done + +lemma uv_refinement_thm: + "[| strict_uv_prop X; + \H. F ok H & G ok H & F Join H : welldef Int X --> + G Join H : welldef |] + ==> (G refines F wrt X) = (G iso_refines F wrt X)" +apply (rule_tac x = SKIP in allE, assumption) +apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v) +done + +(* Added by Sidi Ehmety from Chandy & Sander, section 6 *) +lemma guarantees_equiv: + "(F:X guarantees Y) = (\H. H:X \ (F component_of H \ H:Y))" +by (unfold guar_def component_of_def, auto) + +lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X <= (wg F Y)" +by (unfold wg_def, auto) + +lemma wg_guarantees: "F:((wg F Y) guarantees Y)" +by (unfold wg_def guar_def, blast) + +lemma wg_equiv: + "(H: wg F X) = (F component_of H --> H:X)" +apply (unfold wg_def) +apply (simp (no_asm) add: guarantees_equiv) +apply (rule iffI) +apply (rule_tac [2] x = "{H}" in exI) +apply (blast+) +done + + +lemma component_of_wg: "F component_of H ==> (H:wg F X) = (H:X)" +by (simp add: wg_equiv) + +lemma wg_finite: + "\FF. finite FF & FF Int X ~= {} --> OK FF (%F. F) + --> (\F\FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))" +apply clarify +apply (subgoal_tac "F component_of (JN F:FF. F) ") +apply (drule_tac X = X in component_of_wg, simp) +apply (simp add: component_of_def) +apply (rule_tac x = "JN F: (FF-{F}) . F" in exI) +apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok) +done + +lemma wg_ex_prop: "ex_prop X ==> (F:X) = (\H. H : wg F X)" +apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv) +apply blast +done + +(** From Charpentier and Chandy "Theorems About Composition" **) +(* Proposition 2 *) +lemma wx_subset: "(wx X)<=X" +by (unfold wx_def, auto) + +lemma wx_ex_prop: "ex_prop (wx X)" +apply (unfold wx_def) +apply (simp (no_asm) add: ex_prop_equiv) +apply safe +apply blast +apply auto +done + +lemma wx_weakest: "\Z. Z<= X --> ex_prop Z --> Z <= wx X" +by (unfold wx_def, auto) + +(* Proposition 6 *) +lemma wx'_ex_prop: "ex_prop({F. \G. F ok G --> F Join G:X})" +apply (unfold ex_prop_def, safe) +apply (drule_tac x = "G Join Ga" in spec) +apply (force simp add: ok_Join_iff1 Join_assoc) +apply (drule_tac x = "F Join Ga" in spec) +apply (simp (no_asm_use) add: ok_Join_iff1) +apply safe +apply (simp (no_asm_simp) add: ok_commute) +apply (subgoal_tac "F Join G = G Join F") +apply (simp (no_asm_simp) add: Join_assoc) +apply (simp (no_asm) add: Join_commute) +done + +(* Equivalence with the other definition of wx *) + +lemma wx_equiv: + "wx X = {F. \G. F ok G --> (F Join G):X}" + +apply (unfold wx_def, safe) +apply (simp (no_asm_use) add: ex_prop_def) +apply (drule_tac x = x in spec) +apply (drule_tac x = G in spec) +apply (frule_tac c = "x Join G" in subsetD, safe) +apply (simp (no_asm)) +apply (rule_tac x = "{F. \G. F ok G --> F Join G:X}" in exI, safe) +apply (rule_tac [2] wx'_ex_prop) +apply (rotate_tac 1) +apply (drule_tac x = SKIP in spec, auto) +done + + +(* Propositions 7 to 11 are about this second definition of wx. And + they are the same as the ones proved for the first definition of wx by equivalence *) + +(* Proposition 12 *) +(* Main result of the paper *) +lemma guarantees_wx_eq: + "(X guarantees Y) = wx(-X Un Y)" +apply (unfold guar_def) +apply (simp (no_asm) add: wx_equiv) +done + +(* {* Corollary, but this result has already been proved elsewhere *} + "ex_prop(X guarantees Y)" + by (simp_tac (simpset() addsimps [guar_wx_iff, wx_ex_prop]) 1); + qed "guarantees_ex_prop"; +*) + +(* Rules given in section 7 of Chandy and Sander's + Reasoning About Program composition paper *) + +lemma stable_guarantees_Always: + "Init F <= A ==> F:(stable A) guarantees (Always A)" +apply (rule guaranteesI) +apply (simp (no_asm) add: Join_commute) +apply (rule stable_Join_Always1) +apply (simp_all add: invariant_def Join_stable) +done + +(* To be moved to WFair.ML *) +lemma leadsTo_Basis': "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B" +apply (drule_tac B = "A-B" in constrains_weaken_L) +apply (drule_tac [2] B = "A-B" in transient_strengthen) +apply (rule_tac [3] ensuresI [THEN leadsTo_Basis]) +apply (blast+) +done + + + +lemma constrains_guarantees_leadsTo: + "F : transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))" +apply (rule guaranteesI) +apply (rule leadsTo_Basis') +apply (drule constrains_weaken_R) +prefer 2 apply assumption +apply blast +apply (blast intro: Join_transient_I1) +done + end diff -r 3b6ff7ceaf27 -r d1811693899c src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Wed Jan 29 16:29:38 2003 +0100 +++ b/src/HOL/UNITY/UNITY_tactics.ML Wed Jan 29 16:34:51 2003 +0100 @@ -6,6 +6,193 @@ Specialized UNITY tactics, and ML bindings of theorems *) +(*Union*) +val Init_SKIP = thm "Init_SKIP"; +val Acts_SKIP = thm "Acts_SKIP"; +val AllowedActs_SKIP = thm "AllowedActs_SKIP"; +val reachable_SKIP = thm "reachable_SKIP"; +val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff"; +val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff"; +val SKIP_in_stable = thm "SKIP_in_stable"; +val Init_Join = thm "Init_Join"; +val Acts_Join = thm "Acts_Join"; +val AllowedActs_Join = thm "AllowedActs_Join"; +val JN_empty = thm "JN_empty"; +val JN_insert = thm "JN_insert"; +val Init_JN = thm "Init_JN"; +val Acts_JN = thm "Acts_JN"; +val AllowedActs_JN = thm "AllowedActs_JN"; +val JN_cong = thm "JN_cong"; +val Join_commute = thm "Join_commute"; +val Join_assoc = thm "Join_assoc"; +val Join_left_commute = thm "Join_left_commute"; +val Join_SKIP_left = thm "Join_SKIP_left"; +val Join_SKIP_right = thm "Join_SKIP_right"; +val Join_absorb = thm "Join_absorb"; +val Join_left_absorb = thm "Join_left_absorb"; +val Join_ac = thms "Join_ac"; +val JN_absorb = thm "JN_absorb"; +val JN_Un = thm "JN_Un"; +val JN_constant = thm "JN_constant"; +val JN_Join_distrib = thm "JN_Join_distrib"; +val JN_Join_miniscope = thm "JN_Join_miniscope"; +val JN_Join_diff = thm "JN_Join_diff"; +val JN_constrains = thm "JN_constrains"; +val Join_constrains = thm "Join_constrains"; +val Join_unless = thm "Join_unless"; +val Join_constrains_weaken = thm "Join_constrains_weaken"; +val JN_constrains_weaken = thm "JN_constrains_weaken"; +val JN_stable = thm "JN_stable"; +val invariant_JN_I = thm "invariant_JN_I"; +val Join_stable = thm "Join_stable"; +val Join_increasing = thm "Join_increasing"; +val invariant_JoinI = thm "invariant_JoinI"; +val FP_JN = thm "FP_JN"; +val JN_transient = thm "JN_transient"; +val Join_transient = thm "Join_transient"; +val Join_transient_I1 = thm "Join_transient_I1"; +val Join_transient_I2 = thm "Join_transient_I2"; +val JN_ensures = thm "JN_ensures"; +val Join_ensures = thm "Join_ensures"; +val stable_Join_constrains = thm "stable_Join_constrains"; +val stable_Join_Always1 = thm "stable_Join_Always1"; +val stable_Join_Always2 = thm "stable_Join_Always2"; +val stable_Join_ensures1 = thm "stable_Join_ensures1"; +val stable_Join_ensures2 = thm "stable_Join_ensures2"; +val ok_SKIP1 = thm "ok_SKIP1"; +val ok_SKIP2 = thm "ok_SKIP2"; +val ok_Join_commute = thm "ok_Join_commute"; +val ok_commute = thm "ok_commute"; +val ok_sym = thm "ok_sym"; +val ok_iff_OK = thm "ok_iff_OK"; +val ok_Join_iff1 = thm "ok_Join_iff1"; +val ok_Join_iff2 = thm "ok_Join_iff2"; +val ok_Join_commute_I = thm "ok_Join_commute_I"; +val ok_JN_iff1 = thm "ok_JN_iff1"; +val ok_JN_iff2 = thm "ok_JN_iff2"; +val OK_iff_ok = thm "OK_iff_ok"; +val OK_imp_ok = thm "OK_imp_ok"; +val Allowed_SKIP = thm "Allowed_SKIP"; +val Allowed_Join = thm "Allowed_Join"; +val Allowed_JN = thm "Allowed_JN"; +val ok_iff_Allowed = thm "ok_iff_Allowed"; +val OK_iff_Allowed = thm "OK_iff_Allowed"; +val safety_prop_Acts_iff = thm "safety_prop_Acts_iff"; +val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed"; +val Allowed_eq = thm "Allowed_eq"; +val def_prg_Allowed = thm "def_prg_Allowed"; +val safety_prop_constrains = thm "safety_prop_constrains"; +val safety_prop_stable = thm "safety_prop_stable"; +val safety_prop_Int = thm "safety_prop_Int"; +val safety_prop_INTER1 = thm "safety_prop_INTER1"; +val safety_prop_INTER = thm "safety_prop_INTER"; +val def_UNION_ok_iff = thm "def_UNION_ok_iff"; + +(*Comp*) +val preserves_def = thm "preserves_def"; +val funPair_def = thm "funPair_def"; +val componentI = thm "componentI"; +val component_eq_subset = thm "component_eq_subset"; +val component_SKIP = thm "component_SKIP"; +val component_refl = thm "component_refl"; +val SKIP_minimal = thm "SKIP_minimal"; +val component_Join1 = thm "component_Join1"; +val component_Join2 = thm "component_Join2"; +val Join_absorb1 = thm "Join_absorb1"; +val Join_absorb2 = thm "Join_absorb2"; +val JN_component_iff = thm "JN_component_iff"; +val component_JN = thm "component_JN"; +val component_trans = thm "component_trans"; +val component_antisym = thm "component_antisym"; +val Join_component_iff = thm "Join_component_iff"; +val component_constrains = thm "component_constrains"; +val program_less_le = thm "program_less_le"; +val preservesI = thm "preservesI"; +val preserves_imp_eq = thm "preserves_imp_eq"; +val Join_preserves = thm "Join_preserves"; +val JN_preserves = thm "JN_preserves"; +val SKIP_preserves = thm "SKIP_preserves"; +val funPair_apply = thm "funPair_apply"; +val preserves_funPair = thm "preserves_funPair"; +val funPair_o_distrib = thm "funPair_o_distrib"; +val fst_o_funPair = thm "fst_o_funPair"; +val snd_o_funPair = thm "snd_o_funPair"; +val subset_preserves_o = thm "subset_preserves_o"; +val preserves_subset_stable = thm "preserves_subset_stable"; +val preserves_subset_increasing = thm "preserves_subset_increasing"; +val preserves_id_subset_stable = thm "preserves_id_subset_stable"; +val safety_prop_preserves = thm "safety_prop_preserves"; +val stable_localTo_stable2 = thm "stable_localTo_stable2"; +val Increasing_preserves_Stable = thm "Increasing_preserves_Stable"; +val component_of_imp_component = thm "component_of_imp_component"; +val component_of_refl = thm "component_of_refl"; +val component_of_SKIP = thm "component_of_SKIP"; +val component_of_trans = thm "component_of_trans"; +val strict_component_of_eq = thm "strict_component_of_eq"; +val localize_Init_eq = thm "localize_Init_eq"; +val localize_Acts_eq = thm "localize_Acts_eq"; +val localize_AllowedActs_eq = thm "localize_AllowedActs_eq"; + +(*Guar*) +val guar_def = thm "guar_def"; +val OK_insert_iff = thm "OK_insert_iff"; +val ex1 = thm "ex1"; +val ex2 = thm "ex2"; +val ex_prop_finite = thm "ex_prop_finite"; +val ex_prop_equiv = thm "ex_prop_equiv"; +val uv1 = thm "uv1"; +val uv2 = thm "uv2"; +val uv_prop_finite = thm "uv_prop_finite"; +val guaranteesI = thm "guaranteesI"; +val guaranteesD = thm "guaranteesD"; +val component_guaranteesD = thm "component_guaranteesD"; +val guarantees_weaken = thm "guarantees_weaken"; +val subset_imp_guarantees_UNIV = thm "subset_imp_guarantees_UNIV"; +val subset_imp_guarantees = thm "subset_imp_guarantees"; +val ex_prop_imp = thm "ex_prop_imp"; +val guarantees_imp = thm "guarantees_imp"; +val ex_prop_equiv2 = thm "ex_prop_equiv2"; +val guarantees_UN_left = thm "guarantees_UN_left"; +val guarantees_Un_left = thm "guarantees_Un_left"; +val guarantees_INT_right = thm "guarantees_INT_right"; +val guarantees_Int_right = thm "guarantees_Int_right"; +val guarantees_Int_right_I = thm "guarantees_Int_right_I"; +val guarantees_INT_right_iff = thm "guarantees_INT_right_iff"; +val shunting = thm "shunting"; +val contrapositive = thm "contrapositive"; +val combining1 = thm "combining1"; +val combining2 = thm "combining2"; +val all_guarantees = thm "all_guarantees"; +val ex_guarantees = thm "ex_guarantees"; +val guarantees_Join_Int = thm "guarantees_Join_Int"; +val guarantees_Join_Un = thm "guarantees_Join_Un"; +val guarantees_JN_INT = thm "guarantees_JN_INT"; +val guarantees_JN_UN = thm "guarantees_JN_UN"; +val guarantees_Join_I1 = thm "guarantees_Join_I1"; +val guarantees_Join_I2 = thm "guarantees_Join_I2"; +val guarantees_JN_I = thm "guarantees_JN_I"; +val Join_welldef_D1 = thm "Join_welldef_D1"; +val Join_welldef_D2 = thm "Join_welldef_D2"; +val refines_refl = thm "refines_refl"; +val ex_refinement_thm = thm "ex_refinement_thm"; +val uv_refinement_thm = thm "uv_refinement_thm"; +val guarantees_equiv = thm "guarantees_equiv"; +val wg_weakest = thm "wg_weakest"; +val wg_guarantees = thm "wg_guarantees"; +val wg_equiv = thm "wg_equiv"; +val component_of_wg = thm "component_of_wg"; +val wg_finite = thm "wg_finite"; +val wg_ex_prop = thm "wg_ex_prop"; +val wx_subset = thm "wx_subset"; +val wx_ex_prop = thm "wx_ex_prop"; +val wx_weakest = thm "wx_weakest"; +val wx'_ex_prop = thm "wx'_ex_prop"; +val wx_equiv = thm "wx_equiv"; +val guarantees_wx_eq = thm "guarantees_wx_eq"; +val stable_guarantees_Always = thm "stable_guarantees_Always"; +val leadsTo_Basis = thm "leadsTo_Basis"; +val constrains_guarantees_leadsTo = thm "constrains_guarantees_leadsTo"; + (*Extend*) val Restrict_iff = thm "Restrict_iff"; val Restrict_UNIV = thm "Restrict_UNIV"; diff -r 3b6ff7ceaf27 -r d1811693899c src/HOL/UNITY/Union.ML --- a/src/HOL/UNITY/Union.ML Wed Jan 29 16:29:38 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,471 +0,0 @@ -(* Title: HOL/UNITY/Union.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Unions of programs - -From Misra's Chapter 5: Asynchronous Compositions of Programs -*) - - -(** SKIP **) - -Goal "Init SKIP = UNIV"; -by (simp_tac (simpset() addsimps [SKIP_def]) 1); -qed "Init_SKIP"; - -Goal "Acts SKIP = {Id}"; -by (simp_tac (simpset() addsimps [SKIP_def]) 1); -qed "Acts_SKIP"; - -Goal "AllowedActs SKIP = UNIV"; -by (auto_tac (claset(), simpset() addsimps [SKIP_def])); -qed "AllowedActs_SKIP"; - -Addsimps [Init_SKIP, Acts_SKIP, AllowedActs_SKIP]; - -Goal "reachable SKIP = UNIV"; -by (force_tac (claset() addEs [reachable.induct] - addIs reachable.intrs, simpset()) 1); -qed "reachable_SKIP"; - -Addsimps [reachable_SKIP]; - -(** SKIP and safety properties **) - -Goalw [constrains_def] "(SKIP : A co B) = (A<=B)"; -by Auto_tac; -qed "SKIP_in_constrains_iff"; -AddIffs [SKIP_in_constrains_iff]; - -Goalw [Constrains_def] "(SKIP : A Co B) = (A<=B)"; -by Auto_tac; -qed "SKIP_in_Constrains_iff"; -AddIffs [SKIP_in_Constrains_iff]; - -Goalw [stable_def] "SKIP : stable A"; -by Auto_tac; -qed "SKIP_in_stable"; -AddIffs [SKIP_in_stable, SKIP_in_stable RS stable_imp_Stable]; - - -(** Join **) - -Goal "Init (F Join G) = Init F Int Init G"; -by (simp_tac (simpset() addsimps [Join_def]) 1); -qed "Init_Join"; - -Goal "Acts (F Join G) = Acts F Un Acts G"; -by (auto_tac (claset(), simpset() addsimps [Join_def])); -qed "Acts_Join"; - -Goal "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G"; -by (auto_tac (claset(), simpset() addsimps [Join_def])); -qed "AllowedActs_Join"; - -Addsimps [Init_Join, Acts_Join, AllowedActs_Join]; - - -(** JN **) - -Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP"; -by Auto_tac; -qed "JN_empty"; -Addsimps [JN_empty]; - -Goal "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)"; -by (rtac program_equalityI 1); -by (auto_tac (claset(), simpset() addsimps [JOIN_def, Join_def])); -qed "JN_insert"; -Addsimps[JN_empty, JN_insert]; - -Goal "Init (JN i:I. F i) = (INT i:I. Init (F i))"; -by (simp_tac (simpset() addsimps [JOIN_def]) 1); -qed "Init_JN"; - -Goal "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))"; -by (auto_tac (claset(), simpset() addsimps [JOIN_def])); -qed "Acts_JN"; - -Goal "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))"; -by (auto_tac (claset(), simpset() addsimps [JOIN_def])); -qed "AllowedActs_JN"; - -Addsimps [Init_JN, Acts_JN, AllowedActs_JN]; - -val prems = Goalw [JOIN_def] - "[| I=J; !!i. i:J ==> F i = G i |] ==> \ -\ (JN i:I. F i) = (JN i:J. G i)"; -by (asm_simp_tac (simpset() addsimps prems) 1); -qed "JN_cong"; - -Addcongs [JN_cong]; - - -(** Algebraic laws **) - -Goal "F Join G = G Join F"; -by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1); -qed "Join_commute"; - -Goal "(F Join G) Join H = F Join (G Join H)"; -by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc, insert_absorb]) 1); -qed "Join_assoc"; - -Goal "A Join (B Join C) = B Join (A Join C)"; -by(rtac ([Join_assoc,Join_commute] MRS - read_instantiate[("f","op Join")](thm"mk_left_commute")) 1); -qed "Join_left_commute"; - - -Goalw [Join_def, SKIP_def] "SKIP Join F = F"; -by (rtac program_equalityI 1); -by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb]))); -qed "Join_SKIP_left"; - -Goalw [Join_def, SKIP_def] "F Join SKIP = F"; -by (rtac program_equalityI 1); -by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb]))); -qed "Join_SKIP_right"; - -Addsimps [Join_SKIP_left, Join_SKIP_right]; - -Goalw [Join_def] "F Join F = F"; -by (rtac program_equalityI 1); -by Auto_tac; -qed "Join_absorb"; - -Addsimps [Join_absorb]; - -Goalw [Join_def] "F Join (F Join G) = F Join G"; -by (rtac program_equalityI 1); -by Auto_tac; -qed "Join_left_absorb"; - -(*Join is an AC-operator*) -val Join_ac = [Join_assoc, Join_left_absorb, Join_commute, Join_left_commute]; - - -(*** JN laws ***) - -(*Also follows by JN_insert and insert_absorb, but the proof is longer*) -Goal "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)"; -by (auto_tac (claset() addSIs [program_equalityI], simpset())); -qed "JN_absorb"; - -Goal "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))"; -by (auto_tac (claset() addSIs [program_equalityI], simpset())); -qed "JN_Un"; - -Goal "(JN i:I. c) = (if I={} then SKIP else c)"; -by (rtac program_equalityI 1); -by Auto_tac; -qed "JN_constant"; - -Goal "(JN i:I. F i Join G i) = (JN i:I. F i) Join (JN i:I. G i)"; -by (auto_tac (claset() addSIs [program_equalityI], simpset())); -qed "JN_Join_distrib"; - -Goal "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)"; -by (asm_simp_tac (simpset() addsimps [JN_Join_distrib, JN_constant]) 1); -by Auto_tac; -qed "JN_Join_miniscope"; - -(*Used to prove guarantees_JN_I*) -Goalw [JOIN_def, Join_def] "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F"; -by (rtac program_equalityI 1); -by Auto_tac; -qed "JN_Join_diff"; - - -(*** Safety: co, stable, FP ***) - -(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B. So an - alternative precondition is A<=B, but most proofs using this rule require - I to be nonempty for other reasons anyway.*) -Goalw [constrains_def, JOIN_def] - "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "JN_constrains"; - -Goal "(F Join G : A co B) = (F : A co B & G : A co B)"; -by (auto_tac - (claset(), - simpset() addsimps [constrains_def, Join_def])); -qed "Join_constrains"; - -Goal "(F Join G : A unless B) = (F : A unless B & G : A unless B)"; -by (simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1); -qed "Join_unless"; - -Addsimps [Join_constrains, Join_unless]; - -(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. - reachable (F Join G) could be much bigger than reachable F, reachable G -*) - - -Goal "[| F : A co A'; G : B co B' |] \ -\ ==> F Join G : (A Int B) co (A' Un B')"; -by (Simp_tac 1); -by (blast_tac (claset() addIs [constrains_weaken]) 1); -qed "Join_constrains_weaken"; - -(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*) -Goal "[| ALL i:I. F i : A i co A' i; i: I |] \ -\ ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)"; -by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1); -by (blast_tac (claset() addIs [constrains_weaken]) 1); -qed "JN_constrains_weaken"; - -Goal "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"; -by (asm_simp_tac - (simpset() addsimps [stable_def, constrains_def, JOIN_def]) 1); -qed "JN_stable"; - -Goal "[| ALL i:I. F i : invariant A; i : I |] \ -\ ==> (JN i:I. F i) : invariant A"; -by (asm_full_simp_tac (simpset() addsimps [invariant_def, JN_stable]) 1); -by (Blast_tac 1); -bind_thm ("invariant_JN_I", ballI RS result()); - -Goal "(F Join G : stable A) = \ -\ (F : stable A & G : stable A)"; -by (simp_tac (simpset() addsimps [stable_def]) 1); -qed "Join_stable"; - -Goal "(F Join G : increasing f) = \ -\ (F : increasing f & G : increasing f)"; -by (simp_tac (simpset() addsimps [increasing_def, Join_stable]) 1); -by (Blast_tac 1); -qed "Join_increasing"; - -Addsimps [Join_stable, Join_increasing]; - -Goal "[| F : invariant A; G : invariant A |] \ -\ ==> F Join G : invariant A"; -by (full_simp_tac (simpset() addsimps [invariant_def]) 1); -by (Blast_tac 1); -qed "invariant_JoinI"; - -Goal "FP (JN i:I. F i) = (INT i:I. FP (F i))"; -by (asm_simp_tac (simpset() addsimps [FP_def, JN_stable, INTER_def]) 1); -qed "FP_JN"; - - -(*** Progress: transient, ensures ***) - -Goal "i : I ==> \ -\ (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"; -by (auto_tac (claset(), - simpset() addsimps [transient_def, JOIN_def])); -qed "JN_transient"; - -Goal "F Join G : transient A = \ -\ (F : transient A | G : transient A)"; -by (auto_tac (claset(), - simpset() addsimps [bex_Un, transient_def, - Join_def])); -qed "Join_transient"; - -Addsimps [Join_transient]; - -Goal "F : transient A ==> F Join G : transient A"; -by (asm_simp_tac (simpset() addsimps [Join_transient]) 1); -qed "Join_transient_I1"; - -Goal "G : transient A ==> F Join G : transient A"; -by (asm_simp_tac (simpset() addsimps [Join_transient]) 1); -qed "Join_transient_I2"; - -(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *) -Goal "i : I ==> \ -\ (JN i:I. F i) : A ensures B = \ -\ ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))"; -by (auto_tac (claset(), - simpset() addsimps [ensures_def, JN_constrains, JN_transient])); -qed "JN_ensures"; - -Goalw [ensures_def] - "F Join G : A ensures B = \ -\ (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) & \ -\ (F : transient (A-B) | G : transient (A-B)))"; -by (auto_tac (claset(), simpset() addsimps [Join_transient])); -qed "Join_ensures"; - -Goalw [stable_def, constrains_def, Join_def] - "[| F : stable A; G : A co A' |] \ -\ ==> F Join G : A co A'"; -by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1); -by (Blast_tac 1); -qed "stable_Join_constrains"; - -(*Premise for G cannot use Always because F: Stable A is weaker than - G : stable A *) -Goal "[| F : stable A; G : invariant A |] ==> F Join G : Always A"; -by (full_simp_tac (simpset() addsimps [Always_def, invariant_def, - Stable_eq_stable]) 1); -by (force_tac(claset() addIs [stable_Int], simpset()) 1); -qed "stable_Join_Always1"; - -(*As above, but exchanging the roles of F and G*) -Goal "[| F : invariant A; G : stable A |] ==> F Join G : Always A"; -by (stac Join_commute 1); -by (blast_tac (claset() addIs [stable_Join_Always1]) 1); -qed "stable_Join_Always2"; - -Goal "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B"; -by (asm_simp_tac (simpset() addsimps [Join_ensures]) 1); -by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1); -by (etac constrains_weaken 1); -by Auto_tac; -qed "stable_Join_ensures1"; - -(*As above, but exchanging the roles of F and G*) -Goal "[| F : A ensures B; G : stable A |] ==> F Join G : A ensures B"; -by (stac Join_commute 1); -by (blast_tac (claset() addIs [stable_Join_ensures1]) 1); -qed "stable_Join_ensures2"; - - -(*** the ok and OK relations ***) - -Goal "SKIP ok F"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_SKIP1"; - -Goal "F ok SKIP"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_SKIP2"; - -AddIffs [ok_SKIP1, ok_SKIP2]; - -Goal "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_Join_commute"; - -Goal "(F ok G) = (G ok F)"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_commute"; - -bind_thm ("ok_sym", ok_commute RS iffD1); - -Goal "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"; -by (asm_full_simp_tac - (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, - OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1); -by (Blast_tac 1); -qed "ok_iff_OK"; - -Goal "F ok (G Join H) = (F ok G & F ok H)"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_Join_iff1"; - -Goal "(G Join H) ok F = (G ok F & H ok F)"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_Join_iff2"; -AddIffs [ok_Join_iff1, ok_Join_iff2]; - -(*useful? Not with the previous two around*) -Goal "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_Join_commute_I"; - -Goal "F ok (JOIN I G) = (ALL i:I. F ok G i)"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_JN_iff1"; - -Goal "(JOIN I G) ok F = (ALL i:I. G i ok F)"; -by (auto_tac (claset(), simpset() addsimps [ok_def])); -qed "ok_JN_iff2"; -AddIffs [ok_JN_iff1, ok_JN_iff2]; - -Goal "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))"; -by (auto_tac (claset(), simpset() addsimps [ok_def, OK_def])); -qed "OK_iff_ok"; - -Goal "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)"; -by (auto_tac (claset(), simpset() addsimps [OK_iff_ok])); -qed "OK_imp_ok"; - - -(*** Allowed ***) - -Goal "Allowed SKIP = UNIV"; -by (auto_tac (claset(), simpset() addsimps [Allowed_def])); -qed "Allowed_SKIP"; - -Goal "Allowed (F Join G) = Allowed F Int Allowed G"; -by (auto_tac (claset(), simpset() addsimps [Allowed_def])); -qed "Allowed_Join"; - -Goal "Allowed (JOIN I F) = (INT i:I. Allowed (F i))"; -by (auto_tac (claset(), simpset() addsimps [Allowed_def])); -qed "Allowed_JN"; - -Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN]; - -Goal "F ok G = (F : Allowed G & G : Allowed F)"; -by (simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1); -qed "ok_iff_Allowed"; - -Goal "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"; -by (auto_tac (claset(), simpset() addsimps [OK_iff_ok, ok_iff_Allowed])); -qed "OK_iff_Allowed"; - -(*** safety_prop, for reasoning about given instances of "ok" ***) - -Goal "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)"; -by (auto_tac (claset(), simpset() addsimps [safety_prop_def])); -qed "safety_prop_Acts_iff"; - -Goal "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)"; -by (auto_tac (claset(), - simpset() addsimps [Allowed_def, safety_prop_Acts_iff RS sym])); -qed "safety_prop_AllowedActs_iff_Allowed"; - -Goal "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X"; -by (asm_simp_tac (simpset() addsimps [Allowed_def, safety_prop_Acts_iff]) 1); -qed "Allowed_eq"; - -Goal "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |] \ -\ ==> Allowed F = X"; -by (asm_simp_tac (simpset() addsimps [Allowed_eq]) 1); -qed "def_prg_Allowed"; - -(*For safety_prop to hold, the property must be satisfiable!*) -Goal "safety_prop (A co B) = (A <= B)"; -by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def]) 1); -by (Blast_tac 1); -qed "safety_prop_constrains"; -AddIffs [safety_prop_constrains]; - -Goal "safety_prop (stable A)"; -by (simp_tac (simpset() addsimps [stable_def]) 1); -qed "safety_prop_stable"; -AddIffs [safety_prop_stable]; - -Goal "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)"; -by (full_simp_tac (simpset() addsimps [safety_prop_def]) 1); -by (Blast_tac 1); -qed "safety_prop_Int"; -Addsimps [safety_prop_Int]; - -Goal "(ALL i. safety_prop (X i)) ==> safety_prop (INT i. X i)"; -by (auto_tac (claset(), simpset() addsimps [safety_prop_def])); -by (Blast_tac 1); -bind_thm ("safety_prop_INTER1", allI RS result()); -Addsimps [safety_prop_INTER1]; - -Goal "(ALL i:I. safety_prop (X i)) ==> safety_prop (INT i:I. X i)"; -by (auto_tac (claset(), simpset() addsimps [safety_prop_def])); -by (Blast_tac 1); -bind_thm ("safety_prop_INTER", ballI RS result()); -Addsimps [safety_prop_INTER]; - -Goal "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] \ -\ ==> F ok G = (G : X & acts <= AllowedActs G)"; -by (auto_tac (claset(), simpset() addsimps [ok_def, safety_prop_Acts_iff])); -qed "def_UNION_ok_iff"; diff -r 3b6ff7ceaf27 -r d1811693899c src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Wed Jan 29 16:29:38 2003 +0100 +++ b/src/HOL/UNITY/Union.thy Wed Jan 29 16:34:51 2003 +0100 @@ -8,28 +8,28 @@ Partly from Misra's Chapter 5: Asynchronous Compositions of Programs *) -Union = SubstAx + FP + +theory Union = SubstAx + FP: constdefs (*FIXME: conjoin Init F Int Init G ~= {} *) - ok :: ['a program, 'a program] => bool (infixl 65) + ok :: "['a program, 'a program] => bool" (infixl "ok" 65) "F ok G == Acts F <= AllowedActs G & Acts G <= AllowedActs F" (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) - OK :: ['a set, 'a => 'b program] => bool + OK :: "['a set, 'a => 'b program] => bool" "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))" - JOIN :: ['a set, 'a => 'b program] => 'b program + JOIN :: "['a set, 'a => 'b program] => 'b program" "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i), INT i:I. AllowedActs (F i))" - Join :: ['a program, 'a program] => 'a program (infixl 65) + Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65) "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G, AllowedActs F Int AllowedActs G)" - SKIP :: 'a program + SKIP :: "'a program" "SKIP == mk_program (UNIV, {}, UNIV)" (*Characterizes safety properties. Used with specifying AllowedActs*) @@ -37,8 +37,8 @@ "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)" syntax - "@JOIN1" :: [pttrns, 'b set] => 'b set ("(3JN _./ _)" 10) - "@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10) + "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10) + "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10) translations "JN x:A. B" == "JOIN A (%x. B)" @@ -46,9 +46,375 @@ "JN x. B" == "JOIN UNIV (%x. B)" syntax (xsymbols) - SKIP :: 'a program ("\\") - "op Join" :: ['a program, 'a program] => 'a program (infixl "\\" 65) - "@JOIN1" :: [pttrns, 'b set] => 'b set ("(3\\ _./ _)" 10) - "@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3\\ _:_./ _)" 10) + SKIP :: "'a program" ("\") + "op Join" :: "['a program, 'a program] => 'a program" (infixl "\" 65) + "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\ _./ _)" 10) + "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\ _:_./ _)" 10) + + +(** SKIP **) + +lemma Init_SKIP [simp]: "Init SKIP = UNIV" +by (simp add: SKIP_def) + +lemma Acts_SKIP [simp]: "Acts SKIP = {Id}" +by (simp add: SKIP_def) + +lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV" +by (auto simp add: SKIP_def) + +lemma reachable_SKIP [simp]: "reachable SKIP = UNIV" +by (force elim: reachable.induct intro: reachable.intros) + +(** SKIP and safety properties **) + +lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)" +by (unfold constrains_def, auto) + +lemma SKIP_in_Constrains_iff [iff]: "(SKIP : A Co B) = (A<=B)" +by (unfold Constrains_def, auto) + +lemma SKIP_in_stable [iff]: "SKIP : stable A" +by (unfold stable_def, auto) + +declare SKIP_in_stable [THEN stable_imp_Stable, iff] + + +(** Join **) + +lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G" +by (simp add: Join_def) + +lemma Acts_Join [simp]: "Acts (F Join G) = Acts F Un Acts G" +by (auto simp add: Join_def) + +lemma AllowedActs_Join [simp]: + "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G" +by (auto simp add: Join_def) + + +(** JN **) + +lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP" +by (unfold JOIN_def SKIP_def, auto) + +lemma JN_insert [simp]: "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)" +apply (rule program_equalityI) +apply (auto simp add: JOIN_def Join_def) +done + +lemma Init_JN [simp]: "Init (JN i:I. F i) = (INT i:I. Init (F i))" +by (simp add: JOIN_def) + +lemma Acts_JN [simp]: "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))" +by (auto simp add: JOIN_def) + +lemma AllowedActs_JN [simp]: + "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))" +by (auto simp add: JOIN_def) + + +lemma JN_cong [cong]: + "[| I=J; !!i. i:J ==> F i = G i |] ==> (JN i:I. F i) = (JN i:J. G i)" +by (simp add: JOIN_def) + + +(** Algebraic laws **) + +lemma Join_commute: "F Join G = G Join F" +by (simp add: Join_def Un_commute Int_commute) + +lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)" +by (simp add: Un_ac Join_def Int_assoc insert_absorb) + +lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)" +by (simp add: Un_ac Int_ac Join_def insert_absorb) + +lemma Join_SKIP_left [simp]: "SKIP Join F = F" +apply (unfold Join_def SKIP_def) +apply (rule program_equalityI) +apply (simp_all (no_asm) add: insert_absorb) +done + +lemma Join_SKIP_right [simp]: "F Join SKIP = F" +apply (unfold Join_def SKIP_def) +apply (rule program_equalityI) +apply (simp_all (no_asm) add: insert_absorb) +done + +lemma Join_absorb [simp]: "F Join F = F" +apply (unfold Join_def) +apply (rule program_equalityI, auto) +done + +lemma Join_left_absorb: "F Join (F Join G) = F Join G" +apply (unfold Join_def) +apply (rule program_equalityI, auto) +done + +(*Join is an AC-operator*) +lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute + + +(*** JN laws ***) + +(*Also follows by JN_insert and insert_absorb, but the proof is longer*) +lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)" +by (auto intro!: program_equalityI) + +lemma JN_Un: "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))" +by (auto intro!: program_equalityI) + +lemma JN_constant: "(JN i:I. c) = (if I={} then SKIP else c)" +by (rule program_equalityI, auto) + +lemma JN_Join_distrib: + "(JN i:I. F i Join G i) = (JN i:I. F i) Join (JN i:I. G i)" +by (auto intro!: program_equalityI) + +lemma JN_Join_miniscope: + "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)" +by (auto simp add: JN_Join_distrib JN_constant) + +(*Used to prove guarantees_JN_I*) +lemma JN_Join_diff: "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F" +apply (unfold JOIN_def Join_def) +apply (rule program_equalityI, auto) +done + + +(*** Safety: co, stable, FP ***) + +(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B. So an + alternative precondition is A<=B, but most proofs using this rule require + I to be nonempty for other reasons anyway.*) +lemma JN_constrains: + "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)" +by (simp add: constrains_def JOIN_def, blast) + +lemma Join_constrains [simp]: + "(F Join G : A co B) = (F : A co B & G : A co B)" +by (auto simp add: constrains_def Join_def) + +lemma Join_unless [simp]: + "(F Join G : A unless B) = (F : A unless B & G : A unless B)" +by (simp add: Join_constrains unless_def) + +(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. + reachable (F Join G) could be much bigger than reachable F, reachable G +*) + + +lemma Join_constrains_weaken: + "[| F : A co A'; G : B co B' |] + ==> F Join G : (A Int B) co (A' Un B')" +by (simp, blast intro: constrains_weaken) + +(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*) +lemma JN_constrains_weaken: + "[| ALL i:I. F i : A i co A' i; i: I |] + ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)" +apply (simp (no_asm_simp) add: JN_constrains) +apply (blast intro: constrains_weaken) +done + +lemma JN_stable: "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)" +by (simp add: stable_def constrains_def JOIN_def) + +lemma invariant_JN_I: + "[| !!i. i:I ==> F i : invariant A; i : I |] + ==> (JN i:I. F i) : invariant A" +by (simp add: invariant_def JN_stable, blast) + +lemma Join_stable [simp]: + "(F Join G : stable A) = + (F : stable A & G : stable A)" +by (simp add: stable_def) + +lemma Join_increasing [simp]: + "(F Join G : increasing f) = + (F : increasing f & G : increasing f)" +by (simp add: increasing_def Join_stable, blast) + +lemma invariant_JoinI: + "[| F : invariant A; G : invariant A |] + ==> F Join G : invariant A" +by (simp add: invariant_def, blast) + +lemma FP_JN: "FP (JN i:I. F i) = (INT i:I. FP (F i))" +by (simp add: FP_def JN_stable INTER_def) + + +(*** Progress: transient, ensures ***) + +lemma JN_transient: + "i : I ==> + (JN i:I. F i) : transient A = (EX i:I. F i : transient A)" +by (auto simp add: transient_def JOIN_def) + +lemma Join_transient [simp]: + "F Join G : transient A = + (F : transient A | G : transient A)" +by (auto simp add: bex_Un transient_def Join_def) + +lemma Join_transient_I1: "F : transient A ==> F Join G : transient A" +by (simp add: Join_transient) + +lemma Join_transient_I2: "G : transient A ==> F Join G : transient A" +by (simp add: Join_transient) + +(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *) +lemma JN_ensures: + "i : I ==> + (JN i:I. F i) : A ensures B = + ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))" +by (auto simp add: ensures_def JN_constrains JN_transient) + +lemma Join_ensures: + "F Join G : A ensures B = + (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) & + (F : transient (A-B) | G : transient (A-B)))" +by (auto simp add: ensures_def Join_transient) + +lemma stable_Join_constrains: + "[| F : stable A; G : A co A' |] + ==> F Join G : A co A'" +apply (unfold stable_def constrains_def Join_def) +apply (simp add: ball_Un, blast) +done + +(*Premise for G cannot use Always because F: Stable A is weaker than + G : stable A *) +lemma stable_Join_Always1: + "[| F : stable A; G : invariant A |] ==> F Join G : Always A" +apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable) +apply (force intro: stable_Int) +done + +(*As above, but exchanging the roles of F and G*) +lemma stable_Join_Always2: + "[| F : invariant A; G : stable A |] ==> F Join G : Always A" +apply (subst Join_commute) +apply (blast intro: stable_Join_Always1) +done + +lemma stable_Join_ensures1: + "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B" +apply (simp (no_asm_simp) add: Join_ensures) +apply (simp add: stable_def ensures_def) +apply (erule constrains_weaken, auto) +done + +(*As above, but exchanging the roles of F and G*) +lemma stable_Join_ensures2: + "[| F : A ensures B; G : stable A |] ==> F Join G : A ensures B" +apply (subst Join_commute) +apply (blast intro: stable_Join_ensures1) +done + + +(*** the ok and OK relations ***) + +lemma ok_SKIP1 [iff]: "SKIP ok F" +by (auto simp add: ok_def) + +lemma ok_SKIP2 [iff]: "F ok SKIP" +by (auto simp add: ok_def) + +lemma ok_Join_commute: + "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))" +by (auto simp add: ok_def) + +lemma ok_commute: "(F ok G) = (G ok F)" +by (auto simp add: ok_def) + +lemmas ok_sym = ok_commute [THEN iffD1, standard] + +lemma ok_iff_OK: + "OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)" +by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb all_conj_distrib eq_commute, blast) + +lemma ok_Join_iff1 [iff]: "F ok (G Join H) = (F ok G & F ok H)" +by (auto simp add: ok_def) + +lemma ok_Join_iff2 [iff]: "(G Join H) ok F = (G ok F & H ok F)" +by (auto simp add: ok_def) + +(*useful? Not with the previous two around*) +lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)" +by (auto simp add: ok_def) + +lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (ALL i:I. F ok G i)" +by (auto simp add: ok_def) + +lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (ALL i:I. G i ok F)" +by (auto simp add: ok_def) + +lemma OK_iff_ok: "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))" +by (auto simp add: ok_def OK_def) + +lemma OK_imp_ok: "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)" +by (auto simp add: OK_iff_ok) + + +(*** Allowed ***) + +lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV" +by (auto simp add: Allowed_def) + +lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F Int Allowed G" +by (auto simp add: Allowed_def) + +lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (INT i:I. Allowed (F i))" +by (auto simp add: Allowed_def) + +lemma ok_iff_Allowed: "F ok G = (F : Allowed G & G : Allowed F)" +by (simp add: ok_def Allowed_def) + +lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))" +by (auto simp add: OK_iff_ok ok_iff_Allowed) + +(*** safety_prop, for reasoning about given instances of "ok" ***) + +lemma safety_prop_Acts_iff: + "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)" +by (auto simp add: safety_prop_def) + +lemma safety_prop_AllowedActs_iff_Allowed: + "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)" +by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric]) + +lemma Allowed_eq: + "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X" +by (simp add: Allowed_def safety_prop_Acts_iff) + +lemma def_prg_Allowed: + "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |] + ==> Allowed F = X" +by (simp add: Allowed_eq) + +(*For safety_prop to hold, the property must be satisfiable!*) +lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A <= B)" +by (simp add: safety_prop_def constrains_def, blast) + +lemma safety_prop_stable [iff]: "safety_prop (stable A)" +by (simp add: stable_def) + +lemma safety_prop_Int [simp]: + "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)" +by (simp add: safety_prop_def, blast) + +lemma safety_prop_INTER1 [simp]: + "(!!i. safety_prop (X i)) ==> safety_prop (INT i. X i)" +by (auto simp add: safety_prop_def, blast) + +lemma safety_prop_INTER [simp]: + "(!!i. i:I ==> safety_prop (X i)) ==> safety_prop (INT i:I. X i)" +by (auto simp add: safety_prop_def, blast) + +lemma def_UNION_ok_iff: + "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] + ==> F ok G = (G : X & acts <= AllowedActs G)" +by (auto simp add: ok_def safety_prop_Acts_iff) end