author wenzelm
Sat, 03 Feb 2001 17:40:16 +0100
changeset 11046 b5f5942781a0
parent 5738 0d8698c15439
child 11549 e7265e70fd7c
permissions -rw-r--r--
Induct: converted some theories to new-style format;

(*  Title:      HOL/Induct/Term.thy
    ID:         $Id$
    Author:     Stefan Berghofer,  TU Muenchen
    Copyright   1998  TU Muenchen

header {* Terms over a given alphabet *}

theory Term = Main:

datatype ('a, 'b) "term" =
    Var 'a
  | App 'b "('a, 'b) term list"

text {* \medskip Substitution function on terms *}

  subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
  subst_term_list ::
    "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"

  "subst_term f (Var a) = f a"
  "subst_term f (App b ts) = App b (subst_term_list f ts)"

  "subst_term_list f [] = []"
  "subst_term_list f (t # ts) =
     subst_term f t # subst_term_list f ts"

text {* \medskip A simple theorem about composition of substitutions *}

lemma subst_comp:
  "(subst_term ((subst_term f1) \<circ> f2) t) =
    (subst_term f1 (subst_term f2 t)) \<and>
  (subst_term_list ((subst_term f1) \<circ> f2) ts) =
    (subst_term_list f1 (subst_term_list f2 ts))"
  apply (induct t and ts rule: term.induct)
     apply simp_all

text {* \medskip Alternative induction rule *}

lemma term_induct2:
  "(!!v. P (Var v)) ==>
    (!!f ts. list_all P ts ==> P (App f ts))
  ==> P t"
proof -
  case antecedent
  have "P t \<and> list_all P ts"
    apply (induct t and ts rule: term.induct)
       apply (rule antecedent)
      apply (rule antecedent)
      apply assumption
     apply simp_all
  thus ?thesis ..