<p>If your intention is to model lists a la Haskell (aka "lazy lists"), then you should use something like:</p>

<pre><code>domain 'a list = Nil ("[]") | Cons (lazy 'a) (lazy "'a list") (infix ":" 65)
</code></pre>

<p>(note the "lazy" annotations for <code>Cons</code>). Then you do not need the assumptions on your third equation. E.g.,</p>

<pre><code>fixrec append :: "'a list → 'a list → 'a list"
  where
    "append $ [] $ ys = ys"
  | "append $ (x : xs) $ ys = x : (append $ xs $ ys)"
</code></pre>

<p>for what you called <code>ssnoc</code> and</p>

<pre><code>fixrec reverse :: "'a list → 'a list"
  where
    "reverse $ [] = []"
  | "reverse $ (x : xs) = append $ xs $ (x : [])"
</code></pre>

<p>for reverse.</p>

<p>However, since this type of lists allows for "infinite" values, you will not be able to prove that <code>reverse $ (reverse $ xs) = xs</code> hold in general (because it doesn't). This only holds for finite lists, which can be characterized inductively. (See, e.g., <a href="https://arxiv.org/abs/1306.1340" rel="nofollow noreferrer">https://arxiv.org/abs/1306.1340</a> for a more detailed discussion.)</p>

<p>If, however, you do not want to model lazy lists (i.e., really don't want the "lazy" annotations in your datatype), then your equations might not hold without the assumptions. Now if the equations have those assumptions, they can only be applied in cases where the assumptions are satisfied. So gain, you will not be able to proof (without additional assumptions) that <code>reverse $ (reverse $ xs) = xs</code>. It might again be possible to obtain the appropriate assumptions by an inductive predicate, but I did not investigate further.</p>

<p><strong>Update:</strong> After playing a bit with strict lists in HOLCF, I have some more comments:</p>

<p>First, my guess is that the preconditions in the fixrec specifications are necessary due to the internal construction, but we are able to get rid of them afterwards.</p>

<p>I managed to prove your lemma as follows. For completeness I give the whole content of my theory file. First make sure that notation doesn't clash with existing one:</p>

<pre><code>no_notation
  List.Nil ("[]") and
  Set.member ("op :") and
  Set.member ("(_/ : _)" [51, 51] 50)
</code></pre>

<p>Then define the type of strict lists</p>

<pre><code>domain 'a list = Nil ("[]") | Cons 'a "'a list" (infixr ":" 65)
</code></pre>

<p>and the function <code>snoc</code>.</p>

<pre><code>fixrec snoc :: "'a list → 'a → 'a list"
  where
    "snoc $ [] $ y = y : []"
  | "x ≠ ⊥ ⟹ xs ≠ ⊥ ⟹ snoc $ (x:xs) $ y = x : snoc $ xs $ y"
</code></pre>

<p>Now, we obtain an unconditional variant of the second equation by:</p>

<ol>
<li>Showing that <code>snoc</code> is strict in its first argument (note the usage of <code>fixrec_simp</code>).</li>
<li>Showing that <code>snoc</code> is strict in its second argument (here induction is needed).</li>
<li>And finally, obtaining the equation by case analysis on all three variables.</li>
</ol>

<p><b></b></p>

<pre><code>lemma snoc_bot1 [simp]: "snoc $ ⊥ $ y = ⊥" by fixrec_simp
lemma snoc_bot2 [simp]: "snoc $ xs $ ⊥ = ⊥" by (induct xs) simp_all
lemma snoc_Cons [simp]: "snoc $ (x:xs) $ y = x : snoc $ xs $ y"
  by (cases "x = ⊥"; cases "xs = ⊥"; cases "y = ⊥";simp)
</code></pre>

<p>Then the function <code>reverse</code></p>

<pre><code>fixrec reverse :: "'a list → 'a list"
  where
    "reverse $ [] = []"
  | "x ≠ ⊥ ⟹ xs ≠ ⊥ ⟹ reverse $ (x : xs) = snoc $ (reverse $ xs) $ x"
</code></pre>

<p>and again an unconditional variant of its second equation:</p>

<pre><code>lemma reverse_bot [simp]: "reverse $ ⊥ = ⊥" by fixrec_simp
lemma reverse_Cons [simp]: "reverse $ (x : xs) = snoc $ (reverse $ xs) $ x"
  by (cases "x = ⊥"; cases "xs = ⊥"; simp)
</code></pre>

<p>Now the lemma about <code>reverse</code> and <code>snoc</code> you also had:</p>

<pre><code>lemma reverse_snoc [simp]: "reverse $ (snoc $ xs $ y) = y : reverse $ xs"
  by (induct xs) simp_all
</code></pre>

<p>And finally the desired lemma:</p>

<pre><code>lemma reverse_reverse [simp]:
  "reverse $ (reverse $ xs) = xs"
  by (induct xs) simp_all
</code></pre>

<p>The way I obtained this solution was by just looking into the remaining subgoals of your failed attempts, then get more failed attempts, look into the remaining subgoals, repeat, ...</p>
How to prove in HOLCF that double reversion of a list doesn't change it
<p>Here is a simple theory written on the plain HOL:</p>

<pre><code>theory ToyList
  imports Main
begin

no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
hide_type list
hide_const rev

datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65)

primrec snoc :: "'a list =&gt; 'a =&gt; 'a list" (infixr "#&gt;" 65)
  where
    "[] #&gt; y = y # []" |
    "(x # xs) #&gt; y = x # (xs #&gt; y)"

primrec rev :: "'a list =&gt; 'a list"
  where
    "rev [] = []" |
    "rev (x # xs) = (rev xs) #&gt; x"

lemma rev_snoc [simp]: "rev(xs #&gt; y) = y # (rev xs)"
  apply(induct_tac xs)
  apply(auto)
done

theorem rev_rev [simp]: "rev(rev xs) = xs"
  apply(induct_tac xs)
  apply(auto)
done

end
</code></pre>

<p><code>snoc</code> is an opposite of <code>cons</code>. It adds an item to the end of the list.</p>

<p>I want to prove a similar lemma via HOLCF. At a first stage I consider only strict lists. I declared the domain of strict lists in HOLCF. Also I declared two recursive functions:</p>

<ul>
<li><code>ssnoc</code> - appends an item to the end of a list</li>
<li><code>srev</code> - reverses a list</li>
</ul>

<p>Prefix <code>s</code> means "strict".</p>

<pre><code>theory Test
  imports HOLCF
begin

domain 'a SList = SNil | SCons "'a" "'a SList"

fixrec ssnoc :: "'a SList → 'a → 'a SList"
  where
    "ssnoc ⋅ SNil ⋅ x = SCons ⋅ x ⋅ SNil" |
    "ssnoc ⋅ ⊥ ⋅ x = ⊥" |
    "x ≠ ⊥ ∧ xs ≠ ⊥ ⟹ ssnoc ⋅ (SCons ⋅ x ⋅ xs) ⋅ y = SCons ⋅ x ⋅ (ssnoc ⋅ xs ⋅ y)"

fixrec srev :: "'a SList → 'a SList"
  where
    "srev ⋅ ⊥ = ⊥" |
    "srev ⋅ SNil = SNil" |
    "x ≠ ⊥ ∧ xs ≠ ⊥ ⟹ srev ⋅ (SCons ⋅ x ⋅ xs) = ssnoc ⋅ (srev ⋅ xs) ⋅ x"

lemma srev_singleton [simp]:
  "srev ⋅ (SCons ⋅ a ⋅ SNil) = SCons ⋅ a ⋅ SNil"
  apply(induct)
  apply(simp_all)
done

lemma srev_ssnoc [simp]:
  "srev ⋅ (ssnoc ⋅ xs ⋅ a) = SCons ⋅ a ⋅ (srev ⋅ xs)"
  apply(induct xs)
  apply(simp_all)
done

lemma srev_srev [simp]:
  "srev ⋅ (srev ⋅ xs) = xs"
  apply(induct xs)
  apply(simp_all)
done

end
</code></pre>

<p>I'm trying to prove that double reversion of the list equals to the original list (<code>srev_srev</code> lemma). I have declared two helper lemmas:</p>

<ul>
<li><code>srev_singleton</code> - reverse of the singleton list is the original singleton list</li>
<li><code>srev_ssnoc</code> - reversion of the list equals to the list starting from the last item of the original list appending reversion of the rest items of the original list</li>
</ul>

<p>But I can't prove any of the lemmas. Could you point out the errors?</p>

<p>Also why the precondition <code>"x ≠ ⊥ ∧ xs ≠ ⊥"</code> is necessary in the function definitions? And why should I declare <code>"srev ⋅ ⊥ = ⊥"</code> and <code>"ssnoc ⋅ ⊥ ⋅ x = ⊥"</code> explicitly. I guess that in HOLCF by default functions are undefined if any of the arguments is undefined.</p>