1 theory Moment

     2 imports Main

     3 begin

     4 

     5 fun firstn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"

     6 where

     7   "firstn 0 s = []" |

     8   "firstn (Suc n) [] = []" |

     9   "firstn (Suc n) (e#s) = e#(firstn n s)"

    10 

    11 fun restn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"

    12 where "restn n s = rev (firstn (length s - n) (rev s))"

    13 

    14 definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"

    15 where "moment n s = rev (firstn n (rev s))"

    16 

    17 definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"

    18 where "restm n s = rev (restn n (rev s))"

    19 

    20 definition from_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"

    21   where "from_to i j s = firstn (j - i) (restn i s)"

    22 

    23 definition down_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list"

    24 where "down_to j i s = rev (from_to i j (rev s))"

    25 

    26 (*

    27 value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]"

    28 value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]"

    29 *)

    30 

    31 lemma length_eq_elim_l: "\<lbrakk>length xs = length ys; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs"

    32   by auto

    33 

    34 lemma length_eq_elim_r: "\<lbrakk>length us = length vs; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs"

    35   by simp

    36 

    37 lemma firstn_nil [simp]: "firstn n [] = []"

    38   by (cases n, simp+)

    39 

    40 (*

    41 value "from_to 0 2 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] @ 

    42        from_to 2 5 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]"

    43 *)

    44 

    45 lemma firstn_le: "\<And> n s'. n \<le> length s \<Longrightarrow> firstn n (s@s') = firstn n s"

    46 proof (induct s, simp)

    47   fix a s n s'

    48   assume ih: "\<And>n s'. n \<le> length s \<Longrightarrow> firstn n (s @ s') = firstn n s"

    49   and le_n: " n \<le> length (a # s)"

    50   show "firstn n ((a # s) @ s') = firstn n (a # s)"

    51   proof(cases n, simp)

    52     fix k

    53     assume eq_n: "n = Suc k"

    54     with le_n have "k \<le> length s" by auto

    55     from ih [OF this] and eq_n

    56     show "firstn n ((a # s) @ s') = firstn n (a # s)" by auto

    57   qed

    58 qed

    59 

    60 lemma firstn_ge [simp]: "\<And>n. length s \<le> n \<Longrightarrow> firstn n s = s"

    61 proof(induct s, simp)

    62   fix a s n

    63   assume ih: "\<And>n. length s \<le> n \<Longrightarrow> firstn n s = s"

    64     and le: "length (a # s) \<le> n"

    65   show "firstn n (a # s) = a # s"

    66   proof(cases n)

    67     assume eq_n: "n = 0" with le show ?thesis by simp

    68   next

    69     fix k

    70     assume eq_n: "n = Suc k"

    71     with le have le_k: "length s \<le> k" by simp

    72     from ih [OF this] have "firstn k s = s" .

    73     from eq_n and this

    74     show ?thesis by simp

    75   qed

    76 qed

    77 

    78 lemma firstn_eq [simp]: "firstn (length s) s = s"

    79   by simp

    80 

    81 lemma firstn_restn_s: "(firstn n (s::'a list)) @ (restn n s) = s"

    82 proof(induct n arbitrary:s, simp)

    83   fix n s

    84   assume ih: "\<And>t. firstn n (t::'a list) @ restn n t = t"

    85   show "firstn (Suc n) (s::'a list) @ restn (Suc n) s = s"

    86   proof(cases s, simp)

    87     fix x xs

    88     assume eq_s: "s = x#xs"

    89     show "firstn (Suc n) s @ restn (Suc n) s = s"

    90     proof -

    91       have "firstn (Suc n) s @ restn (Suc n) s =  x # (firstn n xs @ restn n xs)"

    92       proof -

    93         from eq_s have "firstn (Suc n) s =  x # firstn n xs" by simp

    94         moreover have "restn (Suc n) s = restn n xs"

    95         proof -

    96           from eq_s have "restn (Suc n) s = rev (firstn (length xs - n) (rev xs @ [x]))" by simp

    97           also have "\<dots> = restn n xs"

    98           proof -

    99             have "(firstn (length xs - n) (rev xs @ [x])) = (firstn (length xs - n) (rev xs))"

   100               by(rule firstn_le, simp)

   101             hence "rev (firstn (length xs - n) (rev xs @ [x])) = 

   102               rev (firstn (length xs - n) (rev xs))" by simp

   103             also have "\<dots> = rev (firstn (length (rev xs) - n) (rev xs))" by simp

   104             finally show ?thesis by simp

   105           qed

   106           finally show ?thesis by simp

   107         qed

   108         ultimately show ?thesis by simp

   109       qed with ih eq_s show ?thesis by simp

   110     qed

   111   qed

   112 qed

   113 

   114 lemma moment_restm_s: "(restm n s)@(moment n s) = s"

   115 proof -

   116   have " rev  ((firstn n (rev s)) @ (restn n (rev s))) = s" (is "rev ?x = s")

   117   proof -

   118     have "?x = rev s" by (simp only:firstn_restn_s)

   119     thus ?thesis by auto

   120   qed

   121   thus ?thesis 

   122     by (auto simp:restm_def moment_def)

   123 qed

   124 

   125 declare restn.simps [simp del] firstn.simps[simp del]

   126 

   127 lemma length_firstn_ge: "length s \<le> n \<Longrightarrow> length (firstn n s) = length s"

   128 proof(induct n arbitrary:s, simp add:firstn.simps)

   129   case (Suc k)

   130   assume ih: "\<And> s. length (s::'a list) \<le> k \<Longrightarrow> length (firstn k s) = length s"

   131   and le: "length s \<le> Suc k"

   132   show ?case

   133   proof(cases s)

   134     case Nil

   135     from Nil show ?thesis by simp

   136   next

   137     case (Cons x xs)

   138     from le and Cons have "length xs \<le> k" by simp

   139     from ih [OF this] have "length (firstn k xs) = length xs" .

   140     moreover from Cons have "length (firstn (Suc k) s) = Suc (length (firstn k xs))" 

   141       by (simp add:firstn.simps)

   142     moreover note Cons

   143     ultimately show ?thesis by simp

   144   qed

   145 qed

   146 

   147 lemma length_firstn_le: "n \<le> length s \<Longrightarrow> length (firstn n s) = n"

   148 proof(induct n arbitrary:s, simp add:firstn.simps)

   149   case (Suc k)

   150   assume ih: "\<And>s. k \<le> length (s::'a list) \<Longrightarrow> length (firstn k s) = k"

   151     and le: "Suc k \<le> length s"

   152   show ?case

   153   proof(cases s)

   154     case Nil

   155     from Nil and le show ?thesis by auto

   156   next

   157     case (Cons x xs)

   158     from le and Cons have "k \<le> length xs" by simp

   159     from ih [OF this] have "length (firstn k xs) = k" .

   160     moreover from Cons have "length (firstn (Suc k) s) = Suc (length (firstn k xs))" 

   161       by (simp add:firstn.simps)

   162     ultimately show ?thesis by simp

   163   qed

   164 qed

   165 

   166 lemma app_firstn_restn: 

   167   fixes s1 s2

   168   shows "s1 = firstn (length s1) (s1 @ s2) \<and> s2 = restn (length s1) (s1 @ s2)"

   169 proof(rule length_eq_elim_l)

   170   have "length s1 \<le> length (s1 @ s2)" by simp

   171   from length_firstn_le [OF this]

   172   show "length s1 = length (firstn (length s1) (s1 @ s2))" by simp

   173 next

   174   from firstn_restn_s 

   175   show "s1 @ s2 = firstn (length s1) (s1 @ s2) @ restn (length s1) (s1 @ s2)"

   176     by metis

   177 qed

   178 

   179 

   180 lemma length_moment_le:

   181   fixes k s

   182   assumes le_k: "k \<le> length s"

   183   shows "length (moment k s) = k"

   184 proof -

   185   have "length (rev (firstn k (rev s))) = k"

   186   proof -

   187     have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp

   188     also have "\<dots> = k" 

   189     proof(rule length_firstn_le)

   190       from le_k show "k \<le> length (rev s)" by simp

   191     qed

   192     finally show ?thesis .

   193   qed

   194   thus ?thesis by (simp add:moment_def)

   195 qed

   196 

   197 lemma app_moment_restm: 

   198   fixes s1 s2

   199   shows "s1 = restm (length s2) (s1 @ s2) \<and> s2 = moment (length s2) (s1 @ s2)"

   200 proof(rule length_eq_elim_r)

   201   have "length s2 \<le> length (s1 @ s2)" by simp

   202   from length_moment_le [OF this]

   203   show "length s2 = length (moment (length s2) (s1 @ s2))" by simp

   204 next

   205   from moment_restm_s 

   206   show "s1 @ s2 = restm (length s2) (s1 @ s2) @ moment (length s2) (s1 @ s2)"

   207     by metis

   208 qed

   209 

   210 lemma length_moment_ge:

   211   fixes k s

   212   assumes le_k: "length s \<le> k"

   213   shows "length (moment k s) = (length s)"

   214 proof -

   215   have "length (rev (firstn k (rev s))) = length s"

   216   proof -

   217     have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp

   218     also have "\<dots> = length s" 

   219     proof -

   220       have "\<dots> = length (rev s)"

   221       proof(rule length_firstn_ge)

   222         from le_k show "length (rev s) \<le> k" by simp

   223       qed

   224       also have "\<dots> = length s" by simp

   225       finally show ?thesis .

   226     qed

   227     finally show ?thesis .

   228   qed

   229   thus ?thesis by (simp add:moment_def)

   230 qed

   231 

   232 lemma length_firstn: "(length (firstn n s) = length s) \<or> (length (firstn n s) = n)"

   233 proof(cases "n \<le> length s")

   234   case True

   235   from length_firstn_le [OF True] show ?thesis by auto

   236 next

   237   case False

   238   from False have "length s \<le> n" by simp

   239   from firstn_ge [OF this] show ?thesis by auto

   240 qed

   241 

   242 lemma firstn_conc: 

   243   fixes m n

   244   assumes le_mn: "m \<le> n"

   245   shows "firstn m s = firstn m (firstn n  s)"

   246 proof(cases "m \<le> length s")

   247   case True

   248   have "s = (firstn n s) @ (restn n s)" by (simp add:firstn_restn_s)

   249   hence "firstn m s = firstn m \<dots>" by simp

   250   also have "\<dots> = firstn m (firstn n s)" 

   251   proof -

   252     from length_firstn [of n s]

   253     have "m \<le> length (firstn n s)"

   254     proof

   255       assume "length (firstn n s) = length s" with True show ?thesis by simp

   256     next

   257       assume "length (firstn n s) = n " with le_mn show ?thesis by simp

   258     qed

   259     from firstn_le [OF this, of "restn n s"]

   260     show ?thesis .

   261   qed

   262   finally show ?thesis by simp

   263 next

   264   case False

   265   from False and le_mn have "length s \<le> n"  by simp

   266   from firstn_ge [OF this] show ?thesis by simp

   267 qed

   268 

   269 lemma restn_conc: 

   270   fixes i j k s

   271   assumes eq_k: "j + i = k"

   272   shows "restn k s = restn j (restn i s)"

   273 proof -

   274   have "(firstn (length s - k) (rev s)) =

   275         (firstn (length (rev (firstn (length s - i) (rev s))) - j) 

   276                             (rev (rev (firstn (length s - i) (rev s)))))"

   277   proof  -

   278     have "(firstn (length s - k) (rev s)) =

   279             (firstn (length (rev (firstn (length s - i) (rev s))) - j) 

   280                                            (firstn (length s - i) (rev s)))"

   281     proof -

   282       have " (length (rev (firstn (length s - i) (rev s))) - j) = length s - k"

   283       proof -

   284         have "(length (rev (firstn (length s - i) (rev s))) - j) = (length s - i) - j"

   285         proof -

   286           have "(length (rev (firstn (length s - i) (rev s))) - j) = 

   287                                          length ((firstn (length s - i) (rev s))) - j"

   288             by simp

   289           also have "\<dots> = length ((firstn (length (rev s) - i) (rev s))) - j" by simp

   290           also have "\<dots> = (length (rev s) - i) - j" 

   291           proof -

   292             have "length ((firstn (length (rev s) - i) (rev s))) = (length (rev s) - i)"

   293               by (rule length_firstn_le, simp)

   294             thus ?thesis by simp

   295           qed

   296           also have "\<dots> = (length s - i) - j" by simp

   297           finally show ?thesis .

   298         qed

   299         with eq_k show ?thesis by auto

   300       qed

   301       moreover have "(firstn (length s - k) (rev s)) =

   302                              (firstn (length s - k) (firstn (length s - i) (rev s)))"

   303       proof(rule firstn_conc)

   304         from eq_k show "length s - k \<le> length s - i" by simp

   305       qed

   306       ultimately show ?thesis by simp

   307     qed

   308     thus ?thesis by simp

   309   qed

   310   thus ?thesis by (simp only:restn.simps)

   311 qed

   312 

   313 (*

   314 value "down_to 2 0 [5, 4, 3, 2, 1, 0]"

   315 value "moment 2 [5, 4, 3, 2, 1, 0]"

   316 *)

   317 

   318 lemma from_to_firstn: "from_to 0 k s = firstn k s"

   319 by (simp add:from_to_def restn.simps)

   320 

   321 lemma moment_app [simp]:

   322   assumes 

   323   ile: "i \<le> length s"

   324   shows "moment i (s'@s) = moment i s"

   325 proof -

   326   have "moment i (s'@s) = rev (firstn i (rev (s'@s)))" by (simp add:moment_def)

   327   moreover have "firstn i (rev (s'@s)) = firstn i (rev s @ rev s')" by simp

   328   moreover have "\<dots> = firstn i (rev s)"

   329   proof(rule firstn_le)

   330     have "length (rev s) = length s" by simp

   331     with ile show "i \<le> length (rev s)" by simp

   332   qed

   333   ultimately show ?thesis by (simp add:moment_def)

   334 qed

   335 

   336 lemma moment_eq [simp]: "moment (length s) (s'@s) = s"

   337 proof -

   338   have "length s \<le> length s" by simp

   339   from moment_app [OF this, of s'] 

   340   have " moment (length s) (s' @ s) = moment (length s) s" .

   341   moreover have "\<dots> = s" by (simp add:moment_def)

   342   ultimately show ?thesis by simp

   343 qed

   344 

   345 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s"

   346   by (unfold moment_def, simp)

   347 

   348 lemma moment_zero [simp]: "moment 0 s = []"

   349   by (simp add:moment_def firstn.simps)

   350 

   351 lemma p_split_gen: 

   352   "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk> \<Longrightarrow>

   353   (\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"

   354 proof (induct s, simp)

   355   fix a s

   356   assume ih: "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk>

   357            \<Longrightarrow> \<exists>i<length s. k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall>i'>i. Q (moment i' s))"

   358     and nq: "\<not> Q (moment k (a # s))" and qa: "Q (a # s)"

   359   have le_k: "k \<le> length s"

   360   proof -

   361     { assume "length s < k"

   362       hence "length (a#s) \<le> k" by simp

   363       from moment_ge [OF this] and nq and qa

   364       have "False" by auto

   365     } thus ?thesis by arith

   366   qed

   367   have nq_k: "\<not> Q (moment k s)"

   368   proof -

   369     have "moment k (a#s) = moment k s"

   370     proof -

   371       from moment_app [OF le_k, of "[a]"] show ?thesis by simp

   372     qed

   373     with nq show ?thesis by simp

   374   qed

   375   show "\<exists>i<length (a # s). k \<le> i \<and> \<not> Q (moment i (a # s)) \<and> (\<forall>i'>i. Q (moment i' (a # s)))"

   376   proof -

   377     { assume "Q s"

   378       from ih [OF this nq_k]

   379       obtain i where lti: "i < length s" 

   380         and nq: "\<not> Q (moment i s)" 

   381         and rst: "\<forall>i'>i. Q (moment i' s)" 

   382         and lki: "k \<le> i" by auto

   383       have ?thesis 

   384       proof -

   385         from lti have "i < length (a # s)" by auto

   386         moreover have " \<not> Q (moment i (a # s))"

   387         proof -

   388           from lti have "i \<le> (length s)" by simp

   389           from moment_app [OF this, of "[a]"]

   390           have "moment i (a # s) = moment i s" by simp

   391           with nq show ?thesis by auto

   392         qed

   393         moreover have " (\<forall>i'>i. Q (moment i' (a # s)))"

   394         proof -

   395           {

   396             fix i'

   397             assume lti': "i < i'"

   398             have "Q (moment i' (a # s))"

   399             proof(cases "length (a#s) \<le> i'")

   400               case True

   401               from True have "moment i' (a#s) = a#s" by simp

   402               with qa show ?thesis by simp

   403             next

   404               case False

   405               from False have "i' \<le> length s" by simp

   406               from moment_app [OF this, of "[a]"]

   407               have "moment i' (a#s) = moment i' s" by simp

   408               with rst lti' show ?thesis by auto

   409             qed

   410           } thus ?thesis by auto

   411         qed

   412         moreover note lki

   413         ultimately show ?thesis by auto

   414       qed

   415     } moreover {

   416       assume ns: "\<not> Q s"

   417       have ?thesis

   418       proof -

   419         let ?i = "length s"

   420         have "\<not> Q (moment ?i (a#s))"

   421         proof -

   422           have "?i \<le> length s" by simp

   423           from moment_app [OF this, of "[a]"]

   424           have "moment ?i (a#s) = moment ?i s" by simp

   425           moreover have "\<dots> = s" by simp

   426           ultimately show ?thesis using ns by auto

   427         qed

   428         moreover have "\<forall> i' > ?i. Q (moment i' (a#s))" 

   429         proof -

   430           { fix i'

   431             assume "i' > ?i"

   432             hence "length (a#s) \<le> i'" by simp

   433             from moment_ge [OF this] 

   434             have " moment i' (a # s) = a # s" .

   435             with qa have "Q (moment i' (a#s))" by simp

   436           } thus ?thesis by auto

   437         qed

   438         moreover have "?i < length (a#s)" by simp

   439         moreover note le_k

   440         ultimately show ?thesis by auto

   441       qed

   442     } ultimately show ?thesis by auto

   443   qed

   444 qed

   445 

   446 lemma p_split: 

   447   "\<And> s Q. \<lbrakk>Q s; \<not> Q []\<rbrakk> \<Longrightarrow> 

   448        (\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"

   449 proof -

   450   fix s Q

   451   assume qs: "Q s" and nq: "\<not> Q []"

   452   from nq have "\<not> Q (moment 0 s)" by simp

   453   from p_split_gen [of Q s 0, OF qs this]

   454   show "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))"

   455     by auto

   456 qed

   457 

   458 lemma moment_plus: 

   459   "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)"

   460 proof(induct s, simp+)

   461   fix a s

   462   assume ih: "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = hd (moment (Suc i) s) # moment i s"

   463     and le_i: "i \<le> length s"

   464   show "moment (Suc i) (a # s) = hd (moment (Suc i) (a # s)) # moment i (a # s)"

   465   proof(cases "i= length s")

   466     case True

   467     hence "Suc i = length (a#s)" by simp

   468     with moment_eq have "moment (Suc i) (a#s) = a#s" by auto

   469     moreover have "moment i (a#s) = s"

   470     proof -

   471       from moment_app [OF le_i, of "[a]"]

   472       and True show ?thesis by simp

   473     qed

   474     ultimately show ?thesis by auto

   475   next

   476     case False

   477     from False and le_i have lti: "i < length s" by arith

   478     hence les_i: "Suc i \<le> length s" by arith

   479     show ?thesis 

   480     proof -

   481       from moment_app [OF les_i, of "[a]"]

   482       have "moment (Suc i) (a # s) = moment (Suc i) s" by simp

   483       moreover have "moment i (a#s) = moment i s" 

   484       proof -

   485         from lti have "i \<le> length s" by simp

   486         from moment_app [OF this, of "[a]"] show ?thesis by simp

   487       qed

   488       moreover note ih [OF les_i]

   489       ultimately show ?thesis by auto

   490     qed

   491   qed

   492 qed

   493 

   494 lemma from_to_conc:

   495   fixes i j k s

   496   assumes le_ij: "i \<le> j"

   497   and le_jk: "j \<le> k"

   498   shows "from_to i j s @ from_to j k s = from_to i k s"

   499 proof -

   500   let ?ris = "restn i s"

   501   have "firstn (j - i) (restn i s) @ firstn (k - j) (restn j s) =

   502          firstn (k - i) (restn i s)" (is "?x @ ?y = ?z")

   503   proof -

   504     let "firstn (k-j) ?u" = "?y"

   505     let ?rst = " restn (k - j) (restn (j - i) ?ris)"

   506     let ?rst' = "restn (k - i) ?ris"

   507     have "?u = restn (j-i) ?ris"

   508     proof(rule restn_conc)

   509       from le_ij show "j - i + i = j" by simp

   510     qed

   511     hence "?x @ ?y = ?x @ firstn (k-j) (restn (j-i) ?ris)" by simp

   512     moreover have "firstn (k - j) (restn (j - i) (restn i s)) @ ?rst = 

   513                       restn (j-i) ?ris" by (simp add:firstn_restn_s)

   514     ultimately have "?x @ ?y @ ?rst = ?x @ (restn (j-i) ?ris)" by simp

   515     also have "\<dots> = ?ris" by (simp add:firstn_restn_s)

   516     finally have "?x @ ?y @ ?rst = ?ris" .

   517     moreover have "?z @ ?rst = ?ris"

   518     proof -

   519       have "?z @ ?rst' = ?ris" by (simp add:firstn_restn_s)

   520       moreover have "?rst' = ?rst"

   521       proof(rule restn_conc)

   522         from le_ij le_jk show "k - j + (j - i) = k - i" by auto

   523       qed

   524       ultimately show ?thesis by simp

   525     qed

   526     ultimately have "?x @ ?y @ ?rst = ?z @ ?rst" by simp

   527     thus ?thesis by auto    

   528   qed

   529   thus ?thesis by (simp only:from_to_def)

   530 qed

   531 

   532 lemma down_to_conc:

   533   fixes i j k s

   534   assumes le_ij: "i \<le> j"

   535   and le_jk: "j \<le> k"

   536   shows "down_to k j s @ down_to j i s = down_to k i s"

   537 proof -

   538   have "rev (from_to j k (rev s)) @ rev (from_to i j (rev s)) = rev (from_to i k (rev s))"

   539     (is "?L = ?R")

   540   proof -

   541     have "?L = rev (from_to i j (rev s) @ from_to j k (rev s))" by simp

   542     also have "\<dots> = ?R" (is "rev ?x = rev ?y")

   543     proof -

   544       have "?x = ?y" by (rule from_to_conc[OF le_ij le_jk])

   545       thus ?thesis by simp

   546     qed

   547     finally show ?thesis .

   548   qed

   549   thus ?thesis by (simp add:down_to_def)

   550 qed

   551 

   552 lemma restn_ge:

   553   fixes s k

   554   assumes le_k: "length s \<le> k"

   555   shows "restn k s = []"

   556 proof -

   557   from firstn_restn_s [of k s, symmetric] have "s = (firstn k s) @ (restn k s)" .

   558   hence "length s = length \<dots>" by simp

   559   also have "\<dots> = length (firstn k s) + length (restn k s)" by simp

   560   finally have "length s = ..." by simp

   561   moreover from length_firstn_ge and le_k 

   562   have "length (firstn k s) = length s" by simp

   563   ultimately have "length (restn k s) = 0" by auto

   564   thus ?thesis by auto

   565 qed

   566 

   567 lemma from_to_ge: "length s \<le> k \<Longrightarrow> from_to k j s = []"

   568 proof(simp only:from_to_def)

   569   assume "length s \<le> k"

   570   from restn_ge [OF this] 

   571   show "firstn (j - k) (restn k s) = []" by simp

   572 qed

   573 

   574 (*

   575 value "from_to 2 5 [0, 1, 2, 3, 4]"

   576 value "restn 2  [0, 1, 2, 3, 4]"

   577 *)

   578 

   579 lemma from_to_restn: 

   580   fixes k j s

   581   assumes le_j: "length s \<le> j"

   582   shows "from_to k j s = restn k s"

   583 proof -

   584   have "from_to 0 k s @ from_to k j s = from_to 0 j s"

   585   proof(cases "k \<le> j")

   586     case True

   587     from from_to_conc True show ?thesis by auto

   588   next

   589     case False

   590     from False le_j have lek: "length s \<le>  k" by auto

   591     from from_to_ge [OF this] have "from_to k j s = []" .

   592     hence "from_to 0 k s @ from_to k j s = from_to 0 k s" by simp

   593     also have "\<dots> = s"

   594     proof -

   595       from from_to_firstn [of k s]

   596       have "\<dots> = firstn k s" .

   597       also have "\<dots> = s" by (rule firstn_ge [OF lek])

   598       finally show ?thesis .

   599     qed

   600     finally have "from_to 0 k s @ from_to k j s = s" .

   601     moreover have "from_to 0 j s = s"

   602     proof -

   603       have "from_to 0 j s = firstn j s" by (simp add:from_to_firstn)

   604       also have "\<dots> = s"

   605       proof(rule firstn_ge)

   606         from le_j show "length s \<le> j " by simp

   607       qed

   608       finally show ?thesis .

   609     qed

   610     ultimately show ?thesis by auto

   611   qed

   612   also have "\<dots> = s" 

   613   proof -

   614     from from_to_firstn have "\<dots> = firstn j s" .

   615     also have "\<dots> = s"

   616     proof(rule firstn_ge)

   617       from le_j show "length s \<le> j" by simp

   618     qed

   619     finally show ?thesis .

   620   qed

   621   finally have "from_to 0 k s @ from_to k j s = s" .

   622   moreover have "from_to 0 k s @ restn k s = s"

   623   proof -

   624     from from_to_firstn [of k s]

   625     have "from_to 0 k s = firstn k s" .

   626     thus ?thesis by (simp add:firstn_restn_s)

   627   qed

   628   ultimately have "from_to 0 k s @ from_to k j s  = 

   629                     from_to 0 k s @ restn k s" by simp

   630   thus ?thesis by auto

   631 qed

   632 

   633 lemma down_to_moment: "down_to k 0 s = moment k s"

   634 proof -

   635   have "rev (from_to 0 k (rev s)) = rev (firstn k (rev s))" 

   636     using from_to_firstn by metis

   637   thus ?thesis by (simp add:down_to_def moment_def)

   638 qed

   639 

   640 lemma down_to_restm:

   641   assumes le_s: "length s \<le> j"

   642   shows "down_to j k s = restm k s"

   643 proof -

   644   have "rev (from_to k j (rev s)) = rev (restn k (rev s))" (is "?L = ?R")

   645   proof -

   646     from le_s have "length (rev s) \<le> j" by simp

   647     from from_to_restn [OF this, of k] show ?thesis by simp

   648   qed

   649   thus ?thesis by (simp add:down_to_def restm_def)

   650 qed

   651 

   652 lemma moment_split: "moment (m+i) s = down_to (m+i) i s @down_to i 0 s"

   653 proof -

   654   have "moment (m + i) s = down_to (m+i) 0 s" using down_to_moment by metis

   655   also have "\<dots> = (down_to (m+i) i s) @ (down_to i 0 s)" 

   656     by(rule down_to_conc[symmetric], auto)

   657   finally show ?thesis .

   658 qed

   659 

   660 lemma length_restn: "length (restn i s) = length s - i"

   661 proof(cases "i \<le> length s")

   662   case True

   663   from length_firstn_le [OF this] have "length (firstn i s) = i" .

   664   moreover have "length s = length (firstn i s) + length (restn i s)"

   665   proof -

   666     have "s = firstn i s @ restn i s" using firstn_restn_s by metis

   667     hence "length s = length \<dots>" by simp

   668     thus ?thesis by simp

   669   qed

   670   ultimately show ?thesis by simp

   671 next 

   672   case False

   673   hence "length s \<le> i" by simp

   674   from restn_ge [OF this] have "restn i s = []" .

   675   with False show ?thesis by simp

   676 qed

   677 

   678 lemma length_from_to_in:

   679   fixes i j s

   680   assumes le_ij: "i \<le> j"

   681   and le_j: "j \<le> length s"

   682   shows "length (from_to i j s) = j - i"

   683 proof -

   684   have "from_to 0 j s = from_to 0 i s @ from_to i j s"

   685     by (rule from_to_conc[symmetric, OF _ le_ij], simp)

   686   moreover have "length (from_to 0 j s) = j"

   687   proof -

   688     have "from_to 0 j s = firstn j s" using from_to_firstn by metis

   689     moreover have "length \<dots> = j" by (rule length_firstn_le [OF le_j])

   690     ultimately show ?thesis by simp

   691   qed

   692   moreover have "length (from_to 0 i s) = i"

   693   proof -

   694     have "from_to 0 i s = firstn i s" using from_to_firstn by metis

   695     moreover have "length \<dots> = i" 

   696     proof (rule length_firstn_le)

   697       from le_ij le_j show "i \<le> length s" by simp

   698     qed

   699     ultimately show ?thesis by simp

   700   qed

   701   ultimately show ?thesis by auto

   702 qed

   703 

   704 lemma firstn_restn_from_to: "from_to i (m + i) s = firstn m (restn i s)"

   705 proof(cases "m+i \<le> length s")

   706   case True

   707   have "restn i s = from_to i (m+i) s @ from_to (m+i) (length s) s"

   708   proof -

   709     have "restn i s = from_to i (length s) s"

   710       by(rule from_to_restn[symmetric], simp)

   711     also have "\<dots> = from_to i (m+i) s @ from_to (m+i) (length s) s"

   712       by(rule from_to_conc[symmetric, OF _ True], simp)

   713     finally show ?thesis .

   714   qed

   715   hence "firstn m (restn i s) = firstn m \<dots>" by simp

   716   moreover have "\<dots> = firstn (length (from_to i (m+i) s)) 

   717                     (from_to i (m+i) s @ from_to (m+i) (length s) s)"

   718   proof -

   719     have "length (from_to i (m+i) s) = m"

   720     proof -

   721       have "length (from_to i (m+i) s) = (m+i) - i"

   722         by(rule length_from_to_in [OF _ True], simp)

   723       thus ?thesis by simp

   724     qed

   725     thus ?thesis by simp

   726   qed

   727   ultimately show ?thesis using app_firstn_restn by metis

   728 next

   729   case False

   730   hence "length s \<le> m + i" by simp

   731   from from_to_restn [OF this]

   732   have "from_to i (m + i) s = restn i s" .

   733   moreover have "firstn m (restn i s) = restn i s" 

   734   proof(rule firstn_ge)

   735     show "length (restn i s) \<le> m"

   736     proof -

   737       have "length (restn i s) = length s - i" using length_restn by metis

   738       with False show ?thesis by simp

   739     qed

   740   qed

   741   ultimately show ?thesis by simp

   742 qed

   743 

   744 lemma down_to_moment_restm:

   745   fixes m i s

   746   shows "down_to (m + i) i s = moment m (restm i s)"

   747   by (simp add:firstn_restn_from_to down_to_def moment_def restm_def)

   748 

   749 lemma moment_plus_split:

   750   fixes m i s

   751   shows "moment (m + i) s = moment m (restm i s) @ moment i s"

   752 proof -

   753   from moment_split [of m i s]

   754   have "moment (m + i) s = down_to (m + i) i s @ down_to i 0 s" .

   755   also have "\<dots> = down_to (m+i) i s @ moment i s" using down_to_moment by simp

   756   also from down_to_moment_restm have "\<dots> = moment m (restm i s) @ moment i s"

   757     by simp

   758   finally show ?thesis .

   759 qed

   760 

   761 lemma length_restm: "length (restm i s) = length s - i"

   762 proof -

   763   have "length (rev (restn i (rev s))) = length s - i" (is "?L = ?R")

   764   proof -

   765     have "?L = length (restn i (rev s))" by simp

   766     also have "\<dots>  = length (rev s) - i" using length_restn by metis

   767     also have "\<dots> = ?R" by simp

   768     finally show ?thesis .

   769   qed

   770   thus ?thesis by (simp add:restm_def)

   771 qed

   772 

   773 lemma moment_prefix: "(moment i t @ s) = moment (i + length s) (t @ s)"

   774 proof -

   775   from moment_plus_split [of i "length s" "t@s"]

   776   have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)"

   777     by auto

   778   with app_moment_restm[of t s]

   779   have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" by simp

   780   with moment_app show ?thesis by auto

   781 qed

   782 

   783 end