Time 
Nick 
Message 
01:17 

silver 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/ 
06:08 
pruvisto 
chindy: well, for every positive integer n there is a type n with exactly n elements from 0 to n  1 
06:08 
pruvisto 
internally, e.g. "5" is just syntactic sugar for 1 bit1 bit0 bit1 
06:09 
pruvisto 
where "typedef 1 = "{0::nat}"" 
06:09 
pruvisto 
and if 'a is a type with n elements, 'a bit0 is a type with 2*n elements and 'a bit1 is a type with 2*n+1 elements 
06:10 
pruvisto 
and "('a, 'b)" vec is essentially a type copy of "'b ⇒ 'a" 
06:11 
pruvisto 
so if you have a "('a, 3) vec", that's essentially a function that maps any element of the type 3 (i.e. 0, 1, 2) to an element of type 'a 
06:11 
pruvisto 
and that's pretty much the essence of a vector w.r.t. a standard basis 
07:38 

aneas joined #isabelle 
11:26 

silver joined #isabelle 
13:03 
larsrh 
so I tuned the function package to give me exactly the things I need and all so that my tactic will be deterministic and really clean and cool 
13:03 
larsrh 
turns out the dumb thing (nondeterministically applying congruence rules) works far better 
13:40 
larsrh 
I am very tempted to call this thing dumb_tac 
13:50 
JCaesar 
Come up with some cool backronym, and it's on. 
13:51 
JCaesar 
determinismunaware modification builder. 
13:51 
JCaesar 
mmmmh. 
15:14 
pruvisto 
larsrh: so what did you do in the end? 
15:15 
pruvisto 
I for one spent pretty much the entire day proving something completely obvious 
18:15 
larsrh 
pruvisto: a terrible REPEAT_ALL_NEW thingy which just resolve_tacs ALL THE CONGRUENCE RULES 
18:15 
pruvisto 
larsrh: no I mean what did you improve w.r.t. the function package? 
18:16 
larsrh 
only a tiny bit: I generalised the signature of the code which descends a rhs of a function definition and figures out recursive calls 
18:16 
larsrh 
I had another combinator which helped traversing this tree but in the end it was too simplistic 
18:16 
larsrh 
so I didn't push it 
18:17 
larsrh 
the problem, in a nutshell: if you have mutually recursive definitions, that code in the function package assumes that the terms you shove into it already assumes that you have the Inl/Inr representation 
18:17 
larsrh 
but I don't have that, so it was useless for me 
18:18 
larsrh 
and I couldn't be bothered to figure out where exactly that code that does that transformation lies 
18:18 
larsrh 
*lives 
18:18 
larsrh 
in an ideal world this tree structure would obviously be in function_info 