Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Library/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 4 kB

Quelle ListVector.thy Sprache: Isabelle

(*  Author: Tobias Nipkow, 2007 *)

section \<open>Lists as vectors\<close>

theory ListVector
  imports Main
begin

text\<open>\noindent
A vector-space like structure of lists and arithmetic operations on them.
Is only a vector space if restricted to lists of the same length.\<close>

text\<open>Multiplication with a scalar:\<close>

abbreviation scale :: "('a::times) \ 'a list \ 'a list" (infix \*\<^sub>s\ 70)
  where "x *\<^sub>s xs \ map ((*) x) xs"

lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
  by (induct xs) simp_all

subsection \<open>\<open>+\<close> and \<open>-\<close>\<close>

fun zipwith0 :: "('a::zero \ 'b::zero \ 'c) \ 'a list \ 'b list \ 'c list"
  where
    "zipwith0 f [] [] = []" |
    "zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
    "zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
    "zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"

instantiation list :: ("{zero, plus}") plus
begin

definition
  list_add_def: "(+) = zipwith0 (+)"

instance ..

end

instantiation list :: ("{zero, uminus}") uminus
begin

definition
  list_uminus_def: "uminus = map uminus"

instance ..

end

instantiation list :: ("{zero,minus}") minus
begin

definition
  list_diff_def: "(-) = zipwith0 (-)"

instance ..

end

lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
  by(induct ys) simp_all

lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
  by (induct xs) (auto simp:list_add_def)

lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"
  by (induct xs) (auto simp:list_add_def)

lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"
  by(auto simp:list_add_def)

lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"
  by (induct xs) (auto simp:list_diff_def list_uminus_def)

lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"
  by (induct xs) (auto simp:list_diff_def)

lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"
  by (induct xs) (auto simp:list_diff_def)

lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"
  by (induct xs) (auto simp:list_uminus_def)

lemma self_list_diff:
  "xs - xs = replicate (length(xs::'a::group_add list)) 0"
  by(induct xs) simp_all

lemma list_add_assoc:
  fixes xs :: "'a::monoid_add list"
  shows "(xs+ys)+zs = xs+(ys+zs)"
proof (induct xs arbitrary: ys zs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs ys zs)
  show ?case
    by (cases ys; cases zs; simp add: add.assoc Cons)
qed

subsection "Inner product"

definition iprod :: "'a::ring list \ 'a list \ 'a" (\(\open_block notation=\mixfix iprod\\\_,_\)\)
  where "\xs,ys\ = (\(x,y) \ zip xs ys. x*y)"

lemma iprod_Nil[simp]: "\[],ys\ = 0"
  by(simp add: iprod_def)

lemma iprod_Nil2[simp]: "\xs,[]\ = 0"
  by(simp add: iprod_def)

lemma iprod_Cons[simp]: "\x#xs,y#ys\ = x*y + \xs,ys\"
  by(simp add: iprod_def)

lemma iprod0_if_coeffs0: "\c\set cs. c = 0 \ \cs,xs\ = 0"
proof (induct cs arbitrary: xs)
  case Nil
  then show ?case by simp
next
  case (Cons a cs xs)
  then show ?case
    by (cases xs; fastforce)
qed

lemma iprod_uminus[simp]: "\-xs,ys\ = -\xs,ys\"
  by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)

lemma iprod_left_add_distrib: "\xs + ys,zs\ = \xs,zs\ + \ys,zs\"
proof (induct xs arbitrary: ys zs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs ys zs)
  show ?case
    by (cases ys; cases zs; simp add: distrib_right Cons)
qed

lemma iprod_left_diff_distrib: "\xs - ys, zs\ = \xs,zs\ - \ys,zs\"
proof (induct xs arbitrary: ys zs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs ys zs)
  show ?case
    by (cases ys; cases zs; simp add: left_diff_distrib Cons)
qed

lemma iprod_assoc: "\x *\<^sub>s xs, ys\ = x * \xs,ys\"
proof (induct xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons a xs ys)
  show ?case
    by (cases ys; simp add: distrib_left mult.assoc Cons)
qed

end

quality99%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

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.