30 Nel sistema \HOL{}, le librerie sono tipicamente rappresentate da strutture
33 dovrebbe caricare tutte le sotto-componenti rilevanti della libreria e settare
38 pi� di base � \ml{boolLib}, che supporta le definizioni della logica
44 convenzione circa le denominazioni delle librerie). La libreria parser fornisce supporto
53 \theoryimp{sum}, \theoryimp{option}; le teorie aritmetiche
90 le teorie discendenti. Le funzioni che fanno cambiamenti temporanei sono denotate
123 	estendere le categorie $\odot$ e $\nt{tyop}$ facendo nuove definizioni
163 la sintassi concreta per le formalizzazioni. Di solito, la grammatica \HOL{} viene
175 Il parser trasforma le stringhe in termini. Fa questo nella seguente
184 \item[Sintassi Concreta:] Caratteristiche come gli infissi, i binder e le forme
189 	\ml{add\_rule} e \ml{set\_fixity} (per le quali, si veda \REFERENCE).
206 	variabili: bench� le forme \ml{QIDENT} debbano essere delle costanti, gli utente sono
231 allora questa fase del parser non tratter� le stringhe come parte di una
270 	ha costruttori simili a quelli in \ml{Absyn} eccetto che con le forme
271 	per le costanti. %
309 	come una costante, esso � mappato a una forma pretermine che elenca tutte le
312 	l'inferenza di tipo spesso eliminer� le possibilit� dalla lista. Se
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,
339 	in grado di assegnare un tipo unico a tutte le costanti. Se esistono
366 Unicode nei loro nomi, e lasciare le cose come stanno. Il problema con
426 semplicistica: tutt le lettere greche eccetto \holtxt{$\lambda$} sono alfanumerici;
452 costanti. In questo modo, per esempio, le varie teorie aritmetiche possono
461 forma $\lambda x.\;M$), allora il parser eseguir� tutte le $\beta$-riduzioni
477 e le variabili polimorfiche sono generalizzabili, permettendo all'inferenza
487 se queste variabili hanno tipi polimorfici, allora le variabili di tipo in
509 pi� recentemente. (Gli utenti possono cos� manipolare le preferenze del printer
590 Al posto del \holtxt{\$}, si possono anche usare le parentesi per rimuovere dai lessemi
682 le altre due occorrenze sono l'operazione d'inverso additivo per
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}.
804 semantica denotazionale sono le parentesi semantiche. Cos�, le infrastrutture di parsing
833 	� di rimuovere tutte le regole al livello dato della grammatica, e
838   \holtxt{-}. Cos�, rimuoviamo le loro regole:
842   \noindent E poi le rimettiamo con l'associativit�
847 \noindent Si noti che usiamo le versioni \ml{temp\_} di queste due
915 \subsubsection{Nascondere le costanti}
919 \index{sistema HOL@sistema \HOL{}!nascondere le costanti nel|(}
935 fa s� che il parser delle quotation tratti $x$ come una variabile (purch� le regole
937 (le costanti e le variabili possono avere lo stesso nome).
944 per i costruttori, le teorie, ecc; \ml{hide} influisce solo sul parsing e
974 \index{sistema HOL@sistema \HOL{}!nascondere le costanti nel|)}
1065 caret (\ml{\^}, carattere ASCII~94). Per avere un semplice caret, le cose diventano
1101 L'uso principale del caret � d'introdurre le \emph{quntiquotation} (come
1185 vuole sapere come usare le nuove strutture, ma vuole essere sicuro
1198 	dovrebbe rendere in genere pi� facile annotare le tuple, dal momento che ora
1202   \] dove le parentesi extra si sono dovute aggiungere solo per permettere di
1219 	stringa (le stringhe all'interno dei doppi apici) e quelli numerici non possono essere usati
1220 	a meno che le teorie rilevanti non siano state caricate. Inoltre questi
1228 basata sulle tattiche. Quando si vogliono usare le tattiche per decomporre una dimostrazione, sorgono
1330 usare le funzioni \ml{p} e \ml{status}. La prima mostra solo
1374 impegna a lavorare in un contesto che fornisce gi� le teorie
1375 dei booleani, le coppie, le somme, il tipo option, l'aritmetica, e le liste.
1441 le variabili libere dei $M$ sono quantificate universalmente. \ml{Induct\_on} �
1442 pi� generale di \ml{Induct}, ma richiede che le venga dato un termine
1522 elimina tutte le ipotesi della forma $v = M$ o $M = v$ dove $v$ �
1525 \ml{RW\_TAC} solleva le espressioni-\holtxt{let} all'interno del goal cos� che
1536 sistema, le performance di \ml{RW\_TAC} ne possono risentire perch�
1539 \ml{SRW\_TAC} carica le riscritture nel \simpset{} al di sotto di
1544 simpset per la logica pura, le somme, le coppie e il tipo \ml{option} �
1546 \ml{arith\_ss}, e il simpset per le liste � chiamato \ml{list\_ss}.
1607 il fattore di ramificazione nello spazio di ricerca � alto, le tattiche
1610 Tutte le tattiche \texttt{meson} prendono una lista di teoremi. Questi
1612 \texttt{MESON\_TAC} ignora le assunzioni del goal; gli altri due
1613 entry-point includono le assunzioni come pare del sequente da
1628 normalizzazione, prima di passare un goal e le sue assunzioni a
1650 Entrambe le funzioni prendono una lista di teoremi, e questi sono usati come lemmi
1675 a termini, rimpiazzando le istanze di $l$ nel termine con $r$. Cos�, la
1688 semplificatore. Ci sono dei \simpset{} che accompagnano le teorie principali
1717 le loro proprie riscritture. Se un particolare insieme di teoremi � usato spesso come
1753 semplificare il goal attuale (ignorando le assunzioni) usando il \simpset{}
1762 (lasciando le assunzioni intatte), ma include le assunzioni
1796 un goal ma anche le sue assunzioni. Essa procede semplificando
1797 ciascuna assunzione una alla volta, usando inoltre le assunzioni precedenti nella
1800 tattica \ml{STRIP\_ASSUME\_TAC}. Questo significa che le assunzioni che
1806 \ml{FULL\_SIMP\_TAC} attacca le assunzioni nell'ordine in cui
1807 appaiono nella lista dei termini che rappresentano le assunzioni
1835 \holtxt{x} nel goal � stata sostituita in modo analogo. Se le assunzioni fossero
1879 	ma anche con tutte le regole di riscrittura dalla \ml{TypeBase}, e
1880 	anche con le assunzioni del goal.
1918 goal-splitting che fa \ml{RW\_TAC}. Le principali differenze tra le
1922 dei \simpset{} che includano tutte le riscritture ``appropriate'' del contesto
1956 contiene tutti i teoremi di de~Morgan per spostare le negazioni tra i
1958 condizionali), incluse le regole dei quantificatori che hanno $\neg(\forall
1960 contiene anche le regole che specificano il comportamento dei connettivi
1961 quando le costanti \holtxt{T} e \holtxt{F} appaiono come loro
2074 Opportunamente, \ml{list\_ss} include anche delle riscritture per le funzioni
2123 tutte le situazioni dove il semplificatore � utilizzato.
2177 Come regola generale, \ml{(srw\_ss())} include tutte le ``riscritture ovvie''
2203 Per le teorie principali (o gruppi di esse), una collezione di
2207 \ml{numSimps}, e i frammenti per le liste si trovano in \ml{listSimps}.
2222 \ml{CONG\_ss} & Regole di congruenza per l'implicazione e le espressioni
2288 alcun match ulteriore per le regole di riscrittura del semplificatore. La
2292   Mentre c'� un qualsiasi match per le regole di riscrittura archiviate a questo livello,
2293 	si continui ad applicarle. \emph{Non} si pu� fare affidamento sull'ordine in cui le regole
2333 ricorsive, il semplificatore tiene traccia di uno stack di tutte le
2355 Bench� le regole riscrittura condizionali siano potenti, non ogni teorema della
2385 le riscritture di questa stessa forma. L'esatta trasformazione eseguita �
2403 le congiunzioni, le implicazioni e le quantificazioni universali fino a quando o ha
2471 combinato $f(a)$ matcher� qualsiasi termine del tipo appropriato fino a quando le
2514 regola pu� essere vista come un'implementazione di un metodo per muovere le astrazioni
2537 sono poco di pi� che le regole d'inferenza \ml{ABS}
2578 La forma per \ml{ABS} dimostra come � possibile per le regole
2579 di congruenza gestire variabili legate. Dal momento che le regole di congruenza sono
2585 la regola di congruenza (che si trova in \ml{CONG\_ss}) per le implicazioni. Questa
2622 altra regola per le espressioni condizionali (mascherando quella sopra
2624 nella guardia. Con le riscritture standard (da \ml{BOOL\_ss}):
2679 le sue procedure di normalizzazione su misura per l'addizione sui
2751 futura versione di \HOL{} ma per come stanno le cose ora, la chiamata ricorsiva pu�
2792 ampio. Infatti, solo le funzioni che accedono e creano contesti di questa
2807 dagli argomenti lista di teoremi a tutt le varie funzioni di
2808 semplificazione. Mentre un termine � attraversato, le regole di congruenza che governano
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
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
2844 richieste, l'utente pu� usare piuttosto le funzioni \ml{AC} o \ml{Cong}:
2884 solo le guardie delle espressioni condizionali dovrebbero essere semplificate.
2909 (Con le relazioni, il goal pu� spesso rappresentare un'implicazione al posto di
2970 con le procedure di decisione aritmetica), ma l'uso di \ml{limit} �
2987 	(diciamo, \texttt{lamterm}) all'interno della logica, cos� come le definizioni delle
2988 	funzioni appropriate (ad esempio, la sostituzione) e le relazioni su
3031 (sotto le assunzioni che i termini $u$ e $v$ siano variabili del
3112 aumenta questo database con le definizioni rilevanti, in particolare quella
3151 termini enormi. Il caso usuale sono i condizionali con le variabili nel
3161 Ma le due definizioni sono valutate in modo completamente differente.
3248 Sezione~\ref{sec:numerals}. Tuttavia, � preferibile per le dimostrazioni
3255 \paragraph{Archiviare le definizioni}
3259 usata per definire una funzione, le sue equazioni di definizione non sono aggiunte al
3263 \ml{add\_persistent\_funs} in una teoria per essere sicuri che le definizioni
3279 libreria \ml{numLib} comprende le teorie \ml{numTheory},
3303 entrambe le procedure.
3362 I word possono essere stampati usando le basi numeriche standard. Per esempio, la funzione
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:
3441 \subsubsection{Indovinare le lunghezze word}
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.
3465 \item[\ml{BIT\_ss}] prova a semplificare le occorrenze della funzione\holtxt{BIT}.
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:
3574 potenzialmente lenti da dimostrare, ad esempio quando le dimensioni dei word sono grandi e/o quando

Indexes created Tue Sep 03 12:52:19 MDT 2024