Email Gateway (Aug 19 2022 at 11:20): Email Gateway (Aug 19 2022 at 11:20):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.
Last updated: Apr 25 2024 at 16:19 UTC