# HG changeset patch # User paulson # Date 1165598548 -3600 # Node ID 4e4b7c801142911e6e7a27a939a4d11de1b45679 # Parent 9cfd9eb9faec5fcf2d8eccbf4bb9d801629a7572 patched up the proofs agsin diff -r 9cfd9eb9faec -r 4e4b7c801142 src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Fri Dec 08 13:40:26 2006 +0100 +++ b/src/HOL/UNITY/Comp/Alloc.thy Fri Dec 08 18:22:28 2006 +0100 @@ -1,5 +1,4 @@ -(* Title: HOL/UNITY/Alloc - ID: $Id$ +(* ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge @@ -7,90 +6,90 @@ *) theory Alloc -imports AllocBase PPROD +imports AllocBase "../PPROD" begin -(** State definitions. OUTPUT variables are locals **) +subsection{*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*) + 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*) + 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*) + --{*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*) + --{*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*) + 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*) + 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*) + client :: "nat => clientState" --{*states of all clients*} + dummy :: 'a --{*dummy field for new variables*} constdefs -(** Resource allocation system specification **) +--{** Resource allocation system specification **} - (*spec (1)*) + --{*spec (1)*} system_safety :: "'a systemState program set" "system_safety == Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s) - <= NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}" + \ NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}" - (*spec (2)*) + --{*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 \ (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) ***) +--{** Client specification (required) ***} - (*spec (3)*) + --{*spec (3)*} client_increasing :: "'a clientState_d program set" "client_increasing == UNIV guarantees Increasing ask Int Increasing rel" - (*spec (4)*) + --{*spec (4)*} client_bounded :: "'a clientState_d program set" "client_bounded == - UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}" + UNIV guarantees Always {s. ALL elt : set (ask s). elt \ NbT}" - (*spec (5)*) + --{*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})" + (INT h. {s. h \ giv s & h pfixGe ask s} + LeadsTo {s. tokens h \ (tokens o rel) s})" - (*spec: preserves part*) + --{*spec: preserves part*} client_preserves :: "'a clientState_d program set" "client_preserves == preserves giv Int preserves clientState_d.dummy" - (*environmental constraints*) + --{*environmental constraints*} client_allowed_acts :: "'a clientState_d program set" "client_allowed_acts == {F. AllowedActs F = @@ -100,54 +99,54 @@ "client_spec == client_increasing Int client_bounded Int client_progress Int client_allowed_acts Int client_preserves" -(** Allocator specification (required) ***) +--{** Allocator specification (required) **} - (*spec (6)*) + --{*spec (6)*} alloc_increasing :: "'a allocState_d program set" "alloc_increasing == UNIV guarantees (INT i : lessThan Nclients. Increasing (sub i o allocGiv))" - (*spec (7)*) + --{*spec (7)*} alloc_safety :: "'a allocState_d program set" "alloc_safety == (INT i : lessThan Nclients. Increasing (sub i o allocRel)) guarantees Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s) - <= NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}" + \ NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}" - (*spec (8)*) + --{*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 NbT} Int (INT i : lessThan Nclients. - INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} + 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}) + {s. tokens h \ (tokens o sub i o allocRel)s}) guarantees (INT i : lessThan Nclients. - INT h. {s. h <= (sub i o allocAsk) s} + 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} + 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}) + {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*) + --{*spec: preserves part*} alloc_preserves :: "'a allocState_d program set" "alloc_preserves == preserves allocRel Int preserves allocAsk Int preserves allocState_d.dummy" - (*environmental constraints*) + --{*environmental constraints*} alloc_allowed_acts :: "'a allocState_d program set" "alloc_allowed_acts == {F. AllowedActs F = @@ -157,36 +156,36 @@ "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int alloc_allowed_acts Int alloc_preserves" -(** Network specification ***) +--{** Network specification **} - (*spec (9.1)*) + --{*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)*) + --{*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)*) + --{*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*) + --{*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*) + --{*environmental constraints*} network_allowed_acts :: "'a systemState program set" "network_allowed_acts == {F. AllowedActs F = @@ -201,7 +200,7 @@ network_preserves" -(** State mappings **) +--{** State mappings **} sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState" "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s in (| allocGiv = allocGiv s, @@ -331,7 +330,7 @@ apply (tactic record_auto_tac) done -(*We need the inverse; also having it simplifies the proof of surjectivity*) +text{*We need the inverse; also having it simplifies the proof of surjectivity*} lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s = (| allocGiv = allocGiv s, allocAsk = allocAsk s, @@ -351,7 +350,7 @@ done -(*** bijectivity of sysOfClient ***) +subsubsection{*bijectivity of @{term sysOfClient}*} lemma inj_sysOfClient [iff]: "inj sysOfClient" apply (unfold sysOfClient_def) @@ -379,7 +378,7 @@ done -(*** bijectivity of client_map ***) +subsubsection{*bijectivity of @{term client_map}*} lemma inj_client_map [iff]: "inj client_map" apply (unfold inj_on_def) @@ -403,7 +402,7 @@ done -(** o-simprules for client_map **) +text{*o-simprules for @{term client_map}*} lemma fst_o_client_map: "fst o client_map = non_dummy" apply (unfold client_map_def) @@ -421,7 +420,8 @@ ML {* bind_thms ("snd_o_client_map'", make_o_equivs (thm "snd_o_client_map")) *} declare snd_o_client_map' [simp] -(** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **) + +subsection{*o-simprules for @{term sysOfAlloc} [MUST BE AUTOMATED]*} lemma client_o_sysOfAlloc: "client o sysOfAlloc = fst o allocState_d.dummy " apply (tactic record_auto_tac) @@ -451,7 +451,8 @@ ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_sysOfAlloc_eq")) *} declare allocRel_o_sysOfAlloc_eq' [simp] -(** o-simprules for sysOfClient [MUST BE AUTOMATED] **) + +subsection{* o-simprules for @{term sysOfClient} [MUST BE AUTOMATED]*} lemma client_o_sysOfClient: "client o sysOfClient = fst" apply (tactic record_auto_tac) @@ -532,7 +533,7 @@ declare finite_lessThan [iff] -(*Client : *) +text{*Client : *} lemmas client_spec_simps = client_spec_def client_increasing_def client_bounded_def client_progress_def client_allowed_acts_def client_preserves_def @@ -562,7 +563,7 @@ Client_preserves_dummy [iff] -(*Network : *) +text{*Network : *} lemmas network_spec_simps = network_spec_def network_ask_def network_giv_def network_rel_def network_allowed_acts_def network_preserves_def @@ -594,7 +595,7 @@ Network_preserves_rel [simplified o_def, simp] Network_preserves_ask [simplified o_def, simp] -(*Alloc : *) +text{*Alloc : *} lemmas alloc_spec_simps = alloc_spec_def alloc_increasing_def alloc_safety_def alloc_progress_def alloc_allowed_acts_def alloc_preserves_def @@ -615,7 +616,7 @@ bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy); *} -(*Strip off the INT in the guarantees postcondition*) +text{*Strip off the INT in the guarantees postcondition*} ML {* bind_thm ("Alloc_Increasing", normalize Alloc_Increasing_0) @@ -627,50 +628,45 @@ Alloc_preserves_dummy [iff] -(** Components lemmas [MUST BE AUTOMATED] **) +subsection{*Components Lemmas [MUST BE AUTOMATED]*} lemma Network_component_System: "Network Join ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join rename sysOfAlloc Alloc) = System" - apply (simp add: System_def Join_ac) - done + by (simp add: System_def Join_ac) lemma Client_component_System: "(rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join (Network Join rename sysOfAlloc Alloc) = System" - apply (simp add: System_def Join_ac) - done + by (simp add: System_def Join_ac) lemma Alloc_component_System: "rename sysOfAlloc Alloc Join ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join Network) = System" - apply (simp add: System_def Join_ac) - done + by (simp add: System_def Join_ac) declare Client_component_System [iff] Network_component_System [iff] Alloc_component_System [iff] -(** These preservation laws should be generated automatically **) + +text{** These preservation laws should be generated automatically **} lemma Client_Allowed [simp]: "Allowed Client = preserves rel Int preserves ask" - apply (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff) - done + by (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff) lemma Network_Allowed [simp]: "Allowed Network = preserves allocRel Int (INT i: lessThan Nclients. preserves(giv o sub i o client))" - apply (auto simp add: Allowed_def Network_AllowedActs safety_prop_Acts_iff) - done + by (auto simp add: Allowed_def Network_AllowedActs safety_prop_Acts_iff) lemma Alloc_Allowed [simp]: "Allowed Alloc = preserves allocGiv" - apply (auto simp add: Allowed_def Alloc_AllowedActs safety_prop_Acts_iff) - done + by (auto simp add: Allowed_def Alloc_AllowedActs safety_prop_Acts_iff) -(*needed in rename_client_map_tac*) +text{*needed in @{text rename_client_map_tac}*} lemma OK_lift_rename_Client [simp]: "OK I (%i. lift i (rename client_map Client))" apply (rule OK_lift_I) apply auto @@ -679,6 +675,18 @@ apply (auto simp add: o_def split_def) done +lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x" +apply (insert fst_o_lift_map [of i]) +apply (drule fun_cong [where x=x]) +apply (simp add: o_def); +done + +lemma fst_o_lift_map' [simp]: + "(f \ sub i \ fst \ lift_map i \ g) = f o fst o g" +apply (subst fst_o_lift_map [symmetric]) +apply (simp only: o_assoc) +done + (*The proofs of rename_Client_Increasing, rename_Client_Bounded and rename_Client_Progress are similar. All require copying out the original @@ -717,14 +725,13 @@ (simpset() addsimps [thm "o_def", thm "non_dummy_def", thm "guarantees_Int_right"]) 1] *} -(*Lifting Client_Increasing to systemState*) +text{*Lifting @{text Client_Increasing} to @{term systemState}*} lemma rename_Client_Increasing: "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)" - apply (tactic rename_client_map_tac) - sorry + by (tactic rename_client_map_tac) lemma preserves_sub_fst_lift_map: "[| F : preserves w; i ~= j |] ==> F : preserves (sub i o fst o lift_map j o funPair v w)" @@ -735,38 +742,33 @@ lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |] ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)" - apply (case_tac "i=j") - apply (simp add: o_def non_dummy_def) - sorry -(* + apply (case_tac "i=j") + apply (simp, simp add: o_def non_dummy_def) apply (drule Client_preserves_dummy [THEN preserves_sub_fst_lift_map]) apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD]) apply (simp add: o_def client_map_def) done -*) lemma rename_sysOfClient_ok_Network: "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) ok Network" - apply (auto simp add: ok_iff_Allowed client_preserves_giv_oo_client_map) - done + by (auto simp add: ok_iff_Allowed client_preserves_giv_oo_client_map) lemma rename_sysOfClient_ok_Alloc: "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) ok rename sysOfAlloc Alloc" - apply (simp add: ok_iff_Allowed) - done + by (simp add: ok_iff_Allowed) lemma rename_sysOfAlloc_ok_Network: "rename sysOfAlloc Alloc ok Network" - apply (simp add: ok_iff_Allowed) - done + by (simp add: ok_iff_Allowed) declare rename_sysOfClient_ok_Network [iff] rename_sysOfClient_ok_Alloc [iff] rename_sysOfAlloc_ok_Network [iff] -(*The "ok" laws, re-oriented*) +text{*The "ok" laws, re-oriented. + But not sure this works: theorem @{text ok_commute} is needed below*} declare rename_sysOfClient_ok_Network [THEN ok_sym, iff] rename_sysOfClient_ok_Alloc [THEN ok_sym, iff] @@ -784,22 +786,21 @@ (*Lifting Alloc_Increasing up to the level of systemState*) -ML {* -bind_thm ("rename_Alloc_Increasing", - thm "Alloc_Increasing" RS thm "rename_guarantees_sysOfAlloc_I" - |> simplify (simpset() addsimps [thm "surj_rename" RS thm "surj_range", thm "o_def"])) -*} +lemmas rename_Alloc_Increasing = + Alloc_Increasing + [THEN rename_guarantees_sysOfAlloc_I, + simplified surj_rename [THEN surj_range] o_def sub_apply + rename_image_Increasing bij_sysOfAlloc + allocGiv_o_inv_sysOfAlloc_eq']; lemma System_Increasing_allocGiv: "i < Nclients ==> System : Increasing (sub i o allocGiv)" apply (unfold System_def) apply (simp add: o_def) - sorry -(* apply (rule rename_Alloc_Increasing [THEN guarantees_Join_I1, THEN guaranteesD]) apply auto done -*) + ML {* bind_thms ("System_Increasing'", list_of_Int (thm "System_Increasing")) @@ -807,109 +808,92 @@ declare System_Increasing' [intro!] -(** Follows consequences. +text{* Follows consequences. The "Always (INT ...) formulation expresses the general safety property - and allows it to be combined using Always_Int_rule below. **) + and allows it to be combined using @{text Always_Int_rule} below. *} lemma System_Follows_rel: "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))" apply (auto intro!: Network_Rel [THEN component_guaranteesD]) - sorry + apply (simp add: ok_commute [of Network]) + done lemma System_Follows_ask: "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))" - sorry -(* - apply (auto intro!: [Network_Ask [THEN component_guaranteesD]]) + apply (auto intro!: Network_Ask [THEN component_guaranteesD]) + apply (simp add: ok_commute [of Network]) done -*) lemma System_Follows_allocGiv: "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)" apply (auto intro!: Network_Giv [THEN component_guaranteesD] rename_Alloc_Increasing [THEN component_guaranteesD]) - apply (simp_all add: o_def non_dummy_def) - sorry -(* + apply (simp_all add: o_def non_dummy_def ok_commute [of Network]) apply (auto intro!: rename_Alloc_Increasing [THEN component_guaranteesD]) done -*) + lemma Always_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients. - {s. (giv o sub i o client) s <= (sub i o allocGiv) s})" + {s. (giv o sub i o client) s \ (sub i o allocGiv) s})" apply auto - sorry -(* apply (erule System_Follows_allocGiv [THEN Follows_Bounded]) done -*) + lemma Always_allocAsk_le_ask: "System : Always (INT i: lessThan Nclients. - {s. (sub i o allocAsk) s <= (ask o sub i o client) s})" + {s. (sub i o allocAsk) s \ (ask o sub i o client) s})" apply auto - sorry -(* apply (erule System_Follows_ask [THEN Follows_Bounded]) done -*) + lemma Always_allocRel_le_rel: "System : Always (INT i: lessThan Nclients. - {s. (sub i o allocRel) s <= (rel o sub i o client) s})" - sorry -(* - apply (auto intro!: Follows_Bounded System_Follows_rel) - done -*) + {s. (sub i o allocRel) s \ (rel o sub i o client) s})" + by (auto intro!: Follows_Bounded System_Follows_rel) + -(*** Proof of the safety property (1) ***) +subsection{*Proof of the safety property (1)*} -(*safety (1), step 1 is System_Follows_rel*) +text{*safety (1), step 1 is @{text System_Follows_rel}*} -(*safety (1), step 2*) +text{*safety (1), step 2*} (* i < Nclients ==> System : Increasing (sub i o allocRel) *) lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1, standard] (*Lifting Alloc_safety up to the level of systemState. - Simplififying with o_def gets rid of the translations but it unfortunately + Simplifying with o_def gets rid of the translations but it unfortunately gets rid of the other "o"s too.*) -ML {* - val rename_Alloc_Safety = - thm "Alloc_Safety" RS thm "rename_guarantees_sysOfAlloc_I" - |> simplify (simpset() addsimps [o_def]) -*} -(*safety (1), step 3*) -(* +text{*safety (1), step 3*} lemma System_sum_bounded: - "System : Always {s. (\i: lessThan Nclients. (tokens o sub i o allocGiv) s) - <= NbT + (\i: lessThan Nclients. (tokens o sub i o allocRel) s)}" + "System : Always {s. (\i \ lessThan Nclients. (tokens o sub i o allocGiv) s) + \ NbT + (\i \ lessThan Nclients. (tokens o sub i o allocRel) s)}" apply (simp add: o_apply) - apply (rule rename_Alloc_Safety [THEN component_guaranteesD]) - apply (auto simp add: o_simp System_Increasing_allocRel) + apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I]) + apply (simp add: o_def); + apply (erule component_guaranteesD) + apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def]) done -*) -(** Follows reasoning **) +text{* Follows reasoning*} lemma Always_tokens_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients. {s. (tokens o giv o sub i o client) s - <= (tokens o sub i o allocGiv) s})" + \ (tokens o sub i o allocGiv) s})" apply (rule Always_giv_le_allocGiv [THEN Always_weaken]) apply (auto intro: tokens_mono_prefix simp add: o_apply) done lemma Always_tokens_allocRel_le_rel: "System : Always (INT i: lessThan Nclients. {s. (tokens o sub i o allocRel) s - <= (tokens o rel o sub i o client) s})" + \ (tokens o rel o sub i o client) s})" apply (rule Always_allocRel_le_rel [THEN Always_weaken]) apply (auto intro: tokens_mono_prefix simp add: o_apply) done -(*safety (1), step 4 (final result!) *) -lemma System_safety: "System : system_safety" +text{*safety (1), step 4 (final result!) *} +theorem System_safety: "System : system_safety" apply (unfold system_safety_def) - sorry -(* apply (tactic {* rtac (Always_Int_rule [thm "System_sum_bounded", thm "Always_tokens_giv_le_allocGiv", thm "Always_tokens_allocRel_le_rel"] RS thm "Always_weaken") 1 *}) @@ -920,27 +904,27 @@ prefer 3 apply assumption apply auto done -*) -(*** Proof of the progress property (2) ***) +subsection {* Proof of the progress property (2) *} -(*progress (2), step 1 is System_Follows_ask and System_Follows_rel*) +text{*progress (2), step 1 is @{text System_Follows_ask} and + @{text System_Follows_rel}*} -(*progress (2), step 2; see also System_Increasing_allocRel*) +text{*progress (2), step 2; see also @{text System_Increasing_allocRel}*} (* i < Nclients ==> System : Increasing (sub i o allocAsk) *) lemmas System_Increasing_allocAsk = System_Follows_ask [THEN Follows_Increasing1, standard] -(*progress (2), step 3: lifting "Client_Bounded" to systemState*) +text{*progress (2), step 3: lifting @{text Client_Bounded} to systemState*} lemma rename_Client_Bounded: "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}" - apply (tactic rename_client_map_tac) - sorry + Always {s. ALL elt : set ((ask o sub i o client) s). elt \ NbT}" + by (tactic rename_client_map_tac) + lemma System_Bounded_ask: "i < Nclients ==> System : Always - {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}" + {s. ALL elt : set ((ask o sub i o client) s). elt \ NbT}" apply (rule component_guaranteesD [OF rename_Client_Bounded Client_component_System]) apply auto done @@ -949,18 +933,18 @@ apply blast done -(*progress (2), step 4*) +text{*progress (2), step 4*} lemma System_Bounded_allocAsk: "System : Always {s. ALL i NbT}" apply (auto simp add: Collect_all_imp_eq) apply (tactic {* rtac (Always_Int_rule [thm "Always_allocAsk_le_ask", thm "System_Bounded_ask"] RS thm "Always_weaken") 1 *}) apply (auto dest: set_mono) done -(*progress (2), step 5 is System_Increasing_allocGiv*) +text{*progress (2), step 5 is @{text System_Increasing_allocGiv}*} -(*progress (2), step 6*) +text{*progress (2), step 6*} (* i < Nclients ==> System : Increasing (giv o sub i o client) *) lemmas System_Increasing_giv = System_Follows_allocGiv [THEN Follows_Increasing1, standard] @@ -969,23 +953,20 @@ ==> 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 & + (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})" + LeadsTo {s. tokens h \ (tokens o rel o sub i o client) s})" apply (tactic rename_client_map_tac) - sorry -(* apply (simp add: Client_Progress [simplified o_def]) done -*) -(*progress (2), step 7*) +text{*progress (2), step 7*} lemma System_Client_Progress: "System : (INT i : (lessThan Nclients). - INT h. {s. h <= (giv o sub i o client) s & + 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})" + LeadsTo {s. tokens h \ (tokens o rel o sub i o client) s})" apply (rule INT_I) (*Couldn't have just used Auto_tac since the "INT h" must be kept*) apply (rule component_guaranteesD [OF rename_Client_Progress Client_component_System]) @@ -993,44 +974,39 @@ done (*Concludes - System : {s. k <= (sub i o allocGiv) s} + 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} *) -(* -bind_thm ("lemma", - [thm "System_Follows_ask" RS thm "Follows_Bounded", - thm "System_Follows_allocGiv" RS thm "Follows_LeadsTo"] MRS thm "Always_LeadsToD"); -*) + {s. (sub i o allocAsk) s \ (ask o sub i o client) s} Int + {s. k \ (giv o sub i o client) s} *) -(*A more complicated variant of the previous one*) -(* -val lemma2 = [lemma, - System_Follows_ask RS Follows_Increasing1 RS IncreasingD] - MRS PSP_Stable; -*) +lemmas System_lemma1 = + Always_LeadsToD [OF System_Follows_ask [THEN Follows_Bounded] + System_Follows_allocGiv [THEN Follows_LeadsTo]] -lemma lemma3: "i < Nclients - ==> System : {s. h <= (sub i o allocGiv) s & +lemmas System_lemma2 = + PSP_Stable [OF System_lemma1 + System_Follows_ask [THEN Follows_Increasing1, THEN IncreasingD]] + + +lemma System_lemma3: "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 & + {s. h \ (giv o sub i o client) s & h pfixGe (ask o sub i o client) s}" apply (rule single_LeadsTo_I) - sorry -(* - apply (rule_tac k6 = "h" and x2 = " (sub i o allocAsk) s" in lemma2 [THEN LeadsTo_weaken]) + apply (rule_tac k6 = "h" and x2 = " (sub i o allocAsk) s" + in System_lemma2 [THEN LeadsTo_weaken]) apply auto - apply (blast intro: trans_Ge [THEN trans_genPrefix THEN transD] prefix_imp_pfixGe) + apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] prefix_imp_pfixGe) done -*) -(*progress (2), step 8: Client i's "release" action is visible system-wide*) +text{*progress (2), step 8: Client i's "release" action is visible system-wide*} lemma System_Alloc_Client_Progress: "i < Nclients - ==> System : {s. h <= (sub i o allocGiv) s & + ==> 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}" + LeadsTo {s. tokens h \ (tokens o sub i o allocRel) s}" apply (rule LeadsTo_Trans) prefer 2 apply (drule System_Follows_rel [THEN @@ -1041,35 +1017,28 @@ apply (cut_tac [2] System_Client_Progress) prefer 2 apply (blast intro: LeadsTo_Basis) - apply (erule lemma3) + apply (erule System_lemma3) done -(*Lifting Alloc_Progress up to the level of systemState*) -ML {* -bind_thm ("rename_Alloc_Progress", - thm "Alloc_Progress" RS thm "rename_guarantees_sysOfAlloc_I" - |> simplify (simpset() addsimps [thm "o_def"])) -*} +text{*Lifting @{text Alloc_Progress} up to the level of systemState*} -(*progress (2), step 9*) +text{*progress (2), step 9*} lemma System_Alloc_Progress: "System : (INT i : (lessThan Nclients). - INT h. {s. h <= (sub i o allocAsk) s} + INT h. {s. h \ (sub i o allocAsk) s} LeadsTo {s. h pfixLe (sub i o allocGiv) s})" apply (simp only: o_apply sub_def) - sorry -(* - apply (rule rename_Alloc_Progress [THEN component_guaranteesD]) + apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I]) + apply (simp add: o_def del: Set.INT_iff); + apply (erule component_guaranteesD) apply (auto simp add: - System_Increasing_allocRel [simplified o_def] - System_Increasing_allocAsk [simplified o_def] - System_Bounded_allocAsk [simplified o_def] - System_Alloc_Client_Progress [simplified o_def]) + System_Increasing_allocRel [simplified sub_apply o_def] + System_Increasing_allocAsk [simplified sub_apply o_def] + System_Bounded_allocAsk [simplified sub_apply o_def] + System_Alloc_Client_Progress [simplified sub_apply o_def]) done -*) - -(*progress (2), step 10 (final result!) *) +text{*progress (2), step 10 (final result!) *} lemma System_Progress: "System : system_progress" apply (unfold system_progress_def) apply (cut_tac System_Alloc_Progress) @@ -1079,14 +1048,13 @@ done -(*Ultimate goal*) -lemma System_correct: "System : system_spec" +theorem System_correct: "System : system_spec" apply (unfold system_spec_def) apply (blast intro: System_safety System_Progress) done -(** SOME lemmas no longer used **) +text{* Some obsolete lemmas *} lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o (funPair giv (funPair ask rel))" @@ -1104,7 +1072,7 @@ apply (auto simp add: o_def) done -(*Could go to Extend.ML*) +text{*Could go to Extend.ML*} lemma bij_fst_inv_inv_eq: "bij f ==> fst (inv (%(x, u). inv f x) z) = f z" apply (rule fst_inv_equalityI) apply (rule_tac f = "%z. (f z, ?h z) " in surjI) diff -r 9cfd9eb9faec -r 4e4b7c801142 src/HOL/UNITY/Follows.thy --- a/src/HOL/UNITY/Follows.thy Fri Dec 08 13:40:26 2006 +0100 +++ b/src/HOL/UNITY/Follows.thy Fri Dec 08 18:22:28 2006 +0100 @@ -65,7 +65,7 @@ lemma Follows_Increasing2: "F \ f Fols g ==> F \ Increasing g" by (simp add: Follows_def) -lemma Follows_Bounded: "F \ f Fols g ==> F \ Always {s. f s \ g s}" +lemma Follows_Bounded: "F \ f Fols g ==> F \ Always {s. f s \ g s}" by (simp add: Follows_def) lemma Follows_LeadsTo: