[isabelle] Strange behaviour. Errors depend on file length.



Hello everybody.

Enclosed please find two files: Example1.thy and Example2.thy.

---------------------------------------------------------------

The Example1.thy produces the following error:

*** Outer syntax error (line 55 of 
"/home/andrzej/ALMAMER/PUBLIKACJE/DESIGN_PATTERNS/Isabelle/Example1.thy"): 
command expected,
*** but identifier type_synonim (line 55 of 
"/home/andrzej/ALMAMER/PUBLIKACJE/DESIGN_PATTERNS/Isabelle/Example1.thy") was 
found

just before the following lines

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

---------------------------------------------------------------

The Example2.thy file is processed without errors.

The Example2.thy is the Example1.thy with a number of lines deleted. It can be 
easily checked with (on linux):
diff Example2.thy Example1.thy

Sorry for bothering you but I really do not understand the behavior.

I use linux computer with 64 bit kubuntu distribution with 1GB ram and 1GB 
swap. 64 bit OpenSuse 11.3 with 8GB ram gives identical results.

Thanks for help.
Regards
Andrzej Mazurkiewicz
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

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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.