# HG changeset patch
# User mueller
# Date 873296730 -7200
# Node ID 2df8a2bc3ee26da5f7852eb88e31f4c5c43584ef
# Parent  0531f2c64c918efefc103b1ce5bc44087300c24c
some minor changes;

diff -r 0531f2c64c91 -r 2df8a2bc3ee2 src/HOLCF/IOA/meta_theory/Asig.ML
--- a/src/HOLCF/IOA/meta_theory/Asig.ML	Wed Sep 03 16:24:46 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Asig.ML	Wed Sep 03 16:25:30 1997 +0200
@@ -10,6 +10,13 @@
 
 val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def];
 
+goal thy
+ "(outputs    (a,b,c) = b)   & \
+\ (inputs     (a,b,c) = a) & \
+\ (internals  (a,b,c) = c)";
+  by (simp_tac (!simpset addsimps asig_projections) 1);
+qed "asig_triple_proj";
+
 goal thy "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)";
 by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1);
 qed"int_and_ext_is_act";
diff -r 0531f2c64c91 -r 2df8a2bc3ee2 src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Wed Sep 03 16:24:46 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Wed Sep 03 16:25:30 1997 +0200
@@ -100,6 +100,11 @@
       asig_outputs_def,Un_def,set_diff_def]) 1);
 qed"outputs_of_par";
 
+goal thy "int (A1||A2) =\
+\         (int A1) Un (int A2)";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
+      asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1);
+qed"internals_of_par";
 
 (* ---------------------------------------------------------------------------------- *)
 
@@ -262,7 +267,7 @@
 
 
 goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
-\             trans_of(restrict ioa acts) = trans_of(ioa)";
+\         trans_of(restrict ioa acts) = trans_of(ioa)";
 by (simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
 qed "cancel_restrict_a";
 
@@ -280,10 +285,18 @@
 by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
 qed "cancel_restrict_b";
 
+goal thy "act (restrict A acts) = act A";
+by (simp_tac (!simpset addsimps [actions_def,asig_internals_def,
+        asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def,
+        restrict_asig_def]) 1);
+auto();
+qed"acts_restrict";
+
 goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
-\             trans_of(restrict ioa acts) = trans_of(ioa) & \
-\             reachable (restrict ioa acts) s = reachable ioa s";
-by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b]) 1);
+\         trans_of(restrict ioa acts) = trans_of(ioa) & \
+\         reachable (restrict ioa acts) s = reachable ioa s & \
+\         act (restrict A acts) = act A";
+by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b,acts_restrict]) 1);
 qed"cancel_restrict";
 
 (* ---------------------------------------------------------------------------------- *)
@@ -394,45 +407,83 @@
 by (simp_tac (!simpset addsimps [actions_of_par,trans_of_par]) 1);
 qed"is_trans_of_par";
 
-
-(*
-
-goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 
+goalw thy [is_trans_of_def] 
 "!!A. is_trans_of A ==> is_trans_of (restrict A acts)";
-by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def,
-    asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,asig_of_def]) 1);
-
-qed"";
-
+by (asm_simp_tac (!simpset addsimps [cancel_restrict,acts_restrict])1);
+qed"is_trans_of_restrict";
 
 goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 
 "!!A. is_trans_of A ==> is_trans_of (rename A f)";
 by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def,
-    asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,asig_of_def]) 1);
-
-qed"";
-
-goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)";
-
-
-goalw thy [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def,
-           asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def] 
-"!! A. is_asig_of A ==> is_asig_of (restrict A f)";
-by (Asm_full_simp_tac 1);
-
-
-
+    asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,
+   asig_of_def,rename_def,rename_set_def]) 1);
+auto();
+qed"is_trans_of_rename";
 
 goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|]  \
 \         ==> is_asig_of (A||B)";
+by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def,asig_of_par,
+       asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
+     asig_inputs_def,actions_def,is_asig_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [asig_of_def]) 1);
+auto();
+by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
+qed"is_asig_of_par";
 
+goalw thy [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def,
+           asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] 
+"!! A. is_asig_of A ==> is_asig_of (restrict A f)";
+by (Asm_full_simp_tac 1);
+auto();
+by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
+qed"is_asig_of_restrict";
 
-
+goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)";
+by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def,
+     rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
+     asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
+auto(); 
+by (dres_inst_tac [("s","Some xb")] sym 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+by (dres_inst_tac [("s","Some xb")] sym 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+by (dres_inst_tac [("s","Some xb")] sym 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"is_asig_of_rename";
 
 
-*)
+Addsimps [is_asig_of_par,is_asig_of_restrict,is_asig_of_rename,
+          is_trans_of_par,is_trans_of_restrict,is_trans_of_rename];
 
 
-
+goalw thy [compatible_def]
+"!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
+by (asm_full_simp_tac (!simpset addsimps [internals_of_par, 
+   outputs_of_par,actions_of_par]) 1);
+auto();
+by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
+qed"compatible_par";
 
+(* FIX: better derive by previous one and compat_commute *)
+goalw thy [compatible_def]
+"!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
+by (asm_full_simp_tac (!simpset addsimps [internals_of_par, 
+   outputs_of_par,actions_of_par]) 1);
+auto();
+by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
+qed"compatible_par2";
 
+goalw thy [compatible_def]
+"!! A. [| compatible A B; (ext B - S) Int ext A = {}|] \
+\     ==> compatible A (restrict B S)";
+by (asm_full_simp_tac (!simpset addsimps [ioa_triple_proj,asig_triple_proj,
+          externals_def,restrict_def,restrict_asig_def,actions_def]) 1);
+by (auto_tac (!claset addEs [equalityCE],!simpset));
+qed"compatible_restrict";
+ 
\ No newline at end of file
diff -r 0531f2c64c91 -r 2df8a2bc3ee2 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Sep 03 16:24:46 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Sep 03 16:25:30 1997 +0200
@@ -7,6 +7,10 @@
 
 *)
 
+(* re-add extended adm_tactic, as it has been lost during theory merge *) 
+simpset := !simpset addSolver(fn thms =>
+            (adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
+
 Addsimps [andalso_and,andalso_or];
 
 (* ----------------------------------------------------------------------------------- *)
@@ -824,7 +828,7 @@
 \             & Finite (Takewhile (%x. ~ P x)`y)  & P x";
 
 (* FIX: pay attention: is only admissible with chain-finite package to be added to 
-        adm test *)
+        adm test and Finite f x admissibility *)
 by (Seq_induct_tac "y" [] 1);
 by (rtac adm_all 1);
 by (Asm_full_simp_tac 1); 
@@ -850,12 +854,11 @@
 by (Asm_full_simp_tac 1); 
 qed"divide_Seq";
 
-
+ 
 goal thy "~Forall P y --> (? x. HD`(Filter (%a. ~P a)`y) = Def x)";
-(* FIX: pay attention: is only admissible with chain-finite package to be added to 
+(* Pay attention: is only admissible with chain-finite package to be added to 
         adm test *)
-by (Seq_induct_tac "y" [] 1);
-by (rtac adm_all 1);
+by (Seq_induct_tac "y" [Forall_def,sforall_def] 1);
 by (case_tac "P a" 1);
 by (Asm_full_simp_tac 1); 
 by (Asm_full_simp_tac 1);