Re: [isabelle] ... finalement montrer False by blast



Funny how the Italian translation confuses blast with the explosion
principle (ex falso quodlibet).

Best regards, 

Andrei 

On 2/10/18, 12:13 PM, "cl-isabelle-users-bounces at lists.cam.ac.uk on behalf
of Makarius" <cl-isabelle-users-bounces at lists.cam.ac.uk on behalf of
makarius at sketis.net> wrote:

>Dear Isabelle users,
>
>as the peak of the carnival season is approaching, it is a good time to
>have latest deep learning technology produce some formal jokes for us
>(before the .ai bubble bursts).
>
>Presently the best translation service appears to be
>https://emea01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.dee
>pl.com%2Ftranslator&data=02%7C01%7Ca.popescu%40mdx.ac.uk%7C539e7d0fb4984fe
>1d4fe08d5707ff5bc%7C0774df91f25d43fe96e00a1d97632eea%7C0%7C0%7C63653861725
>1756779&sdata=kftRtnTv8%2BQbmpdFoRU%2BLLyPoIuwvJlIsqK%2BZkeO5VA%3D&reserve
>d=0 so lets see if it can turn Isar proofs
>into Coq (French) or Matita (Italian).
>
>
>Here are some bits from
>https://emea01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fisabelle
>.in.tum.de%2Frepos%2Fisabelle%2Fraw-file%2FIsabelle2017%2Fsrc%2FHOL%2FIsar
>_Examples%2FCantor.thy&data=02%7C01%7Ca.popescu%40mdx.ac.uk%7C539e7d0fb498
>4fe1d4fe08d5707ff5bc%7C0774df91f25d43fe96e00a1d97632eea%7C0%7C0%7C63653861
>7251756779&sdata=D2T%2F8adpt8AF2m5xoY4V8ncQzSwbU1V4FhbbEdFrD%2Bw%3D&reserv
>ed=0
>
>theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A.
>\<exists>x. A = f x"
>proof
>  assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x.
>A = f x"
>  then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A.
>\<exists>x. A = f x" ..
>  let ?D = "{x. x \<notin> f x}"
>  from * obtain a where "?D = f a" by blast
>  moreover have "a \<in> ?D \<longleftrightarrow> a \<notin> f a" by blast
>  ultimately show False by blast
>qed
>
>
>French:
>
>théorème Cantor:"¡<<nexistes>f::' a \<Rightarrow>' a set. C'est tout ce
>qui compte. Existe >x. A = f x"
>preuve
>  supposer "{<existe>f::' a \<Rightarrow>' a set. C'est tout ce qui
>compte. Existe >x. A = f x"
>  puis obtenez f:::"' a \<Rightarrow>' a set" où *:"\<<forall>A. Existe
>>x. A = f x"...
>  let? D = "{x. x \<notin> f x}"
>  à partir de * obtenir un où "? D = f a" par explosion
>  de plus ont "a \<in>? D \<<longleft à gauche flèche droite> a \<notin>
>f a" by blast
>  finalement montrer False by blast
>qed
>
>
>Italian:
>
>teorema Cantor:""<allegatoists>f::"a"<Rightarrow> "un set. "<forall>A.
>"<esiste>x. A = f x x".
>attestazione
>  assume ""<esiste>f::' a' a'"<Rightarrow>' un set. "<forall>A.
>"<esiste>x. A = f x x".
>  quindi ottenere f::"a"<Rightarrow>' a set "dove *:""<forall>A.
>"<esiste>x. A = f x"...
>  lasciare che D =" {x. x "<non> f x}".
>  da * ottenere un dove ". D = f = f a" per esplosione
>  inoltre hanno "un"<in>? D "<lunga freccia sinistra destra> un"<notin>
>f a "da esplosione
>  infine mostrare Falso da esplosione
>qed
>
>
>I guess the problem to translate "let ?D = ..." properly into French is
>due to the different spacing rules for ? (and !) in that language.
>
>I also like the ultimate conclusion in Italian better: "infine mostrare
>Falso da esplosione".
>
>
>	Makarius
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.