equal
deleted
inserted
replaced
65 unfolding cont_def comp_def rel_fset_fset .. |
65 unfolding cont_def comp_def rel_fset_fset .. |
66 |
66 |
67 lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]: |
67 lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]: |
68 assumes phi: "\<phi> tr1 tr2" and |
68 assumes phi: "\<phi> tr1 tr2" and |
69 Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow> |
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)" |
70 root tr1 = root tr2 \<and> rel_set (rel_sum (=) \<phi>) (cont tr1) (cont tr2)" |
71 shows "tr1 = tr2" |
71 shows "tr1 = tr2" |
72 using phi apply(elim dtree.coinduct) |
72 using phi apply(elim dtree.coinduct) |
73 apply(rule Lift[unfolded rel_set_cont]) . |
73 apply(rule Lift[unfolded rel_set_cont]) . |
74 |
74 |
75 lemma unfold: |
75 lemma unfold: |