(* 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
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
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.
|
