src/HOL/Isar_examples/NestedDatatype.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 18460 9a1458cb2956
child 23373 ead82c82da9e
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
wenzelm@18153
     1
wenzelm@18153
     2
(* $Id$ *)
wenzelm@8676
     3
wenzelm@10007
     4
header {* Nested datatypes *}
wenzelm@8676
     5
haftmann@16417
     6
theory NestedDatatype imports Main begin
wenzelm@8676
     7
wenzelm@10007
     8
subsection {* Terms and substitution *}
wenzelm@8676
     9
wenzelm@8676
    10
datatype ('a, 'b) "term" =
wenzelm@8676
    11
    Var 'a
wenzelm@10007
    12
  | App 'b "('a, 'b) term list"
wenzelm@8676
    13
wenzelm@8676
    14
consts
wenzelm@8717
    15
  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
wenzelm@8676
    16
  subst_term_list ::
wenzelm@10007
    17
    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
wenzelm@8676
    18
wenzelm@8676
    19
primrec (subst)
wenzelm@8676
    20
  "subst_term f (Var a) = f a"
wenzelm@8676
    21
  "subst_term f (App b ts) = App b (subst_term_list f ts)"
wenzelm@8676
    22
  "subst_term_list f [] = []"
wenzelm@10007
    23
  "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
wenzelm@8676
    24
wenzelm@8676
    25
wenzelm@8676
    26
text {*
wenzelm@8676
    27
 \medskip A simple lemma about composition of substitutions.
wenzelm@10007
    28
*}
wenzelm@8676
    29
wenzelm@18460
    30
lemma "subst_term (subst_term f1 o f2) t =
wenzelm@18460
    31
      subst_term f1 (subst_term f2 t)"
wenzelm@18460
    32
  and "subst_term_list (subst_term f1 o f2) ts =
wenzelm@10007
    33
      subst_term_list f1 (subst_term_list f2 ts)"
wenzelm@11809
    34
  by (induct t and ts) simp_all
wenzelm@8676
    35
wenzelm@9659
    36
lemma "subst_term (subst_term f1 o f2) t =
wenzelm@10007
    37
  subst_term f1 (subst_term f2 t)"
wenzelm@10007
    38
proof -
wenzelm@10007
    39
  let "?P t" = ?thesis
wenzelm@10007
    40
  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 o f2) ts =
wenzelm@10007
    41
    subst_term_list f1 (subst_term_list f2 ts)"
wenzelm@10007
    42
  show ?thesis
wenzelm@10007
    43
  proof (induct t)
wenzelm@10007
    44
    fix a show "?P (Var a)" by simp
wenzelm@10007
    45
  next
wenzelm@10007
    46
    fix b ts assume "?Q ts"
wenzelm@10007
    47
    thus "?P (App b ts)" by (simp add: o_def)
wenzelm@10007
    48
  next
wenzelm@10007
    49
    show "?Q []" by simp
wenzelm@10007
    50
  next
wenzelm@10007
    51
    fix t ts
wenzelm@10007
    52
    assume "?P t" "?Q ts" thus "?Q (t # ts)" by simp
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)"
wenzelm@18153
    61
    and app: "!!b ts. list_all P ts ==> 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
wenzelm@18153
    66
  fix b t ts assume "list_all P ts"
wenzelm@18153
    67
  thus "P (App b ts)" by (rule app)
wenzelm@18153
    68
next
wenzelm@18153
    69
  show "list_all P []" by simp
wenzelm@18153
    70
next
wenzelm@18153
    71
  fix t ts assume "P t" "list_all P ts"
wenzelm@18153
    72
  thus "list_all P (t # ts)" 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@18153
    82
  thus ?case by (induct ts) simp_all
wenzelm@10007
    83
qed
wenzelm@8676
    84
wenzelm@10007
    85
end