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 _") 
neuper@37906:   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@37906:   (*Script-name*)
neuper@37950:   ProbeScript :: "[bool, bool list,       bool] 
neuper@37950: 				      => bool"
neuper@37906:                   ("((Script ProbeScript (_ _ =))// (_))" 9)
neuper@37906: 
neuper@37906: rules
neuper@37906: 
neuper@37906:   null_minus            "0 - a = -a"
neuper@37906:   vor_minus_mal         "- a * b = (-a) * b"
neuper@37906: 
neuper@37906:   (*commute with invariant (a.b).c -association*)
neuper@37950:   tausche_plus		"[| b ist_monom; a kleiner b  |] ==> 
neuper@37950: 			 (b + a) = (a + b)"
neuper@37950:   tausche_minus		"[| b ist_monom; a kleiner b  |] ==> 
neuper@37950: 			 (b - a) = (-a + b)"
neuper@37950:   tausche_vor_plus	"[| b ist_monom; a kleiner b  |] ==> 
neuper@37950: 			 (- b + a) = (a - b)"
neuper@37950:   tausche_vor_minus	"[| b ist_monom; a kleiner b  |] ==> 
neuper@37950: 			 (- b - a) = (-a - b)"
neuper@37906:   tausche_plus_plus	"b kleiner c ==> (a + c + b) = (a + b + c)"
neuper@37906:   tausche_plus_minus	"b kleiner c ==> (a + c - b) = (a - b + c)"
neuper@37906:   tausche_minus_plus	"b kleiner c ==> (a - c + b) = (a + b - c)"
neuper@37906:   tausche_minus_minus	"b kleiner c ==> (a - c - b) = (a - b - c)"
neuper@37906: 
neuper@37906:   (*commute with invariant (a.b).c -association*)
neuper@37950:   tausche_mal		"[| b is_atom; a kleiner b  |] ==> 
neuper@37950: 			 (b * a) = (a * b)"
neuper@37950:   tausche_vor_mal	"[| b is_atom; a kleiner b  |] ==> 
neuper@37950: 			 (-b * a) = (-a * b)"
neuper@37950:   tausche_mal_mal	"[| c is_atom; b kleiner c  |] ==> 
neuper@37950: 			 (x * c * b) = (x * b * c)"
neuper@37906:   x_quadrat             "(x * a) * a = x * a ^^^ 2"
neuper@37906: 
neuper@37906: 
neuper@37950:   subtrahiere               "[| l is_const; m is_const |] ==>  
neuper@37950: 			     m * v - l * v = (m - l) * v"
neuper@37950:   subtrahiere_von_1         "[| l is_const |] ==>  
neuper@37950: 			     v - l * v = (1 - l) * v"
neuper@37950:   subtrahiere_1             "[| l is_const; m is_const |] ==>  
neuper@37950: 			     m * v - v = (m - 1) * v"
neuper@37906: 
neuper@37950:   subtrahiere_x_plus_minus  "[| l is_const; m is_const |] ==>  
neuper@37950: 			     (x + m * v) - l * v = x + (m - l) * v"
neuper@37950:   subtrahiere_x_plus1_minus "[| l is_const |] ==>  
neuper@37950: 			     (x + v) - l * v = x + (1 - l) * v"
neuper@37950:   subtrahiere_x_plus_minus1 "[| m is_const |] ==>  
neuper@37950: 			     (x + m * v) - v = x + (m - 1) * v"
neuper@37906: 
neuper@37950:   subtrahiere_x_minus_plus  "[| l is_const; m is_const |] ==>  
neuper@37950: 			     (x - m * v) + l * v = x + (-m + l) * v"
neuper@37950:   subtrahiere_x_minus1_plus "[| l is_const |] ==>  
neuper@37950: 			     (x - v) + l * v = x + (-1 + l) * v"
neuper@37950:   subtrahiere_x_minus_plus1 "[| m is_const |] ==>  
neuper@37950: 			     (x - m * v) + v = x + (-m + 1) * v"
neuper@37906: 
neuper@37950:   subtrahiere_x_minus_minus "[| l is_const; m is_const |] ==>  
neuper@37950: 			     (x - m * v) - l * v = x + (-m - l) * v"
neuper@37950:   subtrahiere_x_minus1_minus"[| l is_const |] ==>  
neuper@37950: 			     (x - v) - l * v = x + (-1 - l) * v"
neuper@37950:   subtrahiere_x_minus_minus1"[| m is_const |] ==>  
neuper@37950: 			     (x - m * v) - v = x + (-m - 1) * v"
neuper@37906: 
neuper@37906: 
neuper@37950:   addiere_vor_minus         "[| l is_const; m is_const |] ==>  
neuper@37950: 			     - (l * v) +  m * v = (-l + m) * v"
neuper@37950:   addiere_eins_vor_minus    "[| m is_const |] ==>  
neuper@37950: 			     -  v +  m * v = (-1 + m) * v"
neuper@37950:   subtrahiere_vor_minus     "[| l is_const; m is_const |] ==>  
neuper@37950: 			     - (l * v) -  m * v = (-l - m) * v"
neuper@37950:   subtrahiere_eins_vor_minus"[| m is_const |] ==>  
neuper@37950: 			     -  v -  m * v = (-1 - m) * v"
neuper@37906: 
neuper@37950:   vorzeichen_minus_weg1      "l kleiner 0 ==> a + l * b = a - -1*l * b"
neuper@37950:   vorzeichen_minus_weg2      "l kleiner 0 ==> a - l * b = a + -1*l * b"
neuper@37950:   vorzeichen_minus_weg3      "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b"
neuper@37950:   vorzeichen_minus_weg4      "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b"
neuper@37906: 
neuper@37906:   (*klammer_plus_plus = (real_add_assoc RS sym)*)
neuper@37950:   klammer_plus_minus          "a + (b - c) = (a + b) - c"
neuper@37950:   klammer_minus_plus          "a - (b + c) = (a - b) - c"
neuper@37950:   klammer_minus_minus         "a - (b - c) = (a - b) + c"
neuper@37906: 
neuper@37950:   klammer_mult_minus          "a * (b - c) = a * b - a * c"
neuper@37950:   klammer_minus_mult          "(b - c) * a = b * a - c * a"
neuper@37906: 
neuper@37950: ML {*
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 = 
neuper@37950:     let val s::ss = explode str
neuper@37950:     in implode ((chr (ord s + 1))::ss) end;
neuper@37950: fun identifier (Free (id,_)) = id                            (* 2,   a   *)
neuper@37950:   | identifier (Const ("op *", _) $ Free (num, _) $ Free (id, _)) = 
neuper@37950:     id                                                       (* 2*a, a*b *)
neuper@37950:   | identifier (Const ("op *", _) $                          (* 3*a*b    *)
neuper@37950: 		     (Const ("op *", _) $
neuper@37950: 			    Free (num, _) $ Free _) $ Free (id, _)) = 
neuper@37950:     if is_numeral num then id
neuper@37950:     else "|||||||||||||"
neuper@37950:   | identifier (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) =
neuper@37950:     if is_numeral base then "|||||||||||||"                  (* a^2      *)
neuper@37950:     else (*increase*) base
neuper@37950:   | identifier (Const ("op *", _) $ Free (num, _) $          (* 3*a^2    *)
neuper@37950: 		     (Const ("Atools.pow", _) $
neuper@37950: 			    Free (base, _) $ Free (exp, _))) = 
neuper@37950:     if is_numeral num andalso not (is_numeral 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)) _  =
neuper@37950:      if is_num b then
neuper@37950: 	 if is_num a then (*123 kleiner 32 = True !!!*)
neuper@37950: 	     if int_of_Free a < int_of_Free b then 
neuper@37950: 		 SOME ((term2str p) ^ " = True",
neuper@37950: 		       Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950: 	     else SOME ((term2str p) ^ " = False",
neuper@37950: 			Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37950: 	 else (* -1 * -2 kleiner 0 *)
neuper@37950: 	     SOME ((term2str p) ^ " = False",
neuper@37950: 		   Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37950:     else
neuper@37950: 	if identifier a < identifier b then 
neuper@37950: 	     SOME ((term2str p) ^ " = True",
neuper@37950: 		  Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950: 	else SOME ((term2str p) ^ " = False",
neuper@37950: 		   Trueprop $ (mk_equality (p, HOLogic.false_const)))
neuper@37950:   | eval_kleiner _ _ _ _ =  NONE;
neuper@37950: 
neuper@37950: fun ist_monom (Free (id,_)) = true
neuper@37950:   | ist_monom (Const ("op *", _) $ Free (num, _) $ Free (id, _)) = 
neuper@37950:     if is_numeral num then true else false
neuper@37950:   | ist_monom _ = false;
neuper@37950: (*. this function only accepts the most simple monoms       vvvvvvvvvv .*)
neuper@37950: fun ist_monom (Free (id,_)) = true                          (* 2,   a   *)
neuper@37950:   | ist_monom (Const ("op *", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
neuper@37950:     if is_numeral id then false else true
neuper@37950:   | ist_monom (Const ("op *", _) $                          (* 3*a*b    *)
neuper@37950: 		     (Const ("op *", _) $
neuper@37950: 			    Free (num, _) $ Free _) $ Free (id, _)) =
neuper@37950:     if is_numeral num andalso not (is_numeral id) then true else false
neuper@37950:   | ist_monom (Const ("Atools.pow", _) $ Free (base, _) $ Free (exp, _)) = 
neuper@37950:     true                                                    (* a^2      *)
neuper@37950:   | ist_monom (Const ("op *", _) $ Free (num, _) $          (* 3*a^2    *)
neuper@37950: 		     (Const ("Atools.pow", _) $
neuper@37950: 			    Free (base, _) $ Free (exp, _))) = 
neuper@37950:     if is_numeral num then true else false
neuper@37950:   | ist_monom _ = false;
neuper@37950: 
neuper@37950: (* is this a univariate monomial ? *)
neuper@37950: (*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)
neuper@37950: fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _  =
neuper@37950:     if ist_monom a  then 
neuper@37950: 	SOME ((term2str p) ^ " = True",
neuper@37950: 	      Trueprop $ (mk_equality (p, HOLogic.true_const)))
neuper@37950:     else SOME ((term2str p) ^ " = False",
neuper@37950: 	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
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 =
neuper@37950:     append_rls "erls_ordne_alphabetisch" e_rls
neuper@37950: 	       [Calc ("PolyMinus.kleiner", eval_kleiner ""),
neuper@37950: 		Calc ("PolyMinus.ist'_monom", eval_ist_monom "")
neuper@37950: 		];
neuper@37950: 
neuper@37950: val ordne_alphabetisch = 
neuper@37950:   Rls{id = "ordne_alphabetisch", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
neuper@37950:       erls = erls_ordne_alphabetisch, 
neuper@37950:       rules = [Thm ("tausche_plus",num_str tausche_plus),
neuper@37950: 	       (*"b kleiner a ==> (b + a) = (a + b)"*)
neuper@37950: 	       Thm ("tausche_minus",num_str tausche_minus),
neuper@37950: 	       (*"b kleiner a ==> (b - a) = (-a + b)"*)
neuper@37950: 	       Thm ("tausche_vor_plus",num_str tausche_vor_plus),
neuper@37950: 	       (*"[| b ist_monom; a kleiner b  |] ==> (- b + a) = (a - b)"*)
neuper@37950: 	       Thm ("tausche_vor_minus",num_str tausche_vor_minus),
neuper@37950: 	       (*"[| b ist_monom; a kleiner b  |] ==> (- b - a) = (-a - b)"*)
neuper@37950: 	       Thm ("tausche_plus_plus",num_str tausche_plus_plus),
neuper@37950: 	       (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
neuper@37950: 	       Thm ("tausche_plus_minus",num_str tausche_plus_minus),
neuper@37950: 	       (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
neuper@37950: 	       Thm ("tausche_minus_plus",num_str tausche_minus_plus),
neuper@37950: 	       (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
neuper@37950: 	       Thm ("tausche_minus_minus",num_str tausche_minus_minus)
neuper@37950: 	       (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: val fasse_zusammen = 
neuper@37950:     Rls{id = "fasse_zusammen", preconds = [], 
neuper@37950: 	rew_ord = ("dummy_ord", dummy_ord),
neuper@37950: 	erls = append_rls "erls_fasse_zusammen" e_rls 
neuper@37950: 			  [Calc ("Atools.is'_const",eval_const "#is_const_")], 
neuper@37950: 	srls = Erls, calc = [],
neuper@37950: 	rules = 
neuper@37950: 	[Thm ("real_num_collect",num_str real_num_collect), 
neuper@37950: 	 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
neuper@37950: 	 Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
neuper@37950: 	 (*"[| l is_const; m..|] ==>  (k + m * n) + l * n = k + (l + m)*n"*)
neuper@37950: 	 Thm ("real_one_collect",num_str real_one_collect),	
neuper@37950: 	 (*"m is_const ==> n + m * n = (1 + m) * n"*)
neuper@37950: 	 Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r), 
neuper@37950: 	 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
neuper@37950: 
neuper@37950: 
neuper@37950: 	 Thm ("subtrahiere",num_str subtrahiere),
neuper@37950: 	 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
neuper@37950: 	 Thm ("subtrahiere_von_1",num_str subtrahiere_von_1),
neuper@37950: 	 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
neuper@37950: 	 Thm ("subtrahiere_1",num_str subtrahiere_1),
neuper@37950: 	 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
neuper@37950: 
neuper@37950: 	 Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus), 
neuper@37950: 	 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
neuper@37950: 	 Thm ("subtrahiere_x_plus1_minus",num_str subtrahiere_x_plus1_minus),
neuper@37950: 	 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
neuper@37950: 	 Thm ("subtrahiere_x_plus_minus1",num_str subtrahiere_x_plus_minus1),
neuper@37950: 	 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
neuper@37950: 
neuper@37950: 	 Thm ("subtrahiere_x_minus_plus",num_str subtrahiere_x_minus_plus), 
neuper@37950: 	 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
neuper@37950: 	 Thm ("subtrahiere_x_minus1_plus",num_str subtrahiere_x_minus1_plus),
neuper@37950: 	 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
neuper@37950: 	 Thm ("subtrahiere_x_minus_plus1",num_str subtrahiere_x_minus_plus1),
neuper@37950: 	 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
neuper@37950: 
neuper@37950: 	 Thm ("subtrahiere_x_minus_minus",num_str subtrahiere_x_minus_minus), 
neuper@37950: 	 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
neuper@37950: 	 Thm ("subtrahiere_x_minus1_minus",num_str subtrahiere_x_minus1_minus),
neuper@37950: 	 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
neuper@37950: 	 Thm ("subtrahiere_x_minus_minus1",num_str subtrahiere_x_minus_minus1),
neuper@37950: 	 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
neuper@37950: 	 
neuper@37950: 	 Calc ("op +", eval_binop "#add_"),
neuper@37950: 	 Calc ("op -", eval_binop "#subtr_"),
neuper@37950: 	 
neuper@37950: 	 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
neuper@37950:            (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
neuper@37950: 	 Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
neuper@37950: 	 (*"(k + z1) + z1 = k + 2 * z1"*)
neuper@37950: 	 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
neuper@37950: 	 (*"z1 + z1 = 2 * z1"*)
neuper@37950: 
neuper@37950: 	 Thm ("addiere_vor_minus",num_str addiere_vor_minus),
neuper@37950: 	 (*"[| l is_const; m is_const |] ==> -(l * v) +  m * v = (-l + m) *v"*)
neuper@37950: 	 Thm ("addiere_eins_vor_minus",num_str addiere_eins_vor_minus),
neuper@37950: 	 (*"[| m is_const |] ==> -  v +  m * v = (-1 + m) * v"*)
neuper@37950: 	 Thm ("subtrahiere_vor_minus",num_str subtrahiere_vor_minus),
neuper@37950: 	 (*"[| l is_const; m is_const |] ==> -(l * v) -  m * v = (-l - m) *v"*)
neuper@37950: 	 Thm ("subtrahiere_eins_vor_minus",num_str subtrahiere_eins_vor_minus)
neuper@37950: 	 (*"[| m is_const |] ==> -  v -  m * v = (-1 - m) * v"*)
neuper@37950: 	 
neuper@37950: 	 ], scr = EmptyScr}:rls;
neuper@37950:     
neuper@37950: val verschoenere = 
neuper@37950:   Rls{id = "verschoenere", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
neuper@37950:       erls = append_rls "erls_verschoenere" e_rls 
neuper@37950: 			[Calc ("PolyMinus.kleiner", eval_kleiner "")], 
neuper@37950:       rules = [Thm ("vorzeichen_minus_weg1",num_str vorzeichen_minus_weg1),
neuper@37950: 	       (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
neuper@37950: 	       Thm ("vorzeichen_minus_weg2",num_str vorzeichen_minus_weg2),
neuper@37950: 	       (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
neuper@37950: 	       Thm ("vorzeichen_minus_weg3",num_str vorzeichen_minus_weg3),
neuper@37950: 	       (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
neuper@37950: 	       Thm ("vorzeichen_minus_weg4",num_str vorzeichen_minus_weg4),
neuper@37950: 	       (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
neuper@37950: 
neuper@37950: 	       Calc ("op *", eval_binop "#mult_"),
neuper@37950: 
neuper@37950: 	       Thm ("real_mult_0",num_str real_mult_0),    
neuper@37950: 	       (*"0 * z = 0"*)
neuper@37950: 	       Thm ("real_mult_1",num_str real_mult_1),     
neuper@37950: 	       (*"1 * z = z"*)
neuper@37950: 	       Thm ("real_add_zero_left",num_str real_add_zero_left),
neuper@37950: 	       (*"0 + z = z"*)
neuper@37950: 	       Thm ("null_minus",num_str null_minus),
neuper@37950: 	       (*"0 - a = -a"*)
neuper@37950: 	       Thm ("vor_minus_mal",num_str vor_minus_mal)
neuper@37950: 	       (*"- a * b = (-a) * b"*)
neuper@37950: 
neuper@37950: 	       (*Thm ("",num_str ),*)
neuper@37950: 	       (**)
neuper@37950: 	       ], scr = EmptyScr}:rls (*end verschoenere*);
neuper@37950: 
neuper@37950: val klammern_aufloesen = 
neuper@37950:   Rls{id = "klammern_aufloesen", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls, 
neuper@37950:       rules = [Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym)),
neuper@37950: 	       (*"a + (b + c) = (a + b) + c"*)
neuper@37950: 	       Thm ("klammer_plus_minus",num_str klammer_plus_minus),
neuper@37950: 	       (*"a + (b - c) = (a + b) - c"*)
neuper@37950: 	       Thm ("klammer_minus_plus",num_str klammer_minus_plus),
neuper@37950: 	       (*"a - (b + c) = (a - b) - c"*)
neuper@37950: 	       Thm ("klammer_minus_minus",num_str klammer_minus_minus)
neuper@37950: 	       (*"a - (b - c) = (a - b) + c"*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: val klammern_ausmultiplizieren = 
neuper@37950:   Rls{id = "klammern_ausmultiplizieren", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls, 
neuper@37950:       rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
neuper@37950: 	       (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
neuper@37950: 	       Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
neuper@37950: 	       (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
neuper@37950: 	       
neuper@37950: 	       Thm ("klammer_mult_minus",num_str klammer_mult_minus),
neuper@37950: 	       (*"a * (b - c) = a * b - a * c"*)
neuper@37950: 	       Thm ("klammer_minus_mult",num_str klammer_minus_mult)
neuper@37950: 	       (*"(b - c) * a = b * a - c * a"*)
neuper@37950: 
neuper@37950: 	       (*Thm ("",num_str ),
neuper@37950: 	       (*""*)*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: val ordne_monome = 
neuper@37950:   Rls{id = "ordne_monome", preconds = [], 
neuper@37950:       rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], 
neuper@37950:       erls = append_rls "erls_ordne_monome" e_rls
neuper@37950: 	       [Calc ("PolyMinus.kleiner", eval_kleiner ""),
neuper@37950: 		Calc ("Atools.is'_atom", eval_is_atom "")
neuper@37950: 		], 
neuper@37950:       rules = [Thm ("tausche_mal",num_str tausche_mal),
neuper@37950: 	       (*"[| b is_atom; a kleiner b  |] ==> (b * a) = (a * b)"*)
neuper@37950: 	       Thm ("tausche_vor_mal",num_str tausche_vor_mal),
neuper@37950: 	       (*"[| b is_atom; a kleiner b  |] ==> (-b * a) = (-a * b)"*)
neuper@37950: 	       Thm ("tausche_mal_mal",num_str tausche_mal_mal),
neuper@37950: 	       (*"[| c is_atom; b kleiner c  |] ==> (a * c * b) = (a * b *c)"*)
neuper@37950: 	       Thm ("x_quadrat",num_str x_quadrat)
neuper@37950: 	       (*"(x * a) * a = x * a ^^^ 2"*)
neuper@37950: 
neuper@37950: 	       (*Thm ("",num_str ),
neuper@37950: 	       (*""*)*)
neuper@37950: 	       ], scr = EmptyScr}:rls;
neuper@37950: 
neuper@37950: 
neuper@37950: val rls_p_33 = 
neuper@37950:     append_rls "rls_p_33" e_rls
neuper@37950: 	       [Rls_ ordne_alphabetisch,
neuper@37950: 		Rls_ fasse_zusammen,
neuper@37950: 		Rls_ verschoenere
neuper@37950: 		];
neuper@37950: val rls_p_34 = 
neuper@37950:     append_rls "rls_p_34" e_rls
neuper@37950: 	       [Rls_ klammern_aufloesen,
neuper@37950: 		Rls_ ordne_alphabetisch,
neuper@37950: 		Rls_ fasse_zusammen,
neuper@37950: 		Rls_ verschoenere
neuper@37950: 		];
neuper@37950: val rechnen = 
neuper@37950:     append_rls "rechnen" e_rls
neuper@37950: 	       [Calc ("op *", eval_binop "#mult_"),
neuper@37950: 		Calc ("op +", eval_binop "#add_"),
neuper@37950: 		Calc ("op -", eval_binop "#subtr_")
neuper@37950: 		];
neuper@37950: 
neuper@37950: ruleset' := 
neuper@37950: overwritelthy thy (!ruleset',
neuper@37950: 		   [("ordne_alphabetisch", prep_rls ordne_alphabetisch),
neuper@37950: 		    ("fasse_zusammen", prep_rls fasse_zusammen),
neuper@37950: 		    ("verschoenere", prep_rls verschoenere),
neuper@37950: 		    ("ordne_monome", prep_rls ordne_monome),
neuper@37950: 		    ("klammern_aufloesen", prep_rls klammern_aufloesen),
neuper@37950: 		    ("klammern_ausmultiplizieren", 
neuper@37950: 		     prep_rls klammern_ausmultiplizieren)
neuper@37950: 		    ]);
neuper@37950: 
neuper@37950: (** problems **)
neuper@37950: 
neuper@37950: store_pbt
neuper@37950:  (prep_pbt PolyMinus.thy "pbl_vereinf_poly" [] e_pblID
neuper@37950:  (["polynom","vereinfachen"],
neuper@37950:   [], Erls, NONE, []));
neuper@37950: 
neuper@37950: store_pbt
neuper@37950:  (prep_pbt PolyMinus.thy "pbl_vereinf_poly_minus" [] e_pblID
neuper@37950:  (["plus_minus","polynom","vereinfachen"],
neuper@37950:   [("#Given" ,["term t_"]),
neuper@37950:    ("#Where" ,["t_ is_polyexp",
neuper@37950: 	       "Not (matchsub (?a + (?b + ?c)) t_ | " ^
neuper@37950: 	       "     matchsub (?a + (?b - ?c)) t_ | " ^
neuper@37950: 	       "     matchsub (?a - (?b + ?c)) t_ | " ^
neuper@37950: 	       "     matchsub (?a + (?b - ?c)) t_ )",
neuper@37950: 	       "Not (matchsub (?a * (?b + ?c)) t_ | " ^
neuper@37950: 	       "     matchsub (?a * (?b - ?c)) t_ | " ^
neuper@37950: 	       "     matchsub ((?b + ?c) * ?a) t_ | " ^
neuper@37950: 	       "     matchsub ((?b - ?c) * ?a) t_ )"]),
neuper@37950:    ("#Find"  ,["normalform n_"])
neuper@37950:   ],
neuper@37950:   append_rls "prls_pbl_vereinf_poly" e_rls 
neuper@37950: 	     [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
neuper@37950: 	      Calc ("Tools.matchsub", eval_matchsub ""),
neuper@37950: 	      Thm ("or_true",or_true),
neuper@37950: 	      (*"(?a | True) = True"*)
neuper@37950: 	      Thm ("or_false",or_false),
neuper@37950: 	      (*"(?a | False) = ?a"*)
neuper@37950: 	      Thm ("not_true",num_str not_true),
neuper@37950: 	      (*"(~ True) = False"*)
neuper@37950: 	      Thm ("not_false",num_str not_false)
neuper@37950: 	      (*"(~ False) = True"*)], 
neuper@37950:   SOME "Vereinfache t_", 
neuper@37950:   [["simplification","for_polynomials","with_minus"]]));
neuper@37950: 
neuper@37950: store_pbt
neuper@37950:  (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer" [] e_pblID
neuper@37950:  (["klammer","polynom","vereinfachen"],
neuper@37950:   [("#Given" ,["term t_"]),
neuper@37950:    ("#Where" ,["t_ is_polyexp",
neuper@37950: 	       "Not (matchsub (?a * (?b + ?c)) t_ | " ^
neuper@37950: 	       "     matchsub (?a * (?b - ?c)) t_ | " ^
neuper@37950: 	       "     matchsub ((?b + ?c) * ?a) t_ | " ^
neuper@37950: 	       "     matchsub ((?b - ?c) * ?a) t_ )"]),
neuper@37950:    ("#Find"  ,["normalform n_"])
neuper@37950:   ],
neuper@37950:   append_rls "prls_pbl_vereinf_poly_klammer" e_rls [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
neuper@37950: 	      Calc ("Tools.matchsub", eval_matchsub ""),
neuper@37950: 	      Thm ("or_true",or_true),
neuper@37950: 	      (*"(?a | True) = True"*)
neuper@37950: 	      Thm ("or_false",or_false),
neuper@37950: 	      (*"(?a | False) = ?a"*)
neuper@37950: 	      Thm ("not_true",num_str not_true),
neuper@37950: 	      (*"(~ True) = False"*)
neuper@37950: 	      Thm ("not_false",num_str not_false)
neuper@37950: 	      (*"(~ False) = True"*)], 
neuper@37950:   SOME "Vereinfache t_", 
neuper@37950:   [["simplification","for_polynomials","with_parentheses"]]));
neuper@37950: 
neuper@37950: store_pbt
neuper@37950:  (prep_pbt PolyMinus.thy "pbl_vereinf_poly_klammer_mal" [] e_pblID
neuper@37950:  (["binom_klammer","polynom","vereinfachen"],
neuper@37950:   [("#Given" ,["term t_"]),
neuper@37950:    ("#Where" ,["t_ is_polyexp"]),
neuper@37950:    ("#Find"  ,["normalform n_"])
neuper@37950:   ],
neuper@37950:   append_rls "e_rls" e_rls [(*for preds in where_*)
neuper@37950: 			    Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 
neuper@37950:   SOME "Vereinfache t_", 
neuper@37950:   [["simplification","for_polynomials","with_parentheses_mult"]]));
neuper@37950: 
neuper@37950: store_pbt
neuper@37950:  (prep_pbt PolyMinus.thy "pbl_probe" [] e_pblID
neuper@37950:  (["probe"],
neuper@37950:   [], Erls, NONE, []));
neuper@37950: 
neuper@37950: store_pbt
neuper@37950:  (prep_pbt PolyMinus.thy "pbl_probe_poly" [] e_pblID
neuper@37950:  (["polynom","probe"],
neuper@37950:   [("#Given" ,["Pruefe e_", "mitWert ws_"]),
neuper@37950:    ("#Where" ,["e_ is_polyexp"]),
neuper@37950:    ("#Find"  ,["Geprueft p_"])
neuper@37950:   ],
neuper@37950:   append_rls "prls_pbl_probe_poly" 
neuper@37950: 	     e_rls [(*for preds in where_*)
neuper@37950: 		    Calc ("Poly.is'_polyexp", eval_is_polyexp "")], 
neuper@37950:   SOME "Probe e_ ws_", 
neuper@37950:   [["probe","fuer_polynom"]]));
neuper@37950: 
neuper@37950: store_pbt
neuper@37950:  (prep_pbt PolyMinus.thy "pbl_probe_bruch" [] e_pblID
neuper@37950:  (["bruch","probe"],
neuper@37950:   [("#Given" ,["Pruefe e_", "mitWert ws_"]),
neuper@37950:    ("#Where" ,["e_ is_ratpolyexp"]),
neuper@37950:    ("#Find"  ,["Geprueft p_"])
neuper@37950:   ],
neuper@37950:   append_rls "prls_pbl_probe_bruch"
neuper@37950: 	     e_rls [(*for preds in where_*)
neuper@37950: 		    Calc ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")], 
neuper@37950:   SOME "Probe e_ ws_", 
neuper@37950:   [["probe","fuer_bruch"]]));
neuper@37950: 
neuper@37950: 
neuper@37950: (** methods **)
neuper@37950: 
neuper@37950: store_met
neuper@37950:     (prep_met PolyMinus.thy "met_simp_poly_minus" [] e_metID
neuper@37950: 	      (["simplification","for_polynomials","with_minus"],
neuper@37950: 	       [("#Given" ,["term t_"]),
neuper@37950: 		("#Where" ,["t_ is_polyexp",
neuper@37950: 	       "Not (matchsub (?a + (?b + ?c)) t_ | " ^
neuper@37950: 	       "     matchsub (?a + (?b - ?c)) t_ | " ^
neuper@37950: 	       "     matchsub (?a - (?b + ?c)) t_ | " ^
neuper@37950: 	       "     matchsub (?a + (?b - ?c)) t_ )"]),
neuper@37950: 		("#Find"  ,["normalform n_"])
neuper@37950: 		],
neuper@37950: 	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 
neuper@37950: 		prls = append_rls "prls_met_simp_poly_minus" e_rls 
neuper@37950: 				  [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
neuper@37950: 	      Calc ("Tools.matchsub", eval_matchsub ""),
neuper@37950: 	      Thm ("and_true",and_true),
neuper@37950: 	      (*"(?a & True) = ?a"*)
neuper@37950: 	      Thm ("and_false",and_false),
neuper@37950: 	      (*"(?a & False) = False"*)
neuper@37950: 	      Thm ("not_true",num_str not_true),
neuper@37950: 	      (*"(~ True) = False"*)
neuper@37950: 	      Thm ("not_false",num_str not_false)
neuper@37950: 	      (*"(~ False) = True"*)],
neuper@37950: 		crls = e_rls, nrls = rls_p_33},
neuper@37950: "Script SimplifyScript (t_::real) =                   " ^
neuper@37950: "  ((Repeat((Try (Rewrite_Set ordne_alphabetisch False)) @@  " ^
neuper@37950: "           (Try (Rewrite_Set fasse_zusammen     False)) @@  " ^
neuper@37950: "           (Try (Rewrite_Set verschoenere       False)))) t_)"
neuper@37950: 	       ));
neuper@37950: 
neuper@37950: store_met
neuper@37950:     (prep_met PolyMinus.thy "met_simp_poly_parenth" [] e_metID
neuper@37950: 	      (["simplification","for_polynomials","with_parentheses"],
neuper@37950: 	       [("#Given" ,["term t_"]),
neuper@37950: 		("#Where" ,["t_ is_polyexp"]),
neuper@37950: 		("#Find"  ,["normalform n_"])
neuper@37950: 		],
neuper@37950: 	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 
neuper@37950: 		prls = append_rls "simplification_for_polynomials_prls" e_rls 
neuper@37950: 				  [(*for preds in where_*)
neuper@37950: 				   Calc("Poly.is'_polyexp",eval_is_polyexp"")],
neuper@37950: 		crls = e_rls, nrls = rls_p_34},
neuper@37950: "Script SimplifyScript (t_::real) =                          " ^
neuper@37950: "  ((Repeat((Try (Rewrite_Set klammern_aufloesen False)) @@  " ^
neuper@37950: "           (Try (Rewrite_Set ordne_alphabetisch False)) @@  " ^
neuper@37950: "           (Try (Rewrite_Set fasse_zusammen     False)) @@  " ^
neuper@37950: "           (Try (Rewrite_Set verschoenere       False)))) t_)"
neuper@37950: 	       ));
neuper@37950: 
neuper@37950: store_met
neuper@37950:     (prep_met PolyMinus.thy "met_simp_poly_parenth_mult" [] e_metID
neuper@37950: 	      (["simplification","for_polynomials","with_parentheses_mult"],
neuper@37950: 	       [("#Given" ,["term t_"]),
neuper@37950: 		("#Where" ,["t_ is_polyexp"]),
neuper@37950: 		("#Find"  ,["normalform n_"])
neuper@37950: 		],
neuper@37950: 	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 
neuper@37950: 		prls = append_rls "simplification_for_polynomials_prls" e_rls 
neuper@37950: 				  [(*for preds in where_*)
neuper@37950: 				   Calc("Poly.is'_polyexp",eval_is_polyexp"")],
neuper@37950: 		crls = e_rls, nrls = rls_p_34},
neuper@37950: "Script SimplifyScript (t_::real) =                          " ^
neuper@37950: "  ((Repeat((Try (Rewrite_Set klammern_ausmultiplizieren False)) @@ " ^
neuper@37950: "           (Try (Rewrite_Set discard_parentheses        False)) @@ " ^
neuper@37950: "           (Try (Rewrite_Set ordne_monome               False)) @@ " ^
neuper@37950: "           (Try (Rewrite_Set klammern_aufloesen         False)) @@ " ^
neuper@37950: "           (Try (Rewrite_Set ordne_alphabetisch         False)) @@ " ^
neuper@37950: "           (Try (Rewrite_Set fasse_zusammen             False)) @@ " ^
neuper@37950: "           (Try (Rewrite_Set verschoenere               False)))) t_)"
neuper@37950: 	       ));
neuper@37950: 
neuper@37950: store_met
neuper@37950:     (prep_met PolyMinus.thy "met_probe" [] e_metID
neuper@37950: 	      (["probe"],
neuper@37950: 	       [],
neuper@37950: 	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 
neuper@37950: 		prls = Erls, crls = e_rls, nrls = Erls}, 
neuper@37950: 	       "empty_script"));
neuper@37950: 
neuper@37950: store_met
neuper@37950:     (prep_met PolyMinus.thy "met_probe_poly" [] e_metID
neuper@37950: 	      (["probe","fuer_polynom"],
neuper@37950: 	       [("#Given" ,["Pruefe e_", "mitWert ws_"]),
neuper@37950: 		("#Where" ,["e_ is_polyexp"]),
neuper@37950: 		("#Find"  ,["Geprueft p_"])
neuper@37950: 		],
neuper@37950: 	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 
neuper@37950: 		prls = append_rls "prls_met_probe_bruch"
neuper@37950: 				  e_rls [(*for preds in where_*)
neuper@37950: 					 Calc ("Rational.is'_ratpolyexp", 
neuper@37950: 					       eval_is_ratpolyexp "")], 
neuper@37950: 		crls = e_rls, nrls = rechnen}, 
neuper@37950: "Script ProbeScript (e_::bool) (ws_::bool list) = " ^
neuper@37950: " (let e_ = Take e_;                              " ^
neuper@37950: "      e_ = Substitute ws_ e_                     " ^
neuper@37950: " in (Repeat((Try (Repeat (Calculate times))) @@  " ^
neuper@37950: "            (Try (Repeat (Calculate plus ))) @@  " ^
neuper@37950: "            (Try (Repeat (Calculate minus))))) e_)"
neuper@37950: ));
neuper@37950: 
neuper@37950: store_met
neuper@37950:     (prep_met PolyMinus.thy "met_probe_bruch" [] e_metID
neuper@37950: 	      (["probe","fuer_bruch"],
neuper@37950: 	       [("#Given" ,["Pruefe e_", "mitWert ws_"]),
neuper@37950: 		("#Where" ,["e_ is_ratpolyexp"]),
neuper@37950: 		("#Find"  ,["Geprueft p_"])
neuper@37950: 		],
neuper@37950: 	       {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, 
neuper@37950: 		prls = append_rls "prls_met_probe_bruch"
neuper@37950: 				  e_rls [(*for preds in where_*)
neuper@37950: 					 Calc ("Rational.is'_ratpolyexp", 
neuper@37950: 					       eval_is_ratpolyexp "")], 
neuper@37950: 		crls = e_rls, nrls = Erls}, 
neuper@37950: 	       "empty_script"));
neuper@37950: *}
neuper@37906: 
neuper@37906: end
neuper@37906: