theory mp4 imports Main (* + any other theories you wish to use *) begin definition is_palindrome :: "'a list \ 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 definitions, be sure to look in the HOL theories to see if they already exist. You may use anything you find in any theory in the standard library of Isabelle/HOL*} theorem palindrome: fixes list shows "is_palindrome list = (\ half_list. ((list = half_list @ rev half_list) \ (\ x. list = half_list @ (x # rev half_list))))" sorry end