# HG changeset patch
# User mueller
# Date 880477009 -3600
# Node ID 92707e24b62b62817428458e09f0943b4e470f81
# Parent  d30fbe1296831bd02f8820e1a60cb5c66cea4791
managed merge details;

diff -r d30fbe129683 -r 92707e24b62b src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Nov 25 16:34:20 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Nov 25 17:56:49 1997 +0100
@@ -359,6 +359,15 @@
          lemma for eliminating non admissible equations in assumptions      
   --------------------------------------------------------------------------- *)
 
+(* Versuich 
+goal thy "(y~= nil & Map fst`x <<y) --> x= Zip`y`(Map snd`x)";
+by (Seq_induct_tac "x" [] 1);
+by (Seq_case_simp_tac "y" 2);
+by (pair_tac "a" 1);
+by (Auto_tac());
+
+*)
+
 goal thy "!! sch ex. \
 \ Filter (%a. a:act AB)`sch = filter_act`ex  \
 \ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)";
diff -r d30fbe129683 -r 92707e24b62b src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Nov 25 16:34:20 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Nov 25 17:56:49 1997 +0100
@@ -105,14 +105,14 @@
                           nil => UU 
                         | y##ys => <x,y>##(h`xs`ys))))"
  
-
+(*
 nproj_def 
  "nproj == (%n tr.HD`(iterate n TL tr))"   
 
 
 sproj_def 
  "sproj == (%n tr.iterate n TL tr)"   
-
+*)
 
 
 Partial_def
diff -r d30fbe129683 -r 92707e24b62b src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Nov 25 16:34:20 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Tue Nov 25 17:56:49 1997 +0100
@@ -30,15 +30,23 @@
 syntax
 
  "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_>>_)"  [66,65] 65)
+ (* list Enumeration *)
+  "_totlist"      :: args => 'a Seq                          ("[(_)!]")
+  "_partlist"     :: args => 'a Seq                          ("[(_)?]")
+
 
 syntax (symbols)
 
  "@Cons"     ::"'a => 'a Seq => 'a Seq"       ("(_\\<leadsto>_)"  [66,65] 65)
-
+ 
 
 translations
 
   "a>>s" == "Cons a`s"
+  "[x, xs!]"     == "x>>[xs!]"
+  "[x!]"         == "x>>nil"
+  "[x, xs?]"     == "x>>[xs?]"
+  "[x?]"         == "x>>UU" 
 
 defs
 
diff -r d30fbe129683 -r 92707e24b62b src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Nov 25 16:34:20 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Nov 25 17:56:49 1997 +0100
@@ -251,6 +251,7 @@
 
 by (simp_tac (simpset() addsimps [filter_act_def]) 1);
 by (subgoal_tac "Map fst`(Cut (%a. fst a: ext A) y)= Cut (%a. a:ext A) (Map fst`y)" 1);
+
 by (rtac (rewrite_rule [o_def] MapCut) 2);
 by (asm_full_simp_tac (simpset() addsimps [FilterCut RS sym]) 1);
 
diff -r d30fbe129683 -r 92707e24b62b src/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue Nov 25 16:34:20 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Tue Nov 25 17:56:49 1997 +0100
@@ -15,7 +15,7 @@
 
 consts 
 
-  LastActExtex      ::"('a,'s)ioa => ('a,'s) pairs  => bool"
+(*  LastActExtex      ::"('a,'s)ioa => ('a,'s) pairs  => bool"*)
   LastActExtsch     ::"('a,'s)ioa => 'a Seq         => bool"
 
   Cut               ::"('a => bool) => 'a Seq    => 'a Seq"
@@ -27,8 +27,8 @@
 LastActExtsch_def
   "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)"
 
-LastActExtex_def
-  "LastActExtex A ex == LastActExtsch A (filter_act`ex)"
+(* LastActExtex_def
+  "LastActExtex A ex == LastActExtsch A (filter_act`ex)" *)
 
 Cut_def
   "Cut P s == oraclebuild P`s`(Filter P`s)"
diff -r d30fbe129683 -r 92707e24b62b src/HOLCF/IOA/meta_theory/Traces.ML
--- a/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Nov 25 16:34:20 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Nov 25 17:56:49 1997 +0100
@@ -189,6 +189,19 @@
 by (fast_tac (claset() addSIs [exec_in_sig]) 1);
 qed"scheds_in_sig";
 
+(*
+
+is ok but needs ForallQFilterP which has to been proven first (is trivial also)
+
+goalw thy [traces_def,has_trace_def]
+  "!! A.[| x:traces A |] ==> \
+\   Forall (%a. a:act A) x";
+ by (safe_tac set_cs );
+br ForallQFilterP 1;
+by (fast_tac (!claset addSIs [ext_is_act]) 1);
+qed"traces_in_sig";
+*)
+
 
 (* -------------------------------------------------------------------------------- *)