Theory MissingRelation

theory MissingRelation
imports Main
begin

lemma range_dom[simp]:
  "f `` Domain f = Range f"
  "converse f `` Range f = Domain f" by auto

lemma Gr_Image_image[simp]:
  shows "BNF_Def.Gr A f `` B = f ` (A ∩ B)"
  unfolding BNF_Def.Gr_def by auto

definition univalent where "univalent R = (∀ x y z. (x,y)∈ R ∧ (x,z)∈ R ⟶ z = y)"

lemma univalent_right_unique[simp]:
  shows "right_unique (λ x y. (x,y) ∈ R) = univalent R"
        "univalent {(x,y).r x y} = right_unique r"
  unfolding univalent_def right_unique_def by auto

declare univalent_right_unique(1)[pred_set_conv]

lemma univalent_inter[intro]:
  assumes "univalent f_a ∨ univalent f_b"
  shows "univalent (f_a ∩ f_b)"
  using assms unfolding univalent_def by auto

lemma univalent_union[intro]:
  assumes "univalent f_a" "univalent f_b" "Domain f_a ∩ Domain f_b = Domain (f_a ∩ f_b)"
  shows "univalent (f_a ∪ f_b)"
  unfolding univalent_def
proof(clarify,rule ccontr)
  from assms have uni:"univalent (f_a ∩ f_b)" by auto
  fix x y z
  assume a:"(x, y) ∈ f_a ∪ f_b" "(x, z) ∈ f_a ∪ f_b" "z ≠ y"
  show False 
  proof(cases "(x,y) ∈ f_a")
    case True
    hence fb:"(x,z)∈f_b" using a assms[unfolded univalent_def] by auto
    hence "x ∈ (Domain f_a ∩ Domain f_b)" using True by auto
    with assms uni fb True have "z = y" by (metis DomainE IntD1 IntD2 univalent_def)
    with a show False by auto
  next
    case False
    hence fb:"(x,z)∈f_a" "(x,y) ∈ f_b" using a assms[unfolded univalent_def] by auto
    hence "x ∈ (Domain f_a ∩ Domain f_b)" by auto
    with assms uni fb have "z = y" by (metis DomainE IntD1 IntD2 univalent_def)
    with a show False by auto
  qed
qed

lemma Gr_domain[simp]:
  shows "Domain (BNF_Def.Gr A f) = A"
    and "Domain (BNF_Def.Gr A id O R) = A ∩ Domain R" unfolding BNF_Def.Gr_def by auto

lemma in_Gr[simp]:
  shows "(x,y) ∈ BNF_Def.Gr A f ⟷ x ∈ A ∧ f x = y"
  unfolding BNF_Def.Gr_def by auto

lemma Id_on_domain[simp]:
  "Domain (Id_on A O f) = A ∩ Domain f" by auto

lemma Domain_id_on:
  shows "Domain (R O S) = Domain R ∩ R¯ `` Domain S"
  by auto

lemma Id_on_int:
  "Id_on A O f = (A × UNIV) ∩ f" by auto

lemma Domain_int_univ:
  "Domain (A × UNIV ∩ f) = A ∩ Domain f" by auto

lemma Domain_O:
  assumes "a ⊆ Domain x" "x `` a ⊆ Domain y"
  shows "a ⊆ Domain (x O y)"
  proof fix xa assume xa:"xa ∈ a" hence "xa ∈ Domain x" using assms by auto
    then obtain w where xaw:"(xa,w) ∈ x" by auto
    with xa have "w ∈ Domain y" using assms by auto
    then obtain v where "(w,v) ∈ y" by auto
    with xaw have "(xa,v) ∈ x O y" by auto
    thus "xa ∈ Domain (x O y)" by auto qed

lemma fst_UNIV[intro]:
  "A ⊆ fst ` A × UNIV" by force

lemma Gr_range[simp]:
  shows "Range (BNF_Def.Gr A f) = f ` A" unfolding BNF_Def.Gr_def by auto

lemma tuple_disj[simp]:
  shows "{y. y = x ∨ y = z} = {x,z}" by auto

lemma univalent_empty [intro]: "univalent {}" unfolding univalent_def by auto

lemma univalent_char : "univalent R ⟷ converse R O R ⊆ Id"
  unfolding univalent_def by auto

lemma univalentD [dest]: "univalent R ⟹ (x,y)∈ R ⟹ (x,z)∈ R ⟹ z = y"
  unfolding univalent_def by auto

lemma univalentI: "converse R O R ⊆ Id ⟹ univalent R"
  unfolding univalent_def by auto

lemma univalent_composes[intro]:assumes "univalent R" "univalent S"
 shows "univalent (R O S)" using assms unfolding univalent_char by auto

lemma id_univalent[intro]:"univalent (Id_on x)" unfolding univalent_char by auto

lemma univalent_insert:
  assumes "⋀ c. (a,c) ∉ R"
  shows "univalent (insert (a,b) R) ⟷ univalent R"
  using assms unfolding univalent_def by auto

lemma univalent_set_distinctI[intro]: (* not an iff: duplicates of A and B might align *)
  assumes "distinct A"
  shows "univalent (set (zip A B))"
  using assms proof(induct A arbitrary:B)
  case (Cons a A)
  hence univ:"univalent (set (zip A (tl B)))" by auto
  from Cons(2) have "a ∉ set (take x A)" for x using in_set_takeD by fastforce
  hence "a ∉ Domain (set (zip A (tl B)))"
    unfolding Domain_fst set_map[symmetric] map_fst_zip_take by auto
  hence "⋀ c. (a,c) ∉ set (zip A (tl B))" by auto
  from univ univalent_insert[OF this] show ?case by(cases B,auto)
qed auto

lemma set_zip_conv[simp]:
"(set (zip A B))¯ = set (zip B A)" unfolding set_zip by auto

lemma univalent_O_converse[simp]:
  assumes "univalent (converse R)"
  shows "R O converse R = Id_on (Domain R)"
  using assms[unfolded univalent_char] by auto

lemma Image_outside_Domain[simp]:
  assumes "Domain R ∩ A = {}"
  shows "R `` A = {}"
  using assms by auto

lemma Image_Domain[simp]:
  assumes "Domain R = A"
  shows "R `` A = Range R"
  using assms by auto

lemma Domain_set_zip[simp]:
  assumes "length A = length B"
  shows "Domain (set (zip A B)) = set A"
  unfolding Domain_fst set_map[symmetric] map_fst_zip[OF assms]..

lemma Range_set_zip[simp]:
  assumes "length A = length B"
  shows "Range (set (zip A B)) = set B"
  unfolding Range_snd set_map[symmetric] map_snd_zip[OF assms]..

lemma Gr_univalent[intro]:
  shows "univalent (BNF_Def.Gr A f)"
  unfolding BNF_Def.Gr_def univalent_def by auto

lemma univalent_fn[simp]:
  assumes "univalent R"
  shows "BNF_Def.Gr (Domain R) (λ x. SOME y. (x,y) ∈ R) = R" (is "?lhs = _")
  unfolding set_eq_iff
proof(clarify,standard)
  fix a b assume a:"(a, b) ∈ R"
  hence "(a,SOME y. (a, y) ∈ R) ∈ R" using someI by metis
  with assms a have [simp]:"(SOME y. (a, y) ∈ R) = b" by auto
  show "(a, b) ∈ ?lhs" using a by auto
next
  fix a b assume a:"(a,b) ∈ ?lhs"
  hence "a ∈ Domain R" "(SOME y. (a, y) ∈ R) = b" by auto
  thus "(a,b) ∈ R" using someI by auto
qed

lemma Gr_not_in[intro]:
  shows "x ∉ F ∨ f x ≠ y ⟹ (x,y) ∉ BNF_Def.Gr F f" by auto

lemma Gr_insert[simp]:
  shows "BNF_Def.Gr (insert x F) f = insert (x,f x) (BNF_Def.Gr F f)"
  unfolding BNF_Def.Gr_def by auto

lemma Gr_empty[simp]:
  shows "BNF_Def.Gr {} f = {}" by auto

lemma Gr_card[simp]:
  shows "card (BNF_Def.Gr A f) = card A"
proof(cases "finite A")
  case True
  hence "finite (BNF_Def.Gr A f)" by (induct A,auto)
  with True show ?thesis by (induct A,auto)
next
  have [simp]: "infinite (Domain (A - {x})) = infinite (Domain (A::('a × 'b) set))"
    for A x
    using Diff_infinite_finite Domain_Diff_subset finite.emptyI
              finite.insertI finite_Domain finite_subset Diff_subset Domain_mono
    by metis
  have "infinite (Domain A) ⟹ ∃ a. a ∈ fst ` A" for A::"('a × 'b) set"
    using finite.simps unfolding Domain_fst by fastforce
  hence [intro]:"infinite (Domain A) ⟹ ∃ a b. (a,b) ∈ A" for A::"('a × 'b) set"
    by fast
  let ?Gr = "BNF_Def.Gr A f"
  case False
  hence "infinite ?Gr"
    by(intro infinite_coinduct[of "infinite o Domain"],auto)
  with False show ?thesis by (auto simp:BNF_Def.Gr_def)
qed

lemma univalent_finite[simp]:
  assumes "univalent R"
  shows "card (Domain R) = card R"
        "finite (Domain R) ⟷ finite R"
proof -
  let ?R = "BNF_Def.Gr (Domain R) (λ x. SOME y. (x,y) ∈ R)"
  have "card (Domain ?R) = card ?R" by auto
  thus "card (Domain  R) = card  R"
    unfolding univalent_fn[OF assms].
  thus "finite (Domain R) ⟷ finite R"
    by (metis Domain_empty_iff card_0_eq card.infinite finite.emptyI)
qed

lemma trancl_power_least:
  "p ∈ R⇧+ ⟷ (∃n. p ∈ R ^^ Suc n ∧ (p ∈ R ^^ n ⟶ n = 0))"
proof
  assume "p ∈ R⇧+"
  from this[unfolded trancl_power] obtain n where p:"n>0" "p ∈ R ^^ n" by auto
  define n' where "n' = n - 1"
  with p have "Suc n' = n" by auto
  with p have "p ∈ R ^^ Suc n'" by auto
  thus "∃n. p ∈ R ^^ Suc n ∧ (p ∈ R ^^ n ⟶ n = 0)" proof (induct n')
    case 0 hence "p ∈ R ^^ 0 O R ∧ (p ∈ R ^^ 0 ⟶ 0 = 0)" by auto
    then show ?case by force
  next
    case (Suc n)
    show ?case proof(cases "p ∈ R ^^ Suc n")
      case False with Suc show ?thesis by blast
    qed (rule Suc)
  qed next
  assume "∃n. p ∈ R ^^ Suc n ∧ (p ∈ R ^^ n ⟶ n = 0)"
  with zero_less_Suc have "∃n>0. p ∈ R ^^ n" by blast
  thus "p ∈ R⇧+" unfolding trancl_power.
qed

lemma refl_on_tranclI :
  assumes "refl_on A r"
  shows "refl_on A (trancl r)"
  proof
    show "r⇧+ ⊆ A × A"
      by( rule trancl_subset_Sigma
        , auto simp: assms[THEN refl_onD1] assms[THEN refl_onD2])
    show "x ∈ A ⟹ (x, x) ∈ r⇧+" for x
      using assms[THEN refl_onD] by auto
  qed

definition idempotent where
  "idempotent r ≡ r O r = r"

lemma trans_def: "trans r = ((Id ∪ r) O r = r)" "trans r = (r O (Id ∪ r) = r)"
  by(auto simp:trans_def)

lemma idempotent_impl_trans: "idempotent r ⟹ trans r"
  by(auto simp:trans_def idempotent_def)

lemma refl_trans_impl_idempotent[intro]: "refl_on A r ⟹ trans r ⟹ idempotent r"
  by(auto simp:refl_on_def trans_def idempotent_def)

lemma idempotent_subset:
  assumes "idempotent R" "S ⊆ R"
  shows "S O R ⊆ R" "R O S ⊆ R" "S O R O S ⊆ R"
  using assms by (auto simp:idempotent_def)

(* not really about relations, but I need it in GraphRewriting.thy.
   Renaming the entire file to 'preliminaries' just because this is here would be too much. *)
lemma list_sorted_max[simp]:
  shows "sorted list ⟹ list = (x#xs) ⟹ fold max xs x = (last list)"
proof (induct list arbitrary:x xs)
  case (Cons a list) 
  hence "xs = y # ys ⟹ fold max ys y = last xs" "sorted (x # xs)" "sorted xs" for y ys 
    using Cons.prems(1,2) by auto
  hence "xs ≠ [] ⟹ fold max xs x = last xs"
    by (metis fold_simps(2) hd_Cons_tl list.set_intros(1) max.absorb1 sorted_simps(2))
  thus ?case unfolding Cons by auto
qed auto

end