Theory List_Lemmas

section ‹Appendix›
subsection ‹List Lemmas›

theory List_Lemmas
  imports Main
begin

text‹In this theory some simple equalities about lists are established.›

lemma len_those:
  assumes "those l ≠ None"
  shows "length (the (those l)) = length l" 
using assms proof(induct l)
  case Nil
  then show ?case by simp 
next
  case (Cons a l)
  hence "∃x. a = Some x" using those.simps
    using option.collapse by fastforce 
  then obtain x where "a=Some x" by auto
  hence AL: "those (a#l) = map_option (Cons x) (those l)" using those.simps by auto
  hence "those l ≠ None" using assms Cons.prems by auto 
  hence "length (the (those l)) = length l" using Cons by simp
  then show ?case using AL ‹those l ≠ None› by (simp add: option.map_sel)
qed

lemma the_those_n:
  assumes "those (l:: 'a option list) ≠ None" and "(n::nat) < length l"
  shows "(the (those l)) ! n = the (l ! n)" 
  using assms proof (induct l arbitrary: n)
  case Nil
  then show ?case by simp 
next
  case (Cons a l)
  from assms(1) have l_notNone: "those l ≠ None" using those.simps(2)
    by (metis (no_types, lifting) Cons.prems(1) option.collapse option.map_disc_iff option.simps(4) option.simps(5)) 
  from assms(1) have "∃b. a=Some b" using those.simps
    using Cons.prems(1) not_None_eq by fastforce
  from this obtain b where "a=Some b" by auto 
  hence those_al: "those (a#l) = (Some (b# (the (those l))))" using those.simps l_notNone by simp
  then show ?case proof(cases "n=0")
    case True    
    have "the (those (a # l)) ! n = the (Some (b# (the (those l)))) ! n" using those_al nth_def by simp
    also have "... = b" using True by simp
    also have "... = the ((a # l) ! n)" using ‹a=Some b› True by simp 
    finally show ?thesis .
  next
    case False
    hence "∃m. n= Suc m" using old.nat.exhaust by auto 
    from this obtain m where "n = Suc m" by auto
    hence "m < length l" using assms(2) Cons.prems(2) by auto
    hence "the (those l) ! m = the (l ! m)" using Cons l_notNone by simp
    hence A: "the (those l) ! m = the ((a#l) ! n)" using ‹n = Suc m› by auto 
    have "the (those l) ! m = the (those (a # l)) ! n" using ‹n = Suc m› those.simps(2) those_al nth_def
      by simp
    then show ?thesis using A by simp
  qed
qed 

lemma those_all_Some:
  assumes "those l ≠ None" and "n < length l"
  shows "(l ! n)≠None" 
  using assms proof(induct l arbitrary:n)
  case Nil
  then show ?case by simp
next
  case (Cons a l)
  from assms(1) have l_notNone: "those l ≠ None" using those.simps(2)
    by (metis (no_types, lifting) Cons.prems(1) option.collapse option.map_disc_iff option.simps(4) option.simps(5))
  from assms(1) have "∃b. a=Some b" using those.simps
    using Cons.prems(1) not_None_eq by fastforce
  from this obtain b where "a=Some b" by auto 
   then show ?case proof(cases "n=0")
     case True
     then show ?thesis using ‹a=Some b› by fastforce 
   next
     case False
     hence "∃m. n= Suc m" using old.nat.exhaust by auto 
     from this obtain m where "n = Suc m" by auto
     hence "m < length l" using assms(2) Cons.prems(2) by auto
     hence "l ! m ≠ None" using Cons l_notNone by simp
     then show ?thesis using ‹n = Suc m› by simp
   qed
qed

lemma those_map_not_None: 
  assumes "∀n< length xs. f (xs ! n) ≠ None" 
  shows "those (map f xs) ≠ None"
using assms proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  hence " f ((a # xs) ! 0) ≠ None" using Cons(2) by auto 
  hence "∃b. f a = Some b" by auto
  from this obtain b where "f a = Some b" by auto
  have "those (map f xs) ≠ None" using Cons(1) assms those.simps
    by (smt (verit) Cons.prems Ex_less_Suc length_Cons less_trans_Suc nth_Cons_Suc)  
  then show ?case using those.simps ‹f a = Some b›
    by (simp)
qed

lemma last_len:
  assumes "length xs = Suc n"
  shows "last xs = xs ! n"
by (metis One_nat_def assms diff_Suc_1' last_conv_nth length_0_conv nat.discI)

end