Theory Refine_Hyperplane

theory
  Refine_Hyperplane
imports
  Autoref_Misc
  Affine_Arithmetic.Print
  Ordinary_Differential_Equations.Reachability_Analysis
  Refine_Vector_List
begin

lemma convex_halfspace[simp]:
  "convex (below_halfspace sctn)"
  apply (auto simp: below_halfspace_def le_halfspace_def[abs_def])
  using convex_bound_le
  apply (auto intro!: convexI simp: algebra_simps)
  by blast

subsection ‹Planes›

definition "shows_sctn (sctn::real list sctn) =
  shows ''Sctn '' o shows_paren (shows_words (normal sctn)) o shows_space o
    shows_paren (shows (pstn sctn))"

lemma halfspaces_union:
  "sbelow_halfspaces (a ∪ b) = sbelow_halfspaces a ∩ sbelow_halfspaces b"
  "below_halfspaces (a ∪ b) = below_halfspaces a ∩ below_halfspaces b"
  by (auto simp: halfspace_simps)

lemma plane_of_subset_halfspace: "plane_of sctn ⊆ below_halfspace sctn"
  by (auto simp: plane_of_def below_halfspace_def le_halfspace_def)

lemma halfspace_subsets: "sbelow_halfspaces sctns ⊆ below_halfspaces sctns"
  and halfspace_subset: "sbelow_halfspace sctn ⊆ below_halfspace sctn"
  by (force simp: plane_of_def halfspace_simps)+

lemma sbelow_halfspaces_insert:
  "sbelow_halfspaces (insert x2 stop_sctns) = sbelow_halfspace x2 ∩ sbelow_halfspaces stop_sctns"
  by (auto simp: sbelow_halfspaces_def)

lemma sbelow_halfspaces_antimono:
  assumes "A ⊆ B"
  shows "sbelow_halfspaces B ⊆ sbelow_halfspaces A"
  using assms
  by (auto simp: halfspace_simps)

lemma plane_in_halfspace[intro, simp]:
  "x ∈ plane_of sctn ⟹ x ∈ below_halfspace sctn"
  "x ∈ plane_of sctn ⟹ x ∈ above_halfspace sctn"
  by (auto simp: halfspace_simps plane_of_def)

lemma closure_shalfspace[intro, simp]:
  assumes "normal sctn ≠ 0"
  shows "closure (sbelow_halfspace sctn) = below_halfspace sctn"
    and "closure (sabove_halfspace sctn) = above_halfspace sctn"
  using closure_halfspace_lt[OF assms] closure_halfspace_gt[OF assms]
  by (auto simp: halfspace_simps inner_commute)

lemma closure_sbelow_halfspaces[intro, simp]:
  assumes "⋀sctn. sctn ∈ sctns ⟹ normal sctn ≠ 0"
  shows "closure (sbelow_halfspaces sctns) ⊆ below_halfspaces sctns"
proof -
  have *: "{closure S |S. S ∈ sbelow_halfspace ` sctns} = {S |S. S ∈ below_halfspace ` sctns}"
    by (auto simp: assms intro!: closure_shalfspace(1) [symmetric] exI)
  show ?thesis
    unfolding sbelow_halfspaces_def
    by (rule order_trans [OF closure_Int]) (auto simp: halfspace_simps * cong del: image_cong_simp)
qed

lemma halfspaces_empty[simp]: "sbelow_halfspaces {} = UNIV" "below_halfspaces {} = UNIV"
  by (auto simp: halfspace_simps)

lemma halfspaces_planeI:
  assumes "x ∈ below_halfspaces (s)"
  assumes "x ∉ ⋃(plane_of ` (s))"
  shows "x ∈ sbelow_halfspaces (s)"
  using assms
  by (force simp: halfspace_simps plane_of_def)


subsection ‹Section›

definition sctn_rel where sctn_rel_internal: "sctn_rel A = {(a, b). rel_sctn (in_rel A) a b}"
lemma sctn_rel_def: "⟨A⟩sctn_rel = {(a, b). rel_sctn (in_rel A) a b}"
  by (auto simp: sctn_rel_internal relAPP_def)

lemma single_valued_sctn_rel[relator_props]: "single_valued A ⟹ single_valued (⟨A⟩sctn_rel)"
  using sctn.right_unique_rel[of "in_rel A"]
  by (auto simp: single_valued_def right_unique_def sctn_rel_def)

consts i_sctn :: "interface ⇒ interface" ― ‹section datatype›

consts i_halfspace :: "interface ⇒ interface"

lemmas [autoref_rel_intf] = REL_INTFI[of sctn_rel i_sctn]


abbreviation "sctns_rel ≡ ⟨⟨lv_rel⟩sctn_rel⟩list_set_rel"

definition plane_rel_internal: "plane_rel A = ⟨A⟩sctn_rel O br plane_of top"
lemma plane_rel_def: "⟨A⟩plane_rel = ⟨A⟩sctn_rel O br plane_of top"
  by (simp add: plane_rel_internal relAPP_def)
consts i_plane::"interface⇒interface"
lemmas [autoref_rel_intf] = REL_INTFI[of plane_rel i_plane]

definition below_rel_internal: "below_rel A = ⟨A⟩sctn_rel O br below_halfspace top"
lemma below_rel_def: "⟨A⟩below_rel = ⟨A⟩sctn_rel O br below_halfspace top"
  by (simp add: below_rel_internal relAPP_def)
consts i_below::"interface⇒interface"
lemmas [autoref_rel_intf] = REL_INTFI[of below_rel i_below]

definition sbelow_rel_internal: "sbelow_rel A = ⟨A⟩sctn_rel O br sbelow_halfspace top"
lemma sbelow_rel_def: "⟨A⟩sbelow_rel = ⟨A⟩sctn_rel O br sbelow_halfspace top"
  by (simp add: sbelow_rel_internal relAPP_def)
consts i_sbelow::"interface⇒interface"
lemmas [autoref_rel_intf] = REL_INTFI[of sbelow_rel i_sbelow]

definition sbelows_rel_internal: "sbelows_rel A = ⟨⟨A⟩sctn_rel⟩list_set_rel O br sbelow_halfspaces top"
lemma sbelows_rel_def: "⟨A⟩sbelows_rel = ⟨⟨A⟩sctn_rel⟩list_set_rel O br sbelow_halfspaces top"
  by (simp add: sbelows_rel_internal relAPP_def)
consts i_sbelows::"interface⇒interface"
lemmas [autoref_rel_intf] = REL_INTFI[of sbelows_rel i_sbelows]

context includes autoref_syntax begin

lemma plane_of_autoref[autoref_rules]:
  "(λx. x, plane_of) ∈ ⟨A⟩sctn_rel → ⟨A⟩plane_rel"
  by (auto simp: plane_rel_def intro!: brI)

lemma below_halfspace_autoref[autoref_rules]:
  "(λx. x, below_halfspace) ∈ ⟨A⟩sctn_rel → ⟨A⟩below_rel"
  by (auto simp: below_rel_def intro!: brI)

lemma sbelow_halfspace_autoref[autoref_rules]:
  "(λx. x, sbelow_halfspace) ∈ ⟨A⟩sctn_rel → ⟨A⟩sbelow_rel"
  by (auto simp: sbelow_rel_def intro!: brI)

lemma sbelow_halfspaces_autoref[autoref_rules]:
  "(λx. x, sbelow_halfspaces) ∈ ⟨⟨A⟩sctn_rel⟩list_set_rel → ⟨A⟩sbelows_rel"
  by (auto simp: sbelows_rel_def intro!: brI)


end


context includes autoref_syntax begin
lemma [autoref_rules]:
  shows
  "(Sctn, Sctn) ∈ A → rnv_rel → ⟨A⟩sctn_rel"
  "(normal, normal) ∈ ⟨A⟩sctn_rel → A"
  "(pstn, pstn) ∈ ⟨A⟩sctn_rel → rnv_rel"
  by (auto simp: sctn_rel_def sctn.rel_sel)

lemma gen_eq_sctn[autoref_rules]:
  assumes "GEN_OP eq (=) (A → A → bool_rel)"
  shows "(λsctn1 sctn2. eq (normal sctn1) (normal sctn2) ∧ pstn sctn1 = pstn sctn2, (=)) ∈ ⟨A⟩sctn_rel → ⟨A⟩sctn_rel → bool_rel"
  apply safe
  subgoal for a b c d
    using assms
    by (cases a; cases b; cases c; cases d) (auto simp: sctn_rel_def dest: fun_relD)
  subgoal for a b c d
    using assms
    by (cases a; cases b; cases c; cases d) (auto simp: sctn_rel_def dest: fun_relD)
  subgoal for a b c d
    using assms
    by (cases a; cases b; cases c; cases d) (auto simp: sctn_rel_def dest: fun_relD)
  done

lemma inter_sctn_specs_inter_sctn_spec:
  "(inter_sctn_specs d, inter_sctn_spec::'a::executable_euclidean_space set⇒_) ∈ ⟨lv_rel⟩set_rel → ⟨lv_rel⟩sctn_rel → ⟨⟨lv_rel⟩set_rel⟩nres_rel"
  if "d = DIM('a)"
  apply (auto intro!: nres_relI RES_refine
      simp: inter_sctn_specs_def inter_sctn_spec_def set_rel_sv[OF lv_rel_sv] plane_ofs_def plane_of_def that)
  subgoal for a b c d e f
    apply (cases b; cases c)
    apply (rule ImageI, assumption)
    apply (auto simp: lv_rel_def br_def sctn_rel_def plane_of_def)
    apply (rule subsetD, assumption)
    apply auto
    subgoal for x1
      using lv_rel_inner[param_fo, OF lv_relI lv_relI, of f x1]
      by auto
    done
  subgoal for a b c d e f
    apply (cases b; cases c)
    apply (auto simp: sctn_rel_def lv_rel_def br_def)
    apply (drule rev_subsetD, assumption)
    subgoal for x1 x2
      using lv_rel_inner[where 'a = 'a, param_fo, OF lv_relI lv_relI, of f x1]
      by auto
    done
  by (auto simp: sctn_rel_def lv_rel_def br_def env_len_def)

lemma sctn_rel_comp: "⟨A⟩sctn_rel O ⟨B⟩sctn_rel = ⟨A O B⟩ sctn_rel"
  apply safe
  subgoal for a b c d e
    apply (cases c; cases d; cases d; cases e)
    by (auto simp: sctn_rel_def )
  subgoal for a b
    apply (cases a; cases b)
    apply (auto simp: sctn_rel_def )
    subgoal for c d e f
      apply (rule relcompI[where b="Sctn e c"])
       apply auto
      done
    done
  done

lemma sctn_rel: "⟨lv_rel⟩sctn_rel ⊆ ⟨⟨rnv_rel⟩list_rel⟩sctn_rel O ⟨lv_rel⟩sctn_rel"
  "⟨⟨rnv_rel⟩list_rel⟩sctn_rel O ⟨lv_rel⟩sctn_rel ⊆ ⟨lv_rel⟩sctn_rel"
  using sctn_rel_comp[of "⟨rnv_rel⟩list_rel" lv_rel] by auto

definition halfspace_rel_internal: "halfspaces_rel R = ⟨⟨R⟩sctn_rel⟩list_set_rel O br below_halfspaces top"
lemma halfspaces_rel_def: "⟨R⟩halfspaces_rel = ⟨⟨R⟩sctn_rel⟩list_set_rel O br below_halfspaces top"
  by (auto simp: relAPP_def halfspace_rel_internal)

lemmas [autoref_rel_intf] = REL_INTFI[of halfspaces_rel i_halfspace]

lemma below_halfspaces_autoref[autoref_rules]:
  "(λx. x, below_halfspaces) ∈ ⟨⟨R⟩sctn_rel⟩list_set_rel → ⟨R⟩halfspaces_rel"
  by (auto simp: halfspaces_rel_def br_def)

end

lemma plane_rel_br: "⟨br a I⟩plane_rel = br (plane_of o map_sctn a) (λx. I (normal x))"
  apply (auto simp: plane_rel_def sctn_rel_def br_def)
  subgoal for x y z by (cases x; cases y) auto
  subgoal for x y z by (cases x; cases y) auto
  subgoal for x y by (cases x; cases y) auto
  subgoal for a by (cases a; force)
  done


lemma closed_subset_plane[intro]:
  "closed b ⟹ closed {x ∈ b. x ∈ plane_of c}"
  "closed b ⟹ closed {x ∈ b. x ∙ n = d}"
  by (auto simp: plane_of_def intro!: closed_levelset_within continuous_intros)

end