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