Email Gateway (Aug 19 2022 at 09:37): Email Gateway (Aug 19 2022 at 09:37):From: Walther Neuper <wneuper@ist.tugraz.at>
First steps with the function package were successful.
Now I don't know how to remove a proof obligation containing a function
constant named 'function_id_sumC', where 'function_id' is the function
under consideration:
2. ?primes last_p n primesa last_pa na.
(primes, last_p, n) = (primesa, last_pa, na) ?
(if primes ! (length primes - 1) < n
then
if is_prime primes (last_p + 2)
then make_prims_sumC (primes @ [last_p + 2], last_p + 2, n)
else make_prims_sumC (primes, last_p + 2, n) else primes) =
(if primesa ! (length primesa - 1) < na
then
if is_prime primesa (last_pa + 2)
then make_prims_sumC (primesa @ [last_pa + 2], last_pa + 2,
na)
else make_prims_sumC (primesa, last_pa + 2, na)
else primesa)
Why did the function package generate this 'function_id_sumC' ?
And how can I prove the proof obligation ?
Thanks for your help,
Walther
PS: The function definition is in the attachment.
GCD_1_Make_Primes.thy
Email Gateway (Aug 19 2022 at 09:37):From: Lars Noschinski <noschinl@in.tum.de>
This is what you get if you unfold function_id_def which is something
you would never do in a normal proof.
Using function_id.{simps,induct,cases} should suffice.
-- Lars
Email Gateway (Aug 19 2022 at 09:37):From: Johannes Hölzl <hoelzl@in.tum.de>
How does your proof look like?
Do you use make_prims_def ? <func>_def should be only used internally,
to unfold the function you should use make_prims.simps. The ...simps
rules are the one you use in your function specification.
Email Gateway (Aug 19 2022 at 09:37):From: Alexander Krauss <krauss@in.tum.de>
Here, unfortunately, the internal encoding shines through. In your
concrete case, the currying was converted to tuples, in other cases,
several mutual recursive functions may be converted to a function on a
sum type (hence the suffix).
In your concrete case, the simplifier loops because the equation for
is_prime loops in the presence of the usual splitting of ifs.
Thus, "by pat_completeness (simp del: is_prime.simps)" does the trick here.
In general, you cannot prove much about the _sumC functions. The goals
are usually provable when treating them as uninterpreted.
Alex
Email Gateway (Aug 19 2022 at 10:02):From: Walther Neuper <wneuper@ist.tugraz.at>
Sorry for not coming with my problem cut down to a minimal example ---
my problem is the mass of tracing output from the simplifier.
In particular, I'd appreciate hints, how to identify the culprit from
the output created by
declare [[simp_trace_depth_limit=9]]
declare [[simp_trace=true]]
when I activate the outcommented base case in the function below and
thus make the function package loop:
(* dvd for univariate polynomials *)
function dvd_up :: "unipoly ? unipoly ? bool" (infixl "dvd'_up" 70) where
(* FIXME this makes the function package loop ......
"[d] dvd_up [i] =
(if (¦d¦ ? ¦i¦) & (i mod d = 0) then True else False)"
|*) "d dvd_up p =
(let
d = drop_lc0 d;
p = drop_lc0 p;
d000 = (List.replicate (List.length p - List.length d) 0) @ d;
quot = (lc p) div2 (lc d000);
rest = drop_lc0 (p minus_up (d000 div_ups quot))
in
if rest = [] then True
else
(if quot ? 0 & List.length d ? List.length rest
then d dvd_up rest
else False))"
by pat_completeness auto
termination sorry
I'd appreciate help not by a solution (like the one below -- thank you,
Alex!), but by hints how to find the culprit for looping myself.
Walther
PS: The auxiliary functions are in the appendix. Of course, they are all
checked, see
[1]https://intra.ist.tugraz.at/hg/isa/raw-file/913483f0582b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy
GCD_Poly_Test3.thy
Last updated: Apr 18 2024 at 20:16 UTC