src/HOL/Isar_Examples/Nested_Datatype.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 58260 c96e511bfb79
child 58310 91ea607a34d8
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
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
blanchet@58249
     9
datatype_new ('a, 'b) "term" =
wenzelm@55656
    10
  Var 'a
wenzelm@55656
    11
| App 'b "('a, 'b) term list"
wenzelm@8676
    12
wenzelm@55656
    13
primrec subst_term :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term \<Rightarrow> ('a, 'b) term"
wenzelm@55656
    14
  and subst_term_list :: "('a \<Rightarrow> ('a, 'b) term) \<Rightarrow> ('a, 'b) term list \<Rightarrow> ('a, 'b) term list"
wenzelm@37671
    15
where
haftmann@37597
    16
  "subst_term f (Var a) = f a"
haftmann@37597
    17
| "subst_term f (App b ts) = App b (subst_term_list f ts)"
haftmann@37597
    18
| "subst_term_list f [] = []"
haftmann@37597
    19
| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
wenzelm@8676
    20
blanchet@58260
    21
lemmas subst_simps = subst_term.simps subst_term_list.simps
wenzelm@8676
    22
wenzelm@37671
    23
text {* \medskip A simple lemma about composition of substitutions. *}
wenzelm@8676
    24
wenzelm@37671
    25
lemma
wenzelm@55656
    26
  "subst_term (subst_term f1 \<circ> f2) t =
wenzelm@37671
    27
    subst_term f1 (subst_term f2 t)"
wenzelm@37671
    28
  and
wenzelm@55656
    29
  "subst_term_list (subst_term f1 \<circ> f2) ts =
wenzelm@37671
    30
    subst_term_list f1 (subst_term_list f2 ts)"
blanchet@58260
    31
  by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
wenzelm@8676
    32
blanchet@58260
    33
lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
wenzelm@10007
    34
proof -
wenzelm@10007
    35
  let "?P t" = ?thesis
wenzelm@55656
    36
  let ?Q = "\<lambda>ts. subst_term_list (subst_term f1 \<circ> f2) ts =
wenzelm@10007
    37
    subst_term_list f1 (subst_term_list f2 ts)"
wenzelm@10007
    38
  show ?thesis
blanchet@58260
    39
  proof (induct t rule: subst_term.induct)
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@55656
    57
lemma "subst_term (subst_term f1 \<circ> f2) t = subst_term f1 (subst_term f2 t)"
blanchet@58260
    58
proof (induct t rule: term.induct)
wenzelm@11809
    59
  case (Var a)
wenzelm@18153
    60
  show ?case by (simp add: o_def)
wenzelm@10007
    61
next
wenzelm@11809
    62
  case (App b ts)
wenzelm@23373
    63
  then show ?case by (induct ts) simp_all
wenzelm@10007
    64
qed
wenzelm@8676
    65
wenzelm@10007
    66
end