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

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

Best regards, 


On 2/10/18, 12:13 PM, "cl-isabelle-users-bounces at on behalf
of Makarius" <cl-isabelle-users-bounces at on behalf of
makarius at> 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
>d=0 so lets see if it can turn Isar proofs
>into Coq (French) or Matita (Italian).
>Here are some bits from
>theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A.
>\<exists>x. A = f x"
>  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
>théorème Cantor:"¡<<nexistes>f::' a \<Rightarrow>' a set. C'est tout ce
>qui compte. Existe >x. A = f x"
>  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
>teorema Cantor:""<allegatoists>f::"a"<Rightarrow> "un set. "<forall>A.
>"<esiste>x. A = f x x".
>  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
>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.