1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/UNITY/Simple/Channel.ML Mon Mar 05 15:47:11 2001 +0100
1.3 @@ -0,0 +1,57 @@
1.4 +(* Title: HOL/UNITY/Channel
1.5 + ID: $Id$
1.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 + Copyright 1998 University of Cambridge
1.8 +
1.9 +Unordered Channel
1.10 +
1.11 +From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
1.12 +*)
1.13 +
1.14 +(*None represents "infinity" while Some represents proper integers*)
1.15 +Goalw [minSet_def] "minSet A = Some x --> x : A";
1.16 +by (Simp_tac 1);
1.17 +by (fast_tac (claset() addIs [LeastI]) 1);
1.18 +qed_spec_mp "minSet_eq_SomeD";
1.19 +
1.20 +Goalw [minSet_def] " minSet{} = None";
1.21 +by (Asm_simp_tac 1);
1.22 +qed_spec_mp "minSet_empty";
1.23 +Addsimps [minSet_empty];
1.24 +
1.25 +Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)";
1.26 +by Auto_tac;
1.27 +qed_spec_mp "minSet_nonempty";
1.28 +
1.29 +Goal "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))";
1.30 +by (rtac leadsTo_weaken 1);
1.31 +by (res_inst_tac [("x1","x")] ([UC2, UC1] MRS psp) 1);
1.32 +by Safe_tac;
1.33 +by (auto_tac (claset() addDs [minSet_eq_SomeD],
1.34 + simpset() addsimps [linorder_neq_iff]));
1.35 +qed "minSet_greaterThan";
1.36 +
1.37 +(*The induction*)
1.38 +Goal "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))";
1.39 +by (rtac leadsTo_weaken_R 1);
1.40 +by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
1.41 + greaterThan_bounded_induct 1);
1.42 +by Safe_tac;
1.43 +by (ALLGOALS Asm_simp_tac);
1.44 +by (dtac minSet_nonempty 2);
1.45 +by (Asm_full_simp_tac 2);
1.46 +by (rtac (minSet_greaterThan RS leadsTo_weaken) 1);
1.47 +by Safe_tac;
1.48 +by (ALLGOALS Asm_full_simp_tac);
1.49 +by (dtac minSet_nonempty 1);
1.50 +by (Asm_full_simp_tac 1);
1.51 +val lemma = result();
1.52 +
1.53 +
1.54 +Goal "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}";
1.55 +by (rtac (lemma RS leadsTo_weaken_R) 1);
1.56 +by (Clarify_tac 1);
1.57 +by (ftac minSet_nonempty 1);
1.58 +by (auto_tac (claset() addDs [Suc_le_lessD, not_less_Least],
1.59 + simpset()));
1.60 +qed "Channel_progress";
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/UNITY/Simple/Channel.thy Mon Mar 05 15:47:11 2001 +0100
2.3 @@ -0,0 +1,30 @@
2.4 +(* Title: HOL/UNITY/Channel
2.5 + ID: $Id$
2.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
2.7 + Copyright 1998 University of Cambridge
2.8 +
2.9 +Unordered Channel
2.10 +
2.11 +From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
2.12 +*)
2.13 +
2.14 +Channel = WFair + Option +
2.15 +
2.16 +types state = nat set
2.17 +
2.18 +consts
2.19 + F :: state program
2.20 +
2.21 +constdefs
2.22 + minSet :: nat set => nat option
2.23 + "minSet A == if A={} then None else Some (LEAST x. x:A)"
2.24 +
2.25 +rules
2.26 +
2.27 + UC1 "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
2.28 +
2.29 + (* UC1 "F : {s. minSet s = x} co {s. x <= minSet s}" *)
2.30 +
2.31 + UC2 "F : (minSet -` {Some x}) leadsTo {s. x ~: s}"
2.32 +
2.33 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/UNITY/Simple/Common.ML Mon Mar 05 15:47:11 2001 +0100
3.3 @@ -0,0 +1,90 @@
3.4 +(* Title: HOL/UNITY/Common
3.5 + ID: $Id$
3.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3.7 + Copyright 1998 University of Cambridge
3.8 +
3.9 +Common Meeting Time example from Misra (1994)
3.10 +
3.11 +The state is identified with the one variable in existence.
3.12 +
3.13 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
3.14 +*)
3.15 +
3.16 +(*Misra's property CMT4: t exceeds no common meeting time*)
3.17 +Goal "[| ALL m. F : {m} Co (maxfg m); n: common |] \
3.18 +\ ==> F : Stable (atMost n)";
3.19 +by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
3.20 +by (asm_full_simp_tac
3.21 + (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
3.22 + le_max_iff_disj]) 1);
3.23 +by (etac Constrains_weaken_R 1);
3.24 +by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
3.25 +qed "common_stable";
3.26 +
3.27 +Goal "[| Init F <= atMost n; \
3.28 +\ ALL m. F : {m} Co (maxfg m); n: common |] \
3.29 +\ ==> F : Always (atMost n)";
3.30 +by (asm_simp_tac (simpset() addsimps [AlwaysI, common_stable]) 1);
3.31 +qed "common_safety";
3.32 +
3.33 +
3.34 +(*** Some programs that implement the safety property above ***)
3.35 +
3.36 +Goal "SKIP : {m} co (maxfg m)";
3.37 +by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
3.38 + fasc]) 1);
3.39 +result();
3.40 +
3.41 +(*This one is t := ftime t || t := gtime t*)
3.42 +Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) \
3.43 +\ : {m} co (maxfg m)";
3.44 +by (simp_tac (simpset() addsimps [constrains_def, maxfg_def,
3.45 + le_max_iff_disj, fasc]) 1);
3.46 +result();
3.47 +
3.48 +(*This one is t := max (ftime t) (gtime t)*)
3.49 +Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) \
3.50 +\ : {m} co (maxfg m)";
3.51 +by (simp_tac
3.52 + (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
3.53 +result();
3.54 +
3.55 +(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
3.56 +Goal "mk_program \
3.57 +\ (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV) \
3.58 +\ : {m} co (maxfg m)";
3.59 +by (simp_tac
3.60 + (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
3.61 +result();
3.62 +
3.63 +
3.64 +(*It remans to prove that they satisfy CMT3': t does not decrease,
3.65 + and that CMT3' implies that t stops changing once common(t) holds.*)
3.66 +
3.67 +
3.68 +(*** Progress under weak fairness ***)
3.69 +
3.70 +Addsimps [atMost_Int_atLeast];
3.71 +
3.72 +Goal "[| ALL m. F : {m} Co (maxfg m); \
3.73 +\ ALL m: lessThan n. F : {m} LeadsTo (greaterThan m); \
3.74 +\ n: common |] \
3.75 +\ ==> F : (atMost n) LeadsTo common";
3.76 +by (rtac LeadsTo_weaken_R 1);
3.77 +by (res_inst_tac [("f","id"), ("l","n")] GreaterThan_bounded_induct 1);
3.78 +by (ALLGOALS Asm_simp_tac);
3.79 +by (rtac subset_refl 2);
3.80 +by (blast_tac (claset() addDs [PSP_Stable2]
3.81 + addIs [common_stable, LeadsTo_weaken_R]) 1);
3.82 +val lemma = result();
3.83 +
3.84 +(*The "ALL m: -common" form echoes CMT6.*)
3.85 +Goal "[| ALL m. F : {m} Co (maxfg m); \
3.86 +\ ALL m: -common. F : {m} LeadsTo (greaterThan m); \
3.87 +\ n: common |] \
3.88 +\ ==> F : (atMost (LEAST n. n: common)) LeadsTo common";
3.89 +by (rtac lemma 1);
3.90 +by (ALLGOALS Asm_simp_tac);
3.91 +by (etac LeastI 2);
3.92 +by (blast_tac (claset() addSDs [not_less_Least]) 1);
3.93 +qed "leadsTo_common";
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/UNITY/Simple/Common.thy Mon Mar 05 15:47:11 2001 +0100
4.3 @@ -0,0 +1,32 @@
4.4 +(* Title: HOL/UNITY/Common
4.5 + ID: $Id$
4.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4.7 + Copyright 1998 University of Cambridge
4.8 +
4.9 +Common Meeting Time example from Misra (1994)
4.10 +
4.11 +The state is identified with the one variable in existence.
4.12 +
4.13 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
4.14 +*)
4.15 +
4.16 +Common = SubstAx +
4.17 +
4.18 +consts
4.19 + ftime,gtime :: nat=>nat
4.20 +
4.21 +rules
4.22 + fmono "m <= n ==> ftime m <= ftime n"
4.23 + gmono "m <= n ==> gtime m <= gtime n"
4.24 +
4.25 + fasc "m <= ftime n"
4.26 + gasc "m <= gtime n"
4.27 +
4.28 +constdefs
4.29 + common :: nat set
4.30 + "common == {n. ftime n = n & gtime n = n}"
4.31 +
4.32 + maxfg :: nat => nat set
4.33 + "maxfg m == {t. t <= max (ftime m) (gtime m)}"
4.34 +
4.35 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/UNITY/Simple/Deadlock.ML Mon Mar 05 15:47:11 2001 +0100
5.3 @@ -0,0 +1,78 @@
5.4 +(* Title: HOL/UNITY/Deadlock
5.5 + ID: $Id$
5.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
5.7 + Copyright 1998 University of Cambridge
5.8 +
5.9 +Deadlock examples from section 5.6 of
5.10 + Misra, "A Logic for Concurrent Programming", 1994
5.11 +*)
5.12 +
5.13 +(*Trivial, two-process case*)
5.14 +Goalw [constrains_def, stable_def]
5.15 + "[| F : (A Int B) co A; F : (B Int A) co B |] ==> F : stable (A Int B)";
5.16 +by (Blast_tac 1);
5.17 +result();
5.18 +
5.19 +
5.20 +(*a simplification step*)
5.21 +Goal "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)";
5.22 +by (induct_tac "n" 1);
5.23 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc])));
5.24 +by Auto_tac;
5.25 +qed "Collect_le_Int_equals";
5.26 +
5.27 +(*Dual of the required property. Converse inclusion fails.*)
5.28 +Goal "(UN i: lessThan n. A i) Int (- A n) <= \
5.29 +\ (UN i: lessThan n. (A i) Int (- A (Suc i)))";
5.30 +by (induct_tac "n" 1);
5.31 +by (Asm_simp_tac 1);
5.32 +by (simp_tac (simpset() addsimps [lessThan_Suc]) 1);
5.33 +by (Blast_tac 1);
5.34 +qed "UN_Int_Compl_subset";
5.35 +
5.36 +
5.37 +(*Converse inclusion fails.*)
5.38 +Goal "(INT i: lessThan n. -A i Un A (Suc i)) <= \
5.39 +\ (INT i: lessThan n. -A i) Un A n";
5.40 +by (induct_tac "n" 1);
5.41 +by (Asm_simp_tac 1);
5.42 +by (asm_simp_tac (simpset() addsimps [lessThan_Suc]) 1);
5.43 +by (Blast_tac 1);
5.44 +qed "INT_Un_Compl_subset";
5.45 +
5.46 +
5.47 +(*Specialized rewriting*)
5.48 +Goal "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}";
5.49 +by (blast_tac (claset() addIs [gr0I]
5.50 + addDs [impOfSubs INT_Un_Compl_subset]) 1);
5.51 +val lemma = result();
5.52 +
5.53 +(*Reverse direction makes it harder to invoke the ind hyp*)
5.54 +Goal "(INT i: atMost n. A i) = \
5.55 +\ A 0 Int (INT i: lessThan n. -A i Un A(Suc i))";
5.56 +by (induct_tac "n" 1);
5.57 +by (Asm_simp_tac 1);
5.58 +by (asm_simp_tac
5.59 + (simpset() addsimps Int_ac @ [Int_Un_distrib, Int_Un_distrib2, lemma,
5.60 + lessThan_Suc, atMost_Suc]) 1);
5.61 +qed "INT_le_equals_Int";
5.62 +
5.63 +Goal "(INT i: atMost (Suc n). A i) = \
5.64 +\ A 0 Int (INT i: atMost n. -A i Un A(Suc i))";
5.65 +by (simp_tac (simpset() addsimps [lessThan_Suc_atMost, INT_le_equals_Int]) 1);
5.66 +qed "INT_le_Suc_equals_Int";
5.67 +
5.68 +
5.69 +(*The final deadlock example*)
5.70 +val [zeroprem, allprem] = Goalw [stable_def]
5.71 + "[| F : (A 0 Int A (Suc n)) co (A 0); \
5.72 +\ !!i. i: atMost n ==> F : (A(Suc i) Int A i) co (-A i Un A(Suc i)) |] \
5.73 +\ ==> F : stable (INT i: atMost (Suc n). A i)";
5.74 +by (rtac ([zeroprem, constrains_INT] MRS
5.75 + constrains_Int RS constrains_weaken) 1);
5.76 +by (etac allprem 1);
5.77 +by (simp_tac (simpset() addsimps [Collect_le_Int_equals,
5.78 + Int_assoc, INT_absorb]) 1);
5.79 +by (simp_tac (simpset() addsimps [INT_le_Suc_equals_Int]) 1);
5.80 +result();
5.81 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/UNITY/Simple/Deadlock.thy Mon Mar 05 15:47:11 2001 +0100
6.3 @@ -0,0 +1,1 @@
6.4 +Deadlock = UNITY
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/UNITY/Simple/Lift.ML Mon Mar 05 15:47:11 2001 +0100
7.3 @@ -0,0 +1,317 @@
7.4 +(* Title: HOL/UNITY/Lift
7.5 + ID: $Id$
7.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
7.7 + Copyright 1998 University of Cambridge
7.8 +
7.9 +The Lift-Control Example
7.10 +*)
7.11 +
7.12 +Goal "[| x ~: A; y : A |] ==> x ~= y";
7.13 +by (Blast_tac 1);
7.14 +qed "not_mem_distinct";
7.15 +
7.16 +
7.17 +Addsimps [Lift_def RS def_prg_Init];
7.18 +program_defs_ref := [Lift_def];
7.19 +
7.20 +Addsimps (map simp_of_act
7.21 + [request_act_def, open_act_def, close_act_def,
7.22 + req_up_def, req_down_def, move_up_def, move_down_def,
7.23 + button_press_def]);
7.24 +
7.25 +(*The ALWAYS properties*)
7.26 +Addsimps (map simp_of_set [above_def, below_def, queueing_def,
7.27 + goingup_def, goingdown_def, ready_def]);
7.28 +
7.29 +Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
7.30 + moving_up_def, moving_down_def];
7.31 +
7.32 +AddIffs [Min_le_Max];
7.33 +
7.34 +Goal "Lift : Always open_stop";
7.35 +by (always_tac 1);
7.36 +qed "open_stop";
7.37 +
7.38 +Goal "Lift : Always stop_floor";
7.39 +by (always_tac 1);
7.40 +qed "stop_floor";
7.41 +
7.42 +(*This one needs open_stop, which was proved above*)
7.43 +Goal "Lift : Always open_move";
7.44 +by (cut_facts_tac [open_stop] 1);
7.45 +by (always_tac 1);
7.46 +qed "open_move";
7.47 +
7.48 +Goal "Lift : Always moving_up";
7.49 +by (always_tac 1);
7.50 +by (auto_tac (claset() addDs [zle_imp_zless_or_eq],
7.51 + simpset() addsimps [add1_zle_eq]));
7.52 +qed "moving_up";
7.53 +
7.54 +Goal "Lift : Always moving_down";
7.55 +by (always_tac 1);
7.56 +by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
7.57 +qed "moving_down";
7.58 +
7.59 +Goal "Lift : Always bounded";
7.60 +by (cut_facts_tac [moving_up, moving_down] 1);
7.61 +by (always_tac 1);
7.62 +by Auto_tac;
7.63 +by (ALLGOALS (dtac not_mem_distinct THEN' assume_tac));
7.64 +by (ALLGOALS arith_tac);
7.65 +qed "bounded";
7.66 +
7.67 +
7.68 +
7.69 +(*** Progress ***)
7.70 +
7.71 +
7.72 +val abbrev_defs = [moving_def, stopped_def,
7.73 + opened_def, closed_def, atFloor_def, Req_def];
7.74 +
7.75 +Addsimps (map simp_of_set abbrev_defs);
7.76 +
7.77 +
7.78 +(** The HUG'93 paper mistakenly omits the Req n from these! **)
7.79 +
7.80 +(** Lift_1 **)
7.81 +
7.82 +Goal "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)";
7.83 +by (cut_facts_tac [stop_floor] 1);
7.84 +by (ensures_tac "open_act" 1);
7.85 +qed "E_thm01"; (*lem_lift_1_5*)
7.86 +
7.87 +Goal "Lift : (Req n Int stopped - atFloor n) LeadsTo \
7.88 +\ (Req n Int opened - atFloor n)";
7.89 +by (cut_facts_tac [stop_floor] 1);
7.90 +by (ensures_tac "open_act" 1);
7.91 +qed "E_thm02"; (*lem_lift_1_1*)
7.92 +
7.93 +Goal "Lift : (Req n Int opened - atFloor n) LeadsTo \
7.94 +\ (Req n Int closed - (atFloor n - queueing))";
7.95 +by (ensures_tac "close_act" 1);
7.96 +qed "E_thm03"; (*lem_lift_1_2*)
7.97 +
7.98 +Goal "Lift : (Req n Int closed Int (atFloor n - queueing)) \
7.99 +\ LeadsTo (opened Int atFloor n)";
7.100 +by (ensures_tac "open_act" 1);
7.101 +qed "E_thm04"; (*lem_lift_1_7*)
7.102 +
7.103 +
7.104 +(** Lift 2. Statements of thm05a and thm05b were wrong! **)
7.105 +
7.106 +Open_locale "floor";
7.107 +
7.108 +val Min_le_n = thm "Min_le_n";
7.109 +val n_le_Max = thm "n_le_Max";
7.110 +
7.111 +AddIffs [Min_le_n, n_le_Max];
7.112 +
7.113 +val le_MinD = Min_le_n RS order_antisym;
7.114 +val Max_leD = n_le_Max RSN (2,order_antisym);
7.115 +
7.116 +val linorder_leI = linorder_not_less RS iffD1;
7.117 +
7.118 +AddSDs [le_MinD, linorder_leI RS le_MinD,
7.119 + Max_leD, linorder_leI RS Max_leD];
7.120 +
7.121 +(*lem_lift_2_0
7.122 + NOT an ensures property, but a mere inclusion;
7.123 + don't know why script lift_2.uni says ENSURES*)
7.124 +Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \
7.125 +\ LeadsTo ((closed Int goingup Int Req n) Un \
7.126 +\ (closed Int goingdown Int Req n))";
7.127 +by (auto_tac (claset() addSIs [subset_imp_LeadsTo] addSEs [int_neqE],
7.128 + simpset()));
7.129 +qed "E_thm05c";
7.130 +
7.131 +(*lift_2*)
7.132 +Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \
7.133 +\ LeadsTo (moving Int Req n)";
7.134 +by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
7.135 +by (ensures_tac "req_down" 2);
7.136 +by (ensures_tac "req_up" 1);
7.137 +by Auto_tac;
7.138 +qed "lift_2";
7.139 +
7.140 +
7.141 +(** Towards lift_4 ***)
7.142 +
7.143 +val metric_ss = simpset() addsplits [split_if_asm]
7.144 + addsimps [metric_def, vimage_def];
7.145 +
7.146 +
7.147 +(*lem_lift_4_1 *)
7.148 +Goal "#0 < N ==> \
7.149 +\ Lift : (moving Int Req n Int {s. metric n s = N} Int \
7.150 +\ {s. floor s ~: req s} Int {s. up s}) \
7.151 +\ LeadsTo \
7.152 +\ (moving Int Req n Int {s. metric n s < N})";
7.153 +by (cut_facts_tac [moving_up] 1);
7.154 +by (ensures_tac "move_up" 1);
7.155 +by Safe_tac;
7.156 +(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
7.157 +by (etac (linorder_leI RS order_antisym RS sym) 1);
7.158 +by (auto_tac (claset(), metric_ss));
7.159 +qed "E_thm12a";
7.160 +
7.161 +
7.162 +(*lem_lift_4_3 *)
7.163 +Goal "#0 < N ==> \
7.164 +\ Lift : (moving Int Req n Int {s. metric n s = N} Int \
7.165 +\ {s. floor s ~: req s} - {s. up s}) \
7.166 +\ LeadsTo (moving Int Req n Int {s. metric n s < N})";
7.167 +by (cut_facts_tac [moving_down] 1);
7.168 +by (ensures_tac "move_down" 1);
7.169 +by Safe_tac;
7.170 +(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
7.171 +by (etac (linorder_leI RS order_antisym RS sym) 1);
7.172 +by (auto_tac (claset(), metric_ss));
7.173 +qed "E_thm12b";
7.174 +
7.175 +(*lift_4*)
7.176 +Goal "#0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int \
7.177 +\ {s. floor s ~: req s}) LeadsTo \
7.178 +\ (moving Int Req n Int {s. metric n s < N})";
7.179 +by (rtac ([subset_imp_LeadsTo, [E_thm12a, E_thm12b] MRS LeadsTo_Un]
7.180 + MRS LeadsTo_Trans) 1);
7.181 +by Auto_tac;
7.182 +qed "lift_4";
7.183 +
7.184 +
7.185 +(** towards lift_5 **)
7.186 +
7.187 +(*lem_lift_5_3*)
7.188 +Goal "#0<N \
7.189 +\ ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \
7.190 +\ (moving Int Req n Int {s. metric n s < N})";
7.191 +by (cut_facts_tac [bounded] 1);
7.192 +by (ensures_tac "req_up" 1);
7.193 +by (auto_tac (claset(), metric_ss));
7.194 +qed "E_thm16a";
7.195 +
7.196 +
7.197 +(*lem_lift_5_1 has ~goingup instead of goingdown*)
7.198 +Goal "#0<N ==> \
7.199 +\ Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \
7.200 +\ (moving Int Req n Int {s. metric n s < N})";
7.201 +by (cut_facts_tac [bounded] 1);
7.202 +by (ensures_tac "req_down" 1);
7.203 +by (auto_tac (claset(), metric_ss));
7.204 +qed "E_thm16b";
7.205 +
7.206 +
7.207 +(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
7.208 + i.e. the trivial disjunction, leading to an asymmetrical proof.*)
7.209 +Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
7.210 +by (Clarify_tac 1);
7.211 +by (auto_tac (claset(), metric_ss));
7.212 +qed "E_thm16c";
7.213 +
7.214 +
7.215 +(*lift_5*)
7.216 +Goal "#0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo \
7.217 +\ (moving Int Req n Int {s. metric n s < N})";
7.218 +by (rtac ([subset_imp_LeadsTo, [E_thm16a, E_thm16b] MRS LeadsTo_Un]
7.219 + MRS LeadsTo_Trans) 1);
7.220 +by (dtac E_thm16c 1);
7.221 +by Auto_tac;
7.222 +qed "lift_5";
7.223 +
7.224 +
7.225 +(** towards lift_3 **)
7.226 +
7.227 +(*lemma used to prove lem_lift_3_1*)
7.228 +Goal "[| metric n s = #0; Min <= floor s; floor s <= Max |] ==> floor s = n";
7.229 +by (auto_tac (claset(), metric_ss));
7.230 +qed "metric_eq_0D";
7.231 +
7.232 +AddDs [metric_eq_0D];
7.233 +
7.234 +
7.235 +(*lem_lift_3_1*)
7.236 +Goal "Lift : (moving Int Req n Int {s. metric n s = #0}) LeadsTo \
7.237 +\ (stopped Int atFloor n)";
7.238 +by (cut_facts_tac [bounded] 1);
7.239 +by (ensures_tac "request_act" 1);
7.240 +by Auto_tac;
7.241 +qed "E_thm11";
7.242 +
7.243 +(*lem_lift_3_5*)
7.244 +Goal
7.245 + "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
7.246 +\ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
7.247 +by (ensures_tac "request_act" 1);
7.248 +by (auto_tac (claset(), metric_ss));
7.249 +qed "E_thm13";
7.250 +
7.251 +(*lem_lift_3_6*)
7.252 +Goal "#0 < N ==> \
7.253 +\ Lift : \
7.254 +\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
7.255 +\ LeadsTo (opened Int Req n Int {s. metric n s = N})";
7.256 +by (ensures_tac "open_act" 1);
7.257 +by (auto_tac (claset(), metric_ss));
7.258 +qed "E_thm14";
7.259 +
7.260 +(*lem_lift_3_7*)
7.261 +Goal "Lift : (opened Int Req n Int {s. metric n s = N}) \
7.262 +\ LeadsTo (closed Int Req n Int {s. metric n s = N})";
7.263 +by (ensures_tac "close_act" 1);
7.264 +by (auto_tac (claset(), metric_ss));
7.265 +qed "E_thm15";
7.266 +
7.267 +
7.268 +(** the final steps **)
7.269 +
7.270 +Goal "#0 < N ==> \
7.271 +\ Lift : \
7.272 +\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
7.273 +\ LeadsTo (moving Int Req n Int {s. metric n s < N})";
7.274 +by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
7.275 + addIs [LeadsTo_Trans]) 1);
7.276 +qed "lift_3_Req";
7.277 +
7.278 +
7.279 +(*Now we observe that our integer metric is really a natural number*)
7.280 +Goal "Lift : Always {s. #0 <= metric n s}";
7.281 +by (rtac (bounded RS Always_weaken) 1);
7.282 +by (auto_tac (claset(), metric_ss));
7.283 +qed "Always_nonneg";
7.284 +
7.285 +val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken;
7.286 +
7.287 +Goal "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)";
7.288 +by (rtac (Always_nonneg RS integ_0_le_induct) 1);
7.289 +by (case_tac "#0 < z" 1);
7.290 +(*If z <= #0 then actually z = #0*)
7.291 +by (force_tac (claset() addIs [R_thm11, order_antisym],
7.292 + simpset() addsimps [linorder_not_less]) 2);
7.293 +by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
7.294 +by (rtac ([subset_imp_LeadsTo, [lift_4, lift_3_Req] MRS LeadsTo_Un]
7.295 + MRS LeadsTo_Trans) 1);
7.296 +by Auto_tac;
7.297 +qed "lift_3";
7.298 +
7.299 +
7.300 +val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
7.301 +(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *)
7.302 +
7.303 +Goal "Lift : (Req n) LeadsTo (opened Int atFloor n)";
7.304 +by (rtac LeadsTo_Trans 1);
7.305 +by (rtac ([E_thm04, LeadsTo_Un_post] MRS LeadsTo_Un) 2);
7.306 +by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2);
7.307 +by (rtac (lift_3 RS LeadsTo_Trans_Un') 2);
7.308 +by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
7.309 +by (rtac ([E_thm03,E_thm02] MRS LeadsTo_Trans_Un') 2);
7.310 +by (rtac (open_move RS Always_LeadsToI) 1);
7.311 +by (rtac ([open_stop, subset_imp_LeadsTo] MRS Always_LeadsToI) 1);
7.312 +by (Clarify_tac 1);
7.313 +(*The case split is not essential but makes Blast_tac much faster.
7.314 + Calling rotate_tac prevents simplification from looping*)
7.315 +by (case_tac "open x" 1);
7.316 +by (ALLGOALS (rotate_tac ~1));
7.317 +by Auto_tac;
7.318 +qed "lift_1";
7.319 +
7.320 +Close_locale "floor";
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/UNITY/Simple/Lift.thy Mon Mar 05 15:47:11 2001 +0100
8.3 @@ -0,0 +1,169 @@
8.4 +(* Title: HOL/UNITY/Lift.thy
8.5 + ID: $Id$
8.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
8.7 + Copyright 1998 University of Cambridge
8.8 +
8.9 +The Lift-Control Example
8.10 +*)
8.11 +
8.12 +Lift = SubstAx +
8.13 +
8.14 +record state =
8.15 + floor :: int (*current position of the lift*)
8.16 + open :: bool (*whether the door is open at floor*)
8.17 + stop :: bool (*whether the lift is stopped at floor*)
8.18 + req :: int set (*for each floor, whether the lift is requested*)
8.19 + up :: bool (*current direction of movement*)
8.20 + move :: bool (*whether moving takes precedence over opening*)
8.21 +
8.22 +consts
8.23 + Min, Max :: int (*least and greatest floors*)
8.24 +
8.25 +rules
8.26 + Min_le_Max "Min <= Max"
8.27 +
8.28 +constdefs
8.29 +
8.30 + (** Abbreviations: the "always" part **)
8.31 +
8.32 + above :: state set
8.33 + "above == {s. EX i. floor s < i & i <= Max & i : req s}"
8.34 +
8.35 + below :: state set
8.36 + "below == {s. EX i. Min <= i & i < floor s & i : req s}"
8.37 +
8.38 + queueing :: state set
8.39 + "queueing == above Un below"
8.40 +
8.41 + goingup :: state set
8.42 + "goingup == above Int ({s. up s} Un -below)"
8.43 +
8.44 + goingdown :: state set
8.45 + "goingdown == below Int ({s. ~ up s} Un -above)"
8.46 +
8.47 + ready :: state set
8.48 + "ready == {s. stop s & ~ open s & move s}"
8.49 +
8.50 +
8.51 + (** Further abbreviations **)
8.52 +
8.53 + moving :: state set
8.54 + "moving == {s. ~ stop s & ~ open s}"
8.55 +
8.56 + stopped :: state set
8.57 + "stopped == {s. stop s & ~ open s & ~ move s}"
8.58 +
8.59 + opened :: state set
8.60 + "opened == {s. stop s & open s & move s}"
8.61 +
8.62 + closed :: state set (*but this is the same as ready!!*)
8.63 + "closed == {s. stop s & ~ open s & move s}"
8.64 +
8.65 + atFloor :: int => state set
8.66 + "atFloor n == {s. floor s = n}"
8.67 +
8.68 + Req :: int => state set
8.69 + "Req n == {s. n : req s}"
8.70 +
8.71 +
8.72 +
8.73 + (** The program **)
8.74 +
8.75 + request_act :: "(state*state) set"
8.76 + "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
8.77 + & ~ stop s & floor s : req s}"
8.78 +
8.79 + open_act :: "(state*state) set"
8.80 + "open_act ==
8.81 + {(s,s'). s' = s (|open :=True,
8.82 + req := req s - {floor s},
8.83 + move := True|)
8.84 + & stop s & ~ open s & floor s : req s
8.85 + & ~(move s & s: queueing)}"
8.86 +
8.87 + close_act :: "(state*state) set"
8.88 + "close_act == {(s,s'). s' = s (|open := False|) & open s}"
8.89 +
8.90 + req_up :: "(state*state) set"
8.91 + "req_up ==
8.92 + {(s,s'). s' = s (|stop :=False,
8.93 + floor := floor s + #1,
8.94 + up := True|)
8.95 + & s : (ready Int goingup)}"
8.96 +
8.97 + req_down :: "(state*state) set"
8.98 + "req_down ==
8.99 + {(s,s'). s' = s (|stop :=False,
8.100 + floor := floor s - #1,
8.101 + up := False|)
8.102 + & s : (ready Int goingdown)}"
8.103 +
8.104 + move_up :: "(state*state) set"
8.105 + "move_up ==
8.106 + {(s,s'). s' = s (|floor := floor s + #1|)
8.107 + & ~ stop s & up s & floor s ~: req s}"
8.108 +
8.109 + move_down :: "(state*state) set"
8.110 + "move_down ==
8.111 + {(s,s'). s' = s (|floor := floor s - #1|)
8.112 + & ~ stop s & ~ up s & floor s ~: req s}"
8.113 +
8.114 + (*This action is omitted from prior treatments, which therefore are
8.115 + unrealistic: nobody asks the lift to do anything! But adding this
8.116 + action invalidates many of the existing progress arguments: various
8.117 + "ensures" properties fail.*)
8.118 + button_press :: "(state*state) set"
8.119 + "button_press ==
8.120 + {(s,s'). EX n. s' = s (|req := insert n (req s)|)
8.121 + & Min <= n & n <= Max}"
8.122 +
8.123 +
8.124 + Lift :: state program
8.125 + (*for the moment, we OMIT button_press*)
8.126 + "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
8.127 + ~ open s & req s = {}},
8.128 + {request_act, open_act, close_act,
8.129 + req_up, req_down, move_up, move_down},
8.130 + UNIV)"
8.131 +
8.132 +
8.133 + (** Invariants **)
8.134 +
8.135 + bounded :: state set
8.136 + "bounded == {s. Min <= floor s & floor s <= Max}"
8.137 +
8.138 + open_stop :: state set
8.139 + "open_stop == {s. open s --> stop s}"
8.140 +
8.141 + open_move :: state set
8.142 + "open_move == {s. open s --> move s}"
8.143 +
8.144 + stop_floor :: state set
8.145 + "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
8.146 +
8.147 + moving_up :: state set
8.148 + "moving_up == {s. ~ stop s & up s -->
8.149 + (EX f. floor s <= f & f <= Max & f : req s)}"
8.150 +
8.151 + moving_down :: state set
8.152 + "moving_down == {s. ~ stop s & ~ up s -->
8.153 + (EX f. Min <= f & f <= floor s & f : req s)}"
8.154 +
8.155 + metric :: [int,state] => int
8.156 + "metric ==
8.157 + %n s. if floor s < n then (if up s then n - floor s
8.158 + else (floor s - Min) + (n-Min))
8.159 + else
8.160 + if n < floor s then (if up s then (Max - floor s) + (Max-n)
8.161 + else floor s - n)
8.162 + else #0"
8.163 +
8.164 +locale floor =
8.165 + fixes
8.166 + n :: int
8.167 + assumes
8.168 + Min_le_n "Min <= n"
8.169 + n_le_Max "n <= Max"
8.170 + defines
8.171 +
8.172 +end
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/UNITY/Simple/Mutex.ML Mon Mar 05 15:47:11 2001 +0100
9.3 @@ -0,0 +1,166 @@
9.4 +(* Title: HOL/UNITY/Mutex
9.5 + ID: $Id$
9.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
9.7 + Copyright 1998 University of Cambridge
9.8 +
9.9 +Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
9.10 +*)
9.11 +
9.12 +Addsimps [Mutex_def RS def_prg_Init];
9.13 +program_defs_ref := [Mutex_def];
9.14 +
9.15 +Addsimps (map simp_of_act
9.16 + [U0_def, U1_def, U2_def, U3_def, U4_def,
9.17 + V0_def, V1_def, V2_def, V3_def, V4_def]);
9.18 +
9.19 +Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
9.20 +
9.21 +
9.22 +Goal "Mutex : Always IU";
9.23 +by (always_tac 1);
9.24 +qed "IU";
9.25 +
9.26 +Goal "Mutex : Always IV";
9.27 +by (always_tac 1);
9.28 +qed "IV";
9.29 +
9.30 +(*The safety property: mutual exclusion*)
9.31 +Goal "Mutex : Always {s. ~ (m s = #3 & n s = #3)}";
9.32 +by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
9.33 +by Auto_tac;
9.34 +qed "mutual_exclusion";
9.35 +
9.36 +
9.37 +(*The bad invariant FAILS in V1*)
9.38 +Goal "Mutex : Always bad_IU";
9.39 +by (always_tac 1);
9.40 +by Auto_tac;
9.41 +(*Resulting state: n=1, p=false, m=4, u=false.
9.42 + Execution of V1 (the command of process v guarded by n=1) sets p:=true,
9.43 + violating the invariant!*)
9.44 +(*Check that subgoals remain: proof failed.*)
9.45 +getgoal 1;
9.46 +
9.47 +
9.48 +Goal "((#1::int) <= i & i <= #3) = (i = #1 | i = #2 | i = #3)";
9.49 +by (arith_tac 1);
9.50 +qed "eq_123";
9.51 +
9.52 +
9.53 +(*** Progress for U ***)
9.54 +
9.55 +Goalw [Unless_def] "Mutex : {s. m s=#2} Unless {s. m s=#3}";
9.56 +by (constrains_tac 1);
9.57 +qed "U_F0";
9.58 +
9.59 +Goal "Mutex : {s. m s=#1} LeadsTo {s. p s = v s & m s = #2}";
9.60 +by (ensures_tac "U1" 1);
9.61 +qed "U_F1";
9.62 +
9.63 +Goal "Mutex : {s. ~ p s & m s = #2} LeadsTo {s. m s = #3}";
9.64 +by (cut_facts_tac [IU] 1);
9.65 +by (ensures_tac "U2" 1);
9.66 +qed "U_F2";
9.67 +
9.68 +Goal "Mutex : {s. m s = #3} LeadsTo {s. p s}";
9.69 +by (res_inst_tac [("B", "{s. m s = #4}")] LeadsTo_Trans 1);
9.70 +by (ensures_tac "U4" 2);
9.71 +by (ensures_tac "U3" 1);
9.72 +qed "U_F3";
9.73 +
9.74 +Goal "Mutex : {s. m s = #2} LeadsTo {s. p s}";
9.75 +by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
9.76 + MRS LeadsTo_Diff) 1);
9.77 +by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
9.78 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
9.79 +val U_lemma2 = result();
9.80 +
9.81 +Goal "Mutex : {s. m s = #1} LeadsTo {s. p s}";
9.82 +by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
9.83 +by (Blast_tac 1);
9.84 +val U_lemma1 = result();
9.85 +
9.86 +Goal "Mutex : {s. #1 <= m s & m s <= #3} LeadsTo {s. p s}";
9.87 +by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
9.88 + U_lemma1, U_lemma2, U_F3] ) 1);
9.89 +val U_lemma123 = result();
9.90 +
9.91 +(*Misra's F4*)
9.92 +Goal "Mutex : {s. u s} LeadsTo {s. p s}";
9.93 +by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1);
9.94 +by Auto_tac;
9.95 +qed "u_Leadsto_p";
9.96 +
9.97 +
9.98 +(*** Progress for V ***)
9.99 +
9.100 +
9.101 +Goalw [Unless_def] "Mutex : {s. n s=#2} Unless {s. n s=#3}";
9.102 +by (constrains_tac 1);
9.103 +qed "V_F0";
9.104 +
9.105 +Goal "Mutex : {s. n s=#1} LeadsTo {s. p s = (~ u s) & n s = #2}";
9.106 +by (ensures_tac "V1" 1);
9.107 +qed "V_F1";
9.108 +
9.109 +Goal "Mutex : {s. p s & n s = #2} LeadsTo {s. n s = #3}";
9.110 +by (cut_facts_tac [IV] 1);
9.111 +by (ensures_tac "V2" 1);
9.112 +qed "V_F2";
9.113 +
9.114 +Goal "Mutex : {s. n s = #3} LeadsTo {s. ~ p s}";
9.115 +by (res_inst_tac [("B", "{s. n s = #4}")] LeadsTo_Trans 1);
9.116 +by (ensures_tac "V4" 2);
9.117 +by (ensures_tac "V3" 1);
9.118 +qed "V_F3";
9.119 +
9.120 +Goal "Mutex : {s. n s = #2} LeadsTo {s. ~ p s}";
9.121 +by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
9.122 + MRS LeadsTo_Diff) 1);
9.123 +by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
9.124 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
9.125 +val V_lemma2 = result();
9.126 +
9.127 +Goal "Mutex : {s. n s = #1} LeadsTo {s. ~ p s}";
9.128 +by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
9.129 +by (Blast_tac 1);
9.130 +val V_lemma1 = result();
9.131 +
9.132 +Goal "Mutex : {s. #1 <= n s & n s <= #3} LeadsTo {s. ~ p s}";
9.133 +by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
9.134 + V_lemma1, V_lemma2, V_F3] ) 1);
9.135 +val V_lemma123 = result();
9.136 +
9.137 +
9.138 +(*Misra's F4*)
9.139 +Goal "Mutex : {s. v s} LeadsTo {s. ~ p s}";
9.140 +by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
9.141 +by Auto_tac;
9.142 +qed "v_Leadsto_not_p";
9.143 +
9.144 +
9.145 +(** Absence of starvation **)
9.146 +
9.147 +(*Misra's F6*)
9.148 +Goal "Mutex : {s. m s = #1} LeadsTo {s. m s = #3}";
9.149 +by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
9.150 +by (rtac U_F2 2);
9.151 +by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
9.152 +by (stac Un_commute 1);
9.153 +by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
9.154 +by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2);
9.155 +by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
9.156 +by Auto_tac;
9.157 +qed "m1_Leadsto_3";
9.158 +
9.159 +(*The same for V*)
9.160 +Goal "Mutex : {s. n s = #1} LeadsTo {s. n s = #3}";
9.161 +by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
9.162 +by (rtac V_F2 2);
9.163 +by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
9.164 +by (stac Un_commute 1);
9.165 +by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
9.166 +by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2);
9.167 +by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
9.168 +by Auto_tac;
9.169 +qed "n1_Leadsto_3";
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/UNITY/Simple/Mutex.thy Mon Mar 05 15:47:11 2001 +0100
10.3 @@ -0,0 +1,76 @@
10.4 +(* Title: HOL/UNITY/Mutex.thy
10.5 + ID: $Id$
10.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
10.7 + Copyright 1998 University of Cambridge
10.8 +
10.9 +Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
10.10 +*)
10.11 +
10.12 +Mutex = SubstAx +
10.13 +
10.14 +record state =
10.15 + p :: bool
10.16 + m :: int
10.17 + n :: int
10.18 + u :: bool
10.19 + v :: bool
10.20 +
10.21 +types command = "(state*state) set"
10.22 +
10.23 +constdefs
10.24 +
10.25 + (** The program for process U **)
10.26 +
10.27 + U0 :: command
10.28 + "U0 == {(s,s'). s' = s (|u:=True, m:=#1|) & m s = #0}"
10.29 +
10.30 + U1 :: command
10.31 + "U1 == {(s,s'). s' = s (|p:= v s, m:=#2|) & m s = #1}"
10.32 +
10.33 + U2 :: command
10.34 + "U2 == {(s,s'). s' = s (|m:=#3|) & ~ p s & m s = #2}"
10.35 +
10.36 + U3 :: command
10.37 + "U3 == {(s,s'). s' = s (|u:=False, m:=#4|) & m s = #3}"
10.38 +
10.39 + U4 :: command
10.40 + "U4 == {(s,s'). s' = s (|p:=True, m:=#0|) & m s = #4}"
10.41 +
10.42 + (** The program for process V **)
10.43 +
10.44 + V0 :: command
10.45 + "V0 == {(s,s'). s' = s (|v:=True, n:=#1|) & n s = #0}"
10.46 +
10.47 + V1 :: command
10.48 + "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=#2|) & n s = #1}"
10.49 +
10.50 + V2 :: command
10.51 + "V2 == {(s,s'). s' = s (|n:=#3|) & p s & n s = #2}"
10.52 +
10.53 + V3 :: command
10.54 + "V3 == {(s,s'). s' = s (|v:=False, n:=#4|) & n s = #3}"
10.55 +
10.56 + V4 :: command
10.57 + "V4 == {(s,s'). s' = s (|p:=False, n:=#0|) & n s = #4}"
10.58 +
10.59 + Mutex :: state program
10.60 + "Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
10.61 + {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
10.62 + UNIV)"
10.63 +
10.64 +
10.65 + (** The correct invariants **)
10.66 +
10.67 + IU :: state set
10.68 + "IU == {s. (u s = (#1 <= m s & m s <= #3)) & (m s = #3 --> ~ p s)}"
10.69 +
10.70 + IV :: state set
10.71 + "IV == {s. (v s = (#1 <= n s & n s <= #3)) & (n s = #3 --> p s)}"
10.72 +
10.73 + (** The faulty invariant (for U alone) **)
10.74 +
10.75 + bad_IU :: state set
10.76 + "bad_IU == {s. (u s = (#1 <= m s & m s <= #3)) &
10.77 + (#3 <= m s & m s <= #4 --> ~ p s)}"
10.78 +
10.79 +end
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.ML Mon Mar 05 15:47:11 2001 +0100
11.3 @@ -0,0 +1,288 @@
11.4 +(* Title: HOL/Auth/NSP_Bad
11.5 + ID: $Id$
11.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
11.7 + Copyright 1996 University of Cambridge
11.8 +
11.9 +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
11.10 +Flawed version, vulnerable to Lowe's attack.
11.11 +
11.12 +From page 260 of
11.13 + Burrows, Abadi and Needham. A Logic of Authentication.
11.14 + Proc. Royal Soc. 426 (1989)
11.15 +*)
11.16 +
11.17 +fun impOfAlways th =
11.18 + rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
11.19 +
11.20 +AddEs spies_partsEs;
11.21 +AddDs [impOfSubs analz_subset_parts];
11.22 +AddDs [impOfSubs Fake_parts_insert];
11.23 +
11.24 +(*For other theories, e.g. Mutex and Lift, using AddIffs slows proofs down.
11.25 + Here, it facilitates re-use of the Auth proofs.*)
11.26 +
11.27 +AddIffs (map simp_of_act [Fake_def, NS1_def, NS2_def, NS3_def]);
11.28 +
11.29 +Addsimps [Nprg_def RS def_prg_simps];
11.30 +
11.31 +
11.32 +(*A "possibility property": there are traces that reach the end.
11.33 + Replace by LEADSTO proof!*)
11.34 +Goal "A ~= B ==> EX NB. EX s: reachable Nprg. \
11.35 +\ Says A B (Crypt (pubK B) (Nonce NB)) : set s";
11.36 +by (REPEAT (resolve_tac [exI,bexI] 1));
11.37 +by (res_inst_tac [("act", "NS3")] reachable.Acts 2);
11.38 +by (res_inst_tac [("act", "NS2")] reachable.Acts 3);
11.39 +by (res_inst_tac [("act", "NS1")] reachable.Acts 4);
11.40 +by (rtac reachable.Init 5);
11.41 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def])));
11.42 +by (REPEAT_FIRST (rtac exI ));
11.43 +by possibility_tac;
11.44 +result();
11.45 +
11.46 +
11.47 +(**** Inductive proofs about ns_public ****)
11.48 +
11.49 +(*can be used to simulate analz_mono_contra_tac
11.50 +val analz_impI = read_instantiate_sg (sign_of thy)
11.51 + [("P", "?Y ~: analz (spies ?evs)")] impI;
11.52 +
11.53 +val spies_Says_analz_contraD =
11.54 + spies_subset_spies_Says RS analz_mono RS contra_subsetD;
11.55 +
11.56 +by (rtac analz_impI 2);
11.57 +by (auto_tac (claset() addSDs [spies_Says_analz_contraD], simpset()));
11.58 +*)
11.59 +
11.60 +fun ns_constrains_tac i =
11.61 + SELECT_GOAL
11.62 + (EVERY [REPEAT (etac Always_ConstrainsI 1),
11.63 + REPEAT (resolve_tac [StableI, stableI,
11.64 + constrains_imp_Constrains] 1),
11.65 + rtac constrainsI 1,
11.66 + Full_simp_tac 1,
11.67 + REPEAT (FIRSTGOAL (etac disjE)),
11.68 + ALLGOALS (clarify_tac (claset() delrules [impI,impCE])),
11.69 + REPEAT (FIRSTGOAL analz_mono_contra_tac),
11.70 + ALLGOALS Asm_simp_tac]) i;
11.71 +
11.72 +(*Tactic for proving secrecy theorems*)
11.73 +val ns_induct_tac =
11.74 + (SELECT_GOAL o EVERY)
11.75 + [rtac AlwaysI 1,
11.76 + Force_tac 1,
11.77 + (*"reachable" gets in here*)
11.78 + rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1,
11.79 + ns_constrains_tac 1];
11.80 +
11.81 +
11.82 +(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
11.83 + sends messages containing X! **)
11.84 +
11.85 +(*Spy never sees another agent's private key! (unless it's bad at start)*)
11.86 +Goal "Nprg : Always {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
11.87 +by (ns_induct_tac 1);
11.88 +by (Blast_tac 1);
11.89 +qed "Spy_see_priK";
11.90 +Addsimps [impOfAlways Spy_see_priK];
11.91 +
11.92 +Goal "Nprg : Always {s. (Key (priK A) : analz (spies s)) = (A : bad)}";
11.93 +by (rtac (Always_reachable RS Always_weaken) 1);
11.94 +by Auto_tac;
11.95 +qed "Spy_analz_priK";
11.96 +Addsimps [impOfAlways Spy_analz_priK];
11.97 +
11.98 +(**
11.99 +AddSDs [Spy_see_priK RSN (2, rev_iffD1),
11.100 + Spy_analz_priK RSN (2, rev_iffD1)];
11.101 +**)
11.102 +
11.103 +
11.104 +(**** Authenticity properties obtained from NS2 ****)
11.105 +
11.106 +(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
11.107 + is secret. (Honest users generate fresh nonces.)*)
11.108 +Goal
11.109 + "Nprg \
11.110 +\ : Always {s. Nonce NA ~: analz (spies s) --> \
11.111 +\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies s) --> \
11.112 +\ Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies s)}";
11.113 +by (ns_induct_tac 1);
11.114 +by (ALLGOALS Blast_tac);
11.115 +qed "no_nonce_NS1_NS2";
11.116 +
11.117 +(*Adding it to the claset slows down proofs...*)
11.118 +val nonce_NS1_NS2_E = impOfAlways no_nonce_NS1_NS2 RSN (2, rev_notE);
11.119 +
11.120 +
11.121 +(*Unicity for NS1: nonce NA identifies agents A and B*)
11.122 +Goal "Nprg \
11.123 +\ : Always {s. Nonce NA ~: analz (spies s) --> \
11.124 +\ Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies s) --> \
11.125 +\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies s) --> \
11.126 +\ A=A' & B=B'}";
11.127 +by (ns_induct_tac 1);
11.128 +by Auto_tac;
11.129 +(*Fake, NS1 are non-trivial*)
11.130 +val unique_NA_lemma = result();
11.131 +
11.132 +(*Unicity for NS1: nonce NA identifies agents A and B*)
11.133 +Goal "[| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies s); \
11.134 +\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies s); \
11.135 +\ Nonce NA ~: analz (spies s); \
11.136 +\ s : reachable Nprg |] \
11.137 +\ ==> A=A' & B=B'";
11.138 +by (blast_tac (claset() addDs [impOfAlways unique_NA_lemma]) 1);
11.139 +qed "unique_NA";
11.140 +
11.141 +
11.142 +(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
11.143 +Goal "[| A ~: bad; B ~: bad |] \
11.144 +\ ==> Nprg : Always \
11.145 +\ {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set s \
11.146 +\ --> Nonce NA ~: analz (spies s)}";
11.147 +by (ns_induct_tac 1);
11.148 +(*NS3*)
11.149 +by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4);
11.150 +(*NS2*)
11.151 +by (blast_tac (claset() addDs [unique_NA]) 3);
11.152 +(*NS1*)
11.153 +by (Blast_tac 2);
11.154 +(*Fake*)
11.155 +by (spy_analz_tac 1);
11.156 +qed "Spy_not_see_NA";
11.157 +
11.158 +
11.159 +(*Authentication for A: if she receives message 2 and has used NA
11.160 + to start a run, then B has sent message 2.*)
11.161 +val prems =
11.162 +goal thy "[| A ~: bad; B ~: bad |] \
11.163 +\ ==> Nprg : Always \
11.164 +\ {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set s & \
11.165 +\ Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts (knows Spy s) \
11.166 +\ --> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set s}";
11.167 + (*insert an invariant for use in some of the subgoals*)
11.168 +by (cut_facts_tac ([prems MRS Spy_not_see_NA] @ prems) 1);
11.169 +by (ns_induct_tac 1);
11.170 +by (ALLGOALS Clarify_tac);
11.171 +(*NS2*)
11.172 +by (blast_tac (claset() addDs [unique_NA]) 3);
11.173 +(*NS1*)
11.174 +by (Blast_tac 2);
11.175 +(*Fake*)
11.176 +by (Blast_tac 1);
11.177 +qed "A_trusts_NS2";
11.178 +
11.179 +
11.180 +(*If the encrypted message appears then it originated with Alice in NS1*)
11.181 +Goal "Nprg : Always \
11.182 +\ {s. Nonce NA ~: analz (spies s) --> \
11.183 +\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies s) \
11.184 +\ --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set s}";
11.185 +by (ns_induct_tac 1);
11.186 +by (Blast_tac 1);
11.187 +qed "B_trusts_NS1";
11.188 +
11.189 +
11.190 +
11.191 +(**** Authenticity properties obtained from NS2 ****)
11.192 +
11.193 +(*Unicity for NS2: nonce NB identifies nonce NA and agent A
11.194 + [proof closely follows that for unique_NA] *)
11.195 +Goal
11.196 + "Nprg \
11.197 +\ : Always {s. Nonce NB ~: analz (spies s) --> \
11.198 +\ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies s) --> \
11.199 +\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies s) --> \
11.200 +\ A=A' & NA=NA'}";
11.201 +by (ns_induct_tac 1);
11.202 +by Auto_tac;
11.203 +(*Fake, NS2 are non-trivial*)
11.204 +val unique_NB_lemma = result();
11.205 +
11.206 +Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(spies s); \
11.207 +\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies s); \
11.208 +\ Nonce NB ~: analz (spies s); \
11.209 +\ s : reachable Nprg |] \
11.210 +\ ==> A=A' & NA=NA'";
11.211 +by (blast_tac (claset() addDs [impOfAlways unique_NB_lemma]) 1);
11.212 +qed "unique_NB";
11.213 +
11.214 +
11.215 +(*NB remains secret PROVIDED Alice never responds with round 3*)
11.216 +Goal "[| A ~: bad; B ~: bad |] \
11.217 +\ ==> Nprg : Always \
11.218 +\ {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s & \
11.219 +\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set s) \
11.220 +\ --> Nonce NB ~: analz (spies s)}";
11.221 +by (ns_induct_tac 1);
11.222 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
11.223 +by (ALLGOALS Clarify_tac);
11.224 +(*NS3: because NB determines A*)
11.225 +by (blast_tac (claset() addDs [unique_NB]) 4);
11.226 +(*NS2: by freshness and unicity of NB*)
11.227 +by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
11.228 +(*NS1: by freshness*)
11.229 +by (Blast_tac 2);
11.230 +(*Fake*)
11.231 +by (spy_analz_tac 1);
11.232 +qed "Spy_not_see_NB";
11.233 +
11.234 +
11.235 +
11.236 +(*Authentication for B: if he receives message 3 and has used NB
11.237 + in message 2, then A has sent message 3--to somebody....*)
11.238 +val prems =
11.239 +goal thy "[| A ~: bad; B ~: bad |] \
11.240 +\ ==> Nprg : Always \
11.241 +\ {s. Crypt (pubK B) (Nonce NB) : parts (spies s) & \
11.242 +\ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s \
11.243 +\ --> (EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set s)}";
11.244 + (*insert an invariant for use in some of the subgoals*)
11.245 +by (cut_facts_tac ([prems MRS Spy_not_see_NB] @ prems) 1);
11.246 +by (ns_induct_tac 1);
11.247 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
11.248 +by (ALLGOALS Clarify_tac);
11.249 +(*NS3: because NB determines A (this use of unique_NB is more robust) *)
11.250 +by (blast_tac (claset() addIs [unique_NB RS conjunct1]) 3);
11.251 +(*NS1: by freshness*)
11.252 +by (Blast_tac 2);
11.253 +(*Fake*)
11.254 +by (Blast_tac 1);
11.255 +qed "B_trusts_NS3";
11.256 +
11.257 +
11.258 +(*Can we strengthen the secrecy theorem? NO*)
11.259 +Goal "[| A ~: bad; B ~: bad |] \
11.260 +\ ==> Nprg : Always \
11.261 +\ {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s \
11.262 +\ --> Nonce NB ~: analz (spies s)}";
11.263 +by (ns_induct_tac 1);
11.264 +by (ALLGOALS Clarify_tac);
11.265 +(*NS2: by freshness and unicity of NB*)
11.266 +by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
11.267 +(*NS1: by freshness*)
11.268 +by (Blast_tac 2);
11.269 +(*Fake*)
11.270 +by (spy_analz_tac 1);
11.271 +(*NS3: unicity of NB identifies A and NA, but not B*)
11.272 +by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1
11.273 + THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1));
11.274 +by Auto_tac;
11.275 +by (rename_tac "s B' C" 1);
11.276 +
11.277 +(*
11.278 +THIS IS THE ATTACK!
11.279 +[| A ~: bad; B ~: bad |]
11.280 +==> Nprg
11.281 + : Always
11.282 + {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s -->
11.283 + Nonce NB ~: analz (knows Spy s)}
11.284 + 1. !!s B' C.
11.285 + [| A ~: bad; B ~: bad; s : reachable Nprg;
11.286 + Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) : set s;
11.287 + Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s;
11.288 + C : bad; Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s;
11.289 + Nonce NB ~: analz (knows Spy s) |]
11.290 + ==> False
11.291 +*)
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Mon Mar 05 15:47:11 2001 +0100
12.3 @@ -0,0 +1,59 @@
12.4 +(* Title: HOL/Auth/NSP_Bad
12.5 + ID: $Id$
12.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
12.7 + Copyright 1996 University of Cambridge
12.8 +
12.9 +add_path "../Auth"; use_thy"NSP_Bad";
12.10 +
12.11 +Security protocols in UNITY: Needham-Schroeder, public keys (flawed version).
12.12 +
12.13 +Original file is ../Auth/NS_Public_Bad
12.14 +*)
12.15 +
12.16 +NSP_Bad = Public + Constrains +
12.17 +
12.18 +types state = event list
12.19 +
12.20 +constdefs
12.21 +
12.22 + (*The spy MAY say anything he CAN say. We do not expect him to
12.23 + invent new nonces here, but he can also use NS1. Common to
12.24 + all similar protocols.*)
12.25 + Fake :: "(state*state) set"
12.26 + "Fake == {(s,s').
12.27 + EX B X. s' = Says Spy B X # s
12.28 + & X: synth (analz (spies s))}"
12.29 +
12.30 + (*The numeric suffixes on A identify the rule*)
12.31 +
12.32 + (*Alice initiates a protocol run, sending a nonce to Bob*)
12.33 + NS1 :: "(state*state) set"
12.34 + "NS1 == {(s1,s').
12.35 + EX A1 B NA.
12.36 + s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
12.37 + & Nonce NA ~: used s1}"
12.38 +
12.39 + (*Bob responds to Alice's message with a further nonce*)
12.40 + NS2 :: "(state*state) set"
12.41 + "NS2 == {(s2,s').
12.42 + EX A' A2 B NA NB.
12.43 + s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
12.44 + & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) : set s2
12.45 + & Nonce NB ~: used s2}"
12.46 +
12.47 + (*Alice proves her existence by sending NB back to Bob.*)
12.48 + NS3 :: "(state*state) set"
12.49 + "NS3 == {(s3,s').
12.50 + EX A3 B' B NA NB.
12.51 + s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3
12.52 + & Says A3 B (Crypt (pubK B) {|Nonce NA, Agent A3|}) : set s3
12.53 + & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) : set s3}"
12.54 +
12.55 +
12.56 +
12.57 +constdefs
12.58 + Nprg :: state program
12.59 + (*Initial trace is empty*)
12.60 + "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
12.61 +
12.62 +end
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/HOL/UNITY/Simple/Network.ML Mon Mar 05 15:47:11 2001 +0100
13.3 @@ -0,0 +1,59 @@
13.4 +(* Title: HOL/UNITY/Network
13.5 + ID: $Id$
13.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
13.7 + Copyright 1998 University of Cambridge
13.8 +
13.9 +The Communication Network
13.10 +
13.11 +From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
13.12 +*)
13.13 +
13.14 +val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] =
13.15 +Goalw [stable_def]
13.16 + "[| !! m. F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \
13.17 +\ !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \
13.18 +\ !! m proc. F : stable {s. m <= s(proc,Sent)}; \
13.19 +\ !! n proc. F : stable {s. n <= s(proc,Rcvd)}; \
13.20 +\ !! m proc. F : {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} co \
13.21 +\ {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
13.22 +\ !! n proc. F : {s. s(proc,Idle) = 1 & s(proc,Sent) = n} co \
13.23 +\ {s. s(proc,Sent) = n} \
13.24 +\ |] ==> F : stable {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
13.25 +\ s(Aproc,Sent) = s(Bproc,Rcvd) & \
13.26 +\ s(Bproc,Sent) = s(Aproc,Rcvd) & \
13.27 +\ s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
13.28 +
13.29 +val sent_nondec_A = read_instantiate [("proc","Aproc")] sent_nondec;
13.30 +val sent_nondec_B = read_instantiate [("proc","Bproc")] sent_nondec;
13.31 +val rcvd_nondec_A = read_instantiate [("proc","Aproc")] rcvd_nondec;
13.32 +val rcvd_nondec_B = read_instantiate [("proc","Bproc")] rcvd_nondec;
13.33 +val rcvd_idle_A = read_instantiate [("proc","Aproc")] rcvd_idle;
13.34 +val rcvd_idle_B = read_instantiate [("proc","Bproc")] rcvd_idle;
13.35 +val sent_idle_A = read_instantiate [("proc","Aproc")] sent_idle;
13.36 +val sent_idle_B = read_instantiate [("proc","Bproc")] sent_idle;
13.37 +
13.38 +val rs_AB = [rsA, rsB] MRS constrains_Int;
13.39 +val sent_nondec_AB = [sent_nondec_A, sent_nondec_B] MRS constrains_Int;
13.40 +val rcvd_nondec_AB = [rcvd_nondec_A, rcvd_nondec_B] MRS constrains_Int;
13.41 +val rcvd_idle_AB = [rcvd_idle_A, rcvd_idle_B] MRS constrains_Int;
13.42 +val sent_idle_AB = [sent_idle_A, sent_idle_B] MRS constrains_Int;
13.43 +val nondec_AB = [sent_nondec_AB, rcvd_nondec_AB] MRS constrains_Int;
13.44 +val idle_AB = [rcvd_idle_AB, sent_idle_AB] MRS constrains_Int;
13.45 +val nondec_idle = [nondec_AB, idle_AB] MRS constrains_Int;
13.46 +
13.47 +by (rtac constrainsI 1);
13.48 +by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
13.49 +by (assume_tac 1);
13.50 +by (ALLGOALS Asm_full_simp_tac);
13.51 +by (blast_tac (HOL_cs addIs [order_refl]) 1);
13.52 +by (Clarify_tac 1);
13.53 +by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
13.54 + "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);
13.55 +by (REPEAT
13.56 + (blast_tac (claset() addIs [order_antisym, le_trans, eq_imp_le]) 2));
13.57 +by (Asm_simp_tac 1);
13.58 +result();
13.59 +
13.60 +
13.61 +
13.62 +
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/HOL/UNITY/Simple/Network.thy Mon Mar 05 15:47:11 2001 +0100
14.3 @@ -0,0 +1,21 @@
14.4 +(* Title: HOL/UNITY/Network
14.5 + ID: $Id$
14.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
14.7 + Copyright 1998 University of Cambridge
14.8 +
14.9 +The Communication Network
14.10 +
14.11 +From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
14.12 +*)
14.13 +
14.14 +Network = UNITY +
14.15 +
14.16 +(*The state assigns a number to each process variable*)
14.17 +
14.18 +datatype pvar = Sent | Rcvd | Idle
14.19 +
14.20 +datatype pname = Aproc | Bproc
14.21 +
14.22 +types state = "pname * pvar => nat"
14.23 +
14.24 +end
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/HOL/UNITY/Simple/README.html Mon Mar 05 15:47:11 2001 +0100
15.3 @@ -0,0 +1,36 @@
15.4 +<!-- $Id$ -->
15.5 +<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
15.6 +
15.7 +<H2>UNITY: Examples Involving Single Programs</H2>
15.8 +
15.9 +<P> The directory presents verification examples that do not involve program
15.10 +composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'':
15.11 +<UL>
15.12 +<LI>common meeting time (<A HREF="Common.thy"><CODE>Common.thy</CODE></A>)
15.13 +
15.14 +<LI>the token ring (<A HREF="Token.thy"><CODE>Token.thy</CODE></A>)
15.15 +
15.16 +<LI>the communication network
15.17 +(<A HREF="Network.thy"><CODE>Network.thy</CODE></A>)
15.18 +
15.19 +<LI>the lift controller (a standard benchmark) (<A HREF="Lift.thy"><CODE>Lift.thy</CODE></A>)
15.20 +
15.21 +<LI>a mutual exclusion algorithm (<A HREF="Mutex.thy"><CODE>Mutex.thy</CODE></A>)
15.22 +
15.23 +<LI><EM>n</EM>-process deadlock
15.24 +(<A HREF="Deadlock.thy"><CODE>Deadlock.thy</CODE></A>)
15.25 +
15.26 +<LI>unordered channel (<A HREF="Channel.thy"><CODE>Channel.thy</CODE></A>)
15.27 +
15.28 +<LI>reachability in directed graphs (section 6.4 of the book) (<A
15.29 +HREF="Reach.thy"><CODE>Reach.thy</CODE></A> and
15.30 +<A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>)
15.31 +</UL>
15.32 +
15.33 +<HR>
15.34 +<P>Last modified on $Date$
15.35 +
15.36 +<ADDRESS>
15.37 +<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
15.38 +</ADDRESS>
15.39 +</BODY></HTML>
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/HOL/UNITY/Simple/Reach.ML Mon Mar 05 15:47:11 2001 +0100
16.3 @@ -0,0 +1,142 @@
16.4 +(* Title: HOL/UNITY/Reach.thy
16.5 + ID: $Id$
16.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
16.7 + Copyright 1998 University of Cambridge
16.8 +
16.9 +Reachability in Directed Graphs. From Chandy and Misra, section 6.4.
16.10 + [ this example took only four days!]
16.11 +*)
16.12 +
16.13 +(*TO SIMPDATA.ML?? FOR CLASET?? *)
16.14 +val major::prems = goal thy
16.15 + "[| if P then Q else R; \
16.16 +\ [| P; Q |] ==> S; \
16.17 +\ [| ~ P; R |] ==> S |] ==> S";
16.18 +by (cut_facts_tac [major] 1);
16.19 +by (blast_tac (claset() addSDs [if_bool_eq_disj RS iffD1] addIs prems) 1);
16.20 +qed "ifE";
16.21 +
16.22 +AddSEs [ifE];
16.23 +
16.24 +
16.25 +Addsimps [Rprg_def RS def_prg_Init];
16.26 +program_defs_ref := [Rprg_def];
16.27 +
16.28 +Addsimps [simp_of_act asgt_def];
16.29 +
16.30 +(*All vertex sets are finite*)
16.31 +AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
16.32 +
16.33 +Addsimps [simp_of_set reach_invariant_def];
16.34 +
16.35 +Goal "Rprg : Always reach_invariant";
16.36 +by (always_tac 1);
16.37 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
16.38 +qed "reach_invariant";
16.39 +
16.40 +
16.41 +(*** Fixedpoint ***)
16.42 +
16.43 +(*If it reaches a fixedpoint, it has found a solution*)
16.44 +Goalw [fixedpoint_def]
16.45 + "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
16.46 +by (rtac equalityI 1);
16.47 +by (auto_tac (claset() addSIs [ext], simpset()));
16.48 +by (blast_tac (claset() addIs [rtrancl_trans]) 2);
16.49 +by (etac rtrancl_induct 1);
16.50 +by Auto_tac;
16.51 +qed "fixedpoint_invariant_correct";
16.52 +
16.53 +Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
16.54 + "FP Rprg <= fixedpoint";
16.55 +by Auto_tac;
16.56 +by (dtac bspec 1 THEN atac 1);
16.57 +by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
16.58 +by (dtac fun_cong 1);
16.59 +by Auto_tac;
16.60 +val lemma1 = result();
16.61 +
16.62 +Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
16.63 + "fixedpoint <= FP Rprg";
16.64 +by (auto_tac (claset() addSIs [ext], simpset()));
16.65 +val lemma2 = result();
16.66 +
16.67 +Goal "FP Rprg = fixedpoint";
16.68 +by (rtac ([lemma1,lemma2] MRS equalityI) 1);
16.69 +qed "FP_fixedpoint";
16.70 +
16.71 +
16.72 +(*If we haven't reached a fixedpoint then there is some edge for which u but
16.73 + not v holds. Progress will be proved via an ENSURES assertion that the
16.74 + metric will decrease for each suitable edge. A union over all edges proves
16.75 + a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
16.76 + *)
16.77 +
16.78 +Goal "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
16.79 +by (simp_tac (simpset() addsimps
16.80 + [Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, Rprg_def]) 1);
16.81 +by Auto_tac;
16.82 +by (rtac fun_upd_idem 1);
16.83 +by Auto_tac;
16.84 +by (force_tac (claset() addSIs [rev_bexI],
16.85 + simpset() addsimps [fun_upd_idem_iff]) 1);
16.86 +qed "Compl_fixedpoint";
16.87 +
16.88 +Goal "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
16.89 +by (simp_tac (simpset() addsimps [Diff_eq, Compl_fixedpoint]) 1);
16.90 +by (Blast_tac 1);
16.91 +qed "Diff_fixedpoint";
16.92 +
16.93 +
16.94 +(*** Progress ***)
16.95 +
16.96 +Goalw [metric_def] "~ s x ==> Suc (metric (s(x:=True))) = metric s";
16.97 +by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1);
16.98 +by (Force_tac 2);
16.99 +by (asm_full_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1);
16.100 +qed "Suc_metric";
16.101 +
16.102 +Goal "~ s x ==> metric (s(x:=True)) < metric s";
16.103 +by (etac (Suc_metric RS subst) 1);
16.104 +by (Blast_tac 1);
16.105 +qed "metric_less";
16.106 +AddSIs [metric_less];
16.107 +
16.108 +Goal "metric (s(y:=s x | s y)) <= metric s";
16.109 +by (case_tac "s x --> s y" 1);
16.110 +by (auto_tac (claset() addIs [less_imp_le],
16.111 + simpset() addsimps [fun_upd_idem]));
16.112 +qed "metric_le";
16.113 +
16.114 +Goal "Rprg : ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))";
16.115 +by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
16.116 +by (rtac LeadsTo_UN 1);
16.117 +by Auto_tac;
16.118 +by (ensures_tac "asgt a b" 1);
16.119 +by (Blast_tac 2);
16.120 +by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
16.121 +by (dtac (metric_le RS order_antisym) 1);
16.122 +by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)],
16.123 + simpset()));
16.124 +qed "LeadsTo_Diff_fixedpoint";
16.125 +
16.126 +Goal "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)";
16.127 +by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
16.128 + subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
16.129 +by Auto_tac;
16.130 +qed "LeadsTo_Un_fixedpoint";
16.131 +
16.132 +
16.133 +(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
16.134 +Goal "Rprg : UNIV LeadsTo fixedpoint";
16.135 +by (rtac LessThan_induct 1);
16.136 +by Auto_tac;
16.137 +by (rtac LeadsTo_Un_fixedpoint 1);
16.138 +qed "LeadsTo_fixedpoint";
16.139 +
16.140 +Goal "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }";
16.141 +by (stac (fixedpoint_invariant_correct RS sym) 1);
16.142 +by (rtac ([reach_invariant, LeadsTo_fixedpoint]
16.143 + MRS Always_LeadsTo_weaken) 1);
16.144 +by Auto_tac;
16.145 +qed "LeadsTo_correct";
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/HOL/UNITY/Simple/Reach.thy Mon Mar 05 15:47:11 2001 +0100
17.3 @@ -0,0 +1,43 @@
17.4 +(* Title: HOL/UNITY/Reach.thy
17.5 + ID: $Id$
17.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
17.7 + Copyright 1998 University of Cambridge
17.8 +
17.9 +Reachability in Directed Graphs. From Chandy and Misra, section 6.4.
17.10 +*)
17.11 +
17.12 +Reach = FP + SubstAx +
17.13 +
17.14 +types vertex
17.15 + state = "vertex=>bool"
17.16 +
17.17 +arities vertex :: term
17.18 +
17.19 +consts
17.20 + init :: "vertex"
17.21 +
17.22 + edges :: "(vertex*vertex) set"
17.23 +
17.24 +constdefs
17.25 +
17.26 + asgt :: "[vertex,vertex] => (state*state) set"
17.27 + "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
17.28 +
17.29 + Rprg :: state program
17.30 + "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)"
17.31 +
17.32 + reach_invariant :: state set
17.33 + "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
17.34 +
17.35 + fixedpoint :: state set
17.36 + "fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
17.37 +
17.38 + metric :: state => nat
17.39 + "metric s == card {v. ~ s v}"
17.40 +
17.41 +rules
17.42 +
17.43 + (*We assume that the set of vertices is finite*)
17.44 + finite_graph "finite (UNIV :: vertex set)"
17.45 +
17.46 +end
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/HOL/UNITY/Simple/Reachability.ML Mon Mar 05 15:47:11 2001 +0100
18.3 @@ -0,0 +1,308 @@
18.4 +(* Title: HOL/UNITY/Reachability
18.5 + ID: $Id$
18.6 + Author: Tanja Vos, Cambridge University Computer Laboratory
18.7 + Copyright 2000 University of Cambridge
18.8 +
18.9 +Reachability in Graphs
18.10 +
18.11 +From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
18.12 +*)
18.13 +
18.14 +bind_thm("E_imp_in_V_L", Graph2 RS conjunct1);
18.15 +bind_thm("E_imp_in_V_R", Graph2 RS conjunct2);
18.16 +
18.17 +Goal "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v";
18.18 +by (rtac (MA7 RS PSP_Stable RS LeadsTo_weaken_L) 1);
18.19 +by (rtac MA6 3);
18.20 +by (auto_tac (claset(), simpset() addsimps [E_imp_in_V_L, E_imp_in_V_R]));
18.21 +qed "lemma2";
18.22 +
18.23 +Goal "(v,w) : E ==> F : reachable v LeadsTo reachable w";
18.24 +by (rtac (MA4 RS Always_LeadsTo_weaken) 1);
18.25 +by (rtac lemma2 2);
18.26 +by (auto_tac (claset(), simpset() addsimps [nmsg_eq_def, nmsg_gt_def]));
18.27 +qed "Induction_base";
18.28 +
18.29 +Goal "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w";
18.30 +by (etac REACHABLE.induct 1);
18.31 +by (rtac subset_imp_LeadsTo 1);
18.32 +by (Blast_tac 1);
18.33 +by (blast_tac (claset() addIs [LeadsTo_Trans, Induction_base]) 1);
18.34 +qed "REACHABLE_LeadsTo_reachable";
18.35 +
18.36 +Goal "F : {s. (root,v) : REACHABLE} LeadsTo reachable v";
18.37 +by (rtac single_LeadsTo_I 1);
18.38 +by (full_simp_tac (simpset() addsplits [split_if_asm]) 1);
18.39 +by (rtac (MA1 RS Always_LeadsToI) 1);
18.40 +by (etac (REACHABLE_LeadsTo_reachable RS LeadsTo_weaken_L) 1);
18.41 +by Auto_tac;
18.42 +qed "Detects_part1";
18.43 +
18.44 +
18.45 +Goalw [Detects_def]
18.46 + "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}";
18.47 +by Auto_tac;
18.48 +by (blast_tac (claset() addIs [MA2 RS Always_weaken]) 2);
18.49 +by (rtac (Detects_part1 RS LeadsTo_weaken_L) 1);
18.50 +by (Blast_tac 1);
18.51 +qed "Reachability_Detected";
18.52 +
18.53 +
18.54 +Goal "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})";
18.55 +by (etac (Reachability_Detected RS Detects_Imp_LeadstoEQ) 1);
18.56 +qed "LeadsTo_Reachability";
18.57 +
18.58 +(* ------------------------------------ *)
18.59 +
18.60 +(* Some lemmas about <==> *)
18.61 +
18.62 +Goalw [Equality_def]
18.63 + "(reachable v <==> {s. (root,v) : REACHABLE}) = \
18.64 +\ {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
18.65 +by (Blast_tac 1);
18.66 +qed "Eq_lemma1";
18.67 +
18.68 +
18.69 +Goalw [Equality_def]
18.70 + "(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) = \
18.71 +\ {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
18.72 +by Auto_tac;
18.73 +qed "Eq_lemma2";
18.74 +
18.75 +(* ------------------------------------ *)
18.76 +
18.77 +
18.78 +(* Some lemmas about final (I don't need all of them!) *)
18.79 +
18.80 +Goalw [final_def, Equality_def]
18.81 + "(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) & \
18.82 +\ s : nmsg_eq 0 (v,w)}) \
18.83 +\ <= final";
18.84 +by Auto_tac;
18.85 +by (ftac E_imp_in_V_R 1);
18.86 +by (ftac E_imp_in_V_L 1);
18.87 +by (Blast_tac 1);
18.88 +qed "final_lemma1";
18.89 +
18.90 +Goalw [final_def, Equality_def]
18.91 + "E~={} \
18.92 +\ ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))} \
18.93 +\ Int nmsg_eq 0 e) <= final";
18.94 +by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
18.95 +by (ftac E_imp_in_V_L 1);
18.96 +by (Blast_tac 1);
18.97 +qed "final_lemma2";
18.98 +
18.99 +Goal "E~={} \
18.100 +\ ==> (INT v: V. INT e: E. \
18.101 +\ (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
18.102 +\ <= final";
18.103 +by (ftac final_lemma2 1);
18.104 +by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
18.105 +qed "final_lemma3";
18.106 +
18.107 +
18.108 +Goal "E~={} \
18.109 +\ ==> (INT v: V. INT e: E. \
18.110 +\ {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e) \
18.111 +\ = final";
18.112 +by (rtac subset_antisym 1);
18.113 +by (etac final_lemma2 1);
18.114 +by (rewrite_goals_tac [final_def,Equality_def]);
18.115 +by (Blast_tac 1);
18.116 +qed "final_lemma4";
18.117 +
18.118 +Goal "E~={} \
18.119 +\ ==> (INT v: V. INT e: E. \
18.120 +\ ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
18.121 +\ = final";
18.122 +by (ftac final_lemma4 1);
18.123 +by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
18.124 +qed "final_lemma5";
18.125 +
18.126 +
18.127 +Goal "(INT v: V. INT w: V. \
18.128 +\ (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)) \
18.129 +\ <= final";
18.130 +by (simp_tac (simpset() addsimps [Eq_lemma2, Int_def]) 1);
18.131 +by (rtac final_lemma1 1);
18.132 +qed "final_lemma6";
18.133 +
18.134 +
18.135 +Goalw [final_def]
18.136 + "final = \
18.137 +\ (INT v: V. INT w: V. \
18.138 +\ ((reachable v) <==> {s. (root,v) : REACHABLE}) Int \
18.139 +\ (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))";
18.140 +by (rtac subset_antisym 1);
18.141 +by (Blast_tac 1);
18.142 +by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
18.143 +by (ftac E_imp_in_V_R 1);
18.144 +by (ftac E_imp_in_V_L 1);
18.145 +by (Blast_tac 1);
18.146 +qed "final_lemma7";
18.147 +
18.148 +(* ------------------------------------ *)
18.149 +
18.150 +
18.151 +(* ------------------------------------ *)
18.152 +
18.153 +(* Stability theorems *)
18.154 +
18.155 +
18.156 +Goal "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)";
18.157 +by (dtac (MA2 RS AlwaysD) 1);
18.158 +by Auto_tac;
18.159 +qed "not_REACHABLE_imp_Stable_not_reachable";
18.160 +
18.161 +Goal "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})";
18.162 +by (simp_tac (simpset() addsimps [Equality_def, Eq_lemma2]) 1);
18.163 +by (blast_tac (claset() addIs [MA6,not_REACHABLE_imp_Stable_not_reachable]) 1);
18.164 +qed "Stable_reachable_EQ_R";
18.165 +
18.166 +
18.167 +Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
18.168 + "((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
18.169 +\ <= A Un nmsg_eq 0 (v,w)";
18.170 +by Auto_tac;
18.171 +qed "lemma4";
18.172 +
18.173 +
18.174 +Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
18.175 + "reachable v Int nmsg_eq 0 (v,w) = \
18.176 +\ ((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int \
18.177 +\ (reachable v Int nmsg_lte 0 (v,w)))";
18.178 +by Auto_tac;
18.179 +qed "lemma5";
18.180 +
18.181 +Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
18.182 + "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v";
18.183 +by Auto_tac;
18.184 +qed "lemma6";
18.185 +
18.186 +Goal "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))";
18.187 +by (rtac ([MA5, MA3] MRS Always_Int_I RS Always_weaken) 1);
18.188 +by (rtac lemma4 5);
18.189 +by Auto_tac;
18.190 +qed "Always_reachable_OR_nmsg_0";
18.191 +
18.192 +Goal "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))";
18.193 +by (stac lemma5 1);
18.194 +by (blast_tac (claset() addIs [MA5, Always_imp_Stable RS Stable_Int, MA6b]) 1);
18.195 +qed "Stable_reachable_AND_nmsg_0";
18.196 +
18.197 +Goal "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)";
18.198 +by (blast_tac (claset() addSIs [Always_weaken RS Always_imp_Stable,
18.199 + lemma6, MA3]) 1);
18.200 +qed "Stable_nmsg_0_OR_reachable";
18.201 +
18.202 +Goal "[| v : V; w:V; (root,v) ~: REACHABLE |] \
18.203 +\ ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))";
18.204 +by (rtac ([MA2 RS Always_imp_Stable, Stable_nmsg_0_OR_reachable] MRS
18.205 + Stable_Int RS Stable_eq) 1);
18.206 +by (Blast_tac 4);
18.207 +by Auto_tac;
18.208 +qed "not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0";
18.209 +
18.210 +Goal "[| v : V; w:V |] \
18.211 +\ ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int \
18.212 +\ nmsg_eq 0 (v,w))";
18.213 +by (asm_simp_tac
18.214 + (simpset() addsimps [Equality_def, Eq_lemma2,
18.215 + not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0,
18.216 + Stable_reachable_AND_nmsg_0]) 1);
18.217 +qed "Stable_reachable_EQ_R_AND_nmsg_0";
18.218 +
18.219 +
18.220 +(* ------------------------------------ *)
18.221 +
18.222 +
18.223 +(* LeadsTo final predicate (Exercise 11.2 page 274) *)
18.224 +
18.225 +Goal "UNIV <= (INT v: V. UNIV)";
18.226 +by (Blast_tac 1);
18.227 +val UNIV_lemma = result();
18.228 +
18.229 +val UNIV_LeadsTo_completion =
18.230 + [Finite_stable_completion, UNIV_lemma] MRS LeadsTo_weaken_L;
18.231 +
18.232 +Goalw [final_def] "E={} ==> F : UNIV LeadsTo final";
18.233 +by (Asm_full_simp_tac 1);
18.234 +by (rtac UNIV_LeadsTo_completion 1);
18.235 +by Safe_tac;
18.236 +by (etac (simplify (simpset()) LeadsTo_Reachability) 1);
18.237 +by (dtac Stable_reachable_EQ_R 1);
18.238 +by (Asm_full_simp_tac 1);
18.239 +qed "LeadsTo_final_E_empty";
18.240 +
18.241 +
18.242 +Goal "[| v : V; w:V |] \
18.243 +\ ==> F : UNIV LeadsTo \
18.244 +\ ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))";
18.245 +by (rtac (LeadsTo_Reachability RS LeadsTo_Trans) 1);
18.246 +by (Blast_tac 1);
18.247 +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);
18.248 +by (Asm_full_simp_tac 1);
18.249 +by (rtac PSP_Stable2 1);
18.250 +by (rtac MA7 1);
18.251 +by (rtac Stable_reachable_EQ_R 3);
18.252 +by Auto_tac;
18.253 +qed "Leadsto_reachability_AND_nmsg_0";
18.254 +
18.255 +
18.256 +Goal "E~={} ==> F : UNIV LeadsTo final";
18.257 +by (rtac ([LeadsTo_weaken_R, UNIV_lemma] MRS LeadsTo_weaken_L) 1);
18.258 +by (rtac final_lemma6 2);
18.259 +by (rtac Finite_stable_completion 1);
18.260 +by (Blast_tac 1);
18.261 +by (rtac UNIV_LeadsTo_completion 1);
18.262 +by (REPEAT
18.263 + (blast_tac (claset() addIs [Stable_INT,
18.264 + Stable_reachable_EQ_R_AND_nmsg_0,
18.265 + Leadsto_reachability_AND_nmsg_0]) 1));
18.266 +qed "LeadsTo_final_E_NOT_empty";
18.267 +
18.268 +
18.269 +Goal "F : UNIV LeadsTo final";
18.270 +by (case_tac "E={}" 1);
18.271 +by (rtac LeadsTo_final_E_NOT_empty 2);
18.272 +by (rtac LeadsTo_final_E_empty 1);
18.273 +by Auto_tac;
18.274 +qed "LeadsTo_final";
18.275 +
18.276 +(* ------------------------------------ *)
18.277 +
18.278 +(* Stability of final (Exercise 11.2 page 274) *)
18.279 +
18.280 +Goalw [final_def] "E={} ==> F : Stable final";
18.281 +by (Asm_full_simp_tac 1);
18.282 +by (rtac Stable_INT 1);
18.283 +by (dtac Stable_reachable_EQ_R 1);
18.284 +by (Asm_full_simp_tac 1);
18.285 +qed "Stable_final_E_empty";
18.286 +
18.287 +
18.288 +Goal "E~={} ==> F : Stable final";
18.289 +by (stac final_lemma7 1);
18.290 +by (rtac Stable_INT 1);
18.291 +by (rtac Stable_INT 1);
18.292 +by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
18.293 +by Safe_tac;
18.294 +by (rtac Stable_eq 1);
18.295 +by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)} Int nmsg_eq 0 (v,w)) = \
18.296 +\ ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- UNIV Un nmsg_eq 0 (v,w)))" 2);
18.297 +by (Blast_tac 2); by (Blast_tac 2);
18.298 +by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R_AND_nmsg_0) 1);
18.299 +by (Blast_tac 1);by (Blast_tac 1);
18.300 +by (rtac Stable_eq 1);
18.301 +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);
18.302 +by (Blast_tac 2); by (Blast_tac 2);
18.303 +by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R) 1);
18.304 +by Auto_tac;
18.305 +qed "Stable_final_E_NOT_empty";
18.306 +
18.307 +Goal "F : Stable final";
18.308 +by (case_tac "E={}" 1);
18.309 +by (blast_tac (claset() addIs [Stable_final_E_NOT_empty]) 2);
18.310 +by (blast_tac (claset() addIs [Stable_final_E_empty]) 1);
18.311 +qed "Stable_final";
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/HOL/UNITY/Simple/Reachability.thy Mon Mar 05 15:47:11 2001 +0100
19.3 @@ -0,0 +1,72 @@
19.4 +(* Title: HOL/UNITY/Reachability
19.5 + ID: $Id$
19.6 + Author: Tanja Vos, Cambridge University Computer Laboratory
19.7 + Copyright 2000 University of Cambridge
19.8 +
19.9 +Reachability in Graphs
19.10 +
19.11 +From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
19.12 +*)
19.13 +
19.14 +Reachability = Detects +
19.15 +
19.16 +types edge = "(vertex*vertex)"
19.17 +
19.18 +record state =
19.19 + reach :: vertex => bool
19.20 + nmsg :: edge => nat
19.21 +
19.22 +consts REACHABLE :: edge set
19.23 + root :: vertex
19.24 + E :: edge set
19.25 + V :: vertex set
19.26 +
19.27 +inductive "REACHABLE"
19.28 + intrs
19.29 + base "v : V ==> ((v,v) : REACHABLE)"
19.30 + step "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)"
19.31 +
19.32 +constdefs
19.33 + reachable :: vertex => state set
19.34 + "reachable p == {s. reach s p}"
19.35 +
19.36 + nmsg_eq :: nat => edge => state set
19.37 + "nmsg_eq k == %e. {s. nmsg s e = k}"
19.38 +
19.39 + nmsg_gt :: nat => edge => state set
19.40 + "nmsg_gt k == %e. {s. k < nmsg s e}"
19.41 +
19.42 + nmsg_gte :: nat => edge => state set
19.43 + "nmsg_gte k == %e. {s. k <= nmsg s e}"
19.44 +
19.45 + nmsg_lte :: nat => edge => state set
19.46 + "nmsg_lte k == %e. {s. nmsg s e <= k}"
19.47 +
19.48 +
19.49 +
19.50 + final :: state set
19.51 + "final == (INTER V (%v. reachable v <==> {s. (root, v) : REACHABLE})) Int (INTER E (nmsg_eq 0))"
19.52 +
19.53 +rules
19.54 + Graph1 "root : V"
19.55 +
19.56 + Graph2 "(v,w) : E ==> (v : V) & (w : V)"
19.57 +
19.58 + MA1 "F : Always (reachable root)"
19.59 +
19.60 + MA2 "[|v:V|] ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})"
19.61 +
19.62 + MA3 "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))"
19.63 +
19.64 + MA4 "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
19.65 +
19.66 + MA5 "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w))"
19.67 +
19.68 + MA6 "[|v:V|] ==> F : Stable (reachable v)"
19.69 +
19.70 + MA6b "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))"
19.71 +
19.72 + MA7 "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)"
19.73 +
19.74 +end
19.75 +
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/HOL/UNITY/Simple/Token.ML Mon Mar 05 15:47:11 2001 +0100
20.3 @@ -0,0 +1,101 @@
20.4 +(* Title: HOL/UNITY/Token
20.5 + ID: $Id$
20.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
20.7 + Copyright 1998 University of Cambridge
20.8 +
20.9 +The Token Ring.
20.10 +
20.11 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
20.12 +*)
20.13 +
20.14 +val Token_defs = [HasTok_def, H_def, E_def, T_def];
20.15 +
20.16 +Goalw [HasTok_def] "[| s: HasTok i; s: HasTok j |] ==> i=j";
20.17 +by Auto_tac;
20.18 +qed "HasToK_partition";
20.19 +
20.20 +Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)";
20.21 +by (Simp_tac 1);
20.22 +by (case_tac "proc s i" 1);
20.23 +by Auto_tac;
20.24 +qed "not_E_eq";
20.25 +
20.26 +Open_locale "Token";
20.27 +
20.28 +val TR2 = thm "TR2";
20.29 +val TR3 = thm "TR3";
20.30 +val TR4 = thm "TR4";
20.31 +val TR5 = thm "TR5";
20.32 +val TR6 = thm "TR6";
20.33 +val TR7 = thm "TR7";
20.34 +val nodeOrder_def = thm "nodeOrder_def";
20.35 +val next_def = thm "next_def";
20.36 +
20.37 +AddIffs [thm "N_positive"];
20.38 +
20.39 +Goalw [stable_def] "F : stable (-(E i) Un (HasTok i))";
20.40 +by (rtac constrains_weaken 1);
20.41 +by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
20.42 +by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
20.43 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
20.44 +qed "token_stable";
20.45 +
20.46 +
20.47 +(*** Progress under weak fairness ***)
20.48 +
20.49 +Goalw [nodeOrder_def] "wf(nodeOrder j)";
20.50 +by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
20.51 +by (Blast_tac 1);
20.52 +qed"wf_nodeOrder";
20.53 +
20.54 +Goalw [nodeOrder_def, next_def, inv_image_def]
20.55 + "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
20.56 +by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq]));
20.57 +by (auto_tac (claset(),
20.58 + simpset() addsplits [nat_diff_split]
20.59 + addsimps [linorder_neq_iff, mod_geq]));
20.60 +qed "nodeOrder_eq";
20.61 +
20.62 +(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
20.63 + Note the use of case_tac. Reasoning about leadsTo takes practice!*)
20.64 +Goal "[| i<N; j<N |] ==> \
20.65 +\ F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)";
20.66 +by (case_tac "i=j" 1);
20.67 +by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
20.68 +by (rtac (TR7 RS leadsTo_weaken_R) 1);
20.69 +by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
20.70 +qed "TR7_nodeOrder";
20.71 +
20.72 +
20.73 +(*Chapter 4 variant, the one actually used below.*)
20.74 +Goal "[| i<N; j<N; i~=j |] \
20.75 +\ ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}";
20.76 +by (rtac (TR7 RS leadsTo_weaken_R) 1);
20.77 +by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
20.78 +qed "TR7_aux";
20.79 +
20.80 +Goal "({s. token s < N} Int token -` {m}) = (if m<N then token -` {m} else {})";
20.81 +by Auto_tac;
20.82 +val token_lemma = result();
20.83 +
20.84 +
20.85 +(*Misra's TR9: the token reaches an arbitrary node*)
20.86 +Goal "j<N ==> F : {s. token s < N} leadsTo (HasTok j)";
20.87 +by (rtac leadsTo_weaken_R 1);
20.88 +by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
20.89 + (wf_nodeOrder RS bounded_induct) 1);
20.90 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff,
20.91 + HasTok_def])));
20.92 +by (Blast_tac 2);
20.93 +by (Clarify_tac 1);
20.94 +by (rtac (TR7_aux RS leadsTo_weaken) 1);
20.95 +by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_def]));
20.96 +qed "leadsTo_j";
20.97 +
20.98 +(*Misra's TR8: a hungry process eventually eats*)
20.99 +Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)";
20.100 +by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
20.101 +by (rtac TR6 2);
20.102 +by (rtac ([leadsTo_j, TR3] MRS psp RS leadsTo_weaken) 1);
20.103 +by (ALLGOALS Blast_tac);
20.104 +qed "token_progress";
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/src/HOL/UNITY/Simple/Token.thy Mon Mar 05 15:47:11 2001 +0100
21.3 @@ -0,0 +1,66 @@
21.4 +(* Title: HOL/UNITY/Token
21.5 + ID: $Id$
21.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
21.7 + Copyright 1998 University of Cambridge
21.8 +
21.9 +The Token Ring.
21.10 +
21.11 +From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
21.12 +*)
21.13 +
21.14 +
21.15 +Token = WFair +
21.16 +
21.17 +(*process states*)
21.18 +datatype pstate = Hungry | Eating | Thinking
21.19 +
21.20 +record state =
21.21 + token :: nat
21.22 + proc :: nat => pstate
21.23 +
21.24 +
21.25 +constdefs
21.26 + HasTok :: nat => state set
21.27 + "HasTok i == {s. token s = i}"
21.28 +
21.29 + H :: nat => state set
21.30 + "H i == {s. proc s i = Hungry}"
21.31 +
21.32 + E :: nat => state set
21.33 + "E i == {s. proc s i = Eating}"
21.34 +
21.35 + T :: nat => state set
21.36 + "T i == {s. proc s i = Thinking}"
21.37 +
21.38 +
21.39 +locale Token =
21.40 + fixes
21.41 + N :: nat (*number of nodes in the ring*)
21.42 + F :: state program
21.43 + nodeOrder :: "nat => (nat*nat)set"
21.44 + next :: nat => nat
21.45 +
21.46 + assumes
21.47 + N_positive "0<N"
21.48 +
21.49 + TR2 "F : (T i) co (T i Un H i)"
21.50 +
21.51 + TR3 "F : (H i) co (H i Un E i)"
21.52 +
21.53 + TR4 "F : (H i - HasTok i) co (H i)"
21.54 +
21.55 + TR5 "F : (HasTok i) co (HasTok i Un -(E i))"
21.56 +
21.57 + TR6 "F : (H i Int HasTok i) leadsTo (E i)"
21.58 +
21.59 + TR7 "F : (HasTok i) leadsTo (HasTok (next i))"
21.60 +
21.61 + defines
21.62 + nodeOrder_def
21.63 + "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int
21.64 + (lessThan N <*> lessThan N)"
21.65 +
21.66 + next_def
21.67 + "next i == (Suc i) mod N"
21.68 +
21.69 +end