Time 
Nick 
Message 
00:38 
qwertyyyy 
ok I still have a problem with this one here 
00:38 
qwertyyyy 
theorem "¬(∀zs x y u v ::'a list . replace x y (replace u v zs) = replace u v (replace x y zs))" 
00:39 
qwertyyyy 
replace replaces every occurrence of the secend argument in the list with the first one 
00:39 
qwertyyyy 
so my problem is that I can't turn a specific example into a general statement 
00:40 

aindilis joined #isabelle 
00:40 
qwertyyyy 
for example this one "proves" that the theorem is true (or at least I think it is): 
00:40 
qwertyyyy 
" replace (3::nat) (2::nat) (replace (2::nat) 1 [1]) ≠ replace 2 1 (replace 3 2 ([1]::nat list))" 
00:41 
qwertyyyy 
but the problem is that I can't "nat" into "'a" (which makes sense , of course ) 
00:42 
qwertyyyy 
so I really have to find a more general "example" (with type 'a instead of nat), right ? 
00:43 
qwertyyyy 
or is there a way to make this happen (turning/using the nat example to prove the general statement)? 
07:40 
inte 
qwertyyyy: well that statement is false if 'a has only 1 or 2 distinct values. (you can think of 'a as being implicitly universally quantified) 
07:53 
inte 
http://downthetypehole.de/paste/wKnYbACo are the two things you can prove. note that the second lemma shows that you cannot prove what you want for arbitrary types. (the assumption does hold for the unit type, as shown by the third lemma) 
07:57 
inte 
You can get from nat to 'a using the `map` function, of course, but you'd need an injective map from {1,2,3} to 'a for the counterexample to carry over to 'a. 
09:56 
pruvisto 
also note that in practice, you very rarely have to prove things like that 
14:59 
JCaesar 
I think I have a funny proof like that somewhere in the AFP… 
15:19 

silver joined #isabelle 
18:24 

logicmoo joined #isabelle 
19:27 
qwertyyyy 
ok thank you all very much :) 
19:28 
qwertyyyy 
but I have still two "tiny" questions ... sorry 
19:28 
qwertyyyy 
I don't quite get what \<equiv> means ... for example in atomize_imp 
19:29 
qwertyyyy 
the simplifier uses it to rewrite but when I try to naivly try to rewrite something with this using "subst" it won't work 
19:30 
qwertyyyy 
the other question is : what is the type of types in isabelle ... sort , set , or something else ? 
19:30 
pruvisto 
\<equiv> is metaequality, = is objectlogic equality 
19:31 
pruvisto 
basically, Isabelle's core knows only a very basic metalogic consisting only of the metauniversal quantifier (the big ∧), metaimplication (⟹) a, and metaequality 
19:31 
pruvisto 
and the object logic HOL is axiomatised on top of that 
19:32 
pruvisto 
It's desecribed… somewhere in the Isabelle documenttation 
19:32 
pruvisto 
and there is no type of types in Isabelle 
19:32 
inte 
There is a concept of sorts for type classes though. 
19:33 
pruvisto 
Isabelle is not dependently typed; terms and types or something completely different 
19:33 
pruvisto 
*are 
19:33 
pruvisto 
terms can have types, and types are either a variable or a type constructor with a certain arity 
19:34 
pruvisto 
but unlike in Haskell, an unapplied type constructor in Isabelle is not a type 
19:34 
pruvisto 
so you can't just write "list" and expect that to be a type, only "'a list" is a type 
19:35 
pruvisto 
types can have sorts, which are a bit like Type classes in Haskell 
20:39 
qwertyyyy 
ok thank you both again :) 
23:18 

dmiles joined #isabelle 
23:36 
JCaesar 
the white one? 
23:36 
JCaesar 
or the one in the ceiling? 
23:36 
JCaesar 
eh… 
23:36 
JCaesar 
wrong channel… 
23:43 
JCaesar 
what I wanted to say was: qwertyyyy: subst can only be applied to the conclusion or single assumptions. i.e. you can do lemma "(A ==> B) ==> C" apply(subst (asm) atomize_imp). 
23:44 
JCaesar 
otherwise, there's simp add: atomize_imp 