# [isabelle] partial_function: order of variables in induction rule

`I would like to define some set-valued functions whose recursive definition does not
``terminate. I know that such functions can in principle be defined with inductive_set, but
``inductive_set does not allow parameters of the function to change in recursive calls (see
``http://stackoverflow.com/questions/16603886/inductive-set-with-non-fixed-parameters). So I
``thought I should give partial_function a try, as sets form a ccpo with the standard subset
``ordering. Setting up partial_function for sets is straightforward, but I am have trouble
``with the induction rule:
`
lemma fixp_induct_set:
fixes F :: "'c => 'c"
and U :: "'c => 'b => 'a set"
and C :: "('b => 'a set) => 'c"
and P :: "'b => 'a => bool"
assumes mono: "!!x. monotone (fun_ord op <=) op <= (%f. U (F (C f)) x)"
and eq: "f == C (ccpo.fixp (fun_lub Sup) (fun_ord op <=) (%f. U (F (C f))))"
and inverse2: "!!f. U (C f) = f"
and step: "!!f x y. [| y : U (F f) x; !!x y. y : U f x ==> P x y |] ==> P x y"
and enforce_variable_ordering: "x = x"
and elem: "y : U f x"
shows "P x y"

`Note the bogus assumption enforce_variable_ordering. Without it, the variable y occurs
``before x in the order of variables of the theorem. partial_function then tries to
``instantiate them in the wrong way and I get a type error. For example:
`
partial_function (set) test :: "nat => int set"
where "test n = {}"
*** exception THM 0 raised (line 1155 of "thm.ML"):
*** instantiate: type conflict
*** ?y :: int
*** n :: nat
*** [| !!x. monotone (fun_ord op <=) op <= (%f. ?F f x);
*** ?f == ccpo.fixp (fun_lub Union) (fun_ord op <=) ?F;
*** !!f x y. [|y : ?F f x; !!x y. y : f x ==> ?P x y|] ==> ?P x y; ?y : ?f ?x|]
*** ==> ?P ?x ?y
*** At command "partial_function"

`With the superflous assumption enforce_variable_ordering, partial_function accepts the
``specification. Is this a known limitation of partial_function? Is there some other way to
``enforce the variable ordering of a theorem or to tell partial_function to instantiate
``variables in the reversed order?
`
Cheers,
Andreas

`PS: If other people find partial_function for sets useful, I could add the setup to the
``repository.
`

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*