Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] questions about forall


view this post on Zulip Email Gateway (Aug 19 2022 at 16:09):

From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
Hello,

This question is based on some definitions defined in the book Concrete
Semantics. Here's a high-level description of the problem.

I have to prove something in the form
"⋀ x. assumption1 ⟹ ... ⟹ assumptionN ⟹ thesis"

However, the assumptions give me the exact value of x I needed. All
other values make the assumptions false (hence making the thesis true).

How would I go about proving the theorem, removing "⋀ x" and
instantiating x to be that specific value I wanted?

In particular, given the big step semantics of while loops in a simple
programming language (see below), I'm trying to prove the following lemma.

lemma "⟦(WHILE b DO c,s) ⇒ s'';
bval b s;
(c,s) ⇒ s'⟧ ⟹
(WHILE b DO c,s') ⇒ s''"

I'm stuck at the step where I need to prove.
"⋀s2. bval b s ⟹
(c, s) ⇒ s' ⟹
bval b s ⟹
(c, s) ⇒ s2 ⟹
(WHILE b DO c, s2) ⇒ s'' ⟹
(WHILE b DO c, s') ⇒ s''"

In this case, I know that s2 has to be s'.

Below is the code.

Thank you,
Amarin

============================================
theory SemanticsQuestion imports Main begin

type_synonym vname = string
type_synonym val = int
type_synonym state = "vname ⇒ val"

datatype bexp = Bc bool
fun bval :: "bexp ⇒ state ⇒ bool" where
"bval (Bc v) s = v"

datatype
com = SKIP |
While bexp com ("(WHILE _/ DO _)" [0, 61] 61)

inductive
big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
where
WhileFalse: "⟦¬bval b s⟧ ⟹ (WHILE b DO c,s) ⇒ s" |
WhileTrue: "⟦ bval b s1; (c,s1) ⇒ s2; (WHILE b DO c,s2) ⇒ s3 ⟧
⟹ (WHILE b DO c, s1) ⇒ s3"

declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
inductive_cases WhileE[elim]: "(WHILE b DO c,s) ⇒ t"

theorem big_step_determ: "⟦ (c,s) ⇒ t; (c,s) ⇒ u ⟧ ⟹ u = t"
by (induction arbitrary: u as3 rule: big_step_induct) blast+

lemma "⟦(WHILE b DO c,s) ⇒ s'';
bval b s;
(c,s) ⇒ s'⟧ ⟹
(WHILE b DO c,s') ⇒ s''"
apply (erule WhileE)
apply simp
sorry

end

view this post on Zulip Email Gateway (Aug 19 2022 at 16:09):

From: Peter Lammich <lammich@in.tum.de>
You need to exploit determinism of your semantics, e.g.

lemma "⟦(WHILE b DO c,s) ⇒ s'';
bval b s;
(c,s) ⇒ s'⟧ ⟹
(WHILE b DO c,s') ⇒ s''"
apply (erule WhileE)
apply simp
apply (drule (1) big_step_determ, simp)
done

view this post on Zulip Email Gateway (Aug 19 2022 at 16:10):

From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
Thanks. It seems like the simplifier can do the job when I have the
right assumptions.

I have some follow up questions.

What does the "(1)" do?

I see that using drule (without the "(1)") requires me to prove the
other assumption in big_step_determ, while when using "drule (1)"I am
not required to do so.

In general, what does adding "(number)" to a drule do? Also can I use it
with rule, erule, frule as well?

Also, what is the difference between the following?

apply (drule (1) big_step_determ, simp)

and

apply (drule (1)big_step_determ)
apply (simp)

Amarin

view this post on Zulip Email Gateway (Aug 19 2022 at 16:11):

From: Peter Lammich <lammich@in.tum.de>
On Mo, 2014-10-27 at 11:37 -0500, Amarin Phaosawasdi wrote:

What does the "(1)" do?

I see that using drule (without the "(1)") requires me to prove the
other assumption in big_step_determ, while when using "drule (1)"I am
not required to do so.

In general, what does adding "(number)" to a drule do? Also can I use it
with rule, erule, frule as well?

The (n) means, that n extra assumptions should be discharged. It's
roughly the same as adding ",assumption,...,assumption" n times.

Also, what is the difference between the following?

apply (drule (1) big_step_determ, simp)

and

apply (drule (1)big_step_determ)
apply (simp)

In your case, it should be the same, as the drule matches the
assumptions unambiguously.
In general, the "," allows backtracking, while a new "apply"
only takes the first result.

view this post on Zulip Email Gateway (Aug 19 2022 at 16:11):

From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
Got it, thank you for the help.

Amarin


Last updated: Mar 29 2024 at 12:28 UTC