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

val 34 = length thys;

val 479 = length xxx;

\<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