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

[PVS-Help] problem in induction scheme for lemmas involving 'choose'



Hi,

I am trying to prove lemma pred_edge in following theory:

%%%%%%%%%%%%%%%%%%
  grf  [node:TYPE+ ]: THEORY

  BEGIN

  mygraph: VAR non_empty_finite_set[[node, node]]
  p, q: VAR node


  %% recursive definition to find predecessors of node p in mygraph

  predecessors(mygraph, p): RECURSIVE set[node] =
    IF mygraph=emptyset  THEN emptyset
    ELSE LET edge = choose(mygraph) IN
      IF edge`2 = p THEN
        add(edge`1 , predecessors(remove(edge,mygraph), p))
      ELSE
        predecessors(remove(edge,mygraph), p)
      ENDIF
    ENDIF
     MEASURE card(mygraph)

  %%
  % induction scheme :
  % base case :emptyset
  % induction step : assume for g_var and prove for (g_var + 1 edge)
  %%

  graph_induction: LEMMA
   FORALL (p: [non_empty_finite_set[[node,node]] -> boolean]):
    ( p(emptyset) AND
     (FORALL (g_var:non_empty_finite_set[[node,node]],a,b:node):
      (p(g_var) IMPLIES p(add((a,b),g_var)))
    )
    IMPLIES (FORALL (g_var: non_empty_finite_set[[node,node]]): p(g_var)))


  pred_edge : LEMMA
  predecessors(mygraph,p)(q) IFF member((q,p),mygraph)

  END grf
%%%%%%%%%%%%%%%%%%



 while proving this i reached a step which i think can not be proved due
to randomness of choose.


[-1]  choose(add((a!1, b!1), g_var!1))`2 = p!1
[-2]  member((q!1, p!1), add((a!1, b!1), g_var!1))
[-3]  predecessors(g_var!1, p!1)(q!1)
[-4]  member((q!1, p!1), g_var!1)
  |-------
{1}   choose(add((a!1, b!1), g_var!1))`1 = q!1
{2}   member(q!1,
             predecessors(remove(choose(add((a!1, b!1), g_var!1)),
                                 add((a!1, b!1), g_var!1)),
                          p!1))
[3]   add((a!1, b!1), g_var!1) = emptyset


Is there some other induction scheme which will prove such lemmas
involving choose?

thanx in advance,
Sudhir.