src/HOL/Library/List_lexord.thy
author paulson <lp15@cam.ac.uk>
Wed, 26 Apr 2017 15:53:35 +0100
changeset 65583 8d53b3bebab4
parent 61076 bdc1e2f0a86a
permissions -rw-r--r--
Further new material. The simprule status of some exp and ln identities was reverted.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15737
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Library/List_lexord.thy
nipkow
parents:
diff changeset
     2
    Author:     Norbert Voelker
nipkow
parents:
diff changeset
     3
*)
nipkow
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     5
section \<open>Lexicographic order on lists\<close>
15737
nipkow
parents:
diff changeset
     6
nipkow
parents:
diff changeset
     7
theory List_lexord
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
     8
imports Main
15737
nipkow
parents:
diff changeset
     9
begin
nipkow
parents:
diff changeset
    10
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    11
instantiation list :: (ord) ord
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    12
begin
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    13
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    14
definition
37474
ce943f9edf5e added bot instances; tuned
haftmann
parents: 30663
diff changeset
    15
  list_less_def: "xs < ys \<longleftrightarrow> (xs, ys) \<in> lexord {(u, v). u < v}"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    16
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    17
definition
37474
ce943f9edf5e added bot instances; tuned
haftmann
parents: 30663
diff changeset
    18
  list_le_def: "(xs :: _ list) \<le> ys \<longleftrightarrow> xs < ys \<or> xs = ys"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    19
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    20
instance ..
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    21
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    22
end
15737
nipkow
parents:
diff changeset
    23
17200
3a4d03d1a31b tuned presentation;
wenzelm
parents: 15737
diff changeset
    24
instance list :: (order) order
27682
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    25
proof
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    26
  fix xs :: "'a list"
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    27
  show "xs \<le> xs" by (simp add: list_le_def)
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    28
next
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    29
  fix xs ys zs :: "'a list"
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    30
  assume "xs \<le> ys" and "ys \<le> zs"
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    31
  then show "xs \<le> zs"
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    32
    apply (auto simp add: list_le_def list_less_def)
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    33
    apply (rule lexord_trans)
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    34
    apply (auto intro: transI)
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    35
    done
27682
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    36
next
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    37
  fix xs ys :: "'a list"
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    38
  assume "xs \<le> ys" and "ys \<le> xs"
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    39
  then show "xs = ys"
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    40
    apply (auto simp add: list_le_def list_less_def)
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    41
    apply (rule lexord_irreflexive [THEN notE])
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    42
    defer
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    43
    apply (rule lexord_trans)
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    44
    apply (auto intro: transI)
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    45
    done
27682
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    46
next
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    47
  fix xs ys :: "'a list"
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    48
  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    49
    apply (auto simp add: list_less_def list_le_def)
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    50
    defer
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    51
    apply (rule lexord_irreflexive [THEN notE])
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    52
    apply auto
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    53
    apply (rule lexord_irreflexive [THEN notE])
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    54
    defer
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    55
    apply (rule lexord_trans)
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    56
    apply (auto intro: transI)
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    57
    done
27682
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    58
qed
15737
nipkow
parents:
diff changeset
    59
21458
475b321982f7 added code lemmas
haftmann
parents: 17200
diff changeset
    60
instance list :: (linorder) linorder
27682
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    61
proof
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    62
  fix xs ys :: "'a list"
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    63
  have "(xs, ys) \<in> lexord {(u, v). u < v} \<or> xs = ys \<or> (ys, xs) \<in> lexord {(u, v). u < v}"
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    64
    by (rule lexord_linear) auto
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    65
  then show "xs \<le> ys \<or> ys \<le> xs"
27682
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    66
    by (auto simp add: list_le_def list_less_def)
25aceefd4786 added class preorder
haftmann
parents: 27487
diff changeset
    67
qed
15737
nipkow
parents:
diff changeset
    68
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    69
instantiation list :: (linorder) distrib_lattice
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    70
begin
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    71
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
    72
definition "(inf :: 'a list \<Rightarrow> _) = min"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    73
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
    74
definition "(sup :: 'a list \<Rightarrow> _) = max"
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    75
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    76
instance
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
    77
  by standard (auto simp add: inf_list_def sup_list_def max_min_distrib2)
22483
86064f2f2188 added instance for lattice
haftmann
parents: 22316
diff changeset
    78
25764
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    79
end
878c37886eed removed some legacy instantiations
haftmann
parents: 25595
diff changeset
    80
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    81
lemma not_less_Nil [simp]: "\<not> x < []"
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    82
  by (simp add: list_less_def)
15737
nipkow
parents:
diff changeset
    83
22177
515021e98684 improved
haftmann
parents: 21458
diff changeset
    84
lemma Nil_less_Cons [simp]: "[] < a # x"
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    85
  by (simp add: list_less_def)
15737
nipkow
parents:
diff changeset
    86
22177
515021e98684 improved
haftmann
parents: 21458
diff changeset
    87
lemma Cons_less_Cons [simp]: "a # x < b # y \<longleftrightarrow> a < b \<or> a = b \<and> x < y"
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    88
  by (simp add: list_less_def)
15737
nipkow
parents:
diff changeset
    89
22177
515021e98684 improved
haftmann
parents: 21458
diff changeset
    90
lemma le_Nil [simp]: "x \<le> [] \<longleftrightarrow> x = []"
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    91
  unfolding list_le_def by (cases x) auto
22177
515021e98684 improved
haftmann
parents: 21458
diff changeset
    92
515021e98684 improved
haftmann
parents: 21458
diff changeset
    93
lemma Nil_le_Cons [simp]: "[] \<le> x"
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    94
  unfolding list_le_def by (cases x) auto
15737
nipkow
parents:
diff changeset
    95
22177
515021e98684 improved
haftmann
parents: 21458
diff changeset
    96
lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
    97
  unfolding list_le_def by auto
15737
nipkow
parents:
diff changeset
    98
52729
412c9e0381a1 factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents: 38857
diff changeset
    99
instantiation list :: (order) order_bot
37474
ce943f9edf5e added bot instances; tuned
haftmann
parents: 30663
diff changeset
   100
begin
ce943f9edf5e added bot instances; tuned
haftmann
parents: 30663
diff changeset
   101
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
   102
definition "bot = []"
37474
ce943f9edf5e added bot instances; tuned
haftmann
parents: 30663
diff changeset
   103
53214
bae01293f4dd tuned imports;
wenzelm
parents: 52729
diff changeset
   104
instance
60679
ade12ef2773c tuned proofs;
wenzelm
parents: 60500
diff changeset
   105
  by standard (simp add: bot_list_def)
37474
ce943f9edf5e added bot instances; tuned
haftmann
parents: 30663
diff changeset
   106
ce943f9edf5e added bot instances; tuned
haftmann
parents: 30663
diff changeset
   107
end
ce943f9edf5e added bot instances; tuned
haftmann
parents: 30663
diff changeset
   108
ce943f9edf5e added bot instances; tuned
haftmann
parents: 30663
diff changeset
   109
lemma less_list_code [code]:
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
   110
  "xs < ([]::'a::{equal, order} list) \<longleftrightarrow> False"
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
   111
  "[] < (x::'a::{equal, order}) # xs \<longleftrightarrow> True"
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
   112
  "(x::'a::{equal, order}) # xs < y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs < ys"
22177
515021e98684 improved
haftmann
parents: 21458
diff changeset
   113
  by simp_all
515021e98684 improved
haftmann
parents: 21458
diff changeset
   114
37474
ce943f9edf5e added bot instances; tuned
haftmann
parents: 30663
diff changeset
   115
lemma less_eq_list_code [code]:
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
   116
  "x # xs \<le> ([]::'a::{equal, order} list) \<longleftrightarrow> False"
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
   117
  "[] \<le> (xs::'a::{equal, order} list) \<longleftrightarrow> True"
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60679
diff changeset
   118
  "(x::'a::{equal, order}) # xs \<le> y # ys \<longleftrightarrow> x < y \<or> x = y \<and> xs \<le> ys"
22177
515021e98684 improved
haftmann
parents: 21458
diff changeset
   119
  by simp_all
515021e98684 improved
haftmann
parents: 21458
diff changeset
   120
17200
3a4d03d1a31b tuned presentation;
wenzelm
parents: 15737
diff changeset
   121
end