Re: [isabelle] rule then simp in apply style proofs
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
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.
On Di, 2014-11-11 at 14:58 -0600, Amarin Phaosawasdi wrote:
> 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,
> 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"
> com = Assign string aexp ("_ ::= _" [1000, 61] 61)
> big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
> 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
> thus ?thesis by simp
This archive was generated by a fusion of
Pipermail (Mailman edition) and