Theory AutoCorres2.Distinct_Prop

(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section "Distinct Proposition"

theory Distinct_Prop  (* part of non-AFP Word_Lib *)
imports
  Word_Lib.Many_More
  "HOL-Library.Prefix_Order"
begin

primrec
  distinct_prop :: "('a ⇒ 'a ⇒ bool) ⇒ ('a list ⇒ bool)"
where
  "distinct_prop P [] = True"
| "distinct_prop P (x # xs) = ((∀y∈set xs. P x y) ∧ distinct_prop P xs)"

primrec
  distinct_sets :: "'a set list ⇒ bool"
where
  "distinct_sets [] = True"
| "distinct_sets (x#xs) = (x ∩ ⋃ (set xs) = {} ∧ distinct_sets xs)"


lemma distinct_prop_map:
  "distinct_prop P (map f xs) = distinct_prop (λx y. P (f x) (f y)) xs"
  by (induct xs) auto

lemma distinct_prop_append:
  "distinct_prop P (xs @ ys) =
    (distinct_prop P xs ∧ distinct_prop P ys ∧ (∀x ∈ set xs. ∀y ∈ set ys. P x y))"
  by (induct xs arbitrary: ys) (auto simp: conj_comms ball_Un)

lemma distinct_prop_distinct:
  "⟦ distinct xs; ⋀x y. ⟦ x ∈ set xs; y ∈ set xs; x ≠ y ⟧ ⟹ P x y ⟧ ⟹ distinct_prop P xs"
  by (induct xs) auto

lemma distinct_prop_True [simp]:
  "distinct_prop (λx y. True) xs"
  by (induct xs, auto)


lemma distinct_prefix:
  "⟦ distinct xs; ys ≤ xs ⟧ ⟹ distinct ys"
  apply (induct xs arbitrary: ys; clarsimp)
  subgoal for a xs ys
    apply (cases ys; clarsimp)
    by (fastforce simp: less_eq_list_def dest: set_mono_prefix)
  done

lemma distinct_sets_prop:
  "distinct_sets xs = distinct_prop (λx y. x ∩ y = {}) xs"
  by (induct xs) auto

lemma distinct_take_strg:
  "distinct xs ⟶ distinct (take n xs)"
  by simp

lemma distinct_prop_prefixE:
  "⟦ distinct_prop P ys; prefix xs ys ⟧ ⟹ distinct_prop P xs"
  apply (induct xs arbitrary: ys; clarsimp)
  subgoal for a xs ys
    apply (cases ys; clarsimp)
    by (fastforce dest: set_mono_prefix)
  done

lemma distinct_sets_union_sub:
  "⟦x ∈ A; distinct_sets [A,B]⟧ ⟹ A ∪ B - {x} = A - {x} ∪ B"
  by (auto simp: distinct_sets_def)

lemma distinct_sets_append:
  "distinct_sets (xs @ ys) ⟹ distinct_sets xs ∧ distinct_sets ys"
  apply (subst distinct_sets_prop)+
  apply (subst (asm) distinct_sets_prop)
  apply (subst (asm) distinct_prop_append)
  apply clarsimp
  done

lemma distinct_sets_append1:
  "distinct_sets (xs @ ys) ⟹ distinct_sets xs"
  by (drule distinct_sets_append, simp)

lemma distinct_sets_append2:
  "distinct_sets (xs @ ys) ⟹ distinct_sets ys"
  by (drule distinct_sets_append, simp)

lemma distinct_sets_append_Cons:
  "distinct_sets (xs @ a # ys) ⟹ distinct_sets (xs @ ys)"
  apply (subst distinct_sets_prop)+
  apply (subst (asm) distinct_sets_prop)
  apply (subst distinct_prop_append)
  apply (subst (asm) distinct_prop_append)
  apply clarsimp
  done

lemma distinct_sets_append_Cons_disjoint:
  "distinct_sets (xs @ a # ys) ⟹  a ∩ ⋃ (set xs) = {} "
  apply (subst (asm) distinct_sets_prop)
  apply (subst (asm) distinct_prop_append)
  apply (subst Int_commute)
  apply (subst Union_disjoint)
  apply clarsimp
  done

lemma distinct_prop_take:
  "⟦distinct_prop P xs; i < length xs⟧ ⟹ distinct_prop P (take i xs)"
  by (metis take_is_prefix distinct_prop_prefixE)

lemma distinct_sets_take:
  "⟦distinct_sets xs; i < length xs⟧ ⟹ distinct_sets (take i xs)"
  by (simp add: distinct_sets_prop distinct_prop_take)

lemma distinct_prop_take_Suc:
  "⟦distinct_prop P xs; i < length xs⟧ ⟹ distinct_prop P (take (Suc i) xs)"
  by (metis distinct_prop_take not_less take_all)

lemma distinct_sets_take_Suc:
  "⟦distinct_sets xs; i < length xs⟧ ⟹ distinct_sets (take (Suc i) xs)"
  by (simp add: distinct_sets_prop distinct_prop_take_Suc)

lemma distinct_prop_rev:
  "distinct_prop P (rev xs) = distinct_prop (λy x. P x y) xs"
  by (induct xs) (auto simp: distinct_prop_append)

lemma distinct_sets_rev [simp]:
  "distinct_sets (rev xs) = distinct_sets xs"
  apply (unfold distinct_sets_prop)
  apply (subst distinct_prop_rev)
  apply (subst Int_commute)
  apply clarsimp
  done

lemma distinct_sets_drop:
  "⟦distinct_sets xs; i < length xs⟧ ⟹ distinct_sets (drop i xs)"
  apply (cases "i=0", simp)
  apply (subst distinct_sets_rev [symmetric])
  apply (subst rev_drop)
  apply (subst distinct_sets_take, simp_all)
  done

lemma distinct_sets_drop_Suc:
  "⟦distinct_sets xs; i < length xs⟧ ⟹ distinct_sets (drop (Suc i) xs)"
  apply (subst distinct_sets_rev [symmetric])
  apply (subst rev_drop)
  apply (subst distinct_sets_take, simp_all)
  done

lemma distinct_sets_take_nth:
  "⟦distinct_sets xs; i < length xs; x ∈ set (take i xs)⟧ ⟹ x ∩ xs ! i = {}"
  apply (drule (1) distinct_sets_take_Suc)
  apply (subst (asm) take_Suc_conv_app_nth, assumption)
  apply (unfold distinct_sets_prop)
  apply (subst (asm) distinct_prop_append)
  apply clarsimp
  done

lemma distinct_sets_drop_nth:
  "⟦distinct_sets xs; i < length xs; x ∈ set (drop (Suc i) xs)⟧ ⟹ x ∩ xs ! i = {}"
  apply (drule (1) distinct_sets_drop)
  apply (subst (asm) drop_Suc_nth, assumption)
  apply fastforce
  done

lemma distinct_sets_append_distinct:
  "⟦x ∈ set xs; y ∈ set ys; distinct_sets (xs @ ys)⟧ ⟹ x ∩ y = {}"
  unfolding distinct_sets_prop by (clarsimp simp: distinct_prop_append)

lemma distinct_sets_update:
 "⟦a ⊆ xs ! i; distinct_sets xs; i < length xs⟧ ⟹ distinct_sets (xs[i := a])"
  apply (subst distinct_sets_prop)
  apply (subst (asm) distinct_sets_prop)
  apply (subst upd_conv_take_nth_drop, simp)
  apply (subst distinct_prop_append)
  apply (intro conjI)
    apply (erule (1) distinct_prop_take)
   apply (rule conjI|clarsimp)+
    apply (fold distinct_sets_prop)
    apply (drule (1) distinct_sets_drop)
    apply (subst (asm) drop_Suc_nth, assumption)
    apply fastforce
   apply (drule (1) distinct_sets_drop)
   apply (subst (asm) drop_Suc_nth, assumption)
   apply clarsimp
  apply clarsimp
  apply (rule conjI)
   apply (drule (2) distinct_sets_take_nth)
   apply blast
  apply clarsimp
  apply (thin_tac "P ⊆ Q" for P Q)
  apply (subst (asm) id_take_nth_drop, assumption)
  apply (drule distinct_sets_append_Cons)
  apply (erule (2) distinct_sets_append_distinct)
  done

lemma distinct_sets_map_update:
  "⟦distinct_sets (map f xs); i < length xs; f a ⊆ f(xs ! i)⟧
  ⟹ distinct_sets (map f (xs[i := a]))"
  by (metis distinct_sets_update length_map map_update nth_map)

lemma Union_list_update:
  "⟦i < length xs; distinct_sets (map f xs)⟧
  ⟹ (⋃x∈set (xs [i := a]). f x) = (⋃x∈set xs. f x) - f (xs ! i) ∪ f a"
  apply (induct xs arbitrary: i; clarsimp)
  subgoal for x xs i
    apply (cases i; (clarsimp, fastforce))
    done
  done

lemma fst_enumerate:
  "i < length xs ⟹ fst (enumerate n xs ! i) = i + n"
  by (metis add.commute fst_conv nth_enumerate_eq)

lemma snd_enumerate:
  "i < length xs ⟹ snd (enumerate n xs ! i) = xs ! i"
  by (metis nth_enumerate_eq snd_conv)

lemma enumerate_member:
  assumes "i < length xs"
  shows "(n + i, xs ! i) ∈ set (enumerate n xs)"
proof -
  have pair_unpack: "⋀a b x. ((a, b) = x) = (a = fst x ∧ b = snd x)" by fastforce
  from assms have "(n + i, xs ! i) = enumerate n xs ! i"
    by (auto simp: fst_enumerate snd_enumerate pair_unpack)
  with assms show ?thesis by simp
qed

lemma distinct_prop_nth:
  "⟦ distinct_prop P ls; n < n'; n' < length ls ⟧ ⟹ P (ls ! n) (ls ! n')"
  apply (induct ls arbitrary: n n'; simp)
  subgoal for l ls n n'
    apply (cases n'; simp)
    apply (cases n; simp)
    done
  done

lemma distinct_prop_iff:
  "⟦ ⋀x y. P x y ⟷ Q x y ⟧ ⟹ distinct_prop P xs ⟷ distinct_prop Q xs"
  by (induction xs) auto

lemma distinct_prop_impl:
  "⟦ ⋀x y. x ∈ set xs ⟹ y ∈ set xs ⟹ P x y ⟹ Q x y; distinct_prop P xs ⟧ ⟹ distinct_prop Q xs"
  by (induction xs) auto

lemma distinct_iff_distinct_prop_ne: "distinct xs ⟷ distinct_prop (≠) xs"
  by (induction xs) auto

end