[isabelle] Prooving the existence of a splitting field



Hi people,

I'm trying to prove, that for every univariate polynomial has a splitting field i.e. a field where the polynomial factors completely into linear factors. At first it's okay, if this field isn't the smallest field with that property. I'm using the HOL/Algebra library (and version Isabelle2013-1) and have already proved several useful lemmas. I defined term "field extension" this way

locale field_extension =
fixes L::"('a, 'n) ring_scheme" (structure) and K::"('b, 'm) ring_scheme"
and iota::"'b => 'a"
assumes field_L[intro, simp]: "field L"
and field_K[intro, simp]: "field K"
and hom[intro, simp]: "iota ? ring_hom K L"

furthermore I could prove this theorem

theorem extension_with_zero:
fixes K::"'b ring" and p
assumes "field K"
and "p ? carrier (UP K)"
and "deg K p ~= 0"
shows "?(L?(nat ? 'b) set ring). ?iota. ?x ? carrier L. field_extension L K ? ? eval K L iota x p = zero L"

That shows that you can find a field in which the polynomial has at least one root. Next you could use long division to reduce the polynomial and repeat the process until you have a field which contains every root of the polynomial. That would be a solution...

Now the problem:
Isabelle forces me to specify the type of the object which existence I want to show. Unfortunately the field I get from the theorem from above has another "bigger" type than the field I'm starting with. If you want to repeat the process you had to know the number of repetitions you make, but that varies with the polynomial.

Has anyone an idea or a solution?

Best wishes
Markus

and a happy new year :-)



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.