(* 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"

axiomatization where

  null_minus:            "0 - a = -a" and

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

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

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

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

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

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

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

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

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

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

(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)

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

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

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

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

(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)

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

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

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

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

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

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

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

  x_quadrat:             "(x * a) * a = x * a \<up> 2" and

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)

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

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

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

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

(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)

  (*klammer_plus_plus = (add.assoc RS sym)*)

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

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

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

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

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

ML \<open>

(** eval functions **)

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

(*HACK.WN080107*)

fun increase str = 

  let

    val (s, ss) = 

      case Symbol.explode str of

        s :: ss => (s, ss)

      | _ => raise ERROR "PolyMinus.increase: uncovered case"

  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 TermC.is_num' num then id

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

  | identifier (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _)) =

    if TermC.is_num' base then "|||||||||||||"                     (* a^2      *)

    else (*increase*) base

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

		     (Const ("Transcendental.powr", _) $

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

    if TermC.is_num' num andalso not (TermC.is_num' 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 TermC.is_num b then

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

	     if TermC.num_of_term a < TermC.num_of_term b then 

		 SOME ((UnparseC.term p) ^ " = True",

		       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

	     else SOME ((UnparseC.term p) ^ " = False",

			HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

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

	     SOME ((UnparseC.term p) ^ " = False",

		   HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

    else

	if identifier a < identifier b then 

	     SOME ((UnparseC.term p) ^ " = True",

		  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

	else SOME ((UnparseC.term p) ^ " = False",

		   HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

  | eval_kleiner _ _ _ _ =  NONE;

fun ist_monom (Free _) = true

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

    if TermC.is_num' num then true else false

  | ist_monom _ = false;

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

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

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

    if TermC.is_num' 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 TermC.is_num' num andalso not (TermC.is_num' id) then true else false

  | ist_monom (Const ("Transcendental.powr", _) $ Free _ $ Free _) = 

    true                                                    (* a^2      *)

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

		     (Const ("Transcendental.powr", _) $

			    Free _ $ Free _)) = 

    if TermC.is_num' 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 ((UnparseC.term p) ^ " = True",

	      HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))

    else SOME ((UnparseC.term p) ^ " = False",

	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))

  | eval_ist_monom _ _ _ _ =  NONE;

(** rewrite order **)

(** rulesets **)

val erls_ordne_alphabetisch =

    Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty

	       [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),

		     \<^rule_eval>\<open>PolyMinus.ist_monom\<close> (eval_ist_monom "")

		];

val ordne_alphabetisch = 

  Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],

      erls = erls_ordne_alphabetisch, 

      rules = [\<^rule_thm>\<open>tausche_plus\<close>,

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

	       \<^rule_thm>\<open>tausche_minus\<close>,

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

	       \<^rule_thm>\<open>tausche_vor_plus\<close>,

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

	       \<^rule_thm>\<open>tausche_vor_minus\<close>,

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

	       \<^rule_thm>\<open>tausche_plus_plus\<close>,

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

	       \<^rule_thm>\<open>tausche_plus_minus\<close>,

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

	       \<^rule_thm>\<open>tausche_minus_plus\<close>,

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

	       \<^rule_thm>\<open>tausche_minus_minus\<close>

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

	       ], scr = Rule.Empty_Prog};

val fasse_zusammen = 

    Rule_Def.Repeat{id = "fasse_zusammen", preconds = [], 

	rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),

	erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty 

			  [\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")],

	srls = Rule_Set.Empty, calc = [], errpatts = [],

	rules = 

	[\<^rule_thm>\<open>real_num_collect\<close>, 

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

	 \<^rule_thm>\<open>real_num_collect_assoc_r\<close>,

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

	 \<^rule_thm>\<open>real_one_collect\<close>,	

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

	 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, 

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

	 \<^rule_thm>\<open>subtrahiere\<close>,

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

	 \<^rule_thm>\<open>subtrahiere_von_1\<close>,

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

	 \<^rule_thm>\<open>subtrahiere_1\<close>,

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

	 \<^rule_thm>\<open>subtrahiere_x_plus_minus\<close>, 

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

	 \<^rule_thm>\<open>subtrahiere_x_plus1_minus\<close>,

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

	 \<^rule_thm>\<open>subtrahiere_x_plus_minus1\<close>,

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

	 \<^rule_thm>\<open>subtrahiere_x_minus_plus\<close>, 

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

	 \<^rule_thm>\<open>subtrahiere_x_minus1_plus\<close>,

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

	 \<^rule_thm>\<open>subtrahiere_x_minus_plus1\<close>,

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

	 \<^rule_thm>\<open>subtrahiere_x_minus_minus\<close>, 

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

	 \<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>,

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

	 \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>,

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

	 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),

	 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_"),

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

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

	 \<^rule_thm>\<open>real_mult_2_assoc_r\<close>,

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

	 \<^rule_thm_sym>\<open>real_mult_2\<close>,

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

	 \<^rule_thm>\<open>addiere_vor_minus\<close>,

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

	 \<^rule_thm>\<open>addiere_eins_vor_minus\<close>,

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

	 \<^rule_thm>\<open>subtrahiere_vor_minus\<close>,

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

	 \<^rule_thm>\<open>subtrahiere_eins_vor_minus\<close>

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

	 ], scr = Rule.Empty_Prog};

val verschoenere = 

  Rule_Def.Repeat{id = "verschoenere", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],

      erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty 

			[\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")],

      rules = [\<^rule_thm>\<open>vorzeichen_minus_weg1\<close>,

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

	       \<^rule_thm>\<open>vorzeichen_minus_weg2\<close>,

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

	       \<^rule_thm>\<open>vorzeichen_minus_weg3\<close>,

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

	       \<^rule_thm>\<open>vorzeichen_minus_weg4\<close>,

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

	       \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

	       \<^rule_thm>\<open>mult_zero_left\<close>,    

	       (*"0 * z = 0"*)

	       \<^rule_thm>\<open>mult_1_left\<close>,     

	       (*"1 * z = z"*)

	       \<^rule_thm>\<open>add_0_left\<close>,

	       (*"0 + z = z"*)

	       \<^rule_thm>\<open>null_minus\<close>,

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

	       \<^rule_thm>\<open>vor_minus_mal\<close>

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

	       ], scr = Rule.Empty_Prog} (*end verschoenere*);

val klammern_aufloesen = 

  Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty, 

      rules = [\<^rule_thm_sym>\<open>add.assoc\<close>,

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

	       \<^rule_thm>\<open>klammer_plus_minus\<close>,

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

	       \<^rule_thm>\<open>klammer_minus_plus\<close>,

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

	       \<^rule_thm>\<open>klammer_minus_minus\<close>

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

	       ], scr = Rule.Empty_Prog};

val klammern_ausmultiplizieren = 

  Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty, 

      rules = [\<^rule_thm>\<open>distrib_right\<close>,

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

	       \<^rule_thm>\<open>distrib_left\<close>,

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

	       \<^rule_thm>\<open>klammer_mult_minus\<close>,

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

	       \<^rule_thm>\<open>klammer_minus_mult\<close>

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

	       ], scr = Rule.Empty_Prog};

val ordne_monome = 

  Rule_Def.Repeat{id = "ordne_monome", preconds = [], 

      rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], 

      erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty

	       [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),

		      \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "")

		], 

      rules = [\<^rule_thm>\<open>tausche_mal\<close>,

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

	       \<^rule_thm>\<open>tausche_vor_mal\<close>,

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

	       \<^rule_thm>\<open>tausche_mal_mal\<close>,

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

	       \<^rule_thm>\<open>x_quadrat\<close>

	       (*"(x * a) * a = x * a \<up> 2"*)

	       ], scr = Rule.Empty_Prog};

val rls_p_33 = 

    Rule_Set.append_rules "rls_p_33" Rule_Set.empty

	       [Rule.Rls_ ordne_alphabetisch,

		Rule.Rls_ fasse_zusammen,

		Rule.Rls_ verschoenere

		];

val rls_p_34 = 

    Rule_Set.append_rules "rls_p_34" Rule_Set.empty

	       [Rule.Rls_ klammern_aufloesen,

		Rule.Rls_ ordne_alphabetisch,

		Rule.Rls_ fasse_zusammen,

		Rule.Rls_ verschoenere

		];

val rechnen = 

    Rule_Set.append_rules "rechnen" Rule_Set.empty

	       [\<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),

          \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),

          \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_")

		];

\<close>

rule_set_knowledge

  ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and

  fasse_zusammen = \<open>prep_rls' fasse_zusammen\<close> and

  verschoenere = \<open>prep_rls' verschoenere\<close> and

  ordne_monome = \<open>prep_rls' ordne_monome\<close> and

  klammern_aufloesen = \<open>prep_rls' klammern_aufloesen\<close> and

  klammern_ausmultiplizieren = \<open>prep_rls' klammern_ausmultiplizieren\<close>

(** problems **)

setup \<open>KEStore_Elems.add_pbts

  [(Problem.prep_input @{theory} "pbl_vereinf_poly" [] Problem.id_empty

      (["polynom", "vereinfachen"], [], Rule_Set.Empty, NONE, [])),

    (Problem.prep_input @{theory} "pbl_vereinf_poly_minus" [] Problem.id_empty

      (["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"])],

        Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty 

	        [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),

	         \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),

	          \<^rule_thm>\<open>or_true\<close>,

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

            \<^rule_thm>\<open>or_false\<close>,

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

            \<^rule_thm>\<open>not_true\<close>,

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

            \<^rule_thm>\<open>not_false\<close>

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

       SOME "Vereinfache t_t", [["simplification", "for_polynomials", "with_minus"]])),

    (Problem.prep_input @{theory} "pbl_vereinf_poly_klammer" [] Problem.id_empty

      (["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"])],

        Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty

          [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),

	           \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),

             \<^rule_thm>\<open>or_true\<close>,

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

             \<^rule_thm>\<open>or_false\<close>,

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

             \<^rule_thm>\<open>not_true\<close>,

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

             \<^rule_thm>\<open>not_false\<close>

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

        SOME "Vereinfache t_t", 

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

    (Problem.prep_input @{theory} "pbl_vereinf_poly_klammer_mal" [] Problem.id_empty

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

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

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

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

        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)

			      \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")], 

        SOME "Vereinfache t_t", 

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

    (Problem.prep_input @{theory} "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),

    (Problem.prep_input @{theory} "pbl_probe_poly" [] Problem.id_empty

      (["polynom", "probe"],

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

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

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

        Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)

		      \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")], 

        SOME "Probe e_e w_w", 

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

    (Problem.prep_input @{theory} "pbl_probe_bruch" [] Problem.id_empty

      (["bruch", "probe"],

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

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

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

        Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)

		      \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")], 

        SOME "Probe e_e w_w", [["probe", "fuer_bruch"]]))]\<close>

(** methods **)

partial_function (tailrec) simplify :: "real \<Rightarrow> real"

  where

"simplify t_t = (

  (Repeat(

    (Try (Rewrite_Set ''ordne_alphabetisch'')) #>

    (Try (Rewrite_Set ''fasse_zusammen'')) #>

    (Try (Rewrite_Set ''verschoenere'')))

  ) t_t)"

method met_simp_poly_minus : "simplification/for_polynomials/with_minus" =

  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,

    prls =

      Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty 

        [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),

          \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),

          \<^rule_thm>\<open>and_true\<close>,

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

          \<^rule_thm>\<open>and_false\<close>,

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

          \<^rule_thm>\<open>not_true\<close>,

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

          \<^rule_thm>\<open>not_false\<close>

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

    crls = Rule_Set.empty, errpats = [], nrls = rls_p_33}\<close>

  Program: simplify.simps

  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"

partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"

  where

"simplify2 t_t = (

  (Repeat(

    (Try (Rewrite_Set ''klammern_aufloesen'')) #>

    (Try (Rewrite_Set ''ordne_alphabetisch'')) #>

    (Try (Rewrite_Set ''fasse_zusammen'')) #>

    (Try (Rewrite_Set ''verschoenere'')))

  ) t_t)"

method met_simp_poly_parenth : "simplification/for_polynomials/with_parentheses" =

  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 

    prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty 

      [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],

    crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>

  Program: simplify2.simps

  Given: "Term t_t"

  Where: "t_t is_polyexp"

  Find: "normalform n_n"

partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"

  where

"simplify3 t_t = (

  (Repeat(

    (Try (Rewrite_Set ''klammern_ausmultiplizieren'')) #>

    (Try (Rewrite_Set ''discard_parentheses'')) #>

    (Try (Rewrite_Set ''ordne_monome'')) #>

    (Try (Rewrite_Set ''klammern_aufloesen'')) #>

    (Try (Rewrite_Set ''ordne_alphabetisch'')) #>

    (Try (Rewrite_Set ''fasse_zusammen'')) #>

    (Try (Rewrite_Set ''verschoenere'')))

  ) t_t)"

method met_simp_poly_parenth_mult : "simplification/for_polynomials/with_parentheses_mult" =

  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 

    prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty 

      [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],

    crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>

  Program: simplify3.simps

  Given: "Term t_t"

  Where: "t_t is_polyexp"

  Find: "normalform n_n"

method met_probe : "probe" =

  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,

    errpats = [], nrls = Rule_Set.Empty}\<close>

partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"

  where

"mache_probe e_e w_w = (

  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)"

method met_probe_poly : "probe/fuer_polynom" =

  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 

    prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty

        [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")], 

    crls = Rule_Set.empty, errpats = [], nrls = rechnen}\<close>

  Program: mache_probe.simps

  Given: "Pruefe e_e" "mitWert w_w"

  Where: "e_e is_polyexp"

  Find: "Geprueft p_p"

method met_probe_bruch : "probe/fuer_bruch" =

  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 

    prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty

        [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],

    crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty}\<close>

  Given: "Pruefe e_e" "mitWert w_w"

  Where: "e_e is_ratpolyexp"

  Find: "Geprueft p_p"

ML \<open>

\<close> ML \<open>

\<close>

end