# HG changeset patch # User nipkow # Date 784407069 -3600 # Node ID 44ff2275d44f1e5f58f42aa3ccc35acf0373aa67 # Parent 37a6e2f5523076cd20c8c3d26838094034ac873b Added headers and made various small mods. diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Action.ML --- 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); diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Action.thy --- 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) diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Channels.ML --- 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; diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Channels.thy --- 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 == " -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}" diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Correctness.ML --- 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(); diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Correctness.thy --- 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)), \ diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Impl.ML --- 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, diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Impl.thy --- 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)" diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Lemmas.ML --- 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); diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Lemmas.thy --- 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 diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Multiset.ML --- 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); diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Multiset.thy --- 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 diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Packet.thy --- 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 diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Receiver.ML --- 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 = diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Receiver.thy --- 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 == \ -\ " 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) & \ diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Sender.ML --- 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 = diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Sender.thy --- 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" diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Spec.thy --- 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 == " -trans_def "spec_trans = \ +trans_def "spec_trans == \ \ {tr. let s = fst(tr); \ \ t = snd(snd(tr)) \ \ in \ diff -r 37a6e2f55230 -r 44ff2275d44f IOA/meta_theory/Asig.thy --- 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))" diff -r 37a6e2f55230 -r 44ff2275d44f IOA/meta_theory/IOA.ML --- 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 & starts_of() = y & trans_of() = 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)), \ \ :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(); diff -r 37a6e2f55230 -r 44ff2275d44f IOA/meta_theory/IOA.thy --- 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. :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)) & \ diff -r 37a6e2f55230 -r 44ff2275d44f IOA/meta_theory/Option.ML --- 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; diff -r 37a6e2f55230 -r 44ff2275d44f IOA/meta_theory/Option.thy --- 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 diff -r 37a6e2f55230 -r 44ff2275d44f IOA/meta_theory/Solve.ML --- 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]; diff -r 37a6e2f55230 -r 44ff2275d44f IOA/meta_theory/Solve.thy --- 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) & \ -\ :trans_of(C) \ -\ --> if(a:externals(asig_of(C)), \ -\ :trans_of(A), \ + "is_weak_pmap(f,C,A) == \ +\ (!s:starts_of(C). f(s):starts_of(A)) & \ +\ (!s t a. reachable(C,s) & \ +\ :trans_of(C) \ +\ --> if(a:externals(asig_of(C)), \ +\ :trans_of(A), \ \ f(s)=f(t)))" end