--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The transmission channel *}
+section \<open>The transmission channel\<close>
theory Abschannel
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The transmission channel -- finite version *}
+section \<open>The transmission channel -- finite version\<close>
theory Abschannel_finite
imports Abschannel "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
--- a/src/HOL/HOLCF/IOA/ABP/Action.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Action.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The set of all actions of the system *}
+section \<open>The set of all actions of the system\<close>
theory Action
imports Packet
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The main correctness proof: System_fin implements System *}
+section \<open>The main correctness proof: System_fin implements System\<close>
theory Correctness
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Env Impl Impl_finite
@@ -67,7 +67,7 @@
asig_projections set_lemmas
-subsection {* lemmas about reduce *}
+subsection \<open>lemmas about reduce\<close>
lemma l_iff_red_nil: "(reduce l = []) = (l = [])"
by (induct l) (auto split: list.split)
@@ -75,28 +75,28 @@
lemma hd_is_reduce_hd: "s ~= [] --> hd s = hd (reduce s)"
by (induct s) (auto split: list.split)
-text {* to be used in the following Lemma *}
+text \<open>to be used in the following Lemma\<close>
lemma rev_red_not_nil [rule_format]:
"l ~= [] --> reverse (reduce l) ~= []"
by (induct l) (auto split: list.split)
-text {* shows applicability of the induction hypothesis of the following Lemma 1 *}
+text \<open>shows applicability of the induction hypothesis of the following Lemma 1\<close>
lemma last_ind_on_first:
"l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
apply simp
- apply (tactic {* auto_tac (put_simpset HOL_ss @{context}
+ apply (tactic \<open>auto_tac (put_simpset HOL_ss @{context}
addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])
- |> Splitter.add_split @{thm list.split}) *})
+ |> Splitter.add_split @{thm list.split})\<close>)
done
-text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}
+text \<open>Main Lemma 1 for \<open>S_pkt\<close> in showing that reduce is refinement.\<close>
lemma reduce_hd:
"if x=hd(reverse(reduce(l))) & reduce(l)~=[] then
reduce(l@[x])=reduce(l) else
reduce(l@[x])=reduce(l)@[x]"
apply (simplesubst split_if)
apply (rule conjI)
-txt {* @{text "-->"} *}
+txt \<open>\<open>-->\<close>\<close>
apply (induct_tac "l")
apply (simp (no_asm))
apply (case_tac "list=[]")
@@ -108,7 +108,7 @@
apply (erule exE)+
apply hypsubst
apply (simp del: reduce_Cons add: last_ind_on_first l_iff_red_nil)
-txt {* @{text "<--"} *}
+txt \<open>\<open><--\<close>\<close>
apply (simp (no_asm) add: and_de_morgan_and_absorbe l_iff_red_nil)
apply (induct_tac "l")
apply (simp (no_asm))
@@ -120,7 +120,7 @@
done
-text {* Main Lemma 2 for R_pkt in showing that reduce is refinement. *}
+text \<open>Main Lemma 2 for R_pkt in showing that reduce is refinement.\<close>
lemma reduce_tl: "s~=[] ==>
if hd(s)=hd(tl(s)) & tl(s)~=[] then
reduce(tl(s))=reduce(s) else
@@ -132,23 +132,23 @@
done
-subsection {* Channel Abstraction *}
+subsection \<open>Channel Abstraction\<close>
declare split_if [split del]
lemma channel_abstraction: "is_weak_ref_map reduce ch_ioa ch_fin_ioa"
apply (simp (no_asm) add: is_weak_ref_map_def)
-txt {* main-part *}
+txt \<open>main-part\<close>
apply (rule allI)+
apply (rule imp_conj_lemma)
apply (induct_tac "a")
-txt {* 2 cases *}
+txt \<open>2 cases\<close>
apply (simp_all (no_asm) cong del: if_weak_cong add: externals_def)
-txt {* fst case *}
+txt \<open>fst case\<close>
apply (rule impI)
apply (rule disjI2)
apply (rule reduce_hd)
-txt {* snd case *}
+txt \<open>snd case\<close>
apply (rule impI)
apply (erule conjE)+
apply (erule disjE)
@@ -164,49 +164,49 @@
declare split_if [split]
lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa"
-apply (tactic {*
+apply (tactic \<open>
simp_tac (put_simpset HOL_ss @{context}
addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def},
@{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap},
- @{thm channel_abstraction}]) 1 *})
+ @{thm channel_abstraction}]) 1\<close>)
done
lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa"
-apply (tactic {*
+apply (tactic \<open>
simp_tac (put_simpset HOL_ss @{context}
addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def},
@{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap},
- @{thm channel_abstraction}]) 1 *})
+ @{thm channel_abstraction}]) 1\<close>)
done
-text {* 3 thms that do not hold generally! The lucky restriction here is
- the absence of internal actions. *}
+text \<open>3 thms that do not hold generally! The lucky restriction here is
+ the absence of internal actions.\<close>
lemma sender_unchanged: "is_weak_ref_map (%id. id) sender_ioa sender_ioa"
apply (simp (no_asm) add: is_weak_ref_map_def)
-txt {* main-part *}
+txt \<open>main-part\<close>
apply (rule allI)+
apply (induct_tac a)
-txt {* 7 cases *}
+txt \<open>7 cases\<close>
apply (simp_all (no_asm) add: externals_def)
done
-text {* 2 copies of before *}
+text \<open>2 copies of before\<close>
lemma receiver_unchanged: "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa"
apply (simp (no_asm) add: is_weak_ref_map_def)
-txt {* main-part *}
+txt \<open>main-part\<close>
apply (rule allI)+
apply (induct_tac a)
-txt {* 7 cases *}
+txt \<open>7 cases\<close>
apply (simp_all (no_asm) add: externals_def)
done
lemma env_unchanged: "is_weak_ref_map (%id. id) env_ioa env_ioa"
apply (simp (no_asm) add: is_weak_ref_map_def)
-txt {* main-part *}
+txt \<open>main-part\<close>
apply (rule allI)+
apply (induct_tac a)
-txt {* 7 cases *}
+txt \<open>7 cases\<close>
apply (simp_all (no_asm) add: externals_def)
done
@@ -218,7 +218,7 @@
apply simp_all
done
-text {* totally the same as before *}
+text \<open>totally the same as before\<close>
lemma compat_single_fin_ch: "compatible srch_fin_ioa rsch_fin_ioa"
apply (simp add: compatible_def Int_def)
apply (rule set_eqI)
@@ -240,7 +240,7 @@
apply simp_all
done
-text {* 5 proofs totally the same as before *}
+text \<open>5 proofs totally the same as before\<close>
lemma compat_rec_fin: "compatible receiver_ioa (srch_fin_ioa \<parallel> rsch_fin_ioa)"
apply (simp del: del_simps
add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
@@ -291,13 +291,13 @@
done
-text {* lemmata about externals of channels *}
+text \<open>lemmata about externals of channels\<close>
lemma ext_single_ch: "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) &
externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))"
by (simp add: externals_def)
-subsection {* Soundness of Abstraction *}
+subsection \<open>Soundness of Abstraction\<close>
lemmas ext_simps = externals_of_par ext_single_ch
and compat_simps = compat_single_ch compat_single_fin_ch compat_rec
--- a/src/HOL/HOLCF/IOA/ABP/Env.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,14 +2,14 @@
Author: Olaf Müller
*)
-section {* The environment *}
+section \<open>The environment\<close>
theory Env
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
begin
type_synonym
- 'm env_state = bool -- {* give next bit to system *}
+ 'm env_state = bool \<comment> \<open>give next bit to system\<close>
definition
env_asig :: "'m action signature" where
--- a/src/HOL/HOLCF/IOA/ABP/Impl.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The implementation *}
+section \<open>The implementation\<close>
theory Impl
imports Sender Receiver Abschannel
--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The implementation *}
+section \<open>The implementation\<close>
theory Impl_finite
imports Sender Receiver Abschannel_finite
--- a/src/HOL/HOLCF/IOA/ABP/Lemmas.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Lemmas.thy Wed Dec 30 21:57:52 2015 +0100
@@ -6,7 +6,7 @@
imports Main
begin
-subsection {* Logic *}
+subsection \<open>Logic\<close>
lemma and_de_morgan_and_absorbe: "(~(A&B)) = ((~A)&B| ~B)"
by blast
@@ -18,7 +18,7 @@
by blast
-subsection {* Sets *}
+subsection \<open>Sets\<close>
lemma set_lemmas:
"f(x) : (UN x. {f(x)})"
@@ -27,8 +27,8 @@
"!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"
by auto
-text {* 2 Lemmas to add to @{text "set_lemmas"}, used also for action handling,
- namely for Intersections and the empty list (compatibility of IOA!). *}
+text \<open>2 Lemmas to add to \<open>set_lemmas\<close>, used also for action handling,
+ namely for Intersections and the empty list (compatibility of IOA!).\<close>
lemma singleton_set: "(UN b.{x. x=f(b)})= (UN b.{f(b)})"
by blast
@@ -36,7 +36,7 @@
by blast
-subsection {* Lists *}
+subsection \<open>Lists\<close>
lemma cons_not_nil: "l ~= [] --> (? x xs. l = (x#xs))"
by (induct l) simp_all
--- a/src/HOL/HOLCF/IOA/ABP/Packet.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Packets *}
+section \<open>Packets\<close>
theory Packet
imports Main
--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,14 +2,14 @@
Author: Olaf Müller
*)
-section {* The implementation: receiver *}
+section \<open>The implementation: receiver\<close>
theory Receiver
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
begin
type_synonym
- 'm receiver_state = "'m list * bool" -- {* messages, mode *}
+ 'm receiver_state = "'m list * bool" \<comment> \<open>messages, mode\<close>
definition
rq :: "'m receiver_state => 'm list" where
--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,14 +2,14 @@
Author: Olaf Müller
*)
-section {* The implementation: sender *}
+section \<open>The implementation: sender\<close>
theory Sender
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
begin
type_synonym
- 'm sender_state = "'m list * bool" -- {* messages, Alternating Bit *}
+ 'm sender_state = "'m list * bool" \<comment> \<open>messages, Alternating Bit\<close>
definition
sq :: "'m sender_state => 'm list" where
--- a/src/HOL/HOLCF/IOA/ABP/Spec.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The specification of reliable transmission *}
+section \<open>The specification of reliable transmission\<close>
theory Spec
imports IOA Action
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The (faulty) transmission channel (both directions) *}
+section \<open>The (faulty) transmission channel (both directions)\<close>
theory Abschannel
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
--- a/src/HOL/HOLCF/IOA/NTP/Action.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Action.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow & Konrad Slind
*)
-section {* The set of all actions of the system *}
+section \<open>The set of all actions of the system\<close>
theory Action
imports Packet
--- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow & Konrad Slind
*)
-section {* The main correctness proof: Impl implements Spec *}
+section \<open>The main correctness proof: Impl implements Spec\<close>
theory Correctness
imports Impl Spec
@@ -13,7 +13,7 @@
"hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
else tl(sq(sen s)))"
-setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
+setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def
@@ -21,10 +21,10 @@
declare split_paired_All [simp del]
-text {*
+text \<open>
A lemma about restricting the action signature of the implementation
to that of the specification.
-*}
+\<close>
lemma externals_lemma:
"a:externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) =
@@ -43,12 +43,12 @@
apply (induct_tac "a")
apply (simp_all (no_asm) add: actions_def asig_projections)
- txt {* 2 *}
+ txt \<open>2\<close>
apply (simp (no_asm) add: impl_ioas)
apply (simp (no_asm) add: impl_asigs)
apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
apply (simp (no_asm) add: "transitions"(1) unfold_renaming)
- txt {* 1 *}
+ txt \<open>1\<close>
apply (simp (no_asm) add: impl_ioas)
apply (simp (no_asm) add: impl_asigs)
apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
@@ -57,7 +57,7 @@
lemmas sels = sbit_def sq_def ssending_def rbit_def rq_def rsending_def
-text {* Proof of correctness *}
+text \<open>Proof of correctness\<close>
lemma ntp_correct:
"is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) spec_ioa"
apply (unfold Spec.ioa_def is_weak_ref_map_def)
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow & Konrad Slind
*)
-section {* The implementation *}
+section \<open>The implementation\<close>
theory Impl
imports Sender Receiver Abschannel
@@ -59,7 +59,7 @@
definition "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
-subsection {* Invariants *}
+subsection \<open>Invariants\<close>
declare le_SucI [simp]
@@ -101,7 +101,7 @@
2) ss unfolds transition relations
3) renname_ss unfolds transitions and the abstract channel *)
-ML {*
+ML \<open>
val ss = simpset_of (@{context} addsimps @{thms "transitions"});
val rename_ss = simpset_of (put_simpset ss @{context} addsimps @{thms unfold_renaming});
@@ -111,10 +111,10 @@
fun tac_ren ctxt =
asm_simp_tac (put_simpset rename_ss ctxt
|> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
-*}
+\<close>
-subsubsection {* Invariant 1 *}
+subsubsection \<open>Invariant 1\<close>
lemma raw_inv1: "invariant impl_ioa inv1"
@@ -124,7 +124,7 @@
apply (simp (no_asm) del: trans_of_par4 add: imp_conjR inv1_def)
-txt {* Split proof in two *}
+txt \<open>Split proof in two\<close>
apply (rule conjI)
(* First half *)
@@ -135,28 +135,28 @@
apply (tactic "tac @{context} 1")
apply (tactic "tac_ren @{context} 1")
-txt {* 5 + 1 *}
+txt \<open>5 + 1\<close>
apply (tactic "tac @{context} 1")
apply (tactic "tac_ren @{context} 1")
-txt {* 4 + 1 *}
-apply (tactic {* EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}] *})
+txt \<open>4 + 1\<close>
+apply (tactic \<open>EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}]\<close>)
-txt {* Now the other half *}
+txt \<open>Now the other half\<close>
apply (simp add: Impl.inv1_def split del: split_if)
apply (induct_tac a)
apply (tactic "EVERY1 [tac @{context}, tac @{context}]")
-txt {* detour 1 *}
+txt \<open>detour 1\<close>
apply (tactic "tac @{context} 1")
apply (tactic "tac_ren @{context} 1")
apply (rule impI)
apply (erule conjE)+
apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
split add: split_if)
-txt {* detour 2 *}
+txt \<open>detour 2\<close>
apply (tactic "tac @{context} 1")
apply (tactic "tac_ren @{context} 1")
apply (rule impI)
@@ -190,79 +190,79 @@
-subsubsection {* INVARIANT 2 *}
+subsubsection \<open>INVARIANT 2\<close>
lemma raw_inv2: "invariant impl_ioa inv2"
apply (rule invariantI1)
- txt {* Base case *}
+ txt \<open>Base case\<close>
apply (simp add: inv2_def receiver_projections sender_projections impl_ioas)
apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
apply (induct_tac "a")
- txt {* 10 cases. First 4 are simple, since state doesn't change *}
+ txt \<open>10 cases. First 4 are simple, since state doesn't change\<close>
- ML_prf {* val tac2 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv2_def}]) *}
+ ML_prf \<open>val tac2 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv2_def}])\<close>
- txt {* 10 - 7 *}
+ txt \<open>10 - 7\<close>
apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
- txt {* 6 *}
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
- (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
+ txt \<open>6\<close>
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>)
- txt {* 6 - 5 *}
+ txt \<open>6 - 5\<close>
apply (tactic "EVERY1 [tac2,tac2]")
- txt {* 4 *}
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
- (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
+ txt \<open>4\<close>
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>)
apply (tactic "tac2 1")
- txt {* 3 *}
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
- (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
+ txt \<open>3\<close>
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE})] 1\<close>)
apply (tactic "tac2 1")
- apply (tactic {* fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}]
- (@{thm Impl.hdr_sum_def})] *})
+ apply (tactic \<open>fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}]
+ (@{thm Impl.hdr_sum_def})]\<close>)
apply arith
- txt {* 2 *}
+ txt \<open>2\<close>
apply (tactic "tac2 1")
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
- (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>)
apply (intro strip)
apply (erule conjE)+
apply simp
- txt {* 1 *}
+ txt \<open>1\<close>
apply (tactic "tac2 1")
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
- (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1\<close>)
apply (intro strip)
apply (erule conjE)+
- apply (tactic {* fold_goals_tac @{context}
- [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
+ apply (tactic \<open>fold_goals_tac @{context}
+ [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})]\<close>)
apply simp
done
-subsubsection {* INVARIANT 3 *}
+subsubsection \<open>INVARIANT 3\<close>
lemma raw_inv3: "invariant impl_ioa inv3"
apply (rule invariantI)
- txt {* Base case *}
+ txt \<open>Base case\<close>
apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas)
apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
apply (induct_tac "a")
- ML_prf {* val tac3 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv3_def}]) *}
+ ML_prf \<open>val tac3 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv3_def}])\<close>
- txt {* 10 - 8 *}
+ txt \<open>10 - 8\<close>
apply (tactic "EVERY1[tac3,tac3,tac3]")
@@ -272,29 +272,29 @@
apply (erule exE)
apply simp
- txt {* 7 *}
+ txt \<open>7\<close>
apply (tactic "tac3 1")
apply (tactic "tac_ren @{context} 1")
apply force
- txt {* 6 - 3 *}
+ txt \<open>6 - 3\<close>
apply (tactic "EVERY1[tac3,tac3,tac3,tac3]")
- txt {* 2 *}
+ txt \<open>2\<close>
apply (tactic "asm_full_simp_tac (put_simpset ss @{context}) 1")
apply (simp (no_asm) add: inv3_def)
apply (intro strip, (erule conjE)+)
apply (rule imp_disjL [THEN iffD1])
apply (rule impI)
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
- (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
+ (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>)
apply simp
apply (erule conjE)+
apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm inv1_def}]
- (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm inv1_def}]
+ (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1\<close>)
apply (simp add: hdr_sum_def Multiset.count_def)
apply (rule add_le_mono)
apply (rule countm_props)
@@ -303,56 +303,56 @@
apply (simp (no_asm))
apply assumption
- txt {* 1 *}
+ txt \<open>1\<close>
apply (tactic "tac3 1")
apply (intro strip, (erule conjE)+)
apply (rule imp_disjL [THEN iffD1])
apply (rule impI)
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
- (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
+ (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>)
apply simp
done
-subsubsection {* INVARIANT 4 *}
+subsubsection \<open>INVARIANT 4\<close>
lemma raw_inv4: "invariant impl_ioa inv4"
apply (rule invariantI)
- txt {* Base case *}
+ txt \<open>Base case\<close>
apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas)
apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
apply (induct_tac "a")
- ML_prf {* val tac4 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv4_def}]) *}
+ ML_prf \<open>val tac4 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv4_def}])\<close>
- txt {* 10 - 2 *}
+ txt \<open>10 - 2\<close>
apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]")
- txt {* 2 b *}
+ txt \<open>2 b\<close>
apply (intro strip, (erule conjE)+)
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
- (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
+ (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>)
apply simp
- txt {* 1 *}
+ txt \<open>1\<close>
apply (tactic "tac4 1")
apply (intro strip, (erule conjE)+)
apply (rule ccontr)
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
- (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
- apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv3_def}]
- (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
+ (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>)
+ apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv3_def}]
+ (@{thm raw_inv3} RS @{thm invariantE})] 1\<close>)
apply simp
apply (rename_tac m, erule_tac x = "m" in allE)
apply simp
done
-text {* rebind them *}
+text \<open>rebind them\<close>
lemmas inv1 = raw_inv1 [THEN invariantE, unfolded inv1_def]
and inv2 = raw_inv2 [THEN invariantE, unfolded inv2_def]
--- a/src/HOL/HOLCF/IOA/NTP/Lemmas.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Lemmas.thy Wed Dec 30 21:57:52 2015 +0100
@@ -6,13 +6,13 @@
imports Main
begin
-subsubsection {* Logic *}
+subsubsection \<open>Logic\<close>
lemma neg_flip: "(X = (~ Y)) = ((~X) = Y)"
by blast
-subsection {* Sets *}
+subsection \<open>Sets\<close>
lemma set_lemmas:
"f(x) : (UN x. {f(x)})"
@@ -22,7 +22,7 @@
by auto
-subsection {* Arithmetic *}
+subsection \<open>Arithmetic\<close>
lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))"
by (simp add: diff_Suc split add: nat.split)
--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow & Konrad Slind
*)
-section {* Axiomatic multisets *}
+section \<open>Axiomatic multisets\<close>
theory Multiset
imports Lemmas
--- a/src/HOL/HOLCF/IOA/NTP/Packet.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Packet.thy Wed Dec 30 21:57:52 2015 +0100
@@ -18,7 +18,7 @@
"msg == snd"
-text {* Instantiation of a tautology? *}
+text \<open>Instantiation of a tautology?\<close>
lemma eq_packet_imp_eq_hdr: "!x. x = packet --> hdr(x) = hdr(packet)"
by simp
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow & Konrad Slind
*)
-section {* The implementation: receiver *}
+section \<open>The implementation: receiver\<close>
theory Receiver
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow & Konrad Slind
*)
-section {* The implementation: sender *}
+section \<open>The implementation: sender\<close>
theory Sender
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
--- a/src/HOL/HOLCF/IOA/NTP/Spec.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Tobias Nipkow & Konrad Slind
*)
-section {* The specification of reliable transmission *}
+section \<open>The specification of reliable transmission\<close>
theory Spec
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
--- a/src/HOL/HOLCF/IOA/Storage/Action.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Action.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The set of all actions of the system *}
+section \<open>The set of all actions of the system\<close>
theory Action
imports Main
--- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Correctness Proof *}
+section \<open>Correctness Proof\<close>
theory Correctness
imports SimCorrectness Spec Impl
@@ -30,29 +30,29 @@
"is_simulation sim_relation impl_ioa spec_ioa"
apply (simp (no_asm) add: is_simulation_def)
apply (rule conjI)
-txt {* start states *}
+txt \<open>start states\<close>
apply (auto)[1]
apply (rule_tac x = " ({},False) " in exI)
apply (simp add: sim_relation_def starts_of_def spec_ioa_def impl_ioa_def)
-txt {* main-part *}
+txt \<open>main-part\<close>
apply (rule allI)+
apply (rule imp_conj_lemma)
apply (rename_tac k b used c k' b' a)
apply (induct_tac "a")
apply (simp_all (no_asm) add: sim_relation_def impl_ioa_def impl_trans_def trans_of_def)
apply auto
-txt {* NEW *}
+txt \<open>NEW\<close>
apply (rule_tac x = "(used,True)" in exI)
apply simp
apply (rule transition_is_ex)
apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
-txt {* LOC *}
+txt \<open>LOC\<close>
apply (rule_tac x = " (used Un {k},False) " in exI)
apply (simp add: less_SucI)
apply (rule transition_is_ex)
apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
apply fast
-txt {* FREE *}
+txt \<open>FREE\<close>
apply (rename_tac nat, rule_tac x = " (used - {nat},c) " in exI)
apply simp
apply (rule transition_is_ex)
--- a/src/HOL/HOLCF/IOA/Storage/Impl.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The implementation of a memory *}
+section \<open>The implementation of a memory\<close>
theory Impl
imports IOA Action
--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The specification of a memory *}
+section \<open>The specification of a memory\<close>
theory Spec
imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Trivial Abstraction Example *}
+section \<open>Trivial Abstraction Example\<close>
theory TrivEx
imports Abstraction
@@ -51,9 +51,9 @@
"is_abstraction h_abs C_ioa A_ioa"
apply (unfold is_abstraction_def)
apply (rule conjI)
-txt {* start states *}
+txt \<open>start states\<close>
apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
-txt {* step case *}
+txt \<open>step case\<close>
apply (rule allI)+
apply (rule imp_conj_lemma)
apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Trivial Abstraction Example with fairness *}
+section \<open>Trivial Abstraction Example with fairness\<close>
theory TrivEx2
imports IOA Abstraction
@@ -58,9 +58,9 @@
"is_abstraction h_abs C_ioa A_ioa"
apply (unfold is_abstraction_def)
apply (rule conjI)
-txt {* start states *}
+txt \<open>start states\<close>
apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
-txt {* step case *}
+txt \<open>step case\<close>
apply (rule allI)+
apply (rule imp_conj_lemma)
apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
@@ -81,9 +81,9 @@
"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"
apply (unfold is_live_abstraction_def)
apply auto
-txt {* is_abstraction *}
+txt \<open>is_abstraction\<close>
apply (rule h_abs_is_abstraction)
-txt {* temp_weakening *}
+txt \<open>temp_weakening\<close>
apply abstraction
apply (erule Enabled_implication)
done
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Abstraction Theory -- tailored for I/O automata *}
+section \<open>Abstraction Theory -- tailored for I/O automata\<close>
theory Abstraction
imports LiveIOA
@@ -14,7 +14,7 @@
cex_abs :: "('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" where
"cex_abs f ex = (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"
definition
- -- {* equals cex_abs on Sequences -- after ex2seq application *}
+ \<comment> \<open>equals cex_abs on Sequences -- after ex2seq application\<close>
cex_absSeq :: "('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" where
"cex_absSeq f = (%s. Map (%(s,a,t). (f s,a,f t))$s)"
@@ -102,8 +102,8 @@
--> is_exec_frag A (cex_abs h (s,xs))"
apply (unfold cex_abs_def)
apply simp
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
-txt {* main case *}
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
+txt \<open>main case\<close>
apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
done
@@ -112,10 +112,10 @@
apply (simp add: weakeningIOA_def)
apply auto
apply (simp add: executions_def)
-txt {* start state *}
+txt \<open>start state\<close>
apply (rule conjI)
apply (simp add: is_abstraction_def cex_abs_def)
-txt {* is-execution-fragment *}
+txt \<open>is-execution-fragment\<close>
apply (erule exec_frag_abstraction)
apply (simp add: reachable.reachable_0)
done
@@ -202,7 +202,7 @@
==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))"
apply (unfold cex_abs_def mk_trace_def filter_act_def)
apply simp
-apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
done
@@ -218,13 +218,13 @@
apply (rule_tac x = "cex_abs h ex" in exI)
apply auto
(* Traces coincide *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (rule traces_coincide_abs)
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
(* cex_abs is execution *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (simp add: executions_def)
(* start state *)
apply (rule conjI)
@@ -235,7 +235,7 @@
(* Liveness *)
apply (simp add: temp_weakening_def2)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
done
(* FIX: NAch Traces.ML bringen *)
@@ -348,29 +348,29 @@
done
-subsubsection {* Box *}
+subsubsection \<open>Box\<close>
(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))"
-apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
done
lemma ex2seqConc [rule_format]:
"Finite s1 -->
(! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))"
apply (rule impI)
-apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
+apply (tactic \<open>Seq_Finite_induct_tac @{context} 1\<close>)
apply blast
(* main case *)
apply clarify
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
(* UU case *)
apply (simp add: nil_is_Conc)
(* nil case *)
apply (simp add: nil_is_Conc)
(* cons case *)
-apply (tactic {* pair_tac @{context} "aa" 1 *})
+apply (tactic \<open>pair_tac @{context} "aa" 1\<close>)
apply auto
done
@@ -388,11 +388,11 @@
(* FIX: NAch Sequence.ML bringen *)
lemma Mapnil: "(Map f$s = nil) = (s=nil)"
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
done
lemma MapUU: "(Map f$s = UU) = (s=UU)"
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
done
@@ -422,7 +422,7 @@
done
-subsubsection {* Init *}
+subsubsection \<open>Init\<close>
lemma strength_Init:
"[| state_strengthening P Q h |]
@@ -430,35 +430,35 @@
apply (unfold temp_strengthening_def state_strengthening_def
temp_sat_def satisfies_def Init_def unlift_def)
apply auto
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
done
-subsubsection {* Next *}
+subsubsection \<open>Next\<close>
lemma TL_ex2seq_UU:
"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
done
lemma TL_ex2seq_nil:
"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
done
(* FIX: put to Sequence Lemmas *)
lemma MapTL: "Map f$(TL$s) = TL$(Map f$s)"
-apply (tactic {* Seq_induct_tac @{context} "s" [] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "s" [] 1\<close>)
done
(* important property of cex_absSeq: As it is a 1to1 correspondence,
@@ -473,19 +473,19 @@
(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
apply auto
done
lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
done
@@ -508,7 +508,7 @@
done
-text {* Localizing Temporal Weakenings - 2 *}
+text \<open>Localizing Temporal Weakenings - 2\<close>
lemma weak_Init:
"[| state_weakening P Q h |]
@@ -516,13 +516,13 @@
apply (simp add: temp_weakening_def2 state_weakening_def2
temp_sat_def satisfies_def Init_def unlift_def)
apply auto
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
done
-text {* Localizing Temproal Strengthenings - 3 *}
+text \<open>Localizing Temproal Strengthenings - 3\<close>
lemma strength_Diamond:
"[| temp_strengthening P Q h |]
@@ -544,7 +544,7 @@
done
-text {* Localizing Temporal Weakenings - 3 *}
+text \<open>Localizing Temporal Weakenings - 3\<close>
lemma weak_Diamond:
"[| temp_weakening P Q h |]
@@ -602,13 +602,13 @@
strength_IMPLIES strength_Box strength_Next strength_Init
strength_Diamond strength_Leadsto weak_WF weak_SF
-ML {*
+ML \<open>
fun abstraction_tac ctxt =
SELECT_GOAL (auto_tac
(ctxt addSIs @{thms weak_strength_lemmas}
addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
-*}
+\<close>
-method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *}
+method_setup abstraction = \<open>Scan.succeed (SIMPLE_METHOD' o abstraction_tac)\<close>
end
--- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller, Tobias Nipkow & Konrad Slind
*)
-section {* Action signatures *}
+section \<open>Action signatures\<close>
theory Asig
imports Main
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller, Konrad Slind, Tobias Nipkow
*)
-section {* The I/O automata of Lynch and Tuttle in HOLCF *}
+section \<open>The I/O automata of Lynch and Tuttle in HOLCF\<close>
theory Automata
imports Asig
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Compositionality on Execution level *}
+section \<open>Compositionality on Execution level\<close>
theory CompoExecs
imports Traces
@@ -215,7 +215,7 @@
--> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
(* main case *)
apply (auto simp add: trans_of_defs2)
done
@@ -229,8 +229,8 @@
--> stutter (asig_of A) (fst s,ProjA2$xs) &
stutter (asig_of B) (snd s,ProjB2$xs)"
-apply (tactic {* pair_induct_tac @{context} "xs"
- [@{thm stutter_def}, @{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs"
+ [@{thm stutter_def}, @{thm is_exec_frag_def}] 1\<close>)
(* main case *)
apply (auto simp add: trans_of_defs2)
done
@@ -243,8 +243,8 @@
lemma lemma_1_1c: "!s. (is_exec_frag (A\<parallel>B) (s,xs)
--> Forall (%x. fst x:act (A\<parallel>B)) xs)"
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
- @{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
+ @{thm is_exec_frag_def}] 1\<close>)
(* main case *)
apply auto
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
@@ -263,13 +263,13 @@
Forall (%x. fst x:act (A\<parallel>B)) xs
--> is_exec_frag (A\<parallel>B) (s,xs)"
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
- @{thm is_exec_frag_def}, @{thm stutter_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
+ @{thm is_exec_frag_def}, @{thm stutter_def}] 1\<close>)
apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
done
-subsection {* COMPOSITIONALITY on EXECUTION Level -- Main Theorem *}
+subsection \<open>COMPOSITIONALITY on EXECUTION Level -- Main Theorem\<close>
lemma compositionality_ex:
"(ex:executions(A\<parallel>B)) =
@@ -279,7 +279,7 @@
Forall (%x. fst x:act (A\<parallel>B)) (snd ex))"
apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (rule iffI)
(* ==> *)
apply (erule conjE)+
@@ -290,7 +290,7 @@
done
-subsection {* COMPOSITIONALITY on EXECUTION Level -- for Modules *}
+subsection \<open>COMPOSITIONALITY on EXECUTION Level -- for Modules\<close>
lemma compositionality_ex_modules:
"Execs (A\<parallel>B) = par_execs (Execs A) (Execs B)"
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Compositionality on Schedule level *}
+section \<open>Compositionality on Schedule level\<close>
theory CompoScheds
imports CompoExecs
@@ -149,7 +149,7 @@
mkex2_cons_2 [simp] mkex2_cons_3 [simp]
-subsection {* mkex *}
+subsection \<open>mkex\<close>
lemma mkex_UU: "mkex A B UU (s,exA) (t,exB) = ((s,t),UU)"
apply (simp add: mkex_def)
@@ -191,7 +191,7 @@
declare composch_simps [simp]
-subsection {* COMPOSITIONALITY on SCHEDULE Level *}
+subsection \<open>COMPOSITIONALITY on SCHEDULE Level\<close>
subsubsection "Lemmas for ==>"
@@ -215,7 +215,7 @@
lemma lemma_2_1b:
"filter_act$(ProjA2$xs) =filter_act$xs &
filter_act$(ProjB2$xs) =filter_act$xs"
-apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
done
@@ -230,8 +230,8 @@
lemma sch_actions_in_AorB: "!s. is_exec_frag (A\<parallel>B) (s,xs)
--> Forall (%x. x:act (A\<parallel>B)) (filter_act$xs)"
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
- @{thm sforall_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
+ @{thm sforall_def}] 1\<close>)
(* main case *)
apply auto
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
@@ -251,20 +251,20 @@
Filter (%a. a:act B)$sch << filter_act$exB
--> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"
-apply (tactic {* Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
- @{thm sforall_def}, @{thm mkex_def}] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
+ @{thm sforall_def}, @{thm mkex_def}] 1\<close>)
(* main case *)
(* splitting into 4 cases according to a:A, a:B *)
apply auto
(* Case y:A, y:B *)
-apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
(* Case exA=UU, Case exA=nil*)
(* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA
is used! --> to generate a contradiction using ~a\<leadsto>ss<< UU(nil), using theorems
Cons_not_less_UU and Cons_not_less_nil *)
-apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
(* Case exA=a\<leadsto>x, exB=b\<leadsto>y *)
(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case,
as otherwise mkex_cons_3 would not be rewritten without use of rotate_tac: then tactic
@@ -272,11 +272,11 @@
apply simp
(* Case y:A, y~:B *)
-apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
apply simp
(* Case y~:A, y:B *)
-apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
apply simp
(* Case y~:A, y~:B *)
@@ -286,7 +286,7 @@
(* generalizing the proof above to a proof method *)
-ML {*
+ML \<open>
local
val defs = [@{thm Filter_def}, @{thm Forall_def}, @{thm sforall_def}, @{thm mkex_def},
@@ -310,12 +310,12 @@
]
end
-*}
+\<close>
-method_setup mkex_induct = {*
+method_setup mkex_induct = \<open>
Scan.lift (Args.name -- Args.name -- Args.name)
>> (fn ((sch, exA), exB) => fn ctxt => SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
-*}
+\<close>
(*---------------------------------------------------------------------------
@@ -393,7 +393,7 @@
--------------------------------------------------------------------------- *)
lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
-apply (tactic {* Seq_induct_tac @{context} "y" [] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "y" [] 1\<close>)
done
@@ -421,8 +421,8 @@
Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
apply (simp add: ProjA_def Filter_ex_def)
-apply (tactic {* pair_tac @{context} "exA" 1 *})
-apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
apply (rule conjI)
apply (simp (no_asm) add: mkex_def)
apply (simplesubst trick_against_eq_in_ass)
@@ -462,8 +462,8 @@
Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
apply (simp add: ProjB_def Filter_ex_def)
-apply (tactic {* pair_tac @{context} "exA" 1 *})
-apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
apply (rule conjI)
apply (simp (no_asm) add: mkex_def)
apply (simplesubst trick_against_eq_in_ass)
@@ -508,7 +508,7 @@
apply (simp add: compositionality_ex)
apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
apply (simp add: executions_def)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (erule conjE)
apply (simp add: sch_actions_in_AorB)
@@ -519,20 +519,20 @@
apply (rename_tac exA exB)
apply (rule_tac x = "mkex A B sch exA exB" in bexI)
(* mkex actions are just the oracle *)
-apply (tactic {* pair_tac @{context} "exA" 1 *})
-apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
apply (simp add: Mapfst_mkex_is_sch)
(* mkex is an execution -- use compositionality on ex-level *)
apply (simp add: compositionality_ex)
apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
-apply (tactic {* pair_tac @{context} "exA" 1 *})
-apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
apply (simp add: mkex_actions_in_AorB)
done
-subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *}
+subsection \<open>COMPOSITIONALITY on SCHEDULE Level -- for Modules\<close>
lemma compositionality_sch_modules:
"Scheds (A\<parallel>B) = par_scheds (Scheds A) (Scheds B)"
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Compositionality on Trace level *}
+section \<open>Compositionality on Trace level\<close>
theory CompoTraces
imports CompoScheds ShortExecutions
@@ -70,7 +70,7 @@
by (blast intro: finiteR_mksch)
-declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE))) *}
+declaration \<open>fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE)))\<close>
subsection "mksch rewrite rules"
@@ -165,7 +165,7 @@
declare compotr_simps [simp]
-subsection {* COMPOSITIONALITY on TRACE Level *}
+subsection \<open>COMPOSITIONALITY on TRACE Level\<close>
subsubsection "Lemmata for ==>"
@@ -201,8 +201,8 @@
"!!A B. compatible A B ==>
! schA schB. Forall (%x. x:act (A\<parallel>B)) tr
--> Forall (%x. x:act (A\<parallel>B)) (mksch A B$tr$schA$schB)"
-apply (tactic {* Seq_induct_tac @{context} "tr"
- [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "tr"
+ [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
apply auto
apply (simp add: actions_of_par)
apply (case_tac "a:act A")
@@ -229,8 +229,8 @@
lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A ==>
! schA schB. (Forall (%x. x:act B & x~:act A) tr
--> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
-apply (tactic {* Seq_induct_tac @{context} "tr"
- [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "tr"
+ [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
apply auto
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: intA_is_not_actB int_is_act)
@@ -239,8 +239,8 @@
lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>
! schA schB. (Forall (%x. x:act A & x~:act B) tr
--> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
-apply (tactic {* Seq_induct_tac @{context} "tr"
- [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "tr"
+ [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
apply auto
apply (rule Forall_Conc_impl [THEN mp])
apply (simp add: intA_is_not_actB int_is_act)
@@ -414,8 +414,8 @@
Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB
--> Filter (%a. a:ext (A\<parallel>B))$(mksch A B$tr$schA$schB) = tr"
-apply (tactic {* Seq_induct_tac @{context} "tr"
- [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "tr"
+ [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
(* main case *)
(* splitting into 4 cases according to a:A, a:B *)
apply auto
@@ -955,7 +955,7 @@
-subsection {* COMPOSITIONALITY on TRACE Level -- for Modules *}
+subsection \<open>COMPOSITIONALITY on TRACE Level -- for Modules\<close>
lemma compositionality_tr_modules:
@@ -970,7 +970,7 @@
done
-declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym) *}
+declaration \<open>fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym)\<close>
end
--- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Compositionality of I/O automata *}
+section \<open>Compositionality of I/O automata\<close>
theory Compositionality
imports CompoTraces
begin
--- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,13 +2,13 @@
Author: Olaf Müller
*)
-section {* Deadlock freedom of I/O Automata *}
+section \<open>Deadlock freedom of I/O Automata\<close>
theory Deadlock
imports RefCorrectness CompoScheds
begin
-text {* input actions may always be added to a schedule *}
+text \<open>input actions may always be added to a schedule\<close>
lemma scheds_input_enabled:
"[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|]
@@ -17,7 +17,7 @@
apply auto
apply (frule inp_is_act)
apply (simp add: executions_def)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (rename_tac s ex)
apply (subgoal_tac "Finite ex")
prefer 2
@@ -47,12 +47,12 @@
apply assumption
done
-text {*
+text \<open>
Deadlock freedom: component B cannot block an out or int action
of component A in every schedule.
Needs compositionality on schedule level, input-enabledness, compatibility
and distributivity of is_exec_frag over @@
-*}
+\<close>
declare split_if [split del]
lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A\<parallel>B);
--- a/src/HOL/HOLCF/IOA/meta_theory/IOA.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/IOA.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* The theory of I/O automata in HOLCF *}
+section \<open>The theory of I/O automata in HOLCF\<close>
theory IOA
imports SimCorrectness Compositionality Deadlock
--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Live I/O automata -- specified by temproal formulas *}
+section \<open>Live I/O automata -- specified by temproal formulas\<close>
theory LiveIOA
imports TLS
@@ -61,14 +61,14 @@
apply (rule_tac x = "corresp_ex A f ex" in exI)
apply auto
(* Traces coincide, Lemma 1 *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (erule lemma_1 [THEN spec, THEN mp])
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
apply (simp add: executions_def reachable.reachable_0)
(* corresp_ex is execution, Lemma 2 *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (simp add: executions_def)
(* start state *)
apply (rule conjI)
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Logical Connectives lifted to predicates *}
+section \<open>Logical Connectives lifted to predicates\<close>
theory Pred
imports Main
--- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Correctness of Refinement Mappings in HOLCF/IOA *}
+section \<open>Correctness of Refinement Mappings in HOLCF/IOA\<close>
theory RefCorrectness
imports RefMappings
@@ -180,7 +180,7 @@
!s. reachable C s & is_exec_frag C (s,xs) -->
mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))"
apply (unfold corresp_ex_def)
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
(* cons case *)
apply (auto simp add: mk_traceConc)
apply (frule reachable.reachable_n)
@@ -208,7 +208,7 @@
--> is_exec_frag A (s,xs @@ ys))"
apply (rule impI)
-apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
+apply (tactic \<open>Seq_Finite_induct_tac @{context} 1\<close>)
(* main case *)
apply (auto simp add: split_paired_all)
done
@@ -228,7 +228,7 @@
apply (unfold corresp_ex_def)
apply simp
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
(* main case *)
apply auto
apply (rule_tac t = "f x2" in lemma_2_1)
@@ -271,13 +271,13 @@
apply (rule_tac x = "corresp_ex A f ex" in bexI)
(* Traces coincide, Lemma 1 *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (erule lemma_1 [THEN spec, THEN mp])
apply assumption+
apply (simp add: executions_def reachable.reachable_0)
(* corresp_ex is execution, Lemma 2 *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (simp add: executions_def)
(* start state *)
apply (rule conjI)
@@ -322,13 +322,13 @@
apply auto
(* Traces coincide, Lemma 1 *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (erule lemma_1 [THEN spec, THEN mp])
apply assumption+
apply (simp add: executions_def reachable.reachable_0)
(* corresp_ex is execution, Lemma 2 *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (simp add: executions_def)
(* start state *)
apply (rule conjI)
@@ -349,14 +349,14 @@
apply auto
(* Traces coincide, Lemma 1 *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (erule lemma_1 [THEN spec, THEN mp])
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
apply (simp add: executions_def reachable.reachable_0)
(* corresp_ex is execution, Lemma 2 *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (simp add: executions_def)
(* start state *)
apply (rule conjI)
--- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Refinement Mappings in HOLCF/IOA *}
+section \<open>Refinement Mappings in HOLCF/IOA\<close>
theory RefMappings
imports Traces
--- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
+section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close>
theory Seq
imports "../../HOLCF"
@@ -51,9 +51,9 @@
"Infinite x == ~(seq_finite x)"
-subsection {* recursive equations of operators *}
+subsection \<open>recursive equations of operators\<close>
-subsubsection {* smap *}
+subsubsection \<open>smap\<close>
fixrec
smap :: "('a -> 'b) -> 'a seq -> 'b seq"
@@ -64,7 +64,7 @@
lemma smap_UU [simp]: "smap$f$UU=UU"
by fixrec_simp
-subsubsection {* sfilter *}
+subsubsection \<open>sfilter\<close>
fixrec
sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
@@ -77,7 +77,7 @@
lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
by fixrec_simp
-subsubsection {* sforall2 *}
+subsubsection \<open>sforall2\<close>
fixrec
sforall2 :: "('a -> tr) -> 'a seq -> tr"
@@ -92,7 +92,7 @@
definition
sforall_def: "sforall P t == (sforall2$P$t ~=FF)"
-subsubsection {* stakewhile *}
+subsubsection \<open>stakewhile\<close>
fixrec
stakewhile :: "('a -> tr) -> 'a seq -> 'a seq"
@@ -105,7 +105,7 @@
lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
by fixrec_simp
-subsubsection {* sdropwhile *}
+subsubsection \<open>sdropwhile\<close>
fixrec
sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq"
@@ -118,7 +118,7 @@
lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
by fixrec_simp
-subsubsection {* slast *}
+subsubsection \<open>slast\<close>
fixrec
slast :: "'a seq -> 'a"
@@ -130,7 +130,7 @@
lemma slast_UU [simp]: "slast$UU=UU"
by fixrec_simp
-subsubsection {* sconc *}
+subsubsection \<open>sconc\<close>
fixrec
sconc :: "'a seq -> 'a seq -> 'a seq"
@@ -153,7 +153,7 @@
declare sconc_cons' [simp del]
-subsubsection {* sflat *}
+subsubsection \<open>sflat\<close>
fixrec
sflat :: "('a seq) seq -> 'a seq"
@@ -169,7 +169,7 @@
declare sflat_cons' [simp del]
-subsubsection {* szip *}
+subsubsection \<open>szip\<close>
fixrec
szip :: "'a seq -> 'b seq -> ('a*'b) seq"
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Wed Dec 30 21:57:52 2015 +0100
@@ -93,7 +93,7 @@
by (simp add: Map_def Consq_def flift2_def)
-subsubsection {* Filter *}
+subsubsection \<open>Filter\<close>
lemma Filter_UU: "Filter P$UU =UU"
by (simp add: Filter_def)
@@ -106,7 +106,7 @@
by (simp add: Filter_def Consq_def flift2_def If_and_if)
-subsubsection {* Forall *}
+subsubsection \<open>Forall\<close>
lemma Forall_UU: "Forall P UU"
by (simp add: Forall_def sforall_def)
@@ -118,13 +118,13 @@
by (simp add: Forall_def sforall_def Consq_def flift2_def)
-subsubsection {* Conc *}
+subsubsection \<open>Conc\<close>
lemma Conc_cons: "(x\<leadsto>xs) @@ y = x\<leadsto>(xs @@y)"
by (simp add: Consq_def)
-subsubsection {* Takewhile *}
+subsubsection \<open>Takewhile\<close>
lemma Takewhile_UU: "Takewhile P$UU =UU"
by (simp add: Takewhile_def)
@@ -137,7 +137,7 @@
by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
-subsubsection {* DropWhile *}
+subsubsection \<open>DropWhile\<close>
lemma Dropwhile_UU: "Dropwhile P$UU =UU"
by (simp add: Dropwhile_def)
@@ -150,7 +150,7 @@
by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
-subsubsection {* Last *}
+subsubsection \<open>Last\<close>
lemma Last_UU: "Last$UU =UU"
by (simp add: Last_def)
@@ -165,7 +165,7 @@
done
-subsubsection {* Flat *}
+subsubsection \<open>Flat\<close>
lemma Flat_UU: "Flat$UU =UU"
by (simp add: Flat_def)
@@ -177,7 +177,7 @@
by (simp add: Flat_def Consq_def)
-subsubsection {* Zip *}
+subsubsection \<open>Zip\<close>
lemma Zip_unfold:
"Zip = (LAM t1 t2. case t1 of
@@ -1075,7 +1075,7 @@
done
-ML {*
+ML \<open>
fun Seq_case_tac ctxt s i =
Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_cases} i
@@ -1109,6 +1109,6 @@
THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1))))
THEN simp_tac (ctxt addsimps rws) i;
-*}
+\<close>
end
--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Dec 30 21:57:52 2015 +0100
@@ -6,12 +6,12 @@
imports Traces
begin
-text {*
- Some properties about @{text "Cut ex"}, defined as follows:
+text \<open>
+ Some properties about \<open>Cut ex\<close>, defined as follows:
- For every execution ex there is another shorter execution @{text "Cut ex"}
+ For every execution ex there is another shorter execution \<open>Cut ex\<close>
that has the same trace as ex, but its schedule ends with an external action.
-*}
+\<close>
definition
oraclebuild :: "('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" where
@@ -47,12 +47,12 @@
LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
-ML {*
+ML \<open>
fun thin_tac' ctxt j =
rotate_tac (j - 1) THEN'
eresolve_tac ctxt [thin_rl] THEN'
rotate_tac (~ (j - 1))
-*}
+\<close>
subsection "oraclebuild rewrite rules"
@@ -225,7 +225,7 @@
apply auto
apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
apply (simp add: executions_def)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply auto
apply (rule_tac x = " (x1,Cut (%a. fst a:ext A) x2) " in exI)
apply (simp (no_asm_simp))
--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Correctness of Simulations in HOLCF/IOA *}
+section \<open>Correctness of Simulations in HOLCF/IOA\<close>
theory SimCorrectness
imports Simulations
@@ -156,7 +156,7 @@
done
-subsection {* TRACE INCLUSION Part 1: Traces coincide *}
+subsection \<open>TRACE INCLUSION Part 1: Traces coincide\<close>
subsubsection "Lemmata for <=="
@@ -170,7 +170,7 @@
!s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
-apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>)
(* cons case *)
apply auto
apply (rename_tac ex a t s s')
@@ -195,7 +195,7 @@
!s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R
--> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"
-apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>)
(* main case *)
apply auto
apply (rename_tac ex a t s s')
@@ -265,7 +265,7 @@
apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
(* Traces coincide, Lemma 1 *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (rename_tac s ex)
apply (simp (no_asm) add: corresp_ex_sim_def)
apply (rule_tac s = "s" in traces_coincide_sim)
@@ -273,7 +273,7 @@
apply (simp add: executions_def reachable.reachable_0 sim_starts1)
(* corresp_ex_sim is execution, Lemma 2 *)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
apply (simp add: executions_def)
apply (rename_tac s ex)
--- a/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Simulations in HOLCF/IOA *}
+section \<open>Simulations in HOLCF/IOA\<close>
theory Simulations
imports RefCorrectness
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* A General Temporal Logic *}
+section \<open>A General Temporal Logic\<close>
theory TL
imports Pred Sequence
@@ -147,7 +147,7 @@
"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s"
apply (unfold tsuffix_def suffix_def)
apply auto
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
apply (rule_tac x = "a\<leadsto>s1" in exI)
apply auto
done
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Temporal Logic of Steps -- tailored for I/O automata *}
+section \<open>Temporal Logic of Steps -- tailored for I/O automata\<close>
theory TLS
imports IOA TL
@@ -92,10 +92,10 @@
lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
-setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
+setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
-subsection {* ex2seqC *}
+subsection \<open>ex2seqC\<close>
lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of
nil => (s,None,s)\<leadsto>nil
@@ -151,13 +151,13 @@
lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
-apply (tactic {* pair_tac @{context} "exec" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "exec" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
done
-subsection {* Interface TL -- TLS *}
+subsection \<open>Interface TL -- TLS\<close>
(* uses the fact that in executions states overlap, which is lost in
after the translation via ex2seq !! *)
@@ -172,31 +172,31 @@
apply (simp split add: split_if)
(* TL = UU *)
apply (rule conjI)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
(* TL = nil *)
apply (rule conjI)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_tac @{context} "x2" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_tac @{context} "x2" 1\<close>)
apply (simp add: unlift_def)
apply fast
apply (simp add: unlift_def)
apply fast
apply (simp add: unlift_def)
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
(* TL =cons *)
apply (simp add: unlift_def)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
done
end
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
Author: Olaf Müller
*)
-section {* Executions and Traces of I/O automata in HOLCF *}
+section \<open>Executions and Traces of I/O automata in HOLCF\<close>
theory Traces
imports Sequence Automata
@@ -203,7 +203,7 @@
lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
declare Let_def [simp]
-setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
+setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
lemmas exec_rws = executions_def is_exec_frag_def
@@ -367,8 +367,8 @@
lemma execfrag_in_sig:
"!! A. is_trans_of A ==>
! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)"
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
- @{thm Forall_def}, @{thm sforall_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
+ @{thm Forall_def}, @{thm sforall_def}] 1\<close>)
(* main case *)
apply (auto simp add: is_trans_of_def)
done
@@ -377,7 +377,7 @@
"!! A.[| is_trans_of A; x:executions A |] ==>
Forall (%a. a:act A) (filter_act$(snd x))"
apply (simp add: executions_def)
-apply (tactic {* pair_tac @{context} "x" 1 *})
+apply (tactic \<open>pair_tac @{context} "x" 1\<close>)
apply (rule execfrag_in_sig [THEN spec, THEN mp])
apply auto
done
@@ -394,10 +394,10 @@
(* only admissible in y, not if done in x !! *)
lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x --> is_exec_frag A (s,y)"
-apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1\<close>)
apply (intro strip)
-apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
apply auto
done
@@ -409,10 +409,10 @@
lemma exec_prefix2closed [rule_format]:
"! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)"
-apply (tactic {* pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1\<close>)
apply (intro strip)
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
apply auto
done