equal
deleted
inserted
replaced
58 |
58 |
59 val tree_forest_unfold' = rewrite_rule (tl TF.defs) tree_forest_unfold; |
59 val tree_forest_unfold' = rewrite_rule (tl TF.defs) tree_forest_unfold; |
60 |
60 |
61 |
61 |
62 goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}"; |
62 goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}"; |
63 br (Part_Inl RS subst) 1; |
63 by (rtac (Part_Inl RS subst) 1); |
64 br (tree_forest_unfold' RS subst_context) 1; |
64 by (rtac (tree_forest_unfold' RS subst_context) 1); |
65 val tree_unfold = result(); |
65 val tree_unfold = result(); |
66 |
66 |
67 goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}"; |
67 goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}"; |
68 br (Part_Inr RS subst) 1; |
68 by (rtac (Part_Inr RS subst) 1); |
69 br (tree_forest_unfold' RS subst_context) 1; |
69 by (rtac (tree_forest_unfold' RS subst_context) 1); |
70 val forest_unfold = result(); |
70 val forest_unfold = result(); |
71 |
71 |
72 |
72 |
73 |
73 |