# HG changeset patch # User paulson # Date 983802311 -3600 # Node ID 851c90b23a9ef1989b8a967edeaa1051481680bf # Parent 5fd02b905a9a2b2e96c2674a67dc6bfcdb733a90 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Mar 05 12:31:31 2001 +0100 +++ b/src/HOL/IsaMakefile Mon Mar 05 15:25:11 2001 +0100 @@ -320,28 +320,39 @@ HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz $(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ - UNITY/Alloc.ML UNITY/Alloc.thy UNITY/AllocBase.ML UNITY/AllocBase.thy \ - UNITY/Channel.ML UNITY/Channel.thy UNITY/Client.ML UNITY/Client.thy \ - UNITY/Common.ML UNITY/Common.thy UNITY/Comp.ML UNITY/Comp.thy \ - UNITY/Counter.ML UNITY/Counter.thy UNITY/Counterc.ML UNITY/Counterc.thy \ - UNITY/Deadlock.ML UNITY/Deadlock.thy UNITY/Detects.ML \ - UNITY/Detects.thy UNITY/ELT.ML UNITY/ELT.thy UNITY/Extend.ML \ + UNITY/Comp.ML UNITY/Comp.thy \ + UNITY/Detects.ML UNITY/Detects.thy \ + UNITY/ELT.ML UNITY/ELT.thy UNITY/Extend.ML \ UNITY/Extend.thy UNITY/FP.ML UNITY/FP.thy UNITY/Follows.ML \ UNITY/Follows.thy UNITY/GenPrefix.ML UNITY/GenPrefix.thy \ - UNITY/Guar.ML UNITY/Guar.thy UNITY/Handshake.ML UNITY/Handshake.thy \ - UNITY/Lift.ML UNITY/Lift.thy UNITY/Lift_prog.ML UNITY/Lift_prog.thy \ - UNITY/ListOrder.thy UNITY/Mutex.ML UNITY/Mutex.thy UNITY/NSP_Bad.ML \ - UNITY/NSP_Bad.thy UNITY/Network.ML UNITY/Network.thy \ + UNITY/Guar.ML UNITY/Guar.thy \ + UNITY/Lift_prog.ML UNITY/Lift_prog.thy \ + UNITY/ListOrder.thy \ UNITY/PPROD.ML UNITY/PPROD.thy \ - UNITY/PriorityAux.ML UNITY/PriorityAux.thy \ - UNITY/Priority.ML UNITY/Priority.thy \ UNITY/Project.ML UNITY/Project.thy \ - UNITY/Reach.ML UNITY/Reach.thy UNITY/Reachability.ML \ - UNITY/Reachability.thy UNITY/Rename.ML UNITY/Rename.thy \ - UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/TimerArray.ML \ - UNITY/TimerArray.thy UNITY/Token.ML UNITY/Token.thy UNITY/UNITY.ML \ + UNITY/Rename.ML UNITY/Rename.thy \ + UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML \ UNITY/UNITY.thy UNITY/Union.ML UNITY/Union.thy UNITY/WFair.ML \ - UNITY/WFair.thy + UNITY/WFair.thy \ + UNITY/Simple/Channel.ML UNITY/Simple/Channel.thy \ + UNITY/Simple/Common.ML UNITY/Simple/Common.thy \ + UNITY/Simple/Deadlock.ML UNITY/Simple/Deadlock.thy \ + UNITY/Simple/Lift.ML UNITY/Simple/Lift.thy \ + UNITY/Simple/Mutex.ML UNITY/Simple/Mutex.thy \ + UNITY/Simple/NSP_Bad.ML UNITY/Simple/NSP_Bad.thy \ + UNITY/Simple/Network.ML UNITY/Simple/Network.thy \ + UNITY/Simple/Reach.ML UNITY/Simple/Reach.thy \ + UNITY/Simple/Reachability.ML UNITY/Simple/Reachability.thy \ + UNITY/Simple/Token.ML UNITY/Simple/Token.thy \ + UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \ + UNITY/Comp/AllocBase.ML UNITY/Comp/AllocBase.thy \ + UNITY/Comp/Client.ML UNITY/Comp/Client.thy \ + UNITY/Comp/Counter.ML UNITY/Comp/Counter.thy \ + UNITY/Comp/Counterc.ML UNITY/Comp/Counterc.thy \ + UNITY/Comp/Handshake.ML UNITY/Comp/Handshake.thy \ + UNITY/Comp/PriorityAux.ML UNITY/Comp/PriorityAux.thy \ + UNITY/Comp/Priority.ML UNITY/Comp/Priority.thy \ + UNITY/Comp/TimerArray.ML UNITY/Comp/TimerArray.thy @$(ISATOOL) usedir $(OUT)/HOL UNITY diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Alloc.ML --- a/src/HOL/UNITY/Alloc.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,744 +0,0 @@ -(* Title: HOL/UNITY/Alloc - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Specification of Chandy and Charpentier's Allocator -*) - -(*Perhaps equalities.ML shouldn't add this in the first place!*) -Delsimps [image_Collect]; - -AddIs [impOfSubs subset_preserves_o]; -Addsimps [impOfSubs subset_preserves_o]; -Addsimps [funPair_o_distrib]; -Addsimps [Always_INT_distrib]; -Delsimps [o_apply]; - -(*Eliminate the "o" operator*) -val o_simp = simplify (simpset() addsimps [o_def]); - -(*For rewriting of specifications related by "guarantees"*) -Addsimps [rename_image_constrains, rename_image_stable, - rename_image_increasing, rename_image_invariant, - rename_image_Constrains, rename_image_Stable, - rename_image_Increasing, rename_image_Always, - rename_image_leadsTo, rename_image_LeadsTo, - rename_preserves, rename_image_preserves, lift_image_preserves, - bij_image_INT, bij_is_inj RS image_Int, bij_image_Collect_eq]; - -(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*) -fun list_of_Int th = - (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2)) - handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2)) - handle THM _ => (list_of_Int (th RS INT_D)) - handle THM _ => (list_of_Int (th RS bspec)) - handle THM _ => [th]; - -(*Used just once, for Alloc_Increasing*) -val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec); -fun normalize th = - normalize (th RS spec - handle THM _ => th RS lessThanBspec - handle THM _ => th RS bspec - handle THM _ => th RS (guarantees_INT_right_iff RS iffD1)) - handle THM _ => th; - - - -(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***) - -val record_auto_tac = - auto_tac (claset() addIs [ext] addSWrapper record_split_wrapper, - simpset() addsimps [sysOfAlloc_def, sysOfClient_def, - client_map_def, non_dummy_def, funPair_def, - o_apply, Let_def]); - - -Goalw [sysOfAlloc_def, Let_def] "inj sysOfAlloc"; -by (rtac injI 1); -by record_auto_tac; -qed "inj_sysOfAlloc"; -AddIffs [inj_sysOfAlloc]; - -(*We need the inverse; also having it simplifies the proof of surjectivity*) -Goal "!!s. inv sysOfAlloc s = \ -\ (| allocGiv = allocGiv s, \ -\ allocAsk = allocAsk s, \ -\ allocRel = allocRel s, \ -\ allocState_d.dummy = (client s, dummy s) |)"; -by (rtac (inj_sysOfAlloc RS inv_f_eq) 1); -by record_auto_tac; -qed "inv_sysOfAlloc_eq"; -Addsimps [inv_sysOfAlloc_eq]; - -Goal "surj sysOfAlloc"; -by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); -by record_auto_tac; -qed "surj_sysOfAlloc"; -AddIffs [surj_sysOfAlloc]; - -Goal "bij sysOfAlloc"; -by (blast_tac (claset() addIs [bijI]) 1); -qed "bij_sysOfAlloc"; -AddIffs [bij_sysOfAlloc]; - - -(*** bijectivity of sysOfClient ***) - -Goalw [sysOfClient_def] "inj sysOfClient"; -by (rtac injI 1); -by record_auto_tac; -qed "inj_sysOfClient"; -AddIffs [inj_sysOfClient]; - -Goal "!!s. inv sysOfClient s = \ -\ (client s, \ -\ (| allocGiv = allocGiv s, \ -\ allocAsk = allocAsk s, \ -\ allocRel = allocRel s, \ -\ allocState_d.dummy = systemState.dummy s|) )"; -by (rtac (inj_sysOfClient RS inv_f_eq) 1); -by record_auto_tac; -qed "inv_sysOfClient_eq"; -Addsimps [inv_sysOfClient_eq]; - -Goal "surj sysOfClient"; -by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); -by record_auto_tac; -qed "surj_sysOfClient"; -AddIffs [surj_sysOfClient]; - -Goal "bij sysOfClient"; -by (blast_tac (claset() addIs [bijI]) 1); -qed "bij_sysOfClient"; -AddIffs [bij_sysOfClient]; - - -(*** bijectivity of client_map ***) - -Goalw [inj_on_def] "inj client_map"; -by record_auto_tac; -qed "inj_client_map"; -AddIffs [inj_client_map]; - -Goal "!!s. inv client_map s = \ -\ (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, \ -\ clientState_d.dummy = y|)) s"; -by (rtac (inj_client_map RS inv_f_eq) 1); -by record_auto_tac; -qed "inv_client_map_eq"; -Addsimps [inv_client_map_eq]; - -Goal "surj client_map"; -by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); -by record_auto_tac; -qed "surj_client_map"; -AddIffs [surj_client_map]; - -Goal "bij client_map"; -by (blast_tac (claset() addIs [bijI]) 1); -qed "bij_client_map"; -AddIffs [bij_client_map]; - - -(** o-simprules for client_map **) - -Goalw [client_map_def] "fst o client_map = non_dummy"; -by (rtac fst_o_funPair 1); -qed "fst_o_client_map"; -Addsimps (make_o_equivs fst_o_client_map); - -Goalw [client_map_def] "snd o client_map = clientState_d.dummy"; -by (rtac snd_o_funPair 1); -qed "snd_o_client_map"; -Addsimps (make_o_equivs snd_o_client_map); - -(** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **) - -Goal "client o sysOfAlloc = fst o allocState_d.dummy "; -by record_auto_tac; -qed "client_o_sysOfAlloc"; -Addsimps (make_o_equivs client_o_sysOfAlloc); - -Goal "allocGiv o sysOfAlloc = allocGiv"; -by record_auto_tac; -qed "allocGiv_o_sysOfAlloc_eq"; -Addsimps (make_o_equivs allocGiv_o_sysOfAlloc_eq); - -Goal "allocAsk o sysOfAlloc = allocAsk"; -by record_auto_tac; -qed "allocAsk_o_sysOfAlloc_eq"; -Addsimps (make_o_equivs allocAsk_o_sysOfAlloc_eq); - -Goal "allocRel o sysOfAlloc = allocRel"; -by record_auto_tac; -qed "allocRel_o_sysOfAlloc_eq"; -Addsimps (make_o_equivs allocRel_o_sysOfAlloc_eq); - -(** o-simprules for sysOfClient [MUST BE AUTOMATED] **) - -Goal "client o sysOfClient = fst"; -by record_auto_tac; -qed "client_o_sysOfClient"; -Addsimps (make_o_equivs client_o_sysOfClient); - -Goal "allocGiv o sysOfClient = allocGiv o snd "; -by record_auto_tac; -qed "allocGiv_o_sysOfClient_eq"; -Addsimps (make_o_equivs allocGiv_o_sysOfClient_eq); - -Goal "allocAsk o sysOfClient = allocAsk o snd "; -by record_auto_tac; -qed "allocAsk_o_sysOfClient_eq"; -Addsimps (make_o_equivs allocAsk_o_sysOfClient_eq); - -Goal "allocRel o sysOfClient = allocRel o snd "; -by record_auto_tac; -qed "allocRel_o_sysOfClient_eq"; -Addsimps (make_o_equivs allocRel_o_sysOfClient_eq); - -Goal "allocGiv o inv sysOfAlloc = allocGiv"; -by (simp_tac (simpset() addsimps [o_def]) 1); -qed "allocGiv_o_inv_sysOfAlloc_eq"; -Addsimps (make_o_equivs allocGiv_o_inv_sysOfAlloc_eq); - -Goal "allocAsk o inv sysOfAlloc = allocAsk"; -by (simp_tac (simpset() addsimps [o_def]) 1); -qed "allocAsk_o_inv_sysOfAlloc_eq"; -Addsimps (make_o_equivs allocAsk_o_inv_sysOfAlloc_eq); - -Goal "allocRel o inv sysOfAlloc = allocRel"; -by (simp_tac (simpset() addsimps [o_def]) 1); -qed "allocRel_o_inv_sysOfAlloc_eq"; -Addsimps (make_o_equivs allocRel_o_inv_sysOfAlloc_eq); - -Goal "(rel o inv client_map o drop_map i o inv sysOfClient) = \ -\ rel o sub i o client"; -by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1); -qed "rel_inv_client_map_drop_map"; -Addsimps (make_o_equivs rel_inv_client_map_drop_map); - -Goal "(ask o inv client_map o drop_map i o inv sysOfClient) = \ -\ ask o sub i o client"; -by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1); -qed "ask_inv_client_map_drop_map"; -Addsimps (make_o_equivs ask_inv_client_map_drop_map); - -(** -Open_locale "System"; - -val Alloc = thm "Alloc"; -val Client = thm "Client"; -val Network = thm "Network"; -val System_def = thm "System_def"; - -CANNOT use bind_thm: it puts the theorem into standard form, in effect - exporting it from the locale -**) - -AddIffs [finite_lessThan]; - -(*Client : *) -val client_spec_simps = - [client_spec_def, client_increasing_def, client_bounded_def, - client_progress_def, client_allowed_acts_def, client_preserves_def, - guarantees_Int_right]; - -val [Client_Increasing_ask, Client_Increasing_rel, - Client_Bounded, Client_Progress, Client_AllowedActs, - Client_preserves_giv, Client_preserves_dummy] = - Client |> simplify (simpset() addsimps client_spec_simps) - |> list_of_Int; - -AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded, - Client_preserves_giv, Client_preserves_dummy]; - - -(*Network : *) -val network_spec_simps = - [network_spec_def, network_ask_def, network_giv_def, - network_rel_def, network_allowed_acts_def, network_preserves_def, - ball_conj_distrib]; - -val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs, - Network_preserves_allocGiv, Network_preserves_rel, - Network_preserves_ask] = - Network |> simplify (simpset() addsimps network_spec_simps) - |> list_of_Int; - -AddIffs [Network_preserves_allocGiv]; - -Addsimps [Network_preserves_rel, Network_preserves_ask]; -Addsimps [o_simp Network_preserves_rel, o_simp Network_preserves_ask]; - - -(*Alloc : *) -val alloc_spec_simps = - [alloc_spec_def, alloc_increasing_def, alloc_safety_def, - alloc_progress_def, alloc_allowed_acts_def, - alloc_preserves_def]; - -val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs, - Alloc_preserves_allocRel, Alloc_preserves_allocAsk, - Alloc_preserves_dummy] = - Alloc |> simplify (simpset() addsimps alloc_spec_simps) - |> list_of_Int; - -(*Strip off the INT in the guarantees postcondition*) -val Alloc_Increasing = normalize Alloc_Increasing_0; - -AddIffs [Alloc_preserves_allocRel, Alloc_preserves_allocAsk, - Alloc_preserves_dummy]; - -(** Components lemmas [MUST BE AUTOMATED] **) - -Goal "Network Join \ -\ ((rename sysOfClient \ -\ (plam x: (lessThan Nclients). rename client_map Client)) Join \ -\ rename sysOfAlloc Alloc) \ -\ = System"; -by (simp_tac (simpset() addsimps System_def::Join_ac) 1); -qed "Network_component_System"; - -Goal "(rename sysOfClient \ -\ (plam x: (lessThan Nclients). rename client_map Client)) Join \ -\ (Network Join rename sysOfAlloc Alloc) = System"; -by (simp_tac (simpset() addsimps System_def::Join_ac) 1); -qed "Client_component_System"; - -Goal "rename sysOfAlloc Alloc Join \ -\ ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join \ -\ Network) = System"; -by (simp_tac (simpset() addsimps System_def::Join_ac) 1); -qed "Alloc_component_System"; - -AddIffs [Client_component_System, Network_component_System, - Alloc_component_System]; - -(** These preservation laws should be generated automatically **) - -Goal "Allowed Client = preserves rel Int preserves ask"; -by (auto_tac (claset(), - simpset() addsimps [Allowed_def, Client_AllowedActs, - safety_prop_Acts_iff])); -qed "Client_Allowed"; -Addsimps [Client_Allowed]; - -Goal "Allowed Network = \ -\ preserves allocRel Int \ -\ (INT i: lessThan Nclients. preserves(giv o sub i o client))"; -by (auto_tac (claset(), - simpset() addsimps [Allowed_def, Network_AllowedActs, - safety_prop_Acts_iff])); -qed "Network_Allowed"; -Addsimps [Network_Allowed]; - -Goal "Allowed Alloc = preserves allocGiv"; -by (auto_tac (claset(), - simpset() addsimps [Allowed_def, Alloc_AllowedActs, - safety_prop_Acts_iff])); -qed "Alloc_Allowed"; -Addsimps [Alloc_Allowed]; - -Goal "OK I (%i. lift i (rename client_map Client))"; -by (rtac OK_lift_I 1); -by Auto_tac; -by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1); -by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2); -by (auto_tac (claset(), simpset() addsimps [o_def, split_def])); -qed "OK_lift_rename_Client"; -Addsimps [OK_lift_rename_Client]; (*needed in rename_client_map_tac* - -(*The proofs of rename_Client_Increasing, rename_Client_Bounded and - rename_Client_Progress are similar. All require copying out the original - Client property. A forward proof can be constructed as follows: - - Client_Increasing_ask RS - (bij_client_map RS rename_rename_guarantees_eq RS iffD2) - RS (lift_lift_guarantees_eq RS iffD2) - RS guarantees_PLam_I - RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2) - |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def, - surj_rename RS surj_range]); - -However, the "preserves" property remains to be discharged, and the unfolding -of "o" and "sub" complicates subsequent reasoning. - -The following tactic works for all three proofs, though it certainly looks -ad-hoc! -*) -val rename_client_map_tac = - EVERY [ - simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1, - rtac guarantees_PLam_I 1, - assume_tac 2, - (*preserves: routine reasoning*) - asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2, - (*the guarantee for "lift i (rename client_map Client)" *) - asm_simp_tac - (simpset() addsimps [lift_guarantees_eq_lift_inv, - rename_guarantees_eq_rename_inv, - bij_imp_bij_inv, surj_rename RS surj_range, - inv_inv_eq]) 1, - asm_simp_tac - (simpset() addsimps [o_def, non_dummy_def, guarantees_Int_right]) 1]; - - -(*Lifting Client_Increasing to systemState*) -Goal "i : I \ -\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \ -\ UNIV guarantees \ -\ Increasing (ask o sub i o client) Int \ -\ Increasing (rel o sub i o client)"; -by rename_client_map_tac; -qed "rename_Client_Increasing"; - -Goal "[| F : preserves w; i ~= j |] \ -\ ==> F : preserves (sub i o fst o lift_map j o funPair v w)"; -by (auto_tac (claset(), - simpset() addsimps [lift_map_def, split_def, linorder_neq_iff, o_def])); -by (ALLGOALS (dtac (impOfSubs subset_preserves_o))); -by (auto_tac (claset(), simpset() addsimps [o_def])); -qed "preserves_sub_fst_lift_map"; - -Goal "[| i < Nclients; j < Nclients |] \ -\ ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)"; -by (case_tac "i=j" 1); -by (asm_full_simp_tac (simpset() addsimps [o_def, non_dummy_def]) 1); -by (dtac (Client_preserves_dummy RS preserves_sub_fst_lift_map) 1); -by (ALLGOALS (dtac (impOfSubs subset_preserves_o))); -by (asm_full_simp_tac (simpset() addsimps [o_def, client_map_def]) 1); -qed "client_preserves_giv_oo_client_map"; - -Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\ -\ ok Network"; -by (auto_tac (claset(), simpset() addsimps [ok_iff_Allowed, - client_preserves_giv_oo_client_map])); -qed "rename_sysOfClient_ok_Network"; - -Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\ -\ ok rename sysOfAlloc Alloc"; -by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1); -qed "rename_sysOfClient_ok_Alloc"; - -Goal "rename sysOfAlloc Alloc ok Network"; -by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1); -qed "rename_sysOfAlloc_ok_Network"; - -AddIffs [rename_sysOfClient_ok_Network, rename_sysOfClient_ok_Alloc, - rename_sysOfAlloc_ok_Network]; - -(*The "ok" laws, re-oriented*) -AddIffs [rename_sysOfClient_ok_Network RS ok_sym, - rename_sysOfClient_ok_Alloc RS ok_sym, - rename_sysOfAlloc_ok_Network RS ok_sym]; - -Goal "i < Nclients \ -\ ==> System : Increasing (ask o sub i o client) Int \ -\ Increasing (rel o sub i o client)"; -by (rtac ([rename_Client_Increasing, - Client_component_System] MRS component_guaranteesD) 1); -by Auto_tac; -qed "System_Increasing"; - -bind_thm ("rename_guarantees_sysOfAlloc_I", - bij_sysOfAlloc RS rename_rename_guarantees_eq RS iffD2); - - -(*Lifting Alloc_Increasing up to the level of systemState*) -val rename_Alloc_Increasing = - Alloc_Increasing RS rename_guarantees_sysOfAlloc_I - |> simplify (simpset() addsimps [surj_rename RS surj_range, o_def]); - -Goalw [System_def] - "i < Nclients ==> System : Increasing (sub i o allocGiv)"; -by (simp_tac (simpset() addsimps [o_def]) 1); -by (rtac (rename_Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1); -by Auto_tac; -qed "System_Increasing_allocGiv"; - -AddSIs (list_of_Int System_Increasing); - -(** Follows consequences. - The "Always (INT ...) formulation expresses the general safety property - and allows it to be combined using Always_Int_rule below. **) - -Goal - "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))"; -by (auto_tac (claset() addSIs [Network_Rel RS component_guaranteesD], - simpset())); -qed "System_Follows_rel"; - -Goal - "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))"; -by (auto_tac (claset() addSIs [Network_Ask RS component_guaranteesD], - simpset())); -qed "System_Follows_ask"; - -Goal - "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)"; -by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD, - rename_Alloc_Increasing RS component_guaranteesD], - simpset())); -by (ALLGOALS (simp_tac (simpset() addsimps [o_def, non_dummy_def]))); -by (auto_tac - (claset() addSIs [rename_Alloc_Increasing RS component_guaranteesD], - simpset())); -qed "System_Follows_allocGiv"; - -Goal "System : Always (INT i: lessThan Nclients. \ -\ {s. (giv o sub i o client) s <= (sub i o allocGiv) s})"; -by Auto_tac; -by (etac (System_Follows_allocGiv RS Follows_Bounded) 1); -qed "Always_giv_le_allocGiv"; - -Goal "System : Always (INT i: lessThan Nclients. \ -\ {s. (sub i o allocAsk) s <= (ask o sub i o client) s})"; -by Auto_tac; -by (etac (System_Follows_ask RS Follows_Bounded) 1); -qed "Always_allocAsk_le_ask"; - -Goal "System : Always (INT i: lessThan Nclients. \ -\ {s. (sub i o allocRel) s <= (rel o sub i o client) s})"; -by (auto_tac (claset() addSIs [Follows_Bounded, System_Follows_rel], - simpset())); -qed "Always_allocRel_le_rel"; - - -(*** Proof of the safety property (1) ***) - -(*safety (1), step 1 is System_Follows_rel*) - -(*safety (1), step 2*) -(* i < Nclients ==> System : Increasing (sub i o allocRel) *) -bind_thm ("System_Increasing_allocRel", - System_Follows_rel RS Follows_Increasing1); - -(*Lifting Alloc_safety up to the level of systemState. - Simplififying with o_def gets rid of the translations but it unfortunately - gets rid of the other "o"s too.*) -val rename_Alloc_Safety = - Alloc_Safety RS rename_guarantees_sysOfAlloc_I - |> simplify (simpset() addsimps [o_def]); - -(*safety (1), step 3*) -Goal - "System : Always {s. setsum (%i. (tokens o sub i o allocGiv) s) \ -\ (lessThan Nclients) \ -\ <= NbT + setsum (%i. (tokens o sub i o allocRel) s) \ -\ (lessThan Nclients)}"; -by (simp_tac (simpset() addsimps [o_apply]) 1); -by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1); -by (auto_tac (claset(), - simpset() addsimps [o_simp System_Increasing_allocRel])); -qed "System_sum_bounded"; - - -(** Follows reasoning **) - -Goal "System : Always (INT i: lessThan Nclients. \ -\ {s. (tokens o giv o sub i o client) s \ -\ <= (tokens o sub i o allocGiv) s})"; -by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1); -by (auto_tac (claset() addIs [tokens_mono_prefix], - simpset() addsimps [o_apply])); -qed "Always_tokens_giv_le_allocGiv"; - -Goal "System : Always (INT i: lessThan Nclients. \ -\ {s. (tokens o sub i o allocRel) s \ -\ <= (tokens o rel o sub i o client) s})"; -by (rtac (Always_allocRel_le_rel RS Always_weaken) 1); -by (auto_tac (claset() addIs [tokens_mono_prefix], - simpset() addsimps [o_apply])); -qed "Always_tokens_allocRel_le_rel"; - -(*safety (1), step 4 (final result!) *) -Goalw [system_safety_def] "System : system_safety"; -by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv, - Always_tokens_allocRel_le_rel] RS Always_weaken) 1); -by Auto_tac; -by (rtac (setsum_fun_mono RS order_trans) 1); -by (dtac order_trans 2); -by (rtac ([order_refl, setsum_fun_mono] MRS add_le_mono) 2); -by (assume_tac 3); -by Auto_tac; -qed "System_safety"; - - -(*** Proof of the progress property (2) ***) - -(*progress (2), step 1 is System_Follows_ask and System_Follows_rel*) - -(*progress (2), step 2; see also System_Increasing_allocRel*) -(* i < Nclients ==> System : Increasing (sub i o allocAsk) *) -bind_thm ("System_Increasing_allocAsk", - System_Follows_ask RS Follows_Increasing1); - -(*progress (2), step 3: lifting "Client_Bounded" to systemState*) -Goal "i : I \ -\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \ -\ UNIV guarantees \ -\ Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}"; -by rename_client_map_tac; -qed "rename_Client_Bounded"; - -Goal "i < Nclients \ -\ ==> System : Always \ -\ {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}"; -by (rtac ([rename_Client_Bounded, - Client_component_System] MRS component_guaranteesD) 1); -by Auto_tac; -qed "System_Bounded_ask"; - -Goal "{x. ALL y. P y --> Q x y} = (INT y: {y. P y}. {x. Q x y})"; -by (Blast_tac 1); -qed "Collect_all_imp_eq"; - -(*progress (2), step 4*) -Goal "System : Always {s. ALL i System : Increasing (giv o sub i o client) *) -bind_thm ("System_Increasing_giv", - System_Follows_allocGiv RS Follows_Increasing1); - - -Goal "i: I \ -\ ==> rename sysOfClient (plam x: I. rename client_map Client) \ -\ : Increasing (giv o sub i o client) \ -\ guarantees \ -\ (INT h. {s. h <= (giv o sub i o client) s & \ -\ h pfixGe (ask o sub i o client) s} \ -\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})"; -by rename_client_map_tac; -by (asm_simp_tac (simpset() addsimps [o_simp Client_Progress]) 1); -qed "rename_Client_Progress"; - - -(*progress (2), step 7*) -Goal - "System : (INT i : (lessThan Nclients). \ -\ INT h. {s. h <= (giv o sub i o client) s & \ -\ h pfixGe (ask o sub i o client) s} \ -\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})"; -by (rtac INT_I 1); -(*Couldn't have just used Auto_tac since the "INT h" must be kept*) -by (rtac ([rename_Client_Progress, - Client_component_System] MRS component_guaranteesD) 1); -by (auto_tac (claset(), simpset() addsimps [System_Increasing_giv])); -qed "System_Client_Progress"; - -(*Concludes - System : {s. k <= (sub i o allocGiv) s} - LeadsTo - {s. (sub i o allocAsk) s <= (ask o sub i o client) s} Int - {s. k <= (giv o sub i o client) s} *) -val lemma = - [System_Follows_ask RS Follows_Bounded, - System_Follows_allocGiv RS Follows_LeadsTo] MRS Always_LeadsToD; - -(*A more complicated variant of the previous one*) -val lemma2 = [lemma, - System_Follows_ask RS Follows_Increasing1 RS IncreasingD] - MRS PSP_Stable; - -Goal "i < Nclients \ -\ ==> System : {s. h <= (sub i o allocGiv) s & \ -\ h pfixGe (sub i o allocAsk) s} \ -\ LeadsTo \ -\ {s. h <= (giv o sub i o client) s & \ -\ h pfixGe (ask o sub i o client) s}"; -by (rtac single_LeadsTo_I 1); -by (res_inst_tac [("k6", "h"), ("x2", "(sub i o allocAsk) s")] - (lemma2 RS LeadsTo_weaken) 1); -by Auto_tac; -by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD, - prefix_imp_pfixGe]) 1); -val lemma3 = result(); - - -(*progress (2), step 8: Client i's "release" action is visible system-wide*) -Goal "i < Nclients \ -\ ==> System : {s. h <= (sub i o allocGiv) s & \ -\ h pfixGe (sub i o allocAsk) s} \ -\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel) s}"; -by (rtac LeadsTo_Trans 1); -by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS - Follows_LeadsTo) 2); -by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2); -by (rtac LeadsTo_Trans 1); -by (cut_facts_tac [System_Client_Progress] 2); -by (blast_tac (claset() addIs [LeadsTo_Basis]) 2); -by (etac lemma3 1); -qed "System_Alloc_Client_Progress"; - -(*Lifting Alloc_Progress up to the level of systemState*) -val rename_Alloc_Progress = - Alloc_Progress RS rename_guarantees_sysOfAlloc_I - |> simplify (simpset() addsimps [o_def]); - -(*progress (2), step 9*) -Goal - "System : (INT i : (lessThan Nclients). \ -\ INT h. {s. h <= (sub i o allocAsk) s} \ -\ LeadsTo {s. h pfixLe (sub i o allocGiv) s})"; -(*Can't use simpset(): the "INT h" must be kept*) -by (simp_tac (HOL_ss addsimps [o_apply, sub_def]) 1); -by (rtac (rename_Alloc_Progress RS component_guaranteesD) 1); -by (auto_tac (claset(), - simpset() addsimps [o_simp System_Increasing_allocRel, - o_simp System_Increasing_allocAsk, - o_simp System_Bounded_allocAsk, - o_simp System_Alloc_Client_Progress])); -qed "System_Alloc_Progress"; - - -(*progress (2), step 10 (final result!) *) -Goalw [system_progress_def] "System : system_progress"; -by (cut_facts_tac [System_Alloc_Progress] 1); -by (blast_tac (claset() addIs [LeadsTo_Trans, - System_Follows_allocGiv RS Follows_LeadsTo_pfixLe, - System_Follows_ask RS Follows_LeadsTo]) 1); -qed "System_Progress"; - - -(*Ultimate goal*) -Goalw [system_spec_def] "System : system_spec"; -by (blast_tac (claset() addIs [System_safety, System_Progress]) 1); -qed "System_correct"; - - -(** Some lemmas no longer used **) - -Goal "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o \ -\ (funPair giv (funPair ask rel))"; -by (rtac ext 1); -by (auto_tac (claset(), simpset() addsimps [o_def, non_dummy_def])); -qed "non_dummy_eq_o_funPair"; - -Goal "(preserves non_dummy) = \ -\ (preserves rel Int preserves ask Int preserves giv)"; -by (simp_tac (simpset() addsimps [non_dummy_eq_o_funPair]) 1); -by Auto_tac; -by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1); -by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2); -by (dres_inst_tac [("w1", "giv")] (impOfSubs subset_preserves_o) 3); -by (auto_tac (claset(), simpset() addsimps [o_def])); -qed "preserves_non_dummy_eq"; - -(*Could go to Extend.ML*) -Goal "bij f ==> fst (inv (%(x, u). inv f x) z) = f z"; -by (rtac fst_inv_equalityI 1); -by (res_inst_tac [("f","%z. (f z, ?h z)")] surjI 1); -by (asm_full_simp_tac (simpset() addsimps [bij_is_inj, inv_f_f]) 1); -by (asm_full_simp_tac (simpset() addsimps [bij_is_surj, surj_f_inv_f]) 1); -qed "bij_fst_inv_inv_eq"; diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Alloc.thy --- a/src/HOL/UNITY/Alloc.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,261 +0,0 @@ -(* Title: HOL/UNITY/Alloc - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Specification of Chandy and Charpentier's Allocator -*) - -Alloc = AllocBase + PPROD + - -(** State definitions. OUTPUT variables are locals **) - -record clientState = - giv :: nat list (*client's INPUT history: tokens GRANTED*) - ask :: nat list (*client's OUTPUT history: tokens REQUESTED*) - rel :: nat list (*client's OUTPUT history: tokens RELEASED*) - -record 'a clientState_d = - clientState + - dummy :: 'a (*dummy field for new variables*) - -constdefs - (*DUPLICATED FROM Client.thy, but with "tok" removed*) - (*Maybe want a special theory section to declare such maps*) - non_dummy :: 'a clientState_d => clientState - "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)" - - (*Renaming map to put a Client into the standard form*) - client_map :: "'a clientState_d => clientState*'a" - "client_map == funPair non_dummy dummy" - - -record allocState = - allocGiv :: nat => nat list (*OUTPUT history: source of "giv" for i*) - allocAsk :: nat => nat list (*INPUT: allocator's copy of "ask" for i*) - allocRel :: nat => nat list (*INPUT: allocator's copy of "rel" for i*) - -record 'a allocState_d = - allocState + - dummy :: 'a (*dummy field for new variables*) - -record 'a systemState = - allocState + - client :: nat => clientState (*states of all clients*) - dummy :: 'a (*dummy field for new variables*) - - -constdefs - -(** Resource allocation system specification **) - - (*spec (1)*) - system_safety :: 'a systemState program set - "system_safety == - Always {s. setsum(%i.(tokens o giv o sub i o client)s) (lessThan Nclients) - <= NbT + setsum(%i.(tokens o rel o sub i o client)s) (lessThan Nclients)}" - - (*spec (2)*) - system_progress :: 'a systemState program set - "system_progress == INT i : lessThan Nclients. - INT h. - {s. h <= (ask o sub i o client)s} LeadsTo - {s. h pfixLe (giv o sub i o client) s}" - - system_spec :: 'a systemState program set - "system_spec == system_safety Int system_progress" - -(** Client specification (required) ***) - - (*spec (3)*) - client_increasing :: 'a clientState_d program set - "client_increasing == - UNIV guarantees Increasing ask Int Increasing rel" - - (*spec (4)*) - client_bounded :: 'a clientState_d program set - "client_bounded == - UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}" - - (*spec (5)*) - client_progress :: 'a clientState_d program set - "client_progress == - Increasing giv guarantees - (INT h. {s. h <= giv s & h pfixGe ask s} - LeadsTo {s. tokens h <= (tokens o rel) s})" - - (*spec: preserves part*) - client_preserves :: 'a clientState_d program set - "client_preserves == preserves giv Int preserves clientState_d.dummy" - - (*environmental constraints*) - client_allowed_acts :: 'a clientState_d program set - "client_allowed_acts == - {F. AllowedActs F = - insert Id (UNION (preserves (funPair rel ask)) Acts)}" - - client_spec :: 'a clientState_d program set - "client_spec == client_increasing Int client_bounded Int client_progress - Int client_allowed_acts Int client_preserves" - -(** Allocator specification (required) ***) - - (*spec (6)*) - alloc_increasing :: 'a allocState_d program set - "alloc_increasing == - UNIV guarantees - (INT i : lessThan Nclients. Increasing (sub i o allocGiv))" - - (*spec (7)*) - alloc_safety :: 'a allocState_d program set - "alloc_safety == - (INT i : lessThan Nclients. Increasing (sub i o allocRel)) - guarantees - Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients) - <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}" - - (*spec (8)*) - alloc_progress :: 'a allocState_d program set - "alloc_progress == - (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int - Increasing (sub i o allocRel)) - Int - Always {s. ALL i clientState) * 'a) allocState_d => 'a systemState" - "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s - in (| allocGiv = allocGiv s, - allocAsk = allocAsk s, - allocRel = allocRel s, - client = cl, - dummy = xtr|)" - - - sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState" - "sysOfClient == %(cl,al). (| allocGiv = allocGiv al, - allocAsk = allocAsk al, - allocRel = allocRel al, - client = cl, - systemState.dummy = allocState_d.dummy al|)" - -consts - Alloc :: 'a allocState_d program - Client :: 'a clientState_d program - Network :: 'a systemState program - System :: 'a systemState program - -rules - Alloc "Alloc : alloc_spec" - Client "Client : client_spec" - Network "Network : network_spec" - -defs - System_def - "System == rename sysOfAlloc Alloc Join Network Join - (rename sysOfClient - (plam x: lessThan Nclients. rename client_map Client))" - - -(** -locale System = - fixes - Alloc :: 'a allocState_d program - Client :: 'a clientState_d program - Network :: 'a systemState program - System :: 'a systemState program - - assumes - Alloc "Alloc : alloc_spec" - Client "Client : client_spec" - Network "Network : network_spec" - - defines - System_def - "System == rename sysOfAlloc Alloc - Join - Network - Join - (rename sysOfClient - (plam x: lessThan Nclients. rename client_map Client))" -**) - - -end diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/AllocBase.ML --- a/src/HOL/UNITY/AllocBase.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,89 +0,0 @@ -(* Title: HOL/UNITY/AllocBase.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Basis declarations for Chandy and Charpentier's Allocator -*) - -Goal "!!f :: nat=>nat. \ -\ (ALL i. i f i <= g i) --> \ -\ setsum f (lessThan n) <= setsum g (lessThan n)"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [lessThan_Suc])); -by (dres_inst_tac [("x","n")] spec 1); -by (arith_tac 1); -qed_spec_mp "setsum_fun_mono"; - -Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys"; -by (induct_tac "ys" 1); -by (auto_tac (claset(), simpset() addsimps [prefix_Cons])); -qed_spec_mp "tokens_mono_prefix"; - -Goalw [mono_def] "mono tokens"; -by (blast_tac (claset() addIs [tokens_mono_prefix]) 1); -qed "mono_tokens"; - - -(** bag_of **) - -Goal "bag_of (l@l') = bag_of l + bag_of l'"; -by (induct_tac "l" 1); - by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2); -by (Simp_tac 1); -qed "bag_of_append"; -Addsimps [bag_of_append]; - -Goal "mono (bag_of :: 'a list => ('a::order) multiset)"; -by (rtac monoI 1); -by (rewtac prefix_def); -by (etac genPrefix.induct 1); -by Auto_tac; -by (asm_full_simp_tac (simpset() addsimps [thm "union_le_mono"]) 1); -by (etac order_trans 1); -by (rtac (thm "union_upper1") 1); -qed "mono_bag_of"; - -(** setsum **) - -Addcongs [setsum_cong]; - -Goal "setsum (%i. {#if i bag_of (sublist l (A Un B)) = \ -\ bag_of (sublist l A) + bag_of (sublist l B)"; -by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1); -qed "bag_of_sublist_Un_disjoint"; - -Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \ -\ ==> bag_of (sublist l (UNION I A)) = \ -\ setsum (%i. bag_of (sublist l (A i))) I"; -by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym]) - addsimps [bag_of_sublist]) 1); -by (stac setsum_UN_disjoint 1); -by Auto_tac; -qed_spec_mp "bag_of_sublist_UN_disjoint"; diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/AllocBase.thy --- a/src/HOL/UNITY/AllocBase.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -(* Title: HOL/UNITY/AllocBase.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Common declarations for Chandy and Charpentier's Allocator -*) - -AllocBase = Rename + Follows + - -consts - NbT :: nat (*Number of tokens in system*) - Nclients :: nat (*Number of clients*) - -rules - NbT_pos "0 < NbT" - -(*This function merely sums the elements of a list*) -consts tokens :: nat list => nat -primrec - "tokens [] = 0" - "tokens (x#xs) = x + tokens xs" - -consts - bag_of :: 'a list => 'a multiset - -primrec - "bag_of [] = {#}" - "bag_of (x#xs) = {#x#} + bag_of xs" - -end diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/AllocImpl.ML --- a/src/HOL/UNITY/AllocImpl.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,194 +0,0 @@ -(* Title: HOL/UNITY/AllocImpl - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 2000 University of Cambridge - -Implementation of a multiple-client allocator from a single-client allocator -*) - -AddIs [impOfSubs subset_preserves_o]; -Addsimps [funPair_o_distrib]; -Addsimps [Always_INT_distrib]; -Delsimps [o_apply]; - -Open_locale "Merge"; - -val Merge = thm "Merge_spec"; - -Goal "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"; -by (cut_facts_tac [Merge] 1); -by (auto_tac (claset(), - simpset() addsimps [merge_spec_def, merge_allowed_acts_def, - Allowed_def, safety_prop_Acts_iff])); -qed "Merge_Allowed"; - -Goal "M ok G = (G: preserves merge.Out & G: preserves merge.iOut & \ -\ M : Allowed G)"; -by (auto_tac (claset(), simpset() addsimps [Merge_Allowed, ok_iff_Allowed])); -qed "M_ok_iff"; -AddIffs [M_ok_iff]; - -Goal "[| G: preserves merge.Out; G: preserves merge.iOut; M : Allowed G |] \ -\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}"; -by (cut_facts_tac [Merge] 1); -by (force_tac (claset() addDs [guaranteesD], - simpset() addsimps [merge_spec_def, merge_eqOut_def]) 1); -qed "Merge_Always_Out_eq_iOut"; - -Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \ -\ ==> M Join G: Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"; -by (cut_facts_tac [Merge] 1); -by (force_tac (claset() addDs [guaranteesD], - simpset() addsimps [merge_spec_def, merge_bounded_def]) 1); -qed "Merge_Bounded"; - -Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \ -\ ==> M Join G : Always \ -\ {s. setsum (%i. bag_of (sublist (merge.Out s) \ -\ {k. k < length (iOut s) & iOut s ! k = i})) \ -\ (lessThan Nclients) = \ -\ (bag_of o merge.Out) s}"; -by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I, - UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1); - by Auto_tac; -by (stac (bag_of_sublist_UN_disjoint RS sym) 1); - by (Simp_tac 1); - by (Blast_tac 1); -by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1); -by (subgoal_tac - "(UN i:lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) = \ -\ lessThan (length (iOut x))" 1); - by (Blast_tac 2); -by (asm_simp_tac (simpset() addsimps [o_def]) 1); -qed "Merge_Bag_Follows_lemma"; - -Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \ -\ guarantees \ -\ (bag_of o merge.Out) Fols \ -\ (%s. setsum (%i. (bag_of o sub i o merge.In) s) \ -\ (lessThan Nclients))"; -by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1); -by Auto_tac; -by (rtac Follows_setsum 1); -by (cut_facts_tac [Merge] 1); -by (auto_tac (claset(), - simpset() addsimps [merge_spec_def, merge_follows_def, o_def])); -by (dtac guaranteesD 1); -by (best_tac - (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3); -by Auto_tac; -qed "Merge_Bag_Follows"; - -Close_locale "Merge"; - - -(** Distributor **) - -Open_locale "Distrib"; - -val Distrib = thm "Distrib_spec"; - - -Goal "D : Increasing distr.In Int Increasing distr.iIn Int \ -\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \ -\ guarantees \ -\ (INT i : lessThan Nclients. Increasing (sub i o distr.Out))"; -by (cut_facts_tac [Distrib] 1); -by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); -by (Clarify_tac 1); -by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1] - addDs [guaranteesD]) 1); -qed "Distr_Increasing_Out"; - -Goal "[| G : preserves distr.Out; \ -\ D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \ -\ ==> D Join G : Always \ -\ {s. setsum (%i. bag_of (sublist (distr.In s) \ -\ {k. k < length (iIn s) & iIn s ! k = i})) \ -\ (lessThan Nclients) = \ -\ bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"; -by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1); -by Auto_tac; -by (stac (bag_of_sublist_UN_disjoint RS sym) 1); - by (Simp_tac 1); - by (Blast_tac 1); -by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1); -by (subgoal_tac - "(UN i:lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = \ -\ lessThan (length (iIn x))" 1); - by (Blast_tac 2); -by (Asm_simp_tac 1); -qed "Distr_Bag_Follows_lemma"; - -Goal "D ok G = (G: preserves distr.Out & D : Allowed G)"; -by (cut_facts_tac [Distrib] 1); -by (auto_tac (claset(), - simpset() addsimps [distr_spec_def, distr_allowed_acts_def, - Allowed_def, safety_prop_Acts_iff, ok_iff_Allowed])); -qed "D_ok_iff"; -AddIffs [D_ok_iff]; - -Goal - "D : Increasing distr.In Int Increasing distr.iIn Int \ -\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \ -\ guarantees \ -\ (INT i : lessThan Nclients. \ -\ (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \ -\ Fols \ -\ (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))"; -by (rtac guaranteesI 1); -by (Clarify_tac 1); -by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1); -by Auto_tac; -by (rtac Follows_setsum 1); -by (cut_facts_tac [Distrib] 1); -by (auto_tac (claset(), - simpset() addsimps [distr_spec_def, distr_follows_def, o_def])); -by (dtac guaranteesD 1); -by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3); -by Auto_tac; -qed "Distr_Bag_Follows"; - -Close_locale "Distrib"; - - -Goal "!!f::nat=>nat. (INT i:(lessThan n). {s. f i <= g i s}) \ -\ <= {s. setsum f (lessThan n) <= setsum (%i. g i s) (lessThan n)}"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [lessThan_Suc])); -qed "alloc_refinement_lemma"; - -Goal -"(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int \ -\ Increasing (sub i o allocRel)) \ -\ Int \ -\ Always {s. ALL i. i \ -\ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)} \ -\ Int \ -\ (INT i : lessThan Nclients. \ -\ INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} \ -\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s}) \ -\ <= \ -\(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int \ -\ Increasing (sub i o allocRel)) \ -\ Int \ -\ Always {s. ALL i. i \ -\ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)} \ -\ Int \ -\ (INT hf. (INT i : lessThan Nclients. \ -\ {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) \ -\ LeadsTo {s. setsum (%i. tokens (hf i)) (lessThan Nclients) <= \ -\ setsum (%i. (tokens o sub i o allocRel)s) (lessThan Nclients) })"; -by (auto_tac (claset(), simpset() addsimps [ball_conj_distrib])); -by (rename_tac "F hf" 1); -by (rtac ([Finite_stable_completion, alloc_refinement_lemma] - MRS LeadsTo_weaken_R) 1); - by (Blast_tac 1); - by (Blast_tac 1); -by (subgoal_tac "F : Increasing (tokens o (sub i o allocRel))" 1); - by (blast_tac - (claset() addIs [impOfSubs (mono_tokens RS mono_Increasing_o)]) 2); -by (asm_full_simp_tac (simpset() addsimps [Increasing_def, o_assoc]) 1); -qed "alloc_refinement"; - - diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/AllocImpl.thy --- a/src/HOL/UNITY/AllocImpl.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,224 +0,0 @@ -(* Title: HOL/UNITY/AllocImpl - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Implementation of a multiple-client allocator from a single-client allocator -*) - -AllocImpl = AllocBase + Follows + PPROD + - - -(** State definitions. OUTPUT variables are locals **) - -(*Type variable 'b is the type of items being merged*) -record 'b merge = - In :: nat => 'b list (*merge's INPUT histories: streams to merge*) - Out :: 'b list (*merge's OUTPUT history: merged items*) - iOut :: nat list (*merge's OUTPUT history: origins of merged items*) - -record ('a,'b) merge_d = - 'b merge + - dummy :: 'a (*dummy field for new variables*) - -constdefs - non_dummy :: ('a,'b) merge_d => 'b merge - "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)" - -record 'b distr = - In :: 'b list (*items to distribute*) - iIn :: nat list (*destinations of items to distribute*) - Out :: nat => 'b list (*distributed items*) - -record ('a,'b) distr_d = - 'b distr + - dummy :: 'a (*dummy field for new variables*) - -record allocState = - giv :: nat list (*OUTPUT history: source of tokens*) - ask :: nat list (*INPUT: tokens requested from allocator*) - rel :: nat list (*INPUT: tokens released to allocator*) - -record 'a allocState_d = - allocState + - dummy :: 'a (*dummy field for new variables*) - -record 'a systemState = - allocState + - mergeRel :: nat merge - mergeAsk :: nat merge - distr :: nat distr - dummy :: 'a (*dummy field for new variables*) - - -constdefs - -(** Merge specification (the number of inputs is Nclients) ***) - - (*spec (10)*) - merge_increasing :: ('a,'b) merge_d program set - "merge_increasing == - UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)" - - (*spec (11)*) - merge_eqOut :: ('a,'b) merge_d program set - "merge_eqOut == - UNIV guarantees - Always {s. length (merge.Out s) = length (merge.iOut s)}" - - (*spec (12)*) - merge_bounded :: ('a,'b) merge_d program set - "merge_bounded == - UNIV guarantees - Always {s. ALL elt : set (merge.iOut s). elt < Nclients}" - - (*spec (13)*) - merge_follows :: ('a,'b) merge_d program set - "merge_follows == - (INT i : lessThan Nclients. Increasing (sub i o merge.In)) - guarantees - (INT i : lessThan Nclients. - (%s. sublist (merge.Out s) - {k. k < size(merge.iOut s) & merge.iOut s! k = i}) - Fols (sub i o merge.In))" - - (*spec: preserves part*) - merge_preserves :: ('a,'b) merge_d program set - "merge_preserves == preserves merge.In Int preserves merge_d.dummy" - - (*environmental constraints*) - merge_allowed_acts :: ('a,'b) merge_d program set - "merge_allowed_acts == - {F. AllowedActs F = - insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}" - - merge_spec :: ('a,'b) merge_d program set - "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int - merge_follows Int merge_allowed_acts Int merge_preserves" - -(** Distributor specification (the number of outputs is Nclients) ***) - - (*spec (14)*) - distr_follows :: ('a,'b) distr_d program set - "distr_follows == - Increasing distr.In Int Increasing distr.iIn Int - Always {s. ALL elt : set (distr.iIn s). elt < Nclients} - guarantees - (INT i : lessThan Nclients. - (sub i o distr.Out) Fols - (%s. sublist (distr.In s) - {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))" - - distr_allowed_acts :: ('a,'b) distr_d program set - "distr_allowed_acts == - {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}" - - distr_spec :: ('a,'b) distr_d program set - "distr_spec == distr_follows Int distr_allowed_acts" - -(** Single-client allocator specification (required) ***) - - (*spec (18)*) - alloc_increasing :: 'a allocState_d program set - "alloc_increasing == UNIV guarantees Increasing giv" - - (*spec (19)*) - alloc_safety :: 'a allocState_d program set - "alloc_safety == - Increasing rel - guarantees Always {s. tokens (giv s) <= NbT + tokens (rel s)}" - - (*spec (20)*) - alloc_progress :: 'a allocState_d program set - "alloc_progress == - Increasing ask Int Increasing rel Int - Always {s. ALL elt : set (ask s). elt <= NbT} - Int - (INT h. {s. h <= giv s & h pfixGe (ask s)} - LeadsTo - {s. tokens h <= tokens (rel s)}) - guarantees (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})" - - (*spec: preserves part*) - alloc_preserves :: 'a allocState_d program set - "alloc_preserves == preserves rel Int - preserves ask Int - preserves allocState_d.dummy" - - - (*environmental constraints*) - alloc_allowed_acts :: 'a allocState_d program set - "alloc_allowed_acts == - {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}" - - alloc_spec :: 'a allocState_d program set - "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int - alloc_allowed_acts Int alloc_preserves" - -locale Merge = - fixes - M :: ('a,'b::order) merge_d program - assumes - Merge_spec "M : merge_spec" - -locale Distrib = - fixes - D :: ('a,'b::order) distr_d program - assumes - Distrib_spec "D : distr_spec" - - -(**** -# (** Network specification ***) - -# (*spec (9.1)*) -# network_ask :: 'a systemState program set -# "network_ask == INT i : lessThan Nclients. -# Increasing (ask o sub i o client) -# guarantees[ask] -# (ask Fols (ask o sub i o client))" - -# (*spec (9.2)*) -# network_giv :: 'a systemState program set -# "network_giv == INT i : lessThan Nclients. -# Increasing giv -# guarantees[giv o sub i o client] -# ((giv o sub i o client) Fols giv )" - -# (*spec (9.3)*) -# network_rel :: 'a systemState program set -# "network_rel == INT i : lessThan Nclients. -# Increasing (rel o sub i o client) -# guarantees[rel] -# (rel Fols (rel o sub i o client))" - -# (*spec: preserves part*) -# network_preserves :: 'a systemState program set -# "network_preserves == preserves giv Int -# (INT i : lessThan Nclients. -# preserves (funPair rel ask o sub i o client))" - -# network_spec :: 'a systemState program set -# "network_spec == network_ask Int network_giv Int -# network_rel Int network_preserves" - - -# (** State mappings **) -# sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState" -# "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s -# in (| giv = giv s, -# ask = ask s, -# rel = rel s, -# client = cl, -# dummy = xtr|)" - - -# sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState" -# "sysOfClient == %(cl,al). (| giv = giv al, -# ask = ask al, -# rel = rel al, -# client = cl, -# systemState.dummy = allocState_d.dummy al|)" -****) - -end diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Channel.ML --- a/src/HOL/UNITY/Channel.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Channel.thy --- a/src/HOL/UNITY/Channel.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,30 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Client.ML --- a/src/HOL/UNITY/Client.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,174 +0,0 @@ -(* Title: HOL/UNITY/Client - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Distributed Resource Management System: the Client -*) - -Addsimps [Client_def RS def_prg_Init, - Client_def RS def_prg_AllowedActs]; -program_defs_ref := [Client_def]; - -Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]); - -Goal "(Client ok G) = \ -\ (G : preserves rel & G : preserves ask & G : preserves tok &\ -\ Client : Allowed G)"; -by (auto_tac (claset(), - simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed])); -qed "Client_ok_iff"; -AddIffs [Client_ok_iff]; - - -(*Safety property 1: ask, rel are increasing*) -Goal "Client: UNIV guarantees Increasing ask Int Increasing rel"; -by (auto_tac - (claset() addSIs [increasing_imp_Increasing], - simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing])); -by (auto_tac (claset(), simpset() addsimps [increasing_def])); -by (ALLGOALS constrains_tac); -by Auto_tac; -qed "increasing_ask_rel"; - -Addsimps [nth_append, append_one_prefix]; - - -(*Safety property 2: the client never requests too many tokens. - With no Substitution Axiom, we must prove the two invariants - simultaneously. -*) -Goal "Client ok G \ -\ ==> Client Join G : \ -\ Always ({s. tok s <= NbT} Int \ -\ {s. ALL elt : set (ask s). elt <= NbT})"; -by Auto_tac; -by (rtac (invariantI RS stable_Join_Always2) 1); -by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable] - addSIs [stable_Int]) 3); -by (constrains_tac 2); -by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2); -by Auto_tac; -qed "ask_bounded_lemma"; - -(*export version, with no mention of tok in the postcondition, but - unfortunately tok must be declared local.*) -Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"; -by (rtac guaranteesI 1); -by (etac (ask_bounded_lemma RS Always_weaken) 1); -by (rtac Int_lower2 1); -qed "ask_bounded"; - - -(*** Towards proving the liveness property ***) - -Goal "Client: stable {s. rel s <= giv s}"; -by (constrains_tac 1); -by Auto_tac; -qed "stable_rel_le_giv"; - -Goal "[| Client Join G : Increasing giv; G : preserves rel |] \ -\ ==> Client Join G : Stable {s. rel s <= giv s}"; -by (rtac (stable_rel_le_giv RS Increasing_preserves_Stable) 1); -by Auto_tac; -qed "Join_Stable_rel_le_giv"; - -Goal "[| Client Join G : Increasing giv; G : preserves rel |] \ -\ ==> Client Join G : Always {s. rel s <= giv s}"; -by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1); -qed "Join_Always_rel_le_giv"; - -Goal "Client : transient {s. rel s = k & k Client Join G : {s. rel s = k & k Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s} \ -\ LeadsTo {s. h <= rel s}"; -by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1); -by (auto_tac (claset(), simpset() addsimps [vimage_def])); -by (rtac single_LeadsTo_I 1); -by (rtac (induct_lemma RS LeadsTo_weaken) 1); -by Auto_tac; -by (blast_tac (claset() addIs [order_less_le RS iffD2] - addDs [common_prefix_linear]) 1); -by (REPEAT (dtac strict_prefix_length_less 1)); -by (arith_tac 1); -qed "rel_progress_lemma"; - - -Goal "[| Client Join G : Increasing giv; Client ok G |] \ -\ ==> Client Join G : {s. h <= giv s & h pfixGe ask s} \ -\ LeadsTo {s. h <= rel s}"; -by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1); -by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS - LeadsTo_Un RS LeadsTo_weaken_L) 3); -by Auto_tac; -by (blast_tac (claset() addIs [order_less_le RS iffD2] - addDs [common_prefix_linear]) 1); -qed "client_progress_lemma"; - -(*Progress property: all tokens that are given will be released*) -Goal "Client : \ -\ Increasing giv guarantees \ -\ (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})"; -by (rtac guaranteesI 1); -by (Clarify_tac 1); -by (blast_tac (claset() addIs [client_progress_lemma]) 1); -qed "client_progress"; - -(*This shows that the Client won't alter other variables in any state - that it is combined with*) -Goal "Client : preserves dummy"; -by (rewtac preserves_def); -by Auto_tac; -by (constrains_tac 1); -by Auto_tac; -qed "client_preserves_dummy"; - - -(** Obsolete lemmas from first version of the Client **) - -Goal "Client: stable {s. size (rel s) <= size (giv s)}"; -by (constrains_tac 1); -by Auto_tac; -qed "stable_size_rel_le_giv"; - -(*clients return the right number of tokens*) -Goal "Client : Increasing giv guarantees Always {s. rel s <= giv s}"; -by (rtac guaranteesI 1); -by (rtac AlwaysI 1); -by (Force_tac 1); -by (blast_tac (claset() addIs [Increasing_preserves_Stable, - stable_rel_le_giv]) 1); -qed "ok_guar_rel_prefix_giv"; diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Client.thy --- a/src/HOL/UNITY/Client.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,66 +0,0 @@ -(* Title: HOL/UNITY/Client.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Distributed Resource Management System: the Client -*) - -Client = Rename + AllocBase + - -types - tokbag = nat (*tokbags could be multisets...or any ordered type?*) - -record state = - giv :: tokbag list (*input history: tokens granted*) - ask :: tokbag list (*output history: tokens requested*) - rel :: tokbag list (*output history: tokens released*) - tok :: tokbag (*current token request*) - -record 'a state_d = - state + - dummy :: 'a (*new variables*) - - -(*Array indexing is translated to list indexing as A[n] == A!(n-1). *) - -constdefs - - (** Release some tokens **) - - rel_act :: "('a state_d * 'a state_d) set" - "rel_act == {(s,s'). - EX nrel. nrel = size (rel s) & - s' = s (| rel := rel s @ [giv s!nrel] |) & - nrel < size (giv s) & - ask s!nrel <= giv s!nrel}" - - (** Choose a new token requirement **) - - (** Including s'=s suppresses fairness, allowing the non-trivial part - of the action to be ignored **) - - tok_act :: "('a state_d * 'a state_d) set" - "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" - - ask_act :: "('a state_d * 'a state_d) set" - "ask_act == {(s,s'). s'=s | - (s' = s (|ask := ask s @ [tok s]|))}" - - Client :: 'a state_d program - "Client == - mk_program ({s. tok s : atMost NbT & - giv s = [] & ask s = [] & rel s = []}, - {rel_act, tok_act, ask_act}, - UN G: preserves rel Int preserves ask Int preserves tok. - Acts G)" - - (*Maybe want a special theory section to declare such maps*) - non_dummy :: 'a state_d => state - "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)" - - (*Renaming map to put a Client into the standard form*) - client_map :: "'a state_d => state*'a" - "client_map == funPair non_dummy dummy" - -end diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Common.ML --- a/src/HOL/UNITY/Common.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,90 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Common.thy --- a/src/HOL/UNITY/Common.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Counter.ML --- a/src/HOL/UNITY/Counter.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,140 +0,0 @@ -(* Title: HOL/UNITY/Counter - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -A family of similar counters, version close to the original. - -From Charpentier and Chandy, -Examples of Program Composition Illustrating the Use of Universal Properties - In J. Rolim (editor), Parallel and Distributed Processing, - Spriner LNCS 1586 (1999), pages 1215-1227. -*) - -Addsimps [Component_def RS def_prg_Init]; -program_defs_ref := [Component_def]; -Addsimps (map simp_of_act [a_def]); - -(* Theorems about sum and sumj *) -Goal "ALL n. I sum I (s(c n := x)) = sum I s"; -by (induct_tac "I" 1); -by Auto_tac; -qed_spec_mp "sum_upd_gt"; - - -Goal "sum I (s(c I := x)) = sum I s"; -by (induct_tac "I" 1); -by Auto_tac; -by (simp_tac (simpset() - addsimps [rewrite_rule [fun_upd_def] sum_upd_gt]) 1); -qed "sum_upd_eq"; - -Goal "sum I (s(C := x)) = sum I s"; -by (induct_tac "I" 1); -by Auto_tac; -qed "sum_upd_C"; - -Goal "sumj I i (s(c i := x)) = sumj I i s"; -by (induct_tac "I" 1); -by Auto_tac; -by (simp_tac (simpset() addsimps - [rewrite_rule [fun_upd_def] sum_upd_eq]) 1); -qed "sumj_upd_ci"; - -Goal "sumj I i (s(C := x)) = sumj I i s"; -by (induct_tac "I" 1); -by Auto_tac; -by (simp_tac (simpset() - addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1); -qed "sumj_upd_C"; - -Goal "ALL i. I (sumj I i s = sum I s)"; -by (induct_tac "I" 1); -by Auto_tac; -qed_spec_mp "sumj_sum_gt"; - -Goal "(sumj I I s = sum I s)"; -by (induct_tac "I" 1); -by Auto_tac; -by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1); -qed "sumj_sum_eq"; - -Goal "ALL i. i(sum I s = s (c i) + sumj I i s)"; -by (induct_tac "I" 1); -by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq])); -qed_spec_mp "sum_sumj"; - -(* Correctness proofs for Components *) -(* p2 and p3 proofs *) -Goal "Component i : stable {s. s C = s (c i) + k}"; -by (constrains_tac 1); -qed "p2"; - -Goal -"Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}"; -by (constrains_tac 1); -qed "p3"; - - -Goal -"(ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} \ -\ Int {s. ALL v. v~=c i & v~=C --> s v = k v})) \ -\ = (Component i: stable {s. s C = s (c i) + sumj I i s})"; -by (auto_tac (claset(), simpset() - addsimps [constrains_def, stable_def,Component_def, - sumj_upd_C, sumj_upd_ci])); -qed "p2_p3_lemma1"; - -Goal -"ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} Int \ -\ {s. ALL v. v~=c i & v~=C --> s v = k v})"; -by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1); -qed "p2_p3_lemma2"; - - -Goal -"Component i: stable {s. s C = s (c i) + sumj I i s}"; -by (auto_tac (claset() addSIs [p2_p3_lemma2], - simpset() addsimps [p2_p3_lemma1 RS sym])); -qed "p2_p3"; - -(* Compositional Proof *) - -Goal "(ALL i. i < I --> s (c i) = #0) --> sum I s = #0"; -by (induct_tac "I" 1); -by Auto_tac; -qed "sum_0'"; -val sum0_lemma = (sum_0' RS mp) RS sym; - -(* I could'nt be empty *) -Goalw [invariant_def] -"!!I. 0 (JN i:{i. iint - -consts - sum :: "[nat,state]=>int" - sumj :: "[nat, nat, state]=>int" - -primrec (* sum I s = sigma_{icommand" - "a i == {(s, s'). s'=s(c i:= s (c i) + #1, C:= s C + #1)}" - - Component :: "nat => state program" - "Component i == - mk_program({s. s C = #0 & s (c i) = #0}, {a i}, - UN G: preserves (%s. s (c i)). Acts G)" -end diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Counterc.ML --- a/src/HOL/UNITY/Counterc.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,124 +0,0 @@ -(* Title: HOL/UNITY/Counterc - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -A family of similar counters, version with a full use of "compatibility " - -From Charpentier and Chandy, -Examples of Program Composition Illustrating the Use of Universal Properties - In J. Rolim (editor), Parallel and Distributed Processing, - Spriner LNCS 1586 (1999), pages 1215-1227. -*) - -Addsimps [Component_def RS def_prg_Init, -Component_def RS def_prg_AllowedActs]; -program_defs_ref := [Component_def]; -Addsimps (map simp_of_act [a_def]); - -(* Theorems about sum and sumj *) -Goal "ALL i. I (sum I s = sumj I i s)"; -by (induct_tac "I" 1); -by Auto_tac; -qed_spec_mp "sum_sumj_eq1"; - -Goal "i sum I s = c s i + sumj I i s"; -by (induct_tac "I" 1); -by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sum_sumj_eq1])); -qed_spec_mp "sum_sumj_eq2"; - -Goal "(ALL i. i c s' i = c s i) --> (sum I s' = sum I s)"; -by (induct_tac "I" 1 THEN Auto_tac); -qed_spec_mp "sum_ext"; - -Goal "(ALL j. j c s' j = c s j) --> (sumj I i s' = sumj I i s)"; -by (induct_tac "I" 1); -by Safe_tac; -by (auto_tac (claset() addSIs [sum_ext], simpset())); -qed_spec_mp "sumj_ext"; - - -Goal "(ALL i. i c s i = #0) --> sum I s = #0"; -by (induct_tac "I" 1); -by Auto_tac; -qed "sum0"; - - -(* Safety properties for Components *) - -Goal "(Component i ok G) = \ -\ (G: preserves (%s. c s i) & Component i:Allowed G)"; -by (auto_tac (claset(), - simpset() addsimps [ok_iff_Allowed, Component_def RS def_prg_Allowed])); -qed "Component_ok_iff"; -AddIffs [Component_ok_iff]; -AddIffs [OK_iff_ok]; -Addsimps [preserves_def]; - - -Goal "Component i: stable {s. C s = (c s) i + k}"; -by (constrains_tac 1); -qed "p2"; - -Goal "[| OK I Component; i:I |] \ -\ ==> Component i: stable {s. ALL j:I. j~=i --> c s j = c k j}"; -by (full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 1); -by (Blast_tac 1); -qed "p3"; - - -Goal -"[| OK {i. i \ -\ ALL k. Component i: stable ({s. C s = c s i + sumj I i k} Int \ -\ {s. ALL j:{i. i c s j = c k j})"; -by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1); -qed "p2_p3_lemma1"; - - -Goal "(ALL k. F:stable ({s. C s = (c s) i + sumj I i k} Int \ -\ {s. ALL j:{i. i c s j = c k j})) \ -\ ==> (F:stable {s. C s = c s i + sumj I i s})"; -by (full_simp_tac (simpset() addsimps [constrains_def, stable_def]) 1); -by (force_tac (claset() addSIs [sumj_ext], simpset()) 1); -qed "p2_p3_lemma2"; - - -Goal "[| OK {i. i Component i: stable {s. C s = c s i + sumj I i s}"; -by (blast_tac (claset() addIs [p2_p3_lemma1 RS p2_p3_lemma2]) 1); -qed "p2_p3"; - - -(* Compositional correctness *) -Goalw [invariant_def] - "[| 0 (JN i:{i. iint" - c :: "state=>nat=>int" - -consts - sum :: "[nat,state]=>int" - sumj :: "[nat, nat, state]=>int" - -primrec (* sum I s = sigma_{icommand" - "a i == {(s, s'). (c s') i = (c s) i + #1 & (C s') = (C s) + #1}" - - Component :: "nat => state program" - "Component i == mk_program({s. C s = #0 & (c s) i = #0}, {a i}, - UN G: preserves (%s. (c s) i). Acts G)" -end diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Deadlock.ML --- a/src/HOL/UNITY/Deadlock.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,78 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Deadlock.thy --- a/src/HOL/UNITY/Deadlock.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -Deadlock = UNITY diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Handshake.ML --- a/src/HOL/UNITY/Handshake.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,49 +0,0 @@ -(* Title: HOL/UNITY/Handshake - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Handshake Protocol - -From Misra, "Asynchronous Compositions of Programs", Section 5.3.2 -*) - -Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init]; -program_defs_ref := [F_def, G_def]; - -Addsimps (map simp_of_act [cmdF_def, cmdG_def]); -Addsimps [simp_of_set invFG_def]; - - -Goal "(F Join G) : Always invFG"; -by (rtac AlwaysI 1); -by (Force_tac 1); -by (rtac (constrains_imp_Constrains RS StableI) 1); -by Auto_tac; -by (constrains_tac 2); -by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset())); -by (constrains_tac 1); -qed "invFG"; - -Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \ -\ ({s. NF s = k} Int {s. BB s})"; -by (rtac (stable_Join_ensures1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); -by (ensures_tac "cmdG" 2); -by (constrains_tac 1); -qed "lemma2_1"; - -Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}"; -by (rtac (stable_Join_ensures2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); -by (constrains_tac 2); -by (ensures_tac "cmdF" 1); -qed "lemma2_2"; - -Goal "(F Join G) : UNIV LeadsTo {s. m < NF s}"; -by (rtac LeadsTo_weaken_R 1); -by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] - GreaterThan_bounded_induct 1); -(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*) -by (auto_tac (claset() addSIs [lemma2_1, lemma2_2] - addIs[LeadsTo_Trans, LeadsTo_Diff], - simpset() addsimps [vimage_def])); -qed "progress"; diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Handshake.thy --- a/src/HOL/UNITY/Handshake.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,37 +0,0 @@ -(* Title: HOL/UNITY/Handshake.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -Handshake Protocol - -From Misra, "Asynchronous Compositions of Programs", Section 5.3.2 -*) - -Handshake = Union + - -record state = - BB :: bool - NF :: nat - NG :: nat - -constdefs - (*F's program*) - cmdF :: "(state*state) set" - "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" - - F :: "state program" - "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)" - - (*G's program*) - cmdG :: "(state*state) set" - "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" - - G :: "state program" - "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)" - - (*the joint invariant*) - invFG :: "state set" - "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}" - -end diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Lift.ML --- a/src/HOL/UNITY/Lift.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,317 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Lift.thy --- a/src/HOL/UNITY/Lift.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,169 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Mutex.ML --- a/src/HOL/UNITY/Mutex.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,166 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Mutex.thy --- a/src/HOL/UNITY/Mutex.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,76 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/NSP_Bad.ML --- a/src/HOL/UNITY/NSP_Bad.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,288 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/NSP_Bad.thy --- a/src/HOL/UNITY/NSP_Bad.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,59 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Network.ML --- a/src/HOL/UNITY/Network.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,59 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Network.thy --- a/src/HOL/UNITY/Network.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Priority.ML --- a/src/HOL/UNITY/Priority.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,239 +0,0 @@ -(* Title: HOL/UNITY/Priority - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -The priority system - -From Charpentier and Chandy, -Examples of Program Composition Illustrating the Use of Universal Properties - In J. Rolim (editor), Parallel and Distributed Processing, - Spriner LNCS 1586 (1999), pages 1215-1227. -*) - -Addsimps [Component_def RS def_prg_Init]; -program_defs_ref := [Component_def, system_def]; -Addsimps [highest_def, lowest_def]; -Addsimps [simp_of_act act_def]; -Addsimps (map simp_of_set [Highest_def, Lowest_def]); - - - - -(**** Component correctness proofs ****) - -(* neighbors is stable *) -Goal "Component i: stable {s. neighbors k s = n}"; -by (constrains_tac 1); -by Auto_tac; -qed "Component_neighbors_stable"; - -(* property 4 *) -Goal -"Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}"; -by (constrains_tac 1); -qed "Component_waits_priority"; - -(* property 5: charpentier and Chandy mistakenly express it as - 'transient Highest i'. Consider the case where i has neighbors *) -Goal - "Component i: {s. neighbors i s ~= {}} Int Highest i \ -\ ensures - Highest i"; -by (ensures_tac "act i" 1); -by (REPEAT(Fast_tac 1)); -qed "Component_yields_priority"; - -(* or better *) -Goal "Component i: Highest i ensures Lowest i"; -by (ensures_tac "act i" 1); -by (REPEAT(Fast_tac 1)); -qed "Component_yields_priority'"; - -(* property 6: Component doesn't introduce cycle *) -Goal "Component i: Highest i co Highest i Un Lowest i"; -by (constrains_tac 1); -by (Fast_tac 1); -qed "Component_well_behaves"; - -(* property 7: local axiom *) -Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}"; -by (constrains_tac 1); -qed "locality"; - - -(**** System properties ****) -(* property 8: strictly universal *) - -Goalw [Safety_def] - "system: stable Safety"; -by (rtac stable_INT 1); -by (constrains_tac 1); -by (Fast_tac 1); -qed "Safety"; - -(* property 13: universal *) -Goal -"system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}"; -by (constrains_tac 1); -by (Blast_tac 1); -qed "p13"; - -(* property 14: the 'above set' of a Component that hasn't got - priority doesn't increase *) -Goal -"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}"; -by (Clarify_tac 1); -by (cut_inst_tac [("i", "j")] reach_lemma 1); -by (constrains_tac 1); -by (auto_tac (claset(), simpset() addsimps [trancl_converse])); -qed "above_not_increase"; - -Goal -"system: -Highest i Int {s. above i s = x} co {s. above i s <= x}"; -by (cut_inst_tac [("i", "i")] above_not_increase 1); -by (asm_full_simp_tac (simpset() addsimps - [trancl_converse, constrains_def]) 1); -by (Blast_tac 1); -qed "above_not_increase'"; - - - -(* p15: universal property: all Components well behave *) -Goal "ALL i. system: Highest i co Highest i Un Lowest i"; -by (Clarify_tac 1); -by (constrains_tac 1); -by Auto_tac; -qed "system_well_behaves"; - - -Goal "Acyclic = (INT i. {s. i~:above i s})"; -by (auto_tac (claset(), simpset() - addsimps [Acyclic_def, acyclic_def, trancl_converse])); -qed "Acyclic_eq"; - - -val lemma = [above_not_increase RS spec, - system_well_behaves RS spec] MRS constrains_Un; -Goal -"system: stable Acyclic"; -by (auto_tac (claset() addSIs [stable_INT, stableI, - lemma RS constrains_weaken], - simpset() addsimps [Acyclic_eq, - image0_r_iff_image0_trancl,trancl_converse])); -qed "Acyclic_stable"; - - -Goalw [Acyclic_def, Maximal_def] -"Acyclic <= Maximal"; -by (Clarify_tac 1); -by (dtac above_lemma_b 1); -by Auto_tac; -qed "Acyclic_subset_Maximal"; - -(* property 17: original one is an invariant *) -Goal -"system: stable (Acyclic Int Maximal)"; -by (simp_tac (simpset() addsimps - [Acyclic_subset_Maximal RS Int_absorb2, Acyclic_stable]) 1); -qed "Acyclic_Maximal_stable"; - - -(* propert 5: existential property *) - -Goal "system: Highest i leadsTo Lowest i"; -by (ensures_tac "act i" 1); -by (auto_tac (claset(), simpset() addsimps [Component_def])); -qed "Highest_leadsTo_Lowest"; - -(* a lowest i can never be in any abover set *) -Goal "Lowest i <= (INT k. {s. i~:above k s})"; -by (auto_tac (claset(), - simpset() addsimps [image0_r_iff_image0_trancl, trancl_converse])); -qed "Lowest_above_subset"; - -(* property 18: a simpler proof than the original, one which uses psp *) -Goal "system: Highest i leadsTo (INT k. {s. i~:above k s})"; -by (rtac leadsTo_weaken_R 1); -by (rtac Lowest_above_subset 2); -by (rtac Highest_leadsTo_Lowest 1); -qed "Highest_escapes_above"; - -Goal -"system: Highest j Int {s. j:above i s} leadsTo {s. j~:above i s}"; -by (blast_tac (claset() addIs - [[Highest_escapes_above, Int_lower1, INT_lower] MRS leadsTo_weaken]) 1); -qed "Highest_escapes_above'"; - -(*** The main result: above set decreases ***) -(* The original proof of the following formula was wrong *) -val above_decreases_lemma = -[Highest_escapes_above', above_not_increase'] MRS psp RS leadsTo_weaken; - -Goal "Highest i = {s. above i s ={}}"; -by (auto_tac (claset(), - simpset() addsimps [image0_trancl_iff_image0_r])); -qed "Highest_iff_above0"; - - -Goal -"system: (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j) \ -\ leadsTo {s. above i s < x}"; -by (rtac leadsTo_UN 1); -by (rtac single_leadsTo_I 1); -by (Clarify_tac 1); -by (res_inst_tac [("x2", "above i x")] above_decreases_lemma 1); -by (ALLGOALS(full_simp_tac (simpset() delsimps [Highest_def] - addsimps [Highest_iff_above0]))); -by (REPEAT(Blast_tac 1)); -qed "above_decreases"; - -(** Just a massage of conditions to have the desired form ***) -Goalw [Maximal_def, Maximal'_def, Highest_def] -"Maximal = Maximal'"; -by (Blast_tac 1); -qed "Maximal_eq_Maximal'"; - -Goal "x~={} ==> \ -\ Acyclic Int {s. above i s = x} <= \ -\ (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j)"; -by (res_inst_tac [("B", "Maximal' Int {s. above i s = x}")] subset_trans 1); -by (simp_tac (simpset() addsimps [Maximal_eq_Maximal' RS sym]) 1); -by (blast_tac (claset() addIs [Acyclic_subset_Maximal RS subsetD]) 1); -by (simp_tac (simpset() delsimps [above_def] addsimps [Maximal'_def, Highest_iff_above0]) 1); -by (Blast_tac 1); -qed "Acyclic_subset"; - -val above_decreases' = [above_decreases, Acyclic_subset] MRS leadsTo_weaken_L; -val above_decreases_psp = [above_decreases', Acyclic_stable] MRS psp_stable; - -Goal -"x~={}==> \ -\ system: Acyclic Int {s. above i s = x} leadsTo Acyclic Int {s. above i s < x}"; -by (etac (above_decreases_psp RS leadsTo_weaken) 1); -by (Blast_tac 1); -by Auto_tac; -qed "above_decreases_psp'"; - - -val finite_psubset_induct = wf_finite_psubset RS leadsTo_wf_induct; -val leadsTo_weaken_L' = rotate_prems 1 leadsTo_weaken_L; - - -Goal "system: Acyclic leadsTo Highest i"; -by (res_inst_tac [("f", "%s. above i s")] finite_psubset_induct 1); -by (asm_simp_tac (simpset() delsimps [Highest_def, above_def] - addsimps [Highest_iff_above0, - vimage_def, finite_psubset_def]) 1); -by (Clarify_tac 1); -by (case_tac "m={}" 1); -by (rtac (Int_lower2 RS leadsTo_weaken_L') 1); -by (force_tac (claset(), simpset() addsimps [leadsTo_refl]) 1); -by (res_inst_tac [("A'", "Acyclic Int {x. above i x < m}")] - leadsTo_weaken_R 1); -by (REPEAT(blast_tac (claset() addIs [above_decreases_psp']) 1)); -qed "Progress"; - -(* We have proved all (relevant) theorems given in the paper *) -(* We didn't assume any thing about the relation r *) -(* It is not necessary that r be a priority relation as assumed in the original proof *) -(* It suffices that we start from a state which is finite and acyclic *) diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Priority.thy --- a/src/HOL/UNITY/Priority.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,68 +0,0 @@ -(* Title: HOL/UNITY/Priority - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -The priority system - -From Charpentier and Chandy, -Examples of Program Composition Illustrating the Use of Universal Properties - In J. Rolim (editor), Parallel and Distributed Processing, - Spriner LNCS 1586 (1999), pages 1215-1227. -*) - -Priority = PriorityAux + Comp + SubstAx + - -types state = "(vertex*vertex)set" -types command = "vertex=>(state*state)set" - -consts - (* the initial state *) - init :: "(vertex*vertex)set" - -constdefs - (* from the definitions given in section 4.4 *) - (* i has highest priority in r *) - highest :: "[vertex, (vertex*vertex)set]=>bool" - "highest i r == A i r = {}" - - (* i has lowest priority in r *) - lowest :: "[vertex, (vertex*vertex)set]=>bool" - "lowest i r == R i r = {}" - - act :: command - "act i == {(s, s'). s'=reverse i s & highest i s}" - - (* All components start with the same initial state *) - Component :: "vertex=>state program" - "Component i == mk_program({init}, {act i}, UNIV)" - - (* Abbreviations *) - Highest :: "vertex=>state set" - "Highest i == {s. highest i s}" - - Lowest :: "vertex=>state set" - "Lowest i == {s. lowest i s}" - - Acyclic :: "state set" - "Acyclic == {s. acyclic s}" - - (* Every above set has a maximal vertex: two equivalent defs. *) - - Maximal :: "state set" - "Maximal == INT i. {s. ~highest i s-->(EX j:above i s. highest j s)}" - - Maximal' :: "state set" - "Maximal' == INT i. Highest i Un (UN j. {s. j:above i s} Int Highest j)" - - - Safety :: "state set" - "Safety == INT i. {s. highest i s --> (ALL j:neighbors i s. ~highest j s)}" - - - (* Composition of a finite set of component; - the vertex 'UNIV' is finite by assumption *) - - system :: "state program" - "system == JN i. Component i" -end \ No newline at end of file diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/PriorityAux.ML --- a/src/HOL/UNITY/PriorityAux.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,116 +0,0 @@ -(* Title: HOL/UNITY/PriorityAux - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -Auxiliary definitions needed in Priority.thy -*) - -Addsimps [derive_def, derive1_def, symcl_def, A_def, R_def, - above_def, reach_def, reverse_def, neighbors_def]; - -(*All vertex sets are finite \\*) -AddIffs [[subset_UNIV, finite_vertex_univ] MRS finite_subset]; - -(* and relatons over vertex are finite too *) -AddIffs [[subset_UNIV, [finite_vertex_univ, finite_vertex_univ] - MRS finite_Prod_UNIV] MRS finite_subset]; - - -(* The equalities (above i r = {}) = (A i r = {}) - and (reach i r = {}) = (R i r) rely on the following theorem *) - -Goal "((r^+)``{i} = {}) = (r``{i} = {})"; -by Auto_tac; -by (etac trancl_induct 1); -by Auto_tac; -qed "image0_trancl_iff_image0_r"; - -(* Another form usefull in some situation *) -Goal "(r``{i}={}) = (ALL x. ((i,x):r^+) = False)"; -by Auto_tac; -by (dtac (image0_trancl_iff_image0_r RS ssubst) 1); -by Auto_tac; -qed "image0_r_iff_image0_trancl"; - - -(* In finite universe acyclic coincides with wf *) -Goal -"!!r::(vertex*vertex)set. acyclic r = wf r"; -by (auto_tac (claset(), simpset() addsimps [wf_iff_acyclic_if_finite])); -qed "acyclic_eq_wf"; - -(* derive and derive1 are equivalent *) -Goal "derive i r q = derive1 i r q"; -by Auto_tac; -qed "derive_derive1_eq"; - -(* Lemma 1 *) -Goalw [reach_def] -"[| x:reach i q; derive1 k r q |] ==> x~=k --> x:reach i r"; -by (etac ImageE 1); -by (etac trancl_induct 1); -by (case_tac "i=k" 1); -by (auto_tac (claset() addIs [r_into_trancl], simpset())); -by (dres_inst_tac [("x", "y")] spec 1); -by (rotate_tac ~1 1); -by (dres_inst_tac [("x", "z")] spec 1); -by (auto_tac (claset() addDs [r_into_trancl] addIs [trancl_trans], simpset())); -qed "lemma1_a"; - -Goal "ALL k r q. derive k r q -->(reach i q <= (reach i r Un {k}))"; -by (REPEAT(rtac allI 1)); -by (rtac impI 1); -by (rtac subsetI 1 THEN dtac lemma1_a 1); -by (auto_tac (claset(), simpset() addsimps [derive_derive1_eq] - delsimps [reach_def, derive_def, derive1_def])); -qed "reach_lemma"; - -(* An other possible formulation of the above theorem based on - the equivalence x:reach y r = y:above x r *) -Goal -"(ALL i. reach i q <= (reach i r Un {k})) =\ -\ (ALL x. x~=k --> (ALL i. i~:above x r --> i~:above x q))"; -by (auto_tac (claset(), simpset() addsimps [trancl_converse])); -qed "reach_above_lemma"; - -(* Lemma 2 *) -Goal -"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)``{z}={})"; -by Auto_tac; -by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1); -by Auto_tac; -qed "maximal_converse_image0"; - -Goal - "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})"; -by (full_simp_tac (simpset() - addsimps [acyclic_eq_wf, wf_eq_minimal]) 1); -by (dres_inst_tac [("x", "((r^-1)^+)``{i}")] spec 1); -by Auto_tac; -by (rotate_tac ~1 1); -by (asm_full_simp_tac (simpset() - addsimps [maximal_converse_image0, trancl_converse]) 1); -qed "above_lemma_a"; - - -Goal - "acyclic r ==> above i r~={}-->(EX j:above i r. above j r = {})"; -by (dtac above_lemma_a 1); -by (auto_tac (claset(), simpset() - addsimps [image0_trancl_iff_image0_r])); -qed "above_lemma_b"; - - - - - - - - - - - - - - diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/PriorityAux.thy --- a/src/HOL/UNITY/PriorityAux.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ -(* Title: HOL/UNITY/PriorityAux - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2001 University of Cambridge - -Auxiliary definitions needed in Priority.thy -*) - -PriorityAux = Main + - -types vertex -arities vertex::term - -constdefs - (* symmetric closure: removes the orientation of a relation *) - symcl :: "(vertex*vertex)set=>(vertex*vertex)set" - "symcl r == r Un (r^-1)" - - (* Neighbors of a vertex i *) - neighbors :: "[vertex, (vertex*vertex)set]=>vertex set" - "neighbors i r == ((r Un r^-1)``{i}) - {i}" - - R :: "[vertex, (vertex*vertex)set]=>vertex set" - "R i r == r``{i}" - - A :: "[vertex, (vertex*vertex)set]=>vertex set" - "A i r == (r^-1)``{i}" - - (* reachable and above vertices: the original notation was R* and A* *) - reach :: "[vertex, (vertex*vertex)set]=> vertex set" - "reach i r == (r^+)``{i}" - - above :: "[vertex, (vertex*vertex)set]=> vertex set" - "above i r == ((r^-1)^+)``{i}" - - reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set" - "reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1" - - (* The original definition *) - derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" - "derive1 i r q == symcl r = symcl q & - (ALL k k'. k~=i & k'~=i -->((k,k'):r) = ((k,k'):q)) & - A i r = {} & R i q = {}" - - (* Our alternative definition *) - derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" - "derive i r q == A i r = {} & (q = reverse i r)" - -rules - (* we assume that the universe of vertices is finite *) - finite_vertex_univ "finite (UNIV :: vertex set)" - -end diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/README.html --- a/src/HOL/UNITY/README.html Mon Mar 05 12:31:31 2001 +0100 +++ b/src/HOL/UNITY/README.html Mon Mar 05 15:25:11 2001 +0100 @@ -23,32 +23,18 @@ in the propositions-as-types paradigm. The resulting style is readable if unconventional. -

-The directory presents a few small examples, mostly taken from Misra's 1994 -paper: -

    -
  • common meeting time - -
  • the token ring - -
  • the communication network - -
  • the lift controller (a standard benchmark) - -
  • a mutual exclusion algorithm - -
  • n-process deadlock - -
  • unordered channel - -
  • reachability in directed graphs (section 6.4 of the book) -
-

Safety proofs (invariants) are often proved automatically. Progress proofs involving ENSURES can sometimes be proved automatically. The level of automation appears to be about the same as in HOL-UNITY by Flemming Andersen et al. +

+The directory Simple +presents a few examples, mostly taken from Misra's 1994 +paper, involving single programs. +The directory Comp +presents examples of proofs involving program composition. +

Last modified on $Date$ diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/ROOT.ML --- a/src/HOL/UNITY/ROOT.ML Mon Mar 05 12:31:31 2001 +0100 +++ b/src/HOL/UNITY/ROOT.ML Mon Mar 05 15:25:11 2001 +0100 @@ -6,35 +6,39 @@ Root file for UNITY proofs. *) -time_use_thy "UNITY"; -time_use_thy "Deadlock"; +(*Basic meta-theory*) +time_use_thy "FP"; time_use_thy "WFair"; -time_use_thy "Common"; -time_use_thy "Network"; -time_use_thy "Token"; -time_use_thy "Channel"; -time_use_thy "Mutex"; -time_use_thy "FP"; -time_use_thy "Reach"; -time_use_thy "Handshake"; -time_use_thy "Lift"; + +(*Simple examples: no composition*) +time_use_thy "Simple/Deadlock"; +time_use_thy "Simple/Common"; +time_use_thy "Simple/Network"; +time_use_thy "Simple/Token"; +time_use_thy "Simple/Channel"; +time_use_thy "Simple/Lift"; +time_use_thy "Simple/Mutex"; +time_use_thy "Simple/Reach"; +time_use_thy "Simple/Reachability"; + +with_path "../Auth" (*to find Public.thy*) + time_use_thy"Simple/NSP_Bad"; + +(*Example of composition*) time_use_thy "Comp"; -time_use_thy "Reachability"; +time_use_thy "Comp/Handshake"; (*Universal properties examples*) -time_use_thy "Counter"; -time_use_thy "Counterc"; -time_use_thy "Priority"; +time_use_thy "Comp/Counter"; +time_use_thy "Comp/Counterc"; +time_use_thy "Comp/Priority"; (*Allocator example*) time_use_thy "PPROD"; -time_use_thy "TimerArray"; +time_use_thy "Comp/TimerArray"; -time_use_thy "Alloc"; -time_use_thy "AllocImpl"; -time_use_thy "Client"; +time_use_thy "Comp/Alloc"; +time_use_thy "Comp/AllocImpl"; +time_use_thy "Comp/Client"; time_use_thy "ELT"; (*obsolete*) - -with_path "../Auth" (*to find Public.thy*) - time_use_thy"NSP_Bad"; diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Reach.ML --- a/src/HOL/UNITY/Reach.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,142 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Reach.thy --- a/src/HOL/UNITY/Reach.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,43 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Reachability.ML --- a/src/HOL/UNITY/Reachability.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,308 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Reachability.thy --- a/src/HOL/UNITY/Reachability.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,72 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/TimerArray.ML --- a/src/HOL/UNITY/TimerArray.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,53 +0,0 @@ -(* Title: HOL/UNITY/TimerArray.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -A trivial example of reasoning about an array of processes -*) - -Addsimps [Timer_def RS def_prg_Init]; -program_defs_ref := [Timer_def]; - -Addsimps [count_def, decr_def]; - -(*Demonstrates induction, but not used in the following proof*) -Goal "Timer : UNIV leadsTo {s. count s = 0}"; -by (res_inst_tac [("f", "count")] lessThan_induct 1); -by (Simp_tac 1); -by (case_tac "m" 1); -by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1); -by (ensures_tac "decr" 1); -qed "Timer_leadsTo_zero"; - -Goal "Timer : preserves snd"; -by (rtac preservesI 1); -by (constrains_tac 1); -qed "Timer_preserves_snd"; -AddIffs [Timer_preserves_snd]; - -Addsimps [PLam_stable]; - -Goal "finite I \ -\ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"; -by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")] - (finite_stable_completion RS leadsTo_weaken) 1); -by Auto_tac; -(*Safety property, already reduced to the single Timer case*) -by (constrains_tac 2); -(*Progress property for the array of Timers*) -by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1); -by (case_tac "m" 1); -(*Annoying need to massage the conditions to have the form (... <*> UNIV)*) -by (auto_tac (claset() addIs [subset_imp_leadsTo], - simpset() addsimps [insert_absorb, lessThan_Suc RS sym, - lift_set_Un_distrib RS sym, - Times_Un_distrib1 RS sym, - Times_Diff_distrib1 RS sym])); -by (rename_tac "n" 1); -by (rtac PLam_leadsTo_Basis 1); -by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym])); -by (constrains_tac 1); -by (res_inst_tac [("act", "decr")] transientI 1); -by (auto_tac (claset(), simpset() addsimps [Timer_def])); -qed "TimerArray_leadsTo_zero"; diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/TimerArray.thy --- a/src/HOL/UNITY/TimerArray.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* Title: HOL/UNITY/TimerArray.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1998 University of Cambridge - -A trivial example of reasoning about an array of processes -*) - -TimerArray = PPROD + - -types 'a state = "nat * 'a" (*second component allows new variables*) - -constdefs - count :: "'a state => nat" - "count s == fst s" - - decr :: "('a state * 'a state) set" - "decr == UN n uu. {((Suc n, uu), (n,uu))}" - - Timer :: 'a state program - "Timer == mk_program (UNIV, {decr}, UNIV)" - -end diff -r 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Token.ML --- a/src/HOL/UNITY/Token.ML Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,101 +0,0 @@ -(* 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 5fd02b905a9a -r 851c90b23a9e src/HOL/UNITY/Token.thy --- a/src/HOL/UNITY/Token.thy Mon Mar 05 12:31:31 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,66 +0,0 @@ -(* 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