255 (*data from above - M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!)-:*) |
255 (*data from above - M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!)-:*) |
256 (*the model-pattern, O_Model.is_copy_named are filter_out*) |
256 (*the model-pattern, O_Model.is_copy_named are filter_out*) |
257 val pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})), |
257 val pbt = [("#Given", (@{term "equality"}, @{term "e_e :: bool"})), |
258 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))]; |
258 ("#Given", (@{term "solveFor"}, @{term "v_v :: real"} ))]; |
259 (*the model specific for an example*) |
259 (*the model specific for an example*) |
260 val oris = [([1], "#Given", @{term "equality"} , [TermC.str2term "x+1= 2"]), |
260 val oris = [([1], "#Given", @{term "equality"} , [TermC.parse_test @{context} "x+1= 2"]), |
261 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])]; |
261 ([1], "#Given", @{term "solveFor"} , [@{term "x :: real"} ])]; |
262 val cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))]; |
262 val cy = [("#Find", (@{term "solutions"}, @{term "v_v'i' :: bool list"}))]; |
263 (*...all must be true*) |
263 (*...all must be true*) |
264 |
264 |
265 case O_Model.copy_name pbt oris (hd cy) of |
265 case O_Model.copy_name pbt oris (hd cy) of |
272 @{term "solution"}; type_of @{term "ss''' :: bool list"}; |
272 @{term "solution"}; type_of @{term "ss''' :: bool list"}; |
273 (*the model-pattern for ["LINEAR", "system"], O_Model.is_copy_named are filter_out*) |
273 (*the model-pattern for ["LINEAR", "system"], O_Model.is_copy_named are filter_out*) |
274 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})), |
274 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})), |
275 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))]; |
275 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))]; |
276 (*the model specific for an example*) |
276 (*the model specific for an example*) |
277 val oris = [([1], "#Given", @{term "equalities"} ,[TermC.str2term "[x_1+1=2,x_2=0]"]), |
277 val oris = [([1], "#Given", @{term "equalities"} ,[TermC.parse_test @{context} "[x_1+1=2,x_2=0]"]), |
278 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])]; |
278 ([1], "#Given", @{term "solveForVars"} , [@{term "[x_1,x_2]::real list"}])]; |
279 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"})) |
279 val cy = [("#Find", (@{term "solution"}, @{term "ss''' :: bool list"})) |
280 (*could be more than 1*)]; |
280 (*could be more than 1*)]; |
281 |
281 |
282 case O_Model.copy_name pbt oris (hd cy) of |
282 case O_Model.copy_name pbt oris (hd cy) of |