955 in |
955 in |
956 Or_to_List e_e)" |
956 Or_to_List e_e)" |
957 |
957 |
958 method met_polyeq_d0 : "PolyEq/solve_d0_polyeq_equation" = |
958 method met_polyeq_d0 : "PolyEq/solve_d0_polyeq_equation" = |
959 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
959 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
960 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
960 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
961 nrls = norm_Rational}\<close> |
961 nrls = norm_Rational}\<close> |
962 Program: solve_poly_equ.simps |
962 Program: solve_poly_equ.simps |
963 Given: "equality e_e" "solveFor v_v" |
963 Given: "equality e_e" "solveFor v_v" |
964 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 0" |
964 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 0" |
965 Find: "solutions v_v'i'" |
965 Find: "solutions v_v'i'" |
976 in |
976 in |
977 Check_elementwise L_L {(v_v::real). Assumptions})" |
977 Check_elementwise L_L {(v_v::real). Assumptions})" |
978 |
978 |
979 method met_polyeq_d1 : "PolyEq/solve_d1_polyeq_equation" = |
979 method met_polyeq_d1 : "PolyEq/solve_d1_polyeq_equation" = |
980 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
980 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
981 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
981 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
982 nrls = norm_Rational}\<close> |
982 nrls = norm_Rational}\<close> |
983 Program: solve_poly_eq1.simps |
983 Program: solve_poly_eq1.simps |
984 Given: "equality e_e" "solveFor v_v" |
984 Given: "equality e_e" "solveFor v_v" |
985 Where: "(lhs e_e) is_poly_in v_v" "((lhs e_e) has_degree_in v_v) = 1" |
985 Where: "(lhs e_e) is_poly_in v_v" "((lhs e_e) has_degree_in v_v) = 1" |
986 Find: "solutions v_v'i'" |
986 Find: "solutions v_v'i'" |
999 in |
999 in |
1000 Check_elementwise L_L {(v_v::real). Assumptions})" |
1000 Check_elementwise L_L {(v_v::real). Assumptions})" |
1001 |
1001 |
1002 method met_polyeq_d22 : "PolyEq/solve_d2_polyeq_equation" = |
1002 method met_polyeq_d22 : "PolyEq/solve_d2_polyeq_equation" = |
1003 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
1003 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
1004 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1004 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1005 nrls = norm_Rational}\<close> |
1005 nrls = norm_Rational}\<close> |
1006 Program: solve_poly_equ2.simps |
1006 Program: solve_poly_equ2.simps |
1007 Given: "equality e_e" "solveFor v_v" |
1007 Given: "equality e_e" "solveFor v_v" |
1008 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2" |
1008 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2" |
1009 Find: "solutions v_v'i'" |
1009 Find: "solutions v_v'i'" |
1022 in |
1022 in |
1023 Check_elementwise L_L {(v_v::real). Assumptions})" |
1023 Check_elementwise L_L {(v_v::real). Assumptions})" |
1024 |
1024 |
1025 method met_polyeq_d2_bdvonly : "PolyEq/solve_d2_polyeq_bdvonly_equation" = |
1025 method met_polyeq_d2_bdvonly : "PolyEq/solve_d2_polyeq_bdvonly_equation" = |
1026 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
1026 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
1027 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1027 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1028 nrls = norm_Rational}\<close> |
1028 nrls = norm_Rational}\<close> |
1029 Program: solve_poly_equ0.simps |
1029 Program: solve_poly_equ0.simps |
1030 Given: "equality e_e" "solveFor v_v" |
1030 Given: "equality e_e" "solveFor v_v" |
1031 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2" |
1031 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2" |
1032 Find: "solutions v_v'i'" |
1032 Find: "solutions v_v'i'" |
1043 in |
1043 in |
1044 Check_elementwise L_L {(v_v::real). Assumptions})" |
1044 Check_elementwise L_L {(v_v::real). Assumptions})" |
1045 |
1045 |
1046 method met_polyeq_d2_sqonly : "PolyEq/solve_d2_polyeq_sqonly_equation" = |
1046 method met_polyeq_d2_sqonly : "PolyEq/solve_d2_polyeq_sqonly_equation" = |
1047 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
1047 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
1048 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1048 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1049 nrls = norm_Rational}\<close> |
1049 nrls = norm_Rational}\<close> |
1050 Program: solve_poly_equ_sqrt.simps |
1050 Program: solve_poly_equ_sqrt.simps |
1051 Given: "equality e_e" "solveFor v_v" |
1051 Given: "equality e_e" "solveFor v_v" |
1052 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2" |
1052 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2" |
1053 Find: "solutions v_v'i'" |
1053 Find: "solutions v_v'i'" |
1064 in |
1064 in |
1065 Check_elementwise L_L {(v_v::real). Assumptions})" |
1065 Check_elementwise L_L {(v_v::real). Assumptions})" |
1066 |
1066 |
1067 method met_polyeq_d2_pq : "PolyEq/solve_d2_polyeq_pq_equation" = |
1067 method met_polyeq_d2_pq : "PolyEq/solve_d2_polyeq_pq_equation" = |
1068 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
1068 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
1069 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1069 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1070 nrls = norm_Rational}\<close> |
1070 nrls = norm_Rational}\<close> |
1071 Program: solve_poly_equ_pq.simps |
1071 Program: solve_poly_equ_pq.simps |
1072 Given: "equality e_e" "solveFor v_v" |
1072 Given: "equality e_e" "solveFor v_v" |
1073 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2" |
1073 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2" |
1074 Find: "solutions v_v'i'" |
1074 Find: "solutions v_v'i'" |
1084 L_L = Or_to_List e_e |
1084 L_L = Or_to_List e_e |
1085 in Check_elementwise L_L {(v_v::real). Assumptions})" |
1085 in Check_elementwise L_L {(v_v::real). Assumptions})" |
1086 |
1086 |
1087 method met_polyeq_d2_abc : "PolyEq/solve_d2_polyeq_abc_equation" = |
1087 method met_polyeq_d2_abc : "PolyEq/solve_d2_polyeq_abc_equation" = |
1088 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls,srls=Rule_Set.empty, prls=PolyEq_prls, |
1088 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls,srls=Rule_Set.empty, prls=PolyEq_prls, |
1089 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1089 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1090 nrls = norm_Rational}\<close> |
1090 nrls = norm_Rational}\<close> |
1091 Program: solve_poly_equ_abc.simps |
1091 Program: solve_poly_equ_abc.simps |
1092 Given: "equality e_e" "solveFor v_v" |
1092 Given: "equality e_e" "solveFor v_v" |
1093 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2" |
1093 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 2" |
1094 Find: "solutions v_v'i'" |
1094 Find: "solutions v_v'i'" |
1109 in |
1109 in |
1110 Check_elementwise L_L {(v_v::real). Assumptions})" |
1110 Check_elementwise L_L {(v_v::real). Assumptions})" |
1111 |
1111 |
1112 method met_polyeq_d3 : "PolyEq/solve_d3_polyeq_equation" = |
1112 method met_polyeq_d3 : "PolyEq/solve_d3_polyeq_equation" = |
1113 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
1113 \<open>{rew_ord'="termlessI", rls'=PolyEq_erls, srls=Rule_Set.empty, prls=PolyEq_prls, |
1114 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1114 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1115 nrls = norm_Rational}\<close> |
1115 nrls = norm_Rational}\<close> |
1116 Program: solve_poly_equ3.simps |
1116 Program: solve_poly_equ3.simps |
1117 Given: "equality e_e" "solveFor v_v" |
1117 Given: "equality e_e" "solveFor v_v" |
1118 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 3" |
1118 Where: "(lhs e_e) is_poly_in v_v " "((lhs e_e) has_degree_in v_v) = 3" |
1119 Find: "solutions v_v'i'" |
1119 Find: "solutions v_v'i'" |
1138 in |
1138 in |
1139 Or_to_List e_e)" |
1139 Or_to_List e_e)" |
1140 |
1140 |
1141 method met_polyeq_complsq : "PolyEq/complete_square" = |
1141 method met_polyeq_complsq : "PolyEq/complete_square" = |
1142 \<open>{rew_ord'="termlessI",rls'=PolyEq_erls,srls=Rule_Set.empty,prls=PolyEq_prls, |
1142 \<open>{rew_ord'="termlessI",rls'=PolyEq_erls,srls=Rule_Set.empty,prls=PolyEq_prls, |
1143 calc=[("sqrt", ("NthRoot.sqrt", eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1143 calc=[("sqrt", (\<^const_name>\<open>sqrt\<close>, eval_sqrt "#sqrt_"))], crls=PolyEq_crls, errpats = [], |
1144 nrls = norm_Rational}\<close> |
1144 nrls = norm_Rational}\<close> |
1145 Program: solve_by_completing_square.simps |
1145 Program: solve_by_completing_square.simps |
1146 Given: "equality e_e" "solveFor v_v" |
1146 Given: "equality e_e" "solveFor v_v" |
1147 Where: "matches (?a = 0) e_e" "((lhs e_e) has_degree_in v_v) = 2" |
1147 Where: "matches (?a = 0) e_e" "((lhs e_e) has_degree_in v_v) = 2" |
1148 Find: "solutions v_v'i'" |
1148 Find: "solutions v_v'i'" |
1165 | dest_hd' _ (Var v) = (v, 2) |
1165 | dest_hd' _ (Var v) = (v, 2) |
1166 | dest_hd' _ (Bound i) = ((("", i), dummyT), 3) |
1166 | dest_hd' _ (Bound i) = ((("", i), dummyT), 3) |
1167 | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4) |
1167 | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4) |
1168 | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def."; |
1168 | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def."; |
1169 |
1169 |
1170 fun size_of_term' x (Const ("Transcendental.powr",_) $ Free (var,_) $ Free (pot,_)) = |
1170 fun size_of_term' x (Const (\<^const_name>\<open>powr\<close>,_) $ Free (var,_) $ Free (pot,_)) = |
1171 (case x of (*WN*) |
1171 (case x of (*WN*) |
1172 (Free (xstr,_)) => |
1172 (Free (xstr,_)) => |
1173 (if xstr = var then 1000*(the (TermC.int_opt_of_string pot)) else 3) |
1173 (if xstr = var then 1000*(the (TermC.int_opt_of_string pot)) else 3) |
1174 | _ => raise ERROR ("size_of_term' called with subst = "^ |
1174 | _ => raise ERROR ("size_of_term' called with subst = "^ |
1175 (UnparseC.term x))) |
1175 (UnparseC.term x))) |