(* theory collecting all knowledge defined for the isac mathengine

    WN.11.00

  *)

 theory Build_Thydata

 imports 

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

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

 begin

 subsection {* Build <Theory>-Data *}

 text {*

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

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

   comprise theories from ProgLang and from Knowledge.

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

   via "@{theory Pure}" and "Theory.ancestors_of" but not via "Thy_Info_get_theory"

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

 *}

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

 ML {*

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

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

   val knowledge_parent = @{theory}

   val proglang_parent = @{theory ProgLang}

   val allthys = Theory.ancestors_of @{theory};

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

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

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

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

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

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

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

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

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

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

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

 *}

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

 ML {*

   val isacrlsthms =                      (*length = 460*)

     thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (Celem.thmID * thm) list

   val rlsthmsNOTisac = isacrlsthms       (*length =  36*)

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

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

     : (Celem.thmID * thm) list

 *} 

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

 text {*

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

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

   and "IsacScripts" is determined in KEStore.thy.

 *}

 ML {*

 val thydata_list = 

   collect_part       "IsacKnowledge" knowledge_parent knowthys' @

   (map (collect_isab "Isabelle") rlsthmsNOTisac) @

   collect_part       "IsacScripts" proglang_parent progthys'

 : (Celem.theID * Celem.thydata) list

 *}

 setup {* KEStore_Elems.add_thes (map (fn (a, b) => (b, a)) thydata_list) *}

 section {* interface for dialog-authoring *}

 subsection {* Add error patterns *}

 subsubsection {* Error patterns for differentiation *}

 setup {* KEStore_Elems.add_mets

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

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

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

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

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

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

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

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

           @{thm  diff_exp_chain}])]]

 *}

 setup {*

 KEStore_Elems.insert_fillpats

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

     ([("fill-d_d-arg",

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

     ("fill-both-args",

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

     ("fill-d_d",

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

     ("fill-inner-deriv",

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

     ("fill-all",

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

   ]

 *}

 subsubsection {* Error patterns for calculation with rationals *}

 setup {* KEStore_Elems.add_mets

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

       [("addition-of-fractions",

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

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

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

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

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

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

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

 *}

 ML {*

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

 (* TODO insert_errpats overwrites instead of appending

 insert_errpats ["simplification","of_rationals"]

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

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

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

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

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

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

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

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

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

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

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

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

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

 val fillpats = [

   ("fill-cancel-left-num",

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

   ("fill-cancel-left-den",

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

   ("fill-cancel-none",

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  ]: fillpat list;

 *)

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

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

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

 [[[ERROR *** app_py: not found: ["IsacKnowledge","Diff","Rulesets","norm_diff"]

   since KEStore_Elems.set_ref_thy has been shifted below;

   this ERROR will vanish during re-engineering towards KEStore_Elems.]]]

    ...and all other related rls by hand;

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

 *}

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

 text {*

   See the wiki 

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

   val path = "/tmp/xmldata/"; 

   thy_hierarchy2file (path ^ "thy/");

   thes2file          (path ^ "thy/");

   pbl_hierarchy2file (path ^ "pbl/");

   pbls2file          (path ^ "pbl/");

   met_hierarchy2file (path ^ "met/");

   mets2file          (path ^ "met/");

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

   into an ML-block.

   Scroll down the Output window and look for potential error messages.

 *}

 section {* Link KEStore_Elems to completed IsacKnowledge *}

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

 end