1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Thu May 30 12:39:13 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Sat Jun 01 11:09:19 2019 +0200
1.3 @@ -188,12 +188,13 @@
1.4 \<close>
1.5 subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
1.6
1.7 -partial_function (tailrec) biegelinie :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> bool"
1.8 +partial_function (tailrec) biegelinie ::
1.9 + "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> real list \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
1.10 where
1.11 -"biegelinie l q v b s vs =
1.12 +"biegelinie l q v b s vs id_abl =
1.13 (let
1.14 funs = SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
1.15 - [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v]; \<comment> \<open>PROG +args\<close>
1.16 + [''Biegelinien'', ''ausBelastung'']) [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl];
1.17 equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
1.18 [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];
1.19 cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''], [''no_met''])
1.20 @@ -279,10 +280,10 @@
1.21 (Rewrite ''make_fun_explicit'' False)) M__M;
1.22 N__N = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
1.23 [''diff'', ''integration'', ''named''])
1.24 - [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl]; \<comment> \<open>PROG string\<close>
1.25 + [REAL (rhs N__N), REAL v_v, REAL_REAL id_abl];
1.26 B__B = SubProblem (''Biegelinie'', [''named'', ''integrate'', ''function''],
1.27 [''diff'', ''integration'', ''named''])
1.28 - [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun] \<comment> \<open>PROG string\<close>
1.29 + [REAL (rhs N__N), REAL v_v, REAL_REAL id_fun]
1.30 in [Q__Q, M__M, N__N, B__B])"
1.31 setup \<open>KEStore_Elems.add_mets
1.32 [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
1.33 @@ -445,6 +446,8 @@
1.34 " eq_u = (Substitute [su_b]) eq_u " ^
1.35 " in (Rewrite_Set ''norm_Rational'' False) eq_u) "*))]
1.36 \<close>
1.37 -
1.38 +ML \<open>
1.39 +\<close> ML \<open>
1.40 +\<close>
1.41 end
1.42
2.1 --- a/src/Tools/isac/ProgLang/Atools.thy Thu May 30 12:39:13 2019 +0200
2.2 +++ b/src/Tools/isac/ProgLang/Atools.thy Sat Jun 01 11:09:19 2019 +0200
2.3 @@ -6,12 +6,18 @@
2.4 theory Atools imports Descript Script
2.5 begin
2.6
2.7 +subsection \<open>preparation to build up a program from rules\<close>
2.8 +
2.9 partial_function (tailrec) auto_generated :: "'z \<Rightarrow> 'z"
2.10 where "auto_generated t_t = t_t"
2.11 partial_function (tailrec) auto_generated_inst :: "'z \<Rightarrow> real \<Rightarrow> 'z"
2.12 where "auto_generated_inst t_t v = t_t"
2.13 +
2.14 +subsection \<open>use preparation\<close>
2.15 ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
2.16
2.17 +subsection \<open>consts & axiomatization\<close>
2.18 +
2.19 consts
2.20
2.21 Arbfix :: "real"
2.22 @@ -22,7 +28,7 @@
2.23 occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
2.24
2.25 pow :: "[real, real] => real" (infixr "^^^" 80)
2.26 -(* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
2.27 + (* ~~~ power doesn't allow Free("2",real) ^ Free("2",nat)
2.28 ~~~~ ~~~~ ~~~~ ~~~*)
2.29 (*WN0603 at FE-interface encoded strings to '^',
2.30 see 'fun encode', fun 'decode'*)
2.31 @@ -78,11 +84,11 @@
2.32 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
2.33
2.34
2.35 +subsection \<open>Coding standards\<close>
2.36 text \<open>copy from doc/math-eng.tex WN.28.3.03
2.37 WN071228 extended\<close>
2.38
2.39 -section \<open>Coding standards\<close>
2.40 -subsection \<open>Identifiers\<close>
2.41 +subsubsection \<open>Identifiers\<close>
2.42 text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc. However, all the cases (1)..(4) require different typing for one and the same identifier {\tt probe} which is impossible, and actually leads to strange errors (for instance (1) is used as string, except in a script addressing a Subproblem).
2.43
2.44 This are the preliminary rules for naming identifiers>
2.45 @@ -96,7 +102,7 @@
2.46 \end{description}
2.47 %WN071228 extended\<close>
2.48
2.49 -subsection \<open>Rule sets\<close>
2.50 +subsubsection \<open>Rule sets\<close>
2.51 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML where it can be viewed using the knowledge browsers.
2.52
2.53 There are rulesets visible to the student, and there are rulesets visible (in general) only for math authors. There are also rulesets which {\em must} exist for {\em each} theory; these contain the identifier of the respective theory (including all capital letters) as indicated by {\it Thy} below.
2.54 @@ -125,11 +131,10 @@
2.55 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
2.56 \<close>
2.57
2.58 +subsection \<open>evaluation of numerals and special predicates on the meta-level\<close>
2.59 ML \<open>
2.60 val thy = @{theory};
2.61
2.62 -(** evaluation of numerals and special predicates on the meta-level **)
2.63 -
2.64 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
2.65
2.66 (*("occurs_in", ("Atools.occurs'_in", eval_occurs_in ""))*)
2.67 @@ -415,9 +420,8 @@
2.68
2.69 \<close>
2.70
2.71 +subsection \<open>evaluation on the meta-level\<close>
2.72 ML \<open>
2.73 -(** evaluation on the metalevel **)
2.74 -
2.75 (*. evaluate HOL.divide .*)
2.76 (*("DIVIDE" ,("Rings.divide_class.divide" ,eval_cancel "#divide_e"))*)
2.77 fun eval_cancel (thmid:string) "Rings.divide_class.divide" (t as
2.78 @@ -512,9 +516,10 @@
2.79 HOLogic.Trueprop $ (TermC.mk_equality (p, sum)))
2.80 end
2.81 | eval_boollist2sum _ _ _ _ = NONE;
2.82 +\<close>
2.83
2.84 -
2.85 -
2.86 +subsection \<open>rule sets, for evaluating list-expressions in scripts, etc\<close>
2.87 +ML \<open>
2.88 local
2.89
2.90 open Term;
2.91 @@ -524,10 +529,6 @@
2.92 fun term_ordI (_: Rule.subst) uv = Term_Ord.term_ord uv;
2.93 end;
2.94
2.95 -
2.96 -(** rule set, for evaluating list-expressions in scripts 8.01.02 **)
2.97 -
2.98 -
2.99 val list_rls = Rule.append_rls "list_rls" list_rls
2.100 [Rule.Calc ("Groups.times_class.times",eval_binop "#mult_"),
2.101 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
2.102 @@ -667,6 +668,7 @@
2.103 *)
2.104 "******* Atools.ML end *******";
2.105 \<close>
2.106 +subsection \<open>write to KEStore: calcs, rule-sets\<close>
2.107 setup \<open>KEStore_Elems.add_calcs
2.108 [("occurs_in",("Atools.occurs'_in", eval_occurs_in "#occurs_in_")),
2.109 ("some_occur_in",
3.1 --- a/src/Tools/isac/TODO.thy Thu May 30 12:39:13 2019 +0200
3.2 +++ b/src/Tools/isac/TODO.thy Sat Jun 01 11:09:19 2019 +0200
3.3 @@ -13,6 +13,13 @@
3.4 String constants have already bee introduced to old string-programs.
3.5 Shifting this program code into partial_function reveals further issues:
3.6 \begin{itemize}
3.7 +\item Biegelinie.thy was already broken after isabisac15, but never noticed.
3.8 + Switch from script to partial_function has it broken further,
3.9 + mostly due to generalisation of handling of meths which extend the model of a probl.
3.10 + !Check if (*CURRENT*) error is due to "switch from Script to partial_function" 4035ec339062 ?
3.11 + OR ?due to "failed trial to generalise handling of meths
3.12 + which extend the model of a probl " 98298342fb6d
3.13 +\item
3.14 \item Diff.thy
3.15 \begin{itemize}
3.16 \item differentiateX --> differentiate after removal of script-constant
3.17 @@ -68,9 +75,9 @@
3.18 \end{itemize}
3.19 \item \item abstract specify + nxt_specif to common aux-funs;
3.20 see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
3.21 -\item \item
3.22 -\item \item
3.23 -\item \item
3.24 +\item
3.25 +\item
3.26 +\item
3.27 \begin{itemize}
3.28 \item
3.29 \begin{itemize}
4.1 --- a/src/Tools/isac/xmlsrc/thy-hierarchy.sml Thu May 30 12:39:13 2019 +0200
4.2 +++ b/src/Tools/isac/xmlsrc/thy-hierarchy.sml Sat Jun 01 11:09:19 2019 +0200
4.3 @@ -1,4 +1,5 @@
4.4 -(* export theory-data "thehier" to xml
4.5 +(* title: "xmlsrc/thy-hierarchy.sml"
4.6 + export theory-data "thehier" to xml
4.7 author: Walther Neuper 0601
4.8 (c) isac-team
4.9 *)
4.10 @@ -11,7 +12,9 @@
4.11 val fun_ids = Specify.get_fun_ids thy
4.12 in
4.13 filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy
4.14 - andalso not (thm contains_one_of fun_ids))
4.15 + andalso not (thm contains_one_of fun_ids)
4.16 + andalso not (Celem.thmID_of_derivation_name' thm = "mono"))
4.17 + (* created in Biegelinie by partial_function ^^^^^^*)
4.18 (map snd (Global_Theory.all_thms_of thy false))
4.19 end
4.20
5.1 --- a/test/Tools/isac/Interpret/ptyps.sml Thu May 30 12:39:13 2019 +0200
5.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Sat Jun 01 11:09:19 2019 +0200
5.3 @@ -553,5 +553,5 @@
5.4 "-------- fun get_fun_ids ----------------------------------------------------";
5.5 val met_fun_ids = get_fun_ids @{theory Biegelinie};
5.6 if map fst (get_fun_ids @{theory Biegelinie}) =
5.7 - ["Biegelinie.Biegelinie2Script", "Biegelinie.Belastung2BiegelScript",
5.8 - "Biegelinie.SetzeRandbedScript"] then () else error "get_fun_ids changed"
5.9 + ["Biegelinie.function_to_equality", "Biegelinie.biegelinie", "Biegelinie.belastung_zu_biegelinie",
5.10 + "Biegelinie.setzte_randbedingungen"] then () else error "get_fun_ids changed"
6.1 --- a/test/Tools/isac/Interpret/script.sml Thu May 30 12:39:13 2019 +0200
6.2 +++ b/test/Tools/isac/Interpret/script.sml Sat Jun 01 11:09:19 2019 +0200
6.3 @@ -616,7 +616,7 @@
6.4 "~~~~~ fun init_scrstate , args:"; val (thy, itms, metID) = (assoc_thy thy, meth, metID);
6.5 val (ScrState st, ctxt, Prog _) = init_scrstate thy itms metID;
6.6 if scrstate2str st =
6.7 -"([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(id_abl, dy)\",\"\n(b, y)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\"], [], NONE, \n??.empty, Safe, true)"
6.8 +"([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], NONE, \n??.empty, Safe, true)"
6.9 then () else error "init_scrstate changed for Biegelinie";
6.10
6.11 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
7.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Thu May 30 12:39:13 2019 +0200
7.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Sat Jun 01 11:09:19 2019 +0200
7.3 @@ -1,10 +1,12 @@
7.4 -(* biegelinie-3.sml
7.5 +(* "Knowledge/biegelinie-3.sml"
7.6 author: Walther Neuper 190515
7.7 (c) due to copyright terms
7.8 *)
7.9 "table of contents -----------------------------------------------";
7.10 "-----------------------------------------------------------------";
7.11 "----------- see biegelinie-1.sml---------------------------------";
7.12 +(* problems with generalised handling of meths which extend the model of a probl
7.13 + since 98298342fb6d: wait for review of whole model-specify phase *)
7.14 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
7.15 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
7.16 "-----------------------------------------------------------------";
7.17 @@ -324,7 +326,18 @@
7.18 (*----------- 80 -----------*)
7.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.20 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.21 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.22 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.23 +if p = ([2, 1], Pbl) andalso
7.24 + f = PpcKF (Problem [], {Find = [Incompl "equality"], Given = [Incompl "functionEq", Incompl "substitution"], Relate = [], Where = [], With = []})
7.25 +then
7.26 + case nxt of
7.27 + ("Add_Given", Add_Given "functionEq (hd [])") => ((*here is an error in partial_function*))
7.28 + | _ => error "me biegelinie changed 1"
7.29 +else error "me biegelinie changed 2";
7.30 +
7.31 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.32 +nxt;(* = ("Tac ", Tac "[error] appl_add: is_known: seek_oridts: input ('substitution (NTH (1 + -4) [])') not found in oris (typed)")*)
7.33 +(*----- due to problems with generalised handling of meths which extend the model of a probl
7.34 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.35 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.36 (*----------- 90 -----------*)
7.37 @@ -373,7 +386,8 @@
7.38 | _ => error "Bsp.7.70 me changed 1")
7.39 | _ => error "Bsp.7.70 me changed 2"
7.40 else error "Bsp.7.70 me changed 3";
7.41 -
7.42 +-----*)
7.43 +(* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
7.44
7.45 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
7.46 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
7.47 @@ -421,6 +435,15 @@
7.48 val ip = get_pos 1 1;
7.49 val (Form f, tac, asms) = pt_extract (pt, ip);
7.50
7.51 +if ip = ([2, 1, 1], Frm) andalso
7.52 +term2str f = "hd []"
7.53 +then
7.54 + case tac of
7.55 + SOME Empty_Tac => ()
7.56 + | _ => error "ERROR biegel.7.70 changed 1"
7.57 +else error "ERROR biegel.7.70 changed 2";
7.58 +
7.59 +(*----- this state has been reached shortly after 98298342fb6d:
7.60 if ip = ([3, 8, 1], Res) andalso
7.61 term2str f = "[-1 * c_4 / -1 = 0,\n (6 * c_4 * EI + 6 * L * c_3 * EI + -3 * L ^^^ 2 * c_2 + -1 * L ^^^ 3 * c) /\n (6 * EI) =\n L ^^^ 4 * q_0 / (-24 * EI),\n c_2 = 0, c_2 + L * c = L ^^^ 2 * q_0 / 2]"
7.62 then
7.63 @@ -428,3 +451,4 @@
7.64 SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()
7.65 | _ => error "ERROR biegel.7.70 changed 1"
7.66 else error "ERROR biegel.7.70 changed 2";
7.67 +*)
7.68 \ No newline at end of file
8.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu May 30 12:39:13 2019 +0200
8.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Sat Jun 01 11:09:19 2019 +0200
8.3 @@ -1,4 +1,5 @@
8.4 -(* Title: partial fraction decomposition
8.5 +(* Title: "Knowledge/partial_fractions.sml"
8.6 + partial fraction decomposition
8.7 Author: Jan Rocnik
8.8 (c) due to copyright terms
8.9 *)
9.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Thu May 30 12:39:13 2019 +0200
9.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Sat Jun 01 11:09:19 2019 +0200
9.3 @@ -6,70 +6,21 @@
9.4 "-----------------------------------------------------------------";
9.5 "table of contents -----------------------------------------------";
9.6 "-----------------------------------------------------------------";
9.7 -"-------- test auto-generated script '(Repeat (Calculate times))'-";
9.8 "-------- test the same called by interSteps norm_Poly -----------";
9.9 "-------- test the same called by interSteps norm_Rational -------";
9.10 "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
9.11 -"-------- how to stepwise construct Scripts -------";(*TODO remove -- partial_function is easier*)
9.12 "-------- distinguish input to Model -----------------------------------------";
9.13 "-------- fun subpbl, fun pblterm --------------------------------------------";
9.14 "-------- fun stacpbls, fun subst_stacexpr -----------------------------------";
9.15 "-------- fun is_calc, fun op_of_calc ----------------------------------------";
9.16 "-------- fun rule2stac, fun rule2stac_inst ----------------------------------";
9.17 "-------- fun op @@ ----------------------------------------------------------";
9.18 -"-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";
9.19 -"-------- Handle Var from parsing by partial_function ------------------------";
9.20 -"-------- Compare program terms: from old parsing | from partial_function ----";
9.21 "-------- fun get_fun_id -----------------------------------------------------";
9.22 "-------- fun rules2scr_Rls --------------------------------------------------";
9.23 "-----------------------------------------------------------------------------";
9.24 "-----------------------------------------------------------------------------";
9.25 "-----------------------------------------------------------------------------";
9.26
9.27 -
9.28 -"-------- test auto-generated script '(Repeat (Calculate times))'-";
9.29 -"-------- test auto-generated script '(Repeat (Calculate times))'-";
9.30 -"-------- test auto-generated script '(Repeat (Calculate times))'-";
9.31 -val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
9.32 -writeln(term2str auto_script);
9.33 -atomty auto_script;
9.34 -
9.35 -show_mets();
9.36 -val {scr = Prog parsed_script,...} = get_met ["Test","test_interSteps_1"];
9.37 -writeln(term2str parsed_script);
9.38 -atomty parsed_script;
9.39 -
9.40 -(*the structure of the auto-gen. script is interpreted correctly*)
9.41 -reset_states ();
9.42 -CalcTree
9.43 -[(["Term (b + a - b)",(*this is Schalk 299b*)
9.44 - "normalform N"],
9.45 - ("Poly",["polynomial","simplification"],
9.46 - ["Test","test_interSteps_1"]))];
9.47 -Iterator 1;
9.48 -moveActiveRoot 1;
9.49 -autoCalculate 1 CompleteCalcHead;
9.50 -
9.51 -fetchProposedTactic 1 (*..Apply_Method*);
9.52 -autoCalculate 1 (Step 1);
9.53 -getTactic 1 ([1], Frm) (*still empty*);
9.54 -
9.55 -fetchProposedTactic 1 (*discard_minus_*);
9.56 -autoCalculate 1 (Step 1);
9.57 -
9.58 -fetchProposedTactic 1 (*order_add_rls_*);
9.59 -autoCalculate 1 (Step 1);
9.60 -
9.61 -fetchProposedTactic 1 (*collect_numerals_*);
9.62 -autoCalculate 1 (Step 1);
9.63 -
9.64 -autoCalculate 1 CompleteCalc;
9.65 -
9.66 -val ((pt,p),_) = get_calc 1; show_pt pt;
9.67 -if existpt' ([1], Frm) pt then ()
9.68 -else error "scrtools.sml: test-script test_interSteps_1 doesnt work";
9.69 -
9.70 -
9.71 "-------- test the same called by interSteps norm_Poly -----------";
9.72 "-------- test the same called by interSteps norm_Poly -----------";
9.73 "-------- test the same called by interSteps norm_Poly -----------";
9.74 @@ -225,57 +176,11 @@
9.75 if contain_bdv (get_rules rls) then ()
9.76 else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
9.77
9.78 -two_scr_arg auto_script;
9.79 +if terms2str (formal_args auto_script) = "[\"t_t\",\"v\"]"
9.80 +then () else error "formal_args of auto-gen.script changed";
9.81 init_istate (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules"))
9.82 (str2term "someTermWithBdv");
9.83
9.84 -"-------- how to stepwise construct Scripts ----------------------";
9.85 -"-------- how to stepwise construct Scripts ----------------------";
9.86 -"-------- how to stepwise construct Scripts ----------------------";
9.87 -val thy = @{theory "Rational"};
9.88 -(*no trailing _*)
9.89 -val p1 = parse thy (
9.90 -"Script SimplifyScript (t_t::real) = " ^
9.91 -" (Rewrite_Set discard_minus False " ^
9.92 -" t_t)");
9.93 -
9.94 -(*required (): (Rewrite_Set discard_minus False)*)
9.95 -val p2 = parse thy (
9.96 -"Script SimplifyScript (t_t::real) = " ^
9.97 -" (Rewrite_Set discard_minus False " ^
9.98 -" t_t)");
9.99 -
9.100 -val p3 = parse thy (
9.101 -"Script SimplifyScript (t_t::real) = " ^
9.102 -" ((Rewrite_Set discard_minus False) " ^
9.103 -" t_t)");
9.104 -
9.105 -val p4 = parse thy (
9.106 -"Script SimplifyScript (t_t::real) = " ^
9.107 -" ((Rewrite_Set discard_minus False) " ^
9.108 -" t_t)");
9.109 -
9.110 -val p5 = parse thy (
9.111 -"Script SimplifyScript (t_t::real) = " ^
9.112 -" ((Try (Rewrite_Set discard_minus False) " ^
9.113 -" Try (Rewrite_Set discard_parentheses False)) " ^
9.114 -" t_t)");
9.115 -
9.116 -val p6 = parse thy (
9.117 -"Script SimplifyScript (t_t::real) = " ^
9.118 -" ((Try (Rewrite_Set discard_minus False) @@ " ^
9.119 -" Try (Rewrite_Set rat_mult_poly False) @@ " ^
9.120 -" Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ " ^
9.121 -" Try (Rewrite_Set cancel_p_rls False) @@ " ^
9.122 -" (Repeat " ^
9.123 -" ((Try (Rewrite_Set add_fractions_p_rls False) @@ " ^
9.124 -" Try (Rewrite_Set rat_mult_div_pow False) @@ " ^
9.125 -" Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^
9.126 -" Try (Rewrite_Set cancel_p_rls False) @@ " ^
9.127 -" Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^
9.128 -" Try (Rewrite_Set discard_parentheses False)) " ^
9.129 -" t_t)"
9.130 -);
9.131
9.132 "-------- distinguish input to Model -----------------------------------------";
9.133 "-------- distinguish input to Model -----------------------------------------";
9.134 @@ -420,189 +325,12 @@
9.135 "Try (Repeat (Rewrite ''risolate_root_div'' False))"
9.136 then () else error "fun @@ changed"
9.137
9.138 -"-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";
9.139 -"-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";
9.140 -"-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";
9.141 -(* meth for Minisubpbl ["Test", "squ-equ-test-subpbl1"] *)
9.142 -val prog_str_'''' = (* string constants: the intermediate version before partial_function *)
9.143 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
9.144 - " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@ " ^
9.145 - " (Try (Rewrite_Set ''Test_simplify'' False))) e_e; " ^
9.146 - " (L_L::bool list) = " ^
9.147 - " (SubProblem (''TestX'', " ^
9.148 - " [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^
9.149 - " [''Test'', ''solve_linear'']) " ^
9.150 - " [BOOL e_e, REAL v_v]) " ^
9.151 - " in Check_elementwise L_L {(v_v::real). Assumptions}) ";
9.152 -val prog_str_Free = (* Free varibles: the version up to now *)
9.153 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
9.154 - " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
9.155 - " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
9.156 - " (L_L::bool list) = " ^
9.157 - " (SubProblem (TestX, " ^
9.158 - " [LINEAR, univariate, equation, test], " ^
9.159 - " [Test, solve_linear]) " ^
9.160 - " [BOOL e_e, REAL v_v]) " ^
9.161 - " in Check_elementwise L_L {(v_v::real). Assumptions}) "
9.162 -
9.163 -(* term with string constants *)
9.164 -val prog_'''' = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory})) prog_str_''''
9.165 -val Const ("Test.Solve'_root'_equation", _) $
9.166 - Free ("e_e", _) $ Free ("v_v", _) $
9.167 - (Const ("HOL.Let", _) $
9.168 - (Const ("Script.Seq", _) $
9.169 - (Const ("Script.Try", _) $
9.170 - (Const ("Script.Rewrite'_Set", _) $
9.171 - norm_equation_'''' $ Const ("HOL.False", _))) $
9.172 - (Const ("Script.Try", _) $
9.173 - (Const ("Script.Rewrite'_Set", _) $
9.174 - Test_simplify_'''' $ Const ("HOL.False", _))) $
9.175 - Free ("e_e", _)) $
9.176 - Abs ("e_e", _,
9.177 - Const ("HOL.Let", _) $
9.178 - (Const ("Script.SubProblem", _) $
9.179 - (Const ("Product_Type.Pair", _) $ TestX_'''' $
9.180 - (Const ("Product_Type.Pair", _) $
9.181 - pblkey_'''' $ metkey_'''')) $
9.182 - args) $
9.183 - Abs ("L_L", _,
9.184 - Const ("Script.Check'_elementwise", _) $ Free _ $ (_ $ _)))) = prog_''''
9.185 -;
9.186 -(* term with Free varibles *)
9.187 -val prog_Free = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory})) prog_str_Free
9.188 -val Const ("Test.Solve'_root'_equation", _) $
9.189 - Free ("e_e", _) $ Free ("v_v", _) $
9.190 - (Const ("HOL.Let", _) $
9.191 - (Const ("Script.Seq", _) $
9.192 - (Const ("Script.Try", _) $
9.193 - (Const ("Script.Rewrite'_Set", _) $
9.194 - norm_equation_Free $ Const ("HOL.False", _))) $
9.195 - (Const ("Script.Try", _) $
9.196 - (Const ("Script.Rewrite'_Set", _) $
9.197 - Test_simplify_Free $ Const ("HOL.False", _))) $
9.198 - Free ("e_e", _)) $
9.199 - Abs ("e_e", _,
9.200 - Const ("HOL.Let", _) $
9.201 - (Const ("Script.SubProblem", _) $
9.202 - (Const ("Product_Type.Pair", _) $ TestX_Free $
9.203 - (Const ("Product_Type.Pair", _) $
9.204 - pblkey_Free $ metkey_Free)) $
9.205 - args) $
9.206 - Abs ("L_L", _,
9.207 - Const ("Script.Check'_elementwise", _) $ Free _ $ (_ $ _)))) = prog_Free
9.208 -;
9.209 -(* compare term with string constants and term with Free varibles *)
9.210 -if HOLogic.dest_string norm_equation_'''' = "norm_equation" then () else error "dest_string 1";
9.211 -(* --------------------- string constants = Free varibles *)
9.212 -if HOLogic.dest_string norm_equation_'''' = Term.term_name norm_equation_Free then () else error "";
9.213 -if HOLogic.dest_string Test_simplify_'''' = Term.term_name Test_simplify_Free then () else error "";
9.214 -if HOLogic.dest_string TestX_'''' = Term.term_name TestX_Free then () else error "dest_string 2";
9.215 -
9.216 -if (pblkey_'''' |> HOLogic.dest_list |> map HOLogic.dest_string) =
9.217 - ["LINEAR", "univariate", "equation", "test"] then () else error "dest_string 3";
9.218 -(* --------------------- string constants = Free varibles *)
9.219 -if (pblkey_'''' |> HOLogic.dest_list |> map HOLogic.dest_string) =
9.220 - (pblkey_Free |> HOLogic.dest_list |> map Term.term_name) then () else error "dest_string 4";
9.221 -if (metkey_'''' |> HOLogic.dest_list |> map HOLogic.dest_string) =
9.222 - (metkey_Free |> HOLogic.dest_list |> map Term.term_name) then () else error "dest_string 5";
9.223 -
9.224 -"-------- Handle Var from parsing by partial_function ------------------------";
9.225 -"-------- Handle Var from parsing by partial_function ------------------------";
9.226 -"-------- Handle Var from parsing by partial_function ------------------------";
9.227 -(* (1) parsing proprietary as used up to now *)
9.228 -val prog_str_'''' =
9.229 - "xxx e_e = (let e_e = (Rewrite_Set ''yyy'' False) e_e in [e_e])"
9.230 -val prog_'''' = ((*TermC.inst_abs o*) Thm.term_of o the o (TermC.parse @{theory})) prog_str_''''
9.231 -(*Output: val prog_'''' = ... $ (Const ("HOL.Let", "bool... )... $ Free ("e_e", "bool")) $ ...*)
9.232 -
9.233 -(* (2) parsing by funpack: take the definition from test/../ProgLang/scrtools.thy *)
9.234 -val prog_part = (HOLogic.dest_Trueprop o Thm.prop_of) @{thm simplify.simps}
9.235 -(*Output: val prog_part = ... $ (Const ("HOL.Let", "bool... )... $ Var (("e_e", 0), "bool")) $ ...*)
9.236 -;
9.237 -Logic.unvarify_global: term -> term
9.238 -;
9.239 -val prog_part = (Logic.unvarify_global o HOLogic.dest_Trueprop o Thm.prop_of) @{thm simplify.simps};
9.240 -(*val prog_part = ... $ (Const ("HOL.Let", "bool... )... $ Var (("e_e", 0), "bool")) $ ...*)
9.241 -
9.242 -(* (3) compare (1)..(2) *)
9.243 -if prog_'''' = prog_part then () else error "appl of Logic.unvarify_global changed"
9.244 -
9.245 -"-------- Compare program terms: from old parsing | from partial_function ----";
9.246 -"-------- Compare program terms: from old parsing | from partial_function ----";
9.247 -"-------- Compare program terms: from old parsing | from partial_function ----";
9.248 -(* meth for Minisubpbl ["Test", "squ-equ-test-subpbl1"] *)
9.249 -
9.250 -(* (1) parsing proprietary as used up to now *)
9.251 -val prog_str_'''' = (* string constants: the intermediate version before partial_function *)
9.252 - "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
9.253 - " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@ " ^
9.254 - " (Try (Rewrite_Set ''Test_simplify'' False))) e_e; " ^
9.255 - " (L_L::bool list) = " ^
9.256 - " (SubProblem (''TestX'', " ^
9.257 - " [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^
9.258 - " [''Test'', ''solve_linear'']) " ^
9.259 - " [BOOL e_e, REAL v_v]) " ^
9.260 - " in Check_elementwise L_L {(v_v::real). Assumptions}) ";
9.261 -val prog_'''' = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory})) prog_str_''''
9.262 -
9.263 -(* body_of ---> src/../scrtools.sml for test with old parsing *)
9.264 -fun body_of_'''' (_ $ body) = body
9.265 - | body_of_'''' t = raise TERM ("body_of", [t])
9.266 -
9.267 -val body_'''' = body_of_'''' prog_'''';
9.268 -term2str body_''''; (* with TermC.inst_abs:
9.269 - "let e_ea =\n (Try (Rewrite_Set ''norm_equation'' False) @@\n Try (Rewrite_Set ''Test_simplify'' False))\n e_e;\n L_La =\n SubProblem\n (''TestX'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n [''Test'', ''solve_linear''])\n [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}":
9.270 -------------------------> e_e; Free ("e_e", "bool"))
9.271 -*)
9.272 -
9.273 -(* formal_args in src/../scrtools.sml*)
9.274 -fun formal_args_'''' scr = (fst o split_last o snd o strip_comb) scr;
9.275 -
9.276 -val args_'''' = formal_args_'''' prog_'''';
9.277 -case args_'''' of [Free ("e_e", _), Free ("v_v", _)] => ()
9.278 -| _ => error "formal_args";
9.279 -
9.280 -(* (2) parsing by funpack: take the definition from test/../ProgLang/scrtools.thy *)
9.281 -val prog_part = Thm.prop_of @{thm minisubpbl.simps}
9.282 -
9.283 -(* body_of ---> src/../scrtools.sml BEFORE above, new body_of *)
9.284 -fun body_of_part t = (t
9.285 - |> HOLogic.dest_Trueprop
9.286 - |> HOLogic.dest_eq
9.287 - |> snd
9.288 - |> Logic.unvarify_global
9.289 - |> TermC.inst_abs)
9.290 -handle TERM _ => raise TERM ("body_of", [t])
9.291 -
9.292 -val body_part = body_of_part prog_part;
9.293 -term2str body_part; (* with TermC.inst_abs, without:
9.294 - "let e_ea =\n (Try (Rewrite_Set ''norm_equation'' False) @@\n Try (Rewrite_Set ''Test_simplify'' False))\n ?e_e;\n L_La =\n SubProblem\n (''TestX'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n [''Test'', ''solve_linear''])\n [BOOL e_e, REAL ?v_v]\nin Check_elementwise L_L {v_v. Assumptions}":
9.295 -------------------------> ?e_e; Var (("e_e", 0), "bool"))
9.296 -*)
9.297 -
9.298 -(* formal_args ---> src/../scrtools.sml BEFORE old formal_args *)
9.299 -fun formal_args_part prog = (prog
9.300 - |> HOLogic.dest_Trueprop
9.301 - |> HOLogic.dest_eq
9.302 - |> fst
9.303 - |> Logic.unvarify_global
9.304 - |> strip_comb
9.305 - |> snd
9.306 -)
9.307 -handle TERM _ => raise TERM ("formal_args", [t])
9.308 -
9.309 -val args_part = formal_args_part prog_part;
9.310 -
9.311 -(* (3) compare (1)..(2) *)
9.312 -if body_'''' = body_part then () else error "body_of changed";
9.313 -if args_'''' = args_part then () else error "formal_args changed"
9.314 -
9.315 "-------- fun get_fun_id -----------------------------------------------------";
9.316 "-------- fun get_fun_id -----------------------------------------------------";
9.317 "-------- fun get_fun_id -----------------------------------------------------";
9.318 (* fun_id is nested into arguments, compare ... *)
9.319 val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
9.320 - (((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) =
9.321 + (((((((Const (const_id, const_typ) $ _) $ _) $ _) $ _) $ _) $ _) $ _) $ _) =
9.322 Thm.prop_of @{thm biegelinie.simps};
9.323 (* ... to: *)
9.324 val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
9.325 @@ -613,12 +341,14 @@
9.326 val Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $
9.327 nested $ _) =
9.328 Thm.prop_of @{thm biegelinie.simps};
9.329 -val (((((Const ("Biegelinie.biegelinie", _) $
9.330 - Var (("l", 0), _)) $
9.331 - Var (("q", 0), _)) $
9.332 - Var (("v", 0), _)) $
9.333 - Var (("b", 0), _)) $
9.334 - Var (("s", 0), _)) = nested;
9.335 +val (Const ("Biegelinie.biegelinie", _) $
9.336 + Var (("l", 0), _) $
9.337 + Var (("q", 0), _) $
9.338 + Var (("v", 0), _) $
9.339 + Var (("b", 0), _) $
9.340 + Var (("s", 0), _) $
9.341 + Var (("vs", 0), _) $
9.342 + Var (("id_abl", 0), _)) = nested;
9.343 strip_comb nested;
9.344 (*val it =
9.345 (Const ("Biegelinie.biegelinie", "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool")
9.346 @@ -627,10 +357,10 @@
9.347 Var (("b", 0), "real \<Rightarrow> real"), Var (("s", 0), "bool list")]):
9.348 term * term list*)
9.349
9.350 -case get_fun_id (Thm.prop_of @{thm biegelinie.simps}) of
9.351 +case get_fun_id (prep_program @{thm biegelinie.simps}) of
9.352 ("Biegelinie.biegelinie", _) => ()
9.353 | _ => error "get_fun_id changed";
9.354 -case get_fun_id (Thm.prop_of @{thm simplify.simps}) of
9.355 +case get_fun_id (prep_program @{thm simplify.simps}) of
9.356 ("PolyMinus.simplify", _) => ()
9.357 | _ => error "get_fun_id changed";
9.358
10.1 --- a/test/Tools/isac/ProgLang/termC.sml Thu May 30 12:39:13 2019 +0200
10.2 +++ b/test/Tools/isac/ProgLang/termC.sml Sat Jun 01 11:09:19 2019 +0200
10.3 @@ -739,4 +739,4 @@
10.4 val {scr = Prog original, ...} = get_met ["Equation","fromFunction"];
10.5 val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $ scr'_body = scr'
10.6 ;
10.7 -if scr'_body = Lucin.body_of original then () else error "inst_abs changed";
10.8 +if scr'_body = LTool.body_of original then () else error "inst_abs changed";
11.1 --- a/test/Tools/isac/Test_Some.thy Thu May 30 12:39:13 2019 +0200
11.2 +++ b/test/Tools/isac/Test_Some.thy Sat Jun 01 11:09:19 2019 +0200
11.3 @@ -67,10 +67,998 @@
11.4 "~~~~~ fun xxx , args:"; val () = ();
11.5 \<close>
11.6
11.7 -section \<open>===================================================================================\<close>
11.8 +section \<open>================= "Knowledge/partial_fractions.sml" ============================\<close>
11.9 ML \<open>
11.10 "~~~~~ fun xxx , args:"; val () = ();
11.11 \<close> ML \<open>
11.12 +(* Title: partial fraction decomposition
11.13 + Author: Jan Rocnik
11.14 + (c) due to copyright terms
11.15 +*)
11.16 +
11.17 +"--------------------------------------------------------";
11.18 +"table of contents --------------------------------------";
11.19 +"--------------------------------------------------------";
11.20 +"----------- why helpless here ? ------------------------";
11.21 +"----------- why not nxt = Model_Problem here ? ---------";
11.22 +"----------- fun factors_from_solution ------------------";
11.23 +"----------- Logic.unvarify_global ----------------------";
11.24 +"----------- eval_drop_questionmarks --------------------";
11.25 +"----------- = me for met_partial_fraction --------------";
11.26 +"----------- autoCalculate for met_partial_fraction -----";
11.27 +"----------- progr.vers.2: check erls for multiply_ansatz";
11.28 +"----------- progr.vers.2: improve program --------------";
11.29 +"--------------------------------------------------------";
11.30 +"--------------------------------------------------------";
11.31 +"--------------------------------------------------------";
11.32 +
11.33 +
11.34 +"----------- why helpless here ? ------------------------";
11.35 +"----------- why helpless here ? ------------------------";
11.36 +"----------- why helpless here ? ------------------------";
11.37 +\<close> ML \<open>
11.38 +val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
11.39 + "stepResponse (x[n::real]::bool)"];
11.40 +val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
11.41 + ["SignalProcessing","Z_Transform","Inverse"]);
11.42 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
11.43 +\<close> ML \<open>
11.44 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
11.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
11.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
11.47 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
11.48 +\<close> ML \<open>
11.49 +(*CURRENT*)(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Specify_Method ["SignalProcessing", "Z_Transform", "Inverse"])*)
11.50 +\<close> ML \<open>
11.51 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
11.52 +(*CURRENT*)(*ERROR in creating the environment from formal args. of partial_function "HOL.eq"
11.53 +and the actual args., ie. items of the guard of "["SignalProcessing","Z_Transform","Inverse"]" by "assoc_by_type":
11.54 +formal arg "TYPE('a)" doesn't mach an actual arg.
11.55 +with:
11.56 +3 formal args: ["TYPE('a)","X_eq","z"]
11.57 +2 actual args: ["X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))","x [n]"]*)
11.58 +\<close> ML \<open>
11.59 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
11.60 +val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
11.61 +\<close> ML \<open>
11.62 +"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
11.63 +val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
11.64 +val (pt, p) = ptp;
11.65 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
11.66 + (p, ((pt, e_pos'),[]));
11.67 +val pIopt = get_pblID (pt,ip);
11.68 +ip = ([],Res); "false";
11.69 +tacis; " = []";
11.70 +pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
11.71 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
11.72 +(*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
11.73 + THIS MEANS: replace no_meth by [no_meth] in Script.*)
11.74 +(*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
11.75 +(*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
11.76 +
11.77 +\<close> ML \<open>
11.78 +"----------- why not nxt = Model_Problem here ? ---------";
11.79 +"----------- why not nxt = Model_Problem here ? ---------";
11.80 +"----------- why not nxt = Model_Problem here ? ---------";
11.81 +val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt''';
11.82 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
11.83 +val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
11.84 +val (pt, p) = ptp;
11.85 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
11.86 + (p, ((pt, e_pos'),[]));
11.87 +val pIopt = get_pblID (pt,ip);
11.88 +ip = ([],Res); " = false";
11.89 +tacis; " = []";
11.90 +pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);
11.91 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";
11.92 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
11.93 +nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
11.94 +This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form.
11.95 +See TODO.txt
11.96 +*)
11.97 +
11.98 +\<close> ML \<open>
11.99 +"----------- fun factors_from_solution ------------------";
11.100 +"----------- fun factors_from_solution ------------------";
11.101 +"----------- fun factors_from_solution ------------------";
11.102 +val ctxt = Proof_Context.init_global @{theory Isac};
11.103 +val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
11.104 +val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
11.105 +if term2str t' =
11.106 + "factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)"
11.107 +then () else error "factors_from_solution broken";
11.108 +
11.109 +\<close> ML \<open>
11.110 +"----------- Logic.unvarify_global ----------------------";
11.111 +"----------- Logic.unvarify_global ----------------------";
11.112 +"----------- Logic.unvarify_global ----------------------";
11.113 +val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global
11.114 +val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global
11.115 +
11.116 +val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the;
11.117 +val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
11.118 +
11.119 +val test = HOLogic.mk_binop "Groups.plus_class.plus"
11.120 + (HOLogic.mk_binop "Rings.divide_class.divide" (A_var, denom1),
11.121 + HOLogic.mk_binop "Rings.divide_class.divide" (B_var, denom2));
11.122 +
11.123 +if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
11.124 + else error "HOLogic.mk_binop broken ?";
11.125 +
11.126 +(* Logic.unvarify_global test
11.127 +---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"
11.128 +thus we need another fun var2free in termC.sml*)
11.129 +
11.130 +\<close> ML \<open>
11.131 +"----------- = me for met_partial_fraction --------------";
11.132 +"----------- = me for met_partial_fraction --------------";
11.133 +"----------- = me for met_partial_fraction --------------";
11.134 +val fmz =
11.135 + ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
11.136 + "solveFor z", "decomposedFunction p_p"];
11.137 +val (dI',pI',mI') =
11.138 + ("Partial_Fractions",
11.139 + ["partial_fraction", "rational", "simplification"],
11.140 + ["simplification","of_rationals","to_partial_fraction"]);
11.141 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) =
11.142 + CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
11.143 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))")*)
11.144 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)
11.145 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "decomposedFunction p_p")*)
11.146 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Partial_Fractions")*)
11.147 + (*05*)
11.148 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["partial_fraction", "rational", "simplification"])*)
11.149 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
11.150 +(*[ ], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
11.151 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_Rational")*)
11.152 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("PolyEq", ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]))*)
11.153 + (*10*)
11.154 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem)*)
11.155 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*)
11.156 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)
11.157 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions z_i")*)
11.158 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "PolyEq")*)
11.159 +(*[2], Pbl*)(*15*)
11.160 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
11.161 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
11.162 +(*[2], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
11.163 +(*[2, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', z)"], "d2_polyeq_abcFormula_simplify"))*)
11.164 +(*[2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify")*)
11.165 + (*20*)
11.166 +(*[2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Or_to_List)*)
11.167 +(*[2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions")*)
11.168 +(*[2, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
11.169 +(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - -1 / 4))")*)
11.170 +(*[3], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ansatz_rls")*)
11.171 + (*25*)
11.172 +(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)")*)
11.173 +(*[4], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "equival_trans")*)
11.174 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)"*)
11.175 +(*[5], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["z = 1 / 2"])*)
11.176 +(*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*nxt = Rewrite_Set "norm_Rational"*)
11.177 +(*[6], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt;(*nxt = Subproblem ("Isac", ["normalise", "polynomial", "univariate", "equation"]*)
11.178 + (*30+1*)
11.179 +(*[7], Pbl*)val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' [] pt'''; (*nxt = Model_Problem*)
11.180 +(*[7], Pbl*)val (p'v,_,f,nxt'v,_,pt'v) = me nxt'''' p'''' [] pt''''; (*nxt = Add_Given "equality (3 = 3 * AA / 4)")*)
11.181 +(*[7], Pbl*)val (p'v',_,f,nxt'v',_,pt'v') = me nxt'v p'v [] pt'v; (*nxt = Add_Given "solveFor AA")*)
11.182 +(*[7], Pbl*)val (p'v'',_,f,nxt'v'',_,pt'v'') = me nxt'v' p'v' [] pt'v'; (*nxt = Add_Find "solutions AA_i")*)
11.183 +(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt'v'' p'v'' [] pt'v''; (*nxt = Specify_Theory "Isac"*)
11.184 + (*35*)
11.185 +(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*)
11.186 +(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "normalise_poly"])*)
11.187 +(*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
11.188 +(*[7, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"))*)
11.189 +(*[7, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', AA)"], "make_ratpoly_in")*)
11.190 + (*40*)
11.191 +(*[7, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify"*)
11.192 +(*[7, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Isac", ["degree_1", "polynomial", "univariate", "equation"])*)
11.193 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
11.194 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (3 + -3 / 4 * AA = 0)"*)
11.195 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor AA"*)
11.196 + (*45*)
11.197 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.198 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.199 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.200 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.201 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.202 + (*50*)
11.203 +(*[7, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.204 +(*[7, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.205 +(*[7, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.206 +(*[7, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.207 +(*[7, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.208 + (*55*)
11.209 +(*[7, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.210 +(*[7, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.211 +(*[7, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.212 +(*[7], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.213 +(*[8], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.214 + (*60*)
11.215 +(*[8], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.216 +(*[9], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.217 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.218 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.219 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.220 + (*65*)
11.221 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.222 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.223 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.224 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.225 +(*[10], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.226 + (*70*)
11.227 +(*[10, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.228 +(*[10, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.229 +(*[10, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.230 +(*[10, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.231 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.232 + (*75*)
11.233 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.234 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.235 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.236 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.237 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.238 + (*80*)
11.239 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.240 +(*[10, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.241 +(*[10, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.242 +(*[10, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.243 +(*[10, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.244 + (*85*)
11.245 +(*[10, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
11.246 +(*[10, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
11.247 +(*[10, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"*)
11.248 +(*[10, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
11.249 +
11.250 +(*[10], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)"*)
11.251 + (*90*)
11.252 +(*[11], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["AA = 4", "BB = -4"]*)
11.253 +(*[11], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["partial_fraction", "rational", "simplification"]*)
11.254 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
11.255 +
11.256 +case nxt of
11.257 + (_, End_Proof') => if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then ()
11.258 + else error "= me .. met_partial_fraction f changed"
11.259 +| _ => error "= me .. met_partial_fraction nxt changed";
11.260 +
11.261 +show_pt_tac pt; (*[
11.262 +([], Frm), Problem
11.263 + (''Partial_Fractions'',
11.264 + ??.\<^const>String.char.Char ''partial_fraction'' ''rational''
11.265 + ''simplification'')
11.266 +. . . . . . . . . . Apply_Method ["simplification","of_rationals","to_partial_fraction"],
11.267 +([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))
11.268 +. . . . . . . . . . Rewrite_Set "norm_Rational",
11.269 +([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)
11.270 +. . . . . . . . . . Subproblem (Isac, ["abcFormula","degree_2","polynomial","univariate","equation"]),
11.271 +([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)
11.272 +. . . . . . . . . . Apply_Method ["PolyEq","solve_d2_polyeq_abc_equation"],
11.273 +([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0
11.274 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', z)], "d2_polyeq_abcFormula_simplify"),
11.275 +([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) \<or>
11.276 +z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)
11.277 +. . . . . . . . . . Rewrite_Set "polyeq_simplify",
11.278 +([2,2], Res), z = 1 / 2 \<or> z = -1 / 4
11.279 +. . . . . . . . . . Or_to_List ,
11.280 +([2,3], Res), [z = 1 / 2, z = -1 / 4]
11.281 +. . . . . . . . . . Check_elementwise "Assumptions",
11.282 +([2,4], Res), [z = 1 / 2, z = -1 / 4]
11.283 +. . . . . . . . . . Check_Postcond ["abcFormula","degree_2","polynomial","univariate","equation"],
11.284 +([2], Res), [z = 1 / 2, z = -1 / 4]
11.285 +. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4))",
11.286 +([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))
11.287 +. . . . . . . . . . Rewrite_Set "ansatz_rls",
11.288 +([3], Res), AA / (z - 1 / 2) + BB / (z - -1 / 4)
11.289 +. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)",
11.290 +([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)
11.291 +. . . . . . . . . . Rewrite_Set "equival_trans",
11.292 +([4], Res), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
11.293 +. . . . . . . . . . Substitute ["z = 1 / 2"],
11.294 +([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)
11.295 +. . . . . . . . . . Rewrite_Set "norm_Rational",
11.296 +([6], Res), 3 = 3 * AA / 4
11.297 +. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
11.298 +([7], Pbl), solve (3 = 3 * AA / 4, AA)
11.299 +. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
11.300 +([7,1], Frm), 3 = 3 * AA / 4
11.301 +. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
11.302 +([7,1], Res), 3 - 3 * AA / 4 = 0
11.303 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "make_ratpoly_in"),
11.304 +([7,2], Res), 3 / 1 + -3 / 4 * AA = 0
11.305 +. . . . . . . . . . Rewrite_Set "polyeq_simplify",
11.306 +([7,3], Res), 3 + -3 / 4 * AA = 0
11.307 +. . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),
11.308 +([7,4], Pbl), solve (3 + -3 / 4 * AA = 0, AA)
11.309 +. . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],
11.310 +([7,4,1], Frm), 3 + -3 / 4 * AA = 0
11.311 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "d1_polyeq_simplify"),
11.312 +([7,4,1], Res), AA = -1 * 3 / (-3 / 4)
11.313 +. . . . . . . . . . Rewrite_Set "polyeq_simplify",
11.314 +([7,4,2], Res), AA = -3 / (-3 / 4)
11.315 +. . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",
11.316 +([7,4,3], Res), AA = 4
11.317 +. . . . . . . . . . Or_to_List ,
11.318 +([7,4,4], Res), [AA = 4]
11.319 +. . . . . . . . . . Check_elementwise "Assumptions",
11.320 +([7,4,5], Res), [AA = 4]
11.321 +. . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],
11.322 +([7,4], Res), [AA = 4]
11.323 +. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
11.324 +([7], Res), [AA = 4]
11.325 +. . . . . . . . . . Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)",
11.326 +([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
11.327 +. . . . . . . . . . Substitute ["z = -1 / 4"],
11.328 +([8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)
11.329 +. . . . . . . . . . Rewrite_Set "norm_Rational",
11.330 +([9], Res), 3 = -3 * BB / 4
11.331 +. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
11.332 +([10], Pbl), solve (3 = -3 * BB / 4, BB)
11.333 +. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
11.334 +([10,1], Frm), 3 = -3 * BB / 4
11.335 +. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
11.336 +([10,1], Res), 3 - -3 * BB / 4 = 0
11.337 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "make_ratpoly_in"),
11.338 +([10,2], Res), 3 / 1 + 3 / 4 * BB = 0
11.339 +. . . . . . . . . . Rewrite_Set "polyeq_simplify",
11.340 +([10,3], Res), 3 + 3 / 4 * BB = 0
11.341 +. . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),
11.342 +([10,4], Pbl), solve (3 + 3 / 4 * BB = 0, BB)
11.343 +. . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],
11.344 +([10,4,1], Frm), 3 + 3 / 4 * BB = 0
11.345 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "d1_polyeq_simplify"),
11.346 +([10,4,1], Res), BB = -1 * 3 / (3 / 4)
11.347 +. . . . . . . . . . Rewrite_Set "polyeq_simplify",
11.348 +([10,4,2], Res), BB = -3 / (3 / 4)
11.349 +. . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",
11.350 +([10,4,3], Res), BB = -4
11.351 +. . . . . . . . . . Or_to_List ,
11.352 +([10,4,4], Res), [BB = -4]
11.353 +. . . . . . . . . . Check_elementwise "Assumptions",
11.354 +([10,4,5], Res), [BB = -4]
11.355 +. . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],
11.356 +([10,4], Res), [BB = -4]
11.357 +. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
11.358 +([10], Res), [BB = -4]
11.359 +. . . . . . . . . . Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)",
11.360 +([11], Frm), AA / (z - 1 / 2) + BB / (z - -1 / 4)
11.361 +. . . . . . . . . . Substitute ["AA = 4","BB = -4"],
11.362 +([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)
11.363 +. . . . . . . . . . Check_Postcond ["partial_fraction","rational","simplification"],
11.364 +([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)]
11.365 +val it = (): unit
11.366 +*)
11.367 +
11.368 +"----------- autoCalculate for met_partial_fraction -----";
11.369 +"----------- autoCalculate for met_partial_fraction -----";
11.370 +"----------- autoCalculate for met_partial_fraction -----";
11.371 +reset_states ();
11.372 + val fmz =
11.373 + ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
11.374 + "solveFor z", "decomposedFunction p_p"];
11.375 + val (dI', pI', mI') =
11.376 + ("Partial_Fractions",
11.377 + ["partial_fraction", "rational", "simplification"],
11.378 + ["simplification","of_rationals","to_partial_fraction"]);
11.379 +CalcTree [(fmz, (dI' ,pI' ,mI'))];
11.380 +Iterator 1;
11.381 +moveActiveRoot 1;
11.382 +autoCalculate 1 CompleteCalc;
11.383 +
11.384 +val ((pt,p),_) = get_calc 1; val ip = get_pos 1 1;
11.385 +if p = ip andalso ip = ([], Res) then ()
11.386 + else error "autoCalculate for met_partial_fraction changed: final pos'";
11.387 +
11.388 +val (Form f, tac, asms) = pt_extract (pt, p);
11.389 +if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso
11.390 + terms2str' asms =
11.391 + "[BB = -4,BB is_polyexp,AA is_polyexp,AA = 4," ^
11.392 + "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
11.393 + "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]"
11.394 +then case tac of NONE => ()
11.395 + | _ => error "me for met_partial_fraction changed: final result 1"
11.396 +else error "me for met_partial_fraction changed: final result 2"
11.397 +
11.398 +show_pt pt;
11.399 +(*[
11.400 +(([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])),
11.401 +(([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
11.402 +(([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
11.403 +(([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
11.404 +(([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
11.405 +(([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
11.406 +z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
11.407 +(([2,2], Res), z = 1 / 2 | z = -1 / 4),
11.408 +(([2,3], Res), [z = 1 / 2, z = -1 / 4]),
11.409 +(([2,4], Res), [z = 1 / 2, z = -1 / 4]),
11.410 +(([2], Res), [z = 1 / 2, z = -1 / 4]),
11.411 +(([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),
11.412 +(([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
11.413 +(([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
11.414 +(([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)),
11.415 +(([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
11.416 +(([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)),
11.417 +(([6], Res), 3 = 3 * A / 4),
11.418 +(([7], Pbl), solve (3 = 3 * A / 4, A)),
11.419 +(([7,1], Frm), 3 = 3 * A / 4),
11.420 +(([7,1], Res), 3 - 3 * A / 4 = 0),
11.421 +(([7,2], Res), 3 / 1 + -3 / 4 * A = 0),
11.422 +(([7,3], Res), 3 + -3 / 4 * A = 0),
11.423 +(([7,4], Pbl), solve (3 + -3 / 4 * A = 0, A)),
11.424 +(([7,4,1], Frm), 3 + -3 / 4 * A = 0),
11.425 +(([7,4,1], Res), A = -1 * 3 / (-3 / 4)),
11.426 +(([7,4,2], Res), A = -3 / (-3 / 4)),
11.427 +(([7,4,3], Res), A = 4),
11.428 +(([7,4,4], Res), [A = 4]),
11.429 +(([7,4,5], Res), [A = 4]),
11.430 +(([7,4], Res), [A = 4]),
11.431 +(([7], Res), [A = 4]),
11.432 +(([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
11.433 +(([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)),
11.434 +(([9], Res), 3 = -3 * B / 4),
11.435 +(([10], Pbl), solve (3 = -3 * B / 4, B)),
11.436 +(([10,1], Frm), 3 = -3 * B / 4),
11.437 +(([10,1], Res), 3 - -3 * B / 4 = 0),
11.438 +(([10,2], Res), 3 / 1 + 3 / 4 * B = 0),
11.439 +(([10,3], Res), 3 + 3 / 4 * B = 0),
11.440 +(([10,4], Pbl), solve (3 + 3 / 4 * B = 0, B)),
11.441 +(([10,4,1], Frm), 3 + 3 / 4 * B = 0),
11.442 +(([10,4,1], Res), B = -1 * 3 / (3 / 4)),
11.443 +(([10,4,2], Res), B = -3 / (3 / 4)),
11.444 +(([10,4,3], Res), B = -4),
11.445 +(([10,4,4], Res), [B = -4]),
11.446 +(([10,4,5], Res), [B = -4]),
11.447 +(([10,4], Res), [B = -4]),
11.448 +(([10], Res), [B = -4]),
11.449 +(([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)),
11.450 +(([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
11.451 +(([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4))] *)
11.452 +
11.453 +\<close> ML \<open>
11.454 +"----------- progr.vers.2: check erls for multiply_ansatz";
11.455 +"----------- progr.vers.2: check erls for multiply_ansatz";
11.456 +"----------- progr.vers.2: check erls for multiply_ansatz";
11.457 +(*test for outcommented 3 lines in script: is norm_Rational strong enough?*)
11.458 +val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))";
11.459 +val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t;
11.460 +term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
11.461 +
11.462 +val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*)
11.463 +term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
11.464 + "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
11.465 +
11.466 +val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
11.467 +if term2str t''' = "3 = (AA + -2 * BB + 4 * z * AA + 4 * z * BB) / 4" then ()
11.468 +else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
11.469 +
11.470 +(*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
11.471 +val xxx = append_rls "multiply_ansatz_erls" norm_Rational
11.472 + [Calc ("HOL.eq",eval_equal "#equal_")];
11.473 +
11.474 +val multiply_ansatz = prep_rls @{theory} (
11.475 + Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
11.476 + erls = xxx,
11.477 + srls = Erls, calc = [], errpatts = [],
11.478 + rules =
11.479 + [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
11.480 + ],
11.481 + scr = EmptyScr}:rls);
11.482 +
11.483 +rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*)
11.484 +rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?*)
11.485 +
11.486 +"----------- progr.vers.2: improve program --------------";
11.487 +"----------- progr.vers.2: improve program --------------";
11.488 +"----------- progr.vers.2: improve program --------------";
11.489 +(*WN120318 stopped due to much effort with the test above*)
11.490 + "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
11.491 + " (let f_f = Take f_f; " ^
11.492 + " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
11.493 + " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
11.494 + " (numer::real) = get_numerator f_f; " ^(*numer: 24*)
11.495 + " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)
11.496 + " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)
11.497 + " (L_L::bool list) = (SubProblem (PolyEqX, " ^
11.498 + " [abcFormula, degree_2, polynomial, univariate, equation], " ^
11.499 + " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)
11.500 + " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)
11.501 + " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *)
11.502 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
11.503 + " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
11.504 +(*this has been tested below by rewrite_set_
11.505 + " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**)
11.506 + " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**)
11.507 + " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
11.508 +NEXT try to outcomment the very next line..*)
11.509 + " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
11.510 + " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
11.511 + " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*)
11.512 + " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: -1 / 4*)
11.513 + " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
11.514 + " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
11.515 + " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
11.516 + " (sol_a::bool list) = " ^
11.517 + " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
11.518 + " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
11.519 + " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
11.520 + " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
11.521 + " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
11.522 + " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
11.523 + " (sol_b::bool list) = " ^
11.524 + " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
11.525 + " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
11.526 + " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
11.527 + " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
11.528 + " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)
11.529 + " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
11.530 + " in pbz)"
11.531 +
11.532 +\<close> ML \<open>
11.533 +\<close> ML \<open>
11.534 +"~~~~~ fun xxx , args:"; val () = ();
11.535 +\<close>
11.536 +
11.537 +section \<open>=============== "Knowledge/biegelinie-3.sml" ===============================\<close>
11.538 +ML \<open>
11.539 +"~~~~~ fun xxx , args:"; val () = ();
11.540 +\<close> ML \<open>
11.541 +(* "Knowledge/biegelinie-3.sml"
11.542 + author: Walther Neuper 190515
11.543 + (c) due to copyright terms
11.544 +*)
11.545 +"table of contents -----------------------------------------------";
11.546 +"-----------------------------------------------------------------";
11.547 +"----------- see biegelinie-1.sml---------------------------------";
11.548 +(* problems with generalised handling of meths which extend the model of a probl
11.549 + since 98298342fb6d: wait for review of whole model-specify phase *)
11.550 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
11.551 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
11.552 +"-----------------------------------------------------------------";
11.553 +"-----------------------------------------------------------------";
11.554 +"-----------------------------------------------------------------";
11.555 +
11.556 +\<close> ML \<open>
11.557 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
11.558 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
11.559 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
11.560 +"----- Bsp 7.70 with me";
11.561 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
11.562 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
11.563 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
11.564 + "AbleitungBiegelinie dy"];
11.565 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
11.566 + ["IntegrierenUndKonstanteBestimmen2"]);
11.567 +val p = e_pos'; val c = [];
11.568 +(*//----------------------------------vvv CalcTreeTEST ----------------------------------------\\*)
11.569 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
11.570 +
11.571 +(*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p);
11.572 +(*+*)writeln (oris2str oris); (*[
11.573 +(1, ["1"], #Given,Traegerlaenge, ["L"]),
11.574 +(2, ["1"], #Given,Streckenlast, ["q_0"]),
11.575 +(3, ["1"], #Find,Biegelinie, ["y"]),
11.576 +(4, ["1"], #Relate,Randbedingungen, ["[y 0 = 0]","[y L = 0]","[M_b 0 = 0]","[M_b L = 0]"]),
11.577 +(5, ["1"], #undef,FunktionsVariable, ["x"]),
11.578 +(6, ["1"], #undef,GleichungsVariablen, ["[c]","[c_2]","[c_3]","[c_4]"]),
11.579 +(7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*)
11.580 +(*+*)itms2str_ @{context} probl = "[]";
11.581 +(*+*)itms2str_ @{context} meth = "[]";
11.582 +(*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*)
11.583 +
11.584 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
11.585 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
11.586 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
11.587 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
11.588 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
11.589 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
11.590 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
11.591 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
11.592 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
11.593 +(*----------- 10 -----------*)
11.594 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
11.595 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy*)
11.596 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
11.597 +
11.598 +(*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*)
11.599 +(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Model_Problem*)
11.600 +(*AMBIGUITY in creating the environment from formal args. of partial_function "Biegelinie.Biegelinie2Script"
11.601 +and the actual args., ie. items of the guard of "["IntegrierenUndKonstanteBestimmen2"]" by "assoc_by_type":
11.602 +formal arg. "b" type-matches with several...actual args. "["dy","y"]"
11.603 +selected "dy"
11.604 +with
11.605 +formals: ["l","q","v","b","s","vs","id_abl"]
11.606 +actuals: ["L","q_0","x","[c, c_2, c_3, c_4]","dy","y","[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]"]*)
11.607 +
11.608 +"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
11.609 + val (pt''', p''') =
11.610 + (*locatetac is here for testing by me; step would suffice in me*)
11.611 + case locatetac tac (pt,p) of
11.612 + ("ok", (_, _, ptp)) => ptp
11.613 +;
11.614 +(*+*)p = ([], Met);
11.615 +(*+*)p''' = ([1], Pbl);
11.616 +(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');
11.617 +(*+*)(*MISSING after locatetac:*)
11.618 +(*+*)writeln (oris2str oris); (*[
11.619 +(1, ["1"], #Given,Streckenlast, ["q_0"]),
11.620 +(2, ["1"], #Given,FunktionsVariable, ["x"]),
11.621 +(3, ["1"], #Find,Funktionen, ["funs'''"])]
11.622 +MISSING:
11.623 + Biegelinie
11.624 + AbleitungBiegelinie
11.625 +*)
11.626 +"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
11.627 + val (mI, m) = Solve.mk_tac'_ tac;
11.628 +val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
11.629 +(*if*) member op = Solve.specsteps mI = false; (*else*)
11.630 +
11.631 +loc_solve_ (mI,m) ptp;
11.632 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
11.633 +
11.634 +Solve.solve m (pt, pos);
11.635 +"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tac.Apply_Method' (mI, _, _, _)), (pt, (pos as (p, _)))) =
11.636 + (m, (pt, pos));
11.637 +val {srls, ...} = Specify.get_met mI;
11.638 + val itms = case get_obj I pt p of
11.639 + PblObj {meth=itms, ...} => itms
11.640 + | _ => error "solve Apply_Method: uncovered case get_obj"
11.641 + val thy' = get_obj g_domID pt p;
11.642 + val thy = Celem.assoc_thy thy';
11.643 + val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of
11.644 + (is as Selem.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
11.645 + | _ => error "solve Apply_Method: uncovered case init_scrstate"
11.646 + val ini = Lucin.init_form thy sc env;
11.647 + val p = lev_dn p;
11.648 +val NONE = (*case*) ini (*of*);
11.649 + val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
11.650 + val d = Rule.e_rls (*FIXME: get simplifier from domID*);
11.651 +val Steps (_, ss as (_, _, pt', p', c') :: _) =
11.652 +(*case*) Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*);
11.653 +
11.654 +(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');
11.655 +(*+*)(*MISSING after locate_gen:*)
11.656 +(*+*)writeln (oris2str oris); (*[
11.657 +(1, ["1"], #Given,Streckenlast, ["q_0"]),
11.658 +(2, ["1"], #Given,FunktionsVariable, ["x"]),
11.659 +(3, ["1"], #Find,Funktionen, ["funs'''"])]
11.660 +MISSING:
11.661 + Biegelinie
11.662 + AbleitungBiegelinie
11.663 +*)
11.664 +"~~~~~ fun locate_gen , args:"; val ((thy', srls), m, (pt, p),
11.665 + (scr as Rule.Prog sc, d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) =
11.666 + ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
11.667 +val thy = Celem.assoc_thy thy';
11.668 +(*if*) l = [] orelse (
11.669 + (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res) = true;(*then*)
11.670 +(assy (thy',ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) (body_of sc));
11.671 +
11.672 +"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss:step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
11.673 + ((thy',ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (body_of sc));
11.674 +(*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);
11.675 +
11.676 +"~~~~~ fun assy , args:"; val ((thy',ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss), t) =
11.677 + (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
11.678 +val (a', LTool.STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*);
11.679 +(*+*)writeln (term2str stac); (*SubProblem
11.680 + (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
11.681 + [''Biegelinien'', ''ausBelastung''])
11.682 + [REAL q_0, REAL x, REAL_REAL y, REAL_REAL dy] *)
11.683 + val p' =
11.684 + case p_ of Frm => p
11.685 + | Res => lev_on p
11.686 + | _ => error ("assy: call by " ^ pos'2str (p,p_));
11.687 + val Ass (m,v') = (*case*) assod pt d m stac (*of*);
11.688 +
11.689 +"~~~~~ fun assod , args:"; val (pt, _, (Tac.Subproblem' ((domID, pblID, _), _, _, _, _, _)),
11.690 + (stac as Const ("Script.SubProblem", _) $ (Const ("Product_Type.Pair", _) $
11.691 + dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags')) =
11.692 + (pt, d, m, stac);
11.693 + val dI = HOLogic.dest_string dI';
11.694 + val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
11.695 + val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string;
11.696 + val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string;
11.697 + val ags = TermC.isalist2list ags';
11.698 +(*if*) mI = ["no_met"] = false; (*else*)
11.699 +(* val (pI, pors, mI) = *)
11.700 + (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
11.701 + handle ERROR "actual args do not match formal args"
11.702 + => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
11.703 +"~~~~~ fun match_ags , args:"; val (thy, pbt, ags) = (thy, ((#ppc o Specify.get_pbt) pI), ags);
11.704 +(*+*)pbt;
11.705 + fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
11.706 + val pbt' = filter_out is_copy_named pbt
11.707 + val cy = filter is_copy_named pbt
11.708 + val oris' = matc thy pbt' ags []
11.709 + val cy' = map (cpy_nam pbt' oris') cy
11.710 + val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
11.711 +
11.712 +(*+*)val c = [];
11.713 +(*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)
11.714 +
11.715 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Add_Given "Streckenlast q_0"*)
11.716 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
11.717 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Funktionen funs'''"*)
11.718 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
11.719 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
11.720 +(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*)
11.721 +(*----------- 20 -----------*)
11.722 +(*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
11.723 +(*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*)
11.724 +ERROR itms2args: 'Biegelinie' not in itms*)
11.725 +
11.726 +(*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _)
11.727 + [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]
11.728 + ^^^^^^^^^^^ ..ERROR itms2args: 'Biegelinie' not in itms*)
11.729 +(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');
11.730 +(*+*)if oris2str oris =
11.731 +(*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"
11.732 +(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris";
11.733 +writeln (oris2str oris); (*[
11.734 +(1, ["1"], #Given,Streckenlast, ["q_0"]),
11.735 +(2, ["1"], #Given,FunktionsVariable, ["x"]),
11.736 +(3, ["1"], #Find,Funktionen, ["funs'''"])]*)
11.737 +(*+*)if itms2str_ @{context} probl = "[\n(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),\n(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),\n(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]"
11.738 +(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl";
11.739 +writeln (itms2str_ @{context} probl); (*[
11.740 +(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
11.741 +(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
11.742 +(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*)
11.743 +(*+*)if itms2str_ @{context} meth = "[]"
11.744 +(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";
11.745 +writeln (itms2str_ @{context} meth); (*[]*)
11.746 +
11.747 +"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
11.748 +(* val (pt, p) = *)
11.749 + (*locatetac is here for testing by me; step would suffice in me*)
11.750 + case locatetac tac (pt,p) of
11.751 + ("ok", (_, _, ptp)) => ptp
11.752 +;
11.753 +"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
11.754 + val (mI, m) = Solve.mk_tac'_ tac;
11.755 +val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
11.756 +(*if*) member op = Solve.specsteps mI = true; (*then*)
11.757 +
11.758 +(*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
11.759 +"~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);
11.760 +(* val (p, _, f, _, _, pt) =*) Chead.specify m pos [] pt;
11.761 +
11.762 +"~~~~~ fun specify , args:"; val ((Tac.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt);
11.763 + val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
11.764 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
11.765 + (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
11.766 + val {ppc, pre, prls,...} = Specify.get_met mID
11.767 + val thy = Celem.assoc_thy dI
11.768 + val dI'' = if dI = Rule.e_domID then dI' else dI
11.769 + val pI'' = if pI = Celem.e_pblID then pI' else pI
11.770 +;
11.771 +(*+*)writeln (oris2str oris); (*[
11.772 +(1, ["1"], #Given,Streckenlast, ["q_0"]),
11.773 +(2, ["1"], #Given,FunktionsVariable, ["x"]),
11.774 +(3, ["1"], #Find,Funktionen, ["funs'''"])]*)
11.775 +(*+*)writeln (pats2str' ppc);
11.776 +(*["(#Given, (Streckenlast, q__q))
11.777 +","(#Given, (FunktionsVariable, v_v))
11.778 +","(#Given, (Biegelinie, id_fun))
11.779 +","(#Given, (AbleitungBiegelinie, id_abl))
11.780 +","(#Find, (Funktionen, fun_s))"]*)
11.781 +(*+*)writeln (pats2str' ((#ppc o Specify.get_pbt) pI));
11.782 +(*["(#Given, (Streckenlast, q_q))
11.783 +","(#Given, (FunktionsVariable, v_v))
11.784 +","(#Find, (Funktionen, funs'''))"]*)
11.785 + val oris = Specify.add_field' thy ppc oris
11.786 + val met = if met = [] then pbl else met
11.787 + val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
11.788 +;
11.789 +(*+*)writeln (itms2str_ @{context} itms); (*[
11.790 +(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
11.791 +(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
11.792 +(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *)
11.793 +
11.794 +(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
11.795 +val itms =
11.796 + if mI' = ["Biegelinien", "ausBelastung"]
11.797 + then itms @
11.798 + [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
11.799 + [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
11.800 + (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
11.801 + [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
11.802 + (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
11.803 + [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
11.804 + (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
11.805 + [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
11.806 + else itms
11.807 +(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
11.808 +
11.809 +val itms' = itms @
11.810 + [(4, [1], true, "#Given", Cor ((@{term "Biegelinie"},
11.811 + [@{term "y::real \<Rightarrow> real"}]),
11.812 + (@{term "id_fun::real \<Rightarrow> real"},
11.813 + [@{term "y::real \<Rightarrow> real"}] ))),
11.814 + (5, [1], true, "#Given", Cor ((@{term "AbleitungBiegelinie"},
11.815 + [@{term "dy::real \<Rightarrow> real"}]),
11.816 + (@{term "id_abl::real \<Rightarrow> real"},
11.817 + [@{term "dy::real \<Rightarrow> real"}] )))]
11.818 +val itms'' = itms @
11.819 + [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
11.820 + [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
11.821 + (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
11.822 + [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
11.823 + (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
11.824 + [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
11.825 + (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
11.826 + [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
11.827 +;
11.828 +if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN";
11.829 +(*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
11.830 +
11.831 +val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
11.832 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.833 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.834 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.835 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.836 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.837 +(*----------- 30 -----------*)
11.838 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.839 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.840 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.841 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.842 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.843 +(*----------- 40 -----------*)
11.844 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.845 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.846 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.847 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.848 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.849 +(*----------- 50 -----------*)
11.850 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.851 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.852 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.853 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.854 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.855 +(*----------- 60 -----------*)
11.856 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.857 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.858 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.859 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.860 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.861 +(*----------- 70 -----------*)
11.862 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.863 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.864 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.865 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.866 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.867 +(*----------- 80 -----------*)
11.868 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.869 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.870 +\<close> ML \<open>
11.871 +(**)val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.872 +\<close> ML \<open>
11.873 +(*CURRENT*)if p = ([2, 1], Pbl) andalso
11.874 +(*CURRENT*) f = PpcKF (Problem [], {Find = [Incompl "equality"], Given = [Incompl "functionEq", Incompl "substitution"], Relate = [], Where = [], With = []})
11.875 +(*CURRENT*)then
11.876 +(*CURRENT*) case nxt of
11.877 +(*CURRENT*) ("Add_Given", Add_Given "functionEq (hd [])") => ((*here is an error in partial_function*))
11.878 +(*CURRENT*) | _ => error "me biegelinie changed 1"
11.879 +(*CURRENT*)else error "me biegelinie changed 2";
11.880 +\<close> ML \<open>
11.881 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.882 +(*CURRENT*)nxt;(* = ("Tac ", Tac "[error] appl_add: is_known: seek_oridts: input ('substitution (NTH (1 + -4) [])') not found in oris (typed)")*)
11.883 +\<close> ML \<open>
11.884 +(*----- due to "switch from Script to partial_function" 4035ec339062 ?
11.885 + OR ?due to "failed trial to generalise handling of meths which extend the model of a probl " 98298342fb6d
11.886 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.887 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.888 +(*----------- 90 -----------*)
11.889 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.890 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.891 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.892 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.893 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.894 +(*---------- 100 -----------*)
11.895 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.896 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.897 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.898 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.899 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.900 +(*---------- 110 -----------*)
11.901 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.902 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.903 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.904 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.905 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.906 +(*---------- 120 -----------*)
11.907 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.908 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.909 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.910 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.911 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.912 +(*---------- 130 -----------*)
11.913 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.914 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.915 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.916 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.917 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
11.918 +
11.919 +if p = ([3], Pbl)
11.920 +then
11.921 + case nxt of
11.922 + ("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") =>
11.923 + (case f of
11.924 + PpcKF
11.925 + (Problem [],
11.926 + {Find = [Incompl "solution []"], Given =
11.927 + [Correct
11.928 + "equalities\n [0 = -1 * c_4 / -1,\n 0 =\n (-24 * c_4 * EI + -24 * L * c_3 * EI + 12 * L ^^^ 2 * c_2 +\n 4 * L ^^^ 3 * c +\n -1 * L ^^^ 4 * q_0) /\n (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
11.929 + Incompl "solveForVars [c]"],
11.930 + Relate = [], Where = [], With = []}) => ()
11.931 + | _ => error "Bsp.7.70 me changed 1")
11.932 + | _ => error "Bsp.7.70 me changed 2"
11.933 +else error "Bsp.7.70 me changed 3";
11.934 +-----*)
11.935 +(* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
11.936 +
11.937 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
11.938 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
11.939 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
11.940 +(* the error in this test might be independent from introduction of y, dy
11.941 + as arguments in IntegrierenUndKonstanteBestimmen2,
11.942 + rather due to so far untested use of "auto" *)
11.943 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
11.944 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
11.945 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
11.946 + "AbleitungBiegelinie dy"];
11.947 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
11.948 + ["IntegrierenUndKonstanteBestimmen2"]);
11.949 +
11.950 +reset_states ();
11.951 +CalcTree [(fmz, (dI',pI',mI'))];
11.952 +Iterator 1;
11.953 +moveActiveRoot 1;
11.954 +
11.955 +(*[], Met*)autoCalculate 1 CompleteCalcHead;
11.956 +(*[1], Pbl*)autoCalculate 1 (Step 1); (* into SubProblem *)
11.957 +(*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)
11.958 +(*[2], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)
11.959 +(*[2], Res*)autoCalculate 1 CompleteSubpbl;
11.960 +(*[3], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)
11.961 +(*[3], Met*)autoCalculate 1 CompleteCalcHead;
11.962 +(*[3, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.963 +(*(**)autoCalculate 1 CompleteSubpbl; error in kernel 4: generate1: not impl.for Empty_Tac_*)
11.964 +(*[3, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.965 +(*[3, 2], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.966 +(*[3, 3], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.967 +(*[3, 4], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.968 +(*[3, 5], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.969 +(*[3, 6], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.970 +(*[3, 7], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.971 +(*[3, 8], Pbl*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.972 +(*[3, 8], Met*)autoCalculate 1 CompleteCalcHead;
11.973 +(*[3, 8, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.974 +(*[3, 8, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
11.975 +(*(**)autoCalculate 1 (Step 1);
11.976 +*** generate1: not impl.for Empty_Tac_
11.977 +val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)
11.978 +
11.979 +val ((pt,_),_) = get_calc 1;
11.980 +val ip = get_pos 1 1;
11.981 +val (Form f, tac, asms) = pt_extract (pt, ip);
11.982 +
11.983 +if ip = ([2, 1, 1], Frm) andalso
11.984 +term2str f = "hd []"
11.985 +then
11.986 + case tac of
11.987 + SOME Empty_Tac => ()
11.988 + | _ => error "ERROR biegel.7.70 changed 1"
11.989 +else error "ERROR biegel.7.70 changed 2";
11.990 +
11.991 +(*----- this state has been reached shortly after 98298342fb6d:
11.992 +if ip = ([3, 8, 1], Res) andalso
11.993 +term2str f = "[-1 * c_4 / -1 = 0,\n (6 * c_4 * EI + 6 * L * c_3 * EI + -3 * L ^^^ 2 * c_2 + -1 * L ^^^ 3 * c) /\n (6 * EI) =\n L ^^^ 4 * q_0 / (-24 * EI),\n c_2 = 0, c_2 + L * c = L ^^^ 2 * q_0 / 2]"
11.994 +then
11.995 + case tac of
11.996 + SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()
11.997 + | _ => error "ERROR biegel.7.70 changed 1"
11.998 +else error "ERROR biegel.7.70 changed 2";
11.999 +*)
11.1000 \<close> ML \<open>
11.1001 \<close> ML \<open>
11.1002 "~~~~~ fun xxx , args:"; val () = ();
12.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Thu May 30 12:39:13 2019 +0200
12.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Sat Jun 01 11:09:19 2019 +0200
12.3 @@ -1,4 +1,5 @@
12.4 -(* Title: tests for xmlsrc/thy-hierarchy.sml
12.5 +(* Title: "xmlsrc/thy-hierarchy.sml"
12.6 + tests for xmlsrc/thy-hierarchy.sml
12.7 Authors: Walther Neuper 060113
12.8 (c) due to copyright terms
12.9
12.10 @@ -29,7 +30,6 @@
12.11 "----------- ..CONTINUED: we adapt some required MINIfunctions ---";
12.12 "----------- ..CONTINUED: xml from Test_Build_Thydata.thy --------";
12.13 "----------- ..CONTINUED: repair xml-format of thy_*-thm-*.xml ---";
12.14 -"-------- fun thms_of --------------------------------------------------------";
12.15 "-----------------------------------------------------------------";
12.16 "-----------------------------------------------------------------";
12.17 "-----------------------------------------------------------------";
12.18 @@ -52,7 +52,10 @@
12.19 if map thmID_of_derivation_name' thms =
12.20 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment",
12.21 "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()
12.22 -else error "fun thms_of ...changed"
12.23 +else error "fun thms_of ...changed";
12.24 +
12.25 +val without_partial_functions = thms_of @{theory Biegelinie};
12.26 +if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed";
12.27
12.28 "----------- ### thes2file ... Exception- Match raised -----------";
12.29 "----------- ### thes2file ... Exception- Match raised -----------";
12.30 @@ -267,11 +270,10 @@
12.31 " </SRLS>\n" ^
12.32 " <SCRIPT>\n" ^
12.33 " <MATHML>\n" ^
12.34 -" <ISA> Script Stepwise t_t =\n" ^
12.35 -" Repeat\n" ^
12.36 -" ((Try (Repeat (Rewrite ''distrib_right'' False)) @@\n" ^
12.37 -" Try (Repeat (Rewrite ''distrib_left'' False)))\n" ^
12.38 -" ??.empty) </ISA>\n" ^
12.39 +" <ISA> auto_generated t_t =\nRepeat\n" ^
12.40 +" ((Try (Repeat (Rewrite ''distrib_right'' False)) @@\n" ^
12.41 +" Try (Repeat (Rewrite ''distrib_left'' False)))\n" ^
12.42 +" ??.empty) </ISA>\n" ^
12.43 " </MATHML>\n" ^
12.44 " </SCRIPT>\n" ^
12.45 " </RULESET>\n" ^
12.46 @@ -279,9 +281,10 @@
12.47 " <MATHAUTHORS>\n" ^
12.48 " <STRING> isac-team </STRING>\n" ^
12.49 " </MATHAUTHORS>\n" ^
12.50 -" <COURSEDESIGNS>\n </COURSEDESIGNS>\n" ^
12.51 +" <COURSEDESIGNS>\n" ^
12.52 +" </COURSEDESIGNS>\n" ^
12.53 "</RULESETDATA>\n") then ()
12.54 -else error "thydata2xml for rls changed"
12.55 +else error "thydata2xml for rls changed";
12.56
12.57 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
12.58 "----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
12.59 @@ -427,8 +430,3 @@
12.60 " </COURSEDESIGNS>\n" ^
12.61 "</THEOREMDATA>\n") then () else error "thy_isac_Test_Build_Thydata-thm-thm111.xml changed"
12.62
12.63 -"-------- fun thms_of --------------------------------------------------------";
12.64 -"-------- fun thms_of --------------------------------------------------------";
12.65 -"-------- fun thms_of --------------------------------------------------------";
12.66 -val without_partial_functions = thms_of @{theory Biegelinie};
12.67 -if length without_partial_functions = 7 then () else error "thms_of Biegelinie changed";