|
1 (* Title: HOL/BNF/Examples/Infinite_Derivation_Trees/DTree.thy |
|
2 Author: Andrei Popescu, TU Muenchen |
|
3 Copyright 2012 |
|
4 |
|
5 Derivation trees with nonterminal internal nodes and terminal leaves. |
|
6 *) |
|
7 |
|
8 header {* Trees with Nonterminal Internal Nodes and Terminal Leaves *} |
|
9 |
|
10 theory DTree |
|
11 imports Prelim |
|
12 begin |
|
13 |
|
14 hide_fact (open) Quotient_Product.prod_rel_def |
|
15 |
|
16 typedecl N |
|
17 typedecl T |
|
18 |
|
19 codata dtree = NNode (root: N) (ccont: "(T + dtree) fset") |
|
20 |
|
21 |
|
22 subsection{* The characteristic lemmas transported from fset to set *} |
|
23 |
|
24 definition "Node n as \<equiv> NNode n (the_inv fset as)" |
|
25 definition "cont \<equiv> fset o ccont" |
|
26 definition "unfold rt ct \<equiv> dtree_unfold rt (the_inv fset o ct)" |
|
27 definition "corec rt qt ct dt \<equiv> dtree_corec rt qt (the_inv fset o ct) (the_inv fset o dt)" |
|
28 |
|
29 lemma finite_cont[simp]: "finite (cont tr)" |
|
30 unfolding cont_def by auto |
|
31 |
|
32 lemma Node_root_cont[simp]: |
|
33 "Node (root tr) (cont tr) = tr" |
|
34 using dtree.collapse unfolding Node_def cont_def |
|
35 by (metis cont_def finite_cont fset_cong fset_to_fset o_def) |
|
36 |
|
37 lemma dtree_simps[simp]: |
|
38 assumes "finite as" and "finite as'" |
|
39 shows "Node n as = Node n' as' \<longleftrightarrow> n = n' \<and> as = as'" |
|
40 using assms dtree.inject unfolding Node_def |
|
41 by (metis fset_to_fset) |
|
42 |
|
43 lemma dtree_cases[elim, case_names Node Choice]: |
|
44 assumes Node: "\<And> n as. \<lbrakk>finite as; tr = Node n as\<rbrakk> \<Longrightarrow> phi" |
|
45 shows phi |
|
46 apply(cases rule: dtree.exhaust[of tr]) |
|
47 using Node unfolding Node_def |
|
48 by (metis Node Node_root_cont finite_cont) |
|
49 |
|
50 lemma dtree_sel_ctor[simp]: |
|
51 "root (Node n as) = n" |
|
52 "finite as \<Longrightarrow> cont (Node n as) = as" |
|
53 unfolding Node_def cont_def by auto |
|
54 |
|
55 lemmas root_Node = dtree_sel_ctor(1) |
|
56 lemmas cont_Node = dtree_sel_ctor(2) |
|
57 |
|
58 lemma dtree_cong: |
|
59 assumes "root tr = root tr'" and "cont tr = cont tr'" |
|
60 shows "tr = tr'" |
|
61 by (metis Node_root_cont assms) |
|
62 |
|
63 lemma set_rel_cont: |
|
64 "set_rel \<chi> (cont tr1) (cont tr2) = fset_rel \<chi> (ccont tr1) (ccont tr2)" |
|
65 unfolding cont_def comp_def fset_rel_fset .. |
|
66 |
|
67 lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]: |
|
68 assumes phi: "\<phi> tr1 tr2" and |
|
69 Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow> |
|
70 root tr1 = root tr2 \<and> set_rel (sum_rel op = \<phi>) (cont tr1) (cont tr2)" |
|
71 shows "tr1 = tr2" |
|
72 using phi apply(elim dtree.coinduct) |
|
73 apply(rule Lift[unfolded set_rel_cont]) . |
|
74 |
|
75 lemma unfold: |
|
76 "root (unfold rt ct b) = rt b" |
|
77 "finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)" |
|
78 using dtree.sel_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def |
|
79 apply - apply metis |
|
80 unfolding cont_def comp_def |
|
81 by (metis (no_types) fset_to_fset map_fset_image) |
|
82 |
|
83 lemma corec: |
|
84 "root (corec rt qt ct dt b) = rt b" |
|
85 "\<lbrakk>finite (ct b); finite (dt b)\<rbrakk> \<Longrightarrow> |
|
86 cont (corec rt qt ct dt b) = |
|
87 (if qt b then ct b else image (id \<oplus> corec rt qt ct dt) (dt b))" |
|
88 using dtree.sel_corec[of rt qt "the_inv fset \<circ> ct" "the_inv fset \<circ> dt" b] |
|
89 unfolding corec_def |
|
90 apply - |
|
91 apply simp |
|
92 unfolding cont_def comp_def id_def |
|
93 by (metis (no_types) fset_to_fset map_fset_image) |
|
94 |
|
95 end |