equal
deleted
inserted
replaced
14 |
14 |
15 codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF") |
15 codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI listF") |
16 |
16 |
17 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs" |
17 lemma pre_treeFI_listF_set[simp]: "pre_treeFI_set2 (i, xs) = listF_set xs" |
18 unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs |
18 unfolding pre_treeFI_set2_def collect_def[abs_def] prod_set_defs |
19 by (auto simp add: listF.set_map') |
19 by (auto simp add: listF.set_map) |
20 |
20 |
21 lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)" |
21 lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)" |
22 by (metis Tree_def treeFI.collapse treeFI.dtor_ctor) |
22 by (metis Tree_def treeFI.collapse treeFI.dtor_ctor) |
23 |
23 |
24 definition pair_fun (infixr "\<odot>" 50) where |
24 definition pair_fun (infixr "\<odot>" 50) where |