# HG changeset patch # User wenzelm # Date 1186165181 -7200 # Node ID edc90be09ac166077f21538528f0009b03ab451a # Parent e4fbf438376dfc988ee165d4332858312ec3e96b misc cleanup of ML bindings (for multihreading); diff -r e4fbf438376d -r edc90be09ac1 src/HOL/UNITY/Comp.thy --- a/src/HOL/UNITY/Comp.thy Fri Aug 03 16:28:25 2007 +0200 +++ b/src/HOL/UNITY/Comp.thy Fri Aug 03 20:19:41 2007 +0200 @@ -179,7 +179,7 @@ by (auto intro: safety_prop_INTER1 simp add: preserves_def) -(** Some lemmas used only in Client.ML **) +(** Some lemmas used only in Client.thy **) lemma stable_localTo_stable2: "[| F \ stable {s. P (v s) (w s)}; diff -r e4fbf438376d -r edc90be09ac1 src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Fri Aug 03 16:28:25 2007 +0200 +++ b/src/HOL/UNITY/Comp/Alloc.thy Fri Aug 03 20:19:41 2007 +0200 @@ -30,7 +30,7 @@ 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*} @@ -59,9 +59,9 @@ --{*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}" + 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" @@ -81,9 +81,9 @@ --{*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})" + 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" @@ -93,7 +93,7 @@ client_allowed_acts :: "'a clientState_d program set" "client_allowed_acts == {F. AllowedActs F = - insert Id (UNION (preserves (funPair rel ask)) Acts)}" + 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 @@ -104,40 +104,40 @@ --{*spec (6)*} alloc_increasing :: "'a allocState_d program set" "alloc_increasing == - UNIV guarantees - (INT i : lessThan Nclients. Increasing (sub i o allocGiv))" + 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)) + (INT i : lessThan Nclients. Increasing (sub i o allocRel)) guarantees - Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s) + 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)}" --{*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 i : lessThan Nclients. Increasing (sub i o allocAsk) Int + Increasing (sub i o allocRel)) Int Always {s. ALL i NbT} + 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. + 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})" + (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}) + 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.*) @@ -145,12 +145,12 @@ 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)}" + insert Id (UNION (preserves allocGiv) Acts)}" alloc_spec :: "'a allocState_d program set" "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int @@ -161,22 +161,22 @@ --{*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))" + 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))" + 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))" + 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" @@ -184,15 +184,15 @@ 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)}" + (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 @@ -204,25 +204,25 @@ 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|)" + 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|)" + allocAsk = allocAsk al, + allocRel = allocRel al, + client = cl, + systemState.dummy = allocState_d.dummy al|)" -consts +consts Alloc :: "'a allocState_d program" Client :: "'a clientState_d program" Network :: "'a systemState program" System :: "'a systemState program" - + axioms Alloc: "Alloc : alloc_spec" Client: "Client : client_spec" @@ -232,12 +232,12 @@ System_def: "System == rename sysOfAlloc Alloc Join Network Join (rename sysOfClient - (plam x: lessThan Nclients. rename client_map Client))" + (plam x: lessThan Nclients. rename client_map Client))" (** locale System = - fixes + fixes Alloc :: 'a allocState_d program Client :: 'a clientState_d program Network :: 'a systemState program @@ -255,7 +255,7 @@ Network Join (rename sysOfClient - (plam x: lessThan Nclients. rename client_map Client))" + (plam x: lessThan Nclients. rename client_map Client))" **) (*Perhaps equalities.ML shouldn't add this in the first place!*) @@ -287,62 +287,62 @@ bij_image_Collect_eq ML {* -local - val INT_D = thm "INT_D"; -in (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*) -fun list_of_Int th = +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 @{thm INT_D})) handle THM _ => (list_of_Int (th RS bspec)) handle THM _ => [th]; -end; *} lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec] -ML {* -local - val lessThanBspec = thm "lessThanBspec" +setup {* +let + fun normalized th = + normalized (th RS spec + handle THM _ => th RS @{thm lessThanBspec} + handle THM _ => th RS bspec + handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1)) + handle THM _ => th; in -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 + Attrib.add_attributes [("normalized", Attrib.no_args (Thm.rule_attribute (K normalized)), "")] end *} (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***) ML {* -val record_auto_tac = - auto_tac (claset() addIs [ext] addSWrapper record_split_wrapper, - simpset() addsimps [thm "sysOfAlloc_def", thm "sysOfClient_def", - thm "client_map_def", thm "non_dummy_def", thm "funPair_def", thm "o_apply", thm "Let_def"]) +fun record_auto_tac (cs, ss) = + auto_tac (cs addIs [ext] addSWrapper record_split_wrapper, + ss addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def}, + @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def}, + @{thm o_apply}, @{thm Let_def}]) *} +method_setup record_auto = {* + Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt))) +*} "" lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc" apply (unfold sysOfAlloc_def Let_def) apply (rule inj_onI) - apply (tactic record_auto_tac) + apply record_auto done 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, - allocRel = allocRel s, +lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s = + (| allocGiv = allocGiv s, + allocAsk = allocAsk s, + allocRel = allocRel s, allocState_d.dummy = (client s, dummy s) |)" apply (rule inj_sysOfAlloc [THEN inv_f_eq]) - apply (tactic record_auto_tac) + apply record_auto done lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc" apply (simp add: surj_iff expand_fun_eq o_apply) - apply (tactic record_auto_tac) + apply record_auto done lemma bij_sysOfAlloc [iff]: "bij sysOfAlloc" @@ -355,22 +355,22 @@ lemma inj_sysOfClient [iff]: "inj sysOfClient" apply (unfold sysOfClient_def) apply (rule inj_onI) - apply (tactic record_auto_tac) + apply record_auto done -lemma inv_sysOfClient_eq [simp]: "!!s. inv sysOfClient s = - (client s, - (| allocGiv = allocGiv s, - allocAsk = allocAsk s, - allocRel = allocRel s, +lemma inv_sysOfClient_eq [simp]: "!!s. inv sysOfClient s = + (client s, + (| allocGiv = allocGiv s, + allocAsk = allocAsk s, + allocRel = allocRel s, allocState_d.dummy = systemState.dummy s|) )" apply (rule inj_sysOfClient [THEN inv_f_eq]) - apply (tactic record_auto_tac) + apply record_auto done lemma surj_sysOfClient [iff]: "surj sysOfClient" apply (simp add: surj_iff expand_fun_eq o_apply) - apply (tactic record_auto_tac) + apply record_auto done lemma bij_sysOfClient [iff]: "bij sysOfClient" @@ -382,19 +382,19 @@ lemma inj_client_map [iff]: "inj client_map" apply (unfold inj_on_def) - apply (tactic record_auto_tac) + apply record_auto done -lemma inv_client_map_eq [simp]: "!!s. inv client_map s = - (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, +lemma inv_client_map_eq [simp]: "!!s. inv client_map s = + (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, clientState_d.dummy = y|)) s" apply (rule inj_client_map [THEN inv_f_eq]) - apply (tactic record_auto_tac) + apply record_auto done lemma surj_client_map [iff]: "surj client_map" apply (simp add: surj_iff expand_fun_eq o_apply) - apply (tactic record_auto_tac) + apply record_auto done lemma bij_client_map [iff]: "bij client_map" @@ -424,28 +424,28 @@ 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) + apply record_auto done ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs (thm "client_o_sysOfAlloc")) *} declare client_o_sysOfAlloc' [simp] lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv" - apply (tactic record_auto_tac) + apply record_auto done ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_sysOfAlloc_eq")) *} declare allocGiv_o_sysOfAlloc_eq' [simp] lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk" - apply (tactic record_auto_tac) + apply record_auto done ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_sysOfAlloc_eq")) *} declare allocAsk_o_sysOfAlloc_eq' [simp] lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel" - apply (tactic record_auto_tac) + apply record_auto done ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_sysOfAlloc_eq")) *} @@ -455,28 +455,28 @@ subsection{* o-simprules for @{term sysOfClient} [MUST BE AUTOMATED]*} lemma client_o_sysOfClient: "client o sysOfClient = fst" - apply (tactic record_auto_tac) + apply record_auto done ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs (thm "client_o_sysOfClient")) *} declare client_o_sysOfClient' [simp] lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd " - apply (tactic record_auto_tac) + apply record_auto done ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs (thm "allocGiv_o_sysOfClient_eq")) *} declare allocGiv_o_sysOfClient_eq' [simp] lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd " - apply (tactic record_auto_tac) + apply record_auto done ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs (thm "allocAsk_o_sysOfClient_eq")) *} declare allocAsk_o_sysOfClient_eq' [simp] lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd " - apply (tactic record_auto_tac) + apply record_auto done ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs (thm "allocRel_o_sysOfClient_eq")) *} @@ -503,7 +503,7 @@ ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_inv_sysOfAlloc_eq")) *} declare allocRel_o_inv_sysOfAlloc_eq' [simp] -lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) = +lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) = rel o sub i o client" apply (simp add: o_def drop_map_def) done @@ -511,7 +511,7 @@ ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs (thm "rel_inv_client_map_drop_map")) *} declare rel_inv_client_map_drop_map [simp] -lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) = +lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) = ask o sub i o client" apply (simp add: o_def drop_map_def) done @@ -519,17 +519,6 @@ ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs (thm "ask_inv_client_map_drop_map")) *} declare ask_inv_client_map_drop_map [simp] -(** -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 -**) declare finite_lessThan [iff] @@ -541,9 +530,9 @@ ML {* val [Client_Increasing_ask, Client_Increasing_rel, - Client_Bounded, Client_Progress, Client_AllowedActs, + Client_Bounded, Client_Progress, Client_AllowedActs, Client_preserves_giv, Client_preserves_dummy] = - thm "Client" |> simplify (simpset() addsimps (thms "client_spec_simps") ) + @{thm Client} |> simplify (@{simpset} addsimps @{thms client_spec_simps}) |> list_of_Int; bind_thm ("Client_Increasing_ask", Client_Increasing_ask); @@ -571,9 +560,9 @@ ML {* val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs, - Network_preserves_allocGiv, Network_preserves_rel, - Network_preserves_ask] = - thm "Network" |> simplify (simpset() addsimps (thms "network_spec_simps")) + Network_preserves_allocGiv, Network_preserves_rel, + Network_preserves_ask] = + @{thm Network} |> simplify (@{simpset} addsimps @{thms network_spec_simps}) |> list_of_Int; bind_thm ("Network_Ask", Network_Ask); @@ -602,9 +591,9 @@ ML {* val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs, - Alloc_preserves_allocRel, Alloc_preserves_allocAsk, - Alloc_preserves_dummy] = - thm "Alloc" |> simplify (simpset() addsimps (thms "alloc_spec_simps")) + Alloc_preserves_allocRel, Alloc_preserves_allocAsk, + Alloc_preserves_dummy] = + @{thm Alloc} |> simplify (@{simpset} addsimps @{thms alloc_spec_simps}) |> list_of_Int; bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0); @@ -617,10 +606,8 @@ *} text{*Strip off the INT in the guarantees postcondition*} -ML -{* -bind_thm ("Alloc_Increasing", normalize Alloc_Increasing_0) -*} + +lemmas Alloc_Increasing = Alloc_Increasing_0 [normalized] declare Alloc_preserves_allocRel [iff] @@ -630,20 +617,20 @@ 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) +lemma Network_component_System: "Network Join + ((rename sysOfClient + (plam x: (lessThan Nclients). rename client_map Client)) Join + rename sysOfAlloc Alloc) = System" by (simp add: System_def Join_ac) -lemma Client_component_System: "(rename sysOfClient - (plam x: (lessThan Nclients). rename client_map Client)) Join +lemma Client_component_System: "(rename sysOfClient + (plam x: (lessThan Nclients). rename client_map Client)) Join (Network Join rename sysOfAlloc Alloc) = System" 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 +lemma Alloc_component_System: "rename sysOfAlloc Alloc Join + ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join Network) = System" by (simp add: System_def Join_ac) @@ -658,8 +645,8 @@ lemma Client_Allowed [simp]: "Allowed Client = preserves rel Int preserves ask" by (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff) -lemma Network_Allowed [simp]: "Allowed Network = - preserves allocRel Int +lemma Network_Allowed [simp]: "Allowed Network = + preserves allocRel Int (INT i: lessThan Nclients. preserves(giv o sub i o client))" by (auto simp add: Allowed_def Network_AllowedActs safety_prop_Acts_iff) @@ -677,14 +664,14 @@ 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 (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) +apply (subst fst_o_lift_map [symmetric]) +apply (simp only: o_assoc) done @@ -697,8 +684,8 @@ 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]) + |> 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. @@ -708,41 +695,46 @@ *) ML {* -val rename_client_map_tac = +fun rename_client_map_tac ss = EVERY [ - simp_tac (simpset() addsimps [thm "rename_guarantees_eq_rename_inv"]) 1, - rtac (thm "guarantees_PLam_I") 1, + simp_tac (ss addsimps [thm "rename_guarantees_eq_rename_inv"]) 1, + rtac @{thm guarantees_PLam_I} 1, assume_tac 2, - (*preserves: routine reasoning*) - asm_simp_tac (simpset() addsimps [thm "lift_preserves_sub"]) 2, - (*the guarantee for "lift i (rename client_map Client)" *) + (*preserves: routine reasoning*) + asm_simp_tac (ss addsimps [@{thm lift_preserves_sub}]) 2, + (*the guarantee for "lift i (rename client_map Client)" *) asm_simp_tac - (simpset() addsimps [thm "lift_guarantees_eq_lift_inv", - thm "rename_guarantees_eq_rename_inv", - thm "bij_imp_bij_inv", thm "surj_rename" RS thm "surj_range", - thm "inv_inv_eq"]) 1, + (ss addsimps [@{thm lift_guarantees_eq_lift_inv}, + @{thm rename_guarantees_eq_rename_inv}, + @{thm bij_imp_bij_inv}, @{thm surj_rename} RS @{thm surj_range}, + @{thm inv_inv_eq}]) 1, asm_simp_tac - (simpset() addsimps [thm "o_def", thm "non_dummy_def", thm "guarantees_Int_right"]) 1] + (@{simpset} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1] *} +method_setup rename_client_map = {* + Method.ctxt_args (fn ctxt => + Method.SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt))) +*} "" + 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 +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)" - by (tactic rename_client_map_tac) + by rename_client_map -lemma preserves_sub_fst_lift_map: "[| F : preserves w; i ~= j |] +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)" apply (auto simp add: lift_map_def split_def linorder_neq_iff o_def) apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD]) apply (auto simp add: o_def) done -lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |] +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 (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]) @@ -750,12 +742,12 @@ done lemma rename_sysOfClient_ok_Network: - "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) + "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) ok Network" 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) + "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) ok rename sysOfAlloc Alloc" by (simp add: ok_iff_Allowed) @@ -767,7 +759,7 @@ rename_sysOfClient_ok_Alloc [iff] rename_sysOfAlloc_ok_Network [iff] -text{*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] @@ -775,7 +767,7 @@ rename_sysOfAlloc_ok_Network [THEN ok_sym] lemma System_Increasing: "i < Nclients - ==> System : Increasing (ask o sub i o client) Int + ==> System : Increasing (ask o sub i o client) Int Increasing (rel o sub i o client)" apply (rule component_guaranteesD [OF rename_Client_Increasing Client_component_System]) apply auto @@ -788,12 +780,12 @@ (*Lifting Alloc_Increasing up to the level of systemState*) 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 + [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: +lemma System_Increasing_allocGiv: "i < Nclients ==> System : Increasing (sub i o allocGiv)" apply (unfold System_def) apply (simp add: o_def) @@ -812,19 +804,19 @@ The "Always (INT ...) formulation expresses the general safety property and allows it to be combined using @{text Always_Int_rule} below. *} -lemma System_Follows_rel: +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]) - apply (simp add: ok_commute [of Network]) + apply (simp add: ok_commute [of Network]) done -lemma System_Follows_ask: +lemma System_Follows_ask: "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))" apply (auto intro!: Network_Ask [THEN component_guaranteesD]) - apply (simp add: ok_commute [of Network]) + apply (simp add: ok_commute [of Network]) done -lemma System_Follows_allocGiv: +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]) @@ -833,21 +825,21 @@ done -lemma Always_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients. +lemma Always_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients. {s. (giv o sub i o client) s \ (sub i o allocGiv) s})" apply auto apply (erule System_Follows_allocGiv [THEN Follows_Bounded]) done -lemma Always_allocAsk_le_ask: "System : Always (INT i: lessThan Nclients. +lemma Always_allocAsk_le_ask: "System : Always (INT i: lessThan Nclients. {s. (sub i o allocAsk) s \ (ask o sub i o client) s})" apply auto apply (erule System_Follows_ask [THEN Follows_Bounded]) done -lemma Always_allocRel_le_rel: "System : Always (INT i: lessThan Nclients. +lemma Always_allocRel_le_rel: "System : Always (INT i: lessThan Nclients. {s. (sub i o allocRel) s \ (rel o sub i o client) s})" by (auto intro!: Follows_Bounded System_Follows_rel) @@ -865,27 +857,27 @@ gets rid of the other "o"s too.*) text{*safety (1), step 3*} -lemma System_sum_bounded: +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)}" apply (simp add: o_apply) - apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I]) - apply (simp add: o_def); - apply (erule component_guaranteesD) + 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 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 +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})" 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 +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})" apply (rule Always_allocRel_le_rel [THEN Always_weaken]) apply (auto intro: tokens_mono_prefix simp add: o_apply) @@ -915,15 +907,15 @@ lemmas System_Increasing_allocAsk = System_Follows_ask [THEN Follows_Increasing1, standard] 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 +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}" - by (tactic rename_client_map_tac) + by rename_client_map -lemma System_Bounded_ask: "i < Nclients - ==> System : Always +lemma System_Bounded_ask: "i < Nclients + ==> System : Always {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 @@ -934,7 +926,7 @@ done 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", @@ -949,23 +941,23 @@ lemmas System_Increasing_giv = System_Follows_allocGiv [THEN Follows_Increasing1, standard] -lemma rename_Client_Progress: "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} +lemma rename_Client_Progress: "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})" - apply (tactic rename_client_map_tac) + apply rename_client_map apply (simp add: Client_Progress [simplified o_def]) done 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 & - h pfixGe (ask o sub i o client) s} +lemma System_Client_Progress: + "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})" apply (rule INT_I) (*Couldn't have just used Auto_tac since the "INT h" must be kept*) @@ -974,7 +966,7 @@ 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} *) @@ -985,17 +977,17 @@ lemmas System_lemma2 = PSP_Stable [OF System_lemma1 - System_Follows_ask [THEN Follows_Increasing1, THEN IncreasingD]] + 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 & +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 & h pfixGe (ask o sub i o client) s}" apply (rule single_LeadsTo_I) - apply (rule_tac k6 = "h" and x2 = " (sub i o allocAsk) s" + 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) @@ -1003,9 +995,9 @@ 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 & - h pfixGe (sub i o allocAsk) s} +lemma System_Alloc_Client_Progress: "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}" apply (rule LeadsTo_Trans) prefer 2 @@ -1023,15 +1015,15 @@ text{*Lifting @{text Alloc_Progress} up to the level of systemState*} text{*progress (2), step 9*} -lemma System_Alloc_Progress: - "System : (INT i : (lessThan Nclients). - INT h. {s. h \ (sub i o allocAsk) s} +lemma System_Alloc_Progress: + "System : (INT i : (lessThan Nclients). + 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) - apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I]) - apply (simp add: o_def del: Set.INT_iff); + 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: + apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def] System_Increasing_allocAsk [simplified sub_apply o_def] System_Bounded_allocAsk [simplified sub_apply o_def] @@ -1056,13 +1048,13 @@ text{* Some obsolete lemmas *} -lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o +lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o (funPair giv (funPair ask rel))" apply (rule ext) apply (auto simp add: o_def non_dummy_def) done -lemma preserves_non_dummy_eq: "(preserves non_dummy) = +lemma preserves_non_dummy_eq: "(preserves non_dummy) = (preserves rel Int preserves ask Int preserves giv)" apply (simp add: non_dummy_eq_o_funPair) apply auto diff -r e4fbf438376d -r edc90be09ac1 src/HOL/UNITY/Comp/AllocBase.thy --- a/src/HOL/UNITY/Comp/AllocBase.thy Fri Aug 03 16:28:25 2007 +0200 +++ b/src/HOL/UNITY/Comp/AllocBase.thy Fri Aug 03 20:19:41 2007 +0200 @@ -106,19 +106,4 @@ apply (subst setsum_UN_disjoint, auto) done -ML -{* -val NbT_pos = thm "NbT_pos"; -val setsum_fun_mono = thm "setsum_fun_mono"; -val tokens_mono_prefix = thm "tokens_mono_prefix"; -val mono_tokens = thm "mono_tokens"; -val bag_of_append = thm "bag_of_append"; -val mono_bag_of = thm "mono_bag_of"; -val bag_of_sublist_lemma = thm "bag_of_sublist_lemma"; -val bag_of_sublist = thm "bag_of_sublist"; -val bag_of_sublist_Un_Int = thm "bag_of_sublist_Un_Int"; -val bag_of_sublist_Un_disjoint = thm "bag_of_sublist_Un_disjoint"; -val bag_of_sublist_UN_disjoint = thm "bag_of_sublist_UN_disjoint"; -*} - end diff -r e4fbf438376d -r edc90be09ac1 src/HOL/UNITY/Project.thy --- a/src/HOL/UNITY/Project.thy Fri Aug 03 16:28:25 2007 +0200 +++ b/src/HOL/UNITY/Project.thy Fri Aug 03 20:19:41 2007 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/UNITY/Project.ML +(* Title: HOL/UNITY/Project.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge @@ -673,21 +673,4 @@ apply (blast intro: project_LeadsTo_D) done -ML -{* -val projecting_Int = thm "projecting_Int"; -val projecting_Un = thm "projecting_Un"; -val projecting_INT = thm "projecting_INT"; -val projecting_UN = thm "projecting_UN"; -val projecting_weaken = thm "projecting_weaken"; -val projecting_weaken_L = thm "projecting_weaken_L"; -val extending_Int = thm "extending_Int"; -val extending_Un = thm "extending_Un"; -val extending_INT = thm "extending_INT"; -val extending_UN = thm "extending_UN"; -val extending_weaken = thm "extending_weaken"; -val extending_weaken_L = thm "extending_weaken_L"; -val projecting_UNIV = thm "projecting_UNIV"; -*} - end diff -r e4fbf438376d -r edc90be09ac1 src/HOL/UNITY/ROOT.ML --- a/src/HOL/UNITY/ROOT.ML Fri Aug 03 16:28:25 2007 +0200 +++ b/src/HOL/UNITY/ROOT.ML Fri Aug 03 20:19:41 2007 +0200 @@ -6,39 +6,44 @@ Root file for UNITY proofs. *) -(*Basic meta-theory*) -time_use_thy "UNITY_Main"; +(*Verifying security protocols using UNITY*) +no_document use_thy "../Auth/Public"; -(*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"; +use_thys [ + (*Basic meta-theory*) + "UNITY_Main", -(*Verifying security protocols using UNITY*) -with_path "../Auth" (no_document use_thy) "Public"; -with_path "../Auth" time_use_thy "Simple/NSP_Bad"; + (*Simple examples: no composition*) + "Simple/Deadlock", + "Simple/Common", + "Simple/Network", + "Simple/Token", + "Simple/Channel", + "Simple/Lift", + "Simple/Mutex", + "Simple/Reach", + "Simple/Reachability", -(*Example of composition*) -time_use_thy "Comp/Handshake"; + (*Verifying security protocols using UNITY*) + "Simple/NSP_Bad", -(*Universal properties examples*) -time_use_thy "Comp/Counter"; -time_use_thy "Comp/Counterc"; -time_use_thy "Comp/Priority"; + (*Example of composition*) + "Comp/Handshake", -time_use_thy "Comp/TimerArray"; + (*Universal properties examples*) + "Comp/Counter", + "Comp/Counterc", + "Comp/Priority", + + "Comp/TimerArray", + + (*obsolete*) + "ELT" +]; (*Allocator example*) (* FIXME some parts no longer work -- had been commented out for a long time *) setmp quick_and_dirty true - time_use_thy "Comp/Alloc"; -time_use_thy "Comp/AllocImpl"; -time_use_thy "Comp/Client"; + use_thy "Comp/Alloc"; -time_use_thy "ELT"; (*obsolete*) +use_thys ["Comp/AllocImpl", "Comp/Client"]; diff -r e4fbf438376d -r edc90be09ac1 src/HOL/UNITY/Simple/NSP_Bad.thy --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Aug 03 16:28:25 2007 +0200 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Aug 03 20:19:41 2007 +0200 @@ -3,8 +3,6 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge -ML{*add_path "$ISABELLE_HOME/src/HOL/Auth"*} - Original file is ../Auth/NS_Public_Bad *) @@ -103,28 +101,25 @@ text{*This ML code does the inductions directly.*} ML{* -val ns_constrainsI = thm "ns_constrainsI"; -val impCE = thm "impCE"; - fun ns_constrains_tac(cs,ss) i = SELECT_GOAL - (EVERY [REPEAT (etac Always_ConstrainsI 1), - REPEAT (resolve_tac [StableI, stableI, - constrains_imp_Constrains] 1), - rtac ns_constrainsI 1, + (EVERY [REPEAT (etac @{thm Always_ConstrainsI} 1), + REPEAT (resolve_tac [@{thm StableI}, @{thm stableI}, + @{thm constrains_imp_Constrains}] 1), + rtac @{thm ns_constrainsI} 1, full_simp_tac ss 1, REPEAT (FIRSTGOAL (etac disjE)), - ALLGOALS (clarify_tac (cs delrules [impI,impCE])), + ALLGOALS (clarify_tac (cs delrules [impI, @{thm impCE}])), REPEAT (FIRSTGOAL analz_mono_contra_tac), ALLGOALS (asm_simp_tac ss)]) i; (*Tactic for proving secrecy theorems*) fun ns_induct_tac(cs,ss) = (SELECT_GOAL o EVERY) - [rtac AlwaysI 1, + [rtac @{thm AlwaysI} 1, force_tac (cs,ss) 1, (*"reachable" gets in here*) - rtac (Always_reachable RS Always_ConstrainsI RS StableI) 1, + rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1, ns_constrains_tac(cs,ss) 1]; *} diff -r e4fbf438376d -r edc90be09ac1 src/HOL/UNITY/UNITY.thy --- a/src/HOL/UNITY/UNITY.thy Fri Aug 03 16:28:25 2007 +0200 +++ b/src/HOL/UNITY/UNITY.thy Fri Aug 03 20:19:41 2007 +0200 @@ -55,7 +55,7 @@ "increasing f == \z. stable {s. z \ f s}" -text{*Perhaps equalities.ML shouldn't add this in the first place!*} +text{*Perhaps HOL shouldn't add this in the first place!*} declare image_Collect [simp del] subsubsection{*The abstract type of programs*} @@ -346,7 +346,7 @@ lemma Int_Union_Union: "Union(B) \ A = Union((%C. C \ A)`B)" by blast -text{*Needed for WF reasoning in WFair.ML*} +text{*Needed for WF reasoning in WFair.thy*} lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k" by blast diff -r e4fbf438376d -r edc90be09ac1 src/HOL/UNITY/UNITY_Main.thy --- a/src/HOL/UNITY/UNITY_Main.thy Fri Aug 03 16:28:25 2007 +0200 +++ b/src/HOL/UNITY/UNITY_Main.thy Fri Aug 03 20:19:41 2007 +0200 @@ -11,13 +11,13 @@ method_setup safety = {* Method.ctxt_args (fn ctxt => - Method.SIMPLE_METHOD' (gen_constrains_tac (local_clasimpset_of ctxt))) *} + Method.SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *} "for proving safety properties" method_setup ensures_tac = {* fn args => fn ctxt => Method.goal_args' (Scan.lift Args.name) - (gen_ensures_tac (local_clasimpset_of ctxt)) + (ensures_tac (local_clasimpset_of ctxt)) args ctxt *} "for proving progress properties" diff -r e4fbf438376d -r edc90be09ac1 src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Fri Aug 03 16:28:25 2007 +0200 +++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Aug 03 20:19:41 2007 +0200 @@ -3,803 +3,60 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2003 University of Cambridge -Specialized UNITY tactics, and ML bindings of theorems +Specialized UNITY tactics. *) -(*ListOrder*) -val Domain_def = thm "Domain_def"; -val Le_def = thm "Le_def"; -val Ge_def = thm "Ge_def"; -val prefix_def = thm "prefix_def"; -val Nil_genPrefix = thm "Nil_genPrefix"; -val genPrefix_length_le = thm "genPrefix_length_le"; -val cons_genPrefixE = thm "cons_genPrefixE"; -val Cons_genPrefix_Cons = thm "Cons_genPrefix_Cons"; -val refl_genPrefix = thm "refl_genPrefix"; -val genPrefix_refl = thm "genPrefix_refl"; -val genPrefix_mono = thm "genPrefix_mono"; -val append_genPrefix = thm "append_genPrefix"; -val genPrefix_trans_O = thm "genPrefix_trans_O"; -val genPrefix_trans = thm "genPrefix_trans"; -val prefix_genPrefix_trans = thm "prefix_genPrefix_trans"; -val genPrefix_prefix_trans = thm "genPrefix_prefix_trans"; -val trans_genPrefix = thm "trans_genPrefix"; -val genPrefix_antisym = thm "genPrefix_antisym"; -val antisym_genPrefix = thm "antisym_genPrefix"; -val genPrefix_Nil = thm "genPrefix_Nil"; -val same_genPrefix_genPrefix = thm "same_genPrefix_genPrefix"; -val genPrefix_Cons = thm "genPrefix_Cons"; -val genPrefix_take_append = thm "genPrefix_take_append"; -val genPrefix_append_both = thm "genPrefix_append_both"; -val append_cons_eq = thm "append_cons_eq"; -val append_one_genPrefix = thm "append_one_genPrefix"; -val genPrefix_imp_nth = thm "genPrefix_imp_nth"; -val nth_imp_genPrefix = thm "nth_imp_genPrefix"; -val genPrefix_iff_nth = thm "genPrefix_iff_nth"; -val prefix_refl = thm "prefix_refl"; -val prefix_trans = thm "prefix_trans"; -val prefix_antisym = thm "prefix_antisym"; -val prefix_less_le = thm "prefix_less_le"; -val set_mono = thm "set_mono"; -val Nil_prefix = thm "Nil_prefix"; -val prefix_Nil = thm "prefix_Nil"; -val Cons_prefix_Cons = thm "Cons_prefix_Cons"; -val same_prefix_prefix = thm "same_prefix_prefix"; -val append_prefix = thm "append_prefix"; -val prefix_appendI = thm "prefix_appendI"; -val prefix_Cons = thm "prefix_Cons"; -val append_one_prefix = thm "append_one_prefix"; -val prefix_length_le = thm "prefix_length_le"; -val strict_prefix_length_less = thm "strict_prefix_length_less"; -val mono_length = thm "mono_length"; -val prefix_iff = thm "prefix_iff"; -val prefix_snoc = thm "prefix_snoc"; -val prefix_append_iff = thm "prefix_append_iff"; -val common_prefix_linear = thm "common_prefix_linear"; -val reflexive_Le = thm "reflexive_Le"; -val antisym_Le = thm "antisym_Le"; -val trans_Le = thm "trans_Le"; -val pfixLe_refl = thm "pfixLe_refl"; -val pfixLe_trans = thm "pfixLe_trans"; -val pfixLe_antisym = thm "pfixLe_antisym"; -val prefix_imp_pfixLe = thm "prefix_imp_pfixLe"; -val reflexive_Ge = thm "reflexive_Ge"; -val antisym_Ge = thm "antisym_Ge"; -val trans_Ge = thm "trans_Ge"; -val pfixGe_refl = thm "pfixGe_refl"; -val pfixGe_trans = thm "pfixGe_trans"; -val pfixGe_antisym = thm "pfixGe_antisym"; -val prefix_imp_pfixGe = thm "prefix_imp_pfixGe"; - - -(*UNITY*) -val mk_total_program_def = thm "mk_total_program_def"; -val totalize_act_def = thm "totalize_act_def"; -val constrains_def = thm "constrains_def"; -val stable_def = thm "stable_def"; -val invariant_def = thm "invariant_def"; -val increasing_def = thm "increasing_def"; -val Allowed_def = thm "Allowed_def"; -val Id_in_Acts = thm "Id_in_Acts"; -val insert_Id_Acts = thm "insert_Id_Acts"; -val Id_in_AllowedActs = thm "Id_in_AllowedActs"; -val insert_Id_AllowedActs = thm "insert_Id_AllowedActs"; -val Init_eq = thm "Init_eq"; -val Acts_eq = thm "Acts_eq"; -val AllowedActs_eq = thm "AllowedActs_eq"; -val surjective_mk_program = thm "surjective_mk_program"; -val program_equalityI = thm "program_equalityI"; -val program_equalityE = thm "program_equalityE"; -val program_equality_iff = thm "program_equality_iff"; -val def_prg_Init = thm "def_prg_Init"; -val def_prg_Acts = thm "def_prg_Acts"; -val def_prg_AllowedActs = thm "def_prg_AllowedActs"; -val def_act_simp = thm "def_act_simp"; -val def_set_simp = thm "def_set_simp"; -val constrainsI = thm "constrainsI"; -val constrainsD = thm "constrainsD"; -val constrains_empty = thm "constrains_empty"; -val constrains_empty2 = thm "constrains_empty2"; -val constrains_UNIV = thm "constrains_UNIV"; -val constrains_UNIV2 = thm "constrains_UNIV2"; -val constrains_weaken_R = thm "constrains_weaken_R"; -val constrains_weaken_L = thm "constrains_weaken_L"; -val constrains_weaken = thm "constrains_weaken"; -val constrains_Un = thm "constrains_Un"; -val constrains_UN = thm "constrains_UN"; -val constrains_Un_distrib = thm "constrains_Un_distrib"; -val constrains_UN_distrib = thm "constrains_UN_distrib"; -val constrains_Int_distrib = thm "constrains_Int_distrib"; -val constrains_INT_distrib = thm "constrains_INT_distrib"; -val constrains_Int = thm "constrains_Int"; -val constrains_INT = thm "constrains_INT"; -val constrains_imp_subset = thm "constrains_imp_subset"; -val constrains_trans = thm "constrains_trans"; -val constrains_cancel = thm "constrains_cancel"; -val unlessI = thm "unlessI"; -val unlessD = thm "unlessD"; -val stableI = thm "stableI"; -val stableD = thm "stableD"; -val stable_UNIV = thm "stable_UNIV"; -val stable_Un = thm "stable_Un"; -val stable_UN = thm "stable_UN"; -val stable_Int = thm "stable_Int"; -val stable_INT = thm "stable_INT"; -val stable_constrains_Un = thm "stable_constrains_Un"; -val stable_constrains_Int = thm "stable_constrains_Int"; -val stable_constrains_stable = thm "stable_constrains_stable"; -val invariantI = thm "invariantI"; -val invariant_Int = thm "invariant_Int"; -val increasingD = thm "increasingD"; -val increasing_constant = thm "increasing_constant"; -val mono_increasing_o = thm "mono_increasing_o"; -val strict_increasingD = thm "strict_increasingD"; -val elimination = thm "elimination"; -val elimination_sing = thm "elimination_sing"; -val constrains_strongest_rhs = thm "constrains_strongest_rhs"; -val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest"; -val Un_Diff_Diff = thm "Un_Diff_Diff"; -val Int_Union_Union = thm "Int_Union_Union"; -val Image_less_than = thm "Image_less_than"; -val Image_inverse_less_than = thm "Image_inverse_less_than"; -val totalize_constrains_iff = thm "totalize_constrains_iff"; - -(*WFair*) -val stable_transient_empty = thm "stable_transient_empty"; -val transient_strengthen = thm "transient_strengthen"; -val transientI = thm "transientI"; -val totalize_transientI = thm "totalize_transientI"; -val transientE = thm "transientE"; -val transient_empty = thm "transient_empty"; -val ensuresI = thm "ensuresI"; -val ensuresD = thm "ensuresD"; -val ensures_weaken_R = thm "ensures_weaken_R"; -val stable_ensures_Int = thm "stable_ensures_Int"; -val stable_transient_ensures = thm "stable_transient_ensures"; -val ensures_eq = thm "ensures_eq"; -val leadsTo_Basis = thm "leadsTo_Basis"; -val leadsTo_Trans = thm "leadsTo_Trans"; -val transient_imp_leadsTo = thm "transient_imp_leadsTo"; -val leadsTo_Un_duplicate = thm "leadsTo_Un_duplicate"; -val leadsTo_Un_duplicate2 = thm "leadsTo_Un_duplicate2"; -val leadsTo_Union = thm "leadsTo_Union"; -val leadsTo_Union_Int = thm "leadsTo_Union_Int"; -val leadsTo_UN = thm "leadsTo_UN"; -val leadsTo_Un = thm "leadsTo_Un"; -val single_leadsTo_I = thm "single_leadsTo_I"; -val leadsTo_induct = thm "leadsTo_induct"; -val subset_imp_ensures = thm "subset_imp_ensures"; -val subset_imp_leadsTo = thm "subset_imp_leadsTo"; -val leadsTo_refl = thm "leadsTo_refl"; -val empty_leadsTo = thm "empty_leadsTo"; -val leadsTo_UNIV = thm "leadsTo_UNIV"; -val leadsTo_induct_pre = thm "leadsTo_induct_pre"; -val leadsTo_weaken_R = thm "leadsTo_weaken_R"; -val leadsTo_weaken_L = thm "leadsTo_weaken_L"; -val leadsTo_Un_distrib = thm "leadsTo_Un_distrib"; -val leadsTo_UN_distrib = thm "leadsTo_UN_distrib"; -val leadsTo_Union_distrib = thm "leadsTo_Union_distrib"; -val leadsTo_weaken = thm "leadsTo_weaken"; -val leadsTo_Diff = thm "leadsTo_Diff"; -val leadsTo_UN_UN = thm "leadsTo_UN_UN"; -val leadsTo_Un_Un = thm "leadsTo_Un_Un"; -val leadsTo_cancel2 = thm "leadsTo_cancel2"; -val leadsTo_cancel_Diff2 = thm "leadsTo_cancel_Diff2"; -val leadsTo_cancel1 = thm "leadsTo_cancel1"; -val leadsTo_cancel_Diff1 = thm "leadsTo_cancel_Diff1"; -val leadsTo_empty = thm "leadsTo_empty"; -val psp_stable = thm "psp_stable"; -val psp_stable2 = thm "psp_stable2"; -val psp_ensures = thm "psp_ensures"; -val psp = thm "psp"; -val psp2 = thm "psp2"; -val psp_unless = thm "psp_unless"; -val leadsTo_wf_induct = thm "leadsTo_wf_induct"; -val bounded_induct = thm "bounded_induct"; -val lessThan_induct = thm "lessThan_induct"; -val lessThan_bounded_induct = thm "lessThan_bounded_induct"; -val greaterThan_bounded_induct = thm "greaterThan_bounded_induct"; -val wlt_leadsTo = thm "wlt_leadsTo"; -val leadsTo_subset = thm "leadsTo_subset"; -val leadsTo_eq_subset_wlt = thm "leadsTo_eq_subset_wlt"; -val wlt_increasing = thm "wlt_increasing"; -val leadsTo_123 = thm "leadsTo_123"; -val wlt_constrains_wlt = thm "wlt_constrains_wlt"; -val completion = thm "completion"; -val finite_completion = thm "finite_completion"; -val stable_completion = thm "stable_completion"; -val finite_stable_completion = thm "finite_stable_completion"; - -(*Constrains*) -val Increasing_def = thm "Increasing_def"; -val reachable_Init = thm "reachable.Init"; -val reachable_Acts = thm "reachable.Acts"; -val reachable_equiv_traces = thm "reachable_equiv_traces"; -val Init_subset_reachable = thm "Init_subset_reachable"; -val stable_reachable = thm "stable_reachable"; -val invariant_reachable = thm "invariant_reachable"; -val invariant_includes_reachable = thm "invariant_includes_reachable"; -val constrains_reachable_Int = thm "constrains_reachable_Int"; -val Constrains_eq_constrains = thm "Constrains_eq_constrains"; -val constrains_imp_Constrains = thm "constrains_imp_Constrains"; -val stable_imp_Stable = thm "stable_imp_Stable"; -val ConstrainsI = thm "ConstrainsI"; -val Constrains_empty = thm "Constrains_empty"; -val Constrains_UNIV = thm "Constrains_UNIV"; -val Constrains_weaken_R = thm "Constrains_weaken_R"; -val Constrains_weaken_L = thm "Constrains_weaken_L"; -val Constrains_weaken = thm "Constrains_weaken"; -val Constrains_Un = thm "Constrains_Un"; -val Constrains_UN = thm "Constrains_UN"; -val Constrains_Int = thm "Constrains_Int"; -val Constrains_INT = thm "Constrains_INT"; -val Constrains_imp_subset = thm "Constrains_imp_subset"; -val Constrains_trans = thm "Constrains_trans"; -val Constrains_cancel = thm "Constrains_cancel"; -val Stable_eq = thm "Stable_eq"; -val Stable_eq_stable = thm "Stable_eq_stable"; -val StableI = thm "StableI"; -val StableD = thm "StableD"; -val Stable_Un = thm "Stable_Un"; -val Stable_Int = thm "Stable_Int"; -val Stable_Constrains_Un = thm "Stable_Constrains_Un"; -val Stable_Constrains_Int = thm "Stable_Constrains_Int"; -val Stable_UN = thm "Stable_UN"; -val Stable_INT = thm "Stable_INT"; -val Stable_reachable = thm "Stable_reachable"; -val IncreasingD = thm "IncreasingD"; -val mono_Increasing_o = thm "mono_Increasing_o"; -val strict_IncreasingD = thm "strict_IncreasingD"; -val increasing_imp_Increasing = thm "increasing_imp_Increasing"; -val Increasing_constant = thm "Increasing_constant"; -val Elimination = thm "Elimination"; -val Elimination_sing = thm "Elimination_sing"; -val AlwaysI = thm "AlwaysI"; -val AlwaysD = thm "AlwaysD"; -val AlwaysE = thm "AlwaysE"; -val Always_imp_Stable = thm "Always_imp_Stable"; -val Always_includes_reachable = thm "Always_includes_reachable"; -val invariant_imp_Always = thm "invariant_imp_Always"; -val Always_reachable = thm "Always_reachable"; -val Always_eq_invariant_reachable = thm "Always_eq_invariant_reachable"; -val Always_eq_includes_reachable = thm "Always_eq_includes_reachable"; -val Always_UNIV_eq = thm "Always_UNIV_eq"; -val UNIV_AlwaysI = thm "UNIV_AlwaysI"; -val Always_eq_UN_invariant = thm "Always_eq_UN_invariant"; -val Always_weaken = thm "Always_weaken"; -val Always_Constrains_pre = thm "Always_Constrains_pre"; -val Always_Constrains_post = thm "Always_Constrains_post"; -val Always_ConstrainsI = thm "Always_ConstrainsI"; -val Always_ConstrainsD = thm "Always_ConstrainsD"; -val Always_Constrains_weaken = thm "Always_Constrains_weaken"; -val Always_Int_distrib = thm "Always_Int_distrib"; -val Always_INT_distrib = thm "Always_INT_distrib"; -val Always_Int_I = thm "Always_Int_I"; -val Always_Compl_Un_eq = thm "Always_Compl_Un_eq"; -val Always_thin = thm "Always_thin"; - -(*FP*) -val stable_FP_Orig_Int = thm "stable_FP_Orig_Int"; -val FP_Orig_weakest = thm "FP_Orig_weakest"; -val stable_FP_Int = thm "stable_FP_Int"; -val FP_equivalence = thm "FP_equivalence"; -val FP_weakest = thm "FP_weakest"; -val Compl_FP = thm "Compl_FP"; -val Diff_FP = thm "Diff_FP"; - -(*SubstAx*) -val LeadsTo_eq_leadsTo = thm "LeadsTo_eq_leadsTo"; -val Always_LeadsTo_pre = thm "Always_LeadsTo_pre"; -val Always_LeadsTo_post = thm "Always_LeadsTo_post"; -val Always_LeadsToI = thm "Always_LeadsToI"; -val Always_LeadsToD = thm "Always_LeadsToD"; -val leadsTo_imp_LeadsTo = thm "leadsTo_imp_LeadsTo"; -val LeadsTo_Trans = thm "LeadsTo_Trans"; -val LeadsTo_Union = thm "LeadsTo_Union"; -val LeadsTo_UNIV = thm "LeadsTo_UNIV"; -val LeadsTo_Un_duplicate = thm "LeadsTo_Un_duplicate"; -val LeadsTo_Un_duplicate2 = thm "LeadsTo_Un_duplicate2"; -val LeadsTo_UN = thm "LeadsTo_UN"; -val LeadsTo_Un = thm "LeadsTo_Un"; -val single_LeadsTo_I = thm "single_LeadsTo_I"; -val subset_imp_LeadsTo = thm "subset_imp_LeadsTo"; -val empty_LeadsTo = thm "empty_LeadsTo"; -val LeadsTo_weaken_R = thm "LeadsTo_weaken_R"; -val LeadsTo_weaken_L = thm "LeadsTo_weaken_L"; -val LeadsTo_weaken = thm "LeadsTo_weaken"; -val Always_LeadsTo_weaken = thm "Always_LeadsTo_weaken"; -val LeadsTo_Un_post = thm "LeadsTo_Un_post"; -val LeadsTo_Trans_Un = thm "LeadsTo_Trans_Un"; -val LeadsTo_Un_distrib = thm "LeadsTo_Un_distrib"; -val LeadsTo_UN_distrib = thm "LeadsTo_UN_distrib"; -val LeadsTo_Union_distrib = thm "LeadsTo_Union_distrib"; -val LeadsTo_Basis = thm "LeadsTo_Basis"; -val EnsuresI = thm "EnsuresI"; -val Always_LeadsTo_Basis = thm "Always_LeadsTo_Basis"; -val LeadsTo_Diff = thm "LeadsTo_Diff"; -val LeadsTo_UN_UN = thm "LeadsTo_UN_UN"; -val LeadsTo_UN_UN_noindex = thm "LeadsTo_UN_UN_noindex"; -val all_LeadsTo_UN_UN = thm "all_LeadsTo_UN_UN"; -val LeadsTo_Un_Un = thm "LeadsTo_Un_Un"; -val LeadsTo_cancel2 = thm "LeadsTo_cancel2"; -val LeadsTo_cancel_Diff2 = thm "LeadsTo_cancel_Diff2"; -val LeadsTo_cancel1 = thm "LeadsTo_cancel1"; -val LeadsTo_cancel_Diff1 = thm "LeadsTo_cancel_Diff1"; -val LeadsTo_empty = thm "LeadsTo_empty"; -val PSP_Stable = thm "PSP_Stable"; -val PSP_Stable2 = thm "PSP_Stable2"; -val PSP = thm "PSP"; -val PSP2 = thm "PSP2"; -val PSP_Unless = thm "PSP_Unless"; -val Stable_transient_Always_LeadsTo = thm "Stable_transient_Always_LeadsTo"; -val LeadsTo_wf_induct = thm "LeadsTo_wf_induct"; -val Bounded_induct = thm "Bounded_induct"; -val LessThan_induct = thm "LessThan_induct"; -val integ_0_le_induct = thm "integ_0_le_induct"; -val LessThan_bounded_induct = thm "LessThan_bounded_induct"; -val GreaterThan_bounded_induct = thm "GreaterThan_bounded_induct"; -val Completion = thm "Completion"; -val Finite_completion = thm "Finite_completion"; -val Stable_completion = thm "Stable_completion"; -val Finite_stable_completion = thm "Finite_stable_completion"; - -(*Union*) -val Init_SKIP = thm "Init_SKIP"; -val Acts_SKIP = thm "Acts_SKIP"; -val AllowedActs_SKIP = thm "AllowedActs_SKIP"; -val reachable_SKIP = thm "reachable_SKIP"; -val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff"; -val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff"; -val SKIP_in_stable = thm "SKIP_in_stable"; -val Init_Join = thm "Init_Join"; -val Acts_Join = thm "Acts_Join"; -val AllowedActs_Join = thm "AllowedActs_Join"; -val JN_empty = thm "JN_empty"; -val JN_insert = thm "JN_insert"; -val Init_JN = thm "Init_JN"; -val Acts_JN = thm "Acts_JN"; -val AllowedActs_JN = thm "AllowedActs_JN"; -val JN_cong = thm "JN_cong"; -val Join_commute = thm "Join_commute"; -val Join_assoc = thm "Join_assoc"; -val Join_left_commute = thm "Join_left_commute"; -val Join_SKIP_left = thm "Join_SKIP_left"; -val Join_SKIP_right = thm "Join_SKIP_right"; -val Join_absorb = thm "Join_absorb"; -val Join_left_absorb = thm "Join_left_absorb"; -val Join_ac = thms "Join_ac"; -val JN_absorb = thm "JN_absorb"; -val JN_Un = thm "JN_Un"; -val JN_constant = thm "JN_constant"; -val JN_Join_distrib = thm "JN_Join_distrib"; -val JN_Join_miniscope = thm "JN_Join_miniscope"; -val JN_Join_diff = thm "JN_Join_diff"; -val JN_constrains = thm "JN_constrains"; -val Join_constrains = thm "Join_constrains"; -val Join_unless = thm "Join_unless"; -val Join_constrains_weaken = thm "Join_constrains_weaken"; -val JN_constrains_weaken = thm "JN_constrains_weaken"; -val JN_stable = thm "JN_stable"; -val invariant_JN_I = thm "invariant_JN_I"; -val Join_stable = thm "Join_stable"; -val Join_increasing = thm "Join_increasing"; -val invariant_JoinI = thm "invariant_JoinI"; -val FP_JN = thm "FP_JN"; -val JN_transient = thm "JN_transient"; -val Join_transient = thm "Join_transient"; -val Join_transient_I1 = thm "Join_transient_I1"; -val Join_transient_I2 = thm "Join_transient_I2"; -val JN_ensures = thm "JN_ensures"; -val Join_ensures = thm "Join_ensures"; -val stable_Join_constrains = thm "stable_Join_constrains"; -val stable_Join_Always1 = thm "stable_Join_Always1"; -val stable_Join_Always2 = thm "stable_Join_Always2"; -val stable_Join_ensures1 = thm "stable_Join_ensures1"; -val stable_Join_ensures2 = thm "stable_Join_ensures2"; -val ok_SKIP1 = thm "ok_SKIP1"; -val ok_SKIP2 = thm "ok_SKIP2"; -val ok_Join_commute = thm "ok_Join_commute"; -val ok_commute = thm "ok_commute"; -val ok_sym = thm "ok_sym"; -val ok_iff_OK = thm "ok_iff_OK"; -val ok_Join_iff1 = thm "ok_Join_iff1"; -val ok_Join_iff2 = thm "ok_Join_iff2"; -val ok_Join_commute_I = thm "ok_Join_commute_I"; -val ok_JN_iff1 = thm "ok_JN_iff1"; -val ok_JN_iff2 = thm "ok_JN_iff2"; -val OK_iff_ok = thm "OK_iff_ok"; -val OK_imp_ok = thm "OK_imp_ok"; -val Allowed_SKIP = thm "Allowed_SKIP"; -val Allowed_Join = thm "Allowed_Join"; -val Allowed_JN = thm "Allowed_JN"; -val ok_iff_Allowed = thm "ok_iff_Allowed"; -val OK_iff_Allowed = thm "OK_iff_Allowed"; -val safety_prop_Acts_iff = thm "safety_prop_Acts_iff"; -val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed"; -val Allowed_eq = thm "Allowed_eq"; -val def_prg_Allowed = thm "def_prg_Allowed"; -val def_total_prg_Allowed = thm "def_total_prg_Allowed"; -val safety_prop_constrains = thm "safety_prop_constrains"; -val safety_prop_stable = thm "safety_prop_stable"; -val safety_prop_Int = thm "safety_prop_Int"; -val safety_prop_INTER1 = thm "safety_prop_INTER1"; -val safety_prop_INTER = thm "safety_prop_INTER"; -val def_UNION_ok_iff = thm "def_UNION_ok_iff"; -val totalize_JN = thm "totalize_JN"; - -(*Comp*) -val preserves_def = thm "preserves_def"; -val funPair_def = thm "funPair_def"; -val componentI = thm "componentI"; -val component_eq_subset = thm "component_eq_subset"; -val component_SKIP = thm "component_SKIP"; -val component_refl = thm "component_refl"; -val SKIP_minimal = thm "SKIP_minimal"; -val component_Join1 = thm "component_Join1"; -val component_Join2 = thm "component_Join2"; -val Join_absorb1 = thm "Join_absorb1"; -val Join_absorb2 = thm "Join_absorb2"; -val JN_component_iff = thm "JN_component_iff"; -val component_JN = thm "component_JN"; -val component_trans = thm "component_trans"; -val component_antisym = thm "component_antisym"; -val Join_component_iff = thm "Join_component_iff"; -val component_constrains = thm "component_constrains"; -val program_less_le = thm "program_less_le"; -val preservesI = thm "preservesI"; -val preserves_imp_eq = thm "preserves_imp_eq"; -val Join_preserves = thm "Join_preserves"; -val JN_preserves = thm "JN_preserves"; -val SKIP_preserves = thm "SKIP_preserves"; -val funPair_apply = thm "funPair_apply"; -val preserves_funPair = thm "preserves_funPair"; -val funPair_o_distrib = thm "funPair_o_distrib"; -val fst_o_funPair = thm "fst_o_funPair"; -val snd_o_funPair = thm "snd_o_funPair"; -val subset_preserves_o = thm "subset_preserves_o"; -val preserves_subset_stable = thm "preserves_subset_stable"; -val preserves_subset_increasing = thm "preserves_subset_increasing"; -val preserves_id_subset_stable = thm "preserves_id_subset_stable"; -val safety_prop_preserves = thm "safety_prop_preserves"; -val stable_localTo_stable2 = thm "stable_localTo_stable2"; -val Increasing_preserves_Stable = thm "Increasing_preserves_Stable"; -val component_of_imp_component = thm "component_of_imp_component"; -val component_of_refl = thm "component_of_refl"; -val component_of_SKIP = thm "component_of_SKIP"; -val component_of_trans = thm "component_of_trans"; -val strict_component_of_eq = thm "strict_component_of_eq"; -val localize_Init_eq = thm "localize_Init_eq"; -val localize_Acts_eq = thm "localize_Acts_eq"; -val localize_AllowedActs_eq = thm "localize_AllowedActs_eq"; - -(*Guar*) -val guar_def = thm "guar_def"; -val OK_insert_iff = thm "OK_insert_iff"; -val ex1 = thm "ex1"; -val ex2 = thm "ex2"; -val ex_prop_finite = thm "ex_prop_finite"; -val ex_prop_equiv = thm "ex_prop_equiv"; -val uv1 = thm "uv1"; -val uv2 = thm "uv2"; -val uv_prop_finite = thm "uv_prop_finite"; -val guaranteesI = thm "guaranteesI"; -val guaranteesD = thm "guaranteesD"; -val component_guaranteesD = thm "component_guaranteesD"; -val guarantees_weaken = thm "guarantees_weaken"; -val subset_imp_guarantees_UNIV = thm "subset_imp_guarantees_UNIV"; -val subset_imp_guarantees = thm "subset_imp_guarantees"; -val ex_prop_imp = thm "ex_prop_imp"; -val guarantees_imp = thm "guarantees_imp"; -val ex_prop_equiv2 = thm "ex_prop_equiv2"; -val guarantees_UN_left = thm "guarantees_UN_left"; -val guarantees_Un_left = thm "guarantees_Un_left"; -val guarantees_INT_right = thm "guarantees_INT_right"; -val guarantees_Int_right = thm "guarantees_Int_right"; -val guarantees_Int_right_I = thm "guarantees_Int_right_I"; -val guarantees_INT_right_iff = thm "guarantees_INT_right_iff"; -val shunting = thm "shunting"; -val contrapositive = thm "contrapositive"; -val combining1 = thm "combining1"; -val combining2 = thm "combining2"; -val all_guarantees = thm "all_guarantees"; -val ex_guarantees = thm "ex_guarantees"; -val guarantees_Join_Int = thm "guarantees_Join_Int"; -val guarantees_Join_Un = thm "guarantees_Join_Un"; -val guarantees_JN_INT = thm "guarantees_JN_INT"; -val guarantees_JN_UN = thm "guarantees_JN_UN"; -val guarantees_Join_I1 = thm "guarantees_Join_I1"; -val guarantees_Join_I2 = thm "guarantees_Join_I2"; -val guarantees_JN_I = thm "guarantees_JN_I"; -val Join_welldef_D1 = thm "Join_welldef_D1"; -val Join_welldef_D2 = thm "Join_welldef_D2"; -val refines_refl = thm "refines_refl"; -val ex_refinement_thm = thm "ex_refinement_thm"; -val uv_refinement_thm = thm "uv_refinement_thm"; -val guarantees_equiv = thm "guarantees_equiv"; -val wg_weakest = thm "wg_weakest"; -val wg_guarantees = thm "wg_guarantees"; -val wg_equiv = thm "wg_equiv"; -val component_of_wg = thm "component_of_wg"; -val wg_finite = thm "wg_finite"; -val wg_ex_prop = thm "wg_ex_prop"; -val wx_subset = thm "wx_subset"; -val wx_ex_prop = thm "wx_ex_prop"; -val wx_weakest = thm "wx_weakest"; -val wx'_ex_prop = thm "wx'_ex_prop"; -val wx_equiv = thm "wx_equiv"; -val guarantees_wx_eq = thm "guarantees_wx_eq"; -val stable_guarantees_Always = thm "stable_guarantees_Always"; -val leadsTo_Basis = thm "leadsTo_Basis"; -val constrains_guarantees_leadsTo = thm "constrains_guarantees_leadsTo"; - -(*Extend*) -val Restrict_iff = thm "Restrict_iff"; -val Restrict_UNIV = thm "Restrict_UNIV"; -val Restrict_empty = thm "Restrict_empty"; -val Restrict_Int = thm "Restrict_Int"; -val Restrict_triv = thm "Restrict_triv"; -val Restrict_subset = thm "Restrict_subset"; -val Restrict_eq_mono = thm "Restrict_eq_mono"; -val Restrict_imageI = thm "Restrict_imageI"; -val Domain_Restrict = thm "Domain_Restrict"; -val Image_Restrict = thm "Image_Restrict"; -val insert_Id_image_Acts = thm "insert_Id_image_Acts"; -val good_mapI = thm "good_mapI"; -val good_map_is_surj = thm "good_map_is_surj"; -val fst_inv_equalityI = thm "fst_inv_equalityI"; -val project_set_iff = thm "project_set_iff"; -val extend_set_mono = thm "extend_set_mono"; -val extend_set_empty = thm "extend_set_empty"; -val project_set_Int_subset = thm "project_set_Int_subset"; -val Init_extend = thm "Init_extend"; -val Init_project = thm "Init_project"; -val Acts_project = thm "Acts_project"; -val project_set_UNIV = thm "project_set_UNIV"; -val project_set_Union = thm "project_set_Union"; -val project_act_mono = thm "project_act_mono"; -val project_constrains_project_set = thm "project_constrains_project_set"; -val project_stable_project_set = thm "project_stable_project_set"; - - -(*Rename*) -val good_map_bij = thm "good_map_bij"; -val fst_o_inv_eq_inv = thm "fst_o_inv_eq_inv"; -val mem_rename_set_iff = thm "mem_rename_set_iff"; -val extend_set_eq_image = thm "extend_set_eq_image"; -val Init_rename = thm "Init_rename"; -val extend_set_inv = thm "extend_set_inv"; -val bij_extend_act_eq_project_act = thm "bij_extend_act_eq_project_act"; -val bij_extend_act = thm "bij_extend_act"; -val bij_project_act = thm "bij_project_act"; -val bij_inv_project_act_eq = thm "bij_inv_project_act_eq"; -val Acts_project = thm "Acts_project"; -val extend_inv = thm "extend_inv"; -val rename_inv_rename = thm "rename_inv_rename"; -val rename_rename_inv = thm "rename_rename_inv"; -val rename_inv_eq = thm "rename_inv_eq"; -val bij_extend = thm "bij_extend"; -val bij_project = thm "bij_project"; -val inv_project_eq = thm "inv_project_eq"; -val Allowed_rename = thm "Allowed_rename"; -val bij_rename = thm "bij_rename"; -val surj_rename = thm "surj_rename"; -val inj_rename_imp_inj = thm "inj_rename_imp_inj"; -val surj_rename_imp_surj = thm "surj_rename_imp_surj"; -val bij_rename_imp_bij = thm "bij_rename_imp_bij"; -val bij_rename_iff = thm "bij_rename_iff"; -val rename_SKIP = thm "rename_SKIP"; -val rename_Join = thm "rename_Join"; -val rename_JN = thm "rename_JN"; -val rename_constrains = thm "rename_constrains"; -val rename_stable = thm "rename_stable"; -val rename_invariant = thm "rename_invariant"; -val rename_increasing = thm "rename_increasing"; -val reachable_rename_eq = thm "reachable_rename_eq"; -val rename_Constrains = thm "rename_Constrains"; -val rename_Stable = thm "rename_Stable"; -val rename_Always = thm "rename_Always"; -val rename_Increasing = thm "rename_Increasing"; -val rename_transient = thm "rename_transient"; -val rename_ensures = thm "rename_ensures"; -val rename_leadsTo = thm "rename_leadsTo"; -val rename_LeadsTo = thm "rename_LeadsTo"; -val rename_rename_guarantees_eq = thm "rename_rename_guarantees_eq"; -val rename_guarantees_eq_rename_inv = thm "rename_guarantees_eq_rename_inv"; -val rename_preserves = thm "rename_preserves"; -val ok_rename_iff = thm "ok_rename_iff"; -val OK_rename_iff = thm "OK_rename_iff"; -val bij_eq_rename = thm "bij_eq_rename"; -val rename_image_constrains = thm "rename_image_constrains"; -val rename_image_stable = thm "rename_image_stable"; -val rename_image_increasing = thm "rename_image_increasing"; -val rename_image_invariant = thm "rename_image_invariant"; -val rename_image_Constrains = thm "rename_image_Constrains"; -val rename_image_preserves = thm "rename_image_preserves"; -val rename_image_Stable = thm "rename_image_Stable"; -val rename_image_Increasing = thm "rename_image_Increasing"; -val rename_image_Always = thm "rename_image_Always"; -val rename_image_leadsTo = thm "rename_image_leadsTo"; -val rename_image_LeadsTo = thm "rename_image_LeadsTo"; - - - -(*Lift_prog*) -val sub_def = thm "sub_def"; -val lift_map_def = thm "lift_map_def"; -val drop_map_def = thm "drop_map_def"; -val insert_map_inverse = thm "insert_map_inverse"; -val insert_map_delete_map_eq = thm "insert_map_delete_map_eq"; -val insert_map_inject1 = thm "insert_map_inject1"; -val insert_map_inject2 = thm "insert_map_inject2"; -val insert_map_inject = thm "insert_map_inject"; -val insert_map_inject = thm "insert_map_inject"; -val lift_map_eq_iff = thm "lift_map_eq_iff"; -val drop_map_lift_map_eq = thm "drop_map_lift_map_eq"; -val inj_lift_map = thm "inj_lift_map"; -val lift_map_drop_map_eq = thm "lift_map_drop_map_eq"; -val drop_map_inject = thm "drop_map_inject"; -val surj_lift_map = thm "surj_lift_map"; -val bij_lift_map = thm "bij_lift_map"; -val inv_lift_map_eq = thm "inv_lift_map_eq"; -val inv_drop_map_eq = thm "inv_drop_map_eq"; -val bij_drop_map = thm "bij_drop_map"; -val sub_apply = thm "sub_apply"; -val lift_set_empty = thm "lift_set_empty"; -val lift_set_iff = thm "lift_set_iff"; -val lift_set_iff2 = thm "lift_set_iff2"; -val lift_set_mono = thm "lift_set_mono"; -val lift_set_Un_distrib = thm "lift_set_Un_distrib"; -val lift_set_Diff_distrib = thm "lift_set_Diff_distrib"; -val bij_lift = thm "bij_lift"; -val lift_SKIP = thm "lift_SKIP"; -val lift_Join = thm "lift_Join"; -val lift_JN = thm "lift_JN"; -val lift_constrains = thm "lift_constrains"; -val lift_stable = thm "lift_stable"; -val lift_invariant = thm "lift_invariant"; -val lift_Constrains = thm "lift_Constrains"; -val lift_Stable = thm "lift_Stable"; -val lift_Always = thm "lift_Always"; -val lift_transient = thm "lift_transient"; -val lift_ensures = thm "lift_ensures"; -val lift_leadsTo = thm "lift_leadsTo"; -val lift_LeadsTo = thm "lift_LeadsTo"; -val lift_lift_guarantees_eq = thm "lift_lift_guarantees_eq"; -val lift_guarantees_eq_lift_inv = thm "lift_guarantees_eq_lift_inv"; -val lift_preserves_snd_I = thm "lift_preserves_snd_I"; -val delete_map_eqE = thm "delete_map_eqE"; -val delete_map_eqE = thm "delete_map_eqE"; -val delete_map_neq_apply = thm "delete_map_neq_apply"; -val vimage_o_fst_eq = thm "vimage_o_fst_eq"; -val vimage_sub_eq_lift_set = thm "vimage_sub_eq_lift_set"; -val mem_lift_act_iff = thm "mem_lift_act_iff"; -val preserves_snd_lift_stable = thm "preserves_snd_lift_stable"; -val constrains_imp_lift_constrains = thm "constrains_imp_lift_constrains"; -val lift_map_image_Times = thm "lift_map_image_Times"; -val lift_preserves_eq = thm "lift_preserves_eq"; -val lift_preserves_sub = thm "lift_preserves_sub"; -val o_equiv_assoc = thm "o_equiv_assoc"; -val o_equiv_apply = thm "o_equiv_apply"; -val fst_o_lift_map = thm "fst_o_lift_map"; -val snd_o_lift_map = thm "snd_o_lift_map"; -val extend_act_extend_act = thm "extend_act_extend_act"; -val project_act_project_act = thm "project_act_project_act"; -val project_act_extend_act = thm "project_act_extend_act"; -val act_in_UNION_preserves_fst = thm "act_in_UNION_preserves_fst"; -val UNION_OK_lift_I = thm "UNION_OK_lift_I"; -val OK_lift_I = thm "OK_lift_I"; -val Allowed_lift = thm "Allowed_lift"; -val lift_image_preserves = thm "lift_image_preserves"; - - -(*PPROD*) -val Init_PLam = thm "Init_PLam"; -val PLam_empty = thm "PLam_empty"; -val PLam_SKIP = thm "PLam_SKIP"; -val PLam_insert = thm "PLam_insert"; -val PLam_component_iff = thm "PLam_component_iff"; -val component_PLam = thm "component_PLam"; -val PLam_constrains = thm "PLam_constrains"; -val PLam_stable = thm "PLam_stable"; -val PLam_transient = thm "PLam_transient"; -val PLam_ensures = thm "PLam_ensures"; -val PLam_leadsTo_Basis = thm "PLam_leadsTo_Basis"; -val invariant_imp_PLam_invariant = thm "invariant_imp_PLam_invariant"; -val PLam_preserves_fst = thm "PLam_preserves_fst"; -val PLam_preserves_snd = thm "PLam_preserves_snd"; -val guarantees_PLam_I = thm "guarantees_PLam_I"; -val Allowed_PLam = thm "Allowed_PLam"; -val PLam_preserves = thm "PLam_preserves"; - -(*Follows*) -val mono_Always_o = thm "mono_Always_o"; -val mono_LeadsTo_o = thm "mono_LeadsTo_o"; -val Follows_constant = thm "Follows_constant"; -val mono_Follows_o = thm "mono_Follows_o"; -val mono_Follows_apply = thm "mono_Follows_apply"; -val Follows_trans = thm "Follows_trans"; -val Follows_Increasing1 = thm "Follows_Increasing1"; -val Follows_Increasing2 = thm "Follows_Increasing2"; -val Follows_Bounded = thm "Follows_Bounded"; -val Follows_LeadsTo = thm "Follows_LeadsTo"; -val Follows_LeadsTo_pfixLe = thm "Follows_LeadsTo_pfixLe"; -val Follows_LeadsTo_pfixGe = thm "Follows_LeadsTo_pfixGe"; -val Always_Follows1 = thm "Always_Follows1"; -val Always_Follows2 = thm "Always_Follows2"; -val increasing_Un = thm "increasing_Un"; -val Increasing_Un = thm "Increasing_Un"; -val Always_Un = thm "Always_Un"; -val Follows_Un = thm "Follows_Un"; -val increasing_union = thm "increasing_union"; -val Increasing_union = thm "Increasing_union"; -val Always_union = thm "Always_union"; -val Follows_union = thm "Follows_union"; -val Follows_setsum = thm "Follows_setsum"; -val Increasing_imp_Stable_pfixGe = thm "Increasing_imp_Stable_pfixGe"; -val LeadsTo_le_imp_pfixGe = thm "LeadsTo_le_imp_pfixGe"; - - -(*Lazy unfolding of actions or of sets*) -fun simp_of_act def = def RS def_act_simp; - -fun simp_of_set def = def RS def_set_simp; - - (*Combines two invariance ASSUMPTIONS into one. USEFUL??*) -val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin +val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin} (*Combines a list of invariance THEOREMS into one.*) -val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I) +val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}) (*Proves "co" properties when the program is specified. Any use of invariants (from weak constrains) must have been done already.*) -fun gen_constrains_tac(cs,ss) i = +fun constrains_tac(cs,ss) i = SELECT_GOAL (EVERY [REPEAT (Always_Int_tac 1), (*reduce the fancy safety properties to "constrains"*) - REPEAT (etac Always_ConstrainsI 1 - ORELSE - resolve_tac [StableI, stableI, - constrains_imp_Constrains] 1), + REPEAT (etac @{thm Always_ConstrainsI} 1 + ORELSE + resolve_tac [@{thm StableI}, @{thm stableI}, + @{thm constrains_imp_Constrains}] 1), (*for safety, the totalize operator can be ignored*) - simp_tac (HOL_ss addsimps - [mk_total_program_def, totalize_constrains_iff]) 1, - rtac constrainsI 1, - full_simp_tac ss 1, - REPEAT (FIRSTGOAL (etac disjE)), - ALLGOALS (clarify_tac cs), - ALLGOALS (asm_lr_simp_tac ss)]) i; + simp_tac (HOL_ss addsimps + [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1, + rtac @{thm constrainsI} 1, + full_simp_tac ss 1, + REPEAT (FIRSTGOAL (etac disjE)), + ALLGOALS (clarify_tac cs), + ALLGOALS (asm_lr_simp_tac ss)]) i; (*proves "ensures/leadsTo" properties when the program is specified*) -fun gen_ensures_tac(cs,ss) sact = +fun ensures_tac(cs,ss) sact = SELECT_GOAL (EVERY [REPEAT (Always_Int_tac 1), - etac Always_LeadsTo_Basis 1 - ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) - REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis, - EnsuresI, ensuresI] 1), - (*now there are two subgoals: co & transient*) - simp_tac (ss addsimps [mk_total_program_def]) 2, - res_inst_tac [("act", sact)] totalize_transientI 2 - ORELSE res_inst_tac [("act", sact)] transientI 2, + etac @{thm Always_LeadsTo_Basis} 1 + ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) + REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, + @{thm EnsuresI}, @{thm ensuresI}] 1), + (*now there are two subgoals: co & transient*) + simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2, + res_inst_tac [("act", sact)] @{thm totalize_transientI} 2 + ORELSE res_inst_tac [("act", sact)] @{thm transientI} 2, (*simplify the command's domain*) - simp_tac (ss addsimps [Domain_def]) 3, - gen_constrains_tac (cs,ss) 1, - ALLGOALS (clarify_tac cs), - ALLGOALS (asm_lr_simp_tac ss)]); - -fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st; - -fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact; + simp_tac (ss addsimps [@{thm Domain_def}]) 3, + constrains_tac (cs,ss) 1, + ALLGOALS (clarify_tac cs), + ALLGOALS (asm_lr_simp_tac ss)]); (*Composition equivalences, from Lift_prog*) fun make_o_equivs th = [th, - th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]), - th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])]; + th RS @{thm o_equiv_assoc} |> simplify (HOL_ss addsimps [@{thm o_assoc}]), + th RS @{thm o_equiv_apply} |> simplify (HOL_ss addsimps [@{thm o_def}, @{thm sub_def}])]; -Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair); +Addsimps (make_o_equivs @{thm fst_o_funPair} @ make_o_equivs @{thm snd_o_funPair}); -Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map); +Addsimps (make_o_equivs @{thm fst_o_lift_map} @ make_o_equivs @{thm snd_o_lift_map});