1.1 --- a/Try_Polynomial.thy Mon Feb 02 17:00:07 2015 +0100
1.2 +++ b/Try_Polynomial.thy Tue Dec 01 08:38:45 2015 +0100
1.3 @@ -1676,10 +1676,12 @@
1.4 (if (! trace_div2)
1.5 then
1.6 writeln ("a = " ^ PolyML.makestring a ^
1.7 - ", (m', n) = (" ^ PolyML.makestring m' ^ ", " ^ PolyML.makestring n ^ ")" ^
1.8 + ", (m', n) = fact_quot " ^ PolyML.makestring (coeff' (pCons a r) (degree q)) ^
1.9 + " " ^ PolyML.makestring (coeff' q (degree q)) ^
1.10 + " = (" ^ PolyML.makestring m' ^ ", " ^ PolyML.makestring n ^ ")" ^
1.11 ", s: " ^ PolyML.makestring s ^ " --> " ^ PolyML.makestring (pCons n (smult' m' s)) ^
1.12 ", r: " ^ PolyML.makestring r ^ " --> " ^
1.13 - PolyML.makestring (smult' m' (pCons (a*m) r) --- smult' n q))
1.14 + PolyML.makestring (smult' m' (pCons (a * m) r) --- smult' n q))
1.15 else ()
1.16 ;
1.17 if drop' (degree (drop_tl_zeros' (smult' m p)) - (degree (drop_tl_zeros' ((s *** q) +++ r))))
1.18 @@ -1692,9 +1694,8 @@
1.19 " <> " ^ PolyML.makestring (drop_tl_zeros' ((s *** q) +++ r)))
1.20 )
1.21 *} ML {*
1.22 -val p = Poly [9, 8, 7, 6, 5, 4]
1.23 -val q = Poly [1, 2, 3];
1.24 -*} ML {*
1.25 +val p = (*Poly [9, 8, 7, 6, 5, 4]*) Poly [2,2,2, 2,2,2];
1.26 +val q = (*Poly [1, 2, 3]; *) Poly [7,8,6];
1.27 (* 1-1 translation from Prep_Transparent.div_int_up not possible ++ required analysis of pdivmod *)
1.28 fun yyyyy2 a ((m, s), r) =
1.29 let
1.30 @@ -1705,7 +1706,7 @@
1.31 smult' m' (pCons (a * m) r) --- smult' n q)
1.32 end
1.33 *} ML {*
1.34 -val ((m, q'), r) = fold_coeffs yyyyy2 p ((1, Poly []), Poly []) (* <<<<<<<<<<<-------------------*)
1.35 +val ((m, q'), r) = fold_coeffs yyyyy2 p ((1, Poly []), Poly []) (* <<<<<<<<<<<-----GOOON------*)
1.36 val _ = if drop_tl_zeros' (smult' m p) = drop_tl_zeros' ((q' *** q) +++ r)
1.37 then () else writeln "invariant broken";
1.38 (*
2.1 --- a/Try_Recursive.thy Mon Feb 02 17:00:07 2015 +0100
2.2 +++ b/Try_Recursive.thy Tue Dec 01 08:38:45 2015 +0100
2.3 @@ -2,7 +2,7 @@
2.4
2.5 theory Try_Recursive
2.6 imports "~/repos/poly-WORK/Poly_Demo" "~/repos/mle-try-WORK/Try_Recursive_Construct"
2.7 - "~~/src/HOL/Main"
2.8 + "~~/src/HOL/Main" "~/repos/poly-WORK/Test"
2.9 begin
2.10
2.11 section {* trials with current versions *}
2.12 @@ -130,8 +130,8 @@
2.13 subsection {* Monomials *}
2.14
2.15 definition p013 :: "int mpoly" --{* recursive dense *}
2.16 -where "p013 = monom' (REC (\<lambda>_. DENSE)) (Nat_Mapping.single' DENSE 0 1) 2 +
2.17 - monom' (REC (\<lambda>_. DENSE)) (Nat_Mapping.single' DENSE 2 4) 3"
2.18 +where "p013 = monom' (REC DENSE) (Nat_Mapping.single' DENSE 0 1) 2 +
2.19 + monom' (REC DENSE) (Nat_Mapping.single' DENSE 2 4) 3"
2.20
2.21 value "p013" --{* def.Poly_Demo
2.22 "Rec (Powers (Dense (Abs_nat_mapping_dense
2.23 @@ -316,10 +316,10 @@
2.24 term "inc_power_rec" --{**}
2.25 (*"Rec (Coeff 3)" does NOT carry information about DENSE | SPARSE*)
2.26 definition p0013 :: "int mpoly" --{* recursive dense *}
2.27 -where "p0013 = monom' (REC (\<lambda>_. DENSE)) (Nat_Mapping.single' DENSE 0 0) 3"
2.28 +where "p0013 = monom' (REC DENSE) (Nat_Mapping.single' DENSE 0 0) 3"
2.29 value "p0013" --{*"Rec (Coeff 3)" :: "int mpoly"*}
2.30 definition p0014 :: "int mpoly" --{* recursive sparse *}
2.31 -where "p0014 = monom' (REC (\<lambda>_. SPARSE)) (Nat_Mapping.single' DENSE 0 0) 3"
2.32 +where "p0014 = monom' (REC SPARSE) (Nat_Mapping.single' DENSE 0 0) 3"
2.33 value "p0014" --{*"Rec (Coeff 3)" :: "int mpoly"*}
2.34
2.35 (*code_datatype Rec
2.36 @@ -634,6 +634,61 @@
2.37 *}
2.38
2.39 subsection {* Long division of polynomials *}
2.40 +subsubsection {* Pseudo division --- preliminarily only univariate case *}
2.41 +
2.42 +value "gcd"
2.43 +value "gcd 8 6 ::int" --{* = 2 *}
2.44 +value "Divides.div_class.div 6 3"
2.45 +value "Divides.div_class.div 6 3 ::int" --{* = 2 *}
2.46 +
2.47 +(* \<longrightarrow> Recursive.thy *)
2.48 +definition fact_quot :: "('a::{ring_div,ord,gcd}) \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
2.49 + where
2.50 + "fact_quot c1 c2 =
2.51 + (let d = gcd c1 c2; n = Divides.div_class.div c2 d; q = Divides.div_class.div c1 d
2.52 + in if n > 0 then (n, q) else (-1 * n, -1 * q))"
2.53 +
2.54 +value "fact_quot 6 (4::int)" --{* = "(2, 3)"*}
2.55 +
2.56 +(* \<longrightarrow> Recursive.thy *)
2.57 +(* pdivmod_raw p1 p2 = ((n, q), r) --result meets the signature of foldr
2.58 + assumes p2 \<noteq> 0 \<and> deg p1 \<ge> deg p2
2.59 + yields smult_rec n p1 = q * p2 + r
2.60 +*)
2.61 +fun pdivmod_raw :: "('a::zero) poly_rec \<Rightarrow> 'a poly_rec \<Rightarrow> ('a \<times> 'a poly_rec) \<times> 'a poly_rec"
2.62 +where
2.63 + "pdivmod_raw p1 p2 = (if p2 = 0 then ((0, 0), p1)
2.64 + else fold_coeffs (\<lambda>a ((m, s), r).
2.65 + let (m', n) = fact_quot (coeff (pCons a r)
2.66 + (degree_rec 0 p2)) (coeff p2 (degree_rec p2 0))
2.67 +
2.68 + in ((if m' = 0 then m else m * m', pCons n (smult_rec m' s)),
2.69 + smult_rec m' (pCons (a * m) r) - smult n p2)
2.70 + ) p1 ((1, 0), 0))"
2.71 +
2.72 +term "smult_rec" --{*:: "'a \<Rightarrow> 'a poly_rec \<Rightarrow> 'a poly_rec"*}
2.73 +term "xxx" --{**}
2.74 +
2.75 +(* THIS DEFINITION CANNOT BE USED FOR BOTTOM UP CODING ...*)
2.76 +definition p1002003_rec :: "('a::{zero,numeral}) poly_rec" --{* recursive dense *}
2.77 +where "p1002003_rec = (Powers (Dense (Abs_nat_mapping_dense
2.78 + [Coeff 1, Coeff 0, Coeff 0, Coeff 2, Coeff 0, Coeff 0, Coeff 3])))" --{*:: "'a poly_rec"*}
2.79 +(*value "p1002003_rec" --{*Abstraction violation: Abs_nat_mapping_dense*}
2.80 + THIS INHIBITS TO CONSTRUCT poly_rec BYPASSING THE TYPE-SYSTEM *)
2.81 +term "degree_rec" --{*:: "'a poly_rec \<Rightarrow> nat \<Rightarrow> nat"*}
2.82 +term "degree_rec p1002003_rec 0" --{**}
2.83 +(*value "degree_rec p1002003_rec 0" --{*Abstraction violation: Abs_nat_mapping_dense*}
2.84 + THIS INHIBITS TO CONSTRUCT poly_rec BYPASSING THE TYPE-SYSTEM *)
2.85 +term "xxx" --{**}
2.86 +term "xxx" --{**}
2.87 +term "Nat_Mapping.mapp" --{*:: "(nat \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> (\<nat> \<Rightarrow>\<^sub>0 'a) \<Rightarrow> \<nat> \<Rightarrow>\<^sub>0 'b"*}
2.88 +term "xxx" --{**}
2.89 +term "foldr" --{**}
2.90 +term "xxx" --{**}
2.91 +term "xxx" --{**}
2.92 +term "xxx" --{**}
2.93 +term "xxx" --{**}
2.94 +term "xxx" --{**}
2.95
2.96 section {* trials with version 304aa715e1a7: the naive start ---> Intro_140623.thy *}
2.97
3.1 --- a/Try_Test.thy Mon Feb 02 17:00:07 2015 +0100
3.2 +++ b/Try_Test.thy Tue Dec 01 08:38:45 2015 +0100
3.3 @@ -7,9 +7,9 @@
3.4 subsection {* Recursive dense multiplication *}
3.5 subsubsection {* (z-z) OK check times (4.z^3) (3.x^2.y^2.z^2) *}
3.6 definition p3x_2y_2z_2 :: "int mpoly" --{*= 3.x^2.y^2.z^2 *}
3.7 -where "p3x_2y_2z_2 = monom' (REC (\<lambda>_. DENSE)) (Nat_Mapping.single' DENSE 0 2) 1 *(*!!!*)
3.8 - monom' (REC (\<lambda>_. DENSE)) (Nat_Mapping.single' DENSE 1 2) 1 *(*!!!*)
3.9 - monom' (REC (\<lambda>_. DENSE)) (Nat_Mapping.single' DENSE 2 2) 3"
3.10 +where "p3x_2y_2z_2 = monom' (REC DENSE) (Nat_Mapping.single' DENSE 0 2) 1 *(*!!!*)
3.11 + monom' (REC DENSE) (Nat_Mapping.single' DENSE 1 2) 1 *(*!!!*)
3.12 + monom' (REC DENSE) (Nat_Mapping.single' DENSE 2 2) 3"
3.13 value p3x_2y_2z_2 --{*"Rec (Powers (Dense (Abs_nat_mapping_dense [ (* (R[x,y])[z] *)
3.14 Coeff 0, Coeff 0, * (* z^0.0 + z^1.0 + *)
3.15 Powers (Dense (Abs_nat_mapping_dense [ (* z^2.(... ) *)
3.16 @@ -18,7 +18,7 @@
3.17 Coeff 0, Coeff 0, Coeff 3]))]))])))" (* (x^0.0 + x^1.0 + x^2.3) *)
3.18 = z^2.y^2. x^2.3 *}
3.19 definition p4z_3 :: "int mpoly" --{*= 4.z^3 *}
3.20 -where "p4z_3 = monom' (REC (\<lambda>_. DENSE)) (Nat_Mapping.single' DENSE 0 3) 4"
3.21 +where "p4z_3 = monom' (REC DENSE) (Nat_Mapping.single' DENSE 0 3) 4"
3.22 value p4z_3 --{*"Rec (Powers (Dense (Abs_nat_mapping_dense [
3.23 Coeff 0, Coeff 0, Coeff 0, Coeff 4])))"
3.24 = z^3.4 *}
3.25 @@ -32,7 +32,7 @@
3.26
3.27 subsubsection {* (z-y) OK check times (4.y^3) (3.x^2.y^2.z^2) *}
3.28 definition p4y_3 :: "int mpoly" --{* = 4.y^3 *}
3.29 -where "p4y_3 = monom' (REC (\<lambda>_. DENSE)) (Nat_Mapping.single' DENSE 1 3) 4"
3.30 +where "p4y_3 = monom' (REC DENSE) (Nat_Mapping.single' DENSE 1 3) 4"
3.31 value p4y_3 --{*"Rec (Powers (Dense (Abs_nat_mapping_dense [
3.32 Powers (Dense (Abs_nat_mapping_dense [ (* z^0.(... ) *)
3.33 Coeff 0, Coeff 0, Coeff 0, Coeff 4]))])))" (* (y^0.0 + y^1.0 + y^2.0 + y^3.4) *)
3.34 @@ -47,7 +47,7 @@
3.35
3.36 subsubsection {* (z-x) OK check times (4.x^3) (3.x^2.y^2.z^2) *}
3.37 definition p4x_3 :: "int mpoly" --{* = 4.x^3 *}
3.38 -where "p4x_3 = monom' (REC (\<lambda>_. DENSE)) (Nat_Mapping.single' DENSE 2 3) 4"
3.39 +where "p4x_3 = monom' (REC DENSE) (Nat_Mapping.single' DENSE 2 3) 4"
3.40 value p4x_3 --{*"Rec (Powers (Dense (Abs_nat_mapping_dense [
3.41 Powers (Dense (Abs_nat_mapping_dense [ (* z^0.(... )*)
3.42 Powers (Dense (Abs_nat_mapping_dense [ (* y^0.(... ) *)