types -> type_synonym
authorhuffman
Sat Jan 08 09:30:52 2011 -0800 (2011-01-08)
changeset 414760fa9629aa399
parent 41468 0e4f6cf20cdf
child 41477 be6d903e5943
types -> type_synonym
src/HOL/HOLCF/FOCUS/Buffer.thy
src/HOL/HOLCF/FOCUS/Fstream.thy
src/HOL/HOLCF/FOCUS/Fstreams.thy
src/HOL/HOLCF/IMP/HoareEx.thy
src/HOL/HOLCF/IOA/ABP/Env.thy
src/HOL/HOLCF/IOA/ABP/Impl.thy
src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
src/HOL/HOLCF/IOA/ABP/Packet.thy
src/HOL/HOLCF/IOA/ABP/Receiver.thy
src/HOL/HOLCF/IOA/ABP/Sender.thy
src/HOL/HOLCF/IOA/NTP/Impl.thy
src/HOL/HOLCF/IOA/NTP/Packet.thy
src/HOL/HOLCF/IOA/NTP/Receiver.thy
src/HOL/HOLCF/IOA/NTP/Sender.thy
src/HOL/HOLCF/IOA/meta_theory/Asig.thy
src/HOL/HOLCF/IOA/meta_theory/Automata.thy
src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
src/HOL/HOLCF/IOA/meta_theory/Pred.thy
src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
src/HOL/HOLCF/IOA/meta_theory/TL.thy
src/HOL/HOLCF/IOA/meta_theory/TLS.thy
src/HOL/HOLCF/IOA/meta_theory/Traces.thy
src/HOL/HOLCF/ex/Pattern_Match.thy
     1.1 --- a/src/HOL/HOLCF/FOCUS/Buffer.thy	Sat Jan 08 00:28:31 2011 +0100
     1.2 +++ b/src/HOL/HOLCF/FOCUS/Buffer.thy	Sat Jan 08 09:30:52 2011 -0800
     1.3 @@ -33,11 +33,16 @@
     1.4  
     1.5    State = Sd D | Snil ("\<currency>")
     1.6  
     1.7 -types
     1.8 -
     1.9 +type_synonym
    1.10    SPF11         = "M fstream \<rightarrow> D fstream"
    1.11 +
    1.12 +type_synonym
    1.13    SPEC11        = "SPF11 set"
    1.14 +
    1.15 +type_synonym
    1.16    SPSF11        = "State \<Rightarrow> SPF11"
    1.17 +
    1.18 +type_synonym
    1.19    SPECS11       = "SPSF11 set"
    1.20  
    1.21  definition
     2.1 --- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Sat Jan 08 00:28:31 2011 +0100
     2.2 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Sat Jan 08 09:30:52 2011 -0800
     2.3 @@ -14,7 +14,7 @@
     2.4  
     2.5  default_sort type
     2.6  
     2.7 -types 'a fstream = "'a lift stream"
     2.8 +type_synonym 'a fstream = "'a lift stream"
     2.9  
    2.10  definition
    2.11    fscons        :: "'a     \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
     3.1 --- a/src/HOL/HOLCF/FOCUS/Fstreams.thy	Sat Jan 08 00:28:31 2011 +0100
     3.2 +++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy	Sat Jan 08 09:30:52 2011 -0800
     3.3 @@ -12,7 +12,7 @@
     3.4  
     3.5  default_sort type
     3.6  
     3.7 -types 'a fstream = "('a lift) stream"
     3.8 +type_synonym 'a fstream = "('a lift) stream"
     3.9  
    3.10  definition
    3.11    fsingleton    :: "'a => 'a fstream"  ("<_>" [1000] 999) where
     4.1 --- a/src/HOL/HOLCF/IMP/HoareEx.thy	Sat Jan 08 00:28:31 2011 +0100
     4.2 +++ b/src/HOL/HOLCF/IMP/HoareEx.thy	Sat Jan 08 09:30:52 2011 -0800
     4.3 @@ -13,7 +13,7 @@
     4.4    the correctness of the Hoare rule for while-loops.
     4.5  *}
     4.6  
     4.7 -types assn = "state => bool"
     4.8 +type_synonym assn = "state => bool"
     4.9  
    4.10  definition
    4.11    hoare_valid :: "[assn, com, assn] => bool"  ("|= {(1_)}/ (_)/ {(1_)}" 50) where
     5.1 --- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Sat Jan 08 00:28:31 2011 +0100
     5.2 +++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Sat Jan 08 09:30:52 2011 -0800
     5.3 @@ -8,7 +8,7 @@
     5.4  imports IOA Action
     5.5  begin
     5.6  
     5.7 -types
     5.8 +type_synonym
     5.9    'm env_state = bool   -- {* give next bit to system *}
    5.10  
    5.11  definition
     6.1 --- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Sat Jan 08 00:28:31 2011 +0100
     6.2 +++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Sat Jan 08 09:30:52 2011 -0800
     6.3 @@ -8,7 +8,7 @@
     6.4  imports Sender Receiver Abschannel
     6.5  begin
     6.6  
     6.7 -types
     6.8 +type_synonym
     6.9    'm impl_state = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
    6.10    (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
    6.11  
     7.1 --- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Sat Jan 08 00:28:31 2011 +0100
     7.2 +++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Sat Jan 08 09:30:52 2011 -0800
     7.3 @@ -8,7 +8,7 @@
     7.4  imports Sender Receiver Abschannel_finite
     7.5  begin
     7.6  
     7.7 -types
     7.8 +type_synonym
     7.9    'm impl_fin_state
    7.10      = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
    7.11  (*  sender_state   *  receiver_state   *    srch_state  * rsch_state *)
     8.1 --- a/src/HOL/HOLCF/IOA/ABP/Packet.thy	Sat Jan 08 00:28:31 2011 +0100
     8.2 +++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy	Sat Jan 08 09:30:52 2011 -0800
     8.3 @@ -8,7 +8,7 @@
     8.4  imports Main
     8.5  begin
     8.6  
     8.7 -types
     8.8 +type_synonym
     8.9    'msg packet = "bool * 'msg"
    8.10  
    8.11  definition
     9.1 --- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Sat Jan 08 00:28:31 2011 +0100
     9.2 +++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Sat Jan 08 09:30:52 2011 -0800
     9.3 @@ -8,7 +8,7 @@
     9.4  imports IOA Action Lemmas
     9.5  begin
     9.6  
     9.7 -types
     9.8 +type_synonym
     9.9    'm receiver_state = "'m list * bool"  -- {* messages, mode *}
    9.10  
    9.11  definition
    10.1 --- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Sat Jan 08 00:28:31 2011 +0100
    10.2 +++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Sat Jan 08 09:30:52 2011 -0800
    10.3 @@ -8,7 +8,7 @@
    10.4  imports IOA Action Lemmas
    10.5  begin
    10.6  
    10.7 -types
    10.8 +type_synonym
    10.9    'm sender_state = "'m list  *  bool"  -- {* messages, Alternating Bit *}
   10.10  
   10.11  definition
    11.1 --- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sat Jan 08 00:28:31 2011 +0100
    11.2 +++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Sat Jan 08 09:30:52 2011 -0800
    11.3 @@ -8,7 +8,7 @@
    11.4  imports Sender Receiver Abschannel
    11.5  begin
    11.6  
    11.7 -types 'm impl_state
    11.8 +type_synonym 'm impl_state
    11.9    = "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
   11.10    (*  sender_state   *  receiver_state   *    srch_state      * rsch_state *)
   11.11  
    12.1 --- a/src/HOL/HOLCF/IOA/NTP/Packet.thy	Sat Jan 08 00:28:31 2011 +0100
    12.2 +++ b/src/HOL/HOLCF/IOA/NTP/Packet.thy	Sat Jan 08 09:30:52 2011 -0800
    12.3 @@ -6,7 +6,7 @@
    12.4  imports Multiset
    12.5  begin
    12.6  
    12.7 -types
    12.8 +type_synonym
    12.9    'msg packet = "bool * 'msg"
   12.10  
   12.11  definition
    13.1 --- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Sat Jan 08 00:28:31 2011 +0100
    13.2 +++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Sat Jan 08 09:30:52 2011 -0800
    13.3 @@ -8,7 +8,7 @@
    13.4  imports IOA Action
    13.5  begin
    13.6  
    13.7 -types
    13.8 +type_synonym
    13.9  
   13.10  'm receiver_state
   13.11  = "'m list * bool multiset * 'm packet multiset * bool * bool"
    14.1 --- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Sat Jan 08 00:28:31 2011 +0100
    14.2 +++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Sat Jan 08 09:30:52 2011 -0800
    14.3 @@ -8,7 +8,7 @@
    14.4  imports IOA Action
    14.5  begin
    14.6  
    14.7 -types
    14.8 +type_synonym
    14.9  'm sender_state = "'m list * bool multiset * bool multiset * bool * bool"
   14.10  (*                messages   #sent           #received      header  mode *)
   14.11  
    15.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Sat Jan 08 00:28:31 2011 +0100
    15.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Sat Jan 08 09:30:52 2011 -0800
    15.3 @@ -8,7 +8,7 @@
    15.4  imports Main
    15.5  begin
    15.6  
    15.7 -types
    15.8 +type_synonym
    15.9    'a signature = "('a set * 'a set * 'a set)"
   15.10  
   15.11  definition
    16.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sat Jan 08 00:28:31 2011 +0100
    16.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Sat Jan 08 09:30:52 2011 -0800
    16.3 @@ -10,8 +10,10 @@
    16.4  
    16.5  default_sort type
    16.6  
    16.7 -types
    16.8 +type_synonym
    16.9    ('a, 's) transition = "'s * 'a * 's"
   16.10 +
   16.11 +type_synonym
   16.12    ('a, 's) ioa = "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)"
   16.13  
   16.14  consts
    17.1 --- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Jan 08 00:28:31 2011 +0100
    17.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Sat Jan 08 09:30:52 2011 -0800
    17.3 @@ -10,7 +10,7 @@
    17.4  
    17.5  default_sort type
    17.6  
    17.7 -types
    17.8 +type_synonym
    17.9    ('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
   17.10  
   17.11  definition
    18.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Sat Jan 08 00:28:31 2011 +0100
    18.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Sat Jan 08 09:30:52 2011 -0800
    18.3 @@ -10,7 +10,7 @@
    18.4  
    18.5  default_sort type
    18.6  
    18.7 -types
    18.8 +type_synonym
    18.9    'a predicate = "'a => bool"
   18.10  
   18.11  consts
    19.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sat Jan 08 00:28:31 2011 +0100
    19.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Sat Jan 08 09:30:52 2011 -0800
    19.3 @@ -10,7 +10,7 @@
    19.4  
    19.5  default_sort type
    19.6  
    19.7 -types 'a Seq = "'a lift seq"
    19.8 +type_synonym 'a Seq = "'a lift seq"
    19.9  
   19.10  consts
   19.11  
    20.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Sat Jan 08 00:28:31 2011 +0100
    20.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Sat Jan 08 09:30:52 2011 -0800
    20.3 @@ -10,7 +10,7 @@
    20.4  
    20.5  default_sort type
    20.6  
    20.7 -types
    20.8 +type_synonym
    20.9    'a temporal = "'a Seq predicate"
   20.10  
   20.11  
    21.1 --- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Sat Jan 08 00:28:31 2011 +0100
    21.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Sat Jan 08 09:30:52 2011 -0800
    21.3 @@ -10,9 +10,13 @@
    21.4  
    21.5  default_sort type
    21.6  
    21.7 -types
    21.8 +type_synonym
    21.9    ('a, 's) ioa_temp  = "('a option,'s)transition temporal"
   21.10 +
   21.11 +type_synonym
   21.12    ('a, 's) step_pred = "('a option,'s)transition predicate"
   21.13 +
   21.14 +type_synonym
   21.15    's state_pred      = "'s predicate"
   21.16  
   21.17  consts
    22.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Sat Jan 08 00:28:31 2011 +0100
    22.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Sat Jan 08 09:30:52 2011 -0800
    22.3 @@ -10,13 +10,22 @@
    22.4  
    22.5  default_sort type
    22.6  
    22.7 -types
    22.8 +type_synonym
    22.9     ('a,'s)pairs            =    "('a * 's) Seq"
   22.10 +
   22.11 +type_synonym
   22.12     ('a,'s)execution        =    "'s * ('a,'s)pairs"
   22.13 +
   22.14 +type_synonym
   22.15     'a trace                =    "'a Seq"
   22.16  
   22.17 +type_synonym
   22.18     ('a,'s)execution_module = "('a,'s)execution set * 'a signature"
   22.19 +
   22.20 +type_synonym
   22.21     'a schedule_module      = "'a trace set * 'a signature"
   22.22 +
   22.23 +type_synonym
   22.24     'a trace_module         = "'a trace set * 'a signature"
   22.25  
   22.26  consts
    23.1 --- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat Jan 08 00:28:31 2011 +0100
    23.2 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat Jan 08 09:30:52 2011 -0800
    23.3 @@ -172,7 +172,7 @@
    23.4  
    23.5  subsection {* Pattern combinators for data constructors *}
    23.6  
    23.7 -types ('a, 'b) pat = "'a \<rightarrow> 'b match"
    23.8 +type_synonym ('a, 'b) pat = "'a \<rightarrow> 'b match"
    23.9  
   23.10  definition
   23.11    cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where