# HG changeset patch # User paulson # Date 1043413609 -3600 # Node ID e2fcd88be55d288e5fd551f50204265c426750cc # Parent b9f6154427a4ade03b01bc35a19e1331ca5f5ddc Partial conversion of UNITY to Isar new-style theories diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/IsaMakefile Fri Jan 24 14:06:49 2003 +0100 @@ -381,8 +381,8 @@ HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ - UNITY/Comp.ML UNITY/Comp.thy \ - UNITY/Detects.ML UNITY/Detects.thy \ + UNITY/UNITY_Main.thy UNITY/Comp.ML UNITY/Comp.thy \ + UNITY/Detects.thy \ UNITY/ELT.ML UNITY/ELT.thy UNITY/Extend.ML \ UNITY/Extend.thy UNITY/FP.ML UNITY/FP.thy UNITY/Follows.ML \ UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \ @@ -395,16 +395,16 @@ 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/Simple/Channel.ML UNITY/Simple/Channel.thy \ - UNITY/Simple/Common.ML UNITY/Simple/Common.thy \ - UNITY/Simple/Deadlock.ML UNITY/Simple/Deadlock.thy \ - UNITY/Simple/Lift.ML UNITY/Simple/Lift.thy \ - UNITY/Simple/Mutex.ML UNITY/Simple/Mutex.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 \ - UNITY/Simple/Network.ML UNITY/Simple/Network.thy \ - UNITY/Simple/Reach.ML UNITY/Simple/Reach.thy \ - UNITY/Simple/Reachability.ML UNITY/Simple/Reachability.thy \ - UNITY/Simple/Token.ML UNITY/Simple/Token.thy \ + UNITY/Simple/Network.thy \ + UNITY/Simple/Reach.thy \ + UNITY/Simple/Reachability.thy \ + UNITY/Simple/Token.thy \ UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \ UNITY/Comp/AllocBase.ML UNITY/Comp/AllocBase.thy \ UNITY/Comp/Client.ML UNITY/Comp/Client.thy \ diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Detects.ML --- a/src/HOL/UNITY/Detects.ML Thu Jan 23 10:30:14 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,69 +0,0 @@ -(* Title: HOL/UNITY/Detects - ID: $Id$ - Author: Tanja Vos, Cambridge University Computer Laboratory - Copyright 2000 University of Cambridge - -Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo -*) - -(* Corollary from Sectiom 3.6.4 *) - -Goal "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))"; -by (rtac LeadsTo_empty 1); -by (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))" 1); -by (subgoal_tac "(FP F Int A Int - B) = (A Int (FP F Int -B))" 2); -by (subgoal_tac "(B Int (FP F Int -B)) = {}" 1); -by Auto_tac; -by (blast_tac (claset() addIs [PSP_Stable, stable_imp_Stable, - stable_FP_Int]) 1); -qed "Always_at_FP"; - - -Goalw [Detects_def, Int_def] - "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C"; -by (Simp_tac 1); -by Safe_tac; -by (rtac LeadsTo_Trans 2); -by Auto_tac; -by (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))" 1); -by (simp_tac (simpset() addsimps [Always_Int_distrib]) 2); -by Auto_tac; -by (blast_tac (claset() addIs [Always_weaken]) 1); -qed "Detects_Trans"; - - -Goalw [Detects_def] "F : A Detects A"; -by (simp_tac (simpset() addsimps [Un_commute, Compl_partition, - subset_imp_LeadsTo]) 1); -qed "Detects_refl"; - -Goalw [Equality_def] "(A<==>B) = (A Int B) Un (-A Int -B)"; -by (Blast_tac 1); -qed "Detects_eq_Un"; - -(*Not quite antisymmetry: sets A and B agree in all reachable states *) -Goalw [Detects_def, Equality_def] - "[| F : A Detects B; F : B Detects A|] ==> F : Always (A <==> B)"; -by (asm_full_simp_tac (simpset() addsimps [Always_Int_I, Un_commute]) 1); -qed "Detects_antisym"; - - -(* Theorem from Section 3.8 *) - -Goalw [Detects_def, Equality_def] - "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))"; -by (simp_tac (simpset() addsimps [Un_Int_distrib, Always_Int_distrib]) 1); -by (blast_tac (claset() addDs [Always_at_FP] - addIs [Always_weaken]) 1); -qed "Detects_Always"; - -(* Theorem from exercise 11.1 Section 11.3.1 *) - -Goalw [Detects_def, Equality_def] - "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)"; -by (res_inst_tac [("B", "B")] LeadsTo_Diff 1); -by (blast_tac (claset() addIs [Always_LeadsTo_weaken]) 2); -by (blast_tac (claset() addIs [Always_LeadsToI, subset_imp_LeadsTo]) 1); -qed "Detects_Imp_LeadstoEQ"; - - diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Detects.thy --- a/src/HOL/UNITY/Detects.thy Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/Detects.thy Fri Jan 24 14:06:49 2003 +0100 @@ -6,16 +6,78 @@ Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo *) -Detects = WFair + Reach + - +theory Detects = FP + SubstAx: consts op_Detects :: "['a set, 'a set] => 'a program set" (infixl "Detects" 60) op_Equality :: "['a set, 'a set] => 'a set" (infixl "<==>" 60) defs - Detects_def "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)" - Equality_def "A <==> B == (-A Un B) Int (A Un -B)" + Detects_def: "A Detects B == (Always (-A Un B)) Int (B LeadsTo A)" + Equality_def: "A <==> B == (-A Un B) Int (A Un -B)" + + +(* Corollary from Sectiom 3.6.4 *) + +lemma Always_at_FP: "F: A LeadsTo B ==> F : Always (-((FP F) Int A Int -B))" +apply (rule LeadsTo_empty) +apply (subgoal_tac "F : (FP F Int A Int - B) LeadsTo (B Int (FP F Int -B))") +apply (subgoal_tac [2] " (FP F Int A Int - B) = (A Int (FP F Int -B))") +apply (subgoal_tac "(B Int (FP F Int -B)) = {}") +apply auto +apply (blast intro: PSP_Stable stable_imp_Stable stable_FP_Int) +done + + +lemma Detects_Trans: + "[| F : A Detects B; F : B Detects C |] ==> F : A Detects C" +apply (unfold Detects_def Int_def) +apply (simp (no_asm)) +apply safe +apply (rule_tac [2] LeadsTo_Trans) +apply auto +apply (subgoal_tac "F : Always ((-A Un B) Int (-B Un C))") + apply (blast intro: Always_weaken) +apply (simp add: Always_Int_distrib) +done + +lemma Detects_refl: "F : A Detects A" +apply (unfold Detects_def) +apply (simp (no_asm) add: Un_commute Compl_partition subset_imp_LeadsTo) +done + +lemma Detects_eq_Un: "(A<==>B) = (A Int B) Un (-A Int -B)" +apply (unfold Equality_def) +apply blast +done + +(*Not quite antisymmetry: sets A and B agree in all reachable states *) +lemma Detects_antisym: + "[| F : A Detects B; F : B Detects A|] ==> F : Always (A <==> B)" +apply (unfold Detects_def Equality_def) +apply (simp add: Always_Int_I Un_commute) +done + + +(* Theorem from Section 3.8 *) + +lemma Detects_Always: + "F : A Detects B ==> F : Always ((-(FP F)) Un (A <==> B))" +apply (unfold Detects_def Equality_def) +apply (simp (no_asm) add: Un_Int_distrib Always_Int_distrib) +apply (blast dest: Always_at_FP intro: Always_weaken) +done + +(* Theorem from exercise 11.1 Section 11.3.1 *) + +lemma Detects_Imp_LeadstoEQ: + "F : A Detects B ==> F : UNIV LeadsTo (A <==> B)" +apply (unfold Detects_def Equality_def) +apply (rule_tac B = "B" in LeadsTo_Diff) +prefer 2 apply (blast intro: Always_LeadsTo_weaken) +apply (blast intro: Always_LeadsToI subset_imp_LeadsTo) +done + end diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/ROOT.ML --- a/src/HOL/UNITY/ROOT.ML Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/ROOT.ML Fri Jan 24 14:06:49 2003 +0100 @@ -7,8 +7,7 @@ *) (*Basic meta-theory*) -time_use_thy "FP"; -time_use_thy "WFair"; +time_use_thy "UNITY_Main"; (*Simple examples: no composition*) time_use_thy "Simple/Deadlock"; diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Channel.ML --- a/src/HOL/UNITY/Simple/Channel.ML Thu Jan 23 10:30:14 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ -(* Title: HOL/UNITY/Channel - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Unordered Channel - -From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 -*) - -(*None represents "infinity" while Some represents proper integers*) -Goalw [minSet_def] "minSet A = Some x --> x : A"; -by (Simp_tac 1); -by (fast_tac (claset() addIs [LeastI]) 1); -qed_spec_mp "minSet_eq_SomeD"; - -Goalw [minSet_def] " minSet{} = None"; -by (Asm_simp_tac 1); -qed_spec_mp "minSet_empty"; -Addsimps [minSet_empty]; - -Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)"; -by Auto_tac; -qed_spec_mp "minSet_nonempty"; - -Goal "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))"; -by (rtac leadsTo_weaken 1); -by (res_inst_tac [("x1","x")] ([UC2, UC1] MRS psp) 1); -by Safe_tac; -by (auto_tac (claset() addDs [minSet_eq_SomeD], - simpset() addsimps [linorder_neq_iff])); -qed "minSet_greaterThan"; - -(*The induction*) -Goal "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))"; -by (rtac leadsTo_weaken_R 1); -by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")] - greaterThan_bounded_induct 1); -by Safe_tac; -by (ALLGOALS Asm_simp_tac); -by (dtac minSet_nonempty 2); -by (Asm_full_simp_tac 2); -by (rtac (minSet_greaterThan RS leadsTo_weaken) 1); -by Safe_tac; -by (ALLGOALS Asm_full_simp_tac); -by (dtac minSet_nonempty 1); -by (Asm_full_simp_tac 1); -val lemma = result(); - - -Goal "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}"; -by (rtac (lemma RS leadsTo_weaken_R) 1); -by (Clarify_tac 1); -by (ftac minSet_nonempty 1); -by (auto_tac (claset() addDs [Suc_le_lessD, not_less_Least], - simpset())); -qed "Channel_progress"; diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Channel.thy --- a/src/HOL/UNITY/Simple/Channel.thy Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/Simple/Channel.thy Fri Jan 24 14:06:49 2003 +0100 @@ -8,23 +8,65 @@ From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 *) -Channel = WFair + +theory Channel = UNITY_Main: -types state = nat set +types state = "nat set" consts - F :: state program + F :: "state program" constdefs - minSet :: nat set => nat option + minSet :: "nat set => nat option" "minSet A == if A={} then None else Some (LEAST x. x:A)" -rules +axioms - UC1 "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))" + UC1: "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))" (* UC1 "F : {s. minSet s = x} co {s. x <= minSet s}" *) - UC2 "F : (minSet -` {Some x}) leadsTo {s. x ~: s}" + UC2: "F : (minSet -` {Some x}) leadsTo {s. x ~: s}" + + +(*None represents "infinity" while Some represents proper integers*) +lemma minSet_eq_SomeD: "minSet A = Some x ==> x : A" +apply (unfold minSet_def) +apply (simp split: split_if_asm) +apply (fast intro: LeastI) +done + +lemma minSet_empty [simp]: " minSet{} = None" +by (unfold minSet_def, simp) + +lemma minSet_nonempty: "x:A ==> minSet A = Some (LEAST x. x: A)" +by (unfold minSet_def, auto) + +lemma minSet_greaterThan: + "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))" +apply (rule leadsTo_weaken) +apply (rule_tac x1=x in psp [OF UC2 UC1], safe) +apply (auto dest: minSet_eq_SomeD simp add: linorder_neq_iff) +done + +(*The induction*) +lemma Channel_progress_lemma: + "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))" +apply (rule leadsTo_weaken_R) +apply (rule_tac l = y and f = "the o minSet" and B = "{}" + in greaterThan_bounded_induct, safe) +apply (simp_all (no_asm_simp)) +apply (drule_tac [2] minSet_nonempty) + prefer 2 apply simp +apply (rule minSet_greaterThan [THEN leadsTo_weaken], safe) +apply simp_all +apply (drule minSet_nonempty, simp) +done + + +lemma Channel_progress: "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}" +apply (rule Channel_progress_lemma [THEN leadsTo_weaken_R], clarify) +apply (frule minSet_nonempty) +apply (auto dest: Suc_le_lessD not_less_Least) +done end diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Common.ML --- a/src/HOL/UNITY/Simple/Common.ML Thu Jan 23 10:30:14 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,90 +0,0 @@ -(* Title: HOL/UNITY/Common - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Common Meeting Time example from Misra (1994) - -The state is identified with the one variable in existence. - -From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1. -*) - -(*Misra's property CMT4: t exceeds no common meeting time*) -Goal "[| ALL m. F : {m} Co (maxfg m); n: common |] \ -\ ==> F : Stable (atMost n)"; -by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1); -by (asm_full_simp_tac - (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def, - le_max_iff_disj]) 1); -by (etac Constrains_weaken_R 1); -by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1); -qed "common_stable"; - -Goal "[| Init F <= atMost n; \ -\ ALL m. F : {m} Co (maxfg m); n: common |] \ -\ ==> F : Always (atMost n)"; -by (asm_simp_tac (simpset() addsimps [AlwaysI, common_stable]) 1); -qed "common_safety"; - - -(*** Some programs that implement the safety property above ***) - -Goal "SKIP : {m} co (maxfg m)"; -by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj, - fasc]) 1); -result(); - -(*This one is t := ftime t || t := gtime t*) -Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) \ -\ : {m} co (maxfg m)"; -by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, - le_max_iff_disj, fasc]) 1); -result(); - -(*This one is t := max (ftime t) (gtime t)*) -Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) \ -\ : {m} co (maxfg m)"; -by (simp_tac - (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1); -result(); - -(*This one is t := t+1 if t F : (atMost n) LeadsTo common"; -by (rtac LeadsTo_weaken_R 1); -by (res_inst_tac [("f","id"), ("l","n")] GreaterThan_bounded_induct 1); -by (ALLGOALS Asm_simp_tac); -by (rtac subset_refl 2); -by (blast_tac (claset() addDs [PSP_Stable2] - addIs [common_stable, LeadsTo_weaken_R]) 1); -val lemma = result(); - -(*The "ALL m: -common" form echoes CMT6.*) -Goal "[| ALL m. F : {m} Co (maxfg m); \ -\ ALL m: -common. F : {m} LeadsTo (greaterThan m); \ -\ n: common |] \ -\ ==> F : (atMost (LEAST n. n: common)) LeadsTo common"; -by (rtac lemma 1); -by (ALLGOALS Asm_simp_tac); -by (etac LeastI 2); -by (blast_tac (claset() addSDs [not_less_Least]) 1); -qed "leadsTo_common"; diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Common.thy --- a/src/HOL/UNITY/Simple/Common.thy Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/Simple/Common.thy Fri Jan 24 14:06:49 2003 +0100 @@ -10,23 +10,96 @@ From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1. *) -Common = SubstAx + +theory Common = UNITY_Main: consts - ftime,gtime :: nat=>nat + ftime :: "nat=>nat" + gtime :: "nat=>nat" -rules - fmono "m <= n ==> ftime m <= ftime n" - gmono "m <= n ==> gtime m <= gtime n" +axioms + fmono: "m <= n ==> ftime m <= ftime n" + gmono: "m <= n ==> gtime m <= gtime n" - fasc "m <= ftime n" - gasc "m <= gtime n" + fasc: "m <= ftime n" + gasc: "m <= gtime n" constdefs - common :: nat set + common :: "nat set" "common == {n. ftime n = n & gtime n = n}" - maxfg :: nat => nat set + maxfg :: "nat => nat set" "maxfg m == {t. t <= max (ftime m) (gtime m)}" + +(*Misra's property CMT4: t exceeds no common meeting time*) +lemma common_stable: + "[| ALL m. F : {m} Co (maxfg m); n: common |] + ==> F : Stable (atMost n)" +apply (drule_tac M = "{t. t<=n}" in Elimination_sing) +apply (simp add: atMost_def Stable_def common_def maxfg_def le_max_iff_disj) +apply (erule Constrains_weaken_R) +apply (blast intro: order_eq_refl fmono gmono le_trans) +done + +lemma common_safety: + "[| Init F <= atMost n; + ALL m. F : {m} Co (maxfg m); n: common |] + ==> F : Always (atMost n)" +by (simp add: AlwaysI common_stable) + + +(*** Some programs that implement the safety property above ***) + +lemma "SKIP : {m} co (maxfg m)" +by (simp add: constrains_def maxfg_def le_max_iff_disj fasc) + +(*This one is t := ftime t || t := gtime t*) +lemma "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) + : {m} co (maxfg m)" +by (simp add: constrains_def maxfg_def le_max_iff_disj fasc) + +(*This one is t := max (ftime t) (gtime t)*) +lemma "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) + : {m} co (maxfg m)" +by (simp add: constrains_def maxfg_def max_def gasc) + +(*This one is t := t+1 if t F : (atMost n) LeadsTo common" +apply (rule LeadsTo_weaken_R) +apply (rule_tac f = id and l = n in GreaterThan_bounded_induct) +apply (simp_all (no_asm_simp)) +apply (rule_tac [2] subset_refl) +apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R) +done + +(*The "ALL m: -common" form echoes CMT6.*) +lemma leadsTo_common: + "[| ALL m. F : {m} Co (maxfg m); + ALL m: -common. F : {m} LeadsTo (greaterThan m); + n: common |] + ==> F : (atMost (LEAST n. n: common)) LeadsTo common" +apply (rule leadsTo_common_lemma) +apply (simp_all (no_asm_simp)) +apply (erule_tac [2] LeastI) +apply (blast dest!: not_less_Least) +done + end diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Deadlock.ML --- a/src/HOL/UNITY/Simple/Deadlock.ML Thu Jan 23 10:30:14 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,78 +0,0 @@ -(* Title: HOL/UNITY/Deadlock - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Deadlock examples from section 5.6 of - Misra, "A Logic for Concurrent Programming", 1994 -*) - -(*Trivial, two-process case*) -Goalw [constrains_def, stable_def] - "[| F : (A Int B) co A; F : (B Int A) co B |] ==> F : stable (A Int B)"; -by (Blast_tac 1); -result(); - - -(*a simplification step*) -Goal "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)"; -by (induct_tac "n" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc]))); -by Auto_tac; -qed "Collect_le_Int_equals"; - -(*Dual of the required property. Converse inclusion fails.*) -Goal "(UN i: lessThan n. A i) Int (- A n) <= \ -\ (UN i: lessThan n. (A i) Int (- A (Suc i)))"; -by (induct_tac "n" 1); -by (Asm_simp_tac 1); -by (simp_tac (simpset() addsimps [lessThan_Suc]) 1); -by (Blast_tac 1); -qed "UN_Int_Compl_subset"; - - -(*Converse inclusion fails.*) -Goal "(INT i: lessThan n. -A i Un A (Suc i)) <= \ -\ (INT i: lessThan n. -A i) Un A n"; -by (induct_tac "n" 1); -by (Asm_simp_tac 1); -by (asm_simp_tac (simpset() addsimps [lessThan_Suc]) 1); -by (Blast_tac 1); -qed "INT_Un_Compl_subset"; - - -(*Specialized rewriting*) -Goal "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}"; -by (blast_tac (claset() addIs [gr0I] - addDs [impOfSubs INT_Un_Compl_subset]) 1); -val lemma = result(); - -(*Reverse direction makes it harder to invoke the ind hyp*) -Goal "(INT i: atMost n. A i) = \ -\ A 0 Int (INT i: lessThan n. -A i Un A(Suc i))"; -by (induct_tac "n" 1); -by (Asm_simp_tac 1); -by (asm_simp_tac - (simpset() addsimps Int_ac @ [Int_Un_distrib, Int_Un_distrib2, lemma, - lessThan_Suc, atMost_Suc]) 1); -qed "INT_le_equals_Int"; - -Goal "(INT i: atMost (Suc n). A i) = \ -\ A 0 Int (INT i: atMost n. -A i Un A(Suc i))"; -by (simp_tac (simpset() addsimps [lessThan_Suc_atMost, INT_le_equals_Int]) 1); -qed "INT_le_Suc_equals_Int"; - - -(*The final deadlock example*) -val [zeroprem, allprem] = Goalw [stable_def] - "[| F : (A 0 Int A (Suc n)) co (A 0); \ -\ !!i. i: atMost n ==> F : (A(Suc i) Int A i) co (-A i Un A(Suc i)) |] \ -\ ==> F : stable (INT i: atMost (Suc n). A i)"; -by (rtac ([zeroprem, constrains_INT] MRS - constrains_Int RS constrains_weaken) 1); -by (etac allprem 1); -by (simp_tac (simpset() addsimps [Collect_le_Int_equals, - Int_assoc, INT_absorb]) 1); -by (simp_tac (simpset() addsimps [INT_le_Suc_equals_Int]) 1); -result(); - diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Deadlock.thy --- a/src/HOL/UNITY/Simple/Deadlock.thy Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/Simple/Deadlock.thy Fri Jan 24 14:06:49 2003 +0100 @@ -1,1 +1,82 @@ -Deadlock = UNITY +(* Title: HOL/UNITY/Deadlock + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1998 University of Cambridge + +Deadlock examples from section 5.6 of + Misra, "A Logic for Concurrent Programming", 1994 +*) + +theory Deadlock = UNITY: + +(*Trivial, two-process case*) +lemma "[| F : (A Int B) co A; F : (B Int A) co B |] ==> F : stable (A Int B)" +by (unfold constrains_def stable_def, blast) + + +(*a simplification step*) +lemma Collect_le_Int_equals: + "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)" +apply (induct_tac "n") +apply (simp_all (no_asm_simp) add: atMost_Suc) +apply auto +done + +(*Dual of the required property. Converse inclusion fails.*) +lemma UN_Int_Compl_subset: + "(UN i: lessThan n. A i) Int (- A n) <= + (UN i: lessThan n. (A i) Int (- A (Suc i)))" +apply (induct_tac "n") +apply (simp (no_asm_simp)) +apply (simp (no_asm) add: lessThan_Suc) +apply blast +done + + +(*Converse inclusion fails.*) +lemma INT_Un_Compl_subset: + "(INT i: lessThan n. -A i Un A (Suc i)) <= + (INT i: lessThan n. -A i) Un A n" +apply (induct_tac "n") +apply (simp (no_asm_simp)) +apply (simp (no_asm_simp) add: lessThan_Suc) +apply blast +done + + +(*Specialized rewriting*) +lemma INT_le_equals_Int_lemma: + "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}" +by (blast intro: gr0I dest: INT_Un_Compl_subset [THEN subsetD]) + +(*Reverse direction makes it harder to invoke the ind hyp*) +lemma INT_le_equals_Int: + "(INT i: atMost n. A i) = + A 0 Int (INT i: lessThan n. -A i Un A(Suc i))" +apply (induct_tac "n", simp) +apply (simp add: Int_ac Int_Un_distrib Int_Un_distrib2 + INT_le_equals_Int_lemma lessThan_Suc atMost_Suc) +done + +lemma INT_le_Suc_equals_Int: + "(INT i: atMost (Suc n). A i) = + A 0 Int (INT i: atMost n. -A i Un A(Suc i))" +by (simp add: lessThan_Suc_atMost INT_le_equals_Int) + + +(*The final deadlock example*) +lemma + assumes zeroprem: "F : (A 0 Int A (Suc n)) co (A 0)" + and allprem: + "!!i. i: atMost n ==> F : (A(Suc i) Int A i) co (-A i Un A(Suc i))" + shows "F : stable (INT i: atMost (Suc n). A i)" +apply (unfold stable_def) +apply (rule constrains_Int [THEN constrains_weaken]) + apply (rule zeroprem) + apply (rule constrains_INT) + apply (erule allprem) + apply (simp add: Collect_le_Int_equals Int_assoc INT_absorb) +apply (simp add: INT_le_Suc_equals_Int) +done + +end diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Lift.ML --- a/src/HOL/UNITY/Simple/Lift.ML Thu Jan 23 10:30:14 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,317 +0,0 @@ -(* Title: HOL/UNITY/Lift - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -The Lift-Control Example -*) - -Goal "[| x ~: A; y : A |] ==> x ~= y"; -by (Blast_tac 1); -qed "not_mem_distinct"; - - -Addsimps [Lift_def RS def_prg_Init]; -program_defs_ref := [Lift_def]; - -Addsimps (map simp_of_act - [request_act_def, open_act_def, close_act_def, - req_up_def, req_down_def, move_up_def, move_down_def, - button_press_def]); - -(*The ALWAYS properties*) -Addsimps (map simp_of_set [above_def, below_def, queueing_def, - goingup_def, goingdown_def, ready_def]); - -Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def, - moving_up_def, moving_down_def]; - -AddIffs [Min_le_Max]; - -Goal "Lift : Always open_stop"; -by (always_tac 1); -qed "open_stop"; - -Goal "Lift : Always stop_floor"; -by (always_tac 1); -qed "stop_floor"; - -(*This one needs open_stop, which was proved above*) -Goal "Lift : Always open_move"; -by (cut_facts_tac [open_stop] 1); -by (always_tac 1); -qed "open_move"; - -Goal "Lift : Always moving_up"; -by (always_tac 1); -by (auto_tac (claset() addDs [zle_imp_zless_or_eq], - simpset() addsimps [add1_zle_eq])); -qed "moving_up"; - -Goal "Lift : Always moving_down"; -by (always_tac 1); -by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1); -qed "moving_down"; - -Goal "Lift : Always bounded"; -by (cut_facts_tac [moving_up, moving_down] 1); -by (always_tac 1); -by Auto_tac; -by (ALLGOALS (dtac not_mem_distinct THEN' assume_tac)); -by (ALLGOALS arith_tac); -qed "bounded"; - - - -(*** Progress ***) - - -val abbrev_defs = [moving_def, stopped_def, - opened_def, closed_def, atFloor_def, Req_def]; - -Addsimps (map simp_of_set abbrev_defs); - - -(** The HUG'93 paper mistakenly omits the Req n from these! **) - -(** Lift_1 **) - -Goal "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)"; -by (cut_facts_tac [stop_floor] 1); -by (ensures_tac "open_act" 1); -qed "E_thm01"; (*lem_lift_1_5*) - -Goal "Lift : (Req n Int stopped - atFloor n) LeadsTo \ -\ (Req n Int opened - atFloor n)"; -by (cut_facts_tac [stop_floor] 1); -by (ensures_tac "open_act" 1); -qed "E_thm02"; (*lem_lift_1_1*) - -Goal "Lift : (Req n Int opened - atFloor n) LeadsTo \ -\ (Req n Int closed - (atFloor n - queueing))"; -by (ensures_tac "close_act" 1); -qed "E_thm03"; (*lem_lift_1_2*) - -Goal "Lift : (Req n Int closed Int (atFloor n - queueing)) \ -\ LeadsTo (opened Int atFloor n)"; -by (ensures_tac "open_act" 1); -qed "E_thm04"; (*lem_lift_1_7*) - - -(** Lift 2. Statements of thm05a and thm05b were wrong! **) - -Open_locale "floor"; - -val Min_le_n = thm "Min_le_n"; -val n_le_Max = thm "n_le_Max"; - -AddIffs [Min_le_n, n_le_Max]; - -val le_MinD = Min_le_n RS order_antisym; -val Max_leD = n_le_Max RSN (2,order_antisym); - -val linorder_leI = linorder_not_less RS iffD1; - -AddSDs [le_MinD, linorder_leI RS le_MinD, - Max_leD, linorder_leI RS Max_leD]; - -(*lem_lift_2_0 - NOT an ensures property, but a mere inclusion; - don't know why script lift_2.uni says ENSURES*) -Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \ -\ LeadsTo ((closed Int goingup Int Req n) Un \ -\ (closed Int goingdown Int Req n))"; -by (auto_tac (claset() addSIs [subset_imp_LeadsTo] addSEs [int_neqE], - simpset())); -qed "E_thm05c"; - -(*lift_2*) -Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \ -\ LeadsTo (moving Int Req n)"; -by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1); -by (ensures_tac "req_down" 2); -by (ensures_tac "req_up" 1); -by Auto_tac; -qed "lift_2"; - - -(** Towards lift_4 ***) - -val metric_ss = simpset() addsplits [split_if_asm] - addsimps [metric_def, vimage_def]; - - -(*lem_lift_4_1 *) -Goal "0 < N ==> \ -\ Lift : (moving Int Req n Int {s. metric n s = N} Int \ -\ {s. floor s ~: req s} Int {s. up s}) \ -\ LeadsTo \ -\ (moving Int Req n Int {s. metric n s < N})"; -by (cut_facts_tac [moving_up] 1); -by (ensures_tac "move_up" 1); -by Safe_tac; -(*this step consolidates two formulae to the goal metric n s' <= metric n s*) -by (etac (linorder_leI RS order_antisym RS sym) 1); -by (auto_tac (claset(), metric_ss)); -qed "E_thm12a"; - - -(*lem_lift_4_3 *) -Goal "0 < N ==> \ -\ Lift : (moving Int Req n Int {s. metric n s = N} Int \ -\ {s. floor s ~: req s} - {s. up s}) \ -\ LeadsTo (moving Int Req n Int {s. metric n s < N})"; -by (cut_facts_tac [moving_down] 1); -by (ensures_tac "move_down" 1); -by Safe_tac; -(*this step consolidates two formulae to the goal metric n s' <= metric n s*) -by (etac (linorder_leI RS order_antisym RS sym) 1); -by (auto_tac (claset(), metric_ss)); -qed "E_thm12b"; - -(*lift_4*) -Goal "0 Lift : (moving Int Req n Int {s. metric n s = N} Int \ -\ {s. floor s ~: req s}) LeadsTo \ -\ (moving Int Req n Int {s. metric n s < N})"; -by (rtac ([subset_imp_LeadsTo, [E_thm12a, E_thm12b] MRS LeadsTo_Un] - MRS LeadsTo_Trans) 1); -by Auto_tac; -qed "lift_4"; - - -(** towards lift_5 **) - -(*lem_lift_5_3*) -Goal "0 Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \ -\ (moving Int Req n Int {s. metric n s < N})"; -by (cut_facts_tac [bounded] 1); -by (ensures_tac "req_up" 1); -by (auto_tac (claset(), metric_ss)); -qed "E_thm16a"; - - -(*lem_lift_5_1 has ~goingup instead of goingdown*) -Goal "0 \ -\ Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \ -\ (moving Int Req n Int {s. metric n s < N})"; -by (cut_facts_tac [bounded] 1); -by (ensures_tac "req_down" 1); -by (auto_tac (claset(), metric_ss)); -qed "E_thm16b"; - - -(*lem_lift_5_0 proves an intersection involving ~goingup and goingup, - i.e. the trivial disjunction, leading to an asymmetrical proof.*) -Goal "0 Req n Int {s. metric n s = N} <= goingup Un goingdown"; -by (Clarify_tac 1); -by (force_tac (claset(), metric_ss) 1); -qed "E_thm16c"; - - -(*lift_5*) -Goal "0 Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo \ -\ (moving Int Req n Int {s. metric n s < N})"; -by (rtac ([subset_imp_LeadsTo, [E_thm16a, E_thm16b] MRS LeadsTo_Un] - MRS LeadsTo_Trans) 1); -by (dtac E_thm16c 1); -by Auto_tac; -qed "lift_5"; - - -(** towards lift_3 **) - -(*lemma used to prove lem_lift_3_1*) -Goal "[| metric n s = 0; Min <= floor s; floor s <= Max |] ==> floor s = n"; -by (auto_tac (claset(), metric_ss)); -qed "metric_eq_0D"; - -AddDs [metric_eq_0D]; - - -(*lem_lift_3_1*) -Goal "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo \ -\ (stopped Int atFloor n)"; -by (cut_facts_tac [bounded] 1); -by (ensures_tac "request_act" 1); -by Auto_tac; -qed "E_thm11"; - -(*lem_lift_3_5*) -Goal - "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ -\ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"; -by (ensures_tac "request_act" 1); -by (auto_tac (claset(), metric_ss)); -qed "E_thm13"; - -(*lem_lift_3_6*) -Goal "0 < N ==> \ -\ Lift : \ -\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ -\ LeadsTo (opened Int Req n Int {s. metric n s = N})"; -by (ensures_tac "open_act" 1); -by (auto_tac (claset(), metric_ss)); -qed "E_thm14"; - -(*lem_lift_3_7*) -Goal "Lift : (opened Int Req n Int {s. metric n s = N}) \ -\ LeadsTo (closed Int Req n Int {s. metric n s = N})"; -by (ensures_tac "close_act" 1); -by (auto_tac (claset(), metric_ss)); -qed "E_thm15"; - - -(** the final steps **) - -Goal "0 < N ==> \ -\ Lift : \ -\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ -\ LeadsTo (moving Int Req n Int {s. metric n s < N})"; -by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5] - addIs [LeadsTo_Trans]) 1); -qed "lift_3_Req"; - - -(*Now we observe that our integer metric is really a natural number*) -Goal "Lift : Always {s. 0 <= metric n s}"; -by (rtac (bounded RS Always_weaken) 1); -by (auto_tac (claset(), metric_ss)); -qed "Always_nonneg"; - -val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken; - -Goal "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)"; -by (rtac (Always_nonneg RS integ_0_le_induct) 1); -by (case_tac "0 < z" 1); -(*If z <= 0 then actually z = 0*) -by (force_tac (claset() addIs [R_thm11, order_antisym], - simpset() addsimps [linorder_not_less]) 2); -by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1); -by (rtac ([subset_imp_LeadsTo, [lift_4, lift_3_Req] MRS LeadsTo_Un] - MRS LeadsTo_Trans) 1); -by Auto_tac; -qed "lift_3"; - - -val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un; -(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *) - -Goal "Lift : (Req n) LeadsTo (opened Int atFloor n)"; -by (rtac LeadsTo_Trans 1); -by (rtac ([E_thm04, LeadsTo_Un_post] MRS LeadsTo_Un) 2); -by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2); -by (rtac (lift_3 RS LeadsTo_Trans_Un') 2); -by (rtac (lift_2 RS LeadsTo_Trans_Un') 2); -by (rtac ([E_thm03,E_thm02] MRS LeadsTo_Trans_Un') 2); -by (rtac (open_move RS Always_LeadsToI) 1); -by (rtac ([open_stop, subset_imp_LeadsTo] MRS Always_LeadsToI) 1); -by (Clarify_tac 1); -(*The case split is not essential but makes Blast_tac much faster. - Calling rotate_tac prevents simplification from looping*) -by (case_tac "open x" 1); -by (ALLGOALS (rotate_tac ~1)); -by Auto_tac; -qed "lift_1"; - -Close_locale "floor"; diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Lift.thy --- a/src/HOL/UNITY/Simple/Lift.thy Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/Simple/Lift.thy Fri Jan 24 14:06:49 2003 +0100 @@ -6,63 +6,63 @@ The Lift-Control Example *) -Lift = SubstAx + +theory Lift = UNITY_Main: record state = - floor :: int (*current position of the lift*) - open :: bool (*whether the door is open at floor*) - stop :: bool (*whether the lift is stopped at floor*) - req :: int set (*for each floor, whether the lift is requested*) - up :: bool (*current direction of movement*) - move :: bool (*whether moving takes precedence over opening*) + floor :: "int" (*current position of the lift*) + "open" :: "bool" (*whether the door is opened at floor*) + stop :: "bool" (*whether the lift is stopped at floor*) + req :: "int set" (*for each floor, whether the lift is requested*) + up :: "bool" (*current direction of movement*) + move :: "bool" (*whether moving takes precedence over opening*) consts - Min, Max :: int (*least and greatest floors*) + Min :: "int" (*least and greatest floors*) + Max :: "int" (*least and greatest floors*) -rules - Min_le_Max "Min <= Max" +axioms + Min_le_Max [iff]: "Min <= Max" constdefs (** Abbreviations: the "always" part **) - above :: state set + above :: "state set" "above == {s. EX i. floor s < i & i <= Max & i : req s}" - below :: state set + below :: "state set" "below == {s. EX i. Min <= i & i < floor s & i : req s}" - queueing :: state set + queueing :: "state set" "queueing == above Un below" - goingup :: state set + goingup :: "state set" "goingup == above Int ({s. up s} Un -below)" - goingdown :: state set + goingdown :: "state set" "goingdown == below Int ({s. ~ up s} Un -above)" - ready :: state set + ready :: "state set" "ready == {s. stop s & ~ open s & move s}" - (** Further abbreviations **) - moving :: state set + moving :: "state set" "moving == {s. ~ stop s & ~ open s}" - stopped :: state set + stopped :: "state set" "stopped == {s. stop s & ~ open s & ~ move s}" - opened :: state set + opened :: "state set" "opened == {s. stop s & open s & move s}" - closed :: state set (*but this is the same as ready!!*) + closed :: "state set" (*but this is the same as ready!!*) "closed == {s. stop s & ~ open s & move s}" - atFloor :: int => state set + atFloor :: "int => state set" "atFloor n == {s. floor s = n}" - Req :: int => state set + Req :: "int => state set" "Req n == {s. n : req s}" @@ -118,7 +118,7 @@ & Min <= n & n <= Max}" - Lift :: state program + Lift :: "state program" (*for the moment, we OMIT button_press*) "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s & ~ open s & req s = {}}, @@ -129,27 +129,27 @@ (** Invariants **) - bounded :: state set + bounded :: "state set" "bounded == {s. Min <= floor s & floor s <= Max}" - open_stop :: state set + open_stop :: "state set" "open_stop == {s. open s --> stop s}" - open_move :: state set + open_move :: "state set" "open_move == {s. open s --> move s}" - stop_floor :: state set + stop_floor :: "state set" "stop_floor == {s. stop s & ~ move s --> floor s : req s}" - moving_up :: state set + moving_up :: "state set" "moving_up == {s. ~ stop s & up s --> (EX f. floor s <= f & f <= Max & f : req s)}" - moving_down :: state set + moving_down :: "state set" "moving_down == {s. ~ stop s & ~ up s --> (EX f. Min <= f & f <= floor s & f : req s)}" - metric :: [int,state] => int + metric :: "[int,state] => int" "metric == %n s. if floor s < n then (if up s then n - floor s else (floor s - Min) + (n-Min)) @@ -158,12 +158,310 @@ else floor s - n) else 0" -locale floor = - fixes - n :: int - assumes - Min_le_n "Min <= n" - n_le_Max "n <= Max" - defines +locale Floor = + fixes n + assumes Min_le_n [iff]: "Min <= n" + and n_le_Max [iff]: "n <= Max" + +lemma not_mem_distinct: "[| x ~: A; y : A |] ==> x ~= y" +by blast + + +declare Lift_def [THEN def_prg_Init, simp] + +declare request_act_def [THEN def_act_simp, simp] +declare open_act_def [THEN def_act_simp, simp] +declare close_act_def [THEN def_act_simp, simp] +declare req_up_def [THEN def_act_simp, simp] +declare req_down_def [THEN def_act_simp, simp] +declare move_up_def [THEN def_act_simp, simp] +declare move_down_def [THEN def_act_simp, simp] +declare button_press_def [THEN def_act_simp, simp] + +(*The ALWAYS properties*) +declare above_def [THEN def_set_simp, simp] +declare below_def [THEN def_set_simp, simp] +declare queueing_def [THEN def_set_simp, simp] +declare goingup_def [THEN def_set_simp, simp] +declare goingdown_def [THEN def_set_simp, simp] +declare ready_def [THEN def_set_simp, simp] + +(*Basic definitions*) +declare bounded_def [simp] + open_stop_def [simp] + open_move_def [simp] + stop_floor_def [simp] + moving_up_def [simp] + moving_down_def [simp] + +lemma open_stop: "Lift : Always open_stop" +apply (rule AlwaysI, force) +apply (unfold Lift_def, constrains) +done + +lemma stop_floor: "Lift : Always stop_floor" +apply (rule AlwaysI, force) +apply (unfold Lift_def, constrains) +done + +(*This one needs open_stop, which was proved above*) +lemma open_move: "Lift : Always open_move" +apply (cut_tac open_stop) +apply (rule AlwaysI, force) +apply (unfold Lift_def, constrains) +done + +lemma moving_up: "Lift : Always moving_up" +apply (rule AlwaysI, force) +apply (unfold Lift_def, constrains) +apply (auto dest: zle_imp_zless_or_eq simp add: add1_zle_eq) +done + +lemma moving_down: "Lift : Always moving_down" +apply (rule AlwaysI, force) +apply (unfold Lift_def, constrains) +apply (blast dest: zle_imp_zless_or_eq) +done + +lemma bounded: "Lift : Always bounded" +apply (cut_tac moving_up moving_down) +apply (rule AlwaysI, force) +apply (unfold Lift_def, constrains, auto) +apply (drule not_mem_distinct, assumption, arith)+ +done + + +subsection{*Progress*} + +declare moving_def [THEN def_set_simp, simp] +declare stopped_def [THEN def_set_simp, simp] +declare opened_def [THEN def_set_simp, simp] +declare closed_def [THEN def_set_simp, simp] +declare atFloor_def [THEN def_set_simp, simp] +declare Req_def [THEN def_set_simp, simp] + + +(** The HUG'93 paper mistakenly omits the Req n from these! **) + +(** Lift_1 **) +lemma E_thm01: "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)" +apply (cut_tac stop_floor) +apply (unfold Lift_def, ensures_tac "open_act") +done (*lem_lift_1_5*) + +lemma E_thm02: "Lift : (Req n Int stopped - atFloor n) LeadsTo + (Req n Int opened - atFloor n)" +apply (cut_tac stop_floor) +apply (unfold Lift_def, ensures_tac "open_act") +done (*lem_lift_1_1*) + +lemma E_thm03: "Lift : (Req n Int opened - atFloor n) LeadsTo + (Req n Int closed - (atFloor n - queueing))" +apply (unfold Lift_def, ensures_tac "close_act") +done (*lem_lift_1_2*) + +lemma E_thm04: "Lift : (Req n Int closed Int (atFloor n - queueing)) + LeadsTo (opened Int atFloor n)" +apply (unfold Lift_def, ensures_tac "open_act") +done (*lem_lift_1_7*) + + +(** Lift 2. Statements of thm05a and thm05b were wrong! **) + +lemmas linorder_leI = linorder_not_less [THEN iffD1] + +lemmas (in Floor) le_MinD = Min_le_n [THEN order_antisym] + and Max_leD = n_le_Max [THEN [2] order_antisym] + +declare (in Floor) le_MinD [dest!] + and linorder_leI [THEN le_MinD, dest!] + and Max_leD [dest!] + and linorder_leI [THEN Max_leD, dest!] + + +(*lem_lift_2_0 + NOT an ensures_tac property, but a mere inclusion + don't know why script lift_2.uni says ENSURES*) +lemma (in Floor) E_thm05c: + "Lift : (Req n Int closed - (atFloor n - queueing)) + LeadsTo ((closed Int goingup Int Req n) Un + (closed Int goingdown Int Req n))" +by (auto intro!: subset_imp_LeadsTo elim!: int_neqE) + +(*lift_2*) +lemma (in Floor) lift_2: "Lift : (Req n Int closed - (atFloor n - queueing)) + LeadsTo (moving Int Req n)" +apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un]) +apply (unfold Lift_def) +apply (ensures_tac [2] "req_down") +apply (ensures_tac "req_up", auto) +done + + +(** Towards lift_4 ***) + +declare split_if_asm [split] + + +(*lem_lift_4_1 *) +lemma (in Floor) E_thm12a: + "0 < N ==> + Lift : (moving Int Req n Int {s. metric n s = N} Int + {s. floor s ~: req s} Int {s. up s}) + LeadsTo + (moving Int Req n Int {s. metric n s < N})" +apply (cut_tac moving_up) +apply (unfold Lift_def, ensures_tac "move_up", safe) +(*this step consolidates two formulae to the goal metric n s' <= metric n s*) +apply (erule linorder_leI [THEN order_antisym, symmetric]) +apply (auto simp add: metric_def) +done + + +(*lem_lift_4_3 *) +lemma (in Floor) E_thm12b: "0 < N ==> + Lift : (moving Int Req n Int {s. metric n s = N} Int + {s. floor s ~: req s} - {s. up s}) + LeadsTo (moving Int Req n Int {s. metric n s < N})" +apply (cut_tac moving_down) +apply (unfold Lift_def, ensures_tac "move_down", safe) +(*this step consolidates two formulae to the goal metric n s' <= metric n s*) +apply (erule linorder_leI [THEN order_antisym, symmetric]) +apply (auto simp add: metric_def) +done + +(*lift_4*) +lemma (in Floor) lift_4: + "0 Lift : (moving Int Req n Int {s. metric n s = N} Int + {s. floor s ~: req s}) LeadsTo + (moving Int Req n Int {s. metric n s < N})" +apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo + LeadsTo_Un [OF E_thm12a E_thm12b]], auto) +done + + +(** towards lift_5 **) + +(*lem_lift_5_3*) +lemma (in Floor) E_thm16a: "0 Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo + (moving Int Req n Int {s. metric n s < N})" +apply (cut_tac bounded) +apply (unfold Lift_def, ensures_tac "req_up") +apply (auto simp add: metric_def) +done + + +(*lem_lift_5_1 has ~goingup instead of goingdown*) +lemma (in Floor) E_thm16b: "0 + Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo + (moving Int Req n Int {s. metric n s < N})" +apply (cut_tac bounded) +apply (unfold Lift_def, ensures_tac "req_down") +apply (auto simp add: metric_def) +done + + +(*lem_lift_5_0 proves an intersection involving ~goingup and goingup, + i.e. the trivial disjunction, leading to an asymmetrical proof.*) +lemma (in Floor) E_thm16c: + "0 Req n Int {s. metric n s = N} <= goingup Un goingdown" +by (force simp add: metric_def) + + +(*lift_5*) +lemma (in Floor) lift_5: + "0 Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo + (moving Int Req n Int {s. metric n s < N})" +apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo + LeadsTo_Un [OF E_thm16a E_thm16b]]) +apply (drule E_thm16c, auto) +done + + +(** towards lift_3 **) + +(*lemma used to prove lem_lift_3_1*) +lemma (in Floor) metric_eq_0D [dest]: + "[| metric n s = 0; Min <= floor s; floor s <= Max |] ==> floor s = n" +by (force simp add: metric_def) + + +(*lem_lift_3_1*) +lemma (in Floor) E_thm11: "Lift : (moving Int Req n Int {s. metric n s = 0}) LeadsTo + (stopped Int atFloor n)" +apply (cut_tac bounded) +apply (unfold Lift_def, ensures_tac "request_act", auto) +done + +(*lem_lift_3_5*) +lemma (in Floor) E_thm13: + "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) + LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})" +apply (unfold Lift_def, ensures_tac "request_act") +apply (auto simp add: metric_def) +done + +(*lem_lift_3_6*) +lemma (in Floor) E_thm14: "0 < N ==> + Lift : + (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) + LeadsTo (opened Int Req n Int {s. metric n s = N})" +apply (unfold Lift_def, ensures_tac "open_act") +apply (auto simp add: metric_def) +done + +(*lem_lift_3_7*) +lemma (in Floor) E_thm15: "Lift : (opened Int Req n Int {s. metric n s = N}) + LeadsTo (closed Int Req n Int {s. metric n s = N})" +apply (unfold Lift_def, ensures_tac "close_act") +apply (auto simp add: metric_def) +done + + +(** the final steps **) + +lemma (in Floor) lift_3_Req: "0 < N ==> + Lift : + (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) + LeadsTo (moving Int Req n Int {s. metric n s < N})" +apply (blast intro!: E_thm13 E_thm14 E_thm15 lift_5 intro: LeadsTo_Trans) +done + + +(*Now we observe that our integer metric is really a natural number*) +lemma (in Floor) Always_nonneg: "Lift : Always {s. 0 <= metric n s}" +apply (rule bounded [THEN Always_weaken]) +apply (auto simp add: metric_def) +done + +lemmas (in Floor) R_thm11 = Always_LeadsTo_weaken [OF Always_nonneg E_thm11] + +lemma (in Floor) lift_3: + "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)" +apply (rule Always_nonneg [THEN integ_0_le_induct]) +apply (case_tac "0 < z") +(*If z <= 0 then actually z = 0*) +prefer 2 apply (force intro: R_thm11 order_antisym simp add: linorder_not_less) +apply (rule LeadsTo_weaken_R [OF asm_rl Un_upper1]) +apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo + LeadsTo_Un [OF lift_4 lift_3_Req]], auto) +done + + +lemma (in Floor) lift_1: "Lift : (Req n) LeadsTo (opened Int atFloor n)" +apply (rule LeadsTo_Trans) + prefer 2 + apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post]) + apply (rule E_thm01 [THEN [2] LeadsTo_Trans_Un]) + apply (rule lift_3 [THEN [2] LeadsTo_Trans_Un]) + apply (rule lift_2 [THEN [2] LeadsTo_Trans_Un]) + apply (rule LeadsTo_Trans_Un [OF E_thm02 E_thm03]) +apply (rule open_move [THEN Always_LeadsToI]) +apply (rule Always_LeadsToI [OF open_stop subset_imp_LeadsTo], clarify) +(*The case split is not essential but makes the proof much faster.*) +apply (case_tac "open x", auto) +done + end diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Mutex.ML --- a/src/HOL/UNITY/Simple/Mutex.ML Thu Jan 23 10:30:14 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,166 +0,0 @@ -(* Title: HOL/UNITY/Mutex - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra -*) - -Addsimps [Mutex_def RS def_prg_Init]; -program_defs_ref := [Mutex_def]; - -Addsimps (map simp_of_act - [U0_def, U1_def, U2_def, U3_def, U4_def, - V0_def, V1_def, V2_def, V3_def, V4_def]); - -Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]); - - -Goal "Mutex : Always IU"; -by (always_tac 1); -qed "IU"; - -Goal "Mutex : Always IV"; -by (always_tac 1); -qed "IV"; - -(*The safety property: mutual exclusion*) -Goal "Mutex : Always {s. ~ (m s = 3 & n s = 3)}"; -by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1); -by Auto_tac; -qed "mutual_exclusion"; - - -(*The bad invariant FAILS in V1*) -Goal "Mutex : Always bad_IU"; -by (always_tac 1); -by Auto_tac; -(*Resulting state: n=1, p=false, m=4, u=false. - Execution of V1 (the command of process v guarded by n=1) sets p:=true, - violating the invariant!*) -(*Check that subgoals remain: proof failed.*) -getgoal 1; - - -Goal "((1::int) <= i & i <= 3) = (i = 1 | i = 2 | i = 3)"; -by (arith_tac 1); -qed "eq_123"; - - -(*** Progress for U ***) - -Goalw [Unless_def] "Mutex : {s. m s=2} Unless {s. m s=3}"; -by (constrains_tac 1); -qed "U_F0"; - -Goal "Mutex : {s. m s=1} LeadsTo {s. p s = v s & m s = 2}"; -by (ensures_tac "U1" 1); -qed "U_F1"; - -Goal "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}"; -by (cut_facts_tac [IU] 1); -by (ensures_tac "U2" 1); -qed "U_F2"; - -Goal "Mutex : {s. m s = 3} LeadsTo {s. p s}"; -by (res_inst_tac [("B", "{s. m s = 4}")] LeadsTo_Trans 1); -by (ensures_tac "U4" 2); -by (ensures_tac "U3" 1); -qed "U_F3"; - -Goal "Mutex : {s. m s = 2} LeadsTo {s. p s}"; -by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] - MRS LeadsTo_Diff) 1); -by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1); -by (auto_tac (claset() addSEs [less_SucE], simpset())); -val U_lemma2 = result(); - -Goal "Mutex : {s. m s = 1} LeadsTo {s. p s}"; -by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1); -by (Blast_tac 1); -val U_lemma1 = result(); - -Goal "Mutex : {s. 1 <= m s & m s <= 3} LeadsTo {s. p s}"; -by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, - U_lemma1, U_lemma2, U_F3] ) 1); -val U_lemma123 = result(); - -(*Misra's F4*) -Goal "Mutex : {s. u s} LeadsTo {s. p s}"; -by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1); -by Auto_tac; -qed "u_Leadsto_p"; - - -(*** Progress for V ***) - - -Goalw [Unless_def] "Mutex : {s. n s=2} Unless {s. n s=3}"; -by (constrains_tac 1); -qed "V_F0"; - -Goal "Mutex : {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}"; -by (ensures_tac "V1" 1); -qed "V_F1"; - -Goal "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}"; -by (cut_facts_tac [IV] 1); -by (ensures_tac "V2" 1); -qed "V_F2"; - -Goal "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}"; -by (res_inst_tac [("B", "{s. n s = 4}")] LeadsTo_Trans 1); -by (ensures_tac "V4" 2); -by (ensures_tac "V3" 1); -qed "V_F3"; - -Goal "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}"; -by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] - MRS LeadsTo_Diff) 1); -by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1); -by (auto_tac (claset() addSEs [less_SucE], simpset())); -val V_lemma2 = result(); - -Goal "Mutex : {s. n s = 1} LeadsTo {s. ~ p s}"; -by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1); -by (Blast_tac 1); -val V_lemma1 = result(); - -Goal "Mutex : {s. 1 <= n s & n s <= 3} LeadsTo {s. ~ p s}"; -by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, - V_lemma1, V_lemma2, V_F3] ) 1); -val V_lemma123 = result(); - - -(*Misra's F4*) -Goal "Mutex : {s. v s} LeadsTo {s. ~ p s}"; -by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1); -by Auto_tac; -qed "v_Leadsto_not_p"; - - -(** Absence of starvation **) - -(*Misra's F6*) -Goal "Mutex : {s. m s = 1} LeadsTo {s. m s = 3}"; -by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); -by (rtac U_F2 2); -by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); -by (stac Un_commute 1); -by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); -by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2); -by (rtac (U_F1 RS LeadsTo_weaken_R) 1); -by Auto_tac; -qed "m1_Leadsto_3"; - -(*The same for V*) -Goal "Mutex : {s. n s = 1} LeadsTo {s. n s = 3}"; -by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); -by (rtac V_F2 2); -by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1); -by (stac Un_commute 1); -by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1); -by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2); -by (rtac (V_F1 RS LeadsTo_weaken_R) 1); -by Auto_tac; -qed "n1_Leadsto_3"; diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Mutex.thy --- a/src/HOL/UNITY/Simple/Mutex.thy Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/Simple/Mutex.thy Fri Jan 24 14:06:49 2003 +0100 @@ -6,7 +6,7 @@ Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra *) -Mutex = SubstAx + +theory Mutex = UNITY_Main: record state = p :: bool @@ -53,7 +53,7 @@ V4 :: command "V4 == {(s,s'). s' = s (|p:=False, n:=0|) & n s = 4}" - Mutex :: state program + Mutex :: "state program" "Mutex == mk_program ({s. ~ u s & ~ v s & m s = 0 & n s = 0}, {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4}, UNIV)" @@ -61,16 +61,166 @@ (** The correct invariants **) - IU :: state set + IU :: "state set" "IU == {s. (u s = (1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}" - IV :: state set + IV :: "state set" "IV == {s. (v s = (1 <= n s & n s <= 3)) & (n s = 3 --> p s)}" (** The faulty invariant (for U alone) **) - bad_IU :: state set + bad_IU :: "state set" "bad_IU == {s. (u s = (1 <= m s & m s <= 3)) & (3 <= m s & m s <= 4 --> ~ p s)}" + +declare Mutex_def [THEN def_prg_Init, simp] + +declare U0_def [THEN def_act_simp, simp] +declare U1_def [THEN def_act_simp, simp] +declare U2_def [THEN def_act_simp, simp] +declare U3_def [THEN def_act_simp, simp] +declare U4_def [THEN def_act_simp, simp] +declare V0_def [THEN def_act_simp, simp] +declare V1_def [THEN def_act_simp, simp] +declare V2_def [THEN def_act_simp, simp] +declare V3_def [THEN def_act_simp, simp] +declare V4_def [THEN def_act_simp, simp] + +declare IU_def [THEN def_set_simp, simp] +declare IV_def [THEN def_set_simp, simp] +declare bad_IU_def [THEN def_set_simp, simp] + +lemma IU: "Mutex : Always IU" +apply (rule AlwaysI, force) +apply (unfold Mutex_def, constrains) +done + + +lemma IV: "Mutex : Always IV" +apply (rule AlwaysI, force) +apply (unfold Mutex_def, constrains) +done + +(*The safety property: mutual exclusion*) +lemma mutual_exclusion: "Mutex : Always {s. ~ (m s = 3 & n s = 3)}" +apply (rule Always_weaken) +apply (rule Always_Int_I [OF IU IV], auto) +done + + +(*The bad invariant FAILS in V1*) +lemma "Mutex : Always bad_IU" +apply (rule AlwaysI, force) +apply (unfold Mutex_def, constrains, auto) +(*Resulting state: n=1, p=false, m=4, u=false. + Execution of V1 (the command of process v guarded by n=1) sets p:=true, + violating the invariant!*) +oops + + +lemma eq_123: "((1::int) <= i & i <= 3) = (i = 1 | i = 2 | i = 3)" +by arith + + +(*** Progress for U ***) + +lemma U_F0: "Mutex : {s. m s=2} Unless {s. m s=3}" +by (unfold Unless_def Mutex_def, constrains) + +lemma U_F1: "Mutex : {s. m s=1} LeadsTo {s. p s = v s & m s = 2}" +by (unfold Mutex_def, ensures_tac "U1") + +lemma U_F2: "Mutex : {s. ~ p s & m s = 2} LeadsTo {s. m s = 3}" +apply (cut_tac IU) +apply (unfold Mutex_def, ensures_tac U2) +done + +lemma U_F3: "Mutex : {s. m s = 3} LeadsTo {s. p s}" +apply (rule_tac B = "{s. m s = 4}" in LeadsTo_Trans) + apply (unfold Mutex_def) + apply (ensures_tac U3) +apply (ensures_tac U4) +done + +lemma U_lemma2: "Mutex : {s. m s = 2} LeadsTo {s. p s}" +apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L + Int_lower2 [THEN subset_imp_LeadsTo]]) +apply (rule LeadsTo_Trans [OF U_F2 U_F3], auto) +done + +lemma U_lemma1: "Mutex : {s. m s = 1} LeadsTo {s. p s}" +by (rule LeadsTo_Trans [OF U_F1 [THEN LeadsTo_weaken_R] U_lemma2], blast) + +lemma U_lemma123: "Mutex : {s. 1 <= m s & m s <= 3} LeadsTo {s. p s}" +by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib U_lemma1 U_lemma2 U_F3) + +(*Misra's F4*) +lemma u_Leadsto_p: "Mutex : {s. u s} LeadsTo {s. p s}" +by (rule Always_LeadsTo_weaken [OF IU U_lemma123], auto) + + +(*** Progress for V ***) + + +lemma V_F0: "Mutex : {s. n s=2} Unless {s. n s=3}" +by (unfold Unless_def Mutex_def, constrains) + +lemma V_F1: "Mutex : {s. n s=1} LeadsTo {s. p s = (~ u s) & n s = 2}" +by (unfold Mutex_def, ensures_tac "V1") + +lemma V_F2: "Mutex : {s. p s & n s = 2} LeadsTo {s. n s = 3}" +apply (cut_tac IV) +apply (unfold Mutex_def, ensures_tac "V2") +done + +lemma V_F3: "Mutex : {s. n s = 3} LeadsTo {s. ~ p s}" +apply (rule_tac B = "{s. n s = 4}" in LeadsTo_Trans) + apply (unfold Mutex_def) + apply (ensures_tac V3) +apply (ensures_tac V4) +done + +lemma V_lemma2: "Mutex : {s. n s = 2} LeadsTo {s. ~ p s}" +apply (rule LeadsTo_Diff [OF LeadsTo_weaken_L + Int_lower2 [THEN subset_imp_LeadsTo]]) +apply (rule LeadsTo_Trans [OF V_F2 V_F3], auto) +done + +lemma V_lemma1: "Mutex : {s. n s = 1} LeadsTo {s. ~ p s}" +by (rule LeadsTo_Trans [OF V_F1 [THEN LeadsTo_weaken_R] V_lemma2], blast) + +lemma V_lemma123: "Mutex : {s. 1 <= n s & n s <= 3} LeadsTo {s. ~ p s}" +by (simp add: eq_123 Collect_disj_eq LeadsTo_Un_distrib V_lemma1 V_lemma2 V_F3) + + +(*Misra's F4*) +lemma v_Leadsto_not_p: "Mutex : {s. v s} LeadsTo {s. ~ p s}" +by (rule Always_LeadsTo_weaken [OF IV V_lemma123], auto) + + +(** Absence of starvation **) + +(*Misra's F6*) +lemma m1_Leadsto_3: "Mutex : {s. m s = 1} LeadsTo {s. m s = 3}" +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) +apply (rule_tac [2] U_F2) +apply (simp add: Collect_conj_eq) +apply (subst Un_commute) +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) + apply (rule_tac [2] PSP_Unless [OF v_Leadsto_not_p U_F0]) +apply (rule U_F1 [THEN LeadsTo_weaken_R], auto) +done + +(*The same for V*) +lemma n1_Leadsto_3: "Mutex : {s. n s = 1} LeadsTo {s. n s = 3}" +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) +apply (rule_tac [2] V_F2) +apply (simp add: Collect_conj_eq) +apply (subst Un_commute) +apply (rule LeadsTo_cancel2 [THEN LeadsTo_Un_duplicate]) + apply (rule_tac [2] PSP_Unless [OF u_Leadsto_p V_F0]) +apply (rule V_F1 [THEN LeadsTo_weaken_R], auto) +done + end diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Network.ML --- a/src/HOL/UNITY/Simple/Network.ML Thu Jan 23 10:30:14 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,59 +0,0 @@ -(* Title: HOL/UNITY/Network - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -The Communication Network - -From Misra, "A Logic for Concurrent Programming" (1994), section 5.7 -*) - -val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] = -Goalw [stable_def] - "[| !! m. F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \ -\ !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \ -\ !! m proc. F : stable {s. m <= s(proc,Sent)}; \ -\ !! n proc. F : stable {s. n <= s(proc,Rcvd)}; \ -\ !! m proc. F : {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m} co \ -\ {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}; \ -\ !! n proc. F : {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n} co \ -\ {s. s(proc,Sent) = n} \ -\ |] ==> F : stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 & \ -\ s(Aproc,Sent) = s(Bproc,Rcvd) & \ -\ s(Bproc,Sent) = s(Aproc,Rcvd) & \ -\ s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}"; - -val sent_nondec_A = read_instantiate [("proc","Aproc")] sent_nondec; -val sent_nondec_B = read_instantiate [("proc","Bproc")] sent_nondec; -val rcvd_nondec_A = read_instantiate [("proc","Aproc")] rcvd_nondec; -val rcvd_nondec_B = read_instantiate [("proc","Bproc")] rcvd_nondec; -val rcvd_idle_A = read_instantiate [("proc","Aproc")] rcvd_idle; -val rcvd_idle_B = read_instantiate [("proc","Bproc")] rcvd_idle; -val sent_idle_A = read_instantiate [("proc","Aproc")] sent_idle; -val sent_idle_B = read_instantiate [("proc","Bproc")] sent_idle; - -val rs_AB = [rsA, rsB] MRS constrains_Int; -val sent_nondec_AB = [sent_nondec_A, sent_nondec_B] MRS constrains_Int; -val rcvd_nondec_AB = [rcvd_nondec_A, rcvd_nondec_B] MRS constrains_Int; -val rcvd_idle_AB = [rcvd_idle_A, rcvd_idle_B] MRS constrains_Int; -val sent_idle_AB = [sent_idle_A, sent_idle_B] MRS constrains_Int; -val nondec_AB = [sent_nondec_AB, rcvd_nondec_AB] MRS constrains_Int; -val idle_AB = [rcvd_idle_AB, sent_idle_AB] MRS constrains_Int; -val nondec_idle = [nondec_AB, idle_AB] MRS constrains_Int; - -by (rtac constrainsI 1); -by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1); -by (assume_tac 1); -by (ALLGOALS Asm_full_simp_tac); -by (blast_tac (HOL_cs addIs [order_refl]) 1); -by (Clarify_tac 1); -by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)", - "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1); -by (REPEAT - (blast_tac (claset() addIs [order_antisym, le_trans, eq_imp_le]) 2)); -by (Asm_simp_tac 1); -result(); - - - - diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Network.thy --- a/src/HOL/UNITY/Simple/Network.thy Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/Simple/Network.thy Fri Jan 24 14:06:49 2003 +0100 @@ -8,7 +8,7 @@ From Misra, "A Logic for Concurrent Programming" (1994), section 5.7 *) -Network = UNITY + +theory Network = UNITY: (*The state assigns a number to each process variable*) @@ -18,4 +18,53 @@ types state = "pname * pvar => nat" +locale F_props = + fixes F + assumes rsA: "F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}" + and rsB: "F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}" + and sent_nondec: "F : stable {s. m <= s(proc,Sent)}" + and rcvd_nondec: "F : stable {s. n <= s(proc,Rcvd)}" + and rcvd_idle: "F : {s. s(proc,Idle) = Suc 0 & s(proc,Rcvd) = m} + co {s. s(proc,Rcvd) = m --> s(proc,Idle) = Suc 0}" + and sent_idle: "F : {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n} + co {s. s(proc,Sent) = n}" + + +lemmas (in F_props) + sent_nondec_A = sent_nondec [of _ Aproc] + and sent_nondec_B = sent_nondec [of _ Bproc] + and rcvd_nondec_A = rcvd_nondec [of _ Aproc] + and rcvd_nondec_B = rcvd_nondec [of _ Bproc] + and rcvd_idle_A = rcvd_idle [of Aproc] + and rcvd_idle_B = rcvd_idle [of Bproc] + and sent_idle_A = sent_idle [of Aproc] + and sent_idle_B = sent_idle [of Bproc] + + and rs_AB = stable_Int [OF rsA rsB] + and sent_nondec_AB = stable_Int [OF sent_nondec_A sent_nondec_B] + and rcvd_nondec_AB = stable_Int [OF rcvd_nondec_A rcvd_nondec_B] + and rcvd_idle_AB = constrains_Int [OF rcvd_idle_A rcvd_idle_B] + and sent_idle_AB = constrains_Int [OF sent_idle_A sent_idle_B] + and nondec_AB = stable_Int [OF sent_nondec_AB rcvd_nondec_AB] + and idle_AB = constrains_Int [OF rcvd_idle_AB sent_idle_AB] + and nondec_idle = constrains_Int [OF nondec_AB [unfolded stable_def] + idle_AB] + +lemma (in F_props) + shows "F : stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 & + s(Aproc,Sent) = s(Bproc,Rcvd) & + s(Bproc,Sent) = s(Aproc,Rcvd) & + s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}" +apply (unfold stable_def) +apply (rule constrainsI) +apply (drule constrains_Int [OF rs_AB [unfolded stable_def] nondec_idle, + THEN constrainsD], assumption) +apply simp_all +apply (blast intro!: order_refl del: le0, clarify) +apply (subgoal_tac "s' (Aproc, Rcvd) = s (Aproc, Rcvd)") +apply (subgoal_tac "s' (Bproc, Rcvd) = s (Bproc, Rcvd)") +apply simp +apply (blast intro: order_antisym le_trans eq_imp_le)+ +done + end diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Reach.ML --- a/src/HOL/UNITY/Simple/Reach.ML Thu Jan 23 10:30:14 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,142 +0,0 @@ -(* Title: HOL/UNITY/Reach.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Reachability in Directed Graphs. From Chandy and Misra, section 6.4. - [ this example took only four days!] -*) - -(*TO SIMPDATA.ML?? FOR CLASET?? *) -val major::prems = goal thy - "[| if P then Q else R; \ -\ [| P; Q |] ==> S; \ -\ [| ~ P; R |] ==> S |] ==> S"; -by (cut_facts_tac [major] 1); -by (blast_tac (claset() addSDs [if_bool_eq_disj RS iffD1] addIs prems) 1); -qed "ifE"; - -AddSEs [ifE]; - - -Addsimps [Rprg_def RS def_prg_Init]; -program_defs_ref := [Rprg_def]; - -Addsimps [simp_of_act asgt_def]; - -(*All vertex sets are finite*) -AddIffs [[subset_UNIV, finite_graph] MRS finite_subset]; - -Addsimps [simp_of_set reach_invariant_def]; - -Goal "Rprg : Always reach_invariant"; -by (always_tac 1); -by (blast_tac (claset() addIs [rtrancl_trans]) 1); -qed "reach_invariant"; - - -(*** Fixedpoint ***) - -(*If it reaches a fixedpoint, it has found a solution*) -Goalw [fixedpoint_def] - "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }"; -by (rtac equalityI 1); -by (auto_tac (claset() addSIs [ext], simpset())); -by (blast_tac (claset() addIs [rtrancl_trans]) 2); -by (etac rtrancl_induct 1); -by Auto_tac; -qed "fixedpoint_invariant_correct"; - -Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def] - "FP Rprg <= fixedpoint"; -by Auto_tac; -by (dtac bspec 1 THEN atac 1); -by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1); -by (dtac fun_cong 1); -by Auto_tac; -val lemma1 = result(); - -Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def] - "fixedpoint <= FP Rprg"; -by (auto_tac (claset() addSIs [ext], simpset())); -val lemma2 = result(); - -Goal "FP Rprg = fixedpoint"; -by (rtac ([lemma1,lemma2] MRS equalityI) 1); -qed "FP_fixedpoint"; - - -(*If we haven't reached a fixedpoint then there is some edge for which u but - not v holds. Progress will be proved via an ENSURES assertion that the - metric will decrease for each suitable edge. A union over all edges proves - a LEADSTO assertion that the metric decreases if we are not at a fixedpoint. - *) - -Goal "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})"; -by (simp_tac (simpset() addsimps - [Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, Rprg_def]) 1); -by Auto_tac; -by (rtac fun_upd_idem 1); -by Auto_tac; -by (force_tac (claset() addSIs [rev_bexI], - simpset() addsimps [fun_upd_idem_iff]) 1); -qed "Compl_fixedpoint"; - -Goal "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})"; -by (simp_tac (simpset() addsimps [Diff_eq, Compl_fixedpoint]) 1); -by (Blast_tac 1); -qed "Diff_fixedpoint"; - - -(*** Progress ***) - -Goalw [metric_def] "~ s x ==> Suc (metric (s(x:=True))) = metric s"; -by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1); -by (Force_tac 2); -by (asm_full_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1); -qed "Suc_metric"; - -Goal "~ s x ==> metric (s(x:=True)) < metric s"; -by (etac (Suc_metric RS subst) 1); -by (Blast_tac 1); -qed "metric_less"; -AddSIs [metric_less]; - -Goal "metric (s(y:=s x | s y)) <= metric s"; -by (case_tac "s x --> s y" 1); -by (auto_tac (claset() addIs [less_imp_le], - simpset() addsimps [fun_upd_idem])); -qed "metric_le"; - -Goal "Rprg : ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))"; -by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1); -by (rtac LeadsTo_UN 1); -by Auto_tac; -by (ensures_tac "asgt a b" 1); -by (Blast_tac 2); -by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1); -by (dtac (metric_le RS order_antisym) 1); -by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)], - simpset())); -qed "LeadsTo_Diff_fixedpoint"; - -Goal "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)"; -by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R, - subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); -by Auto_tac; -qed "LeadsTo_Un_fixedpoint"; - - -(*Execution in any state leads to a fixedpoint (i.e. can terminate)*) -Goal "Rprg : UNIV LeadsTo fixedpoint"; -by (rtac LessThan_induct 1); -by Auto_tac; -by (rtac LeadsTo_Un_fixedpoint 1); -qed "LeadsTo_fixedpoint"; - -Goal "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }"; -by (stac (fixedpoint_invariant_correct RS sym) 1); -by (rtac ([reach_invariant, LeadsTo_fixedpoint] - MRS Always_LeadsTo_weaken) 1); -by Auto_tac; -qed "LeadsTo_correct"; diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Reach.thy --- a/src/HOL/UNITY/Simple/Reach.thy Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/Simple/Reach.thy Fri Jan 24 14:06:49 2003 +0100 @@ -4,14 +4,14 @@ Copyright 1998 University of Cambridge Reachability in Directed Graphs. From Chandy and Misra, section 6.4. + [this example took only four days!] *) -Reach = FP + SubstAx + +theory Reach = UNITY_Main: -types vertex - state = "vertex=>bool" +typedecl vertex -arities vertex :: type +types state = "vertex=>bool" consts init :: "vertex" @@ -23,21 +23,142 @@ asgt :: "[vertex,vertex] => (state*state) set" "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" - Rprg :: state program + Rprg :: "state program" "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)" - reach_invariant :: state set + reach_invariant :: "state set" "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}" - fixedpoint :: state set + fixedpoint :: "state set" "fixedpoint == {s. ALL (u,v): edges. s u --> s v}" - metric :: state => nat + metric :: "state => nat" "metric s == card {v. ~ s v}" -rules + +text{**We assume that the set of vertices is finite*} +axioms + finite_graph: "finite (UNIV :: vertex set)" + + + + +(*TO SIMPDATA.ML?? FOR CLASET?? *) +lemma ifE [elim!]: + "[| if P then Q else R; + [| P; Q |] ==> S; + [| ~ P; R |] ==> S |] ==> S" +by (simp split: split_if_asm) + + +declare Rprg_def [THEN def_prg_Init, simp] + +declare asgt_def [THEN def_act_simp,simp] + +(*All vertex sets are finite*) +declare finite_subset [OF subset_UNIV finite_graph, iff] + +declare reach_invariant_def [THEN def_set_simp, simp] + +lemma reach_invariant: "Rprg : Always reach_invariant" +apply (rule AlwaysI, force) +apply (unfold Rprg_def, constrains) +apply (blast intro: rtrancl_trans) +done + + +(*** Fixedpoint ***) + +(*If it reaches a fixedpoint, it has found a solution*) +lemma fixedpoint_invariant_correct: + "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }" +apply (unfold fixedpoint_def) +apply (rule equalityI) +apply (auto intro!: ext) + prefer 2 apply (blast intro: rtrancl_trans) +apply (erule rtrancl_induct, auto) +done + +lemma lemma1: + "FP Rprg <= fixedpoint" +apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def, auto) +apply (drule bspec, assumption) +apply (simp add: Image_singleton image_iff) +apply (drule fun_cong, auto) +done + +lemma lemma2: + "fixedpoint <= FP Rprg" +apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def) +apply (auto intro!: ext) +done + +lemma FP_fixedpoint: "FP Rprg = fixedpoint" +by (rule equalityI [OF lemma1 lemma2]) + - (*We assume that the set of vertices is finite*) - finite_graph "finite (UNIV :: vertex set)" - +(*If we haven't reached a fixedpoint then there is some edge for which u but + not v holds. Progress will be proved via an ENSURES assertion that the + metric will decrease for each suitable edge. A union over all edges proves + a LEADSTO assertion that the metric decreases if we are not at a fixedpoint. + *) + +lemma Compl_fixedpoint: "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})" +apply (simp add: Compl_FP UN_UN_flatten FP_fixedpoint [symmetric] Rprg_def, auto) + apply (rule fun_upd_idem, force) +apply (force intro!: rev_bexI simp add: fun_upd_idem_iff) +done + +lemma Diff_fixedpoint: + "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})" +apply (simp add: Diff_eq Compl_fixedpoint, blast) +done + + +(*** Progress ***) + +lemma Suc_metric: "~ s x ==> Suc (metric (s(x:=True))) = metric s" +apply (unfold metric_def) +apply (subgoal_tac "{v. ~ (s (x:=True)) v} = {v. ~ s v} - {x}") + prefer 2 apply force +apply (simp add: card_Suc_Diff1) +done + +lemma metric_less [intro!]: "~ s x ==> metric (s(x:=True)) < metric s" +by (erule Suc_metric [THEN subst], blast) + +lemma metric_le: "metric (s(y:=s x | s y)) <= metric s" +apply (case_tac "s x --> s y") +apply (auto intro: less_imp_le simp add: fun_upd_idem) +done + +lemma LeadsTo_Diff_fixedpoint: + "Rprg : ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))" +apply (simp (no_asm) add: Diff_fixedpoint Rprg_def) +apply (rule LeadsTo_UN, auto) +apply (ensures_tac "asgt a b") + prefer 2 apply blast +apply (simp (no_asm_use) add: not_less_iff_le) +apply (drule metric_le [THEN order_antisym]) +apply (auto elim: less_not_refl3 [THEN [2] rev_notE]) +done + +lemma LeadsTo_Un_fixedpoint: + "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)" +apply (rule LeadsTo_Diff [OF LeadsTo_Diff_fixedpoint [THEN LeadsTo_weaken_R] + subset_imp_LeadsTo], auto) +done + + +(*Execution in any state leads to a fixedpoint (i.e. can terminate)*) +lemma LeadsTo_fixedpoint: "Rprg : UNIV LeadsTo fixedpoint" +apply (rule LessThan_induct, auto) +apply (rule LeadsTo_Un_fixedpoint) +done + +lemma LeadsTo_correct: "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }" +apply (subst fixedpoint_invariant_correct [symmetric]) +apply (rule Always_LeadsTo_weaken [OF reach_invariant LeadsTo_fixedpoint], auto) +done + end diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Reachability.ML --- a/src/HOL/UNITY/Simple/Reachability.ML Thu Jan 23 10:30:14 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,306 +0,0 @@ -(* Title: HOL/UNITY/Reachability - ID: $Id$ - Author: Tanja Vos, Cambridge University Computer Laboratory - Copyright 2000 University of Cambridge - -Reachability in Graphs - -From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3 -*) - -bind_thm("E_imp_in_V_L", Graph2 RS conjunct1); -bind_thm("E_imp_in_V_R", Graph2 RS conjunct2); - -Goal "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v"; -by (rtac (MA7 RS PSP_Stable RS LeadsTo_weaken_L) 1); -by (rtac MA6 3); -by (auto_tac (claset(), simpset() addsimps [E_imp_in_V_L, E_imp_in_V_R])); -qed "lemma2"; - -Goal "(v,w) : E ==> F : reachable v LeadsTo reachable w"; -by (rtac (MA4 RS Always_LeadsTo_weaken) 1); -by (rtac lemma2 2); -by (auto_tac (claset(), simpset() addsimps [nmsg_eq_def, nmsg_gt_def])); -qed "Induction_base"; - -Goal "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w"; -by (etac REACHABLE.induct 1); -by (rtac subset_imp_LeadsTo 1); -by (Blast_tac 1); -by (blast_tac (claset() addIs [LeadsTo_Trans, Induction_base]) 1); -qed "REACHABLE_LeadsTo_reachable"; - -Goal "F : {s. (root,v) : REACHABLE} LeadsTo reachable v"; -by (rtac single_LeadsTo_I 1); -by (full_simp_tac (simpset() addsplits [split_if_asm]) 1); -by (rtac (MA1 RS Always_LeadsToI) 1); -by (etac (REACHABLE_LeadsTo_reachable RS LeadsTo_weaken_L) 1); -by Auto_tac; -qed "Detects_part1"; - - -Goalw [Detects_def] - "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}"; -by Auto_tac; -by (blast_tac (claset() addIs [MA2 RS Always_weaken]) 2); -by (rtac (Detects_part1 RS LeadsTo_weaken_L) 1); -by (Blast_tac 1); -qed "Reachability_Detected"; - - -Goal "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})"; -by (etac (Reachability_Detected RS Detects_Imp_LeadstoEQ) 1); -qed "LeadsTo_Reachability"; - -(* ------------------------------------ *) - -(* Some lemmas about <==> *) - -Goalw [Equality_def] - "(reachable v <==> {s. (root,v) : REACHABLE}) = \ -\ {s. ((s : reachable v) = ((root,v) : REACHABLE))}"; -by (Blast_tac 1); -qed "Eq_lemma1"; - - -Goalw [Equality_def] - "(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) = \ -\ {s. ((s : reachable v) = ((root,v) : REACHABLE))}"; -by Auto_tac; -qed "Eq_lemma2"; - -(* ------------------------------------ *) - - -(* Some lemmas about final (I don't need all of them!) *) - -Goalw [final_def, Equality_def] - "(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) & \ -\ s : nmsg_eq 0 (v,w)}) \ -\ <= final"; -by Auto_tac; -by (ftac E_imp_in_V_R 1); -by (ftac E_imp_in_V_L 1); -by (Blast_tac 1); -qed "final_lemma1"; - -Goalw [final_def, Equality_def] - "E~={} \ -\ ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))} \ -\ Int nmsg_eq 0 e) <= final"; -by (auto_tac (claset(), simpset() addsplits [split_if_asm])); -by (ftac E_imp_in_V_L 1); -by (Blast_tac 1); -qed "final_lemma2"; - -Goal "E~={} \ -\ ==> (INT v: V. INT e: E. \ -\ (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \ -\ <= final"; -by (ftac final_lemma2 1); -by (full_simp_tac (simpset() addsimps [Eq_lemma2]) 1); -qed "final_lemma3"; - - -Goal "E~={} \ -\ ==> (INT v: V. INT e: E. \ -\ {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e) \ -\ = final"; -by (rtac subset_antisym 1); -by (etac final_lemma2 1); -by (rewrite_goals_tac [final_def,Equality_def]); -by (Blast_tac 1); -qed "final_lemma4"; - -Goal "E~={} \ -\ ==> (INT v: V. INT e: E. \ -\ ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \ -\ = final"; -by (ftac final_lemma4 1); -by (full_simp_tac (simpset() addsimps [Eq_lemma2]) 1); -qed "final_lemma5"; - - -Goal "(INT v: V. INT w: V. \ -\ (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)) \ -\ <= final"; -by (simp_tac (simpset() addsimps [Eq_lemma2, Int_def]) 1); -by (rtac final_lemma1 1); -qed "final_lemma6"; - - -Goalw [final_def] - "final = \ -\ (INT v: V. INT w: V. \ -\ ((reachable v) <==> {s. (root,v) : REACHABLE}) Int \ -\ (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))"; -by (rtac subset_antisym 1); -by (Blast_tac 1); -by (auto_tac (claset(), simpset() addsplits [split_if_asm])); -by (ALLGOALS (blast_tac (claset() addDs [E_imp_in_V_L, E_imp_in_V_R]))); -qed "final_lemma7"; - -(* ------------------------------------ *) - - -(* ------------------------------------ *) - -(* Stability theorems *) - - -Goal "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)"; -by (dtac (MA2 RS AlwaysD) 1); -by Auto_tac; -qed "not_REACHABLE_imp_Stable_not_reachable"; - -Goal "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})"; -by (simp_tac (simpset() addsimps [Equality_def, Eq_lemma2]) 1); -by (blast_tac (claset() addIs [MA6,not_REACHABLE_imp_Stable_not_reachable]) 1); -qed "Stable_reachable_EQ_R"; - - -Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def] - "((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \ -\ <= A Un nmsg_eq 0 (v,w)"; -by Auto_tac; -qed "lemma4"; - - -Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def] - "reachable v Int nmsg_eq 0 (v,w) = \ -\ ((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int \ -\ (reachable v Int nmsg_lte 0 (v,w)))"; -by Auto_tac; -qed "lemma5"; - -Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def] - "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v"; -by Auto_tac; -qed "lemma6"; - -Goal "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))"; -by (rtac ([MA5, MA3] MRS Always_Int_I RS Always_weaken) 1); -by (rtac lemma4 5); -by Auto_tac; -qed "Always_reachable_OR_nmsg_0"; - -Goal "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))"; -by (stac lemma5 1); -by (blast_tac (claset() addIs [MA5, Always_imp_Stable RS Stable_Int, MA6b]) 1); -qed "Stable_reachable_AND_nmsg_0"; - -Goal "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)"; -by (blast_tac (claset() addSIs [Always_weaken RS Always_imp_Stable, - lemma6, MA3]) 1); -qed "Stable_nmsg_0_OR_reachable"; - -Goal "[| v : V; w:V; (root,v) ~: REACHABLE |] \ -\ ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))"; -by (rtac ([MA2 RS Always_imp_Stable, Stable_nmsg_0_OR_reachable] MRS - Stable_Int RS Stable_eq) 1); -by (Blast_tac 4); -by Auto_tac; -qed "not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0"; - -Goal "[| v : V; w:V |] \ -\ ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int \ -\ nmsg_eq 0 (v,w))"; -by (asm_simp_tac - (simpset() addsimps [Equality_def, Eq_lemma2, - not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0, - Stable_reachable_AND_nmsg_0]) 1); -qed "Stable_reachable_EQ_R_AND_nmsg_0"; - - -(* ------------------------------------ *) - - -(* LeadsTo final predicate (Exercise 11.2 page 274) *) - -Goal "UNIV <= (INT v: V. UNIV)"; -by (Blast_tac 1); -val UNIV_lemma = result(); - -val UNIV_LeadsTo_completion = - [Finite_stable_completion, UNIV_lemma] MRS LeadsTo_weaken_L; - -Goalw [final_def] "E={} ==> F : UNIV LeadsTo final"; -by (Asm_full_simp_tac 1); -by (rtac UNIV_LeadsTo_completion 1); -by Safe_tac; -by (etac (simplify (simpset()) LeadsTo_Reachability) 1); -by (dtac Stable_reachable_EQ_R 1); -by (Asm_full_simp_tac 1); -qed "LeadsTo_final_E_empty"; - - -Goal "[| v : V; w:V |] \ -\ ==> F : UNIV LeadsTo \ -\ ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))"; -by (rtac (LeadsTo_Reachability RS LeadsTo_Trans) 1); -by (Blast_tac 1); -by (subgoal_tac "F : (reachable v <==> {s. (root,v) : REACHABLE}) Int UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)" 1); -by (Asm_full_simp_tac 1); -by (rtac PSP_Stable2 1); -by (rtac MA7 1); -by (rtac Stable_reachable_EQ_R 3); -by Auto_tac; -qed "Leadsto_reachability_AND_nmsg_0"; - - -Goal "E~={} ==> F : UNIV LeadsTo final"; -by (rtac ([LeadsTo_weaken_R, UNIV_lemma] MRS LeadsTo_weaken_L) 1); -by (rtac final_lemma6 2); -by (rtac Finite_stable_completion 1); -by (Blast_tac 1); -by (rtac UNIV_LeadsTo_completion 1); -by (REPEAT - (blast_tac (claset() addIs [Stable_INT, - Stable_reachable_EQ_R_AND_nmsg_0, - Leadsto_reachability_AND_nmsg_0]) 1)); -qed "LeadsTo_final_E_NOT_empty"; - - -Goal "F : UNIV LeadsTo final"; -by (case_tac "E={}" 1); -by (rtac LeadsTo_final_E_NOT_empty 2); -by (rtac LeadsTo_final_E_empty 1); -by Auto_tac; -qed "LeadsTo_final"; - -(* ------------------------------------ *) - -(* Stability of final (Exercise 11.2 page 274) *) - -Goalw [final_def] "E={} ==> F : Stable final"; -by (Asm_full_simp_tac 1); -by (rtac Stable_INT 1); -by (dtac Stable_reachable_EQ_R 1); -by (Asm_full_simp_tac 1); -qed "Stable_final_E_empty"; - - -Goal "E~={} ==> F : Stable final"; -by (stac final_lemma7 1); -by (rtac Stable_INT 1); -by (rtac Stable_INT 1); -by (simp_tac (simpset() addsimps [Eq_lemma2]) 1); -by Safe_tac; -by (rtac Stable_eq 1); -by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)} Int nmsg_eq 0 (v,w)) = \ -\ ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- UNIV Un nmsg_eq 0 (v,w)))" 2); -by (Blast_tac 2); by (Blast_tac 2); -by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R_AND_nmsg_0) 1); -by (Blast_tac 1);by (Blast_tac 1); -by (rtac Stable_eq 1); -by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)}) = ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- {} Un nmsg_eq 0 (v,w)))" 2); -by (Blast_tac 2); by (Blast_tac 2); -by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R) 1); -by Auto_tac; -qed "Stable_final_E_NOT_empty"; - -Goal "F : Stable final"; -by (case_tac "E={}" 1); -by (blast_tac (claset() addIs [Stable_final_E_NOT_empty]) 2); -by (blast_tac (claset() addIs [Stable_final_E_empty]) 1); -qed "Stable_final"; diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Reachability.thy --- a/src/HOL/UNITY/Simple/Reachability.thy Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/Simple/Reachability.thy Fri Jan 24 14:06:49 2003 +0100 @@ -8,65 +8,367 @@ From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3 *) -Reachability = Detects + +theory Reachability = Detects + Reach: types edge = "(vertex*vertex)" record state = - reach :: vertex => bool - nmsg :: edge => nat + reach :: "vertex => bool" + nmsg :: "edge => nat" -consts REACHABLE :: edge set - root :: vertex - E :: edge set - V :: vertex set +consts REACHABLE :: "edge set" + root :: "vertex" + E :: "edge set" + V :: "vertex set" inductive "REACHABLE" - intrs - base "v : V ==> ((v,v) : REACHABLE)" - step "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)" + intros + base: "v : V ==> ((v,v) : REACHABLE)" + step: "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)" constdefs - reachable :: vertex => state set + reachable :: "vertex => state set" "reachable p == {s. reach s p}" - nmsg_eq :: nat => edge => state set + nmsg_eq :: "nat => edge => state set" "nmsg_eq k == %e. {s. nmsg s e = k}" - nmsg_gt :: nat => edge => state set + nmsg_gt :: "nat => edge => state set" "nmsg_gt k == %e. {s. k < nmsg s e}" - nmsg_gte :: nat => edge => state set + nmsg_gte :: "nat => edge => state set" "nmsg_gte k == %e. {s. k <= nmsg s e}" - nmsg_lte :: nat => edge => state set + nmsg_lte :: "nat => edge => state set" "nmsg_lte k == %e. {s. nmsg s e <= k}" - final :: state set + final :: "state set" "final == (INTER V (%v. reachable v <==> {s. (root, v) : REACHABLE})) Int (INTER E (nmsg_eq 0))" -rules - Graph1 "root : V" +axioms + + Graph1: "root : V" + + Graph2: "(v,w) : E ==> (v : V) & (w : V)" + + MA1: "F : Always (reachable root)" + + MA2: "v: V ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})" + + MA3: "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))" + + MA4: "(v,w) : E ==> + F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))" + + MA5: "[|v:V; w:V|] + ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w))" + + MA6: "[|v:V|] ==> F : Stable (reachable v)" + + MA6b: "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))" + + MA7: "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)" + + +lemmas E_imp_in_V_L = Graph2 [THEN conjunct1, standard] +lemmas E_imp_in_V_R = Graph2 [THEN conjunct2, standard] + +lemma lemma2: + "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v" +apply (rule MA7 [THEN PSP_Stable, THEN LeadsTo_weaken_L]) +apply (rule_tac [3] MA6) +apply (auto simp add: E_imp_in_V_L E_imp_in_V_R) +done + +lemma Induction_base: "(v,w) : E ==> F : reachable v LeadsTo reachable w" +apply (rule MA4 [THEN Always_LeadsTo_weaken]) +apply (rule_tac [2] lemma2) +apply (auto simp add: nmsg_eq_def nmsg_gt_def) +done + +lemma REACHABLE_LeadsTo_reachable: + "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w" +apply (erule REACHABLE.induct) +apply (rule subset_imp_LeadsTo, blast) +apply (blast intro: LeadsTo_Trans Induction_base) +done + +lemma Detects_part1: "F : {s. (root,v) : REACHABLE} LeadsTo reachable v" +apply (rule single_LeadsTo_I) +apply (simp split add: split_if_asm) +apply (rule MA1 [THEN Always_LeadsToI]) +apply (erule REACHABLE_LeadsTo_reachable [THEN LeadsTo_weaken_L], auto) +done + + +lemma Reachability_Detected: + "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}" +apply (unfold Detects_def, auto) + prefer 2 apply (blast intro: MA2 [THEN Always_weaken]) +apply (rule Detects_part1 [THEN LeadsTo_weaken_L], blast) +done + + +lemma LeadsTo_Reachability: + "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})" +by (erule Reachability_Detected [THEN Detects_Imp_LeadstoEQ]) + + +(* ------------------------------------ *) + +(* Some lemmas about <==> *) + +lemma Eq_lemma1: + "(reachable v <==> {s. (root,v) : REACHABLE}) = + {s. ((s : reachable v) = ((root,v) : REACHABLE))}" +apply (unfold Equality_def, blast) +done + - Graph2 "(v,w) : E ==> (v : V) & (w : V)" +lemma Eq_lemma2: + "(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) = + {s. ((s : reachable v) = ((root,v) : REACHABLE))}" +apply (unfold Equality_def, auto) +done + +(* ------------------------------------ *) + + +(* Some lemmas about final (I don't need all of them!) *) + +lemma final_lemma1: + "(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) & + s : nmsg_eq 0 (v,w)}) + <= final" +apply (unfold final_def Equality_def, auto) +apply (frule E_imp_in_V_R) +apply (frule E_imp_in_V_L, blast) +done + +lemma final_lemma2: + "E~={} + ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))} + Int nmsg_eq 0 e) <= final" +apply (unfold final_def Equality_def) +apply (auto split add: split_if_asm) +apply (frule E_imp_in_V_L, blast) +done + +lemma final_lemma3: + "E~={} + ==> (INT v: V. INT e: E. + (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) + <= final" +apply (frule final_lemma2) +apply (simp (no_asm_use) add: Eq_lemma2) +done + - MA1 "F : Always (reachable root)" +lemma final_lemma4: + "E~={} + ==> (INT v: V. INT e: E. + {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e) + = final" +apply (rule subset_antisym) +apply (erule final_lemma2) +apply (unfold final_def Equality_def, blast) +done + +lemma final_lemma5: + "E~={} + ==> (INT v: V. INT e: E. + ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) + = final" +apply (frule final_lemma4) +apply (simp (no_asm_use) add: Eq_lemma2) +done + - MA2 "[|v:V|] ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})" +lemma final_lemma6: + "(INT v: V. INT w: V. + (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)) + <= final" +apply (simp (no_asm) add: Eq_lemma2 Int_def) +apply (rule final_lemma1) +done + + +lemma final_lemma7: + "final = + (INT v: V. INT w: V. + ((reachable v) <==> {s. (root,v) : REACHABLE}) Int + (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))" +apply (unfold final_def) +apply (rule subset_antisym, blast) +apply (auto split add: split_if_asm) +apply (blast dest: E_imp_in_V_L E_imp_in_V_R)+ +done + +(* ------------------------------------ *) - MA3 "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))" + +(* ------------------------------------ *) + +(* Stability theorems *) +lemma not_REACHABLE_imp_Stable_not_reachable: + "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)" +apply (drule MA2 [THEN AlwaysD], auto) +done + +lemma Stable_reachable_EQ_R: + "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})" +apply (simp (no_asm) add: Equality_def Eq_lemma2) +apply (blast intro: MA6 not_REACHABLE_imp_Stable_not_reachable) +done + + +lemma lemma4: + "((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int + (- nmsg_gt 0 (v,w) Un A)) + <= A Un nmsg_eq 0 (v,w)" +apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto) +done + + +lemma lemma5: + "reachable v Int nmsg_eq 0 (v,w) = + ((nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w)) Int + (reachable v Int nmsg_lte 0 (v,w)))" +apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto) +done + +lemma lemma6: + "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v" +apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto) +done - MA4 "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))" +lemma Always_reachable_OR_nmsg_0: + "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))" +apply (rule Always_Int_I [OF MA5 MA3, THEN Always_weaken]) +apply (rule_tac [5] lemma4, auto) +done + +lemma Stable_reachable_AND_nmsg_0: + "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))" +apply (subst lemma5) +apply (blast intro: MA5 Always_imp_Stable [THEN Stable_Int] MA6b) +done + +lemma Stable_nmsg_0_OR_reachable: + "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)" +by (blast intro!: Always_weaken [THEN Always_imp_Stable] lemma6 MA3) - MA5 "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w))" +lemma not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0: + "[| v : V; w:V; (root,v) ~: REACHABLE |] + ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))" +apply (rule Stable_Int [OF MA2 [THEN Always_imp_Stable] + Stable_nmsg_0_OR_reachable, + THEN Stable_eq]) + prefer 4 apply blast +apply auto +done + +lemma Stable_reachable_EQ_R_AND_nmsg_0: + "[| v : V; w:V |] + ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int + nmsg_eq 0 (v,w))" +by (simp add: Equality_def Eq_lemma2 Stable_reachable_AND_nmsg_0 + not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0) + + + +(* ------------------------------------ *) + + +(* LeadsTo final predicate (Exercise 11.2 page 274) *) + +lemma UNIV_lemma: "UNIV <= (INT v: V. UNIV)" +by blast - MA6 "[|v:V|] ==> F : Stable (reachable v)" +lemmas UNIV_LeadsTo_completion = + LeadsTo_weaken_L [OF Finite_stable_completion UNIV_lemma] + +lemma LeadsTo_final_E_empty: "E={} ==> F : UNIV LeadsTo final" +apply (unfold final_def, simp) +apply (rule UNIV_LeadsTo_completion) + apply safe + apply (erule LeadsTo_Reachability [simplified]) +apply (drule Stable_reachable_EQ_R, simp) +done + + +lemma Leadsto_reachability_AND_nmsg_0: + "[| v : V; w:V |] + ==> F : UNIV LeadsTo + ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))" +apply (rule LeadsTo_Reachability [THEN LeadsTo_Trans], blast) +apply (subgoal_tac + "F : (reachable v <==> {s. (root,v) : REACHABLE}) Int + UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE}) Int + nmsg_eq 0 (v,w) ") +apply simp +apply (rule PSP_Stable2) +apply (rule MA7) +apply (rule_tac [3] Stable_reachable_EQ_R, auto) +done + +lemma LeadsTo_final_E_NOT_empty: "E~={} ==> F : UNIV LeadsTo final" +apply (rule LeadsTo_weaken_L [OF LeadsTo_weaken_R UNIV_lemma]) +apply (rule_tac [2] final_lemma6) +apply (rule Finite_stable_completion) + apply blast + apply (rule UNIV_LeadsTo_completion) + apply (blast intro: Stable_INT Stable_reachable_EQ_R_AND_nmsg_0 + Leadsto_reachability_AND_nmsg_0)+ +done - MA6b "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))" +lemma LeadsTo_final: "F : UNIV LeadsTo final" +apply (case_tac "E={}") +apply (rule_tac [2] LeadsTo_final_E_NOT_empty) +apply (rule LeadsTo_final_E_empty, auto) +done + +(* ------------------------------------ *) + +(* Stability of final (Exercise 11.2 page 274) *) + +lemma Stable_final_E_empty: "E={} ==> F : Stable final" +apply (unfold final_def, simp) +apply (rule Stable_INT) +apply (drule Stable_reachable_EQ_R, simp) +done + - MA7 "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)" +lemma Stable_final_E_NOT_empty: "E~={} ==> F : Stable final" +apply (subst final_lemma7) +apply (rule Stable_INT) +apply (rule Stable_INT) +apply (simp (no_asm) add: Eq_lemma2) +apply safe +apply (rule Stable_eq) +apply (subgoal_tac [2] "({s. (s : reachable v) = ((root,v) : REACHABLE) } Int nmsg_eq 0 (v,w)) = ({s. (s : reachable v) = ( (root,v) : REACHABLE) } Int (- UNIV Un nmsg_eq 0 (v,w))) ") +prefer 2 apply blast +prefer 2 apply blast +apply (rule Stable_reachable_EQ_R_AND_nmsg_0 + [simplified Eq_lemma2 Collect_const]) +apply (blast, blast) +apply (rule Stable_eq) + apply (rule Stable_reachable_EQ_R [simplified Eq_lemma2 Collect_const]) + apply simp +apply (subgoal_tac + "({s. (s : reachable v) = ((root,v) : REACHABLE) }) = + ({s. (s : reachable v) = ( (root,v) : REACHABLE) } Int + (- {} Un nmsg_eq 0 (v,w)))") +apply blast+ +done + +lemma Stable_final: "F : Stable final" +apply (case_tac "E={}") +prefer 2 apply (blast intro: Stable_final_E_NOT_empty) +apply (blast intro: Stable_final_E_empty) +done end diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Token.ML --- a/src/HOL/UNITY/Simple/Token.ML Thu Jan 23 10:30:14 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,101 +0,0 @@ -(* Title: HOL/UNITY/Token - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -The Token Ring. - -From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2. -*) - -val Token_defs = [HasTok_def, H_def, E_def, T_def]; - -Goalw [HasTok_def] "[| s: HasTok i; s: HasTok j |] ==> i=j"; -by Auto_tac; -qed "HasToK_partition"; - -Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)"; -by (Simp_tac 1); -by (case_tac "proc s i" 1); -by Auto_tac; -qed "not_E_eq"; - -Open_locale "Token"; - -val TR2 = thm "TR2"; -val TR3 = thm "TR3"; -val TR4 = thm "TR4"; -val TR5 = thm "TR5"; -val TR6 = thm "TR6"; -val TR7 = thm "TR7"; -val nodeOrder_def = thm "nodeOrder_def"; -val next_def = thm "next_def"; - -AddIffs [thm "N_positive"]; - -Goalw [stable_def] "F : stable (-(E i) Un (HasTok i))"; -by (rtac constrains_weaken 1); -by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1); -by (auto_tac (claset(), simpset() addsimps [not_E_eq])); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def]))); -qed "token_stable"; - - -(*** Progress under weak fairness ***) - -Goalw [nodeOrder_def] "wf(nodeOrder j)"; -by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1); -by (Blast_tac 1); -qed"wf_nodeOrder"; - -Goalw [nodeOrder_def, next_def, inv_image_def] - "[| i ((next i, i) : nodeOrder j) = (i ~= j)"; -by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq])); -by (auto_tac (claset(), - simpset() addsplits [nat_diff_split] - addsimps [linorder_neq_iff, mod_geq])); -qed "nodeOrder_eq"; - -(*From "A Logic for Concurrent Programming", but not used in Chapter 4. - Note the use of case_tac. Reasoning about leadsTo takes practice!*) -Goal "[| i \ -\ F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)"; -by (case_tac "i=j" 1); -by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); -by (rtac (TR7 RS leadsTo_weaken_R) 1); -by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq])); -qed "TR7_nodeOrder"; - - -(*Chapter 4 variant, the one actually used below.*) -Goal "[| i F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}"; -by (rtac (TR7 RS leadsTo_weaken_R) 1); -by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq])); -qed "TR7_aux"; - -Goal "({s. token s < N} Int token -` {m}) = (if m F : {s. token s < N} leadsTo (HasTok j)"; -by (rtac leadsTo_weaken_R 1); -by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")] - (wf_nodeOrder RS bounded_induct) 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff, - HasTok_def]))); -by (Blast_tac 2); -by (Clarify_tac 1); -by (rtac (TR7_aux RS leadsTo_weaken) 1); -by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_def])); -qed "leadsTo_j"; - -(*Misra's TR8: a hungry process eventually eats*) -Goal "j F : ({s. token s < N} Int H j) leadsTo (E j)"; -by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); -by (rtac TR6 2); -by (rtac ([leadsTo_j, TR3] MRS psp RS leadsTo_weaken) 1); -by (ALLGOALS Blast_tac); -qed "token_progress"; diff -r b9f6154427a4 -r e2fcd88be55d src/HOL/UNITY/Simple/Token.thy --- a/src/HOL/UNITY/Simple/Token.thy Thu Jan 23 10:30:14 2003 +0100 +++ b/src/HOL/UNITY/Simple/Token.thy Fri Jan 24 14:06:49 2003 +0100 @@ -9,58 +9,120 @@ *) -Token = WFair + +theory Token = WFair: (*process states*) datatype pstate = Hungry | Eating | Thinking record state = - token :: nat - proc :: nat => pstate + token :: "nat" + proc :: "nat => pstate" constdefs - HasTok :: nat => state set + HasTok :: "nat => state set" "HasTok i == {s. token s = i}" - H :: nat => state set + H :: "nat => state set" "H i == {s. proc s i = Hungry}" - E :: nat => state set + E :: "nat => state set" "E i == {s. proc s i = Eating}" - T :: nat => state set + T :: "nat => state set" "T i == {s. proc s i = Thinking}" locale Token = - fixes - N :: nat (*number of nodes in the ring*) - F :: state program - nodeOrder :: "nat => (nat*nat)set" - next :: nat => nat + fixes N and F and nodeOrder and "next" + defines nodeOrder_def: + "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int + (lessThan N <*> lessThan N)" + and next_def: + "next i == (Suc i) mod N" + assumes N_positive [iff]: "0 i=j" +by (unfold HasTok_def, auto) - assumes - N_positive "0 ((next i, i) : nodeOrder j) = (i ~= j)" +apply (unfold nodeOrder_def next_def inv_image_def) +apply (auto simp add: mod_Suc mod_geq) +apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq) +done - TR6 "F : (H i Int HasTok i) leadsTo (E i)" +(*From "A Logic for Concurrent Programming", but not used in Chapter 4. + Note the use of case_tac. Reasoning about leadsTo takes practice!*) +lemma (in Token) TR7_nodeOrder: + "[| i + F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)" +apply (case_tac "i=j") +apply (blast intro: subset_imp_leadsTo) +apply (rule TR7 [THEN leadsTo_weaken_R]) +apply (auto simp add: HasTok_def nodeOrder_eq) +done - TR7 "F : (HasTok i) leadsTo (HasTok (next i))" + +(*Chapter 4 variant, the one actually used below.*) +lemma (in Token) TR7_aux: "[| i F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}" +apply (rule TR7 [THEN leadsTo_weaken_R]) +apply (auto simp add: HasTok_def nodeOrder_eq) +done - defines - nodeOrder_def - "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int - (lessThan N <*> lessThan N)" +lemma (in Token) token_lemma: + "({s. token s < N} Int token -` {m}) = (if m F : {s. token s < N} leadsTo (HasTok j)" +apply (rule leadsTo_weaken_R) +apply (rule_tac I = "-{j}" and f = token and B = "{}" + in wf_nodeOrder [THEN bounded_induct]) +apply (simp_all (no_asm_simp) add: token_lemma vimage_Diff HasTok_def) + prefer 2 apply blast +apply clarify +apply (rule TR7_aux [THEN leadsTo_weaken]) +apply (auto simp add: HasTok_def nodeOrder_def) +done + +(*Misra's TR8: a hungry process eventually eats*) +lemma (in Token) token_progress: + "j F : ({s. token s < N} Int H j) leadsTo (E j)" +apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate]) +apply (rule_tac [2] TR6) +apply (rule psp [OF leadsTo_j TR3, THEN leadsTo_weaken], blast+) +done + end