Lines Matching defs:con
5 \newcommand{\KC}{\con{K}}
6 \newcommand{\SC}{\con{S}}
73 $\con{K}\;x\;y$ dovrebbe essere letto come $\con{K}\;\#\;x\;\#\;y$ che � a sua
74 volta $(\con{K}\;\#\;x)\;\#\;y$.
83 In HOL, possiamo catturare questa relazione con una definizione induttiva.
94 di scrivere questo e averlo con il significato di \verb!x --> y /\ y --> z!, ma questo al
95 momento non � possibile con il parser di HOL.
97 Il nostro prossimo passo � di definire di fatto la relazione con la
174 Cos�, iniziamo la nostra digressione astratta con un'altra definizione
175 induttiva. La nostra nuova costante � \con{RTC}, tale che
176 $\con{RTC}\;R\;x\;y$ � vera se � possibile andare da $x$ a $y$
177 con zero o pi� ``passi'' della relazione $R$. (La notazione
178 standard per $\con{RTC}\;R$ � $R^*$.) Possiamo esprimere quest'idea con
179 solo due regole. La prima \[ \infer{\con{RTC}\;R\;x\;x}{} \] dice
182 \infer{\con{RTC}\;R\;x\;z}{R\;x\;y\qquad\con{RTC}\;R\;y\;z}
188 (Come accade, \con{RTC} � una costante gi� definita nel conteso
234 allora possiamo completare con un nuovo valore $u$:
323 concludere con
341 dimostrare e salvare il teorema per l'uso futuro con:
382 $\con{RTC}\;R$? La risposta che salta alla mente � di sperare che se
385 \[ \con{diamond}\;R \supset \con{diamond}\,(\con{RTC}\;R)\] Graficmente,
397 per esempio) stanno usando $\con{RTC}\;R$. La presenza di due istanze
398 di $\con{RTC}\;R$ � un'indicazione che questa dimostrazione richieder� due
412 l'assunzione pi� esterna (che $R$ ha la propriet� diamante), esso si accorder� con il
413 principio di induzione per \con{RTC}\footnote{In questa e nelle seguenti
469 Eseguiamo uno strip del goal il pi� possibile con l'obiettivo di rendere ci� che
498 noi gli diciamo quali sono le regole che governano \con{RTC}:
541 c'� un $u$ tale che $\con{RTC}\;R\;p\;u$ e $\con{RTC}\;R\;v\;u$. Di
542 fatto abbiamo bisogno un $u$ tale che $\con{RTC}\;R\;z\;u$, ma poich� c'�
544 di cui abbiamo bisogno di fornire a \texttt{PROVE\_TAC} sono le regole per \con{RTC}:
580 anche $\con{RTC}\;R$. Vogliamo dimostrare questo di nuovo per induzione.
582 \con{diamond}\;R\supset\con{diamond}\,(\con{RTC}\;R)
584 d'induzione quando � il momento giusto. E' meglio partire con una
586 d'induzione. Cos�, espandiamo manualmente il significato di \con{diamond} e dichiariamo
668 appellandoci soltanto alle regole per \con{RTC}. Questa volta non �
673 concludere $\con{RTC}\;R\;z\;u$ quando conosciamo che
674 $\con{RTC}\;R\;z\;v$ (assunzione 6 di sopra) e
675 $\con{RTC}\;R\;v\;u$ (la nostra conseguenza dell'ipotesi
720 \con{diamond}\;R & \supset & \con{diamond}\,(\con{RTC}\;R)\\
722 & & \con{diamond}\,(\con{RTC}\;R) & \equiv & \con{confluent}\;R\\
798 \subsection{Usare \con{RTC}}
830 Incidentalmente, in congiunzione con \texttt{PROVE} possiamo ora
849 \subsection{Dimostrare che le \con{RTC} sono le stesse}
852 Iniziamo con la direzione pi� facile, e mostriamo che ogni cosa che � in
854 \con{RTC} � monotona (fatto che � lasciato da dimostrare al lettore),
920 \con{RTC}; un passo della relazione di riduzione parallela non pu� essere riflesso
976 estremamente lungo per esaurire il suo spazio di ricerca, e poi arrendersi con un
1014 con solo un'altra applicazione di \texttt{PROVE\_TAC}, non abbiamo bisogno di
1015 usare il nostro footwork con \texttt{TRY} al passo precedente. Piuttosto,
1017 con \texttt{REPEAT CONJ\_TAC} e avere di fatto una dimostrazione con una tattica
1031 sono concatenati insieme, allora possiamo riflettere questo con qualche numero di
1056 dirci che \verb!x -->* y!. Poi questo pu� essere concatenato insieme con
1094 � di riscrivere con il teorema \texttt{FUN\_EQ\_THM}:
1157 \ml{predn\_cases} con il termine di input, e quindi semplifica. Il
1309 qui. Tuttavia, se riscriviamo in modo indiscriminato con esso,
1337 le composizioni da destra a sinistra, prima semplificheremo con il
1349 ad eliminare i casi semplici con una chiamata ``speculativa'' a
1523 che coinvolge direttamente la costante \con{diamond}:
1554 \item Dimostrare che \[\con{RTC}\;R \;x\; y \;\;\land \;\;
1555 \con{RTC}\;R\;y\;z\;\;\;\supset\;\;\; \con{RTC}\;R\;x\;z
1562 (\forall x\,y.\; \con{RTC}\;R_1\;x\;y \supset \con{RTC}\;R_2\;x\;y)
1564 \item Ancora un'altra induzione \con{RTC}, ma dove $R$ non � pi�
1579 & \exists u.\;\con{RTC}\;R\;y\;u \;\;\land\;\;\con{RTC}\;R\;z\;u
1582 \con{diamond}\;(\con{RTC}\;R)