theory mp5
imports Main (* + any other theories you wish to use *)
begin

definition is_palindrome :: "'a list \<Rightarrow> bool" where
"is_palindrome list = (List.rev list = list)"

text{* Problem: Prove the theorem below.  You will probably want to
prove auxiliary lemmas, and you may even find it helpful to make some
additional definitions.  (Of course, none of these are necessary.)
Before making deinitions, be sure to look in the HOL theories to see
if they already exist.

Part 1: English language proof, submitted as an ascii text file.
        Due Friday 26 February 2010

Part 2: Isabelle/HOL proof.  Due Friday 5 March 2010
You may use anything you find in any theory in:
/home/class/sp10/cs576/public_html/Isabelle/src/HOL}
on the csil-linux machine
*}

(*
You may add paths to Isabelle's search for theories by, for example

ML "add_path \"$ISABELLE_HOME/src/HOL/Number_Theory\"";

to allow Isabelle to find all the .thy files in the directory
Number_Theory.  You may add other paths this way so long as they are
in src/HOL.
*)

lemma append_rev_palindrome [simp]:
fixes half_list
shows "is_palindrome (half_list @ rev half_list)"
by (simp add: is_palindrome_def)

lemma append_cons_rev_palindrome [simp]:
fixes half_list x
shows "is_palindrome (half_list @ (x # rev half_list))"
by (simp add: is_palindrome_def)

lemma rev_tl: 
fixes list ::"'a list"
assumes A: "length list > 0"
shows "tl(butlast list) = butlast(tl list)"
proof (case_tac list)
 assume "list = []"
 with A
 show ?thesis by simp
 next fix x l
 assume "list = x # l"
 with A 
 show ?thesis by simp
qed

lemma chop:
fixes list::"'a list"
assumes A1: "length list >= Suc(Suc 0)" and A2: "is_palindrome list"
shows "is_palindrome (butlast(tl list)) \<and> (\<exists> x. list = x # (butlast(tl list)) @ [x])"
using A2
proof (unfold is_palindrome_def)
 assume A2': "rev list = list"
 show "rev (butlast (tl list)) = butlast (tl list) \<and> (\<exists>x. list = x # butlast (tl list) @ [x])"
 proof (case_tac list)
  assume "list = []"
  with A1 show ?thesis by simp
  next fix x l assume "list = x # l"
  with A1 A2' show ?thesis
  proof simp
   assume A1': "Suc 0 \<le> length l" and A2'': "rev l @ [x] = x # l"
   show "(rev (butlast l) = butlast l) \<and> (l = butlast l @ [x])"
   proof (rule_tac xs="l" in rev_cases)
    assume "l = []"
    with A1'
    show ?thesis by simp
    next fix y ys
    assume A3: "l = ys @ [y]"
    then show ?thesis
    proof simp
     have "y # (rev ys @ [x]) = (rev (ys @ [y])) @ [x]" by simp
     also have "\<dots> = rev l @ [x]" using A3 by simp
     also have "\<dots> = x # l" using A2'' by simp
     finally have A2''': "y # (rev ys @ [x]) = x # (ys @ [y])" using A3 by (simp only: A3)
     have "y = hd(y # (rev ys @ [x]))" by simp
     also have "\<dots> = hd(x # (ys @ [y]))" using A2''' by (simp only: A2''')
     finally have YeqX: "y = x" by simp
     from YeqX A2''' have "x # (rev ys @ [x]) = x # (ys @ [x])" by simp
     then have RevYseqYs: "rev ys = ys" by simp
     with YeqX
     show "rev ys = ys \<and> y = x" by simp
    qed
   qed
  qed
 qed
qed

lemma even_case [rule_format]:
fixes n
shows
"\<forall> list::'a list. ((length list = 2 * n) \<and> is_palindrome list)\<longrightarrow>
 (\<exists> half_list. (list = half_list @ rev half_list))"
proof (induct n)
 show "\<forall>list::'a list. length list = 2 * 0 \<and> is_palindrome list \<longrightarrow>
              (\<exists>half_list. list = half_list @ rev half_list)"
 by simp
 next
 fix n
 assume IndHyp: "\<forall>list::'a list. length list = 2 * n \<and> is_palindrome list \<longrightarrow>
                        (\<exists>half_list. list = half_list @ rev half_list)"
 show "\<forall>list::'a list. length list = 2 * Suc n \<and> is_palindrome list \<longrightarrow>
              (\<exists>half_list. list = half_list @ rev half_list)"
 proof clarsimp
  fix list::"'a list"
  assume Length: "length list = Suc(Suc (2 * n))"
  and is_pal: "is_palindrome list"
  from Length
  have Length1: "Suc(Suc 0) <= length list" by arith
  from Length
  have Length2: "length (butlast(tl list)) = 2 * n" by simp
  have Conj: "is_palindrome (butlast(tl list)) \<and> (\<exists> x. list = x # (butlast(tl list)) @ [x])"
  proof (rule_tac list="list" in chop)
   from Length1 show "Suc(Suc 0) <= length list" .
   next from is_pal show "is_palindrome list" .
  qed
  from Conj have is_pal1: "is_palindrome (butlast(tl list))" by simp
  from Conj have exX: "\<exists> x. list = x # (butlast(tl list)) @ [x]" by simp
  from exX obtain x where Red: "list = x # (butlast(tl list)) @ [x]" by (rule exE)
  from IndHyp
  have InnerHalfEx: "(\<exists>half_list. (butlast(tl list)) = half_list @ rev half_list)"
  proof (rule_tac x="butlast(tl list)" in allE[OF IndHyp])
   assume "length (butlast (tl list)) = (2\<Colon>nat) * n \<and> is_palindrome (butlast (tl list)) \<longrightarrow>
           (\<exists>half_list\<Colon>'a list. butlast (tl list) = half_list @ rev half_list)"
   from this
   show ?thesis
   proof (rule mp)
    from Length2 and is_pal1
    show "length (butlast (tl list)) = 2 * n \<and> is_palindrome (butlast (tl list))"
    by simp
   qed
  qed
  from InnerHalfEx obtain half_list::"'a list"
  where InnerHalf: "(butlast(tl list)) = half_list @ rev half_list" by (rule exE)
  show "\<exists>half_list. list = half_list @ rev half_list"
  proof (rule_tac x="x # half_list" in exI)
   show "list = (x # half_list) @ rev (x # half_list)"
   proof simp
    from Red have "list = x # (butlast(tl list)) @ [x]" .
    also from InnerHalf have "\<dots> = x # (half_list @ rev half_list) @ [x]"  by simp
    finally show "list = x # half_list @ rev half_list @ [x]" by simp
   qed
  qed
 qed
qed

lemma odd_case[rule_format]: 
fixes n
shows
"\<forall> list::'a list. ((length list = Suc(2 * n)) \<and> is_palindrome list)\<longrightarrow>
 (\<exists> half_list x. (list = half_list @ (x # rev half_list)))"
proof (induct n)
 show "\<forall> list::'a list. ((length list = Suc(2 * 0)) \<and> is_palindrome list)\<longrightarrow>
       (\<exists> half_list x. (list = half_list @ (x # rev half_list)))"
 proof clarsimp
  fix list::"'a list" assume L1: "length list = Suc 0"
  show "\<exists>half_list x::'a. list = half_list @ x # rev half_list"
  proof (rule_tac x="[]" in exI, simp)
   show "\<exists> x. list = [x]"
   using L1
   by (case_tac list, simp+)
  qed
 qed
 next
 fix n
 assume IndHyp: "\<forall>list::'a list. length list = Suc (2 * n) \<and> is_palindrome list \<longrightarrow>
                  (\<exists>half_list x. list = half_list @ x # rev half_list)"
  show "\<forall>list::'a list. length list = Suc (2 * Suc n) \<and> is_palindrome list \<longrightarrow>
         (\<exists>half_list x. list = half_list @ x # rev half_list)"
  proof clarsimp
  fix list::"'a list"
  assume Length: "length list = Suc(Suc(Suc (2 * n)))"
  and is_pal: "is_palindrome list"
  from Length
  have Length1: "Suc(Suc 0) <= length list" by arith
  from Length
  have Length2: "length (butlast(tl list)) = Suc(2 * n)" by simp
  have Conj: "is_palindrome (butlast(tl list)) \<and> (\<exists> x. list = x # (butlast(tl list)) @ [x])"
  proof (rule_tac list="list" in chop)
   from Length1 show "Suc(Suc 0) <= length list" .
   next from is_pal show "is_palindrome list" .
  qed
  from Conj have is_pal1: "is_palindrome (butlast(tl list))" by simp
  from Conj have exX: "\<exists> x. list = x # (butlast(tl list)) @ [x]" by simp
  from exX obtain x where Red: "list = x # (butlast(tl list)) @ [x]" by (rule exE)
  from IndHyp
  have InnerHalfEx: "(\<exists>half_list x. (butlast(tl list)) = half_list @ x # rev half_list)"
  proof (rule_tac x="butlast(tl list)" in allE[OF IndHyp])
   assume "length (butlast (tl list)) = Suc ((2\<Colon>nat) * n) \<and> is_palindrome (butlast (tl list)) \<longrightarrow>
     (\<exists>(half_list\<Colon>'a list) x\<Colon>'a. butlast (tl list) = half_list @ x # rev half_list)"
   from this
   show ?thesis
   proof (rule mp)
    from Length2 and is_pal1
    show "length (butlast (tl list)) = Suc(2 * n) \<and> is_palindrome (butlast (tl list))"
    by simp
   qed
  qed
  from InnerHalfEx obtain half_list::"'a list" and y::"'a"
  where InnerHalf: "(butlast(tl list)) = half_list @ y # rev half_list" by clarsimp
  show "\<exists>half_list x. list = half_list @ x # rev half_list"
  proof (rule_tac x="x # half_list" in exI, rule_tac x="y" in exI)
   show "list = (x # half_list) @ y # rev (x # half_list)"
   proof simp
    from Red have "list = x # (butlast(tl list)) @ [x]" .
    also from InnerHalf have "\<dots> = x # (half_list @ y # rev half_list) @ [x]"  by simp
    finally show "list = x # half_list @ y # rev half_list @ [x]" by simp
   qed
  qed
 qed
qed


theorem palindrome:
fixes list
shows "is_palindrome list = 
       (\<exists> half_list. ((list = half_list @ rev half_list) \<or>
                      (\<exists> x. list = half_list @ (x # rev half_list))))"
proof (rule iffI)
 assume is_pal: "is_palindrome list"
 show "\<exists>half_list. (list = half_list @ rev half_list) \<or>
         (\<exists>x. list = half_list @ x # rev half_list)"
 proof -
  presume "\<exists> n. (length list = (2 * n)) \<or> length list = Suc(2 * n)" 
  from this obtain n where even_odd: "(length list = (2 * n)) \<or> length list = Suc(2 * n)"
  by (rule exE)
  then
  show ?thesis
  proof (rule disjE)
   assume even: "length list = 2 * n"
   from even is_pal even_case
   obtain half_list where list_eq: "list = half_list @ rev half_list" by auto
   show ?thesis
   proof (rule_tac x="half_list" in exI)
    show "list = half_list @ rev half_list \<or> (\<exists>x. list = half_list @ x # rev half_list)"
    using list_eq by (rule disjI1)
   qed
  next assume odd: "length list = Suc (2 * n)"
   from  odd_case [OF conjI [OF odd is_pal] ]
   obtain half_list and x
   where list_eq: "list = half_list @ (x # rev half_list)"
   by clarsimp
   show "\<exists>half_list. list = half_list @ rev half_list \<or>
                    (\<exists>x. list = half_list @ x # rev half_list)"
   proof (rule_tac x="half_list" in exI)
    show "(list = half_list @ rev half_list) \<or> (\<exists>x. list = half_list @ x # rev half_list)"
    proof (rule disjI2)
     show "\<exists>x\<Colon>'a. list = half_list @ x # rev half_list"
     using list_eq by (rule_tac x="x" in exI)
    qed
   qed
  qed
 next
  show "\<exists>n\<Colon>nat. length list = (2\<Colon>nat) * n \<or> length list = Suc ((2\<Colon>nat) * n)"
  by arith
 qed
next
 assume "\<exists>half_list. list = half_list @ rev half_list \<or> (\<exists>x. list = half_list @ x # rev half_list)"
 from this obtain half_list
 where "(list = half_list @ rev half_list) \<or> (\<exists>x. list = half_list @ x # rev half_list)"
 by (rule exE)
 then
 show "is_palindrome list"
 proof (rule disjE)
  assume "list = half_list @ rev half_list"
  then show ?thesis by simp
 next
  assume "\<exists>x. list = half_list @ x # rev half_list"
  then obtain x where "list = half_list @ x # rev half_list"  by (rule exE)
  then show ?thesis by simp
 qed 
qed

end