Uni notes pvs

blatt 3 : (lemma "trans")

(skolem 1 (a b c e))

(prop) : fertig 

(induct l) FOR skolem
(induct-and-simplify l) FOR skolem
(measure-induct+ "lenght(l)" l)
(name-replace name formular)
(inst? -3)  instanzierung automatisch suchen
(undo)y = tab+u
(delete 2 3) : ziele 2 und 3 löschen
(expand "occ" 1 1) : erstes vorkommen von okk in  1 auspacken !!!
(use lemma_name) : versucht lemma gleich zu instanzieren

z.b. (use sort_induct) , induktionsschema verwenden

"let (u,v)" : mit (beta-1) splitten 


nach expand  oder (lemma + inst) immer mal grind probieren...


C-cc : abbrechen
(restore) : zum vorigen stand zurückgehen !!!!

blatt7 :   induktionsschema als lemma instanzieren, und dann inst? für andere und dann grind
tccs 2 (über split): (lemma "split1") (grind)
tccs 3 (über split) : (induct-and-simplify l)
tccs (merge) : (lemma "merge-induct") (inst?) (split -1) (grind) , (falsches goal löschen mit delete),

occ(...,merge(...)) = occ(...)  : (expand merge) (lift-if) (split) (grind,grind) fall : beide listen nicht null : (skolem,flatten) (inst alles mit allgemeinem z) (expand merge in goal),

=== tcc's beweisen ===

C-cpt : status der tccs anzeigen
M-x show-tccs
C-cpp in show-tccs bei unfinished obligations


prelude.pvs : einige lemmas....
list_adt.pvs : listen lemmas....

I,J : [D -> boolean]  

% 2 teilmengen-funktionen

  idealI : AXIOM 

FORALL (a,b:D) : I(b) AND a <= b IMPLIES I(a)

 idealJ : AXIOM 

FORALL (a,b:D) : J(b) AND a <= b IMPLIES J(a)

 intersect(P,Q:[D->boolean]) : [D->boolean]

= LAMBDA (d:D) : P(d) AND Q(d)

% lambda : funtkion

% baut funktion zusammen, die zuerst P(d) aufruft, und dann das ergebnis AND verknüpft mit dem ergebnis Q(d)

 aufg4 : THEOREM  

FORALL (a,b:D) intersect(I,J)(b) AND a <= b IMPLIES intersect(I,J)(a)

zu Ü blatt 4 :

Spass :

befehl : SPASS datei.in

in pränex form bringen : -> durch /\ und \/ ersetzten,

klauseln(literale-disjunktion)

klauselmengen(klausel-konjunktion)

Ex aussen(links) : konstante einführen

Ex innen : funktion, die von allen vorherigen(äussereren) abhängt

TCCs ("type checking conditions") sind Formeln, die sich aus der Typüberprüfung ergeben. Sie müssen auch separat bewiesen werden, allerdings oft voll-automatisch.

Bsp:

 IF FORALL(n:nat): EXISTS(p,q:nat): prime(p) AND prime(q) AND p+q = n+4
    THEN 1 ELSE 0.5 
 ENDIF : nat

M-x show-tccs

M-x tcp

 "type check proof"  Versuche alle tccs zu automatisch zu beweisen.