equal
deleted
inserted
replaced
10 theory Polynomial |
10 theory Polynomial |
11 imports Main "~~/src/HOL/Deriv" "~~/src/HOL/Library/More_List" |
11 imports Main "~~/src/HOL/Deriv" "~~/src/HOL/Library/More_List" |
12 "~~/src/HOL/Library/Infinite_Set" |
12 "~~/src/HOL/Library/Infinite_Set" |
13 begin |
13 begin |
14 |
14 |
15 subsection \<open>Misc\<close> |
|
16 |
|
17 lemma quotient_of_denom_pos': "snd (quotient_of x) > 0" |
|
18 using quotient_of_denom_pos [OF surjective_pairing] . |
|
19 |
|
20 lemma (in idom_divide) of_int_divide_in_Ints: |
|
21 "of_int a div of_int b \<in> \<int>" if "b dvd a" |
|
22 proof - |
|
23 from that obtain c where "a = b * c" .. |
|
24 then show ?thesis |
|
25 by (cases "of_int b = 0") simp_all |
|
26 qed |
|
27 |
|
28 |
|
29 subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close> |
15 subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close> |
30 |
16 |
31 definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "##" 65) |
17 definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "##" 65) |
32 where |
18 where |
33 "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)" |
19 "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)" |