src/HOL/Library/Prefix_Order.thy
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 63465 d7610beb98bc
permissions -rw-r--r--
tuned headers;
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
wenzelm@63465
    14
definition "xs \<le> ys \<equiv> prefix xs ys" for xs ys :: "'a list"
wenzelm@63465
    15
definition "xs < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)" for xs ys :: "'a list"
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
wenzelm@63465
    22
lemma less_list_def': "xs < ys \<longleftrightarrow> strict_prefix xs ys" for xs ys :: "'a list"
wenzelm@63465
    23
  by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le)
nipkow@63117
    24
nipkow@63117
    25
lemmas prefixI [intro?] = prefixI [folded less_eq_list_def]
nipkow@63117
    26
lemmas prefixE [elim?] = prefixE [folded less_eq_list_def]
nipkow@63117
    27
lemmas strict_prefixI' [intro?] = strict_prefixI' [folded less_list_def']
nipkow@63117
    28
lemmas strict_prefixE' [elim?] = strict_prefixE' [folded less_list_def']
nipkow@63117
    29
lemmas strict_prefixI [intro?] = strict_prefixI [folded less_list_def']
nipkow@63117
    30
lemmas strict_prefixE [elim?] = strict_prefixE [folded less_list_def']
nipkow@63117
    31
lemmas Nil_prefix [iff] = Nil_prefix [folded less_eq_list_def]
nipkow@63117
    32
lemmas prefix_Nil [simp] = prefix_Nil [folded less_eq_list_def]
nipkow@63117
    33
lemmas prefix_snoc [simp] = prefix_snoc [folded less_eq_list_def]
nipkow@63117
    34
lemmas Cons_prefix_Cons [simp] = Cons_prefix_Cons [folded less_eq_list_def]
nipkow@63117
    35
lemmas same_prefix_prefix [simp] = same_prefix_prefix [folded less_eq_list_def]
nipkow@63117
    36
lemmas same_prefix_nil [iff] = same_prefix_nil [folded less_eq_list_def]
nipkow@63117
    37
lemmas prefix_prefix [simp] = prefix_prefix [folded less_eq_list_def]
nipkow@63117
    38
lemmas prefix_Cons = prefix_Cons [folded less_eq_list_def]
nipkow@63117
    39
lemmas prefix_length_le = prefix_length_le [folded less_eq_list_def]
nipkow@63117
    40
lemmas strict_prefix_simps [simp, code] = strict_prefix_simps [folded less_list_def']
Christian@49089
    41
lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] =
nipkow@63117
    42
  not_prefix_induct [folded less_eq_list_def]
Christian@49089
    43
Christian@49089
    44
end