Theory IMP2_Aux_Lemmas

section ‹Auxiliary Lemma Library›  
theory IMP2_Aux_Lemmas
imports "HOL-Library.Multiset" "HOL-Library.Rewrite"
begin

text ‹This library contains auxiliary lemmas, which are useful for proving 
  various VCs.
›
 



subsection ‹Termination Proofs›

― ‹Useful lemma to show well-foundedness of some process approaching a finite upper bound›
lemma wf_bounded_supset: "finite S ⟹ wf {(Q',Q). Q'⊃Q ∧ Q'⊆ S}"
proof -
  assume [simp]: "finite S"
  hence [simp]: "!!x. finite (S-x)" by auto
  have "{(Q',Q). Q⊂Q' ∧ Q'⊆ S} ⊆ inv_image ({(s'::nat,s). s'<s}) (λQ. card (S-Q))"
  proof (intro subsetI, case_tac x, simp)
    fix a b
    assume A: "b⊂a ∧ a⊆S"
    hence "S-a ⊂ S-b" by blast
    thus "card (S-a) < card (S-b)" by (auto simp add: psubset_card_mono)
  qed
  moreover have "wf ({(s'::nat,s). s'<s})" by (rule wf_less)
  ultimately show ?thesis by (blast intro: wf_subset)
qed

text ‹Well-founded relation to approximate a finite set from below›
definition "finite_psupset S ≡ { (Q',Q). Q⊂Q' ∧ Q' ⊆ S }"
lemma finite_psupset_wf[simp, intro]: "finite S ⟹ wf (finite_psupset S)"
  unfolding finite_psupset_def by (blast intro: wf_bounded_supset)




 
subsection ‹Conversion between ‹nat› and ‹int››

lemmas nat_distribs = nat_add_distrib nat_diff_distrib Suc_diff_le nat_mult_distrib nat_div_distrib


subsection ‹Interval Sets›

lemma intvs_singleton[simp]: 
  "{i::int..<i + 1} = {i}" 
  "{i-1..<i::int} = {i-1}" 
  by auto

lemma intvs_incr_h:
  "l≤h ⟹ {l::int..<h + 1} = insert h {l..<h}"
  by auto

lemma intvs_decr_h:
  "{l::int..<h - 1} = {l..<h} - {h-1}"
  by auto
  
lemma intvs_incr_l:
  "{l+1..<h::int} = {l..<h} - {l}"
  by auto

lemma intvs_decr_l:
  "l≤h ⟹ {l-1..<h::int} = insert (l-1) {l..<h}"
  by auto
  
lemma intvs_ii_incdec:
  fixes l h :: int
  shows "l≤h+1 ⟹ {l..h+1} = insert (h+1) {l..h}"  
    and "l-1≤h ⟹ {l-1..h} = insert (l-1) {l..h}"  
    and "{l+1..h} = {l..h} - {l}"
    and "{l..h-1} = {l..h} - {h}"
  by auto
  
lemmas intvs_ie_incdec = intvs_incr_h intvs_incr_l intvs_decr_h intvs_decr_l
(* TODO: Add lemmas for ei, ee *)
lemmas intvs_incdec = intvs_ie_incdec intvs_ii_incdec

lemma intvs_lower_incr: "l<h ⟹ {l::int..<h} = insert l ({l+1..<h})" by auto
lemma intvs_upper_decr: "l<h ⟹ {l::int..<h} = insert (h-1) ({l..<h-1})" by auto

subsubsection ‹Induction on Intervals›

function intv_fwd_induct_scheme :: "int ⇒ int ⇒ unit" where
  "intv_fwd_induct_scheme l h = (if l<h then intv_fwd_induct_scheme (l+1) h else ())"
  by pat_completeness auto
termination apply (relation "measure (λ(l,h). nat (h-l))") by auto 
lemmas intv_induct = intv_fwd_induct_scheme.induct[case_names incr]

function intv_bwd_induct_scheme :: "int ⇒ int ⇒ unit" where
  "intv_bwd_induct_scheme l h = (if l<h then intv_bwd_induct_scheme l (h-1) else ())"
  by pat_completeness auto
termination apply (relation "measure (λ(l,h). nat (h-l))") by auto 
lemmas intv_bwd_induct = intv_bwd_induct_scheme.induct[case_names decr]
  


subsection ‹Multiset Lemmas›

lemma image_mset_subst_outside: "x∉#s ⟹ image_mset (f(x:=y)) s = image_mset f s"
  by (induction s) auto
  
lemma image_mset_set_subst_inside:
  assumes "finite S"
  assumes "i∈S"
  shows "image_mset (f(i:=x)) (mset_set S) = image_mset f (mset_set S) + {#x#} - {#f i#} "
  using assms  
  by (induction rule: finite_induct) (auto simp: image_mset_subst_outside)

lemma image_mset_eq_imp_set_eq: 
  assumes "image_mset f s = image_mset g s"  
  shows "f`(set_mset s) = g`set_mset s"
  using assms
  by (metis set_image_mset)
  
  
subsection ‹Equal on Set›
definition eq_on :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ 'a set ⇒ bool" ("_ = _ on _" [50,50,50] 50)
  where "s=t on X ⟷ (∀x∈X. s x = t x)"
  
lemma eq_on_subst_same: 
  "x∈X ⟹ s(x:=v) = t on X ⟷ t x = v ∧ s=t on (X-{x})"  
  "x∈X ⟹ s = t(x:=v) on X ⟷ s x = v ∧ s=t on (X-{x})"  
  by (auto simp: eq_on_def)
  
lemma eq_on_subst_other[simp]: 
  "x∉X ⟹ s(x:=v) = t on X ⟷ s=t on X"
  "x∉X ⟹ s = t(x:=v) on X ⟷ s=t on X"
  by (auto simp: eq_on_def)
  
lemma eq_on_refl[simp]: "s = s on X"  
  by (auto simp: eq_on_def)

lemma eq_on_sym[sym]: "s=t on X ⟹ t=s on X"  
  by (auto simp: eq_on_def)

lemma eq_on_trans[trans]: "r=s on X ⟹ s=t on X ⟹ r=t on X"  
  by (auto simp: eq_on_def)

lemma eq_on_trans'[trans]: "r=s on X ⟹ s=t on X' ⟹ r=t on (X∩X')"  
  by (auto simp: eq_on_def)
  
lemma eq_onD: "r = s on X ⟹ x∈X ⟹ r x = s x"  
  by (auto simp: eq_on_def)
  
      
lemma eq_on_xfer_pointwise: "⟦a=a' on r'; r⊆r'⟧ ⟹ (∀i∈r. P (a i)) ⟷ (∀i∈r. P (a' i))"  
  by (auto simp: eq_on_def subset_iff)
  
  
subsection ‹Arrays›  
  
  
subsubsection ‹Sortedness›
text ‹Sortedness as monotonicity property›
definition ran_sorted :: "(int ⇒ int) ⇒ int ⇒ int ⇒ bool" where
  "ran_sorted a l h ≡ ∀i∈{l..<h}. ∀j∈{l..<h}. i≤j ⟶ a i ≤ a j"

text ‹Alternative definition›  
lemma ran_sorted_alt: "ran_sorted a l h = ( ∀i j. l≤i ∧ i<j ∧ j<h ⟶ a i ≤ a j)" 
  unfolding ran_sorted_def 
  by auto (metis dual_order.order_iff_strict)
  
lemma ran_sorted_empty[simp]: "ran_sorted a l l"  
  by (auto simp: ran_sorted_def)
  
lemma ran_sorted_singleton[simp]: "ran_sorted a l (l+1)"  
  by (auto simp: ran_sorted_def)

lemma eq_on_xfer_ran_sorted: "⟦ a=a' on r'; {l..<h} ⊆ r' ⟧ ⟹ ran_sorted a l h ⟷ ran_sorted a' l h"
  unfolding ran_sorted_alt eq_on_def by (auto simp: subset_iff)
  
lemma combine_sorted_pivot:
  assumes "l≤i" "i<h"
  assumes "ran_sorted a l i"
  assumes "ran_sorted a (i+1) h"
  assumes "∀k∈{l..<i}. a k < a i"
  assumes "∀k∈{i+1..<h}. a k ≥ a i"
  shows "ran_sorted a l h"
  using assms unfolding ran_sorted_def Ball_def
  by clarsimp smt
  
  
  
subsubsection ‹Multiset of Ranges in Arrays›  
definition mset_ran :: "(int ⇒ 'a) ⇒ int set ⇒ 'a multiset"
  where "mset_ran a r ≡ image_mset a (mset_set r)"

lemma mset_ran_infinite[simp]: "infinite r ⟹ mset_ran a r = {#}"  
  by (auto simp: mset_ran_def)
  
lemma mset_ran_by_sum: "mset_ran a r = (∑i∈r. {#a i#})"
proof (cases "finite r")
  case True thus ?thesis
    apply (induction r)
     apply (auto simp: mset_ran_def)
    done
qed simp    

lemma mset_ran_mem[simp, intro]: "finite r ⟹ i∈r ⟹ a i ∈# mset_ran a r"
  by (auto simp: mset_ran_def)

lemma mset_ran_empty[simp]: 
  "mset_ran a {} = {#}"  
  by (auto simp: mset_ran_def)
  
lemma mset_ran_empty_iff[simp]: 
  "finite r ⟹ mset_ran a r = {#} ⟷ r={}"
  by (auto simp: mset_ran_def mset_set_empty_iff)

lemma mset_ran_single[simp]: "mset_ran a {i} = {#a i#}"  
  by (auto simp: mset_ran_def)
  
lemma mset_ran_eq_single_conv: "mset_ran a r = {#x#} ⟷ (∃i. r={i} ∧ x= a i)"  
  apply (cases "finite r")
   apply (auto simp: mset_ran_def)
  using finite_set_mset_mset_set msed_map_invR by force
  
lemma mset_ran_insert: "⟦finite r; i∉r⟧ ⟹ mset_ran a (insert i r) = add_mset (a i) (mset_ran a r)"  
  by (auto simp: mset_ran_def) 
  
  
lemma mset_ran_subst_outside: "i∉r ⟹ mset_ran (a(i:=x)) r = mset_ran a r"  
  unfolding mset_ran_def by (cases "finite r") (auto simp: image_mset_subst_outside)

lemma mset_ran_subst_inside: "finite r ⟹ i∈r ⟹ mset_ran (a(i:=x)) r = mset_ran a r + {#x#} - {#a i#}"  
  unfolding mset_ran_def by (auto simp: image_mset_set_subst_inside)
  
lemma mset_ran_combine1: "⟦finite r⇩1; finite r⇩2; r⇩1∩r⇩2={}⟧ ⟹ mset_ran a r⇩1 + mset_ran a r⇩2 = mset_ran a (r⇩1∪r⇩2)"
  by (auto simp: mset_ran_by_sum sum.union_disjoint[symmetric])

lemma mset_ran_combine2: "⟦finite r; i∉r⟧ ⟹ add_mset (a i) (mset_ran a r) = mset_ran a (insert i r)"
  using mset_ran_combine1[of "{i}" r a]
  by auto
  
lemmas mset_ran_combine = mset_ran_combine1 mset_ran_combine2
    
lemma mset_ran_cong:  
  "a = b on r ⟹ mset_ran a r = mset_ran b r"
  apply (cases "finite r")
  by (auto simp: mset_ran_by_sum eq_on_def)
  
lemma mset_ran_shift:
  "inj_on f r ⟹ mset_ran (a o f) r = mset_ran a (f`r)"
  apply (auto simp: mset_ran_def)
  by (metis image_mset_mset_set multiset.map_comp)
  
lemma mset_ran_combine_eqs:
  assumes "mset_ran a r⇩1 = mset_ran b r⇩1"
  assumes "mset_ran a r⇩2 = mset_ran b r⇩2"
  assumes "r⇩1∩r⇩2 = {}"
  shows "mset_ran a (r⇩1∪r⇩2) = mset_ran b (r⇩1∪r⇩2)"
  apply (cases "finite r⇩1"; cases "finite r⇩2"; simp?)
  using assms(1,2)
  apply (simp add: mset_ran_combine1[OF _ _ assms(3), symmetric])
  done
  
lemma mset_ran_combine_eq_diff:
  assumes "mset_ran a (r-I) = mset_ran a' (r-I)" 
  assumes "a=a' on I"  
  shows "mset_ran a r = mset_ran a' r"  
proof -
  have [simp]: "(r - I) ∩ (r ∩ I) = {}" by auto
  have [simp]: "r - I ∪ r ∩ I = r" by auto

  from assms(2) have "mset_ran a (r ∩ I) = mset_ran a' (r ∩ I)"
    by (auto simp: mset_ran_by_sum eq_on_def)
  from mset_ran_combine_eqs[OF assms(1) this] show ?thesis by auto
qed    

lemma mset_ran_eq_extend:
  assumes "mset_ran a r' = mset_ran a' r'"
  assumes "a = a' on r2"
  assumes "r-r' ⊆ r2"
  assumes "r'⊆r"
  shows "mset_ran a r = mset_ran a' r"
proof -
  have [simp]: "r' ∩ (r - r') = {}" "r' ∪ r = r" using assms(4) by auto

  from assms(2,3) have "a=a' on r-r'" by (auto simp: eq_on_def)
  then have "mset_ran a (r-r') = mset_ran a' (r-r')"
    by (auto simp: mset_ran_by_sum eq_on_def)
  from mset_ran_combine_eqs[OF assms(1) this] show ?thesis by auto 
qed    
  
lemma mset_ran_xfer_pointwise:
  assumes "mset_ran a r = mset_ran a' r"
  assumes "finite r"
  shows "(∀i∈r. P (a i)) ⟷ (∀i∈r. P (a' i))"
  using assms unfolding mset_ran_def 
  by (auto;force dest: image_mset_eq_imp_set_eq)
  

  
  
subsection ‹Swap›
definition "swap a i j ≡ a(i:=a j, j:=a i)"

lemma mset_ran_swap: "⟦ i∈r; j∈r ⟧ 
  ⟹ mset_ran (swap a i j) r = mset_ran a r"
  by (cases "finite r") (auto simp: swap_def mset_ran_subst_inside)
  

subsection ‹Range of an Array as List›  
function (sequential) lran :: "(int ⇒ 'a) ⇒ int ⇒ int ⇒ 'a list" where
  "lran a l h = (if l<h then a l # lran a (l+1) h else [])"
  by pat_completeness auto
termination 
  by (relation "measure (λ(_,l,h). nat (h-l))") auto
  
declare lran.simps[simp del]  
  
text ‹
  ‹lran a l h› is the list ‹[a⇩l,a⇩l⇩+⇩1,...,a⇩h⇩-⇩1]›
›

subsubsection ‹Auxiliary Lemmas›

lemma lran_empty[simp]: 
  "lran a l l = []"
  "lran a l h = [] ⟷ h≤l"
  by (subst lran.simps; auto)+

lemma lran_bwd_simp: "lran a l h = (if l<h then lran a l (h-1)@[a (h-1)] else [])"
  apply (induction a l h rule: lran.induct)
  apply (rewrite in "⌑ = _" lran.simps)
  apply (rewrite in "_ = ⌑" lran.simps)
  by (auto simp: less_le)
    
lemma length_lran[simp]: "length (lran a l h) = nat (h-l)"
  apply (induction a l h rule: lran.induct)
  apply (subst lran.simps)
  apply (auto)
  done

lemma nth_lran[simp]: "int i < h-l ⟹ lran a l h ! i = a (l + int i)"
  apply (induction a l h arbitrary: i rule: lran.induct)
  apply (subst lran.simps)
  apply (auto simp: nth_Cons nth_tl algebra_simps split: nat.splits)
  done

  
lemma lran_append1[simp]: "l≤h ⟹ lran a l (h + 1) = lran a l h @ [a h]"
  by (rewrite in "⌑ = _" lran_bwd_simp) auto

lemma lran_prepend1[simp]: "l≤h ⟹ lran a (l-1) h = a(l-1) # lran a l h"
  by (rewrite in "⌑ = _" lran.simps) auto
    
lemma lran_tail[simp]: "lran a (l+1) h = tl (lran a l h)"
  apply (rewrite in "_ = ⌑" lran.simps)
  apply auto
  done
    
lemma lran_butlast[simp]: "lran a l (h-1) = butlast (lran a l h)"
  apply (rewrite in "_ = ⌑" lran_bwd_simp)
  apply auto
  done
  
lemma hd_lran[simp]: "l<h ⟹ hd (lran a l h) = a l"  
  apply (subst lran.simps) by simp
  
lemma last_lran[simp]: "l<h ⟹ last (lran a l h) = a (h-1)"  
  apply (subst lran_bwd_simp) by simp
  

lemma lran_upd_outside[simp]:
  "i<l ⟹ lran (a(i:=x)) l h = lran a l h"
  "h≤i ⟹ lran (a(i:=x)) l h = lran a l h"
  subgoal
    apply (induction a l h rule: lran.induct)
    apply (rewrite in "⌑ = _" lran.simps)
    apply (rewrite in "_ = ⌑" lran.simps)
    by (auto)
  subgoal
    apply (induction a l h rule: lran.induct)
    apply (rewrite in "⌑ = _" lran.simps)
    apply (rewrite in "_ = ⌑" lran.simps)
    by (auto)
  done  

  
lemma lran_upd_inside: "i∈{l..<h} ⟹ lran (a(i:=x)) l h = (lran a l h)[nat (i-l) := x]"
  apply (rule nth_equalityI)
   apply (simp_all add: nth_list_update, linarith)
  done


lemma tl_upd_at0[simp]: "tl (xs[0:=x]) = tl xs" by (cases xs) auto 

    
  
  
lemma lran_eq_iff: "lran a l h = lran a' l h ⟷ (∀i. l≤i ∧ i<h ⟶ a i = a' i)"  
  apply (induction a l h rule: lran.induct)
  apply (rewrite in "⌑ = _" lran.simps)
  apply (rewrite in "_ = ⌑" lran.simps)
  apply auto
  by (metis antisym_conv not_less zless_imp_add1_zle)
  
lemma set_lran: "set (lran a l h) = a`{l..<h}"  
  apply (induction a l h rule: lran.induct)
  apply (rewrite in "⌑ = _" lran.simps)
  apply auto
  by (metis atLeastLessThan_iff image_iff not_less not_less_iff_gr_or_eq zless_imp_add1_zle)
  
lemma mset_lran: "mset (lran a l h) = mset_ran a {l..<h}"
  apply (induction a l h rule: lran.induct)
  apply (rewrite in "⌑ = _" lran.simps)
  by (auto simp: intvs_lower_incr mset_ran_insert)
  

end