*To*: 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*: Tue, 15 Oct 2013 13:55:50 +1100*In-reply-to*: <fbaeabd536cc4.525c474f@rwth-aachen.de>*References*: <fb86700f35dac.52544b91@rwth-aachen.de> <1381768130.4401.40.camel@macbroy12.informatik.tu-muenchen.de> <fbaeabd536cc4.525c474f@rwth-aachen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Hey all.

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

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)

I'm not exactly sure what you're looking for. Good luck, Thomas. On 15/10/13 04:34, Michael Vu wrote:

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

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

**Re: [isabelle] Evaluation of record expressions***From:*Johannes Hölzl

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

- Previous by Date: Re: [isabelle] Isabelle2013-1-RC2 available for testing
- Next by Date: Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore
- Previous by Thread: Re: [isabelle] Evaluation of record expressions
- Next by Thread: Re: [isabelle] General code_abort'd constant
- 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