# Theory DiamExample

```section ‹The Diamond Example›

theory DiamExample
imports Green SymmetricR2Shapes
begin

lemma abs_if':
fixes a :: "'a :: {abs_if,ordered_ab_group_add}"
shows "¦a¦ = (if a ≤ 0 then - a else a)"

locale diamond = R2 +
fixes d::real
assumes d_gt_0: "0 < d"
begin

definition diamond_y_gen :: "real ⇒ real" where
"diamond_y_gen ≡λt.  1/2 - ¦t¦"

definition diamond_cube_gen:: "((real * real) ⇒ (real * real))" where
"diamond_cube_gen ≡ (λ(x,y). (d * x_coord x, (2 * y - 1) * (d * diamond_y_gen (x_coord x))))"

lemma diamond_y_gen_valid:
assumes "a ≤ 0" "0 ≤ b"
shows "diamond_y_gen piecewise_C1_differentiable_on {a..b}"
unfolding piecewise_C1_differentiable_on_def diamond_y_gen_def
proof (intro conjI exI)
show "continuous_on {a..b} (λt. 1 / 2 - ¦t¦)"
by (intro continuous_intros)
show "finite{0}"
by simp
show "(λt. 1 / 2 - ¦t¦) C1_differentiable_on {a..b} - {0}"
by (intro derivative_intros) auto
qed

lemma diamond_cube_gen_boundary_valid:
assumes "(k,γ)∈boundary (diamond_cube_gen)"
shows "valid_path γ"
using assms
proof (auto simp add: valid_path_def boundary_def horizontal_boundary_def vertical_boundary_def diamond_cube_gen_def)
have rw2: "(λx. diamond_y_gen (x_coord x)) = diamond_y_gen o x_coord" by auto
note [derivative_intros] = C1_differentiable_on_pair pair_prod_smooth_pw_smooth scale_piecewise_C1_differentiable_on piecewise_C1_differentiable_neg piecewise_C1_differentiable_compose diamond_y_gen_valid
show "(λx. (d * x_coord x, - (d * diamond_y_gen (x_coord x)))) piecewise_C1_differentiable_on {0..1}"
apply(auto intro!: derivative_intros)+
apply (auto simp add: x_coord_smooth rw2)
by(auto intro!: derivative_intros simp add: x_coord_img x_coord_back_img C1_differentiable_imp_piecewise[OF x_coord_smooth])+
show "(λx. (d * x_coord x, d * diamond_y_gen (x_coord x))) piecewise_C1_differentiable_on {0..1}"
apply(auto intro!: derivative_intros)+
apply (auto simp add: x_coord_smooth rw2)
by(auto intro!: derivative_intros simp add: x_coord_img x_coord_back_img C1_differentiable_imp_piecewise[OF x_coord_smooth])+
qed

definition diamond_x where
"diamond_x ≡ λt. (t - 1/2) * d"

definition diamond_y where
"diamond_y ≡ λt. d/2 - ¦t¦"

definition diamond_cube where
"diamond_cube = (λ(x,y). (diamond_x x, (2 * y - 1) * (diamond_y (diamond_x x))))"

definition rot_diamond_cube where
"rot_diamond_cube = prod.swap o (diamond_cube) o prod.swap"

lemma diamond_eq_characterisations:
shows "diamond_cube (x,y)= diamond_cube_gen (x,y)"
by(auto simp add: diamond_cube_def diamond_cube_gen_def diamond_x_def x_coord_def diamond_y_def diamond_y_gen_def d_gt_0 field_simps mult_le_0_iff abs_if split: if_split_asm)

lemma diamond_eq_characterisations_fun: "diamond_cube = diamond_cube_gen"
using diamond_eq_characterisations by auto

lemma diamond_y_valid:
shows "diamond_y piecewise_C1_differentiable_on {-d/2..d/2}"         (is ?P)
"(λx. diamond_y x) piecewise_C1_differentiable_on {-d/2..d/2}" (is ?Q)
proof -
have f0: "finite {0}"
by simp
show ?P ?Q
unfolding piecewise_C1_differentiable_on_def diamond_y_def
by (fastforce intro!: f0 continuous_intros derivative_intros)+
qed

lemma diamond_cube_boundary_valid:
assumes "(k,γ) ∈ boundary (diamond_cube)"
shows "valid_path γ"
using diamond_cube_gen_boundary_valid assms d_gt_0

lemma diamond_cube_is_type_I:
shows "typeI_twoCube (diamond_cube)"
unfolding typeI_twoCube_def
proof (intro exI conjI ballI)
show "-d/2 < d/2"
using d_gt_0 by auto
show "⋀x. x ∈ {- d / 2..d / 2} ⟹ - diamond_y x ≤ diamond_y x"
using diamond_y_def by auto
have f0: "finite {0}"
by simp
show "diamond_y piecewise_C1_differentiable_on {- d / 2..d / 2}"
"(λx. - diamond_y x) piecewise_C1_differentiable_on {- d / 2..d / 2}"
unfolding diamond_y_def piecewise_C1_differentiable_on_def
by (rule conjI exI f0 continuous_intros derivative_intros | force)+
show "diamond_cube =
(λ(x, y). ((1 - x) * (- d / 2) + x * (d / 2),
(1 - y) * - diamond_y ((1 - x) * (- d / 2) + x * (d / 2)) +
y * diamond_y ((1 - x) * (- d / 2) + x * (d / 2))))"
by (auto simp: diamond_cube_def diamond_x_def diamond_y_def divide_simps algebra_simps)
qed

lemma diamond_cube_valid_two_cube:
shows "valid_two_cube (diamond_cube)"
apply (auto simp add: valid_two_cube_def boundary_def horizontal_boundary_def vertical_boundary_def diamond_cube_def
diamond_x_def card_insert_if)
apply (metis (no_types, opaque_lifting) cancel_comm_monoid_add_class.diff_cancel d_gt_0 mult.commute mult_2 mult_zero_right order_less_irrefl prod.inject field_sum_of_halves)
apply (metis (no_types, opaque_lifting) add_diff_cancel_right' d_gt_0 mult_cancel_left mult_zero_right order_less_irrefl prod.inject)
done

lemma rot_diamond_cube_boundary_valid:
assumes "(k,γ)∈boundary (rot_diamond_cube)"
shows "valid_path γ"
using d_gt_0 swap_valid_boundaries diamond_cube_boundary_valid
using assms diamond_cube_is_type_I rot_diamond_cube_def by fastforce

lemma rot_diamond_cube_is_type_II:
shows "typeII_twoCube (rot_diamond_cube)"
using d_gt_0 swap_typeI_is_typeII diamond_cube_is_type_I

lemma rot_diamond_cube_valid_two_cube: "valid_two_cube (rot_diamond_cube)"
using valid_cube_valid_swap diamond_cube_valid_two_cube d_gt_0 rot_diamond_cube_def
by force

definition diamond_top_edges where
"diamond_top_edges = (- 1::int, λx. (diamond_x x, diamond_y (diamond_x x)))"

definition diamond_bot_edges where
"diamond_bot_edges = (1::int,  λx. (diamond_x x, - diamond_y (diamond_x x)))"

lemma diamond_cube_boundary_explicit:
"boundary (diamond_cube ) =
{diamond_top_edges,
diamond_bot_edges,
(- 1::int, λy. (diamond_x 0, (2 * y - 1) * diamond_y (diamond_x 0))),
(1::int, λy. (diamond_x 1, (2 * y - 1) * diamond_y (diamond_x 1)))}"
by (auto simp only: diamond_top_edges_def diamond_bot_edges_def valid_two_cube_def boundary_def horizontal_boundary_def vertical_boundary_def diamond_cube_def Un_iff algebra_simps)

definition diamond_top_left_edge where
"diamond_top_left_edge = (- 1::int, (λx. (diamond_x (1/2 * x),  (diamond_x (1/2 * x)) + d/2)))"

definition diamond_top_right_edge where
"diamond_top_right_edge = (- 1::int, (λx. (diamond_x (1/2 * x + 1/2),  (-(diamond_x (1/2 * x + 1/2)) + d/2))))"

definition diamond_bot_left_edge where
"diamond_bot_left_edge = (1::int, (λx. (diamond_x (1/2 * x), - (diamond_x (1/2 * x) + d/2))))"

definition diamond_bot_right_edge where
"diamond_bot_right_edge = (1::int, (λx. (diamond_x (1/2 * x + 1/2), - (-(diamond_x (1/2 * x + 1/2)) + d/2))))"

lemma diamond_edges_are_valid:
"valid_path (snd (diamond_top_left_edge))"
"valid_path (snd (diamond_top_right_edge))"
"valid_path (snd (diamond_bot_left_edge))"
"valid_path (snd (diamond_bot_right_edge))"
by (auto simp add: valid_path_def diamond_top_left_edge_def diamond_bot_right_edge_def diamond_bot_left_edge_def diamond_top_right_edge_def diamond_x_def)

definition diamond_cube_boundary_to_subdiv where
"diamond_cube_boundary_to_subdiv (gamma::(int × (real ⇒ real × real))) ≡
if (gamma = diamond_top_edges) then
{diamond_top_left_edge, diamond_top_right_edge}
else if (gamma = diamond_bot_edges) then
{diamond_bot_left_edge, diamond_bot_right_edge}
else {}"

lemma rot_diam_edge_1:
"(1::int, λx::real. ((x::real) * (2 * diamond_y (diamond_x 0)) - 1 * diamond_y (diamond_x 0), diamond_x 0)) =
(1, λx. (x * (2 * diamond_y (diamond_x 0)) -  (diamond_y (diamond_x 0)), diamond_x 0))"

definition diamond_left_edges where
"diamond_left_edges = (- 1, λy. (- diamond_y (diamond_x y), diamond_x y))"

definition diamond_right_edges where
"diamond_right_edges = (1, λy. ( diamond_y (diamond_x y), diamond_x y))"

lemma rot_diamond_cube_boundary_explicit:
"boundary (rot_diamond_cube) = {(1::int, λx::real. ((2 * x - 1) * diamond_y (diamond_x 0), diamond_x 0)),
(- 1, λx. ((2 * x - 1) * diamond_y (diamond_x 1), diamond_x 1)),
diamond_left_edges, diamond_right_edges}"
proof -
have "boundary (rot_diamond_cube) = { (1::int, λx::real. ((2 * x - 1) * diamond_y (diamond_x 0), diamond_x 0)),
(- 1, λx. ((2 * x - 1) * diamond_y (diamond_x 1), diamond_x 1)),
(- 1, λy. ((2 * 0 - 1) * diamond_y (diamond_x y), diamond_x y)),
(1, λy. ((2 * 1 - 1) * diamond_y (diamond_x y), diamond_x y))}"
by (auto simp only: valid_two_cube_def boundary_def horizontal_boundary_def vertical_boundary_def rot_diamond_cube_def diamond_cube_def o_def swap_simp Un_iff)
then show ?thesis
by (auto simp add: diamond_left_edges_def diamond_right_edges_def)
qed

lemma rot_diamond_cube_vertical_boundary_explicit:
"vertical_boundary (rot_diamond_cube) = {diamond_left_edges, diamond_right_edges}"
proof -
have "vertical_boundary (rot_diamond_cube) = {(- 1::int, λy. ((2 * 0 - 1) * diamond_y (diamond_x y), diamond_x y)),
(1, λy. ((2 * 1 - 1) * diamond_y (diamond_x y), diamond_x y))}"
by (auto simp only: valid_two_cube_def boundary_def horizontal_boundary_def vertical_boundary_def rot_diamond_cube_def diamond_cube_def o_def swap_simp Un_iff)
then show ?thesis
by (auto simp add: diamond_left_edges_def diamond_right_edges_def)
qed

definition rot_diamond_cube_boundary_to_subdiv where
"rot_diamond_cube_boundary_to_subdiv (gamma::(int × (real ⇒ real × real))) ≡
if (gamma = diamond_left_edges ) then {diamond_bot_left_edge , diamond_top_left_edge}
else if (gamma = diamond_right_edges) then {diamond_bot_right_edge, diamond_top_right_edge}
else {}"

definition diamond_boundaries_reparam_map where
"diamond_boundaries_reparam_map ≡ id"

lemma diamond_boundaries_reparam_map_bij:
"bij (diamond_boundaries_reparam_map)"
by(auto simp add: bij_def full_SetCompr_eq[symmetric] diamond_boundaries_reparam_map_def)

lemma diamond_bot_edges_neq_diamond_top_edges:
"diamond_bot_edges ≠  diamond_top_edges"

lemma diamond_top_left_edge_neq_diamond_top_right_edge:
"diamond_top_left_edge ≠ diamond_top_right_edge"
apply (simp add: diamond_top_left_edge_def diamond_top_right_edge_def diamond_x_def diamond_y_def)
using d_gt_0
apply (auto simp add: algebra_simps divide_simps)
by (metis (no_types, opaque_lifting) diff_zero div_0 divide_divide_eq_right order_less_irrefl prod.inject field_sum_of_halves)

lemma neqs1:
shows "(λx. (diamond_x x, diamond_y (diamond_x x))) ≠ (λx. (diamond_x x, - diamond_y (diamond_x x)))"
and "(λy. (- diamond_y (diamond_x y), diamond_x y)) ≠ (λy. (diamond_y (diamond_x y), diamond_x y))"
and "(λx. (diamond_x(x/2 + 1/2), diamond_x(x/2 + 1/2) - d/2)) ≠ (λx. (diamond_x(x/2), - diamond_x(x/2) - d/2))"
and "(λx. (diamond_x(x/2 + 1/2), d/2 - diamond_x(x/2 + 1/2))) ≠ (λx. (diamond_x(x/2), diamond_x(x/2) + d/2))"
and "(λx. (diamond_x(x/2), - diamond_x(x/2) - d/2)) ≠ (λx. (diamond_x(x/2 + 1/2), diamond_x(x/2 + 1/2) - d/2))"
and "(λx. (diamond_x(x/2), diamond_x(x/2) + d/2)) ≠ (λx. (diamond_x(x/2 + 1/2), d/2 - diamond_x(x/2 + 1/2)))"
using d_gt_0 by (auto simp: diamond_x_def diamond_y_def dest: fun_cong [where x = "1/2"])

lemma neqs2:
shows "(λx. (diamond_x x, diamond_y (diamond_x x))) ≠ (λx. ((2 * x - 1) * diamond_y (diamond_x 1), diamond_x 1))"
and "(λx. (diamond_x x, - diamond_y (diamond_x x))) ≠ (λx. ((2 * x - 1) * diamond_y (diamond_x 0), diamond_x 0))"
using d_gt_0 by (auto simp: diamond_x_def diamond_y_def dest: fun_cong [where x = "1"])

lemma diamond_cube_is_only_horizontal_div_of_rot:
shows "only_horizontal_division (boundary (diamond_cube)) {rot_diamond_cube}"
unfolding only_horizontal_division_def
proof (rule exI [of _ "{}"], simp, intro conjI ballI)
show "finite (boundary diamond_cube)"
by (simp add: boundary_def horizontal_boundary_def vertical_boundary_def)
show "boundary_chain (boundary diamond_cube)"
show "⋀x. x ∈ boundary diamond_cube ⟹ case x of (k, x) ⇒ valid_path x"
using diamond_cube_boundary_valid by blast
let ?𝒱 = "(boundary (diamond_cube))"
have 0: "finite ?𝒱"
by (auto simp add: boundary_def horizontal_boundary_def vertical_boundary_def)
have 1: "boundary_chain ?𝒱" using two_cube_boundary_is_boundary by auto
let ?subdiv = "{diamond_top_left_edge, diamond_top_right_edge, diamond_bot_left_edge, diamond_bot_right_edge}"
let ?pi = "{(1::int, λx. ((2 * x - 1) * diamond_y (diamond_x 0), diamond_x 0)),
(- 1, λx. ((2 * x - 1) * diamond_y (diamond_x 1), diamond_x 1))}"
let ?pj = "{(-1::int, λy. (diamond_x 0, (2 * y - 1) * diamond_y (diamond_x 0))),
(1, λy. (diamond_x 1, (2 * y - 1) * diamond_y (diamond_x 1)))}"
let ?f = "diamond_cube_boundary_to_subdiv"
have 2: "common_sudiv_exists (two_chain_vertical_boundary {rot_diamond_cube}) ?𝒱"
unfolding common_sudiv_exists_def
proof (intro exI conjI)
show "chain_subdiv_chain (boundary (diamond_cube) - ?pj) ?subdiv"
unfolding chain_subdiv_chain_character
proof (intro exI conjI)
have 1: "(boundary (diamond_cube)) - ?pj = {diamond_top_edges, diamond_bot_edges}"
apply (auto simp add: diamond_cube_boundary_explicit diamond_x_def diamond_top_edges_def diamond_bot_edges_def)
apply (metis (no_types, opaque_lifting) abs_zero cancel_comm_monoid_add_class.diff_cancel diamond_x_def diamond_y_def diff_0 minus_diff_eq mult.commute mult_zero_right prod.inject neqs2)
by (metis (no_types, opaque_lifting) cancel_comm_monoid_add_class.diff_cancel d_gt_0 divide_eq_0_iff linorder_not_le mult.commute mult_zero_right order_refl prod.sel(1) zero_neq_numeral)
then show "⋃ (?f ` (boundary (diamond_cube) - ?pj)) = ?subdiv"
by (auto simp add: diamond_top_edges_def diamond_bot_edges_def diamond_cube_boundary_to_subdiv_def)
have "chain_subdiv_path (reversepath (λx. (diamond_x x, diamond_y (diamond_x x))))
{(- 1::int, λx. (diamond_x(x/2), diamond_x(x/2) + d/2)),
(- 1::int, λx. (diamond_x(x/2 + 1/2), d/2 - diamond_x(x/2 + 1/2)))}"
proof -
let ?F = "λx. (diamond_x(x/2 + 1/2), d/2 - diamond_x(x/2 + 1/2))"
let ?G = "λx. (diamond_x(x/2), diamond_x(x/2) + d/2)"
have dist: "distinct [(-1, ?F), (-1, ?G)]"
using d_gt_0 by (auto simp: diamond_x_def diamond_y_def dest: fun_cong)
have rj: "rec_join [(-1, ?F), (-1, ?G)] = reversepath (λx. (diamond_x x, diamond_y (diamond_x x)))"
using d_gt_0 by (auto simp add: subpath_def diamond_x_def diamond_y_def joinpaths_def reversepath_def algebra_simps divide_simps)
have "pathstart ?F = pathfinish ?G"
using d_gt_0 by(auto simp add: subpath_def diamond_x_def diamond_y_def pathfinish_def pathstart_def)
then have val: "valid_chain_list [(-1, ?F), (-1, ?G)]"
show ?thesis
using chain_subdiv_path.I [OF dist rj val]
qed
moreover have "chain_subdiv_path (λx. (diamond_x x, - diamond_y (diamond_x x)))
{(1::int, λx. (diamond_x(x/2), - diamond_x(x/2) - d/2)),
(1::int, λx. (diamond_x(x/2 + 1/2), diamond_x(x/2 + 1/2) - d/2))}"
proof -
let ?F = "λx. (diamond_x(x/2), - diamond_x(x/2) - d/2)"
let ?G = "λx. (diamond_x(x/2 + 1/2), diamond_x(x/2 + 1/2) - d/2)"
have dist: "distinct [(1, ?F), (1, ?G)]"
using d_gt_0 by (auto simp: diamond_x_def diamond_y_def dest: fun_cong)
have rj: "rec_join [(1, ?F), (1, ?G)] = (λx. (diamond_x x, - diamond_y (diamond_x x)))"
using d_gt_0 by (auto simp add: subpath_def diamond_x_def diamond_y_def joinpaths_def algebra_simps divide_simps)
have "pathfinish ?F = pathstart ?G"
using d_gt_0 by(auto simp add: subpath_def diamond_x_def diamond_y_def pathfinish_def pathstart_def)
then have val: "valid_chain_list [(1, ?F), (1, ?G)]"
show ?thesis
using chain_subdiv_path.I [OF dist rj val] by simp
qed
ultimately show **:
"∀(k::int, γ)∈boundary (diamond_cube) - ?pj.
if k = (1::int) then chain_subdiv_path γ (?f (k::int, γ))
else chain_subdiv_path (reversepath γ) (?f (k::int, γ))"
"∀p∈boundary (diamond_cube) - ?pj. ∀p'∈boundary (diamond_cube) - ?pj.
p ≠ p' ⟶ ?f p ∩ ?f p' = {}"
"∀x∈boundary (diamond_cube) - ?pj. finite (?f x)"
by(simp_all add: diamond_cube_boundary_to_subdiv_def UNION_eq 1 diamond_top_edges_def diamond_bot_edges_def diamond_bot_left_edge_def diamond_bot_right_edge_def diamond_top_left_edge_def diamond_top_right_edge_def neqs1)
qed
have *: "⋀f. ⋃ (f ` {rot_diamond_cube}) = f (rot_diamond_cube)" by auto
show "chain_subdiv_chain (two_chain_vertical_boundary {rot_diamond_cube} - ?pi) ?subdiv"
unfolding chain_subdiv_chain_character two_chain_vertical_boundary_def *
proof (intro exI conjI)
let ?f = "rot_diamond_cube_boundary_to_subdiv"
have 1: "(vertical_boundary (rot_diamond_cube) - ?pi) = {diamond_left_edges, diamond_right_edges}"
apply (auto simp add: rot_diamond_cube_vertical_boundary_explicit  diamond_left_edges_def diamond_right_edges_def)
by (metis (no_types, opaque_lifting) diff_0 mult.left_neutral mult_minus_left mult_zero_right prod.inject neqs1(2))
show "⋃ (?f ` (vertical_boundary (rot_diamond_cube) - ?pi)) = ?subdiv"
apply (simp add: rot_diamond_cube_boundary_to_subdiv_def 1 UNION_eq subpath_def)
apply (auto simp add: set_eq_iff diamond_right_edges_def diamond_left_edges_def)
done
have "chain_subdiv_path (reversepath (λy. (- diamond_y (diamond_x y), diamond_x y)))
{(1, λx. (diamond_x(x/2), - diamond_x(x/2) - d/2)),
(-1, λx. (diamond_x(x/2), diamond_x(x/2) + d/2))}"
proof -
let ?F = "λx. (diamond_x(x/2), - diamond_x(x/2) - d/2)"
let ?G = "λx. (diamond_x(x/2), diamond_x(x/2) + d/2)"
have dist: "distinct [(-1, ?G), (1::int, ?F)]"
using d_gt_0 by simp
have rj: "rec_join [(-1, ?G), (1::int, ?F)] = reversepath (λy. (- diamond_y (diamond_x y), diamond_x y))"
using d_gt_0 by (auto simp add: subpath_def diamond_x_def diamond_y_def joinpaths_def reversepath_def algebra_simps divide_simps)
have "pathstart ?G = pathstart ?F"
using d_gt_0 by(auto simp add: subpath_def diamond_x_def diamond_y_def pathstart_def)
then have val: "valid_chain_list [(-1, ?G), (1::int, ?F)]"
show ?thesis
using chain_subdiv_path.I [OF dist rj val] by (simp add: insert_commute)
qed
moreover have "chain_subdiv_path (λy. (diamond_y (diamond_x y), diamond_x y))
{(1, λx. (diamond_x(x/2 + 1/2), diamond_x(x/2 + 1/2) - d/2)),
(-1, λx. (diamond_x(x/2 + 1/2), d/2 - diamond_x(x/2 + 1/2)))}"
proof -
let ?F = "λx. (diamond_x(x/2 + 1/2), d/2 - diamond_x(x/2 + 1/2))"
let ?G = "λx. (diamond_x(x/2 + 1/2), diamond_x(x/2 + 1/2) - d/2)"
have dist: "distinct [(1::int, ?G), (-1, ?F)]"
by simp
have rj: "rec_join [(1::int, ?G), (-1, ?F)] = (λy. (diamond_y (diamond_x y), diamond_x y))"
using d_gt_0 by (auto simp add: subpath_def diamond_x_def diamond_y_def joinpaths_def reversepath_def algebra_simps divide_simps)
have "pathfinish ?F = pathfinish ?G"
using d_gt_0 by(auto simp add: subpath_def diamond_x_def diamond_y_def pathfinish_def pathstart_def)
then have val: "valid_chain_list [(1::int, ?G), (-1, ?F)]"
show ?thesis
using chain_subdiv_path.I [OF dist rj val] by simp
qed
ultimately show "∀(k, γ)∈vertical_boundary (rot_diamond_cube) - ?pi.
if k = 1 then chain_subdiv_path γ (?f (k, γ))
else chain_subdiv_path (reversepath γ) (?f (k, γ))"
"∀p∈vertical_boundary (rot_diamond_cube) - ?pi.
∀p'∈vertical_boundary (rot_diamond_cube) - ?pi.
p ≠ p' ⟶ ?f p ∩ ?f p' = {}"
"∀x∈vertical_boundary (rot_diamond_cube) - ?pi. finite (?f x)"
by(auto simp add: rot_diamond_cube_boundary_to_subdiv_def 1 diamond_left_edges_def
diamond_right_edges_def diamond_bot_left_edge_def diamond_bot_right_edge_def
diamond_top_left_edge_def diamond_top_right_edge_def neqs1)
qed
show "(∀(k::int, γ)∈?subdiv. valid_path γ)"
by (simp add: diamond_edges_are_valid prod.case_eq_if set_eq_iff)
show "boundary_chain ?subdiv"
by (auto simp add: boundary_chain_def diamond_top_left_edge_def diamond_top_right_edge_def diamond_bot_left_edge_def diamond_bot_right_edge_def)
show "(∀(k, γ)∈?pi. point_path γ)"
using d_gt_0 by (auto simp add: point_path_def diamond_x_def diamond_y_def)
show "(∀(k, γ)∈?pj. point_path γ)"
using d_gt_0 by (auto simp add: point_path_def diamond_x_def diamond_y_def)
qed
show "common_sudiv_exists (two_chain_vertical_boundary {rot_diamond_cube}) (boundary diamond_cube) ∨
common_reparam_exists (boundary diamond_cube) (two_chain_vertical_boundary {rot_diamond_cube})"
using 0 1 2 diamond_cube_boundary_valid by auto
qed

abbreviation "rot_y t1 t2 ≡ (t1 - 1/2) / (2* diamond_y_gen (x_coord (rot_x t1 t2))) + 1/2"

lemma rot_y_ivl:
assumes "(0::real) ≤ x" "x ≤ 1" "0 ≤ y" "y ≤ 1"
shows "0 ≤ rot_y x y ∧ rot_y x y ≤ 1"
using assms
apply(auto simp add: x_coord_def diamond_y_gen_def algebra_simps divide_simps linorder_class.not_le abs_if)
using mult_nonneg_nonneg apply fastforce
using dual_order.order_iff_strict apply fastforce
apply (sos "(((((A<0 * A<1) * R<1) + (((A<=4 * (A<1 * R<1)) * (R<1/2 * [1]^2)) + (((A<=3 * (A<0 * R<1)) * (R<1/2 * [1]^2)) + ((A<=0 * (A<=2 * (A<=3 * R<1))) * (R<1 * [1]^2)))))) & ((((A<0 * A<1) * R<1) + (((A<=4 * (A<1 * R<1)) * (R<1/3 * [1]^2)) + (((A<=4 * (A<0 * R<1)) * (R<1/3 * [1]^2)) + ((A<=3 * (A<=4 * R<1)) * (R<1/3 * [1]^2)))))))")
using assms(1) mult_left_le_one_le apply blast
using affine_ineq apply fastforce+
done

lemma diamond_gen_eq_rot_diamond:
assumes"0 ≤ x" "x ≤ 1" "0 ≤ y" "y ≤ 1"
shows "(diamond_cube_gen (x, y)) = (rot_diamond_cube (rot_y x y, rot_x x y))"
proof
show "snd (diamond_cube_gen (x, y)) = snd (rot_diamond_cube (rot_y x y, rot_x x y))"
apply(simp only: rot_diamond_cube_def diamond_eq_characterisations_fun)
by(auto simp add:  diamond_cube_gen_def x_coord_def diamond_y_gen_def algebra_simps divide_simps)
show "fst (diamond_cube_gen (x, y)) = fst (rot_diamond_cube (rot_y x y, rot_x x y))"
using assms
apply(auto simp add: diamond_cube_gen_def rot_diamond_cube_def diamond_eq_characterisations_fun)
apply(auto simp add: x_coord_def diamond_y_gen_def algebra_simps divide_simps abs_if split: if_split_asm)
apply sos+
done
qed

lemma rot_diamond_eq_diamond_gen:
assumes "0 ≤ x" "x ≤ 1" "0 ≤ y" "y ≤ 1"
shows "rot_diamond_cube (x, y) = diamond_cube_gen (rot_x y x, rot_y y x)"
proof
show "fst (rot_diamond_cube (x, y)) = fst (diamond_cube_gen (rot_x y x, rot_y y x))"
apply(simp only: rot_diamond_cube_def diamond_eq_characterisations_fun)
by(auto simp add:  diamond_cube_gen_def x_coord_def diamond_y_gen_def algebra_simps divide_simps)
show "snd (rot_diamond_cube (x, y)) = snd (diamond_cube_gen (rot_x y x, rot_y y x))"
using assms
apply(auto simp add: diamond_cube_gen_def rot_diamond_cube_def diamond_eq_characterisations_fun)
apply(auto simp add: x_coord_def diamond_y_gen_def algebra_simps divide_simps abs_if split: if_split_asm)
apply sos+
done
qed

lemma rot_img_eq: "cubeImage (diamond_cube_gen) = cubeImage (rot_diamond_cube)"
proof(auto simp add: cubeImage_def image_def cbox_def real_pair_basis)
show "∃a≥0. a ≤ 1 ∧ (∃b≥0. b ≤ 1 ∧ diamond_cube_gen (x, y) = rot_diamond_cube (a, b))"
if "0 ≤ x" "x ≤ 1" "0 ≤ y" "y ≤ 1" "(a, b) = diamond_cube_gen (x, y)"
for a b x y
proof (intro exI conjI)
let ?a = "rot_y x y"
let ?b = "rot_x x y"
show "0 ≤ ?a" "?a ≤ 1"
using rot_y_ivl that by blast+
show "0 ≤ ?b" "?b ≤ 1"
using rot_x_ivl that by blast+
show "diamond_cube_gen (x, y) = rot_diamond_cube (?a, ?b)"
using that d_gt_0 diamond_gen_eq_rot_diamond by auto
qed
show "∃a≥0. a ≤ 1 ∧ (∃b≥0. b ≤ 1 ∧ rot_diamond_cube (x, y) = diamond_cube_gen (a, b))"
if "0 ≤ x" "x ≤ 1" "0 ≤ y" "y ≤ 1" "(a, b) = rot_diamond_cube (x, y)" for a b x y
proof (intro exI conjI)
let ?a = "rot_x y x"
let ?b = "rot_y y x"
show "0 ≤ ?a" "?a ≤ 1"
using rot_x_ivl that by blast+
show "0 ≤ ?b" "?b ≤ 1"
using rot_y_ivl that by blast+
show "rot_diamond_cube (x, y) = diamond_cube_gen (?a, ?b)"
using that d_gt_0 rot_diamond_eq_diamond_gen by auto
qed
qed

lemma rot_diamond_gen_div_diamond_gen:
shows "gen_division (cubeImage (diamond_cube_gen)) (cubeImage ` {rot_diamond_cube})"
using rot_img_eq by(auto simp add: gen_division_def)

lemma rot_diamond_gen_div_diamond:
shows "gen_division (cubeImage (diamond_cube)) (cubeImage ` {rot_diamond_cube})"
using rot_diamond_gen_div_diamond_gen
by(simp only: diamond_eq_characterisations_fun)

lemma GreenThm_diamond:
assumes "analytically_valid (cubeImage (diamond_cube)) (λx. F x ∙ i) j"
"analytically_valid (cubeImage (diamond_cube)) (λx. F x ∙ j) i"
shows "integral (cubeImage (diamond_cube)) (λx. partial_vector_derivative (λx. F x ∙ j) i x - partial_vector_derivative (λx. F x ∙ i) j x) =
one_chain_line_integral F {i, j} (boundary (diamond_cube))"
proof -
have 0: "∀(k, γ)∈boundary (diamond_cube). valid_path γ"
using diamond_cube_boundary_valid d_gt_0 by auto
have "⋀twoCube. twoCube ∈ {diamond_cube} ⟹ typeI_twoCube twoCube"
using assms diamond_cube_is_type_I by auto
moreover have "valid_two_chain {diamond_cube}"
using assms(1) diamond_cube_valid_two_cube valid_two_chain_def by auto
moreover have "gen_division (cubeImage (diamond_cube)) (cubeImage ` {diamond_cube})"
moreover have "(∀twoCube∈({rot_diamond_cube}). typeII_twoCube twoCube)"
using assms rot_diamond_cube_is_type_II by auto
moreover have "valid_two_chain {rot_diamond_cube}"
using assms(1) rot_diamond_cube_valid_two_cube valid_two_chain_def by auto
moreover have "gen_division (cubeImage (diamond_cube)) (cubeImage ` {rot_diamond_cube})"
using rot_diamond_gen_div_diamond by auto
moreover have 3: "only_vertical_division (boundary (diamond_cube)) {diamond_cube}"
using twoChainVertDiv_of_itself[of "{diamond_cube}"] diamond_cube_boundary_valid assms