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