# IRC log for #isabelle, 2017-07-07

All times shown according to UTC.

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