Re: [isabelle] Evaluation of record expressions



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.