--- a/src/HOL/UNITY/Comp.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp.thy Wed May 25 11:50:58 2016 +0200
@@ -8,7 +8,7 @@
Technical Report 2000-003, University of Florida, 2000.
*)
-section{*Composition: Basic Primitives*}
+section\<open>Composition: Basic Primitives\<close>
theory Comp
imports Union
@@ -42,7 +42,7 @@
where "funPair f g == %x. (f x, g x)"
-subsection{*The component relation*}
+subsection\<open>The component relation\<close>
lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F\<squnion>G)"
apply (unfold component_def, auto)
apply (rule_tac x = "G\<squnion>Ga" in exI)
@@ -115,7 +115,7 @@
lemmas program_less_le = strict_component_def
-subsection{*The preserves property*}
+subsection\<open>The preserves property\<close>
lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
by (unfold preserves_def, blast)
--- a/src/HOL/UNITY/Comp/Alloc.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Wed May 25 11:50:58 2016 +0200
@@ -9,55 +9,55 @@
imports AllocBase "../PPROD"
begin
-subsection{*State definitions. OUTPUT variables are locals*}
+subsection\<open>State definitions. OUTPUT variables are locals\<close>
record clientState =
- giv :: "nat list" --{*client's INPUT history: tokens GRANTED*}
- ask :: "nat list" --{*client's OUTPUT history: tokens REQUESTED*}
- rel :: "nat list" --{*client's OUTPUT history: tokens RELEASED*}
+ giv :: "nat list" \<comment>\<open>client's INPUT history: tokens GRANTED\<close>
+ ask :: "nat list" \<comment>\<open>client's OUTPUT history: tokens REQUESTED\<close>
+ rel :: "nat list" \<comment>\<open>client's OUTPUT history: tokens RELEASED\<close>
record 'a clientState_d =
clientState +
- dummy :: 'a --{*dummy field for new variables*}
+ dummy :: 'a \<comment>\<open>dummy field for new variables\<close>
definition
- --{*DUPLICATED FROM Client.thy, but with "tok" removed*}
- --{*Maybe want a special theory section to declare such maps*}
+ \<comment>\<open>DUPLICATED FROM Client.thy, but with "tok" removed\<close>
+ \<comment>\<open>Maybe want a special theory section to declare such maps\<close>
non_dummy :: "'a clientState_d => clientState"
where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s|)"
definition
- --{*Renaming map to put a Client into the standard form*}
+ \<comment>\<open>Renaming map to put a Client into the standard form\<close>
client_map :: "'a clientState_d => clientState*'a"
where "client_map = funPair non_dummy dummy"
record allocState =
- allocGiv :: "nat => nat list" --{*OUTPUT history: source of "giv" for i*}
- allocAsk :: "nat => nat list" --{*INPUT: allocator's copy of "ask" for i*}
- allocRel :: "nat => nat list" --{*INPUT: allocator's copy of "rel" for i*}
+ allocGiv :: "nat => nat list" \<comment>\<open>OUTPUT history: source of "giv" for i\<close>
+ allocAsk :: "nat => nat list" \<comment>\<open>INPUT: allocator's copy of "ask" for i\<close>
+ allocRel :: "nat => nat list" \<comment>\<open>INPUT: allocator's copy of "rel" for i\<close>
record 'a allocState_d =
allocState +
- dummy :: 'a --{*dummy field for new variables*}
+ dummy :: 'a \<comment>\<open>dummy field for new variables\<close>
record 'a systemState =
allocState +
- client :: "nat => clientState" --{*states of all clients*}
- dummy :: 'a --{*dummy field for new variables*}
+ client :: "nat => clientState" \<comment>\<open>states of all clients\<close>
+ dummy :: 'a \<comment>\<open>dummy field for new variables\<close>
---{** Resource allocation system specification **}
+\<comment>\<open>* Resource allocation system specification *\<close>
definition
- --{*spec (1)*}
+ \<comment>\<open>spec (1)\<close>
system_safety :: "'a systemState program set"
where "system_safety =
Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o giv o sub i o client)s)
\<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o rel o sub i o client)s)}"
definition
- --{*spec (2)*}
+ \<comment>\<open>spec (2)\<close>
system_progress :: "'a systemState program set"
where "system_progress = (INT i : lessThan Nclients.
INT h.
@@ -68,20 +68,20 @@
system_spec :: "'a systemState program set"
where "system_spec = system_safety Int system_progress"
---{** Client specification (required) ***}
+\<comment>\<open>* Client specification (required) **\<close>
definition
- --{*spec (3)*}
+ \<comment>\<open>spec (3)\<close>
client_increasing :: "'a clientState_d program set"
where "client_increasing = UNIV guarantees Increasing ask Int Increasing rel"
definition
- --{*spec (4)*}
+ \<comment>\<open>spec (4)\<close>
client_bounded :: "'a clientState_d program set"
where "client_bounded = UNIV guarantees Always {s. ALL elt : set (ask s). elt \<le> NbT}"
definition
- --{*spec (5)*}
+ \<comment>\<open>spec (5)\<close>
client_progress :: "'a clientState_d program set"
where "client_progress =
Increasing giv guarantees
@@ -89,12 +89,12 @@
LeadsTo {s. tokens h \<le> (tokens o rel) s})"
definition
- --{*spec: preserves part*}
+ \<comment>\<open>spec: preserves part\<close>
client_preserves :: "'a clientState_d program set"
where "client_preserves = preserves giv Int preserves clientState_d.dummy"
definition
- --{*environmental constraints*}
+ \<comment>\<open>environmental constraints\<close>
client_allowed_acts :: "'a clientState_d program set"
where "client_allowed_acts =
{F. AllowedActs F =
@@ -105,17 +105,17 @@
where "client_spec = client_increasing Int client_bounded Int client_progress
Int client_allowed_acts Int client_preserves"
---{** Allocator specification (required) **}
+\<comment>\<open>* Allocator specification (required) *\<close>
definition
- --{*spec (6)*}
+ \<comment>\<open>spec (6)\<close>
alloc_increasing :: "'a allocState_d program set"
where "alloc_increasing =
UNIV guarantees
(INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
definition
- --{*spec (7)*}
+ \<comment>\<open>spec (7)\<close>
alloc_safety :: "'a allocState_d program set"
where "alloc_safety =
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
@@ -124,7 +124,7 @@
\<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)}"
definition
- --{*spec (8)*}
+ \<comment>\<open>spec (8)\<close>
alloc_progress :: "'a allocState_d program set"
where "alloc_progress =
(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
@@ -151,13 +151,13 @@
looked at.*)
definition
- --{*spec: preserves part*}
+ \<comment>\<open>spec: preserves part\<close>
alloc_preserves :: "'a allocState_d program set"
where "alloc_preserves = preserves allocRel Int preserves allocAsk Int
preserves allocState_d.dummy"
definition
- --{*environmental constraints*}
+ \<comment>\<open>environmental constraints\<close>
alloc_allowed_acts :: "'a allocState_d program set"
where "alloc_allowed_acts =
{F. AllowedActs F =
@@ -168,17 +168,17 @@
where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int
alloc_allowed_acts Int alloc_preserves"
---{** Network specification **}
+\<comment>\<open>* Network specification *\<close>
definition
- --{*spec (9.1)*}
+ \<comment>\<open>spec (9.1)\<close>
network_ask :: "'a systemState program set"
where "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)))"
definition
- --{*spec (9.2)*}
+ \<comment>\<open>spec (9.2)\<close>
network_giv :: "'a systemState program set"
where "network_giv = (INT i : lessThan Nclients.
Increasing (sub i o allocGiv)
@@ -186,7 +186,7 @@
((giv o sub i o client) Fols (sub i o allocGiv)))"
definition
- --{*spec (9.3)*}
+ \<comment>\<open>spec (9.3)\<close>
network_rel :: "'a systemState program set"
where "network_rel = (INT i : lessThan Nclients.
Increasing (rel o sub i o client)
@@ -194,7 +194,7 @@
((sub i o allocRel) Fols (rel o sub i o client)))"
definition
- --{*spec: preserves part*}
+ \<comment>\<open>spec: preserves part\<close>
network_preserves :: "'a systemState program set"
where "network_preserves =
preserves allocGiv Int
@@ -202,7 +202,7 @@
preserves (ask o sub i o client))"
definition
- --{*environmental constraints*}
+ \<comment>\<open>environmental constraints\<close>
network_allowed_acts :: "'a systemState program set"
where "network_allowed_acts =
{F. AllowedActs F =
@@ -218,7 +218,7 @@
network_preserves"
---{** State mappings **}
+\<comment>\<open>* State mappings *\<close>
definition
sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
where "sysOfAlloc = (%s. let (cl,xtr) = allocState_d.dummy s
@@ -300,7 +300,7 @@
bij_is_inj [THEN image_Int]
bij_image_Collect_eq
-ML {*
+ML \<open>
(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
fun list_of_Int th =
(list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
@@ -308,11 +308,11 @@
handle THM _ => (list_of_Int (th RS @{thm INT_D}))
handle THM _ => (list_of_Int (th RS bspec))
handle THM _ => [th];
-*}
+\<close>
lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
-attribute_setup normalized = {*
+attribute_setup normalized = \<open>
let
fun normalized th =
normalized (th RS spec
@@ -323,10 +323,10 @@
in
Scan.succeed (Thm.rule_attribute [] (K normalized))
end
-*}
+\<close>
(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
-ML {*
+ML \<open>
fun record_auto_tac ctxt =
let val ctxt' =
ctxt addSWrapper Record.split_wrapper
@@ -336,9 +336,9 @@
@{thm o_apply}, @{thm Let_def}]
in auto_tac ctxt' end;
-*}
+\<close>
-method_setup record_auto = {* Scan.succeed (SIMPLE_METHOD o record_auto_tac) *}
+method_setup record_auto = \<open>Scan.succeed (SIMPLE_METHOD o record_auto_tac)\<close>
lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
apply (unfold sysOfAlloc_def Let_def)
@@ -346,7 +346,7 @@
apply record_auto
done
-text{*We need the inverse; also having it simplifies the proof of surjectivity*}
+text\<open>We need the inverse; also having it simplifies the proof of surjectivity\<close>
lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s =
(| allocGiv = allocGiv s,
allocAsk = allocAsk s,
@@ -366,7 +366,7 @@
done
-subsubsection{*bijectivity of @{term sysOfClient}*}
+subsubsection\<open>bijectivity of @{term sysOfClient}\<close>
lemma inj_sysOfClient [iff]: "inj sysOfClient"
apply (unfold sysOfClient_def)
@@ -394,7 +394,7 @@
done
-subsubsection{*bijectivity of @{term client_map}*}
+subsubsection\<open>bijectivity of @{term client_map}\<close>
lemma inj_client_map [iff]: "inj client_map"
apply (unfold inj_on_def)
@@ -418,14 +418,14 @@
done
-text{*o-simprules for @{term client_map}*}
+text\<open>o-simprules for @{term client_map}\<close>
lemma fst_o_client_map: "fst o client_map = non_dummy"
apply (unfold client_map_def)
apply (rule fst_o_funPair)
done
-ML {* ML_Thms.bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map}) *}
+ML \<open>ML_Thms.bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map})\<close>
declare fst_o_client_map' [simp]
lemma snd_o_client_map: "snd o client_map = clientState_d.dummy"
@@ -433,90 +433,90 @@
apply (rule snd_o_funPair)
done
-ML {* ML_Thms.bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map}) *}
+ML \<open>ML_Thms.bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map})\<close>
declare snd_o_client_map' [simp]
-subsection{*o-simprules for @{term sysOfAlloc} [MUST BE AUTOMATED]*}
+subsection\<open>o-simprules for @{term sysOfAlloc} [MUST BE AUTOMATED]\<close>
lemma client_o_sysOfAlloc: "client o sysOfAlloc = fst o allocState_d.dummy "
apply record_auto
done
-ML {* ML_Thms.bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc}) *}
+ML \<open>ML_Thms.bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc})\<close>
declare client_o_sysOfAlloc' [simp]
lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv"
apply record_auto
done
-ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq})\<close>
declare allocGiv_o_sysOfAlloc_eq' [simp]
lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk"
apply record_auto
done
-ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq})\<close>
declare allocAsk_o_sysOfAlloc_eq' [simp]
lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel"
apply record_auto
done
-ML {* ML_Thms.bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq})\<close>
declare allocRel_o_sysOfAlloc_eq' [simp]
-subsection{* o-simprules for @{term sysOfClient} [MUST BE AUTOMATED]*}
+subsection\<open>o-simprules for @{term sysOfClient} [MUST BE AUTOMATED]\<close>
lemma client_o_sysOfClient: "client o sysOfClient = fst"
apply record_auto
done
-ML {* ML_Thms.bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient}) *}
+ML \<open>ML_Thms.bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient})\<close>
declare client_o_sysOfClient' [simp]
lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd "
apply record_auto
done
-ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq})\<close>
declare allocGiv_o_sysOfClient_eq' [simp]
lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd "
apply record_auto
done
-ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq})\<close>
declare allocAsk_o_sysOfClient_eq' [simp]
lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd "
apply record_auto
done
-ML {* ML_Thms.bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq})\<close>
declare allocRel_o_sysOfClient_eq' [simp]
lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv"
apply (simp add: o_def)
done
-ML {* ML_Thms.bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq})\<close>
declare allocGiv_o_inv_sysOfAlloc_eq' [simp]
lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk"
apply (simp add: o_def)
done
-ML {* ML_Thms.bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq})\<close>
declare allocAsk_o_inv_sysOfAlloc_eq' [simp]
lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel"
apply (simp add: o_def)
done
-ML {* ML_Thms.bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq})\<close>
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) =
@@ -524,7 +524,7 @@
apply (simp add: o_def drop_map_def)
done
-ML {* ML_Thms.bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map}) *}
+ML \<open>ML_Thms.bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map})\<close>
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) =
@@ -532,17 +532,17 @@
apply (simp add: o_def drop_map_def)
done
-ML {* ML_Thms.bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map}) *}
+ML \<open>ML_Thms.bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map})\<close>
declare ask_inv_client_map_drop_map [simp]
-text{*Client : <unfolded specification> *}
+text\<open>Client : <unfolded specification>\<close>
lemmas client_spec_simps =
client_spec_def client_increasing_def client_bounded_def
client_progress_def client_allowed_acts_def client_preserves_def
guarantees_Int_right
-ML {*
+ML \<open>
val [Client_Increasing_ask, Client_Increasing_rel,
Client_Bounded, Client_Progress, Client_AllowedActs,
Client_preserves_giv, Client_preserves_dummy] =
@@ -556,7 +556,7 @@
ML_Thms.bind_thm ("Client_AllowedActs", Client_AllowedActs);
ML_Thms.bind_thm ("Client_preserves_giv", Client_preserves_giv);
ML_Thms.bind_thm ("Client_preserves_dummy", Client_preserves_dummy);
-*}
+\<close>
declare
Client_Increasing_ask [iff]
@@ -566,13 +566,13 @@
Client_preserves_dummy [iff]
-text{*Network : <unfolded specification> *}
+text\<open>Network : <unfolded specification>\<close>
lemmas network_spec_simps =
network_spec_def network_ask_def network_giv_def
network_rel_def network_allowed_acts_def network_preserves_def
ball_conj_distrib
-ML {*
+ML \<open>
val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
Network_preserves_allocGiv, Network_preserves_rel,
Network_preserves_ask] =
@@ -586,7 +586,7 @@
ML_Thms.bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv);
ML_Thms.bind_thm ("Network_preserves_rel", Network_preserves_rel);
ML_Thms.bind_thm ("Network_preserves_ask", Network_preserves_ask);
-*}
+\<close>
declare Network_preserves_allocGiv [iff]
@@ -598,12 +598,12 @@
Network_preserves_rel [simplified o_def, simp]
Network_preserves_ask [simplified o_def, simp]
-text{*Alloc : <unfolded specification> *}
+text\<open>Alloc : <unfolded specification>\<close>
lemmas alloc_spec_simps =
alloc_spec_def alloc_increasing_def alloc_safety_def
alloc_progress_def alloc_allowed_acts_def alloc_preserves_def
-ML {*
+ML \<open>
val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
Alloc_preserves_dummy] =
@@ -617,9 +617,9 @@
ML_Thms.bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel);
ML_Thms.bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk);
ML_Thms.bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy);
-*}
+\<close>
-text{*Strip off the INT in the guarantees postcondition*}
+text\<open>Strip off the INT in the guarantees postcondition\<close>
lemmas Alloc_Increasing = Alloc_Increasing_0 [normalized]
@@ -629,7 +629,7 @@
Alloc_preserves_dummy [iff]
-subsection{*Components Lemmas [MUST BE AUTOMATED]*}
+subsection\<open>Components Lemmas [MUST BE AUTOMATED]\<close>
lemma Network_component_System: "Network \<squnion>
((rename sysOfClient
@@ -654,7 +654,7 @@
Alloc_component_System [iff]
-text{** These preservation laws should be generated automatically **}
+text\<open>* These preservation laws should be generated automatically *\<close>
lemma Client_Allowed [simp]: "Allowed Client = preserves rel Int preserves ask"
by (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff)
@@ -667,7 +667,7 @@
lemma Alloc_Allowed [simp]: "Allowed Alloc = preserves allocGiv"
by (auto simp add: Allowed_def Alloc_AllowedActs safety_prop_Acts_iff)
-text{*needed in @{text rename_client_map_tac}*}
+text\<open>needed in \<open>rename_client_map_tac\<close>\<close>
lemma OK_lift_rename_Client [simp]: "OK I (%i. lift i (rename client_map Client))"
apply (rule OK_lift_I)
apply auto
@@ -708,7 +708,7 @@
ad-hoc!
*)
ML
-{*
+\<open>
fun rename_client_map_tac ctxt =
EVERY [
simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1,
@@ -724,13 +724,13 @@
@{thm inv_inv_eq}]) 1,
asm_simp_tac
(ctxt addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
-*}
+\<close>
-method_setup rename_client_map = {*
+method_setup rename_client_map = \<open>
Scan.succeed (fn ctxt => SIMPLE_METHOD (rename_client_map_tac ctxt))
-*}
+\<close>
-text{*Lifting @{text Client_Increasing} to @{term systemState}*}
+text\<open>Lifting \<open>Client_Increasing\<close> to @{term systemState}\<close>
lemma rename_Client_Increasing: "i : I
==> rename sysOfClient (plam x: I. rename client_map Client) :
UNIV guarantees
@@ -772,8 +772,8 @@
rename_sysOfClient_ok_Alloc [iff]
rename_sysOfAlloc_ok_Network [iff]
-text{*The "ok" laws, re-oriented.
- But not sure this works: theorem @{text ok_commute} is needed below*}
+text\<open>The "ok" laws, re-oriented.
+ But not sure this works: theorem \<open>ok_commute\<close> is needed below\<close>
declare
rename_sysOfClient_ok_Network [THEN ok_sym, iff]
rename_sysOfClient_ok_Alloc [THEN ok_sym, iff]
@@ -807,15 +807,15 @@
done
-ML {*
+ML \<open>
ML_Thms.bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
-*}
+\<close>
declare System_Increasing' [intro!]
-text{* Follows consequences.
+text\<open>Follows consequences.
The "Always (INT ...) formulation expresses the general safety property
- and allows it to be combined using @{text Always_Int_rule} below. *}
+ and allows it to be combined using \<open>Always_Int_rule\<close> below.\<close>
lemma System_Follows_rel:
"i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))"
@@ -857,11 +857,11 @@
by (auto intro!: Follows_Bounded System_Follows_rel)
-subsection{*Proof of the safety property (1)*}
+subsection\<open>Proof of the safety property (1)\<close>
-text{*safety (1), step 1 is @{text System_Follows_rel}*}
+text\<open>safety (1), step 1 is \<open>System_Follows_rel\<close>\<close>
-text{*safety (1), step 2*}
+text\<open>safety (1), step 2\<close>
(* i < Nclients ==> System : Increasing (sub i o allocRel) *)
lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1]
@@ -869,7 +869,7 @@
Simplifying with o_def gets rid of the translations but it unfortunately
gets rid of the other "o"s too.*)
-text{*safety (1), step 3*}
+text\<open>safety (1), step 3\<close>
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)}"
@@ -880,7 +880,7 @@
apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
done
-text{* Follows reasoning*}
+text\<open>Follows reasoning\<close>
lemma Always_tokens_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients.
{s. (tokens o giv o sub i o client) s
@@ -896,12 +896,12 @@
apply (auto intro: tokens_mono_prefix simp add: o_apply)
done
-text{*safety (1), step 4 (final result!) *}
+text\<open>safety (1), step 4 (final result!)\<close>
theorem System_safety: "System : system_safety"
apply (unfold system_safety_def)
- apply (tactic {* resolve_tac @{context} [Always_Int_rule [@{thm System_sum_bounded},
+ apply (tactic \<open>resolve_tac @{context} [Always_Int_rule [@{thm System_sum_bounded},
@{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS
- @{thm Always_weaken}] 1 *})
+ @{thm Always_weaken}] 1\<close>)
apply auto
apply (rule setsum_fun_mono [THEN order_trans])
apply (drule_tac [2] order_trans)
@@ -910,16 +910,16 @@
apply auto
done
-subsection {* Proof of the progress property (2) *}
+subsection \<open>Proof of the progress property (2)\<close>
-text{*progress (2), step 1 is @{text System_Follows_ask} and
- @{text System_Follows_rel}*}
+text\<open>progress (2), step 1 is \<open>System_Follows_ask\<close> and
+ \<open>System_Follows_rel\<close>\<close>
-text{*progress (2), step 2; see also @{text System_Increasing_allocRel}*}
+text\<open>progress (2), step 2; see also \<open>System_Increasing_allocRel\<close>\<close>
(* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
lemmas System_Increasing_allocAsk = System_Follows_ask [THEN Follows_Increasing1]
-text{*progress (2), step 3: lifting @{text Client_Bounded} to systemState*}
+text\<open>progress (2), step 3: lifting \<open>Client_Bounded\<close> to systemState\<close>
lemma rename_Client_Bounded: "i : I
==> rename sysOfClient (plam x: I. rename client_map Client) :
UNIV guarantees
@@ -938,18 +938,18 @@
apply blast
done
-text{*progress (2), step 4*}
+text\<open>progress (2), step 4\<close>
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 {* resolve_tac @{context} [Always_Int_rule [@{thm Always_allocAsk_le_ask},
- @{thm System_Bounded_ask}] RS @{thm Always_weaken}] 1 *})
+ apply (tactic \<open>resolve_tac @{context} [Always_Int_rule [@{thm Always_allocAsk_le_ask},
+ @{thm System_Bounded_ask}] RS @{thm Always_weaken}] 1\<close>)
apply (auto dest: set_mono)
done
-text{*progress (2), step 5 is @{text System_Increasing_allocGiv}*}
+text\<open>progress (2), step 5 is \<open>System_Increasing_allocGiv\<close>\<close>
-text{*progress (2), step 6*}
+text\<open>progress (2), step 6\<close>
(* i < Nclients ==> System : Increasing (giv o sub i o client) *)
lemmas System_Increasing_giv = System_Follows_allocGiv [THEN Follows_Increasing1]
@@ -966,7 +966,7 @@
done
-text{*progress (2), step 7*}
+text\<open>progress (2), step 7\<close>
lemma System_Client_Progress:
"System : (INT i : (lessThan Nclients).
INT h. {s. h \<le> (giv o sub i o client) s &
@@ -1007,7 +1007,7 @@
done
-text{*progress (2), step 8: Client i's "release" action is visible system-wide*}
+text\<open>progress (2), step 8: Client i's "release" action is visible system-wide\<close>
lemma System_Alloc_Client_Progress: "i < Nclients
==> System : {s. h \<le> (sub i o allocGiv) s &
h pfixGe (sub i o allocAsk) s}
@@ -1025,9 +1025,9 @@
apply (erule System_lemma3)
done
-text{*Lifting @{text Alloc_Progress} up to the level of systemState*}
+text\<open>Lifting \<open>Alloc_Progress\<close> up to the level of systemState\<close>
-text{*progress (2), step 9*}
+text\<open>progress (2), step 9\<close>
lemma System_Alloc_Progress:
"System : (INT i : (lessThan Nclients).
INT h. {s. h \<le> (sub i o allocAsk) s}
@@ -1043,7 +1043,7 @@
System_Alloc_Client_Progress [simplified sub_apply o_def])
done
-text{*progress (2), step 10 (final result!) *}
+text\<open>progress (2), step 10 (final result!)\<close>
lemma System_Progress: "System : system_progress"
apply (unfold system_progress_def)
apply (cut_tac System_Alloc_Progress)
@@ -1060,7 +1060,7 @@
done
-text{* Some obsolete lemmas *}
+text\<open>Some obsolete lemmas\<close>
lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o
(funPair giv (funPair ask rel))"
@@ -1078,7 +1078,7 @@
apply (auto simp add: o_def)
done
-text{*Could go to Extend.ML*}
+text\<open>Could go to Extend.ML\<close>
lemma bij_fst_inv_inv_eq: "bij f ==> fst (inv (%(x, u). inv f x) z) = f z"
apply (rule fst_inv_equalityI)
apply (rule_tac f = "%z. (f z, h z)" for h in surjI)
--- a/src/HOL/UNITY/Comp/AllocBase.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
Copyright 1998 University of Cambridge
*)
-section{*Common Declarations for Chandy and Charpentier's Allocator*}
+section\<open>Common Declarations for Chandy and Charpentier's Allocator\<close>
theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin
--- a/src/HOL/UNITY/Comp/AllocImpl.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
Copyright 1998 University of Cambridge
*)
-section{*Implementation of a multiple-client allocator from a single-client allocator*}
+section\<open>Implementation of a multiple-client allocator from a single-client allocator\<close>
theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin
@@ -238,7 +238,7 @@
declare o_apply [simp del]
-subsection{*Theorems for Merge*}
+subsection\<open>Theorems for Merge\<close>
context Merge
begin
@@ -307,7 +307,7 @@
end
-subsection{*Theorems for Distributor*}
+subsection\<open>Theorems for Distributor\<close>
context Distrib
begin
@@ -371,7 +371,7 @@
end
-subsection{*Theorems for Allocator*}
+subsection\<open>Theorems for Allocator\<close>
lemma alloc_refinement_lemma:
"!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
--- a/src/HOL/UNITY/Comp/Client.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy Wed May 25 11:50:58 2016 +0200
@@ -3,22 +3,22 @@
Copyright 1998 University of Cambridge
*)
-section{*Distributed Resource Management System: the Client*}
+section\<open>Distributed Resource Management System: the Client\<close>
theory Client imports "../Rename" AllocBase begin
type_synonym
- tokbag = nat --{*tokbags could be multisets...or any ordered type?*}
+ tokbag = nat \<comment>\<open>tokbags could be multisets...or any ordered type?\<close>
record state =
- giv :: "tokbag list" --{*input history: tokens granted*}
- ask :: "tokbag list" --{*output history: tokens requested*}
- rel :: "tokbag list" --{*output history: tokens released*}
- tok :: tokbag --{*current token request*}
+ giv :: "tokbag list" \<comment>\<open>input history: tokens granted\<close>
+ ask :: "tokbag list" \<comment>\<open>output history: tokens requested\<close>
+ rel :: "tokbag list" \<comment>\<open>output history: tokens released\<close>
+ tok :: tokbag \<comment>\<open>current token request\<close>
record 'a state_d =
state +
- dummy :: 'a --{*new variables*}
+ dummy :: 'a \<comment>\<open>new variables\<close>
(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
@@ -82,7 +82,7 @@
by (auto simp add: ok_iff_Allowed Client_def [THEN def_total_prg_Allowed])
-text{*Safety property 1: ask, rel are increasing*}
+text\<open>Safety property 1: ask, rel are increasing\<close>
lemma increasing_ask_rel:
"Client \<in> UNIV guarantees Increasing ask Int Increasing rel"
apply (auto intro!: increasing_imp_Increasing simp add: guar_def preserves_subset_increasing [THEN subsetD])
@@ -93,9 +93,9 @@
declare nth_append [simp] append_one_prefix [simp]
-text{*Safety property 2: the client never requests too many tokens.
+text\<open>Safety property 2: the client never requests too many tokens.
With no Substitution Axiom, we must prove the two invariants
- simultaneously. *}
+ simultaneously.\<close>
lemma ask_bounded_lemma:
"Client ok G
==> Client \<squnion> G \<in>
@@ -109,8 +109,8 @@
apply (cut_tac m = "tok s" in NbT_pos [THEN mod_less_divisor], auto)
done
-text{*export version, with no mention of tok in the postcondition, but
- unfortunately tok must be declared local.*}
+text\<open>export version, with no mention of tok in the postcondition, but
+ unfortunately tok must be declared local.\<close>
lemma ask_bounded:
"Client \<in> UNIV guarantees Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}"
apply (rule guaranteesI)
@@ -119,7 +119,7 @@
done
-text{*** Towards proving the liveness property ***}
+text\<open>** Towards proving the liveness property **\<close>
lemma stable_rel_le_giv: "Client \<in> stable {s. rel s \<le> giv s}"
by (simp add: Client_def, safety, auto)
@@ -189,7 +189,7 @@
apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
done
-text{*Progress property: all tokens that are given will be released*}
+text\<open>Progress property: all tokens that are given will be released\<close>
lemma client_progress:
"Client \<in>
Increasing giv guarantees
@@ -198,19 +198,19 @@
apply (blast intro: client_progress_lemma)
done
-text{*This shows that the Client won't alter other variables in any state
- that it is combined with*}
+text\<open>This shows that the Client won't alter other variables in any state
+ that it is combined with\<close>
lemma client_preserves_dummy: "Client \<in> preserves dummy"
by (simp add: Client_def preserves_def, clarify, safety, auto)
-text{** Obsolete lemmas from first version of the Client **}
+text\<open>* Obsolete lemmas from first version of the Client *\<close>
lemma stable_size_rel_le_giv:
"Client \<in> stable {s. size (rel s) \<le> size (giv s)}"
by (simp add: Client_def, safety, auto)
-text{*clients return the right number of tokens*}
+text\<open>clients return the right number of tokens\<close>
lemma ok_guar_rel_prefix_giv:
"Client \<in> Increasing giv guarantees Always {s. rel s \<le> giv s}"
apply (rule guaranteesI)
--- a/src/HOL/UNITY/Comp/Counter.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy Wed May 25 11:50:58 2016 +0200
@@ -8,7 +8,7 @@
Springer LNCS 1586 (1999), pages 1215-1227.
*)
-section{*A Family of Similar Counters: Original Version*}
+section\<open>A Family of Similar Counters: Original Version\<close>
theory Counter imports "../UNITY_Main" begin
--- a/src/HOL/UNITY/Comp/Counterc.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy Wed May 25 11:50:58 2016 +0200
@@ -11,7 +11,7 @@
Spriner LNCS 1586 (1999), pages 1215-1227.
*)
-section{*A Family of Similar Counters: Version with Compatibility*}
+section\<open>A Family of Similar Counters: Version with Compatibility\<close>
theory Counterc imports "../UNITY_Main" begin
--- a/src/HOL/UNITY/Comp/Priority.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy Wed May 25 11:50:58 2016 +0200
@@ -3,41 +3,41 @@
Copyright 2001 University of Cambridge
*)
-section{*The priority system*}
+section\<open>The priority system\<close>
theory Priority imports PriorityAux begin
-text{*From Charpentier and Chandy,
+text\<open>From Charpentier and Chandy,
Examples of Program Composition Illustrating the Use of Universal Properties
In J. Rolim (editor), Parallel and Distributed Processing,
- Spriner LNCS 1586 (1999), pages 1215-1227.*}
+ Spriner LNCS 1586 (1999), pages 1215-1227.\<close>
type_synonym state = "(vertex*vertex)set"
type_synonym command = "vertex=>(state*state)set"
consts
init :: "(vertex*vertex)set"
- --{* the initial state *}
+ \<comment>\<open>the initial state\<close>
-text{*Following the definitions given in section 4.4 *}
+text\<open>Following the definitions given in section 4.4\<close>
definition highest :: "[vertex, (vertex*vertex)set]=>bool"
where "highest i r \<longleftrightarrow> A i r = {}"
- --{* i has highest priority in r *}
+ \<comment>\<open>i has highest priority in r\<close>
definition lowest :: "[vertex, (vertex*vertex)set]=>bool"
where "lowest i r \<longleftrightarrow> R i r = {}"
- --{* i has lowest priority in r *}
+ \<comment>\<open>i has lowest priority in r\<close>
definition act :: command
where "act i = {(s, s'). s'=reverse i s & highest i s}"
definition Component :: "vertex=>state program"
where "Component i = mk_total_program({init}, {act i}, UNIV)"
- --{* All components start with the same initial state *}
+ \<comment>\<open>All components start with the same initial state\<close>
-text{*Some Abbreviations *}
+text\<open>Some Abbreviations\<close>
definition Highest :: "vertex=>state set"
where "Highest i = {s. highest i s}"
@@ -49,11 +49,11 @@
definition Maximal :: "state set"
- --{* Every ``above'' set has a maximal vertex*}
+ \<comment>\<open>Every ``above'' set has a maximal vertex\<close>
where "Maximal = (\<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i s. highest j s)})"
definition Maximal' :: "state set"
- --{* Maximal vertex: equivalent definition*}
+ \<comment>\<open>Maximal vertex: equivalent definition\<close>
where "Maximal' = (\<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j))"
@@ -77,18 +77,18 @@
-subsection{*Component correctness proofs*}
+subsection\<open>Component correctness proofs\<close>
-text{* neighbors is stable *}
+text\<open>neighbors is stable\<close>
lemma Component_neighbors_stable: "Component i \<in> stable {s. neighbors k s = n}"
by (simp add: Component_def, safety, auto)
-text{* property 4 *}
+text\<open>property 4\<close>
lemma Component_waits_priority: "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}"
by (simp add: Component_def, safety)
-text{* property 5: charpentier and Chandy mistakenly express it as
- 'transient Highest i'. Consider the case where i has neighbors *}
+text\<open>property 5: charpentier and Chandy mistakenly express it as
+ 'transient Highest i'. Consider the case where i has neighbors\<close>
lemma Component_yields_priority:
"Component i: {s. neighbors i s \<noteq> {}} Int Highest i
ensures - Highest i"
@@ -96,23 +96,23 @@
apply (ensures_tac "act i", blast+)
done
-text{* or better *}
+text\<open>or better\<close>
lemma Component_yields_priority': "Component i \<in> Highest i ensures Lowest i"
apply (simp add: Component_def)
apply (ensures_tac "act i", blast+)
done
-text{* property 6: Component doesn't introduce cycle *}
+text\<open>property 6: Component doesn't introduce cycle\<close>
lemma Component_well_behaves: "Component i \<in> Highest i co Highest i Un Lowest i"
by (simp add: Component_def, safety, fast)
-text{* property 7: local axiom *}
+text\<open>property 7: local axiom\<close>
lemma locality: "Component i \<in> stable {s. \<forall>j k. j\<noteq>i & k\<noteq>i--> ((j,k):s) = b j k}"
by (simp add: Component_def, safety)
-subsection{*System properties*}
-text{* property 8: strictly universal *}
+subsection\<open>System properties\<close>
+text\<open>property 8: strictly universal\<close>
lemma Safety: "system \<in> stable Safety"
apply (unfold Safety_def)
@@ -120,12 +120,12 @@
apply (simp add: system_def, safety, fast)
done
-text{* property 13: universal *}
+text\<open>property 13: universal\<close>
lemma p13: "system \<in> {s. s = q} co {s. s=q} Un {s. \<exists>i. derive i q s}"
by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, blast)
-text{* property 14: the 'above set' of a Component that hasn't got
- priority doesn't increase *}
+text\<open>property 14: the 'above set' of a Component that hasn't got
+ priority doesn't increase\<close>
lemma above_not_increase:
"system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}"
apply (insert reach_lemma [of concl: j])
@@ -142,7 +142,7 @@
-text{* p15: universal property: all Components well behave *}
+text\<open>p15: universal property: all Components well behave\<close>
lemma system_well_behaves: "system \<in> Highest i co Highest i Un Lowest i"
by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, auto)
@@ -166,23 +166,23 @@
apply (drule above_lemma_b, auto)
done
-text{* property 17: original one is an invariant *}
+text\<open>property 17: original one is an invariant\<close>
lemma Acyclic_Maximal_stable: "system \<in> stable (Acyclic Int Maximal)"
by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable)
-text{* property 5: existential property *}
+text\<open>property 5: existential property\<close>
lemma Highest_leadsTo_Lowest: "system \<in> Highest i leadsTo Lowest i"
apply (simp add: system_def Component_def mk_total_program_def totalize_JN)
apply (ensures_tac "act i", auto)
done
-text{* a lowest i can never be in any abover set *}
+text\<open>a lowest i can never be in any abover set\<close>
lemma Lowest_above_subset: "Lowest i <= (\<Inter>k. {s. i\<notin>above k s})"
by (auto simp add: image0_r_iff_image0_trancl trancl_converse)
-text{* property 18: a simpler proof than the original, one which uses psp *}
+text\<open>property 18: a simpler proof than the original, one which uses psp\<close>
lemma Highest_escapes_above: "system \<in> Highest i leadsTo (\<Inter>k. {s. i\<notin>above k s})"
apply (rule leadsTo_weaken_R)
apply (rule_tac [2] Lowest_above_subset)
@@ -193,9 +193,9 @@
"system \<in> Highest j Int {s. j \<in> above i s} leadsTo {s. j\<notin>above i s}"
by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower])
-subsection{*The main result: above set decreases*}
+subsection\<open>The main result: above set decreases\<close>
-text{* The original proof of the following formula was wrong *}
+text\<open>The original proof of the following formula was wrong\<close>
lemma Highest_iff_above0: "Highest i = {s. above i s ={}}"
by (auto simp add: image0_trancl_iff_image0_r)
@@ -253,10 +253,10 @@
done
-text{*We have proved all (relevant) theorems given in the paper. We didn't
+text\<open>We have proved all (relevant) theorems given in the paper. We didn't
assume any thing about the relation @{term r}. It is not necessary that
@{term r} be a priority relation as assumed in the original proof. It
-suffices that we start from a state which is finite and acyclic.*}
+suffices that we start from a state which is finite and acyclic.\<close>
end
--- a/src/HOL/UNITY/Comp/PriorityAux.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy Wed May 25 11:50:58 2016 +0200
@@ -13,11 +13,11 @@
definition symcl :: "(vertex*vertex)set=>(vertex*vertex)set" where
"symcl r == r \<union> (r^-1)"
- --{* symmetric closure: removes the orientation of a relation*}
+ \<comment>\<open>symmetric closure: removes the orientation of a relation\<close>
definition neighbors :: "[vertex, (vertex*vertex)set]=>vertex set" where
"neighbors i r == ((r \<union> r^-1)``{i}) - {i}"
- --{* Neighbors of a vertex i *}
+ \<comment>\<open>Neighbors of a vertex i\<close>
definition R :: "[vertex, (vertex*vertex)set]=>vertex set" where
"R i r == r``{i}"
@@ -27,7 +27,7 @@
definition reach :: "[vertex, (vertex*vertex)set]=> vertex set" where
"reach i r == (r^+)``{i}"
- --{* reachable and above vertices: the original notation was R* and A* *}
+ \<comment>\<open>reachable and above vertices: the original notation was R* and A*\<close>
definition above :: "[vertex, (vertex*vertex)set]=> vertex set" where
"above i r == ((r^-1)^+)``{i}"
@@ -36,28 +36,28 @@
"reverse i r == (r - {(x,y). x=i | y=i} \<inter> r) \<union> ({(x,y). x=i|y=i} \<inter> r)^-1"
definition derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" where
- --{* The original definition *}
+ \<comment>\<open>The original definition\<close>
"derive1 i r q == symcl r = symcl q &
(\<forall>k k'. k\<noteq>i & k'\<noteq>i -->((k,k'):r) = ((k,k'):q)) &
A i r = {} & R i q = {}"
definition derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" where
- --{* Our alternative definition *}
+ \<comment>\<open>Our alternative definition\<close>
"derive i r q == A i r = {} & (q = reverse i r)"
axiomatization where
finite_vertex_univ: "finite (UNIV :: vertex set)"
- --{* we assume that the universe of vertices is finite *}
+ \<comment>\<open>we assume that the universe of vertices is finite\<close>
declare derive_def [simp] derive1_def [simp] symcl_def [simp]
A_def [simp] R_def [simp]
above_def [simp] reach_def [simp]
reverse_def [simp] neighbors_def [simp]
-text{*All vertex sets are finite*}
+text\<open>All vertex sets are finite\<close>
declare finite_subset [OF subset_UNIV finite_vertex_univ, iff]
-text{* and relatons over vertex are finite too *}
+text\<open>and relatons over vertex are finite too\<close>
lemmas finite_UNIV_Prod =
finite_Prod_UNIV [OF finite_vertex_univ finite_vertex_univ]
--- a/src/HOL/UNITY/Comp/Progress.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Progress.thy Wed May 25 11:50:58 2016 +0200
@@ -5,12 +5,12 @@
David Meier's thesis
*)
-section{*Progress Set Examples*}
+section\<open>Progress Set Examples\<close>
theory Progress imports "../UNITY_Main" begin
-subsection {*The Composition of Two Single-Assignment Programs*}
-text{*Thesis Section 4.4.2*}
+subsection \<open>The Composition of Two Single-Assignment Programs\<close>
+text\<open>Thesis Section 4.4.2\<close>
definition FF :: "int program" where
"FF = mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
@@ -18,7 +18,7 @@
definition GG :: "int program" where
"GG = mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
-subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
+subsubsection \<open>Calculating @{term "wens_set FF (atLeast k)"}\<close>
lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV"
by force
@@ -62,7 +62,7 @@
apply (simp add: wens_single_finite_FF)
done
-subsubsection {*Proving @{term "FF \<in> UNIV leadsTo atLeast (k::int)"}*}
+subsubsection \<open>Proving @{term "FF \<in> UNIV leadsTo atLeast (k::int)"}\<close>
lemma atLeast_ensures: "FF \<in> atLeast (k - 1) ensures atLeast (k::int)"
apply (simp add: Progress.wens_FF [symmetric] wens_ensures)
@@ -86,7 +86,7 @@
apply (rule leadsTo_UN [OF atLeast_leadsTo])
done
-text{*Result (4.39): Applying the leadsTo-Join Theorem*}
+text\<open>Result (4.39): Applying the leadsTo-Join Theorem\<close>
theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)"
apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
apply simp
--- a/src/HOL/UNITY/Constrains.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Constrains.thy Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
Weak safety relations: restricted to the set of reachable states.
*)
-section{*Weak Safety*}
+section\<open>Weak Safety\<close>
theory Constrains imports UNITY begin
@@ -50,7 +50,7 @@
"Increasing f == \<Inter>z. Stable {s. z \<le> f s}"
-subsection{*traces and reachable*}
+subsection\<open>traces and reachable\<close>
lemma reachable_equiv_traces:
"reachable F = {s. \<exists>evs. (s,evs) \<in> traces (Init F) (Acts F)}"
@@ -82,7 +82,7 @@
done
-subsection{*Co*}
+subsection\<open>Co\<close>
(*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
lemmas constrains_reachable_Int =
@@ -185,7 +185,7 @@
done
-subsection{*Stable*}
+subsection\<open>Stable\<close>
(*Useful because there's no Stable_weaken. [Tanja Vos]*)
lemma Stable_eq: "[| F \<in> Stable A; A = B |] ==> F \<in> Stable B"
@@ -239,7 +239,7 @@
-subsection{*Increasing*}
+subsection\<open>Increasing\<close>
lemma IncreasingD:
"F \<in> Increasing f ==> F \<in> Stable {s. x \<le> f s}"
@@ -265,7 +265,7 @@
lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff]
-subsection{*The Elimination Theorem*}
+subsection\<open>The Elimination Theorem\<close>
(*The "free" m has become universally quantified! Should the premise be !!m
instead of \<forall>m ? Would make it harder to use in forward proof.*)
@@ -282,7 +282,7 @@
by (unfold Constrains_def constrains_def, blast)
-subsection{*Specialized laws for handling Always*}
+subsection\<open>Specialized laws for handling Always\<close>
(** Natural deduction rules for "Always A" **)
@@ -339,7 +339,7 @@
by (auto simp add: Always_eq_includes_reachable)
-subsection{*"Co" rules involving Always*}
+subsection\<open>"Co" rules involving Always\<close>
lemma Always_Constrains_pre:
"F \<in> Always INV ==> (F \<in> (INV \<inter> A) Co A') = (F \<in> A Co A')"
@@ -390,7 +390,7 @@
lemmas Always_thin = thin_rl [of "F \<in> Always A"]
-subsection{*Totalize*}
+subsection\<open>Totalize\<close>
lemma reachable_imp_reachable_tot:
"s \<in> reachable F ==> s \<in> reachable (totalize F)"
--- a/src/HOL/UNITY/Detects.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Detects.thy Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
*)
-section{*The Detects Relation*}
+section\<open>The Detects Relation\<close>
theory Detects imports FP SubstAx begin
--- a/src/HOL/UNITY/ELT.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/ELT.thy Wed May 25 11:50:58 2016 +0200
@@ -21,7 +21,7 @@
monos Pow_mono
*)
-section{*Progress Under Allowable Sets*}
+section\<open>Progress Under Allowable Sets\<close>
theory ELT imports Project begin
--- a/src/HOL/UNITY/Extend.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Extend.thy Wed May 25 11:50:58 2016 +0200
@@ -7,7 +7,7 @@
function g (forgotten) maps the extended state to the "extending part"
*)
-section{*Extending State Sets*}
+section\<open>Extending State Sets\<close>
theory Extend imports Guar begin
@@ -67,7 +67,7 @@
(** These we prove OUTSIDE the locale. **)
-subsection{*Restrict*}
+subsection\<open>Restrict\<close>
(*MOVE to Relation.thy?*)
lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x \<in> A)"
@@ -130,7 +130,7 @@
by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h)
-subsection{*Trivial properties of f, g, h*}
+subsection\<open>Trivial properties of f, g, h\<close>
context Extend
begin
@@ -167,7 +167,7 @@
end
-subsection{*@{term extend_set}: basic properties*}
+subsection\<open>@{term extend_set}: basic properties\<close>
lemma project_set_iff [iff]:
"(x \<in> project_set h C) = (\<exists>y. h(x,y) \<in> C)"
@@ -215,7 +215,7 @@
apply (auto simp add: split_extended_all)
done
-subsection{*@{term project_set}: basic properties*}
+subsection\<open>@{term project_set}: basic properties\<close>
(*project_set is simply image!*)
lemma project_set_eq: "project_set h C = f ` C"
@@ -226,7 +226,7 @@
by (auto simp add: split_extended_all)
-subsection{*More laws*}
+subsection\<open>More laws\<close>
(*Because A and B could differ on the "other" part of the state,
cannot generalize to
@@ -262,7 +262,7 @@
by (auto simp: extend_set_def)
-subsection{*@{term extend_act}*}
+subsection\<open>@{term extend_act}\<close>
(*Can't strengthen it to
((h(s,y), h(s',y')) \<in> extend_act h act) = ((s, s') \<in> act & y=y')
@@ -318,9 +318,9 @@
unfolding project_act_def by (force simp add: split_extended_all)
-subsection{*extend*}
+subsection\<open>extend\<close>
-text{*Basic properties*}
+text\<open>Basic properties\<close>
lemma (in -) Init_extend [simp]:
"Init (extend h F) = extend_set h (Init F)"
@@ -431,7 +431,7 @@
lemma all_total_extend: "all_total F ==> all_total (extend h F)"
by (simp add: all_total_def Domain_extend_act)
-subsection{*Safety: co, stable*}
+subsection\<open>Safety: co, stable\<close>
lemma extend_constrains:
"(extend h F \<in> (extend_set h A) co (extend_set h B)) =
@@ -457,7 +457,7 @@
by (simp add: stable_def extend_constrains_project_set)
-subsection{*Weak safety primitives: Co, Stable*}
+subsection\<open>Weak safety primitives: Co, Stable\<close>
lemma reachable_extend_f: "p \<in> reachable (extend h F) ==> f p \<in> reachable F"
by (induct set: reachable) (auto intro: reachable.intros simp add: extend_act_def image_iff)
@@ -539,7 +539,7 @@
by (simp add: stable_def project_constrains_project_set)
-subsection{*Progress: transient, ensures*}
+subsection\<open>Progress: transient, ensures\<close>
lemma extend_transient:
"(extend h F \<in> transient (extend_set h A)) = (F \<in> transient A)"
@@ -560,7 +560,7 @@
apply (simp add: leadsTo_UN extend_set_Union)
done
-subsection{*Proving the converse takes some doing!*}
+subsection\<open>Proving the converse takes some doing!\<close>
lemma slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
by (simp add: slice_def)
@@ -621,7 +621,7 @@
extend_set_Int_distrib [symmetric])
-subsection{*preserves*}
+subsection\<open>preserves\<close>
lemma project_preserves_I:
"G \<in> preserves (v o f) ==> project h C G \<in> preserves v"
@@ -642,7 +642,7 @@
constrains_def g_def)
-subsection{*Guarantees*}
+subsection\<open>Guarantees\<close>
lemma project_extend_Join: "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
apply (rule program_equalityI)
--- a/src/HOL/UNITY/FP.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/FP.thy Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-section{*Fixed Point of a Program*}
+section\<open>Fixed Point of a Program\<close>
theory FP imports UNITY begin
--- a/src/HOL/UNITY/Follows.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Follows.thy Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
Copyright 1998 University of Cambridge
*)
-section{*The Follows Relation of Charpentier and Sivilotte*}
+section\<open>The Follows Relation of Charpentier and Sivilotte\<close>
theory Follows
imports SubstAx ListOrder "~~/src/HOL/Library/Multiset"
@@ -62,7 +62,7 @@
done
-subsection{*Destruction rules*}
+subsection\<open>Destruction rules\<close>
lemma Follows_Increasing1: "F \<in> f Fols g ==> F \<in> Increasing f"
by (simp add: Follows_def)
@@ -118,7 +118,7 @@
done
-subsection{*Union properties (with the subset ordering)*}
+subsection\<open>Union properties (with the subset ordering)\<close>
(*Can replace "Un" by any sup. But existing max only works for linorders.*)
@@ -174,7 +174,7 @@
done
-subsection{*Multiset union properties (with the multiset ordering)*}
+subsection\<open>Multiset union properties (with the multiset ordering)\<close>
(*TODO: remove when multiset is of sort ord again*)
instantiation multiset :: (order) ordered_ab_semigroup_add
begin
--- a/src/HOL/UNITY/Guar.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Guar.thy Wed May 25 11:50:58 2016 +0200
@@ -10,7 +10,7 @@
Fifth International Conference on Mathematics of Program, 2000.
*)
-section{*Guarantees Specifications*}
+section\<open>Guarantees Specifications\<close>
theory Guar
imports Comp
@@ -19,8 +19,8 @@
instance program :: (type) order
by standard (auto simp add: program_less_le dest: component_antisym intro: component_trans)
-text{*Existential and Universal properties. I formalize the two-program
- case, proving equivalence with Chandy and Sanders's n-ary definitions*}
+text\<open>Existential and Universal properties. I formalize the two-program
+ case, proving equivalence with Chandy and Sanders's n-ary definitions\<close>
definition ex_prop :: "'a program set => bool" where
"ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F\<squnion>G) \<in> X"
@@ -36,7 +36,7 @@
SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F\<squnion>G \<in> X))"
-text{*Guarantees properties*}
+text\<open>Guarantees properties\<close>
definition guar :: "['a program set, 'a program set] => 'a program set" (infixl "guarantees" 55) where
(*higher than membership, lower than Co*)
@@ -73,7 +73,7 @@
by (auto intro: ok_sym simp add: OK_iff_ok)
-subsection{*Existential Properties*}
+subsection\<open>Existential Properties\<close>
lemma ex1:
assumes "ex_prop X" and "finite GG"
@@ -110,7 +110,7 @@
done
-subsection{*Universal Properties*}
+subsection\<open>Universal Properties\<close>
lemma uv1:
assumes "uv_prop X"
@@ -143,7 +143,7 @@
(\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)"
by (blast intro: uv1 uv2)
-subsection{*Guarantees*}
+subsection\<open>Guarantees\<close>
lemma guaranteesI:
"(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y) ==> F \<in> X guarantees Y"
@@ -191,7 +191,7 @@
done
-subsection{*Distributive Laws. Re-Orient to Perform Miniscoping*}
+subsection\<open>Distributive Laws. Re-Orient to Perform Miniscoping\<close>
lemma guarantees_UN_left:
"(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)"
@@ -252,7 +252,7 @@
by (unfold guar_def, blast)
-subsection{*Guarantees: Additional Laws (by lcp)*}
+subsection\<open>Guarantees: Additional Laws (by lcp)\<close>
lemma guarantees_Join_Int:
"[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |]
@@ -297,7 +297,7 @@
done
-subsection{*Guarantees Laws for Breaking Down the Program (by lcp)*}
+subsection\<open>Guarantees Laws for Breaking Down the Program (by lcp)\<close>
lemma guarantees_Join_I1:
"[| F \<in> X guarantees Y; F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
@@ -440,7 +440,7 @@
apply (simp add: ok_commute Join_ac)
done
-text{* Equivalence with the other definition of wx *}
+text\<open>Equivalence with the other definition of wx\<close>
lemma wx_equiv: "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G) \<in> X}"
apply (unfold wx_def, safe)
@@ -453,9 +453,9 @@
done
-text{* Propositions 7 to 11 are about this second definition of wx.
+text\<open>Propositions 7 to 11 are about this second definition of wx.
They are the same as the ones proved for the first definition of wx,
- by equivalence *}
+ by equivalence\<close>
(* Proposition 12 *)
(* Main result of the paper *)
--- a/src/HOL/UNITY/Lift_prog.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
lift_prog, etc: replication of components and arrays of processes.
*)
-section{*Replication of Components*}
+section\<open>Replication of Components\<close>
theory Lift_prog imports Rename begin
@@ -44,7 +44,7 @@
apply (auto split add: nat_diff_split)
done
-subsection{*Injectiveness proof*}
+subsection\<open>Injectiveness proof\<close>
lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
by (drule_tac x = i in fun_cong, simp)
@@ -77,7 +77,7 @@
apply (rule inj_onI, auto)
done
-subsection{*Surjectiveness proof*}
+subsection\<open>Surjectiveness proof\<close>
lemma lift_map_drop_map_eq [simp]: "!!s. lift_map i (drop_map i s) = s"
apply (unfold lift_map_def drop_map_def)
@@ -121,7 +121,7 @@
else insert_map j t (f(i - Suc 0 := s)))"
apply (rule ext)
apply (simp split add: nat_diff_split)
- txt{*This simplification is VERY slow*}
+ txt\<open>This simplification is VERY slow\<close>
done
lemma insert_map_eq_diff:
@@ -140,7 +140,7 @@
done
-subsection{*The Operator @{term lift_set}*}
+subsection\<open>The Operator @{term lift_set}\<close>
lemma lift_set_empty [simp]: "lift_set i {} = {}"
by (unfold lift_set_def, auto)
@@ -170,7 +170,7 @@
done
-subsection{*The Lattice Operations*}
+subsection\<open>The Lattice Operations\<close>
lemma bij_lift [iff]: "bij (lift i)"
by (simp add: lift_def)
@@ -184,7 +184,7 @@
lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
by (simp add: lift_def)
-subsection{*Safety: constrains, stable, invariant*}
+subsection\<open>Safety: constrains, stable, invariant\<close>
lemma lift_constrains:
"(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)"
@@ -210,7 +210,7 @@
"(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)"
by (simp add: lift_def lift_set_def rename_Always)
-subsection{*Progress: transient, ensures*}
+subsection\<open>Progress: transient, ensures\<close>
lemma lift_transient:
"(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)"
@@ -333,7 +333,7 @@
done
-subsection{*Lemmas to Handle Function Composition (o) More Consistently*}
+subsection\<open>Lemmas to Handle Function Composition (o) More Consistently\<close>
(*Lets us prove one version of a theorem and store others*)
lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
@@ -353,9 +353,9 @@
done
-subsection{*More lemmas about extend and project*}
+subsection\<open>More lemmas about extend and project\<close>
-text{*They could be moved to theory Extend or Project*}
+text\<open>They could be moved to theory Extend or Project\<close>
lemma extend_act_extend_act:
"extend_act h' (extend_act h act) =
@@ -375,7 +375,7 @@
by (simp add: extend_act_def project_act_def, blast)
-subsection{*OK and "lift"*}
+subsection\<open>OK and "lift"\<close>
lemma act_in_UNION_preserves_fst:
"act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
--- a/src/HOL/UNITY/ListOrder.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/ListOrder.thy Wed May 25 11:50:58 2016 +0200
@@ -10,7 +10,7 @@
Also overloads <= and < for lists!
*)
-section {*The Prefix Ordering on Lists*}
+section \<open>The Prefix Ordering on Lists\<close>
theory ListOrder
imports Main
@@ -57,7 +57,7 @@
"xs pfixGe ys == (xs,ys) : genPrefix Ge"
-subsection{*preliminary lemmas*}
+subsection\<open>preliminary lemmas\<close>
lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r"
by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto)
@@ -84,7 +84,7 @@
by (blast intro: genPrefix.prepend)
-subsection{*genPrefix is a partial order*}
+subsection\<open>genPrefix is a partial order\<close>
lemma refl_genPrefix: "refl r ==> refl (genPrefix r)"
apply (unfold refl_on_def, auto)
@@ -176,7 +176,7 @@
by (blast intro: antisymI genPrefix_antisym)
-subsection{*recursion equations*}
+subsection\<open>recursion equations\<close>
lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
by (induct xs) auto
@@ -216,7 +216,7 @@
apply (erule genPrefix.induct)
apply blast
apply simp
-txt{*Append case is hardest*}
+txt\<open>Append case is hardest\<close>
apply simp
apply (frule genPrefix_length_le [THEN le_imp_less_or_eq])
apply (erule disjE)
@@ -258,7 +258,7 @@
done
-subsection{*The type of lists is partially ordered*}
+subsection\<open>The type of lists is partially ordered\<close>
declare refl_Id [iff]
antisym_Id [iff]
@@ -376,7 +376,7 @@
shows "xs <= zs \<Longrightarrow> ys <= zs \<Longrightarrow> xs <= ys | ys <= xs"
by (induct zs rule: rev_induct) auto
-subsection{*pfixLe, pfixGe: properties inherited from the translations*}
+subsection\<open>pfixLe, pfixGe: properties inherited from the translations\<close>
(** pfixLe **)
--- a/src/HOL/UNITY/PPROD.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/PPROD.thy Wed May 25 11:50:58 2016 +0200
@@ -68,7 +68,7 @@
PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
by (simp add: JN_transient PLam_def)
-text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
+text\<open>This holds because the @{term "F j"} cannot change @{term "lift_set i"}\<close>
lemma PLam_ensures:
"[| i \<in> I; F i \<in> (A \<times> UNIV) ensures (B \<times> UNIV);
\<forall>j. F j \<in> preserves snd |]
@@ -114,11 +114,11 @@
(*** guarantees properties ***)
-text{*This rule looks unsatisfactory because it refers to @{term lift}.
+text\<open>This rule looks unsatisfactory because it refers to @{term lift}.
One must use
- @{text lift_guarantees_eq_lift_inv} to rewrite the first subgoal and
- something like @{text lift_preserves_sub} to rewrite the third. However
- there's no obvious alternative for the third premise.*}
+ \<open>lift_guarantees_eq_lift_inv\<close> to rewrite the first subgoal and
+ something like \<open>lift_preserves_sub\<close> to rewrite the third. However
+ there's no obvious alternative for the third premise.\<close>
lemma guarantees_PLam_I:
"[| lift i (F i): X guarantees Y; i \<in> I;
OK I (%i. lift i (F i)) |]
--- a/src/HOL/UNITY/ProgressSets.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy Wed May 25 11:50:58 2016 +0200
@@ -13,19 +13,19 @@
Swiss Federal Institute of Technology Zurich (1997)
*)
-section{*Progress Sets*}
+section\<open>Progress Sets\<close>
theory ProgressSets imports Transformers begin
-subsection {*Complete Lattices and the Operator @{term cl}*}
+subsection \<open>Complete Lattices and the Operator @{term cl}\<close>
definition lattice :: "'a set set => bool" where
- --{*Meier calls them closure sets, but they are just complete lattices*}
+ \<comment>\<open>Meier calls them closure sets, but they are just complete lattices\<close>
"lattice L ==
(\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)"
definition cl :: "['a set set, 'a set] => 'a set" where
- --{*short for ``closure''*}
+ \<comment>\<open>short for ``closure''\<close>
"cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}"
lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L"
@@ -59,8 +59,8 @@
lemma lattice_stable: "lattice {X. F \<in> stable X}"
by (simp add: lattice_def stable_def constrains_def, blast)
-text{*The next three results state that @{term "cl L r"} is the minimal
- element of @{term L} that includes @{term r}.*}
+text\<open>The next three results state that @{term "cl L r"} is the minimal
+ element of @{term L} that includes @{term r}.\<close>
lemma cl_in_lattice: "lattice L ==> cl L r \<in> L"
apply (simp add: lattice_def cl_def)
apply (erule conjE)
@@ -70,18 +70,18 @@
lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c"
by (force simp add: cl_def)
-text{*The next three lemmas constitute assertion (4.61)*}
+text\<open>The next three lemmas constitute assertion (4.61)\<close>
lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'"
by (simp add: cl_def, blast)
lemma subset_cl: "r \<subseteq> cl L r"
by (simp add: cl_def le_Inf_iff)
-text{*A reformulation of @{thm subset_cl}*}
+text\<open>A reformulation of @{thm subset_cl}\<close>
lemma clI: "x \<in> r ==> x \<in> cl L r"
by (simp add: cl_def, blast)
-text{*A reformulation of @{thm cl_least}*}
+text\<open>A reformulation of @{thm cl_least}\<close>
lemma clD: "[|c \<in> cl L r; B \<in> L; r \<subseteq> B|] ==> c \<in> B"
by (force simp add: cl_def)
@@ -120,7 +120,7 @@
lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
by (simp add: cl_ident UNIV_in_lattice)
-text{*Assertion (4.62)*}
+text\<open>Assertion (4.62)\<close>
lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)"
apply (rule iffI)
apply (erule subst)
@@ -132,9 +132,9 @@
by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
-subsection {*Progress Sets and the Main Lemma*}
-text{*A progress set satisfies certain closure conditions and is a
-simple way of including the set @{term "wens_set F B"}.*}
+subsection \<open>Progress Sets and the Main Lemma\<close>
+text\<open>A progress set satisfies certain closure conditions and is a
+simple way of including the set @{term "wens_set F B"}.\<close>
definition closed :: "['a program, 'a set, 'a set, 'a set set] => bool" where
"closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
@@ -149,15 +149,15 @@
==> T \<inter> (B \<union> wp act M) \<in> L"
by (simp add: closed_def)
-text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
-and @{term m} by @{term X}. *}
+text\<open>Note: the formalization below replaces Meier's @{term q} by @{term B}
+and @{term m} by @{term X}.\<close>
-text{*Part of the proof of the claim at the bottom of page 97. It's
+text\<open>Part of the proof of the claim at the bottom of page 97. It's
proved separately because the argument requires a generalization over
-all @{term "act \<in> Acts F"}.*}
+all @{term "act \<in> Acts F"}.\<close>
lemma lattice_awp_lemma:
- assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
- and BsubX: "B \<subseteq> X" --{*holds in inductive step*}
+ assumes TXC: "T\<inter>X \<in> C" \<comment>\<open>induction hypothesis in theorem below\<close>
+ and BsubX: "B \<subseteq> X" \<comment>\<open>holds in inductive step\<close>
and latt: "lattice C"
and TC: "T \<in> C"
and BC: "B \<in> C"
@@ -173,10 +173,10 @@
apply (blast intro: Un_in_lattice latt cl_in_lattice TXC)
done
-text{*Remainder of the proof of the claim at the bottom of page 97.*}
+text\<open>Remainder of the proof of the claim at the bottom of page 97.\<close>
lemma lattice_lemma:
- assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
- and BsubX: "B \<subseteq> X" --{*holds in inductive step*}
+ assumes TXC: "T\<inter>X \<in> C" \<comment>\<open>induction hypothesis in theorem below\<close>
+ and BsubX: "B \<subseteq> X" \<comment>\<open>holds in inductive step\<close>
and act: "act \<in> Acts F"
and latt: "lattice C"
and TC: "T \<in> C"
@@ -202,9 +202,9 @@
done
-text{*Induction step for the main lemma*}
+text\<open>Induction step for the main lemma\<close>
lemma progress_induction_step:
- assumes TXC: "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
+ assumes TXC: "T\<inter>X \<in> C" \<comment>\<open>induction hypothesis in theorem below\<close>
and act: "act \<in> Acts F"
and Xwens: "X \<in> wens_set F B"
and latt: "lattice C"
@@ -242,25 +242,25 @@
by (rule cl_subset_in_lattice [OF cl_subset latt])
qed
-text{*Proved on page 96 of Meier's thesis. The special case when
+text\<open>Proved on page 96 of Meier's thesis. The special case when
@{term "T=UNIV"} states that every progress set for the program @{term F}
- and set @{term B} includes the set @{term "wens_set F B"}.*}
+ and set @{term B} includes the set @{term "wens_set F B"}.\<close>
lemma progress_set_lemma:
"[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
apply (simp add: progress_set_def, clarify)
apply (erule wens_set.induct)
- txt{*Base*}
+ txt\<open>Base\<close>
apply (simp add: Int_in_lattice)
- txt{*The difficult @{term wens} case*}
+ txt\<open>The difficult @{term wens} case\<close>
apply (simp add: progress_induction_step)
-txt{*Disjunctive case*}
+txt\<open>Disjunctive case\<close>
apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C")
apply simp
apply (blast intro: UN_in_lattice)
done
-subsection {*The Progress Set Union Theorem*}
+subsection \<open>The Progress Set Union Theorem\<close>
lemma closed_mono:
assumes BB': "B \<subseteq> B'"
@@ -306,22 +306,22 @@
done
-subsection {*Some Progress Sets*}
+subsection \<open>Some Progress Sets\<close>
lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
by (simp add: progress_set_def lattice_def closed_def)
-subsubsection {*Lattices and Relations*}
-text{*From Meier's thesis, section 4.5.3*}
+subsubsection \<open>Lattices and Relations\<close>
+text\<open>From Meier's thesis, section 4.5.3\<close>
definition relcl :: "'a set set => ('a * 'a) set" where
- -- {*Derived relation from a lattice*}
+ \<comment> \<open>Derived relation from a lattice\<close>
"relcl L == {(x,y). y \<in> cl L {x}}"
definition latticeof :: "('a * 'a) set => 'a set set" where
- -- {*Derived lattice from a relation: the set of upwards-closed sets*}
+ \<comment> \<open>Derived lattice from a relation: the set of upwards-closed sets\<close>
"latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}"
@@ -350,7 +350,7 @@
apply (simp only: UN_in_lattice)
done
-text{*Equation (4.71) of Meier's thesis. He gives no proof.*}
+text\<open>Equation (4.71) of Meier's thesis. He gives no proof.\<close>
lemma cl_latticeof:
"[|refl r; trans r|]
==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}"
@@ -362,7 +362,7 @@
apply (unfold cl_def, blast)
done
-text{*Related to (4.71).*}
+text\<open>Related to (4.71).\<close>
lemma cl_eq_Collect_relcl:
"lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}"
apply (cut_tac UN_singleton [of X])
@@ -370,7 +370,7 @@
apply (force simp only: relcl_def cl_UN)
done
-text{*Meier's theorem of section 4.5.3*}
+text\<open>Meier's theorem of section 4.5.3\<close>
theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L"
apply (rule equalityI)
prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify)
@@ -394,14 +394,14 @@
by (simp add: relcl_def cl_latticeof)
-subsubsection {*Decoupling Theorems*}
+subsubsection \<open>Decoupling Theorems\<close>
definition decoupled :: "['a program, 'a program] => bool" where
"decoupled F G ==
\<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)"
-text{*Rao's Decoupling Theorem*}
+text\<open>Rao's Decoupling Theorem\<close>
lemma stableco: "F \<in> stable A ==> F \<in> A-B co A"
by (simp add: stable_def constrains_def, blast)
@@ -421,7 +421,7 @@
qed
-text{*Rao's Weak Decoupling Theorem*}
+text\<open>Rao's Weak Decoupling Theorem\<close>
theorem weak_decoupling:
assumes leadsTo: "F \<in> A leadsTo B"
and stable: "F\<squnion>G \<in> stable B"
@@ -439,12 +439,12 @@
thus ?thesis by simp
qed
-text{*The ``Decoupling via @{term G'} Union Theorem''*}
+text\<open>The ``Decoupling via @{term G'} Union Theorem''\<close>
theorem decoupling_via_aux:
assumes leadsTo: "F \<in> A leadsTo B"
and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B"
and GG': "G \<le> G'"
- --{*Beware! This is the converse of the refinement relation!*}
+ \<comment>\<open>Beware! This is the converse of the refinement relation!\<close>
shows "F\<squnion>G \<in> A leadsTo B"
proof -
from prog have stable: "G' \<in> stable B"
@@ -456,16 +456,16 @@
qed
-subsection{*Composition Theorems Based on Monotonicity and Commutativity*}
+subsection\<open>Composition Theorems Based on Monotonicity and Commutativity\<close>
-subsubsection{*Commutativity of @{term "cl L"} and assignment.*}
+subsubsection\<open>Commutativity of @{term "cl L"} and assignment.\<close>
definition commutes :: "['a program, 'a set, 'a set, 'a set set] => bool" where
"commutes F T B L ==
\<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M -->
cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"
-text{*From Meier's thesis, section 4.5.6*}
+text\<open>From Meier's thesis, section 4.5.6\<close>
lemma commutativity1_lemma:
assumes commutes: "commutes F T B L"
and lattice: "lattice L"
@@ -484,7 +484,7 @@
apply (blast intro: rev_subsetD [OF _ wp_mono])
done
-text{*Version packaged with @{thm progress_set_Union}*}
+text\<open>Version packaged with @{thm progress_set_Union}\<close>
lemma commutativity1:
assumes leadsTo: "F \<in> A leadsTo B"
and lattice: "lattice L"
@@ -499,7 +499,7 @@
-text{*Possibly move to Relation.thy, after @{term single_valued}*}
+text\<open>Possibly move to Relation.thy, after @{term single_valued}\<close>
definition funof :: "[('a*'b)set, 'a] => 'b" where
"funof r == (\<lambda>x. THE y. (x,y) \<in> r)"
@@ -518,11 +518,11 @@
by (force simp add: in_wp_iff funof_eq)
-subsubsection{*Commutativity of Functions and Relation*}
-text{*Thesis, page 109*}
+subsubsection\<open>Commutativity of Functions and Relation\<close>
+text\<open>Thesis, page 109\<close>
(*FIXME: this proof is still an ungodly mess*)
-text{*From Meier's thesis, section 4.5.6*}
+text\<open>From Meier's thesis, section 4.5.6\<close>
lemma commutativity2_lemma:
assumes dcommutes:
"\<And>act s t. act \<in> Acts F \<Longrightarrow> s \<in> T \<Longrightarrow> (s, t) \<in> relcl L \<Longrightarrow>
@@ -564,7 +564,7 @@
then show "commutes F T B L" unfolding commutes_def by clarify
qed
-text{*Version packaged with @{thm progress_set_Union}*}
+text\<open>Version packaged with @{thm progress_set_Union}\<close>
lemma commutativity2:
assumes leadsTo: "F \<in> A leadsTo B"
and dcommutes:
@@ -585,8 +585,8 @@
done
-subsection {*Monotonicity*}
-text{*From Meier's thesis, section 4.5.7, page 110*}
+subsection \<open>Monotonicity\<close>
+text\<open>From Meier's thesis, section 4.5.7, page 110\<close>
(*to be continued?*)
end
--- a/src/HOL/UNITY/Project.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Project.thy Wed May 25 11:50:58 2016 +0200
@@ -7,7 +7,7 @@
Inheritance of GUARANTEES properties under extension.
*)
-section{*Projections of State Sets*}
+section\<open>Projections of State Sets\<close>
theory Project imports Extend begin
@@ -35,7 +35,7 @@
done
-subsection{*Safety*}
+subsection\<open>Safety\<close>
(*used below to prove Join_project_ensures*)
lemma project_unless:
@@ -103,7 +103,7 @@
end
-subsection{*"projecting" and union/intersection (no converses)*}
+subsection\<open>"projecting" and union/intersection (no converses)\<close>
lemma projecting_Int:
"[| projecting C h F XA' XA; projecting C h F XB' XB |]
@@ -206,7 +206,7 @@
by (force simp only: extending_def Join_project_increasing)
-subsection{*Reachability and project*}
+subsection\<open>Reachability and project\<close>
(*In practice, C = reachable(...): the inclusion is equality*)
lemma reachable_imp_reachable_project:
@@ -255,7 +255,7 @@
done
-subsection{*Converse results for weak safety: benefits of the argument C *}
+subsection\<open>Converse results for weak safety: benefits of the argument C\<close>
(*In practice, C = reachable(...): the inclusion is equality*)
lemma reachable_project_imp_reachable:
@@ -337,8 +337,8 @@
apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
done
-subsection{*A lot of redundant theorems: all are proved to facilitate reasoning
- about guarantees.*}
+subsection\<open>A lot of redundant theorems: all are proved to facilitate reasoning
+ about guarantees.\<close>
lemma projecting_Constrains:
"projecting (%G. reachable (extend h F\<squnion>G)) h F
@@ -398,9 +398,9 @@
done
-subsection{*leadsETo in the precondition (??)*}
+subsection\<open>leadsETo in the precondition (??)\<close>
-subsubsection{*transient*}
+subsubsection\<open>transient\<close>
lemma transient_extend_set_imp_project_transient:
"[| G \<in> transient (C \<inter> extend_set h A); G \<in> stable C |]
@@ -424,7 +424,7 @@
done
-subsubsection{*ensures -- a primitive combining progress with safety*}
+subsubsection\<open>ensures -- a primitive combining progress with safety\<close>
(*Used to prove project_leadsETo_I*)
lemma ensures_extend_set_imp_project_ensures:
@@ -458,7 +458,7 @@
[THEN project_extend_transient_D, THEN transient_strengthen])
done
-text{*Transferring a transient property upwards*}
+text\<open>Transferring a transient property upwards\<close>
lemma project_transient_extend_set:
"project h C G \<in> transient (project_set h C \<inter> A - B)
==> G \<in> transient (C \<inter> extend_set h A - extend_set h B)"
@@ -496,8 +496,8 @@
apply (blast intro: project_transient_extend_set transient_strengthen)
done
-text{*Lemma useful for both STRONG and WEAK progress, but the transient
- condition's very strong*}
+text\<open>Lemma useful for both STRONG and WEAK progress, but the transient
+ condition's very strong\<close>
(*The strange induction formula allows induction over the leadsTo
assumption's non-atomic precondition*)
@@ -528,7 +528,7 @@
project_set_reachable_extend_eq)
-subsection{*Towards the theorem @{text project_Ensures_D}*}
+subsection\<open>Towards the theorem \<open>project_Ensures_D\<close>\<close>
lemma project_ensures_D_lemma:
"[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));
@@ -566,7 +566,7 @@
done
-subsection{*Guarantees*}
+subsection\<open>Guarantees\<close>
lemma project_act_Restrict_subset_project_act:
"project_act h (Restrict C act) \<subseteq> project_act h act"
@@ -618,9 +618,9 @@
(*It seems that neither "guarantees" law can be proved from the other.*)
-subsection{*guarantees corollaries*}
+subsection\<open>guarantees corollaries\<close>
-subsubsection{*Some could be deleted: the required versions are easy to prove*}
+subsubsection\<open>Some could be deleted: the required versions are easy to prove\<close>
lemma extend_guar_increasing:
"[| F \<in> UNIV guarantees increasing func;
@@ -651,7 +651,7 @@
done
-subsubsection{*Guarantees with a leadsTo postcondition*}
+subsubsection\<open>Guarantees with a leadsTo postcondition\<close>
lemma project_leadsTo_D:
"F\<squnion>project h UNIV G \<in> A leadsTo B
--- a/src/HOL/UNITY/Rename.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Rename.thy Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
Copyright 2000 University of Cambridge
*)
-section{*Renaming of State Sets*}
+section\<open>Renaming of State Sets\<close>
theory Rename imports Extend begin
@@ -39,7 +39,7 @@
by (simp add: rename_def)
-subsection{*inverse properties*}
+subsection\<open>inverse properties\<close>
lemma extend_set_inv:
"bij h
@@ -164,7 +164,7 @@
by (blast intro: bij_rename bij_rename_imp_bij)
-subsection{*the lattice operations*}
+subsection\<open>the lattice operations\<close>
lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP"
by (simp add: rename_def Extend.extend_SKIP)
@@ -178,7 +178,7 @@
by (simp add: rename_def Extend.extend_JN)
-subsection{*Strong Safety: co, stable*}
+subsection\<open>Strong Safety: co, stable\<close>
lemma rename_constrains:
"bij h ==> (rename h F \<in> (h`A) co (h`B)) = (F \<in> A co B)"
@@ -203,7 +203,7 @@
done
-subsection{*Weak Safety: Co, Stable*}
+subsection\<open>Weak Safety: Co, Stable\<close>
lemma reachable_rename_eq:
"bij h ==> reachable (rename h F) = h ` (reachable F)"
@@ -228,7 +228,7 @@
bij_is_surj [THEN surj_f_inv_f])
-subsection{*Progress: transient, ensures*}
+subsection\<open>Progress: transient, ensures\<close>
lemma rename_transient:
"bij h ==> (rename h F \<in> transient (h`A)) = (F \<in> transient A)"
@@ -288,7 +288,7 @@
by (simp add: Extend.OK_extend_iff rename_def)
-subsection{*"image" versions of the rules, for lifting "guarantees" properties*}
+subsection\<open>"image" versions of the rules, for lifting "guarantees" properties\<close>
(*All the proofs are similar. Better would have been to prove one
meta-theorem, but how can we handle the polymorphism? E.g. in
--- a/src/HOL/UNITY/Simple/Common.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy Wed May 25 11:50:58 2016 +0200
@@ -97,7 +97,7 @@
then show ?case by simp
qed
next
- from `n \<in> common`
+ from \<open>n \<in> common\<close>
show "{..n} \<inter> id -` {n..} \<union> common \<subseteq> common"
by (simp add: atMost_Int_atLeast)
qed
--- a/src/HOL/UNITY/Simple/Lift.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/Lift.thy Wed May 25 11:50:58 2016 +0200
@@ -10,21 +10,21 @@
begin
record state =
- floor :: "int" --{*current position of the lift*}
- "open" :: "bool" --{*whether the door is opened at floor*}
- stop :: "bool" --{*whether the lift is stopped at floor*}
- req :: "int set" --{*for each floor, whether the lift is requested*}
- up :: "bool" --{*current direction of movement*}
- move :: "bool" --{*whether moving takes precedence over opening*}
+ floor :: "int" \<comment>\<open>current position of the lift\<close>
+ "open" :: "bool" \<comment>\<open>whether the door is opened at floor\<close>
+ stop :: "bool" \<comment>\<open>whether the lift is stopped at floor\<close>
+ req :: "int set" \<comment>\<open>for each floor, whether the lift is requested\<close>
+ up :: "bool" \<comment>\<open>current direction of movement\<close>
+ move :: "bool" \<comment>\<open>whether moving takes precedence over opening\<close>
axiomatization
- Min :: "int" and --{*least and greatest floors*}
- Max :: "int" --{*least and greatest floors*}
+ Min :: "int" and \<comment>\<open>least and greatest floors\<close>
+ Max :: "int" \<comment>\<open>least and greatest floors\<close>
where
Min_le_Max [iff]: "Min \<le> Max"
- --{*Abbreviations: the "always" part*}
+ \<comment>\<open>Abbreviations: the "always" part\<close>
definition
above :: "state set"
@@ -50,7 +50,7 @@
ready :: "state set"
where "ready = {s. stop s & ~ open s & move s}"
- --{*Further abbreviations*}
+ \<comment>\<open>Further abbreviations\<close>
definition
moving :: "state set"
@@ -65,7 +65,7 @@
where "opened = {s. stop s & open s & move s}"
definition
- closed :: "state set" --{*but this is the same as ready!!*}
+ closed :: "state set" \<comment>\<open>but this is the same as ready!!\<close>
where "closed = {s. stop s & ~ open s & move s}"
definition
@@ -78,7 +78,7 @@
- --{*The program*}
+ \<comment>\<open>The program\<close>
definition
request_act :: "(state*state) set"
@@ -128,12 +128,12 @@
definition
button_press :: "(state*state) set"
- --{*This action is omitted from prior treatments, which therefore are
+ \<comment>\<open>This action is omitted from prior treatments, which therefore are
unrealistic: nobody asks the lift to do anything! But adding this
action invalidates many of the existing progress arguments: various
"ensures" properties fail. Maybe it should be constrained to only
allow button presses in the current direction of travel, like in a
- real lift.*}
+ real lift.\<close>
where "button_press =
{(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
& Min \<le> n & n \<le> Max}"
@@ -141,7 +141,7 @@
definition
Lift :: "state program"
- --{*for the moment, we OMIT @{text button_press}*}
+ \<comment>\<open>for the moment, we OMIT \<open>button_press\<close>\<close>
where "Lift = mk_total_program
({s. floor s = Min & ~ up s & move s & stop s &
~ open s & req s = {}},
@@ -150,7 +150,7 @@
UNIV)"
- --{*Invariants*}
+ \<comment>\<open>Invariants\<close>
definition
bounded :: "state set"
@@ -261,7 +261,7 @@
done
-subsection{*Progress*}
+subsection\<open>Progress\<close>
declare moving_def [THEN def_set_simp, simp]
declare stopped_def [THEN def_set_simp, simp]
@@ -271,7 +271,7 @@
declare Req_def [THEN def_set_simp, simp]
-text{*The HUG'93 paper mistakenly omits the Req n from these!*}
+text\<open>The HUG'93 paper mistakenly omits the Req n from these!\<close>
(** Lift_1 **)
lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Wed May 25 11:50:58 2016 +0200
@@ -5,15 +5,15 @@
Original file is ../Auth/NS_Public_Bad
*)
-section{*Analyzing the Needham-Schroeder Public-Key Protocol in UNITY*}
+section\<open>Analyzing the Needham-Schroeder Public-Key Protocol in UNITY\<close>
theory NSP_Bad imports "../../Auth/Public" "../UNITY_Main" begin
-text{*This is the flawed version, vulnerable to Lowe's attack.
+text\<open>This is the flawed version, vulnerable to Lowe's attack.
From page 260 of
Burrows, Abadi and Needham. A Logic of Authentication.
Proc. Royal Soc. 426 (1989).
-*}
+\<close>
type_synonym state = "event list"
@@ -63,8 +63,8 @@
declare analz_into_parts [dest]
declare Fake_parts_insert_in_Un [dest]
-text{*For other theories, e.g. Mutex and Lift, using [iff] slows proofs down.
- Here, it facilitates re-use of the Auth proofs.*}
+text\<open>For other theories, e.g. Mutex and Lift, using [iff] slows proofs down.
+ Here, it facilitates re-use of the Auth proofs.\<close>
declare Fake_def [THEN def_act_simp, iff]
declare NS1_def [THEN def_act_simp, iff]
@@ -74,8 +74,8 @@
declare Nprg_def [THEN def_prg_Init, simp]
-text{*A "possibility property": there are traces that reach the end.
- Replace by LEADSTO proof!*}
+text\<open>A "possibility property": there are traces that reach the end.
+ Replace by LEADSTO proof!\<close>
lemma "A \<noteq> B ==>
\<exists>NB. \<exists>s \<in> reachable Nprg. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set s"
apply (intro exI bexI)
@@ -88,7 +88,7 @@
done
-subsection{*Inductive Proofs about @{term ns_public}*}
+subsection\<open>Inductive Proofs about @{term ns_public}\<close>
lemma ns_constrainsI:
"(!!act s s'. [| act \<in> {Id, Fake, NS1, NS2, NS3};
@@ -99,8 +99,8 @@
done
-text{*This ML code does the inductions directly.*}
-ML{*
+text\<open>This ML code does the inductions directly.\<close>
+ML\<open>
fun ns_constrains_tac ctxt i =
SELECT_GOAL
(EVERY
@@ -121,17 +121,17 @@
(*"reachable" gets in here*)
resolve_tac ctxt [@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}] 1,
ns_constrains_tac ctxt 1];
-*}
+\<close>
-method_setup ns_induct = {*
- Scan.succeed (SIMPLE_METHOD' o ns_induct_tac) *}
+method_setup ns_induct = \<open>
+ Scan.succeed (SIMPLE_METHOD' o ns_induct_tac)\<close>
"for inductive reasoning about the Needham-Schroeder protocol"
-text{*Converts invariants into statements about reachable states*}
+text\<open>Converts invariants into statements about reachable states\<close>
lemmas Always_Collect_reachableD =
Always_includes_reachable [THEN subsetD, THEN CollectD]
-text{*Spy never sees another agent's private key! (unless it's bad at start)*}
+text\<open>Spy never sees another agent's private key! (unless it's bad at start)\<close>
lemma Spy_see_priK:
"Nprg \<in> Always {s. (Key (priK A) \<in> parts (spies s)) = (A \<in> bad)}"
apply ns_induct
@@ -145,10 +145,10 @@
declare Spy_analz_priK [THEN Always_Collect_reachableD, simp]
-subsection{*Authenticity properties obtained from NS2*}
+subsection\<open>Authenticity properties obtained from NS2\<close>
-text{*It is impossible to re-use a nonce in both NS1 and NS2 provided the
- nonce is secret. (Honest users generate fresh nonces.)*}
+text\<open>It is impossible to re-use a nonce in both NS1 and NS2 provided the
+ nonce is secret. (Honest users generate fresh nonces.)\<close>
lemma no_nonce_NS1_NS2:
"Nprg
\<in> Always {s. Crypt (pubK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies s) -->
@@ -158,12 +158,12 @@
apply (blast intro: analz_insertI)+
done
-text{*Adding it to the claset slows down proofs...*}
+text\<open>Adding it to the claset slows down proofs...\<close>
lemmas no_nonce_NS1_NS2_reachable =
no_nonce_NS1_NS2 [THEN Always_Collect_reachableD, rule_format]
-text{*Unicity for NS1: nonce NA identifies agents A and B*}
+text\<open>Unicity for NS1: nonce NA identifies agents A and B\<close>
lemma unique_NA_lemma:
"Nprg
\<in> Always {s. Nonce NA \<notin> analz (spies s) -->
@@ -172,10 +172,10 @@
A=A' & B=B'}"
apply ns_induct
apply auto
-txt{*Fake, NS1 are non-trivial*}
+txt\<open>Fake, NS1 are non-trivial\<close>
done
-text{*Unicity for NS1: nonce NA identifies agents A and B*}
+text\<open>Unicity for NS1: nonce NA identifies agents A and B\<close>
lemma unique_NA:
"[| Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts(spies s);
Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies s);
@@ -185,26 +185,26 @@
by (blast dest: unique_NA_lemma [THEN Always_Collect_reachableD])
-text{*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*}
+text\<open>Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure\<close>
lemma Spy_not_see_NA:
"[| A \<notin> bad; B \<notin> bad |]
==> Nprg \<in> Always
{s. Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s
--> Nonce NA \<notin> analz (spies s)}"
apply ns_induct
-txt{*NS3*}
+txt\<open>NS3\<close>
prefer 4 apply (blast intro: no_nonce_NS1_NS2_reachable)
-txt{*NS2*}
+txt\<open>NS2\<close>
prefer 3 apply (blast dest: unique_NA)
-txt{*NS1*}
+txt\<open>NS1\<close>
prefer 2 apply blast
-txt{*Fake*}
+txt\<open>Fake\<close>
apply spy_analz
done
-text{*Authentication for A: if she receives message 2 and has used NA
- to start a run, then B has sent message 2.*}
+text\<open>Authentication for A: if she receives message 2 and has used NA
+ to start a run, then B has sent message 2.\<close>
lemma A_trusts_NS2:
"[| A \<notin> bad; B \<notin> bad |]
==> Nprg \<in> Always
@@ -217,7 +217,7 @@
done
-text{*If the encrypted message appears then it originated with Alice in NS1*}
+text\<open>If the encrypted message appears then it originated with Alice in NS1\<close>
lemma B_trusts_NS1:
"Nprg \<in> Always
{s. Nonce NA \<notin> analz (spies s) -->
@@ -228,10 +228,10 @@
done
-subsection{*Authenticity properties obtained from NS2*}
+subsection\<open>Authenticity properties obtained from NS2\<close>
-text{*Unicity for NS2: nonce NB identifies nonce NA and agent A.
- Proof closely follows that of @{text unique_NA}.*}
+text\<open>Unicity for NS2: nonce NB identifies nonce NA and agent A.
+ Proof closely follows that of \<open>unique_NA\<close>.\<close>
lemma unique_NB_lemma:
"Nprg
\<in> Always {s. Nonce NB \<notin> analz (spies s) -->
@@ -240,7 +240,7 @@
A=A' & NA=NA'}"
apply ns_induct
apply auto
-txt{*Fake, NS2 are non-trivial*}
+txt\<open>Fake, NS2 are non-trivial\<close>
done
lemma unique_NB:
@@ -253,7 +253,7 @@
done
-text{*NB remains secret PROVIDED Alice never responds with round 3*}
+text\<open>NB remains secret PROVIDED Alice never responds with round 3\<close>
lemma Spy_not_see_NB:
"[| A \<notin> bad; B \<notin> bad |]
==> Nprg \<in> Always
@@ -262,20 +262,20 @@
--> Nonce NB \<notin> analz (spies s)}"
apply ns_induct
apply (simp_all (no_asm_simp) add: all_conj_distrib)
-txt{*NS3: because NB determines A*}
+txt\<open>NS3: because NB determines A\<close>
prefer 4 apply (blast dest: unique_NB)
-txt{*NS2: by freshness and unicity of NB*}
+txt\<open>NS2: by freshness and unicity of NB\<close>
prefer 3 apply (blast intro: no_nonce_NS1_NS2_reachable)
-txt{*NS1: by freshness*}
+txt\<open>NS1: by freshness\<close>
prefer 2 apply blast
-txt{*Fake*}
+txt\<open>Fake\<close>
apply spy_analz
done
-text{*Authentication for B: if he receives message 3 and has used NB
- in message 2, then A has sent message 3--to somebody....*}
+text\<open>Authentication for B: if he receives message 3 and has used NB
+ in message 2, then A has sent message 3--to somebody....\<close>
lemma B_trusts_NS3:
"[| A \<notin> bad; B \<notin> bad |]
==> Nprg \<in> Always
@@ -286,29 +286,29 @@
apply (insert Spy_not_see_NB [of A B NA NB], simp, ns_induct)
apply (simp_all (no_asm_simp) add: ex_disj_distrib)
apply auto
-txt{*NS3: because NB determines A. This use of @{text unique_NB} is robust.*}
+txt\<open>NS3: because NB determines A. This use of \<open>unique_NB\<close> is robust.\<close>
apply (blast intro: unique_NB [THEN conjunct1])
done
-text{*Can we strengthen the secrecy theorem? NO*}
+text\<open>Can we strengthen the secrecy theorem? NO\<close>
lemma "[| A \<notin> bad; B \<notin> bad |]
==> Nprg \<in> Always
{s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s
--> Nonce NB \<notin> analz (spies s)}"
apply ns_induct
apply auto
-txt{*Fake*}
+txt\<open>Fake\<close>
apply spy_analz
-txt{*NS2: by freshness and unicity of NB*}
+txt\<open>NS2: by freshness and unicity of NB\<close>
apply (blast intro: no_nonce_NS1_NS2_reachable)
-txt{*NS3: unicity of NB identifies A and NA, but not B*}
+txt\<open>NS3: unicity of NB identifies A and NA, but not B\<close>
apply (frule_tac A'=A in Says_imp_spies [THEN parts.Inj, THEN unique_NB])
apply (erule Says_imp_spies [THEN parts.Inj], auto)
apply (rename_tac s B' C)
-txt{*This is the attack!
+txt\<open>This is the attack!
@{subgoals[display,indent=0,margin=65]}
-*}
+\<close>
oops
--- a/src/HOL/UNITY/Simple/Reach.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy Wed May 25 11:50:58 2016 +0200
@@ -33,7 +33,7 @@
where "metric s = card {v. ~ s v}"
-text{**We assume that the set of vertices is finite*}
+text\<open>*We assume that the set of vertices is finite\<close>
axiomatization where
finite_graph: "finite (UNIV :: vertex set)"
@@ -52,7 +52,7 @@
declare asgt_def [THEN def_act_simp,simp]
-text{*All vertex sets are finite*}
+text\<open>All vertex sets are finite\<close>
declare finite_subset [OF subset_UNIV finite_graph, iff]
declare reach_invariant_def [THEN def_set_simp, simp]
--- a/src/HOL/UNITY/Simple/Token.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/Token.thy Wed May 25 11:50:58 2016 +0200
@@ -4,19 +4,19 @@
*)
-section {*The Token Ring*}
+section \<open>The Token Ring\<close>
theory Token
imports "../WFair"
begin
-text{*From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.*}
+text\<open>From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.\<close>
-subsection{*Definitions*}
+subsection\<open>Definitions\<close>
datatype pstate = Hungry | Eating | Thinking
- --{*process states*}
+ \<comment>\<open>process states\<close>
record state =
token :: "nat"
@@ -71,7 +71,7 @@
done
-subsection{*Progress under Weak Fairness*}
+subsection\<open>Progress under Weak Fairness\<close>
lemma wf_nodeOrder: "wf(nodeOrder j)"
apply (unfold nodeOrder_def)
@@ -85,8 +85,8 @@
apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
done
-text{*From "A Logic for Concurrent Programming", but not used in Chapter 4.
- Note the use of @{text cases}. Reasoning about leadsTo takes practice!*}
+text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4.
+ Note the use of \<open>cases\<close>. Reasoning about leadsTo takes practice!\<close>
lemma TR7_nodeOrder:
"[| i<N; j<N |] ==>
F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
@@ -97,7 +97,7 @@
done
-text{*Chapter 4 variant, the one actually used below.*}
+text\<open>Chapter 4 variant, the one actually used below.\<close>
lemma TR7_aux: "[| i<N; j<N; i\<noteq>j |]
==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
apply (rule TR7 [THEN leadsTo_weaken_R])
@@ -109,7 +109,7 @@
by auto
-text{*Misra's TR9: the token reaches an arbitrary node*}
+text\<open>Misra's TR9: the token reaches an arbitrary node\<close>
lemma leadsTo_j: "j<N ==> F \<in> {s. token s < N} leadsTo (HasTok j)"
apply (rule leadsTo_weaken_R)
apply (rule_tac I = "-{j}" and f = token and B = "{}"
@@ -121,7 +121,7 @@
apply (auto simp add: HasTok_def nodeOrder_def)
done
-text{*Misra's TR8: a hungry process eventually eats*}
+text\<open>Misra's TR8: a hungry process eventually eats\<close>
lemma token_progress:
"j<N ==> F \<in> ({s. token s < N} \<inter> H j) leadsTo (E j)"
apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
--- a/src/HOL/UNITY/SubstAx.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
Weak LeadsTo relation (restricted to the set of reachable states)
*)
-section{*Weak Progress*}
+section\<open>Weak Progress\<close>
theory SubstAx imports WFair Constrains begin
@@ -18,7 +18,7 @@
notation LeadsTo (infixl "\<longmapsto>w" 60)
-text{*Resembles the previous definition of LeadsTo*}
+text\<open>Resembles the previous definition of LeadsTo\<close>
lemma LeadsTo_eq_leadsTo:
"A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}"
apply (unfold LeadsTo_def)
@@ -26,7 +26,7 @@
done
-subsection{*Specialized laws for handling invariants*}
+subsection\<open>Specialized laws for handling invariants\<close>
(** Conjoining an Always property **)
@@ -47,7 +47,7 @@
lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2]
-subsection{*Introduction rules: Basis, Trans, Union*}
+subsection\<open>Introduction rules: Basis, Trans, Union\<close>
lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
apply (simp add: LeadsTo_def)
@@ -68,12 +68,12 @@
done
-subsection{*Derived rules*}
+subsection\<open>Derived rules\<close>
lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV"
by (simp add: LeadsTo_def)
-text{*Useful with cancellation, disjunction*}
+text\<open>Useful with cancellation, disjunction\<close>
lemma LeadsTo_Un_duplicate:
"F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
by (simp add: Un_ac)
@@ -87,12 +87,12 @@
apply (blast intro: LeadsTo_Union)
done
-text{*Binary union introduction rule*}
+text\<open>Binary union introduction rule\<close>
lemma LeadsTo_Un:
"[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
using LeadsTo_UN [of "{A, B}" F id C] by auto
-text{*Lets us look at the starting state*}
+text\<open>Lets us look at the starting state\<close>
lemma single_LeadsTo_I:
"(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B"
by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
@@ -176,8 +176,8 @@
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
done
-text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??
- This is the most useful form of the "disjunction" rule*}
+text\<open>Set difference: maybe combine with \<open>leadsTo_weaken_L\<close>??
+ This is the most useful form of the "disjunction" rule\<close>
lemma LeadsTo_Diff:
"[| F \<in> (A-B) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C |]
==> F \<in> A LeadsTo C"
@@ -191,18 +191,18 @@
done
-text{*Version with no index set*}
+text\<open>Version with no index set\<close>
lemma LeadsTo_UN_UN_noindex:
"(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
by (blast intro: LeadsTo_UN_UN)
-text{*Version with no index set*}
+text\<open>Version with no index set\<close>
lemma all_LeadsTo_UN_UN:
"\<forall>i. F \<in> (A i) LeadsTo (A' i)
==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
by (blast intro: LeadsTo_UN_UN)
-text{*Binary union version*}
+text\<open>Binary union version\<close>
lemma LeadsTo_Un_Un:
"[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |]
==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')"
@@ -240,18 +240,18 @@
done
-text{*The impossibility law*}
+text\<open>The impossibility law\<close>
-text{*The set "A" may be non-empty, but it contains no reachable states*}
+text\<open>The set "A" may be non-empty, but it contains no reachable states\<close>
lemma LeadsTo_empty: "[|F \<in> A LeadsTo {}; all_total F|] ==> F \<in> Always (-A)"
apply (simp add: LeadsTo_def Always_eq_includes_reachable)
apply (drule leadsTo_empty, auto)
done
-subsection{*PSP: Progress-Safety-Progress*}
+subsection\<open>PSP: Progress-Safety-Progress\<close>
-text{*Special case of PSP: Misra's "stable conjunction"*}
+text\<open>Special case of PSP: Misra's "stable conjunction"\<close>
lemma PSP_Stable:
"[| F \<in> A LeadsTo A'; F \<in> Stable B |]
==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)"
@@ -298,7 +298,7 @@
done
-subsection{*Induction rules*}
+subsection\<open>Induction rules\<close>
(** Meta or object quantifier ????? **)
lemma LeadsTo_wf_induct:
@@ -329,7 +329,7 @@
==> F \<in> A LeadsTo B"
by (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
-text{*Integer version. Could generalize from 0 to any lower bound*}
+text\<open>Integer version. Could generalize from 0 to any lower bound\<close>
lemma integ_0_le_induct:
"[| F \<in> Always {s. (0::int) \<le> f s};
!! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo
@@ -363,7 +363,7 @@
done
-subsection{*Completion: Binary and General Finite versions*}
+subsection\<open>Completion: Binary and General Finite versions\<close>
lemma Completion:
"[| F \<in> A LeadsTo (A' \<union> C); F \<in> A' Co (A' \<union> C);
--- a/src/HOL/UNITY/Transformers.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Transformers.thy Wed May 25 11:50:58 2016 +0200
@@ -13,30 +13,30 @@
Swiss Federal Institute of Technology Zurich (1997)
*)
-section{*Predicate Transformers*}
+section\<open>Predicate Transformers\<close>
theory Transformers imports Comp begin
-subsection{*Defining the Predicate Transformers @{term wp},
- @{term awp} and @{term wens}*}
+subsection\<open>Defining the Predicate Transformers @{term wp},
+ @{term awp} and @{term wens}\<close>
definition wp :: "[('a*'a) set, 'a set] => 'a set" where
- --{*Dijkstra's weakest-precondition operator (for an individual command)*}
+ \<comment>\<open>Dijkstra's weakest-precondition operator (for an individual command)\<close>
"wp act B == - (act^-1 `` (-B))"
definition awp :: "['a program, 'a set] => 'a set" where
- --{*Dijkstra's weakest-precondition operator (for a program)*}
+ \<comment>\<open>Dijkstra's weakest-precondition operator (for a program)\<close>
"awp F B == (\<Inter>act \<in> Acts F. wp act B)"
definition wens :: "['a program, ('a*'a) set, 'a set] => 'a set" where
- --{*The weakest-ensures transformer*}
+ \<comment>\<open>The weakest-ensures transformer\<close>
"wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)"
-text{*The fundamental theorem for wp*}
+text\<open>The fundamental theorem for wp\<close>
theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
by (force simp add: wp_def)
-text{*This lemma is a good deal more intuitive than the definition!*}
+text\<open>This lemma is a good deal more intuitive than the definition!\<close>
lemma in_wp_iff: "(a \<in> wp act B) = (\<forall>x. (a,x) \<in> act --> x \<in> B)"
by (simp add: wp_def, blast)
@@ -46,7 +46,7 @@
lemma wp_empty [simp]: "wp act {} = - (Domain act)"
by (force simp add: wp_def)
-text{*The identity relation is the skip action*}
+text\<open>The identity relation is the skip action\<close>
lemma wp_Id [simp]: "wp Id B = B"
by (simp add: wp_def)
@@ -60,7 +60,7 @@
lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
by (simp add: awp_def wp_def, blast)
-text{*The fundamental theorem for awp*}
+text\<open>The fundamental theorem for awp\<close>
theorem awp_iff_constrains: "(A <= awp F B) = (F \<in> A co B)"
by (simp add: awp_def constrains_def wp_iff INT_subset_iff)
@@ -88,8 +88,8 @@
lemma wens_Id [simp]: "wens F Id B = B"
by (simp add: wens_def gfp_def wp_def awp_def, blast)
-text{*These two theorems justify the claim that @{term wens} returns the
-weakest assertion satisfying the ensures property*}
+text\<open>These two theorems justify the claim that @{term wens} returns the
+weakest assertion satisfying the ensures property\<close>
lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B"
apply (simp add: wens_def ensures_def transient_def, clarify)
apply (rule rev_bexI, assumption)
@@ -101,7 +101,7 @@
by (simp add: wens_def gfp_def constrains_def awp_def wp_def
ensures_def transient_def, blast)
-text{*These two results constitute assertion (4.13) of the thesis*}
+text\<open>These two results constitute assertion (4.13) of the thesis\<close>
lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
apply (simp add: wens_def wp_def awp_def)
apply (rule gfp_mono, blast)
@@ -110,22 +110,22 @@
lemma wens_weakening: "B \<subseteq> wens F act B"
by (simp add: wens_def gfp_def, blast)
-text{*Assertion (6), or 4.16 in the thesis*}
+text\<open>Assertion (6), or 4.16 in the thesis\<close>
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B"
apply (simp add: wens_def wp_def awp_def)
apply (rule gfp_upperbound, blast)
done
-text{*Assertion 4.17 in the thesis*}
+text\<open>Assertion 4.17 in the thesis\<close>
lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
- --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
+ \<comment>\<open>Proved instantly, yet remarkably fragile. If \<open>Un_subset_iff\<close>
is declared as an iff-rule, then it's almost impossible to prove.
- One proof is via @{text meson} after expanding all definitions, but it's
- slow!*}
+ One proof is via \<open>meson\<close> after expanding all definitions, but it's
+ slow!\<close>
-text{*Assertion (7): 4.18 in the thesis. NOTE that many of these results
-hold for an arbitrary action. We often do not require @{term "act \<in> Acts F"}*}
+text\<open>Assertion (7): 4.18 in the thesis. NOTE that many of these results
+hold for an arbitrary action. We often do not require @{term "act \<in> Acts F"}\<close>
lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)"
apply (simp add: stable_def)
apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]])
@@ -134,7 +134,7 @@
apply (simp add: wens_weakening)
done
-text{*Assertion 4.20 in the thesis.*}
+text\<open>Assertion 4.20 in the thesis.\<close>
lemma wens_Int_eq_lemma:
"[|T-B \<subseteq> awp F T; act \<in> Acts F|]
==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
@@ -143,8 +143,8 @@
apply (simp add: wp_def awp_def, blast)
done
-text{*Assertion (8): 4.21 in the thesis. Here we indeed require
- @{term "act \<in> Acts F"}*}
+text\<open>Assertion (8): 4.21 in the thesis. Here we indeed require
+ @{term "act \<in> Acts F"}\<close>
lemma wens_Int_eq:
"[|T-B \<subseteq> awp F T; act \<in> Acts F|]
==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
@@ -155,7 +155,7 @@
done
-subsection{*Defining the Weakest Ensures Set*}
+subsection\<open>Defining the Weakest Ensures Set\<close>
inductive_set
wens_set :: "['a program, 'a set] => 'a set set"
@@ -198,29 +198,29 @@
apply (blast intro: wens_set.Union)
done
-text{*Assertion (9): 4.27 in the thesis.*}
+text\<open>Assertion (9): 4.27 in the thesis.\<close>
lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)"
by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo)
-text{*This is the result that requires the definition of @{term wens_set} to
+text\<open>This is the result that requires the definition of @{term wens_set} to
require @{term W} to be non-empty in the Unio case, for otherwise we should
- always have @{term "{} \<in> wens_set F B"}.*}
+ always have @{term "{} \<in> wens_set F B"}.\<close>
lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A"
apply (erule wens_set.induct)
apply (blast intro: wens_weakening [THEN subsetD])+
done
-subsection{*Properties Involving Program Union*}
+subsection\<open>Properties Involving Program Union\<close>
-text{*Assertion (4.30) of thesis, reoriented*}
+text\<open>Assertion (4.30) of thesis, reoriented\<close>
lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B"
by (simp add: awp_def wp_def, blast)
lemma wens_subset: "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
by (subst wens_unfold, fast)
-text{*Assertion (4.31)*}
+text\<open>Assertion (4.31)\<close>
lemma subset_wens_Join:
"[|A = T \<inter> wens F act B; T-B \<subseteq> awp F T; A-B \<subseteq> awp G (A \<union> B)|]
==> A \<subseteq> wens (F\<squnion>G) act B"
@@ -232,14 +232,14 @@
apply (insert wens_subset [of F act B], blast)
done
-text{*Assertion (4.32)*}
+text\<open>Assertion (4.32)\<close>
lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B"
apply (simp add: wens_def)
apply (rule gfp_mono)
apply (auto simp add: awp_Join_eq)
done
-text{*Lemma, because the inductive step is just too messy.*}
+text\<open>Lemma, because the inductive step is just too messy.\<close>
lemma wens_Union_inductive_step:
assumes awpF: "T-B \<subseteq> awp F T"
and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
@@ -272,14 +272,14 @@
and major: "X \<in> wens_set F B"
shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y"
apply (rule wens_set.induct [OF major])
- txt{*Basis: trivial*}
+ txt\<open>Basis: trivial\<close>
apply (blast intro: wens_set.Basis)
- txt{*Inductive step*}
+ txt\<open>Inductive step\<close>
apply clarify
apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI)
apply (force intro: wens_set.Wens)
apply (simp add: wens_Union_inductive_step [OF awpF awpG])
-txt{*Union: by Axiom of Choice*}
+txt\<open>Union: by Axiom of Choice\<close>
apply (simp add: ball_conj_distrib Bex_def)
apply (clarify dest!: bchoice)
apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI)
@@ -299,10 +299,10 @@
done
-subsection {*The Set @{term "wens_set F B"} for a Single-Assignment Program*}
-text{*Thesis Section 4.3.3*}
+subsection \<open>The Set @{term "wens_set F B"} for a Single-Assignment Program\<close>
+text\<open>Thesis Section 4.3.3\<close>
-text{*We start by proving laws about single-assignment programs*}
+text\<open>We start by proving laws about single-assignment programs\<close>
lemma awp_single_eq [simp]:
"awp (mk_program (init, {act}, allowed)) B = B \<inter> wp act B"
by (force simp add: awp_def wp_def)
@@ -332,7 +332,7 @@
by (simp add: wens_def gfp_def wp_def, blast)
-text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
+text\<open>Next, we express the @{term "wens_set"} for single-assignment programs\<close>
definition wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set" where
"wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act ^^ i) B"
@@ -416,7 +416,7 @@
apply (simp add: atMost_Suc, blast)
done
-text{*lemma for Union case*}
+text\<open>lemma for Union case\<close>
lemma Union_eq_wens_single:
"\<lbrakk>\<forall>k. \<not> W \<subseteq> wens_single_finite act B ` {..k};
W \<subseteq> insert (wens_single act B)
@@ -439,15 +439,15 @@
insert (wens_single act B) (range (wens_single_finite act B))"
apply (rule subsetI)
apply (erule wens_set.induct)
- txt{*Basis*}
+ txt\<open>Basis\<close>
apply (fastforce simp add: wens_single_finite_def)
- txt{*Wens inductive step*}
+ txt\<open>Wens inductive step\<close>
apply (case_tac "acta = Id", simp)
apply (simp add: wens_single_eq)
apply (elim disjE)
apply (simp add: wens_single_Un_eq)
apply (force simp add: wens_single_finite_Un_eq)
-txt{*Union inductive step*}
+txt\<open>Union inductive step\<close>
apply (case_tac "\<exists>k. W \<subseteq> wens_single_finite act B ` (atMost k)")
apply (blast dest!: subset_wens_single_finite, simp)
apply (rule disjI1 [OF Union_eq_wens_single], blast+)
@@ -471,7 +471,7 @@
apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
done
-text{*Theorem (4.29)*}
+text\<open>Theorem (4.29)\<close>
theorem wens_set_single_eq:
"[|F = mk_program (init, {act}, allowed); single_valued act|]
==> wens_set F B =
@@ -481,7 +481,7 @@
apply (erule ssubst, erule single_subset_wens_set)
done
-text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}
+text\<open>Generalizing Misra's Fixed Point Union Theorem (4.41)\<close>
lemma fp_leadsTo_Join:
"[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B"
--- a/src/HOL/UNITY/UNITY.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/UNITY.thy Wed May 25 11:50:58 2016 +0200
@@ -8,7 +8,7 @@
From Misra, "A Logic for Concurrent Programming", 1994.
*)
-section {*The Basic UNITY Theory*}
+section \<open>The Basic UNITY Theory\<close>
theory UNITY imports Main begin
@@ -54,11 +54,11 @@
"invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
definition increasing :: "['a => 'b::{order}] => 'a program set" where
- --{*Polymorphic in both states and the meaning of @{text "\<le>"}*}
+ \<comment>\<open>Polymorphic in both states and the meaning of \<open>\<le>\<close>\<close>
"increasing f == \<Inter>z. stable {s. z \<le> f s}"
-subsubsection{*The abstract type of programs*}
+subsubsection\<open>The abstract type of programs\<close>
lemmas program_typedef =
Rep_Program Rep_Program_inverse Abs_Program_inverse
@@ -83,7 +83,7 @@
lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
by (simp add: insert_absorb)
-subsubsection{*Inspectors for type "program"*}
+subsubsection\<open>Inspectors for type "program"\<close>
lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
by (simp add: program_typedef)
@@ -95,7 +95,7 @@
"AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
by (simp add: program_typedef)
-subsubsection{*Equality for UNITY programs*}
+subsubsection\<open>Equality for UNITY programs\<close>
lemma surjective_mk_program [simp]:
"mk_program (Init F, Acts F, AllowedActs F) = F"
@@ -124,7 +124,7 @@
by (blast intro: program_equalityI program_equalityE)
-subsubsection{*co*}
+subsubsection\<open>co\<close>
lemma constrainsI:
"(!!act s s'. [| act: Acts F; (s,s') \<in> act; s \<in> A |] ==> s': A')
@@ -147,12 +147,12 @@
lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
by (unfold constrains_def, blast)
-text{*monotonic in 2nd argument*}
+text\<open>monotonic in 2nd argument\<close>
lemma constrains_weaken_R:
"[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
by (unfold constrains_def, blast)
-text{*anti-monotonic in 1st argument*}
+text\<open>anti-monotonic in 1st argument\<close>
lemma constrains_weaken_L:
"[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
by (unfold constrains_def, blast)
@@ -161,7 +161,7 @@
"[| F \<in> A co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B co B'"
by (unfold constrains_def, blast)
-subsubsection{*Union*}
+subsubsection\<open>Union\<close>
lemma constrains_Un:
"[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
@@ -184,7 +184,7 @@
lemma constrains_INT_distrib: "A co (\<Inter>i \<in> I. B i) = (\<Inter>i \<in> I. A co B i)"
by (unfold constrains_def, blast)
-subsubsection{*Intersection*}
+subsubsection\<open>Intersection\<close>
lemma constrains_Int:
"[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
@@ -198,8 +198,8 @@
lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
by (unfold constrains_def, auto)
-text{*The reasoning is by subsets since "co" refers to single actions
- only. So this rule isn't that useful.*}
+text\<open>The reasoning is by subsets since "co" refers to single actions
+ only. So this rule isn't that useful.\<close>
lemma constrains_trans:
"[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
by (unfold constrains_def, blast)
@@ -209,7 +209,7 @@
by (unfold constrains_def, clarify, blast)
-subsubsection{*unless*}
+subsubsection\<open>unless\<close>
lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
by (unfold unless_def, assumption)
@@ -218,7 +218,7 @@
by (unfold unless_def, assumption)
-subsubsection{*stable*}
+subsubsection\<open>stable\<close>
lemma stableI: "F \<in> A co A ==> F \<in> stable A"
by (unfold stable_def, assumption)
@@ -229,7 +229,7 @@
lemma stable_UNIV [simp]: "stable UNIV = UNIV"
by (unfold stable_def constrains_def, auto)
-subsubsection{*Union*}
+subsubsection\<open>Union\<close>
lemma stable_Un:
"[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
@@ -248,7 +248,7 @@
"(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Union>X)"
by (unfold stable_def constrains_def, blast)
-subsubsection{*Intersection*}
+subsubsection\<open>Intersection\<close>
lemma stable_Int:
"[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<inter> A')"
@@ -278,18 +278,18 @@
lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI]
-subsubsection{*invariant*}
+subsubsection\<open>invariant\<close>
lemma invariantI: "[| Init F \<subseteq> A; F \<in> stable A |] ==> F \<in> invariant A"
by (simp add: invariant_def)
-text{*Could also say @{term "invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)"}*}
+text\<open>Could also say @{term "invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)"}\<close>
lemma invariant_Int:
"[| F \<in> invariant A; F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
by (auto simp add: invariant_def stable_Int)
-subsubsection{*increasing*}
+subsubsection\<open>increasing\<close>
lemma increasingD:
"F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
@@ -319,15 +319,15 @@
==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
by (unfold constrains_def, blast)
-text{*As above, but for the trivial case of a one-variable state, in which the
- state is identified with its one variable.*}
+text\<open>As above, but for the trivial case of a one-variable state, in which the
+ state is identified with its one variable.\<close>
lemma elimination_sing:
"(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
by (unfold constrains_def, blast)
-subsubsection{*Theoretical Results from Section 6*}
+subsubsection\<open>Theoretical Results from Section 6\<close>
lemma constrains_strongest_rhs:
"F \<in> A co (strongest_rhs F A )"
@@ -338,7 +338,7 @@
by (unfold constrains_def strongest_rhs_def, blast)
-subsubsection{*Ad-hoc set-theory rules*}
+subsubsection\<open>Ad-hoc set-theory rules\<close>
lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
by blast
@@ -346,7 +346,7 @@
lemma Int_Union_Union: "\<Union>B \<inter> A = \<Union>((%C. C \<inter> A)`B)"
by blast
-text{*Needed for WF reasoning in WFair.thy*}
+text\<open>Needed for WF reasoning in WFair.thy\<close>
lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
by blast
@@ -355,7 +355,7 @@
by blast
-subsection{*Partial versus Total Transitions*}
+subsection\<open>Partial versus Total Transitions\<close>
definition totalize_act :: "('a * 'a)set => ('a * 'a)set" where
"totalize_act act == act \<union> Id_on (-(Domain act))"
@@ -376,7 +376,7 @@
by (blast intro: sym [THEN image_eqI])
-subsubsection{*Basic properties*}
+subsubsection\<open>Basic properties\<close>
lemma totalize_act_Id [simp]: "totalize_act Id = Id"
by (simp add: totalize_act_def)
@@ -427,9 +427,9 @@
by (simp add: mk_total_program_def)
-subsection{*Rules for Lazy Definition Expansion*}
+subsection\<open>Rules for Lazy Definition Expansion\<close>
-text{*They avoid expanding the full program, which is a large expression*}
+text\<open>They avoid expanding the full program, which is a large expression\<close>
lemma def_prg_Init:
"F = mk_total_program (init,acts,allowed) ==> Init F = init"
@@ -445,16 +445,16 @@
==> AllowedActs F = insert Id allowed"
by (simp add: mk_total_program_def)
-text{*An action is expanded if a pair of states is being tested against it*}
+text\<open>An action is expanded if a pair of states is being tested against it\<close>
lemma def_act_simp:
"act = {(s,s'). P s s'} ==> ((s,s') \<in> act) = P s s'"
by (simp add: mk_total_program_def)
-text{*A set is expanded only if an element is being tested against it*}
+text\<open>A set is expanded only if an element is being tested against it\<close>
lemma def_set_simp: "A = B ==> (x \<in> A) = (x \<in> B)"
by (simp add: mk_total_program_def)
-subsubsection{*Inspectors for type "program"*}
+subsubsection\<open>Inspectors for type "program"\<close>
lemma Init_total_eq [simp]:
"Init (mk_total_program (init,acts,allowed)) = init"
--- a/src/HOL/UNITY/UNITY_Main.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
Copyright 2003 University of Cambridge
*)
-section{*Comprehensive UNITY Theory*}
+section\<open>Comprehensive UNITY Theory\<close>
theory UNITY_Main
imports Detects PPROD Follows ProgressSets
@@ -11,19 +11,19 @@
ML_file "UNITY_tactics.ML"
-method_setup safety = {*
- Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
+method_setup safety = \<open>
+ Scan.succeed (SIMPLE_METHOD' o constrains_tac)\<close>
"for proving safety properties"
-method_setup ensures_tac = {*
+method_setup ensures_tac = \<open>
Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
-*} "for proving progress properties"
+\<close> "for proving progress properties"
-setup {*
+setup \<open>
map_theory_simpset (fn ctxt => ctxt
addsimps (make_o_equivs ctxt @{thm fst_o_funPair} @ make_o_equivs ctxt @{thm snd_o_funPair})
addsimps (make_o_equivs ctxt @{thm fst_o_lift_map} @ make_o_equivs ctxt @{thm snd_o_lift_map}))
-*}
+\<close>
end
--- a/src/HOL/UNITY/Union.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Union.thy Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs.
*)
-section{*Unions of Programs*}
+section\<open>Unions of Programs\<close>
theory Union imports SubstAx FP begin
@@ -47,7 +47,7 @@
"\<Squnion>x. B" == "CONST JOIN (CONST UNIV) (\<lambda>x. B)"
-subsection{*SKIP*}
+subsection\<open>SKIP\<close>
lemma Init_SKIP [simp]: "Init SKIP = UNIV"
by (simp add: SKIP_def)
@@ -61,7 +61,7 @@
lemma reachable_SKIP [simp]: "reachable SKIP = UNIV"
by (force elim: reachable.induct intro: reachable.intros)
-subsection{*SKIP and safety properties*}
+subsection\<open>SKIP and safety properties\<close>
lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) = (A \<subseteq> B)"
by (unfold constrains_def, auto)
@@ -75,7 +75,7 @@
declare SKIP_in_stable [THEN stable_imp_Stable, iff]
-subsection{*Join*}
+subsection\<open>Join\<close>
lemma Init_Join [simp]: "Init (F\<squnion>G) = Init F \<inter> Init G"
by (simp add: Join_def)
@@ -88,7 +88,7 @@
by (auto simp add: Join_def)
-subsection{*JN*}
+subsection\<open>JN\<close>
lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP"
by (unfold JOIN_def SKIP_def, auto)
@@ -114,7 +114,7 @@
by (simp add: JOIN_def)
-subsection{*Algebraic laws*}
+subsection\<open>Algebraic laws\<close>
lemma Join_commute: "F\<squnion>G = G\<squnion>F"
by (simp add: Join_def Un_commute Int_commute)
@@ -151,7 +151,7 @@
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
-subsection{*Laws Governing @{text "\<Squnion>"}*}
+subsection\<open>Laws Governing \<open>\<Squnion>\<close>\<close>
(*Also follows by JN_insert and insert_absorb, but the proof is longer*)
lemma JN_absorb: "k \<in> I ==> F k\<squnion>(\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
@@ -178,7 +178,7 @@
done
-subsection{*Safety: co, stable, FP*}
+subsection\<open>Safety: co, stable, FP\<close>
(*Fails if I={} because it collapses to SKIP \<in> A co B, i.e. to A \<subseteq> B. So an
alternative precondition is A \<subseteq> B, but most proofs using this rule require
@@ -240,7 +240,7 @@
by (simp add: FP_def JN_stable INTER_eq)
-subsection{*Progress: transient, ensures*}
+subsection\<open>Progress: transient, ensures\<close>
lemma JN_transient:
"i \<in> I ==>
@@ -308,7 +308,7 @@
done
-subsection{*the ok and OK relations*}
+subsection\<open>the ok and OK relations\<close>
lemma ok_SKIP1 [iff]: "SKIP ok F"
by (simp add: ok_def)
@@ -355,7 +355,7 @@
by (auto simp add: OK_iff_ok)
-subsection{*Allowed*}
+subsection\<open>Allowed\<close>
lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
by (auto simp add: Allowed_def)
@@ -372,8 +372,8 @@
lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))"
by (auto simp add: OK_iff_ok ok_iff_Allowed)
-subsection{*@{term safety_prop}, for reasoning about
- given instances of "ok"*}
+subsection\<open>@{term safety_prop}, for reasoning about
+ given instances of "ok"\<close>
lemma safety_prop_Acts_iff:
"safety_prop X ==> (Acts G \<subseteq> insert Id (UNION X Acts)) = (G \<in> X)"
@@ -418,7 +418,7 @@
moreover assume "Acts G \<subseteq> (\<Union>j\<in>\<Inter>i\<in>I. X i. Acts j)"
ultimately have "Acts G \<subseteq> (\<Union>i\<in>X i. Acts i)"
by auto
- with * `i \<in> I` show "G \<in> X i" by blast
+ with * \<open>i \<in> I\<close> show "G \<in> X i" by blast
qed
lemma safety_prop_INTER1 [simp]:
@@ -443,7 +443,7 @@
==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
by (auto simp add: ok_def safety_prop_Acts_iff)
-text{*The union of two total programs is total.*}
+text\<open>The union of two total programs is total.\<close>
lemma totalize_Join: "totalize F\<squnion>totalize G = totalize (F\<squnion>G)"
by (simp add: program_equalityI totalize_def Join_def image_Un)
--- a/src/HOL/UNITY/WFair.thy Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/WFair.thy Wed May 25 11:50:58 2016 +0200
@@ -7,11 +7,11 @@
From Misra, "A Logic for Concurrent Programming", 1994
*)
-section{*Progress*}
+section\<open>Progress\<close>
theory WFair imports UNITY begin
-text{*The original version of this theory was based on weak fairness. (Thus,
+text\<open>The original version of this theory was based on weak fairness. (Thus,
the entire UNITY development embodied this assumption, until February 2003.)
Weak fairness states that if a command is enabled continuously, then it is
eventually executed. Ernie Cohen suggested that I instead adopt unconditional
@@ -30,14 +30,14 @@
property, it simplifies many proofs. A drawback is that some laws only hold
under the assumption that all transitions are total. The best-known of these
is the impossibility law for leads-to.
-*}
+\<close>
definition
- --{*This definition specifies conditional fairness. The rest of the theory
+ \<comment>\<open>This definition specifies conditional fairness. The rest of the theory
is generic to all forms of fairness. To get weak fairness, conjoin
the inclusion below with @{term "A \<subseteq> Domain act"}, which specifies
- that the action is enabled over all of @{term A}.*}
+ that the action is enabled over all of @{term A}.\<close>
transient :: "'a set => 'a program set" where
"transient A == {F. \<exists>act\<in>Acts F. act``A \<subseteq> -A}"
@@ -48,7 +48,7 @@
inductive_set
leads :: "'a program => ('a set * 'a set) set"
- --{*LEADS-TO constant for the inductive definition*}
+ \<comment>\<open>LEADS-TO constant for the inductive definition\<close>
for F :: "'a program"
where
@@ -60,17 +60,17 @@
definition leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60) where
- --{*visible version of the LEADS-TO relation*}
+ \<comment>\<open>visible version of the LEADS-TO relation\<close>
"A leadsTo B == {F. (A,B) \<in> leads F}"
definition wlt :: "['a program, 'a set] => 'a set" where
- --{*predicate transformer: the largest set that leads to @{term B}*}
+ \<comment>\<open>predicate transformer: the largest set that leads to @{term B}\<close>
"wlt F B == \<Union>{A. F \<in> A leadsTo B}"
notation leadsTo (infixl "\<longmapsto>" 60)
-subsection{*transient*}
+subsection\<open>transient\<close>
lemma stable_transient:
"[| F \<in> stable A; F \<in> transient A |] ==> \<exists>act\<in>Acts F. A \<subseteq> - (Domain act)"
@@ -104,9 +104,9 @@
by (unfold transient_def, auto)
-text{*This equation recovers the notion of weak fairness. A totalized
+text\<open>This equation recovers the notion of weak fairness. A totalized
program satisfies a transient assertion just if the original program
- contains a suitable action that is also enabled.*}
+ contains a suitable action that is also enabled.\<close>
lemma totalize_transient_iff:
"(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
apply (simp add: totalize_def totalize_act_def transient_def
@@ -119,7 +119,7 @@
==> totalize F \<in> transient A"
by (simp add: totalize_transient_iff, blast)
-subsection{*ensures*}
+subsection\<open>ensures\<close>
lemma ensuresI:
"[| F \<in> (A-B) co (A \<union> B); F \<in> transient (A-B) |] ==> F \<in> A ensures B"
@@ -135,7 +135,7 @@
apply (blast intro: constrains_weaken transient_strengthen)
done
-text{*The L-version (precondition strengthening) fails, but we have this*}
+text\<open>The L-version (precondition strengthening) fails, but we have this\<close>
lemma stable_ensures_Int:
"[| F \<in> stable C; F \<in> A ensures B |]
==> F \<in> (C \<inter> A) ensures (C \<inter> B)"
@@ -155,7 +155,7 @@
by (simp (no_asm) add: ensures_def unless_def)
-subsection{*leadsTo*}
+subsection\<open>leadsTo\<close>
lemma leadsTo_Basis [intro]: "F \<in> A ensures B ==> F \<in> A leadsTo B"
apply (unfold leadsTo_def)
@@ -179,7 +179,7 @@
lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (-A)"
by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
-text{*Useful with cancellation, disjunction*}
+text\<open>Useful with cancellation, disjunction\<close>
lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"
by (simp add: Un_ac)
@@ -187,7 +187,7 @@
"F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"
by (simp add: Un_ac)
-text{*The Union introduction rule as we should have liked to state it*}
+text\<open>The Union introduction rule as we should have liked to state it\<close>
lemma leadsTo_Union:
"(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (\<Union>S) leadsTo B"
apply (unfold leadsTo_def)
@@ -206,7 +206,7 @@
apply (blast intro: leadsTo_Union)
done
-text{*Binary union introduction rule*}
+text\<open>Binary union introduction rule\<close>
lemma leadsTo_Un:
"[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
using leadsTo_Union [of "{A, B}" F C] by auto
@@ -216,7 +216,7 @@
by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
-text{*The INDUCTION rule as we should have liked to state it*}
+text\<open>The INDUCTION rule as we should have liked to state it\<close>
lemma leadsTo_induct:
"[| F \<in> za leadsTo zb;
!!A B. F \<in> A ensures B ==> P A B;
@@ -245,16 +245,16 @@
(** Variant induction rule: on the preconditions for B **)
-text{*Lemma is the weak version: can't see how to do it in one step*}
+text\<open>Lemma is the weak version: can't see how to do it in one step\<close>
lemma leadsTo_induct_pre_lemma:
"[| F \<in> za leadsTo zb;
P zb;
!!A B. [| F \<in> A ensures B; P B |] ==> P A;
!!S. \<forall>A \<in> S. P A ==> P (\<Union>S)
|] ==> P za"
-txt{*by induction on this formula*}
+txt\<open>by induction on this formula\<close>
apply (subgoal_tac "P zb --> P za")
-txt{*now solve first subgoal: this formula is sufficient*}
+txt\<open>now solve first subgoal: this formula is sufficient\<close>
apply (blast intro: leadsTo_refl)
apply (erule leadsTo_induct)
apply (blast+)
@@ -282,7 +282,7 @@
"[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
by (blast intro: leadsTo_Trans subset_imp_leadsTo)
-text{*Distributes over binary unions*}
+text\<open>Distributes over binary unions\<close>
lemma leadsTo_Un_distrib:
"F \<in> (A \<union> B) leadsTo C = (F \<in> A leadsTo C & F \<in> B leadsTo C)"
by (blast intro: leadsTo_Un leadsTo_weaken_L)
@@ -301,7 +301,7 @@
by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)
-text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}
+text\<open>Set difference: maybe combine with \<open>leadsTo_weaken_L\<close>??\<close>
lemma leadsTo_Diff:
"[| F \<in> (A-B) leadsTo C; F \<in> B leadsTo C |] ==> F \<in> A leadsTo C"
by (blast intro: leadsTo_Un leadsTo_weaken)
@@ -312,7 +312,7 @@
apply (blast intro: leadsTo_Union leadsTo_weaken_R)
done
-text{*Binary union version*}
+text\<open>Binary union version\<close>
lemma leadsTo_Un_Un:
"[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |]
==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
@@ -350,7 +350,7 @@
done
-text{*The impossibility law*}
+text\<open>The impossibility law\<close>
lemma leadsTo_empty: "[|F \<in> A leadsTo {}; all_total F|] ==> A={}"
apply (erule leadsTo_induct_pre)
apply (simp_all add: ensures_def constrains_def transient_def all_total_def, clarify)
@@ -358,9 +358,9 @@
apply blast
done
-subsection{*PSP: Progress-Safety-Progress*}
+subsection\<open>PSP: Progress-Safety-Progress\<close>
-text{*Special case of PSP: Misra's "stable conjunction"*}
+text\<open>Special case of PSP: Misra's "stable conjunction"\<close>
lemma psp_stable:
"[| F \<in> A leadsTo A'; F \<in> stable B |]
==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)"
@@ -389,9 +389,9 @@
==> F \<in> (A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B' - B))"
apply (erule leadsTo_induct)
prefer 3 apply (blast intro: leadsTo_Union_Int)
- txt{*Basis case*}
+ txt\<open>Basis case\<close>
apply (blast intro: psp_ensures)
-txt{*Transitivity case has a delicate argument involving "cancellation"*}
+txt\<open>Transitivity case has a delicate argument involving "cancellation"\<close>
apply (rule leadsTo_Un_duplicate2)
apply (erule leadsTo_cancel_Diff1)
apply (simp add: Int_Diff Diff_triv)
@@ -413,7 +413,7 @@
done
-subsection{*Proving the induction rules*}
+subsection\<open>Proving the induction rules\<close>
(** The most general rule: r is any wf relation; f is any variant function **)
@@ -490,9 +490,9 @@
done
-subsection{*wlt*}
+subsection\<open>wlt\<close>
-text{*Misra's property W3*}
+text\<open>Misra's property W3\<close>
lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B"
apply (unfold wlt_def)
apply (blast intro!: leadsTo_Union)
@@ -503,17 +503,17 @@
apply (blast intro!: leadsTo_Union)
done
-text{*Misra's property W2*}
+text\<open>Misra's property W2\<close>
lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)"
by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
-text{*Misra's property W4*}
+text\<open>Misra's property W4\<close>
lemma wlt_increasing: "B \<subseteq> wlt F B"
apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
done
-text{*Used in the Trans case below*}
+text\<open>Used in the Trans case below\<close>
lemma lemma1:
"[| B \<subseteq> A2;
F \<in> (A1 - B) co (A1 \<union> B);
@@ -521,18 +521,18 @@
==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)"
by (unfold constrains_def, clarify, blast)
-text{*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*}
+text\<open>Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"\<close>
lemma leadsTo_123:
"F \<in> A leadsTo A'
==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
apply (erule leadsTo_induct)
- txt{*Basis*}
+ txt\<open>Basis\<close>
apply (blast dest: ensuresD)
- txt{*Trans*}
+ txt\<open>Trans\<close>
apply clarify
apply (rule_tac x = "Ba \<union> Bb" in exI)
apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
-txt{*Union*}
+txt\<open>Union\<close>
apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
apply (rule_tac x = "\<Union>A \<in> S. f A" in exI)
apply (auto intro: leadsTo_UN)
@@ -542,7 +542,7 @@
done
-text{*Misra's property W5*}
+text\<open>Misra's property W5\<close>
lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)"
proof -
from wlt_leadsTo [of F B, THEN leadsTo_123]
@@ -564,7 +564,7 @@
qed
-subsection{*Completion: Binary and General Finite versions*}
+subsection\<open>Completion: Binary and General Finite versions\<close>
lemma completion_lemma :
"[| W = wlt F (B' \<union> C);