theory Unit_Interval_Group 
  imports Fractional_Part_Arithmetic
          "HOL-Algebra.Ring"   

begin

section \<open>Unit interval as Abelian group\<close>

definition unit_interval_set :: "'a::floor_ceiling set" ("\<U>")
where "unit_interval_set = {x. 0 \<le> x \<and> x < 1}"

definition ui_plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a::floor_ceiling"
where "ui_plus a b = frac (a + b)"

definition ui_minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a::floor_ceiling"
where "ui_minus a b = frac (a - b)"

definition ui_uminus :: "'a \<Rightarrow> 'a::floor_ceiling"
where "ui_uminus a = 1 - frac a"

abbreviation unit_interval :: "'a::floor_ceiling ring" ("\<UU>")
  where "unit_interval \<equiv> \<lparr>carrier = \<U>, mult = (*), one = 1, zero = 0, add = ui_plus \<rparr>"

interpretation fracs: abelian_group "\<UU> :: 'a::floor_ceiling ring" 
proof-    
  have all_units: "Units (add_monoid \<UU>) = (\<U> :: 'a ::  floor_ceiling set)"
  proof
    show "\<U> \<subseteq> Units (add_monoid (\<UU> :: 'a::floor_ceiling ring))"
    proof
      fix x :: "'a :: floor_ceiling"
      assume "x \<in> \<U>"
      show "x \<in> Units (add_monoid \<UU>)"
      proof (cases "x = 0")
        assume "x = 0"
        show "x \<in> Units (add_monoid \<UU>)"
          unfolding \<open>x = 0\<close> Units_def ui_plus_def unit_interval_set_def          
          by force
      next 
        assume "x \<noteq> 0"
        show "x \<in> Units (add_monoid \<UU>)"
          unfolding Units_def ui_plus_def unit_interval_set_def 
          partial_object.select_convs monoid.select_convs ring.select_convs
        proof (rule CollectI, rule conjI)  
          show "\<exists>xa\<in>{x. 0 \<le> x \<and> x < 1}. frac (xa + x) = 0 \<and> frac (x + xa) = 0"
          proof
            show "1 - x \<in> {x. 0 \<le> x \<and> x < 1}"
              using \<open>x \<in> \<U>\<close> \<open>x \<noteq> 0\<close> unfolding unit_interval_set_def by auto
            show "frac (1 - x + x) = 0 \<and> frac (x + (1 - x)) = 0"
              using \<open>x \<in> \<U>\<close> unfolding unit_interval_set_def by auto
          qed
      qed (use \<open>x \<in> \<U>\<close>[unfolded unit_interval_set_def] in blast)
    qed
  qed
  show "Units (add_monoid \<UU>) \<subseteq> \<U>"
    unfolding partial_object.select_convs Units_def by blast 
qed
  show "abelian_group (\<UU> :: 'a::floor_ceiling ring)"
    by (standard, unfold all_units, unfold ui_plus_def unit_interval_set_def) 
    (simp_all add: frac_eq frac_lt_1 add.assoc, simp add: add.commute)
qed

end