diff -r 44840614ea0c -r b52b72676e20 Nominal/Fv.thy --- a/Nominal/Fv.thy Thu Mar 18 14:29:42 2010 +0100 +++ b/Nominal/Fv.thy Thu Mar 18 14:48:27 2010 +0100 @@ -50,9 +50,9 @@ with fv of the appropriate type - otherwise empty -2) fv functions generated for all new datatypes: +2) fv_ty functions generated for all types being defined: - An fv for a constructor is a union of values for the arguments. + fv_ty for a constructor is a union of values for the arguments. For an argument that is bound in a shallow binding we return empty. @@ -92,6 +92,29 @@ - for other arguments in the bn function we return: True - for other arguments not in the bn function we return: argl = argr +2) alpha_ty relations are generated for all the types being defined: + + !!! permutations !!! + + An alpha_ty for a constructor is true if a conjunction of + propositions for each argument holds. + + For an argument we allow bindings where only one of the following + holds: + + - Argument is bound in some shallow bindings: We return true + - Argument is bound in some deep recursive bindings + !!! still to describe !!! + - Argument is bound in some deep non-recursive bindings. + We return: alpha_bn argl argr + - Argument has some shallow and/or non-recursive bindings. + !!! still to describe !!! + - Argument has some recursive bindings. The bindings were + already treated in 2nd case so we return: True + - Argument has no bindings and is not bound. + If it is recursive for type ty, we return: alpha_ty argl argr + Otherwise we return: argl = argr + *) ML {*