theory FarmUserModel
imports Main Multiset RealDef Map Finite_Set SetInterval
begin  

typedef PositiveReal = "{x::real. x > 0}"
apply(rule_tac x = 1 in exI)
by simp

typedef PositiveReal0 = "{x::real. x >= 0}"
apply(rule_tac x = 1 in exI)
by simp

definition le1 :: "[PositiveReal0, PositiveReal] => bool" where
  "(le1 x y) == ((Rep_PositiveReal0 x) <= (Rep_PositiveReal y))"

datatype PositiveLimit = Infinity | Limit1  PositiveReal

(* datatype 'a option = None | Some 'a   niepotrzebne - zaznacza, że dotąd dobrze *)

primrec  "le2" :: "[PositiveReal0, PositiveLimit] => bool" where
   "(le2 x Infinity) = True" |
   "(le2 x (Limit1 y)) = (le1 x y)"

typedef PositiveNat = "{x::nat. x> 0}"
apply(rule_tac x =1 in exI)
by simp

typedef Money = "{x::real. x > 0}"
apply(rule_tac x = 1 in exI)
by simp

typedef Money0 = "{x::real. x >= 0}"
apply(rule_tac x = 1 in exI)
by simp

typedef TimeDur = "{x::nat. x > 0 \<and> x <= 365}"
apply(rule_tac x = 1 in exI)
by simp

typedef Moment = "{x::nat. x >= 0 \<and> x < 365}"
apply(rule_tac x = 1 in exI)
by simp

definition add_m_td_circ :: "Moment => TimeDur => Moment"          (infixl "+c" 60)
where "add_m_td_circ m td == if ((Rep_Moment m) + (Rep_TimeDur td) < 365)
                        then Abs_Moment ((Rep_Moment m) + (Rep_TimeDur td))
                        else Abs_Moment ((Rep_Moment m) + (Rep_TimeDur td) - 365)"

definition mod_m_td :: "[Moment, TimeDur] \<Rightarrow> nat"
where "mod_m_td m td == ((Rep_Moment m) mod (Rep_TimeDur td))"

definition moment_eq :: "[Moment, Moment] => bool" where
  "(moment_eq x y) == (Rep_Moment x = Rep_Moment y)"

end