1.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy	Thu Dec 22 17:06:19 2022 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy	Fri Jan 06 08:04:36 2023 +0100
     1.3 @@ -133,23 +133,31 @@
     1.4  setup \<open>Know_Store.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>
     1.5  
     1.6  section \<open>interface for dialog-authoring\<close>
     1.7 -subsection \<open>Add error patterns\<close>
     1.8 -subsubsection \<open>Error patterns for differentiation\<close>
     1.9 +text \<open>
    1.10 +  Dialog authoring needs re-dsign since error patterns went to theories they are defined in.
    1.11 +\<close>
    1.12  
    1.13 +(*DELETE
    1.14 +  subsubsection \<open>Error patterns for differentiation\<close>
    1.15 +  vvv--- replaced by Diff: setup \<open>Error_Pattern.store_fill_ins ???..
    1.16 +  ATTENTION: while "eliminate thy-hierarchy 1: make find_fill_patterns independent"
    1.17 +  THE errpat "chain-rule-diff-both" IS FOUND ONLY WITH MethodC.from_store' @{theory Build_Thydata},
    1.18 +  see test --- re-build: fill_from_store without thy-hierarchy ---
    1.19 +*)
    1.20  setup \<open>Know_Store.add_mets @{context}
    1.21    [Pbl_Met_Hierarchy.update_metpair @{theory Diff} ["diff", "differentiate_on_R"]
    1.22 -      [("chain-rule-diff-both",
    1.23 -        [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
    1.24 -         TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
    1.25 -         TermC.parse_patt @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
    1.26 -         TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
    1.27 -         TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
    1.28 -        [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @{thm diff_ln_chain},
    1.29 -          @{thm  diff_exp_chain}])]]
    1.30 -\<close>
    1.31 +    [("chain-rule-diff-both",
    1.32 +      [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
    1.33 +       TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
    1.34 +       TermC.parse_patt @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)"(*,
    1.35 +       TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
    1.36 +       TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"*)],
    1.37 +      [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}(*, @{thm diff_ln_chain},
    1.38 +        @{thm  diff_exp_chain}*)])]
    1.39 +  ]\<close>
    1.40  
    1.41 -setup \<open>
    1.42 -Know_Store.insert_fillpats
    1.43 +(*vvv--- replaced by Diff: setup \<open>Error_Pattern.store_fill_ins*)
    1.44 +setup \<open>Know_Store.insert_fillpats
    1.45    [(["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"],
    1.46      ([("fill-d_d-arg",
    1.47        TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
    1.48 @@ -161,11 +169,12 @@
    1.49        TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
    1.50      ("fill-all",
    1.51        TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Error_Pattern_Def.fill_in list))
    1.52 -  ]
    1.53 -\<close>
    1.54 +  ]\<close>
    1.55  
    1.56 -subsubsection \<open>Error patterns for calculation with rationals\<close>
    1.57 -
    1.58 +(*
    1.59 +  subsubsection \<open>Error patterns for calculation with rationals\<close>
    1.60 +  replaced by Rational.thy: setup \<open>Error_Pattern.store_fill_ins
    1.61 +*)
    1.62  setup \<open>Know_Store.add_mets @{context}
    1.63    [Pbl_Met_Hierarchy.update_metpair @{theory Rational} ["simplification", "of_rationals"]
    1.64        [("addition-of-fractions",
    1.65 @@ -177,7 +186,6 @@
    1.66          [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, @{thm rat_add1_assoc},
    1.67            @{thm rat_add2}, @{thm rat_add2_assoc}, @{thm rat_add3}, @{thm rat_add3_assoc}])]]
    1.68  \<close>
    1.69 -
    1.70  ML \<open>
    1.71  (*TODO insert_fillpats ["IsacKnowledge", "Rational", "Theorems", "???"]*)
    1.72  
    1.73 @@ -236,20 +244,14 @@
    1.74      parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel")
    1.75   ]: fillpat list;
    1.76  *)
    1.77 -
    1.78 -(* still ununsed; planned for stepToErrorpattern: this is just a reminder... 
    1.79 -
    1.80 -insert_errpatIDs @{theory} ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
    1.81 -  (["chain-rule-diff-both", "cancel"]: errpatID list);
    1.82 -[[[ERROR *** app_py: not found: ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
    1.83 -  since Know_Store.set_ref_last_thy has been shifted below;
    1.84 -  this ERROR will vanish during re-engineering towards Know_Store.]]]
    1.85 -
    1.86 -   ...and all other related rls by hand;
    1.87 -   TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)
    1.88  \<close>
    1.89  
    1.90  section \<open>Link Know_Store to completed IsacKnowledge\<close>
    1.91  ML \<open>Know_Store.set_ref_last_thy @{theory}\<close>
    1.92  
    1.93 +ML \<open>
    1.94 +\<close> ML \<open>
    1.95 +\<close> ML \<open>
    1.96 +\<close> 
    1.97 +
    1.98  end