# HG changeset patch
# User wenzelm
# Date 1451509500 -3600
# Node ID ba465fcd02674f1d83c7b4c07b676a487103827a
# Parent  f1599e98c4d08c369303af5a68d5e4d5936a219f
more symbols;

diff -r f1599e98c4d0 -r ba465fcd0267 src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
--- 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
diff -r f1599e98c4d0 -r ba465fcd0267 src/HOL/HOLCF/IOA/meta_theory/Automata.thy
--- 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
 
diff -r f1599e98c4d0 -r ba465fcd0267 src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy
--- 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)
diff -r f1599e98c4d0 -r ba465fcd0267 src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- 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)
diff -r f1599e98c4d0 -r ba465fcd0267 src/HOL/HOLCF/IOA/meta_theory/Simulations.thy
--- 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'))))"
 
diff -r f1599e98c4d0 -r ba465fcd0267 src/HOL/HOLCF/IOA/meta_theory/TLS.thy
--- 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)