src/HOL/Library/Prefix_Order.thy
author traytel
Wed Feb 19 10:30:21 2014 +0100 (2014-02-19)
changeset 55579 207538943038
parent 54538 ba7392b52a7c
child 58881 b9556a055632
permissions -rw-r--r--
reverted ba7392b52a7c: List_Prefix not needed anymore by codatatypes
     1 (*  Title:      HOL/Library/Prefix_Order.thy
     2     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 header {* Prefix order on lists as order class instance *}
     6 
     7 theory Prefix_Order
     8 imports Sublist
     9 begin
    10 
    11 instantiation list :: (type) order
    12 begin
    13 
    14 definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
    15 definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
    16 
    17 instance by (default, unfold less_eq_list_def less_list_def) auto
    18 
    19 end
    20 
    21 lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def]
    22 lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def]
    23 lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def]
    24 lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def]
    25 lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
    26 lemmas strict_prefixE [elim?] = prefixE [folded less_list_def]
    27 theorems Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def]
    28 theorems prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
    29 lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def]
    30 lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def]
    31 lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def]
    32 lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def]
    33 lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def]
    34 theorems prefix_Cons = prefixeq_Cons [folded less_eq_list_def]
    35 theorems prefix_length_le = prefixeq_length_le [folded less_eq_list_def]
    36 lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def]
    37 lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] =
    38   not_prefixeq_induct [folded less_eq_list_def]
    39 
    40 end