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

Another Problem during a proof !

My retrieve Function looks like:
retrDictc (d_c): Dicta = {w:Word | length(w)<length(d_c) and
(member(w,(d_c(length(w)))))}

Where Dicta is a finite_set of Word, and
 Section : TYPE = finite_set[Word]
 Dictc : TYPE = {d:finite_sequence[Section] | inv_Dictc(d)} 

This yields a TCC:
retrDictc_TCC1: OBLIGATION
      (FORALL (d_c: Dictc):
         is_finite[Word]({w: Word |
                           length[character](w) < length(d_c)
                               AND (member[list[character]](w,
(finseq_appl[Section](d_c)(length[character](w)))))}));

which i have to proof !!

I tried this by a finite_sequence induction of the form:

fsinduction[T : TYPE]: THEORY
BEGIN

empty_fin_seq : TYPE = {fs: finite_sequence[T] | length(fs) = 0}
p : VAR pred[finite_sequence[T]]
e : VAR T
fs : VAR finite_sequence[T]
empty_fs : VAR empty_fin_seq

  finite_sequence_induction : THEOREM
      FORALL (p : pred[finseq[T]]) :
          ((FORALL (fs : finseq[T] | length(fs) = 0) : p(fs)) AND
            (FORALL (l : nat) :
                        (FORALL (fs : finseq[T] | length(fs) = l)       
: p(fs)) =>
                        (FORALL (fs : finseq[T] | length(fs) = l + 1) :
p(fs))))
          IMPLIES FORALL (fs : finseq[T]) : p(fs)
END fsinduction

the proof leeds me to this subgoal:

[-1]    length(fs!1) = 1 + l!1
[-2]    (FORALL (fs: finseq[Section] | length(fs) = l!1):
         inv_Dictc(fs)
             IMPLIES
           is_finite[Word]({w: Word |
                             length[character](w) < length(fs)
                                 AND (member[list[character]](w,
(finseq_appl[Section](fs)(length[character](w)))))}))
{-3}    inv_Dictc(fs!1)
  |-------
{1}    is_finite[Word]({w: Word |
                        length[character](w) < length(fs!1)
                            AND (member[list[character]](w,
(finseq_appl[Section](fs!1)(length[character](w)))))})

which i tried to proof with (inst?), this yields two subgoals.
The first one is easily proofed with (ground). But the second one looks
like:

[-1]    length(fs!1) = 1 + l!1
[-2]    inv_Dictc(fs!1)
  |-------
[1]    is_finite[Word]({w: Word |
                        length[character](w) < length(fs!1)
                            AND (member[list[character]](w,
(finseq_appl[Section](fs!1)(length[character](w)))))})

Which is nearly the expression i wanted to proof at the beginning. 
Can i do a workaround at this problem, by defining an AXIOM: is_finite
(retrDictc), or would this cause inconsitance ? If this is the fact, has
anyone an idea, how i can proof the above expression ?

Thanks to all

-- 
---------------------------------------------------------
 ("\''/").__..-''"`-. .         Gernot Lepuschitz
 `9_ 9  )   `-. (    ).`-._.`)gernot@sbox.tu-graz.ac.at 
 (_Y_.)' ._   ) `._`.  " -.-'   Telematik - Student
 ..`-'_..-_/ /-'_.'/               TU - Graz
(l)-'' ((i).' ((!.'              
In the softwarerequirements they said Win95 or better
so I installed Linux.