Time 
Nick 
Message 
02:47 

ilbot3 joined #isabelle 
02:47 

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/ 
02:54 

vanila joined #isabelle 
02:54 
vanila 
hi 
02:54 
vanila 
would isabelle be good for working with modular arithmetic? 
02:55 
vanila 
just to do basica number theory stuff for example 
02:55 
vanila 
im more familiar with coq and I know that doing that is very hard there 
03:02 
tangentstorm 
probably, vanila 
03:03 
tangentstorm 
do you have an example of a proof you might want to attempt? 
03:03 
vanila 
stuff like bezouts theorem (given coprime a,b exists x,y with ax+by = 1) 
03:03 
vanila 
fermats little theorem x^p = x mod p 
03:04 
tangentstorm 
hold please 
03:04 
vanila 
squares mod p 
03:06 
tangentstorm 
there is a mod_type here but i don't yet understand it myself: http://afp.sourceforge.net/browser_info/devel/HOL/HOLWord/Numeral_Type.html 
03:08 
tangentstorm 
not exactly pretty. 
03:10 
vanila 
well i'd like to define it myself from scratch 
03:10 
vanila 
i can use this as reference though 
03:10 
tangentstorm 
it sounds like a fun problem. 
03:10 
vanila 
I guess the best thing is to just dive in 
03:11 
tangentstorm 
i'm still basically a beginner. the nice thing i like about isabelle compared to other systems is the declarative language: 
03:12 
tangentstorm 
https://github.com/tangentstorm/tangentlabs/blob/master/isar/Exponents.thy 
03:12 
vanila 
oh yeah that's interesting! looks nice and readable 
03:12 
tangentstorm 
if you can express your proof as a series of rewrites then you can almost surely prove it in isar. i just don't have the math chops to know how yet. 
03:13 
tangentstorm 
some of these other folks in here are much better, but probably asleep :) 
03:20 
tangentstorm 
vanila: http://isabelle.in.tum.de/repos/isabelle/file/d3996d5873dd/src/HOL/Number_Theory/Primes.thy 
03:20 
tangentstorm 
(see also other things in that directory) 
03:22 
vanila 
ah! 
03:22 
vanila 
looks like they use latex for operators 
03:22 
vanila 
i guess there's an emacs mode or something thath displays it? 
03:22 
tangentstorm 
also http://isabelle.in.tum.de/repos/isabelle/file/d3996d5873dd/src/HOL/GCD.thy#l1524 bezout's theorem 
03:22 
vanila 
i use proof general before 
03:22 
vanila 
oh this is super ill reference these a bunch thanks a lot 
03:22 
tangentstorm 
no you use a custom gui that comes with it. it's very nice. 
03:23 
vanila 
oh i see! 
03:23 
tangentstorm 
it'll turn all that latex junk into pretty symbols for you, and color code the lines of your proof as you go along. 
03:25 
tangentstorm 
http://www.concretesemantics.org/ is about writing proofs of functional programs, but the first part makes for a nice general intro to isabelle/isar and the gui 
03:26 
vanila 
ill power through part 1 and then get started then, thanks again :) 
03:27 
tangentstorm 
np. let us know how it goes. i'd love to see a beginner friendly version. 
03:28 
vanila 
sure! 
10:13 
JCaesar 
There used to be an emacs "mode"… 
18:25 

wagle joined #isabelle 
18:27 

inte joined #isabelle 
18:27 

lispy joined #isabelle 
23:32 
JCaesar 
Say, is there some kind of defaultdefined record constructor? i.e. one that is just a plain function without any syntactic sugar. 
23:49 
larsrh 
JCaesar: try foobar.make 
23:50 
JCaesar 
ty. 