1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Fri Dec 31 14:58:03 2010 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri Dec 31 15:19:05 2010 +0100
     1.3 @@ -251,6 +251,7 @@
     1.4  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
     1.5  atomty sc;
     1.6  
     1.7 +
     1.8  "----------- me simplification.for_polynomials.with_minus";
     1.9  "----------- me simplification.for_polynomials.with_minus";
    1.10  "----------- me simplification.for_polynomials.with_minus";
    1.11 @@ -261,11 +262,22 @@
    1.12             "normalform N"],
    1.13  	          ("PolyMinus",["plus_minus","polynom","vereinfachen"],
    1.14  	           ["simplification","for_polynomials","with_minus"]))];
    1.15 -(*========== inhibit exn =======================================================
    1.16  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.17 -============ inhibit exn =====================================================*)
    1.18 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.19 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.20 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.21 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.22 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.23  
    1.24 -(*========== inhibit exn ?======================================================
    1.25 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.26 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.27 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.28 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.29 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.30 +if f2str f = "3 - 2 * e + 2 * f + 2 * g" andalso #1 nxt = "End_Proof'" then ()
    1.31 +else error "polyminus.sml: me simplification.for_polynomials.with_minus";
    1.32 +
    1.33 +
    1.34  "----------- pbl polynom vereinfachen p.33 -----------------------";
    1.35  "----------- pbl polynom vereinfachen p.33 -----------------------";
    1.36  "----------- pbl polynom vereinfachen p.33 -----------------------";
    1.37 @@ -340,9 +352,9 @@
    1.38  "----------- met probe fuer_polynom ------------------------------";
    1.39  "----------- met probe fuer_polynom ------------------------------";
    1.40  val str = 
    1.41 -"Script ProbeScript (e_e::bool) (ws_::bool list) =\
    1.42 +"Script ProbeScript (e_e::bool) (w_s::bool list) =\
    1.43  \ (let e_e = Take e_e;                             \
    1.44 -\      e_e = Substitute ws_ e_e                    \
    1.45 +\      e_e = Substitute w_s e_e                    \
    1.46  \ in (Repeat((Try (Repeat (Calculate TIMES))) @@  \
    1.47  \            (Try (Repeat (Calculate PLUS ))) @@  \
    1.48  \            (Try (Repeat (Calculate MINUS))))) e_e)"
    1.49 @@ -428,12 +440,12 @@
    1.50  val erls = erls_ordne_alphabetisch;
    1.51  val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
    1.52  val SOME (t',_) = 
    1.53 -    rewrite_ (theory "Isac") e_rew_ord erls false tausche_minus t;
    1.54 +    rewrite_ (theory "Isac") e_rew_ord erls false @{thm tausche_minus} t;
    1.55  term2str t';     "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
    1.56  
    1.57  val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
    1.58  val NONE = 
    1.59 -    rewrite_ (theory "Isac") e_rew_ord erls false tausche_minus_plus t;
    1.60 +    rewrite_ (theory "Isac") e_rew_ord erls false @{thm tausche_minus_plus} t;
    1.61  
    1.62  val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
    1.63  val SOME (t',_) = 
    1.64 @@ -568,6 +580,8 @@
    1.65  
    1.66  "----- go into details, if it seems not to work -----";
    1.67  "--- does the predicate evaluate correctly ?";
    1.68 +(*=== inhibit exn ==============================================================
    1.69 +!!!!! no '?a' ............
    1.70  val t = str2term 
    1.71  	    "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + \
    1.72  	    \3 * (a - 2 * q))";
    1.73 @@ -581,9 +595,9 @@
    1.74  val prls = append_rls "prls_pbl_vereinf_poly" e_rls 
    1.75  	     [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),
    1.76  	      Calc ("Tools.matchsub", eval_matchsub ""),
    1.77 -	      Thm ("or_true",or_true),
    1.78 +	      Thm ("or_true",@{thm or_true}),
    1.79  	      (*"(?a | True) = True"*)
    1.80 -	      Thm ("or_false",or_false),
    1.81 +	      Thm ("or_false",@{thm or_false}),
    1.82  	      (*"(?a | False) = ?a"*)
    1.83  	      Thm ("not_true",num_str @{thm not_true}),
    1.84  	      (*"(~ True) = False"*)
    1.85 @@ -604,8 +618,7 @@
    1.86  trace_rewrite := false;
    1.87  if term2str t' = "False" then ()
    1.88  else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
    1.89 -
    1.90 -============ inhibit exn ?====================================================*)
    1.91 +============ inhibit exn =====================================================*)
    1.92  
    1.93  
    1.94  "----------- *** prep_pbt: syntax error in '#Where' of [v";
    1.95 @@ -640,3 +653,10 @@
    1.96  atomwy t;
    1.97  val t = str2term "Term ttt";
    1.98  atomwy t;
    1.99 +val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];
   1.100 +prep_ori fmz thy ((#ppc o get_pbt) pI);
   1.101 +(*val it =
   1.102 +   [(1, [1], "#Given", Const (...), [...]),
   1.103 +    (2, [1], "#Find", Const (...), [...])]
   1.104 +   : ori list
   1.105 +*)