modernized specifications;
authorwenzelm
Wed Mar 30 23:26:40 2011 +0200 (2011-03-30)
changeset 42174d0be2722ce9f
parent 42173 5d33c12ccf22
child 42177 5cb4a2f4f2a4
modernized specifications;
src/HOL/Hoare/Hoare_Logic.thy
src/HOL/Hoare/Hoare_Logic_Abort.thy
src/HOL/Hoare/SepLogHeap.thy
src/HOL/Hoare_Parallel/Graph.thy
src/HOL/Hoare_Parallel/OG_Com.thy
src/HOL/Hoare_Parallel/OG_Tran.thy
src/HOL/Hoare_Parallel/RG_Com.thy
src/HOL/Hoare_Parallel/RG_Hoare.thy
src/HOL/Hoare_Parallel/RG_Tran.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Expr.thy
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Machines.thy
src/HOL/IMPP/Com.thy
src/HOL/IMPP/Hoare.thy
src/HOL/IOA/Asig.thy
src/HOL/IOA/IOA.thy
     1.1 --- a/src/HOL/Hoare/Hoare_Logic.thy	Wed Mar 30 22:53:18 2011 +0200
     1.2 +++ b/src/HOL/Hoare/Hoare_Logic.thy	Wed Mar 30 23:26:40 2011 +0200
     1.3 @@ -13,9 +13,8 @@
     1.4  uses ("hoare_syntax.ML") ("hoare_tac.ML")
     1.5  begin
     1.6  
     1.7 -types
     1.8 -    'a bexp = "'a set"
     1.9 -    'a assn = "'a set"
    1.10 +type_synonym 'a bexp = "'a set"
    1.11 +type_synonym 'a assn = "'a set"
    1.12  
    1.13  datatype
    1.14   'a com = Basic "'a \<Rightarrow> 'a"
    1.15 @@ -25,7 +24,7 @@
    1.16  
    1.17  abbreviation annskip ("SKIP") where "SKIP == Basic id"
    1.18  
    1.19 -types 'a sem = "'a => 'a => bool"
    1.20 +type_synonym 'a sem = "'a => 'a => bool"
    1.21  
    1.22  inductive Sem :: "'a com \<Rightarrow> 'a sem"
    1.23  where
     2.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Mar 30 22:53:18 2011 +0200
     2.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Mar 30 23:26:40 2011 +0200
     2.3 @@ -10,9 +10,8 @@
     2.4  uses ("hoare_syntax.ML") ("hoare_tac.ML")
     2.5  begin
     2.6  
     2.7 -types
     2.8 -    'a bexp = "'a set"
     2.9 -    'a assn = "'a set"
    2.10 +type_synonym 'a bexp = "'a set"
    2.11 +type_synonym 'a assn = "'a set"
    2.12  
    2.13  datatype
    2.14   'a com = Basic "'a \<Rightarrow> 'a"
    2.15 @@ -23,7 +22,7 @@
    2.16  
    2.17  abbreviation annskip ("SKIP") where "SKIP == Basic id"
    2.18  
    2.19 -types 'a sem = "'a option => 'a option => bool"
    2.20 +type_synonym 'a sem = "'a option => 'a option => bool"
    2.21  
    2.22  inductive Sem :: "'a com \<Rightarrow> 'a sem"
    2.23  where
     3.1 --- a/src/HOL/Hoare/SepLogHeap.thy	Wed Mar 30 22:53:18 2011 +0200
     3.2 +++ b/src/HOL/Hoare/SepLogHeap.thy	Wed Mar 30 23:26:40 2011 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -types heap = "(nat \<Rightarrow> nat option)"
     3.8 +type_synonym heap = "(nat \<Rightarrow> nat option)"
     3.9  
    3.10  text{* @{text "Some"} means allocated, @{text "None"} means
    3.11  free. Address @{text "0"} serves as the null reference. *}
     4.1 --- a/src/HOL/Hoare_Parallel/Graph.thy	Wed Mar 30 22:53:18 2011 +0200
     4.2 +++ b/src/HOL/Hoare_Parallel/Graph.thy	Wed Mar 30 23:26:40 2011 +0200
     4.3 @@ -6,10 +6,9 @@
     4.4  
     4.5  datatype node = Black | White
     4.6  
     4.7 -types 
     4.8 -  nodes = "node list"
     4.9 -  edge  = "nat \<times> nat"
    4.10 -  edges = "edge list"
    4.11 +type_synonym nodes = "node list"
    4.12 +type_synonym edge = "nat \<times> nat"
    4.13 +type_synonym edges = "edge list"
    4.14  
    4.15  consts Roots :: "nat set"
    4.16  
     5.1 --- a/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Mar 30 22:53:18 2011 +0200
     5.2 +++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Wed Mar 30 23:26:40 2011 +0200
     5.3 @@ -7,9 +7,8 @@
     5.4  
     5.5  text {* Type abbreviations for boolean expressions and assertions: *}
     5.6  
     5.7 -types
     5.8 -    'a bexp = "'a set"
     5.9 -    'a assn = "'a set"
    5.10 +type_synonym 'a bexp = "'a set"
    5.11 +type_synonym 'a assn = "'a set"
    5.12  
    5.13  text {* The syntax of commands is defined by two mutually recursive
    5.14  datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
     6.1 --- a/src/HOL/Hoare_Parallel/OG_Tran.thy	Wed Mar 30 22:53:18 2011 +0200
     6.2 +++ b/src/HOL/Hoare_Parallel/OG_Tran.thy	Wed Mar 30 23:26:40 2011 +0200
     6.3 @@ -3,9 +3,8 @@
     6.4  
     6.5  theory OG_Tran imports OG_Com begin
     6.6  
     6.7 -types
     6.8 -  'a ann_com_op = "('a ann_com) option"
     6.9 -  'a ann_triple_op = "('a ann_com_op \<times> 'a assn)"
    6.10 +type_synonym 'a ann_com_op = "('a ann_com) option"
    6.11 +type_synonym 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)"
    6.12    
    6.13  primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
    6.14    "com (c, q) = c"
     7.1 --- a/src/HOL/Hoare_Parallel/RG_Com.thy	Wed Mar 30 22:53:18 2011 +0200
     7.2 +++ b/src/HOL/Hoare_Parallel/RG_Com.thy	Wed Mar 30 23:26:40 2011 +0200
     7.3 @@ -10,8 +10,7 @@
     7.4  of states.  Syntax of commands @{text com} and parallel commands
     7.5  @{text par_com}. *}
     7.6  
     7.7 -types
     7.8 -  'a bexp = "'a set"
     7.9 +type_synonym 'a bexp = "'a set"
    7.10  
    7.11  datatype 'a com = 
    7.12      Basic "'a \<Rightarrow>'a"
    7.13 @@ -20,6 +19,6 @@
    7.14    | While "'a bexp" "'a com"       
    7.15    | Await "'a bexp" "'a com"                 
    7.16  
    7.17 -types 'a par_com = "(('a com) option) list"
    7.18 +type_synonym 'a par_com = "'a com option list"
    7.19  
    7.20  end
    7.21 \ No newline at end of file
     8.1 --- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Mar 30 22:53:18 2011 +0200
     8.2 +++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Wed Mar 30 23:26:40 2011 +0200
     8.3 @@ -55,7 +55,8 @@
     8.4  
     8.5  subsection {* Proof System for Parallel Programs *}
     8.6  
     8.7 -types 'a par_rgformula = "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
     8.8 +type_synonym 'a par_rgformula =
     8.9 +  "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
    8.10  
    8.11  inductive
    8.12    par_rghoare :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool"
     9.1 --- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Mar 30 22:53:18 2011 +0200
     9.2 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Wed Mar 30 23:26:40 2011 +0200
     9.3 @@ -8,7 +8,7 @@
     9.4  
     9.5  subsubsection {* Environment transitions *}
     9.6  
     9.7 -types 'a conf = "(('a com) option) \<times> 'a"
     9.8 +type_synonym 'a conf = "(('a com) option) \<times> 'a"
     9.9  
    9.10  inductive_set
    9.11    etran :: "('a conf \<times> 'a conf) set" 
    9.12 @@ -48,7 +48,7 @@
    9.13  
    9.14  subsection {* Semantics of Parallel Programs *}
    9.15  
    9.16 -types 'a par_conf = "('a par_com) \<times> 'a"
    9.17 +type_synonym 'a par_conf = "('a par_com) \<times> 'a"
    9.18  
    9.19  inductive_set
    9.20    par_etran :: "('a par_conf \<times> 'a par_conf) set"
    9.21 @@ -73,9 +73,9 @@
    9.22  
    9.23  subsubsection {* Sequential computations *}
    9.24  
    9.25 -types 'a confs = "('a conf) list"
    9.26 +type_synonym 'a confs = "'a conf list"
    9.27  
    9.28 -inductive_set cptn :: "('a confs) set"
    9.29 +inductive_set cptn :: "'a confs set"
    9.30  where
    9.31    CptnOne: "[(P,s)] \<in> cptn"
    9.32  | CptnEnv: "(P, t)#xs \<in> cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> cptn"
    9.33 @@ -86,9 +86,9 @@
    9.34  
    9.35  subsubsection {* Parallel computations *}
    9.36  
    9.37 -types  'a par_confs = "('a par_conf) list"
    9.38 +type_synonym 'a par_confs = "'a par_conf list"
    9.39  
    9.40 -inductive_set par_cptn :: "('a par_confs) set"
    9.41 +inductive_set par_cptn :: "'a par_confs set"
    9.42  where
    9.43    ParCptnOne: "[(P,s)] \<in> par_cptn"
    9.44  | ParCptnEnv: "(P,t)#xs \<in> par_cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> par_cptn"
    9.45 @@ -363,7 +363,8 @@
    9.46  
    9.47  subsection {* Validity for Component Programs. *}
    9.48  
    9.49 -types 'a rgformula = "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
    9.50 +type_synonym 'a rgformula =
    9.51 +  "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
    9.52  
    9.53  definition assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a confs) set" where
    9.54    "assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow> 
    10.1 --- a/src/HOL/IMP/Com.thy	Wed Mar 30 22:53:18 2011 +0200
    10.2 +++ b/src/HOL/IMP/Com.thy	Wed Mar 30 23:26:40 2011 +0200
    10.3 @@ -11,11 +11,10 @@
    10.4    -- "an unspecified (arbitrary) type of locations 
    10.5        (adresses/names) for variables"
    10.6        
    10.7 -types 
    10.8 -  val   = nat -- "or anything else, @{text nat} used in examples"
    10.9 -  state = "loc \<Rightarrow> val"
   10.10 -  aexp  = "state \<Rightarrow> val"  
   10.11 -  bexp  = "state \<Rightarrow> bool"
   10.12 +type_synonym val = nat -- "or anything else, @{text nat} used in examples"
   10.13 +type_synonym state = "loc \<Rightarrow> val"
   10.14 +type_synonym aexp = "state \<Rightarrow> val"
   10.15 +type_synonym bexp = "state \<Rightarrow> bool"
   10.16    -- "arithmetic and boolean expressions are not modelled explicitly here,"
   10.17    -- "they are just functions on states"
   10.18  
    11.1 --- a/src/HOL/IMP/Denotation.thy	Wed Mar 30 22:53:18 2011 +0200
    11.2 +++ b/src/HOL/IMP/Denotation.thy	Wed Mar 30 23:26:40 2011 +0200
    11.3 @@ -6,7 +6,7 @@
    11.4  
    11.5  theory Denotation imports Natural begin
    11.6  
    11.7 -types com_den = "(state\<times>state)set"
    11.8 +type_synonym com_den = "(state \<times> state) set"
    11.9  
   11.10  definition
   11.11    Gamma :: "[bexp,com_den] => (com_den => com_den)" where
    12.1 --- a/src/HOL/IMP/Expr.thy	Wed Mar 30 22:53:18 2011 +0200
    12.2 +++ b/src/HOL/IMP/Expr.thy	Wed Mar 30 23:26:40 2011 +0200
    12.3 @@ -14,8 +14,7 @@
    12.4  subsection "Arithmetic expressions"
    12.5  typedecl loc
    12.6  
    12.7 -types
    12.8 -  state = "loc => nat"
    12.9 +type_synonym state = "loc => nat"
   12.10  
   12.11  datatype
   12.12    aexp = N nat
    13.1 --- a/src/HOL/IMP/Hoare.thy	Wed Mar 30 22:53:18 2011 +0200
    13.2 +++ b/src/HOL/IMP/Hoare.thy	Wed Mar 30 23:26:40 2011 +0200
    13.3 @@ -6,7 +6,7 @@
    13.4  
    13.5  theory Hoare imports Natural begin
    13.6  
    13.7 -types assn = "state => bool"
    13.8 +type_synonym assn = "state => bool"
    13.9  
   13.10  inductive
   13.11    hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    14.1 --- a/src/HOL/IMP/Machines.thy	Wed Mar 30 22:53:18 2011 +0200
    14.2 +++ b/src/HOL/IMP/Machines.thy	Wed Mar 30 23:26:40 2011 +0200
    14.3 @@ -14,7 +14,7 @@
    14.4  text {* There are only three instructions: *}
    14.5  datatype instr = SET loc aexp | JMPF bexp nat | JMPB nat
    14.6  
    14.7 -types instrs = "instr list"
    14.8 +type_synonym instrs = "instr list"
    14.9  
   14.10  subsection "M0 with PC"
   14.11  
   14.12 @@ -47,7 +47,7 @@
   14.13    an operational (small step) semantics:
   14.14  *}
   14.15  
   14.16 -types config = "instrs \<times> instrs \<times> state"
   14.17 +type_synonym config = "instrs \<times> instrs \<times> state"
   14.18  
   14.19  
   14.20  inductive_set
    15.1 --- a/src/HOL/IMPP/Com.thy	Wed Mar 30 22:53:18 2011 +0200
    15.2 +++ b/src/HOL/IMPP/Com.thy	Wed Mar 30 23:26:40 2011 +0200
    15.3 @@ -8,8 +8,9 @@
    15.4  imports Main
    15.5  begin
    15.6  
    15.7 -types    val = nat   (* for the meta theory, this may be anything, but with
    15.8 -                        current Isabelle, types cannot be refined later *)
    15.9 +type_synonym val = nat
   15.10 +  (* for the meta theory, this may be anything, but types cannot be refined later *)
   15.11 +
   15.12  typedecl glb
   15.13  typedecl loc
   15.14  
   15.15 @@ -18,15 +19,15 @@
   15.16    Res :: loc
   15.17  
   15.18  datatype vname  = Glb glb | Loc loc
   15.19 -types    globs  = "glb => val"
   15.20 -         locals = "loc => val"
   15.21 +type_synonym globs = "glb => val"
   15.22 +type_synonym locals = "loc => val"
   15.23  datatype state  = st globs locals
   15.24  (* for the meta theory, the following would be sufficient:
   15.25  typedecl state
   15.26  consts   st :: "[globs , locals] => state"
   15.27  *)
   15.28 -types    aexp   = "state => val"
   15.29 -         bexp   = "state => bool"
   15.30 +type_synonym aexp = "state => val"
   15.31 +type_synonym bexp = "state => bool"
   15.32  
   15.33  typedecl pname
   15.34  
    16.1 --- a/src/HOL/IMPP/Hoare.thy	Wed Mar 30 22:53:18 2011 +0200
    16.2 +++ b/src/HOL/IMPP/Hoare.thy	Wed Mar 30 23:26:40 2011 +0200
    16.3 @@ -16,7 +16,7 @@
    16.4    vs. simultaneous recursion in call rule
    16.5  *}
    16.6  
    16.7 -types 'a assn = "'a => state => bool"
    16.8 +type_synonym 'a assn = "'a => state => bool"
    16.9  translations
   16.10    (type) "'a assn" <= (type) "'a => state => bool"
   16.11  
    17.1 --- a/src/HOL/IOA/Asig.thy	Wed Mar 30 22:53:18 2011 +0200
    17.2 +++ b/src/HOL/IOA/Asig.thy	Wed Mar 30 23:26:40 2011 +0200
    17.3 @@ -9,7 +9,7 @@
    17.4  imports Main
    17.5  begin
    17.6  
    17.7 -types
    17.8 +type_synonym
    17.9    'a signature = "('a set * 'a set * 'a set)"
   17.10  
   17.11  consts
    18.1 --- a/src/HOL/IOA/IOA.thy	Wed Mar 30 22:53:18 2011 +0200
    18.2 +++ b/src/HOL/IOA/IOA.thy	Wed Mar 30 23:26:40 2011 +0200
    18.3 @@ -9,12 +9,11 @@
    18.4  imports Asig
    18.5  begin
    18.6  
    18.7 -types
    18.8 -   'a seq            =   "nat => 'a"
    18.9 -   'a oseq           =   "nat => 'a option"
   18.10 -   ('a,'b)execution  =   "'a oseq * 'b seq"
   18.11 -   ('a,'s)transition =   "('s * 'a * 's)"
   18.12 -   ('a,'s)ioa        =   "'a signature * 's set * ('a,'s)transition set"
   18.13 +type_synonym 'a seq = "nat => 'a"
   18.14 +type_synonym 'a oseq = "nat => 'a option"
   18.15 +type_synonym ('a, 'b) execution = "'a oseq * 'b seq"
   18.16 +type_synonym ('a, 's) transition = "('s * 'a * 's)"
   18.17 +type_synonym ('a,'s) ioa = "'a signature * 's set * ('a, 's) transition set"
   18.18  
   18.19  consts
   18.20