Theory Enclosure_Operations

theory Enclosure_Operations
imports
  Autoref_Misc
  Affine_Arithmetic.Print
  Ordinary_Differential_Equations.Reachability_Analysis
begin

section ‹interfaces›

consts i_appr :: interface ― ‹reachable set›

section ‹Operations on Enclosures (Sets)›

definition [refine_vcg_def]: "split_spec X = SPEC (λ(A, B). X ⊆ A ∪ B)"

definition [refine_vcg_def]: "split_spec_param (n::nat) X = SPEC (λ(A, B). X ⊆ A ∪ B)"
definition [refine_vcg_def]: "split_spec_params d n X = SPEC (λ(A, B). env_len A d ∧ env_len B d ∧ X ⊆ A ∪ B)"

definition [refine_vcg_def]: "split_spec_exact x = SPEC (λ(a, b). x = a ∪ b)"

definition [refine_vcg_def]: "Inf_specs d X = SPEC (λr::real list. length r = d ∧ (∀x ∈ X. list_all2 (≤) r x))"
definition [refine_vcg_def]: "Inf_spec X = SPEC (λr. ∀x ∈ X. r ≤ x)"

definition [refine_vcg_def]: "Sup_specs d X = SPEC (λr::real list. length r = d ∧ (∀x ∈ X. list_all2 (≤) x r))"
definition [refine_vcg_def]: "Sup_spec X = SPEC (λr. ∀x ∈ X. x ≤ r)"

definition [refine_vcg_def]: "Inf_inners X y = SPEC (λr::real. (∀x ∈ X. r ≤ inner_lv_rel x y))" ― ‹TODO: generic image of aforms, then Inf›
definition [refine_vcg_def]: "Inf_inner X y = SPEC (λr. ∀x ∈ X. r ≤ x ∙ y)" ― ‹TODO: generic image of aforms, then Inf›

definition [refine_vcg_def]: "Sup_inners X y = SPEC (λr::real. (∀x ∈ X. r ≥ inner_lv_rel x y))" ― ‹TODO: generic image of aforms, then Inf›
definition [refine_vcg_def]: "Sup_inner X y = SPEC (λr. ∀x ∈ X. x ∙ y ≤ r)" ― ‹TODO: generic image of aforms. then Sup›

definition "plane_ofs sctn = {x. inner_lv_rel x (normal sctn) = pstn sctn}"
definition [refine_vcg_def]: "inter_sctn_specs d X sctn = SPEC (λR. env_len R d ∧ X ∩ plane_ofs sctn ⊆ R ∧ R ⊆ plane_ofs sctn)"
definition [refine_vcg_def]: "inter_sctn_spec X sctn = SPEC (λR. X ∩ plane_of sctn ⊆ R ∧ R ⊆ plane_of sctn)"

definition [refine_vcg_def]: "intersects_spec X sctn = SPEC (λb. b ∨ X ∩ plane_of sctn = {})"

definition [refine_vcg_def]: "intersects_sctns_spec X sctns = SPEC (λb. b ∨ X ∩ ⋃(plane_of ` sctns) = {})"

definition [refine_vcg_def]: "reduce_spec (reach_options_o::unit) X = SPEC (λR. X ⊆ R)"
definition [refine_vcg_def]: "reduce_specs d (reach_options_o::unit) X = SPEC (λR. env_len R d ∧ X ⊆ R)"

definition [refine_vcg_def]: "width_spec X = SPEC (top::real⇒_)"

definition [refine_vcg_def]: "ivl_rep_of_set X = SPEC (λ(i, s). i ≤ s ∧ X ⊆ {i .. s})"

definition "strongest_direction T =
  (let
    b = fold (λb' b. if abs (T ∙ b') ≥ abs (T ∙ b) then b' else b) (Basis_list::'a::executable_euclidean_space list) 0
  in
    (sgn (T ∙ b) *⇩R b, abs (T ∙ b)))"

subsection ‹subset approximation›

definition[refine_vcg_def]:  "subset_spec X Y = SPEC (λb. b ⟶ X ⊆ Y)"

definition [refine_vcg_def]: "above_sctn X sctn = SPEC (λb. b ⟶ (X ⊆ sabove_halfspace sctn))"

lemma above_sctn_nres: "do { ii ← Inf_inner X (normal sctn); RETURN (ii > pstn sctn)} ≤ above_sctn X sctn"
  by (auto simp: above_sctn_def Inf_inner_def sabove_halfspace_def gt_halfspace_def intro!: refine_vcg)

definition [refine_vcg_def]: "below_sctn X sctn = SPEC (λb. b ⟶ (X ⊆ below_halfspace sctn))"

lemma below_sctn_nres:
  "do { si ← Sup_inner X (normal sctn); RETURN (si ≤ pstn sctn)} ≤ below_sctn X sctn"
  by (auto simp: below_sctn_def Sup_inner_def below_halfspace_def le_halfspace_def intro!: refine_vcg)

definition [refine_vcg_def]: "sbelow_sctn X sctn = SPEC (λb. b ⟶ (X ⊆ sbelow_halfspace sctn))"

lemma sbelow_sctn_nres:
  "do { si ← Sup_inner X (normal sctn); RETURN (si < pstn sctn)} ≤ sbelow_sctn X sctn"
  by (auto simp: sbelow_sctn_def Sup_inner_def sbelow_halfspace_def lt_halfspace_def intro!: refine_vcg)

definition [refine_vcg_def]: "sbelow_sctns X sctn = SPEC (λb. b ⟶ (X ⊆ sbelow_halfspaces sctn))"

lemma sbelow_sctns_nres:
  assumes "finite sctns"
  shows "FOREACH⇗(λit b. b ⟶ (∀sctn ∈ sctns - it. X ⊆ sbelow_halfspace sctn))⇖ sctns  (λsctn b.
    do {
      b' ← sbelow_sctn X sctn;
      RETURN (b' ∧ b)}) True ≤ sbelow_sctns X sctns"
  unfolding sbelow_sctns_def
  by (refine_vcg assms) (auto simp: sbelow_halfspaces_def)


definition [refine_vcg_def]: "disjoint_sets X Y = SPEC (λb. b ⟶ X ∩ Y = {})"


section ‹Dependencies (Set of vectors)›

subsection ‹singleton projection›

definition [refine_vcg_def]: "nth_image_precond X n ⟷ X ≠ {} ∧ (∀xs∈X. n < length xs ∧ env_len X (length xs))"

definition [refine_vcg_def]: "nth_image X n = SPEC (λR. nth_image_precond X n ∧ (R = (λx. x ! n) ` X))"


subsection ‹projection›

definition "project_env_precond env is ≡ (∀i ∈ set is. ∀xs∈env. i < length xs ∧ env_len env (length xs))"

definition project_env where [refine_vcg_def]:
  "project_env env is = SPEC (λR. project_env_precond env is ∧ env_len R (length is) ∧ (λxs. map (λi. xs ! i) is) ` env ⊆ R)"

subsection ‹expressions›

definition approx_slp_spec::"floatarith list ⇒ nat ⇒ slp ⇒ real list set ⇒ real list set option nres"
  where [refine_vcg_def]: "approx_slp_spec fas l slp env =
    (ASSERT (slp_of_fas fas = slp ∧ length fas = l)) ⤜
    (λ_. SPEC (λR. case R of Some R ⇒ ∃e. env_len env e ∧ env_len R l ∧
        (∀e∈env. interpret_floatariths fas e ∈ R) | None ⇒ True))"

definition approx_form_spec::"form ⇒ real list set ⇒ bool nres"
where "approx_form_spec ea E = SPEC (λr. r ⟶ (∀e∈E. interpret_form ea e))"

definition isFDERIV_spec
  :: "nat ⇒ nat list ⇒ floatarith list ⇒ real list set ⇒ bool nres"
  where "isFDERIV_spec N xs fas VS = SPEC (λr. r ⟶ (∀vs ∈ VS. isFDERIV N xs fas vs))"

subsection ‹singleton environment›

definition sings_spec where [refine_vcg_def]:
  "sings_spec X = SPEC (λenv. env_len env 1 ∧ X ≠ {} ∧ (env = (λx. [x]) ` X))"

definition [refine_vcg_def]: "project_set X b y = SPEC (λivl. X ∩ {x. x ∙ b = y} ⊆ ivl ∧ ivl ⊆ {x. x ∙ b = y})"

definition [refine_vcg_def]: "sets_of_coll X = SPEC (λXS. X = ⋃XS)"

definition [simp]: "is_empty ≡ λx. x = {}"
lemma [autoref_itype]: "is_empty ::⇩i A →⇩i i_bool"
  by simp

definition [refine_vcg_def]: "project_sets X b y = SPEC (λivl. X ∩ {x. x ∙ b = y} ⊆ ivl ∧ ivl ⊆ {x. x ∙ b = y})"

definition [refine_vcg_def]: "restrict_to_halfspaces sctns X = SPEC (λR. R = X ∩ below_halfspaces sctns)"

end