header {* GCD for polynomials, implemented using the function package (_FP) *}

theory GCD_Poly_FP 

imports "~~/src/HOL/Library/Polynomial" "~~/src/HOL/Number_Theory/Primes"

begin

text {* 

  This code has been translated from GCD_Poly.thy by Diana Meindl,

  who follows Franz Winkler, Polynomial algorithyms in computer algebra, Springer 1996.

  Winkler's original identifiers are in test/./gcd_poly_winkler.sml;

  test/../gcd_poly.sml documents the changes towards GCD_Poly.thy;

  the style of GCD_Poly.thy has been adapted to the function package.

*}

(* WN130304.TODO see Algebra/poly/LongDiv.thy: lcoeff_def*)

(*---------------------------------------------------------------------------------------------

declare [[simp_trace_depth_limit = 99]]

declare [[simp_trace = true]]

---------------------------------------------------------------------------------------------*)

section {* gcd for univariate polynomials *}

type_synonym unipoly = "int list"

value "[0, 1, 2, 3, 4, 5] :: unipoly"

subsection {* a variant for div *}

(* 5 div 2 = 2; ~5 div 2 = ~3; but ~5 div2 2 = ~2; *)

definition div2 :: "int \<Rightarrow> int \<Rightarrow> int" (infixl "div2" 70) where

"a div2 b = (if a div b < 0 then (\<bar>a\<bar> div \<bar>b\<bar>) * -1 else a div b)"

value " 5 div2  2 =  2"

value "-5 div2  2 = -2"

value "-5 div2 -2 =  2"

value " 5 div2 -2 = -2"

value "gcd (15::int) (6::int) = 3"

value "gcd (10::int) (3::int) = 1"

value "gcd (6::int) (24::int) = 6"

(*---------------------------------------------------------------------------------------------*)

subsection {* modulo calculations for integers *}

(* modi is just local for mod_inv *)

function modi :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where

  "modi r rold m rinv = 

    (if m \<le> rinv

      then 0 else

        if r mod m = 1 

        then rinv 

        else modi (rold * (rinv + 1)) rold m (rinv + 1))"

  by auto

  termination sorry

(* mod_inv :: int \<Rightarrow> nat 

   mod_inv r m = s

   assumes True

   yields r * s mod m = 1 *)

fun mod_inv :: "int \<Rightarrow> int \<Rightarrow> int" where

  "mod_inv r m = modi r r m 1"

value "modi 5 5 7 1   = 3"

value "modi 3 3 7 1   = 5"

value "modi 4 4 339 1 = 85"

value "mod_inv 5 7    = 3"

value "mod_inv 3 7    = 5"

value "mod_inv 4 339  = 85"

(* mod_div :: int \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> nat

   mod_div a b m = c

   assumes True

   yields a * b ^(-1) mod m = c   <\<Longrightarrow>  a mod m = *)

definition mod_div :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where

  "mod_div a b m = a * (mod_inv b m) mod m"

(* root1 is just local to approx_root *)

function root1 :: "int \<Rightarrow> int \<Rightarrow> int" where

  "root1 a n = (if n * n < a then root1 a (n + 1) else n)"

by auto

termination sorry

(* required just for one approximation:

   approx_root :: nat \<Rightarrow> nat

   approx_root a = r

   assumes True

   yields r * r \<ge> a *)

definition approx_root :: "int \<Rightarrow> int" where

  "approx_root a = root1 a 1"

(* chinese_remainder :: int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int

   chinese_remainder r1 m1 r2 m2 = r

   assumes True

   yields r = r1 mod m1 \<and> r = r2 mod m2 *)

definition chinese_remainder :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where

  "chinese_remainder r1 m1 r2 m2 = 

    (r1 mod m1) + ((r2 - (r1 mod m1)) * (mod_inv m1 m2) mod m2) * m1"

value "chinese_remainder 17 9 3 4  = 35"

value "chinese_remainder  7 2 6 11 = 17"

subsection {* operations with primes *}

(* is_prime :: int list \<Rightarrow> int \<Rightarrow> bool

   is_prime ps n = b

   assumes max ps < n  \<and>  n \<le> (max ps)^2  \<and>  

     (*     FIXME: really ^^^^^^^^^^^^^^^? *)

     (\<forall>p. List.member ps p \<longrightarrow> Primes.prime p) \<and> (\<forall>p. p < n \<and> Primes.prime p \<longrightarrow> List.member ps p)

   yields Primes.prime n *)

fun is_prime :: "nat list \<Rightarrow> nat \<Rightarrow> bool" where

  "is_prime ps n = 

    (if List.length ps > 0

    then 

      if (n mod (List.hd ps)) = 0

      then False

      else is_prime (List.tl ps) n

    else True)"

declare is_prime.simps [simp del] -- "make_primes, next_prime_not_dvd"

value "is_prime [2, 3] 2  = False"    --"... precondition!"

value "is_prime [2, 3] 3  = False"    --"... precondition!"

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] 6  = False"

value "is_prime [2, 3] 7  = True"

value "is_prime [2, 3] 25 = True"     -- "... because 5 not in list"

(* make_primes is just local to primes_upto only:

   make_primes :: int list \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int list

   make_primes ps last_p n = pps

   assumes last_p = maxs ps  \<and>  (\<forall>p. List.member ps p \<longrightarrow> Primes.prime p)  \<and>

     (\<forall>p. p < last_p \<and> Primes.prime p \<longrightarrow> List.member ps p)

   yields n \<le> maxs pps  \<and>  (\<forall>p. List.member pps p \<longrightarrow> Primes.prime p)  \<and>

     (\<forall>p. (p < maxs pps \<and> Primes.prime p) \<longrightarrow> List.member pps p)*)

function make_primes :: "nat list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat list" where

  "make_primes ps last_p n =

    (if (List.nth ps (List.length ps - 1)) < n

    then

      if is_prime ps (last_p + 2)

      then make_primes (ps @ [(last_p + 2)]) (last_p + 2) n

      else make_primes  ps (last_p + 2) n

    else ps)"

by pat_completeness simp

termination sorry

declare make_primes.simps [simp del] -- "next_prime_not_dvd"

value "make_primes [2, 3] 3 4 = [2, 3, 5]"

value "make_primes [2, 3] 3 5 = [2, 3, 5]"

value "make_primes [2, 3] 3 6 = [2, 3, 5, 7]"

value "make_primes [2, 3] 3 7 = [2, 3, 5, 7]"

value "make_primes [2, 3] 3 8 = [2, 3, 5, 7, 11]"

value "make_primes [2, 3] 3 9 = [2, 3, 5, 7, 11]"

value "make_primes [2, 3] 3 10 = [2, 3, 5, 7, 11]"

value "make_primes [2, 3] 3 11 = [2, 3, 5, 7, 11]"

value "make_primes [2, 3] 3 12 = [2, 3, 5, 7, 11, 13]"

value "make_primes [2, 3] 3 13 = [2, 3, 5, 7, 11, 13]"

value "make_primes [2, 3] 3 14 = [2, 3, 5, 7, 11, 13, 17]"

value "make_primes [2, 3] 3 15 = [2, 3, 5, 7, 11, 13, 17]"

value "make_primes [2, 3] 3 16 = [2, 3, 5, 7, 11, 13, 17]"

value "make_primes [2, 3] 3 17 = [2, 3, 5, 7, 11, 13, 17]"

value "make_primes [2, 3] 3 18 = [2, 3, 5, 7, 11, 13, 17, 19]"

value "make_primes [2, 3] 3 19 = [2, 3, 5, 7, 11, 13, 17, 19]"

value "make_primes [2, 3, 5, 7] 7 4 = [2, 3, 5, 7]"

(* primes_upto :: nat \<Rightarrow> nat list

   primes_upto n = ps

     assumes True

     yields (\<forall>p. List.member ps p \<longrightarrow> Primes.prime p) \<and>

       n \<le> maxs ps \<and> maxs ps \<le> Fact.fact n + 1 \<and>

       (\<forall>p. p \<le> maxs ps \<and> Primes.prime p \<longrightarrow> List.member ps p) *)

fun primes_upto :: "nat \<Rightarrow> nat list" where

  "primes_upto n = (if n < 3 then [2] else make_primes [2, 3] 3 n)"

declare primes_upto.simps [simp del] -- "next_prime_not_dvd"

value "primes_upto  2 = [2]"

value "primes_upto  3 = [2, 3]"

value "primes_upto  4 = [2, 3, 5]"

value "primes_upto  5 = [2, 3, 5]"

value "primes_upto  6 = [2, 3, 5, 7]"

value "primes_upto  7 = [2, 3, 5, 7]"

value "primes_upto  8 = [2, 3, 5, 7, 11]"

value "primes_upto  9 = [2, 3, 5, 7, 11]"

value "primes_upto 10 = [2, 3, 5, 7, 11]"

value "primes_upto 11 = [2, 3, 5, 7, 11]"

(* max's' is analogous to Integer.gcds *)

fun maxs :: "nat list \<Rightarrow> nat" where

  "maxs ns = List.fold max ns (List.hd ns)"

value "maxs [5, 3, 7, 1, 2, 4] = 7"

(* find the next prime greater p not dividing the number n:

  next_prime_not_dvd :: int \<Rightarrow> int \<Rightarrow> int (infix)

  n1 next_prime_not_dvd n2 = p

    assumes True

    yields p is_prime  \<and>  n1 < p  \<and>  \<not> p dvd n2  \<and> (* smallest with these properties... *)

      (\<forall> p'. (p' is_prime  \<and>  n1 < p'  \<and>  \<not> p' dvd n2)  \<longrightarrow>  p \<le> p') *)

function next_prime_not_dvd :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "next'_prime'_not'_dvd" 70) where

 "n1 next_prime_not_dvd n2 = 

  (let

    ps = primes_upto (n1 + 1);

    nxt = List.nth ps (List.length ps - 1) (* take_last *)

  in

    if n2 mod nxt \<noteq> 0

    then nxt

    else nxt next_prime_not_dvd n2)"

by auto

termination sorry

subsection {* auxiliary functions for univariate polynomials *}

(* not in List.thy, copy from library.ML *)

fun nth_drop :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where

  "nth_drop n xs = List.take n xs @ List.drop (n + 1) xs"

value "nth_drop 0 []              = []"

value "nth_drop 0 [1, 2, 3::int]  = [2, 3]"

value "nth_drop 2 [1, 2, 3::int]  = [1, 2]"

value "nth_drop 77 [1, 2, 3::int] = [1, 2, 3]"

(* leading coefficient *)

function lcoeff :: "unipoly \<Rightarrow> int" where

  "lcoeff uvp =

    (if List.nth uvp (List.length uvp - 1) \<noteq> 0

    then List.nth uvp (List.length uvp - 1)

    else lcoeff (nth_drop (List.length uvp - 1) uvp))"

by auto 

termination sorry

value "lcoeff [3, 4, 5, 6]    = 6"

value "lcoeff [3, 4, 5, 6, 0] = 6"

(* degree *)

function deg :: "unipoly \<Rightarrow> nat" where

  "deg uvp =

    (let len = List.length uvp - 1

    in

      if nth uvp len \<noteq> 0 then len else deg (nth_drop len uvp))"

by auto 

termination sorry

value "deg [3, 4, 5, 6]    = 3"

value "deg [3, 4, 5, 6, 0] = 3"

(* drop leading coefficients equal 0 *)

fun drop_lc0 :: "unipoly \<Rightarrow> unipoly" where 

  "drop_lc0 [] = []"

| "drop_lc0 uvp = 

    (let l = List.length uvp - 1

    in

      if nth uvp l = 0

      then drop_lc0 (nth_drop l uvp)

      else uvp)"

value "drop_lc0 [0, 1, 2, 3, 4, 5, 0, 0] = [0, 1, 2, 3, 4, 5]"

value "drop_lc0 [0, 1, 2, 3, 4, 5]       = [0, 1, 2, 3, 4, 5]"

(* norm is just local to normalise *)

fun norm :: "unipoly \<Rightarrow> unipoly \<Rightarrow> int (*nat?*) \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> unipoly" where

  "norm pol nrm m lcp i = 

    (if i = 0

        then [mod_div (nth pol i) lcp m] @ nrm

        else norm pol ([mod_div (nth pol i) lcp m] @  nrm) m lcp (i - 1))"

(* normalise a unipoly such that lcoeff mod m = 1.

   normalise :: unipoly \<Rightarrow> nat \<Rightarrow> unipoly

   normalise [p_0, .., p_k] m = [q_0, .., q_k]

     assumes 

     yields \<exists> t. 0 \<le> i \<le> k \<Rightarrow> (p_i * t) mod m = q_i  \<and>  (p_k * t) mod m = 1 *)

fun normalise :: "unipoly \<Rightarrow> int (*nat?*) \<Rightarrow> unipoly" where

  "normalise p m = 

    (let

     p = drop_lc0 p;

     lcp = lcoeff p

    in 

      if List.length p = 0 then p else norm p [] m lcp (List.length p - 1))"

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]"

(* scalar multiplication, %* in GCD_Poly.thy *)

fun  mult_ups :: "unipoly \<Rightarrow> int \<Rightarrow> unipoly" (infixl "mult'_ups" 70) where

 "p mult_ups m = List.map (op * m) p"

value "[5, 4, 7, 8, 1] mult_ups 5   = [25, 20, 35, 40, 5]"

value "[5, 4, -7, 8, -1] mult_ups 5 = [25, 20, -35, 40, -5]"

(* scalar divison, %/ in GCD_Poly.thy *)

definition swapf :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where

  "swapf f a b = f b a"

definition div_ups :: "unipoly \<Rightarrow> int \<Rightarrow> unipoly" (infixl "div'_ups" 70) where

  "p div_ups m = map (swapf op div2 m) p"

value "[4, 3, 2, 5, 6] div_ups 3 = [1, 1, 0, 1, 2]"

value "[4, 3, 2, 0] div_ups 3    = [1, 1, 0, 0]"

(* not in List.thy, copy from library.ML *)

fun map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where

  "map2 _ [] [] = []"

| "map2 f (x # xs) (y # ys) = f x y # map2 f xs ys"

| "map2 _ _ _ = []" (*raise ListPair.UnequalLengths*)

(* minus of polys,  %-% in GCD_Poly.thy *)

definition minus_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> unipoly" (infixl "minus'_up" 70) where

  "p1 minus_up p2 = map2 (op -) p1 p2"

value "[8, -7, 0, 1] minus_up [-2, 2, 3, 0]     = [10, -9, -3, 1]"

value "[8, 7, 6, 5, 4] minus_up [2, 2, 3, 1, 1] = [6, 5, 3, 4, 3]"

ML {*1-1-1-1-1-1-1-1-1-1-1-1-1-1-1-1-1*}

(* dvd for univariate polynomials *)

(*---------------------------------------------------------------------------------------------

declare [[simp_trace_depth_limit = 99]]

declare [[simp_trace = true]]

//===========================================================================================

  THIS IS THE GOAL as 'function'

===========================================================================================

function (sequential) dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[d] dvd_up [i] =

    (if (\<bar>d\<bar> \<le> \<bar>i\<bar>) & (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 = (lcoeff p) div2 (lcoeff d000);

      rest = drop_lc0 (p minus_up (d000 div_ups quot))

    in 

      if rest = [] then True else 

        if quot \<noteq> 0 & List.length d \<le> List.length rest

        then d dvd_up rest

        else False)"

by pat_completeness auto 

termination sorry

===========================================================================================//

//===========================================================================================

  futile trials

===========================================================================================

THIS PART WORKS:

-------------------------------------------------------------------------------------------

function dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "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 = (lcoeff p) div2 (lcoeff d000);

      rest = drop_lc0 (p minus_up (d000 div_ups quot))

    in 

      if rest = [] then True else 

        if quot \<noteq> 0 & List.length d \<le> List.length rest

        then d dvd_up rest

        else False)"

by pat_completeness auto 

termination sorry

---------------------------------------------------------------------------------------------

THIS PART ONLY WORKS AS 'fun' (because_vvv 'fun' completes the sequence of equations)

---------------------------------------------------------------------------------------------

function dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[d] dvd_up [i] =

    (if (\<bar>d\<bar> \<le> \<bar>i\<bar>) & (i mod d = 0) then True else False)"

by pat_completeness auto 

termination sorry

---------------------------------------------------------------------------------------------

THIS IS THE GOAL as fun

---------------------------------------------------------------------------------------------

fun dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[d] dvd_up [i] =

    (if (\<bar>d\<bar> \<le> \<bar>i\<bar>) & (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 = (lcoeff p) div2 (lcoeff d000);

      rest = drop_lc0 (p minus_up (d000 div_ups quot))

    in 

      if rest = [] then True else 

        if quot \<noteq> 0 & List.length d \<le> List.length rest

        then d dvd_up rest

        else False)"

---------------------------------------------------------------------------------------------

THIS WORKS

---------------------------------------------------------------------------------------------

fun dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[d] dvd_up [i] =

    (if (\<bar>d\<bar> \<le> \<bar>i\<bar>) & (i mod d = 0) then True else False)"

| "d dvd_up p = True"               (*<<<######################################*)

---------------------------------------------------------------------------------------------

THIS WORKS

---------------------------------------------------------------------------------------------

fun dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[d] dvd_up [i] =

    (if (\<bar>d\<bar> \<le> \<bar>i\<bar>) & (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 = (lcoeff p) div2 (lcoeff d000);

      rest = drop_lc0 (p minus_up (d000 div_ups quot))

    in True)"                     (*<<<######################################*)

---------------------------------------------------------------------------------------------

THIS LOOPS

---------------------------------------------------------------------------------------------

function dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[d] dvd_up [i] =

    (if (\<bar>d\<bar> \<le> \<bar>i\<bar>) & (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 = (lcoeff p) div2 (lcoeff d000);

      rest = drop_lc0 (p minus_up (d000 div_ups quot))

    in 

      if rest = [] then True else

      False)"                     (*<<<######################################*)

apply pat_completeness

---------------------------------------------------------------------------------------------

  (sequential) blows up the number of equations; proving compatibility of patterns not simpler:

---------------------------------------------------------------------------------------------

function (sequential) dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[d] dvd_up [i] =

    (if (\<bar>d\<bar> \<le> \<bar>i\<bar>) & (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 = (lcoeff p) div2 (lcoeff d000);

      rest = drop_lc0 (p minus_up (d000 div_ups quot))

    in 

      if rest = [] then True else 

        if quot \<noteq> 0 & List.length d \<le> List.length rest

        then d dvd_up rest

        else False)"

using [[simp_trace_depth_limit = 99]]

using [[simp_trace = true]]

(*separating provers like that: functions.pdf p.10, with (sequential), see functions.pdf p.10*)

apply pat_completeness (*resolves subgoal 1. (out of 16) on 'completeness of patterns',

                         see \<section>3.2 Completeness and Compatibility in Alexander Krauss, Partial Recursive Functions in Higher-Order Logic

                         leaves 15 subgoals on 'compatibility of patterns':

goal (15 subgoals):

 1. \<And>d i da ia. ([d], [i]) = ([da], [ia]) \<Longrightarrow> (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) = (if \<bar>da\<bar> \<le> \<bar>ia\<bar> \<and> ia mod da = 0 then True else False)

 2. \<And>d i p. ([d], [i]) = ([], p) \<Longrightarrow> (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) = (let d = drop_lc0 []; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 3. \<And>d i v vb vc p. ([d], [i]) = (v # vb # vc, p) \<Longrightarrow> (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) = (let d = drop_lc0 (v # vb # vc); p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 4. \<And>d i da. ([d], [i]) = (da, []) \<Longrightarrow> (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) = (let d = drop_lc0 da; p = drop_lc0 []; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 5. \<And>d i da v vb vc. ([d], [i]) = (da, v # vb # vc) \<Longrightarrow> (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) = (let d = drop_lc0 da; p = drop_lc0 (v # vb # vc); d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 6. \<And>p pa. ([], p) = ([], pa) \<Longrightarrow> (let d = drop_lc0 []; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))  in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) = (let d = drop_lc0 []; p = drop_lc0 pa; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 7. \<And>p v vb vc pa. ([], p) = (v # vb # vc, pa) \<Longrightarrow> (let d = drop_lc0 []; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) = (let d = drop_lc0 (v # vb # vc); p = drop_lc0 pa; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 8. \<And>p d. ([], p) = (d, []) \<Longrightarrow> (let d = drop_lc0 []; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) = (let d = drop_lc0 d; p = drop_lc0 []; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 9. \<And>p d v vb vc. ([], p) = (d, v # vb # vc) \<Longrightarrow> (let d = drop_lc0 []; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))  in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) = (let d = drop_lc0 d; p = drop_lc0 (v # vb # vc); d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 10. \<And>v vb vc p va vba vca pa. (v # vb # vc, p) = (va # vba # vca, pa) \<Longrightarrow> (let d = drop_lc0 (v # vb # vc); p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) = (let d = drop_lc0 (va # vba # vca); p = drop_lc0 pa; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

A total of 15 subgoals... *)

(*by auto  ..LOOPS*)

apply simp (*goal (14 subgoals): ^2. = 1. \<And>d i p. ([d], [i]) = ([], p) \<Longrightarrow> *)

apply simp (*goal (13 subgoals): ^3. = 1. \<And>d i v vb vc p. ([d], [i]) = (v # vb # vc, p) \<Longrightarrow> *)

(*apply simp  LOOPS: ^4. \<And>d i da. ([d], [i]) = (da, []) \<Longrightarrow>*)

defer      (*goal (13 subgoals): ^4 = 1. \<And>d i da. ([d], [i]) = (da, []) \<Longrightarrow> *)

apply simp (*goal (12 subgoals): ^5 = 1. \<And>d i da v vb vc. ([d], [i]) = (da, v # vb # vc) \<Longrightarrow> *)

(*apply simp LOOPS*)

defer      (*goal (12 subgoals): ^6 = 1. \<And>p pa. ([], p) = ([], pa) \<Longrightarrow> *)

apply simp (*goal (11 subgoals):  1. \<And>p v vb vc pa. ([], p) = (v # vb # vc, pa) \<Longrightarrow> *)

(*apply simp LOOPS*)

defer

apply simp (*goal (10 subgoals):  1. \<And>p d v vb vc. ([], p) = (d, v # vb # vc) \<Longrightarrow> *)

apply simp (*goal (9 subgoals):  1. \<And>v vb vc p va vba vca pa. (v # vb # vc, p) = (va ..*)

apply simp (*goal (8 subgoals):  1. \<And>v vb vc p d. (v # vb # vc, p) = (d, []) \<Longrightarrow> *)

apply simp (*goal (7 subgoals):  1. \<And>v vb vc p d va vba vca. (v # vb # vc, p) = (d, va ..*)

apply simp (*goal (6 subgoals):  1. \<And>d da. (d, []) = (da, []) \<Longrightarrow> *)

apply simp (*goal (5 subgoals):  1. \<And>d da v vb vc. (d, []) = (da, v # vb # vc) \<Longrightarrow> *)

(*apply simp LOOPS*)

defer

apply simp (*goal (4 subgoals):  1. \<And>d i v vb vc p. ([d], [i]) = (v # vb # vc, p) \<Longrightarrow> *)

(*apply simp LOOPS --- these are the 4 looping subgoals cp from above

*)

sorry

===========================================================================================//

//===========================================================================================

  looking at proof obligations from pattern completeness and pattern compatibility.

===========================================================================================

  separate provers by 'apply'

---------------------------------------------------------------------------------------------

function dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[d] dvd_up [i] =

    (if (\<bar>d\<bar> \<le> \<bar>i\<bar>) & (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 = (lcoeff p) div2 (lcoeff d000);

      rest = drop_lc0 (p minus_up (d000 div_ups quot))

    in 

      if rest = [] then True else 

        if quot \<noteq> 0 & List.length d \<le> List.length rest

        then d dvd_up rest

        else False)"

using [[simp_trace_depth_limit = 99]]

using [[simp_trace = true]]

(*goal (4 subgoals): #1 is completeness of patterns

 1. \<And>P x. (\<And>d i. x = ([d], [i]) \<Longrightarrow> P) \<Longrightarrow> (\<And>d p. x = (d, p) \<Longrightarrow> P) \<Longrightarrow> P

 2. \<And>d i da ia. ([d], [i]) = ([da], [ia]) \<Longrightarrow> (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) = (if \<bar>da\<bar> \<le> \<bar>ia\<bar> \<and> ia mod da = 0 then True else False)

 3. \<And>d i da p. ([d], [i]) = (da, p) \<Longrightarrow> (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) = (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 4. \<And>d p da pa. (d, p) = (da, pa) \<Longrightarrow> (let d = drop_lc0 d; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) = (let d = drop_lc0 da; p = drop_lc0 pa; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) *)

apply pat_completeness 

(*goal (3 subgoals): #1-3 compatibility of patterns

 1. \<And>d i da ia. ([d], [i]) = ([da], [ia]) \<Longrightarrow> (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) = (if \<bar>da\<bar> \<le> \<bar>ia\<bar> \<and> ia mod da = 0 then True else False)

 2. \<And>d i da p. ([d], [i]) = (da, p) \<Longrightarrow> (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) = (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 3. \<And>d p da pa. (d, p) = (da, pa) \<Longrightarrow> (let d = drop_lc0 d; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) = (let d = drop_lc0 da; p = drop_lc0 pa; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) *)

apply simp (*goal (2 subgoals):

 1. \<And>d i da p. ([d], [i]) = (da, p) \<Longrightarrow> (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) = (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 2. \<And>d p da pa. (d, p) = (da, pa) \<Longrightarrow> (let d = drop_lc0 d; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) = (let d = drop_lc0 da; p = drop_lc0 pa; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) *)

(*apply simp   ...LOOPS*)

defer

apply simp (*goal (1 subgoal):   <<<################ this took very long, on the largest subgoa)

goal (1 subgoal):

 1. \<And>d i da p. ([d], [i]) = (da, p) \<Longrightarrow>

               (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) =

               (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))

                in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) 

... this subgoal relates equation 1 and 2, and appears provable only with deep math knowledge.*)

sorry

===========================================================================================//

//===========================================================================================

  The above conclusion about 'not provable' originated from trials in Try_Funktions.thy.

  These trials provided hints on how to complete equations wrt. patterns on the lhs.

===========================================================================================//

//===========================================================================================

  complete sequence of equations wrt. patterns on the lhs.

===========================================================================================

  1st trial --> 4 unsolvable subgoals

-------------------------------------------------------------------------------------------

function dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[] dvd_up [] = False"

| "[] dvd_up p = False"

| "d dvd_up [] = False"

| "[d] dvd_up [i] =

    (if (\<bar>d\<bar> \<le> \<bar>i\<bar>) & (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 = (lcoeff p) div2 (lcoeff d000);

      rest = drop_lc0 (p minus_up (d000 div_ups quot))

    in 

      if rest = [] then True else 

        if quot \<noteq> 0 & List.length d \<le> List.length rest

        then d dvd_up rest

        else False)"

apply pat_completeness

apply simp

apply simp

apply simp

apply simp

(*apply simp*)

defer

apply simp

apply simp

apply simp

(*apply simp*)

defer

apply simp

apply simp

(*apply simp*)

defer

apply simp

(*apply simp*)

defer

apply simp (*this was the last successful apply*)

(*goal (4 subgoals):

 1. \<And>d p. ([], []) = (d, p) \<Longrightarrow>

          False = (let d = drop_lc0 d; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))

                   in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 2. \<And>p d pa. ([], p) = (d, pa) \<Longrightarrow>

             False = (let d = drop_lc0 d; p = drop_lc0 pa; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))

                      in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 3. \<And>d da p. (d, []) = (da, p) \<Longrightarrow>

             False = (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))

                      in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 4. \<And>d i da p. ([d], [i]) = (da, p) \<Longrightarrow>

               (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) =

               (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))

                in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) *)

-------------------------------------------------------------------------------------------

  2nd trial --> 3 unsolvable subgoals on compatiblity of patterns

-------------------------------------------------------------------------------------------

function dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[] dvd_up p = False"

| "d dvd_up [] = False"

| "[d] dvd_up [i] =

    (if (\<bar>d\<bar> \<le> \<bar>i\<bar>) & (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 = (lcoeff p) div2 (lcoeff d000);

      rest = drop_lc0 (p minus_up (d000 div_ups quot))

    in 

      if rest = [] then True else 

        if quot \<noteq> 0 & List.length d \<le> List.length rest

        then d dvd_up rest

        else False)"

apply pat_completeness

apply simp

apply simp

apply simp

defer

apply simp

apply simp

defer

apply simp

defer

apply simp

(*goal (3 subgoals):   ### the 1st subgoals disappears, the others are the same

 1. \<And>p d pa. ([], p) = (d, pa) \<Longrightarrow>

             False = (let d = drop_lc0 d; p = drop_lc0 pa; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))

                      in if rest = [] then True else if quot \<noteq> 0 \<and> replicate length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 2. \<And>d da p. (d, []) = (da, p) \<Longrightarrow>

             False = (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))

                      in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False)

 3. \<And>d i da p. ([d], [i]) = (da, p) \<Longrightarrow>

               (if \<bar>d\<bar> \<le> \<bar>i\<bar> \<and> i mod d = 0 then True else False) =

               (let d = drop_lc0 da; p = drop_lc0 p; d000 = replicate (length p - length d) 0 @ d; quot = lcoeff p div2 lcoeff d000; rest = drop_lc0 (p minus_up (d000 div_ups quot))

                in if rest = [] then True else if quot \<noteq> 0 \<and> length d \<le> length rest then dvd_up_sumC (d, rest) else False) 

---------------------------------------------------------------------------------------------

but completing the sequence of equations doesn't help, 

because the most difficult subgoal (3. above, 4. above above) remains the same.

---------------------------------------------------------------------------------------------

*)

------------------------------GCD_Poly ML-->Isabelle:-------------------------------------------*)

function dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "dvd'_up" 70) where

  "[d] dvd_up [p] =

    (if (\<bar>d\<bar> \<le> \<bar>p\<bar>) & (p mod d = 0) then True else False)"

| "ds dvd_up ps =

    (let 

      ds = drop_lc0 ds; ps = drop_lc0 ps;

      d000 = (List.replicate (List.length ps - List.length ds) 0) @ ds;

      quot = (lcoeff ps) div2 (lcoeff d000);

      rest = drop_lc0 (ps minus_up (d000 mult_ups quot))

    in 

      if rest = [] then True else 

        if quot \<noteq> 0 & List.length ds \<le> List.length rest then ds dvd_up rest else False)"

apply pat_completeness

apply simp

defer

apply simp

(*---------------------------------------------------------------------------------------------

  FINALLY WE HAVE TO SHOW THE COMPATIBILITY OF THE TWO EQUATIONS

 1. \<And>(d\<Colon>int) (p\<Colon>int) (ds\<Colon>int list) ps\<Colon>int list.

       ([d], [p]) = (ds, ps) \<Longrightarrow>

       (if \<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = (0\<Colon>int) then True else False) =

       (let ds\<Colon>int list = drop_lc0 ds; ps\<Colon>int list = drop_lc0 ps;

            d000\<Colon>int list = replicate (length ps - length ds) (0\<Colon>int) @ ds;

            quot\<Colon>int = (lcoeff ps) div2 (lcoeff d000);

            rest\<Colon>int list = drop_lc0 (ps minus_up (d000 mult_ups quot))

        in if rest = [] then True

           else if quot \<noteq> (0\<Colon>int) \<and> length ds \<le> length rest then dvd_up_sumC (ds, rest) else False)

---------------------------------------------------------------------------------------------*)

sorry

(*FINALLY WE HAVE TO SHOW THE COMPATIBILITY OF THE TWO EQUATIONS*)

lemma pat_compatibility:

  fixes d p :: int and ds ps rest :: "unipoly"

  assumes args_equal: "([d], [p]) = (ds, ps)" and not_zero: "d \<noteq> 0 \<and> p \<noteq> 0"

  assumes DELETE: "foo_sumC = body1"

  shows 

   "(if \<bar>d\<bar> \<le> \<bar>p\<bar> \<and> p mod d = 0 then True else False) =

    (let ds = drop_lc0 ds; ps = drop_lc0 ps;

         d000 = replicate (length ps - length ds) (0\<Colon>int) @ ds;

         quot = lcoeff ps div2 lcoeff d000;

         rest = drop_lc0 (ps minus_up (d000 div_ups quot))

     in if rest = [] then True else

          if quot \<noteq> 0 \<and> length ds \<le> length rest then dvd_up_sumC (ds, rest) else False)"

          (* using the assumptions reachable is only ^^^^^^^^^^^^^^^^^^^^^^^ *)

   (is "?body\<^isub>1 = ?body\<^isub>2")

proof -

  have "ds = [d]" and "ps = [p]" using args_equal by auto

    -- "required by hypsubst: assume 'ds = [d] \<Longrightarrow> ps = [p]' creates ((ds = [d] \<Longrightarrow> ps = [p])) \<Longrightarrow>" 

  have simp1_ds: "drop_lc0 [d] = [d]" using not_zero by auto

  have simp1_ps: "drop_lc0 [p] = [p]" using not_zero by auto

  have simp2_body2: "drop_lc0 ([p] minus_up ([d] div_ups quot)) \<noteq> []" sorry

  have simp_body2: "True" sorry

  from `ds = [d]` `ps = [p]` have simp_body2: "?body\<^isub>2 = dvd_up_sumC (ds, rest)"

    proof -

      have "?body\<^isub>2 = 

        (let quot = lcoeff [p] div2 lcoeff [d];

             rest = drop_lc0 ([p] minus_up ([d] div_ups quot))

        in if rest = [] then True else

             if quot \<noteq> 0 \<and> length [d] \<le> length rest then dvd_up_sumC ([d], rest) else False)"

        using `ds = [d]` `ps = [p]` 

        by (hypsubst, subst simp1_ds, subst simp1_ps, simp add: Let_def)

      also have "\<dots> = dvd_up_sumC (ds, rest)" 

        using simp2_body2 

        sorry

      finally show ?thesis .

    qed

  from simp_body2 DELETE show ?thesis sorry

qed

ML {* 1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1*1 *}

(*---------------------------------------------------------------------------------------------

declare [[simp_trace_depth_limit = 99]]

declare [[simp_trace = true]]

lemma trial: 

  assumes "[d] = ds \<Longrightarrow> [p] = ps" 

    and "(let d000 = replicate (length ps - length ds) (0\<Colon>int) @ ds;

              quot = lcoeff ps div2 lcoeff d000;

              rest = drop_lc0 (ps minus_up (d000 div_ups quot))

          in if rest = [] then True else

               if quot \<noteq> (0\<Colon>int) \<and> length ds \<le> length rest then dvd_up_sumC (ds, rest) else False)"

  shows "(let d000 = replicate (length [p] - length [d]) (0\<Colon>int) @ [d];

              quot = lcoeff [p] div2 lcoeff d000;

              rest = drop_lc0 ([p] minus_up (d000 div_ups quot))

         in if rest = [] then True else

             if quot \<noteq> (0\<Colon>int) \<and> length [d] \<le> length rest then dvd_up_sumC ([d], rest) else False)" 

oops

---------------------------------------------------------------------------------------------*)

(*---------------------------------------------------------------------------------------------

(* 

value "[2, 3] dvd_up [8, 22, 15] = True"

... FIXME loops, incorrect: ALL SHOULD EVALUATE TO TRUE .......

*)

value "[4] dvd_up [6]                 = False"

value "[8] dvd_up [16, 0]             = True"

value "[3, 2] dvd_up [0, 0, 9, 12, 4] = True"

value "[8, 0] dvd_up [16]             = True"

(* centr is just local to poly_centr *)

definition centr :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where

  "centr m mid p_i = (if mid < p_i then p_i - m else p_i)"

(* normalise :: poly_centr \<Rightarrow> unipoly => int \<Rightarrow> unipoly

   normalise [p_0, .., p_k] m = [q_0, .., q_k]

     assumes 

     yields 0 \<le> i \<le> k \<Rightarrow> |^ ~m/2 ^| <= q_i <=|^ m/2 ^| 

      (where |^ x ^| means round x up to the next greater integer) *)

definition poly_centr :: "unipoly \<Rightarrow> int \<Rightarrow> unipoly" where

  "poly_centr p m =

   (let

      mi = m div2 2;

      mid = if m mod mi = 0 then mi else mi + 1

   in map (centr m mid) p)"

value "poly_centr [7, 3, 5, 8, 1, 3] 10 = [-3, 3, 5, -2, 1, 3]"

value "poly_centr [1, 2, 3, 4, 5] 2     = [1, 0, 1, 2, 3]"

value "poly_centr [1, 2, 3, 4, 5] 3     = [1, -1, 0, 1, 2]"

value "poly_centr [1, 2, 3, 4, 5] 4     = [1, 2, -1, 0, 1]"

value "poly_centr [1, 2, 3, 4, 5] 5     = [1, 2, 3, -1, 0]"

value "poly_centr [1, 2, 3, 4, 5] 6     = [1, 2, 3, -2, -1]"

value "poly_centr [1, 2, 3, 4, 5] 7     = [1, 2, 3, 4, -2]"

value "poly_centr [1, 2, 3, 4, 5] 8     = [1, 2, 3, 4, -3]"

value "poly_centr [1, 2, 3, 4, 5] 9     = [1, 2, 3, 4, 5]"

value "poly_centr [1, 2, 3, 4, 5] 10    = [1, 2, 3, 4, 5]"

value "poly_centr [1, 2, 3, 4, 5] 11    = [1, 2, 3, 4, 5]"

 (*  sum_lmb :: poly_centr \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int

   sum_lmb [p_0, .., p_k] e = s

     assumes exp >= 0

     yields. p_0^e + p_1^e + ... + p_k^e *)

definition sum_lmb :: "unipoly \<Rightarrow> nat \<Rightarrow> int" where

  "sum_lmb p exp = List.fold ((op +) o (swapf power exp)) p 0"

value "sum_lmb [-1, 2, -3, 4, -5] 1 = -3"

value "sum_lmb [-1, 2, -3, 4, -5] 2 = 55"

value "sum_lmb [-1, 2, -3, 4, -5] 3 = -81"

value "sum_lmb [-1, 2, -3, 4, -5] 4 = 979"

value "sum_lmb [-1, 2, -3, 4, -5] 5 = -2313"

value "sum_lmb [-1, 2, -3, 4, -5] 6 = 20515"

(* LANDAU_MIGNOTTE_bound :: poly_centr \<Rightarrow> unipoly => unipoly \<Rightarrow> int

   LANDAU_MIGNOTTE_bound [a_0, ..., a_m] [b_0, .., b_n] = lmb

     assumes True

     yields lmb = 2^min(m,n) * gcd(a_m,b_n) * 

       min( 1/|a_m| * root(sum_lmb [a_0,...a_m] 2 , 1/|b_n| * root(sum_lmb [b_0,...b_n] 2)*)

definition LANDAU_MIGNOTTE_bound :: "unipoly \<Rightarrow> unipoly \<Rightarrow> nat" where

  "LANDAU_MIGNOTTE_bound p1 p2 =

    ((power 2 (min (deg p1) (deg p2))) * (nat (gcd (lcoeff p1) (lcoeff p2))) * 

    (nat (min (abs ((approx_root (sum_lmb p1 2)) div2 -(lcoeff p1)))

                (abs ((approx_root (sum_lmb p2 2)) div2 -(lcoeff p2))))))"

value "LANDAU_MIGNOTTE_bound [1] [4, 5]          = 1"

value "LANDAU_MIGNOTTE_bound [1, 2] [4, 5]       = 2"

value "LANDAU_MIGNOTTE_bound [1, 2, 3] [4, 5]    = 2"

value "LANDAU_MIGNOTTE_bound [1, 2, 3] [4]       = 1"

value "LANDAU_MIGNOTTE_bound [1, 2, 3] [4, 5]    = 2"

value "LANDAU_MIGNOTTE_bound [1, 2, 3] [4, 5, 6] = 12"

value "LANDAU_MIGNOTTE_bound [-1] [4, 5]            = 1"

value "LANDAU_MIGNOTTE_bound [-1, 2] [4, 5]         = 2"

value "LANDAU_MIGNOTTE_bound [-1, 2, -3] [4, -5]    = 2"

value "LANDAU_MIGNOTTE_bound [-1, 2, -3] [4]        = 1"

value "LANDAU_MIGNOTTE_bound [-1, 2, -3] [4, -5]    = 2"

value "LANDAU_MIGNOTTE_bound [-1, 2, -3] [4, -5, 6] = 12"

subsection {* modulo calculations for polynomials *}

(* pair is just local to chinese_remainder_poly, is "op ~~" in library.ML *)

fun pair :: "unipoly \<Rightarrow> unipoly \<Rightarrow> ((int * int) list)" (infix "pair" 4) where

  "([] pair []) = []"

| "([] pair ys) = []" (*raise ListPair.UnequalLengths*)

| "(xs pair []) = []" (*raise ListPair.UnequalLengths*)

| "((x#xs) pair (y#ys)) = (x, y) # (xs pair ys)"

fun chinese_rem :: "int * int \<Rightarrow> int * int \<Rightarrow> int" where

  "chinese_rem (m1, m2) (p1, p2) = (chinese_remainder p1 m1 p2 m2)"

(* TODO *)

fun chinese_remainder_poly :: "int * int \<Rightarrow> unipoly * unipoly \<Rightarrow> unipoly" where

  "chinese_remainder_poly (m1, m2) (p1, p2) = map (chinese_rem (m1, m2)) (p1 pair p2)"

value "chinese_remainder_poly (5, 7) ([2, 2, 4, 3], [3, 2, 3, 5]) = [17, 2, 24, 33]"

(* mod_pol is just local to mod_poly *)

function mod_pol :: "unipoly \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> unipoly" where

  "mod_pol p m n = (if n < List.length p

      then mod_pol ((List.tl p) @ [(List.hd p) mod m]) m (n + 1)

      else p)"

by auto 

termination sorry

(* TODO *)

definition mod_poly :: "unipoly \<Rightarrow> int \<Rightarrow> unipoly" (infixl "mod'_poly" 70) where

  "p mod_poly m = mod_pol p m 0"

value "[5, 4, 7, 8, 1] mod_poly 5 = [0, 4, 2, 3, 1]"

value "[5, 4, -7, 8, -1] mod_poly 5 = [0, 4, 3, 3, 4]"

(* euclidean algoritm in Z_p[x].

   mod_poly_gcd :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> unipoly

   mod_poly_gcd p1 p2 m = g

     assumes 

     yields  gcd (p1 mod m) (p2 mod m) = g *)

function mod_poly_gcd :: "unipoly \<Rightarrow> unipoly  \<Rightarrow> int \<Rightarrow> unipoly" where

 "mod_poly_gcd p1 p2 m = 

   (let 

      p1m = p1 mod_poly m;

      p2m = drop_lc0 (p2 mod_poly m);

      p2n = (replicate (List.length p1 - List.length p2m) 0) @ p2m;

      quot =  mod_div (lcoeff p1m) (lcoeff p2n) m;

      rest = drop_lc0 ((p1m minus_up (p2n mult_ups quot)) mod_poly m)

    in 

      if rest = [] 

      then p2

      else

        if List.length rest < List.length p2

        then mod_poly_gcd p2 rest m 

        else mod_poly_gcd rest p2 m)"

by auto 

termination sorry

value "mod_poly_gcd [-18, -15, -20, 12, 20, -13, 2] [8, 28, 22, -11, -14, 1, 2] 7 = [2, 6, 0, 2, 6]" 

value "mod_poly_gcd [8, 28, 22, -11, -14, 1, 2] [2, 6, 0, 2, 6] 7 = [2, 6, 0, 2, 6]" 

value "mod_poly_gcd [20, 15, 8, 6] [8, -2, -2, 3] 2 = [0, 1]"

(* analogous to Integer.gcds 

  gcds :: int list \<Rightarrow> int

  gcds ns = d

  assumes True

  yields THE d. ((\<forall>n. List.member ns n \<longrightarrow> d dvd n) \<and>

    (\<forall>d'. (\<forall>n. List.member ns n \<and> d' dvd n) \<longrightarrow> d' \<le> d)) *)

fun gcds :: "int list \<Rightarrow> int" where

  "gcds ns = List.fold gcd ns (List.hd ns)"

value "gcds [6, 9, 12] = 3"

value "gcds [6, -9, 12] = 3"

value "gcds [8, 12, 16] = 4"

value "gcds [-8, 12, -16] = 4"

(* prim_poly :: unipoly \<Rightarrow> unipoly

   prim_poly p = pp

   assumes True

   yields \<forall>p1, p2. (List.member pp p1 \<and> List.member pp p2 \<and> p1 \<noteq> p2) \<longrightarrow> gcd p1 p2 = 1 *)

fun prim_poly :: "unipoly \<Rightarrow> unipoly" where

  "prim_poly [c] = (if c = 0 then [0] else [1])"

| "prim_poly p =

    (let d = gcds p

    in

      if d = 1 then p else p div_ups d)"

value "prim_poly [12, 16, 32, 44] = [3, 4, 8, 11]"

value "prim_poly [4, 5, 12] =  [4, 5, 12]"

value "prim_poly [0] = [0]"

value "prim_poly [6] = [1]"

(*

print_configs

declare [[simp_trace_depth_limit = 99]]

declare [[simp_trace = true]]

using [[simp_trace_depth_limit = 99]]

using [[simp_trace = true]]

*)

---------------------------------------------------------------------------------------------*)

(*---------------------------------------------------------------------------------------------

locale gcd_poly =

  fixes gcd_poly :: int poly -> int poly -> int poly

  assumes gcd_poly p1 p2 = d

    and p1 \<noteq> [:0:] and p2 \<noteq> [:0:]

  ==> d dvd_poly p1  \<and>  d dvd_poly p2  \<and> 

    (\<forall>d'. (d' dvd_poly p1 \<and> d' dvd_poly p2) \<longrightarrow> d' \<le> d)

---------------------------------------------------------------------------------------------*)

end