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



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
Description: S/MIME Cryptographic Signature



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