--- a/IMP/Denotation.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IMP/Denotation.thy Wed Jun 21 15:12:40 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/IOA/example/Channels.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Channels.thy Wed Jun 21 15:12:40 1995 +0200
@@ -21,46 +21,46 @@
defs
-srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)}, \
-\ UN pkt. {R_pkt(pkt)}, \
-\ {}>"
+srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)},
+ UN pkt. {R_pkt(pkt)},
+ {}>"
-rsch_asig_def "rsch_asig == <UN b. {S_ack(b)}, \
-\ UN b. {R_ack(b)}, \
-\ {}>"
+rsch_asig_def "rsch_asig == <UN b. {S_ack(b)},
+ UN b. {R_ack(b)},
+ {}>"
-srch_trans_def "srch_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in \
-\ case fst(snd(tr)) \
-\ of S_msg(m) => False | \
-\ R_msg(m) => False | \
-\ S_pkt(pkt) => t = addm(s, pkt) | \
-\ R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) | \
-\ 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}"
+srch_trans_def "srch_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of S_msg(m) => False |
+ R_msg(m) => False |
+ S_pkt(pkt) => t = addm(s, pkt) |
+ R_pkt(pkt) => count(s, pkt) ~= 0 & t = delm(s, pkt) |
+ 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}"
-rsch_trans_def "rsch_trans == \
-\ {tr. let s = fst(tr); \
-\ t = snd(snd(tr)) \
-\ in \
-\ case fst(snd(tr)) \
-\ of \
-\ S_msg(m) => False | \
-\ R_msg(m) => False | \
-\ S_pkt(pkt) => False | \
-\ R_pkt(pkt) => False | \
-\ S_ack(b) => t = addm(s,b) | \
-\ R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) | \
-\ C_m_s => False | \
-\ C_m_r => False | \
-\ C_r_s => False | \
-\ C_r_r(m) => False}"
+rsch_trans_def "rsch_trans ==
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ S_msg(m) => False |
+ R_msg(m) => False |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => False |
+ S_ack(b) => t = addm(s,b) |
+ R_ack(b) => count(s,b) ~= 0 & t = delm(s,b) |
+ C_m_s => False |
+ C_m_r => False |
+ C_r_s => False |
+ C_r_r(m) => False}"
srch_ioa_def "srch_ioa == <srch_asig, {{|}}, srch_trans>"
--- a/IOA/example/Correctness.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Correctness.thy Wed Jun 21 15:12:40 1995 +0200
@@ -15,8 +15,8 @@
defs
hom_def
-"hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)), \
-\ sq(sen(s)), \
-\ ttl(sq(sen(s))))"
+"hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)),
+ sq(sen(s)),
+ ttl(sq(sen(s))))"
end
--- a/IOA/example/Impl.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Impl.thy Wed Jun 21 15:12:40 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/IOA/example/Receiver.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Receiver.thy Wed Jun 21 15:12:40 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/IOA/example/Sender.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Sender.thy Wed Jun 21 15:12:40 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/IOA/example/Spec.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/example/Spec.thy Wed Jun 21 15:12:40 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/IOA/meta_theory/Asig.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/meta_theory/Asig.thy Wed Jun 21 15:12:40 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/IOA/meta_theory/IOA.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/meta_theory/IOA.thy Wed Jun 21 15:12:40 1995 +0200
@@ -60,9 +60,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"
@@ -70,9 +70,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:
@@ -80,15 +80,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)}"
(* Is a state reachable. Using an inductive definition, this could be defined
@@ -113,10 +113,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),Some(x),None))"
+ "filter_oseq(p,s) ==
+ (%i.case s(i)
+ of None => None
+ | Some(x) => if(p(x),Some(x),None))"
mk_behaviour_def
@@ -125,8 +125,8 @@
(* Does an ioa have an execution with the given behaviour *)
has_behaviour_def
- "has_behaviour(ioa,b) == \
-\ (? ex:executions(ioa). b = mk_behaviour(ioa,fst(ex)))"
+ "has_behaviour(ioa,b) ==
+ (? ex:executions(ioa). b = mk_behaviour(ioa,fst(ex)))"
(* All the behaviours of an ioa *)
@@ -135,10 +135,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
@@ -146,41 +146,41 @@
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)), \
- \ <fst(s),a,fst(t)>:trans_of(ioa1), \
- \ fst(t) = fst(s)) \
- \ & \
- \ if(a:actions(asig_of(ioa2)), \
- \ <snd(s),a,snd(t)>:trans_of(ioa2), \
- \ 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)),
+ <fst(s),a,fst(t)>:trans_of(ioa1),
+ fst(t) = fst(s))
+ &
+ if(a:actions(asig_of(ioa2)),
+ <snd(s),a,snd(t)>:trans_of(ioa2),
+ 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) == \
-\ (externals(asig_of(ioa1)) = externals(asig_of(ioa2)) & \
-\ behaviours(ioa1) <= behaviours(ioa2))"
+ "ioa_implements(ioa1,ioa2) ==
+ (externals(asig_of(ioa1)) = externals(asig_of(ioa2)) &
+ behaviours(ioa1) <= behaviours(ioa2))"
end
--- a/IOA/meta_theory/Solve.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/IOA/meta_theory/Solve.thy Wed Jun 21 15:12:40 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)), \
-\ <f(s),a,f(t)>:trans_of(A), \
-\ 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)),
+ <f(s),a,f(t)>:trans_of(A),
+ f(s)=f(t)))"
end
--- a/Integ/Equiv.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Integ/Equiv.thy Wed Jun 21 15:12:40 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/Integ/Integ.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Integ/Integ.thy Wed Jun 21 15:12:40 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/Nat.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Nat.thy Wed Jun 21 15:12:40 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/Sexp.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Sexp.thy Wed Jun 21 15:12:40 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/Subst/Subst.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Subst/Subst.thy Wed Jun 21 15:12:40 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, g Int Compl({x}), g Un {x}))"
+ "sdom(al) == alist_rec(al, {},
+ %x y xs g.if(Var(x)=y, g Int Compl({x}), g Un {x}))"
srange_def
"srange(al) == Union({y. EX x:sdom(al).y=vars_of(Var(x) <| al)})"
--- a/Subst/UTerm.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Subst/UTerm.thy Wed Jun 21 15:12:40 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/Subst/Unifier.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Subst/Unifier.thy Wed Jun 21 15:12:40 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/Sum.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Sum.thy Wed Jun 21 15:12:40 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/Univ.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Univ.thy Wed Jun 21 15:12:40 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,18 +86,18 @@
(*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" **)
diag_def "diag(A) == UN x:A. {<x,x>}"
- dprod_def "r<**>s == UN u:r. split(%x x'. \
-\ UN v:s. split(%y y'. {<x$y,x'$y'>}, v), u)"
+ dprod_def "r<**>s == UN u:r. split(%x x'.
+ UN v:s. split(%y y'. {<x$y,x'$y'>}, v), u)"
- dsum_def "r<++>s == (UN u:r. split(%x x'. {<In0(x),In0(x')>}, u)) Un \
-\ (UN v:s. split(%y y'. {<In1(y),In1(y')>}, v))"
+ dsum_def "r<++>s == (UN u:r. split(%x x'. {<In0(x),In0(x')>}, u)) Un
+ (UN v:s. split(%y y'. {<In1(y),In1(y')>}, v))"
end
--- a/ex/LList.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/LList.thy Wed Jun 21 15:12:40 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(Unity), %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(Unity), %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(Unity), %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(Unity), %n1 n2. Inr(<n1, <LNil,n2>>)),
+ %l1 l2 n. Inr(<l1, <l2,n>>))))"
rules
(*faking a type definition...*)
--- a/ex/LexProd.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/LexProd.thy Wed Jun 21 15:12:40 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/ex/MT.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/MT.thy Wed Jun 21 15:12:40 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/ex/Qsort.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/Qsort.thy Wed Jun 21 15:12:40 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/ex/SList.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/SList.thy Wed Jun 21 15:12:40 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, True, r))"
+ mem_def "x mem xs ==
+ list_rec(xs, False, %y ys r. if(y=x, True, 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), x#r, r))"
+ filter_def "filter(P,xs) ==
+ list_rec(xs, [], %x xs r. if(P(x), x#r, r))"
list_case_def "list_case(a, f, xs) == list_rec(xs, a, %x xs r.f(x, xs))"
--- a/ex/Simult.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/Simult.thy Wed Jun 21 15:12:40 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/ex/Term.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/ex/Term.thy Wed Jun 21 15:12:40 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...*)