Theory SymmetricR2Shapes

theory SymmetricR2Shapes
  imports Green
begin 

context R2
begin

lemma valid_path_valid_swap:
  assumes "valid_path (λx::real. ((f x)::real, (g x)::real))"
  shows "valid_path (prod.swap o (λx. (f x, g x)))"
  unfolding o_def valid_path_def piecewise_C1_differentiable_on_def swap_simp
proof (intro conjI)
  show "continuous_on {0..1} (λx. (g x, f x))"
    using assms
    using continuous_on_Pair continuous_on_componentwise[where f = "(λx. (f x, g x))"]
    by (auto simp add: real_pair_basis valid_path_def piecewise_C1_differentiable_on_def)
  show "∃S. finite S ∧ (λx. (g x, f x)) C1_differentiable_on {0..1} - S"
  proof -
    obtain S where "finite S" and S: "(λx. (f x, g x)) C1_differentiable_on {0..1} - S"
      using assms
      by (auto simp add: real_pair_basis valid_path_def piecewise_C1_differentiable_on_def)
    have 0: "f C1_differentiable_on {0..1} - S" using S assms
      using C1_diff_components_2[of "(1,0)" "(λx. (f x, g x))"] 
      by (auto simp add: real_pair_basis algebra_simps)
    have 1: "g C1_differentiable_on {0..1} - S" using S assms
      using C1_diff_components_2 [of "(0,1)", OF _ S] real_pair_basis by fastforce
    have *: "(λx. (g x, f x)) C1_differentiable_on {0..1} - S"
      using 0 1 C1_differentiable_on_components[where f = "(λx. (g x, f x))"]
      by (auto simp add: real_pair_basis valid_path_def piecewise_C1_differentiable_on_def)
    then show ?thesis using ‹finite S› by auto
  qed
qed

lemma pair_fun_components: "C = (λx. (C x ∙ i, C x ∙ j))"
  by (simp add: i_is_x_axis inner_Pair_0 j_is_y_axis)

lemma swap_pair_fun: "(λy. prod.swap (C (y, 0))) =  (λx. (C (x, 0) ∙ j, C (x, 0) ∙ i))"
  by (simp add: prod.swap_def i_is_x_axis inner_Pair_0 j_is_y_axis)

lemma swap_pair_fun': "(λy. prod.swap (C (y, 1))) =  (λx. (C (x, 1) ∙ j, C (x, 1) ∙ i))"
  by (simp add: prod.swap_def i_is_x_axis inner_Pair_0 j_is_y_axis)

lemma swap_pair_fun'': "(λy. prod.swap (C (0, y))) =  (λx. (C (0,x) ∙ j, C (0,x) ∙ i))"
  by (simp add: prod.swap_def i_is_x_axis inner_Pair_0 j_is_y_axis)

lemma swap_pair_fun''': "(λy. prod.swap (C (1, y))) =  (λx. (C (1,x) ∙ j, C (1,x) ∙ i))"
  by (simp add: prod.swap_def i_is_x_axis inner_Pair_0 j_is_y_axis)

lemma swap_valid_boundaries:
  assumes "∀(k,γ)∈boundary C. valid_path γ"
  assumes "(k,γ)∈boundary (prod.swap o C o prod.swap)"
  shows "valid_path γ"
  using assms
    valid_path_valid_swap[of "λx. (λx. C (x, 0)) x ∙ i" "λx. (λx. C (x, 0)) x ∙ j"] pair_fun_components[of "(λx. C (x, 0))"]
    pair_fun_components[of "(λy. C (y, 0))"]           
    valid_path_valid_swap[of "λx. (λy. C (y, 1)) x ∙ i" "λx. (λy. C (y, 1)) x ∙ j"] pair_fun_components[of "(λy. C (y, 1))"]
    pair_fun_components[of "(λx. C (x, 1))"]           
    valid_path_valid_swap[of "λx. (λy. C (1,y)) x ∙ i" "λx. (λy. C (1,y)) x ∙ j"] pair_fun_components[of "(λy. C (1,y))"]
    pair_fun_components[of "(λx. C (1,x))"]           
    valid_path_valid_swap[of "λx. (λy. C (0,y)) x ∙ i" "λx. (λy. C (0,y)) x ∙ j"] pair_fun_components[of "(λy. C (0,y))"]
    pair_fun_components[of "(λx. C (0,x))"]           
  by (auto simp add: boundary_def horizontal_boundary_def vertical_boundary_def
       o_def real_pair_basis swap_pair_fun swap_pair_fun' swap_pair_fun'' swap_pair_fun''')

lemma prod_comp_eq: 
  assumes "f = prod.swap o g"
  shows "prod.swap o f  = g"
  using swap_comp_swap assms
  by fastforce

lemma swap_typeI_is_typeII:
  assumes "typeI_twoCube C"
  shows "typeII_twoCube (prod.swap o C o prod.swap)"
proof (simp add: typeI_twoCube_def typeII_twoCube_def)
  obtain a b g1 g2 where C: " a < b "
    "(∀x∈{a..b}. g2 x ≤ g1 x) "
    "cubeImage C = {(x, y). x ∈ {a..b} ∧ y ∈ {g2 x..g1 x}} "
    "C = (λ(x, y). ((1 - x) * a + x * b, (1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b))) "
    "g1 piecewise_C1_differentiable_on {a..b} "
    "g2 piecewise_C1_differentiable_on {a..b}"
    using typeI_cube_explicit_spec[OF assms]
    by blast
  show "∃a b. a < b ∧
              (∃g1 g2. (∀x∈{a..b}. g2 x ≤ g1 x) ∧
                  prod.swap ∘ C ∘ prod.swap =
                  (λ(y, x). ((1 - y) * g2 ((1 - x) * a + x * b) + y * g1 ((1 - x) * a + x * b), (1 - x) * a + x * b)) ∧
                  g1 piecewise_C1_differentiable_on {a..b} ∧ g2 piecewise_C1_differentiable_on {a..b})"
    using C by (fastforce simp add: prod.swap_def o_def)
qed

lemma valid_cube_valid_swap:
  assumes "valid_two_cube C"
  shows "valid_two_cube (prod.swap o C o prod.swap)"
  using assms unfolding valid_two_cube_def boundary_def horizontal_boundary_def vertical_boundary_def
  apply (auto simp: card_insert_if  split: if_split_asm)
   apply (metis swap_swap)+
  done

lemma twoChainVertDiv_of_itself:
  assumes "finite C"
    "∀(k, γ)∈(two_chain_boundary C). valid_path γ"
  shows "only_vertical_division (two_chain_boundary C) C"
proof(clarsimp simp add: only_vertical_division_def)
  show "∃𝒱 ℋ. finite ℋ ∧ finite 𝒱 ∧
              (∀x∈𝒱. case x of (k, γ) ⇒ ∃x∈two_chain_vertical_boundary C. case x of (k', γ') ⇒ ∃a∈{0..1}. ∃b∈{0..1}. a ≤ b ∧ subpath a b γ' = γ) ∧
              (common_sudiv_exists (two_chain_horizontal_boundary C) ℋ ∨
               common_reparam_exists ℋ (two_chain_horizontal_boundary C)) ∧
              boundary_chain ℋ ∧ two_chain_boundary C = 𝒱 ∪ ℋ ∧ (∀(k,γ)∈ℋ. valid_path γ)"
  proof (intro exI)
    let ?ℋ = "two_chain_horizontal_boundary C"
    have 0: "∀(k,γ)∈?ℋ. valid_path γ" using assms(2)
      by (auto simp add: two_chain_horizontal_boundary_def two_chain_boundary_def boundary_def)
    have "⋀a b. (a, b) ∈ two_chain_vertical_boundary C ⟹
                  ∃x∈two_chain_vertical_boundary C. case x of (k', γ') ⇒ ∃a∈{0..1}. ∃c∈{0..1}. a ≤ c ∧ subpath a c γ' = b"
      by (metis (mono_tags, lifting) atLeastAtMost_iff case_prod_conv le_numeral_extra(1) order_refl subpath_trivial)
    moreover have "common_sudiv_exists ?ℋ ?ℋ"
      using gen_common_boundary_subdiv_exists_refl_twochain_boundary[OF 0 two_chain_horizontal_boundary_is_boundary_chain]
      by auto
    moreover have "boundary_chain ?ℋ"
      using two_chain_horizontal_boundary_is_boundary_chain by auto
    moreover have "⋀a b. (a, b) ∈ two_chain_boundary C ⟹ (a, b) ∉ ?ℋ ⟹ (a, b) ∈ two_chain_vertical_boundary C"
      by (auto simp add: two_chain_boundary_def two_chain_horizontal_boundary_def two_chain_vertical_boundary_def boundary_def)
    moreover have "⋀a b. (a, b) ∈ two_chain_vertical_boundary C ⟹ (a, b) ∈ two_chain_boundary C"
      "⋀a b. (a, b) ∈ ?ℋ ⟹ (a, b) ∈ two_chain_boundary C"
      by (auto simp add: two_chain_boundary_def two_chain_horizontal_boundary_def two_chain_vertical_boundary_def boundary_def)
    moreover have "⋀a b. (a, b) ∈ ?ℋ ⟹ valid_path b"
      using 0 by blast 
    ultimately show "finite ?ℋ ∧
           finite (two_chain_vertical_boundary C) ∧
           (∀x∈two_chain_vertical_boundary C.
               case x of (k, γ) ⇒ ∃x∈two_chain_vertical_boundary C. case x of (k', γ') ⇒ ∃a∈{0..1}. ∃b∈{0..1}. a ≤ b ∧ subpath a b γ' = γ) ∧
           (common_sudiv_exists ?ℋ ?ℋ ∨
            common_reparam_exists ?ℋ ?ℋ) ∧
           boundary_chain ?ℋ ∧ two_chain_boundary C = two_chain_vertical_boundary C ∪ ?ℋ ∧ (∀(k,γ)∈?ℋ. valid_path γ)"
      by (auto simp add: finite_two_chain_horizontal_boundary[OF assms(1)] finite_two_chain_vertical_boundary[OF assms(1)])
  qed
qed


end

definition x_coord where "x_coord ≡ (λt::real. t - 1/2)"

lemma x_coord_smooth: "x_coord C1_differentiable_on {a..b}"
  by (simp add: x_coord_def)

lemma x_coord_bounds:
  assumes "(0::real) ≤ x" "x ≤ 1"
  shows "-1/2 ≤ x_coord x ∧ x_coord x ≤ 1/2"
  using assms by(auto simp add: x_coord_def)

lemma x_coord_img: "x_coord ` {(0::real)..1} = {-1/2 .. 1/2}"
  by (auto simp add: x_coord_def image_def algebra_simps)

lemma x_coord_back_img: "finite ({0..1} ∩ x_coord -` {x::real})"
  by (simp add: finite_vimageI inj_on_def x_coord_def)


abbreviation "rot_x t1 t2 ≡ (if (t1 - 1/2) ≤ 0 then (2 * t2 - 1) * t1 + 1/2 ::real else 2 * t2 - 2 * t1 * t2 +t1 -1/2::real)"

lemma rot_x_ivl:
  assumes "0 ≤ x"
    "x ≤ 1"
    "0 ≤ y"
    "y ≤ 1" 
  shows "0 ≤ rot_x x y ∧ rot_x x y ≤ 1"
proof - 
  have i: "⋀a::real. a ≤ 0 ⟹ 0 ≤ y ⟹ y ≤ 1  ⟹ -1/2 < a ⟹ (a * (1 - 2*y) ≤ 1/2)"
  proof -
    have 0: "⋀a::real. a ≤ 0 ⟹ 0 ≤ y ⟹ y ≤ 1  ⟹ -1/2 < a ⟹ (-a ≤ 1/2)"
      by (sos "((((A<0 * A<1) * R<1) + (R<1 * (R<1/4 * [2*a + 1]^2))))")
    have 1: "⋀a. a ≤ 0 ⟹ 0 ≤ y ⟹ y ≤ 1  ⟹ -1/2 < a ⟹ (a * (1 - 2*y) ≤ -a)"
      by (sos "((((A<0 * A<1) * R<1) + (((A<=0 * (A<1 * R<1)) * (R<2/3 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<2/3 * [1]^2)) + ((A<=0 * (A<=2 * (A<0 * R<1))) * (R<2/3 * [1]^2))))))")
    show "⋀a::real. a ≤ 0 ⟹ 0 ≤ y ⟹ y ≤ 1 ⟹ -1/2 < a ⟹ (a * (1 - 2*y) ≤ 1/2)" using 0 1 by force
  qed
  have *: "(x * 2 + y * 4 ≤ 3 + x * (y * 4)) =  ( (x-1) ≤ 1/2+ (x-1) * (y * 2))"
    by (sos "((((A<0 * R<1) + ((A<=0 * R<1) * (R<2 * [1]^2)))) & (((A<0 * R<1) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))")
  show ?thesis
    using assms
    apply(auto simp add: algebra_simps divide_simps linorder_class.not_le)
       apply (sos "(((A<0 * R<1) + (((A<=2 * (A<=3 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<2 * [1]^2))))))")
      apply (sos "(((A<0 * R<1) + (((A<=2 * R<1) * (R<1 * [1]^2)) + (((A<=1 * (A<=3 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=2 * R<1)) * (R<2 * [1]^2))))))")
    using i[of "(x::real) - 1"] affine_ineq
     apply (fastforce simp: algebra_simps *)+
    done
qed

end