Email Gateway (Aug 19 2022 at 16:38): Email Gateway (Aug 19 2022 at 16:38):From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
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
Email Gateway (Aug 19 2022 at 16:38):From: Peter Lammich <lammich@in.tum.de>
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.
Email Gateway (Aug 19 2022 at 16:38):From: Tobias Nipkow <nipkow@in.tum.de>
Yet another variation:
lemma "(''x'' ::= N 1,λx.0) ⇒ (λx.0)(''x'':=1)"
using Assign[of "''x''" "N 1" "λx. 0"] by simp
Tobias
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC