neuper@37906: (* attempts to perserve binary minus as wanted by Austrian teachers
neuper@37906:    WN071207
neuper@37906:    (c) due to copyright terms
neuper@37906: *)
neuper@37906: 
neuper@37950: theory PolyMinus imports (*Poly// due to "is_ratpolyexp" in...*) Rational begin
neuper@37906: 
neuper@37906: consts
neuper@37906: 
neuper@37906:   (*predicates for conditions in rewriting*)
neuper@37906:   kleiner     :: "['a, 'a] => bool" 	("_ kleiner _") 
walther@60278:   ist_monom  :: "'a => bool"		("_ ist'_monom")
neuper@37906: 
neuper@37906:   (*the CAS-command*)
neuper@37906:   Probe       :: "[bool, bool list] => bool"  
neuper@37906: 	(*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*)
neuper@37906: 
neuper@37906:   (*descriptions for the pbl and met*)
neuper@37950:   Pruefe      :: "bool => una"
neuper@37950:   mitWert     :: "bool list => tobooll"
neuper@37950:   Geprueft    :: "bool => una"
neuper@37906: 
neuper@52148: axiomatization where
neuper@37906: 
neuper@52148:   null_minus:            "0 - a = -a" and
neuper@52148:   vor_minus_mal:         "- a * b = (-a) * b" and
neuper@37906: 
neuper@37906:   (*commute with invariant (a.b).c -association*)
neuper@37980:   tausche_plus:		"[| b ist_monom; a kleiner b  |] ==> 
neuper@52148: 			 (b + a) = (a + b)" and
neuper@37980:   tausche_minus:		"[| b ist_monom; a kleiner b  |] ==> 
neuper@52148: 			 (b - a) = (-a + b)" and
neuper@37980:   tausche_vor_plus:	"[| b ist_monom; a kleiner b  |] ==> 
neuper@52148: 			 (- b + a) = (a - b)" and
neuper@37980:   tausche_vor_minus:	"[| b ist_monom; a kleiner b  |] ==> 
neuper@52148: 			 (- b - a) = (-a - b)" and
walther@60269: (*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
neuper@52148:   tausche_plus_plus:	"b kleiner c ==> (a + c + b) = (a + b + c)" and
neuper@52148:   tausche_plus_minus:	"b kleiner c ==> (a + c - b) = (a - b + c)" and
neuper@52148:   tausche_minus_plus:	"b kleiner c ==> (a - c + b) = (a + b - c)" and
neuper@52148:   tausche_minus_minus:	"b kleiner c ==> (a - c - b) = (a - b - c)" and
walther@60269: (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
neuper@37906: 
neuper@37906:   (*commute with invariant (a.b).c -association*)
neuper@37980:   tausche_mal:		"[| b is_atom; a kleiner b  |] ==> 
neuper@52148: 			 (b * a) = (a * b)" and
neuper@37980:   tausche_vor_mal:	"[| b is_atom; a kleiner b  |] ==> 
neuper@52148: 			 (-b * a) = (-a * b)" and
neuper@37980:   tausche_mal_mal:	"[| c is_atom; b kleiner c  |] ==> 
neuper@52148: 			 (x * c * b) = (x * b * c)" and
walther@60242:   x_quadrat:             "(x * a) * a = x * a \<up> 2" and
neuper@37906: 
neuper@37906: 
neuper@37980:   subtrahiere:               "[| l is_const; m is_const |] ==>  
neuper@52148: 			     m * v - l * v = (m - l) * v" and
neuper@37980:   subtrahiere_von_1:         "[| l is_const |] ==>  
neuper@52148: 			     v - l * v = (1 - l) * v" and
neuper@37980:   subtrahiere_1:             "[| l is_const; m is_const |] ==>  
neuper@52148: 			     m * v - v = (m - 1) * v" and
neuper@37906: 
neuper@37980:   subtrahiere_x_plus_minus:  "[| l is_const; m is_const |] ==>  
neuper@52148: 			     (x + m * v) - l * v = x + (m - l) * v" and
neuper@37980:   subtrahiere_x_plus1_minus: "[| l is_const |] ==>  
neuper@52148: 			     (x + v) - l * v = x + (1 - l) * v" and
neuper@37980:   subtrahiere_x_plus_minus1: "[| m is_const |] ==>  
neuper@52148: 			     (x + m * v) - v = x + (m - 1) * v" and
neuper@37906: 
neuper@37980:   subtrahiere_x_minus_plus:  "[| l is_const; m is_const |] ==>  
neuper@52148: 			     (x - m * v) + l * v = x + (-m + l) * v" and
neuper@37980:   subtrahiere_x_minus1_plus: "[| l is_const |] ==>  
neuper@52148: 			     (x - v) + l * v = x + (-1 + l) * v" and
neuper@37980:   subtrahiere_x_minus_plus1: "[| m is_const |] ==>  
neuper@52148: 			     (x - m * v) + v = x + (-m + 1) * v" and
neuper@37906: 
neuper@37980:   subtrahiere_x_minus_minus: "[| l is_const; m is_const |] ==>  
neuper@52148: 			     (x - m * v) - l * v = x + (-m - l) * v" and
neuper@37980:   subtrahiere_x_minus1_minus:"[| l is_const |] ==>  
neuper@52148: 			     (x - v) - l * v = x + (-1 - l) * v" and
neuper@37980:   subtrahiere_x_minus_minus1:"[| m is_const |] ==>  
neuper@52148: 			     (x - m * v) - v = x + (-m - 1) * v" and
neuper@37906: 
neuper@37906: 
neuper@37980:   addiere_vor_minus:         "[| l is_const; m is_const |] ==>  
neuper@52148: 			     - (l * v) +  m * v = (-l + m) * v" and
neuper@37980:   addiere_eins_vor_minus:    "[| m is_const |] ==>  
neuper@52148: 			     -  v +  m * v = (-1 + m) * v" and
neuper@37980:   subtrahiere_vor_minus:     "[| l is_const; m is_const |] ==>  
neuper@52148: 			     - (l * v) -  m * v = (-l - m) * v" and
neuper@37980:   subtrahiere_eins_vor_minus:"[| m is_const |] ==>  
neuper@52148: 			     -  v -  m * v = (-1 - m) * v" and
neuper@37906: 
walther@60269: (*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
neuper@52148:   vorzeichen_minus_weg1:      "l kleiner 0 ==> a + l * b = a - -1*l * b" and
neuper@52148:   vorzeichen_minus_weg2:      "l kleiner 0 ==> a - l * b = a + -1*l * b" and
neuper@52148:   vorzeichen_minus_weg3:      "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and
neuper@52148:   vorzeichen_minus_weg4:      "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and
walther@60269: (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
neuper@37906: 
walther@59877:   (*klammer_plus_plus = (add.assoc RS sym)*)
neuper@52148:   klammer_plus_minus:          "a + (b - c) = (a + b) - c" and
neuper@52148:   klammer_minus_plus:          "a - (b + c) = (a - b) - c" and
neuper@52148:   klammer_minus_minus:         "a - (b - c) = (a - b) + c" and
neuper@37906: 
neuper@52148:   klammer_mult_minus:          "a * (b - c) = a * b - a * c" and
neuper@37980:   klammer_minus_mult:          "(b - c) * a = b * a - c * a"
neuper@37906: 
wneuper@59472: ML \<open>
neuper@37972: val thy = @{theory};
neuper@37972: 
neuper@37950: (** eval functions **)
neuper@37906: 
neuper@37950: (*. get the identifier from specific monomials; see fun ist_monom .*)
neuper@37950: (*HACK.WN080107*)
neuper@37950: fun increase str = 
walther@60269:   let
walther@60269:     val (s, ss) = 
walther@60269:       case Symbol.explode str of
walther@60269:         s :: ss => (s, ss)
walther@60269:       | _ => raise ERROR "PolyMinus.increase: uncovered case"
walther@60269:   in implode ((chr (ord s + 1))::ss) end;
walther@60269: fun identifier (Free (id,_)) = id                            (* 2     ,   a   *)
walther@60269:   | identifier (Const ("Groups.times_class.times", _) $ Free (_(*num*), _) $ Free (id, _)) = 
walther@60269:     id                                                       (* 2*a   , a*b *)
neuper@38034:   | identifier (Const ("Groups.times_class.times", _) $                          (* 3*a*b    *)
neuper@38034: 		     (Const ("Groups.times_class.times", _) $
neuper@37950: 			    Free (num, _) $ Free _) $ Free (id, _)) = 
wneuper@59390:     if TermC.is_num' num then id
neuper@37950:     else "|||||||||||||"
walther@60275:   | identifier (Const ("Transcendental.powr", _) $ Free (base, _) $ Free (_(*exp*), _)) =
walther@60269:     if TermC.is_num' base then "|||||||||||||"                     (* a^2      *)
neuper@37950:     else (*increase*) base
neuper@38034:   | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $          (* 3*a^2    *)
walther@60275: 		     (Const ("Transcendental.powr", _) $
walther@60269: 			    Free (base, _) $ Free (_(*exp*), _))) = 
wneuper@59390:     if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base
neuper@37950:     else "|||||||||||||"
neuper@37950:   | identifier _ = "|||||||||||||"(*the "largest" string*);
neuper@37950: 
neuper@37950: (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
neuper@37950: (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
neuper@37950: fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _  =
wneuper@59389:      if TermC.is_num b then
wneuper@59389: 	 if TermC.is_num a then (*123 kleiner 32 = True !!!*)
wneuper@59392: 	     if TermC.num_of_term a < TermC.num_of_term b then 
walther@59868: 		 SOME ((UnparseC.term p) ^ " = True",
wneuper@59390: 		       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
walther@59868: 	     else SOME ((UnparseC.term p) ^ " = False",
wneuper@59390: 			HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
neuper@37950: 	 else (* -1 * -2 kleiner 0 *)
walther@59868: 	     SOME ((UnparseC.term p) ^ " = False",
wneuper@59390: 		   HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
neuper@37950:     else
neuper@37950: 	if identifier a < identifier b then 
walther@59868: 	     SOME ((UnparseC.term p) ^ " = True",
wneuper@59390: 		  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
walther@59868: 	else SOME ((UnparseC.term p) ^ " = False",
wneuper@59390: 		   HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
neuper@37950:   | eval_kleiner _ _ _ _ =  NONE;
neuper@37950: 
walther@60269: fun ist_monom (Free _) = true
walther@60269:   | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free _) = 
wneuper@59390:     if TermC.is_num' num then true else false
neuper@37950:   | ist_monom _ = false;
walther@60269: (*. this function only accepts the most simple monoms  vvvvvvvvvv .*)
walther@60269: fun ist_monom (Free _) = true                          (* 2,   a   *)
neuper@38034:   | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
wneuper@59390:     if TermC.is_num' id then false else true
neuper@38034:   | ist_monom (Const ("Groups.times_class.times", _) $                          (* 3*a*b    *)
neuper@38034: 		     (Const ("Groups.times_class.times", _) $
neuper@37950: 			    Free (num, _) $ Free _) $ Free (id, _)) =
wneuper@59390:     if TermC.is_num' num andalso not (TermC.is_num' id) then true else false
walther@60275:   | ist_monom (Const ("Transcendental.powr", _) $ Free _ $ Free _) = 
neuper@37950:     true                                                    (* a^2      *)
neuper@38034:   | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $          (* 3*a^2    *)
walther@60275: 		     (Const ("Transcendental.powr", _) $
walther@60269: 			    Free _ $ Free _)) = 
wneuper@59390:     if TermC.is_num' num then true else false
neuper@37950:   | ist_monom _ = false;
neuper@37950: 
neuper@37950: (* is this a univariate monomial ? *)
walther@60278: (*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*)
walther@60278: fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist_monom",_) $ a)) _  =
neuper@37950:     if ist_monom a  then 
walther@59868: 	SOME ((UnparseC.term p) ^ " = True",
wneuper@59390: 	      HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
walther@59868:     else SOME ((UnparseC.term p) ^ " = False",
wneuper@59390: 	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
neuper@37950:   | eval_ist_monom _ _ _ _ =  NONE;
neuper@37950: 
neuper@37950: 
neuper@37950: (** rewrite order **)
neuper@37950: 
neuper@37950: (** rulesets **)
neuper@37950: 
neuper@37950: val erls_ordne_alphabetisch =
walther@59852:     Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty
walther@59878: 	       [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""),
walther@60278: 		Rule.Eval ("PolyMinus.ist_monom", eval_ist_monom "")
neuper@37950: 		];
neuper@37950: 
neuper@37950: val ordne_alphabetisch = 
walther@59851:   Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [], 
walther@59857:       rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
neuper@37950:       erls = erls_ordne_alphabetisch, 
walther@59871:       rules = [Rule.Thm ("tausche_plus",ThmC.numerals_to_Free @{thm tausche_plus}),
neuper@37950: 	       (*"b kleiner a ==> (b + a) = (a + b)"*)
walther@59871: 	       Rule.Thm ("tausche_minus",ThmC.numerals_to_Free @{thm tausche_minus}),
neuper@37950: 	       (*"b kleiner a ==> (b - a) = (-a + b)"*)
walther@59871: 	       Rule.Thm ("tausche_vor_plus",ThmC.numerals_to_Free @{thm tausche_vor_plus}),
neuper@37950: 	       (*"[| b ist_monom; a kleiner b  |] ==> (- b + a) = (a - b)"*)
walther@59871: 	       Rule.Thm ("tausche_vor_minus",ThmC.numerals_to_Free @{thm tausche_vor_minus}),
neuper@37950: 	       (*"[| b ist_monom; a kleiner b  |] ==> (- b - a) = (-a - b)"*)
walther@59871: 	       Rule.Thm ("tausche_plus_plus",ThmC.numerals_to_Free @{thm tausche_plus_plus}),
neuper@37950: 	       (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
walther@59871: 	       Rule.Thm ("tausche_plus_minus",ThmC.numerals_to_Free @{thm tausche_plus_minus}),
neuper@37950: 	       (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
walther@59871: 	       Rule.Thm ("tausche_minus_plus",ThmC.numerals_to_Free @{thm tausche_minus_plus}),
neuper@37950: 	       (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
walther@59871: 	       Rule.Thm ("tausche_minus_minus",ThmC.numerals_to_Free @{thm tausche_minus_minus})
neuper@37950: 	       (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
walther@59878: 	       ], scr = Rule.Empty_Prog};
neuper@37950: 
neuper@37950: val fasse_zusammen = 
walther@59851:     Rule_Def.Repeat{id = "fasse_zusammen", preconds = [], 
walther@59857: 	rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
walther@59852: 	erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty 
walther@60278: 			  [Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")], 
walther@59851: 	srls = Rule_Set.Empty, calc = [], errpatts = [],
neuper@37950: 	rules = 
walther@59871: 	[Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}), 
neuper@37950: 	 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
walther@59871: 	 Rule.Thm ("real_num_collect_assoc_r",ThmC.numerals_to_Free @{thm real_num_collect_assoc_r}),
neuper@37950: 	 (*"[| l is_const; m..|] ==>  (k + m * n) + l * n = k + (l + m)*n"*)
walther@59871: 	 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),	
neuper@37950: 	 (*"m is_const ==> n + m * n = (1 + m) * n"*)
walther@59871: 	 Rule.Thm ("real_one_collect_assoc_r",ThmC.numerals_to_Free @{thm real_one_collect_assoc_r}), 
neuper@37950: 	 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
neuper@37950: 
neuper@37950: 
walther@59871: 	 Rule.Thm ("subtrahiere",ThmC.numerals_to_Free @{thm subtrahiere}),
neuper@37950: 	 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
walther@59871: 	 Rule.Thm ("subtrahiere_von_1",ThmC.numerals_to_Free @{thm subtrahiere_von_1}),
neuper@37950: 	 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
walther@59871: 	 Rule.Thm ("subtrahiere_1",ThmC.numerals_to_Free @{thm subtrahiere_1}),
neuper@37950: 	 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
neuper@37950: 
walther@59871: 	 Rule.Thm ("subtrahiere_x_plus_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_plus_minus}), 
neuper@37950: 	 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
walther@59871: 	 Rule.Thm ("subtrahiere_x_plus1_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_plus1_minus}),
neuper@37950: 	 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
walther@59871: 	 Rule.Thm ("subtrahiere_x_plus_minus1",ThmC.numerals_to_Free @{thm subtrahiere_x_plus_minus1}),
neuper@37950: 	 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
neuper@37950: 
walther@59871: 	 Rule.Thm ("subtrahiere_x_minus_plus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_plus}), 
neuper@37950: 	 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
walther@59871: 	 Rule.Thm ("subtrahiere_x_minus1_plus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus1_plus}),
neuper@37950: 	 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
walther@59871: 	 Rule.Thm ("subtrahiere_x_minus_plus1",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_plus1}),
neuper@37950: 	 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
neuper@37950: 
walther@59871: 	 Rule.Thm ("subtrahiere_x_minus_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_minus}), 
neuper@37950: 	 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
walther@59871: 	 Rule.Thm ("subtrahiere_x_minus1_minus",ThmC.numerals_to_Free @{thm subtrahiere_x_minus1_minus}),
neuper@37950: 	 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
walther@59871: 	 Rule.Thm ("subtrahiere_x_minus_minus1",ThmC.numerals_to_Free @{thm subtrahiere_x_minus_minus1}),
neuper@37950: 	 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
neuper@37950: 	 
walther@59878: 	 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
walther@59878: 	 Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#subtr_"),
neuper@37950: 	 
wneuper@59416: 	 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
neuper@37950:            (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
walther@59871: 	 Rule.Thm ("real_mult_2_assoc_r",ThmC.numerals_to_Free @{thm real_mult_2_assoc_r}),
neuper@37950: 	 (*"(k + z1) + z1 = k + 2 * z1"*)
walther@59871: 	 Rule.Thm ("sym_real_mult_2",ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
neuper@37950: 	 (*"z1 + z1 = 2 * z1"*)
neuper@37950: 
walther@59871: 	 Rule.Thm ("addiere_vor_minus",ThmC.numerals_to_Free @{thm addiere_vor_minus}),
neuper@37950: 	 (*"[| l is_const; m is_const |] ==> -(l * v) +  m * v = (-l + m) *v"*)
walther@59871: 	 Rule.Thm ("addiere_eins_vor_minus",ThmC.numerals_to_Free @{thm addiere_eins_vor_minus}),
neuper@37950: 	 (*"[| m is_const |] ==> -  v +  m * v = (-1 + m) * v"*)
walther@59871: 	 Rule.Thm ("subtrahiere_vor_minus",ThmC.numerals_to_Free @{thm subtrahiere_vor_minus}),
neuper@37950: 	 (*"[| l is_const; m is_const |] ==> -(l * v) -  m * v = (-l - m) *v"*)
walther@59871: 	 Rule.Thm ("subtrahiere_eins_vor_minus",ThmC.numerals_to_Free @{thm subtrahiere_eins_vor_minus})
neuper@37950: 	 (*"[| m is_const |] ==> -  v -  m * v = (-1 - m) * v"*)
neuper@37950: 	 
walther@59878: 	 ], scr = Rule.Empty_Prog};
neuper@37950:     
neuper@37950: val verschoenere = 
walther@59851:   Rule_Def.Repeat{id = "verschoenere", preconds = [], 
walther@59857:       rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@59852:       erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty 
walther@59878: 			[Rule.Eval ("PolyMinus.kleiner", eval_kleiner "")], 
walther@59871:       rules = [Rule.Thm ("vorzeichen_minus_weg1",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg1}),
neuper@37950: 	       (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
walther@59871: 	       Rule.Thm ("vorzeichen_minus_weg2",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg2}),
neuper@37950: 	       (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
walther@59871: 	       Rule.Thm ("vorzeichen_minus_weg3",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg3}),
neuper@37950: 	       (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
walther@59871: 	       Rule.Thm ("vorzeichen_minus_weg4",ThmC.numerals_to_Free @{thm vorzeichen_minus_weg4}),
neuper@37950: 	       (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
neuper@37950: 
walther@59878: 	       Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
neuper@37950: 
walther@59871: 	       Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),    
neuper@37950: 	       (*"0 * z = 0"*)
walther@59871: 	       Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),     
neuper@37950: 	       (*"1 * z = z"*)
walther@59871: 	       Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
neuper@37950: 	       (*"0 + z = z"*)
walther@59871: 	       Rule.Thm ("null_minus",ThmC.numerals_to_Free @{thm null_minus}),
neuper@37950: 	       (*"0 - a = -a"*)
walther@59871: 	       Rule.Thm ("vor_minus_mal",ThmC.numerals_to_Free @{thm vor_minus_mal})
neuper@37950: 	       (*"- a * b = (-a) * b"*)
neuper@37950: 
walther@59871: 	       (*Rule.Thm ("",ThmC.numerals_to_Free @{}),*)
neuper@37950: 	       (**)
walther@59878: 	       ], scr = Rule.Empty_Prog} (*end verschoenere*);
neuper@37950: 
neuper@37950: val klammern_aufloesen = 
walther@59851:   Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [], 
walther@59857:       rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty, 
walther@59877:       rules = [Rule.Thm ("sym_add.assoc",
walther@59871:                      ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym})),
neuper@37950: 	       (*"a + (b + c) = (a + b) + c"*)
walther@59871: 	       Rule.Thm ("klammer_plus_minus",ThmC.numerals_to_Free @{thm klammer_plus_minus}),
neuper@37950: 	       (*"a + (b - c) = (a + b) - c"*)
walther@59871: 	       Rule.Thm ("klammer_minus_plus",ThmC.numerals_to_Free @{thm klammer_minus_plus}),
neuper@37950: 	       (*"a - (b + c) = (a - b) - c"*)
walther@59871: 	       Rule.Thm ("klammer_minus_minus",ThmC.numerals_to_Free @{thm klammer_minus_minus})
neuper@37950: 	       (*"a - (b - c) = (a - b) + c"*)
walther@59878: 	       ], scr = Rule.Empty_Prog};
neuper@37950: 
neuper@37950: val klammern_ausmultiplizieren = 
walther@59851:   Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [], 
walther@59857:       rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], erls = Rule_Set.Empty, 
walther@59871:       rules = [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
neuper@37950: 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
walther@59871: 	       Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
neuper@37950: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950: 	       
walther@59871: 	       Rule.Thm ("klammer_mult_minus",ThmC.numerals_to_Free @{thm klammer_mult_minus}),
neuper@37950: 	       (*"a * (b - c) = a * b - a * c"*)
walther@59871: 	       Rule.Thm ("klammer_minus_mult",ThmC.numerals_to_Free @{thm klammer_minus_mult})
neuper@37950: 	       (*"(b - c) * a = b * a - c * a"*)
neuper@37950: 
walther@59871: 	       (*Rule.Thm ("",ThmC.numerals_to_Free @{}),
neuper@37950: 	       (*""*)*)
walther@59878: 	       ], scr = Rule.Empty_Prog};
neuper@37950: 
neuper@37950: val ordne_monome = 
walther@59851:   Rule_Def.Repeat{id = "ordne_monome", preconds = [], 
walther@59857:       rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [], 
walther@59852:       erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty
walther@59878: 	       [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""),
walther@60278: 		Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "")
neuper@37950: 		], 
walther@59871:       rules = [Rule.Thm ("tausche_mal",ThmC.numerals_to_Free @{thm tausche_mal}),
neuper@37950: 	       (*"[| b is_atom; a kleiner b  |] ==> (b * a) = (a * b)"*)
walther@59871: 	       Rule.Thm ("tausche_vor_mal",ThmC.numerals_to_Free @{thm tausche_vor_mal}),
neuper@37950: 	       (*"[| b is_atom; a kleiner b  |] ==> (-b * a) = (-a * b)"*)
walther@59871: 	       Rule.Thm ("tausche_mal_mal",ThmC.numerals_to_Free @{thm tausche_mal_mal}),
neuper@37950: 	       (*"[| c is_atom; b kleiner c  |] ==> (a * c * b) = (a * b *c)"*)
walther@59871: 	       Rule.Thm ("x_quadrat",ThmC.numerals_to_Free @{thm x_quadrat})
walther@60242: 	       (*"(x * a) * a = x * a \<up> 2"*)
neuper@37950: 
walther@59871: 	       (*Rule.Thm ("",ThmC.numerals_to_Free @{}),
neuper@37950: 	       (*""*)*)
walther@59878: 	       ], scr = Rule.Empty_Prog};
neuper@37950: 
neuper@37950: 
neuper@37950: val rls_p_33 = 
walther@59852:     Rule_Set.append_rules "rls_p_33" Rule_Set.empty
wneuper@59416: 	       [Rule.Rls_ ordne_alphabetisch,
wneuper@59416: 		Rule.Rls_ fasse_zusammen,
wneuper@59416: 		Rule.Rls_ verschoenere
neuper@37950: 		];
neuper@37950: val rls_p_34 = 
walther@59852:     Rule_Set.append_rules "rls_p_34" Rule_Set.empty
wneuper@59416: 	       [Rule.Rls_ klammern_aufloesen,
wneuper@59416: 		Rule.Rls_ ordne_alphabetisch,
wneuper@59416: 		Rule.Rls_ fasse_zusammen,
wneuper@59416: 		Rule.Rls_ verschoenere
neuper@37950: 		];
neuper@37950: val rechnen = 
walther@59852:     Rule_Set.append_rules "rechnen" Rule_Set.empty
walther@59878: 	       [Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
walther@59878: 		Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
walther@59878: 		Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#subtr_")
neuper@37950: 		];
wneuper@59472: \<close>
wneuper@59472: setup \<open>KEStore_Elems.add_rlss 
s1210629013@55444:   [("ordne_alphabetisch", (Context.theory_name @{theory}, prep_rls' ordne_alphabetisch)), 
s1210629013@55444:   ("fasse_zusammen", (Context.theory_name @{theory}, prep_rls' fasse_zusammen)), 
s1210629013@55444:   ("verschoenere", (Context.theory_name @{theory}, prep_rls' verschoenere)), 
s1210629013@55444:   ("ordne_monome", (Context.theory_name @{theory}, prep_rls' ordne_monome)), 
s1210629013@55444:   ("klammern_aufloesen", (Context.theory_name @{theory}, prep_rls' klammern_aufloesen)), 
neuper@52125:   ("klammern_ausmultiplizieren",
wneuper@59472:     (Context.theory_name @{theory}, prep_rls' klammern_ausmultiplizieren))]\<close>
neuper@37950: 
neuper@37950: (** problems **)
wneuper@59472: setup \<open>KEStore_Elems.add_pbts
walther@59973:   [(Problem.prep_input thy "pbl_vereinf_poly" [] Problem.id_empty
walther@59997:       (["polynom", "vereinfachen"], [], Rule_Set.Empty, NONE, [])),
walther@59973:     (Problem.prep_input thy "pbl_vereinf_poly_minus" [] Problem.id_empty
walther@59997:       (["plus_minus", "polynom", "vereinfachen"],
s1210629013@55339:         [("#Given", ["Term t_t"]),
s1210629013@55339:           ("#Where", ["t_t is_polyexp",
s1210629013@55339:             "Not (matchsub (?a + (?b + ?c)) t_t | " ^
s1210629013@55339:             "     matchsub (?a + (?b - ?c)) t_t | " ^
s1210629013@55339:             "     matchsub (?a - (?b + ?c)) t_t | " ^
s1210629013@55339:             "     matchsub (?a + (?b - ?c)) t_t )",
s1210629013@55339:             "Not (matchsub (?a * (?b + ?c)) t_t | " ^
s1210629013@55339:             "     matchsub (?a * (?b - ?c)) t_t | " ^
s1210629013@55339:             "     matchsub ((?b + ?c) * ?a) t_t | " ^
s1210629013@55339:             "     matchsub ((?b - ?c) * ?a) t_t )"]),
s1210629013@55339:           ("#Find", ["normalform n_n"])],
walther@59852:         Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty 
walther@60278: 	        [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
walther@59878: 	          Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
walther@59871: 	          Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
s1210629013@55339:             (*"(?a | True) = True"*)
walther@59871:             Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
s1210629013@55339:             (*"(?a | False) = ?a"*)
walther@59871:             Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
s1210629013@55339:             (*"(~ True) = False"*)
walther@59871:             Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
s1210629013@55339:             (*"(~ False) = True"*)], 
walther@59997:        SOME "Vereinfache t_t", [["simplification", "for_polynomials", "with_minus"]])),
walther@59973:     (Problem.prep_input thy "pbl_vereinf_poly_klammer" [] Problem.id_empty
walther@59997:       (["klammer", "polynom", "vereinfachen"],
s1210629013@55339:         [("#Given" ,["Term t_t"]),
s1210629013@55339:           ("#Where" ,["t_t is_polyexp",
s1210629013@55339:             "Not (matchsub (?a * (?b + ?c)) t_t | " ^
s1210629013@55339:             "     matchsub (?a * (?b - ?c)) t_t | " ^
s1210629013@55339:             "     matchsub ((?b + ?c) * ?a) t_t | " ^
s1210629013@55339:             "     matchsub ((?b - ?c) * ?a) t_t )"]),
s1210629013@55339:           ("#Find"  ,["normalform n_n"])],
walther@59852:         Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty
walther@60278:           [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
walther@59878: 	           Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
walther@59871:              Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
s1210629013@55339:              (*"(?a | True) = True"*)
walther@59871:              Rule.Thm ("or_false", ThmC.numerals_to_Free @{thm or_false}),
s1210629013@55339:              (*"(?a | False) = ?a"*)
walther@59871:              Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
s1210629013@55339:              (*"(~ True) = False"*)
walther@59871:              Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
s1210629013@55339:              (*"(~ False) = True"*)], 
s1210629013@55339:         SOME "Vereinfache t_t", 
walther@59997:         [["simplification", "for_polynomials", "with_parentheses"]])),
walther@59973:     (Problem.prep_input thy "pbl_vereinf_poly_klammer_mal" [] Problem.id_empty
walther@59997:       (["binom_klammer", "polynom", "vereinfachen"],
s1210629013@55339:         [("#Given", ["Term t_t"]),
s1210629013@55339:           ("#Where", ["t_t is_polyexp"]),
s1210629013@55339:           ("#Find", ["normalform n_n"])],
walther@59852:         Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
walther@60278: 			      Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")], 
s1210629013@55339:         SOME "Vereinfache t_t", 
walther@59997:         [["simplification", "for_polynomials", "with_parentheses_mult"]])),
walther@59973:     (Problem.prep_input thy "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),
walther@59973:     (Problem.prep_input thy "pbl_probe_poly" [] Problem.id_empty
walther@59997:       (["polynom", "probe"],
s1210629013@55339:         [("#Given", ["Pruefe e_e", "mitWert w_w"]),
s1210629013@55339:           ("#Where", ["e_e is_polyexp"]),
s1210629013@55339:           ("#Find", ["Geprueft p_p"])],
walther@59852:         Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
walther@60278: 		      Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")], 
s1210629013@55339:         SOME "Probe e_e w_w", 
walther@59997:         [["probe", "fuer_polynom"]])),
walther@59973:     (Problem.prep_input thy "pbl_probe_bruch" [] Problem.id_empty
walther@59997:       (["bruch", "probe"],
s1210629013@55339:         [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
s1210629013@55339:           ("#Where" ,["e_e is_ratpolyexp"]),
s1210629013@55339:           ("#Find"  ,["Geprueft p_p"])],
walther@59852:         Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
walther@60278: 		      Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")], 
walther@59997:         SOME "Probe e_e w_w", [["probe", "fuer_bruch"]]))]\<close>
neuper@37950: 
neuper@37950: (** methods **)
wneuper@59545: 
wneuper@59504: partial_function (tailrec) simplify :: "real \<Rightarrow> real"
wneuper@59504:   where
walther@59635: "simplify t_t = (
walther@59635:   (Repeat(
walther@59637:     (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
walther@59637:     (Try (Rewrite_Set ''fasse_zusammen'')) #>
walther@59635:     (Try (Rewrite_Set ''verschoenere'')))
walther@59635:   ) t_t)"
wneuper@59472: setup \<open>KEStore_Elems.add_mets
walther@60154:     [MethodC.prep_input thy "met_simp_poly_minus" [] MethodC.id_empty
walther@59997: 	    (["simplification", "for_polynomials", "with_minus"],
s1210629013@55373: 	      [("#Given" ,["Term t_t"]),
s1210629013@55373: 	        ("#Where" ,["t_t is_polyexp",
s1210629013@55373: 	            "Not (matchsub (?a + (?b + ?c)) t_t | " ^
s1210629013@55373: 	            "     matchsub (?a + (?b - ?c)) t_t | " ^
s1210629013@55373: 	            "     matchsub (?a - (?b + ?c)) t_t | " ^
s1210629013@55373: 	            "     matchsub (?a + (?b - ?c)) t_t )"]),
s1210629013@55373: 	        ("#Find"  ,["normalform n_n"])],
walther@59852: 	      {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
walther@59852: 	        prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty 
walther@60278: 				      [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
walther@59878: 				        Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
walther@59871: 				        Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
s1210629013@55373:                 (*"(?a & True) = ?a"*)
walther@59871:                 Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
s1210629013@55373:                 (*"(?a & False) = False"*)
walther@59871:                 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
s1210629013@55373:                 (*"(~ True) = False"*)
walther@59871:                 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
s1210629013@55373:                 (*"(~ False) = True"*)],
walther@59852:           crls = Rule_Set.empty, errpats = [], nrls = rls_p_33},
wneuper@59551:           @{thm simplify.simps})]
wneuper@59473: \<close>
wneuper@59545: 
wneuper@59504: partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
wneuper@59504:   where
walther@59635: "simplify2 t_t = (
walther@59635:   (Repeat(
walther@59637:     (Try (Rewrite_Set ''klammern_aufloesen'')) #>
walther@59637:     (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
walther@59637:     (Try (Rewrite_Set ''fasse_zusammen'')) #>
walther@59635:     (Try (Rewrite_Set ''verschoenere'')))
walther@59635:   ) t_t)"
wneuper@59473: setup \<open>KEStore_Elems.add_mets
walther@60154:     [MethodC.prep_input thy "met_simp_poly_parenth" [] MethodC.id_empty
walther@59997: 	    (["simplification", "for_polynomials", "with_parentheses"],
s1210629013@55373: 	      [("#Given" ,["Term t_t"]),
s1210629013@55373: 	        ("#Where" ,["t_t is_polyexp"]),
s1210629013@55373: 	        ("#Find"  ,["normalform n_n"])],
walther@59852: 	      {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
walther@59852: 	        prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty 
walther@60278: 				    [(*for preds in where_*) Rule.Eval("Poly.is_polyexp", eval_is_polyexp"")],
walther@59852: 				  crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
wneuper@59551: 				@{thm simplify2.simps})]
wneuper@59473: \<close>
wneuper@59545: 
wneuper@59504: partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
wneuper@59504:   where
walther@59635: "simplify3 t_t = (
walther@59635:   (Repeat(
walther@59637:     (Try (Rewrite_Set ''klammern_ausmultiplizieren'')) #>
walther@59637:     (Try (Rewrite_Set ''discard_parentheses'')) #>
walther@59637:     (Try (Rewrite_Set ''ordne_monome'')) #>
walther@59637:     (Try (Rewrite_Set ''klammern_aufloesen'')) #>
walther@59637:     (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
walther@59637:     (Try (Rewrite_Set ''fasse_zusammen'')) #>
walther@59635:     (Try (Rewrite_Set ''verschoenere'')))
walther@59635:   ) t_t)"
wneuper@59473: setup \<open>KEStore_Elems.add_mets
walther@60154:     [MethodC.prep_input thy "met_simp_poly_parenth_mult" [] MethodC.id_empty
walther@59997: 	    (["simplification", "for_polynomials", "with_parentheses_mult"],
s1210629013@55373: 	      [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find"  ,["normalform n_n"])],
walther@59852: 	        {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
walther@59852: 	          prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty 
walther@60278: 				      [(*for preds in where_*) Rule.Eval("Poly.is_polyexp", eval_is_polyexp"")],
walther@59852: 				    crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
wneuper@59551: 				  @{thm simplify3.simps})]
wneuper@59473: \<close>
wneuper@59473: setup \<open>KEStore_Elems.add_mets
walther@60154:     [MethodC.prep_input thy "met_probe" [] MethodC.id_empty
s1210629013@55373: 	    (["probe"], [],
walther@59852: 	      {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
walther@59851: 	        errpats = [], nrls = Rule_Set.Empty}, 
wneuper@59545: 	      @{thm refl})]
wneuper@59473: \<close>
wneuper@59545: 
wneuper@59504: partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"
wneuper@59504:   where
walther@59635: "mache_probe e_e w_w = (
walther@59635:   let
walther@59635:      e_e = Take e_e;
walther@59635:      e_e = Substitute w_w e_e
walther@59635:   in (
walther@59635:     Repeat (
walther@59637:       (Try (Repeat (Calculate ''TIMES''))) #>
walther@59637:       (Try (Repeat (Calculate ''PLUS'' ))) #>
walther@59635:       (Try (Repeat (Calculate ''MINUS''))))
walther@59635:     ) e_e)"
wneuper@59473: setup \<open>KEStore_Elems.add_mets
walther@60154:     [MethodC.prep_input thy "met_probe_poly" [] MethodC.id_empty
walther@59997: 	    (["probe", "fuer_polynom"],
s1210629013@55373: 	      [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
s1210629013@55373: 	        ("#Where" ,["e_e is_polyexp"]),
s1210629013@55373: 	        ("#Find"  ,["Geprueft p_p"])],
walther@59852: 	      {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
walther@59852: 	        prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
walther@60278: 	            [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")], 
walther@59852: 	        crls = Rule_Set.empty, errpats = [], nrls = rechnen}, 
wneuper@59551: 	      @{thm mache_probe.simps})]
wneuper@59473: \<close>
wneuper@59473: setup \<open>KEStore_Elems.add_mets
walther@60154:     [MethodC.prep_input thy "met_probe_bruch" [] MethodC.id_empty
walther@59997: 	    (["probe", "fuer_bruch"],
s1210629013@55373: 	      [("#Given" ,["Pruefe e_e", "mitWert w_w"]),
s1210629013@55373: 	        ("#Where" ,["e_e is_ratpolyexp"]),
s1210629013@55373: 	        ("#Find"  ,["Geprueft p_p"])],
walther@59852: 	      {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
walther@59852: 	        prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
walther@60278: 	            [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")], 
walther@59852: 	        crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty}, 
wneuper@59545: 	      @{thm refl})]
walther@60278: \<close> ML \<open>
walther@60278: \<close> ML \<open>
wneuper@59472: \<close>
neuper@37906: 
neuper@37906: end
neuper@37906: