Theory PAC_More_Poly

(*
File:         PAC_More_Poly.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Maintainer:   Mathias Fleury, JKU
*)
theory PAC_More_Poly
imports "HOL-Library.Poly_Mapping" "HOL-Algebra.Polynomials" "Polynomials.MPoly_Type_Class"
"HOL-Algebra.Module" "HOL-Library.Countable_Set"
begin

section ‹Overview›

text ‹

One solution to check circuit of multipliers is to use algebraic method, like producing proofs on
polynomials.  We are here interested in checking PAC proofs on the Boolean ring. The idea is the
following: each variable represents an input or the output of a gate and we want to prove the
bitwise multiplication of the input bits yields the output, namely the bitwise representation of the
multiplication of the input (modulo \<^term>‹(2::nat)^n› where \<^term>‹n::nat› is the number of bits of the
circuit).

Algebraic proof systems typically reason over polynomials in a ring $\set K[X]$,
where the variables $X$ represent Boolean values.
The aim of an algebraic proof is to derive whether a polynomial $f$ can be derived from a given set of polynomials
$G = \{g_1,\dots,g_l\} \subseteq \set K[X]$ together with the Boolean value constraints
$B(X) = \{x^2_i-x_i \mid x_i \in X\}$. In algebraic terms this means to show that the polynomial \<^latex>‹$$f \in \langle G \cup B(X)\rangle$$›.

In our setting we set $\set K = \set Z$ and we treat the Boolean value constraints implicitly, i.e.,
we consider proofs in the ring \<^latex>‹$$\set Z[X]/\langle B(X)\rangle$$› to admit shorter proofs

The checker takes as input 3 files:
▸ an input file containing all polynomials that are initially present;
▸ a target (or specification) polynomial ;
▸ a proof'' file to check that contains the proof in PAC format that shows that the specification
is in the ideal generated by the polynomials present initially.

Each step of the proof is either an addition of two polynomials previously derived, a multiplication
from a previously derived polynomial and an arbitrary polynomial, and the deletion a derived
polynomial.

One restriction on the proofs compared to generic PAC proofs is that \<^term>‹(x::nat)^2 = x› in the
Boolean ring we are considering.

The checker can produce two outputs: valid (meaning that each derived polynomial in the proof has
been correctly derived and the specification polynomial was also derived at some point [either in
the proof or as input]) or invalid (without proven information what went wrong).

The development is organised as follows:
▪ 🗏‹PAC_Specification.thy› (this file) contains the specification as described above on ideals
without any peculiarities on the PAC proof format
▪ 🗏‹PAC_Checker_Specification.thy› specialises to the PAC format and enters the nondeterminism
monad to prepare the subsequent refinements.
▪ 🗏‹PAC_Checker.thy› contains the refined version where polynomials are represented as lists.
▪ 🗏‹PAC_Checker_Synthesis.thy› contains the efficient implementation with imperative data
structure like a hash set.
▪ 🗏‹PAC_Checker_MLton.thy› contains the code generation and the command to compile the file with
the ML compiler MLton.

Here is an example of a proof and an input file (taken from the appendix of our FMCAD
paper~\cite{KaufmannFleuryBiere-FMCAD20}, available at 🌐‹http://fmv.jku.at/pacheck_pasteque›):
▩‹
<res.input>      <res.proof>
1 x*y;           3  = fz, -z+1;
2 y*z-y-z+1;     4  *  3,  y-1, -fz*y+fz-y*z+y+z-1;
5  +  2,    4, -fz*y+fz;
2  d;
4  d;
<res.target>      6  *  1,   fz, fz*x*y;
-x*z+x;          1  d;
7  *  5,    x, -fz*x*y+fz*x;
8  +  6,    7, fz*x;
9  *  3,    x, -fz*x-x*z+x;
10  +  8,    9, -x*z+x;
›

Each line starts with a number that is used to index the (conclusion) polynomial. In the proof,
there are four kind of steps:
▸ ▩‹3 = fz, -z+1;› is an extension that introduces a new variable (in this case ▩‹fz›);
▸ ▩‹4  *  3,  y-1, -fz*y+fz-y*z+y+z-1;› is a multiplication of the existing polynomial with
index 3 by the arbitrary polynomial ▩‹y-1› and generates the new polynomial
▩‹-fz*y+fz-y*z+y+z-1› with index 4;
▸ ▩‹5  +  2,    4, -fz*y+fz;› is an addition of the existing polynomials with
index 2 and 4 and generates the new polynomial ▩‹-fz*y+fz› with index 5;
▸ ▩‹1  d;› deletes the polynomial with index 1 and it cannot be reused in subsequent steps.

Remark that unlike DRAT checker, we do forward checking and check every derived polynomial. The
target polynomial can also be part of the input file.
›

section ‹Libraries›

subsection ‹More Polynomials›

text ‹

Here are more theorems on polynomials. Most of these facts are
extremely trivial and should probably be generalised and moved to
the Isabelle distribution.
›

‹Const⇩0 (a + b) = Const⇩0 a + Const⇩0 b›
by transfer

lemma Const_mult:
‹Const (a * b) = Const a * Const b›
by transfer (simp add: Const⇩0_def times_monomial_monomial)

lemma Const⇩0_mult:
‹Const⇩0 (a * b) = Const⇩0 a * Const⇩0 b›
by transfer (simp add: Const⇩0_def times_monomial_monomial)

lemma Const0[simp]:
‹Const 0 = 0›
by transfer (simp add: Const⇩0_def)

lemma (in -) Const_uminus[simp]:
‹Const (-n) = - Const n›
by transfer (auto simp: Const⇩0_def monomial_uminus)

lemma [simp]: ‹Const⇩0 0 = 0›
‹MPoly 0 = 0›
by (auto simp: Const⇩0_def zero_mpoly_def)

‹Const (a + b) = Const a + Const b›

instance mpoly :: (comm_semiring_1) comm_semiring_1
by standard

lemma degree_uminus[simp]:
‹degree (-A) x' = degree A x'›
by (auto simp: degree_def uminus_mpoly.rep_eq)

lemma degree_sum_notin:
‹x' ∉ vars B ⟹ degree (A + B) x' = degree A x'›
apply (auto simp: degree_def)
apply (rule arg_cong[of _ _ Max])
apply standard+
apply (auto simp: plus_mpoly.rep_eq UN_I UnE image_iff in_keys_iff subsetD vars_def lookup_add
dest: keys_add intro: in_keys_plusI1 cong: ball_cong_simp)
done

lemma degree_notin_vars:
‹x ∉ (vars B) ⟹ degree (B :: 'a :: {monoid_add} mpoly) x = 0›
using degree_sum_notin[of x B 0]
by auto

lemma not_in_vars_coeff0:
‹x ∉ vars p ⟹ MPoly_Type.coeff p (monomial (Suc 0) x) = 0›
by (subst not_not[symmetric], subst coeff_keys[symmetric])
(auto simp: vars_def)

"p ∈ keys (f + g) ⟹ p ∈ keys f ∪ keys g"
by transfer auto

‹finite A ⟹ keys (mapping_of (∑v ∈ A. f v)) ⊆ ⋃(keys  mapping_of  f  UNIV)›
by (induction A rule: finite_induct)
(auto simp add: zero_mpoly.rep_eq plus_mpoly.rep_eq

lemma vars_sum_vars_union:
fixes f :: ‹int mpoly ⇒ int mpoly›
assumes ‹finite {v. f v ≠ 0}›
shows ‹vars (∑v | f v ≠ 0. f v * v) ⊆ ⋃(vars  {v. f v ≠ 0}) ∪ ⋃(vars  f  {v. f v ≠ 0})›
(is ‹?A ⊆ ?B›)
proof
fix p
assume ‹p ∈ vars (∑v | f v ≠ 0. f v * v)›
then obtain x where ‹x ∈ keys (mapping_of (∑v | f v ≠ 0. f v * v))› and
p: ‹p ∈ keys x›
by (auto simp: vars_def times_mpoly.rep_eq simp del: keys_mult)
then have ‹x ∈ (⋃x. keys (mapping_of (f x) * mapping_of x))›
using keys_mapping_sum_add[of ‹{v. f v ≠ 0}› ‹λx. f x * x›] assms
by (auto simp: vars_def times_mpoly.rep_eq)
then have ‹x ∈ (⋃x. {a+b| a b. a ∈ keys (mapping_of (f x)) ∧ b ∈ keys (mapping_of x)})›
using Union_mono[OF ] keys_mult by fast
then show ‹p ∈ ?B›
using p by (force simp: vars_def zero_mpoly.rep_eq dest!: keys_add')
qed

lemma vars_in_right_only:
"x ∈ vars q ⟹ x ∉ vars p ⟹ x ∈ vars (p+q)"
unfolding  vars_def keys_def plus_mpoly.rep_eq lookup_plus_fun
apply clarify
subgoal for xa
by (auto simp: vars_def keys_def plus_mpoly.rep_eq
lookup_plus_fun intro!: exI[of _ xa] dest!: spec[of _ xa])
done

lemma [simp]:
‹vars 0 = {}›
by (simp add: vars_def zero_mpoly.rep_eq)

lemma vars_Un_nointer:
‹keys (mapping_of p) ∩  keys (mapping_of q) = {} ⟹ vars (p + q) = vars p ∪ vars q›
by (auto simp: vars_def plus_mpoly.rep_eq simp flip: More_MPoly_Type.keys_add dest!: keys_add')

lemmas [simp] = zero_mpoly.rep_eq

lemma polynomial_sum_monoms:
fixes p :: ‹'a :: {comm_monoid_add,cancel_comm_monoid_add} mpoly›
shows
‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))›
‹keys (mapping_of p) ⊆ I ⟹ finite I ⟹ p = (∑x∈I. MPoly_Type.monom x (MPoly_Type.coeff p x))›
proof -
define J where ‹J ≡ keys (mapping_of p)›
define a where ‹a x ≡ coeff p x› for x
have ‹finite (keys (mapping_of p))›
by auto
have ‹p = (∑x∈I. MPoly_Type.monom x (MPoly_Type.coeff p x))›
if ‹finite I› and ‹keys (mapping_of p) ⊆ I›
for I
using that
unfolding a_def
proof (induction I arbitrary: p rule: finite_induct)
case empty
then have ‹p = 0›
using empty coeff_all_0 coeff_keys by blast
then show ?case using empty by (auto simp: zero_mpoly.rep_eq)
next
case (insert x F) note fin = this(1) and xF = this(2) and IH = this(3) and
incl = this(4)
let ?p = ‹p - MPoly_Type.monom x (MPoly_Type.coeff p x)›
have H: ‹⋀xa. x ∉ F ⟹ xa ∈ F ⟹
MPoly_Type.monom xa (MPoly_Type.coeff (p - MPoly_Type.monom x (MPoly_Type.coeff p x)) xa) =
MPoly_Type.monom xa (MPoly_Type.coeff p xa)›
by (metis (mono_tags, hide_lams) add_diff_cancel_right' remove_term_coeff
remove_term_sum when_def)
have ‹?p = (∑xa∈F. MPoly_Type.monom xa (MPoly_Type.coeff ?p xa))›
apply (rule IH)
using incl apply -
by standard (smt Diff_iff Diff_insert_absorb add_diff_cancel_right'
remove_term_keys remove_term_sum subsetD xF)
also have ‹... = (∑xa∈F. MPoly_Type.monom xa (MPoly_Type.coeff p xa))›
by (use xF in ‹auto intro!: sum.cong simp: H›)
finally show ?case
apply (subst (asm) remove_term_sum[of x p, symmetric])
apply (subst remove_term_sum[of x p, symmetric])
using xF fin by (auto simp: ac_simps)
qed
from this[of I] this[of J] show
‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))›
‹keys (mapping_of p) ⊆ I ⟹ finite I ⟹ p = (∑x∈I. MPoly_Type.monom x (MPoly_Type.coeff p x))›
by (auto simp: J_def)
qed

lemma vars_mult_monom:
fixes p :: ‹int mpoly›
shows ‹vars (p * (monom (monomial (Suc 0) x') 1)) = (if p = 0 then {} else insert x' (vars p))›
proof -

let ?v = ‹monom (monomial (Suc 0) x') 1›
have
p: ‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))› (is ‹_ = (∑x ∈ ?I. ?f x)›)
using polynomial_sum_monoms(1)[of p] .
have pv: ‹p * ?v = (∑x ∈ ?I. ?f x * ?v)›
by (subst p) (auto simp:  field_simps sum_distrib_left)
define I where ‹I ≡ ?I›
have in_keysD: ‹x ∈ keys (mapping_of (∑x∈I. MPoly_Type.monom x (h x)))  ⟹ x ∈ I›
if ‹finite I› for I and h :: ‹_ ⇒ int› and x
using that by (induction rule: finite_induct)
(force simp: monom.rep_eq empty_iff insert_iff keys_single coeff_monom
simp: coeff_keys simp flip: coeff_add
have in_keys: ‹keys (mapping_of (∑x∈I. MPoly_Type.monom x (h x))) = (⋃x ∈ I. (if h x  = 0 then {} else {x}))›
if ‹finite I› for I and h :: ‹_ ⇒ int› and x
supply in_keysD[dest]
using that by (induction rule: finite_induct)
(auto simp: plus_mpoly.rep_eq MPoly_Type_Class.keys_plus_eqI)

have H[simp]: ‹vars ((∑x∈I. MPoly_Type.monom x (h x))) = (⋃x∈I. (if h x  = 0 then {} else keys x))›
if ‹finite I› for I and h :: ‹_ ⇒ int›
using that by (auto simp: vars_def in_keys)

have sums: ‹(∑x∈I.
MPoly_Type.monom (x + a') (c x)) =
(∑x∈ (λx. x + a')  I.
MPoly_Type.monom x (c (x - a')))›
if ‹finite I› for I a' c q
using that apply (induction rule: finite_induct)
subgoal by auto
subgoal
unfolding image_insert by (subst sum.insert) auto
done
have non_zero_keysEx: ‹p ≠ 0 ⟹ ∃a. a ∈ keys (mapping_of p)› for p :: ‹int mpoly›
using mapping_of_inject by (fastforce simp add: ex_in_conv)
have ‹finite I› ‹keys (mapping_of p) ⊆ I›
unfolding I_def by auto
then show
‹vars (p * (monom (monomial (Suc 0) x') 1)) = (if p = 0 then {} else insert x' (vars p))›
apply (subst pv, subst I_def[symmetric], subst mult_monom)
apply (auto simp: mult_monom sums I_def)
using Poly_Mapping.keys_add vars_def apply fastforce
apply (auto dest!: non_zero_keysEx)
apply (rule_tac x= ‹a + monomial (Suc 0) x'› in bexI)
apply (auto simp: coeff_keys)
apply (auto simp: vars_def)
apply (rule_tac x= ‹xa + monomial (Suc 0) x'› in bexI)
apply (auto simp: coeff_keys)
done
qed

term ‹(x', u, lookup u x', A)›
lemma in_mapping_mult_single:
‹x ∈ (λx. lookup x x')  keys (A * (Var⇩0 x' :: (nat ⇒⇩0 nat) ⇒⇩0 'b :: {monoid_mult,zero_neq_one,semiring_0})) ⟷
x > 0 ∧ x - 1 ∈ (λx. lookup x x')  keys (A)›
apply (standard+; clarify)
subgoal
apply (auto  elim!: in_keys_timesE simp: lookup_add)
apply (auto simp: keys_def lookup_times_monomial_right Var⇩0_def lookup_single image_iff)
done
subgoal
apply (auto  elim!: in_keys_timesE simp: lookup_add)
apply (auto simp: keys_def lookup_times_monomial_right Var⇩0_def lookup_single image_iff)
done
subgoal for  xa
apply (auto  elim!: in_keys_timesE simp: lookup_add)
apply (auto simp: keys_def lookup_times_monomial_right Var⇩0_def lookup_single image_iff lookup_add
intro!: exI[of _ ‹xa + Poly_Mapping.single x' 1›])
done
done

lemma Max_Suc_Suc_Max:
‹finite A ⟹ A ≠ {} ⟹ Max (insert 0 (Suc  A)) =
Suc (Max (insert 0 A))›
by (induction rule: finite_induct)
(auto simp: hom_Max_commute)

lemma [simp]:
‹keys (Var⇩0 x' :: ('a ⇒⇩0 nat) ⇒⇩0 'b :: {zero_neq_one}) = {Poly_Mapping.single x' 1}›
by (auto simp: Var⇩0_def)

lemma degree_mult_Var:
‹degree (A * Var x') x' = (if A = 0 then 0 else Suc (degree A x'))› for A :: ‹int mpoly›
proof -
have [simp]: ‹A ≠ 0 ⟹
Max (insert 0 ((λx. Suc (lookup x x'))  keys (mapping_of A))) =
Max (insert (Suc 0) ((λx. Suc (lookup x x'))  keys (mapping_of A)))›
unfolding image_image[of Suc ‹λx. lookup x x'›, symmetric] image_insert[symmetric]
by (subst Max_Suc_Suc_Max, use mapping_of_inject in fastforce, use mapping_of_inject in fastforce)+
have ‹A ≠ 0 ⟹
Max (insert 0
((λx. lookup x x')
keys (mapping_of A * mapping_of (Var x')))) =
Suc (Max (insert 0 ((λm. lookup m x')  keys (mapping_of A))))›
by (subst arg_cong[of _ ‹insert 0
(Suc  ((λx. lookup x x')  keys (mapping_of A)))› Max])
(auto simp: image_image Var.rep_eq lookup_plus_fun in_mapping_mult_single
hom_Max_commute Max_Suc_Suc_Max
elim!: in_keys_timesE  split: if_splits)
then show ?thesis
by (auto simp: degree_def times_mpoly.rep_eq
intro!: arg_cong[of _ ‹insert 0
(Suc  ((λx. lookup x x')  keys (mapping_of A)))› Max])
qed

lemma degree_mult_Var':
‹degree (Var x' * A) x' = (if A = 0 then 0 else Suc (degree A x'))› for A :: ‹int mpoly›
by (simp add: degree_mult_Var semiring_normalization_rules(7))

lemma degree_times_le:
‹degree (A * B) x ≤ degree A x + degree B x›
by (auto simp: degree_def times_mpoly.rep_eq
dest!: set_rev_mp[OF _ Poly_Mapping.keys_add]
elim!: in_keys_timesE)

lemma monomial_inj:
"monomial c s = monomial (d::'b::zero_neq_one) t ⟷ (c = 0 ∧ d = 0) ∨ (c = d ∧ s = t)"
by (fastforce simp add: monomial_inj Poly_Mapping.single_def
poly_mapping.Abs_poly_mapping_inject when_def fun_eq_iff
cong: if_cong
split: if_splits)

lemma MPoly_monomial_power':
‹MPoly (monomial 1 x') ^ (n+1) =  MPoly (monomial (1) (((λx. x + x') ^^ n) x'))›
by (induction n)
(auto simp: times_mpoly.abs_eq mult_single ac_simps)

lemma MPoly_monomial_power:
‹n > 0 ⟹ MPoly (monomial 1 x') ^ (n) =  MPoly (monomial (1) (((λx. x + x') ^^ (n - 1)) x'))›
using MPoly_monomial_power'[of _ ‹n-1›]
by auto

lemma vars_uminus[simp]:
‹vars (-p) = vars p›
by (auto simp: vars_def uminus_mpoly.rep_eq)

lemma coeff_uminus[simp]:
‹MPoly_Type.coeff (-p) x = -MPoly_Type.coeff p x›
by (auto simp: coeff_def uminus_mpoly.rep_eq)

definition decrease_key::"'a ⇒ ('a ⇒⇩0 'b::{monoid_add, minus,one}) ⇒ ('a ⇒⇩0 'b)" where
"decrease_key k0 f = Abs_poly_mapping (λk. if k = k0 ∧ lookup f k ≠ 0 then lookup f k - 1 else lookup f k)"

lemma remove_key_lookup:
"lookup (decrease_key k0 f) k = (if k = k0 ∧ lookup f k ≠ 0 then lookup f k - 1 else lookup f k)"
unfolding decrease_key_def using finite_subset apply (simp add: )
apply (subst lookup_Abs_poly_mapping)
apply (auto intro: finite_subset[of _ ‹{x. lookup f x ≠ 0}›])
apply (subst lookup_Abs_poly_mapping)
apply (auto intro: finite_subset[of _ ‹{x. lookup f x ≠ 0}›])
done

lemma polynomial_split_on_var:
fixes p :: ‹'a :: {comm_monoid_add,cancel_comm_monoid_add,semiring_0,comm_semiring_1} mpoly›
obtains q r where
‹p = monom (monomial (Suc 0) x') 1 * q + r› and
‹x' ∉ vars r›
proof -
have [simp]: ‹{x ∈ keys (mapping_of p). x' ∈ keys x} ∪
{x ∈ keys (mapping_of p). x' ∉ keys x} = keys (mapping_of p)›
by auto
have
‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))› (is ‹_ = (∑x ∈ ?I. ?f x)›)
using polynomial_sum_monoms(1)[of p] .
also have ‹... = (∑x∈ {x ∈ ?I. x' ∈ keys x}. ?f x) + (∑x∈ {x ∈ ?I. x' ∉ keys x}. ?f x)› (is ‹_ = ?pX + ?qX›)
by (subst comm_monoid_add_class.sum.union_disjoint[symmetric]) auto
finally have 1: ‹p = ?pX + ?qX› .
have H: ‹0 < lookup x x' ⟹ (λk. (if x' = k then Suc 0 else 0) +
(if k = x' ∧ 0 < lookup x k then lookup x k - 1
else lookup x k)) = lookup x› for x x'
by auto
have [simp]: ‹finite {x. 0 < (Suc 0 when x' = x)}› for x' :: nat and x
by (smt bounded_nat_set_is_finite lessI mem_Collect_eq neq0_conv when_cong when_neq_zero)
have H: ‹x' ∈ keys x ⟹ monomial (Suc 0) x' + Abs_poly_mapping (λk. if k = x' ∧ 0 < lookup x k then lookup x k - 1 else lookup x k) = x›
for x and x' :: nat
apply (simp only: keys_def single.abs_eq)
apply (subst plus_poly_mapping.abs_eq)
by (auto simp: eq_onp_def when_def H
intro!: finite_subset[of ‹{xa. (xa = x' ∧ 0 < lookup x xa ⟶ Suc 0 < lookup x x') ∧
(xa ≠ x' ⟶ 0 < lookup x xa)}› ‹{xa. 0 < lookup x xa}›])

have [simp]: ‹x' ∈ keys x ⟹
MPoly_Type.monom (monomial (Suc 0) x' + decrease_key x' x) n =
MPoly_Type.monom x n› for x n and x'
apply (subst mpoly.mapping_of_inject[symmetric], subst poly_mapping.lookup_inject[symmetric])
unfolding mapping_of_monom lookup_single
apply (auto intro!: ext simp: decrease_key_def when_def H)
done
have pX: ‹?pX = monom (monomial (Suc 0) x') 1 * (∑x∈ {x ∈ ?I. x' ∈ keys x}. MPoly_Type.monom (decrease_key x' x) (MPoly_Type.coeff p x))›
(is ‹_ = _ * ?pX'›)
by (subst sum_distrib_left, subst mult_monom)
(auto intro!: sum.cong)
have ‹x' ∉ vars ?qX›
using vars_setsum[of ‹{x. x ∈ keys (mapping_of p) ∧ x' ∉ keys x}› ‹?f›]
by (auto dest!: vars_monom_subset[unfolded subset_eq Ball_def, rule_format])
then show ?thesis
using that[of ?pX' ?qX]
unfolding pX[symmetric] 1[symmetric]
by blast
qed

lemma polynomial_split_on_var2:
fixes p :: ‹int mpoly›
assumes ‹x' ∉ vars s›
obtains q r where
‹p = (monom (monomial (Suc 0) x') 1 - s) * q + r› and
‹x' ∉ vars r›
proof -
have eq[simp]: ‹monom (monomial (Suc 0) x') 1 = Var x'›
by (simp add: Var.abs_eq Var⇩0_def monom.abs_eq)
have ‹∀m ≤ n. ∀P::int mpoly. degree P x' < m ⟶ (∃A B. P = (Var x' - s) * A + B ∧ x' ∉ vars B)› for n
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
then have IH: ‹m≤n ⟹ MPoly_Type.degree P x' < m ⟹
(∃A B. P = (Var x' - s) * A + B ∧ x' ∉ vars B)› for m P
by fast
show ?case
proof (intro allI impI)
fix m and P :: ‹int mpoly›
assume ‹m ≤ Suc n› and deg: ‹MPoly_Type.degree P x' < m›
consider
‹m ≤ n› |
‹m = Suc n›
using ‹m ≤ Suc n› by linarith
then show ‹∃A B. P = (Var x' - s) * A + B ∧ x' ∉ vars B›
proof cases
case 1
then show ‹?thesis›
using Suc deg by blast
next
case [simp]: 2
obtain A B where
P: ‹P = Var x' * A + B› and
‹x' ∉ vars B›
using polynomial_split_on_var[of P x'] unfolding eq by blast
have P': ‹P = (Var x' - s) * A + (s * A + B)›
by (auto simp: field_simps P)
have ‹A = 0 ∨ degree (s * A) x' < degree P x'›
using deg ‹x' ∉ vars B› ‹x' ∉ vars s› degree_times_le[of s A x'] deg
unfolding P
by (auto simp: degree_sum_notin degree_mult_Var' degree_mult_Var degree_notin_vars
split: if_splits)
then obtain A' B' where
sA: ‹s*A = (Var x' - s) * A' + B'› and
‹x' ∉ vars B'›
using IH[of ‹m-1› ‹s*A›] deg ‹x' ∉ vars B› that[of 0 0]
by (cases ‹0 < n›) (auto dest!: vars_in_right_only)
have ‹P = (Var x' - s) * (A + A') + (B' + B)›
unfolding P' sA by (auto simp: field_simps)
moreover have ‹x' ∉ vars (B' + B)›
using ‹x' ∉ vars B'›  ‹x' ∉ vars B›
by (meson UnE subset_iff vars_add)
ultimately show ?thesis
by fast
qed
qed
qed
then show ?thesis
using that unfolding eq
by blast
qed

lemma finit_whenI[intro]:
‹finite  {x. (0 :: nat) < (y x)} ⟹ finite {x. 0 < (y x when x ≠ x')}›
apply (rule finite_subset)
defer apply assumption
apply (auto simp: when_def)
done

lemma polynomial_split_on_var_diff_sq2:
fixes p :: ‹int mpoly›
obtains q r s where
‹p = monom (monomial (Suc 0) x') 1 * q + r + s * (monom (monomial (Suc 0) x') 1^2 - monom (monomial (Suc 0) x') 1)› and
‹x' ∉ vars r› and
‹x' ∉ vars q›
proof -
let ?v = ‹monom (monomial (Suc 0) x') 1 :: int mpoly›
have H: ‹n < m ⟹ n > 0 ⟹ ∃q. ?v^n = ?v + q * (?v^2 - ?v)› for n m :: nat
proof (induction m arbitrary: n)
case 0
then show ?case by auto
next
case (Suc m n) note IH = this(1-)
consider
‹n < m› |
‹m = n› ‹n > 1› |
‹n = 1›
using IH
by (cases ‹n < m›; cases n) auto
then show ?case
proof cases
case 1
then show ?thesis using IH by auto
next
case 2
have eq: ‹?v^(n) = ((?v :: int mpoly) ^ (n-2)) * (?v^2-?v) + ?v^(n-1)›
using 2 by (auto simp: field_simps power_eq_if
ideal.scale_right_diff_distrib)
obtain q where
q: ‹?v^(n-1) = ?v + q * (?v^2 - ?v)›
using IH(1)[of ‹n-1›] 2
by auto
show ?thesis
using q unfolding eq
by (auto intro!: exI[of _ ‹?v ^ (n - 2) + q›] simp: distrib_right)
next
case 3
then show ‹?thesis›
by auto
qed
qed
have H: ‹n>0 ⟹ ∃q. ?v^n = ?v + q * (?v^2-?v)› for n
using H[of n ‹n+1›]
by auto
obtain qr :: ‹nat ⇒ int mpoly› where
qr: ‹n > 0 ⟹ ?v^n = ?v + qr n * (?v^2-?v)› for n
using H by metis
have vn: ‹(if lookup x x' = 0 then 1 else Var x' ^ lookup x x') =
(if lookup x x' = 0 then 1 else ?v) + (if lookup x x' = 0 then 0 else 1) * qr (lookup x x') * (?v^2-?v)› for x
by (simp add: qr[symmetric] Var_def Var⇩0_def monom.abs_eq[symmetric] cong: if_cong)

have q: ‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))›
by (rule polynomial_sum_monoms(1)[of p])
have [simp]:
‹lookup x x' = 0 ⟹
Abs_poly_mapping (λk. lookup x k when k ≠ x') = x› for x
by (cases x, auto simp: poly_mapping.Abs_poly_mapping_inject)
(auto intro!: ext simp: when_def)
have [simp]: ‹finite {x. 0 < (a when x' = x)}› for a :: nat
by (metis (no_types, lifting) infinite_nat_iff_unbounded less_not_refl lookup_single lookup_single_not_eq mem_Collect_eq)

have [simp]: ‹((λx. x + monomial (Suc 0) x') ^^ (n))
(monomial (Suc 0) x') = Abs_poly_mapping (λk. (if k = x' then n+1 else 0))› for n
by (induction n)
(auto simp: single_def Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def cong:if_cong)
have [simp]: ‹0 < lookup x x' ⟹
Abs_poly_mapping (λk. lookup x k when k ≠ x') +
Abs_poly_mapping (λk. if k = x' then lookup x x' - Suc 0 + 1 else 0) =
x› for x
apply (cases x, auto simp: poly_mapping.Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def)
apply (subst plus_poly_mapping.abs_eq)
apply (auto simp: poly_mapping.Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def)
apply (subst Abs_poly_mapping_inject)
apply auto
done
define f where
‹f x = (MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)) *
(if lookup x x' = 0 then 1 else Var x' ^ (lookup x x'))› for x
have f_alt_def: ‹f x = MPoly_Type.monom x (MPoly_Type.coeff p x)› for x
by (auto simp: f_def monom_def remove_key_def Var_def MPoly_monomial_power Var⇩0_def
mpoly.MPoly_inject monomial_inj times_mpoly.abs_eq
times_mpoly.abs_eq mult_single)
have p: ‹p = (∑x∈keys (mapping_of p).
MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
(if lookup x x' = 0 then 1 else ?v)) +
(∑x∈keys (mapping_of p).
MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
(if lookup x x' = 0 then 0
else 1) * qr (lookup x x')) *
(?v⇧2 - ?v)›
(is ‹_ = ?a + ?v2v›)
apply (subst q)
unfolding f_alt_def[symmetric, abs_def] f_def vn semiring_class.distrib_left
comm_semiring_1_class.semiring_normalization_rules(18) semiring_0_class.sum_distrib_right
by (simp add: semiring_class.distrib_left
sum.distrib)

have I: ‹keys (mapping_of p) = {x ∈ keys (mapping_of p). lookup x x' = 0} ∪ {x ∈ keys (mapping_of p). lookup x x' ≠ 0}›
by auto

have ‹p = (∑x | x ∈ keys (mapping_of p) ∧ lookup x x' = 0.
MPoly_Type.monom x (MPoly_Type.coeff p x)) +
(∑x | x ∈ keys (mapping_of p) ∧ lookup x x' ≠ 0.
MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)) *
(MPoly_Type.monom (monomial (Suc 0) x') 1) +
(∑x | x ∈ keys (mapping_of p) ∧ lookup x x' ≠ 0.
MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
qr (lookup x x')) *
(?v⇧2 - ?v)›
(is ‹p = ?A + ?B * _ + ?C * _›)
unfolding semiring_0_class.sum_distrib_right[of _ _ ‹(MPoly_Type.monom (monomial (Suc 0) x') 1)›]
apply (subst p)
apply (subst (2)I)
apply (subst I)
apply auto[3]
apply auto[3]
apply (subst (4) sum.cong[OF refl, of _ _ ‹λx. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
qr (lookup x x')›])
apply (auto; fail)
apply (subst (3) sum.cong[OF refl, of _ _ ‹λx. 0›])
apply (auto; fail)
apply (subst (2) sum.cong[OF refl, of _ _ ‹λx. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
(MPoly_Type.monom (monomial (Suc 0) x') 1)›])
apply (auto; fail)
apply (subst (1) sum.cong[OF refl, of _ _ ‹λx. MPoly_Type.monom x (MPoly_Type.coeff p x)›])
by (auto simp: f_def simp flip: f_alt_def)

moreover have ‹x' ∉ vars ?A›
using vars_setsum[of ‹{x ∈ keys (mapping_of p). lookup x x' = 0}›
‹λx. MPoly_Type.monom x (MPoly_Type.coeff p x)›]
apply auto
apply (drule set_rev_mp, assumption)
apply (auto dest!: lookup_eq_zero_in_keys_contradict)
by (meson lookup_eq_zero_in_keys_contradict subsetD vars_monom_subset)
moreover have ‹x' ∉ vars ?B›
using vars_setsum[of ‹{x ∈ keys (mapping_of p). lookup x x' ≠ 0}›
‹λx. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)›]
apply auto
apply (drule set_rev_mp, assumption)
apply (auto dest!: lookup_eq_zero_in_keys_contradict)
apply (drule subsetD[OF vars_monom_subset])
apply (auto simp: remove_key_keys[symmetric])
done
ultimately show ?thesis apply -
apply (rule that[of ?B ?A ?C])
apply (auto simp: ac_simps)
done
qed

lemma polynomial_decomp_alien_var:
fixes q A b :: ‹int mpoly›
assumes
q: ‹q = A * (monom (monomial (Suc 0) x') 1) + b› and
x: ‹x' ∉ vars q› ‹x' ∉ vars b›
shows
‹A = 0› and
‹q = b›
proof -
let ?A = ‹A * (monom (monomial (Suc 0) x') 1)›
have ‹?A = q - b›
using arg_cong[OF q, of ‹λa. a - b›]
by auto
moreover have ‹x' ∉ vars (q - b)›
using x vars_in_right_only
by fastforce
ultimately have ‹x' ∉ vars (?A)›
by simp
then have ‹?A = 0›
by (auto simp: vars_mult_monom split: if_splits)
moreover have ‹?A = 0 ⟹ A = 0›
by (metis empty_not_insert mult_zero_left vars_mult_monom)
ultimately show ‹A = 0›
by blast
then show ‹q = b›
using q by auto
qed

lemma polynomial_decomp_alien_var2:
fixes q A b :: ‹int mpoly›
assumes
q: ‹q = A * (monom (monomial (Suc 0) x') 1 + p) + b› and
x: ‹x' ∉ vars q› ‹x' ∉ vars b› ‹x' ∉ vars p›
shows
‹A = 0› and
‹q = b›
proof -
let ?x = ‹monom (monomial (Suc 0) x') 1›
have x'[simp]: ‹?x = Var x'›
by (simp add: Var.abs_eq Var⇩0_def monom.abs_eq)
have ‹∃n Ax A'. A = ?x * Ax + A' ∧ x' ∉ vars A' ∧ degree Ax x' = n›
using polynomial_split_on_var[of A x'] by metis
from wellorder_class.exists_least_iff[THEN iffD1, OF this] obtain Ax A' n where
A: ‹A = Ax * ?x + A'› and
‹x' ∉ vars A'› and
n: ‹MPoly_Type.degree Ax x' = n› and
H: ‹⋀m Ax A'. m < n ⟶
A ≠ Ax * MPoly_Type.monom (monomial (Suc 0) x') 1 + A' ∨
x' ∈ vars A' ∨ MPoly_Type.degree Ax x' ≠ m›
unfolding wellorder_class.exists_least_iff[of ‹λn. ∃Ax A'. A = Ax * ?x + A' ∧ x' ∉ vars A' ∧
degree Ax x' = n›]
by (auto simp: field_simps)

have ‹q = (A + Ax * p) * monom (monomial (Suc 0) x') 1 + (p * A' + b)›
unfolding q A by (auto simp: field_simps)
moreover have ‹x' ∉ vars q› ‹x' ∉ vars (p * A' + b)›
using x ‹x' ∉ vars A'›
by (smt UnE add.assoc add.commute calculation subset_iff vars_in_right_only vars_mult)+
ultimately have ‹A + Ax * p = 0› ‹q = p * A' + b›
by (rule polynomial_decomp_alien_var)+

have A': ‹A' = -Ax * ?x - Ax * p›
using ‹A + Ax * p = 0› unfolding A
mult_minus_left)

have ‹A = - (Ax * p)›
using A unfolding A'
apply auto
done

obtain Axx Ax' where
Ax: ‹Ax = ?x * Axx + Ax'› and
‹x' ∉ vars Ax'›
using polynomial_split_on_var[of Ax x'] by metis

have ‹A = ?x * (- Axx * p) + (- Ax' * p)›
unfolding ‹A = - (Ax * p)› Ax
by (auto simp: field_simps)

moreover have ‹x' ∉ vars (-Ax' * p)›
using ‹x' ∉ vars Ax'› by (metis (no_types, hide_lams) UnE add.right_neutral
add_minus_cancel assms(4) subsetD vars_in_right_only vars_mult)
moreover have ‹Axx ≠ 0 ⟹ MPoly_Type.degree (- Axx * p) x' < degree Ax x'›
using degree_times_le[of Axx p x'] x
by (auto simp: Ax degree_sum_notin ‹x' ∉ vars Ax'› degree_mult_Var'
degree_notin_vars)
ultimately have [simp]: ‹Axx = 0›
using H[of ‹MPoly_Type.degree (- Axx * p) x'› ‹- Axx * p› ‹- Ax' * p›]
by (auto simp: n)
then have [simp]: ‹Ax' = Ax›
using Ax by auto

show ‹A = 0›
using A ‹A = - (Ax * p)› ‹x' ∉ vars (- Ax' * p)› ‹x' ∉ vars A'› polynomial_decomp_alien_var(1) by force
then show ‹q = b›
using q by auto
qed

lemma vars_unE: ‹x ∈ vars (a * b) ⟹ (x ∈ vars a ⟹ thesis) ⟹ (x ∈ vars b ⟹ thesis) ⟹ thesis›
using vars_mult[of a b] by auto

lemma in_keys_minusI1:
assumes "t ∈ keys p" and "t ∉ keys q"
shows "t ∈ keys (p - q)"
using assms unfolding in_keys_iff lookup_minus by simp

lemma in_keys_minusI2:
fixes t :: ‹'a› and q :: ‹'a ⇒⇩0 'b :: {cancel_comm_monoid_add,group_add}›
assumes "t ∈ keys q" and "t ∉ keys p"
shows "t ∈ keys (p - q)"
using assms unfolding in_keys_iff lookup_minus by simp

‹x ∈ vars (p + q) ⟹ (x ∈ vars p ⟹ thesis) ⟹ (x ∈ vars q ⟹ thesis) ⟹ thesis›
by (meson UnE in_mono vars_add)

lemma lookup_monomial_If:
‹lookup (monomial v k) = (λk'. if k = k' then v else 0)›
by (intro ext) (auto simp: lookup_single_not_eq)

lemma vars_mult_Var:
‹vars (Var x * p) = (if p = 0 then {} else insert x (vars p))› for p :: ‹int mpoly›
proof -
have ‹p ≠ 0 ⟹
∃xa. (∃k. xa = monomial (Suc 0) x + k) ∧
lookup (mapping_of p) (xa - monomial (Suc 0) x) ≠ 0 ∧
0 < lookup xa x›
neq0_conv one_neq_zero plus_eq_zero_2 zero_mpoly.rep_eq)
then show ?thesis
apply (auto simp: vars_def times_mpoly.rep_eq Var.rep_eq
elim!: in_keys_timesE dest: keys_add')
apply (auto simp: keys_def lookup_times_monomial_left Var.rep_eq Var⇩0_def adds_def
done
qed

lemma keys_mult_monomial:
‹keys (monomial (n :: int) k * mapping_of a) = (if n = 0 then {} else ((+) k)  keys (mapping_of a))›
proof -
have [simp]: ‹(∑aa. (if k = aa then n else 0) *
(∑q. lookup (mapping_of a) q when k + xa = aa + q)) =
(∑aa. (if k = aa then n * (∑q. lookup (mapping_of a) q when k + xa = aa + q) else 0))›
for xa
by (smt Sum_any.cong mult_not_zero)
show ?thesis
apply (auto simp: vars_def times_mpoly.rep_eq Const.rep_eq times_poly_mapping.rep_eq
Const⇩0_def elim!: in_keys_timesE split: if_splits)
apply (auto simp: lookup_monomial_If prod_fun_def
keys_def times_poly_mapping.rep_eq)
done
qed

lemma vars_mult_Const:
‹vars (Const n * a) = (if n = 0 then {} else vars a)› for a :: ‹int mpoly›
by (auto simp: vars_def times_mpoly.rep_eq Const.rep_eq keys_mult_monomial
Const⇩0_def elim!: in_keys_timesE split: if_splits)

lemma coeff_minus: "coeff p m - coeff q m = coeff (p-q) m"
by (simp add: coeff_def lookup_minus minus_mpoly.rep_eq)

lemma Const_1_eq_1: ‹Const (1 :: int) = (1 :: int mpoly)›
by (simp add: Const.abs_eq Const⇩0_one one_mpoly.abs_eq)

lemma [simp]:
‹vars (1 :: int mpoly) = {}›
by (auto simp: vars_def one_mpoly.rep_eq Const_1_eq_1)

subsection ‹More Ideals›

lemma
fixes A :: ‹(('x ⇒⇩0 nat) ⇒⇩0 'a::comm_ring_1) set›
assumes ‹p ∈ ideal A›
shows ‹p * q ∈ ideal A›
by (metis assms ideal.span_scale semiring_normalization_rules(7))

text ‹The following theorem is very close to @{thm ideal.span_insert}, except that it
is more useful if we need to take an element of \<^term>‹More_Modules.ideal (insert a S)›.›
lemma ideal_insert':
‹More_Modules.ideal (insert a S) = {y. ∃x k. y = x + k * a ∧ x ∈ More_Modules.ideal S}›
apply (auto simp: ideal.span_insert
intro: exI[of _ ‹_ - k * a›])
apply (rule_tac x = ‹x - k * a› in exI)
apply auto
apply (rule_tac x = ‹k› in exI)
apply auto
done

lemma ideal_mult_right_in:
‹a ∈ ideal A ⟹ a * b ∈ More_Modules.ideal A›
by (metis ideal.span_scale mult.commute)

lemma ideal_mult_right_in2:
‹a ∈ ideal A ⟹ b * a ∈ More_Modules.ideal A›
by (metis ideal.span_scale)

lemma [simp]: ‹vars (Var x :: 'a :: {zero_neq_one} mpoly) = {x}›
by (auto simp: vars_def Var.rep_eq  Var⇩0_def)

lemma vars_minus_Var_subset:
‹vars (p' - Var x :: 'a :: {ab_group_add,one,zero_neq_one} mpoly) ⊆  𝒱 ⟹ vars p' ⊆ insert x 𝒱›
using vars_add[of ‹p' - Var x› ‹Var x›]
by auto

‹vars (p' + Var x :: 'a :: {ab_group_add,one,zero_neq_one} mpoly) ⊆  𝒱 ⟹ vars p' ⊆ insert x 𝒱›
using vars_add[of ‹p' + Var x› ‹-Var x›]
by auto

lemma coeff_monomila_in_varsD:
‹coeff p (monomial (Suc 0) x) ≠ 0 ⟹ x ∈ vars (p :: int mpoly)›
by (auto simp: coeff_def vars_def keys_def
intro!: exI[of _ ‹monomial (Suc 0) x›])

lemma coeff_MPoly_monomial[simp]:
‹(MPoly_Type.coeff (MPoly (monomial a m)) m) = a›
by (metis MPoly_Type.coeff_def lookup_single_eq monom.abs_eq monom.rep_eq)

end

Theory Finite_Map_Multiset

(*
File:         Finite_Map_Multiset.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Maintainer:   Mathias Fleury, JKU
*)
theory Finite_Map_Multiset
imports
"HOL-Library.Finite_Map"
Nested_Multisets_Ordinals.Duplicate_Free_Multiset
begin

notation image_mset (infixr "#" 90)

section ‹Finite maps and multisets›

subsection ‹Finite sets and multisets›

abbreviation mset_fset :: ‹'a fset ⇒ 'a multiset› where
‹mset_fset N ≡ mset_set (fset N)›

definition fset_mset :: ‹'a multiset ⇒ 'a fset› where
‹fset_mset N ≡ Abs_fset (set_mset N)›

lemma fset_mset_mset_fset: ‹fset_mset (mset_fset N) = N›
by (auto simp: fset.fset_inverse fset_mset_def)

lemma mset_fset_fset_mset[simp]:
‹mset_fset (fset_mset N) = remdups_mset N›
by (auto simp: fset.fset_inverse fset_mset_def Abs_fset_inverse remdups_mset_def)

lemma in_mset_fset_fmember[simp]: ‹x ∈# mset_fset N ⟷ x |∈| N›
by (auto simp: fmember.rep_eq)

lemma in_fset_mset_mset[simp]: ‹x |∈| fset_mset N ⟷ x ∈# N›
by (auto simp: fmember.rep_eq fset_mset_def Abs_fset_inverse)

subsection ‹Finite map and multisets›

text ‹Roughly the same as \<^term>‹ran› and \<^term>‹dom›, but with duplication in the content (unlike their
finite sets counterpart) while still working on finite domains (unlike a function mapping).
Remark that \<^term>‹dom_m› (the keys) does not contain duplicates, but we keep for symmetry (and for
easier use of multiset operators as in the definition of \<^term>‹ran_m›).
›
definition dom_m where
‹dom_m N = mset_fset (fmdom N)›

definition ran_m where
‹ran_m N = the # fmlookup N # dom_m N›

lemma dom_m_fmdrop[simp]: ‹dom_m (fmdrop C N) = remove1_mset C (dom_m N)›
unfolding dom_m_def
by (cases ‹C |∈| fmdom N›)
(auto simp: mset_set.remove fmember.rep_eq)

lemma dom_m_fmdrop_All: ‹dom_m (fmdrop C N) = removeAll_mset C (dom_m N)›
unfolding dom_m_def
by (cases ‹C |∈| fmdom N›)
(auto simp: mset_set.remove fmember.rep_eq)

lemma dom_m_fmupd[simp]: ‹dom_m (fmupd k C N) = add_mset k (remove1_mset k (dom_m N))›
unfolding dom_m_def
by (cases ‹k |∈| fmdom N›)
(auto simp: mset_set.remove fmember.rep_eq mset_set.insert_remove)

lemma distinct_mset_dom: ‹distinct_mset (dom_m N)›
by (simp add: distinct_mset_mset_set dom_m_def)

lemma in_dom_m_lookup_iff: ‹C ∈# dom_m N' ⟷ fmlookup N' C ≠ None›
by (auto simp: dom_m_def fmdom.rep_eq fmlookup_dom'_iff)

lemma in_dom_in_ran_m[simp]: ‹i ∈# dom_m N ⟹ the (fmlookup N i) ∈# ran_m N›
by (auto simp: ran_m_def)

lemma fmupd_same[simp]:
‹x1 ∈# dom_m x1aa ⟹ fmupd x1 (the (fmlookup x1aa x1)) x1aa = x1aa›
by (metis fmap_ext fmupd_lookup in_dom_m_lookup_iff option.collapse)

lemma ran_m_fmempty[simp]: ‹ran_m fmempty = {#}› and
dom_m_fmempty[simp]: ‹dom_m fmempty = {#}›
by (auto simp: ran_m_def dom_m_def)

lemma fmrestrict_set_fmupd:
‹a ∈ xs ⟹ fmrestrict_set xs (fmupd a C N) = fmupd a C (fmrestrict_set xs N)›
‹a ∉ xs ⟹ fmrestrict_set xs (fmupd a C N) = fmrestrict_set xs N›
by (auto simp: fmfilter_alt_defs)

lemma fset_fmdom_fmrestrict_set:
‹fset (fmdom (fmrestrict_set xs N)) = fset (fmdom N) ∩ xs›
by (auto simp: fmfilter_alt_defs)

lemma dom_m_fmrestrict_set: ‹dom_m (fmrestrict_set (set xs) N) = mset xs ∩# dom_m N›
using fset_fmdom_fmrestrict_set[of ‹set xs› N] distinct_mset_dom[of N]
distinct_mset_inter_remdups_mset[of ‹mset_fset (fmdom N)› ‹mset xs›]
by (auto simp: dom_m_def fset_mset_mset_fset finite_mset_set_inter multiset_inter_commute
remdups_mset_def)

lemma dom_m_fmrestrict_set': ‹dom_m (fmrestrict_set xs N) = mset_set (xs ∩ set_mset (dom_m N))›
using fset_fmdom_fmrestrict_set[of ‹xs› N] distinct_mset_dom[of N]
by (auto simp: dom_m_def fset_mset_mset_fset finite_mset_set_inter multiset_inter_commute
remdups_mset_def)

lemma indom_mI: ‹fmlookup m x = Some y ⟹ x ∈# dom_m m›
by (drule fmdomI)  (auto simp: dom_m_def fmember.rep_eq)

lemma fmupd_fmdrop_id:
assumes ‹k |∈| fmdom N'›
shows ‹fmupd k (the (fmlookup N' k)) (fmdrop k N') = N'›
proof -
have [simp]: ‹map_upd k (the (fmlookup N' k))
(λx. if x ≠ k then fmlookup N' x else None) =
map_upd k (the (fmlookup N' k))
(fmlookup N')›
by (auto intro!: ext simp: map_upd_def)
have [simp]: ‹map_upd k (the (fmlookup N' k)) (fmlookup N') = fmlookup N'›
using assms
by (auto intro!: ext simp: map_upd_def)
have [simp]: ‹finite (dom (λx. if x = k then None else fmlookup N' x))›
by (subst dom_if) auto
show ?thesis
apply (auto simp: fmupd_def fmupd.abs_eq[symmetric])
unfolding fmlookup_drop
apply (simp add: fmlookup_inverse)
done
qed

lemma fm_member_split: ‹k |∈| fmdom N' ⟹ ∃N'' v. N' = fmupd k v N'' ∧ the (fmlookup N' k) = v ∧
k |∉| fmdom N''›
by (rule exI[of _ ‹fmdrop k N'›])
(auto simp: fmupd_fmdrop_id)

lemma ‹fmdrop k (fmupd k va N'') = fmdrop k N''›
by (simp add: fmap_ext)

lemma fmap_ext_fmdom:
‹(fmdom N = fmdom N') ⟹ (⋀ x. x |∈| fmdom N ⟹ fmlookup N x = fmlookup N' x) ⟹
N = N'›
by (rule fmap_ext)
(case_tac ‹x |∈| fmdom N›, auto simp: fmdom_notD)

lemma fmrestrict_set_insert_in:
‹xa  ∈ fset (fmdom N) ⟹
fmrestrict_set (insert xa l1) N = fmupd xa (the (fmlookup N xa)) (fmrestrict_set l1 N)›
apply (rule fmap_ext_fmdom)
apply (auto simp: fset_fmdom_fmrestrict_set fmember.rep_eq notin_fset; fail)[]
apply (auto simp: fmlookup_dom_iff; fail)
done

lemma fmrestrict_set_insert_notin:
‹xa  ∉ fset (fmdom N) ⟹
fmrestrict_set (insert xa l1) N = fmrestrict_set l1 N›
by (rule fmap_ext_fmdom)
(auto simp: fset_fmdom_fmrestrict_set fmember.rep_eq notin_fset)

lemma fmrestrict_set_insert_in_dom_m[simp]:
‹xa  ∈# dom_m N ⟹
fmrestrict_set (insert xa l1) N = fmupd xa (the (fmlookup N xa)) (fmrestrict_set l1 N)›
by (simp add: fmrestrict_set_insert_in dom_m_def)

lemma fmrestrict_set_insert_notin_dom_m[simp]:
‹xa  ∉# dom_m N ⟹
fmrestrict_set (insert xa l1) N = fmrestrict_set l1 N›
by (simp add: fmrestrict_set_insert_notin dom_m_def)

lemma fmlookup_restrict_set_id: ‹fset (fmdom N) ⊆ A ⟹ fmrestrict_set A N = N›
by (metis fmap_ext fmdom'_alt_def fmdom'_notD fmlookup_restrict_set subset_iff)

lemma fmlookup_restrict_set_id': ‹set_mset (dom_m N) ⊆ A ⟹ fmrestrict_set A N = N›
by (rule fmlookup_restrict_set_id)
(auto simp: dom_m_def)

lemma ran_m_mapsto_upd:
assumes
NC: ‹C ∈# dom_m N›
shows ‹ran_m (fmupd C C' N) = add_mset C' (remove1_mset (the (fmlookup N C)) (ran_m N))›
proof -
define N' where
‹N' = fmdrop C N›
have N_N': ‹dom_m N = add_mset C (dom_m N')›
using NC unfolding N'_def by auto
have ‹C ∉# dom_m N'›
using NC distinct_mset_dom[of N] unfolding N_N' by auto
then show ?thesis
by (auto simp: N_N' ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
intro!: image_mset_cong)
qed

lemma ran_m_mapsto_upd_notin:
assumes NC: ‹C ∉# dom_m N›
shows ‹ran_m (fmupd C C' N) = add_mset C' (ran_m N)›
using NC
by (auto simp: ran_m_def mset_set.insert_remove image_mset_remove1_mset_if
intro!: image_mset_cong split: if_splits)

lemma image_mset_If_eq_notin:
‹C ∉# A ⟹ {#f (if x = C then a x else b x). x ∈# A#} = {# f(b x). x ∈# A #}›
by (induction A) auto

lemma filter_mset_cong2:
"(⋀x. x ∈# M ⟹ f x = g x) ⟹ M = N ⟹ filter_mset f M = filter_mset g N"
by (hypsubst, rule filter_mset_cong, simp)

lemma ran_m_fmdrop:
‹C ∈# dom_m N ⟹  ran_m (fmdrop C N) = remove1_mset (the (fmlookup N C)) (ran_m N)›
using distinct_mset_dom[of N]
by (cases ‹fmlookup N C›)
(auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)

lemma ran_m_fmdrop_notin:
‹C ∉# dom_m N ⟹ ran_m (fmdrop C N) = ran_m N›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)

lemma ran_m_fmdrop_If:
‹ran_m (fmdrop C N) = (if C ∈# dom_m N then remove1_mset (the (fmlookup N C)) (ran_m N) else ran_m N)›
using distinct_mset_dom[of N]
by (auto simp: ran_m_def image_mset_If_eq_notin[of C _ ‹λx. fst (the x)›]
dest!: multi_member_split
intro!: filter_mset_cong2 image_mset_cong2)

lemma dom_m_empty_iff[iff]:
‹dom_m NU = {#} ⟷ NU = fmempty›
by (cases NU) (auto simp: dom_m_def mset_set.insert_remove)

end

Theory WB_Sort

(*
File:         WB_Sort.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Author:       Maximilian Wuttke, Saarland University
Maintainer:   Mathias Fleury, JKU

Correctness proof contributed by Maximilian Wuttke *)
theory WB_Sort
imports
Refine_Imperative_HOL.IICF
"HOL-Library.Rewrite"
Nested_Multisets_Ordinals.Duplicate_Free_Multiset
begin

text ‹This a complete copy-paste of the IsaFoL version because sharing is too hard.›

text ‹Every element between \<^term>‹lo› and \<^term>‹hi› can be chosen as pivot element.›
definition choose_pivot :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ nat nres› where
‹choose_pivot _ _ _ lo hi = SPEC(λk. k ≥ lo ∧ k ≤ hi)›

text ‹The element at index ‹p› partitions the subarray ‹lo..hi›. This means that every element ›
definition isPartition_wrt :: ‹('b ⇒ 'b ⇒ bool) ⇒ 'b list ⇒ nat ⇒ nat ⇒ nat ⇒ bool› where
‹isPartition_wrt R xs lo hi p ≡ (∀ i. i ≥ lo ∧ i < p ⟶ R (xs!i) (xs!p)) ∧ (∀ j. j > p ∧ j ≤ hi ⟶ R (xs!p) (xs!j))›

lemma isPartition_wrtI:
‹(⋀ i. ⟦i ≥ lo; i < p⟧ ⟹ R (xs!i) (xs!p)) ⟹ (⋀ j. ⟦j > p; j ≤ hi⟧ ⟹ R (xs!p) (xs!j)) ⟹ isPartition_wrt R xs lo hi p›
by (simp add: isPartition_wrt_def)

definition isPartition :: ‹'a :: order list ⇒ nat ⇒ nat ⇒ nat ⇒ bool› where
‹isPartition xs lo hi p ≡ isPartition_wrt (≤) xs lo hi p›

abbreviation isPartition_map :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ nat ⇒ bool› where
‹isPartition_map R h xs i j k ≡ isPartition_wrt (λa b. R (h a) (h b)) xs i j k›

lemma isPartition_map_def':
‹lo ≤ p ⟹ p ≤ hi ⟹ hi < length xs ⟹ isPartition_map R h xs lo hi p = isPartition_wrt R (map h xs) lo hi p›
by (auto simp add: isPartition_wrt_def conjI)

text ‹Example: 6 is the pivot element (with index 4); \<^term>‹7› is equal to the \<^term>‹length xs - 1›.›
lemma ‹isPartition [0,5,3,4,6,9,8,10::nat] 0 7 4›
by (auto simp add: isPartition_def isPartition_wrt_def nth_Cons')

definition sublist :: ‹'a list ⇒ nat ⇒ nat ⇒ 'a list› where
‹sublist xs i j ≡ take (Suc j - i) (drop i xs)›

(*take from HashMap *)
lemma take_Suc0:
"l≠[] ⟹ take (Suc 0) l = [l!0]"
"0 < length l ⟹ take (Suc 0) l = [l!0]"
"Suc n ≤ length l ⟹ take (Suc 0) l = [l!0]"
by (cases l, auto)+

lemma sublist_single: ‹i < length xs ⟹ sublist xs i i = [xs!i]›
by (cases xs) (auto simp add: sublist_def take_Suc0)

lemma insert_eq: ‹insert a b = b ∪ {a}›
by auto

lemma sublist_nth: ‹⟦lo ≤ hi; hi < length xs; k+lo ≤ hi⟧ ⟹ (sublist xs lo hi)!k = xs!(lo+k)›
by (simp add: sublist_def)

lemma sublist_length: ‹⟦i ≤ j; j < length xs⟧ ⟹ length (sublist xs i j) = 1 + j - i›
by (simp add: sublist_def)

lemma sublist_not_empty: ‹⟦i ≤ j; j < length xs; xs ≠ []⟧ ⟹ sublist xs i j ≠ []›
apply simp
apply (rewrite List.length_greater_0_conv[symmetric])
apply (rewrite sublist_length)
by auto

lemma sublist_app: ‹⟦i1 ≤ i2; i2 ≤ i3⟧ ⟹ sublist xs i1 i2 @ sublist xs (Suc i2) i3 = sublist xs i1 i3›
unfolding sublist_def
by (smt Suc_eq_plus1_left Suc_le_mono append.assoc le_SucI le_add_diff_inverse le_trans same_append_eq take_add)

definition sorted_sublist_wrt :: ‹('b ⇒ 'b ⇒ bool) ⇒ 'b list ⇒ nat ⇒ nat ⇒ bool› where
‹sorted_sublist_wrt R xs lo hi = sorted_wrt R (sublist xs lo hi)›

definition sorted_sublist :: ‹'a :: linorder list ⇒ nat ⇒ nat ⇒ bool› where
‹sorted_sublist xs lo hi = sorted_sublist_wrt (≤) xs lo hi›

abbreviation sorted_sublist_map :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ bool› where
‹sorted_sublist_map R h xs lo hi ≡ sorted_sublist_wrt (λa b. R (h a) (h b)) xs lo hi›

lemma sorted_sublist_map_def':
‹lo < length xs ⟹ sorted_sublist_map R h xs lo hi ≡ sorted_sublist_wrt R (map h xs) lo hi›
apply (simp add: sorted_sublist_wrt_def)
by (simp add: drop_map sorted_wrt_map sublist_def take_map)

lemma sorted_sublist_wrt_refl: ‹i < length xs ⟹ sorted_sublist_wrt R xs i i›
by (auto simp add: sorted_sublist_wrt_def sublist_single)

lemma sorted_sublist_refl: ‹i < length xs ⟹ sorted_sublist xs i i›
by (auto simp add: sorted_sublist_def sorted_sublist_wrt_refl)

lemma sublist_map: ‹sublist (map f xs) i j = map f (sublist xs i j)›
apply (auto simp add: sublist_def)
by (simp add: drop_map take_map)

lemma take_set: ‹j ≤ length xs ⟹ x ∈ set (take j xs) ≡ (∃ k. k < j ∧ xs!k = x)›
by (rule eq_reflection) (auto simp add: take_set)

lemma drop_set: ‹j ≤ length xs ⟹ x ∈ set (drop j xs) ≡ (∃k. j≤k∧k<length xs ∧ xs!k=x)›
by (smt Misc.in_set_drop_conv_nth) (* lemma found by sledgehammer *)

lemma sublist_el: ‹i ≤ j ⟹ j < length xs ⟹ x ∈ set (sublist xs i j) ≡ (∃ k. k < Suc j-i ∧ xs!(i+k)=x)›
by (auto simp add: take_set sublist_def)

lemma sublist_el': ‹i ≤ j ⟹ j < length xs ⟹ x ∈ set (sublist xs i j) ≡ (∃ k. i≤k∧k≤j ∧ xs!k=x)›
apply (subst sublist_el, assumption, assumption)

lemma sublist_lt: ‹hi < lo ⟹ sublist xs lo hi = []›
by (auto simp add: sublist_def)

lemma nat_le_eq_or_lt: ‹(a :: nat) ≤ b = (a = b ∨ a < b)›
by linarith

lemma sorted_sublist_wrt_le: ‹hi ≤ lo ⟹ hi < length xs ⟹ sorted_sublist_wrt R xs lo hi›
apply (auto simp add: nat_le_eq_or_lt)
unfolding sorted_sublist_wrt_def
subgoal apply (rewrite sublist_single) by auto
subgoal by (auto simp add: sublist_lt)
done

text ‹Elements in a sorted sublists are actually sorted›
lemma sorted_sublist_wrt_nth_le:
assumes ‹sorted_sublist_wrt R xs lo hi› and ‹lo ≤ hi› and ‹hi < length xs› and
‹lo ≤ i› and ‹i < j› and ‹j ≤ hi›
shows ‹R (xs!i) (xs!j)›
proof -
have A: ‹lo < length xs› using assms(2) assms(3) by linarith
obtain i' where I: ‹i = lo + i'› using assms(4) le_Suc_ex by auto
obtain j' where J: ‹j = lo + j'› by (meson assms(4) assms(5) dual_order.trans le_iff_add less_imp_le_nat)
show ?thesis
using assms(1) apply (simp add: sorted_sublist_wrt_def I J)
apply (rewrite sublist_nth[symmetric, where k=i', where lo=lo, where hi=hi])
using assms apply auto subgoal using I by linarith
apply (rewrite sublist_nth[symmetric, where k=j', where lo=lo, where hi=hi])
using assms apply auto subgoal using J by linarith
apply (rule sorted_wrt_nth_less)
apply auto
subgoal using I J nat_add_left_cancel_less by blast
subgoal apply (simp add: sublist_length) using J by linarith
done
qed

text ‹We can make the assumption \<^term>‹i < j› weaker if we have a reflexivie relation.›
lemma sorted_sublist_wrt_nth_le':
assumes ref: ‹⋀ x. R x x›
and ‹sorted_sublist_wrt R xs lo hi› and ‹lo ≤ hi› and ‹hi < length xs›
and ‹lo ≤ i› and ‹i ≤ j› and ‹j ≤ hi›
shows ‹R (xs!i) (xs!j)›
proof -
have ‹i < j ∨ i = j› using ‹i ≤ j› by linarith
then consider (a) ‹i < j› |
(b) ‹i = j› by blast
then show ?thesis
proof cases
case a
then show ?thesis
using assms(2-5,7) sorted_sublist_wrt_nth_le by blast
next
case b
then show ?thesis
by (simp add: ref)
qed
qed

(*
lemma sorted_sublist_map_nth_le:
assumes ‹sorted_sublist_map R h xs lo hi› and ‹lo ≤ hi› and ‹hi < length xs› and
‹lo ≤ i› and ‹i < j› and ‹j ≤ hi›
shows ‹R (h (xs!i)) (h (xs!j))›
proof -
show ?thesis
using assms by (rule sorted_sublist_wrt_nth_le)
qed
*)

lemma sorted_sublist_le: ‹hi ≤ lo ⟹ hi < length xs ⟹ sorted_sublist xs lo hi›
by (auto simp add: sorted_sublist_def sorted_sublist_wrt_le)

lemma sorted_sublist_map_le: ‹hi ≤ lo ⟹ hi < length xs ⟹ sorted_sublist_map R h xs lo hi›
by (auto simp add: sorted_sublist_wrt_le)

lemma sublist_cons: ‹lo < hi ⟹ hi < length xs ⟹ sublist xs lo hi = xs!lo # sublist xs (Suc lo) hi›
by (metis Cons_eq_appendI append_self_conv2 less_imp_le_nat less_or_eq_imp_le less_trans
sublist_app sublist_single)

lemma sorted_sublist_wrt_cons':
‹sorted_sublist_wrt R xs (lo+1) hi ⟹ lo ≤ hi ⟹ hi < length xs ⟹ (∀j. lo<j∧j≤hi ⟶ R (xs!lo) (xs!j)) ⟹ sorted_sublist_wrt R xs lo hi›
apply (auto simp add: nat_le_eq_or_lt sorted_sublist_wrt_def)
apply (auto 5 4 simp add: sublist_cons sublist_el less_diff_conv add.commute[of _ lo]
dest: Suc_lessI sublist_single)
done

lemma sorted_sublist_wrt_cons:
assumes trans: ‹(⋀ x y z. ⟦R x y; R y z⟧ ⟹ R x z)› and
‹sorted_sublist_wrt R xs (lo+1) hi› and
‹lo ≤ hi› and ‹hi < length xs › and ‹R (xs!lo) (xs!(lo+1))›
shows ‹sorted_sublist_wrt R xs lo hi›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_cons') using assms apply auto
subgoal premises assms' for j
proof -
have A: ‹j=lo+1 ∨ j>lo+1› using assms'(5) by linarith
show ?thesis
using A proof
assume A: ‹j=lo+1› show ?thesis
by (simp add: A assms')
next
assume A: ‹j>lo+1› show ?thesis
apply (rule trans)
apply (rule assms(5))
apply (rule sorted_sublist_wrt_nth_le[OF assms(2), where i=‹lo+1›, where j=j])
subgoal using A assms'(6) by linarith
subgoal using assms'(3) less_imp_diff_less by blast
subgoal using assms'(5) by auto
subgoal using A by linarith
subgoal by (simp add: assms'(6))
done
qed
qed
done
qed

lemma sorted_sublist_map_cons:
‹(⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)) ⟹
sorted_sublist_map R h xs (lo+1) hi ⟹ lo ≤ hi ⟹ hi < length xs ⟹ R (h (xs!lo)) (h (xs!(lo+1))) ⟹ sorted_sublist_map R h xs lo hi›
by (blast intro: sorted_sublist_wrt_cons)

lemma sublist_snoc: ‹lo < hi ⟹ hi < length xs ⟹ sublist xs lo hi = sublist xs lo (hi-1) @ [xs!hi]›
apply (simp add: sublist_def)
proof -
assume a1: "lo < hi"
assume "hi < length xs"
then have "take lo xs @ take (Suc hi - lo) (drop lo xs) = (take lo xs @ take (hi - lo) (drop lo xs)) @ [xs ! hi]"
using a1 by (metis (no_types) Suc_diff_le add_Suc_right hd_drop_conv_nth le_add_diff_inverse less_imp_le_nat take_add take_hd_drop)
then show "take (Suc hi - lo) (drop lo xs) = take (hi - lo) (drop lo xs) @ [xs ! hi]"
by simp
qed

lemma sorted_sublist_wrt_snoc':
‹sorted_sublist_wrt R xs lo (hi-1) ⟹ lo ≤ hi ⟹ hi < length xs ⟹ (∀j. lo≤j∧j<hi ⟶ R (xs!j) (xs!hi)) ⟹ sorted_sublist_wrt R xs lo hi›
apply (simp add: sorted_sublist_wrt_def)
apply (auto simp add: nat_le_eq_or_lt)
subgoal by (simp add: sublist_single)
by (auto simp add: sublist_snoc sublist_el sorted_wrt_append add.commute[of lo] less_diff_conv
simp: leI simp flip:nat_le_eq_or_lt)

lemma sorted_sublist_wrt_snoc:
assumes trans: ‹(⋀ x y z. ⟦R x y; R y z⟧ ⟹ R x z)› and
‹sorted_sublist_wrt R xs lo (hi-1)› and
‹lo ≤ hi› and ‹hi < length xs› and ‹(R (xs!(hi-1)) (xs!hi))›
shows ‹sorted_sublist_wrt R xs lo hi›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_snoc') using assms apply auto
subgoal premises assms' for j
proof -
have A: ‹j=hi-1 ∨ j<hi-1› using assms'(6) by linarith
show ?thesis
using A proof
assume A: ‹j=hi-1› show ?thesis
by (simp add: A assms')
next
assume A: ‹j<hi-1› show ?thesis
apply (rule trans)
apply (rule sorted_sublist_wrt_nth_le[OF assms(2), where i=j, where j=‹hi-1›])
prefer 6
apply (rule assms(5))
apply auto
subgoal using A assms'(5) by linarith
subgoal using assms'(3) less_imp_diff_less by blast
subgoal using assms'(5) by auto
subgoal using A by linarith
done
qed
qed
done
qed

lemma sublist_split: ‹lo ≤ hi ⟹ lo < p ⟹ p < hi ⟹ hi < length xs ⟹ sublist xs lo p @ sublist xs (p+1) hi = sublist xs lo hi›
by (simp add: sublist_app)

lemma sublist_split_part: ‹lo ≤ hi ⟹ lo < p ⟹ p < hi ⟹ hi < length xs ⟹ sublist xs lo (p-1) @ xs!p # sublist xs (p+1) hi = sublist xs lo hi›
by (auto simp add: sublist_split[symmetric] sublist_snoc[where xs=xs,where lo=lo,where hi=p])

text ‹A property for partitions (we always assume that \<^term>‹R› is transitive.›
lemma isPartition_wrt_trans:
‹(⋀ x y z. ⟦R x y; R y z⟧ ⟹ R x z) ⟹
isPartition_wrt R xs lo hi p ⟹
(∀i j. lo ≤ i ∧ i < p ∧ p < j ∧ j ≤ hi ⟶ R (xs!i) (xs!j))›
by (auto simp add: isPartition_wrt_def)

lemma isPartition_map_trans:
‹(⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)) ⟹
hi < length xs ⟹
isPartition_map R h xs lo hi p ⟹
(∀i j. lo ≤ i ∧ i < p ∧ p < j ∧ j ≤ hi ⟶ R (h (xs!i)) (h (xs!j)))›
by (auto simp add: isPartition_wrt_def)

lemma merge_sorted_wrt_partitions_between':
‹lo ≤ hi ⟹ lo < p ⟹ p < hi ⟹ hi < length xs ⟹
isPartition_wrt R xs lo hi p ⟹
sorted_sublist_wrt R xs lo (p-1) ⟹ sorted_sublist_wrt R xs (p+1) hi ⟹
(∀i j. lo ≤ i ∧ i < p ∧ p < j ∧ j ≤ hi ⟶ R (xs!i) (xs!j)) ⟹
sorted_sublist_wrt R xs lo hi›
apply (auto simp add: isPartition_def isPartition_wrt_def sorted_sublist_def sorted_sublist_wrt_def sublist_map)
apply (simp add: sublist_split_part[symmetric])
apply (auto simp add: List.sorted_wrt_append)
subgoal by (auto simp add: sublist_el)
subgoal by (auto simp add: sublist_el)
subgoal by (auto simp add: sublist_el')
done

lemma merge_sorted_wrt_partitions_between:
‹(⋀ x y z. ⟦R x y; R y z⟧ ⟹ R x z) ⟹
isPartition_wrt R xs lo hi p ⟹
sorted_sublist_wrt R xs lo (p-1) ⟹ sorted_sublist_wrt R xs (p+1) hi ⟹
lo ≤ hi ⟹ hi < length xs ⟹ lo < p ⟹ p < hi ⟹ hi < length xs ⟹
sorted_sublist_wrt R xs lo hi›
by (simp add: merge_sorted_wrt_partitions_between' isPartition_wrt_trans)

(*
lemma merge_sorted_map_partitions_between:
‹(⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)) ⟹
isPartition_map R h xs lo hi p ⟹
sorted_sublist_map R h xs lo (p-1) ⟹ sorted_sublist_map R h xs (p+1) hi ⟹
lo ≤ hi ⟹ hi < length xs ⟹ lo < p ⟹ p < hi ⟹ hi < length xs ⟹
sorted_sublist_map R h xs lo hi›
by (simp add: merge_sorted_wrt_partitions_between' isPartition_map_trans)
*)

text ‹The main theorem to merge sorted lists›
lemma merge_sorted_wrt_partitions:
‹isPartition_wrt R xs lo hi p ⟹
sorted_sublist_wrt R xs lo (p - Suc 0) ⟹ sorted_sublist_wrt R xs (Suc p) hi ⟹
lo ≤ hi ⟹ lo ≤ p ⟹ p ≤ hi ⟹ hi < length xs ⟹
(∀i j. lo ≤ i ∧ i < p ∧ p < j ∧ j ≤ hi ⟶ R (xs!i) (xs!j)) ⟹
sorted_sublist_wrt R xs lo hi›
subgoal premises assms
proof -
have C: ‹lo=p∧p=hi ∨ lo=p∧p<hi ∨ lo<p∧p=hi ∨ lo<p∧p<hi›
using assms by linarith
show ?thesis
using C apply auto
subgoal ― ‹lo=p=hi›
apply (rule sorted_sublist_wrt_refl)
using assms by auto
subgoal ― ‹lo=p<hi›
using assms by (simp add: isPartition_def isPartition_wrt_def sorted_sublist_wrt_cons')
subgoal ― ‹lo<p=hi›
using assms by (simp add: isPartition_def isPartition_wrt_def sorted_sublist_wrt_snoc')
subgoal ― ‹lo<p<hi›
using assms
apply (rewrite merge_sorted_wrt_partitions_between'[where p=p])
by auto
done
qed
done

theorem merge_sorted_map_partitions:
‹(⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)) ⟹
isPartition_map R h xs lo hi p ⟹
sorted_sublist_map R h xs lo (p - Suc 0) ⟹ sorted_sublist_map R h xs (Suc p) hi ⟹
lo ≤ hi ⟹ lo ≤ p ⟹ p ≤ hi ⟹ hi < length xs ⟹
sorted_sublist_map R h xs lo hi›
apply (rule merge_sorted_wrt_partitions) apply auto
by (simp add: merge_sorted_wrt_partitions isPartition_map_trans)

lemma partition_wrt_extend:
‹isPartition_wrt R xs lo' hi' p ⟹
hi < length xs ⟹
lo ≤ lo' ⟹ lo' ≤ hi ⟹ hi' ≤ hi ⟹
lo' ≤ p ⟹ p ≤ hi' ⟹
(⋀ i. lo≤i ⟹ i <lo' ⟹ R (xs!i) (xs!p)) ⟹
(⋀ j. hi'<j ⟹ j≤hi ⟹ R (xs!p) (xs!j)) ⟹
isPartition_wrt R xs lo hi p›
unfolding isPartition_wrt_def
apply (intro conjI)
subgoal
by (force simp: not_le)
subgoal
using leI by blast
done

lemma partition_map_extend:
‹isPartition_map R h xs lo' hi' p ⟹
hi < length xs ⟹
lo ≤ lo' ⟹ lo' ≤ hi ⟹ hi' ≤ hi ⟹
lo' ≤ p ⟹ p ≤ hi' ⟹
(⋀ i. lo≤i ⟹ i <lo' ⟹ R (h (xs!i)) (h (xs!p))) ⟹
(⋀ j. hi'<j ⟹ j≤hi ⟹ R (h (xs!p)) (h (xs!j))) ⟹
isPartition_map R h xs lo hi p›
by (auto simp add: partition_wrt_extend)

lemma isPartition_empty:
‹(⋀ j. ⟦lo < j; j ≤ hi⟧ ⟹ R (xs ! lo) (xs ! j)) ⟹
isPartition_wrt R xs lo hi lo›
by (auto simp add: isPartition_wrt_def)

lemma take_ext:
‹(∀i<k. xs'!i=xs!i) ⟹
k < length xs ⟹ k < length xs' ⟹
take k xs' = take k xs›
by (simp add: nth_take_lemma)

lemma drop_ext':
‹(∀i. i≥k ∧ i<length xs ⟶ xs'!i=xs!i) ⟹
0<k ⟹ xs≠[] ⟹ ― ‹These corner cases will be dealt with in the next lemma›
length xs'=length xs ⟹
drop k xs' = drop k xs›
apply (rewrite in ‹drop _ ⌑ = _› List.rev_rev_ident[symmetric])
apply (rewrite in ‹_ = drop _ ⌑› List.rev_rev_ident[symmetric])
apply (rewrite in ‹⌑ = _› List.drop_rev)
apply (rewrite in ‹_ = ⌑› List.drop_rev)
apply simp
apply (rule take_ext)
by (auto simp add: rev_nth)

lemma drop_ext:
‹(∀i. i≥k ∧ i<length xs ⟶ xs'!i=xs!i) ⟹
length xs'=length xs ⟹
drop k xs' = drop k xs›
apply (cases xs)
apply auto
apply (cases k)
subgoal  by (simp add: nth_equalityI)
subgoal apply (rule drop_ext') by auto
done

lemma sublist_ext':
‹(∀i. lo≤i∧i≤hi ⟶ xs'!i=xs!i) ⟹
length xs' = length xs ⟹
lo ≤ hi ⟹ Suc hi < length xs ⟹
sublist xs' lo hi = sublist xs lo hi›
apply (simp add: sublist_def)
apply (rule take_ext)
by auto

lemma lt_Suc: ‹(a < b) = (Suc a = b ∨ Suc a < b)›
by auto

lemma sublist_until_end_eq_drop: ‹Suc hi = length xs ⟹ sublist xs lo hi = drop lo xs›
by (simp add: sublist_def)

lemma sublist_ext:
‹(∀i. lo≤i∧i≤hi ⟶ xs'!i=xs!i) ⟹
length xs' = length xs ⟹
lo ≤ hi ⟹ hi < length xs ⟹
sublist xs' lo hi = sublist xs lo hi›
apply (auto simp add: lt_Suc[where a=hi])
subgoal by (auto simp add: sublist_until_end_eq_drop drop_ext)
subgoal by (auto simp add: sublist_ext')
done

lemma sorted_wrt_lower_sublist_still_sorted:
assumes ‹sorted_sublist_wrt R xs lo (lo' - Suc 0)› and
‹lo ≤ lo'› and ‹lo' < length xs› and
‹(∀ i. lo≤i∧i<lo' ⟶ xs'!i=xs!i)› and ‹length xs' = length xs›
shows ‹sorted_sublist_wrt R xs' lo (lo' - Suc 0)›
proof -
have l: ‹lo < lo' - 1 ∨ lo ≥ lo'-1›
by linarith
show ?thesis
using l apply auto
subgoal ― ‹lo < lo' - 1›
apply (auto simp add: sorted_sublist_wrt_def)
apply (rewrite sublist_ext[where xs=xs])
using assms by (auto simp add: sorted_sublist_wrt_def)
subgoal ― ‹lo >= lo' - 1›
using assms by (auto simp add: sorted_sublist_wrt_le)
done
qed

lemma sorted_map_lower_sublist_still_sorted:
assumes ‹sorted_sublist_map R h xs lo (lo' - Suc 0)› and
‹lo ≤ lo'› and ‹lo' < length xs› and
‹(∀ i. lo≤i∧i<lo' ⟶ xs'!i=xs!i)› and ‹length xs' = length xs›
shows ‹sorted_sublist_map R h xs' lo (lo' - Suc 0)›
using assms by (rule sorted_wrt_lower_sublist_still_sorted)

lemma sorted_wrt_upper_sublist_still_sorted:
assumes ‹sorted_sublist_wrt R xs (hi'+1) hi› and
‹lo ≤ lo'› and ‹hi < length xs› and
‹∀ j. hi'<j∧j≤hi ⟶ xs'!j=xs!j› and ‹length xs' = length xs›
shows ‹sorted_sublist_wrt R xs' (hi'+1) hi›
proof -
have l: ‹hi' + 1 < hi ∨ hi' + 1 ≥ hi›
by linarith
show ?thesis
using l apply auto
subgoal ― ‹hi' + 1 < h›
apply (auto simp add: sorted_sublist_wrt_def)
apply (rewrite sublist_ext[where xs=xs])
using assms by (auto simp add: sorted_sublist_wrt_def)
subgoal ― ‹\<^term>‹hi' + 1 ≥ hi››
using assms by (auto simp add: sorted_sublist_wrt_le)
done
qed

lemma sorted_map_upper_sublist_still_sorted:
assumes ‹sorted_sublist_map R h xs (hi'+1) hi› and
‹lo ≤ lo'› and ‹hi < length xs› and
‹∀ j. hi'<j∧j≤hi ⟶ xs'!j=xs!j› and ‹length xs' = length xs›
shows ‹sorted_sublist_map R h xs' (hi'+1) hi›
using assms by (rule sorted_wrt_upper_sublist_still_sorted)

text ‹The specification of the partition function›
definition partition_spec :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ 'a list ⇒ nat ⇒ bool› where
‹partition_spec R h xs lo hi xs' p ≡
mset xs' = mset xs ∧ ― ‹The list is a permutation›
isPartition_map R h xs' lo hi p ∧ ― ‹We have a valid partition on the resulting list›
lo ≤ p ∧ p ≤ hi ∧ ― ‹The partition index is in bounds›
(∀ i. i<lo ⟶ xs'!i=xs!i) ∧ (∀ i. hi<i∧i<length xs' ⟶ xs'!i=xs!i)› ― ‹Everything else is unchanged.›

lemma in_set_take_conv_nth:
‹x ∈ set (take n xs) ⟷ (∃m<min n (length xs). xs ! m = x)›
by (metis in_set_conv_nth length_take min.commute min.strict_boundedE nth_take)

lemma mset_drop_upto: ‹mset (drop a N) = {#N!i. i ∈# mset_set {a..<length N}#}›
proof (induction N arbitrary: a)
case Nil
then show ?case by simp
next
case (Cons c N)
have upt: ‹{0..<Suc (length N)} = insert 0 {1..<Suc (length N)}›
by auto
then have H: ‹mset_set {0..<Suc (length N)} = add_mset 0 (mset_set {1..<Suc (length N)})›
unfolding upt by auto
have mset_case_Suc: ‹{#case x of 0 ⇒ c | Suc x ⇒ N ! x . x ∈# mset_set {Suc a..<Suc b}#} =
{#N ! (x-1) . x ∈# mset_set {Suc a..<Suc b}#}› for a b
by (rule image_mset_cong) (auto split: nat.splits)
have Suc_Suc: ‹{Suc a..<Suc b} = Suc  {a..<b}› for a b
by auto
then have mset_set_Suc_Suc: ‹mset_set {Suc a..<Suc b} = {#Suc n. n ∈# mset_set {a..<b}#}› for a b
unfolding Suc_Suc by (subst image_mset_mset_set[symmetric]) auto
have *: ‹{#N ! (x-Suc 0) . x ∈# mset_set {Suc a..<Suc b}#} = {#N ! x . x ∈# mset_set {a..<b}#}›
for a b
by (auto simp add: mset_set_Suc_Suc multiset.map_comp comp_def)
show ?case
apply (cases a)
using Cons[of 0] Cons by (auto simp: nth_Cons drop_Cons H mset_case_Suc *)
qed

(* Actually, I only need that ‹set (sublist xs' lo hi) = set (sublist xs lo hi)› *)
lemma mathias:
assumes
Perm: ‹mset xs' = mset xs›
and I: ‹lo≤i› ‹i≤hi› ‹xs'!i=x›
and Bounds: ‹hi < length xs›
and Fix: ‹⋀ i. i<lo ⟹ xs'!i = xs!i› ‹⋀ j. ⟦hi<j; j<length xs⟧ ⟹ xs'!j = xs!j›
shows ‹∃j. lo≤j∧j≤hi ∧ xs!j = x›
proof -
define xs1 xs2 xs3 xs1' xs2' xs3' where
‹xs1 = take lo xs› and
‹xs2 = take (Suc hi - lo) (drop lo xs)› and
‹xs3 = drop (Suc hi) xs› and
‹xs1' = take lo xs'› and
‹xs2' = take (Suc hi - lo) (drop lo xs')› and
‹xs3' = drop (Suc hi) xs'›
have [simp]: ‹length xs' = length xs›
using Perm by (auto dest: mset_eq_length)
have [simp]: ‹mset xs1 = mset xs1'›
using Fix(1) unfolding xs1_def xs1'_def
by (metis Perm le_cases mset_eq_length nth_take_lemma take_all)
have [simp]: ‹mset xs3 = mset xs3'›
using Fix(2) unfolding xs3_def xs3'_def mset_drop_upto
by (auto intro: image_mset_cong)
have ‹xs = xs1 @ xs2 @ xs3› ‹xs' = xs1' @ xs2' @ xs3'›
using I unfolding xs1_def xs2_def xs3_def xs1'_def xs2'_def xs3'_def
by (metis append.assoc append_take_drop_id le_SucI le_add_diff_inverse order_trans take_add)+
moreover have ‹xs ! i = xs2 ! (i - lo)› ‹i ≥ length xs1›
using I Bounds unfolding xs2_def xs1_def by (auto simp: nth_take min_def)
moreover have  ‹x ∈ set xs2'›
using I Bounds unfolding xs2'_def
by (auto simp: in_set_take_conv_nth
intro!: exI[of _ ‹i - lo›])
ultimately have ‹x ∈ set xs2›
using Perm I by (auto dest: mset_eq_setD)
then obtain j where ‹xs ! (lo + j) = x› ‹j ≤ hi - lo›
unfolding in_set_conv_nth xs2_def
by auto
then show ?thesis
using Bounds I
by (auto intro: exI[of _ ‹lo+j›])
qed

text ‹If we fix the left and right rest of two permutated lists, then the sublists are also permutations.›
text ‹But we only need that the sets are equal.›
lemma mset_sublist_incl:
assumes Perm: ‹mset xs' = mset xs›
and Fix: ‹⋀ i. i<lo ⟹ xs'!i = xs!i› ‹⋀ j. ⟦hi<j; j<length xs⟧ ⟹ xs'!j = xs!j›
and bounds: ‹lo ≤ hi› ‹hi < length xs›
shows ‹set (sublist xs' lo hi) ⊆ set (sublist xs lo hi)›
proof
fix x
assume ‹x ∈ set (sublist xs' lo hi)›
then have ‹∃i. lo≤i∧i≤hi ∧ xs'!i=x›
by (metis assms(1) bounds(1) bounds(2) size_mset sublist_el')
then obtain i where I: ‹lo≤i› ‹i≤hi› ‹xs'!i=x› by blast
have ‹∃j. lo≤j∧j≤hi ∧ xs!j=x›
using Perm I bounds(2) Fix by (rule mathias, auto)
then show ‹x ∈ set (sublist xs lo hi)›
by (simp add: bounds(1) bounds(2) sublist_el')
qed

lemma mset_sublist_eq:
assumes ‹mset xs' = mset xs›
and ‹⋀ i. i<lo ⟹ xs'!i = xs!i›
and ‹⋀ j. ⟦hi<j; j<length xs⟧ ⟹ xs'!j = xs!j›
and bounds: ‹lo ≤ hi› ‹hi < length xs›
shows ‹set (sublist xs' lo hi) = set (sublist xs lo hi)›
proof
show ‹set (sublist xs' lo hi) ⊆ set (sublist xs lo hi)›
apply (rule mset_sublist_incl)
using assms by auto
show ‹set (sublist xs lo hi) ⊆ set (sublist xs' lo hi)›
by (rule mset_sublist_incl) (metis assms size_mset)+
qed

text ‹Our abstract recursive quicksort procedure. We abstract over a partition procedure.›
definition quicksort :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat × nat × 'a list ⇒ 'a list nres› where
‹quicksort R h = (λ(lo,hi,xs0). do {
RECT (λf (lo,hi,xs). do {
ASSERT(lo ≤ hi ∧ hi < length xs ∧ mset xs = mset xs0); ― ‹Premise for a partition function›
(xs, p) ← SPEC(uncurry (partition_spec R h xs lo hi)); ― ‹Abstract partition function›
ASSERT(mset xs = mset xs0);
xs ← (if p-1≤lo then RETURN xs else f (lo, p-1, xs));
ASSERT(mset xs = mset xs0);
if hi≤p+1 then RETURN xs else f (p+1, hi, xs)
}) (lo,hi,xs0)
})›

text ‹As premise for quicksor, we only need that the indices are ok.›
definition quicksort_pre :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒  nat ⇒ nat ⇒ 'a list ⇒ bool› where
‹quicksort_pre R h xs0 lo hi xs ≡ lo ≤ hi ∧ hi < length xs ∧ mset xs = mset xs0›

definition quicksort_post :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat ⇒ nat ⇒ 'a list ⇒ 'a list ⇒ bool› where
‹quicksort_post R h lo hi xs xs' ≡
mset xs' = mset xs ∧
sorted_sublist_map R h xs' lo hi ∧
(∀ i. i<lo ⟶ xs'!i = xs!i) ∧
(∀ j. hi<j∧j<length xs ⟶ xs'!j = xs!j)›

text ‹Convert Pure to HOL›
lemma quicksort_postI:
‹⟦mset xs' = mset xs; sorted_sublist_map R h xs' lo hi; (⋀ i. ⟦i<lo⟧ ⟹ xs'!i = xs!i); (⋀ j. ⟦hi<j; j<length xs⟧ ⟹ xs'!j = xs!j)⟧ ⟹ quicksort_post R h lo hi xs xs'›
by (auto simp add: quicksort_post_def)

text ‹The first case for the correctness proof of (abstract) quicksort: We assume that we called the partition function, and we have \<^term>‹p-1≤lo› and \<^term>‹hi≤p+1›.›
lemma quicksort_correct_case1:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. x ≠ y ⟹ R (h x) (h y) ∨ R (h y) (h x)›
and pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹p-1 ≤ lo› ‹hi ≤ p+1›
shows ‹quicksort_post R h lo hi xs xs'›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs›
using pre by (auto simp add: quicksort_pre_def)
(*
have part_perm: ‹set (sublist xs' lo hi) = set (sublist xs lo hi)›
using part partition_spec_set_sublist pre(1) pre(2) by blast
*)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)

have sorted_lower: ‹sorted_sublist_map R h xs' lo (p - Suc 0)›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_le)
subgoal using ifs(1) by auto
subgoal using ifs(1) mset_eq_length part(1) pre(1) pre(2) by fastforce
done
qed

have sorted_upper: ‹sorted_sublist_map R h xs' (Suc p) hi›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_le)
subgoal using ifs(2) by auto
subgoal using ifs(1) mset_eq_length part(1) pre(1) pre(2) by fastforce
done
qed

have sorted_middle: ‹sorted_sublist_map R h xs' lo hi›
proof -
show ?thesis
apply (rule merge_sorted_map_partitions[where p=p])
subgoal by (rule trans)
subgoal by (rule part)
subgoal by (rule sorted_lower)
subgoal by (rule sorted_upper)
subgoal using pre(1) by auto
subgoal by (simp add: part(4))
subgoal by (simp add: part(5))
subgoal by (metis part(1) pre(2) size_mset)
done
qed

show ?thesis
proof (intro quicksort_postI)
show ‹mset xs' = mset xs›
by (simp add: part(1))
next
show ‹sorted_sublist_map R h xs' lo hi›
by (rule sorted_middle)
next
show ‹⋀i. i < lo ⟹ xs' ! i = xs ! i›
using part(6) by blast
next
show ‹⋀j. ⟦hi < j; j < length xs⟧ ⟹ xs' ! j = xs ! j›
by (metis part(1) part(7) size_mset)
qed
qed

text ‹In the second case, we have to show that the precondition still holds for (p+1, hi, x') after the partition.›
lemma quicksort_correct_case2:
assumes
pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹¬ hi ≤ p + 1›
shows ‹quicksort_pre R h xs0 (Suc p) hi xs'›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs› ‹mset xs = mset xs0›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
show ?thesis
unfolding quicksort_pre_def
proof (intro conjI)
show ‹Suc p ≤ hi›
using ifs by linarith
show ‹hi < length xs'›
by (metis part(1) pre(2) size_mset)
show ‹mset xs' = mset xs0›
using pre(3) part(1) by (auto dest: mset_eq_setD)
qed
qed

lemma quicksort_post_set:
assumes ‹quicksort_post R h lo hi xs xs'›
and bounds: ‹lo ≤ hi› ‹hi < length xs›
shows ‹set (sublist xs' lo hi) = set (sublist xs lo hi)›
proof -
have ‹mset xs' = mset xs› ‹⋀ i. i<lo ⟹ xs'!i = xs!i› ‹⋀ j. ⟦hi<j; j<length xs⟧ ⟹ xs'!j = xs!j›
using assms by (auto simp add: quicksort_post_def)
then show ?thesis
using bounds by (rule mset_sublist_eq, auto)
qed

text ‹In the third case, we have run quicksort recursively on (p+1, hi, xs') after the partition, with hi<=p+1 and p-1<=lo.›
lemma quicksort_correct_case3:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. x ≠ y ⟹ R (h x) (h y) ∨ R (h y) (h x)›
and pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹p - Suc 0 ≤ lo› ‹¬ hi ≤ Suc p›
and IH1': ‹quicksort_post R h (Suc p) hi xs' xs''›
shows ‹quicksort_post R h lo hi xs xs''›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs› ‹mset xs = mset xs0›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
have IH1: ‹mset xs'' = mset xs'› ‹sorted_sublist_map R h xs'' (Suc p) hi›
‹⋀ i. i<Suc p ⟹ xs'' ! i = xs' ! i› ‹⋀ j. ⟦hi < j; j < length xs'⟧ ⟹ xs'' ! j = xs' ! j›
using IH1' by (auto simp add: quicksort_post_def)
note IH1_perm = quicksort_post_set[OF IH1']

have still_partition: ‹isPartition_map R h xs'' lo hi p›
proof(intro isPartition_wrtI)
fix i assume ‹lo ≤ i› ‹i < p›
show ‹R (h (xs'' ! i)) (h (xs'' ! p))›
text ‹This holds because this part hasn't changed›
using IH1(3) ‹i < p› ‹lo ≤ i› isPartition_wrt_def part(3) by fastforce
next
fix j assume ‹p < j› ‹j ≤ hi›
text ‹Obtain the position \<^term>‹posJ› where \<^term>‹xs''!j› was stored in \<^term>‹xs'›.›
have ‹xs''!j ∈ set (sublist xs'' (Suc p) hi)›
by (metis IH1(1) Suc_leI ‹j ≤ hi› ‹p < j› less_le_trans mset_eq_length part(1) pre(2) sublist_el')
then have ‹xs''!j ∈ set (sublist xs' (Suc p) hi)›
by (metis IH1_perm ifs(2) nat_le_linear part(1) pre(2) size_mset)
then have ‹∃ posJ. Suc p≤posJ∧posJ≤hi ∧ xs''!j = xs'!posJ›
by (metis Suc_leI ‹j ≤ hi› ‹p < j› less_le_trans part(1) pre(2) size_mset sublist_el')
then obtain posJ :: nat where PosJ: ‹Suc p≤posJ› ‹posJ≤hi› ‹xs''!j = xs'!posJ› by blast

then show ‹R (h (xs'' ! p)) (h (xs'' ! j))›
by (metis IH1(3) Suc_le_lessD isPartition_wrt_def lessI part(3))
qed

have sorted_lower: ‹sorted_sublist_map R h xs'' lo (p - Suc 0)›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_le)
subgoal by (simp add: ifs(1))
subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
done
qed

note sorted_upper = IH1(2)

have sorted_middle: ‹sorted_sublist_map R h xs'' lo hi›
proof -
show ?thesis
apply (rule merge_sorted_map_partitions[where p=p])
subgoal by (rule trans)
subgoal by (rule still_partition)
subgoal by (rule sorted_lower)
subgoal by (rule sorted_upper)
subgoal using pre(1) by auto
subgoal by (simp add: part(4))
subgoal by (simp add: part(5))
subgoal by (metis IH1(1) part(1) pre(2) size_mset)
done
qed

show ?thesis
proof (intro quicksort_postI)
show ‹mset xs'' = mset xs›
using part(1) IH1(1) by auto ― ‹I was faster than sledgehammer :-)›
next
show ‹sorted_sublist_map R h xs'' lo hi›
by (rule sorted_middle)
next
show ‹⋀i. i < lo ⟹ xs'' ! i = xs ! i›
using IH1(3) le_SucI part(4) part(6) by auto
next show ‹⋀j. hi < j ⟹ j < length xs ⟹ xs'' ! j = xs ! j›
by (metis IH1(4) part(1) part(7) size_mset)
qed
qed

text ‹In the 4th case, we have to show that the premise holds for \<^term>‹(lo,p-1,xs')›, in case \<^term>‹¬p-1≤lo››
text ‹Analogous to case 2.›
lemma quicksort_correct_case4:
assumes
pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs: ‹¬ p - Suc 0 ≤ lo ›
shows ‹quicksort_pre R h xs0 lo (p-Suc 0) xs'›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs› ‹mset xs0 = mset xs›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)

show ?thesis
unfolding quicksort_pre_def
proof (intro conjI)
show ‹lo ≤ p - Suc 0›
using ifs by linarith
show ‹p - Suc 0 < length xs'›
using mset_eq_length part(1) part(5) pre(2) by fastforce
show ‹mset xs' = mset xs0›
using pre(3) part(1) by (auto dest: mset_eq_setD)
qed
qed

text ‹In the 5th case, we have run quicksort recursively on (lo, p-1, xs').›
lemma quicksort_correct_case5:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. x ≠ y ⟹ R (h x) (h y) ∨ R (h y) (h x)›
and pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs:  ‹¬ p - Suc 0 ≤ lo› ‹hi ≤ Suc p›
and IH1': ‹quicksort_post R h lo (p - Suc 0) xs' xs''›
shows ‹quicksort_post R h lo hi xs xs''›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
have IH1: ‹mset xs'' = mset xs'› ‹sorted_sublist_map R h xs'' lo (p - Suc 0)›
‹⋀ i. i<lo ⟹ xs''!i = xs'!i› ‹⋀ j. ⟦p-Suc 0<j; j<length xs'⟧ ⟹ xs''!j = xs'!j›
using IH1' by (auto simp add: quicksort_post_def)
note IH1_perm = quicksort_post_set[OF IH1']

have still_partition: ‹isPartition_map R h xs'' lo hi p›
proof(intro isPartition_wrtI)
fix i assume ‹lo ≤ i› ‹i < p›
text ‹Obtain the position \<^term>‹posI› where \<^term>‹xs''!i› was stored in \<^term>‹xs'›.›
have ‹xs''!i ∈ set (sublist xs'' lo (p-Suc 0))›
by (metis (no_types, lifting) IH1(1) Suc_leI Suc_pred ‹i < p› ‹lo ≤ i› le_less_trans less_imp_diff_less mset_eq_length not_le not_less_zero part(1) part(5) pre(2) sublist_el')
then have ‹xs''!i ∈ set (sublist xs' lo (p-Suc 0))›
by (metis IH1_perm ifs(1) le_less_trans less_imp_diff_less mset_eq_length nat_le_linear part(1) part(5) pre(2))
then have ‹∃ posI. lo≤posI∧posI≤p-Suc 0 ∧ xs''!i = xs'!posI›
proof - ― ‹sledgehammer›
have "p - Suc 0 < length xs"
by (meson diff_le_self le_less_trans part(5) pre(2))
then show ?thesis
by (metis (no_types) ‹xs'' ! i ∈ set (sublist xs' lo (p - Suc 0))› ifs(1) mset_eq_length nat_le_linear part(1) sublist_el')
qed
then obtain posI :: nat where PosI: ‹lo≤posI› ‹posI≤p-Suc 0› ‹xs''!i = xs'!posI› by blast
then show ‹R (h (xs'' ! i)) (h (xs'' ! p))›
by (metis (no_types, lifting) IH1(4) ‹i < p› diff_Suc_less isPartition_wrt_def le_less_trans mset_eq_length not_le not_less_eq part(1) part(3) part(5) pre(2) zero_less_Suc)
next
fix j assume ‹p < j› ‹j ≤ hi›
then show ‹R (h (xs'' ! p)) (h (xs'' ! j))›
text ‹This holds because this part hasn't changed›
by (smt IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2))
qed

note sorted_lower = IH1(2)

have sorted_upper: ‹sorted_sublist_map R h xs'' (Suc p) hi›
proof -
show ?thesis
apply (rule sorted_sublist_wrt_le)
subgoal by (simp add: ifs(2))
subgoal using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
done
qed

have sorted_middle: ‹sorted_sublist_map R h xs'' lo hi›
proof -
show ?thesis
apply (rule merge_sorted_map_partitions[where p=p])
subgoal by (rule trans)
subgoal by (rule still_partition)
subgoal by (rule sorted_lower)
subgoal by (rule sorted_upper)
subgoal using pre(1) by auto
subgoal by (simp add: part(4))
subgoal by (simp add: part(5))
subgoal by (metis IH1(1) part(1) pre(2) size_mset)
done
qed

show ?thesis
proof (intro quicksort_postI)
show ‹mset xs'' = mset xs›
by (simp add: IH1(1) part(1))
next
show ‹sorted_sublist_map R h xs'' lo hi›
by (rule sorted_middle)
next
show ‹⋀i. i < lo ⟹ xs'' ! i = xs ! i›
by (simp add: IH1(3) part(6))
next
show ‹⋀j. hi < j ⟹ j < length xs ⟹ xs'' ! j = xs ! j›
by (metis IH1(4) diff_le_self dual_order.strict_trans2 mset_eq_length part(1) part(5) part(7))
qed
qed

text ‹In the 6th case, we have run quicksort recursively on (lo, p-1, xs'). We show the precondition on the second call on (p+1, hi, xs'')›
lemma quicksort_correct_case6:
assumes
pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs:  ‹¬ p - Suc 0 ≤ lo› ‹¬ hi ≤ Suc p›
and IH1: ‹quicksort_post R h lo (p - Suc 0) xs' xs''›
shows ‹quicksort_pre R h xs0 (Suc p) hi xs''›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs› ‹mset xs0 = mset xs›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
have IH1: ‹mset xs'' = mset xs'› ‹sorted_sublist_map R h xs'' lo (p - Suc 0)›
‹⋀ i. i<lo ⟹ xs''!i = xs'!i› ‹⋀ j. ⟦p-Suc 0<j; j<length xs'⟧ ⟹ xs''!j = xs'!j›
using IH1 by (auto simp add: quicksort_post_def)

show ?thesis
unfolding quicksort_pre_def
proof (intro conjI)
show ‹Suc p ≤ hi›
using ifs(2) by linarith
show ‹hi < length xs''›
using IH1(1) mset_eq_length part(1) pre(2) by fastforce
show ‹mset xs'' = mset xs0›
using pre(3) part(1) IH1(1) by (auto dest: mset_eq_setD)
qed
qed

text ‹In the 7th (and last) case, we have run quicksort recursively on (lo, p-1, xs'). We show the postcondition on the second call on (p+1, hi, xs'')›
lemma quicksort_correct_case7:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. x ≠ y ⟹ R (h x) (h y) ∨ R (h y) (h x)›
and pre: ‹quicksort_pre R h xs0 lo hi xs›
and part: ‹partition_spec R h xs lo hi xs' p›
and ifs:  ‹¬ p - Suc 0 ≤ lo› ‹¬ hi ≤ Suc p›
and IH1': ‹quicksort_post R h lo (p - Suc 0) xs' xs''›
and IH2': ‹quicksort_post R h (Suc p) hi xs'' xs'''›
shows ‹quicksort_post R h lo hi xs xs'''›
proof -
text ‹First boilerplate code step: 'unfold' the HOL definitions in the assumptions and convert them to Pure›
have pre: ‹lo ≤ hi› ‹hi < length xs›
using pre by (auto simp add: quicksort_pre_def)
have part: ‹mset xs' = mset xs› True
‹isPartition_map R h xs' lo hi p› ‹lo ≤ p› ‹p ≤ hi›
‹⋀ i. i<lo ⟹ xs'!i=xs!i› ‹⋀ i. ⟦hi<i; i<length xs'⟧ ⟹ xs'!i=xs!i›
using part by (auto simp add: partition_spec_def)
have IH1: ‹mset xs'' = mset xs'› ‹sorted_sublist_map R h xs'' lo (p - Suc 0)›
‹⋀ i. i<lo ⟹ xs''!i = xs'!i› ‹⋀ j. ⟦p-Suc 0<j; j<length xs'⟧ ⟹ xs''!j = xs'!j›
using IH1' by (auto simp add: quicksort_post_def)
note IH1_perm = quicksort_post_set[OF IH1']
have IH2: ‹mset xs''' = mset xs''› ‹sorted_sublist_map R h xs''' (Suc p) hi›
‹⋀ i. i<Suc p ⟹ xs'''!i = xs''!i› ‹⋀ j. ⟦hi<j; j<length xs''⟧ ⟹ xs'''!j = xs''!j›
using IH2' by (auto simp add: quicksort_post_def)
note IH2_perm = quicksort_post_set[OF IH2']

text ‹We still have a partition after the first call (same as in case 5)›
have still_partition1: ‹isPartition_map R h xs'' lo hi p›
proof(intro isPartition_wrtI)
fix i assume ‹lo ≤ i› ‹i < p›
text ‹Obtain the position \<^term>‹posI› where \<^term>‹xs''!i› was stored in \<^term>‹xs'›.›
have ‹xs''!i ∈ set (sublist xs'' lo (p-Suc 0))›
by (metis (no_types, lifting) IH1(1) Suc_leI Suc_pred ‹i < p› ‹lo ≤ i› le_less_trans less_imp_diff_less mset_eq_length not_le not_less_zero part(1) part(5) pre(2) sublist_el')
then have ‹xs''!i ∈ set (sublist xs' lo (p-Suc 0))›
by (metis IH1_perm ifs(1) le_less_trans less_imp_diff_less mset_eq_length nat_le_linear part(1) part(5) pre(2))
then have ‹∃ posI. lo≤posI∧posI≤p-Suc 0 ∧ xs''!i = xs'!posI›
proof - ― ‹sledgehammer›
have "p - Suc 0 < length xs"
by (meson diff_le_self le_less_trans part(5) pre(2))
then show ?thesis
by (metis (no_types) ‹xs'' ! i ∈ set (sublist xs' lo (p - Suc 0))› ifs(1) mset_eq_length nat_le_linear part(1) sublist_el')
qed
then obtain posI :: nat where PosI: ‹lo≤posI› ‹posI≤p-Suc 0› ‹xs''!i = xs'!posI› by blast
then show ‹R (h (xs'' ! i)) (h (xs'' ! p))›
by (metis (no_types, lifting) IH1(4) ‹i < p› diff_Suc_less isPartition_wrt_def le_less_trans mset_eq_length not_le not_less_eq part(1) part(3) part(5) pre(2) zero_less_Suc)
next
fix j assume ‹p < j› ‹j ≤ hi›
then show ‹R (h (xs'' ! p)) (h (xs'' ! j))›
text ‹This holds because this part hasn't changed›
by (smt IH1(4) add_diff_cancel_left' add_diff_inverse_nat diff_Suc_eq_diff_pred diff_le_self ifs(1) isPartition_wrt_def le_less_Suc_eq less_le_trans mset_eq_length nat_less_le part(1) part(3) part(4) plus_1_eq_Suc pre(2))
qed

text ‹We still have a partition after the second call (similar as in case 3)›
have still_partition2: ‹isPartition_map R h xs''' lo hi p›
proof(intro isPartition_wrtI)
fix i assume ‹lo ≤ i› ‹i < p›
show ‹R (h (xs''' ! i)) (h (xs''' ! p))›
text ‹This holds because this part hasn't changed›
using IH2(3) ‹i < p› ‹lo ≤ i› isPartition_wrt_def still_partition1 by fastforce
next
fix j assume ‹p < j› ‹j ≤ hi›
text ‹Obtain the position \<^term>‹posJ› where \<^term>‹xs'''!j› was stored in \<^term>‹xs'''›.›
have ‹xs'''!j ∈ set (sublist xs''' (Suc p) hi)›
by (metis IH1(1) IH2(1) Suc_leI ‹j ≤ hi› ‹p < j› ifs(2) nat_le_linear part(1) pre(2) size_mset sublist_el')
then have ‹xs'''!j ∈ set (sublist xs'' (Suc p) hi)›
by (metis IH1(1) IH2_perm ifs(2) mset_eq_length nat_le_linear part(1) pre(2))
then have ‹∃ posJ. Suc p≤posJ∧posJ≤hi ∧ xs'''!j = xs''!posJ›
by (metis IH1(1) ifs(2) mset_eq_length nat_le_linear part(1) pre(2) sublist_el')
then obtain posJ :: nat where PosJ: ‹Suc p≤posJ› ‹posJ≤hi› ‹xs'''!j = xs''!posJ› by blast

then show ‹R (h (xs''' ! p)) (h (xs''' ! j))›
proof - ― ‹sledgehammer›
have "∀n na as p. (p (as ! na::'a) (as ! posJ) ∨ posJ ≤ na) ∨ ¬ isPartition_wrt p as n hi na"
by (metis (no_types) PosJ(2) isPartition_wrt_def not_less)
then show ?thesis
by (metis IH2(3) PosJ(1) PosJ(3) lessI not_less_eq_eq still_partition1)
qed
qed

text ‹We have that the lower part is sorted after the first recursive call›
note sorted_lower1 = IH1(2)

text ‹We show that it is still sorted after the second call.›
have sorted_lower2: ‹sorted_sublist_map R h xs''' lo (p-Suc 0)›
proof -
show ?thesis
using sorted_lower1 apply (rule sorted_wrt_lower_sublist_still_sorted)
subgoal by (rule part)
subgoal
using IH1(1) mset_eq_length part(1) part(5) pre(2) by fastforce
subgoal
by (simp add: IH2(3))
subgoal
by (metis IH2(1) size_mset)
done
qed

text ‹The second IH gives us the the upper list is sorted after the second recursive call›
note sorted_upper2 = IH2(2)

text ‹Finally, we have to show that the entire list is sorted after the second recursive call.›
have sorted_middle: ‹sorted_sublist_map R h xs''' lo hi›
proof -
show ?thesis
apply (rule merge_sorted_map_partitions[where p=p])
subgoal by (rule trans)
subgoal by (rule still_partition2)
subgoal by (rule sorted_lower2)
subgoal by (rule sorted_upper2)
subgoal using pre(1) by auto
subgoal by (simp add: part(4))
subgoal by (simp add: part(5))
subgoal by (metis IH1(1) IH2(1) part(1) pre(2) size_mset)
done
qed

show ?thesis
proof (intro quicksort_postI)
show ‹mset xs''' = mset xs›
by (simp add: IH1(1) IH2(1) part(1))
next
show ‹sorted_sublist_map R h xs''' lo hi›
by (rule sorted_middle)
next
show ‹⋀i. i < lo ⟹ xs''' ! i = xs ! i›
using IH1(3) IH2(3) part(4) part(6) by auto
next
show ‹⋀j. hi < j ⟹ j < length xs ⟹ xs''' ! j = xs ! j›
by (metis IH1(1) IH1(4) IH2(4) diff_le_self ifs(2) le_SucI less_le_trans nat_le_eq_or_lt not_less part(1) part(7) size_mset)
qed

qed

text ‹We can now show the correctness of the abstract quicksort procedure, using the refinement framework and the above case lemmas.›
lemma quicksort_correct:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. x ≠ y ⟹ R (h x) (h y) ∨ R (h y) (h x)›
and Pre: ‹lo0 ≤ hi0› ‹hi0 < length xs0›
shows ‹quicksort R h (lo0,hi0,xs0) ≤ ⇓ Id (SPEC(λxs. quicksort_post R h lo0 hi0 xs0 xs))›
proof -
have wf: ‹wf (measure (λ(lo, hi, xs). Suc hi - lo))›
by auto
define pre where ‹pre = (λ(lo,hi,xs). quicksort_pre R h xs0 lo hi xs)›
define post where ‹post = (λ(lo,hi,xs). quicksort_post R h lo hi xs)›
have pre: ‹pre (lo0,hi0,xs0)›
unfolding quicksort_pre_def pre_def by (simp add: Pre)

text ‹We first generalize the goal a over all states.›
have ‹WB_Sort.quicksort R h (lo0,hi0,xs0) ≤ ⇓ Id (SPEC (post (lo0,hi0,xs0)))›
unfolding quicksort_def prod.case
apply (rule RECT_rule)
apply (refine_mono)
apply (rule wf)
apply (rule pre)
subgoal premises IH for f x
apply (refine_vcg ASSERT_leI)
unfolding pre_def post_def

subgoal ― ‹First premise (assertion) for partition›
using IH(2) by (simp add: quicksort_pre_def pre_def)
subgoal ― ‹Second premise (assertion) for partition›
using IH(2) by (simp add: quicksort_pre_def pre_def)
subgoal
using IH(2) by (auto simp add: quicksort_pre_def pre_def dest: mset_eq_setD)

text ‹Termination case: \<^term>‹(p-1 ≤ lo')› and \<^term>‹(hi' ≤ p+1)›; directly show postcondition›
subgoal unfolding partition_spec_def by (auto dest: mset_eq_setD)
subgoal ― ‹Postcondition (after partition)›
apply -
using IH(2) unfolding pre_def apply (simp, elim conjE, split prod.splits)
using trans lin apply (rule quicksort_correct_case1) by auto

text ‹Case \<^term>‹(p-1 ≤ lo')› and \<^term>‹(hi' < p+1)› (Only second recursive call)›
subgoal
apply (rule IH(1)[THEN order_trans])

text ‹Show that the invariant holds for the second recursive call›
subgoal
using IH(2) unfolding pre_def apply (simp, elim conjE, split prod.splits)
apply (rule quicksort_correct_case2) by auto

text ‹Wellfoundness (easy)›
subgoal by (auto simp add: quicksort_pre_def partition_spec_def)

text ‹Show that the postcondition holds›
subgoal
apply (simp add: Misc.subset_Collect_conv post_def, intro allI impI, elim conjE)
using trans lin apply (rule quicksort_correct_case3)
using IH(2) unfolding pre_def by auto
done

text ‹Case: At least the first recursive call›
subgoal
apply (rule IH(1)[THEN order_trans])

text ‹Show that the precondition holds for the first recursive call›
subgoal
using IH(2) unfolding pre_def post_def apply (simp, elim conjE, split prod.splits) apply auto
apply (rule quicksort_correct_case4) by auto

text ‹Wellfoundness for first recursive call (easy)›
subgoal by (auto simp add: quicksort_pre_def partition_spec_def)

text ‹Simplify some refinement suff...›
apply (simp add: Misc.subset_Collect_conv ASSERT_leI, intro allI impI conjI, elim conjE)
apply (rule ASSERT_leI)
apply (simp_all add: Misc.subset_Collect_conv ASSERT_leI)
subgoal unfolding quicksort_post_def pre_def post_def by (auto dest: mset_eq_setD)
text ‹Only the first recursive call: show postcondition›
subgoal
using trans lin apply (rule quicksort_correct_case5)
using IH(2) unfolding pre_def post_def by auto

apply (rule ASSERT_leI)
subgoal unfolding quicksort_post_def pre_def post_def by (auto dest: mset_eq_setD)

text ‹Both recursive calls.›
subgoal
apply (rule IH(1)[THEN order_trans])

text ‹Show precondition for second recursive call (after the first call)›
subgoal
unfolding pre_def post_def
apply auto
apply (rule quicksort_correct_case6)
using IH(2) unfolding pre_def post_def  by auto

text ‹Wellfoundedness for second recursive call (easy)›
subgoal by (auto simp add: quicksort_pre_def partition_spec_def)

text ‹Show that the postcondition holds (after both recursive calls)›
subgoal
apply (simp add: Misc.subset_Collect_conv, intro allI impI, elim conjE)
using trans lin apply (rule quicksort_correct_case7)
using IH(2) unfolding pre_def post_def by auto
done
done
done
done

text ‹Finally, apply the generalized lemma to show the thesis.›
then show ?thesis unfolding post_def  by auto
qed

(* TODO: Show that our (abstract) partition satisifies the specification *)

definition partition_main_inv :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat ⇒ nat ⇒ 'a list ⇒ (nat×nat×'a list) ⇒ bool› where
‹partition_main_inv R h lo hi xs0 p ≡
case p of (i,j,xs) ⇒
j < length xs ∧ j ≤ hi ∧ i < length xs ∧ lo ≤ i ∧ i ≤ j ∧ mset xs = mset xs0 ∧
(∀k. k ≥ lo ∧ k < i ⟶ R (h (xs!k)) (h (xs!hi))) ∧ ― ‹All elements from \<^term>‹lo› to \<^term>‹i-1› are smaller than the pivot›
(∀k. k ≥ i ∧ k < j ⟶  R (h (xs!hi)) (h (xs!k))) ∧ ― ‹All elements from \<^term>‹i› to \<^term>‹j-1› are greater than the pivot›
(∀k. k < lo ⟶ xs!k = xs0!k) ∧ ― ‹Everything below \<^term>‹lo› is unchanged›
(∀k. k ≥ j ∧ k < length xs ⟶ xs!k = xs0!k) ― ‹All elements from \<^term>‹j› are unchanged (including everyting above \<^term>‹hi›)›
›

text ‹The main part of the partition function. The pivot is assumed to be the last element. This is
exactly the "Lomuto partition scheme" partition function from Wikipedia.›
definition partition_main :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat ⇒ nat ⇒ 'a list ⇒ ('a list × nat) nres› where
‹partition_main R h lo hi xs0 = do {
ASSERT(hi < length xs0);
pivot ← RETURN (h (xs0 ! hi));
(i,j,xs) ← WHILE⇩T⇗partition_main_inv R h lo hi xs0⇖ ― ‹We loop from \<^term>‹j=lo› to \<^term>‹j=hi-1›.›
(λ(i,j,xs). j < hi)
(λ(i,j,xs). do {
ASSERT(i < length xs ∧ j < length xs);
if R (h (xs!j)) pivot
then RETURN (i+1, j+1, swap xs i j)
else RETURN (i,   j+1, xs)
})
(lo, lo, xs0); ― ‹i and j are both initialized to lo›
ASSERT(i < length xs ∧ j = hi ∧ lo ≤ i ∧ hi < length xs ∧ mset xs = mset xs0);
RETURN (swap xs i hi, i)
}›

(*
definition partition_spec :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ 'a list ⇒ nat ⇒ nat ⇒ 'a list ⇒ nat ⇒ bool› where
‹partition_spec R h xs lo hi xs' p ≡
mset xs' = mset xs ∧ ― ‹The list is a permutation›
isPartition_map R h xs' lo hi p ∧ ― ‹We have a valid partition on the resulting list›
lo ≤ p ∧ p ≤ hi ∧ ― ‹The partition index is in bounds›
(∀ i. i<lo ⟶ xs'!i=xs!i) ∧ (∀ i. hi<i∧i<length xs' ⟶ xs'!i=xs!i)› ― ‹Everything else is unchanged.›
*)

lemma partition_main_correct:
assumes bounds: ‹hi < length xs› ‹lo ≤ hi› and
trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹partition_main R h lo hi xs ≤ SPEC(λ(xs', p). mset xs = mset xs' ∧
lo ≤ p ∧ p ≤ hi ∧ isPartition_map R h xs' lo hi p ∧ (∀ i. i<lo ⟶ xs'!i=xs!i) ∧ (∀ i. hi<i∧i<length xs' ⟶ xs'!i=xs!i))›
proof -
have K: ‹b ≤ hi - Suc n ⟹ n > 0 ⟹ Suc n ≤ hi ⟹ Suc b ≤ hi - n› for b hi n
by auto
have L: ‹~ R (h x) (h y) ⟹ R (h y) (h x)› for x y ― ‹Corollary of linearity›
using assms by blast
have M: ‹a < Suc b ≡ a = b ∨ a < b› for a b
by linarith
have N: ‹(a::nat) ≤ b ≡ a = b ∨ a < b› for a b
by arith

show ?thesis
unfolding partition_main_def choose_pivot_def
apply (refine_vcg WHILEIT_rule[where R = ‹measure(λ(i,j,xs). hi-j)›])
subgoal using assms by blast ― ‹We feed our assumption to the assertion›
subgoal by auto ― ‹WF›
subgoal ― ‹Invariant holds before the first iteration›
unfolding partition_main_inv_def
using assms apply simp by linarith
subgoal unfolding partition_main_inv_def by simp
subgoal unfolding partition_main_inv_def by simp
subgoal
unfolding partition_main_inv_def
apply (auto dest: mset_eq_length)
done
subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
subgoal
unfolding partition_main_inv_def apply (auto dest: mset_eq_length)
by (metis L M mset_eq_length nat_le_eq_or_lt)

subgoal unfolding partition_main_inv_def by simp ― ‹assertions, etc›
subgoal unfolding partition_main_inv_def by simp
subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
subgoal unfolding partition_main_inv_def by simp
subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
subgoal unfolding partition_main_inv_def by (auto dest: mset_eq_length)
subgoal unfolding partition_main_inv_def by simp
subgoal unfolding partition_main_inv_def by simp

subgoal ― ‹After the last iteration, we have a partitioning! :-)›
unfolding partition_main_inv_def by (auto simp add: isPartition_wrt_def)
subgoal ― ‹And the lower out-of-bounds parts of the list haven't been changed›
unfolding partition_main_inv_def by auto
subgoal ― ‹And the upper out-of-bounds parts of the list haven't been changed›
unfolding partition_main_inv_def by auto
done
qed

definition partition_between :: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat ⇒ nat ⇒ 'a list ⇒ ('a list × nat) nres› where
‹partition_between R h lo hi xs0 = do {
ASSERT(hi < length xs0 ∧ lo ≤ hi);
k ← choose_pivot R h xs0 lo hi; ― ‹choice of pivot›
ASSERT(k < length xs0);
xs ← RETURN (swap xs0 k hi); ― ‹move the pivot to the last position, before we start the actual loop›
ASSERT(length xs = length xs0);
partition_main R h lo hi xs
}›

lemma partition_between_correct:
assumes ‹hi < length xs› and ‹lo ≤ hi› and
‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹partition_between R h lo hi xs ≤ SPEC(uncurry (partition_spec R h xs lo hi))›
proof -
have K: ‹b ≤ hi - Suc n ⟹ n > 0 ⟹ Suc n ≤ hi ⟹ Suc b ≤ hi - n› for b hi n
by auto
show ?thesis
unfolding partition_between_def choose_pivot_def
apply (refine_vcg partition_main_correct)
using assms apply (auto dest: mset_eq_length simp add: partition_spec_def)
by (metis dual_order.strict_trans2 less_imp_not_eq2 mset_eq_length swap_nth)
qed

text ‹We use the median of the first, the middle, and the last element.›
definition choose_pivot3 where
‹choose_pivot3 R h xs lo (hi::nat) = do {
ASSERT(lo < length xs);
ASSERT(hi < length xs);
let k' = (hi - lo) div 2;
let k = lo + k';
ASSERT(k < length xs);
let start = h (xs ! lo);
let mid = h (xs ! k);
let end = h (xs ! hi);
if (R start mid ∧ R mid end) ∨ (R end mid ∧ R mid start) then RETURN k
else if (R start end ∧ R end mid) ∨ (R mid end ∧ R end start) then RETURN hi
else RETURN lo
}›

― ‹We only have to show that this procedure yields a valid index between ‹lo› and ‹hi›.›
lemma choose_pivot3_choose_pivot:
assumes ‹lo < length xs› ‹hi < length xs› ‹hi ≥ lo›
shows ‹choose_pivot3 R h xs lo hi ≤ ⇓ Id (choose_pivot R h xs lo hi)›
unfolding choose_pivot3_def choose_pivot_def
using assms by (auto intro!: ASSERT_leI simp: Let_def)

text ‹The refined partion function: We use the above pivot function and fold instead of non-deterministic iteration.›
definition partition_between_ref
:: ‹('b ⇒ 'b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ nat ⇒ nat ⇒ 'a list ⇒ ('a list × nat) nres›
where
‹partition_between_ref R h lo hi xs0 = do {
ASSERT(hi < length xs0 ∧ hi < length xs0 ∧ lo ≤ hi);
k ← choose_pivot3 R h xs0 lo hi; ― ‹choice of pivot›
ASSERT(k < length xs0);
xs ← RETURN (swap xs0 k hi); ― ‹move the pivot to the last position, before we start the actual loop›
ASSERT(length xs = length xs0);
partition_main R h lo hi xs
}›

lemma partition_main_ref':
‹partition_main R h lo hi xs
≤ ⇓ ((λ a b c d. Id) a b c d) (partition_main R h lo hi xs)›
by auto

(*TODO already exists somewhere*)
lemma Down_id_eq:
‹⇓Id x = x›
by auto

lemma partition_between_ref_partition_between:
‹partition_between_ref R h lo hi xs ≤ (partition_between R h lo hi xs)›
proof -
have swap: ‹(swap xs k hi, swap xs ka hi) ∈ Id› if ‹k = ka›
for k ka
using that by auto
have [refine0]: ‹(h (xsa ! hi), h (xsaa ! hi)) ∈ Id›
if ‹(xsa, xsaa) ∈ Id›
for xsa xsaa
using that by auto

show ?thesis
apply (subst (2) Down_id_eq[symmetric])
unfolding partition_between_ref_def
partition_between_def
OP_def
apply (refine_vcg choose_pivot3_choose_pivot swap partition_main_correct)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
by (auto intro: Refine_Basic.Id_refine dest: mset_eq_length)
qed

text ‹Technical lemma for sepref›

lemma partition_between_ref_partition_between':
‹(uncurry2 (partition_between_ref R h), uncurry2 (partition_between R h)) ∈
(nat_rel ×⇩r nat_rel) ×⇩r ⟨Id⟩list_rel →⇩f ⟨⟨Id⟩list_rel ×⇩r nat_rel⟩nres_rel›
by (intro frefI nres_relI)
(auto intro: partition_between_ref_partition_between)

text ‹Example instantiation for pivot›
definition choose_pivot3_impl where
‹choose_pivot3_impl = choose_pivot3 (≤) id›

lemma partition_between_ref_correct:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
and bounds: ‹hi < length xs› ‹lo ≤ hi›
shows ‹partition_between_ref R h lo hi xs ≤ SPEC (uncurry (partition_spec R h xs lo hi))›
proof -
show ?thesis
apply (rule partition_between_ref_partition_between[THEN order_trans])
using bounds apply (rule partition_between_correct[where h=h])
subgoal by (rule trans)
subgoal by (rule lin)
done
qed

text ‹Refined quicksort algorithm: We use the refined partition function.›
definition quicksort_ref :: ‹_ ⇒ _ ⇒ nat × nat × 'a list ⇒ 'a list nres› where
‹quicksort_ref R h = (λ(lo,hi,xs0).
do {
RECT (λf (lo,hi,xs). do {
ASSERT(lo ≤ hi ∧ hi < length xs0 ∧ mset xs = mset xs0);
(xs, p) ← partition_between_ref R h lo hi xs; ― ‹This is the refined partition function. Note that we need the premises (trans,lin,bounds) here.›
ASSERT(mset xs = mset xs0 ∧ p ≥ lo ∧ p < length xs0);
xs ← (if p-1≤lo then RETURN xs else f (lo, p-1, xs));
ASSERT(mset xs = mset xs0);
if hi≤p+1 then RETURN xs else f (p+1, hi, xs)
}) (lo,hi,xs0)
})›

(*TODO share*)
lemma fref_to_Down_curry2:
‹(uncurry2 f, uncurry2 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' y y' z z'. P ((x', y'), z') ⟹ (((x, y), z), ((x', y'), z')) ∈ A⟹
f x y z ≤ ⇓ B (g x' y' z'))›
unfolding fref_def uncurry_def nres_rel_def
by auto

lemma fref_to_Down_curry:
‹(f, g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
(⋀x x' . P x' ⟹ (x, x') ∈ A⟹
f x  ≤ ⇓ B (g x'))›
unfolding fref_def uncurry_def nres_rel_def
by auto

lemma quicksort_ref_quicksort:
assumes bounds: ‹hi < length xs› ‹lo ≤ hi› and
trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹quicksort_ref R h x0 ≤ ⇓ Id (quicksort R h x0)›
proof -
have wf: ‹wf (measure (λ(lo, hi, xs). Suc hi - lo))›
by auto
have pre: ‹x0 = x0' ⟹ (x0, x0') ∈ Id ×⇩r Id ×⇩r ⟨Id⟩list_rel› for x0 x0' :: ‹nat × nat × 'b list›
by auto
have [refine0]: ‹(x1e = x1d) ⟹ (x1e,x1d) ∈ Id› for x1e x1d :: ‹'b list›
by auto

show ?thesis
unfolding quicksort_def quicksort_ref_def
apply (refine_vcg pre partition_between_ref_partition_between'[THEN fref_to_Down_curry2])

text ‹First assertion (premise for partition)›
subgoal
by auto
text ‹First assertion (premise for partition)›
subgoal
by auto
subgoal
by (auto dest: mset_eq_length)
subgoal
by (auto dest: mset_eq_length mset_eq_setD)

text ‹Correctness of the concrete partition function›
subgoal
apply (simp, rule partition_between_ref_correct)
subgoal by (rule trans)
subgoal by (rule lin)
subgoal by auto ― ‹first premise›
subgoal by auto ― ‹second premise›
done
subgoal
by (auto dest: mset_eq_length mset_eq_setD)
subgoal by (auto simp: partition_spec_def isPartition_wrt_def)
subgoal by (auto simp: partition_spec_def isPartition_wrt_def dest: mset_eq_length)
subgoal
by (auto dest: mset_eq_length mset_eq_setD)
subgoal
by (auto dest: mset_eq_length mset_eq_setD)
subgoal
by (auto dest: mset_eq_length mset_eq_setD)
subgoal
by (auto dest: mset_eq_length mset_eq_setD)

by simp+
qed

― ‹Sort the entire list›
definition full_quicksort where
‹full_quicksort R h xs ≡ if xs = [] then RETURN xs else quicksort R h (0, length xs - 1, xs)›

definition full_quicksort_ref where
‹full_quicksort_ref R h xs ≡
if List.null xs then RETURN xs
else quicksort_ref R h (0, length xs - 1, xs)›

definition full_quicksort_impl :: ‹nat list ⇒ nat list nres› where
‹full_quicksort_impl xs = full_quicksort_ref (≤) id xs›

lemma full_quicksort_ref_full_quicksort:
assumes trans: ‹⋀ x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹(full_quicksort_ref R h, full_quicksort R h) ∈
⟨Id⟩list_rel →⇩f ⟨ ⟨Id⟩list_rel⟩nres_rel›
proof -
show ?thesis
unfolding full_quicksort_ref_def full_quicksort_def
apply (intro frefI nres_relI)
apply (auto intro!: quicksort_ref_quicksort[unfolded Down_id_eq] simp: List.null_def)
subgoal by (rule trans)
subgoal using lin by blast
done
qed

lemma sublist_entire:
‹sublist xs 0 (length xs - 1) = xs›
by (simp add: sublist_def)

lemma sorted_sublist_wrt_entire:
assumes ‹sorted_sublist_wrt R xs 0 (length xs - 1)›
shows ‹sorted_wrt R xs›
proof -
have ‹sorted_wrt R (sublist xs 0 (length xs - 1))›
using assms by (simp add: sorted_sublist_wrt_def )
then show ?thesis
by (metis sublist_entire)
qed

lemma sorted_sublist_map_entire:
assumes ‹sorted_sublist_map R h xs 0 (length xs - 1)›
shows ‹sorted_wrt (λ x y. R (h x) (h y)) xs›
proof -
show ?thesis
using assms by (rule sorted_sublist_wrt_entire)
qed

text ‹Final correctness lemma›
theorem full_quicksort_correct_sorted:
assumes
trans: ‹⋀x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and lin: ‹⋀x y. x ≠ y ⟹ R (h x) (h y) ∨ R (h y) (h x)›
shows ‹full_quicksort R h xs ≤ ⇓ Id (SPEC(λxs'. mset xs' = mset xs ∧ sorted_wrt (λ x y. R (h x) (h y)) xs'))›
proof -
show ?thesis
unfolding full_quicksort_def
apply (refine_vcg)
subgoal by simp ― ‹case xs=[]›
subgoal by simp ― ‹case xs=[]›

apply (rule quicksort_correct[THEN order_trans])
subgoal by (rule trans)
subgoal by (rule lin)
subgoal by linarith
subgoal by simp

apply (simp add: Misc.subset_Collect_conv, intro allI impI conjI)
subgoal
by (auto simp add: quicksort_post_def)
subgoal
apply (rule sorted_sublist_map_entire)
by (auto simp add: quicksort_post_def dest: mset_eq_length)
done
qed

lemma full_quicksort_correct:
assumes
trans: ‹⋀x y z. ⟦R (h x) (h y); R (h y) (h z)⟧ ⟹ R (h x) (h z)› and
lin: ‹⋀x y. R (h x) (h y) ∨ R (h y) (h x)›
shows ‹full_quicksort R h xs ≤ ⇓ Id (SPEC(λxs'. mset xs' = mset xs))›
by (rule order_trans[OF full_quicksort_correct_sorted])
(use assms in auto)

end


Theory More_Loops

(*
File:         More_Loops.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Maintainer:   Mathias Fleury, JKU
*)
theory More_Loops
imports
"HOL-Library.Rewrite"
begin

subsection ‹More Theorem about Loops›

text ‹Most theorem below have a counterpart in the Refinement Framework that is weaker (by missing
assertions for example that are critical for code generation).
›
lemma Down_id_eq:
‹⇓Id x = x›
by auto

lemma while_upt_while_direct1:
"b ≥ a ⟹
do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
([a..<b],σ);
RETURN σ
} ≤ do {
(_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
RETURN σ
}"
apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
apply (refine_vcg WHILET_refine[where R = ‹{((l, x'), (i::nat, x::'a)). x= x' ∧ i ≤ b ∧ i ≥ a ∧
l = drop (i-a) [a..<b]}›])
subgoal by auto
subgoal by (auto simp: FOREACH_cond_def)
subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
subgoal by auto
done

lemma while_upt_while_direct2:
"b ≥ a ⟹
do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
([a..<b],σ);
RETURN σ
} ≥ do {
(_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
RETURN σ
}"
apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
apply (refine_vcg WHILET_refine[where R = ‹{((i::nat, x::'a), (l, x')). x= x' ∧ i ≤ b ∧ i ≥ a ∧
l = drop (i-a) [a..<b]}›])
subgoal by auto
subgoal by (auto simp: FOREACH_cond_def)
subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
subgoal by auto
done

lemma while_upt_while_direct:
"b ≥ a ⟹
do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x})
([a..<b],σ);
RETURN σ
} = do {
(_,σ) ← WHILE⇩T (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
RETURN σ
}"
using while_upt_while_direct1[of a b] while_upt_while_direct2[of a b]
unfolding order_eq_iff by fast

lemma while_nfoldli:
"do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
RETURN σ
} ≤ nfoldli l c f σ"
apply (induct l arbitrary: σ)
apply (subst WHILET_unfold)
apply (simp add: FOREACH_cond_def)

apply (subst WHILET_unfold)
apply (auto
simp: FOREACH_cond_def FOREACH_body_def
intro: bind_mono Refine_Basic.bind_mono(1))
done
lemma nfoldli_while: "nfoldli l c f σ
≤
(WHILE⇩T⇗I⇖
(FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l, σ) ⤜
(λ(_, σ). RETURN σ))"
proof (induct l arbitrary: σ)
case Nil thus ?case by (subst WHILEIT_unfold) (auto simp: FOREACH_cond_def)
next
case (Cons x ls)
show ?case
proof (cases "c σ")
case False thus ?thesis
apply (subst WHILEIT_unfold)
unfolding FOREACH_cond_def
by simp
next
case [simp]: True
from Cons show ?thesis
apply (subst WHILEIT_unfold)
unfolding FOREACH_cond_def FOREACH_body_def
apply clarsimp
apply (rule Refine_Basic.bind_mono)
apply simp_all
done
qed
qed

lemma while_eq_nfoldli: "do {
(_,σ) ← WHILE⇩T (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
RETURN σ
} = nfoldli l c f σ"
apply (rule antisym)
apply (rule while_nfoldli)
apply (rule order_trans[OF nfoldli_while[where I="λ_. True"]])
apply (simp add: WHILET_def)
done

end

Theory PAC_Specification

(*
File:         PAC_Specification.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Maintainer:   Mathias Fleury, JKU
*)
theory PAC_Specification
imports PAC_More_Poly
begin

section ‹Specification of the PAC checker›

subsection ‹Ideals›

type_synonym int_poly = ‹int mpoly›
definition polynomial_bool :: ‹int_poly set› where
‹polynomial_bool = (λc. Var c ^ 2 - Var c)  UNIV›

definition pac_ideal where
‹pac_ideal A ≡ ideal (A ∪ polynomial_bool)›

lemma X2_X_in_pac_ideal:
‹Var c ^ 2 - Var c ∈ pac_ideal A›
unfolding polynomial_bool_def pac_ideal_def
by (auto intro: ideal.span_base)

lemma pac_idealI1[intro]:
‹p ∈ A ⟹ p ∈ pac_ideal A›
unfolding pac_ideal_def
by (auto intro: ideal.span_base)

lemma pac_idealI2[intro]:
‹p ∈ ideal A ⟹ p ∈ pac_ideal A›
using ideal.span_subspace_induct pac_ideal_def by blast

lemma pac_idealI3[intro]:
‹p ∈ ideal A ⟹ p*q ∈ pac_ideal A›
by (metis ideal.span_scale mult.commute pac_idealI2)

lemma pac_ideal_Xsq2_iff:
‹Var c ^ 2 ∈ pac_ideal A ⟷ Var c ∈ pac_ideal A›
unfolding pac_ideal_def
apply (subst (2) ideal.span_add_eq[symmetric, OF X2_X_in_pac_ideal[of c, unfolded pac_ideal_def]])
apply auto
done

lemma diff_in_polynomial_bool_pac_idealI:
assumes a1: "p ∈ pac_ideal A"
assumes a2: "p - p' ∈ More_Modules.ideal polynomial_bool"
shows ‹p' ∈ pac_ideal A›
proof -
have "insert p polynomial_bool ⊆ pac_ideal A"
using a1 unfolding pac_ideal_def by (meson ideal.span_superset insert_subset le_sup_iff)
then show ?thesis
using a2 unfolding pac_ideal_def by (metis (no_types) ideal.eq_span_insert_eq ideal.span_subset_spanI ideal.span_superset insert_subset subsetD)
qed

lemma diff_in_polynomial_bool_pac_idealI2:
assumes a1: "p ∈ A"
assumes a2: "p - p' ∈ More_Modules.ideal polynomial_bool"
shows ‹p' ∈ pac_ideal A›
using diff_in_polynomial_bool_pac_idealI[OF _ assms(2), of A] assms(1)
by (auto simp: ideal.span_base)

lemma pac_ideal_alt_def:
‹pac_ideal A = ideal (A ∪ ideal polynomial_bool)›
unfolding pac_ideal_def
by (meson ideal.span_eq ideal.span_mono ideal.span_superset le_sup_iff subset_trans sup_ge2)

text ‹

The equality on ideals is restricted to polynomials whose variable
appear in the set of ideals. The function restrict sets:

›
definition restricted_ideal_to where
‹restricted_ideal_to B A = {p ∈ A. vars p  ⊆ B}›

abbreviation restricted_ideal_to⇩I where
‹restricted_ideal_to⇩I B A ≡ restricted_ideal_to B (pac_ideal (set_mset A))›

abbreviation restricted_ideal_to⇩V where
‹restricted_ideal_to⇩V B ≡ restricted_ideal_to (⋃(vars  set_mset B))›

abbreviation restricted_ideal_to⇩V⇩I where
‹restricted_ideal_to⇩V⇩I B A ≡ restricted_ideal_to (⋃(vars  set_mset B)) (pac_ideal (set_mset A))›

lemma restricted_idealI:
‹p ∈ pac_ideal (set_mset A) ⟹ vars p ⊆ C ⟹ p ∈ restricted_ideal_to⇩I C A›
unfolding restricted_ideal_to_def
by auto

‹pq ∈ pac_ideal (set_mset A) ⟹ pac_ideal (insert pq (set_mset A)) = pac_ideal (set_mset A)›
by (auto simp: pac_ideal_alt_def ideal.span_insert_idI)

‹p ∈# A ⟹ q ∈# A ⟹ p + q ∈ pac_ideal (set_mset A)›
lemma pac_ideal_mult:
‹p ∈# A ⟹ p * q ∈ pac_ideal (set_mset A)›
by (simp add: ideal.span_base pac_idealI3)

lemma pac_ideal_mono:
‹A ⊆ B ⟹ pac_ideal A ⊆ pac_ideal B›
using ideal.span_mono[of ‹A ∪ _› ‹B ∪ _›]
by (auto simp: pac_ideal_def intro: ideal.span_mono)

subsection ‹PAC Format›

text ‹The PAC format contains three kind of steps:
▪ ▩‹add› that adds up two polynomials that are known.
▪ ▩‹mult› that multiply a known polynomial with another one.
▪ ▩‹del› that removes a polynomial that cannot be reused anymore.

To model the simplification that happens, we add the \<^term>‹p - p' ∈ polynomial_bool›
stating that \<^term>‹p› and  \<^term>‹p'› are equivalent.
›

type_synonym pac_st = ‹(nat set × int_poly multiset)›

inductive PAC_Format :: ‹pac_st ⇒ pac_st ⇒ bool› where
‹PAC_Format (𝒱, A) (𝒱, add_mset p' A)›
if
‹p ∈# A› ‹q ∈# A›
‹p+q - p' ∈ ideal polynomial_bool›
‹vars p' ⊆ 𝒱› |
mult:
‹PAC_Format (𝒱, A) (𝒱, add_mset p' A)›
if
‹p ∈# A›
‹p*q - p' ∈ ideal polynomial_bool›
‹vars p' ⊆ 𝒱›
‹vars q ⊆ 𝒱› |
del:
‹p ∈# A ⟹ PAC_Format (𝒱, A) (𝒱, A - {#p#})› |
extend_pos:
‹PAC_Format (𝒱, A) (𝒱 ∪ {x' ∈ vars (-Var x + p'). x' ∉ 𝒱}, add_mset (-Var x + p') A)›
if
‹(p')⇧2 - p' ∈ ideal polynomial_bool›
‹vars p' ⊆ 𝒱›
‹x ∉ 𝒱›

text  ‹
In the PAC format above, we have a technical condition on the
normalisation: \<^term>‹vars p' ⊆ vars (p + q)› is here to ensure that
we don't normalise \<^term>‹0 :: int mpoly› to  \<^term>‹Var x^2 - Var x :: int mpoly›
for a new variable \<^term>‹x :: nat›. This is completely obvious for the normalisation
process we have in mind when we write the specification, but we must add it
explicitly because we are too general.
›

lemmas  PAC_Format_induct_split =
PAC_Format.induct[split_format(complete), of V A V' A' for V A V' A']

lemma PAC_Format_induct[consumes 1, case_names add mult del ext]:
assumes
‹PAC_Format (𝒱, A) (𝒱', A')› and
cases:
‹⋀p q p'  A 𝒱. p ∈# A ⟹ q ∈# A ⟹ p+q - p' ∈ ideal polynomial_bool ⟹ vars p' ⊆ 𝒱 ⟹ P 𝒱 A 𝒱 (add_mset p' A)›
‹⋀p q p' A 𝒱. p ∈# A ⟹ p*q - p' ∈ ideal polynomial_bool ⟹ vars p' ⊆ 𝒱 ⟹ vars q ⊆ 𝒱 ⟹
P 𝒱 A 𝒱 (add_mset p' A)›
‹⋀p A 𝒱. p ∈# A ⟹ P 𝒱 A 𝒱 (A - {#p#})›
‹⋀p' x r.
(p')^2 - (p') ∈ ideal polynomial_bool ⟹ vars p' ⊆ 𝒱 ⟹
x ∉ 𝒱 ⟹ P 𝒱 A (𝒱 ∪ {x' ∈ vars (p' - Var x). x' ∉ 𝒱}) (add_mset (p' -Var x) A)›
shows
‹P 𝒱 A 𝒱' A'›
using assms(1) apply -
by (induct V≡𝒱 A≡A 𝒱' A' rule: PAC_Format_induct_split)
(auto intro: assms(1) cases)

text ‹

The theorem below (based on the proof ideal by Manuel Kauers) is the
correctness theorem of extensions. Remark that the assumption \<^term>‹vars
q ⊆ 𝒱› is only used to show that \<^term>‹x' ∉ vars q›.

›
lemma extensions_are_safe:
assumes ‹x' ∈ vars p› and
x': ‹x' ∉ 𝒱› and
‹⋃ (vars  set_mset A) ⊆ 𝒱› and
p_x_coeff: ‹coeff p (monomial (Suc 0) x') = 1› and
vars_q: ‹vars q ⊆ 𝒱› and
q: ‹q ∈ More_Modules.ideal (insert p (set_mset A ∪ polynomial_bool))› and
leading: ‹x' ∉ vars (p - Var x')› and
diff: ‹(Var x' - p)⇧2 - (Var x' - p) ∈ More_Modules.ideal polynomial_bool›
shows
‹q ∈ More_Modules.ideal (set_mset A ∪ polynomial_bool)›
proof -
define p' where ‹p' ≡ p - Var x'›
let ?v = ‹Var x' :: int mpoly›
have p_p': ‹p = ?v + p'›
by (auto simp: p'_def)
define q' where ‹q' ≡ Var x' - p›
have q_q': ‹p = ?v - q'›
by (auto simp: q'_def)
have diff: ‹q'^2 - q' ∈ More_Modules.ideal polynomial_bool›
using diff unfolding q_q' by auto

have [simp]: ‹vars ((Var c)⇧2 - Var c :: int mpoly) = {c}› for c
apply (auto simp: vars_def Var_def Var⇩0_def mpoly.MPoly_inverse keys_def lookup_minus_fun
lookup_times_monomial_right single.rep_eq split: if_splits)
apply (auto simp: vars_def Var_def Var⇩0_def mpoly.MPoly_inverse keys_def lookup_minus_fun
lookup_times_monomial_right single.rep_eq when_def ac_simps adds_def lookup_plus_fun
power2_eq_square times_mpoly.rep_eq minus_mpoly.rep_eq split: if_splits)
apply (rule_tac x = ‹(2 :: nat ⇒⇩0 nat) * monomial (Suc 0) c› in exI)
apply (auto dest: monomial_0D simp: plus_eq_zero_2 lookup_plus_fun mult_2)
by (meson Suc_neq_Zero monomial_0D plus_eq_zero_2)

have eq: ‹More_Modules.ideal (insert p (set_mset A ∪ polynomial_bool)) =
More_Modules.ideal (insert p (set_mset A ∪ (λc. Var c ^ 2 - Var c)  {c. c ≠ x'}))›
(is ‹?A = ?B› is ‹_ = More_Modules.ideal ?trimmed›)
proof -
let ?C = ‹insert p (set_mset A ∪ (λc. Var c ^ 2 - Var c)  {c. c ≠ x'})›
let ?D = ‹(λc. Var c ^ 2 - Var c)  {c. c ≠ x'}›
have diff: ‹q'^2 - q' ∈ More_Modules.ideal ?D› (is ‹?q ∈ _›)
proof -
obtain r t where
q: ‹?q = (∑a∈t. r a * a)› and
fin_t: ‹finite t› and
t: ‹t ⊆ polynomial_bool›
using diff unfolding ideal.span_explicit
by auto
show ?thesis
proof (cases ‹?v^2-?v ∉ t›)
case True
then show ‹?thesis›
using q fin_t t unfolding ideal.span_explicit
by (auto intro!: exI[of _ ‹t - {?v^2 -?v}›] exI[of _ r]
simp: polynomial_bool_def sum_diff1)
next
case False
define t' where ‹t' = t - {?v^2 - ?v}›
have t_t': ‹t = insert (?v^2 - ?v) t'› and
notin: ‹?v^2 - ?v ∉ t'› and
‹t' ⊆ (λc. Var c ^ 2 - Var c)  {c. c ≠ x'}›
using False t unfolding t'_def polynomial_bool_def by auto
have mon: ‹monom (monomial (Suc 0) x') 1 = Var x'›
by (auto simp: coeff_def minus_mpoly.rep_eq Var_def Var⇩0_def monom_def
times_mpoly.rep_eq lookup_minus lookup_times_monomial_right mpoly.MPoly_inverse)
then have ‹∀a. ∃g h. r a = ?v * g + h ∧ x' ∉ vars h›
using polynomial_split_on_var[of ‹r _› x']
by metis
then obtain g h where
r: ‹r a = ?v * g a + h a› and
x'_h: ‹x' ∉ vars (h a)› for a
using polynomial_split_on_var[of ‹r a› x']
by metis
have  ‹?q = ((∑a∈t'. g a * a) + r (?v^2-?v) * (?v - 1)) * ?v + (∑a∈t'. h a * a)›
using fin_t notin unfolding t_t' q r
by (auto simp: field_simps comm_monoid_add_class.sum.distrib
power2_eq_square ideal.scale_left_commute sum_distrib_left)
moreover have ‹x' ∉ vars ?q›
by (metis (no_types, hide_lams) Groups.add_ac(2) Un_iff add_diff_cancel_left'
vars_in_right_only vars_mult)
moreover {
have ‹x' ∉ (⋃m∈t' - {?v^2-?v}. vars (h m * m))›
using fin_t x'_h vars_mult[of ‹h _›] ‹t ⊆ polynomial_bool›
by (auto simp: polynomial_bool_def t_t' elim!: vars_unE)
then have ‹x' ∉ vars (∑a∈t'. h a * a)›
using vars_setsum[of ‹t'› ‹λa. h a * a›] fin_t x'_h t notin
by (auto simp: t_t')
}
ultimately have ‹?q = (∑a∈t'. h a * a)›
unfolding mon[symmetric]
by (rule polynomial_decomp_alien_var(2)[unfolded])
then show ?thesis
using t fin_t ‹t' ⊆ (λc. Var c ^ 2 - Var c)  {c. c ≠ x'}›
unfolding ideal.span_explicit t_t'
by auto
qed
qed
have eq1: ‹More_Modules.ideal (insert p (set_mset A ∪ polynomial_bool)) =
More_Modules.ideal (insert (?v^2 - ?v) ?C)›
(is ‹More_Modules.ideal _ = More_Modules.ideal (insert _ ?C)›)
by (rule arg_cong[of _ _ More_Modules.ideal])
(auto simp: polynomial_bool_def)
moreover have ‹?v^2 - ?v ∈ More_Modules.ideal ?C›
proof -
have ‹?v - q' ∈ More_Modules.ideal ?C›
by (auto simp: q_q' ideal.span_base)
from ideal.span_scale[OF this, of ‹?v + q' - 1›] have ‹(?v - q') * (?v + q' - 1) ∈ More_Modules.ideal ?C›
by (auto simp: field_simps)
moreover have ‹q'^2 - q' ∈ More_Modules.ideal ?C›
using diff by (smt Un_insert_right ideal.span_mono insert_subset subsetD sup_ge2)
ultimately have ‹(?v - q') * (?v + q' - 1) + (q'^2 - q') ∈ More_Modules.ideal ?C›
moreover have ‹?v^2 - ?v = (?v - q') * (?v + q' - 1) + (q'^2 - q')›
by (auto simp: p'_def q_q' field_simps power2_eq_square)
ultimately show ?thesis by simp
qed
ultimately show ?thesis
using ideal.span_insert_idI by blast
qed

have ‹n < m ⟹ n > 0 ⟹ ∃q. ?v^n = ?v + q * (?v^2 - ?v)› for n m :: nat
proof (induction m arbitrary: n)
case 0
then show ?case by auto
next
case (Suc m n) note IH = this(1-)
consider
‹n < m› |
‹m = n› ‹n > 1› |
‹n = 1›
using IH
by (cases ‹n < m›; cases n) auto
then show ?case
proof cases
case 1
then show ?thesis using IH by auto
next
case 2
have eq: ‹?v^(n) = ((?v :: int mpoly) ^ (n-2)) * (?v^2-?v) + ?v^(n-1)›
using 2 by (auto simp: field_simps power_eq_if
ideal.scale_right_diff_distrib)
obtain q where
q: ‹?v^(n-1) = ?v + q * (?v^2 - ?v)›
using IH(1)[of ‹n-1›] 2
by auto
show ?thesis
using q unfolding eq
by (auto intro!: exI[of _ ‹Var x' ^ (n - 2) + q›] simp: distrib_right)
next
case 3
then show ‹?thesis›
by auto
qed
qed

obtain r t where
q: ‹q = (∑a∈t. r a * a)› and
fin_t: ‹finite t› and
t: ‹t ⊆ ?trimmed›
using q unfolding eq unfolding ideal.span_explicit
by auto

define t' where ‹t' ≡ t - {p}›
have t': ‹t = (if p ∈ t then insert p t' else t')› and
t''[simp]: ‹p ∉ t'›
unfolding t'_def by auto
show ?thesis
proof (cases ‹r p = 0 ∨ p ∉ t›)
case True
have
q: ‹q = (∑a∈t'. r a * a)› and
fin_t: ‹finite t'› and
t: ‹t' ⊆ set_mset A ∪ polynomial_bool›
using q fin_t t True t''
apply (subst (asm) t')
apply (auto intro: sum.cong simp: sum.insert_remove t'_def)
using q fin_t t True t''
apply (auto intro: sum.cong simp: sum.insert_remove t'_def polynomial_bool_def)
done
then show ?thesis
by (auto simp: ideal.span_explicit)
next
case False
then have ‹r p ≠ 0› and ‹p ∈ t›
by auto
then have t: ‹t = insert p t'›
by (auto simp: t'_def)

have ‹x' ∉ vars (- p')›
using leading p'_def vars_in_right_only by fastforce
have mon: ‹monom (monomial (Suc 0) x') 1 = Var x'›
by (auto simp:coeff_def minus_mpoly.rep_eq Var_def Var⇩0_def monom_def
times_mpoly.rep_eq lookup_minus lookup_times_monomial_right mpoly.MPoly_inverse)
then have ‹∀a. ∃g h. r a = (?v + p') * g + h ∧ x' ∉ vars h›
using polynomial_split_on_var2[of x' ‹-p'› ‹r _›]  ‹x' ∉ vars (- p')›
then obtain g h where
r: ‹r a = p * g a + h a› and
x'_h: ‹x' ∉ vars (h a)› for a
using polynomial_split_on_var2[of x' p' ‹r a›] unfolding p_p'[symmetric]
by metis

have ISABLLE_come_on: ‹a * (p * g a) = p * (a * g a)› for a
by auto
have q1: ‹q = p * (∑a∈t'. g a * a) + (∑a∈t'. h a * a) + p * r p›
(is ‹_ = _ + ?NOx' + _›)
using fin_t t'' unfolding q t ISABLLE_come_on r
apply (subst semiring_class.distrib_right)+
apply (auto simp: comm_monoid_add_class.sum.distrib semigroup_mult_class.mult.assoc
ISABLLE_come_on simp flip: semiring_0_class.sum_distrib_right
semiring_0_class.sum_distrib_left)
by (auto simp: field_simps)
also have ‹... = ((∑a∈t'. g a * a) + r p) * p + (∑a∈t'. h a * a)›
by (auto simp: field_simps)
finally have q_decomp: ‹q = ((∑a∈t'. g a * a) + r p) * p + (∑a∈t'. h a * a)›
(is ‹q = ?X * p + ?NOx'›).

have [iff]: ‹monomial (Suc 0) c = 0 - monomial (Suc 0) c = False› for c
by (metis One_nat_def diff_is_0_eq' le_eq_less_or_eq less_Suc_eq_le monomial_0_iff single_diff zero_neq_one)
have ‹x ∈ t' ⟹ x' ∈ vars x ⟹ False› for x
using  ‹t ⊆ ?trimmed› t assms(2,3)
apply (auto simp: polynomial_bool_def dest!: multi_member_split)
apply (frule set_rev_mp)
apply assumption
apply (auto dest!: multi_member_split)
done
then have ‹x' ∉ (⋃m∈t'. vars (h m * m))›
using fin_t x'_h vars_mult[of ‹h _›]
by (auto simp: t elim!: vars_unE)
then have ‹x' ∉ vars ?NOx'›
using vars_setsum[of ‹t'› ‹λa. h a * a›] fin_t x'_h
by (auto simp: t)

moreover {
have ‹x' ∉ vars p'›
using assms(7)
unfolding p'_def
by auto
then have ‹x' ∉ vars (h p * p')›
using vars_mult[of ‹h p› p'] x'_h
by auto
}
ultimately have
‹x' ∉ vars q›
‹x' ∉ vars ?NOx'›
‹x' ∉ vars p'›
using x' vars_q vars_add[of ‹h p * p'› ‹∑a∈t'. h a * a›] x'_h
by auto
then have ‹?X = 0› and q_decomp: ‹q = ?NOx'›
unfolding mon[symmetric] p_p'
using polynomial_decomp_alien_var2[OF q_decomp[unfolded p_p' mon[symmetric]]]
by auto

then have ‹r p = (∑a∈t'. (- g a) * a)›
(is ‹_ = ?CL›)
by (auto simp: sum_negf ac_simps)

then have q2: ‹q = (∑a∈t'. a * (r a - p * g a))›
using fin_t unfolding q
apply (auto simp: t r q
sum_distrib_left
sum_distrib_right
left_diff_distrib
intro!: sum.cong)
apply (auto simp: field_simps)
done
then show ‹?thesis›
using t fin_t ‹t ⊆ ?trimmed› unfolding ideal.span_explicit
by (auto intro!: exI[of _ t'] exI[of _ ‹λa. r a - p * g a›]
simp: field_simps polynomial_bool_def)
qed
qed

lemma extensions_are_safe_uminus:
assumes ‹x' ∈ vars p› and
x': ‹x' ∉ 𝒱› and
‹⋃ (vars  set_mset A) ⊆ 𝒱› and
p_x_coeff: ‹coeff p (monomial (Suc 0) x') = -1› and
vars_q: ‹vars q ⊆ 𝒱› and
q: ‹q ∈ More_Modules.ideal (insert p (set_mset A ∪ polynomial_bool))› and
leading: ‹x' ∉ vars (p + Var x')› and
diff: ‹(Var x' + p)^2 - (Var x' + p) ∈ More_Modules.ideal polynomial_bool›
shows
‹q ∈ More_Modules.ideal (set_mset A ∪ polynomial_bool)›
proof -
have ‹q ∈ More_Modules.ideal (insert (- p) (set_mset A ∪ polynomial_bool))›
by (metis ideal.span_breakdown_eq minus_mult_minus q)

then show ?thesis
using extensions_are_safe[of x' ‹-p› 𝒱 A q] assms
using vars_in_right_only by force
qed

text ‹This is the correctness theorem of a PAC step: no polynomials are
added to the ideal.›

lemma vars_subst_in_left_only:
‹x ∉ vars p ⟹ x ∈ vars (p - Var x)› for p :: ‹int mpoly›
by (metis One_nat_def Var.abs_eq Var⇩0_def group_eq_aux monom.abs_eq mult_numeral_1 polynomial_decomp_alien_var(1) zero_neq_numeral)

lemma vars_subst_in_left_only_diff_iff:
fixes p :: ‹int mpoly›
assumes ‹x ∉ vars p›
shows ‹vars (p - Var x) = insert x (vars p)›
proof -
have ‹⋀xa. x ∉ vars p ⟹ xa ∈ vars (p - Var x) ⟹ xa ∉ vars p ⟹ xa = x›
by (metis (no_types, hide_lams) diff_0_right diff_minus_eq_add empty_iff in_vars_addE insert_iff
keys_single minus_diff_eq monom_one mult.right_neutral one_neq_zero single_zero
vars_monom_keys vars_mult_Var vars_uminus)
moreover have ‹⋀xa. x ∉ vars p ⟹ xa ∈ vars p ⟹ xa ∈ vars (p - Var x)›
by (metis add.inverse_inverse diff_minus_eq_add empty_iff insert_iff keys_single minus_diff_eq
monom_one mult.right_neutral one_neq_zero single_zero vars_in_right_only vars_monom_keys
vars_mult_Var vars_uminus)
ultimately show ?thesis
using assms
by (auto simp: vars_subst_in_left_only)
qed

lemma vars_subst_in_left_only_iff:
‹x ∉ vars p ⟹ vars (p + Var x) = insert x (vars p)› for p :: ‹int mpoly›
using vars_subst_in_left_only_diff_iff[of x ‹-p›]
by (metis diff_0 diff_diff_add vars_uminus)

‹x ∉ vars p ⟹ MPoly_Type.coeff (Var x - p) (monomial (Suc 0) x) = 1›
apply (auto simp flip: coeff_minus simp: not_in_vars_coeff0)
by (simp add: MPoly_Type.coeff_def Var.rep_eq Var⇩0_def)

‹x ∉ vars p ⟹ MPoly_Type.coeff (p - Var x) (monomial (Suc 0) x) = -1› for p :: ‹int mpoly›
apply (auto simp flip: coeff_minus simp: not_in_vars_coeff0)
by (simp add: MPoly_Type.coeff_def Var.rep_eq Var⇩0_def)

lemma ideal_insert_polynomial_bool_swap: ‹r - s ∈ ideal polynomial_bool ⟹
More_Modules.ideal (insert r  (A ∪ polynomial_bool)) = More_Modules.ideal (insert s (A ∪ polynomial_bool))›
apply auto
using ideal.eq_span_insert_eq ideal.span_mono sup_ge2 apply blast+
done

lemma PAC_Format_subset_ideal:
‹PAC_Format (𝒱, A) (𝒱', B) ⟹ ⋃(vars  set_mset A) ⊆ 𝒱 ⟹
restricted_ideal_to⇩I 𝒱 B ⊆ restricted_ideal_to⇩I 𝒱 A ∧ 𝒱 ⊆ 𝒱' ∧ ⋃(vars  set_mset B) ⊆ 𝒱'›
unfolding restricted_ideal_to_def
apply (induction rule:PAC_Format_induct)
subgoal for p q pq A 𝒱
by (force simp: ideal.span_add_eq ideal.span_base pac_ideal_insert_already_in[OF diff_in_polynomial_bool_pac_idealI[of ‹p + q› ‹_› pq]]
intro!: diff_in_polynomial_bool_pac_idealI[of ‹p + q› ‹_› pq])
subgoal for p q pq
using vars_mult[of p q]
by (force simp: ideal.span_add_eq ideal.span_base pac_ideal_mult
pac_ideal_insert_already_in[OF diff_in_polynomial_bool_pac_idealI[of ‹p*q› ‹_› pq]])
subgoal for p A
using pac_ideal_mono[of ‹set_mset (A - {#p#})› ‹set_mset A›]
by (auto dest: in_diffD)
subgoal for p x' r'
apply (subgoal_tac ‹x' ∉ vars p›)
using extensions_are_safe_uminus[of x' ‹-Var x' + p› 𝒱 A] unfolding pac_ideal_def
apply (auto simp: vars_subst_in_left_only coeff_add_left_notin)
done
done

text ‹
In general, if deletions are disallowed, then the stronger \<^term>‹B = pac_ideal A› holds.
›
lemma restricted_ideal_to_restricted_ideal_to⇩ID:
‹restricted_ideal_to 𝒱 (set_mset A) ⊆ restricted_ideal_to⇩I 𝒱 A›
by (auto simp add: Collect_disj_eq pac_idealI1 restricted_ideal_to_def)

lemma rtranclp_PAC_Format_subset_ideal:
‹rtranclp PAC_Format (𝒱, A) (𝒱', B) ⟹ ⋃(vars  set_mset A) ⊆ 𝒱 ⟹
restricted_ideal_to⇩I 𝒱 B ⊆ restricted_ideal_to⇩I 𝒱 A ∧ 𝒱 ⊆ 𝒱' ∧ ⋃(vars  set_mset B) ⊆ 𝒱'›
apply (induction rule:rtranclp_induct[of PAC_Format ‹(_, _)› ‹(_, _)›, split_format(complete)])
subgoal
by (simp add: restricted_ideal_to_restricted_ideal_to⇩ID)
subgoal
by (drule PAC_Format_subset_ideal)
(auto simp: restricted_ideal_to_def Collect_mono_iff)
done

end

Theory PAC_Map_Rel

(*
File:         PAC_Map_Rel.thy
Author:       Mathias Fleury, Daniela Kaufmann, JKU
Maintainer:   Mathias Fleury, JKU
*)
theory PAC_Map_Rel
imports
Refine_Imperative_HOL.IICF Finite_Map_Multiset
begin

section ‹Hash-Map for finite mappings›

text ‹

This function declares hash-maps for \<^typ>‹('a, 'b)fmap›, that are nicer
to use especially here where everything is finite.

›
definition fmap_rel where
[to_relAPP]:
"fmap_rel K V ≡ {(m1, m2).
(∀i j. i |∈| fmdom m2 ⟶ (j, i) ∈ K ⟶ (the (fmlookup m1 j), the (fmlookup m2 i)) ∈ V) ∧
fset (fmdom m1) ⊆ Domain K ∧ fset (fmdom m2) ⊆ Range K ∧
(∀i `