--- a/src/HOL/UNITY/Simple/Channel.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Channel.thy Wed Feb 05 13:35:32 2003 +0100
@@ -17,19 +17,19 @@
constdefs
minSet :: "nat set => nat option"
- "minSet A == if A={} then None else Some (LEAST x. x:A)"
+ "minSet A == if A={} then None else Some (LEAST x. x \<in> A)"
axioms
- UC1: "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
+ UC1: "F \<in> (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
- (* UC1 "F : {s. minSet s = x} co {s. x <= minSet s}" *)
+ (* UC1 "F \<in> {s. minSet s = x} co {s. x \<subseteq> minSet s}" *)
- UC2: "F : (minSet -` {Some x}) leadsTo {s. x ~: s}"
+ UC2: "F \<in> (minSet -` {Some x}) leadsTo {s. x \<notin> s}"
(*None represents "infinity" while Some represents proper integers*)
-lemma minSet_eq_SomeD: "minSet A = Some x ==> x : A"
+lemma minSet_eq_SomeD: "minSet A = Some x ==> x \<in> A"
apply (unfold minSet_def)
apply (simp split: split_if_asm)
apply (fast intro: LeastI)
@@ -38,11 +38,11 @@
lemma minSet_empty [simp]: " minSet{} = None"
by (unfold minSet_def, simp)
-lemma minSet_nonempty: "x:A ==> minSet A = Some (LEAST x. x: A)"
+lemma minSet_nonempty: "x \<in> A ==> minSet A = Some (LEAST x. x \<in> A)"
by (unfold minSet_def, auto)
lemma minSet_greaterThan:
- "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))"
+ "F \<in> (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)
@@ -50,7 +50,7 @@
(*The induction*)
lemma Channel_progress_lemma:
- "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))"
+ "F \<in> (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)
@@ -63,7 +63,7 @@
done
-lemma Channel_progress: "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}"
+lemma Channel_progress: "!!y::nat. F \<in> (UNIV-{{}}) leadsTo {s. y \<notin> s}"
apply (rule Channel_progress_lemma [THEN leadsTo_weaken_R], clarify)
apply (frule minSet_nonempty)
apply (auto dest: Suc_le_lessD not_less_Least)
--- a/src/HOL/UNITY/Simple/Common.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Common.thy Wed Feb 05 13:35:32 2003 +0100
@@ -17,56 +17,56 @@
gtime :: "nat=>nat"
axioms
- fmono: "m <= n ==> ftime m <= ftime n"
- gmono: "m <= n ==> gtime m <= gtime n"
+ fmono: "m \<le> n ==> ftime m \<le> ftime n"
+ gmono: "m \<le> n ==> gtime m \<le> gtime n"
- fasc: "m <= ftime n"
- gasc: "m <= gtime n"
+ fasc: "m \<le> ftime n"
+ gasc: "m \<le> gtime n"
constdefs
common :: "nat set"
"common == {n. ftime n = n & gtime n = n}"
maxfg :: "nat => nat set"
- "maxfg m == {t. t <= max (ftime m) (gtime m)}"
+ "maxfg m == {t. t \<le> 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)
+ "[| \<forall>m. F \<in> {m} Co (maxfg m); n \<in> common |]
+ ==> F \<in> Stable (atMost n)"
+apply (drule_tac M = "{t. t \<le> 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)"
+ "[| Init F \<subseteq> atMost n;
+ \<forall>m. F \<in> {m} Co (maxfg m); n \<in> common |]
+ ==> F \<in> Always (atMost n)"
by (simp add: AlwaysI common_stable)
(*** Some programs that implement the safety property above ***)
-lemma "SKIP : {m} co (maxfg m)"
+lemma "SKIP \<in> {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)"
+ \<in> {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)"
+ \<in> {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)"
+ \<in> {m} co (maxfg m)"
by (simp add: constrains_def maxfg_def max_def gasc)
@@ -79,10 +79,10 @@
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"
+ "[| \<forall>m. F \<in> {m} Co (maxfg m);
+ \<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m);
+ n \<in> common |]
+ ==> F \<in> (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))
@@ -90,12 +90,12 @@
apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
done
-(*The "ALL m: -common" form echoes CMT6.*)
+(*The "\<forall>m \<in> -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"
+ "[| \<forall>m. F \<in> {m} Co (maxfg m);
+ \<forall>m \<in> -common. F \<in> {m} LeadsTo (greaterThan m);
+ n \<in> common |]
+ ==> F \<in> (atMost (LEAST n. n \<in> common)) LeadsTo common"
apply (rule leadsTo_common_lemma)
apply (simp_all (no_asm_simp))
apply (erule_tac [2] LeastI)
--- a/src/HOL/UNITY/Simple/Deadlock.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Deadlock.thy Wed Feb 05 13:35:32 2003 +0100
@@ -10,66 +10,61 @@
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)"
+lemma "[| F \<in> (A \<inter> B) co A; F \<in> (B \<inter> A) co B |] ==> F \<in> stable (A \<inter> 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)"
+ "(\<Inter>i \<in> atMost n. A(Suc i) \<inter> A i) = (\<Inter>i \<in> atMost (Suc n). A i)"
apply (induct_tac "n")
-apply (simp_all (no_asm_simp) add: atMost_Suc)
-apply auto
+apply (auto simp add: atMost_Suc)
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
+ "(\<Union>i \<in> lessThan n. A i) \<inter> (- A n) \<subseteq>
+ (\<Union>i \<in> lessThan n. (A i) \<inter> (- A (Suc i)))"
+apply (induct_tac "n", simp)
+apply (simp add: lessThan_Suc, 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
+ "(\<Inter>i \<in> lessThan n. -A i \<union> A (Suc i)) \<subseteq>
+ (\<Inter>i \<in> lessThan n. -A i) \<union> A n"
+apply (induct_tac "n", simp)
+apply (simp add: lessThan_Suc, 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))) = {}"
+ "A 0 \<inter> (-(A n) \<inter> (\<Inter>i \<in> lessThan n. -A i \<union> 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))"
+ "(\<Inter>i \<in> atMost n. A i) =
+ A 0 \<inter> (\<Inter>i \<in> lessThan n. -A i \<union> 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))"
+ "(\<Inter>i \<in> atMost (Suc n). A i) =
+ A 0 \<inter> (\<Inter>i \<in> atMost n. -A i \<union> 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)"
+ assumes zeroprem: "F \<in> (A 0 \<inter> 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)"
+ "!!i. i \<in> atMost n ==> F \<in> (A(Suc i) \<inter> A i) co (-A i \<union> A(Suc i))"
+ shows "F \<in> stable (\<Inter>i \<in> atMost (Suc n). A i)"
apply (unfold stable_def)
apply (rule constrains_Int [THEN constrains_weaken])
apply (rule zeroprem)
--- a/src/HOL/UNITY/Simple/Lift.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Lift.thy Wed Feb 05 13:35:32 2003 +0100
@@ -21,26 +21,26 @@
Max :: "int" (*least and greatest floors*)
axioms
- Min_le_Max [iff]: "Min <= Max"
+ Min_le_Max [iff]: "Min \<le> Max"
constdefs
(** Abbreviations: the "always" part **)
above :: "state set"
- "above == {s. EX i. floor s < i & i <= Max & i : req s}"
+ "above == {s. \<exists>i. floor s < i & i \<le> Max & i \<in> req s}"
below :: "state set"
- "below == {s. EX i. Min <= i & i < floor s & i : req s}"
+ "below == {s. \<exists>i. Min \<le> i & i < floor s & i \<in> req s}"
queueing :: "state set"
- "queueing == above Un below"
+ "queueing == above \<union> below"
goingup :: "state set"
- "goingup == above Int ({s. up s} Un -below)"
+ "goingup == above \<inter> ({s. up s} \<union> -below)"
goingdown :: "state set"
- "goingdown == below Int ({s. ~ up s} Un -above)"
+ "goingdown == below \<inter> ({s. ~ up s} \<union> -above)"
ready :: "state set"
"ready == {s. stop s & ~ open s & move s}"
@@ -63,7 +63,7 @@
"atFloor n == {s. floor s = n}"
Req :: "int => state set"
- "Req n == {s. n : req s}"
+ "Req n == {s. n \<in> req s}"
@@ -71,15 +71,15 @@
request_act :: "(state*state) set"
"request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
- & ~ stop s & floor s : req s}"
+ & ~ stop s & floor s \<in> req s}"
open_act :: "(state*state) set"
"open_act ==
{(s,s'). s' = s (|open :=True,
req := req s - {floor s},
move := True|)
- & stop s & ~ open s & floor s : req s
- & ~(move s & s: queueing)}"
+ & stop s & ~ open s & floor s \<in> req s
+ & ~(move s & s \<in> queueing)}"
close_act :: "(state*state) set"
"close_act == {(s,s'). s' = s (|open := False|) & open s}"
@@ -89,24 +89,24 @@
{(s,s'). s' = s (|stop :=False,
floor := floor s + 1,
up := True|)
- & s : (ready Int goingup)}"
+ & s \<in> (ready \<inter> goingup)}"
req_down :: "(state*state) set"
"req_down ==
{(s,s'). s' = s (|stop :=False,
floor := floor s - 1,
up := False|)
- & s : (ready Int goingdown)}"
+ & s \<in> (ready \<inter> goingdown)}"
move_up :: "(state*state) set"
"move_up ==
{(s,s'). s' = s (|floor := floor s + 1|)
- & ~ stop s & up s & floor s ~: req s}"
+ & ~ stop s & up s & floor s \<notin> req s}"
move_down :: "(state*state) set"
"move_down ==
{(s,s'). s' = s (|floor := floor s - 1|)
- & ~ stop s & ~ up s & floor s ~: req s}"
+ & ~ stop s & ~ up s & floor s \<notin> req s}"
(*This action is omitted from prior treatments, which therefore are
unrealistic: nobody asks the lift to do anything! But adding this
@@ -114,8 +114,8 @@
"ensures" properties fail.*)
button_press :: "(state*state) set"
"button_press ==
- {(s,s'). EX n. s' = s (|req := insert n (req s)|)
- & Min <= n & n <= Max}"
+ {(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
+ & Min \<le> n & n \<le> Max}"
Lift :: "state program"
@@ -130,7 +130,7 @@
(** Invariants **)
bounded :: "state set"
- "bounded == {s. Min <= floor s & floor s <= Max}"
+ "bounded == {s. Min \<le> floor s & floor s \<le> Max}"
open_stop :: "state set"
"open_stop == {s. open s --> stop s}"
@@ -139,15 +139,15 @@
"open_move == {s. open s --> move s}"
stop_floor :: "state set"
- "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
+ "stop_floor == {s. stop s & ~ move s --> floor s \<in> req s}"
moving_up :: "state set"
"moving_up == {s. ~ stop s & up s -->
- (EX f. floor s <= f & f <= Max & f : req s)}"
+ (\<exists>f. floor s \<le> f & f \<le> Max & f \<in> req s)}"
moving_down :: "state set"
"moving_down == {s. ~ stop s & ~ up s -->
- (EX f. Min <= f & f <= floor s & f : req s)}"
+ (\<exists>f. Min \<le> f & f \<le> floor s & f \<in> req s)}"
metric :: "[int,state] => int"
"metric ==
@@ -160,10 +160,10 @@
locale Floor =
fixes n
- assumes Min_le_n [iff]: "Min <= n"
- and n_le_Max [iff]: "n <= Max"
+ assumes Min_le_n [iff]: "Min \<le> n"
+ and n_le_Max [iff]: "n \<le> Max"
-lemma not_mem_distinct: "[| x ~: A; y : A |] ==> x ~= y"
+lemma not_mem_distinct: "[| x \<notin> A; y \<in> A |] ==> x \<noteq> y"
by blast
@@ -194,36 +194,36 @@
moving_up_def [simp]
moving_down_def [simp]
-lemma open_stop: "Lift : Always open_stop"
+lemma open_stop: "Lift \<in> Always open_stop"
apply (rule AlwaysI, force)
apply (unfold Lift_def, constrains)
done
-lemma stop_floor: "Lift : Always stop_floor"
+lemma stop_floor: "Lift \<in> 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"
+lemma open_move: "Lift \<in> 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"
+lemma moving_up: "Lift \<in> 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"
+lemma moving_down: "Lift \<in> 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"
+lemma bounded: "Lift \<in> Always bounded"
apply (cut_tac moving_up moving_down)
apply (rule AlwaysI, force)
apply (unfold Lift_def, constrains, auto)
@@ -244,24 +244,24 @@
(** 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)"
+lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> 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)"
+lemma E_thm02: "Lift \<in> (Req n \<inter> stopped - atFloor n) LeadsTo
+ (Req n \<inter> 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))"
+lemma E_thm03: "Lift \<in> (Req n \<inter> opened - atFloor n) LeadsTo
+ (Req n \<inter> 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)"
+lemma E_thm04: "Lift \<in> (Req n \<inter> closed \<inter> (atFloor n - queueing))
+ LeadsTo (opened \<inter> atFloor n)"
apply (unfold Lift_def, ensures_tac "open_act")
done (*lem_lift_1_7*)
@@ -283,14 +283,14 @@
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))"
+ "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))
+ LeadsTo ((closed \<inter> goingup \<inter> Req n) \<union>
+ (closed \<inter> goingdown \<inter> 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)"
+lemma (in Floor) lift_2: "Lift \<in> (Req n \<inter> closed - (atFloor n - queueing))
+ LeadsTo (moving \<inter> Req n)"
apply (rule LeadsTo_Trans [OF E_thm05c LeadsTo_Un])
apply (unfold Lift_def)
apply (ensures_tac [2] "req_down")
@@ -306,13 +306,13 @@
(*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})
+ Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter>
+ {s. floor s \<notin> req s} \<inter> {s. up s})
LeadsTo
- (moving Int Req n Int {s. metric n s < N})"
+ (moving \<inter> Req n \<inter> {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*)
+(*this step consolidates two formulae to the goal metric n s' \<le> metric n s*)
apply (erule linorder_leI [THEN order_antisym, symmetric])
apply (auto simp add: metric_def)
done
@@ -320,21 +320,21 @@
(*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})"
+ Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter>
+ {s. floor s \<notin> req s} - {s. up s})
+ LeadsTo (moving \<inter> Req n \<inter> {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*)
+(*this step consolidates two formulae to the goal metric n s' \<le> 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})"
+ "0<N ==> Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter>
+ {s. floor s \<notin> req s}) LeadsTo
+ (moving \<inter> Req n \<inter> {s. metric n s < N})"
apply (rule LeadsTo_Trans [OF subset_imp_LeadsTo
LeadsTo_Un [OF E_thm12a E_thm12b]], auto)
done
@@ -344,8 +344,8 @@
(*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})"
+ ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingup) LeadsTo
+ (moving \<inter> Req n \<inter> {s. metric n s < N})"
apply (cut_tac bounded)
apply (unfold Lift_def, ensures_tac "req_up")
apply (auto simp add: metric_def)
@@ -354,8 +354,8 @@
(*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})"
+ Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N} \<inter> goingdown) LeadsTo
+ (moving \<inter> Req n \<inter> {s. metric n s < N})"
apply (cut_tac bounded)
apply (unfold Lift_def, ensures_tac "req_down")
apply (auto simp add: metric_def)
@@ -365,14 +365,14 @@
(*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"
+ "0<N ==> Req n \<inter> {s. metric n s = N} \<subseteq> goingup \<union> 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})"
+ "0<N ==> Lift \<in> (closed \<inter> Req n \<inter> {s. metric n s = N}) LeadsTo
+ (moving \<inter> Req n \<inter> {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)
@@ -383,37 +383,37 @@
(*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"
+ "[| metric n s = 0; Min \<le> floor s; floor s \<le> 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)"
+lemma (in Floor) E_thm11: "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = 0}) LeadsTo
+ (stopped \<inter> 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})"
+ "Lift \<in> (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})
+ LeadsTo (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> 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})"
+ Lift \<in>
+ (stopped \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})
+ LeadsTo (opened \<inter> Req n \<inter> {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})"
+lemma (in Floor) E_thm15: "Lift \<in> (opened \<inter> Req n \<inter> {s. metric n s = N})
+ LeadsTo (closed \<inter> Req n \<inter> {s. metric n s = N})"
apply (unfold Lift_def, ensures_tac "close_act")
apply (auto simp add: metric_def)
done
@@ -422,15 +422,15 @@
(** 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})"
+ Lift \<in>
+ (moving \<inter> Req n \<inter> {s. metric n s = N} \<inter> {s. floor s \<in> req s})
+ LeadsTo (moving \<inter> Req n \<inter> {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}"
+lemma (in Floor) Always_nonneg: "Lift \<in> Always {s. 0 \<le> metric n s}"
apply (rule bounded [THEN Always_weaken])
apply (auto simp add: metric_def)
done
@@ -438,10 +438,10 @@
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)"
+ "Lift \<in> (moving \<inter> Req n) LeadsTo (stopped \<inter> atFloor n)"
apply (rule Always_nonneg [THEN integ_0_le_induct])
apply (case_tac "0 < z")
-(*If z <= 0 then actually z = 0*)
+(*If z \<le> 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
@@ -449,7 +449,7 @@
done
-lemma (in Floor) lift_1: "Lift : (Req n) LeadsTo (opened Int atFloor n)"
+lemma (in Floor) lift_1: "Lift \<in> (Req n) LeadsTo (opened \<inter> atFloor n)"
apply (rule LeadsTo_Trans)
prefer 2
apply (rule LeadsTo_Un [OF E_thm04 LeadsTo_Un_post])
--- a/src/HOL/UNITY/Simple/Mutex.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Mutex.thy Wed Feb 05 13:35:32 2003 +0100
@@ -62,16 +62,16 @@
(** The correct invariants **)
IU :: "state set"
- "IU == {s. (u s = (1 <= m s & m s <= 3)) & (m s = 3 --> ~ p s)}"
+ "IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) & (m s = 3 --> ~ p s)}"
IV :: "state set"
- "IV == {s. (v s = (1 <= n s & n s <= 3)) & (n s = 3 --> p s)}"
+ "IV == {s. (v s = (1 \<le> n s & n s \<le> 3)) & (n s = 3 --> p s)}"
(** The faulty invariant (for U alone) **)
bad_IU :: "state set"
- "bad_IU == {s. (u s = (1 <= m s & m s <= 3)) &
- (3 <= m s & m s <= 4 --> ~ p s)}"
+ "bad_IU == {s. (u s = (1 \<le> m s & m s \<le> 3)) &
+ (3 \<le> m s & m s \<le> 4 --> ~ p s)}"
declare Mutex_def [THEN def_prg_Init, simp]
@@ -91,26 +91,26 @@
declare IV_def [THEN def_set_simp, simp]
declare bad_IU_def [THEN def_set_simp, simp]
-lemma IU: "Mutex : Always IU"
+lemma IU: "Mutex \<in> Always IU"
apply (rule AlwaysI, force)
apply (unfold Mutex_def, constrains)
done
-lemma IV: "Mutex : Always IV"
+lemma IV: "Mutex \<in> 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)}"
+lemma mutual_exclusion: "Mutex \<in> 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"
+lemma "Mutex \<in> Always bad_IU"
apply (rule AlwaysI, force)
apply (unfold Mutex_def, constrains, auto)
(*Resulting state: n=1, p=false, m=4, u=false.
@@ -119,90 +119,90 @@
oops
-lemma eq_123: "((1::int) <= i & i <= 3) = (i = 1 | i = 2 | i = 3)"
+lemma eq_123: "((1::int) \<le> i & i \<le> 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}"
+lemma U_F0: "Mutex \<in> {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_F1: "Mutex \<in> {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}"
+lemma U_F2: "Mutex \<in> {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}"
+lemma U_F3: "Mutex \<in> {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}"
+lemma U_lemma2: "Mutex \<in> {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}"
+lemma U_lemma1: "Mutex \<in> {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}"
+lemma U_lemma123: "Mutex \<in> {s. 1 \<le> m s & m s \<le> 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}"
+lemma u_Leadsto_p: "Mutex \<in> {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}"
+lemma V_F0: "Mutex \<in> {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}"
+lemma V_F1: "Mutex \<in> {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}"
+lemma V_F2: "Mutex \<in> {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}"
+lemma V_F3: "Mutex \<in> {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}"
+lemma V_lemma2: "Mutex \<in> {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}"
+lemma V_lemma1: "Mutex \<in> {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}"
+lemma V_lemma123: "Mutex \<in> {s. 1 \<le> n s & n s \<le> 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}"
+lemma v_Leadsto_not_p: "Mutex \<in> {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}"
+lemma m1_Leadsto_3: "Mutex \<in> {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)
@@ -213,7 +213,7 @@
done
(*The same for V*)
-lemma n1_Leadsto_3: "Mutex : {s. n s = 1} LeadsTo {s. n s = 3}"
+lemma n1_Leadsto_3: "Mutex \<in> {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)
--- a/src/HOL/UNITY/Simple/Network.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Network.thy Wed Feb 05 13:35:32 2003 +0100
@@ -20,13 +20,13 @@
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}
+ assumes rsA: "F \<in> stable {s. s(Bproc,Rcvd) \<le> s(Aproc,Sent)}"
+ and rsB: "F \<in> stable {s. s(Aproc,Rcvd) \<le> s(Bproc,Sent)}"
+ and sent_nondec: "F \<in> stable {s. m \<le> s(proc,Sent)}"
+ and rcvd_nondec: "F \<in> stable {s. n \<le> s(proc,Rcvd)}"
+ and rcvd_idle: "F \<in> {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}
+ and sent_idle: "F \<in> {s. s(proc,Idle) = Suc 0 & s(proc,Sent) = n}
co {s. s(proc,Sent) = n}"
@@ -51,7 +51,7 @@
idle_AB]
lemma (in F_props)
- shows "F : stable {s. s(Aproc,Idle) = Suc 0 & s(Bproc,Idle) = Suc 0 &
+ shows "F \<in> 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}"
@@ -60,7 +60,7 @@
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 (blast del: le0, clarify)
apply (subgoal_tac "s' (Aproc, Rcvd) = s (Aproc, Rcvd)")
apply (subgoal_tac "s' (Bproc, Rcvd) = s (Bproc, Rcvd)")
apply simp
--- a/src/HOL/UNITY/Simple/Reach.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Reach.thy Wed Feb 05 13:35:32 2003 +0100
@@ -24,13 +24,13 @@
"asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
Rprg :: "state program"
- "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)"
+ "Rprg == mk_program ({%v. v=init}, \<Union>(u,v)\<in>edges. {asgt u v}, UNIV)"
reach_invariant :: "state set"
- "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
+ "reach_invariant == {s. (\<forall>v. s v --> (init, v) \<in> edges^*) & s init}"
fixedpoint :: "state set"
- "fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
+ "fixedpoint == {s. \<forall>(u,v)\<in>edges. s u --> s v}"
metric :: "state => nat"
"metric s == card {v. ~ s v}"
@@ -60,7 +60,7 @@
declare reach_invariant_def [THEN def_set_simp, simp]
-lemma reach_invariant: "Rprg : Always reach_invariant"
+lemma reach_invariant: "Rprg \<in> Always reach_invariant"
apply (rule AlwaysI, force)
apply (unfold Rprg_def, constrains)
apply (blast intro: rtrancl_trans)
@@ -71,7 +71,7 @@
(*If it reaches a fixedpoint, it has found a solution*)
lemma fixedpoint_invariant_correct:
- "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }"
+ "fixedpoint \<inter> reach_invariant = { %v. (init, v) \<in> edges^* }"
apply (unfold fixedpoint_def)
apply (rule equalityI)
apply (auto intro!: ext)
@@ -80,7 +80,7 @@
done
lemma lemma1:
- "FP Rprg <= fixedpoint"
+ "FP Rprg \<subseteq> 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)
@@ -88,7 +88,7 @@
done
lemma lemma2:
- "fixedpoint <= FP Rprg"
+ "fixedpoint \<subseteq> FP Rprg"
apply (unfold FP_def fixedpoint_def stable_def constrains_def Rprg_def)
apply (auto intro!: ext)
done
@@ -103,16 +103,15 @@
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)
+lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
+apply (auto simp add: Compl_FP UN_UN_flatten FP_fixedpoint [symmetric] Rprg_def)
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
+ "A - fixedpoint = (\<Union>(u,v)\<in>edges. A \<inter> {s. s u & ~ s v})"
+by (simp add: Diff_eq Compl_fixedpoint, blast)
(*** Progress ***)
@@ -127,13 +126,13 @@
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"
+lemma metric_le: "metric (s(y:=s x | s y)) \<le> 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))"
+ "Rprg \<in> ((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")
@@ -144,19 +143,19 @@
done
lemma LeadsTo_Un_fixedpoint:
- "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)"
+ "Rprg \<in> (metric-`{m}) LeadsTo (metric-`(lessThan m) \<union> 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"
+lemma LeadsTo_fixedpoint: "Rprg \<in> UNIV LeadsTo fixedpoint"
apply (rule LessThan_induct, auto)
apply (rule LeadsTo_Un_fixedpoint)
done
-lemma LeadsTo_correct: "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }"
+lemma LeadsTo_correct: "Rprg \<in> UNIV LeadsTo { %v. (init, v) \<in> edges^* }"
apply (subst fixedpoint_invariant_correct [symmetric])
apply (rule Always_LeadsTo_weaken [OF reach_invariant LeadsTo_fixedpoint], auto)
done
--- a/src/HOL/UNITY/Simple/Reachability.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy Wed Feb 05 13:35:32 2003 +0100
@@ -23,8 +23,8 @@
inductive "REACHABLE"
intros
- base: "v : V ==> ((v,v) : REACHABLE)"
- step: "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)"
+ base: "v \<in> V ==> ((v,v) \<in> REACHABLE)"
+ step: "((u,v) \<in> REACHABLE) & (v,w) \<in> E ==> ((u,w) \<in> REACHABLE)"
constdefs
reachable :: "vertex => state set"
@@ -37,65 +37,64 @@
"nmsg_gt k == %e. {s. k < nmsg s e}"
nmsg_gte :: "nat => edge => state set"
- "nmsg_gte k == %e. {s. k <= nmsg s e}"
+ "nmsg_gte k == %e. {s. k \<le> nmsg s e}"
nmsg_lte :: "nat => edge => state set"
- "nmsg_lte k == %e. {s. nmsg s e <= k}"
-
-
+ "nmsg_lte k == %e. {s. nmsg s e \<le> k}"
final :: "state set"
- "final == (INTER V (%v. reachable v <==> {s. (root, v) : REACHABLE})) Int (INTER E (nmsg_eq 0))"
+ "final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter>
+ (INTER E (nmsg_eq 0))"
axioms
- Graph1: "root : V"
+ Graph1: "root \<in> V"
- Graph2: "(v,w) : E ==> (v : V) & (w : V)"
+ Graph2: "(v,w) \<in> E ==> (v \<in> V) & (w \<in> V)"
- MA1: "F : Always (reachable root)"
+ MA1: "F \<in> Always (reachable root)"
- MA2: "v: V ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})"
+ MA2: "v \<in> V ==> F \<in> Always (- reachable v \<union> {s. ((root,v) \<in> REACHABLE)})"
- MA3: "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))"
+ MA3: "[|v \<in> V;w \<in> V|] ==> F \<in> Always (-(nmsg_gt 0 (v,w)) \<union> (reachable v))"
- MA4: "(v,w) : E ==>
- F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
+ MA4: "(v,w) \<in> E ==>
+ F \<in> Always (-(reachable v) \<union> (nmsg_gt 0 (v,w)) \<union> (reachable w))"
- MA5: "[|v:V; w:V|]
- ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte (Suc 0) (v,w))"
+ MA5: "[|v \<in> V; w \<in> V|]
+ ==> F \<in> Always (nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w))"
- MA6: "[|v:V|] ==> F : Stable (reachable v)"
+ MA6: "[|v \<in> V|] ==> F \<in> Stable (reachable v)"
- MA6b: "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))"
+ MA6b: "[|v \<in> V;w \<in> W|] ==> F \<in> Stable (reachable v \<inter> nmsg_lte k (v,w))"
- MA7: "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)"
+ MA7: "[|v \<in> V;w \<in> V|] ==> F \<in> 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"
+ "(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> 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"
+lemma Induction_base: "(v,w) \<in> E ==> F \<in> 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"
+ "(v,w) \<in> REACHABLE ==> F \<in> 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"
+lemma Detects_part1: "F \<in> {s. (root,v) \<in> REACHABLE} LeadsTo reachable v"
apply (rule single_LeadsTo_I)
apply (simp split add: split_if_asm)
apply (rule MA1 [THEN Always_LeadsToI])
@@ -104,7 +103,7 @@
lemma Reachability_Detected:
- "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}"
+ "v \<in> V ==> F \<in> (reachable v) Detects {s. (root,v) \<in> REACHABLE}"
apply (unfold Detects_def, auto)
prefer 2 apply (blast intro: MA2 [THEN Always_weaken])
apply (rule Detects_part1 [THEN LeadsTo_weaken_L], blast)
@@ -112,7 +111,7 @@
lemma LeadsTo_Reachability:
- "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})"
+ "v \<in> V ==> F \<in> UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE})"
by (erule Reachability_Detected [THEN Detects_Imp_LeadstoEQ])
@@ -121,17 +120,15 @@
(* 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
+ "(reachable v <==> {s. (root,v) \<in> REACHABLE}) =
+ {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}"
+by (unfold Equality_def, blast)
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
+ "(reachable v <==> (if (root,v) \<in> REACHABLE then UNIV else {})) =
+ {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}"
+by (unfold Equality_def, auto)
(* ------------------------------------ *)
@@ -139,37 +136,37 @@
(* 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"
+ "(\<Inter>v \<in> V. \<Inter>w \<in> V. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE)) &
+ s \<in> nmsg_eq 0 (v,w)})
+ \<subseteq> 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"
+ "E\<noteq>{}
+ ==> (\<Inter>v \<in> V. \<Inter>e \<in> E. {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))}
+ \<inter> nmsg_eq 0 e) \<subseteq> 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"
+ "E\<noteq>{}
+ ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.
+ (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e)
+ \<subseteq> final"
apply (frule final_lemma2)
apply (simp (no_asm_use) add: Eq_lemma2)
done
lemma final_lemma4:
- "E~={}
- ==> (INT v: V. INT e: E.
- {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e)
+ "E\<noteq>{}
+ ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.
+ {s. ((s \<in> reachable v) = ((root,v) \<in> REACHABLE))} \<inter> nmsg_eq 0 e)
= final"
apply (rule subset_antisym)
apply (erule final_lemma2)
@@ -177,9 +174,9 @@
done
lemma final_lemma5:
- "E~={}
- ==> (INT v: V. INT e: E.
- ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e)
+ "E\<noteq>{}
+ ==> (\<Inter>v \<in> V. \<Inter>e \<in> E.
+ ((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 e)
= final"
apply (frule final_lemma4)
apply (simp (no_asm_use) add: Eq_lemma2)
@@ -187,9 +184,9 @@
lemma final_lemma6:
- "(INT v: V. INT w: V.
- (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w))
- <= final"
+ "(\<Inter>v \<in> V. \<Inter>w \<in> V.
+ (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter> nmsg_eq 0 (v,w))
+ \<subseteq> final"
apply (simp (no_asm) add: Eq_lemma2 Int_def)
apply (rule final_lemma1)
done
@@ -197,9 +194,9 @@
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))))"
+ (\<Inter>v \<in> V. \<Inter>w \<in> V.
+ ((reachable v) <==> {s. (root,v) \<in> REACHABLE}) \<inter>
+ (-{s. (v,w) \<in> E} \<union> (nmsg_eq 0 (v,w))))"
apply (unfold final_def)
apply (rule subset_antisym, blast)
apply (auto split add: split_if_asm)
@@ -213,56 +210,55 @@
(* Stability theorems *)
lemma not_REACHABLE_imp_Stable_not_reachable:
- "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)"
+ "[| v \<in> V; (root,v) \<notin> REACHABLE |] ==> F \<in> 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})"
+ "v \<in> V ==> F \<in> Stable (reachable v <==> {s. (root,v) \<in> 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)"
+ "((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter>
+ (- nmsg_gt 0 (v,w) \<union> A))
+ \<subseteq> A \<union> 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
+ "reachable v \<inter> nmsg_eq 0 (v,w) =
+ ((nmsg_gte 0 (v,w) \<inter> nmsg_lte (Suc 0) (v,w)) \<inter>
+ (reachable v \<inter> nmsg_lte 0 (v,w)))"
+by (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
lemma lemma6:
- "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v"
+ "- nmsg_gt 0 (v,w) \<union> reachable v \<subseteq> nmsg_eq 0 (v,w) \<union> reachable v"
apply (unfold nmsg_gte_def nmsg_lte_def nmsg_gt_def nmsg_eq_def, auto)
done
lemma Always_reachable_OR_nmsg_0:
- "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))"
+ "[|v \<in> V; w \<in> V|] ==> F \<in> Always (reachable v \<union> 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))"
+ "[|v \<in> V; w \<in> V|] ==> F \<in> Stable (reachable v \<inter> 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)"
+ "[|v \<in> V; w \<in> V|] ==> F \<in> Stable (nmsg_eq 0 (v,w) \<union> reachable v)"
by (blast intro!: Always_weaken [THEN Always_imp_Stable] lemma6 MA3)
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))"
+ "[| v \<in> V; w \<in> V; (root,v) \<notin> REACHABLE |]
+ ==> F \<in> Stable (- reachable v \<inter> nmsg_eq 0 (v,w))"
apply (rule Stable_Int [OF MA2 [THEN Always_imp_Stable]
Stable_nmsg_0_OR_reachable,
THEN Stable_eq])
@@ -271,8 +267,8 @@
done
lemma Stable_reachable_EQ_R_AND_nmsg_0:
- "[| v : V; w:V |]
- ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int
+ "[| v \<in> V; w \<in> V |]
+ ==> F \<in> Stable ((reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter>
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)
@@ -284,13 +280,13 @@
(* LeadsTo final predicate (Exercise 11.2 page 274) *)
-lemma UNIV_lemma: "UNIV <= (INT v: V. UNIV)"
+lemma UNIV_lemma: "UNIV \<subseteq> (\<Inter>v \<in> V. UNIV)"
by blast
lemmas UNIV_LeadsTo_completion =
LeadsTo_weaken_L [OF Finite_stable_completion UNIV_lemma]
-lemma LeadsTo_final_E_empty: "E={} ==> F : UNIV LeadsTo final"
+lemma LeadsTo_final_E_empty: "E={} ==> F \<in> UNIV LeadsTo final"
apply (unfold final_def, simp)
apply (rule UNIV_LeadsTo_completion)
apply safe
@@ -300,13 +296,13 @@
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))"
+ "[| v \<in> V; w \<in> V |]
+ ==> F \<in> UNIV LeadsTo
+ ((reachable v <==> {s. (root,v): REACHABLE}) \<inter> 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
+ "F \<in> (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter>
+ UNIV LeadsTo (reachable v <==> {s. (root,v) \<in> REACHABLE}) \<inter>
nmsg_eq 0 (v,w) ")
apply simp
apply (rule PSP_Stable2)
@@ -314,7 +310,7 @@
apply (rule_tac [3] Stable_reachable_EQ_R, auto)
done
-lemma LeadsTo_final_E_NOT_empty: "E~={} ==> F : UNIV LeadsTo final"
+lemma LeadsTo_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> 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)
@@ -324,9 +320,9 @@
Leadsto_reachability_AND_nmsg_0)+
done
-lemma LeadsTo_final: "F : UNIV LeadsTo final"
+lemma LeadsTo_final: "F \<in> UNIV LeadsTo final"
apply (case_tac "E={}")
-apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
+ apply (rule_tac [2] LeadsTo_final_E_NOT_empty)
apply (rule LeadsTo_final_E_empty, auto)
done
@@ -334,21 +330,23 @@
(* Stability of final (Exercise 11.2 page 274) *)
-lemma Stable_final_E_empty: "E={} ==> F : Stable final"
+lemma Stable_final_E_empty: "E={} ==> F \<in> Stable final"
apply (unfold final_def, simp)
apply (rule Stable_INT)
apply (drule Stable_reachable_EQ_R, simp)
done
-lemma Stable_final_E_NOT_empty: "E~={} ==> F : Stable final"
+lemma Stable_final_E_NOT_empty: "E\<noteq>{} ==> F \<in> 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))) ")
+apply (subgoal_tac [2]
+ "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) } \<inter> nmsg_eq 0 (v,w)) =
+ ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } \<inter> (- UNIV \<union> nmsg_eq 0 (v,w)))")
prefer 2 apply blast
prefer 2 apply blast
apply (rule Stable_reachable_EQ_R_AND_nmsg_0
@@ -358,15 +356,15 @@
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)))")
+ "({s. (s \<in> reachable v) = ((root,v) \<in> REACHABLE) }) =
+ ({s. (s \<in> reachable v) = ( (root,v) \<in> REACHABLE) } Int
+ (- {} \<union> nmsg_eq 0 (v,w)))")
apply blast+
done
-lemma Stable_final: "F : Stable final"
+lemma Stable_final: "F \<in> Stable final"
apply (case_tac "E={}")
-prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
+ prefer 2 apply (blast intro: Stable_final_E_NOT_empty)
apply (blast intro: Stable_final_E_empty)
done
--- a/src/HOL/UNITY/Simple/Token.thy Tue Feb 04 18:12:40 2003 +0100
+++ b/src/HOL/UNITY/Simple/Token.thy Wed Feb 05 13:35:32 2003 +0100
@@ -41,23 +41,23 @@
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))"
+ and TR2: "F \<in> (T i) co (T i \<union> H i)"
+ and TR3: "F \<in> (H i) co (H i \<union> E i)"
+ and TR4: "F \<in> (H i - HasTok i) co (H i)"
+ and TR5: "F \<in> (HasTok i) co (HasTok i \<union> -(E i))"
+ and TR6: "F \<in> (H i \<inter> HasTok i) leadsTo (E i)"
+ and TR7: "F \<in> (HasTok i) leadsTo (HasTok (next i))"
-lemma HasToK_partition: "[| s: HasTok i; s: HasTok j |] ==> i=j"
+lemma HasToK_partition: "[| s \<in> HasTok i; s \<in> HasTok j |] ==> i=j"
by (unfold HasTok_def, auto)
-lemma not_E_eq: "(s ~: E i) = (s : H i | s : T i)"
+lemma not_E_eq: "(s \<notin> E i) = (s \<in> H i | s \<in> T i)"
apply (simp add: H_def E_def T_def)
apply (case_tac "proc s i", auto)
done
-lemma (in Token) token_stable: "F : stable (-(E i) Un (HasTok i))"
+lemma (in Token) token_stable: "F \<in> stable (-(E i) \<union> (HasTok i))"
apply (unfold stable_def)
apply (rule constrains_weaken)
apply (rule constrains_Un [OF constrains_Un [OF TR2 TR4] TR5])
@@ -74,7 +74,7 @@
done
lemma (in Token) nodeOrder_eq:
- "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)"
+ "[| i<N; j<N |] ==> ((next i, i) \<in> nodeOrder j) = (i \<noteq> 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)
@@ -84,7 +84,7 @@
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)"
+ F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
apply (case_tac "i=j")
apply (blast intro: subset_imp_leadsTo)
apply (rule TR7 [THEN leadsTo_weaken_R])
@@ -93,19 +93,19 @@
(*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}"
+lemma (in Token) TR7_aux: "[| i<N; j<N; i\<noteq>j |]
+ ==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
apply (rule TR7 [THEN leadsTo_weaken_R])
apply (auto simp add: HasTok_def nodeOrder_eq)
done
lemma (in Token) token_lemma:
- "({s. token s < N} Int token -` {m}) = (if m<N then token -` {m} else {})"
+ "({s. token s < N} \<inter> token -` {m}) = (if m<N then token -` {m} else {})"
by auto
(*Misra's TR9: the token reaches an arbitrary node*)
-lemma (in Token) leadsTo_j: "j<N ==> F : {s. token s < N} leadsTo (HasTok j)"
+lemma (in Token) leadsTo_j: "j<N ==> F \<in> {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])
@@ -118,7 +118,7 @@
(*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)"
+ "j<N ==> F \<in> ({s. token s < N} \<inter> 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+)