(* simplification of terms

   author: Walther Neuper 050912

   (c) due to copyright terms

use"Knowledge/Simplify.ML";

use"Simplify.ML";

*)

(** interface isabelle -- isac **)

theory' := overwritel (!theory', [("Simplify.thy",Simplify.thy)]);

(** problems **)

store_pbt

 (prep_pbt Simplify.thy "pbl_simp" [] e_pblID

 (["simplification"],

  [("#Given" ,["term t_"]),

   ("#Find"  ,["normalform n_"])

  ],

  append_rls "e_rls" e_rls [(*for preds in where_*)], 

  SOME "Simplify t_", 

  []));

store_pbt

 (prep_pbt Simplify.thy "pbl_vereinfache" [] e_pblID

 (["vereinfachen"],

  [("#Given" ,["term t_"]),

   ("#Find"  ,["normalform n_"])

  ],

  append_rls "e_rls" e_rls [(*for preds in where_*)], 

  SOME "Vereinfache t_", 

  []));

(** methods **)

store_met

    (prep_met Simplify.thy "met_simp" [] e_metID

	      (["simplification"],

	       [("#Given" ,["term t_"]),

		("#Find"  ,["normalform n_"])

		],

	       {rew_ord'="tless_true",

		rls'= e_rls, 

		calc = [], 

		srls = e_rls, 

		prls=e_rls,

		crls = e_rls, nrls = e_rls},

	       "empty_script"

	       ));

(** CAS-command **)

(*.function for handling the cas-input "Simplify (2*a + 3*a)":

   make a model which is already in ptree-internal format.*)

(* val (h,argl) = strip_comb (str2term "Simplify (2*a + 3*a)");

   val (h,argl) = strip_comb ((term_of o the o (parse thy)) 

				  "Simplify (2*a + 3*a)");

   *)

fun argl2dtss t =

    [((term_of o the o (parse thy)) "term", t),

     ((term_of o the o (parse thy)) "normalform", 

      [(term_of o the o (parse thy)) "N"])

     ]

  | argl2dtss _ = raise error "Simplify.ML: wrong argument for argl2dtss";

castab := 

overwritel (!castab, 

	    [((term_of o the o (parse thy)) "Simplify",  

	      (("Isac.thy", ["simplification"], ["no_met"]), 

	       argl2dtss)),

	     ((term_of o the o (parse thy)) "Vereinfache",  

	      (("Isac.thy", ["vereinfachen"], ["no_met"]), 

	       argl2dtss))

	     ]);