Time 
Nick 
Message 
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/ 
03:07 

keep_learning joined #isabelle 
06:38 

cmr joined #isabelle 
06:38 

cmr joined #isabelle 
06:59 

Merv_ joined #isabelle 
06:59 

Merv_ joined #isabelle 
09:56 

dmiles joined #isabelle 
11:10 

silver joined #isabelle 
17:06 

cmr joined #isabelle 
17:06 

cmr joined #isabelle 
19:12 

Merv_ joined #isabelle 
20:10 
qwertyyyy 
when I want to prove somethin like this : theorem "¬(∀xs . length xs = (5::nat))" 
20:10 
qwertyyyy 
I would assume the not negated theorem and basically do what quickcheck does (finding a counterexample) 
20:11 
qwertyyyy 
but I can't use "rule allE" like this : 
20:11 
pruvisto 
you first have to do "rule notI" 
20:11 
pruvisto 
or just "apply safe" 
20:12 
pruvisto 
that should get rid of the negation and the universal quantifier 
20:12 
qwertyyyy 
ok I will immediatelly try it , thank you :) 
20:12 
pruvisto 
in fact, I would probably just prove "length [] ≠ 5" and then, using that, "show ?thesis by blast" 
20:12 
pruvisto 
and let "blast" take care of the logical stuff 
21:52 

Merv__ joined #isabelle 
22:04 
qwertyyyy 
ok that works fine :) 
22:04 
qwertyyyy 
I still have some questions 
22:04 
qwertyyyy 
you can't just do the following : 
22:07 
qwertyyyy 
assume "∀xs. length xs = (5::nat)" 
22:07 
qwertyyyy 
hence "length someTing = (5::nat)" by (rule allE) 
22:07 
qwertyyyy 
it does't really tell my why ... but I think it has a problem with the types ... 
22:23 
pruvisto 
correct 
22:23 
pruvisto 
you need to annotate a type 
22:23 
pruvisto 
assume "∀xs. length xs = 5" 
22:24 
pruvisto 
err 
22:24 
pruvisto 
assume "∀xs::'a list. length xs = 5" 
22:24 
pruvisto 
hence "length (someTing :: 'a list) = 5" by (rule allE) 
22:24 
pruvisto 
that works 
22:24 
pruvisto 
note that you don't need that "nat" annotation since "length" has the return type nat anyway 
22:46 
qwertyyyy 
so would this: theorem "¬(∀xs. length (xs::'a list) = 5)" 
22:47 
qwertyyyy 
and the theorem from above cosidered to be the same ? theorem "¬(∀xs . length xs = 5) 
22:50 
pruvisto 
yes 
22:51 
pruvisto 
the type checking introduces free type variables if you don't annotate them 
23:51 

silver joined #isabelle 