Re: [isabelle] questions about forall



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.

--
  Peter




> 
> Amarin
> 
> On 10/27/2014 04:17 AM, Peter Lammich wrote:
> > 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
> >
> > --
> >    Peter
> >
> > On So, 2014-10-26 at 23:55 -0500, Amarin Phaosawasdi wrote:
> >> 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
> >>
> >
> 
> 






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