Theory AuxLemmas

section ‹Auxiliary lemmas›

theory AuxLemmas imports Main begin

text ‹Lemma concerning maps and @›

lemma map_append_append_maps:
  assumes map:"map f xs = ys@zs"
  obtains xs' xs'' where "map f xs' = ys" and "map f xs'' = zs" and "xs=xs'@xs''"
by (metis append_eq_conv_conj append_take_drop_id assms drop_map take_map that)

text ‹Lemma concerning splitting of @{term list}s›

lemma  path_split_general:
assumes all:"zs. xs  ys@zs"
obtains j zs where "xs = (take j ys)@zs" and "j < length ys"
  and "k > j. zs'. xs  (take k ys)@zs'"
  from zs. xs  ys@zs
  show "j zs. xs = take j ys @ zs  j < length ys  
               (k>j. zs'. xs  take k ys @ zs')"
  proof(induct ys arbitrary:xs)
    case Nil thus ?case by auto
    case (Cons y' ys')
    note IH = xs. zs. xs  ys' @ zs 
      j zs. xs = take j ys' @ zs  j < length ys'  
      (k. j < k  (zs'. xs  take k ys' @ zs'))
    show ?case
    proof(cases xs)
      case Nil thus ?thesis by simp
      case (Cons x' xs')
      with zs. xs  (y' # ys') @ zs have "x'  y'  (zs. xs'  ys' @ zs)"
        by simp
      show ?thesis
      proof(cases "x' = y'")
        case True
        with x'  y'  (zs. xs'  ys' @ zs) have "zs. xs'  ys' @ zs" by simp
        from IH[OF this] have "j zs. xs' = take j ys' @ zs  j < length ys' 
          (k. j < k  (zs'. xs'  take k ys' @ zs'))" .
        then obtain j zs where "xs' = take j ys' @ zs"
          and "j < length ys'"
          and all_sub:"k. j < k  (zs'. xs'  take k ys' @ zs')"
          by blast
        from xs' = take j ys' @ zs True
          have "(x'#xs') = take (Suc j) (y' # ys') @ zs"
          by simp
        from all_sub True have all_imp:"k. j < k  
          (zs'. (x'#xs')  take (Suc k) (y' # ys') @ zs')"
          by auto
        { fix l assume "(Suc j) < l"
          then obtain k where [simp]:"l = Suc k" by(cases l) auto
          with (Suc j) < l have "j < k" by simp
          with all_imp 
          have "zs'. (x'#xs')  take (Suc k) (y' # ys') @ zs'"
            by simp
          hence "zs'. (x'#xs')  take l (y' # ys') @ zs'"
            by simp }
        with (x'#xs') = take (Suc j) (y' # ys') @ zs j < length ys' Cons
        show ?thesis by (metis Suc_length_conv less_Suc_eq_0_disj)
        case False
        with Cons have "i zs'. i > 0  xs  take i (y' # ys') @ zs'"
          by auto(case_tac i,auto)
        have "zs. xs = take 0 (y' # ys') @ zs" by simp
        ultimately show ?thesis by(rule_tac x="0" in exI,auto)