[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

rewrite rule for expressions inside LAMBDA



Hi,
  I'm trying to find a way to use the rewrite rule for an expression
inside an lambda expression.

I have an axiom that states that
  FORALL (x:State): A(s)=B(s)

and I want to be able to use this axiom in the derivation of a theorem
of the form

  G(LAMBDA (s: State): B(s))

to replace this expression by

  G(LAMBDA (s: State): A(s))

using this axiom where G is a function that I do not want to expand at
this point in time.  I have tried to use the rewrite rules in various
ways without success.  Can anyone help me in how to deal with this type
of expressions in PVS in an easy way?  Or if this is even possible in
PVS?

Thanks,
Jacob

I have include a simplified example below of what I want to do:

------------------------------------------------------------------
LTLlib[State:TYPE] : THEORY 
BEGIN
  Path : TYPE = [nat -> State]

  StateFormula : TYPE = pred[State]

  pi: VAR Path

  G(sf: StateFormula)(pi) : bool = FORALL (i:nat) :sf(pi(i));

END LTLlib

submodule : THEORY
BEGIN
  State : TYPE = [#
	inp : boolean,
	#]

  IMPORTING LTLlib[State]

END submodule

module : THEORY
BEGIN

  IMPORTING submodule

  State : TYPE = [#
	submod_inst : submodule.State,

	mainin : boolean,
	#]

  IMPORTING LTLlib[State]

  pi : VAR LTLlib[State].Path
 
  conninput : AXIOM (
    FORALL (st: State) :
      st`mainin = st`submod_inst`inp
  )

  them1 : THEOREM (
% Want to transform this expressions to
% G(LAMBDA(st: State): st`mainin
% using the conninput axiom
    G(LAMBDA(st: State): st`submod_inst`inp)(pi)
  )

END module

-----------------------------------------------
And a representative of what I tried to do to prove it.  As shown, I was
unable to push the proof through unless I expand the expression G, which
I do not want to do because the expression can be very complicated.

them1 :  

  |-------
{1}   FORALL (pi: LTLlib[State].Path):
        (G(LAMBDA (st: State): st`submod_inst`inp)(pi))

Rule? (skosimp)
Skolemizing and flattening,
this simplifies to: 
them1 :  

  |-------
{1}   (G(LAMBDA (st: State): st`submod_inst`inp)(pi!1))

them1 : 

Rule? (rewrite "conninput")
No matching instance for conninput found.
No change on: (rewrite "conninput")
them1 :  

  |-------
{1}   (G(LAMBDA (st: State): st`submod_inst`inp)(pi!1))

Rule? (use "conninput")
Using lemma conninput,
this simplifies to: 
them1 :  

{-1}  FORALL (st: State): st`mainin = st`submod_inst`inp
  |-------
[1]   (G(LAMBDA (st: State): st`submod_inst`inp)(pi!1))

Rule? (rewrite -1 1)
The following errors occurred within the strategy:

No suitable redexes found.

No sequent formula corresponding to -2,


No change on: (rewrite -1 1)
them1 :  

{-1}  FORALL (st: State): st`mainin = st`submod_inst`inp
  |-------
[1]   (G(LAMBDA (st: State): st`submod_inst`inp)(pi!1))

Rule? (rewrite -1 1 :dir rl)
The following errors occurred within the strategy:

No suitable redexes found.

No sequent formula corresponding to -2,


No change on: (rewrite -1 1 :dir rl)
them1 :  

{-1}  FORALL (st: State): st`mainin = st`submod_inst`inp
  |-------
[1]   (G(LAMBDA (st: State): st`submod_inst`inp)(pi!1))

Rule? (expand "G")
Expanding the definition of G,
this simplifies to: 
them1 :  

[-1]  FORALL (st: State): st`mainin = st`submod_inst`inp
  |-------
{1}   FORALL (i: nat): pi!1(i)`submod_inst`inp

Rule? (skosimp)
Skolemizing and flattening,
this simplifies to: 
them1 :  

[-1]  FORALL (st: State): st`mainin = st`submod_inst`inp
  |-------
{1}   pi!1(i!1)`submod_inst`inp

Rule? (inst?)
Found substitution:
st: State gets pi!1(i!1),
Using template: st
Instantiating quantified variables,
this simplifies to: 
them1 :  

{-1}  pi!1(i!1)`mainin = pi!1(i!1)`submod_inst`inp
  |-------
[1]   pi!1(i!1)`submod_inst`inp

Rule? (replace -1 1 :dir rl)
Replacing using formula -1,
this simplifies to: 
them1 :  

[-1]  pi!1(i!1)`mainin = pi!1(i!1)`submod_inst`inp
  |-------
{1}   pi!1(i!1)`mainin

Rule?