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