(*  Title:      Tools/isac/Knowledge/Build_Thydata.thy

     Author:     Walther Neuper, JKU Linz

     (c) due to copyright terms

 Collect all knowledge defined for the isac mathengine

 *)

 theory Build_Thydata

 imports

   Isac_Knowledge

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

 begin

 subsection \<open>Build <Theory>-Data\<close>

 text \<open>

   <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 under normal circumstances, theories are only available from the given formal

   context, not the global theory database (\<^ML_structure>\<open>Thy_Info\<close>). The following

   operations always work:

     \<^item> \<^ML>\<open>@{theory Pure}\<close>, \<^ML>\<open>@{theory Main}\<close>, \<^ML>\<open>@{theory Complex_Main}\<close>

     \<^item> \<^ML>\<open>Theory.ancestors_of\<close>, or better \<^ML>\<open>Theory.nodes_of\<close>

     \<^item> \<^ML>\<open>Context.get_theory\<close> for situations of explicit name-lookup (short or long)

   In contrast, old-style \<^ML>\<open>Thy_Info.get_theory\<close> requires a finished logic image, for

   example in \<^file>\<open>$ISABELLE_ISAC_TEST/Tools/isac/Test_Some.thy\<close> loaded from session Isac.

   All theories below ML_structure\<open>MathEngine\<close> in the theories' dependency graph

   can be considered as Isac's version of Pure: the respective code handles items

   declared later between \<^ML>\<open>@{theory Base_Tools}\<close> and \<^ML>\<open>@{theory Isac_Knowledge}\<close>.

   These items are contained in the  ML_structure\<open>Context\<close> in current Isabelle,

   thus all ML_structure\<open>Know_Store\<close> can be replaced by more native Isabelle mechanisms --

   with two exceptions

     \<^item> \<^ML>\<open>Know_Store.add_pbls\<close> and \<^ML>\<open>Know_Store.get_pbls\<close>, 

       handling a tree of \<^ML_type>\<open>Problem.T\<close>

     \<^item> \<^ML>\<open>Know_Store.add_mets\<close> and \<^ML>\<open>Know_Store.get_mets\<close>, 

       handling a tree of \<^ML_type>\<open>MethodC.T\<close>

   where both trees have a structure independent from the dependency graph 

   between \<^ML>\<open>@{theory Base_Tools}\<close> and \<^ML>\<open>@{theory Isac_Knowledge}\<close>.

 \<close>

 subsubsection \<open>Get and group the theories defined in Isac\<close>

 ML \<open>

   (* 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 MathEngine},

     @{theory BridgeLibisabelle}, knowledge_parent]) allthys         (*["Isac_Knowledge", ..., "Isac_Knowledge"]*)

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

     drop ((find_index (curry Context.eq_thy ThyC.last_isabelle_thy) allthys), allthys);

   val isacthys' =                         (*["Isac_Knowledge", "Inverse_Z_Transform",  .., "Know_Store"]*)

     take ((find_index (curry Context.eq_thy ThyC.last_isabelle_thy) allthys), allthys)

     |> remove Context.eq_thy @{theory Test_Build_Thydata};

   val knowthys' =                         (*["Isac_Knowledge", .., "Input_Descript"]*)

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

   val progthys' =                         (*["Auto_Prog", .., "Know_Store"]*)

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

     |> remove Context.eq_thy @{theory BaseDefinitions};

 \<close> 

 declare[[ML_print_depth = 999]]

 ML \<open>

 \<close> ML \<open>

 \<close> ML \<open>

 \<close>

 subsubsection \<open>From rule-sets collect theorems, which have been taken from Isabelle\<close>

 ML \<open>

   val isacrlsthms =                      (*length = 460*)

     Thy_Hierarchy.thms_of_rlss @{theory} (Know_Store.get_rlss knowledge_parent) : ThmC.T list

   val rlsthmsNOTisac = isacrlsthms       (*length =  36*)

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

       member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))

     : ThmC.T list

 \<close> 

 subsubsection \<open>Collect data in a (key, data) list and insert data into the tree\<close>

 text \<open>

   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 Know_Store.thy.

 \<close>

 text \<open>

   ATTENTION: ===================================================================================

   the code below does NOT terminate in x86_64_32 mode of Poly/ML 5.8.

   Nevertheless, Build_Isac.thy should (and can!) be used in this mode,

   while preferences ML_system_64 = "true" never reaches Build_Isac.thy.

   ==============================================================================================

   See "etc/preferences".

 \<close>

 ML \<open>

 val thydata_list = (* SEE NOTE ABOVE *)

   Thy_Hierarchy.collect_part       "IsacKnowledge" knowledge_parent knowthys' @

   (map (Thy_Hierarchy.collect_isab "Isabelle") rlsthmsNOTisac) @

   Thy_Hierarchy.collect_part       "IsacScripts" proglang_parent progthys'

 : (Thy_Write.theID * Thy_Write.thydata) list

 \<close>

 ML \<open>

 map Context.theory_name knowthys'

 \<close> ML \<open>

 Context.theory_name knowledge_parent

 \<close> text \<open>

   collect_part       "IsacKnowledge" knowledge_parent knowthys'

 \<close> ML \<open>

 "~~~~~ fun collect_part , args:"; val (part, parent, thys) = ("IsacKnowledge", knowledge_parent, knowthys');

 \<close> ML \<open>

     val xxx = (flat (map (Thy_Hierarchy.collect_thms part) thys))

 \<close> ML \<open> (*isa*)

 length thys = 32;

 length xxx = 471

 \<close> text \<open>

      (collect_rlss part (Know_Store.get_rlss parent) thys)

 \<close> text \<open>

 "~~~~~ fun collect_rlss , args:"; val (part, rlss, thys) = (part, (Know_Store.get_rlss parent), thys);

 \<close> text \<open>

 (* Build_Thydata.thy in jedit leads to "Exception- Size raised" <<<=============================== 

    =============================== but batch process =============================================

      ~~$ ./bin/isabelle build -o browser_info -v -b Isac

    =============================== works =========================================================

 *)

 Know_Store.get_rlss parent

 \<close>

 setup \<open>Know_Store.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>

 section \<open>interface for dialog-authoring\<close>

 subsection \<open>Add error patterns\<close>

 subsubsection \<open>Error patterns for differentiation\<close>

 setup \<open>Know_Store.add_mets @{context}

   [Pbl_Met_Hierarchy.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 \<up> ?n) = ?n * ?u \<up> (?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}])]]

 \<close>

 setup \<open>

 Know_Store.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")]: Error_Pattern_Def.fill_in list))

   ]

 \<close>

 subsubsection \<open>Error patterns for calculation with rationals\<close>

 setup \<open>Know_Store.add_mets @{context}

   [Pbl_Met_Hierarchy.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}])]]

 \<close>

 ML \<open>

 (*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 Know_Store.set_ref_last_thy has been shifted below;

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

    ...and all other related rls by hand;

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

 \<close>

 section \<open>Link Know_Store to completed IsacKnowledge\<close>

 ML \<open>Know_Store.set_ref_last_thy @{theory}\<close>

 end