(* Title: HOL/Induct/Term.thy Author: Stefan Berghofer, TU Muenchen
*)
section \<open>Terms over a given alphabet\<close>
theoryTerm imports Main begin
datatype ('a, 'b) "term" =
Var 'a
| App 'b "('a, 'b) term list"
text\<open>\medskip Substitution function on terms\<close>
primrec subst_term :: "('a \ ('a, 'b) term) \ ('a, 'b) term \ ('a, 'b) term" and subst_term_list :: "('a \ ('a, 'b) term) \ ('a, 'b) term list \ ('a, 'b) term list" where "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\<open>\medskip A simple theorem about composition of substitutions\<close>
lemma subst_comp: "subst_term (subst_term f1 \ f2) t =
subst_term f1 (subst_term f2 t)" and"subst_term_list (subst_term f1 \ f2) ts =
subst_term_list f1 (subst_term_list f2 ts)" by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
text\<open>\medskip Alternative induction rule\<close>
lemma assumes var: "\v. P (Var v)" and app: "\f ts. (\t \ set ts. P t) \ P (App f ts)" shows term_induct2: "P t" and"\t \ set ts. P t" apply (induct t and ts rule: subst_term.induct subst_term_list.induct) apply (rule var) apply (rule app) apply assumption apply simp_all done
end
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
