--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Channel.ML Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,57 @@
+(* Title: HOL/UNITY/Channel
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Unordered Channel
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
+*)
+
+(*None represents "infinity" while Some represents proper integers*)
+Goalw [minSet_def] "minSet A = Some x --> x : A";
+by (Simp_tac 1);
+by (fast_tac (claset() addIs [LeastI]) 1);
+qed_spec_mp "minSet_eq_SomeD";
+
+Goalw [minSet_def] " minSet{} = None";
+by (Asm_simp_tac 1);
+qed_spec_mp "minSet_empty";
+Addsimps [minSet_empty];
+
+Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)";
+by Auto_tac;
+qed_spec_mp "minSet_nonempty";
+
+Goal "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))";
+by (rtac leadsTo_weaken 1);
+by (res_inst_tac [("x1","x")] ([UC2, UC1] MRS psp) 1);
+by Safe_tac;
+by (auto_tac (claset() addDs [minSet_eq_SomeD],
+ simpset() addsimps [linorder_neq_iff]));
+qed "minSet_greaterThan";
+
+(*The induction*)
+Goal "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))";
+by (rtac leadsTo_weaken_R 1);
+by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
+ greaterThan_bounded_induct 1);
+by Safe_tac;
+by (ALLGOALS Asm_simp_tac);
+by (dtac minSet_nonempty 2);
+by (Asm_full_simp_tac 2);
+by (rtac (minSet_greaterThan RS leadsTo_weaken) 1);
+by Safe_tac;
+by (ALLGOALS Asm_full_simp_tac);
+by (dtac minSet_nonempty 1);
+by (Asm_full_simp_tac 1);
+val lemma = result();
+
+
+Goal "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}";
+by (rtac (lemma RS leadsTo_weaken_R) 1);
+by (Clarify_tac 1);
+by (ftac minSet_nonempty 1);
+by (auto_tac (claset() addDs [Suc_le_lessD, not_less_Least],
+ simpset()));
+qed "Channel_progress";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Channel.thy Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,30 @@
+(* Title: HOL/UNITY/Channel
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Unordered Channel
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
+*)
+
+Channel = WFair + Option +
+
+types state = nat set
+
+consts
+ F :: state program
+
+constdefs
+ minSet :: nat set => nat option
+ "minSet A == if A={} then None else Some (LEAST x. x:A)"
+
+rules
+
+ UC1 "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))"
+
+ (* UC1 "F : {s. minSet s = x} co {s. x <= minSet s}" *)
+
+ UC2 "F : (minSet -` {Some x}) leadsTo {s. x ~: s}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Common.ML Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,90 @@
+(* Title: HOL/UNITY/Common
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Common Meeting Time example from Misra (1994)
+
+The state is identified with the one variable in existence.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
+*)
+
+(*Misra's property CMT4: t exceeds no common meeting time*)
+Goal "[| ALL m. F : {m} Co (maxfg m); n: common |] \
+\ ==> F : Stable (atMost n)";
+by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
+ le_max_iff_disj]) 1);
+by (etac Constrains_weaken_R 1);
+by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
+qed "common_stable";
+
+Goal "[| Init F <= atMost n; \
+\ ALL m. F : {m} Co (maxfg m); n: common |] \
+\ ==> F : Always (atMost n)";
+by (asm_simp_tac (simpset() addsimps [AlwaysI, common_stable]) 1);
+qed "common_safety";
+
+
+(*** Some programs that implement the safety property above ***)
+
+Goal "SKIP : {m} co (maxfg m)";
+by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, le_max_iff_disj,
+ fasc]) 1);
+result();
+
+(*This one is t := ftime t || t := gtime t*)
+Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) \
+\ : {m} co (maxfg m)";
+by (simp_tac (simpset() addsimps [constrains_def, maxfg_def,
+ le_max_iff_disj, fasc]) 1);
+result();
+
+(*This one is t := max (ftime t) (gtime t)*)
+Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) \
+\ : {m} co (maxfg m)";
+by (simp_tac
+ (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
+result();
+
+(*This one is t := t+1 if t <max (ftime t) (gtime t) *)
+Goal "mk_program \
+\ (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV) \
+\ : {m} co (maxfg m)";
+by (simp_tac
+ (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
+result();
+
+
+(*It remans to prove that they satisfy CMT3': t does not decrease,
+ and that CMT3' implies that t stops changing once common(t) holds.*)
+
+
+(*** Progress under weak fairness ***)
+
+Addsimps [atMost_Int_atLeast];
+
+Goal "[| ALL m. F : {m} Co (maxfg m); \
+\ ALL m: lessThan n. F : {m} LeadsTo (greaterThan m); \
+\ n: common |] \
+\ ==> F : (atMost n) LeadsTo common";
+by (rtac LeadsTo_weaken_R 1);
+by (res_inst_tac [("f","id"), ("l","n")] GreaterThan_bounded_induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (rtac subset_refl 2);
+by (blast_tac (claset() addDs [PSP_Stable2]
+ addIs [common_stable, LeadsTo_weaken_R]) 1);
+val lemma = result();
+
+(*The "ALL m: -common" form echoes CMT6.*)
+Goal "[| ALL m. F : {m} Co (maxfg m); \
+\ ALL m: -common. F : {m} LeadsTo (greaterThan m); \
+\ n: common |] \
+\ ==> F : (atMost (LEAST n. n: common)) LeadsTo common";
+by (rtac lemma 1);
+by (ALLGOALS Asm_simp_tac);
+by (etac LeastI 2);
+by (blast_tac (claset() addSDs [not_less_Least]) 1);
+qed "leadsTo_common";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Common.thy Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,32 @@
+(* Title: HOL/UNITY/Common
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Common Meeting Time example from Misra (1994)
+
+The state is identified with the one variable in existence.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
+*)
+
+Common = SubstAx +
+
+consts
+ ftime,gtime :: nat=>nat
+
+rules
+ fmono "m <= n ==> ftime m <= ftime n"
+ gmono "m <= n ==> gtime m <= gtime n"
+
+ fasc "m <= ftime n"
+ gasc "m <= 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)}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Deadlock.ML Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,78 @@
+(* Title: HOL/UNITY/Deadlock
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Deadlock examples from section 5.6 of
+ Misra, "A Logic for Concurrent Programming", 1994
+*)
+
+(*Trivial, two-process case*)
+Goalw [constrains_def, stable_def]
+ "[| F : (A Int B) co A; F : (B Int A) co B |] ==> F : stable (A Int B)";
+by (Blast_tac 1);
+result();
+
+
+(*a simplification step*)
+Goal "(INT i: atMost n. A(Suc i) Int A i) = (INT i: atMost (Suc n). A i)";
+by (induct_tac "n" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [atMost_Suc])));
+by Auto_tac;
+qed "Collect_le_Int_equals";
+
+(*Dual of the required property. Converse inclusion fails.*)
+Goal "(UN i: lessThan n. A i) Int (- A n) <= \
+\ (UN i: lessThan n. (A i) Int (- A (Suc i)))";
+by (induct_tac "n" 1);
+by (Asm_simp_tac 1);
+by (simp_tac (simpset() addsimps [lessThan_Suc]) 1);
+by (Blast_tac 1);
+qed "UN_Int_Compl_subset";
+
+
+(*Converse inclusion fails.*)
+Goal "(INT i: lessThan n. -A i Un A (Suc i)) <= \
+\ (INT i: lessThan n. -A i) Un A n";
+by (induct_tac "n" 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [lessThan_Suc]) 1);
+by (Blast_tac 1);
+qed "INT_Un_Compl_subset";
+
+
+(*Specialized rewriting*)
+Goal "A 0 Int (-(A n) Int (INT i: lessThan n. -A i Un A (Suc i))) = {}";
+by (blast_tac (claset() addIs [gr0I]
+ addDs [impOfSubs INT_Un_Compl_subset]) 1);
+val lemma = result();
+
+(*Reverse direction makes it harder to invoke the ind hyp*)
+Goal "(INT i: atMost n. A i) = \
+\ A 0 Int (INT i: lessThan n. -A i Un A(Suc i))";
+by (induct_tac "n" 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac
+ (simpset() addsimps Int_ac @ [Int_Un_distrib, Int_Un_distrib2, lemma,
+ lessThan_Suc, atMost_Suc]) 1);
+qed "INT_le_equals_Int";
+
+Goal "(INT i: atMost (Suc n). A i) = \
+\ A 0 Int (INT i: atMost n. -A i Un A(Suc i))";
+by (simp_tac (simpset() addsimps [lessThan_Suc_atMost, INT_le_equals_Int]) 1);
+qed "INT_le_Suc_equals_Int";
+
+
+(*The final deadlock example*)
+val [zeroprem, allprem] = Goalw [stable_def]
+ "[| F : (A 0 Int A (Suc n)) co (A 0); \
+\ !!i. i: atMost n ==> F : (A(Suc i) Int A i) co (-A i Un A(Suc i)) |] \
+\ ==> F : stable (INT i: atMost (Suc n). A i)";
+by (rtac ([zeroprem, constrains_INT] MRS
+ constrains_Int RS constrains_weaken) 1);
+by (etac allprem 1);
+by (simp_tac (simpset() addsimps [Collect_le_Int_equals,
+ Int_assoc, INT_absorb]) 1);
+by (simp_tac (simpset() addsimps [INT_le_Suc_equals_Int]) 1);
+result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Deadlock.thy Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,1 @@
+Deadlock = UNITY
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Lift.ML Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,317 @@
+(* Title: HOL/UNITY/Lift
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Lift-Control Example
+*)
+
+Goal "[| x ~: A; y : A |] ==> x ~= y";
+by (Blast_tac 1);
+qed "not_mem_distinct";
+
+
+Addsimps [Lift_def RS def_prg_Init];
+program_defs_ref := [Lift_def];
+
+Addsimps (map simp_of_act
+ [request_act_def, open_act_def, close_act_def,
+ req_up_def, req_down_def, move_up_def, move_down_def,
+ button_press_def]);
+
+(*The ALWAYS properties*)
+Addsimps (map simp_of_set [above_def, below_def, queueing_def,
+ goingup_def, goingdown_def, ready_def]);
+
+Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
+ moving_up_def, moving_down_def];
+
+AddIffs [Min_le_Max];
+
+Goal "Lift : Always open_stop";
+by (always_tac 1);
+qed "open_stop";
+
+Goal "Lift : Always stop_floor";
+by (always_tac 1);
+qed "stop_floor";
+
+(*This one needs open_stop, which was proved above*)
+Goal "Lift : Always open_move";
+by (cut_facts_tac [open_stop] 1);
+by (always_tac 1);
+qed "open_move";
+
+Goal "Lift : Always moving_up";
+by (always_tac 1);
+by (auto_tac (claset() addDs [zle_imp_zless_or_eq],
+ simpset() addsimps [add1_zle_eq]));
+qed "moving_up";
+
+Goal "Lift : Always moving_down";
+by (always_tac 1);
+by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
+qed "moving_down";
+
+Goal "Lift : Always bounded";
+by (cut_facts_tac [moving_up, moving_down] 1);
+by (always_tac 1);
+by Auto_tac;
+by (ALLGOALS (dtac not_mem_distinct THEN' assume_tac));
+by (ALLGOALS arith_tac);
+qed "bounded";
+
+
+
+(*** Progress ***)
+
+
+val abbrev_defs = [moving_def, stopped_def,
+ opened_def, closed_def, atFloor_def, Req_def];
+
+Addsimps (map simp_of_set abbrev_defs);
+
+
+(** The HUG'93 paper mistakenly omits the Req n from these! **)
+
+(** Lift_1 **)
+
+Goal "Lift : (stopped Int atFloor n) LeadsTo (opened Int atFloor n)";
+by (cut_facts_tac [stop_floor] 1);
+by (ensures_tac "open_act" 1);
+qed "E_thm01"; (*lem_lift_1_5*)
+
+Goal "Lift : (Req n Int stopped - atFloor n) LeadsTo \
+\ (Req n Int opened - atFloor n)";
+by (cut_facts_tac [stop_floor] 1);
+by (ensures_tac "open_act" 1);
+qed "E_thm02"; (*lem_lift_1_1*)
+
+Goal "Lift : (Req n Int opened - atFloor n) LeadsTo \
+\ (Req n Int closed - (atFloor n - queueing))";
+by (ensures_tac "close_act" 1);
+qed "E_thm03"; (*lem_lift_1_2*)
+
+Goal "Lift : (Req n Int closed Int (atFloor n - queueing)) \
+\ LeadsTo (opened Int atFloor n)";
+by (ensures_tac "open_act" 1);
+qed "E_thm04"; (*lem_lift_1_7*)
+
+
+(** Lift 2. Statements of thm05a and thm05b were wrong! **)
+
+Open_locale "floor";
+
+val Min_le_n = thm "Min_le_n";
+val n_le_Max = thm "n_le_Max";
+
+AddIffs [Min_le_n, n_le_Max];
+
+val le_MinD = Min_le_n RS order_antisym;
+val Max_leD = n_le_Max RSN (2,order_antisym);
+
+val linorder_leI = linorder_not_less RS iffD1;
+
+AddSDs [le_MinD, linorder_leI RS le_MinD,
+ Max_leD, linorder_leI RS Max_leD];
+
+(*lem_lift_2_0
+ NOT an ensures property, but a mere inclusion;
+ don't know why script lift_2.uni says ENSURES*)
+Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \
+\ LeadsTo ((closed Int goingup Int Req n) Un \
+\ (closed Int goingdown Int Req n))";
+by (auto_tac (claset() addSIs [subset_imp_LeadsTo] addSEs [int_neqE],
+ simpset()));
+qed "E_thm05c";
+
+(*lift_2*)
+Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \
+\ LeadsTo (moving Int Req n)";
+by (rtac ([E_thm05c, LeadsTo_Un] MRS LeadsTo_Trans) 1);
+by (ensures_tac "req_down" 2);
+by (ensures_tac "req_up" 1);
+by Auto_tac;
+qed "lift_2";
+
+
+(** Towards lift_4 ***)
+
+val metric_ss = simpset() addsplits [split_if_asm]
+ addsimps [metric_def, vimage_def];
+
+
+(*lem_lift_4_1 *)
+Goal "#0 < N ==> \
+\ Lift : (moving Int Req n Int {s. metric n s = N} Int \
+\ {s. floor s ~: req s} Int {s. up s}) \
+\ LeadsTo \
+\ (moving Int Req n Int {s. metric n s < N})";
+by (cut_facts_tac [moving_up] 1);
+by (ensures_tac "move_up" 1);
+by Safe_tac;
+(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
+by (etac (linorder_leI RS order_antisym RS sym) 1);
+by (auto_tac (claset(), metric_ss));
+qed "E_thm12a";
+
+
+(*lem_lift_4_3 *)
+Goal "#0 < N ==> \
+\ Lift : (moving Int Req n Int {s. metric n s = N} Int \
+\ {s. floor s ~: req s} - {s. up s}) \
+\ LeadsTo (moving Int Req n Int {s. metric n s < N})";
+by (cut_facts_tac [moving_down] 1);
+by (ensures_tac "move_down" 1);
+by Safe_tac;
+(*this step consolidates two formulae to the goal metric n s' <= metric n s*)
+by (etac (linorder_leI RS order_antisym RS sym) 1);
+by (auto_tac (claset(), metric_ss));
+qed "E_thm12b";
+
+(*lift_4*)
+Goal "#0<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int \
+\ {s. floor s ~: req s}) LeadsTo \
+\ (moving Int Req n Int {s. metric n s < N})";
+by (rtac ([subset_imp_LeadsTo, [E_thm12a, E_thm12b] MRS LeadsTo_Un]
+ MRS LeadsTo_Trans) 1);
+by Auto_tac;
+qed "lift_4";
+
+
+(** towards lift_5 **)
+
+(*lem_lift_5_3*)
+Goal "#0<N \
+\ ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \
+\ (moving Int Req n Int {s. metric n s < N})";
+by (cut_facts_tac [bounded] 1);
+by (ensures_tac "req_up" 1);
+by (auto_tac (claset(), metric_ss));
+qed "E_thm16a";
+
+
+(*lem_lift_5_1 has ~goingup instead of goingdown*)
+Goal "#0<N ==> \
+\ Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \
+\ (moving Int Req n Int {s. metric n s < N})";
+by (cut_facts_tac [bounded] 1);
+by (ensures_tac "req_down" 1);
+by (auto_tac (claset(), metric_ss));
+qed "E_thm16b";
+
+
+(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
+ i.e. the trivial disjunction, leading to an asymmetrical proof.*)
+Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
+by (Clarify_tac 1);
+by (auto_tac (claset(), metric_ss));
+qed "E_thm16c";
+
+
+(*lift_5*)
+Goal "#0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo \
+\ (moving Int Req n Int {s. metric n s < N})";
+by (rtac ([subset_imp_LeadsTo, [E_thm16a, E_thm16b] MRS LeadsTo_Un]
+ MRS LeadsTo_Trans) 1);
+by (dtac E_thm16c 1);
+by Auto_tac;
+qed "lift_5";
+
+
+(** towards lift_3 **)
+
+(*lemma used to prove lem_lift_3_1*)
+Goal "[| metric n s = #0; Min <= floor s; floor s <= Max |] ==> floor s = n";
+by (auto_tac (claset(), metric_ss));
+qed "metric_eq_0D";
+
+AddDs [metric_eq_0D];
+
+
+(*lem_lift_3_1*)
+Goal "Lift : (moving Int Req n Int {s. metric n s = #0}) LeadsTo \
+\ (stopped Int atFloor n)";
+by (cut_facts_tac [bounded] 1);
+by (ensures_tac "request_act" 1);
+by Auto_tac;
+qed "E_thm11";
+
+(*lem_lift_3_5*)
+Goal
+ "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
+\ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
+by (ensures_tac "request_act" 1);
+by (auto_tac (claset(), metric_ss));
+qed "E_thm13";
+
+(*lem_lift_3_6*)
+Goal "#0 < N ==> \
+\ Lift : \
+\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
+\ LeadsTo (opened Int Req n Int {s. metric n s = N})";
+by (ensures_tac "open_act" 1);
+by (auto_tac (claset(), metric_ss));
+qed "E_thm14";
+
+(*lem_lift_3_7*)
+Goal "Lift : (opened Int Req n Int {s. metric n s = N}) \
+\ LeadsTo (closed Int Req n Int {s. metric n s = N})";
+by (ensures_tac "close_act" 1);
+by (auto_tac (claset(), metric_ss));
+qed "E_thm15";
+
+
+(** the final steps **)
+
+Goal "#0 < N ==> \
+\ Lift : \
+\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
+\ LeadsTo (moving Int Req n Int {s. metric n s < N})";
+by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
+ addIs [LeadsTo_Trans]) 1);
+qed "lift_3_Req";
+
+
+(*Now we observe that our integer metric is really a natural number*)
+Goal "Lift : Always {s. #0 <= metric n s}";
+by (rtac (bounded RS Always_weaken) 1);
+by (auto_tac (claset(), metric_ss));
+qed "Always_nonneg";
+
+val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken;
+
+Goal "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)";
+by (rtac (Always_nonneg RS integ_0_le_induct) 1);
+by (case_tac "#0 < z" 1);
+(*If z <= #0 then actually z = #0*)
+by (force_tac (claset() addIs [R_thm11, order_antisym],
+ simpset() addsimps [linorder_not_less]) 2);
+by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
+by (rtac ([subset_imp_LeadsTo, [lift_4, lift_3_Req] MRS LeadsTo_Un]
+ MRS LeadsTo_Trans) 1);
+by Auto_tac;
+qed "lift_3";
+
+
+val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
+(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *)
+
+Goal "Lift : (Req n) LeadsTo (opened Int atFloor n)";
+by (rtac LeadsTo_Trans 1);
+by (rtac ([E_thm04, LeadsTo_Un_post] MRS LeadsTo_Un) 2);
+by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2);
+by (rtac (lift_3 RS LeadsTo_Trans_Un') 2);
+by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
+by (rtac ([E_thm03,E_thm02] MRS LeadsTo_Trans_Un') 2);
+by (rtac (open_move RS Always_LeadsToI) 1);
+by (rtac ([open_stop, subset_imp_LeadsTo] MRS Always_LeadsToI) 1);
+by (Clarify_tac 1);
+(*The case split is not essential but makes Blast_tac much faster.
+ Calling rotate_tac prevents simplification from looping*)
+by (case_tac "open x" 1);
+by (ALLGOALS (rotate_tac ~1));
+by Auto_tac;
+qed "lift_1";
+
+Close_locale "floor";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Lift.thy Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,169 @@
+(* Title: HOL/UNITY/Lift.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Lift-Control Example
+*)
+
+Lift = SubstAx +
+
+record state =
+ floor :: int (*current position of the lift*)
+ open :: bool (*whether the door is open at floor*)
+ stop :: bool (*whether the lift is stopped at floor*)
+ req :: int set (*for each floor, whether the lift is requested*)
+ up :: bool (*current direction of movement*)
+ move :: bool (*whether moving takes precedence over opening*)
+
+consts
+ Min, Max :: int (*least and greatest floors*)
+
+rules
+ Min_le_Max "Min <= Max"
+
+constdefs
+
+ (** Abbreviations: the "always" part **)
+
+ above :: state set
+ "above == {s. EX i. floor s < i & i <= Max & i : req s}"
+
+ below :: state set
+ "below == {s. EX i. Min <= i & i < floor s & i : req s}"
+
+ queueing :: state set
+ "queueing == above Un below"
+
+ goingup :: state set
+ "goingup == above Int ({s. up s} Un -below)"
+
+ goingdown :: state set
+ "goingdown == below Int ({s. ~ up s} Un -above)"
+
+ ready :: state set
+ "ready == {s. stop s & ~ open s & move s}"
+
+
+ (** Further abbreviations **)
+
+ moving :: state set
+ "moving == {s. ~ stop s & ~ open s}"
+
+ stopped :: state set
+ "stopped == {s. stop s & ~ open s & ~ move s}"
+
+ opened :: state set
+ "opened == {s. stop s & open s & move s}"
+
+ closed :: state set (*but this is the same as ready!!*)
+ "closed == {s. stop s & ~ open s & move s}"
+
+ atFloor :: int => state set
+ "atFloor n == {s. floor s = n}"
+
+ Req :: int => state set
+ "Req n == {s. n : req s}"
+
+
+
+ (** The program **)
+
+ request_act :: "(state*state) set"
+ "request_act == {(s,s'). s' = s (|stop:=True, move:=False|)
+ & ~ stop s & floor s : 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)}"
+
+ close_act :: "(state*state) set"
+ "close_act == {(s,s'). s' = s (|open := False|) & open s}"
+
+ req_up :: "(state*state) set"
+ "req_up ==
+ {(s,s'). s' = s (|stop :=False,
+ floor := floor s + #1,
+ up := True|)
+ & s : (ready Int goingup)}"
+
+ req_down :: "(state*state) set"
+ "req_down ==
+ {(s,s'). s' = s (|stop :=False,
+ floor := floor s - #1,
+ up := False|)
+ & s : (ready Int goingdown)}"
+
+ move_up :: "(state*state) set"
+ "move_up ==
+ {(s,s'). s' = s (|floor := floor s + #1|)
+ & ~ stop s & up s & floor s ~: 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}"
+
+ (*This action is omitted from prior treatments, which therefore are
+ unrealistic: nobody asks the lift to do anything! But adding this
+ action invalidates many of the existing progress arguments: various
+ "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}"
+
+
+ Lift :: state program
+ (*for the moment, we OMIT button_press*)
+ "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
+ ~ open s & req s = {}},
+ {request_act, open_act, close_act,
+ req_up, req_down, move_up, move_down},
+ UNIV)"
+
+
+ (** Invariants **)
+
+ bounded :: state set
+ "bounded == {s. Min <= floor s & floor s <= Max}"
+
+ open_stop :: state set
+ "open_stop == {s. open s --> stop s}"
+
+ open_move :: state set
+ "open_move == {s. open s --> move s}"
+
+ stop_floor :: state set
+ "stop_floor == {s. stop s & ~ move s --> floor s : req s}"
+
+ moving_up :: state set
+ "moving_up == {s. ~ stop s & up s -->
+ (EX f. floor s <= f & f <= Max & f : req s)}"
+
+ moving_down :: state set
+ "moving_down == {s. ~ stop s & ~ up s -->
+ (EX f. Min <= f & f <= floor s & f : req s)}"
+
+ metric :: [int,state] => int
+ "metric ==
+ %n s. if floor s < n then (if up s then n - floor s
+ else (floor s - Min) + (n-Min))
+ else
+ if n < floor s then (if up s then (Max - floor s) + (Max-n)
+ else floor s - n)
+ else #0"
+
+locale floor =
+ fixes
+ n :: int
+ assumes
+ Min_le_n "Min <= n"
+ n_le_Max "n <= Max"
+ defines
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Mutex.ML Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,166 @@
+(* Title: HOL/UNITY/Mutex
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+*)
+
+Addsimps [Mutex_def RS def_prg_Init];
+program_defs_ref := [Mutex_def];
+
+Addsimps (map simp_of_act
+ [U0_def, U1_def, U2_def, U3_def, U4_def,
+ V0_def, V1_def, V2_def, V3_def, V4_def]);
+
+Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
+
+
+Goal "Mutex : Always IU";
+by (always_tac 1);
+qed "IU";
+
+Goal "Mutex : Always IV";
+by (always_tac 1);
+qed "IV";
+
+(*The safety property: mutual exclusion*)
+Goal "Mutex : Always {s. ~ (m s = #3 & n s = #3)}";
+by (rtac ([IU, IV] MRS Always_Int_I RS Always_weaken) 1);
+by Auto_tac;
+qed "mutual_exclusion";
+
+
+(*The bad invariant FAILS in V1*)
+Goal "Mutex : Always bad_IU";
+by (always_tac 1);
+by Auto_tac;
+(*Resulting state: n=1, p=false, m=4, u=false.
+ Execution of V1 (the command of process v guarded by n=1) sets p:=true,
+ violating the invariant!*)
+(*Check that subgoals remain: proof failed.*)
+getgoal 1;
+
+
+Goal "((#1::int) <= i & i <= #3) = (i = #1 | i = #2 | i = #3)";
+by (arith_tac 1);
+qed "eq_123";
+
+
+(*** Progress for U ***)
+
+Goalw [Unless_def] "Mutex : {s. m s=#2} Unless {s. m s=#3}";
+by (constrains_tac 1);
+qed "U_F0";
+
+Goal "Mutex : {s. m s=#1} LeadsTo {s. p s = v s & m s = #2}";
+by (ensures_tac "U1" 1);
+qed "U_F1";
+
+Goal "Mutex : {s. ~ p s & m s = #2} LeadsTo {s. m s = #3}";
+by (cut_facts_tac [IU] 1);
+by (ensures_tac "U2" 1);
+qed "U_F2";
+
+Goal "Mutex : {s. m s = #3} LeadsTo {s. p s}";
+by (res_inst_tac [("B", "{s. m s = #4}")] LeadsTo_Trans 1);
+by (ensures_tac "U4" 2);
+by (ensures_tac "U3" 1);
+qed "U_F3";
+
+Goal "Mutex : {s. m s = #2} LeadsTo {s. p s}";
+by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
+ MRS LeadsTo_Diff) 1);
+by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
+by (auto_tac (claset() addSEs [less_SucE], simpset()));
+val U_lemma2 = result();
+
+Goal "Mutex : {s. m s = #1} LeadsTo {s. p s}";
+by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
+by (Blast_tac 1);
+val U_lemma1 = result();
+
+Goal "Mutex : {s. #1 <= m s & m s <= #3} LeadsTo {s. p s}";
+by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
+ U_lemma1, U_lemma2, U_F3] ) 1);
+val U_lemma123 = result();
+
+(*Misra's F4*)
+Goal "Mutex : {s. u s} LeadsTo {s. p s}";
+by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1);
+by Auto_tac;
+qed "u_Leadsto_p";
+
+
+(*** Progress for V ***)
+
+
+Goalw [Unless_def] "Mutex : {s. n s=#2} Unless {s. n s=#3}";
+by (constrains_tac 1);
+qed "V_F0";
+
+Goal "Mutex : {s. n s=#1} LeadsTo {s. p s = (~ u s) & n s = #2}";
+by (ensures_tac "V1" 1);
+qed "V_F1";
+
+Goal "Mutex : {s. p s & n s = #2} LeadsTo {s. n s = #3}";
+by (cut_facts_tac [IV] 1);
+by (ensures_tac "V2" 1);
+qed "V_F2";
+
+Goal "Mutex : {s. n s = #3} LeadsTo {s. ~ p s}";
+by (res_inst_tac [("B", "{s. n s = #4}")] LeadsTo_Trans 1);
+by (ensures_tac "V4" 2);
+by (ensures_tac "V3" 1);
+qed "V_F3";
+
+Goal "Mutex : {s. n s = #2} LeadsTo {s. ~ p s}";
+by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo]
+ MRS LeadsTo_Diff) 1);
+by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
+by (auto_tac (claset() addSEs [less_SucE], simpset()));
+val V_lemma2 = result();
+
+Goal "Mutex : {s. n s = #1} LeadsTo {s. ~ p s}";
+by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
+by (Blast_tac 1);
+val V_lemma1 = result();
+
+Goal "Mutex : {s. #1 <= n s & n s <= #3} LeadsTo {s. ~ p s}";
+by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib,
+ V_lemma1, V_lemma2, V_F3] ) 1);
+val V_lemma123 = result();
+
+
+(*Misra's F4*)
+Goal "Mutex : {s. v s} LeadsTo {s. ~ p s}";
+by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
+by Auto_tac;
+qed "v_Leadsto_not_p";
+
+
+(** Absence of starvation **)
+
+(*Misra's F6*)
+Goal "Mutex : {s. m s = #1} LeadsTo {s. m s = #3}";
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
+by (rtac U_F2 2);
+by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
+by (stac Un_commute 1);
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
+by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless) 2);
+by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
+by Auto_tac;
+qed "m1_Leadsto_3";
+
+(*The same for V*)
+Goal "Mutex : {s. n s = #1} LeadsTo {s. n s = #3}";
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
+by (rtac V_F2 2);
+by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
+by (stac Un_commute 1);
+by (rtac (LeadsTo_cancel2 RS LeadsTo_Un_duplicate) 1);
+by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless) 2);
+by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
+by Auto_tac;
+qed "n1_Leadsto_3";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Mutex.thy Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,76 @@
+(* Title: HOL/UNITY/Mutex.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
+*)
+
+Mutex = SubstAx +
+
+record state =
+ p :: bool
+ m :: int
+ n :: int
+ u :: bool
+ v :: bool
+
+types command = "(state*state) set"
+
+constdefs
+
+ (** The program for process U **)
+
+ U0 :: command
+ "U0 == {(s,s'). s' = s (|u:=True, m:=#1|) & m s = #0}"
+
+ U1 :: command
+ "U1 == {(s,s'). s' = s (|p:= v s, m:=#2|) & m s = #1}"
+
+ U2 :: command
+ "U2 == {(s,s'). s' = s (|m:=#3|) & ~ p s & m s = #2}"
+
+ U3 :: command
+ "U3 == {(s,s'). s' = s (|u:=False, m:=#4|) & m s = #3}"
+
+ U4 :: command
+ "U4 == {(s,s'). s' = s (|p:=True, m:=#0|) & m s = #4}"
+
+ (** The program for process V **)
+
+ V0 :: command
+ "V0 == {(s,s'). s' = s (|v:=True, n:=#1|) & n s = #0}"
+
+ V1 :: command
+ "V1 == {(s,s'). s' = s (|p:= ~ u s, n:=#2|) & n s = #1}"
+
+ V2 :: command
+ "V2 == {(s,s'). s' = s (|n:=#3|) & p s & n s = #2}"
+
+ V3 :: command
+ "V3 == {(s,s'). s' = s (|v:=False, n:=#4|) & n s = #3}"
+
+ V4 :: command
+ "V4 == {(s,s'). s' = s (|p:=False, n:=#0|) & n s = #4}"
+
+ Mutex :: state program
+ "Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
+ {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
+ UNIV)"
+
+
+ (** The correct invariants **)
+
+ IU :: state set
+ "IU == {s. (u s = (#1 <= m s & m s <= #3)) & (m s = #3 --> ~ p s)}"
+
+ IV :: state set
+ "IV == {s. (v s = (#1 <= n s & n s <= #3)) & (n s = #3 --> p s)}"
+
+ (** The faulty invariant (for U alone) **)
+
+ bad_IU :: state set
+ "bad_IU == {s. (u s = (#1 <= m s & m s <= #3)) &
+ (#3 <= m s & m s <= #4 --> ~ p s)}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/NSP_Bad.ML Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,288 @@
+(* Title: HOL/Auth/NSP_Bad
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+
+Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol.
+Flawed version, vulnerable to Lowe's attack.
+
+From page 260 of
+ Burrows, Abadi and Needham. A Logic of Authentication.
+ Proc. Royal Soc. 426 (1989)
+*)
+
+fun impOfAlways th =
+ rulify (th RS Always_includes_reachable RS subsetD RS CollectD);
+
+AddEs spies_partsEs;
+AddDs [impOfSubs analz_subset_parts];
+AddDs [impOfSubs Fake_parts_insert];
+
+(*For other theories, e.g. Mutex and Lift, using AddIffs slows proofs down.
+ Here, it facilitates re-use of the Auth proofs.*)
+
+AddIffs (map simp_of_act [Fake_def, NS1_def, NS2_def, NS3_def]);
+
+Addsimps [Nprg_def RS def_prg_simps];
+
+
+(*A "possibility property": there are traces that reach the end.
+ Replace by LEADSTO proof!*)
+Goal "A ~= B ==> EX NB. EX s: reachable Nprg. \
+\ Says A B (Crypt (pubK B) (Nonce NB)) : set s";
+by (REPEAT (resolve_tac [exI,bexI] 1));
+by (res_inst_tac [("act", "NS3")] reachable.Acts 2);
+by (res_inst_tac [("act", "NS2")] reachable.Acts 3);
+by (res_inst_tac [("act", "NS1")] reachable.Acts 4);
+by (rtac reachable.Init 5);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Nprg_def])));
+by (REPEAT_FIRST (rtac exI ));
+by possibility_tac;
+result();
+
+
+(**** Inductive proofs about ns_public ****)
+
+(*can be used to simulate analz_mono_contra_tac
+val analz_impI = read_instantiate_sg (sign_of thy)
+ [("P", "?Y ~: analz (spies ?evs)")] impI;
+
+val spies_Says_analz_contraD =
+ spies_subset_spies_Says RS analz_mono RS contra_subsetD;
+
+by (rtac analz_impI 2);
+by (auto_tac (claset() addSDs [spies_Says_analz_contraD], simpset()));
+*)
+
+fun ns_constrains_tac i =
+ SELECT_GOAL
+ (EVERY [REPEAT (etac Always_ConstrainsI 1),
+ REPEAT (resolve_tac [StableI, stableI,
+ constrains_imp_Constrains] 1),
+ rtac constrainsI 1,
+ Full_simp_tac 1,
+ REPEAT (FIRSTGOAL (etac disjE)),
+ ALLGOALS (clarify_tac (claset() delrules [impI,impCE])),
+ REPEAT (FIRSTGOAL analz_mono_contra_tac),
+ ALLGOALS Asm_simp_tac]) i;
+
+(*Tactic for proving secrecy theorems*)
+val ns_induct_tac =
+ (SELECT_GOAL o EVERY)
+ [rtac AlwaysI 1,
+ Force_tac 1,
+ (*"reachable" gets in here*)
+ rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1,
+ ns_constrains_tac 1];
+
+
+(** Theorems of the form X ~: parts (spies evs) imply that NOBODY
+ sends messages containing X! **)
+
+(*Spy never sees another agent's private key! (unless it's bad at start)*)
+Goal "Nprg : Always {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
+by (ns_induct_tac 1);
+by (Blast_tac 1);
+qed "Spy_see_priK";
+Addsimps [impOfAlways Spy_see_priK];
+
+Goal "Nprg : Always {s. (Key (priK A) : analz (spies s)) = (A : bad)}";
+by (rtac (Always_reachable RS Always_weaken) 1);
+by Auto_tac;
+qed "Spy_analz_priK";
+Addsimps [impOfAlways Spy_analz_priK];
+
+(**
+AddSDs [Spy_see_priK RSN (2, rev_iffD1),
+ Spy_analz_priK RSN (2, rev_iffD1)];
+**)
+
+
+(**** Authenticity properties obtained from NS2 ****)
+
+(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
+ is secret. (Honest users generate fresh nonces.)*)
+Goal
+ "Nprg \
+\ : Always {s. Nonce NA ~: analz (spies s) --> \
+\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies s) --> \
+\ Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies s)}";
+by (ns_induct_tac 1);
+by (ALLGOALS Blast_tac);
+qed "no_nonce_NS1_NS2";
+
+(*Adding it to the claset slows down proofs...*)
+val nonce_NS1_NS2_E = impOfAlways no_nonce_NS1_NS2 RSN (2, rev_notE);
+
+
+(*Unicity for NS1: nonce NA identifies agents A and B*)
+Goal "Nprg \
+\ : Always {s. Nonce NA ~: analz (spies s) --> \
+\ Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies s) --> \
+\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies s) --> \
+\ A=A' & B=B'}";
+by (ns_induct_tac 1);
+by Auto_tac;
+(*Fake, NS1 are non-trivial*)
+val unique_NA_lemma = result();
+
+(*Unicity for NS1: nonce NA identifies agents A and B*)
+Goal "[| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(spies s); \
+\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies s); \
+\ Nonce NA ~: analz (spies s); \
+\ s : reachable Nprg |] \
+\ ==> A=A' & B=B'";
+by (blast_tac (claset() addDs [impOfAlways unique_NA_lemma]) 1);
+qed "unique_NA";
+
+
+(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
+Goal "[| A ~: bad; B ~: bad |] \
+\ ==> Nprg : Always \
+\ {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set s \
+\ --> Nonce NA ~: analz (spies s)}";
+by (ns_induct_tac 1);
+(*NS3*)
+by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 4);
+(*NS2*)
+by (blast_tac (claset() addDs [unique_NA]) 3);
+(*NS1*)
+by (Blast_tac 2);
+(*Fake*)
+by (spy_analz_tac 1);
+qed "Spy_not_see_NA";
+
+
+(*Authentication for A: if she receives message 2 and has used NA
+ to start a run, then B has sent message 2.*)
+val prems =
+goal thy "[| A ~: bad; B ~: bad |] \
+\ ==> Nprg : Always \
+\ {s. Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set s & \
+\ Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts (knows Spy s) \
+\ --> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set s}";
+ (*insert an invariant for use in some of the subgoals*)
+by (cut_facts_tac ([prems MRS Spy_not_see_NA] @ prems) 1);
+by (ns_induct_tac 1);
+by (ALLGOALS Clarify_tac);
+(*NS2*)
+by (blast_tac (claset() addDs [unique_NA]) 3);
+(*NS1*)
+by (Blast_tac 2);
+(*Fake*)
+by (Blast_tac 1);
+qed "A_trusts_NS2";
+
+
+(*If the encrypted message appears then it originated with Alice in NS1*)
+Goal "Nprg : Always \
+\ {s. Nonce NA ~: analz (spies s) --> \
+\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies s) \
+\ --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set s}";
+by (ns_induct_tac 1);
+by (Blast_tac 1);
+qed "B_trusts_NS1";
+
+
+
+(**** Authenticity properties obtained from NS2 ****)
+
+(*Unicity for NS2: nonce NB identifies nonce NA and agent A
+ [proof closely follows that for unique_NA] *)
+Goal
+ "Nprg \
+\ : Always {s. Nonce NB ~: analz (spies s) --> \
+\ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies s) --> \
+\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies s) --> \
+\ A=A' & NA=NA'}";
+by (ns_induct_tac 1);
+by Auto_tac;
+(*Fake, NS2 are non-trivial*)
+val unique_NB_lemma = result();
+
+Goal "[| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(spies s); \
+\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies s); \
+\ Nonce NB ~: analz (spies s); \
+\ s : reachable Nprg |] \
+\ ==> A=A' & NA=NA'";
+by (blast_tac (claset() addDs [impOfAlways unique_NB_lemma]) 1);
+qed "unique_NB";
+
+
+(*NB remains secret PROVIDED Alice never responds with round 3*)
+Goal "[| A ~: bad; B ~: bad |] \
+\ ==> Nprg : Always \
+\ {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s & \
+\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set s) \
+\ --> Nonce NB ~: analz (spies s)}";
+by (ns_induct_tac 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
+by (ALLGOALS Clarify_tac);
+(*NS3: because NB determines A*)
+by (blast_tac (claset() addDs [unique_NB]) 4);
+(*NS2: by freshness and unicity of NB*)
+by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
+(*NS1: by freshness*)
+by (Blast_tac 2);
+(*Fake*)
+by (spy_analz_tac 1);
+qed "Spy_not_see_NB";
+
+
+
+(*Authentication for B: if he receives message 3 and has used NB
+ in message 2, then A has sent message 3--to somebody....*)
+val prems =
+goal thy "[| A ~: bad; B ~: bad |] \
+\ ==> Nprg : Always \
+\ {s. Crypt (pubK B) (Nonce NB) : parts (spies s) & \
+\ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s \
+\ --> (EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set s)}";
+ (*insert an invariant for use in some of the subgoals*)
+by (cut_facts_tac ([prems MRS Spy_not_see_NB] @ prems) 1);
+by (ns_induct_tac 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
+by (ALLGOALS Clarify_tac);
+(*NS3: because NB determines A (this use of unique_NB is more robust) *)
+by (blast_tac (claset() addIs [unique_NB RS conjunct1]) 3);
+(*NS1: by freshness*)
+by (Blast_tac 2);
+(*Fake*)
+by (Blast_tac 1);
+qed "B_trusts_NS3";
+
+
+(*Can we strengthen the secrecy theorem? NO*)
+Goal "[| A ~: bad; B ~: bad |] \
+\ ==> Nprg : Always \
+\ {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s \
+\ --> Nonce NB ~: analz (spies s)}";
+by (ns_induct_tac 1);
+by (ALLGOALS Clarify_tac);
+(*NS2: by freshness and unicity of NB*)
+by (blast_tac (claset() addEs [nonce_NS1_NS2_E]) 3);
+(*NS1: by freshness*)
+by (Blast_tac 2);
+(*Fake*)
+by (spy_analz_tac 1);
+(*NS3: unicity of NB identifies A and NA, but not B*)
+by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1
+ THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1));
+by Auto_tac;
+by (rename_tac "s B' C" 1);
+
+(*
+THIS IS THE ATTACK!
+[| A ~: bad; B ~: bad |]
+==> Nprg
+ : Always
+ {s. Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s -->
+ Nonce NB ~: analz (knows Spy s)}
+ 1. !!s B' C.
+ [| A ~: bad; B ~: bad; s : reachable Nprg;
+ Says A C (Crypt (pubK C) {|Nonce NA, Agent A|}) : set s;
+ Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s;
+ C : bad; Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set s;
+ Nonce NB ~: analz (knows Spy s) |]
+ ==> False
+*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,59 @@
+(* Title: HOL/Auth/NSP_Bad
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+
+add_path "../Auth"; use_thy"NSP_Bad";
+
+Security protocols in UNITY: Needham-Schroeder, public keys (flawed version).
+
+Original file is ../Auth/NS_Public_Bad
+*)
+
+NSP_Bad = Public + Constrains +
+
+types state = event list
+
+constdefs
+
+ (*The spy MAY say anything he CAN say. We do not expect him to
+ invent new nonces here, but he can also use NS1. Common to
+ all similar protocols.*)
+ Fake :: "(state*state) set"
+ "Fake == {(s,s').
+ EX B X. s' = Says Spy B X # s
+ & X: synth (analz (spies s))}"
+
+ (*The numeric suffixes on A identify the rule*)
+
+ (*Alice initiates a protocol run, sending a nonce to Bob*)
+ NS1 :: "(state*state) set"
+ "NS1 == {(s1,s').
+ EX A1 B NA.
+ s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
+ & Nonce NA ~: used s1}"
+
+ (*Bob responds to Alice's message with a further nonce*)
+ NS2 :: "(state*state) set"
+ "NS2 == {(s2,s').
+ EX A' A2 B NA NB.
+ s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
+ & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) : set s2
+ & Nonce NB ~: used s2}"
+
+ (*Alice proves her existence by sending NB back to Bob.*)
+ NS3 :: "(state*state) set"
+ "NS3 == {(s3,s').
+ EX A3 B' B NA NB.
+ s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3
+ & Says A3 B (Crypt (pubK B) {|Nonce NA, Agent A3|}) : set s3
+ & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) : set s3}"
+
+
+
+constdefs
+ Nprg :: state program
+ (*Initial trace is empty*)
+ "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Network.ML Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,59 @@
+(* Title: HOL/UNITY/Network
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Communication Network
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
+*)
+
+val [rsA, rsB, sent_nondec, rcvd_nondec, rcvd_idle, sent_idle] =
+Goalw [stable_def]
+ "[| !! m. F : stable {s. s(Bproc,Rcvd) <= s(Aproc,Sent)}; \
+\ !! m. F : stable {s. s(Aproc,Rcvd) <= s(Bproc,Sent)}; \
+\ !! m proc. F : stable {s. m <= s(proc,Sent)}; \
+\ !! n proc. F : stable {s. n <= s(proc,Rcvd)}; \
+\ !! m proc. F : {s. s(proc,Idle) = 1 & s(proc,Rcvd) = m} co \
+\ {s. s(proc,Rcvd) = m --> s(proc,Idle) = 1}; \
+\ !! n proc. F : {s. s(proc,Idle) = 1 & s(proc,Sent) = n} co \
+\ {s. s(proc,Sent) = n} \
+\ |] ==> F : stable {s. s(Aproc,Idle) = 1 & s(Bproc,Idle) = 1 & \
+\ s(Aproc,Sent) = s(Bproc,Rcvd) & \
+\ s(Bproc,Sent) = s(Aproc,Rcvd) & \
+\ s(Aproc,Rcvd) = m & s(Bproc,Rcvd) = n}";
+
+val sent_nondec_A = read_instantiate [("proc","Aproc")] sent_nondec;
+val sent_nondec_B = read_instantiate [("proc","Bproc")] sent_nondec;
+val rcvd_nondec_A = read_instantiate [("proc","Aproc")] rcvd_nondec;
+val rcvd_nondec_B = read_instantiate [("proc","Bproc")] rcvd_nondec;
+val rcvd_idle_A = read_instantiate [("proc","Aproc")] rcvd_idle;
+val rcvd_idle_B = read_instantiate [("proc","Bproc")] rcvd_idle;
+val sent_idle_A = read_instantiate [("proc","Aproc")] sent_idle;
+val sent_idle_B = read_instantiate [("proc","Bproc")] sent_idle;
+
+val rs_AB = [rsA, rsB] MRS constrains_Int;
+val sent_nondec_AB = [sent_nondec_A, sent_nondec_B] MRS constrains_Int;
+val rcvd_nondec_AB = [rcvd_nondec_A, rcvd_nondec_B] MRS constrains_Int;
+val rcvd_idle_AB = [rcvd_idle_A, rcvd_idle_B] MRS constrains_Int;
+val sent_idle_AB = [sent_idle_A, sent_idle_B] MRS constrains_Int;
+val nondec_AB = [sent_nondec_AB, rcvd_nondec_AB] MRS constrains_Int;
+val idle_AB = [rcvd_idle_AB, sent_idle_AB] MRS constrains_Int;
+val nondec_idle = [nondec_AB, idle_AB] MRS constrains_Int;
+
+by (rtac constrainsI 1);
+by (dtac ([rs_AB, nondec_idle] MRS constrains_Int RS constrainsD) 1);
+by (assume_tac 1);
+by (ALLGOALS Asm_full_simp_tac);
+by (blast_tac (HOL_cs addIs [order_refl]) 1);
+by (Clarify_tac 1);
+by (subgoals_tac ["s' (Aproc, Rcvd) = s (Aproc, Rcvd)",
+ "s' (Bproc, Rcvd) = s (Bproc, Rcvd)"] 1);
+by (REPEAT
+ (blast_tac (claset() addIs [order_antisym, le_trans, eq_imp_le]) 2));
+by (Asm_simp_tac 1);
+result();
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Network.thy Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,21 @@
+(* Title: HOL/UNITY/Network
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Communication Network
+
+From Misra, "A Logic for Concurrent Programming" (1994), section 5.7
+*)
+
+Network = UNITY +
+
+(*The state assigns a number to each process variable*)
+
+datatype pvar = Sent | Rcvd | Idle
+
+datatype pname = Aproc | Bproc
+
+types state = "pname * pvar => nat"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/README.html Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,36 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
+
+<H2>UNITY: Examples Involving Single Programs</H2>
+
+<P> The directory presents verification examples that do not involve program
+composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'':
+<UL>
+<LI>common meeting time (<A HREF="Common.thy"><CODE>Common.thy</CODE></A>)
+
+<LI>the token ring (<A HREF="Token.thy"><CODE>Token.thy</CODE></A>)
+
+<LI>the communication network
+(<A HREF="Network.thy"><CODE>Network.thy</CODE></A>)
+
+<LI>the lift controller (a standard benchmark) (<A HREF="Lift.thy"><CODE>Lift.thy</CODE></A>)
+
+<LI>a mutual exclusion algorithm (<A HREF="Mutex.thy"><CODE>Mutex.thy</CODE></A>)
+
+<LI><EM>n</EM>-process deadlock
+(<A HREF="Deadlock.thy"><CODE>Deadlock.thy</CODE></A>)
+
+<LI>unordered channel (<A HREF="Channel.thy"><CODE>Channel.thy</CODE></A>)
+
+<LI>reachability in directed graphs (section 6.4 of the book) (<A
+HREF="Reach.thy"><CODE>Reach.thy</CODE></A> and
+<A HREF="Reachability.thy"><CODE>Reachability.thy</CODE></A>)
+</UL>
+
+<HR>
+<P>Last modified on $Date$
+
+<ADDRESS>
+<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
+</ADDRESS>
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Reach.ML Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,142 @@
+(* Title: HOL/UNITY/Reach.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Reachability in Directed Graphs. From Chandy and Misra, section 6.4.
+ [ this example took only four days!]
+*)
+
+(*TO SIMPDATA.ML?? FOR CLASET?? *)
+val major::prems = goal thy
+ "[| if P then Q else R; \
+\ [| P; Q |] ==> S; \
+\ [| ~ P; R |] ==> S |] ==> S";
+by (cut_facts_tac [major] 1);
+by (blast_tac (claset() addSDs [if_bool_eq_disj RS iffD1] addIs prems) 1);
+qed "ifE";
+
+AddSEs [ifE];
+
+
+Addsimps [Rprg_def RS def_prg_Init];
+program_defs_ref := [Rprg_def];
+
+Addsimps [simp_of_act asgt_def];
+
+(*All vertex sets are finite*)
+AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
+
+Addsimps [simp_of_set reach_invariant_def];
+
+Goal "Rprg : Always reach_invariant";
+by (always_tac 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
+qed "reach_invariant";
+
+
+(*** Fixedpoint ***)
+
+(*If it reaches a fixedpoint, it has found a solution*)
+Goalw [fixedpoint_def]
+ "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
+by (rtac equalityI 1);
+by (auto_tac (claset() addSIs [ext], simpset()));
+by (blast_tac (claset() addIs [rtrancl_trans]) 2);
+by (etac rtrancl_induct 1);
+by Auto_tac;
+qed "fixedpoint_invariant_correct";
+
+Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
+ "FP Rprg <= fixedpoint";
+by Auto_tac;
+by (dtac bspec 1 THEN atac 1);
+by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
+by (dtac fun_cong 1);
+by Auto_tac;
+val lemma1 = result();
+
+Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
+ "fixedpoint <= FP Rprg";
+by (auto_tac (claset() addSIs [ext], simpset()));
+val lemma2 = result();
+
+Goal "FP Rprg = fixedpoint";
+by (rtac ([lemma1,lemma2] MRS equalityI) 1);
+qed "FP_fixedpoint";
+
+
+(*If we haven't reached a fixedpoint then there is some edge for which u but
+ not v holds. Progress will be proved via an ENSURES assertion that the
+ metric will decrease for each suitable edge. A union over all edges proves
+ a LEADSTO assertion that the metric decreases if we are not at a fixedpoint.
+ *)
+
+Goal "- fixedpoint = (UN (u,v): edges. {s. s u & ~ s v})";
+by (simp_tac (simpset() addsimps
+ [Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, Rprg_def]) 1);
+by Auto_tac;
+by (rtac fun_upd_idem 1);
+by Auto_tac;
+by (force_tac (claset() addSIs [rev_bexI],
+ simpset() addsimps [fun_upd_idem_iff]) 1);
+qed "Compl_fixedpoint";
+
+Goal "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
+by (simp_tac (simpset() addsimps [Diff_eq, Compl_fixedpoint]) 1);
+by (Blast_tac 1);
+qed "Diff_fixedpoint";
+
+
+(*** Progress ***)
+
+Goalw [metric_def] "~ s x ==> Suc (metric (s(x:=True))) = metric s";
+by (subgoal_tac "{v. ~ (s(x:=True)) v} = {v. ~ s v} - {x}" 1);
+by (Force_tac 2);
+by (asm_full_simp_tac (simpset() addsimps [card_Suc_Diff1]) 1);
+qed "Suc_metric";
+
+Goal "~ s x ==> metric (s(x:=True)) < metric s";
+by (etac (Suc_metric RS subst) 1);
+by (Blast_tac 1);
+qed "metric_less";
+AddSIs [metric_less];
+
+Goal "metric (s(y:=s x | s y)) <= metric s";
+by (case_tac "s x --> s y" 1);
+by (auto_tac (claset() addIs [less_imp_le],
+ simpset() addsimps [fun_upd_idem]));
+qed "metric_le";
+
+Goal "Rprg : ((metric-`{m}) - fixedpoint) LeadsTo (metric-`(lessThan m))";
+by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
+by (rtac LeadsTo_UN 1);
+by Auto_tac;
+by (ensures_tac "asgt a b" 1);
+by (Blast_tac 2);
+by (full_simp_tac (simpset() addsimps [not_less_iff_le]) 1);
+by (dtac (metric_le RS order_antisym) 1);
+by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)],
+ simpset()));
+qed "LeadsTo_Diff_fixedpoint";
+
+Goal "Rprg : (metric-`{m}) LeadsTo (metric-`(lessThan m) Un fixedpoint)";
+by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R,
+ subset_imp_LeadsTo] MRS LeadsTo_Diff) 1);
+by Auto_tac;
+qed "LeadsTo_Un_fixedpoint";
+
+
+(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
+Goal "Rprg : UNIV LeadsTo fixedpoint";
+by (rtac LessThan_induct 1);
+by Auto_tac;
+by (rtac LeadsTo_Un_fixedpoint 1);
+qed "LeadsTo_fixedpoint";
+
+Goal "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }";
+by (stac (fixedpoint_invariant_correct RS sym) 1);
+by (rtac ([reach_invariant, LeadsTo_fixedpoint]
+ MRS Always_LeadsTo_weaken) 1);
+by Auto_tac;
+qed "LeadsTo_correct";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Reach.thy Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,43 @@
+(* Title: HOL/UNITY/Reach.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Reachability in Directed Graphs. From Chandy and Misra, section 6.4.
+*)
+
+Reach = FP + SubstAx +
+
+types vertex
+ state = "vertex=>bool"
+
+arities vertex :: term
+
+consts
+ init :: "vertex"
+
+ edges :: "(vertex*vertex) set"
+
+constdefs
+
+ asgt :: "[vertex,vertex] => (state*state) set"
+ "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)"
+
+ reach_invariant :: state set
+ "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
+
+ fixedpoint :: state set
+ "fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
+
+ metric :: state => nat
+ "metric s == card {v. ~ s v}"
+
+rules
+
+ (*We assume that the set of vertices is finite*)
+ finite_graph "finite (UNIV :: vertex set)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Reachability.ML Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,308 @@
+(* Title: HOL/UNITY/Reachability
+ ID: $Id$
+ Author: Tanja Vos, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Reachability in Graphs
+
+From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
+*)
+
+bind_thm("E_imp_in_V_L", Graph2 RS conjunct1);
+bind_thm("E_imp_in_V_R", Graph2 RS conjunct2);
+
+Goal "(v,w) : E ==> F : reachable v LeadsTo nmsg_eq 0 (v,w) Int reachable v";
+by (rtac (MA7 RS PSP_Stable RS LeadsTo_weaken_L) 1);
+by (rtac MA6 3);
+by (auto_tac (claset(), simpset() addsimps [E_imp_in_V_L, E_imp_in_V_R]));
+qed "lemma2";
+
+Goal "(v,w) : E ==> F : reachable v LeadsTo reachable w";
+by (rtac (MA4 RS Always_LeadsTo_weaken) 1);
+by (rtac lemma2 2);
+by (auto_tac (claset(), simpset() addsimps [nmsg_eq_def, nmsg_gt_def]));
+qed "Induction_base";
+
+Goal "(v,w) : REACHABLE ==> F : reachable v LeadsTo reachable w";
+by (etac REACHABLE.induct 1);
+by (rtac subset_imp_LeadsTo 1);
+by (Blast_tac 1);
+by (blast_tac (claset() addIs [LeadsTo_Trans, Induction_base]) 1);
+qed "REACHABLE_LeadsTo_reachable";
+
+Goal "F : {s. (root,v) : REACHABLE} LeadsTo reachable v";
+by (rtac single_LeadsTo_I 1);
+by (full_simp_tac (simpset() addsplits [split_if_asm]) 1);
+by (rtac (MA1 RS Always_LeadsToI) 1);
+by (etac (REACHABLE_LeadsTo_reachable RS LeadsTo_weaken_L) 1);
+by Auto_tac;
+qed "Detects_part1";
+
+
+Goalw [Detects_def]
+ "v : V ==> F : (reachable v) Detects {s. (root,v) : REACHABLE}";
+by Auto_tac;
+by (blast_tac (claset() addIs [MA2 RS Always_weaken]) 2);
+by (rtac (Detects_part1 RS LeadsTo_weaken_L) 1);
+by (Blast_tac 1);
+qed "Reachability_Detected";
+
+
+Goal "v : V ==> F : UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE})";
+by (etac (Reachability_Detected RS Detects_Imp_LeadstoEQ) 1);
+qed "LeadsTo_Reachability";
+
+(* ------------------------------------ *)
+
+(* Some lemmas about <==> *)
+
+Goalw [Equality_def]
+ "(reachable v <==> {s. (root,v) : REACHABLE}) = \
+\ {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
+by (Blast_tac 1);
+qed "Eq_lemma1";
+
+
+Goalw [Equality_def]
+ "(reachable v <==> (if (root,v) : REACHABLE then UNIV else {})) = \
+\ {s. ((s : reachable v) = ((root,v) : REACHABLE))}";
+by Auto_tac;
+qed "Eq_lemma2";
+
+(* ------------------------------------ *)
+
+
+(* Some lemmas about final (I don't need all of them!) *)
+
+Goalw [final_def, Equality_def]
+ "(INT v: V. INT w:V. {s. ((s : reachable v) = ((root,v) : REACHABLE)) & \
+\ s : nmsg_eq 0 (v,w)}) \
+\ <= final";
+by Auto_tac;
+by (ftac E_imp_in_V_R 1);
+by (ftac E_imp_in_V_L 1);
+by (Blast_tac 1);
+qed "final_lemma1";
+
+Goalw [final_def, Equality_def]
+ "E~={} \
+\ ==> (INT v: V. INT e: E. {s. ((s : reachable v) = ((root,v) : REACHABLE))} \
+\ Int nmsg_eq 0 e) <= final";
+by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
+by (ftac E_imp_in_V_L 1);
+by (Blast_tac 1);
+qed "final_lemma2";
+
+Goal "E~={} \
+\ ==> (INT v: V. INT e: E. \
+\ (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
+\ <= final";
+by (ftac final_lemma2 1);
+by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
+qed "final_lemma3";
+
+
+Goal "E~={} \
+\ ==> (INT v: V. INT e: E. \
+\ {s. ((s : reachable v) = ((root,v) : REACHABLE))} Int nmsg_eq 0 e) \
+\ = final";
+by (rtac subset_antisym 1);
+by (etac final_lemma2 1);
+by (rewrite_goals_tac [final_def,Equality_def]);
+by (Blast_tac 1);
+qed "final_lemma4";
+
+Goal "E~={} \
+\ ==> (INT v: V. INT e: E. \
+\ ((reachable v) <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 e) \
+\ = final";
+by (ftac final_lemma4 1);
+by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
+qed "final_lemma5";
+
+
+Goal "(INT v: V. INT w: V. \
+\ (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)) \
+\ <= final";
+by (simp_tac (simpset() addsimps [Eq_lemma2, Int_def]) 1);
+by (rtac final_lemma1 1);
+qed "final_lemma6";
+
+
+Goalw [final_def]
+ "final = \
+\ (INT v: V. INT w: V. \
+\ ((reachable v) <==> {s. (root,v) : REACHABLE}) Int \
+\ (-{s. (v,w) : E} Un (nmsg_eq 0 (v,w))))";
+by (rtac subset_antisym 1);
+by (Blast_tac 1);
+by (auto_tac (claset(), simpset() addsplits [split_if_asm]));
+by (ftac E_imp_in_V_R 1);
+by (ftac E_imp_in_V_L 1);
+by (Blast_tac 1);
+qed "final_lemma7";
+
+(* ------------------------------------ *)
+
+
+(* ------------------------------------ *)
+
+(* Stability theorems *)
+
+
+Goal "[| v : V; (root,v) ~: REACHABLE |] ==> F : Stable (- reachable v)";
+by (dtac (MA2 RS AlwaysD) 1);
+by Auto_tac;
+qed "not_REACHABLE_imp_Stable_not_reachable";
+
+Goal "v : V ==> F : Stable (reachable v <==> {s. (root,v) : REACHABLE})";
+by (simp_tac (simpset() addsimps [Equality_def, Eq_lemma2]) 1);
+by (blast_tac (claset() addIs [MA6,not_REACHABLE_imp_Stable_not_reachable]) 1);
+qed "Stable_reachable_EQ_R";
+
+
+Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
+ "((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
+\ <= A Un nmsg_eq 0 (v,w)";
+by Auto_tac;
+qed "lemma4";
+
+
+Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
+ "reachable v Int nmsg_eq 0 (v,w) = \
+\ ((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int \
+\ (reachable v Int nmsg_lte 0 (v,w)))";
+by Auto_tac;
+qed "lemma5";
+
+Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
+ "- nmsg_gt 0 (v,w) Un reachable v <= nmsg_eq 0 (v,w) Un reachable v";
+by Auto_tac;
+qed "lemma6";
+
+Goal "[|v : V; w : V|] ==> F : Always (reachable v Un nmsg_eq 0 (v,w))";
+by (rtac ([MA5, MA3] MRS Always_Int_I RS Always_weaken) 1);
+by (rtac lemma4 5);
+by Auto_tac;
+qed "Always_reachable_OR_nmsg_0";
+
+Goal "[|v : V; w : V|] ==> F : Stable (reachable v Int nmsg_eq 0 (v,w))";
+by (stac lemma5 1);
+by (blast_tac (claset() addIs [MA5, Always_imp_Stable RS Stable_Int, MA6b]) 1);
+qed "Stable_reachable_AND_nmsg_0";
+
+Goal "[|v : V; w : V|] ==> F : Stable (nmsg_eq 0 (v,w) Un reachable v)";
+by (blast_tac (claset() addSIs [Always_weaken RS Always_imp_Stable,
+ lemma6, MA3]) 1);
+qed "Stable_nmsg_0_OR_reachable";
+
+Goal "[| v : V; w:V; (root,v) ~: REACHABLE |] \
+\ ==> F : Stable (- reachable v Int nmsg_eq 0 (v,w))";
+by (rtac ([MA2 RS Always_imp_Stable, Stable_nmsg_0_OR_reachable] MRS
+ Stable_Int RS Stable_eq) 1);
+by (Blast_tac 4);
+by Auto_tac;
+qed "not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0";
+
+Goal "[| v : V; w:V |] \
+\ ==> F : Stable ((reachable v <==> {s. (root,v) : REACHABLE}) Int \
+\ nmsg_eq 0 (v,w))";
+by (asm_simp_tac
+ (simpset() addsimps [Equality_def, Eq_lemma2,
+ not_REACHABLE_imp_Stable_not_reachable_AND_nmsg_0,
+ Stable_reachable_AND_nmsg_0]) 1);
+qed "Stable_reachable_EQ_R_AND_nmsg_0";
+
+
+(* ------------------------------------ *)
+
+
+(* LeadsTo final predicate (Exercise 11.2 page 274) *)
+
+Goal "UNIV <= (INT v: V. UNIV)";
+by (Blast_tac 1);
+val UNIV_lemma = result();
+
+val UNIV_LeadsTo_completion =
+ [Finite_stable_completion, UNIV_lemma] MRS LeadsTo_weaken_L;
+
+Goalw [final_def] "E={} ==> F : UNIV LeadsTo final";
+by (Asm_full_simp_tac 1);
+by (rtac UNIV_LeadsTo_completion 1);
+by Safe_tac;
+by (etac (simplify (simpset()) LeadsTo_Reachability) 1);
+by (dtac Stable_reachable_EQ_R 1);
+by (Asm_full_simp_tac 1);
+qed "LeadsTo_final_E_empty";
+
+
+Goal "[| v : V; w:V |] \
+\ ==> F : UNIV LeadsTo \
+\ ((reachable v <==> {s. (root,v): REACHABLE}) Int nmsg_eq 0 (v,w))";
+by (rtac (LeadsTo_Reachability RS LeadsTo_Trans) 1);
+by (Blast_tac 1);
+by (subgoal_tac "F : (reachable v <==> {s. (root,v) : REACHABLE}) Int UNIV LeadsTo (reachable v <==> {s. (root,v) : REACHABLE}) Int nmsg_eq 0 (v,w)" 1);
+by (Asm_full_simp_tac 1);
+by (rtac PSP_Stable2 1);
+by (rtac MA7 1);
+by (rtac Stable_reachable_EQ_R 3);
+by Auto_tac;
+qed "Leadsto_reachability_AND_nmsg_0";
+
+
+Goal "E~={} ==> F : UNIV LeadsTo final";
+by (rtac ([LeadsTo_weaken_R, UNIV_lemma] MRS LeadsTo_weaken_L) 1);
+by (rtac final_lemma6 2);
+by (rtac Finite_stable_completion 1);
+by (Blast_tac 1);
+by (rtac UNIV_LeadsTo_completion 1);
+by (REPEAT
+ (blast_tac (claset() addIs [Stable_INT,
+ Stable_reachable_EQ_R_AND_nmsg_0,
+ Leadsto_reachability_AND_nmsg_0]) 1));
+qed "LeadsTo_final_E_NOT_empty";
+
+
+Goal "F : UNIV LeadsTo final";
+by (case_tac "E={}" 1);
+by (rtac LeadsTo_final_E_NOT_empty 2);
+by (rtac LeadsTo_final_E_empty 1);
+by Auto_tac;
+qed "LeadsTo_final";
+
+(* ------------------------------------ *)
+
+(* Stability of final (Exercise 11.2 page 274) *)
+
+Goalw [final_def] "E={} ==> F : Stable final";
+by (Asm_full_simp_tac 1);
+by (rtac Stable_INT 1);
+by (dtac Stable_reachable_EQ_R 1);
+by (Asm_full_simp_tac 1);
+qed "Stable_final_E_empty";
+
+
+Goal "E~={} ==> F : Stable final";
+by (stac final_lemma7 1);
+by (rtac Stable_INT 1);
+by (rtac Stable_INT 1);
+by (simp_tac (simpset() addsimps [Eq_lemma2]) 1);
+by Safe_tac;
+by (rtac Stable_eq 1);
+by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)} Int nmsg_eq 0 (v,w)) = \
+\ ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- UNIV Un nmsg_eq 0 (v,w)))" 2);
+by (Blast_tac 2); by (Blast_tac 2);
+by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R_AND_nmsg_0) 1);
+by (Blast_tac 1);by (Blast_tac 1);
+by (rtac Stable_eq 1);
+by (subgoal_tac "({s. (s : reachable v) = ((root,v) : REACHABLE)}) = ({s. (s : reachable v) = ((root,v) : REACHABLE)} Int (- {} Un nmsg_eq 0 (v,w)))" 2);
+by (Blast_tac 2); by (Blast_tac 2);
+by (rtac (simplify (simpset() addsimps [Eq_lemma2]) Stable_reachable_EQ_R) 1);
+by Auto_tac;
+qed "Stable_final_E_NOT_empty";
+
+Goal "F : Stable final";
+by (case_tac "E={}" 1);
+by (blast_tac (claset() addIs [Stable_final_E_NOT_empty]) 2);
+by (blast_tac (claset() addIs [Stable_final_E_empty]) 1);
+qed "Stable_final";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Reachability.thy Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,72 @@
+(* Title: HOL/UNITY/Reachability
+ ID: $Id$
+ Author: Tanja Vos, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Reachability in Graphs
+
+From Chandy and Misra, "Parallel Program Design" (1989), sections 6.2 and 11.3
+*)
+
+Reachability = Detects +
+
+types edge = "(vertex*vertex)"
+
+record state =
+ reach :: vertex => bool
+ nmsg :: edge => nat
+
+consts REACHABLE :: edge set
+ root :: vertex
+ E :: edge set
+ V :: vertex set
+
+inductive "REACHABLE"
+ intrs
+ base "v : V ==> ((v,v) : REACHABLE)"
+ step "((u,v) : REACHABLE) & (v,w) : E ==> ((u,w) : REACHABLE)"
+
+constdefs
+ reachable :: vertex => state set
+ "reachable p == {s. reach s p}"
+
+ nmsg_eq :: nat => edge => state set
+ "nmsg_eq k == %e. {s. nmsg s e = k}"
+
+ nmsg_gt :: nat => edge => state set
+ "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_lte :: nat => edge => state set
+ "nmsg_lte k == %e. {s. nmsg s e <= k}"
+
+
+
+ final :: state set
+ "final == (INTER V (%v. reachable v <==> {s. (root, v) : REACHABLE})) Int (INTER E (nmsg_eq 0))"
+
+rules
+ Graph1 "root : V"
+
+ Graph2 "(v,w) : E ==> (v : V) & (w : V)"
+
+ MA1 "F : Always (reachable root)"
+
+ MA2 "[|v:V|] ==> F : Always (- reachable v Un {s. ((root,v) : REACHABLE)})"
+
+ MA3 "[|v:V;w:V|] ==> F : Always (-(nmsg_gt 0 (v,w)) Un (reachable v))"
+
+ MA4 "[|(v,w) : E|] ==> F : Always (-(reachable v) Un (nmsg_gt 0 (v,w)) Un (reachable w))"
+
+ MA5 "[|v:V;w:V|] ==> F : Always (nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w))"
+
+ MA6 "[|v:V|] ==> F : Stable (reachable v)"
+
+ MA6b "[|v:V;w:W|] ==> F : Stable (reachable v Int nmsg_lte k (v,w))"
+
+ MA7 "[|v:V;w:V|] ==> F : UNIV LeadsTo nmsg_eq 0 (v,w)"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Token.ML Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,101 @@
+(* Title: HOL/UNITY/Token
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Token Ring.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
+*)
+
+val Token_defs = [HasTok_def, H_def, E_def, T_def];
+
+Goalw [HasTok_def] "[| s: HasTok i; s: HasTok j |] ==> i=j";
+by Auto_tac;
+qed "HasToK_partition";
+
+Goalw Token_defs "(s ~: E i) = (s : H i | s : T i)";
+by (Simp_tac 1);
+by (case_tac "proc s i" 1);
+by Auto_tac;
+qed "not_E_eq";
+
+Open_locale "Token";
+
+val TR2 = thm "TR2";
+val TR3 = thm "TR3";
+val TR4 = thm "TR4";
+val TR5 = thm "TR5";
+val TR6 = thm "TR6";
+val TR7 = thm "TR7";
+val nodeOrder_def = thm "nodeOrder_def";
+val next_def = thm "next_def";
+
+AddIffs [thm "N_positive"];
+
+Goalw [stable_def] "F : stable (-(E i) Un (HasTok i))";
+by (rtac constrains_weaken 1);
+by (rtac ([[TR2, TR4] MRS constrains_Un, TR5] MRS constrains_Un) 1);
+by (auto_tac (claset(), simpset() addsimps [not_E_eq]));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [H_def, E_def, T_def])));
+qed "token_stable";
+
+
+(*** Progress under weak fairness ***)
+
+Goalw [nodeOrder_def] "wf(nodeOrder j)";
+by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
+by (Blast_tac 1);
+qed"wf_nodeOrder";
+
+Goalw [nodeOrder_def, next_def, inv_image_def]
+ "[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
+by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq]));
+by (auto_tac (claset(),
+ simpset() addsplits [nat_diff_split]
+ addsimps [linorder_neq_iff, mod_geq]));
+qed "nodeOrder_eq";
+
+(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
+ Note the use of case_tac. Reasoning about leadsTo takes practice!*)
+Goal "[| i<N; j<N |] ==> \
+\ F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)";
+by (case_tac "i=j" 1);
+by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
+by (rtac (TR7 RS leadsTo_weaken_R) 1);
+by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
+qed "TR7_nodeOrder";
+
+
+(*Chapter 4 variant, the one actually used below.*)
+Goal "[| i<N; j<N; i~=j |] \
+\ ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}";
+by (rtac (TR7 RS leadsTo_weaken_R) 1);
+by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
+qed "TR7_aux";
+
+Goal "({s. token s < N} Int token -` {m}) = (if m<N then token -` {m} else {})";
+by Auto_tac;
+val token_lemma = result();
+
+
+(*Misra's TR9: the token reaches an arbitrary node*)
+Goal "j<N ==> F : {s. token s < N} leadsTo (HasTok j)";
+by (rtac leadsTo_weaken_R 1);
+by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
+ (wf_nodeOrder RS bounded_induct) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff,
+ HasTok_def])));
+by (Blast_tac 2);
+by (Clarify_tac 1);
+by (rtac (TR7_aux RS leadsTo_weaken) 1);
+by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_def]));
+qed "leadsTo_j";
+
+(*Misra's TR8: a hungry process eventually eats*)
+Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)";
+by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
+by (rtac TR6 2);
+by (rtac ([leadsTo_j, TR3] MRS psp RS leadsTo_weaken) 1);
+by (ALLGOALS Blast_tac);
+qed "token_progress";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/Token.thy Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,66 @@
+(* Title: HOL/UNITY/Token
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+The Token Ring.
+
+From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
+*)
+
+
+Token = WFair +
+
+(*process states*)
+datatype pstate = Hungry | Eating | Thinking
+
+record state =
+ token :: nat
+ proc :: nat => pstate
+
+
+constdefs
+ HasTok :: nat => state set
+ "HasTok i == {s. token s = i}"
+
+ H :: nat => state set
+ "H i == {s. proc s i = Hungry}"
+
+ E :: nat => state set
+ "E i == {s. proc s i = Eating}"
+
+ T :: nat => state set
+ "T i == {s. proc s i = Thinking}"
+
+
+locale Token =
+ fixes
+ N :: nat (*number of nodes in the ring*)
+ F :: state program
+ nodeOrder :: "nat => (nat*nat)set"
+ next :: nat => nat
+
+ assumes
+ N_positive "0<N"
+
+ TR2 "F : (T i) co (T i Un H i)"
+
+ TR3 "F : (H i) co (H i Un E i)"
+
+ TR4 "F : (H i - HasTok i) co (H i)"
+
+ TR5 "F : (HasTok i) co (HasTok i Un -(E i))"
+
+ TR6 "F : (H i Int HasTok i) leadsTo (E i)"
+
+ TR7 "F : (HasTok i) leadsTo (HasTok (next i))"
+
+ defines
+ nodeOrder_def
+ "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int
+ (lessThan N <*> lessThan N)"
+
+ next_def
+ "next i == (Suc i) mod N"
+
+end