# Theory Tuple

```(*  Title:       Safe OCL
Author:      Denis Nikiforov, March 2019
Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
*)
(* 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
```