[isabelle] Question concerning HOAS



Dear Isabelle-Community!

Given the following definition of a tree:

datatype myTree =
  leaf
| bin_node "myTree" "myTree"
| inf_node "nat => myTree"


I would like to prove that trees are acyclic. But I do not even have an idea how to prove the following lemma

lemma "t n \<noteq> bin_node T (inf_node t)"


I would greatly appreciate any hints!

Best regards,
Thomas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.