1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.ML	Wed Aug 25 16:20:07 2010 +0200
     1.3 @@ -0,0 +1,76 @@
     1.4 +(* simplification of terms
     1.5 +   author: Walther Neuper 050912
     1.6 +   (c) due to copyright terms
     1.7 +
     1.8 +use"Knowledge/Simplify.ML";
     1.9 +use"Simplify.ML";
    1.10 +*)
    1.11 +
    1.12 +
    1.13 +(** interface isabelle -- isac **)
    1.14 +
    1.15 +theory' := overwritel (!theory', [("Simplify.thy",Simplify.thy)]);
    1.16 +
    1.17 +(** problems **)
    1.18 +
    1.19 +store_pbt
    1.20 + (prep_pbt Simplify.thy "pbl_simp" [] e_pblID
    1.21 + (["simplification"],
    1.22 +  [("#Given" ,["term t_"]),
    1.23 +   ("#Find"  ,["normalform n_"])
    1.24 +  ],
    1.25 +  append_rls "e_rls" e_rls [(*for preds in where_*)], 
    1.26 +  SOME "Simplify t_", 
    1.27 +  []));
    1.28 +
    1.29 +store_pbt
    1.30 + (prep_pbt Simplify.thy "pbl_vereinfache" [] e_pblID
    1.31 + (["vereinfachen"],
    1.32 +  [("#Given" ,["term t_"]),
    1.33 +   ("#Find"  ,["normalform n_"])
    1.34 +  ],
    1.35 +  append_rls "e_rls" e_rls [(*for preds in where_*)], 
    1.36 +  SOME "Vereinfache t_", 
    1.37 +  []));
    1.38 +
    1.39 +(** methods **)
    1.40 +
    1.41 +store_met
    1.42 +    (prep_met Simplify.thy "met_simp" [] e_metID
    1.43 +	      (["simplification"],
    1.44 +	       [("#Given" ,["term t_"]),
    1.45 +		("#Find"  ,["normalform n_"])
    1.46 +		],
    1.47 +	       {rew_ord'="tless_true",
    1.48 +		rls'= e_rls, 
    1.49 +		calc = [], 
    1.50 +		srls = e_rls, 
    1.51 +		prls=e_rls,
    1.52 +		crls = e_rls, nrls = e_rls},
    1.53 +	       "empty_script"
    1.54 +	       ));
    1.55 +
    1.56 +(** CAS-command **)
    1.57 +
    1.58 +(*.function for handling the cas-input "Simplify (2*a + 3*a)":
    1.59 +   make a model which is already in ptree-internal format.*)
    1.60 +(* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");
    1.61 +   val (h,argl) = strip_comb ((term_of o the o (parse thy)) 
    1.62 +				  "Simplify (2*a + 3*a)");
    1.63 +   *)
    1.64 +fun argl2dtss t =
    1.65 +    [((term_of o the o (parse thy)) "term", t),
    1.66 +     ((term_of o the o (parse thy)) "normalform", 
    1.67 +      [(term_of o the o (parse thy)) "N"])
    1.68 +     ]
    1.69 +  | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";
    1.70 +
    1.71 +castab := 
    1.72 +overwritel (!castab, 
    1.73 +	    [((term_of o the o (parse thy)) "Simplify",  
    1.74 +	      (("Isac.thy", ["simplification"], ["no_met"]), 
    1.75 +	       argl2dtss)),
    1.76 +	     ((term_of o the o (parse thy)) "Vereinfache",  
    1.77 +	      (("Isac.thy", ["vereinfachen"], ["no_met"]), 
    1.78 +	       argl2dtss))
    1.79 +	     ]);