theory Real_Unit_Interval  
  imports "HOL.Real" 
          Unit_Interval_Group
          "HOL-Analysis.Abstract_Metric_Spaces"
begin

text \<open>Examples\<close>

lemma "[(0::nat)] \<cdot>\<^bsub>\<UU>\<^esub> (x :: real) = \<zero>\<^bsub>\<UU>\<^esub>"
  using fracs.add.nat_pow_0. 
       
lemma 
  shows "[Suc k] \<cdot>\<^bsub>\<UU>\<^esub> (\<alpha> :: rat) = [k] \<cdot>\<^bsub>\<UU>\<^esub> \<alpha> \<oplus>\<^bsub>\<UU>\<^esub> \<alpha>"
  using fracs.add.nat_pow_Suc[of k \<alpha>].

definition crot :: "real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real"
  where "crot \<alpha> \<beta> n \<equiv> [n] \<cdot>\<^bsub>\<UU>\<^esub> \<alpha> \<oplus>\<^bsub>\<UU>\<^esub> \<beta>"

(* obtained claims about abelian group *)
find_theorems (170) name: rui

section \<open>Metric space\<close>

definition circle_distance :: "real \<Rightarrow> real \<Rightarrow> real" ("dRot")
  where "circle_distance x y \<equiv> min (frac (x-y)) (frac (y-x))"

lemma circle_distance_def': 
  "dRot x y = (min (abs ((frac x)-(frac y))) (1-(abs ((frac x)-(frac y)))))"
proof (rule linorder_cases[of "frac x" "frac y"])
  assume a: "frac x < frac y"
  then show ?thesis
    unfolding circle_distance_def
      frac_diff_neg[OF a]  
      frac_diff_pos[OF less_imp_le, OF a] by simp
next
  assume a: "frac x = frac y"
  then show ?thesis
    unfolding circle_distance_def 
      frac_diff_pos[OF order_eq_refl, OF a]
      frac_diff_pos[OF order_eq_refl, OF a[symmetric]] a by simp
next
  assume a: "frac y < frac x"
  then show ?thesis
    unfolding circle_distance_def
      frac_diff_neg[OF a]  
      frac_diff_pos[OF less_imp_le, OF a] by simp
qed

lemma dRot_if: "dRot x y = (if (abs ((frac x)-(frac y))) \<le> 1/2 then (abs ((frac x)-(frac y))) else (1-(abs ((frac x)-(frac y)))))"
  unfolding circle_distance_def'
by fastforce

lemma dRot_max: "dRot x y \<le> 1/2"
  unfolding circle_distance_def'
  by argo

lemma dRot_min: "0 \<le> dRot x y"
  unfolding circle_distance_def by simp

lemma dRot_sym: "dRot x y = dRot y x"
  by (simp add: circle_distance_def)

lemma dRot_frac_frac: "dRot (frac x) (frac y) = dRot x y"
  by (simp add: dRot_if)

lemma dRot_triang:
  shows "dRot x y \<le> (dRot x z) + (dRot z y)"
proof(cases "\<bar>frac x - frac z\<bar> \<le> 1 / 2")
  case True
  then show ?thesis
    unfolding dRot_if
    using field_sum_of_halves[of 1, symmetric] by argo
    (* by (smt (verit) field_sum_of_halves) *)
next
  case False
  then show ?thesis
    unfolding dRot_if
    by (smt (verit, best) field_sum_of_halves frac_ge_0 frac_lt_1) (*1.3 sec*)
qed

(*dissected proof*)
lemma  shows "dRot x y \<le> (dRot x z) + (dRot z y)"
proof(cases "\<bar>frac x - frac z\<bar> \<le> 1 / 2")
  case c1: True
  show ?thesis
  proof(cases "\<bar>frac x - frac y\<bar> \<le> 1 / 2")
    case c2: True
    show ?thesis
    proof(cases "\<bar>frac z - frac y\<bar> \<le> 1 / 2")
      case True
      show ?thesis
        unfolding dRot_if if_P[OF c1] if_P[OF c2] if_P[OF True]   
        by auto
    next
      case False
      show ?thesis
        unfolding dRot_if if_P[OF c1] if_P[OF c2] if_not_P[OF False]   
        using c2 by linarith
    qed
  next
    case c2: False
    show ?thesis
    proof(cases "\<bar>frac z - frac y\<bar> \<le> 1 / 2")
      case True
      show ?thesis
        unfolding dRot_if if_P[OF c1] if_not_P[OF c2] if_P[OF True]   
        using c2 by linarith
    next
      case False
      show ?thesis
        unfolding dRot_if if_P[OF c1] if_not_P[OF c2] if_not_P[OF False]   
        using c2 by linarith  
    qed
  qed
next
  case c1: False
  show ?thesis
  proof(cases "\<bar>frac x - frac y\<bar> \<le> 1 / 2")
    case c2: True
    show ?thesis
    proof(cases "\<bar>frac z - frac y\<bar> \<le> 1 / 2")
      case True
      show ?thesis
        unfolding dRot_if if_not_P[OF c1] if_P[OF c2] if_P[OF True]   
        using c2 by linarith
    next
      case False
      show ?thesis
        using dRot_min[of z y] dRot_min[of x z]
        unfolding dRot_if if_not_P[OF c1] if_P[OF c2] if_not_P[OF False]
        using c2 by linarith
    qed
  next
    case c2: False
    show ?thesis
    proof(cases "\<bar>frac z - frac y\<bar> \<le> 1 / 2")
      case True
      show ?thesis
        unfolding dRot_if if_not_P[OF c1] if_not_P[OF c2] if_P[OF True]   
        using c2 by linarith
    next
      case False
      show ?thesis
        using dRot_min[of z y] dRot_min[of x z] dRot_max[of x y]
        unfolding dRot_if if_not_P[OF c1] if_not_P[OF c2] if_not_P[OF False]   
        by linarith   
    qed
  qed
qed

global_interpretation msui: Metric_space \<U> dRot
proof
  show " 0 \<le> dRot x y" and "dRot x y = dRot y x" for x y
    unfolding circle_distance_def by simp_all
  show "(dRot x y = 0) = (x = y)" if "x \<in> \<U>" "y \<in> \<U>" for x y
  proof
    assume "x = y"
    thus "dRot x y = 0"
      unfolding circle_distance_def by simp
  next 
    assume "dRot x y = 0"
    hence "frac x = frac y"
      unfolding circle_distance_def min_def 
      using frac_diff_zero by metis
    thus "x = y"
      using that 
      unfolding unit_interval_set_def mem_Collect_eq frac_eq[symmetric]
      by simp
  qed
  show "dRot x y \<le> dRot x z + dRot z y" for x y z
    using dRot_triang.
qed


section \<open>Real interval as a quotient type\<close>

definition frac_equiv where
   "frac_equiv a b \<equiv> frac a = frac b"

quotient_type qrui = "real" / "\<lambda> x y. frac x = frac y"
  by (rule equivpI, unfold reflp_def symp_def transp_def)
   simp_all

instantiation qrui ::  "ab_group_add" 
begin
lift_definition zero_qrui :: qrui is 0.
lift_definition plus_qrui :: "qrui \<Rightarrow> qrui \<Rightarrow> qrui" is "\<lambda> x y. frac (x + y)"
  by (simp add: frac_add)
lift_definition uminus_qrui :: "qrui \<Rightarrow> qrui" is "uminus"
  using frac_in_Ints_iff frac_neg qrui_equivp by metis
lift_definition minus_qrui :: "qrui \<Rightarrow> qrui \<Rightarrow> qrui" is "\<lambda> x y. frac (x - y)"
  unfolding frac_frac frac_diff by fastforce

instance
proof
  show " a + b = b + a" for a b :: qrui 
    by (simp add: add.commute plus_qrui_def)
qed (transfer, simp add: add.assoc)+

end

find_theorems(46) name: qrui

end