Theory Relation_Closure

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
License: LGPL (see file COPYING.LESSER)
*)
chapter ‹Closure-Operations on Relations›

theory Relation_Closure
  imports "Abstract-Rewriting.Relative_Rewriting"
begin

locale rel_closure =
  fixes cop :: "'b ⇒ 'a ⇒ 'a" ― ‹closure operator›
    and nil :: "'b"
    and add :: "'b ⇒ 'b ⇒ 'b"
  assumes cop_nil: "cop nil x = x"
  assumes cop_add: "cop (add a b) x = cop a (cop b x)"
begin

inductive_set closure for r :: "'a rel"
  where
    [intro]: "(x, y) ∈ r ⟹ (cop a x, cop a y) ∈ closure r"

lemma closureI2: "(x, y) ∈ r ⟹ u = cop a x ⟹ v = cop a y ⟹ (u, v) ∈ closure r" by auto

lemma closure_mono: "r ⊆ s ⟹ closure r ⊆ closure s" by (auto elim: closure.cases)

lemma subset_closure: "r ⊆ closure r"
  using closure.intros [where a = nil] by (auto simp: cop_nil)

definition "closed r ⟷ closure r ⊆ r"

lemma closure_subset: "closed r ⟹ closure r ⊆ r"
  by (auto simp: closed_def)

lemma closedI [Pure.intro, intro]: "(⋀x y a. (x, y) ∈ r ⟹ (cop a x, cop a y) ∈ r) ⟹ closed r"
  by (auto simp: closed_def elim: closure.cases)

lemma closedD [dest]: "closed r ⟹ (x, y) ∈ r ⟹ (cop a x, cop a y) ∈ r"
  by (auto simp: closed_def)

lemma closed_closure [intro]: "closed (closure r)"
  using closure.intros [where a = "add a b" for a b]
  by (auto simp: closed_def cop_add elim!: closure.cases)

lemma subset_closure_Un:
  "closure r ⊆ closure (r ∪ s)"
  "closure s ⊆ closure (r ∪ s)"
  by (auto elim!: closure.cases)

lemma closure_Un: "closure (r ∪ s) = closure r ∪ closure s"
  using subset_closure_Un by (auto elim: closure.cases)

lemma closure_id [simp]: "closed r ⟹ closure r = r"
  using subset_closure and closure_subset by blast

lemma closed_Un [intro]: "closed r ⟹ closed s ⟹ closed (r ∪ s)" by blast

lemma closed_Inr [intro]: "closed r ⟹ closed s ⟹ closed (r ∩ s)" by blast

lemma closed_rtrancl [intro]: "closed r ⟹ closed (r⇧*)"
  by (best intro: rtrancl_into_rtrancl elim: rtrancl.induct)

lemma closed_trancl [intro]: "closed r ⟹ closed (r⇧+)"
  by (best intro: trancl_into_trancl elim: trancl.induct)

lemma closed_converse [intro]: "closed r ⟹ closed (r¯)" by blast

lemma closed_comp [intro]: "closed r ⟹ closed s ⟹ closed (r O s)" by blast

lemma closed_relpow [intro]: "closed r ⟹ closed (r ^^ n)"
  by (auto intro: relpow_image [OF closedD])

lemma closed_conversion [intro]: "closed r ⟹ closed (r⇧↔⇧*)"
  by (auto simp: conversion_def)

lemma closed_relto [intro]: "closed r ⟹ closed s ⟹ closed (relto r s)" by blast

lemma closure_diff_subset: "closure r - closure s ⊆ closure (r - s)" by (auto elim: closure.cases)

end

end