src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
 changeset 55938 f20d1db5aa3c parent 55933 12ee2c407dad child 55943 5c2df04e97d1
```     1.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 14:25:55 2014 +0100
1.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 14:57:14 2014 +0100
1.3 @@ -60,17 +60,17 @@
1.4  shows "tr = tr'"
1.5  by (metis Node_root_cont assms)
1.6
1.7 -lemma set_rel_cont:
1.8 -"set_rel \<chi> (cont tr1) (cont tr2) = rel_fset \<chi> (ccont tr1) (ccont tr2)"
1.9 +lemma rel_set_cont:
1.10 +"rel_set \<chi> (cont tr1) (cont tr2) = rel_fset \<chi> (ccont tr1) (ccont tr2)"
1.11  unfolding cont_def comp_def rel_fset_fset ..
1.12
1.13  lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]:
1.14  assumes phi: "\<phi> tr1 tr2" and
1.15  Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
1.16 -                  root tr1 = root tr2 \<and> set_rel (sum_rel op = \<phi>) (cont tr1) (cont tr2)"
1.17 +                  root tr1 = root tr2 \<and> rel_set (sum_rel op = \<phi>) (cont tr1) (cont tr2)"
1.18  shows "tr1 = tr2"
1.19  using phi apply(elim dtree.coinduct)
1.20 -apply(rule Lift[unfolded set_rel_cont]) .
1.21 +apply(rule Lift[unfolded rel_set_cont]) .
1.22
1.23  lemma unfold:
1.24  "root (unfold rt ct b) = rt b"
```