src/HOL/Isar_examples/NestedDatatype.thy
author wenzelm
Wed Apr 05 21:07:09 2000 +0200 (2000-04-05)
changeset 8676 4bf18b611a75
child 8717 20c42415c07d
permissions -rw-r--r--
added NestedDatatype.thy;
wenzelm@8676
     1
wenzelm@8676
     2
header {* Nested datatypes *};
wenzelm@8676
     3
wenzelm@8676
     4
theory NestedDatatype = Main:;
wenzelm@8676
     5
wenzelm@8676
     6
subsection {* Terms and substitution *};
wenzelm@8676
     7
wenzelm@8676
     8
datatype ('a, 'b) "term" =
wenzelm@8676
     9
    Var 'a
wenzelm@8676
    10
  | App 'b "('a, 'b) term list";
wenzelm@8676
    11
wenzelm@8676
    12
consts
wenzelm@8676
    13
  subst_term :: "('a \\<Rightarrow> ('a, 'b) term) \\<Rightarrow> ('a, 'b) term \\<Rightarrow> ('a, 'b) term"
wenzelm@8676
    14
  subst_term_list ::
wenzelm@8676
    15
    "('a \\<Rightarrow> ('a, 'b) term) \\<Rightarrow> ('a, 'b) term list \\<Rightarrow> ('a, 'b) term list";
wenzelm@8676
    16
wenzelm@8676
    17
primrec (subst)
wenzelm@8676
    18
  "subst_term f (Var a) = f a"
wenzelm@8676
    19
  "subst_term f (App b ts) = App b (subst_term_list f ts)"
wenzelm@8676
    20
  "subst_term_list f [] = []"
wenzelm@8676
    21
  "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts";
wenzelm@8676
    22
wenzelm@8676
    23
wenzelm@8676
    24
text {*
wenzelm@8676
    25
 \medskip A simple lemma about composition of substitutions.
wenzelm@8676
    26
*};
wenzelm@8676
    27
wenzelm@8676
    28
lemma
wenzelm@8676
    29
   "subst_term (subst_term f1 o f2) t =
wenzelm@8676
    30
      subst_term f1 (subst_term f2 t) \\<and>
wenzelm@8676
    31
    subst_term_list (subst_term f1 o f2) ts =
wenzelm@8676
    32
      subst_term_list f1 (subst_term_list f2 ts)";
wenzelm@8676
    33
  by (induct t and ts rule: term.induct) simp_all;
wenzelm@8676
    34
wenzelm@8676
    35
lemma "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)";
wenzelm@8676
    36
proof -;
wenzelm@8676
    37
  let "?P t" = ?thesis;
wenzelm@8676
    38
  let ?Q = "\\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
wenzelm@8676
    39
    subst_term_list f1 (subst_term_list f2 ts)";
wenzelm@8676
    40
  show ?thesis;
wenzelm@8676
    41
  proof (induct t);
wenzelm@8676
    42
    fix a; show "?P (Var a)"; by simp;
wenzelm@8676
    43
  next;
wenzelm@8676
    44
    fix b ts; assume "?Q ts";
wenzelm@8676
    45
    thus "?P (App b ts)"; by (simp add: o_def);
wenzelm@8676
    46
  next;
wenzelm@8676
    47
    show "?Q []"; by simp;
wenzelm@8676
    48
  next;
wenzelm@8676
    49
    fix t ts;
wenzelm@8676
    50
    assume "?P t" "?Q ts"; thus "?Q (t # ts)"; by simp;
wenzelm@8676
    51
  qed;
wenzelm@8676
    52
qed;
wenzelm@8676
    53
wenzelm@8676
    54
wenzelm@8676
    55
subsection {* Alternative induction *};
wenzelm@8676
    56
wenzelm@8676
    57
theorem term_induct' [case_names Var App]:
wenzelm@8676
    58
 "(\\<And>a. P (Var a))
wenzelm@8676
    59
  \\<Longrightarrow> (\\<And>b ts. list_all P ts \\<Longrightarrow> P (App b ts))
wenzelm@8676
    60
  \\<Longrightarrow> P t";
wenzelm@8676
    61
proof -;
wenzelm@8676
    62
  assume var: "\\<And>a. P (Var a)";
wenzelm@8676
    63
  assume app: "\\<And>b ts. list_all P ts \\<Longrightarrow> P (App b ts)";
wenzelm@8676
    64
  show ?thesis;
wenzelm@8676
    65
  proof (induct P t);
wenzelm@8676
    66
    fix a; show "P (Var a)"; by (rule var);
wenzelm@8676
    67
  next;
wenzelm@8676
    68
    fix b t ts; assume "list_all P ts";
wenzelm@8676
    69
    thus "P (App b ts)"; by (rule app);
wenzelm@8676
    70
  next;
wenzelm@8676
    71
    show "list_all P []"; by simp;
wenzelm@8676
    72
  next;
wenzelm@8676
    73
    fix t ts; assume "P t" "list_all P ts";
wenzelm@8676
    74
    thus "list_all P (t # ts)"; by simp;
wenzelm@8676
    75
  qed;
wenzelm@8676
    76
qed;
wenzelm@8676
    77
wenzelm@8676
    78
lemma "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
wenzelm@8676
    79
  (is "?P t");
wenzelm@8676
    80
proof (induct ?P t rule: term_induct');
wenzelm@8676
    81
  case Var;
wenzelm@8676
    82
  show "?P (Var a)"; by (simp add: o_def);
wenzelm@8676
    83
next;
wenzelm@8676
    84
  case App;
wenzelm@8676
    85
  have "?this \\<longrightarrow> ?P (App b ts)";
wenzelm@8676
    86
    by (induct ts) simp_all;
wenzelm@8676
    87
  thus "..."; ..;
wenzelm@8676
    88
qed;
wenzelm@8676
    89
wenzelm@8676
    90
end;