src/HOL/Datatype_Examples/TreeFI.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58309 a09ec6daaa19
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
blanchet@58309
     1
(*  Title:      HOL/Datatype_Examples/TreeFI.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     4
    Copyright   2012
blanchet@48975
     5
blanchet@48975
     6
Finitely branching possibly infinite trees.
blanchet@48975
     7
*)
blanchet@48975
     8
blanchet@48975
     9
header {* Finitely Branching Possibly Infinite Trees *}
blanchet@48975
    10
blanchet@48975
    11
theory TreeFI
blanchet@57207
    12
imports Main
blanchet@48975
    13
begin
blanchet@48975
    14
blanchet@57207
    15
codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI list")
blanchet@48975
    16
blanchet@48975
    17
(* Tree reverse:*)
traytel@54027
    18
primcorec trev where
traytel@54027
    19
  "lab (trev t) = lab t"
blanchet@57207
    20
| "sub (trev t) = map trev (rev (sub t))"
blanchet@48975
    21
blanchet@48975
    22
lemma treeFI_coinduct:
traytel@53470
    23
  assumes *: "phi x y"
traytel@53470
    24
  and step: "\<And>a b. phi a b \<Longrightarrow>
traytel@53470
    25
     lab a = lab b \<and>
blanchet@57207
    26
     length (sub a) = length (sub b) \<and>
blanchet@57207
    27
     (\<forall>i < length (sub a). phi (nth (sub a) i) (nth (sub b) i))"
traytel@53470
    28
  shows "x = y"
traytel@54027
    29
using * proof (coinduction arbitrary: x y)
traytel@54027
    30
  case (Eq_treeFI t1 t2)
traytel@54027
    31
  from conjunct1[OF conjunct2[OF step[OF Eq_treeFI]]] conjunct2[OF conjunct2[OF step[OF Eq_treeFI]]]
blanchet@57207
    32
  have "list_all2 phi (sub t1) (sub t2)"
blanchet@57207
    33
  proof (induction "sub t1" "sub t2" arbitrary: t1 t2 rule: list_induct2)
blanchet@57207
    34
    case (Cons x xs y ys)
blanchet@57207
    35
    note sub = Cons(3,4)[symmetric] and phi = mp[OF spec[OF Cons(5)], unfolded sub]
blanchet@57207
    36
      and IH = Cons(2)[of "Tree (lab t1) (tl (sub t1))" "Tree (lab t2) (tl (sub t2))",
traytel@53355
    37
        unfolded sub, simplified]
traytel@53355
    38
    from phi[of 0] show ?case unfolding sub by (auto intro!: IH dest: phi[simplified, OF Suc_mono])
traytel@53355
    39
  qed simp
traytel@54027
    40
  with conjunct1[OF step[OF Eq_treeFI]] show ?case by simp
blanchet@48975
    41
qed
blanchet@48975
    42
blanchet@48975
    43
lemma trev_trev: "trev (trev tr) = tr"
blanchet@57207
    44
  by (coinduction arbitrary: tr rule: treeFI_coinduct) (auto simp add: rev_map)
blanchet@48975
    45
blanchet@48975
    46
end