src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
 author blanchet Mon Aug 18 17:19:58 2014 +0200 (2014-08-18) changeset 57983 6edc3529bb4e parent 55943 5c2df04e97d1 child 57991 f50b3726266f permissions -rw-r--r--
reordered some (co)datatype property names for more consistency
```     1 (*  Title:      HOL/BNF_Examples/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 typedecl N
```
```    15 typedecl T
```
```    16
```
```    17 codatatype dtree = NNode (root: N) (ccont: "(T + dtree) fset")
```
```    18
```
```    19 subsection{* Transporting the Characteristic Lemmas from @{text "fset"} to @{text "set"} *}
```
```    20
```
```    21 definition "Node n as \<equiv> NNode n (the_inv fset as)"
```
```    22 definition "cont \<equiv> fset o ccont"
```
```    23 definition "unfold rt ct \<equiv> corec_dtree rt (the_inv fset o image (map_sum id Inr) o ct)"
```
```    24 definition "corec rt ct \<equiv> corec_dtree rt (the_inv fset o ct)"
```
```    25
```
```    26 lemma finite_cont[simp]: "finite (cont tr)"
```
```    27   unfolding cont_def comp_apply by (cases tr, clarsimp)
```
```    28
```
```    29 lemma Node_root_cont[simp]:
```
```    30   "Node (root tr) (cont tr) = tr"
```
```    31   unfolding Node_def cont_def comp_apply
```
```    32   apply (rule trans[OF _ dtree.collapse])
```
```    33   apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]])
```
```    34   apply (simp_all add: fset_inject)
```
```    35   done
```
```    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 rel_set_cont:
```
```    64 "rel_set \<chi> (cont tr1) (cont tr2) = rel_fset \<chi> (ccont tr1) (ccont tr2)"
```
```    65 unfolding cont_def comp_def rel_fset_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> rel_set (rel_sum op = \<phi>) (cont tr1) (cont tr2)"
```
```    71 shows "tr1 = tr2"
```
```    72 using phi apply(elim dtree.coinduct)
```
```    73 apply(rule Lift[unfolded rel_set_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.corec_sel[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def
```
```    79 apply blast
```
```    80 unfolding cont_def comp_def
```
```    81 by (simp add: case_sum_o_inj map_sum.compositionality image_image)
```
```    82
```
```    83 lemma corec:
```
```    84 "root (corec rt ct b) = rt b"
```
```    85 "finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
```
```    86 using dtree.corec_sel[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
```
```    87 unfolding cont_def comp_def id_def
```
```    88 by simp_all
```
```    89
```
```    90 end
```