Theory Transitive_Closure_Ext

(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
section ‹Transitive Closures›
theory Transitive_Closure_Ext
  imports "HOL-Library.FuncSet"
begin

(*** Basic Properties *******************************************************)

subsection ‹Basic Properties›

text ‹
  @{text "R⇧⁺⇧⁺"} is a transitive closure of a relation @{text R}.
  @{text "R⇧^*⇧^*"} is a reflexive transitive closure of a relation @{text R}.›

text ‹
  A function @{text f} is surjective on @{text "R⇧⁺⇧⁺"} iff for any
  two elements in the range of @{text f}, related through @{text "R⇧⁺⇧⁺"},
  all their intermediate elements belong to the range of @{text f}.›

abbreviation "surj_on_trancl R f ≡
  (∀x y z. R⇧⁺⇧⁺ (f x) y ⟶ R y (f z) ⟶ y ∈ range f)"

text ‹
  A function @{text f} is bijective on @{text "R⇧⁺⇧⁺"} iff
  it is injective and surjective on @{text "R⇧⁺⇧⁺"}.›

abbreviation "bij_on_trancl R f ≡ inj f ∧ surj_on_trancl R f"

(*** Helper Lemmas **********************************************************)

subsection ‹Helper Lemmas›

lemma rtranclp_eq_rtranclp [iff]:
  "(λx y. P x y ∨ x = y)⇧^*⇧^* = P⇧^*⇧^*"
proof (intro ext iffI)
  fix x y
  have "(λx y. P x y ∨ x = y)⇧^*⇧^* x y ⟶ P⇧⁼⇧⁼⇧^*⇧^* x y"
    by (rule mono_rtranclp) simp
  thus "(λx y. P x y ∨ x = y)⇧^*⇧^* x y ⟹ P⇧^*⇧^* x y"
    by simp
  show "P⇧^*⇧^* x y ⟹ (λx y. P x y ∨ x = y)⇧^*⇧^* x y"
    by (metis (no_types, lifting) mono_rtranclp)
qed

lemma tranclp_eq_rtranclp [iff]:
  "(λx y. P x y ∨ x = y)⇧⁺⇧⁺ = P⇧^*⇧^*"
proof (intro ext iffI)
  fix x y
  have "(λx y. P x y ∨ x = y)⇧^*⇧^* x y ⟶ P⇧⁼⇧⁼⇧^*⇧^* x y"
    by (rule mono_rtranclp) simp
  thus "(λx y. P x y ∨ x = y)⇧⁺⇧⁺ x y ⟹ P⇧^*⇧^* x y"
    using tranclp_into_rtranclp by force
  show "P⇧^*⇧^* x y ⟹ (λx y. P x y ∨ x = y)⇧⁺⇧⁺ x y"
    by (metis (mono_tags, lifting) mono_rtranclp rtranclpD tranclp.r_into_trancl)
qed

lemma rtranclp_eq_rtranclp' [iff]:
  "(λx y. P x y ∧ x ≠ y)⇧^*⇧^* = P⇧^*⇧^*"
proof (intro ext iffI)
  fix x y
  show "(λx y. P x y ∧ x ≠ y)⇧^*⇧^* x y ⟹ P⇧^*⇧^* x y"
    by (metis (no_types, lifting) mono_rtranclp)
  assume "P⇧^*⇧^* x y"
  hence "(inf P (≠))⇧^*⇧^* x y"
    by (simp add: rtranclp_r_diff_Id)
  also have "(inf P (≠))⇧^*⇧^* x y ⟶ (λx y. P x y ∧ x ≠ y)⇧^*⇧^* x y"
    by (rule mono_rtranclp) simp
  finally show "P⇧^*⇧^* x y ⟹ (λx y. P x y ∧ x ≠ y)⇧^*⇧^* x y" by simp
qed

lemma tranclp_tranclp_to_tranclp_r:
  assumes "(⋀x y z. R⇧⁺⇧⁺ x y ⟹ R y z ⟹ P x ⟹ P z ⟹ P y)"
  assumes "R⇧⁺⇧⁺ x y" and "R⇧⁺⇧⁺ y z"
  assumes "P x" and "P z"
  shows "P y"
proof -
  have "(⋀x y z. R⇧⁺⇧⁺ x y ⟹ R y z ⟹ P x ⟹ P z ⟹ P y) ⟹
         R⇧⁺⇧⁺ y z ⟹ R⇧⁺⇧⁺ x y ⟹ P x ⟶ P z ⟶ P y"
    by (erule tranclp_induct, auto) (meson tranclp_trans)
  thus ?thesis using assms by auto
qed

(*** Transitive Closure Preservation & Reflection ***************************)

subsection ‹Transitive Closure Preservation›

text ‹
  A function @{text f} preserves @{text "R⇧⁺⇧⁺"} if it preserves @{text R}.›

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/52573551/632199"}
  and provided with the permission of the author of the answer.›

lemma preserve_tranclp:
  assumes "⋀x y. R x y ⟹ S (f x) (f y)"
  assumes "R⇧⁺⇧⁺ x y"
  shows "S⇧⁺⇧⁺ (f x) (f y)"
proof -
  define P where P: "P = (λx y. S⇧⁺⇧⁺ (f x) (f y))" 
  define r where r: "r = (λx y. S (f x) (f y))"
  have "r⇧⁺⇧⁺ x y" by (insert assms r; erule tranclp_trans_induct; auto)
  moreover have "⋀x y. r x y ⟹ P x y" unfolding P r by simp
  moreover have "⋀x y z. r⇧⁺⇧⁺ x y ⟹ P x y ⟹ r⇧⁺⇧⁺ y z ⟹ P y z ⟹ P x z"
    unfolding P by auto
  ultimately have "P x y" by (rule tranclp_trans_induct)
  with P show ?thesis by simp
qed

text ‹
  A function @{text f} preserves @{text "R⇧^*⇧^*"} if it preserves @{text R}.›

lemma preserve_rtranclp:
  "(⋀x y. R x y ⟹ S (f x) (f y)) ⟹
   R⇧^*⇧^* x y ⟹ S⇧^*⇧^* (f x) (f y)"
  unfolding Nitpick.rtranclp_unfold
  by (metis preserve_tranclp)

text ‹
  If one needs to prove that @{text "(f x)"} and @{text "(g y)"}
  are related through @{text "S⇧^*⇧^*"} then one can use the previous
  lemma and add a one more step from @{text "(f y)"} to @{text "(g y)"}.›

lemma preserve_rtranclp':
  "(⋀x y. R x y ⟹ S (f x) (f y)) ⟹
   (⋀y. S (f y) (g y)) ⟹
   R⇧^*⇧^* x y ⟹ S⇧^*⇧^* (f x) (g y)"
  by (metis preserve_rtranclp rtranclp.rtrancl_into_rtrancl)

lemma preserve_rtranclp'':
  "(⋀x y. R x y ⟹ S (f x) (f y)) ⟹
   (⋀y. S (f y) (g y)) ⟹
   R⇧^*⇧^* x y ⟹ S⇧⁺⇧⁺ (f x) (g y)"
  apply (rule_tac ?b="f y" in rtranclp_into_tranclp1, auto)
  by (rule preserve_rtranclp, auto)

subsection ‹Transitive Closure Reflection›

text ‹
  A function @{text f} reflects @{text "S⇧⁺⇧⁺"} if it reflects
  @{text S} and is bijective on @{text "S⇧⁺⇧⁺"}.›

text ‹
  The proof was derived from the accepted answer on the website
  Stack Overflow that is available at
  @{url "https://stackoverflow.com/a/52573551/632199"}
  and provided with the permission of the author of the answer.›

lemma reflect_tranclp:
  assumes refl_f: "⋀x y. S (f x) (f y) ⟹ R x y"
  assumes bij_f: "bij_on_trancl S f"
  assumes prem: "S⇧⁺⇧⁺ (f x) (f y)"
  shows "R⇧⁺⇧⁺ x y"
proof -
  define B where B: "B = range f"
  define g where g: "g = the_inv_into UNIV f"
  define gr where gr: "gr = restrict g B"
  define P where P: "P = (λx y. x ∈ B ⟶ y ∈ B ⟶ R⇧⁺⇧⁺ (gr x) (gr y))"
  from prem have major: "S⇧⁺⇧⁺ (f x) (f y)" by blast
  from refl_f bij_f have cases_1: "⋀x y. S x y ⟹ P x y"
    unfolding B P g gr
    by (simp add: f_the_inv_into_f tranclp.r_into_trancl)
  from refl_f bij_f
  have "(⋀x y z. S⇧⁺⇧⁺ x y ⟹ S⇧⁺⇧⁺ y z ⟹ x ∈ B ⟹ z ∈ B ⟹ y ∈ B)"
    unfolding B
    by (rule_tac ?z="z" in tranclp_tranclp_to_tranclp_r, auto, blast)
  with P have cases_2:
    "⋀x y z. S⇧⁺⇧⁺ x y ⟹ P x y ⟹ S⇧⁺⇧⁺ y z ⟹ P y z ⟹ P x z"
    unfolding B
    by auto
  from major cases_1 cases_2 have "P (f x) (f y)"
    by (rule tranclp_trans_induct)
  with bij_f show ?thesis unfolding P B g gr by (simp add: the_inv_f_f)
qed

text ‹
  A function @{text f} reflects @{text "S⇧^*⇧^*"} if it reflects
  @{text S} and is bijective on @{text "S⇧⁺⇧⁺"}.›

lemma reflect_rtranclp:
  "(⋀x y. S (f x) (f y) ⟹ R x y) ⟹
   bij_on_trancl S f ⟹
   S⇧^*⇧^* (f x) (f y) ⟹ R⇧^*⇧^* x y"
  unfolding Nitpick.rtranclp_unfold
  by (metis (full_types) injD reflect_tranclp)

end