src/HOL/Isar_examples/NestedDatatype.thy
author wenzelm
Sun Sep 17 22:19:02 2000 +0200 (2000-09-17)
changeset 10007 64bf7da1994a
parent 9659 b9cf6801f3da
child 10458 df4e182c0fcd
permissions -rw-r--r--
isar-strip-terminators;
wenzelm@8676
     1
wenzelm@10007
     2
header {* Nested datatypes *}
wenzelm@8676
     3
wenzelm@10007
     4
theory NestedDatatype = Main:
wenzelm@8676
     5
wenzelm@10007
     6
subsection {* Terms and substitution *}
wenzelm@8676
     7
wenzelm@8676
     8
datatype ('a, 'b) "term" =
wenzelm@8676
     9
    Var 'a
wenzelm@10007
    10
  | App 'b "('a, 'b) term list"
wenzelm@8676
    11
wenzelm@8676
    12
consts
wenzelm@8717
    13
  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
wenzelm@8676
    14
  subst_term_list ::
wenzelm@10007
    15
    "('a => ('a, 'b) term) => ('a, 'b) term list => ('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@10007
    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@10007
    26
*}
wenzelm@8676
    27
wenzelm@8676
    28
lemma
wenzelm@8676
    29
   "subst_term (subst_term f1 o f2) t =
wenzelm@8717
    30
      subst_term f1 (subst_term f2 t) &
wenzelm@8676
    31
    subst_term_list (subst_term f1 o f2) ts =
wenzelm@10007
    32
      subst_term_list f1 (subst_term_list f2 ts)"
wenzelm@10007
    33
  by (induct t and ts rule: term.induct) simp_all
wenzelm@8676
    34
wenzelm@9659
    35
lemma "subst_term (subst_term f1 o f2) t =
wenzelm@10007
    36
  subst_term f1 (subst_term f2 t)"
wenzelm@10007
    37
proof -
wenzelm@10007
    38
  let "?P t" = ?thesis
wenzelm@10007
    39
  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
wenzelm@10007
    40
    subst_term_list f1 (subst_term_list f2 ts)"
wenzelm@10007
    41
  show ?thesis
wenzelm@10007
    42
  proof (induct t)
wenzelm@10007
    43
    fix a show "?P (Var a)" by simp
wenzelm@10007
    44
  next
wenzelm@10007
    45
    fix b ts assume "?Q ts"
wenzelm@10007
    46
    thus "?P (App b ts)" by (simp add: o_def)
wenzelm@10007
    47
  next
wenzelm@10007
    48
    show "?Q []" by simp
wenzelm@10007
    49
  next
wenzelm@10007
    50
    fix t ts
wenzelm@10007
    51
    assume "?P t" "?Q ts" thus "?Q (t # ts)" by simp
wenzelm@10007
    52
  qed
wenzelm@10007
    53
qed
wenzelm@8676
    54
wenzelm@8676
    55
wenzelm@10007
    56
subsection {* Alternative induction *}
wenzelm@8676
    57
wenzelm@8676
    58
theorem term_induct' [case_names Var App]:
wenzelm@9659
    59
  "(!!a. P (Var a)) ==>
wenzelm@10007
    60
   (!!b ts. list_all P ts ==> P (App b ts)) ==> P t"
wenzelm@10007
    61
proof -
wenzelm@10007
    62
  assume var: "!!a. P (Var a)"
wenzelm@10007
    63
  assume app: "!!b ts. list_all P ts ==> P (App b ts)"
wenzelm@10007
    64
  show ?thesis
wenzelm@10007
    65
  proof (induct P t)
wenzelm@10007
    66
    fix a show "P (Var a)" by (rule var)
wenzelm@10007
    67
  next
wenzelm@10007
    68
    fix b t ts assume "list_all P ts"
wenzelm@10007
    69
    thus "P (App b ts)" by (rule app)
wenzelm@10007
    70
  next
wenzelm@10007
    71
    show "list_all P []" by simp
wenzelm@10007
    72
  next
wenzelm@10007
    73
    fix t ts assume "P t" "list_all P ts"
wenzelm@10007
    74
    thus "list_all P (t # ts)" by simp
wenzelm@10007
    75
  qed
wenzelm@10007
    76
qed
wenzelm@8676
    77
wenzelm@8717
    78
lemma
wenzelm@8717
    79
  "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
wenzelm@10007
    80
  (is "?P t")
wenzelm@10007
    81
proof (induct (open) ?P t rule: term_induct')
wenzelm@10007
    82
  case Var
wenzelm@10007
    83
  show "?P (Var a)" by (simp add: o_def)
wenzelm@10007
    84
next
wenzelm@10007
    85
  case App
wenzelm@10007
    86
  have "?this --> ?P (App b ts)"
wenzelm@10007
    87
    by (induct ts) simp_all
wenzelm@10007
    88
  thus "..." ..
wenzelm@10007
    89
qed
wenzelm@8676
    90
wenzelm@10007
    91
end