src/HOL/Library/Prefix_Order.thy
author wenzelm
Sat, 12 Jan 2013 14:53:56 +0100
changeset 50843 1465521b92a1
parent 49322 fbb320d02420
child 54538 ba7392b52a7c
permissions -rw-r--r--
removed unused/non-portable bash_output_fifo;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49322
fbb320d02420 tuned headers;
wenzelm
parents: 49089
diff changeset
     1
(*  Title:      HOL/Library/Prefix_Order.thy
49089
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
     3
*)
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
     4
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
     5
header {* Prefix order on lists as order class instance *}
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
     6
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
     7
theory Prefix_Order
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
     8
imports Sublist
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
     9
begin
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    10
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    11
instantiation list :: (type) order
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    12
begin
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    13
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    14
definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    15
definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    16
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    17
instance by (default, unfold less_eq_list_def less_list_def) auto
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    18
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    19
end
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    20
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    21
lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    22
lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    23
lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    24
lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    25
lemmas strict_prefixI [intro?] = prefixI [folded less_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    26
lemmas strict_prefixE [elim?] = prefixE [folded less_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    27
theorems Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    28
theorems prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    29
lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    30
lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    31
lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    32
lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    33
lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    34
theorems prefix_Cons = prefixeq_Cons [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    35
theorems prefix_length_le = prefixeq_length_le [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    36
lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    37
lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] =
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    38
  not_prefixeq_induct [folded less_eq_list_def]
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    39
cd73b439cbe5 added theory instantiating type class order for list prefixes
Christian Sternagel
parents:
diff changeset
    40
end