# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID c96e511bfb7901d9e6fc5957126fe3e355009393
# Parent  52c35a59bbf53d67e80ca34cf8451dfb6f34f768
ported Isar_Examples to new datatypes

diff -r 52c35a59bbf5 -r c96e511bfb79 src/HOL/Isar_Examples/Expr_Compiler.thy
--- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -31,7 +31,7 @@
   consisting of variables, constants, and binary operations on
   expressions. *}
 
-datatype_new ('adr, 'val) expr =
+datatype_new (dead 'adr, dead 'val) expr =
     Variable 'adr
   | Constant 'val
   | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
@@ -51,7 +51,7 @@
 text {* Next we model a simple stack machine, with three
   instructions. *}
 
-datatype_new ('adr, 'val) instr =
+datatype_new (dead 'adr, dead 'val) instr =
     Const 'val
   | Load 'adr
   | Apply "'val binop"
diff -r 52c35a59bbf5 -r c96e511bfb79 src/HOL/Isar_Examples/Nested_Datatype.thy
--- 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