subsequence

subseq.thy

theory subseq imports "~~/src/HOL/Hoare/Hoare_Logic" begin

definition is_subseq :: "'a list => 'a list => bool" where
  "is_subseq xs ys ==
    (\<exists>c.
      (\<forall>i. i + 1 < length ys --> c i < c (i + 1))
    \<and> (length ys > 0 \<longrightarrow> c (length ys - 1) < length xs)
    \<and> (\<forall>i. i < length ys \<longrightarrow> ys ! i = xs ! (c i)))"

fun is_subseq2 :: "'a list => 'a list => bool" where
  "is_subseq2 xs [] = True"
| "is_subseq2 [] (y#ys) = False"
| "is_subseq2 (x#xs) (y#ys) =
     (if x=y then is_subseq2 xs ys else is_subseq2 xs (y#ys))"

lemma "ALL xs. is_subseq xs ys --> is_subseq2 xs ys"
apply(induct_tac ys)
apply(auto)
(*
goal (1 subgoal):
 1. !!a list xs.
       [| ALL xs. is_subseq xs list --> is_subseq2 xs list;
          is_subseq xs (a # list) |]
       ==> is_subseq2 xs (a # list)
*)
oops

lemma
  "ALL list.
  (ALL xs. is_subseq xs list --> is_subseq2 xs list) -->
  is_subseq xs (a # list) -->
  is_subseq2 xs (a # list)"
apply(induct_tac xs)
apply(auto)
(*
 1. !!list.
       [| ALL xs. is_subseq xs list --> is_subseq2 xs list;
          is_subseq [] (a # list) |]
       ==> False
*)
oops

lemma x1 [dest]: "is_subseq [] (a # list) ==> False"
apply(unfold is_subseq_def)
apply(auto)
done

lemma
  "ALL list.
  (ALL xs. is_subseq xs list --> is_subseq2 xs list) -->
  is_subseq xs (a # list) -->
  is_subseq2 xs (a # list)"
apply(induct_tac xs)
apply(auto)
(*
goal (2 subgoals):
 1. !!list lista.
       [| ALL lista.
             (ALL xs.
                 is_subseq xs lista -->
                 is_subseq2 xs lista) -->
             is_subseq list (a # lista) -->
             is_subseq2 list (a # lista);
          ALL xs. is_subseq xs lista --> is_subseq2 xs lista;
          is_subseq (a # list) (a # lista) |]
       ==> is_subseq2 list lista
*)
oops

lemma x2 [dest]:
  "is_subseq (a # lista) (a # list) ==> is_subseq lista list"
apply(unfold is_subseq_def)
apply(auto)
(*
goal (1 subgoal):
 1. !!c. [| ALL i<length list. c i < c (Suc i);
            c (length list) < Suc (length lista);
            ALL i<Suc (length list).
               (a # list) ! i = (a # lista) ! c i |]
         ==> EX c. (ALL i.
                       Suc i < length list -->
                       c i < c (Suc i)) &
                   (list ~= [] -->
                    c (length list - Suc 0) < length lista) &
                   (ALL i<length list.
                       list ! i = lista ! c i)
*)
apply(rule_tac x="%i. (c (i + 1)) - 1" in exI)
apply(auto)
apply (metis Suc_lessD diff_less_mono gr_implies_not0 less_Suc0 not_less)
apply (metis (erased, hide_lams) Suc_lessD Suc_pred diff_Suc_less gr_implies_not0 length_0_conv less_antisym not_gr0)
by (metis One_nat_def Suc_less_eq not_less0 nth_Cons' nth_Cons_Suc)

lemma
  "ALL list.
  (ALL xs. is_subseq xs list --> is_subseq2 xs list) -->
  is_subseq xs (a # list) -->
  is_subseq2 xs (a # list)"
apply(induct_tac xs)
apply(auto)
(*
goal (1 subgoal):
 1. !!aa list lista.
       [| ALL lista.
             (ALL xs.
                 is_subseq xs lista -->
                 is_subseq2 xs lista) -->
             is_subseq list (a # lista) -->
             is_subseq2 list (a # lista);
          aa ~= a;
          ALL xs. is_subseq xs lista --> is_subseq2 xs lista;
          is_subseq (aa # list) (a # lista) |]
       ==> is_subseq2 list (a # lista)
*)
oops

lemma x3:
  "is_subseq (x#xs) (y#ys) ==>
   x ~= y ==>
   is_subseq xs (y#ys)"
apply(unfold is_subseq_def)
apply(auto)
(*
goal (1 subgoal):
 1. !!c. [| x ~= y; ALL i<length ys. c i < c (Suc i);
            c (length ys) < Suc (length xs);
            ALL i<Suc (length ys).
               (y # ys) ! i = (x # xs) ! c i |]
         ==> EX ca.
                (ALL i<length ys. ca i < ca (Suc i)) &
                ca (length ys) < length xs &
                (ALL i<Suc (length ys).
                    (x # xs) ! c i = xs ! ca i)
*)
apply(rule_tac x="%i. (c i) - 1" in exI)
apply(auto)
apply (metis Suc_lessD diff_less_mono less_Suc_eq_0_disj not_less not_less0 nth_Cons' old.nat.exhaust)
apply (metis Suc_pred diff_Suc_less length_greater_0_conv less_antisym less_imp_diff_less list.size(3) not_less0 nth_Cons')
by (metis One_nat_def less_Suc_eq_0_disj not_less0 nth_Cons')

lemma x0 [rule_format]:
  "ALL list.
  (ALL xs. is_subseq xs list --> is_subseq2 xs list) -->
  is_subseq xs (a # list) -->
  is_subseq2 xs (a # list)"
apply(induct_tac xs)
apply(auto)
apply(case_tac list)
apply(auto)
apply(drule x3)
apply(assumption)
apply(clarsimp)
apply(rotate_tac -2)
apply(drule_tac x="listb" in spec)
apply(rotate_tac -1)
apply(drule mp)
apply(drule x3)
apply(assumption)
apply(drule x2)
apply(assumption)
apply(assumption)

apply(drule_tac x="lista" in spec)
apply(drule mp)
apply(assumption)
apply(drule mp)
apply(drule x3)
apply(assumption)
apply(assumption)
apply(assumption)
done

lemma subseq1 [rule_format]:
  "ALL xs. is_subseq xs ys --> is_subseq2 xs ys"
apply(induct_tac ys)
apply(auto)
apply(rule x0)
apply metis
apply(assumption)
done

lemma "ALL xs. is_subseq2 xs ys --> is_subseq xs ys"
apply(induct_tac ys)
apply(auto)
(*
goal (2 subgoals):
 1. !!xs. is_subseq xs []
*)
oops

lemma x4 [simp]: "is_subseq xs []"
apply(unfold is_subseq_def)
apply(auto)
done

lemma "ALL xs. is_subseq2 xs ys --> is_subseq xs ys"
apply(induct_tac ys)
apply(auto)
(*
goal (1 subgoal):
 1. !!a list xs.
       [| ALL xs. is_subseq2 xs list --> is_subseq xs list;
          is_subseq2 xs (a # list) |]
       ==> is_subseq xs (a # list)
*)
oops

lemma
  "ALL list.
  (ALL xs. is_subseq2 xs list --> is_subseq xs list) -->
  is_subseq2 xs (a # list) -->
  is_subseq xs (a # list)"
apply(induct_tac xs)
apply(auto)
(*
goal (2 subgoals):
 1. !!list lista.
       [| ALL lista.
             (ALL xs.
                 is_subseq2 xs lista -->
                 is_subseq xs lista) -->
             is_subseq2 list (a # lista) -->
             is_subseq list (a # lista);
          ALL xs. is_subseq2 xs lista --> is_subseq xs lista;
          is_subseq2 list lista |]
       ==> is_subseq (a # list) (a # lista)
*)
oops

lemma
  "is_subseq lista list ==> is_subseq (a # lista) (a # list)"
apply(unfold is_subseq_def)
apply(auto)
(*
goal (1 subgoal):
 1. !!c. [| ALL i. Suc i < length list --> c i < c (Suc i);
            ALL i<length list. list ! i = lista ! c i;
            c (length list - Suc 0) < length lista |]
         ==> EX c. (ALL i<length list. c i < c (Suc i)) &
                   c (length list) < Suc (length lista) &
                   (ALL i<Suc (length list).
                       (a # list) ! i = (a # lista) ! c i)
*)
apply(rule_tac x="%i. (c (i - 1)) + 1" in exI)
apply(auto)
(*
goal (2 subgoals):
 1. !!c i.
       [| ALL i. Suc i < length list --> c i < c (Suc i);
          ALL i<length list. list ! i = lista ! c i;
          c (length list - Suc 0) < length lista;
          i < length list |]
       ==> c (i - Suc 0) < c i
*)
oops

lemma x5:
  "is_subseq lista list ==> is_subseq (a # lista) (a # list)"
apply(unfold is_subseq_def)
apply(auto)
(*
goal (1 subgoal):
 1. !!c. [| ALL i. Suc i < length list --> c i < c (Suc i);
            ALL i<length list. list ! i = lista ! c i;
            c (length list - Suc 0) < length lista |]
         ==> EX c. (ALL i<length list. c i < c (Suc i)) &
                   c (length list) < Suc (length lista) &
                   (ALL i<Suc (length list).
                       (a # list) ! i = (a # lista) ! c i)
*)
apply(rule_tac x="%i. (if i=0 then 0 else (c (i - 1)) + 1)" in exI)
apply(auto)
by (metis Suc_pred)

lemma
  "ALL list.
  (ALL xs. is_subseq2 xs list --> is_subseq xs list) -->
  is_subseq2 xs (a # list) -->
  is_subseq xs (a # list)"
apply(induct_tac xs)
apply(auto)
apply(rule x5)
apply metis
(*
goal (1 subgoal):
 1. !!aa list lista.
       [| ALL lista.
             (ALL xs.
                 is_subseq2 xs lista -->
                 is_subseq xs lista) -->
             is_subseq2 list (a # lista) -->
             is_subseq list (a # lista);
          aa ~= a;
          ALL xs. is_subseq2 xs lista --> is_subseq xs lista;
          is_subseq2 list (a # lista) |]
       ==> is_subseq (aa # list) (a # lista)
*)
oops

lemma x7:
  "is_subseq list (a # lista) ==>
  aa ~= a ==>
  is_subseq (aa # list) (a # lista)"
apply(unfold is_subseq_def)
apply(auto)
(*
goal (1 subgoal):
 1. !!c. [| aa ~= a; ALL i<length lista. c i < c (Suc i);
            c (length lista) < length list;
            ALL i<Suc (length lista).
               (a # lista) ! i = list ! c i |]
         ==> EX ca.
                (ALL i<length lista. ca i < ca (Suc i)) &
                ca (length lista) < Suc (length list) &
                (ALL i<Suc (length lista).
                    list ! c i = (aa # list) ! ca i)
*)
apply(rule_tac x="%i. (c i) + 1" in exI)
apply(auto)
done

lemma x6:
  "ALL list.
  (ALL xs. is_subseq2 xs list --> is_subseq xs list) -->
  is_subseq2 xs (a # list) -->
  is_subseq xs (a # list)"
apply(induct_tac xs)
apply(auto)
apply(rule x5)
apply metis

apply(drule_tac x="lista" in spec)
apply(drule mp)
apply(assumption)
apply(drule mp)
apply(assumption)
apply(erule x7)
apply(assumption)
done

lemma subseq2 [rule_format]:
  "ALL xs. is_subseq2 xs ys --> is_subseq xs ys"
apply(induct_tac ys)
apply(auto)
apply(rule x6[rule_format])
apply(auto)
done

theorem subseq:
  "is_subseq2 xs ys = is_subseq xs ys"
by (metis subseq1 subseq2)

(************************************************)

lemma
  "VARS i j
  {True}
  i := 0;
  j := 0;
  WHILE i < length xs & j < length ys
  INV {
  i <= length xs & j <= length ys
  & is_subseq2 (take i xs) (take j ys)
  }
  DO
    IF xs!i = ys!j THEN
      i := i + 1; j := j + 1
    ELSE
      i := i + 1
    FI
  OD
  {(j = length ys) = is_subseq2 xs ys}"

apply(vcg)
apply(auto)
(*
goal (4 subgoals):
 1. !!i j.
       [| is_subseq2 (take i xs) (take j ys); i < length xs;
          j < length ys; xs ! i = ys ! j |]
       ==> is_subseq2 (take (Suc i) xs) (take (Suc j) ys)
*)
oops

lemma take_0 [rule_format]:
  "ALL n. n < length xs --> take (Suc n) xs = take n xs @ [xs!n]"
apply(induct_tac xs)
apply(auto)
by (metis length_Cons take_Suc_Cons take_Suc_conv_app_nth)

lemma
  "VARS i j
  {True}
  i := 0;
  j := 0;
  WHILE i < length xs & j < length ys
  INV {
  i <= length xs & j <= length ys
  & is_subseq2 (take i xs) (take j ys)
  }
  DO
    IF xs!i = ys!j THEN
      i := i + 1; j := j + 1
    ELSE
      i := i + 1
    FI
  OD
  {(j = length ys) = is_subseq2 xs ys}"

apply(vcg)
apply(auto)
apply(subst take_0)
apply(assumption)
apply(subst take_0)
apply(assumption)
(*
goal (4 subgoals):
 1. !!i j.
       [| is_subseq2 (take i xs) (take j ys); i < length xs;
          j < length ys; xs ! i = ys ! j |]
       ==> is_subseq2 (take i xs @ [xs ! i])
            (take j ys @ [ys ! j])
*)
oops

lemma
  "ALL ys us vs.
  is_subseq2 xs ys -->
  is_subseq2 us vs -->
  is_subseq2 (xs @ us) (ys @ vs)"
apply(induct_tac xs)
apply(auto)
(*
goal (2 subgoals):
 1. !!ys us vs.
       [| is_subseq2 [] ys; is_subseq2 us vs |]
       ==> is_subseq2 us (ys @ vs)
*)
apply(case_tac ys)
apply(auto)
(*
goal (1 subgoal):
 1. !!a list ys us vs.
       [| ALL ys.
             is_subseq2 list ys -->
             (ALL us vs.
                 is_subseq2 us vs -->
                 is_subseq2 (list @ us) (ys @ vs));
          is_subseq2 (a # list) ys; is_subseq2 us vs |]
       ==> is_subseq2 (a # list @ us) (ys @ vs)
*)
oops

lemma
  "ALL list us vs.
  (ALL ys.
    is_subseq2 list ys -->
    (ALL us vs.
      is_subseq2 us vs -->
      is_subseq2 (list @ us) (ys @ vs))) -->
      is_subseq2 (a # list) ys -->
      is_subseq2 us vs -->
      is_subseq2 (a # list @ us) (ys @ vs)"
apply(induct_tac ys)
apply(auto)
(*
goal (1 subgoal):
 1. !!list us vs.
       [| ALL ys.
             is_subseq2 list ys -->
             (ALL us vs.
                 is_subseq2 us vs -->
                 is_subseq2 (list @ us) (ys @ vs));
          is_subseq2 us vs |]
       ==> is_subseq2 (a # list @ us) vs
*)
oops

lemma
  "ALL xs ys. is_subseq2 xs ys --> is_subseq2 (zs @ xs) ys"
apply(induct_tac zs)
apply(auto)
apply(drule_tac x="xs" in spec)
apply(drule_tac x="ys" in spec)
apply(drule mp)
apply(assumption)
(*
goal (1 subgoal):
 1. !!a list xs ys.
       [| is_subseq2 xs ys; is_subseq2 (list @ xs) ys |]
       ==> is_subseq2 (a # list @ xs) ys
*)
oops

lemma
  "ALL x ys. is_subseq2 xs ys --> is_subseq2 (x#xs) ys"
apply(induct_tac xs)
apply(auto)
apply(case_tac ys)
apply(auto)
(*
2nd induction is needed
goal (1 subgoal):
 1. !!a list x ys.
       [| ALL x ys.
             is_subseq2 list ys --> is_subseq2 (x # list) ys;
          is_subseq2 (a # list) ys |]
       ==> is_subseq2 (x # a # list) ys
*)
oops

lemma x12 [rule_format]:
  "ALL list a x.
  (ALL x ys.
    is_subseq2 list ys --> is_subseq2 (x # list) ys) -->
    is_subseq2 (a # list) ys -->
    is_subseq2 (x # a # list) ys"
apply(induct_tac ys)
apply(auto)
by (metis is_subseq2.simps(3))

lemma x11 [rule_format]:
  "ALL x ys. is_subseq2 xs ys --> is_subseq2 (x#xs) ys"
apply(induct_tac xs)
apply(auto)
apply(case_tac ys)
apply(auto)
apply(rule x12)
apply(auto)
done

lemma x10 [rule_format]:
  "ALL xs ys. is_subseq2 xs ys --> is_subseq2 (zs @ xs) ys"
apply(induct_tac zs)
apply(auto)
apply(drule_tac x="xs" in spec)
apply(drule_tac x="ys" in spec)
apply(drule mp)
apply(assumption)
apply(rule x11)
apply(assumption)
done

lemma x9 [rule_format]:
  "ALL list us vs.
  (ALL ys.
    is_subseq2 list ys -->
    (ALL us vs.
      is_subseq2 us vs -->
      is_subseq2 (list @ us) (ys @ vs))) -->
      is_subseq2 (a # list) ys -->
      is_subseq2 us vs -->
      is_subseq2 (a # list @ us) (ys @ vs)"
apply(induct_tac ys)
apply(auto)
apply(drule_tac zs="a#list" in x10)
apply(auto)
done

lemma subseq_app [rule_format]:
  "ALL ys us vs.
  is_subseq2 xs ys -->
  is_subseq2 us vs -->
  is_subseq2 (xs @ us) (ys @ vs)"
apply(induct_tac xs)
apply(auto)
apply(case_tac ys)
apply(auto)
apply(rule x9)
apply(auto)
done

lemma
  "VARS i j
  {True}
  i := 0;
  j := 0;
  WHILE i < length xs & j < length ys
  INV {
  i <= length xs & j <= length ys
  & is_subseq2 (take i xs) (take j ys)
  }
  DO
    IF xs!i = ys!j THEN
      i := i + 1; j := j + 1
    ELSE
      i := i + 1
    FI
  OD
  {(j = length ys) = is_subseq2 xs ys}"

apply(vcg)
apply(auto)
apply(subst take_0)
apply(assumption)
apply(subst take_0)
apply(assumption)
apply(rule subseq_app)
apply(auto)
apply(subst take_0)
apply(auto)
apply (metis append_Nil2 is_subseq_def list.size(3) not_less0 subseq1 subseq_app)
(*
goal (2 subgoals):
 1. !!j. [| j <= length ys; is_subseq2 xs (take j ys);
            is_subseq2 xs ys |]
         ==> j = length ys
 2. !!i. [| i <= length xs; is_subseq2 (take i xs) ys |]
         ==> is_subseq2 xs ys
*)
oops

lemma
  "ALL zs ys. is_subseq2 xs ys --> is_subseq2 (xs @ zs) ys"
apply(induct_tac xs)
apply(auto)
apply(case_tac ys)
apply(auto)
(* 2nd induction
goal (1 subgoal):
 1. !!a list zs ys.
       [| ALL zs ys.
             is_subseq2 list ys -->
             is_subseq2 (list @ zs) ys;
          is_subseq2 (a # list) ys |]
       ==> is_subseq2 (a # list @ zs) ys
*)
oops

lemma x14 [rule_format]:
  "ALL list a ys.
  (ALL zs ys.
    is_subseq2 list ys --> is_subseq2 (list @ zs) ys) -->
    is_subseq2 (a # list) ys -->
    is_subseq2 (a # list @ zs) ys"
apply(induct_tac zs)
apply(auto)
by (metis append_Cons append_Nil2 is_subseq2.simps(1) subseq_app)

lemma x13 [rule_format]:
  "ALL zs ys. is_subseq2 xs ys --> is_subseq2 (xs @ zs) ys"
apply(induct_tac xs)
apply(auto)
apply(case_tac ys)
apply(auto)
apply(rule x14)
apply(auto)
done

lemma
  "VARS i j
  {True}
  i := 0;
  j := 0;
  WHILE i < length xs & j < length ys
  INV {
  i <= length xs & j <= length ys
  & is_subseq2 (take i xs) (take j ys)
  }
  DO
    IF xs!i = ys!j THEN
      i := i + 1; j := j + 1
    ELSE
      i := i + 1
    FI
  OD
  {(j = length ys) = is_subseq2 xs ys}"

apply(vcg)
apply(auto)
apply(subst take_0)
apply(assumption)
apply(subst take_0)
apply(assumption)
apply(rule subseq_app)
apply(auto)
apply(subst take_0)
apply(auto)
apply (metis append_Nil2 is_subseq_def list.size(3) not_less0 subseq1 subseq_app)
defer
apply (metis append_take_drop_id x13)
oops

lemma
  "VARS i j
  {True}
  i := 0;
  j := 0;
  WHILE i < length xs & j < length ys
  INV {
  i <= length xs & j <= length ys
  & is_subseq2 (take i xs) (take j ys)
  & (is_subseq2 xs ys --> is_subseq2 (drop i xs) (drop j ys))
  }
  DO
    IF xs!i = ys!j THEN
      i := i + 1; j := j + 1
    ELSE
      i := i + 1
    FI
  OD
  {(j = length ys) = is_subseq2 xs ys}"

apply(vcg)
apply(auto)
apply(subst take_0)
apply(assumption)
apply(subst take_0)
apply(assumption)
apply(rule subseq_app)
apply(auto)
apply(subst take_0)
apply(auto)
apply (metis append_Nil2 is_subseq_def list.size(3) not_less0 subseq1 subseq_app)
apply(subst take_0)
apply(assumption)
apply(subst take_0)
apply(assumption)
apply(rule subseq_app)
apply(auto)
  apply (metis Cons_nth_drop_Suc is_subseq2.simps(3))
  apply (metis take_hd_drop x13)
  apply (metis Cons_nth_drop_Suc is_subseq2.simps(3))
  apply (metis append_take_drop_id x13)
  apply (meson antisym_conv drop_eq_Nil is_subseq2.elims(2) list.distinct(1))
  by (metis append_take_drop_id x13)