Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/C/Lyx/src/     Datei vom 26.9.1998 mit Größe 6 kB image not shown  

SSL Term.thy   Interaktion und
PortierbarkeitIsabelle

 
(*  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

95%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.13Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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:

sprechenden Kalenders