Up to index of Isabelle/HOLCF/IOA
theory ShortExecutions(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy ID: $Id: ShortExecutions.thy,v 1.10 2005/09/03 20:27:06 wenzelm Exp $ Author: Olaf Müller *) theory ShortExecutions imports Traces begin 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. *} 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 A sch == (Cut (%x. x: ext A) sch = sch)" (* LastActExtex_def: "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *) Cut_def: "Cut P s == oraclebuild P$s$(Filter P$s)" oraclebuild_def: "oraclebuild P == (fix$(LAM h s t. case t of nil => nil | x##xs => (case x of UU => UU | Def y => (Takewhile (%x.~P x)$s) @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs)) ) ))" axioms Cut_prefixcl_Finite: "Finite s ==> (? y. s = Cut P s @@ y)" LastActExtsmall1: "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))" LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2" ML {* use_legacy_bindings (the_context ()) *} end
theorem oraclebuild_unfold:
oraclebuild P = (LAM s t. case t of nil => nil | x ## xs => case x of UU => UU | Def y => Takewhile (%a. ¬ P a)·s @@ y>>oraclebuild P·(TL·(Dropwhile (%a. ¬ P a)·s))·xs)
theorem oraclebuild_UU:
oraclebuild P·sch·UU = UU
theorem oraclebuild_nil:
oraclebuild P·sch·nil = nil
theorem oraclebuild_cons:
oraclebuild P·s·(x>>t) = Takewhile (%a. ¬ P a)·s @@ x>>oraclebuild P·(TL·(Dropwhile (%a. ¬ P a)·s))·t
theorem Cut_nil:
[| Forall (%a. ¬ P a) s; Finite s |] ==> Cut P s = nil
theorem Cut_UU:
[| Forall (%a. ¬ P a) s; ¬ Finite s |] ==> Cut P s = UU
theorem Cut_Cons:
[| P t; Forall (%x. ¬ P x) ss; Finite ss |] ==> Cut P (ss @@ t>>rs) = ss @@ t>>Cut P rs
theorem FilterCut:
Filter P·s = Filter P·(Cut P s)
theorem Cut_idemp:
Cut P (Cut P s) = Cut P s
theorem MapCut:
Map f·(Cut (P o f) s) = Cut P (Map f·s)
theorem Cut_prefixcl_nFinite:
¬ Finite s ==> Cut P s << s
theorem execThruCut:
is_exec_frag A (s, ex) ==> is_exec_frag A (s, Cut P ex)
theorem exists_LastActExtsch:
[| sch ∈ schedules A; tr = Filter (%a. a ∈ ext A)·sch |] ==> ∃sch. sch ∈ schedules A ∧ tr = Filter (%a. a ∈ ext A)·sch ∧ LastActExtsch A sch
theorem LastActExtimplnil:
[| LastActExtsch A sch; Filter (%x. x ∈ ext A)·sch = nil |] ==> sch = nil
theorem LastActExtimplUU:
[| LastActExtsch A sch; Filter (%x. x ∈ ext A)·sch = UU |] ==> sch = UU