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 HOLAnalysis 
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 ..... 