Quelle ShortExecutions.thy Sprache: Isabelle

(*  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

quality99%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.