renewing specifications in HOL: replacing types by type_synonym
authorbulwahn
Wed Mar 30 11:32:52 2011 +0200 (2011-03-30)
changeset 42163392fd6c4669c
parent 42162 00899500c6ca
child 42164 f88c7315d72d
renewing specifications in HOL: replacing types by type_synonym
src/HOL/DSequence.thy
src/HOL/Datatype.thy
src/HOL/Lazy_Sequence.thy
src/HOL/Map.thy
src/HOL/New_DSequence.thy
src/HOL/New_Random_Sequence.thy
src/HOL/Quickcheck.thy
src/HOL/Random.thy
src/HOL/Random_Sequence.thy
src/HOL/Set.thy
src/HOL/String.thy
     1.1 --- a/src/HOL/DSequence.thy	Wed Mar 30 11:32:51 2011 +0200
     1.2 +++ b/src/HOL/DSequence.thy	Wed Mar 30 11:32:52 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  imports Lazy_Sequence Code_Numeral
     1.5  begin
     1.6  
     1.7 -types 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
     1.8 +type_synonym 'a dseq = "code_numeral => bool => 'a Lazy_Sequence.lazy_sequence option"
     1.9  
    1.10  definition empty :: "'a dseq"
    1.11  where
     2.1 --- a/src/HOL/Datatype.thy	Wed Mar 30 11:32:51 2011 +0200
     2.2 +++ b/src/HOL/Datatype.thy	Wed Mar 30 11:32:52 2011 +0200
     2.3 @@ -28,8 +28,8 @@
     2.4  
     2.5  text{*Datatypes will be represented by sets of type @{text node}*}
     2.6  
     2.7 -types 'a item        = "('a, unit) node set"
     2.8 -      ('a, 'b) dtree = "('a, 'b) node set"
     2.9 +type_synonym 'a item        = "('a, unit) node set"
    2.10 +type_synonym ('a, 'b) dtree = "('a, 'b) node set"
    2.11  
    2.12  consts
    2.13    Push      :: "[('b + nat), nat => ('b + nat)] => (nat => ('b + nat))"
     3.1 --- a/src/HOL/Lazy_Sequence.thy	Wed Mar 30 11:32:51 2011 +0200
     3.2 +++ b/src/HOL/Lazy_Sequence.thy	Wed Mar 30 11:32:52 2011 +0200
     3.3 @@ -208,7 +208,7 @@
     3.4  subsection {* With Hit Bound Value *}
     3.5  text {* assuming in negative context *}
     3.6  
     3.7 -types 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
     3.8 +type_synonym 'a hit_bound_lazy_sequence = "'a option lazy_sequence"
     3.9  
    3.10  definition hit_bound :: "'a hit_bound_lazy_sequence"
    3.11  where
     4.1 --- a/src/HOL/Map.thy	Wed Mar 30 11:32:51 2011 +0200
     4.2 +++ b/src/HOL/Map.thy	Wed Mar 30 11:32:52 2011 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4  imports List
     4.5  begin
     4.6  
     4.7 -types ('a,'b) "map" = "'a => 'b option" (infixr "~=>" 0)
     4.8 +type_synonym ('a,'b) "map" = "'a => 'b option" (infixr "~=>" 0)
     4.9  
    4.10  type_notation (xsymbols)
    4.11    "map" (infixr "\<rightharpoonup>" 0)
     5.1 --- a/src/HOL/New_DSequence.thy	Wed Mar 30 11:32:51 2011 +0200
     5.2 +++ b/src/HOL/New_DSequence.thy	Wed Mar 30 11:32:52 2011 +0200
     5.3 @@ -9,7 +9,7 @@
     5.4  
     5.5  subsection {* Positive Depth-Limited Sequence *}
     5.6  
     5.7 -types 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
     5.8 +type_synonym 'a pos_dseq = "code_numeral => 'a Lazy_Sequence.lazy_sequence"
     5.9  
    5.10  definition pos_empty :: "'a pos_dseq"
    5.11  where
    5.12 @@ -49,7 +49,7 @@
    5.13  
    5.14  subsection {* Negative Depth-Limited Sequence *}
    5.15  
    5.16 -types 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
    5.17 +type_synonym 'a neg_dseq = "code_numeral => 'a Lazy_Sequence.hit_bound_lazy_sequence"
    5.18  
    5.19  definition neg_empty :: "'a neg_dseq"
    5.20  where
     6.1 --- a/src/HOL/New_Random_Sequence.thy	Wed Mar 30 11:32:51 2011 +0200
     6.2 +++ b/src/HOL/New_Random_Sequence.thy	Wed Mar 30 11:32:52 2011 +0200
     6.3 @@ -5,8 +5,8 @@
     6.4  imports Quickcheck New_DSequence
     6.5  begin
     6.6  
     6.7 -types 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"
     6.8 -types 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.neg_dseq"
     6.9 +type_synonym 'a pos_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.pos_dseq"
    6.10 +type_synonym 'a neg_random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> 'a New_DSequence.neg_dseq"
    6.11  
    6.12  definition pos_empty :: "'a pos_random_dseq"
    6.13  where
     7.1 --- a/src/HOL/Quickcheck.thy	Wed Mar 30 11:32:51 2011 +0200
     7.2 +++ b/src/HOL/Quickcheck.thy	Wed Mar 30 11:32:52 2011 +0200
     7.3 @@ -164,7 +164,7 @@
     7.4     in Predicate.Seq (%u. Predicate.Insert x (iter (nrandom - 1) sz seed')))"
     7.5  unfolding iter_def iter'.simps[of _ nrandom] ..
     7.6  
     7.7 -types 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
     7.8 +type_synonym 'a randompred = "Random.seed \<Rightarrow> ('a Predicate.pred \<times> Random.seed)"
     7.9  
    7.10  definition empty :: "'a randompred"
    7.11    where "empty = Pair (bot_class.bot)"
     8.1 --- a/src/HOL/Random.thy	Wed Mar 30 11:32:51 2011 +0200
     8.2 +++ b/src/HOL/Random.thy	Wed Mar 30 11:32:52 2011 +0200
     8.3 @@ -25,7 +25,7 @@
     8.4  
     8.5  subsection {* Random seeds *}
     8.6  
     8.7 -types seed = "code_numeral \<times> code_numeral"
     8.8 +type_synonym seed = "code_numeral \<times> code_numeral"
     8.9  
    8.10  primrec "next" :: "seed \<Rightarrow> code_numeral \<times> seed" where
    8.11    "next (v, w) = (let
     9.1 --- a/src/HOL/Random_Sequence.thy	Wed Mar 30 11:32:51 2011 +0200
     9.2 +++ b/src/HOL/Random_Sequence.thy	Wed Mar 30 11:32:52 2011 +0200
     9.3 @@ -5,7 +5,7 @@
     9.4  imports Quickcheck DSequence
     9.5  begin
     9.6  
     9.7 -types 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"
     9.8 +type_synonym 'a random_dseq = "code_numeral \<Rightarrow> code_numeral \<Rightarrow> Random.seed \<Rightarrow> ('a DSequence.dseq \<times> Random.seed)"
     9.9  
    9.10  definition empty :: "'a random_dseq"
    9.11  where
    10.1 --- a/src/HOL/Set.thy	Wed Mar 30 11:32:51 2011 +0200
    10.2 +++ b/src/HOL/Set.thy	Wed Mar 30 11:32:52 2011 +0200
    10.3 @@ -8,7 +8,7 @@
    10.4  
    10.5  subsection {* Sets as predicates *}
    10.6  
    10.7 -types 'a set = "'a \<Rightarrow> bool"
    10.8 +type_synonym 'a set = "'a \<Rightarrow> bool"
    10.9  
   10.10  definition Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" where -- "comprehension"
   10.11    "Collect P = P"
    11.1 --- a/src/HOL/String.thy	Wed Mar 30 11:32:51 2011 +0200
    11.2 +++ b/src/HOL/String.thy	Wed Mar 30 11:32:52 2011 +0200
    11.3 @@ -74,7 +74,7 @@
    11.4  
    11.5  subsection {* Strings *}
    11.6  
    11.7 -types string = "char list"
    11.8 +type_synonym string = "char list"
    11.9  
   11.10  syntax
   11.11    "_String" :: "xstr => string"    ("_")