# HG changeset patch # User paulson # Date 1056125596 -7200 # Node ID abcb32a7b212cdf4edc047c4118d056ac6483c95 # Parent c0c4af41fa3bb0c3a3d248c1674a65cf5aa45fd1 conversion of ClientImpl to Isar script diff -r c0c4af41fa3b -r abcb32a7b212 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Fri Jun 20 12:10:45 2003 +0200 +++ b/src/ZF/IsaMakefile Fri Jun 20 18:13:16 2003 +0200 @@ -121,7 +121,7 @@ UNITY/SubstAx.ML UNITY/SubstAx.thy UNITY/UNITY.ML UNITY/UNITY.thy \ UNITY/UNITYMisc.ML UNITY/UNITYMisc.thy UNITY/Union.ML UNITY/Union.thy \ UNITY/AllocBase.ML UNITY/AllocBase.thy UNITY/AllocImpl.thy\ - UNITY/ClientImpl.ML UNITY/ClientImpl.thy\ + UNITY/ClientImpl.thy\ UNITY/Distributor.ML UNITY/Distributor.thy\ UNITY/Follows.ML UNITY/Follows.thy\ UNITY/Increasing.ML UNITY/Increasing.thy\ diff -r c0c4af41fa3b -r abcb32a7b212 src/ZF/UNITY/AllocImpl.thy --- a/src/ZF/UNITY/AllocImpl.thy Fri Jun 20 12:10:45 2003 +0200 +++ b/src/ZF/UNITY/AllocImpl.thy Fri Jun 20 18:13:16 2003 +0200 @@ -9,15 +9,20 @@ (*LOCALE NEEDED FOR PROOF OF GUARANTEES THEOREM*) -theory AllocImpl = ClientImpl: +(*????FIXME: sort out this mess +FoldSet.cons_Int_right_lemma1: + ?x \ ?D \ cons(?x, ?C) \ ?D = cons(?x, ?C \ ?D) +FoldSet.cons_Int_right_lemma2: ?x \ ?D \ cons(?x, ?C) \ ?D = ?C \ ?D +Multiset.cons_Int_right_cases: + cons(?x, ?A) \ ?B = (if ?x \ ?B then cons(?x, ?A \ ?B) else ?A \ ?B) +UNITYMisc.Int_cons_right: + ?A \ cons(?a, ?B) = (if ?a \ ?A then cons(?a, ?A \ ?B) else ?A \ ?B) +UNITYMisc.Int_succ_right: + ?A \ succ(?k) = (if ?k \ ?A then cons(?k, ?A \ ?k) else ?A \ ?k) +*) -(*????MOVE UP*) -method_setup constrains = {* - Method.ctxt_args (fn ctxt => - Method.METHOD (fn facts => - gen_constrains_tac (Classical.get_local_claset ctxt, - Simplifier.get_local_simpset ctxt) 1)) *} - "for proving safety properties" + +theory AllocImpl = ClientImpl: consts @@ -62,21 +67,6 @@ preserves(lift(giv)). Acts(G))" - - -(*????FIXME: sort out this mess -FoldSet.cons_Int_right_lemma1: - ?x \ ?D \ cons(?x, ?C) \ ?D = cons(?x, ?C \ ?D) -FoldSet.cons_Int_right_lemma2: ?x \ ?D \ cons(?x, ?C) \ ?D = ?C \ ?D -Multiset.cons_Int_right_cases: - cons(?x, ?A) \ ?B = (if ?x \ ?B then cons(?x, ?A \ ?B) else ?A \ ?B) -UNITYMisc.Int_cons_right: - ?A \ cons(?a, ?B) = (if ?a \ ?A then cons(?a, ?A \ ?B) else ?A \ ?B) -UNITYMisc.Int_succ_right: - ?A \ succ(?k) = (if ?k \ ?A then cons(?k, ?A \ ?k) else ?A \ ?k) -*) - - declare alloc_type_assumes [simp] alloc_default_val_assumes [simp] lemma available_tok_value_type [simp,TC]: "s\state ==> s`available_tok \ nat" @@ -591,14 +581,6 @@ apply auto done -(*For using "disjunction" (union over an index set) to eliminate a variable. - ????move way up*) -lemma UN_conj_eq: "\s\state. f(s) \ A - ==> (\k\A. {s\state. P(s) & f(s) = k}) = {s\state. P(s)}" -apply blast -done - - (*Fifth step in proof of (31): from the fourth step, taking the union over all k\nat *) lemma alloc_prog_LeadsTo_length_giv_disj3: diff -r c0c4af41fa3b -r abcb32a7b212 src/ZF/UNITY/ClientImpl.ML --- a/src/ZF/UNITY/ClientImpl.ML Fri Jun 20 12:10:45 2003 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,309 +0,0 @@ -(* Title: ZF/UNITY/Client.ML - ID: $Id$ - Author: Sidi O Ehmety, Cambridge University Computer Laboratory - Copyright 2002 University of Cambridge - -Distributed Resource Management System: the Client -*) -Addsimps [type_assumes, default_val_assumes]; -(* This part should be automated *) - -Goalw [state_def] "s \\ state ==> s`ask \\ list(nat)"; -by (dres_inst_tac [("a", "ask")] apply_type 1); -by Auto_tac; -qed "ask_value_type"; -AddTCs [ask_value_type]; -Addsimps [ask_value_type]; - -Goalw [state_def] "s \\ state ==> s`giv \\ list(nat)"; -by (dres_inst_tac [("a", "giv")] apply_type 1); -by Auto_tac; -qed "giv_value_type"; -AddTCs [giv_value_type]; -Addsimps [giv_value_type]; - -Goalw [state_def] -"s \\ state ==> s`rel \\ list(nat)"; -by (dres_inst_tac [("a", "rel")] apply_type 1); -by Auto_tac; -qed "rel_value_type"; -AddTCs [rel_value_type]; -Addsimps [rel_value_type]; - -Goalw [state_def] "s \\ state ==> s`tok \\ nat"; -by (dres_inst_tac [("a", "tok")] apply_type 1); -by Auto_tac; -qed "tok_value_type"; -AddTCs [tok_value_type]; -Addsimps [tok_value_type]; - -(** The Client Program **) - -Goalw [client_prog_def] "client_prog \\ program"; -by (Simp_tac 1); -qed "client_type"; -Addsimps [client_type]; -AddTCs [client_type]; - -Addsimps [client_prog_def RS def_prg_Init, - client_prog_def RS def_prg_AllowedActs]; -program_defs_ref := [client_prog_def]; - -Addsimps (map simp_of_act [client_rel_act_def, -client_tok_act_def, client_ask_act_def]); - -Goal "\\G \\ program. (client_prog ok G) <-> \ -\ (G \\ preserves(lift(rel)) & G \\ preserves(lift(ask)) & \ -\ G \\ preserves(lift(tok)) & client_prog \\ Allowed(G))"; -by (auto_tac (claset(), - simpset() addsimps [ok_iff_Allowed, client_prog_def RS def_prg_Allowed])); -qed "client_prog_ok_iff"; - -Goal "client_prog:(\\x \\ var-{ask, rel, tok}. preserves(lift(x)))"; -by (rtac Inter_var_DiffI 1); -by (rtac ballI 2); -by (rtac preservesI 2); -by (constrains_tac 2); -by Auto_tac; -qed "client_prog_preserves"; - - -(*Safety property 1: ask, rel are increasing : (24) *) -Goalw [guar_def] -"client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))"; -by (auto_tac (claset() addSIs [increasing_imp_Increasing], - simpset() addsimps [client_prog_ok_iff, increasing_def])); -by (ALLGOALS(constrains_tac)); -by (ALLGOALS(thin_tac "mk_program(?u, ?v, ?w):Allowed(?x)")); -by (auto_tac (claset() addDs [ActsD], simpset())); -by (dres_inst_tac [("f", "lift(rel)")] preserves_imp_eq 2); -by (dres_inst_tac [("f", "lift(ask)")] preserves_imp_eq 1); -by (TRYALL(assume_tac)); -by (ALLGOALS(dtac ActsD)); -by (TRYALL(assume_tac)); -by (ALLGOALS(Clarify_tac)); -by (ALLGOALS(rotate_tac ~2)); -by Auto_tac; -qed "client_prog_Increasing_ask_rel"; - -Addsimps [nth_append, append_one_prefix]; - -Goal "0 program |]\ -\ ==> client_prog Join G : \ -\ Always({s \\ state. s`tok le NbT} Int \ -\ {s \\ state. \\elt \\ set_of_list(s`ask). elt le NbT})"; -by (rotate_tac ~1 1); -by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff])); -by (rtac (invariantI RS stable_Join_Always2) 1); -by (ALLGOALS(Clarify_tac)); -by (ALLGOALS(Asm_full_simp_tac)); -by (rtac stable_Int 2); -by (dres_inst_tac [("f", "lift(ask)")] preserves_imp_stable 3); -by (dres_inst_tac [("f", "lift(tok)")] preserves_imp_stable 2); -by (REPEAT(Force_tac 2)); -by (constrains_tac 1); -by (auto_tac (claset() addDs [ActsD], simpset())); -by (cut_facts_tac [NbT_pos] 1); -by (resolve_tac [NbT_pos2 RS mod_less_divisor] 1); -by (auto_tac (claset() addDs [ActsD, preserves_imp_eq], - simpset() addsimps [set_of_list_append])); -qed "ask_Bounded_lemma"; - -(* Export version, with no mention of tok in the postcondition, but - unfortunately tok must be declared local.*) -Goal -"client_prog \\ program guarantees \ -\ Always({s \\ state. \\elt \\ set_of_list(s`ask). elt le NbT})"; -by (rtac guaranteesI 1); -by (etac (ask_Bounded_lemma RS Always_weaken) 1); -by Auto_tac; -qed "client_prog_ask_Bounded"; - -(*** Towards proving the liveness property ***) - -Goal -"client_prog \\ stable({s \\ state. :prefix(nat)})"; -by (constrains_tac 1); -by Auto_tac; -qed "client_prog_stable_rel_le_giv"; - -Goal -"[| client_prog Join G \\ Incr(lift(giv)); G \\ preserves(lift(rel)) |] \ -\ ==> client_prog Join G \\ Stable({s \\ state. :prefix(nat)})"; -by (rtac (client_prog_stable_rel_le_giv RS Increasing_preserves_Stable) 1); -by (auto_tac (claset(), simpset() addsimps [lift_def])); -qed "client_prog_Join_Stable_rel_le_giv"; - -Goal "[| client_prog Join G \\ Incr(lift(giv)); G \\ preserves(lift(rel)) |] \ -\ ==> client_prog Join G \\ Always({s \\ state. :prefix(nat)})"; -by (force_tac (claset() addSIs [AlwaysI, client_prog_Join_Stable_rel_le_giv], - simpset()) 1); -qed "client_prog_Join_Always_rel_le_giv"; - -Goal "xs \\ list(A) ==> xs@[a]=xs --> False"; -by (etac list.induct 1); -by Auto_tac; -qed "list_app_lemma"; - -Goal "A == {:state*state. P(s, t)} ==> A={:state*state. P(s, t)}"; -by Auto_tac; -qed "def_act_eq"; - -Goal "A={:state*state. P(s, t)} ==> A<=state*state"; -by Auto_tac; -qed "act_subset"; - -Goal -"client_prog \\ \ -\ transient({s \\ state. s`rel = k & :strict_prefix(nat) \ -\ & :prefix(nat) & h pfixGe s`ask})"; -by (res_inst_tac [("act", "client_rel_act")] transientI 1); -by (simp_tac (simpset() addsimps - [client_prog_def RS def_prg_Acts]) 1); -by (simp_tac (simpset() addsimps - [client_rel_act_def RS def_act_eq RS act_subset]) 1); -by (auto_tac (claset(), - simpset() addsimps [client_prog_def RS def_prg_Acts,domain_def])); -by (resolve_tac [ReplaceI] 1); -by (res_inst_tac [("x", "x(rel:= x`rel @\ - \ [nth(length(x`rel), x`giv)])")] exI 1); -by (auto_tac (claset() addSIs [state_update_type, - app_type, length_type, nth_type], - simpset())); -by Auto_tac; -by (blast_tac (claset() addIs [lt_trans2, prefix_length_le, - strict_prefix_length_lt]) 1); -by (blast_tac (claset() addIs [lt_trans2, prefix_length_le, - strict_prefix_length_lt]) 1); -by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1); -by (ALLGOALS(subgoal_tac "h \\ list(nat)")); -by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1]))); -by (auto_tac (claset(), - simpset() addsimps [prefix_def, Ge_def])); -by (dtac strict_prefix_length_lt 1); -by (dres_inst_tac [("x", "length(x`rel)")] spec 1); -by Auto_tac; -by (full_simp_tac (simpset() addsimps [gen_prefix_iff_nth]) 1); -by (auto_tac (claset(), simpset() addsimps [id_def, lam_def])); -qed "transient_lemma"; - -Goalw [strict_prefix_def,id_def, lam_def] -":strict_prefix(A) <-> :prefix(A) & xs~=ys"; -by (auto_tac (claset() addDs [prefix_type RS subsetD], simpset())); -qed "strict_prefix_is_prefix"; - -Goal -"[| client_prog Join G \\ Incr(lift(giv)); client_prog ok G; G \\ program |] \ -\ ==> client_prog Join G \\ \ -\ {s \\ state. s`rel = k & :strict_prefix(nat) \ -\ & :prefix(nat) & h pfixGe s`ask} \ -\ LeadsTo {s \\ state. :strict_prefix(nat) \ -\ & :prefix(nat) & \ -\ :prefix(nat) & \ -\ h pfixGe s`ask}"; -by (rtac single_LeadsTo_I 1); -by (Asm_simp_tac 2); -by (ftac (client_prog_Increasing_ask_rel RS guaranteesD) 1); -by (rotate_tac 2 3); -by (auto_tac (claset(), simpset() addsimps [client_prog_ok_iff])); -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", "lift(giv)"), ("a", "s`giv")] Increasing_imp_Stable 1); -by (Asm_simp_tac 1); -by (eres_inst_tac [("f", "lift(ask)"), ("a", "s`ask")] Increasing_imp_Stable 1); -by (Asm_simp_tac 1); -by (eres_inst_tac [("f", "lift(rel)"), ("a", "s`rel")] Increasing_imp_Stable 1); -by (Asm_simp_tac 1); -by (etac client_prog_Join_Stable_rel_le_giv 1); -by (Blast_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 2); -by (blast_tac (claset() addIs [sym, strict_prefix_is_prefix RS iffD2, - prefix_trans, prefix_imp_pfixGe, - pfixGe_trans]) 2); -by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD1 RS conjunct1, - prefix_trans], simpset())); -qed "induct_lemma"; - -Goal -"[| client_prog Join G \\ Incr(lift(giv)); client_prog ok G; G \\ program |] \ -\ ==> client_prog Join G \\ \ -\ {s \\ state. :strict_prefix(nat) \ -\ & :prefix(nat) & h pfixGe s`ask} \ -\ LeadsTo {s \\ state. :prefix(nat)}"; -by (res_inst_tac [("f", "\\x \\ state. length(h) #- length(x`rel)")] - 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 (resolve_tac [imageI] 3); -by (resolve_tac [converseI] 3); -by (asm_simp_tac (simpset() addsimps [lam_def]) 3); -by (asm_simp_tac (simpset() addsimps [length_type]) 3); -by (etac swap 2); -by (resolve_tac [imageI] 2); -by (resolve_tac [converseI] 2); -by (asm_full_simp_tac (simpset() addsimps [lam_def]) 2); -by (REPEAT (dtac strict_prefix_length_lt 2)); -by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 2); -by (ALLGOALS(subgoal_tac "h \\ list(nat)")); -by (ALLGOALS(asm_simp_tac (simpset() addsimps [prefix_type RS subsetD RS SigmaD1]))); -by (dtac less_imp_succ_add 2); -by (dtac less_imp_succ_add 3); -by (ALLGOALS(Clarify_tac)); -by (ALLGOALS(Asm_simp_tac)); -by (etac (diff_le_self RS ltD) 2); -by (asm_full_simp_tac (simpset() addsimps [length_type, lam_def]) 1); -by (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD2] - addDs [rotate_prems 2 common_prefix_linear, - prefix_type RS subsetD], simpset())); -qed "rel_progress_lemma"; - -Goal -"[| client_prog Join G \\ Incr(lift(giv)); client_prog ok G; G \\ program |] ==> \ -\ client_prog Join G \\ \ -\ {s \\ state. :prefix(nat) & h pfixGe s`ask} \ -\ LeadsTo {s \\ state. :prefix(nat)}"; -by (rtac (client_prog_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 (auto_tac (claset() addIs [strict_prefix_is_prefix RS iffD2] - addDs [rotate_prems 3 common_prefix_linear, - prefix_type RS subsetD], simpset())); -by (rotate_tac ~1 1); -by (force_tac (claset(), simpset() addsimps [client_prog_ok_iff]) 1); -qed "progress_lemma"; - -(*Progress property: all tokens that are given will be released*) -Goal -"client_prog \\ Incr(lift(giv)) guarantees \ -\ (\\h \\ list(nat). {s \\ state. :prefix(nat) &\ -\ h pfixGe s`ask} LeadsTo {s \\ state. :prefix(nat)})"; -by (rtac guaranteesI 1); -by (Clarify_tac 1); -by (blast_tac (claset() addIs [progress_lemma]) 1); -by Auto_tac; -qed "client_prog_progress"; - -Goal "Allowed(client_prog) = \ -\ preserves(lift(rel)) Int preserves(lift(ask)) Int preserves(lift(tok))"; -by (cut_facts_tac [inst "v" "lift(ask)" preserves_type] 1); -by (auto_tac (claset(), - simpset() addsimps [Allowed_def, - client_prog_def RS def_prg_Allowed, - cons_Int_distrib, safety_prop_Acts_iff])); -qed "client_prog_Allowed"; - diff -r c0c4af41fa3b -r abcb32a7b212 src/ZF/UNITY/ClientImpl.thy --- a/src/ZF/UNITY/ClientImpl.thy Fri Jun 20 12:10:45 2003 +0200 +++ b/src/ZF/UNITY/ClientImpl.thy Fri Jun 20 18:13:16 2003 +0200 @@ -7,7 +7,7 @@ *) -ClientImpl = AllocBase + Guar + +theory ClientImpl = AllocBase + Guar: consts ask :: i (* input history: tokens requested *) giv :: i (* output history: tokens granted *) @@ -20,11 +20,11 @@ "rel" == "Var([1])" "tok" == "Var([2])" -rules - type_assumes +axioms + type_assumes: "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) & type_of(rel) = list(tokbag) & type_of(tok) = nat" - default_val_assumes + default_val_assumes: "default_val(ask) = Nil & default_val(giv) = Nil & default_val(rel) = Nil & default_val(tok) = 0" @@ -36,29 +36,299 @@ client_rel_act ::i "client_rel_act == - { \\ state*state. - \\nrel \\ nat. nrel = length(s`rel) & + { \ state*state. + \nrel \ nat. nrel = length(s`rel) & t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) & nrel < length(s`giv) & - nth(nrel, s`ask) le nth(nrel, s`giv)}" + nth(nrel, s`ask) \ nth(nrel, s`giv)}" (** Choose a new token requirement **) (** Including t=s suppresses fairness, allowing the non-trivial part of the action to be ignored **) client_tok_act :: i - "client_tok_act == { \\ state*state. t=s | + "client_tok_act == { \ state*state. t=s | t = s(tok:=succ(s`tok mod NbT))}" client_ask_act :: i - "client_ask_act == { \\ state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}" + "client_ask_act == { \ state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}" client_prog :: i "client_prog == - mk_program({s \\ state. s`tok le NbT & s`giv = Nil & + mk_program({s \ state. s`tok \ NbT & s`giv = Nil & s`ask = Nil & s`rel = Nil}, {client_rel_act, client_tok_act, client_ask_act}, - \\G \\ preserves(lift(rel)) Int + \G \ preserves(lift(rel)) Int preserves(lift(ask)) Int preserves(lift(tok)). Acts(G))" + + +declare type_assumes [simp] default_val_assumes [simp] +(* This part should be automated *) + +(*????MOVE UP*) +method_setup constrains = {* + Method.ctxt_args (fn ctxt => + Method.METHOD (fn facts => + gen_constrains_tac (Classical.get_local_claset ctxt, + Simplifier.get_local_simpset ctxt) 1)) *} + "for proving safety properties" + +(*For using "disjunction" (union over an index set) to eliminate a variable. + ????move way up*) +lemma UN_conj_eq: "\s\state. f(s) \ A + ==> (\k\A. {s\state. P(s) & f(s) = k}) = {s\state. P(s)}" +by blast + +lemma ask_value_type [simp,TC]: "s \ state ==> s`ask \ list(nat)" +apply (unfold state_def) +apply (drule_tac a = ask in apply_type, auto) +done + +lemma giv_value_type [simp,TC]: "s \ state ==> s`giv \ list(nat)" +apply (unfold state_def) +apply (drule_tac a = giv in apply_type, auto) +done + +lemma rel_value_type [simp,TC]: "s \ state ==> s`rel \ list(nat)" +apply (unfold state_def) +apply (drule_tac a = rel in apply_type, auto) +done + +lemma tok_value_type [simp,TC]: "s \ state ==> s`tok \ nat" +apply (unfold state_def) +apply (drule_tac a = tok in apply_type, auto) +done + +(** The Client Program **) + +lemma client_type [simp,TC]: "client_prog \ program" +apply (unfold client_prog_def) +apply (simp (no_asm)) +done + +declare client_prog_def [THEN def_prg_Init, simp] +declare client_prog_def [THEN def_prg_AllowedActs, simp] +ML +{* +program_defs_ref := [thm"client_prog_def"] +*} + +declare client_rel_act_def [THEN def_act_simp, simp] +declare client_tok_act_def [THEN def_act_simp, simp] +declare client_ask_act_def [THEN def_act_simp, simp] + +lemma client_prog_ok_iff: + "\G \ program. (client_prog ok G) <-> + (G \ preserves(lift(rel)) & G \ preserves(lift(ask)) & + G \ preserves(lift(tok)) & client_prog \ Allowed(G))" +by (auto simp add: ok_iff_Allowed client_prog_def [THEN def_prg_Allowed]) + +lemma client_prog_preserves: + "client_prog:(\x \ var-{ask, rel, tok}. preserves(lift(x)))" +apply (rule Inter_var_DiffI, force) +apply (rule ballI) +apply (rule preservesI, constrains, auto) +done + + +lemma preserves_lift_imp_stable: + "G \ preserves(lift(ff)) ==> G \ stable({s \ state. P(s`ff)})"; +apply (drule preserves_imp_stable) +apply (simp add: lift_def) +done + +lemma preserves_imp_prefix: + "G \ preserves(lift(ff)) + ==> G \ stable({s \ state. \k, s`ff\ \ prefix(nat)})"; +by (erule preserves_lift_imp_stable) + +(*Safety property 1: ask, rel are increasing: (24) *) +lemma client_prog_Increasing_ask_rel: +"client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))" +apply (unfold guar_def) +apply (auto intro!: increasing_imp_Increasing + simp add: client_prog_ok_iff increasing_def preserves_imp_prefix) +apply (constrains, force, force)+ +done + +declare nth_append [simp] append_one_prefix [simp] + +lemma NbT_pos2: "0 program |] + ==> client_prog Join G \ + Always({s \ state. s`tok \ NbT} Int + {s \ state. \elt \ set_of_list(s`ask). elt \ NbT})" +apply (rotate_tac -1) +apply (auto simp add: client_prog_ok_iff) +apply (rule invariantI [THEN stable_Join_Always2], force) + prefer 2 + apply (fast intro: stable_Int preserves_lift_imp_stable, constrains) +apply (auto dest: ActsD) +apply (cut_tac NbT_pos) +apply (rule NbT_pos2 [THEN mod_less_divisor]) +apply (auto dest: ActsD preserves_imp_eq simp add: set_of_list_append) +done + +(* Export version, with no mention of tok in the postcondition, but + unfortunately tok must be declared local.*) +lemma client_prog_ask_Bounded: + "client_prog \ program guarantees + Always({s \ state. \elt \ set_of_list(s`ask). elt \ NbT})" +apply (rule guaranteesI) +apply (erule ask_Bounded_lemma [THEN Always_weaken], auto) +done + +(*** Towards proving the liveness property ***) + +lemma client_prog_stable_rel_le_giv: + "client_prog \ stable({s \ state. \ prefix(nat)})" +by (constrains, auto) + +lemma client_prog_Join_Stable_rel_le_giv: +"[| client_prog Join G \ Incr(lift(giv)); G \ preserves(lift(rel)) |] + ==> client_prog Join G \ Stable({s \ state. \ prefix(nat)})" +apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable]) +apply (auto simp add: lift_def) +done + +lemma client_prog_Join_Always_rel_le_giv: + "[| client_prog Join G \ Incr(lift(giv)); G \ preserves(lift(rel)) |] + ==> client_prog Join G \ Always({s \ state. \ prefix(nat)})" +by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv) + +lemma def_act_eq: + "A == { \ state*state. P(s, t)} ==> A={ \ state*state. P(s, t)}" +by auto + +lemma act_subset: "A={ \ state*state. P(s, t)} ==> A<=state*state" +by auto + +lemma transient_lemma: +"client_prog \ + transient({s \ state. s`rel = k & \ strict_prefix(nat) + & \ prefix(nat) & h pfixGe s`ask})" +apply (rule_tac act = client_rel_act in transientI) +apply (simp (no_asm) add: client_prog_def [THEN def_prg_Acts]) +apply (simp (no_asm) add: client_rel_act_def [THEN def_act_eq, THEN act_subset]) +apply (auto simp add: client_prog_def [THEN def_prg_Acts] domain_def) +apply (rule ReplaceI) +apply (rule_tac x = "x (rel:= x`rel @ [nth (length (x`rel), x`giv) ]) " in exI) +apply (auto intro!: state_update_type app_type length_type nth_type, auto) +apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt) +apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt) +apply (simp (no_asm_use) add: gen_prefix_iff_nth) +apply (subgoal_tac "h \ list(nat)") + apply (simp_all (no_asm_simp) add: prefix_type [THEN subsetD, THEN SigmaD1]) +apply (auto simp add: prefix_def Ge_def) +apply (drule strict_prefix_length_lt) +apply (drule_tac x = "length (x`rel) " in spec) +apply auto +apply (simp (no_asm_use) add: gen_prefix_iff_nth) +apply (auto simp add: id_def lam_def) +done + +lemma strict_prefix_is_prefix: + " \ strict_prefix(A) <-> \ prefix(A) & xs\ys" +apply (unfold strict_prefix_def id_def lam_def) +apply (auto dest: prefix_type [THEN subsetD]) +done + +lemma induct_lemma: +"[| client_prog Join G \ Incr(lift(giv)); client_prog ok G; G \ program |] + ==> client_prog Join G \ + {s \ state. s`rel = k & \ strict_prefix(nat) + & \ prefix(nat) & h pfixGe s`ask} + LeadsTo {s \ state. \ strict_prefix(nat) + & \ prefix(nat) & + \ prefix(nat) & + h pfixGe s`ask}" +apply (rule single_LeadsTo_I) + prefer 2 apply simp +apply (frule client_prog_Increasing_ask_rel [THEN guaranteesD]) +apply (rotate_tac [3] 2) +apply (auto simp add: client_prog_ok_iff) +apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken]) +apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int]) +apply (erule_tac f = "lift (giv) " and a = "s`giv" in Increasing_imp_Stable) +apply (simp (no_asm_simp)) +apply (erule_tac f = "lift (ask) " and a = "s`ask" in Increasing_imp_Stable) +apply (simp (no_asm_simp)) +apply (erule_tac f = "lift (rel) " and a = "s`rel" in Increasing_imp_Stable) +apply (simp (no_asm_simp)) +apply (erule client_prog_Join_Stable_rel_le_giv, blast, simp_all) + prefer 2 + apply (blast intro: sym strict_prefix_is_prefix [THEN iffD2] prefix_trans prefix_imp_pfixGe pfixGe_trans) +apply (auto intro: strict_prefix_is_prefix [THEN iffD1, THEN conjunct1] + prefix_trans) +done + +lemma rel_progress_lemma: +"[| client_prog Join G \ Incr(lift(giv)); client_prog ok G; G \ program |] + ==> client_prog Join G \ + {s \ state. \ strict_prefix(nat) + & \ prefix(nat) & h pfixGe s`ask} + LeadsTo {s \ state. \ prefix(nat)}" +apply (rule_tac f = "\x \ state. length(h) #- length(x`rel)" + in LessThan_induct) +apply (auto simp add: vimage_def) + prefer 2 apply (force simp add: lam_def) +apply (rule single_LeadsTo_I) + prefer 2 apply simp +apply (subgoal_tac "h \ list(nat)") + prefer 2 apply (blast dest: prefix_type [THEN subsetD]) +apply (rule induct_lemma [THEN LeadsTo_weaken]) + apply (simp add: length_type lam_def) +apply (auto intro: strict_prefix_is_prefix [THEN iffD2] + dest: common_prefix_linear prefix_type [THEN subsetD]) +apply (erule swap) +apply (rule imageI) + apply (force dest!: simp add: lam_def) +apply (simp add: length_type lam_def, clarify) +apply (drule strict_prefix_length_lt)+ +apply (drule less_imp_succ_add, simp)+ +apply clarify +apply simp +apply (erule diff_le_self [THEN ltD]) +done + +lemma progress_lemma: +"[| client_prog Join G \ Incr(lift(giv)); client_prog ok G; G \ program |] + ==> client_prog Join G \ + {s \ state. \ prefix(nat) & h pfixGe s`ask} + LeadsTo {s \ state. \ prefix(nat)}" +apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI], assumption) +apply (force simp add: client_prog_ok_iff) +apply (rule LeadsTo_weaken_L) +apply (rule LeadsTo_Un [OF rel_progress_lemma + subset_refl [THEN subset_imp_LeadsTo]]) +apply (auto intro: strict_prefix_is_prefix [THEN iffD2] + dest: common_prefix_linear prefix_type [THEN subsetD]) +done + +(*Progress property: all tokens that are given will be released*) +lemma client_prog_progress: +"client_prog \ Incr(lift(giv)) guarantees + (\h \ list(nat). {s \ state. \ prefix(nat) & + h pfixGe s`ask} LeadsTo {s \ state. \ prefix(nat)})" +apply (rule guaranteesI) +apply (blast intro: progress_lemma, auto) +done + +lemma client_prog_Allowed: + "Allowed(client_prog) = + preserves(lift(rel)) Int preserves(lift(ask)) Int preserves(lift(tok))" +apply (cut_tac v = "lift (ask)" in preserves_type) +apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed] + cons_Int_distrib safety_prop_Acts_iff) +done + end \ No newline at end of file diff -r c0c4af41fa3b -r abcb32a7b212 src/ZF/UNITY/GenPrefix.ML --- a/src/ZF/UNITY/GenPrefix.ML Fri Jun 20 12:10:45 2003 +0200 +++ b/src/ZF/UNITY/GenPrefix.ML Fri Jun 20 18:13:16 2003 +0200 @@ -523,7 +523,13 @@ \ --> \\ prefix(A) | \\ prefix(A)"; by (etac list_append_induct 1); by Auto_tac; -qed_spec_mp "common_prefix_linear"; +qed_spec_mp "common_prefix_linear_lemma"; + +Goal "[| \\ prefix(A); \\ prefix(A) |] \ +\ ==> \\ prefix(A) | \\ prefix(A)"; +by (cut_facts_tac [prefix_type] 1); +by (blast_tac (claset() delrules [disjCI] addIs [common_prefix_linear_lemma]) 1); +qed "common_prefix_linear"; (*** pfixLe, pfixGe: properties inherited from the translations ***)