src/HOL/Induct/Term.ML

Version 1.0 of linear nat arithmetic.

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

Terms over a given alphabet -- function applications
*)

(** a simple theorem about composition of substitutions **)

Goal "(subst_term ((subst_term f1) o f2) t) =  \
  \  (subst_term f1 (subst_term f2 t)) &  \
  \  (subst_term_list ((subst_term f1) o f2) ts) =  \
  \  (subst_term_list f1 (subst_term_list f2 ts))";
by (mutual_induct_tac ["t", "ts"] 1);
by (ALLGOALS Asm_full_simp_tac);
qed "subst_comp";

(**** alternative induction rule ****)

bind_thm ("term_induct2", prove_goal thy
  "[| !!v. P (Var v);  \
   \  !!f ts. list_all P ts ==> P (App f ts) |] ==>  \
   \    P t & list_all P ts"
  (fn prems =>
    [mutual_induct_tac ["t", "ts"] 1,
     resolve_tac prems 1,
     resolve_tac prems 1,
     atac 1,
     ALLGOALS Asm_simp_tac]) RS conjunct1);