322 erls = Rule_Def.Repeat { |
322 erls = Rule_Def.Repeat { |
323 id="erls_prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
323 id="erls_prls_triangular", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
324 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
324 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
325 rules = [(*for precond NTH_CONS ...*) |
325 rules = [(*for precond NTH_CONS ...*) |
326 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
326 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
327 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
327 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
328 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")], |
328 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")], |
329 (*immediately repeated rewrite pushes '+' into precondition !*) |
329 (*immediately repeated rewrite pushes '+' into precondition !*) |
330 scr = Rule.Empty_Prog}, |
330 scr = Rule.Empty_Prog}, |
331 srls = Rule_Set.Empty, calc = [], errpatts = [], |
331 srls = Rule_Set.Empty, calc = [], errpatts = [], |
332 rules = [ |
332 rules = [ |
333 \<^rule_thm>\<open>NTH_CONS\<close>, |
333 \<^rule_thm>\<open>NTH_CONS\<close>, |
334 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
334 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
335 \<^rule_thm>\<open>NTH_NIL\<close>, |
335 \<^rule_thm>\<open>NTH_NIL\<close>, |
336 \<^rule_thm>\<open>tl_Cons\<close>, |
336 \<^rule_thm>\<open>tl_Cons\<close>, |
337 \<^rule_thm>\<open>tl_Nil\<close>, |
337 \<^rule_thm>\<open>tl_Nil\<close>, |
338 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")], |
338 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")], |
339 scr = Rule.Empty_Prog}; |
339 scr = Rule.Empty_Prog}; |
348 erls = Rule_Def.Repeat { |
348 erls = Rule_Def.Repeat { |
349 id="erls_prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
349 id="erls_prls_triangular4", preconds = [], rew_ord = ("Rewrite_Ord.id_empty", Rewrite_Ord.function_empty), |
350 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
350 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
351 rules = [(*for precond NTH_CONS ...*) |
351 rules = [(*for precond NTH_CONS ...*) |
352 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
352 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
353 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_")], |
353 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_")], |
354 (*immediately repeated rewrite pushes '+' into precondition !*) |
354 (*immediately repeated rewrite pushes '+' into precondition !*) |
355 scr = Rule.Empty_Prog}, |
355 scr = Rule.Empty_Prog}, |
356 srls = Rule_Set.Empty, calc = [], errpatts = [], |
356 srls = Rule_Set.Empty, calc = [], errpatts = [], |
357 rules = [ |
357 rules = [ |
358 \<^rule_thm>\<open>NTH_CONS\<close>, |
358 \<^rule_thm>\<open>NTH_CONS\<close>, |
359 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
359 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
360 \<^rule_thm>\<open>NTH_NIL\<close>, |
360 \<^rule_thm>\<open>NTH_NIL\<close>, |
361 \<^rule_thm>\<open>tl_Cons\<close>, |
361 \<^rule_thm>\<open>tl_Cons\<close>, |
362 \<^rule_thm>\<open>tl_Nil\<close>, |
362 \<^rule_thm>\<open>tl_Nil\<close>, |
363 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")], |
363 \<^rule_eval>\<open>occur_exactly_in\<close> (eval_occur_exactly_in "#eval_occur_exactly_in_")], |
364 scr = Rule.Empty_Prog}; |
364 scr = Rule.Empty_Prog}; |
392 |
392 |
393 problem pbl_equsys_lin_2x2: "2x2/LINEAR/system" = |
393 problem pbl_equsys_lin_2x2: "2x2/LINEAR/system" = |
394 \<open>Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty |
394 \<open>Rule_Set.append_rules "prls_2x2_linear_system" Rule_Set.empty |
395 [\<^rule_thm>\<open>LENGTH_CONS\<close>, |
395 [\<^rule_thm>\<open>LENGTH_CONS\<close>, |
396 \<^rule_thm>\<open>LENGTH_NIL\<close>, |
396 \<^rule_thm>\<open>LENGTH_NIL\<close>, |
397 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
397 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
398 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close> |
398 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close> |
399 CAS: "solveSystem e_s v_s" |
399 CAS: "solveSystem e_s v_s" |
400 Given: "equalities e_s" "solveForVars v_s" |
400 Given: "equalities e_s" "solveForVars v_s" |
401 Where: "Length (e_s:: bool list) = 2" "Length v_s = 2" |
401 Where: "Length (e_s:: bool list) = 2" "Length v_s = 2" |
402 Find: "solution ss'''" |
402 Find: "solution ss'''" |
420 |
420 |
421 problem pbl_equsys_lin_3x3 : "3x3/LINEAR/system" = |
421 problem pbl_equsys_lin_3x3 : "3x3/LINEAR/system" = |
422 \<open>Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty |
422 \<open>Rule_Set.append_rules "prls_3x3_linear_system" Rule_Set.empty |
423 [\<^rule_thm>\<open>LENGTH_CONS\<close>, |
423 [\<^rule_thm>\<open>LENGTH_CONS\<close>, |
424 \<^rule_thm>\<open>LENGTH_NIL\<close>, |
424 \<^rule_thm>\<open>LENGTH_NIL\<close>, |
425 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
425 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
426 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close> |
426 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close> |
427 CAS: "solveSystem e_s v_s" |
427 CAS: "solveSystem e_s v_s" |
428 Given: "equalities e_s" "solveForVars v_s" |
428 Given: "equalities e_s" "solveForVars v_s" |
429 Where: "Length (e_s:: bool list) = 3" "Length v_s = 3" |
429 Where: "Length (e_s:: bool list) = 3" "Length v_s = 3" |
430 Find: "solution ss'''" |
430 Find: "solution ss'''" |
431 |
431 |
432 problem pbl_equsys_lin_4x4 : "4x4/LINEAR/system" = |
432 problem pbl_equsys_lin_4x4 : "4x4/LINEAR/system" = |
433 \<open>Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty |
433 \<open>Rule_Set.append_rules "prls_4x4_linear_system" Rule_Set.empty |
434 [\<^rule_thm>\<open>LENGTH_CONS\<close>, |
434 [\<^rule_thm>\<open>LENGTH_CONS\<close>, |
435 \<^rule_thm>\<open>LENGTH_NIL\<close>, |
435 \<^rule_thm>\<open>LENGTH_NIL\<close>, |
436 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
436 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
437 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close> |
437 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_")]\<close> |
438 CAS: "solveSystem e_s v_s" |
438 CAS: "solveSystem e_s v_s" |
439 Given: "equalities e_s" "solveForVars v_s" |
439 Given: "equalities e_s" "solveForVars v_s" |
440 Where: "Length (e_s:: bool list) = 4" "Length v_s = 4" |
440 Where: "Length (e_s:: bool list) = 4" "Length v_s = 4" |
441 Find: "solution ss'''" |
441 Find: "solution ss'''" |
468 rew_ord = ("termlessI",termlessI), |
468 rew_ord = ("termlessI",termlessI), |
469 erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty |
469 erls = Rule_Set.append_rules "erls_in_srls_IntegrierenUnd.." Rule_Set.empty |
470 [(*for asm in NTH_CONS ...*) |
470 [(*for asm in NTH_CONS ...*) |
471 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
471 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"), |
472 (*2nd NTH_CONS pushes n+-1 into asms*) |
472 (*2nd NTH_CONS pushes n+-1 into asms*) |
473 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_") |
473 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_") |
474 ], |
474 ], |
475 srls = Rule_Set.Empty, calc = [], errpatts = [], |
475 srls = Rule_Set.Empty, calc = [], errpatts = [], |
476 rules = [\<^rule_thm>\<open>NTH_CONS\<close>, |
476 rules = [\<^rule_thm>\<open>NTH_CONS\<close>, |
477 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"), |
477 \<^rule_eval>\<open>plus\<close> (**)(Calc_Binop.numeric "#add_"), |
478 \<^rule_thm>\<open>NTH_NIL\<close>], |
478 \<^rule_thm>\<open>NTH_NIL\<close>], |
479 scr = Rule.Empty_Prog}; |
479 scr = Rule.Empty_Prog}; |
480 \<close> |
480 \<close> |
481 |
481 |
482 section \<open>Methods\<close> |
482 section \<open>Methods\<close> |