1.1 --- a/src/Tools/isac/BaseDefinitions/Know_Store.thy Thu Dec 22 17:06:19 2022 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/Know_Store.thy Fri Jan 06 08:04:36 2023 +0100
1.3 @@ -86,7 +86,7 @@
1.4 val add_expls: (Example.T * Store.key) list -> theory -> theory
1.5 val get_thes: theory -> (Thy_Write.thydata Store.node) list
1.6 val add_thes: (Thy_Write.thydata * Thy_Write.theID) list -> theory -> theory
1.7 - val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
1.8 + val insert_fillpats: (Thy_Write.theID * Error_Pattern_Def.fill_in list) list -> theory -> theory
1.9 val get_ref_last_thy: unit -> theory
1.10 val set_ref_last_thy: theory -> unit
1.11 val get_via_last_thy: ThyC.id -> theory (*only used for (Sub-)problem retrieving respective thy*)
2.1 --- a/src/Tools/isac/BaseDefinitions/error-pattern-def.sml Thu Dec 22 17:06:19 2022 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/error-pattern-def.sml Fri Jan 06 08:04:36 2023 +0100
2.3 @@ -24,11 +24,10 @@
2.4 type id = Rule_Def.errpatID
2.5
2.6 type T =
2.7 - id (* one identifier for a list of patterns *)
2.8 + id (* one identifier for a list of error patterns *)
2.9 * term list (* error patterns *)
2.10 * thm list (* thms related to error patterns; note that respective lhs
2.11 - do not match (which reflects student's error).
2.12 - fillpatterns are stored with these thms. *)
2.13 + do not match (which reflects student's error). *)
2.14 fun errpat2str (id, tms, thms) =
2.15 "(\"" ^ id ^ "\",\n" ^ UnparseC.terms tms ^ ",\n" ^ ThmC_Def.string_of_thms thms
2.16 fun s_to_string errpats = (strs2str' o (map errpat2str)) errpats
3.1 --- a/src/Tools/isac/BaseDefinitions/substitution.sml Thu Dec 22 17:06:19 2022 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/substitution.sml Fri Jan 06 08:04:36 2023 +0100
3.3 @@ -21,6 +21,7 @@
3.4 type program = term (* in programs: @{term "[(''bdv_1'', x::real), ..]} *)
3.5 type input = TermC.as_string list (* by student: ["(''bdv'', x)", ..] *)
3.6 val input_empty: input
3.7 + val string_of_input: input -> string
3.8
3.9 type as_string_eqs (* for Tactic.Substitute ["bdv_1 = x", ...] *)
3.10 val string_eqs_to_string: as_string_eqs -> string
3.11 @@ -61,6 +62,7 @@
3.12
3.13 type input = TermC.as_string list;
3.14 val input_empty = [];
3.15 +fun string_of_input ins = strs2str' ins
3.16
3.17 type as_string_eqs = TermC.as_string list;
3.18 \<^isac_test>\<open>
4.1 --- a/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Thu Dec 22 17:06:19 2022 +0100
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/pbl-met-hierarchy.sml Fri Jan 06 08:04:36 2023 +0100
4.3 @@ -16,7 +16,7 @@
4.4 val met_hierarchy2file : filepath -> filepath * string
4.5 val pbl_hierarchy2file_test : filepath -> filepath * string
4.6 val met_hierarchy2file_test : filepath -> filepath * string
4.7 - val update_metpair: theory -> MethodC.id -> Error_Pattern_Def.T list -> MethodC.T * MethodC.id
4.8 + val update_metpair: theory -> MethodC.id -> Error_Pattern.T list -> MethodC.T * MethodC.id
4.9 end
4.10
4.11 (**)
4.12 @@ -115,16 +115,17 @@
4.13
4.14
4.15 fun update_metdata
4.16 - ({guh, mathauthors, start_refine, rew_ord, asm_rls, prog_rls, where_rls, (*crls,*) rew_rls, calc, model, where_, program, ...}: MethodC.T)
4.17 - errpats' =
4.18 - {guh = guh, mathauthors = mathauthors, start_refine = start_refine, rew_ord = rew_ord, asm_rls = asm_rls,
4.19 - prog_rls = prog_rls, where_rls = where_rls, (*crls = crls,*) rew_rls = rew_rls, calc = calc,
4.20 + ({guh, mathauthors, start_refine, rew_ord, asm_rls, prog_rls, where_rls, rew_rls, calc, model,
4.21 + where_, program, ...}: MethodC.T) errpats' =
4.22 + {guh = guh, mathauthors = mathauthors, start_refine = start_refine, rew_ord = rew_ord,
4.23 + asm_rls = asm_rls, prog_rls = prog_rls, where_rls = where_rls, rew_rls = rew_rls, calc = calc,
4.24 model = model, where_ = where_, program = program, errpats = errpats'}: MethodC.T
4.25
4.26 (* interface for dialog-authoring: call in Buld_Thydata.thy only ! *)
4.27 -fun update_metpair thy metID errpats = let
4.28 - val ret = (update_metdata (MethodC.from_store' thy metID) errpats, metID)
4.29 - handle ERROR _ => raise ERROR ("update_metpair: " ^ (strs2str metID) ^ " must address a method");
4.30 - in ret end;
4.31 +fun update_metpair thy metID errpats =
4.32 + let
4.33 + val ret = (update_metdata (MethodC.from_store' thy metID) errpats, metID)
4.34 + handle ERROR _ => raise ERROR ("update_metpair: " ^ strs2str metID ^ " must address a method");
4.35 + in ret end;
4.36
4.37 (**)end(**)
5.1 --- a/src/Tools/isac/Build_Isac.thy Thu Dec 22 17:06:19 2022 +0100
5.2 +++ b/src/Tools/isac/Build_Isac.thy Fri Jan 06 08:04:36 2023 +0100
5.3 @@ -164,12 +164,22 @@
5.4 begin
5.5 ML \<open>
5.6 \<close> ML \<open>
5.7 +val {errpats, program = Rule.Prog prog, ...} =
5.8 + MethodC.from_store @{context} ["diff", "differentiate_on_R"]
5.9 \<close> ML \<open>
5.10 +val 1 = length errpats
5.11 \<close> ML \<open>
5.12 \<close> ML \<open>
5.13 \<close>
5.14 -subsection \<open>basic functionality on simple example first -- cp for first tests\<close>
5.15 -(**)
5.16 +subsection \<open>make Minisubpbl independent from Thy_Info\<close>
5.17 +text \<open>
5.18 + We want Isac to become independent from sessions Specify, Interpret and Isac.
5.19 + This goal will be checked by the tests finally.
5.20 + As first step we go top down and make Minisubpbl independent form Thy_Info here
5.21 + and make sure, that the right ctxt is passed throughout the code.
5.22 + As next step we go bottom up from Thy_Info.get_theory and remove it.
5.23 + Afterwards $ISABELLE_ISAC_TEST will be changed accordingly.
5.24 +\<close>
5.25 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
5.26 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
5.27 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
5.28 @@ -194,11 +204,6 @@
5.29 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/790-complete.sml"
5.30 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/800-append-on-Frm.sml"
5.31
5.32 -text \<open>
5.33 - show theory dependencies using the graph browser,
5.34 - open "browser_info/HOL/Isac/session.graph"
5.35 - and proceed from the ancestors towards the siblings.
5.36 -\<close>
5.37
5.38 section \<open>check presence of definitions from directories\<close>
5.39
6.1 --- a/src/Tools/isac/Interpret/Interpret.thy Thu Dec 22 17:06:19 2022 +0100
6.2 +++ b/src/Tools/isac/Interpret/Interpret.thy Fri Jan 06 08:04:36 2023 +0100
6.3 @@ -29,6 +29,33 @@
6.4 if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then ()
6.5 else raise ERROR "theory dependencies not as anticipated in ThyC"
6.6 end
6.7 +\<close> ML \<open> (*\------------------------------------ keep ------------------------------------------/*)
6.8 +\<close> text \<open> (* error in Integrate, EqSystem *)
6.9 +open ThyC (* <---------------------------------------------------------------------------------*)
6.10 +
6.11 + type authors = string list; (* no more for thm, rls, rew_ord, cal *)
6.12 + type metadata = {coursedesign: authors, html: string, mathauthors: authors}
6.13 +(*WAS IN Thy_Write: datatype thydata
6.14 + = ...
6.15 + | Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}*)
6.16 +
6.17 + structure Data = Theory_Data
6.18 + (
6.19 + type T = metadata option;
6.20 + val empty = NONE; (*####### TODO: Htmldefault mit 2006 nehmen ############################*)
6.21 + fun merge _ = NONE;
6.22 + );
6.23 + val the_metadata = the o Data.get;
6.24 + val set_metadata = Data.put o SOME;
6.25 +
6.26 +the_metadata: theory -> metadata;
6.27 +set_metadata: metadata -> theory -> theory;
6.28 +\<close> text \<open>
6.29 +open Error_Pattern (* <------------------------------------------------------------------------*)
6.30 +\<close> ML \<open>
6.31 +\<close> text \<open> (*Pbl_Met_Hierarchy.update_metpair WITHIN Know_Store.add_mets AS MODEL*)
6.32 +fun insert_in_method thy metID errpats = 123
6.33 +
6.34 \<close> ML \<open>
6.35 \<close> ML \<open>
6.36 \<close>
7.1 --- a/src/Tools/isac/Interpret/error-pattern.sml Thu Dec 22 17:06:19 2022 +0100
7.2 +++ b/src/Tools/isac/Interpret/error-pattern.sml Fri Jan 06 08:04:36 2023 +0100
7.3 @@ -4,7 +4,7 @@
7.4 (c) due to copyright terms
7.5
7.6 In case a term is input, which contains an "error pattern" (provided by a mathauthor),
7.7 -several "fill patterns" can be presented as help for the next step.)
7.8 +several "fill_ins" can be presented as help for the next step.)
7.9 *)
7.10
7.11 signature ERROR_PATTERN =
7.12 @@ -18,20 +18,24 @@
7.13 type fill_in = Error_Pattern_Def.fill_in
7.14 val fill_in_empty: fill_in
7.15
7.16 - type record
7.17 -
7.18 - val from_store: Proof.context -> Tactic.input -> Error_Pattern_Def.id list
7.19 + val from_store: Proof.context -> Tactic.input -> id list
7.20 val filled_exactly: Calc.T -> string -> string * Tactic.input
7.21 val check_for: Proof.context -> term * term -> term * Env.T -> T list * Rule_Set.T -> id option
7.22
7.23 + val get_fill_ins: theory -> fill_in_id -> fill_in list
7.24 + val store_fill_ins: (fill_in_id * fill_in list) list -> theory -> theory
7.25 + type record
7.26 +(*val find_fill_ins: Calc.T -> id -> record list*)
7.27 val find_fill_patterns: Calc.T -> id -> record list
7.28 -
7.29 -\<^isac_test>\<open>
7.30 - val check_for': Proof.context -> term * term -> subst -> id * term -> Rule_Set.T -> id option
7.31 +(*from isac_test for Minisubpbl*)
7.32 val fill_from_store: Proof.context -> Subst.input option * Subst.T -> term -> id -> thm ->
7.33 record list
7.34 val fill_form: Proof.context -> Subst.input option * Subst.T -> thm * term -> id -> fill_in ->
7.35 record option
7.36 +
7.37 +\<^isac_test>\<open>
7.38 + val get_fill_inss: theory -> (fill_in_id * fill_in list) list
7.39 + val check_for': Proof.context -> term * term -> subst -> id * term -> Rule_Set.T -> id option
7.40 \<close>
7.41 end
7.42
7.43 @@ -51,6 +55,20 @@
7.44
7.45 type record = (fill_in_id * term * thm * Subst.input option);
7.46
7.47 +structure Data = Theory_Data (
7.48 + type T = (fill_in_id * fill_in list) list;
7.49 + val empty = [];
7.50 + val merge = merge op=;
7.51 + );
7.52 +fun get_fill_inss thy = Data.get thy
7.53 +fun store_fill_ins fill_in = Data.map (curry (Library.merge op=) fill_in)
7.54 +fun get_fill_ins thy fill_in_id =
7.55 + case AList.lookup (op =) (get_fill_inss thy) fill_in_id of
7.56 + SOME fill_ins => fill_ins
7.57 + | NONE => raise ERROR ("fill_ins for thm \"" ^ fill_in_id ^ "\" missing in theory \"" ^
7.58 + (thy |> ThyC.id_of) ^ "\" (and ancestors)" ^
7.59 + "\nTODO exception hierarchy needs to be established.")
7.60 +
7.61 (*
7.62 check if (agreed result, input formula) matches the error pattern "pat" modulo simplifier rls
7.63 *)
7.64 @@ -62,7 +80,7 @@
7.65 in
7.66 if rewritten then
7.67 let
7.68 - val norm_res = case Rewrite.rewrite_set_inst_ ctxt false subst rls res' of
7.69 + val norm_res = case Rewrite.rewrite_set_inst_ ctxt false subst rls res' of
7.70 NONE => res'
7.71 | SOME (norm_res, _) => norm_res
7.72 val norm_inf = case Rewrite.rewrite_set_inst_ ctxt false subst rls inf of
7.73 @@ -105,25 +123,23 @@
7.74 else NONE
7.75 end
7.76
7.77 -fun fill_from_store ctxt subst form id thm =
7.78 +fun fill_from_store ctxt subst form errpat_id thm =
7.79 let
7.80 - val thmDeriv = Thm.get_name_hint thm
7.81 - val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
7.82 - val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
7.83 - val fillpats = case Thy_Read.from_store ctxt theID of
7.84 - Thy_Write.Hthm {fillpats, ...} => fillpats
7.85 - | _ => raise ERROR "fill_from_store: uncovered case of get_the"
7.86 - val some = map (fill_form ctxt subst (thm, form) id) fillpats
7.87 + val thm_id_long = Thm.get_name_hint thm
7.88 + val thm_id = ThmC.cut_id thm_id_long
7.89 + val fill_ins = get_fill_ins (Proof_Context.theory_of ctxt) thm_id;
7.90 + val some = map (fill_form ctxt subst (thm, form) errpat_id) fill_ins;
7.91 in some |> filter is_some |> map the end
7.92
7.93 fun find_fill_patterns (pt, pos as (p, _): Pos.pos') id =
7.94 let
7.95 - val f_curr = Ctree.get_curr_formula (pt, pos);
7.96 - val (_, _, _, ctxt) = LItool.parent_node pt pos (*-------------------- double code*)
7.97 - val pp = Ctree.par_pblobj pt p (*by ^^^^^^^ replace with extension --- double code*)
7.98 - val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
7.99 - {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
7.100 - | _ => raise ERROR "find_fill_patterns: uncovered case of get_met"
7.101 + val ctxt = Ctree.get_ctxt pt pos
7.102 + val f_curr = Ctree.get_curr_formula (pt, pos)
7.103 + val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
7.104 + val (errpats, prog) =
7.105 + case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
7.106 + {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
7.107 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
7.108 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
7.109 val subst = Subst.for_bdv ctxt prog env
7.110 val errpatthms = errpats
7.111 @@ -173,7 +189,7 @@
7.112 Thy_Write.Hrls {thy_rls = (_, rls), ...} => rls
7.113 | _ => raise ERROR "from_store: uncovered case of get_the"
7.114 in case rls of
7.115 - Rule_Def.Repeat {errpatts, ...} => errpatts
7.116 + Rule_Set.Repeat {errpatts, ...} => errpatts
7.117 | Rule_Set.Sequence {errpatts, ...} => errpatts
7.118 | Rule_Set.Rrls {errpatts, ...} => errpatts
7.119 | Rule_Set.Empty => []
8.1 --- a/src/Tools/isac/Interpret/li-tool.sml Thu Dec 22 17:06:19 2022 +0100
8.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Fri Jan 06 08:04:36 2023 +0100
8.3 @@ -213,7 +213,7 @@
8.4 | associate _ ctxt (tac, _) =
8.5 (trace_msg_3 ctxt tac; Not_Associated);
8.6
8.7 -(* find the next parent, which is either a PblObj xor a PrfObj in case of detail step*)
8.8 +(* in detail step find the next parent, which is either a PblObj xor a PrfObj *)
8.9 fun parent_node _ ([], _) = (true, [], Rule_Set.Empty, ContextC.empty)
8.10 | parent_node pt (pos as (p, _)) =
8.11 let
9.1 --- a/src/Tools/isac/Interpret/step-solve.sml Thu Dec 22 17:06:19 2022 +0100
9.2 +++ b/src/Tools/isac/Interpret/step-solve.sml Fri Jan 06 08:04:36 2023 +0100
9.3 @@ -106,9 +106,10 @@
9.4 ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
9.5 | LI.Not_Derivable =>
9.6 let
9.7 - val (_, _, _, ctxt) = LItool.parent_node pt pos (*--------------- double code*)
9.8 - val pp = Ctree.par_pblobj pt p (*by ^^^^^^^ replace with extension --- double code*)
9.9 - val (errpats, rew_rls, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
9.10 + val ctxt = Ctree.get_ctxt pt pos
9.11 + val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
9.12 + val (errpats, rew_rls, prog) = (* after shift to Diff --vvvvvvvvvvvvvvv ctxt should be sufficient*)
9.13 + case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
9.14 {errpats, rew_rls, program = Rule.Prog prog, ...} => (errpats, rew_rls, prog)
9.15 | _ => raise ERROR "inform: uncovered case of get_met"
9.16 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
10.1 --- a/src/Tools/isac/Interpret/thy-read.sml Thu Dec 22 17:06:19 2022 +0100
10.2 +++ b/src/Tools/isac/Interpret/thy-read.sml Fri Jan 06 08:04:36 2023 +0100
10.3 @@ -7,16 +7,18 @@
10.4
10.5 signature THEORY_STORE_READ =
10.6 sig
10.7 - val thy_containing_thm : string -> string * string
10.8 + val thy_containing_thm : string -> string * ThmC.id
10.9 val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
10.10 val thy_containing_cal : ThyC.id -> Eval_Def.prog_id -> string * string
10.11
10.12 - val for_thy_hierarchy : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
10.13 - val from_store : Proof.context -> Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
10.14 + val for_thy_hierarchy : Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
10.15 + val from_store : Proof.context -> Thy_Write.theID -> Thy_Write.thydata (* for inform.sml *)
10.16 +(*from isac_test for Minisubpbl*)
10.17 + val partID': ThyC.id -> string
10.18 +
10.19 \<^isac_test>\<open>
10.20 val isabthys: unit -> theory list
10.21 val knowthys: unit -> theory list
10.22 - val partID': ThyC.id -> string
10.23 \<close>
10.24 end
10.25 (**)
11.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Dec 22 17:06:19 2022 +0100
11.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Jan 06 08:04:36 2023 +0100
11.3 @@ -133,23 +133,31 @@
11.4 setup \<open>Know_Store.add_thes (map (fn (a, b) => (b, a)) thydata_list)\<close>
11.5
11.6 section \<open>interface for dialog-authoring\<close>
11.7 -subsection \<open>Add error patterns\<close>
11.8 -subsubsection \<open>Error patterns for differentiation\<close>
11.9 +text \<open>
11.10 + Dialog authoring needs re-dsign since error patterns went to theories they are defined in.
11.11 +\<close>
11.12
11.13 +(*DELETE
11.14 + subsubsection \<open>Error patterns for differentiation\<close>
11.15 + vvv--- replaced by Diff: setup \<open>Error_Pattern.store_fill_ins ???..
11.16 + ATTENTION: while "eliminate thy-hierarchy 1: make find_fill_patterns independent"
11.17 + THE errpat "chain-rule-diff-both" IS FOUND ONLY WITH MethodC.from_store' @{theory Build_Thydata},
11.18 + see test --- re-build: fill_from_store without thy-hierarchy ---
11.19 +*)
11.20 setup \<open>Know_Store.add_mets @{context}
11.21 [Pbl_Met_Hierarchy.update_metpair @{theory Diff} ["diff", "differentiate_on_R"]
11.22 - [("chain-rule-diff-both",
11.23 - [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
11.24 - TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
11.25 - TermC.parse_patt @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
11.26 - TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
11.27 - TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
11.28 - [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}, @{thm diff_ln_chain},
11.29 - @{thm diff_exp_chain}])]]
11.30 -\<close>
11.31 + [("chain-rule-diff-both",
11.32 + [TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
11.33 + TermC.parse_patt @{theory Diff} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
11.34 + TermC.parse_patt @{theory Diff} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)"(*,
11.35 + TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
11.36 + TermC.parse_patt @{theory Diff} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"*)],
11.37 + [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain}(*, @{thm diff_ln_chain},
11.38 + @{thm diff_exp_chain}*)])]
11.39 + ]\<close>
11.40
11.41 -setup \<open>
11.42 -Know_Store.insert_fillpats
11.43 +(*vvv--- replaced by Diff: setup \<open>Error_Pattern.store_fill_ins*)
11.44 +setup \<open>Know_Store.insert_fillpats
11.45 [(["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"],
11.46 ([("fill-d_d-arg",
11.47 TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
11.48 @@ -161,11 +169,12 @@
11.49 TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
11.50 ("fill-all",
11.51 TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Error_Pattern_Def.fill_in list))
11.52 - ]
11.53 -\<close>
11.54 + ]\<close>
11.55
11.56 -subsubsection \<open>Error patterns for calculation with rationals\<close>
11.57 -
11.58 +(*
11.59 + subsubsection \<open>Error patterns for calculation with rationals\<close>
11.60 + replaced by Rational.thy: setup \<open>Error_Pattern.store_fill_ins
11.61 +*)
11.62 setup \<open>Know_Store.add_mets @{context}
11.63 [Pbl_Met_Hierarchy.update_metpair @{theory Rational} ["simplification", "of_rationals"]
11.64 [("addition-of-fractions",
11.65 @@ -177,7 +186,6 @@
11.66 [@{thm rat_add}, @{thm rat_add_assoc}, @{thm rat_add1}, @{thm rat_add1_assoc},
11.67 @{thm rat_add2}, @{thm rat_add2_assoc}, @{thm rat_add3}, @{thm rat_add3_assoc}])]]
11.68 \<close>
11.69 -
11.70 ML \<open>
11.71 (*TODO insert_fillpats ["IsacKnowledge", "Rational", "Theorems", "???"]*)
11.72
11.73 @@ -236,20 +244,14 @@
11.74 parse_patt @{theory Rational} "(?a * ?b) / (?a * (?c + ?d)) = ?b / (?c + ?d)", "cancel")
11.75 ]: fillpat list;
11.76 *)
11.77 -
11.78 -(* still ununsed; planned for stepToErrorpattern: this is just a reminder...
11.79 -
11.80 -insert_errpatIDs @{theory} ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
11.81 - (["chain-rule-diff-both", "cancel"]: errpatID list);
11.82 -[[[ERROR *** app_py: not found: ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
11.83 - since Know_Store.set_ref_last_thy has been shifted below;
11.84 - this ERROR will vanish during re-engineering towards Know_Store.]]]
11.85 -
11.86 - ...and all other related rls by hand;
11.87 - TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY *)
11.88 \<close>
11.89
11.90 section \<open>Link Know_Store to completed IsacKnowledge\<close>
11.91 ML \<open>Know_Store.set_ref_last_thy @{theory}\<close>
11.92
11.93 +ML \<open>
11.94 +\<close> ML \<open>
11.95 +\<close> ML \<open>
11.96 +\<close>
11.97 +
11.98 end
12.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Dec 22 17:06:19 2022 +0100
12.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Fri Jan 06 08:04:36 2023 +0100
12.3 @@ -403,6 +403,64 @@
12.4 \<close>
12.5 cas Differentiate = \<open>argl2dtss\<close>
12.6 Problem_Ref: "named/derivative_of/function"
12.7 +
12.8 +section \<open>Error_Pattern\<close>
12.9 +
12.10 +(*replaces Builds_Thydata:
12.11 +setup \<open>Know_Store.insert_fillpats
12.12 + [(["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"],
12.13 + :
12.14 +*)
12.15 +(*WN230105 ? do fill_ins really work wrt. substitutions ?*)
12.16 +setup \<open>Error_Pattern.store_fill_ins
12.17 + [("diff_sin_chain",
12.18 + ([("fill-d_d-arg",
12.19 + TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
12.20 + ("fill-both-args",
12.21 + TermC.parse_patt @{theory} "d_d ?bdv (sin _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
12.22 + ("fill-d_d",
12.23 + TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
12.24 + ("fill-inner-deriv",
12.25 + TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos ?u * _", "chain-rule-diff-both"),
12.26 + ("fill-all",
12.27 + TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")])),
12.28 + ("diff_cos_chain",
12.29 + ([("fill-d_d-arg",
12.30 + TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
12.31 + ("fill-both-args",
12.32 + TermC.parse_patt @{theory} "d_d ?bdv (cos _) = cos ?u * d_d ?bdv _", "chain-rule-diff-both"),
12.33 + ("fill-d_d",
12.34 + TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = cos ?u * _ ?bdv ?u", "chain-rule-diff-both"),
12.35 + ("fill-inner-deriv",
12.36 + TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = cos ?u * _", "chain-rule-diff-both"),
12.37 + ("fill-all",
12.38 + TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = _", "chain-rule-diff-both")])),
12.39 + ("diff_pow_chain",
12.40 + ([("fill-d_d-arg",
12.41 + TermC.parse_patt @{theory} "d_d ?bdv (?u \<up> ?n) = _", "chain-rule-diff-both")]))
12.42 + ]
12.43 +\<close>
12.44 +(** )
12.45 +ML \<open>
12.46 + val fill_ins = get_fill_ins @{theory Diff} "chain-rule-diff-both"
12.47 +ERROR: (*Unfinished theory "Diff"\<^here>*)
12.48 ++ see success at end of Isac_Knowledge.thy
12.49 +\<close>
12.50 +( **)
12.51 +
12.52 +
12.53 +(* still ununsed; planned for stepToErrorpattern: this is just a reminder...
12.54 +
12.55 +insert_errpatIDs @{theory} ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
12.56 + (["chain-rule-diff-both", "cancel"]: errpatID list);
12.57 +[[[ERROR *** app_py: not found: ["IsacKnowledge", "Diff", "Rulesets", "norm_diff"]
12.58 + since Know_Store.set_ref_last_thy has been shifted below;
12.59 + this ERROR will vanish during re-engineering towards Know_Store.]]]
12.60 +
12.61 + ...and all other related rls by hand;
12.62 + TODO: lift errpattIDs from theorems to respective rls AUTOMATICALLY
12.63 +*)
12.64 +
12.65 ML \<open>
12.66 \<close> ML \<open>
12.67 \<close>
13.1 --- a/src/Tools/isac/MathEngBasic/method.sml Thu Dec 22 17:06:19 2022 +0100
13.2 +++ b/src/Tools/isac/MathEngBasic/method.sml Fri Jan 06 08:04:36 2023 +0100
13.3 @@ -128,12 +128,12 @@
13.4 fun from_store' thy id =
13.5 (Store.get (Know_Store.get_mets thy) id id)
13.6 handle ERROR _ =>
13.7 - raise error ("*** ERROR MethodC.from_store thy " ^ strs2str id ^ " not found");
13.8 + raise error ("*** ERROR MethodC.from_store' thy " ^ strs2str id ^ " not found");
13.9 fun from_store ctxt id =
13.10 let
13.11 val pbl = Store.get (get_mets ()) id id
13.12 in adapt_to_type ctxt pbl end
13.13 handle ERROR _ =>
13.14 - raise error ("*** ERROR MethodC.from_store thy " ^ strs2str id ^ " not found");
13.15 + raise error ("*** ERROR MethodC.from_store ctxt " ^ strs2str id ^ " not found");
13.16
13.17 (**)end(**)
14.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Thu Dec 22 17:06:19 2022 +0100
14.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Fri Jan 06 08:04:36 2023 +0100
14.3 @@ -1046,12 +1046,12 @@
14.4 ( *old*)
14.5 val LI.Not_Derivable =
14.6 (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
14.7 - val pp = Ctree.par_pblobj pt p
14.8 - val (errpats, rew_rls, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
14.9 + val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
14.10 + val (errpats, rew_rls, prog) = case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
14.11 {errpats, rew_rls, program = Rule.Prog prog, ...} => (errpats, rew_rls, prog)
14.12 | _ => error "inform: uncovered case of MethodC.from_store ctxt"
14.13 ;
14.14 -(*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)\", \"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\", \"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\", \"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\", \"d_d ?bdv (exp ?u) = exp ?u * d_d ?x ?u\"]]"
14.15 +(*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\"]]"
14.16 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
14.17
14.18 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
14.19 @@ -1069,6 +1069,115 @@
14.20 | _ => error "inform with (positive) Error_Pattern.check_for broken"
14.21
14.22
14.23 +"----------- re-build: fill_from_store without thy-hierarchy -----------------------------------";
14.24 +"----------- re-build: fill_from_store without thy-hierarchy -----------------------------------";
14.25 +"----------- re-build: fill_from_store without thy-hierarchy -----------------------------------";
14.26 +open Error_Pattern
14.27 +val c = []: int list
14.28 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context}
14.29 +[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
14.30 + ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
14.31 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.32 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.33 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.34 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.35 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.36 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.37 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["diff", "differentiate_on_R"]*)
14.38 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))*)
14.39 + val ([1], Frm) = p;
14.40 + val "d_d x (x \<up> 2 + sin (x \<up> 4))" = f2str f;
14.41 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))*)
14.42 + val ([1], Res) = p;
14.43 + val "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" = f2str f
14.44 +
14.45 +val return_of_me = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_pow", "d_d ?bdv (?bdv \<up> ?n) = ?n * ?bdv \<up> (?n - 1)"))*)
14.46 + val ([1], Res) = p
14.47 + val "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" = f2str f;
14.48 + (* "d_d x (x \<up> 2) + cos (x \<up> 4)" .. wrong user input within next step *)
14.49 +(*//------------------ step into find_fill_patterns ----------------------------------------\\*)
14.50 +(* INSTEAD OF STEPPING INTO me WE DO SO FOR Kernel.findFillpatterns cI errpatID =
14.51 + let
14.52 + val ((pt, _), _) = States.get_calc cI
14.53 + val pos = States.get_pos cI 1;
14.54 + val fillpats = Error_Pattern.find_fill_patterns (pt, pos) errpatID
14.55 +*)
14.56 +"~~~~~ fun findFillpatterns , args:"; val (pt, p, errpatID) = (pt, p, "chain-rule-diff-both");
14.57 +"~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), id) = ((pt, p), errpatID);
14.58 +(*old-------\* )
14.59 + val f_curr = Ctree.get_curr_formula (pt, pos);
14.60 + val pp = Ctree.par_pblobj pt p
14.61 + val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
14.62 + {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
14.63 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
14.64 +( *new-------\*)
14.65 + val ctxt = Ctree.get_ctxt pt pos
14.66 + val f_curr = Ctree.get_curr_formula (pt, pos)
14.67 + val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
14.68 + val (errpats, prog) = case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
14.69 + {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
14.70 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
14.71 +(*new-------/*)
14.72 +
14.73 +(*+*)val 1 = length errpats(*ONLY WITH from_store' @{theory (*!!!*)Build_Thydata}*)
14.74 + val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
14.75 + val subst = Subst.for_bdv ctxt prog env
14.76 + val errpatthms = errpats
14.77 + |> filter ((curry op = errpatID) o (#1: Error_Pattern.T -> Error_Pattern.id))
14.78 + |> map (#3: Error_Pattern.T -> thm list)
14.79 + |> flat;
14.80 +
14.81 +(*+*)val 3 = length errpatthms;
14.82 +(*+*)val 5 = length (get_fill_ins @{theory} "diff_sin_chain");
14.83 +
14.84 +(*case*) map (
14.85 + fill_from_store ctxt subst f_curr errpatID) errpatthms |> flat (*of*);
14.86 +"~~~~~ fun fill_from_store , args:"; val (ctxt, subst, form, (*id*)errpat_id, thm) =
14.87 + (ctxt, subst, f_curr, errpatID, hd errpatthms);
14.88 + val thm_id_long = Thm.get_name_hint thm
14.89 +
14.90 +(*+*)val "Diff.diff_sin_chain" = thm_id_long;
14.91 +(*+*)val "diff_sin_chain" = ThmC.cut_id thm_id_long;
14.92 +
14.93 + val thm_id = ThmC.cut_id thm_id_long
14.94 + val fill_ins =
14.95 +
14.96 +Error_Pattern.get_fill_ins (Proof_Context.theory_of ctxt) thm_id;
14.97 +"~~~~~ fun get_fill_ins , args:"; val (thy, thm_id) =
14.98 + ((Proof_Context.theory_of ctxt), thm_id);
14.99 + (*case*) AList.lookup (op =) (get_fill_inss thy) thm_id (*of*);
14.100 +val ERROR "fill_ins for thm \"diff_sin_chain\" missing in theory \"Isac_Knowledge\" (and ancestors)\nTODO exception hierarchy needs to be established." =
14.101 + ERROR ("fill_ins for thm \"" ^ thm_id ^ "\" missing in theory \"" ^
14.102 + (thy |> ThyC.id_of) ^ "\" (and ancestors)" ^
14.103 + "\nTODO exception hierarchy needs to be established.");
14.104 +
14.105 +(*return to fill_from_store..*)
14.106 + val some = map (fill_form ctxt subst (thm, form) errpat_id) fill_ins;
14.107 +val return_fill_from_store = some |> filter is_some |> map the;
14.108 +
14.109 +(* final test ... ----------------------------------------------------------------------------*)
14.110 +(*+*)if length return_fill_from_store = 5 then
14.111 +(*+*) case return_fill_from_store of
14.112 +(*+*) ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm =
14.113 +(*+*) "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
14.114 +(*+*) then () else error "find_fill_patterns changed 2a"
14.115 +(*+*) | _ => error "find_fill_patterns changed 2b"
14.116 +(*+*)else error "find_fill_patterns changed 2c";
14.117 +(*-------------------- stop step into find_fill_patterns -------------------------------------*)
14.118 +(*\\------------------ step into find_fill_patterns ----------------------------------------//*)
14.119 +
14.120 +val (p,_,f,nxt,_,pt) = return_of_me
14.121 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_pow", "d_d ?bdv (?bdv \<up> ?n) = ?n * ?bdv \<up> (?n - 1)"))*)
14.122 + val ([3], Res) = p
14.123 + val "d_d x (x \<up> 2) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))" = f2str f;
14.124 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.125 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Check_Postcond ["derivative_of", "function"]*)
14.126 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.127 + val ([], Res) = p;
14.128 + val "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" = f2str f
14.129 + val End_Proof' = nxt;
14.130 +
14.131 +
14.132 "--------- embed fun find_fill_patterns ---------------------------";
14.133 "--------- embed fun find_fill_patterns ---------------------------";
14.134 "--------- embed fun find_fill_patterns ---------------------------";
14.135 @@ -1081,78 +1190,27 @@
14.136 autoCalculate 1 CompleteCalcHead;
14.137 autoCalculate 1 (Steps 1);
14.138 autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
14.139 -appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (*|> Future.join*);
14.140 +appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)";
14.141 (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
14.142 (*or
14.143 <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
14.144 -
14.145 "~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
14.146 val ((pt, _), _) = States.get_calc cI
14.147 val pos = States.get_pos cI 1;
14.148 -"~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
14.149 - val f_curr = Ctree.get_curr_formula (pt, pos);
14.150 - val pp = Ctree.par_pblobj pt p
14.151 - val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
14.152 - {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
14.153 - | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
14.154 - val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
14.155 - val subst = Subst.for_bdv ctxt prog env
14.156 - val errpatthms = errpats
14.157 - |> filter ((curry op = errpatID) o (#1: Error_Pattern.T -> Error_Pattern.id))
14.158 - |> map (#3: Error_Pattern.T -> thm list)
14.159 - |> flat;
14.160
14.161 -case map (Error_Pattern.fill_from_store ctxt subst f_curr errpatID) errpatthms |> flat of
14.162 - ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if UnparseC.term tm =
14.163 - "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
14.164 - then () else error "find_fill_patterns changed 1a"
14.165 -| _ => error "find_fill_patterns changed 1b"
14.166 +val return_from_find_fill_patterns = find_fill_patterns (pt, pos) errpatID;
14.167 +DEconstrCalcTree 1;
14.168
14.169 -"~~~~~ fun fill_from_store, args:"; val (ctxt, subst, form, errpatID, thm) =
14.170 - (ctxt, subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
14.171 - val thmDeriv = Thm.get_name_hint thm
14.172 - val (part, thyID) = Thy_Read.thy_containing_thm thmDeriv
14.173 - val theID = [part, thyID, "Theorems", ThmC.cut_id thmDeriv]
14.174 - val Thy_Write.Hthm {fillpats, ...} = Thy_Read.from_store ctxt theID
14.175 - val some = map (Error_Pattern.fill_form ctxt subst (thm, form) errpatID) fillpats;
14.176 +(* final test ... ----------------------------------------------------------------------------*)
14.177 +val 6 = length return_from_find_fill_patterns
14.178 +val (fill_in_id, term, thm, subst) :: _ = return_from_find_fill_patterns
14.179
14.180 -case some |> filter is_some |> map the of
14.181 - ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm =
14.182 - "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
14.183 - then () else error "find_fill_patterns changed 2a"
14.184 -| _ => error "find_fill_patterns changed 2b"
14.185 +val "fill-d_d-arg" = fill_in_id
14.186 +val "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" =
14.187 + UnparseC.term_in_ctxt @{context} term
14.188 +val "Diff.diff_sin_chain" = Thm.get_name_hint thm
14.189 +val "[(''bdv'', x)]" = subst |> the |> Subst.string_of_input;
14.190
14.191 -"~~~~~ fun fill_form, args:";
14.192 - val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
14.193 - (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
14.194 -val (form', _, _, rewritten) =
14.195 - rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) form;
14.196 -
14.197 -if UnparseC.term form' = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" then ()
14.198 -else error "find_fill_patterns changed 3";
14.199 -
14.200 -"~~~~~ to findFillpatterns return val:"; val (fillpats) =
14.201 - (map (Error_Pattern.fill_from_store ctxt (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
14.202 -
14.203 -"vvv--- dropped this code WN120730";
14.204 -val msg = "fill patterns " ^
14.205 - ((map ((apsnd UnparseC.term) o quad2pair) fillpats) |> map pair2str_ |> strs2str_);
14.206 -msg =
14.207 - "fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
14.208 - " =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" ^
14.209 - "#fill-both-args#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
14.210 - " =\nd_d x (x \<up> 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^
14.211 - "#fill-d_d#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
14.212 - " =\nd_d x (x \<up> 2) + cos (x \<up> 4) * ?_dummy_1 x (x \<up> 4)" ^
14.213 - "#fill-inner-deriv#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" ^
14.214 - " =\nd_d x (x \<up> 2) + cos (x \<up> 4) * ?_dummy_1" ^
14.215 - "#fill-all#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) = d_d x (x \<up> 2) + ?_dummy_1#";
14.216 -" \<up> --- dropped this code WN120730";
14.217 -
14.218 -if (map #1 fillpats) =
14.219 - ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
14.220 -then () else error "find_fill_patterns changed 4b";
14.221 -DEconstrCalcTree 1;
14.222
14.223 "--------- build fun is_exactly_equal, inputFillFormula ----------";
14.224 "--------- build fun is_exactly_equal, inputFillFormula ----------";
15.1 --- a/test/Tools/isac/Test_Some.thy Thu Dec 22 17:06:19 2022 +0100
15.2 +++ b/test/Tools/isac/Test_Some.thy Fri Jan 06 08:04:36 2023 +0100
15.3 @@ -120,13 +120,1587 @@
15.4 \<close> ML \<open>
15.5 \<close>
15.6
15.7 -section \<open>===================================================================================\<close>
15.8 +section \<open>========== "Specify/step-specify.sml" REQUIRED TO RUN TESTS BELOW ..==============\<close>
15.9 ML \<open>
15.10 \<close> ML \<open>
15.11 +(* Title: "Specify/step-specify.sml"
15.12 + Author: Walther Neuper
15.13 + (c) due to copyright terms
15.14 +*)
15.15 +
15.16 +"-----------------------------------------------------------------------------------------------";
15.17 +"table of contents -----------------------------------------------------------------------------";
15.18 +"-----------------------------------------------------------------------------------------------";
15.19 +"-----------------------------------------------------------------------------------------------";
15.20 +"----------- re-build: Step_Specify.do_next ---------------------------------------------------";
15.21 +"-----------------------------------------------------------------------------------------------";
15.22 +"-----------------------------------------------------------------------------------------------";
15.23 +"-----------------------------------------------------------------------------------------------";
15.24 +
15.25 +open Step_Specify;
15.26 +"----------- re-build: Step_Specify.do_next ---------------------------------------------------";
15.27 +"----------- re-build: Step_Specify.do_next ---------------------------------------------------";
15.28 +"----------- re-build: Step_Specify.do_next ---------------------------------------------------";
15.29 +States.reset ();
15.30 +CalcTree @{context} (*ATTENTION: encode_fmz ... unlike Test_Code.init_calc @{context}*)
15.31 + [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
15.32 + ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
15.33 +Iterator 1;
15.34 +moveActiveRoot 1;
15.35 +autoCalculate 1 (Steps 1);
15.36 +
15.37 +val (ptp as (pt, p), _) = States.get_calc 1;
15.38 +pt;(*isa==REP*)
15.39 +val (_, ("Integrate", ["integrate", "function"], ["diff", "integration"]), _)
15.40 + = get_obj g_origin pt (fst p);
15.41 +get_obj g_spec pt (fst p) = References.empty; (*isa==REP*)
15.42 +
15.43 +(*this steps into according to "----- step 2 ---" below*)
15.44 +"~~~~~ fun autoCalculate , args:"; val (cI, auto) = (1, (Steps 1));
15.45 + val pold = States.get_pos cI 1
15.46 +;
15.47 + (*case*) Math_Engine.autocalc [] pold (States.get_calc cI) auto (*of*);
15.48 +"~~~~~ fun autocalc , args:"; val (c: pos' list, ip, cs, (Solve.Steps s)) = ([], pold, (States.get_calc cI), auto);
15.49 +val c''''' = c; (*for from fun nxt_specify_\<longrightarrow>fun Step.do_next\<longrightarrow>fun autocalc, return*)
15.50 +
15.51 + (*if*) s <= 1 (*then*);
15.52 + (**)val ("ok", (([(Specify_Theory "Integrate", _, _)]), c', ptp)) =(**)
15.53 +Step.do_next ip cs;
15.54 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (ip, cs);
15.55 + val pIopt = Ctree.get_pblID (pt, ip);
15.56 + (*if*) ip = ([], Pos.Res) (*else*);
15.57 + val [] = (*case*) tacis (*of*);
15.58 + val SOME _ = (*case*) pIopt (*of*);
15.59 + (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*then*);
15.60 +
15.61 + val ("ok", ([(Specify_Theory "Integrate", _, _)], _, _)) =
15.62 + Step.specify_do_next (pt, ip);
15.63 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, ip);
15.64 + val (_, (p_', tac)) = Specify.find_next_step ptp
15.65 + val ist_ctxt = Ctree.get_loc pt (p, p_)
15.66 + val _ = (*case*) tac (*of*);
15.67 + ("ok", Step_Specify.by_tactic_input tac (pt, (p, p_'))) (*return from specify_do_next*);
15.68 +
15.69 +"~~~~~ from fun nxt_specify_\<longrightarrow>fun Step.do_next\<longrightarrow>fun autocalc, return:"; val (str, (_, c', ptp))
15.70 + = Step_Specify.by_tactic_input tac ptp;
15.71 +
15.72 + (str, c''''' @ c', ptp) (*return from autocalc*);
15.73 +
15.74 +"----- step 2 ---";(*isa<>REP*)
15.75 +autoCalculate 1 (Steps 1);
15.76 +
15.77 +val (ptp as (pt, p), _) = States.get_calc 1;
15.78 +pt;(*REP
15.79 +val it =
15.80 + Nd (PblObj
15.81 +:
15.82 + result = (Const ("empty", "??.'a"), []), spec =
15.83 + ("Integrate", ["integrate", "function"], MethodC.id_empty)},
15.84 + []):
15.85 + ctree*)
15.86 +
15.87 +"----- step 3 ---";
15.88 +autoCalculate 1 (Steps 1);
15.89 +val (ptp as (pt, p), _) = States.get_calc 1;
15.90 +
15.91 +"----- step 4 ---";
15.92 +autoCalculate 1 (Steps 1);
15.93 +"----- step 5 ---";
15.94 +autoCalculate 1 (Steps 1);
15.95 +"----- step 6 ---";
15.96 +autoCalculate 1 (Steps 1);
15.97 +"----- step 7 ---";
15.98 +autoCalculate 1 (Steps 1);
15.99 +"----- step 8 ---";
15.100 +autoCalculate 1 (Steps 1);
15.101 +
15.102 +val (ptp as (_, p), _) = States.get_calc 1;
15.103 +
15.104 +val (Form t,_,_) = ME_Misc.pt_extract ctxt ptp;
15.105 +
15.106 +if UnparseC.term t = "c + x + 1 / 3 * x \<up> 3" andalso p = ([], Res) then ()
15.107 +else error "mathengine.sml -- fun autoCalculate -- end";
15.108 \<close> ML \<open>
15.109 \<close> ML \<open>
15.110 \<close>
15.111
15.112 +section \<open>========== "Interpret/error-pattern.sml" REQUIRED TO RUN TESTS BELOW ..============\<close>
15.113 +ML \<open>
15.114 +\<close> ML \<open>
15.115 +(* Title: "Interpret/error-pattern.sml"
15.116 + Author: Walther Neuper 060225,
15.117 + (c) due to copyright terms
15.118 +
15.119 +Strange ERROR "Undefined fact: "all_left""
15.120 +*)
15.121 +
15.122 +"-----------------------------------------------------------------";
15.123 +"table of contents -----------------------------------------------";
15.124 +"-----------------------------------------------------------------";
15.125 +"appendForm with miniscript with mini-subpbl:";
15.126 +"--------- appendFormula: on Res + equ_nrls ----------------------";
15.127 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
15.128 +"--------- appendFormula: on Res + NO deriv ----------------------";
15.129 +"--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
15.130 +"replaceForm with miniscript with mini-subpbl:";
15.131 +"--------- replaceFormula: on Res + = ----------------------------";
15.132 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
15.133 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
15.134 +"--------- replaceFormula: cut calculation -----------------------";
15.135 +"--------- replaceFormula: cut calculation -----------------------";
15.136 +(* 040307 copied from informtest.sml ... old versions
15.137 +"--------- maximum-example, UC: Modeling / modifyCalcHead --------";*)
15.138 +"--------- syntax error ------------------------------------------";
15.139 +"CAS-command:";
15.140 +(*"--------- CAS-command on ([],Pbl) -------------------------------";*)
15.141 +(*"--------- CAS-command on ([],Pbl) FE-interface ------------------";*)
15.142 +"--------- locate_input_term [rational,simplification] ----------------------";
15.143 +(*"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";*)
15.144 +"--------- Take as 1st tac, start from exp -----------------------";
15.145 +(*"--------- implicit_take, start with <NEW> (CAS input) ---------------";*)
15.146 +"--------- build fun check_for' ------------------------------";
15.147 +"--------- build fun check_for' ?bdv -------------------------";
15.148 +"--------- build fun check_for ------------------------";
15.149 +"--------- embed fun check_for ------------------------";
15.150 +"--------- embed fun find_fill_patterns ---------------------------";
15.151 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
15.152 +"--------- fun appl_adds -----------------------------------------";
15.153 +"--------- fun concat_deriv --------------------------------------";
15.154 +"--------- handle an input formula -------------------------------";
15.155 +"--------- fun dropwhile' ----------------------------------------";
15.156 +"-----------------------------------------------------------------";
15.157 +"-----------------------------------------------------------------";
15.158 +"-----------------------------------------------------------------";
15.159 +
15.160 +
15.161 +"--------- appendFormula: on Res + equ_nrls ----------------------";
15.162 +"--------- appendFormula: on Res + equ_nrls ----------------------";
15.163 +"--------- appendFormula: on Res + equ_nrls ----------------------";
15.164 + val Prog sc = (#program o MethodC.from_store ctxt) ["Test", "squ-equ-test-subpbl1"];
15.165 + (writeln o UnparseC.term) sc;
15.166 + val Prog sc = (#program o MethodC.from_store ctxt) ["Test", "solve_linear"];
15.167 + (writeln o UnparseC.term) sc;
15.168 +
15.169 + States.reset ();
15.170 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
15.171 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
15.172 + ["Test", "squ-equ-test-subpbl1"]))];
15.173 + Iterator 1; moveActiveRoot 1;
15.174 + autoCalculate 1 CompleteCalcHead;
15.175 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
15.176 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
15.177 +
15.178 + appendFormula 1 "- 2 * 1 + (1 + x) = 0" (*|> Future.join*); refFormula 1 (States.get_pos 1 1);
15.179 + val ((pt,_),_) = States.get_calc 1;
15.180 + val str = pr_ctree ctxt pr_short pt;
15.181 +if str =
15.182 +(". ----- pblobj -----\n" ^
15.183 +"1. x + 1 = 2\n" ^
15.184 +"2. x + 1 + - 1 * 2 = 0\n" ^
15.185 +"2.1. x + 1 + - 1 * 2 = 0\n" ^
15.186 +"2.2. 1 + x + - 1 * 2 = 0\n" ^
15.187 +"2.3. 1 + (x + - 1 * 2) = 0\n" ^
15.188 +"2.4. 1 + (x + - 2) = 0\n" ^
15.189 +"2.5. 1 + (x + - 2 * 1) = 0\n" ^
15.190 +"2.6. 1 + x + - 2 * 1 = 0\n" ) then ()
15.191 +else error "inform.sml: diff.behav.appendFormula: on Res + equ 1";
15.192 +
15.193 + moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
15.194 + moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + - 1 * 2 = 0*)
15.195 +
15.196 + (*the seven steps of detailed derivation*)
15.197 + moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm);
15.198 + moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res);
15.199 + moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res);
15.200 + moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res);
15.201 + moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
15.202 + moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
15.203 + moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
15.204 + val ((pt,_),_) = States.get_calc 1;
15.205 + if "- 2 * 1 + (1 + x) = 0" = UnparseC.term (fst (get_obj g_result pt [2,6])) then()
15.206 + else error "inform.sml: diff.behav.appendFormula: on Res + equ 2";
15.207 +
15.208 + fetchProposedTactic 1; (*takes Iterator 1 _1_*)
15.209 +(* <ERROR> error in kernel </ERROR> ALREADY IN 2009-2*)
15.210 +(*========== inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 =============
15.211 + val (_,(tac,_,_)::_) = States.get_calc 1;
15.212 + if tac = Rewrite_Set "Test_simplify" then ()
15.213 + else error "inform.sml: diff.behav.appendFormula: on Res + equ 3";
15.214 +============ inhibit exn WN1130701 broken at Isabelle2002 --> 2009-2 ============*)
15.215 +
15.216 + autoCalculate 1 CompleteCalc;
15.217 + val ((pt,_),_) = States.get_calc 1;
15.218 + if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
15.219 + else error "inform.sml: diff.behav.appendFormula: on Res + equ 4";
15.220 + (* autoCalculate 1 CompleteCalc;
15.221 + val ((pt,p),_) = States.get_calc 1;
15.222 + (writeln o istates2str) (get_obj g_loc pt [ ]);
15.223 + (writeln o istates2str) (get_obj g_loc pt [1]);
15.224 + (writeln o istates2str) (get_obj g_loc pt [2]);
15.225 + (writeln o istates2str) (get_obj g_loc pt [3]);
15.226 + (writeln o istates2str) (get_obj g_loc pt [3,1]);
15.227 + (writeln o istates2str) (get_obj g_loc pt [3,2]);
15.228 + (writeln o istates2str) (get_obj g_loc pt [4]);
15.229 +
15.230 + *)
15.231 +"----------------------------------------------------------";
15.232 +
15.233 + val fod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls
15.234 + ((#rules o Rule_Set.rep) Test_simplify)
15.235 + (sqrt_right false) NONE
15.236 + (TermC.parse_test @{context} "x + 1 + - 1 * 2 = 0");
15.237 + (writeln o (Derive.trtas2str ctxt)) fod;
15.238 +
15.239 + val ifod = Derive.do_one (Proof_Context.init_global @{theory "Isac_Knowledge"}) Atools_erls
15.240 + ((#rules o Rule_Set.rep) Test_simplify)
15.241 + (sqrt_right false) NONE
15.242 + (TermC.parse_test @{context} "- 2 * 1 + (1 + x) = 0");
15.243 + (writeln o (Derive.trtas2str ctxt)) ifod;
15.244 + fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1 = t2;
15.245 + val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
15.246 + val der = fod' @ (map (Derive.rev_deriv' ctxt) rifod');
15.247 + (writeln o (Derive.trtas2str ctxt)) der;
15.248 + "----------------------------------------------------------";
15.249 +DEconstrCalcTree 1;
15.250 +
15.251 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
15.252 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
15.253 +"--------- appendFormula: on Frm + equ_nrls ----------------------";
15.254 + States.reset ();
15.255 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
15.256 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
15.257 + ["Test", "squ-equ-test-subpbl1"]))];
15.258 + Iterator 1; moveActiveRoot 1;
15.259 + autoCalculate 1 CompleteCalcHead;
15.260 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1) (*x + 1 = 2*);
15.261 + appendFormula 1 "2+ - 1 + x = 2" (*|> Future.join*); refFormula 1 (States.get_pos 1 1);
15.262 +
15.263 + moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
15.264 +
15.265 + moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm);
15.266 + moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res);
15.267 + moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res);
15.268 + moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res);
15.269 + moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
15.270 + moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
15.271 + moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
15.272 + val ((pt,_),_) = States.get_calc 1;
15.273 + if "2 + - 1 + x = 2" = UnparseC.term (fst (get_obj g_result pt [1,6])) then()
15.274 + else error "inform.sml: diff.behav.appendFormula: on Frm + equ 1";
15.275 +
15.276 + fetchProposedTactic 1; (*takes Iterator 1 _1_*)
15.277 + val (_,(tac,_,_)::_) = States.get_calc 1;
15.278 + case tac of Rewrite_Set "norm_equation" => ()
15.279 + | _ => error "inform.sml: diff.behav.appendFormula: on Frm + equ 2";
15.280 + autoCalculate 1 CompleteCalc;
15.281 + val ((pt,_),_) = States.get_calc 1;
15.282 + if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
15.283 + else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
15.284 +DEconstrCalcTree 1;
15.285 +
15.286 +"--------- appendFormula: on Res + NO deriv ----------------------";
15.287 +"--------- appendFormula: on Res + NO deriv ----------------------";
15.288 +"--------- appendFormula: on Res + NO deriv ----------------------";
15.289 + States.reset ();
15.290 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
15.291 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
15.292 + ["Test", "squ-equ-test-subpbl1"]))];
15.293 + Iterator 1; moveActiveRoot 1;
15.294 + autoCalculate 1 CompleteCalcHead;
15.295 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
15.296 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
15.297 +
15.298 + appendFormula 1 "x = 2" (*|> Future.join*);
15.299 + val ((pt,p),_) = States.get_calc 1;
15.300 + val str = pr_ctree ctxt pr_short pt;
15.301 + writeln str;
15.302 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
15.303 + then ()
15.304 + else error "inform.sml: diff.behav.appendFormula: Res + NOder 1";
15.305 +
15.306 + fetchProposedTactic 1;
15.307 + val (_,(tac,_,_)::_) = States.get_calc 1;
15.308 + case tac of Rewrite_Set "Test_simplify" => ()
15.309 + | _ => error "inform.sml: diff.behav.appendFormula: Res + NOder 2";
15.310 + autoCalculate 1 CompleteCalc;
15.311 + val ((pt,_),_) = States.get_calc 1;
15.312 + if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
15.313 + else error "inform.sml: diff.behav.appendFormula: on Frm + equ 3";
15.314 +DEconstrCalcTree 1;
15.315 +
15.316 +"--------- appendFormula: on Res + late deriv --------------------";
15.317 +"--------- appendFormula: on Res + late deriv --------------------";
15.318 +"--------- appendFormula: on Res + late deriv --------------------";
15.319 +(*cp with "fun me" to test/../lucas-interpreter.sml:
15.320 + re-build: fun locate_input_term ---------------------------------------------------";
15.321 +*)
15.322 + States.reset ();
15.323 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
15.324 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
15.325 + ["Test", "squ-equ-test-subpbl1"]))];
15.326 + Iterator 1; moveActiveRoot 1;
15.327 + autoCalculate 1 CompleteCalcHead;
15.328 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
15.329 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
15.330 +
15.331 + appendFormula 1 "x = 1" (*|> Future.join*);
15.332 + val ((pt,p),_) = States.get_calc 1;
15.333 + val str = pr_ctree ctxt pr_short pt;
15.334 + writeln str;
15.335 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n3.2.1. x = 0 + - 1 * - 1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
15.336 + then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
15.337 + else error "inform.sml: diff.behav.appendFormula: Res + late d 1";
15.338 +
15.339 + fetchProposedTactic 1;
15.340 + val (_,(tac,_,_)::_) = States.get_calc 1;
15.341 + case tac of Check_Postcond ["LINEAR", "univariate", "equation", "test"] => ()
15.342 + | _ => error "inform.sml: diff.behav.appendFormula: Res + late d 2";
15.343 + autoCalculate 1 CompleteCalc;
15.344 + val ((pt,_),_) = States.get_calc 1;
15.345 + if "[x = 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
15.346 + else error "inform.sml: diff.behav.appendFormula: Res + late d 3";
15.347 +DEconstrCalcTree 1;
15.348 +
15.349 +"--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
15.350 +"--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
15.351 +"--------- appendFormula: on Res + late deriv [x = 3 + - 2]---///--";
15.352 + States.reset ();
15.353 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
15.354 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
15.355 + ["Test", "squ-equ-test-subpbl1"]))];
15.356 + Iterator 1; moveActiveRoot 1;
15.357 + autoCalculate 1 CompleteCalcHead;
15.358 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
15.359 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
15.360 + appendFormula 1 "[x = 3 + -2*1]" (*|> Future.join*);
15.361 + val ((pt,p),_) = States.get_calc 1;
15.362 + val str = pr_ctree ctxt pr_short pt;
15.363 + writeln str;
15.364 + if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + - 1 * 2 = 0\n3. ----- pblobj -----\n3.1. - 1 + x = 0\n3.2. x = 0 + - 1 * - 1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = - 2 + 3]\n4.3. [x = 3 + - 2]\n" then ()
15.365 + else error "inform.sml: diff.behav.appendFormula: Res + latEE 1";
15.366 + autoCalculate 1 CompleteCalc;
15.367 + val ((pt,p),_) = States.get_calc 1;
15.368 + if "[x = 3 + - 2 * 1]" = UnparseC.term (fst (get_obj g_result pt [])) then ()
15.369 + (* ~~~~~~~~~~ simplify as last step in any script ?!*)
15.370 + else error "inform.sml: diff.behav.appendFormula: Res + latEE 2";
15.371 +DEconstrCalcTree 1;
15.372 +
15.373 +"--------- replaceFormula: on Res + = ----------------------------";
15.374 +"--------- replaceFormula: on Res + = ----------------------------";
15.375 +"--------- replaceFormula: on Res + = ----------------------------";
15.376 + States.reset ();
15.377 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
15.378 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
15.379 + ["Test", "squ-equ-test-subpbl1"]))];
15.380 + Iterator 1; moveActiveRoot 1;
15.381 + autoCalculate 1 CompleteCalcHead;
15.382 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
15.383 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
15.384 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*- 1 + x*);
15.385 +
15.386 + replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (States.get_pos 1 1);
15.387 + val ((pt,_),_) = States.get_calc 1;
15.388 + val str = pr_ctree ctxt pr_short pt;
15.389 +
15.390 +(* before AK110725 this was
15.391 +". ----- pblobj -----\n
15.392 +1. x + 1 = 2\n
15.393 +2. x + 1 + - 1 * 2 = 0\n
15.394 +2.1. x + 1 + - 1 * 2 = 0\n
15.395 +2.2. 1 + x + - 1 * 2 = 0\n
15.396 +2.3. 1 + (x + - 1 * 2) = 0\n
15.397 +2.4. 1 + (x + -2) = 0\n
15.398 +2.5. 1 + (x + -2 * 1) = 0\n
15.399 +2.6. 1 + x + -2 * 1 = 0\n";
15.400 +*)
15.401 +if str =
15.402 +". ----- pblobj -----\n"^
15.403 +"1. x + 1 = 2\n"^
15.404 +"2. x + 1 + - 1 * 2 = 0\n"^
15.405 +"2.1. x + 1 + - 1 * 2 = 0\n"^
15.406 +"2.2. 1 + x + - 1 * 2 = 0\n"^
15.407 +"2.3. 1 + (x + - 1 * 2) = 0\n"^
15.408 +"2.4. 1 + (x + - 2) = 0\n"^
15.409 +"2.5. 1 + (x + - 2 * 1) = 0\n"^
15.410 +"2.6. 1 + x + - 2 * 1 = 0\n" then()
15.411 +else error "inform.sml: diff.behav.replaceFormula: on Res += 1";
15.412 +
15.413 + autoCalculate 1 CompleteCalc;
15.414 + val ((pt,pos as (p,_)),_) = States.get_calc 1;
15.415 + if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst) (get_obj g_result pt p) then()
15.416 + else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
15.417 +DEconstrCalcTree 1;
15.418 +
15.419 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
15.420 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
15.421 +"--------- replaceFormula: on Res + = 1st Nd ---------------------";
15.422 + States.reset ();
15.423 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
15.424 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
15.425 + ["Test", "squ-equ-test-subpbl1"]))];
15.426 + Iterator 1; moveActiveRoot 1;
15.427 + autoCalculate 1 CompleteCalcHead;
15.428 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
15.429 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
15.430 +
15.431 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
15.432 + val ((pt,_),_) = States.get_calc 1;
15.433 + val str = pr_ctree ctxt pr_short pt;
15.434 + writeln str;
15.435 + if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then ()
15.436 + else error "inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
15.437 + autoCalculate 1 CompleteCalc;
15.438 + val ((pt,pos as (p,_)),_) = States.get_calc 1;
15.439 + if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
15.440 + else error "inform.sml: diff.behav.replaceFormula: on Res + = 2";
15.441 +DEconstrCalcTree 1;
15.442 +
15.443 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
15.444 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
15.445 +"--------- replaceFormula: on Frm + = 1st Nd ---------------------";
15.446 + States.reset ();
15.447 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
15.448 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
15.449 + ["Test", "squ-equ-test-subpbl1"]))];
15.450 + Iterator 1; moveActiveRoot 1;
15.451 + autoCalculate 1 CompleteCalcHead;
15.452 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
15.453 +
15.454 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
15.455 + val ((pt,_),_) = States.get_calc 1;
15.456 + val str = pr_ctree ctxt pr_short pt;
15.457 + writeln str;
15.458 + if str= ". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = - 2 + 4\n1.4. x + 1 = - 2 + 4\n" then ()
15.459 + else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
15.460 + autoCalculate 1 CompleteCalc;
15.461 + val ((pt,pos as (p,_)),_) = States.get_calc 1;
15.462 + if pos = ([],Res) andalso "[x = 1]" = (UnparseC.term o fst)(get_obj g_result pt p) then()
15.463 + else error "inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
15.464 +DEconstrCalcTree 1;
15.465 +
15.466 +"--------- replaceFormula: cut calculation -----------------------";
15.467 +"--------- replaceFormula: cut calculation -----------------------";
15.468 +"--------- replaceFormula: cut calculation -----------------------";
15.469 + States.reset ();
15.470 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
15.471 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
15.472 + ["Test", "squ-equ-test-subpbl1"]))];
15.473 + Iterator 1; moveActiveRoot 1;
15.474 + autoCalculate 1 CompleteCalc;
15.475 + moveActiveRoot 1; moveActiveDown 1;
15.476 + if States.get_pos 1 1 = ([1], Frm) then ()
15.477 + else error "inform.sml: diff.behav. cut calculation 1";
15.478 +
15.479 + replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (States.get_pos 1 1);
15.480 + val ((pt,p),_) = States.get_calc 1;
15.481 + val str = pr_ctree ctxt pr_short pt;
15.482 + writeln str;
15.483 + if p = ([1], Res) then ()
15.484 + else error "inform.sml: diff.behav. cut calculation 2";
15.485 +
15.486 +
15.487 +(* 040307 copied from informtest.sml; ... old version
15.488 + "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
15.489 + "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
15.490 + "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
15.491 +
15.492 + val p = ([],Pbl);
15.493 + val elems = ["fixedValues [r=Arbfix]", "maximum A", "valuesFor [a,b]",
15.494 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
15.495 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
15.496 + "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
15.497 + (* \<up> these are the elements for the root-problem (in variants)*)
15.498 + (*vvv these are elements required for subproblems*)
15.499 + "boundVariable a", "boundVariable b", "boundVariable alpha",
15.500 + "interval {x::real. 0 <= x & x <= 2*r}",
15.501 + "interval {x::real. 0 <= x & x <= 2*r}",
15.502 + "interval {x::real. 0 <= x & x <= pi}",
15.503 + "errorBound (eps=(0::real))"]
15.504 + (*specifying is not interesting for this example*)
15.505 + val spec = ("Diff_App", ["maximum_of", "function"],
15.506 + ["Diff_App", "max_by_calculus"]);
15.507 + (*the empty model with descriptions for user-guidance by Model_Problem*)
15.508 + val empty_model = [Given ["fixedValues []"],
15.509 + Find ["maximum", "valuesFor"],
15.510 + Relate ["relations []"]];
15.511 +
15.512 +
15.513 + (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
15.514 + val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(elems, spec)];
15.515 + (*val nxt = ("Model_Problem", ...*)
15.516 + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
15.517 +
15.518 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.519 + (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
15.520 + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
15.521 +(*[
15.522 +(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
15.523 +(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
15.524 +(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
15.525 +(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
15.526 +
15.527 + (*the empty CalcHead is checked w.r.t the model and re-established as such*)
15.528 + val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, References.empty);
15.529 + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
15.530 + if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then () else error "informtest.sml: diff.behav. max 1";
15.531 +
15.532 + (*there is one input to the model (could be more)*)
15.533 + val (b,pt,ocalhd) =
15.534 + input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
15.535 + Find ["maximum", "valuesFor"],
15.536 + Relate ["relations"]], Pbl, References.empty);
15.537 + val pbl = get_obj g_pbl pt (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
15.538 + if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"ThyC.id_empty\", [\"e_pblID\"], [\"e_metID\"]) )" then ()
15.539 + else error "informtest.sml: diff.behav. max 2";
15.540 +
15.541 + (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
15.542 + val (b,pt''''',ocalhd) =
15.543 + input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
15.544 + Find ["maximum A", "valuesFor [a,b]"],
15.545 + Relate ["relations [A=a*b, a/2=r*sin alpha, \
15.546 + \b/2=r*cos alpha]"]], Pbl, References.empty);
15.547 + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
15.548 + if ocalhd2str ocalhd = ------------ \<up> \<up> \<up> ^ missing !!!*)
15.549 +
15.550 + (*this input is complete in variant 1 (variant 3 does not work yet)*)
15.551 + val (b,pt''''',ocalhd) =
15.552 + input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
15.553 + Find ["maximum A", "valuesFor [a,b]"],
15.554 + Relate ["relations [A=a*b, \
15.555 + \(a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]"]],
15.556 + Pbl, References.empty);
15.557 + val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (I_Model.to_string ctxt)) pbl;
15.558 +
15.559 + modifycalcheadOK2xml 111 (bool2str b) ocalhd;
15.560 +*)
15.561 +DEconstrCalcTree 1;
15.562 +
15.563 +"--------- syntax error ------------------------------------------";
15.564 +"--------- syntax error ------------------------------------------";
15.565 +"--------- syntax error ------------------------------------------";
15.566 + States.reset ();
15.567 + CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
15.568 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
15.569 + ["Test", "squ-equ-test-subpbl1"]))];
15.570 + Iterator 1; moveActiveRoot 1;
15.571 + autoCalculate 1 CompleteCalcHead;
15.572 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 = 2*)
15.573 + autoCalculate 1 (Steps 1); refFormula 1 (States.get_pos 1 1);(*x + 1 + - 1 * 2 = 0*);
15.574 +
15.575 + appendFormula 1 " x - "; (*<ERROR> syntax error in ' x - ' </ERROR>*)
15.576 + val ((pt,_),_) = States.get_calc 1;
15.577 + val str = pr_ctree ctxt pr_short pt;
15.578 + writeln str;
15.579 + if str = ". ----- pblobj -----\n1. x + 1 = 2\n" then ()
15.580 + else error "inform.sml: diff.behav.appendFormula: syntax error";
15.581 +DEconstrCalcTree 1;
15.582 +
15.583 +(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd)
15.584 +"--------- CAS-command on ([],Pbl) -------------------------------";
15.585 +"--------- CAS-command on ([],Pbl) -------------------------------";
15.586 +"--------- CAS-command on ([],Pbl) -------------------------------";
15.587 +val (p,_,f,nxt,_,pt) =
15.588 + Test_Code.init_calc @{context} [([], References.empty)];
15.589 +val ifo = "solve(x+1=2,x)";
15.590 +val (_,(_,c,(pt,p))) = Step_Solve.by_term (pt,p) "solve(x+1=2,x)";
15.591 +( *
15.592 + This trick \<up> \<up> \<up> micked input of \<up> \<up> \<up> \<up> \<up> ^^ in the front-end.
15.593 + The trick worked in changeset fbaff8cf0179, it does not work in 59c5dd27d589 anymore
15.594 + (TODO hg bisect ?) and raises the ERROR Undefined fact: "xfoldr_Nil".
15.595 +
15.596 + Compare tests "CAS-command" in test/../inssort.sml etc.
15.597 + ---------------------------------------------------------------------------------------------
15.598 +Test_Tool.show_pt pt;
15.599 +val nxt = (Apply_Method ["Test", "squ-equ-test-subpbl1"]);
15.600 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.601 +if p = ([1], Frm) andalso f2str f = "x + 1 = 2" then ()
15.602 +else error "inform.sml: diff.behav. CAScmd ([],Pbl)";
15.603 +DEconstrCalcTree 1;
15.604 +-----------------------------------------------------------------------------------------------*)
15.605 +
15.606 +(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd)
15.607 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
15.608 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
15.609 +"--------- CAS-command on ([],Pbl) FE-interface ------------------";
15.610 +States.reset ();
15.611 +CalcTree @{context} [([], References.empty)];
15.612 +Iterator 1;
15.613 +moveActiveRoot 1;
15.614 +replaceFormula 1 "solve(x+1=2,x)";
15.615 +autoCalculate 1 CompleteCalc;
15.616 +val ((pt,p),_) = States.get_calc 1;
15.617 +Test_Tool.show_pt pt;
15.618 +if p = ([], Res) then ()
15.619 +else error "inform.sml: diff.behav. CAScmd ([],Pbl) FE-interface";
15.620 +DEconstrCalcTree 1;
15.621 +-----------------------------------------------------------------------------------------------*)
15.622 +
15.623 +"--------- inform [rational,simplification] ----------------------";
15.624 +"--------- inform [rational,simplification] ----------------------";
15.625 +"--------- inform [rational,simplification] ----------------------";
15.626 +States.reset ();
15.627 +CalcTree @{context} [(["Term (a * x / (b * x) + c * x / (d * x) + e / f)", "normalform N"],
15.628 + ("Rational", ["rational", "simplification"], ["simplification", "of_rationals"]))];
15.629 +Iterator 1; moveActiveRoot 1;
15.630 +autoCalculate 1 CompleteCalcHead;
15.631 +
15.632 +"--- (- 1) give a preview on the calculation without any input";
15.633 +(*
15.634 +autoCalculate 1 CompleteCalc;
15.635 +val ((pt, p), _) = States.get_calc 1;
15.636 +Test_Tool.show_pt pt;
15.637 +[
15.638 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
15.639 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
15.640 +(([1], Res), a / b + c / d + e / f), <--- (1) input arbitrary
15.641 +(([2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.642 +(([3], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
15.643 +(([4], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)), <--- (2) input next
15.644 +(([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))] <--- (3) is also final result
15.645 + EXAMPLE NOT OPTIMAL
15.646 +*)
15.647 +"--- (0) user input as the *first* step does not work, thus impdo at least 1 step";
15.648 +autoCalculate 1 (Steps 1);
15.649 +autoCalculate 1 (Steps 1);
15.650 +val ((pt, p), _) = States.get_calc 1;
15.651 +(*Test_Tool.show_pt pt;
15.652 +[
15.653 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
15.654 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
15.655 +(([1], Res), a / b + c / d + e / f)]
15.656 +*)
15.657 +"--- (1) input an arbitrary next formula";
15.658 +appendFormula 1 "((a * d) + (c * b)) / (b * d) + e / f" (*|> Future.join*);
15.659 +val ((pt, p), _) = States.get_calc 1;
15.660 +(*Test_Tool.show_pt pt;
15.661 +[
15.662 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
15.663 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
15.664 +(([1], Res), a / b + c / d + e / f),
15.665 +(([2,1], Frm), a / b + c / d + e / f),
15.666 +(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.667 +(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
15.668 +(([2], Res), (a * d + c * b) / (b * d) + e / f)]
15.669 +*)
15.670 +val ((pt,p),_) = States.get_calc 1;
15.671 +if p = ([2], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
15.672 +else error ("inform.sml: [rational,simplification] 1");
15.673 +
15.674 +"--- (2) input the next formula that would be presented by mat-engine";
15.675 +(* generate a preview:
15.676 +autoCalculate 1 (Steps 1);
15.677 +val ((pt, p), _) = States.get_calc 1;
15.678 +Test_Tool.show_pt pt;
15.679 +[
15.680 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
15.681 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
15.682 +(([1], Res), a / b + c / d + e / f),
15.683 +(([2,1], Frm), a / b + c / d + e / f),
15.684 +(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.685 +(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
15.686 +(([2], Res), (a * d + c * b) / (b * d) + e / f),
15.687 +(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))] <--- input this
15.688 +*)
15.689 +appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
15.690 +val ((pt, p), _) = States.get_calc 1;
15.691 +(*Test_Tool.show_pt pt;
15.692 +[
15.693 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
15.694 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
15.695 +(([1], Res), a / b + c / d + e / f),
15.696 +(([2,1], Frm), a / b + c / d + e / f),
15.697 +(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.698 +(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
15.699 +(([2], Res), (a * d + c * b) / (b * d) + e / f),
15.700 +(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))]
15.701 +*)
15.702 +if p = ([3], Res) andalso (length o children o (get_nd pt)) (fst p) = 0 then ()
15.703 +else error ("inform.sml: [rational,simplification] 2");
15.704 +
15.705 +"--- (3) input the exact final result";
15.706 +appendFormula 1 "(b * d * e + b * c * f + a * d * f) / (b * d * f)" (*|> Future.join*);
15.707 +val ((pt, p), _) = States.get_calc 1;
15.708 +(*Test_Tool.show_pt pt;
15.709 +[
15.710 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
15.711 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
15.712 +(([1], Res), a / b + c / d + e / f),
15.713 +(([2,1], Frm), a / b + c / d + e / f),
15.714 +(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.715 +(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
15.716 +(([2], Res), (a * d + c * b) / (b * d) + e / f),
15.717 +(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.718 +(([4,1], Frm), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.719 +(([4,1], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
15.720 +(([4,2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.721 +(([4], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f))]
15.722 +*)
15.723 +if p = ([4], Res) andalso (length o children o (get_nd pt)) (fst p) = 2 then ()
15.724 +else error ("inform.sml: [rational,simplification] 3");
15.725 +
15.726 +"--- (4) finish the calculation + check the postcondition (in the future)";
15.727 +autoCalculate 1 CompleteCalc;
15.728 +val ((pt, p), _) = States.get_calc 1;
15.729 +val (t, asm) = get_obj g_result pt [];
15.730 +if UnparseC.term t = "(a * d * f + b * c * f + b * d * e) / (b * d * f)" andalso
15.731 +UnparseC.terms asm =(*"[\"b * d * f \<noteq> 0\",\"d \<noteq> 0\",\"b \<noteq> 0\",\"a * x / (b * x) + c * x / (d * x) + e / f is_ratpolyexp\"]"*)
15.732 + "[]" (*..found broken in child of 33913fe24685, error covered by CAS-command *)
15.733 +then () else error "inform [rational,simplification] changed at end";
15.734 +(*Test_Tool.show_pt pt;
15.735 +[
15.736 +(([], Frm), Simplify (a * x / (b * x) + c * x / (d * x) + e / f)),
15.737 +(([1], Frm), a * x / (b * x) + c * x / (d * x) + e / f),
15.738 +(([1], Res), a / b + c / d + e / f),
15.739 +(([2,1], Frm), a / b + c / d + e / f),
15.740 +(([2,1], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.741 +(([2,2], Res), (a * d + c * b) / (b * d) + e / f),
15.742 +(([2], Res), (a * d + c * b) / (b * d) + e / f),
15.743 +(([3], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.744 +(([4,1], Frm), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.745 +(([4,1], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
15.746 +(([4,2], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.747 +(([4], Res), (b * d * e + b * c * f + a * d * f) / (b * d * f)),
15.748 +(([5], Res), (a * (d * f) + b * (c * f) + b * (d * e)) / (b * (d * f))),
15.749 +(([6], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f)),
15.750 +(([], Res), (a * d * f + b * c * f + b * d * e) / (b * d * f))]
15.751 +*)
15.752 +DEconstrCalcTree 1;
15.753 +
15.754 +(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd)
15.755 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
15.756 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
15.757 +"--------- Take as 1st tac, start with <NEW> (CAS input) ---------";
15.758 +val t = TermC.parse_test @{context} "Diff (x \<up> 2 + x + 1, x)";
15.759 +case t of Const (\<^const_name>\<open>Diff\<close>, _) $ _ => ()
15.760 + | _ => raise
15.761 + error "diff.sml behav.changed for CAS Diff (..., x)";
15.762 +TermC.atomty t;
15.763 +"-----------------------------------------------------------------";
15.764 +(*1>*)States.reset ();
15.765 +(*2>*)CalcTree @{context} [([], References.empty)];
15.766 +(*3>*)Iterator 1;moveActiveRoot 1;
15.767 +"----- here the Headline has been finished";
15.768 +(*4>*)moveActiveFormula 1 ([],Pbl);
15.769 +(*5>*)replaceFormula 1 "Diff (x \<up> 2 + x + 1, x)";
15.770 +val ((pt,_),_) = States.get_calc 1;
15.771 +val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
15.772 +val (SOME istate, NONE) = loc;
15.773 +(*default_print_depth 5;*)
15.774 +writeln"-----------------------------------------------------------";
15.775 +spec;
15.776 +writeln (I_Model.to_string ctxt probl);
15.777 +writeln (I_Model.to_string ctxt meth);
15.778 +writeln (Istate.string_of (fst istate));
15.779 +
15.780 +refFormula 1 ([],Pbl) (*--> correct CalcHead*);
15.781 + (*081016 NOT necessary (but leave it in Java):*)
15.782 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
15.783 +"----- here the CalcHead has been completed --- ONCE MORE ?????";
15.784 +
15.785 +(***difference II***)
15.786 +val ((pt,p),_) = States.get_calc 1;
15.787 +(*val p = ([], Pbl)*)
15.788 +val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
15.789 +val (SOME istate, NONE) = loc;
15.790 +(*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
15.791 +(*Pstate ([],
15.792 + [], NONE,
15.793 + ??.empty, Sundef, false)*)
15.794 +(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
15.795 +(*("Isac_Knowledge",
15.796 + ["derivative_of", "function"],
15.797 + ["diff", "differentiate_on_R"]) : spec*)
15.798 +writeln (I_Model.to_string ctxt probl);
15.799 +(*[
15.800 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])),
15.801 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
15.802 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
15.803 +writeln (I_Model.to_string ctxt meth);
15.804 +(*[
15.805 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])),
15.806 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
15.807 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
15.808 +writeln"-----------------------------------------------------------";
15.809 +(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
15.810 +(*WN081028 fixed <ERROR> helpless </ERROR> by inform returning ...(.,Met)*)
15.811 +autoCalculate 1 CompleteCalc;
15.812 +val ((pt,p),_) = States.get_calc 1;
15.813 +val Form res = (#1 o ME_Misc.pt_extract) (pt, ([],Res));
15.814 +Test_Tool.show_pt pt;
15.815 +
15.816 +if p = ([], Res) andalso UnparseC.term res = "1 + 2 * x" then ()
15.817 +else error "diff.sml behav.changed for Diff (x \<up> 2 + x + 1, x)";
15.818 +DEconstrCalcTree 1;
15.819 +-----------------------------------------------------------------------------------------------*)
15.820 +
15.821 +"--------- Take as 1st tac, start from exp -----------------------";
15.822 +"--------- Take as 1st tac, start from exp -----------------------";
15.823 +"--------- Take as 1st tac, start from exp -----------------------";
15.824 +(*the following input is copied from BridgeLog Java <==> SML,
15.825 + omitting unnecessary inputs*)
15.826 +(*1>*)States.reset ();
15.827 +(*2>*)CalcTree @{context} [(["functionTerm (x \<up> 2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of", "function"],["diff", "differentiate_on_R"]))];
15.828 +(*3>*)Iterator 1; moveActiveRoot 1;
15.829 +
15.830 +(*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
15.831 +(***difference II***)
15.832 +val ((pt,_),_) = States.get_calc 1;
15.833 +val PblObj {probl, meth, spec, fmz, loc, ...} = get_obj I pt [];
15.834 +val (SOME istate, NONE) = loc;
15.835 +(*default_print_depth 5;*) writeln (Istate.string_of (fst istate)); (*default_print_depth 3;*)
15.836 +(*Pstate ([],
15.837 + [], NONE,
15.838 + ??.empty, Sundef, false)*)
15.839 +(*default_print_depth 5;*) spec; (*default_print_depth 3;*)
15.840 +(*("Isac_Knowledge",
15.841 + ["derivative_of", "function"],
15.842 + ["diff", "differentiate_on_R"]) : spec*)
15.843 +writeln (I_Model.to_string ctxt probl);
15.844 +(*[
15.845 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])),
15.846 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
15.847 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
15.848 +writeln (I_Model.to_string ctxt meth);
15.849 +(*[
15.850 +(1 ,[1] ,true ,#Given ,Cor functionTerm (x \<up> 2 + x + 1) ,(f_, [x \<up> 2 + x + 1])),
15.851 +(2 ,[1] ,true ,#Given ,Cor differentiateFor x ,(v_, [x])),
15.852 +(3 ,[1] ,true ,#Find ,Cor derivative f_'_f ,(f_'_f, [f_'_f]))]*)
15.853 +writeln"-----------------------------------------------------------";
15.854 +(*7>*)fetchProposedTactic 1 (*--> Apply_Method*);
15.855 +autoCalculate 1 (Steps 1);
15.856 +val ((pt,p),_) = States.get_calc 1;
15.857 +val Form res = (#1 o (ME_Misc.pt_extract ctxt)) (pt, p);
15.858 +if UnparseC.term res = "d_d x (x \<up> 2 + x + 1)" then ()
15.859 +else error "diff.sml Diff (x \<up> 2 + x + 1, x) from exp";
15.860 +DEconstrCalcTree 1;
15.861 +
15.862 +(*POSTPONE CORRECTION AT END OF TRANSITION TO Isabelle/PIDE/Isac (~ Cas_Cmd)
15.863 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
15.864 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
15.865 +"--------- implicit_take, start with <NEW> (CAS input) ---------------";
15.866 +States.reset ();
15.867 +CalcTree @{context} [([], References.empty)];
15.868 +(*[[from sml: > @@@@@begin@@@@@
15.869 +[[from sml: 1
15.870 +[[from sml: <CALCTREE>
15.871 +[[from sml: <CALCID> 1 </CALCID>
15.872 +[[from sml: </CALCTREE>
15.873 +[[from sml: @@@@@end@@@@@*)
15.874 +Iterator 1;
15.875 +(*[[from sml: > @@@@@begin@@@@@
15.876 +[[from sml: 1
15.877 +[[from sml: <ADDUSER>
15.878 +[[from sml: <CALCID> 1 </CALCID>
15.879 +[[from sml: <USERID> 1 </USERID>
15.880 +[[from sml: </ADDUSER>
15.881 +[[from sml: @@@@@end@@@@@*)
15.882 +moveActiveRoot 1;
15.883 +(*[[from sml: > @@@@@begin@@@@@
15.884 +[[from sml: 1
15.885 +[[from sml: <CALCITERATOR>
15.886 +[[from sml: <CALCID> 1 </CALCID>
15.887 +[[from sml: <POSITION>
15.888 +[[from sml: <INTLIST>
15.889 +[[from sml: </INTLIST>
15.890 +[[from sml: <POS> Pbl </POS>
15.891 +[[from sml: </POSITION>
15.892 +[[from sml: </CALCITERATOR>
15.893 +[[from sml: @@@@@end@@@@@*)
15.894 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false;
15.895 +(*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
15.896 +[[from sml: 1
15.897 +[[from sml: <GETELEMENTSFROMTO>
15.898 +[[from sml: <CALCID> 1 </CALCID>
15.899 +[[from sml: <FORMHEADS>
15.900 +[[from sml: <CALCFORMULA>
15.901 +[[from sml: <POSITION>
15.902 +[[from sml: <INTLIST>
15.903 +[[from sml: </INTLIST>
15.904 +[[from sml: <POS> Pbl </POS>
15.905 +[[from sml: </POSITION>
15.906 +[[from sml: <FORMULA>
15.907 +[[from sml: <MATHML>
15.908 +[[from sml: <ISA> ________________________________________________ </ISA>
15.909 +[[from sml: </MATHML>
15.910 +[[from sml:
15.911 +[[from sml: </FORMULA>
15.912 +[[from sml: </CALCFORMULA>
15.913 +[[from sml: </FORMHEADS>
15.914 +[[from sml: </GETELEMENTSFROMTO>
15.915 +[[from sml: @@@@@end@@@@@*)
15.916 +refFormula 1 ([],Pbl);
15.917 +(*[[from sml: > @@@@@begin@@@@@ STILL CORRECT
15.918 +[[from sml: 1
15.919 +[[from sml: <REFFORMULA>
15.920 +[[from sml: <CALCID> 1 </CALCID>
15.921 +[[from sml: <CALCHEAD status = "incorrect">
15.922 +[[from sml: <POSITION>
15.923 +[[from sml: <INTLIST>
15.924 +[[from sml: </INTLIST>
15.925 +[[from sml: <POS> Pbl </POS>
15.926 +[[from sml: </POSITION>
15.927 +[[from sml: <HEAD>
15.928 +[[from sml: <MATHML>
15.929 +[[from sml: <ISA> Problem (ThyC.id_empty, [e_pblID]) </ISA>
15.930 +[[from sml: </MATHML>
15.931 +[[from sml: </HEAD>
15.932 +[[from sml: <MODEL>
15.933 +[[from sml: <GIVEN> </GIVEN>
15.934 +[[from sml: <WHERE> </WHERE>
15.935 +[[from sml: <FIND> </FIND>
15.936 +[[from sml: <RELATE> </RELATE>
15.937 +[[from sml: </MODEL>
15.938 +[[from sml: <BELONGSTO> Pbl </BELONGSTO>
15.939 +[[from sml: <SPECIFICATION>
15.940 +[[from sml: <THEORYID> ThyC.id_empty </THEORYID>
15.941 +[[from sml: <PROBLEMID>
15.942 +[[from sml: <STRINGLIST>
15.943 +[[from sml: <STRING> Problem.id_empty </STRING>
15.944 +[[from sml: </STRINGLIST>
15.945 +[[from sml: </PROBLEMID>
15.946 +[[from sml: <METHODID>
15.947 +[[from sml: <STRINGLIST>
15.948 +[[from sml: <STRING> e_metID </STRING>
15.949 +[[from sml: </STRINGLIST>
15.950 +[[from sml: </METHODID>
15.951 +[[from sml: </SPECIFICATION>
15.952 +[[from sml: </CALCHEAD>
15.953 +[[from sml: </REFFORMULA>
15.954 +[[from sml: @@@@@end@@@@@*)
15.955 +moveActiveFormula 1 ([],Pbl);
15.956 +(*[[from sml: > @@@@@begin@@@@@
15.957 +[[from sml: 1
15.958 +[[from sml: <CALCITERATOR>
15.959 +[[from sml: <CALCID> 1 </CALCID>
15.960 +[[from sml: <POSITION>
15.961 +[[from sml: <INTLIST>
15.962 +[[from sml: </INTLIST>
15.963 +[[from sml: <POS> Pbl </POS>
15.964 +[[from sml: </POSITION>
15.965 +[[from sml: </CALCITERATOR>
15.966 +[[from sml: @@@@@end@@@@@*)
15.967 +replaceFormula 1 "Simplify (1+2)";
15.968 +(*[[from sml: > @@@@@begin@@@@@
15.969 +[[from sml: 1
15.970 +[[from sml: <REPLACEFORMULA>
15.971 +[[from sml: <CALCID> 1 </CALCID>
15.972 +[[from sml: <CALCCHANGED>
15.973 +[[from sml: <UNCHANGED>
15.974 +[[from sml: <INTLIST>
15.975 +[[from sml: </INTLIST>
15.976 +[[from sml: <POS> Pbl </POS>
15.977 +[[from sml: </UNCHANGED>
15.978 +[[from sml: <DELETED>
15.979 +[[from sml: <INTLIST>
15.980 +[[from sml: </INTLIST>
15.981 +[[from sml: <POS> Pbl </POS>
15.982 +[[from sml: </DELETED>
15.983 +[[from sml: <GENERATED>
15.984 +[[from sml: <INTLIST>
15.985 +[[from sml: </INTLIST>
15.986 +[[from sml: <POS> Met </POS> DIFFERENCE: Pbl
15.987 +[[from sml: </GENERATED>
15.988 +[[from sml: </CALCCHANGED>
15.989 +[[from sml: </REPLACEFORMULA>
15.990 +[[from sml: @@@@@end@@@@@*)
15.991 +getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false(* DIFFERENCE: Pbl*);
15.992 +(*@@@@@begin@@@@@
15.993 + 1
15.994 +<GETELEMENTSFROMTO>
15.995 + <CALCID> 1 </CALCID>
15.996 + <FORMHEADS>
15.997 + <CALCFORMULA>
15.998 + <POSITION>
15.999 + <INTLIST>
15.1000 + </INTLIST>
15.1001 + <POS> Pbl </POS>
15.1002 + </POSITION>
15.1003 + <FORMULA>
15.1004 + <MATHML>
15.1005 + <ISA> Simplify (1 + 2) </ISA> WORKS !!!!!
15.1006 + </MATHML>
15.1007 + </FORMULA>
15.1008 + </CALCFORMULA>
15.1009 + </FORMHEADS>
15.1010 +</GETELEMENTSFROMTO>
15.1011 +@@@@@end@@@@@*)
15.1012 +getFormulaeFromTo 1 ([],Pbl) ([],Met) 0 false;
15.1013 +(*[[from sml: > @@@@@begin@@@@@
15.1014 +[[from sml: 1
15.1015 +[[from sml: <SYSERROR>
15.1016 +[[from sml: <CALCID> 1 </CALCID>
15.1017 +[[from sml: <ERROR> error in getFormulaeFromTo </ERROR>
15.1018 +[[from sml: </SYSERROR>
15.1019 +[[from sml: @@@@@end@@@@@*)
15.1020 +(*step into getFormulaeFromTo --- bug corrected...*)
15.1021 +-----------------------------------------------------------------------------------------------*)
15.1022 +
15.1023 +"--------- build fun check_for' ------------------------------";
15.1024 +"--------- build fun check_for' ------------------------------";
15.1025 +"--------- build fun check_for' ------------------------------";
15.1026 +val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]: subst;
15.1027 +val rls = norm_Rational
15.1028 +val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
15.1029 +val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "2 / 4");
15.1030 +val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "1 / 2");
15.1031 +
15.1032 +val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
15.1033 + rew_sub ctxt 1 [] Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
15.1034 +if rewritten then NONE else SOME "e_errpatID";
15.1035 +
15.1036 +val norm_res = case rewrite_set_ ctxt false rls res' of
15.1037 + NONE => res'
15.1038 +| SOME (norm_res, _) => norm_res
15.1039 +
15.1040 +val norm_inf = case rewrite_set_ ctxt false rls inf of
15.1041 + NONE => inf
15.1042 +| SOME (norm_inf, _) => norm_inf;
15.1043 +
15.1044 +res' = inf;
15.1045 +norm_res = norm_inf;
15.1046 +
15.1047 +val pat = TermC.parse_patt @{theory} "(?a + ?b)/?a = ?b";
15.1048 +val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/2", TermC.parse_test @{context} "3");
15.1049 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
15.1050 +then () else error "error patt example1 changed";
15.1051 +
15.1052 +val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?a + ?c) = ?b / ?c";
15.1053 +val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(2 + 4)", TermC.parse_test @{context} "3 / 4");
15.1054 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
15.1055 +then () else error "error patt example2 changed";
15.1056 +
15.1057 +val pat = TermC.parse_patt @{theory} "(?a + ?b)/(?b + ?c) = ?a / ?c";
15.1058 +val (res, inf) = (TermC.parse_test @{context} "(2 + 3)/(3 + 4)", TermC.parse_test @{context} "2 / 4");
15.1059 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
15.1060 +then () else error "error patt example3 changed";
15.1061 +
15.1062 +val inf = TermC.parse_test @{context} "1 / 2";
15.1063 +if check_for' ctxt (res, inf) subst ("errpatID", pat) rls = SOME "errpatID"
15.1064 +then () else error "error patt example3 changed";
15.1065 +
15.1066 +"--------- build fun check_for' ?bdv -------------------------";
15.1067 +"--------- build fun check_for' ?bdv -------------------------";
15.1068 +"--------- build fun check_for' ?bdv -------------------------";
15.1069 +val ctxt = Proof_Context.init_global @{theory}
15.1070 +val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")]: subst;
15.1071 +val t = TermC.parse_test @{context} "d_d x (x \<up> 2 + sin (x \<up> 4))";
15.1072 +val SOME (t, _) = rewrite_set_inst_ ctxt false subst norm_diff t;
15.1073 +if UnparseC.term t = "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" then ()
15.1074 +else error "build fun check_for' ?bdv changed 1";
15.1075 +
15.1076 +val rls = norm_diff
15.1077 +val pat = TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)";
15.1078 +val (res, inf) = (TermC.parse_test @{context} "2 * x + d_d x (sin (x \<up> 4))", TermC.parse_test @{context} "2 * x + cos (4 * x \<up> 3)");
15.1079 +
15.1080 +val (res', _, _, rewritten) = (*rewritten: the lhs of the pattern TermC.matches in res*)
15.1081 + rew_sub ctxt 1 subst Rewrite_Ord.function_empty Rule_Set.empty false [] (HOLogic.Trueprop $ pat) res;
15.1082 +if UnparseC.term res' = "2 * x + cos (d_d x (x \<up> 4))" andalso rewritten then ()
15.1083 +else error "build fun check_for' ?bdv changed 2";
15.1084 +
15.1085 +val norm_res = case rewrite_set_inst_ ctxt false subst rls res' of
15.1086 + NONE => res'
15.1087 +| SOME (norm_res, _) => norm_res;
15.1088 +if UnparseC.term norm_res = "2 * x + cos (4 * x \<up> 3)" then ()
15.1089 +else error "build fun check_for' ?bdv changed 3";
15.1090 +
15.1091 +val norm_inf = case rewrite_set_inst_ ctxt false subst rls inf of
15.1092 + NONE => inf
15.1093 +| SOME (norm_inf, _) => norm_inf;
15.1094 +if UnparseC.term norm_inf = "2 * x + cos (4 * x \<up> 3)" then ()
15.1095 +else error "build fun check_for' ?bdv changed 4";
15.1096 +
15.1097 +res' = inf;
15.1098 +if norm_res = norm_inf then ()
15.1099 +else error "build fun check_for' ?bdv changed 5";
15.1100 +
15.1101 +if Error_Pattern.check_for' ctxt (res, inf) (subst: subst) ("errpatID": Error_Pattern.id, pat) rls = SOME "errpatID"
15.1102 +then () else error "error patt example1 changed";
15.1103 +
15.1104 +"--------- build fun check_for ------------------------";
15.1105 +"--------- build fun check_for ------------------------";
15.1106 +"--------- build fun check_for ------------------------";
15.1107 +val (res, inf) =
15.1108 + (TermC.parse_test @{context} "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))",
15.1109 + TermC.parse_test @{context} "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
15.1110 +val {errpats, rew_rls = rls, program = Prog prog, ...} = MethodC.from_store ctxt ["diff", "differentiate_on_R"]
15.1111 +
15.1112 +val env = [(TermC.parse_test @{context} "v_v", TermC.parse_test @{context} "x")];
15.1113 +val errpats =
15.1114 + [Error_Pattern.empty, (*generalised for testing*)
15.1115 + ("chain-rule-diff-both",
15.1116 + [TermC.parse_patt @{theory} "d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)",
15.1117 + TermC.parse_patt @{theory} "d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)",
15.1118 + TermC.parse_patt @{theory} "d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)",
15.1119 + TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / ?u",
15.1120 + TermC.parse_patt @{theory} "d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u"],
15.1121 + [@{thm diff_sin_chain}, @{thm diff_cos_chain}, @{thm diff_pow_chain},
15.1122 + @{thm diff_ln_chain}, @{thm diff_exp_chain}])];
15.1123 +case Error_Pattern.check_for ctxt (res, inf) (prog, env) (errpats, rls) of SOME _ => ()
15.1124 +| NONE => error "Error_Pattern.check_for broken";
15.1125 +DEconstrCalcTree 1;
15.1126 +
15.1127 +"--------- embed fun check_for ------------------------";
15.1128 +"--------- embed fun check_for ------------------------";
15.1129 +"--------- embed fun check_for ------------------------";
15.1130 +States.reset ();
15.1131 +CalcTree @{context}
15.1132 +[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
15.1133 + ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
15.1134 +Iterator 1;
15.1135 +moveActiveRoot 1;
15.1136 +autoCalculate 1 CompleteCalcHead;
15.1137 +autoCalculate 1 (Steps 1);
15.1138 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
15.1139 +(*autoCalculate 1 (Steps 1);([2], Res), d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> \<up> 4)*)
15.1140 +
15.1141 +"~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x \<up> 2) + cos (4 * x \<up> 3)");
15.1142 +"~~~~~ fun appendFormula' , args:"; val (cI, (ifo: TermC.as_string)) = (cI, ifo);
15.1143 + val cs = States.get_calc cI
15.1144 + val pos = States.get_pos cI 1;
15.1145 +(*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
15.1146 + val ("ok", cs' as (_, _, ptp)) = (*case*) Step.do_next pos cs (*of*);
15.1147 + (*case*) Step_Solve.by_term ptp (encode ifo) (*of*); (*ERROR WAS: "no derivation found"*)
15.1148 +"~~~~~ fun Step_Solve.by_term , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Calc.state_post), istr)
15.1149 + = (cs', (encode ifo));
15.1150 + val ctxt = get_ctxt pt pos (*see TODO.thy*)
15.1151 + val SOME f_in = (*case*) TermC.parseNEW ctxt istr (*of*);
15.1152 + val pos_pred = lev_back' pos
15.1153 + val f_pred = Ctree.get_curr_formula (pt, pos_pred);
15.1154 + (*if*) f_pred = f_in; (*else*)
15.1155 + val NONE = (*case*) CAS_Cmd.input f_in (*of*);
15.1156 + (*old* )val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
15.1157 + (*old*)val {program = prog, ...} = MethodC.from_store ctxt metID
15.1158 + (*old*)val istate = get_istate_LI pt pos
15.1159 + (*old*)val ctxt = get_ctxt pt pos
15.1160 + ( *old*)
15.1161 + val LI.Not_Derivable =
15.1162 + (*case*) LI.locate_input_term (pt, pos) f_in (*of*);
15.1163 + val ctxt = Ctree.get_ctxt pt pos
15.1164 + val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
15.1165 + val (errpats, rew_rls, prog) =
15.1166 + case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
15.1167 + {errpats, rew_rls, program = Rule.Prog prog, ...} => (errpats, rew_rls, prog)
15.1168 + | _ => error "inform: uncovered case of MethodC.from_store ctxt"
15.1169 +;
15.1170 +\<close> ML \<open>
15.1171 +Error_Pattern.s_to_string errpats
15.1172 +\<close> ML \<open>
15.1173 +(*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\"]]"
15.1174 +(*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
15.1175 +
15.1176 + val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
15.1177 +;
15.1178 +\<close> ML \<open>
15.1179 +(*+*)if UnparseC.term f_pred = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" andalso
15.1180 +(*+*) UnparseC.term f_in = "d_d x (x \<up> 2) + cos (4 * x \<up> 3)"
15.1181 +(*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 2";
15.1182 +
15.1183 +\<close> ML \<open>
15.1184 + val SOME "chain-rule-diff-both" = (*case*) Error_Pattern.check_for ctxt (f_pred, f_in) (prog, env) (errpats, rew_rls) (*of*);
15.1185 +
15.1186 +\<close> ML \<open>
15.1187 +"--- final check:";
15.1188 +(*+*)val (_, _, ptp') = cs';
15.1189 +\<close> ML \<open>
15.1190 +Step_Solve.by_term ptp' (encode ifo)
15.1191 +\<close> ML \<open>
15.1192 +(* ATTENTION: THE error pattern GOT LOST ...
15.1193 +case Step_Solve.by_term ptp' (encode ifo) of
15.1194 + ("error pattern #chain-rule-diff-both#", calcstate') => ()
15.1195 +| _ => error "inform with (positive) Error_Pattern.check_for broken"
15.1196 +*)
15.1197 +
15.1198 +\<close> ML \<open>
15.1199 +"----------- re-build: fill_from_store without thy-hierarchy -----------------------------------";
15.1200 +"----------- re-build: fill_from_store without thy-hierarchy -----------------------------------";
15.1201 +"----------- re-build: fill_from_store without thy-hierarchy -----------------------------------";
15.1202 +open Error_Pattern
15.1203 +val c = []: int list
15.1204 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context}
15.1205 +[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
15.1206 + ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
15.1207 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.1208 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.1209 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.1210 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.1211 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.1212 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.1213 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["diff", "differentiate_on_R"]*)
15.1214 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_sum", "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v"))*)
15.1215 + val ([1], Frm) = p;
15.1216 + val "d_d x (x \<up> 2 + sin (x \<up> 4))" = f2str f;
15.1217 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_sin_chain", "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u"))*)
15.1218 + val ([1], Res) = p;
15.1219 + val "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" = f2str f
15.1220 +
15.1221 +val return_of_me = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_pow", "d_d ?bdv (?bdv \<up> ?n) = ?n * ?bdv \<up> (?n - 1)"))*)
15.1222 + val ([1], Res) = p
15.1223 + val "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" = f2str f;
15.1224 + (* "d_d x (x \<up> 2) + cos (x \<up> 4)" .. wrong user input within next step *)
15.1225 +(*//------------------ step into find_fill_patterns ----------------------------------------\\*)
15.1226 +(* INSTEAD OF STEPPING INTO me WE DO SO FOR Kernel.findFillpatterns cI errpatID =
15.1227 + let
15.1228 + val ((pt, _), _) = States.get_calc cI
15.1229 + val pos = States.get_pos cI 1;
15.1230 + val fillpats = Error_Pattern.find_fill_patterns (pt, pos) errpatID
15.1231 +*)
15.1232 +"~~~~~ fun findFillpatterns , args:"; val (pt, p, errpatID) = (pt, p, "chain-rule-diff-both");
15.1233 +"~~~~~ fun find_fill_patterns , args:"; val ((pt, pos as (p, _)), id) = ((pt, p), errpatID);
15.1234 +(*old-------\* )
15.1235 + val f_curr = Ctree.get_curr_formula (pt, pos);
15.1236 + val pp = Ctree.par_pblobj pt p
15.1237 + val (errpats, prog) = case MethodC.from_store ctxt (Ctree.get_obj Ctree.g_metID pt pp) of
15.1238 + {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
15.1239 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
15.1240 +( *new-------\*)
15.1241 + val ctxt = Ctree.get_ctxt pt pos
15.1242 + val f_curr = Ctree.get_curr_formula (pt, pos)
15.1243 + val met_id = Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p)
15.1244 + val (errpats, prog) = case MethodC.from_store' (Know_Store.get_via_last_thy "Build_Thydata") met_id of
15.1245 + {errpats, program = Rule.Prog prog, ...} => (errpats, prog)
15.1246 + | _ => error "find_fill_patterns: uncovered case of MethodC.from_store ctxt"
15.1247 +(*new-------/*)
15.1248 +
15.1249 +(*+*)val 1 = length errpats(*ONLY WITH from_store' @{theory (*!!!*)Build_Thydata}*)
15.1250 + val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
15.1251 + val subst = Subst.for_bdv ctxt prog env
15.1252 + val errpatthms = errpats
15.1253 + |> filter ((curry op = errpatID) o (#1: Error_Pattern.T -> Error_Pattern.id))
15.1254 + |> map (#3: Error_Pattern.T -> thm list)
15.1255 + |> flat;
15.1256 +
15.1257 +(*+*)val 3 = length errpatthms;
15.1258 +(*+*)val 5 = length (get_fill_ins @{theory} "diff_sin_chain");
15.1259 +
15.1260 +(*case*) map (
15.1261 + fill_from_store ctxt subst f_curr errpatID) errpatthms |> flat (*of*);
15.1262 +"~~~~~ fun fill_from_store , args:"; val (ctxt, subst, form, (*id*)errpat_id, thm) =
15.1263 + (ctxt, subst, f_curr, errpatID, hd errpatthms);
15.1264 + val thm_id_long = Thm.get_name_hint thm
15.1265 +
15.1266 +(*+*)val "Diff.diff_sin_chain" = thm_id_long;
15.1267 +(*+*)val "diff_sin_chain" = ThmC.cut_id thm_id_long;
15.1268 +
15.1269 + val thm_id = ThmC.cut_id thm_id_long
15.1270 + val fill_ins =
15.1271 +
15.1272 +Error_Pattern.get_fill_ins (Proof_Context.theory_of ctxt) thm_id;
15.1273 +"~~~~~ fun get_fill_ins , args:"; val (thy, thm_id) =
15.1274 + ((Proof_Context.theory_of ctxt), thm_id);
15.1275 + (*case*) AList.lookup (op =) (get_fill_inss thy) thm_id (*of*);
15.1276 +val ERROR "fill_ins for thm \"diff_sin_chain\" missing in theory \"Isac_Knowledge\" (and ancestors)\nTODO exception hierarchy needs to be established." =
15.1277 + ERROR ("fill_ins for thm \"" ^ thm_id ^ "\" missing in theory \"" ^
15.1278 + (thy |> ThyC.id_of) ^ "\" (and ancestors)" ^
15.1279 + "\nTODO exception hierarchy needs to be established.");
15.1280 +
15.1281 +(*return to fill_from_store..*)
15.1282 + val some = map (fill_form ctxt subst (thm, form) errpat_id) fill_ins;
15.1283 +val return_fill_from_store = some |> filter is_some |> map the;
15.1284 +
15.1285 +(* final test ... ----------------------------------------------------------------------------*)
15.1286 +(*+*)if length return_fill_from_store = 5 then
15.1287 +(*+*) case return_fill_from_store of
15.1288 +(*+*) ("fill-d_d-arg", tm, thm, subsopt) :: _ => if UnparseC.term tm =
15.1289 +(*+*) "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1"
15.1290 +(*+*) then () else error "find_fill_patterns changed 2a"
15.1291 +(*+*) | _ => error "find_fill_patterns changed 2b"
15.1292 +(*+*)else error "find_fill_patterns changed 2c";
15.1293 +(*-------------------- stop step into find_fill_patterns -------------------------------------*)
15.1294 +(*\\------------------ step into find_fill_patterns ----------------------------------------//*)
15.1295 +
15.1296 +val (p,_,f,nxt,_,pt) = return_of_me
15.1297 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Rewrite_Inst (["(''bdv'', x)"], ("diff_pow", "d_d ?bdv (?bdv \<up> ?n) = ?n * ?bdv \<up> (?n - 1)"))*)
15.1298 + val ([3], Res) = p
15.1299 + val "d_d x (x \<up> 2) + cos (x \<up> 4) * (4 * x \<up> (4 - 1))" = f2str f;
15.1300 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.1301 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Check_Postcond ["derivative_of", "function"]*)
15.1302 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
15.1303 + val ([], Res) = p;
15.1304 + val "2 * x + cos (x \<up> 4) * 4 * x \<up> 3" = f2str f
15.1305 + val End_Proof' = nxt;
15.1306 +
15.1307 +
15.1308 +\<close> ML \<open>
15.1309 +"--------- embed fun find_fill_patterns ---------------------------";
15.1310 +"--------- embed fun find_fill_patterns ---------------------------";
15.1311 +"--------- embed fun find_fill_patterns ---------------------------";
15.1312 +States.reset ();
15.1313 +CalcTree @{context}
15.1314 +[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
15.1315 + ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
15.1316 +Iterator 1;
15.1317 +moveActiveRoot 1;
15.1318 +autoCalculate 1 CompleteCalcHead;
15.1319 +autoCalculate 1 (Steps 1);
15.1320 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
15.1321 +appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)";
15.1322 + (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
15.1323 + (*or
15.1324 + <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
15.1325 +"~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
15.1326 + val ((pt, _), _) = States.get_calc cI
15.1327 + val pos = States.get_pos cI 1;
15.1328 +
15.1329 +val return_from_find_fill_patterns = find_fill_patterns (pt, pos) errpatID;
15.1330 +DEconstrCalcTree 1;
15.1331 +
15.1332 +(* final test ... ----------------------------------------------------------------------------*)
15.1333 +val 6 = length return_from_find_fill_patterns
15.1334 +val (fill_in_id, term, thm, subst) :: _ = return_from_find_fill_patterns
15.1335 +
15.1336 +val "fill-d_d-arg" = fill_in_id
15.1337 +val "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =\nd_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1" =
15.1338 + UnparseC.term_in_ctxt @{context} term
15.1339 +val "Diff.diff_sin_chain" = Thm.get_name_hint thm
15.1340 +val "[(''bdv'', x)]" = subst |> the |> Subst.string_of_input;
15.1341 +
15.1342 +
15.1343 +\<close> ML \<open>
15.1344 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
15.1345 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
15.1346 +"--------- build fun is_exactly_equal, inputFillFormula ----------";
15.1347 +States.reset ();
15.1348 +CalcTree @{context}
15.1349 +[(["functionTerm (x \<up> 2 + sin (x \<up> 4))", "differentiateFor x", "derivative f_f'"],
15.1350 + ("Isac_Knowledge", ["derivative_of", "function"], ["diff", "differentiate_on_R"]))];
15.1351 +Iterator 1;
15.1352 +moveActiveRoot 1;
15.1353 +autoCalculate 1 CompleteCalcHead;
15.1354 +autoCalculate 1 (Steps 1);
15.1355 +autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))*)
15.1356 +appendFormula 1 "d_d x (x \<up> 2) + cos (4 * x \<up> 3)" (*|> Future.join*); (*<<<<<<<=========================*)
15.1357 +(* the check for errpat is maximally liberal (whole term modulo "rew_rls" from "type met"),
15.1358 + would recognize "cos (4 * x \<up> (4 - 1)) + 2 * x" as well.
15.1359 + results in <CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>
15.1360 + instead of <CALCMESSAGE> no derivation found </CALCMESSAGE> *)
15.1361 + val ((pt,pos), _) = States.get_calc 1;
15.1362 + val p = States.get_pos 1 1;
15.1363 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
15.1364 +
15.1365 + if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
15.1366 + case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
15.1367 + ("diff_sum", thm)) =>
15.1368 + if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
15.1369 + else error "embed fun fill_form changed 11"
15.1370 + | _ => error "embed fun fill_form changed 12"
15.1371 + else error "embed fun fill_form changed 13";
15.1372 +
15.1373 +findFillpatterns 1 "chain-rule-diff-both"; (*<<<<<<<=================================*)
15.1374 +(*<CALCMESSAGE> fill patterns #fill-d_d-arg#d_d x (x \<up> 2) + d_d x (sin (x \<up> 4)) =
15.1375 + d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x ?_dummy_1#fill-both-args#...#...#... *)
15.1376 + val ((pt,pos),_) = States.get_calc 1;
15.1377 + val p = States.get_pos 1 1;
15.1378 +
15.1379 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
15.1380 + if p = ([1], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))" then
15.1381 + case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
15.1382 + ("diff_sum", thm)) =>
15.1383 + if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
15.1384 + else error "embed fun fill_form changed 21"
15.1385 + | _ => error "embed fun fill_form changed 22"
15.1386 + else error "embed fun fill_form changed 23";
15.1387 +
15.1388 +requestFillformula 1 ("chain-rule-diff-both", "fill-both-args");(*<<<<<<<============*)
15.1389 + (*<AUTOCALC> ([1], Res) ([2], Res) ([2], Res) </AUTOCALC>*)
15.1390 + val ((pt,pos),_) = States.get_calc 1;
15.1391 + val p = States.get_pos 1 1;
15.1392 + val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
15.1393 + if p = ([1], Res) andalso existpt [2] pt
15.1394 + andalso UnparseC.term f = "d_d x (x \<up> 2) + d_d x (sin (x \<up> 4))"
15.1395 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
15.1396 + ("diff_sum", thm)) =>
15.1397 + if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" then ()
15.1398 + else error "embed fun fill_form changed 31"
15.1399 + | _ => error "embed fun fill_form changed 32"
15.1400 + else error "embed fun fill_form changed 33";
15.1401 +
15.1402 +(* input a formula which exactly fills the gaps in a "fillformula"
15.1403 + presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":
15.1404 + errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.
15.1405 + the respective thm is in the ctree ................
15.1406 +*)
15.1407 +"~~~~~ fun inputFillFormula, args:"; val (cI, ifo) =
15.1408 + (1, "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)");
15.1409 + val ((pt, _), _) = States.get_calc cI
15.1410 + val pos = States.get_pos cI 1;
15.1411 +
15.1412 +"~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
15.1413 + val SOME ifo = parseNEW (ThyC.get_theory "Isac_Knowledge" |> Proof_Context.init_global) istr
15.1414 + val p' = lev_on p;
15.1415 + val tac = get_obj g_tac pt p';
15.1416 +val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
15.1417 +if (UnparseC.term o Thm.prop_of) ttt = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
15.1418 +else error "inputFillFormula changed 10";
15.1419 + val Applicable.Yes rew = Step.check tac (pt, pos);
15.1420 + val Rewrite_Inst' (_, _, _, _, _, _, _, (res, _)) = rew;
15.1421 +
15.1422 +"~~~~~ to inputFillFormula return val:"; val ("ok", tac) = ("ok", tac);
15.1423 + val ("ok", (_, c, ptp as (_,p'))) = Step.by_tactic tac (pt, pos);
15.1424 + States.upd_calc cI (ptp, []);
15.1425 + States.upd_ipos cI 1 p';
15.1426 + autocalculateOK2xml cI pos (if null c then p' else last_elem c) p';
15.1427 +
15.1428 +"~~~~~ final check:";
15.1429 +val ((pt, _),_) = States.get_calc 1;
15.1430 +val p = States.get_pos 1 1;
15.1431 +val (Form f, _, asms) = ME_Misc.pt_extract ctxt (pt, p);
15.1432 + if p = ([2], Res) andalso UnparseC.term f = "d_d x (x \<up> 2) + cos (x \<up> 4) * d_d x (x \<up> 4)"
15.1433 + then case get_obj g_tac pt (fst p) of Rewrite_Inst (["(''bdv'', x)"],
15.1434 + ("diff_sin_chain", thm)) =>
15.1435 + if (UnparseC.term o Thm.prop_of) thm = "d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u" then ()
15.1436 + else error "inputFillFormula changed 111"
15.1437 + | _ => error "inputFillFormula changed 112"
15.1438 + else error "inputFillFormula changed 113";
15.1439 +
15.1440 +"--------- fun appl_adds -----------------------------------------";
15.1441 +"--------- fun appl_adds -----------------------------------------";
15.1442 +"--------- fun appl_adds -----------------------------------------";
15.1443 +(* val (dI, oris, model, pbt, selct::ss) =
15.1444 + (dI, pors, probl, model, map itms2fstr probl);
15.1445 + ...vvv
15.1446 + *)
15.1447 +(* val (dI, oris, model, pbt, (selct::ss))=
15.1448 + (#1 (References.select_input ospec spec), oris, []:I_Model.T,
15.1449 + ((#model o Problem.from_store) (#2 (References.select_input ospec spec))),(imodel2fstr imodel));
15.1450 + val iii = appl_adds dI oris model pbt (selct::ss);
15.1451 + tracing(I_Model.to_string thy iii);
15.1452 +
15.1453 + val itm = add_single' dI oris model pbt selct;
15.1454 + val model = I_Model.add itm model;
15.1455 +
15.1456 + val _::selct::ss = (selct::ss);
15.1457 + val itm = add_single' dI oris model pbt selct;
15.1458 + val model = I_Model.add itm model;
15.1459 +
15.1460 + val _::selct::ss = (selct::ss);
15.1461 + val itm = add_single' dI oris model pbt selct;
15.1462 + val model = I_Model.add itm model;
15.1463 + tracing(I_Model.to_string thy model);
15.1464 +
15.1465 + val _::selct::ss = (selct::ss);
15.1466 + val itm = add_single' dI oris model pbt selct;
15.1467 + val model = I_Model.add itm model;
15.1468 + *)
15.1469 +"--------- fun concat_deriv --------------------------------------";
15.1470 +"--------- fun concat_deriv --------------------------------------";
15.1471 +"--------- fun concat_deriv --------------------------------------";
15.1472 +(*
15.1473 + val ({rew_ord, asm_rls, rules,...}, fo, ifo) =
15.1474 + (Rule_Set.rep Test_simplify, TermC.parse_test @{context} "x+1+ - 1*2=0", TermC.parse_test @{context} "-2*1+(x+1)=0");
15.1475 + (tracing o Derive.trtas2str) fod';
15.1476 +> ["
15.1477 +(x + 1 + - 1 * 2 = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (x + 1) = 0, []))", "
15.1478 +(- 1 * 2 + (x + 1) = 0, Thm ("radd_commute", "?m + ?n = ?n + ?m"), (- 1 * 2 + (1 + x) = 0, []))", "
15.1479 +(- 1 * 2 + (1 + x) = 0, Thm ("radd_left_commute", "?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (- 1 * 2 + x) = 0, []))", "
15.1480 +(1 + (- 1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))", "- 1 * 2 = -2"), (1 + (-2 + x) = 0, []))"]
15.1481 +val it = () : unit
15.1482 + (tracing o Derive.trtas2str) (map Derive.rev_deriv' rifod');
15.1483 +> ["
15.1484 +(1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))", "-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))", "
15.1485 +(1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))", "
15.1486 +(-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute", "?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"]
15.1487 +val it = () : unit
15.1488 +*)
15.1489 +"--------- handle an input formula -------------------------------";
15.1490 +"--------- handle an input formula -------------------------------";
15.1491 +"--------- handle an input formula -------------------------------";
15.1492 +(*
15.1493 +Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler:
15.1494 +Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden,
15.1495 +wenn Abteilungen nur auf gleichem Level gesucht werden ?
15.1496 +WN.040216
15.1497 +
15.1498 +Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
15.1499 +
15.1500 +------------------------------------------------------------------------------
15.1501 +"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
15.1502 +------------------------------------------------------------------------------
15.1503 +1. "5 * x / (x - 2) - x / (x + 2) = 4"
15.1504 +...
15.1505 +4. "12 * x + 4 * x \<up> 2 = 4 * (-4 + x \<up> 2)",Subproblem["normalise", "poly"..
15.1506 +...
15.1507 +4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
15.1508 +...
15.1509 +4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
15.1510 +...
15.1511 +"[x = -4 / 3]"
15.1512 +------------------------------------------------------------------------------
15.1513 +(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
15.1514 +
15.1515 +(4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
15.1516 +------------------------------------------------------------------------------
15.1517 +
15.1518 +
15.1519 +------------------------------------------------------------------------------
15.1520 +"Schalk I s.87 Bsp 55b (x/(x \<up> 2 - 6*x+9) - 1/(x \<up> 2 - 3*x) =1/x)";
15.1521 +------------------------------------------------------------------------------
15.1522 +1. "x / (x \<up> 2 - 6 * x + 9) - 1 / (x \<up> 2 - 3 * x) = 1 / x"
15.1523 +...
15.1524 +4. "(3 + (- 1 * x + x \<up> 2)) * x = 1 * (9 * x + (x \<up> 3 + -6 * x \<up> 2))"
15.1525 + Subproblem["normalise", "polynomial", "univariate"..
15.1526 +...
15.1527 +4.4. "-6 * x + 5 * x \<up> 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
15.1528 +...
15.1529 +4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
15.1530 +4.4.5. "[x = 0, x = 6 / 5]"
15.1531 +...
15.1532 +5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
15.1533 + "[x = 6 / 5]"
15.1534 +------------------------------------------------------------------------------
15.1535 +(1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
15.1536 +
15.1537 +(4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.]
15.1538 +------------------------------------------------------------------------------
15.1539 +
15.1540 +
15.1541 +------------------------------------------------------------------------------
15.1542 +"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
15.1543 +------------------------------------------------------------------------------
15.1544 +1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)"
15.1545 +...
15.1546 +6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
15.1547 + Subproblem["sq", "rootX", "univariate", "equation"]
15.1548 +...
15.1549 +6.6. "144 + 288 * x + 144 * x \<up> 2 = 144 + x \<up> 2 + 288 * x + 143 * x \<up> 2"
15.1550 + Subproblem["normalise", "polynomial", "univariate", "equation"]
15.1551 +...6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
15.1552 +... Or_to_List
15.1553 +6.6.3.2 "UniversalList"
15.1554 +------------------------------------------------------------------------------
15.1555 +(1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n]
15.1556 +
15.1557 +(6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n]
15.1558 +------------------------------------------------------------------------------
15.1559 +*)
15.1560 +(*sh. comments auf 498*)
15.1561 +"--------- fun dropwhile' ----------------------------------------";
15.1562 +"--------- fun dropwhile' ----------------------------------------";
15.1563 +"--------- fun dropwhile' ----------------------------------------";
15.1564 +(*
15.1565 + fun equal a b = a=b;
15.1566 + val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5];
15.1567 + val r_foder = rev foder; val r_ifoder = rev ifoder;
15.1568 + dropwhile' equal r_foder r_ifoder;
15.1569 +> val it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list
15.1570 +
15.1571 + val foder = [3,4,5]; val ifoder = [11,12,3,4,5];
15.1572 + val r_foder = rev foder; val r_ifoder = rev ifoder;
15.1573 + dropwhile' equal r_foder r_ifoder;
15.1574 +> val it = ([3], [3, 12, 11]) : int list * int list
15.1575 +
15.1576 + val foder = [5]; val ifoder = [11,12,3,4,5];
15.1577 + val r_foder = rev foder; val r_ifoder = rev ifoder;
15.1578 + dropwhile' equal r_foder r_ifoder;
15.1579 +> val it = ([5], [5, 4, 3, 12, 11]) : int list * int list
15.1580 +
15.1581 + val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5];
15.1582 + val r_foder = rev foder; val r_ifoder = rev ifoder;
15.1583 + dropwhile' equal r_foder r_ifoder;
15.1584 +> *** dropwhile': did not start with equal elements*)
15.1585 +\<close> ML \<open>
15.1586 +\<close> ML \<open>
15.1587 +\<close>
15.1588 +
15.1589 section \<open>===================================================================================\<close>
15.1590 ML \<open>
15.1591 \<close> ML \<open>