|
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 ListF |
|
13 begin |
|
14 |
|
15 hide_const (open) Sublist.sub |
|
16 |
|
17 codata_raw treeFI: 'tree = "'a \<times> 'tree listF" |
|
18 |
|
19 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs" |
|
20 unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs |
|
21 by (auto simp add: listF.set_natural') |
|
22 |
|
23 (* selectors for trees *) |
|
24 definition "lab tr \<equiv> fst (treeFI_dtor tr)" |
|
25 definition "sub tr \<equiv> snd (treeFI_dtor tr)" |
|
26 |
|
27 lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)" |
|
28 unfolding lab_def sub_def by simp |
|
29 |
|
30 definition pair_fun (infixr "\<odot>" 50) where |
|
31 "f \<odot> g \<equiv> \<lambda>x. (f x, g x)" |
|
32 |
|
33 lemma unfold_pair_fun_lab: "lab (treeFI_dtor_unfold (f \<odot> g) t) = f t" |
|
34 unfolding lab_def pair_fun_def treeFI.dtor_unfolds pre_treeFI_map_def by simp |
|
35 |
|
36 lemma unfold_pair_fun_sub: "sub (treeFI_dtor_unfold (f \<odot> g) t) = listF_map (treeFI_dtor_unfold (f \<odot> g)) (g t)" |
|
37 unfolding sub_def pair_fun_def treeFI.dtor_unfolds pre_treeFI_map_def by simp |
|
38 |
|
39 (* Tree reverse:*) |
|
40 definition "trev \<equiv> treeFI_dtor_unfold (lab \<odot> lrev o sub)" |
|
41 |
|
42 lemma trev_simps1[simp]: "lab (trev t) = lab t" |
|
43 unfolding trev_def by (simp add: unfold_pair_fun_lab) |
|
44 |
|
45 lemma trev_simps2[simp]: "sub (trev t) = listF_map trev (lrev (sub t))" |
|
46 unfolding trev_def by (simp add: unfold_pair_fun_sub) |
|
47 |
|
48 lemma treeFI_coinduct: |
|
49 assumes *: "phi x y" |
|
50 and step: "\<And>a b. phi a b \<Longrightarrow> |
|
51 lab a = lab b \<and> |
|
52 lengthh (sub a) = lengthh (sub b) \<and> |
|
53 (\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))" |
|
54 shows "x = y" |
|
55 proof (rule mp[OF treeFI.dtor_coinduct, of phi, OF _ *]) |
|
56 fix a b :: "'a treeFI" |
|
57 let ?zs = "zipp (sub a) (sub b)" |
|
58 let ?z = "(lab a, ?zs)" |
|
59 assume "phi a b" |
|
60 with step have step': "lab a = lab b" "lengthh (sub a) = lengthh (sub b)" |
|
61 "\<forall>i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i)" by auto |
|
62 hence "pre_treeFI_map id fst ?z = treeFI_dtor a" "pre_treeFI_map id snd ?z = treeFI_dtor b" |
|
63 unfolding pre_treeFI_map_def by auto |
|
64 moreover have "\<forall>(x, y) \<in> pre_treeFI_set2 ?z. phi x y" |
|
65 proof safe |
|
66 fix z1 z2 |
|
67 assume "(z1, z2) \<in> pre_treeFI_set2 ?z" |
|
68 hence "(z1, z2) \<in> listF_set ?zs" by auto |
|
69 hence "\<exists>i < lengthh ?zs. nthh ?zs i = (z1, z2)" by auto |
|
70 with step'(2) obtain i where "i < lengthh (sub a)" |
|
71 "nthh (sub a) i = z1" "nthh (sub b) i = z2" by auto |
|
72 with step'(3) show "phi z1 z2" by auto |
|
73 qed |
|
74 ultimately show "\<exists>z. |
|
75 (pre_treeFI_map id fst z = treeFI_dtor a \<and> |
|
76 pre_treeFI_map id snd z = treeFI_dtor b) \<and> |
|
77 (\<forall>x y. (x, y) \<in> pre_treeFI_set2 z \<longrightarrow> phi x y)" by blast |
|
78 qed |
|
79 |
|
80 lemma trev_trev: "trev (trev tr) = tr" |
|
81 by (rule treeFI_coinduct[of "%a b. trev (trev b) = a"]) auto |
|
82 |
|
83 end |