src/HOL/Isar_examples/NestedDatatype.thy
changeset 18153 a084aa91f701
parent 16417 9bc16273c2d4
child 18460 9a1458cb2956
     1.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Thu Nov 10 20:57:22 2005 +0100
     1.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Thu Nov 10 21:14:05 2005 +0100
     1.3 @@ -1,3 +1,5 @@
     1.4 +
     1.5 +(* $Id$ *)
     1.6  
     1.7  header {* Nested datatypes *}
     1.8  
     1.9 @@ -56,34 +58,29 @@
    1.10  subsection {* Alternative induction *}
    1.11  
    1.12  theorem term_induct' [case_names Var App]:
    1.13 -  "(!!a. P (Var a)) ==>
    1.14 -   (!!b ts. list_all P ts ==> P (App b ts)) ==> P t"
    1.15 -proof -
    1.16 -  assume var: "!!a. P (Var a)"
    1.17 -  assume app: "!!b ts. list_all P ts ==> P (App b ts)"
    1.18 -  show ?thesis
    1.19 -  proof (induct t)
    1.20 -    fix a show "P (Var a)" by (rule var)
    1.21 -  next
    1.22 -    fix b t ts assume "list_all P ts"
    1.23 -    thus "P (App b ts)" by (rule app)
    1.24 -  next
    1.25 -    show "list_all P []" by simp
    1.26 -  next
    1.27 -    fix t ts assume "P t" "list_all P ts"
    1.28 -    thus "list_all P (t # ts)" by simp
    1.29 -  qed
    1.30 +  assumes var: "!!a. P (Var a)"
    1.31 +    and app: "!!b ts. list_all P ts ==> P (App b ts)"
    1.32 +  shows "P t"
    1.33 +proof (induct t)
    1.34 +  fix a show "P (Var a)" by (rule var)
    1.35 +next
    1.36 +  fix b t ts assume "list_all P ts"
    1.37 +  thus "P (App b ts)" by (rule app)
    1.38 +next
    1.39 +  show "list_all P []" by simp
    1.40 +next
    1.41 +  fix t ts assume "P t" "list_all P ts"
    1.42 +  thus "list_all P (t # ts)" by simp
    1.43  qed
    1.44  
    1.45  lemma
    1.46    "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
    1.47 -  (is "?P t")
    1.48  proof (induct t rule: term_induct')
    1.49    case (Var a)
    1.50 -  show "?P (Var a)" by (simp add: o_def)
    1.51 +  show ?case by (simp add: o_def)
    1.52  next
    1.53    case (App b ts)
    1.54 -  thus "?P (App b ts)" by (induct ts) simp_all
    1.55 +  thus ?case by (induct ts) simp_all
    1.56  qed
    1.57  
    1.58  end