(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
(* TODO: There are a lot of similar lemmas in the theory.
         They should be generalized *)
section ‹Tuples›
theory Tuple
  imports Finite_Map_Ext Transitive_Closure_Ext
begin

subsection ‹Definitions›

abbreviation "subtuple f xm ym ≡ fmrel_on_fset (fmdom ym) f xm ym"

abbreviation "strict_subtuple f xm ym ≡ subtuple f xm ym ∧ xm ≠ ym"

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

subsection ‹Helper Lemmas›

lemma fmrel_to_subtuple:
  "fmrel r xm ym ==> subtuple r xm ym"
  unfolding fmrel_on_fset_fmrel_restrict by blast

lemma subtuple_eq_fmrel_fmrestrict_fset:
  "subtuple r xm ym = fmrel r (fmrestrict_fset (fmdom ym) xm) ym"
  by (simp add: fmrel_on_fset_fmrel_restrict)

lemma subtuple_fmdom:
  "subtuple f xm ym ==>
   subtuple g ym xm ==>
   fmdom xm = fmdom ym"
  by (meson fmrel_on_fset_fmdom fset_eqI)

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

subsection ‹Basic Properties›

lemma subtuple_refl:
  "reflp R ==> subtuple R xm xm"
  by (simp add: fmrel_on_fsetI option.rel_reflp reflpD)

lemma subtuple_mono [mono]:
  "(∧x y. x ∈ fmran' xm ==> y ∈ fmran' ym ==> f x y ⟶ g x y) ==>
   subtuple f xm ym ⟶ subtuple g xm ym"
  apply (auto)
  apply (rule fmrel_on_fsetI)
  apply (drule_tac ?P="f" and ?m="xm" and ?n="ym" in fmrel_on_fsetD, simp)
  apply (erule option.rel_cases, simp)
  by (auto simp add: option.rel_sel fmran'I)

lemma strict_subtuple_mono [mono]:
  "(∧x y. x ∈ fmran' xm ==> y ∈ fmran' ym ==> f x y ⟶ g x y) ==>
   strict_subtuple f xm ym ⟶ strict_subtuple g xm ym"
  using subtuple_mono by blast

lemma subtuple_antisym:
  assumes "subtuple (λx y. f x y ∨ x = y) xm ym"
  assumes "subtuple (λx y. f x y ∧ ¬ f y x ∨ x = y) ym xm"
  shows "xm = ym"
proof (rule fmap_ext)
  fix x
  from assms have "fmdom xm = fmdom ym"
    using subtuple_fmdom by blast
  with assms have "fmrel (λx y. f x y ∨ x = y) xm ym"
      and "fmrel (λx y. f x y ∧ ¬ f y x ∨ x = y) ym xm"
    by (metis (mono_tags, lifting) fmrel_code fmrel_on_fset_alt_def)+
  thus "fmlookup xm x = fmlookup ym x"
    apply (erule_tac ?x="x" in fmrel_cases)
    by (erule_tac ?x="x" in fmrel_cases, auto)+
qed

lemma strict_subtuple_antisym:
  "strict_subtuple (λx y. f x y ∨ x = y) xm ym ==>
   strict_subtuple (λx y. f x y ∧ ¬ f y x ∨ x = y) ym xm ==> False"
  by (auto simp add: subtuple_antisym)

lemma subtuple_acyclic:
  assumes "acyclicP_on (fmran' xm) P"
  assumes "subtuple (λx y. P x y ∨ x = y)⁺⁺ xm ym"
  assumes "subtuple (λx y. P x y ∨ x = y) ym xm"
  shows "xm = ym"
proof (rule fmap_ext)
  fix x
  from assms have fmdom_eq: "fmdom xm = fmdom ym"
    using subtuple_fmdom by blast
  have "∧x a b. acyclicP_on (fmran' xm) P ==>
     fmlookup xm x = Some a ==>
     fmlookup ym x = Some b ==>
    P^** a b ==> P b a ∨ a = b ==> a = b"
    by (meson Nitpick.tranclp_unfold fmran'I rtranclp_into_tranclp1)
  moreover from fmdom_eq assms(2) have "fmrel P^** xm ym"
    unfolding fmrel_on_fset_fmrel_restrict apply auto
    by (metis fmrestrict_fset_dom)
  moreover from fmdom_eq assms(3) have "fmrel (λx y. P x y ∨ x = y) ym xm"
    unfolding fmrel_on_fset_fmrel_restrict apply auto
    by (metis fmrestrict_fset_dom)
  ultimately show "fmlookup xm x = fmlookup ym x"
    apply (erule_tac ?x="x" in fmrel_cases)
    apply (erule_tac ?x="x" in fmrel_cases, simp_all)+
    using assms(1) by blast
qed

lemma subtuple_acyclic':
  assumes "acyclicP_on (fmran' ym) P"
  assumes "subtuple (λx y. P x y ∨ x = y)⁺⁺ xm ym"
  assumes "subtuple (λx y. P x y ∨ x = y) ym xm"
  shows "xm = ym"
proof (rule fmap_ext)
  fix x
  from assms have fmdom_eq: "fmdom xm = fmdom ym"
    using subtuple_fmdom by blast
  have "∧x a b. acyclicP_on (fmran' ym) P ==>
     fmlookup xm x = Some a ==>
     fmlookup ym x = Some b ==>
    P^** a b ==> P b a ∨ a = b ==> a = b"
    by (meson Nitpick.tranclp_unfold fmran'I rtranclp_into_tranclp2)
  moreover from fmdom_eq assms(2) have "fmrel P^** xm ym"
    unfolding fmrel_on_fset_fmrel_restrict apply auto
    by (metis fmrestrict_fset_dom)
  moreover from fmdom_eq assms(3) have "fmrel (λx y. P x y ∨ x = y) ym xm"
    unfolding fmrel_on_fset_fmrel_restrict apply auto
    by (metis fmrestrict_fset_dom)
  ultimately show "fmlookup xm x = fmlookup ym x"
    apply (erule_tac ?x="x" in fmrel_cases)
    apply (erule_tac ?x="x" in fmrel_cases, simp_all)+
    using assms(1) by blast
qed

lemma subtuple_acyclic'':
  "acyclicP_on (fmran' ym) R ==>
   subtuple R^** xm ym ==>
   subtuple R ym xm ==>
   xm = ym"
  by (metis (no_types, lifting) subtuple_acyclic' subtuple_mono tranclp_eq_rtranclp)

lemma strict_subtuple_trans:
  "acyclicP_on (fmran' xm) P ==>
   strict_subtuple (λx y. P x y ∨ x = y)⁺⁺ xm ym ==>
   strict_subtuple (λx y. P x y ∨ x = y) ym zm ==>
   strict_subtuple (λx y. P x y ∨ x = y)⁺⁺ xm zm"
  apply auto
  apply (rule fmrel_on_fset_trans, auto)
  by (drule_tac ?ym="ym" in subtuple_acyclic; auto)

lemma strict_subtuple_trans':
  "acyclicP_on (fmran' zm) P ==>
   strict_subtuple (λx y. P x y ∨ x = y) xm ym ==>
   strict_subtuple (λx y. P x y ∨ x = y)⁺⁺ ym zm ==>
   strict_subtuple (λx y. P x y ∨ x = y)⁺⁺ xm zm"
  apply auto
  apply (rule fmrel_on_fset_trans, auto)
  by (drule_tac ?xm="ym" in subtuple_acyclic'; auto)

lemma strict_subtuple_trans'':
  "acyclicP_on (fmran' zm) R ==>
   strict_subtuple R xm ym ==>
   strict_subtuple R^** ym zm ==>
   strict_subtuple R^** xm zm"
  apply auto
  apply (rule fmrel_on_fset_trans, auto)
  by (drule_tac ?xm="ym" in subtuple_acyclic''; auto)

lemma strict_subtuple_trans''':
  "acyclicP_on (fmran' zm) P ==>
   strict_subtuple (λx y. P x y ∨ x = y) xm ym ==>
   strict_subtuple (λx y. P x y ∨ x = y)^** ym zm ==>
   strict_subtuple (λx y. P x y ∨ x = y)^** xm zm"
  apply auto
  apply (rule fmrel_on_fset_trans, auto)
  by (drule_tac ?xm="ym" in subtuple_acyclic'; auto)

lemma subtuple_fmmerge2 [intro]:
  "(∧x y. x ∈ fmran' xm ==> f x (g x y)) ==>
   subtuple f xm (fmmerge g xm ym)"
  by (rule_tac ?S="fmdom ym" in fmrel_on_fsubset; auto)

(*** Transitive Closures ****************************************************)

subsection ‹Transitive Closures›

lemma trancl_to_subtuple:
  "(subtuple r)⁺⁺ xm ym ==>
   subtuple r⁺⁺ xm ym"
  apply (induct rule: tranclp_induct)
  apply (metis subtuple_mono tranclp.r_into_trancl)
  by (rule fmrel_on_fset_trans; auto)

lemma rtrancl_to_subtuple:
  "(subtuple r)^** xm ym ==>
   subtuple r^** xm ym"
  apply (induct rule: rtranclp_induct)
  apply (simp add: fmap.rel_refl_strong fmrel_to_subtuple)
  by (rule fmrel_on_fset_trans; auto)

lemma fmrel_to_subtuple_trancl:
  "reflp r ==>
   (fmrel r)⁺⁺ (fmrestrict_fset (fmdom ym) xm) ym ==>
   (subtuple r)⁺⁺ xm ym"
  apply (frule trancl_to_fmrel)
  apply (rule_tac ?r="r" in fmrel_tranclp_induct, auto)
  apply (metis (no_types, lifting) fmrel_fmdom_eq
          subtuple_eq_fmrel_fmrestrict_fset tranclp.r_into_trancl)
  by (meson fmrel_to_subtuple tranclp.simps)

lemma subtuple_to_trancl:
  "reflp r ==>
   subtuple r⁺⁺ xm ym ==>
   (subtuple r)⁺⁺ xm ym"
  apply (rule fmrel_to_subtuple_trancl)
  unfolding fmrel_on_fset_fmrel_restrict
  by (simp_all add: fmrel_to_trancl)

lemma trancl_to_strict_subtuple:
  "acyclicP_on (fmran' ym) R ==>
   (strict_subtuple R)⁺⁺ xm ym ==>
   strict_subtuple R^** xm ym"
  apply (erule converse_tranclp_induct)
  apply (metis r_into_rtranclp strict_subtuple_mono)
  using strict_subtuple_trans'' by blast

lemma trancl_to_strict_subtuple':
  "acyclicP_on (fmran' ym) R ==>
   (strict_subtuple (λx y. R x y ∨ x = y))⁺⁺ xm ym ==>
   strict_subtuple (λx y. R x y ∨ x = y)^** xm ym"
  apply (erule converse_tranclp_induct)
  apply (metis (no_types, lifting) r_into_rtranclp strict_subtuple_mono)
  using strict_subtuple_trans''' by blast

lemma subtuple_rtranclp_intro:
  assumes "∧xm ym. R (f xm) (f ym) ==> subtuple R xm ym"
      and "bij_on_trancl R f"
      and "R^** (f xm) (f ym)"
    shows "subtuple R^** xm ym"
proof -
  have "(λxm ym. R (f xm) (f ym))^** xm ym"
    apply (insert assms(2) assms(3))
    by (rule reflect_rtranclp; auto)
  with assms(1) have "(subtuple R)^** xm ym"
    by (metis (mono_tags, lifting) mono_rtranclp)
  hence "subtuple R^** xm ym"
    by (rule rtrancl_to_subtuple)
  thus ?thesis by simp
qed

lemma strict_subtuple_rtranclp_intro:
  assumes "∧xm ym. R (f xm) (f ym) ==>
           strict_subtuple (λx y. R x y ∨ x = y) xm ym"
      and "bij_on_trancl R f"
      and "acyclicP_on (fmran' ym) R"
      and "R⁺⁺ (f xm) (f ym)"
    shows "strict_subtuple R^** xm ym"
proof -
  have "(λxm ym. R (f xm) (f ym))⁺⁺ xm ym"
    apply (insert assms(1) assms(2) assms(4))
    by (rule reflect_tranclp; auto)
  hence "(strict_subtuple (λx y. R x y ∨ x = y))⁺⁺ xm ym"
    by (rule tranclp_trans_induct;
        auto simp add: assms(1) tranclp.r_into_trancl)
  with assms(3) have "strict_subtuple (λx y. R x y ∨ x = y)^** xm ym"
    by (rule trancl_to_strict_subtuple')
  thus ?thesis by simp
qed

(*** Code Setup *************************************************************)

subsection ‹Code Setup›

abbreviation "subtuple_fun f xm ym ≡
  fBall (fmdom ym) (λx. rel_option f (fmlookup xm x) (fmlookup ym x))"

abbreviation "strict_subtuple_fun f xm ym ≡
  subtuple_fun f xm ym ∧ xm ≠ ym"

lemma subtuple_fun_simp [code_abbrev, simp]:
  "subtuple_fun f xm ym = subtuple f xm ym"
  by (simp add: fmrel_on_fset_alt_def)

lemma strict_subtuple_fun_simp [code_abbrev, simp]:
  "strict_subtuple_fun f xm ym = strict_subtuple f xm ym"
  by simp

end