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)"

type_synonim StateFun = "Moment \<Rightarrow> PositiveReal0"

(* For subsystems that are simply switched on/off and if operating,
   they are doing it at nominal yield.
   Simple operations are such subsystems
 *)

type_synonim State1Fun = "Moment \<Rightarrow> bool"

typedef FiniteNatSet = "{x::nat. EX y::nat. (x <= y)}"
apply(auto)
done

(* BEGIN by Brian Huffman *)

definition  assocs :: "('a ~=> 'b) => ('a * 'b) set"
where "assocs m = {(x, y). m x = Some y}"


definition "RangeSum m = (SUM (x,y) : assocs m. y)"

lemma assocs_empty: "assocs empty = {}"
   unfolding assocs_def by simp

lemma assocs_upd: "assocs (m(a |-> b)) = insert (a, b) {x : assocs m.  
fst x ~= a}"
   unfolding assocs_def by (auto split: if_splits)

lemma rangeSum0: "RangeSum (map_of [(x, 1)]) = 1"
unfolding RangeSum_def by (simp add: assocs_upd assocs_empty)

(* END by Brian Huffman *)

(* lemma map0: "map_of [(x, 1)] = [x |-> 1]"
apply(auto)
done

lemma map1: "[x |-> 1] = map_of [(x, 1)]"
apply(auto)
done
*)

lemma rangeSum1: "RangeSum ([x |-> 1]) = 1"
unfolding RangeSum_def
apply(simp add: assocs_upd)
apply(simp add: assocs_empty)
done

record Gen1ParData =
  breedingOpGap :: TimeDur

(* other needed primitives *)
(* Crop is a plant growing on a certain field according to a certain technology.
*)

type_synonim "Crop" = FiniteNatSet

record CropData =
    areaSubvention :: Money0

type_synonim "Crops" = "Crop ~=> CropData"

type_synonim CropRotation = "(Crop \<times> Crop) set"

(* Fixed resources *)
(* fields *)

type_synonim Field = FiniteNatSet

record FieldData =
  area :: PositiveReal
  tax_rent_per_unit :: Money0
  crops :: Crops
  cropRotGr :: CropRotation

type_synonim "Fields" = "Field ~=> FieldData"

(* machines *)

type_synonim "Machine" = FiniteNatSet

record MachineData =
    numberAtDisposal :: PositiveNat
    costPerHour :: Money0

type_synonim Machines = "Machine ~=> MachineData"

type_synonim NecessMachines = "Machine multiset"

type_synonim MachinesHours = "Machine ~=> PositiveReal0"

(* animals stands *)

type_synonim AnimalStandsResource = FiniteNatSet

record AnimalStandsData =
   amountAtDisposal :: PositiveReal
   usageCost_Month_Unit :: Money

type_synonim AnimalStands = "AnimalStandsResource ~=> AnimalStandsData"

(* labor power *)

type_synonim "Worker" = FiniteNatSet

type_synonim "Skill" = FiniteNatSet

type_synonim "NecessSkills" = "Skill multiset"

type_synonim "LaborPower" = "Worker \<times> Skill"

(* Reources "consumed" and "produced". *)

type_synonim ConsumMaterial = FiniteNatSet

type_synonim MaterialQuantity = "ConsumMaterial ~=> PositiveReal"

type_synonim Service = FiniteNatSet
type_synonim ServiceQuantity = "Service ~=> PositiveReal"

type_synonim Animal = FiniteNatSet
type_synonim Animals = "Animal set"
type_synonim AnimalGroup = FiniteNatSet
type_synonim Animal2GroupMap = "Animal ~=> AnimalGroup"
type_synonim AnSeasonalityMap = "AnimalGroup ~=> bool"

type_synonim AnimalRotGr = "(Animal \<times> Animal) set"

record AnimalsRec =
   animals :: Animals
   anGrM :: Animal2GroupMap
   seasonality :: AnSeasonalityMap
   rotGr :: AnimalRotGr

definition animalsWithinGroup :: "Animals => Animal2GroupMap => bool"
where "animalsWithinGroup ans anGr == card(anGr ` ans) = 1"

(*
definition ex1AnimalGroupM ::Animal2GroupMap
where "ex1AnimalGroupM == [(Abs_FiniteNatSet 0) \<mapsto> (Abs_FiniteNatSet 0)] ++ [(Abs_FiniteNatSet 1) \<mapsto> (Abs_FiniteNatSet 0)]"

definition ex1AnSeasonalityMap :: AnSeasonalityMap
where "ex1AnSeasonalityMap == [(Abs_FiniteNatSet 0) \<mapsto> False]"

definition ex1AnimalRotGr :: AnimalRotGr
where "ex1AnimalRotGr == {(Abs_FiniteNatSet 0, Abs_FiniteNatSet 1), (Abs_FiniteNatSet 1, Abs_FiniteNatSet 0)}"
*)

definition ex1AnimalsRec :: AnimalsRec
where "ex1AnimalsRec == \<lparr> animals = {Abs_FiniteNatSet 0, Abs_FiniteNatSet 1},
                         anGrM = [(Abs_FiniteNatSet 0) \<mapsto> (Abs_FiniteNatSet 0)]
                                 ++ [(Abs_FiniteNatSet 1) \<mapsto> (Abs_FiniteNatSet 0)],
                         seasonality = [(Abs_FiniteNatSet 0) \<mapsto> False],
                         rotGr = {(Abs_FiniteNatSet 0, Abs_FiniteNatSet 1),
                                  (Abs_FiniteNatSet 1, Abs_FiniteNatSet 0)} \<rparr>"

lemma ex1AnimalsRec_lemma0 [simp]:
" a = Abs_FiniteNatSet 0 \<and> b = Abs_FiniteNatSet (Suc 0)
\<Longrightarrow> animalsWithinGroup {a, b}
     [Abs_FiniteNatSet 0 \<mapsto> Abs_FiniteNatSet 0, Abs_FiniteNatSet (Suc 0) \<mapsto> Abs_FiniteNatSet 0]"
unfolding animalsWithinGroup_def
unfolding card_def
apply(auto)
done

lemma ex1AnimalsRec_lemma1 [simp]:
"a = Abs_FiniteNatSet (Suc 0) \<and> b = Abs_FiniteNatSet 0
\<Longrightarrow>  animalsWithinGroup {a, b}
     [Abs_FiniteNatSet 0 \<mapsto> Abs_FiniteNatSet 0, Abs_FiniteNatSet (Suc 0) \<mapsto> Abs_FiniteNatSet 0]"
unfolding animalsWithinGroup_def
unfolding card_def
apply(auto)
done

lemma ex1AnimalsRec_lemma2 [simp]:
"\<forall> a b. (a, b) \<in> rotGr ex1AnimalsRec \<Longrightarrow> a = Abs_FiniteNatSet 0 \<and> b = Abs_FiniteNatSet (Suc 0) \<or> a = 
Abs_FiniteNatSet (Suc 0) \<and> b =  Abs_FiniteNatSet 0 "
unfolding ex1AnimalsRec_def
apply(auto)
done

lemma ex1AnimalsRec_lemma3 [simp]:
" a = Abs_FiniteNatSet 0 \<and> b = Abs_FiniteNatSet (Suc 0)
   \<or> a = Abs_FiniteNatSet (Suc 0) \<and> b =  Abs_FiniteNatSet 0
\<Longrightarrow> animalsWithinGroup {a, b}
     [Abs_FiniteNatSet 0 \<mapsto> Abs_FiniteNatSet 0, Abs_FiniteNatSet (Suc 0) \<mapsto> Abs_FiniteNatSet 0]"
apply(auto)
done


lemma ex1AnimalsRec_lemma4 [simp]:
"\<forall> a b. (a, b) \<in> rotGr ex1AnimalsRec \<Longrightarrow> animalsWithinGroup {a, b} (anGrM ex1AnimalsRec)"
unfolding ex1AnimalsRec_def
apply(auto)
done

(* obrót zwierzętami może być wyłącznie w ramach grupy *)

typedef AnimalsData = "{x::AnimalsRec. 
     \<forall> (y1, y2) \<in> (rotGr x). (animalsWithinGroup {y1, y2} (anGrM x))}"
apply(rule_tac x = ex1AnimalsRec in exI)
unfolding ex1AnimalsRec_def
unfolding animalsWithinGroup_def
apply(simp_all)
done



type_synonim AnimalsAmount = "Animal ~=> PositiveReal"

type_synonim AnimalsShareRec = "Animal ~=> real"

(* necessary for the typedef AnimalsShare *)
definition simpleAnSh :: AnimalsShareRec where
  "simpleAnSh == [(Abs_FiniteNatSet 0) |-> 1::real]"

(* necessary for the typedef AnimalsShare *)
lemma simpleAnSh0: "RangeSum simpleAnSh = 1"
unfolding simpleAnSh_def
apply(simp add: rangeSum1)
done

typedef AnimalsShare = "{x::AnimalsShareRec. (RangeSum x) = 1 \<and> (\<forall> y \<in> (ran x). ((y > 0) \<and> (y <= 1)))}"
apply(rule_tac x = simpleAnSh in exI)
apply(simp add: rangeSum1)
apply(simp add: simpleAnSh0)
unfolding ran_def
unfolding simpleAnSh_def
apply(auto)
done

(* fixed resources assemblies *)

(* technological operations *)

record SimpleTechnOpData =
   duration :: TimeDur
   machines :: NecessMachines
   skills :: NecessSkills
   materialsConsumption :: MaterialQuantity
   serviceConsumption :: ServiceQuantity
   materialProduction :: MaterialQuantity
   serviceProduction :: ServiceQuantity

type_synonim SimpleTechnOps = "SimpleTechnOpData set"

type_synonim SimpleTechnOpsStateVec = "SimpleTechnOps \<Rightarrow> State1Fun"

(* record SeasBreedOpData = AseasBreedOpData +
   startT :: Moment *)

record SeasBreedOpData =
   duration :: TimeDur
   inputAnimal :: Animal
   outputAnimals :: AnimalsShare
   animalsBiths :: AnimalsAmount
   standsOccupied :: AnimalStandsResource
   standSizeOccupied :: PositiveReal
   machinesHours_perDay :: MachinesHours
   materialsConsuption :: MaterialQuantity
   serviceConsumption :: ServiceQuantity
   materialProduction :: MaterialQuantity
   startT :: Moment

type_synonim SeasBreedOps = "SeasBreedOpData set"

type_synonim SeasBreedOpsStateVec = "SeasBreedOps \<Rightarrow> PositiveReal0"

(* na razie nie używane *)
definition seasOpNext1 :: "SeasBreedOpData => TimeDur => SeasBreedOpData"
where "seasOpNext1 so td == so (| startT := (startT so) +c td |)"

instantiation Moment :: zero
begin

definition Zero_Moment_def [code func del]:
  "0 = Abs_Moment (Abs_Nat (Zero_Rep))"

instance ..

end

definition Sucm :: "Moment => Moment"
where "Sucm m == Abs_Moment (1 + (Rep_Moment m))"

(* cultivation measures *)

record CultivationMeasureData =
   durationPerAreaUnit :: TimeDur
   earliestStart :: Moment
   acceptiblePeriodDuration :: TimeDur
   machines :: NecessMachines
   skills :: NecessSkills
   materialsConsumption :: MaterialQuantity
   serviceConsumption :: ServiceQuantity
   materialProduction :: MaterialQuantity

type_synonim CropTechnology = "FiniteNatSet ~=> CultivationMeasureData"
type_synonim CropsTechnologies = "Crop ~=> CropTechnology"

(* teraz warunki zakupu i warunki sprzedaży oraz limity *)

record SimplePriceCond =
   price :: Money
   validSince :: Moment
   pCDduration :: TimeDur

type_synonim PriceConds = "SimplePriceCond set"

record ContractRec =
   lowerLimit :: PositiveReal0
   upperLimit :: PositiveLimit
   priceConds :: PriceConds

lemma b [simp]: "upperLimit (| lowerLimit = a, upperLimit = b, priceConds = c |) = b"
apply(simp)
done

definition exampleContract :: ContractRec where
  "exampleContract == (| lowerLimit = (Abs_PositiveReal0 0), upperLimit = Infinity, priceConds = {}|)"

lemma c [simp]: "lowerLimit exampleContract = (Abs_PositiveReal0 0)"
apply(simp add: exampleContract_def)
done

lemma d [simp]: "upperLimit exampleContract = Infinity"
apply(simp add: exampleContract_def)
done

lemma e: "le2 (lowerLimit exampleContract) (upperLimit exampleContract)"
apply(auto)
done

typedef Contracts = "{x::ContractRec. le2 (lowerLimit x) (upperLimit x)}"
apply(rule_tac x = exampleContract in exI)
by simp

type_synonim ContractSet = "ContractRec set"
type_synonim ContractSetSet = "ContractSet set"

type_synonim AnimalsSellingConds = "Animal ~=> ContractSetSet"
type_synonim MaterialsSellingConds = "ConsumMaterial ~=> ((ContractSet) set)"
type_synonim ServicesSellingConds = "Service ~=> ((ContractSet) set)"

type_synonim AnimalsPurchaseConds = "Animal ~=> ((ContractSet) set)"
type_synonim MaterialsPurchaseConds = "ConsumMaterial ~=> ((ContractSet) set)"
type_synonim ServicesPurchaseConds = "Service ~=> ((ContractSet) set)"

record FarmData =
   field_s :: Fields
   machines :: Machines
   animalStands :: AnimalStands
   cropsTechnologies :: CropsTechnologies
   seasBreedOps :: SeasBreedOps
   ansSellConds :: AnimalsSellingConds
   matsSellConds :: MaterialsSellingConds
   servSellConds :: ServicesSellingConds
   anPurchConds :: AnimalsPurchaseConds
   matsPurchConds :: MaterialsPurchaseConds
   servPurchConds :: ServicesPurchaseConds

(* Initial balance of the system *)
(* There is a mapping  between*)

(* Determining moments of change *)

definition genMomentsCirc :: "FarmData => Moment set"
where "genMomentsCirc fd == {x::Moment. \<exists> y::SeasBreedOpData \<in> (seasBreedOps fd).
                                  (startT y = x)
                               \<or> ((startT y) +c (duration y) = x)}
                 \<union> {x::Moment. \<exists> ct::CropTechnology \<in> ran (cropsTechnologies fd). \<exists> cm \<in> (ran ct).
                               ((earliestStart cm) = x)
                               \<or> ((earliestStart cm) +c (acceptiblePeriodDuration cm) = x)}
                 \<union> {x::Moment. \<exists> asc::ContractSetSet \<in> (ran (ansSellConds fd)
                                                          \<union> ran (matsSellConds fd)
                                                          \<union> ran (servSellConds fd)
                                                          \<union> ran (anPurchConds fd)
                                                          \<union> ran (matsPurchConds fd)
                                                          \<union> ran (servPurchConds fd)).
                                          \<exists> cs::ContractSet \<in> asc.
                                          \<exists> cr::ContractRec \<in> cs.
                                          \<exists> spc::SimplePriceCond \<in> (priceConds cr).
                              (x = (validSince spc)) \<or> (x = (validSince spc) +c (pCDduration spc))}"


end