# HG changeset patch
# User wenzelm
# Date 1125779226 -7200
# Node ID 526ff7cfd6ea67b4b1f219b9fc9d7971083dd02e
# Parent  f9c5cbdce4227ce27d00cb21a640e5e11e08471e
converted to Isar theory format;

diff -r f9c5cbdce422 -r 526ff7cfd6ea src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Sat Sep 03 21:51:10 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Sat Sep 03 22:27:06 2005 +0200
@@ -1,17 +1,12 @@
 (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
     ID:         $Id$
-    Author:     Olaf Mller
-
-Some properties about (Cut ex), defined as follows:
-
-For every execution ex there is another shorter execution (Cut ex) 
-that has the same trace as ex, but its schedule ends with an external action.
-*) 
+    Author:     Olaf Müller
+*)
 
 
 fun thin_tac' j =
   rotate_tac (j - 1) THEN'
-  etac thin_rl THEN' 
+  etac thin_rl THEN'
   rotate_tac (~ (j - 1));
 
 
@@ -21,11 +16,11 @@
 (* ---------------------------------------------------------------- *)
 
 
-bind_thm ("oraclebuild_unfold", fix_prover2 thy oraclebuild_def 
+bind_thm ("oraclebuild_unfold", fix_prover2 (the_context ()) oraclebuild_def
 "oraclebuild P = (LAM s t. case t of \
 \       nil => nil\
 \    | x##xs => \
-\      (case x of\ 
+\      (case x of\
 \        UU => UU\
 \      | Def y => (Takewhile (%a.~ P a)$s)\
 \                  @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))\
@@ -44,7 +39,7 @@
 
 Goal "oraclebuild P$s$(x>>t) = \
 \         (Takewhile (%a.~ P a)$s)   \
-\          @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))";     
+\          @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))";
 by (rtac trans 1);
 by (stac oraclebuild_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1);
@@ -53,7 +48,7 @@
 
 
 
- 
+
 (* ---------------------------------------------------------------- *)
                    section "Cut rewrite rules";
 (* ---------------------------------------------------------------- *)
@@ -133,14 +128,14 @@
                  (take_lemma_less_induct RS mp) 1);
 by (Fast_tac 3);
 by (case_tac "Finite s" 1);
-by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [Cut_nil]) 1);
 by (rtac (Cut_nil RS sym) 1);
-by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1);
 by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1);
 (* csae ~ Finite s *)
 by (asm_full_simp_tac (simpset() addsimps [Cut_UU]) 1);
 by (rtac (Cut_UU (*RS sym*)) 1);
-by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [ForallMap,o_def]) 1);
 by (asm_full_simp_tac (simpset() addsimps [Map2Finite]) 1);
 (* main case *)
 by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,MapConc,
diff -r f9c5cbdce422 -r 526ff7cfd6ea src/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Sep 03 21:51:10 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Sat Sep 03 22:27:06 2005 +0200
@@ -1,41 +1,44 @@
 (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
     ID:         $Id$
     Author:     Olaf Müller
+*)
 
-Some properties about (Cut ex), defined as follows:
+theory ShortExecutions
+imports Traces
+begin
 
-For every execution ex there is another shorter execution (Cut ex) 
-that has the same trace as ex, but its schedule ends with an external action.
-*) 
+text {*
+  Some properties about @{text "Cut ex"}, defined as follows:
 
+  For every execution ex there is another shorter execution @{text "Cut ex"}
+  that has the same trace as ex, but its schedule ends with an external action.
+*}
 
-ShortExecutions = Traces + 
-
-consts 
+consts
 
 (*  LastActExtex      ::"('a,'s)ioa => ('a,'s) pairs  => bool"*)
   LastActExtsch     ::"('a,'s)ioa => 'a Seq         => bool"
 
   Cut               ::"('a => bool) => 'a Seq    => 'a Seq"
- 
+
   oraclebuild       ::"('a => bool) => 'a Seq -> 'a Seq -> 'a Seq"
 
 defs
 
-LastActExtsch_def
+LastActExtsch_def:
   "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)"
 
-(* LastActExtex_def
+(* LastActExtex_def:
   "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
 
-Cut_def
+Cut_def:
   "Cut P s == oraclebuild P$s$(Filter P$s)"
 
-oraclebuild_def
-  "oraclebuild P == (fix$(LAM h s t. case t of 
+oraclebuild_def:
+  "oraclebuild P == (fix$(LAM h s t. case t of
        nil => nil
-    | x##xs => 
-      (case x of 
+    | x##xs =>
+      (case x of
         UU => UU
       | Def y => (Takewhile (%x.~P x)$s)
                   @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))
@@ -43,18 +46,17 @@
     ))"
 
 
-
+axioms
 
-rules
-
-Cut_prefixcl_Finite
+Cut_prefixcl_Finite:
   "Finite s ==> (? y. s = Cut P s @@ y)"
 
-LastActExtsmall1
+LastActExtsmall1:
   "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
 
-LastActExtsmall2
+LastActExtsmall2:
   "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
 
+ML {* use_legacy_bindings (the_context ()) *}
+
 end
-