--- a/src/HOL/IOA/ABP/Correctness.ML Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/ABP/Correctness.ML Mon Mar 11 23:59:22 1996 +0100
@@ -393,8 +393,9 @@
by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
rsch_fin_ioa_def] @ env_ioas @ impl_ioas)
- addsimps [system_def, system_fin_def, abs_def, impl_def,
- impl_fin_def, sys_IOA, sys_fin_IOA]) 1);
+ addsimps [system_def, system_fin_def, abs_def,
+ impl_ioa_def, impl_fin_ioa_def, sys_IOA,
+ sys_fin_IOA]) 1);
by (REPEAT (EVERY[rtac fxg_is_weak_pmap_of_product_IOA 1,
simp_tac (ss addsimps abstractions) 1,
--- a/src/HOL/IOA/ABP/Impl.thy Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/ABP/Impl.thy Mon Mar 11 23:59:22 1996 +0100
@@ -15,21 +15,21 @@
(* sender_state * receiver_state * srch_state * rsch_state *)
-consts
+constdefs
+
impl_ioa :: ('m action, 'm impl_state)ioa
+ "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
+
sen :: 'm impl_state => 'm sender_state
- rec :: 'm impl_state => 'm receiver_state
- srch :: 'm impl_state => 'm packet list
- rsch :: 'm impl_state => bool list
+ "sen == fst"
-defs
-
- impl_def
- "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
+ rec :: 'm impl_state => 'm receiver_state
+ "rec == fst o snd"
- sen_def "sen == fst"
- rec_def "rec == fst o snd"
- srch_def "srch == fst o snd o snd"
- rsch_def "rsch == snd o snd o snd"
+ srch :: 'm impl_state => 'm packet list
+ "srch == fst o snd o snd"
+
+ rsch :: 'm impl_state => bool list
+ "rsch == snd o snd o snd"
end
--- a/src/HOL/IOA/ABP/Impl_finite.thy Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/ABP/Impl_finite.thy Mon Mar 11 23:59:22 1996 +0100
@@ -14,22 +14,23 @@
= "'m sender_state * 'm receiver_state * 'm packet list * bool list"
(* sender_state * receiver_state * srch_state * rsch_state *)
-consts
+constdefs
impl_fin_ioa :: ('m action, 'm impl_fin_state)ioa
+ "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa ||
+ rsch_fin_ioa)"
+
sen_fin :: 'm impl_fin_state => 'm sender_state
- rec_fin :: 'm impl_fin_state => 'm receiver_state
- srch_fin :: 'm impl_fin_state => 'm packet list
- rsch_fin :: 'm impl_fin_state => bool list
-
-defs
+ "sen_fin == fst"
- impl_fin_def
- "impl_fin_ioa == (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"
- sen_fin_def "sen_fin == fst"
- rec_fin_def "rec_fin == fst o snd"
- srch_fin_def "srch_fin == fst o snd o snd"
- rsch_fin_def "rsch_fin == snd o snd o snd"
+ rec_fin :: 'm impl_fin_state => 'm receiver_state
+ "rec_fin == fst o snd"
+
+ srch_fin :: 'm impl_fin_state => 'm packet list
+ "srch_fin == fst o snd o snd"
+
+ rsch_fin :: 'm impl_fin_state => bool list
+ "rsch_fin == snd o snd o snd"
end
--- a/src/HOL/IOA/ABP/Packet.thy Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/ABP/Packet.thy Mon Mar 11 23:59:22 1996 +0100
@@ -12,14 +12,12 @@
'msg packet = "bool * 'msg"
-consts
+constdefs
hdr :: 'msg packet => bool
- msg :: 'msg packet => 'msg
+ "hdr == fst"
-defs
-
- hdr_def "hdr == fst"
- msg_def "msg == snd"
+ msg :: 'msg packet => 'msg
+ "msg == snd"
end
--- a/src/HOL/IOA/NTP/Correctness.thy Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/NTP/Correctness.thy Mon Mar 11 23:59:22 1996 +0100
@@ -8,14 +8,10 @@
Correctness = Solve + Impl + Spec +
-consts
-
-hom :: 'm impl_state => 'm list
+constdefs
-defs
-
-hom_def
-"hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
- else ttl(sq(sen s)))"
+ hom :: 'm impl_state => 'm list
+ "hom(s) == rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
+ else ttl(sq(sen s)))"
end
--- a/src/HOL/IOA/NTP/Packet.thy Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/NTP/Packet.thy Mon Mar 11 23:59:22 1996 +0100
@@ -12,14 +12,12 @@
'msg packet = "bool * 'msg"
-consts
+constdefs
hdr :: 'msg packet => bool
- msg :: 'msg packet => 'msg
+ "hdr == fst"
-defs
-
- hdr_def "hdr == fst"
- msg_def "msg == snd"
+ msg :: 'msg packet => 'msg
+ "msg == snd"
end
--- a/src/HOL/IOA/meta_theory/Solve.thy Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/IOA/meta_theory/Solve.thy Mon Mar 11 23:59:22 1996 +0100
@@ -8,13 +8,9 @@
Solve = IOA +
-consts
+constdefs
is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
-
-defs
-
-is_weak_pmap_def
"is_weak_pmap f C A ==
(!s:starts_of(C). f(s):starts_of(A)) &
(!s t a. reachable C s &
--- a/src/HOL/ex/Acc.thy Mon Mar 11 19:42:55 1996 +0100
+++ b/src/HOL/ex/Acc.thy Mon Mar 11 23:59:22 1996 +0100
@@ -11,13 +11,13 @@
Acc = WF +
+constdefs
+ pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
+ "pred x r == {y. (y,x):r}"
+
consts
- pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
acc :: "('a * 'a)set => 'a set" (*Accessible part*)
-defs
- pred_def "pred x r == {y. (y,x):r}"
-
inductive "acc(r)"
intrs
pred "pred a r: Pow(acc(r)) ==> a: acc(r)"