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

     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 ML {*

    23 store_pbt

    24  (prep_pbt thy "pbl_equ_dio" [] e_pblID

    25  (["diophantine","equation"],

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

    27   (*                                      TODO: drop ^^^^^*)

    28    ("#Where" ,[]),

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

    30   ],

    31   e_rls, SOME "solve (e_e::bool, v_v::int)",

    32   [["LinEq","solve_lineq_equation"]])); (*-----TODO*)

    33 show_ptyps();

    34 get_pbt ["diophantine","equation"];

    35 *}

    36 setup {* KEStore_Elems.store_pbts

    37   [(prep_pbt thy "pbl_equ_dio" [] e_pblID

    38       (["diophantine","equation"],

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

    40           (*                                      TODO: drop ^^^^^*)

    41           ("#Where" ,[]),

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

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

    45 text {*method solving the usecase*}

    46 ML {*

    47 store_met

    48 (prep_met thy "met_test_diophant" [] e_metID

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

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

    51   (*                                      TODO: drop ^^^^^*)

    52    ("#Where" ,[]),

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

    54   ],

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

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

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

    58  "(Repeat                                                          " ^

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

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

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

    62  ))

    63 *}

    65 end

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Tue, 21 Jan 2014 00:27:44 +0100
changeset 55339	cccd24e959ba
parent 52148	aabc6c8e930a
child 55347	6cee13cd9403
permissions	-rw-r--r--