IT/Description/libraries.tex

50 standard su cui lavorare. Essa � pre-caricata e aperta quando il sistema
57 un gestore di dimostrazione per dimostrazioni basate su tattiche; \ml{simpLib}, che fornisce
200 	a un'altra); \ml{LA} (un'astrazione di una variabile su un corpo),
303 	\holtxt{int\_add}, e su word � \holtxt{word\_add}. (Si noti
773 Questo significa che \holtxt{f\,univ(:'a)} � elaborato dal parser come \holtxt{f(univ(:'a))}, non come \holtxt{(f univ)(:'a)} (su cui il parser fallirebbe il controllo di tipo).
1251 \ml{term list * term}. Per partire su un nuovo goal, si da a
1347 \subsection{Spostare il fuoco su un differente subgoal o tentativo di dimostrazione}
1371 per l'interazione. La libreria attualmente si concentra su tre cose:
1421 che si conosce il termine su cui effettuare lo split, il suo tipo e i fatti associati sono
1434 termine su cui effettuare l'induzione � conosciuto, il suo tipo e i fatti associati sono
1453 	si esegue l'induzione su $n$, � permesso assumere che la propriet� valga per
1527 abbreviazioni\index{abbreviazioni!dimostrazione basata-su-tattche} nelle
1571 	delle dimostrazioni basate su tattiche.}
1690 in \ml{boolSimps} incorpora tutti i teoremi di riscrittura usuali desiderabili su formule
1745 il semplificatore ai goal (alternativamente, per eseguire dimostrazioni basate su tattiche
2046 Si noti che la sottrazione su numeri naturali funziona in modi che possono
2230 su insiemi. (In \ml{pred\_setSimps}.)
2334 condizioni collaterali su cui sta lavorando. Il semplificatore smette la dimostrazione
2335 su una condizione collaterale se nota una ripetizione in questo stack.
2584 condizioni $\mathit{ctxt}$ su sotto-equazioni. Un esempio di questo �
2621 Se aggiunta al semplificatore, questa regola prender� la precedenza su qualsiasi
2679 le sue procedure di normalizzazione su misura per l'addizione sui
2693 Si veda la Sezione~\ref{sec:simp-special-rewrite-forms} per maggiori informazioni su speciali
2766 propri contesti logici costruiti su misura.
2960 poi lavora su un termine, non applicher� mai pi� del numero dato
2988 	funzioni appropriate (ad esempio, la sostituzione) e le relazioni su
3091 funzionale. Se si vuole quindi `eseguire' programmi funzionali su
3110 \ml{EVAL\_TAC}. Queste dipendono su un database interno che archivia
3114 \holtxt{QSORT} su una lista concreta.
3127 come nell'esempio di sopra. Tuttavia, \ml{EVAL} pu� anche valutare funzioni su
3177 su un argomento ground, poi su un argomento simbolico.
3232 personalizzato, specializzato su un insieme fissato di definizioni. Il tipo
3244 Le funzioni definite per pattern-matching su numeri nello stile di Peano non sono
3247 usata su numerali, che � una notazione posizionale descritta nella
3249 lavorare su numeri di Peano. Per colmare questa lacuna, la funzione
3251 su numeri di Peano in una su numerali, che � il formato che
3271 \index{procedure di decisione!Aritemtica Presburger su numeri naturali}
3290 \index{procedure di decisione!Aritemtica Presburger su interi}
3464 \item[\ml{SIZES\_ss}] valuta un gruppo di funzioni che operano su tipi numerici, come \holtxt{dimindex} e \holtxt{dimword}.
3494 Il frammento \ml{BIT\_ss} converte \holtxt{BIT} in un test di appartenenza su un insieme di posizioni bit (pi� alte):
3505 Questa semplificazione fornisce supporto per il ragionamento circa le operazioni bitwise su lunghezze word arbitrarie. I frammenti aritmetico, logico e shift aiutano a ripulire espressioni word di base: