gistfile1.txt

lemma strip_while_snoc:
  "strip_while P (xs @ [x]) = (if P x then strip_while P xs else xs @ [x])"
proof -
  have "strip_while P (xs @ [x]) = rev (List.dropWhile P (rev (xs @ [x])))" by (simp only: strip_while_def)
  also have "... =rev (dropWhile P (rev [x] @ rev xs))" by (simp only: List.rev_append)
  also have "... = rev (dropWhile P ((rev [] @ [x]) @ rev xs))" by (simp only: rev.simps(2))
  also have "... = rev (dropWhile P (([] @ [x]) @ rev xs))" by (simp only: rev.simps(1))
  also have "... = rev (dropWhile P ([x] @ rev xs))" by (simp only: List.append.append_Nil)
  also have "... = rev (dropWhile P (x # [] @ rev xs))" by (simp only: List.append.append_Cons)
  also have "... = rev (dropWhile P (x # rev xs))" by (simp only: List.append.append_Nil)
  also have "... = rev (if P x then dropWhile P (rev xs) else x # rev xs)" by (simp only: List.dropWhile.simps(2))
  also have "... = (if P x then rev (dropWhile P (rev xs)) else rev (x # rev xs))" by (simp only: if_distrib)
  
Failed to finish proof⌂:
goal (1 subgoal):
 1. if P x then (if P x then (=) (rev (dropWhile P (rev xs))) else (=) (rev (x # rev xs))) (rev (dropWhile P (rev xs)))
    else (if P x then (=) (rev (dropWhile P (rev xs))) else (=) (rev (x # rev xs))) (rev (x # rev xs))