Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: Lattice_Syntax.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Hahn_Banach/Linearform.thy
    Author:     Gertrud Bauer, TU Munich
*)

section \<open>Linearforms\<close>

theory Linearform
imports Vector_Space
begin

text \<open>
  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is
  additive and multiplicative.
\<close>

locale linearform =
  fixes V :: "'a::{minus, plus, zero, uminus} set" and f
  assumes add [iff]: "x \ V \ y \ V \ f (x + y) = f x + f y"
    and mult [iff]: "x \ V \ f (a \ x) = a * f x"

declare linearform.intro [intro?]

lemma (in linearform) neg [iff]:
  assumes "vectorspace V"
  shows "x \ V \ f (- x) = - f x"
proof -
  interpret vectorspace V by fact
  assume x: "x \ V"
  then have "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1)
  also from x have "\ = (- 1) * (f x)" by (rule mult)
  also from x have "\ = - (f x)" by simp
  finally show ?thesis .
qed

lemma (in linearform) diff [iff]:
  assumes "vectorspace V"
  shows "x \ V \ y \ V \ f (x - y) = f x - f y"
proof -
  interpret vectorspace V by fact
  assume x: "x \ V" and y: "y \ V"
  then have "x - y = x + - y" by (rule diff_eq1)
  also have "f \ = f x + f (- y)" by (rule add) (simp_all add: x y)
  also have "f (- y) = - f y" using \<open>vectorspace V\<close> y by (rule neg)
  finally show ?thesis by simp
qed

text \<open>Every linear form yields \<open>0\<close> for the \<open>0\<close> vector.\<close>

lemma (in linearform) zero [iff]:
  assumes "vectorspace V"
  shows "f 0 = 0"
proof -
  interpret vectorspace V by fact
  have "f 0 = f (0 - 0)" by simp
  also have "\ = f 0 - f 0" using \vectorspace V\ by (rule diff) simp_all
  also have "\ = 0" by simp
  finally show ?thesis .
qed

end

¤ Dauer der Verarbeitung: 0.0 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.