# [isabelle] questions about forall

Hello,

`This question is based on some definitions defined in the book Concrete
``Semantics. Here's a high-level description of the problem.
`
I have to prove something in the form
"⋀ x. assumption1 ⟹ ... ⟹ assumptionN ⟹ thesis"

`However, the assumptions give me the exact value of x I needed. All
``other values make the assumptions false (hence making the thesis true).
`

`How would I go about proving the theorem, removing "⋀ x" and
``instantiating x to be that specific value I wanted?
`

`In particular, given the big step semantics of while loops in a simple
``programming language (see below), I'm trying to prove the following lemma.
`
lemma "⟦(WHILE b DO c,s) ⇒ s'';
bval b s;
(c,s) ⇒ s'⟧ ⟹
(WHILE b DO c,s') ⇒ s''"
I'm stuck at the step where I need to prove.
"⋀s2. bval b s ⟹
(c, s) ⇒ s' ⟹
bval b s ⟹
(c, s) ⇒ s2 ⟹
(WHILE b DO c, s2) ⇒ s'' ⟹
(WHILE b DO c, s') ⇒ s''"
In this case, I know that s2 has to be s'.
Below is the code.
Thank you,
Amarin
============================================
theory SemanticsQuestion imports Main begin
type_synonym vname = string
type_synonym val = int
type_synonym state = "vname ⇒ val"
datatype bexp = Bc bool
fun bval :: "bexp ⇒ state ⇒ bool" where
"bval (Bc v) s = v"
datatype
com = SKIP |
While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
inductive
big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
where
WhileFalse: "⟦¬bval b s⟧ ⟹ (WHILE b DO c,s) ⇒ s" |
WhileTrue: "⟦ bval b s1; (c,s1) ⇒ s2; (WHILE b DO c,s2) ⇒ s3 ⟧
⟹ (WHILE b DO c, s1) ⇒ s3"
declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
inductive_cases WhileE[elim]: "(WHILE b DO c,s) ⇒ t"
theorem big_step_determ: "⟦ (c,s) ⇒ t; (c,s) ⇒ u ⟧ ⟹ u = t"
by (induction arbitrary: u as3 rule: big_step_induct) blast+
lemma "⟦(WHILE b DO c,s) ⇒ s'';
bval b s;
(c,s) ⇒ s'⟧ ⟹
(WHILE b DO c,s') ⇒ s''"
apply (erule WhileE)
apply simp
sorry
end

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