Quelle Subseq_Order.thy Sprache: Isabelle

(*  Title:      HOL/Library/Subseq_Order.thy
    Author:     Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
    Author:     Florian Haftmann, TU Muenchen
    Author:     Tobias Nipkow, TU Muenchen
*)

section \<open>Subsequence Ordering\<close>

theory Subseq_Order
imports Sublist
begin

text \<open>
  This theory defines subsequence ordering on lists. A list \<open>ys\<close> is a subsequence of a
  list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
\<close>

subsection \<open>Definitions and basic lemmas\<close>

instantiation list :: (type) ord
begin

definition less_eq_list
  where \<open>xs \<le> ys \<longleftrightarrow> subseq xs ys\<close> for xs ys :: \<open>'a list\<close>

definition less_list
  where \<open>xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs\<close> for xs ys :: \<open>'a list\<close>

instance ..

end

instance list :: (type) order
proof
  fix xs ys zs :: "'a list"
  show "xs < ys \ xs \ ys \ \ ys \ xs"
    unfolding less_list_def ..
  show "xs \ xs"
    by (simp add: less_eq_list_def)
  show "xs = ys" if "xs \ ys" and "ys \ xs"
    using that unfolding less_eq_list_def
    by (rule subseq_order.antisym)
  show "xs \ zs" if "xs \ ys" and "ys \ zs"
    using that unfolding less_eq_list_def
    by (rule subseq_order.order_trans)
qed

lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
  list_emb.induct [of "(=)", folded less_eq_list_def]

lemma less_eq_list_empty [code]:
  \<open>[] \<le> xs \<longleftrightarrow> True\<close>
  by (simp add: less_eq_list_def)

lemma less_eq_list_below_empty [code]:
  \<open>x # xs \<le> [] \<longleftrightarrow> False\<close>
  by (simp add: less_eq_list_def)

lemma le_list_Cons2_iff [simp, code]:
  \<open>x # xs \<le> y # ys \<longleftrightarrow> (if x = y then xs \<le> ys else x # xs \<le> ys)\<close>
  by (simp add: less_eq_list_def)

lemma less_list_empty [simp]:
  \<open>[] < xs \<longleftrightarrow> xs \<noteq> []\<close>
  by (metis less_eq_list_def list_emb_Nil order_less_le)

lemma less_list_empty_Cons [code]:
  \<open>[] < x # xs \<longleftrightarrow> True\<close>
  by simp_all

lemma less_list_below_empty [simp, code]:
  \<open>xs < [] \<longleftrightarrow> False\<close>
  by (metis list_emb_Nil less_eq_list_def less_list_def)

lemma less_list_Cons2_iff [code]:
  \<open>x # xs < y # ys \<longleftrightarrow> (if x = y then xs < ys else x # xs \<le> ys)\<close>
  by (simp add: less_le)

lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "(=)", folded less_eq_list_def]
lemmas le_list_map = subseq_map [folded less_eq_list_def]
lemmas le_list_filter = subseq_filter [folded less_eq_list_def]
lemmas le_list_length = list_emb_length [of "(=)", folded less_eq_list_def]

lemma less_list_length: "xs < ys \ length xs < length ys"
  by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq_list_def)

lemma less_list_drop: "xs < ys \ xs < x # ys"
  by (unfold less_le less_eq_list_def) (auto)

lemma less_list_take_iff: "x # xs < x # ys \ xs < ys"
  by (metis subseq_Cons2_iff less_list_def less_eq_list_def)

lemma less_list_drop_many: "xs < ys \ xs < zs @ ys"
  by (metis subseq_append_le_same_iff subseq_drop_many order_less_le
      self_append_conv2 less_eq_list_def)

lemma less_list_take_many_iff: "zs @ xs < zs @ ys \ xs < ys"
  by (metis less_list_def less_eq_list_def subseq_append')

lemma less_list_rev_take: "xs @ zs < ys @ zs \ xs < ys"
  by (unfold less_le less_eq_list_def) auto

end

quality100%

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