equal
deleted
inserted
replaced
515 @{thm (rhs) fresh_star_def[no_vars]}. |
515 @{thm (rhs) fresh_star_def[no_vars]}. |
516 A striking consequence of these definitions is that we can prove |
516 A striking consequence of these definitions is that we can prove |
517 without knowing anything about the structure of @{term x} that |
517 without knowing anything about the structure of @{term x} that |
518 swapping two fresh atoms, say @{text a} and @{text b}, leaves |
518 swapping two fresh atoms, say @{text a} and @{text b}, leaves |
519 @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"} |
519 @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"} |
520 then @{term "(a \<rightleftharpoons> b) \<bullet> x"}. |
520 then @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}. |
521 % |
521 % |
522 %\begin{myproperty}\label{swapfreshfresh} |
522 %\begin{myproperty}\label{swapfreshfresh} |
523 %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]} |
523 %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]} |
524 %\end{myproperty} |
524 %\end{myproperty} |
525 % |
525 % |
1134 terms. The main restriction is that we cannot return an atom in a binding function that is also |
1134 terms. The main restriction is that we cannot return an atom in a binding function that is also |
1135 bound in the corresponding term-constructor. That means in \eqref{letpat} |
1135 bound in the corresponding term-constructor. That means in \eqref{letpat} |
1136 that the term-constructors @{text PVar} and @{text PTup} may |
1136 that the term-constructors @{text PVar} and @{text PTup} may |
1137 not have a binding clause (all arguments are used to define @{text "bn"}). |
1137 not have a binding clause (all arguments are used to define @{text "bn"}). |
1138 In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons} |
1138 In contrast, in case of \eqref{letrecs} the term-constructor @{text ACons} |
1139 may have a binding clause involving the argument @{text t} (the only one that |
1139 may have a binding clause involving the argument @{text trm} (the only one that |
1140 is \emph{not} used in the definition of the binding function). This restriction |
1140 is \emph{not} used in the definition of the binding function). This restriction |
1141 is sufficient for lifting the binding function to $\alpha$-equated terms. |
1141 is sufficient for lifting the binding function to $\alpha$-equated terms. |
1142 |
1142 |
1143 In the version of |
1143 In the version of |
1144 Nominal Isabelle described here, we also adopted the restriction from the |
1144 Nominal Isabelle described here, we also adopted the restriction from the |
1184 term-constructors so that binders and their bodies are next to each other will |
1184 term-constructors so that binders and their bodies are next to each other will |
1185 result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}. |
1185 result in inadequate representations in cases like @{text "Let x\<^isub>1 = t\<^isub>1\<dots>x\<^isub>n = t\<^isub>n in s"}. |
1186 Therefore we will first |
1186 Therefore we will first |
1187 extract ``raw'' datatype definitions from the specification and then define |
1187 extract ``raw'' datatype definitions from the specification and then define |
1188 explicitly an $\alpha$-equivalence relation over them. We subsequently |
1188 explicitly an $\alpha$-equivalence relation over them. We subsequently |
1189 quotient the datatypes according to our $\alpha$-equivalence. |
1189 construct the quotient of the datatypes according to our $\alpha$-equivalence. |
1190 |
|
1191 |
1190 |
1192 The ``raw'' datatype definition can be obtained by stripping off the |
1191 The ``raw'' datatype definition can be obtained by stripping off the |
1193 binding clauses and the labels from the types. We also have to invent |
1192 binding clauses and the labels from the types. We also have to invent |
1194 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"} |
1193 new names for the types @{text "ty\<^sup>\<alpha>"} and term-constructors @{text "C\<^sup>\<alpha>"} |
1195 given by the user. In our implementation we just use the affix ``@{text "_raw"}''. |
1194 given by the user. In our implementation we just use the affix ``@{text "_raw"}''. |