New meta theory for IOA based on HOLCF.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/README.html Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,38 @@
+<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
+
+<H3>IOA: A formalization of I/O automata in HOLCF</H3>
+
+Author: Olaf Mueller<BR>
+Copyright 1997 Technische Universität München<P>
+
+Version: 1.0<BR>
+Date: 1.05.97<P>
+
+The distribution contains
+
+<UL>
+ <li> A semantic model of the meta theory of I/O automata including proofs for the refinement notion
+ and the compositionality of the model. For details see: <BR>
+ Olaf Müller and Tobias Nipkow,
+ <A HREF="http://www4.informatik.tu-muenchen.de/papers/tapsoft_mueller_1997_Conference.html">Traces of I/O Automata in Isabelle/HOLCF</A>.
+In <i> TAPSOFT'97, Proc. of the 7th International Joint Conference on Theory and Practice of Software Development </i>, LNCS 1224, 1997.<P>
+
+ <li> A proof of the Alternating Bit Protocol (ABP subdirectory) with unbounded buffers using
+ a combination of Isabelle and a model checker. This case study is performed within the
+ theory of IOA described above. For details see:<BR>
+Olaf Müller and Tobias Nipkow,
+<A HREF="http://www4.informatik.tu-muenchen.de/papers/MuellerNipkow_TaAf1995.html">Combining Model Checking and Deduction for I/O Automata </A>.
+In <i> TACAS'95, Proc. of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems </i>, LNCS 1019, 1995.<P>
+ <li> A proof of a Network Transmission Protocol (NTP subdirectory) using the theory of IOA described above. For details see:<BR>
+
+ Tobias Nipkow, Konrad Slind.
+<A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ioa.html>
+I/O Automata in Isabelle/HOL</A>. In <i>Types for Proofs and Programs</i>,
+LNCS 996, 1995, 101-119.
+
+</UL>
+
+</BODY></HTML>
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/ROOT.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,18 @@
+(* Title: HOL/IOA/meta_theory/ROOT.ML
+ ID: $Id$
+ Author: Olaf Mueller
+ Copyright 1997 TU Muenchen
+
+This is the ROOT file for the formalization of a semantic model of I/O-Automata.
+
+See the README.html file for details.
+
+Should be executed in the subdirectory HOLCF/IOA/meta_theory.
+*)
+
+
+goals_limit:=1;
+
+loadpath := ["meta_theory"];
+
+use_thy"IOA";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Asig.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,38 @@
+(* Title: HOL/IOA/meta_theory/Asig.ML
+ ID: $Id$
+ Author: Olaf Mueller, Tobias Nipkow & Konrad Slind
+ Copyright 1994,1996 TU Muenchen
+
+Action signatures
+*)
+
+open Asig;
+
+val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
+
+goal thy "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
+by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
+qed"int_and_ext_is_act";
+
+goal thy "!!a.[|a:externals(S)|] ==> a:actions(S)";
+by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
+qed"ext_is_act";
+
+goal thy "!!a.[|a:internals S|] ==> a:actions S";
+by (asm_full_simp_tac (!simpset addsimps [asig_internals_def,actions_def]) 1);
+qed"int_is_act";
+
+goal thy "(x: actions S & x : externals S) = (x: externals S)";
+by (fast_tac (!claset addSIs [ext_is_act]) 1 );
+qed"ext_and_act";
+
+goal thy "!!S. [|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,is_asig_def,externals_def]) 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"not_ext_is_int";
+
+goalw thy [externals_def,actions_def,is_asig_def]
+ "!! x. [| is_asig (S); x:internals S |] ==> x~:externals S";
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"int_is_not_ext";
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Asig.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,45 @@
+(* Title: HOL/IOA/meta_theory/Asig.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
+
+Action signatures
+*)
+
+Asig = Arith +
+
+types
+
+'a signature = "('a set * 'a set * 'a set)"
+
+consts
+ actions,inputs,outputs,internals,externals
+ ::"'action signature => 'action set"
+ is_asig ::"'action signature => bool"
+ mk_ext_asig ::"'action signature => 'action signature"
+
+
+defs
+
+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))"
+
+externals_def
+ "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) = {}))"
+
+
+mk_ext_asig_def
+ "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,283 @@
+(* Title: HOLCF/IOA/meta_theory/Automata.ML
+ ID: $$
+ Author: Olaf Mueller, Tobias Nipkow, Konrad Slind
+ Copyright 1994, 1996 TU Muenchen
+
+The I/O automata of Lynch and Tuttle.
+*)
+
+(* Has been removed from HOL-simpset, who knows why? *)
+Addsimps [Let_def];
+
+open reachable;
+
+val ioa_projections = [asig_of_def, starts_of_def, trans_of_def];
+
+(* ----------------------------------------------------------------------------------- *)
+
+section "asig_of, starts_of, trans_of";
+
+
+goal thy
+"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z";
+ by (simp_tac (!simpset addsimps ioa_projections) 1);
+qed "ioa_triple_proj";
+
+goalw thy [ioa_def,state_trans_def,actions_def, is_asig_def]
+ "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:act A";
+ by (REPEAT(etac conjE 1));
+ by (EVERY1[etac allE, etac impE, atac]);
+ by (Asm_full_simp_tac 1);
+qed "trans_in_actions";
+
+goal thy
+"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
+ by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+qed "starts_of_par";
+
+
+(* ----------------------------------------------------------------------------------- *)
+
+section "actions and par";
+
+
+goal thy
+"actions(asig_comp a b) = actions(a) Un actions(b)";
+ by(simp_tac (!simpset addsimps
+ ([actions_def,asig_comp_def]@asig_projections)) 1);
+ by (fast_tac (set_cs addSIs [equalityI]) 1);
+qed "actions_asig_comp";
+
+
+goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
+ by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+qed "asig_of_par";
+
+
+goal thy "ext (A1||A2) = \
+\ (ext A1) Un (ext A2)";
+by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,
+ asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
+by (rtac set_ext 1);
+by (fast_tac set_cs 1);
+qed"externals_of_par";
+
+goal thy "act (A1||A2) = \
+\ (act A1) Un (act A2)";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
+ asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
+by (rtac set_ext 1);
+by (fast_tac set_cs 1);
+qed"actions_of_par";
+
+
+goal thy "inp (A1||A2) =\
+\ ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
+ asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
+qed"inputs_of_par";
+
+goal thy "out (A1||A2) =\
+\ (out A1) Un (out A2)";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
+ asig_outputs_def,Un_def,set_diff_def]) 1);
+qed"outputs_of_par";
+
+
+(* ---------------------------------------------------------------------------------- *)
+
+section "actions and compatibility";
+
+goal thy"compat_ioas A B = compat_ioas B A";
+by (asm_full_simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_commute]) 1);
+auto();
+qed"compat_commute";
+
+goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
+ "!! a. [| compat_ioas A1 A2; a:ext A1|] ==> a~:int A2";
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"ext1_is_not_int2";
+
+(* just commuting the previous one: better commute compat_ioas *)
+goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
+ "!! a. [| compat_ioas A2 A1 ; a:ext A1|] ==> a~:int A2";
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"ext2_is_not_int1";
+
+bind_thm("ext1_ext2_is_not_act2",ext1_is_not_int2 RS int_and_ext_is_act);
+bind_thm("ext1_ext2_is_not_act1",ext2_is_not_int1 RS int_and_ext_is_act);
+
+goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
+ "!! x. [| compat_ioas A B; x:int A |] ==> x~:ext B";
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"intA_is_not_extB";
+
+goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def,is_asig_def,asig_of_def]
+"!! a. [| compat_ioas A B; a:int A |] ==> a ~: act B";
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"intA_is_not_actB";
+
+
+(* ---------------------------------------------------------------------------------- *)
+
+section "invariants";
+
+val [p1,p2] = goalw thy [invariant_def]
+ "[| !!s. s:starts_of(A) ==> P(s); \
+\ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
+\ ==> invariant A P";
+by (rtac allI 1);
+by (rtac impI 1);
+by (res_inst_tac [("za","s")] reachable.induct 1);
+by (atac 1);
+by (etac p1 1);
+by (eres_inst_tac [("s1","sa")] (p2 RS mp) 1);
+by (REPEAT (atac 1));
+qed"invariantI";
+
+
+val [p1,p2] = goal thy
+ "[| !!s. s : starts_of(A) ==> P(s); \
+\ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
+\ |] ==> invariant A P";
+ by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
+qed "invariantI1";
+
+val [p1,p2] = goalw thy [invariant_def]
+"[| invariant A P; reachable A s |] ==> P(s)";
+ br(p2 RS (p1 RS spec RS mp))1;
+qed "invariantE";
+
+(* ---------------------------------------------------------------------------------- *)
+
+section "restrict";
+
+
+goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \
+\ trans_of(restrict ioa acts) = trans_of(ioa)";
+by(simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
+qed "cancel_restrict_a";
+
+goal thy "reachable (restrict ioa acts) s = reachable ioa s";
+by (rtac iffI 1);
+be reachable.induct 1;
+by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1);
+by (etac reachable_n 1);
+by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+(* <-- *)
+be reachable.induct 1;
+by (rtac reachable_0 1);
+by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+by (etac reachable_n 1);
+by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+qed "cancel_restrict_b";
+
+goal 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 (!simpset addsimps [cancel_restrict_a,cancel_restrict_b]) 1);
+qed"cancel_restrict";
+
+(* ---------------------------------------------------------------------------------- *)
+
+section "rename";
+
+
+
+goal thy "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
+by (asm_full_simp_tac (!simpset addsimps [Let_def,rename_def,trans_of_def]) 1);
+qed"trans_rename";
+
+
+goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
+be reachable.induct 1;
+br reachable_0 1;
+by(asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1);
+bd trans_rename 1;
+be exE 1;
+be conjE 1;
+be reachable_n 1;
+ba 1;
+qed"reachable_rename";
+
+
+
+(* ---------------------------------------------------------------------------------- *)
+
+section "trans_of(A||B)";
+
+
+goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \
+\ ==> (fst s,a,fst t):trans_of A";
+by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+qed"trans_A_proj";
+
+goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \
+\ ==> (snd s,a,snd t):trans_of B";
+by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+qed"trans_B_proj";
+
+goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\
+\ ==> fst s = fst t";
+by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+qed"trans_A_proj2";
+
+goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\
+\ ==> snd s = snd t";
+by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+qed"trans_B_proj2";
+
+goal thy "!!A.(s,a,t):trans_of (A||B) \
+\ ==> a :act A | a :act B";
+by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+qed"trans_AB_proj";
+
+goal thy "!!A. [|a:act A;a:act B;\
+\ (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]\
+\ ==> (s,a,t):trans_of (A||B)";
+by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+qed"trans_AB";
+
+goal thy "!!A. [|a:act A;a~:act B;\
+\ (fst s,a,fst t):trans_of A;snd s=snd t|]\
+\ ==> (s,a,t):trans_of (A||B)";
+by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+qed"trans_A_notB";
+
+goal thy "!!A. [|a~:act A;a:act B;\
+\ (snd s,a,snd t):trans_of B;fst s=fst t|]\
+\ ==> (s,a,t):trans_of (A||B)";
+by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
+qed"trans_notA_B";
+
+val trans_of_defs1 = [trans_AB,trans_A_notB,trans_notA_B];
+val trans_of_defs2 = [trans_A_proj,trans_B_proj,trans_A_proj2,
+ trans_B_proj2,trans_AB_proj];
+
+
+goal thy
+"(s,a,t) : trans_of(A || B || C || D) = \
+\ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) | \
+\ a:actions(asig_of(D))) & \
+\ (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A) \
+\ else fst t=fst s) & \
+\ (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B) \
+\ else fst(snd(t))=fst(snd(s))) & \
+\ (if a:actions(asig_of(C)) then \
+\ (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C) \
+\ else fst(snd(snd(t)))=fst(snd(snd(s)))) & \
+\ (if a:actions(asig_of(D)) then \
+\ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \
+\ else snd(snd(snd(t)))=snd(snd(snd(s)))))";
+
+ by(simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
+ ioa_projections)
+ setloop (split_tac [expand_if])) 1);
+qed "trans_of_par4";
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,162 @@
+(* Title: HOLCF/IOA/meta_theory/Automata.thy
+ ID:
+ Author: Olaf M"uller, Konrad Slind, Tobias Nipkow
+ Copyright 1995, 1996 TU Muenchen
+
+The I/O automata of Lynch and Tuttle in HOLCF.
+*)
+
+
+Automata = Option + Asig +
+
+default term
+
+types
+ ('a,'s)transition = "'s * 'a * 's"
+ ('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set"
+
+consts
+
+ (* IO automata *)
+ state_trans::"['a signature, ('a,'s)transition set] => bool"
+ asig_of ::"('a,'s)ioa => 'a signature"
+ starts_of ::"('a,'s)ioa => 's set"
+ trans_of ::"('a,'s)ioa => ('a,'s)transition set"
+ IOA ::"('a,'s)ioa => bool"
+
+ (* reachability and invariants *)
+ reachable :: "('a,'s)ioa => 's set"
+ invariant :: "[('a,'s)ioa, 's=>bool] => bool"
+
+ (* binary composition of action signatures and automata *)
+ compat_asigs ::"['a signature, 'a signature] => bool"
+ asig_comp ::"['a signature, 'a signature] => 'a signature"
+ compat_ioas ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
+ "||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr 10)
+
+ (* hiding *)
+ restrict_asig :: "['a signature, 'a set] => 'a signature"
+ restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
+
+ (* renaming *)
+ rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
+
+
+syntax
+
+ "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" ("_ -_--_-> _" [81,81,81,81] 100)
+ "reachable" :: "[('a,'s)ioa, 's] => bool"
+ "act" :: "('a,'s)ioa => 'a set"
+ "ext" :: "('a,'s)ioa => 'a set"
+ "int" :: "('a,'s)ioa => 'a set"
+ "inp" :: "('a,'s)ioa => 'a set"
+ "out" :: "('a,'s)ioa => 'a set"
+
+
+syntax (symbols)
+
+ "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool"
+ ("_ \\<midarrow>_\\<midarrow>_\\<midarrow>\\<rightarrow> _" [81,81,81,81] 100)
+ "op ||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\\<parallel>" 10)
+
+
+inductive "reachable C"
+ intrs
+ reachable_0 "s:(starts_of C) ==> s : reachable C"
+ reachable_n "[|s:reachable C; (s,a,t):trans_of C|] ==> t:reachable C"
+
+
+translations
+ "s -a--A-> t" == "(s,a,t):trans_of A"
+ "reachable A s" == "s:reachable A"
+ "act A" == "actions (asig_of A)"
+ "ext A" == "externals (asig_of A)"
+ "int A" == "internals (asig_of A)"
+ "inp A" == "inputs (asig_of A)"
+ "out A" == "outputs (asig_of A)"
+
+
+defs
+
+(* --------------------------------- IOA ---------------------------------*)
+
+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))"
+
+
+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)) &
+ (~ starts_of(ioa) = {}) &
+ state_trans (asig_of ioa) (trans_of ioa))"
+
+
+invariant_def "invariant A P == (!s. reachable A s --> P(s))"
+
+
+(* ------------------------- parallel composition --------------------------*)
+
+compat_asigs_def
+ "compat_asigs a1 a2 ==
+ (((outputs(a1) Int outputs(a2)) = {}) &
+ ((internals(a1) Int actions(a2)) = {}) &
+ ((internals(a2) Int actions(a1)) = {}))"
+
+
+compat_ioas_def
+ "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
+
+
+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))))"
+
+
+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:act ioa1 | a:act ioa2) &
+ (if a:act ioa1 then
+ (fst(s),a,fst(t)):trans_of(ioa1)
+ else fst(t) = fst(s))
+ &
+ (if a:act ioa2 then
+ (snd(s),a,snd(t)):trans_of(ioa2)
+ else snd(t) = snd(s))})"
+
+(* ------------------------ hiding -------------------------------------------- *)
+
+restrict_asig_def
+ "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))"
+
+(* ------------------------- renaming ------------------------------------------- *)
+
+rename_def
+"rename ioa ren ==
+ (({b. ? x. Some(x)= ren(b) & x : inp ioa},
+ {b. ? x. Some(x)= ren(b) & x : out ioa},
+ {b. ? x. Some(x)= ren(b) & x : int 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
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,262 @@
+(* Title: HOLCF/IOA/meta_theory/CompoExecs.ML
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Compositionality on Execution level.
+*)
+
+Delsimps (ex_simps @ all_simps);
+Delsimps [split_paired_All];
+
+(* ----------------------------------------------------------------------------------- *)
+
+
+section "recursive equations of operators";
+
+
+(* ---------------------------------------------------------------- *)
+(* ProjA2 *)
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "ProjA2`UU = UU";
+by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
+qed"ProjA2_UU";
+
+goal thy "ProjA2`nil = nil";
+by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
+qed"ProjA2_nil";
+
+goal thy "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs";
+by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
+qed"ProjA2_cons";
+
+
+(* ---------------------------------------------------------------- *)
+(* ProjB2 *)
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "ProjB2`UU = UU";
+by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
+qed"ProjB2_UU";
+
+goal thy "ProjB2`nil = nil";
+by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
+qed"ProjB2_nil";
+
+goal thy "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs";
+by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
+qed"ProjB2_cons";
+
+
+
+(* ---------------------------------------------------------------- *)
+(* Filter_ex2 *)
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "Filter_ex2 A`UU=UU";
+by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
+qed"Filter_ex2_UU";
+
+goal thy "Filter_ex2 A`nil=nil";
+by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
+qed"Filter_ex2_nil";
+
+goal thy "Filter_ex2 A`(at >> xs) = \
+\ (if (fst at:act A) \
+\ then at >> (Filter_ex2 A`xs) \
+\ else Filter_ex2 A`xs)";
+
+by (asm_full_simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
+qed"Filter_ex2_cons";
+
+
+(* ---------------------------------------------------------------- *)
+(* stutter2 *)
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "stutter2 A = (LAM ex. (%s. case ex of \
+\ nil => TT \
+\ | x##xs => (flift1 \
+\ (%p.(If Def ((fst p)~:act A) \
+\ then Def (s=(snd p)) \
+\ else TT fi) \
+\ andalso (stutter2 A`xs) (snd p)) \
+\ `x) \
+\ ))";
+by (rtac trans 1);
+br fix_eq2 1;
+br stutter2_def 1;
+br beta_cfun 1;
+by (simp_tac (!simpset addsimps [flift1_def]) 1);
+qed"stutter2_unfold";
+
+goal thy "(stutter2 A`UU) s=UU";
+by (stac stutter2_unfold 1);
+by (Simp_tac 1);
+qed"stutter2_UU";
+
+goal thy "(stutter2 A`nil) s = TT";
+by (stac stutter2_unfold 1);
+by (Simp_tac 1);
+qed"stutter2_nil";
+
+goal thy "(stutter2 A`(at>>xs)) s = \
+\ ((if (fst at)~:act A then Def (s=snd at) else TT) \
+\ andalso (stutter2 A`xs) (snd at))";
+br trans 1;
+by (stac stutter2_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1);
+by (Simp_tac 1);
+qed"stutter2_cons";
+
+
+Addsimps [stutter2_UU,stutter2_nil,stutter2_cons];
+
+
+(* ---------------------------------------------------------------- *)
+(* stutter *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "stutter A (s, UU)";
+by (simp_tac (!simpset addsimps [stutter_def]) 1);
+qed"stutter_UU";
+
+goal thy "stutter A (s, nil)";
+by (simp_tac (!simpset addsimps [stutter_def]) 1);
+qed"stutter_nil";
+
+goal thy "stutter A (s, (a,t)>>ex) = \
+\ ((a~:act A --> (s=t)) & stutter A (t,ex))";
+by (simp_tac (!simpset addsimps [stutter_def]
+ setloop (split_tac [expand_if]) ) 1);
+qed"stutter_cons";
+
+(* ----------------------------------------------------------------------------------- *)
+
+Delsimps [stutter2_UU,stutter2_nil,stutter2_cons];
+
+val compoex_simps = [ProjA2_UU,ProjA2_nil,ProjA2_cons,
+ ProjB2_UU,ProjB2_nil,ProjB2_cons,
+ Filter_ex2_UU,Filter_ex2_nil,Filter_ex2_cons,
+ stutter_UU,stutter_nil,stutter_cons];
+
+Addsimps compoex_simps;
+
+
+
+(* ------------------------------------------------------------------ *)
+(* The following lemmata aim for *)
+(* COMPOSITIONALITY on EXECUTION Level *)
+(* ------------------------------------------------------------------ *)
+
+
+(* --------------------------------------------------------------------- *)
+(* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *)
+(* --------------------------------------------------------------------- *)
+
+goal thy "!s. is_execution_fragment (A||B) (s,xs) \
+\ --> is_execution_fragment A (fst s, Filter_ex2 A`(ProjA2`xs)) &\
+\ is_execution_fragment B (snd s, Filter_ex2 B`(ProjB2`xs))";
+
+by (pair_induct_tac "xs" [is_execution_fragment_def] 1);
+(* main case *)
+ren "ss a t" 1;
+by (safe_tac set_cs);
+by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2
+ setloop (split_tac [expand_if])) 1));
+qed"lemma_1_1a";
+
+
+(* --------------------------------------------------------------------- *)
+(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *)
+(* --------------------------------------------------------------------- *)
+
+goal thy "!s. is_execution_fragment (A||B) (s,xs) \
+\ --> stutter A (fst s,ProjA2`xs) &\
+\ stutter B (snd s,ProjB2`xs)";
+
+by (pair_induct_tac "xs" [stutter_def,is_execution_fragment_def] 1);
+(* main case *)
+by (safe_tac set_cs);
+by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2
+ setloop (split_tac [expand_if])) 1));
+qed"lemma_1_1b";
+
+
+(* --------------------------------------------------------------------- *)
+(* Lemma_1_1c : Executions of A||B have only A- or B-actions *)
+(* --------------------------------------------------------------------- *)
+
+goal thy "!s. (is_execution_fragment (A||B) (s,xs) \
+\ --> Forall (%x.fst x:act (A||B)) xs)";
+
+by (pair_induct_tac "xs" [Forall_def,sforall_def,is_execution_fragment_def] 1);
+(* main case *)
+by (safe_tac set_cs);
+by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @
+ [actions_asig_comp,asig_of_par]) 1));
+qed"lemma_1_1c";
+
+
+(* ----------------------------------------------------------------------- *)
+(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *)
+(* ----------------------------------------------------------------------- *)
+
+goal thy
+"!s. is_execution_fragment A (fst s,Filter_ex2 A`(ProjA2`xs)) &\
+\ is_execution_fragment B (snd s,Filter_ex2 B`(ProjB2`xs)) &\
+\ stutter A (fst s,(ProjA2`xs)) & \
+\ stutter B (snd s,(ProjB2`xs)) & \
+\ Forall (%x.fst x:act (A||B)) xs \
+\ --> is_execution_fragment (A||B) (s,xs)";
+
+by (pair_induct_tac "xs" [Forall_def,sforall_def,
+ is_execution_fragment_def, stutter_def] 1);
+(* main case *)
+by (rtac allI 1);
+ren "ss a t s" 1;
+by (asm_full_simp_tac (!simpset addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]
+ setloop (split_tac [expand_if])) 1);
+by (safe_tac set_cs);
+(* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *)
+by (rotate_tac ~4 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (rotate_tac ~4 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+qed"lemma_1_2";
+
+
+(* ------------------------------------------------------------------ *)
+(* COMPOSITIONALITY on EXECUTION Level *)
+(* Main Theorem *)
+(* ------------------------------------------------------------------ *)
+
+
+goal thy
+"ex:executions(A||B) =\
+\(Filter_ex A (ProjA ex) : executions A &\
+\ Filter_ex B (ProjB ex) : executions B &\
+\ stutter A (ProjA ex) & stutter B (ProjB ex) &\
+\ Forall (%x.fst x:act (A||B)) (snd ex))";
+
+by (simp_tac (!simpset addsimps [executions_def,ProjB_def,
+ Filter_ex_def,ProjA_def,starts_of_par]) 1);
+by (pair_tac "ex" 1);
+by (rtac iffI 1);
+(* ==> *)
+by (REPEAT (etac conjE 1));
+by (asm_full_simp_tac (!simpset addsimps [lemma_1_1a RS spec RS mp,
+ lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1);
+(* <== *)
+by (REPEAT (etac conjE 1));
+by (asm_full_simp_tac (!simpset addsimps [lemma_1_2 RS spec RS mp]) 1);
+qed"compositionality_ex";
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,65 @@
+(* Title: HOLCF/IOA/meta_theory/CompoExecs.thy
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Compositionality on Execution level.
+*)
+
+CompoExecs = Traces +
+
+
+consts
+
+ ProjA ::"('a,'s * 't)execution => ('a,'s)execution"
+ ProjA2 ::"('a,'s * 't)pairs -> ('a,'s)pairs"
+ ProjB ::"('a,'s * 't)execution => ('a,'t)execution"
+ ProjB2 ::"('a,'s * 't)pairs -> ('a,'t)pairs"
+ Filter_ex ::"('a,'s)ioa => ('a,'s)execution => ('a,'s)execution"
+ Filter_ex2 ::"('a,'s)ioa => ('a,'s)pairs -> ('a,'s)pairs"
+ stutter ::"('a,'s)ioa => ('a,'s)execution => bool"
+ stutter2 ::"('a,'s)ioa => ('a,'s)pairs -> ('s => tr)"
+
+
+defs
+
+
+ProjA_def
+ "ProjA ex == (fst (fst ex), ProjA2`(snd ex))"
+
+ProjB_def
+ "ProjB ex == (snd (fst ex), ProjB2`(snd ex))"
+
+
+ProjA2_def
+ "ProjA2 == Map (%x.(fst x,fst(snd x)))"
+
+ProjB2_def
+ "ProjB2 == Map (%x.(fst x,snd(snd x)))"
+
+
+Filter_ex_def
+ "Filter_ex A ex == (fst ex,Filter_ex2 A`(snd ex))"
+
+
+Filter_ex2_def
+ "Filter_ex2 A == Filter (%x.fst x:act A)"
+
+stutter_def
+ "stutter A ex == ((stutter2 A`(snd ex)) (fst ex) ~= FF)"
+
+stutter2_def
+ "stutter2 A ==(fix`(LAM h ex. (%s. case ex of
+ nil => TT
+ | x##xs => (flift1
+ (%p.(If Def ((fst p)~:act A)
+ then Def (s=(snd p))
+ else TT fi)
+ andalso (h`xs) (snd p))
+ `x)
+ )))"
+
+
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,503 @@
+(* Title: HOLCF/IOA/meta_theory/CompoScheds.ML
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Compositionality on Schedule level.
+*)
+
+
+
+Addsimps [surjective_pairing RS sym];
+
+
+
+(* ------------------------------------------------------------------------------- *)
+
+section "mkex rewrite rules";
+
+(* ---------------------------------------------------------------- *)
+(* mkex2 *)
+(* ---------------------------------------------------------------- *)
+
+
+bind_thm ("mkex2_unfold", fix_prover2 thy mkex2_def
+"mkex2 A B = (LAM sch exA exB. (%s t. case sch of \
+\ nil => nil \
+\ | x##xs => \
+\ (case x of \
+\ Undef => UU \
+\ | Def y => \
+\ (if y:act A then \
+\ (if y:act B then \
+\ (case HD`exA of \
+\ Undef => UU \
+\ | Def a => (case HD`exB of \
+\ Undef => UU \
+\ | Def b => \
+\ (y,(snd a,snd b))>> \
+\ (mkex2 A B`xs`(TL`exA)`(TL`exB)) (snd a) (snd b))) \
+\ else \
+\ (case HD`exA of \
+\ Undef => UU \
+\ | Def a => \
+\ (y,(snd a,t))>>(mkex2 A B`xs`(TL`exA)`exB) (snd a) t) \
+\ ) \
+\ else \
+\ (if y:act B then \
+\ (case HD`exB of \
+\ Undef => UU \
+\ | Def b => \
+\ (y,(s,snd b))>>(mkex2 A B`xs`exA`(TL`exB)) s (snd b)) \
+\ else \
+\ UU \
+\ ) \
+\ ) \
+\ )))");
+
+
+goal thy "(mkex2 A B`UU`exA`exB) s t = UU";
+by (stac mkex2_unfold 1);
+by (Simp_tac 1);
+qed"mkex2_UU";
+
+goal thy "(mkex2 A B`nil`exA`exB) s t= nil";
+by (stac mkex2_unfold 1);
+by (Simp_tac 1);
+qed"mkex2_nil";
+
+goal thy "!!x.[| x:act A; x~:act B; HD`exA=Def a|] \
+\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
+\ (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
+br trans 1;
+by (stac mkex2_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"mkex2_cons_1";
+
+goal thy "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
+\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
+\ (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
+br trans 1;
+by (stac mkex2_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"mkex2_cons_2";
+
+goal thy "!!x.[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
+\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
+\ (x,snd a,snd b) >> \
+\ (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
+br trans 1;
+by (stac mkex2_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"mkex2_cons_3";
+
+Addsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
+
+
+(* ---------------------------------------------------------------- *)
+(* mkex *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "mkex A B UU (s,exA) (t,exB) = ((s,t),UU)";
+by (simp_tac (!simpset addsimps [mkex_def]) 1);
+qed"mkex_UU";
+
+goal thy "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)";
+by (simp_tac (!simpset addsimps [mkex_def]) 1);
+qed"mkex_nil";
+
+goal thy "!!x.[| x:act A; x~:act B |] \
+\ ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) = \
+\ ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))";
+by (simp_tac (!simpset addsimps [mkex_def]
+ setloop (split_tac [expand_if]) ) 1);
+by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
+auto();
+qed"mkex_cons_1";
+
+goal thy "!!x.[| x~:act A; x:act B |] \
+\ ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = \
+\ ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
+by (simp_tac (!simpset addsimps [mkex_def]
+ setloop (split_tac [expand_if]) ) 1);
+by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
+auto();
+qed"mkex_cons_2";
+
+goal thy "!!x.[| x:act A; x:act B |] \
+\ ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
+\ ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
+by (simp_tac (!simpset addsimps [mkex_def]
+ setloop (split_tac [expand_if]) ) 1);
+by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
+auto();
+qed"mkex_cons_3";
+
+Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
+
+val composch_simps = [mkex_UU,mkex_nil,
+ mkex_cons_1,mkex_cons_2,mkex_cons_3];
+
+Addsimps composch_simps;
+
+
+
+(* ------------------------------------------------------------------ *)
+(* The following lemmata aim for *)
+(* COMPOSITIONALITY on SCHEDULE Level *)
+(* ------------------------------------------------------------------ *)
+
+(* ---------------------------------------------------------------------- *)
+ section "Lemmas for ==>";
+(* ----------------------------------------------------------------------*)
+
+(* --------------------------------------------------------------------- *)
+(* Lemma_2_1 : tfilter(ex) and filter_act are commutative *)
+(* --------------------------------------------------------------------- *)
+
+goalw thy [filter_act_def,Filter_ex2_def]
+ "filter_act`(Filter_ex2 A`xs)=\
+\ Filter (%a.a:act A)`(filter_act`xs)";
+
+by (simp_tac (!simpset addsimps [MapFilter,o_def]) 1);
+qed"lemma_2_1a";
+
+
+(* --------------------------------------------------------------------- *)
+(* Lemma_2_2 : State-projections do not affect filter_act *)
+(* --------------------------------------------------------------------- *)
+
+goal thy
+ "filter_act`(ProjA2`xs) =filter_act`xs &\
+\ filter_act`(ProjB2`xs) =filter_act`xs";
+
+by (pair_induct_tac "xs" [] 1);
+qed"lemma_2_1b";
+
+
+(* --------------------------------------------------------------------- *)
+(* Schedules of A||B have only A- or B-actions *)
+(* --------------------------------------------------------------------- *)
+
+(* FIX: very similar to lemma_1_1c, but it is not checking if every action element of
+ an ex is in A or B, but after projecting it onto the action schedule. Of course, this
+ is the same proposition, but we cannot change this one, when then rather lemma_1_1c *)
+
+goal thy "!s. is_execution_fragment (A||B) (s,xs) \
+\ --> Forall (%x.x:act (A||B)) (filter_act`xs)";
+
+by (pair_induct_tac "xs" [is_execution_fragment_def,Forall_def,sforall_def] 1);
+(* main case *)
+by (safe_tac set_cs);
+by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @
+ [actions_asig_comp,asig_of_par]) 1));
+qed"sch_actions_in_AorB";
+
+
+(* --------------------------------------------------------------------------*)
+ section "Lemmas for <==";
+(* ---------------------------------------------------------------------------*)
+
+(*---------------------------------------------------------------------------
+ Filtering actions out of mkex(sch,exA,exB) yields the oracle sch
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+goal thy "! exA exB s t. \
+\ Forall (%x.x:act (A||B)) sch & \
+\ Filter (%a.a:act A)`sch << filter_act`exA &\
+\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch";
+
+by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1);
+
+(* main case *)
+(* splitting into 4 cases according to a:A, a:B *)
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (safe_tac set_cs);
+
+(* Case y:A, y:B *)
+by (Seq_case_simp_tac "exA" 1);
+(* Case exA=UU, Case exA=nil*)
+(* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA
+ is used! --> to generate a contradiction using ~a>>ss<< UU(nil), using theorems
+ Cons_not_less_UU and Cons_not_less_nil *)
+by (Seq_case_simp_tac "exB" 1);
+(* Case exA=a>>x, exB=b>>y *)
+(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case,
+ as otherwise mkex_cons_3 would not be rewritten without use of rotate_tac: then tactic
+ would not be generally applicable *)
+by (Asm_full_simp_tac 1);
+
+(* Case y:A, y~:B *)
+by (Seq_case_simp_tac "exB" 1);
+by (Asm_full_simp_tac 1);
+
+(* Case y~:A, y:B *)
+by (Seq_case_simp_tac "exA" 1);
+by (Asm_full_simp_tac 1);
+
+(* Case y~:A, y~:B *)
+by (asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp]) 1);
+qed"Mapfst_mkex_is_sch";
+
+
+(* generalizing the proof above to a tactic *)
+
+fun mkex_induct_tac sch exA exB =
+ EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def],
+ asm_full_simp_tac (!simpset setloop split_tac [expand_if]),
+ SELECT_GOAL (safe_tac set_cs),
+ Seq_case_simp_tac exA,
+ Seq_case_simp_tac exB,
+ Asm_full_simp_tac,
+ Seq_case_simp_tac exB,
+ Asm_full_simp_tac,
+ Seq_case_simp_tac exA,
+ Asm_full_simp_tac,
+ asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp])
+ ];
+
+
+
+(*---------------------------------------------------------------------------
+ Projection of mkex(sch,exA,exB) onto A stutters on A
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+
+goal thy "! exA exB s t. \
+\ Forall (%x.x:act (A||B)) sch & \
+\ Filter (%a.a:act A)`sch << filter_act`exA &\
+\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ --> stutter A (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
+
+by (mkex_induct_tac "sch" "exA" "exB");
+
+qed"stutterA_mkex";
+
+
+goal thy "!! sch.[| \
+\ Forall (%x.x:act (A||B)) sch ; \
+\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
+\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
+\ ==> stutter A (ProjA (mkex A B sch exA exB))";
+
+by (cut_facts_tac [stutterA_mkex] 1);
+by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1);
+by (REPEAT (etac allE 1));
+bd mp 1;
+ba 2;
+by (Asm_full_simp_tac 1);
+qed"stutter_mkex_on_A";
+
+
+(*---------------------------------------------------------------------------
+ Projection of mkex(sch,exA,exB) onto B stutters on B
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+goal thy "! exA exB s t. \
+\ Forall (%x.x:act (A||B)) sch & \
+\ Filter (%a.a:act A)`sch << filter_act`exA &\
+\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ --> stutter B (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
+
+by (mkex_induct_tac "sch" "exA" "exB");
+
+qed"stutterB_mkex";
+
+
+goal thy "!! sch.[| \
+\ Forall (%x.x:act (A||B)) sch ; \
+\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
+\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
+\ ==> stutter B (ProjB (mkex A B sch exA exB))";
+
+by (cut_facts_tac [stutterB_mkex] 1);
+by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1);
+by (REPEAT (etac allE 1));
+bd mp 1;
+ba 2;
+by (Asm_full_simp_tac 1);
+qed"stutter_mkex_on_B";
+
+
+(*---------------------------------------------------------------------------
+ Filter of mkex(sch,exA,exB) to A after projection onto A is exA
+ -- using zip`(proj1`exA)`(proj2`exA) instead of exA --
+ -- because of admissibility problems --
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+goal thy "! exA exB s t. \
+\ Forall (%x.x:act (A||B)) sch & \
+\ Filter (%a.a:act A)`sch << filter_act`exA &\
+\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ --> Filter_ex2 A`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) = \
+\ Zip`(Filter (%a.a:act A)`sch)`(Map snd`exA)";
+
+by (mkex_induct_tac "sch" "exA" "exB");
+
+qed"filter_mkex_is_exA_tmp";
+
+(*---------------------------------------------------------------------------
+ zip`(proj1`y)`(proj2`y) = y (using the lift operations)
+ lemma for admissibility problems
+ --------------------------------------------------------------------------- *)
+
+goal thy "Zip`(Map fst`y)`(Map snd`y) = y";
+by (Seq_induct_tac "y" [] 1);
+qed"Zip_Map_fst_snd";
+
+
+(*---------------------------------------------------------------------------
+ filter A`sch = proj1`ex --> zip`(filter A`sch)`(proj2`ex) = ex
+ lemma for eliminating non admissible equations in assumptions
+ --------------------------------------------------------------------------- *)
+
+goal thy "!! sch ex. \
+\ Filter (%a.a:act AB)`sch = filter_act`ex \
+\ ==> ex = Zip`(Filter (%a.a:act AB)`sch)`(Map snd`ex)";
+by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (rtac (Zip_Map_fst_snd RS sym) 1);
+qed"trick_against_eq_in_ass";
+
+(*---------------------------------------------------------------------------
+ Filter of mkex(sch,exA,exB) to A after projection onto A is exA
+ using the above trick
+ --------------------------------------------------------------------------- *)
+
+
+goal thy "!!sch exA exB.\
+\ [| Forall (%a.a:act (A||B)) sch ; \
+\ Filter (%a.a:act A)`sch = filter_act`(snd exA) ;\
+\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
+\ ==> Filter_ex A (ProjA (mkex A B sch exA exB)) = exA";
+by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
+by (pair_tac "exA" 1);
+by (pair_tac "exB" 1);
+br conjI 1;
+by (simp_tac (!simpset addsimps [mkex_def]) 1);
+by (stac trick_against_eq_in_ass 1);
+back();
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exA_tmp]) 1);
+qed"filter_mkex_is_exA";
+
+
+(*---------------------------------------------------------------------------
+ Filter of mkex(sch,exA,exB) to B after projection onto B is exB
+ -- using zip`(proj1`exB)`(proj2`exB) instead of exB --
+ -- because of admissibility problems --
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+
+goal thy "! exA exB s t. \
+\ Forall (%x.x:act (A||B)) sch & \
+\ Filter (%a.a:act A)`sch << filter_act`exA &\
+\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ --> Filter_ex2 B`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) = \
+\ Zip`(Filter (%a.a:act B)`sch)`(Map snd`exB)";
+
+(* notice necessary change of arguments exA and exB *)
+by (mkex_induct_tac "sch" "exB" "exA");
+
+qed"filter_mkex_is_exB_tmp";
+
+
+(*---------------------------------------------------------------------------
+ Filter of mkex(sch,exA,exB) to A after projection onto B is exB
+ using the above trick
+ --------------------------------------------------------------------------- *)
+
+
+goal thy "!!sch exA exB.\
+\ [| Forall (%a.a:act (A||B)) sch ; \
+\ Filter (%a.a:act A)`sch = filter_act`(snd exA) ;\
+\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
+\ ==> Filter_ex B (ProjB (mkex A B sch exA exB)) = exB";
+by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
+by (pair_tac "exA" 1);
+by (pair_tac "exB" 1);
+br conjI 1;
+by (simp_tac (!simpset addsimps [mkex_def]) 1);
+by (stac trick_against_eq_in_ass 1);
+back();
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exB_tmp]) 1);
+qed"filter_mkex_is_exB";
+
+(* --------------------------------------------------------------------- *)
+(* mkex has only A- or B-actions *)
+(* --------------------------------------------------------------------- *)
+
+
+goal thy "!s t exA exB. \
+\ Forall (%x. x : act (A || B)) sch &\
+\ Filter (%a.a:act A)`sch << filter_act`exA &\
+\ Filter (%a.a:act B)`sch << filter_act`exB \
+\ --> Forall (%x.fst x : act (A ||B)) \
+\ (snd (mkex A B sch (s,exA) (t,exB)))";
+
+by (mkex_induct_tac "sch" "exA" "exB");
+
+qed"mkex_actions_in_AorB";
+
+
+(* ------------------------------------------------------------------ *)
+(* COMPOSITIONALITY on SCHEDULE Level *)
+(* Main Theorem *)
+(* ------------------------------------------------------------------ *)
+
+goal thy
+"sch : schedules (A||B) = \
+\ (Filter (%a.a:act A)`sch : schedules A &\
+\ Filter (%a.a:act B)`sch : schedules B &\
+\ Forall (%x. x:act (A||B)) sch)";
+
+by (simp_tac (!simpset addsimps [schedules_def, has_schedule_def]) 1);
+by (safe_tac set_cs);
+(* ==> *)
+by (res_inst_tac [("x","Filter_ex A (ProjA ex)")] bexI 1);
+by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
+by (simp_tac (!simpset addsimps [Filter_ex_def,ProjA_def,
+ lemma_2_1a,lemma_2_1b]) 1);
+by (res_inst_tac [("x","Filter_ex B (ProjB ex)")] bexI 1);
+by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
+by (simp_tac (!simpset addsimps [Filter_ex_def,ProjB_def,
+ lemma_2_1a,lemma_2_1b]) 1);
+by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (pair_tac "ex" 1);
+be conjE 1;
+by (asm_full_simp_tac (!simpset addsimps [sch_actions_in_AorB]) 1);
+
+(* <== *)
+
+(* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
+ we need here *)
+ren "exA exB" 1;
+by (res_inst_tac [("x","mkex A B sch exA exB")] bexI 1);
+(* mkex actions are just the oracle *)
+by (pair_tac "exA" 1);
+by (pair_tac "exB" 1);
+by (asm_full_simp_tac (!simpset addsimps [Mapfst_mkex_is_sch]) 1);
+
+(* mkex is an execution -- use compositionality on ex-level *)
+by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 1);
+by (asm_full_simp_tac (!simpset addsimps
+ [stutter_mkex_on_A, stutter_mkex_on_B,
+ filter_mkex_is_exB,filter_mkex_is_exA]) 1);
+by (pair_tac "exA" 1);
+by (pair_tac "exB" 1);
+by (asm_full_simp_tac (!simpset addsimps [mkex_actions_in_AorB]) 1);
+qed"compositionality_sch";
+
+
+
+Delsimps compoex_simps;
+Delsimps composch_simps;
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,63 @@
+(* Title: HOLCF/IOA/meta_theory/CompoScheds.thy
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Compositionality on Schedule level.
+*)
+
+CompoScheds = CompoExecs +
+
+
+
+consts
+
+ mkex ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
+ ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution"
+ mkex2 ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
+ ('a,'s)pairs -> ('a,'t)pairs ->
+ ('s => 't => ('a,'s*'t)pairs)"
+
+
+defs
+
+mkex_def
+ "mkex A B sch exA exB ==
+ ((fst exA,fst exB),
+ (mkex2 A B`sch`(snd exA)`(snd exB)) (fst exA) (fst exB))"
+
+mkex2_def
+ "mkex2 A B == (fix`(LAM h sch exA exB. (%s t. case sch of
+ nil => nil
+ | x##xs =>
+ (case x of
+ Undef => UU
+ | Def y =>
+ (if y:act A then
+ (if y:act B then
+ (case HD`exA of
+ Undef => UU
+ | Def a => (case HD`exB of
+ Undef => UU
+ | Def b =>
+ (y,(snd a,snd b))>>
+ (h`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))
+ else
+ (case HD`exA of
+ Undef => UU
+ | Def a =>
+ (y,(snd a,t))>>(h`xs`(TL`exA)`exB) (snd a) t)
+ )
+ else
+ (if y:act B then
+ (case HD`exB of
+ Undef => UU
+ | Def b =>
+ (y,(s,snd b))>>(h`xs`exA`(TL`exB)) s (snd b))
+ else
+ UU
+ )
+ )
+ ))))"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,734 @@
+(* Title: HOLCF/IOA/meta_theory/CompoTraces.ML
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Compositionality on Trace level.
+*)
+
+(* FIX:Proof and add in Sequence.ML *)
+Addsimps [Finite_Conc];
+
+
+(*
+Addsimps [forall_cons];
+
+Addsimps [(* LastActExtsmall1, LastActExtsmall2, looping !! *) ext_and_act];
+*)
+
+fun thin_tac' j =
+ rotate_tac (j - 1) THEN'
+ etac thin_rl THEN'
+ rotate_tac (~ (j - 1));
+
+
+
+(* ---------------------------------------------------------------- *)
+ section "mksch rewrite rules";
+(* ---------------------------------------------------------------- *)
+
+
+
+
+bind_thm ("mksch_unfold", fix_prover2 thy mksch_def
+"mksch A B = (LAM tr schA schB. case tr of \
+\ nil => nil\
+\ | x##xs => \
+\ (case x of \
+\ Undef => UU \
+\ | Def y => \
+\ (if y:act A then \
+\ (if y:act B then \
+\ ((Takewhile (%a.a:int A)`schA) \
+\ @@(Takewhile (%a.a:int B)`schB) \
+\ @@(y>>(mksch A B`xs \
+\ `(TL`(Dropwhile (%a.a:int A)`schA)) \
+\ `(TL`(Dropwhile (%a.a:int B)`schB)) \
+\ ))) \
+\ else \
+\ ((Takewhile (%a.a:int A)`schA) \
+\ @@ (y>>(mksch A B`xs \
+\ `(TL`(Dropwhile (%a.a:int A)`schA)) \
+\ `schB))) \
+\ ) \
+\ else \
+\ (if y:act B then \
+\ ((Takewhile (%a.a:int B)`schB) \
+\ @@ (y>>(mksch A B`xs \
+\ `schA \
+\ `(TL`(Dropwhile (%a.a:int B)`schB)) \
+\ ))) \
+\ else \
+\ UU \
+\ ) \
+\ ) \
+\ ))");
+
+
+goal thy "mksch A B`UU`schA`schB = UU";
+by (stac mksch_unfold 1);
+by (Simp_tac 1);
+qed"mksch_UU";
+
+goal thy "mksch A B`nil`schA`schB = nil";
+by (stac mksch_unfold 1);
+by (Simp_tac 1);
+qed"mksch_nil";
+
+goal thy "!!x.[|x:act A;x~:act B|] \
+\ ==> mksch A B`(x>>tr)`schA`schB = \
+\ (Takewhile (%a.a:int A)`schA) \
+\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
+\ `schB))";
+br trans 1;
+by (stac mksch_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"mksch_cons1";
+
+goal thy "!!x.[|x~:act A;x:act B|] \
+\ ==> mksch A B`(x>>tr)`schA`schB = \
+\ (Takewhile (%a.a:int B)`schB) \
+\ @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a.a:int B)`schB)) \
+\ ))";
+br trans 1;
+by (stac mksch_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"mksch_cons2";
+
+goal thy "!!x.[|x:act A;x:act B|] \
+\ ==> mksch A B`(x>>tr)`schA`schB = \
+\ (Takewhile (%a.a:int A)`schA) \
+\ @@ ((Takewhile (%a.a:int B)`schB) \
+\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
+\ `(TL`(Dropwhile (%a.a:int B)`schB)))) \
+\ )";
+br trans 1;
+by (stac mksch_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"mksch_cons3";
+
+val compotr_simps =[mksch_UU,mksch_nil, mksch_cons1,mksch_cons2,mksch_cons3];
+
+Addsimps compotr_simps;
+
+
+(* ------------------------------------------------------------------ *)
+(* The following lemmata aim for *)
+(* COMPOSITIONALITY on TRACE Level *)
+(* ------------------------------------------------------------------ *)
+
+
+(* ---------------------------------------------------------------------------- *)
+(* Specifics for "==>" *)
+(* ---------------------------------------------------------------------------- *)
+
+(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of
+ the compatibility of IOA, in particular out of the condition that internals are
+ really hidden. *)
+
+goal thy "(eB & ~eA --> ~A) --> \
+\ (A & (eA | eB)) = (eA & A)";
+by (Fast_tac 1);
+qed"compatibility_consequence1";
+
+
+(* very similar to above, only the commutativity of | is used to make a slight change *)
+
+goal thy "(eB & ~eA --> ~A) --> \
+\ (A & (eB | eA)) = (eA & A)";
+by (Fast_tac 1);
+qed"compatibility_consequence2";
+
+
+goal thy "!!x. [| x = nil; y = z|] ==> (x @@ y) = z";
+auto();
+qed"nil_and_tconc";
+
+(* FIX: should be easy to get out of lemma before *)
+goal thy "!!x. [| x = nil; f`y = f`z|] ==> f`(x @@ y) = f`z";
+auto();
+qed"nil_and_tconc_f";
+
+(* FIX: should be something like subst: or better improve simp_tac so that these lemmat are
+ superfluid *)
+goal thy "!!x. [| x1 = x2; f`(x2 @@ y) = f`z|] ==> f`(x1 @@ y) = f`z";
+auto();
+qed"tconcf";
+
+
+
+(*
+
+
+(* -------------------------------------------------------------------------------- *)
+
+
+goal thy "!!A B. compat_ioas A B ==> \
+\ ! schA schB. Forall (%x. x:act (A||B)) tr \
+\ --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)";
+by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
+by (safe_tac set_cs);
+by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 1);
+by (case_tac "a:act A" 1);
+by (case_tac "a:act B" 1);
+(* a:A, a:B *)
+by (Asm_full_simp_tac 1);
+br (Forall_Conc_impl RS mp) 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+br (Forall_Conc_impl RS mp) 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+(* a:A,a~:B *)
+by (Asm_full_simp_tac 1);
+br (Forall_Conc_impl RS mp) 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (case_tac "a:act B" 1);
+(* a~:A, a:B *)
+by (Asm_full_simp_tac 1);
+br (Forall_Conc_impl RS mp) 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+(* a~:A,a~:B *)
+auto();
+qed"ForallAorB_mksch";
+
+
+goal thy "!!A B. compat_ioas A B ==> \
+\ ! schA schB. (Forall (%x. x:act B & x~:act A) tr \
+\ --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))";
+
+by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
+by (safe_tac set_cs);
+br (Forall_Conc_impl RS mp) 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+qed"ForallBnA_mksch";
+
+goal thy "!!A B. compat_ioas B A ==> \
+\ ! schA schB. (Forall (%x. x:act A & x~:act B) tr \
+\ --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))";
+
+by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
+by (safe_tac set_cs);
+by (Asm_full_simp_tac 1);
+br (Forall_Conc_impl RS mp) 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+qed"ForallAnB_mksch";
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+(*
+goal thy "!! tr. Finite tr ==> \
+\ ! x y. Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
+\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
+\ Forall (%x. x:ext (A||B)) tr \
+\ --> Finite (mksch A B`tr`x`y)";
+
+be Seq_Finite_ind 1;
+by (Asm_full_simp_tac 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (safe_tac set_cs);
+by (Asm_full_simp_tac 1);
+
+
+
+qed"FiniteL_mksch";
+
+goal thy " !!bs. Finite bs ==> \
+\ Forall (%x. x:act B & x~:act A) bs &\
+\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
+\ --> (? y1 y2. (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
+\ Forall (%x. x:act B & x~:act A) y1 & \
+\ Finite y1 & y = (y1 @@ y2) & \
+\ Filter (%a. a:ext B)`y1 = bs)";
+be Seq_Finite_ind 1;
+by (rtac impI 1);
+by (res_inst_tac [("x","nil")] exI 1);
+by (res_inst_tac [("x","y")] exI 1);
+by (Asm_full_simp_tac 1);
+(* main case *)
+by (rtac impI 1);
+by (Asm_full_simp_tac 1);
+by (REPEAT (etac conjE 1));
+
+
+
+
+
+qed"reduce_mksch";
+
+*)
+
+
+(* Lemma for substitution of looping assumption in another specific assumption *)
+val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
+by (cut_facts_tac [p1] 1);
+be (p2 RS subst) 1;
+qed"subst_lemma1";
+
+
+
+
+
+(*---------------------------------------------------------------------------
+ Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr
+ structural induction
+ --------------------------------------------------------------------------- *)
+
+goal thy "! schA schB. compat_ioas A B & compat_ioas B A &\
+\ is_asig(asig_of A) & is_asig(asig_of B) &\
+\ Forall (%x.x:ext (A||B)) tr & \
+\ Filter (%a.a:act A)`tr << Filter (%a.a:ext A)`schA &\
+\ Filter (%a.a:act B)`tr << Filter (%a.a:ext B)`schB \
+\ --> Filter (%a.a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
+
+by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
+
+(* main case *)
+(* splitting into 4 cases according to a:A, a:B *)
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (safe_tac set_cs);
+
+(* Case a:A, a:B *)
+by (forward_tac [divide_Seq] 1);
+by (forward_tac [divide_Seq] 1);
+back();
+by (REPEAT (etac conjE 1));
+(* filtering internals of A is nil *)
+br nil_and_tconc 1;
+br FilterPTakewhileQnil 1;
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
+ intA_is_not_extB,int_is_not_ext]) 1);
+(* end*)
+(* filtering internals of B is nil *)
+(* FIX: should be done by simp_tac and claset combined until end*)
+br nil_and_tconc 1;
+br FilterPTakewhileQnil 1;
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
+ intA_is_not_extB,int_is_not_ext]) 1);
+(* end*)
+(* conclusion of IH ok, but assumptions of IH have to be transformed *)
+by (dres_inst_tac [("x","schA")] subst_lemma1 1);
+ba 1;
+by (dres_inst_tac [("x","schB")] subst_lemma1 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1);
+
+(* Case a:B, a~:A *)
+
+by (forward_tac [divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+(* filtering internals of A is nil *)
+(* FIX: should be done by simp_tac and claset combined until end*)
+br nil_and_tconc 1;
+br FilterPTakewhileQnil 1;
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
+ intA_is_not_extB,int_is_not_ext]) 1);
+(* end*)
+by (dres_inst_tac [("x","schB")] subst_lemma1 1);
+back();
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1);
+
+(* Case a:A, a~:B *)
+
+by (forward_tac [divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+(* filtering internals of A is nil *)
+(* FIX: should be done by simp_tac and claset combined until end*)
+br nil_and_tconc 1;
+br FilterPTakewhileQnil 1;
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
+ intA_is_not_extB,int_is_not_ext]) 1);
+(* end*)
+by (dres_inst_tac [("x","schA")] subst_lemma1 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1);
+
+(* Case a~:A, a~:B *)
+
+by (fast_tac (!claset addSIs [ext_is_act]
+ addss (!simpset addsimps [externals_of_par]) ) 1);
+qed"filterA_mksch_is_tr";
+
+
+
+
+goal thy "!!x y. [|x=UU; y=UU|] ==> x=y";
+auto();
+qed"both_UU";
+
+goal thy "!!x y. [|x=nil; y=nil|] ==> x=y";
+auto();
+qed"both_nil";
+
+
+(* FIX: does it exist already? *)
+(* To eliminate representation a##xs, if only ~=UU & ~=nil is needed *)
+goal thy "!!tr. [|tr=a##xs; a~=UU |] ==> tr~=UU & tr~=nil";
+ by (Asm_full_simp_tac 1);
+qed"yields_not_UU_or_nil";
+
+
+
+
+
+(*---------------------------------------------------------------------------
+ Filter of mksch(tr,schA,schB) to A is schA
+ take lemma
+ --------------------------------------------------------------------------- *)
+
+goal thy "compat_ioas A B & compat_ioas B A &\
+\ Forall (%x.x:ext (A||B)) tr & \
+\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
+\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ LastActExtsch schA & LastActExtsch schB \
+\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
+
+
+by (res_inst_tac [("Q","%x. x:act B & x~:act A")] take_lemma_less_induct 1);
+
+
+(*---------------------------------------------------------------------------
+ Filter of mksch(tr,schA,schB) to A is schA
+ take lemma
+ --------------------------------------------------------------------------- *)
+
+goal thy "! schA schB tr. compat_ioas A B & compat_ioas B A &\
+\ forall (plift (%x.x:externals(asig_of (A||B)))) tr & \
+\ tfilter`(plift (%a.a:externals(asig_of A)))`schA = tfilter`(plift (%a.a:actions(asig_of A)))`tr &\
+\ tfilter`(plift (%a.a:externals(asig_of B)))`schB = tfilter`(plift (%a.a:actions(asig_of B)))`tr &\
+\ LastActExtsch schA & LastActExtsch schB \
+\ --> trace_take n`(tfilter`(plift (%a.a:actions(asig_of A)))`(mksch A B`tr`schA`schB)) = trace_take n`schA";
+
+by (res_inst_tac[("n","n")] less_induct 1);
+by (REPEAT(rtac allI 1));
+br impI 1;
+by (REPEAT (etac conjE 1));
+by (res_inst_tac [("x","tr")] trace.cases 1);
+
+(* tr = UU *)
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+by (dtac LastActExtimplUU 1);
+ba 1;
+by (Asm_simp_tac 1);
+
+(* tr = nil *)
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+by (dtac LastActExtimplnil 1);
+ba 1;
+by (Asm_simp_tac 1);
+
+(* tr = t##ts *)
+
+(* just to delete tr=a##xs, as we do not make induction on a but on an element in
+ xs we find later *)
+by (dtac yields_not_UU_or_nil 1);
+ba 1;
+by (REPEAT (etac conjE 1));
+
+(* FIX: or use equality "hd(f ~P x)=UU = fa P x" to make distinction on that *)
+by (case_tac "forall (plift (%x.x:actions(asig_of B) & x~:actions(asig_of A))) tr" 1);
+(* This case holds for whole streams, not only for takes *)
+br (trace_take_lemma RS iffD2 RS spec) 1;
+
+by (case_tac "tr : tfinite" 1);
+
+(* FIX: Check if new trace lemmata with ==> instead of --> allow for simplifiaction instead
+ of ares_tac in the following *)
+br both_nil 1;
+(* mksch = nil *)
+by (REPEAT (ares_tac [forallQfilterPnil,forallBnA_mksch,finiteL_mksch] 1));
+by (Fast_tac 1);
+(* schA = nil *)
+by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
+by (Asm_simp_tac 1);
+br forallQfilterPnil 1;
+ba 1;
+back();
+ba 1;
+by (Fast_tac 1);
+
+(* case tr~:tfinite *)
+
+br both_UU 1;
+(* mksch = UU *)
+by (REPEAT (ares_tac [forallQfilterPUU,(finiteR_mksch RS mp COMP rev_contrapos),
+ forallBnA_mksch] 1));
+by (Fast_tac 1);
+(* schA = UU *)
+by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
+by (Asm_simp_tac 1);
+br forallQfilterPUU 1;
+by (REPEAT (atac 1));
+back();
+by (Fast_tac 1);
+
+(* case" ~ forall (plift (%x.x:actions(asig_of B) & x~:actions(asig_of A))) tr" *)
+
+by (dtac divide_trace3 1);
+by (REPEAT (atac 1));
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+
+(* rewrite assuption for tr *)
+by (hyp_subst_tac 1);
+(* bring in lemma reduce_mksch *)
+by (forw_inst_tac [("y","schB"),("x","schA")] reduce_mksch 1);
+ba 1;
+by (asm_simp_tac HOL_min_ss 1);
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+
+(* use reduce_mksch to rewrite conclusion *)
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac 1);
+
+(* eliminate the B-only prefix *)
+(* FIX: Cannot be done by
+ by (asm_full_simp_tac (HOL_min_ss addsimps [forallQfilterPnil]) 1);
+ as P&Q --> Q is looping. Perhaps forall (and other) operations not on predicates but on
+ sets because of this reason ?????? *)
+br nil_and_tconc_f 1;
+be forallQfilterPnil 1;
+ba 1;
+by (Fast_tac 1);
+
+(* Now real recursive step follows (in Def x) *)
+
+by (case_tac "x:actions(asig_of A)" 1);
+by (case_tac "x~:actions(asig_of B)" 1);
+by (rotate_tac ~2 1);
+by (asm_full_simp_tac (!simpset addsimps [filter_rep]) 1);
+
+(* same problem as above for the B-onlu prefix *)
+(* FIX: eliminate generated subgoal immeadiately ! (as in case below x:A & x: B *)
+by (subgoal_tac "tfilter`(plift (%a. a : actions (asig_of A) & a : externals (asig_of B)))`y1=nil" 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+(* eliminate introduced subgoal 2 *)
+be forallQfilterPnil 2;
+ba 2;
+by (Fast_tac 2);
+
+(* f A (tw iA) = tw iA *)
+by (simp_tac (HOL_min_ss addsimps [filterPtakewhileQ,int_is_act]) 1);
+
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace] 1);
+(* subst divide_trace in conlcusion, but only at the righest occurence *)
+by (res_inst_tac [("t","schA")] ssubst 1);
+back();
+back();
+back();
+ba 1;
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite] 1);
+
+by (REPEAT (etac conjE 1));
+(* reduce trace_takes from n to strictly smaller k *)
+by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext]) 1);
+br take_reduction 1;
+ba 1;
+(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
+by (rotate_tac ~10 1);
+(* assumption forall and schB *)
+by (asm_full_simp_tac (!simpset addsimps [tconc_cong,forall_cons,forall_tconc,ext_and_act]) 1);
+(* assumption schA *)
+by (dres_inst_tac [("x","schA"),
+ ("g","tfilter`(plift (%a. a : actions (asig_of A)))`rs")] lemma22 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [tfiltertconc,not_int_is_ext,tfilterPtakewhileQ]) 1);
+by (REPEAT (etac conjE 1));
+(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
+by (dres_inst_tac [("sch","schA"),("P","plift (%a. a : internals (asig_of A))")] LastActExtsmall1 1);
+by (dres_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
+ba 1;
+by (Asm_full_simp_tac 1);
+
+(* case x:actions(asig_of A) & x: actions(asig_of B) *)
+by (rotate_tac ~2 1);
+by (asm_full_simp_tac (!simpset addsimps [filter_rep]) 1);
+by (subgoal_tac "tfilter`(plift (%a. a : actions (asig_of A) & a : externals (asig_of B)))`y1=nil" 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+by (thin_tac' 1 1);
+(* eliminate introduced subgoal 2 *)
+be forallQfilterPnil 2;
+ba 2;
+by (Fast_tac 2);
+
+(* f A (tw iA) = tw iA *)
+by (simp_tac (HOL_min_ss addsimps [filterPtakewhileQ,int_is_act]) 1);
+
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace] 1);
+(* subst divide_trace in conlcusion, but only at the righest occurence *)
+by (res_inst_tac [("t","schA")] ssubst 1);
+back();
+back();
+back();
+ba 1;
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite] 1);
+by (REPEAT (etac conjE 1));
+(* tidy up *)
+by (thin_tac' 12 1);
+by (thin_tac' 12 1);
+by (thin_tac' 14 1);
+by (thin_tac' 14 1);
+by (rotate_tac ~8 1);
+(* rewrite assumption forall and schB *)
+by (asm_full_simp_tac (!simpset addsimps [tconc_cong,forall_cons,forall_tconc,ext_and_act]) 1);
+(* divide_trace for schB2 *)
+by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_trace) 1);
+by (forw_inst_tac [("y","y2")](sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite) 1);
+by (REPEAT (etac conjE 1));
+by (rotate_tac ~6 1);
+(* assumption schA *)
+by (dres_inst_tac [("x","schA"),
+ ("g","tfilter`(plift (%a. a : actions (asig_of A)))`rs")] lemma22 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [tfiltertconc,not_int_is_ext,tfilterPtakewhileQ]) 1);
+by (REPEAT (etac conjE 1));
+(* f A (tw iB schB2) = nil *)
+
+(* good luck: intAisnotextB is not looping *)
+by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext,tfilterPtakewhileQ,intAisnotextB]) 1);
+(* reduce trace_takes from n to strictly smaller k *)
+by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext]) 1);
+br take_reduction 1;
+ba 1;
+(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
+(* assumption schB *)
+by (dres_inst_tac [("x","y2"),
+ ("g","tfilter`(plift (%a. a : actions (asig_of B)))`rs")] lemma22 1);
+ba 1;
+(* FIX: hey wonder: why does loopin rule for y2 here rewrites !!!!!!!!!!!!!!!!!!!!!!!!*)
+by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext,tfilterPtakewhileQ,intAisnotextB]) 1);
+by (REPEAT (etac conjE 1));
+(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
+by (dres_inst_tac [("sch","schA"),("P","plift (%a. a : internals (asig_of A))")] LastActExtsmall1 1);
+by (dres_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
+ba 1;
+by (dres_inst_tac [("sch","y2"),("P","plift (%a. a : internals (asig_of B))")] LastActExtsmall1 1);
+by (Asm_full_simp_tac 1);
+
+(* case x~:A & x:B *)
+(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
+by (case_tac "x:actions(asig_of B)" 1);
+by (Fast_tac 1);
+
+(* case x~:A & x~:B *)
+(* cannot occur because of assumption: forall (a:ext A | a:ext B) *)
+by (rotate_tac ~8 1);
+(* reduce forall assumption from tr to (Def x ## rs) *)
+by (asm_full_simp_tac (!simpset addsimps [forall_cons,forall_tconc]) 1);
+by (REPEAT (etac conjE 1));
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
+by (fast_tac (!claset addSIs [ext_is_act]) 1);
+
+qed"filterAmksch_is_schA";
+
+
+goal thy "!! tr. [|compat_ioas A B ; compat_ioas B A ;\
+\ forall (plift (%x.x:externals(asig_of (A||B)))) tr ; \
+\ tfilter`(plift (%a.a:externals(asig_of A)))`schA = tfilter`(plift (%a.a:actions(asig_of A)))`tr ;\
+\ tfilter`(plift (%a.a:externals(asig_of B)))`schB = tfilter`(plift (%a.a:actions(asig_of B)))`tr ;\
+\ LastActExtsch schA ; LastActExtsch schB |] \
+\ ==> tfilter`(plift (%a.a:actions(asig_of A)))`(mksch A B`tr`schA`schB) = schA";
+
+br trace.take_lemma 1;
+by (asm_simp_tac (!simpset addsimps [filterAmksch_is_schA]) 1);
+qed"filterAmkschschA";
+
+
+
+(* ------------------------------------------------------------------ *)
+(* COMPOSITIONALITY on TRACE Level *)
+(* Main Theorem *)
+(* ------------------------------------------------------------------ *)
+
+goal thy
+"!! A B. [| compat_ioas A B; compat_ioas B A; \
+\ is_asig(asig_of A); is_asig(asig_of B)|] \
+\ ==> traces(A||B) = \
+\ { tr.(Filter (%a.a:act A)`tr : traces A &\
+\ Filter (%a.a:act B)`tr : traces B &\
+\ Forall (%x. x:ext(A||B)) tr) }";
+
+by (simp_tac (!simpset addsimps [traces_def,has_trace_def]) 1);
+br set_ext 1;
+by (safe_tac set_cs);
+
+(* ==> *)
+(* There is a schedule of A *)
+by (res_inst_tac [("x","Filter (%a.a:act A)`sch")] bexI 1);
+by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
+by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence1,
+ externals_of_par,ext1_ext2_is_not_act1]) 1);
+(* There is a schedule of B *)
+by (res_inst_tac [("x","Filter (%a.a:act B)`sch")] bexI 1);
+by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
+by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2,
+ externals_of_par,ext1_ext2_is_not_act2]) 1);
+(* Traces of A||B have only external actions from A or B *)
+br ForallPFilterP 1;
+
+(* <== *)
+
+(* replace schA and schB by cutsch(schA) and cutsch(schB) *)
+by (dtac exists_LastActExtsch 1);
+ba 1;
+by (dtac exists_LastActExtsch 1);
+ba 1;
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+
+(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
+ we need here *)
+by (res_inst_tac [("x","mksch A B`tr`schb`schc")] bexI 1);
+
+(* External actions of mksch are just the oracle *)
+by (asm_full_simp_tac (!simpset addsimps [filterA_mksch_is_tr]) 1);
+
+(* mksch is a schedule -- use compositionality on sch-level *)
+by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 1);
+
+ das hier loopt: ForallPForallQ, ext_is_act,ForallAorB_mksch]) 1);
+
+
+
+
+
+
+*)
+
+
+
+(* -------------------------------------------------------------------------------
+ Other useful things
+ -------------------------------------------------------------------------------- *)
+
+
+(* Lemmata not needed yet
+goal Trace.thy "!!x. nil<<x ==> nil=x";
+by (res_inst_tac [("x","x")] trace.cases 1);
+by (hyp_subst_tac 1);
+by (etac antisym_less 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac 1);
+qed"nil_less_is_nil";
+
+
+*)
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,91 @@
+(* Title: HOLCF/IOA/meta_theory/CompoTraces.thy
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Compositionality on Trace level.
+*)
+
+CompoTraces = CompoScheds + ShortExecutions +
+
+
+consts
+
+ mksch ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq"
+
+
+defs
+
+mksch_def
+ "mksch A B == (fix`(LAM h tr schA schB. case tr of
+ nil => nil
+ | x##xs =>
+ (case x of
+ Undef => UU
+ | Def y =>
+ (if y:act A then
+ (if y:act B then
+ ((Takewhile (%a.a:int A)`schA)
+ @@ (Takewhile (%a.a:int B)`schB)
+ @@ (y>>(h`xs
+ `(TL`(Dropwhile (%a.a:int A)`schA))
+ `(TL`(Dropwhile (%a.a:int B)`schB))
+ )))
+ else
+ ((Takewhile (%a.a:int A)`schA)
+ @@ (y>>(h`xs
+ `(TL`(Dropwhile (%a.a:int A)`schA))
+ `schB)))
+ )
+ else
+ (if y:act B then
+ ((Takewhile (%a.a:int B)`schB)
+ @@ (y>>(h`xs
+ `schA
+ `(TL`(Dropwhile (%a.a:int B)`schB))
+ )))
+ else
+ UU
+ )
+ )
+ )))"
+
+
+rules
+
+(* FIX: x:actions S is further assumption, see Asig.ML: how to fulfill this in proofs ? *)
+not_ext_is_int_FIX
+ "[|is_asig S|] ==> (x~:externals S) = (x: internals S)"
+
+(* FIX: should be more general , something like subst *)
+lemma12
+"[| f << (g x) ; (x= (h x)) |] ==> f << g (h x)"
+
+(* FIX: as above, should be done more intelligent *)
+lemma22
+"[| (f x) = y >> g ; x = h x |] ==> (f (h x)) = y >> g"
+
+Finite_Conc
+ "Finite (x @@ y) = (Finite x & Finite y)"
+
+finiteR_mksch
+ "Finite (mksch A B`tr`x`y) --> Finite tr"
+
+finiteL_mksch
+ "[| Finite tr;
+ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr;
+ Filter (%a. a:ext B)`y = Filter (%a. a:actB)`tr;
+ Forall (%x. x:ext (A||B)) tr |]
+ ==> Finite (mksch A B`tr`x`y)"
+
+reduce_mksch
+ "[| Finite bs; Forall (%x. x:act B & x~:act A) bs;
+ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) |]
+ ==> ? y1 y2. (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) &
+ Forall (%x. x:act B & x~:act A) y1 &
+ Finite y1 & y = (y1 @@ y2) &
+ Filter (%a. a:ext B)`y1 = bs"
+
+end
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,23 @@
+(* Title: HOLCF/IOA/meta_theory/Compositionality.ML
+ ID:
+ Author: Olaf M"uller
+ Copyright 1997 TU Muenchen
+
+Compositionality of I/O automata
+*)
+
+
+goal thy "!! A1 A2 B1 B2. \
+\ [| is_asig (asig_of A1); is_asig (asig_of A2); \
+\ is_asig (asig_of B1); is_asig (asig_of B2); \
+\ compat_ioas A1 B1; compat_ioas B1 A1; compat_ioas A2 B2; compat_ioas B2 A2; \
+\ A1 =<| A2; \
+\ B1 =<| B2 |] \
+\ ==> (A1 || B1) =<| (A2 || B2)";
+by (asm_full_simp_tac (!simpset addsimps [ioa_implements_def,
+ inputs_of_par,outputs_of_par]) 1);
+
+
+by (safe_tac set_cs);
+by (asm_full_simp_tac (!simpset addsimps [compotraces]) 1);
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,21 @@
+(* Title: HOLCF/IOA/meta_theory/Compositionality.thy
+ ID:
+ Author: Olaf M"uller
+ Copyright 1997 TU Muenchen
+
+Compositionality of I/O automata
+*)
+
+Compositionality = CompoTraces +
+
+rules
+
+compotraces
+"[| compat_ioas A B; compat_ioas B A;
+ is_asig(asig_of A); is_asig(asig_of B)|]
+ ==> traces(A||B) =
+ {tr. (Filter (%a.a:act A)`tr : traces A &
+ Filter (%a.a:act B)`tr : traces B &
+ Forall (%x. x:ext(A||B)) tr)}"
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/IOA.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,7 @@
+(* Title: HOLCF/IOA/meta_theory/IOA.thy
+ ID:
+ Author: Olaf Mueller
+ Copyright 1996,1997 TU Muenchen
+
+The theory of I/O automata in HOLCF.
+*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/IOA.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,13 @@
+(* Title: HOLCF/IOA/meta_theory/IOA.thy
+ ID:
+ Author: Olaf Mueller
+ Copyright 1996,1997 TU Muenchen
+
+The theory of I/O automata in HOLCF.
+*)
+
+
+
+IOA = RefCorrectness + Compositionality
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,292 @@
+(* Title: HOLCF/IOA/meta_theory/RefCorrectness.ML
+ ID: $$
+ Author: Olaf Mueller
+ Copyright 1996 TU Muenchen
+
+Correctness of Refinement Mappings in HOLCF/IOA
+*)
+
+
+
+(* -------------------------------------------------------------------------------- *)
+
+section "corresp_ex";
+
+
+(* ---------------------------------------------------------------- *)
+(* corresp_ex2 *)
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "corresp_ex2 A f = (LAM ex. (%s. case ex of \
+\ nil => nil \
+\ | x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr)))) \
+\ @@ ((corresp_ex2 A f `xs) (f (snd pr)))) \
+\ `x) ))";
+by (rtac trans 1);
+br fix_eq2 1;
+br corresp_ex2_def 1;
+br beta_cfun 1;
+by (simp_tac (!simpset addsimps [flift1_def]) 1);
+qed"corresp_ex2_unfold";
+
+goal thy "(corresp_ex2 A f`UU) s=UU";
+by (stac corresp_ex2_unfold 1);
+by (Simp_tac 1);
+qed"corresp_ex2_UU";
+
+goal thy "(corresp_ex2 A f`nil) s = nil";
+by (stac corresp_ex2_unfold 1);
+by (Simp_tac 1);
+qed"corresp_ex2_nil";
+
+goal thy "(corresp_ex2 A f`(at>>xs)) s = \
+\ (snd(@cex. move A cex s (fst at) (f (snd at)))) \
+\ @@ ((corresp_ex2 A f`xs) (f (snd at)))";
+br trans 1;
+by (stac corresp_ex2_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
+by (Simp_tac 1);
+qed"corresp_ex2_cons";
+
+
+Addsimps [corresp_ex2_UU,corresp_ex2_nil,corresp_ex2_cons];
+
+
+
+(* ------------------------------------------------------------------ *)
+(* The following lemmata describe the definition *)
+(* of move in more detail *)
+(* ------------------------------------------------------------------ *)
+
+section"properties of move";
+
+goalw thy [is_ref_map_def]
+ "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+\ move A (@x. move A x (f s) a (f t)) (f s) a (f t)";
+
+by (subgoal_tac "? ex.move A ex (f s) a (f t)" 1);
+by (Asm_full_simp_tac 2);
+by (etac exE 1);
+by (rtac selectI 1);
+by (assume_tac 1);
+qed"move_is_move";
+
+goal thy
+ "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+\ is_execution_fragment A (@x. move A x (f s) a (f t))";
+by (cut_inst_tac [] move_is_move 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+qed"move_subprop1";
+
+goal thy
+ "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+\ Finite (snd (@x. move A x (f s) a (f t)))";
+by (cut_inst_tac [] move_is_move 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+qed"move_subprop2";
+
+goal thy
+ "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+\ fst (@x. move A x (f s) a (f t)) = (f s)";
+by (cut_inst_tac [] move_is_move 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+qed"move_subprop3";
+
+goal thy
+ "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+\ laststate (@x. move A x (f s) a (f t)) = (f t)";
+by (cut_inst_tac [] move_is_move 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+qed"move_subprop4";
+
+goal thy
+ "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+\ mk_trace A`(snd(@x. move A x (f s) a (f t))) = \
+\ (if a:ext A then a>>nil else nil)";
+
+by (cut_inst_tac [] move_is_move 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+qed"move_subprop5";
+
+goal thy
+ "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+\ (is_execution_fragment A (f s,(snd (@x. move A x (f s) a (f t)))))";
+by (cut_inst_tac [] move_subprop3 1);
+by (REPEAT (assume_tac 1));
+by (cut_inst_tac [] move_subprop1 1);
+by (REPEAT (assume_tac 1));
+by (res_inst_tac [("s","fst (@x. move A x (f s) a (f t))")] subst 1);
+back();
+back();
+back();
+ba 1;
+by (simp_tac (HOL_basic_ss addsimps [surjective_pairing RS sym]) 1);
+qed"move_subprop_1and3";
+
+goal thy
+ "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
+\ (case Last`(snd (@x. move A x (f s) a (f t))) of \
+\ Undef => (f s) \
+\ | Def p => snd p) = (f t)";
+by (cut_inst_tac [] move_subprop3 1);
+by (REPEAT (assume_tac 1));
+by (cut_inst_tac [] move_subprop4 1);
+by (REPEAT (assume_tac 1));
+by (asm_full_simp_tac (!simpset addsimps [laststate_def]) 1);
+qed"move_subprop_4and3";
+
+
+
+(* ------------------------------------------------------------------ *)
+(* The following lemmata contribute to *)
+(* TRACE INCLUSION Part 1: Traces coincide *)
+(* ------------------------------------------------------------------ *)
+
+section "Lemmata for <==";
+
+(* --------------------------------------------------- *)
+(* Lemma 1.1: Distribution of mk_trace and @@ *)
+(* --------------------------------------------------- *)
+
+
+goal thy "mk_trace C`(ex1 @@ ex2)= (mk_trace C`ex1) @@ (mk_trace C`ex2)";
+by (simp_tac (!simpset addsimps [mk_trace_def,filter_act_def,
+ FilterConc,MapConc]) 1);
+qed"mk_traceConc";
+
+
+
+(* ------------------------------------------------------
+ Lemma 1 :Traces coincide
+ ------------------------------------------------------- *)
+
+goalw thy [corresp_ex_def]
+ "!!f.[|is_ref_map f C A; ext C = ext A|] ==> \
+\ !s. reachable C s & is_execution_fragment C (s,xs) --> \
+\ mk_trace C`xs = mk_trace A`(snd (corresp_ex A f (s,xs)))";
+
+by (pair_induct_tac "xs" [is_execution_fragment_def] 1);
+(* cons case *)
+by (safe_tac set_cs);
+by (asm_full_simp_tac (!simpset addsimps [mk_traceConc]) 1);
+by (forward_tac [reachable.reachable_n] 1);
+ba 1;
+by (eres_inst_tac [("x","y")] allE 1);
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [move_subprop5]
+ setloop split_tac [expand_if] ) 1);
+qed"lemma_1";
+
+
+(* ------------------------------------------------------------------ *)
+(* The following lemmata contribute to *)
+(* TRACE INCLUSION Part 2: corresp_ex is execution *)
+(* ------------------------------------------------------------------ *)
+
+section "Lemmata for ==>";
+
+(* -------------------------------------------------- *)
+(* Lemma 2.1 *)
+(* -------------------------------------------------- *)
+
+goal thy
+"Finite xs --> \
+\(!s .is_execution_fragment A (s,xs) & is_execution_fragment A (t,ys) & \
+\ t = laststate (s,xs) \
+\ --> is_execution_fragment A (s,xs @@ ys))";
+
+br impI 1;
+by (Seq_Finite_induct_tac 1);
+(* base_case *)
+by (fast_tac HOL_cs 1);
+(* main case *)
+by (safe_tac set_cs);
+by (pair_tac "a" 1);
+qed"lemma_2_1";
+
+
+(* ----------------------------------------------------------- *)
+(* Lemma 2 : corresp_ex is execution *)
+(* ----------------------------------------------------------- *)
+
+
+
+goalw thy [corresp_ex_def]
+ "!!f.[| is_ref_map f C A |] ==>\
+\ !s. reachable C s & is_execution_fragment C (s,xs) \
+\ --> is_execution_fragment A (corresp_ex A f (s,xs))";
+
+by (Asm_full_simp_tac 1);
+by (pair_induct_tac "xs" [is_execution_fragment_def] 1);
+(* main case *)
+by (safe_tac set_cs);
+by (res_inst_tac [("t3","f y")] (lemma_2_1 RS mp RS spec RS mp) 1);
+
+(* Finite *)
+be move_subprop2 1;
+by (REPEAT (atac 1));
+by (rtac conjI 1);
+
+(* is_execution_fragment *)
+be move_subprop_1and3 1;
+by (REPEAT (atac 1));
+by (rtac conjI 1);
+
+(* Induction hypothesis *)
+(* reachable_n looping, therefore apply it manually *)
+by (eres_inst_tac [("x","y")] allE 1);
+by (Asm_full_simp_tac 1);
+by (forward_tac [reachable.reachable_n] 1);
+ba 1;
+by (Asm_full_simp_tac 1);
+(* laststate *)
+by (simp_tac (!simpset addsimps [laststate_def]) 1);
+be (move_subprop_4and3 RS sym) 1;
+by (REPEAT (atac 1));
+qed"lemma_2";
+
+
+(* -------------------------------------------------------------------------------- *)
+
+section "Main Theorem: T R A C E - I N C L U S I O N";
+
+(* -------------------------------------------------------------------------------- *)
+
+
+goalw thy [traces_def]
+ "!!f. [| IOA C; IOA A; ext C = ext A; is_ref_map f C A |] \
+\ ==> traces C <= traces A";
+
+ by (simp_tac(!simpset addsimps [has_trace_def2])1);
+ by (safe_tac set_cs);
+
+ (* give execution of abstract automata *)
+ by (res_inst_tac[("x","corresp_ex A f ex")] bexI 1);
+
+ (* Traces coincide, Lemma 1 *)
+ by (pair_tac "ex" 1);
+ by (etac (lemma_1 RS spec RS mp) 1);
+ by (REPEAT (atac 1));
+ by (asm_full_simp_tac (!simpset addsimps [executions_def,reachable.reachable_0]) 1);
+
+ (* corresp_ex is execution, Lemma 2 *)
+ by (pair_tac "ex" 1);
+ by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+ (* start state *)
+ by (rtac conjI 1);
+ by (asm_full_simp_tac (!simpset addsimps [is_ref_map_def,corresp_ex_def]) 1);
+ (* is-execution-fragment *)
+ by (etac (lemma_2 RS spec RS mp) 1);
+ by (asm_full_simp_tac (!simpset addsimps [reachable.reachable_0]) 1);
+qed"trace_inclusion";
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,35 @@
+(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy
+ ID: $$
+ Author: Olaf Mueller
+ Copyright 1996 TU Muenchen
+
+Correctness of Refinement Mappings in HOLCF/IOA
+*)
+
+
+RefCorrectness = RefMappings +
+
+consts
+
+ corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) =>
+ ('a,'s1)execution => ('a,'s2)execution"
+ corresp_ex2 ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
+ -> ('s2 => ('a,'s2)pairs)"
+
+
+defs
+
+corresp_ex_def
+ "corresp_ex A f ex == (f (fst ex),(corresp_ex2 A f`(snd ex)) (f (fst ex)))"
+
+
+corresp_ex2_def
+ "corresp_ex2 A f == (fix`(LAM h ex. (%s. case ex of
+ nil => nil
+ | x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr))))
+ @@ ((h`xs) (f (snd pr))))
+ `x) )))"
+
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,132 @@
+(* Title: HOLCF/IOA/meta_theory/RefMappings.ML
+ ID: $$
+ Author: Olaf Mueller
+ Copyright 1996 TU Muenchen
+
+Refinement Mappings in HOLCF/IOA
+*)
+
+
+
+goal thy "laststate (s,UU) = s";
+by (simp_tac (!simpset addsimps [laststate_def]) 1);
+qed"laststate_UU";
+
+goal thy "laststate (s,nil) = s";
+by (simp_tac (!simpset addsimps [laststate_def]) 1);
+qed"laststate_nil";
+
+goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
+by (simp_tac (!simpset addsimps [laststate_def]) 1);
+by (case_tac "ex=nil" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+bd (Finite_Last1 RS mp) 1;
+ba 1;
+by (def_tac 1);
+qed"laststate_cons";
+
+Addsimps [laststate_UU,laststate_nil,laststate_cons];
+
+(* ---------------------------------------------------------------------------- *)
+
+section "transitions and moves";
+
+
+goal thy"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
+
+by (res_inst_tac [("x","(s,(a,t)>>nil)")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+qed"transition_is_ex";
+
+
+goal thy"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
+
+by (res_inst_tac [("x","(s,nil)")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+qed"nothing_is_ex";
+
+
+goal thy"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
+\ ==> ? ex. move A ex s a s''";
+
+by (res_inst_tac [("x","(s,(a,s')>>(a',s'')>>nil)")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+qed"ei_transitions_are_ex";
+
+
+goal thy
+"!!f. (s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\
+\ (~a2:ext A) & (~a3:ext A) ==> \
+\ ? ex. move A ex s1 a1 s4";
+
+by (res_inst_tac [("x","(s1,(a1,s2)>>(a2,s3)>>(a3,s4)>>nil)")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
+qed"eii_transitions_are_ex";
+
+
+(* ---------------------------------------------------------------------------- *)
+
+section "weak_ref_map and ref_map";
+
+
+goalw thy [is_weak_ref_map_def,is_ref_map_def]
+ "!!f. [| ext C = ext A; \
+\ is_weak_ref_map f C A |] ==> is_ref_map f C A";
+by (safe_tac set_cs);
+by (case_tac "a:ext A" 1);
+by (rtac transition_is_ex 1);
+by (Asm_simp_tac 1);
+by (rtac nothing_is_ex 1);
+by (Asm_simp_tac 1);
+qed"weak_ref_map2ref_map";
+
+
+val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
+ by(fast_tac (!claset addDs prems) 1);
+qed "imp_conj_lemma";
+
+goal thy "!!f.[| is_weak_ref_map f C A |]\
+\ ==> (is_weak_ref_map f (rename C g) (rename A g))";
+by (asm_full_simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
+by (rtac conjI 1);
+(* 1: start states *)
+by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1);
+(* 2: reachable transitions *)
+by (REPEAT (rtac allI 1));
+by (rtac imp_conj_lemma 1);
+by (simp_tac (!simpset addsimps [rename_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
+asig_outputs_def,asig_of_def,trans_of_def]) 1);
+by (safe_tac (!claset));
+by (rtac (expand_if RS ssubst) 1);
+ by (rtac conjI 1);
+ by (rtac impI 1);
+ by (etac disjE 1);
+ by (etac exE 1);
+by (etac conjE 1);
+(* x is input *)
+ by (dtac sym 1);
+ by (dtac sym 1);
+by (Asm_full_simp_tac 1);
+by (REPEAT (hyp_subst_tac 1));
+by (forward_tac [reachable_rename] 1);
+by (Asm_full_simp_tac 1);
+(* x is output *)
+ by (etac exE 1);
+by (etac conjE 1);
+ by (dtac sym 1);
+ by (dtac sym 1);
+by (Asm_full_simp_tac 1);
+by (REPEAT (hyp_subst_tac 1));
+by (forward_tac [reachable_rename] 1);
+by (Asm_full_simp_tac 1);
+(* x is internal *)
+by (simp_tac (!simpset addcongs [conj_cong]) 1);
+by (rtac impI 1);
+by (etac conjE 1);
+by (forward_tac [reachable_rename] 1);
+by (Auto_tac());
+qed"rename_through_pmap";
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,50 @@
+(* Title: HOLCF/IOA/meta_theory/RefMappings.thy
+ ID: $$
+ Author: Olaf Mueller
+ Copyright 1996 TU Muenchen
+
+Refinement Mappings in HOLCF/IOA
+*)
+
+RefMappings = Traces +
+
+default term
+
+consts
+ laststate ::"('a,'s)execution => 's"
+ move ::"[('a,'s)ioa,('a,'s)execution,'s,'a,'s] => bool"
+ is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
+ is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
+
+defs
+
+laststate_def
+ "laststate ex == case Last`(snd ex) of
+ Undef => fst ex
+ | Def at => snd at"
+
+(* FIX: see paper, move should be defined on pairs, not on execs, then fst ex=s can
+ be omitted *)
+move_def
+ "move ioa ex s a t ==
+ (is_execution_fragment ioa ex & Finite (snd ex) &
+ fst ex=s & laststate ex=t &
+ mk_trace ioa`(snd ex) = (if a:ext(ioa) then a>>nil else nil))"
+
+is_ref_map_def
+ "is_ref_map f C A ==
+ (!s:starts_of(C). f(s):starts_of(A)) &
+ (!s t a. reachable C s &
+ s -a--C-> t
+ --> (? ex. move A ex (f s) a (f t)))"
+
+is_weak_ref_map_def
+ "is_weak_ref_map f C A ==
+ (!s:starts_of(C). f(s):starts_of(A)) &
+ (!s t a. reachable C s &
+ s -a--C-> t
+ --> (if a:ext(C)
+ then (f s) -a--A-> (f t)
+ else (f s)=(f t)))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,510 @@
+(* Title: HOLCF/IOA/meta_theory/Seq.ML
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+*)
+
+Addsimps (sfinite.intrs @ seq.rews);
+
+
+(* Instead of adding UU_neq_nil every equation UU~=x could be changed to x~=UU *)
+goal thy "UU ~=nil";
+by (res_inst_tac [("s1","UU"),("t1","nil")] (sym RS rev_contrapos) 1);
+by (REPEAT (Simp_tac 1));
+qed"UU_neq_nil";
+
+Addsimps [UU_neq_nil];
+
+(* ------------------------------------------------------------------------------------- *)
+
+
+(* ---------------------------------------------------- *)
+ section "recursive equations of operators";
+(* ---------------------------------------------------- *)
+
+
+(* ----------------------------------------------------------- *)
+(* smap *)
+(* ----------------------------------------------------------- *)
+
+bind_thm ("smap_unfold", fix_prover2 thy smap_def
+ "smap = (LAM f tr. case tr of \
+ \ nil => nil \
+ \ | x##xs => f`x ## smap`f`xs)");
+
+goal thy "smap`f`nil=nil";
+by (stac smap_unfold 1);
+by (Simp_tac 1);
+qed"smap_nil";
+
+goal thy "smap`f`UU=UU";
+by (stac smap_unfold 1);
+by (Simp_tac 1);
+qed"smap_UU";
+
+goal thy
+"!!x.[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs";
+br trans 1;
+by (stac smap_unfold 1);
+by (Asm_full_simp_tac 1);
+br refl 1;
+qed"smap_cons";
+
+(* ----------------------------------------------------------- *)
+(* sfilter *)
+(* ----------------------------------------------------------- *)
+
+bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def
+ "sfilter = (LAM P tr. case tr of \
+ \ nil => nil \
+ \ | x##xs => If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)");
+
+goal thy "sfilter`P`nil=nil";
+by (stac sfilter_unfold 1);
+by (Simp_tac 1);
+qed"sfilter_nil";
+
+goal thy "sfilter`P`UU=UU";
+by (stac sfilter_unfold 1);
+by (Simp_tac 1);
+qed"sfilter_UU";
+
+goal thy
+"!!x.x~=UU ==> sfilter`P`(x##xs)= \
+\ (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
+br trans 1;
+by (stac sfilter_unfold 1);
+by (Asm_full_simp_tac 1);
+br refl 1;
+qed"sfilter_cons";
+
+(* ----------------------------------------------------------- *)
+(* sforall2 *)
+(* ----------------------------------------------------------- *)
+
+bind_thm ("sforall2_unfold", fix_prover2 thy sforall2_def
+ "sforall2 = (LAM P tr. case tr of \
+ \ nil => TT \
+ \ | x##xs => (P`x andalso sforall2`P`xs))");
+
+goal thy "sforall2`P`nil=TT";
+by (stac sforall2_unfold 1);
+by (Simp_tac 1);
+qed"sforall2_nil";
+
+goal thy "sforall2`P`UU=UU";
+by (stac sforall2_unfold 1);
+by (Simp_tac 1);
+qed"sforall2_UU";
+
+goal thy
+"!!x.x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
+br trans 1;
+by (stac sforall2_unfold 1);
+by (Asm_full_simp_tac 1);
+br refl 1;
+qed"sforall2_cons";
+
+
+(* ----------------------------------------------------------- *)
+(* stakewhile *)
+(* ----------------------------------------------------------- *)
+
+
+bind_thm ("stakewhile_unfold", fix_prover2 thy stakewhile_def
+ "stakewhile = (LAM P tr. case tr of \
+ \ nil => nil \
+ \ | x##xs => (If P`x then x##(stakewhile`P`xs) else nil fi))");
+
+goal thy "stakewhile`P`nil=nil";
+by (stac stakewhile_unfold 1);
+by (Simp_tac 1);
+qed"stakewhile_nil";
+
+goal thy "stakewhile`P`UU=UU";
+by (stac stakewhile_unfold 1);
+by (Simp_tac 1);
+qed"stakewhile_UU";
+
+goal thy
+"!!x.x~=UU ==> stakewhile`P`(x##xs) = \
+\ (If P`x then x##(stakewhile`P`xs) else nil fi)";
+br trans 1;
+by (stac stakewhile_unfold 1);
+by (Asm_full_simp_tac 1);
+br refl 1;
+qed"stakewhile_cons";
+
+(* ----------------------------------------------------------- *)
+(* sdropwhile *)
+(* ----------------------------------------------------------- *)
+
+
+bind_thm ("sdropwhile_unfold", fix_prover2 thy sdropwhile_def
+ "sdropwhile = (LAM P tr. case tr of \
+ \ nil => nil \
+ \ | x##xs => (If P`x then sdropwhile`P`xs else tr fi))");
+
+goal thy "sdropwhile`P`nil=nil";
+by (stac sdropwhile_unfold 1);
+by (Simp_tac 1);
+qed"sdropwhile_nil";
+
+goal thy "sdropwhile`P`UU=UU";
+by (stac sdropwhile_unfold 1);
+by (Simp_tac 1);
+qed"sdropwhile_UU";
+
+goal thy
+"!!x.x~=UU ==> sdropwhile`P`(x##xs) = \
+\ (If P`x then sdropwhile`P`xs else x##xs fi)";
+br trans 1;
+by (stac sdropwhile_unfold 1);
+by (Asm_full_simp_tac 1);
+br refl 1;
+qed"sdropwhile_cons";
+
+
+(* ----------------------------------------------------------- *)
+(* slast *)
+(* ----------------------------------------------------------- *)
+
+
+bind_thm ("slast_unfold", fix_prover2 thy slast_def
+ "slast = (LAM tr. case tr of \
+ \ nil => UU \
+ \ | x##xs => (If is_nil`xs then x else slast`xs fi))");
+
+
+goal thy "slast`nil=UU";
+by (stac slast_unfold 1);
+by (Simp_tac 1);
+qed"slast_nil";
+
+goal thy "slast`UU=UU";
+by (stac slast_unfold 1);
+by (Simp_tac 1);
+qed"slast_UU";
+
+goal thy
+"!!x.x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
+br trans 1;
+by (stac slast_unfold 1);
+by (Asm_full_simp_tac 1);
+br refl 1;
+qed"slast_cons";
+
+
+(* ----------------------------------------------------------- *)
+(* sconc *)
+(* ----------------------------------------------------------- *)
+
+bind_thm ("sconc_unfold", fix_prover2 thy sconc_def
+ "sconc = (LAM t1 t2. case t1 of \
+ \ nil => t2 \
+ \ | x##xs => x ## (xs @@ t2))");
+
+
+goal thy "nil @@ y = y";
+by (stac sconc_unfold 1);
+by (Simp_tac 1);
+qed"sconc_nil";
+
+goal thy "UU @@ y=UU";
+by (stac sconc_unfold 1);
+by (Simp_tac 1);
+qed"sconc_UU";
+
+goal thy "(x##xs) @@ y=x##(xs @@ y)";
+br trans 1;
+by (stac sconc_unfold 1);
+by (Asm_full_simp_tac 1);
+by (case_tac "x=UU" 1);
+by (REPEAT (Asm_full_simp_tac 1));
+qed"sconc_cons";
+
+Addsimps [sconc_nil, sconc_UU,sconc_cons];
+
+
+(* ----------------------------------------------------------- *)
+(* sflat *)
+(* ----------------------------------------------------------- *)
+
+bind_thm ("sflat_unfold", fix_prover2 thy sflat_def
+ "sflat = (LAM tr. case tr of \
+ \ nil => nil \
+ \ | x##xs => x @@ sflat`xs)");
+
+goal thy "sflat`nil=nil";
+by (stac sflat_unfold 1);
+by (Simp_tac 1);
+qed"sflat_nil";
+
+goal thy "sflat`UU=UU";
+by (stac sflat_unfold 1);
+by (Simp_tac 1);
+qed"sflat_UU";
+
+goal thy "sflat`(x##xs)= x@@(sflat`xs)";
+br trans 1;
+by (stac sflat_unfold 1);
+by (Asm_full_simp_tac 1);
+by (case_tac "x=UU" 1);
+by (REPEAT (Asm_full_simp_tac 1));
+qed"sflat_cons";
+
+
+
+
+(* ----------------------------------------------------------- *)
+(* szip *)
+(* ----------------------------------------------------------- *)
+
+bind_thm ("szip_unfold", fix_prover2 thy szip_def
+ "szip = (LAM t1 t2. case t1 of \
+\ nil => nil \
+\ | x##xs => (case t2 of \
+\ nil => UU \
+\ | y##ys => <x,y>##(szip`xs`ys)))");
+
+goal thy "szip`nil`y=nil";
+by (stac szip_unfold 1);
+by (Simp_tac 1);
+qed"szip_nil";
+
+goal thy "szip`UU`y=UU";
+by (stac szip_unfold 1);
+by (Simp_tac 1);
+qed"szip_UU1";
+
+goal thy "!!x. x~=nil ==> szip`x`UU=UU";
+by (stac szip_unfold 1);
+by (Asm_full_simp_tac 1);
+by (res_inst_tac [("x","x")] seq.cases 1);
+by (REPEAT (Asm_full_simp_tac 1));
+qed"szip_UU2";
+
+goal thy "!!x.x~=UU ==> szip`(x##xs)`nil=UU";
+br trans 1;
+by (stac szip_unfold 1);
+by (REPEAT (Asm_full_simp_tac 1));
+qed"szip_cons_nil";
+
+goal thy "!!x.[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
+br trans 1;
+by (stac szip_unfold 1);
+by (REPEAT (Asm_full_simp_tac 1));
+qed"szip_cons";
+
+
+Addsimps [sfilter_UU,sfilter_nil,sfilter_cons,
+ smap_UU,smap_nil,smap_cons,
+ sforall2_UU,sforall2_nil,sforall2_cons,
+ slast_UU,slast_nil,slast_cons,
+ stakewhile_UU, stakewhile_nil, stakewhile_cons,
+ sdropwhile_UU, sdropwhile_nil, sdropwhile_cons,
+ sflat_UU,sflat_nil,sflat_cons,
+ szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons];
+
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+section "scons";
+
+goal thy
+ "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
+by (rtac iffI 1);
+by (etac (hd seq.injects) 1);
+auto();
+qed"scons_inject_eq";
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+section "sfilter, sforall, sconc";
+
+
+goal thy "(if b then tr1 else tr2) @@ tr \
+ \= (if b then tr1 @@ tr else tr2 @@ tr)";
+by (res_inst_tac [("P","b"),("Q","b")] impCE 1);
+by (fast_tac HOL_cs 1);
+by (REPEAT (Asm_full_simp_tac 1));
+qed"if_and_sconc";
+
+Addsimps [if_and_sconc];
+
+
+goal thy "sfilter`P`(x @@ y) = (sfilter`P`x @@ sfilter`P`y)";
+
+by (res_inst_tac[("x","x")] seq.ind 1);
+(* adm *)
+by (Simp_tac 1);
+(* base cases *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
+qed"sfiltersconc";
+
+goal thy "sforall P (stakewhile`P`x)";
+by (simp_tac (!simpset addsimps [sforall_def]) 1);
+by (res_inst_tac[("x","x")] seq.ind 1);
+(* adm *)
+by (simp_tac (!simpset addsimps [adm_trick_1]) 1);
+(* base cases *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
+qed"sforallPstakewhileP";
+
+goal thy "sforall P (sfilter`P`x)";
+by (simp_tac (!simpset addsimps [sforall_def]) 1);
+by (res_inst_tac[("x","x")] seq.ind 1);
+(* adm *)
+(* FIX should be refined in _one_ tactic *)
+by (simp_tac (!simpset addsimps [adm_trick_1]) 1);
+(* base cases *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
+qed"forallPsfilterP";
+
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+section "Finite";
+
+(* ---------------------------------------------------- *)
+(* Proofs of rewrite rules for Finite: *)
+(* 1. Finite(nil), (by definition) *)
+(* 2. ~Finite(UU), *)
+(* 3. a~=UU==> Finite(a##x)=Finite(x) *)
+(* ---------------------------------------------------- *)
+
+goal thy "Finite x --> x~=UU";
+br impI 1;
+be sfinite.induct 1;
+ by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed"Finite_UU_a";
+
+goal thy "~(Finite UU)";
+by (cut_inst_tac [("x","UU")]Finite_UU_a 1);
+by (fast_tac HOL_cs 1);
+qed"Finite_UU";
+
+goal thy "Finite x --> a~=UU --> x=a##xs --> Finite xs";
+by (strip_tac 1);
+be sfinite.elim 1;
+by (fast_tac (HOL_cs addss !simpset) 1);
+by (fast_tac (HOL_cs addSDs seq.injects) 1);
+qed"Finite_cons_a";
+
+goal thy "!!x.a~=UU ==>(Finite (a##x)) = (Finite x)";
+by (rtac iffI 1);
+by (rtac (Finite_cons_a RS mp RS mp RS mp) 1);
+by (REPEAT (assume_tac 1));
+by (fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+qed"Finite_cons";
+
+Addsimps [Finite_UU];
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+section "induction";
+
+
+(*-------------------------------- *)
+(* Extensions to Induction Theorems *)
+(*-------------------------------- *)
+
+
+qed_goalw "seq_finite_ind_lemma" thy [seq.finite_def]
+"(!!n.P(seq_take n`s)) ==> seq_finite(s) -->P(s)"
+ (fn prems =>
+ [
+ (strip_tac 1),
+ (etac exE 1),
+ (etac subst 1),
+ (resolve_tac prems 1)
+ ]);
+
+
+goal thy
+"!!P.[|P(UU);P(nil);\
+\ !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\
+\ |] ==> seq_finite(s) --> P(s)";
+by (rtac seq_finite_ind_lemma 1);
+be seq.finite_ind 1;
+ ba 1;
+by (Asm_full_simp_tac 1);
+qed"seq_finite_ind";
+
+
+
+
+(*
+(* -----------------------------------------------------------------
+ Fr"uhere Herleitung des endlichen Induktionsprinzips
+ aus dem seq_finite Induktionsprinzip.
+ Problem bei admissibility von Finite-->seq_finite!
+ Deshalb Finite jetzt induktiv und nicht mehr rekursiv definiert!
+ ------------------------------------------------------------------ *)
+
+goal thy "seq_finite nil";
+by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1);
+by (res_inst_tac [("x","Suc 0")] exI 1);
+by (simp_tac (!simpset addsimps seq.rews) 1);
+qed"seq_finite_nil";
+
+goal thy "seq_finite UU";
+by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1);
+qed"seq_finite_UU";
+
+Addsimps[seq_finite_nil,seq_finite_UU];
+
+goal HOL.thy "(B-->A) --> (A--> (B-->C))--> (B--> C)";
+by (fast_tac HOL_cs 1);
+qed"logic_lemma";
+
+
+goal thy "!!P.[| P nil; \
+\ !!a t. [|a~=UU;Finite t; P t|] ==> P (a##t)|]\
+\ ==> Finite x --> P x";
+
+by (rtac (logic_lemma RS mp RS mp) 1);
+by (rtac trf_impl_tf 1);
+by (rtac seq_finite_ind 1);
+by (simp_tac (!simpset addsimps [Finite_def]) 1);
+by (simp_tac (!simpset addsimps [Finite_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Finite_def]) 1);
+qed"Finite_ind";
+
+
+goal thy "Finite tr --> seq_finite tr";
+by (rtac seq.ind 1);
+(* adm *)
+(* hier grosses Problem !!!!!!!!!!!!!!! *)
+
+by (simp_tac (!simpset addsimps [Finite_def]) 2);
+by (simp_tac (!simpset addsimps [Finite_def]) 2);
+
+(* main case *)
+by (asm_full_simp_tac (!simpset addsimps [Finite_def,seq.sfinite_def]) 2);
+by (rtac impI 2);
+by (rotate_tac 2 2);
+by (Asm_full_simp_tac 2);
+by (etac exE 2);
+by (res_inst_tac [("x","Suc n")] exI 2);
+by (asm_full_simp_tac (!simpset addsimps seq.rews) 2);
+qed"tf_is_trf";
+
+*)
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,124 @@
+(* Title: HOLCF/IOA/meta_theory/Seq.thy
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Partial, Finite and Infinite Sequences (lazy lists), modeled as domain.
+*)
+
+
+Seq = HOLCF +
+
+domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq) (cinfixr 65)
+
+
+consts
+ sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
+ smap :: "('a -> 'b) -> 'a seq -> 'b seq"
+ sforall :: "('a -> tr) => 'a seq => bool"
+ sforall2 :: "('a -> tr) -> 'a seq -> tr"
+ slast :: "'a seq -> 'a"
+ sconc :: "'a seq -> 'a seq -> 'a seq"
+ sdropwhile,
+ stakewhile ::"('a -> tr) -> 'a seq -> 'a seq"
+ szip ::"'a seq -> 'b seq -> ('a*'b) seq"
+ sflat :: "('a seq) seq -> 'a seq"
+
+ sfinite :: "'a seq set"
+ Partial ::"'a seq => bool"
+ Infinite ::"'a seq => bool"
+
+ nproj :: "nat => 'a seq => 'a"
+
+syntax
+ "@@" :: "'a seq => 'a seq => 'a seq" (infixr 65)
+ "Finite" :: "'a seq => bool"
+
+translations
+ "xs @@ ys" == "sconc`xs`ys"
+ "Finite x" == "x:sfinite"
+ "~(Finite x)" =="x~:sfinite"
+
+defs
+
+
+
+(* f not possible at lhs, as "pattern matching" only for % x arguments,
+ f cannot be written at rhs in front, as fix_eq3 does not apply later *)
+smap_def
+ "smap == (fix`(LAM h f tr. case tr of
+ nil => nil
+ | x##xs => f`x ## h`f`xs))"
+
+sfilter_def
+ "sfilter == (fix`(LAM h P t. case t of
+ nil => nil
+ | x##xs => If P`x
+ then x##(h`P`xs)
+ else h`P`xs
+ fi))"
+sforall_def
+ "sforall P t == (sforall2`P`t ~=FF)"
+
+
+sforall2_def
+ "sforall2 == (fix`(LAM h P t. case t of
+ nil => TT
+ | x##xs => P`x andalso h`P`xs))"
+
+sconc_def
+ "sconc == (fix`(LAM h t1 t2. case t1 of
+ nil => t2
+ | x##xs => x##(h`xs`t2)))"
+
+slast_def
+ "slast == (fix`(LAM h t. case t of
+ nil => UU
+ | x##xs => (If is_nil`xs
+ then x
+ else h`xs fi)))"
+
+stakewhile_def
+ "stakewhile == (fix`(LAM h P t. case t of
+ nil => nil
+ | x##xs => If P`x
+ then x##(h`P`xs)
+ else nil
+ fi))"
+sdropwhile_def
+ "sdropwhile == (fix`(LAM h P t. case t of
+ nil => nil
+ | x##xs => If P`x
+ then h`P`xs
+ else t
+ fi))"
+sflat_def
+ "sflat == (fix`(LAM h t. case t of
+ nil => nil
+ | x##xs => x @@ (h`xs)))"
+
+szip_def
+ "szip == (fix`(LAM h t1 t2. case t1 of
+ nil => nil
+ | x##xs => (case t2 of
+ nil => UU
+ | y##ys => <x,y>##(h`xs`ys))))"
+
+
+proj_def
+ "nproj == (%n tr.HD`(iterate n TL tr))"
+
+Partial_def
+ "Partial x == (seq_finite x) & ~(Finite x)"
+
+Infinite_def
+ "Infinite x == ~(seq_finite x)"
+
+
+inductive "sfinite"
+ intrs
+ sfinite_0 "nil:sfinite"
+ sfinite_n "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite"
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,851 @@
+(* Title: HOLCF/IOA/meta_theory/Sequence.ML
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Theorems about Sequences over flat domains with lifted elements
+
+*)
+
+
+Addsimps [andalso_and,andalso_or];
+
+(* ----------------------------------------------------------------------------------- *)
+
+section "recursive equations of operators";
+
+(* ---------------------------------------------------------------- *)
+(* Map *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "Map f`UU =UU";
+by (simp_tac (!simpset addsimps [Map_def]) 1);
+qed"Map_UU";
+
+goal thy "Map f`nil =nil";
+by (simp_tac (!simpset addsimps [Map_def]) 1);
+qed"Map_nil";
+
+goal thy "Map f`(x>>xs)=(f x) >> Map f`xs";
+by (simp_tac (!simpset addsimps [Map_def, Cons_def,flift2_def]) 1);
+qed"Map_cons";
+
+(* ---------------------------------------------------------------- *)
+(* Filter *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "Filter P`UU =UU";
+by (simp_tac (!simpset addsimps [Filter_def]) 1);
+qed"Filter_UU";
+
+goal thy "Filter P`nil =nil";
+by (simp_tac (!simpset addsimps [Filter_def]) 1);
+qed"Filter_nil";
+
+goal thy "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)";
+by (simp_tac (!simpset addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1);
+qed"Filter_cons";
+
+(* ---------------------------------------------------------------- *)
+(* Forall *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "Forall P UU";
+by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1);
+qed"Forall_UU";
+
+goal thy "Forall P nil";
+by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1);
+qed"Forall_nil";
+
+goal thy "Forall P (x>>xs)= (P x & Forall P xs)";
+by (simp_tac (!simpset addsimps [Forall_def, sforall_def,
+ Cons_def,flift2_def]) 1);
+qed"Forall_cons";
+
+(* ---------------------------------------------------------------- *)
+(* Conc *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "UU @@ y =UU";
+by (Simp_tac 1);
+qed"Conc_UU";
+
+goal thy "nil @@ y =y";
+by (Simp_tac 1);
+qed"Conc_nil";
+
+goal thy "(x>>xs) @@ y = x>>(xs @@y)";
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"Conc_cons";
+
+(* ---------------------------------------------------------------- *)
+(* Takewhile *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "Takewhile P`UU =UU";
+by (simp_tac (!simpset addsimps [Takewhile_def]) 1);
+qed"Takewhile_UU";
+
+goal thy "Takewhile P`nil =nil";
+by (simp_tac (!simpset addsimps [Takewhile_def]) 1);
+qed"Takewhile_nil";
+
+goal thy "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)";
+by (simp_tac (!simpset addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1);
+qed"Takewhile_cons";
+
+(* ---------------------------------------------------------------- *)
+(* Dropwhile *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "Dropwhile P`UU =UU";
+by (simp_tac (!simpset addsimps [Dropwhile_def]) 1);
+qed"Dropwhile_UU";
+
+goal thy "Dropwhile P`nil =nil";
+by (simp_tac (!simpset addsimps [Dropwhile_def]) 1);
+qed"Dropwhile_nil";
+
+goal thy "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)";
+by (simp_tac (!simpset addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1);
+qed"Dropwhile_cons";
+
+(* ---------------------------------------------------------------- *)
+(* Last *)
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "Last`UU =UU";
+by (simp_tac (!simpset addsimps [Last_def]) 1);
+qed"Last_UU";
+
+goal thy "Last`nil =UU";
+by (simp_tac (!simpset addsimps [Last_def]) 1);
+qed"Last_nil";
+
+goal thy "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)";
+by (simp_tac (!simpset addsimps [Last_def, Cons_def]) 1);
+by (res_inst_tac [("x","xs")] seq.cases 1);
+by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (REPEAT (Asm_simp_tac 1));
+qed"Last_cons";
+
+
+(* ---------------------------------------------------------------- *)
+(* Flat *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "Flat`UU =UU";
+by (simp_tac (!simpset addsimps [Flat_def]) 1);
+qed"Flat_UU";
+
+goal thy "Flat`nil =nil";
+by (simp_tac (!simpset addsimps [Flat_def]) 1);
+qed"Flat_nil";
+
+goal thy "Flat`(x##xs)= x @@ (Flat`xs)";
+by (simp_tac (!simpset addsimps [Flat_def, Cons_def]) 1);
+qed"Flat_cons";
+
+
+(* ---------------------------------------------------------------- *)
+(* Zip *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "Zip = (LAM t1 t2. case t1 of \
+\ nil => nil \
+\ | x##xs => (case t2 of \
+\ nil => UU \
+\ | y##ys => (case x of \
+\ Undef => UU \
+\ | Def a => (case y of \
+\ Undef => UU \
+\ | Def b => Def (a,b)##(Zip`xs`ys)))))";
+by (rtac trans 1);
+br fix_eq2 1;
+br Zip_def 1;
+br beta_cfun 1;
+by (Simp_tac 1);
+qed"Zip_unfold";
+
+goal thy "Zip`UU`y =UU";
+by (stac Zip_unfold 1);
+by (Simp_tac 1);
+qed"Zip_UU1";
+
+goal thy "!! x. x~=nil ==> Zip`x`UU =UU";
+by (stac Zip_unfold 1);
+by (Simp_tac 1);
+by (res_inst_tac [("x","x")] seq.cases 1);
+by (REPEAT (Asm_full_simp_tac 1));
+qed"Zip_UU2";
+
+goal thy "Zip`nil`y =nil";
+by (stac Zip_unfold 1);
+by (Simp_tac 1);
+qed"Zip_nil";
+
+goal thy "Zip`(x>>xs)`nil= UU";
+by (stac Zip_unfold 1);
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"Zip_cons_nil";
+
+goal thy "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys";
+br trans 1;
+by (stac Zip_unfold 1);
+by (Simp_tac 1);
+(* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not
+ completely ready ? *)
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"Zip_cons";
+
+
+Delsimps [sfilter_UU,sfilter_nil,sfilter_cons,
+ smap_UU,smap_nil,smap_cons,
+ sforall2_UU,sforall2_nil,sforall2_cons,
+ slast_UU,slast_nil,slast_cons,
+ stakewhile_UU, stakewhile_nil, stakewhile_cons,
+ sdropwhile_UU, sdropwhile_nil, sdropwhile_cons,
+ sflat_UU,sflat_nil,sflat_cons,
+ szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons];
+
+
+Addsimps [Filter_UU,Filter_nil,Filter_cons,
+ Map_UU,Map_nil,Map_cons,
+ Forall_UU,Forall_nil,Forall_cons,
+ Last_UU,Last_nil,Last_cons,
+ Conc_UU,Conc_nil,Conc_cons,
+ Takewhile_UU, Takewhile_nil, Takewhile_cons,
+ Dropwhile_UU, Dropwhile_nil, Dropwhile_cons,
+ Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons];
+
+
+(*
+
+Can Filter with HOL predicate directly be defined as fixpoint ?
+
+goal thy "Filter2 P = (LAM tr. case tr of \
+ \ nil => nil \
+ \ | x##xs => (case x of Undef => UU | Def y => \
+\ (if P y then y>>(Filter2 P`xs) else Filter2 P`xs)))";
+by (rtac trans 1);
+br fix_eq2 1;
+br Filter2_def 1;
+br beta_cfun 1;
+by (Simp_tac 1);
+
+is also possible, if then else has to be proven continuous and it would be nice if a case for
+Seq would be available.
+
+*)
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+
+section "Cons";
+
+goal thy "a>>s = (Def a)##s";
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"Cons_def2";
+
+goal thy "x = UU | x = nil | (? a s. x = a >> s)";
+by (simp_tac (!simpset addsimps [Cons_def2]) 1);
+by (cut_facts_tac [seq.exhaust] 1);
+by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1);
+qed"Seq_exhaust";
+
+
+goal thy "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s ==> P |] ==> P";
+by (cut_inst_tac [("x","x")] Seq_exhaust 1);
+be disjE 1;
+by (Asm_full_simp_tac 1);
+be disjE 1;
+by (Asm_full_simp_tac 1);
+by (REPEAT (etac exE 1));
+by (Asm_full_simp_tac 1);
+qed"Seq_cases";
+
+fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i
+ THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
+
+(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
+fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2)
+ THEN Asm_full_simp_tac (i+1)
+ THEN Asm_full_simp_tac i;
+
+goal thy "a>>s ~= UU";
+by (stac Cons_def2 1);
+by (resolve_tac seq.con_rews 1);
+br Def_not_UU 1;
+qed"Cons_not_UU";
+
+goal thy "~(a>>x) << UU";
+by (rtac notI 1);
+by (dtac antisym_less 1);
+by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_not_UU]) 1);
+qed"Cons_not_less_UU";
+
+goal thy "~a>>s << nil";
+by (stac Cons_def2 1);
+by (resolve_tac seq.rews 1);
+br Def_not_UU 1;
+qed"Cons_not_less_nil";
+
+goal thy "a>>s ~= nil";
+by (stac Cons_def2 1);
+by (resolve_tac seq.rews 1);
+qed"Cons_not_nil";
+
+goal thy "(a>>s = b>>t) = (a = b & s = t)";
+by (simp_tac (HOL_ss addsimps [Cons_def2]) 1);
+by (stac (hd lift.inject RS sym) 1);
+back(); back();
+by (rtac scons_inject_eq 1);
+by (REPEAT(rtac Def_not_UU 1));
+qed"Cons_inject_eq";
+
+goal thy "(a>>s<<b>>t) = (a = b & s<<t)";
+by (simp_tac (!simpset addsimps [Cons_def2]) 1);
+by (stac (Def_inject_less_eq RS sym) 1);
+back();
+by (rtac iffI 1);
+(* 1 *)
+by (etac (hd seq.inverts) 1);
+by (REPEAT(rtac Def_not_UU 1));
+(* 2 *)
+by (Asm_full_simp_tac 1);
+by (etac conjE 1);
+by (etac monofun_cfun_arg 1);
+qed"Cons_inject_less_eq";
+
+goal thy "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)";
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"seq_take_Cons";
+
+Addsimps [Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
+ Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil];
+
+
+(* ----------------------------------------------------------------------------------- *)
+
+section "induction";
+
+goal thy "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x";
+be seq.ind 1;
+by (REPEAT (atac 1));
+by (def_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"Seq_induct";
+
+goal thy "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |] \
+\ ==> seq_finite x --> P x";
+be seq_finite_ind 1;
+by (REPEAT (atac 1));
+by (def_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"Seq_FinitePartial_ind";
+
+goal thy "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
+be sfinite.induct 1;
+ba 1;
+by (def_tac 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"Seq_Finite_ind";
+
+
+(* rws are definitions to be unfolded for admissibility check *)
+fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
+ THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
+ THEN simp_tac (!simpset addsimps rws) i;
+
+fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
+ THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
+
+fun pair_tac s = res_inst_tac [("p",s)] PairE
+ THEN' hyp_subst_tac THEN' Asm_full_simp_tac;
+
+(* induction on a sequence of pairs with pairsplitting and simplification *)
+fun pair_induct_tac s rws i =
+ res_inst_tac [("x",s)] Seq_induct i
+ THEN pair_tac "a" (i+3)
+ THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1))))
+ THEN simp_tac (!simpset addsimps rws) i;
+
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+section "HD,TL";
+
+goal thy "HD`(x>>y) = Def x";
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"HD_Cons";
+
+goal thy "TL`(x>>y) = y";
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"TL_Cons";
+
+Addsimps [HD_Cons,TL_Cons];
+
+(* ------------------------------------------------------------------------------------ *)
+
+section "Finite, Partial, Infinite";
+
+goal thy "Finite (a>>xs) = Finite xs";
+by (simp_tac (!simpset addsimps [Cons_def2,Finite_cons]) 1);
+qed"Finite_Cons";
+
+Addsimps [Finite_Cons];
+
+(* ------------------------------------------------------------------------------------ *)
+
+section "Conc";
+
+goal thy "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)";
+by (Seq_Finite_induct_tac 1);
+qed"Conc_cong";
+
+(* ------------------------------------------------------------------------------------ *)
+
+section "Last";
+
+goal thy "!! s.Finite s ==> s~=nil --> Last`s~=UU";
+by (Seq_Finite_induct_tac 1);
+by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+qed"Finite_Last1";
+
+goal thy "!! s. Finite s ==> Last`s=UU --> s=nil";
+by (Seq_Finite_induct_tac 1);
+by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
+by (fast_tac HOL_cs 1);
+qed"Finite_Last2";
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+
+section "Filter, Conc";
+
+
+goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
+by (Seq_induct_tac "s" [Filter_def] 1);
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"FilterPQ";
+
+goal thy "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
+by (simp_tac (!simpset addsimps [Filter_def,sfiltersconc]) 1);
+qed"FilterConc";
+
+(* ------------------------------------------------------------------------------------ *)
+
+section "Map";
+
+goal thy "Map f`(Map g`s) = Map (f o g)`s";
+by (Seq_induct_tac "s" [] 1);
+qed"MapMap";
+
+goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
+by (Seq_induct_tac "x" [] 1);
+qed"MapConc";
+
+goal thy "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)";
+by (Seq_induct_tac "x" [] 1);
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"MapFilter";
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+section "Forall, Conc";
+
+
+goal thy "Forall P ys & (! x. P x --> Q x) \
+\ --> Forall Q ys";
+by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
+qed"ForallPForallQ1";
+
+bind_thm ("ForallPForallQ",impI RSN (2,allI RSN (2,conjI RS (ForallPForallQ1 RS mp))));
+
+goal thy "(Forall P x & Forall P y) --> Forall P (x @@ y)";
+by (Seq_induct_tac "x" [Forall_def,sforall_def] 1);
+qed"Forall_Conc_impl";
+
+goal thy "!! x. Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
+by (Seq_Finite_induct_tac 1);
+qed"Forall_Conc";
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+section "Forall, Filter";
+
+
+goal thy "Forall P (Filter P`x)";
+by (simp_tac (!simpset addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
+qed"ForallPFilterP";
+
+(* FIX: holds also in other direction, then equal to forallPfilterP *)
+goal thy "Forall P x --> Filter P`x = x";
+by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
+qed"ForallPFilterPid1";
+
+val ForallPFilterPid = standard (ForallPFilterPid1 RS mp);
+
+
+(* holds also in <-- direction. FIX: prove that also *)
+
+goal thy "!! P. Finite ys & Forall (%x. ~P x) ys \
+\ --> Filter P`ys = nil ";
+by (res_inst_tac[("x","ys")] Seq_induct 1);
+(* adm *)
+(* FIX: cont tfinite behandeln *)
+br adm_all 1;
+(* base cases *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"ForallnPFilterPnil1";
+
+val ForallnPFilterPnil = standard (conjI RS (ForallnPFilterPnil1 RS mp));
+
+
+(* FIX: holds also in <== direction *)
+goal thy "!! P. ~Finite ys & Forall (%x. ~P x) ys \
+\ --> Filter P`ys = UU ";
+by (res_inst_tac[("x","ys")] Seq_induct 1);
+(* adm *)
+(* FIX: cont ~tfinite behandeln *)
+br adm_all 1;
+(* base cases *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"ForallnPFilterPUU1";
+
+val ForallnPFilterPUU = standard (conjI RS (ForallnPFilterPUU1 RS mp));
+
+
+goal thy "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
+\ ==> Filter P`ys = nil";
+be ForallnPFilterPnil 1;
+be ForallPForallQ 1;
+auto();
+qed"ForallQFilterPnil";
+
+goal thy "!! Q P. [| ~Finite ys; Forall Q ys; !!x. Q x ==> ~P x|] \
+\ ==> Filter P`ys = UU ";
+be ForallnPFilterPUU 1;
+be ForallPForallQ 1;
+auto();
+qed"ForallQFilterPUU";
+
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+section "Takewhile, Forall, Filter";
+
+
+goal thy "Forall P (Takewhile P`x)";
+by (simp_tac (!simpset addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
+qed"ForallPTakewhileP";
+
+
+goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
+br ForallPForallQ 1;
+br ForallPTakewhileP 1;
+auto();
+qed"ForallPTakewhileQ";
+
+
+goal thy "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \
+\ ==> Filter P`(Takewhile Q`ys) = nil";
+be ForallnPFilterPnil 1;
+br ForallPForallQ 1;
+br ForallPTakewhileP 1;
+auto();
+qed"FilterPTakewhileQnil";
+
+goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \
+\ Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)";
+br ForallPFilterPid 1;
+br ForallPForallQ 1;
+br ForallPTakewhileP 1;
+auto();
+qed"FilterPTakewhileQid";
+
+Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
+ FilterPTakewhileQnil,FilterPTakewhileQid];
+
+
+
+(* ----------------------------------------------------------------------------------- *)
+
+
+(*
+section "admissibility";
+
+goal thy "adm(%x.~Finite x)";
+br admI 1;
+bd spec 1;
+be contrapos 1;
+
+*)
+
+(* ----------------------------------------------------------------------------------- *)
+
+section "coinductive characterizations of Filter";
+
+
+goal thy "HD`(Filter P`y) = Def x \
+\ --> y = ((Takewhile (%x. ~P x)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
+\ & Finite (Takewhile (%x. ~ P x)`y) & P x";
+
+(* FIX: pay attention: is only admissible with chain-finite package to be added to
+ adm test *)
+by (Seq_induct_tac "y" [] 1);
+br adm_all 1;
+by (Asm_full_simp_tac 1);
+by (case_tac "P a" 1);
+by (Asm_full_simp_tac 1);
+br impI 1;
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac 1);
+(* ~ P a *)
+by (Asm_full_simp_tac 1);
+br impI 1;
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+by (REPEAT (etac conjE 1));
+ba 1;
+qed"divide_Seq_lemma";
+
+goal thy "!! x. (x>>xs) << Filter P`y \
+\ ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
+\ & Finite (Takewhile (%a. ~ P a)`y) & P x";
+br (divide_Seq_lemma RS mp) 1;
+by (dres_inst_tac [("fo","HD"),("xa","x>>xs")] monofun_cfun_arg 1);
+by (Asm_full_simp_tac 1);
+qed"divide_Seq";
+
+
+goal thy "~Forall P y --> (? x. HD`(Filter (%a. ~P a)`y) = Def x)";
+(* FIX: pay attention: is only admissible with chain-finite package to be added to
+ adm test *)
+by (Seq_induct_tac "y" [] 1);
+br adm_all 1;
+by (case_tac "P a" 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed"nForall_HDFilter";
+
+
+goal thy "!!y. ~Forall P y \
+\ ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
+\ Finite (Takewhile P`y) & (~ P x)";
+bd (nForall_HDFilter RS mp) 1;
+by (safe_tac set_cs);
+by (res_inst_tac [("x","x")] exI 1);
+by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1);
+auto();
+qed"divide_Seq2";
+
+
+goal thy "!! y. ~Forall P y \
+\ ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
+by (cut_inst_tac [] divide_Seq2 1);
+auto();
+qed"divide_Seq3";
+
+Addsimps [FilterPQ,FilterConc,Conc_cong,Forall_Conc];
+
+
+(* ------------------------------------------------------------------------------------- *)
+
+
+section "take_lemma";
+
+goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
+by (rtac iffI 1);
+br seq.take_lemma 1;
+auto();
+qed"seq_take_lemma";
+
+(*
+
+goal thy "Finite x & (! k. k < n --> seq_take k`y1 = seq_take k`y2) \
+\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2))";
+br less_induct 1;
+
+
+goal thy "!!x. Finite x ==> \
+\ ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \
+\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2)))";
+by (Seq_Finite_induct_tac 1);
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+
+
+qed"take_reduction";
+*)
+
+goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
+\ !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
+\ ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |] \
+\ ==> A x --> (f x)=(g x)";
+by (case_tac "Forall Q x" 1);
+by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+qed"take_lemma_principle1";
+
+goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
+\ !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
+\ ==> ! n. seq_take n`(f (s1 @@ y>>s2)) \
+\ = seq_take n`(g (s1 @@ y>>s2)) |] \
+\ ==> A x --> (f x)=(g x)";
+by (case_tac "Forall Q x" 1);
+by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+br seq.take_lemma 1;
+auto();
+qed"take_lemma_principle2";
+
+
+(* Note: in the following proofs the ordering of proof steps is very
+ important, as otherwise either (Forall Q s1) would be in the IH as
+ assumption (then rule useless) or it is not possible to strengthen
+ the IH by doing a forall closure of the sequence t (then rule also useless).
+ This is also the reason why the induction rule (less_induct or nat_induct) has to
+ to be imbuilt into the rule, as induction has to be done early and the take lemma
+ has to be used in the trivial direction afterwards for the (Forall Q x) case. *)
+
+goal thy
+"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
+\ !! s1 s2 y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\
+\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
+\ ==> seq_take (Suc n)`(f (s1 @@ y>>s2)) \
+\ = seq_take (Suc n)`(g (s1 @@ y>>s2)) |] \
+\ ==> A x --> (f x)=(g x)";
+br impI 1;
+br seq.take_lemma 1;
+br mp 1;
+ba 2;
+by (res_inst_tac [("x","x")] spec 1);
+br nat_induct 1;
+by (Simp_tac 1);
+br allI 1;
+by (case_tac "Forall Q xa" 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
+ !simpset)) 1);
+by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+qed"take_lemma_induct";
+
+
+goal thy
+"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
+\ !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m`(f t) = seq_take m`(g t);\
+\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
+\ ==> seq_take n`(f (s1 @@ y>>s2)) \
+\ = seq_take n`(g (s1 @@ y>>s2)) |] \
+\ ==> A x --> (f x)=(g x)";
+br impI 1;
+br seq.take_lemma 1;
+br mp 1;
+ba 2;
+by (res_inst_tac [("x","x")] spec 1);
+br less_induct 1;
+br allI 1;
+by (case_tac "Forall Q xa" 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
+ !simpset)) 1);
+by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+qed"take_lemma_less_induct";
+
+goal thy
+"!! Q. [| A UU ==> (f UU) = (g UU) ; \
+\ A nil ==> (f nil) = (g nil) ; \
+\ !! s y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\
+\ A (y>>s) |] \
+\ ==> seq_take (Suc n)`(f (y>>s)) \
+\ = seq_take (Suc n)`(g (y>>s)) |] \
+\ ==> A x --> (f x)=(g x)";
+br impI 1;
+br seq.take_lemma 1;
+br mp 1;
+ba 2;
+by (res_inst_tac [("x","x")] spec 1);
+br nat_induct 1;
+by (Simp_tac 1);
+br allI 1;
+by (Seq_case_simp_tac "xa" 1);
+qed"take_lemma_in_eq_out";
+
+
+(* ------------------------------------------------------------------------------------ *)
+
+section "alternative take_lemma proofs";
+
+
+(* --------------------------------------------------------------- *)
+(* Alternative Proof of FilterPQ *)
+(* --------------------------------------------------------------- *)
+
+Delsimps [FilterPQ];
+
+
+(* In general: How to do this case without the same adm problems
+ as for the entire proof ? *)
+goal thy "Forall (%x.~(P x & Q x)) s \
+\ --> Filter P`(Filter Q`s) =\
+\ Filter (%x. P x & Q x)`s";
+
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"Filter_lemma1";
+
+goal thy "!! s. Finite s ==> \
+\ (Forall (%x. (~P x) | (~ Q x)) s \
+\ --> Filter P`(Filter Q`s) = nil)";
+by (Seq_Finite_induct_tac 1);
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"Filter_lemma2";
+
+goal thy "!! s. Finite s ==> \
+\ Forall (%x. (~P x) | (~ Q x)) s \
+\ --> Filter (%x.P x & Q x)`s = nil";
+by (Seq_Finite_induct_tac 1);
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"Filter_lemma3";
+
+
+goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
+by (res_inst_tac [("A1","%x.True")
+ ,("Q1","%x.~(P x & Q x)")]
+ (take_lemma_induct RS mp) 1);
+(* FIX: rule always needs a back: eliminate *)
+back();
+(* FIX: better support for A = %.True *)
+by (Fast_tac 3);
+by (asm_full_simp_tac (!simpset addsimps [Filter_lemma1]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Filter_lemma2,Filter_lemma3]
+ setloop split_tac [expand_if]) 1);
+qed"FilterPQ_takelemma";
+
+Addsimps [FilterPQ];
+
+
+(* --------------------------------------------------------------- *)
+(* Alternative Proof of MapConc *)
+(* --------------------------------------------------------------- *)
+
+Delsimps [MapConc];
+
+goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
+by (res_inst_tac [("A1","%x.True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
+auto();
+qed"MapConc_takelemma";
+
+Addsimps [MapConc];
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,91 @@
+(* Title: HOLCF/IOA/meta_theory/Sequence.thy
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Sequences over flat domains with lifted elements
+
+*)
+
+Sequence = Seq +
+
+default term
+
+types 'a Seq = ('a::term lift)seq
+
+ops curried
+
+ Cons ::"'a => 'a Seq -> 'a Seq"
+ Filter ::"('a => bool) => 'a Seq -> 'a Seq"
+ Map ::"('a => 'b) => 'a Seq -> 'b Seq"
+ Forall ::"('a => bool) => 'a Seq => bool"
+ Last ::"'a Seq -> 'a lift"
+ Dropwhile,
+ Takewhile ::"('a => bool) => 'a Seq -> 'a Seq"
+ Zip ::"'a Seq -> 'b Seq -> ('a * 'b) Seq"
+ Flat ::"('a Seq) seq -> 'a Seq"
+
+ Filter2 ::"('a => bool) => 'a Seq -> 'a Seq"
+
+syntax
+
+ "@Cons" ::"'a => 'a Seq => 'a Seq" ("(_>>_)" [66,65] 65)
+
+syntax (symbols)
+
+ "@Cons" ::"'a => 'a Seq => 'a Seq" ("(_\\<leadsto>_)" [66,65] 65)
+
+
+translations
+
+ "a>>s" == "Cons a`s"
+
+defs
+
+
+Cons_def "Cons a == LAM s. Def a ## s"
+
+Filter_def "Filter P == sfilter`(flift2 P)"
+
+Map_def "Map f == smap`(flift2 f)"
+
+Forall_def "Forall P == sforall (flift2 P)"
+
+Last_def "Last == slast"
+
+Dropwhile_def "Dropwhile P == sdropwhile`(flift2 P)"
+
+Takewhile_def "Takewhile P == stakewhile`(flift2 P)"
+
+Flat_def "Flat == sflat"
+
+Zip_def
+ "Zip == (fix`(LAM h t1 t2. case t1 of
+ nil => nil
+ | x##xs => (case t2 of
+ nil => UU
+ | y##ys => (case x of
+ Undef => UU
+ | Def a => (case y of
+ Undef => UU
+ | Def b => Def (a,b)##(h`xs`ys))))))"
+
+Filter2_def "Filter2 P == (fix`(LAM h t. case t of
+ nil => nil
+ | x##xs => (case x of Undef => UU | Def y => (if P y
+ then x##(h`xs)
+ else h`xs))))"
+
+rules
+
+
+(* for test purposes should be deleted FIX !! *)
+adm_all "adm f"
+
+
+take_reduction
+ "[| Finite x; !! k. k < n ==> seq_take k`y1 = seq_take k`y2 |]
+ ==> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2))"
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,11 @@
+(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy
+ ID:
+ Author: Olaf M"uller
+ Copyright 1997 TU Muenchen
+
+Some properties about cut(ex), defined as follows:
+
+For every execution ex there is another shorter execution cut(ex)
+that has the same trace as ex, but its schedule ends with an external action.
+
+*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,54 @@
+(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy
+ ID:
+ Author: Olaf M"uller
+ Copyright 1997 TU Muenchen
+
+Some properties about cut(ex), defined as follows:
+
+For every execution ex there is another shorter execution cut(ex)
+that has the same trace as ex, but its schedule ends with an external action.
+
+*)
+
+
+ShortExecutions = Traces +
+
+consts
+
+ LastActExtsch ::"'a Seq => bool"
+ cutsch ::"'a Seq => 'a Seq"
+
+
+defs
+
+LastActExtsch_def
+ "LastActExtsch sch == (cutsch sch = sch)"
+
+
+rules
+
+exists_LastActExtsch
+ "[|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|]
+ ==> ? sch. sch : schedules A &
+ tr = Filter (%a.a:ext A)`sch &
+ LastActExtsch sch"
+
+(* FIX: 1. LastActExtsch should have argument A also?
+ 2. use equality: (I) f P x =UU <-> (II) (fa ~P x) & ~finite(x) to prove it for (II) instead *)
+LastActExtimplUU
+ "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = UU |]
+ ==> sch=UU"
+
+(* FIX: see above *)
+LastActExtimplnil
+ "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = nil |]
+ ==> sch=nil"
+
+LastActExtsmall1
+ "LastActExtsch sch ==> LastActExtsch (TL`(Dropwhile P`sch))"
+
+LastActExtsmall2
+ "[| Finite sch1; LastActExtsch (sch1 @@ sch2) |] ==> LastActExtsch (sch2)"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,152 @@
+(* Title: HOLCF/IOA/meta_theory/Traces.ML
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Theorems about Executions and Traces of I/O automata in HOLCF.
+*)
+
+
+
+val exec_rws = [executions_def,is_execution_fragment_def];
+
+
+
+(* ----------------------------------------------------------------------------------- *)
+
+section "recursive equations of operators";
+
+
+(* ---------------------------------------------------------------- *)
+(* filter_act *)
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "filter_act`UU = UU";
+by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+qed"filter_act_UU";
+
+goal thy "filter_act`nil = nil";
+by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+qed"filter_act_nil";
+
+goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
+by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+qed"filter_act_cons";
+
+Addsimps [filter_act_UU,filter_act_nil,filter_act_cons];
+
+
+(* ---------------------------------------------------------------- *)
+(* mk_trace *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "mk_trace A`UU=UU";
+by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
+qed"mk_trace_UU";
+
+goal thy "mk_trace A`nil=nil";
+by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
+qed"mk_trace_nil";
+
+goal thy "mk_trace A`(at >> xs) = \
+\ (if ((fst at):ext A) \
+\ then (fst at) >> (mk_trace A`xs) \
+\ else mk_trace A`xs)";
+
+by (asm_full_simp_tac (!simpset addsimps [mk_trace_def]) 1);
+qed"mk_trace_cons";
+
+Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons];
+
+(* ---------------------------------------------------------------- *)
+(* is_ex_fr *)
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "is_ex_fr A = (LAM ex. (%s. case ex of \
+\ nil => TT \
+\ | x##xs => (flift1 \
+\ (%p.Def ((s,p):trans_of A) andalso (is_ex_fr A`xs) (snd p)) \
+\ `x) \
+\ ))";
+by (rtac trans 1);
+br fix_eq2 1;
+br is_ex_fr_def 1;
+br beta_cfun 1;
+by (simp_tac (!simpset addsimps [flift1_def]) 1);
+qed"is_ex_fr_unfold";
+
+goal thy "(is_ex_fr A`UU) s=UU";
+by (stac is_ex_fr_unfold 1);
+by (Simp_tac 1);
+qed"is_ex_fr_UU";
+
+goal thy "(is_ex_fr A`nil) s = TT";
+by (stac is_ex_fr_unfold 1);
+by (Simp_tac 1);
+qed"is_ex_fr_nil";
+
+goal thy "(is_ex_fr A`(pr>>xs)) s = \
+\ (Def ((s,pr):trans_of A) \
+\ andalso (is_ex_fr A`xs)(snd pr))";
+br trans 1;
+by (stac is_ex_fr_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
+by (Simp_tac 1);
+qed"is_ex_fr_cons";
+
+
+Addsimps [is_ex_fr_UU,is_ex_fr_nil,is_ex_fr_cons];
+
+
+(* ---------------------------------------------------------------- *)
+(* is_execution_fragment *)
+(* ---------------------------------------------------------------- *)
+
+goal thy "is_execution_fragment A (s, UU)";
+by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1);
+qed"is_execution_fragment_UU";
+
+goal thy "is_execution_fragment A (s, nil)";
+by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1);
+qed"is_execution_fragment_nil";
+
+goal thy "is_execution_fragment A (s, (a,t)>>ex) = \
+\ (((s,a,t):trans_of A) & \
+\ is_execution_fragment A (t, ex))";
+by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1);
+qed"is_execution_fragment_cons";
+
+
+(* Delsimps [is_ex_fr_UU,is_ex_fr_nil,is_ex_fr_cons]; *)
+Addsimps [is_execution_fragment_UU,is_execution_fragment_nil, is_execution_fragment_cons];
+
+
+(* -------------------------------------------------------------------------------- *)
+
+section "has_trace, mk_trace";
+
+(* alternative definition of has_trace tailored for the refinement proof, as it does not
+ take the detour of schedules *)
+
+goalw thy [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def]
+"has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))";
+
+by (safe_tac set_cs);
+(* 1 *)
+by (res_inst_tac[("x","ex")] bexI 1);
+by (stac beta_cfun 1);
+by (cont_tacR 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+(* 2 *)
+by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1);
+by (stac beta_cfun 1);
+by (cont_tacR 1);
+by (Simp_tac 1);
+by (safe_tac set_cs);
+by (res_inst_tac[("x","ex")] bexI 1);
+by (REPEAT (Asm_simp_tac 1));
+qed"has_trace_def2";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy Wed Apr 30 11:20:15 1997 +0200
@@ -0,0 +1,107 @@
+(* Title: HOLCF/IOA/meta_theory/Traces.thy
+ ID:
+ Author: Olaf M"uller
+ Copyright 1996 TU Muenchen
+
+Executions and Traces of I/O automata in HOLCF.
+*)
+
+
+Traces = Automata + Sequence +
+
+default term
+
+types
+ ('a,'s)pairs = "('a * 's) Seq"
+ ('a,'s)execution = "'s * ('a,'s)pairs"
+ 'a trace = "'a Seq"
+
+consts
+
+ (* Executions *)
+ is_ex_fr ::"('a,'s)ioa => ('a,'s)pairs -> ('s => tr)"
+ is_execution_fragment,
+ has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool"
+ executions :: "('a,'s)ioa => ('a,'s)execution set"
+
+ (* Schedules and traces *)
+ filter_act ::"('a,'s)pairs -> 'a trace"
+ has_schedule,
+ has_trace :: "[('a,'s)ioa, 'a trace] => bool"
+ schedules,
+ traces :: "('a,'s)ioa => 'a trace set"
+
+ mk_trace :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"
+
+ (* Notion of implementation *)
+ "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr 12)
+
+(*
+(* FIX: introduce good symbol *)
+syntax (symbols)
+
+ "op <<|" ::"[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "\\<parallel>" 10)
+*)
+
+
+defs
+
+
+(* ------------------- Executions ------------------------------ *)
+
+
+is_execution_fragment_def
+ "is_execution_fragment A ex == ((is_ex_fr A`(snd ex)) (fst ex) ~= FF)"
+
+is_ex_fr_def
+ "is_ex_fr A ==(fix`(LAM h ex. (%s. case ex of
+ nil => TT
+ | x##xs => (flift1
+ (%p.Def ((s,p):trans_of A) andalso (h`xs) (snd p))
+ `x)
+ )))"
+
+executions_def
+ "executions ioa == {e. ((fst e) : starts_of(ioa)) &
+ is_execution_fragment ioa e}"
+
+
+(* ------------------- Schedules ------------------------------ *)
+
+
+filter_act_def
+ "filter_act == Map fst"
+
+has_schedule_def
+ "has_schedule ioa sch ==
+ (? ex:executions ioa. sch = filter_act`(snd ex))"
+
+schedules_def
+ "schedules ioa == {sch. has_schedule ioa sch}"
+
+
+(* ------------------- Traces ------------------------------ *)
+
+has_trace_def
+ "has_trace ioa tr ==
+ (? sch:schedules ioa. tr = Filter (%a.a:ext(ioa))`sch)"
+
+traces_def
+ "traces ioa == {tr. has_trace ioa tr}"
+
+
+mk_trace_def
+ "mk_trace ioa == LAM tr.
+ Filter (%a.a:ext(ioa))`(filter_act`tr)"
+
+
+(* ------------------- Implementation ------------------------------ *)
+
+ioa_implements_def
+ "ioa1 =<| ioa2 ==
+ (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
+ (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
+ traces(ioa1) <= traces(ioa2))"
+
+
+end
\ No newline at end of file