Quelle JBasis.thy Sprache: Isabelle

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

quality100%

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.