IT/Description/theories.tex

39 In questa teoria sono dichiarate la costante di tipo {\small\verb+bool+} dei booleani,
40 l'operatore di tipo binario $(\alpha,\beta)${\small\verb+fun+} delle funzioni, e la costante
41 di tipo {\small\verb+ind+} degli individui. Sulla base di
50 \item [Eguaglianza] ({\small\verb+= : 'a -> 'a -> bool+}) � un
54   ({\small\verb+==> : bool -> bool -> bool+}) � l'
56   associativo a destra, cio�, \verb+x ==> y ==> z+ � parsato allo stesso termine
57   di \verb+x ==> (y ==> z)+.
61 pi� esotica: se $t$ � un termine che ha il tipo $\sigma${\small\verb+->bool+},
62 allora {\small\verb+@x.+}$t${\small\verb+ x+} (o, equivalentemente,
63 {\small\verb+$@+}$t$) denota \emph{qualche} membro dell'insieme la cui
66 {\small\verb+@x.+}$t${\small\verb+ x+} denota un membro arbitrario
67 dell'insieme denotato da $\sigma$. La costante {\small\verb+@+} � una versione
240 propriet� di funzione {\small\verb+ONE_ONE+} e {\small\verb+ONTO+}. Le
376 quantificazione ristretta con il simbolo {\small\verb+::+}, che si riferisce
474 Negazione & {\small\verb+~+}$t$ & {\small\verb+$~ +}$t$ & {\small\verb+mk_neg(+}$t${\small\verb+)+} \\ \hline
475 Disgiunzione & $t_1${\small\verb+\/+}$t_2$ & {\small\verb+$\/ +}$t_1\ t_2$ &
476 {\small\verb+mk_disj(+}$t_1${\small\verb+,+}$t_2${\small\verb+)+} \\ \hline
479 {\small\verb+mk_conj(+}$t_1${\small\verb+,+}$t_2${\small\verb+)+} \\
482 Implicazione & $t_1${\small\verb+==>+}$t_2$ & {\small\verb+$==> +}$t_1\ t_2$ &
483 {\small\verb+mk_imp(+}$t_1${\small\verb+,+}$t_2${\small\verb+)+} \\ \hline
485 Eguaglianza & $t_1${\small\verb+=+}$t_2$ & {\small\verb+$= +}$t_1\ t_2$ &
486 {\small\verb+mk_eq(+}$t_1${\small\verb+,+}$t_2${\small\verb+)+} \\ \hline
488 Quantificazione-$\forall$ & {\small\verb+!+}$x${\small\verb+.+}$t$ &
489 \holtxt{\$!(\bs}$x${\small\verb+.+}$t${\small\verb+)+} & {\small\verb+mk_forall(+}$x${\small\verb+,+}$t${\small\verb+)+} \\ \hline
491 Quantificazione-$\exists$ & {\small\verb+?+}$x${\small\verb+.+}$t$ &
492 \holtxt{\$?(\bs}$x${\small\verb+.+}$t${\small\verb+)+} & {\small\verb+mk_exists(+}$x${\small\verb+,+}$t${\small\verb+)+} \\ \hline
494 Termine-$\hilbert$ & {\small\verb+@+}$x${\small\verb+.+}$t$ &
495 \holtxt{\$@(\bs}$x${\small\verb+.+}$t${\small\verb+)+} & {\small\verb+mk_select(+}$x${\small\verb+,+}$t${\small\verb+)+} \\ \hline
497 Condizionale & {\small\verb+if +}$t\ ${\small\verb+then +}$t_1${\small\verb+ else +}$t_2$ &
498 {\small\verb+COND +}$t\ t_1\ t_2$ & {\small\verb+mk_cond(+}$t${\small\verb+,+}$t_1${\small\verb+,+}$t_2${\small\verb+)+}
501 Espressione-{\small\verb+let+} & {\small\verb+let +}$x${\small\verb+=+}$t_1${\small\verb+ in +}$t_2$ &
502 \holtxt{LET(\bs}$x${\small\verb+.+}$t_2${\small\verb+)+}$t_1$ &
534 \HOL{} tradurr� $t_1\ c\ t_2$ in {\small\verb+$+}$c\ t_1\ t_2$.
536 Le costanti {\small\verb+!+}, {\small\verb+?+} e {\small\verb+@+}
566 {\small\verb+(+}$\cdots${\small\verb+(+}$t\ t_1${\small\verb+)+}$\cdots t_n${\small\verb+)+} &
567 {\small\verb+list_mk_comb(+}$t${\small\verb+,[+}$t_1${\small\verb+, +}$\ldots${\small\verb+ ,+}$t_n${\small\verb+])+} \\ \hline
568 \holtxt{\bs}$x_1\cdots x_n${\small\verb+.+}$t$ &
569 \holtxt{\bs}$x_1${\small\verb+. +}$\cdots$\holtxt{ \bs}$x_n${\small\verb+.+}$t$ &
570 {\small\verb+list_mk_abs([+}$x_1${\small\verb+, +}$\ldots${\small\verb+ ,+}$x_n${\small\verb+],+}$t${\small\verb+)+}
572 {\small\verb+!+}$x_1\cdots x_n${\small\verb+.+}$t$ &
573 {\small\verb+!+}$x_1${\small\verb+. +}$\cdots${\small\verb+ !+}$x_n${\small\verb+.+}$t$ &
574 {\small\verb+list_mk_forall([+}$x_1${\small\verb+, +}$\ldots${\small\verb+ ,+}$x_n${\small\verb+],+}$t${\small\verb+)+}
576 {\small\verb+?+}$x_1\cdots x_n${\small\verb+.+}$t$ &
577 {\small\verb+?+}$x_1${\small\verb+. +}$\cdots${\small\verb+ ?+}$x_n${\small\verb+.+}$t$ &
578 {\small\verb+list_mk_exists([+}$x_1${\small\verb+, +}$\ldots${\small\verb+ ,+}$x_n${\small\verb+],+}$t${\small\verb+)+} \\
634 ({\small\verb+SKOLEM_THM+}). Nella teoria \theoryimp{bool} si possono trovare molti altri teoremi.
784 {\small\verb%(%}$t_1${\small\verb%,%}$t_2${\small\verb%)%}
794 $\sigma_1${\small\verb%#%}$\sigma_2$ � cos�
795 $\sigma_1${\small\verb%->%}$\sigma_2${\small\verb%->bool%}.
806 L'operatore di tipo {\small\verb%prod%} � definito invocando \ml{new\_type\_definition}\index{new_type_definition@\ml{new\_type\_definition}} con questo teorema che risulta nell'asserazione nella teoria \ml{pair} dell'assioma definizionale \index{assiomi!non-primitivi, della logica HOL@non-primitivi, della logica \HOL{}!per prodotti} \index{assiomi!nella teoria bool@nella teoria \ml{bool}} \ml{prod\_TY\_DEF} mostrato di sotto.
829 Il costruttore infisso `{\small\verb%,%}' � poi definito
831 dimostrati due teoremi cruciali: {\small\verb+PAIR_EQ+} afferma che coppie
832 uguali hanno componenti uguali e {\small\verb+ABS_PAIR_THM+} mostra che
848 Skolemizzando {\small\verb+ABS_PAIR_THM+} e facendo le specifiche di costante
849 per {\small\verb+FST+} e {\small\verb+SND+}, sono dimostrati i
890 applicate in modo componente ({\small\verb+##+}, infisso) su una coppia di tipo
926 delle relazioni ({\small\verb+LEX+}, infisso) pu� essere definita usando
955 {\small\bs\texttt{(}}$x_1${\small\verb%,%}$x_2${\small\verb%).%}$t$
956 in {\small\verb%UNCURRY(%\bs}$x_1\ x_2${\small\verb%.%}$t${\small\verb%)%}.
1253 La teoria \theoryimp{option} definisce un operatore di tipo \verb+option+
1291 La costante sottostante a questo addolcimento sintattico � \verb+option_case+
1441 Questa definizione dice che {\small\verb%m < n%} se esiste un insieme (con
1442 funzione caratteristica {\small\verb%P%}) che � chiuso
1445 contiene {\small\verb%m%} ma non {\small\verb%n%}.
1481 \ml{num\_Axiom} mostrato di sopra. La specializzazione delle variabili quantificate \verb!x!
1482 e \verb!f! con un'adeguata istanziazione dei tipi di \ml{num\_Axiom} cos�
1555 \theoryimp{prim\_rec} dimostra l'Assioma di Scelta Dipendente ({\small\verb+DC+}).
1568 La dimostrazione usa {\small\verb+SELECT_AX+}. Il teorema {\small\verb+DC+}
1584 Per mezzo dell'uso di {\small\verb+DC+}, questo enunciato pu� essere dimostrato
1585 essere uguale alla nozione di benfondatezza {\small\verb+WF+}
1644 Un completo insieme di operatori di confronto � definito in termini di \verb+<+.
1659 Per introdurre gli operatori divisione ({\small\verb+DIV+}, infisso) e
1660 modulo ({\small\verb+MOD+}, infisso) � usata una specifica di costante, insieme con le loro
1786 \theoryimp{numeral}; questi sono meccanizzati dalla libreria \verb+reduce+. Cos�,
1809 \ml{Arbnum} che implementa numeri di precisione arbitraria {\verb+num+}. La
1811 tipo \verb+num+ e come i numerali sono de-costruiti. La structure
1812 {\small\verb+Arbnum+} fornisce una collezione completa di operazioni
1813 aritmetiche, che usano i nomi usuali per le operazioni, ad esempio \verb|+|,
1814 \verb|*|, \verb|-|, ecc.
1902 gli interi), i numerali sono sottoposti all'overloading cos� che il numerale {\small\verb+1+} pu�
1907 numerale \verb+2+ � considerato essere un intero.
1936 Un letterale numerico per un tipo \HOL{} diverso da \verb+num+, come
1937 \verb+42i+, � rappresentato dall'applicazione di una funzione
1938 d'\emph{iniezione} di tipo {\small\verb+num -> ty+} per un
1940 {\small\verb+ty+}. Si veda la Sezione \ref{integers} per un'ulteriore discussione.
1942 Le funzioni {\verb+mk_numeral+}, {\verb+dest_numeral+}, e
1943 {\verb+is_numeral+} funzionano solo per numerali, e per letterali
1944 numerici con suffissi di un carattere diverso da {\small\verb+n+}. Per
1963 {\small\verb+int_ge+} &{\small\verb+>=+} & 450 & nessuna \\
1964 {\small\verb+int_le+} &{\small\verb+<=+} & 450 & nessuna \\
1965 {\small\verb+int_gt+} &{\small\verb+>+}  & 450 & nessuna \\
1966 {\small\verb+int_lt+} &{\small\verb+<+}  & 450 & nessuna \\
1967 {\small\verb+int_add+} &{\small\verb%+%} & 500 & sinistra \\
1968 {\small\verb+int_sub+} &{\small\verb%-%} & 500 & sinistra \\
1969 {\small\verb+int_neg+} &{\small\verb%~%} & 900 & vero prefisso \\
1970 {\small\verb+int_mul+} &{\small\verb%*%} & 600 & sinistra \\
1971 {\small\verb%/%} & & 600 & sinistra \\
1972 {\small\verb+%+} & & 650 & sinistra \\
1973 {\small\verb+int_exp+} &{\small\verb%**%} & 700 & destra \\
1974 {\small\verb+int_of_num+} &{\small\verb%&%} & & prefisso \\
1978 Il simbolo sottoposto a overload {\small\verb+& : num -> int+} denota la
2010 dal simbolo sottoposto a overload {\small\verb+& : num -> rat+} e dal
2011 suffisso {\small\verb+q+}.
2018 {\small\verb+rat_geq+} &{\small\verb+>=+} & 450 & nessuna \\
2019 {\small\verb+rat_leq+} &{\small\verb+<=+} & 450 & nessuna \\
2020 {\small\verb+rat_gre+} &{\small\verb+>+}  & 450 & nessuna \\
2021 {\small\verb+rat_les+} &{\small\verb+<+}  & 450 & nessuna \\
2022 {\small\verb+rat_add+} &{\small\verb%+%} & 500 & sinistra \\
2023 {\small\verb+rat_sub+} &{\small\verb%-%} & 500 & sinistra \\
2024 {\small\verb+rat_ainv+} &{\small\verb%~%} & 900 & vero prefisso \\
2025 {\small\verb+rat_minv+} & & & \\
2026 {\small\verb+rat_mul+} &{\small\verb%*%} & 600 & sinistra \\
2027 {\small\verb+rat_div+} &{\small\verb%/%} & 600 & sinistra \\
2028 {\small\verb+rat_of_num+} &{\small\verb%&%} & & \\
2051 � registrata in {\small\verb+hratTheory+} e
2052 {\small\verb+hrealTheory+}, ma non � usata una volta che i reali sono stati
2054 {\small\verb+realaxTheory+}. Una collezione standard di operatori sui
2055 reali, e di teoremi che li riguardano, si trova in {\small\verb+realaxTheory+}
2056 and {\small\verb+realTheory+}. Gli operatori e il loro status di parsing sono
2063 {\small\verb+real_ge+} &{\small\verb+>=+} & 450 & nessuna \\
2064 {\small\verb+real_lte+} &{\small\verb+<=+} & 450 & nessuna \\
2065 {\small\verb+real_gt+} &{\small\verb+>+}  & 450 & nessuna \\
2066 {\small\verb+real_lt+} &{\small\verb+<+}  & 450 & nessuna \\
2067 {\small\verb+real_add+} &{\small\verb%+%} & 500 & sinistra \\
2068 {\small\verb+real_sub+} &{\small\verb%-%} & 500 & sinistra \\
2069 {\small\verb+real_neg+} &{\small\verb%~%} & 900 & trueprefix \\
2070 {\small\verb+real_mul+} &{\small\verb%*%} & 600 & sinistra \\
2071 {\small\verb+real_div+} & {\small\verb%/%} & 600 & sinistra \\
2072 {\small\verb+pow+} & &700 & right \\
2073 {\small\verb+real_of_num+} &{\small\verb%&%} & & prefisso \\
2077 Sulla base di {\small\verb+realTheory+}, � costruita la seguente sequenza di
2528 liste. I costruttori primitivi {\small\verb+NIL+} e {\small\verb+CONS+}
2601 Il teorema {\small\verb+CONS_11+}  mostra che {\small\verb+CONS+} � iniettiva;
2602 i teoremi {\small\verb+NOT_NIL_CONS+} e {\small\verb+NOT_CONS_NIL+} mostrano che
2603 {\small\verb+NIL+} e {\small\verb+CONS+} sono distinte, cio�,
2669 La concatenazione binaria di liste ({\small\verb+APPEND+}) pu� anche essere denotata
2670 dall'operatore infisso {\small\verb|++|}; cos� l'espressione
2671 {\small\verb|L1 ++ L2|} � tradotta in {\small\verb+APPEND L1 L2+}.
2673 {\small\verb+FLAT+}.
2828 l'operazione {\small\verb+ZIP+}. Il risultato non � specificato
2830 {\small\verb+UNZIP+}, traduce una lista di coppie in una coppia di
3294 definite due costanti: {\small\verb+CHR +}$: \konst{num}\to\konst{char}$ e
3295 {\small\verb+ORD +}$: \konst{char}\to\konst{num}$. Valgono i seguenti
3375 C'� anche una funzione de-costruttore {\small\verb+DEST_STRING+} per
3498 L'inserimento ({\small\verb+INSERT+}, scritto infisso) di un elemento
3500 discussa nella sottosezione successiva. Le definizioni usuali per l'unione insiemistica ({\small\verb+UNION+},
3501 scritto infisso) e l'intersezione ({\small\verb+INTER+}, anch'esso infisso)
3644 Il prodotto di due insiemi ({\small\verb+CROSS+}, infisso) � definito
3666 un altro teorema per giustificare un fold ({\small\verb+ITSET+}) per insiemi finiti.
3689 Per la completa derivazione, si vedano i sorgenti di {\small\verb+pred_set+}.
3690 La definizione di {\small\verb+ITSET+} permette, per esempio, la
3741 {\small\verb%{%}$t_1 ;t_2 ; \ldots ; t_n${\small\verb%}%} e
3742 {\small\verb%{%}$t${\small\verb% | %}$p${\small\verb%}%} sono riconosciute
3761 {\small\verb%{%}$t${\small\verb% | %}$p${\small\verb%}%} �
3820 La variabile quantificata esistenzialmente \verb+x+ ha un tipo coppia,
3821 cos� che pu� essere sostituita da una coppia \verb+(p,q)+ e
3915 \noindent La sintassi speciale {\verb+{||}+} pu� essere usata per rappresentare il multinsieme
3922 in a bag ({\small\verb+BAG_INN+}); and does an element occur in a bag
3923 at all ({\small\verb+BAG_IN+}).
3974 {\small\verb%{|%}$t_1 ;t_2 ; \ldots ; t_n${\small\verb%|}%}, dove
3977 \verb+{|1; 2; 3; 2; 1|}+ � analizzato dal parser a
4283 Si noti che {\small\verb+RTC_RULES+}, in linea con la definizione
4284 di {\small\verb+RTC+}, estende un \verb+R+-passo da \verb+x+ a
4285 \verb+y+ con una sequenza di \verb+R+-passi da \verb+y+ a \verb+z+
4286 per costruire \verb+RTC x z+. Il teorema
4287 {\small\verb+RTC_RULES_RIGHT1+} prima fa una serie di \verb+R+
4288 passi e poi un singolo \verb+R+ passo per formare \verb+RTC x z+. Analoghi
4291 Per esempio, {\small\verb+TC_CASES1+} e {\small\verb+TC_CASES2+} in ci� che
4292 segue de-compongono {\small\verb+RTC R x z+} o a
4293 {\small\verb+R x y+} seguito da {\small\verb+RTC R y z+}
4294 ({\small\verb+TC_CASES1+})
4296 {\small\verb+RTC R x y+} seguito da {\small\verb+R y z+}
4297 ({\small\verb+TC_CASES2+}).
4316 Esattamente come i teoremi d'induzione di base per {\small\verb+TC+} e
4317 {\small\verb+RTC+}, ci sono i cosiddetti teoremi d'induzione
4347 ({\small\verb+EQC+}) � la chiusura simmetrica poi transitiva poi riflessiva
4360 Una relazione $R$ � benfondata ({\small\verb+WF+}) se ogni insieme non-vuoto
4362 principio d'induzione benfondata ({\small\verb+WF_INDUCTION_THM+}).
4373 La \emph{parte benfondata} ({\small\verb+WFP+}) di una relazione pu� essere
4404 I teoremi di ricorsione {\small\verb+WFREC_COROLLARY+} e
4405 {\small\verb+WF_RECURSION_THM+} usano la nozione di una restrizione
4406 di funzione ({\small\verb+RESTRICT+}) al fine di forzare l'applicazione della funzione
4422 \noindent I teoremi {\small\verb+WF_INDUCTION_THM+} e
4423 {\small\verb+WFREC_COROLLARY+} sono usati per automatizzare le definizioni
4442 (la propriet� diamante (\verb+diamond+), la propriet�
4443 Church-Rosser ({\small\verb+CR+} e {\small\verb+WCR+}), e la Normalizzazione
4444 Forte ({\small\verb+SN+})) appaiono
4476 $\beta$ e il resto mappano a \verb+one+. la sintassi
4496 l'applicazione della mappa finita \verb+f+ to argument \verb+x+, cio�, come
4499 \verb+f+ per mezzo della coppia \verb+(x,y)+.
4502 propriet� pi� utili. {\small\verb+FAPPLY_FUPDATE_THM+} collega
4503 l'aggiornamento di una mappa con l'applicazione di una mappa. {\small\verb+fmap_EXT+} � un
4507 ({\small\verb+fmap_INDUCT+}). La cardinalit� di una mappa finita �
4508 semplicemente la cardinalit� del suo dominio ({\small\verb+FCARD_DEF+}); da
4510 ({\small\verb+FCARD_FUPDATE+}).
4543 ({\small\verb+FDOM_FUPDATE+}). Il rango di una mappa � definito nel
4554 Una mappa finita pu� avere il suo dominio ({\small\verb+DRESTRICT+})
4555 o rango ({\small\verb+RRESTRICT+}) ristretti per intersezione con un
4557 ({\small\verb+DRESTRICT_FUPDATE+} e {\small\verb+RRESTRICT_FUPDATE+}).
4643 mappe finite (\verb+f_o_f+, infisso) ha attaccati dei vincoli
4645 (\verb+o_f+, infisso) applica prima la mappa finita, poi la funzione
4647 (\verb+f_o+, infisso) applica la funzione ordinaria e poi la mappa
4705 per \verb+f+ nella dimostrazione del seguente teorema:
4721 che ne limitano la sua applicazione. Al fine di applicare \verb+WHILE_INDUCTION+,
4722 le istanziazione per \verb+B+ e \verb+C+ devono essere conosciute prima
4723 che una relazione benfondata per \verb+R+ sia trovata e usata per eliminare i
4752 \verb+P+.