1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Mon Jan 28 13:58:23 2013 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Tue Jan 29 13:42:00 2013 +0100
     1.3 @@ -294,8 +294,13 @@
     1.4          (if quot \<noteq> 0 & List.length d \<le> List.length rest
     1.5          then d dvd_up rest
     1.6          else False))"
     1.7 -by pat_completeness simp 
     1.8 +using [[simp_trace_depth_limit=999]]
     1.9 +using [[simp_trace=true]]
    1.10 +by pat_completeness auto 
    1.11  termination sorry
    1.12 +
    1.13 +thm dvd_up.simps
    1.14 +thm dvd_up.induct
    1.15  (*
    1.16  value "[2, 3] dvd_up [8, 22, 15]" -- "True"
    1.17  ... loops, incorrect .......
    1.18 @@ -306,4 +311,16 @@
    1.19  value "[8, 0] dvd_up [16]"             -- "True"
    1.20  
    1.21  
    1.22 +(* TEST ON FUNCTION.PDF: USING ABOVE scalar divison *)
    1.23 +function swapfX :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    1.24 +  "swapfX f a b = f b a"
    1.25 +using [[simp_trace_depth_limit=999]]
    1.26 +using [[simp_trace=true]]
    1.27 +by auto
    1.28 +termination sorry
    1.29 +
    1.30 +fun  div_upsX :: "unipoly \<Rightarrow> int \<Rightarrow> unipoly" (infixl "div'_upsX" 70) where
    1.31 +  "p div_upsX m = map (swapfX op div2 m) p"
    1.32 +
    1.33 +
    1.34  end