--- 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 \<le> (ask o sub i o client)s} LeadsTo
- {s. h pfixLe (giv o sub i o client) s}"
+ INT h.
+ {s. h \<le> (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 \<le> giv s & h pfixGe ask s}
- LeadsTo {s. tokens h \<le> (tokens o rel) s})"
+ Increasing giv guarantees
+ (INT h. {s. h \<le> giv s & h pfixGe ask s}
+ LeadsTo {s. tokens h \<le> (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)
\<le> 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<Nclients.
- ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}
+ ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}
Int
- (INT i : lessThan Nclients.
- INT h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
- LeadsTo
- {s. tokens h \<le> (tokens o sub i o allocRel)s})
+ (INT i : lessThan Nclients.
+ INT h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
+ LeadsTo
+ {s. tokens h \<le> (tokens o sub i o allocRel)s})
guarantees
- (INT i : lessThan Nclients.
- INT h. {s. h \<le> (sub i o allocAsk) s}
- LeadsTo
- {s. h pfixLe (sub i o allocGiv) s})"
+ (INT i : lessThan Nclients.
+ INT h. {s. h \<le> (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 \<le> (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
- LeadsTo
- {s. tokens h i \<le> (tokens o sub i o allocRel)s})
+ INT h. {s. h i \<le> (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
+ LeadsTo
+ {s. tokens h i \<le> (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 \<circ> sub i \<circ> fst \<circ> lift_map i \<circ> 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 \<le> (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 \<le> (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 \<le> (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. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv) s)
\<le> NbT + (\<Sum>i \<in> 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
\<le> (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
\<le> (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 \<le> 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 \<le> 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<Nclients.
+lemma System_Bounded_allocAsk: "System : Always {s. ALL i<Nclients.
ALL elt : set ((sub i o allocAsk) s). elt \<le> 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 \<le> (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 \<le> (giv o sub i o client) s &
+ h pfixGe (ask o sub i o client) s}
LeadsTo {s. tokens h \<le> (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 \<le> (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 \<le> (giv o sub i o client) s &
+ h pfixGe (ask o sub i o client) s}
LeadsTo {s. tokens h \<le> (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 \<le> (sub i o allocGiv) s}
+ System : {s. k \<le> (sub i o allocGiv) s}
LeadsTo
{s. (sub i o allocAsk) s \<le> (ask o sub i o client) s} Int
{s. k \<le> (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 \<le> (sub i o allocGiv) s &
- h pfixGe (sub i o allocAsk) s}
- LeadsTo
- {s. h \<le> (giv o sub i o client) s &
+lemma System_lemma3: "i < Nclients
+ ==> System : {s. h \<le> (sub i o allocGiv) s &
+ h pfixGe (sub i o allocAsk) s}
+ LeadsTo
+ {s. h \<le> (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 \<le> (sub i o allocGiv) s &
- h pfixGe (sub i o allocAsk) s}
+lemma System_Alloc_Client_Progress: "i < Nclients
+ ==> System : {s. h \<le> (sub i o allocGiv) s &
+ h pfixGe (sub i o allocAsk) s}
LeadsTo {s. tokens h \<le> (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 \<le> (sub i o allocAsk) s}
+lemma System_Alloc_Progress:
+ "System : (INT i : (lessThan Nclients).
+ INT h. {s. h \<le> (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
--- 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});