Re: [isabelle] questions about forall



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.