# Theory ShortExecutions

theory ShortExecutions
imports Traces
```(*  Title:      HOL/HOLCF/IOA/ShortExecutions.thy
Author:     Olaf MÃ¼ller
*)

theory ShortExecutions
imports Traces
begin

text ‹
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.
›

definition oraclebuild :: "('a ⇒ bool) ⇒ 'a Seq → 'a Seq → 'a Seq"
where "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)))))"

definition Cut :: "('a ⇒ bool) ⇒ 'a Seq ⇒ 'a Seq"
where "Cut P s = oraclebuild P ⋅ s ⋅ (Filter P ⋅ s)"

definition LastActExtsch :: "('a,'s) ioa ⇒ 'a Seq ⇒ bool"
where "LastActExtsch A sch ⟷ Cut (λx. x ∈ ext A) sch = sch"

axiomatization where
Cut_prefixcl_Finite: "Finite s ⟹ ∃y. s = Cut P s @@ y"

axiomatization where
LastActExtsmall1: "LastActExtsch A sch ⟹ LastActExtsch A (TL ⋅ (Dropwhile P ⋅ sch))"

axiomatization where
LastActExtsmall2: "Finite sch1 ⟹ LastActExtsch A (sch1 @@ sch2) ⟹ LastActExtsch A sch2"

ML ‹
fun thin_tac' ctxt j =
rotate_tac (j - 1) THEN'
eresolve_tac ctxt [thin_rl] THEN'
rotate_tac (~ (j - 1))
›

subsection ‹‹oraclebuild› rewrite rules›

lemma 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))))"
apply (rule trans)
apply (rule fix_eq2)
apply (simp only: oraclebuild_def)
apply (rule beta_cfun)
apply simp
done

lemma oraclebuild_UU: "oraclebuild P ⋅ sch ⋅ UU = UU"
apply (subst oraclebuild_unfold)
apply simp
done

lemma oraclebuild_nil: "oraclebuild P ⋅ sch ⋅ nil = nil"
apply (subst oraclebuild_unfold)
apply simp
done

lemma oraclebuild_cons:
"oraclebuild P ⋅ s ⋅ (x ↝ t) =
(Takewhile (λa. ¬ P a) ⋅ s) @@
(x ↝ (oraclebuild P ⋅ (TL ⋅ (Dropwhile (λa. ¬ P a) ⋅ s)) ⋅ t))"
apply (rule trans)
apply (subst oraclebuild_unfold)
done

subsection ‹Cut rewrite rules›

lemma Cut_nil: "Forall (λa. ¬ P a) s ⟹ Finite s ⟹ Cut P s = nil"
apply (unfold Cut_def)
apply (subgoal_tac "Filter P ⋅ s = nil")
apply (rule ForallQFilterPnil)
apply assumption+
done

lemma Cut_UU: "Forall (λa. ¬ P a) s ⟹ ¬ Finite s ⟹ Cut P s = UU"
apply (unfold Cut_def)
apply (subgoal_tac "Filter P ⋅ s = UU")
apply (rule ForallQFilterPUU)
apply assumption+
done

lemma Cut_Cons:
"P t ⟹ Forall (λx. ¬ P x) ss ⟹ Finite ss ⟹
Cut P (ss @@ (t ↝ rs)) = ss @@ (t ↝ Cut P rs)"
apply (unfold Cut_def)
apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc)
done

subsection ‹Cut lemmas for main theorem›

lemma FilterCut: "Filter P ⋅ s = Filter P ⋅ (Cut P s)"
apply (rule_tac A1 = "λx. True" and Q1 = "λx. ¬ P x" and x1 = "s" in take_lemma_induct [THEN mp])
prefer 3
apply fast
apply (case_tac "Finite s")
text ‹main case›
done

lemma Cut_idemp: "Cut P (Cut P s) = (Cut P s)"
apply (rule_tac A1 = "λx. True" and Q1 = "λx. ¬ P x" and x1 = "s" in
take_lemma_less_induct [THEN mp])
prefer 3
apply fast
apply (case_tac "Finite s")
text ‹main case›
apply (rule take_reduction)
apply auto
done

lemma MapCut: "Map f⋅(Cut (P ∘ f) s) = Cut P (Map f⋅s)"
apply (rule_tac A1 = "λx. True" and Q1 = "λx. ¬ P (f x) " and x1 = "s" in
take_lemma_less_induct [THEN mp])
prefer 3
apply fast
apply (case_tac "Finite s")
apply (rule Cut_nil [symmetric])
text ‹case ‹¬ Finite s››
apply (rule Cut_UU)
text ‹main case›
apply (simp add: Cut_Cons MapConc ForallMap FiniteMap1 o_def)
apply (rule take_reduction)
apply auto
done

lemma Cut_prefixcl_nFinite [rule_format]: "¬ Finite s ⟶ Cut P s ⊑ s"
apply (intro strip)
apply (rule take_lemma_less [THEN iffD1])
apply (intro strip)
apply (rule mp)
prefer 2
apply assumption
apply (tactic "thin_tac' @{context} 1 1")
apply (rule_tac x = "s" in spec)
apply (rule nat_less_induct)
apply (intro strip)
apply (rename_tac na n s)
apply (case_tac "Forall (λx. ¬ P x) s")
apply (rule take_lemma_less [THEN iffD2, THEN spec])
text ‹main case›
apply (drule divide_Seq3)
apply (erule exE)+
apply (erule conjE)+
apply hypsubst
apply (rule take_reduction_less)
text ‹auto makes also reasoning about Finiteness of parts of ‹s›!›
apply auto
done

lemma execThruCut: "is_exec_frag A (s, ex) ⟹ is_exec_frag A (s, Cut P ex)"
apply (case_tac "Finite ex")
apply (cut_tac s = "ex" and P = "P" in Cut_prefixcl_Finite)
apply assumption
apply (erule exE)
apply (rule exec_prefix2closed)
apply (erule_tac s = "ex" and t = "Cut P ex @@ y" in subst)
apply assumption
apply (erule exec_prefixclosed)
apply (erule Cut_prefixcl_nFinite)
done

subsection ‹Main Cut Theorem›

lemma 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"
apply (unfold schedules_def has_schedule_def [abs_def])
apply auto
apply (rule_tac x = "filter_act ⋅ (Cut (λa. fst a ∈ ext A) (snd ex))" in exI)
apply (pair ex)
apply auto
apply (rule_tac x = "(x1, Cut (λa. fst a ∈ ext A) x2)" in exI)
apply simp

text ‹Subgoal 1: Lemma:  propagation of execution through ‹Cut››

text ‹Subgoal 2:  Lemma:  ‹Filter P s = Filter P (Cut P s)››
apply (subgoal_tac "Map fst ⋅ (Cut (λa. fst a ∈ ext A) x2) = Cut (λa. a ∈ ext A) (Map fst ⋅ x2)")
apply (rule_tac [2] MapCut [unfolded o_def])

text ‹Subgoal 3: Lemma: ‹Cut› idempotent›
apply (subgoal_tac "Map fst ⋅ (Cut (λa. fst a ∈ ext A) x2) = Cut (λa. a ∈ ext A) (Map fst ⋅ x2)")
apply (rule_tac [2] MapCut [unfolded o_def])
done

subsection ‹Further Cut lemmas›

lemma LastActExtimplnil: "LastActExtsch A sch ⟹ Filter (λx. x ∈ ext A) ⋅ sch = nil ⟹ sch = nil"
apply (unfold LastActExtsch_def)
apply (drule FilternPnilForallP)
apply (erule conjE)
apply (drule Cut_nil)
apply assumption
apply simp
done

lemma LastActExtimplUU: "LastActExtsch A sch ⟹ Filter (λx. x ∈ ext A) ⋅ sch = UU ⟹ sch = UU"
apply (unfold LastActExtsch_def)
apply (drule FilternPUUForallP)
apply (erule conjE)
apply (drule Cut_UU)
apply assumption
apply simp
done

end
```