338 \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""), |
338 \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""), |
339 \<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*) |
339 \<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*) |
340 \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*) |
340 \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*) |
341 \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*) |
341 \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*) |
342 \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close> |
342 \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close> |
343 Method: "simplification/for_polynomials/with_minus" |
343 Method_Ref: "simplification/for_polynomials/with_minus" |
344 CAS: "Vereinfache t_t" |
344 CAS: "Vereinfache t_t" |
345 Given: "Term t_t" |
345 Given: "Term t_t" |
346 Where: |
346 Where: |
347 "t_t is_polyexp" |
347 "t_t is_polyexp" |
348 "Not (matchsub (?a + (?b + ?c)) t_t | |
348 "Not (matchsub (?a + (?b + ?c)) t_t | |
361 \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""), |
361 \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""), |
362 \<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*) |
362 \<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*) |
363 \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*) |
363 \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*) |
364 \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*) |
364 \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*) |
365 \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close> |
365 \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close> |
366 Method: "simplification/for_polynomials/with_parentheses" |
366 Method_Ref: "simplification/for_polynomials/with_parentheses" |
367 CAS: "Vereinfache t_t" |
367 CAS: "Vereinfache t_t" |
368 Given: "Term t_t" |
368 Given: "Term t_t" |
369 Where: |
369 Where: |
370 "t_t is_polyexp" |
370 "t_t is_polyexp" |
371 "Not (matchsub (?a * (?b + ?c)) t_t | |
371 "Not (matchsub (?a * (?b + ?c)) t_t | |
375 Find: "normalform n_n" |
375 Find: "normalform n_n" |
376 |
376 |
377 problem pbl_vereinf_poly_klammer_mal : "binom_klammer/polynom/vereinfachen" = |
377 problem pbl_vereinf_poly_klammer_mal : "binom_klammer/polynom/vereinfachen" = |
378 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*) |
378 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*) |
379 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close> |
379 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close> |
380 Method: "simplification/for_polynomials/with_parentheses_mult" |
380 Method_Ref: "simplification/for_polynomials/with_parentheses_mult" |
381 CAS: "Vereinfache t_t" |
381 CAS: "Vereinfache t_t" |
382 Given: "Term t_t" |
382 Given: "Term t_t" |
383 Where: "t_t is_polyexp" |
383 Where: "t_t is_polyexp" |
384 Find: "normalform n_n" |
384 Find: "normalform n_n" |
385 |
385 |
386 problem pbl_probe : "probe" = \<open>Rule_Set.Empty\<close> |
386 problem pbl_probe : "probe" = \<open>Rule_Set.Empty\<close> |
387 |
387 |
388 problem pbl_probe_poly : "polynom/probe" = |
388 problem pbl_probe_poly : "polynom/probe" = |
389 \<open>Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*) |
389 \<open>Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*) |
390 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close> |
390 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close> |
391 Method: "probe/fuer_polynom" |
391 Method_Ref: "probe/fuer_polynom" |
392 CAS: "Probe e_e w_w" |
392 CAS: "Probe e_e w_w" |
393 Given: "Pruefe e_e" "mitWert w_w" |
393 Given: "Pruefe e_e" "mitWert w_w" |
394 Where: "e_e is_polyexp" |
394 Where: "e_e is_polyexp" |
395 Find: "Geprueft p_p" |
395 Find: "Geprueft p_p" |
396 |
396 |
397 problem pbl_probe_bruch : "bruch/probe" = |
397 problem pbl_probe_bruch : "bruch/probe" = |
398 \<open>Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*) |
398 \<open>Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*) |
399 \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")]\<close> |
399 \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")]\<close> |
400 Method: "probe/fuer_bruch" |
400 Method_Ref: "probe/fuer_bruch" |
401 CAS: "Probe e_e w_w" |
401 CAS: "Probe e_e w_w" |
402 Given: "Pruefe e_e" "mitWert w_w" |
402 Given: "Pruefe e_e" "mitWert w_w" |
403 Where: "e_e is_ratpolyexp" |
403 Where: "e_e is_ratpolyexp" |
404 Find: "Geprueft p_p" |
404 Find: "Geprueft p_p" |
405 |
405 |