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"