src/Tools/isac/Knowledge/PolyMinus.thy
author wneuper <walther.neuper@jku.at>
Tue, 10 Aug 2021 09:43:07 +0200
changeset 60358 8377b6c37640
parent 60351 d74e7e33db35
child 60360 49680d595342
permissions -rw-r--r--
complete replacement of Rule.Thm/Eval by \<^rule_thm> and \<^rule_eval> in src/*
neuper@37906
     1
(* attempts to perserve binary minus as wanted by Austrian teachers
neuper@37906
     2
   WN071207
neuper@37906
     3
   (c) due to copyright terms
neuper@37906
     4
*)
neuper@37906
     5
neuper@37950
     6
theory PolyMinus imports (*Poly// due to "is_ratpolyexp" in...*) Rational begin
neuper@37906
     7
neuper@37906
     8
consts
neuper@37906
     9
neuper@37906
    10
  (*predicates for conditions in rewriting*)
neuper@37906
    11
  kleiner     :: "['a, 'a] => bool" 	("_ kleiner _") 
walther@60278
    12
  ist_monom  :: "'a => bool"		("_ ist'_monom")
neuper@37906
    13
neuper@37906
    14
  (*the CAS-command*)
neuper@37906
    15
  Probe       :: "[bool, bool list] => bool"  
neuper@37906
    16
	(*"Probe (3*a+2*b+a = 4*a+2*b) [a=1,b=2]"*)
neuper@37906
    17
neuper@37906
    18
  (*descriptions for the pbl and met*)
neuper@37950
    19
  Pruefe      :: "bool => una"
neuper@37950
    20
  mitWert     :: "bool list => tobooll"
neuper@37950
    21
  Geprueft    :: "bool => una"
neuper@37906
    22
neuper@52148
    23
axiomatization where
neuper@37906
    24
neuper@52148
    25
  null_minus:            "0 - a = -a" and
neuper@52148
    26
  vor_minus_mal:         "- a * b = (-a) * b" and
neuper@37906
    27
neuper@37906
    28
  (*commute with invariant (a.b).c -association*)
neuper@37980
    29
  tausche_plus:		"[| b ist_monom; a kleiner b  |] ==> 
neuper@52148
    30
			 (b + a) = (a + b)" and
neuper@37980
    31
  tausche_minus:		"[| b ist_monom; a kleiner b  |] ==> 
neuper@52148
    32
			 (b - a) = (-a + b)" and
neuper@37980
    33
  tausche_vor_plus:	"[| b ist_monom; a kleiner b  |] ==> 
neuper@52148
    34
			 (- b + a) = (a - b)" and
neuper@37980
    35
  tausche_vor_minus:	"[| b ist_monom; a kleiner b  |] ==> 
neuper@52148
    36
			 (- b - a) = (-a - b)" and
walther@60269
    37
(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
neuper@52148
    38
  tausche_plus_plus:	"b kleiner c ==> (a + c + b) = (a + b + c)" and
neuper@52148
    39
  tausche_plus_minus:	"b kleiner c ==> (a + c - b) = (a - b + c)" and
neuper@52148
    40
  tausche_minus_plus:	"b kleiner c ==> (a - c + b) = (a + b - c)" and
neuper@52148
    41
  tausche_minus_minus:	"b kleiner c ==> (a - c - b) = (a - b - c)" and
walther@60269
    42
(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
neuper@37906
    43
neuper@37906
    44
  (*commute with invariant (a.b).c -association*)
neuper@37980
    45
  tausche_mal:		"[| b is_atom; a kleiner b  |] ==> 
neuper@52148
    46
			 (b * a) = (a * b)" and
neuper@37980
    47
  tausche_vor_mal:	"[| b is_atom; a kleiner b  |] ==> 
neuper@52148
    48
			 (-b * a) = (-a * b)" and
neuper@37980
    49
  tausche_mal_mal:	"[| c is_atom; b kleiner c  |] ==> 
neuper@52148
    50
			 (x * c * b) = (x * b * c)" and
walther@60242
    51
  x_quadrat:             "(x * a) * a = x * a \<up> 2" and
neuper@37906
    52
neuper@37906
    53
neuper@37980
    54
  subtrahiere:               "[| l is_const; m is_const |] ==>  
neuper@52148
    55
			     m * v - l * v = (m - l) * v" and
neuper@37980
    56
  subtrahiere_von_1:         "[| l is_const |] ==>  
neuper@52148
    57
			     v - l * v = (1 - l) * v" and
neuper@37980
    58
  subtrahiere_1:             "[| l is_const; m is_const |] ==>  
neuper@52148
    59
			     m * v - v = (m - 1) * v" and
neuper@37906
    60
neuper@37980
    61
  subtrahiere_x_plus_minus:  "[| l is_const; m is_const |] ==>  
neuper@52148
    62
			     (x + m * v) - l * v = x + (m - l) * v" and
neuper@37980
    63
  subtrahiere_x_plus1_minus: "[| l is_const |] ==>  
neuper@52148
    64
			     (x + v) - l * v = x + (1 - l) * v" and
neuper@37980
    65
  subtrahiere_x_plus_minus1: "[| m is_const |] ==>  
neuper@52148
    66
			     (x + m * v) - v = x + (m - 1) * v" and
neuper@37906
    67
neuper@37980
    68
  subtrahiere_x_minus_plus:  "[| l is_const; m is_const |] ==>  
neuper@52148
    69
			     (x - m * v) + l * v = x + (-m + l) * v" and
neuper@37980
    70
  subtrahiere_x_minus1_plus: "[| l is_const |] ==>  
neuper@52148
    71
			     (x - v) + l * v = x + (-1 + l) * v" and
neuper@37980
    72
  subtrahiere_x_minus_plus1: "[| m is_const |] ==>  
neuper@52148
    73
			     (x - m * v) + v = x + (-m + 1) * v" and
neuper@37906
    74
neuper@37980
    75
  subtrahiere_x_minus_minus: "[| l is_const; m is_const |] ==>  
neuper@52148
    76
			     (x - m * v) - l * v = x + (-m - l) * v" and
neuper@37980
    77
  subtrahiere_x_minus1_minus:"[| l is_const |] ==>  
neuper@52148
    78
			     (x - v) - l * v = x + (-1 - l) * v" and
neuper@37980
    79
  subtrahiere_x_minus_minus1:"[| m is_const |] ==>  
neuper@52148
    80
			     (x - m * v) - v = x + (-m - 1) * v" and
neuper@37906
    81
neuper@37906
    82
neuper@37980
    83
  addiere_vor_minus:         "[| l is_const; m is_const |] ==>  
neuper@52148
    84
			     - (l * v) +  m * v = (-l + m) * v" and
neuper@37980
    85
  addiere_eins_vor_minus:    "[| m is_const |] ==>  
neuper@52148
    86
			     -  v +  m * v = (-1 + m) * v" and
neuper@37980
    87
  subtrahiere_vor_minus:     "[| l is_const; m is_const |] ==>  
neuper@52148
    88
			     - (l * v) -  m * v = (-l - m) * v" and
neuper@37980
    89
  subtrahiere_eins_vor_minus:"[| m is_const |] ==>  
neuper@52148
    90
			     -  v -  m * v = (-1 - m) * v" and
neuper@37906
    91
walther@60269
    92
(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
neuper@52148
    93
  vorzeichen_minus_weg1:      "l kleiner 0 ==> a + l * b = a - -1*l * b" and
neuper@52148
    94
  vorzeichen_minus_weg2:      "l kleiner 0 ==> a - l * b = a + -1*l * b" and
neuper@52148
    95
  vorzeichen_minus_weg3:      "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and
neuper@52148
    96
  vorzeichen_minus_weg4:      "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and
walther@60269
    97
(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
neuper@37906
    98
walther@59877
    99
  (*klammer_plus_plus = (add.assoc RS sym)*)
neuper@52148
   100
  klammer_plus_minus:          "a + (b - c) = (a + b) - c" and
neuper@52148
   101
  klammer_minus_plus:          "a - (b + c) = (a - b) - c" and
neuper@52148
   102
  klammer_minus_minus:         "a - (b - c) = (a - b) + c" and
neuper@37906
   103
neuper@52148
   104
  klammer_mult_minus:          "a * (b - c) = a * b - a * c" and
neuper@37980
   105
  klammer_minus_mult:          "(b - c) * a = b * a - c * a"
neuper@37906
   106
wneuper@59472
   107
ML \<open>
neuper@37972
   108
val thy = @{theory};
neuper@37972
   109
neuper@37950
   110
(** eval functions **)
neuper@37906
   111
neuper@37950
   112
(*. get the identifier from specific monomials; see fun ist_monom .*)
walther@60351
   113
fun Free_to_string (Free (str, _)) = str
walther@60351
   114
  | Free_to_string t =
walther@60351
   115
    if TermC.is_num t then TermC.string_of_num t else "|||||||||||||"(*the "largest" string*);
walther@60351
   116
walther@60351
   117
(* quick and dirty solution just before a field test *)
walther@60351
   118
fun identifier (Free (id,_)) = id                                   (* _a_                   *)
walther@60351
   119
  | identifier (Const (\<^const_name>\<open>times\<close>, _) $ t1 $ t2) =           (* 2*_a_, a*_b_, 3*a*_b_ *)
walther@60351
   120
    if TermC.is_atom t2 
walther@60351
   121
    then Free_to_string t2
walther@60351
   122
    else
walther@60351
   123
      (case t1 of
walther@60351
   124
        Const (\<^const_name>\<open>times\<close>, _) $ num $ t1' =>                 (* 3*_a_ \<up> 2             *)
walther@60351
   125
          if TermC.is_atom num andalso TermC.is_atom t1' then Free_to_string t2
walther@60351
   126
          else "|||||||||||||"
walther@60351
   127
      | _ => 
walther@60351
   128
        (case t2 of
walther@60351
   129
          Const (\<^const_name>\<open>powr\<close>, _) $ base $ exp => 
walther@60351
   130
            if TermC.is_atom base andalso TermC.is_atom exp then
walther@60351
   131
              if TermC.is_num base then "|||||||||||||"
walther@60351
   132
              else Free_to_string base
walther@60351
   133
            else "|||||||||||||"
walther@60351
   134
      | _ => "|||||||||||||"))
walther@60351
   135
  | identifier (Const (\<^const_name>\<open>powr\<close>, _) $ base $ exp) =         (* _a_\<up>2, _3_^2          *)
walther@60351
   136
    if TermC.is_atom base andalso TermC.is_atom exp then Free_to_string base
neuper@37950
   137
    else "|||||||||||||"
walther@60351
   138
  | identifier t =                                                   (* 12                    *)
walther@60351
   139
    if TermC.is_num t
walther@60351
   140
    then TermC.string_of_num t
walther@60351
   141
    else "|||||||||||||" (*the "largest" string*);
neuper@37950
   142
neuper@37950
   143
(*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
neuper@37950
   144
(* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
walther@60335
   145
fun eval_kleiner _ _ (p as (Const (\<^const_name>\<open>PolyMinus.kleiner\<close>,_) $ a $ b)) _  =
walther@60325
   146
    if TermC.is_num b then
walther@60325
   147
  	  if TermC.is_num a then (*123 kleiner 32 = True !!!*)
walther@60325
   148
  	    if TermC.num_of_term a < TermC.num_of_term b then 
walther@60325
   149
  		    SOME ((UnparseC.term p) ^ " = True", 
walther@60325
   150
            HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
walther@60325
   151
  	    else SOME ((UnparseC.term p) ^ " = False",
walther@60325
   152
  			  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
walther@60325
   153
  	  else (* -1 * -2 kleiner 0 *)
walther@60325
   154
  	    SOME ((UnparseC.term p) ^ " = False",
walther@60325
   155
  		    HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
neuper@37950
   156
    else
walther@60325
   157
    	if identifier a < identifier b then 
walther@60325
   158
    	  SOME ((UnparseC.term p) ^ " = True",
walther@60325
   159
    		  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
walther@60325
   160
    	else SOME ((UnparseC.term p) ^ " = False",
walther@60325
   161
    		HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
neuper@37950
   162
  | eval_kleiner _ _ _ _ =  NONE;
neuper@37950
   163
walther@60325
   164
fun ist_monom t =
walther@60325
   165
  if TermC.is_atom t then true
walther@60325
   166
  else
walther@60325
   167
    case t of
walther@60335
   168
      Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ t1 $ t2 =>
walther@60325
   169
        ist_monom t1 andalso ist_monom t2
walther@60335
   170
    | Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ t1 $ t2 =>
walther@60325
   171
        ist_monom t1 andalso ist_monom t2
walther@60325
   172
    | _ => false
neuper@37950
   173
neuper@37950
   174
(* is this a univariate monomial ? *)
walther@60278
   175
(*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*)
walther@60335
   176
fun eval_ist_monom _ _ (p as (Const (\<^const_name>\<open>PolyMinus.ist_monom\<close>,_) $ a)) _  =
neuper@37950
   177
    if ist_monom a  then 
walther@59868
   178
	SOME ((UnparseC.term p) ^ " = True",
wneuper@59390
   179
	      HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
walther@59868
   180
    else SOME ((UnparseC.term p) ^ " = False",
wneuper@59390
   181
	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
neuper@37950
   182
  | eval_ist_monom _ _ _ _ =  NONE;
neuper@37950
   183
neuper@37950
   184
neuper@37950
   185
(** rewrite order **)
neuper@37950
   186
neuper@37950
   187
(** rulesets **)
neuper@37950
   188
neuper@37950
   189
val erls_ordne_alphabetisch =
walther@60358
   190
  Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty [
walther@60358
   191
    \<^rule_eval>\<open>kleiner\<close> (eval_kleiner ""),
walther@60358
   192
    \<^rule_eval>\<open>ist_monom\<close> (eval_ist_monom "")];
neuper@37950
   193
neuper@37950
   194
val ordne_alphabetisch = 
walther@59851
   195
  Rule_Def.Repeat{id = "ordne_alphabetisch", preconds = [], 
walther@60358
   196
    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358
   197
    erls = erls_ordne_alphabetisch, 
walther@60358
   198
    rules = [
walther@60358
   199
      \<^rule_thm>\<open>tausche_plus\<close>, (*"b kleiner a ==> (b + a) = (a + b)"*)
walther@60358
   200
      \<^rule_thm>\<open>tausche_minus\<close>, (*"b kleiner a ==> (b - a) = (-a + b)"*)
walther@60358
   201
      \<^rule_thm>\<open>tausche_vor_plus\<close>, (*"[| b ist_monom; a kleiner b  |] ==> (- b + a) = (a - b)"*)
walther@60358
   202
      \<^rule_thm>\<open>tausche_vor_minus\<close>, (*"[| b ist_monom; a kleiner b  |] ==> (- b - a) = (-a - b)"*)
walther@60358
   203
      \<^rule_thm>\<open>tausche_plus_plus\<close>, (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
walther@60358
   204
      \<^rule_thm>\<open>tausche_plus_minus\<close>, (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
walther@60358
   205
      \<^rule_thm>\<open>tausche_minus_plus\<close>, (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
walther@60358
   206
      \<^rule_thm>\<open>tausche_minus_minus\<close>], (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
walther@60358
   207
    scr = Rule.Empty_Prog};
neuper@37950
   208
neuper@37950
   209
val fasse_zusammen = 
walther@60358
   210
  Rule_Def.Repeat{id = "fasse_zusammen", preconds = [], 
walther@60358
   211
	  rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
walther@60358
   212
	  erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty 
walther@60358
   213
	  	[\<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")],
walther@60358
   214
	  srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358
   215
	  rules = [
walther@60358
   216
     \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
walther@60358
   217
  	 \<^rule_thm>\<open>real_num_collect_assoc_r\<close>, (*"[| l is_const; m..|] ==>  (k + m * n) + l * n = k + (l + m)*n"*)
walther@60358
   218
  	 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_const ==> n + m * n = (1 + m) * n"*)
walther@60358
   219
  	 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
neuper@37950
   220
walther@60358
   221
  	 \<^rule_thm>\<open>subtrahiere\<close>, (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
walther@60358
   222
  	 \<^rule_thm>\<open>subtrahiere_von_1\<close>, (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
walther@60358
   223
  	 \<^rule_thm>\<open>subtrahiere_1\<close>, (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
neuper@37950
   224
walther@60358
   225
  	 \<^rule_thm>\<open>subtrahiere_x_plus_minus\<close>, (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
walther@60358
   226
  	 \<^rule_thm>\<open>subtrahiere_x_plus1_minus\<close>, (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
walther@60358
   227
  	 \<^rule_thm>\<open>subtrahiere_x_plus_minus1\<close>, (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
neuper@37950
   228
walther@60358
   229
  	 \<^rule_thm>\<open>subtrahiere_x_minus_plus\<close>, (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
walther@60358
   230
  	 \<^rule_thm>\<open>subtrahiere_x_minus1_plus\<close>, (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
walther@60358
   231
  	 \<^rule_thm>\<open>subtrahiere_x_minus_plus1\<close>, (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
neuper@37950
   232
walther@60358
   233
  	 \<^rule_thm>\<open>subtrahiere_x_minus_minus\<close>, (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
walther@60358
   234
  	 \<^rule_thm>\<open>subtrahiere_x_minus1_minus\<close>, (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
walther@60358
   235
  	 \<^rule_thm>\<open>subtrahiere_x_minus_minus1\<close>, (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
neuper@37950
   236
walther@60358
   237
  	 \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
walther@60358
   238
  	 \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_"),
neuper@37950
   239
walther@60358
   240
  	 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
walther@60358
   241
        (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
walther@60358
   242
  	 \<^rule_thm>\<open>real_mult_2_assoc_r\<close>, (*"(k + z1) + z1 = k + 2 * z1"*)
walther@60358
   243
  	 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
walther@60358
   244
walther@60358
   245
  	 \<^rule_thm>\<open>addiere_vor_minus\<close>, (*"[| l is_const; m is_const |] ==> -(l * v) +  m * v = (-l + m) *v"*)
walther@60358
   246
  	 \<^rule_thm>\<open>addiere_eins_vor_minus\<close>, (*"[| m is_const |] ==> -  v +  m * v = (-1 + m) * v"*)
walther@60358
   247
  	 \<^rule_thm>\<open>subtrahiere_vor_minus\<close>, (*"[| l is_const; m is_const |] ==> -(l * v) -  m * v = (-l - m) *v"*)
walther@60358
   248
  	 \<^rule_thm>\<open>subtrahiere_eins_vor_minus\<close>], (*"[| m is_const |] ==> -  v -  m * v = (-1 - m) * v"*)	 
walther@60358
   249
	  scr = Rule.Empty_Prog};
neuper@37950
   250
    
neuper@37950
   251
val verschoenere = 
walther@59851
   252
  Rule_Def.Repeat{id = "verschoenere", preconds = [], 
walther@60358
   253
    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
walther@60358
   254
    erls = Rule_Set.append_rules "erls_verschoenere" Rule_Set.empty 
walther@60358
   255
		  [\<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner "")],
walther@60358
   256
    rules = [
walther@60358
   257
      \<^rule_thm>\<open>vorzeichen_minus_weg1\<close>, (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
walther@60358
   258
      \<^rule_thm>\<open>vorzeichen_minus_weg2\<close>, (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
walther@60358
   259
      \<^rule_thm>\<open>vorzeichen_minus_weg3\<close>, (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
walther@60358
   260
      \<^rule_thm>\<open>vorzeichen_minus_weg4\<close>, (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
neuper@37950
   261
walther@60358
   262
      \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
neuper@37950
   263
walther@60358
   264
      \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
walther@60358
   265
      \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
walther@60358
   266
      \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
walther@60358
   267
      \<^rule_thm>\<open>null_minus\<close>, (*"0 - a = -a"*)
walther@60358
   268
      \<^rule_thm>\<open>vor_minus_mal\<close>], (*"- a * b = (-a) * b"*)
walther@60358
   269
	  scr = Rule.Empty_Prog};
neuper@37950
   270
neuper@37950
   271
val klammern_aufloesen = 
walther@59851
   272
  Rule_Def.Repeat{id = "klammern_aufloesen", preconds = [], 
walther@60358
   273
    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, 
walther@60358
   274
    calc = [], errpatts = [], erls = Rule_Set.Empty, 
walther@60358
   275
    rules = [
walther@60358
   276
      \<^rule_thm_sym>\<open>add.assoc\<close>, (*"a + (b + c) = (a + b) + c"*)
walther@60358
   277
      \<^rule_thm>\<open>klammer_plus_minus\<close>, (*"a + (b - c) = (a + b) - c"*)
walther@60358
   278
      \<^rule_thm>\<open>klammer_minus_plus\<close>, (*"a - (b + c) = (a - b) - c"*)
walther@60358
   279
      \<^rule_thm>\<open>klammer_minus_minus\<close>], (*"a - (b - c) = (a - b) + c"*)
walther@60358
   280
	  scr = Rule.Empty_Prog};
neuper@37950
   281
neuper@37950
   282
val klammern_ausmultiplizieren = 
walther@59851
   283
  Rule_Def.Repeat{id = "klammern_ausmultiplizieren", preconds = [], 
walther@60358
   284
    rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, 
walther@60358
   285
    calc = [], errpatts = [], erls = Rule_Set.Empty, 
walther@60358
   286
    rules = [
walther@60358
   287
      \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
walther@60358
   288
      \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
walther@60358
   289
walther@60358
   290
      \<^rule_thm>\<open>klammer_mult_minus\<close>, (*"a * (b - c) = a * b - a * c"*)
walther@60358
   291
      \<^rule_thm>\<open>klammer_minus_mult\<close>], (*"(b - c) * a = b * a - c * a"*)
walther@60358
   292
	  scr = Rule.Empty_Prog};
neuper@37950
   293
neuper@37950
   294
val ordne_monome = 
walther@60358
   295
  Rule_Def.Repeat {
walther@60358
   296
    id = "ordne_monome", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), 
walther@60358
   297
    srls = Rule_Set.Empty, calc = [], errpatts = [], 
walther@60358
   298
    erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty [
walther@60358
   299
      \<^rule_eval>\<open>PolyMinus.kleiner\<close> (eval_kleiner ""),
walther@60358
   300
		  \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "")], 
walther@60358
   301
    rules = [
walther@60358
   302
      \<^rule_thm>\<open>tausche_mal\<close>, (*"[| b is_atom; a kleiner b  |] ==> (b * a) = (a * b)"*)
walther@60358
   303
      \<^rule_thm>\<open>tausche_vor_mal\<close>, (*"[| b is_atom; a kleiner b  |] ==> (-b * a) = (-a * b)"*)
walther@60358
   304
      \<^rule_thm>\<open>tausche_mal_mal\<close>, (*"[| c is_atom; b kleiner c  |] ==> (a * c * b) = (a * b *c)"*)
walther@60358
   305
      \<^rule_thm>\<open>x_quadrat\<close>], (*"(x * a) * a = x * a \<up> 2"*)
walther@60358
   306
	  scr = Rule.Empty_Prog};
neuper@37950
   307
neuper@37950
   308
val rls_p_33 = 
walther@60358
   309
  Rule_Set.append_rules "rls_p_33" Rule_Set.empty [
walther@60358
   310
    Rule.Rls_ ordne_alphabetisch,
wneuper@59416
   311
		Rule.Rls_ fasse_zusammen,
walther@60358
   312
		Rule.Rls_ verschoenere];
neuper@37950
   313
val rls_p_34 = 
walther@60358
   314
  Rule_Set.append_rules "rls_p_34" Rule_Set.empty [
walther@60358
   315
    Rule.Rls_ klammern_aufloesen,
walther@60358
   316
  	Rule.Rls_ ordne_alphabetisch,
walther@60358
   317
  	Rule.Rls_ fasse_zusammen,
walther@60358
   318
  	Rule.Rls_ verschoenere];
neuper@37950
   319
val rechnen = 
walther@60358
   320
  Rule_Set.append_rules "rechnen" Rule_Set.empty [
walther@60358
   321
    \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
walther@60358
   322
    \<^rule_eval>\<open>plus\<close> (**)(eval_binop "#add_"),
walther@60358
   323
    \<^rule_eval>\<open>minus\<close> (**)(eval_binop "#subtr_")];
wneuper@59472
   324
\<close>
wenzelm@60289
   325
rule_set_knowledge
wenzelm@60286
   326
  ordne_alphabetisch = \<open>prep_rls' ordne_alphabetisch\<close> and
wenzelm@60286
   327
  fasse_zusammen = \<open>prep_rls' fasse_zusammen\<close> and
wenzelm@60286
   328
  verschoenere = \<open>prep_rls' verschoenere\<close> and
wenzelm@60286
   329
  ordne_monome = \<open>prep_rls' ordne_monome\<close> and
wenzelm@60286
   330
  klammern_aufloesen = \<open>prep_rls' klammern_aufloesen\<close> and
wenzelm@60286
   331
  klammern_ausmultiplizieren = \<open>prep_rls' klammern_ausmultiplizieren\<close>
neuper@37950
   332
neuper@37950
   333
(** problems **)
wenzelm@60306
   334
wenzelm@60306
   335
problem pbl_vereinf_poly : "polynom/vereinfachen" = \<open>Rule_Set.Empty\<close>
wenzelm@60306
   336
wenzelm@60306
   337
problem pbl_vereinf_poly_minus : "plus_minus/polynom/vereinfachen" =
walther@60358
   338
  \<open>Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty [
walther@60358
   339
     \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
wenzelm@60306
   340
     \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
walther@60358
   341
     \<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*)
walther@60358
   342
     \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
walther@60358
   343
     \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
walther@60358
   344
     \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close>
wenzelm@60306
   345
  Method: "simplification/for_polynomials/with_minus"
wenzelm@60306
   346
  CAS: "Vereinfache t_t"
wenzelm@60306
   347
  Given: "Term t_t"
wenzelm@60306
   348
  Where:
wenzelm@60306
   349
    "t_t is_polyexp"
wenzelm@60306
   350
    "Not (matchsub (?a + (?b + ?c)) t_t |
wenzelm@60306
   351
          matchsub (?a + (?b - ?c)) t_t |
wenzelm@60306
   352
          matchsub (?a - (?b + ?c)) t_t |
wenzelm@60306
   353
          matchsub (?a + (?b - ?c)) t_t )"
wenzelm@60306
   354
    "Not (matchsub (?a * (?b + ?c)) t_t |
wenzelm@60306
   355
          matchsub (?a * (?b - ?c)) t_t |
wenzelm@60306
   356
          matchsub ((?b + ?c) * ?a) t_t |
wenzelm@60306
   357
          matchsub ((?b - ?c) * ?a) t_t )"
wenzelm@60306
   358
  Find: "normalform n_n"
wenzelm@60306
   359
wenzelm@60306
   360
problem pbl_vereinf_poly_klammer : "klammer/polynom/vereinfachen" =
walther@60358
   361
  \<open>Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty [
walther@60358
   362
     \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
wenzelm@60306
   363
     \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
walther@60358
   364
     \<^rule_thm>\<open>or_true\<close>, (*"(?a | True) = True"*)
walther@60358
   365
     \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
walther@60358
   366
     \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
walther@60358
   367
     \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close>
wenzelm@60306
   368
  Method: "simplification/for_polynomials/with_parentheses"
wenzelm@60306
   369
  CAS: "Vereinfache t_t"
wenzelm@60306
   370
  Given: "Term t_t"
wenzelm@60306
   371
  Where:
wenzelm@60306
   372
    "t_t is_polyexp"
wenzelm@60306
   373
    "Not (matchsub (?a * (?b + ?c)) t_t |
wenzelm@60306
   374
          matchsub (?a * (?b - ?c)) t_t |
wenzelm@60306
   375
          matchsub ((?b + ?c) * ?a) t_t |
wenzelm@60306
   376
          matchsub ((?b - ?c) * ?a) t_t )"
wenzelm@60306
   377
  Find: "normalform n_n"
wenzelm@60306
   378
wenzelm@60306
   379
problem pbl_vereinf_poly_klammer_mal : "binom_klammer/polynom/vereinfachen" =
wenzelm@60306
   380
  \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
wenzelm@60306
   381
    \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
wenzelm@60306
   382
  Method: "simplification/for_polynomials/with_parentheses_mult"
wenzelm@60306
   383
  CAS: "Vereinfache t_t"
wenzelm@60306
   384
  Given: "Term t_t"
wenzelm@60306
   385
  Where: "t_t is_polyexp"
wenzelm@60306
   386
  Find: "normalform n_n"
wenzelm@60306
   387
wenzelm@60306
   388
problem pbl_probe : "probe" = \<open>Rule_Set.Empty\<close>
wenzelm@60306
   389
wenzelm@60306
   390
problem pbl_probe_poly : "polynom/probe" =
wenzelm@60306
   391
  \<open>Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
wenzelm@60306
   392
    \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
wenzelm@60306
   393
  Method: "probe/fuer_polynom"
wenzelm@60306
   394
  CAS: "Probe e_e w_w"
wenzelm@60306
   395
  Given: "Pruefe e_e" "mitWert w_w"
wenzelm@60306
   396
  Where: "e_e is_polyexp"
wenzelm@60306
   397
  Find: "Geprueft p_p"
wenzelm@60306
   398
wenzelm@60306
   399
problem pbl_probe_bruch : "bruch/probe" =
wenzelm@60306
   400
  \<open>Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
wenzelm@60306
   401
    \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")]\<close>
wenzelm@60306
   402
  Method: "probe/fuer_bruch"
wenzelm@60306
   403
  CAS: "Probe e_e w_w"
wenzelm@60306
   404
  Given: "Pruefe e_e" "mitWert w_w"
wenzelm@60306
   405
  Where: "e_e is_ratpolyexp"
wenzelm@60306
   406
  Find: "Geprueft p_p"
neuper@37950
   407
neuper@37950
   408
(** methods **)
wneuper@59545
   409
wneuper@59504
   410
partial_function (tailrec) simplify :: "real \<Rightarrow> real"
wneuper@59504
   411
  where
walther@59635
   412
"simplify t_t = (
walther@59635
   413
  (Repeat(
walther@59637
   414
    (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
walther@59637
   415
    (Try (Rewrite_Set ''fasse_zusammen'')) #>
walther@59635
   416
    (Try (Rewrite_Set ''verschoenere'')))
walther@59635
   417
  ) t_t)"
wenzelm@60303
   418
wenzelm@60303
   419
method met_simp_poly_minus : "simplification/for_polynomials/with_minus" =
wenzelm@60303
   420
  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
walther@60358
   421
    prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty [
walther@60358
   422
      \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
walther@60358
   423
      \<^rule_eval>\<open>Prog_Expr.matchsub\<close> (Prog_Expr.eval_matchsub ""),
walther@60358
   424
      \<^rule_thm>\<open>and_true\<close>, (*"(?a & True) = ?a"*)
walther@60358
   425
      \<^rule_thm>\<open>and_false\<close>, (*"(?a & False) = False"*)
walther@60358
   426
      \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
walther@60358
   427
      \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)],
wenzelm@60303
   428
    crls = Rule_Set.empty, errpats = [], nrls = rls_p_33}\<close>
wenzelm@60303
   429
  Program: simplify.simps
wenzelm@60303
   430
  Given: "Term t_t"
wenzelm@60303
   431
  Where:
wenzelm@60303
   432
    "t_t is_polyexp"
wenzelm@60303
   433
    "Not (matchsub (?a + (?b + ?c)) t_t |
wenzelm@60303
   434
          matchsub (?a + (?b - ?c)) t_t |
wenzelm@60303
   435
          matchsub (?a - (?b + ?c)) t_t |
wenzelm@60303
   436
          matchsub (?a + (?b - ?c)) t_t)"
wenzelm@60303
   437
  Find: "normalform n_n"
wneuper@59545
   438
wneuper@59504
   439
partial_function (tailrec) simplify2 :: "real \<Rightarrow> real"
wneuper@59504
   440
  where
walther@59635
   441
"simplify2 t_t = (
walther@59635
   442
  (Repeat(
walther@59637
   443
    (Try (Rewrite_Set ''klammern_aufloesen'')) #>
walther@59637
   444
    (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
walther@59637
   445
    (Try (Rewrite_Set ''fasse_zusammen'')) #>
walther@59635
   446
    (Try (Rewrite_Set ''verschoenere'')))
walther@59635
   447
  ) t_t)"
wenzelm@60303
   448
wenzelm@60303
   449
method met_simp_poly_parenth : "simplification/for_polynomials/with_parentheses" =
wenzelm@60303
   450
  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
wenzelm@60303
   451
    prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty 
wenzelm@60303
   452
      [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
wenzelm@60303
   453
    crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>
wenzelm@60303
   454
  Program: simplify2.simps
wenzelm@60303
   455
  Given: "Term t_t"
wenzelm@60303
   456
  Where: "t_t is_polyexp"
wenzelm@60303
   457
  Find: "normalform n_n"
wneuper@59545
   458
wneuper@59504
   459
partial_function (tailrec) simplify3 :: "real \<Rightarrow> real"
wneuper@59504
   460
  where
walther@59635
   461
"simplify3 t_t = (
walther@59635
   462
  (Repeat(
walther@59637
   463
    (Try (Rewrite_Set ''klammern_ausmultiplizieren'')) #>
walther@59637
   464
    (Try (Rewrite_Set ''discard_parentheses'')) #>
walther@59637
   465
    (Try (Rewrite_Set ''ordne_monome'')) #>
walther@59637
   466
    (Try (Rewrite_Set ''klammern_aufloesen'')) #>
walther@59637
   467
    (Try (Rewrite_Set ''ordne_alphabetisch'')) #>
walther@59637
   468
    (Try (Rewrite_Set ''fasse_zusammen'')) #>
walther@59635
   469
    (Try (Rewrite_Set ''verschoenere'')))
walther@59635
   470
  ) t_t)"
wenzelm@60303
   471
wenzelm@60303
   472
method met_simp_poly_parenth_mult : "simplification/for_polynomials/with_parentheses_mult" =
wenzelm@60303
   473
  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
wenzelm@60303
   474
    prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty 
wenzelm@60303
   475
      [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
wenzelm@60303
   476
    crls = Rule_Set.empty, errpats = [], nrls = rls_p_34}\<close>
wenzelm@60303
   477
  Program: simplify3.simps
wenzelm@60303
   478
  Given: "Term t_t"
wenzelm@60303
   479
  Where: "t_t is_polyexp"
wenzelm@60303
   480
  Find: "normalform n_n"
wenzelm@60303
   481
wenzelm@60303
   482
method met_probe : "probe" =
wenzelm@60303
   483
  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.Empty, crls = Rule_Set.empty,
wenzelm@60303
   484
    errpats = [], nrls = Rule_Set.Empty}\<close>
wneuper@59545
   485
wneuper@59504
   486
partial_function (tailrec) mache_probe :: "bool \<Rightarrow> bool list \<Rightarrow> bool"
wneuper@59504
   487
  where
walther@59635
   488
"mache_probe e_e w_w = (
walther@59635
   489
  let
walther@59635
   490
     e_e = Take e_e;
walther@59635
   491
     e_e = Substitute w_w e_e
walther@59635
   492
  in (
walther@59635
   493
    Repeat (
walther@59637
   494
      (Try (Repeat (Calculate ''TIMES''))) #>
walther@59637
   495
      (Try (Repeat (Calculate ''PLUS'' ))) #>
walther@59635
   496
      (Try (Repeat (Calculate ''MINUS''))))
walther@59635
   497
    ) e_e)"
wenzelm@60303
   498
wenzelm@60303
   499
method met_probe_poly : "probe/fuer_polynom" =
wenzelm@60303
   500
  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
wenzelm@60303
   501
    prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
wenzelm@60303
   502
        [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")], 
wenzelm@60303
   503
    crls = Rule_Set.empty, errpats = [], nrls = rechnen}\<close>
wenzelm@60303
   504
  Program: mache_probe.simps
wenzelm@60303
   505
  Given: "Pruefe e_e" "mitWert w_w"
wenzelm@60303
   506
  Where: "e_e is_polyexp"
wenzelm@60303
   507
  Find: "Geprueft p_p"
wenzelm@60303
   508
wenzelm@60303
   509
method met_probe_bruch : "probe/fuer_bruch" =
wenzelm@60303
   510
  \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, 
wenzelm@60303
   511
    prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
wenzelm@60303
   512
        [(*for preds in where_*) \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")],
wenzelm@60303
   513
    crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty}\<close>
wenzelm@60303
   514
  Given: "Pruefe e_e" "mitWert w_w"
wenzelm@60303
   515
  Where: "e_e is_ratpolyexp"
wenzelm@60303
   516
  Find: "Geprueft p_p"
wenzelm@60303
   517
wenzelm@60303
   518
ML \<open>
walther@60278
   519
\<close> ML \<open>
wneuper@59472
   520
\<close>
neuper@37906
   521
neuper@37906
   522
end
neuper@37906
   523