|
(* Title: HOL/HOLCF/IOA/ShortExecutions.thy
Author: Olaf Müller
*)
theory ShortExecutions
imports Traces
begin
text \<open>
Some properties about \<open>Cut ex\<close>, defined as follows:
For every execution ex there is another shorter execution \<open>Cut ex\<close>
that has the same trace as ex, but its schedule ends with an external action.
\<close>
definition oraclebuild :: "('a \ bool) \ 'a Seq \ 'a Seq \ 'a Seq"
where "oraclebuild P =
(fix \<cdot>
(LAM h s t.
case t of
nil \<Rightarrow> nil
| x ## xs \<Rightarrow>
(case x of
UU \<Rightarrow> UU
| Def y \<Rightarrow>
(Takewhile (\<lambda>x. \<not> P x) \<cdot> s) @@
(y \<leadsto> (h \<cdot> (TL \<cdot> (Dropwhile (\<lambda>x. \<not> P x) \<cdot> s)) \<cdot> 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 \<open>
fun thin_tac' ctxt j =
rotate_tac (j - 1) THEN'
eresolve_tac ctxt [thin_rl] THEN'
rotate_tac (~ (j - 1))
\<close>
subsection \<open>\<open>oraclebuild\<close> rewrite rules\<close>
lemma oraclebuild_unfold:
"oraclebuild P =
(LAM s t.
case t of
nil \<Rightarrow> nil
| x ## xs \<Rightarrow>
(case x of
UU \<Rightarrow> UU
| Def y \<Rightarrow>
(Takewhile (\<lambda>a. \<not> P a) \<cdot> s) @@
(y \<leadsto> (oraclebuild P \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> s)) \<cdot> 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 (\<lambda>a. \<not> P a) \<cdot> s) @@
(x \<leadsto> (oraclebuild P \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> s)) \<cdot> t))"
apply (rule trans)
apply (subst oraclebuild_unfold)
apply (simp add: Consq_def)
apply (simp add: Consq_def)
done
subsection \<open>Cut rewrite rules\<close>
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 (simp add: oraclebuild_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 (simp add: oraclebuild_UU)
apply (rule ForallQFilterPUU)
apply assumption+
done
lemma Cut_Cons:
"P t \ Forall (\x. \ P x) ss \ Finite ss \
Cut P (ss @@ (t \<leadsto> rs)) = ss @@ (t \<leadsto> Cut P rs)"
apply (unfold Cut_def)
apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc)
done
subsection \<open>Cut lemmas for main theorem\<close>
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")
apply (simp add: Cut_nil ForallQFilterPnil)
apply (simp add: Cut_UU ForallQFilterPUU)
text \<open>main case\<close>
apply (simp add: Cut_Cons ForallQFilterPnil)
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")
apply (simp add: Cut_nil ForallQFilterPnil)
apply (simp add: Cut_UU ForallQFilterPUU)
text \<open>main case\<close>
apply (simp add: Cut_Cons ForallQFilterPnil)
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 (simp add: Cut_nil)
apply (rule Cut_nil [symmetric])
apply (simp add: ForallMap o_def)
apply (simp add: Map2Finite)
text \<open>case \<open>\<not> Finite s\<close>\<close>
apply (simp add: Cut_UU)
apply (rule Cut_UU)
apply (simp add: ForallMap o_def)
apply (simp add: Map2Finite)
text \<open>main case\<close>
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])
apply (simp add: Cut_UU)
text \<open>main case\<close>
apply (drule divide_Seq3)
apply (erule exE)+
apply (erule conjE)+
apply hypsubst
apply (simp add: Cut_Cons)
apply (rule take_reduction_less)
text \<open>auto makes also reasoning about Finiteness of parts of \<open>s\<close>!\<close>
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 \<open>Main Cut Theorem\<close>
lemma exists_LastActExtsch:
"sch \ schedules A \ tr = Filter (\a. a \ ext A) \ sch \
\<exists>sch. sch \<in> schedules A \<and> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> sch \<and> 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 (simp add: executions_def)
apply (pair ex)
apply auto
apply (rule_tac x = "(x1, Cut (\a. fst a \ ext A) x2)" in exI)
apply simp
text \<open>Subgoal 1: Lemma: propagation of execution through \<open>Cut\<close>\<close>
apply (simp add: execThruCut)
text \<open>Subgoal 2: Lemma: \<open>Filter P s = Filter P (Cut P s)\<close>\<close>
apply (simp add: filter_act_def)
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])
apply (simp add: FilterCut [symmetric])
text \<open>Subgoal 3: Lemma: \<open>Cut\<close> idempotent\<close>
apply (simp add: LastActExtsch_def filter_act_def)
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])
apply (simp add: Cut_idemp)
done
subsection \<open>Further Cut lemmas\<close>
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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
