src/HOL/Hoare_Parallel/OG_Tran.thy
changeset 52141 eff000cab70f
parent 46362 b2878f059f91
child 58884 be4d203d35b3
equal deleted inserted replaced
52140:88a69da5d3fa 52141:eff000cab70f
    88 
    88 
    89 definition ann_sem :: "'a ann_com \<Rightarrow> 'a \<Rightarrow> 'a set" where
    89 definition ann_sem :: "'a ann_com \<Rightarrow> 'a \<Rightarrow> 'a set" where
    90   "ann_sem c \<equiv> \<lambda>s. {t. (Some c, s) -*\<rightarrow> (None, t)}"
    90   "ann_sem c \<equiv> \<lambda>s. {t. (Some c, s) -*\<rightarrow> (None, t)}"
    91 
    91 
    92 definition ann_SEM :: "'a ann_com \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    92 definition ann_SEM :: "'a ann_com \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    93   "ann_SEM c S \<equiv> \<Union>ann_sem c ` S"  
    93   "ann_SEM c S \<equiv> \<Union>(ann_sem c ` S)"
    94 
    94 
    95 definition sem :: "'a com \<Rightarrow> 'a \<Rightarrow> 'a set" where
    95 definition sem :: "'a com \<Rightarrow> 'a \<Rightarrow> 'a set" where
    96   "sem c \<equiv> \<lambda>s. {t. \<exists>Ts. (c, s) -P*\<rightarrow> (Parallel Ts, t) \<and> All_None Ts}"
    96   "sem c \<equiv> \<lambda>s. {t. \<exists>Ts. (c, s) -P*\<rightarrow> (Parallel Ts, t) \<and> All_None Ts}"
    97 
    97 
    98 definition SEM :: "'a com \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    98 definition SEM :: "'a com \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    99   "SEM c S \<equiv> \<Union>sem c ` S "
    99   "SEM c S \<equiv> \<Union>(sem c ` S)"
   100 
   100 
   101 abbreviation Omega :: "'a com"    ("\<Omega>" 63)
   101 abbreviation Omega :: "'a com"    ("\<Omega>" 63)
   102   where "\<Omega> \<equiv> While UNIV UNIV (Basic id)"
   102   where "\<Omega> \<equiv> While UNIV UNIV (Basic id)"
   103 
   103 
   104 primrec fwhile :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> nat \<Rightarrow> 'a com" where
   104 primrec fwhile :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> nat \<Rightarrow> 'a com" where