src/HOL/Imperative_HOL/ex/Sublist.thy
author bulwahn
Thu Apr 08 08:17:27 2010 +0200 (2010-04-08)
changeset 36098 53992c639da5
parent 32960 69916a850301
child 41413 64cd30d6b0b8
permissions -rw-r--r--
added imperative SAT checker; improved headers of example files; adopted IsaMakefile
     1 (*  Title:      HOL/Imperative_HOL/ex/Sublist.thy
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 *)
     4 
     5 header {* Slices of lists *}
     6 
     7 theory Sublist
     8 imports Multiset
     9 begin
    10 
    11 lemma sublist_split: "i \<le> j \<and> j \<le> k \<Longrightarrow> sublist xs {i..<j} @ sublist xs {j..<k} = sublist xs {i..<k}" 
    12 apply (induct xs arbitrary: i j k)
    13 apply simp
    14 apply (simp only: sublist_Cons)
    15 apply simp
    16 apply safe
    17 apply simp
    18 apply (erule_tac x="0" in meta_allE)
    19 apply (erule_tac x="j - 1" in meta_allE)
    20 apply (erule_tac x="k - 1" in meta_allE)
    21 apply (subgoal_tac "0 \<le> j - 1 \<and> j - 1 \<le> k - 1")
    22 apply simp
    23 apply (subgoal_tac "{ja. Suc ja < j} = {0..<j - Suc 0}")
    24 apply (subgoal_tac "{ja. j \<le> Suc ja \<and> Suc ja < k} = {j - Suc 0..<k - Suc 0}")
    25 apply (subgoal_tac "{j. Suc j < k} = {0..<k - Suc 0}")
    26 apply simp
    27 apply fastsimp
    28 apply fastsimp
    29 apply fastsimp
    30 apply fastsimp
    31 apply (erule_tac x="i - 1" in meta_allE)
    32 apply (erule_tac x="j - 1" in meta_allE)
    33 apply (erule_tac x="k - 1" in meta_allE)
    34 apply (subgoal_tac " {ja. i \<le> Suc ja \<and> Suc ja < j} = {i - 1 ..<j - 1}")
    35 apply (subgoal_tac " {ja. j \<le> Suc ja \<and> Suc ja < k} = {j - 1..<k - 1}")
    36 apply (subgoal_tac "{j. i \<le> Suc j \<and> Suc j < k} = {i - 1..<k - 1}")
    37 apply (subgoal_tac " i - 1 \<le> j - 1 \<and> j - 1 \<le> k - 1")
    38 apply simp
    39 apply fastsimp
    40 apply fastsimp
    41 apply fastsimp
    42 apply fastsimp
    43 done
    44 
    45 lemma sublist_update1: "i \<notin> inds \<Longrightarrow> sublist (xs[i := v]) inds = sublist xs inds"
    46 apply (induct xs arbitrary: i inds)
    47 apply simp
    48 apply (case_tac i)
    49 apply (simp add: sublist_Cons)
    50 apply (simp add: sublist_Cons)
    51 done
    52 
    53 lemma sublist_update2: "i \<in> inds \<Longrightarrow> sublist (xs[i := v]) inds = (sublist xs inds)[(card {k \<in> inds. k < i}):= v]"
    54 proof (induct xs arbitrary: i inds)
    55   case Nil thus ?case by simp
    56 next
    57   case (Cons x xs)
    58   thus ?case
    59   proof (cases i)
    60     case 0 with Cons show ?thesis by (simp add: sublist_Cons)
    61   next
    62     case (Suc i')
    63     with Cons show ?thesis
    64       apply simp
    65       apply (simp add: sublist_Cons)
    66       apply auto
    67       apply (auto simp add: nat.split)
    68       apply (simp add: card_less_Suc[symmetric])
    69       apply (simp add: card_less_Suc2)
    70       done
    71   qed
    72 qed
    73 
    74 lemma sublist_update: "sublist (xs[i := v]) inds = (if i \<in> inds then (sublist xs inds)[(card {k \<in> inds. k < i}) := v] else sublist xs inds)"
    75 by (simp add: sublist_update1 sublist_update2)
    76 
    77 lemma sublist_take: "sublist xs {j. j < m} = take m xs"
    78 apply (induct xs arbitrary: m)
    79 apply simp
    80 apply (case_tac m)
    81 apply simp
    82 apply (simp add: sublist_Cons)
    83 done
    84 
    85 lemma sublist_take': "sublist xs {0..<m} = take m xs"
    86 apply (induct xs arbitrary: m)
    87 apply simp
    88 apply (case_tac m)
    89 apply simp
    90 apply (simp add: sublist_Cons sublist_take)
    91 done
    92 
    93 lemma sublist_all[simp]: "sublist xs {j. j < length xs} = xs"
    94 apply (induct xs)
    95 apply simp
    96 apply (simp add: sublist_Cons)
    97 done
    98 
    99 lemma sublist_all'[simp]: "sublist xs {0..<length xs} = xs"
   100 apply (induct xs)
   101 apply simp
   102 apply (simp add: sublist_Cons)
   103 done
   104 
   105 lemma sublist_single: "a < length xs \<Longrightarrow> sublist xs {a} = [xs ! a]"
   106 apply (induct xs arbitrary: a)
   107 apply simp
   108 apply(case_tac aa)
   109 apply simp
   110 apply (simp add: sublist_Cons)
   111 apply simp
   112 apply (simp add: sublist_Cons)
   113 done
   114 
   115 lemma sublist_is_Nil: "\<forall>i \<in> inds. i \<ge> length xs \<Longrightarrow> sublist xs inds = []" 
   116 apply (induct xs arbitrary: inds)
   117 apply simp
   118 apply (simp add: sublist_Cons)
   119 apply auto
   120 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   121 apply auto
   122 done
   123 
   124 lemma sublist_Nil': "sublist xs inds = [] \<Longrightarrow> \<forall>i \<in> inds. i \<ge> length xs"
   125 apply (induct xs arbitrary: inds)
   126 apply simp
   127 apply (simp add: sublist_Cons)
   128 apply (auto split: if_splits)
   129 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   130 apply (case_tac x, auto)
   131 done
   132 
   133 lemma sublist_Nil[simp]: "(sublist xs inds = []) = (\<forall>i \<in> inds. i \<ge> length xs)"
   134 apply (induct xs arbitrary: inds)
   135 apply simp
   136 apply (simp add: sublist_Cons)
   137 apply auto
   138 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   139 apply (case_tac x, auto)
   140 done
   141 
   142 lemma sublist_eq_subseteq: " \<lbrakk> inds' \<subseteq> inds; sublist xs inds = sublist ys inds \<rbrakk> \<Longrightarrow> sublist xs inds' = sublist ys inds'"
   143 apply (induct xs arbitrary: ys inds inds')
   144 apply simp
   145 apply (drule sym, rule sym)
   146 apply (simp add: sublist_Nil, fastsimp)
   147 apply (case_tac ys)
   148 apply (simp add: sublist_Nil, fastsimp)
   149 apply (auto simp add: sublist_Cons)
   150 apply (erule_tac x="list" in meta_allE)
   151 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   152 apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   153 apply fastsimp
   154 apply (erule_tac x="list" in meta_allE)
   155 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   156 apply (erule_tac x="{j. Suc j \<in> inds'}" in meta_allE)
   157 apply fastsimp
   158 done
   159 
   160 lemma sublist_eq: "\<lbrakk> \<forall>i \<in> inds. ((i < length xs) \<and> (i < length ys)) \<or> ((i \<ge> length xs ) \<and> (i \<ge> length ys)); \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
   161 apply (induct xs arbitrary: ys inds)
   162 apply simp
   163 apply (rule sym, simp add: sublist_Nil)
   164 apply (case_tac ys)
   165 apply (simp add: sublist_Nil)
   166 apply (auto simp add: sublist_Cons)
   167 apply (erule_tac x="list" in meta_allE)
   168 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   169 apply fastsimp
   170 apply (erule_tac x="list" in meta_allE)
   171 apply (erule_tac x="{j. Suc j \<in> inds}" in meta_allE)
   172 apply fastsimp
   173 done
   174 
   175 lemma sublist_eq_samelength: "\<lbrakk> length xs = length ys; \<forall>i \<in> inds. xs ! i = ys ! i \<rbrakk> \<Longrightarrow> sublist xs inds = sublist ys inds"
   176 by (rule sublist_eq, auto)
   177 
   178 lemma sublist_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist xs inds = sublist ys inds) = (\<forall>i \<in> inds. xs ! i = ys ! i)"
   179 apply (induct xs arbitrary: ys inds)
   180 apply simp
   181 apply (rule sym, simp add: sublist_Nil)
   182 apply (case_tac ys)
   183 apply (simp add: sublist_Nil)
   184 apply (auto simp add: sublist_Cons)
   185 apply (case_tac i)
   186 apply auto
   187 apply (case_tac i)
   188 apply auto
   189 done
   190 
   191 section {* Another sublist function *}
   192 
   193 function sublist' :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   194 where
   195   "sublist' n m [] = []"
   196 | "sublist' n 0 xs = []"
   197 | "sublist' 0 (Suc m) (x#xs) = (x#sublist' 0 m xs)"
   198 | "sublist' (Suc n) (Suc m) (x#xs) = sublist' n m xs"
   199 by pat_completeness auto
   200 termination by lexicographic_order
   201 
   202 subsection {* Proving equivalence to the other sublist command *}
   203 
   204 lemma sublist'_sublist: "sublist' n m xs = sublist xs {j. n \<le> j \<and> j < m}"
   205 apply (induct xs arbitrary: n m)
   206 apply simp
   207 apply (case_tac n)
   208 apply (case_tac m)
   209 apply simp
   210 apply (simp add: sublist_Cons)
   211 apply (case_tac m)
   212 apply simp
   213 apply (simp add: sublist_Cons)
   214 done
   215 
   216 
   217 lemma "sublist' n m xs = sublist xs {n..<m}"
   218 apply (induct xs arbitrary: n m)
   219 apply simp
   220 apply (case_tac n, case_tac m)
   221 apply simp
   222 apply simp
   223 apply (simp add: sublist_take')
   224 apply (case_tac m)
   225 apply simp
   226 apply (simp add: sublist_Cons sublist'_sublist)
   227 done
   228 
   229 
   230 subsection {* Showing equivalence to use of drop and take for definition *}
   231 
   232 lemma "sublist' n m xs = take (m - n) (drop n xs)"
   233 apply (induct xs arbitrary: n m)
   234 apply simp
   235 apply (case_tac m)
   236 apply simp
   237 apply (case_tac n)
   238 apply simp
   239 apply simp
   240 done
   241 
   242 subsection {* General lemma about sublist *}
   243 
   244 lemma sublist'_Nil[simp]: "sublist' i j [] = []"
   245 by simp
   246 
   247 lemma sublist'_Cons[simp]: "sublist' i (Suc j) (x#xs) = (case i of 0 \<Rightarrow> (x # sublist' 0 j xs) | Suc i' \<Rightarrow>  sublist' i' j xs)"
   248 by (cases i) auto
   249 
   250 lemma sublist'_Cons2[simp]: "sublist' i j (x#xs) = (if (j = 0) then [] else ((if (i = 0) then [x] else []) @ sublist' (i - 1) (j - 1) xs))"
   251 apply (cases j)
   252 apply auto
   253 apply (cases i)
   254 apply auto
   255 done
   256 
   257 lemma sublist_n_0: "sublist' n 0 xs = []"
   258 by (induct xs, auto)
   259 
   260 lemma sublist'_Nil': "n \<ge> m \<Longrightarrow> sublist' n m xs = []"
   261 apply (induct xs arbitrary: n m)
   262 apply simp
   263 apply (case_tac m)
   264 apply simp
   265 apply (case_tac n)
   266 apply simp
   267 apply simp
   268 done
   269 
   270 lemma sublist'_Nil2: "n \<ge> length xs \<Longrightarrow> sublist' n m xs = []"
   271 apply (induct xs arbitrary: n m)
   272 apply simp
   273 apply (case_tac m)
   274 apply simp
   275 apply (case_tac n)
   276 apply simp
   277 apply simp
   278 done
   279 
   280 lemma sublist'_Nil3: "(sublist' n m xs = []) = ((n \<ge> m) \<or> (n \<ge> length xs))"
   281 apply (induct xs arbitrary: n m)
   282 apply simp
   283 apply (case_tac m)
   284 apply simp
   285 apply (case_tac n)
   286 apply simp
   287 apply simp
   288 done
   289 
   290 lemma sublist'_notNil: "\<lbrakk> n < length xs; n < m \<rbrakk> \<Longrightarrow> sublist' n m xs \<noteq> []"
   291 apply (induct xs arbitrary: n m)
   292 apply simp
   293 apply (case_tac m)
   294 apply simp
   295 apply (case_tac n)
   296 apply simp
   297 apply simp
   298 done
   299 
   300 lemma sublist'_single: "n < length xs \<Longrightarrow> sublist' n (Suc n) xs = [xs ! n]"
   301 apply (induct xs arbitrary: n)
   302 apply simp
   303 apply simp
   304 apply (case_tac n)
   305 apply (simp add: sublist_n_0)
   306 apply simp
   307 done
   308 
   309 lemma sublist'_update1: "i \<ge> m \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   310 apply (induct xs arbitrary: n m i)
   311 apply simp
   312 apply simp
   313 apply (case_tac i)
   314 apply simp
   315 apply simp
   316 done
   317 
   318 lemma sublist'_update2: "i < n \<Longrightarrow> sublist' n m (xs[i:=v]) = sublist' n m xs"
   319 apply (induct xs arbitrary: n m i)
   320 apply simp
   321 apply simp
   322 apply (case_tac i)
   323 apply simp
   324 apply simp
   325 done
   326 
   327 lemma sublist'_update3: "\<lbrakk>n \<le> i; i < m\<rbrakk> \<Longrightarrow> sublist' n m (xs[i := v]) = (sublist' n m xs)[i - n := v]"
   328 proof (induct xs arbitrary: n m i)
   329   case Nil thus ?case by auto
   330 next
   331   case (Cons x xs)
   332   thus ?case
   333     apply -
   334     apply auto
   335     apply (cases i)
   336     apply auto
   337     apply (cases i)
   338     apply auto
   339     done
   340 qed
   341 
   342 lemma "\<lbrakk> sublist' i j xs = sublist' i j ys; n \<ge> i; m \<le> j \<rbrakk> \<Longrightarrow> sublist' n m xs = sublist' n m ys"
   343 proof (induct xs arbitrary: i j ys n m)
   344   case Nil
   345   thus ?case
   346     apply -
   347     apply (rule sym, drule sym)
   348     apply (simp add: sublist'_Nil)
   349     apply (simp add: sublist'_Nil3)
   350     apply arith
   351     done
   352 next
   353   case (Cons x xs i j ys n m)
   354   note c = this
   355   thus ?case
   356   proof (cases m)
   357     case 0 thus ?thesis by (simp add: sublist_n_0)
   358   next
   359     case (Suc m')
   360     note a = this
   361     thus ?thesis
   362     proof (cases n)
   363       case 0 note b = this
   364       show ?thesis
   365       proof (cases ys)
   366         case Nil  with a b Cons.prems show ?thesis by (simp add: sublist'_Nil3)
   367       next
   368         case (Cons y ys)
   369         show ?thesis
   370         proof (cases j)
   371           case 0 with a b Cons.prems show ?thesis by simp
   372         next
   373           case (Suc j') with a b Cons.prems Cons show ?thesis 
   374             apply -
   375             apply (simp, rule Cons.hyps [of "0" "j'" "ys" "0" "m'"], auto)
   376             done
   377         qed
   378       qed
   379     next
   380       case (Suc n')
   381       show ?thesis
   382       proof (cases ys)
   383         case Nil with Suc a Cons.prems show ?thesis by (auto simp add: sublist'_Nil3)
   384       next
   385         case (Cons y ys) with Suc a Cons.prems show ?thesis
   386           apply -
   387           apply simp
   388           apply (cases j)
   389           apply simp
   390           apply (cases i)
   391           apply simp
   392           apply (rule_tac j="nat" in Cons.hyps [of "0" _ "ys" "n'" "m'"])
   393           apply simp
   394           apply simp
   395           apply simp
   396           apply simp
   397           apply (rule_tac i="nata" and j="nat" in Cons.hyps [of _ _ "ys" "n'" "m'"])
   398           apply simp
   399           apply simp
   400           apply simp
   401           done
   402       qed
   403     qed
   404   qed
   405 qed
   406 
   407 lemma length_sublist': "j \<le> length xs \<Longrightarrow> length (sublist' i j xs) = j - i"
   408 by (induct xs arbitrary: i j, auto)
   409 
   410 lemma sublist'_front: "\<lbrakk> i < j; i < length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = xs ! i # sublist' (Suc i) j xs"
   411 apply (induct xs arbitrary: a i j)
   412 apply simp
   413 apply (case_tac j)
   414 apply simp
   415 apply (case_tac i)
   416 apply simp
   417 apply simp
   418 done
   419 
   420 lemma sublist'_back: "\<lbrakk> i < j; j \<le> length xs \<rbrakk> \<Longrightarrow> sublist' i j xs = sublist' i (j - 1) xs @ [xs ! (j - 1)]"
   421 apply (induct xs arbitrary: a i j)
   422 apply simp
   423 apply simp
   424 apply (case_tac j)
   425 apply simp
   426 apply auto
   427 apply (case_tac nat)
   428 apply auto
   429 done
   430 
   431 (* suffices that j \<le> length xs and length ys *) 
   432 lemma sublist'_eq_samelength_iff: "length xs = length ys \<Longrightarrow> (sublist' i j xs  = sublist' i j ys) = (\<forall>i'. i \<le> i' \<and> i' < j \<longrightarrow> xs ! i' = ys ! i')"
   433 proof (induct xs arbitrary: ys i j)
   434   case Nil thus ?case by simp
   435 next
   436   case (Cons x xs)
   437   thus ?case
   438     apply -
   439     apply (cases ys)
   440     apply simp
   441     apply simp
   442     apply auto
   443     apply (case_tac i', auto)
   444     apply (erule_tac x="Suc i'" in allE, auto)
   445     apply (erule_tac x="i' - 1" in allE, auto)
   446     apply (case_tac i', auto)
   447     apply (erule_tac x="Suc i'" in allE, auto)
   448     done
   449 qed
   450 
   451 lemma sublist'_all[simp]: "sublist' 0 (length xs) xs = xs"
   452 by (induct xs, auto)
   453 
   454 lemma sublist'_sublist': "sublist' n m (sublist' i j xs) = sublist' (i + n) (min (i + m) j) xs" 
   455 by (induct xs arbitrary: i j n m) (auto simp add: min_diff)
   456 
   457 lemma sublist'_append: "\<lbrakk> i \<le> j; j \<le> k \<rbrakk> \<Longrightarrow>(sublist' i j xs) @ (sublist' j k xs) = sublist' i k xs"
   458 by (induct xs arbitrary: i j k) auto
   459 
   460 lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
   461 apply (induct xs arbitrary: i j k)
   462 apply auto
   463 apply (case_tac k)
   464 apply auto
   465 apply (case_tac i)
   466 apply auto
   467 done
   468 
   469 lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"
   470 apply (simp add: sublist'_sublist)
   471 apply (simp add: set_sublist)
   472 apply auto
   473 done
   474 
   475 lemma all_in_set_sublist'_conv: "(\<forall>j. j \<in> set (sublist' l r xs) \<longrightarrow> P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
   476 unfolding set_sublist' by blast
   477 
   478 lemma ball_in_set_sublist'_conv: "(\<forall>j \<in> set (sublist' l r xs). P j) = (\<forall>k. l \<le> k \<and> k < r \<and> k < List.length xs \<longrightarrow> P (xs ! k))"
   479 unfolding set_sublist' by blast
   480 
   481 
   482 lemma multiset_of_sublist:
   483 assumes l_r: "l \<le> r \<and> r \<le> List.length xs"
   484 assumes left: "\<forall> i. i < l \<longrightarrow> (xs::'a list) ! i = ys ! i"
   485 assumes right: "\<forall> i. i \<ge> r \<longrightarrow> (xs::'a list) ! i = ys ! i"
   486 assumes multiset: "multiset_of xs = multiset_of ys"
   487   shows "multiset_of (sublist' l r xs) = multiset_of (sublist' l r ys)"
   488 proof -
   489   from l_r have xs_def: "xs = (sublist' 0 l xs) @ (sublist' l r xs) @ (sublist' r (List.length xs) xs)" (is "_ = ?xs_long") 
   490     by (simp add: sublist'_append)
   491   from multiset have length_eq: "List.length xs = List.length ys" by (rule multiset_of_eq_length)
   492   with l_r have ys_def: "ys = (sublist' 0 l ys) @ (sublist' l r ys) @ (sublist' r (List.length ys) ys)" (is "_ = ?ys_long") 
   493     by (simp add: sublist'_append)
   494   from xs_def ys_def multiset have "multiset_of ?xs_long = multiset_of ?ys_long" by simp
   495   moreover
   496   from left l_r length_eq have "sublist' 0 l xs = sublist' 0 l ys"
   497     by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   498   moreover
   499   from right l_r length_eq have "sublist' r (List.length xs) xs = sublist' r (List.length ys) ys"
   500     by (auto simp add: length_sublist' nth_sublist' intro!: nth_equalityI)
   501   moreover
   502   ultimately show ?thesis by (simp add: multiset_of_append)
   503 qed
   504 
   505 
   506 end