src/HOL/Library/List_lexord.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 61076 bdc1e2f0a86a permissions -rw-r--r--
executable domain membership checks
```     1 (*  Title:      HOL/Library/List_lexord.thy
```
```     2     Author:     Norbert Voelker
```
```     3 *)
```
```     4
```
```     5 section \<open>Lexicographic order on lists\<close>
```
```     6
```
```     7 theory List_lexord
```
```     8 imports Main
```
```     9 begin
```
```    10
```
```    11 instantiation list :: (ord) ord
```
```    12 begin
```
```    13
```
```    14 definition
```
```    15   list_less_def: "xs < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u, v). u < v}"
```
```    16
```
```    17 definition
```
```    18   list_le_def: "(xs :: _ list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys"
```
```    19
```
```    20 instance ..
```
```    21
```
```    22 end
```
```    23
```
```    24 instance list :: (order) order
```
```    25 proof
```
```    26   fix xs :: "'a list"
```
```    27   show "xs \<le> xs" by (simp add: list_le_def)
```
```    28 next
```
```    29   fix xs ys zs :: "'a list"
```
```    30   assume "xs \<le> ys" and "ys \<le> zs"
```
```    31   then show "xs \<le> zs"
```
```    32     apply (auto simp add: list_le_def list_less_def)
```
```    33     apply (rule lexord_trans)
```
```    34     apply (auto intro: transI)
```
```    35     done
```
```    36 next
```
```    37   fix xs ys :: "'a list"
```
```    38   assume "xs \<le> ys" and "ys \<le> xs"
```
```    39   then show "xs = ys"
```
```    40     apply (auto simp add: list_le_def list_less_def)
```
```    41     apply (rule lexord_irreflexive [THEN notE])
```
```    42     defer
```
```    43     apply (rule lexord_trans)
```
```    44     apply (auto intro: transI)
```
```    45     done
```
```    46 next
```
```    47   fix xs ys :: "'a list"
```
```    48   show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
```
```    49     apply (auto simp add: list_less_def list_le_def)
```
```    50     defer
```
```    51     apply (rule lexord_irreflexive [THEN notE])
```
```    52     apply auto
```
```    53     apply (rule lexord_irreflexive [THEN notE])
```
```    54     defer
```
```    55     apply (rule lexord_trans)
```
```    56     apply (auto intro: transI)
```
```    57     done
```
```    58 qed
```
```    59
```
```    60 instance list :: (linorder) linorder
```
```    61 proof
```
```    62   fix xs ys :: "'a list"
```
```    63   have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}"
```
```    64     by (rule lexord_linear) auto
```
```    65   then show "xs \<le> ys \<or> ys \<le> xs"
```
```    66     by (auto simp add: list_le_def list_less_def)
```
```    67 qed
```
```    68
```
```    69 instantiation list :: (linorder) distrib_lattice
```
```    70 begin
```
```    71
```
```    72 definition "(inf :: 'a list \<Rightarrow> _) = min"
```
```    73
```
```    74 definition "(sup :: 'a list \<Rightarrow> _) = max"
```
```    75
```
```    76 instance
```
```    77   by standard (auto simp add: inf_list_def sup_list_def max_min_distrib2)
```
```    78
```
```    79 end
```
```    80
```
```    81 lemma not_less_Nil [simp]: "\<not> x < []"
```
```    82   by (simp add: list_less_def)
```
```    83
```
```    84 lemma Nil_less_Cons [simp]: "[] < a # x"
```
```    85   by (simp add: list_less_def)
```
```    86
```
```    87 lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y"
```
```    88   by (simp add: list_less_def)
```
```    89
```
```    90 lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
```
```    91   unfolding list_le_def by (cases x) auto
```
```    92
```
```    93 lemma Nil_le_Cons [simp]: "[] \<le> x"
```
```    94   unfolding list_le_def by (cases x) auto
```
```    95
```
```    96 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
```
```    97   unfolding list_le_def by auto
```
```    98
```
```    99 instantiation list :: (order) order_bot
```
```   100 begin
```
```   101
```
```   102 definition "bot = []"
```
```   103
```
```   104 instance
```
```   105   by standard (simp add: bot_list_def)
```
```   106
```
```   107 end
```
```   108
```
```   109 lemma less_list_code [code]:
```
```   110   "xs < ([]::'a::{equal, order} list) \<longleftrightarrow> False"
```
```   111   "[] < (x::'a::{equal, order}) # xs \<longleftrightarrow> True"
```
```   112   "(x::'a::{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
```
```   113   by simp_all
```
```   114
```
```   115 lemma less_eq_list_code [code]:
```
```   116   "x # xs \<le> ([]::'a::{equal, order} list) \<longleftrightarrow> False"
```
```   117   "[] \<le> (xs::'a::{equal, order} list) \<longleftrightarrow> True"
```
```   118   "(x::'a::{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
```
```   119   by simp_all
```
```   120
```
```   121 end
```