# HG changeset patch # User paulson # Date 950093110 -3600 # Node ID e4b3192dfefad55601be16f0d66f0ac4dc865740 # Parent d3eba67a9e6730bf2c4864bd7796b5b777841d91 updated the Client example diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/Client.ML --- a/src/HOL/UNITY/Client.ML Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/Client.ML Wed Feb 09 11:45:10 2000 +0100 @@ -6,9 +6,8 @@ Distributed Resource Management System: the Client *) - -Addsimps [Cli_prg_def RS def_prg_Init]; -program_defs_ref := [Cli_prg_def]; +Addsimps [Client_def RS def_prg_Init]; +program_defs_ref := [Client_def]; Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]); @@ -17,121 +16,150 @@ rtac invariantI i THEN constrains_tac (i+1); -(*Safety property 1(a): ask is nondecreasing*) -Goalw [increasing_def] "Cli_prg: increasing ask"; -by (Clarify_tac 1); -by (constrains_tac 1); -by Auto_tac; -qed "increasing_ask"; -(*Safety property 1(b): rel is nondecreasing*) -Goalw [increasing_def] "Cli_prg: increasing rel"; -by (Clarify_tac 1); -by (constrains_tac 1); +(*Safety property 1: ask, rel are increasing*) +Goal "Client: UNIV guarantees[funPair rel ask] \ +\ Increasing ask Int Increasing rel"; +by (safe_tac (claset() addSIs [guaranteesI,increasing_imp_Increasing])); +by (auto_tac + (claset(), + simpset() addsimps [impOfSubs preserves_subset_increasing, + Join_increasing])); +by (auto_tac (claset(), simpset() addsimps [increasing_def])); +by (ALLGOALS constrains_tac); by Auto_tac; -qed "increasing_rel"; +qed "increasing_ask_rel"; + Addsimps [nth_append, append_one_prefix]; -Goal "Cli_prg: invariant {s. tok s <= Max}"; -by (invariant_tac 1); -by Auto_tac; -qed "tok_bounded"; -(*Safety property 3: no client requests "too many" tokens. +(*Safety property 2: the client never requests too many tokens. With no Substitution Axiom, we must prove the two invariants - simultaneously. Could combine tok_bounded, stable_constrains_stable - and a rule invariant_implies_stable... + simultaneously. *) -Goal "Cli_prg: \ -\ invariant ({s. tok s <= Max} Int \ -\ {s. ALL n: lessThan (size (ask s)). ask s!n <= Max})"; -by (invariant_tac 1); -by (auto_tac (claset() addSEs [less_SucE], simpset())); +Goal "G : preserves (funPair ask tok) \ +\ ==> Client Join G : \ +\ Always ({s. tok s <= NbT} Int \ +\ {s. ALL elt : set (ask s). elt <= NbT})"; +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 Auto_tac; +qed "ask_bounded_lemma"; + +(*export version, with no mention of tok*) +Goal "Client: UNIV guarantees[funPair ask tok] \ +\ 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"; -(** Several facts used to prove Lemma 1 **) -Goal "Cli_prg: stable {s. rel s <= giv s}"; +(*** 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 "Cli_prg: stable {s. size (rel s) <= size (giv s)}"; +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 (rtac AlwaysI 1); +by (rtac Join_Stable_rel_le_giv 2); +by Auto_tac; +qed "Join_Always_rel_le_giv"; + +Goal "Client : transient {s. rel s = k & k Client Join G : {s. rel s = k & k Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s} \ +\ LeadsTo {s. h <= rel s}"; +by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1); +by (auto_tac (claset(), simpset() addsimps [vimage_def])); +by (rtac single_LeadsTo_I 1); +by (rtac (induct_lemma RS LeadsTo_weaken) 1); +by Auto_tac; +by (blast_tac (claset() addIs [order_less_le RS iffD2] + addDs [common_prefix_linear]) 1); +by (REPEAT (dtac strict_prefix_length_less 1)); +by (arith_tac 1); +qed "rel_progress_lemma"; + + +Goal "[| Client Join G : Increasing giv; G : preserves (funPair rel ask) |] \ +\ ==> 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"; + +Goal "Client : \ +\ Increasing giv guarantees[funPair rel ask] \ +\ (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"; + + +(** 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"; -Goal "Cli_prg: stable {s. size (ask s) <= Suc (size (rel s))}"; -by (constrains_tac 1); -by Auto_tac; -qed "stable_size_ask_le_rel"; - - -(*We no longer need constrains_tac to expand the program definition, and - expanding it is extremely expensive!*) -program_defs_ref := []; - -(*Safety property 2: clients return the right number of tokens*) -Goal "Cli_prg : Increasing giv guarantees[rel] Always {s. rel s <= giv s}"; +(*clients return the right number of tokens*) +Goal "Client : Increasing giv guarantees[rel] 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"; - - -(*** Towards proving the liveness property ***) - -Goal "Cli_prg Join G \ -\ : transient {s. size (giv s) = Suc k & \ -\ size (rel s) = k & ask s ! k <= giv s ! k}"; -by (res_inst_tac [("act", "rel_act")] transientI 1); -by (auto_tac (claset(), - simpset() addsimps [Domain_def, Cli_prg_def])); -qed "transient_lemma"; - - - -val rewrite_o = rewrite_rule [o_def]; - -val Increasing_length = mono_length RS mono_Increasing_o; - -Goal "Cli_prg : \ -\ Increasing giv guarantees[funPair rel ask] \ -\ Always ({s. size (ask s) <= Suc (size (rel s))} Int \ -\ {s. size (rel s) <= size (giv s)})"; -by (rtac guaranteesI 1); -by (dtac (impOfSubs (rewrite_o Increasing_length)) 1); -by (rtac AlwaysI 1); -by (Force_tac 1); -by (rtac Stable_Int 1); -by (fast_tac (claset() addEs [rewrite_o (impOfSubs subset_preserves_o)] - addIs [Increasing_preserves_Stable, - stable_size_rel_le_giv]) 2); -by (res_inst_tac [("v1", "ask"), ("w1", "rel")] - (stable_localTo_stable2 RS stable_imp_Stable) 1); -by (ALLGOALS - (fast_tac (claset() addEs [rewrite_o (impOfSubs subset_preserves_o)] - addIs [stable_size_ask_le_rel]))); -val lemma1 = result(); - - -Goal "Cli_prg : \ -\ Increasing giv Int Always giv_meets_ask \ -\ guarantees[funPair rel ask] \ -\ ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})"; -by (rtac guaranteesI 1); -by (Clarify_tac 1); -by (rtac Stable_transient_Always_LeadsTo 1); -by (res_inst_tac [("k", "k")] transient_lemma 2); -by (force_tac (claset() addDs [impOfSubs Increasing_length, - impOfSubs Increasing_Stable_less], - simpset()) 1); -by (rtac (make_elim (lemma1 RS guaranteesD)) 1); -by Auto_tac; -by (force_tac (claset(), - simpset() addsimps [Always_eq_includes_reachable, - giv_meets_ask_def]) 1); -qed "client_correct"; diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/Client.thy --- a/src/HOL/UNITY/Client.thy Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/Client.thy Wed Feb 09 11:45:10 2000 +0100 @@ -6,10 +6,10 @@ Distributed Resource Management System: the Client *) -Client = Guar + +Client = Extend + consts - Max :: nat (*Maximum number of tokens*) + NbT :: nat (*Maximum number of tokens*) types tokbag = nat (*tokbags could be multisets...or any ordered type?*) @@ -40,19 +40,21 @@ of the action to be ignored **) tok_act :: "(state*state) set" - "tok_act == {(s,s'). s'=s | (EX t: atMost Max. s' = s (|tok := t|))}" + "tok_act == {(s,s'). s'=s | (EX t: atMost NbT. s' = s (|tok := t|))}" + (* + "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" + *) + + ask_act :: "(state*state) set" "ask_act == {(s,s'). s'=s | - (s' = s (|ask := ask s @ [tok s]|) & - size (ask s) = size (rel s))}" + (s' = s (|ask := ask s @ [tok s]|))}" - Cli_prg :: state program - "Cli_prg == mk_program ({s. tok s : atMost Max & - giv s = [] & - ask s = [] & - rel s = []}, - {rel_act, tok_act, ask_act})" + Client :: state program + "Client == mk_program ({s. tok s : atMost NbT & + giv s = [] & ask s = [] & rel s = []}, + {rel_act, tok_act, ask_act})" giv_meets_ask :: state set "giv_meets_ask == diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/Comp.ML --- a/src/HOL/UNITY/Comp.ML Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/Comp.ML Wed Feb 09 11:45:10 2000 +0100 @@ -132,6 +132,12 @@ by (ALLGOALS Force_tac); qed "preserves_subset_stable"; +Goal "preserves v <= increasing v"; +by (auto_tac (claset(), + simpset() addsimps [impOfSubs preserves_subset_stable, + increasing_def])); +qed "preserves_subset_increasing"; + Goal "preserves id <= stable A"; by (force_tac (claset(), simpset() addsimps [preserves_def, stable_def, constrains_def]) 1); diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/Constrains.ML --- a/src/HOL/UNITY/Constrains.ML Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/Constrains.ML Wed Feb 09 11:45:10 2000 +0100 @@ -203,6 +203,11 @@ (*** Increasing ***) +Goalw [Increasing_def] + "F : Increasing f ==> F : Stable {s. x <= f s}"; +by (Blast_tac 1); +qed "IncreasingD"; + Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def] "mono g ==> Increasing f <= Increasing (g o f)"; by Auto_tac; @@ -210,10 +215,10 @@ qed "mono_Increasing_o"; Goalw [Increasing_def] - "Increasing f <= {F. ALL z::nat. F: Stable {s. z < f s}}"; + "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}"; by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); by (Blast_tac 1); -qed "Increasing_Stable_less"; +qed "strict_IncreasingD"; Goalw [increasing_def, Increasing_def] "F : increasing f ==> F : Increasing f"; diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/Extend.ML --- a/src/HOL/UNITY/Extend.ML Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/Extend.ML Wed Feb 09 11:45:10 2000 +0100 @@ -203,6 +203,9 @@ (*** extend_act ***) +(*Can't strengthen it to + ((h(s,y), h(s',y')) : extend_act h act) = ((s, s') : act & y=y') + because h doesn't have to be injective in the 2nd argument*) Goalw [extend_act_def] "((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)"; by Auto_tac; diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/Follows.ML --- a/src/HOL/UNITY/Follows.ML Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/Follows.ML Wed Feb 09 11:45:10 2000 +0100 @@ -110,11 +110,6 @@ by (Blast_tac 1); qed "Always_Un"; -Goalw [Increasing_def] - "F : Increasing f ==> F : Stable {s. x <= f s}"; -by (Blast_tac 1); -qed "IncreasingD"; - (*Lemma to re-use the argument that one variable increases (progress) while the other variable doesn't decrease (safety)*) Goal "[| F : Increasing f; F : Increasing g; \ diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/GenPrefix.ML --- a/src/HOL/UNITY/GenPrefix.ML Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/GenPrefix.ML Wed Feb 09 11:45:10 2000 +0100 @@ -278,6 +278,15 @@ by (etac genPrefix_length_le 1); qed "prefix_length_le"; +Goalw [prefix_def] "xs<=ys ==> xs~=ys --> length xs < length ys"; +by (etac genPrefix.induct 1); +by Auto_tac; +val lemma = result(); + +Goalw [strict_prefix_def] "xs < ys ==> length xs < length ys"; +by (blast_tac (claset() addIs [lemma RS mp]) 1); +qed "strict_prefix_length_less"; + Goal "mono length"; by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1); qed "mono_length"; @@ -313,6 +322,13 @@ by (Force_tac 1); qed "prefix_append_iff"; +(*Although the prefix ordering is not linear, the prefixes of a list + are linearly ordered.*) +Goal "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"; +by (rev_induct_tac "zs" 1); +by Auto_tac; +qed_spec_mp "common_prefix_linear"; + Goal "r<=s ==> genPrefix r <= genPrefix s"; by (Clarify_tac 1); by (etac genPrefix.induct 1); diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/Lift_prog.ML --- a/src/HOL/UNITY/Lift_prog.ML Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/Lift_prog.ML Wed Feb 09 11:45:10 2000 +0100 @@ -122,7 +122,7 @@ fun lift_export0 th = good_map_lift_map RS export th - |> simplify (simpset() addsimps [fold_o_sub]);; + |> simplify (simpset() addsimps [fold_o_sub]); Goal "fst (inv (lift_map i) g) = g i"; by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1); diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/SubstAx.ML --- a/src/HOL/UNITY/SubstAx.ML Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/SubstAx.ML Wed Feb 09 11:45:10 2000 +0100 @@ -129,7 +129,7 @@ (** Two theorems for "proof lattices" **) -Goal "[| F : A LeadsTo B |] ==> F : (A Un B) LeadsTo B"; +Goal "F : A LeadsTo B ==> F : (A Un B) LeadsTo B"; by (blast_tac (claset() addIs [LeadsTo_Un, subset_imp_LeadsTo]) 1); qed "LeadsTo_Un_post"; @@ -334,11 +334,11 @@ qed "Bounded_induct"; -Goal "[| ALL m. F : (A Int f-``{m}) LeadsTo \ -\ ((A Int f-``(lessThan m)) Un B) |] \ +val prems = +Goal "(!! m. F : (A Int f-``{m}) LeadsTo ((A Int f-``(lessThan m)) Un B)) \ \ ==> F : A LeadsTo B"; by (rtac (wf_less_than RS LeadsTo_wf_induct) 1); -by (Asm_simp_tac 1); +by (auto_tac (claset() addIs prems, simpset())); qed "LessThan_induct"; (*Integer version. Could generalize from #0 to any lower bound*) @@ -347,7 +347,7 @@ \ !! z. F : (A Int {s. f s = z}) LeadsTo \ \ ((A Int {s. f s < z}) Un B) |] \ \ ==> F : A LeadsTo B"; -by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1); +by (res_inst_tac [("f", "nat o f")] LessThan_induct 1); by (simp_tac (simpset() addsimps [vimage_def]) 1); by (rtac ([reach, prem] MRS Always_LeadsTo_weaken) 1); by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff])); diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/UNITY.ML --- a/src/HOL/UNITY/UNITY.ML Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/UNITY.ML Wed Feb 09 11:45:10 2000 +0100 @@ -306,17 +306,23 @@ (*** increasing ***) +Goalw [increasing_def] + "F : increasing f ==> F : stable {s. z <= f s}"; +by (Blast_tac 1); +qed "increasingD"; + Goalw [increasing_def, stable_def, constrains_def] "mono g ==> increasing f <= increasing (g o f)"; by Auto_tac; by (blast_tac (claset() addIs [monoD, order_trans]) 1); qed "mono_increasing_o"; +(*Holds by the theorem (Suc m <= n) = (m < n) *) Goalw [increasing_def] - "increasing f <= {F. ALL z::nat. F: stable {s. z < f s}}"; + "!!z::nat. F : increasing f ==> F: stable {s. z < f s}"; by (simp_tac (simpset() addsimps [Suc_le_eq RS sym]) 1); by (Blast_tac 1); -qed "increasing_stable_less"; +qed "strict_increasingD"; (** The Elimination Theorem. The "free" m has become universally quantified! diff -r d3eba67a9e67 -r e4b3192dfefa src/HOL/UNITY/Union.ML --- a/src/HOL/UNITY/Union.ML Wed Feb 09 11:43:53 2000 +0100 +++ b/src/HOL/UNITY/Union.ML Wed Feb 09 11:45:10 2000 +0100 @@ -250,6 +250,14 @@ Join_def])); qed "Join_transient"; +Goal "F : transient A ==> F Join G : transient A"; +by (asm_simp_tac (simpset() addsimps [Join_transient]) 1); +qed "Join_transient_I1"; + +Goal "G : transient A ==> F Join G : transient A"; +by (asm_simp_tac (simpset() addsimps [Join_transient]) 1); +qed "Join_transient_I2"; + Goal "i : I ==> \ \ (JN i:I. F i) : A ensures B = \ \ ((ALL i:I. F i : (A-B) co (A Un B)) & \ @@ -279,7 +287,13 @@ by (full_simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_eq_stable, Join_stable]) 1); by (force_tac(claset() addIs [stable_Int], simpset()) 1); -qed "stable_Join_Always"; +qed "stable_Join_Always1"; + +(*As above, but exchanging the roles of F and G*) +Goal "[| F : invariant A; G : stable A |] ==> F Join G : Always A"; +by (stac Join_commute 1); +by (blast_tac (claset() addIs [stable_Join_Always1]) 1); +qed "stable_Join_Always2"; Goal "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B"; by (asm_simp_tac (simpset() addsimps [Join_ensures]) 1);