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