Re: [isabelle] Evaluation of record expressions



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.

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





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