(* attempts to perserve binary minus as wanted by Austrian teachers

   WN071207

   (c) due to copyright terms

*)

theory PolyMinus imports (*Poly// due to "is_ratpolyexp" in...*) Rational begin

consts

  (*predicates for conditions in rewriting*)

  kleiner     :: "['a, 'a] => bool" 	("_ kleiner _") 

  ist'_monom  :: "'a => bool"		("_ ist'_monom")

  (*the CAS-command*)

  Probe       :: "[bool, bool list] => bool"  

	(*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*)

  (*descriptions for the pbl and met*)

  Pruefe      :: "bool => una"

  mitWert     :: "bool list => tobooll"

  Geprueft    :: "bool => una"

  (*Script-name*)

  ProbeScript :: "[bool, bool list,       bool] 

				      => bool"

                  ("((Script ProbeScript (_ _ =))// (_))" 9)

axioms

  null_minus:            "0 - a = -a"

  vor_minus_mal:         "- a * b = (-a) * b"

  (*commute with invariant (a.b).c -association*)

  tausche_plus:		"[| b ist_monom; a kleiner b  |] ==> 

			 (b + a) = (a + b)"

  tausche_minus:		"[| b ist_monom; a kleiner b  |] ==> 

			 (b - a) = (-a + b)"

  tausche_vor_plus:	"[| b ist_monom; a kleiner b  |] ==> 

			 (- b + a) = (a - b)"

  tausche_vor_minus:	"[| b ist_monom; a kleiner b  |] ==> 

			 (- b - a) = (-a - b)"

  tausche_plus_plus:	"b kleiner c ==> (a + c + b) = (a + b + c)"

  tausche_plus_minus:	"b kleiner c ==> (a + c - b) = (a - b + c)"

  tausche_minus_plus:	"b kleiner c ==> (a - c + b) = (a + b - c)"

  tausche_minus_minus:	"b kleiner c ==> (a - c - b) = (a - b - c)"

  (*commute with invariant (a.b).c -association*)

  tausche_mal:		"[| b is_atom; a kleiner b  |] ==> 

			 (b * a) = (a * b)"

  tausche_vor_mal:	"[| b is_atom; a kleiner b  |] ==> 

			 (-b * a) = (-a * b)"

  tausche_mal_mal:	"[| c is_atom; b kleiner c  |] ==> 

			 (x * c * b) = (x * b * c)"

  x_quadrat:             "(x * a) * a = x * a ^^^ 2"

  subtrahiere:               "[| l is_const; m is_const |] ==>  

			     m * v - l * v = (m - l) * v"

  subtrahiere_von_1:         "[| l is_const |] ==>  

			     v - l * v = (1 - l) * v"

  subtrahiere_1:             "[| l is_const; m is_const |] ==>  

			     m * v - v = (m - 1) * v"

  subtrahiere_x_plus_minus:  "[| l is_const; m is_const |] ==>  

			     (x + m * v) - l * v = x + (m - l) * v"

  subtrahiere_x_plus1_minus: "[| l is_const |] ==>  

			     (x + v) - l * v = x + (1 - l) * v"

  subtrahiere_x_plus_minus1: "[| m is_const |] ==>  

			     (x + m * v) - v = x + (m - 1) * v"

  subtrahiere_x_minus_plus:  "[| l is_const; m is_const |] ==>  

			     (x - m * v) + l * v = x + (-m + l) * v"

  subtrahiere_x_minus1_plus: "[| l is_const |] ==>  

			     (x - v) + l * v = x + (-1 + l) * v"

  subtrahiere_x_minus_plus1: "[| m is_const |] ==>  

			     (x - m * v) + v = x + (-m + 1) * v"

  subtrahiere_x_minus_minus: "[| l is_const; m is_const |] ==>  

			     (x - m * v) - l * v = x + (-m - l) * v"

  subtrahiere_x_minus1_minus:"[| l is_const |] ==>  

			     (x - v) - l * v = x + (-1 - l) * v"

  subtrahiere_x_minus_minus1:"[| m is_const |] ==>  

			     (x - m * v) - v = x + (-m - 1) * v"

  addiere_vor_minus:         "[| l is_const; m is_const |] ==>  

			     - (l * v) +  m * v = (-l + m) * v"

  addiere_eins_vor_minus:    "[| m is_const |] ==>  

			     -  v +  m * v = (-1 + m) * v"

  subtrahiere_vor_minus:     "[| l is_const; m is_const |] ==>  

			     - (l * v) -  m * v = (-l - m) * v"

  subtrahiere_eins_vor_minus:"[| m is_const |] ==>  

			     -  v -  m * v = (-1 - m) * v"

  vorzeichen_minus_weg1:      "l kleiner 0 ==> a + l * b = a - -1*l * b"

  vorzeichen_minus_weg2:      "l kleiner 0 ==> a - l * b = a + -1*l * b"

  vorzeichen_minus_weg3:      "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"

  vorzeichen_minus_weg4:      "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"

  (*klammer_plus_plus = (add_assoc RS sym)*)

  klammer_plus_minus:          "a + (b - c) = (a + b) - c"

  klammer_minus_plus:          "a - (b + c) = (a - b) - c"

  klammer_minus_minus:         "a - (b - c) = (a - b) + c"

  klammer_mult_minus:          "a * (b - c) = a * b - a * c"

  klammer_minus_mult:          "(b - c) * a = b * a - c * a"

ML {*

val thy = @{theory};

(** eval functions **)

(*. get the identifier from specific monomials; see fun ist_monom .*)

(*HACK.WN080107*)

fun increase str = 

    let val s::ss = explode str

    in implode ((chr (ord s + 1))::ss) end;

fun identifier (Free (id,_)) = id                            (* 2,   a   *)

  | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) = 

    id                                                       (* 2*a, a*b *)

  | identifier (Const ("Groups.times_class.times", _) $                          (* 3*a*b    *)

		     (Const ("Groups.times_class.times", _) $

			    Free (num, _) $ Free _) $ Free (id, _)) = 

    if is_numeral num then id

    else "|||||||||||||"

  | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =

    if is_numeral base then "|||||||||||||"                  (* a^2      *)

    else (*increase*) base

  | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $          (* 3*a^2    *)

		     (Const ("Atools.pow", _) $

			    Free (base, _) $ Free (exp, _))) = 

    if is_numeral num andalso not (is_numeral base) then (*increase*) base

    else "|||||||||||||"

  | identifier _ = "|||||||||||||"(*the "largest" string*);

(*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)

(* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)

fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _  =

     if is_num b then

	 if is_num a then (*123 kleiner 32 = True !!!*)

	     if int_of_Free a < int_of_Free b then 

		 SOME ((term2str p) ^ " = True",

		       Trueprop $ (mk_equality (p, HOLogic.true_const)))

	     else SOME ((term2str p) ^ " = False",

			Trueprop $ (mk_equality (p, HOLogic.false_const)))

	 else (* -1 * -2 kleiner 0 *)

	     SOME ((term2str p) ^ " = False",

		   Trueprop $ (mk_equality (p, HOLogic.false_const)))

    else

	if identifier a < identifier b then 

	     SOME ((term2str p) ^ " = True",

		  Trueprop $ (mk_equality (p, HOLogic.true_const)))

	else SOME ((term2str p) ^ " = False",

		   Trueprop $ (mk_equality (p, HOLogic.false_const)))

  | eval_kleiner _ _ _ _ =  NONE;

fun ist_monom (Free (id,_)) = true

  | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) = 

    if is_numeral num then true else false

  | ist_monom _ = false;

(*. this function only accepts the most simple monoms       vvvvvvvvvv .*)

fun ist_monom (Free (id,_)) = true                          (* 2,   a   *)

  | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)

    if is_numeral id then false else true

  | ist_monom (Const ("Groups.times_class.times", _) $                          (* 3*a*b    *)

		     (Const ("Groups.times_class.times", _) $

			    Free (num, _) $ Free _) $ Free (id, _)) =

    if is_numeral num andalso not (is_numeral id) then true else false

  | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) = 

    true                                                    (* a^2      *)

  | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $          (* 3*a^2    *)

		     (Const ("Atools.pow", _) $

			    Free (base, _) $ Free (exp, _))) = 

    if is_numeral num then true else false

  | ist_monom _ = false;

(* is this a univariate monomial ? *)

(*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)

fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _  =

    if ist_monom a  then 

	SOME ((term2str p) ^ " = True",

	      Trueprop $ (mk_equality (p, HOLogic.true_const)))

    else SOME ((term2str p) ^ " = False",

	       Trueprop $ (mk_equality (p, HOLogic.false_const)))

  | eval_ist_monom _ _ _ _ =  NONE;

(** rewrite order **)

(** rulesets **)

val erls_ordne_alphabetisch =

    append_rls "erls_ordne_alphabetisch" e_rls

	       [Calc ("PolyMinus.kleiner", eval_kleiner ""),

		Calc ("PolyMinus.ist'_monom", eval_ist_monom "")

		];

val ordne_alphabetisch = 

  Rls{id = "ordne_alphabetisch", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],

      erls = erls_ordne_alphabetisch, 

      rules = [Thm ("tausche_plus",num_str @{thm tausche_plus}),

	       (*"b kleiner a ==> (b + a) = (a + b)"*)

	       Thm ("tausche_minus",num_str @{thm tausche_minus}),

	       (*"b kleiner a ==> (b - a) = (-a + b)"*)

	       Thm ("tausche_vor_plus",num_str @{thm tausche_vor_plus}),

	       (*"[| b ist_monom; a kleiner b  |] ==> (- b + a) = (a - b)"*)

	       Thm ("tausche_vor_minus",num_str @{thm tausche_vor_minus}),

	       (*"[| b ist_monom; a kleiner b  |] ==> (- b - a) = (-a - b)"*)

	       Thm ("tausche_plus_plus",num_str @{thm tausche_plus_plus}),

	       (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)

	       Thm ("tausche_plus_minus",num_str @{thm tausche_plus_minus}),

	       (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)

	       Thm ("tausche_minus_plus",num_str @{thm tausche_minus_plus}),

	       (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)

	       Thm ("tausche_minus_minus",num_str @{thm tausche_minus_minus})

	       (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)

	       ], scr = EmptyScr}:rls;

val fasse_zusammen = 

    Rls{id = "fasse_zusammen", preconds = [], 

	rew_ord = ("dummy_ord", dummy_ord),

	erls = append_rls "erls_fasse_zusammen" e_rls 

			  [Calc ("Atools.is'_const",eval_const "#is_const_")], 

	srls = Erls, calc = [],

	rules = 

	[Thm ("real_num_collect",num_str @{thm real_num_collect}), 

	 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)

	 Thm ("real_num_collect_assoc_r",num_str @{thm real_num_collect_assoc_r}),

	 (*"[| l is_const; m..|] ==>  (k + m * n) + l * n = k + (l + m)*n"*)

	 Thm ("real_one_collect",num_str @{thm real_one_collect}),	

	 (*"m is_const ==> n + m * n = (1 + m) * n"*)

	 Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}), 

	 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)

	 Thm ("subtrahiere",num_str @{thm subtrahiere}),

	 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)

	 Thm ("subtrahiere_von_1",num_str @{thm subtrahiere_von_1}),

	 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)

	 Thm ("subtrahiere_1",num_str @{thm subtrahiere_1}),

	 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)

	 Thm ("subtrahiere_x_plus_minus",num_str @{thm subtrahiere_x_plus_minus}), 

	 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)

	 Thm ("subtrahiere_x_plus1_minus",num_str @{thm subtrahiere_x_plus1_minus}),

	 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)

	 Thm ("subtrahiere_x_plus_minus1",num_str @{thm subtrahiere_x_plus_minus1}),

	 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)

	 Thm ("subtrahiere_x_minus_plus",num_str @{thm subtrahiere_x_minus_plus}), 

	 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)

	 Thm ("subtrahiere_x_minus1_plus",num_str @{thm subtrahiere_x_minus1_plus}),

	 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)

	 Thm ("subtrahiere_x_minus_plus1",num_str @{thm subtrahiere_x_minus_plus1}),

	 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)

	 Thm ("subtrahiere_x_minus_minus",num_str @{thm subtrahiere_x_minus_minus}), 

	 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)

	 Thm ("subtrahiere_x_minus1_minus",num_str @{thm subtrahiere_x_minus1_minus}),

	 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)

	 Thm ("subtrahiere_x_minus_minus1",num_str @{thm subtrahiere_x_minus_minus1}),

	 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)

	 Calc ("Groups.plus_class.plus", eval_binop "#add_"),

	 Calc ("Groups.minus_class.minus", eval_binop "#subtr_"),

	 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen

           (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)

	 Thm ("real_mult_2_assoc_r",num_str @{thm real_mult_2_assoc_r}),

	 (*"(k + z1) + z1 = k + 2 * z1"*)

	 Thm ("sym_real_mult_2",num_str (@{thm real_mult_2} RS @{thm sym})),

	 (*"z1 + z1 = 2 * z1"*)

	 Thm ("addiere_vor_minus",num_str @{thm addiere_vor_minus}),

	 (*"[| l is_const; m is_const |] ==> -(l * v) +  m * v = (-l + m) *v"*)

	 Thm ("addiere_eins_vor_minus",num_str @{thm addiere_eins_vor_minus}),

	 (*"[| m is_const |] ==> -  v +  m * v = (-1 + m) * v"*)

	 Thm ("subtrahiere_vor_minus",num_str @{thm subtrahiere_vor_minus}),

	 (*"[| l is_const; m is_const |] ==> -(l * v) -  m * v = (-l - m) *v"*)

	 Thm ("subtrahiere_eins_vor_minus",num_str @{thm subtrahiere_eins_vor_minus})

	 (*"[| m is_const |] ==> -  v -  m * v = (-1 - m) * v"*)

	 ], scr = EmptyScr}:rls;

val verschoenere = 

  Rls{id = "verschoenere", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],

      erls = append_rls "erls_verschoenere" e_rls 

			[Calc ("PolyMinus.kleiner", eval_kleiner "")], 

      rules = [Thm ("vorzeichen_minus_weg1",num_str @{thm vorzeichen_minus_weg1}),

	       (*"l kleiner 0 ==> a + l * b = a - -l * b"*)

	       Thm ("vorzeichen_minus_weg2",num_str @{thm vorzeichen_minus_weg2}),

	       (*"l kleiner 0 ==> a - l * b = a + -l * b"*)

	       Thm ("vorzeichen_minus_weg3",num_str @{thm vorzeichen_minus_weg3}),

	       (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)

	       Thm ("vorzeichen_minus_weg4",num_str @{thm vorzeichen_minus_weg4}),

	       (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)

	       Calc ("Groups.times_class.times", eval_binop "#mult_"),

	       Thm ("mult_zero_left",num_str @{thm mult_zero_left}),    

	       (*"0 * z = 0"*)

	       Thm ("mult_1_left",num_str @{thm mult_1_left}),     

	       (*"1 * z = z"*)

	       Thm ("add_0_left",num_str @{thm add_0_left}),

	       (*"0 + z = z"*)

	       Thm ("null_minus",num_str @{thm null_minus}),

	       (*"0 - a = -a"*)

	       Thm ("vor_minus_mal",num_str @{thm vor_minus_mal})

	       (*"- a * b = (-a) * b"*)

	       (*Thm ("",num_str @{}),*)

	       (**)

	       ], scr = EmptyScr}:rls (*end verschoenere*);

val klammern_aufloesen = 

  Rls{id = "klammern_aufloesen", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls, 

      rules = [Thm ("sym_add_assoc",

                     num_str (@{thm add_assoc} RS @{thm sym})),

	       (*"a + (b + c) = (a + b) + c"*)

	       Thm ("klammer_plus_minus",num_str @{thm klammer_plus_minus}),

	       (*"a + (b - c) = (a + b) - c"*)

	       Thm ("klammer_minus_plus",num_str @{thm klammer_minus_plus}),

	       (*"a - (b + c) = (a - b) - c"*)

	       Thm ("klammer_minus_minus",num_str @{thm klammer_minus_minus})

	       (*"a - (b - c) = (a - b) + c"*)

	       ], scr = EmptyScr}:rls;

val klammern_ausmultiplizieren = 

  Rls{id = "klammern_ausmultiplizieren", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls, 

      rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),

	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)

	       Thm ("right_distrib",num_str @{thm right_distrib}),

	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)

	       Thm ("klammer_mult_minus",num_str @{thm klammer_mult_minus}),

	       (*"a * (b - c) = a * b - a * c"*)

	       Thm ("klammer_minus_mult",num_str @{thm klammer_minus_mult})

	       (*"(b - c) * a = b * a - c * a"*)

	       (*Thm ("",num_str @{}),

	       (*""*)*)

	       ], scr = EmptyScr}:rls;

val ordne_monome = 

  Rls{id = "ordne_monome", preconds = [], 

      rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], 

      erls = append_rls "erls_ordne_monome" e_rls

	       [Calc ("PolyMinus.kleiner", eval_kleiner ""),

		Calc ("Atools.is'_atom", eval_is_atom "")

		], 

      rules = [Thm ("tausche_mal",num_str @{thm tausche_mal}),

	       (*"[| b is_atom; a kleiner b  |] ==> (b * a) = (a * b)"*)

	       Thm ("tausche_vor_mal",num_str @{thm tausche_vor_mal}),

	       (*"[| b is_atom; a kleiner b  |] ==> (-b * a) = (-a * b)"*)

	       Thm ("tausche_mal_mal",num_str @{thm tausche_mal_mal}),

	       (*"[| c is_atom; b kleiner c  |] ==> (a * c * b) = (a * b *c)"*)

	       Thm ("x_quadrat",num_str @{thm x_quadrat})

	       (*"(x * a) * a = x * a ^^^ 2"*)

	       (*Thm ("",num_str @{}),

	       (*""*)*)

	       ], scr = EmptyScr}:rls;

val rls_p_33 = 

    append_rls "rls_p_33" e_rls

	       [Rls_ ordne_alphabetisch,

		Rls_ fasse_zusammen,

		Rls_ verschoenere

		];

val rls_p_34 = 

    append_rls "rls_p_34" e_rls

	       [Rls_ klammern_aufloesen,

		Rls_ ordne_alphabetisch,

		Rls_ fasse_zusammen,

		Rls_ verschoenere

		];

val rechnen = 

    append_rls "rechnen" e_rls

	       [Calc ("Groups.times_class.times", eval_binop "#mult_"),

		Calc ("Groups.plus_class.plus", eval_binop "#add_"),

		Calc ("Groups.minus_class.minus", eval_binop "#subtr_")

		];

ruleset' := 

overwritelthy @{theory} (!ruleset',

		   [("ordne_alphabetisch", prep_rls ordne_alphabetisch),

		    ("fasse_zusammen", prep_rls fasse_zusammen),

		    ("verschoenere", prep_rls verschoenere),

		    ("ordne_monome", prep_rls ordne_monome),

		    ("klammern_aufloesen", prep_rls klammern_aufloesen),

		    ("klammern_ausmultiplizieren", 

		     prep_rls klammern_ausmultiplizieren)

		    ]);

(** problems **)

store_pbt

 (prep_pbt thy "pbl_vereinf_poly" [] e_pblID

 (["polynom","vereinfachen"],

  [], Erls, NONE, []));

store_pbt

 (prep_pbt thy "pbl_vereinf_poly_minus" [] e_pblID

 (["plus_minus","polynom","vereinfachen"],

  [("#Given" ,["TERM t_t"]),

   ("#Where" ,["t_t is_polyexp",

	       "Not (matchsub (?a + (?b + ?c)) t_t | " ^

	       "     matchsub (?a + (?b - ?c)) t_t | " ^

	       "     matchsub (?a - (?b + ?c)) t_t | " ^

	       "     matchsub (?a + (?b - ?c)) t_t )",

	       "Not (matchsub (?a * (?b + ?c)) t_t | " ^

	       "     matchsub (?a * (?b - ?c)) t_t | " ^

	       "     matchsub ((?b + ?c) * ?a) t_t | " ^

	       "     matchsub ((?b - ?c) * ?a) t_t )"]),

   ("#Find"  ,["normalform n_n"])

  ],

  append_rls "prls_pbl_vereinf_poly" e_rls 

	     [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),

	      Calc ("Tools.matchsub", eval_matchsub ""),

	      Thm ("or_true", num_str @{thm or_true}),

	      (*"(?a | True) = True"*)

	      Thm ("or_false", num_str @{thm or_false}),

	      (*"(?a | False) = ?a"*)

	      Thm ("not_true",num_str @{thm not_true}),

	      (*"(~ True) = False"*)

	      Thm ("not_false",num_str @{thm not_false})

	      (*"(~ False) = True"*)], 

  SOME "Vereinfache t_t", 

  [["simplification","for_polynomials","with_minus"]]));

store_pbt

 (prep_pbt thy "pbl_vereinf_poly_klammer" [] e_pblID

 (["klammer","polynom","vereinfachen"],

  [("#Given" ,["TERM t_t"]),

   ("#Where" ,["t_t is_polyexp",

	       "Not (matchsub (?a * (?b + ?c)) t_t | " ^

	       "     matchsub (?a * (?b - ?c)) t_t | " ^

	       "     matchsub ((?b + ?c) * ?a) t_t | " ^

	       "     matchsub ((?b - ?c) * ?a) t_t )"]),

   ("#Find"  ,["normalform n_n"])

  ],

  append_rls "prls_pbl_vereinf_poly_klammer" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),

	      Calc ("Tools.matchsub", eval_matchsub ""),

	      Thm ("or_true", num_str @{thm or_true}),

	      (*"(?a | True) = True"*)

	      Thm ("or_false", num_str @{thm or_false}),

	      (*"(?a | False) = ?a"*)

	      Thm ("not_true",num_str @{thm not_true}),

	      (*"(~ True) = False"*)

	      Thm ("not_false",num_str @{thm not_false})

	      (*"(~ False) = True"*)], 

  SOME "Vereinfache t_t", 

  [["simplification","for_polynomials","with_parentheses"]]));

store_pbt

 (prep_pbt thy "pbl_vereinf_poly_klammer_mal" [] e_pblID

 (["binom_klammer","polynom","vereinfachen"],

  [("#Given" ,["TERM t_t"]),

   ("#Where" ,["t_t is_polyexp"]),

   ("#Find"  ,["normalform n_n"])

  ],

  append_rls "e_rls" e_rls [(*for preds in where_*)

			    Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 

  SOME "Vereinfache t_t", 

  [["simplification","for_polynomials","with_parentheses_mult"]]));

store_pbt

 (prep_pbt thy "pbl_probe" [] e_pblID

 (["probe"],

  [], Erls, NONE, []));

store_pbt

 (prep_pbt thy "pbl_probe_poly" [] e_pblID

 (["polynom","probe"],

  [("#Given" ,["Pruefe e_e", "mitWert w_w"]),

   ("#Where" ,["e_e is_polyexp"]),

   ("#Find"  ,["Geprueft p_p"])

  ],

  append_rls "prls_pbl_probe_poly" 

	     e_rls [(*for preds in where_*)

		    Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 

  SOME "Probe e_e w_w", 

  [["probe","fuer_polynom"]]));

store_pbt

 (prep_pbt thy "pbl_probe_bruch" [] e_pblID

 (["bruch","probe"],

  [("#Given" ,["Pruefe e_e", "mitWert w_w"]),

   ("#Where" ,["e_e is_ratpolyexp"]),

   ("#Find"  ,["Geprueft p_p"])

  ],

  append_rls "prls_pbl_probe_bruch"

	     e_rls [(*for preds in where_*)

		    Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")], 

  SOME "Probe e_e w_w", 

  [["probe","fuer_bruch"]]));

(** methods **)

store_met

    (prep_met thy "met_simp_poly_minus" [] e_metID

	      (["simplification","for_polynomials","with_minus"],

	       [("#Given" ,["TERM t_t"]),

		("#Where" ,["t_t is_polyexp",

	       "Not (matchsub (?a + (?b + ?c)) t_t | " ^

	       "     matchsub (?a + (?b - ?c)) t_t | " ^

	       "     matchsub (?a - (?b + ?c)) t_t | " ^

	       "     matchsub (?a + (?b - ?c)) t_t )"]),

		("#Find"  ,["normalform n_n"])

		],

	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 

		prls = append_rls "prls_met_simp_poly_minus" e_rls 

				  [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),

	      Calc ("Tools.matchsub", eval_matchsub ""),

	      Thm ("and_true",num_str @{thm and_true}),

	      (*"(?a & True) = ?a"*)

	      Thm ("and_false",num_str @{thm and_false}),

	      (*"(?a & False) = False"*)

	      Thm ("not_true",num_str @{thm not_true}),

	      (*"(~ True) = False"*)

	      Thm ("not_false",num_str @{thm not_false})

	      (*"(~ False) = True"*)],

		crls = e_rls, nrls = rls_p_33},

"Script SimplifyScript (t_t::real) =                   " ^

"  ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@  " ^

"           (Try (Rewrite_Set fasse_zusammen     False)) @@  " ^

"           (Try (Rewrite_Set verschoenere       False)))) t_t)"

	       ));

store_met

    (prep_met thy "met_simp_poly_parenth" [] e_metID

	      (["simplification","for_polynomials","with_parentheses"],

	       [("#Given" ,["TERM t_t"]),

		("#Where" ,["t_t is_polyexp"]),

		("#Find"  ,["normalform n_n"])

		],

	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 

		prls = append_rls "simplification_for_polynomials_prls" e_rls 

				  [(*for preds in where_*)

				   Calc("Poly.is'_polyexp",eval_is_polyexp"")],

		crls = e_rls, nrls = rls_p_34},

"Script SimplifyScript (t_t::real) =                          " ^

"  ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@  " ^

"           (Try (Rewrite_Set ordne_alphabetisch False)) @@  " ^

"           (Try (Rewrite_Set fasse_zusammen     False)) @@  " ^

"           (Try (Rewrite_Set verschoenere       False)))) t_t)"

	       ));

store_met

    (prep_met thy "met_simp_poly_parenth_mult" [] e_metID

	      (["simplification","for_polynomials","with_parentheses_mult"],

	       [("#Given" ,["TERM t_t"]),

		("#Where" ,["t_t is_polyexp"]),

		("#Find"  ,["normalform n_n"])

		],

	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 

		prls = append_rls "simplification_for_polynomials_prls" e_rls 

				  [(*for preds in where_*)

				   Calc("Poly.is'_polyexp",eval_is_polyexp"")],

		crls = e_rls, nrls = rls_p_34},

"Script SimplifyScript (t_t::real) =                          " ^

"  ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ " ^

"           (Try (Rewrite_Set discard_parentheses        False)) @@ " ^

"           (Try (Rewrite_Set ordne_monome               False)) @@ " ^

"           (Try (Rewrite_Set klammern_aufloesen         False)) @@ " ^

"           (Try (Rewrite_Set ordne_alphabetisch         False)) @@ " ^

"           (Try (Rewrite_Set fasse_zusammen             False)) @@ " ^

"           (Try (Rewrite_Set verschoenere               False)))) t_t)"

	       ));

store_met

    (prep_met thy "met_probe" [] e_metID

	      (["probe"],

	       [],

	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 

		prls = Erls, crls = e_rls, nrls = Erls}, 

	       "empty_script"));

store_met

    (prep_met thy "met_probe_poly" [] e_metID

	      (["probe","fuer_polynom"],

	       [("#Given" ,["Pruefe e_e", "mitWert w_w"]),

		("#Where" ,["e_e is_polyexp"]),

		("#Find"  ,["Geprueft p_p"])

		],

	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 

		prls = append_rls "prls_met_probe_bruch"

				  e_rls [(*for preds in where_*)

					 Calc ("Rational.is'_ratpolyexp", 

					       eval_is_ratpolyexp "")], 

		crls = e_rls, nrls = rechnen}, 

"Script ProbeScript (e_e::bool) (w_w::bool list) = " ^

" (let e_e = Take e_e;                              " ^

"      e_e = Substitute w_w e_e                     " ^

" in (Repeat((Try (Repeat (Calculate TIMES))) @@  " ^

"            (Try (Repeat (Calculate PLUS ))) @@  " ^

"            (Try (Repeat (Calculate MINUS))))) e_e)"

));

store_met

    (prep_met thy "met_probe_bruch" [] e_metID

	      (["probe","fuer_bruch"],

	       [("#Given" ,["Pruefe e_e", "mitWert w_w"]),

		("#Where" ,["e_e is_ratpolyexp"]),

		("#Find"  ,["Geprueft p_p"])

		],

	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 

		prls = append_rls "prls_met_probe_bruch"

				  e_rls [(*for preds in where_*)

					 Calc ("Rational.is'_ratpolyexp", 

					       eval_is_ratpolyexp "")], 

		crls = e_rls, nrls = Erls}, 

	       "empty_script"));

*}

end