1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Fri Aug 24 13:05:00 2018 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Fri Aug 24 14:23:13 2018 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  *}
     1.5  
     1.6  section {* Isabelle's predefined polynomials *}
     1.7 ---"TODO"
     1.8 +\<comment> \<open>TODO\<close>
     1.9  
    1.10  section {* gcd for univariate polynomials *}
    1.11  
    1.12 @@ -147,16 +147,16 @@
    1.13    then False
    1.14    else is_prime (List.tl ps) n
    1.15  else True)"
    1.16 -declare is_prime.simps [simp del] -- "make_primes, next_prime_not_dvd"
    1.17 +declare is_prime.simps [simp del]     \<comment> \<open>make_primes, next_prime_not_dvd\<close>
    1.18  
    1.19 -value "is_prime [2, 3] 2  = False"    --"... precondition!"
    1.20 -value "is_prime [2, 3] 3  = False"    --"... precondition!"
    1.21 +value "is_prime [2, 3] 2  = False"    \<comment> \<open>... precondition!\<close>
    1.22 +value "is_prime [2, 3] 3  = False"    \<comment> \<open>... precondition!\<close>
    1.23  value "is_prime [2, 3] 4  = False"
    1.24  value "is_prime [2, 3] 5  = True"
    1.25 -value "is_prime [2, 3, 5] 5  = False" --"... precondition!"
    1.26 +value "is_prime [2, 3, 5] 5  = False" \<comment> \<open>... precondition!\<close>
    1.27  value "is_prime [2, 3] 6  = False"
    1.28  value "is_prime [2, 3] 7  = True"
    1.29 -value "is_prime [2, 3] 25 = True"     -- "... because 5 not in list"
    1.30 +value "is_prime [2, 3] 25 = True"     \<comment> \<open>... because 5 not in list\<close>
    1.31  
    1.32  (* make_primes is just local to primes_upto only:
    1.33     make_primes :: int list \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int list
    1.34 @@ -170,11 +170,11 @@
    1.35    (if n \<le> last ps then ps
    1.36     else make_primes (last_p + 2) n 
    1.37      (if is_prime ps (last_p + 2) then ps @ [last_p + 2] else ps))"
    1.38 -by pat_completeness auto --"simp del: is_prime.simps <-- declare"
    1.39 +by pat_completeness auto \<comment> \<open>simp del: is_prime.simps <-- declare\<close>
    1.40  termination make_primes (*by lexicographic_order +PROOF primes? / size_change LOOPS*)
    1.41 -sorry -- {* FIXME proof needs semantic properties of primes themselves *}
    1.42 +sorry \<comment> \<open>FIXME proof needs semantic properties of primes themselves\<close>
    1.43  
    1.44 -declare make_primes.simps [simp del] -- "next_prime_not_dvd"
    1.45 +declare make_primes.simps [simp del] \<comment> \<open>next_prime_not_dvd\<close>
    1.46  
    1.47  value "make_primes 3  3 [2, 3] = [2, 3]"
    1.48  value "make_primes 3  4 [2, 3] = [2, 3, 5]"
    1.49 @@ -245,7 +245,7 @@
    1.50    if n2 mod nxt \<noteq> 0
    1.51    then nxt
    1.52    else nxt next_prime_not_dvd n2)"
    1.53 -by auto --"simp del: is_prime.simps, make_primes.simps, primes_upto.simps <-- declare"
    1.54 +by auto \<comment> \<open>simp del: is_prime.simps, make_primes.simps, primes_upto.simps < -- declare*\<close>
    1.55  termination sorry (*next_prime_not_dvd: lexicographic_order  +PROOF primes? / size_change: Failed*)
    1.56  
    1.57  value "1 next_prime_not_dvd 15 = 2"
    1.58 @@ -301,7 +301,7 @@
    1.59   lcp = lcoeff_up p
    1.60  in 
    1.61    if List.length p = 0 then [] else norm p [] m lcp (List.length p - 1))"
    1.62 -declare normalise.simps [simp del] --"HENSEL_lifting_up"
    1.63 +declare normalise.simps [simp del] \<comment> \<open>HENSEL_lifting_up\<close>
    1.64  
    1.65  value "normalise [-18, -15, -20, 12, 20, -13, 2] 5 = [1, 0, 0, 1, 0, 1, 1]"
    1.66  value "normalise [9, 6, 3] 10                      = [3, 2, 1]"
    1.67 @@ -502,7 +502,7 @@
    1.68  by auto
    1.69  termination mod_up_gcd (*by lexicographic_order +PROOF primes? / size_change LOOPS*)
    1.70  sorry
    1.71 -declare mod_up_gcd.simps [simp del] --"HENSEL_lifting_up"
    1.72 +declare mod_up_gcd.simps [simp del] \<comment> \<open>HENSEL_lifting_up\<close>
    1.73  
    1.74  value "mod_up_gcd [-18, -15, -20, 12, 20, -13, 2] [8, 28, 22, -11, -14, 1, 2] 7 = [2, 6, 0, 2, 6]" 
    1.75  value "mod_up_gcd [8, 28, 22, -11, -14, 1, 2] [2, 6, 0, 2, 6] 7 = [2, 6, 0, 2, 6]" 
    1.76 @@ -567,7 +567,7 @@
    1.77            P = P * p;
    1.78            g = centr_up ((chinese_remainder_up (P, p) (g, g_p)) mod_up P) P
    1.79          in try_new_prime_up a b d M P g p)"
    1.80 -by pat_completeness auto --"simp del: centr_up_def normalise.simps mod_up_gcd.simps"
    1.81 +by pat_completeness auto \<comment> \<open>simp del: centr_up_def normalise.simps mod_up_gcd.simps\<close>
    1.82  termination try_new_prime_up (*by lexicographic_order +PROOF primes? / by size_change LOOPS*)
    1.83  sorry
    1.84  
    1.85 @@ -590,7 +590,7 @@
    1.86        g = primitive_up (try_new_prime_up a b d M p g_p p)
    1.87      in
    1.88        if (g %|% a) \<and> (g %|% b) then g else HENSEL_lifting_up a b d M p))"
    1.89 -by pat_completeness auto --"simp del: centr_up_def normalise.simps mod_up_gcd.simps"
    1.90 +by pat_completeness auto \<comment> \<open>simp del: centr_up_def normalise.simps mod_up_gcd.simps\<close>
    1.91  termination HENSEL_lifting_up (*by lexicographic_order LOOPS +PROOF primes? / by size_change LOOPS*)
    1.92  sorry 
    1.93  
    1.94 @@ -605,7 +605,7 @@
    1.95  in
    1.96    if a = b then a else
    1.97      HENSEL_lifting_up a b (nat d) (2 * (nat d) * LANDAU_MIGNOTTE_bound a b) 1)"
    1.98 -by pat_completeness auto --"simp del: lcoeff_up.simps ?+ others?"
    1.99 +by pat_completeness auto \<comment> \<open>simp del: lcoeff_up.simps ?+ others?\<close>
   1.100  termination by lexicographic_order (*works*)
   1.101  
   1.102  ML {*"----------- fun gcd_up ---------------------------------";*}