src/HOL/Isar_Examples/Nested_Datatype.thy
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 37671 fa53d267dab3
child 55656 eb07b0acbebc
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
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
wenzelm@37671
    13
primrec
wenzelm@37671
    14
  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term" and
wenzelm@37671
    15
  subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
wenzelm@37671
    16
where
haftmann@37597
    17
  "subst_term f (Var a) = f a"
haftmann@37597
    18
| "subst_term f (App b ts) = App b (subst_term_list f ts)"
haftmann@37597
    19
| "subst_term_list f [] = []"
haftmann@37597
    20
| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
wenzelm@8676
    21
haftmann@37597
    22
lemmas subst_simps = subst_term_subst_term_list.simps
wenzelm@8676
    23
wenzelm@37671
    24
text {* \medskip A simple lemma about composition of substitutions. *}
wenzelm@8676
    25
wenzelm@37671
    26
lemma
wenzelm@37671
    27
  "subst_term (subst_term f1 o f2) t =
wenzelm@37671
    28
    subst_term f1 (subst_term f2 t)"
wenzelm@37671
    29
  and
wenzelm@37671
    30
  "subst_term_list (subst_term f1 o f2) ts =
wenzelm@37671
    31
    subst_term_list f1 (subst_term_list f2 ts)"
wenzelm@11809
    32
  by (induct t and ts) simp_all
wenzelm@8676
    33
wenzelm@9659
    34
lemma "subst_term (subst_term f1 o f2) t =
wenzelm@37671
    35
    subst_term f1 (subst_term f2 t)"
wenzelm@10007
    36
proof -
wenzelm@10007
    37
  let "?P t" = ?thesis
wenzelm@10007
    38
  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
wenzelm@10007
    39
    subst_term_list f1 (subst_term_list f2 ts)"
wenzelm@10007
    40
  show ?thesis
wenzelm@10007
    41
  proof (induct t)
wenzelm@10007
    42
    fix a show "?P (Var a)" by simp
wenzelm@10007
    43
  next
wenzelm@10007
    44
    fix b ts assume "?Q ts"
wenzelm@23373
    45
    then show "?P (App b ts)"
haftmann@37597
    46
      by (simp only: subst_simps)
wenzelm@10007
    47
  next
wenzelm@10007
    48
    show "?Q []" by simp
wenzelm@10007
    49
  next
wenzelm@10007
    50
    fix t ts
wenzelm@23373
    51
    assume "?P t" "?Q ts" then show "?Q (t # ts)"
haftmann@37597
    52
      by (simp only: subst_simps)
wenzelm@10007
    53
  qed
wenzelm@10007
    54
qed
wenzelm@8676
    55
wenzelm@8676
    56
wenzelm@10007
    57
subsection {* Alternative induction *}
wenzelm@8676
    58
wenzelm@8676
    59
theorem term_induct' [case_names Var App]:
wenzelm@18153
    60
  assumes var: "!!a. P (Var a)"
haftmann@37597
    61
    and app: "!!b ts. (\<forall>t \<in> set ts. P t) ==> P (App b ts)"
wenzelm@18153
    62
  shows "P t"
wenzelm@18153
    63
proof (induct t)
wenzelm@18153
    64
  fix a show "P (Var a)" by (rule var)
wenzelm@18153
    65
next
haftmann@37597
    66
  fix b t ts assume "\<forall>t \<in> set ts. P t"
wenzelm@23373
    67
  then show "P (App b ts)" by (rule app)
wenzelm@18153
    68
next
haftmann@37597
    69
  show "\<forall>t \<in> set []. P t" by simp
wenzelm@18153
    70
next
haftmann@37597
    71
  fix t ts assume "P t" "\<forall>t' \<in> set ts. P t'"
haftmann@37597
    72
  then show "\<forall>t' \<in> set (t # ts). P t'" by simp
wenzelm@10007
    73
qed
wenzelm@8676
    74
wenzelm@8717
    75
lemma
wenzelm@8717
    76
  "subst_term (subst_term f1 o f2) t = subst_term f1 (subst_term f2 t)"
wenzelm@11809
    77
proof (induct t rule: term_induct')
wenzelm@11809
    78
  case (Var a)
wenzelm@18153
    79
  show ?case by (simp add: o_def)
wenzelm@10007
    80
next
wenzelm@11809
    81
  case (App b ts)
wenzelm@23373
    82
  then show ?case by (induct ts) simp_all
wenzelm@10007
    83
qed
wenzelm@8676
    84
wenzelm@10007
    85
end