wneuper/isa: src/Tools/isac/Knowledge/DiophantEq.thy@4f3f530f3cf6

     1 (* Title:  Knowledge/DiophantEq.thy

     2    Author: Mathias Lehnfeld 2011

     3    (c) due to copyright terms

     4 12345678901234567890123456789012345678901234567890123456789012345678901234567890

     5         10        20        30        40        50        60        70        80

     6 *)

     8 theory DiophantEq imports Atools Equation Test

     9 begin

    11 consts

    12   Diophant'_equation :: "[bool, int, bool ]

    13                                        => bool "

    14                     ("((Script Diophant'_equation (_ _ =))//(_))" 9)

    16 axiomatization where

    17   int_isolate_add: "(bdv + a = b) = (bdv = b + (-1)*(a::int))"

    19 ML {*val thy = @{theory}*}

    21 text {*problemclass for the usecase*}

    22 setup {* KEStore_Elems.add_pbts

    23   [(prep_pbt thy "pbl_equ_dio" [] e_pblID

    24       (["diophantine","equation"],

    25         [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),

    26           (*                                      TODO: drop ^^^^^*)

    27           ("#Where" ,[]),

    28           ("#Find"  ,["boolTestFind s_s"])],

    29         e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}

    31 text {*method solving the usecase*}

    32 ML {*

    33 store_met

    34 (prep_met thy "met_test_diophant" [] e_metID

    35  (["Test","solve_diophant"]:metID,

    36   [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),

    37   (*                                      TODO: drop ^^^^^*)

    38    ("#Where" ,[]),

    39    ("#Find"  ,["boolTestFind s_s"])

    40   ],

    41    {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,

    42     prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},

    43  "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^

    44  "(Repeat                                                          " ^

    45  "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^

    46  "     (Try (Calculate PLUS)) @@  " ^

    47  "     (Try (Calculate TIMES))) e_e::bool)"

    48  ))

    49 *}

    50 setup {* KEStore_Elems.add_mets

    51   [prep_met thy "met_test_diophant" [] e_metID

    52       (["Test","solve_diophant"]:metID,

    53         [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),

    54           (*                                      TODO: drop ^^^^^*)

    55           ("#Where" ,[]),

    56           ("#Find"  ,["boolTestFind s_s"])],

    57         {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls, prls = e_rls, calc = [],

    58           crls = tval_rls, errpats = [], nrls = Test_simplify},

    59         "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^

    60           "(Repeat                                                          " ^

    61           "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^

    62           "     (Try (Calculate PLUS)) @@  " ^

    63           "     (Try (Calculate TIMES))) e_e::bool)")]

    64 *}

    66 end

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Sat, 01 Feb 2014 16:44:45 +0100
changeset 55373	4f3f530f3cf6
parent 55363	d78bc1342183
child 55380	7be2ad0e4acb
permissions	-rw-r--r--