src/HOL/Isar_Examples/Nested_Datatype.thy
author haftmann
Wed Jun 30 16:46:44 2010 +0200 (2010-06-30)
changeset 37659 14cabf5fa710
parent 37597 a02ea93e88c6
child 37671 fa53d267dab3
permissions -rw-r--r--
more speaking names
wenzelm@10007
     1
header {* Nested datatypes *}
wenzelm@8676
     2
wenzelm@31758
     3
theory Nested_Datatype
wenzelm@31758
     4
imports Main
wenzelm@31758
     5
begin
wenzelm@8676
     6
wenzelm@10007
     7
subsection {* Terms and substitution *}
wenzelm@8676
     8
wenzelm@8676
     9
datatype ('a, 'b) "term" =
wenzelm@8676
    10
    Var 'a
wenzelm@10007
    11
  | App 'b "('a, 'b) term list"
wenzelm@8676
    12
haftmann@37597
    13
primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
haftmann@37597
    14
  subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list" where
haftmann@37597
    15
  "subst_term f (Var a) = f a"
haftmann@37597
    16
| "subst_term f (App b ts) = App b (subst_term_list f ts)"
haftmann@37597
    17
| "subst_term_list f [] = []"
haftmann@37597
    18
| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
wenzelm@8676
    19
haftmann@37597
    20
lemmas subst_simps = subst_term_subst_term_list.simps
wenzelm@8676
    21
wenzelm@8676
    22
text {*
wenzelm@8676
    23
 \medskip A simple lemma about composition of substitutions.
wenzelm@10007
    24
*}
wenzelm@8676
    25
wenzelm@18460
    26
lemma "subst_term (subst_term f1 o f2) t =
wenzelm@18460
    27
      subst_term f1 (subst_term f2 t)"
wenzelm@18460
    28
  and "subst_term_list (subst_term f1 o f2) ts =
wenzelm@10007
    29
      subst_term_list f1 (subst_term_list f2 ts)"
wenzelm@11809
    30
  by (induct t and ts) simp_all
wenzelm@8676
    31
wenzelm@9659
    32
lemma "subst_term (subst_term f1 o f2) t =
wenzelm@10007
    33
  subst_term f1 (subst_term f2 t)"
wenzelm@10007
    34
proof -
wenzelm@10007
    35
  let "?P t" = ?thesis
wenzelm@10007
    36
  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
wenzelm@10007
    37
    subst_term_list f1 (subst_term_list f2 ts)"
wenzelm@10007
    38
  show ?thesis
wenzelm@10007
    39
  proof (induct t)
wenzelm@10007
    40
    fix a show "?P (Var a)" by simp
wenzelm@10007
    41
  next
wenzelm@10007
    42
    fix b ts assume "?Q ts"
wenzelm@23373
    43
    then show "?P (App b ts)"
haftmann@37597
    44
      by (simp only: subst_simps)
wenzelm@10007
    45
  next
wenzelm@10007
    46
    show "?Q []" by simp
wenzelm@10007
    47
  next
wenzelm@10007
    48
    fix t ts
wenzelm@23373
    49
    assume "?P t" "?Q ts" then show "?Q (t # ts)"
haftmann@37597
    50
      by (simp only: subst_simps)
wenzelm@10007
    51
  qed
wenzelm@10007
    52
qed
wenzelm@8676
    53
wenzelm@8676
    54
wenzelm@10007
    55
subsection {* Alternative induction *}
wenzelm@8676
    56
wenzelm@8676
    57
theorem term_induct' [case_names Var App]:
wenzelm@18153
    58
  assumes var: "!!a. P (Var a)"
haftmann@37597
    59
    and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
wenzelm@18153
    60
  shows "P t"
wenzelm@18153
    61
proof (induct t)
wenzelm@18153
    62
  fix a show "P (Var a)" by (rule var)
wenzelm@18153
    63
next
haftmann@37597
    64
  fix b t ts assume "\<forall>t \<in> set ts. P t"
wenzelm@23373
    65
  then show "P (App b ts)" by (rule app)
wenzelm@18153
    66
next
haftmann@37597
    67
  show "\<forall>t \<in> set []. P t" by simp
wenzelm@18153
    68
next
haftmann@37597
    69
  fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"
haftmann@37597
    70
  then show "\<forall>t' \<in> set (t # ts). P t'" by simp
wenzelm@10007
    71
qed
wenzelm@8676
    72
wenzelm@8717
    73
lemma
wenzelm@8717
    74
  "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
wenzelm@11809
    75
proof (induct t rule: term_induct')
wenzelm@11809
    76
  case (Var a)
wenzelm@18153
    77
  show ?case by (simp add: o_def)
wenzelm@10007
    78
next
wenzelm@11809
    79
  case (App b ts)
wenzelm@23373
    80
  then show ?case by (induct ts) simp_all
wenzelm@10007
    81
qed
wenzelm@8676
    82
wenzelm@10007
    83
end