src/HOL/Induct/Term.thy
author wenzelm
Wed May 12 14:17:26 2010 +0200 (2010-05-12)
changeset 36862 952b2b102a0a
parent 18461 9125d278fdc8
child 37597 a02ea93e88c6
permissions -rw-r--r--
removed obsolete CVS Ids;
     1 (*  Title:      HOL/Induct/Term.thy
     2     Author:     Stefan Berghofer,  TU Muenchen
     3 *)
     4 
     5 header {* Terms over a given alphabet *}
     6 
     7 theory Term imports Main begin
     8 
     9 datatype ('a, 'b) "term" =
    10     Var 'a
    11   | App 'b "('a, 'b) term list"
    12 
    13 
    14 text {* \medskip Substitution function on terms *}
    15 
    16 consts
    17   subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
    18   subst_term_list ::
    19     "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
    20 
    21 primrec
    22   "subst_term f (Var a) = f a"
    23   "subst_term f (App b ts) = App b (subst_term_list f ts)"
    24 
    25   "subst_term_list f [] = []"
    26   "subst_term_list f (t # ts) =
    27      subst_term f t # subst_term_list f ts"
    28 
    29 
    30 text {* \medskip A simple theorem about composition of substitutions *}
    31 
    32 lemma subst_comp:
    33   "subst_term (subst_term f1 \<circ> f2) t =
    34     subst_term f1 (subst_term f2 t)"
    35 and "subst_term_list (subst_term f1 \<circ> f2) ts =
    36     subst_term_list f1 (subst_term_list f2 ts)"
    37   by (induct t and ts) simp_all
    38 
    39 
    40 text {* \medskip Alternative induction rule *}
    41 
    42 lemma
    43   assumes var: "!!v. P (Var v)"
    44     and app: "!!f ts. list_all P ts ==> P (App f ts)"
    45   shows term_induct2: "P t"
    46     and "list_all P ts"
    47   apply (induct t and ts)
    48      apply (rule var)
    49     apply (rule app)
    50     apply assumption
    51    apply simp_all
    52   done
    53 
    54 end