# HG changeset patch # User paulson # Date 983803631 -3600 # Node ID 65ede8dfe3041619f77c901554681d53c12dd205 # Parent ea13ff5a26d125531f4fbdad860c85f04be29376 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Channel.ML --- /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"; diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Channel.thy --- /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 diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Common.ML --- /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 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"; diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Common.thy --- /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 diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Deadlock.ML --- /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(); + diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Deadlock.thy --- /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 diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Lift.ML --- /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 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 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 \ +\ 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 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 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"; diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Lift.thy --- /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 diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Mutex.ML --- /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"; diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Mutex.thy --- /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 diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/NSP_Bad.ML --- /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 +*) diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/NSP_Bad.thy --- /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 diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Network.ML --- /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(); + + + + diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Network.thy --- /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 diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/README.html --- /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 @@ + +HOL/UNITY/README + +

UNITY: Examples Involving Single Programs

+ +

The directory presents verification examples that do not involve program +composition. They are mostly taken from Misra's 1994 papers on ``New UNITY'': +

+ +
+

Last modified on $Date$ + +

+lcp@cl.cam.ac.uk +
+ diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Reach.ML --- /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"; diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Reach.thy --- /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 diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Reachability.ML --- /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"; diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Reachability.thy --- /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 + diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Token.ML --- /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 ((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 \ +\ 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 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 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 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"; diff -r ea13ff5a26d1 -r 65ede8dfe304 src/HOL/UNITY/Simple/Token.thy --- /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 lessThan N)" + + next_def + "next i == (Suc i) mod N" + +end