9 begin |
9 begin |
10 |
10 |
11 instantiation list :: (type) order |
11 instantiation list :: (type) order |
12 begin |
12 begin |
13 |
13 |
14 definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys" |
14 definition "(xs::'a list) \<le> ys \<equiv> prefix xs ys" |
15 definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)" |
15 definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)" |
16 |
16 |
17 instance |
17 instance |
18 by standard (auto simp: less_eq_list_def less_list_def) |
18 by standard (auto simp: less_eq_list_def less_list_def) |
19 |
19 |
20 end |
20 end |
21 |
21 |
22 lemmas prefixI [intro?] = prefixeqI [folded less_eq_list_def] |
22 lemma less_list_def': "(xs::'a list) < ys \<longleftrightarrow> strict_prefix xs ys" |
23 lemmas prefixE [elim?] = prefixeqE [folded less_eq_list_def] |
23 by (simp add: less_eq_list_def order.strict_iff_order prefix_order.less_le) |
24 lemmas strict_prefixI' [intro?] = prefixI' [folded less_list_def] |
24 |
25 lemmas strict_prefixE' [elim?] = prefixE' [folded less_list_def] |
25 lemmas prefixI [intro?] = prefixI [folded less_eq_list_def] |
26 lemmas strict_prefixI [intro?] = prefixI [folded less_list_def] |
26 lemmas prefixE [elim?] = prefixE [folded less_eq_list_def] |
27 lemmas strict_prefixE [elim?] = prefixE [folded less_list_def] |
27 lemmas strict_prefixI' [intro?] = strict_prefixI' [folded less_list_def'] |
28 lemmas Nil_prefix [iff] = Nil_prefixeq [folded less_eq_list_def] |
28 lemmas strict_prefixE' [elim?] = strict_prefixE' [folded less_list_def'] |
29 lemmas prefix_Nil [simp] = prefixeq_Nil [folded less_eq_list_def] |
29 lemmas strict_prefixI [intro?] = strict_prefixI [folded less_list_def'] |
30 lemmas prefix_snoc [simp] = prefixeq_snoc [folded less_eq_list_def] |
30 lemmas strict_prefixE [elim?] = strict_prefixE [folded less_list_def'] |
31 lemmas Cons_prefix_Cons [simp] = Cons_prefixeq_Cons [folded less_eq_list_def] |
31 lemmas Nil_prefix [iff] = Nil_prefix [folded less_eq_list_def] |
32 lemmas same_prefix_prefix [simp] = same_prefixeq_prefixeq [folded less_eq_list_def] |
32 lemmas prefix_Nil [simp] = prefix_Nil [folded less_eq_list_def] |
33 lemmas same_prefix_nil [iff] = same_prefixeq_nil [folded less_eq_list_def] |
33 lemmas prefix_snoc [simp] = prefix_snoc [folded less_eq_list_def] |
34 lemmas prefix_prefix [simp] = prefixeq_prefixeq [folded less_eq_list_def] |
34 lemmas Cons_prefix_Cons [simp] = Cons_prefix_Cons [folded less_eq_list_def] |
35 lemmas prefix_Cons = prefixeq_Cons [folded less_eq_list_def] |
35 lemmas same_prefix_prefix [simp] = same_prefix_prefix [folded less_eq_list_def] |
36 lemmas prefix_length_le = prefixeq_length_le [folded less_eq_list_def] |
36 lemmas same_prefix_nil [iff] = same_prefix_nil [folded less_eq_list_def] |
37 lemmas strict_prefix_simps [simp, code] = prefix_simps [folded less_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'] |
38 lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] = |
41 lemmas not_prefix_induct [consumes 1, case_names Nil Neq Eq] = |
39 not_prefixeq_induct [folded less_eq_list_def] |
42 not_prefix_induct [folded less_eq_list_def] |
40 |
43 |
41 end |
44 end |