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