--- a/src/HOL/Induct/Term.thy Sat Feb 03 15:22:57 2001 +0100
+++ b/src/HOL/Induct/Term.thy Sat Feb 03 17:40:16 2001 +0100
@@ -2,23 +2,23 @@
ID: $Id$
Author: Stefan Berghofer, TU Muenchen
Copyright 1998 TU Muenchen
-
-Terms over a given alphabet -- function applications
*)
-Term = Main +
+header {* Terms over a given alphabet *}
+
+theory Term = Main:
-datatype
- ('a, 'b) term = Var 'a
- | App 'b ((('a, 'b) term) list)
+datatype ('a, 'b) "term" =
+ Var 'a
+ | App 'b "('a, 'b) term list"
-(** substitution function on terms **)
+text {* \medskip Substitution function on terms *}
consts
- subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term"
+ 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"
+ "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
primrec
"subst_term f (Var a) = f a"
@@ -28,4 +28,35 @@
"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
+ done
+
+
+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
+ done
+ thus ?thesis ..
+qed
+
end