# [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.