1\chapter{La logica di \HOL{}}\label{HOLlogic} 2 3Il sistema \HOL{} supporta \emph{la logica di ordine superiore}. 4Questa � una versione del calcolo dei predicati con tre estensioni principali: 5 6\begin{itemize} 7\item Le variabili possono variare su funzioni e predicati (da qui `ordine superiore'). 8\item La logica � \emph{tipizzata}. 9\item Non c'� una categoria sintattica separata per le \emph{formule} (i termini di tipo \ml{bool} adempiono a questo ruolo). 10\end{itemize} 11 12In questo capitolo, daremo una breve panoramica della notazione usata per scrivere l'espressioni della logica di \HOL{} in \ML{}, e discuteremo anche alcune tecniche fondamentali di dimostrazione in \HOL{}. 13Si assume che il lettore sia familiare con la logica dei predicati. 14La sintassi e la semantica del particolare sistema logico supportato da \HOL{} � descritta nei dettagli in \DESCRIPTION. I lettori che desiderano vedere \HOL{} in azione, senza l'introduzione ai dettagli pi� sottili dei fondamenti di \HOL, potrebbero preferire di saltare al Capitolo~\ref{chap:euclid}. 15 16 17La tabella di sotto riassume un utile sottoinsieme della notazione (ASCII) usata in \HOL. 18 19\begin{center} 20\begin{tabular}{|l|l|l|l|} \hline 21\multicolumn{4}{|c|}{ } \\ 22\multicolumn{4}{|c|}{\bf Termini della Logica di HOL} \\ 23\multicolumn{4}{|c|}{ } \\ 24{\it Genere di termine} & {\it Notazione \HOL{}} & 25{\it Notazione standard} & 26{\it Descrizione} \\ \hline 27 & & & \\ 28Verit� & {\small\verb|T|} & $\top$ & {\it vero}\\ \hline 29Falsit� & {\small\verb|F|} & $\bot$ & {\it falso}\\ \hline 30Negazione & {\small\verb|~|}$t$ & $\neg t$ & {\it non}$\ t$\\ \hline 31Disgiunzione & $t_1${\small\verb|\/|}$t_2$ & $t_1\vee t_2$ & 32$t_1\ ${\it o}$\ t_2$ \\ \hline 33Congiunzione & $t_1${\small\verb|/\|}$t_2$ & $t_1\wedge t_2$ & 34$t_1\ ${\it e}$\ t_2$ \\ \hline 35Implicazione & $t_1${\small\verb|==>|}$t_2$ & $t_1\imp t_2$ & 36$t_1\ ${\it implica}$\ t_2$ \\ \hline 37Uguaglianza & $t_1${\small\verb|=|}$t_2$ & $t_1 = t_2$ & 38$t_1\ ${\it � uguale a}$\ t_2$ \\ \hline 39Quantificazione-$\forall$ & {\small\verb|!|}$x${\small\verb|.|}$t$ & 40$\uquant{x}t$ & {\it per\ tutti\ gli\ }$x: t$ \\ \hline 41Quantificazione-$\exists$ & {\small\verb|?|}$x${\small\verb|.|}$t$ & 42$\equant{x}\ t$ & {\it per\ qualche\ }$x: t$ \\ \hline 43Termine-$\hilbert$ & {\small\verb|@|}$x${\small\verb|.|}$t$ & 44$\hquant{x}t$ & {\it un}$\ x\ ${\it tale\ che:}$\ t$ \\ \hline 45Condizionale & {\small\verb|if|} $t$ {\small\verb|then|} $t_1$ 46 {\small\verb|else|} $t_2$ & 47$(t\rightarrow t_1, t_2)$ & {\it se\ }$t${\it \ allora\ }$t_1${\it\ altrimenti\ }$t_2$ 48 \\ \hline 49\end{tabular} 50\end{center}\label{logic-table} 51 52I termini della logica di \HOL{} sono rappresentati in \ML{} da un \emph{tipo astratto} chiamato {\small\verb|term|}. 53Normalmente essi sono inseriti tra due segni di doppio accento grave. 54Per esempio, l'espressione \holtxt{``x /\bs{} y ==> z``} � valutata in \ML{} a un termine che rappresenta $\holtxt{x} \land \holtxt{y} \Rightarrow \holtxt{z}$. 55I termini possono essere manipolati da varie funzioni incorporate in \ML{}. 56Per esempio, la funzione \ML{} \ml{dest\_imp} con il tipo \ML{} \ml{term -> term * term} divide un'implicazione in una coppia di termini che consiste nel suo antecedente e nel suo conseguente, e la funzione \ML\ \ml{dest\_conj} di tipo \ml{term -> term * term} divide una congiunzione nei suoi due congiunti% 57\footnote{Tutti gli esempi di sotto assumono che l'utente stia eseguendo \texttt{hol}, il cui eseguibile � nella directory \texttt{bin/}. 58A seconda della configurazione del sistema, � anche possibile che la notazione ASCII utilizzata nelle sessioni di esempio che seguono sia sostituita da una notazione 59Unicode pi� gradevole: in cui per esempio \holtxt{/\bs} � sostituito da $\land$.}. 60 61\setcounter{sessioncount}{0} 62\begin{session} 63\begin{verbatim} 64- ``x /\ y ==> z``; 65> val it = ``x /\ y ==> z`` : term 66 67- dest_imp it; 68> val it = (``x /\ y``, ``z``) : term * term 69 70- dest_conj(#1 it); 71> val it = (``x``, ``y``) : term * term 72\end{verbatim} 73\end{session} 74 75I termini della logica di \HOL{} sono piuttosto simili a espressioni \ML{}, e questo all'inizio pu� confondere. 76Di fatto, i termini della logica hanno tipi analoghi a quelli dell'espressioni \ML{}. 77Per esempio, \holtxt{``(1,2)``} � un'espressione \ML{} con tipo \ML{} \ml{term}. 78Il tipo \HOL{} di questo termine � \holtxt{num \# num}. 79Per contro, l'espressione \ML{} \ml{(``1``, ``2``)} ha il tipo (\ML{}) \ml{term * term}. 80 81\paragraph{Sintassi dei tipi \HOL} 82 83I tipi dei termini \HOL{} formano un tipo \ML{} chiamato \ml{hol_type}. 84L'espressioni che hanno la forma \ml{``: $\cdots$ ``} sono valutate a tipi logici. 85La funzione incorporata \ml{type_of} ha il tipo \ML{} \ml{term->hol_type} e restituisce il tipo logico di un termine. 86 87\begin{session} 88\begin{verbatim} 89- ``(1,2)``; 90> val it = ``(1,2)`` : term 91 92- type_of it; 93> val it = ``:num # num`` : hol_type 94 95- (``1``, ``2``); 96> val it = (``1``, ``2``) : term * term 97 98- type_of(#1 it); 99> val it = ``:num`` : hol_type 100\end{verbatim} 101\end{session} 102 103Per tentare di minimizzare la confusione tra i tipi logici dei termini \HOL{} e i tipi \ML{} di espressioni \ML{}, ci si riferir� ai primi come a \emph{tipi del linguaggio oggetto} e ai secondi come a \emph{tipi del meta-linguaggio}. 104Per esempio, \ml{``(1,T)``} � un'espressione \ML{} che ha il tipo \ml{term} del meta-linguaggio ed � valutato a un termine con il tipo \ml{``:num\#bool``} del linguaggio oggetto. 105% 106\begin{session} 107\begin{verbatim} 108- ``(1,T)``; 109> val it = ``(1,T)`` : term 110 111- type_of it; 112> val it = ``:num # bool`` : hol_type 113\end{verbatim} 114\end{session} 115% 116\paragraph{Costruttori di termine} 117I termini \HOL{} possono essere inseriti, come di sopra, usando \emph{quotation} esplicite, o possono essere costruiti chiamando le funzioni costruttore \ML{}. 118La funzione \ml{mk_var} costruisce una variabile da una stringa e un tipo. 119Nell'esempio di sotto, sono costruite tre variabili di tipo {\small\verb|bool|}. 120Queste sono usate pi� avanti. 121 122\begin{session} 123\begin{verbatim} 124- val x = mk_var("x", ``:bool``) 125 and y = mk_var("y", ``:bool``) 126 and z = mk_var("z", ``:bool``); 127> val x = ``x`` : term 128 val y = ``y`` : term 129 val z = ``z`` : term 130\end{verbatim} 131\end{session} 132 133I costruttori \ml{mk_conj} e \ml{mk_imp} costruiscono rispettivamente delle congiunzioni e delle implicazioni. 134E' disponibile un'ampia collezione di costruttori e distruttori di termini per le teorie core di \HOL. 135 136\begin{session} 137\begin{verbatim} 138- val t = mk_imp(mk_conj(x,y),z); 139> val t = ``x /\ y ==> z`` : term 140\end{verbatim} 141\end{session} 142 143\paragraph{Controllo di tipo} 144 145Di fatto ci sono quattro generi differenti di termini in \HOL: variabili, costanti, applicazioni di funzione (\ml{``$t_1$ $t_2$``}), e lambda astrazioni (\ml{``\bs$x$.$t$``}). 146Termini pi� complicati, come quelli che abbiamo gi� visto di sopra, sono soltanto composizioni di termini da questo semplice insieme. 147Al fine di comprendere il comportamento del parser delle quotation, � necessario capire come il controllore dei tipi deduca i tipi per le quattro categorie base di termini. 148 149Sia le variabili sia le costanti hanno un nome e un tipo; la differenza � che le costanti non possono essere legate da quantificatori, e il loro tipo � fissato quando sono dichiarate (si veda di sotto). 150Quando una quotation � immessa in \HOL{}, l'algoritmo di controllo del tipo usa i tipi delle costanti per dedurre i tipi delle variabili nella stessa quotation. 151Per esempio, nel caso seguente, il controllore di tipi di \HOL{} ha usato il tipo conosciuto \holtxt{bool->bool} della negazione booleana (\holtxt{\td}) per dedurre che la variabile \holtxt{x} deve avere il tipo \holtxt{bool}. 152 153\begin{session} 154\begin{verbatim} 155- ``~x``; 156> val it = ``~x`` : term 157\end{verbatim} 158\end{session} 159 160Nei prossimi due casi, il tipo di \ml{x} e \ml{y} non pu� essere 161dedotto. 162(Di default lo `scopo' dell'informazione di tipo per il controllore di tipo � una singola quotation, cos� un tipo in una quotation non pu� influenzare il controllo di tipo di un'altra. 163Cos� \ml{x} non � costretta ad avere il tipo \ml{bool} nella seconda quotation.) 164 165\begin{session} 166\begin{verbatim} 167- ``x``; 168<<HOL message: inventing new type variable names: 'a.>> 169> val it = ``x`` : Term.term 170 171- type_of it; 172> val it = ``:'a`` : hol_type 173 174- ``(x,y)``; 175<<HOL message: inventing new type variable names: 'a, 'b.>> 176> val it = ``(x,y)`` : term 177 178- type_of it; 179> val it = ``:'a # 'b`` : hol_type 180\end{verbatim} 181\end{session} 182 183Se non c'� abbastanza informazione di tipo determinata dal contesto per risolvere i tipi di tutte le variabili in una quotation, allora il sistema ipotizzer� variabili di tipo differenti per tutte le variabili non vincolate. 184 185\paragraph{Vincoli di tipo} 186 187In alternativa, � possibile indicare esplicitamente i tipi richiesti usando la notazione \ml{``$\mathit{term}$:$\mathit{type}$``}, come illustrato di sotto. 188 189\begin{session} 190\begin{verbatim} 191- ``x:num``; 192> val it = ``x`` : term 193 194- type_of it; 195> val it = ``:num`` : hol_type 196\end{verbatim} 197\end{session} 198 199\paragraph{I tipi delle applicazioni di funzione} 200 201Un'applicazione $(t_1\ t_2)$ � ben tipizzata se $t_1$ � una funzione con tipo $\tau_1 \to \tau_2$ e $t_2$ ha tipo $\tau_1$. 202Vice versa, un'applicazione $(t_1\ t_2)$ � mal tipizzata se $t_1$ non � una funzione: 203 204\begin{session} 205\begin{verbatim} 206- ``1 2``; 207 208Type inference failure: unable to infer a type for the application of 209 210(1 :num) 211 212to 213 214(2 :num) 215 216unification failure message: unify failed 217! Uncaught exception: 218! HOL_ERR 219\end{verbatim} 220\end{session} 221 222\noindent oppure se � una funzione, ma $t_2$ non � il suo dominio: 223 224\begin{session} 225\begin{verbatim} 226- ``~1``; 227 228Type inference failure: unable to infer a type for the application of 229 230$~ :bool -> bool 231 232at line 1, character 3 233 234to 235 236(1 :num) 237 238unification failure message: unify failed 239! Uncaught exception: 240! HOL_ERR 241\end{verbatim} 242\end{session} 243 244Il simbolo di dollaro all'inizio di \holtxt{\td} indica che la costante di negazione booleana ha uno stato sintattico speciale (in questo caso una precedenza non standard). 245Mettere \holtxt{\$} davanti a un simbolo qualsiasi fa s� che il parser ignori qualsiasi status sintattico speciale esso possa avere (come l'essere un infisso). 246Lo stesso effetto si pu� ottenere racchiudendo il simbolo fra parentesi. 247Questo � analogo al modo in cui \texttt{op} � usato in \ML. 248 249\begin{session} 250\begin{verbatim} 251- ``$==> t1 t2``; 252> val it = ``t1 ==> t2`` : term 253 254- ``(/\) t1 t2``; 255> val it = ``t1 /\ t2`` : term 256\end{verbatim} 257\end{session} 258 259\paragraph{I tipi delle funzioni} 260 261Le funzioni hanno tipi della forma \ml{$\sigma_1$->$\sigma_2$}, dove $\sigma_1$ e $\sigma_2$ sono i tipi del dominio e del rango della funzione, rispettivamente. 262 263\begin{session} 264\begin{verbatim} 265- type_of ``(==>)``; 266> val it = ``:bool -> bool -> bool`` : hol_type 267 268- type_of ``$+``; 269> val it = ``:num -> num -> num`` : hol_type $ 270\end{verbatim} 271\end{session} 272 273\noindent Di nuovo, sia \holtxt{+} che \holtxt{==>} sono infissi, cos� il loro uso in contesti dove non sono usati come tali richiede un'escaping della sintassi. 274La sessione di sotto illustra l'uso di queste costanti come infissi, illustra anche i tipi del linguaggio oggetto di contro a quelli del meta-linguaggio. 275 276\begin{session} 277\begin{verbatim} 278- ``(x + 1, t1 ==> t2)``; 279> val it = ``(x + 1,t1 ==> t2)`` : term 280 281- type_of it; 282> val it = ``:num # bool`` : hol_type 283 284- (``x=1``, ``t1==>t2``); 285> val it = (``x = 1``, ``t1 ==> t2``) : term * term 286 287- (type_of (#1 it), type_of (#2 it)); 288> val it = (``:bool``, ``:bool``) : hol_type * hol_type 289\end{verbatim} 290\end{session} 291 292I lambda-termini, o $\lambda$-termini, denotano funzioni. 293Il simbolo `\holtxt{\bs}' � usato come una approssimazione ASCII di $\lambda$. 294Cos� `{\small\verb|\|}$x$\ml{.}$t$' dovrebbe essere letto come `$\lquant{x}t$'. 295Per esempio, {\small\verb|``\x. x+1``|} � un termine che denota la funzione $n\mapsto n{+}1$. 296 297\begin{session} 298\begin{verbatim} 299- ``\x. x + 1``; 300> val it = ``\x. x + 1`` : term 301 302- type_of it; 303> val it = ``:num -> num`` : hol_type 304\end{verbatim} 305\end{session} 306 307Altri due simboli di binding nella logica sono i suoi due pi� importanti quantificatori: \ml{!} e \ml{?}, i quantificatori universale ed esistenziale. 308Per esempio, l'enunciato logico che ogni numero � pari o dispari potrebbe essere espresso come 309\begin{verbatim} 310 !n. (n MOD 2 = 1) \/ (n MOD 2 = 0) 311\end{verbatim} 312mentre una versione del risultato di Euclide circa l'infinit� dei numeri primi �: 313\begin{verbatim} 314 !n. ?p. prime p /\ p > n 315\end{verbatim} 316% 317Simboli di binding come questi possono essere usati su pi� `parametri' cos�: 318\begin{session} 319\begin{verbatim} 320- ``\x y. (x, y * x)``; 321> val it = ``\x y. (x,y * x)`` : term 322 323- type_of it; 324> val it = ``:num -> num -> num # num`` : hol_type 325 326- ``!x y. x <= x + y``; 327> val it = ``!x y. x <= x + y`` : term 328\end{verbatim} 329\end{session} 330 331 332\section{Dimostrazioni di base in \HOL{}} 333 334\newcommand\tacticline{\hline \hline} 335\newenvironment{proofenumerate}{\begin{enumerate}}{\end{enumerate}} 336% proofenumerate is distinguished from a normal enumeration so that 337% h e v e a can spot these special cases and treat them better. 338 339\setcounter{sessioncount}{0} 340 341Questa sezione discute la natura della dimostrazione in \HOL{}. 342Per un logico, una\linebreak definizione di una dimostrazione formale � che � una sequenza, ciascuno dei cui elementi � o un \emph{assioma} o segue dai membri precedenti della sequenza da una \emph{regola d'inferenza}. 343Un teorema � l'ultimo elemento di una dimostrazione. 344 345I teoremi sono rappresentati in \HOL{} da valori di un tipo astratto \ml{thm}. 346L'unico modo per creare teoremi � quello di generare una tale dimostrazione. 347In \HOL, seguendo lo stile \LCF, questo consiste nell'applicazione di funzioni \ML{} che rappresentano \emph{regole d'inferenza} ad assiomi o teoremi generati in precedenza. 348La sequenza di tali applicazioni corrisponde direttamente alla dimostrazione di un logico. 349 350Ci sono cinque assiomi della logica di \HOL{} e otto regole primitive d'inferenza. 351Gli assiomi sono legati a nomi ML. 352Per esempio, la Legge del Terzo Escluso � legata al nome \ML{} \ml{BOOL_CASES_AX}:\footnote{% 353Si noti ora come il printer di termini rende le uguaglianze nel teorema con il simbolo \holtxt{<=>} piuttosto che \holtxt{=}. 354La costante sottostante � la stessa, ma il modo in cui � stampata � un indizio per l'utente che si tratta dell'uguaglianza su valori booleani. 355Il parser accetta sia \holtxt{<=>} che \holtxt{=} con argomenti booleani; tentare di usare \holtxt{<=>} su valori che non sono di tipo booleano (diciamo numeri) risulter� in un errore di parsing.% 356} 357 358\begin{session} 359\begin{verbatim} 360- BOOL_CASES_AX; 361> val it = |- !t. (t <=> T) \/ (t <=> F) : thm 362\end{verbatim} 363\end{session} 364 365 366I teoremi sono stampati con un turnstile anteposto {\small\verb+|-+} come illustrato di sotto; il simbolo `{\small\verb|!|}' � il quantificatore universale `$\forall$'. 367Le regole d'inferenza sono funzioni \ML{} che restituiscono valori di tipo \ml{thm}. 368Un esempio di una regola d'inferenza � la {\it specializzazione\/} (o $\forall$-eliminazione). 369Nella notazione standard della `deduzione naturale' questo �: 370 371\[ \frac{\Gamma\turn \uquant{x}t}{\Gamma\turn t[t'/x]}\] 372 373\begin{itemize} 374\item $t[t'/x]$ denota il risultato della sostituzione di $t'$ per tutte le occorrenze libere di $x$ in $t$, con la restrizione che nessuna variabile libera in $t'$ venga legata dopo la sostituzione. 375\end{itemize} 376 377\noindent Questa regola � rappresentata in \ML{} da una funzione \ml{SPEC},% 378\footnote{\ml{SPEC} non � una regola primitiva d'inferenza nella logica HOL, ma � una regola derivata. 379Le regole derivate sono descritte nella Sezione~\ref{forward}.} 380che prende come argomenti un termine \ml{``$a$``} e un teorema \holtxt{|-~!$x.\,t[x]$} e restituisce il teorema \holtxt{|-~$t[a]$}, il risultato della sostituzione di $a$ per $x$ in $t[x]$. 381 382\begin{session} 383\begin{verbatim} 384- val Th1 = BOOL_CASES_AX; 385> val Th1 = |- !t. (t <=> T) \/ (t <=> F) : thm 386 387- val Th2 = SPEC ``1 = 2`` Th1; 388> val Th2 = |- ((1 = 2) <=> T) \/ ((1 = 2) <=> F) : thm 389\end{verbatim} 390\end{session} 391 392Questa sessione consiste di una dimostrazione di due passi: usando un assioma e applicando la regola \ml{SPEC}; essa esegue in modo interattivo la seguente dimostrazione: 393\begin{samepage} 394\begin{proofenumerate} 395\item $ \turn \uquant{t}\;\; t\Leftrightarrow\top \;\disj\; t\Leftrightarrow\bot$ \hfill 396[Assioma \ml{BOOL\_CASES\_AX}] 397\item $ \turn (1{=}2)\Leftrightarrow\top\ \disj\ (1{=}2)\Leftrightarrow\bot$\hfill [Specializzazione della linea 1 a `$1{=}2$'] 398\end{proofenumerate} 399\end{samepage} 400 401Se l'argomento a una funzione \ML{} che rappresenta una regola d'inferenza � del genere sbagliato, o viola una condizione della regola, allora l'applicazione fallisce. 402Per esempio, $\ml{SPEC}\ t\ th$ fallir� se $th$ non � della forma $\ml{|-\ !}x\ml{.}\cdots$ o se � di questa forma ma il tipo di $t$ non � lo stesso del tipo di $x$, o se non � soddisfatta la restrizione della variabile libera. 403Quando � sollevata una delle eccezioni \ml{HOL\_ERR} standard, si pu� spesso ottenere pi� informazione circa il fallimento usando la funzione \ml{Raise}.% 404\footnote{La funzione \ml{Raise} passa su tutte le eccezioni che vede; essa non incide per nulla sulla semantica della computazione. 405Comunque, quando le viene passata un'eccezione \ml{HOL\_ERR}, stampa alcune utili informazioni prima di passare l'eccezione al livello successivo.}. 406 407\begin{session} 408\begin{verbatim} 409- SPEC ``1=2`` Th2; 410! Uncaught exception: 411! HOL_ERR 412 413- SPEC ``1 = 2`` Th2 handle e => Raise e; 414 415Exception raised at Thm.SPEC: 416 417! Uncaught exception: 418! HOL_ERR 419\end{verbatim} 420\end{session} 421Comunque, come illustra questa sessione, il messaggio di fallimento non sempre indica la ragione esatta del fallimento. 422In \REFERENCE\ sono date dettagliate condizioni di fallimento per le regole d'inferenza. 423 424Nel sistema \HOL{} una dimostrazione � costruita applicando ripetutamente regole\linebreak d'inferenza ad assiomi o a teoremi dimostrati in precedenza. 425Dal momento che le dimostrazioni possono consistere di milioni di passi, � necessario fornire strumenti per rendere pi� facile la costruzione della dimostrazione da parte dell'utente. 426Gli strumenti che generano dimostrazioni nel sistema \HOL{} sono soltanto quelli di \LCF, e sono descritti pi� avanti. 427 428La forma generale di un teorema � $t_1,\ldots,t_n\;\ml{|-}\;t$, dove $t_1$, $\ldots$ , $t_n$ sono termini booleani chiamati le {\it assunzioni} e $t$ � un termine booleano chiamato la {\it conclusione\/}. 429Un tale teorema afferma che se le sue assunzioni sono vere allora lo � anche la sua conclusione. 430Le sue condizioni di verit� sono cos� le stesse di quelle per il 431singolo termine $(t_1\,\ml{/\bs}\ldots\ml{/\bs}\,t_n)\,\ml{==>}\,t$. 432I teoremi senza assunzioni sono stampati nella forma \ml{|-}$\ t$. 433 434I cinque assiomi e le otto regole primitive d'inferenza della logica di \HOL{} sono descritte nel dettaglio nel documento \DESCRIPTION. 435Ogni valore di tipo \ml{thm} nel sistema \HOL{} si pu� ottenere applicando ripetutamente regole primitive d'inferenza agli assiomi. 436Quando il sistema \HOL{} � costruito, le otto regole primitive d'inferenza sono definite e i cinque assiomi sono legati ai loro nomi \ML{}. 437Tutti gli altri teoremi predefiniti sono dimostrati usando le regole d'inferenza mentre il sistema si costruisce\footnote{Questa � una semplificazione leggeremnte eccessiva}. 438Questa � una delle ragioni per cui la costruzione di \ml{hol} richiede cos� tanto tempo. 439 440Nel resto di questa sezione, il processo di \emph{dimostrazione in avanti}, che � stato appena abbozzato, � descritto in maggior dettaglio. 441Nella Sezione~\ref{tactics} � descritta la \emph{dimostrazione diretta dal goal}, incluse le importanti nozioni di \emph{tattiche} e \emph{tatticali}, dovute a Robin Milner. 442 443\section{Dimostrazione in avanti} 444\label{forward} 445 446Tre delle regole primitive d'inferenza della logica \HOL{} sono 447\ml{ASSUME} (introduzione di un'assunzione), \ml{DISCH} (scaricamento o 448eliminazione di un'assunzione) e \ml{MP} (Modus Ponens). Queste regole saranno 449usate per illustrare la dimostrazione in avanti e la scrittura di regole derivate. 450 451La regola d'inferenza \ml{ASSUME} genera teoremi della forma \ml{$t$ 452 |- $t$}. Si noti, comunque, che il printer \ML{} stampa ogni 453assunzione come un punto (ma questo default pu� essere cambiato; si veda di sotto). La 454funzione \ml{dest\_thm} decompone un teorema in una coppia che consiste nella 455lista delle assunzioni e nella conclusione 456 457\begin{session} 458\begin{verbatim} 459- val Th3 = ASSUME ``t1==>t2``;; 460> val Th3 = [.] |- t1 ==> t2 : thm 461 462- dest_thm Th3; 463> val it = ([``t1 ==> t2``], ``t1 ==> t2``) : term list * term 464\end{verbatim} 465\end{session} 466 467Una sorta di duale di \ml{ASSUME} � la regola primitiva d'inferenza 468\ml{DISCH} (scaricamento, eliminazione di un'assunzione) che deduce da 469un teorema della forma $\cdots t_1\cdots\ml{\ |-\ }t_2$ il nuovo teorema 470$\cdots\ \cdots\ \ml{|-}\ t_1\ml{==>}t_2$. \ml{DISCH} prende come argomenti 471il termine che deve essere scaricato (\ie\ $t_1$) e il teorema da cui 472le assunzioni devono essere scaricate e restituisce il risultato dello scaricamento. 473La seguente sessione illustra questo: 474 475\begin{session} 476\begin{verbatim} 477- val Th4 = DISCH ``t1==>t2`` Th3; 478> val Th4 = |- (t1 ==> t2) ==> t1 ==> t2 : thm 479\end{verbatim} 480\end{session} 481Si noti che non � necessario che il termine che deve essere scaricato sia nelle assunzioni; in 482questo caso esse rimarranno invariate. 483 484\begin{session} 485\begin{verbatim} 486- DISCH ``1=2`` Th3; 487> val it = [.] |- (1 = 2) ==> t1 ==> t2 : thm 488 489- dest_thm it; 490> val it = ([``t1 ==> t2``], ``(1 = 2) ==> t1 ==> t2``) : term list * term 491\end{verbatim} 492\end{session} 493 494In \HOL\, la regola \ml{MP} del Modus Ponens � specificata nella notazione convenzionale da: 495\[ 496\frac{\Gamma_1 \turn t_1 \imp t_2 \qquad\qquad \Gamma_2\turn t_1} 497{\Gamma_1 \cup \Gamma_2 \turn t_2} 498\] 499La funzione \ML{} \ml{MP} prende come argomenti teoremi della forma 500\ml{$\cdots\ $|-$\ t_1$\ ==>\ $t_2$} e \ml{$\cdots\ $|-$\ t_1$} e 501restituisce \ml{$\cdots\ $|-$\ t_2$}. La prossima sessione illustrer� l'uso 502di \ml{MP} e anche un errore comune, cio� il non fornire informazione sufficiente 503al controllore di tipo logico di \HOL\ . 504 505\begin{session} 506\begin{verbatim} 507- val Th5 = ASSUME ``t1``; 508<<HOL message: inventing new type variable names: 'a.>> 509! Uncaught exception: 510! HOL_ERR 511- val Th5 = ASSUME ``t1`` handle e => Raise e; 512<<HOL message: inventing new type variable names: 'a.>> 513 514Exception raised at Thm.ASSUME: 515not a proposition 516! Uncaught exception: 517! HOL_ERR 518 519- val Th5 = ASSUME ``t1:bool``; 520> val Th5 = [.] |- t1 : thm 521 522- val Th6 = MP Th3 Th5; 523> val Th6 = [..] |- t2 : thm 524\end{verbatim} 525\end{session} 526 527Le ipotesi di \ml{Th6} possono essere ispezionate con la funzione \ML{} 528\ml{hyp}, che restituisce la lista delle assunzioni di un teorema (la 529conclusione � restituita da \ml{concl}). 530 531\begin{session} 532\begin{verbatim} 533- hyp Th6; 534> val it = [``t1 ==> t2``, ``t1``] : term list 535\end{verbatim} 536\end{session} 537 538Si pu� far s� che \HOL{} stampi in modo esplicito le ipotesi dei teoremi impostando il flag globale \ml{show\_assums} a vero. 539 540\begin{session} 541\begin{verbatim} 542- show_assums := true; 543> val it = () : unit 544 545- Th5; 546> val it = [t1] |- t1 : thm 547 548- Th6; 549> val it = [t1 ==> t2, t1] |- t2 : thm 550\end{verbatim} 551\end{session} 552 553 554\noindent Scaricando \ml{Th6} due volte si stabilisce il teorema 555\ml{|-\ t1 ==> (t1==>t2) ==> t2}. 556 557\begin{session} 558\begin{verbatim} 559- val Th7 = DISCH ``t1==>t2`` Th6; 560> val Th7 = [t1] |- (t1 ==> t2) ==> t2 : thm 561 562- val Th8 = DISCH ``t1:bool`` Th7; 563> val Th8 = |- t1 ==> (t1 ==> t2) ==> t2 : thm 564\end{verbatim} 565\end{session} 566 567La sequenza di teoremi: \ml{Th3}, \ml{Th5}, \ml{Th6}, \ml{Th7}, \ml{Th8} costituisce una dimostrazione in \HOL{} del teorema \ml{|-\ t1 ==> (t1 ==> t2) ==> t2}. 568In notazione logica standard questa dimostrazione potrebbe essere scritta: 569 570\begin{proofenumerate} 571\item $ t_1\imp t_2\turn t_1\imp t_2$ \hfill 572[Introduzione di assunzione] 573\item $ t_1\turn t_1$ \hfill 574[Introduzione di assunzione] 575\item $ t_1\imp t_2,\ t_1 \turn t_2 $ \hfill 576[Modus Ponens applicato alle linee 1 e 2] 577\item $ t_1 \turn (t_1\imp t_2)\imp t_2$ \hfill 578[Scaricamento della prima assunzione della linea 3] 579\item $ \turn t_1 \imp (t_1 \imp t_2) \imp t_2$ \hfill 580[Scaricamento dell'unica assunzione della linea 4] 581\end{proofenumerate} 582 583\subsection{Regole derivate} 584 585 586Una \emph{dimostrazione dalle ipotesi} $th_1, \ldots, th_n$ � una sequenza ciascuno dei cui elementi � o un assioma, o una delle ipotesi $th_i$, o segue dagli elementi precedenti per mezzo di una regola d'inferenza. 587 588Per esempio, una dimostrazione di $\Gamma,\ t'\turn t$ dalle ipotesi $\Gamma\turn t$ �: 589 590\begin{proofenumerate} 591\item $ t'\turn t'$ \hfill [Introduzione di assunzione] 592\item $ \Gamma\turn t$ \hfill [Ipotesi] 593\item $ \Gamma\turn t'\imp t$ \hfill [Scarica $t'$ dalla linea 2] 594\item $ \Gamma,\ t'\turn t$ \hfill [Modus Ponens applicato alle linee 3 e 1] 595\end{proofenumerate} 596 597\noindent Questa dimostrazione funziona per qualunque ipotesi della forma $\Gamma\turn t$ 598e qualsiasi termine booleano $t'$ e mostra che il risultato di aggiungere un'ipotesi 599arbitraria a un teorema � un altro teorema (perch� le quattro 600linee di sopra possono essere aggiunte a qualsiasi dimostrazione di $\Gamma\turn t$ per ottenere una 601dimostrazione di $\Gamma,\ t'\turn t$)\footnote{Questa propriet� della logica � 602 chiamata {\it monotonicit�}.}. Per esempio, la prossima sessione usa questa 603dimostrazione per aggiungere l'ipotesi \ml{``t3``} a \ml{Th6}. 604 605\begin{session} 606\begin{verbatim} 607- val Th9 = ASSUME ``t3:bool``; 608> val Th9 = [t3] |- t3 : thm 609 610- val Th10 = DISCH ``t3:bool`` Th6; 611> val Th10 = [t1 ==> t2, t1] |- t3 ==> t2 : thm 612 613- val Th11 = MP Th10 Th9; 614> val Th11 = [t1 ==> t2, t1, t3] |- t2 : thm 615\end{verbatim} 616\end{session} 617 618 619 Una {\it regola derivata\/} � una procedura \ML{} che genera una dimostrazione 620 dalle ipotesi date ogni volta che � invocata. Le ipotesi sono 621 gli argomenti della regola. Per illustrare questo, una regola, chiamata 622 \ml{ADD\_ASSUM}, sar� ora definita come una procedura \ML{} che 623 svolge la dimostrazione di sopra. In notazione standard questo sarebbe 624 descritto da: 625 626\[ \frac{\Gamma\turn t}{\Gamma,\ t'\turn t} \] 627 628\noindent La definizione \ML{} �: 629 630\begin{session} 631\begin{verbatim} 632- fun ADD_ASSUM t th = let 633 val th9 = ASSUME t 634 val th10 = DISCH t th 635 in 636 MP th10 th9 637 end; 638> val ADD_ASSUM = fn : term -> thm -> thm 639 640- ADD_ASSUM ``t3:bool`` Th6; 641> val it = [t1, t1 ==> t2, t3] |- t2 : thm 642\end{verbatim} 643\end{session} 644 645\noindent Il corpo di \ml{ADD\_ASSUM} � stato codificato per riflettere la dimostrazione fatta 646nella sessione~10 di sopra, cos� da mostrare come una dimostrazione interattiva pu� essere 647generalizzata in una procedura. Ma \ml{ADD\_ASSUM} pu� essere scritta in modo 648molto pi� conciso come. 649 650\begin{session} 651\begin{verbatim} 652- fun ADD_ASSUM t th = MP (DISCH t th) (ASSUME t); 653> val ADD_ASSUM = fn : term -> thm -> thm 654 655- ADD_ASSUM ``t3:bool`` Th6; 656val it = [t1 ==> t2, t1, t3] |- t2 : thm 657\end{verbatim} 658\end{session} 659 660Un altro esempio di una regola d'inferenza derivata � \ml{UNDISCH}; questa sposta l'antecedente di un'implicazione nelle assunzioni. 661\[ 662\frac{\Gamma\turn t_1\imp t_2}{\Gamma,\ t_1\turn t_2} 663\] 664Una regola derivata \ML{} che implementa questo �: 665 666 667\begin{session} 668\begin{verbatim} 669- fun UNDISCH th = MP th (ASSUME(#1(dest_imp(concl th)))); 670> val UNDISCH = fn : thm -> thm 671 672- Th10; 673> val it = [t1 ==> t2, t1] |- t3 ==> t2 : thm 674 675- UNDISCH Th10; 676> val it = [t1, t1 ==> t2, t3] |- t2 : thm 677\end{verbatim} 678\end{session} 679 680\noindent Ogni volta che � eseguita \ml{UNDISCH\ $\Gamma\turn t_1\imp t_2$}, 681� svolta la seguente dimostrazione: 682 683\begin{proofenumerate} 684\item $ t_1\turn t_1$ \hfill [Introduzione di assunzione] 685\item $ \Gamma\turn t_1\imp t_2$ \hfill [Ipotesi] 686\item $ \Gamma,\ t_1\turn t_2$ \hfill [Modus Ponens applicata alle linee 2 and 1] 687\end{proofenumerate} 688 689Le regole \ml{ADD\_ASSUM} e \ml{UNDISCH} sono le prime regole derivate 690definite quando il sistema \HOL{} � costruito. Per una descrizione delle regole 691principali si veda la sezione sulle regole derivate in \DESCRIPTION. 692 693\subsubsection{Riscrittura} 694 695Un'interessante regola derivata � \ml{REWRITE\_RULE}. Questa prende una lista di 696teoremi equazionali della forma: 697 698\[ 699\Gamma\turn (u_1 = v_1) \conj (u_2 = v_2) \conj \ldots\ \conj (u_n = v_n) 700\] 701e un teorema $\Delta\turn t$ e sostituisce ripetutamente istanze di $u_i$ in $t$ con l'istanza corrispondente di $v_i$ fino a quando non occorrono altri cambiamenti. 702Il risultato � un teorema $\Gamma\cup\Delta\turn t'$ dove $t'$ � il risultato di riscrivere $t$ in questo modo. 703La sessione di sotto illustra l'uso di \ml{REWRITE\_RULE}. 704In essa la lista di equazioni � il valore \ml{rewrite\_list} che contiene i teoremi pre-dimostrati \ml{ADD\_CLAUSES} and \ml{MULT\_CLAUSES}. 705Questi teoremi appartengono alla teoria \ml{arithmetic}, cos� per riferirsi ad essi dobbiamo usare un nome completo con il nome della teoria come primo componente. 706(In alternativa, potremmo, come nell'esempio Euclide della sezione~\ref{chap:euclid}, usare \ml{open} per dichiarare tutti i valori nella teoria al top level.) 707 708\begin{session} 709\begin{verbatim} 710- open arithmeticTheory; 711 ... 712 713- val rewrite_list = [ADD_CLAUSES,MULT_CLAUSES]; 714> val rewrite_list = 715 [ |- (0 + m = m) /\ (m + 0 = m) /\ (SUC m + n = SUC (m + n)) /\ 716 (m + SUC n = SUC (m + n)), 717 |- !m n. 718 (0 * m = 0) /\ (m * 0 = 0) /\ (1 * m = m) /\ (m * 1 = m) /\ 719 (SUC m * n = m * n + n) /\ (m * SUC n = m + m * n)] 720 : thm list 721\end{verbatim} 722\end{session} 723 724\begin{session} 725\begin{verbatim} 726- REWRITE_RULE rewrite_list (ASSUME ``(m+0)<(1*n)+(SUC 0)``); 727> val it = [m + 0 < 1 * n + SUC 0] |- m < SUC n : thm 728\end{verbatim} 729\end{session} 730 731\noindent 732Questo pu� essere riscritto usando un altro teorema pre-dimostrato 733\ml{LESS\_THM}, che appartiene alla teoria \ml{prim\_rec}: 734 735\begin{session} 736\begin{verbatim} 737- REWRITE_RULE [prim_recTheory.LESS_THM] it; 738> val it = [m + 0 < 1 * n + SUC 0] |- (m = n) \/ m < n : thm 739\end{verbatim} 740\end{session} 741 742\ml{REWRITE\_RULE} non � una regola primitiva in \HOL, ma � una regola derivata. 743E' ereditata dal Cambridge \LCF\ e fu implementata da Larry Paulson (per i dettagli si veda il suo scritto \cite{lcp-rewrite}). 744In aggiunta alle equazioni fornite, \ml{REWRITE\_RULE} ha incorporate alcune semplificazioni standard: 745 746\begin{session} 747\begin{verbatim} 748- REWRITE_RULE [] (ASSUME ``(T /\ x) \/ F ==> F``); 749> val it = [T /\ x \/ F ==> F] |- ~x : thm 750\end{verbatim} 751\end{session} 752 753Ci sono degli strumenti elaborati in \HOL{} per produrre riscritture personalizzate che eseguono la scansione dei termini in un ordine programmato dall'utente; \ml{REWRITE\_RULE} � la punta di un iceberg, si veda \DESCRIPTION\ per maggiori dettagli. 754 755\section{Dimostrazioni Dirette dal Goal: Tattiche e Tatticali} 756\label{backward}\label{tactics} 757 758Lo stile della dimostrazione in avanti descritto nella sessione precedente � 759innaturale e troppo di `basso livello' per molte applicazioni. Un importante 760passo in avanti nella metodologia di generazione delle dimostrazioni fu fatto da Robin Milner nei primi 761anno 1970 quando invent� la nozione delle {\it tattiche\/}. Una 762tattica � una funzione che fa le seguenti cose. 763\begin{myenumerate} 764\item Divide un `goal' in `subgoals'. 765\item Tiene traccia del motivo per cui risolvere i subgoals risolve il goal. 766\end{myenumerate} 767 768\noindent Si consideri, per esempio, la regola di $\wedge$-introduzione\footnote{Nella 769 logica di ordine superiore questa � una regola derivata; nella logica del primo ordine essa 770 di solito � primitiva. In HOL la regola � chiamata {\tt CONJ} e la sua 771 derivazione � data in \DESCRIPTION.} mostrata di sotto: 772 773\[ \frac{\Gamma_1\turn 774t_1\qquad\qquad\qquad\Gamma_2\turn t_2}{\Gamma_1\cup\Gamma_2 \turn t_1\conj 775t_2} \] 776 777 778\noindent In \HOL, la $\wedge$-introduzione � rappresentata dalla funzione \ML{} 779\ml{CONJ}: 780 781\[\ml{CONJ}\ (\Gamma_1\turn t_1)\ (\Gamma_2\turn t_2) \ \ \leadsto\ 782\ (\Gamma_1\cup\Gamma_2\turn t_1\conj t_2)\] 783 784\noindent Questo � illustrato nella 785seguente nuova sessione (si noti che il numero di sessione � stata reimpostato a 786{\small\sl 1}: 787 788\setcounter{sessioncount}{0} 789\begin{session} 790\begin{verbatim} 791- show_assums := true; 792val it = () : unit 793 794- val Th1 = ASSUME ``A:bool`` and Th2 = ASSUME ``B:bool``; 795> val Th1 = [A] |- A : thm 796 val Th2 = [B] |- B : thm 797 798- val Th3 = CONJ Th1 Th2; 799> val Th3 = [A, B] |- A /\ B : thm 800\end{verbatim} 801\end{session} 802 803 Si supponga che il goal sia dimostrare $A\conj B$, quindi questa regola dice che 804 � sufficiente dimostrare i due subgoal $A$ e $B$, perch� 805 da $\turn A$ e $\turn B$ pu� essere dedotto il teorema 806 $\turn A\conj B$. Cos�: 807 808\begin{myenumerate} 809\item Per dimostrare $\turn A \conj B$ � sufficiente 810 dimostrare $\turn A$ e $\turn B$. 811\item La giustificazione per la riduzione del 812goal $\turn A \conj B$ ai due subgoals $\turn A$ 813e $\turn B$ � la regola di $\wedge$-introduzione. 814\end{myenumerate} 815 816Un \emph{goal} in \HOL{} � una coppia \ml{([$t_1$,\ldots,$t_n$],$t$)} di tipo \ML{} \ml{term list~*~term}. 817Una \emph{realizzazione} di un tale goal � un teorema \ml{$t_1$,$\ldots$,$t_n$\ |-\ $t$}. 818Una tattica � una funzione \ML{} che quando applicata a un goal genera i subgoal insieme con una \emph{funzione di giustificazione} o di {\it validazione\/}, che sar� una regola d'inferenza derivata \ML{}, che pu� essere usata per inferire una realizzazione del goal originale dalla realizzazione dei subgoal. 819 820Se $T$ � una tattica (cio� una funzione \ML{} di tipo\linebreak \ml{goal\,->\,(goal\,list\,*\,(thm\,list\,->\,thm))}) e $g$ � un goal, allora applicare $T$ a 821$g$ (cio� valutare l'espressione \ML{} $T\ g$) risulter� in un 822oggetto che � una coppia il cui primo componente � una lista di goal e 823il cui secondo componente � una funzione di giustificazione, cio� un valore con 824tipo \ML{} {\small\verb|thm list -> thm|}. 825 826Un esempio di tattica � \ml{CONJ\_TAC} che implementa (i) e (ii) di sopra. 827Per esempio, si consideri il goal del tutto banale di mostrare \holtxt{T~/\bs{}~T}, dove \ml{T} � una costante che sta per $\top$ (verit�): 828 829\begin{session} 830\begin{verbatim} 831- val goal1 = ([]:term list, ``T /\ T``); 832> val goal1 = ([], ``T /\ T``) : term list * term 833 834- CONJ_TAC goal1; 835> val it = 836 ([([], ``T``), ([], ``T``)], fn) 837 : (term list * term) list * (thm list -> thm) 838 839- val (goal_list,just_fn) = it; 840> val goal_list = 841 [([], ``T``), ([], ``T``)] 842 : (term list * term) list 843 val just_fn = fn : thm list -> thm 844\end{verbatim} 845\end{session} 846 847\noindent \ml{CONJ\_TAC} ha prodotto una lista di goal che consiste di due subgoal 848identici di dimostrare soltanto \ml{([],"T")}. Ora, c'� un teorema 849pre-dimostrato in \HOL, chiamato \ml{TRUTH}, che ottiene questo goal. 850 851\begin{session} 852\begin{verbatim} 853- TRUTH; 854> val it = [] |- T : thm 855\end{verbatim} 856\end{session} 857 858\noindent Applicare la funzione di giustificazione \ml{just\_fn} a una lista 859di teoremi che ottengono i goal nella \ml{goal\_list} risulta 860in un teorema che ottiene il goal originario: 861 862\begin{session} 863\begin{verbatim} 864- just_fn [TRUTH,TRUTH]; 865> val it = [] |- T /\ T : thm 866\end{verbatim} 867\end{session} 868 869 Nonostante questo esempio sia banale, esso illustra l'idea 870 essenziale delle tattiche. Si noti che le tattiche non sono delle primitive 871 speciali di dimostrazione di teoremi; esse sono solo funzioni \ML{}. Per 872 esempio, la definizione di \ml{CONJ\_TAC} � semplicemente: 873 874\begin{hol} 875\begin{verbatim} 876 fun CONJ_TAC (asl,w) = let 877 val (l,r) = dest_conj w 878 in 879 ([(asl,l), (asl,r)], fn [th1,th2] => CONJ th1 th2) 880 end 881\end{verbatim} 882\end{hol} 883 884\noindent La funzione \ml{dest\_conj} divide una congiunzione nei suoi 885due congiunti: se\linebreak \ml{(asl,``$t_1$}{\small\verb|/\|}\ml{$t_2$``)} � un 886goal, allora \ml{CONJ\_TAC} lo divide nella lista dei due subgoal 887\ml{(asl,$t_1$)} e \ml{(asl,$t_2$)}. La funzione di giustificazione, 888{\small\verb|fn [th1,th2] => CONJ th1 th2|} prende una lista 889di teoremi \ml{[$th_1$,$th_2$]} e applica la regola \ml{CONJ} a 890$th_1$ e $th_2$. 891 892Riassumendo: se $T$ � una tattica e $g$ � un goal, allora l'applicazione di $T$ 893a $g$ risulter� in una coppia il cui primo componente � una lista di goal 894e il cui secondo componente � una funzione di giustificazione, con tipo \ML{} 895{\small\verb|thm list -> thm|}. 896 897Supponiamo 898$T\ g${\small\verb| = ([|}$g_1${\small\verb|,|}$\ldots${\small\verb|,|}$g_n${\small\verb|],|}$p${\small\verb|)|}. 899L'idea � che $g_1$ , $\ldots$ , $g_n$ siano subgoal e $p$ sia una 900`giustificazione' della riduzione del goal $g$ ai subgoal $g_1$ , 901$\ldots$ , $g_n$. Supponiamo inoltre che i subgoal $g_1$ , $\ldots$ 902, $g_n$ siano stati risolti. Questo significherebbe che i teoremi $th_1$ , 903$\ldots$ , $th_n$ sono stati dimostrati in modo tale che $th_i$ ($1\leq i\leq 904n$) `ottiene' il goal $g_i$. La giustificazione $p$ (prodotta 905dall'applicazione di $T$ a $g$) � una funzione \ML{} che quando applicata alla 906lista 907{\small\verb|[|}$th_1${\small\verb|,|}$\ldots${\small\verb|,|}$th_n${\small\verb|]|} 908restituisce un teorema $th$, che `ottiene' il goal originario $g$. Cos� 909$p$ � una funzione per convertire una soluzione dei subgoal in una 910soluzione del goal originario. Se $p$ fa questo con successo, allora la 911tattica $T$ � chiamata {\it valida\/}. Tattiche non valide non possono risultare nella 912dimostrazione di teoremi non validi; il peggio che possono fare � risultare in 913goal irrisolvibili o nella dimostrazione di teoremi diversi da quelli che si aveva l'intenzione di dimostrare. Se $T$ fosse 914non valida e fosse usata per ridurre il goal $g$ ai subgoal $g_1$ , $\ldots$ 915, $g_n$, potrebbero essere spese energie per dimostrare i teoremi $th_1$ , $\ldots$ 916, $th_n$ per ottenere i subgoal $g_1$ , $\ldots$ , $g_n$, solo per 917poi scoprire che il lavoro fatto � un vicolo cieco perch� 918$p${\small\verb|[|}$th_1${\small\verb|,|}$\ldots${\small\verb|,|}$th_n${\small\verb|]|} 919non ottiene $g$ (cio� fallisce, oppure ottiene un altro 920goal). 921 922Un teorema {\it ottiene\/} un goal se le assunzioni del teorema sono 923incluse nelle assunzioni del goal {\it e\/} se la conclusione del 924teorema � uguale (a meno della rinomina delle variabili legate) alla conclusione del 925goal. Pi� precisamente, un teorema 926\begin{center} 927$t_1$, $\dots$, $t_m${\small\verb% |- %}$t$ 928\end{center} 929 930\noindent ottiene un goal 931\begin{center} 932{\small\verb|([|}$u_1${\small\verb|,|}$\ldots${\small\verb|,|}$u_n${\small\verb|],|}$u${\small\verb|)|} 933\end{center} 934 935\noindent se e solo se $\{t_1,\ldots,t_m\}$ 936� un sottoinsieme di $\{u_1,\ldots,u_n\}$ e $t$ � uguale a $u$ (a meno 937della rinomina delle variabili legate). Per esempio, il goal\linebreak 938{\small\verb|([``x=y``, ``y=z``, ``z=w``], ``x=z``)|} � ottenuto dal 939teorema {\small\verb+[x=y, y=z] |- x=z+}\linebreak (l'assunzione 940{\small\verb|``z=w``|} non � necessaria). 941 942Una tattica {\it risolve\/} un goal se esso riduce il goal 943alla lista vuota 944di subgoal. Cos� $T$ risolve $g$ se 945$T\ g${\small\verb| = ([],|}$p${\small\verb|)|}. 946Se questo � vero e se $T$ � valida, allora $p${\small\verb|[]|} 947sar� valutata a un teorema che ottiene $g$. 948Cos� se $T$ risolve $g$ allora l'espressione \ML{} 949{\small\verb|snd(|}$T\ g${\small\verb|)[]|} � valutata 950un teorema che ottiene $g$ 951 952Le tattiche sono specificate usando la seguente notazione: 953 954\begin{center} 955\begin{tabular}{c} \\ 956$goal$ \\ \tacticline 957$goal_1\ \ \ goal_2 \ \ \ \cdots\ \ \ goal_n$ \\ 958\end{tabular} 959\end{center} 960 961\noindent Per esempio, una tattica {\small\verb|CONJ_TAC|} � descritta da 962 963%\newcommand\ttbs{\texttt{\symbol{"5C}}} 964%\newcommand\ttland{\texttt{/\ttbs}} %this command must be put before the begin{document} to work with italian babel 965 966\begin{center} 967\begin{tabular}{lr} \\ 968\multicolumn{2}{c}{$t_1$ \ttland{} $t_2$} \\ \tacticline 969$t_1$ & $t_2$ \\ 970\end{tabular} 971\end{center} 972 973 974 975\noindent Cos� {\small\verb|CONJ_TAC|} riduce un goal della forma 976{\small\verb|(|}$\Gamma${\small\verb|,``|}$t_1${\small\verb|/\|}$t_2${\small\verb|``)|} 977ai subgoal 978{\small\verb|(|}$\Gamma${\small\verb|,``|}$t_1${\small\verb|``)|} e {\small\verb|(|}$\Gamma${\small\verb|,``|}$t_2${\small\verb|``)|}. 979Il fatto che le assunzioni del goal principale 980sono propagate senza modifica ai due subgoal � indicato dall'assenza 981delle assunzioni nella notazione. 982 983Un altro esempio � \ml{numLib.INDUCT_TAC},\footnote{Pi� avanti, scriveremo \ml{INDUCT_TAC} da solo, senza anteporre ad esso il prefisso \ml{numLib}. Per permettere questo dobbiamo immettere il comando \ml{open~numLib}.} la tattica per 984eseguire l'induzione matematica sui numeri naturali. 985 986\begin{center} 987\begin{tabular}{lr} \\ 988\multicolumn{2}{c}{\texttt{!}$n$\texttt{.}$t[n]$} \\ \tacticline 989$t[\texttt{0}]$ & $\quad\{t[n]\}\ t[\texttt{SUC}\;n]$ 990\end{tabular} 991\end{center} 992 993{\small\verb|INDUCT_TAC|} riduce un goal 994{\small\verb|(|}$\Gamma${\small\verb|,``!|}$n${\small\verb|.|}$t[n]${\small\verb|``)|} a un subgoal base 995{\small\verb|(|}$\Gamma${\small\verb|,``|}$t[${\small\verb|0|}$]${\small\verb|``)|} 996e a un subgoal passo d'induzione 997{\small\verb|(|}$\Gamma\cup\{${\small\verb|``|}$t[n]${\small\verb|``|}$\}${\small\verb|,``|}$t[${\small\verb|SUC |}$n]${\small\verb|``)|}. 998L'assunzione extra {\small\verb|``|}$t[n]${\small\verb|``|} 999� indicata nella notazione delle tattiche con le parentesi di insieme. 1000 1001\begin{session} 1002\begin{verbatim} 1003- numLib.INDUCT_TAC([], ``!m n. m+n = n+m``); 1004> val it = 1005 ([([], ``!n. 0 + n = n + 0``), 1006 ([``!n. m + n = n + m``], ``!n. SUC m + n = n + SUC m``)], fn) 1007 : (term list * term) list * (thm list -> thm) 1008\end{verbatim} 1009\end{session} 1010 1011\noindent Il primo subgoal � il caso base e il secondo subgoal � 1012il caso passo d'induzione. 1013 1014Le tattiche in genere falliscono (nel senso \ML{}, cio� sollevano un'eccezione) se 1015sono applicate a goal inappropriati. Per esempio, 1016{\small\verb|CONJ_TAC|} fallir� se � applicata a un goal la cui 1017conclusione non � una congiunzione. Alcune tattiche non falliscono mail, per esempio 1018{\small\verb|ALL_TAC|} 1019 1020 1021\begin{center} 1022\begin{tabular}{c} \\ 1023$t$ \\ \tacticline 1024$t$ 1025\end{tabular} 1026\end{center} 1027 1028\noindent � la `tattica identit�'; essa riduce un goal 1029{\small\verb|(|}$\Gamma${\small\verb|,|}$t${\small\verb|)|} all'unico 1030subgoal 1031{\small\verb|(|}$\Gamma${\small\verb|,|}$t${\small\verb|)|}---\ie\ non 1032ha alcun effetto. {\small\verb|ALL_TAC|} � utile per scrivere tattiche 1033complesse usando i tatticali. 1034 1035\subsection{Usare le tattiche per dimostrare teoremi} 1036\label{using-tactics} 1037 1038Supponiamo di dover risolvere il goal $g$. Se $g$ � semplice potrebbe essere 1039possibile pensare immediatamente a una tattica, diciamo $T$, che lo riduce 1040alla lista vuota di subgoal. Se questo � il caso allora eseguire: 1041 1042$\ ${\small\verb| val (|}$gl${\small\verb|,|}$p${\small\verb|) = |}$T\ g$ 1043 1044\noindent legher� $p$ a una funzione che quando applicata alla lista vuota 1045di teoremi restituisce un teorema $th$ che ottiene $g$. (La dichiarazione 1046di sopra legher� anche $gl$ alla lista vuota di goal.) Cos� un teorema 1047che ottiene $g$ pu� essere computato eseguendo: 1048 1049$\ ${\small\verb| val |}$th${\small\verb| = |}$p${\small\verb|[]|} 1050 1051\noindent Questo sar� illustrato usando \ml{REWRITE\_TAC} che prende una lista 1052di equazioni (vuota nell'esempio che segue) e prover� a dimostrare un goal 1053riscrivendo con queste equazioni insieme con 1054\ml{basic\_rewrites}: 1055 1056\begin{session} 1057\begin{verbatim} 1058- val goal2 = ([]:term list, ``T /\ x ==> x \/ (y /\ F)``); 1059> val goal2 = ([], ``T /\ x ==> x \/ y /\ F``) : (term list * term) 1060 1061- REWRITE_TAC [] goal2; 1062> val it = ([], fn) : (term list * term) list * (thm list -> thm) 1063 1064- #2 it []; 1065> val it = [] |- T /\ x ==> x \/ y /\ F : thm 1066\end{verbatim} 1067\end{session} 1068 1069\noindent I teoremi dimostrati sono di solito archiviati nella teoria attuale 1070cos� che possano essere usati nelle sessioni successive. 1071 1072La funzione incorporata 1073 \ml{store\_thm} di 1074tipo \ML{} {\small\verb|(string * term * tactic) -> thm|} facilita l'uso 1075delle tattiche: 1076{\small\verb|store_thm("foo",|}$t${\small\verb|,|}$T${\small\verb|)|} dimostra 1077il goal {\small\verb|([],|}$t${\small\verb|)|} (cio� il goal senza 1078assunzioni e con la conclusione $t$) usando la tattica $T$ e salva il teorema 1079risultante con il nome {\small\verb|foo|} nella teoria corrente. 1080 1081Se non si deve salvare il teorema, si pu� usare la funzione \ml{prove} di tipo\linebreak 1082{\small\verb|(term * tactic) -> thm|}. Valutare 1083{\small\verb|prove(|}$t${\small\verb|,|}$T${\small\verb|)|} dimostra il goal 1084{\small\verb|([],|}$t${\small\verb|)|} usando $T$ e restituisce il risultato senza 1085salvarlo. In entrambi i case, la valutazione fallisce se $T$ non risolve il 1086goal {\small\verb|([],|}$t${\small\verb|)|}. 1087 1088Quando si conduce una dimostrazione che coinvolge molti subgoal e tattiche, � necessario tenere traccia di tutte le funzioni di giustificazione e comporle nell'ordine corretto. 1089Nonostante questo sia fattibile anche per grandi dimostrazioni, � noioso. 1090\HOL{} fornisce un pacchetto per costruire e traversare l'albero dei subgoal, raccogliendo le funzioni di giustificazione e applicandole in modo appropriato; questo pacchetto fu inizialmente implementato per \LCF\ da Larry Paulson. 1091Il suo utilizzo � dimostrato di sotto in alcune delle sessioni di esempio, e nel Capitolo~\ref{chap:euclid}. 1092E' documentato in modo completo in \DESCRIPTION. 1093(In breve, la funzione \ML{} \ml{g} stabilisce un goal, e la funzione \ML{} \ml{e} applica una tattica allo stato corrente del goal.) 1094 1095\subsection{Tatticali} 1096\label{tacticals} 1097 1098Un {\it tatticale\/} � una funzione \ML{} che prende una o pi� tattiche 1099come argomenti, possibilmente con anche altri argomenti, e restituisce una 1100tattica come suo risultato. I diversi parametri passati ai tatticali sono 1101riflessi nei vari tipi \ML{} che hanno i tatticali incorporati nel sistema. 1102Alcuni tatticali importanti nel sistema \HOL{} sono elencati di sotto. 1103 1104\subsubsection{\tt THENL : tactic -> tactic list -> tactic} 1105 1106Se una tattica $T$ produce $n$ subgoal e $T_1$, $\ldots$ , $T_n$ sono tattiche allora \ml{$T$~THENL~[$T_1$,$\ldots$,$T_n$]} � una tattica che prima applica $T$ e poi applica $T_i$ all'$i$-esimo subgoal prodotto da $T$. 1107Il tatticale \ml{THENL} � utile se si vogliono fare cose differenti per subgoal differenti. 1108 1109\ml{THENL} pu� essere illustrata eseguendo la dimostrazione di $\vdash \uquant{m}m+0=m$ in 1110un solo passo. 1111 1112\setcounter{sessioncount}{0} 1113\begin{session} 1114\begin{verbatim} 1115- g `!m. m + 0 = m`; 1116> val it = 1117 Proof manager status: 1 proof. 1118 1. Incomplete: 1119 Initial goal: 1120 !m. m + 0 = m 1121 1122- e (INDUCT_TAC THENL [REWRITE_TAC[ADD], ASM_REWRITE_TAC[ADD]]); 1123OK.. 1124> val it = 1125 Initial goal proved. 1126 |- !m. m + 0 = m 1127\end{verbatim} 1128\end{session} 1129 1130\noindent La tattica composta \[ 1131\ml{INDUCT\_TAC~THENL~[REWRITE\_TAC~[ADD],~ASM\_REWRITE\_TAC~[ADD]]} 1132\] 1133prima applica \ml{INDUCT_TAC} e quindi applica \ml{REWRITE\_TAC[ADD]} al primo subgoal (la base) e \ml{ASM\_REWRITE\_TAC[ADD]} al secondo subgoal (il passo). 1134 1135Il tatticale {\small\verb|THENL|} � utile per fare cose differenti 1136per subgoal differenti. il tatticale \ml{THEN} pu� essere usato per applicare 1137la stessa tattica a tutti i subgoal. 1138 1139\subsubsection{\tt THEN : tactic -> tactic -> tactic}\label{THEN} 1140 1141Il tatticale {\small\verb|THEN|} � un \ML{} infisso. Se $T_1$ e $T_2$ 1142sono tattiche, allora l'espressione \ML{} $T_1${\small\verb| THEN |}$T_2$ 1143� valutata a una tattica che prima applica $T_1$ e poi applica $T_2$ 1144a tutti i subgoal prodotti da $T_1$. 1145 1146Di fatto, \ml{ASM\_REWRITE\_TAC[ADD]} risolver� tanto la base che 1147il passo dell'induzione per $\uquant{m}m+0=m$, cos� esiste una 1148dimostrazione di un solo passo persino pi� semplice di quella di sopra: 1149\setcounter{sessioncount}{0} 1150\begin{session} 1151\begin{verbatim} 1152- g `!m. m+0 = m`; 1153> val it = 1154 Proof manager status: 1 proof. 1155 1. Incomplete: 1156 Initial goal: 1157 !m. m + 0 = m 1158 1159- e(INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); 1160OK.. 1161> val it = 1162 Initial goal proved. 1163 |- !m. m + 0 = m 1164\end{verbatim} 1165\end{session} 1166 1167\noindent Questo � tipico: � comune usare un'unica tattica per molti 1168goal. Qui, per esempio, ci sono le prime quattro conseguenze della 1169definizione \ml{ADD} dell'addizione che sono pre-dimostrate quando la 1170teoria \ml{arithmetic} incorporata in \HOL{} � costruita. 1171 1172\begin{hol} 1173\begin{verbatim} 1174 val ADD_0 = prove ( 1175 ``!m. m + 0 = m``, 1176 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); 1177\end{verbatim} 1178\end{hol} 1179 1180\begin{hol} 1181\begin{verbatim} 1182 val ADD_SUC = prove ( 1183 ``!m n. SUC(m + n) = m + SUC n``, 1184 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]); 1185\end{verbatim} 1186\end{hol} 1187 1188\begin{hol} 1189\begin{verbatim} 1190 val ADD_CLAUSES = prove ( 1191 ``(0 + m = m) /\ 1192 (m + 0 = m) /\ 1193 (SUC m + n = SUC(m + n)) /\ 1194 (m + SUC n = SUC(m + n))``, 1195 REWRITE_TAC[ADD, ADD_0, ADD_SUC]); 1196\end{verbatim} 1197\end{hol} 1198 1199\begin{hol} 1200\begin{verbatim} 1201 val ADD_COMM = prove ( 1202 ``!m n. m + n = n + m``, 1203 INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_0, ADD, ADD_SUC]); 1204\end{verbatim} 1205\end{hol} 1206 1207 1208\noindent Queste dimostrazioni sono eseguite quando il sistema \HOL{} � costruito e i 1209teoremi sono salvati nella teoria \ml{arithmetic}. La lista completa delle 1210dimostrazioni per questa teoria incorporata si possono trovare nel file 1211\ml{src/num/theories/arithmeticScript.sml}. 1212 1213 1214\subsubsection{\tt ORELSE : tactic -> tactic -> tactic}\label{ORELSE} 1215 1216Il tatticale {\small\verb|ORELSE|} � un \ML{} infisso. Se $T_1$ e 1217$T_2$ sono tattiche, 1218%\index{tacticals!for alternation} 1219allora $T_1${\small\verb| ORELSE |}$T_2$ � valutata a una tattica che 1220applica $T_1$ a meno che fallisce; se fallisce, applica $T_2$. 1221\ml{ORELSE} � definita in \ML{} come un infisso curried\footnote{Questa � 1222 una semplificazione minore.} 1223 1224\begin{hol} 1225 {\small\verb|(|}$T_1${\small\verb| ORELSE |}$T_2${\small\verb|)|} $g$ 1226 {\small\verb|=|} $T_1\; g$ {\small\verb|handle _ =>|} $T_2\; g$ 1227\end{hol} 1228%\index{alternation!of tactics|)} 1229 1230\subsubsection{\tt REPEAT : tactic -> tactic} 1231 1232Se $T$ � una tattica allora {\small\verb|REPEAT |}$T$ � una tattiche che 1233applica ripetutamente $T$ fino a quando fallisce. Questo pu� essere illustrato in 1234congiunzione con \ml{GEN\_TAC}, che � specificato da: 1235 1236\begin{center} 1237\begin{tabular}{c} \\ 1238{\small\verb|!|}$x${\small\verb|.|}$t[x]$ 1239\\ \tacticline 1240$t[x']$ 1241\\ 1242\end{tabular} 1243\end{center} 1244 1245\begin{itemize} 1246\item Dove $x'$ � una variante di $x$ 1247non libera nel goal o nelle assunzioni. 1248\end{itemize} 1249 1250\noindent \ml{GEN\_TAC} toglie un quantificatore; 1251\ml{REPEAT\ GEN\_TAC} toglie tutti i quantificatori: 1252 1253\begin{session} 1254\begin{verbatim} 1255- g `!x y z. x+(y+z) = (x+y)+z`; 1256> val it = 1257 Proof manager status: 1 proof. 1258 1. Incomplete: 1259 Initial goal: 1260 !x y z. x + (y + z) = x + y + z 1261 1262- e GEN_TAC; 1263OK.. 12641 subgoal: 1265> val it = 1266 !y z. x + (y + z) = x + y + z 1267 1268- e (REPEAT GEN_TAC); 1269OK.. 12701 subgoal: 1271> val it = 1272 x + (y + z) = x + y + z 1273\end{verbatim} 1274\end{session} 1275 1276\subsection{Alcune tattiche incorporate in \HOL{}} 1277 1278Questa sezione contiene un sommario di alcune tattiche incorporate nel 1279sistema \HOL{} (incluse quelle gi� discusse). Le tattiche date 1280qui sono quelle che sono usate nell'esempio del bit di parit�. 1281 1282\subsubsection{\tt REWRITE\_TAC : thm list -> tactic} 1283\label{rewrite} 1284 1285\begin{itemize} 1286\item{\bf Sommario:} {\small\verb|REWRITE_TAC[|}$th_1${\small\verb|,|}$\ldots${\small\verb|,|}$th_n${\small\verb|]|} 1287semplifica il goal riscrivendolo 1288con i teoremi dati esplicitamente $th_1$, $\ldots$ , $th_n$, 1289e varie regole di riscrittura incorporate. 1290 1291 1292\begin{center} 1293\begin{tabular}{c} \\ 1294$\{t_1, \ldots , t_m\}t$ 1295\\ \tacticline 1296$\{t_1, \ldots , t_m\}t'$ 1297\\ 1298\end{tabular} 1299\end{center} 1300 1301\noindent dove $t'$ � ottenuto da $t$ attraverso la riscrittura con 1302\begin{enumerate} 1303\item $th_1$, $\ldots$ , $th_n$ e 1304\item le scritture standard contenute nella variabile \ML{} {\small\verb|basic_rewrites|}. 1305\end{enumerate} 1306 1307\item{\bf Usi:} Semplificare goal usando teoremi precedentemente dimostrati. 1308 1309\item{\bf Altre tattiche di riscrittura}: 1310\begin{enumerate} 1311\item {\small\verb|ASM_REWRITE_TAC|} aggiunge le assunzioni del goal 1312 alla lista dei teoremi usati per la riscrittura. 1313\item {\small\verb|PURE_REWRITE_TAC|} non usa n� le assunzioni 1314 n� le riscritture incorporate. 1315\item {\small\verb|RW_TAC|} di tipo \ml{simpLib.simpset -> thm 1316 list -> tactic}. Un \ml{simpset} � una speciale collezione 1317 di teoremi di riscrittura e altre funzionalit� di dimostrazione di teoremi. I valori 1318 definiti da \HOL{} includono \ml{bossLib.std\_ss}, che ha la conoscenza 1319 di base dei connettivi booleani, \ml{bossLib.arith\_ss} che 1320 ``conosce'' tutto riguardo all'aritmetica, e \ml{HOLSimps.list\_ss}, che 1321 include teoremi appropriati per le liste, le coppie, e l'aritmetica. 1322 Teoremi aggiuntivi per la riscrittura possono essere aggiunti usando il secondo 1323 argomento di \ml{RW\_TAC}. 1324\end{enumerate} 1325\end{itemize} 1326 1327 1328\subsubsection{\tt CONJ\_TAC : tactic}\label{CONJTAC} 1329 1330\begin{itemize} 1331 1332\item{\bf Sommario:} Divide un 1333goal {\small\verb|``|}$t_1${\small\verb|/\|}$t_2${\small\verb|``|} in due subgoals {\small\verb|``|}$t_1${\small\verb|``|} 1334e {\small\verb|``|}$t_2${\small\verb|``|}. 1335 1336\begin{center} 1337\begin{tabular}{lr} \\ 1338\multicolumn{2}{c}{$t_1$ \ttland{} $t_2$} \\ \tacticline 1339$t_1$ & $t_2$ \\ 1340\end{tabular} 1341\end{center} 1342 1343\item{\bf Usi:} Risolvere goal congiuntivi. 1344\ml{CONJ_TAC} � invocata da \ml{STRIP_TAC} (si veda di sotto). 1345 1346\end{itemize} 1347 1348\subsubsection{\tt EQ\_TAC : tactic}\label{EQTAC} 1349 1350 1351\begin{itemize} 1352 1353\item{\bf Sommario:} 1354\ml{EQ_TAC} divide un goal equazionale in due implicazioni (il `caso-se' e il caso `solo-se'): 1355 1356\begin{center} 1357 1358 1359\begin{tabular}{lr} \\ 1360\multicolumn{2}{c}{$u\; \ml{=}\; v$} \\ \tacticline 1361$u\; \ml{==>}\; v$ & $\quad v\; \ml{==>}\; u$ \\ 1362\end{tabular} 1363\end{center} 1364 1365\item{\bf Uso:} Dimostrare equivalenze logiche, \ie\ goal della forma 1366``$u$\ml{=}$v$'' dove $u$ e $v$ sono termini booleani. 1367 1368\end{itemize} 1369 1370 1371 1372 1373\subsubsection{\tt DISCH\_TAC : tactic}\label{DISCHTAC} 1374 1375\begin{itemize} 1376 1377\item{\bf Sommario:} Sposta l'antecedente 1378di un goal implicazione nelle assunzioni 1379 1380\begin{center} 1381\begin{tabular}{c} \\ 1382$u${\small\verb| ==> |}$v$ 1383\\ \tacticline 1384$\{u\}v$ 1385\\ 1386\end{tabular} 1387\end{center} 1388 1389 1390\item{\bf Usi:} Risolve goal della forma \holtxt{$u$~==>~$v$} assumendo \holtxt{$u$} e poi risolvendo \holtxt{$v$}. 1391{\small\verb|STRIP_TAC|} (si veda sotto) invocher� {\small\verb|DISCH_TAC|} su goal con la forma di implicazioni. 1392\end{itemize} 1393 1394\subsubsection{\tt GEN\_TAC : tactic} 1395 1396\begin{itemize} 1397 1398\item{\bf Sommario:} Elimina un quantificatore universale. 1399 1400 1401\begin{center} 1402\begin{tabular}{c} \\ 1403{\small\verb|!|}$x${\small\verb|.|}$t[x]$ 1404\\ \tacticline 1405$t[x']$ 1406\\ 1407\end{tabular} 1408\end{center} 1409 1410\noindent Dove $x'$ � una variante di $x$ 1411non libera nel goal o nelle assunzioni. 1412 1413\item{\bf Usi:} Risolvere goal quantificati universalmente. 1414{\small\verb|REPEAT GEN_TAC|} elimina tutti 1415i quantificatori universali ed � spesso la prima cosa che si fa in una dimostrazione. 1416{\small\verb|STRIP_TAC|} (si veda di sotto) applica {\small\verb|GEN_TAC|} ai goal quantificati universalmente. 1417\end{itemize} 1418 1419 1420\subsubsection{\tt PROVE\_TAC : thm list -> tactic} 1421 1422\begin{itemize} 1423\item {\bf Sommario:} Usato per eseguire un ragionamento al primo ordine; risolvendo il 1424 goal completamente se ha successo, e fallendo altrimenti. Usando 1425 i teoremi forniti e le assunzioni del goal, 1426 {\small\verb|PROVE_TAC|} esegue una ricerca delle dimostrazioni possibili del 1427 goal. Alla fine fallisce se la ricerca fallisce di trovare una dimostrazione pi� corta 1428 di una profondit� ragionevole. 1429\item {\bf Usi:} Per concludere un goal quando � chiaro che � una 1430 conseguenza delle assunzioni e dei teoremi forniti. 1431\end{itemize} 1432 1433 1434\subsubsection{\tt STRIP\_TAC : tactic} 1435 1436\begin{itemize} 1437 1438\item{\bf Sommario:} Spezza un goal. {\small\verb|STRIP_TAC|} 1439 rimuove un connettivo esterno dal goal, usando 1440 {\small\verb|CONJ_TAC|}, {\small\verb|DISCH_TAC|}, 1441 {\small\verb|GEN_TAC|}, \etc\ Se il goal � 1442$t_1${\small\verb|/\|}$\cdots${\small\verb|/\|}$t_n${\small\verb| ==> |}$t$ 1443allora {\small\verb|STRIP_TAC|} rende ogni $t_i$ in una assunzione separata. 1444 1445\item{\bf Usi:} utile per dividere un goal in pezzi maneggevoli. 1446Spesso la cosa migliore da fare per prima � {\small\verb|REPEAT STRIP_TAC|}. 1447\end{itemize} 1448 1449 1450\subsubsection{\tt ACCEPT\_TAC : thm -> tactic}\label{ACCEPTTAC} 1451 1452 1453\begin{itemize} 1454 1455\item{\bf Sommario:} {\small\verb|ACCEPT_TAC |}$th$ 1456� una tattica che risolve qualsiasi goal che sia 1457ottenuto da $th$. 1458 1459\item{\bf Uso:} Incorporare dimostrazioni in avanti, o teoremi gi� 1460 dimostrati, in dimostrazioni dirette dal goal. Per esempio, si potrebbe ridurre un 1461 goal $g$ ai subgoal $g_1$, $\dots$, $g_n$ usando una tattica $T$ e 1462 poi dimostrare i teoremi $th_1$ , $\dots$, $th_n$ ottenendo rispettivamente 1463 questi goal attraverso dimostrazioni in avanti. La tattica 1464 1465\[\ml{ T THENL[ACCEPT\_TAC }th_1\ml{,}\ldots\ml{,ACCEPT\_TAC }th_n\ml{]} 1466\] 1467 1468risolverebbe poi $g$, dove \ml{THENL} 1469%\index{THENL@\ml{THENL}} 1470� il tatticale che applica gli elementi rispettivi della lista di 1471tattiche ai subgoal prodotti da \ml{T}. 1472 1473\end{itemize} 1474 1475 1476 1477\subsubsection{\tt ALL\_TAC : tactic} 1478 1479\begin{itemize} 1480\item{\bf Sommario:} Identifica la tattica per il tatticale {\small\verb%THEN%} 1481(si veda \DESCRIPTION). 1482 1483\item{\bf Usi:} 1484\begin{enumerate} 1485\item Scrivere tatticali (si veda la descrizione di {\small\verb|REPEAT|} 1486in \DESCRIPTION). 1487\item Con {\small\verb|THENL|}; per esempio, se la tattica $T$ produce due subgoal 1488e vogliamo applicare $T_1$ 1489al primo ma non fare nulla al secondo, quindi 1490la tattica da usare � \ml{$T$~THENL[$T_1$,ALL_TAC]}. 1491\end{enumerate} 1492\end{itemize} 1493 1494\subsubsection{\tt NO\_TAC : tactic} 1495 1496\begin{itemize} 1497\item{\bf Sommario:} Tattica che fallisce sempre. 1498 1499\item{\bf Usi:} Scrivere tatticali. 1500\end{itemize} 1501 1502%%% Local Variables: 1503%%% mode: latex 1504%%% TeX-master: "tutorial" 1505%%% End: 1506