Re: [isabelle] Evaluation of record expressions



Hello Johannes,

Yes, "⊩" basically means "≤".
I tried to define a similar lemma:

lemma test_bounded:
  "0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 < a + b - a * b ⟹
    ∀s. ((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
        (if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a /
        (a + b -
         a * b)) ≤ ((if c s ≠ 1 then 1 else 0) *
                      ((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
                       (if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / (a + b - a * b)))"
  apply(rule allI)
  apply(auto)

In this case the simplifier is able to split all possible cases, it's just the matter that it won't evaluate all expressions afterwards.
So my question is if there's a way how i can deduce this test_bounded lemma from the first one I posted and then make Isabelle evaluate all
cases. Thanks!

Michael

Am 14-10-13, schrieb Johannes Hölzl  <hoelzl at in.tum.de>:

> Am Dienstag, den 08.10.2013, 18:14 +0200 schrieb Michael Vu:
> > Dear isabelle experts,
> > 
> > I am currently working with records and I'm trying to write a small automation tool for generating calculations. But I'm stuck at proving some simple expressions like this one:
> > 
> > record state =
> >   t  :: real
> >   c :: real
> > 
> > lemma weakly_bounded:
> > "0 < a ⟹
> >     a < 1 ⟹
> >     0 < b ⟹
> >     b < 1 ⟹
> >     0 < a + b - a * b ⟹
> >     ∀s. t s = 0 ∨ t s = 1 ⟹
> >     ∀s. c s = 0 ∨ c s = 1 ⟹
> >     λs. (if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
> >         (if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a /
> >         (a + b -
> >          a * b) ⊩ λs. (if c s ≠ 1 then 1 else 0) *
> >                       ((if t s = 0 ∧ c s = 0 then 1 else 0) + (if t s = 0 ∧ c s = 1 then 1 else 0) * a / (a + b - a * b) +
> >                        (if t s = 1 ∧ c s = 1 then 1 else 0) * (1 - b) * a / (a + b - a * b))"
> > 
> > I thought simp would be enough to evaluate this, but it seems not to be the case. So I am looking for a way to make isabelle automatically verify
> > all possible states (the space is finite due to the conditions). I would appreciate every help.
> 
> Is ⊩ point wise  less or equal? If yes, you first should
> unfold fun_le_def, then the splitter can operate on it. Also I don't
> think that the simplifier can deduce that the set of states is finite.
> 
> > And secondly I've another cosmetic question. Given following subgoals:
> > 
> > 1. 0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 ≤ a
> > 2. 0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 ≤ 1 - b
> > 3. 0 < a ⟹ a < 1 ⟹ 0 < b ⟹ b < 1 ⟹ 0 ≤ a
> > 4. some complicated subgoal
> > apply(simp) 
> > apply(simp)
> > apply(simp) 
> > 
> > Is there any more elegant way other than to invoke simp 3 times? I also tried "auto" but it gets stuck on subgoal 4. 
> 
> You can use Isar to proof subgoal 4 first and subgoal 1, 2, 3 by the
> qed-command:
> 
> proof -
>   assumes "" then show "" ...
> qed simp_all
> 
> 
>   - Johannes




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