# [isabelle] rule then simp in apply style proofs

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