products/Sources/formale Sprachen/Isabelle/HOL/Metis_Examples/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Options.pas.~113~   Sprache: Isabelle

Untersuchung Isabelle©
(*  Title:      HOL/Metis_Examples/Trans_Closure.thy
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
    Author:     Jasmin Blanchette, TU Muenchen

Metis example featuring the transitive closure.
*)

section \<open>Metis Example Featuring the Transitive Closure\<close>

theory Trans_Closure
imports Main
begin

declare [[metis_new_skolem]]

type_synonym addr = nat

datatype val
  = Unit        \<comment> \<open>dummy result value of void expressions\<close>
  | Null        \<comment> \<open>null reference\<close>
  | Bool bool   \<comment> \<open>Boolean value\<close>
  | Intg int    \<comment> \<open>integer value\<close>
  | Addr addr   \<comment> \<open>addresses of objects in the heap\<close>

consts R :: "(addr \ addr) set"

consts f :: "addr \ val"

lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b, c) \ R\<^sup>*\
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
(* sledgehammer *)
proof -
  assume A1: "f c = Intg x"
  assume A2: "\y. f b = Intg y \ y \ x"
  assume A3: "(a, b) \ R\<^sup>*"
  assume A4: "(b, c) \ R\<^sup>*"
  have F1: "f c \ f b" using A2 A1 by metis
  have F2: "\u. (b, u) \ R \ (a, u) \ R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
  have F3: "\x. (b, x b c R) \ R \ c = b" using A4 by (metis converse_rtranclE)
  have "c \ b" using F1 by metis
  hence "\u. (b, u) \ R" using F3 by metis
  thus "\c. (b, c) \ R \ (a, c) \ R\<^sup>*" using F2 by metis
qed

lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b,c) \ R\<^sup>*\
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
(* sledgehammer [isar_proofs, compress = 2] *)
proof -
  assume A1: "f c = Intg x"
  assume A2: "\y. f b = Intg y \ y \ x"
  assume A3: "(a, b) \ R\<^sup>*"
  assume A4: "(b, c) \ R\<^sup>*"
  have "b \ c" using A1 A2 by metis
  hence "\x\<^sub>1. (b, x\<^sub>1) \ R" using A4 by (metis converse_rtranclE)
  thus "\c. (b, c) \ R \ (a, c) \ R\<^sup>*" using A3 by (metis transitive_closure_trans(6))
qed

lemma "\f c = Intg x; \y. f b = Intg y \ y \ x; (a, b) \ R\<^sup>*; (b, c) \ R\<^sup>*\
       \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*"
apply (erule_tac x = b in converse_rtranclE)
 apply metis
by (metis transitive_closure_trans(6))

end

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



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff