Email Gateway (Aug 23 2022 at 09:20): Email Gateway (Aug 23 2022 at 09:20):From: Karolis Petrauskas <k.petrauskas@gmail.com>
I'm just starting with Isabelle/HOL so please excuse me for a simple question.
I'm working on an algorithm in the context of group theory and get
stuck while proving function termination.
Below is a simple example reproducing my confusion :)
In the original problem the Src variable does not decrease
monotonically, so I rely on the fact that the group G I work with is
finite and Dst is a strictly growing subset of carrier G.
The sets in copyRec are subsets of carrier G, although I don't find a
way to specify that.
Another precondition I would like to specify for the copyRec function
is that Src and Dst are disjoint.
How can I do that? Or maybe I should approach it in a different way?
theory TestCopy imports Main "HOL-Algebra.Group" begin
locale loc = group + assumes Finite: "finite (carrier G)"
begin
function copyRec :: "'a set ⇒ 'a set ⇒ 'a set" where
"copyRec Src Dst = (if Src = {} then Dst else (
let e = SOME e. e ∈ Src;
Src' = Src - {e};
Dst' = insert e Dst
in copyRec Src' Dst'
))"
by (pat_completeness, auto)
termination
proof (relation "measure (λ(Src, Dst). (card (carrier G)) - (card
Dst))", simp, simp)
fix Src Dst x xa xb
assume ne: "Src ≠ {}"
and ax: "x = (SOME e. e ∈ Src)"
and aa: "xa = Src - {SOME e. e ∈ Src}"
and ab: "xb = insert (SOME e. e ∈ Src) Dst"
have xs: "x ∈ Src" using ne and ax by (simp add: some_in_eq)
have nd: "x ∉ Dst" oops (here I need a fact that Src and Dst are disjoint)
have "card (insert x Dst) > card Dst" using nd by (blast)
qed
fun (in group) copy :: "'a set ⇒ 'a ⇒ 'a set" where
"copy H g = copyRec H {g}"
end
end
Thanks in advance,
Karolis Petrauskas
Email Gateway (Aug 23 2022 at 09:20):From: Martin Raszyk <m.raszyk@gmail.com>
Dear Karolis,
the easiest way to state your precondition is to put it into the
if-condition, i.e., have "if Src = {} ∨ Src ∩ Dst ≠ {} then Dst". This
way, the function is well-defined to be Dst if the precondition is not
satisfied and you can assume the precondition for the recursive call
which helps you proving the function's termination. More generally,
you can express a precondition as "if \neg P then undefined else ..."
where P expresses your precondition and "..." corresponds to the
definition assuming the precondition.
To get your original definition, you can then prove a lemma which has
the precondition as an assumption and contains your original function
definition as the conclusion, i.e., after the termination proof you
could state a lemma "Src ∩ Dst ≠ {} ==> copyRec Src Dst = ..." where
"..." correspond to your original definition.
Best regards,
Martin
Email Gateway (Aug 23 2022 at 09:20):From: Karolis Petrauskas <k.petrauskas@gmail.com>
Thanks, Martin, it worked.
Best regards,
Karolis
Last updated: Nov 21 2024 at 12:39 UTC