wneuper/isa: src/Tools/isac/Knowledge/Simplify.thy@bb4e8b01b072

     1 (* simplification of terms

     2    author: Walther Neuper 050912

     3    (c) due to copyright terms

     4 *)

     6 theory Simplify imports Base_Tools begin

     8 consts

    10   (*descriptions in the related problem*)

    11   Term        :: "real => una"

    12 (*TERM -->   Const ("Pure.term", "RealDef.real => prop")  (*!!!*) $

    13                Free ("ttt", "RealDef.real")

    14   term -->   Free ("term", "RealDef.real => RealDef.real") $

    15                Free ("ttt", "RealDef.real")

    16     but 'term' is a keyword in *.thy*)

    17   normalform  :: "real => una"

    19   (*the CAS-command*)

    20   Simplify    :: "real => real"  (*"Simplify (1+2a+3+4a)*)

    21   Vereinfache :: "real => real"  (*"Vereinfache (1+2a+3+4a)*)

    23 ML \<open>

    24 val thy = @{theory};

    25 \<close>

    26 (** problems **)

    27 setup \<open>KEStore_Elems.add_pbts

    28   [(Problem.prep_input @{theory} "pbl_simp" [] Problem.id_empty

    29       (["simplification"],

    30         [("#Given" ,["Term t_t"]),

    31           ("#Find"  ,["normalform n_n"])],

    32         Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Simplify t_t", [])),

    33     (Problem.prep_input @{theory} "pbl_vereinfache" [] Problem.id_empty

    34       (["vereinfachen"],

    35         [("#Given", ["Term t_t"]),

    36           ("#Find", ["normalform n_n"])],

    37         Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], SOME "Vereinfache t_t", []))]\<close>

    39 (** methods **)

    40 setup \<open>KEStore_Elems.add_mets

    41     [MethodC.prep_input @{theory} "met_tsimp" [] MethodC.id_empty

    42 	    (["simplification"],

    43 	      [("#Given" ,["Term t_t"]),

    44 		      ("#Find"  ,["normalform n_n"])],

    45 		    {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Rule_Set.empty,

    46 		      errpats = [], nrls = Rule_Set.empty},

    47 	      @{thm refl})]

    48 \<close>

    50 ML \<open>

    52 (** CAS-command **)

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

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

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

    57    val (h,argl) = strip_comb ((Thm.term_of o the o (parse (Thy_Info_get_theory "Simplify")))

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

    59    *)

    60 fun argl2dtss t =

    61     [((Thm.term_of o the o (TermC.parse @{theory})) "Term", t),

    62      ((Thm.term_of o the o (TermC.parse @{theory})) "normalform",

    63       [(Thm.term_of o the o (TermC.parse @{theory})) "N"])

    64      ]

    65   (*| argl2dtss _ = raise ERROR "Simplify.ML: wrong argument for argl2dtss"*);

    66 \<close>

    67 setup \<open>KEStore_Elems.add_cas

    68   [((Thm.term_of o the o (TermC.parse @{theory})) "Simplify",

    69     (("Isac_Knowledge", ["simplification"], ["no_met"]), argl2dtss)),

    70    ((Thm.term_of o the o (TermC.parse @{theory})) "Vereinfache",

    71      (("Isac_Knowledge", ["vereinfachen"], ["no_met"]), argl2dtss))]\<close>

    73 ML \<open>

    74 \<close> ML \<open>

    75 \<close> ML \<open>

    76 \<close>

    77 end

author	wenzelm
	Thu, 10 Jun 2021 12:23:57 +0200
changeset 60290	bb4e8b01b072
parent 60269	74965ce81297
child 60291	52921aa0e14a
permissions	-rw-r--r--