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

     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 *}

    34 setup {* KEStore_Elems.add_pbts

    35   [(prep_pbt thy "pbl_equ_dio" [] e_pblID

    36       (["diophantine","equation"],

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

    38           (*                                      TODO: drop ^^^^^*)

    39           ("#Where" ,[]),

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

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

    43 text {*method solving the usecase*}

    44 ML {*

    45 store_met

    46 (prep_met thy "met_test_diophant" [] e_metID

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

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

    49   (*                                      TODO: drop ^^^^^*)

    50    ("#Where" ,[]),

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

    52   ],

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

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

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

    56  "(Repeat                                                          " ^

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

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

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

    60  ))

    61 *}

    63 end

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Mon, 27 Jan 2014 21:49:27 +0100
changeset 55359	73dc85c025ab
parent 55347	6cee13cd9403
child 55363	d78bc1342183
permissions	-rw-r--r--