[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.