author | Christian Sternagel |
Thu, 30 Aug 2012 15:44:03 +0900 | |
changeset 49093 | fdc301f592c4 |
parent 46008 | c296c75f4cf4 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/Simple/Deadlock.thy |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
3 |
Copyright 1998 University of Cambridge |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
4 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
5 |
Deadlock examples from section 5.6 of |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
6 |
Misra, "A Logic for Concurrent Programming", 1994 |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
7 |
*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
8 |
|
44871 | 9 |
theory Deadlock imports "../UNITY" begin |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
10 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
11 |
(*Trivial, two-process case*) |
13806 | 12 |
lemma "[| F \<in> (A \<inter> B) co A; F \<in> (B \<inter> A) co B |] ==> F \<in> stable (A \<inter> B)" |
44871 | 13 |
unfolding constrains_def stable_def by blast |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
14 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
15 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
16 |
(*a simplification step*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
17 |
lemma Collect_le_Int_equals: |
13806 | 18 |
"(\<Inter>i \<in> atMost n. A(Suc i) \<inter> A i) = (\<Inter>i \<in> atMost (Suc n). A i)" |
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
44871
diff
changeset
|
19 |
by (induct n) (auto simp add: atMost_Suc) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
20 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
21 |
(*Dual of the required property. Converse inclusion fails.*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
22 |
lemma UN_Int_Compl_subset: |
13806 | 23 |
"(\<Union>i \<in> lessThan n. A i) \<inter> (- A n) \<subseteq> |
24 |
(\<Union>i \<in> lessThan n. (A i) \<inter> (- A (Suc i)))" |
|
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
44871
diff
changeset
|
25 |
by (induct n) (auto simp: lessThan_Suc) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
26 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
27 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
28 |
(*Converse inclusion fails.*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
29 |
lemma INT_Un_Compl_subset: |
13806 | 30 |
"(\<Inter>i \<in> lessThan n. -A i \<union> A (Suc i)) \<subseteq> |
31 |
(\<Inter>i \<in> lessThan n. -A i) \<union> A n" |
|
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
44871
diff
changeset
|
32 |
by (induct n) (auto simp: lessThan_Suc) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
33 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
34 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
35 |
(*Specialized rewriting*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
36 |
lemma INT_le_equals_Int_lemma: |
13806 | 37 |
"A 0 \<inter> (-(A n) \<inter> (\<Inter>i \<in> lessThan n. -A i \<union> A (Suc i))) = {}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
38 |
by (blast intro: gr0I dest: INT_Un_Compl_subset [THEN subsetD]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
39 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
40 |
(*Reverse direction makes it harder to invoke the ind hyp*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
41 |
lemma INT_le_equals_Int: |
13806 | 42 |
"(\<Inter>i \<in> atMost n. A i) = |
43 |
A 0 \<inter> (\<Inter>i \<in> lessThan n. -A i \<union> A(Suc i))" |
|
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
44871
diff
changeset
|
44 |
by (induct n) |
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
44871
diff
changeset
|
45 |
(simp_all add: Int_ac Int_Un_distrib Int_Un_distrib2 |
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
44871
diff
changeset
|
46 |
INT_le_equals_Int_lemma lessThan_Suc atMost_Suc) |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
47 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
48 |
lemma INT_le_Suc_equals_Int: |
13806 | 49 |
"(\<Inter>i \<in> atMost (Suc n). A i) = |
50 |
A 0 \<inter> (\<Inter>i \<in> atMost n. -A i \<union> A(Suc i))" |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
51 |
by (simp add: lessThan_Suc_atMost INT_le_equals_Int) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
52 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
53 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
54 |
(*The final deadlock example*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
55 |
lemma |
13806 | 56 |
assumes zeroprem: "F \<in> (A 0 \<inter> A (Suc n)) co (A 0)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
57 |
and allprem: |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26824
diff
changeset
|
58 |
"!!i. i \<in> atMost n ==> F \<in> (A(Suc i) \<inter> A i) co (-A i \<union> A(Suc i))" |
13806 | 59 |
shows "F \<in> stable (\<Inter>i \<in> atMost (Suc n). A i)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
60 |
apply (unfold stable_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
61 |
apply (rule constrains_Int [THEN constrains_weaken]) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
62 |
apply (rule zeroprem) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
63 |
apply (rule constrains_INT) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
64 |
apply (erule allprem) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
65 |
apply (simp add: Collect_le_Int_equals Int_assoc INT_absorb) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
66 |
apply (simp add: INT_le_Suc_equals_Int) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
67 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
68 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
11195
diff
changeset
|
69 |
end |