# 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:  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:  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
shows
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))) "

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
shows
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
show "𝒱 . finite   finite 𝒱
(x𝒱. case x of (k, γ)  xtwo_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 ?ℋ =
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
xtwo_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)
(xtwo_chain_vertical_boundary C.
case x of (k, γ)  xtwo_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:

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