text:
(*
  File:     Randomised_Quick_Sort.thy
  Author:   Manuel Eberl <manuel@pruvisto.org>

  Definition and cost analysis of randomised QuickSort (i.e. pivot chosen uniformly at random).
*)
section \<open>Randomised QuickSort\<close>
theory Randomised_Quick_Sort
  imports
    "HOL-Probability.Probability"
    "Landau_Symbols.Landau_More"
    Comparison_Sort_Lower_Bound.Linorder_Relations
begin

subsection \<open>Deletion by index\<close>

text \<open>
  The following function deletes the $n$-th element of a list.
\<close>

fun delete_index :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "delete_index _ [] = []"
| "delete_index 0 (x # xs) = xs"
| "delete_index (Suc n) (x # xs) = x # delete_index n xs"

lemma delete_index_altdef: "delete_index n xs = take n xs @ drop (Suc n) xs"
  by (induction n xs rule: delete_index.induct) simp_all

lemma delete_index_ge_length: "n \<ge> length xs \<Longrightarrow> delete_index n xs = xs"
  by (simp add: delete_index_altdef)

lemma length_delete_index [simp]: "n < length xs \<Longrightarrow> length (delete_index n xs) = length xs - 1"
  by (simp add: delete_index_altdef)

lemma delete_index_Cons:
  "delete_index n (x # xs) = (if n = 0 then xs else x # delete_index (n - 1) xs)"
  by (cases n) simp_all

lemma insert_set_delete_index:
  "n < length xs \<Longrightarrow> insert (xs ! n) (set (delete_index n xs)) = set xs"
  by (induction n xs rule: delete_index.induct) auto

lemma add_mset_delete_index:
  "i < length xs \<Longrightarrow> add_mset (xs ! i) (mset (delete_index i xs)) = mset xs"
  by (induction i xs rule: delete_index.induct) simp_all

lemma nth_delete_index:
  "i < length xs \<Longrightarrow> n < length xs \<Longrightarrow>
     delete_index n xs ! i = (if i < n then xs ! i else xs ! Suc i)"
  by (auto simp: delete_index_altdef nth_append min_def)

lemma set_delete_index_distinct:
  assumes "distinct xs" "n < length xs"
  shows   "set (delete_index n xs) = set xs - {xs ! n}"
  using assms by (induction n xs rule: delete_index.induct) fastforce+

lemma distinct_delete_index [simp, intro]:
  assumes "distinct xs"
  shows   "distinct (delete_index n xs)"
proof (cases "n < length xs")
  case True
  with assms show ?thesis
    by (induction n xs rule: delete_index.induct) (auto simp: set_delete_index_distinct)
qed (simp_all add: delete_index_ge_length assms)

lemma mset_delete_index [simp]:
  "i < length xs \<Longrightarrow> mset (delete_index i xs) = mset xs - {# xs!i #}"
  by (induction i xs rule: delete_index.induct) simp_all

subsection \<open>Definition\<close>

text \<open>
  The following is a functional randomised version of QuickSort that also records the number
  of comparisons that were made. The randomisation is in the selection of the pivot element:
  In each step, the next pivot is chosen uniformly at random from all remaining list elements.

  The function takes the ordering relation to use as a first argument in the form of a set of
  pairs.
\<close>

function rquicksort :: "('a \<times> 'a) set \<Rightarrow> 'a list \<Rightarrow> ('a list \<times> nat) pmf" where
  "rquicksort R xs =
     (if xs = [] then
        return_pmf ([], 0)
      else
        do {
          i \<leftarrow> pmf_of_set {..<length xs};
          let x = xs ! i;
          case partition (\<lambda>y. (y,x) \<in> R) (delete_index i xs) of
            (ls, rs) \<Rightarrow> do {
              (ls, n1) \<leftarrow> rquicksort R ls;
              (rs, n2) \<leftarrow> rquicksort R rs;
              return_pmf (ls @ [x] @ rs, length xs - 1 + n1 + n2)
            }
        })"
  by auto
termination proof (relation "Wellfounded.measure (length \<circ> snd)", goal_cases)
  show "wf (Wellfounded.measure (length \<circ> snd))" by simp
qed (subst (asm) set_pmf_of_set; force intro!: le_less_trans[OF length_filter_le])+

declare rquicksort.simps [simp del]

lemma rquicksort_Nil [simp]: "rquicksort R [] = return_pmf ([], 0)"
  by (simp add: rquicksort.simps)

subsection \<open>Correctness proof\<close>

lemma set_pmf_of_set_lessThan_length [simp]:
  "xs \<noteq> [] \<Longrightarrow> set_pmf (pmf_of_set {..<length xs}) = {..<length xs}"
  by (subst set_pmf_of_set) auto

text \<open>
  We can now prove that any list that can be returned by QuickSort is sorted w.\,r.\,t.\ the
  given relation. (as long as that relation is reflexive, transitive, and total)
\<close>

theorem rquicksort_correct:
  assumes "trans R" and "total_on (set xs) R" and "\<forall>x\<in>set xs. (x,x) \<in> R"
  assumes "(ys, n) \<in> set_pmf (rquicksort R xs)"
  shows   "sorted_wrt R ys \<and> mset ys = mset xs"
  using assms(2-)
proof (induction xs arbitrary: ys n rule: length_induct)
  case (1 xs)
  have IH: "sorted_wrt R zs" "mset zs = mset ys"
    if "(zs, n) \<in> set_pmf (rquicksort R ys)" "length ys < length xs" "set ys \<subseteq> set xs" for zs ys n
    using that "1.IH" total_on_subset[OF "1.prems"(1) that(3)] "1.prems"(2) by blast+
  show ?case
  proof (cases "xs = []")
    case False
    with "1.prems" obtain ls rs n1 n2 i where *:
       "i < length xs" "(ls, n1) \<in> set_pmf (rquicksort R [y\<leftarrow>delete_index i xs. (y, xs ! i) \<in> R])"
       "(rs, n2) \<in> set_pmf (rquicksort R [y\<leftarrow>delete_index i xs. (y, xs ! i) \<notin> R])"
       "ys = ls @ [xs ! i] @ rs"
      by (subst (asm) rquicksort.simps[of _ xs]) (auto simp: Let_def o_def)
    note ys = \<open>ys = ls @ [xs ! i] @ rs\<close>
    define ls' where "ls' = [y\<leftarrow>delete_index i xs. (y, xs ! i) \<in> R]"
    define rs' where "rs' = [y\<leftarrow>delete_index i xs. (y, xs ! i) \<notin> R]"
    from \<open>i < length xs\<close> have less: "length ls' < length xs" "length rs' < length xs"
      unfolding ls'_def rs'_def by (intro le_less_trans[OF length_filter_le]; force)+
    have ls: "(ls, n1) \<in> set_pmf (rquicksort R ls')" and rs: "(rs, n2) \<in> set_pmf (rquicksort R rs')"
      using * unfolding ls'_def rs'_def by blast+
    have subset: "set ls' \<subseteq> set xs" "set rs' \<subseteq> set xs"
      using insert_set_delete_index[of i xs] \<open>i < length xs\<close>
      by (auto simp: ls'_def rs'_def)
    have sorted: "sorted_wrt R ls" "sorted_wrt R rs"
     and mset: "mset ls = mset ls'" "mset rs = mset rs'"
      by (rule IH[of ls n1 ls'] IH[of rs n2 rs'] less ls rs subset)+

    have ls_le: "(x, xs ! i) \<in> R" if "x \<in> set ls" for x
    proof -
      from that have "x \<in># mset ls" by simp
      also note mset(1)
      finally show ?thesis by (simp add: ls'_def)
    qed
    have rs_ge: "(x, xs ! i) \<notin> R" "(xs ! i, x) \<in> R" if "x \<in> set rs" for x
    proof -
      from that have "x \<in># mset rs" by simp
      also note mset(2)
      finally have x: "x \<in> set rs'" by simp
      thus "(x, xs ! i) \<notin> R" by (simp_all add: rs'_def)
      from x and subset and \<open>i < length xs\<close> have "x \<in> set xs" "xs ! i \<in> set xs" by auto
      with "1.prems" and \<open>(x, xs ! i) \<notin> R\<close> show "(xs ! i, x) \<in> R"
        unfolding total_on_def by (cases "xs ! i = x") auto
    qed

    have "sorted_wrt R ys" unfolding ys
      by (intro sorted_wrt_append \<open>trans R\<close> sorted_wrt_singleton sorted)
         (auto intro: rs_ge ls_le transD[OF \<open>trans R\<close>, of _ "xs!i"])
    moreover have "mset ys = mset xs" unfolding ys using \<open>i < length xs\<close>
      by (simp add: mset ls'_def rs'_def add_mset_delete_index)
    ultimately show ?thesis ..
  qed (insert "1.prems", simp_all)
qed

subsection \<open>Cost analysis\<close>

text \<open>
  The following distribution describes the number of comparisons made by randomised
  QuickSort in terms of the list length. (This is only valid if all list elements are distinct)

  A succinct explanation of this cost analysis is given by Jacek Cicho\'{n}~\<^cite>\<open>"cichon"\<close>.
\<close>
fun rqs_cost :: "nat \<Rightarrow> nat pmf" where
  "rqs_cost 0 = return_pmf 0"
| "rqs_cost (Suc n) =
     do {i \<leftarrow> pmf_of_set {..n}; a \<leftarrow> rqs_cost i; b \<leftarrow> rqs_cost (n - i); return_pmf (n + a + b)}"

lemma finite_set_pmf_rqs_cost [intro!]: "finite (set_pmf (rqs_cost n))"
  by (induction n rule: rqs_cost.induct) simp_all

text \<open>
  We connect the @{const rqs_cost} function to the @{const rquicksort} function by showing that
  projecting out the number of comparisons from a run of @{const rquicksort} on a list with distinct
  elements yields the same distribution as @{const rqs_cost} for the length of that list.
\<close>
theorem snd_rquicksort:
  assumes "linorder_on A R" and "set xs \<subseteq> A" and "distinct xs"
  shows   "map_pmf snd (rquicksort R xs) = rqs_cost (length xs)"
  using assms(2-)
proof (induction xs rule: length_induct)
  case (1 xs)
  have IH: "map_pmf snd (rquicksort R ys) = rqs_cost (length ys)"
    if "length ys < length xs" "mset ys \<subseteq># mset xs" for ys
  proof -
    from set_mset_mono[OF that(2)] have "set ys \<subseteq> set xs" by simp
    also note \<open>set xs \<subseteq> A\<close>
    finally have "set ys \<subseteq> A" .
    moreover from \<open>distinct xs\<close> and that(2) have "distinct ys"
      by (rule distinct_mset_mono)
    ultimately show ?thesis using that and "1.IH" by blast
  qed
  define n where "n = length xs"
  define cnt where "cnt = (\<lambda>i. length [y\<leftarrow>delete_index i xs. (y, xs ! i) \<in> R])"
  have cnt_altdef: "cnt i = linorder_rank R (set xs) (xs ! i)" if i: "i < n" for i
  proof -
    have "cnt i = length [y\<leftarrow>delete_index i xs. (y, xs ! i) \<in> R]" by (simp add: cnt_def)
    also have "\<dots> = card (set [y\<leftarrow>delete_index i xs. (y, xs ! i) \<in> R])"
      by (intro distinct_card [symmetric] distinct_filter distinct_delete_index "1.prems")
    also have "set [y\<leftarrow>delete_index i xs. (y, xs ! i) \<in> R] =
                      {x \<in> set xs-{xs!i}. (x, xs ! i) \<in> R}"
      using "1.prems" and i by (simp add: set_delete_index_distinct n_def)
    also have "card \<dots> = linorder_rank R (set xs) (xs ! i)" by (simp add: linorder_rank_def)
    finally show ?thesis .
  qed

  from "1.prems" have "bij_betw ((!) xs) {..<n} (set xs)"
    by (intro bij_betw_byWitness[where f' = "index xs"]) (auto simp: n_def index_nth_id)
  moreover have "bij_betw (linorder_rank R (set xs)) (set xs) {..<card (set xs)}"
    using assms(1) by (rule bij_betw_linorder_rank) (insert "1.prems", auto)
  ultimately have "bij_betw (linorder_rank R (set xs) \<circ> (\<lambda>i. xs ! i)) {..<n} {..<card (set xs)}"
    by (rule bij_betw_trans)
  hence bij: "bij_betw (\<lambda>i. linorder_rank R (set xs) (xs ! i)) {..<n} {..<n}"
    using "1.prems" by (simp add: n_def o_def distinct_card)

  show ?case
  proof (cases "xs = []")
    case False
    hence "n > 0" by (simp add: n_def)
    hence [simp]: "n \<noteq> 0" by (intro notI) auto
    from False have "map_pmf snd (rquicksort R xs) =
             pmf_of_set {..<length xs} \<bind>
               (\<lambda>i. map_pmf (\<lambda>z. length xs - 1 + fst z + snd z)
                  (pair_pmf (map_pmf snd (rquicksort R [y\<leftarrow>delete_index i xs. (y, xs ! i) \<in> R]))
                            (map_pmf snd (rquicksort R [y\<leftarrow>delete_index i xs. (y, xs ! i) \<notin> R]))))"
      by (subst rquicksort.simps)
         (simp add: map_bind_pmf bind_map_pmf Let_def case_prod_unfold o_def pair_pmf_def)
    also have "\<dots> = pmf_of_set {..<length xs} \<bind>
                      (\<lambda>i. map_pmf (\<lambda>z. n - 1 + fst z + snd z)
                         (pair_pmf (rqs_cost (cnt i)) (rqs_cost (n - 1 - cnt i))))"
    proof (intro bind_pmf_cong refl, goal_cases)
      case (1 i)
      with \<open>xs \<noteq> []\<close> have i: "i < length xs" by auto
      from i have "map_pmf snd (rquicksort R [y\<leftarrow>delete_index i xs. (y, xs ! i) \<notin> R]) =
                              rqs_cost (length [y\<leftarrow>delete_index i xs. (y, xs ! i) \<notin> R])"
        by (intro IH)
           (auto intro!: le_less_trans[OF length_filter_le]
                 intro: subset_mset.trans multiset_filter_subset diff_subset_eq_self)
      also have "length [y\<leftarrow>delete_index i xs. (y, xs ! i) \<notin> R] = n - 1 - cnt i"
        unfolding n_def cnt_def
        using sum_length_filter_compl[of "\<lambda>y. (y, xs ! i) \<in> R" "delete_index i xs"] i by simp
      finally have "map_pmf snd (rquicksort R [y\<leftarrow>delete_index i xs. (y, xs ! i) \<notin> R]) =
                      rqs_cost (n - 1 - cnt i)" .
      moreover have "map_pmf snd (rquicksort R [y\<leftarrow>delete_index i xs. (y, xs ! i) \<in> R]) =
                       rqs_cost (cnt i)" unfolding cnt_def using i
        by (intro IH)
           (auto intro!: le_less_trans[OF length_filter_le]
                 intro: subset_mset.trans multiset_filter_subset diff_subset_eq_self)
      ultimately show ?case by (simp only: n_def)
    qed
    also have "\<dots> = map_pmf cnt (pmf_of_set {..<n}) \<bind>
          (\<lambda>i. map_pmf (\<lambda>z. n - 1 + fst z + snd z) (pair_pmf (rqs_cost i) (rqs_cost (n - 1 - i))))"
      (is "_ = bind_pmf _ ?f") by (simp add: bind_map_pmf n_def)
    also have "map_pmf cnt (pmf_of_set {..<n}) =
                 map_pmf (\<lambda>i. linorder_rank R (set xs) (xs ! i)) (pmf_of_set {..<n})"
      using \<open>n > 0\<close> by (intro map_pmf_cong refl, subst (asm) set_pmf_of_set) (auto simp: cnt_altdef)
    also from \<open>n > 0\<close> have "\<dots> = pmf_of_set {..<n}" by (intro map_pmf_of_set_bij_betw bij) auto
    also have "pmf_of_set {..<n} \<bind> ?f = rqs_cost n"
      by (cases n) (simp_all add: lessThan_Suc_atMost bind_map_pmf map_bind_pmf pair_pmf_def)
    finally show ?thesis by (simp add: n_def)
  qed simp_all
qed

subsection \<open>Expected cost\<close>

text \<open>
  It is relatively straightforward to see that the following recursive function
  (sometimes called the `QuickSort equation') describes the expectation of @{const rqs_cost},
  i.e. the expected number of comparisons of QuickSort when run on a list with distinct elements.
\<close>
fun rqs_cost_exp :: "nat \<Rightarrow> real" where
  "rqs_cost_exp 0 = 0"
| "rqs_cost_exp (Suc n) = real n + (\<Sum>i\<le>n. rqs_cost_exp i + rqs_cost_exp (n - i)) / real (Suc n)"

lemmas rqs_cost_exp_0 = rqs_cost_exp.simps(1)
lemmas rqs_cost_exp_Suc [simp del] = rqs_cost_exp.simps(2)
lemma rqs_cost_exp_Suc_0 [simp]: "rqs_cost_exp (Suc 0) = 0" by (simp add: rqs_cost_exp_Suc)

text \<open>
  The following theorem shows that @{const rqs_cost_exp} is indeed the expectation of
  @{const rqs_cost}.
\<close>
theorem expectation_rqs_cost: "measure_pmf.expectation (rqs_cost n) real = rqs_cost_exp n"
proof (induction n rule: rqs_cost.induct)
  case (2 n)
  note IH = "2.IH"
  have "measure_pmf.expectation (rqs_cost (Suc n)) real =
          (\<Sum>a\<le>n. inverse (real (Suc n)) *
              measure_pmf.expectation (rqs_cost a \<bind> (\<lambda>aa. rqs_cost (n - a) \<bind>
                 (\<lambda>b. return_pmf (n + aa + b)))) real)"
    unfolding rqs_cost.simps by (subst pmf_expectation_bind_pmf_of_set) auto
  also have "\<dots> = (\<Sum>i\<le>n. inverse (real (Suc n)) * (real n + rqs_cost_exp i + rqs_cost_exp (n - i)))"
  proof (intro sum.cong refl, goal_cases)
    case (1 i)
    have "rqs_cost i \<bind> (\<lambda>a. rqs_cost (n - i) \<bind> (\<lambda>b. return_pmf (n + a + b))) =
            map_pmf (\<lambda>(a,b). n + a + b) (pair_pmf (rqs_cost i) (rqs_cost (n - i)))"
      by (simp add: pair_pmf_def map_bind_pmf)
    also have "measure_pmf.expectation \<dots> real =
                 measure_pmf.expectation (pair_pmf (rqs_cost i) (rqs_cost (n - i)))
                   (\<lambda>z. real n + (real (fst z) + real (snd z)))"
      by (subst integral_map_pmf) (simp add: case_prod_unfold add_ac)
    also have "\<dots> = real n + measure_pmf.expectation (pair_pmf (rqs_cost i) (rqs_cost (n - i)))
                      (\<lambda>z. real (fst z) + real (snd z))" (is "_ = _ + ?A")
      by (subst Bochner_Integration.integral_add) (auto intro!: integrable_measure_pmf_finite)
    also have "?A = measure_pmf.expectation (map_pmf fst (pair_pmf (rqs_cost i) (rqs_cost (n - i)))) real +
                    measure_pmf.expectation (map_pmf snd (pair_pmf (rqs_cost i) (rqs_cost (n - i)))) real"
      unfolding integral_map_pmf
      by (subst Bochner_Integration.integral_add) (auto intro!: integrable_measure_pmf_finite)
    also have "\<dots> = measure_pmf.expectation (rqs_cost i) real +
                    measure_pmf.expectation (rqs_cost (n - i)) real"
      unfolding map_fst_pair_pmf map_snd_pair_pmf ..
    also from 1 have "\<dots> = rqs_cost_exp i + rqs_cost_exp (n - i)" by (simp_all add: IH)
    finally show ?case by simp
  qed
  also have "\<dots> = (\<Sum>i\<le>n. inverse (real (Suc n)) * real n) +
                    (\<Sum>i\<le>n. rqs_cost_exp i + rqs_cost_exp (n - i)) / real (Suc n)"
    by (simp add: sum.distrib field_simps sum_distrib_left sum_distrib_right
          sum_divide_distrib [symmetric] del: of_nat_Suc)
  also have "(\<Sum>i\<le>n. inverse (real (Suc n)) * real n) = real n" by simp
  also have "\<dots> + (\<Sum>i\<le>n. rqs_cost_exp i + rqs_cost_exp (n - i)) / real (Suc n) = rqs_cost_exp (Suc n)"
    by (simp add: rqs_cost_exp_Suc)
  finally show ?case .
qed simp_all

text \<open>
  We will now obtain a closed-form solution for @{const rqs_cost_exp}. First of all, we can
  reindex the right-most sum in the recursion step and obtain:
\<close>
lemma rqs_cost_exp_Suc':
  "rqs_cost_exp (Suc n) = real n + 2 / real (Suc n) * (\<Sum>i\<le>n. rqs_cost_exp i)"
proof -
  have "rqs_cost_exp (Suc n) = real n + (\<Sum>i\<le>n. rqs_cost_exp i + rqs_cost_exp (n - i)) / real (Suc n)"
    by (rule rqs_cost_exp_Suc)
  also have "(\<Sum>i\<le>n. rqs_cost_exp i + rqs_cost_exp (n - i)) = (\<Sum>i\<le>n. rqs_cost_exp i) + (\<Sum>i\<le>n. rqs_cost_exp (n - i))"
    by (simp add: sum.distrib)
  also have "(\<Sum>i\<le>n. rqs_cost_exp (n - i)) = (\<Sum>i\<le>n. rqs_cost_exp i)"
    by (intro sum.reindex_bij_witness[of _ "\<lambda>i. n - i" "\<lambda>i. n - i"]) auto
  also have "\<dots> + \<dots> = 2 * \<dots>" by simp
  also have "\<dots> / real (Suc n) = 2 / real (Suc n) * (\<Sum>i\<le>n. rqs_cost_exp i)" by simp
  finally show ?thesis .
qed

text \<open>
  Next, we can apply some standard techniques to transform this equation into a simple
  linear recurrence, which we can then solve easily in terms of harmonic numbers:
\<close>
theorem rqs_cost_exp_eq [code]: "rqs_cost_exp n = 2 * real (n + 1) * harm n - 4 * real n"
proof -
  define F where "F = (\<lambda>n. rqs_cost_exp n / (real n + 1))"
  have [simp]: "F 0 = 0" "F (Suc 0) = 0" by (simp_all add: F_def)
  have F_Suc: "F (Suc m) = F m + real (2*m) / (real ((m+1)*(m+2)))" if "m > 0" for m
  proof (cases m)
    case (Suc n)
    have A: "rqs_cost_exp (Suc (Suc n)) * real (Suc (Suc n)) =
            real ((n+1)*(n+2)) + 2 * (\<Sum>i\<le>n. rqs_cost_exp i) + 2 * rqs_cost_exp (Suc n)"
      by (subst rqs_cost_exp_Suc') (simp_all add: field_simps)
    have B: "rqs_cost_exp (Suc n) * real (Suc n) = real (n*(n+1)) + 2 * (\<Sum>i\<le>n. rqs_cost_exp i)"
      by (subst rqs_cost_exp_Suc') (simp_all add: field_simps)
    have "rqs_cost_exp (Suc (Suc n)) * real (Suc (Suc n)) - rqs_cost_exp (Suc n) * real (Suc n) =
            real ((n+1)*(n+2)) - real (n*(n+1)) + 2 * rqs_cost_exp (Suc n)"
      by (subst A, subst B) simp_all
    also have "real ((n+1)*(n+2)) - real (n*(n+1)) = real (2*(n+1))" by simp
    finally have "rqs_cost_exp (Suc (Suc n)) * real (n+2) = rqs_cost_exp (Suc n) * real (n+3) + real (2*(n+1))"
      by (simp add: algebra_simps)
    hence "rqs_cost_exp (Suc (Suc n)) / real (n+3) =
             rqs_cost_exp (Suc n) / real (n+2) + real (2*(n+1)) / (real (n+2)*real (n+3))"
      by (simp add: divide_simps del: of_nat_Suc of_nat_add)
    thus ?thesis by (simp add: F_def algebra_simps Suc)
  qed simp_all

  have F_eq: "F n = 2 * (\<Sum>k=1..n. real (k - 1) / real (k * (k + 1)))" for n
  proof (cases "n \<ge> 1")
    case True
    thus ?thesis by (induction n rule: dec_induct) (simp_all add: F_Suc algebra_simps)
  qed (simp_all add: not_le)

  have "F n = 2 * (\<Sum>k=1..n. real (k - 1) / real (k * (k + 1)))" (is "_ = 2 * ?S") by (fact F_eq)
  also have "?S = (\<Sum>k=1..n. 2 / real (Suc k) - 1 / real k)"
    by (intro sum.cong) (simp_all add: field_simps of_nat_diff)
  also have "\<dots> = 2 * (\<Sum>k=1..n. inverse (real (Suc k))) - harm n"
    by (subst sum_subtractf) (simp add: harm_def sum.distrib sum_distrib_left divide_simps)
  also have "(\<Sum>k=1..n. inverse (real (Suc k))) = (\<Sum>k=Suc 1..Suc n. inverse (real k))"
    by (intro sum.reindex_bij_witness[of _ "\<lambda>x. x - 1" Suc]) auto
  also have "\<dots> = harm (Suc n) - 1" unfolding harm_def by (subst (2) sum.atLeast_Suc_atMost) simp_all
  finally have "F n = 2 * harm n + 4 * (1 / (n + 1) - 1)" by (simp add: harm_Suc field_simps)
  also have "\<dots> * real (n + 1) = 2 * real (n + 1) * harm n - 4 * real n"
    by (simp add: field_simps)
  also have "F n * real (n + 1) = rqs_cost_exp n" by (simp add: F_def add_ac)
  finally show ?thesis .
qed

(* TODO Move *)
lemma asymp_equiv_harm [asymp_equiv_intros]: "harm \<sim>[at_top] (\<lambda>n. ln (real n))"
proof -
  have "(\<lambda>n. harm n - ln (real n)) \<in> O(\<lambda>_. 1)" using euler_mascheroni_LIMSEQ
    by (intro bigoI_tendsto[where c = euler_mascheroni]) simp_all
  also have "(\<lambda>_. 1) \<in> o(\<lambda>n. ln (real n))" by auto
  finally have "(\<lambda>n. ln (real n) + (harm n - ln (real n))) \<sim>[at_top] (\<lambda>n. ln (real n))"
    by (subst asymp_equiv_add_right) simp_all
  thus ?thesis by simp
qed

corollary rqs_cost_exp_asymp_equiv: "rqs_cost_exp \<sim>[at_top] (\<lambda>n. 2 * n * ln n)"
proof -
  have "rqs_cost_exp = (\<lambda>n. 2 * real (n + 1) * harm n - 4 * real n)" using rqs_cost_exp_eq ..
  also have "\<dots> = (\<lambda>n. 2 * real n * harm n + (2 * harm n - 4 * real n))"
    by (simp add: algebra_simps)
  finally have "rqs_cost_exp \<sim>[at_top] \<dots>" by simp
  also have "\<dots> \<sim>[at_top] (\<lambda>n. 2 * real n * harm n)"
  proof (subst asymp_equiv_add_right)
    have "(\<lambda>x. 1 * harm x) \<in> o(\<lambda>x. real x * harm x)"
      by (intro landau_o.small_big_mult smallo_real_nat_transfer) simp_all
    moreover have "harm \<in> \<omega>(\<lambda>_. 1 :: real)"
      by (intro smallomegaI_filterlim_at_top_norm) (auto simp: harm_at_top)
    hence "(\<lambda>x. real x * 1) \<in> o(\<lambda>x. real x * harm x)"
      by (intro landau_o.big_small_mult) (simp_all add: smallomega_iff_smallo)
    ultimately show "(\<lambda>n. 2 * harm n - 4 * real n) \<in> o(\<lambda>n. 2 * real n * harm n)"
      by (intro sum_in_smallo) simp_all
  qed simp_all
  also have "\<dots> \<sim>[at_top] (\<lambda>n. 2 * real n * ln (real n))" by (intro asymp_equiv_intros)
  finally show ?thesis .
qed

lemma harm_mono: "m \<le> n \<Longrightarrow> harm m \<le> (harm n :: real)"
  unfolding harm_def by (intro sum_mono2) auto

lemma harm_Suc_0 [simp]: "harm (Suc 0) = 1"
  by (simp add: harm_def)

lemma harm_ge_1: "n > 0 \<Longrightarrow> harm n \<ge> (1::real)"
  using harm_mono[of 1 n] by simp

lemma mono_rqs_cost_exp: "mono rqs_cost_exp"
proof (rule incseq_SucI)
  fix n show "rqs_cost_exp n \<le> rqs_cost_exp (Suc n)"
  proof (cases "n = 0")
    case False
    have "0 < (1 * 2 * (real n + 1) - 2 * real n) / (real n + 1)" by simp
    also have "\<dots> \<le> (harm n * 2 * (real n + 1) - 2 * real n) / (real n + 1)" using False
      by (intro divide_right_mono diff_right_mono mult_right_mono) (auto simp: harm_ge_1)
    also have "\<dots> = rqs_cost_exp (Suc n) - rqs_cost_exp n"
      by (simp add: rqs_cost_exp_eq harm_Suc field_simps)
    finally show ?thesis by simp
  qed auto
qed

lemma rqs_cost_exp_leI: "m \<le> n \<Longrightarrow> rqs_cost_exp m \<le> rqs_cost_exp n"
  using mono_rqs_cost_exp by (simp add: mono_def)

subsection \<open>Version for lists with repeated elements\<close>

definition threeway_partition where
  "threeway_partition x R xs =
     (filter (\<lambda>y. (y,x) \<in> R \<and> (x,y) \<notin> R) xs,
      filter (\<lambda>y. (x,y) \<in> R \<and> (y,x) \<in> R) xs,
      filter (\<lambda>y. (x,y) \<in> R \<and> (y,x) \<notin> R) xs)"

text \<open>
  The following version of randomised Quicksort uses a three-way partitioning function
  in order to also achieve expected logarithmic running time on lists with repeated elements.
\<close>
function rquicksort' :: "('a \<times> 'a) set \<Rightarrow> 'a list \<Rightarrow> ('a list \<times> nat) pmf" where
  "rquicksort' R xs =
     (if xs = [] then
        return_pmf ([], 0)
      else
        do {
          i \<leftarrow> pmf_of_set {..<length xs};
          let x = xs ! i;
          case threeway_partition x R (delete_index i xs) of
            (ls, es, rs) \<Rightarrow> do {
              (ls, n1) \<leftarrow> rquicksort' R ls;
              (rs, n2) \<leftarrow> rquicksort' R rs;
              return_pmf (ls @ x # es @ rs, length xs - 1 + n1 + n2)
            }
        })"
  by auto
termination proof (relation "Wellfounded.measure (length \<circ> snd)", goal_cases)
  show "wf (Wellfounded.measure (length \<circ> snd))" by simp
qed (subst (asm) set_pmf_of_set;
     force intro!: le_less_trans[OF length_filter_le] simp: threeway_partition_def)+

declare rquicksort'.simps [simp del]

lemma rquicksort'_Nil [simp]: "rquicksort' R [] = return_pmf ([], 0)"
  by (simp add: rquicksort'.simps)

context
begin

qualified definition lesss :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "lesss R x xs = filter (\<lambda>y. (y, x) \<in> R \<and> (x, y) \<notin> R) xs"

qualified definition greaters :: "('a \<times> 'a) set \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "greaters R x xs = filter (\<lambda>y. (x, y) \<in> R \<and> (y, x) \<notin> R) xs"

qualified lemma lesss_Cons:
  "lesss R x (y # ys) =
     (if (y, x) \<in> R \<and> (x, y) \<notin> R then y # lesss R x ys else lesss R x ys)"
  by (simp add: lesss_def)

qualified lemma length_lesss_le [intro]: "length (lesss R x xs) \<le> length xs"
  by (simp add: lesss_def)

qualified lemma length_lesss_less [intro]:
  assumes "x \<in> set xs"
  shows   "length (lesss R x xs) < length xs"
  using assms by (induction xs) (auto simp: lesss_Cons intro: le_less_trans)

qualified lemma greaters_Cons:
  "greaters R x (y # ys) =
     (if (x, y) \<in> R \<and> (y, x) \<notin> R then y # greaters R x ys else greaters R x ys)"
  by (simp add: greaters_def)

qualified lemma length_greaters_le [intro]: "length (greaters R x xs) \<le> length xs"
  by (simp add: greaters_def)

qualified lemma length_greaters_less [intro]:
  assumes "x \<in> set xs"
  shows   "length (greaters R x xs) < length xs"
  using assms by (induction xs) (auto simp: greaters_Cons intro: le_less_trans)

text \<open>
  The following function counts the comparisons made by the modified randomised Quicksort.
\<close>
function rqs'_cost :: "('a \<times> 'a) set \<Rightarrow> 'a list \<Rightarrow> nat pmf" where
  "rqs'_cost R xs =
     (if xs = [] then
        return_pmf 0
      else
        do {
          i \<leftarrow> pmf_of_set {..<length xs};
          let x = xs ! i;
          map_pmf (\<lambda>(n1,n2). length xs - 1 + n1 + n2)
            (pair_pmf (rqs'_cost R (lesss R x xs)) (rqs'_cost R (greaters R x xs)))
        })"
  by auto
termination by (relation "Wellfounded.measure (length \<circ> snd)") auto

declare rqs'_cost.simps [simp del]

lemma rqs'_cost_nonempty:
  "xs \<noteq> [] \<Longrightarrow> rqs'_cost R xs =
     do {
       i \<leftarrow> pmf_of_set {..<length xs};
       let x = xs ! i;
       n1 \<leftarrow> rqs'_cost R (lesss R x xs);
       n2 \<leftarrow> rqs'_cost R (greaters R x xs);
       return_pmf (length xs - 1 + n1 + n2)
     }"
  by (subst rqs'_cost.simps) (auto simp: pair_pmf_def Let_def map_bind_pmf)

lemma finite_set_pmf_rqs'_cost [simp, intro]:
  "finite (set_pmf (rqs'_cost R xs))"
  by (induction R xs rule: rqs'_cost.induct) (auto simp: rqs'_cost.simps Let_def)

(* TODO: Move? *)
lemma expectation_pair_pmf_fst [simp]:
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  shows "measure_pmf.expectation (pair_pmf p q) (\<lambda>x. f (fst x)) = measure_pmf.expectation p f"
proof -
  have "measure_pmf.expectation (pair_pmf p q) (\<lambda>x. f (fst x)) =
          measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f" by simp
  also have "map_pmf fst (pair_pmf p q) = p"
    by (simp add: map_fst_pair_pmf)
  finally show ?thesis .
qed

lemma expectation_pair_pmf_snd [simp]:
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
  shows "measure_pmf.expectation (pair_pmf p q) (\<lambda>x. f (snd x)) = measure_pmf.expectation q f"
proof -
  have "measure_pmf.expectation (pair_pmf p q) (\<lambda>x. f (snd x)) =
          measure_pmf.expectation (map_pmf snd (pair_pmf p q)) f" by simp
  also have "map_pmf snd (pair_pmf p q) = q"
    by (simp add: map_snd_pair_pmf)
  finally show ?thesis .
qed

qualified lemma length_lesss_le_sorted:
  assumes "sorted_wrt R xs" "i < length xs"
  shows   "length (lesss R (xs ! i) xs) \<le> i"
  using assms by (induction arbitrary: i rule: sorted_wrt.induct)
                 (force simp: lesss_def nth_Cons le_Suc_eq split: nat.splits)+

qualified lemma length_greaters_le_sorted:
  assumes "sorted_wrt R xs" "i < length xs"
  shows   "length (greaters R (xs ! i) xs) \<le> length xs - i - 1"
  using assms
  by (induction arbitrary: i rule: sorted_wrt.induct)
     (force simp: greaters_def nth_Cons le_Suc_eq split: nat.splits)+

qualified lemma length_lesss_le':
  assumes "i < length xs" "linorder_on A R" "set xs \<subseteq> A"
  shows   "length (lesss R (insort_wrt R xs ! i) xs) \<le> i"
proof -
  define x where "x = insort_wrt R xs ! i"
  define less where "less = (\<lambda>x y. (x,y) \<in> R \<and> (y,x) \<notin> R)"
  have "length (lesss R x xs) = size {# y \<in># mset xs. less y x #}"
    by (simp add: lesss_def size_mset [symmetric] less_def mset_filter del: size_mset)
  also have "mset xs = mset (insort_wrt R xs)" by simp
  also have "size {#y \<in># mset (insort_wrt R xs). less y x#} =
               length (lesss R x (insort_wrt R xs))"
    by (simp only: mset_filter [symmetric] size_mset lesss_def less_def)
  also have "\<dots> \<le> i" unfolding x_def by (rule length_lesss_le_sorted) (use assms in auto)
  finally show ?thesis unfolding x_def .
qed

qualified lemma length_greaters_le':
  assumes "i < length xs" "linorder_on A R" "set xs \<subseteq> A"
  shows   "length (greaters R (insort_wrt R xs ! i) xs) \<le> length xs - i - 1"
proof -
  define x where "x = insort_wrt R xs ! i"
  define less where "less = (\<lambda>x y. (x,y) \<in> R \<and> (y,x) \<notin> R)"
  have "length (greaters R x xs) = size {# y \<in># mset xs. less x y #}"
    by (simp add: greaters_def size_mset [symmetric] less_def mset_filter del: size_mset)
  also have "mset xs = mset (insort_wrt R xs)" by simp
  also have "size {#y \<in># mset (insort_wrt R xs). less x y#} =
               length (greaters R x (insort_wrt R xs))"
    by (simp only: mset_filter [symmetric] size_mset greaters_def less_def)
  also have "\<dots> \<le> length (insort_wrt R xs) - i - 1" unfolding x_def
    by (rule length_greaters_le_sorted) (use assms in auto)
  finally show ?thesis unfolding x_def by simp
qed

text \<open>
  We can show quite easily that the expected number of comparisons in this modified
  QuickSort is bounded above by the expected number of comparisons on a list of the same length
  with no repeated elements.
\<close>
theorem rqs'_cost_expectation_le:
  assumes "linorder_on A R" "set xs \<subseteq> A"
  shows   "measure_pmf.expectation (rqs'_cost R xs) real \<le> rqs_cost_exp (length xs)"
  using assms
proof (induction R xs rule: rqs'_cost.induct)
  case (1 R xs)
  show ?case
  proof (cases "xs = []")
    case False
    define n where "n = length xs - 1"
    have length_eq: "length xs = Suc n" using False by (simp add: n_def)
    define E where "E = (\<lambda>xs. measure_pmf.expectation (rqs'_cost R xs) real)"
    define f where "f = (\<lambda>x. rqs_cost_exp (length (lesss R x xs)) +
                                rqs_cost_exp (length (greaters R x xs)))"
    have "rqs'_cost R xs =
            do {
              i \<leftarrow> pmf_of_set {..<length xs};
              map_pmf (\<lambda>(n1, y). length xs - Suc 0 + n1 + y)
                (pair_pmf (rqs'_cost R (lesss R (xs ! i) xs))
                          (rqs'_cost R (greaters R (xs ! i) xs)))
            }"
      using False by (subst rqs'_cost.simps) (simp_all add: Let_def)
    also have "measure_pmf.expectation \<dots> real = real n +
           (\<Sum>k<length xs. E (lesss R (xs ! k) xs) + E (greaters R (xs ! k) xs)) / real (length xs)"
      using False
      by (subst pmf_expectation_bind_pmf_of_set)
         (auto intro!: finite_imageI finite_cartesian_product simp: case_prod_unfold
            integrable_measure_pmf_finite sum_divide_distrib [symmetric] field_simps
            length_eq sum.distrib E_def)
    also have "\<dots> \<le> real n + (\<Sum>k<length xs. f (xs ! k)) / real (length xs)"
      unfolding E_def f_def using False "1.prems"
      by (intro add_mono order.refl divide_right_mono sum_mono "1.IH"[OF _ _ refl] False)
         (auto simp: lesss_def greaters_def)
    also have "(\<Sum>k<length xs. f (xs ! k)) = (\<Sum>x\<in>#mset xs. f x)"
      by (simp only: mset_map [symmetric] sum_mset_sum_list sum_list_sum_nth)
         (simp_all add: atLeast0LessThan)
    also have "mset xs = mset (insort_wrt R xs)"
      by simp
    also have "(\<Sum>x\<in>#\<dots>. f x) = (\<Sum>i<length xs. f (insort_wrt R xs ! i))"
      by (simp only: mset_map [symmetric] sum_mset_sum_list sum_list_sum_nth)
         (simp_all add: atLeast0LessThan)
    also have "\<dots> \<le> (\<Sum>i<length xs. rqs_cost_exp i + rqs_cost_exp (length xs - i - 1))"
      unfolding f_def
    proof (intro sum_mono add_mono rqs_cost_exp_leI)
      fix i assume i: "i \<in> {..<length xs}"
      show "length (lesss R (insort_wrt R xs ! i) xs) \<le> i"
        using i "1.prems" by (intro length_lesss_le'[where A = A]) auto
      show "length (greaters R (insort_wrt R xs ! i) xs) \<le> length xs - i - 1"
        using i "1.prems" by (intro length_greaters_le'[where A = A]) auto
    qed
    also have "\<dots> = (\<Sum>i\<le>n. rqs_cost_exp i + rqs_cost_exp (n - i))"
      by (intro sum.cong) (auto simp: length_eq)
    also have "real n + \<dots> / real (length xs) = rqs_cost_exp (length xs)"
      by (simp add: length_eq rqs_cost_exp.simps(2))
    finally show ?thesis by (simp add: divide_right_mono)
  qed (auto simp: rqs'_cost.simps)
qed

end
end

author: isabelle-prover

repo: mirror-afp-devel


text:
(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

section "Normalising Word Numerals"

theory Norm_Words
  imports Bits_Int Signed_Words
begin

text \<open>
  Normalise word numerals, including negative ones apart from @{term "-1"}, to the
  interval \<open>[0..2^len_of 'a)\<close>. Only for concrete word lengths.
\<close>

lemma neg_num_bintr:
  "(- numeral x :: 'a::len word) = word_of_int (take_bit LENGTH('a) (- numeral x))"
  by transfer simp

ML \<open>
  fun is_refl (Const (@{const_name Pure.eq}, _) $ x $ y) = (x = y)
    | is_refl _ = false;

  fun signed_dest_wordT (Type (@{type_name word}, [Type (@{type_name signed}, [T])])) = Word_Lib.dest_binT T
    | signed_dest_wordT T = Word_Lib.dest_wordT T

  fun typ_size_of t = signed_dest_wordT (type_of (Thm.term_of t));

  fun num_len (Const (@{const_name Num.Bit0}, _) $ n) = num_len n + 1
    | num_len (Const (@{const_name Num.Bit1}, _) $ n) = num_len n + 1
    | num_len (Const (@{const_name Num.One}, _)) = 1
    | num_len (Const (@{const_name numeral}, _) $ t) = num_len t
    | num_len (Const (@{const_name uminus}, _) $ t) = num_len t
    | num_len t = raise TERM ("num_len", [t])

  fun unsigned_norm is_neg _ ctxt ct =
  (if is_neg orelse num_len (Thm.term_of ct) > typ_size_of ct then let
      val btr = if is_neg
                then @{thm neg_num_bintr} else @{thm num_abs_bintr}
      val th = [Thm.reflexive ct, mk_eq btr] MRS transitive_thm

      (* will work in context of theory Word as well *)
      val ss = simpset_of (@{context} addsimps @{thms bintrunc_numeral})
      val cnv = simplify (put_simpset ss ctxt) th
    in if is_refl (Thm.prop_of cnv) then NONE else SOME cnv end
    else NONE)
  handle TERM ("num_len", _) => NONE
       | TYPE ("dest_binT", _, _) => NONE
\<close>

simproc_setup
  unsigned_norm ("numeral n::'a::len word") = \<open>unsigned_norm false\<close>

simproc_setup
  unsigned_norm_neg0 ("-numeral (num.Bit0 num)::'a::len word") = \<open>unsigned_norm true\<close>

simproc_setup
  unsigned_norm_neg1 ("-numeral (num.Bit1 num)::'a::len word") = \<open>unsigned_norm true\<close>

lemma minus_one_norm:
  "(-1 :: 'a :: len word) = of_nat (2 ^ LENGTH('a) - 1)"
  by (simp add:of_nat_diff)

lemmas minus_one_norm_num =
  minus_one_norm [where 'a="'b::len bit0"] minus_one_norm [where 'a="'b::len0 bit1"]

lemma "f (7 :: 2 word) = f 3" by simp

lemma "f (-2) = f (21 + 1 :: 3 word)" by simp

lemma "f (-2) = f (13 + 1 :: 'a::len word)"
  apply simp (* does not touch generic word length *)
  oops

lemma "f (-2) = f (0xFFFFFFFE :: 32 word)" by simp

lemma "(-1 :: 2 word) = 3" by simp

lemma "f (-2) = f (0xFFFFFFFE :: 32 signed word)" by simp

text \<open>
  We leave @{term "-1"} untouched by default, because it is often useful
  and its normal form can be large.
  To include it in the normalisation, add @{thm [source] minus_one_norm_num}.
  The additional normalisation is restricted to concrete numeral word lengths,
  like the rest.
\<close>
context
  notes minus_one_norm_num [simp]
begin

lemma "f (-1) = f (15 :: 4 word)" by simp

lemma "f (-1) = f (7 :: 3 word)" by simp

lemma "f (-1) = f (0xFFFF :: 16 word)" by simp

lemma "f (-1) = f (0xFFFF + 1 :: 'a::len word)"
  apply simp (* does not touch generic -1 *)
  oops

end

end

repo: barakzai


text:
(* Property from Case-Analysis for Rippling and Inductive Proof,
   Moa Johansson, Lucas Dixon and Alan Bundy, ITP 2010.
   This Isabelle theory is produced using the TIP tool offered at the following website:
     https://github.com/tip-org/tools
   This file was originally provided as part of TIP benchmark at the following website:
     https://github.com/tip-org/benchmarks
   Yutaka Nagashima at CIIRC, CTU changed the TIP output theory file slightly
   to make it compatible with Isabelle2017.
   Some proofs were added by Yutaka Nagashima.*)
  theory TIP_prop_85
imports "../../Test_Base"
begin

datatype ('a, 'b) pair = pair2 "'a" "'b"

datatype 'a list = nil2 | cons2 "'a" "'a list"

datatype Nat = Z | S "Nat"

fun zip :: "'a list => 'b list => (('a, 'b) pair) list" where
"zip (nil2) z = nil2"
| "zip (cons2 z2 x2) (nil2) = nil2"
| "zip (cons2 z2 x2) (cons2 x3 x4) =
     cons2 (pair2 z2 x3) (zip x2 x4)"

fun x :: "'a list => 'a list => 'a list" where
"x (nil2) z = z"
| "x (cons2 z2 xs) z = cons2 z2 (x xs z)"

fun rev :: "'a list => 'a list" where
"rev (nil2) = nil2"
| "rev (cons2 z xs) = x (rev xs) (cons2 z (nil2))"

fun len :: "'a list => Nat" where
"len (nil2) = Z"
| "len (cons2 z xs) = S (len xs)"

theorem property0 :
  "(((len xs) = (len ys)) ==>
      ((zip (rev xs) (rev ys)) = (rev (zip xs ys))))"
  oops

end

repo: PSL


text:
section {* Map type: extra functions and properties *}

theory Map_Extra
imports
  Main
  "~~/src/HOL/Library/Countable_Set"
  "~~/src/HOL/Library/Char_ord"
  "~~/src/HOL/Library/Monad_Syntax"
begin

subsection {* Functional relations *}

definition functional :: "('a * 'b) set \<Rightarrow> bool" where
"functional g = inj_on fst g"

definition functional_list :: "('a * 'b) list \<Rightarrow> bool" where
"functional_list xs = (\<forall> x y z. ListMem (x,y) xs \<and> ListMem (x,z) xs \<longrightarrow> y = z)"

lemma functional_insert [simp]: "functional (insert (x,y) g) \<longleftrightarrow> (g``{x} \<subseteq> {y} \<and> functional g)"
  by (auto simp add:functional_def inj_on_def image_def)

(*
lemma functional_listD: "\<lbrakk>finite g; functional g\<rbrakk> \<Longrightarrow> functional_list (sorted_list_of_set g)"
  by (force simp add:functional_list_def ListMem_iff functional_def inj_on_def)
*)

lemma functional_list_nil[simp]: "functional_list []"
  by (simp add:functional_list_def ListMem_iff)

lemma functional_list: "functional_list xs \<longleftrightarrow> functional (set xs)"
  apply (induct xs)
  apply (simp add:functional_def)
  apply (simp add:functional_def functional_list_def ListMem_iff)
  apply (safe)
  apply (force)
  apply (force)
  apply (force)
  apply (force)
  apply (force)
  apply (force)
  apply (force)
  apply (force)
done

subsection {* Graphing maps *}

definition map_graph :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a * 'b) set" where
"map_graph f = {(x,y) | x y. f x = Some y}"

definition graph_map :: "('a * 'b) set \<Rightarrow> ('a \<rightharpoonup> 'b)" where
"graph_map g = (\<lambda> x. if (x \<in> fst ` g) then Some (SOME y. (x,y) \<in> g) else None)"

definition graph_map' :: "('a \<times> 'b) set \<rightharpoonup> ('a \<rightharpoonup> 'b)" where
"graph_map' R = (if (functional R) then Some (graph_map R) else None)"

lemma map_graph_mem_equiv: "(x, y) \<in> map_graph f \<longleftrightarrow> f(x) = Some y"
  by (simp add: map_graph_def)

lemma map_graph_functional[simp]: "functional (map_graph f)"
  by (simp add:functional_def map_graph_def inj_on_def)

lemma map_graph_countable [simp]: "countable (dom f) \<Longrightarrow> countable (map_graph f)"
  apply (auto simp add:map_graph_def countable_def)
  apply (rule_tac x="fa \<circ> fst" in exI)
  apply (auto simp add:inj_on_def dom_def)
  apply fastforce
done

lemma map_graph_inv [simp]: "graph_map (map_graph f) = f"
  by (auto intro!:ext simp add:map_graph_def graph_map_def image_def)

lemma graph_map_empty[simp]: "graph_map {} = empty"
  by (simp add:graph_map_def)

lemma graph_map_insert [simp]: "\<lbrakk>functional g; g``{x} \<subseteq> {y}\<rbrakk> \<Longrightarrow> graph_map (insert (x,y) g) = (graph_map g)(x \<mapsto> y)"
  by (rule ext, auto simp add:graph_map_def)

lemma dom_map_graph: "dom f = Domain(map_graph f)"
  by (simp add: map_graph_def dom_def image_def)

lemma ran_map_graph: "ran f = Range(map_graph f)"
  by (simp add: map_graph_def ran_def image_def)

lemma ran_map_add_subset:
  "ran (x ++ y) \<subseteq> (ran x) \<union> (ran y)"
  by (auto simp add:ran_def)

lemma finite_dom_graph: "finite (dom f) \<Longrightarrow> finite (map_graph f)"
  by (metis dom_map_graph finite_imageD fst_eq_Domain functional_def map_graph_functional)

lemma finite_dom_ran [simp]: "finite (dom f) \<Longrightarrow> finite (ran f)"
  by (metis finite_Range finite_dom_graph ran_map_graph)

lemma graph_map_inv [simp]: "functional g \<Longrightarrow> map_graph (graph_map g) = g"
  apply (auto simp add:map_graph_def graph_map_def functional_def)
  apply (metis (lifting, no_types) image_iff option.distinct(1) option.inject someI surjective_pairing)
  apply (simp add:inj_on_def)
  apply (metis fst_conv snd_conv some_equality)
  apply (metis (lifting) fst_conv image_iff)
done

lemma graph_map_dom: "dom (graph_map R) = fst ` R"
  by (simp add: graph_map_def dom_def)

lemma graph_map_countable_dom: "countable R \<Longrightarrow> countable (dom (graph_map R))"
  by (simp add: graph_map_dom)

lemma countable_ran:
  assumes "countable (dom f)"
  shows "countable (ran f)"
proof -
  have "countable (map_graph f)"
    by (simp add: assms)
  then have "countable (Range(map_graph f))"
    by (simp add: Range_snd)
  thus ?thesis
    by (simp add: ran_map_graph)
qed

lemma map_graph_inv' [simp]:
  "graph_map' (map_graph f) = Some f"
  by (simp add: graph_map'_def)

lemma map_graph_inj:
  "inj map_graph"
  by (metis injI map_graph_inv)

lemma map_eq_graph: "f = g \<longleftrightarrow> map_graph f = map_graph g"
  by (auto simp add: inj_eq map_graph_inj)

(*
lemma functional_list_graph: "\<lbrakk>functional_list xs; sorted xs; distinct xs\<rbrakk> \<Longrightarrow> map_of xs = graph_map (set xs)"
  apply (simp add:functional_list)
  apply (induct xs)
  apply (simp)
  apply (auto)
  apply (rule ext)
  apply (auto)
  apply (metis sorted_Cons)
done

lemma map_graph_list: "\<lbrakk>finite g; functional g\<rbrakk> \<Longrightarrow> map_of (sorted_list_of_set g) = graph_map g"
  apply (subgoal_tac "\<exists> xs. functional_list xs \<and> sorted xs \<and> distinct xs \<and> g = set xs")
  apply (auto)
  apply (simp add:sorted_list_of_set_sort_remdups distinct_remdups_id sorted_sort_id functional_list_graph)
  apply (auto dest:functional_listD)
done
*)

lemma map_le_graph: "f \<subseteq>\<^sub>m g \<longleftrightarrow> map_graph f \<subseteq> map_graph g"
  by (force simp add: map_le_def map_graph_def)

lemma map_graph_comp: "map_graph (g \<circ>\<^sub>m f) = (map_graph f) O (map_graph g)"
  apply (auto simp add: map_comp_def map_graph_def relcomp_unfold)
  apply (rename_tac a b)
  apply (case_tac "f a", auto)
done

subsection {* Map application *}

definition map_apply :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ("_'(_')\<^sub>m" [999,0] 999) where
"map_apply = (\<lambda> f x. the (f x))"

subsection {* Map membership *}

fun map_member :: "'a \<times> 'b \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infix "\<in>\<^sub>m" 50) where
"(k, v) \<in>\<^sub>m m \<longleftrightarrow> m(k) = Some(v)"

lemma map_ext:
  "\<lbrakk> \<And> x y. (x, y) \<in>\<^sub>m A \<longleftrightarrow> (x, y) \<in>\<^sub>m B \<rbrakk> \<Longrightarrow> A = B"
  by (rule ext, auto, metis not_Some_eq)

lemma map_member_alt_def:
  "(x, y) \<in>\<^sub>m A \<longleftrightarrow> (x \<in> dom A \<and> A(x)\<^sub>m = y)"
  by (auto simp add: map_apply_def)

lemma map_le_member:
  "f \<subseteq>\<^sub>m g \<longleftrightarrow> (\<forall> x y. (x,y) \<in>\<^sub>m f \<longrightarrow> (x,y) \<in>\<^sub>m g)"
  by (force simp add: map_le_def)

subsection {* Preimage *}

definition preimage :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a set" where
"preimage f B = {x \<in> dom(f). the(f(x)) \<in> B}"

lemma preimage_range: "preimage f (ran f) = dom f"
  by (auto simp add: preimage_def ran_def)

lemma dom_preimage: "dom (m \<circ>\<^sub>m f) = preimage f (dom m)"
  apply (auto simp add: dom_def preimage_def)
  apply (meson map_comp_Some_iff)
  apply (metis map_comp_def option.case_eq_if option.distinct(1))
done

lemma countable_preimage:
  "\<lbrakk> countable A; inj_on f (preimage f A) \<rbrakk> \<Longrightarrow> countable (preimage f A)"
  apply (auto simp add: countable_def)
  apply (rename_tac g)
  apply (rule_tac x="g \<circ> the \<circ> f" in exI)
  apply (rule inj_onI)
  apply (drule inj_onD)
  apply (auto simp add: preimage_def inj_onD)
done

subsection {* Minus operation for maps *}

definition map_minus :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" (infixl "--" 100)
where "map_minus f g = (\<lambda> x. if (f x = g x) then None else f x)"

lemma map_minus_apply [simp]: "y \<in> dom(f -- g) \<Longrightarrow> (f -- g)(y)\<^sub>m = f(y)\<^sub>m"
  by (auto simp add: map_minus_def dom_def map_apply_def)

lemma map_member_plus:
  "(x, y) \<in>\<^sub>m f ++ g \<longleftrightarrow> ((x \<notin> dom(g) \<and> (x, y) \<in>\<^sub>m f) \<or> (x, y) \<in>\<^sub>m g)"
  by (auto simp add: map_add_Some_iff)

lemma map_member_minus:
  "(x, y) \<in>\<^sub>m f -- g \<longleftrightarrow> (x, y) \<in>\<^sub>m f \<and> (\<not> (x, y) \<in>\<^sub>m g)"
  by (auto simp add: map_minus_def)

lemma map_minus_plus_commute:
  "dom(g) \<inter> dom(h) = {} \<Longrightarrow> (f -- g) ++ h = (f ++ h) -- g"
  apply (rule map_ext)
  apply (auto simp add: map_member_plus map_member_minus simp del: map_member.simps)
  apply (auto simp add: map_member_alt_def)
done

lemma map_graph_minus: "map_graph (f -- g) = map_graph f - map_graph g"
  by (auto simp add: map_minus_def map_graph_def, (meson option.distinct(1))+)

lemma map_minus_common_subset:
  "\<lbrakk> h \<subseteq>\<^sub>m f; h \<subseteq>\<^sub>m g \<rbrakk> \<Longrightarrow> (f -- h = g -- h) = (f = g)"
  by (auto simp add: map_eq_graph map_graph_minus map_le_graph)

text {* Create some extra intro/elim rules to help dealing with proof about
        option bind. *}

lemma option_bindSomeE [elim!]:
  "\<lbrakk> X >>= F = Some(v); \<And> x. \<lbrakk> X = Some(x); F(x) = Some(v) \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
  by (case_tac X, auto)

lemma option_bindSomeI [intro]:
  "\<lbrakk> X = Some(x); F(x) = Some(y) \<rbrakk> \<Longrightarrow> X >>= F = Some(y)"
  by (simp)

lemma ifSomeE [elim]: "\<lbrakk> (if c then Some(x) else None) = Some(y); \<lbrakk> c; x = y \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
  by (case_tac c, auto)

text {* A range restriction operator; only domain restriction is provided in HOL *}

definition ran_restrict_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a \<rightharpoonup> 'b" ("_\<upharpoonleft>\<^bsub>_\<^esub>" [111,110] 110) where
"ran_restrict_map f B = (\<lambda>x. do { v <- f(x); if (v \<in> B) then Some(v) else None })"

lemma ran_restrict_empty [simp]: "f\<upharpoonleft>\<^bsub>{}\<^esub> = Map.empty"
  by (simp add:ran_restrict_map_def)

lemma ran_restrict_ran [simp]: "f\<upharpoonleft>\<^bsub>ran(f) \<^esub> = f"
  apply (auto simp add:ran_restrict_map_def ran_def)
  apply (rule ext)
  apply (case_tac "f(x)", auto)
done

lemma ran_ran_restrict [simp]: "ran(f\<upharpoonleft>\<^bsub>B\<^esub>) = ran(f) \<inter> B"
  by (auto intro!:option_bindSomeI simp add:ran_restrict_map_def ran_def)

lemma dom_ran_restrict: "dom(f\<upharpoonleft>\<^bsub>B\<^esub>) \<subseteq> dom(f)"
  by (auto simp add:ran_restrict_map_def dom_def)

lemma ran_restrict_finite_dom [intro]:
  "finite(dom(f)) \<Longrightarrow> finite(dom(f\<upharpoonleft>\<^bsub>B\<^esub>))"
  by (metis finite_subset dom_ran_restrict)

lemma dom_Some [simp]: "dom (Some \<circ> f) = UNIV"
  by (auto)

definition map_inv :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('b \<rightharpoonup> 'a)" where
"map_inv f \<equiv> \<lambda> y. if (y \<in> ran f) then Some (SOME x. f x = Some y) else None"

definition map_id_on :: "'a set \<Rightarrow> ('a \<rightharpoonup> 'a)" where
"map_id_on xs \<equiv> \<lambda> x. if (x \<in> xs) then Some x else None"

lemma map_id_on_in [simp]:
  "x \<in> xs \<Longrightarrow> map_id_on xs x = Some x"
  by (simp add:map_id_on_def)

lemma map_id_on_out [simp]:
  "x \<notin> xs \<Longrightarrow> map_id_on xs x = None"
  by (simp add:map_id_on_def)

lemma map_id_dom [simp]: "dom (map_id_on xs) = xs"
  by (simp add:dom_def map_id_on_def)

lemma map_id_ran [simp]: "ran (map_id_on xs) = xs"
  by (force simp add:ran_def map_id_on_def)

lemma map_id_on_UNIV[simp]: "map_id_on UNIV = Some"
  by (simp add:map_id_on_def)

lemma map_id_on_inj [simp]:
  "inj_on (map_id_on xs) xs"
  by (simp add:inj_on_def)

lemma map_inv_empty [simp]: "map_inv empty = empty"
  by (simp add:map_inv_def)

lemma map_inv_id [simp]:
  "map_inv (map_id_on xs) = map_id_on xs"
  by (force simp add:map_inv_def map_id_on_def ran_def)

lemma map_inv_Some [simp]: "map_inv Some = Some"
  by (simp add:map_inv_def ran_def)

lemma map_inv_f_f [simp]:
  "\<lbrakk> inj_on f (dom f); f x = Some y \<rbrakk> \<Longrightarrow> map_inv f y = Some x"
  apply (auto simp add: map_inv_def)
  apply (rule some_equality)
  apply (auto simp add:inj_on_def dom_def ran_def)
done

lemma dom_map_inv [simp]:
  "dom (map_inv f) = ran f"
  by (auto simp add:map_inv_def)

lemma ran_map_inv [simp]:
  "inj_on f (dom f) \<Longrightarrow> ran (map_inv f) = dom f"
  apply (auto simp add:map_inv_def ran_def)
  apply (rule_tac x="a" in exI)
  apply (force intro:someI)
  apply (rule_tac x="y" in exI)
  apply (auto)
  apply (rule some_equality, simp_all)
  apply (auto simp add:inj_on_def dom_def)
done

lemma dom_image_ran: "f ` dom f = Some ` ran f"
  by (auto simp add:dom_def ran_def image_def)

lemma inj_map_inv [intro]:
  "inj_on f (dom f) \<Longrightarrow> inj_on (map_inv f) (ran f)"
  apply (auto simp add:map_inv_def inj_on_def dom_def ran_def)
  apply (frule_tac P="\<lambda> xa. f xa = Some x" in some_equality)
  apply (auto)
  apply (metis (mono_tags) option.sel someI)
done

lemma inj_map_bij: "inj_on f (dom f) \<Longrightarrow> bij_betw f (dom f) (Some ` ran f)"
  by (auto simp add:inj_on_def dom_def ran_def image_def bij_betw_def)

lemma map_inv_map_inv [simp]:
  assumes "inj_on f (dom f)"
  shows "map_inv (map_inv f) = f"
proof -

  from assms have "inj_on (map_inv f) (ran f)"
    by auto

  thus ?thesis
    apply (rule_tac ext)
    apply (case_tac "\<exists> y. map_inv f y = Some x")
    apply (auto)[1]
    apply (simp add:map_inv_def)
    apply (case_tac "y \<in> ran f", simp_all)
    apply (auto)
    apply (rule someI2_ex)
    apply (simp add:ran_def)
    apply (simp)
    apply (metis assms dom_image_ran dom_map_inv image_iff map_add_dom_app_simps(2) map_add_dom_app_simps(3) ran_map_inv)
  done
qed

lemma dom_left_map_add [simp]: "x \<in> dom g \<Longrightarrow> (f ++ g) x = g x"
  by (auto simp add:map_add_def dom_def)

lemma dom_right_map_add [simp]: "\<lbrakk> x \<notin> dom g; x \<in> dom f \<rbrakk> \<Longrightarrow> (f ++ g) x = f x"
  by (auto simp add:map_add_def dom_def)

lemma map_add_restrict:
  "f ++ g = (f |` (- dom g)) ++ g"
  by (rule ext, auto simp add: map_add_def restrict_map_def)

lemma map_self_adjoin_complete [intro]:
  assumes "dom f \<inter> ran f = {}" "inj_on f (dom f)"
  shows "inj_on (map_inv f ++ f) (dom f \<union> ran f)"
  apply (rule inj_onI)
  apply (insert assms)
  apply (case_tac "x \<in> dom f")
  apply (simp)
  apply (case_tac "y \<in> dom f")
  apply (simp add:inj_on_def)
  apply (case_tac "y \<in> ran f")
  apply (subgoal_tac "y \<in> dom (map_inv f)")
  apply (simp)
  apply (metis Int_iff domD empty_iff ranI ran_map_inv)
  apply (simp)
  apply (simp)
  apply (simp)
  apply (case_tac "y \<in> dom f")
  apply (simp)
  apply (case_tac "y \<in> ran f")
  apply (subgoal_tac "y \<in> dom (map_inv f)")
  apply (simp)
  apply (metis Int_iff domD empty_iff ranI ran_map_inv)
  apply (simp)
  apply (metis Int_iff domD empty_iff ranI ran_map_inv)
  apply (simp)
  apply (metis (lifting) inj_map_inv inj_on_contraD)
done

lemma inj_completed_map [intro]:
  "\<lbrakk> dom f = ran f; inj_on f (dom f) \<rbrakk> \<Longrightarrow> inj (Some ++ f)"
  apply (drule inj_map_bij)
  apply (auto simp add:bij_betw_def)
  apply (auto simp add:inj_on_def)[1]
  apply (case_tac "x \<in> dom f")
  apply (simp)
  apply (case_tac "y \<in> dom f")
  apply (simp)
  apply (simp add:ran_def)
  apply (case_tac "y \<in> dom f")
  apply (auto intro:ranI)
done

lemma bij_completed_map [intro]:
  "\<lbrakk> dom f = ran f; inj_on f (dom f) \<rbrakk> \<Longrightarrow>
   bij_betw (Some ++ f) UNIV (range Some)"
  apply (auto intro: inj_completed_map simp add:bij_betw_def)
  apply (case_tac "xa \<in> dom f")
  apply (simp)
  apply (metis domD rangeI)
  apply (simp)
  apply (simp add:image_def)
  apply (metis (full_types) dom_image_ran dom_left_map_add image_iff map_add_dom_app_simps(3))
done

lemma bij_map_Some:
  "bij_betw f a (Some ` b) \<Longrightarrow> bij_betw (the \<circ> f) a b"
  apply (simp add:bij_betw_def)
  apply (safe)
  apply (metis (hide_lams, no_types) comp_inj_on_iff f_the_inv_into_f inj_on_inverseI option.sel)
  apply (metis (hide_lams, no_types) comp_apply image_iff option.sel)
  apply (metis imageI image_comp option.sel)
done

lemma ran_map_add [simp]:
  "m`(dom m \<inter> dom n) = n`(dom m \<inter> dom n) \<Longrightarrow>
   ran(m++n) = ran n \<union> ran m"
  apply (auto simp add:ran_def)
  apply (metis map_add_find_right)
  apply (case_tac "a \<in> dom n")
  apply (subgoal_tac "\<exists> b. n b = Some x")
  apply (auto)
  apply (rule_tac x="b" in exI)
  apply (simp)
  apply (metis (hide_lams, no_types) IntI domI image_iff)
  apply (metis (full_types) map_add_None map_add_dom_app_simps(1) map_add_dom_app_simps(3) not_None_eq)
done

lemma ran_maplets [simp]:
  "\<lbrakk> length xs = length ys; distinct xs \<rbrakk> \<Longrightarrow> ran [xs [\<mapsto>] ys] = set ys"
    by (induct rule:list_induct2, simp_all)

lemma inj_map_add:
  "\<lbrakk> inj_on f (dom f); inj_on g (dom g); ran f \<inter> ran g = {} \<rbrakk> \<Longrightarrow>
   inj_on (f ++ g) (dom f \<union> dom g)"
  apply (auto simp add:inj_on_def)
  apply (metis (full_types) disjoint_iff_not_equal domI dom_left_map_add map_add_dom_app_simps(3) ranI)
  apply (metis domI)
  apply (metis disjoint_iff_not_equal ranI)
  apply (metis disjoint_iff_not_equal domIff map_add_Some_iff ranI)
  apply (metis domI)
done

lemma map_inv_add [simp]:
  assumes "inj_on f (dom f)" "inj_on g (dom g)"
          "dom f \<inter> dom g = {}" "ran f \<inter> ran g = {}"
  shows "map_inv (f ++ g) = map_inv f ++ map_inv g"
proof (rule ext)

  from assms have minj: "inj_on (f ++ g) (dom (f ++ g))"
    by (simp, metis inj_map_add sup_commute)

  fix x
  have "x \<in> ran g \<Longrightarrow> map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
  proof -
    assume ran:"x \<in> ran g"
    then obtain y where dom:"g y = Some x" "y \<in> dom g"
      by (auto simp add:ran_def)

    hence "(f ++ g) y = Some x"
      by simp

    with assms minj ran dom show "map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
      by simp
  qed

  moreover have "\<lbrakk> x \<notin> ran g; x \<in> ran f \<rbrakk> \<Longrightarrow> map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
  proof -
    assume ran:"x \<notin> ran g" "x \<in> ran f"
    with assms obtain y where dom:"f y = Some x" "y \<in> dom f" "y \<notin> dom g"
      by (auto simp add:ran_def)

    with ran have "(f ++ g) y = Some x"
      by (simp)

    with assms minj ran dom show "map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
      by simp
  qed

  moreover from assms minj have "\<lbrakk> x \<notin> ran g; x \<notin> ran f \<rbrakk> \<Longrightarrow> map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
    apply (auto simp add:map_inv_def ran_def map_add_def)
    apply (metis dom_left_map_add map_add_def map_add_dom_app_simps(3))
  done

  ultimately show "map_inv (f ++ g) x = (map_inv f ++ map_inv g) x"
    apply (case_tac "x \<in> ran g")
    apply (simp)
    apply (case_tac "x \<in> ran f")
    apply (simp_all)
  done
qed

lemma map_add_lookup [simp]:
  "x \<notin> dom f \<Longrightarrow> ([x \<mapsto> y] ++ f) x = Some y"
  by (simp add:map_add_def dom_def)

lemma map_add_Some: "Some ++ f = map_id_on (- dom f) ++ f"
  apply (rule ext)
  apply (case_tac "x \<in> dom f")
  apply (simp_all)
done

lemma distinct_map_dom:
  "x \<notin> set xs \<Longrightarrow> x \<notin> dom [xs [\<mapsto>] ys]"
  by (simp add:dom_def)

lemma distinct_map_ran:
  "\<lbrakk> distinct xs; y \<notin> set ys; length xs = length ys \<rbrakk> \<Longrightarrow>
   y \<notin> ran ([xs [\<mapsto>] ys])"
  apply (simp add:map_upds_def)
  apply (subgoal_tac "distinct (map fst (rev (zip xs ys)))")
  apply (simp add:ran_distinct)
  apply (metis (hide_lams, no_types) image_iff set_zip_rightD surjective_pairing)
  apply (simp add:zip_rev[THEN sym])
done

lemma maplets_lookup[rule_format,dest]:
  "\<lbrakk> length xs = length ys; distinct xs \<rbrakk> \<Longrightarrow>
     \<forall> y. [xs [\<mapsto>] ys] x = Some y \<longrightarrow> y \<in> set ys"
  by (induct rule:list_induct2, auto)

lemma maplets_distinct_inj [intro]:
  "\<lbrakk> length xs = length ys; distinct xs; distinct ys; set xs \<inter> set ys = {} \<rbrakk> \<Longrightarrow>
   inj_on [xs [\<mapsto>] ys] (set xs)"
  apply (induct rule:list_induct2)
  apply (simp_all)
  apply (rule conjI)
  apply (rule inj_onI)
  apply (case_tac "xa = x")
  apply (simp)
  apply (case_tac "xa = y")
  apply (simp)
  apply (simp)
  apply (case_tac "ya = x")
  apply (simp)
  apply (simp add:inj_on_def)
  apply (auto)
  apply (case_tac "xa = y")
  apply (simp)
  apply (metis maplets_lookup)
done

lemma map_inv_maplet[simp]: "map_inv [x \<mapsto> y] = [y \<mapsto> x]"
  by (auto simp add:map_inv_def)

lemma map_inv_maplets [simp]:
  "\<lbrakk> length xs = length ys; distinct xs; distinct ys; set xs \<inter> set ys = {} \<rbrakk> \<Longrightarrow>
  map_inv [xs [\<mapsto>] ys] = [ys [\<mapsto>] xs]"
  apply (induct rule:list_induct2)
  apply (simp_all)
  apply (subgoal_tac "map_inv ([xs [\<mapsto>] ys] ++ [x \<mapsto> y]) = map_inv [xs [\<mapsto>] ys] ++ map_inv [x \<mapsto> y]")
  apply (simp)
  apply (rule map_inv_add)
  apply (auto)
done

lemma maplets_lookup_nth [rule_format,simp]:
  "\<lbrakk> length xs = length ys; distinct xs \<rbrakk> \<Longrightarrow>
   \<forall> i < length ys. [xs [\<mapsto>] ys] (xs ! i) = Some (ys ! i)"
  apply (induct rule:list_induct2)
  apply (auto)
  apply (case_tac i)
  apply (simp_all)
  apply (metis nth_mem)
  apply (case_tac i)
  apply (auto)
done

theorem the_Some[simp]: "the \<circ> Some = id"
  by (simp add:comp_def id_def)

theorem map_inv_expand [simp]:
  "\<lbrakk> inj_on f (dom f); f x = Some y \<rbrakk> \<Longrightarrow> map_inv f y = Some x"
  apply (auto simp add:ran_def map_inv_def)
  apply (rule some_equality, simp)
  apply (metis map_inv_f_f option.inject)
done

theorem inv_map_inv:
  "\<lbrakk> inj_on f (dom f); ran f = dom f \<rbrakk>
  \<Longrightarrow> inv (the \<circ> (Some ++ f)) = the \<circ> map_inv (Some ++ f)"
  apply (rule ext)
  apply (simp add:map_add_Some)
  apply (simp add:inv_def)
  apply (case_tac "\<exists> y. f y = Some x")
  apply (erule exE)
  apply (subgoal_tac "x \<in> ran f")
  apply (subgoal_tac "y \<in> dom f")
  apply (simp)
  apply (rule some_equality)
  apply (simp)
  apply (metis (hide_lams, mono_tags) domD domI dom_left_map_add inj_on_contraD map_add_Some map_add_dom_app_simps(3) option.sel)
  apply (simp add:dom_def)
  apply (metis ranI)
  apply (simp)
  apply (subgoal_tac "x \<notin> ran f")
  apply (simp)
  apply (rule some_equality)
  apply (simp)
  apply (metis domD dom_left_map_add map_add_Some map_add_dom_app_simps(3) option.sel)
  apply (metis dom_image_ran image_iff)
done

lemma map_comp_dom: "dom (g \<circ>\<^sub>m f) \<subseteq> dom f"
  by (metis (lifting, full_types) Collect_mono dom_def map_comp_simps(1))

lemma map_comp_assoc: "f \<circ>\<^sub>m (g \<circ>\<^sub>m h) = f \<circ>\<^sub>m g \<circ>\<^sub>m h"
proof
  fix x
  show "(f \<circ>\<^sub>m (g \<circ>\<^sub>m h)) x = (f \<circ>\<^sub>m g \<circ>\<^sub>m h) x"
  proof (cases "h x")
    case None thus ?thesis
      by (auto simp add: map_comp_def)
  next
    case (Some y) thus ?thesis
      by (auto simp add: map_comp_def)
  qed
qed

lemma map_comp_runit [simp]: "f \<circ>\<^sub>m Some = f"
  by (simp add: map_comp_def)

lemma map_comp_lunit [simp]: "Some \<circ>\<^sub>m f = f"
proof
  fix x
  show "(Some \<circ>\<^sub>m f) x = f x"
  proof (cases "f x")
    case None thus ?thesis
      by (simp add: map_comp_def)
  next
    case (Some y) thus ?thesis
      by (simp add: map_comp_def)
  qed
qed

lemma map_comp_apply [simp]: "(f \<circ>\<^sub>m g) x = g(x) >>= f"
  by (auto simp add: map_comp_def option.case_eq_if)

text {* Merging of compatible maps *}

definition comp_map :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> bool" (infixl "\<parallel>\<^sub>m" 60) where
"comp_map f g = (\<forall> x \<in> dom(f) \<inter> dom(g). the(f(x)) = the(g(x)))"

lemma comp_map_unit: "Map.empty \<parallel>\<^sub>m f"
  by (simp add: comp_map_def)

lemma comp_map_refl: "f \<parallel>\<^sub>m f"
  by (simp add: comp_map_def)

lemma comp_map_sym: "f \<parallel>\<^sub>m g \<Longrightarrow> g \<parallel>\<^sub>m f"
  by (simp add: comp_map_def)

definition merge :: "('a \<rightharpoonup> 'b) set \<Rightarrow> 'a \<rightharpoonup> 'b" where
"merge fs =
  (\<lambda> x. if (\<exists> f \<in> fs. x \<in> dom(f)) then (THE y. \<forall> f \<in> fs. x \<in> dom(f) \<longrightarrow> f(x) = y) else None)"

lemma merge_empty: "merge {} = Map.empty"
  by (simp add: merge_def)

lemma merge_singleton: "merge {f} = f"
  apply (auto intro!: ext simp add: merge_def)
  using option.collapse apply fastforce
done

text {* Conversion between lists and maps *}

definition map_of_list :: "'a list \<Rightarrow> (nat \<rightharpoonup> 'a)" where
"map_of_list xs = (\<lambda> i. if (i < length xs) then Some (xs!i) else None)"

lemma map_of_list_nil [simp]: "map_of_list [] = Map.empty"
  by (simp add: map_of_list_def)

lemma dom_map_of_list [simp]: "dom (map_of_list xs) = {0..<length xs}"
  by (auto simp add: map_of_list_def dom_def)

lemma ran_map_of_list [simp]: "ran (map_of_list xs) = set xs"
  apply (simp add: ran_def map_of_list_def)
  apply (safe)
  apply (force)
  apply (meson in_set_conv_nth)
done

definition list_of_map :: "(nat \<rightharpoonup> 'a) \<Rightarrow> 'a list" where
"list_of_map f = (if (f = Map.empty) then [] else map (the \<circ> f) [0 ..< Suc(GREATEST x. x \<in> dom f)])"

lemma list_of_map_empty [simp]: "list_of_map Map.empty = []"
  by (simp add: list_of_map_def)

definition list_of_map' :: "(nat \<rightharpoonup> 'a) \<rightharpoonup> 'a list" where
"list_of_map' f = (if (\<exists> n. dom f = {0..<n}) then Some (list_of_map f) else None)"

lemma map_of_list_inv [simp]: "list_of_map (map_of_list xs) = xs"
proof (cases "xs = []")
  case True thus ?thesis by (simp)
next
  case False
  moreover hence "(GREATEST x. x \<in> dom (map_of_list xs)) = length xs - 1"
    by (auto intro: Greatest_equality)
  moreover from False have "map_of_list xs \<noteq> Map.empty"
    by (metis ran_empty ran_map_of_list set_empty)
  ultimately show ?thesis
    by (auto simp add: list_of_map_def map_of_list_def nth_equalityI)
qed
subsection {* Map comprehension *}

text {* Map comprehension simply converts a relation built through set comprehension into a map *}

syntax
  "_Mapcompr" :: "'a \<Rightarrow> 'b \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a \<rightharpoonup> 'b"    ("(1[_ \<mapsto> _ |/_./ _])")

translations
  "_Mapcompr F G xs P" == "CONST graph_map {(F, G) | xs. P}"

lemma map_compr_eta:
  "[x \<mapsto> y | x y. (x, y) \<in>\<^sub>m f] = f"
  apply (rule ext)
  apply (auto simp add: graph_map_def)
  apply (metis (mono_tags, lifting) Domain.DomainI fst_eq_Domain mem_Collect_eq old.prod.case option.distinct(1) option.expand option.sel)
done

lemma map_compr_simple:
  "[x \<mapsto> F x y | x y. (x, y) \<in>\<^sub>m f] = (\<lambda> x. do { y \<leftarrow> f(x); Some(F x y) })"
  apply (rule ext)
  apply (auto simp add: graph_map_def image_Collect)
done

lemma map_compr_dom_simple [simp]:
  "dom [x \<mapsto> f x | x. P x] = {x. P x}"
  by (force simp add: graph_map_dom image_Collect)

lemma map_compr_ran_simple [simp]:
  "ran [x \<mapsto> f x | x. P x] = {f x | x. P x}"
  apply (auto simp add: graph_map_def ran_def)
  apply (metis (mono_tags, lifting) fst_eqD image_eqI mem_Collect_eq someI)
done

lemma map_compr_eval_simple [simp]:
  "[x \<mapsto> f x | x. P x] x = (if (P x) then Some (f x) else None)"
  by (auto simp add: graph_map_def image_Collect)

subsection {* Sorted lists from maps *}

definition sorted_list_of_map :: "('a::linorder \<rightharpoonup> 'b) \<Rightarrow> ('a \<times> 'b) list" where
"sorted_list_of_map f = map (\<lambda> k. (k, the (f k))) (sorted_list_of_set(dom(f)))"

lemma sorted_list_of_map_empty [simp]:
  "sorted_list_of_map Map.empty = []"
  by (simp add: sorted_list_of_map_def)

lemma sorted_list_of_map_inv:
  assumes "finite(dom(f))"
  shows "map_of (sorted_list_of_map f) = f"
proof -
  obtain A where "finite A" "A = dom(f)"
    by (simp add: assms)
  thus ?thesis
  proof (induct A rule: finite_induct)
    case empty thus ?thesis
      by (simp add: sorted_list_of_map_def, metis dom_empty empty_iff map_le_antisym map_le_def)
  next
    case (insert x A) thus ?thesis
      by (simp add: sorted_list_of_map_def, metis finite_insert map_of_map_keys sorted_list_of_set)
  qed
qed

declare map_member.simps [simp del]

subsection {* Extra map lemmas *}

lemma map_eqI:
  "\<lbrakk> dom f = dom g; \<forall> x\<in>dom(f). the(f x) = the(g x) \<rbrakk> \<Longrightarrow> f = g"
  by (metis domIff map_le_antisym map_le_def option.expand)

lemma map_restrict_dom_compl: "f |` (- dom f) = Map.empty"
  by (metis dom_eq_empty_conv dom_restrict inf_compl_bot)

lemma restrict_map_neg_disj:
  "dom(f) \<inter> A = {} \<Longrightarrow> f |` (- A) = f"
  by (auto simp add: restrict_map_def, rule ext, auto, metis disjoint_iff_not_equal domIff)

lemma map_plus_restrict_dist: "(f ++ g) |` A = (f |` A) ++ (g |` A)"
  by (auto simp add: restrict_map_def map_add_def)

lemma map_plus_eq_left:
  assumes "f ++ h = g ++ h"
  shows "(f |` (- dom h)) = (g |` (- dom h))"
proof -
  have "h |` (- dom h) = Map.empty"
    by (metis Compl_disjoint dom_eq_empty_conv dom_restrict)
  then have f2: "f |` (- dom h) = (f ++ h) |` (- dom h)"
    by (simp add: map_plus_restrict_dist)
  have "h |` (- dom h) = Map.empty"
    by (metis (no_types) Compl_disjoint dom_eq_empty_conv dom_restrict)
  then show ?thesis
    using f2 assms by (simp add: map_plus_restrict_dist)
qed

lemma map_add_split:
  "dom(f) = A \<union> B \<Longrightarrow> (f |` A) ++ (f |` B) = f"
  by (rule ext, auto simp add: map_add_def restrict_map_def option.case_eq_if)

lemma map_le_via_restrict:
  "f \<subseteq>\<^sub>m g \<longleftrightarrow> g |` dom(f) = f"
  by (auto simp add: map_le_def restrict_map_def dom_def fun_eq_iff)

end

author: git-vt

repo: orca

save_path: github-repos/isabelle/git-vt-orca


text:
(* Property from Productive Use of Failure in Inductive Proof,
   Andrew Ireland and Alan Bundy, JAR 1996.
   This Isabelle theory is produced using the TIP tool offered at the following website:
     https://github.com/tip-org/tools
   This file was originally provided as part of TIP benchmark at the following website:
     https://github.com/tip-org/benchmarks
   Yutaka Nagashima at CIIRC, CTU changed the TIP output theory file slightly
   to make it compatible with Isabelle2017.
   Some proofs were added by Yutaka Nagashima and Kei Shirakizawa.*)
  theory TIP_prop_13
  imports "../../Test_Base"
begin

datatype Nat = Z | S "Nat"

fun half :: "Nat => Nat" where
"half (Z) = Z"
| "half (S (Z)) = Z"
| "half (S (S z)) = S (half z)"

fun t2 :: "Nat => Nat => Nat" where
"t2 (Z) y = y"
| "t2 (S z) y = S (t2 z y)"

theorem property0 :
  "((half (t2 x x)) = x)"
  apply(induct x rule: half.induct)
    apply fastforce+
  (*Kei conjectured "\<And>n m. t2 n (S m) = t2 (S n) m"*)
  apply(subgoal_tac "\<And>n m. t2 n (S m) = t2 (S n) m")
   apply fastforce
  apply(thin_tac "half (t2 z z) = z")
  apply(induct_tac n)
   apply auto
  done

(*Conjecturing "\<And>n m. t2 n (S m) = t2 (S n) m" from
 *"\<And>z. half (t2 z z) = z \<Longrightarrow> half (t2 (S (S z)) (S (S z))) = S (S z)" is a hard task for machines.
 *In the following, we take a step-by-step approach.*)
theorem property04 :
  "((half (t2 x x)) = x)"
  apply(induct x rule: half.induct)
    apply fastforce+
  apply clarsimp
  (*Since "z" and "(S (S z))" in "t2 z (S (S z))" are of the same type and
   *"t2"'s pattern-matching is complete on the first argument...*)
  apply(subgoal_tac "(t2 z (S (S z))) = (t2 (S (S z)) z)")
   apply fastforce
  (*Since "S z" appears twice in "t2 z (S (S z)) = t2 (S (S z)) z", we generalize it.*)
  apply(subgoal_tac "\<And>z Sz. t2 z (S Sz) = t2 (S Sz) z")
   apply fastforce
  apply(thin_tac "half (t2 z z) = z")
  apply(induct_tac za)
   apply clarsimp
   apply(induct_tac Sz)
    apply fastforce+
  apply clarsimp
  apply(induct_tac Sz)
   apply fastforce+
  done

theorem property01 :
  "((half (t2 x x)) = x)"
  apply(induct x rule: half.induct)
    apply fastforce+
    (* "(t2 (S (S z)) (S (S z)))" in "half (t2 (S (S z)) (S (S z))) = S (S z)" is problematic:
   * t2's pattern matching is complete only on the first argument.
   * So, we want to rewrite "(t2 (S (S z)) (S (S z)))" to "t2 (S (S (S (S z))))".
   * Furthermore, "half"'s last clause can simplify "t2 (S (S (S (S z))))" very well. *)
  apply(subgoal_tac "(t2 (S (S z)) (S (S z))) = t2 (S (S (S (S z)))) z")
   apply fastforce
  apply clarsimp
  apply(thin_tac "half (t2 z z) = z")
  apply(subgoal_tac "t2 z (S (S z)) = t2 (S (S z)) z")
   apply fastforce
  apply(subgoal_tac "\<And>z Sz. t2 z (S Sz) = t2 (S Sz) z")
   apply fastforce
  apply(induct_tac za)
   apply clarsimp
   apply(induct_tac Sz)
    apply fastforce+
  apply clarsimp
  apply(induct_tac Sz)
   apply auto
  done

theorem property02 :
  "((half (t2 x x)) = x)"
  apply(induct x x rule:t2.induct)thm t2.induct
  quickcheck
  oops (*The induction step "\<And>z y. half (t2 y y) = y \<Longrightarrow> half (t2 y y) = y" is not useful at all.*)

theorem property03 :
  "((half (t2 x x)) = x)"
  apply(induct rule:t2.induct)thm t2.induct
  quickcheck
  oops

end


text:
(* This Isabelle theory is produced using the TIP tool offered at the following website:
     https://github.com/tip-org/tools
   This file was originally provided as part of TIP benchmark at the following website:
     https://github.com/tip-org/benchmarks
   Yutaka Nagashima at CIIRC, CTU changed the TIP output theory file slightly
   to make it compatible with Isabelle2017.
\:w
   Some proofs were added by Yutaka Nagashima.*)
  theory TIP_sort_nat_MSortTDIsSort
  imports "../../Test_Base"
begin

datatype 'a list = nil2 | cons2 "'a" "'a list"

datatype Nat = Z | S "Nat"

fun plus :: "Nat => Nat => Nat" where
  "plus (Z) y = y"
| "plus (S z) y = S (plus z y)"

fun minus :: "Nat => Nat => Nat" where
  "minus (Z) y = Z"
| "minus (S z) (S y2) = minus z y2"

fun lt :: "Nat => Nat => bool" where
  "lt x (Z) = False"
| "lt (Z) (S z) = True"
| "lt (S n) (S z) = lt n z"

fun length :: "'a list => Nat" where
  "length (nil2) = Z"
| "length (cons2 y l) = plus (S Z) (length l)"

fun le :: "Nat => Nat => bool" where
  "le (Z) y = True"
| "le (S z) (Z) = False"
| "le (S z) (S x2) = le z x2"

fun lmerge :: "Nat list => Nat list => Nat list" where
  "lmerge (nil2) y = y"
| "lmerge (cons2 z x2) (nil2) = cons2 z x2"
| "lmerge (cons2 z x2) (cons2 x3 x4) =
     (if le z x3 then cons2 z (lmerge x2 (cons2 x3 x4)) else
        cons2 x3 (lmerge (cons2 z x2) x4))"

fun take :: "Nat => 'a list => 'a list" where
  "take x y =
   (if le x Z then nil2 else
      (case y of
         nil2 => nil2
         | cons2 z xs => (case x of S x2 => cons2 z (take x2 xs))))"

fun insert :: "Nat => Nat list => Nat list" where
  "insert x (nil2) = cons2 x (nil2)"
| "insert x (cons2 z xs) =
     (if le x z then cons2 x (cons2 z xs) else cons2 z (insert x xs))"

fun isort :: "Nat list => Nat list" where
  "isort (nil2) = nil2"
| "isort (cons2 y xs) = insert y (isort xs)"

(*fun did not finish the proof*)
function idiv :: "Nat => Nat => Nat" where
  "idiv x y = (if lt x y then Z else S (idiv (minus x y) y))"
  by pat_completeness auto

fun drop :: "Nat => 'a list => 'a list" where
  "drop x y =
   (if le x Z then y else
      (case y of
         nil2 => nil2
         | cons2 z xs1 => (case x of S x2 => drop x2 xs1)))"

(*fun did not finish the proof*)
function msorttd :: "Nat list => Nat list" where
  "msorttd (nil2) = nil2"
| "msorttd (cons2 y (nil2)) = cons2 y (nil2)"
| "msorttd (cons2 y (cons2 x2 x3)) =
     (let k :: Nat = idiv (length (cons2 y (cons2 x2 x3))) (S (S Z))
     in lmerge
          (msorttd (take k (cons2 y (cons2 x2 x3))))
          (msorttd (drop k (cons2 y (cons2 x2 x3)))))"
  by pat_completeness auto

theorem property0 :
  "((msorttd xs) = (isort xs))"
  oops

end


text:
theory M
imports TermsAndClauses Sig
begin

subsection\<open>Well-typed (well-formed) terms, clauses, literals and problems\<close>

context Signature begin

text\<open>The type of a term\<close>
fun tpOf where
"tpOf (Var x) = tpOfV x"
|
"tpOf (Fn f Tl) = resOf f"

(* Well-typed terms *)
fun wt where
"wt (Var x) \<longleftrightarrow> True"
|
"wt (Fn f Tl) \<longleftrightarrow>
 wtFsym f \<and> list_all wt Tl \<and> arOf f = map tpOf Tl"

(* Well-typed atoms (atomic formulas) *)
fun wtA where
"wtA (Eq T1 T2) \<longleftrightarrow> wt T1 \<and> wt T2 \<and> tpOf T1 = tpOf T2"
|
"wtA (Pr p Tl) \<longleftrightarrow>
 wtPsym p \<and> list_all wt Tl \<and> parOf p = map tpOf Tl"

(* Well-typed literals *)
fun wtL where
"wtL (Pos a) \<longleftrightarrow> wtA a"
|
"wtL (Neg a) \<longleftrightarrow> wtA a"

(* Well-typed clauses *)
definition "wtC \<equiv> list_all wtL"

lemma wtC_append[simp]: "wtC (c1 @ c2) \<longleftrightarrow> wtC c1 \<and> wtC c2"
unfolding wtC_def by simp

(* Well-typed problems *)
definition "wtPB \<Phi> \<equiv> \<forall> c \<in> \<Phi>. wtC c"

lemma wtPB_Un[simp]: "wtPB (\<Phi>1 \<union> \<Phi>2) \<longleftrightarrow> wtPB \<Phi>1 \<and> wtPB \<Phi>2"
unfolding wtPB_def by auto

lemma wtPB_UN[simp]: "wtPB (\<Union> i \<in> I. \<Phi> i) \<longleftrightarrow> (\<forall> i \<in> I. wtPB (\<Phi> i))"
unfolding wtPB_def by auto

lemma wtPB_sappend[simp]:
assumes "wtPB \<Phi>1" and "wtPB \<Phi>2"  shows "wtPB (\<Phi>1 @@ \<Phi>2)"
using assms unfolding wtPB_def sappend_def by auto

(* Well-typed substitutions *)
definition "wtSB \<pi> \<equiv> \<forall> x. wt (\<pi> x) \<and> tpOf (\<pi> x) = tpOfV x"

lemma wtSB_wt[simp]: "wtSB \<pi> \<Longrightarrow> wt (\<pi> x)"
unfolding wtSB_def by auto

lemma wtSB_tpOf[simp]: "wtSB \<pi> \<Longrightarrow> tpOf (\<pi> x) = tpOfV x"
unfolding wtSB_def by auto

lemma wt_tpOf_subst:
assumes "wtSB \<pi>" and "wt T"
shows "wt (subst \<pi> T) \<and> tpOf (subst \<pi> T) = tpOf T"
using assms apply(induct T) by (auto simp add: list_all_iff)

lemmas wt_subst[simp] = wt_tpOf_subst[THEN conjunct1]
lemmas tpOf_subst[simp] = wt_tpOf_subst[THEN conjunct2]

lemma wtSB_o:
assumes 1: "wtSB \<pi>1" and 2: "wtSB \<pi>2"
shows "wtSB (subst \<pi>1 o \<pi>2)"
using 2 unfolding wtSB_def using 1 by auto

(* Getting variable terms for given types: *)
definition "getTvars \<sigma>l \<equiv> map Var (getVars \<sigma>l)"

lemma length_getTvars[simp]: "length (getTvars \<sigma>l) = length \<sigma>l"
unfolding getTvars_def by auto

lemma wt_getTvars[simp]: "list_all wt (getTvars \<sigma>l)"
unfolding list_all_length getTvars_def by simp

lemma wt_nth_getTvars[simp]:
"i < length \<sigma>l \<Longrightarrow> wt (getTvars \<sigma>l ! i)"
unfolding getTvars_def by auto

lemma map_tpOf_getTvars[simp]: "map tpOf (getTvars \<sigma>l) = \<sigma>l"
unfolding getTvars_def unfolding list_eq_iff by auto

lemma tpOf_nth_getTvars[simp]:
"i < length \<sigma>l \<Longrightarrow> tpOf (getTvars \<sigma>l ! i) = \<sigma>l ! i"
unfolding getTvars_def by auto

end (* context Signature *)

subsection \<open>Structures\<close>

text\<open>We split a structre into a ``type structure'' that interprets the types
and the rest of the structure that interprets the function and relation symbols.\<close>

text\<open>Type structures:\<close>

locale Tstruct =
fixes intT :: "'tp \<Rightarrow> 'univ \<Rightarrow> bool"
assumes NE_intT: "NE (intT \<sigma>)"

text\<open>Environment:\<close>

type_synonym ('tp,'univ) env = "'tp \<Rightarrow> var \<Rightarrow> 'univ"

text\<open>Structures:\<close>

locale Struct = Signature wtFsym wtPsym arOf resOf parOf +
                Tstruct intT
for wtFsym and wtPsym
and arOf :: "'fsym \<Rightarrow> 'tp list"
and resOf :: "'fsym \<Rightarrow> 'tp"
and parOf :: "'psym \<Rightarrow> 'tp list"
and intT :: "'tp \<Rightarrow> 'univ \<Rightarrow> bool"
+
fixes
    intF :: "'fsym \<Rightarrow> 'univ list \<Rightarrow> 'univ"
and intP :: "'psym \<Rightarrow> 'univ list \<Rightarrow> bool"
assumes
intF: "\<lbrakk>wtFsym f; list_all2 intT (arOf f) al\<rbrakk> \<Longrightarrow> intT (resOf f) (intF f al)"
and
dummy: "intP = intP"
begin

text\<open>Well-typed environment:\<close>

definition "wtE \<xi> \<equiv> \<forall> x. intT (tpOfV x) (\<xi> x)"

lemma wtTE_intT[simp]: "wtE \<xi> \<Longrightarrow> intT (tpOfV x) (\<xi> x)"
unfolding wtE_def dom_def by auto

(* Picking an element from the domain of a given type: *)
definition "pickT \<sigma> \<equiv> SOME a. intT \<sigma> a"

lemma pickT[simp]: "intT \<sigma> (pickT \<sigma>)"
unfolding pickT_def apply(rule someI_ex) using NE_intT by auto

text\<open>Picking a well-typed environment:\<close>

definition
"pickE (xl::var list) al \<equiv>
 SOME \<xi>. wtE \<xi> \<and> (\<forall> i < length xl. \<xi> (xl!i) = al!i)"

lemma ex_pickE:
assumes "length xl = length al"
and "distinct xl" and "\<And> i. i < length xl \<Longrightarrow> intT (tpOfV (xl!i)) (al!i)"
shows "\<exists> \<xi>. wtE \<xi> \<and> (\<forall> i < length xl. \<xi> (xl!i) = al!i)"
using assms
proof(induct rule: list_induct2)
  case Nil show ?case apply(rule exI[of _ "\<lambda> x. pickT (tpOfV x)"])
  unfolding wtE_def by auto
next
  case (Cons x xl a al)
  then obtain \<xi> where 1: "wtE \<xi>" and 2: "\<forall> i < length xl. \<xi> (xl!i) = al!i" by force
  define \<xi>' where "\<xi>' x' = (if x = x' then a else \<xi> x')" for x'
  show ?case
  proof(rule exI[of _ \<xi>'], unfold wtE_def, safe)
    fix x' show "intT (tpOfV x') (\<xi>' x')"
    using 1 Cons.prems(2)[of 0] unfolding \<xi>'_def by auto
  next
    fix i assume i: "i < length (x # xl)"
    thus "\<xi>' ((x # xl) ! i) = (a # al) ! i"
    proof(cases i)
      case (Suc j) hence j: "j < length xl" using i by auto
      have "\<not> x = (x # xl) ! i" using Suc i Cons.prems(1) by auto
      thus ?thesis using Suc using j Cons.prems(1) Cons.hyps 2 unfolding \<xi>'_def by auto
    qed(insert Cons.prems(1) Cons.hyps 2, unfold \<xi>'_def, simp)
  qed
qed

lemma wtE_pickE_pickE:
assumes "length xl = length al"
and "distinct xl" and "\<And> i. i < length xl \<Longrightarrow> intT (tpOfV (xl!i)) (al!i)"
shows "wtE (pickE xl al) \<and> (\<forall> i. i < length xl \<longrightarrow> pickE xl al (xl!i) = al!i)"
proof-
  let ?phi = "\<lambda> \<xi>. wtE \<xi> \<and> (\<forall> i < length xl. \<xi> (xl!i) = al!i)"
  show ?thesis unfolding pickE_def apply(rule someI_ex[of ?phi])
  using ex_pickE[OF assms] by simp
qed

lemmas wtE_pickE[simp] = wtE_pickE_pickE[THEN conjunct1]

lemma pickE[simp]:
assumes "length xl = length al"
and "distinct xl" and "\<And> i. i < length xl \<Longrightarrow> intT (tpOfV (xl!i)) (al!i)"
and "i < length xl"
shows "pickE xl al (xl!i) = al!i"
using assms wtE_pickE_pickE by auto

definition "pickAnyE \<equiv> pickE [] []"

lemma wtE_pickAnyE[simp]: "wtE pickAnyE"
unfolding pickAnyE_def by (rule wtE_pickE) auto

(* Interpretation of terms: *)
fun int where
"int \<xi> (Var x) = \<xi> x"
|
"int \<xi> (Fn f Tl) = intF f (map (int \<xi>) Tl)"

(* Satisfaction of atoms: *)
fun satA where
"satA \<xi> (Eq T1 T2) \<longleftrightarrow> int \<xi> T1 = int \<xi> T2"
|
"satA \<xi> (Pr p Tl) \<longleftrightarrow> intP p (map (int \<xi>) Tl)"

(* Satisfaction literals: *)
fun satL where
"satL \<xi> (Pos a) \<longleftrightarrow> satA \<xi> a"
|
"satL \<xi> (Neg a) \<longleftrightarrow> \<not> satA \<xi> a"

(* Satisfaction of clauses: *)
definition "satC \<xi> \<equiv> list_ex (satL \<xi>)"

lemma satC_append[simp]: "satC \<xi> (c1 @ c2) \<longleftrightarrow> satC \<xi> c1 \<or> satC \<xi> c2"
unfolding satC_def by auto

lemma satC_iff_set: "satC \<xi> c \<longleftrightarrow> (\<exists> l \<in> set c. satL \<xi> l)"
unfolding satC_def Bex_set[symmetric] ..

(* satisfaction of problems *)
definition "satPB \<xi> \<Phi> \<equiv> \<forall> c \<in> \<Phi>. satC \<xi> c"

lemma satPB_UN[simp]: "satPB \<xi> (\<Union> i \<in> I. \<Phi> i) \<longleftrightarrow> (\<forall> i \<in> I. satPB \<xi> (\<Phi> i))"
unfolding satPB_def by auto

lemma satPB_sappend[simp]: "satPB \<xi> (\<Phi>1 @@ \<Phi>2) \<longleftrightarrow> satPB \<xi> \<Phi>1 \<or> satPB \<xi> \<Phi>2"
unfolding satPB_def sappend_def by (fastforce simp: satC_append)

definition "SAT \<Phi> \<equiv> \<forall> \<xi>. wtE \<xi> \<longrightarrow> satPB \<xi> \<Phi>"

lemma SAT_UN[simp]: "SAT (\<Union> i \<in> I. \<Phi> i) \<longleftrightarrow> (\<forall> i \<in> I. SAT (\<Phi> i))"
unfolding SAT_def by auto

text\<open>Soundness of typing w.r.t. interpretation:\<close>

lemma wt_int:
assumes wtE: "wtE \<xi>" and wt: "wt T"
shows "intT (tpOf T) (int \<xi> T)"
using wt apply(induct T) using wtE
by (auto intro!: intF simp add: list_all2_map_map)

lemma satA_cong:
assumes "\<And>x. x \<in> varsA at \<Longrightarrow> \<xi>1 x = \<xi>2 x"
shows "satA \<xi>1 at \<longleftrightarrow> satA \<xi>2 at"
using assms int_cong[of _ \<xi>1 \<xi>2]
apply(cases at) apply(fastforce intro!: int_cong[of _ \<xi>1 \<xi>2])
apply simp by (metis (hide_lams, mono_tags) map_eq_conv)

lemma satL_cong:
assumes "\<And> x. x \<in> varsL l \<Longrightarrow> \<xi>1 x = \<xi>2 x"
shows "satL \<xi>1 l \<longleftrightarrow> satL \<xi>2 l"
using assms satA_cong[of _ \<xi>1 \<xi>2] by (cases l, auto)

lemma satC_cong:
assumes "\<And> x. x \<in> varsC c \<Longrightarrow> \<xi>1 x = \<xi>2 x"
shows "satC \<xi>1 c \<longleftrightarrow> satC \<xi>2 c"
using assms satL_cong[of _ \<xi>1 \<xi>2] unfolding satC_def varsC_def
apply (induct c) by (fastforce intro!: satL_cong[of _ \<xi>1 \<xi>2])+

lemma satPB_cong:
assumes "\<And> x. x \<in> varsPB \<Phi> \<Longrightarrow> \<xi>1 x = \<xi>2 x"
shows "satPB \<xi>1 \<Phi> \<longleftrightarrow> satPB \<xi>2 \<Phi>"
by (force simp: satPB_def varsPB_def intro!: satC_cong ball_cong assms)

lemma int_o:
"int (int \<xi> o \<rho>) T = int \<xi> (subst \<rho> T)"
apply(induct T) apply simp_all unfolding list_all_iff o_def
using map_ext by (metis (lifting, no_types))

lemmas int_subst = int_o[symmetric]

lemma int_o_subst:
"int \<xi> o subst \<rho> = int (int \<xi> o \<rho>)"
apply(rule ext) apply(subst comp_def) unfolding int_o[symmetric] ..

lemma satA_o:
"satA (int \<xi> o \<rho>) at = satA \<xi> (substA \<rho> at)"
by (cases at, simp_all add: int_o_subst int_o[of \<xi> \<rho>])

lemmas satA_subst = satA_o[symmetric]

lemma satA_o_subst:
"satA \<xi> o substA \<rho> = satA (int \<xi> o \<rho>)"
apply(rule ext) apply(subst comp_def) unfolding satA_o[symmetric] ..

lemma satL_o:
"satL (int \<xi> o \<rho>) l = satL \<xi> (substL \<rho> l)"
using satA_o[of \<xi> \<rho>] by (cases l, simp_all)

lemmas satL_subst = satL_o[symmetric]

lemma satL_o_subst:
"satL \<xi> o substL \<rho> = satL (int \<xi> o \<rho>)"
apply(rule ext) apply(subst comp_def) unfolding satL_o[symmetric] ..

lemma satC_o:
"satC (int \<xi> o \<rho>) c = satC \<xi> (substC \<rho> c)"
using satL_o[of \<xi> \<rho>] unfolding satC_def substC_def by (induct c, auto)

lemmas satC_subst = satC_o[symmetric]

lemma satC_o_subst:
"satC \<xi> o substC \<rho> = satC (int \<xi> o \<rho>)"
apply(rule ext) apply(subst comp_def) unfolding satC_o[symmetric] ..

lemma satPB_o:
"satPB (int \<xi> o \<rho>) \<Phi> = satPB \<xi> (substPB \<rho> \<Phi>)"
using satC_o[of \<xi> \<rho>] unfolding satPB_def substPB_def by auto

lemmas satPB_subst = satPB_o[symmetric]

lemma satPB_o_subst:
"satPB \<xi> o substPB \<rho> = satPB (int \<xi> o \<rho>)"
apply(rule ext) apply(subst comp_def) unfolding satPB_o[symmetric] ..

lemma wtE_o:
assumes 1: "wtE \<xi>" and 2: "wtSB \<rho>"
shows "wtE (int \<xi> o \<rho>)"
unfolding wtE_def proof
  fix x have 0: "tpOfV x = tpOf (\<rho> x)" using 2 by auto
  show "intT (tpOfV x) ((int \<xi> \<circ> \<rho>) x)" apply(subst 0) unfolding comp_def
  apply(rule wt_int[OF 1]) using 2 by auto
qed

(* fixme: unify compE and int \<xi> o \<rho>, since they are the same *)
definition "compE \<rho> \<xi> x \<equiv> int \<xi> (\<rho> x)"

lemma wtE_compE:
assumes "wtSB \<rho>" and "wtE \<xi>"  shows "wtE (compE \<rho> \<xi>)"
unfolding wtE_def using assms wt_int
unfolding wtSB_def compE_def by fastforce

lemma compE_upd: "compE (\<rho> (x := T)) \<xi> = (compE \<rho> \<xi>) (x := int \<xi> T)"
unfolding compE_def[abs_def] by auto

end (* context Struct *)

context Signature begin

(* The function symbols of: *)

fun fsyms where
"fsyms (Var x) = {}"
|
"fsyms (Fn f Tl) = {f} \<union> \<Union> (set (map fsyms Tl))"

fun fsymsA where
"fsymsA (Eq T1 T2) = fsyms T1 \<union> fsyms T2"
|
"fsymsA (Pr p Tl) = \<Union> (set (map fsyms Tl))"

fun fsymsL where
"fsymsL (Pos at) = fsymsA at"
|
"fsymsL (Neg at) = fsymsA at"

definition "fsymsC c = \<Union> (set (map fsymsL c))"

definition "fsymsPB \<Phi> = \<Union> {fsymsC c | c. c \<in> \<Phi>}"

lemma fsyms_int_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: "\<And> f. f \<in> fsyms T \<Longrightarrow> intF1 f = intF2 f"
shows "Struct.int intF1 \<xi> T = Struct.int intF2 \<xi> T"
using 0 proof(induct T)
  case (Fn f Tl)
  hence 1: "map (Struct.int intF1 \<xi>) Tl = map (Struct.int intF2 \<xi>) Tl"
  unfolding list_all_iff map_ext by auto
  show ?case
  using Fn Struct.int.simps[OF S1, of \<xi>] Struct.int.simps[OF S2, of \<xi>] apply simp
  using 1 by metis
qed (auto simp: Struct.int.simps[OF S1, of \<xi>] Struct.int.simps[OF S2, of \<xi>])

lemma fsyms_satA_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: "\<And> f. f \<in> fsymsA at \<Longrightarrow> intF1 f = intF2 f"
shows "Struct.satA intF1 intP \<xi> at \<longleftrightarrow> Struct.satA intF2 intP \<xi> at"
using 0 fsyms_int_cong[OF S1 S2]
apply(cases at)
apply(fastforce intro!: fsyms_int_cong[OF S1 S2, of _ \<xi>]
                simp: Struct.satA.simps[OF S1, of \<xi>] Struct.satA.simps[OF S2, of \<xi>])
apply (simp add: Struct.satA.simps[OF S1, of \<xi>] Struct.satA.simps[OF S2, of \<xi>])
by (metis (hide_lams, mono_tags) map_eq_conv)

lemma fsyms_satL_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: "\<And> f. f \<in> fsymsL l \<Longrightarrow> intF1 f = intF2 f"
shows "Struct.satL intF1 intP \<xi> l \<longleftrightarrow> Struct.satL intF2 intP \<xi> l"
using 0 fsyms_satA_cong[OF S1 S2]
by (cases l, auto simp: Struct.satL.simps[OF S1, of \<xi>] Struct.satL.simps[OF S2, of \<xi>])

lemma fsyms_satC_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: "\<And> f. f \<in> fsymsC c \<Longrightarrow> intF1 f = intF2 f"
shows "Struct.satC intF1 intP \<xi> c \<longleftrightarrow> Struct.satC intF2 intP \<xi> c"
using 0 fsyms_satL_cong[OF S1 S2]
unfolding Struct.satC_def[OF S1] Struct.satC_def[OF S2] fsymsC_def
apply (induct c) by (fastforce intro!: fsyms_satL_cong[OF S1 S2])+

lemma fsyms_satPB_cong:
assumes S1: "Struct wtFsym wtPsym arOf resOf intT intF1 intP"
and S2: "Struct wtFsym wtPsym arOf resOf intT intF2 intP"
and 0: "\<And> f. f \<in> fsymsPB \<Phi> \<Longrightarrow> intF1 f = intF2 f"
shows "Struct.satPB intF1 intP \<xi> \<Phi> \<longleftrightarrow> Struct.satPB intF2 intP \<xi> \<Phi>"
by (force simp: Struct.satPB_def[OF S1] Struct.satPB_def[OF S2] fsymsPB_def
          intro!: fsyms_satC_cong[OF S1 S2] ball_cong 0)

lemma fsymsPB_Un[simp]: "fsymsPB (\<Phi>1 \<union> \<Phi>2) = fsymsPB \<Phi>1 \<union> fsymsPB \<Phi>2"
unfolding fsymsPB_def by auto

lemma fsymsC_append[simp]: "fsymsC (c1 @ c2) = fsymsC c1 \<union> fsymsC c2"
unfolding fsymsC_def by auto

lemma fsymsPB_sappend_incl[simp]:
"fsymsPB (\<Phi>1 @@ \<Phi>2) \<subseteq>  fsymsPB \<Phi>1 \<union> fsymsPB \<Phi>2"
by (unfold fsymsPB_def sappend_def, fastforce)

lemma fsymsPB_sappend[simp]:
assumes 1: "\<Phi>1 \<noteq> {}" and 2: "\<Phi>2 \<noteq> {}"
shows "fsymsPB (\<Phi>1 @@ \<Phi>2) = fsymsPB \<Phi>1 \<union> fsymsPB \<Phi>2"
proof safe
  fix x
  {assume "x \<in> fsymsPB \<Phi>1"
   then obtain c1 c2 where "x \<in> fsymsC c1" and "c1 \<in> \<Phi>1" and "c2 \<in> \<Phi>2"
   using 2 unfolding fsymsPB_def by auto
   thus "x \<in> fsymsPB (\<Phi>1 @@ \<Phi>2)" unfolding sappend_def fsymsPB_def by fastforce
  }
  {assume "x \<in> fsymsPB \<Phi>2"
   then obtain c1 c2 where "x \<in> fsymsC c2" and "c1 \<in> \<Phi>1" and "c2 \<in> \<Phi>2"
   using 1 unfolding fsymsPB_def by auto
   thus "x \<in> fsymsPB (\<Phi>1 @@ \<Phi>2)" unfolding sappend_def fsymsPB_def by fastforce
  }
qed(unfold fsymsPB_def sappend_def, fastforce)

lemma Struct_upd:
assumes "Struct wtFsym wtPsym arOf resOf intT intF intP"
and "\<And> al. list_all2 intT (arOf ef) al \<Longrightarrow> intT (resOf ef) (EF al)"
shows "Struct wtFsym wtPsym arOf resOf intT (intF (ef := EF)) intP"
apply standard using assms
unfolding Struct_def Struct_axioms_def Tstruct_def by auto

end (* context Signature *)

subsection\<open>Problems\<close>

text\<open>A problem is a potentially infinitary formula in clausal form, i.e.,
a potentially infinite conjunction of clauses.\<close>

locale Problem = Signature wtFsym wtPsym arOf resOf parOf
for wtFsym wtPsym
and arOf :: "'fsym \<Rightarrow> 'tp list"
and resOf :: "'fsym \<Rightarrow> 'tp"
and parOf :: "'psym \<Rightarrow> 'tp list"
+
fixes \<Phi> :: "('fsym, 'psym) prob"
assumes wt_\<Phi>: "wtPB \<Phi>"

subsection\<open>Models of a problem\<close>

text\<open>Model of a problem:\<close>

locale Model = Problem + Struct +
assumes SAT: "SAT \<Phi>"
begin
lemma sat_\<Phi>: "wtE \<xi> \<Longrightarrow> satPB \<xi> \<Phi>"
using SAT unfolding SAT_def by auto
end

end