src/HOL/Library/Prefix_Order.thy
author wenzelm
Mon Dec 28 17:43:30 2015 +0100 (2015-12-28)
changeset 61952 546958347e05
parent 61337 4645502c3c64
child 63117 acb6d72fc42e
permissions -rw-r--r--
prefer symbols for "Union", "Inter";
wenzelm@49322
     1
(*  Title:      HOL/Library/Prefix_Order.thy
Christian@49089
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
Christian@49089
     3
*)
Christian@49089
     4
wenzelm@60500
     5
section \<open>Prefix order on lists as order class instance\<close>
Christian@49089
     6
Christian@49089
     7
theory Prefix_Order
traytel@55579
     8
imports Sublist
Christian@49089
     9
begin
Christian@49089
    10
Christian@49089
    11
instantiation list :: (type) order
Christian@49089
    12
begin
Christian@49089
    13
Christian@49089
    14
definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
Christian@49089
    15
definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
Christian@49089
    16
wenzelm@60679
    17
instance
wenzelm@60679
    18
  by standard (auto simp: less_eq_list_def less_list_def)
Christian@49089
    19
Christian@49089
    20
end
Christian@49089
    21
Christian@49089
    22
lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def]
Christian@49089
    23
lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def]
Christian@49089
    24
lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def]
Christian@49089
    25
lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def]
Christian@49089
    26
lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
Christian@49089
    27
lemmas strict_prefixE [elim?] = prefixE [folded less_list_def]
wenzelm@61337
    28
lemmas Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def]
wenzelm@61337
    29
lemmas prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
Christian@49089
    30
lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def]
Christian@49089
    31
lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def]
Christian@49089
    32
lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def]
Christian@49089
    33
lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def]
Christian@49089
    34
lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def]
wenzelm@61337
    35
lemmas prefix_Cons = prefixeq_Cons [folded less_eq_list_def]
wenzelm@61337
    36
lemmas prefix_length_le = prefixeq_length_le [folded less_eq_list_def]
Christian@49089
    37
lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def]
Christian@49089
    38
lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] =
Christian@49089
    39
  not_prefixeq_induct [folded less_eq_list_def]
Christian@49089
    40
Christian@49089
    41
end