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

All times shown according to UTC.

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 int-e 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 int-e 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 int-e 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 meta-equality, = is object-logic equality
19:31 pruvisto basically, Isabelle's core knows only a very basic meta-logic consisting only of the meta-universal quantifier (the big ∧), meta-implication (⟹) a, and meta-equality
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 int-e 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