--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Wed Dec 30 21:57:52 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy Wed Dec 30 22:05:00 2015 +0100
@@ -22,8 +22,8 @@
is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
"is_abstraction f C A =
((!s:starts_of(C). f(s):starts_of(A)) &
- (!s t a. reachable C s & s -a--C-> t
- --> (f s) -a--A-> (f t)))"
+ (!s t a. reachable C s & s \<midarrow>a\<midarrow>C\<rightarrow> t
+ --> (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t)))"
definition
weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" where
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Dec 30 21:57:52 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Dec 30 22:05:00 2015 +0100
@@ -78,11 +78,8 @@
| reachable_n: "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t"
abbreviation
- trans_of_syn ("_ -_--_-> _" [81,81,81,81] 100) where
- "s -a--A-> t == (s,a,t):trans_of A"
-
-notation (xsymbols)
- trans_of_syn ("_ \<midarrow>_\<midarrow>_\<longrightarrow> _" [81,81,81,81] 100)
+ trans_of_syn ("_ \<midarrow>_\<midarrow>_\<rightarrow> _" [81,81,81,81] 100) where
+ "s \<midarrow>a\<midarrow>A\<rightarrow> t == (s,a,t):trans_of A"
abbreviation "act A == actions (asig_of A)"
abbreviation "ext A == externals (asig_of A)"
@@ -218,11 +215,11 @@
input_resistant_def:
"input_resistant A == ! W : sfair_of A. ! s a t.
reachable A s & reachable A t & a:inp A &
- Enabled A W s & s -a--A-> t
+ Enabled A W s & s \<midarrow>a\<midarrow>A\<rightarrow> t
--> Enabled A W t"
enabled_def:
- "enabled A a s == ? t. s-a--A-> t"
+ "enabled A a s == ? t. s \<midarrow>a\<midarrow>A\<rightarrow> t"
Enabled_def:
"Enabled A W s == ? w:W. enabled A w s"
@@ -230,10 +227,10 @@
en_persistent_def:
"en_persistent A W == ! s a t. Enabled A W s &
a ~:W &
- s -a--A-> t
+ s \<midarrow>a\<midarrow>A\<rightarrow> t
--> Enabled A W t"
was_enabled_def:
- "was_enabled A a t == ? s. s-a--A-> t"
+ "was_enabled A a t == ? s. s \<midarrow>a\<midarrow>A\<rightarrow> t"
set_was_enabled_def:
"set_was_enabled A W t == ? w:W. was_enabled A w t"
@@ -524,7 +521,7 @@
subsection "rename"
-lemma trans_rename: "s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)"
+lemma trans_rename: "s \<midarrow>a\<midarrow>(rename C f)\<rightarrow> t ==> (? x. Some(x) = f(a) & s \<midarrow>x\<midarrow>C\<rightarrow> t)"
apply (simp add: Let_def rename_def trans_of_def)
done
--- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy Wed Dec 30 21:57:52 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy Wed Dec 30 22:05:00 2015 +0100
@@ -22,7 +22,7 @@
"is_ref_map f C A =
((!s:starts_of(C). f(s):starts_of(A)) &
(!s t a. reachable C s &
- s -a--C-> t
+ s \<midarrow>a\<midarrow>C\<rightarrow> t
--> (? ex. move A ex (f s) a (f t))))"
definition
@@ -30,16 +30,16 @@
"is_weak_ref_map f C A =
((!s:starts_of(C). f(s):starts_of(A)) &
(!s t a. reachable C s &
- s -a--C-> t
+ s \<midarrow>a\<midarrow>C\<rightarrow> t
--> (if a:ext(C)
- then (f s) -a--A-> (f t)
+ then (f s) \<midarrow>a\<midarrow>A\<rightarrow> (f t)
else (f s)=(f t))))"
subsection "transitions and moves"
-lemma transition_is_ex: "s -a--A-> t ==> ? ex. move A ex s a t"
+lemma transition_is_ex: "s \<midarrow>a\<midarrow>A\<rightarrow> t ==> ? ex. move A ex s a t"
apply (rule_tac x = " (a,t) \<leadsto>nil" in exI)
apply (simp add: move_def)
done
@@ -51,14 +51,14 @@
done
-lemma ei_transitions_are_ex: "(s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A)
+lemma ei_transitions_are_ex: "(s \<midarrow>a\<midarrow>A\<rightarrow> s') & (s' \<midarrow>a'\<midarrow>A\<rightarrow> s'') & (~a':ext A)
==> ? ex. move A ex s a s''"
apply (rule_tac x = " (a,s') \<leadsto> (a',s'') \<leadsto>nil" in exI)
apply (simp add: move_def)
done
-lemma eii_transitions_are_ex: "(s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &
+lemma eii_transitions_are_ex: "(s1 \<midarrow>a1\<midarrow>A\<rightarrow> s2) & (s2 \<midarrow>a2\<midarrow>A\<rightarrow> s3) & (s3 \<midarrow>a3\<midarrow>A\<rightarrow> s4) &
(~a2:ext A) & (~a3:ext A) ==>
? ex. move A ex s1 a1 s4"
apply (rule_tac x = " (a1,s2) \<leadsto> (a2,s3) \<leadsto> (a3,s4) \<leadsto>nil" in exI)
--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Dec 30 21:57:52 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy Wed Dec 30 22:05:00 2015 +0100
@@ -76,7 +76,7 @@
declare Let_def [simp del]
lemma move_is_move_sim:
- "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>
+ "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
(t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'"
apply (unfold is_simulation_def)
@@ -105,7 +105,7 @@
declare Let_def [simp]
lemma move_subprop1_sim:
- "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
+ "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
is_exec_frag A (s',@x. move A x s' a T')"
apply (cut_tac move_is_move_sim)
@@ -115,7 +115,7 @@
done
lemma move_subprop2_sim:
- "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
+ "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
Finite (@x. move A x s' a T')"
apply (cut_tac move_is_move_sim)
@@ -125,7 +125,7 @@
done
lemma move_subprop3_sim:
- "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
+ "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
laststate (s',@x. move A x s' a T') = T'"
apply (cut_tac move_is_move_sim)
@@ -135,7 +135,7 @@
done
lemma move_subprop4_sim:
- "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
+ "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
mk_trace A$((@x. move A x s' a T')) =
(if a:ext A then a\<leadsto>nil else nil)"
@@ -146,7 +146,7 @@
done
lemma move_subprop5_sim:
- "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
+ "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==>
let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
(t,T'):R"
apply (cut_tac move_is_move_sim)
--- a/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy Wed Dec 30 21:57:52 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy Wed Dec 30 22:05:00 2015 +0100
@@ -15,7 +15,7 @@
"is_simulation R C A =
((!s:starts_of C. R``{s} Int starts_of A ~= {}) &
(!s s' t a. reachable C s &
- s -a--C-> t &
+ s \<midarrow>a\<midarrow>C\<rightarrow> t &
(s,s') : R
--> (? t' ex. (t,t'):R & move A ex s' a t')))"
@@ -24,7 +24,7 @@
"is_backward_simulation R C A =
((!s:starts_of C. R``{s} <= starts_of A) &
(!s t t' a. reachable C s &
- s -a--C-> t &
+ s \<midarrow>a\<midarrow>C\<rightarrow> t &
(t,t') : R
--> (? ex s'. (s,s'):R & move A ex s' a t')))"
@@ -33,7 +33,7 @@
"is_forw_back_simulation R C A =
((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &
(!s S' t a. reachable C s &
- s -a--C-> t &
+ s \<midarrow>a\<midarrow>C\<rightarrow> t &
(s,S') : R
--> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))"
@@ -42,7 +42,7 @@
"is_back_forw_simulation R C A =
((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &
(!s t T' a. reachable C s &
- s -a--C-> t &
+ s \<midarrow>a\<midarrow>C\<rightarrow> t &
(t,T') : R
--> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))"
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Dec 30 21:57:52 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Dec 30 22:05:00 2015 +0100
@@ -163,8 +163,8 @@
after the translation via ex2seq !! *)
lemma TL_TLS:
- "[| ! s a t. (P s) & s-a--A-> t --> (Q t) |]
- ==> ex \<TTurnstile> (Init (%(s,a,t). P s) \<^bold>\<and> Init (%(s,a,t). s -a--A-> t)
+ "[| ! s a t. (P s) & s \<midarrow>a\<midarrow>A\<rightarrow> t --> (Q t) |]
+ ==> ex \<TTurnstile> (Init (%(s,a,t). P s) \<^bold>\<and> Init (%(s,a,t). s \<midarrow>a\<midarrow>A\<rightarrow> t)
\<^bold>\<longrightarrow> (Next (Init (%(s,a,t).Q s))))"
apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)