1.1 --- a/src/HOL/Library/Poly_Represent/Polynomial2.thy Mon Dec 23 16:35:24 2013 +0100
1.2 +++ b/src/HOL/Library/Poly_Represent/Polynomial2.thy Fri Dec 27 17:16:44 2013 +0100
1.3 @@ -1,7 +1,7 @@
1.4 (* Title: HOL/Library/Poly_Represent/Polynomial.thy
1.5 Author: Walther Neuper, following ideas of Andreas Lochbihler
1.6 *)
1.7 -header {* Sparse distributive representation of polynomials *}
1.8 +header {* Collect representations of Poly_Abstract.thy *}
1.9
1.10 theory Polynomial2
1.11 imports "~~/src/HOL/Library/Phantom_Type"
1.12 @@ -11,26 +11,88 @@
1.13 "~~/src/HOL/Library/Poly_Represent/Poly_Dist_Sparse"
1.14 begin
1.15
1.16 +section {* Last trial *}
1.17 +ML {*
1.18 +
1.19 +datatype 'a poly = Poly of 'a list
1.20 +
1.21 +
1.22 +*}
1.23 +
1.24 +(* abstractions from the representations *)
1.25 +datatype 'a poly =
1.26 + Poly_Rec "'a poly_rec" |
1.27 + Poly_Rec2 "'a mpoly" |
1.28 +(*Poly_Dense "'a poly_dense" | *)
1.29 + Poly_Sparse "'a poly_sparse"
1.30 +
1.31 +(* conversion functions preliminarily just for zero:
1.32 + THE CONVERSIONS ARE DIFFERENT FROM THE SUGGESTED ONES,
1.33 + because 'a Poly_Abstract.poly doesn't have any representation.
1.34 +
1.35 +MAIN PROBLEM: 'a Polynomial2.poly SHOULD BE Poly_Abstract.poly ...
1.36 +==================================================================*)
1.37 +
1.38 +fun recursive_of :: "'a::zero Polynomial2.poly \<Rightarrow> 'a poly_rec"
1.39 +where
1.40 + "recursive_of (Poly_Rec p) = p" |
1.41 + "recursive_of (Poly_Rec2 p) = 0 (*TODO*)" |
1.42 +(*"recursive_of (Poly_Dense p) = ..." | *)
1.43 + "recursive_of (Poly_Sparse p) = 0 (*TODO*)"
1.44 +
1.45 +(*fun recursive2_of :: "'a::zero Polynomial2.poly \<Rightarrow> 'a mpoly"
1.46 +where
1.47 + "recursive2_of (Poly_Rec p) = ..." |
1.48 + "recursive2_of (Poly_Rec2 p) = p" |
1.49 + "recursive2_of (Poly_Dense p) = ..." |
1.50 + "recursive2_of (Poly_Sparse p) = ..." ...ERROR: Clash of types "_ MPoly" and "_ mpoly"*)
1.51 +
1.52 +(*fun dense_of :: "'a::zero Polynomial2.poly \<Rightarrow> 'a poly_dense"
1.53 + ... ...ERROR: Undeclared type constructor: "poly_dense"
1.54 +*)
1.55 +fun sparse_of :: "'a::zero Polynomial2.poly \<Rightarrow> 'a poly_sparse"
1.56 +where
1.57 + "sparse_of (Poly_Rec p) = [] (*TODO*)" |
1.58 + "sparse_of (Poly_Rec2 p) = [] (*TODO*)" |
1.59 +(*"sparse_of (Poly_Dense p) = ..." | *)
1.60 + "sparse_of (Poly_Sparse p) = p"
1.61 +
1.62 +(* determine representation at the beginning of an algorithm *)
1.63 +lemma algo_code [code]: "algo p = algo_sparse (sparse_of p)" sorry
1.64 +lemma algo_code' [code]: "algo p = Poly_Sparse (algo_sparse (sparse_of p))" sorry
1.65 +
1.66 +(* determine representation within an algorithm *)
1.67 +lemma algo2_code [code]: "algo p =
1.68 + (if a = b then Poly_Sparse (sparse_of p) else Poly_Dense (dense_of p))" sorry
1.69 +
1.70 +section {* Previous trial *}
1.71 subsection {* Abstraction over representations *}
1.72
1.73 datatype 'a represent =
1.74 - Poly_Rec "'a poly_rec \<Rightarrow> 'a Poly_Abstract.poly" |
1.75 - Poly_Rec2 "'a mpoly \<Rightarrow> 'a Poly_Abstract.poly" |
1.76 -(*Poly_Dense "'a poly_dense \<Rightarrow> 'a Poly_Abstract.poly" | *)
1.77 - Poly_Sparse "'a poly_sparse \<Rightarrow> 'a Poly_Abstract.poly"
1.78 + Poly2_Rec "'a poly_rec \<Rightarrow> 'a Poly_Abstract.poly" |
1.79 + Poly2_Rec2 "'a mpoly \<Rightarrow> 'a Poly_Abstract.poly" |
1.80 +(*Poly2_Dense "'a poly_dense \<Rightarrow> 'a Poly_Abstract.poly" | *)
1.81 + Poly2_Sparse "'a poly_sparse \<Rightarrow> 'a Poly_Abstract.poly"
1.82
1.83 -code_datatype Poly_Rec Poly_Rec2 (*Poly_Dense*) Poly_Sparse
1.84 +code_datatype Poly2_Rec Poly2_Rec2 (*Poly2_Dense*) Poly2_Sparse
1.85
1.86 subsection {* Code setup for the representations *}
1.87
1.88 subsection {* Conversion functions *}
1.89 -term "Const 0" --{*"Const 0" :: "'a MPoly"*}
1.90 -term "Poly_Rec2" --{**}
1.91 +(* renamed in order to avoid ERRO: Duplicate constant declaration *)
1.92 +definition recursive_of2 :: "'a::zero Poly_Abstract.poly \<Rightarrow> 'a poly_rec"
1.93 +where "recursive_of2 p = (0 :: 'a poly_rec)"
1.94 +(*
1.95 +definition recursive2_of :: "'a::zero poly \<Rightarrow> 'a mpoly"
1.96 +where "recursive2_of p = (Const 0 :: 'a mpoly)" ...ERROR: Clash of types "_ MPoly" and "_ mpoly"
1.97
1.98 -(*
1.99 -lemma sparse_of_rec1 [code]: "sparse_of_rec1 (Poly_Rec (Const 0)) = Poly_Sparse (\<lambda>_. 0)" sorry
1.100 +definition dense_of :: "'a poly \<Rightarrow> 'a poly_dense"
1.101 +where "dense_of p = ([] :: 'a poly_dense)" ...ERROR: Undeclared type constructor: "poly_dense"
1.102 *)
1.103 -(*
1.104 +definition sparse_of2 :: "'a Poly_Abstract.poly \<Rightarrow> 'a poly_sparse"
1.105 +where "sparse_of2 p = ([] :: 'a poly_sparse)"
1.106 +
1.107 +(* SUGGESTION:
1.108 recursive_of :: "'a poly => 'a poly_rec"
1.109 sparse_of :: "'a poly => 'a poly_sparse"
1.110 dense_of :: "'a poly => 'a poly_dense"
1.111 @@ -39,10 +101,11 @@
1.112
1.113 subsection {* Dummy examples for algorithms with variable*}
1.114
1.115 -lemma algo_code [code]: "algo p = algo_sparse (sparse_of p)" sorry
1.116 -lemma algo_code' [code]: "algo p = Poly_Sparse (algo_sparse (sparse_of p))" sorry
1.117 +(* determine representation at the beginning of an algorithm *)
1.118 +lemma algo_code2 [code]: "algo p = algo_sparse (sparse_of2 p)" sorry
1.119 +lemma algo_code2' [code]: "algo p = Poly2_Sparse (algo_sparse (sparse_of p))" sorry
1.120
1.121 -subsection {* A previous trial *}
1.122 +section {* The initial trial *}
1.123
1.124 datatype ('a, 'b) phantom = phantom 'b
1.125
1.126 @@ -55,4 +118,5 @@
1.127
1.128 code_datatype poly_Recursive poly_Distrib_Sparse poly_Distrib_Dense
1.129
1.130 +
1.131 end