# HG changeset patch
# User Walther Neuper <wneuper@ist.tugraz.at>
# Date 1535113393 -7200
# Node ID d732e8e2f17c005f85fcff14a290132887b16505
# Parent  9ceb8e1e39594eb13c36f759ab3a0c24ef1d12d6
Isabelle2017->18: for Test_Isac.thy adopt new comments

diff -r 9ceb8e1e3959 -r d732e8e2f17c src/Tools/isac/Knowledge/GCD_Poly_FP.thy
--- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Fri Aug 24 13:05:00 2018 +0200
+++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Fri Aug 24 14:23:13 2018 +0200
@@ -13,7 +13,7 @@
 *}
 
 section {* Isabelle's predefined polynomials *}
---"TODO"
+\<comment> \<open>TODO\<close>
 
 section {* gcd for univariate polynomials *}
 
@@ -147,16 +147,16 @@
   then False
   else is_prime (List.tl ps) n
 else True)"
-declare is_prime.simps [simp del] -- "make_primes, next_prime_not_dvd"
+declare is_prime.simps [simp del]     \<comment> \<open>make_primes, next_prime_not_dvd\<close>
 
-value "is_prime [2, 3] 2  = False"    --"... precondition!"
-value "is_prime [2, 3] 3  = False"    --"... precondition!"
+value "is_prime [2, 3] 2  = False"    \<comment> \<open>... precondition!\<close>
+value "is_prime [2, 3] 3  = False"    \<comment> \<open>... precondition!\<close>
 value "is_prime [2, 3] 4  = False"
 value "is_prime [2, 3] 5  = True"
-value "is_prime [2, 3, 5] 5  = False" --"... precondition!"
+value "is_prime [2, 3, 5] 5  = False" \<comment> \<open>... precondition!\<close>
 value "is_prime [2, 3] 6  = False"
 value "is_prime [2, 3] 7  = True"
-value "is_prime [2, 3] 25 = True"     -- "... because 5 not in list"
+value "is_prime [2, 3] 25 = True"     \<comment> \<open>... because 5 not in list\<close>
 
 (* make_primes is just local to primes_upto only:
    make_primes :: int list \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int list
@@ -170,11 +170,11 @@
   (if n \<le> last ps then ps
    else make_primes (last_p + 2) n 
     (if is_prime ps (last_p + 2) then ps @ [last_p + 2] else ps))"
-by pat_completeness auto --"simp del: is_prime.simps <-- declare"
+by pat_completeness auto \<comment> \<open>simp del: is_prime.simps <-- declare\<close>
 termination make_primes (*by lexicographic_order +PROOF primes? / size_change LOOPS*)
-sorry -- {* FIXME proof needs semantic properties of primes themselves *}
+sorry \<comment> \<open>FIXME proof needs semantic properties of primes themselves\<close>
 
-declare make_primes.simps [simp del] -- "next_prime_not_dvd"
+declare make_primes.simps [simp del] \<comment> \<open>next_prime_not_dvd\<close>
 
 value "make_primes 3  3 [2, 3] = [2, 3]"
 value "make_primes 3  4 [2, 3] = [2, 3, 5]"
@@ -245,7 +245,7 @@
   if n2 mod nxt \<noteq> 0
   then nxt
   else nxt next_prime_not_dvd n2)"
-by auto --"simp del: is_prime.simps, make_primes.simps, primes_upto.simps <-- declare"
+by auto \<comment> \<open>simp del: is_prime.simps, make_primes.simps, primes_upto.simps < -- declare*\<close>
 termination sorry (*next_prime_not_dvd: lexicographic_order  +PROOF primes? / size_change: Failed*)
 
 value "1 next_prime_not_dvd 15 = 2"
@@ -301,7 +301,7 @@
  lcp = lcoeff_up p
 in 
   if List.length p = 0 then [] else norm p [] m lcp (List.length p - 1))"
-declare normalise.simps [simp del] --"HENSEL_lifting_up"
+declare normalise.simps [simp del] \<comment> \<open>HENSEL_lifting_up\<close>
 
 value "normalise [-18, -15, -20, 12, 20, -13, 2] 5 = [1, 0, 0, 1, 0, 1, 1]"
 value "normalise [9, 6, 3] 10                      = [3, 2, 1]"
@@ -502,7 +502,7 @@
 by auto
 termination mod_up_gcd (*by lexicographic_order +PROOF primes? / size_change LOOPS*)
 sorry
-declare mod_up_gcd.simps [simp del] --"HENSEL_lifting_up"
+declare mod_up_gcd.simps [simp del] \<comment> \<open>HENSEL_lifting_up\<close>
 
 value "mod_up_gcd [-18, -15, -20, 12, 20, -13, 2] [8, 28, 22, -11, -14, 1, 2] 7 = [2, 6, 0, 2, 6]" 
 value "mod_up_gcd [8, 28, 22, -11, -14, 1, 2] [2, 6, 0, 2, 6] 7 = [2, 6, 0, 2, 6]" 
@@ -567,7 +567,7 @@
           P = P * p;
           g = centr_up ((chinese_remainder_up (P, p) (g, g_p)) mod_up P) P
         in try_new_prime_up a b d M P g p)"
-by pat_completeness auto --"simp del: centr_up_def normalise.simps mod_up_gcd.simps"
+by pat_completeness auto \<comment> \<open>simp del: centr_up_def normalise.simps mod_up_gcd.simps\<close>
 termination try_new_prime_up (*by lexicographic_order +PROOF primes? / by size_change LOOPS*)
 sorry
 
@@ -590,7 +590,7 @@
       g = primitive_up (try_new_prime_up a b d M p g_p p)
     in
       if (g %|% a) \<and> (g %|% b) then g else HENSEL_lifting_up a b d M p))"
-by pat_completeness auto --"simp del: centr_up_def normalise.simps mod_up_gcd.simps"
+by pat_completeness auto \<comment> \<open>simp del: centr_up_def normalise.simps mod_up_gcd.simps\<close>
 termination HENSEL_lifting_up (*by lexicographic_order LOOPS +PROOF primes? / by size_change LOOPS*)
 sorry 
 
@@ -605,7 +605,7 @@
 in
   if a = b then a else
     HENSEL_lifting_up a b (nat d) (2 * (nat d) * LANDAU_MIGNOTTE_bound a b) 1)"
-by pat_completeness auto --"simp del: lcoeff_up.simps ?+ others?"
+by pat_completeness auto \<comment> \<open>simp del: lcoeff_up.simps ?+ others?\<close>
 termination by lexicographic_order (*works*)
 
 ML {*"----------- fun gcd_up ---------------------------------";*}