# IRC log for #isabelle, 2017-06-29

All times shown according to UTC.

Time Nick Message
00:28 keep_learning joined #isabelle
01:48 ilbot3 joined #isabelle
01:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
07:27 wagle joined #isabelle
10:05 Merv__ joined #isabelle
10:06 Merv_ joined #isabelle
14:15 Merv_ joined #isabelle
16:33 chindy If I want to reason with about vectors without specifing the dimension except that it has to be finite and non 0. How would one go about this?
16:36 chindy I tried with locales and a carrier set that is an ordered_euclidean_space but that does not entail the ordering that i need (specifically the one defined in Cartesian_Euclidean_Space.thy)
16:39 pruvisto what ordering do you need?
16:39 chindy x ≤ y ⟷ (∀i. x\$i ≤ y\$i)
16:39 pruvisto real vector space with positive finite dimension sounds like euclidean_space
16:41 chindy pruvisto: yea thats what i thought/have... but as i said i am missing the order
16:41 pruvisto why
16:41 pruvisto (?x ≤ ?y) = (∀i∈Basis. ?x ∙ i ≤ ?y ∙ i)
16:41 pruvisto this holds for the Euclidean space
16:42 chindy okay... maybe i mussunderstand an error message: Variable 'a::euclidean_space not of sort ord
16:42 pruvisto you probably have to import Ordered_Euclidean_Space or something
16:43 pruvisto but you should import "Analysis" anyway when you use something from HOL-Analysis
16:43 chindy I importet analysis
16:43 chindy ...
16:43 pruvisto oh yes you need ordered_euclidean_space
16:43 pruvisto not euclidean_space
16:45 chindy Ah... im an idiot thanks. I had ordered_euc... before but in the lemma i did not specify the type to be of ord_euc...
16:45 chindy Thanks!
17:25 chindy is there a syntactically nice way for definitions in locales?
17:54 chindy Lets say i have a locale called abstract_somoneorder  that has a carrier set and a relation. Now I want to reason about an instance of abstract_order where the carrier set is of type 'a::ordered_euclidean_space how do i go about that? Do i have to instanciate abstract_someorder or can i create another locale called someorder_with_ordered_eucl_space somehow
18:44 dmiles joined #isabelle
18:46 dmiles joined #isabelle
21:14 dmiles joined #isabelle
21:15 dmiles joined #isabelle
22:52 chindy to be more precise... I have a locale with a carrier of type 'a set and now i want to say if that 'a is of type euclidean_space we can do .....