Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Question on hypothesis

view this post on Zulip Email Gateway (Aug 18 2022 at 16:36):

From: Makarius <makarius@sketis.net>
Here are some examples that illustrate goal-free experimentation in
Isabelle2009-2:

theory Scratch
imports Main
begin

example_proof
assume "P (xs @ [])"
thm this [simplified]

have "xs @ [] = xxx" apply simp
oops

Makarius

view this post on Zulip Email Gateway (Aug 18 2022 at 16:38):

From: olfa mraihi <olfa.mraihi@yahoo.fr>
Hi Isabelle community,
I' m newbie on using Isabelle and I need you help by answering if possible these 2 questions:

1)how to represent hypothesis in isabelle? is it with the keyword "assume"?

2)how to tell isabelle to simplify a set of hypothesis under the use of the adequate theory?  (remark:there is no goal to prove,only hypothesis to simplify),is it like that?:
use_thy "theoryname.thy";
assume a & b & c;
by auto;

Thank you very much.

view this post on Zulip Email Gateway (Aug 18 2022 at 16:42):

From: olfa mraihi <olfa.mraihi@yahoo.fr>
how to do when I have a conjunction of hypothesis to simplify
I have tried :
theory Scratch
  imports Main
  begin
example_proof
have "(i+length l2=iP+length l2P) & (l1 @ l2=l1P @ l2P) & (l2P=[]) & (length l1+length l2=length l1P+length l2P)"  apply simp

but it doesn't work.

Best Regards.

view this post on Zulip Email Gateway (Aug 18 2022 at 16:42):

From: Tobias Nipkow <nipkow@in.tum.de>
It works. The simplifier simply cannot simplify it any further. You may
have hoped that it replaces l2P by [] everywhere, but by default it does
not use one conjunct to simplify another. You can explicitly instruct it
to use the left conjunct to simplify the right one:

apply(simp cong: conj_cong)

Regards
Tobias

PS No need for parentheses in your example.

olfa mraihi schrieb:

view this post on Zulip Email Gateway (Aug 18 2022 at 16:42):

From: olfa mraihi <olfa.mraihi@yahoo.fr>
this is what I have as output
 i + length l2 = iP + length l2P &
    l1 @ l2 = l1P @ l2P & l2P = [] & length l1 + length l2 = length l1P

but the simplification should return
 i + length l2 = iP &  l1 @ l2 = l1P & length l1 + length l2 = length l1P
is it possible?if yes how?
thank you very much.

--- En date de : Mer 15.12.10, Tobias Nipkow <nipkow@in.tum.de> a écrit :

view this post on Zulip Email Gateway (Aug 18 2022 at 16:42):

From: Tobias Nipkow <nipkow@in.tum.de>
olfa mraihi schrieb:

this is what I have as output
i + length l2 = iP + length l2P &
l1 @ l2 = l1P @ l2P & l2P = [] & length l1 + length l2 = length l1P

but the simplification should return
i + length l2 = iP & l1 @ l2 = l1P & length l1 + length l2 = length l1P
is it possible?if yes how?

That is not directly possible. If the formulas you want to simplify are
assumptions, it works. Try

lemma "[| i+length l2=iP+length l2P; l1 @ l2=l1P @ l2P; l2P=[]; length
l1+length l2=length l1P+length l2P |] ==> P"
apply simp

Tobias

thank you very much.

--- En date de : Mer 15.12.10, Tobias Nipkow <nipkow@in.tum.de> a écrit :

De: Tobias Nipkow <nipkow@in.tum.de>
Objet: Re: [isabelle] Fw : Re: Question on hypothesis
À: "olfa mraihi" <olfa.mraihi@yahoo.fr>
Cc: cl-isabelle-users@lists.cam.ac.uk
Date: Mercredi 15 décembre 2010, 22h12

It works. The simplifier simply cannot simplify it any further. You may
have hoped that it replaces l2P by [] everywhere, but by default it does
not use one conjunct to simplify another. You can explicitly instruct it
to use the left conjunct to simplify the right one:

apply(simp cong: conj_cong)

Regards
Tobias

PS No need for parentheses in your example.

olfa mraihi schrieb:

how to do when I have a conjunction of hypothesis to simplify
I have tried :
theory Scratch
imports Main
begin
example_proof
have "(i+length l2=iP+length l2P) & (l1 @ l2=l1P @ l2P) & (l2P=[]) & (length l1+length l2=length l1P+length l2P)" apply simp

but it doesn't work.

Best Regards.

view this post on Zulip Email Gateway (Aug 18 2022 at 16:44):

From: olfa mraihi <olfa.mraihi@yahoo.fr>
0)thank you very much for your usefull answer
1)what does it mean [| |]?
2)what does it mean P?
3)it works only with assumption l2P=[] or l1P=[] but when I put l1=[], the last assumption (which is  l1+length l2=length l1P+length l2P) disappears in the output and the same thing happens when I put l2=[]!!

--- En date de : Jeu 16.12.10, Tobias Nipkow <nipkow@in.tum.de> a écrit :

De: Tobias Nipkow <nipkow@in.tum.de>
Objet: Re: [isabelle] Fw : Re: Question on hypothesis
À: "olfa mraihi" <olfa.mraihi@yahoo.fr>
Cc: cl-isabelle-users@lists.cam.ac.uk
Date: Jeudi 16 décembre 2010, 7h37

olfa mraihi schrieb:

this is what I have as output
  i + length l2 = iP + length l2P &
     l1 @ l2 = l1P @ l2P & l2P = [] & length l1 + length l2 = length l1P

but the simplification should return
  i + length l2 = iP &  l1 @ l2 = l1P & length l1 + length l2 = length l1P
is it possible?if yes how?

That is not directly possible. If the formulas you want to simplify are
assumptions, it works. Try

lemma "[| i+length l2=iP+length l2P; l1 @ l2=l1P @ l2P; l2P=[]; length
l1+length l2=length l1P+length l2P |] ==> P"
apply simp

Tobias

thank you very much.

--- En date de : Mer 15.12.10, Tobias Nipkow <nipkow@in.tum.de> a écrit :

De: Tobias Nipkow <nipkow@in.tum.de>
Objet: Re: [isabelle] Fw : Re: Question on hypothesis
À: "olfa mraihi" <olfa.mraihi@yahoo.fr>
Cc: cl-isabelle-users@lists.cam.ac.uk
Date: Mercredi 15 décembre 2010, 22h12

It works. The simplifier simply cannot simplify it any further. You may
have hoped that it replaces l2P by [] everywhere, but by default it does
not use one conjunct to simplify another. You can explicitly instruct it
to use the left conjunct to simplify the right one:

apply(simp cong: conj_cong)

Regards
Tobias

PS No need for parentheses in your example.

olfa mraihi schrieb:

how to do when I have a conjunction of hypothesis to simplify
I have tried :
theory Scratch
    imports Main
    begin
example_proof
have "(i+length l2=iP+length l2P) & (l1 @ l2=l1P @ l2P) & (l2P=[]) & (length l1+length l2=length l1P+length l2P)"  apply simp

but it doesn't work.

Best Regards.

view this post on Zulip Email Gateway (Aug 18 2022 at 16:44):

From: Tobias Nipkow <nipkow@in.tum.de>
olfa mraihi schrieb:

0)thank you very much for your usefull answer
1)what does it mean [| |]?
2)what does it mean P?

Please refer to the extensive Isabelle documentation. This mailing list
is intended to discuss technical questions and not to give an
introduction to the system to save you reading the basic material.

3)it works only with assumption l2P=[] or l1P=[] but when I put l1=[],
the last assumption (which is l1+length l2=length l1P+length l2P)
disappears in the output and the same thing happens when I put l2=[]!!

Assumptions that simplify to True disappear.

Tobias

--- En date de : Jeu 16.12.10, Tobias Nipkow /<nipkow@in.tum.de>/ a
écrit :

De: Tobias Nipkow <nipkow@in.tum.de>
Objet: Re: [isabelle] Fw : Re: Question on hypothesis
À: "olfa mraihi" <olfa.mraihi@yahoo.fr>
Cc: cl-isabelle-users@lists.cam.ac.uk
Date: Jeudi 16 décembre 2010, 7h37

olfa mraihi schrieb:
> this is what I have as output
> i + length l2 = iP + length l2P &
> l1 @ l2 = l1P @ l2P & l2P = [] & length l1 + length l2 =
length l1P
>
> but the simplification should return
> i + length l2 = iP & l1 @ l2 = l1P & length l1 + length l2 =
length l1P
> is it possible?if yes how?

That is not directly possible. If the formulas you want to simplify are
assumptions, it works. Try

lemma "[| i+length l2=iP+length l2P; l1 @ l2=l1P @ l2P; l2P=[]; length
l1+length l2=length l1P+length l2P |] ==> P"
apply simp

Tobias

> thank you very much.
>
> --- En date de : Mer 15.12.10, Tobias Nipkow <nipkow@in.tum.de
<http://fr.mc261.mail.yahoo.com/mc/compose?to=nipkow@in.tum.de>> a
écrit :
>
>
> De: Tobias Nipkow <nipkow@in.tum.de
<http://fr.mc261.mail.yahoo.com/mc/compose?to=nipkow@in.tum.de>>
> Objet: Re: [isabelle] Fw : Re: Question on hypothesis
> À: "olfa mraihi" <olfa.mraihi@yahoo.fr
<http://fr.mc261.mail.yahoo.com/mc/compose?to=olfa.mraihi@yahoo.fr>>
> Cc: cl-isabelle-users@lists.cam.ac.uk
<http://fr.mc261.mail.yahoo.com/mc/compose?to=cl-isabelle-users@lists.cam.ac.uk>
> Date: Mercredi 15 décembre 2010, 22h12
>
>
> It works. The simplifier simply cannot simplify it any further.
You may
> have hoped that it replaces l2P by [] everywhere, but by default
it does
> not use one conjunct to simplify another. You can explicitly
instruct it
> to use the left conjunct to simplify the right one:
>
> apply(simp cong: conj_cong)
>
> Regards
> Tobias
>
> PS No need for parentheses in your example.
>
> olfa mraihi schrieb:
>> how to do when I have a conjunction of hypothesis to simplify
>> I have tried :
>> theory Scratch
>> imports Main
>> begin
>> example_proof
>> have "(i+length l2=iP+length l2P) & (l1 @ l2=l1P @ l2P) &
(l2P=[]) & (length l1+length l2=length l1P+length l2P)" apply simp
>>
>> but it doesn't work.
>>
>> Best Regards.
>>
>>
>>
>>
>
>
>
>

view this post on Zulip Email Gateway (Aug 18 2022 at 16:44):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Since I've just looked at the indexes of several likely choices among
the Isabelle documentation, and the nearest I found to an adequate
answer to question (1) was an a manual described as "old" and
"outdated", it seems reasonable to answer it here.

[| P ; Q |] ==> R is an abbreviation (at the level of the parser and
prettyprinter) for
P ==> (Q ==> R)

Jeremy

view this post on Zulip Email Gateway (Aug 18 2022 at 16:44):

From: Tobias Nipkow <nipkow@in.tum.de>
I beg to disagree. The Tutorial (not under old/outdated) has "[|" and
"|]" in the index, pointing to a table that explains that they are the
same as the similar looking symbols [| |], and those symbols are used
throughout the documentation, in particular on page 13, where it is
explained that they group together assumptions. I consider this an
adequate explanation.

Tobias

Jeremy Dawson schrieb:

Last updated: Nov 21 2024 at 12:39 UTC