*To*: Michael Vu <michael.vu at rwth-aachen.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Evaluation of record expressions*From*: Thomas Sewell <thomas.sewell at nicta.com.au>*Date*: Fri, 18 Oct 2013 17:41:39 +1100*In-reply-to*: <fb1a724739db5.5260a920@rwth-aachen.de>*References*: <fb1a724739db5.5260a920@rwth-aachen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Hey Michael.

apply (drule_tac x="some_value (| t := 0.5 |)" in spec) apply simp done

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.

**References**:**Re: [isabelle] Evaluation of record expressions***From:*Michael Vu

- Previous by Date: Re: [isabelle] Evaluation of record expressions
- Next by Date: Re: [isabelle] Jinja-Threads build problem
- Previous by Thread: Re: [isabelle] Evaluation of record expressions
- Next by Thread: Re: [isabelle] Evaluation of record expressions
- Cl-isabelle-users October 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list