1 (* Title: HOL/BNF/Examples/TreeFsetI.thy |
|
2 Author: Dmitriy Traytel, TU Muenchen |
|
3 Author: Andrei Popescu, TU Muenchen |
|
4 Copyright 2012 |
|
5 |
|
6 Finitely branching possibly infinite trees, with sets of children. |
|
7 *) |
|
8 |
|
9 header {* Finitely Branching Possibly Infinite Trees, with Sets of Children *} |
|
10 |
|
11 theory TreeFsetI |
|
12 imports "../BNF" |
|
13 begin |
|
14 |
|
15 hide_const (open) Sublist.sub |
|
16 hide_fact (open) Quotient_Product.prod_rel_def |
|
17 |
|
18 definition pair_fun (infixr "\<odot>" 50) where |
|
19 "f \<odot> g \<equiv> \<lambda>x. (f x, g x)" |
|
20 |
|
21 codata_raw treeFsetI: 't = "'a \<times> 't fset" |
|
22 |
|
23 (* selectors for trees *) |
|
24 definition "lab t \<equiv> fst (treeFsetI_dtor t)" |
|
25 definition "sub t \<equiv> snd (treeFsetI_dtor t)" |
|
26 |
|
27 lemma dtor[simp]: "treeFsetI_dtor t = (lab t, sub t)" |
|
28 unfolding lab_def sub_def by simp |
|
29 |
|
30 lemma unfold_pair_fun_lab: "lab (treeFsetI_dtor_unfold (f \<odot> g) t) = f t" |
|
31 unfolding lab_def pair_fun_def treeFsetI.dtor_unfolds pre_treeFsetI_map_def by simp |
|
32 |
|
33 lemma unfold_pair_fun_sub: "sub (treeFsetI_dtor_unfold (f \<odot> g) t) = map_fset (treeFsetI_dtor_unfold (f \<odot> g)) (g t)" |
|
34 unfolding sub_def pair_fun_def treeFsetI.dtor_unfolds pre_treeFsetI_map_def by simp |
|
35 |
|
36 (* tree map (contrived example): *) |
|
37 definition "tmap f \<equiv> treeFsetI_dtor_unfold (f o lab \<odot> sub)" |
|
38 |
|
39 lemma tmap_simps1[simp]: "lab (tmap f t) = f (lab t)" |
|
40 unfolding tmap_def by (simp add: unfold_pair_fun_lab) |
|
41 |
|
42 lemma trev_simps2[simp]: "sub (tmap f t) = map_fset (tmap f) (sub t)" |
|
43 unfolding tmap_def by (simp add: unfold_pair_fun_sub) |
|
44 |
|
45 lemma pre_treeFsetI_rel[simp]: "pre_treeFsetI_rel R1 R2 a b = (R1 (fst a) (fst b) \<and> |
|
46 (\<forall>t \<in> fset (snd a). (\<exists>u \<in> fset (snd b). R2 t u)) \<and> |
|
47 (\<forall>t \<in> fset (snd b). (\<exists>u \<in> fset (snd a). R2 u t)))" |
|
48 apply (cases a) |
|
49 apply (cases b) |
|
50 apply (simp add: pre_treeFsetI_rel_def prod_rel_def fset_rel_def) |
|
51 done |
|
52 |
|
53 lemmas treeFsetI_coind = mp[OF treeFsetI.rel_coinduct] |
|
54 |
|
55 lemma "tmap (f o g) x = tmap f (tmap g x)" |
|
56 by (intro treeFsetI_coind[where P="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"]) |
|
57 force+ |
|
58 |
|
59 end |
|