Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 15 kB image not shown  

SSL JBasis.thy   Interaktion und
PortierbarkeitIsabelle

 
(*  Title:      HOL/MicroJava/J/JBasis.thy
    Author:     David von Oheimb, TU Muenchen
*)

chapter \<open>Java Source Language \label{cha:j}\<close>

section \<open>Some Auxiliary Definitions\<close>

theory JBasis
imports
  Main
  "HOL-Library.Transitive_Closure_Table"
  "HOL-Eisbach.Eisbach"
begin

lemmas [simp] = Let_def

subsection "unique"
 
definition unique :: "('a \ 'b) list => bool" where
  "unique == distinct \ map fst"


lemma fst_in_set_lemma: "(x, y) \ set xys \ x \ fst ` set xys"
  by (induct xys) auto

lemma unique_Nil [simp]: "unique []"
  by (simp add: unique_def)

lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (\y. (x,y) \ set l))"
  by (auto simp: unique_def dest: fst_in_set_lemma)

lemma unique_append: "unique l' \ unique l \
    (\<forall>(x,y) \<in> set l. \<forall>(x',y') \<in> set l'. x' \<noteq> x) \<Longrightarrow> unique (l @ l')"
  by (induct l) (auto dest: fst_in_set_lemma)

lemma unique_map_inj: "unique l ==> inj f ==> unique (map (%(k,x). (f k, g k x)) l)"
  by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq)


subsection "More about Maps"

lemma map_of_SomeI: "unique l \ (k, x) \ set l \ map_of l k = Some x"
  by (induct l) auto

lemma Ball_set_table: "(\(x,y)\set l. P x y) ==> (\x. \y. map_of l x = Some y --> P x y)"
  by (induct l) auto

lemma table_of_remap_SomeD:
  "map_of (map (\((k,k'),x). (k,(k',x))) t) k = Some (k',x) ==>
    map_of t (k, k') = Some x"
  by (atomize (full), induct t) auto

end

100%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.3Angebot  ¤

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

Die farbliche Syntaxdarstellung ist noch experimentell.