equal
deleted
inserted
replaced
32 lemma forest_def: "forest(A) == Part(tree_forest(A), Inr)" |
32 lemma forest_def: "forest(A) == Part(tree_forest(A), Inr)" |
33 by (simp only: tree_forest.defs) |
33 by (simp only: tree_forest.defs) |
34 |
34 |
35 |
35 |
36 text \<open> |
36 text \<open> |
37 \medskip @{term "tree_forest(A)"} as the union of @{term "tree(A)"} |
37 \medskip \<^term>\<open>tree_forest(A)\<close> as the union of \<^term>\<open>tree(A)\<close> |
38 and @{term "forest(A)"}. |
38 and \<^term>\<open>forest(A)\<close>. |
39 \<close> |
39 \<close> |
40 |
40 |
41 lemma tree_subset_TF: "tree(A) \<subseteq> tree_forest(A)" |
41 lemma tree_subset_TF: "tree(A) \<subseteq> tree_forest(A)" |
42 apply (unfold tree_forest.defs) |
42 apply (unfold tree_forest.defs) |
43 apply (rule Part_subset) |
43 apply (rule Part_subset) |