# HG changeset patch
# User wenzelm
# Date 1301520400 -7200
# Node ID d0be2722ce9f360a582df76003bc084268f056e0
# Parent  5d33c12ccf2292c9c18bb26e3759289707200568
modernized specifications;

diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -13,9 +13,8 @@
 uses ("hoare_syntax.ML") ("hoare_tac.ML")
 begin
 
-types
-    'a bexp = "'a set"
-    'a assn = "'a set"
+type_synonym 'a bexp = "'a set"
+type_synonym 'a assn = "'a set"
 
 datatype
  'a com = Basic "'a \<Rightarrow> 'a"
@@ -25,7 +24,7 @@
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
-types 'a sem = "'a => 'a => bool"
+type_synonym 'a sem = "'a => 'a => bool"
 
 inductive Sem :: "'a com \<Rightarrow> 'a sem"
 where
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -10,9 +10,8 @@
 uses ("hoare_syntax.ML") ("hoare_tac.ML")
 begin
 
-types
-    'a bexp = "'a set"
-    'a assn = "'a set"
+type_synonym 'a bexp = "'a set"
+type_synonym 'a assn = "'a set"
 
 datatype
  'a com = Basic "'a \<Rightarrow> 'a"
@@ -23,7 +22,7 @@
 
 abbreviation annskip ("SKIP") where "SKIP == Basic id"
 
-types 'a sem = "'a option => 'a option => bool"
+type_synonym 'a sem = "'a option => 'a option => bool"
 
 inductive Sem :: "'a com \<Rightarrow> 'a sem"
 where
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/Hoare/SepLogHeap.thy
--- a/src/HOL/Hoare/SepLogHeap.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare/SepLogHeap.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -10,7 +10,7 @@
 imports Main
 begin
 
-types heap = "(nat \<Rightarrow> nat option)"
+type_synonym heap = "(nat \<Rightarrow> nat option)"
 
 text{* @{text "Some"} means allocated, @{text "None"} means
 free. Address @{text "0"} serves as the null reference. *}
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/Hoare_Parallel/Graph.thy
--- a/src/HOL/Hoare_Parallel/Graph.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Graph.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -6,10 +6,9 @@
 
 datatype node = Black | White
 
-types 
-  nodes = "node list"
-  edge  = "nat \<times> nat"
-  edges = "edge list"
+type_synonym nodes = "node list"
+type_synonym edge = "nat \<times> nat"
+type_synonym edges = "edge list"
 
 consts Roots :: "nat set"
 
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/Hoare_Parallel/OG_Com.thy
--- a/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -7,9 +7,8 @@
 
 text {* Type abbreviations for boolean expressions and assertions: *}
 
-types
-    'a bexp = "'a set"
-    'a assn = "'a set"
+type_synonym 'a bexp = "'a set"
+type_synonym 'a assn = "'a set"
 
 text {* The syntax of commands is defined by two mutually recursive
 datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/Hoare_Parallel/OG_Tran.thy
--- a/src/HOL/Hoare_Parallel/OG_Tran.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Tran.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -3,9 +3,8 @@
 
 theory OG_Tran imports OG_Com begin
 
-types
-  'a ann_com_op = "('a ann_com) option"
-  'a ann_triple_op = "('a ann_com_op \<times> 'a assn)"
+type_synonym 'a ann_com_op = "('a ann_com) option"
+type_synonym 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)"
   
 primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
   "com (c, q) = c"
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/Hoare_Parallel/RG_Com.thy
--- a/src/HOL/Hoare_Parallel/RG_Com.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Com.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -10,8 +10,7 @@
 of states.  Syntax of commands @{text com} and parallel commands
 @{text par_com}. *}
 
-types
-  'a bexp = "'a set"
+type_synonym 'a bexp = "'a set"
 
 datatype 'a com = 
     Basic "'a \<Rightarrow>'a"
@@ -20,6 +19,6 @@
   | While "'a bexp" "'a com"       
   | Await "'a bexp" "'a com"                 
 
-types 'a par_com = "(('a com) option) list"
+type_synonym 'a par_com = "'a com option list"
 
 end
\ No newline at end of file
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/Hoare_Parallel/RG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -55,7 +55,8 @@
 
 subsection {* Proof System for Parallel Programs *}
 
-types 'a par_rgformula = "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
+type_synonym 'a par_rgformula =
+  "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
 
 inductive
   par_rghoare :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/Hoare_Parallel/RG_Tran.thy
--- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -8,7 +8,7 @@
 
 subsubsection {* Environment transitions *}
 
-types 'a conf = "(('a com) option) \<times> 'a"
+type_synonym 'a conf = "(('a com) option) \<times> 'a"
 
 inductive_set
   etran :: "('a conf \<times> 'a conf) set" 
@@ -48,7 +48,7 @@
 
 subsection {* Semantics of Parallel Programs *}
 
-types 'a par_conf = "('a par_com) \<times> 'a"
+type_synonym 'a par_conf = "('a par_com) \<times> 'a"
 
 inductive_set
   par_etran :: "('a par_conf \<times> 'a par_conf) set"
@@ -73,9 +73,9 @@
 
 subsubsection {* Sequential computations *}
 
-types 'a confs = "('a conf) list"
+type_synonym 'a confs = "'a conf list"
 
-inductive_set cptn :: "('a confs) set"
+inductive_set cptn :: "'a confs set"
 where
   CptnOne: "[(P,s)] \<in> cptn"
 | CptnEnv: "(P, t)#xs \<in> cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> cptn"
@@ -86,9 +86,9 @@
 
 subsubsection {* Parallel computations *}
 
-types  'a par_confs = "('a par_conf) list"
+type_synonym 'a par_confs = "'a par_conf list"
 
-inductive_set par_cptn :: "('a par_confs) set"
+inductive_set par_cptn :: "'a par_confs set"
 where
   ParCptnOne: "[(P,s)] \<in> par_cptn"
 | ParCptnEnv: "(P,t)#xs \<in> par_cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> par_cptn"
@@ -363,7 +363,8 @@
 
 subsection {* Validity for Component Programs. *}
 
-types 'a rgformula = "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
+type_synonym 'a rgformula =
+  "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
 
 definition assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a confs) set" where
   "assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow> 
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IMP/Com.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -11,11 +11,10 @@
   -- "an unspecified (arbitrary) type of locations 
       (adresses/names) for variables"
       
-types 
-  val   = nat -- "or anything else, @{text nat} used in examples"
-  state = "loc \<Rightarrow> val"
-  aexp  = "state \<Rightarrow> val"  
-  bexp  = "state \<Rightarrow> bool"
+type_synonym val = nat -- "or anything else, @{text nat} used in examples"
+type_synonym state = "loc \<Rightarrow> val"
+type_synonym aexp = "state \<Rightarrow> val"
+type_synonym bexp = "state \<Rightarrow> bool"
   -- "arithmetic and boolean expressions are not modelled explicitly here,"
   -- "they are just functions on states"
 
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IMP/Denotation.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -6,7 +6,7 @@
 
 theory Denotation imports Natural begin
 
-types com_den = "(state\<times>state)set"
+type_synonym com_den = "(state \<times> state) set"
 
 definition
   Gamma :: "[bexp,com_den] => (com_den => com_den)" where
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IMP/Expr.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -14,8 +14,7 @@
 subsection "Arithmetic expressions"
 typedecl loc
 
-types
-  state = "loc => nat"
+type_synonym state = "loc => nat"
 
 datatype
   aexp = N nat
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IMP/Hoare.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -6,7 +6,7 @@
 
 theory Hoare imports Natural begin
 
-types assn = "state => bool"
+type_synonym assn = "state => bool"
 
 inductive
   hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IMP/Machines.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -14,7 +14,7 @@
 text {* There are only three instructions: *}
 datatype instr = SET loc aexp | JMPF bexp nat | JMPB nat
 
-types instrs = "instr list"
+type_synonym instrs = "instr list"
 
 subsection "M0 with PC"
 
@@ -47,7 +47,7 @@
   an operational (small step) semantics:
 *}
 
-types config = "instrs \<times> instrs \<times> state"
+type_synonym config = "instrs \<times> instrs \<times> state"
 
 
 inductive_set
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/IMPP/Com.thy
--- a/src/HOL/IMPP/Com.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IMPP/Com.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -8,8 +8,9 @@
 imports Main
 begin
 
-types    val = nat   (* for the meta theory, this may be anything, but with
-                        current Isabelle, types cannot be refined later *)
+type_synonym val = nat
+  (* for the meta theory, this may be anything, but types cannot be refined later *)
+
 typedecl glb
 typedecl loc
 
@@ -18,15 +19,15 @@
   Res :: loc
 
 datatype vname  = Glb glb | Loc loc
-types    globs  = "glb => val"
-         locals = "loc => val"
+type_synonym globs = "glb => val"
+type_synonym locals = "loc => val"
 datatype state  = st globs locals
 (* for the meta theory, the following would be sufficient:
 typedecl state
 consts   st :: "[globs , locals] => state"
 *)
-types    aexp   = "state => val"
-         bexp   = "state => bool"
+type_synonym aexp = "state => val"
+type_synonym bexp = "state => bool"
 
 typedecl pname
 
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/IMPP/Hoare.thy
--- a/src/HOL/IMPP/Hoare.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IMPP/Hoare.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -16,7 +16,7 @@
   vs. simultaneous recursion in call rule
 *}
 
-types 'a assn = "'a => state => bool"
+type_synonym 'a assn = "'a => state => bool"
 translations
   (type) "'a assn" <= (type) "'a => state => bool"
 
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/IOA/Asig.thy
--- a/src/HOL/IOA/Asig.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IOA/Asig.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -9,7 +9,7 @@
 imports Main
 begin
 
-types
+type_synonym
   'a signature = "('a set * 'a set * 'a set)"
 
 consts
diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/IOA/IOA.thy
--- a/src/HOL/IOA/IOA.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/IOA/IOA.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -9,12 +9,11 @@
 imports Asig
 begin
 
-types
-   'a seq            =   "nat => 'a"
-   'a oseq           =   "nat => 'a option"
-   ('a,'b)execution  =   "'a oseq * 'b seq"
-   ('a,'s)transition =   "('s * 'a * 's)"
-   ('a,'s)ioa        =   "'a signature * 's set * ('a,'s)transition set"
+type_synonym 'a seq = "nat => 'a"
+type_synonym 'a oseq = "nat => 'a option"
+type_synonym ('a, 'b) execution = "'a oseq * 'b seq"
+type_synonym ('a, 's) transition = "('s * 'a * 's)"
+type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set"
 
 consts