src/HOL/Library/Subseq_Order.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (4 months ago) changeset 69946 494934c30f38 parent 67399 eab6ce8368fa permissions -rw-r--r--
improved code equations taken over from AFP
```     1 (*  Title:      HOL/Library/Subseq_Order.thy
```
```     2     Author:     Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
```
```     3     Author:     Florian Haftmann, TU Muenchen
```
```     4     Author:     Tobias Nipkow, TU Muenchen
```
```     5 *)
```
```     6
```
```     7 section \<open>Subsequence Ordering\<close>
```
```     8
```
```     9 theory Subseq_Order
```
```    10 imports Sublist
```
```    11 begin
```
```    12
```
```    13 text \<open>
```
```    14   This theory defines subsequence ordering on lists. A list \<open>ys\<close> is a subsequence of a
```
```    15   list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>.
```
```    16 \<close>
```
```    17
```
```    18 subsection \<open>Definitions and basic lemmas\<close>
```
```    19
```
```    20 instantiation list :: (type) ord
```
```    21 begin
```
```    22
```
```    23 definition "xs \<le> ys \<longleftrightarrow> subseq xs ys" for xs ys :: "'a list"
```
```    24 definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list"
```
```    25
```
```    26 instance ..
```
```    27
```
```    28 end
```
```    29
```
```    30 instance list :: (type) order
```
```    31 proof
```
```    32   fix xs ys zs :: "'a list"
```
```    33   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
```
```    34     unfolding less_list_def ..
```
```    35   show "xs \<le> xs"
```
```    36     by (simp add: less_eq_list_def)
```
```    37   show "xs = ys" if "xs \<le> ys" and "ys \<le> xs"
```
```    38     using that unfolding less_eq_list_def by (rule subseq_order.antisym)
```
```    39   show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs"
```
```    40     using that unfolding less_eq_list_def by (rule subseq_order.order_trans)
```
```    41 qed
```
```    42
```
```    43 lemmas less_eq_list_induct [consumes 1, case_names empty drop take] =
```
```    44   list_emb.induct [of "(=)", folded less_eq_list_def]
```
```    45 lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "(=)", folded less_eq_list_def]
```
```    46 lemmas le_list_Cons2_iff [simp, code] = subseq_Cons2_iff [folded less_eq_list_def]
```
```    47 lemmas le_list_map = subseq_map [folded less_eq_list_def]
```
```    48 lemmas le_list_filter = subseq_filter [folded less_eq_list_def]
```
```    49 lemmas le_list_length = list_emb_length [of "(=)", folded less_eq_list_def]
```
```    50
```
```    51 lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys"
```
```    52   by (metis list_emb_length subseq_same_length le_neq_implies_less less_list_def less_eq_list_def)
```
```    53
```
```    54 lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
```
```    55   by (metis less_eq_list_def list_emb_Nil order_less_le)
```
```    56
```
```    57 lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False"
```
```    58   by (metis list_emb_Nil less_eq_list_def less_list_def)
```
```    59
```
```    60 lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys"
```
```    61   by (unfold less_le less_eq_list_def) (auto)
```
```    62
```
```    63 lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys"
```
```    64   by (metis subseq_Cons2_iff less_list_def less_eq_list_def)
```
```    65
```
```    66 lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
```
```    67   by (metis subseq_append_le_same_iff subseq_drop_many order_less_le
```
```    68       self_append_conv2 less_eq_list_def)
```
```    69
```
```    70 lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys"
```
```    71   by (metis less_list_def less_eq_list_def subseq_append')
```
```    72
```
```    73 lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys"
```
```    74   by (unfold less_le less_eq_list_def) auto
```
```    75
```
```    76 end
```