27 text \<open>these might be used for variants of fac_from_sol\<close> |
27 text \<open>these might be used for variants of fac_from_sol\<close> |
28 ML \<open> |
28 ML \<open> |
29 fun mk_minus_1 T = Free("-1", T); (*TODO DELETE WITH numbers_to_string*) |
29 fun mk_minus_1 T = Free("-1", T); (*TODO DELETE WITH numbers_to_string*) |
30 fun flip_sign t = (*TODO improve for use in factors_from_solution: -(-1) etc*) |
30 fun flip_sign t = (*TODO improve for use in factors_from_solution: -(-1) etc*) |
31 let val minus_1 = t |> type_of |> mk_minus_1 |
31 let val minus_1 = t |> type_of |> mk_minus_1 |
32 in HOLogic.mk_binop "Groups.times_class.times" (minus_1, t) end; |
32 in HOLogic.mk_binop \<^const_name>\<open>times\<close> (minus_1, t) end; |
33 \<close> |
33 \<close> |
34 |
34 |
35 text \<open>from solutions (e.g. [z = 1, z = -2]) make linear factors (e.g. (z - 1)*(z - -2))\<close> |
35 text \<open>from solutions (e.g. [z = 1, z = -2]) make linear factors (e.g. (z - 1)*(z - -2))\<close> |
36 ML \<open> |
36 ML \<open> |
37 fun fac_from_sol s = |
37 fun fac_from_sol s = |
38 let val (lhs, rhs) = HOLogic.dest_eq s |
38 let val (lhs, rhs) = HOLogic.dest_eq s |
39 in HOLogic.mk_binop "Groups.minus_class.minus" (lhs, rhs) end; |
39 in HOLogic.mk_binop \<^const_name>\<open>minus\<close> (lhs, rhs) end; |
40 |
40 |
41 fun mk_prod prod [] = |
41 fun mk_prod prod [] = |
42 if prod = TermC.empty then raise ERROR "mk_prod called with []" else prod |
42 if prod = TermC.empty then raise ERROR "mk_prod called with []" else prod |
43 | mk_prod prod (t :: []) = |
43 | mk_prod prod (t :: []) = |
44 if prod = TermC.empty then t else HOLogic.mk_binop "Groups.times_class.times" (prod, t) |
44 if prod = TermC.empty then t else HOLogic.mk_binop \<^const_name>\<open>times\<close> (prod, t) |
45 | mk_prod prod (t1 :: t2 :: ts) = |
45 | mk_prod prod (t1 :: t2 :: ts) = |
46 if prod = TermC.empty |
46 if prod = TermC.empty |
47 then |
47 then |
48 let val p = HOLogic.mk_binop "Groups.times_class.times" (t1, t2) |
48 let val p = HOLogic.mk_binop \<^const_name>\<open>times\<close> (t1, t2) |
49 in mk_prod p ts end |
49 in mk_prod p ts end |
50 else |
50 else |
51 let val p = HOLogic.mk_binop "Groups.times_class.times" (prod, t1) |
51 let val p = HOLogic.mk_binop \<^const_name>\<open>times\<close> (prod, t1) |
52 in mk_prod p (t2 :: ts) end |
52 in mk_prod p (t2 :: ts) end |
53 |
53 |
54 fun factors_from_solution sol = |
54 fun factors_from_solution sol = |
55 let val ts = HOLogic.dest_list sol |
55 let val ts = HOLogic.dest_list sol |
56 in mk_prod TermC.empty (map fac_from_sol ts) end; |
56 in mk_prod TermC.empty (map fac_from_sol ts) end; |