# Re: [isabelle] rule then simp in apply style proofs

Hi Amarin,
The problem is that, for the introduction rule Assign, auto, blast, etc.
must see the pattern "x:=aval ...". However, you could use metis:
by (metis Assign aval.simps)
or you could use the simplification rules generated for the big_step
predicate:
by (simp add: big_step.simps)
Yet another option may be to prove a lemma of the form
[| ...; s'=aval e s |] ==> (Assign x e,s) => s'
or define the assign-rule like this in first place.
--
Peter
On Di, 2014-11-11 at 14:58 -0600, 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
>

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