*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] rule then simp in apply style proofs*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 12 Nov 2014 10:36:43 +0100*In-reply-to*: <54627891.5050306@illinois.edu>*References*: <54627891.5050306@illinois.edu>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

Yet another variation: lemma "(''x'' ::= N 1,λx.0) ⇒ (λx.0)(''x'':=1)" using Assign[of "''x''" "N 1" "λx. 0"] by simp Tobias On 11/11/2014 21:58, Amarin Phaosawasdi wrote:

Hi, Based on the Concrete Semantics book, I want to prove that after assigning 1 to x, the state is updated with x being 1. To do this informally, I would use the semantics of assignmentfollowed by simplification. Is there a one-liner proof that can do this? Below are the definitions and the Isar style proof. What are the other simpler ways to prove this lemma using Isar (e.g., do I really need to spell out the intermediate state to match the assignment rule)? Thank you, Amarin ============================= theory Question imports Main begin type_synonym state = "string ⇒ int" datatype aexp = N int fun aval :: "aexp ⇒ state ⇒ int" where "aval (N n) s = n" datatype com = Assign string aexp ("_ ::= _" [1000, 61] 61) inductive big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55) where Assign: "(x ::= a,s) ⇒ (s(x := aval a s))" lemma "(''x'' ::= N 1,λx.0) ⇒ (λx.0)(''x'':=1)" proof - let ?s="λx.0" have "(''x'' ::= N 1,λx.0) ⇒ (λx.0)(''x'':=aval (N 1) ?s)" by (rule Assign) thus ?thesis by simp qed end

**Attachment:
smime.p7s**

**References**:**[isabelle] rule then simp in apply style proofs***From:*Amarin Phaosawasdi

- Previous by Date: Re: [isabelle] rule then simp in apply style proofs
- Next by Date: [isabelle] AFP installation instructions
- Previous by Thread: Re: [isabelle] rule then simp in apply style proofs
- Next by Thread: [isabelle] AFP installation instructions
- Cl-isabelle-users November 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