Re: [isabelle] Evaluation of record expressions



Hey Michael.

Sorry about being short with you before. I wasn't actually annoyed by the previous question, just pointing out that it didn't quite make sense and there was probably a misunderstanding inherent in it somewhere.

It looks like you're closer to the right track. I note two things you might want to work on.

My first observation was that you probably want to hide the THE operator somehow. Using Hilbert choice semantically is fine (as long as you're OK with it), but the operator also happens to be syntactically difficult to grapple with.

In short, "THE x. isLub UNIV (range f) x" seems like a verbose description of the least upper bound of "range f". I wonder if there's an instantiation/proof anywhere that lets you show "(THE x. isLub UNIV (range f) x) = Sup (range f)".

I don't have an answer to that myself, I don't really know anything about reals in Isabelle. Maybe one of the calculus experts can comment?

The other problem is that you're assuming that "t s" is 0 or 1 for every s. That's never true. So your proof can be finished by:
  apply (drule_tac x="some_value (| t := 0.5 |)" in spec)
  apply simp
  done

That's almost certainly not what you want. I guess you probably just want to constrain the s's considered in computing the ranges of the lambda functions, but you would do that by replace range f
with f ` S instead.

Good luck,
    Thomas.

On 18/10/13 12:21, Michael Vu wrote:
Hello Thomas, hello all,

you're right, I really failed...Thanks for your counter example. Well the reason behind this is that i work with a custom package of theorems and used the wrong lemma which resulted in an unsolveable goal. So I'm really sorry.
Anyway, I managed to correct this and now Isabelle outputs this subgoal:

0 < (a::real) ⟹
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 ⟹
     (THE ba. isLub UNIV
               (range (λ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)))
               ba)
     ≤ (THE ba. isLub UNIV
                 (range (λ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))))
                 ba)

The remaining functions are all defined in Set.thy/Lubs.thy and now I am stuck on how to prove this. This subgoal just shows that the upper bound of
the first lambda function is less or equal than the upper bound of the second function. Any help would be appreciated. I hope I didn't forget anything this time. Thanks!

Michael

Am 15-10-13, schrieb Thomas Sewell  <thomas.sewell at nicta.com.au>:

Hey all.

I had a look at this on the assumption that this was somehow related to the record package.

Looking at this test lemma, it would seem that

a) it is false in the case where "t s = 1 & c s = 1 & a * 2 = 1 & b * 2 = 1"
b) it seems to have nothing to do with the record package
c) nothing needs to be evaluated, instead, hypotheses need to be proven, which is hard when they're false.

You can see that the lemma is false via:
   apply (rule allI)
   apply (case_tac "t s = 1 & c s = 1 & a = 0.5 & b = 0.5")
    apply (elim conjE, simp only: )
    apply (simp add: field_simps)

(the fact that all these tools are conservative means the original goal was false also)

I'm not exactly sure what you're looking for.

Good luck,
     Thomas.






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