(* 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. *) header {* Metis Example Featuring the Transitive Closure *} theory Trans_Closure imports Main begin declare [[metis_new_skolemizer]] type_synonym addr = nat datatype val = Unit -- "dummy result value of void expressions" | Null -- "null reference" | Bool bool -- "Boolean value" | Intg int -- "integer value" | Addr addr -- "addresses of objects in the heap" 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>*\ \ \c. (b, c) \ R \ (a, c) \ 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>*\ \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" (* sledgehammer [isar_proof, isar_shrink_factor = 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\<^isub>1. (b, x\<^isub>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>*\ \ \c. (b, c) \ R \ (a, c) \ R\<^sup>*" apply (erule_tac x = b in converse_rtranclE) apply metis by (metis transitive_closure_trans(6)) end