Theory More_Sepref.WB_More_Refinement

theory WB_More_Refinement
  imports Weidenbach_Book_Base.WB_List_More
    "HOL-Library.Cardinality"
    "HOL-Eisbach.Eisbach"
    "HOL-Library.Rewrite"
    "Isabelle_LLVM.Refine_Monadic_Thin"
    ― ‹don't import ‹Refine_Monadic.Monadic›, that imports too much.›
    Isabelle_LLVM.Sepref_Rules
    Isabelle_LLVM.Sepref_Misc
    More_Refinement_Libs.WB_More_Refinement_Loops
    WB_More_Refinement_List
begin

no_notation funcset (infixr "→" 60)

chapter ‹More Theorems on Refinement›

text ‹

We first attempted to keep both the LLVM and the SML version
working. Due to where things are defined, some constants have to be
duplicated (including simple ones like swap or critical ones like
fref -- although none of them should be in IICF).

We finally give up (at least temporary) when we realised that the LLVM
version is twice as fast as the SML version while providing better
tooling than the SML version. However, some things remains in the
theories from this attempt like fref defined below.

Additionaly some of the things developed here moved to Isabelle\_LLVM.
›

hide_const Autoref_Fix_Rel.CONSTRAINT

section ‹Some Tooling for Refinement›

text ‹
  The following very simple tactics remove duplicate variables generated by some tactic like
  ‹refine_rcg›. For example, if the problem contains \<^term>‹(i, C) = (xa, xb)›, then only
  \<^term>‹i› and \<^term>‹C› will remain. It can also prove trivial goals where the goals already
  appears in the assumptions.
  ›

method remove_dummy_vars uses simps =
  ((unfold prod.inject)?; (simp only: prod.inject)?; (elim conjE)?;
    hypsubst?; (simp only: triv_forall_equality simps)?)


subsection ‹From @{text →} to @{text ⇓}›


ML ‹
signature MORE_REFINEMENT = sig
  val down_converse: Proof.context -> thm -> thm
end

structure More_Refinement: MORE_REFINEMENT = struct
  val unfold_refine = (fn context => Local_Defs.unfold (context)
   @{thms refine_rel_defs nres_rel_def in_pair_collect_simp})
  val unfold_Ball = (fn context => Local_Defs.unfold (context)
    @{thms Ball2_split_def all_to_meta})
  val replace_ALL_by_meta = (fn context => fn thm => Object_Logic.rulify context thm)
  val down_converse = (fn context =>
    replace_ALL_by_meta context o (unfold_Ball context) o (unfold_refine context))
end
›

attribute_setup "to_⇓" = ‹
    Scan.succeed (Thm.rule_attribute [] (More_Refinement.down_converse o Context.proof_of))
  › "convert theorem from @{text →}-form to @{text ⇓}-form."

method "to_⇓" =
   (unfold refine_rel_defs nres_rel_def in_pair_collect_simp;
   unfold Ball2_split_def all_to_meta;
   intro allI impI)

lemma fref_syn_invert:
  ‹a = a' ⟹ b ⊆ b' ⟹ a →⇩f b ⊆ a' →⇩f b'›
  unfolding fref_param1[symmetric]
  by (rule fun_rel_syn_invert)

method match_spec =
  (match conclusion in ‹(f, g) ∈ R› for f g R ⇒
    ‹print_term f; match premises in I[thin]: ‹(f, g) ∈ R'› for R'
       ⇒ ‹print_term R'; rule mem_set_trans[OF _ I]››)

method match_fun_rel =
  ((match conclusion in
       ‹fun_rel_syn _  _ ⊆ _ → _› ⇒ ‹rule fun_rel_mono›
     ¦ ‹_ →⇩f _ ⊆ _ →⇩f _› ⇒ ‹rule fref_syn_invert›
     ¦ ‹⟨_⟩nres_rel ⊆ ⟨_⟩nres_rel› ⇒ ‹rule nres_rel_mono›
     ¦ ‹[_]⇩f _ → _ ⊆ [_]⇩f _ → _› ⇒ ‹rule fref_mono›
   )+)


section ‹More Theorems for Refinement›


lemma fref_weaken_pre_weaken:
  assumes "⋀x. P x ⟶ P' x"
  assumes "(f,h) ∈ frefnd P' R S"
  assumes ‹S ⊆ S'›
  shows "(f,h) ∈ frefnd P R S'"
  using assms unfolding fref_def by blast

lemma fref_to_Down:
  ‹(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 fref_to_Down_curry_left:
  fixes f:: ‹'a ⇒ 'b ⇒ 'c nres› and
    A::‹(('a × 'b) × 'd) set›
  shows
    ‹(uncurry f, g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
      (⋀a b x'. P x' ⟹ ((a, b), x') ∈ A ⟹ f a b ≤ ⇓ B (g x'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

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

lemma fref_to_Down_Id_keep:
  assumes ‹(f, RETURN o g) ∈ [P]⇩f A → ⟨Id⟩nres_rel›
  shows ‹(⋀x x'. P x' ⟹ (x, x') ∈ A ⟹ f x ≤ ⇓ {(x, y). x = y ∧ x = g x'} (RETURN (g x')))›
  using assms
  unfolding fref_def uncurry_def nres_rel_def RETURN_def conc_fun_RES
  by auto

text ‹This has been moved to theory ‹Isabelle_LLVM.Sepref_Misc›. However, we cannot import it here
  due to ‹Refine_Imperative_HOL.Sepref_Misc›. Therefore, we mark the abbreviations as input only
  and hope for the best.›


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_curry2':
  ‹(uncurry2 f, uncurry2 g) ∈ A →⇩f ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z 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_curry3:
  ‹(uncurry3 f, uncurry3 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z' a a'. P (((x', y'), z'), a') ⟹
        ((((x, y), z), a), (((x', y'), z'), a')) ∈ A ⟹
         f x y z a ≤ ⇓ B (g x' y' z' a'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

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

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

lemma fref_to_Down_curry6:
  ‹(uncurry6 f, uncurry6 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z' a a' b b' c c' d d'. P ((((((x', y'), z'), a'), b'), c'), d') ⟹
        (((((((x, y), z), a), b), c), d), ((((((x', y'), z'), a'), b'), c'), d')) ∈ A ⟹
         f x y z a b c d ≤ ⇓ B (g x' y' z' a' b' c' d'))›
  unfolding fref_def uncurry_def nres_rel_def by auto

lemma fref_to_Down_curry7:
  ‹(uncurry7 f, uncurry7 g) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z' a a' b b' c c' d d' e e'. P (((((((x', y'), z'), a'), b'), c'), d'), e') ⟹
       ((((((((x, y), z), a), b), c), d), e), (((((((x', y'), z'), a'), b'), c'), d'), e')) ∈ A ⟹
         f x y z a b c d e ≤ ⇓ B (g x' y' z' a' b' c' d' e'))›
  unfolding fref_def uncurry_def nres_rel_def by auto

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

lemma fref_to_Down_unRET_uncurry2:
  fixes f :: ‹'a ⇒ 'b ⇒ 'c ⇒ 'f›
    and g :: ‹'a2 ⇒ 'b2 ⇒ 'c2 ⇒ 'g›
  shows
    ‹(uncurry2 (RETURN ooo f), uncurry2 (RETURN ooo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
       (⋀(x :: 'a) x' y y' (z :: 'c) (z' :: 'c2).
         P ((x', y'), z') ⟹ (((x, y), z), ((x', y'), z')) ∈ A ⟹
         (f x y z, g x' y' z') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_unRET_uncurry3:
  shows
    ‹(uncurry3 (RETURN oooo f), uncurry3 (RETURN oooo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
       (⋀(x :: 'a) x' y y' (z :: 'c) (z' :: 'c2) a a'.
         P (((x', y'), z'), a') ⟹ ((((x, y), z), a), (((x', y'), z'), a')) ∈ A ⟹
         (f x y z a, g x' y' z' a') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_unRET_uncurry4:
  shows
    ‹(uncurry4 (RETURN ooooo f), uncurry4 (RETURN ooooo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
       (⋀(x :: 'a) x' y y' (z :: 'c) (z' :: 'c2) a a' b b'.
         P ((((x', y'), z'), a'), b') ⟹ (((((x, y), z), a), b), ((((x', y'), z'), a'), b')) ∈ A ⟹
         (f x y z a b, g x' y' z' a' b') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto


lemma fref_to_Down_curry_no_nres_Id:
  ‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]⇩f A → ⟨Id⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ f x y = g x' y')›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

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

lemma fref_to_Down_curry_no_nres:
  ‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ (f x y, g x' y') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma RES_RETURN_RES4:
   ‹SPEC Φ ⤜ (λ(T, T', T'', T'''). RETURN (f T T' T'' T''')) =
      RES ((λ(a, b, c, d). f a b c d) ` {T. Φ T})›
  using RES_RETURN_RES[of ‹Collect Φ› ‹λ(a, b, c, d). f a b c d›]
  apply (subst (asm)(2) split_prod_bound)
  apply (subst (asm)(3) split_prod_bound)
  apply (subst (asm)(4) split_prod_bound)
  by auto

declare RETURN_as_SPEC_refine[refine2 del]


lemma fref_to_Down_unRET_uncurry_Id:
  ‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]⇩f A → ⟨Id⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ f x y = (g x' y'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto
lemma fref_to_Down_unRET_uncurry:
  ‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]⇩f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ (f x y, g x' y') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_unRET_Id:
  ‹((RETURN o f), (RETURN o g)) ∈ [P]⇩f A → ⟨Id⟩nres_rel ⟹
     (⋀x x'. P x' ⟹ (x, x') ∈ A ⟹ f x = (g x'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

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


thm in_pair_collect_simp


section ‹More declarations›

(* TODO: only input notation? *)
notation prod_rel_syn (infixl "×⇩f" 70)


section ‹More Functions, Relations, and Theorems›

definition emptied_list :: ‹'a list ⇒ 'a list› where
  ‹emptied_list l = []›



subsection ‹Ghost parameters›

text ‹
  This is a trick to recover from consumption of a variable (\<^term>‹𝒜⇩i⇩n›) that is passed as
  argument and destroyed by the initialisation: We copy it as a zero-cost
  (by creating a \<^term>‹()›), because we don't need it in the code and only in the specification.

  This is a way to have ghost parameters, without having them: The parameter is replaced by \<^term>‹()›
  and we hope that the compiler will do the right thing.
›
definition virtual_copy where
  [simp]: ‹virtual_copy = id›

definition virtual_copy_rel where
  ‹virtual_copy_rel = {(c, b). c = ()}›

lemma refine_add_inv:
  fixes f :: ‹'a ⇒ 'a nres› and f' :: ‹'b ⇒ 'b nres› and h :: ‹'b ⇒ 'a›
  assumes
    ‹(f', f) ∈ {(S, S'). S' = h S ∧ R S} → ⟨{(T, T'). T' = h T ∧ P' T}⟩ nres_rel›
    (is ‹_ ∈ ?R → ⟨{(T, T'). ?H T T' ∧ P' T}⟩ nres_rel›)
  assumes
    ‹⋀S. R S ⟹ f (h S) ≤ SPEC (λT. Q T)›
  shows
    ‹(f', f) ∈ ?R → ⟨{(T, T'). ?H T T' ∧ P' T ∧ Q (h T)}⟩ nres_rel›
  using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
  by fastforce

lemma refine_add_inv_generalised:
  fixes f :: ‹'a ⇒ 'b nres› and f' :: ‹'c ⇒ 'd nres›
  assumes
    ‹(f', f) ∈ A →⇩f ⟨B⟩ nres_rel›
  assumes
    ‹⋀S S'. (S, S') ∈ A ⟹ f S' ≤ RES C›
  shows
    ‹(f', f) ∈ A →⇩f ⟨{(T, T'). (T, T') ∈ B ∧ T' ∈ C}⟩ nres_rel›
  using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
   fref_param1[symmetric]
  by fastforce

lemma refine_add_inv_pair:
  fixes f :: ‹'a ⇒ ('c × 'a) nres› and f' :: ‹'b ⇒ ('c × 'b) nres› and h :: ‹'b ⇒ 'a›
  assumes
    ‹(f', f) ∈ {(S, S'). S' = h S ∧ R S} → ⟨{(S, S'). (fst S' = h' (fst S) ∧
    snd S' = h (snd S)) ∧ P' S}⟩ nres_rel›  (is ‹_ ∈ ?R → ⟨{(S, S'). ?H S S' ∧ P' S}⟩ nres_rel›)
  assumes
    ‹⋀S. R S ⟹ f (h S) ≤ SPEC (λT. Q (snd T))›
  shows
    ‹(f', f) ∈ ?R → ⟨{(S, S'). ?H S S' ∧ P' S ∧ Q (h (snd S))}⟩ nres_rel›
  using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
  by fastforce

lemma refine_itself0:
    ‹(X, X) ∈ Id →⇩f ⟨Id⟩nres_rel› and
  refine_itself1:
    ‹(uncurry X1, uncurry X1) ∈ Id ×⇩f Id →⇩f ⟨Id⟩nres_rel› and
  refine_itself2:
    ‹(uncurry2 X2, uncurry2 X2) ∈ Id ×⇩f Id ×⇩f Id →⇩f ⟨Id⟩nres_rel› and
  refine_itself3:
    ‹(uncurry3 X3, uncurry3 X3) ∈ Id ×⇩f Id ×⇩f Id ×⇩f Id →⇩f ⟨Id⟩nres_rel›and
  refine_itself4:
    ‹(uncurry4 X4, uncurry4 X4) ∈ Id ×⇩f Id ×⇩f Id ×⇩f Id ×⇩f Id →⇩f ⟨Id⟩nres_rel›
  by (intro frefI nres_relI; auto; fail)+

lemma fref_to_Down_unRET_Id_uncurry:
  ‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]⇩f A → ⟨Id⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ f x y = (g x' y'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma (in -) nofail_ASSERT_bind: ‹nofail (do {ASSERT(P); (Φ :: 'a nres)}) ⟷ P ∧ nofail Φ›
  by (auto simp: nofail_def ASSERT_eq iASSERT_def)


lemma RES_RES11_RETURN_RES:
   ‹RES A ⤜ (λ(a, b, c, d, e, g, h, i, j, k, l). RES (f a b c d e g h i j k l)) =
   RES (⋃((λ(a, b, c, d, e, g, h, i, j, k, l). f a b c d e g h i j k l) ` A))›
  by (auto simp:  pw_eq_iff refine_pw_simps uncurry_def Bex_def
    split: prod.splits)

lemma RES_RES13_RETURN_RES_bound:
   ‹RES A ⤜ (λ(a, b, c, d, e, g, h, i, j, k, l, m, n). RES (f a b c d e g h i j k l m n)) =
   RES (⋃((λ(a, b, c, d, e, g, h, i, j, k, l, m, n). f a b c d e g h i j k l m n) ` A))›
  by (auto simp:  pw_eq_iff refine_pw_simps uncurry_def Bex_def
    split: prod.splits)

lemma ref_two_step'': ‹R ⊆ R' ⟹ A ≤ B ⟹ ⇓ R A ≤  ⇓ R' B›
  by (simp add: "weaken_⇓" ref_two_step')

lemma RES_RETURN_RES3':
  ‹RES Φ ⤜ (λ(T, T', T''). RETURN (f T T' T'')) = RES ((λ(a, b, c). f a b c) ` Φ)›
  apply (subst RES_SPEC_conv)
  apply (subst RES_RETURN_RES3)
  by auto

lemma RETURN_le_RES_no_return3:
  ‹f ≤ SPEC (λ(S,T,U). g S T U ∈ Φ) ⟹ do {(S, T, U) ← f; RETURN (g S T U)} ≤ RES Φ›
  by (cases f)
   (auto simp: RES_RETURN_RES3')

lemma RES_RETURN_RES4':
  ‹RES Φ ⤜ (λ(T, T', T'', T'''). RETURN (f T T' T'' T''')) = RES ((λ(a, b, c, d). f a b c d) ` Φ)›
  apply (subst RES_SPEC_conv)
  apply (subst RES_RETURN_RES4)
  by auto

lemma RETURN_le_RES_no_return4:
  ‹f ≤ SPEC (λ(S,T,U,V). g S T U V ∈ Φ) ⟹ do {(S, T, U, V) ← f; RETURN (g S T U V)} ≤ RES Φ›
  by (cases f)
    (auto simp: RES_RETURN_RES4')

lemma RES_RETURN_RES5':
  ‹RES Φ ⤜ (λ(T, T', T'', T''', T''''). RETURN (f T T' T'' T''' T'''')) =
    RES ((λ(a, b, c, d, e). f a b c d e) ` Φ)›
  apply (subst RES_SPEC_conv)
  apply (subst RES_RETURN_RES5)
  by auto

lemma RETURN_le_RES_no_return5:
  ‹f ≤ SPEC (λ(S,T,U,V, W). g S T U V W ∈ Φ) ⟹ do {(S, T, U, V, W) ← f; RETURN (g S T U V W)} ≤ RES Φ›
  by (cases f)
    (auto simp: RES_RETURN_RES5')

end