Lines Matching defs:di
23 di organizzazione per applicazioni \HOL{}. In generale, una libreria pu�
24 contenere una collezione di teorie, procedure di dimostrazione, e materiale
25 di supporto, come la documentazione. Alcune librerie forniscono semplicemente
26 procedure di dimostrazione, come \ml{simpLib}, mentre altre forniscono teorie e
27 procedure di dimostrazioni, tale che \ml{intLib}. Le librerie possono includere altre
34 qualunque parametro di sistema che sia appropriato per l'uso della libreria.
38 pi� di base � \ml{boolLib}, che supporta le definizioni della logica
40 suite di strumenti di definizione e ragionamento.
48 La libreria \ml{boss} fornisce una collezione base di teorie
49 standard e di procedure di dimostrazione di alto livello, e serve come una piattaforma
57 un gestore di dimostrazione per dimostrazioni basate su tattiche; \ml{simpLib}, che fornisce
58 una variet� di semplificatori; \ml{numLib}, che fornisce una procedura
59 di decisione per l'aritmetica; \ml{Datatype}, che fornisce
60 supporto di alto-livello per definire tipi di dato algebrici; e \ml{tflLib},
69 fine di ospitare un'ampia variet� di espressioni matematiche, \HOL{}
73 Il parser dei termini supporta l'inferenza di tipo, l'overloading, i binders, e
74 varie dichiarazioni di fixity (infisso, prefisso, suffisso, e
80 comportamento del parser e del prettyprinter di conseguenza � di solito alterato
81 da manipolazioni di grammatica.
85 Queste possono essere di due generi: \emph{temporanee} o \emph{permanenti}.
86 I cambiamenti temporanei dovrebbero essere usati nelle implementazioni di librerie, o nei
87 file di script per quei cambiamenti che l'utente non vuole far
89 sono appropriati per l'uso in file di script, e saranno forzati in tutte
99 di tipo) pu� essere ispezionata usando la funzione \ml{type\_grammar}.
117 legano sempre pi� debolmente dei gli operatori di tipo~($\nt{tyop}$) (e
118 e dei sottoscritti di tipo~($\tau\tok{[}\tau\tok{]}$)), cos� che
121 differenti, e gli infissi a diversi livelli di priorit� possono associare
124 di tipo, e manipolando la grammatica direttamente.}
128 \paragraph{Infissi di tipo}
131 nome di un operatore di tipo esistente (come \texttt{fun}). E' necessario
132 dare al simbolo binario un livello di precedenza e
135 \paragraph{Abbreviazioni di tipo}
136 \index{abbreviazioni di tipo}
138 Gli utenti possono abbreviare pattern di tipo comuni con delle \emph{abbreviazioni}.
145 Un'abbreviazione � un nuovo operatore di tipo, di qualsiasi numero di argomenti,
147 teoria leggera di numeri estesi con un infinito, in cui
152 nella Sezione~\ref{sec:theory-of-sets}, l'abbreviazione \holtxt{set}, di
164 estesa quando viene fatta una nuova definizione o una specifica di costante. (L'introduzione
165 di una nuova costante � discussa
167 qualsiasi identificatore pu� avere assegnato ad esso in ogni momento uno stato di parsing.
176 serie di fasi, ciascuna delle quali � influenzata dalla grammatica fornita.
177 Di solito questa grammatica � la grammatica globale di default, ma gli utenti possono
182 serie di token. Per maggiori informazioni sul lexing, si veda la Sezione~\ref{HOL-lex}.
185 mix-fix sono tradotte, creando una forma di ``sintassi
187 discusse nella Sezione~\ref{sec:parseprint:fixities} di sotto. Le forme
188 di sintassi concreta sono aggiunte alla grammatica con funzioni come
190 L'azione di questa fase di parsing � incarnata nella funzione
199 dato come \holtxt{thy\$ident}); \ml{APP} (un'applicazione di una forma
200 a un'altra); \ml{LA} (un'astrazione di una variabile su un corpo),
201 e \ml{TYPED} (una forma accompagnata da un vincolo di tipo\footnote{I
207 anche in grado di riferirsi alle costanti dando loro dei nomi nudi.
219 \ml{Absyn}, incluso \ml{APP}, prendono anche parametri di localizzazione.)
226 Se si usa la sintassi di ``quotation'' con un dollaro nudo,%
229 \index{token!sopprimere il comportamento di parsing dei|(}
231 allora questa fase del parser non tratter� le stringhe come parte di una
244 Senza il segno di dollaro, il parser della sintassi concreta si lamenterebbe
246 sinistro. Quando il risultato di successo del parsing � passato alla
251 Cos�, quello di sopra si potrebbe scrivere \holtxt{\holquote{(+)~x}} per avere
253 \index{token!sopprimere il comportamento di parsing dei|)}
255 L'utente pu� inserire a questo punto nel processo di parsing delle funzioni
256 di trasformazione intermedia sviluppate per proprio conto . Questo � fatto
261 La funzione dell'utente sar� di tipo \ml{Absyn~->~Absyn} e potr�
263 parsing, queste funzioni sono parte di una grammatica: se l'utente non vuole
269 Questo processo risulta in un valore del tipo di dati \ml{Preterm}, che
277 identificatore che occorro sul lato sinistro di una freccia di
278 una espressione case, o un identificatore che occorre all'interno di un pattern
279 di comprensione d'insieme. Una costante � una stringa che � presente nel dominio
293 L'``overloap map'' � una mappa da stringhe a liste di termini. I
294 termini di solito sono solo costanti, ma possono essere termini arbitrari (dando
296 Questa infrastruttura � usata per permettere ad un nome come \holtxt{+} di mappare a
297 costanti di addizione differenti in teorie come
301 pi� sui numeri naturali � di fatto chiamato \holtxt{+} (strettamente,
307 \index{inferenza di tipo!nel parser HOL@nel parser \HOL{}}
311 range della mappa di overload tipicamente avranno tipi differenti,
312 l'inferenza di tipo spesso eliminer� le possibilit� dalla lista. Se
313 rimangono pi� possibilit� dopo che l'inferenza di tipo � stata
318 Quando un termine nella mappa di overload � scelto come l'opzione migliore, �
325 \item[Inferenza di Tipo:] %
326 \index{inferenza di tipo!nel parser HOL@nel parser \HOL{}}%
328 questo attraverso le API per il tipo di dato \ml{term}. (In particolare,
333 parser � di trasformare le stringhe fornite dall'utente in termini. Per convenienza,
336 di sotto.)
338 In presenza di identificatori sottoposti a overload, l'inferenza di tipo pu� non essere
339 in grado di assegnare un tipo unico a tutte le costanti. Se esistono
343 Quando � stato completato il controllo di tipo di un \ml{Preterm}, la conversione finale da
355 E' possibile fare in modo che l'infrastruttura \HOL{} di parsing e stampa
368 di teoria che includono binding \ML{} (illegali) come \ml{val $\rightarrow$\_def =
370 \ml{...Theory.sml} che falliranno di compilare, anche se la chiamata a
372 l'uso di funzioni come \ml{set\_MLname}, probabilmente � una pratica
377 Se gli utenti hanno a disposizione dei font con il repertorio di caratteri appropriati per
384 di traccia \ml{"Unicode"} � $0$, la sintassi ASCII sar� usata per
401 il nome di una costante, o un token che appare in una regola di sintassi concreta
403 nome di una costante, allora, con la variabili di traccia abilitata, la stringa
405 stesso di un token di una regola di sintassi concreta, allora il comportamento � di
409 \paragraph{Regole di lexing con caratteri Unicode}
416 influenza il comportamento del lexer quando incontra delle stringhe di
418 i token si dividono quando la classe di caratteri cambia. Cos�, nella
427 il simbolo di negazione logica \holtxt{$\neg$} non associa; e
429 permettere a stringhe come \holtxt{$\lambda$x.x} di essere divise dal lexer in \emph{quattro} token.)
438 La ``mappa di overload'' menzionata in precedenza � di fatto una combinazione di
439 mappe, una per il parsing, e una per la stampa. La mappa di parsing � da
440 nomi a liste di termini, e determina come i nomi che appaiono in un
446 l'inferenza di tipo sceglier� da quelli che hanno tipi coerenti con
447 il resto del termine dato. Se la lista risultante contiene pi� di
451 Il caso d'uso pi� comune per la mappa di overload � di avere nomi mappati a
453 mappare la stringa \ml{"+"} alla nozione rilevante di addizione, ognuna delle
456 possibile mappare a istanze di costanti con specifici tipi. Cos�, la
458 essere di tipo \holquote{:bool}.
478 di tipo di dare i tipi (identici) appropriati a \ml{x} e \ml{y}.
480 dopo l'inferenza di tipo, allora il termine risultante sar�
482 sottostante del termine in memoria, esso sar� di fatto stampato come
485 Se il termine mappato nella mappa di overload contiene qualsiasi variabili libere,
487 se queste variabili hanno tipi polimorfici, allora le variabili di tipo in
489 di tipo.
491 \paragraph{Il pretty-printing e i pattern sintattici} La seconda parte della ``mappa di overload'' � una mappa da termini a stringhe, che specifica come
492 i termini dovrebbero essere trasformati indietro in identificatori. (Bench� di fatto
494 di risoluzione dei nomi, producendo qualcosa che � poi stampato
495 secondo la parte di sintassi concreta della grammatica data.)
497 Poich� il parsing pu� mappare nomi singoli in complicate strutture di termine,
498 la stampa deve essere in grado di ricondurre una complicata struttura di termine a
503 \footnote{Il matching eseguito � del primo ordine; per contro il matching di ordine superiore
512 Nell'esempio di sopra dell'operatore non-uguale-a, il pattern sar�
518 Non c'� alcun'altra finezza nell'uso di questa infrastruttura: matching
519 ``pi� grandi'', che coprono pi� di un termine hanno la precedenza. La difficolt�
521 \theoryimp{rich\_listTheory}. Per questioni di retro-compatibilit�
529 macro � impostata la mappa di overload contiene gi� un mapping dalla
531 accade con ogni definizione di costante). Ma dopo la chiamata
538 Piuttosto (supponendo che \holtxt{isPREFIX} sia di fatto la forma
539 di stampa preferita), la chiamata deve essere
543 cos� che il pattern di \ml{isPREFIX} � lungo quanto quella di \ml{IS\_PREFIX}.
547 \subsubsection{Vincoli di tipo}
550 \index{vincoli di tipo!nel parser HOL@nel parser \HOL{}}
553 \holtxt{bool}. Un tentativo di vincolare un
560 fallir� perch� entrambi i rami di un condizionale dovono essere dello stesso
561 tipo. I vincoli di tipo possono essere visti come un suffisso che lega pi�
562 strettamente di qualunque altra cosa eccetto l'applicazione di funzione. Cos� $\term\
568 L'inclusione di \holtxt{:} negli identificatori simbolici significa che pu�
582 lista di termini argomento [\holtxt{bool}, \holtxt{->}, \holtxt{bool},
591 un comportamento di parsing speciale:
598 \subsubsection{Inferenza di tipo}
601 \index{inferenza di tipo!nel parser HOL@nel parser \HOL{}|(}
605 per qualche tipo \holtxt{xty}. Dal momento che lo schema di tipo per \holtxt{=} �
606 \holtxt{'a -> 'a -> bool}, sappiamo che \holtxt{xty} di fatto deve essere
607 \holtxt{bool} perch� l'istanza di tipo sia ben formata. Sapendo
608 questo, possiamo dedurre che il tipo di \holtxt{x} deve essere \holtxt{bool}.
611 paragrafo, abbiamo condotto un assegnamento di tipo alla struttura di termine,
614 Cos�, \HOL{} usa un adattamento dell'algoritmo d'inferenza di tipo di Milner
616 di tipo, alle variabili di tipo non vincolate sono assegnati dei nomi da parte del sistema.
619 di tipo ai sotto termini rilevanti. Per situazioni complicate, si pu� assegnare la
623 delle variabili di tipo per proprio conto, si pu� impostare la variabile globale
625 l'esistenza delle variabili di tipo non assegnate alla fine dell'inferenza di tipo
634 Una misura limitata di risoluzione di overloading � eseguita dal parser
636 denota la negazione booleana nella teoria iniziale di \HOL, e denota anche
657 Per risolvere pi� scelte possibili � usato un meccanismo di priorit�.
661 vincoli di tipo espliciti. Nella seguente sessione, il
663 mentre nella seconda, un vincolo di tipo assicura che \holtxt{\~{}\~{}x} ha
689 Al fine di fornire qualche flessibilit� notazionale, le costanti sono disponibili in varie forme o {\it fixity}: oltre a essere costanti ordinarie (senza alcuna fixity), le costanti possono essere anche dei {\it binder}, {\it prefissi}, {\it suffissi}, {\it infissi}, o {\it closefix}.
693 Per esempio, nel momento in cui � introdotto, \verb-+- ha una precedenza di 500, mentre il pi� stretto binder moltiplicazione (\verb+*+) ha una precedenza di 600.
722 desiderato.) L'ordine di precedenza per l'insieme iniziale di infissi �
752 Mentre gli infissi appaiono tra i loro argomenti, i prefissi appaiono prima di essi.
753 Questo potrebbe inizialmente apparire la stessa cosa di quanto accade con la normale applicazione di funzione dove il simbolo alla sinistra semplicemente non ha alcuna fixity: $f$ in $f(x)$ non si comporta forse come un prefisso?
754 Di fatto tuttavia, in un termine come $f(x)$, dove $f$ e $x$ non hanno fixity, la sintassi � trattata come se ci fosse una invisibile applicazione di funzione infissa tra i due token: $f\cdot{}x$.
755 Questo operatore infisso lega pi� strettamente, cos� che quando si scrive $f\,x + y$, il risultato del parser � $(f\cdot{}x) + y$\footnote{Ci sono operatori infissi che legano pi� strettamente, il punto nella selezione di campo fa s� che $f\,x.fld$ sia elaborato dal parser come $f\cdot(x.fld)$.\index{tipi record!notazione di selezione del campo}}.
756 E' quindi utile permettere dei prefissi genuini cos� che gli operatori possano vivere a livelli di precedenza differenti rispetto all'applicazione di funzione.
757 Un esempio di questo � \verb+~+, la negazione logica.
758 Questo � un prefisso con una precedenza pi� bassa dell'applicazione di funzione.
766 poich� la precedenza di \verb+~+ � pi� bassa di quella dell'applicazione di funzione.
767 Il simbolo unario di negazione sarebbe anche tipicamente definito come un prefisso, se non altro per permettere di scrivere \[
770 (qualunque cosa sia {\it negop}) senza bisogno di parentesi extra.
772 Dall'altro lato, la sintassi \holtxt{univ} per l'insieme universale (si veda la Sezione~\ref{sec:theory-of-sets}\index{universal set}) � un esempio di un operatore prefisso che lega pi� strettamente dell'applicazione.
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).
779 sono sempre in grado di introdurli per loro conto se lo scelgono. I suffissi sono
783 operatori, sulla base delle loro precedenze, dando cinque risultati per il parsing di
803 Un esempio che si potrebbe usare nello sviluppo di una teoria della
804 semantica denotazionale sono le parentesi semantiche. Cos�, le infrastrutture di parsing
805 di \HOL{} possono essere configurate in modo da permettere di scrivere \holtxt{denotation x}
819 di fatto hanno fatto proprio questo. Tuttavia, se si vuole avere soltanto una
820 normale sostituzione uno-a-uno di una stringa per un'altra, non si pu�
822 pu� usare il meccanismo di overloading. Per esempio, sia
830 \item[Rendere l'addizione associativa a destra] Se si ha un numero di vecchi
833 � di rimuovere tutte le regole al livello dato della grammatica, e
847 \noindent Si noti che usiamo le versioni \ml{temp\_} di queste due
850 livello di precedenza con differenti associativit�, cos� dobbiamo
856 Il primo passo per andare in questa direzione � di guardare all'aspetto generale
857 delle espressioni di questa forma. In questo caso, sar�:
880 \item[Sintassi mix-fix sintassi per la sostituzione di termini:]
882 Qui ci� che si desidera � di essere in grado di scrivere qualcosa come:
886 denotando la sostituzione di $t_1$ per $t_2$ in $t_3$, magari
891 Dato che i letterali lista sono di fatto della classe
897 in modo che mappi a \holtxt{SUB $t_1$ $t_2$}, un valore di un tipo
900 l'esempio \textit{if-then-else} di sopra sarebbe
901 inappropriato, dal momento che permetterebbe di scrivere
918 \index{parsing, della logica HOL@parsing, della logica \HOL{}!nascondere lo status di costante|(}
923 La seguente funzione pu� essere usata per nascondere lo status di costante di un
934 \noindent La valutazione di \ml{hide "$x$"}
936 lessicali lo permettano), anche se $x$ � il nome di una costante nella teoria attuale
940 \index{variabili, nella logica HOL@variabili, nella logica \HOL{}!con nomi di costante}
942 con lo stesso nome di costanti dichiarate in precedenza (o incorporate)
945 la stampa rimuovendo il nome dato dalla ``mappa di overload'' descritta
946 di sopra nella Sezione~\ref{sec:parser:architecture}. Si noti che l'effetto
947 di \ml{hide} � \emph{temporaneo}; i suoi effetti non persistono nelle
972 \noindent controlla se una stringa � il nome di una costante nascosta.
975 \index{parsing, della logica HOL@parsing, della logica \HOL{}!nascondere lo status di costante nel|)}
990 \index{profondit� di stampa di default, per la logica HOL@profondit� di stampa di default, per la logica \HOL{}|(}
992 \noindent La profondit� di default della stampa � $-1$ che � intesa significare
994 massima di stampa sono stampati come \holtxt{...}. Per esempio:
1010 \index{profondit� di stampa di default, per la logica HOL@profondit� di stampa di default, per la logica \HOL{}|)}
1016 \index{parsing, della logica HOL@parsing, della logica \HOL{}!della sintassi di quotation|(}
1018 parser in forme speciali conosciute come \emph{quotation}. Una quotation di base
1021 piuttosto brutti a causa dello speciale filtro che � fatto di questi
1039 carattere non spazio dopo il delimitatore principale deve essere un segno di deu punti.
1051 L'espressione legata alla variabile ML \ml{t} di sopra di fatto � espansa
1054 in un'applicazione di \ml{Parse.Type} alla quotation \ml{`:'a -> bool`}.
1057 che esse possono includere caratteri di nuova riga e backslash senza
1058 richiedere caratteri speciali di escape. Le nuove righe occorrono ogni volta che i termini vanno oltre
1060 rappresentazione di $\lambda$, ma anche nella sintassi per la congiunzione e
1063 Se una quotation deve includere un carattere di accento grave, allora questo dovrebbe
1064 essere fatto usando il carattere di escape proprio della sintassi della quotation, il
1066 leggermente pi� complicate. Se una sequenza di caret � seguita dallo
1067 spazio vuoto (incluso un carattere di nuova riga), allora quella sequenza di caret �
1068 passata al parser di HOL senza modifiche. Altrimenti, un singolo caret si pu�
1102 suggerito nell'ultimo esempio di sopra). All'interno di una quotation, l'espressioni
1107 (dove $t$ � un'espressione \ML\ di tipo
1109 \index{controllo di tipo, nella logica HOL@controllo di tipo, nella logica \HOL{}!antiquotation nel}
1117 valore \ML{} di $t$. Per esempio, {\small\verb+``x \/ ^(mk_conj(``y:bool``, ``z:bool``))``+}
1118 � valutata allo stesso termine di {\small\verb+``x \/ (y /\ z)``+}. L'uso
1151 \noindent Le quotation sono polimorfiche, e la variabile di tipo di una
1154 sottoposti ad antiquotation, l'antiquotation di un tipo all'interno di una quotation di termine richiede l'uso di
1183 parsing di \HOL{} dei termini e dei tipi nella release Taupo (una delle
1184 release HOL3) e al di l� del punto di vista di un utente che non
1191 \item La precedenza delle annotazioni di tipo � completamente cambiata. Ora
1192 � un suffisso molto stretto (bench� con una precedenza pi� debole di quella
1193 associata con l'applicazione di funzione), invece di uno debole.
1196 parsata come un'annotazione di tipo che si applica solo a \verb+y+. Questo
1200 \] al posto di \[
1202 \] dove le parentesi extra si sono dovute aggiungere solo per permettere di
1203 scrivere una forma di vincolo che occorre frequentemente.
1208 a sinistra. Questo porta il parser di \HOL{} in linea con la pratica
1212 di \HOL, l'eguaglianze in questo contesto hanno una precedenza di bindig differente
1221 letterali non possono essere usati come variabili all'interno di scopi di binding.
1225 \section{Un Semplice Gestore di Dimostrazione Interattivo}\label{sec:goalstack}
1227 Il \emph{goal stack} fornisce una semplice interfaccia di dimostrazione interattiva
1230 di queste informazioni. L'implementazione dei goalstack qui riportati � un
1231 ridisegno della concezione originale di Larry Paulson.
1236 punto focale delle operazioni di dimostrazione all'indietro. il tipo \ml{proofs} pu� essere
1237 considerato come una lista di goalstack indipendenti. La maggior parte delle operazioni agiscono sulla
1241 \subsection{Avviare un goalstack di dimostrazione}
1253 punto focale di ulteriori operazioni.
1256 invoca il parser automaticamente, e non permette al goal di
1259 La chiamata a \ml{set\_goal}, o \ml{g}, aggiunge un nuovo tentativo di dimostrazione a
1260 quelli esistenti, \textit{cio�}, al posto di sovrascrivere il tentativo
1261 di dimostrazione attuale, il nuovo tentativo � impilato in cima.
1273 Come si fa dunque di fatto a fare una dimostrazione goalstack? Nella maggior parte dei casi,
1277 spiegazione delle tattiche invalide, si veda il Capitolo 24 di \& Melham.)
1294 Spesso (siamo tentati di dire {\it di solito}!) si prende una strada sbagliata
1303 dei tentativi di dimostrazione che sono sbagliati; per questo c'� \ml{drop},
1304 che si sbarazza del tentativo di dimostrazione corrente, e \ml{dropn}, che
1305 elimina i primi $n$ tentativi di dimostrazione.
1308 Ogni tentativo di dimostrazione ha la sua \emph{lista-di-annullamento} degli stati
1309 precedenti. La lista di annullamento per ciascun tentativo � di dimensione fissata (inzialmente
1310 12). Se si vuole impostare questo valore per il tentativo corrente di dimostrazione, si pu�
1311 usare la funzione \ml{set\_backup}. Se la dimensione della lista di
1312 backup � impostata essere pi� piccola di quanto sia attualmente, la lista di annullamente sar�
1332 sintesi di ogni tentativo di dimostrazione.
1338 Per ottenere il o i top goal di un tentativo di dimostrazione, si usi \ml{top\_goal}
1339 e \ml{top\_goals}. Per ottenere il goal originale di un tentativo di dimostrazione,
1343 continua ad esistere (e anche la sua lista-di-annullamento): il suo compito principale ora � quello di
1347 \subsection{Spostare il fuoco su un differente subgoal o tentativo di dimostrazione}
1363 \section{Dimostrazione di Alto Livello---\texttt{bossLib}}
1369 La libreria \bossLib\ introduce alcuni degli strumenti di dimostrazione di teoremi
1370 pi� ampiamente utilizzati in \HOL{} e li fornisce di un'interfaccia conveniente
1372 definizione di datatype e funzioni; operazioni interattive di dimostrazione
1373 di alto livello, e composizione di ragionatori automatici. Il caricamento di \bossLib\
1378 \subsection{Supporto per passi di dimostrazione di alto livello}
1382 l'applicazione delle funzionalit� di \HOL{} sottostanti.
1385 \index{Cases_on (tattica ML di case-split)@\ml{Cases\_on} (tattica \ML{} di case-split)}
1398 database sottostante \ml{TypeBase} e restituir� utili regole di riscrittura per
1399 quel tipo. Le regole di riscrittura del datatype sono costruite a partire dai
1400 teoremi di iniettivit� e distinzione, insieme con la definizione di costante
1401 case. Le tattiche di semplificazione \ml{RW\_TAC}, \ml{SRW\_TAC},
1403 teoremi. Altre tattiche usate con altri \simpset{} avranno bisogno di questi
1406 \index{teoremi d'induzione, nella logica HOL@teoremi d'induzione, nella logica \HOL{}!per tipi di dato algebrici}
1410 se il suo tipo � quello di un datatype conosciuto, � estratta e applicata
1423 split. Se alcune delle variabili libere di $M$ sono legate nel goal, � fatto un tentativo
1425 vigore. Infine, $M$ non ha bisogno di apparire nel goal, bench� dovrebbe almeno
1427 che la tattica \ml{Cases\_on} � pi� generale di \ml{Cases}, ma
1442 pi� generale di \ml{Induct}, ma richiede che le venga dato un termine
1454 \emph{tutti} gli $m$ pi� piccoli di $n$. Formalmente: $\forall P.\ (\forall x.\
1456 P\,x$. Questo permette di usare l'ipotesi d'induzione pi� di
1462 Per esempio, se si volesse fare un'induzione sulla lunghezza di una lista
1478 ma il punto di \ml{bossLib} � di fornire un livello di astrazione cos�
1482 potenti sono descritte nel dettaglio nelle sezioni di sotto.)
1496 \texttt{PROVE\_TAC}) prende una lista di teoremi e un termine, e tenta
1497 di dimostrare il termine usando un ragionatore al primo ordine. Le due funzioni
1498 \ml{METIS} eseguono la stessa funzionalit� ma usano un metodo di dimostrazione
1501 Sezione~\ref{sec:mesonLib} di sotto. Il sistema \ml{METIS} � descritto
1504 di decisione che (al meno) gestisce enunciati dell'aritmetica lineare.
1518 \index{RW_TAC@\ml{RW\_TAC}} La tattica di riscrittura \ml{RW\_TAC} lavora
1534 l'aggiornamento di ``frammenti \simpset{} '' (valori \ml{ssfrag}) e
1536 sistema, le performance di \ml{RW\_TAC} ne possono risentire perch�
1537 aggiunge ripetutamente tutti i teoremi di riscrittura per i tipi conosciuti in un
1538 \simpset{} prima di attaccare il goal. Dall'altro lato,
1539 \ml{SRW\_TAC} carica le riscritture nel \simpset{} al di sotto di
1543 \ml{bossLib} fornisce un numero d'insiemi di semplificazione. Il
1547 I simpset forniti da \bossLib{} aumentano strettamente di forza:
1550 per costruire un nuovo \simpset{} da un \simpset{} e una lista di
1551 teoremi dati. La tecnologia di semplificazione di \HOL{} � ulteriormente descritta nella
1552 Sezione~\ref{sec:simpLib} di sotto e nelle \REFERENCE.
1567 se la de-costruzione di $\ \vdash M$ espone delle disgiunzioni.) Cos�
1568 \ml{by} permette di mischiare un utile stile di ragionamento `asserzionale' o `Mizar-like'
1581 \index{procedure di decisione!logica del primo ordine}
1583 La dimostrazione del primo ordine � una potente tecnica di dimostrazione di teoremi che pu�
1595 metodo model-elimination per trovare dimostrazioni di goal nella logica
1605 Ciascuna di quest tattiche tenta di dimostrare il goal. Esse o avranno
1607 il fattore di ramificazione nello spazio di ricerca � alto, le tattiche
1610 Tutte le tattiche \texttt{meson} prendono una lista di teoremi. Questi
1611 fatti extra sono usati dalla procedura di decisione per aiutare a dimostrare il goal.
1619 per una dimostrazione di profondit� non pi� alta di un parametro $d$. Il
1620 comportamento di default per \ml{MESON\_TAC} e \ml{ASM\_MESON\_TAC} � di iniziare $d$
1621 a 0, incrementarlo di uno ogni volta che una ricerca fallisce, e di fallire se
1625 di \ml{step}, e rinuncia quando $d$ eccede \ml{max}.
1628 normalizzazione, prima di passare un goal e le sue assunzioni a
1629 \ml{ASM\_MESON\_TAC}. A causa di questa normalizzazione, nella maggior parte
1637 \index{metodo di risoluzione per la logica del primo ordine}
1639 La libreria \ml{metis} � un'implementazione del metodo di risoluzione
1640 per trovare dimostrazioni di goal nella logica del primo ordine. Ci sono due
1650 Entrambe le funzioni prendono una lista di teoremi, e questi sono usati come lemmi
1658 La famiglia \texttt{metisLib} di strumenti di dimostrazione implementano la risoluzione
1659 ordinata e il calcolo di paramodulazione ordinata per la logica del primo ordine,
1660 che di solito li rende pi� adatti a goal che richiedono ragionamenti di eguaglianza
1668 Il semplificatore � il motore di riscrittura pi� sofisticato in \HOL{}. E'
1669 raccomandato come un cavallo di battaglia di scopo generale durante la dimostrazione di teoremi
1670 interattiva. Come strumenti di riscrittura, il ruolo generale del semplificatore
1671 � di applicare teoremi della forma generale
1675 a termini, rimpiazzando le istanze di $l$ nel termine con $r$. Cos�, la
1676 ruotine base di semplificazione � una \emph{conversione}, che prende un termine
1680 La conversione di base �
1686 Il primo argomento, un \simpset, � il modo standard di fornire una
1687 collezione di regole di (e altri dati, che saranno spiegati di sotto) al
1689 di \HOL{}. Per esempio, il \simpset{} \ml{bool\_ss}
1690 in \ml{boolSimps} incorpora tutti i teoremi di riscrittura usuali desiderabili su formule
1700 anche capace di eseguire semplificazioni che non sono esprimibili come
1714 Il secondo argomento a \ml{SIMP\_CONV} � una lista di teoremi da
1715 aggiungere al \simpset fornito, e da aggiungere come regole di riscrittura addizionali.
1717 le loro proprie riscritture. Se un particolare insieme di teoremi � usato spesso come
1722 afferma che $p(m + n) = pm + pn$, non fa parte di alcun \simpset{} standard
1723 di \HOL{}. Questo perch� pu� causare un aumento poco attraente nella
1724 dimensione del termine (ci sono due occorrenze di $p$ al lato destro
1739 \subsection{Tattiche di semplificazione}
1752 \ml{SIMP\_TAC} � la tattica di semplificazione pi� semplice: essa tenta di
1754 dato e i teoremi aggiuntivi. Non � niente di pi� che il
1756 di tattica attraverso l'uso della funzione standard \ml{CONV\_TAC}.
1763 del goal come regole di riscrittura extra. Cos�:
1785 regola di riscrittura addizionale, e ha sostituito la \holtxt{x} di \holtxt{P x}
1787 � convertita in regole di riscrittura nello stesso modo dei teoremi passati nella
1795 La tattica \ml{FULL\_SIMP\_TAC} semplifica non solo la conclusione di
1799 assunzione � ri-aggiunta alla lista di assunzioni del goal con la
1809 sar� l'assunzione aggiunta pi� di recente. Vista alla luce della
1810 stampa dei goal di \ml{goalstackLib}, \ml{FULL\_SIMP\_TAC} si fa
1813 La seguente sessione dimostra un uso semplice di \ml{FULL\_SIMP\_TAC}:
1867 Nel secondo di questi, l'assunzione \holtxt{x = 4} ha ulteriormente
1873 Nonostante il suo tipo sia lo stesso delle tattiche di semplificazioni gi�
1879 ma anche con tutte le regole di riscrittura dalla \ml{TypeBase}, e
1898 tattiche di semplificazione. Non prende un \simpset{} come un argomento.
1901 teoremi forniti come il secondo argomento di \ml{SRW\_TAC} sono trattati nello
1902 stesso modo delle altre tattiche di semplificazione. Infine, la
1904 sottostante, permettendo all'utente di fondere capacit� di semplificazione
1907 Per esempio, per includere la procedura di decisione Presburger, si potrebbe
1914 I frammenti \Simpset{} sono descritti di sotto nella
1917 La tattica \ml{SRW\_TAC} esegue la stessa combinazione di semplificazione e
1925 di riscritture non utilizzate non � mai un problema: la presenza di riscritture che
1926 fanno la cosa sbagliata pu� essere causa di maggiore irritazione.
1931 \HOL{} � fornito con un numero di \simpset{} standard. Ognuno di questi �
1932 accessibile dall'interno di \ml{bossLib}, bench� alcuni si originano in altre
1941 non contiene del tutto teoremi di riscrittura, e gioca il ruolo di una tabula
1943 \simpset{} completamente nuovo, \ml{pure\_ss} � un punto di partenza possibile.
1944 Il \simpset{} \ml{pure\_ss} ha solo due componenti: regole di congruenza
1946 i teoremi in regole di riscrittura. Le regole di congruenza sono ulteriormente descritte
1947 nella Sezione~\ref{sec:advanced-simplifier}; la generazione di regole
1948 di riscrittura da teoremi � descritta nella
1951 \index{bool_ss (insieme di semplificazione)@\ml{bool\_ss} (insieme di semplificazione)}
1955 regole di riscritture per i connettivi booleani, e poco altro. Esso
1956 contiene tutti i teoremi di de~Morgan per spostare le negazioni tra i
1962 argomenti. (Una di queste regole � \holtxt{|- T /\bs{} p = p}.)
1964 Come nell'esempio di sopra, \ml{bool\_ss} esegue anche
1965 delle $\beta$-riduzioni e svolgimenti di un solo punto. Questi ultimi trasformano termini
1976 Infine, \ml{bool\_ss} include anche regole di congruenza che permettono
1977 al semplificatore di fare delle assunzioni aggiuntive quando sono semplificate
1979 ulteriormente nella Sezione~\ref{sec:simplifier-rewriting} di sotto, ma pu� essere
1995 \index{std_ss (insieme di semplificazione)@\ml{std\_ss} (insieme di semplificazione)}
1998 regole di riscrittura pertinenti ai tipi di somme, coppie, option e
2012 con valori ground, e anche includere una suite di ``riscritture ovvie''
2026 \index{arith_ss (insieme di semplificazione)@\ml{arith\_ss} (insieme di semplificazione)}
2029 \ml{std\_ss} aggiungendo la capacit� di decidere formule dell'aritmetica
2031 coefficienti , e ri-ordinazione di addendi). La sottostante procedura di decisione
2033 Sezione~\ref{sec:numLib} di sotto.
2062 \index{list_ss (insieme di semplificazione)@\ml{list\_ss} (insieme di semplificazione)}
2065 teoremi di riscrittura circa il tipo delle liste a \ml{arith\_ss}. Queste
2090 simbolico di scopo generale per termini che assomigliano in grande misura a quelli
2091 che appaiono in un linguaggio di programmazione funzionale. Si noti che
2093 la Sezione~\ref{sec:computeLib} di sotto); \ml{computeLib} � pi�
2106 \index{srw_ss (insieme di semplificazione)@\ml{srw\_ss} (insieme di semplificazione)}
2111 Questo uso di un tipo funzione permette al \simpset{} sottostante di essere
2112 archiviato in una reference \ML{}, e permette ad esso di essere aggiornato
2115 \ml{SIMP\_CONV~bool\_ss} � la stessa routine di semplificazione ovunque
2120 cambia, e il comportamento di \ml{SIMP\_CONV} applicato a
2121 \ml{(srw\_ss())} cambia con esso. La filosofia di sviluppo dietro
2154 Le stringhe passate a \ml{export\_rewrites} sono i nomi di teoremi
2155 nell'attuale segmento di teoria (quelli che saranno esportati quando
2179 (come l'aritmetica esegita nell'esempio di sopra). Non
2180 include procedure di decisione che possono esibire performance occasionalmente
2182 dovrebbero essere aggiunte manualmente a quelle invocazioni di semplificazione che ne
2189 Il frammento \simpset{} � il blocco base di costruzione usato per
2198 il \simpset{} \ml{pure\_ss} o uno dei sui discendenti al fine di
2199 selezionare la funzione ``filtro'' di default per convertire teoremi in
2200 regole di riscrittura. (Questo processo di filtro � descritto di sotto nella
2203 Per le teorie principali (o gruppi di esse), una collezione di
2204 frammenti \simpset{} rilevanti si trova di solito nel modulo \ml{<thy>Simps},
2222 \ml{CONG\_ss} & Regole di congruenza per l'implicazione e le espressioni
2226 La procedura di decisione sui numeri naturali
2233 \caption{Alcuni dei frammenti \simpset{} standard di \HOL{}}
2255 frammento che include solo una lista di riscritture:
2266 descrive l'azione di riscrittura in maggior dettaglio.
2269 \subsubsection{Riscrittura di base}
2272 Data una regola di riscrittura della forma \[
2275 il semplificatore eseguir� una scansione dall'alto verso il basso del termine di input $t$,
2276 cercando per dei \emph{match}~(si veda la Sezione~\ref{sec:simp-homatch} di sotto)
2277 di $\ell$ all'interno di $t$. Questo match occorrer� in un sotto termine di $t$
2279 istanziazione � applicata alla regola di riscrittura, il risultato sar� una nuova
2288 alcun match ulteriore per le regole di riscrittura del semplificatore. La
2289 strategia di attraversamento �
2292 Mentre c'� un qualsiasi match per le regole di riscrittura archiviate a questo livello,
2294 di riscrittura sono applicate, eccetto quando un \simpset{}
2297 certa misura di overloading della riscrittura nella costruzione dei
2302 attraversati a questo passo pu� essere controllato da \emph{regole di
2304 di sotto)
2306 completamente, si provi un'altra fase di riscrittura a questo livello. Se questo fallisce,
2308 qualsiasi procedura di decisione incorporata (si veda
2309 la Sezione~\ref{sec:simp-embedding-code}). Se la fase di riscrittura o
2310 qualsiasi delle procedure di decisione ha alterato il termine, ri ritorni al
2311 passo~\ref{enum:simp-traverse-toplevel}. Altrimenti di termini.
2317 La descrizione di sopra � una leggera semplificazione dello stato reale delle
2319 essa realmente usa regole di riscrittura \emph{condizionali}. Questi sono teoremi
2325 del termine, tenta di scaricare la condizione $P$. Se il
2326 semplificatore pu� semplificare il termine $P$ a vero, allora l'istanza di
2328 istanziazione di $r$.
2332 regola di riscrittura condizionale. Per fermare eccessive applicazioni
2333 ricorsive, il semplificatore tiene traccia di uno stack di tutte le
2338 di usare.
2343 scaricare queste, in particolare se include una procedura di decisione
2352 \holtxt{(k~MOD~(x~+~1))~MOD~(x~+~1)}: la procedura di decisione
2356 forma descritta di sopra � una scelta appropriata. Una riscrittura scelta male
2358 che perde tempo nel tentare di dimostrare condizioni collaterali impossibili. Per
2364 buon strumento per eseguire ragionamenti di transitivit�. (Si provi invece uno strumento
2367 \subsubsection{Generare regole di riscrittura per i teoremi}
2373 \ML{} (\ml{SIMP\_CONV}, \ml{ASM\_SIMP\_TAC} ecc) che prendono liste di
2376 trasformati prima di essere usati. Le trasformazioni applicate sono
2384 Piuttosto, il semplificatore trasformer� i suoi teoremi di input per estrarre
2385 le riscritture di questa stessa forma. L'esatta trasformazione eseguita �
2392 � di tipo \ml{controlled\_thm~->~controlled\_thm~list}, ed � applicata
2396 (Un teorema ``controllato'' � uno che � accompagnato da un pezzo di
2397 dati di ``controllo'' che esprimono il limite (se ne esiste uno) sul numero di volte
2399 per come gli utenti possono introdurre questi limiti. Il tipo di ``controllo''
2404 un teorema di eguaglianza, o qualche altra forma booleana. Per esempio,
2415 Questo teorema si trasforma in due regole di riscrittura \[
2450 La restrizione che il lato destro di una tale regola non sia esso stesso
2451 un'eguaglianza � una semplifice euristica che previene alcune forme di looping.
2454 \subsubsection{Regole di riscrittura di matching}
2457 Dato un teorema di riscrittura $\vdash \ell = r$, il primo passo di
2458 esecuzione di una riscrittura � determinare se $\ell$ pu� o meno essere
2466 \index{matching di ordine superiore} \index{matching!di ordine superiore} Il semplificatore
2467 usa una speciale forma di matching di ordine superiore. Se un pattern
2468 include una variabile di qualche tipo funzione (diciamo $f$), e quella variabile
2482 Un matching di ordine superiore di questo genere rende pi� facile esprimere i risultati
2483 dei movimenti dei quantificatori come regole di riscrittura, e avere queste regole applicate dal
2489 ha due variabili di un tipo funzione ($P$ e $Q$), ed entrambe sono
2502 sulla regola di riscrittura, si produce il teorema \[
2508 Un altro esempio di una regola che il semplificatore user� con successo �
2514 regola pu� essere vista come un'implementazione di un metodo per muovere le astrazioni
2515 al di sopra delle composizioni di funzione.
2517 Un esempio di un possibile lato sinistro che \emph{non} matchare come
2527 \subsubsection{Regole di congruenza}
2529 \index{semplificazione!regole di congruenza}
2530 \index{regole di congruenza!nella semplificazione}
2531 Le regole di congruenza controllano il modo in cui il semplificatore traversa un termine.
2534 contesto contenitore. Le regole di congruenza pi� semplici sono incorporate nel
2536 astrazione. A questo livello fondamentale, queste regole di congruenza
2537 sono poco di pi� che le regole d'inferenza \ml{ABS}
2553 Ulteriori regole di congruenza dovrebbero essere aggiunte al semplificatore nella forma
2554 di teoremi, attraverso il campo \ml{congs} dei record passati al
2555 costruttore \ml{SSFRAG}. Tali regole di congruenza dovrebbero essere della forma
2569 Per esempio, la forma teorema di \ml{MK\_COMB} sarebbe
2573 e la forma teorema di \ml{ABS} sarebbe
2579 di congruenza gestire variabili legate. Dal momento che le regole di congruenza sono
2580 matchate con il match di ordine superiore della Sezione~\ref{sec:simp-homatch},
2584 condizioni $\mathit{ctxt}$ su sotto-equazioni. Un esempio di questo �
2585 la regola di congruenza (che si trova in \ml{CONG\_ss}) per le implicazioni. Questa
2604 Questa regola permette di assumere la guardia quando si semplifica il
2605 ramo-vero del condizionale, e di assumere la sua negazione quando si
2608 Le assunzioni contestuali da regole di congruenza sono trasformate in
2612 Le regole di congruenza possono essere usate per ottenere un numero di interessanti
2623 \ml{CONG\_ss}, diciamo) e far� s� che il semplificatore di scendere solo
2632 i rami di un condizionali fino a quando la guarda di quel condizionale � semplificata
2674 \index{arith_ss (insieme di semplificazione)@\ml{arith\_ss} (insieme di semplificazione)}
2679 le sue procedure di normalizzazione su misura per l'addizione sui
2683 I teoremi AC possono essere aggiunti ai \simpset{} anche attraverso la lista di teoremi parte
2684 dell'interfaccia della tattica e della conversione, usando la forma speciale di riscrittura
2694 forme di riscrittura.
2699 Il semplificatore dispone di due modi diversi in cui il codice dell'utente pu� essere
2700 incorporato nel suo attraversamento e semplificazione dei termini di input. Incorporando
2705 Il pi� semplice dei due metodi permente al semplificatore di includere
2707 campo {convs} dei frammenti \simpset{}. Questo campo prende liste di
2708 valori di tipo
2719 � acceso. Se la conversione � applicata, e se il livello di traccia del
2720 semplificatore � maggiore di o uguale al campo \ml{trace}, allora sar�
2724 Il campo \ml{key} del record di sopra � usato per specificare i
2727 Altrimenti, la conversione � applicata a posizioni di termine che matchano il
2728 pattern fornito. Il primo componente del pattern � una lista di
2730 del pattern. Il secondo componente � il pattern di termine stesso. Il matching
2731 verso questa componente \emph{non} � fatto dal match di ordine superiore della
2732 Sezione~\ref{sec:simp-homatch}, ma da una ``term-net'' di ordine superiore.
2733 Questa forma di matching non cerca di essere precisa; essa � usata per
2739 Infine, la conversione stessa. Molti usi di questa infrastruttura sono per aggiungere
2740 normali conversioni \HOL{} (di tipo \ml{term->thm}), e questo pu� essere
2742 conversione \ml{myconv}, l'idioma standard � di scrivere
2746 primo permette al codice dell'utente di richiamare il semplificatore, passando
2748 L'argomento \ml{term} deve essere di tipo \holtxt{:bool}, e la chiamata
2751 futura versione di \HOL{} ma per come stanno le cose ora, la chiamata ricorsiva pu�
2753 � responsabilit� dell'utente passare uno stack appropriatamente aggiornato di
2757 (un'istanza di $\vdash t = t$). Questo far� andare in loop il
2761 \paragraph{Procedure di decisione consapevoli del contesto}
2765 conversioni, e permette anche al codice utente di costruire e mantenere i suoi
2768 Il campo \ml{dprocs} richiede liste di valori di tipo
2783 ``tipo universale'', capace di archiviare dati di qualsiasi tipo. Per esempio,
2784 se il dato desiderato � una coppia di un intero e un booleano, allora si
2792 ampio. Infatti, solo le funzioni che accedono e creano contesti di questa
2793 forma hanno bisogno di vederla. Per esempio:
2801 Quando crea un valore di tipo \ml{reducer}, l'utente deve fornire un
2803 chiamata dal meccanismo di attraversamento del semplificatore per dare ad ogni
2804 procedura di decisione incorporata accesso ai teoremi che rappresentano la nuova informazione
2805 di contesto. Per esempio, questa funzione � chiamata con i teoremi dalle
2807 dagli argomenti lista di teoremi a tutt le varie funzioni di
2808 semplificazione. Mentre un termine � attraversato, le regole di congruenza che governano
2817 risolutore di condizione collaterale, l'attuale contesto della procedura di decisione. e
2820 dall'utente. La potenza dell'astrazione del riduttore � di avere accesso a
2821 un contesto che pu� essere costruito in modo appropriato per ogni procedura di decisione.
2823 Le procedure di decisione sono applicate per l'ultima volta quando un termine � incontrato dal
2825 gia� eseguito un ricorsione in ogni sotto-termine e ha tentato di fare quante pi� riscritture
2827 dall'alto verso il basso, le procedure di decisione saranno applicate dal basso verso l'alto e
2830 Come per le conversioni-utente, le procedure di decisione devono sollevare un'eccezione
2831 piuttosto che restituire istanze di riflessivit�.
2833 \subsubsection{Forme speciali di riscrittura}
2838 di teorema. Questi teoremi speciali possono poi essere passati negli
2839 argomenti lista-di-teoremi delle tattiche di semplificazione.
2842 le regole di congruenza si pu� accedere in questo modo. Piuttosto che costruire un
2843 frammento \simpset{} custom che include le regole AC o di congruenza
2857 appare tra i teoremi passati a una tattica di semplificazionie, allora
2858 il semplificatore eseguir� una normalizzazione-AC di disgiunzioni. La
2859 funzione \ml{Cong} fornisce un'interfaccia analoga per l'aggiunta di
2860 nuove regole di congruenza.
2863 \index{Once (controllo delle applicazioni di riscrittura)@\ml{Once} (controllo delle applicazioni di riscrittura)|pin}
2864 \index{Ntimes (controllo delle applicazioni di riscrittura)@\ml{Ntimes} (controllo delle applicazioni di riscrittura)|pin}
2866 numero di volte che una riscrittura individuale sar� applicata.
2880 Abbiamo gi� visto (Sezione~\ref{sec:simp-congruences} di sopra) che
2881 la tecnologia di congruenza del semplificatore pu� essere usata per forzare il
2883 di sopra ha discusso come un regola di congruenza potrebbe essere usata per assicurare che
2887 l'altro di un connettivo binario (spesso, questo connettivo �
2891 avr� un simbolo funzione attaccato a una sequenza di variabili, ad esempio:
2897 Teoremi di una forma analoga sono anche restituiti come i teoremi
2900 Qualunque sia la loro origine, tali teoremi sono il classico esempio di
2902 Tuttavia, questo pu� non essere sufficiente: si pu� desiderare di dimostrare un risultato
2909 (Con le relazioni, il goal pu� spesso rappresentare un'implicazione al posto di
2911 l'istanza di \holtxt{f} sulla sinistra, lasciando l'altra occorrenza
2912 da sola. Usare \ml{Once} espander� solo una di esse, ma senza
2915 La soluzione a questo problema � di usare speciali regole di congruenza,
2924 costruiscono regole di congruenza per forzare la riscritture alla sinistra o alla destra di
2935 la semplificazione sulla sinistra o sulla destra di un'eguaglianza rispettivamente.
2936 Queste sono definite essere solo applicazioni di \ml{SimpL} e \ml{SimpR}
2940 all'occorrenza pi� alta di un operatore. Inoltre, l'operatore pi� alto nel
2941 termine non ha bisogno di essere quello della regola di congruenza. Questo comportamento �
2942 una conseguenza automatica dell'implementazione in termini di regole
2943 di congruenza.
2949 Oltre alle forme-di-teoremi \ml{Once} and \ml{Ntimes} appena
2950 discusse, che limitano il numero di volte che una particolare riscrittura �
2951 applicata, il semplificatore pu� anche essere limitato nel numero totale di
2961 di riscritture a quel termine. Quando sono usate riscritture condizionali, la
2964 delle regole di congruenza, delle conversioni e delle procedure
2965 di decisione fornite dall'utente pesano tutte negativamente sul limite.
2967 Quando il semplificatore cede il controllo a una conversione o a una procedura di
2970 con le procedure di decisione aritmetica), ma l'uso di \ml{limit} �
2980 modo molto potente di lavorare con relazioni di transizione nella semantica
2986 $\lambda$-calcolo. Questo implicher� la definizione di un nuovo tipo
2991 regole di congruenza come
3003 dato termine iniziale si pu� ridurre a una particolare destinazione � di solito
3005 di sopra, ma anche quelle dei teoremi che descrivono la chiusura riflessiva e
3022 la riflessivit� di \bred{} dimostrer� il risultato desiderato. I teoremi
3023 come questi, che giustificano il cambio da una relazione di riscrittura a
3027 i cinque teoremi di sopra, e dimostrare automaticamente risultati come
3034 Inoltre, si avranno probabilmente vari teoremi di riscrittura
3035 che si vorranno usare oltre a quelli specificati di sopra. Per
3055 \item[\texttt{weakenings}] Una lista di congruenze d'indebolimento, della
3060 nell'esempio di sopra che il termine $N$ sia in forma $\beta$-normale.
3071 incluse riscritture sull'eguaglianza, che permettono di includere utili fatti aggiuntivi. Per
3073 la riscrittura per $K$ di sopra, cos� come la definizione della
3078 L'applicazione di questa funzione a un \simpset{} \texttt{ss}
3080 \texttt{ss} esistente, cos� come la capacit� di riscrivere con la relazione
3089 La Sezione~\ref{sec:datatype} e la Sezione~\ref{TFL} mostrano la capacit� di
3090 \HOL{} di rappresentare molti dei costrutti standard della programmazione
3094 di esercitare tutto il potere del processo di riscrittura,
3095 inclusa, per esempio, l'applicazione delle procedure di decisione per
3096 dimostrare vincoli sulle regole di riscrittura condizionale. Secondo, si potrebbe
3099 un interprete. Questa funzionalit� � disponibile in \HOL{} attraverso l'uso di
3111 definizioni di funzione. Nel seguente esempio, caricare \ml{sortingTheory}
3113 di Quicksort (\holtxt{QSORT}), e poi possiamo valutare
3126 l'applicazione di \ml{EVAL} dovrebbe restituire un risultato ground,
3127 come nell'esempio di sopra. Tuttavia, \ml{EVAL} pu� anche valutare funzioni su
3129 in quel caso, il comportamento di \ml{EVAL} dipende dalla struttura
3130 dell'equazioni di ricorsione. Per esempio, nella seguente sessione, se c'�
3149 La difficolt� maggiore con l'uso di \ml{EVAL} � la terminazione. Troppo
3174 La definizione ricorsiva primitiva di \holtxt{FACT} non si espande
3175 per nulla, mentre la ricorsione stile-decostruttore di \holtxt{fact} non smette mai
3176 di espandere. Un rudimentale strumento di monitoraggio mostra il comportamento, prima
3208 In ogni espansione ricorsiva, il testo coinvolge una variabile, e di conseguenza
3219 che prende una lista extra di costanti. Durante
3221 non sar� espansa. Questo permette di valutare gi� fino a un livello specificato.
3225 una discussione di \ml{set\_skip}
3232 personalizzato, specializzato su un insieme fissato di definizioni. Il tipo
3233 \ml{compset} che si trova in \ml{computeLib} � il tipo dei database di definizione. Le
3242 \paragraph{Trattare con Funzioni sui Numeri di Peano}
3244 Le funzioni definite per pattern-matching su numeri nello stile di Peano non sono
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
3259 usata per definire una funzione, le sue equazioni di definizione non sono aggiunte al
3261 di terminazione. Inoltre, \ml{tprove} non aggiunge la definizione
3266 prima di chiamare \ml{export\_theory}.
3271 \index{procedure di decisione!Aritemtica Presburger su numeri naturali}
3273 Ognuna delle librerie aritmetiche di \HOL{} fornisce una
3274 suite di definizioni e teoremi cos� come il supporto per l'inferenza automatica.
3278 I numeri pi� di base in \HOL{} sono i numeri naturali. La
3282 da \ml{reduceLib} e una procedura di decisione per l'aritmetica lineare
3283 \ml{ARITH\_CONV}. Il valutatore e la procedura di decisione sono
3285 Allo stesso modo, la procedura di decisione dell'aritmetica lineare pu� essere invocata
3290 \index{procedure di decisione!Aritemtica Presburger su interi}
3294 teoria degli interi, pi� due procedure di decisione
3297 procedure di decisione sono in grado di trattare con l'aritmetica lineare
3298 sugli interi e i numeri naturali, cos� come di trattare
3299 con un'alternanza arbitraria di quantificatori. La procedura
3301 in generale avere migliori performance rispetto all'algoritmo di Cooper. Ci sono
3311 Una procedura di decisione per l'aritmetica lineare sui numeri reali
3317 La libreria \theoryimp{wordsLib} fornisce uno strumento di supporto per i bit-vectors, questo include infrastrutture per: la valutazione, il parsing, il pretty-printing e la semplificazione.
3322 pu� essere usato nella costruzione di \emph{compese} e conversioni personalizzati.
3333 Si noti che qui � usata un'annotazione di tipo per designare la dimensione word. Quando la dimensione word � rappresentata da una variabile di tipo (cio� per word i lunghezza arbitraria), la valutazione
3348 E' possibile fare il parsing di numeri ottali, ma questo deve essere prima abilitato impostando la reference \ml{base\_tokens.allow\_octal\_input} a true. Per esempio:
3373 La funzione \ml{output\_words\_as} � pi� flessibile e permette alla base numerica di variare a seconda della
3374 lunghezza del word e del valore numerico. Il pretty-printer di default (installato quando si carica \theoryimp{wordsLib}) stampa valori piccoli in decimale e valori grandi in esadecimale.
3377 La variabile di traccia \ml{"word printing"} fornisce un metodo alternativo per cambiare la base numerica di output --- � particolarmente adatta per selezionare temporaneamente una base numerica, per esempio:
3389 Si pu� aver notato che \ty{:word4} e \ty{:word8} sono stati usati come convenienti abbreviazioni di parsing per \ty{:\bool[4]} e \ty{:\bool[8]} --- questa agevolazione � disponibile per molte dimensioni standard di word. Gli utenti che desiderano usare questa notazione per dimensioni di non-standard di word possono usare la funzione \ml{wordsLib.mk\_word\_size}:
3406 I simboli per le operazioni aritmetiche standard (addizione, sottrazione e moltiplicazione) sono sottoposte a overload con operatori per altre teorie standard, cio� per i numeri naturali, interi, razionali e reali. In molti casi l'inferenza di tipo risolver� l'overloading, tuttavia, in alcuni casi questo non � possibile. La scelta dell'operatore dipender� dall'ordine in cui le teorie sono caricate. Per cambiare questo comportamento sono fornite le funzioni \ml{wordsLib.deprecate\_word} e \ml{wordsLib.prefer\_word}. Per esempio, nella seguente sessione, la selezione degli operatori word � deprecata:
3422 Di sopra, l'addizione tra numeri naturali � scelta al posto dell'addizione word. Al contrario, i word sono preferiti rispetto agli interi di sotto:
3439 Naturalmente, potrebbero essere state aggiunte annotazioni di tipo per evitare questo problema completamente. Si noti che, diversamente da \ml{deprecate\_int}, la funzione \ml{deprecate\_word} non rimuove gli overloading, semplicemente abbassa la loro precedenza.
3443 Pu� essere una seccatura aggiungere annotazioni di tipo quando si specifica il tipo di ritorno per operazioni come: \holtxt{word\_extract}, \holtxt{word\_concat}, \holtxt{concat\_word\_list} e \holtxt{word\_replicate}. Questo perch� c'� spesso una lunghezza ``standard'' che potrebbe essere indovinata, ad esempio la concatenazione di solito somma le lunghezze dei word costituenti. Un'agevolazione per indovinare la lunghezza word � controllata dalla reference \ml{wordsLib.guessing\_word\_lengths}, che � falsa di default. Le congetture sono eseguite durante un passo di post-processing che avviene dopo l'applicazione di \ml{Parse.Term}. Questo � mostrato di sotto.
3458 Nell'esempio di sopra, le congetture sulla lunghezza dei word sono attivate. Sono fatte due congetture: ci si aspetta che l'estrazione dia un word di quattro bit, e che la concatenazione dia un word di dodici bit ($3 \times 4$). Se sono richieste lunghezze numeriche non standard allo si possono aggiungere delle annotazioni di tipo per evitare che siano fatte delle congetture. Quando la congettura � disattivata i tipi risultanti rimangono come variabili di tipo inventate, cio� come gli alfa e i beta di sopra.
3464 \item[\ml{SIZES\_ss}] valuta un gruppo di funzioni che operano su tipi numerici, come \holtxt{dimindex} e \holtxt{dimword}.
3469 \item[\ml{WORD\_ss}] contiene tutti i frammenti di sopra, e fa anche una valutazione estra dei termini ground. Questo frammento � aggiunto a \ml{srw\_ss}.
3472 \item[\ml{WORD\_EXTRACT\_ss}] semplificazione per una variet� di operazioni: conversioni da word a word; concatenazione; shift e estrazione bit-field. Pu� essere usata in situationi dove \ml{WORD\_BIT\_EQ\_ss} non � adatta.
3473 \item[\ml{WORD\_MUL\_LSL\_ss}] semplifica la moltiplicazione con un letterale word in una somma di prodotti parziali.
3475 Molti di questi frammenti \emph{simpset} hanno delle conversioni corrispondenti. Per esempio, la conversione \ml{WORD\_ARITH\_CONV} � basata si \ml{WORD\_ARITH\_EQ\_ss}, tuttavia, fa del lavoro extra per assicurare che \holtxt{``a = b``} e \holtxt{``b = a``} si convertano nella stessa espressioni. Di conseguenza, questa conversione � adatta per ragionare circa l'eguaglianza delle espressioni aritmetiche word.
3477 Il comportamento dei frammenti elencati di sopra � mostrato usando la seguente funzione:
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:
3527 I frammenti rimanenti non sono inclusi in \ml{wordsLib.WORD\_ss} or \ml{srw\_ss}. Il frammento eguaglianza bit � mostrato di sotto.
3546 Infine, il frammento \ml{WORD\_MUL\_LSL\_ss} � mostrato di sotto.
3561 Ovviamente, senza aggiungere delle garanzie, questo teorema di riscrittura non pu� essere dispiegato in combinazione con il frammento \ml{WORD\_MUL\_LSL\_ss}.
3563 \subsubsection{Procedure di decisione}
3565 Una procedura di decisione per i word � fornita nella forma di
3568 decidere il goal\footnote{Questo approccio permette di dare contro-esempi
3569 quando la negazione di un goal � insoddisfacibile.}. Questo approccio � ragionevolmente generale e
3570 pu� affrontare un ampia gamma di problemi bit-vector. Tuttavia, ci sono alcune
3590 La procedura di decisione \ml{BBLAST\_PROVE} � basata sulla conversione