diff -r 235c7661a96b -r 8ae6f86a3477 src/HOL/BNF_Examples/TreeFI.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Examples/TreeFI.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -0,0 +1,46 @@
+(*  Title:      HOL/BNF/Examples/TreeFI.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Andrei Popescu, TU Muenchen
+    Copyright   2012
+
+Finitely branching possibly infinite trees.
+*)
+
+header {* Finitely Branching Possibly Infinite Trees *}
+
+theory TreeFI
+imports ListF
+begin
+
+codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF")
+
+(* Tree reverse:*)
+primcorec trev where
+  "lab (trev t) = lab t"
+| "sub (trev t) = mapF trev (lrev (sub t))"
+
+lemma treeFI_coinduct:
+  assumes *: "phi x y"
+  and step: "\<And>a b. phi a b \<Longrightarrow>
+     lab a = lab b \<and>
+     lengthh (sub a) = lengthh (sub b) \<and>
+     (\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))"
+  shows "x = y"
+using * proof (coinduction arbitrary: x y)
+  case (Eq_treeFI t1 t2)
+  from conjunct1[OF conjunct2[OF step[OF Eq_treeFI]]] conjunct2[OF conjunct2[OF step[OF Eq_treeFI]]]
+  have "relF phi (sub t1) (sub t2)"
+  proof (induction "sub t1" "sub t2" arbitrary: t1 t2 rule: listF_induct2)
+    case (Conss x xs y ys)
+    note sub = Conss(2,3)[symmetric] and phi = mp[OF spec[OF Conss(4)], unfolded sub]
+      and IH = Conss(1)[of "Tree (lab t1) (tlF (sub t1))" "Tree (lab t2) (tlF (sub t2))",
+        unfolded sub, simplified]
+    from phi[of 0] show ?case unfolding sub by (auto intro!: IH dest: phi[simplified, OF Suc_mono])
+  qed simp
+  with conjunct1[OF step[OF Eq_treeFI]] show ?case by simp
+qed
+
+lemma trev_trev: "trev (trev tr) = tr"
+  by (coinduction arbitrary: tr rule: treeFI_coinduct) auto
+
+end