128 unknowns may occur. Higher-order patterns are terms in $\beta$-normal |
128 unknowns may occur. Higher-order patterns are terms in $\beta$-normal |
129 form. (This means there are no subterms of the form $(\lambda x. M)(N)$.) |
129 form. (This means there are no subterms of the form $(\lambda x. M)(N)$.) |
130 Each occurrence of an unknown is of the form |
130 Each occurrence of an unknown is of the form |
131 $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound |
131 $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound |
132 variables. Thus all ordinary rewrite rules, where all unknowns are |
132 variables. Thus all ordinary rewrite rules, where all unknowns are |
133 of base type, for example @{thm add_assoc}, are acceptable: if an unknown is |
133 of base type, for example @{thm add.assoc}, are acceptable: if an unknown is |
134 of base type, it cannot have any arguments. Additionally, the rule |
134 of base type, it cannot have any arguments. Additionally, the rule |
135 @{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also acceptable, in |
135 @{text"(\<forall>x. ?P x \<and> ?Q x) = ((\<forall>x. ?P x) \<and> (\<forall>x. ?Q x))"} is also acceptable, in |
136 both directions: all arguments of the unknowns @{text"?P"} and |
136 both directions: all arguments of the unknowns @{text"?P"} and |
137 @{text"?Q"} are distinct bound variables. |
137 @{text"?Q"} are distinct bound variables. |
138 |
138 |