# Theory Trans_Closure

```(*  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 ‹Metis Example Featuring the Transitive Closure›

theory Trans_Closure
imports Main
begin

declare [[metis_new_skolem]]

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⇧*; (b, c) ∈ R⇧*⟧
⟹ ∃c. (b, c) ∈ R ∧ (a, c) ∈ R⇧*"
(* sledgehammer *)
proof -
assume A1: "f c = Intg x"
assume A2: "∀y. f b = Intg y ⟶ y ≠ x"
assume A3: "(a, b) ∈ R⇧*"
assume A4: "(b, c) ∈ R⇧*"
have F1: "f c ≠ f b" using A2 A1 by metis
have F2: "∀u. (b, u) ∈ R ⟶ (a, u) ∈ R⇧*" 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⇧*" using F2 by metis
qed

lemma "⟦f c = Intg x; ∀y. f b = Intg y ⟶ y ≠ x; (a, b) ∈ R⇧*; (b,c) ∈ R⇧*⟧
⟹ ∃c. (b, c) ∈ R ∧ (a, c) ∈ R⇧*"
(* 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⇧*"
assume A4: "(b, c) ∈ R⇧*"
have "b ≠ c" using A1 A2 by metis
hence "∃x⇩1. (b, x⇩1) ∈ R" using A4 by (metis converse_rtranclE)
thus "∃c. (b, c) ∈ R ∧ (a, c) ∈ R⇧*" using A3 by (metis transitive_closure_trans(6))
qed

lemma "⟦f c = Intg x; ∀y. f b = Intg y ⟶ y ≠ x; (a, b) ∈ R⇧*; (b, c) ∈ R⇧*⟧
⟹ ∃c. (b, c) ∈ R ∧ (a, c) ∈ R⇧*"
apply (erule_tac x = b in converse_rtranclE)
apply metis
by (metis transitive_closure_trans(6))

end
```