Isabelle exercise proof that trev (trev t) = t

Question

I'm learning Isabelle and I'm trying to solve Exercise 3.4.3 from A Proof Assistant for Higher-Order Logic book (page 42).

https://isabelle.in.tum.de/doc/tutorial.pdf

Define a function trev of type ('v, 'f) Nested.term ⇒ ('v, 'f) Nested.term that recursively reverses the order of arguments of all function symbols in a term. Prove that trev (trev t) = t.

where

datatype ('v,'f)"term" = Var 'v | App 'f "('v,'f)term list"

My definition is

primrec trev :: "('v,'f)term ⇒ ('v,'f)term"
where
"trev (Var x) = Var x" |
"trev (App f ts) = App f (rev (map trev ts))"

I can't figure out how to prove the lemma.

Here's what I've tried so far.

lemma "trev (trev t) = (t::('v,'f)term)"
  apply(induct_tac t)
   apply(simp_all)

which leads to goal

1. ⋀x2. (⋀x2a. x2a ∈ set x2 ⟹ trev (trev x2a) = x2a) ⟹ rev (map trev (rev (map trev x2))) = x2

At this point I decided to backtrack and first prove a helper lemma

lemma map_rev_map : "map f (rev (l:: 'a list)) = rev (map f l)"
  apply(induct_tac l)
   apply(simp_all)
  done

once this helper lemma is proved I can proceed with the original lemma

apply(simp add:map_rev_map)

and arrive at

1. ⋀x2. (⋀x2a. x2a ∈ set x2 ⟹ trev (trev x2a) = x2a) ⟹ map (trev ∘ trev) x2 = x2

Now I want to prove a second helper lemma

lemma map_trev_trev : "⟦∀ t. trev (trev t) = t ⟧ ⟹ map (trev ∘ trev) ts = ts"

but I'm stuck here. I know I should use

apply(unfold o_def)

which leads to

 1. ∀t. trev (trev t) = t ⟹ map (λx. trev (trev x)) ts = ts

Then something like drule spec or erule ssubst and rewrite trev (trev x) as x but it doesn't work.

Answer 1

Thank you very much for adding details to the question: you show clearly what you are trying to achieve and what is failing.

Your problem is that you are using the wrong quantifier and simp does not pick it up:

lemma ‹(⋀t::('a,'b) term. trev (trev (t)) = t) ⟹ map (λx. trev (trev (x::('a,'b) term))) ts = ts›
  by auto

I had to add the type information to make sure that t and ts get the same type.

For the sake, of giving slightly more information:

lemma "trev (trev t) = (t::('v,'f)term)"
  apply(induct_tac t)
   apply(simp_all)

produces a goal involving rev (map trev (rev (map trev x2))) = x2. To simplify this we need to swap rev and map. find_thm or the query panel, will tell you that rev_map looks very promising.

Now, we have to prove that map (trev ∘ trev) x2 = x2. The problem is that the simplifier does not rewrite trev ∘ trev, so you have to guide it with the so-called cong rule from map, yielding:

lemma "trev (trev t) = (t::('v,'f)term)"
  by (induct_tac t)
   (simp_all add: rev_map cong: map_cong)