src/HOL/Isar_examples/NestedDatatype.thy
changeset 8717 20c42415c07d
parent 8676 4bf18b611a75
child 9659 b9cf6801f3da
     1.1 --- a/src/HOL/Isar_examples/NestedDatatype.thy	Fri Apr 14 17:30:22 2000 +0200
     1.2 +++ b/src/HOL/Isar_examples/NestedDatatype.thy	Sat Apr 15 15:00:57 2000 +0200
     1.3 @@ -10,9 +10,9 @@
     1.4    | App 'b "('a, 'b) term list";
     1.5  
     1.6  consts
     1.7 -  subst_term :: "('a \\<Rightarrow> ('a, 'b) term) \\<Rightarrow> ('a, 'b) term \\<Rightarrow> ('a, 'b) term"
     1.8 +  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
     1.9    subst_term_list ::
    1.10 -    "('a \\<Rightarrow> ('a, 'b) term) \\<Rightarrow> ('a, 'b) term list \\<Rightarrow> ('a, 'b) term list";
    1.11 +    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list";
    1.12  
    1.13  primrec (subst)
    1.14    "subst_term f (Var a) = f a"
    1.15 @@ -27,7 +27,7 @@
    1.16  
    1.17  lemma
    1.18     "subst_term (subst_term f1 o f2) t =
    1.19 -      subst_term f1 (subst_term f2 t) \\<and>
    1.20 +      subst_term f1 (subst_term f2 t) &
    1.21      subst_term_list (subst_term f1 o f2) ts =
    1.22        subst_term_list f1 (subst_term_list f2 ts)";
    1.23    by (induct t and ts rule: term.induct) simp_all;
    1.24 @@ -55,12 +55,10 @@
    1.25  subsection {* Alternative induction *};
    1.26  
    1.27  theorem term_induct' [case_names Var App]:
    1.28 - "(\\<And>a. P (Var a))
    1.29 -  \\<Longrightarrow> (\\<And>b ts. list_all P ts \\<Longrightarrow> P (App b ts))
    1.30 -  \\<Longrightarrow> P t";
    1.31 + "(!!a. P (Var a)) ==> (!!b ts. list_all P ts ==> P (App b ts)) ==> P t";
    1.32  proof -;
    1.33 -  assume var: "\\<And>a. P (Var a)";
    1.34 -  assume app: "\\<And>b ts. list_all P ts \\<Longrightarrow> P (App b ts)";
    1.35 +  assume var: "!!a. P (Var a)";
    1.36 +  assume app: "!!b ts. list_all P ts ==> P (App b ts)";
    1.37    show ?thesis;
    1.38    proof (induct P t);
    1.39      fix a; show "P (Var a)"; by (rule var);
    1.40 @@ -75,14 +73,15 @@
    1.41    qed;
    1.42  qed;
    1.43  
    1.44 -lemma "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
    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 ?P t rule: term_induct');
    1.49    case Var;
    1.50    show "?P (Var a)"; by (simp add: o_def);
    1.51  next;
    1.52    case App;
    1.53 -  have "?this \\<longrightarrow> ?P (App b ts)";
    1.54 +  have "?this --> ?P (App b ts)";
    1.55      by (induct ts) simp_all;
    1.56    thus "..."; ..;
    1.57  qed;