Quelle Transitive_Closure_Table.thy Sprache: Isabelle

(*  Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen  *)

section \<open>A table-based implementation of the reflexive transitive closure\<close>

theory Transitive_Closure_Table
imports Main
begin

inductive rtrancl_path :: "('a \ 'a \ bool) \ 'a \ 'a list \ 'a \ bool"
  for r :: "'a \ 'a \ bool"
where
  base: "rtrancl_path r x [] x"
| step: "r x y \ rtrancl_path r y ys z \ rtrancl_path r x (y # ys) z"

lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y \ (\xs. rtrancl_path r x xs y)"
proof
  show "\xs. rtrancl_path r x xs y" if "r\<^sup>*\<^sup>* x y"
    using that
  proof (induct rule: converse_rtranclp_induct)
    case base
    have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
    then show ?case ..
  next
    case (step x z)
    from \<open>\<exists>xs. rtrancl_path r z xs y\<close>
    obtain xs where "rtrancl_path r z xs y" ..
    with \<open>r x z\<close> have "rtrancl_path r x (z # xs) y"
      by (rule rtrancl_path.step)
    then show ?case ..
  qed
  show "r\<^sup>*\<^sup>* x y" if "\xs. rtrancl_path r x xs y"
  proof -
    from that obtain xs where "rtrancl_path r x xs y" ..
    then show ?thesis
    proof induct
      case (base x)
      show ?case
        by (rule rtranclp.rtrancl_refl)
    next
      case (step x y ys z)
      from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case
        by (rule converse_rtranclp_into_rtranclp)
    qed
  qed
qed

lemma rtrancl_path_trans:
  assumes xy: "rtrancl_path r x xs y"
    and yz: "rtrancl_path r y ys z"
  shows "rtrancl_path r x (xs @ ys) z" using xy yz
proof (induct arbitrary: z)
  case (base x)
  then show ?case by simp
next
  case (step x y xs)
  then have "rtrancl_path r y (xs @ ys) z"
    by simp
  with \<open>r x y\<close> have "rtrancl_path r x (y # (xs @ ys)) z"
    by (rule rtrancl_path.step)
  then show ?case by simp
qed

lemma rtrancl_path_appendE:
  assumes xz: "rtrancl_path r x (xs @ y # ys) z"
  obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z"
  using xz
proof (induct xs arbitrary: x)
  case Nil
  then have "rtrancl_path r x (y # ys) z" by simp
  then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
    by cases auto
  from xy have "rtrancl_path r x [y] y"
    by (rule rtrancl_path.step [OF _ rtrancl_path.base])
  then have "rtrancl_path r x ([] @ [y]) y" by simp
  then show thesis using yz by (rule Nil)
next
  case (Cons a as)
  then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
  then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
    by cases auto
  show thesis
  proof (rule Cons(1) [OF _ az])
    assume "rtrancl_path r y ys z"
    assume "rtrancl_path r a (as @ [y]) y"
    with xa have "rtrancl_path r x (a # (as @ [y])) y"
      by (rule rtrancl_path.step)
    then have "rtrancl_path r x ((a # as) @ [y]) y"
      by simp
    then show thesis using \<open>rtrancl_path r y ys z\<close>
      by (rule Cons(2))
  qed
qed

lemma rtrancl_path_distinct:
  assumes xy: "rtrancl_path r x xs y"
  obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" and "set xs' \<subseteq> set xs"
  using xy
proof (induct xs rule: measure_induct_rule [of length])
  case (less xs)
  show ?case
  proof (cases "distinct (x # xs)")
    case True
    with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) simp
  next
    case False
    then have "\as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
      by (rule not_distinct_decomp)
    then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
      by iprover
    show ?thesis
    proof (cases as)
      case Nil
      with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
        by auto
      from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" "set cs \<subseteq> set xs"
        by (auto elim: rtrancl_path_appendE)
      from xs have "length cs < length xs" by simp
      then show ?thesis
        by (rule less(1))(blast intro: cs less(2) order_trans del: subsetI)+
    next
      case (Cons d ds)
      with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
        by auto
      with \<open>rtrancl_path r x xs y\<close> obtain xa: "rtrancl_path r x (ds @ [a]) a"
        and ay: "rtrancl_path r a (bs @ a # cs) y"
        by (auto elim: rtrancl_path_appendE)
      from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
      with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
        by (rule rtrancl_path_trans)
      from xs have set: "set ((ds @ [a]) @ cs) \ set xs" by auto
      from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
      then show ?thesis
        by (rule less(1))(blast intro: xy less(2) set[THEN subsetD])+
    qed
  qed
qed

inductive rtrancl_tab :: "('a \ 'a \ bool) \ 'a list \ 'a \ 'a \ bool"
  for r :: "'a \ 'a \ bool"
where
  base: "rtrancl_tab r xs x x"
| step: "x \ set xs \ r x y \ rtrancl_tab r (x # xs) y z \ rtrancl_tab r xs x z"

lemma rtrancl_path_imp_rtrancl_tab:
  assumes path: "rtrancl_path r x xs y"
    and x: "distinct (x # xs)"
    and ys: "({x} \ set xs) \ set ys = {}"
  shows "rtrancl_tab r ys x y"
  using path x ys
proof (induct arbitrary: ys)
  case base
  show ?case
    by (rule rtrancl_tab.base)
next
  case (step x y zs z)
  then have "x \ set ys"
    by auto
  from step have "distinct (y # zs)"
    by simp
  moreover from step have "({y} \ set zs) \ set (x # ys) = {}"
    by auto
  ultimately have "rtrancl_tab r (x # ys) y z"
    by (rule step)
  with \<open>x \<notin> set ys\<close> \<open>r x y\<close> show ?case
    by (rule rtrancl_tab.step)
qed

lemma rtrancl_tab_imp_rtrancl_path:
  assumes tab: "rtrancl_tab r ys x y"
  obtains xs where "rtrancl_path r x xs y"
  using tab
proof induct
  case base
  from rtrancl_path.base show ?case
    by (rule base)
next
  case step
  show ?case
    by (iprover intro: step rtrancl_path.step)
qed

lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y \ rtrancl_tab r [] x y"
proof
  show "rtrancl_tab r [] x y" if "r\<^sup>*\<^sup>* x y"
  proof -
    from that obtain xs where "rtrancl_path r x xs y"
      by (auto simp add: rtranclp_eq_rtrancl_path)
    then obtain xs' where xs': "rtrancl_path r x xs' y" and distinct: "distinct (x # xs')"
      by (rule rtrancl_path_distinct)
    have "({x} \ set xs') \ set [] = {}"
      by simp
    with xs' distinct show ?thesis
      by (rule rtrancl_path_imp_rtrancl_tab)
  qed
  show "r\<^sup>*\<^sup>* x y" if "rtrancl_tab r [] x y"
  proof -
    from that obtain xs where "rtrancl_path r x xs y"
      by (rule rtrancl_tab_imp_rtrancl_path)
    then show ?thesis
      by (auto simp add: rtranclp_eq_rtrancl_path)
  qed
qed

declare rtranclp_rtrancl_eq [code del]
declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro]

code_pred rtranclp
  using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce

lemma rtrancl_path_Range: "\ rtrancl_path R x xs y; z \ set xs \ \ Rangep R z"
by(induction rule: rtrancl_path.induct) auto

lemma rtrancl_path_Range_end: "\ rtrancl_path R x xs y; xs \ [] \ \ Rangep R y"
by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)

lemma rtrancl_path_nth:
  "\ rtrancl_path R x xs y; i < length xs \ \ R ((x # xs) ! i) (xs ! i)"
proof(induction arbitrary: i rule: rtrancl_path.induct)
  case step thus ?case by(cases i) simp_all
qed simp

lemma rtrancl_path_last: "\ rtrancl_path R x xs y; xs \ [] \ \ last xs = y"
by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)

lemma rtrancl_path_mono:
  "\ rtrancl_path R x p y; \x y. R x y \ S x y \ \ rtrancl_path S x p y"
by(induction rule: rtrancl_path.induct)(auto intro: rtrancl_path.intros)

end

quality100%

¤ Dauer der Verarbeitung: 0.11 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:

sprechenden Kalenders