equal
deleted
inserted
replaced
48 apply (cases a) |
48 apply (cases a) |
49 apply (cases b) |
49 apply (cases b) |
50 apply (simp add: pre_treeFsetI_rel_def prod_rel_def fset_rel_def) |
50 apply (simp add: pre_treeFsetI_rel_def prod_rel_def fset_rel_def) |
51 done |
51 done |
52 |
52 |
53 lemmas treeFsetI_coind = mp[OF treeFsetI.rel_coinduct] |
53 lemmas treeFsetI_coind = mp[OF treeFsetI.dtor_rel_coinduct] |
54 |
54 |
55 lemma "tmap (f o g) x = tmap f (tmap g x)" |
55 lemma "tmap (f o g) x = tmap f (tmap g x)" |
56 by (intro treeFsetI_coind[where P="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"]) |
56 by (intro treeFsetI_coind[where P="%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"]) |
57 force+ |
57 force+ |
58 |
58 |