--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Tue Sep 09 20:51:36 2014 +0200
@@ -18,7 +18,7 @@
| "subst_term_list f [] = []"
| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
-lemmas subst_simps = subst_term_subst_term_list.simps
+lemmas subst_simps = subst_term.simps subst_term_list.simps
text {* \medskip A simple lemma about composition of substitutions. *}
@@ -28,16 +28,15 @@
and
"subst_term_list (subst_term f1 \<circ> f2) ts =
subst_term_list f1 (subst_term_list f2 ts)"
- by (induct t and ts) simp_all
+ by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
-lemma "subst_term (subst_term f1 \<circ> f2) t =
- subst_term f1 (subst_term f2 t)"
+lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
proof -
let "?P t" = ?thesis
let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 \<circ> f2) ts =
subst_term_list f1 (subst_term_list f2 ts)"
show ?thesis
- proof (induct t)
+ proof (induct t rule: subst_term.induct)
fix a show "?P (Var a)" by simp
next
fix b ts assume "?Q ts"
@@ -55,24 +54,8 @@
subsection {* Alternative induction *}
-theorem term_induct' [case_names Var App]:
- assumes var: "\<And>a. P (Var a)"
- and app: "\<And>b ts. (\<forall>t \<in> set ts. P t) \<Longrightarrow> P (App b ts)"
- shows "P t"
-proof (induct t)
- fix a show "P (Var a)" by (rule var)
-next
- fix b t ts assume "\<forall>t \<in> set ts. P t"
- then show "P (App b ts)" by (rule app)
-next
- show "\<forall>t \<in> set []. P t" by simp
-next
- fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"
- then show "\<forall>t' \<in> set (t # ts). P t'" by simp
-qed
-
lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
-proof (induct t rule: term_induct')
+proof (induct t rule: term.induct)
case (Var a)
show ?case by (simp add: o_def)
next