ported Isar_Examples to new datatypes
authorblanchet
Tue Sep 09 20:51:36 2014 +0200 (2014-09-09)
changeset 58260c96e511bfb79
parent 58259 52c35a59bbf5
child 58261 10bd5ba8c9e6
ported Isar_Examples to new datatypes
src/HOL/Isar_Examples/Expr_Compiler.thy
src/HOL/Isar_Examples/Nested_Datatype.thy
     1.1 --- a/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Sep 09 20:51:36 2014 +0200
     1.2 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Sep 09 20:51:36 2014 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    consisting of variables, constants, and binary operations on
     1.5    expressions. *}
     1.6  
     1.7 -datatype_new ('adr, 'val) expr =
     1.8 +datatype_new (dead 'adr, dead 'val) expr =
     1.9      Variable 'adr
    1.10    | Constant 'val
    1.11    | Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
    1.12 @@ -51,7 +51,7 @@
    1.13  text {* Next we model a simple stack machine, with three
    1.14    instructions. *}
    1.15  
    1.16 -datatype_new ('adr, 'val) instr =
    1.17 +datatype_new (dead 'adr, dead 'val) instr =
    1.18      Const 'val
    1.19    | Load 'adr
    1.20    | Apply "'val binop"
     2.1 --- a/src/HOL/Isar_Examples/Nested_Datatype.thy	Tue Sep 09 20:51:36 2014 +0200
     2.2 +++ b/src/HOL/Isar_Examples/Nested_Datatype.thy	Tue Sep 09 20:51:36 2014 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4  | "subst_term_list f [] = []"
     2.5  | "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
     2.6  
     2.7 -lemmas subst_simps = subst_term_subst_term_list.simps
     2.8 +lemmas subst_simps = subst_term.simps subst_term_list.simps
     2.9  
    2.10  text {* \medskip A simple lemma about composition of substitutions. *}
    2.11  
    2.12 @@ -28,16 +28,15 @@
    2.13    and
    2.14    "subst_term_list (subst_term f1 \<circ> f2) ts =
    2.15      subst_term_list f1 (subst_term_list f2 ts)"
    2.16 -  by (induct t and ts) simp_all
    2.17 +  by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
    2.18  
    2.19 -lemma "subst_term (subst_term f1 \<circ> f2) t =
    2.20 -    subst_term f1 (subst_term f2 t)"
    2.21 +lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
    2.22  proof -
    2.23    let "?P t" = ?thesis
    2.24    let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 \<circ> f2) ts =
    2.25      subst_term_list f1 (subst_term_list f2 ts)"
    2.26    show ?thesis
    2.27 -  proof (induct t)
    2.28 +  proof (induct t rule: subst_term.induct)
    2.29      fix a show "?P (Var a)" by simp
    2.30    next
    2.31      fix b ts assume "?Q ts"
    2.32 @@ -55,24 +54,8 @@
    2.33  
    2.34  subsection {* Alternative induction *}
    2.35  
    2.36 -theorem term_induct' [case_names Var App]:
    2.37 -  assumes var: "\<And>a. P (Var a)"
    2.38 -    and app: "\<And>b ts. (\<forall>t \<in> set ts. P t) \<Longrightarrow> P (App b ts)"
    2.39 -  shows "P t"
    2.40 -proof (induct t)
    2.41 -  fix a show "P (Var a)" by (rule var)
    2.42 -next
    2.43 -  fix b t ts assume "\<forall>t \<in> set ts. P t"
    2.44 -  then show "P (App b ts)" by (rule app)
    2.45 -next
    2.46 -  show "\<forall>t \<in> set []. P t" by simp
    2.47 -next
    2.48 -  fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"
    2.49 -  then show "\<forall>t' \<in> set (t # ts). P t'" by simp
    2.50 -qed
    2.51 -
    2.52  lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
    2.53 -proof (induct t rule: term_induct')
    2.54 +proof (induct t rule: term.induct)
    2.55    case (Var a)
    2.56    show ?case by (simp add: o_def)
    2.57  next