src/HOL/Hoare_Parallel/RG_Tran.thy
changeset 42174 d0be2722ce9f
parent 41842 d8f76db6a207
child 51119 6b2352111017
     1.1 --- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Mar 30 22:53:18 2011 +0200
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Mar 30 23:26:40 2011 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  subsubsection {* Environment transitions *}
     1.6  
     1.7 -types 'a conf = "(('a com) option) \<times> 'a"
     1.8 +type_synonym 'a conf = "(('a com) option) \<times> 'a"
     1.9  
    1.10  inductive_set
    1.11    etran :: "('a conf \<times> 'a conf) set" 
    1.12 @@ -48,7 +48,7 @@
    1.13  
    1.14  subsection {* Semantics of Parallel Programs *}
    1.15  
    1.16 -types 'a par_conf = "('a par_com) \<times> 'a"
    1.17 +type_synonym 'a par_conf = "('a par_com) \<times> 'a"
    1.18  
    1.19  inductive_set
    1.20    par_etran :: "('a par_conf \<times> 'a par_conf) set"
    1.21 @@ -73,9 +73,9 @@
    1.22  
    1.23  subsubsection {* Sequential computations *}
    1.24  
    1.25 -types 'a confs = "('a conf) list"
    1.26 +type_synonym 'a confs = "'a conf list"
    1.27  
    1.28 -inductive_set cptn :: "('a confs) set"
    1.29 +inductive_set cptn :: "'a confs set"
    1.30  where
    1.31    CptnOne: "[(P,s)] \<in> cptn"
    1.32  | CptnEnv: "(P, t)#xs \<in> cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> cptn"
    1.33 @@ -86,9 +86,9 @@
    1.34  
    1.35  subsubsection {* Parallel computations *}
    1.36  
    1.37 -types  'a par_confs = "('a par_conf) list"
    1.38 +type_synonym 'a par_confs = "'a par_conf list"
    1.39  
    1.40 -inductive_set par_cptn :: "('a par_confs) set"
    1.41 +inductive_set par_cptn :: "'a par_confs set"
    1.42  where
    1.43    ParCptnOne: "[(P,s)] \<in> par_cptn"
    1.44  | ParCptnEnv: "(P,t)#xs \<in> par_cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> par_cptn"
    1.45 @@ -363,7 +363,8 @@
    1.46  
    1.47  subsection {* Validity for Component Programs. *}
    1.48  
    1.49 -types 'a rgformula = "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
    1.50 +type_synonym 'a rgformula =
    1.51 +  "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
    1.52  
    1.53  definition assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a confs) set" where
    1.54    "assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow>