1.1 --- a/src/HOL/Library/Poly/Collect.thy Mon Feb 03 16:04:26 2014 +0100
1.2 +++ b/src/HOL/Library/Poly/Collect.thy Tue Feb 04 12:41:14 2014 +0100
1.3 @@ -23,11 +23,41 @@
1.4 oops
1.5 (*
1.6 code_datatype Poly_DR Poly_DD
1.7 -*)
1.8 +ERROR: Not a constant: Poly_DR
1.9 +
1.10 +We make some tests below run by ...*)
1.11 +fun Poly_DR :: "'a :: zero poly_dr \<Rightarrow> 'a mpoly"
1.12 +where "Poly_DR p = 0 (*TODO*)"
1.13 +fun Poly_DD :: "'a :: zero poly_dd \<Rightarrow> 'a mpoly"
1.14 +where "Poly_DD p = 0 (*TODO*)"
1.15
1.16 subsection {* Conversion functions between the representations *}
1.17
1.18 -lift_definition ddistr_of_drecur :: "'a :: zero poly_dr \<Rightarrow> 'a poly_dd"
1.19 +lift_definition dd_of_dr :: "'a::zero poly_dr \<Rightarrow> 'a poly_dd"
1.20 is "TODO" oops
1.21
1.22 +lift_definition dr_of_dd :: "'a::zero poly_dd \<Rightarrow> 'a poly_dr"
1.23 +is "TODO" oops
1.24 +
1.25 +(* ... other representations*)
1.26 +
1.27 +(*ERROR: Malformed definition:
1.28 + Non-constructor pattern not allowed
1.29 +??? W"URDE EIN PSEUDO-CONSTRUKTOR HIER AKZEPTIERT ??? --- HACK vvv
1.30 +
1.31 +fun dr_of_some :: "'a :: zero mpoly \<Rightarrow> 'a poly_dr"
1.32 +where
1.33 + "dr_of_some (Poly_DR p) = p"
1.34 +| "dr_of_some (Poly_DD q) = dr_of_dd q"
1.35 +(*| ... other representations*)
1.36 +*)
1.37 +fun dr_of_some :: "'a :: zero mpoly \<Rightarrow> 'a poly_dr" (*HACK ^^^ F"UR Notes.thy*)
1.38 +where "dr_of_some p = 0(*dummy*)"
1.39 +
1.40 +lemma "dr_of_some (Poly_DR p) = normalize_rec p" sorry (*Mail Andreas 02/03/2014 09:41 AM*)
1.41 +lemma "Poly_Rec p (dr_of_some p) = p" sorry (*??? Poly_Rec --^^^^^^^ ???*)
1.42 +
1.43 +fun dd_of_some :: "'a :: zero mpoly \<Rightarrow> 'a poly_dd" (*HACK ^^^ F"UR Notes.thy*)
1.44 +where "dd_of_some p = [](*dummy*)"
1.45 +
1.46 end
2.1 --- a/src/HOL/Library/Poly/Notes.thy Mon Feb 03 16:04:26 2014 +0100
2.2 +++ b/src/HOL/Library/Poly/Notes.thy Tue Feb 04 12:41:14 2014 +0100
2.3 @@ -70,6 +70,7 @@
2.4 take an arbitrary number vor variables into account.
2.5 \item[Evaluation] TODO
2.6 \item[Order] TODO
2.7 + \item[?] leading coefficient, leading term ?
2.8 \end{description}
2.9 *}
2.10
2.11 @@ -190,10 +191,96 @@
2.12 \end{enumerate}
2.13 *}
2.14
2.15 -subsection {* Examples *}
2.16 +subsection {* Application to polynomial algorithms *}
2.17 text {*
2.18 - And that is what the working mathematician has to do:
2.19 - TODO (may wait for answers to Wolfgangs questions after Jan.30)
2.20 + And that is what the working mathematician has to do,
2.21 + when writing polynomial algorithms. Algorithms are finite
2.22 + descriptions comprising executable steps only.
2.23 +*}
2.24 +
2.25 +subsubsection {* Make algorithms executable for code generation *}
2.26 +text {*
2.27 + "Abstract operations" are those defined for @{typ "'a mpoly"}.
2.28 + The following function is an example for the abstract case:
2.29 +*}
2.30 +
2.31 +fun double :: "'a::{zero, plus} mpoly => 'a mpoly"
2.32 + where "double p = p + p"
2.33 +(*export_code double in SML
2.34 +ERROR: No code equations for plus_mpoly_inst.plus_mpoly*)
2.35 +
2.36 +text {*
2.37 + However, trying to generate code for this function by
2.38 + "export_code double in SML"
2.39 + results in an error message
2.40 + "No code equations for plus_mpoly_inst.plus_mpoly"
2.41 + which is no surprise, the message is self-explanatory.
2.42 +
2.43 + In principle there are three variants to provide executable code:
2.44 +
2.45 + Variant (a): implement an algorithm for all representations:
2.46 +*}
2.47 +fun double_dr :: "'a::zero poly_dr \<Rightarrow> 'a poly_dr"
2.48 + where "double_dr p = p (* + p*)"
2.49 +fun double_dd :: "'a::zero poly_dd \<Rightarrow> 'a poly_dd"
2.50 + where "double_dd p = p (* + p*)"
2.51 +
2.52 +lemma [code]:
2.53 + "double (Poly_DR p) = Poly_DR (double_dr p)"
2.54 + "double (Poly_DD q) = Poly_DD (double_dd q)" sorry
2.55 +
2.56 +text {*
2.57 + Variant (b): implement an algorithm for some representations:
2.58 + For representations not implemented the first line below will
2.59 + raise the error "No code equations ..." encountered above.
2.60 +*}
2.61 +lemma [code]:
2.62 + "double p = p (* + p*)"
2.63 + "double (Poly_DR q) = Poly_DR (double_dr q)" sorry
2.64 +
2.65 +text {*
2.66 + Variant (c): implement an algorithms in one representation and
2.67 + convert other representations:
2.68 +*}
2.69 +lemma [code]:
2.70 + "double p = Poly_DR (double_dr (dr_of_some p))" sorry
2.71 +text {*
2.72 + In case
2.73 +*}
2.74 +
2.75 +subsubsection {* Algorithms addressing several representations *}
2.76 +text {*
2.77 + We expect algorithms to use one representation in one part
2.78 + and another representation in another part.
2.79 + Below is an example, where some "algorithm" comprises two parts,
2.80 + where one of them, "algorithm_1_dr", requires one representation and
2.81 + the other, "algorithm_2_dd", requires another:
2.82 +*}
2.83 +fun algorithm_1_dr :: "'a poly_dr \<Rightarrow> 'a poly_dr"
2.84 + where "algorithm_1_dr p = (* algorithm_1 ... *) p"
2.85 +fun algorithm_2_dd :: "'a poly_dd \<Rightarrow> 'a poly_dd"
2.86 + where "algorithm_2_dd p = (* algorithm_2 ... *) p"
2.87 +
2.88 +fun algorithm :: "'a::zero mpoly => 'a mpoly"
2.89 + where
2.90 + "algorithm p =
2.91 + (if Abstract.degree p > 10
2.92 + then algorithm_1_dr (Poly_DR (dr_of_some p))
2.93 + else algorithm_2_dd (Poly_DD (dd_of_some p)))"
2.94 +
2.95 +text {*
2.96 + Actually, the approach used in this example is a generalisation
2.97 + of variant (c) above.
2.98 +
2.99 + WEITER Mail Andreas 02/03/2014 09:41 AM:
2.100 + (i) Vollautomatisch
2.101 + (ii) Halbautomatisch
2.102 + (iii) Manuell
2.103 +*}
2.104 +
2.105 +subsubsection {* TODO *}
2.106 +text {*
2.107 +
2.108 *}
2.109
2.110 end
3.1 --- a/src/HOL/Library/Poly/Rep_Recur_Dense.thy Mon Feb 03 16:04:26 2014 +0100
3.2 +++ b/src/HOL/Library/Poly/Rep_Recur_Dense.thy Tue Feb 04 12:41:14 2014 +0100
3.3 @@ -164,27 +164,44 @@
3.4 typedef 'a poly_dr = "{xs :: 'a::zero list. no_trailing_zero xs}"
3.5 morphisms coeff Abs_poly
3.6 unfolding no_trailing_zero_def by auto
3.7 -(*----GOON---*)
3.8
3.9 +setup_lifting (no_code) type_definition_poly_dr
3.10 +
3.11 +lemma poly_dr_eq_iff: "p = q <-> (coeff p = coeff q)"
3.12 + by (simp add: coeff_inject [symmetric] fun_eq_iff)
3.13 +
3.14 +lemma poly_dr_eqI: "(coeff p = coeff q) ==> p = q"
3.15 + by (simp add: poly_dr_eq_iff)
3.16 +
3.17 +subsection {* The zero polynomial *}
3.18 +
3.19 +instantiation poly_dr :: (zero) zero
3.20 +begin
3.21 +
3.22 +lift_definition zero_poly_dr :: "'a poly_dr"
3.23 + is "[]" sorry
3.24 +
3.25 +instance ..
3.26 +
3.27 +end
3.28
3.29 subsection {* List-style constructor for polynomials *}
3.30
3.31 -(*----GOON---
3.32 -definition pCons :: "'a::zero => 'a poly_dr => 'a poly_dr"
3.33 -where "pCons c p = c ## p"
3.34 -*)
3.35 +lift_definition pCons :: "'a::zero => 'a poly_dr => 'a poly_dr"
3.36 + is "\<lambda>a p. a ## p" sorry
3.37 +
3.38 +lemmas coeff_pCons = pCons.rep_eq
3.39 +
3.40 (*TODO: take and adapt from respective section in HOL/Library/Polynomial.thy*)
3.41
3.42 subsection {* List-style syntax for polynomials *}
3.43
3.44 syntax
3.45 "_mpoly_dr" :: "args => 'a poly_dr" ("[:(_):]")
3.46 -(*
3.47 translations
3.48 "[:x, xs:]" == "CONST pCons x [:xs:]"
3.49 "[:x:]" == "CONST pCons x 0"
3.50 "[:x:]" <= "CONST pCons x (_constrain 0 t)"
3.51 -*)
3.52
3.53 subsection {* Representation of polynomials by lists of coefficients *}
3.54 (*TODO: take and adapt from respective section in HOL/Library/Polynomial.thy*)