--- a/src/HOL/IMP/Com.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IMP/Com.thy Wed Jun 21 15:47:10 1995 +0200
@@ -34,8 +34,8 @@
N "<N(n),s> -a-> n"
X "<X(x),s> -a-> s(x)"
Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
- Op2 "[| <e0,s> -a-> n0; <e1,s> -a-> n1 |] \
-\ ==> <Op2 f e0 e1,s> -a-> f n0 n1"
+ Op2 "[| <e0,s> -a-> n0; <e1,s> -a-> n1 |]
+ ==> <Op2 f e0 e1,s> -a-> f n0 n1"
types n2n2b = "[nat,nat] => bool"
@@ -60,13 +60,13 @@
intrs (*avoid clash with ML constructors true, false*)
tru "<true,s> -b-> True"
fls "<false,s> -b-> False"
- ROp "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] \
-\ ==> <ROp f a0 a1,s> -b-> f n0 n1"
+ ROp "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |]
+ ==> <ROp f a0 a1,s> -b-> f n0 n1"
noti "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
- andi "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
-\ ==> <b0 andi b1,s> -b-> (w0 & w1)"
- ori "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \
-\ ==> <b0 ori b1,s> -b-> (w0 | w1)"
+ andi "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |]
+ ==> <b0 andi b1,s> -b-> (w0 & w1)"
+ ori "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |]
+ ==> <b0 ori b1,s> -b-> (w0 | w1)"
(** Commands **)
@@ -94,19 +94,19 @@
assign "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
- semi "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] \
-\ ==> <c0 ; c1, s> -c-> s1"
+ semi "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |]
+ ==> <c0 ; c1, s> -c-> s1"
- ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] \
-\ ==> <ifc b then c0 else c1, s> -c-> s1"
+ ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |]
+ ==> <ifc b then c0 else c1, s> -c-> s1"
- ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] \
-\ ==> <ifc b then c0 else c1, s> -c-> s1"
+ ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |]
+ ==> <ifc b then c0 else c1, s> -c-> s1"
whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s"
- whileTrue "[| <b,s> -b-> True; <c,s> -c-> s2; \
-\ <while b do c, s2> -c-> s1 |] \
-\ ==> <while b do c, s> -c-> s1 "
+ whileTrue "[| <b,s> -b-> True; <c,s> -c-> s2;
+ <while b do c, s2> -c-> s1 |]
+ ==> <while b do c, s> -c-> s1 "
end
--- a/src/HOL/IMP/Denotation.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IMP/Denotation.thy Wed Jun 21 15:47:10 1995 +0200
@@ -30,17 +30,17 @@
B_or "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
defs
- Gamma_def "Gamma b cd == \
-\ (%phi.{st. st : (phi O cd) & B b (fst st)} Un \
-\ {st. st : id & ~B b (fst st)})"
+ Gamma_def "Gamma b cd ==
+ (%phi.{st. st : (phi O cd) & B b (fst st)} Un
+ {st. st : id & ~B b (fst st)})"
primrec C com
C_skip "C(skip) = id"
C_assign "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
C_comp "C(c0 ; c1) = C(c1) O C(c0)"
- C_if "C(ifc b then c0 else c1) = \
-\ {st. st:C(c0) & (B b (fst st))} Un \
-\ {st. st:C(c1) & ~(B b (fst st))}"
+ C_if "C(ifc b then c0 else c1) =
+ {st. st:C(c0) & (B b (fst st))} Un
+ {st. st:C(c1) & ~(B b (fst st))}"
C_while "C(while b do c) = lfp (Gamma b (C c))"
end
--- a/src/HOL/IOA/ABP/Abschannel.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Abschannel.thy Wed Jun 21 15:47:10 1995 +0200
@@ -49,15 +49,15 @@
ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
-ch_trans_def "ch_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in \
-\ case fst(snd(tr)) \
-\ of S(b) => ((t = s) | (t = s @ [b])) | \
-\ R(b) => s ~= [] & \
-\ b = hd(s) & \
-\ ((t = s) | (t = tl(s))) }"
+ch_trans_def "ch_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of S(b) => ((t = s) | (t = s @ [b])) |
+ R(b) => s ~= [] &
+ b = hd(s) &
+ ((t = s) | (t = tl(s))) }"
ch_ioa_def "ch_ioa == (ch_asig, {[]}, ch_trans)"
@@ -65,25 +65,25 @@
C o n c r e t e C h a n n e l s b y R e n a m i n g
*********************************************************)
-rsch_actions_def "rsch_actions (akt) == \
-\ case akt of \
-\ Next => None | \
-\ S_msg(m) => None | \
-\ R_msg(m) => None | \
-\ S_pkt(packet) => None | \
-\ R_pkt(packet) => None | \
-\ S_ack(b) => Some(S(b)) | \
-\ R_ack(b) => Some(R(b))"
+rsch_actions_def "rsch_actions (akt) ==
+ case akt of
+ Next => None |
+ S_msg(m) => None |
+ R_msg(m) => None |
+ S_pkt(packet) => None |
+ R_pkt(packet) => None |
+ S_ack(b) => Some(S(b)) |
+ R_ack(b) => Some(R(b))"
-srch_actions_def "srch_actions (akt) == \
-\ case akt of \
-\ Next => None | \
-\ S_msg(m) => None | \
-\ R_msg(m) => None | \
-\ S_pkt(p) => Some(S(p)) | \
-\ R_pkt(p) => Some(R(p)) | \
-\ S_ack(b) => None | \
-\ R_ack(b) => None"
+srch_actions_def "srch_actions (akt) ==
+ case akt of
+ Next => None |
+ S_msg(m) => None |
+ R_msg(m) => None |
+ S_pkt(p) => Some(S(p)) |
+ R_pkt(p) => Some(R(p)) |
+ S_ack(b) => None |
+ R_ack(b) => None"
end
--- a/src/HOL/IOA/ABP/Abschannel_finite.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Abschannel_finite.thy Wed Jun 21 15:47:10 1995 +0200
@@ -46,16 +46,16 @@
ch_fin_asig_def "ch_fin_asig == ch_asig"
-ch_fin_trans_def "ch_fin_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in \
-\ case fst(snd(tr)) \
-\ of S(b) => ((t = s) | \
-\ (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) | \
-\ R(b) => s ~= [] & \
-\ b = hd(s) & \
-\ ((t = s) | (t = tl(s))) }"
+ch_fin_trans_def "ch_fin_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of S(b) => ((t = s) |
+ (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) |
+ R(b) => s ~= [] &
+ b = hd(s) &
+ ((t = s) | (t = tl(s))) }"
ch_fin_ioa_def "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans)"
--- a/src/HOL/IOA/ABP/Correctness.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Correctness.thy Wed Jun 21 15:47:10 1995 +0200
@@ -19,12 +19,12 @@
primrec
reduce List.list
reduce_Nil "reduce [] = []"
- reduce_Cons "reduce(x#xs) = \
-\ (case xs of \
-\ [] => [x] \
-\ | y#ys => (if (x=y) \
-\ then reduce xs \
-\ else (x#(reduce xs))))"
+ reduce_Cons "reduce(x#xs) =
+ (case xs of
+ [] => [x]
+ | y#ys => (if (x=y)
+ then reduce xs
+ else (x#(reduce xs))))"
defs
@@ -35,9 +35,9 @@
system_fin_def
"system_fin_ioa == (env_ioa || impl_fin_ioa)"
-abs_def "abs == \
-\ (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), \
-\ (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
+abs_def "abs ==
+ (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))),
+ (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p))))))))))"
rules
@@ -47,4 +47,3 @@
end
-
\ No newline at end of file
--- a/src/HOL/IOA/ABP/Env.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Env.thy Wed Jun 21 15:47:10 1995 +0200
@@ -24,25 +24,25 @@
defs
env_asig_def
- "env_asig == ({Next}, \
-\ UN m. {S_msg(m)}, \
-\ {})"
+ "env_asig == ({Next},
+ UN m. {S_msg(m)},
+ {})"
-env_trans_def "env_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in case fst(snd(tr)) \
-\ of \
-\ Next => t=True | \
-\ S_msg(m) => s=True & t=False | \
-\ R_msg(m) => False | \
-\ S_pkt(pkt) => False | \
-\ R_pkt(pkt) => False | \
-\ S_ack(b) => False | \
-\ R_ack(b) => False}"
+env_trans_def "env_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ Next => t=True |
+ S_msg(m) => s=True & t=False |
+ R_msg(m) => False |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => False}"
-env_ioa_def "env_ioa == \
-\ (env_asig, {True}, env_trans)"
+env_ioa_def "env_ioa ==
+ (env_asig, {True}, env_trans)"
end
--- a/src/HOL/IOA/ABP/Receiver.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Receiver.thy Wed Jun 21 15:47:10 1995 +0200
@@ -27,33 +27,33 @@
rq_def "rq == fst"
rbit_def "rbit == snd"
-receiver_asig_def "receiver_asig == \
-\ (UN pkt. {R_pkt(pkt)}, \
-\ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), \
-\ {})"
+receiver_asig_def "receiver_asig ==
+ (UN pkt. {R_pkt(pkt)},
+ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
+ {})"
-receiver_trans_def "receiver_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in \
-\ case fst(snd(tr)) \
-\ of \
-\ Next => False | \
-\ S_msg(m) => False | \
-\ R_msg(m) => (rq(s) ~= []) & \
-\ m = hd(rq(s)) & \
-\ rq(t) = tl(rq(s)) & \
-\ rbit(t)=rbit(s) | \
-\ S_pkt(pkt) => False | \
-\ R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then \
-\ rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else \
-\ rq(t) =rq(s) & rbit(t)=rbit(s) | \
-\ S_ack(b) => b = rbit(s) & \
-\ rq(t) = rq(s) & \
-\ rbit(t)=rbit(s) | \
-\ R_ack(b) => False}"
+receiver_trans_def "receiver_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ Next => False |
+ S_msg(m) => False |
+ R_msg(m) => (rq(s) ~= []) &
+ m = hd(rq(s)) &
+ rq(t) = tl(rq(s)) &
+ rbit(t)=rbit(s) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => if (hdr(pkt) ~= rbit(s))&rq(s)=[] then
+ rq(t) = (rq(s)@[msg(pkt)]) &rbit(t) = (~rbit(s)) else
+ rq(t) =rq(s) & rbit(t)=rbit(s) |
+ S_ack(b) => b = rbit(s) &
+ rq(t) = rq(s) &
+ rbit(t)=rbit(s) |
+ R_ack(b) => False}"
-receiver_ioa_def "receiver_ioa == \
-\ (receiver_asig, {([],False)}, receiver_trans)"
+receiver_ioa_def "receiver_ioa ==
+ (receiver_asig, {([],False)}, receiver_trans)"
end
--- a/src/HOL/IOA/ABP/Sender.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Sender.thy Wed Jun 21 15:47:10 1995 +0200
@@ -27,31 +27,31 @@
sbit_def "sbit == snd"
sender_asig_def
- "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), \
-\ UN pkt. {S_pkt(pkt)}, \
-\ {})"
+ "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
+ UN pkt. {S_pkt(pkt)},
+ {})"
-sender_trans_def "sender_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in case fst(snd(tr)) \
-\ of \
-\ Next => if sq(s)=[] then t=s else False | \
-\ S_msg(m) => sq(t)=sq(s)@[m] & \
-\ sbit(t)=sbit(s) | \
-\ R_msg(m) => False | \
-\ S_pkt(pkt) => sq(s) ~= [] & \
-\ hdr(pkt) = sbit(s) & \
-\ msg(pkt) = hd(sq(s)) & \
-\ sq(t) = sq(s) & \
-\ sbit(t) = sbit(s) | \
-\ R_pkt(pkt) => False | \
-\ S_ack(b) => False | \
-\ R_ack(b) => if b = sbit(s) then \
-\ sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else \
-\ sq(t)=sq(s) & sbit(t)=sbit(s)}"
+sender_trans_def "sender_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ Next => if sq(s)=[] then t=s else False |
+ S_msg(m) => sq(t)=sq(s)@[m] &
+ sbit(t)=sbit(s) |
+ R_msg(m) => False |
+ S_pkt(pkt) => sq(s) ~= [] &
+ hdr(pkt) = sbit(s) &
+ msg(pkt) = hd(sq(s)) &
+ sq(t) = sq(s) &
+ sbit(t) = sbit(s) |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => if b = sbit(s) then
+ sq(t)=tl(sq(s)) & sbit(t)=(~sbit(s)) else
+ sq(t)=sq(s) & sbit(t)=sbit(s)}"
-sender_ioa_def "sender_ioa == \
-\ (sender_asig, {([],True)}, sender_trans)"
+sender_ioa_def "sender_ioa ==
+ (sender_asig, {([],True)}, sender_trans)"
end
--- a/src/HOL/IOA/ABP/Spec.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/ABP/Spec.thy Wed Jun 21 15:47:10 1995 +0200
@@ -16,23 +16,23 @@
defs
-sig_def "spec_sig == (UN m.{S_msg(m)}, \
-\ UN m.{R_msg(m)} Un {Next}, \
-\ {})"
+sig_def "spec_sig == (UN m.{S_msg(m)},
+ UN m.{R_msg(m)} Un {Next},
+ {})"
-trans_def "spec_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in \
-\ case fst(snd(tr)) \
-\ of \
-\ Next => t=s |\ (* Note that there is condition as in Sender *)
-\ S_msg(m) => t = s@[m] | \
-\ R_msg(m) => s = (m#t) | \
-\ S_pkt(pkt) => False | \
-\ R_pkt(pkt) => False | \
-\ S_ack(b) => False | \
-\ R_ack(b) => False}"
+trans_def "spec_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ Next => t=s |\ (* Note that there is condition as in Sender *)
+ S_msg(m) => t = s@[m] |
+ R_msg(m) => s = (m#t) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => False}"
ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
--- a/src/HOL/IOA/NTP/Abschannel.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Abschannel.thy Wed Jun 21 15:47:10 1995 +0200
@@ -45,42 +45,42 @@
ch_asig_def "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
-ch_trans_def "ch_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in \
-\ case fst(snd(tr)) \
-\ of S(b) => t = addm s b | \
-\ R(b) => count s b ~= 0 & t = delm s b}"
+ch_trans_def "ch_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of S(b) => t = addm s b |
+ R(b) => count s b ~= 0 & t = delm s b}"
ch_ioa_def "ch_ioa == (ch_asig, {{|}}, ch_trans)"
-rsch_actions_def "rsch_actions (act) == \
-\ case act of \
-\ S_msg(m) => None | \
-\ R_msg(m) => None | \
-\ S_pkt(packet) => None | \
-\ R_pkt(packet) => None | \
-\ S_ack(b) => Some(S(b)) | \
-\ R_ack(b) => Some(R(b)) | \
-\ C_m_s => None | \
-\ C_m_r => None | \
-\ C_r_s => None | \
-\ C_r_r(m) => None"
+rsch_actions_def "rsch_actions (act) ==
+ case act of
+ S_msg(m) => None |
+ R_msg(m) => None |
+ S_pkt(packet) => None |
+ R_pkt(packet) => None |
+ S_ack(b) => Some(S(b)) |
+ R_ack(b) => Some(R(b)) |
+ C_m_s => None |
+ C_m_r => None |
+ C_r_s => None |
+ C_r_r(m) => None"
-srch_actions_def "srch_actions (act) == \
-\ case act of \
-\ S_msg(m) => None | \
-\ R_msg(m) => None | \
-\ S_pkt(p) => Some(S(p)) | \
-\ R_pkt(p) => Some(R(p)) | \
-\ S_ack(b) => None | \
-\ R_ack(b) => None | \
-\ C_m_s => None | \
-\ C_m_r => None | \
-\ C_r_s => None | \
-\ C_r_r(m) => None"
+srch_actions_def "srch_actions (act) ==
+ case act of
+ S_msg(m) => None |
+ R_msg(m) => None |
+ S_pkt(p) => Some(S(p)) |
+ R_pkt(p) => Some(R(p)) |
+ S_ack(b) => None |
+ R_ack(b) => None |
+ C_m_s => None |
+ C_m_r => None |
+ C_r_s => None |
+ C_r_r(m) => None"
end
--- a/src/HOL/IOA/NTP/Correctness.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Correctness.thy Wed Jun 21 15:47:10 1995 +0200
@@ -15,7 +15,7 @@
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(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/Impl.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Impl.thy Wed Jun 21 15:47:10 1995 +0200
@@ -40,30 +40,30 @@
(* Lemma 5.1 *)
inv1_def
- "inv1(s) == \
- \ (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b) \
- \ & (!b. count (ssent(sen s)) b \
- \ = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
+ "inv1(s) ==
+ (!b. count (rsent(rec s)) b = count (srcvd(sen s)) b + count (rsch s) b)
+ & (!b. count (ssent(sen s)) b
+ = hdr_sum (rrcvd(rec s)) b + hdr_sum (srch s) b)"
(* Lemma 5.2 *)
- inv2_def "inv2(s) == \
-\ (rbit(rec(s)) = sbit(sen(s)) & \
-\ ssending(sen(s)) & \
-\ count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &\
-\ count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s))) \
-\ | \
-\ (rbit(rec(s)) = (~sbit(sen(s))) & \
-\ rsending(rec(s)) & \
-\ count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) &\
-\ count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
+ inv2_def "inv2(s) ==
+ (rbit(rec(s)) = sbit(sen(s)) &
+ ssending(sen(s)) &
+ count (rsent(rec s)) (~sbit(sen s)) <= count (ssent(sen s)) (~sbit(sen s)) &
+ count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)))
+ |
+ (rbit(rec(s)) = (~sbit(sen(s))) &
+ rsending(rec(s)) &
+ count (ssent(sen s)) (~sbit(sen s)) <= count (rsent(rec s)) (sbit(sen s)) &
+ count (rsent(rec s)) (sbit(sen s)) <= count (ssent(sen s)) (sbit(sen s)))"
(* Lemma 5.3 *)
- inv3_def "inv3(s) == \
-\ rbit(rec(s)) = sbit(sen(s)) \
-\ --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s))) \
-\ --> count (rrcvd(rec s)) (sbit(sen(s)),m) \
-\ + count (srch s) (sbit(sen(s)),m) \
-\ <= count (rsent(rec s)) (~sbit(sen s)))"
+ inv3_def "inv3(s) ==
+ rbit(rec(s)) = sbit(sen(s))
+ --> (!m. sq(sen(s))=[] | m ~= hd(sq(sen(s)))
+ --> count (rrcvd(rec s)) (sbit(sen(s)),m)
+ + count (srch s) (sbit(sen(s)),m)
+ <= count (rsent(rec s)) (~sbit(sen s)))"
(* Lemma 5.4 *)
inv4_def "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
--- a/src/HOL/IOA/NTP/Receiver.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Receiver.thy Wed Jun 21 15:47:10 1995 +0200
@@ -33,57 +33,57 @@
rbit_def "rbit == fst o snd o snd o snd"
rsending_def "rsending == snd o snd o snd o snd"
-receiver_asig_def "receiver_asig == \
-\ (UN pkt. {R_pkt(pkt)}, \
-\ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}), \
-\ insert C_m_r (UN m. {C_r_r(m)}))"
+receiver_asig_def "receiver_asig ==
+ (UN pkt. {R_pkt(pkt)},
+ (UN m. {R_msg(m)}) Un (UN b. {S_ack(b)}),
+ insert C_m_r (UN m. {C_r_r(m)}))"
-receiver_trans_def "receiver_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in \
-\ case fst(snd(tr)) \
-\ of \
-\ S_msg(m) => False | \
-\ R_msg(m) => rq(s) = (m # rq(t)) & \
-\ rsent(t)=rsent(s) & \
-\ rrcvd(t)=rrcvd(s) & \
-\ rbit(t)=rbit(s) & \
-\ rsending(t)=rsending(s) | \
-\ S_pkt(pkt) => False | \
-\ R_pkt(pkt) => rq(t) = rq(s) & \
-\ rsent(t) = rsent(s) & \
-\ rrcvd(t) = addm (rrcvd s) pkt & \
-\ rbit(t) = rbit(s) & \
-\ rsending(t) = rsending(s) | \
-\ S_ack(b) => b = rbit(s) & \
-\ rq(t) = rq(s) & \
-\ rsent(t) = addm (rsent s) (rbit s) & \
-\ rrcvd(t) = rrcvd(s) & \
-\ rbit(t)=rbit(s) & \
-\ rsending(s) & \
-\ rsending(t) | \
-\ R_ack(b) => False | \
-\ C_m_s => False | \
-\ C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y.hdr(y)=rbit(s)) & \
-\ rq(t) = rq(s) & \
-\ rsent(t)=rsent(s) & \
-\ rrcvd(t)=rrcvd(s) & \
-\ rbit(t)=rbit(s) & \
-\ rsending(s) & \
-\ ~rsending(t) | \
-\ C_r_s => False | \
-\ C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y.hdr(y)=rbit(s)) & \
-\ count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) & \
-\ rq(t) = rq(s)@[m] & \
-\ rsent(t)=rsent(s) & \
-\ rrcvd(t)=rrcvd(s) & \
-\ rbit(t) = (~rbit(s)) & \
-\ ~rsending(s) & \
-\ rsending(t)}"
+receiver_trans_def "receiver_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ S_msg(m) => False |
+ R_msg(m) => rq(s) = (m # rq(t)) &
+ rsent(t)=rsent(s) &
+ rrcvd(t)=rrcvd(s) &
+ rbit(t)=rbit(s) &
+ rsending(t)=rsending(s) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => rq(t) = rq(s) &
+ rsent(t) = rsent(s) &
+ rrcvd(t) = addm (rrcvd s) pkt &
+ rbit(t) = rbit(s) &
+ rsending(t) = rsending(s) |
+ S_ack(b) => b = rbit(s) &
+ rq(t) = rq(s) &
+ rsent(t) = addm (rsent s) (rbit s) &
+ rrcvd(t) = rrcvd(s) &
+ rbit(t)=rbit(s) &
+ rsending(s) &
+ rsending(t) |
+ R_ack(b) => False |
+ C_m_s => False |
+ C_m_r => count (rsent s) (~rbit s) < countm (rrcvd s) (%y.hdr(y)=rbit(s)) &
+ rq(t) = rq(s) &
+ rsent(t)=rsent(s) &
+ rrcvd(t)=rrcvd(s) &
+ rbit(t)=rbit(s) &
+ rsending(s) &
+ ~rsending(t) |
+ C_r_s => False |
+ C_r_r(m) => count (rsent s) (rbit s) <= countm (rrcvd s) (%y.hdr(y)=rbit(s)) &
+ count (rsent s) (~rbit s) < count (rrcvd s) (rbit(s),m) &
+ rq(t) = rq(s)@[m] &
+ rsent(t)=rsent(s) &
+ rrcvd(t)=rrcvd(s) &
+ rbit(t) = (~rbit(s)) &
+ ~rsending(s) &
+ rsending(t)}"
-receiver_ioa_def "receiver_ioa == \
-\ (receiver_asig, {([],{|},{|},False,False)}, receiver_trans)"
+receiver_ioa_def "receiver_ioa ==
+ (receiver_asig, {([],{|},{|},False,False)}, receiver_trans)"
end
--- a/src/HOL/IOA/NTP/Sender.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Sender.thy Wed Jun 21 15:47:10 1995 +0200
@@ -32,54 +32,54 @@
ssending_def "ssending == snd o snd o snd o snd"
sender_asig_def
- "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}), \
-\ UN pkt. {S_pkt(pkt)}, \
-\ {C_m_s,C_r_s})"
+ "sender_asig == ((UN m. {S_msg(m)}) Un (UN b. {R_ack(b)}),
+ UN pkt. {S_pkt(pkt)},
+ {C_m_s,C_r_s})"
-sender_trans_def "sender_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in case fst(snd(tr)) \
-\ of \
-\ S_msg(m) => sq(t)=sq(s)@[m] & \
-\ ssent(t)=ssent(s) & \
-\ srcvd(t)=srcvd(s) & \
-\ sbit(t)=sbit(s) & \
-\ ssending(t)=ssending(s) | \
-\ R_msg(m) => False | \
-\ S_pkt(pkt) => hdr(pkt) = sbit(s) & \
-\ (? Q. sq(s) = (msg(pkt)#Q)) & \
-\ sq(t) = sq(s) & \
-\ ssent(t) = addm (ssent s) (sbit s) & \
-\ srcvd(t) = srcvd(s) & \
-\ sbit(t) = sbit(s) & \
-\ ssending(s) & \
-\ ssending(t) | \
-\ R_pkt(pkt) => False | \
-\ S_ack(b) => False | \
-\ R_ack(b) => sq(t)=sq(s) & \
-\ ssent(t)=ssent(s) & \
-\ srcvd(t) = addm (srcvd s) b & \
-\ sbit(t)=sbit(s) & \
-\ ssending(t)=ssending(s) | \
-\ C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) & \
-\ sq(t)=sq(s) & \
-\ ssent(t)=ssent(s) & \
-\ srcvd(t)=srcvd(s) & \
-\ sbit(t)=sbit(s) & \
-\ ssending(s) & \
-\ ~ssending(t) | \
-\ C_m_r => False | \
-\ C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) & \
-\ sq(t)=tl(sq(s)) & \
-\ ssent(t)=ssent(s) & \
-\ srcvd(t)=srcvd(s) & \
-\ sbit(t) = (~sbit(s)) & \
-\ ~ssending(s) & \
-\ ssending(t) | \
-\ C_r_r(m) => False}"
+sender_trans_def "sender_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ S_msg(m) => sq(t)=sq(s)@[m] &
+ ssent(t)=ssent(s) &
+ srcvd(t)=srcvd(s) &
+ sbit(t)=sbit(s) &
+ ssending(t)=ssending(s) |
+ R_msg(m) => False |
+ S_pkt(pkt) => hdr(pkt) = sbit(s) &
+ (? Q. sq(s) = (msg(pkt)#Q)) &
+ sq(t) = sq(s) &
+ ssent(t) = addm (ssent s) (sbit s) &
+ srcvd(t) = srcvd(s) &
+ sbit(t) = sbit(s) &
+ ssending(s) &
+ ssending(t) |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => sq(t)=sq(s) &
+ ssent(t)=ssent(s) &
+ srcvd(t) = addm (srcvd s) b &
+ sbit(t)=sbit(s) &
+ ssending(t)=ssending(s) |
+ C_m_s => count (ssent s) (~sbit s) < count (srcvd s) (~sbit s) &
+ sq(t)=sq(s) &
+ ssent(t)=ssent(s) &
+ srcvd(t)=srcvd(s) &
+ sbit(t)=sbit(s) &
+ ssending(s) &
+ ~ssending(t) |
+ C_m_r => False |
+ C_r_s => count (ssent s) (sbit s) <= count (srcvd s) (~sbit s) &
+ sq(t)=tl(sq(s)) &
+ ssent(t)=ssent(s) &
+ srcvd(t)=srcvd(s) &
+ sbit(t) = (~sbit(s)) &
+ ~ssending(s) &
+ ssending(t) |
+ C_r_r(m) => False}"
-sender_ioa_def "sender_ioa == \
-\ (sender_asig, {([],{|},{|},False,True)}, sender_trans)"
+sender_ioa_def "sender_ioa ==
+ (sender_asig, {([],{|},{|},False,True)}, sender_trans)"
end
--- a/src/HOL/IOA/NTP/Spec.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/NTP/Spec.thy Wed Jun 21 15:47:10 1995 +0200
@@ -16,26 +16,26 @@
defs
-sig_def "spec_sig == (UN m.{S_msg(m)}, \
-\ UN m.{R_msg(m)}, \
-\ {})"
+sig_def "spec_sig == (UN m.{S_msg(m)},
+ UN m.{R_msg(m)},
+ {})"
-trans_def "spec_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in \
-\ case fst(snd(tr)) \
-\ of \
-\ S_msg(m) => t = s@[m] | \
-\ R_msg(m) => s = (m#t) | \
-\ S_pkt(pkt) => False | \
-\ R_pkt(pkt) => False | \
-\ S_ack(b) => False | \
-\ R_ack(b) => False | \
-\ C_m_s => False | \
-\ C_m_r => False | \
-\ C_r_s => False | \
-\ C_r_r(m) => False}"
+trans_def "spec_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ S_msg(m) => t = s@[m] |
+ R_msg(m) => s = (m#t) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => False |
+ C_m_s => False |
+ C_m_r => False |
+ C_r_s => False |
+ C_r_r(m) => False}"
ioa_def "spec_ioa == (spec_sig, {[]}, spec_trans)"
--- a/src/HOL/IOA/meta_theory/Asig.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/meta_theory/Asig.thy Wed Jun 21 15:47:10 1995 +0200
@@ -32,10 +32,10 @@
"externals(asig) == (inputs(asig) Un outputs(asig))"
is_asig_def
- "is_asig(triple) == \
- \ ((inputs(triple) Int outputs(triple) = {}) & \
- \ (outputs(triple) Int internals(triple) = {}) & \
- \ (inputs(triple) Int internals(triple) = {}))"
+ "is_asig(triple) ==
+ ((inputs(triple) Int outputs(triple) = {}) &
+ (outputs(triple) Int internals(triple) = {}) &
+ (inputs(triple) Int internals(triple) = {}))"
mk_ext_asig_def
--- a/src/HOL/IOA/meta_theory/IOA.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/meta_theory/IOA.thy Wed Jun 21 15:47:10 1995 +0200
@@ -63,9 +63,9 @@
defs
state_trans_def
- "state_trans asig R == \
- \ (!triple. triple:R --> fst(snd(triple)):actions(asig)) & \
- \ (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
+ "state_trans asig R ==
+ (!triple. triple:R --> fst(snd(triple)):actions(asig)) &
+ (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
asig_of_def "asig_of == fst"
@@ -73,9 +73,9 @@
trans_of_def "trans_of == (snd o snd)"
ioa_def
- "IOA(ioa) == (is_asig(asig_of(ioa)) & \
- \ (~ starts_of(ioa) = {}) & \
- \ state_trans (asig_of ioa) (trans_of ioa))"
+ "IOA(ioa) == (is_asig(asig_of(ioa)) &
+ (~ starts_of(ioa) = {}) &
+ state_trans (asig_of ioa) (trans_of ioa))"
(* An execution fragment is modelled with a pair of sequences:
@@ -83,15 +83,15 @@
* Finite executions have None actions from some point on.
*******)
is_execution_fragment_def
- "is_execution_fragment A ex == \
- \ let act = fst(ex); state = snd(ex) \
- \ in !n a. (act(n)=None --> state(Suc(n)) = state(n)) & \
- \ (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
+ "is_execution_fragment A ex ==
+ let act = fst(ex); state = snd(ex)
+ in !n a. (act(n)=None --> state(Suc(n)) = state(n)) &
+ (act(n)=Some(a) --> (state(n),a,state(Suc(n))):trans_of(A))"
executions_def
- "executions(ioa) == {e. snd e 0:starts_of(ioa) & \
-\ is_execution_fragment ioa e}"
+ "executions(ioa) == {e. snd e 0:starts_of(ioa) &
+ is_execution_fragment ioa e}"
reachable_def
@@ -103,10 +103,10 @@
(* Restrict the trace to those members of the set s *)
filter_oseq_def
- "filter_oseq p s == \
-\ (%i.case s(i) \
-\ of None => None \
-\ | Some(x) => if p x then Some x else None)"
+ "filter_oseq p s ==
+ (%i.case s(i)
+ of None => None
+ | Some(x) => if p x then Some x else None)"
mk_trace_def
@@ -115,13 +115,13 @@
(* Does an ioa have an execution with the given trace *)
has_trace_def
- "has_trace ioa b == \
-\ (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
+ "has_trace ioa b ==
+ (? ex:executions(ioa). b = mk_trace ioa (fst ex))"
normal_form_def
- "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) & \
-\ (!j. j ~: range(f) --> nf(j)= None) & \
-\ (!i. nf(i)=None --> (nf (Suc i)) = None) "
+ "NF(tr) == @nf. ? f. mono(f) & (!i. nf(i)=tr(f(i))) &
+ (!j. j ~: range(f) --> nf(j)= None) &
+ (!i. nf(i)=None --> (nf (Suc i)) = None) "
(* All the traces of an ioa *)
@@ -134,10 +134,10 @@
*)
compat_asigs_def
- "compat_asigs a1 a2 == \
- \ (((outputs(a1) Int outputs(a2)) = {}) & \
- \ ((internals(a1) Int actions(a2)) = {}) & \
- \ ((internals(a2) Int actions(a1)) = {}))"
+ "compat_asigs a1 a2 ==
+ (((outputs(a1) Int outputs(a2)) = {}) &
+ ((internals(a1) Int actions(a2)) = {}) &
+ ((internals(a2) Int actions(a1)) = {}))"
compat_ioas_def
@@ -145,52 +145,52 @@
asig_comp_def
- "asig_comp a1 a2 == \
- \ (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)), \
- \ (outputs(a1) Un outputs(a2)), \
- \ (internals(a1) Un internals(a2))))"
+ "asig_comp a1 a2 ==
+ (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
+ (outputs(a1) Un outputs(a2)),
+ (internals(a1) Un internals(a2))))"
par_def
- "(ioa1 || ioa2) == \
- \ (asig_comp (asig_of ioa1) (asig_of ioa2), \
- \ {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)}, \
- \ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \
- \ in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) & \
- \ (if a:actions(asig_of(ioa1)) then \
- \ (fst(s),a,fst(t)):trans_of(ioa1) \
- \ else fst(t) = fst(s)) \
- \ & \
- \ (if a:actions(asig_of(ioa2)) then \
- \ (snd(s),a,snd(t)):trans_of(ioa2) \
- \ else snd(t) = snd(s))})"
+ "(ioa1 || ioa2) ==
+ (asig_comp (asig_of ioa1) (asig_of ioa2),
+ {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},
+ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
+ in (a:actions(asig_of(ioa1)) | a:actions(asig_of(ioa2))) &
+ (if a:actions(asig_of(ioa1)) then
+ (fst(s),a,fst(t)):trans_of(ioa1)
+ else fst(t) = fst(s))
+ &
+ (if a:actions(asig_of(ioa2)) then
+ (snd(s),a,snd(t)):trans_of(ioa2)
+ else snd(t) = snd(s))})"
restrict_asig_def
- "restrict_asig asig actns == \
-\ (inputs(asig) Int actns, outputs(asig) Int actns, \
-\ internals(asig) Un (externals(asig) - actns))"
+ "restrict_asig asig actns ==
+ (inputs(asig) Int actns, outputs(asig) Int actns,
+ internals(asig) Un (externals(asig) - actns))"
restrict_def
- "restrict ioa actns == \
-\ (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
+ "restrict ioa actns ==
+ (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
ioa_implements_def
- "ioa_implements ioa1 ioa2 == \
-\ ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) & \
-\ (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) & \
-\ traces(ioa1) <= traces(ioa2))"
+ "ioa_implements ioa1 ioa2 ==
+ ((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
+ (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2))) &
+ traces(ioa1) <= traces(ioa2))"
rename_def
-"rename ioa ren == \
-\ (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))}, \
-\ {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))}, \
-\ {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}), \
-\ starts_of(ioa) , \
-\ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \
-\ in \
-\ ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
+"rename ioa ren ==
+ (({b. ? x. Some(x)= ren(b) & x : inputs(asig_of(ioa))},
+ {b. ? x. Some(x)= ren(b) & x : outputs(asig_of(ioa))},
+ {b. ? x. Some(x)= ren(b) & x : internals(asig_of(ioa))}),
+ starts_of(ioa) ,
+ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
+ in
+ ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
end
--- a/src/HOL/IOA/meta_theory/Solve.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/IOA/meta_theory/Solve.thy Wed Jun 21 15:47:10 1995 +0200
@@ -15,12 +15,12 @@
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 & \
-\ (s,a,t):trans_of(C) \
-\ --> (if a:externals(asig_of(C)) then \
-\ (f(s),a,f(t)):trans_of(A) \
-\ else f(s)=f(t)))"
+ "is_weak_pmap f C A ==
+ (!s:starts_of(C). f(s):starts_of(A)) &
+ (!s t a. reachable C s &
+ (s,a,t):trans_of(C)
+ --> (if a:externals(asig_of(C)) then
+ (f(s),a,f(t)):trans_of(A)
+ else f(s)=f(t)))"
end
--- a/src/HOL/Integ/Equiv.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Integ/Equiv.thy Wed Jun 21 15:47:10 1995 +0200
@@ -23,6 +23,6 @@
equiv_def "equiv A r == refl A r & sym(r) & trans(r)"
quotient_def "A/r == UN x:A. {r^^{x}}"
congruent_def "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)"
- congruent2_def "congruent2 r b == ALL y1 z1 y2 z2. \
-\ (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
+ congruent2_def "congruent2 r b == ALL y1 z1 y2 z2.
+ (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2"
end
--- a/src/HOL/Integ/Integ.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Integ/Integ.thy Wed Jun 21 15:47:10 1995 +0200
@@ -46,9 +46,9 @@
"zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{((y-x) + (x-y),0)}) p)"
zadd_def
- "Z1 + Z2 == \
-\ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). \
-\ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
+ "Z1 + Z2 ==
+ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2).
+ split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)"
@@ -57,21 +57,21 @@
zle_def "Z1 <= (Z2::int) == ~(Z2 < Z1)"
zmult_def
- "Z1 * Z2 == \
-\ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \
-\ split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
+ "Z1 * Z2 ==
+ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.
+ split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
zdiv_def
- "Z1 zdiv Z2 == \
-\ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. \
-\ split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2), \
-\ (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
+ "Z1 zdiv Z2 ==
+ Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.
+ split (%x2 y2. intrel^^{((x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),
+ (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2))}) p2) p1)"
zmod_def
- "Z1 zmod Z2 == \
-\ Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1. \
-\ split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)), \
-\ (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
+ "Z1 zmod Z2 ==
+ Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.
+ split (%x2 y2. intrel^^{((x1-y1)mod((x2-y2)+(y2-x2)),
+ (x1-y1)mod((x2-y2)+(x2-y2)))}) p2) p1)"
zsuc_def "zsuc(Z) == Z + $# Suc(0)"
--- a/src/HOL/Lambda/Confluence.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Lambda/Confluence.thy Wed Jun 21 15:47:10 1995 +0200
@@ -26,6 +26,6 @@
"confluent2(R) ==
!x y z. (x,y):R --> (x,z):R^* --> (EX u. (y,u):R^* & (z,u):R)"
- Church_Rosser_def "Church_Rosser(R) == \
-\ !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
+ Church_Rosser_def "Church_Rosser(R) ==
+ !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
end
--- a/src/HOL/Nat.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Nat.thy Wed Jun 21 15:47:10 1995 +0200
@@ -57,14 +57,14 @@
Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
(*nat operations and recursion*)
- nat_case_def "nat_case a f n == @z. (n=0 --> z=a) \
-\ & (!x. n=Suc(x) --> z=f(x))"
+ nat_case_def "nat_case a f n == @z. (n=0 --> z=a)
+ & (!x. n=Suc(x) --> z=f(x))"
pred_nat_def "pred_nat == {p. ? n. p = (n, Suc(n))}"
less_def "m<n == (m,n):trancl(pred_nat)"
le_def "m<=(n::nat) == ~(n<m)"
- nat_rec_def "nat_rec n c d == wfrec pred_nat n \
-\ (nat_case (%g.c) (%m g.(d m (g m))))"
+ nat_rec_def "nat_rec n c d == wfrec pred_nat n
+ (nat_case (%g.c) (%m g.(d m (g m))))"
end
--- a/src/HOL/Sexp.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Sexp.thy Wed Jun 21 15:47:10 1995 +0200
@@ -10,11 +10,11 @@
consts
sexp :: "'a item set"
- sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, \
-\ 'a item] => 'b"
+ sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b,
+ 'a item] => 'b"
- sexp_rec :: "['a item, 'a=>'b, nat=>'b, \
-\ ['a item, 'a item, 'b, 'b]=>'b] => 'b"
+ sexp_rec :: "['a item, 'a=>'b, nat=>'b,
+ ['a item, 'a item, 'b, 'b]=>'b] => 'b"
pred_sexp :: "('a item * 'a item)set"
@@ -27,14 +27,14 @@
defs
sexp_case_def
- "sexp_case c d e M == @ z. (? x. M=Leaf(x) & z=c(x)) \
-\ | (? k. M=Numb(k) & z=d(k)) \
-\ | (? N1 N2. M = N1 $ N2 & z=e N1 N2)"
+ "sexp_case c d e M == @ z. (? x. M=Leaf(x) & z=c(x))
+ | (? k. M=Numb(k) & z=d(k))
+ | (? N1 N2. M = N1 $ N2 & z=e N1 N2)"
pred_sexp_def
"pred_sexp == UN M: sexp. UN N: sexp. {(M, M$N), (N, M$N)}"
sexp_rec_def
- "sexp_rec M c d e == wfrec pred_sexp M \
-\ (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)"
+ "sexp_rec M c d e == wfrec pred_sexp M
+ (%M g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)) M)"
end
--- a/src/HOL/Subst/Subst.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Subst/Subst.thy Wed Jun 21 15:47:10 1995 +0200
@@ -12,8 +12,8 @@
"=s=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52)
"<|" :: "['a uterm,('a*('a uterm)) list] => 'a uterm" (infixl 55)
- "<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] => \
-\ ('a*('a uterm)) list" (infixl 56)
+ "<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] =>
+ ('a*('a uterm)) list" (infixl 56)
sdom :: "('a*('a uterm)) list => 'a set"
srange :: "('a*('a uterm)) list => 'a set"
@@ -22,15 +22,15 @@
subst_eq_def "r =s= s == ALL t.t <| r = t <| s"
subst_def
- "t <| al == uterm_rec t (%x.assoc x (Var x) al) \
-\ (%x.Const(x)) \
-\ (%u v q r.Comb q r)"
+ "t <| al == uterm_rec t (%x.assoc x (Var x) al)
+ (%x.Const(x))
+ (%u v q r.Comb q r)"
comp_def "al <> bl == alist_rec al bl (%x y xs g.(x,y <| bl)#g)"
sdom_def
- "sdom(al) == alist_rec al {} \
-\ (%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})"
+ "sdom(al) == alist_rec al {}
+ (%x y xs g.if Var(x)=y then g Int Compl({x}) else g Un {x})"
srange_def
"srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})"
--- a/src/HOL/Subst/UTerm.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Subst/UTerm.thy Wed Jun 21 15:47:10 1995 +0200
@@ -23,10 +23,10 @@
Var :: "'a => 'a uterm"
Const :: "'a => 'a uterm"
Comb :: "['a uterm, 'a uterm] => 'a uterm"
- UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, \
-\ ['a item , 'a item, 'b, 'b]=>'b] => 'b"
- uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, \
-\ ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
+ UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b,
+ ['a item , 'a item, 'b, 'b]=>'b] => 'b"
+ uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b,
+ ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
defs
(*defining the concrete constructors*)
@@ -54,12 +54,12 @@
(*uterm recursion*)
UTerm_rec_def
- "UTerm_rec M b c d == wfrec (trancl pred_sexp) M \
-\ (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
+ "UTerm_rec M b c d == wfrec (trancl pred_sexp) M
+ (Case (%x g.b(x)) (Case (%y g. c(y)) (Split (%x y g. d x y (g x) (g y)))))"
uterm_rec_def
- "uterm_rec t b c d == \
-\ UTerm_rec (Rep_uterm t) (%x.b(Inv Leaf x)) (%x.c(Inv Leaf x)) \
-\ (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)"
+ "uterm_rec t b c d ==
+ UTerm_rec (Rep_uterm t) (%x.b(Inv Leaf x)) (%x.c(Inv Leaf x))
+ (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)"
end
--- a/src/HOL/Subst/Unifier.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Subst/Unifier.thy Wed Jun 21 15:47:10 1995 +0200
@@ -21,13 +21,13 @@
Idem_def "Idem(s) == s <> s =s= s"
Unifier_def "Unifier s t u == t <| s = u <| s"
MoreGeneral_def "r >> s == ? q.s =s= r <> q"
- MGUnifier_def "MGUnifier s t u == Unifier s t u & \
-\ (! r.Unifier r t u --> s >> r)"
+ MGUnifier_def "MGUnifier s t u == Unifier s t u &
+ (! r.Unifier r t u --> s >> r)"
MGIUnifier_def "MGIUnifier s t u == MGUnifier s t u & Idem(s)"
UWFD_def
- "UWFD x y x' y' == \
-\ (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) | \
-\ (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
+ "UWFD x y x' y' ==
+ (vars_of(x) Un vars_of(y) < vars_of(x') Un vars_of(y')) |
+ (vars_of(x) Un vars_of(y) = vars_of(x') Un vars_of(y') & x <: x')"
end
--- a/src/HOL/Sum.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Sum.thy Wed Jun 21 15:47:10 1995 +0200
@@ -40,8 +40,8 @@
defs
Inl_def "Inl == (%a. Abs_Sum(Inl_Rep(a)))"
Inr_def "Inr == (%b. Abs_Sum(Inr_Rep(b)))"
- sum_case_def "sum_case f g p == @z. (!x. p=Inl(x) --> z=f(x)) \
-\ & (!y. p=Inr(y) --> z=g(y))"
+ sum_case_def "sum_case f g p == @z. (!x. p=Inl(x) --> z=f(x))
+ & (!y. p=Inr(y) --> z=g(y))"
sum_def "A plus B == (Inl``A) Un (Inr``B)"
--- a/src/HOL/Univ.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/Univ.thy Wed Jun 21 15:47:10 1995 +0200
@@ -45,10 +45,10 @@
Case :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"
diag :: "'a set => ('a * 'a)set"
- "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
-\ => ('a item * 'a item)set" (infixr 80)
- "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
-\ => ('a item * 'a item)set" (infixr 70)
+ "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set]
+ => ('a item * 'a item)set" (infixr 80)
+ "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set]
+ => ('a item * 'a item)set" (infixr 70)
defs
@@ -86,8 +86,8 @@
(*the corresponding eliminators*)
Split_def "Split c M == @u. ? x y. M = x$y & u = c x y"
- Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x)) \
-\ | (? y . M = In1(y) & u = d(y))"
+ Case_def "Case c d M == @u. (? x . M = In0(x) & u = c(x))
+ | (? y . M = In1(y) & u = d(y))"
(** diagonal sets and equality for the "universe" **)
@@ -96,7 +96,7 @@
dprod_def "r<**>s == UN (x,x'):r. UN (y,y'):s. {(x$y,x'$y')}"
- dsum_def "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un \
-\ (UN (y,y'):s. {(In1(y),In1(y'))})"
+ dsum_def "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un
+ (UN (y,y'):s. {(In1(y),In1(y'))})"
end
--- a/src/HOL/ex/LList.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/LList.thy Wed Jun 21 15:47:10 1995 +0200
@@ -18,9 +18,9 @@
Previous definition of llistD_Fun was explicit:
llistD_Fun_def
- "llistD_Fun(r) == \
-\ {(LNil,LNil)} Un \
-\ (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
+ "llistD_Fun(r) ==
+ {(LNil,LNil)} Un
+ (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
*)
LList = Gfp + SList +
@@ -34,8 +34,8 @@
consts
list_Fun :: "['a item set, 'a item set] => 'a item set"
LListD_Fun ::
- "[('a item * 'a item)set, ('a item * 'a item)set] => \
-\ ('a item * 'a item)set"
+ "[('a item * 'a item)set, ('a item * 'a item)set] =>
+ ('a item * 'a item)set"
llist :: "'a item set => 'a item set"
LListD :: "('a item * 'a item)set => ('a item * 'a item)set"
@@ -70,45 +70,45 @@
coinductive "LListD(r)"
intrs
NIL_I "(NIL, NIL) : LListD(r)"
- CONS_I "[| (a,b): r; (M,N) : LListD(r) \
-\ |] ==> (CONS a M, CONS b N) : LListD(r)"
+ CONS_I "[| (a,b): r; (M,N) : LListD(r)
+ |] ==> (CONS a M, CONS b N) : LListD(r)"
defs
(*Now used exclusively for abbreviating the coinduction rule*)
- list_Fun_def "list_Fun A X == \
-\ {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
+ list_Fun_def "list_Fun A X ==
+ {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
- LListD_Fun_def "LListD_Fun r X == \
-\ {z. z = (NIL, NIL) | \
-\ (? M N a b. z = (CONS a M, CONS b N) & \
-\ (a, b) : r & (M, N) : X)}"
+ LListD_Fun_def "LListD_Fun r X ==
+ {z. z = (NIL, NIL) |
+ (? M N a b. z = (CONS a M, CONS b N) &
+ (a, b) : r & (M, N) : X)}"
(*defining the abstract constructors*)
LNil_def "LNil == Abs_llist(NIL)"
LCons_def "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
llist_case_def
- "llist_case c d l == \
-\ List_case c (%x y. d (Inv Leaf x) (Abs_llist y)) (Rep_llist l)"
+ "llist_case c d l ==
+ List_case c (%x y. d (Inv Leaf x) (Abs_llist y)) (Rep_llist l)"
LList_corec_fun_def
- "LList_corec_fun k f == \
-\ nat_rec k (%x. {}) \
-\ (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
+ "LList_corec_fun k f ==
+ nat_rec k (%x. {})
+ (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))"
LList_corec_def
"LList_corec a f == UN k. LList_corec_fun k f a"
llist_corec_def
- "llist_corec a f == \
-\ Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) \
-\ (split(%v w. Inr((Leaf(v), w)))) (f z)))"
+ "llist_corec a f ==
+ Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x))
+ (split(%v w. Inr((Leaf(v), w)))) (f z)))"
llistD_Fun_def
- "llistD_Fun(r) == \
-\ prod_fun Abs_llist Abs_llist `` \
-\ LListD_Fun (diag(range Leaf)) \
-\ (prod_fun Rep_llist Rep_llist `` r)"
+ "llistD_Fun(r) ==
+ prod_fun Abs_llist Abs_llist ``
+ LListD_Fun (diag(range Leaf))
+ (prod_fun Rep_llist Rep_llist `` r)"
Lconst_def "Lconst(M) == lfp(%N. CONS M N)"
@@ -127,14 +127,14 @@
*)
Lappend_def
- "Lappend M N == LList_corec (M,N) \
-\ (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) \
-\ (%M1 M2 N. Inr((M1, (M2,N))))))"
+ "Lappend M N == LList_corec (M,N)
+ (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2)))))
+ (%M1 M2 N. Inr((M1, (M2,N))))))"
lappend_def
- "lappend l n == llist_corec (l,n) \
-\ (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) \
-\ (%l1 l2 n. Inr((l1, (l2,n))))))"
+ "lappend l n == llist_corec (l,n)
+ (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2)))))
+ (%l1 l2 n. Inr((l1, (l2,n))))))"
rules
(*faking a type definition...*)
--- a/src/HOL/ex/LexProd.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/LexProd.thy Wed Jun 21 15:47:10 1995 +0200
@@ -9,7 +9,7 @@
LexProd = WF + Prod +
consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70)
rules
-lex_prod_def "ra**rb == {p. ? a a' b b'. \
-\ p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
+lex_prod_def "ra**rb == {p. ? a a' b b'.
+ p = ((a,b),(a',b')) & ((a,a') : ra | a=a' & (b,b') : rb)}"
end
--- a/src/HOL/ex/MT.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/MT.thy Wed Jun 21 15:47:10 1995 +0200
@@ -102,9 +102,9 @@
e_var_inj "e_var(ev1) = e_var(ev2) ==> ev1 = ev2"
e_fn_inj "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2"
e_fix_inj
- " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> \
-\ ev11 = ev21 & ev12 = ev22 & e1 = e2 \
-\ "
+ " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==>
+ ev11 = ev21 & ev12 = ev22 & e1 = e2
+ "
e_app_inj "e11 @ e12 = e21 @ e22 ==> e11 = e21 & e12 = e22"
(* All constructors are distinct *)
@@ -123,14 +123,14 @@
(* Strong elimination, induction on expressions *)
e_ind
- " [| !!ev. P(e_var(ev)); \
-\ !!c. P(e_const(c)); \
-\ !!ev e. P(e) ==> P(fn ev => e); \
-\ !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); \
-\ !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2) \
-\ |] ==> \
-\ P(e) \
-\ "
+ " [| !!ev. P(e_var(ev));
+ !!c. P(e_const(c));
+ !!ev e. P(e) ==> P(fn ev => e);
+ !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e);
+ !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2)
+ |] ==>
+ P(e)
+ "
(* Types - same scheme as for expressions *)
@@ -144,8 +144,8 @@
(* Strong elimination, induction on types *)
t_ind
- "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |] \
-\ ==> P(t)"
+ "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |]
+ ==> P(t)"
(* Values - same scheme again *)
@@ -154,8 +154,8 @@
v_const_inj "v_const(c1) = v_const(c2) ==> c1 = c2"
v_clos_inj
- " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> \
-\ ev1 = ev2 & e1 = e2 & ve1 = ve2"
+ " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==>
+ ev1 = ev2 & e1 = e2 & ve1 = ve2"
(* All constructors are distinct *)
@@ -194,26 +194,26 @@
*)
eval_fun_def
- " eval_fun(s) == \
-\ { pp. \
-\ (? ve c. pp=((ve,e_const(c)),v_const(c))) | \
-\ (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |\
-\ (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))| \
-\ ( ? ve e x f cl. \
-\ pp=((ve,fix f(x) = e),v_clos(cl)) & \
-\ cl=<|x, e, ve+{f |-> v_clos(cl)} |> \
-\ ) | \
-\ ( ? ve e1 e2 c1 c2. \
-\ pp=((ve,e1 @ e2),v_const(c_app c1 c2)) & \
-\ ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s \
-\ ) | \
-\ ( ? ve vem e1 e2 em xm v v2. \
-\ pp=((ve,e1 @ e2),v) & \
-\ ((ve,e1),v_clos(<|xm,em,vem|>)):s & \
-\ ((ve,e2),v2):s & \
-\ ((vem+{xm |-> v2},em),v):s \
-\ ) \
-\ }"
+ " eval_fun(s) ==
+ { pp.
+ (? ve c. pp=((ve,e_const(c)),v_const(c))) |
+ (? ve x. pp=((ve,e_var(x)),ve_app ve x) & x:ve_dom(ve)) |
+ (? ve e x. pp=((ve,fn x => e),v_clos(<|x,e,ve|>)))|
+ ( ? ve e x f cl.
+ pp=((ve,fix f(x) = e),v_clos(cl)) &
+ cl=<|x, e, ve+{f |-> v_clos(cl)} |>
+ ) |
+ ( ? ve e1 e2 c1 c2.
+ pp=((ve,e1 @ e2),v_const(c_app c1 c2)) &
+ ((ve,e1),v_const(c1)):s & ((ve,e2),v_const(c2)):s
+ ) |
+ ( ? ve vem e1 e2 em xm v v2.
+ pp=((ve,e1 @ e2),v) &
+ ((ve,e1),v_clos(<|xm,em,vem|>)):s &
+ ((ve,e2),v2):s &
+ ((vem+{xm |-> v2},em),v):s
+ )
+ }"
eval_rel_def "eval_rel == lfp(eval_fun)"
eval_def "ve |- e ---> v == ((ve,e),v):eval_rel"
@@ -224,18 +224,18 @@
*)
elab_fun_def
- "elab_fun(s) == \
-\ { pp. \
-\ (? te c t. pp=((te,e_const(c)),t) & c isof t) | \
-\ (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) | \
-\ (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) | \
-\ (? te f x e t1 t2. \
-\ pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s \
-\ ) | \
-\ (? te e1 e2 t1 t2. \
-\ pp=((te,e1 @ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s \
-\ ) \
-\ }"
+ "elab_fun(s) ==
+ { pp.
+ (? te c t. pp=((te,e_const(c)),t) & c isof t) |
+ (? te x. pp=((te,e_var(x)),te_app te x) & x:te_dom(te)) |
+ (? te x e t1 t2. pp=((te,fn x => e),t1->t2) & ((te+{x |=> t1},e),t2):s) |
+ (? te f x e t1 t2.
+ pp=((te,fix f(x)=e),t1->t2) & ((te+{f |=> t1->t2}+{x |=> t1},e),t2):s
+ ) |
+ (? te e1 e2 t1 t2.
+ pp=((te,e1 @ e2),t2) & ((te,e1),t1->t2):s & ((te,e2),t1):s
+ )
+ }"
elab_rel_def "elab_rel == lfp(elab_fun)"
elab_def "te |- e ===> t == ((te,e),t):elab_rel"
@@ -243,36 +243,36 @@
(* The original correspondence relation *)
isof_env_def
- " ve isofenv te == \
-\ ve_dom(ve) = te_dom(te) & \
-\ ( ! x. \
-\ x:ve_dom(ve) --> \
-\ (? c.ve_app ve x = v_const(c) & c isof te_app te x) \
-\ ) \
-\ "
+ " ve isofenv te ==
+ ve_dom(ve) = te_dom(te) &
+ ( ! x.
+ x:ve_dom(ve) -->
+ (? c.ve_app ve x = v_const(c) & c isof te_app te x)
+ )
+ "
isof_app "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2"
(* The extented correspondence relation *)
hasty_fun_def
- " hasty_fun(r) == \
-\ { p. \
-\ ( ? c t. p = (v_const(c),t) & c isof t) | \
-\ ( ? ev e ve t te. \
-\ p = (v_clos(<|ev,e,ve|>),t) & \
-\ te |- fn ev => e ===> t & \
-\ ve_dom(ve) = te_dom(te) & \
-\ (! ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r) \
-\ ) \
-\ } \
-\ "
+ " hasty_fun(r) ==
+ { p.
+ ( ? c t. p = (v_const(c),t) & c isof t) |
+ ( ? ev e ve t te.
+ p = (v_clos(<|ev,e,ve|>),t) &
+ te |- fn ev => e ===> t &
+ ve_dom(ve) = te_dom(te) &
+ (! ev1.ev1:ve_dom(ve) --> (ve_app ve ev1,te_app te ev1) : r)
+ )
+ }
+ "
hasty_rel_def "hasty_rel == gfp(hasty_fun)"
hasty_def "v hasty t == (v,t) : hasty_rel"
hasty_env_def
- " ve hastyenv te == \
-\ ve_dom(ve) = te_dom(te) & \
-\ (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
+ " ve hastyenv te ==
+ ve_dom(ve) = te_dom(te) &
+ (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)"
end
--- a/src/HOL/ex/Qsort.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/Qsort.thy Wed Jun 21 15:47:10 1995 +0200
@@ -13,15 +13,15 @@
rules
qsort_Nil "qsort le [] = []"
-qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ \
-\ (x# qsort le [y:xs . le x y])"
+qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @
+ (x# qsort le [y:xs . le x y])"
(* computational induction.
The dependence of p on x but not xs is intentional.
*)
qsort_ind
- "[| P([]); \
-\ !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> \
-\ P(x#xs) |] \
-\ ==> P(xs)"
+ "[| P([]);
+ !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==>
+ P(x#xs) |]
+ ==> P(xs)"
end
--- a/src/HOL/ex/SList.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/SList.thy Wed Jun 21 15:47:10 1995 +0200
@@ -89,12 +89,12 @@
(* list Recursion -- the trancl is Essential; see list.ML *)
List_rec_def
- "List_rec M c d == wfrec (trancl pred_sexp) M \
-\ (List_case (%g.c) (%x y g. d x y (g y)))"
+ "List_rec M c d == wfrec (trancl pred_sexp) M
+ (List_case (%g.c) (%x y g. d x y (g y)))"
list_rec_def
- "list_rec l c d == \
-\ List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)"
+ "list_rec l c d ==
+ List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)"
(* Generalized Map Functionals *)
@@ -107,13 +107,13 @@
(* a total version of tl: *)
ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)"
- mem_def "x mem xs == \
-\ list_rec xs False (%y ys r. if y=x then True else r)"
+ mem_def "x mem xs ==
+ list_rec xs False (%y ys r. if y=x then True else r)"
list_all_def "list_all P xs == list_rec xs True (%x l r. P(x) & r)"
map_def "map f xs == list_rec xs [] (%x l r. f(x)#r)"
append_def "xs@ys == list_rec xs ys (%x l r. x#r)"
- filter_def "filter P xs == \
-\ list_rec xs [] (%x xs r. if P(x) then x#r else r)"
+ filter_def "filter P xs ==
+ list_rec xs [] (%x xs r. if P(x) then x#r else r)"
list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
--- a/src/HOL/ex/Simult.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/Simult.thy Wed Jun 21 15:47:10 1995 +0200
@@ -31,12 +31,12 @@
Tcons :: "['a, 'a forest] => 'a tree"
Fcons :: "['a tree, 'a forest] => 'a forest"
Fnil :: "'a forest"
- TF_rec :: "['a item, ['a item , 'a item, 'b]=>'b, \
-\ 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
- tree_rec :: "['a tree, ['a, 'a forest, 'b]=>'b, \
-\ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
- forest_rec :: "['a forest, ['a, 'a forest, 'b]=>'b, \
-\ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
+ TF_rec :: "['a item, ['a item , 'a item, 'b]=>'b,
+ 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
+ tree_rec :: "['a tree, ['a, 'a forest, 'b]=>'b,
+ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
+ forest_rec :: "['a forest, ['a, 'a forest, 'b]=>'b,
+ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
defs
(*the concrete constants*)
@@ -48,8 +48,8 @@
Fnil_def "Fnil == Abs_Forest(FNIL)"
Fcons_def "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
- TF_def "TF(A) == lfp(%Z. A <*> Part Z In1 \
-\ <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
+ TF_def "TF(A) == lfp(%Z. A <*> Part Z In1
+ <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
rules
(*faking a type definition for tree...*)
@@ -66,17 +66,17 @@
defs
(*recursion*)
TF_rec_def
- "TF_rec M b c d == wfrec (trancl pred_sexp) M \
-\ (Case (Split(%x y g. b x y (g y))) \
-\ (List_case (%g.c) (%x y g. d x y (g x) (g y))))"
+ "TF_rec M b c d == wfrec (trancl pred_sexp) M
+ (Case (Split(%x y g. b x y (g y)))
+ (List_case (%g.c) (%x y g. d x y (g x) (g y))))"
tree_rec_def
- "tree_rec t b c d == \
-\ TF_rec (Rep_Tree t) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) \
-\ c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
+ "tree_rec t b c d ==
+ TF_rec (Rep_Tree t) (%x y r. b (Inv Leaf x) (Abs_Forest y) r)
+ c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
forest_rec_def
- "forest_rec tf b c d == \
-\ TF_rec (Rep_Forest tf) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) \
-\ c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
+ "forest_rec tf b c d ==
+ TF_rec (Rep_Forest tf) (%x y r. b (Inv Leaf x) (Abs_Forest y) r)
+ c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
end
--- a/src/HOL/ex/Term.thy Wed Jun 21 15:14:58 1995 +0200
+++ b/src/HOL/ex/Term.thy Wed Jun 21 15:47:10 1995 +0200
@@ -40,12 +40,12 @@
(*list recursion*)
Term_rec_def
- "Term_rec M d == wfrec (trancl pred_sexp) M \
-\ (Split(%x y g. d x y (Abs_map g y)))"
+ "Term_rec M d == wfrec (trancl pred_sexp) M
+ (Split(%x y g. d x y (Abs_map g y)))"
term_rec_def
- "term_rec t d == \
-\ Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)"
+ "term_rec t d ==
+ Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)"
rules
(*faking a type definition for term...*)