--- a/src/HOL/HOLCF/Cfun.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/Cfun.thy Sat Jan 08 11:29:25 2011 -0800
@@ -30,36 +30,26 @@
subsection {* Syntax for continuous lambda abstraction *}
-syntax "_cabs" :: "'a"
+syntax "_cabs" :: "[logic, logic] \<Rightarrow> logic"
parse_translation {*
(* rewrite (_cabs x t) => (Abs_cfun (%x. t)) *)
[mk_binder_tr (@{syntax_const "_cabs"}, @{const_syntax Abs_cfun})];
*}
-text {* To avoid eta-contraction of body: *}
-typed_print_translation {*
- let
- fun cabs_tr' _ _ [Abs abs] = let
- val (x,t) = atomic_abs_tr' abs
- in Syntax.const @{syntax_const "_cabs"} $ x $ t end
-
- | cabs_tr' _ T [t] = let
- val xT = domain_type (domain_type T);
- val abs' = ("x",xT,(incr_boundvars 1 t)$Bound 0);
- val (x,t') = atomic_abs_tr' abs';
- in Syntax.const @{syntax_const "_cabs"} $ x $ t' end;
-
- in [(@{const_syntax Abs_cfun}, cabs_tr')] end;
-*}
+print_translation {*
+ [(@{const_syntax Abs_cfun}, fn [Abs abs] =>
+ let val (x, t) = atomic_abs_tr' abs
+ in Syntax.const @{syntax_const "_cabs"} $ x $ t end)]
+*} -- {* To avoid eta-contraction of body *}
text {* Syntax for nested abstractions *}
syntax
- "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3LAM _./ _)" [1000, 10] 10)
+ "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3LAM _./ _)" [1000, 10] 10)
syntax (xsymbols)
- "_Lambda" :: "[cargs, 'a] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
+ "_Lambda" :: "[cargs, logic] \<Rightarrow> logic" ("(3\<Lambda> _./ _)" [1000, 10] 10)
parse_ast_translation {*
(* rewrite (LAM x y z. t) => (_cabs x (_cabs y (_cabs z t))) *)
--- a/src/HOL/HOLCF/ConvexPD.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy Sat Jan 08 11:29:25 2011 -0800
@@ -181,7 +181,7 @@
"xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys"
syntax
- "_convex_pd" :: "args \<Rightarrow> 'a convex_pd" ("{_}\<natural>")
+ "_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>")
translations
"{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"
--- a/src/HOL/HOLCF/FOCUS/Buffer.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Buffer.thy Sat Jan 08 11:29:25 2011 -0800
@@ -33,11 +33,16 @@
State = Sd D | Snil ("\<currency>")
-types
-
+type_synonym
SPF11 = "M fstream \<rightarrow> D fstream"
+
+type_synonym
SPEC11 = "SPF11 set"
+
+type_synonym
SPSF11 = "State \<Rightarrow> SPF11"
+
+type_synonym
SPECS11 = "SPSF11 set"
definition
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy Sat Jan 08 11:29:25 2011 -0800
@@ -14,7 +14,7 @@
default_sort type
-types 'a fstream = "'a lift stream"
+type_synonym 'a fstream = "'a lift stream"
definition
fscons :: "'a \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
--- a/src/HOL/HOLCF/FOCUS/Fstreams.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstreams.thy Sat Jan 08 11:29:25 2011 -0800
@@ -12,7 +12,7 @@
default_sort type
-types 'a fstream = "('a lift) stream"
+type_synonym 'a fstream = "('a lift) stream"
definition
fsingleton :: "'a => 'a fstream" ("<_>" [1000] 999) where
--- a/src/HOL/HOLCF/IMP/HoareEx.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IMP/HoareEx.thy Sat Jan 08 11:29:25 2011 -0800
@@ -13,7 +13,7 @@
the correctness of the Hoare rule for while-loops.
*}
-types assn = "state => bool"
+type_synonym assn = "state => bool"
definition
hoare_valid :: "[assn, com, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where
--- a/src/HOL/HOLCF/IOA/ABP/Env.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy Sat Jan 08 11:29:25 2011 -0800
@@ -8,7 +8,7 @@
imports IOA Action
begin
-types
+type_synonym
'm env_state = bool -- {* give next bit to system *}
definition
--- a/src/HOL/HOLCF/IOA/ABP/Impl.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy Sat Jan 08 11:29:25 2011 -0800
@@ -8,7 +8,7 @@
imports Sender Receiver Abschannel
begin
-types
+type_synonym
'm impl_state = "'m sender_state * 'm receiver_state * 'm packet list * bool list"
(* sender_state * receiver_state * srch_state * rsch_state *)
--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy Sat Jan 08 11:29:25 2011 -0800
@@ -8,7 +8,7 @@
imports Sender Receiver Abschannel_finite
begin
-types
+type_synonym
'm impl_fin_state
= "'m sender_state * 'm receiver_state * 'm packet list * bool list"
(* sender_state * receiver_state * srch_state * rsch_state *)
--- a/src/HOL/HOLCF/IOA/ABP/Packet.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy Sat Jan 08 11:29:25 2011 -0800
@@ -8,7 +8,7 @@
imports Main
begin
-types
+type_synonym
'msg packet = "bool * 'msg"
definition
--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy Sat Jan 08 11:29:25 2011 -0800
@@ -8,7 +8,7 @@
imports IOA Action Lemmas
begin
-types
+type_synonym
'm receiver_state = "'m list * bool" -- {* messages, mode *}
definition
--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy Sat Jan 08 11:29:25 2011 -0800
@@ -8,7 +8,7 @@
imports IOA Action Lemmas
begin
-types
+type_synonym
'm sender_state = "'m list * bool" -- {* messages, Alternating Bit *}
definition
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy Sat Jan 08 11:29:25 2011 -0800
@@ -8,7 +8,7 @@
imports Sender Receiver Abschannel
begin
-types 'm impl_state
+type_synonym 'm impl_state
= "'m sender_state * 'm receiver_state * 'm packet multiset * bool multiset"
(* sender_state * receiver_state * srch_state * rsch_state *)
--- a/src/HOL/HOLCF/IOA/NTP/Packet.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Packet.thy Sat Jan 08 11:29:25 2011 -0800
@@ -6,7 +6,7 @@
imports Multiset
begin
-types
+type_synonym
'msg packet = "bool * 'msg"
definition
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy Sat Jan 08 11:29:25 2011 -0800
@@ -8,7 +8,7 @@
imports IOA Action
begin
-types
+type_synonym
'm receiver_state
= "'m list * bool multiset * 'm packet multiset * bool * bool"
--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy Sat Jan 08 11:29:25 2011 -0800
@@ -8,7 +8,7 @@
imports IOA Action
begin
-types
+type_synonym
'm sender_state = "'m list * bool multiset * bool multiset * bool * bool"
(* messages #sent #received header mode *)
--- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy Sat Jan 08 11:29:25 2011 -0800
@@ -8,7 +8,7 @@
imports Main
begin
-types
+type_synonym
'a signature = "('a set * 'a set * 'a set)"
definition
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Sat Jan 08 11:29:25 2011 -0800
@@ -10,8 +10,10 @@
default_sort type
-types
+type_synonym
('a, 's) transition = "'s * 'a * 's"
+
+type_synonym
('a, 's) ioa = "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)"
consts
--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy Sat Jan 08 11:29:25 2011 -0800
@@ -10,7 +10,7 @@
default_sort type
-types
+type_synonym
('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
definition
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Sat Jan 08 11:29:25 2011 -0800
@@ -10,7 +10,7 @@
default_sort type
-types
+type_synonym
'a predicate = "'a => bool"
consts
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Sat Jan 08 11:29:25 2011 -0800
@@ -10,7 +10,7 @@
default_sort type
-types 'a Seq = "'a lift seq"
+type_synonym 'a Seq = "'a lift seq"
consts
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy Sat Jan 08 11:29:25 2011 -0800
@@ -10,7 +10,7 @@
default_sort type
-types
+type_synonym
'a temporal = "'a Seq predicate"
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Sat Jan 08 11:29:25 2011 -0800
@@ -10,9 +10,13 @@
default_sort type
-types
+type_synonym
('a, 's) ioa_temp = "('a option,'s)transition temporal"
+
+type_synonym
('a, 's) step_pred = "('a option,'s)transition predicate"
+
+type_synonym
's state_pred = "'s predicate"
consts
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Sat Jan 08 11:29:25 2011 -0800
@@ -10,13 +10,22 @@
default_sort type
-types
+type_synonym
('a,'s)pairs = "('a * 's) Seq"
+
+type_synonym
('a,'s)execution = "'s * ('a,'s)pairs"
+
+type_synonym
'a trace = "'a Seq"
+type_synonym
('a,'s)execution_module = "('a,'s)execution set * 'a signature"
+
+type_synonym
'a schedule_module = "'a trace set * 'a signature"
+
+type_synonym
'a trace_module = "'a trace set * 'a signature"
consts
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sat Jan 08 11:29:25 2011 -0800
@@ -5,7 +5,7 @@
header {* Algebraic deflations are a bifinite domain *}
theory Defl_Bifinite
-imports HOLCF Infinite_Set
+imports HOLCF "~~/src/HOL/Library/Infinite_Set"
begin
subsection {* Lemmas about MOST *}
--- a/src/HOL/HOLCF/LowerPD.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/LowerPD.thy Sat Jan 08 11:29:25 2011 -0800
@@ -136,7 +136,7 @@
"xs \<union>\<flat> ys == lower_plus\<cdot>xs\<cdot>ys"
syntax
- "_lower_pd" :: "args \<Rightarrow> 'a lower_pd" ("{_}\<flat>")
+ "_lower_pd" :: "args \<Rightarrow> logic" ("{_}\<flat>")
translations
"{x,xs}\<flat>" == "{x}\<flat> \<union>\<flat> {xs}\<flat>"
--- a/src/HOL/HOLCF/Sprod.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/Sprod.thy Sat Jan 08 11:29:25 2011 -0800
@@ -44,7 +44,8 @@
"ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
syntax
- "_stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))")
+ "_stuple" :: "[logic, args] \<Rightarrow> logic" ("(1'(:_,/ _:'))")
+
translations
"(:x, y, z:)" == "(:x, (:y, z:):)"
"(:x, y:)" == "CONST spair\<cdot>x\<cdot>y"
--- a/src/HOL/HOLCF/UpperPD.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy Sat Jan 08 11:29:25 2011 -0800
@@ -134,7 +134,7 @@
"xs \<union>\<sharp> ys == upper_plus\<cdot>xs\<cdot>ys"
syntax
- "_upper_pd" :: "args \<Rightarrow> 'a upper_pd" ("{_}\<sharp>")
+ "_upper_pd" :: "args \<Rightarrow> logic" ("{_}\<sharp>")
translations
"{x,xs}\<sharp>" == "{x}\<sharp> \<union>\<sharp> {xs}\<sharp>"
--- a/src/HOL/HOLCF/ex/Letrec.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/ex/Letrec.thy Sat Jan 08 11:29:25 2011 -0800
@@ -17,12 +17,12 @@
nonterminal recbinds and recbindt and recbind
syntax
- "_recbind" :: "['a, 'a] \<Rightarrow> recbind" ("(2_ =/ _)" 10)
+ "_recbind" :: "[logic, logic] \<Rightarrow> recbind" ("(2_ =/ _)" 10)
"" :: "recbind \<Rightarrow> recbindt" ("_")
"_recbindt" :: "[recbind, recbindt] \<Rightarrow> recbindt" ("_,/ _")
"" :: "recbindt \<Rightarrow> recbinds" ("_")
"_recbinds" :: "[recbindt, recbinds] \<Rightarrow> recbinds" ("_;/ _")
- "_Letrec" :: "[recbinds, 'a] \<Rightarrow> 'a" ("(Letrec (_)/ in (_))" 10)
+ "_Letrec" :: "[recbinds, logic] \<Rightarrow> logic" ("(Letrec (_)/ in (_))" 10)
translations
(recbindt) "x = a, (y,ys) = (b,bs)" == (recbindt) "(x,y,ys) = (a,b,bs)"
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sat Jan 08 18:01:10 2011 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sat Jan 08 11:29:25 2011 -0800
@@ -172,7 +172,7 @@
subsection {* Pattern combinators for data constructors *}
-types ('a, 'b) pat = "'a \<rightarrow> 'b match"
+type_synonym ('a, 'b) pat = "'a \<rightarrow> 'b match"
definition
cpair_pat :: "('a, 'c) pat \<Rightarrow> ('b, 'd) pat \<Rightarrow> ('a \<times> 'b, 'c \<times> 'd) pat" where