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



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.

--
  Peter


On Di, 2014-11-11 at 14:58 -0600, 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
> 






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