Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ListOrder.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Proofs/Lambda/ListOrder.thy
    Author:     Tobias Nipkow
    Copyright   1998 TU Muenchen
*)

section \<open>Lifting an order to lists of elements\<close>

theory ListOrder
imports Main
begin

declare [[syntax_ambiguity_warning = false]]

text \<open>
  Lifting an order to lists of elements, relating exactly one
  element.
\<close>

definition
  step1 :: "('a => 'a => bool) => 'a list => 'a list => bool" where
  "step1 r =
    (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys =
      us @ z' # vs)"

lemma step1_converse [simp]: "step1 (r\\) = (step1 r)\\"
  apply (unfold step1_def)
  apply (blast intro!: order_antisym)
  done

lemma in_step1_converse [iff]: "(step1 (r\\) x y) = ((step1 r)\\ x y)"
  apply auto
  done

lemma not_Nil_step1 [iff]: "\ step1 r [] xs"
  apply (unfold step1_def)
  apply blast
  done

lemma not_step1_Nil [iff]: "\ step1 r xs []"
  apply (unfold step1_def)
  apply blast
  done

lemma Cons_step1_Cons [iff]:
    "(step1 r (y # ys) (x # xs)) =
      (r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)"
  apply (unfold step1_def)
  apply (rule iffI)
   apply (erule exE)
   apply (rename_tac ts)
   apply (case_tac ts)
    apply fastforce
   apply force
  apply (erule disjE)
   apply blast
  apply (blast intro: Cons_eq_appendI)
  done

lemma append_step1I:
  "step1 r ys xs \ vs = us \ ys = xs \ step1 r vs us
    ==> step1 r (ys @ vs) (xs @ us)"
  apply (unfold step1_def)
  apply auto
   apply blast
  apply (blast intro: append_eq_appendI)
  done

lemma Cons_step1E [elim!]:
  assumes "step1 r ys (x # xs)"
    and "!!y. ys = y # xs \ r y x \ R"
    and "!!zs. ys = x # zs \ step1 r zs xs \ R"
  shows R
  using assms
  apply (cases ys)
   apply (simp add: step1_def)
  apply blast
  done

lemma Snoc_step1_SnocD:
  "step1 r (ys @ [y]) (xs @ [x])
    ==> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)"
  apply (unfold step1_def)
  apply (clarify del: disjCI)
  apply (rename_tac vs)
  apply (rule_tac xs = vs in rev_exhaust)
   apply force
  apply simp
  apply blast
  done

lemma Cons_acc_step1I [intro!]:
    "Wellfounded.accp r x ==> Wellfounded.accp (step1 r) xs \ Wellfounded.accp (step1 r) (x # xs)"
  apply (induct arbitrary: xs set: Wellfounded.accp)
  apply (erule thin_rl)
  apply (erule accp_induct)
  apply (rule accp.accI)
  apply blast
  done

lemma lists_accD: "listsp (Wellfounded.accp r) xs ==> Wellfounded.accp (step1 r) xs"
  apply (induct set: listsp)
   apply (rule accp.accI)
   apply simp
  apply (rule accp.accI)
  apply (fast dest: accp_downward)
  done

lemma ex_step1I:
  "[| x \ set xs; r y x |]
    ==> \<exists>ys. step1 r ys xs \<and> y \<in> set ys"
  apply (unfold step1_def)
  apply (drule in_set_conv_decomp [THEN iffD1])
  apply force
  done

lemma lists_accI: "Wellfounded.accp (step1 r) xs ==> listsp (Wellfounded.accp r) xs"
  apply (induct set: Wellfounded.accp)
  apply clarify
  apply (rule accp.accI)
  apply (drule_tac r=r in ex_step1I, assumption)
  apply blast
  done

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.