--- 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
--- 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
--- 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. *}
--- 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"
--- 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
--- 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"
--- 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
--- 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"
--- 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>
--- 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"
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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"
--- 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
--- 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