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

     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"   (*"term" is a keyword in *.thy*)

    12   normalform  :: "real => una"

    14   (*the CAS-command*)

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

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

    18 (** problems **)

    20 problem pbl_simp : "simplification" =

    21   \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>

    22   CAS: "Simplify t_t"

    23   Given: "Term t_t"

    24   Find: "normalform n_n"

    26 problem pbl_vereinfache : "vereinfachen" =

    27   \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>

    28   CAS: "Vereinfache t_t"

    29   Given: "Term t_t"

    30   Find: "normalform n_n"

    32 (** methods **)

    34 method met_tsimp : "simplification" =

    35   \<open>{rew_ord="tless_true", rls'= Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty, where_rls=Rule_Set.empty,

    36     errpats = [], rew_rls = Rule_Set.empty}\<close>

    37   Given: "Term t_t"

    38   Find: "normalform n_n"

    40 ML \<open>

    42 (** CAS-command **)

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

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

    46 (* val (h,argl) = strip_comb (TermC.parse_test @{context} "Simplify (2*a + 3*a)");

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

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

    49    *)

    50 fun argl2dtss t =

    51   [(Syntax.read_term (Proof_Context.init_global \<^theory>) "Term", t),

    52    (Syntax.read_term (Proof_Context.init_global \<^theory>) "normalform",

    53      [(Syntax.read_term (Proof_Context.init_global \<^theory>)) "N"])]

    54 \<close>

    55 cas Simplify = \<open>argl2dtss\<close>

    56   Problem_Ref: "simplification"

    57 cas Vereinfache = \<open>argl2dtss\<close>

    58   Problem_Ref: "vereinfachen"

    60 ML \<open>

    61 \<close> ML \<open>

    62 \<close> ML \<open>

    63 \<close>

    64 end

author	wneuper <Walther.Neuper@jku.at>
	Mon, 01 Jan 2024 11:31:16 +0100
changeset 60789	8fa678b678e8
parent 60664	ed6f9e67349d
permissions	-rw-r--r--