wneuper/isa: src/Tools/isac/Knowledge/Build

     1 (* theory collecting all knowledge defined for the isac mathengine

     2    WN.11.00

     3  *)

     5 theory Build_Thydata

     6 imports

     7   Isac "~~/src/Tools/isac/Interpret/Interpret"

     8   Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*)

     9 begin

    11 subsection {* Build <Theory>-Data *}

    12 text {*

    13   <Theory>-Data represent Isac's "deductive knowledge" (whereas <Problems> and <Methods>

    14   represent application-oriented and algorithmic knowledge respectively.) <Theory>-Data

    15   comprise theories from ProgLang and from Knowledge.

    16   Note, that for bootstrapping Isac "Build_Thydata" theories are available only

    17   via "@{theory Pure}" and "Theory.ancestors_of" but not via "Thy_Info.get_theory"

    18   (while the latter is available in Test_Some.thy loaded from session Isac).

    19 *}

    20 subsubsection {* Get and group the theories defined in Isac *}

    21 ML {*

    22   (* we don't use "fun isacthys ()" etc HERE,

    23     because Thy_Info.get_theory only works with session Isac, not with Build_Isac.thy *)

    24   val knowledge_parent = @{theory}

    25   val proglang_parent = @{theory ProgLang}

    27   val allthys = Theory.ancestors_of @{theory};

    28   val allthys = filter_out (member Theory.eq_thy (* thys for isac bootstrap *)

    29     [(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory xmlsrc},

    30     @{theory Frontend}, knowledge_parent]) allthys         (*["Isac", ..., "Pure"]*)

    32   val isabthys' =                         (*["Complex_Main", "Taylor", .., "Pure"]*)

    33     drop ((find_index (curry Theory.eq_thy @{theory Complex_Main}) allthys), allthys);

    34   val isacthys' =                         (*["Isac", "Inverse_Z_Transform",  .., "KEStore"]*)

    35     take ((find_index (curry Theory.eq_thy @{theory Complex_Main}) allthys), allthys);

    37   val knowthys' =                         (*["Isac", .., "Descript", "Delete"]*)

    38     take ((find_index (curry Theory.eq_thy proglang_parent) isacthys'), isacthys');

    39   val progthys' =                         (*["Script", "Tools", "ListC", "KEStore"]*)

    40     drop ((find_index (curry Theory.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');

    41 *}

    43 subsubsection {* From rule-sets collect theorems, which have been taken from Isabelle *}

    44 ML {*

    45   val isacrlsthms' =                      (*length = 468*)

    46     thms_of_rlss (KEStore_Elems.get_rlss knowledge_parent) : (thmID * term) list

    48   val isacrlsthms = isacrlsthms'            (*length = 457  DELETE AFTER vvv..TODO*)

    49   (*|> filter (fn (thyID, _) => "??.unknown" = thyID)   ...INVESTIGATE THESE..TODO  length = 9*)

    50     |> filter_out (fn (thyID, _) => "??.unknown" = thyID) (*DELETE AFTER ^^^..TODO*)

    52   val rlsthmsNOTisac = isacrlsthms          (*length = 49*)

    53     |> filter (fn (deriv, _) =>

    54       member op= (map Context.theory_name isabthys') (thyID_of_derivation_name deriv))

    55     : (thmID * term) list

    56 *}

    58 subsubsection {* Collect data in a (key, data) list and insert data into the tree *}

    59 text {*

    60   The sequence in the (key, data) list is arbitrary, because insertion using the key

    61   is random. The sequence of the root nodes "IsacKnowledge", "Isabelle"

    62   and "IsacScripts" is determined in KEStore.thy.

    63 *}

    64 ML {*

    65 val thydata_list =

    66   collect_part       "IsacKnowledge" knowledge_parent knowthys' @

    67   (map (collect_isab "Isabelle") rlsthmsNOTisac) @

    68   collect_part       "IsacScripts" proglang_parent progthys'

    69 : (theID * thydata) list

    70 *}

    71 setup {* KEStore_Elems.add_thes (map swap thydata_list) *}

    73 section {* interface for dialog-authoring *}

    74 subsection {* Add error patterns *}

    75 subsubsection {* Error patterns for differentiation *}

    77 setup {* KEStore_Elems.add_mets

    78   [update_metpair @{theory Diff} ["diff","differentiate_on_R"]

    79       [("chain-rule-diff-both",

    80         [parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",

    81           parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",

    82           parse_patt @{theory Diff} "d_d ?bdv (?u ^^^ ?n) = ?n * ?u ^^^ (?n - 1)",

    83           parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",

    84           parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],

    85         [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @{thm diff_ln_chain},

    86           @{thm  diff_exp_chain}])]]

    87 *}

    89 setup {*

    90 KEStore_Elems.insert_fillpats

    91   [(["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"],

    92     ([("fill-d_d-arg",

    93       parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),

    94     ("fill-both-args",

    95       parse_patt @{theory Diff} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),

    96     ("fill-d_d",

    97       parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),

    98     ("fill-inner-deriv",

    99       parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),

   100     ("fill-all",

   101       parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: fillpat list))

   102   ]

   103 *}

   105 subsubsection {* Error patterns for calculation with rationals *}

   107 setup {* KEStore_Elems.add_mets

   108   [update_metpair @{theory Rational} ["simplification", "of_rationals"]

   109       [("addition-of-fractions",

   110         [parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b + ?d)",

   111           parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?a + ?c)/(?b * ?d)",

   112           parse_patt @{theory Rational} "(?a / ?b + ?c / ?d) = (?c * ?a)/(?d * ?b)",

   113           parse_patt @{theory Rational} "?a + (?b /?c)= (?a + ?b)/ ?c",

   114           parse_patt @{theory Rational} "?a + (?b /?c)= (?a * ?b)/ ?c"],

   115         [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, @{thm rat_add1_assoc},

   116           @{thm rat_add2}, @{thm rat_add2_assoc}, @{thm rat_add3}, @{thm rat_add3_assoc}])]]

   117 *}

   119 ML {*

   120 (*TODO insert_fillpats ["IsacKnowledge", "Rational", "Theorems", "???"]*)

   122 (* TODO insert_errpats overwrites instead of appending

   123 insert_errpats ["simplification","of_rationals"]

   124  (("cancel", (*see master thesis gdarocy*)

   125     [(*a*)parse_patt @{theory Rational} "(?a + ?b)/?a = ?b",

   126      (*b*)parse_patt @{theory Rational} "(?a + ?b)/?b = ?a",

   127      (*c*)parse_patt @{theory Rational} "(?a + ?b)/(?b + ?c) = ?a / ?c",

   128      (*d*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?b",

   129      (*e*)parse_patt @{theory Rational} "(?a + ?c)/(?b + ?c) = ?a / ?c",

   130      (*f*)parse_patt @{theory Rational} "(?a + ?b)/(?c + ?a) = ?b / ?c",

   131      (*g*)parse_patt @{theory Rational} "(?a*?b + ?c)/?a = ?b + ?c",

   132      (*h*)parse_patt @{theory Rational} "(?a*?b + ?c)/?b = ?a + ?c",

   133      (*i*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?c",

   134      (*j*)parse_patt @{theory Rational} "(?a + ?b*?c)/?b = ?a + ?b",

   135      (*k*)parse_patt @{theory Rational} "(?a + ?b*?e)/(?c + ?d*?e) = (?a + ?b)/(?c + ?d)"],

   136     [@{thm real_times_divide_1_eq}, (*TODO*) @{thm real_times_divide_1_eq}]));

   138 val fillpats = [

   139   ("fill-cancel-left-num",

   140     parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = _ / ?c", "cancel"),

   141   ("fill-cancel-left-den",

   142     parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / _", "cancel"),

   143   ("fill-cancel-none",

   144     parse_patt @{theory Rational} "(?a * ?b) / (?a * ?c) = ?b / ?c", "cancel"),

   146   ("fill-cancel-left-add-num1",

   147     parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / ?d", "cancel"),

   148   ("fill-cancel-left-add-num2",

   149     parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / ?d", "cancel"),

   150   ("fill-cancel-left-add-num3",

   151     parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + _) / ?d", "cancel"),

   152   ("fill-cancel-left-add-num4",

   153     parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / _", "cancel"),

   154   ("fill-cancel-left-add-num5",

   155     parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (_ + ?c) / _", "cancel"),

   156   ("fill-cancel-left-add-num6",

   157     parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + _) / _", "cancel"),

   158   ("fill-cancel-left-add-none",

   159     parse_patt @{theory Rational} "(?a * (?b + ?c)) / (?a * ?d) = (?b + ?c) / ?d", "cancel"),

   161   ("fill-cancel-left-add-den1",

   162     parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

   163   ("fill-cancel-left-add-den2",

   164     parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

   165   ("fill-cancel-left-add-den3",

   166     parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

   167   ("fill-cancel-left-add-den4",

   168     parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

   169   ("fill-cancel-left-add-den5",

   170     parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

   171   ("fill-cancel-left-add-den6",

   172     parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel"),

   173   ("fill-cancel-left-add-none",

   174     parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel")

   175  ]: fillpat list;

   176 *)

   178 (* still ununsed; planned for stepToErrorpattern: this is just a reminder... *)

   180 insert_errpatIDs @{theory} ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]

   181   (["chain-rule-diff-both", "cancel"]: errpatID list);

   183 (* ...and all other related rls by hand;

   184    TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)

   185 *}

   187 subsection {* Generate XML representation from SML (data in KEStore) *}

   188 text {*

   189   See the wiki

   190   http://www.ist.tugraz.at/isac/Generate_representations_for_ISAC_Knowledge#Step_1:_Generate_XML_representation_from_SML

   192   val path = "/tmp/xmldata/";

   193   thy_hierarchy2file (path ^ "thy/");

   194   thes2file          (path ^ "thy/");

   195   pbl_hierarchy2file (path ^ "pbl/");

   196   pbls2file          (path ^ "pbl/");

   197   met_hierarchy2file (path ^ "met/");

   198   mets2file          (path ^ "met/");

   200   Adjust ''val path'' (for details see wiki) and copy line for line

   201   into the ML-block below:

   202 *}

   204 section {* Link KEStore_Elems to completed IsacKnowledge *}

   205 ML {* KEStore_Elems.set_ref_thy @{theory} *}

   207 end

author	Walther Neuper <neuper@ist.tugraz.at>
	Sun, 22 Jun 2014 15:22:30 +0200
changeset 55460	ee6ffa1fc437
parent 55456	467ccd9ef7d6
child 55462	e308b31f0405
permissions	-rw-r--r--