New meta theory for IOA based on HOLCF.
authormueller
Wed Apr 30 11:20:15 1997 +0200 (1997-04-30)
changeset 3071981258186b71
parent 3070 cadbaef4f4a5
child 3072 a31419014be5
New meta theory for IOA based on HOLCF.
src/HOLCF/IOA/README.html
src/HOLCF/IOA/ROOT.ML
src/HOLCF/IOA/meta_theory/Asig.ML
src/HOLCF/IOA/meta_theory/Asig.thy
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/IOA/meta_theory/CompoExecs.ML
src/HOLCF/IOA/meta_theory/CompoExecs.thy
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/CompoTraces.thy
src/HOLCF/IOA/meta_theory/Compositionality.ML
src/HOLCF/IOA/meta_theory/Compositionality.thy
src/HOLCF/IOA/meta_theory/IOA.ML
src/HOLCF/IOA/meta_theory/IOA.thy
src/HOLCF/IOA/meta_theory/RefCorrectness.ML
src/HOLCF/IOA/meta_theory/RefCorrectness.thy
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/IOA/meta_theory/RefMappings.thy
src/HOLCF/IOA/meta_theory/Seq.ML
src/HOLCF/IOA/meta_theory/Seq.thy
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/IOA/meta_theory/ShortExecutions.ML
src/HOLCF/IOA/meta_theory/ShortExecutions.thy
src/HOLCF/IOA/meta_theory/Traces.ML
src/HOLCF/IOA/meta_theory/Traces.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/README.html	Wed Apr 30 11:20:15 1997 +0200
     1.3 @@ -0,0 +1,38 @@
     1.4 +<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
     1.5 +
     1.6 +<H3>IOA: A formalization of I/O automata in HOLCF</H3>
     1.7 +
     1.8 +Author:     Olaf Mueller<BR>
     1.9 +Copyright   1997 Technische Universit&auml;t M&uuml;nchen<P>
    1.10 +
    1.11 +Version: 1.0<BR>
    1.12 +Date: 1.05.97<P>
    1.13 +
    1.14 +The distribution contains
    1.15 +
    1.16 +<UL>
    1.17 +  <li> A semantic model of the meta theory of I/O automata including proofs for the refinement notion
    1.18 +       and the compositionality of the model. For details see: <BR>
    1.19 +       Olaf M&uuml;ller and Tobias Nipkow,
    1.20 +       <A HREF="http://www4.informatik.tu-muenchen.de/papers/tapsoft_mueller_1997_Conference.html">Traces of I/O Automata in Isabelle/HOLCF</A>.
    1.21 +In <i> TAPSOFT'97, Proc. of the 7th  International Joint Conference on Theory and Practice of Software Development </i>, LNCS 1224, 1997.<P>
    1.22 +
    1.23 +  <li> A proof of the Alternating Bit Protocol (ABP subdirectory) with unbounded buffers using 
    1.24 +       a combination of Isabelle and a model checker. This case study is performed within the 
    1.25 +       theory of IOA described above. For details see:<BR>
    1.26 +Olaf M&uuml;ller and Tobias Nipkow,
    1.27 +<A HREF="http://www4.informatik.tu-muenchen.de/papers/MuellerNipkow_TaAf1995.html">Combining Model Checking and Deduction for I/O Automata  </A>.
    1.28 +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>
    1.29 +   <li> A proof of a Network Transmission Protocol (NTP subdirectory) using the theory of IOA described above. For details see:<BR>
    1.30 +
    1.31 +        Tobias Nipkow, Konrad Slind.
    1.32 +<A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/ioa.html>
    1.33 +I/O Automata in Isabelle/HOL</A>. In <i>Types for Proofs and Programs</i>,
    1.34 +LNCS 996, 1995, 101-119.
    1.35 +
    1.36 +</UL>
    1.37 +
    1.38 +</BODY></HTML>
    1.39 +
    1.40 +
    1.41 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOLCF/IOA/ROOT.ML	Wed Apr 30 11:20:15 1997 +0200
     2.3 @@ -0,0 +1,18 @@
     2.4 +(*  Title:      HOL/IOA/meta_theory/ROOT.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Olaf Mueller
     2.7 +    Copyright   1997  TU Muenchen
     2.8 +
     2.9 +This is the ROOT file for the formalization of a semantic model of I/O-Automata.
    2.10 +
    2.11 +See the README.html file for details.
    2.12 +
    2.13 +Should be executed in the subdirectory HOLCF/IOA/meta_theory.
    2.14 +*)
    2.15 +
    2.16 +
    2.17 +goals_limit:=1;
    2.18 +
    2.19 +loadpath := ["meta_theory"];
    2.20 +
    2.21 +use_thy"IOA";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/IOA/meta_theory/Asig.ML	Wed Apr 30 11:20:15 1997 +0200
     3.3 @@ -0,0 +1,38 @@
     3.4 +(*  Title:      HOL/IOA/meta_theory/Asig.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Olaf Mueller, Tobias Nipkow & Konrad Slind
     3.7 +    Copyright   1994,1996  TU Muenchen
     3.8 +
     3.9 +Action signatures
    3.10 +*)
    3.11 +
    3.12 +open Asig;
    3.13 +
    3.14 +val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
    3.15 +
    3.16 +goal thy "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
    3.17 +by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
    3.18 +qed"int_and_ext_is_act";
    3.19 +
    3.20 +goal thy "!!a.[|a:externals(S)|] ==> a:actions(S)";
    3.21 +by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
    3.22 +qed"ext_is_act";
    3.23 +
    3.24 +goal thy "!!a.[|a:internals S|] ==> a:actions S";
    3.25 +by (asm_full_simp_tac (!simpset addsimps [asig_internals_def,actions_def]) 1);
    3.26 +qed"int_is_act";
    3.27 +
    3.28 +goal thy "(x: actions S & x : externals S) = (x: externals S)";
    3.29 +by (fast_tac (!claset addSIs [ext_is_act]) 1 );
    3.30 +qed"ext_and_act";
    3.31 + 
    3.32 +goal thy "!!S. [|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)";
    3.33 +by (asm_full_simp_tac (!simpset addsimps [actions_def,is_asig_def,externals_def]) 1);
    3.34 +by (best_tac (set_cs addEs [equalityCE]) 1);
    3.35 +qed"not_ext_is_int";
    3.36 +
    3.37 +goalw thy  [externals_def,actions_def,is_asig_def]
    3.38 + "!! x. [| is_asig (S); x:internals S |] ==> x~:externals S";
    3.39 +by (Asm_full_simp_tac 1);
    3.40 +by (best_tac (set_cs addEs [equalityCE]) 1);
    3.41 +qed"int_is_not_ext";
    3.42 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOLCF/IOA/meta_theory/Asig.thy	Wed Apr 30 11:20:15 1997 +0200
     4.3 @@ -0,0 +1,45 @@
     4.4 +(*  Title:      HOL/IOA/meta_theory/Asig.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Nipkow & Konrad Slind
     4.7 +    Copyright   1994  TU Muenchen
     4.8 +
     4.9 +Action signatures
    4.10 +*)
    4.11 +
    4.12 +Asig = Arith +
    4.13 +
    4.14 +types 
    4.15 +
    4.16 +'a signature = "('a set * 'a set * 'a set)"
    4.17 +
    4.18 +consts
    4.19 +  actions,inputs,outputs,internals,externals
    4.20 +                ::"'action signature => 'action set"
    4.21 +  is_asig       ::"'action signature => bool"
    4.22 +  mk_ext_asig   ::"'action signature => 'action signature"
    4.23 +
    4.24 +
    4.25 +defs
    4.26 +
    4.27 +asig_inputs_def    "inputs == fst"
    4.28 +asig_outputs_def   "outputs == (fst o snd)"
    4.29 +asig_internals_def "internals == (snd o snd)"
    4.30 +
    4.31 +actions_def
    4.32 +   "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
    4.33 +
    4.34 +externals_def
    4.35 +   "externals(asig) == (inputs(asig) Un outputs(asig))"
    4.36 +
    4.37 +is_asig_def
    4.38 +  "is_asig(triple) ==            
    4.39 +     ((inputs(triple) Int outputs(triple) = {})    & 
    4.40 +      (outputs(triple) Int internals(triple) = {}) & 
    4.41 +      (inputs(triple) Int internals(triple) = {}))"
    4.42 +
    4.43 +
    4.44 +mk_ext_asig_def
    4.45 +  "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
    4.46 +
    4.47 +
    4.48 +end 
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Wed Apr 30 11:20:15 1997 +0200
     5.3 @@ -0,0 +1,283 @@
     5.4 +(*  Title:      HOLCF/IOA/meta_theory/Automata.ML
     5.5 +    ID:         $$
     5.6 +    Author:     Olaf Mueller, Tobias Nipkow, Konrad Slind
     5.7 +    Copyright   1994, 1996  TU Muenchen
     5.8 +
     5.9 +The I/O automata of Lynch and Tuttle.
    5.10 +*)
    5.11 +
    5.12 +(* Has been removed from HOL-simpset, who knows why? *)
    5.13 +Addsimps [Let_def];
    5.14 +
    5.15 +open reachable;
    5.16 +
    5.17 +val ioa_projections = [asig_of_def, starts_of_def, trans_of_def];
    5.18 +
    5.19 +(* ----------------------------------------------------------------------------------- *)
    5.20 +
    5.21 +section "asig_of, starts_of, trans_of";
    5.22 +
    5.23 +
    5.24 +goal thy
    5.25 +"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z";
    5.26 +  by (simp_tac (!simpset addsimps ioa_projections) 1);
    5.27 +qed "ioa_triple_proj";
    5.28 +
    5.29 +goalw thy [ioa_def,state_trans_def,actions_def, is_asig_def]
    5.30 +  "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:act A";
    5.31 +  by (REPEAT(etac conjE 1));
    5.32 +  by (EVERY1[etac allE, etac impE, atac]);
    5.33 +  by (Asm_full_simp_tac 1);
    5.34 +qed "trans_in_actions";
    5.35 +
    5.36 +goal thy
    5.37 +"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
    5.38 +  by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
    5.39 +qed "starts_of_par";
    5.40 +
    5.41 +
    5.42 +(* ----------------------------------------------------------------------------------- *)
    5.43 +
    5.44 +section "actions and par";
    5.45 +
    5.46 +
    5.47 +goal thy 
    5.48 +"actions(asig_comp a b) = actions(a) Un actions(b)";
    5.49 +  by(simp_tac (!simpset addsimps
    5.50 +               ([actions_def,asig_comp_def]@asig_projections)) 1);
    5.51 +  by (fast_tac (set_cs addSIs [equalityI]) 1);
    5.52 +qed "actions_asig_comp";
    5.53 +
    5.54 +
    5.55 +goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
    5.56 +  by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
    5.57 +qed "asig_of_par";
    5.58 +
    5.59 +
    5.60 +goal thy "ext (A1||A2) =    \
    5.61 +\  (ext A1) Un (ext A2)";
    5.62 +by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def,
    5.63 +      asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
    5.64 +by (rtac set_ext 1); 
    5.65 +by (fast_tac set_cs 1);
    5.66 +qed"externals_of_par"; 
    5.67 +
    5.68 +goal thy "act (A1||A2) =    \
    5.69 +\  (act A1) Un (act A2)";
    5.70 +by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
    5.71 +      asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
    5.72 +by (rtac set_ext 1); 
    5.73 +by (fast_tac set_cs 1);
    5.74 +qed"actions_of_par"; 
    5.75 +
    5.76 +
    5.77 +goal thy "inp (A1||A2) =\
    5.78 +\         ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))";
    5.79 +by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
    5.80 +      asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1);
    5.81 +qed"inputs_of_par";
    5.82 +  
    5.83 +goal thy "out (A1||A2) =\
    5.84 +\         (out A1) Un (out A2)";
    5.85 +by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
    5.86 +      asig_outputs_def,Un_def,set_diff_def]) 1);
    5.87 +qed"outputs_of_par";
    5.88 +
    5.89 +
    5.90 +(* ---------------------------------------------------------------------------------- *)
    5.91 +
    5.92 +section "actions and compatibility"; 
    5.93 +
    5.94 +goal thy"compat_ioas A B = compat_ioas B A";
    5.95 +by (asm_full_simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_commute]) 1);
    5.96 +auto();
    5.97 +qed"compat_commute";
    5.98 +
    5.99 +goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
   5.100 + "!! a. [| compat_ioas A1 A2; a:ext A1|] ==> a~:int A2";
   5.101 +by (Asm_full_simp_tac 1);
   5.102 +by (best_tac (set_cs addEs [equalityCE]) 1);
   5.103 +qed"ext1_is_not_int2";
   5.104 +
   5.105 +(* just commuting the previous one: better commute compat_ioas *)
   5.106 +goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
   5.107 + "!! a. [| compat_ioas A2 A1 ; a:ext A1|] ==> a~:int A2";
   5.108 +by (Asm_full_simp_tac 1);
   5.109 +by (best_tac (set_cs addEs [equalityCE]) 1);
   5.110 +qed"ext2_is_not_int1";
   5.111 +
   5.112 +bind_thm("ext1_ext2_is_not_act2",ext1_is_not_int2 RS int_and_ext_is_act);
   5.113 +bind_thm("ext1_ext2_is_not_act1",ext2_is_not_int1 RS int_and_ext_is_act);
   5.114 +
   5.115 +goalw thy  [externals_def,actions_def,compat_ioas_def,compat_asigs_def]
   5.116 + "!! x. [| compat_ioas A B; x:int A |] ==> x~:ext B";
   5.117 +by (Asm_full_simp_tac 1);
   5.118 +by (best_tac (set_cs addEs [equalityCE]) 1);
   5.119 +qed"intA_is_not_extB";
   5.120 +
   5.121 +goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def,is_asig_def,asig_of_def]
   5.122 +"!! a. [| compat_ioas A B; a:int A |] ==> a ~: act B";
   5.123 +by (Asm_full_simp_tac 1);
   5.124 +by (best_tac (set_cs addEs [equalityCE]) 1);
   5.125 +qed"intA_is_not_actB";
   5.126 +
   5.127 +
   5.128 +(* ---------------------------------------------------------------------------------- *)
   5.129 +
   5.130 +section "invariants";
   5.131 +
   5.132 +val [p1,p2] = goalw thy [invariant_def]
   5.133 +  "[| !!s. s:starts_of(A) ==> P(s);     \
   5.134 +\     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
   5.135 +\  ==> invariant A P";
   5.136 +by (rtac allI 1);
   5.137 +by (rtac impI 1);
   5.138 +by (res_inst_tac [("za","s")] reachable.induct 1);
   5.139 +by (atac 1);
   5.140 +by (etac p1 1);
   5.141 +by (eres_inst_tac [("s1","sa")] (p2 RS mp) 1);
   5.142 +by (REPEAT (atac 1));
   5.143 +qed"invariantI";
   5.144 +
   5.145 +
   5.146 +val [p1,p2] = goal thy
   5.147 + "[| !!s. s : starts_of(A) ==> P(s); \
   5.148 +\   !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t) \
   5.149 +\ |] ==> invariant A P";
   5.150 +  by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1);
   5.151 +qed "invariantI1";
   5.152 +
   5.153 +val [p1,p2] = goalw thy [invariant_def]
   5.154 +"[| invariant A P; reachable A s |] ==> P(s)";
   5.155 +   br(p2 RS (p1 RS spec RS mp))1;
   5.156 +qed "invariantE";
   5.157 +
   5.158 +(* ---------------------------------------------------------------------------------- *)
   5.159 +
   5.160 +section "restrict";
   5.161 +
   5.162 +
   5.163 +goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
   5.164 +\             trans_of(restrict ioa acts) = trans_of(ioa)";
   5.165 +by(simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
   5.166 +qed "cancel_restrict_a";
   5.167 +
   5.168 +goal thy "reachable (restrict ioa acts) s = reachable ioa s";
   5.169 +by (rtac iffI 1);
   5.170 +be reachable.induct 1;
   5.171 +by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1);
   5.172 +by (etac reachable_n 1);
   5.173 +by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
   5.174 +(* <--  *)
   5.175 +be reachable.induct 1;
   5.176 +by (rtac reachable_0 1);
   5.177 +by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
   5.178 +by (etac reachable_n 1);
   5.179 +by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
   5.180 +qed "cancel_restrict_b";
   5.181 +
   5.182 +goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
   5.183 +\             trans_of(restrict ioa acts) = trans_of(ioa) & \
   5.184 +\             reachable (restrict ioa acts) s = reachable ioa s";
   5.185 +by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b]) 1);
   5.186 +qed"cancel_restrict";
   5.187 +
   5.188 +(* ---------------------------------------------------------------------------------- *)
   5.189 +
   5.190 +section "rename";
   5.191 +
   5.192 +
   5.193 +
   5.194 +goal thy "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)";
   5.195 +by (asm_full_simp_tac (!simpset addsimps [Let_def,rename_def,trans_of_def]) 1);
   5.196 +qed"trans_rename";
   5.197 +
   5.198 +
   5.199 +goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
   5.200 +be reachable.induct 1;
   5.201 +br reachable_0 1;
   5.202 +by(asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1);
   5.203 +bd trans_rename 1;
   5.204 +be exE 1;
   5.205 +be conjE 1;
   5.206 +be reachable_n 1;
   5.207 +ba 1;
   5.208 +qed"reachable_rename";
   5.209 +
   5.210 +
   5.211 +
   5.212 +(* ---------------------------------------------------------------------------------- *)
   5.213 +
   5.214 +section "trans_of(A||B)";
   5.215 +
   5.216 +
   5.217 +goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \
   5.218 +\             ==> (fst s,a,fst t):trans_of A";
   5.219 +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
   5.220 +qed"trans_A_proj";
   5.221 +
   5.222 +goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \
   5.223 +\             ==> (snd s,a,snd t):trans_of B";
   5.224 +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
   5.225 +qed"trans_B_proj";
   5.226 +
   5.227 +goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\
   5.228 +\             ==> fst s = fst t";
   5.229 +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
   5.230 +qed"trans_A_proj2";
   5.231 +
   5.232 +goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\
   5.233 +\             ==> snd s = snd t";
   5.234 +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
   5.235 +qed"trans_B_proj2";
   5.236 +
   5.237 +goal thy "!!A.(s,a,t):trans_of (A||B) \
   5.238 +\              ==> a :act A | a :act B";
   5.239 +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
   5.240 +qed"trans_AB_proj";
   5.241 +
   5.242 +goal thy "!!A. [|a:act A;a:act B;\
   5.243 +\      (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]\
   5.244 +\  ==> (s,a,t):trans_of (A||B)";
   5.245 +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
   5.246 +qed"trans_AB";
   5.247 +
   5.248 +goal thy "!!A. [|a:act A;a~:act B;\
   5.249 +\      (fst s,a,fst t):trans_of A;snd s=snd t|]\
   5.250 +\  ==> (s,a,t):trans_of (A||B)";
   5.251 +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
   5.252 +qed"trans_A_notB";
   5.253 +
   5.254 +goal thy "!!A. [|a~:act A;a:act B;\
   5.255 +\      (snd s,a,snd t):trans_of B;fst s=fst t|]\
   5.256 +\  ==> (s,a,t):trans_of (A||B)";
   5.257 +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1);
   5.258 +qed"trans_notA_B";
   5.259 +
   5.260 +val trans_of_defs1 = [trans_AB,trans_A_notB,trans_notA_B];
   5.261 +val trans_of_defs2 = [trans_A_proj,trans_B_proj,trans_A_proj2,
   5.262 +                      trans_B_proj2,trans_AB_proj];
   5.263 +
   5.264 +
   5.265 +goal thy 
   5.266 +"(s,a,t) : trans_of(A || B || C || D) =                                      \
   5.267 +\ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |  \
   5.268 +\   a:actions(asig_of(D))) &                                                 \
   5.269 +\  (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)              \
   5.270 +\   else fst t=fst s) &                                                      \
   5.271 +\  (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)    \
   5.272 +\   else fst(snd(t))=fst(snd(s))) &                                          \
   5.273 +\  (if a:actions(asig_of(C)) then                                            \
   5.274 +\     (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)                      \
   5.275 +\   else fst(snd(snd(t)))=fst(snd(snd(s)))) &                                \
   5.276 +\  (if a:actions(asig_of(D)) then                                            \
   5.277 +\     (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                      \
   5.278 +\   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
   5.279 +
   5.280 +  by(simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
   5.281 +                            ioa_projections)
   5.282 +                  setloop (split_tac [expand_if])) 1);
   5.283 +qed "trans_of_par4";
   5.284 +
   5.285 +
   5.286 +
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Wed Apr 30 11:20:15 1997 +0200
     6.3 @@ -0,0 +1,162 @@
     6.4 +(*  Title:      HOLCF/IOA/meta_theory/Automata.thy
     6.5 +    ID:        
     6.6 +    Author:     Olaf M"uller, Konrad Slind, Tobias Nipkow
     6.7 +    Copyright   1995, 1996  TU Muenchen
     6.8 +
     6.9 +The I/O automata of Lynch and Tuttle in HOLCF.
    6.10 +*)   
    6.11 +
    6.12 +		       
    6.13 +Automata = Option + Asig +  
    6.14 +
    6.15 +default term
    6.16 + 
    6.17 +types
    6.18 +   ('a,'s)transition       =    "'s * 'a * 's"
    6.19 +   ('a,'s)ioa              =    "'a signature * 's set * ('a,'s)transition set"
    6.20 +
    6.21 +consts
    6.22 + 
    6.23 +  (* IO automata *)
    6.24 +  state_trans::"['a signature, ('a,'s)transition set] => bool"
    6.25 +  asig_of    ::"('a,'s)ioa => 'a signature"
    6.26 +  starts_of  ::"('a,'s)ioa => 's set"
    6.27 +  trans_of   ::"('a,'s)ioa => ('a,'s)transition set"
    6.28 +  IOA	     ::"('a,'s)ioa => bool"
    6.29 +
    6.30 +  (* reachability and invariants *)
    6.31 +  reachable     :: "('a,'s)ioa => 's set"
    6.32 +  invariant     :: "[('a,'s)ioa, 's=>bool] => bool"
    6.33 +
    6.34 +  (* binary composition of action signatures and automata *)
    6.35 +  compat_asigs ::"['a signature, 'a signature] => bool"
    6.36 +  asig_comp    ::"['a signature, 'a signature] => 'a signature"
    6.37 +  compat_ioas  ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
    6.38 +  "||"         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr 10)
    6.39 +
    6.40 +  (* hiding *)
    6.41 +  restrict_asig :: "['a signature, 'a set] => 'a signature"
    6.42 +  restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
    6.43 +
    6.44 +  (* renaming *)
    6.45 +  rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
    6.46 +
    6.47 +
    6.48 +syntax 
    6.49 +
    6.50 +  "_trans_of"  :: "'s => 'a => ('a,'s)ioa => 's => bool"  ("_ -_--_-> _" [81,81,81,81] 100)
    6.51 +  "reachable"  :: "[('a,'s)ioa, 's] => bool"
    6.52 +  "act"        :: "('a,'s)ioa => 'a set"
    6.53 +  "ext"        :: "('a,'s)ioa => 'a set"
    6.54 +  "int"        :: "('a,'s)ioa => 'a set"
    6.55 +  "inp"        :: "('a,'s)ioa => 'a set"
    6.56 +  "out"        :: "('a,'s)ioa => 'a set"
    6.57 +
    6.58 +
    6.59 +syntax (symbols)
    6.60 +
    6.61 +  "_trans_of"  :: "'s => 'a => ('a,'s)ioa => 's => bool"  
    6.62 +                  ("_ \\<midarrow>_\\<midarrow>_\\<midarrow>\\<rightarrow> _" [81,81,81,81] 100)
    6.63 +  "op ||"         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "\\<parallel>" 10)
    6.64 +
    6.65 +
    6.66 +inductive "reachable C" 
    6.67 +   intrs  
    6.68 +    reachable_0  "s:(starts_of C) ==> s : reachable C"
    6.69 +    reachable_n  "[|s:reachable C; (s,a,t):trans_of C|] ==> t:reachable C"
    6.70 +
    6.71 +
    6.72 +translations
    6.73 +  "s -a--A-> t"   == "(s,a,t):trans_of A"
    6.74 +  "reachable A s" == "s:reachable A"
    6.75 +  "act A"         == "actions (asig_of A)"
    6.76 +  "ext A"         == "externals (asig_of A)"
    6.77 +  "int A"         == "internals (asig_of A)"
    6.78 +  "inp A"         == "inputs (asig_of A)"
    6.79 +  "out A"         == "outputs (asig_of A)"
    6.80 +
    6.81 +
    6.82 +defs
    6.83 +
    6.84 +(* --------------------------------- IOA ---------------------------------*)
    6.85 +
    6.86 +state_trans_def
    6.87 +  "state_trans asig R == 
    6.88 +    (!triple. triple:R --> fst(snd(triple)):actions(asig)) & 
    6.89 +    (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
    6.90 +
    6.91 +
    6.92 +asig_of_def   "asig_of == fst"
    6.93 +starts_of_def "starts_of == (fst o snd)"
    6.94 +trans_of_def  "trans_of == (snd o snd)"
    6.95 +
    6.96 +ioa_def
    6.97 +  "IOA(ioa) == (is_asig(asig_of(ioa))      &                            
    6.98 +                (~ starts_of(ioa) = {})    &                            
    6.99 +               state_trans (asig_of ioa) (trans_of ioa))"
   6.100 +
   6.101 +
   6.102 +invariant_def "invariant A P == (!s. reachable A s --> P(s))"
   6.103 +
   6.104 +
   6.105 +(* ------------------------- parallel composition --------------------------*)
   6.106 +
   6.107 +compat_asigs_def
   6.108 +  "compat_asigs a1 a2 ==                                                
   6.109 +  (((outputs(a1) Int outputs(a2)) = {}) &                              
   6.110 +   ((internals(a1) Int actions(a2)) = {}) &                            
   6.111 +   ((internals(a2) Int actions(a1)) = {}))"
   6.112 +
   6.113 +
   6.114 +compat_ioas_def
   6.115 +  "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))"
   6.116 +
   6.117 +
   6.118 +asig_comp_def
   6.119 +  "asig_comp a1 a2 ==                                                   
   6.120 +     (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),      
   6.121 +       (outputs(a1) Un outputs(a2)),                                   
   6.122 +       (internals(a1) Un internals(a2))))"
   6.123 +
   6.124 +
   6.125 +par_def
   6.126 +  "(ioa1 || ioa2) ==                                                    
   6.127 +      (asig_comp (asig_of ioa1) (asig_of ioa2),                        
   6.128 +       {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},        
   6.129 +       {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))        
   6.130 +            in (a:act ioa1 | a:act ioa2) & 
   6.131 +               (if a:act ioa1 then                       
   6.132 +                  (fst(s),a,fst(t)):trans_of(ioa1)                     
   6.133 +                else fst(t) = fst(s))                                  
   6.134 +               &                                                       
   6.135 +               (if a:act ioa2 then                       
   6.136 +                  (snd(s),a,snd(t)):trans_of(ioa2)                     
   6.137 +                else snd(t) = snd(s))})"
   6.138 +
   6.139 +(* ------------------------ hiding -------------------------------------------- *)
   6.140 +
   6.141 +restrict_asig_def
   6.142 +  "restrict_asig asig actns ==                                          
   6.143 +    (inputs(asig) Int actns, outputs(asig) Int actns,                  
   6.144 +     internals(asig) Un (externals(asig) - actns))"
   6.145 +
   6.146 +
   6.147 +restrict_def
   6.148 +  "restrict ioa actns ==                                               
   6.149 +    (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
   6.150 +
   6.151 +(* ------------------------- renaming ------------------------------------------- *)
   6.152 +  
   6.153 +rename_def 
   6.154 +"rename ioa ren ==  
   6.155 +  (({b. ? x. Some(x)= ren(b) & x : inp ioa},         
   6.156 +    {b. ? x. Some(x)= ren(b) & x : out ioa},        
   6.157 +    {b. ? x. Some(x)= ren(b) & x : int ioa}),     
   6.158 +              starts_of(ioa)   ,                                            
   6.159 +   {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))    
   6.160 +        in                                                      
   6.161 +        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
   6.162 +
   6.163 +
   6.164 +end
   6.165 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Wed Apr 30 11:20:15 1997 +0200
     7.3 @@ -0,0 +1,262 @@
     7.4 +(*  Title:      HOLCF/IOA/meta_theory/CompoExecs.ML
     7.5 +    ID:        
     7.6 +    Author:     Olaf M"uller
     7.7 +    Copyright   1996  TU Muenchen
     7.8 +
     7.9 +Compositionality on Execution level.
    7.10 +*)  
    7.11 +
    7.12 +Delsimps (ex_simps @ all_simps); 
    7.13 +Delsimps [split_paired_All];
    7.14 +
    7.15 +(* ----------------------------------------------------------------------------------- *)
    7.16 +
    7.17 +
    7.18 +section "recursive equations of operators";
    7.19 +
    7.20 +
    7.21 +(* ---------------------------------------------------------------- *)
    7.22 +(*                               ProjA2                             *)
    7.23 +(* ---------------------------------------------------------------- *)
    7.24 +
    7.25 +
    7.26 +goal thy  "ProjA2`UU = UU";
    7.27 +by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
    7.28 +qed"ProjA2_UU";
    7.29 +
    7.30 +goal thy  "ProjA2`nil = nil";
    7.31 +by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
    7.32 +qed"ProjA2_nil";
    7.33 +
    7.34 +goal thy "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs";
    7.35 +by (simp_tac (!simpset addsimps [ProjA2_def]) 1);
    7.36 +qed"ProjA2_cons";
    7.37 +
    7.38 +
    7.39 +(* ---------------------------------------------------------------- *)
    7.40 +(*                               ProjB2                             *)
    7.41 +(* ---------------------------------------------------------------- *)
    7.42 +
    7.43 +
    7.44 +goal thy  "ProjB2`UU = UU";
    7.45 +by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
    7.46 +qed"ProjB2_UU";
    7.47 +
    7.48 +goal thy  "ProjB2`nil = nil";
    7.49 +by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
    7.50 +qed"ProjB2_nil";
    7.51 +
    7.52 +goal thy "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs";
    7.53 +by (simp_tac (!simpset addsimps [ProjB2_def]) 1);
    7.54 +qed"ProjB2_cons";
    7.55 +
    7.56 +
    7.57 +
    7.58 +(* ---------------------------------------------------------------- *)
    7.59 +(*                             Filter_ex2                           *)
    7.60 +(* ---------------------------------------------------------------- *)
    7.61 +
    7.62 +
    7.63 +goal thy "Filter_ex2 A`UU=UU";
    7.64 +by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
    7.65 +qed"Filter_ex2_UU";
    7.66 +
    7.67 +goal thy "Filter_ex2 A`nil=nil";
    7.68 +by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
    7.69 +qed"Filter_ex2_nil";
    7.70 +
    7.71 +goal thy "Filter_ex2 A`(at >> xs) =    \
    7.72 +\            (if (fst at:act A)    \       
    7.73 +\                 then at >> (Filter_ex2 A`xs) \   
    7.74 +\                 else        Filter_ex2 A`xs)";
    7.75 +
    7.76 +by (asm_full_simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
    7.77 +qed"Filter_ex2_cons";
    7.78 +
    7.79 +
    7.80 +(* ---------------------------------------------------------------- *)
    7.81 +(*                             stutter2                             *)
    7.82 +(* ---------------------------------------------------------------- *)
    7.83 +
    7.84 +
    7.85 +goal thy "stutter2 A = (LAM ex. (%s. case ex of \
    7.86 +\      nil => TT \
    7.87 +\    | x##xs => (flift1 \ 
    7.88 +\            (%p.(If Def ((fst p)~:act A) \
    7.89 +\                 then Def (s=(snd p)) \
    7.90 +\                 else TT fi) \
    7.91 +\                andalso (stutter2 A`xs) (snd p))  \
    7.92 +\             `x) \
    7.93 +\           ))";
    7.94 +by (rtac trans 1);
    7.95 +br fix_eq2 1;
    7.96 +br stutter2_def 1;
    7.97 +br beta_cfun 1;
    7.98 +by (simp_tac (!simpset addsimps [flift1_def]) 1);
    7.99 +qed"stutter2_unfold";
   7.100 +
   7.101 +goal thy "(stutter2 A`UU) s=UU";
   7.102 +by (stac stutter2_unfold 1);
   7.103 +by (Simp_tac 1);
   7.104 +qed"stutter2_UU";
   7.105 +
   7.106 +goal thy "(stutter2 A`nil) s = TT";
   7.107 +by (stac stutter2_unfold 1);
   7.108 +by (Simp_tac 1);
   7.109 +qed"stutter2_nil";
   7.110 +
   7.111 +goal thy "(stutter2 A`(at>>xs)) s = \
   7.112 +\              ((if (fst at)~:act A then Def (s=snd at) else TT) \
   7.113 +\                andalso (stutter2 A`xs) (snd at))"; 
   7.114 +br trans 1;
   7.115 +by (stac stutter2_unfold 1);
   7.116 +by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1);
   7.117 +by (Simp_tac 1);
   7.118 +qed"stutter2_cons";
   7.119 +
   7.120 +
   7.121 +Addsimps [stutter2_UU,stutter2_nil,stutter2_cons];
   7.122 +
   7.123 +
   7.124 +(* ---------------------------------------------------------------- *)
   7.125 +(*                             stutter                              *)
   7.126 +(* ---------------------------------------------------------------- *)
   7.127 +
   7.128 +goal thy "stutter A (s, UU)";
   7.129 +by (simp_tac (!simpset addsimps [stutter_def]) 1);
   7.130 +qed"stutter_UU";
   7.131 +
   7.132 +goal thy "stutter A (s, nil)";
   7.133 +by (simp_tac (!simpset addsimps [stutter_def]) 1);
   7.134 +qed"stutter_nil";
   7.135 +
   7.136 +goal thy "stutter A (s, (a,t)>>ex) = \
   7.137 +\     ((a~:act A --> (s=t)) & stutter A (t,ex))";
   7.138 +by (simp_tac (!simpset addsimps [stutter_def] 
   7.139 +                       setloop (split_tac [expand_if]) ) 1);
   7.140 +qed"stutter_cons";
   7.141 +
   7.142 +(* ----------------------------------------------------------------------------------- *)
   7.143 +
   7.144 +Delsimps [stutter2_UU,stutter2_nil,stutter2_cons];
   7.145 +
   7.146 +val compoex_simps = [ProjA2_UU,ProjA2_nil,ProjA2_cons,
   7.147 +                     ProjB2_UU,ProjB2_nil,ProjB2_cons,
   7.148 +                     Filter_ex2_UU,Filter_ex2_nil,Filter_ex2_cons,
   7.149 +                     stutter_UU,stutter_nil,stutter_cons];
   7.150 +
   7.151 +Addsimps compoex_simps;
   7.152 +
   7.153 +
   7.154 +
   7.155 +(* ------------------------------------------------------------------ *)
   7.156 +(*                      The following lemmata aim for                 *)
   7.157 +(*             COMPOSITIONALITY   on    EXECUTION     Level           *)
   7.158 +(* ------------------------------------------------------------------ *)
   7.159 +
   7.160 +
   7.161 +(* --------------------------------------------------------------------- *)
   7.162 +(*  Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B    *)
   7.163 +(* --------------------------------------------------------------------- *)
   7.164 +
   7.165 +goal thy "!s. is_execution_fragment (A||B) (s,xs) \
   7.166 +\      -->  is_execution_fragment A (fst s, Filter_ex2 A`(ProjA2`xs)) &\
   7.167 +\           is_execution_fragment B (snd s, Filter_ex2 B`(ProjB2`xs))";
   7.168 +
   7.169 +by (pair_induct_tac "xs" [is_execution_fragment_def] 1);
   7.170 +(* main case *)
   7.171 +ren "ss a t" 1;
   7.172 +by (safe_tac set_cs);
   7.173 +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2
   7.174 +                       setloop (split_tac [expand_if])) 1));
   7.175 +qed"lemma_1_1a";
   7.176 +
   7.177 +
   7.178 +(* --------------------------------------------------------------------- *)
   7.179 +(*  Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections       *)
   7.180 +(* --------------------------------------------------------------------- *)
   7.181 +
   7.182 +goal thy "!s. is_execution_fragment (A||B) (s,xs) \
   7.183 +\      --> stutter A (fst s,ProjA2`xs)  &\
   7.184 +\          stutter B (snd s,ProjB2`xs)"; 
   7.185 +
   7.186 +by (pair_induct_tac "xs" [stutter_def,is_execution_fragment_def] 1);
   7.187 +(* main case *)
   7.188 +by (safe_tac set_cs);
   7.189 +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2
   7.190 +                 setloop (split_tac [expand_if])) 1));
   7.191 +qed"lemma_1_1b";
   7.192 +
   7.193 +
   7.194 +(* --------------------------------------------------------------------- *)
   7.195 +(*  Lemma_1_1c : Executions of A||B have only  A- or B-actions           *)
   7.196 +(* --------------------------------------------------------------------- *)
   7.197 +
   7.198 +goal thy "!s. (is_execution_fragment (A||B) (s,xs) \
   7.199 +\  --> Forall (%x.fst x:act (A||B)) xs)";
   7.200 +
   7.201 +by (pair_induct_tac "xs" [Forall_def,sforall_def,is_execution_fragment_def] 1);
   7.202 +(* main case *)
   7.203 +by (safe_tac set_cs);
   7.204 +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @ 
   7.205 +                                [actions_asig_comp,asig_of_par]) 1));
   7.206 +qed"lemma_1_1c";
   7.207 +
   7.208 +
   7.209 +(* ----------------------------------------------------------------------- *)
   7.210 +(*  Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B)   *)
   7.211 +(* ----------------------------------------------------------------------- *)
   7.212 +
   7.213 +goal thy 
   7.214 +"!s. is_execution_fragment A (fst s,Filter_ex2 A`(ProjA2`xs)) &\
   7.215 +\    is_execution_fragment B (snd s,Filter_ex2 B`(ProjB2`xs)) &\
   7.216 +\    stutter A (fst s,(ProjA2`xs)) & \
   7.217 +\    stutter B (snd s,(ProjB2`xs)) & \
   7.218 +\    Forall (%x.fst x:act (A||B)) xs \
   7.219 +\    --> is_execution_fragment (A||B) (s,xs)";
   7.220 +
   7.221 +by (pair_induct_tac "xs" [Forall_def,sforall_def,
   7.222 +         is_execution_fragment_def, stutter_def] 1);
   7.223 +(* main case *)
   7.224 +by (rtac allI 1); 
   7.225 +ren "ss a t s" 1;
   7.226 +by (asm_full_simp_tac (!simpset addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par]
   7.227 +               setloop (split_tac [expand_if])) 1);
   7.228 +by (safe_tac set_cs);
   7.229 +(* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *)
   7.230 +by (rotate_tac ~4 1);
   7.231 +by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   7.232 +by (rotate_tac ~4 1);
   7.233 +by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   7.234 +qed"lemma_1_2";
   7.235 +
   7.236 +
   7.237 +(* ------------------------------------------------------------------ *)
   7.238 +(*           COMPOSITIONALITY   on    EXECUTION     Level             *)
   7.239 +(*                          Main Theorem                              *)
   7.240 +(* ------------------------------------------------------------------ *)
   7.241 +
   7.242 +
   7.243 +goal thy 
   7.244 +"ex:executions(A||B) =\
   7.245 +\(Filter_ex A (ProjA ex) : executions A &\
   7.246 +\ Filter_ex B (ProjB ex) : executions B &\
   7.247 +\ stutter A (ProjA ex) & stutter B (ProjB ex) &\
   7.248 +\ Forall (%x.fst x:act (A||B)) (snd ex))";
   7.249 +
   7.250 +by (simp_tac (!simpset addsimps [executions_def,ProjB_def,
   7.251 +                                 Filter_ex_def,ProjA_def,starts_of_par]) 1);
   7.252 +by (pair_tac "ex" 1);
   7.253 +by (rtac iffI 1);
   7.254 +(* ==>  *)
   7.255 +by (REPEAT (etac conjE 1));
   7.256 +by (asm_full_simp_tac (!simpset addsimps [lemma_1_1a RS spec RS mp,
   7.257 +               lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1);
   7.258 +(* <==  *)
   7.259 +by (REPEAT (etac conjE 1));
   7.260 +by (asm_full_simp_tac (!simpset addsimps [lemma_1_2 RS spec RS mp]) 1);
   7.261 +qed"compositionality_ex";
   7.262 +
   7.263 +
   7.264 +
   7.265 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Apr 30 11:20:15 1997 +0200
     8.3 @@ -0,0 +1,65 @@
     8.4 +(*  Title:      HOLCF/IOA/meta_theory/CompoExecs.thy
     8.5 +    ID:        
     8.6 +    Author:     Olaf M"uller
     8.7 +    Copyright   1996  TU Muenchen
     8.8 +
     8.9 +Compositionality on Execution level.
    8.10 +*)  
    8.11 +
    8.12 +CompoExecs = Traces + 
    8.13 +
    8.14 +
    8.15 +consts 
    8.16 +
    8.17 + ProjA      ::"('a,'s * 't)execution => ('a,'s)execution"
    8.18 + ProjA2     ::"('a,'s * 't)pairs     -> ('a,'s)pairs"
    8.19 + ProjB      ::"('a,'s * 't)execution => ('a,'t)execution"
    8.20 + ProjB2     ::"('a,'s * 't)pairs     -> ('a,'t)pairs"
    8.21 + Filter_ex  ::"('a,'s)ioa => ('a,'s)execution => ('a,'s)execution"
    8.22 + Filter_ex2 ::"('a,'s)ioa => ('a,'s)pairs     -> ('a,'s)pairs" 
    8.23 + stutter    ::"('a,'s)ioa => ('a,'s)execution => bool" 
    8.24 + stutter2   ::"('a,'s)ioa => ('a,'s)pairs     -> ('s => tr)"
    8.25 +
    8.26 +
    8.27 +defs 
    8.28 +
    8.29 +
    8.30 +ProjA_def
    8.31 + "ProjA ex == (fst (fst ex), ProjA2`(snd ex))" 
    8.32 +
    8.33 +ProjB_def
    8.34 + "ProjB ex == (snd (fst ex), ProjB2`(snd ex))" 
    8.35 +
    8.36 +
    8.37 +ProjA2_def
    8.38 +  "ProjA2 == Map (%x.(fst x,fst(snd x)))"
    8.39 +
    8.40 +ProjB2_def
    8.41 +  "ProjB2 == Map (%x.(fst x,snd(snd x)))"
    8.42 + 
    8.43 +
    8.44 +Filter_ex_def
    8.45 +  "Filter_ex A ex == (fst ex,Filter_ex2 A`(snd ex))"
    8.46 +
    8.47 +
    8.48 +Filter_ex2_def
    8.49 +  "Filter_ex2 A ==  Filter (%x.fst x:act A)"
    8.50 +
    8.51 +stutter_def
    8.52 +  "stutter A ex == ((stutter2 A`(snd ex)) (fst ex) ~= FF)"
    8.53 +
    8.54 +stutter2_def
    8.55 +  "stutter2 A ==(fix`(LAM h ex. (%s. case ex of 
    8.56 +      nil => TT
    8.57 +    | x##xs => (flift1 
    8.58 +            (%p.(If Def ((fst p)~:act A)
    8.59 +                 then Def (s=(snd p)) 
    8.60 +                 else TT fi)
    8.61 +                andalso (h`xs) (snd p)) 
    8.62 +             `x)
    8.63 +   )))" 
    8.64 +
    8.65 +
    8.66 +
    8.67 +
    8.68 +end
    8.69 \ No newline at end of file
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed Apr 30 11:20:15 1997 +0200
     9.3 @@ -0,0 +1,503 @@
     9.4 +(*  Title:      HOLCF/IOA/meta_theory/CompoScheds.ML
     9.5 +    ID:        
     9.6 +    Author:     Olaf M"uller
     9.7 +    Copyright   1996  TU Muenchen
     9.8 +
     9.9 +Compositionality on Schedule level.
    9.10 +*) 
    9.11 +
    9.12 +
    9.13 +
    9.14 +Addsimps [surjective_pairing RS sym];
    9.15 +
    9.16 +
    9.17 +
    9.18 +(* ------------------------------------------------------------------------------- *)
    9.19 +
    9.20 +section "mkex rewrite rules";
    9.21 +
    9.22 +(* ---------------------------------------------------------------- *)
    9.23 +(*                             mkex2                                *)
    9.24 +(* ---------------------------------------------------------------- *)
    9.25 +
    9.26 +
    9.27 +bind_thm ("mkex2_unfold", fix_prover2 thy mkex2_def 
    9.28 +"mkex2 A B = (LAM sch exA exB. (%s t. case sch of  \
    9.29 +\      nil => nil \
    9.30 +\   | x##xs => \
    9.31 +\     (case x of  \
    9.32 +\       Undef => UU   \
    9.33 +\     | Def y =>  \
    9.34 +\        (if y:act A then \
    9.35 +\            (if y:act B then \
    9.36 +\               (case HD`exA of \
    9.37 +\                  Undef => UU \
    9.38 +\                | Def a => (case HD`exB of \
    9.39 +\                             Undef => UU \
    9.40 +\                           | Def b => \
    9.41 +\                  (y,(snd a,snd b))>>  \
    9.42 +\                    (mkex2 A B`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))  \
    9.43 +\             else   \
    9.44 +\               (case HD`exA of   \
    9.45 +\                  Undef => UU  \
    9.46 +\                | Def a => \
    9.47 +\                  (y,(snd a,t))>>(mkex2 A B`xs`(TL`exA)`exB) (snd a) t)  \
    9.48 +\             )  \       
    9.49 +\         else   \
    9.50 +\            (if y:act B then \
    9.51 +\               (case HD`exB of  \
    9.52 +\                  Undef => UU  \
    9.53 +\                | Def b =>  \
    9.54 +\                  (y,(s,snd b))>>(mkex2 A B`xs`exA`(TL`exB)) s (snd b))  \
    9.55 +\            else  \
    9.56 +\              UU  \
    9.57 +\            )  \
    9.58 +\        )  \
    9.59 +\      )))");
    9.60 +
    9.61 +
    9.62 +goal thy "(mkex2 A B`UU`exA`exB) s t = UU";
    9.63 +by (stac mkex2_unfold 1);
    9.64 +by (Simp_tac 1);
    9.65 +qed"mkex2_UU";
    9.66 +
    9.67 +goal thy "(mkex2 A B`nil`exA`exB) s t= nil";
    9.68 +by (stac mkex2_unfold 1);
    9.69 +by (Simp_tac 1);
    9.70 +qed"mkex2_nil";
    9.71 +
    9.72 +goal thy "!!x.[| x:act A; x~:act B; HD`exA=Def a|] \
    9.73 +\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =   \
    9.74 +\       (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
    9.75 +br trans 1;
    9.76 +by (stac mkex2_unfold 1);
    9.77 +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
    9.78 +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
    9.79 +qed"mkex2_cons_1";
    9.80 +
    9.81 +goal thy "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
    9.82 +\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
    9.83 +\       (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
    9.84 +br trans 1;
    9.85 +by (stac mkex2_unfold 1);
    9.86 +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
    9.87 +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
    9.88 +qed"mkex2_cons_2";
    9.89 +
    9.90 +goal thy "!!x.[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
    9.91 +\   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =  \
    9.92 +\        (x,snd a,snd b) >> \
    9.93 +\           (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
    9.94 +br trans 1;
    9.95 +by (stac mkex2_unfold 1);
    9.96 +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
    9.97 +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
    9.98 +qed"mkex2_cons_3";
    9.99 +
   9.100 +Addsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
   9.101 +
   9.102 +
   9.103 +(* ---------------------------------------------------------------- *)
   9.104 +(*                             mkex                                 *)
   9.105 +(* ---------------------------------------------------------------- *)
   9.106 +
   9.107 +goal thy "mkex A B UU  (s,exA) (t,exB) = ((s,t),UU)";
   9.108 +by (simp_tac (!simpset addsimps [mkex_def]) 1);
   9.109 +qed"mkex_UU";
   9.110 +
   9.111 +goal thy "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)";
   9.112 +by (simp_tac (!simpset addsimps [mkex_def]) 1);
   9.113 +qed"mkex_nil";
   9.114 +
   9.115 +goal thy "!!x.[| x:act A; x~:act B |] \
   9.116 +\   ==> mkex A B (x>>sch) (s,a>>exA) (t,exB)  =  \
   9.117 +\       ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))";
   9.118 +by (simp_tac (!simpset addsimps [mkex_def] 
   9.119 +                       setloop (split_tac [expand_if]) ) 1);
   9.120 +by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
   9.121 +auto();
   9.122 +qed"mkex_cons_1";
   9.123 +
   9.124 +goal thy "!!x.[| x~:act A; x:act B |] \
   9.125 +\   ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =  \ 
   9.126 +\       ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
   9.127 +by (simp_tac (!simpset addsimps [mkex_def] 
   9.128 +                       setloop (split_tac [expand_if]) ) 1);
   9.129 +by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
   9.130 +auto();
   9.131 +qed"mkex_cons_2";
   9.132 +
   9.133 +goal thy "!!x.[| x:act A; x:act B |]  \
   9.134 +\   ==>  mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
   9.135 +\        ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
   9.136 +by (simp_tac (!simpset addsimps [mkex_def] 
   9.137 +                       setloop (split_tac [expand_if]) ) 1);
   9.138 +by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
   9.139 +auto();
   9.140 +qed"mkex_cons_3";
   9.141 +
   9.142 +Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
   9.143 +
   9.144 +val composch_simps = [mkex_UU,mkex_nil,
   9.145 +                      mkex_cons_1,mkex_cons_2,mkex_cons_3];
   9.146 +
   9.147 +Addsimps composch_simps;
   9.148 +
   9.149 +
   9.150 +
   9.151 +(* ------------------------------------------------------------------ *)
   9.152 +(*                      The following lemmata aim for                 *)
   9.153 +(*             COMPOSITIONALITY   on    SCHEDULE     Level            *)
   9.154 +(* ------------------------------------------------------------------ *)
   9.155 +
   9.156 +(* ---------------------------------------------------------------------- *)
   9.157 +             section   "Lemmas for ==>";
   9.158 +(* ----------------------------------------------------------------------*)
   9.159 +
   9.160 +(* --------------------------------------------------------------------- *)
   9.161 +(*    Lemma_2_1 :  tfilter(ex) and filter_act are commutative            *)
   9.162 +(* --------------------------------------------------------------------- *)
   9.163 +
   9.164 +goalw thy [filter_act_def,Filter_ex2_def]
   9.165 +   "filter_act`(Filter_ex2 A`xs)=\
   9.166 +\   Filter (%a.a:act A)`(filter_act`xs)";
   9.167 +
   9.168 +by (simp_tac (!simpset addsimps [MapFilter,o_def]) 1);
   9.169 +qed"lemma_2_1a";
   9.170 +
   9.171 +
   9.172 +(* --------------------------------------------------------------------- *)
   9.173 +(*    Lemma_2_2 : State-projections do not affect filter_act             *)
   9.174 +(* --------------------------------------------------------------------- *)
   9.175 +
   9.176 +goal thy 
   9.177 +   "filter_act`(ProjA2`xs) =filter_act`xs &\
   9.178 +\   filter_act`(ProjB2`xs) =filter_act`xs";
   9.179 +
   9.180 +by (pair_induct_tac "xs" [] 1);
   9.181 +qed"lemma_2_1b";
   9.182 +
   9.183 +
   9.184 +(* --------------------------------------------------------------------- *)
   9.185 +(*             Schedules of A||B have only  A- or B-actions              *)
   9.186 +(* --------------------------------------------------------------------- *)
   9.187 +
   9.188 +(* FIX: very similar to lemma_1_1c, but it is not checking if every action element of 
   9.189 +   an ex is in A or B, but after projecting it onto the action schedule. Of course, this
   9.190 +   is the same proposition, but we cannot change this one, when then rather lemma_1_1c  *)
   9.191 +
   9.192 +goal thy "!s. is_execution_fragment (A||B) (s,xs) \
   9.193 +\  --> Forall (%x.x:act (A||B)) (filter_act`xs)";
   9.194 +
   9.195 +by (pair_induct_tac "xs" [is_execution_fragment_def,Forall_def,sforall_def] 1);
   9.196 +(* main case *)
   9.197 +by (safe_tac set_cs);
   9.198 +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @ 
   9.199 +                                [actions_asig_comp,asig_of_par]) 1));
   9.200 +qed"sch_actions_in_AorB";
   9.201 +
   9.202 +
   9.203 +(* --------------------------------------------------------------------------*)
   9.204 +                 section "Lemmas for <=="; 
   9.205 +(* ---------------------------------------------------------------------------*)
   9.206 +
   9.207 +(*---------------------------------------------------------------------------
   9.208 +    Filtering actions out of mkex(sch,exA,exB) yields the oracle sch
   9.209 +                             structural induction
   9.210 +  --------------------------------------------------------------------------- *)
   9.211 +
   9.212 +goal thy "! exA exB s t. \
   9.213 +\ Forall (%x.x:act (A||B)) sch  & \
   9.214 +\ Filter (%a.a:act A)`sch << filter_act`exA &\
   9.215 +\ Filter (%a.a:act B)`sch << filter_act`exB \
   9.216 +\ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch";
   9.217 +
   9.218 +by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1);
   9.219 +
   9.220 +(* main case *) 
   9.221 +(* splitting into 4 cases according to a:A, a:B *)
   9.222 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
   9.223 +by (safe_tac set_cs);
   9.224 +
   9.225 +(* Case y:A, y:B *)
   9.226 +by (Seq_case_simp_tac "exA" 1);
   9.227 +(* Case exA=UU, Case exA=nil*)
   9.228 +(* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA 
   9.229 +   is used! --> to generate a contradiction using  ~a>>ss<< UU(nil), using theorems 
   9.230 +   Cons_not_less_UU and Cons_not_less_nil  *)
   9.231 +by (Seq_case_simp_tac "exB" 1);
   9.232 +(* Case exA=a>>x, exB=b>>y *)
   9.233 +(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case, 
   9.234 +   as otherwise mkex_cons_3 would  not be rewritten without use of rotate_tac: then tactic 
   9.235 +   would not be generally applicable *)
   9.236 +by (Asm_full_simp_tac 1);
   9.237 +
   9.238 +(* Case y:A, y~:B *)
   9.239 +by (Seq_case_simp_tac "exB" 1);
   9.240 +by (Asm_full_simp_tac 1);
   9.241 +
   9.242 +(* Case y~:A, y:B *)
   9.243 +by (Seq_case_simp_tac "exA" 1);
   9.244 +by (Asm_full_simp_tac 1);
   9.245 +
   9.246 +(* Case y~:A, y~:B *)
   9.247 +by (asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp]) 1);
   9.248 +qed"Mapfst_mkex_is_sch";
   9.249 +
   9.250 +
   9.251 +(* generalizing the proof above to a tactic *)
   9.252 +
   9.253 +fun mkex_induct_tac sch exA exB = 
   9.254 +    EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def], 
   9.255 +           asm_full_simp_tac (!simpset setloop split_tac [expand_if]),
   9.256 +           SELECT_GOAL (safe_tac set_cs),
   9.257 +           Seq_case_simp_tac exA,
   9.258 +           Seq_case_simp_tac exB,
   9.259 +           Asm_full_simp_tac,
   9.260 +           Seq_case_simp_tac exB,
   9.261 +           Asm_full_simp_tac,
   9.262 +           Seq_case_simp_tac exA,
   9.263 +           Asm_full_simp_tac,
   9.264 +           asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp])
   9.265 +          ];
   9.266 +
   9.267 +
   9.268 +
   9.269 +(*---------------------------------------------------------------------------
   9.270 +               Projection of mkex(sch,exA,exB) onto A stutters on A
   9.271 +                             structural induction
   9.272 +  --------------------------------------------------------------------------- *)
   9.273 +
   9.274 +
   9.275 +goal thy "! exA exB s t. \
   9.276 +\ Forall (%x.x:act (A||B)) sch & \
   9.277 +\ Filter (%a.a:act A)`sch << filter_act`exA &\
   9.278 +\ Filter (%a.a:act B)`sch << filter_act`exB \
   9.279 +\ --> stutter A (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
   9.280 +
   9.281 +by (mkex_induct_tac "sch" "exA" "exB");
   9.282 +
   9.283 +qed"stutterA_mkex";
   9.284 +
   9.285 +
   9.286 +goal thy "!! sch.[|  \
   9.287 +\ Forall (%x.x:act (A||B)) sch ; \
   9.288 +\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
   9.289 +\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
   9.290 +\ ==> stutter A (ProjA (mkex A B sch exA exB))";
   9.291 +
   9.292 +by (cut_facts_tac [stutterA_mkex] 1);
   9.293 +by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1);
   9.294 +by (REPEAT (etac allE 1));
   9.295 +bd mp 1;
   9.296 +ba 2;
   9.297 +by (Asm_full_simp_tac 1);
   9.298 +qed"stutter_mkex_on_A";
   9.299 +
   9.300 +
   9.301 +(*---------------------------------------------------------------------------
   9.302 +               Projection of mkex(sch,exA,exB) onto B stutters on B
   9.303 +                             structural induction
   9.304 +  --------------------------------------------------------------------------- *)
   9.305 +
   9.306 +goal thy "! exA exB s t. \
   9.307 +\ Forall (%x.x:act (A||B)) sch & \
   9.308 +\ Filter (%a.a:act A)`sch << filter_act`exA &\
   9.309 +\ Filter (%a.a:act B)`sch << filter_act`exB \
   9.310 +\ --> stutter B (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
   9.311 +
   9.312 +by (mkex_induct_tac "sch" "exA" "exB");
   9.313 +
   9.314 +qed"stutterB_mkex";
   9.315 +
   9.316 +
   9.317 +goal thy "!! sch.[|  \
   9.318 +\ Forall (%x.x:act (A||B)) sch ; \
   9.319 +\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
   9.320 +\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
   9.321 +\ ==> stutter B (ProjB (mkex A B sch exA exB))";
   9.322 +
   9.323 +by (cut_facts_tac [stutterB_mkex] 1);
   9.324 +by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1);
   9.325 +by (REPEAT (etac allE 1));
   9.326 +bd mp 1;
   9.327 +ba 2;
   9.328 +by (Asm_full_simp_tac 1);
   9.329 +qed"stutter_mkex_on_B";
   9.330 +
   9.331 +
   9.332 +(*---------------------------------------------------------------------------
   9.333 +     Filter of mkex(sch,exA,exB) to A after projection onto A is exA 
   9.334 +        --  using zip`(proj1`exA)`(proj2`exA) instead of exA    --
   9.335 +        --           because of admissibility problems          --
   9.336 +                             structural induction
   9.337 +  --------------------------------------------------------------------------- *)
   9.338 +
   9.339 +goal thy "! exA exB s t. \
   9.340 +\ Forall (%x.x:act (A||B)) sch & \
   9.341 +\ Filter (%a.a:act A)`sch << filter_act`exA  &\
   9.342 +\ Filter (%a.a:act B)`sch << filter_act`exB \
   9.343 +\ --> Filter_ex2 A`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   9.344 +\     Zip`(Filter (%a.a:act A)`sch)`(Map snd`exA)";
   9.345 +
   9.346 +by (mkex_induct_tac "sch" "exA" "exB");
   9.347 +
   9.348 +qed"filter_mkex_is_exA_tmp";
   9.349 +
   9.350 +(*---------------------------------------------------------------------------
   9.351 +                      zip`(proj1`y)`(proj2`y) = y   (using the lift operations)
   9.352 +                    lemma for admissibility problems         
   9.353 +  --------------------------------------------------------------------------- *)
   9.354 +
   9.355 +goal thy  "Zip`(Map fst`y)`(Map snd`y) = y";
   9.356 +by (Seq_induct_tac "y" [] 1);
   9.357 +qed"Zip_Map_fst_snd";
   9.358 +
   9.359 +
   9.360 +(*---------------------------------------------------------------------------
   9.361 +      filter A`sch = proj1`ex   -->  zip`(filter A`sch)`(proj2`ex) = ex 
   9.362 +         lemma for eliminating non admissible equations in assumptions      
   9.363 +  --------------------------------------------------------------------------- *)
   9.364 +
   9.365 +goal thy "!! sch ex. \
   9.366 +\ Filter (%a.a:act AB)`sch = filter_act`ex  \
   9.367 +\ ==> ex = Zip`(Filter (%a.a:act AB)`sch)`(Map snd`ex)";
   9.368 +by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 1);
   9.369 +by (rtac (Zip_Map_fst_snd RS sym) 1);
   9.370 +qed"trick_against_eq_in_ass";
   9.371 +
   9.372 +(*---------------------------------------------------------------------------
   9.373 +     Filter of mkex(sch,exA,exB) to A after projection onto A is exA 
   9.374 +                       using the above trick
   9.375 +  --------------------------------------------------------------------------- *)
   9.376 +
   9.377 +
   9.378 +goal thy "!!sch exA exB.\
   9.379 +\ [| Forall (%a.a:act (A||B)) sch ; \
   9.380 +\ Filter (%a.a:act A)`sch = filter_act`(snd exA)  ;\
   9.381 +\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
   9.382 +\ ==> Filter_ex A (ProjA (mkex A B sch exA exB)) = exA";
   9.383 +by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
   9.384 +by (pair_tac "exA" 1);
   9.385 +by (pair_tac "exB" 1);
   9.386 +br conjI 1;
   9.387 +by (simp_tac (!simpset addsimps [mkex_def]) 1);
   9.388 +by (stac trick_against_eq_in_ass 1);
   9.389 +back();
   9.390 +ba 1;
   9.391 +by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exA_tmp]) 1);
   9.392 +qed"filter_mkex_is_exA";
   9.393 + 
   9.394 +
   9.395 +(*---------------------------------------------------------------------------
   9.396 +     Filter of mkex(sch,exA,exB) to B after projection onto B is exB 
   9.397 +        --  using zip`(proj1`exB)`(proj2`exB) instead of exB    --
   9.398 +        --           because of admissibility problems          --
   9.399 +                             structural induction
   9.400 +  --------------------------------------------------------------------------- *)
   9.401 +
   9.402 +
   9.403 +goal thy "! exA exB s t. \
   9.404 +\ Forall (%x.x:act (A||B)) sch & \
   9.405 +\ Filter (%a.a:act A)`sch << filter_act`exA  &\
   9.406 +\ Filter (%a.a:act B)`sch << filter_act`exB \
   9.407 +\ --> Filter_ex2 B`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   9.408 +\     Zip`(Filter (%a.a:act B)`sch)`(Map snd`exB)";
   9.409 +
   9.410 +(* notice necessary change of arguments exA and exB *)
   9.411 +by (mkex_induct_tac "sch" "exB" "exA");
   9.412 +
   9.413 +qed"filter_mkex_is_exB_tmp";
   9.414 +
   9.415 +
   9.416 +(*---------------------------------------------------------------------------
   9.417 +     Filter of mkex(sch,exA,exB) to A after projection onto B is exB 
   9.418 +                       using the above trick
   9.419 +  --------------------------------------------------------------------------- *)
   9.420 +
   9.421 +
   9.422 +goal thy "!!sch exA exB.\
   9.423 +\ [| Forall (%a.a:act (A||B)) sch ; \
   9.424 +\ Filter (%a.a:act A)`sch = filter_act`(snd exA)  ;\
   9.425 +\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
   9.426 +\ ==> Filter_ex B (ProjB (mkex A B sch exA exB)) = exB";
   9.427 +by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
   9.428 +by (pair_tac "exA" 1);
   9.429 +by (pair_tac "exB" 1);
   9.430 +br conjI 1;
   9.431 +by (simp_tac (!simpset addsimps [mkex_def]) 1);
   9.432 +by (stac trick_against_eq_in_ass 1);
   9.433 +back();
   9.434 +ba 1;
   9.435 +by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exB_tmp]) 1);
   9.436 +qed"filter_mkex_is_exB";
   9.437 +
   9.438 +(* --------------------------------------------------------------------- *)
   9.439 +(*                    mkex has only  A- or B-actions                    *)
   9.440 +(* --------------------------------------------------------------------- *)
   9.441 +
   9.442 +
   9.443 +goal thy "!s t exA exB. \
   9.444 +\ Forall (%x. x : act (A || B)) sch &\
   9.445 +\ Filter (%a.a:act A)`sch << filter_act`exA  &\
   9.446 +\ Filter (%a.a:act B)`sch << filter_act`exB \
   9.447 +\  --> Forall (%x.fst x : act (A ||B))   \
   9.448 +\        (snd (mkex A B sch (s,exA) (t,exB)))";
   9.449 +
   9.450 +by (mkex_induct_tac "sch" "exA" "exB");
   9.451 +
   9.452 +qed"mkex_actions_in_AorB";
   9.453 +
   9.454 +
   9.455 +(* ------------------------------------------------------------------ *)
   9.456 +(*           COMPOSITIONALITY   on    SCHEDULE      Level             *)
   9.457 +(*                          Main Theorem                              *)
   9.458 +(* ------------------------------------------------------------------ *)
   9.459 +
   9.460 +goal thy  
   9.461 +"sch : schedules (A||B) = \
   9.462 +\ (Filter (%a.a:act A)`sch : schedules A &\
   9.463 +\  Filter (%a.a:act B)`sch : schedules B &\
   9.464 +\  Forall (%x. x:act (A||B)) sch)";
   9.465 +
   9.466 +by (simp_tac (!simpset addsimps [schedules_def, has_schedule_def]) 1);
   9.467 +by (safe_tac set_cs); 
   9.468 +(* ==> *) 
   9.469 +by (res_inst_tac [("x","Filter_ex A (ProjA ex)")] bexI 1);
   9.470 +by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
   9.471 +by (simp_tac (!simpset addsimps [Filter_ex_def,ProjA_def,
   9.472 +                                 lemma_2_1a,lemma_2_1b]) 1); 
   9.473 +by (res_inst_tac [("x","Filter_ex B (ProjB ex)")] bexI 1);
   9.474 +by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
   9.475 +by (simp_tac (!simpset addsimps [Filter_ex_def,ProjB_def,
   9.476 +                                 lemma_2_1a,lemma_2_1b]) 1);
   9.477 +by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
   9.478 +by (pair_tac "ex" 1);
   9.479 +be conjE 1;
   9.480 +by (asm_full_simp_tac (!simpset addsimps [sch_actions_in_AorB]) 1);
   9.481 +
   9.482 +(* <== *)
   9.483 +
   9.484 +(* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
   9.485 +   we need here *)
   9.486 +ren "exA exB" 1;
   9.487 +by (res_inst_tac [("x","mkex A B sch exA exB")] bexI 1);
   9.488 +(* mkex actions are just the oracle *)
   9.489 +by (pair_tac "exA" 1);
   9.490 +by (pair_tac "exB" 1);
   9.491 +by (asm_full_simp_tac (!simpset addsimps [Mapfst_mkex_is_sch]) 1);
   9.492 +
   9.493 +(* mkex is an execution -- use compositionality on ex-level *)
   9.494 +by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 1);
   9.495 +by (asm_full_simp_tac (!simpset addsimps 
   9.496 +                 [stutter_mkex_on_A, stutter_mkex_on_B,
   9.497 +                  filter_mkex_is_exB,filter_mkex_is_exA]) 1);
   9.498 +by (pair_tac "exA" 1);
   9.499 +by (pair_tac "exB" 1);
   9.500 +by (asm_full_simp_tac (!simpset addsimps [mkex_actions_in_AorB]) 1);
   9.501 +qed"compositionality_sch";
   9.502 +
   9.503 +
   9.504 +
   9.505 +Delsimps compoex_simps;
   9.506 +Delsimps composch_simps;
   9.507 \ No newline at end of file
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Apr 30 11:20:15 1997 +0200
    10.3 @@ -0,0 +1,63 @@
    10.4 +(*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
    10.5 +    ID:        
    10.6 +    Author:     Olaf M"uller
    10.7 +    Copyright   1996  TU Muenchen
    10.8 +
    10.9 +Compositionality on Schedule level.
   10.10 +*) 
   10.11 +
   10.12 +CompoScheds = CompoExecs + 
   10.13 +
   10.14 +
   10.15 +
   10.16 +consts
   10.17 +
   10.18 + mkex     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
   10.19 +              ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" 
   10.20 + mkex2    ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 
   10.21 +              ('a,'s)pairs -> ('a,'t)pairs -> 
   10.22 +              ('s => 't => ('a,'s*'t)pairs)"
   10.23 +
   10.24 +
   10.25 +defs
   10.26 +
   10.27 +mkex_def  
   10.28 +  "mkex A B sch exA exB == 
   10.29 +       ((fst exA,fst exB),
   10.30 +        (mkex2 A B`sch`(snd exA)`(snd exB)) (fst exA) (fst exB))"
   10.31 +
   10.32 +mkex2_def
   10.33 +  "mkex2 A B == (fix`(LAM h sch exA exB. (%s t. case sch of 
   10.34 +       nil => nil
   10.35 +    | x##xs => 
   10.36 +      (case x of 
   10.37 +        Undef => UU
   10.38 +      | Def y => 
   10.39 +         (if y:act A then 
   10.40 +             (if y:act B then 
   10.41 +                (case HD`exA of
   10.42 +                   Undef => UU
   10.43 +                 | Def a => (case HD`exB of
   10.44 +                              Undef => UU
   10.45 +                            | Def b => 
   10.46 +                   (y,(snd a,snd b))>>
   10.47 +                     (h`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))
   10.48 +              else
   10.49 +                (case HD`exA of
   10.50 +                   Undef => UU
   10.51 +                 | Def a => 
   10.52 +                   (y,(snd a,t))>>(h`xs`(TL`exA)`exB) (snd a) t)
   10.53 +              )
   10.54 +          else 
   10.55 +             (if y:act B then 
   10.56 +                (case HD`exB of
   10.57 +                   Undef => UU
   10.58 +                 | Def b => 
   10.59 +                   (y,(s,snd b))>>(h`xs`exA`(TL`exB)) s (snd b))
   10.60 +             else
   10.61 +               UU
   10.62 +             )
   10.63 +         )
   10.64 +       ))))"
   10.65 +
   10.66 +end
   10.67 \ No newline at end of file
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Apr 30 11:20:15 1997 +0200
    11.3 @@ -0,0 +1,734 @@
    11.4 +(*  Title:      HOLCF/IOA/meta_theory/CompoTraces.ML
    11.5 +    ID:        
    11.6 +    Author:     Olaf M"uller
    11.7 +    Copyright   1996  TU Muenchen
    11.8 +
    11.9 +Compositionality on Trace level.
   11.10 +*) 
   11.11 +
   11.12 +(* FIX:Proof and add in Sequence.ML *)
   11.13 +Addsimps [Finite_Conc];
   11.14 +
   11.15 +
   11.16 +(*
   11.17 +Addsimps [forall_cons];
   11.18 +
   11.19 +Addsimps [(* LastActExtsmall1, LastActExtsmall2, looping !! *) ext_and_act];
   11.20 +*)
   11.21 +
   11.22 +fun thin_tac' j =
   11.23 +  rotate_tac (j - 1) THEN'
   11.24 +  etac thin_rl THEN'
   11.25 +  rotate_tac (~ (j - 1));
   11.26 +
   11.27 +
   11.28 +
   11.29 +(* ---------------------------------------------------------------- *)
   11.30 +                   section "mksch rewrite rules";
   11.31 +(* ---------------------------------------------------------------- *)
   11.32 +
   11.33 +
   11.34 +
   11.35 +
   11.36 +bind_thm ("mksch_unfold", fix_prover2 thy mksch_def 
   11.37 +"mksch A B = (LAM tr schA schB. case tr of \
   11.38 +\       nil => nil\
   11.39 +\    | x##xs => \
   11.40 +\      (case x of  \ 
   11.41 +\        Undef => UU  \
   11.42 +\      | Def y => \
   11.43 +\         (if y:act A then \
   11.44 +\             (if y:act B then \ 
   11.45 +\                   ((Takewhile (%a.a:int A)`schA) \
   11.46 +\                         @@(Takewhile (%a.a:int B)`schB) \
   11.47 +\                              @@(y>>(mksch A B`xs   \
   11.48 +\                                       `(TL`(Dropwhile (%a.a:int A)`schA))  \
   11.49 +\                                       `(TL`(Dropwhile (%a.a:int B)`schB))  \
   11.50 +\                    )))   \
   11.51 +\              else  \
   11.52 +\                 ((Takewhile (%a.a:int A)`schA)  \
   11.53 +\                      @@ (y>>(mksch A B`xs  \
   11.54 +\                              `(TL`(Dropwhile (%a.a:int A)`schA))  \
   11.55 +\                              `schB)))  \
   11.56 +\              )   \
   11.57 +\          else    \
   11.58 +\             (if y:act B then  \ 
   11.59 +\                 ((Takewhile (%a.a:int B)`schB)  \
   11.60 +\                       @@ (y>>(mksch A B`xs   \
   11.61 +\                              `schA   \
   11.62 +\                              `(TL`(Dropwhile (%a.a:int B)`schB))  \
   11.63 +\                              )))  \
   11.64 +\             else  \
   11.65 +\               UU  \
   11.66 +\             )  \
   11.67 +\         )  \
   11.68 +\       ))");
   11.69 +
   11.70 +
   11.71 +goal thy "mksch A B`UU`schA`schB = UU";
   11.72 +by (stac mksch_unfold 1);
   11.73 +by (Simp_tac 1);
   11.74 +qed"mksch_UU";
   11.75 +
   11.76 +goal thy "mksch A B`nil`schA`schB = nil";
   11.77 +by (stac mksch_unfold 1);
   11.78 +by (Simp_tac 1);
   11.79 +qed"mksch_nil";
   11.80 +
   11.81 +goal thy "!!x.[|x:act A;x~:act B|]  \
   11.82 +\   ==> mksch A B`(x>>tr)`schA`schB = \
   11.83 +\         (Takewhile (%a.a:int A)`schA) \
   11.84 +\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
   11.85 +\                             `schB))";
   11.86 +br trans 1;
   11.87 +by (stac mksch_unfold 1);
   11.88 +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   11.89 +by (simp_tac (!simpset addsimps [Cons_def]) 1);
   11.90 +qed"mksch_cons1";
   11.91 +
   11.92 +goal thy "!!x.[|x~:act A;x:act B|] \
   11.93 +\   ==> mksch A B`(x>>tr)`schA`schB = \
   11.94 +\        (Takewhile (%a.a:int B)`schB)  \
   11.95 +\         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a.a:int B)`schB))  \
   11.96 +\                            ))";
   11.97 +br trans 1;
   11.98 +by (stac mksch_unfold 1);
   11.99 +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
  11.100 +by (simp_tac (!simpset addsimps [Cons_def]) 1);
  11.101 +qed"mksch_cons2";
  11.102 +
  11.103 +goal thy "!!x.[|x:act A;x:act B|] \
  11.104 +\   ==> mksch A B`(x>>tr)`schA`schB = \
  11.105 +\            (Takewhile (%a.a:int A)`schA) \
  11.106 +\         @@ ((Takewhile (%a.a:int B)`schB)  \
  11.107 +\         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
  11.108 +\                            `(TL`(Dropwhile (%a.a:int B)`schB))))  \
  11.109 +\             )";
  11.110 +br trans 1;
  11.111 +by (stac mksch_unfold 1);
  11.112 +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
  11.113 +by (simp_tac (!simpset addsimps [Cons_def]) 1);
  11.114 +qed"mksch_cons3";
  11.115 +
  11.116 +val compotr_simps =[mksch_UU,mksch_nil, mksch_cons1,mksch_cons2,mksch_cons3];
  11.117 +
  11.118 +Addsimps compotr_simps;
  11.119 +
  11.120 +
  11.121 +(* ------------------------------------------------------------------ *)
  11.122 +(*                      The following lemmata aim for                 *)
  11.123 +(*               COMPOSITIONALITY   on    TRACE     Level             *)
  11.124 +(* ------------------------------------------------------------------ *)
  11.125 +
  11.126 +
  11.127 +(* ---------------------------------------------------------------------------- *)
  11.128 +(*                  Specifics for "==>"                                         *)
  11.129 +(* ---------------------------------------------------------------------------- *)
  11.130 +
  11.131 +(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of 
  11.132 +   the compatibility of IOA, in particular out of the condition that internals are 
  11.133 +   really hidden. *)
  11.134 +
  11.135 +goal thy "(eB & ~eA --> ~A) -->       \
  11.136 +\         (A & (eA | eB)) = (eA & A)";
  11.137 +by (Fast_tac 1);
  11.138 +qed"compatibility_consequence1";
  11.139 +
  11.140 +
  11.141 +(* very similar to above, only the commutativity of | is used to make a slight change *)
  11.142 +
  11.143 +goal thy "(eB & ~eA --> ~A) -->       \
  11.144 +\         (A & (eB | eA)) = (eA & A)";
  11.145 +by (Fast_tac 1);
  11.146 +qed"compatibility_consequence2";
  11.147 +
  11.148 +
  11.149 +goal thy "!!x. [| x = nil;  y = z|] ==> (x @@ y) = z";
  11.150 +auto();
  11.151 +qed"nil_and_tconc";
  11.152 +
  11.153 +(* FIX: should be easy to get out of lemma before *)
  11.154 +goal thy "!!x. [| x = nil;  f`y = f`z|] ==> f`(x @@ y) = f`z";
  11.155 +auto();
  11.156 +qed"nil_and_tconc_f";
  11.157 +
  11.158 +(* FIX: should be something like subst: or better improve simp_tac so that these lemmat are
  11.159 +        superfluid *)
  11.160 +goal thy "!!x. [| x1 = x2;  f`(x2 @@ y) = f`z|] ==> f`(x1 @@ y) = f`z";
  11.161 +auto();
  11.162 +qed"tconcf";
  11.163 +
  11.164 +
  11.165 +
  11.166 +(*
  11.167 +
  11.168 +
  11.169 +(* -------------------------------------------------------------------------------- *)
  11.170 +
  11.171 +
  11.172 +goal thy "!!A B. compat_ioas A B ==> \
  11.173 +\   ! schA schB. Forall (%x. x:act (A||B)) tr \
  11.174 +\   --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)";
  11.175 +by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); 
  11.176 +by (safe_tac set_cs);
  11.177 +by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 1);
  11.178 +by (case_tac "a:act A" 1);
  11.179 +by (case_tac "a:act B" 1);
  11.180 +(* a:A, a:B *)
  11.181 +by (Asm_full_simp_tac 1);
  11.182 +br (Forall_Conc_impl RS mp) 1;
  11.183 +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
  11.184 +br (Forall_Conc_impl RS mp) 1;
  11.185 +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
  11.186 +(* a:A,a~:B *)
  11.187 +by (Asm_full_simp_tac 1);
  11.188 +br (Forall_Conc_impl RS mp) 1;
  11.189 +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
  11.190 +by (case_tac "a:act B" 1);
  11.191 +(* a~:A, a:B *)
  11.192 +by (Asm_full_simp_tac 1);
  11.193 +br (Forall_Conc_impl RS mp) 1;
  11.194 +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
  11.195 +(* a~:A,a~:B *)
  11.196 +auto();
  11.197 +qed"ForallAorB_mksch";
  11.198 +
  11.199 +
  11.200 +goal thy "!!A B. compat_ioas A B ==> \
  11.201 +\   ! schA schB.  (Forall (%x. x:act B & x~:act A) tr \
  11.202 +\   --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))";
  11.203 +
  11.204 +by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
  11.205 +by (safe_tac set_cs);
  11.206 +br (Forall_Conc_impl RS mp) 1;
  11.207 +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
  11.208 +qed"ForallBnA_mksch";
  11.209 +
  11.210 +goal thy "!!A B. compat_ioas B A ==> \
  11.211 +\   ! schA schB.  (Forall (%x. x:act A & x~:act B) tr \
  11.212 +\   --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))";
  11.213 +
  11.214 +by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
  11.215 +by (safe_tac set_cs);
  11.216 +by (Asm_full_simp_tac 1);
  11.217 +br (Forall_Conc_impl RS mp) 1;
  11.218 +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
  11.219 +qed"ForallAnB_mksch";
  11.220 +
  11.221 +
  11.222 +(* ------------------------------------------------------------------------------------ *)
  11.223 +
  11.224 +(*
  11.225 +goal thy "!! tr. Finite tr ==> \
  11.226 +\   ! x y. Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
  11.227 +\          Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
  11.228 +\          Forall (%x. x:ext (A||B)) tr \
  11.229 +\          --> Finite (mksch A B`tr`x`y)";
  11.230 +
  11.231 +be Seq_Finite_ind  1;
  11.232 +by (Asm_full_simp_tac 1);
  11.233 +(* main case *)
  11.234 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  11.235 +by (safe_tac set_cs);
  11.236 +by (Asm_full_simp_tac 1);
  11.237 +
  11.238 +
  11.239 +
  11.240 +qed"FiniteL_mksch";
  11.241 +
  11.242 +goal thy " !!bs. Finite bs ==>  \
  11.243 +\ Forall (%x. x:act B & x~:act A) bs &\
  11.244 +\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
  11.245 +\ --> (? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
  11.246 +\                Forall (%x. x:act B & x~:act A) y1 & \
  11.247 +\                Finite y1 & y = (y1 @@ y2) & \
  11.248 +\                Filter (%a. a:ext B)`y1 = bs)";
  11.249 +be Seq_Finite_ind  1;
  11.250 +by (rtac impI 1);
  11.251 +by (res_inst_tac [("x","nil")] exI 1);
  11.252 +by (res_inst_tac [("x","y")] exI 1);
  11.253 +by (Asm_full_simp_tac 1);
  11.254 +(* main case *)
  11.255 +by (rtac impI 1);
  11.256 +by (Asm_full_simp_tac 1);
  11.257 +by (REPEAT (etac conjE 1));
  11.258 +
  11.259 +
  11.260 +
  11.261 +
  11.262 +
  11.263 +qed"reduce_mksch";
  11.264 +
  11.265 +*)
  11.266 +
  11.267 +
  11.268 +(* Lemma for substitution of looping assumption in another specific assumption *) 
  11.269 +val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
  11.270 +by (cut_facts_tac [p1] 1);
  11.271 +be (p2 RS subst) 1;
  11.272 +qed"subst_lemma1";
  11.273 +
  11.274 +
  11.275 +
  11.276 +
  11.277 + 
  11.278 +(*---------------------------------------------------------------------------
  11.279 +    Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr
  11.280 +                             structural induction
  11.281 +  --------------------------------------------------------------------------- *)
  11.282 +
  11.283 +goal thy "! schA schB. compat_ioas A B & compat_ioas B A &\
  11.284 +\ is_asig(asig_of A) & is_asig(asig_of B) &\
  11.285 +\ Forall (%x.x:ext (A||B)) tr & \
  11.286 +\ Filter (%a.a:act A)`tr << Filter (%a.a:ext A)`schA &\
  11.287 +\ Filter (%a.a:act B)`tr << Filter (%a.a:ext B)`schB  \
  11.288 +\ --> Filter (%a.a:ext (A||B))`(mksch A B`tr`schA`schB) = tr";
  11.289 +
  11.290 +by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
  11.291 +
  11.292 +(* main case *) 
  11.293 +(* splitting into 4 cases according to a:A, a:B *)
  11.294 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  11.295 +by (safe_tac set_cs);
  11.296 +
  11.297 +(* Case a:A, a:B *)
  11.298 +by (forward_tac [divide_Seq] 1);
  11.299 +by (forward_tac [divide_Seq] 1);
  11.300 +back();
  11.301 +by (REPEAT (etac conjE 1));
  11.302 +(* filtering internals of A is nil *)
  11.303 +br nil_and_tconc 1;
  11.304 +br FilterPTakewhileQnil 1;
  11.305 +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
  11.306 +by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
  11.307 +             intA_is_not_extB,int_is_not_ext]) 1);
  11.308 +(* end*)
  11.309 +(* filtering internals of B is nil *)
  11.310 +(* FIX: should be done by simp_tac and claset combined until end*)
  11.311 +br nil_and_tconc 1;
  11.312 +br FilterPTakewhileQnil 1;
  11.313 +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
  11.314 +by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
  11.315 +             intA_is_not_extB,int_is_not_ext]) 1);
  11.316 +(* end*)
  11.317 +(* conclusion of IH ok, but assumptions of IH have to be transformed *)
  11.318 +by (dres_inst_tac [("x","schA")] subst_lemma1 1);
  11.319 +ba 1;
  11.320 +by (dres_inst_tac [("x","schB")] subst_lemma1 1);
  11.321 +ba 1;
  11.322 +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1);
  11.323 +
  11.324 +(* Case a:B, a~:A *)
  11.325 +
  11.326 +by (forward_tac [divide_Seq] 1);
  11.327 +by (REPEAT (etac conjE 1));
  11.328 +(* filtering internals of A is nil *)
  11.329 +(* FIX: should be done by simp_tac and claset combined until end*)
  11.330 +br nil_and_tconc 1;
  11.331 +br FilterPTakewhileQnil 1;
  11.332 +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
  11.333 +by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
  11.334 +             intA_is_not_extB,int_is_not_ext]) 1);
  11.335 +(* end*)
  11.336 +by (dres_inst_tac [("x","schB")] subst_lemma1 1);
  11.337 +back();
  11.338 +ba 1;
  11.339 +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1);
  11.340 +
  11.341 +(* Case a:A, a~:B *)
  11.342 +
  11.343 +by (forward_tac [divide_Seq] 1);
  11.344 +by (REPEAT (etac conjE 1));
  11.345 +(* filtering internals of A is nil *)
  11.346 +(* FIX: should be done by simp_tac and claset combined until end*)
  11.347 +br nil_and_tconc 1;
  11.348 +br FilterPTakewhileQnil 1;
  11.349 +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
  11.350 +by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
  11.351 +             intA_is_not_extB,int_is_not_ext]) 1);
  11.352 +(* end*)
  11.353 +by (dres_inst_tac [("x","schA")] subst_lemma1 1);
  11.354 +ba 1;
  11.355 +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1);
  11.356 +
  11.357 +(* Case a~:A, a~:B *)
  11.358 +
  11.359 +by (fast_tac (!claset addSIs [ext_is_act] 
  11.360 +                      addss (!simpset addsimps [externals_of_par]) ) 1);
  11.361 +qed"filterA_mksch_is_tr";
  11.362 +
  11.363 +
  11.364 +
  11.365 +
  11.366 +goal thy "!!x y. [|x=UU; y=UU|] ==> x=y";
  11.367 +auto();
  11.368 +qed"both_UU"; 
  11.369 +
  11.370 +goal thy "!!x y. [|x=nil; y=nil|] ==> x=y";
  11.371 +auto();
  11.372 +qed"both_nil";
  11.373 +
  11.374 +
  11.375 +(* FIX: does it exist already? *)
  11.376 +(* To eliminate representation a##xs, if only ~=UU & ~=nil is needed *)
  11.377 +goal thy "!!tr.  [|tr=a##xs; a~=UU |] ==> tr~=UU & tr~=nil";
  11.378 + by (Asm_full_simp_tac 1);
  11.379 +qed"yields_not_UU_or_nil";
  11.380 +
  11.381 +
  11.382 +
  11.383 +
  11.384 +
  11.385 +(*---------------------------------------------------------------------------
  11.386 +              Filter of mksch(tr,schA,schB) to A is schA 
  11.387 +                             take lemma
  11.388 +  --------------------------------------------------------------------------- *)
  11.389 +
  11.390 +goal thy "compat_ioas A B &  compat_ioas B A &\
  11.391 +\ Forall (%x.x:ext (A||B)) tr & \
  11.392 +\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
  11.393 +\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
  11.394 +\ LastActExtsch schA & LastActExtsch schB  \
  11.395 +\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
  11.396 +
  11.397 +
  11.398 +by (res_inst_tac [("Q","%x. x:act B & x~:act A")] take_lemma_less_induct 1);
  11.399 +
  11.400 +
  11.401 +(*---------------------------------------------------------------------------
  11.402 +              Filter of mksch(tr,schA,schB) to A is schA 
  11.403 +                             take lemma
  11.404 +  --------------------------------------------------------------------------- *)
  11.405 +
  11.406 +goal thy "! schA schB tr. compat_ioas A B &  compat_ioas B A &\
  11.407 +\ forall (plift (%x.x:externals(asig_of (A||B)))) tr & \
  11.408 +\ tfilter`(plift (%a.a:externals(asig_of A)))`schA = tfilter`(plift (%a.a:actions(asig_of A)))`tr &\
  11.409 +\ tfilter`(plift (%a.a:externals(asig_of B)))`schB = tfilter`(plift (%a.a:actions(asig_of B)))`tr &\
  11.410 +\ LastActExtsch schA & LastActExtsch schB  \
  11.411 +\ --> trace_take n`(tfilter`(plift (%a.a:actions(asig_of A)))`(mksch A B`tr`schA`schB)) = trace_take n`schA";
  11.412 +
  11.413 +by (res_inst_tac[("n","n")] less_induct 1);
  11.414 +by (REPEAT(rtac allI 1));
  11.415 +br impI 1;
  11.416 +by (REPEAT (etac conjE 1));
  11.417 +by (res_inst_tac [("x","tr")] trace.cases 1);
  11.418 +
  11.419 +(* tr = UU *)
  11.420 +by (rotate_tac ~1 1);
  11.421 +by (Asm_full_simp_tac 1);
  11.422 +by (dtac LastActExtimplUU 1);
  11.423 +ba 1;
  11.424 +by (Asm_simp_tac 1);
  11.425 +
  11.426 +(* tr = nil *)
  11.427 +by (rotate_tac ~1 1);
  11.428 +by (Asm_full_simp_tac 1);
  11.429 +by (dtac LastActExtimplnil 1);
  11.430 +ba 1;
  11.431 +by (Asm_simp_tac 1);
  11.432 +
  11.433 +(* tr = t##ts *)
  11.434 +
  11.435 +(* just to delete tr=a##xs, as we do not make induction on a but on an element in 
  11.436 +   xs we find later *)
  11.437 +by (dtac yields_not_UU_or_nil 1);
  11.438 +ba 1;
  11.439 +by (REPEAT (etac conjE 1));
  11.440 +
  11.441 +(* FIX: or use equality "hd(f ~P x)=UU  =  fa P x" to make distinction on that *)
  11.442 +by (case_tac "forall (plift (%x.x:actions(asig_of B) & x~:actions(asig_of A))) tr" 1);
  11.443 +(* This case holds for whole streams, not only for takes *)
  11.444 +br (trace_take_lemma RS iffD2 RS spec) 1;
  11.445 +
  11.446 +by (case_tac "tr : tfinite" 1);
  11.447 +
  11.448 +(* FIX: Check if new trace lemmata with ==> instead of --> allow for simplifiaction instead
  11.449 +       of ares_tac in the following *)
  11.450 +br both_nil 1;
  11.451 +(* mksch = nil *)
  11.452 +by (REPEAT (ares_tac [forallQfilterPnil,forallBnA_mksch,finiteL_mksch] 1));
  11.453 +by (Fast_tac 1);
  11.454 +(* schA = nil *)
  11.455 +by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
  11.456 +by (Asm_simp_tac 1);
  11.457 +br forallQfilterPnil 1;
  11.458 +ba 1;
  11.459 +back();
  11.460 +ba 1;
  11.461 +by (Fast_tac 1);
  11.462 +
  11.463 +(* case tr~:tfinite *)
  11.464 +
  11.465 +br both_UU 1;
  11.466 +(* mksch = UU *)
  11.467 +by (REPEAT (ares_tac [forallQfilterPUU,(finiteR_mksch RS mp COMP rev_contrapos),
  11.468 +                      forallBnA_mksch] 1));
  11.469 +by (Fast_tac 1);
  11.470 +(* schA = UU *)
  11.471 +by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
  11.472 +by (Asm_simp_tac 1);
  11.473 +br forallQfilterPUU 1;
  11.474 +by (REPEAT (atac  1));
  11.475 +back();
  11.476 +by (Fast_tac 1);
  11.477 +
  11.478 +(* case" ~ forall (plift (%x.x:actions(asig_of B) & x~:actions(asig_of A))) tr" *)
  11.479 +
  11.480 +by (dtac divide_trace3 1);
  11.481 +by (REPEAT (atac 1));
  11.482 +by (REPEAT (etac exE 1));
  11.483 +by (REPEAT (etac conjE 1));
  11.484 +
  11.485 +(* rewrite assuption for tr *)
  11.486 +by (hyp_subst_tac 1);
  11.487 +(* bring in lemma reduce_mksch *)
  11.488 +by (forw_inst_tac [("y","schB"),("x","schA")] reduce_mksch 1);
  11.489 +ba 1;
  11.490 +by (asm_simp_tac HOL_min_ss 1);
  11.491 +by (REPEAT (etac exE 1));
  11.492 +by (REPEAT (etac conjE 1));
  11.493 +
  11.494 +(* use reduce_mksch to rewrite conclusion *)
  11.495 +by (hyp_subst_tac 1);
  11.496 +by (Asm_full_simp_tac  1);
  11.497 +
  11.498 +(* eliminate the B-only prefix *)
  11.499 +(* FIX: Cannot be done by 
  11.500 +   by (asm_full_simp_tac (HOL_min_ss addsimps [forallQfilterPnil]) 1);
  11.501 +   as P&Q --> Q is looping. Perhaps forall (and other) operations not on predicates but on 
  11.502 +   sets because of this reason ?????? *)
  11.503 +br nil_and_tconc_f 1;
  11.504 +be forallQfilterPnil 1;
  11.505 +ba 1;
  11.506 +by (Fast_tac 1);
  11.507 +
  11.508 +(* Now real recursive step follows (in Def x) *)
  11.509 +
  11.510 +by (case_tac "x:actions(asig_of A)" 1);
  11.511 +by (case_tac "x~:actions(asig_of B)" 1);
  11.512 +by (rotate_tac ~2 1);
  11.513 +by (asm_full_simp_tac (!simpset addsimps [filter_rep])  1);
  11.514 +
  11.515 +(* same problem as above for the B-onlu prefix *)
  11.516 +(* FIX: eliminate generated subgoal immeadiately ! (as in case below x:A & x: B *)
  11.517 +by (subgoal_tac "tfilter`(plift (%a. a : actions (asig_of A) & a : externals (asig_of B)))`y1=nil" 1);
  11.518 +by (rotate_tac ~1 1);
  11.519 +by (Asm_full_simp_tac  1);
  11.520 +(* eliminate introduced subgoal 2 *)
  11.521 +be forallQfilterPnil 2;
  11.522 +ba 2;
  11.523 +by (Fast_tac 2);
  11.524 + 
  11.525 +(* f A (tw iA) = tw iA *)
  11.526 +by (simp_tac (HOL_min_ss addsimps [filterPtakewhileQ,int_is_act]) 1);
  11.527 +
  11.528 +by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace] 1);
  11.529 +(* subst divide_trace in conlcusion, but only at the righest occurence *)
  11.530 +by (res_inst_tac [("t","schA")] ssubst 1);
  11.531 +back();
  11.532 +back();
  11.533 +back();
  11.534 +ba 1;
  11.535 +by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite] 1);
  11.536 +
  11.537 +by (REPEAT (etac conjE 1));
  11.538 +(* reduce trace_takes from n to strictly smaller k *)
  11.539 +by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext]) 1);
  11.540 +br take_reduction 1;
  11.541 +ba 1;
  11.542 +(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
  11.543 +by (rotate_tac ~10 1);
  11.544 +(* assumption forall and schB *)
  11.545 +by (asm_full_simp_tac (!simpset addsimps [tconc_cong,forall_cons,forall_tconc,ext_and_act]) 1);
  11.546 +(* assumption schA *)
  11.547 +by (dres_inst_tac [("x","schA"),
  11.548 +                   ("g","tfilter`(plift (%a. a : actions (asig_of A)))`rs")] lemma22 1);
  11.549 +ba 1;
  11.550 +by (asm_full_simp_tac (!simpset addsimps [tfiltertconc,not_int_is_ext,tfilterPtakewhileQ]) 1);
  11.551 +by (REPEAT (etac conjE 1));
  11.552 +(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  11.553 +by (dres_inst_tac [("sch","schA"),("P","plift (%a. a : internals (asig_of A))")] LastActExtsmall1 1);
  11.554 +by (dres_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
  11.555 +ba 1;
  11.556 +by (Asm_full_simp_tac 1);
  11.557 +
  11.558 +(* case x:actions(asig_of A) & x: actions(asig_of B) *)
  11.559 +by (rotate_tac ~2 1);
  11.560 +by (asm_full_simp_tac (!simpset addsimps [filter_rep])  1);
  11.561 +by (subgoal_tac "tfilter`(plift (%a. a : actions (asig_of A) & a : externals (asig_of B)))`y1=nil" 1);
  11.562 +by (rotate_tac ~1 1);
  11.563 +by (Asm_full_simp_tac  1);
  11.564 +by (thin_tac' 1 1);
  11.565 +(* eliminate introduced subgoal 2 *)
  11.566 +be forallQfilterPnil 2;
  11.567 +ba 2;
  11.568 +by (Fast_tac 2);
  11.569 + 
  11.570 +(* f A (tw iA) = tw iA *)
  11.571 +by (simp_tac (HOL_min_ss addsimps [filterPtakewhileQ,int_is_act]) 1);
  11.572 +
  11.573 +by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace] 1);
  11.574 +(* subst divide_trace in conlcusion, but only at the righest occurence *)
  11.575 +by (res_inst_tac [("t","schA")] ssubst 1);
  11.576 +back();
  11.577 +back();
  11.578 +back();
  11.579 +ba 1;
  11.580 +by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite] 1);
  11.581 +by (REPEAT (etac conjE 1));
  11.582 +(* tidy up *)
  11.583 +by (thin_tac' 12 1);
  11.584 +by (thin_tac' 12 1);
  11.585 +by (thin_tac' 14 1);
  11.586 +by (thin_tac' 14 1);
  11.587 +by (rotate_tac ~8 1);
  11.588 +(* rewrite assumption forall and schB *)
  11.589 +by (asm_full_simp_tac (!simpset addsimps [tconc_cong,forall_cons,forall_tconc,ext_and_act]) 1);
  11.590 +(* divide_trace for schB2 *)
  11.591 +by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_trace) 1);
  11.592 +by (forw_inst_tac [("y","y2")](sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite) 1);
  11.593 +by (REPEAT (etac conjE 1));
  11.594 +by (rotate_tac ~6 1);
  11.595 +(* assumption schA *)
  11.596 +by (dres_inst_tac [("x","schA"),
  11.597 +                   ("g","tfilter`(plift (%a. a : actions (asig_of A)))`rs")] lemma22 1);
  11.598 +ba 1;
  11.599 +by (asm_full_simp_tac (!simpset addsimps [tfiltertconc,not_int_is_ext,tfilterPtakewhileQ]) 1);
  11.600 +by (REPEAT (etac conjE 1));
  11.601 +(* f A (tw iB schB2) = nil *) 
  11.602 +
  11.603 +(* good luck: intAisnotextB is not looping *)
  11.604 +by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext,tfilterPtakewhileQ,intAisnotextB]) 1);
  11.605 +(* reduce trace_takes from n to strictly smaller k *)
  11.606 +by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext]) 1);
  11.607 +br take_reduction 1;
  11.608 +ba 1;
  11.609 +(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
  11.610 +(* assumption schB *)
  11.611 +by (dres_inst_tac [("x","y2"),
  11.612 +                   ("g","tfilter`(plift (%a. a : actions (asig_of B)))`rs")] lemma22 1);
  11.613 +ba 1;
  11.614 +(* FIX: hey wonder: why does loopin rule for y2 here rewrites !!!!!!!!!!!!!!!!!!!!!!!!*)
  11.615 +by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext,tfilterPtakewhileQ,intAisnotextB]) 1);
  11.616 +by (REPEAT (etac conjE 1));
  11.617 +(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  11.618 +by (dres_inst_tac [("sch","schA"),("P","plift (%a. a : internals (asig_of A))")] LastActExtsmall1 1);
  11.619 +by (dres_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
  11.620 +ba 1;
  11.621 +by (dres_inst_tac [("sch","y2"),("P","plift (%a. a : internals (asig_of B))")] LastActExtsmall1 1);
  11.622 +by (Asm_full_simp_tac 1);
  11.623 + 
  11.624 +(* case x~:A & x:B  *)
  11.625 +(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
  11.626 +by (case_tac "x:actions(asig_of B)" 1);
  11.627 +by (Fast_tac 1);
  11.628 +
  11.629 +(* case x~:A & x~:B  *)
  11.630 +(* cannot occur because of assumption: forall (a:ext A | a:ext B) *)
  11.631 +by (rotate_tac ~8 1);
  11.632 +(* reduce forall assumption from tr to (Def x ## rs) *)
  11.633 +by (asm_full_simp_tac (!simpset addsimps [forall_cons,forall_tconc]) 1);
  11.634 +by (REPEAT (etac conjE 1));
  11.635 +by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
  11.636 +by (fast_tac (!claset addSIs [ext_is_act]) 1);
  11.637 +
  11.638 +qed"filterAmksch_is_schA";
  11.639 +
  11.640 +
  11.641 +goal thy "!! tr. [|compat_ioas A B ;  compat_ioas B A ;\
  11.642 +\ forall (plift (%x.x:externals(asig_of (A||B)))) tr ; \
  11.643 +\ tfilter`(plift (%a.a:externals(asig_of A)))`schA = tfilter`(plift (%a.a:actions(asig_of A)))`tr ;\
  11.644 +\ tfilter`(plift (%a.a:externals(asig_of B)))`schB = tfilter`(plift (%a.a:actions(asig_of B)))`tr ;\
  11.645 +\ LastActExtsch schA ; LastActExtsch schB |] \
  11.646 +\ ==> tfilter`(plift (%a.a:actions(asig_of A)))`(mksch A B`tr`schA`schB) = schA";
  11.647 +
  11.648 +br trace.take_lemma 1;
  11.649 +by (asm_simp_tac (!simpset addsimps [filterAmksch_is_schA]) 1);
  11.650 +qed"filterAmkschschA";
  11.651 +
  11.652 +
  11.653 +
  11.654 +(* ------------------------------------------------------------------ *)
  11.655 +(*                COMPOSITIONALITY   on    TRACE    Level             *)
  11.656 +(*                             Main Theorem                           *)
  11.657 +(* ------------------------------------------------------------------ *)
  11.658 + 
  11.659 +goal thy 
  11.660 +"!! A B. [| compat_ioas A B; compat_ioas B A; \
  11.661 +\           is_asig(asig_of A); is_asig(asig_of B)|] \
  11.662 +\       ==> traces(A||B) = \
  11.663 +\           { tr.(Filter (%a.a:act A)`tr : traces A &\
  11.664 +\                 Filter (%a.a:act B)`tr : traces B &\
  11.665 +\                 Forall (%x. x:ext(A||B)) tr) }";
  11.666 +
  11.667 +by (simp_tac (!simpset addsimps [traces_def,has_trace_def]) 1);
  11.668 +br set_ext 1;
  11.669 +by (safe_tac set_cs);
  11.670 + 
  11.671 +(* ==> *) 
  11.672 +(* There is a schedule of A *)
  11.673 +by (res_inst_tac [("x","Filter (%a.a:act A)`sch")] bexI 1);
  11.674 +by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
  11.675 +by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence1,
  11.676 +                  externals_of_par,ext1_ext2_is_not_act1]) 1);
  11.677 +(* There is a schedule of B *)
  11.678 +by (res_inst_tac [("x","Filter (%a.a:act B)`sch")] bexI 1);
  11.679 +by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2);
  11.680 +by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2,
  11.681 +                  externals_of_par,ext1_ext2_is_not_act2]) 1);
  11.682 +(* Traces of A||B have only external actions from A or B *)  
  11.683 +br ForallPFilterP 1;
  11.684 +
  11.685 +(* <== *)
  11.686 +
  11.687 +(* replace schA and schB by cutsch(schA) and cutsch(schB) *)
  11.688 +by (dtac exists_LastActExtsch 1);
  11.689 +ba 1;
  11.690 +by (dtac exists_LastActExtsch 1);
  11.691 +ba 1;
  11.692 +by (REPEAT (etac exE 1));
  11.693 +by (REPEAT (etac conjE 1));
  11.694 +
  11.695 +(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
  11.696 +   we need here *)
  11.697 +by (res_inst_tac [("x","mksch A B`tr`schb`schc")] bexI 1);
  11.698 +
  11.699 +(* External actions of mksch are just the oracle *)
  11.700 +by (asm_full_simp_tac (!simpset addsimps [filterA_mksch_is_tr]) 1);
  11.701 +
  11.702 +(* mksch is a schedule -- use compositionality on sch-level *)
  11.703 +by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 1);
  11.704 +
  11.705 +       das hier loopt: ForallPForallQ, ext_is_act,ForallAorB_mksch]) 1);
  11.706 +
  11.707 +
  11.708 +
  11.709 +
  11.710 +
  11.711 +
  11.712 +*)
  11.713 +
  11.714 +
  11.715 +
  11.716 +(* -------------------------------------------------------------------------------
  11.717 +         Other useful things
  11.718 +  -------------------------------------------------------------------------------- *)
  11.719 +
  11.720 +
  11.721 +(* Lemmata not needed yet 
  11.722 +goal Trace.thy "!!x. nil<<x ==> nil=x";
  11.723 +by (res_inst_tac [("x","x")] trace.cases 1);
  11.724 +by (hyp_subst_tac 1);
  11.725 +by (etac antisym_less 1);
  11.726 +by (Asm_full_simp_tac 1);
  11.727 +by (Asm_full_simp_tac 1);
  11.728 +by (hyp_subst_tac 1);
  11.729 +by (Asm_full_simp_tac 1);
  11.730 +qed"nil_less_is_nil";
  11.731 +
  11.732 +
  11.733 +*)
  11.734 +
  11.735 +
  11.736 +
  11.737 +
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Apr 30 11:20:15 1997 +0200
    12.3 @@ -0,0 +1,91 @@
    12.4 +(*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
    12.5 +    ID:        
    12.6 +    Author:     Olaf M"uller
    12.7 +    Copyright   1996  TU Muenchen
    12.8 +
    12.9 +Compositionality on Trace level.
   12.10 +*) 
   12.11 +
   12.12 +CompoTraces = CompoScheds + ShortExecutions +
   12.13 + 
   12.14 +
   12.15 +consts  
   12.16 +
   12.17 + mksch     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" 
   12.18 +
   12.19 +
   12.20 +defs
   12.21 +
   12.22 +mksch_def
   12.23 +  "mksch A B == (fix`(LAM h tr schA schB. case tr of 
   12.24 +       nil => nil
   12.25 +    | x##xs => 
   12.26 +      (case x of 
   12.27 +        Undef => UU
   12.28 +      | Def y => 
   12.29 +         (if y:act A then 
   12.30 +             (if y:act B then 
   12.31 +                   ((Takewhile (%a.a:int A)`schA)
   12.32 +                      @@ (Takewhile (%a.a:int B)`schB)
   12.33 +                           @@ (y>>(h`xs
   12.34 +                                    `(TL`(Dropwhile (%a.a:int A)`schA))
   12.35 +                                    `(TL`(Dropwhile (%a.a:int B)`schB))
   12.36 +                    )))
   12.37 +              else
   12.38 +                 ((Takewhile (%a.a:int A)`schA)
   12.39 +                  @@ (y>>(h`xs
   12.40 +                           `(TL`(Dropwhile (%a.a:int A)`schA))
   12.41 +                           `schB)))
   12.42 +              )
   12.43 +          else 
   12.44 +             (if y:act B then 
   12.45 +                 ((Takewhile (%a.a:int B)`schB)
   12.46 +                     @@ (y>>(h`xs
   12.47 +                              `schA
   12.48 +                              `(TL`(Dropwhile (%a.a:int B)`schB))
   12.49 +                              )))
   12.50 +             else
   12.51 +               UU
   12.52 +             )
   12.53 +         )
   12.54 +       )))"
   12.55 +
   12.56 +
   12.57 +rules
   12.58 +
   12.59 +(* FIX: x:actions S is further assumption, see Asig.ML: how to fulfill this in proofs ? *)
   12.60 +not_ext_is_int_FIX
   12.61 +  "[|is_asig S|] ==> (x~:externals S) = (x: internals S)"
   12.62 +
   12.63 +(* FIX: should be more general , something like subst *)
   12.64 +lemma12
   12.65 +"[| f << (g x) ; (x= (h x)) |] ==> f << g (h x)"
   12.66 +
   12.67 +(* FIX: as above, should be done more intelligent *)
   12.68 +lemma22
   12.69 +"[| (f x) = y >> g ; x = h x |] ==> (f (h x)) = y >> g"
   12.70 +
   12.71 +Finite_Conc
   12.72 +  "Finite (x @@ y) = (Finite x & Finite y)"
   12.73 +
   12.74 +finiteR_mksch
   12.75 +  "Finite (mksch A B`tr`x`y) --> Finite tr"
   12.76 +
   12.77 +finiteL_mksch
   12.78 +  "[| Finite tr; 
   12.79 +   Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr;
   12.80 +   Filter (%a. a:ext B)`y = Filter (%a. a:actB)`tr;
   12.81 +   Forall (%x. x:ext (A||B)) tr |]
   12.82 +   ==> Finite (mksch A B`tr`x`y)"
   12.83 +
   12.84 +reduce_mksch
   12.85 +  "[| Finite bs; Forall (%x. x:act B & x~:act A) bs;
   12.86 +      Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) |] 
   12.87 +  ==> ? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) &
   12.88 +                Forall (%x. x:act B & x~:act A) y1 &
   12.89 +                Finite y1 & y = (y1 @@ y2) & 
   12.90 +                Filter (%a. a:ext B)`y1 = bs"
   12.91 +
   12.92 +end
   12.93 +
   12.94 +
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Wed Apr 30 11:20:15 1997 +0200
    13.3 @@ -0,0 +1,23 @@
    13.4 +(*  Title:      HOLCF/IOA/meta_theory/Compositionality.ML
    13.5 +    ID:        
    13.6 +    Author:     Olaf M"uller
    13.7 +    Copyright   1997  TU Muenchen
    13.8 +
    13.9 +Compositionality of I/O automata
   13.10 +*) 
   13.11 +
   13.12 +
   13.13 +goal thy "!! A1 A2 B1 B2. \
   13.14 +\         [| is_asig (asig_of A1); is_asig (asig_of A2); \
   13.15 +\            is_asig (asig_of B1); is_asig (asig_of B2); \
   13.16 +\            compat_ioas A1 B1; compat_ioas B1 A1; compat_ioas A2 B2; compat_ioas B2 A2; \
   13.17 +\            A1 =<| A2; \
   13.18 +\            B1 =<| B2 |] \
   13.19 +\        ==> (A1 || B1) =<| (A2 || B2)";
   13.20 +by (asm_full_simp_tac (!simpset addsimps [ioa_implements_def,
   13.21 +                               inputs_of_par,outputs_of_par]) 1);
   13.22 +
   13.23 +
   13.24 +by (safe_tac set_cs);
   13.25 +by (asm_full_simp_tac (!simpset addsimps [compotraces]) 1);
   13.26 +
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy	Wed Apr 30 11:20:15 1997 +0200
    14.3 @@ -0,0 +1,21 @@
    14.4 +(*  Title:      HOLCF/IOA/meta_theory/Compositionality.thy
    14.5 +    ID:        
    14.6 +    Author:     Olaf M"uller
    14.7 +    Copyright   1997  TU Muenchen
    14.8 +
    14.9 +Compositionality of I/O automata
   14.10 +*) 
   14.11 +
   14.12 +Compositionality = CompoTraces + 
   14.13 +
   14.14 +rules 
   14.15 +
   14.16 +compotraces
   14.17 +"[| compat_ioas A B; compat_ioas B A; 
   14.18 +    is_asig(asig_of A); is_asig(asig_of B)|] 
   14.19 + ==> traces(A||B) = 
   14.20 +     {tr. (Filter (%a.a:act A)`tr : traces A &
   14.21 +      Filter (%a.a:act B)`tr : traces B &
   14.22 +      Forall (%x. x:ext(A||B)) tr)}"
   14.23 +
   14.24 +end 
   14.25 \ No newline at end of file
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOLCF/IOA/meta_theory/IOA.ML	Wed Apr 30 11:20:15 1997 +0200
    15.3 @@ -0,0 +1,7 @@
    15.4 +(*  Title:      HOLCF/IOA/meta_theory/IOA.thy
    15.5 +    ID:        
    15.6 +    Author:     Olaf Mueller
    15.7 +    Copyright   1996,1997  TU Muenchen
    15.8 +
    15.9 +The theory of I/O automata in HOLCF.
   15.10 +*)  
   15.11 \ No newline at end of file
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOLCF/IOA/meta_theory/IOA.thy	Wed Apr 30 11:20:15 1997 +0200
    16.3 @@ -0,0 +1,13 @@
    16.4 +(*  Title:      HOLCF/IOA/meta_theory/IOA.thy
    16.5 +    ID:        
    16.6 +    Author:     Olaf Mueller
    16.7 +    Copyright   1996,1997  TU Muenchen
    16.8 +
    16.9 +The theory of I/O automata in HOLCF.
   16.10 +*)   
   16.11 +
   16.12 + 
   16.13 +	       
   16.14 +IOA = RefCorrectness + Compositionality
   16.15 +
   16.16 +
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Wed Apr 30 11:20:15 1997 +0200
    17.3 @@ -0,0 +1,292 @@
    17.4 +(*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.ML
    17.5 +    ID:         $$
    17.6 +    Author:     Olaf Mueller
    17.7 +    Copyright   1996  TU Muenchen
    17.8 +
    17.9 +Correctness of Refinement Mappings in HOLCF/IOA
   17.10 +*)
   17.11 +
   17.12 +
   17.13 +
   17.14 +(* -------------------------------------------------------------------------------- *)
   17.15 +
   17.16 +section "corresp_ex";
   17.17 +
   17.18 +
   17.19 +(* ---------------------------------------------------------------- *)
   17.20 +(*                             corresp_ex2                          *)
   17.21 +(* ---------------------------------------------------------------- *)
   17.22 +
   17.23 +
   17.24 +goal thy "corresp_ex2 A f  = (LAM ex. (%s. case ex of \
   17.25 +\      nil =>  nil   \
   17.26 +\    | x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr))))   \
   17.27 +\                              @@ ((corresp_ex2 A f `xs) (f (snd pr))))   \
   17.28 +\                        `x) ))";
   17.29 +by (rtac trans 1);
   17.30 +br fix_eq2 1;
   17.31 +br corresp_ex2_def 1;
   17.32 +br beta_cfun 1;
   17.33 +by (simp_tac (!simpset addsimps [flift1_def]) 1);
   17.34 +qed"corresp_ex2_unfold";
   17.35 +
   17.36 +goal thy "(corresp_ex2 A f`UU) s=UU";
   17.37 +by (stac corresp_ex2_unfold 1);
   17.38 +by (Simp_tac 1);
   17.39 +qed"corresp_ex2_UU";
   17.40 +
   17.41 +goal thy "(corresp_ex2 A f`nil) s = nil";
   17.42 +by (stac corresp_ex2_unfold 1);
   17.43 +by (Simp_tac 1);
   17.44 +qed"corresp_ex2_nil";
   17.45 +
   17.46 +goal thy "(corresp_ex2 A f`(at>>xs)) s = \
   17.47 +\          (snd(@cex. move A cex s (fst at) (f (snd at))))  \
   17.48 +\          @@ ((corresp_ex2 A f`xs) (f (snd at)))";
   17.49 +br trans 1;
   17.50 +by (stac corresp_ex2_unfold 1);
   17.51 +by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
   17.52 +by (Simp_tac 1);
   17.53 +qed"corresp_ex2_cons";
   17.54 +
   17.55 +
   17.56 +Addsimps [corresp_ex2_UU,corresp_ex2_nil,corresp_ex2_cons];
   17.57 +
   17.58 +
   17.59 +
   17.60 +(* ------------------------------------------------------------------ *)
   17.61 +(*               The following lemmata describe the definition        *)
   17.62 +(*                         of move in more detail                     *)
   17.63 +(* ------------------------------------------------------------------ *)
   17.64 +
   17.65 +section"properties of move";
   17.66 +
   17.67 +goalw thy [is_ref_map_def]
   17.68 +   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   17.69 +\     move A (@x. move A x (f s) a (f t)) (f s) a (f t)";
   17.70 +
   17.71 +by (subgoal_tac "? ex.move A ex (f s) a (f t)" 1);
   17.72 +by (Asm_full_simp_tac 2);
   17.73 +by (etac exE 1);
   17.74 +by (rtac selectI 1);
   17.75 +by (assume_tac 1);
   17.76 +qed"move_is_move";
   17.77 +
   17.78 +goal thy
   17.79 +   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   17.80 +\    is_execution_fragment A (@x. move A x (f s) a (f t))";
   17.81 +by (cut_inst_tac [] move_is_move 1);
   17.82 +by (REPEAT (assume_tac 1));
   17.83 +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   17.84 +qed"move_subprop1";
   17.85 +
   17.86 +goal thy
   17.87 +   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   17.88 +\    Finite (snd (@x. move A x (f s) a (f t)))";
   17.89 +by (cut_inst_tac [] move_is_move 1);
   17.90 +by (REPEAT (assume_tac 1));
   17.91 +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   17.92 +qed"move_subprop2";
   17.93 +
   17.94 +goal thy
   17.95 +   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
   17.96 +\    fst (@x. move A x (f s) a (f t)) = (f s)";
   17.97 +by (cut_inst_tac [] move_is_move 1);
   17.98 +by (REPEAT (assume_tac 1));
   17.99 +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
  17.100 +qed"move_subprop3";
  17.101 +
  17.102 +goal thy
  17.103 +   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
  17.104 +\    laststate (@x. move A x (f s) a (f t)) = (f t)";
  17.105 +by (cut_inst_tac [] move_is_move 1);
  17.106 +by (REPEAT (assume_tac 1));
  17.107 +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
  17.108 +qed"move_subprop4";
  17.109 +
  17.110 +goal thy
  17.111 +   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
  17.112 +\     mk_trace A`(snd(@x. move A x (f s) a (f t))) = \
  17.113 +\       (if a:ext A then a>>nil else nil)";
  17.114 +
  17.115 +by (cut_inst_tac [] move_is_move 1);
  17.116 +by (REPEAT (assume_tac 1));
  17.117 +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
  17.118 +qed"move_subprop5";
  17.119 +
  17.120 +goal thy
  17.121 +   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
  17.122 +\    (is_execution_fragment A (f s,(snd (@x. move A x (f s) a (f t)))))";
  17.123 +by (cut_inst_tac [] move_subprop3 1);
  17.124 +by (REPEAT (assume_tac 1));
  17.125 +by (cut_inst_tac [] move_subprop1 1);
  17.126 +by (REPEAT (assume_tac 1));
  17.127 +by (res_inst_tac [("s","fst (@x. move A x (f s) a (f t))")] subst 1);
  17.128 +back();
  17.129 +back();
  17.130 +back();
  17.131 +ba 1;
  17.132 +by (simp_tac (HOL_basic_ss addsimps [surjective_pairing RS sym]) 1);
  17.133 +qed"move_subprop_1and3";
  17.134 +
  17.135 +goal thy
  17.136 +   "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\
  17.137 +\    (case Last`(snd (@x. move A x (f s) a (f t))) of \
  17.138 +\       Undef => (f s) \
  17.139 +\     | Def p => snd p) = (f t)";
  17.140 +by (cut_inst_tac [] move_subprop3 1);
  17.141 +by (REPEAT (assume_tac 1));
  17.142 +by (cut_inst_tac [] move_subprop4 1);
  17.143 +by (REPEAT (assume_tac 1));
  17.144 +by (asm_full_simp_tac (!simpset addsimps [laststate_def]) 1);
  17.145 +qed"move_subprop_4and3";
  17.146 +
  17.147 +
  17.148 +
  17.149 +(* ------------------------------------------------------------------ *)
  17.150 +(*                   The following lemmata contribute to              *)
  17.151 +(*                 TRACE INCLUSION Part 1: Traces coincide            *)
  17.152 +(* ------------------------------------------------------------------ *)
  17.153 +
  17.154 +section "Lemmata for <==";
  17.155 +
  17.156 +(* --------------------------------------------------- *)
  17.157 +(*   Lemma 1.1: Distribution of mk_trace and @@        *)
  17.158 +(* --------------------------------------------------- *)
  17.159 +
  17.160 +
  17.161 +goal thy "mk_trace C`(ex1 @@ ex2)= (mk_trace C`ex1) @@ (mk_trace C`ex2)";
  17.162 +by (simp_tac (!simpset addsimps [mk_trace_def,filter_act_def,
  17.163 +                                 FilterConc,MapConc]) 1);
  17.164 +qed"mk_traceConc";
  17.165 +
  17.166 +
  17.167 +
  17.168 +(* ------------------------------------------------------
  17.169 +                 Lemma 1 :Traces coincide  
  17.170 +   ------------------------------------------------------- *)
  17.171 +
  17.172 +goalw thy [corresp_ex_def]
  17.173 +  "!!f.[|is_ref_map f C A; ext C = ext A|] ==>  \     
  17.174 +\        !s. reachable C s & is_execution_fragment C (s,xs) --> \
  17.175 +\            mk_trace C`xs = mk_trace A`(snd (corresp_ex A f (s,xs)))";
  17.176 +
  17.177 +by (pair_induct_tac "xs" [is_execution_fragment_def] 1);
  17.178 +(* cons case *) 
  17.179 +by (safe_tac set_cs);
  17.180 +by (asm_full_simp_tac (!simpset addsimps [mk_traceConc]) 1);
  17.181 +by (forward_tac [reachable.reachable_n] 1);
  17.182 +ba 1;
  17.183 +by (eres_inst_tac [("x","y")] allE 1);
  17.184 +by (Asm_full_simp_tac 1);
  17.185 +by (asm_full_simp_tac (!simpset addsimps [move_subprop5] 
  17.186 +                          setloop split_tac [expand_if] ) 1);
  17.187 +qed"lemma_1";
  17.188 +
  17.189 +
  17.190 +(* ------------------------------------------------------------------ *)
  17.191 +(*                   The following lemmata contribute to              *)
  17.192 +(*              TRACE INCLUSION Part 2: corresp_ex is execution       *)
  17.193 +(* ------------------------------------------------------------------ *)
  17.194 +
  17.195 +section "Lemmata for ==>";
  17.196 +
  17.197 +(* -------------------------------------------------- *)
  17.198 +(*                   Lemma 2.1                        *)
  17.199 +(* -------------------------------------------------- *)
  17.200 +
  17.201 +goal thy 
  17.202 +"Finite xs --> \
  17.203 +\(!s .is_execution_fragment A (s,xs) & is_execution_fragment A (t,ys) & \ 
  17.204 +\     t = laststate (s,xs) \
  17.205 +\ --> is_execution_fragment A (s,xs @@ ys))";
  17.206 +
  17.207 +br impI 1;
  17.208 +by (Seq_Finite_induct_tac 1);
  17.209 +(* base_case *)
  17.210 +by (fast_tac HOL_cs 1);
  17.211 +(* main case *)
  17.212 +by (safe_tac set_cs);
  17.213 +by (pair_tac "a" 1);
  17.214 +qed"lemma_2_1";
  17.215 +
  17.216 +
  17.217 +(* ----------------------------------------------------------- *)
  17.218 +(*               Lemma 2 : corresp_ex is execution             *)
  17.219 +(* ----------------------------------------------------------- *)
  17.220 +
  17.221 +
  17.222 +
  17.223 +goalw thy [corresp_ex_def]
  17.224 + "!!f.[| is_ref_map f C A |] ==>\
  17.225 +\ !s. reachable C s & is_execution_fragment C (s,xs) \
  17.226 +\ --> is_execution_fragment A (corresp_ex A f (s,xs))"; 
  17.227 +
  17.228 +by (Asm_full_simp_tac 1);
  17.229 +by (pair_induct_tac "xs" [is_execution_fragment_def] 1);
  17.230 +(* main case *)
  17.231 +by (safe_tac set_cs);
  17.232 +by (res_inst_tac [("t3","f y")]  (lemma_2_1 RS mp RS spec RS mp) 1);
  17.233 +
  17.234 +(* Finite *)
  17.235 +be move_subprop2 1;
  17.236 +by (REPEAT (atac 1));
  17.237 +by (rtac conjI 1);
  17.238 +
  17.239 +(* is_execution_fragment *)
  17.240 +be  move_subprop_1and3 1;
  17.241 +by (REPEAT (atac 1));
  17.242 +by (rtac conjI 1);
  17.243 +
  17.244 +(* Induction hypothesis  *)
  17.245 +(* reachable_n looping, therefore apply it manually *)
  17.246 +by (eres_inst_tac [("x","y")] allE 1);
  17.247 +by (Asm_full_simp_tac 1);
  17.248 +by (forward_tac [reachable.reachable_n] 1);
  17.249 +ba 1;
  17.250 +by (Asm_full_simp_tac 1);
  17.251 +(* laststate *)
  17.252 +by (simp_tac (!simpset addsimps [laststate_def]) 1); 
  17.253 +be (move_subprop_4and3 RS sym) 1;
  17.254 +by (REPEAT (atac 1));
  17.255 +qed"lemma_2";
  17.256 +
  17.257 +
  17.258 +(* -------------------------------------------------------------------------------- *)
  17.259 +
  17.260 +section "Main Theorem: T R A C E - I N C L U S I O N";
  17.261 +
  17.262 +(* -------------------------------------------------------------------------------- *)
  17.263 +
  17.264 +
  17.265 +goalw thy [traces_def]
  17.266 +  "!!f. [| IOA C; IOA A; ext C = ext A; is_ref_map f C A |] \
  17.267 +\          ==> traces C <= traces A"; 
  17.268 +
  17.269 +  by (simp_tac(!simpset addsimps [has_trace_def2])1);
  17.270 +  by (safe_tac set_cs);
  17.271 +
  17.272 +  (* give execution of abstract automata *)
  17.273 +  by (res_inst_tac[("x","corresp_ex A f ex")] bexI 1);
  17.274 +  
  17.275 +  (* Traces coincide, Lemma 1 *)
  17.276 +  by (pair_tac "ex" 1);
  17.277 +  by (etac (lemma_1 RS spec RS mp) 1);
  17.278 +  by (REPEAT (atac 1));
  17.279 +  by (asm_full_simp_tac (!simpset addsimps [executions_def,reachable.reachable_0]) 1);
  17.280 + 
  17.281 +  (* corresp_ex is execution, Lemma 2 *)
  17.282 +  by (pair_tac "ex" 1);
  17.283 +  by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
  17.284 +  (* start state *) 
  17.285 +  by (rtac conjI 1);
  17.286 +  by (asm_full_simp_tac (!simpset addsimps [is_ref_map_def,corresp_ex_def]) 1);
  17.287 +  (* is-execution-fragment *)
  17.288 +  by (etac (lemma_2 RS spec RS mp) 1);
  17.289 +  by (asm_full_simp_tac (!simpset addsimps [reachable.reachable_0]) 1);
  17.290 +qed"trace_inclusion"; 
  17.291 +
  17.292 +
  17.293 +
  17.294 +
  17.295 +
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Wed Apr 30 11:20:15 1997 +0200
    18.3 @@ -0,0 +1,35 @@
    18.4 +(*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
    18.5 +    ID:         $$
    18.6 +    Author:     Olaf Mueller
    18.7 +    Copyright   1996  TU Muenchen
    18.8 +
    18.9 +Correctness of Refinement Mappings in HOLCF/IOA
   18.10 +*)
   18.11 +
   18.12 +
   18.13 +RefCorrectness = RefMappings + 
   18.14 +
   18.15 +consts
   18.16 +
   18.17 +  corresp_ex   ::"('a,'s2)ioa => ('s1 => 's2) => 
   18.18 +                  ('a,'s1)execution => ('a,'s2)execution"
   18.19 +  corresp_ex2  ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
   18.20 +                   -> ('s2 => ('a,'s2)pairs)"
   18.21 +
   18.22 +
   18.23 +defs
   18.24 +
   18.25 +corresp_ex_def
   18.26 +  "corresp_ex A f ex == (f (fst ex),(corresp_ex2 A f`(snd ex)) (f (fst ex)))"
   18.27 +
   18.28 +
   18.29 +corresp_ex2_def
   18.30 +  "corresp_ex2 A f  == (fix`(LAM h ex. (%s. case ex of 
   18.31 +      nil =>  nil
   18.32 +    | x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr))))
   18.33 +                              @@ ((h`xs) (f (snd pr))))
   18.34 +                        `x) )))"
   18.35 + 
   18.36 +
   18.37 +
   18.38 +end
   18.39 \ No newline at end of file
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Wed Apr 30 11:20:15 1997 +0200
    19.3 @@ -0,0 +1,132 @@
    19.4 +(*  Title:      HOLCF/IOA/meta_theory/RefMappings.ML
    19.5 +    ID:         $$
    19.6 +    Author:     Olaf Mueller
    19.7 +    Copyright   1996  TU Muenchen
    19.8 +
    19.9 +Refinement Mappings in HOLCF/IOA
   19.10 +*)
   19.11 +
   19.12 +
   19.13 +
   19.14 +goal thy "laststate (s,UU) = s";
   19.15 +by (simp_tac (!simpset addsimps [laststate_def]) 1); 
   19.16 +qed"laststate_UU";
   19.17 +
   19.18 +goal thy "laststate (s,nil) = s";
   19.19 +by (simp_tac (!simpset addsimps [laststate_def]) 1);
   19.20 +qed"laststate_nil";
   19.21 +
   19.22 +goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)";
   19.23 +by (simp_tac (!simpset addsimps [laststate_def]) 1);
   19.24 +by (case_tac "ex=nil" 1);
   19.25 +by (Asm_simp_tac 1);
   19.26 +by (Asm_simp_tac 1);
   19.27 +bd (Finite_Last1 RS mp) 1;
   19.28 +ba 1;
   19.29 +by (def_tac 1);
   19.30 +qed"laststate_cons";
   19.31 +
   19.32 +Addsimps [laststate_UU,laststate_nil,laststate_cons];
   19.33 +
   19.34 +(* ---------------------------------------------------------------------------- *)
   19.35 +
   19.36 +section "transitions and moves";
   19.37 +
   19.38 +
   19.39 +goal thy"!!f. s -a--A-> t ==> ? ex. move A ex s a t";
   19.40 +
   19.41 +by (res_inst_tac [("x","(s,(a,t)>>nil)")] exI 1);
   19.42 +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   19.43 +qed"transition_is_ex";
   19.44 +
   19.45 +
   19.46 +goal thy"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t";
   19.47 +
   19.48 +by (res_inst_tac [("x","(s,nil)")] exI 1);
   19.49 +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   19.50 +qed"nothing_is_ex";
   19.51 +
   19.52 +
   19.53 +goal thy"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \
   19.54 +\        ==> ? ex. move A ex s a s''";
   19.55 +
   19.56 +by (res_inst_tac [("x","(s,(a,s')>>(a',s'')>>nil)")] exI 1);
   19.57 +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   19.58 +qed"ei_transitions_are_ex";
   19.59 +
   19.60 +
   19.61 +goal thy
   19.62 +"!!f. (s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\
   19.63 +\     (~a2:ext A) & (~a3:ext A) ==> \
   19.64 +\     ? ex. move A ex s1 a1 s4";
   19.65 +  
   19.66 +by (res_inst_tac [("x","(s1,(a1,s2)>>(a2,s3)>>(a3,s4)>>nil)")] exI 1);
   19.67 +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1);
   19.68 +qed"eii_transitions_are_ex";
   19.69 +
   19.70 +
   19.71 +(* ---------------------------------------------------------------------------- *)
   19.72 +
   19.73 +section "weak_ref_map and ref_map";
   19.74 +
   19.75 +
   19.76 +goalw thy [is_weak_ref_map_def,is_ref_map_def]
   19.77 +  "!!f. [| ext C = ext A; \
   19.78 +\    is_weak_ref_map f C A |] ==> is_ref_map f C A";
   19.79 +by (safe_tac set_cs);
   19.80 +by (case_tac "a:ext A" 1);
   19.81 +by (rtac transition_is_ex 1);
   19.82 +by (Asm_simp_tac 1);
   19.83 +by (rtac nothing_is_ex 1);
   19.84 +by (Asm_simp_tac 1);
   19.85 +qed"weak_ref_map2ref_map";
   19.86 +
   19.87 +
   19.88 +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
   19.89 +  by(fast_tac (!claset addDs prems) 1);
   19.90 +qed "imp_conj_lemma";
   19.91 +
   19.92 +goal thy "!!f.[| is_weak_ref_map f C A |]\
   19.93 +\                      ==> (is_weak_ref_map f (rename C g) (rename A g))";
   19.94 +by (asm_full_simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
   19.95 +by (rtac conjI 1);
   19.96 +(* 1: start states *)
   19.97 +by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1);
   19.98 +(* 2: reachable transitions *)
   19.99 +by (REPEAT (rtac allI 1));
  19.100 +by (rtac imp_conj_lemma 1);
  19.101 +by (simp_tac (!simpset addsimps [rename_def]) 1);
  19.102 +by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
  19.103 +asig_outputs_def,asig_of_def,trans_of_def]) 1);
  19.104 +by (safe_tac (!claset));
  19.105 +by (rtac (expand_if RS ssubst) 1);
  19.106 + by (rtac conjI 1);
  19.107 + by (rtac impI 1);
  19.108 + by (etac disjE 1);
  19.109 + by (etac exE 1);
  19.110 +by (etac conjE 1);
  19.111 +(* x is input *)
  19.112 + by (dtac sym 1);
  19.113 + by (dtac sym 1);
  19.114 +by (Asm_full_simp_tac 1);
  19.115 +by (REPEAT (hyp_subst_tac 1));
  19.116 +by (forward_tac  [reachable_rename] 1);
  19.117 +by (Asm_full_simp_tac 1);
  19.118 +(* x is output *)
  19.119 + by (etac exE 1);
  19.120 +by (etac conjE 1);
  19.121 + by (dtac sym 1);
  19.122 + by (dtac sym 1);
  19.123 +by (Asm_full_simp_tac 1);
  19.124 +by (REPEAT (hyp_subst_tac 1));
  19.125 +by (forward_tac  [reachable_rename] 1);
  19.126 +by (Asm_full_simp_tac 1);
  19.127 +(* x is internal *)
  19.128 +by (simp_tac (!simpset addcongs [conj_cong]) 1);
  19.129 +by (rtac impI 1);
  19.130 +by (etac conjE 1);
  19.131 +by (forward_tac  [reachable_rename] 1);
  19.132 +by (Auto_tac());
  19.133 +qed"rename_through_pmap";
  19.134 +
  19.135 +
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Wed Apr 30 11:20:15 1997 +0200
    20.3 @@ -0,0 +1,50 @@
    20.4 +(*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
    20.5 +    ID:         $$
    20.6 +    Author:     Olaf Mueller
    20.7 +    Copyright   1996  TU Muenchen
    20.8 +
    20.9 +Refinement Mappings in HOLCF/IOA
   20.10 +*)
   20.11 +
   20.12 +RefMappings = Traces  +
   20.13 +
   20.14 +default term
   20.15 +
   20.16 +consts
   20.17 +  laststate    ::"('a,'s)execution => 's"
   20.18 +  move         ::"[('a,'s)ioa,('a,'s)execution,'s,'a,'s] => bool"
   20.19 +  is_ref_map   ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
   20.20 +  is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
   20.21 + 
   20.22 +defs
   20.23 +
   20.24 +laststate_def
   20.25 +  "laststate ex == case Last`(snd ex) of
   20.26 +                      Undef  => fst ex
   20.27 +                    | Def at => snd at"
   20.28 +
   20.29 +(* FIX: see paper, move should be defined on pairs, not on execs, then fst ex=s can
   20.30 +   be omitted *)
   20.31 +move_def
   20.32 +  "move ioa ex s a t ==    
   20.33 +    (is_execution_fragment ioa ex &  Finite (snd ex) & 
   20.34 +     fst ex=s & laststate ex=t  &     
   20.35 +     mk_trace ioa`(snd ex) = (if a:ext(ioa) then a>>nil else nil))"
   20.36 +
   20.37 +is_ref_map_def
   20.38 +  "is_ref_map f C A ==                          
   20.39 +   (!s:starts_of(C). f(s):starts_of(A)) &        
   20.40 +   (!s t a. reachable C s &                      
   20.41 +            s -a--C-> t                 
   20.42 +            --> (? ex. move A ex (f s) a (f t)))"
   20.43 + 
   20.44 +is_weak_ref_map_def
   20.45 +  "is_weak_ref_map f C A ==                          
   20.46 +   (!s:starts_of(C). f(s):starts_of(A)) &        
   20.47 +   (!s t a. reachable C s &                      
   20.48 +            s -a--C-> t     
   20.49 +            --> (if a:ext(C) 
   20.50 +                 then (f s) -a--A-> (f t)
   20.51 +                 else (f s)=(f t)))" 
   20.52 +
   20.53 +end
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Wed Apr 30 11:20:15 1997 +0200
    21.3 @@ -0,0 +1,510 @@
    21.4 +(*  Title:      HOLCF/IOA/meta_theory/Seq.ML
    21.5 +    ID:        
    21.6 +    Author:     Olaf M"uller
    21.7 +    Copyright   1996  TU Muenchen
    21.8 +
    21.9 +*)  
   21.10 +
   21.11 +Addsimps (sfinite.intrs @ seq.rews);
   21.12 +
   21.13 +
   21.14 +(* Instead of adding UU_neq_nil every equation UU~=x could be changed to x~=UU *)
   21.15 +goal thy "UU ~=nil";
   21.16 +by (res_inst_tac [("s1","UU"),("t1","nil")]  (sym RS rev_contrapos) 1);
   21.17 +by (REPEAT (Simp_tac 1));
   21.18 +qed"UU_neq_nil";
   21.19 +
   21.20 +Addsimps [UU_neq_nil];
   21.21 +
   21.22 +(* ------------------------------------------------------------------------------------- *)
   21.23 +
   21.24 +
   21.25 +(* ----------------------------------------------------  *)
   21.26 +       section "recursive equations of operators";
   21.27 +(* ----------------------------------------------------  *)
   21.28 +
   21.29 +
   21.30 +(* ----------------------------------------------------------- *)
   21.31 +(*                        smap                                 *)
   21.32 +(* ----------------------------------------------------------- *)
   21.33 +
   21.34 +bind_thm ("smap_unfold", fix_prover2 thy smap_def 
   21.35 +   "smap = (LAM f tr. case tr of  \
   21.36 + \                         nil   => nil \
   21.37 + \                       | x##xs => f`x ## smap`f`xs)");
   21.38 +
   21.39 +goal thy "smap`f`nil=nil"; 
   21.40 +by (stac smap_unfold 1);
   21.41 +by (Simp_tac 1);
   21.42 +qed"smap_nil";
   21.43 +
   21.44 +goal thy "smap`f`UU=UU"; 
   21.45 +by (stac smap_unfold 1);
   21.46 +by (Simp_tac 1);
   21.47 +qed"smap_UU";
   21.48 +
   21.49 +goal thy 
   21.50 +"!!x.[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; 
   21.51 +br trans 1;
   21.52 +by (stac smap_unfold 1);
   21.53 +by (Asm_full_simp_tac 1);
   21.54 +br refl 1;
   21.55 +qed"smap_cons";
   21.56 +
   21.57 +(* ----------------------------------------------------------- *)
   21.58 +(*                        sfilter                              *)
   21.59 +(* ----------------------------------------------------------- *)
   21.60 +
   21.61 +bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def 
   21.62 +  "sfilter = (LAM P tr. case tr of  \
   21.63 + \         nil   => nil \
   21.64 + \       | x##xs => If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)");
   21.65 +
   21.66 +goal thy "sfilter`P`nil=nil";
   21.67 +by (stac sfilter_unfold 1);
   21.68 +by (Simp_tac 1);
   21.69 +qed"sfilter_nil";
   21.70 +
   21.71 +goal thy "sfilter`P`UU=UU";
   21.72 +by (stac sfilter_unfold 1);
   21.73 +by (Simp_tac 1);
   21.74 +qed"sfilter_UU";
   21.75 +
   21.76 +goal thy 
   21.77 +"!!x.x~=UU ==> sfilter`P`(x##xs)=   \
   21.78 +\             (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
   21.79 +br trans 1;
   21.80 +by (stac sfilter_unfold 1);
   21.81 +by (Asm_full_simp_tac 1);
   21.82 +br refl 1;
   21.83 +qed"sfilter_cons";
   21.84 +
   21.85 +(* ----------------------------------------------------------- *)
   21.86 +(*                        sforall2                             *)
   21.87 +(* ----------------------------------------------------------- *)
   21.88 +
   21.89 +bind_thm ("sforall2_unfold", fix_prover2 thy sforall2_def 
   21.90 +   "sforall2 = (LAM P tr. case tr of  \
   21.91 + \                         nil   => TT \
   21.92 + \                       | x##xs => (P`x andalso sforall2`P`xs))");
   21.93 +
   21.94 +goal thy "sforall2`P`nil=TT"; 
   21.95 +by (stac sforall2_unfold 1);
   21.96 +by (Simp_tac 1);
   21.97 +qed"sforall2_nil";
   21.98 +
   21.99 +goal thy "sforall2`P`UU=UU"; 
  21.100 +by (stac sforall2_unfold 1);
  21.101 +by (Simp_tac 1);
  21.102 +qed"sforall2_UU";
  21.103 +
  21.104 +goal thy 
  21.105 +"!!x.x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
  21.106 +br trans 1;
  21.107 +by (stac sforall2_unfold 1);
  21.108 +by (Asm_full_simp_tac 1);
  21.109 +br refl 1;
  21.110 +qed"sforall2_cons";
  21.111 +
  21.112 +
  21.113 +(* ----------------------------------------------------------- *)
  21.114 +(*                        stakewhile                           *)
  21.115 +(* ----------------------------------------------------------- *)
  21.116 +
  21.117 +
  21.118 +bind_thm ("stakewhile_unfold", fix_prover2 thy stakewhile_def 
  21.119 +   "stakewhile = (LAM P tr. case tr of  \
  21.120 + \                         nil   => nil \
  21.121 + \                       | x##xs => (If P`x then x##(stakewhile`P`xs) else nil fi))");
  21.122 +
  21.123 +goal thy "stakewhile`P`nil=nil"; 
  21.124 +by (stac stakewhile_unfold 1);
  21.125 +by (Simp_tac 1);
  21.126 +qed"stakewhile_nil";
  21.127 +
  21.128 +goal thy "stakewhile`P`UU=UU"; 
  21.129 +by (stac stakewhile_unfold 1);
  21.130 +by (Simp_tac 1);
  21.131 +qed"stakewhile_UU";
  21.132 +
  21.133 +goal thy 
  21.134 +"!!x.x~=UU ==> stakewhile`P`(x##xs) =   \
  21.135 +\             (If P`x then x##(stakewhile`P`xs) else nil fi)";
  21.136 +br trans 1;
  21.137 +by (stac stakewhile_unfold 1);
  21.138 +by (Asm_full_simp_tac 1);
  21.139 +br refl 1;
  21.140 +qed"stakewhile_cons";
  21.141 +
  21.142 +(* ----------------------------------------------------------- *)
  21.143 +(*                        sdropwhile                           *)
  21.144 +(* ----------------------------------------------------------- *)
  21.145 +
  21.146 +
  21.147 +bind_thm ("sdropwhile_unfold", fix_prover2 thy sdropwhile_def 
  21.148 +   "sdropwhile = (LAM P tr. case tr of  \
  21.149 + \                         nil   => nil \
  21.150 + \                       | x##xs => (If P`x then sdropwhile`P`xs else tr fi))");
  21.151 +
  21.152 +goal thy "sdropwhile`P`nil=nil"; 
  21.153 +by (stac sdropwhile_unfold 1);
  21.154 +by (Simp_tac 1);
  21.155 +qed"sdropwhile_nil";
  21.156 +
  21.157 +goal thy "sdropwhile`P`UU=UU"; 
  21.158 +by (stac sdropwhile_unfold 1);
  21.159 +by (Simp_tac 1);
  21.160 +qed"sdropwhile_UU";
  21.161 +
  21.162 +goal thy 
  21.163 +"!!x.x~=UU ==> sdropwhile`P`(x##xs) =   \
  21.164 +\             (If P`x then sdropwhile`P`xs else x##xs fi)";
  21.165 +br trans 1;
  21.166 +by (stac sdropwhile_unfold 1);
  21.167 +by (Asm_full_simp_tac 1);
  21.168 +br refl 1;
  21.169 +qed"sdropwhile_cons";
  21.170 +
  21.171 +
  21.172 +(* ----------------------------------------------------------- *)
  21.173 +(*                        slast                                 *)
  21.174 +(* ----------------------------------------------------------- *)
  21.175 +
  21.176 +
  21.177 +bind_thm ("slast_unfold", fix_prover2 thy slast_def 
  21.178 +   "slast = (LAM tr. case tr of  \
  21.179 + \                         nil   => UU \
  21.180 + \                       | x##xs => (If is_nil`xs then x else slast`xs fi))");
  21.181 +
  21.182 +
  21.183 +goal thy "slast`nil=UU"; 
  21.184 +by (stac slast_unfold 1);
  21.185 +by (Simp_tac 1);
  21.186 +qed"slast_nil";
  21.187 +
  21.188 +goal thy "slast`UU=UU"; 
  21.189 +by (stac slast_unfold 1);
  21.190 +by (Simp_tac 1);
  21.191 +qed"slast_UU";
  21.192 +
  21.193 +goal thy 
  21.194 +"!!x.x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
  21.195 +br trans 1;
  21.196 +by (stac slast_unfold 1);
  21.197 +by (Asm_full_simp_tac 1);
  21.198 +br refl 1;
  21.199 +qed"slast_cons";
  21.200 +
  21.201 +
  21.202 +(* ----------------------------------------------------------- *)
  21.203 +(*                        sconc                                 *)
  21.204 +(* ----------------------------------------------------------- *)
  21.205 +
  21.206 +bind_thm ("sconc_unfold", fix_prover2 thy sconc_def 
  21.207 +   "sconc = (LAM t1 t2. case t1 of  \
  21.208 + \                         nil   => t2 \
  21.209 + \                       | x##xs => x ## (xs @@ t2))");
  21.210 +
  21.211 +
  21.212 +goal thy "nil @@ y = y"; 
  21.213 +by (stac sconc_unfold 1);
  21.214 +by (Simp_tac 1);
  21.215 +qed"sconc_nil";
  21.216 +
  21.217 +goal thy "UU @@ y=UU"; 
  21.218 +by (stac sconc_unfold 1);
  21.219 +by (Simp_tac 1);
  21.220 +qed"sconc_UU";
  21.221 +
  21.222 +goal thy "(x##xs) @@ y=x##(xs @@ y)";
  21.223 +br trans 1;
  21.224 +by (stac sconc_unfold 1);
  21.225 +by (Asm_full_simp_tac 1);
  21.226 +by (case_tac "x=UU" 1);
  21.227 +by (REPEAT (Asm_full_simp_tac 1));
  21.228 +qed"sconc_cons";
  21.229 +
  21.230 +Addsimps [sconc_nil, sconc_UU,sconc_cons];
  21.231 +
  21.232 +
  21.233 +(* ----------------------------------------------------------- *)
  21.234 +(*                        sflat                                 *)
  21.235 +(* ----------------------------------------------------------- *)
  21.236 +
  21.237 +bind_thm ("sflat_unfold", fix_prover2 thy sflat_def 
  21.238 +   "sflat = (LAM tr. case tr of  \
  21.239 + \                         nil   => nil \
  21.240 + \                       | x##xs => x @@ sflat`xs)");
  21.241 +
  21.242 +goal thy "sflat`nil=nil"; 
  21.243 +by (stac sflat_unfold 1);
  21.244 +by (Simp_tac 1);
  21.245 +qed"sflat_nil";
  21.246 +
  21.247 +goal thy "sflat`UU=UU"; 
  21.248 +by (stac sflat_unfold 1);
  21.249 +by (Simp_tac 1);
  21.250 +qed"sflat_UU";
  21.251 +
  21.252 +goal thy "sflat`(x##xs)= x@@(sflat`xs)"; 
  21.253 +br trans 1;
  21.254 +by (stac sflat_unfold 1);
  21.255 +by (Asm_full_simp_tac 1);
  21.256 +by (case_tac "x=UU" 1);
  21.257 +by (REPEAT (Asm_full_simp_tac 1));
  21.258 +qed"sflat_cons";
  21.259 +
  21.260 +
  21.261 +
  21.262 +
  21.263 +(* ----------------------------------------------------------- *)
  21.264 +(*                        szip                                 *)
  21.265 +(* ----------------------------------------------------------- *)
  21.266 +
  21.267 +bind_thm ("szip_unfold", fix_prover2 thy szip_def 
  21.268 +   "szip = (LAM t1 t2. case t1 of \
  21.269 +\               nil   => nil    \
  21.270 +\             | x##xs => (case t2 of     \
  21.271 +\                          nil => UU    \
  21.272 +\                        | y##ys => <x,y>##(szip`xs`ys)))");
  21.273 +
  21.274 +goal thy "szip`nil`y=nil"; 
  21.275 +by (stac szip_unfold 1);
  21.276 +by (Simp_tac 1);
  21.277 +qed"szip_nil";
  21.278 +
  21.279 +goal thy "szip`UU`y=UU"; 
  21.280 +by (stac szip_unfold 1);
  21.281 +by (Simp_tac 1);
  21.282 +qed"szip_UU1";
  21.283 +
  21.284 +goal thy "!!x. x~=nil ==> szip`x`UU=UU"; 
  21.285 +by (stac szip_unfold 1);
  21.286 +by (Asm_full_simp_tac 1);
  21.287 +by (res_inst_tac [("x","x")] seq.cases 1);
  21.288 +by (REPEAT (Asm_full_simp_tac 1));
  21.289 +qed"szip_UU2";
  21.290 +
  21.291 +goal thy "!!x.x~=UU ==> szip`(x##xs)`nil=UU";
  21.292 +br trans 1;
  21.293 +by (stac szip_unfold 1);
  21.294 +by (REPEAT (Asm_full_simp_tac 1));
  21.295 +qed"szip_cons_nil";
  21.296 +
  21.297 +goal thy "!!x.[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
  21.298 +br trans 1;
  21.299 +by (stac szip_unfold 1);
  21.300 +by (REPEAT (Asm_full_simp_tac 1));
  21.301 +qed"szip_cons";
  21.302 +
  21.303 +
  21.304 +Addsimps [sfilter_UU,sfilter_nil,sfilter_cons,
  21.305 +          smap_UU,smap_nil,smap_cons,
  21.306 +          sforall2_UU,sforall2_nil,sforall2_cons,
  21.307 +          slast_UU,slast_nil,slast_cons,
  21.308 +          stakewhile_UU, stakewhile_nil, stakewhile_cons, 
  21.309 +          sdropwhile_UU, sdropwhile_nil, sdropwhile_cons,
  21.310 +          sflat_UU,sflat_nil,sflat_cons,
  21.311 +          szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons]; 
  21.312 +
  21.313 +
  21.314 +
  21.315 +(* ------------------------------------------------------------------------------------- *)
  21.316 +
  21.317 +section "scons";
  21.318 +
  21.319 +goal thy 
  21.320 + "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
  21.321 +by (rtac iffI 1);
  21.322 +by (etac (hd seq.injects) 1);
  21.323 +auto();
  21.324 +qed"scons_inject_eq";
  21.325 +
  21.326 +
  21.327 +(* ------------------------------------------------------------------------------------- *)
  21.328 +
  21.329 +section "sfilter, sforall, sconc";
  21.330 +
  21.331 +
  21.332 +goal thy  "(if b then tr1 else tr2) @@ tr \
  21.333 +        \= (if b then tr1 @@ tr else tr2 @@ tr)";
  21.334 +by (res_inst_tac [("P","b"),("Q","b")] impCE 1);
  21.335 +by (fast_tac HOL_cs 1);
  21.336 +by (REPEAT (Asm_full_simp_tac 1));
  21.337 +qed"if_and_sconc";
  21.338 +
  21.339 +Addsimps [if_and_sconc];
  21.340 +
  21.341 +
  21.342 +goal thy "sfilter`P`(x @@ y) = (sfilter`P`x @@ sfilter`P`y)";
  21.343 +
  21.344 +by (res_inst_tac[("x","x")] seq.ind 1);
  21.345 +(* adm *)
  21.346 +by (Simp_tac 1);
  21.347 +(* base cases *)
  21.348 +by (Simp_tac 1);
  21.349 +by (Simp_tac 1);
  21.350 +(* main case *)
  21.351 +by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
  21.352 +qed"sfiltersconc";
  21.353 +
  21.354 +goal thy "sforall P (stakewhile`P`x)";
  21.355 +by (simp_tac (!simpset addsimps [sforall_def]) 1);
  21.356 +by (res_inst_tac[("x","x")] seq.ind 1);
  21.357 +(* adm *)
  21.358 +by (simp_tac (!simpset addsimps [adm_trick_1]) 1);
  21.359 +(* base cases *)
  21.360 +by (Simp_tac 1);
  21.361 +by (Simp_tac 1);
  21.362 +(* main case *)
  21.363 +by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
  21.364 +qed"sforallPstakewhileP";
  21.365 +
  21.366 +goal thy "sforall P (sfilter`P`x)";
  21.367 +by (simp_tac (!simpset addsimps [sforall_def]) 1);
  21.368 +by (res_inst_tac[("x","x")] seq.ind 1);
  21.369 +(* adm *)
  21.370 +(* FIX should be refined in _one_ tactic *)
  21.371 +by (simp_tac (!simpset addsimps [adm_trick_1]) 1);
  21.372 +(* base cases *)
  21.373 +by (Simp_tac 1);
  21.374 +by (Simp_tac 1);
  21.375 +(* main case *)
  21.376 +by (asm_full_simp_tac (!simpset setloop split_If_tac) 1);
  21.377 +qed"forallPsfilterP";
  21.378 +
  21.379 +
  21.380 +
  21.381 +(* ------------------------------------------------------------------------------------- *)
  21.382 +
  21.383 +section "Finite";
  21.384 +
  21.385 +(* ----------------------------------------------------  *)
  21.386 +(* Proofs of rewrite rules for Finite:                  *)
  21.387 +(* 1. Finite(nil),   (by definition)                    *)
  21.388 +(* 2. ~Finite(UU),                                      *)
  21.389 +(* 3. a~=UU==> Finite(a##x)=Finite(x)                  *)
  21.390 +(* ----------------------------------------------------  *)
  21.391 +
  21.392 +goal thy "Finite x --> x~=UU";
  21.393 +br impI 1;
  21.394 +be sfinite.induct 1;
  21.395 + by (Asm_full_simp_tac 1);
  21.396 +by (Asm_full_simp_tac 1);
  21.397 +qed"Finite_UU_a";
  21.398 +
  21.399 +goal thy "~(Finite UU)";
  21.400 +by (cut_inst_tac [("x","UU")]Finite_UU_a  1);
  21.401 +by (fast_tac HOL_cs 1);
  21.402 +qed"Finite_UU";
  21.403 +
  21.404 +goal thy "Finite x --> a~=UU --> x=a##xs --> Finite xs";
  21.405 +by (strip_tac 1);
  21.406 +be sfinite.elim 1;
  21.407 +by (fast_tac (HOL_cs addss !simpset) 1);
  21.408 +by (fast_tac (HOL_cs addSDs seq.injects) 1);
  21.409 +qed"Finite_cons_a";
  21.410 +
  21.411 +goal thy "!!x.a~=UU ==>(Finite (a##x)) = (Finite x)";
  21.412 +by (rtac iffI 1);
  21.413 +by (rtac (Finite_cons_a RS mp RS mp RS mp) 1);
  21.414 +by (REPEAT (assume_tac 1));
  21.415 +by (fast_tac HOL_cs 1);
  21.416 +by (Asm_full_simp_tac 1);
  21.417 +qed"Finite_cons";
  21.418 +
  21.419 +Addsimps [Finite_UU];
  21.420 +
  21.421 +
  21.422 +(* ------------------------------------------------------------------------------------- *)
  21.423 +
  21.424 +section "induction";
  21.425 +
  21.426 +
  21.427 +(*--------------------------------   *)
  21.428 +(* Extensions to Induction Theorems  *)
  21.429 +(*--------------------------------   *)
  21.430 +
  21.431 +
  21.432 +qed_goalw "seq_finite_ind_lemma" thy  [seq.finite_def]
  21.433 +"(!!n.P(seq_take n`s)) ==>  seq_finite(s) -->P(s)"
  21.434 + (fn prems =>
  21.435 +        [
  21.436 +        (strip_tac 1),
  21.437 +        (etac exE 1),
  21.438 +        (etac subst 1),
  21.439 +        (resolve_tac prems 1)
  21.440 +        ]);
  21.441 +
  21.442 +
  21.443 +goal  thy 
  21.444 +"!!P.[|P(UU);P(nil);\
  21.445 +\  !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\
  21.446 +\  |] ==> seq_finite(s) --> P(s)";
  21.447 +by (rtac seq_finite_ind_lemma 1);
  21.448 +be seq.finite_ind 1;
  21.449 + ba 1;
  21.450 +by (Asm_full_simp_tac 1);
  21.451 +qed"seq_finite_ind";
  21.452 +
  21.453 +
  21.454 +
  21.455 +
  21.456 +(*
  21.457 +(* -----------------------------------------------------------------
  21.458 +   Fr"uhere Herleitung des endlichen Induktionsprinzips 
  21.459 +   aus dem seq_finite Induktionsprinzip.
  21.460 +   Problem bei admissibility von Finite-->seq_finite!
  21.461 +   Deshalb Finite jetzt induktiv und nicht mehr rekursiv definiert! 
  21.462 +   ------------------------------------------------------------------ *)
  21.463 +
  21.464 +goal thy "seq_finite nil";
  21.465 +by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1);
  21.466 +by (res_inst_tac [("x","Suc 0")] exI 1);
  21.467 +by (simp_tac (!simpset addsimps seq.rews) 1);
  21.468 +qed"seq_finite_nil";
  21.469 +
  21.470 +goal thy "seq_finite UU";
  21.471 +by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1);
  21.472 +qed"seq_finite_UU";
  21.473 +
  21.474 +Addsimps[seq_finite_nil,seq_finite_UU];
  21.475 +
  21.476 +goal HOL.thy "(B-->A) --> (A--> (B-->C))--> (B--> C)";
  21.477 +by (fast_tac HOL_cs 1);
  21.478 +qed"logic_lemma";
  21.479 +
  21.480 +
  21.481 +goal thy "!!P.[| P nil; \
  21.482 +\                !!a t. [|a~=UU;Finite t; P t|] ==> P (a##t)|]\
  21.483 +\            ==> Finite x --> P x";
  21.484 +
  21.485 +by (rtac (logic_lemma RS mp RS mp) 1);
  21.486 +by (rtac trf_impl_tf 1);
  21.487 +by (rtac seq_finite_ind 1);
  21.488 +by (simp_tac (!simpset addsimps [Finite_def]) 1);
  21.489 +by (simp_tac (!simpset addsimps [Finite_def]) 1);
  21.490 +by (asm_full_simp_tac (!simpset addsimps [Finite_def]) 1);
  21.491 +qed"Finite_ind";
  21.492 +
  21.493 +
  21.494 +goal thy "Finite tr --> seq_finite tr";
  21.495 +by (rtac seq.ind 1);
  21.496 +(* adm *)
  21.497 +(* hier grosses Problem !!!!!!!!!!!!!!! *)
  21.498 +
  21.499 +by (simp_tac (!simpset addsimps [Finite_def]) 2);
  21.500 +by (simp_tac (!simpset addsimps [Finite_def]) 2);
  21.501 +
  21.502 +(* main case *)
  21.503 +by (asm_full_simp_tac (!simpset addsimps [Finite_def,seq.sfinite_def]) 2);
  21.504 +by (rtac impI 2);
  21.505 +by (rotate_tac 2 2);
  21.506 +by (Asm_full_simp_tac 2);
  21.507 +by (etac exE 2);
  21.508 +by (res_inst_tac [("x","Suc n")] exI 2);
  21.509 +by (asm_full_simp_tac (!simpset addsimps seq.rews) 2);
  21.510 +qed"tf_is_trf";
  21.511 +
  21.512 +*)
  21.513 +
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Wed Apr 30 11:20:15 1997 +0200
    22.3 @@ -0,0 +1,124 @@
    22.4 +(*  Title:      HOLCF/IOA/meta_theory/Seq.thy
    22.5 +    ID:        
    22.6 +    Author:     Olaf M"uller
    22.7 +    Copyright   1996  TU Muenchen
    22.8 +
    22.9 +Partial, Finite and Infinite Sequences (lazy lists), modeled as domain.
   22.10 +*)  
   22.11 +
   22.12 +
   22.13 +Seq = HOLCF + 
   22.14 +
   22.15 +domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq)  (cinfixr 65) 
   22.16 +
   22.17 +
   22.18 +consts    
   22.19 +   sfilter       :: "('a -> tr) -> 'a seq -> 'a seq"  
   22.20 +   smap          :: "('a -> 'b) -> 'a seq -> 'b seq"
   22.21 +   sforall       :: "('a -> tr) => 'a seq => bool"
   22.22 +   sforall2      :: "('a -> tr) -> 'a seq -> tr"
   22.23 +   slast         :: "'a seq     -> 'a"
   22.24 +   sconc         :: "'a seq     -> 'a seq -> 'a seq"
   22.25 +   sdropwhile,
   22.26 +   stakewhile    ::"('a -> tr)  -> 'a seq -> 'a seq"  
   22.27 +   szip          ::"'a seq      -> 'b seq -> ('a*'b) seq"  
   22.28 +   sflat        :: "('a seq) seq  -> 'a seq"
   22.29 +
   22.30 +   sfinite       :: "'a seq set"
   22.31 +   Partial       ::"'a seq => bool"
   22.32 +   Infinite      ::"'a seq => bool"
   22.33 +
   22.34 +   nproj        :: "nat => 'a seq => 'a"
   22.35 +
   22.36 +syntax
   22.37 +   "@@"		:: "'a seq => 'a seq => 'a seq"	(infixr 65)
   22.38 +   "Finite"     :: "'a seq => bool"
   22.39 +
   22.40 +translations
   22.41 +   "xs @@ ys" == "sconc`xs`ys"
   22.42 +   "Finite x" == "x:sfinite"
   22.43 +   "~(Finite x)" =="x~:sfinite"
   22.44 +
   22.45 +defs 
   22.46 +
   22.47 +
   22.48 +
   22.49 +(* f not possible at lhs, as "pattern matching" only for % x arguments,
   22.50 +   f cannot be written at rhs in front, as fix_eq3 does not apply later *)
   22.51 +smap_def
   22.52 +  "smap == (fix`(LAM h f tr. case tr of 
   22.53 +      nil   => nil
   22.54 +    | x##xs => f`x ## h`f`xs))"
   22.55 +
   22.56 +sfilter_def       
   22.57 +  "sfilter == (fix`(LAM h P t. case t of 
   22.58 +	   nil => nil
   22.59 +	 | x##xs => If P`x                                 
   22.60 +                    then x##(h`P`xs)
   22.61 +                    else     h`P`xs
   22.62 +                    fi))" 
   22.63 +sforall_def
   22.64 +  "sforall P t == (sforall2`P`t ~=FF)" 
   22.65 +
   22.66 +
   22.67 +sforall2_def
   22.68 +  "sforall2 == (fix`(LAM h P t. case t of 
   22.69 +	   nil => TT
   22.70 +	 | x##xs => P`x andalso h`P`xs))"
   22.71 +  
   22.72 +sconc_def
   22.73 +  "sconc == (fix`(LAM h t1 t2. case t1 of 
   22.74 +               nil       => t2
   22.75 +             | x##xs => x##(h`xs`t2)))"
   22.76 +
   22.77 +slast_def
   22.78 +  "slast == (fix`(LAM h t. case t of 
   22.79 +	   nil => UU
   22.80 +	 | x##xs => (If is_nil`xs                              
   22.81 +                          then x
   22.82 +                         else h`xs fi)))"
   22.83 +
   22.84 +stakewhile_def      
   22.85 +  "stakewhile == (fix`(LAM h P t. case t of 
   22.86 +	   nil => nil
   22.87 +	 | x##xs => If P`x                                 
   22.88 +                    then x##(h`P`xs)
   22.89 +                    else nil
   22.90 +                    fi))" 
   22.91 +sdropwhile_def
   22.92 +  "sdropwhile == (fix`(LAM h P t. case t of 
   22.93 +	   nil => nil
   22.94 +	 | x##xs => If P`x                                 
   22.95 +                    then h`P`xs
   22.96 +                    else t
   22.97 +                    fi))" 
   22.98 +sflat_def
   22.99 +  "sflat == (fix`(LAM h t. case t of 
  22.100 +	   nil => nil
  22.101 +	 | x##xs => x @@ (h`xs)))"
  22.102 +
  22.103 +szip_def
  22.104 +  "szip == (fix`(LAM h t1 t2. case t1 of 
  22.105 +               nil   => nil
  22.106 +             | x##xs => (case t2 of 
  22.107 +                          nil => UU 
  22.108 +                        | y##ys => <x,y>##(h`xs`ys))))"
  22.109 +
  22.110 +
  22.111 +proj_def 
  22.112 + "nproj == (%n tr.HD`(iterate n TL tr))"   
  22.113 +
  22.114 +Partial_def
  22.115 +  "Partial x  == (seq_finite x) & ~(Finite x)"
  22.116 +
  22.117 +Infinite_def
  22.118 +  "Infinite x == ~(seq_finite x)"
  22.119 +
  22.120 +
  22.121 +inductive "sfinite" 
  22.122 +   intrs  
  22.123 +    sfinite_0  "nil:sfinite"
  22.124 +    sfinite_n  "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite"
  22.125 +
  22.126 +
  22.127 +end
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Apr 30 11:20:15 1997 +0200
    23.3 @@ -0,0 +1,851 @@
    23.4 +(*  Title:      HOLCF/IOA/meta_theory/Sequence.ML
    23.5 +    ID:        
    23.6 +    Author:     Olaf M"uller
    23.7 +    Copyright   1996  TU Muenchen
    23.8 +
    23.9 +Theorems about Sequences over flat domains with lifted elements
   23.10 +
   23.11 +*)
   23.12 +
   23.13 +
   23.14 +Addsimps [andalso_and,andalso_or];
   23.15 +
   23.16 +(* ----------------------------------------------------------------------------------- *)
   23.17 +
   23.18 +section "recursive equations of operators";
   23.19 +
   23.20 +(* ---------------------------------------------------------------- *)
   23.21 +(*                               Map                                *)
   23.22 +(* ---------------------------------------------------------------- *)
   23.23 +
   23.24 +goal thy "Map f`UU =UU";
   23.25 +by (simp_tac (!simpset addsimps [Map_def]) 1);
   23.26 +qed"Map_UU";
   23.27 +
   23.28 +goal thy "Map f`nil =nil";
   23.29 +by (simp_tac (!simpset addsimps [Map_def]) 1);
   23.30 +qed"Map_nil";
   23.31 +
   23.32 +goal thy "Map f`(x>>xs)=(f x) >> Map f`xs";
   23.33 +by (simp_tac (!simpset addsimps [Map_def, Cons_def,flift2_def]) 1);
   23.34 +qed"Map_cons";
   23.35 +
   23.36 +(* ---------------------------------------------------------------- *)
   23.37 +(*                               Filter                             *)
   23.38 +(* ---------------------------------------------------------------- *)
   23.39 +
   23.40 +goal thy "Filter P`UU =UU";
   23.41 +by (simp_tac (!simpset addsimps [Filter_def]) 1);
   23.42 +qed"Filter_UU";
   23.43 +
   23.44 +goal thy "Filter P`nil =nil";
   23.45 +by (simp_tac (!simpset addsimps [Filter_def]) 1);
   23.46 +qed"Filter_nil";
   23.47 +
   23.48 +goal thy "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)"; 
   23.49 +by (simp_tac (!simpset addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1);
   23.50 +qed"Filter_cons";
   23.51 +
   23.52 +(* ---------------------------------------------------------------- *)
   23.53 +(*                               Forall                             *)
   23.54 +(* ---------------------------------------------------------------- *)
   23.55 +
   23.56 +goal thy "Forall P UU";
   23.57 +by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1);
   23.58 +qed"Forall_UU";
   23.59 +
   23.60 +goal thy "Forall P nil";
   23.61 +by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1);
   23.62 +qed"Forall_nil";
   23.63 +
   23.64 +goal thy "Forall P (x>>xs)= (P x & Forall P xs)";
   23.65 +by (simp_tac (!simpset addsimps [Forall_def, sforall_def,
   23.66 +                                 Cons_def,flift2_def]) 1);
   23.67 +qed"Forall_cons";
   23.68 +
   23.69 +(* ---------------------------------------------------------------- *)
   23.70 +(*                               Conc                               *)
   23.71 +(* ---------------------------------------------------------------- *)
   23.72 +
   23.73 +goal thy "UU @@ y =UU";
   23.74 +by (Simp_tac 1);
   23.75 +qed"Conc_UU";
   23.76 +
   23.77 +goal thy "nil @@ y =y";
   23.78 +by (Simp_tac 1);
   23.79 +qed"Conc_nil";
   23.80 +
   23.81 +goal thy "(x>>xs) @@ y = x>>(xs @@y)"; 
   23.82 +by (simp_tac (!simpset addsimps [Cons_def]) 1);
   23.83 +qed"Conc_cons";
   23.84 +
   23.85 +(* ---------------------------------------------------------------- *)
   23.86 +(*                               Takewhile                          *)
   23.87 +(* ---------------------------------------------------------------- *)
   23.88 +
   23.89 +goal thy "Takewhile P`UU =UU";
   23.90 +by (simp_tac (!simpset addsimps [Takewhile_def]) 1);
   23.91 +qed"Takewhile_UU";
   23.92 +
   23.93 +goal thy "Takewhile P`nil =nil";
   23.94 +by (simp_tac (!simpset addsimps [Takewhile_def]) 1);
   23.95 +qed"Takewhile_nil";
   23.96 +
   23.97 +goal thy "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)"; 
   23.98 +by (simp_tac (!simpset addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1);
   23.99 +qed"Takewhile_cons";
  23.100 +
  23.101 +(* ---------------------------------------------------------------- *)
  23.102 +(*                               Dropwhile                          *)
  23.103 +(* ---------------------------------------------------------------- *)
  23.104 +
  23.105 +goal thy "Dropwhile P`UU =UU";
  23.106 +by (simp_tac (!simpset addsimps [Dropwhile_def]) 1);
  23.107 +qed"Dropwhile_UU";
  23.108 +
  23.109 +goal thy "Dropwhile P`nil =nil";
  23.110 +by (simp_tac (!simpset addsimps [Dropwhile_def]) 1);
  23.111 +qed"Dropwhile_nil";
  23.112 +
  23.113 +goal thy "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)"; 
  23.114 +by (simp_tac (!simpset addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1);
  23.115 +qed"Dropwhile_cons";
  23.116 +
  23.117 +(* ---------------------------------------------------------------- *)
  23.118 +(*                               Last                               *)
  23.119 +(* ---------------------------------------------------------------- *)
  23.120 +
  23.121 +
  23.122 +goal thy "Last`UU =UU";
  23.123 +by (simp_tac (!simpset addsimps [Last_def]) 1);
  23.124 +qed"Last_UU";
  23.125 +
  23.126 +goal thy "Last`nil =UU";
  23.127 +by (simp_tac (!simpset addsimps [Last_def]) 1);
  23.128 +qed"Last_nil";
  23.129 +
  23.130 +goal thy "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)"; 
  23.131 +by (simp_tac (!simpset addsimps [Last_def, Cons_def]) 1);
  23.132 +by (res_inst_tac [("x","xs")] seq.cases 1);
  23.133 +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  23.134 +by (REPEAT (Asm_simp_tac 1));
  23.135 +qed"Last_cons";
  23.136 +
  23.137 +
  23.138 +(* ---------------------------------------------------------------- *)
  23.139 +(*                               Flat                               *)
  23.140 +(* ---------------------------------------------------------------- *)
  23.141 +
  23.142 +goal thy "Flat`UU =UU";
  23.143 +by (simp_tac (!simpset addsimps [Flat_def]) 1);
  23.144 +qed"Flat_UU";
  23.145 +
  23.146 +goal thy "Flat`nil =nil";
  23.147 +by (simp_tac (!simpset addsimps [Flat_def]) 1);
  23.148 +qed"Flat_nil";
  23.149 +
  23.150 +goal thy "Flat`(x##xs)= x @@ (Flat`xs)"; 
  23.151 +by (simp_tac (!simpset addsimps [Flat_def, Cons_def]) 1);
  23.152 +qed"Flat_cons";
  23.153 +
  23.154 +
  23.155 +(* ---------------------------------------------------------------- *)
  23.156 +(*                               Zip                                *)
  23.157 +(* ---------------------------------------------------------------- *)
  23.158 +
  23.159 +goal thy "Zip = (LAM t1 t2. case t1 of \
  23.160 +\               nil   => nil \
  23.161 +\             | x##xs => (case t2 of \ 
  23.162 +\                          nil => UU  \
  23.163 +\                        | y##ys => (case x of \
  23.164 +\                                      Undef  => UU \
  23.165 +\                                    | Def a => (case y of \
  23.166 +\                                                  Undef => UU \
  23.167 +\                                                | Def b => Def (a,b)##(Zip`xs`ys)))))";
  23.168 +by (rtac trans 1);
  23.169 +br fix_eq2 1;
  23.170 +br Zip_def 1;
  23.171 +br beta_cfun 1;
  23.172 +by (Simp_tac 1);
  23.173 +qed"Zip_unfold";
  23.174 +
  23.175 +goal thy "Zip`UU`y =UU";
  23.176 +by (stac Zip_unfold 1);
  23.177 +by (Simp_tac 1);
  23.178 +qed"Zip_UU1";
  23.179 +
  23.180 +goal thy "!! x. x~=nil ==> Zip`x`UU =UU";
  23.181 +by (stac Zip_unfold 1);
  23.182 +by (Simp_tac 1);
  23.183 +by (res_inst_tac [("x","x")] seq.cases 1);
  23.184 +by (REPEAT (Asm_full_simp_tac 1));
  23.185 +qed"Zip_UU2";
  23.186 +
  23.187 +goal thy "Zip`nil`y =nil";
  23.188 +by (stac Zip_unfold 1);
  23.189 +by (Simp_tac 1);
  23.190 +qed"Zip_nil";
  23.191 +
  23.192 +goal thy "Zip`(x>>xs)`nil= UU"; 
  23.193 +by (stac Zip_unfold 1);
  23.194 +by (simp_tac (!simpset addsimps [Cons_def]) 1);
  23.195 +qed"Zip_cons_nil";
  23.196 +
  23.197 +goal thy "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys"; 
  23.198 +br trans 1;
  23.199 +by (stac Zip_unfold 1);
  23.200 +by (Simp_tac 1);
  23.201 +(* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not 
  23.202 +  completely ready ? *)
  23.203 +by (simp_tac (!simpset addsimps [Cons_def]) 1);
  23.204 +qed"Zip_cons";
  23.205 +
  23.206 +
  23.207 +Delsimps [sfilter_UU,sfilter_nil,sfilter_cons,
  23.208 +          smap_UU,smap_nil,smap_cons,
  23.209 +          sforall2_UU,sforall2_nil,sforall2_cons,
  23.210 +          slast_UU,slast_nil,slast_cons,
  23.211 +          stakewhile_UU, stakewhile_nil, stakewhile_cons, 
  23.212 +          sdropwhile_UU, sdropwhile_nil, sdropwhile_cons,
  23.213 +          sflat_UU,sflat_nil,sflat_cons,
  23.214 +          szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons];
  23.215 +
  23.216 +
  23.217 +Addsimps [Filter_UU,Filter_nil,Filter_cons,
  23.218 +          Map_UU,Map_nil,Map_cons,
  23.219 +          Forall_UU,Forall_nil,Forall_cons,
  23.220 +          Last_UU,Last_nil,Last_cons,
  23.221 +          Conc_UU,Conc_nil,Conc_cons,
  23.222 +          Takewhile_UU, Takewhile_nil, Takewhile_cons, 
  23.223 +          Dropwhile_UU, Dropwhile_nil, Dropwhile_cons,
  23.224 +          Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons];
  23.225 +
  23.226 +
  23.227 +(*
  23.228 +
  23.229 +Can Filter with HOL predicate directly be defined as fixpoint ?
  23.230 +
  23.231 +goal thy "Filter2 P = (LAM tr. case tr of  \
  23.232 + \         nil   => nil \
  23.233 + \       | x##xs => (case x of Undef => UU | Def y => \
  23.234 +\                   (if P y then y>>(Filter2 P`xs) else Filter2 P`xs)))";
  23.235 +by (rtac trans 1);
  23.236 +br fix_eq2 1;
  23.237 +br Filter2_def 1;
  23.238 +br beta_cfun 1;
  23.239 +by (Simp_tac 1);
  23.240 +
  23.241 +is also possible, if then else has to be proven continuous and it would be nice if a case for 
  23.242 +Seq would be available.
  23.243 +
  23.244 +*)
  23.245 +
  23.246 +
  23.247 +(* ------------------------------------------------------------------------------------- *)
  23.248 +
  23.249 +
  23.250 +section "Cons";
  23.251 +
  23.252 +goal thy "a>>s = (Def a)##s";
  23.253 +by (simp_tac (!simpset addsimps [Cons_def]) 1);
  23.254 +qed"Cons_def2";
  23.255 +
  23.256 +goal thy "x = UU | x = nil | (? a s. x = a >> s)";
  23.257 +by (simp_tac (!simpset addsimps [Cons_def2]) 1);
  23.258 +by (cut_facts_tac [seq.exhaust] 1);
  23.259 +by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1);
  23.260 +qed"Seq_exhaust";
  23.261 +
  23.262 +
  23.263 +goal thy "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s  ==> P |] ==> P";
  23.264 +by (cut_inst_tac [("x","x")] Seq_exhaust 1);
  23.265 +be disjE 1;
  23.266 +by (Asm_full_simp_tac 1);
  23.267 +be disjE 1;
  23.268 +by (Asm_full_simp_tac 1);
  23.269 +by (REPEAT (etac exE 1));
  23.270 +by (Asm_full_simp_tac 1);
  23.271 +qed"Seq_cases";
  23.272 +
  23.273 +fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i
  23.274 +	  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
  23.275 +
  23.276 +(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
  23.277 +fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2)
  23.278 +                                             THEN Asm_full_simp_tac (i+1)
  23.279 +                                             THEN Asm_full_simp_tac i;
  23.280 +
  23.281 +goal thy "a>>s ~= UU";
  23.282 +by (stac Cons_def2 1);
  23.283 +by (resolve_tac seq.con_rews 1);
  23.284 +br Def_not_UU 1;
  23.285 +qed"Cons_not_UU";
  23.286 +
  23.287 +goal thy "~(a>>x) << UU";
  23.288 +by (rtac notI 1);
  23.289 +by (dtac antisym_less 1);
  23.290 +by (Simp_tac 1);
  23.291 +by (asm_full_simp_tac (!simpset addsimps [Cons_not_UU]) 1);
  23.292 +qed"Cons_not_less_UU";
  23.293 +
  23.294 +goal thy "~a>>s << nil";
  23.295 +by (stac Cons_def2 1);
  23.296 +by (resolve_tac seq.rews 1);
  23.297 +br Def_not_UU 1;
  23.298 +qed"Cons_not_less_nil";
  23.299 +
  23.300 +goal thy "a>>s ~= nil";
  23.301 +by (stac Cons_def2 1);
  23.302 +by (resolve_tac seq.rews 1);
  23.303 +qed"Cons_not_nil";
  23.304 +
  23.305 +goal thy "(a>>s = b>>t) = (a = b & s = t)";
  23.306 +by (simp_tac (HOL_ss addsimps [Cons_def2]) 1);
  23.307 +by (stac (hd lift.inject RS sym) 1);
  23.308 +back(); back();
  23.309 +by (rtac scons_inject_eq 1);
  23.310 +by (REPEAT(rtac Def_not_UU 1));
  23.311 +qed"Cons_inject_eq";
  23.312 +
  23.313 +goal thy "(a>>s<<b>>t) = (a = b & s<<t)";
  23.314 +by (simp_tac (!simpset addsimps [Cons_def2]) 1);
  23.315 +by (stac (Def_inject_less_eq RS sym) 1);
  23.316 +back();
  23.317 +by (rtac iffI 1);
  23.318 +(* 1 *)
  23.319 +by (etac (hd seq.inverts) 1);
  23.320 +by (REPEAT(rtac Def_not_UU 1));
  23.321 +(* 2 *)
  23.322 +by (Asm_full_simp_tac 1);
  23.323 +by (etac conjE 1);
  23.324 +by (etac monofun_cfun_arg 1);
  23.325 +qed"Cons_inject_less_eq";
  23.326 +
  23.327 +goal thy "seq_take (Suc n)`(a>>x) = a>> (seq_take n`x)";
  23.328 +by (simp_tac (!simpset addsimps [Cons_def]) 1);
  23.329 +qed"seq_take_Cons";
  23.330 +
  23.331 +Addsimps [Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
  23.332 +          Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil];
  23.333 +
  23.334 +
  23.335 +(* ----------------------------------------------------------------------------------- *)
  23.336 +
  23.337 +section "induction";
  23.338 +
  23.339 +goal thy "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x";
  23.340 +be seq.ind 1;
  23.341 +by (REPEAT (atac 1));
  23.342 +by (def_tac 1);
  23.343 +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
  23.344 +qed"Seq_induct";
  23.345 +
  23.346 +goal thy "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]  \
  23.347 +\               ==> seq_finite x --> P x";
  23.348 +be seq_finite_ind 1;
  23.349 +by (REPEAT (atac 1));
  23.350 +by (def_tac 1);
  23.351 +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
  23.352 +qed"Seq_FinitePartial_ind";
  23.353 +
  23.354 +goal thy "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
  23.355 +be sfinite.induct 1;
  23.356 +ba 1;
  23.357 +by (def_tac 1);
  23.358 +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
  23.359 +qed"Seq_Finite_ind"; 
  23.360 +
  23.361 +
  23.362 +(* rws are definitions to be unfolded for admissibility check *)
  23.363 +fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
  23.364 +                         THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
  23.365 +                         THEN simp_tac (!simpset addsimps rws) i;
  23.366 +
  23.367 +fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
  23.368 +                              THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
  23.369 +
  23.370 +fun pair_tac s = res_inst_tac [("p",s)] PairE
  23.371 +			  THEN' hyp_subst_tac THEN' Asm_full_simp_tac;
  23.372 +
  23.373 +(* induction on a sequence of pairs with pairsplitting and simplification *)
  23.374 +fun pair_induct_tac s rws i = 
  23.375 +           res_inst_tac [("x",s)] Seq_induct i 
  23.376 +           THEN pair_tac "a" (i+3) 
  23.377 +           THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1)))) 
  23.378 +           THEN simp_tac (!simpset addsimps rws) i;
  23.379 +
  23.380 +
  23.381 +
  23.382 +(* ------------------------------------------------------------------------------------ *)
  23.383 +
  23.384 +section "HD,TL";
  23.385 +
  23.386 +goal thy "HD`(x>>y) = Def x";
  23.387 +by (simp_tac (!simpset addsimps [Cons_def]) 1);
  23.388 +qed"HD_Cons";
  23.389 +
  23.390 +goal thy "TL`(x>>y) = y";
  23.391 +by (simp_tac (!simpset addsimps [Cons_def]) 1);
  23.392 +qed"TL_Cons";
  23.393 +
  23.394 +Addsimps [HD_Cons,TL_Cons];
  23.395 +
  23.396 +(* ------------------------------------------------------------------------------------ *)
  23.397 +
  23.398 +section "Finite, Partial, Infinite";
  23.399 +
  23.400 +goal thy "Finite (a>>xs) = Finite xs";
  23.401 +by (simp_tac (!simpset addsimps [Cons_def2,Finite_cons]) 1);
  23.402 +qed"Finite_Cons";
  23.403 +
  23.404 +Addsimps [Finite_Cons];
  23.405 +
  23.406 +(* ------------------------------------------------------------------------------------ *)
  23.407 +
  23.408 +section "Conc";
  23.409 +
  23.410 +goal thy "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)";
  23.411 +by (Seq_Finite_induct_tac 1);
  23.412 +qed"Conc_cong";
  23.413 +
  23.414 +(* ------------------------------------------------------------------------------------ *)
  23.415 +
  23.416 +section "Last";
  23.417 +
  23.418 +goal thy "!! s.Finite s ==> s~=nil --> Last`s~=UU";
  23.419 +by (Seq_Finite_induct_tac  1);
  23.420 +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  23.421 +qed"Finite_Last1";
  23.422 +
  23.423 +goal thy "!! s. Finite s ==> Last`s=UU --> s=nil";
  23.424 +by (Seq_Finite_induct_tac  1);
  23.425 +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  23.426 +by (fast_tac HOL_cs 1);
  23.427 +qed"Finite_Last2";
  23.428 +
  23.429 +
  23.430 +(* ------------------------------------------------------------------------------------ *)
  23.431 +
  23.432 +
  23.433 +section "Filter, Conc";
  23.434 +
  23.435 +
  23.436 +goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
  23.437 +by (Seq_induct_tac "s" [Filter_def] 1);
  23.438 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  23.439 +qed"FilterPQ";
  23.440 +
  23.441 +goal thy "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)";
  23.442 +by (simp_tac (!simpset addsimps [Filter_def,sfiltersconc]) 1);
  23.443 +qed"FilterConc";
  23.444 +
  23.445 +(* ------------------------------------------------------------------------------------ *)
  23.446 +
  23.447 +section "Map";
  23.448 +
  23.449 +goal thy "Map f`(Map g`s) = Map (f o g)`s";
  23.450 +by (Seq_induct_tac "s" [] 1);
  23.451 +qed"MapMap";
  23.452 +
  23.453 +goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
  23.454 +by (Seq_induct_tac "x" [] 1);
  23.455 +qed"MapConc";
  23.456 +
  23.457 +goal thy "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)";
  23.458 +by (Seq_induct_tac "x" [] 1);
  23.459 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  23.460 +qed"MapFilter";
  23.461 +
  23.462 +
  23.463 +(* ------------------------------------------------------------------------------------ *)
  23.464 +
  23.465 +section "Forall, Conc";
  23.466 +
  23.467 +
  23.468 +goal thy "Forall P ys & (! x. P x --> Q x) \
  23.469 +\         --> Forall Q ys";
  23.470 +by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1);
  23.471 +qed"ForallPForallQ1";
  23.472 +
  23.473 +bind_thm ("ForallPForallQ",impI RSN (2,allI RSN (2,conjI RS (ForallPForallQ1 RS mp))));
  23.474 +
  23.475 +goal thy "(Forall P x & Forall P y) --> Forall P (x @@ y)";
  23.476 +by (Seq_induct_tac "x" [Forall_def,sforall_def] 1);
  23.477 +qed"Forall_Conc_impl";
  23.478 +
  23.479 +goal thy "!! x. Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)";
  23.480 +by (Seq_Finite_induct_tac  1);
  23.481 +qed"Forall_Conc";
  23.482 +
  23.483 +
  23.484 +(* ------------------------------------------------------------------------------------- *)
  23.485 +
  23.486 +section "Forall, Filter";
  23.487 +
  23.488 +
  23.489 +goal thy "Forall P (Filter P`x)";
  23.490 +by (simp_tac (!simpset addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
  23.491 +qed"ForallPFilterP";
  23.492 +
  23.493 +(* FIX: holds also in other direction, then equal to forallPfilterP *)
  23.494 +goal thy "Forall P x --> Filter P`x = x";
  23.495 +by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
  23.496 +qed"ForallPFilterPid1";
  23.497 +
  23.498 +val ForallPFilterPid = standard (ForallPFilterPid1 RS mp);
  23.499 +
  23.500 +
  23.501 +(* holds also in <-- direction. FIX: prove that also *)
  23.502 +
  23.503 +goal thy "!! P. Finite ys & Forall (%x. ~P x) ys \
  23.504 +\   --> Filter P`ys = nil ";
  23.505 +by (res_inst_tac[("x","ys")] Seq_induct 1);
  23.506 +(* adm *)
  23.507 +(* FIX: cont tfinite behandeln *)
  23.508 +br adm_all 1;
  23.509 +(* base cases *)
  23.510 +by (Simp_tac 1);
  23.511 +by (Simp_tac 1);
  23.512 +(* main case *)
  23.513 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  23.514 +qed"ForallnPFilterPnil1";
  23.515 +
  23.516 +val ForallnPFilterPnil = standard (conjI RS (ForallnPFilterPnil1 RS mp));
  23.517 +
  23.518 +
  23.519 +(* FIX: holds also in <== direction *)
  23.520 +goal thy   "!! P. ~Finite ys & Forall (%x. ~P x) ys \
  23.521 +\                  --> Filter P`ys = UU ";
  23.522 +by (res_inst_tac[("x","ys")] Seq_induct 1);
  23.523 +(* adm *)
  23.524 +(* FIX: cont ~tfinite behandeln *)
  23.525 +br adm_all 1;
  23.526 +(* base cases *)
  23.527 +by (Simp_tac 1);
  23.528 +by (Simp_tac 1);
  23.529 +(* main case *)
  23.530 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  23.531 +qed"ForallnPFilterPUU1";
  23.532 +
  23.533 +val ForallnPFilterPUU = standard (conjI RS (ForallnPFilterPUU1 RS mp));
  23.534 +
  23.535 +
  23.536 +goal thy  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
  23.537 +\   ==> Filter P`ys = nil";
  23.538 +be ForallnPFilterPnil 1;
  23.539 +be ForallPForallQ 1;
  23.540 +auto();
  23.541 +qed"ForallQFilterPnil";
  23.542 +
  23.543 +goal thy "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|] \
  23.544 +\   ==> Filter P`ys = UU ";
  23.545 +be ForallnPFilterPUU 1;
  23.546 +be ForallPForallQ 1;
  23.547 +auto();
  23.548 +qed"ForallQFilterPUU";
  23.549 +
  23.550 +
  23.551 +
  23.552 +(* ------------------------------------------------------------------------------------- *)
  23.553 +
  23.554 +section "Takewhile, Forall, Filter";
  23.555 +
  23.556 +
  23.557 +goal thy "Forall P (Takewhile P`x)";
  23.558 +by (simp_tac (!simpset addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1);
  23.559 +qed"ForallPTakewhileP";
  23.560 +
  23.561 +
  23.562 +goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
  23.563 +br ForallPForallQ 1;
  23.564 +br ForallPTakewhileP 1;
  23.565 +auto();
  23.566 +qed"ForallPTakewhileQ";
  23.567 +
  23.568 +
  23.569 +goal thy  "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \
  23.570 +\   ==> Filter P`(Takewhile Q`ys) = nil";
  23.571 +be ForallnPFilterPnil 1;
  23.572 +br ForallPForallQ 1;
  23.573 +br ForallPTakewhileP 1;
  23.574 +auto();
  23.575 +qed"FilterPTakewhileQnil";
  23.576 +
  23.577 +goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \
  23.578 +\            Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)";
  23.579 +br ForallPFilterPid 1;
  23.580 +br ForallPForallQ 1;
  23.581 +br ForallPTakewhileP 1;
  23.582 +auto();
  23.583 +qed"FilterPTakewhileQid";
  23.584 +
  23.585 +Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
  23.586 +          FilterPTakewhileQnil,FilterPTakewhileQid];
  23.587 +
  23.588 +
  23.589 +
  23.590 +(* ----------------------------------------------------------------------------------- *)
  23.591 +
  23.592 +
  23.593 +(*
  23.594 +section "admissibility";
  23.595 +
  23.596 +goal thy "adm(%x.~Finite x)";
  23.597 +br admI 1;
  23.598 +bd spec 1;
  23.599 +be contrapos 1;
  23.600 +
  23.601 +*)
  23.602 +
  23.603 +(* ----------------------------------------------------------------------------------- *)
  23.604 +
  23.605 +section "coinductive characterizations of Filter";
  23.606 +
  23.607 +
  23.608 +goal thy "HD`(Filter P`y) = Def x \
  23.609 +\         --> y = ((Takewhile (%x. ~P x)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y)))  \
  23.610 +\             & Finite (Takewhile (%x. ~ P x)`y)  & P x";
  23.611 +
  23.612 +(* FIX: pay attention: is only admissible with chain-finite package to be added to 
  23.613 +        adm test *)
  23.614 +by (Seq_induct_tac "y" [] 1);
  23.615 +br adm_all 1;
  23.616 +by (Asm_full_simp_tac 1); 
  23.617 +by (case_tac "P a" 1);
  23.618 +by (Asm_full_simp_tac 1); 
  23.619 +br impI 1;
  23.620 +by (hyp_subst_tac 1);
  23.621 +by (Asm_full_simp_tac 1); 
  23.622 +(* ~ P a *)
  23.623 +by (Asm_full_simp_tac 1); 
  23.624 +br impI 1;
  23.625 +by (rotate_tac ~1 1);
  23.626 +by (Asm_full_simp_tac 1); 
  23.627 +by (REPEAT (etac conjE 1));
  23.628 +ba 1;
  23.629 +qed"divide_Seq_lemma";
  23.630 +
  23.631 +goal thy "!! x. (x>>xs) << Filter P`y  \
  23.632 +\   ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
  23.633 +\      & Finite (Takewhile (%a. ~ P a)`y)  & P x";
  23.634 +br (divide_Seq_lemma RS mp) 1;
  23.635 +by (dres_inst_tac [("fo","HD"),("xa","x>>xs")]  monofun_cfun_arg 1);
  23.636 +by (Asm_full_simp_tac 1); 
  23.637 +qed"divide_Seq";
  23.638 +
  23.639 +
  23.640 +goal thy "~Forall P y --> (? x. HD`(Filter (%a. ~P a)`y) = Def x)";
  23.641 +(* FIX: pay attention: is only admissible with chain-finite package to be added to 
  23.642 +        adm test *)
  23.643 +by (Seq_induct_tac "y" [] 1);
  23.644 +br adm_all 1;
  23.645 +by (case_tac "P a" 1);
  23.646 +by (Asm_full_simp_tac 1); 
  23.647 +by (Asm_full_simp_tac 1); 
  23.648 +qed"nForall_HDFilter";
  23.649 +
  23.650 +
  23.651 +goal thy "!!y. ~Forall P y  \
  23.652 +\  ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
  23.653 +\      Finite (Takewhile P`y) & (~ P x)";
  23.654 +bd (nForall_HDFilter RS mp) 1;
  23.655 +by (safe_tac set_cs);
  23.656 +by (res_inst_tac [("x","x")] exI 1);
  23.657 +by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1);
  23.658 +auto();
  23.659 +qed"divide_Seq2";
  23.660 +
  23.661 +
  23.662 +goal thy  "!! y. ~Forall P y \
  23.663 +\  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
  23.664 +by (cut_inst_tac [] divide_Seq2 1);
  23.665 +auto();
  23.666 +qed"divide_Seq3";
  23.667 +
  23.668 +Addsimps [FilterPQ,FilterConc,Conc_cong,Forall_Conc];
  23.669 +
  23.670 +
  23.671 +(* ------------------------------------------------------------------------------------- *)
  23.672 +
  23.673 +
  23.674 +section "take_lemma";
  23.675 +
  23.676 +goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
  23.677 +by (rtac iffI 1);
  23.678 +br seq.take_lemma 1;
  23.679 +auto();
  23.680 +qed"seq_take_lemma";
  23.681 +
  23.682 +(*
  23.683 +
  23.684 +goal thy "Finite x & (! k. k < n --> seq_take k`y1 = seq_take k`y2) \
  23.685 +\   --> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2))";
  23.686 +br less_induct 1;
  23.687 +
  23.688 +
  23.689 +goal thy "!!x. Finite x ==> \
  23.690 +\  ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \
  23.691 +\   --> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2)))";
  23.692 +by (Seq_Finite_induct_tac 1);
  23.693 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  23.694 +
  23.695 +
  23.696 +qed"take_reduction";
  23.697 +*)
  23.698 +
  23.699 +goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
  23.700 +\           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
  23.701 +\                         ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |] \
  23.702 +\              ==> A x --> (f x)=(g x)";
  23.703 +by (case_tac "Forall Q x" 1);
  23.704 +by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  23.705 +qed"take_lemma_principle1";
  23.706 +
  23.707 +goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
  23.708 +\           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
  23.709 +\                         ==> ! n. seq_take n`(f (s1 @@ y>>s2)) \
  23.710 +\                                = seq_take n`(g (s1 @@ y>>s2)) |] \
  23.711 +\              ==> A x --> (f x)=(g x)";
  23.712 +by (case_tac "Forall Q x" 1);
  23.713 +by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  23.714 +br seq.take_lemma 1;
  23.715 +auto();
  23.716 +qed"take_lemma_principle2";
  23.717 +
  23.718 +
  23.719 +(* Note: in the following proofs the ordering of proof steps is very 
  23.720 +         important, as otherwise either (Forall Q s1) would be in the IH as
  23.721 +         assumption (then rule useless) or it is not possible to strengthen 
  23.722 +         the IH by doing a forall closure of the sequence t (then rule also useless).
  23.723 +         This is also the reason why the induction rule (less_induct or nat_induct) has to 
  23.724 +         to be imbuilt into the rule, as induction has to be done early and the take lemma 
  23.725 +         has to be used in the trivial direction afterwards for the (Forall Q x) case.  *)
  23.726 +
  23.727 +goal thy 
  23.728 +"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
  23.729 +\        !! s1 s2 y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\
  23.730 +\                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
  23.731 +\                         ==>   seq_take (Suc n)`(f (s1 @@ y>>s2)) \
  23.732 +\                             = seq_take (Suc n)`(g (s1 @@ y>>s2)) |] \
  23.733 +\              ==> A x --> (f x)=(g x)";
  23.734 +br impI 1;
  23.735 +br seq.take_lemma 1;
  23.736 +br mp 1;
  23.737 +ba 2;
  23.738 +by (res_inst_tac [("x","x")] spec 1);
  23.739 +br nat_induct 1;
  23.740 +by (Simp_tac 1);
  23.741 +br allI 1;
  23.742 +by (case_tac "Forall Q xa" 1);
  23.743 +by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
  23.744 +                           !simpset)) 1);
  23.745 +by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  23.746 +qed"take_lemma_induct";
  23.747 +
  23.748 +
  23.749 +goal thy 
  23.750 +"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
  23.751 +\        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m`(f t) = seq_take m`(g t);\
  23.752 +\                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \
  23.753 +\                         ==>   seq_take n`(f (s1 @@ y>>s2)) \
  23.754 +\                             = seq_take n`(g (s1 @@ y>>s2)) |] \
  23.755 +\              ==> A x --> (f x)=(g x)";
  23.756 +br impI 1;
  23.757 +br seq.take_lemma 1;
  23.758 +br mp 1;
  23.759 +ba 2;
  23.760 +by (res_inst_tac [("x","x")] spec 1);
  23.761 +br less_induct 1;
  23.762 +br allI 1;
  23.763 +by (case_tac "Forall Q xa" 1);
  23.764 +by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
  23.765 +                           !simpset)) 1);
  23.766 +by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  23.767 +qed"take_lemma_less_induct";
  23.768 +
  23.769 +goal thy 
  23.770 +"!! Q. [| A UU  ==> (f UU) = (g UU) ; \
  23.771 +\         A nil ==> (f nil) = (g nil) ; \
  23.772 +\         !! s y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\
  23.773 +\                    A (y>>s) |]   \
  23.774 +\                    ==>   seq_take (Suc n)`(f (y>>s)) \
  23.775 +\                        = seq_take (Suc n)`(g (y>>s)) |] \
  23.776 +\              ==> A x --> (f x)=(g x)";
  23.777 +br impI 1;
  23.778 +br seq.take_lemma 1;
  23.779 +br mp 1;
  23.780 +ba 2;
  23.781 +by (res_inst_tac [("x","x")] spec 1);
  23.782 +br nat_induct 1;
  23.783 +by (Simp_tac 1);
  23.784 +br allI 1;
  23.785 +by (Seq_case_simp_tac "xa" 1);
  23.786 +qed"take_lemma_in_eq_out";
  23.787 +
  23.788 +
  23.789 +(* ------------------------------------------------------------------------------------ *)
  23.790 +
  23.791 +section "alternative take_lemma proofs";
  23.792 +
  23.793 +
  23.794 +(* --------------------------------------------------------------- *)
  23.795 +(*              Alternative Proof of FilterPQ                      *)
  23.796 +(* --------------------------------------------------------------- *)
  23.797 +
  23.798 +Delsimps [FilterPQ];
  23.799 +
  23.800 +
  23.801 +(* In general: How to do this case without the same adm problems 
  23.802 +   as for the entire proof ? *) 
  23.803 +goal thy "Forall (%x.~(P x & Q x)) s \
  23.804 +\         --> Filter P`(Filter Q`s) =\
  23.805 +\             Filter (%x. P x & Q x)`s";
  23.806 +
  23.807 +by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
  23.808 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  23.809 +qed"Filter_lemma1";
  23.810 +
  23.811 +goal thy "!! s. Finite s ==>  \
  23.812 +\         (Forall (%x. (~P x) | (~ Q x)) s  \
  23.813 +\         --> Filter P`(Filter Q`s) = nil)";
  23.814 +by (Seq_Finite_induct_tac 1);
  23.815 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  23.816 +qed"Filter_lemma2";
  23.817 +
  23.818 +goal thy "!! s. Finite s ==>  \
  23.819 +\         Forall (%x. (~P x) | (~ Q x)) s  \
  23.820 +\         --> Filter (%x.P x & Q x)`s = nil";
  23.821 +by (Seq_Finite_induct_tac 1);
  23.822 +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
  23.823 +qed"Filter_lemma3";
  23.824 +
  23.825 +
  23.826 +goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
  23.827 +by (res_inst_tac [("A1","%x.True") 
  23.828 +                 ,("Q1","%x.~(P x & Q x)")]
  23.829 +                 (take_lemma_induct RS mp) 1);
  23.830 +(* FIX: rule always needs a back: eliminate *)
  23.831 +back();
  23.832 +(* FIX: better support for A = %.True *)
  23.833 +by (Fast_tac 3);
  23.834 +by (asm_full_simp_tac (!simpset addsimps [Filter_lemma1]) 1);
  23.835 +by (asm_full_simp_tac (!simpset addsimps [Filter_lemma2,Filter_lemma3] 
  23.836 +                                setloop split_tac [expand_if]) 1);
  23.837 +qed"FilterPQ_takelemma";
  23.838 +
  23.839 +Addsimps [FilterPQ];
  23.840 +
  23.841 +
  23.842 +(* --------------------------------------------------------------- *)
  23.843 +(*              Alternative Proof of MapConc                       *)
  23.844 +(* --------------------------------------------------------------- *)
  23.845 +
  23.846 +Delsimps [MapConc];
  23.847 +
  23.848 +goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
  23.849 +by (res_inst_tac [("A1","%x.True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
  23.850 +auto();
  23.851 +qed"MapConc_takelemma";
  23.852 +
  23.853 +Addsimps [MapConc];
  23.854 +
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Apr 30 11:20:15 1997 +0200
    24.3 @@ -0,0 +1,91 @@
    24.4 +(*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
    24.5 +    ID:        
    24.6 +    Author:     Olaf M"uller
    24.7 +    Copyright   1996  TU Muenchen
    24.8 +
    24.9 +Sequences over flat domains with lifted elements
   24.10 +
   24.11 +*)  
   24.12 +
   24.13 +Sequence = Seq + 
   24.14 +
   24.15 +default term
   24.16 +
   24.17 +types 'a Seq = ('a::term lift)seq
   24.18 +
   24.19 +ops curried
   24.20 +
   24.21 +  Cons             ::"'a            => 'a Seq -> 'a Seq"
   24.22 +  Filter           ::"('a => bool)  => 'a Seq -> 'a Seq"
   24.23 +  Map              ::"('a => 'b)    => 'a Seq -> 'b Seq"
   24.24 +  Forall           ::"('a => bool)  => 'a Seq => bool"
   24.25 +  Last             ::"'a Seq        -> 'a lift"
   24.26 +  Dropwhile,
   24.27 +  Takewhile        ::"('a => bool)  => 'a Seq -> 'a Seq" 
   24.28 +  Zip              ::"'a Seq        -> 'b Seq -> ('a * 'b) Seq"
   24.29 +  Flat             ::"('a Seq) seq   -> 'a Seq"
   24.30 +
   24.31 +  Filter2          ::"('a => bool)  => 'a Seq -> 'a Seq"
   24.32 +
   24.33 +syntax
   24.34 +
   24.35 + "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_>>_)"  [66,65] 65)
   24.36 +
   24.37 +syntax (symbols)
   24.38 +
   24.39 + "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_\\<leadsto>_)"  [66,65] 65)
   24.40 +
   24.41 +
   24.42 +translations
   24.43 +
   24.44 +  "a>>s" == "Cons a`s"
   24.45 +
   24.46 +defs
   24.47 +
   24.48 +
   24.49 +Cons_def      "Cons a == LAM s. Def a ## s"
   24.50 +
   24.51 +Filter_def    "Filter P == sfilter`(flift2 P)"
   24.52 +
   24.53 +Map_def       "Map f  == smap`(flift2 f)"
   24.54 +
   24.55 +Forall_def    "Forall P == sforall (flift2 P)"
   24.56 +
   24.57 +Last_def      "Last == slast"
   24.58 +
   24.59 +Dropwhile_def "Dropwhile P == sdropwhile`(flift2 P)"
   24.60 +
   24.61 +Takewhile_def "Takewhile P == stakewhile`(flift2 P)"
   24.62 +
   24.63 +Flat_def      "Flat == sflat"
   24.64 +
   24.65 +Zip_def
   24.66 +  "Zip == (fix`(LAM h t1 t2. case t1 of 
   24.67 +               nil   => nil
   24.68 +             | x##xs => (case t2 of 
   24.69 +                          nil => UU 
   24.70 +                        | y##ys => (case x of 
   24.71 +                                      Undef  => UU
   24.72 +                                    | Def a => (case y of 
   24.73 +                                                  Undef => UU
   24.74 +                                                | Def b => Def (a,b)##(h`xs`ys))))))"
   24.75 +
   24.76 +Filter2_def    "Filter2 P == (fix`(LAM h t. case t of 
   24.77 +            nil => nil
   24.78 +	  | x##xs => (case x of Undef => UU | Def y => (if P y                                 
   24.79 +                     then x##(h`xs)
   24.80 +                     else     h`xs))))" 
   24.81 +
   24.82 +rules
   24.83 +
   24.84 +
   24.85 +(* for test purposes should be deleted FIX !! *)
   24.86 +adm_all    "adm f"
   24.87 +
   24.88 +
   24.89 +take_reduction
   24.90 +  "[| Finite x; !! k. k < n ==> seq_take k`y1 = seq_take k`y2 |]
   24.91 +   ==> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2))"
   24.92 +
   24.93 +
   24.94 +end
   24.95 \ No newline at end of file
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Wed Apr 30 11:20:15 1997 +0200
    25.3 @@ -0,0 +1,11 @@
    25.4 +(*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
    25.5 +    ID:        
    25.6 +    Author:     Olaf M"uller
    25.7 +    Copyright   1997  TU Muenchen
    25.8 +
    25.9 +Some properties about cut(ex), defined as follows:
   25.10 +
   25.11 +For every execution ex there is another shorter execution cut(ex) 
   25.12 +that has the same trace as ex, but its schedule ends with an external action.
   25.13 +
   25.14 +*) 
   25.15 \ No newline at end of file
    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Wed Apr 30 11:20:15 1997 +0200
    26.3 @@ -0,0 +1,54 @@
    26.4 +(*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
    26.5 +    ID:        
    26.6 +    Author:     Olaf M"uller
    26.7 +    Copyright   1997  TU Muenchen
    26.8 +
    26.9 +Some properties about cut(ex), defined as follows:
   26.10 +
   26.11 +For every execution ex there is another shorter execution cut(ex) 
   26.12 +that has the same trace as ex, but its schedule ends with an external action.
   26.13 +
   26.14 +*) 
   26.15 +
   26.16 +
   26.17 +ShortExecutions = Traces + 
   26.18 +
   26.19 +consts 
   26.20 +
   26.21 +  LastActExtsch     ::"'a Seq  => bool"
   26.22 +  cutsch            ::"'a Seq => 'a Seq"
   26.23 +
   26.24 +
   26.25 +defs
   26.26 +
   26.27 +LastActExtsch_def
   26.28 +  "LastActExtsch sch == (cutsch sch = sch)"
   26.29 +
   26.30 +
   26.31 +rules
   26.32 +
   26.33 +exists_LastActExtsch
   26.34 +  "[|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|]
   26.35 +   ==> ? sch. sch : schedules A & 
   26.36 +              tr = Filter (%a.a:ext A)`sch &
   26.37 +              LastActExtsch sch"
   26.38 +
   26.39 +(* FIX: 1. LastActExtsch should have argument A also? 
   26.40 +        2. use equality: (I) f P x =UU <-> (II) (fa ~P x) & ~finite(x) to prove it for (II) instead *)
   26.41 +LastActExtimplUU
   26.42 +  "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = UU |]
   26.43 +   ==> sch=UU"
   26.44 +
   26.45 +(* FIX: see above *)
   26.46 +LastActExtimplnil
   26.47 +  "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = nil |]
   26.48 +   ==> sch=nil"
   26.49 +
   26.50 +LastActExtsmall1
   26.51 +  "LastActExtsch sch ==> LastActExtsch (TL`(Dropwhile P`sch))"
   26.52 +
   26.53 +LastActExtsmall2
   26.54 +  "[| Finite sch1; LastActExtsch (sch1 @@ sch2) |] ==> LastActExtsch (sch2)"
   26.55 +
   26.56 +end
   26.57 +
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Wed Apr 30 11:20:15 1997 +0200
    27.3 @@ -0,0 +1,152 @@
    27.4 +(*  Title:      HOLCF/IOA/meta_theory/Traces.ML
    27.5 +    ID:        
    27.6 +    Author:     Olaf M"uller
    27.7 +    Copyright   1996  TU Muenchen
    27.8 +
    27.9 +Theorems about Executions and Traces of I/O automata in HOLCF.
   27.10 +*)   
   27.11 +
   27.12 +
   27.13 +
   27.14 +val exec_rws = [executions_def,is_execution_fragment_def];
   27.15 +
   27.16 +
   27.17 +
   27.18 +(* ----------------------------------------------------------------------------------- *)
   27.19 +
   27.20 +section "recursive equations of operators";
   27.21 +
   27.22 +
   27.23 +(* ---------------------------------------------------------------- *)
   27.24 +(*                               filter_act                         *)
   27.25 +(* ---------------------------------------------------------------- *)
   27.26 +
   27.27 +
   27.28 +goal thy  "filter_act`UU = UU";
   27.29 +by (simp_tac (!simpset addsimps [filter_act_def]) 1);
   27.30 +qed"filter_act_UU";
   27.31 +
   27.32 +goal thy  "filter_act`nil = nil";
   27.33 +by (simp_tac (!simpset addsimps [filter_act_def]) 1);
   27.34 +qed"filter_act_nil";
   27.35 +
   27.36 +goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs";
   27.37 +by (simp_tac (!simpset addsimps [filter_act_def]) 1);
   27.38 +qed"filter_act_cons";
   27.39 +
   27.40 +Addsimps [filter_act_UU,filter_act_nil,filter_act_cons];
   27.41 +
   27.42 +
   27.43 +(* ---------------------------------------------------------------- *)
   27.44 +(*                             mk_trace                             *)
   27.45 +(* ---------------------------------------------------------------- *)
   27.46 +
   27.47 +goal thy "mk_trace A`UU=UU";
   27.48 +by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
   27.49 +qed"mk_trace_UU";
   27.50 +
   27.51 +goal thy "mk_trace A`nil=nil";
   27.52 +by (simp_tac (!simpset addsimps [mk_trace_def]) 1);
   27.53 +qed"mk_trace_nil";
   27.54 +
   27.55 +goal thy "mk_trace A`(at >> xs) =    \
   27.56 +\            (if ((fst at):ext A)    \       
   27.57 +\                 then (fst at) >> (mk_trace A`xs) \   
   27.58 +\                 else mk_trace A`xs)";
   27.59 +
   27.60 +by (asm_full_simp_tac (!simpset addsimps [mk_trace_def]) 1);
   27.61 +qed"mk_trace_cons";
   27.62 +
   27.63 +Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons];
   27.64 +
   27.65 +(* ---------------------------------------------------------------- *)
   27.66 +(*                             is_ex_fr                             *)
   27.67 +(* ---------------------------------------------------------------- *)
   27.68 +
   27.69 +
   27.70 +goal thy "is_ex_fr A = (LAM ex. (%s. case ex of \
   27.71 +\      nil => TT \
   27.72 +\    | x##xs => (flift1 \ 
   27.73 +\            (%p.Def ((s,p):trans_of A) andalso (is_ex_fr A`xs) (snd p)) \
   27.74 +\             `x) \
   27.75 +\   ))";
   27.76 +by (rtac trans 1);
   27.77 +br fix_eq2 1;
   27.78 +br is_ex_fr_def 1;
   27.79 +br beta_cfun 1;
   27.80 +by (simp_tac (!simpset addsimps [flift1_def]) 1);
   27.81 +qed"is_ex_fr_unfold";
   27.82 +
   27.83 +goal thy "(is_ex_fr A`UU) s=UU";
   27.84 +by (stac is_ex_fr_unfold 1);
   27.85 +by (Simp_tac 1);
   27.86 +qed"is_ex_fr_UU";
   27.87 +
   27.88 +goal thy "(is_ex_fr A`nil) s = TT";
   27.89 +by (stac is_ex_fr_unfold 1);
   27.90 +by (Simp_tac 1);
   27.91 +qed"is_ex_fr_nil";
   27.92 +
   27.93 +goal thy "(is_ex_fr A`(pr>>xs)) s = \
   27.94 +\                        (Def ((s,pr):trans_of A) \
   27.95 +\                andalso (is_ex_fr A`xs)(snd pr))";
   27.96 +br trans 1;
   27.97 +by (stac is_ex_fr_unfold 1);
   27.98 +by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
   27.99 +by (Simp_tac 1);
  27.100 +qed"is_ex_fr_cons";
  27.101 +
  27.102 +
  27.103 +Addsimps [is_ex_fr_UU,is_ex_fr_nil,is_ex_fr_cons];
  27.104 +
  27.105 +
  27.106 +(* ---------------------------------------------------------------- *)
  27.107 +(*                        is_execution_fragment                     *)
  27.108 +(* ---------------------------------------------------------------- *)
  27.109 +
  27.110 +goal thy "is_execution_fragment A (s, UU)";
  27.111 +by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1);
  27.112 +qed"is_execution_fragment_UU";
  27.113 +
  27.114 +goal thy "is_execution_fragment A (s, nil)";
  27.115 +by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1);
  27.116 +qed"is_execution_fragment_nil";
  27.117 +
  27.118 +goal thy "is_execution_fragment A (s, (a,t)>>ex) = \
  27.119 +\                               (((s,a,t):trans_of A) & \
  27.120 +\                               is_execution_fragment A (t, ex))";
  27.121 +by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1);
  27.122 +qed"is_execution_fragment_cons";
  27.123 +
  27.124 +
  27.125 +(* Delsimps [is_ex_fr_UU,is_ex_fr_nil,is_ex_fr_cons]; *)
  27.126 +Addsimps [is_execution_fragment_UU,is_execution_fragment_nil, is_execution_fragment_cons];  
  27.127 +
  27.128 +
  27.129 +(* -------------------------------------------------------------------------------- *)
  27.130 +
  27.131 +section "has_trace, mk_trace";
  27.132 +
  27.133 +(* alternative definition of has_trace tailored for the refinement proof, as it does not 
  27.134 +   take the detour of schedules *)
  27.135 +
  27.136 +goalw thy  [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] 
  27.137 +"has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))";
  27.138 +
  27.139 +by (safe_tac set_cs);
  27.140 +(* 1 *)
  27.141 +by (res_inst_tac[("x","ex")] bexI 1);
  27.142 +by (stac beta_cfun 1);
  27.143 +by (cont_tacR 1);
  27.144 +by (Simp_tac 1);
  27.145 +by (Asm_simp_tac 1);
  27.146 +(* 2 *)
  27.147 +by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1);
  27.148 +by (stac beta_cfun 1);
  27.149 +by (cont_tacR 1);
  27.150 +by (Simp_tac 1);
  27.151 +by (safe_tac set_cs);
  27.152 +by (res_inst_tac[("x","ex")] bexI 1);
  27.153 +by (REPEAT (Asm_simp_tac 1));
  27.154 +qed"has_trace_def2";
  27.155 +
    28.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Apr 30 11:20:15 1997 +0200
    28.3 @@ -0,0 +1,107 @@
    28.4 +(*  Title:      HOLCF/IOA/meta_theory/Traces.thy
    28.5 +    ID:        
    28.6 +    Author:     Olaf M"uller
    28.7 +    Copyright   1996  TU Muenchen
    28.8 +
    28.9 +Executions and Traces of I/O automata in HOLCF.
   28.10 +*)   
   28.11 +
   28.12 +		       
   28.13 +Traces = Automata + Sequence +
   28.14 +
   28.15 +default term
   28.16 + 
   28.17 +types  
   28.18 +   ('a,'s)pairs            =    "('a * 's) Seq"
   28.19 +   ('a,'s)execution        =    "'s * ('a,'s)pairs"
   28.20 +   'a trace                =    "'a Seq"
   28.21 + 
   28.22 +consts
   28.23 +
   28.24 +   (* Executions *)
   28.25 +  is_ex_fr      ::"('a,'s)ioa => ('a,'s)pairs -> ('s => tr)"
   28.26 +  is_execution_fragment,
   28.27 +  has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool"
   28.28 +  executions    :: "('a,'s)ioa => ('a,'s)execution set"
   28.29 +
   28.30 +  (* Schedules and traces *)
   28.31 +  filter_act    ::"('a,'s)pairs -> 'a trace"
   28.32 +  has_schedule,
   28.33 +  has_trace     :: "[('a,'s)ioa, 'a trace] => bool"
   28.34 +  schedules,
   28.35 +  traces        :: "('a,'s)ioa => 'a trace set"
   28.36 + 
   28.37 +  mk_trace      :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"
   28.38 +
   28.39 +  (* Notion of implementation *)
   28.40 +  "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool"   (infixr 12) 
   28.41 +
   28.42 +(*
   28.43 +(* FIX: introduce good symbol *)
   28.44 +syntax (symbols)
   28.45 +
   28.46 +  "op <<|"       ::"[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "\\<parallel>" 10)
   28.47 +*)
   28.48 +
   28.49 +
   28.50 +defs
   28.51 +
   28.52 +
   28.53 +(*  ------------------- Executions ------------------------------ *)
   28.54 +
   28.55 +
   28.56 +is_execution_fragment_def
   28.57 +  "is_execution_fragment A ex == ((is_ex_fr A`(snd ex)) (fst ex) ~= FF)"
   28.58 +
   28.59 +is_ex_fr_def
   28.60 +  "is_ex_fr A ==(fix`(LAM h ex. (%s. case ex of 
   28.61 +      nil => TT
   28.62 +    | x##xs => (flift1 
   28.63 +            (%p.Def ((s,p):trans_of A) andalso (h`xs) (snd p)) 
   28.64 +             `x)
   28.65 +   )))" 
   28.66 +  
   28.67 +executions_def
   28.68 +  "executions ioa == {e. ((fst e) : starts_of(ioa)) &               
   28.69 +                         is_execution_fragment ioa e}"
   28.70 +
   28.71 +
   28.72 +(*  ------------------- Schedules ------------------------------ *)
   28.73 +
   28.74 +
   28.75 +filter_act_def
   28.76 +  "filter_act == Map fst"
   28.77 +
   28.78 +has_schedule_def
   28.79 +  "has_schedule ioa sch ==                                               
   28.80 +     (? ex:executions ioa. sch = filter_act`(snd ex))"
   28.81 +
   28.82 +schedules_def
   28.83 +  "schedules ioa == {sch. has_schedule ioa sch}"
   28.84 +
   28.85 +
   28.86 +(*  ------------------- Traces ------------------------------ *)
   28.87 +
   28.88 +has_trace_def
   28.89 +  "has_trace ioa tr ==                                               
   28.90 +     (? sch:schedules ioa. tr = Filter (%a.a:ext(ioa))`sch)"
   28.91 +
   28.92 +traces_def
   28.93 +  "traces ioa == {tr. has_trace ioa tr}"
   28.94 +
   28.95 +
   28.96 +mk_trace_def
   28.97 +  "mk_trace ioa == LAM tr. 
   28.98 +     Filter (%a.a:ext(ioa))`(filter_act`tr)"
   28.99 +
  28.100 +
  28.101 +(*  ------------------- Implementation ------------------------------ *)
  28.102 +
  28.103 +ioa_implements_def
  28.104 +  "ioa1 =<| ioa2 ==   
  28.105 +    (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &   
  28.106 +     (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
  28.107 +      traces(ioa1) <= traces(ioa2))"
  28.108 +
  28.109 +
  28.110 +end
  28.111 \ No newline at end of file