# HG changeset patch # User paulson # Date 1057221445 -7200 # Node ID cb07c394866865171b9d526e2bca99dde420c7f9 # Parent a9be38579840fc8a414152045b8a90f97a8360ab Conversion of UNITY/Comp/Priority.thy to a linear Isar script diff -r a9be38579840 -r cb07c3948668 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Jul 02 16:57:57 2003 +0200 +++ b/src/HOL/IsaMakefile Thu Jul 03 10:37:25 2003 +0200 @@ -394,7 +394,7 @@ UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \ UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \ UNITY/Comp/PriorityAux.ML UNITY/Comp/PriorityAux.thy \ - UNITY/Comp/Priority.ML UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ + UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ UNITY/Comp/TimerArray.thy @$(ISATOOL) usedir $(OUT)/HOL UNITY diff -r a9be38579840 -r cb07c3948668 src/HOL/UNITY/Comp/Priority.ML --- a/src/HOL/UNITY/Comp/Priority.ML Wed Jul 02 16:57:57 2003 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,245 +0,0 @@ -(* Title: HOL/UNITY/Priority - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -The priority system - -From Charpentier and Chandy, -Examples of Program Composition Illustrating the Use of Universal Properties - In J. Rolim (editor), Parallel and Distributed Processing, - Spriner LNCS 1586 (1999), pages 1215-1227. -*) - -Addsimps [Component_def RS def_prg_Init]; -Addsimps [highest_def, lowest_def]; -Addsimps [simp_of_act act_def]; -Addsimps (map simp_of_set [Highest_def, Lowest_def]); - - - - -(**** Component correctness proofs ****) - -(* neighbors is stable *) -Goal "Component i: stable {s. neighbors k s = n}"; -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); -by (constrains_tac 1); -by Auto_tac; -qed "Component_neighbors_stable"; - -(* property 4 *) -Goal "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}"; -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); -by (constrains_tac 1); -qed "Component_waits_priority"; - -(* property 5: charpentier and Chandy mistakenly express it as - 'transient Highest i'. Consider the case where i has neighbors *) -Goal - "Component i: {s. neighbors i s ~= {}} Int Highest i \ -\ ensures - Highest i"; -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); -by (ensures_tac "act i" 1); -by (REPEAT(Fast_tac 1)); -qed "Component_yields_priority"; - -(* or better *) -Goal "Component i: Highest i ensures Lowest i"; -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); -by (ensures_tac "act i" 1); -by (REPEAT(Fast_tac 1)); -qed "Component_yields_priority'"; - -(* property 6: Component doesn't introduce cycle *) -Goal "Component i: Highest i co Highest i Un Lowest i"; -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); -by (constrains_tac 1); -by (Fast_tac 1); -qed "Component_well_behaves"; - -(* property 7: local axiom *) -Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}"; -by (asm_full_simp_tac (simpset() addsimps [Component_def]) 1); -by (constrains_tac 1); -qed "locality"; - - -(**** System properties ****) -(* property 8: strictly universal *) - -Goalw [Safety_def] "system: stable Safety"; -by (rtac stable_INT 1); -by (asm_full_simp_tac (simpset() addsimps [system_def]) 1); -by (constrains_tac 1); -by (Fast_tac 1); -qed "Safety"; - -(* property 13: universal *) -Goal "system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}"; -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); -by (constrains_tac 1); -by (Blast_tac 1); -qed "p13"; - -(* property 14: the 'above set' of a Component that hasn't got - priority doesn't increase *) -Goal -"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}"; -by (Clarify_tac 1); -by (cut_inst_tac [("i", "j")] reach_lemma 1); -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); -by (constrains_tac 1); -by (auto_tac (claset(), simpset() addsimps [trancl_converse])); -qed "above_not_increase"; - -Goal "system: -Highest i Int {s. above i s = x} co {s. above i s <= x}"; -by (cut_inst_tac [("i", "i")] above_not_increase 1); -by (asm_full_simp_tac - (simpset() addsimps [trancl_converse, constrains_def]) 1); -by (Blast_tac 1); -qed "above_not_increase'"; - - - -(* p15: universal property: all Components well behave *) -Goal "ALL i. system: Highest i co Highest i Un Lowest i"; -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); -by (constrains_tac 1); -by Auto_tac; -qed "system_well_behaves"; - - -Goal "Acyclic = (INT i. {s. i~:above i s})"; -by (auto_tac (claset(), simpset() - addsimps [Acyclic_def, acyclic_def, trancl_converse])); -qed "Acyclic_eq"; - - -val lemma = [above_not_increase RS spec, - system_well_behaves RS spec] MRS constrains_Un; -Goal -"system: stable Acyclic"; -by (auto_tac (claset() addSIs [stable_INT, stableI, - lemma RS constrains_weaken], - simpset() addsimps [Acyclic_eq, - image0_r_iff_image0_trancl,trancl_converse])); -qed "Acyclic_stable"; - - -Goalw [Acyclic_def, Maximal_def] -"Acyclic <= Maximal"; -by (Clarify_tac 1); -by (dtac above_lemma_b 1); -by Auto_tac; -qed "Acyclic_subset_Maximal"; - -(* property 17: original one is an invariant *) -Goal -"system: stable (Acyclic Int Maximal)"; -by (simp_tac (simpset() addsimps - [Acyclic_subset_Maximal RS Int_absorb2, Acyclic_stable]) 1); -qed "Acyclic_Maximal_stable"; - - -(* propert 5: existential property *) - -Goal "system: Highest i leadsTo Lowest i"; -by (asm_full_simp_tac (simpset() addsimps [system_def, Component_def, mk_total_program_def, totalize_JN]) 1); -by (ensures_tac "act i" 1); -by Auto_tac; -qed "Highest_leadsTo_Lowest"; - -(* a lowest i can never be in any abover set *) -Goal "Lowest i <= (INT k. {s. i~:above k s})"; -by (auto_tac (claset(), - simpset() addsimps [image0_r_iff_image0_trancl, trancl_converse])); -qed "Lowest_above_subset"; - -(* property 18: a simpler proof than the original, one which uses psp *) -Goal "system: Highest i leadsTo (INT k. {s. i~:above k s})"; -by (rtac leadsTo_weaken_R 1); -by (rtac Lowest_above_subset 2); -by (rtac Highest_leadsTo_Lowest 1); -qed "Highest_escapes_above"; - -Goal -"system: Highest j Int {s. j:above i s} leadsTo {s. j~:above i s}"; -by (blast_tac (claset() addIs - [[Highest_escapes_above, Int_lower1, INT_lower] MRS leadsTo_weaken]) 1); -qed "Highest_escapes_above'"; - -(*** The main result: above set decreases ***) -(* The original proof of the following formula was wrong *) -val above_decreases_lemma = -[Highest_escapes_above', above_not_increase'] MRS psp RS leadsTo_weaken; - -Goal "Highest i = {s. above i s ={}}"; -by (auto_tac (claset(), - simpset() addsimps [image0_trancl_iff_image0_r])); -qed "Highest_iff_above0"; - - -Goal -"system: (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j) \ -\ leadsTo {s. above i s < x}"; -by (rtac leadsTo_UN 1); -by (rtac single_leadsTo_I 1); -by (Clarify_tac 1); -by (res_inst_tac [("x2", "above i x")] above_decreases_lemma 1); -by (ALLGOALS(full_simp_tac (simpset() delsimps [Highest_def] - addsimps [Highest_iff_above0]))); -by (REPEAT(Blast_tac 1)); -qed "above_decreases"; - -(** Just a massage of conditions to have the desired form ***) -Goalw [Maximal_def, Maximal'_def, Highest_def] -"Maximal = Maximal'"; -by (Blast_tac 1); -qed "Maximal_eq_Maximal'"; - -Goal "x~={} ==> \ -\ Acyclic Int {s. above i s = x} <= \ -\ (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j)"; -by (res_inst_tac [("B", "Maximal' Int {s. above i s = x}")] subset_trans 1); -by (simp_tac (simpset() addsimps [Maximal_eq_Maximal' RS sym]) 1); -by (blast_tac (claset() addIs [Acyclic_subset_Maximal RS subsetD]) 1); -by (simp_tac (simpset() delsimps [above_def] addsimps [Maximal'_def, Highest_iff_above0]) 1); -by (Blast_tac 1); -qed "Acyclic_subset"; - -val above_decreases' = [above_decreases, Acyclic_subset] MRS leadsTo_weaken_L; -val above_decreases_psp = [above_decreases', Acyclic_stable] MRS psp_stable; - -Goal -"x~={}==> \ -\ system: Acyclic Int {s. above i s = x} leadsTo Acyclic Int {s. above i s < x}"; -by (etac (above_decreases_psp RS leadsTo_weaken) 1); -by (Blast_tac 1); -by Auto_tac; -qed "above_decreases_psp'"; - - -val finite_psubset_induct = wf_finite_psubset RS leadsTo_wf_induct; -val leadsTo_weaken_L' = rotate_prems 1 leadsTo_weaken_L; - - -Goal "system: Acyclic leadsTo Highest i"; -by (res_inst_tac [("f", "%s. above i s")] finite_psubset_induct 1); -by (asm_simp_tac (simpset() delsimps [Highest_def, thm "above_def"] - addsimps [Highest_iff_above0, - vimage_def, finite_psubset_def]) 1); -by (Clarify_tac 1); -by (case_tac "m={}" 1); -by (rtac (Int_lower2 RS leadsTo_weaken_L') 1); -by (force_tac (claset(), simpset() addsimps [leadsTo_refl]) 1); -by (res_inst_tac [("A'", "Acyclic Int {x. above i x < m}")] - leadsTo_weaken_R 1); -by (REPEAT(blast_tac (claset() addIs [above_decreases_psp']) 1)); -qed "Progress"; - -(* We have proved all (relevant) theorems given in the paper *) -(* We didn't assume any thing about the relation r *) -(* It is not necessary that r be a priority relation as assumed in the original proof *) -(* It suffices that we start from a state which is finite and acyclic *) diff -r a9be38579840 -r cb07c3948668 src/HOL/UNITY/Comp/Priority.thy --- a/src/HOL/UNITY/Comp/Priority.thy Wed Jul 02 16:57:57 2003 +0200 +++ b/src/HOL/UNITY/Comp/Priority.thy Thu Jul 03 10:37:25 2003 +0200 @@ -3,15 +3,17 @@ Author: Sidi O Ehmety, Cambridge University Computer Laboratory Copyright 2001 University of Cambridge -The priority system + +*) -From Charpentier and Chandy, +header{*The priority system*} + +theory Priority = PriorityAux: + +text{*From Charpentier and Chandy, Examples of Program Composition Illustrating the Use of Universal Properties In J. Rolim (editor), Parallel and Distributed Processing, - Spriner LNCS 1586 (1999), pages 1215-1227. -*) - -Priority = PriorityAux + + Spriner LNCS 1586 (1999), pages 1215-1227.*} types state = "(vertex*vertex)set" types command = "vertex=>(state*state)set" @@ -50,14 +52,14 @@ (* Every above set has a maximal vertex: two equivalent defs. *) Maximal :: "state set" - "Maximal == INT i. {s. ~highest i s-->(EX j:above i s. highest j s)}" + "Maximal == \i. {s. ~highest i s-->(\j \ above i s. highest j s)}" Maximal' :: "state set" - "Maximal' == INT i. Highest i Un (UN j. {s. j:above i s} Int Highest j)" + "Maximal' == \i. Highest i Un (\j. {s. j \ above i s} Int Highest j)" Safety :: "state set" - "Safety == INT i. {s. highest i s --> (ALL j:neighbors i s. ~highest j s)}" + "Safety == \i. {s. highest i s --> (\j \ neighbors i s. ~highest j s)}" (* Composition of a finite set of component; @@ -65,4 +67,202 @@ system :: "state program" "system == JN i. Component i" + + +declare highest_def [simp] lowest_def [simp] +declare Highest_def [THEN def_set_simp, simp] + and Lowest_def [THEN def_set_simp, simp] + +declare Component_def [THEN def_prg_Init, simp] +declare act_def [THEN def_act_simp, simp] + + + +subsection{*Component correctness proofs*} + +(* neighbors is stable *) +lemma Component_neighbors_stable: "Component i \ stable {s. neighbors k s = n}" +by (simp add: Component_def, constrains, auto) + +(* property 4 *) +lemma Component_waits_priority: "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}" +by (simp add: Component_def, constrains) + +(* property 5: charpentier and Chandy mistakenly express it as + 'transient Highest i'. Consider the case where i has neighbors *) +lemma Component_yields_priority: + "Component i: {s. neighbors i s \ {}} Int Highest i + ensures - Highest i" +apply (simp add: Component_def) +apply (ensures_tac "act i", blast+) +done + +(* or better *) +lemma Component_yields_priority': "Component i \ Highest i ensures Lowest i" +apply (simp add: Component_def) +apply (ensures_tac "act i", blast+) +done + +(* property 6: Component doesn't introduce cycle *) +lemma Component_well_behaves: "Component i \ Highest i co Highest i Un Lowest i" +by (simp add: Component_def, constrains, fast) + +(* property 7: local axiom *) +lemma locality: "Component i \ stable {s. \j k. j\i & k\i--> ((j,k):s) = b j k}" +by (simp add: Component_def, constrains) + + +subsection{*System properties*} +(* property 8: strictly universal *) + +lemma Safety: "system \ stable Safety" +apply (unfold Safety_def) +apply (rule stable_INT) +apply (simp add: system_def, constrains, fast) +done + +(* property 13: universal *) +lemma p13: "system \ {s. s = q} co {s. s=q} Un {s. \i. derive i q s}" +by (simp add: system_def Component_def mk_total_program_def totalize_JN, constrains, blast) + +(* property 14: the 'above set' of a Component that hasn't got + priority doesn't increase *) +lemma above_not_increase: + "\j. system \ -Highest i Int {s. j\above i s} co {s. j\above i s}" +apply clarify +apply (cut_tac i = j in reach_lemma) +apply (simp add: system_def Component_def mk_total_program_def totalize_JN, + constrains) +apply (auto simp add: trancl_converse) +done + +lemma above_not_increase': + "system \ -Highest i Int {s. above i s = x} co {s. above i s <= x}" +apply (cut_tac i = i in above_not_increase) +apply (simp add: trancl_converse constrains_def, blast) +done + + + +(* p15: universal property: all Components well behave *) +lemma system_well_behaves [rule_format]: + "\i. system \ Highest i co Highest i Un Lowest i" +apply clarify +apply (simp add: system_def Component_def mk_total_program_def totalize_JN, + constrains, auto) +done + + +lemma Acyclic_eq: "Acyclic = (\i. {s. i\above i s})" +by (auto simp add: Acyclic_def acyclic_def trancl_converse) + + +lemmas system_co = + constrains_Un [OF above_not_increase [rule_format] system_well_behaves] + +lemma Acyclic_stable: "system \ stable Acyclic" +apply (simp add: stable_def Acyclic_eq) +apply (auto intro!: constrains_INT system_co [THEN constrains_weaken] + simp add: image0_r_iff_image0_trancl trancl_converse) +done + + +lemma Acyclic_subset_Maximal: "Acyclic <= Maximal" +apply (unfold Acyclic_def Maximal_def, clarify) +apply (drule above_lemma_b, auto) +done + +(* property 17: original one is an invariant *) +lemma Acyclic_Maximal_stable: "system \ stable (Acyclic Int Maximal)" +apply (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable) +done + + +(* propert 5: existential property *) + +lemma Highest_leadsTo_Lowest: "system \ Highest i leadsTo Lowest i" +apply (simp add: system_def Component_def mk_total_program_def totalize_JN) +apply (ensures_tac "act i", auto) +done + +(* a lowest i can never be in any abover set *) +lemma Lowest_above_subset: "Lowest i <= (\k. {s. i\above k s})" +by (auto simp add: image0_r_iff_image0_trancl trancl_converse) + +(* property 18: a simpler proof than the original, one which uses psp *) +lemma Highest_escapes_above: "system \ Highest i leadsTo (\k. {s. i\above k s})" +apply (rule leadsTo_weaken_R) +apply (rule_tac [2] Lowest_above_subset) +apply (rule Highest_leadsTo_Lowest) +done + +lemma Highest_escapes_above': + "system \ Highest j Int {s. j \ above i s} leadsTo {s. j\above i s}" +by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower]) + +(*** The main result: above set decreases ***) +(* The original proof of the following formula was wrong *) + +lemma Highest_iff_above0: "Highest i = {s. above i s ={}}" +by (auto simp add: image0_trancl_iff_image0_r) + +lemmas above_decreases_lemma = + psp [THEN leadsTo_weaken, OF Highest_escapes_above' above_not_increase'] + + +lemma above_decreases: + "system \ (\j. {s. above i s = x} Int {s. j \ above i s} Int Highest j) + leadsTo {s. above i s < x}" +apply (rule leadsTo_UN) +apply (rule single_leadsTo_I, clarify) +apply (rule_tac x2 = "above i x" in above_decreases_lemma) +apply (simp_all (no_asm_use) del: Highest_def add: Highest_iff_above0) +apply blast+ +done + +(** Just a massage of conditions to have the desired form ***) +lemma Maximal_eq_Maximal': "Maximal = Maximal'" +by (unfold Maximal_def Maximal'_def Highest_def, blast) + +lemma Acyclic_subset: + "x\{} ==> + Acyclic Int {s. above i s = x} <= + (\j. {s. above i s = x} Int {s. j \ above i s} Int Highest j)" +apply (rule_tac B = "Maximal' Int {s. above i s = x}" in subset_trans) +apply (simp (no_asm) add: Maximal_eq_Maximal' [symmetric]) +apply (blast intro: Acyclic_subset_Maximal [THEN subsetD]) +apply (simp (no_asm) del: above_def add: Maximal'_def Highest_iff_above0) +apply blast +done + +lemmas above_decreases' = leadsTo_weaken_L [OF above_decreases Acyclic_subset] +lemmas above_decreases_psp = psp_stable [OF above_decreases' Acyclic_stable] + +lemma above_decreases_psp': +"x\{}==> system \ Acyclic Int {s. above i s = x} leadsTo + Acyclic Int {s. above i s < x}" +by (erule above_decreases_psp [THEN leadsTo_weaken], blast, auto) + + +lemmas finite_psubset_induct = wf_finite_psubset [THEN leadsTo_wf_induct] + + +lemma Progress: "system \ Acyclic leadsTo Highest i" +apply (rule_tac f = "%s. above i s" in finite_psubset_induct) +apply (simp del: Highest_def above_def + add: Highest_iff_above0 vimage_def finite_psubset_def, clarify) +apply (case_tac "m={}") +apply (rule Int_lower2 [THEN [2] leadsTo_weaken_L]) +apply (force simp add: leadsTo_refl) +apply (rule_tac A' = "Acyclic Int {x. above i x < m}" in leadsTo_weaken_R) +apply (blast intro: above_decreases_psp')+ +done + + +text{*We have proved all (relevant) theorems given in the paper. We didn't +assume any thing about the relation @{term r}. It is not necessary that +@{term r} be a priority relation as assumed in the original proof. It +suffices that we start from a state which is finite and acyclic.*} + + end \ No newline at end of file