src/HOL/Induct/Term.thy
 changeset 11046 b5f5942781a0 parent 5738 0d8698c15439 child 11549 e7265e70fd7c
```--- 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
-
-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```