Added headers and made various small mods.
--- a/IOA/example/Action.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Action.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/IOA/example/Action.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Derived rules for actions
+*)
+
goal Action.thy "!!x. x = y ==> action_case(a,b,c,d,e,f,g,h,i,j,x) = \
\ action_case(a,b,c,d,e,f,g,h,i,j,y)";
by (asm_simp_tac HOL_ss 1);
--- a/IOA/example/Action.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Action.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/IOA/example/Action.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The set of all actions of the system
+*)
+
Action = Packet +
datatype 'm action = S_msg ('m) | R_msg ('m)
| S_pkt ('m packet) | R_pkt ('m packet)
--- a/IOA/example/Channels.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Channels.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,10 +1,19 @@
+(* Title: HOL/IOA/example/Channels.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Derived rules
+*)
+
local
val SS = action_ss addsimps
(Channels.srch_asig_def ::
Channels.rsch_asig_def ::
- actions_def :: asig_projections_def :: set_lemmas)
+ actions_def :: asig_projections @ set_lemmas)
in
-val _ = goal Channels.thy
+
+val in_srch_asig = prove_goal Channels.thy
"S_msg(m) ~: actions(srch_asig) & \
\ R_msg(m) ~: actions(srch_asig) & \
\ S_pkt(pkt) : actions(srch_asig) & \
@@ -14,13 +23,10 @@
\ C_m_s ~: actions(srch_asig) & \
\ C_m_r ~: actions(srch_asig) & \
\ C_r_s ~: actions(srch_asig) & \
- \ C_r_r(m) ~: actions(srch_asig)";
-
-val _ = by (simp_tac SS 1);
+ \ C_r_r(m) ~: actions(srch_asig)"
+ (fn _ => [simp_tac SS 1]);
-val in_srch_asig = result();
-
-val _ = goal Channels.thy
+val in_rsch_asig = prove_goal Channels.thy
"S_msg(m) ~: actions(rsch_asig) & \
\ R_msg(m) ~: actions(rsch_asig) & \
\ S_pkt(pkt) ~: actions(rsch_asig) & \
@@ -30,10 +36,7 @@
\ C_m_s ~: actions(rsch_asig) & \
\ C_m_r ~: actions(rsch_asig) & \
\ C_r_s ~: actions(rsch_asig) & \
- \ C_r_r(m) ~: actions(rsch_asig)";
-
-val _ = by (simp_tac SS 1);
-
-val in_rsch_asig = result();
+ \ C_r_r(m) ~: actions(rsch_asig)"
+ (fn _ => [simp_tac SS 1]);
end;
--- a/IOA/example/Channels.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Channels.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,12 @@
-Channels = IOA + Action + Multiset + "Lemmas" + Packet +
+(* Title: HOL/IOA/example/Channels.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The (faulty) transmission channels (both directions)
+*)
+
+Channels = IOA + Action + Multiset +
consts
@@ -11,7 +19,7 @@
srch_ioa :: "('m action, 'm packet multiset)ioa"
rsch_ioa :: "('m action, bool multiset)ioa"
-rules
+defs
srch_asig_def "srch_asig == <UN pkt. {S_pkt(pkt)}, \
\ UN pkt. {R_pkt(pkt)}, \
@@ -21,37 +29,37 @@
\ 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 | \
+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_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 | \
+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_m_s => False | \
+\ C_m_r => False | \
+\ C_r_s => False | \
\ C_r_r(m) => False}"
--- a/IOA/example/Correctness.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Correctness.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/IOA/example/Correctness.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The main correctness proof: Impl implements Spec
+*)
+
open Impl;
open Spec;
@@ -28,13 +36,12 @@
\ | C_r_s => False \
\ | C_r_r(m) => False)";
by(simp_tac (hom_ss addcongs [if_weak_cong]
- addsimps ([asig_projections_def,externals_def,
- restrict_def,restrict_asig_def,
- asig_of_par, asig_comp_def, Spec.sig_def]
- @ impl_ioas @ impl_asigs)) 1);
- by(Action.action.induct_tac "a" 1);
+ addsimps ([externals_def, restrict_def, restrict_asig_def,
+ asig_of_par, asig_comp_def, Spec.sig_def] @
+ asig_projections @ impl_ioas @ impl_asigs)) 1);
+ by(Action.action.induct_tac "a" 1);
by(ALLGOALS(simp_tac (action_ss addsimps
- (actions_def :: asig_projections_def :: set_lemmas))));
+ (actions_def :: asig_projections @ set_lemmas))));
val externals_lemma = result();
--- a/IOA/example/Correctness.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Correctness.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,11 +1,18 @@
-Correctness = Solve + Impl + Spec + "Lemmas" +
+(* Title: HOL/IOA/example/Correctness.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The main correctness proof: Impl implements Spec
+*)
+
+Correctness = Solve + Impl + Spec +
consts
hom :: "'m impl_state => 'm list"
-
-rules
+defs
hom_def
"hom(s) == rq(rec(s)) @ if(rbit(rec(s)) = sbit(sen(s)), \
--- a/IOA/example/Impl.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Impl.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/IOA/example/Impl.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation --- Invariants
+*)
+
val impl_ioas =
[Impl.impl_def,
Sender.sender_ioa_def,
--- a/IOA/example/Impl.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Impl.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/IOA/example/Impl.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation
+*)
+
Impl = Sender + Receiver + Channels +
types
@@ -17,7 +25,7 @@
inv3, inv4 :: "'m impl_state => bool"
hdr_sum :: "'m packet multiset => bool => nat"
-rules
+defs
impl_def
"impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
--- a/IOA/example/Lemmas.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Lemmas.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,13 @@
+(* Title: HOL/IOA/example/Lemmas.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+(Mostly) Arithmetic lemmas
+Should realy go in Arith.ML.
+Also: Get rid of all the --> in favour of ==> !!!
+*)
+
(* Logic *)
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
by(fast_tac (HOL_cs addDs prems) 1);
--- a/IOA/example/Lemmas.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Lemmas.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,1 +1,9 @@
+(* Title: HOL/IOA/example/Lemmas.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Arithmetic lemmas
+*)
+
Lemmas = Arith
--- a/IOA/example/Multiset.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Multiset.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,12 @@
+(* Title: HOL/IOA/example/Multiset.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Axiomatic multisets.
+Should be done as a subtype and moved to a global place.
+*)
+
goalw Multiset.thy [Multiset.count_def, Multiset.countm_empty_def]
"count({|},x) = 0";
by (rtac refl 1);
--- a/IOA/example/Multiset.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Multiset.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,12 @@
+(* Title: HOL/IOA/example/Multiset.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Axiomatic multisets.
+Should be done as a subtype and moved to a global place.
+*)
+
Multiset = Arith + "Lemmas" +
types
--- a/IOA/example/Packet.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Packet.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/IOA/example/Packet.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Packets
+*)
+
Packet = Arith +
types
@@ -9,10 +17,9 @@
hdr :: "'msg packet => bool"
msg :: "'msg packet => 'msg"
-rules
+defs
hdr_def "hdr == fst"
-
msg_def "msg == snd"
end
--- a/IOA/example/Receiver.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Receiver.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,9 @@
+(* Title: HOL/IOA/example/Receiver.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+*)
+
goal Receiver.thy
"S_msg(m) ~: actions(receiver_asig) & \
\ R_msg(m) : actions(receiver_asig) & \
@@ -11,7 +17,7 @@
\ C_r_r(m) : actions(receiver_asig)";
by(simp_tac (action_ss addsimps
(Receiver.receiver_asig_def :: actions_def ::
- asig_projections_def :: set_lemmas)) 1);
+ asig_projections @ set_lemmas)) 1);
val in_receiver_asig = result();
val receiver_projections =
--- a/IOA/example/Receiver.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Receiver.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,12 @@
-Receiver = List + IOA + Action + Multiset + "Lemmas" +
+(* Title: HOL/IOA/example/Receiver.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation: receiver
+*)
+
+Receiver = List + IOA + Action + Multiset +
types
@@ -17,7 +25,7 @@
rbit :: "'m receiver_state => bool"
rsending :: "'m receiver_state => bool"
-rules
+defs
rq_def "rq == fst"
rsent_def "rsent == fst o snd"
@@ -25,9 +33,9 @@
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)}), \
+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 == \
@@ -55,7 +63,7 @@
\ rbit(t)=rbit(s) & \
\ rsending(s) & \
\ rsending(t) | \
-\R_ack(b) => False | \
+\ 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) & \
--- a/IOA/example/Sender.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Sender.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,9 @@
+(* Title: HOL/IOA/example/Sender.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+*)
+
goal Sender.thy
"S_msg(m) : actions(sender_asig) & \
\ R_msg(m) ~: actions(sender_asig) & \
@@ -11,7 +17,7 @@
\ C_r_r(m) ~: actions(sender_asig)";
by(simp_tac (action_ss addsimps
(Sender.sender_asig_def :: actions_def ::
- asig_projections_def :: set_lemmas)) 1);
+ asig_projections @ set_lemmas)) 1);
val in_sender_asig = result();
val sender_projections =
--- a/IOA/example/Sender.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Sender.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,12 @@
-Sender = IOA + Action + Multiset + List + "Lemmas" +
+(* Title: HOL/IOA/example/Sender.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The implementation: sender
+*)
+
+Sender = IOA + Action + Multiset + List +
types
@@ -15,7 +23,7 @@
sbit :: "'m sender_state => bool"
ssending :: "'m sender_state => bool"
-rules
+defs
sq_def "sq == fst"
ssent_def "ssent == fst o snd"
--- a/IOA/example/Spec.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/example/Spec.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/IOA/example/Spec.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The specification of reliable transmission
+*)
+
Spec = List + IOA + Action +
consts
@@ -6,13 +14,13 @@
spec_trans :: "('m action, 'm list)transition set"
spec_ioa :: "('m action, 'm list)ioa"
-rules
+defs
sig_def "spec_sig == <UN m.{S_msg(m)}, \
\ UN m.{R_msg(m)}, \
\ {}>"
-trans_def "spec_trans = \
+trans_def "spec_trans == \
\ {tr. let s = fst(tr); \
\ t = snd(snd(tr)) \
\ in \
--- a/IOA/meta_theory/Asig.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/Asig.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: HOL/IOA/meta_theory/Asig.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Action signatures
+*)
+
Asig = Option +
types
@@ -11,10 +19,11 @@
mk_ext_asig ::"'action signature => 'action signature"
-rules
+defs
-asig_projections_def
- "inputs = fst & outputs = (fst o snd) & internals = (snd o snd)"
+asig_inputs_def "inputs == fst"
+asig_outputs_def "outputs == (fst o snd)"
+asig_internals_def "internals == (snd o snd)"
actions_def
"actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
--- a/IOA/meta_theory/IOA.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/IOA.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,10 +1,20 @@
+(* Title: HOL/IOA/meta_theory/IOA.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The I/O automata of Lynch and Tuttle.
+*)
+
open IOA Asig;
+val ioa_projections = [asig_of_def, starts_of_def, trans_of_def];
+
val exec_rws = [executions_def,is_execution_fragment_def];
goal IOA.thy
"asig_of(<x,y,z>) = x & starts_of(<x,y,z>) = y & trans_of(<x,y,z>) = z";
- by (simp_tac (SS addsimps [ioa_projections_def]) 1);
+ by (simp_tac (SS addsimps ioa_projections) 1);
val ioa_triple_proj = result();
goalw IOA.thy [ioa_def,state_trans_def,actions_def, is_asig_def]
@@ -94,13 +104,13 @@
goal IOA.thy
"actions(asig_comp(a,b)) = actions(a) Un actions(b)";
by(simp_tac (pair_ss addsimps
- [actions_def,asig_projections_def,asig_comp_def]) 1);
+ ([actions_def,asig_comp_def]@asig_projections)) 1);
by(fast_tac eq_cs 1);
val actions_asig_comp = result();
goal IOA.thy
"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
- by(simp_tac (SS addsimps [par_def,ioa_projections_def]) 1);
+ by(simp_tac (SS addsimps (par_def::ioa_projections)) 1);
val starts_of_par = result();
(* Every state in an execution is reachable *)
@@ -123,18 +133,18 @@
\ if(a:actions(asig_of(D)), \
\ <snd(snd(snd(s))),a,snd(snd(snd(t)))>:trans_of(D), \
\ snd(snd(snd(t)))=snd(snd(snd(s)))))";
- by(simp_tac (SS addsimps [par_def,ioa_projections_def,actions_asig_comp,
- Pair_fst_snd_eq (* old pair_eq *)]
+ by(simp_tac (SS addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@
+ ioa_projections)
setloop (split_tac [expand_if])) 1);
val trans_of_par4 = result();
goal IOA.thy "starts_of(restrict(ioa,acts)) = starts_of(ioa) & \
\ trans_of(restrict(ioa,acts)) = trans_of(ioa) & \
\ reachable(restrict(ioa,acts),s) = reachable(ioa,s)";
- by (simp_tac (SS addsimps [ioa_projections_def,is_execution_fragment_def,
- executions_def,reachable_def,restrict_def]) 1);
+by(simp_tac (SS addsimps ([is_execution_fragment_def,executions_def,
+ reachable_def,restrict_def]@ioa_projections)) 1);
val cancel_restrict = result();
goal IOA.thy "asig_of(A || B) = asig_comp(asig_of(A),asig_of(B))";
- by(simp_tac (SS addsimps [ioa_projections_def,par_def]) 1);
+ by(simp_tac (SS addsimps (par_def::ioa_projections)) 1);
val asig_of_par = result();
--- a/IOA/meta_theory/IOA.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/IOA.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,10 @@
-(* The I/O automata of Lynch and Tuttle. *)
+(* Title: HOL/IOA/meta_theory/IOA.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+The I/O automata of Lynch and Tuttle.
+*)
IOA = Asig +
@@ -51,7 +57,7 @@
ioa_implements :: "[('action,'state1)ioa, ('action,'state2)ioa] => bool"
-rules
+defs
state_trans_def
"state_trans(asig,R) == \
@@ -59,9 +65,9 @@
\ (!a. (a:inputs(asig)) --> (!s1. ? s2. <s1,a,s2>:R))"
-ioa_projections_def
- "asig_of = fst & starts_of = (fst o snd) & trans_of = (snd o snd)"
-
+asig_of_def "asig_of == fst"
+starts_of_def "starts_of == (fst o snd)"
+trans_of_def "trans_of == (snd o snd)"
ioa_def
"IOA(ioa) == (is_asig(asig_of(ioa)) & \
--- a/IOA/meta_theory/Option.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/Option.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: Option.ML
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1994 TU Muenchen
+
+Derived rules
+*)
+
val option_rws = Let_def :: Option.option.simps;
val SS = arith_ss addsimps option_rws;
--- a/IOA/meta_theory/Option.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/Option.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,3 +1,11 @@
+(* Title: Option.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1994 TU Muenchen
+
+Datatype 'a option
+*)
+
Option = Arith +
datatype 'a option = None | Some('a)
end
--- a/IOA/meta_theory/Solve.ML Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/Solve.ML Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,12 @@
-open Solve IOA Asig;
+(* Title: HOL/IOA/meta_theory/Solve.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Weak possibilities mapping (abstraction)
+*)
+
+open Solve;
val SS = SS addsimps [mk_behaviour_thm,trans_in_actions];
--- a/IOA/meta_theory/Solve.thy Wed Nov 09 19:50:36 1994 +0100
+++ b/IOA/meta_theory/Solve.thy Wed Nov 09 19:51:09 1994 +0100
@@ -1,4 +1,10 @@
-(* Methods of proof for IOA. *)
+(* Title: HOL/IOA/meta_theory/Solve.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Weak possibilities mapping (abstraction)
+*)
Solve = IOA +
@@ -6,15 +12,15 @@
is_weak_pmap :: "['c => 'a, ('action,'c)ioa,('action,'a)ioa] => bool"
-rules
+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), \
+ "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