--- a/src/ZF/Induct/Tree_Forest.thy Thu Dec 22 00:28:41 2005 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Thu Dec 22 00:28:43 2005 +0100
@@ -18,6 +18,12 @@
datatype "tree(A)" = Tcons ("a \<in> A", "f \<in> forest(A)")
and "forest(A)" = Fnil | Fcons ("t \<in> tree(A)", "f \<in> forest(A)")
+(* FIXME *)
+lemmas tree'induct =
+ tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, standard, consumes 1]
+ and forest'induct =
+ tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, standard, consumes 1]
+
declare tree_forest.intros [simp, TC]
lemma tree_def: "tree(A) == Part(tree_forest(A), Inl)"
@@ -158,36 +164,28 @@
lemma list_of_TF_type [TC]:
"z \<in> tree_forest(A) ==> list_of_TF(z) \<in> list(tree(A))"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
lemma of_list_type [TC]: "l \<in> list(tree(A)) ==> of_list(l) \<in> forest(A)"
- apply (erule list.induct)
- apply simp_all
- done
+ by (induct set: list) simp_all
text {*
\medskip @{text map}.
*}
lemma
- assumes h_type: "!!x. x \<in> A ==> h(x): B"
+ assumes "!!x. x \<in> A ==> h(x): B"
shows map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
- apply (induct rule: tree_forest.mutual_induct)
- apply (insert h_type)
- apply simp_all
- done
+ using prems
+ by (induct rule: tree'induct forest'induct) simp_all
text {*
\medskip @{text size}.
*}
lemma size_type [TC]: "z \<in> tree_forest(A) ==> size(z) \<in> nat"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
text {*
@@ -195,9 +193,7 @@
*}
lemma preorder_type [TC]: "z \<in> tree_forest(A) ==> preorder(z) \<in> list(A)"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
text {*
@@ -229,15 +225,11 @@
*}
lemma map_ident: "z \<in> tree_forest(A) ==> map(\<lambda>u. u, z) = z"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
lemma map_compose:
"z \<in> tree_forest(A) ==> map(h, map(j,z)) = map(\<lambda>u. h(j(u)), z)"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
text {*
@@ -245,14 +237,10 @@
*}
lemma size_map: "z \<in> tree_forest(A) ==> size(map(h,z)) = size(z)"
- apply (erule tree_forest.induct)
- apply simp_all
- done
+ by (induct set: tree_forest) simp_all
lemma size_length: "z \<in> tree_forest(A) ==> size(z) = length(preorder(z))"
- apply (erule tree_forest.induct)
- apply (simp_all add: length_app)
- done
+ by (induct set: tree_forest) (simp_all add: length_app)
text {*
\medskip Theorems about @{text preorder}.
@@ -260,8 +248,6 @@
lemma preorder_map:
"z \<in> tree_forest(A) ==> preorder(map(h,z)) = List.map(h, preorder(z))"
- apply (erule tree_forest.induct)
- apply (simp_all add: map_app_distrib)
- done
+ by (induct set: tree_forest) (simp_all add: map_app_distrib)
end