7 % \ml{..}         for typewriter text that is ML input, including the
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
32 si trover� nella struttura \ML{} \ml{xLib}. Caricare questa struttura
38 pi� di base � \ml{boolLib}, che supporta le definizioni della logica
42 Un'altra libreria usata in modo pervasivo si trova nella struttura \ml{Parse}
48 La libreria \ml{boss} fornisce una collezione base di teorie
51 \HOL{} si avvia. Essa include \ml{boolLib} e
52 \ml{Parse}. Le teorie fornite includono \theoryimp{pair},
56 incluse in \ml{bossLib} sono \ml{goalstackLib}, che fornisce
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},
71 e dei termini attraverso la struttura \ml{Parse}.
91 da un prefisso \ml{temp\_} nei loro nomi.
99 di tipo) pu� essere ispezionata usando la funzione \ml{type\_grammar}.
129 Gli infissi possono essere introdotti con la funzione \ml{add\_infix\_type}.
139 Questo � fatto con la funzione \ML{} \ml{type\_abbrev}:
157 Per maggiori informazioni, si veda la voce \ml{type\_abbrev} in \REFERENCE.
186 	astratta'' intermedia (tipo ML \ml{Absyn}). Le fixity possibili sono
189 	\ml{add\_rule} e \ml{set\_fixity} (per le quali, si veda \REFERENCE).
191 	\ml{Absyn}.
193  Il data type \ml{Absyn} � costruito usando i costruttori \ml{AQ}
198   \ml{IDENT} (un identificatore); \ml{QIDENT} (un identificatore qualificato,
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
202 		tipi nei vincoli \ml{Absyn} non sono tipi HOL completi, ma valori
203 		da un'altro tipo intermedio \ml{Pretype}.}, si veda
206 	variabili: bench� le forme \ml{QIDENT} debbano essere delle costanti, gli utente sono
209   E' possibile che i nomi che occorrono nel valore \ml{Absyn} siano
219 	\ml{Absyn}, incluso \ml{APP}, prendono anche parametri di localizzazione.)
228 \index{ escape, nel parser della logica HOL@\ml{\$} (escape, nel parser della logica \HOL{})}%
233 nella forma \ml{Absyn}
261   La funzione dell'utente sar� di tipo \ml{Absyn~->~Absyn} e potr�
267 \item[Risoluzione dei Nomi:] Le forme nude \ml{IDENT} nel valore \ml{Absyn}
269 	Questo processo risulta in un valore del tipo di dati \ml{Preterm}, che
270 	ha costruttori simili a quelli in \ml{Absyn} eccetto che con le forme
273 	Una stringa pu� essere convertita direttamente in un \ml{Preterm} per mezzo della
274 	funzione \ml{Preterm}.
276   Un nome legato � il primo argomento a un costruttore \ml{LAM}, un
328 	questo attraverso le API per il tipo di dato \ml{term}. (In particolare,
329 	la funzione \ml{mk\_comb} %
330 	\index{mk_comb@\ml{mk\_comb}}%
340 	pi� possibilit�, ne sar� scelto uno quando il \ml{Preterm} � infine
343   Quando � stato completato il controllo di tipo di un \ml{Preterm}, la conversione finale da
344 	quel tipo al tipo del \ml{term} � per lo pi� semplice. L'utente
368 di teoria che includono binding \ML{} (illegali) come \ml{val $\rightarrow$\_def =
369   \dots}. Il risultato saranno file \ml{...Theory.sig} e
370 \ml{...Theory.sml} che falliranno di compilare, anche se la chiamata a
371 \ml{export\_theory} pu� avere successo. Questo problema pu� essere manovrato attraverso
372 l'uso di funzioni come \ml{set\_MLname}, probabilmente � una pratica
374 usare poi funzioni come \ml{overload\_on} e \ml{add\_rule} per creare
383 funzione \ml{Unicode.unicode\_version}. Quindi, quando la variabile
384 di traccia \ml{"Unicode"}  � $0$, la sintassi ASCII sar� usata per
389 Per esempio, in \ml{boolScript.sml}, il carattere Unicode per l'and
395 (In questo contesto, � stata aperta la struttura \ml{Unicode},
396 dando accesso anche alla struttura \ml{UChar} che contiene i binding
399 L'argomento a \ml{unicode\_version} � un record con campi \ml{u}
400 e \ml{tmnm}. Entrambe sono stringhe. Il campo \ml{tmnm} pu� essere o
402 (che possibilmente mappa a qualche altro nome). Se il \ml{tmnm} � solo il
404 \ml{u} sar� sottoposta a overloading con lo stesso nome. Se il \ml{tmnm} � lo
406 creare una nuova regola che mappa allo stesso nome, ma con la stringa \ml{u}
441 \ml{Preterm} saranno tradotti in termini. In sostanza, i nomi legati sono tradotti
453 mappare la stringa \ml{"+"} alla nozione rilevante di addizione, ognuna delle
457 stringa \ml{"<=>"} mappa l'eguaglianza, ma dove gli argomenti sono forzati
464 \ml{"<>"} � sottoposta a overload rispetto al termine \holquote{\bs{}x~y.~\td{}(x~=~y)}.
465 Inoltre, \ml{"<>"} � impostato come un infisso al livello della sintassi
467 \ml{Absyn} risultante �
471 The \ml{"x"}  and \ml{"y"} identifiers will map to free variables, but
472 the \ml{"<>"} identifier maps to a list containing
478 di tipo di dare i tipi (identici) appropriati a \ml{x} e \ml{y}.
479 Assumendo che questa opzione sia l'unico oveloading per il \ml{"<>"} lasciato
493 non costruisca un valore \ml{Absyn}, questo processo inverte la fase del parsing
510 eseguendo delle chiamate altrimenti ridondanti alla funzione \ml{overload\_on}.)
515 la \ml{x} e la \ml{y} in questo esempio erano legate da un'astrazione),
543 cos� che il pattern di \ml{isPREFIX} � lungo quanto quella di \ml{IS\_PREFIX}.
620 variabili globale \ml{show\_types}. Quando � impostato questo flag,
624 \ml{guessing\_tyvars} a \ml{false}, nel qual caso
637 l'invero additivo nelle teorie \ml{integer} e
638 \ml{real}. Se carichiamo la teoria \ml{integer}
836 	\ml{term\_grammar()}). Con la sola \ml{arithmeticTheory}
847 \noindent Si noti che usiamo le versioni \ml{temp\_} di queste due
865 	fixity appropriata � \ml{Prefix}. Sapendo che il termine costante
888 come ci dovesse essere un altro \ml{Prefix}, ma la scelta delle
892 \ml{CloseFix}, la nuova sintassi deve essere della stessa classe. Questo � abbastanza semplice
927 \index{hide@\ml{hide}|pin}
934 \noindent La valutazione di \ml{hide "$x$"}
943 (ad esempio \ml{o}, \ml{I}, \ml{S} \etc). Il nome $x$ � ancora una costante
944 per i costruttori, le teorie, ecc; \ml{hide} influisce solo sul parsing e
947 di \ml{hide} � \emph{temporaneo}; i suoi effetti non persistono nelle
948 teorie discendenti da quella attuale. Si veda la voce \ml{hide} in
955 \index{reveal@\ml{reveal}|pin}
966 \index{hidden@\ml{hidden}|pin}
984 \index{max_print_depth@\ml{max\_print\_depth}|pin}
1019 � delimitata da singoli accenti grave (cio�, \ml{`}, carattere ASCII~96). Quando
1030 Quotations (Moscow ML prints the type as \ml{'a frag list}) are the
1033 \ml{Parse.Term} function takes a (term) quotation and returns a term,
1034 and is thus of type \[ \ml{term quotation -> term}
1051 L'espressione legata alla variabile ML \ml{t} di sopra di fatto � espansa
1052 a un'applicazione della funzione \ml{Parse.Term} alla quotation
1053 argomento \ml{`p /\bs{} q`}. Analogamente, la seconda espressione si espande
1054 in un'applicazione di \ml{Parse.Type} alla quotation \ml{`:'a -> bool`}.
1065 caret (\ml{\^}, carattere ASCII~94). Per avere un semplice caret, le cose diventano
1111 \ml{term} o \ml{type}) sono chiamate antiquotation.
1157 \index{ty_antiq@\ml{ty\_antiq}}
1235 I tipi astratti \ml{goalstack} e \ml{proofs} sono il
1236 punto focale delle operazioni di dimostrazione all'indietro. il tipo \ml{proofs} pu� essere
1250 Si ricordi che il tipo \ml{goal} � un'abbreviazione per
1251 \ml{term list * term}. Per partire su un nuovo goal, si da a
1252 \ml{set\_goal} un goal. Questa crea un nuovo goalstack e lo rende il
1255 Un'abbreviazione per \ml{set\_goal} � la funzione \ml{g}: essa
1259 La chiamata a \ml{set\_goal}, o \ml{g}, aggiunge un nuovo tentativo di dimostrazione a
1296 nel goalstack, sono usate la funzione \ml{backup} e la sua abbreviazione
1297 \ml{b}. Questo ripristiner� il goalstack al suo stato
1302 la funzione \ml{restart}. Ovviamente, � anche importante liberarsi
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
1311 usare la funzione \ml{set\_backup}. Se la dimensione della lista di
1314 \ml{set\_goal} o \ml{drop}.
1330 usare le funzioni \ml{p} e \ml{status}. La prima mostra solo
1334 To get the top goal or goals of a proof attempt, use \ml{top\_goal}
1335 and \ml{top\_goals}. To get the original goal of a proof attempt,
1336 use \ml{initial\_goal}.
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,
1340 si usi \ml{initial\_goal}.
1345 \ml{top\_thm}.
1360 \ml{rotate} e \ml{rotate\_proofs}, rispettivamente. Le abbreviazioni
1361 \ml{r} e \ml{R} sono pi� semplici da digitare.
1364 % would use \ml{boss} above but it puts LaTeX into fits
1366 \newcommand\bossLib{\ml{bossLib}}
1368 \index{bossLib@\ml{bossLib}}
1384 \index{Induct_on (tattica ML d'induzione)@\ml{Induct\_on} (tattica \ML{} d'induzione)}
1385 \index{Cases_on (tattica ML di case-split)@\ml{Cases\_on} (tattica \ML{} di case-split)}
1394 \index{type_rws@\ml{type\_rws}}
1395 \index{TypeBase@\ml{TypeBase}}
1397 La funzione \ml{type\_rws} cercher� per il tipo dato nel
1398 database sottostante \ml{TypeBase} e restituir� utili regole di riscrittura per
1401 case. Le tattiche di semplificazione \ml{RW\_TAC}, \ml{SRW\_TAC},
1402 e il \simpset{} \ml{(srw\_ss())} includono automaticamente questi
1408 La tattica \ml{Induct} rende conveniente invocare l'induzione. Quando
1413 The \ml{Cases} tactic makes it convenient to invoke case
1418 La tattica \ml{Cases\_on} prende una quotation, che �
1427 che la tattica \ml{Cases\_on} � pi� generale di \ml{Cases}, ma
1430 \index{Induct_on (tattica ML d'induzione)@\ml{Induct\_on} (tattica \ML{} d'induzione)}
1431 La tattica \ml{Induct\_on} prende una quotation, che � parsata in un
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
1448 \item [\ml{completeInduct\_on}] esegue un'induzione completa sul
1460 \item [\ml{measureInduct\_on}] prende una quotation, e la suddivide
1463 	\holtxt{L}, l'invocazione \ml{measureInduct\_on~`LENGTH L`}
1466 \item [\ml{recInduct}] prende un teorema d'induzione generato da
1467 	\ml{Define} o \ml{Hol\_defn} e lo applica al goal attuale.
1475 \ml{bossLib} riunisce i pi� potenti ragionatori in \HOL{} e
1477 base da \ml{mesonLib}, \ml{simpLib}, e \ml{numLib},
1478 ma il punto di \ml{bossLib} � di fornire un livello di astrazione cos�
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
1518 \index{RW_TAC@\ml{RW\_TAC}} La tattica di riscrittura \ml{RW\_TAC} lavora
1525 \ml{RW\_TAC} solleva le espressioni-\holtxt{let} all'interno del goal cos� che
1530 \index{SRW_TAC@\ml{SRW\_TAC}} La tattica \ml{SRW\_TAC} � analoga a
1531 \ml{RW\_TAC}, ma lavora rispetto a un \simpset{} sottostante
1532 (accessibile attraverso la funzione \ml{srw\_ss}) che viene aggiornato ogni volta che viene caricato
1534 l'aggiornamento di ``frammenti \simpset{} '' (valori \ml{ssfrag}) e
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
1540 \ml{srw\_ss()} una volta sola, rendendo l'operazione pi� veloce in questa
1543 \ml{bossLib} fornisce un numero d'insiemi di semplificazione. Il
1544 simpset per la logica pura, le somme, le coppie e il tipo \ml{option} �
1545 chiamato \ml{std\_ss}. Il simpset per l'aritmetica � chiamato
1546 \ml{arith\_ss}, e il simpset per le liste � chiamato \ml{list\_ss}.
1548 \ml{std\_ss} � contenuto in \ml{arith\_ss}, e \ml{arith\_ss} �
1549 contenuto in \ml{list\_ss}. Il combinatore infisso \ml{\&\&} � usato
1560 La funzione \ml{by} � un operatore infisso che prende una quotation
1562 l'invocazione ``\ml{$M$ by $\mathit{tac}$}'' � applicata a un goal
1568 \ml{by} permette di mischiare un utile stile di ragionamento `asserzionale' o `Mizar-like'
1573 L'entry-point \ml{SPOSE\_NOT\_THEN} inizia una dimostrazione per
1591 \index{meson (model elimination) procedura@\ml{meson} (model elimination) procedura}
1594 La libreria \ml{meson} � un'implementazione del
1616 I parametri extra a \ml{GEN\_MESON\_TAC} forniscono un controllo extra del
1620 comportamento di default per \ml{MESON\_TAC} e \ml{ASM\_MESON\_TAC} � di iniziare $d$
1623 \ml{mesonLib.max\_depth}. Per contro,
1624 \ml{GEN\_MESON\_TAC~min~max~step} inizia $d$ a \ml{min}, lo incrementa
1625 di \ml{step}, e rinuncia quando $d$ eccede \ml{max}.
1627 La funzione \ml{PROVE\_TAC} da \ml{bossLib} esegue qualche
1629 \ml{ASM\_MESON\_TAC}. A causa di questa normalizzazione, nella maggior parte
1630 delle circostanze, si dovrebbe preferire \ml{PROVE\_TAC}
1631 a \ml{ASM\_MESON\_TAC}.
1636 \index{procedura metis (risoluzione)@procedura \ml{metis} (risoluzione)}
1639 La libreria \ml{metis} � un'implementazione del metodo di risoluzione
1678 \ml{UNCHANGED}.
1689 di \HOL{}. Per esempio, il \simpset{} \ml{bool\_ss}
1690 in \ml{boolSimps} incorpora tutti i teoremi di riscrittura usuali desiderabili su formule
1699 Oltre alla riscrittura con i teoremi ovvi, \ml{bool\_ss} �
1714 Il secondo argomento a \ml{SIMP\_CONV} � una lista di teoremi da
1721 Per esempio, la riscrittura \ml{arithmeticTheory.LEFT\_ADD\_DISTRIB}, che
1733 Si noti come il \simpset{} \ml{arith\_ss} non ha solamente semplificato il
1734 termine intermedio \ml{(p * 1)}, ma ha anche riordinato l'addizione per
1743 Il semplificatore � implementato intorno alla conversione \ml{SIMP\_CONV},
1747 disponibile in \ml{bossLib}.
1749 \subsubsection{\ml{SIMP\_TAC : simpset -> thm list -> tactic}}
1750 \index{SIMP_TAC@\ml{SIMP\_TAC}}
1752 \ml{SIMP\_TAC} � la tattica di semplificazione pi� semplice: essa tenta di
1755 sollevamento della sottostante conversione \ml{SIMP\_CONV} al livello
1756 di tattica attraverso l'uso della funzione standard \ml{CONV\_TAC}.
1758 \subsubsection{\ml{ASM\_SIMP\_TAC : simpset -> thm list -> tactic}}
1759 \index{ASM_SIMP_TAC@\ml{ASM\_SIMP\_TAC}}
1761 Come \ml{SIMP\_TAC}, \ml{ASM\_SIMP\_TAC} semplifica il goal attuale
1784 In questo esempio, \ml{ASM\_SIMP\_TAC} ha usato \holtxt{x = 3} come una
1786 con \holtxt{3}. Quando un'assunzione � usata da \ml{ASM\_SIMP\_TAC} essa
1791 \subsubsection{\ml{FULL\_SIMP\_TAC : simpset -> thm list -> tactic}}
1792 \index{FULL_SIMP_TAC@\ml{FULL\_SIMP\_TAC}}
1795 La tattica \ml{FULL\_SIMP\_TAC} semplifica non solo la conclusione di
1800 tattica \ml{STRIP\_ASSUME\_TAC}. Questo significa che le assunzioni che
1806 \ml{FULL\_SIMP\_TAC} attacca le assunzioni nell'ordine in cui
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}:
1870 \subsubsection{\ml{RW\_TAC : simpset -> thm list -> tactic}}
1871 \index{RW_TAC@\ml{RW\_TAC}}
1874 descritte, \ml{RW\_TAC} � una tattica ``aumentata''. Essa � aumentata in
1879 	ma anche con tutte le regole di riscrittura dalla \ml{TypeBase}, e
1882   \index{TypeBase@\ml{TypeBase}}
1883 \item \ml{RW\_TAC} also does more than just perform simplification.
1890   sub-goals.  \ml{RW\_TAC}'s augmented behaviours are intertwined with
1894 \subsubsection{\ml{SRW\_TAC : ssfrag list -> thm list -> tactic}}
1895 \index{SRW_TAC@\ml{SRW\_TAC}}
1897 La tattica \ml{SRW\_TAC} ha un tipo differente dalle altre
1900 \ml{srw\_ss()} (ulteriormente descritto nella Sezione~\ref{sec:srw_ss}). I
1901 teoremi forniti come il secondo argomento di \ml{SRW\_TAC} sono trattati nello
1917 La tattica \ml{SRW\_TAC} esegue la stessa combinazione di semplificazione e
1918 goal-splitting che fa \ml{RW\_TAC}. Le principali differenze tra le
1920 si lavora con una grande \ml{TypeBase}, e nel fatto che lavorare con
1921 \ml{SRW\_TAC} risparmia dal dover costruire esplicitamente
1924 \ml{(srw\_ss())} non include mai riscritture inappropriate. La presenza
1932 accessibile dall'interno di \ml{bossLib}, bench� alcuni si originano in altre
1935 \subsubsection{\ml{pure\_ss} and \ml{bool\_ss}}
1938 \index{pure_ss@\ml{pure\_ss}}
1940 Il \simpset{} \ml{pure\_ss} (definito nella struttura \ml{pureSimps})
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
1951 \index{bool_ss (insieme di semplificazione)@\ml{bool\_ss} (insieme di semplificazione)}
1953 Il \simpset{} \ml{bool\_ss} (definito nella struttura \ml{boolSimps}) �
1964 Come nell'esempio di sopra, \ml{bool\_ss} esegue anche
1976 Infine, \ml{bool\_ss} include anche regole di congruenza che permettono
1993 \subsubsection{\ml{std\_ss}}
1995 \index{std_ss (insieme di semplificazione)@\ml{std\_ss} (insieme di semplificazione)}
1997 Il \simpset{} \ml{std\_ss} � definito in \ml{bossLib}, e aggiunge
1999 numeri naturali a \ml{bool\_ss}.
2011 Con i numeri naturali, il \simpset{} \ml{std\_ss} pu� calcolare
2024 \subsubsection{\ml{arith\_ss}}
2026 \index{arith_ss (insieme di semplificazione)@\ml{arith\_ss} (insieme di semplificazione)}
2028 Il \simpset{} \ml{arith\_ss} (definito in \ml{bossLib}) estende
2029 \ml{std\_ss} aggiungendo la capacit� di decidere formule dell'aritmetica
2035 Questi due aspetti del \simpset{} \ml{arith\_ss} sono dimostrati
2060 \subsubsection{\ml{list\_ss}}
2062 \index{list_ss (insieme di semplificazione)@\ml{list\_ss} (insieme di semplificazione)}
2064 L'ultimo valore \simpset{} puro in \ml{bossLib}, \ml{list\_ss} aggiunge
2065 teoremi di riscrittura circa il tipo delle liste a \ml{arith\_ss}. Queste
2074 Opportunamente, \ml{list\_ss} include anche delle riscritture per le funzioni
2092 questa funzionalit� � fornita anche da \ml{computeLib} (si veda
2093 la Sezione~\ref{sec:computeLib} di sotto); \ml{computeLib} � pi�
2104 \subsubsection{Il \simpset{} ``stateful''---\ml{srw\_ss()}}
2106 \index{srw_ss (insieme di semplificazione)@\ml{srw\_ss} (insieme di semplificazione)}
2108 L'ultimo \simpset{} esportato da \ml{bossLib} � nascosto dietro una
2109 funzione. Il valore \ml{srw\_ss} ha il tipo \ml{unit -> simpset}, cos�
2110 che si deve digitare \ml{srw\_ss()}  per ottenere un valore \simpset{}.
2115 \ml{SIMP\_CONV~bool\_ss} � la stessa routine di semplificazione ovunque
2118 Per contro, \ml{srw\_ss} � progettata per essere aggiornata. Quando una teoria �
2119 caricata, quando un nuovo tipo � definito. il valore dietro \ml{srw\_ss()}
2120 cambia, e il comportamento di \ml{SIMP\_CONV} applicato a
2121 \ml{(srw\_ss())} cambia con esso. La filosofia di sviluppo dietro
2122 \ml{srw\_ss} � che essa dovrebbe essere sempre una ragionevole prima scelta in
2149 \index{export_rewrites@\ml{export\_rewrites}}
2154 Le stringhe passate a \ml{export\_rewrites} sono i nomi di teoremi
2156 \ml{export\_theory} � chiamata). Non solo questi teoremi sono aggiunti
2177 Come regola generale, \ml{(srw\_ss())} include tutte le ``riscritture ovvie''
2197 dove \ml{++} � un infisso. In generale, � meglio costruire sopra
2198 il \simpset{} \ml{pure\_ss} o uno dei sui discendenti al fine di
2204 frammenti \simpset{} rilevanti si trova di solito nel modulo \ml{<thy>Simps},
2205 dove \ml{<thy>} � il nome della teoria. Per esempio, i frammenti
2207 \ml{numSimps}, e i frammenti per le liste si trovano in \ml{listSimps}.
2217 \ml{BOOL\_ss} &
2220 $\beta$-riduzioni.  (In \ml{boolSimps}.)
2222 \ml{CONG\_ss} & Regole di congruenza per l'implicazione e le espressioni
2223 condizionali. (In \ml{boolSimps}.)
2225 \ml{ARITH\_ss} &
2227 per l'aritmetica universale Presburger. (In \ml{numSimps}.)
2229 \ml{PRED\_SET\_AC\_ss} & Normalizzazione-AC per unioni e intersezioni
2230 su insiemi. (In \ml{pred\_setSimps}.)
2238 \ml{SSFRAG}:
2253 \ml{SSFRAG}, e il loro significato � dato in \REFERENCE. La
2254 funzione \ml{rewrites} fornisce una strada semplice per costruire un
2336 C'� anche una variabile accessibile dall'utente, \ml{Cond\_rewr.stack\_limit}
2344 aritmetica. Per esempio, il teorema \ml{MOD\_MOD} dalla teoria
2345 \ml{arithmetic} afferma
2350 Il semplificatore (in modo specifico, \ml{SIMP\_CONV~arith\_ss~[MOD\_MOD]})
2365 al primo ordine come \ml{PROVE\_TAC})
2373 \ML{} (\ml{SIMP\_CONV}, \ml{ASM\_SIMP\_TAC} ecc) che prendono liste di
2389 \ml{pure\_ss} (si veda la Sezione~\ref{sec:purebool-ss}). Tuttavia, quando un
2392 � di tipo \ml{controlled\_thm~->~controlled\_thm~list}, ed � applicata
2400 appare nel modulo \ML{} \ml{BoundedRewrites}.)
2402 Il filtro che produce riscritture in \ml{pure\_ss} elimina
2405 il teorema \ml{ADD\_MODULUS} afferma
2535 simpset \ml{pure\_ss}. Esse specificano come traversare termini applicazione e
2537 sono poco di pi� che le regole d'inferenza \ml{ABS}
2542 (dove $x\not\in\Gamma$) e \ml{MK\_COMB}
2548 lette verso l'alto. Con \ml{ABS}, per esempio, la regola dice ``quando
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
2578 La forma per \ml{ABS} dimostra come � possibile per le regole
2585 la regola di congruenza (che si trova in \ml{CONG\_ss}) per le implicazioni. Questa
2623 \ml{CONG\_ss}, diciamo) e far� s� che il semplificatore di scendere solo
2624 nella guardia. Con le riscritture standard (da \ml{BOOL\_ss}):
2643 theorems provided in a constituent \simpset{} fragment's \ml{ac}
2664 above is bound to the \ML{} identifier \ml{DISJ\_ss}, its behaviour is
2674 \index{arith_ss (insieme di semplificazione)@\ml{arith\_ss} (insieme di semplificazione)}
2678 \ml{arith\_ss}, e il frammento \ml{ARITH\_ss} che ne � la base, ha
2681 \ml{arith\_ss} pu� far s� che il semplificatore entri in un loop infinito.
2685 \ml{AC}:
2718 I campo \ml{name} e \ml{trace} sono usati quando il tracing del semplificatore
2720 semplificatore � maggiore di o uguale al campo \ml{trace}, allora sar�
2722 (che include il suo \ml{name}).
2724 Il campo \ml{key} del record di sopra � usato per specificare i
2726 \ml{NONE}, allora la conversione sar� provata ad ogni posizione.
2740 normali conversioni \HOL{} (di tipo \ml{term->thm}), e questo pu� essere
2741 fatto ignorando i primi due parametri del campo \ml{conv} Per una
2742 conversione \ml{myconv}, l'idioma standard � di scrivere
2743 \ml{K~(K~myconv)}. Se l'utente lo desidera, tuttavia, il suo codice
2748 L'argomento \ml{term} deve essere di tipo \holtxt{:bool}, e la chiamata
2749 ricorsiva lo semplificher� a vero (e richiamer� \ml{EQT\_ELIM} per trasformare un termine
2758 semplificatore. Piuttosto che restituire un tale risultato, si sollevi un \ml{HOL\_ERR} o
2759 un'eccezione \ml{Conv.UNCHANGED}. (Entrambe sono trattate allo stesso modo dal semplificatore.)
2763 semplificatore � \emph{attraverso} il campo \ml{dprocs} della struttura
2768 Il campo \ml{dprocs} richiede liste di valori di tipo
2769 \ml{Traverse.reducer}. Questi valori sono costruiti con il
2770 costruttore \ml{REDUCER}:
2781 Il tipo \ml{context} � un alias per il tipo \ML{} incorporato
2782 \ml{exn}, quello delle eccezioni. Le eccezioni sono qui usate come un
2801 Quando crea un valore di tipo \ml{reducer}, l'utente deve fornire un
2802 contesto iniziale, e due funzioni. La prima, \ml{addcontext}, �
2806 assunzioni attuali in \ml{ASM\_SIMP\_TAC}, e con i teoremi
2810 anche alla funzione \ml{addcontext}. (Naturalmente, � del tutto a carico
2811 della funzione \ml{addcontext} come questi teoremi saranno
2815 \ml{apply} fornita. Oltre che al termine da trasformare, la
2816 funzione \ml{apply} � passata anche a un record che contiene un
2844 richieste, l'utente pu� usare piuttosto le funzioni \ml{AC} o \ml{Cong}:
2859 funzione \ml{Cong} fornisce un'interfaccia analoga per l'aggiunta di
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}
2873 Un teorema ``avvolto'' nella funzione \ml{Once} sar� applicato
2875 avvolto in \ml{Ntimes} sar� applicato tante volte quante sono date nel
2901 qualcosa a cui si vorrebbe attaccare il qualificatore \ml{Once}.
2912 da sola. Usare \ml{Once} espander� solo una di esse, ma senza
2917 \ml{Once}. Le funzioni
2926 \ml{SimpL~\holquote{(opn)}} restituisce \ml{Cong} applicato al teorema
2932 \index{SimpLHS@\ml{SimpLHS}|pin}\index{SimpRHS@\ml{SimpRHS}|pin}
2934 \ml{SimpLHS} e \ml{SimpRHS} sono forniti per forzare
2936 Queste sono definite essere solo applicazioni di \ml{SimpL} e \ml{SimpR}
2949 Oltre alle forme-di-teoremi \ml{Once} and \ml{Ntimes} appena
2952 riscritture che esso esegue. La funzione \ml{limit} (in \ml{simpLib} e
2953 \ml{bossLib})
2970 con le procedure di decisione aritmetica), ma l'uso di \ml{limit} �
3043 \index{add_relsimp@\ml{add\_relsimp}}
3100 \ml{EmitML.exportML}.
3102 Terzo, si pu� usare \ml{computeLib}. Questa libreria supporta una valutazione
3108 Gli entry-point pi� accessibili per usare la libreria \ml{computeLib}
3109 sono la conversione \ml{EVAL} e la sua tattica corrispondente
3110 \ml{EVAL\_TAC}. Queste dipendono su un database interno che archivia
3111 definizioni di funzione. Nel seguente esempio, caricare \ml{sortingTheory}
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
3149 La difficolt� maggiore con l'uso di \ml{EVAL} � la terminazione. Troppo
3150 spesso, la valutazione simbolica con \ml{EVAL} diverger�, o generer�
3218 \item \ml{RESTR\_EVAL\_CONV} si comporta come \ml{EVAL} eccetto
3223 \item anche \ml{set\_skip} pu� essere usata per controllare
3224 	la valutazione. Si veda la voce per \ml{CBV\_CONV} in \REFERENCE{} per
3225 	una discussione di \ml{set\_skip}
3233 \ml{compset} che si trova in \ml{computeLib} � il tipo dei database di definizione. Le
3234 funzioni \ml{new\_compset}, \ml{bool\_compset}, \ml{add\_funs}, e
3235 \ml{add\_convs} forniscono il modo standard per costruire tali
3237 \ml{reduceLib.num\_compset}, che pu� essere usato per valutare
3238 termini con numeri e booleani. Dato un \ml{compset}, la funzione
3239 \ml{CBV\_CONV} genera un valutatore: � usata per implementare \ml{EVAL}.
3245 nel formato giusto per \ml{EVAL}, dal momento che i calcoli saranno
3250 \ml{numLib.SUC\_TO\_NUMERAL\_DEFN\_CONV} � usata per convertire una funzione
3252 \ml{Eval} preferisce. \ml{Define} chiamer� automaticamente
3253 \ml{SUC\_TO\_NUMERAL\_DEFN\_CONV} sul suo risultato.
3257 \ml{Define} aggiunge automaticamente la sua definizione al compset globale
3258 usato da \ml{EVAL} e \ml{EVAL\_TAC}. Tuttavia, quando \ml{Hol\_defn} �
3260 compset globale fino a quando \ml{tprove} � usata per dimostrare i vincoli
3261 di terminazione. Inoltre, \ml{tprove} non aggiunge la definizione
3263 \ml{add\_persistent\_funs} in una teoria per essere sicuri che le definizioni
3264 fatte da \ml{Hol\_defn} siano disponibili a \ml{Eval} nelle teorie
3265 discendenti. Un altro punto: si deve chiamare \ml{add\_persistent\_funs}
3266 prima di chiamare \ml{export\_theory}.
3279 libreria \ml{numLib} comprende le teorie \ml{numTheory},
3280 \ml{prim\_recTheory}, \ml{arithmeticTheory}, e \ml{numeralTheory}.
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
3284 integrati nel simpset \ml{arith\_ss} usato dal semplificatore.
3286 direttamente attraverso \ml{DECIDE} e \ml{DECIDE\_TAC}, che si trovano entrambe in
3287 \ml{bossLib}.
3293 La libreria \ml{intLib} comprende \ml{integerTheory}, un'estesa
3296 \ml{intLib.COOPER\_CONV} e \ml{intLib.ARITH\_CONV}. Queste
3300 \ml{ARITH\_CONV} � un'implementazione dell'Omega Test, e sembra
3307 La libreria \ml{realLib} fornisce uno sviluppo fondazionale
3312 � anche fornita da \ml{realLib}, sotto il nome \ml{REAL\_ARITH\_CONV}
3313 e \ml{REAL\_ARITH\_TAC}.
3321 La libreria \theoryimp{wordsLib} dovrebbe essere caricata quando si valutano termini bit-vector ground. Questa libreria fornisce un \emph{compset} \ml{words\_compset}, che
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:
3363 \ml{wordsLib.output\_words\_as\_bin} selezioner� il formato binario:
3373 La funzione \ml{output\_words\_as} � pi� flessibile e permette alla base numerica di variare a seconda della
3375 La funzione \ml{output\_words\_as\_oct} abiliter� automaticamente il parsing per i numeri ottali.
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:
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.
3464 \item[\ml{SIZES\_ss}] valuta un gruppo di funzioni che operano su tipi numerici, come \holtxt{dimindex} e \holtxt{dimword}.
3465 \item[\ml{BIT\_ss}] prova a semplificare le occorrenze della funzione\holtxt{BIT}.
3466 \item[\ml{WORD\_LOGIC\_ss}] semplifica operazioni logiche bitwise.
3467 \item[\ml{WORD\_ARITH\_ss}] semplifica operazioni aritmetiche word. La sottrazione � sostituita con la moltiplicazione da -1.
3468 \item[\ml{WORD\_SHIFT\_ss}] semplifica operazioni shift.
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}.
3470 \item[\ml{WORD\_ARITH\_EQ\_ss}] semplifica \holtxt{``a = b``} to \holtxt{``a - b = 0w``}.
3471 \item[\ml{WORD\_BIT\_EQ\_ss}] espande in modo aggressivo operazioni bit-vector non-aritmetiche in espressioni booleane. (Dovrebbe essere usata con attenzione -- include \ml{fcpLib.FCP\_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.
3484 La seguente sessione mostra \ml{SIZES\_ss}:
3494 Il frammento \ml{BIT\_ss} converte \holtxt{BIT} in un test di appartenenza su un insieme di posizioni bit (pi� alte):
3527 I frammenti rimanenti non sono inclusi in \ml{wordsLib.WORD\_ss} or \ml{srw\_ss}. Il frammento eguaglianza bit � mostrato di sotto.
3536 Il frammento esatto � utile per il ragionamento circa operazioni bit-field ed � usato meglio in combinazione con \ml{wordsLib.SIZES\_ss} o \ml{wordsLib.WORD\_ss}, per esempio:
3546 Infine, il frammento \ml{WORD\_MUL\_LSL\_ss} � mostrato di sotto.
3553 Riscrivere con il teorema \ml{wordsTheory.WORD\_MUL\_LSL} fornisce un mezzo per annullare questa semplificazione, per esempio:
3561 Ovviamente, senza aggiungere delle garanzie, questo teorema di riscrittura non pu� essere dispiegato in combinazione con il frammento \ml{WORD\_MUL\_LSL\_ss}.
3566 \ml{blastLib.BBLAST\_PROVE}. Questa procedura usa il \emph{bit-blasting} ---
3578 I seguenti esempi mostrano \ml{BBLAST\_PROVE} in uso:
3590 La procedura di decisione \ml{BBLAST\_PROVE} � basata sulla conversione
3591 \ml{BBLAST\_CONV}. Questa conversione pu� essere usata per convertire problemi bit-vector
3601 Ci sono anche tattiche bit-blasting: \ml{BBLAST\_TAC} e \ml{FULL\_BBLAST\_TAC}; dove solo la seconda fa uso delle assunzioni del goal.

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