--- 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 \
--- 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";
-
-
--- 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
--- 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";
--- 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";
--- 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
--- 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 <max (ftime t) (gtime t) *)
-Goal "mk_program \
-\ (UNIV, { {(t, Suc t) | 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();
-
-
-(*It remans to prove that they satisfy CMT3': t does not decrease,
- and that CMT3' implies that t stops changing once common(t) holds.*)
-
-
-(*** Progress under weak fairness ***)
-
-Addsimps [atMost_Int_atLeast];
-
-Goal "[| ALL m. F : {m} Co (maxfg m); \
-\ ALL m: lessThan n. F : {m} LeadsTo (greaterThan m); \
-\ n: common |] \
-\ ==> 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";
--- 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 <max (ftime t) (gtime t) *)
+lemma "mk_program
+ (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)
+ : {m} co (maxfg m)"
+by (simp add: constrains_def maxfg_def max_def gasc)
+
+
+(*It remans to prove that they satisfy CMT3': t does not decrease,
+ and that CMT3' implies that t stops changing once common(t) holds.*)
+
+
+(*** Progress under weak fairness ***)
+
+declare atMost_Int_atLeast [simp]
+
+lemma leadsTo_common_lemma:
+ "[| ALL m. F : {m} Co (maxfg m);
+ ALL m: lessThan n. F : {m} LeadsTo (greaterThan m);
+ n: common |]
+ ==> 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
--- 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();
-
--- 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
--- 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<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 (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<N \
-\ ==> 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<N ==> \
-\ 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<N ==> 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<N ==> 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";
--- 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<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 (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<N
+ ==> 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<N ==>
+ 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<N ==> 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<N ==> 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
--- 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";
--- 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
--- 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();
-
-
-
-
--- 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
--- 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";
--- 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
--- 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";
--- 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
--- 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<N; j<N |] ==> ((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<N; j<N |] ==> \
-\ 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<N; j<N; i~=j |] \
-\ ==> 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<N then token -` {m} else {})";
-by Auto_tac;
-val token_lemma = result();
-
-
-(*Misra's TR9: the token reaches an arbitrary node*)
-Goal "j<N ==> 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<N ==> 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";
--- 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<N"
+ and TR2: "F : (T i) co (T i Un H i)"
+ and TR3: "F : (H i) co (H i Un E i)"
+ and TR4: "F : (H i - HasTok i) co (H i)"
+ and TR5: "F : (HasTok i) co (HasTok i Un -(E i))"
+ and TR6: "F : (H i Int HasTok i) leadsTo (E i)"
+ and TR7: "F : (HasTok i) leadsTo (HasTok (next i))"
+
+
+lemma HasToK_partition: "[| s: HasTok i; s: HasTok j |] ==> i=j"
+by (unfold HasTok_def, auto)
- assumes
- N_positive "0<N"
+lemma not_E_eq: "(s ~: E i) = (s : H i | s : T i)"
+apply (simp add: H_def E_def T_def)
+apply (case_tac "proc s i", auto)
+done
- TR2 "F : (T i) co (T i Un H i)"
+lemma (in Token) token_stable: "F : stable (-(E i) Un (HasTok i))"
+apply (unfold stable_def)
+apply (rule constrains_weaken)
+apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
+apply (auto simp add: not_E_eq)
+apply (simp_all add: H_def E_def T_def)
+done
- TR3 "F : (H i) co (H i Un E i)"
+
+(*** Progress under weak fairness ***)
+
+lemma (in Token) wf_nodeOrder: "wf(nodeOrder j)"
+apply (unfold nodeOrder_def)
+apply (rule wf_less_than [THEN wf_inv_image, THEN wf_subset], blast)
+done
- TR4 "F : (H i - HasTok i) co (H i)"
-
- TR5 "F : (HasTok i) co (HasTok i Un -(E i))"
+lemma (in Token) nodeOrder_eq:
+ "[| i<N; j<N |] ==> ((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<N; j<N |] ==>
+ 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<N; j<N; i~=j |]
+ ==> 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<N then token -` {m} else {})"
+by auto
+
- next_def
- "next i == (Suc i) mod N"
+(*Misra's TR9: the token reaches an arbitrary node*)
+lemma (in Token) leadsTo_j: "j<N ==> 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<N ==> 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