Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Term.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Induct/Term.thy
    Author:     Stefan Berghofer,  TU Muenchen
*)

section \<open>Terms over a given alphabet\<close>

theory Term
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.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.