author | wenzelm |
Sat, 12 Jan 2013 14:53:56 +0100 | |
changeset 50843 | 1465521b92a1 |
parent 49322 | fbb320d02420 |
child 54538 | ba7392b52a7c |
permissions | -rw-r--r-- |
49322 | 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 |