src/HOL/Induct/Term.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 18461 9125d278fdc8
child 36862 952b2b102a0a
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
berghofe@5738
     1
(*  Title:      HOL/Induct/Term.thy
paulson@3120
     2
    ID:         $Id$
berghofe@5738
     3
    Author:     Stefan Berghofer,  TU Muenchen
paulson@3120
     4
*)
paulson@3120
     5
wenzelm@11046
     6
header {* Terms over a given alphabet *}
wenzelm@11046
     7
haftmann@16417
     8
theory Term imports Main begin
paulson@3120
     9
wenzelm@11046
    10
datatype ('a, 'b) "term" =
wenzelm@11046
    11
    Var 'a
wenzelm@11046
    12
  | App 'b "('a, 'b) term list"
paulson@3120
    13
berghofe@5738
    14
wenzelm@11046
    15
text {* \medskip Substitution function on terms *}
paulson@3120
    16
paulson@3120
    17
consts
wenzelm@11046
    18
  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
berghofe@5738
    19
  subst_term_list ::
wenzelm@11046
    20
    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
paulson@3120
    21
berghofe@5738
    22
primrec
berghofe@5738
    23
  "subst_term f (Var a) = f a"
berghofe@5738
    24
  "subst_term f (App b ts) = App b (subst_term_list f ts)"
paulson@3120
    25
berghofe@5738
    26
  "subst_term_list f [] = []"
berghofe@5738
    27
  "subst_term_list f (t # ts) =
berghofe@5738
    28
     subst_term f t # subst_term_list f ts"
paulson@3120
    29
wenzelm@11046
    30
wenzelm@11046
    31
text {* \medskip A simple theorem about composition of substitutions *}
wenzelm@11046
    32
wenzelm@11046
    33
lemma subst_comp:
wenzelm@12171
    34
  "subst_term (subst_term f1 \<circ> f2) t =
wenzelm@12171
    35
    subst_term f1 (subst_term f2 t)"
wenzelm@12171
    36
and "subst_term_list (subst_term f1 \<circ> f2) ts =
wenzelm@12171
    37
    subst_term_list f1 (subst_term_list f2 ts)"
wenzelm@12171
    38
  by (induct t and ts) simp_all
wenzelm@11046
    39
wenzelm@11046
    40
wenzelm@11046
    41
text {* \medskip Alternative induction rule *}
wenzelm@11046
    42
wenzelm@12171
    43
lemma
wenzelm@12937
    44
  assumes var: "!!v. P (Var v)"
wenzelm@12937
    45
    and app: "!!f ts. list_all P ts ==> P (App f ts)"
wenzelm@12937
    46
  shows term_induct2: "P t"
wenzelm@18461
    47
    and "list_all P ts"
wenzelm@12171
    48
  apply (induct t and ts)
wenzelm@12171
    49
     apply (rule var)
wenzelm@12171
    50
    apply (rule app)
wenzelm@12171
    51
    apply assumption
wenzelm@12171
    52
   apply simp_all
wenzelm@12171
    53
  done
wenzelm@11046
    54
paulson@3120
    55
end