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

*To*: pvs-help@csl.sri.com*Subject*: rewrite rule for expressions inside LAMBDA*From*: Jacob Chang <Jacob.Chang@stanford.edu>*Date*: 11 Mar 2003 20:38:28 -0800*In-Reply-To*: <3E6EA07F.5010705@sdl.sri.com>*References*: <Pine.GSO.4.31.0303101934580.18653-100000@arctic.cse.msu.edu> <3E6EA07F.5010705@sdl.sri.com>*Sender*: pvs-help-owner@csl.sri.com

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?

**References**:**problem with finite types***From:*Borzoo Bonakdarpour <borzoo@cse.msu.edu>

**Re: problem with finite types***From:*Bruno Dutertre <bruno@sdl.sri.com>

- Prev by Date:
**Re: problem with finite types** - Next by Date:
**Re: rewrite rule for expressions inside LAMBDA** - Prev by thread:
**Re: problem with finite types** - Next by thread:
**Induction derivation tree** - Index(es):