src/HOL/Library/Prefix_Order.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 63465 d7610beb98bc
permissions -rw-r--r--
improved code equations taken over from AFP
     1 (*  Title:      HOL/Library/Prefix_Order.thy
     2     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 section \<open>Prefix order on lists as order class instance\<close>
     6 
     7 theory Prefix_Order
     8 imports Sublist
     9 begin
    10 
    11 instantiation list :: (type) order
    12 begin
    13 
    14 definition "xs \<le> ys \<equiv> prefix xs ys" for xs ys :: "'a list"
    15 definition "xs < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)" for xs ys :: "'a list"
    16 
    17 instance
    18   by standard (auto simp: less_eq_list_def less_list_def)
    19 
    20 end
    21 
    22 lemma less_list_def': "xs < ys \<longleftrightarrow> strict_prefix xs ys" for xs ys :: "'a list"
    23   by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le)
    24 
    25 lemmas prefixI [intro?] = prefixI [folded less_eq_list_def]
    26 lemmas prefixE [elim?] = prefixE [folded less_eq_list_def]
    27 lemmas strict_prefixI' [intro?] = strict_prefixI' [folded less_list_def']
    28 lemmas strict_prefixE' [elim?] = strict_prefixE' [folded less_list_def']
    29 lemmas strict_prefixI [intro?] = strict_prefixI [folded less_list_def']
    30 lemmas strict_prefixE [elim?] = strict_prefixE [folded less_list_def']
    31 lemmas Nil_prefix [iff] = Nil_prefix [folded less_eq_list_def]
    32 lemmas prefix_Nil [simp] = prefix_Nil [folded less_eq_list_def]
    33 lemmas prefix_snoc [simp] = prefix_snoc [folded less_eq_list_def]
    34 lemmas Cons_prefix_Cons [simp] = Cons_prefix_Cons [folded less_eq_list_def]
    35 lemmas same_prefix_prefix [simp] = same_prefix_prefix [folded less_eq_list_def]
    36 lemmas same_prefix_nil [iff] = same_prefix_nil [folded less_eq_list_def]
    37 lemmas prefix_prefix [simp] = prefix_prefix [folded less_eq_list_def]
    38 lemmas prefix_Cons = prefix_Cons [folded less_eq_list_def]
    39 lemmas prefix_length_le = prefix_length_le [folded less_eq_list_def]
    40 lemmas strict_prefix_simps [simp, code] = strict_prefix_simps [folded less_list_def']
    41 lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] =
    42   not_prefix_induct [folded less_eq_list_def]
    43 
    44 end