src/HOL/Library/List_Lexorder.thy
 changeset 68312 e9b5f25f6712 parent 61076 bdc1e2f0a86a child 71766 1249b998e377
equal inserted replaced
68311:c551d8acaa42 68312:e9b5f25f6712
`       `
`     1 (*  Title:      HOL/Library/List_Lexorder.thy`
`       `
`     2     Author:     Norbert Voelker`
`       `
`     3 *)`
`       `
`     4 `
`       `
`     5 section \<open>Lexicographic order on lists\<close>`
`       `
`     6 `
`       `
`     7 theory List_Lexorder`
`       `
`     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`