*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] questions about forall*From*: Amarin Phaosawasdi <phaosaw2 at illinois.edu>*Date*: Tue, 28 Oct 2014 09:27:49 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1414481913.16189.53.camel@lapbroy33>*References*: <544DD032.20400@illinois.edu> <1414401430.16189.43.camel@lapbroy33> <544E74D9.9000507@illinois.edu> <1414481913.16189.53.camel@lapbroy33>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.2.0

Got it, thank you for the help. Amarin On 10/28/2014 02:38 AM, Peter Lammich wrote:

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. -- PeterAmarin 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

**References**:**[isabelle] questions about forall***From:*Amarin Phaosawasdi

**Re: [isabelle] questions about forall***From:*Peter Lammich

**Re: [isabelle] questions about forall***From:*Amarin Phaosawasdi

**Re: [isabelle] questions about forall***From:*Peter Lammich

- Previous by Date: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- Next by Date: Re: [isabelle] incompatible operand type
- Previous by Thread: Re: [isabelle] questions about forall
- Next by Thread: [isabelle] TERM exception in fologic.ML
- Cl-isabelle-users October 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list