Simon Wimmer

2016-10-01 14:20:53 UTC

Hi Igor,

I did not look at your definitions in detail nor do I know anything about

the problem domain but there a few general things I can say.

If you look closely at the proof state that you give to blast in the

theorem you want to prove at the end of the theory, you might see

that the definitions did not get unfolded as you wanted them to be. You can

remedy this by adding the attribute 'abs_def' to the definitional theorems

before unfolding them (e.g. 'CC_active_b7_def[abs_def]').

The second thing is that your are trying to prove an existential statement,

so the best way is to explicitly specify a witness.

(Use 'apply (rule exI[where x = <your witness>]')

I do not know what it looks like or if you need to construct it by

induction, etc.

Sometimes Isabelle proof methods can find such a witness automatically,

however given the complexity of the formulae involved,

I fear that you're out of luck here .

I hope that was somewhat helpful.

Simon

I did not look at your definitions in detail nor do I know anything about

the problem domain but there a few general things I can say.

If you look closely at the proof state that you give to blast in the

theorem you want to prove at the end of the theory, you might see

that the definitions did not get unfolded as you wanted them to be. You can

remedy this by adding the attribute 'abs_def' to the definitional theorems

before unfolding them (e.g. 'CC_active_b7_def[abs_def]').

The second thing is that your are trying to prove an existential statement,

so the best way is to explicitly specify a witness.

(Use 'apply (rule exI[where x = <your witness>]')

I do not know what it looks like or if you need to construct it by

induction, etc.

Sometimes Isabelle proof methods can find such a witness automatically,

however given the complexity of the formulae involved,

I fear that you're out of luck here .

I hope that was somewhat helpful.

Simon

Hallo,

I am trying to do model checking of Simulink components? with Isabelle

and now a little bit stuck on the way.

In general we would like to compare two software components for

behavior equivalence. The components are represented by automaton made

from Simulink components.

Since the theory file is a bit long, I attached it to the mail.

The problem of this task is that one component has 7 input ports (that

are programed in Isabelle as functions of time: V_V LU_s LD_s BF_pc PB_b

P_b CC_b FTS_a_b) and the second one has 8 input ports. We are trying

to find a value the on the 8th port of the second component which make

both of components equal. (This value must exist.) After that the

plan is to prove it by induction on t (?).

The internal variable update functions

(pV_eF7, pV_eR7, pV_FF7, pV_eF8, pV_eR8, pV_FF8) are calculated from

port values taken on the previous time step (t-1). The functions pV_FF8

and pV_FF7 are recursive while the other are not. The output value

are CC_active_b7 and CC_active_b8 respectively.

If you have time, could you please take a look at the Isabelle code,

probably you can suggest the best way to prove such things or the

direction I have to go? Or you immediately see that my approach is

totally wrong.

Sorry for a not concrete question any help or advice is highly appreciated.

Best regards,

Igor

I am trying to do model checking of Simulink components? with Isabelle

and now a little bit stuck on the way.

In general we would like to compare two software components for

behavior equivalence. The components are represented by automaton made

from Simulink components.

Since the theory file is a bit long, I attached it to the mail.

The problem of this task is that one component has 7 input ports (that

are programed in Isabelle as functions of time: V_V LU_s LD_s BF_pc PB_b

P_b CC_b FTS_a_b) and the second one has 8 input ports. We are trying

to find a value the on the 8th port of the second component which make

both of components equal. (This value must exist.) After that the

plan is to prove it by induction on t (?).

The internal variable update functions

(pV_eF7, pV_eR7, pV_FF7, pV_eF8, pV_eR8, pV_FF8) are calculated from

port values taken on the previous time step (t-1). The functions pV_FF8

and pV_FF7 are recursive while the other are not. The output value

are CC_active_b7 and CC_active_b8 respectively.

If you have time, could you please take a look at the Isabelle code,

probably you can suggest the best way to prove such things or the

direction I have to go? Or you immediately see that my approach is

totally wrong.

Sorry for a not concrete question any help or advice is highly appreciated.

Best regards,

Igor