author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 63465  d7610beb98bc 
child 65869  a6ed757b8585 
permissions  rwrr 
26735  1 
(* Title: HOL/Library/Sublist_Order.thy 
63465  2 
Author: Peter Lammich, Uni Muenster <peter.lammich@unimuenster.de> 
3 
Author: Florian Haftmann, , TU Muenchen 

4 
Author: Tobias Nipkow, TU Muenchen 

26735  5 
*) 
6 

60500  7 
section \<open>Sublist Ordering\<close> 
26735  8 

9 
theory Sublist_Order 

49088
5cd8b4426a57
Main is implicitly imported via Sublist
Christian Sternagel
parents:
49085
diff
changeset

10 
imports Sublist 
26735  11 
begin 
12 

60500  13 
text \<open> 
63465  14 
This theory defines sublist ordering on lists. A list \<open>ys\<close> is a sublist of a 
15 
list \<open>xs\<close>, iff one obtains \<open>ys\<close> by erasing some elements from \<open>xs\<close>. 

60500  16 
\<close> 
26735  17 

60500  18 
subsection \<open>Definitions and basic lemmas\<close> 
26735  19 

33431  20 
instantiation list :: (type) ord 
26735  21 
begin 
22 

63465  23 
definition "xs \<le> ys \<longleftrightarrow> sublisteq xs ys" for xs ys :: "'a list" 
24 
definition "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" for xs ys :: "'a list" 

26735  25 

49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset

26 
instance .. 
33431  27 

28 
end 

29 

49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset

30 
instance list :: (type) order 
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset

31 
proof 
26735  32 
fix xs ys zs :: "'a list" 
63465  33 
show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs" 
34 
unfolding less_list_def .. 

35 
show "xs \<le> xs" 

36 
by (simp add: less_eq_list_def) 

37 
show "xs = ys" if "xs \<le> ys" and "ys \<le> xs" 

38 
using that unfolding less_eq_list_def by (rule sublisteq_antisym) 

39 
show "xs \<le> zs" if "xs \<le> ys" and "ys \<le> zs" 

40 
using that unfolding less_eq_list_def by (rule sublisteq_trans) 

26735  41 
qed 
42 

49093  43 
lemmas less_eq_list_induct [consumes 1, case_names empty drop take] = 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset

44 
list_emb.induct [of "op =", folded less_eq_list_def] 
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset

45 
lemmas less_eq_list_drop = list_emb.list_emb_Cons [of "op =", folded less_eq_list_def] 
50516  46 
lemmas le_list_Cons2_iff [simp, code] = sublisteq_Cons2_iff [folded less_eq_list_def] 
47 
lemmas le_list_map = sublisteq_map [folded less_eq_list_def] 

48 
lemmas le_list_filter = sublisteq_filter [folded less_eq_list_def] 

57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset

49 
lemmas le_list_length = list_emb_length [of "op =", folded less_eq_list_def] 
49093  50 

33431  51 
lemma less_list_length: "xs < ys \<Longrightarrow> length xs < length ys" 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset

52 
by (metis list_emb_length sublisteq_same_length le_neq_implies_less less_list_def less_eq_list_def) 
26735  53 

33431  54 
lemma less_list_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []" 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset

55 
by (metis less_eq_list_def list_emb_Nil order_less_le) 
33431  56 

49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset

57 
lemma less_list_below_empty [simp]: "xs < [] \<longleftrightarrow> False" 
57497
4106a2bc066a
renamed "list_hembeq" into slightly shorter "list_emb"
Christian Sternagel
parents:
50516
diff
changeset

58 
by (metis list_emb_Nil less_eq_list_def less_list_def) 
33431  59 

60 
lemma less_list_drop: "xs < ys \<Longrightarrow> xs < x # ys" 

49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset

61 
by (unfold less_le less_eq_list_def) (auto) 
26735  62 

33431  63 
lemma less_list_take_iff: "x # xs < x # ys \<longleftrightarrow> xs < ys" 
50516  64 
by (metis sublisteq_Cons2_iff less_list_def less_eq_list_def) 
33431  65 

66 
lemma less_list_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys" 

63465  67 
by (metis sublisteq_append_le_same_iff sublisteq_drop_many order_less_le 
68 
self_append_conv2 less_eq_list_def) 

33431  69 

70 
lemma less_list_take_many_iff: "zs @ xs < zs @ ys \<longleftrightarrow> xs < ys" 

50516  71 
by (metis less_list_def less_eq_list_def sublisteq_append') 
33431  72 

73 
lemma less_list_rev_take: "xs @ zs < ys @ zs \<longleftrightarrow> xs < ys" 

49085
4eef5c2ff5ad
introduced "sub" as abbreviation for "emb (op =)";
Christian Sternagel
parents:
49084
diff
changeset

74 
by (unfold less_le less_eq_list_def) auto 
26735  75 

76 
end 