added theory Sublist_Order
authorhaftmann
Tue Apr 22 08:33:21 2008 +0200 (2008-04-22)
changeset 2673539be3c7e643a
parent 26734 a92057c1ee21
child 26736 e6091328718f
added theory Sublist_Order
src/HOL/IsaMakefile
src/HOL/Library/Library/ROOT.ML
src/HOL/Library/Sublist_Order.thy
     1.1 --- a/src/HOL/IsaMakefile	Tue Apr 22 08:33:20 2008 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Apr 22 08:33:21 2008 +0200
     1.3 @@ -226,7 +226,7 @@
     1.4    Library/Library/ROOT.ML Library/Library/document/root.tex \
     1.5    Library/Library/document/root.bib Library/While_Combinator.thy \
     1.6    Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \
     1.7 -  Library/Option_ord.thy \
     1.8 +  Library/Option_ord.thy Library/Sublist_Order.thy \
     1.9    Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
    1.10    Library/Coinductive_List.thy Library/AssocList.thy \
    1.11    Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
     2.1 --- a/src/HOL/Library/Library/ROOT.ML	Tue Apr 22 08:33:20 2008 +0200
     2.2 +++ b/src/HOL/Library/Library/ROOT.ML	Tue Apr 22 08:33:21 2008 +0200
     2.3 @@ -1,3 +1,3 @@
     2.4  (* $Id$ *)
     2.5  
     2.6 -use_thys ["Library", "List_Prefix", "List_lexord"];
     2.7 +use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Sublist_Order.thy	Tue Apr 22 08:33:21 2008 +0200
     3.3 @@ -0,0 +1,187 @@
     3.4 +(*  Title:      HOL/Library/Sublist_Order.thy
     3.5 +    ID:         $Id$
     3.6 +    Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
     3.7 +                Florian Haftmann, TU M√ľnchen
     3.8 +*)
     3.9 +
    3.10 +header {* Sublist Ordering *}
    3.11 +
    3.12 +theory Sublist_Order
    3.13 +imports Main
    3.14 +begin
    3.15 +
    3.16 +text {*
    3.17 +  This theory defines sublist ordering on lists.
    3.18 +  A list @{text ys} is a sublist of a list @{text xs},
    3.19 +  iff one obtains @{text ys} by erasing some elements from @{text xs}.
    3.20 +*}
    3.21 +
    3.22 +subsection {* Definitions and basic lemmas *}
    3.23 +
    3.24 +instantiation list :: (type) order
    3.25 +begin
    3.26 +
    3.27 +inductive less_eq_list where
    3.28 +  empty [simp, intro!]: "[] \<le> xs"
    3.29 +  | drop: "ys \<le> xs \<Longrightarrow> ys \<le> x # xs"
    3.30 +  | take: "ys \<le> xs \<Longrightarrow> x # ys \<le> x # xs"
    3.31 +
    3.32 +lemmas ileq_empty = empty
    3.33 +lemmas ileq_drop = drop
    3.34 +lemmas ileq_take = take
    3.35 +
    3.36 +lemma ileq_cases [cases set, case_names empty drop take]:
    3.37 +  assumes "xs \<le> ys"
    3.38 +    and "xs = [] \<Longrightarrow> P"
    3.39 +    and "\<And>z zs. ys = z # zs \<Longrightarrow> xs \<le> zs \<Longrightarrow> P"
    3.40 +    and "\<And>x zs ws. xs = x # zs \<Longrightarrow> ys = x # ws \<Longrightarrow> zs \<le> ws \<Longrightarrow> P"
    3.41 +  shows P
    3.42 +  using assms by (blast elim: less_eq_list.cases)
    3.43 +
    3.44 +lemma ileq_induct [induct set, case_names empty drop take]:
    3.45 +  assumes "xs \<le> ys"
    3.46 +    and "\<And>zs. P [] zs"
    3.47 +    and "\<And>z zs ws. ws \<le> zs \<Longrightarrow>  P ws zs \<Longrightarrow> P ws (z # zs)"
    3.48 +    and "\<And>z zs ws. ws \<le> zs \<Longrightarrow> P ws zs \<Longrightarrow> P (z # ws) (z # zs)"
    3.49 +  shows "P xs ys" 
    3.50 +  using assms by (induct rule: less_eq_list.induct) blast+
    3.51 +
    3.52 +definition
    3.53 +  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys"
    3.54 +
    3.55 +lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
    3.56 +  by (induct rule: ileq_induct) auto
    3.57 +lemma ileq_below_empty [simp]: "xs \<le> [] \<longleftrightarrow> xs = []"
    3.58 +  by (auto dest: ileq_length)
    3.59 +
    3.60 +instance proof
    3.61 +  fix xs ys :: "'a list"
    3.62 +  show "xs < ys \<longleftrightarrow> xs \<le> ys \<and> xs \<noteq> ys" unfolding less_list_def ..
    3.63 +next
    3.64 +  fix xs :: "'a list"
    3.65 +  show "xs \<le> xs" by (induct xs) (auto intro!: ileq_empty ileq_drop ileq_take)
    3.66 +next
    3.67 +  fix xs ys :: "'a list"
    3.68 +  (* TODO: Is there a simpler proof ? *)
    3.69 +  { fix n
    3.70 +    have "!!l l'. \<lbrakk>l\<le>l'; l'\<le>l; n=length l + length l'\<rbrakk> \<Longrightarrow> l=l'"
    3.71 +    proof (induct n rule: nat_less_induct)
    3.72 +      case (1 n l l') from "1.prems"(1) show ?case proof (cases rule: ileq_cases)
    3.73 +        case empty with "1.prems"(2) show ?thesis by auto 
    3.74 +      next
    3.75 +        case (drop a l2') with "1.prems"(2) have "length l'\<le>length l" "length l \<le> length l2'" "1+length l2' = length l'" by (auto dest: ileq_length)
    3.76 +        hence False by simp thus ?thesis ..
    3.77 +      next
    3.78 +        case (take a l1' l2') hence LEN': "length l1' + length l2' < length l + length l'" by simp
    3.79 +        from "1.prems" have LEN: "length l' = length l" by (auto dest!: ileq_length)
    3.80 +        from "1.prems"(2) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take'])
    3.81 +          case empty' with take LEN show ?thesis by simp 
    3.82 +        next
    3.83 +          case (drop' ah l2h) with take LEN have "length l1' \<le> length l2h" "1+length l2h = length l2'" "length l2' = length l1'" by (auto dest: ileq_length)
    3.84 +          hence False by simp thus ?thesis ..
    3.85 +        next
    3.86 +          case (take' ah l1h l2h)
    3.87 +          with take have 2: "ah=a" "l1h=l2'" "l2h=l1'" "l1' \<le> l2'" "l2' \<le> l1'" by auto
    3.88 +          with LEN' "1.hyps" "1.prems"(3) have "l1'=l2'" by blast
    3.89 +          with take 2 show ?thesis by simp
    3.90 +        qed
    3.91 +      qed
    3.92 +    qed
    3.93 +  }
    3.94 +  moreover assume "xs \<le> ys" "ys \<le> xs"
    3.95 +  ultimately show "xs = ys" by blast
    3.96 +next
    3.97 +  fix xs ys zs :: "'a list"
    3.98 +  {
    3.99 +    fix n
   3.100 +    have "!!x y z. \<lbrakk>x \<le> y; y \<le> z; n=length x + length y + length z\<rbrakk> \<Longrightarrow> x \<le> z" 
   3.101 +    proof (induct rule: nat_less_induct[case_names I])
   3.102 +      case (I n x y z)
   3.103 +      from I.prems(2) show ?case proof (cases rule: ileq_cases)
   3.104 +        case empty with I.prems(1) show ?thesis by auto
   3.105 +      next
   3.106 +        case (drop a z') hence "length x + length y + length z' < length x + length y + length z" by simp
   3.107 +        with I.hyps I.prems(3,1) drop(2) have "x\<le>z'" by blast
   3.108 +        with drop(1) show ?thesis by (auto intro: ileq_drop)
   3.109 +      next
   3.110 +        case (take a y' z') from I.prems(1) show ?thesis proof (cases rule: ileq_cases[case_names empty' drop' take'])
   3.111 +          case empty' thus ?thesis by auto
   3.112 +        next
   3.113 +          case (drop' ah y'h) with take have "x\<le>y'" "y'\<le>z'" "length x + length y' + length z' < length x + length y + length z" by auto
   3.114 +          with I.hyps I.prems(3) have "x\<le>z'" by (blast)
   3.115 +          with take(2) show ?thesis  by (auto intro: ileq_drop)
   3.116 +        next
   3.117 +          case (take' ah x' y'h) with take have 2: "x=a#x'" "x'\<le>y'" "y'\<le>z'" "length x' + length y' + length z' < length x + length y + length z" by auto
   3.118 +          with I.hyps I.prems(3) have "x'\<le>z'" by blast
   3.119 +          with 2 take(2) show ?thesis by (auto intro: ileq_take)
   3.120 +        qed
   3.121 +      qed
   3.122 +    qed
   3.123 +  }
   3.124 +  moreover assume "xs \<le> ys" "ys \<le> zs"
   3.125 +  ultimately show "xs \<le> zs" by blast
   3.126 +qed
   3.127 +
   3.128 +end
   3.129 +
   3.130 +lemmas ileq_intros = ileq_empty ileq_drop ileq_take
   3.131 +
   3.132 +lemma ileq_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> zs @ ys"
   3.133 +  by (induct zs) (auto intro: ileq_drop)
   3.134 +lemma ileq_take_many: "xs \<le> ys \<Longrightarrow> zs @ xs \<le> zs @ ys"
   3.135 +  by (induct zs) (auto intro: ileq_take)
   3.136 +
   3.137 +lemma ileq_same_length: "xs \<le> ys \<Longrightarrow> length xs = length ys \<Longrightarrow> xs = ys"
   3.138 +  by (induct rule: ileq_induct) (auto dest: ileq_length)
   3.139 +lemma ileq_same_append [simp]: "x # xs \<le> xs \<longleftrightarrow> False"
   3.140 +  by (auto dest: ileq_length)
   3.141 +
   3.142 +lemma ilt_length [intro]:
   3.143 +  assumes "xs < ys"
   3.144 +  shows "length xs < length ys"
   3.145 +proof -
   3.146 +  from assms have "xs \<le> ys" and "xs \<noteq> ys" by (simp_all add: less_list_def)
   3.147 +  moreover with ileq_length have "length xs \<le> length ys" by auto
   3.148 +  ultimately show ?thesis by (auto intro: ileq_same_length)
   3.149 +qed
   3.150 +
   3.151 +lemma ilt_empty [simp]: "[] < xs \<longleftrightarrow> xs \<noteq> []"
   3.152 +  by (unfold less_list_def, auto)
   3.153 +lemma ilt_emptyI: "xs \<noteq> [] \<Longrightarrow> [] < xs"
   3.154 +  by (unfold less_list_def, auto)
   3.155 +lemma ilt_emptyD: "[] < xs \<Longrightarrow> xs \<noteq> []"
   3.156 +  by (unfold less_list_def, auto)
   3.157 +lemma ilt_below_empty[simp]: "xs < [] \<Longrightarrow> False"
   3.158 +  by (auto dest: ilt_length)
   3.159 +lemma ilt_drop: "xs < ys \<Longrightarrow> xs < x # ys"
   3.160 +  by (unfold less_list_def) (auto intro: ileq_intros)
   3.161 +lemma ilt_take: "xs < ys \<Longrightarrow> x # xs < x # ys"
   3.162 +  by (unfold less_list_def) (auto intro: ileq_intros)
   3.163 +lemma ilt_drop_many: "xs < ys \<Longrightarrow> xs < zs @ ys"
   3.164 +  by (induct zs) (auto intro: ilt_drop)
   3.165 +lemma ilt_take_many: "xs < ys \<Longrightarrow> zs @ xs < zs @ ys"
   3.166 +  by (induct zs) (auto intro: ilt_take)
   3.167 +
   3.168 +
   3.169 +subsection {* Appending elements *}
   3.170 +
   3.171 +lemma ileq_rev_take: "xs \<le> ys \<Longrightarrow> xs @ [x] \<le> ys @ [x]"
   3.172 +  by (induct rule: ileq_induct) (auto intro: ileq_intros ileq_drop_many)
   3.173 +lemma ilt_rev_take: "xs < ys \<Longrightarrow> xs @ [x] < ys @ [x]"
   3.174 +  by (unfold less_list_def) (auto dest: ileq_rev_take)
   3.175 +lemma ileq_rev_drop: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ [x]"
   3.176 +  by (induct rule: ileq_induct) (auto intro: ileq_intros)
   3.177 +lemma ileq_rev_drop_many: "xs \<le> ys \<Longrightarrow> xs \<le> ys @ zs"
   3.178 +  by (induct zs rule: rev_induct) (auto dest: ileq_rev_drop)
   3.179 +
   3.180 +
   3.181 +subsection {* Relation to standard list operations *}
   3.182 +
   3.183 +lemma ileq_map: "xs \<le> ys \<Longrightarrow> map f xs \<le> map f ys"
   3.184 +  by (induct rule: ileq_induct) (auto intro: ileq_intros)
   3.185 +lemma ileq_filter_left[simp]: "filter f xs \<le> xs"
   3.186 +  by (induct xs) (auto intro: ileq_intros)
   3.187 +lemma ileq_filter: "xs \<le> ys \<Longrightarrow> filter f xs \<le> filter f ys"
   3.188 +  by (induct rule: ileq_induct) (auto intro: ileq_intros) 
   3.189 +
   3.190 +end