--- 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
--- 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 : <unfolded specification> *)
-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 : <unfolded specification> *)
-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 : <unfolded specification> *)
-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<Nclients. \
-\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
-by (auto_tac (claset(), simpset() addsimps [Collect_all_imp_eq]));
-by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask]
- RS Always_weaken) 1);
-by (auto_tac (claset() addDs [set_mono], simpset()));
-qed "System_Bounded_allocAsk";
-
-(*progress (2), step 5 is System_Increasing_allocGiv*)
-
-(*progress (2), step 6*)
-(* i < Nclients ==> 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";
--- 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<Nclients.
- 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})
- guarantees
- (INT i : lessThan Nclients.
- INT h. {s. h <= (sub i o allocAsk) s}
- LeadsTo
- {s. h pfixLe (sub i o allocGiv) s})"
-
- (*NOTE: to follow the original paper, the formula above should have had
- INT h. {s. h i <= (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
- LeadsTo
- {s. tokens h i <= (tokens o sub i o allocRel)s})
- thus h should have been a function variable. However, only h i is ever
- looked at.*)
-
- (*spec: preserves part*)
- alloc_preserves :: 'a allocState_d program set
- "alloc_preserves == preserves allocRel Int preserves allocAsk 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 allocGiv) 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"
-
-(** 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
- ((sub i o allocAsk) Fols (ask o sub i o client))"
-
- (*spec (9.2)*)
- network_giv :: 'a systemState program set
- "network_giv == INT i : lessThan Nclients.
- Increasing (sub i o allocGiv)
- guarantees
- ((giv o sub i o client) Fols (sub i o allocGiv))"
-
- (*spec (9.3)*)
- network_rel :: 'a systemState program set
- "network_rel == INT i : lessThan Nclients.
- Increasing (rel o sub i o client)
- guarantees
- ((sub i o allocRel) Fols (rel o sub i o client))"
-
- (*spec: preserves part*)
- network_preserves :: 'a systemState program set
- "network_preserves ==
- preserves allocGiv Int
- (INT i : lessThan Nclients. preserves (rel o sub i o client) Int
- preserves (ask o sub i o client))"
-
- (*environmental constraints*)
- network_allowed_acts :: 'a systemState program set
- "network_allowed_acts ==
- {F. AllowedActs F =
- insert Id
- (UNION (preserves allocRel Int
- (INT i: lessThan Nclients. preserves(giv o sub i o client)))
- Acts)}"
-
- network_spec :: 'a systemState program set
- "network_spec == network_ask Int network_giv Int
- network_rel Int network_allowed_acts Int
- network_preserves"
-
-
-(** State mappings **)
- sysOfAlloc :: "((nat => 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
--- 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<n --> 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<k then f i else g i#}) (A Int lessThan k) = \
-\ setsum (%i. {#f i#}) (A Int lessThan k)";
-by (rtac setsum_cong 1);
-by Auto_tac;
-qed "bag_of_sublist_lemma";
-
-Goal "bag_of (sublist l A) = \
-\ setsum (%i. {# l!i #}) (A Int lessThan (length l))";
-by (rev_induct_tac "l" 1);
-by (Simp_tac 1);
-by (asm_simp_tac
- (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc,
- nth_append, bag_of_sublist_lemma] @ thms "plus_ac0") 1);
-qed "bag_of_sublist";
-
-
-Goal "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
-\ bag_of (sublist l A) + bag_of (sublist l B)";
-by (subgoal_tac "A Int B Int {..length l(} = \
-\ (A Int {..length l(}) Int (B Int {..length l(})" 1);
-by (asm_simp_tac (simpset() addsimps [bag_of_sublist, Int_Un_distrib2,
- setsum_Un_Int]) 1);
-by (Blast_tac 1);
-qed "bag_of_sublist_Un_Int";
-
-Goal "A Int B = {} \
-\ ==> 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";
--- 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
--- 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<Nclients --> \
-\ (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<Nclients --> \
-\ (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";
-
-
--- 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
--- 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";
--- 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
--- 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<h & h <= giv s & h pfixGe ask s}";
-by (res_inst_tac [("act", "rel_act")] transientI 1);
-by (auto_tac (claset(),
- simpset() addsimps [Domain_def, Client_def]));
-by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
- strict_prefix_length_less]) 1);
-by (auto_tac (claset(),
- simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def]));
-by (blast_tac (claset() addIs [strict_prefix_length_less]) 1);
-qed "transient_lemma";
-
-
-Goal "[| Client Join G : Increasing giv; Client ok G |] \
-\ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s} \
-\ LeadsTo {s. k < rel s & rel s <= giv s & \
-\ h <= giv s & h pfixGe ask s}";
-by (rtac single_LeadsTo_I 1);
-by (ftac (increasing_ask_rel RS guaranteesD) 1);
-by Auto_tac;
-by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS
- leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
-by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
-by (eres_inst_tac [("f", "giv"), ("x", "giv s")] IncreasingD 1);
-by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1);
-by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1);
-by (etac Join_Stable_rel_le_giv 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addIs [sym, order_less_le RS iffD2,
- order_trans, prefix_imp_pfixGe,
- pfixGe_trans]) 2);
-by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1);
-qed "induct_lemma";
-
-
-Goal "[| Client Join G : Increasing giv; Client ok G |] \
-\ ==> 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";
--- 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
--- 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 <max (ftime t) (gtime t) *)
-Goal "mk_program \
-\ (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV) \
-\ : {m} co (maxfg m)";
-by (simp_tac
- (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
-result();
-
-
-(*It remans to prove that they satisfy CMT3': t does not decrease,
- and that CMT3' implies that t stops changing once common(t) holds.*)
-
-
-(*** Progress under weak fairness ***)
-
-Addsimps [atMost_Int_atLeast];
-
-Goal "[| ALL m. F : {m} Co (maxfg m); \
-\ ALL m: lessThan n. F : {m} LeadsTo (greaterThan m); \
-\ n: common |] \
-\ ==> F : (atMost n) LeadsTo common";
-by (rtac LeadsTo_weaken_R 1);
-by (res_inst_tac [("f","id"), ("l","n")] GreaterThan_bounded_induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (rtac subset_refl 2);
-by (blast_tac (claset() addDs [PSP_Stable2]
- addIs [common_stable, LeadsTo_weaken_R]) 1);
-val lemma = result();
-
-(*The "ALL m: -common" form echoes CMT6.*)
-Goal "[| ALL m. F : {m} Co (maxfg m); \
-\ ALL m: -common. F : {m} LeadsTo (greaterThan m); \
-\ n: common |] \
-\ ==> F : (atMost (LEAST n. n: common)) LeadsTo common";
-by (rtac lemma 1);
-by (ALLGOALS Asm_simp_tac);
-by (etac LeastI 2);
-by (blast_tac (claset() addSDs [not_less_Least]) 1);
-qed "leadsTo_common";
--- 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
--- 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<n --> 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<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<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<I ==> (JN i:{i. i<I}. Component i):invariant {s. s C = sum I s}";
-by (simp_tac (simpset() addsimps [JN_stable,Init_JN,sum_sumj]) 1);
-by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1);
-qed "safety";
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- a/src/HOL/UNITY/Counter.thy Mon Mar 05 12:31:31 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +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.
-*)
-
-Counter = Comp +
-(* Variables are names *)
-datatype name = C | c nat
-types state = name=>int
-
-consts
- sum :: "[nat,state]=>int"
- sumj :: "[nat, nat, state]=>int"
-
-primrec (* sum I s = sigma_{i<I}. s (c i) *)
- "sum 0 s = #0"
- "sum (Suc i) s = s (c i) + sum i s"
-
-primrec
- "sumj 0 i s = #0"
- "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
-
-types command = "(state*state)set"
-
-constdefs
- a :: "nat=>command"
- "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
--- 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<i--> (sum I s = sumj I i s)";
-by (induct_tac "I" 1);
-by Auto_tac;
-qed_spec_mp "sum_sumj_eq1";
-
-Goal "i<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<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<I & j~=i --> 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<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<I} Component; i<I |] ==> \
-\ ALL k. Component i: stable ({s. C s = c s i + sumj I i k} Int \
-\ {s. ALL j:{i. i<I}. j~=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<I}. j~=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<I} Component; 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<I; OK {i. i<I} Component |] \
-\ ==> (JN i:{i. i<I}. (Component i)) : invariant {s. C s = sum I s}";
-by (simp_tac (simpset() addsimps [JN_stable, sum_sumj_eq2]) 1);
-by (auto_tac (claset() addSIs [sum0 RS mp, p2_p3],
- simpset()));
-qed "safety";
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- a/src/HOL/UNITY/Counterc.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/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.
-*)
-
-Counterc = Comp +
-types state
-arities state :: term
-
-consts
- C :: "state=>int"
- c :: "state=>nat=>int"
-
-consts
- sum :: "[nat,state]=>int"
- sumj :: "[nat, nat, state]=>int"
-
-primrec (* sum I s = sigma_{i<I}. c s i *)
- "sum 0 s = #0"
- "sum (Suc i) s = (c s) i + sum i s"
-
-primrec
- "sumj 0 i s = #0"
- "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
-
-types command = "(state*state)set"
-
-constdefs
- a :: "nat=>command"
- "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
--- 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();
-
--- 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
--- 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";
--- 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
--- 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<N ==> Lift : (moving Int Req n Int {s. metric n s = N} Int \
-\ {s. floor s ~: req s}) LeadsTo \
-\ (moving Int Req n Int {s. metric n s < N})";
-by (rtac ([subset_imp_LeadsTo, [E_thm12a, E_thm12b] MRS LeadsTo_Un]
- MRS LeadsTo_Trans) 1);
-by Auto_tac;
-qed "lift_4";
-
-
-(** towards lift_5 **)
-
-(*lem_lift_5_3*)
-Goal "#0<N \
-\ ==> Lift : (closed Int Req n Int {s. metric n s = N} Int goingup) LeadsTo \
-\ (moving Int Req n Int {s. metric n s < N})";
-by (cut_facts_tac [bounded] 1);
-by (ensures_tac "req_up" 1);
-by (auto_tac (claset(), metric_ss));
-qed "E_thm16a";
-
-
-(*lem_lift_5_1 has ~goingup instead of goingdown*)
-Goal "#0<N ==> \
-\ Lift : (closed Int Req n Int {s. metric n s = N} Int goingdown) LeadsTo \
-\ (moving Int Req n Int {s. metric n s < N})";
-by (cut_facts_tac [bounded] 1);
-by (ensures_tac "req_down" 1);
-by (auto_tac (claset(), metric_ss));
-qed "E_thm16b";
-
-
-(*lem_lift_5_0 proves an intersection involving ~goingup and goingup,
- i.e. the trivial disjunction, leading to an asymmetrical proof.*)
-Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
-by (Clarify_tac 1);
-by (auto_tac (claset(), metric_ss));
-qed "E_thm16c";
-
-
-(*lift_5*)
-Goal "#0<N ==> Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo \
-\ (moving Int Req n Int {s. metric n s < N})";
-by (rtac ([subset_imp_LeadsTo, [E_thm16a, E_thm16b] MRS LeadsTo_Un]
- MRS LeadsTo_Trans) 1);
-by (dtac E_thm16c 1);
-by Auto_tac;
-qed "lift_5";
-
-
-(** towards lift_3 **)
-
-(*lemma used to prove lem_lift_3_1*)
-Goal "[| metric n s = #0; Min <= floor s; floor s <= Max |] ==> floor s = n";
-by (auto_tac (claset(), metric_ss));
-qed "metric_eq_0D";
-
-AddDs [metric_eq_0D];
-
-
-(*lem_lift_3_1*)
-Goal "Lift : (moving Int Req n Int {s. metric n s = #0}) LeadsTo \
-\ (stopped Int atFloor n)";
-by (cut_facts_tac [bounded] 1);
-by (ensures_tac "request_act" 1);
-by Auto_tac;
-qed "E_thm11";
-
-(*lem_lift_3_5*)
-Goal
- "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
-\ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
-by (ensures_tac "request_act" 1);
-by (auto_tac (claset(), metric_ss));
-qed "E_thm13";
-
-(*lem_lift_3_6*)
-Goal "#0 < N ==> \
-\ Lift : \
-\ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
-\ LeadsTo (opened Int Req n Int {s. metric n s = N})";
-by (ensures_tac "open_act" 1);
-by (auto_tac (claset(), metric_ss));
-qed "E_thm14";
-
-(*lem_lift_3_7*)
-Goal "Lift : (opened Int Req n Int {s. metric n s = N}) \
-\ LeadsTo (closed Int Req n Int {s. metric n s = N})";
-by (ensures_tac "close_act" 1);
-by (auto_tac (claset(), metric_ss));
-qed "E_thm15";
-
-
-(** the final steps **)
-
-Goal "#0 < N ==> \
-\ Lift : \
-\ (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
-\ LeadsTo (moving Int Req n Int {s. metric n s < N})";
-by (blast_tac (claset() addSIs [E_thm13, E_thm14, E_thm15, lift_5]
- addIs [LeadsTo_Trans]) 1);
-qed "lift_3_Req";
-
-
-(*Now we observe that our integer metric is really a natural number*)
-Goal "Lift : Always {s. #0 <= metric n s}";
-by (rtac (bounded RS Always_weaken) 1);
-by (auto_tac (claset(), metric_ss));
-qed "Always_nonneg";
-
-val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken;
-
-Goal "Lift : (moving Int Req n) LeadsTo (stopped Int atFloor n)";
-by (rtac (Always_nonneg RS integ_0_le_induct) 1);
-by (case_tac "#0 < z" 1);
-(*If z <= #0 then actually z = #0*)
-by (force_tac (claset() addIs [R_thm11, order_antisym],
- simpset() addsimps [linorder_not_less]) 2);
-by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1);
-by (rtac ([subset_imp_LeadsTo, [lift_4, lift_3_Req] MRS LeadsTo_Un]
- MRS LeadsTo_Trans) 1);
-by Auto_tac;
-qed "lift_3";
-
-
-val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un;
-(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *)
-
-Goal "Lift : (Req n) LeadsTo (opened Int atFloor n)";
-by (rtac LeadsTo_Trans 1);
-by (rtac ([E_thm04, LeadsTo_Un_post] MRS LeadsTo_Un) 2);
-by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2);
-by (rtac (lift_3 RS LeadsTo_Trans_Un') 2);
-by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
-by (rtac ([E_thm03,E_thm02] MRS LeadsTo_Trans_Un') 2);
-by (rtac (open_move RS Always_LeadsToI) 1);
-by (rtac ([open_stop, subset_imp_LeadsTo] MRS Always_LeadsToI) 1);
-by (Clarify_tac 1);
-(*The case split is not essential but makes Blast_tac much faster.
- Calling rotate_tac prevents simplification from looping*)
-by (case_tac "open x" 1);
-by (ALLGOALS (rotate_tac ~1));
-by Auto_tac;
-qed "lift_1";
-
-Close_locale "floor";
--- 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
--- 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";
--- 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
--- 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
-*)
--- 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
--- 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();
-
-
-
-
--- 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
--- 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 *)
--- 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
--- 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 \\<dots>*)
-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";
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- 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
--- 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.
-<P>
-The directory presents a few small examples, mostly taken from Misra's 1994
-paper:
-<UL>
-<LI>common meeting time
-
-<LI>the token ring
-
-<LI>the communication network
-
-<LI>the lift controller (a standard benchmark)
-
-<LI>a mutual exclusion algorithm
-
-<LI><EM>n</EM>-process deadlock
-
-<LI>unordered channel
-
-<LI>reachability in directed graphs (section 6.4 of the book)
-</UL>
-
<P> 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.
+<P>
+The directory <A HREF="Simple/"><CODE>Simple</CODE></A>
+presents a few examples, mostly taken from Misra's 1994
+paper, involving single programs.
+The directory <A HREF="Comp/"><CODE>Comp</CODE></A>
+presents examples of proofs involving program composition.
+
<HR>
<P>Last modified on $Date$
--- 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";
--- 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";
--- 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
--- 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";
--- 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
-
--- 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";
--- 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
--- 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<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
-by (auto_tac (claset(), simpset() addsimps [mod_Suc, mod_geq]));
-by (auto_tac (claset(),
- simpset() addsplits [nat_diff_split]
- addsimps [linorder_neq_iff, mod_geq]));
-qed "nodeOrder_eq";
-
-(*From "A Logic for Concurrent Programming", but not used in Chapter 4.
- Note the use of case_tac. Reasoning about leadsTo takes practice!*)
-Goal "[| i<N; j<N |] ==> \
-\ F : (HasTok i) leadsTo ({s. (token s, i) : nodeOrder j} Un HasTok j)";
-by (case_tac "i=j" 1);
-by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
-by (rtac (TR7 RS leadsTo_weaken_R) 1);
-by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
-qed "TR7_nodeOrder";
-
-
-(*Chapter 4 variant, the one actually used below.*)
-Goal "[| i<N; j<N; i~=j |] \
-\ ==> F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}";
-by (rtac (TR7 RS leadsTo_weaken_R) 1);
-by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq]));
-qed "TR7_aux";
-
-Goal "({s. token s < N} Int token -` {m}) = (if m<N then token -` {m} else {})";
-by Auto_tac;
-val token_lemma = result();
-
-
-(*Misra's TR9: the token reaches an arbitrary node*)
-Goal "j<N ==> F : {s. token s < N} leadsTo (HasTok j)";
-by (rtac leadsTo_weaken_R 1);
-by (res_inst_tac [("I", "-{j}"), ("f", "token"), ("B", "{}")]
- (wf_nodeOrder RS bounded_induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [token_lemma, vimage_Diff,
- HasTok_def])));
-by (Blast_tac 2);
-by (Clarify_tac 1);
-by (rtac (TR7_aux RS leadsTo_weaken) 1);
-by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_def]));
-qed "leadsTo_j";
-
-(*Misra's TR8: a hungry process eventually eats*)
-Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)";
-by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
-by (rtac TR6 2);
-by (rtac ([leadsTo_j, TR3] MRS psp RS leadsTo_weaken) 1);
-by (ALLGOALS Blast_tac);
-qed "token_progress";
--- 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<N"
-
- TR2 "F : (T i) co (T i Un H i)"
-
- TR3 "F : (H i) co (H i Un E i)"
-
- TR4 "F : (H i - HasTok i) co (H i)"
-
- TR5 "F : (HasTok i) co (HasTok i Un -(E i))"
-
- TR6 "F : (H i Int HasTok i) leadsTo (E i)"
-
- TR7 "F : (HasTok i) leadsTo (HasTok (next i))"
-
- defines
- nodeOrder_def
- "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int
- (lessThan N <*> lessThan N)"
-
- next_def
- "next i == (Suc i) mod N"
-
-end