Walther Neuper <neuper@ist.tugraz.at> [Fri, 24 May 2013 12:40:15 +0200] rev 48868
tuned
Walther Neuper <neuper@ist.tugraz.at> [Fri, 24 May 2013 10:41:57 +0200] rev 48867
GCD_Poly.thy with writeln for HENSEL
Walther Neuper <neuper@ist.tugraz.at> [Thu, 23 May 2013 12:29:02 +0200] rev 48866
tuned
Walther Neuper <neuper@ist.tugraz.at> [Thu, 23 May 2013 12:20:28 +0200] rev 48865
GCD_Poly_FP.thy all termination proofs checked with size_change
size_change seems not appropriate for CA.
The key for progress is make_primes => next_prime_not_dvd => HENSEL_lifting_up.
The most difficult termination proof seems try_new_prime_up.
Walther Neuper <neuper@ist.tugraz.at> [Tue, 21 May 2013 11:33:03 +0200] rev 48864
GCD_Poly_FP.thy formatted according to 2013/../List.thy
Walther Neuper <neuper@ist.tugraz.at> [Tue, 21 May 2013 10:38:16 +0200] rev 48863
GCD_Poly_FP.thy all termination proofs checked
checked for simple provability, imperfect state documented here.
+ improved some int / nat signature(s)
+ replaced "nth" by "!"
Walther Neuper <neuper@ist.tugraz.at> [Sun, 19 May 2013 08:51:27 +0200] rev 48862
GCD_Poly_FP.thy improved with nat as much as possible instead int
Walther Neuper <neuper@ist.tugraz.at> [Mon, 13 May 2013 12:08:14 +0200] rev 48861
intermed. GCD_Poly_FP.thy termination
Walther Neuper <neuper@ist.tugraz.at> [Fri, 10 May 2013 10:47:23 +0200] rev 48860
GCD_Poly_FP.thy finished for univariate case
# 2 reasons for gcd_up not working are not resolved and marked with (*?FLORIAN*)
# strange observation: the not working version of dvd_up in 3cf89adce552
does not require the lemmata, but succeeds 'by pat_completenes auto'
Walther Neuper <neuper@ist.tugraz.at> [Fri, 10 May 2013 10:22:39 +0200] rev 48859
gcd_up works again
results of investigation will follow in subsequent commits