Quelle Trans_Closure.thy Sprache: 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

quality100%

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