title: How to prove in HOLCF that double reversion of a list doesn't change it
body: <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>