1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Aug 26 09:20:07 2019 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Mon Aug 26 17:40:27 2019 +0200
1.3 @@ -104,7 +104,7 @@
1.4
1.5 ML \<open>Celem.check_guhs_unique := false;\<close>
1.6 ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close>
1.7 -ML \<open>@{theory "Isac"}\<close>
1.8 +ML \<open>@{theory "Isac_Knowledge"}\<close>
1.9 ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"]
1.10 ERROR: app_py: not found: ["IsacKnowledge","Diff","Theorems","diff_sin_chain"]*)\<close>
1.11
2.1 --- a/src/Tools/isac/CalcElements/KEStore.thy Mon Aug 26 09:20:07 2019 +0200
2.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy Mon Aug 26 17:40:27 2019 +0200
2.3 @@ -135,13 +135,13 @@
2.4 section \<open>Re-use existing access functions for knowledge elements\<close>
2.5 text \<open>
2.6 The independence of problems' and methods' structure enforces the accesse
2.7 - functions to use "Isac", the final theory which comprises all knowledge defined.
2.8 + functions to use "Isac_Knowledge", the final theory which comprises all knowledge defined.
2.9 \<close>
2.10 ML \<open>
2.11 val get_ref_thy = KEStore_Elems.get_ref_thy;
2.12
2.13 fun assoc_rls (rls' : Rule.rls') =
2.14 - case AList.lookup (op =) (KEStore_Elems.get_rlss (Rule.Thy_Info_get_theory "Isac")) rls' of
2.15 + case AList.lookup (op =) (KEStore_Elems.get_rlss (Rule.Thy_Info_get_theory "Isac_Knowledge")) rls' of
2.16 SOME (_, rls) => rls
2.17 | NONE => raise ERROR ("rls \""^ rls' ^ "\" missing in KEStore.\n" ^
2.18 "TODO exception hierarchy needs to be established.")
3.1 --- a/src/Tools/isac/CalcElements/calcelems.sml Mon Aug 26 09:20:07 2019 +0200
3.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml Mon Aug 26 17:40:27 2019 +0200
3.3 @@ -205,7 +205,7 @@
3.4 and interactively specifiying thys in subpbl is not very relevant.
3.5
3.6 Other solutions possible:
3.7 - # always parse and type-check with Thy_Info_get_theory "Isac"
3.8 + # always parse and type-check with Thy_Info_get_theory "Isac_Knowledge"
3.9 (rejected due to the vague idea eg. to re-use equations for R in C etc.)
3.10 # regard the subthy-relation in specifying thys of subpbls
3.11 # specifically handle 'SubProblem (undefined, pbl, arglist)'
3.12 @@ -710,9 +710,9 @@
3.13 in
3.14 drop ((find_index (curry Context.eq_thy (Thy_Info.get_theory "Complex_Main")) allthys), allthys)
3.15 end
3.16 -fun knowthys () = (*["Isac", .., "Descript"]*)
3.17 +fun knowthys () = (*["Isac_Knowledge", .., "Descript"]*)
3.18 let
3.19 - fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
3.20 + fun isacthys () = (* ["Isac_Knowledge", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
3.21 let
3.22 val allthys = filter_out (member Context.eq_thy
3.23 [(*Thy_Info_get_theory "ProgLang",*) Rule.Thy_Info_get_theory "Interpret",
3.24 @@ -728,9 +728,9 @@
3.25 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys')
3.26 end
3.27
3.28 -fun progthys () = (*["Isac", .., "Descript"]*)
3.29 +fun progthys () = (*["Isac_Knowledge", .., "Descript"]*)
3.30 let
3.31 - fun isacthys () = (* ["Isac", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
3.32 + fun isacthys () = (* ["Isac_Knowledge", .., "KEStore"] without Build_Isac thys: "Interpret" etc *)
3.33 let
3.34 val allthys = filter_out (member Context.eq_thy
3.35 [(*Thy_Info_get_theory "ProgLang",*) Rule.Thy_Info_get_theory "Interpret",
4.1 --- a/src/Tools/isac/CalcElements/rule.sml Mon Aug 26 09:20:07 2019 +0200
4.2 +++ b/src/Tools/isac/CalcElements/rule.sml Mon Aug 26 17:40:27 2019 +0200
4.3 @@ -183,7 +183,7 @@
4.4 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
4.5 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
4.6 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
4.7 -fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac"); (*@{theory "Isac"}*)
4.8 +fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac_Knowledge"); (*@{theory "Isac_Knowledge"}*)
4.9
4.10 fun term_to_string' ctxt t =
4.11 let
4.12 @@ -198,7 +198,7 @@
4.13 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
4.14 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
4.15
4.16 -fun term2str t = term_to_string' (thy2ctxt' "Isac") t;
4.17 +fun term2str t = term_to_string' (thy2ctxt' "Isac_Knowledge") t;
4.18 fun t2str thy t = term_to_string' (thy2ctxt thy) t;
4.19 fun ts2str thy ts = ts |> map (t2str thy) |> strs2str';
4.20 fun terms2strs ts = map term2str ts; (* terms2strs [t1,t2] = ["1 + 2", "abc"]; *)
4.21 @@ -210,7 +210,7 @@
4.22 fun thm2str thm =
4.23 let
4.24 val t = Thm.prop_of thm
4.25 - val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac"))
4.26 + val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
4.27 val ctxt' = Config.put show_markup false ctxt
4.28 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
4.29 fun thms2str thms = (strs2str o (map thm2str)) thms
4.30 @@ -371,12 +371,12 @@
4.31 let
4.32 val ctxt' = Config.put show_markup false (Proof_Context.init_global (Thy_Info_get_theory thyID))
4.33 in Print_Mode.setmp [] (Syntax.string_of_typ ctxt') t end;
4.34 -fun type2str typ = type_to_string'' "Isac" typ; (*TODO legacy*)
4.35 +fun type2str typ = type_to_string'' "Isac_Knowledge" typ; (*TODO legacy*)
4.36 val string_of_typ = type2str; (*legacy*)
4.37 fun string_of_typ_thy thy typ = type_to_string'' thy typ; (*legacy*)
4.38
4.39 (*check for [.] as caused by "fun assoc_thm'"*)
4.40 -fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (Thm.prop_of thm)
4.41 +fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
4.42 fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (Thm.prop_of thm)
4.43 fun string_of_thmI thm =
4.44 let
5.1 --- a/src/Tools/isac/CalcElements/termC.sml Mon Aug 26 09:20:07 2019 +0200
5.2 +++ b/src/Tools/isac/CalcElements/termC.sml Mon Aug 26 17:40:27 2019 +0200
5.3 @@ -496,7 +496,7 @@
5.4 |-> Proof_Context.read_term_pattern
5.5 |> numbers_to_string (*TODO drop*)
5.6 |> typ_a2real; (*TODO drop*)
5.7 -fun str2term str = parse_patt (Rule.Thy_Info_get_theory "Isac") str
5.8 +fun str2term str = parse_patt (Rule.Thy_Info_get_theory "Isac_Knowledge") str
5.9
5.10 (* TODO decide with Test_Isac *)
5.11 fun is_atom t = length (vars t) = 1
6.1 --- a/src/Tools/isac/Frontend/interface.sml Mon Aug 26 09:20:07 2019 +0200
6.2 +++ b/src/Tools/isac/Frontend/interface.sml Mon Aug 26 17:40:27 2019 +0200
6.3 @@ -346,7 +346,7 @@
6.4 let
6.5 val ctxt = get_ctxt pt pold
6.6 val (p, c, _, pt) =
6.7 - Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.Uistate, ctxt) ip pt
6.8 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m (Istate.Uistate, ctxt) ip pt
6.9 in upd_calc cI ((pt, p), []);
6.10 autocalculateOK2xml cI pold (if null c then pold else last_elem c) p
6.11 end)
7.1 --- a/src/Tools/isac/Interpret/calchead.sml Mon Aug 26 09:20:07 2019 +0200
7.2 +++ b/src/Tools/isac/Interpret/calchead.sml Mon Aug 26 17:40:27 2019 +0200
7.3 @@ -824,7 +824,7 @@
7.4 let
7.5 val ctxt = get_ctxt pt pos
7.6 val (pos, _, _, pt) =
7.7 - Generate.generate1 (Celem.assoc_thy "Isac") (Tactic.Refine_Problem' rfd) (Istate.Uistate, ctxt) pos pt
7.8 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Refine_Problem' rfd) (Istate.Uistate, ctxt) pos pt
7.9 in
7.10 (pos(*p,Pbl*), (pos(*p,Pbl*), Istate.Uistate), Generate.RefinedKF rfd, Tactic.Model_Problem, Istate.Safe, pt)
7.11 end
7.12 @@ -955,7 +955,7 @@
7.13 end
7.14 | Err msg => (*TODO.WN03 pass error-msgs to the frontend..
7.15 FIXME ..and dont abuse a tactic for that purpose*)
7.16 - ([(Tactic.Tac msg, Tactic.Tac_ (Rule.Thy_Info_get_theory "Isac", msg,msg,msg),
7.17 + ([(Tactic.Tac msg, Tactic.Tac_ (Rule.Thy_Info_get_theory "Isac_Knowledge", msg,msg,msg),
7.18 (e_pos', (Istate.e_istate, ContextC.e_ctxt)))], [], ptp)
7.19 end
7.20 | nxt_specif_additem sel ct (ptp as (pt, (p, Met))) =
7.21 @@ -1159,7 +1159,7 @@
7.22 let
7.23 val ctxt = get_ctxt pt pos
7.24 val (pos, c, _, pt) =
7.25 - Generate.generate1 (Celem.assoc_thy "Isac") (Tactic.Specify_Theory' dI) (Istate.Uistate, ctxt) pos pt
7.26 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate.Uistate, ctxt) pos pt
7.27 in (*FIXXXME: check if pbl can still be parsed*)
7.28 ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate.Uistate, ctxt)))], c,
7.29 (pt, pos))
7.30 @@ -1167,7 +1167,7 @@
7.31 | nxt_specif (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =
7.32 let
7.33 val ctxt = get_ctxt pt pos
7.34 - val (pos, c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac") (Tactic.Specify_Theory' dI) (Istate.Uistate, ctxt) pos pt
7.35 + val (pos, c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate.Uistate, ctxt) pos pt
7.36 in (*FIXXXME: check if met can still be parsed*)
7.37 ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate.Uistate, ctxt)))], c, (pt, pos))
7.38 end
7.39 @@ -1198,7 +1198,7 @@
7.40 then (* from met-browser *)
7.41 let
7.42 val {ppc, ...} = Specify.get_met mI
7.43 - val dI = if dI = "" then "Isac" else dI
7.44 + val dI = if dI = "" then "Isac_Knowledge" else dI
7.45 val (pt, _) =
7.46 cappend_problem e_ctree [] (Istate.e_istate, ContextC.e_ctxt) ([], (dI, pI, mI)) ([], (dI, pI, mI), Rule.e_term (*FIXME met*))
7.47 val pt = update_spec pt [] (dI, pI, mI)
7.48 @@ -1533,7 +1533,7 @@
7.49 PblObj {origin = (_, ospec, hdf'), spec, probl,...} => (ospec, hdf', spec, probl)
7.50 | _ => error "get_ocalhd Pbl: uncovered case get_obj"
7.51 val {prls, where_, ...} = Specify.get_pbt (#2 (some_spec ospec spec))
7.52 - val pre = Stool.check_preconds (Celem.assoc_thy "Isac") prls where_ probl
7.53 + val pre = Stool.check_preconds (Celem.assoc_thy "Isac_Knowledge") prls where_ probl
7.54 in
7.55 (ocalhd_complete probl pre spec, Pbl, hdf', probl, pre, spec) : ocalhd
7.56 end
7.57 @@ -1543,7 +1543,7 @@
7.58 PblObj {origin = (_, ospec, hdf'), spec, meth, ...} => (ospec, hdf', spec, meth)
7.59 | _ => error "get_ocalhd Met: uncovered case get_obj"
7.60 val {prls, pre, ...} = Specify.get_met (#3 (some_spec ospec spec))
7.61 - val pre = Stool.check_preconds (Celem.assoc_thy "Isac") prls pre meth
7.62 + val pre = Stool.check_preconds (Celem.assoc_thy "Isac_Knowledge") prls pre meth
7.63 in
7.64 (ocalhd_complete meth pre spec, Met, hdf', meth, pre, spec)
7.65 end
8.1 --- a/src/Tools/isac/Interpret/ctree-basic.sml Mon Aug 26 09:20:07 2019 +0200
8.2 +++ b/src/Tools/isac/Interpret/ctree-basic.sml Mon Aug 26 17:40:27 2019 +0200
8.3 @@ -613,7 +613,7 @@
8.4 (apfst bool2str)))) bts;
8.5 fun ocalhd2str (b, p, hdf, itms, prec, spec) = (* for tests only *)
8.6 "(" ^ bool2str b ^ ", " ^ pos_2str p ^ ", " ^ Rule.term2str hdf ^
8.7 - ", " ^ Model.itms2str_ (Rule.thy2ctxt' "Isac") itms ^
8.8 + ", " ^ Model.itms2str_ (Rule.thy2ctxt' "Isac_Knowledge") itms ^
8.9 ", " ^ preconds2str prec ^ ", \n" ^ Celem.spec2str spec ^ " )";
8.10
8.11 fun is_pblnd (Nd (ppobj, _)) = is_pblobj ppobj
9.1 --- a/src/Tools/isac/Interpret/generate.sml Mon Aug 26 09:20:07 2019 +0200
9.2 +++ b/src/Tools/isac/Interpret/generate.sml Mon Aug 26 17:40:27 2019 +0200
9.3 @@ -61,7 +61,7 @@
9.4 | _ => error "init_istate Rewrite_Set: uncovered case assoc_rls")
9.5 | init_istate (Tactic.Rewrite_Set_Inst (subs, rls)) t =
9.6 let
9.7 - val v = case Selem.subs2subst (Celem.assoc_thy "Isac") subs of
9.8 + val v = case Selem.subs2subst (Celem.assoc_thy "Isac_Knowledge") subs of
9.9 (_, v) :: _ => v
9.10 | _ => error "init_istate: uncovered case "
9.11 (*...we suppose the substitution of only _one_ bound variable*)
9.12 @@ -393,7 +393,7 @@
9.13 | generate tacis (pt, c, _: pos'(*!dropped!WN0504redesign generate/tacis?*))=
9.14 let
9.15 val (tacis', (_, tac_, (p, is))) = split_last tacis
9.16 - val (p',c',_,pt') = generate1 (Celem.assoc_thy "Isac") tac_ is p pt
9.17 + val (p',c',_,pt') = generate1 (Celem.assoc_thy "Isac_Knowledge") tac_ is p pt
9.18 in
9.19 generate tacis' (pt', c@c', p')
9.20 end
10.1 --- a/src/Tools/isac/Interpret/inform.sml Mon Aug 26 09:20:07 2019 +0200
10.2 +++ b/src/Tools/isac/Interpret/inform.sml Mon Aug 26 17:40:27 2019 +0200
10.3 @@ -105,7 +105,7 @@
10.4 let
10.5 val (h, argl) = strip_comb hdt
10.6 in
10.7 - case assoc_cas (Celem.assoc_thy "Isac") h of
10.8 + case assoc_cas (Celem.assoc_thy "Isac_Knowledge") h of
10.9 NONE => NONE
10.10 | SOME (spec as (dI,_,_), argl2dtss) =>
10.11 let
10.12 @@ -123,8 +123,8 @@
10.13 end
10.14 end
10.15
10.16 -(*lazy evaluation for (Thy_Info_get_theory "Isac")*)
10.17 -fun Isac _ = Celem.assoc_thy "Isac";
10.18 +(*lazy evaluation for (Thy_Info_get_theory "Isac_Knowledge")*)
10.19 +fun Isac _ = Celem.assoc_thy "Isac_Knowledge";
10.20
10.21 (* re-parse itms with a new thy and prepare for checking with ori list *)
10.22 fun parsitm dI (itm as (i, v, _, f, Model.Cor ((d, ts), _))) =
10.23 @@ -244,7 +244,7 @@
10.24 else oris2itms pbt vat os
10.25
10.26 fun par2fstr (_, _, _, f, Model.Par s) = (f, s)
10.27 - | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (Rule.thy2ctxt' "Isac") itm)
10.28 + | par2fstr itm = error ("par2fstr: called with " ^ Model.itm2str_ (Rule.thy2ctxt' "Isac_Knowledge") itm)
10.29 fun itms2fstr (_, _, _, f, Model.Cor ((d, ts), _)) = (f, Model.comp_dts'' (d, ts))
10.30 | itms2fstr (_, _, _, f, Model.Syn str) = (f, str)
10.31 | itms2fstr (_, _, _, f, Model.Typ str) = (f, str)
10.32 @@ -252,7 +252,7 @@
10.33 | itms2fstr (_, _, _, f, Model.Sup (d, ts)) = (f, Model.comp_dts'' (d, ts))
10.34 | itms2fstr (_, _, _, f, Model.Mis (d, t)) = (f, Rule.term2str (d $ t))
10.35 | itms2fstr (itm as (_, _, _, _, Model.Par _)) =
10.36 - error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt' "Isac") itm ^ "): Par should be internal");
10.37 + error ("parsitm (" ^ Model.itm2str_ (Rule.thy2ctxt' "Isac_Knowledge") itm ^ "): Par should be internal");
10.38
10.39 fun imodel2fstr iitems =
10.40 let
10.41 @@ -285,7 +285,7 @@
10.42 let val pbt = (#ppc o Specify.get_pbt) pI
10.43 val dI' = #1 (Chead.some_spec ospec spec)
10.44 val oris = if pI = #2 ospec then oris
10.45 - else Specify.prep_ori fmz_(Celem.assoc_thy"Isac") pbt |> #1;
10.46 + else Specify.prep_ori fmz_(Celem.assoc_thy"Isac_Knowledge") pbt |> #1;
10.47 in (Ctree.Pbl, appl_adds dI' oris probl pbt
10.48 (map itms2fstr probl), meth) end
10.49 else if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*)
10.50 @@ -300,12 +300,12 @@
10.51 val pt = Ctree.update_spec pt p spec;
10.52 in if pos_ = Ctree.Pbl
10.53 then let val {prls,where_,...} = Specify.get_pbt (#2 (Chead.some_spec ospec spec))
10.54 - val pre = Stool.check_preconds (Celem.assoc_thy"Isac") prls where_ pits
10.55 + val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls where_ pits
10.56 in (Ctree.update_pbl pt p pits,
10.57 (Chead.ocalhd_complete pits pre spec, Ctree.Pbl, hdf', pits, pre, spec): Ctree.ocalhd)
10.58 end
10.59 else let val {prls,pre,...} = Specify.get_met (#3 (Chead.some_spec ospec spec))
10.60 - val pre = Stool.check_preconds (Celem.assoc_thy"Isac") prls pre mits
10.61 + val pre = Stool.check_preconds (Celem.assoc_thy"Isac_Knowledge") prls pre mits
10.62 in (Ctree.update_met pt p mits,
10.63 (Chead.ocalhd_complete mits pre spec, Ctree.Met, hdf', mits, pre, spec) : Ctree.ocalhd)
10.64 end
10.65 @@ -339,11 +339,11 @@
10.66
10.67 fun mk_tacis ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
10.68 (Tactic.Rewrite (id, thm),
10.69 - Tactic.Rewrite' ("Isac", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
10.70 + Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, Lucin.rule2thm'' r, t, (t', a)),
10.71 (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
10.72 | mk_tacis _ _ (t, r as Rule.Rls_ rls, (t', a)) =
10.73 (Tactic.Rewrite_Set (Lucin.rule2rls' r),
10.74 - Tactic.Rewrite_Set' ("Isac", false, rls, t, (t', a)),
10.75 + Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
10.76 (Ctree.e_pos'(*to be updated before generate tacis!!!*), (Istate.Uistate, ContextC.e_ctxt)))
10.77 | mk_tacis _ _ (t, r, _) = error ("mk_tacis: not impl. for " ^ Rule.rule2str r ^ " at " ^ Rule.term2str t)
10.78
10.79 @@ -449,7 +449,7 @@
10.80 (* check if an input formula is exactly equal the rewrite from a rule
10.81 which is stored at the pos where the input is stored of "ok". *)
10.82 fun is_exactly_equal (pt, pos as (p, _)) istr =
10.83 - case TermC.parseNEW (Celem.assoc_thy "Isac" |> Rule.thy2ctxt) istr of
10.84 + case TermC.parseNEW (Celem.assoc_thy "Isac_Knowledge" |> Rule.thy2ctxt) istr of
10.85 NONE => ("syntax error in '" ^ istr ^ "'", Tactic.Tac "")
10.86 | SOME ifo =>
10.87 let
10.88 @@ -479,7 +479,7 @@
10.89 Tactic.Rewrite_Set rlsID => rlsID
10.90 |Tactic.Rewrite_Set_Inst (_, rlsID) => rlsID
10.91 | _ => "e_rls"
10.92 - val (part, thyID) = Rtools.thy_containing_rls "Isac" rlsID;
10.93 + val (part, thyID) = Rtools.thy_containing_rls "Isac_Knowledge" rlsID;
10.94 val rls = case Specify.get_the [part, thyID, "Rulesets", rlsID] of
10.95 Celem.Hrls {thy_rls = (_, rls), ...} => rls
10.96 | _ => error "fetchErrorpatterns: uncovered case of get_the"
11.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Aug 26 09:20:07 2019 +0200
11.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Aug 26 17:40:27 2019 +0200
11.3 @@ -357,15 +357,15 @@
11.4 in assy ya ((E', l @ [Celem.R, Celem.D], a,v,S,b),ss) body end
11.5 | ay => ay)
11.6 | assy (ya as (ctxt,srls,_,_)) ((E,l,_,v,S,b),ss) (Const ("Program.While",_) $ c $ e $ a) =
11.7 - if Rewrite.eval_true_ "Isac" srls (subst_atomic (LTool.upd_env E (a,v)) c)
11.8 + if Rewrite.eval_true_ "Isac_Knowledge" srls (subst_atomic (LTool.upd_env E (a,v)) c)
11.9 then assy ya ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e
11.10 else NasNap (v, E)
11.11 | assy (ya as (ctxt,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("Program.While",_) $ c $ e) =
11.12 - if Rewrite.eval_true_ "Isac" srls (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
11.13 + if Rewrite.eval_true_ "Isac_Knowledge" srls (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
11.14 then assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e
11.15 else NasNap (v, E)
11.16 | assy (ya as (_,srls,_,_)) ((E,l,a,v,S,b),ss) (Const ("If",_) $ c $ e1 $ e2) =
11.17 - if Rewrite.eval_true_ "Isac" srls (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
11.18 + if Rewrite.eval_true_ "Isac_Knowledge" srls (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
11.19 then assy ya ((E, l @ [Celem.L, Celem.R], a,v,S,b),ss) e1
11.20 else assy ya ((E, l @ [Celem.R], a,v,S,b),ss) e2
11.21 | assy ya ((E,l,_,v,S,b),ss) (Const ("Program.Try"(*2*),_) $ e $ a) =
11.22 @@ -404,9 +404,9 @@
11.23 | ay => (ay))
11.24 (*======= end of scanning tacticals, a leaf =======*)
11.25 | assy (ctxt,sr,d,ap) ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss) t =
11.26 - (case Lucin.handle_leaf "locate" "Isac" sr E a v t of
11.27 + (case Lucin.handle_leaf "locate" "Isac_Knowledge" sr E a v t of
11.28 (a', LTool.Expr _) =>
11.29 - (NasNap (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac") sr
11.30 + (NasNap (Rewrite.eval_listexpr_ (Celem.assoc_thy "Isac_Knowledge") sr
11.31 (subst_atomic (Lucin.upd_env_opt E (a',v)) t), E))
11.32 | (a', LTool.STac stac) =>
11.33 let
11.34 @@ -418,22 +418,22 @@
11.35 case Lucin.associate pt ctxt (m, stac) of
11.36 Lucin.Ass (m, v', ctxt) =>
11.37 let val (p'',c',f',pt') =
11.38 - Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.Pstate (E,l,a',v',S,true), ctxt) (p',p_) pt;
11.39 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m (Istate.Pstate (E,l,a',v',S,true), ctxt) (p',p_) pt;
11.40 in Assoc ((E,l,a',v',S,true), (m,f',pt',p'',c @ c')::ss) end
11.41 | Lucin.Ass_Weak (m, v', ctxt) =>
11.42 let val (p'',c',f',pt') =
11.43 - Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.Pstate (E,l,a',v',S,false), ctxt) (p',p_) pt;
11.44 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m (Istate.Pstate (E,l,a',v',S,false), ctxt) (p',p_) pt;
11.45 in Assoc ((E,l,a',v',S,false), (m,f',pt',p'',c @ c')::ss) end
11.46 | Lucin.NotAss =>
11.47 (case ap of (*switch for Or: 1st AssOnly, 2nd AssGen*)
11.48 AssOnly => (NasNap (v, E))
11.49 | _ =>
11.50 - (case Applicable.applicable_in (p,p_) pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac") stac) of
11.51 + (case Applicable.applicable_in (p,p_) pt (Lucin.stac2tac pt (Celem.assoc_thy "Isac_Knowledge") stac) of
11.52 Chead.Appl m' =>
11.53 let
11.54 val is = (E,l,a',Lucin.tac_2res m',S,false(*FIXXXME.WN0?*))
11.55 val (p'',c',f',pt') =
11.56 - Generate.generate1 (Celem.assoc_thy "Isac") m' (Istate.Pstate is, ctxt) (p', p_) pt;
11.57 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m' (Istate.Pstate is, ctxt) (p', p_) pt;
11.58 in NasApp (is,(m,f',pt',p'',c @ c')::ss) end
11.59 | Chead.Notappl _ => (NasNap (v, E))
11.60 )
11.61 @@ -481,7 +481,7 @@
11.62 | ass_up (ys as ((*y,*)ctxt,s,_,d)) ((E,l,_,v,S,b),ss)
11.63 (*(Const ("Program.While",_) $ c $ e $ a) = WN050930 blind fix*)
11.64 (t as Const ("Program.While",_) $ c $ e $ a) =
11.65 - if Rewrite.eval_true_ "Isac" s (subst_atomic (LTool.upd_env E (a,v)) c)
11.66 + if Rewrite.eval_true_ "Isac_Knowledge" s (subst_atomic (LTool.upd_env E (a,v)) c)
11.67 then case assy ((*y,*)ctxt,s,d,Aundef) ((E, l @ [Celem.L, Celem.R], SOME a,v,S,b),ss) e of
11.68 NasNap (v,E') => astep_up ys ((E',l, SOME a,v,S,b),ss)
11.69 | NasApp ((E',l,a,v,S,b),ss) =>
11.70 @@ -491,7 +491,7 @@
11.71 | ass_up (ys as ((*y,*)ctxt,s,_,d)) ((E,l,a,v,S,b),ss)
11.72 (*(Const ("Program.While",_) $ c $ e) = WN050930 blind fix*)
11.73 (t as Const ("Program.While",_) $ c $ e) =
11.74 - if Rewrite.eval_true_ "Isac" s (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
11.75 + if Rewrite.eval_true_ "Isac_Knowledge" s (subst_atomic (Lucin.upd_env_opt E (a,v)) c)
11.76 then case assy ((*y,*)ctxt,s,d,Aundef) ((E, l @ [Celem.R], a,v,S,b),ss) e of
11.77 NasNap (v,E') => astep_up ys ((E',l, a,v,S,b),ss)
11.78 | NasApp ((E',l,a,v,S,b),ss) =>
11.79 @@ -565,7 +565,7 @@
11.80 (Rule.Rfuns {locate_rule=lo,...}, _) (Istate.RrlsState (_,f'',rss,rts), _) =
11.81 (case lo rss f (Rule.Thm thm) of
11.82 [] => NotLocatable
11.83 - | rts' => Steps (Lucin.rts2steps [] ((pt,p),(f,f'',rss,rts),("Isac",ro,er,pa)) rts') ) *)
11.84 + | rts' => Steps (Lucin.rts2steps [] ((pt,p),(f,f'',rss,rts),("Isac_Knowledge",ro,er,pa)) rts') ) *)
11.85 (*| locate_input_tactic (thy', srls) m (pt, p)
11.86 (scr as Rule.Prog _, d) (Istate.Pstate (E,l,a,v,S,b), ctxt) = *)
11.87 fun locate_input_tactic (progr as Rule.Prog _) (cstate as (pt, pos)) istate ctxt tac =
11.88 @@ -702,7 +702,7 @@
11.89 (p, Met) => ((lev_on o lev_dn) p, Frm) (* begin script *)
11.90 | (p, Res) => (lev_on p, Res) (* somewhere in script *)
11.91 | _ => pos
11.92 - val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac") tac_ is pos pt;
11.93 + val (pos', c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac_ is pos pt;
11.94 in
11.95 ([(Lucin.tac_2tac tac_, tac_, (pos, is))], c, (pt, pos'))
11.96 end
12.1 --- a/src/Tools/isac/Interpret/mathengine.sml Mon Aug 26 09:20:07 2019 +0200
12.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Mon Aug 26 17:40:27 2019 +0200
12.3 @@ -281,7 +281,7 @@
12.4 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
12.5 else pI'
12.6 val {ppc, where_, prls, ...} = Specify.get_pbt pblID
12.7 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc, where_, prls) os
12.8 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") probl (ppc, where_, prls) os
12.9 in
12.10 (model_ok, pblID, hdl, pbl, pre)
12.11 end
12.12 @@ -296,7 +296,7 @@
12.13 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
12.14 else mI'
12.15 val {ppc, pre, prls, scr, ...} = Specify.get_met metID
12.16 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") meth (ppc,pre,prls) os
12.17 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") meth (ppc,pre,prls) os
12.18 in
12.19 (model_ok, metID, scr, pbl, pre)
12.20 end
12.21 @@ -309,7 +309,7 @@
12.22 Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
12.23 | Ctree.PrfObj _ => error "context_pbl: uncovered case"
12.24 val {ppc,where_,prls,...} = Specify.get_pbt pI
12.25 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc,where_,prls) os
12.26 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") probl (ppc,where_,prls) os
12.27 in
12.28 (model_ok, pI, hdl, pbl, pre)
12.29 end
12.30 @@ -321,7 +321,7 @@
12.31 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
12.32 | Ctree.PrfObj _ => error "context_met: uncovered case"
12.33 val {ppc,pre,prls,scr,...} = Specify.get_met mI
12.34 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") meth (ppc,pre,prls) os
12.35 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") meth (ppc,pre,prls) os
12.36 in
12.37 (model_ok, mI, scr, pbl, pre)
12.38 end
12.39 @@ -333,11 +333,11 @@
12.40 Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
12.41 | Ctree.PrfObj _ => error "context_met: uncovered case"
12.42 in
12.43 - case Specify.refine_pbl (Celem.assoc_thy "Isac") pI probl of
12.44 + case Specify.refine_pbl (Celem.assoc_thy "Isac_Knowledge") pI probl of
12.45 NONE => (*copy from context_pbl*)
12.46 let
12.47 val {ppc,where_,prls,...} = Specify.get_pbt pI
12.48 - val (_, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc,where_,prls) os
12.49 + val (_, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") probl (ppc,where_,prls) os
12.50 in
12.51 (false, pI, hdl, pbl, pre)
12.52 end
12.53 @@ -375,7 +375,7 @@
12.54 (case p_ of Ctree.Pbl => Generate.Problem []
12.55 | Ctree.Met => Generate.Method []
12.56 | _ => error "TESTg_form: uncovered case",
12.57 - Specify.itms2itemppc (Celem.assoc_thy"Isac") gfr pre))
12.58 + Specify.itms2itemppc (Celem.assoc_thy"Isac_Knowledge") gfr pre))
12.59 end
12.60
12.61 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
12.62 @@ -396,32 +396,33 @@
12.63 NEW loeschen, eigene Version von locatetac, step
12.64 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
12.65
12.66 -fun me (_, tac) p _(*NEW remove*) pt =
12.67 - let
12.68 - val (pt, p) =
12.69 - (*locatetac is here for testing by me; step would suffice in me*)
12.70 - case locatetac tac (pt, p) of
12.71 - ("ok", (_, _, ptp)) => ptp
12.72 - | ("unsafe-ok", (_, _, ptp)) => ptp
12.73 - | ("not-applicable",_) => (pt, p)
12.74 - | ("end-of-calculation", (_, _, ptp)) => ptp
12.75 - | ("failure", _) => error "sys-error"
12.76 - | _ => error "me: uncovered case"
12.77 - val (_, ts) =
12.78 - (case step p ((pt, Ctree.e_pos'), []) of
12.79 - ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
12.80 - | ("helpless", _) => ("helpless: cannot propose tac", [])
12.81 - | ("no-fmz-spec", _) => error "no-fmz-spec"
12.82 - | ("end-of-calculation", (ts, _, _)) => ("", ts)
12.83 - | _ => error "me: uncovered case")
12.84 - handle ERROR msg => raise ERROR msg
12.85 - val tac =
12.86 - case ts of
12.87 - tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
12.88 - | _ => if p = ([], Ctree.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
12.89 - in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
12.90 - (Tactic.tac2IDstr tac, tac), Istate.Sundef, pt)
12.91 - end
12.92 +fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
12.93 + | me*) (_, tac) p _(*NEW remove*) pt =
12.94 + let
12.95 + val (pt, p) =
12.96 + (*locatetac is here for testing by me; step would suffice in me*)
12.97 + case locatetac tac (pt, p) of
12.98 + ("ok", (_, _, ptp)) => ptp
12.99 + | ("unsafe-ok", (_, _, ptp)) => ptp
12.100 + | ("not-applicable",_) => (pt, p)
12.101 + | ("end-of-calculation", (_, _, ptp)) => ptp
12.102 + | ("failure", _) => error "sys-error"
12.103 + | _ => error "me: uncovered case"
12.104 + val (_, ts) =
12.105 + (case step p ((pt, Ctree.e_pos'), []) of
12.106 + ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
12.107 + | ("helpless", _) => ("helpless: cannot propose tac", [])
12.108 + | ("no-fmz-spec", _) => error "no-fmz-spec"
12.109 + | ("end-of-calculation", (ts, _, _)) => ("", ts)
12.110 + | _ => error "me: uncovered case")
12.111 + handle ERROR msg => raise ERROR msg
12.112 + val tac =
12.113 + case ts of
12.114 + tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
12.115 + | _ => if p = ([], Ctree.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
12.116 + in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
12.117 + (Tactic.tac2IDstr tac, tac), Istate.Sundef, pt)
12.118 + end
12.119
12.120 (* for quick test-print-out, until 'type inout' is removed *)
12.121 fun f2str (Generate.FormKF cterm') = cterm'
13.1 --- a/src/Tools/isac/Interpret/model.sml Mon Aug 26 09:20:07 2019 +0200
13.2 +++ b/src/Tools/isac/Interpret/model.sml Mon Aug 26 17:40:27 2019 +0200
13.3 @@ -198,17 +198,17 @@
13.4 (* revert split_:
13.5 WN050903 we do NOT know which is from subtheory, description or term;
13.6 typecheck thus may lead to TYPE-error 'unknown constant';
13.7 - solution: typecheck with (Thy_Info_get_theory "Isac"); i.e. arg 'thy' superfluous*)
13.8 + solution: typecheck with (Thy_Info_get_theory "Isac_Knowledge"); i.e. arg 'thy' superfluous*)
13.9 (*fun comp_dts thy (d,[]) =
13.10 - Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac"*)
13.11 - (Thy_Info_get_theory "Isac")
13.12 + Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
13.13 + (Thy_Info_get_theory "Isac_Knowledge")
13.14 (*comp_dts:FIXXME stay with term for efficiency !!!*)
13.15 (if is_reall_dsc d then (d $ e_listReal)
13.16 else if is_booll_dsc d then (d $ e_listBool)
13.17 else d)
13.18 | comp_dts (d,ts) =
13.19 - (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac"*)
13.20 - (Thy_Info_get_theory "Isac")
13.21 + (Thm.global_cterm_of (*(sign_of o assoc_thy) "Isac_Knowledge"*)
13.22 + (Thy_Info_get_theory "Isac_Knowledge")
13.23 (*comp_dts:FIXXME stay with term for efficiency !!*)
13.24 (d $ (comp_ts (d, ts)))
13.25 handle _ => error ("comp_dts: "^(term2str d)^
13.26 @@ -441,7 +441,7 @@
13.27 | itm_2str_ ctxt (Mis (d, pid)) =
13.28 "Mis "^ Rule.term_to_string' ctxt d ^ " " ^ Rule.term_to_string' ctxt pid
13.29 | itm_2str_ _ (Par s) = "Trm "^s;
13.30 -fun itm_2str t = itm_2str_ (Rule.thy2ctxt' "Isac") t;
13.31 +fun itm_2str t = itm_2str_ (Rule.thy2ctxt' "Isac_Knowledge") t;
13.32 fun itm2str_ ctxt ((i, is, b, s, itm_):itm) =
13.33 "(" ^ string_of_int i ^ " ," ^ ints2str' is ^ " ," ^ bool2str b ^ " ," ^
13.34 s ^ " ," ^ itm_2str_ ctxt itm_ ^ ")";
14.1 --- a/src/Tools/isac/Interpret/mstools.sml Mon Aug 26 09:20:07 2019 +0200
14.2 +++ b/src/Tools/isac/Interpret/mstools.sml Mon Aug 26 17:40:27 2019 +0200
14.3 @@ -72,7 +72,7 @@
14.4 (*NOT ALL Free's have been substituted, eg. because of incomplete model*)
14.5 (false, pre)
14.6 | evalprecond prls (true, pre) =
14.7 - if Rewrite.eval_true (Celem.assoc_thy "Isac") (* for Pattern.match *)
14.8 + if Rewrite.eval_true (Celem.assoc_thy "Isac_Knowledge") (* for Pattern.match *)
14.9 [pre] prls (* pre parsed, prls.thy *)
14.10 then (true , pre)
14.11 else (false , pre);
14.12 @@ -93,6 +93,6 @@
14.13 fun common_subthy (thy1, thy2) =
14.14 if Context.subthy (thy1, thy2) then thy2
14.15 else if Context.subthy (thy2, thy1) then thy1
14.16 - else Celem.assoc_thy "Isac"
14.17 + else Celem.assoc_thy "Isac_Knowledge"
14.18
14.19 end;
15.1 --- a/src/Tools/isac/Interpret/script.sml Mon Aug 26 09:20:07 2019 +0200
15.2 +++ b/src/Tools/isac/Interpret/script.sml Mon Aug 26 17:40:27 2019 +0200
15.3 @@ -349,7 +349,7 @@
15.4 else Ass_Weak (m ,f', ctxt)
15.5 else NotAss
15.6 | (Const ("Program.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ _ $ f_) =>
15.7 - let val thy = Celem.assoc_thy "Isac";
15.8 + let val thy = Celem.assoc_thy "Isac_Knowledge";
15.9 in
15.10 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
15.11 (assoc_rls (HOLogic.dest_string rls_))
15.12 @@ -360,7 +360,7 @@
15.13 else NotAss
15.14 end
15.15 | (Const ("Program.Rewrite'_Set",_) $ rls_ $ _ $ f_) =>
15.16 - let val thy = Celem.assoc_thy "Isac";
15.17 + let val thy = Celem.assoc_thy "Isac_Knowledge";
15.18 in
15.19 if Rtools.contains_rule (Rule.Calc (assoc_calc' thy op_ |> snd))
15.20 (assoc_rls (HOLogic.dest_string rls_))
16.1 --- a/src/Tools/isac/Interpret/solve.sml Mon Aug 26 09:20:07 2019 +0200
16.2 +++ b/src/Tools/isac/Interpret/solve.sml Mon Aug 26 17:40:27 2019 +0200
16.3 @@ -141,7 +141,7 @@
16.4 LucinNEW.Safe_Step (cstate, istate, ctxt, tac) =>
16.5 ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate))
16.6 | _ => (* NotLocatable *)
16.7 - let val (p, ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, Frm) pt;
16.8 + let val (p, ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, Frm) pt;
16.9 in
16.10 ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt, p)))
16.11 end
16.12 @@ -224,7 +224,7 @@
16.13 ("ok", ([(Lucin.tac_2tac tac, tac, (snd cstate, (istate, ctxt)))], [(*ctree NOT cut*)], cstate))
16.14 | _ => (* NotLocatable *)
16.15 let
16.16 - val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac") m (p, p_) pt;
16.17 + val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, p_) pt;
16.18 in
16.19 ("not-found-in-script", ([(Lucin.tac_2tac m, m, (po, is))], ps, (pt, p)))
16.20 end
16.21 @@ -317,7 +317,7 @@
16.22 is wrong for simpl, but working ?!? *)
16.23 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
16.24 val pos' = ((lev_on o lev_dn) p, Frm)
16.25 - val thy = Celem.assoc_thy "Isac"
16.26 + val thy = Celem.assoc_thy "Isac_Knowledge"
16.27 val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *)
16.28 val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')
16.29 val newnds = children (get_nd pt'' p)
16.30 @@ -339,7 +339,7 @@
16.31 let
16.32 val ctxt = get_ctxt pt pos (*see TODO.thy*)
16.33 in
16.34 - case TermC.parse (Celem.assoc_thy "Isac") istr of
16.35 + case TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr of
16.36 NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate' (*TODO: previous cs'*))
16.37 | SOME f_in =>
16.38 let
17.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Mon Aug 26 09:20:07 2019 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Mon Aug 26 17:40:27 2019 +0200
17.3 @@ -4,7 +4,7 @@
17.4
17.5 theory Build_Thydata
17.6 imports
17.7 - Isac "~~/src/Tools/isac/Interpret/Interpret"
17.8 + Isac_Knowledge "~~/src/Tools/isac/Interpret/Interpret"
17.9 Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*)
17.10 begin
17.11
17.12 @@ -27,14 +27,14 @@
17.13 val allthys = Theory.ancestors_of @{theory};
17.14 val allthys = filter_out (member Context.eq_thy (* thys for isac bootstrap *)
17.15 [(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory xmlsrc},
17.16 - @{theory Frontend}, knowledge_parent]) allthys (*["Isac", ..., "Isac"]*)
17.17 + @{theory Frontend}, knowledge_parent]) allthys (*["Isac_Knowledge", ..., "Isac_Knowledge"]*)
17.18
17.19 - val isabthys' = (*["Complex_Main", "Taylor", .., "Isac"]*)
17.20 + val isabthys' = (*["Complex_Main", "Taylor", .., "Isac_Knowledge"]*)
17.21 drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
17.22 - val isacthys' = (*["Isac", "Inverse_Z_Transform", .., "KEStore"]*)
17.23 + val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "KEStore"]*)
17.24 take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
17.25
17.26 - val knowthys' = (*["Isac", .., "Descript"]*)
17.27 + val knowthys' = (*["Isac_Knowledge", .., "Descript"]*)
17.28 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
17.29 val progthys' = (*["Program", "Tools", "ListC", "KEStore"]*)
17.30 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
18.1 --- a/src/Tools/isac/Knowledge/Diff.thy Mon Aug 26 09:20:07 2019 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Aug 26 17:40:27 2019 +0200
18.3 @@ -405,7 +405,7 @@
18.4 \<close>
18.5 setup \<open>KEStore_Elems.add_cas
18.6 [((Thm.term_of o the o (TermC.parse thy)) "Diff",
18.7 - (("Isac", ["derivative_of","function"], ["no_met"]), argl2dtss))]\<close>
18.8 + (("Isac_Knowledge", ["derivative_of","function"], ["no_met"]), argl2dtss))]\<close>
18.9 ML \<open>
18.10
18.11 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
18.12 @@ -422,6 +422,6 @@
18.13 \<close>
18.14 setup \<open>KEStore_Elems.add_cas
18.15 [((Thm.term_of o the o (TermC.parse thy)) "Differentiate",
18.16 - (("Isac", ["named","derivative_of","function"], ["no_met"]), argl2dtss))]\<close>
18.17 + (("Isac_Knowledge", ["named","derivative_of","function"], ["no_met"]), argl2dtss))]\<close>
18.18
18.19 end
19.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Mon Aug 26 09:20:07 2019 +0200
19.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Mon Aug 26 17:40:27 2019 +0200
19.3 @@ -122,7 +122,7 @@
19.4 m_x = SubProblem (''DiffApp'', [''on_interval'', ''maximum_of'', ''function''],
19.5 [''DiffApp'', ''max_on_interval_by_calculus''])
19.6 [BOOL t_t, REAL v_v, REAL_SET itv_v]
19.7 - in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac'', ''find_values''])
19.8 + in SubProblem (''DiffApp'',[''find_values'', ''tool''], [''Isac_Knowledge'', ''find_values''])
19.9 [REAL m_x, REAL (rhs t_t), REAL v_v, REAL m_m, BOOL_LIST (dropWhile (ident e_e) r_s)])"
19.10 setup \<open>KEStore_Elems.add_mets
19.11 [Specify.prep_met thy "met_diffapp_max" [] Celem.e_metID
20.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Mon Aug 26 09:20:07 2019 +0200
20.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Aug 26 17:40:27 2019 +0200
20.3 @@ -147,7 +147,7 @@
20.4 | ord => ord)
20.5 and hd_ord (f, g) = (* ~ term.ML *)
20.6 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
20.7 -and terms_ord str pr (ts, us) = list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);
20.8 +and terms_ord str pr (ts, us) = list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
20.9 (**)
20.10 in
20.11 (**)
21.1 --- a/src/Tools/isac/Knowledge/Equation.thy Mon Aug 26 09:20:07 2019 +0200
21.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Mon Aug 26 17:40:27 2019 +0200
21.3 @@ -77,7 +77,7 @@
21.4 [((Thm.term_of o the o (TermC.parse thy)) "solveTest",
21.5 (("Test", ["univariate","equation","test"], ["no_met"]), argl2dtss)),
21.6 ((Thm.term_of o the o (TermC.parse thy)) "solve",
21.7 - (("Isac", ["univariate","equation"], ["no_met"]), argl2dtss))]\<close>
21.8 + (("Isac_Knowledge", ["univariate","equation"], ["no_met"]), argl2dtss))]\<close>
21.9
21.10
21.11 setup \<open>KEStore_Elems.add_mets
22.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon Aug 26 09:20:07 2019 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Mon Aug 26 17:40:27 2019 +0200
22.3 @@ -103,7 +103,7 @@
22.4 X'_z = lhs X';
22.5 zzz = argument_in X'_z;
22.6 funterm = rhs X';
22.7 - pbz = SubProblem (''Isac'',
22.8 + pbz = SubProblem (''Isac_Knowledge'',
22.9 [''partial_fraction'',''rational'',''simplification''],
22.10 [''simplification'',''of_rationals'',''to_partial_fraction''])
22.11 [REAL funterm, REAL zzz];
23.1 --- a/src/Tools/isac/Knowledge/Isac.thy Mon Aug 26 09:20:07 2019 +0200
23.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
23.3 @@ -1,34 +0,0 @@
23.4 -(* theory collecting all knowledge defined so far
23.5 - WN.11.00
23.6 - *)
23.7 -
23.8 -theory Isac
23.9 -imports "~~/src/Tools/isac/Frontend/Frontend"
23.10 - PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin InsSort
23.11 - DiophantEq Inverse_Z_Transform Test
23.12 - (*THIS WAITS UNITL Isabelle2013 (? how include into dependency graph?).....
23.13 - ..... GCD_Poly_FP*)
23.14 -begin
23.15 -
23.16 -text \<open>dependencies alternative to those defined by R.Lang during his thesis:
23.17 -
23.18 - Poly Root
23.19 - |\__________ |
23.20 - | \ |
23.21 - | Rational |
23.22 - | | |
23.23 - PolyEq RatEq RootEq
23.24 - \ / \ /
23.25 - \ / \ /
23.26 - RatPolyEq RatRootEq etc.
23.27 -\<close>
23.28 -
23.29 -ML \<open>val version_isac = "isac version 120504 15:33";\<close>
23.30 -ML \<open>
23.31 -"~~~~~ fun xxx , args:"; val () = ();
23.32 -\<close> ML \<open>
23.33 -\<close> ML \<open>
23.34 -"~~~~~ fun xxx , args:"; val () = ();
23.35 -\<close>
23.36 -
23.37 -end
24.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
24.2 +++ b/src/Tools/isac/Knowledge/Isac_Knowledge.thy Mon Aug 26 17:40:27 2019 +0200
24.3 @@ -0,0 +1,34 @@
24.4 +(* theory collecting all knowledge defined so far
24.5 + WN.11.00
24.6 + *)
24.7 +
24.8 +theory Isac_Knowledge
24.9 +imports "~~/src/Tools/isac/Frontend/Frontend"
24.10 + PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin InsSort
24.11 + DiophantEq Inverse_Z_Transform Test
24.12 + (*THIS WAITS UNITL Isabelle2013 (? how include into dependency graph?).....
24.13 + ..... GCD_Poly_FP*)
24.14 +begin
24.15 +
24.16 +text \<open>dependencies alternative to those defined by R.Lang during his thesis:
24.17 +
24.18 + Poly Root
24.19 + |\__________ |
24.20 + | \ |
24.21 + | Rational |
24.22 + | | |
24.23 + PolyEq RatEq RootEq
24.24 + \ / \ /
24.25 + \ / \ /
24.26 + RatPolyEq RatRootEq etc.
24.27 +\<close>
24.28 +
24.29 +ML \<open>val version_isac = "isac version 120504 15:33";\<close>
24.30 +ML \<open>
24.31 +"~~~~~ fun xxx , args:"; val () = ();
24.32 +\<close> ML \<open>
24.33 +\<close> ML \<open>
24.34 +"~~~~~ fun xxx , args:"; val () = ();
24.35 +\<close>
24.36 +
24.37 +end
25.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Aug 26 09:20:07 2019 +0200
25.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Aug 26 17:40:27 2019 +0200
25.3 @@ -214,13 +214,13 @@
25.4 eq_a = (Rewrite_Set ''norm_Rational'' False) eq_a;
25.5 \<comment> \<open>----- ([7], Pbl), solve (3 = 3 * AA / 4, AA)\<close>
25.6 \<comment> \<open>([7], Res), [AA = 4]\<close>
25.7 - sol_a = SubProblem (''Isac'', [''univariate'',''equation''], [''no_met''])
25.8 + sol_a = SubProblem (''Isac_Knowledge'', [''univariate'',''equation''], [''no_met''])
25.9 [BOOL eq_a, REAL (AA::real)] ; \<comment> \<open>a = 4\<close>
25.10 a = rhs (NTH 1 sol_a); \<comment> \<open>([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)\<close>
25.11 eq_b = Take eq; \<comment> \<open>([8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)\<close>
25.12 eq_b = Substitute [zzz = z2] eq_b; \<comment> \<open>([9], Res), 3 = -3 * BB / 4\<close>
25.13 eq_b = (Rewrite_Set ''norm_Rational'' False) eq_b; \<comment> \<open>([10], Pbl), solve (3 = -3 * BB / 4, BB)\<close>
25.14 - sol_b = SubProblem (''Isac'', \<comment> \<open>([10], Res), [BB = -4]\<close>
25.15 + sol_b = SubProblem (''Isac_Knowledge'', \<comment> \<open>([10], Res), [BB = -4]\<close>
25.16 [''univariate'',''equation''], [''no_met''])
25.17 [BOOL eq_b, REAL (BB::real)]; \<comment> \<open>b = -4\<close>
25.18 b = rhs (NTH 1 sol_b); \<comment> \<open>eqr = AA / (z - 1 / 2) + BB / (z - -1 / 4)\<close>
26.1 --- a/src/Tools/isac/Knowledge/Poly.thy Mon Aug 26 09:20:07 2019 +0200
26.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Aug 26 17:40:27 2019 +0200
26.3 @@ -501,7 +501,7 @@
26.4 and hd_ord (f, g) = (* ~ term.ML *)
26.5 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
26.6 and terms_ord _ pr (ts, us) =
26.7 - list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);
26.8 + list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
26.9
26.10 in
26.11
27.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Mon Aug 26 09:20:07 2019 +0200
27.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Aug 26 17:40:27 2019 +0200
27.3 @@ -1,7 +1,7 @@
27.4 (* theory collecting all knowledge
27.5 (predicates 'is_rootEq_in', 'is_sqrt_in', 'is_ratEq_in')
27.6 for PolynomialEquations.
27.7 - alternative dependencies see @{theory "Isac"}
27.8 + alternative dependencies see @{theory "Isac_Knowledge"}
27.9 created by: rlang
27.10 date: 02.07
27.11 changed by: rlang
27.12 @@ -1186,7 +1186,7 @@
27.13 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord)
27.14 int_ord (dest_hd' x f, dest_hd' x g)
27.15 and terms_ord x str pr (ts, us) =
27.16 - list_ord (term_ord' x pr (Celem.assoc_thy "Isac"))(ts, us);
27.17 + list_ord (term_ord' x pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
27.18
27.19 in
27.20
28.1 --- a/src/Tools/isac/Knowledge/Root.thy Mon Aug 26 09:20:07 2019 +0200
28.2 +++ b/src/Tools/isac/Knowledge/Root.thy Mon Aug 26 17:40:27 2019 +0200
28.3 @@ -137,7 +137,7 @@
28.4 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
28.5 (dest_hd' f, dest_hd' g)
28.6 and terms_ord str pr (ts, us) =
28.7 - list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);
28.8 + list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
28.9
28.10 in
28.11 (* associates a+(b+c) => (a+b)+c = a+b+c ... avoiding parentheses
29.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Mon Aug 26 09:20:07 2019 +0200
29.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Mon Aug 26 17:40:27 2019 +0200
29.3 @@ -66,8 +66,8 @@
29.4 \<close>
29.5 setup \<open>KEStore_Elems.add_cas
29.6 [((Thm.term_of o the o (TermC.parse thy)) "Simplify",
29.7 - (("Isac", ["simplification"], ["no_met"]), argl2dtss)),
29.8 + (("Isac_Knowledge", ["simplification"], ["no_met"]), argl2dtss)),
29.9 ((Thm.term_of o the o (TermC.parse thy)) "Vereinfache",
29.10 - (("Isac", ["vereinfachen"], ["no_met"]), argl2dtss))]\<close>
29.11 + (("Isac_Knowledge", ["vereinfachen"], ["no_met"]), argl2dtss))]\<close>
29.12
29.13 end
29.14 \ No newline at end of file
30.1 --- a/src/Tools/isac/Knowledge/Test.thy Mon Aug 26 09:20:07 2019 +0200
30.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Aug 26 17:40:27 2019 +0200
30.3 @@ -342,7 +342,7 @@
30.4 and hd_ord (f, g) = (* ~ term.ML *)
30.5 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
30.6 and terms_ord str pr (ts, us) =
30.7 - list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);
30.8 + list_ord (term_ord' pr (Celem.assoc_thy "Isac_Knowledge"))(ts, us);
30.9 in
30.10
30.11 fun ord_make_polytest (pr:bool) thy (_: Rule.subst) tu =
31.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Mon Aug 26 09:20:07 2019 +0200
31.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Mon Aug 26 17:40:27 2019 +0200
31.3 @@ -87,9 +87,9 @@
31.4 (* make the term 'Subproblem (domID, pblID)' to a formula for frontend;
31.5 needs to be here after def. Subproblem in Program.thy *)
31.6 val subpbl_t $ (pair_t $ _ $ _) = (Thm.term_of o the o (TermC.parse @{theory Program}))
31.7 - "Subproblem (''Isac'',[''equation'',''univar''])"
31.8 + "Subproblem (''Isac_Knowledge'',[''equation'',''univar''])"
31.9 val pbl_t $ _ =
31.10 - (Thm.term_of o the o (TermC.parse @{theory Program})) "Problem (''Isac'',[''equation'',''univar''])"
31.11 + (Thm.term_of o the o (TermC.parse @{theory Program})) "Problem (''Isac_Knowledge'',[''equation'',''univar''])"
31.12
31.13 fun subpbl domID pblID =
31.14 subpbl_t $ (pair_t $ HOLogic.mk_string domID $
32.1 --- a/src/Tools/isac/TODO.thy Mon Aug 26 09:20:07 2019 +0200
32.2 +++ b/src/Tools/isac/TODO.thy Mon Aug 26 17:40:27 2019 +0200
32.3 @@ -45,13 +45,6 @@
32.4 \item xxx
32.5 \item xxx
32.6 \end{itemize}
32.7 - \item rm Delete.thy
32.8 - \begin{itemize}
32.9 - \item Atools requires "fun calcul", "fun float_op_var", term_of_float ?!?
32.10 - \item xxx
32.11 - \item xxx
32.12 - \end{itemize}
32.13 - \item Isac.thy --> All_Knowledge.thy
32.14 \item xxx
32.15 \item xxx
32.16 \end{itemize}
32.17 @@ -72,6 +65,11 @@
32.18 \item Check_Elementwise "Assumptions": prerequisite for ^^goal
32.19 rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
32.20 \item xxx
32.21 + \item clenup fun me:
32.22 + fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
32.23 + | me*) (_, tac) p _(*NEW remove*) pt =
32.24 + + -------------------------^^^^^^
32.25 + \item xxx
32.26 \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
32.27 \item rm ctxt from Subproblem' (is separated in associate!))
32.28 \item check Tactic.Subproblem': are 2 terms required?
32.29 @@ -79,7 +77,7 @@
32.30 \item Test_Some.--- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts --
32.31 --: wait for deleting Check_Elementwise Assumptions
32.32 \item xxx
32.33 - \item lucas-intrpreter.assy: Generate.generate1 (Celem.assoc_thy "Isac")
32.34 + \item lucas-intrpreter.assy: Generate.generate1 (Celem.assoc_thy "Isac_Knowledge")
32.35 \end{itemize}
32.36 \item xxx
32.37 \item complete mstools.sml (* survey on handling contexts:
32.38 @@ -100,7 +98,7 @@
32.39 \item xxx
32.40 \item in locate_input_tactic .. ?assy?; Program.is_eval_expr .use Term.exists_Const
32.41 \item xxx
32.42 - \item change Lucin.handle_leaf "locate" "Isac" sr E a v t
32.43 + \item change Lucin.handle_leaf "locate" "Isac_Knowledge" sr E a v t
32.44 to Lucin.handle_leaf "locate" ctxt ( pstate ) !!srls in scrstate!!^^
32.45 and redesign handle_leaf .. subst_stacexpr .. associate
32.46 to Tactic.from_code :
32.47 @@ -153,7 +151,7 @@
32.48 \item ? what is the difference headline <--> cascmd in
32.49 Subproblem' (spec, oris, headline, fmz_, context, cascmd)
32.50 \item xxx
32.51 - \item inform: TermC.parse (Celem.assoc_thy "Isac") istr --> parseNEW context istr
32.52 + \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr
32.53 \item extract common code from associate.. stac2tac_
32.54 \end{itemize}
32.55 \<close>
32.56 @@ -307,7 +305,7 @@
32.57 \item 1. Rewrite.eval_true_, then
32.58 Lucin.handle_leaf, Rewrite.eval_listexpr_, Generate.generate1, Lucin.stac2tac.
32.59 \item fun associate
32.60 - let val thy = Celem.assoc_thy "Isac";(*TODO*)
32.61 + let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
32.62 \item xxx
32.63 \item xxx
32.64 \item xxx
33.1 --- a/src/Tools/isac/xmlsrc/datatypes.sml Mon Aug 26 09:20:07 2019 +0200
33.2 +++ b/src/Tools/isac/xmlsrc/datatypes.sml Mon Aug 26 17:40:27 2019 +0200
33.3 @@ -453,13 +453,13 @@
33.4 XML.Elem (("VALUE", []), [value])])) = (xml_to_term id, xml_to_term value)
33.5 | xml_to_sub x = raise ERROR ("xml_to_sub wrong arg: " ^ xmlstr 0 x)
33.6 fun xml_of_subs (subs : Selem.subs) =
33.7 - XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.subs2subst (Celem.assoc_thy "Isac") subs))
33.8 + XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.subs2subst (Celem.assoc_thy "Isac_Knowledge") subs))
33.9 fun xml_to_subs
33.10 (XML.Elem (("SUBSTITUTION", []),
33.11 subs)) = Selem.subst2subs (map xml_to_sub subs)
33.12 | xml_to_subs x = raise ERROR ("xml_to_subs wrong arg: " ^ xmlstr 0 x)
33.13 fun xml_of_sube sube =
33.14 - XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.sube2subst (Celem.assoc_thy "Isac") sube))
33.15 + XML.Elem (("SUBSTITUTION", []), map xml_of_sub (Selem.sube2subst (Celem.assoc_thy "Isac_Knowledge") sube))
33.16 fun xml_to_sube
33.17 (XML.Elem (("SUBSTITUTION", []),
33.18 xml_var_val_pairs)) = Selem.subst2sube (map xml_to_sub xml_var_val_pairs)
34.1 --- a/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Mon Aug 26 09:20:07 2019 +0200
34.2 +++ b/src/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Mon Aug 26 17:40:27 2019 +0200
34.3 @@ -109,7 +109,7 @@
34.4 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
34.5 fun pbl2term thy (pblRD: Specify.pblRD) = (*WN120405.TODO.txt*)
34.6 TermC.str2term ("Problem (" ^ (get_thy o Rule.theory2domID) thy ^ "', " ^ (strs2str' o rev) pblRD ^ ")");
34.7 -(* term2str (pbl2term (Thy_Info_get_theory "Isac") ["equations","univariate","normalise"]);
34.8 +(* term2str (pbl2term (Thy_Info_get_theory "Isac_Knowledge") ["equations","univariate","normalise"]);
34.9 val it = "Problem (Isac, [normalise, univariate, equations])" : string
34.10 *)
34.11 val i = indentation;
34.12 @@ -193,7 +193,7 @@
34.13 (*######## ATTENTION: THIS IS not THE ACTUAL VERSION ################*)
34.14 fun met2xml (id: Celem.metID) ({guh,mathauthors,init,ppc,pre,scr,calc,
34.15 crls,erls,errpats,nrls,prls,srls,rew_ord'}: Celem.met) =
34.16 - let val thy' = "Isac" (*FIXME.WN0607 get thy from met ?!?*)
34.17 + let val thy' = "Isac_Knowledge" (*FIXME.WN0607 get thy from met ?!?*)
34.18 val crls' = (#id o Rule.rep_rls) crls
34.19 val erls' = (#id o Rule.rep_rls) erls
34.20 val nrls' = (#id o Rule.rep_rls) nrls
35.1 --- a/test/Tools/isac/ADDTESTS/All_Ctxt.thy Mon Aug 26 09:20:07 2019 +0200
35.2 +++ b/test/Tools/isac/ADDTESTS/All_Ctxt.thy Mon Aug 26 17:40:27 2019 +0200
35.3 @@ -5,7 +5,7 @@
35.4 this theory is evaluated BEFORE Test_Isac.thy opens structures.
35.5 So, if you encounter errors here, first fix them in ~~/test/Tools/isac/Minimsubpbl/* *)
35.6
35.7 -theory All_Ctxt imports Isac.Isac
35.8 +theory All_Ctxt imports Isac.Isac_Knowledge
35.9 begin
35.10
35.11 text \<open>all changes of context are demonstrated in a mini example.
35.12 @@ -18,6 +18,7 @@
35.13 val (dI',pI',mI') =
35.14 ("Test", ["sqroot-test","univariate","equation","test"],
35.15 ["Test","squ-equ-test-subpbl1"]);
35.16 +\<close> ML \<open>
35.17 val (p,_,f,nxt,_,pt) = Math_Engine.CalcTreeTEST [(fmz, (dI',pI',mI'))];
35.18 \<close>
35.19
36.1 --- a/test/Tools/isac/ADDTESTS/Test_Units.thy Mon Aug 26 09:20:07 2019 +0200
36.2 +++ b/test/Tools/isac/ADDTESTS/Test_Units.thy Mon Aug 26 17:40:27 2019 +0200
36.3 @@ -1,4 +1,4 @@
36.4 -theory Test_Units imports Isac.Isac
36.5 +theory Test_Units imports Isac.Isac_Knowledge
36.6 begin
36.7
36.8 subsection \<open>Variant 1: \<close>
37.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy Mon Aug 26 09:20:07 2019 +0200
37.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Lucas_Interpreter.thy Mon Aug 26 17:40:27 2019 +0200
37.3 @@ -1,5 +1,5 @@
37.4 theory Lucas_Interpreter
37.5 -imports Isac.Isac
37.6 +imports Isac.Isac_Knowledge
37.7 begin
37.8
37.9 ML_file "lucas_interpreter.sml"
38.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy Mon Aug 26 09:20:07 2019 +0200
38.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_1.thy Mon Aug 26 17:40:27 2019 +0200
38.3 @@ -1,21 +1,21 @@
38.4
38.5
38.6 -theory example_1 imports Isac.Isac
38.7 +theory example_1 imports Isac.Isac_Knowledge
38.8 begin
38.9
38.10 -section\<open>Equation Solving\<close>
38.11 -text\<open>Setup equation, Calc Tree,\ldots\<close>
38.12 +section \<open>Equation Solving\<close>
38.13 +text \<open>Setup equation, Calc Tree,\ldots\<close>
38.14
38.15 ML \<open>
38.16 val expr = ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
38.17 "solveFor z", "solutions L"];
38.18 - val (dI',pI',mI') =
38.19 - ("Isac",
38.20 + val (dI', pI', mI') =
38.21 + ("Isac_Knowledge",
38.22 ["abcFormula","degree_2","polynomial","univariate","equation"],
38.23 ["no_met"]);
38.24 \<close>
38.25
38.26 -text\<open>Step through the Calculation\<close>
38.27 +text \<open>Step through the Calculation\<close>
38.28
38.29 ML \<open>
38.30 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(expr, (dI',pI',mI'))];
38.31 @@ -35,7 +35,7 @@
38.32 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
38.33 \<close>
38.34
38.35 -ML\<open>
38.36 +ML \<open>
38.37 f2str f;
38.38 Chead.show_pt pt;
38.39 \<close>
39.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy Mon Aug 26 09:20:07 2019 +0200
39.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy Mon Aug 26 17:40:27 2019 +0200
39.3 @@ -1,5 +1,5 @@
39.4
39.5 -theory example_2 imports Isac.Isac
39.6 +theory example_2 imports Isac.Isac_Knowledge
39.7 begin
39.8
39.9 section\<open>Symbol Representation\<close>
40.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Mon Aug 26 09:20:07 2019 +0200
40.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_3.thy Mon Aug 26 17:40:27 2019 +0200
40.3 @@ -1,6 +1,6 @@
40.4
40.5
40.6 -theory example_3 imports Isac.Isac
40.7 +theory example_3 imports Isac.Isac_Knowledge
40.8 begin
40.9
40.10 section\<open>Function Declaration\<close>
41.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Aug 26 09:20:07 2019 +0200
41.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Mon Aug 26 17:40:27 2019 +0200
41.3 @@ -261,7 +261,7 @@
41.4 val fmz = ["equality (z^^^2 - 1/4*z - 1/8 = (0::real))",
41.5 "solveFor z",
41.6 "solutions L"];
41.7 - val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
41.8 + val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
41.9 \<close>
41.10 text \<open>\noindent Check if the given equation matches the specification of this
41.11 equation type.\<close>
41.12 @@ -273,7 +273,7 @@
41.13 equation with a more specific type definition.\<close>
41.14
41.15 ML \<open>
41.16 - Context.theory_name thy = "Isac";
41.17 + Context.theory_name thy = "Isac_Knowledge";
41.18 val denominator = TermC.parseNEW ctxt "-1 + -2 * z + 8 * z ^^^ 2 = 0";
41.19 val fmz = (*specification*)
41.20 ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",(*equality*)
41.21 @@ -281,7 +281,7 @@
41.22 "solutions L"]; (*identifier for
41.23 solution*)
41.24 val (dI',pI',mI') =
41.25 - ("Isac",
41.26 + ("Isac_Knowledge",
41.27 ["abcFormula","degree_2","polynomial","univariate","equation"],
41.28 ["no_met"]);
41.29 \<close>
41.30 @@ -597,7 +597,7 @@
41.31 expression 2nd order. Follow up the calculation in
41.32 Section~\ref{sec:calc:ztrans} Step~03.\<close>
41.33
41.34 -ML \<open>Context.theory_name thy = "Isac"\<close>
41.35 +ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
41.36
41.37 text\<open>\noindent We define two axiomatization, the first one is the main ansatz,
41.38 the next one is just an equivalent transformation of the resulting
41.39 @@ -686,7 +686,7 @@
41.40
41.41 text\<open>\noindent Still working at {\sisac}\ldots\<close>
41.42
41.43 -ML \<open>Context.theory_name thy = "Isac"\<close>
41.44 +ML \<open>Context.theory_name thy = "Isac_Knowledge"\<close>
41.45
41.46 subsubsection \<open>Build a Rule-Set for the Ansatz\<close>
41.47 text \<open>\noindent The \emph{ansatz} rules violate the principle that each
41.48 @@ -739,7 +739,7 @@
41.49 term2str eq4_2;
41.50
41.51 val fmz = ["equality (3=3*A/(4::real))", "solveFor A","solutions L"];
41.52 - val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
41.53 + val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
41.54 (*
41.55 * Solve the simple linear equation for A:
41.56 * Return eq, not list of eq's
41.57 @@ -752,7 +752,7 @@
41.58 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
41.59 (*Add_Find "solutions L"*)
41.60 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
41.61 - (*Specify_Theory "Isac"*)
41.62 + (*Specify_Theory "Isac_Knowledge"*)
41.63 val (p,_,fa,nxt,_,pt) = me nxt p [] pt;
41.64 (*Specify_Problem ["normalise","polynomial",
41.65 "univariate","equation"])*)
41.66 @@ -819,7 +819,7 @@
41.67 term2str eq4b_2;
41.68
41.69 val fmz = ["equality (3= -3*B/(4::real))", "solveFor B","solutions L"];
41.70 - val (dI',pI',mI') =("Isac", ["univariate","equation"], ["no_met"]);
41.71 + val (dI',pI',mI') =("Isac_Knowledge", ["univariate","equation"], ["no_met"]);
41.72 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
41.73 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
41.74 val (p,_,fb,nxt,_,pt) = me nxt p [] pt;
41.75 @@ -1214,7 +1214,7 @@
41.76 ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
41.77 "stepResponse (x[n::real]::bool)"];
41.78 val (dI,pI,mI) =
41.79 - ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
41.80 + ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
41.81 ["SignalProcessing","Z_Transform","Inverse"]);
41.82
41.83 val ([
41.84 @@ -1256,7 +1256,7 @@
41.85 "stepResponse (x[n::real]::bool)"];
41.86
41.87 val (dI,pI,mI) =
41.88 - ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
41.89 + ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
41.90 ["SignalProcessing","Z_Transform","Inverse"]);
41.91
41.92 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
41.93 @@ -1423,7 +1423,7 @@
41.94 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
41.95 (*Rewrite_Set "polyeq_simplify"*)
41.96 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
41.97 - (*Subproblem("Isac",["degree_1","polynomial","univariate","equation"])*)
41.98 + (*Subproblem("Isac_Knowledge",["degree_1","polynomial","univariate","equation"])*)
41.99 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
41.100 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
41.101 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
41.102 @@ -1603,7 +1603,7 @@
41.103 \end{verbatim}
41.104 \item We check if the \textbf{semantics of the program} by stepwise evaluation
41.105 of the program. Evaluation is done by the Lucas-Interpreter, which works
41.106 - using the knowledge in theory Isac; so we have to re-build Isac. And the
41.107 + using the knowledge in theory Isac_Knowledge; so we have to re-build Isac. And the
41.108 test are performed simplest in a file which is loaded with Isac.
41.109 See \ttfamily tests/../partial\_fractions.sml \normalfont.
41.110 \end{enumerate}
42.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Aug 26 09:20:07 2019 +0200
42.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/document/Build_Inverse_Z_Transform.tex Mon Aug 26 17:40:27 2019 +0200
42.3 @@ -2705,7 +2705,7 @@
42.4 \end{verbatim}
42.5 \item We check if the \textbf{semantics of the program} by stepwise evaluation
42.6 of the program. Evaluation is done by the Lucas-Interpreter, which works
42.7 - using the knowledge in theory Isac; so we have to re-build Isac. And the
42.8 + using the knowledge in theory Isac_Knowledge; so we have to re-build Isac. And the
42.9 test are performed simplest in a file which is loaded with Isac.
42.10 See \ttfamily tests/../partial\_fractions.sml \normalfont.
42.11 \end{enumerate}%
43.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML1_Basics.thy Mon Aug 26 09:20:07 2019 +0200
43.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML1_Basics.thy Mon Aug 26 17:40:27 2019 +0200
43.3 @@ -1,5 +1,5 @@
43.4 (* Quick introduction to ML, session 1 *)
43.5 -theory ML1_Basics imports Isac.Isac begin
43.6 +theory ML1_Basics imports Isac.Isac_Knowledge begin
43.7
43.8 text\<open>This course follows the book:
43.9 J.D.Ullmann, Elements of ML Programming. Prenctice Hall 1998.
44.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML2_Functions.thy Mon Aug 26 09:20:07 2019 +0200
44.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML2_Functions.thy Mon Aug 26 17:40:27 2019 +0200
44.3 @@ -1,5 +1,5 @@
44.4 (* Quick introduction to ML, session 2 *)
44.5 -theory ML2_Functions imports Isac.Isac begin
44.6 +theory ML2_Functions imports Isac.Isac_Knowledge begin
44.7
44.8 text\<open>
44.9 This course follows the book:
45.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML3_Combinators.thy Mon Aug 26 09:20:07 2019 +0200
45.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML3_Combinators.thy Mon Aug 26 17:40:27 2019 +0200
45.3 @@ -1,6 +1,6 @@
45.4 (* Quick introduction to ML, session 3 *)
45.5
45.6 -theory ML3_Combinators imports Isac.Isac begin
45.7 +theory ML3_Combinators imports Isac.Isac_Knowledge begin
45.8
45.9 text\<open>This course follows the book:
45.10 J.D.Ullmann, Elements of ML Programming. Prenctice Hall 1998.
46.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML4_Datastructure.thy Mon Aug 26 09:20:07 2019 +0200
46.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML4_Datastructure.thy Mon Aug 26 17:40:27 2019 +0200
46.3 @@ -1,6 +1,6 @@
46.4 (* Quick introduction to ML, session 3 *)
46.5
46.6 -theory ML4_Datastructure imports Isac.Isac begin
46.7 +theory ML4_Datastructure imports Isac.Isac_Knowledge begin
46.8
46.9 text\<open>This course follows the book:
46.10 J.D.Ullmann, Elements of ML Programming. Prenctice Hall 1998.
47.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Aug 26 09:20:07 2019 +0200
47.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T1_Basics.thy Mon Aug 26 17:40:27 2019 +0200
47.3 @@ -4,7 +4,7 @@
47.4 0 1 2 3 4 5 6 7 8
47.5 *)
47.6
47.7 -theory T1_Basics imports Isac.Isac
47.8 +theory T1_Basics imports Isac.Isac_Knowledge
47.9 begin
47.10
47.11 chapter \<open>Basics on Linux, Isabelle and ISAC\<close>
47.12 @@ -88,7 +88,7 @@
47.13 Presently, ISAC uses a slightly different representation for terms (which soon
47.14 will disappear), which does not encode numerals as binary numbers:
47.15 \<close>
47.16 -ML \<open>val SOME t = TermC.parse @{theory "Isac"} "a + b * 3";
47.17 +ML \<open>val SOME t = TermC.parse @{theory "Isac_Knowledge"} "a + b * 3";
47.18 TermC.atomwy (Thm.term_of t);
47.19 \<close>
47.20 text \<open>From the above we see: the internal representation of a term contains
48.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Mon Aug 26 09:20:07 2019 +0200
48.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy Mon Aug 26 17:40:27 2019 +0200
48.3 @@ -3,7 +3,7 @@
48.4 /usr/local/Isabelle/bin/isabelle jedit -l Isac T2_Rewriting.thy &
48.5 *)
48.6
48.7 -theory T2_Rewriting imports Isac.Isac
48.8 +theory T2_Rewriting imports Isac.Isac_Knowledge
48.9 begin
48.10
48.11 chapter \<open>Rewriting\<close>
48.12 @@ -36,7 +36,7 @@
48.13 ML \<open>
48.14 (*default_print_depth 1;*)
48.15 val (thy, ro, er, inst) =
48.16 - (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
48.17 + (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
48.18 \<close>
48.19 text \<open>... and let us differentiate the term t:\<close>
48.20 ML \<open>
49.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Mon Aug 26 09:20:07 2019 +0200
49.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T3_MathEngine.thy Mon Aug 26 17:40:27 2019 +0200
49.3 @@ -1,6 +1,6 @@
49.4 (* this is evaluated BEFORE Test_Isac.thu opens structures*)
49.5
49.6 -theory T3_MathEngine imports Isac.Isac
49.7 +theory T3_MathEngine imports Isac.Isac_Knowledge
49.8 begin
49.9
49.10 chapter \<open>ISACs mathematics engine\<close>
50.1 --- a/test/Tools/isac/Frontend/use-cases.sml Mon Aug 26 09:20:07 2019 +0200
50.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Mon Aug 26 17:40:27 2019 +0200
50.3 @@ -762,7 +762,7 @@
50.4 see isac.bridge.TestSpecify#testMatchRefine*)
50.5 CalcTree
50.6 [(["equality (x^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"],
50.7 - ("Isac",
50.8 + ("Isac_Knowledge",
50.9 ["univariate","equation"],
50.10 ["no_met"]))];
50.11 Iterator 1;
50.12 @@ -1445,7 +1445,7 @@
50.13 "--------- UC errpat chain-rule-diff-both, fillpat by input ------";
50.14 CalcTree
50.15 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
50.16 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
50.17 + ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
50.18 Iterator 1;
50.19 moveActiveRoot 1;
50.20 autoCalculate 1 CompleteCalcHead;
50.21 @@ -1546,7 +1546,7 @@
50.22 CalcTree
50.23 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
50.24 "differentiateFor x", "derivative f_f'"],
50.25 - ("Isac", ["derivative_of","function"],
50.26 + ("Isac_Knowledge", ["derivative_of","function"],
50.27 ["diff","differentiate_on_R"]))]; (*<<<======= EP is directly in script*)
50.28 Iterator 1;
50.29 moveActiveRoot 1;
50.30 @@ -1560,7 +1560,7 @@
50.31 CalcTree
50.32 [(["functionTerm ((x ^ 2) ^ 3 + sin (x ^ 4))",
50.33 "differentiateFor x", "derivative f_f'"],
50.34 - ("Isac", ["derivative_of","function"],
50.35 + ("Isac_Knowledge", ["derivative_of","function"],
50.36 ["diff","after_simplification"]))]; (*<<<======= EP is in a ruleset*)
50.37 Iterator 1;
50.38 moveActiveRoot 1;
51.1 --- a/test/Tools/isac/Interpret/calchead.sml Mon Aug 26 09:20:07 2019 +0200
51.2 +++ b/test/Tools/isac/Interpret/calchead.sml Mon Aug 26 17:40:27 2019 +0200
51.3 @@ -341,7 +341,7 @@
51.4 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
51.5 val xxx = match_ags @{theory "EqSystem"} pats ags;
51.6 "-a2-----------------------------------------------------";
51.7 -case match_ags @{theory "Isac"} pats ags of
51.8 +case match_ags @{theory "Isac_Knowledge"} pats ags of
51.9 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
51.10 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
51.11 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
51.12 @@ -363,7 +363,7 @@
51.13 val pI = ["LINEAR","system"];
51.14 val pats = (#ppc o get_pbt) pI;
51.15 "-b1-----------------------------------------------------";
51.16 -val xxx = match_ags @{theory "Isac"} pats ags;
51.17 +val xxx = match_ags @{theory "Isac_Knowledge"} pats ags;
51.18 "-b2-----------------------------------------------------";
51.19 case match_ags @{theory "EqSystem"} pats ags of
51.20 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
51.21 @@ -432,7 +432,7 @@
51.22 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
51.23 val xxx = match_ags @{theory "EqSystem"} pats ags;
51.24 "-a2-----------------------------------------------------";
51.25 -case match_ags @{theory "Isac"} pats ags of
51.26 +case match_ags @{theory "Isac_Knowledge"} pats ags of
51.27 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
51.28 (2, [1], "#Given", Const ("EqSystem.solveForVars", _),
51.29 [ _ $ Free ("c", _) $ _, _ $ Free ("c_2", _) $ _]),
51.30 @@ -454,7 +454,7 @@
51.31 val pI = ["LINEAR","system"];
51.32 val pats = (#ppc o get_pbt) pI;
51.33 "-b1-----------------------------------------------------";
51.34 -val xxx = match_ags @{theory "Isac"} pats ags;
51.35 +val xxx = match_ags @{theory "Isac_Knowledge"} pats ags;
51.36 "-b2-----------------------------------------------------";
51.37 case match_ags @{theory "EqSystem"} pats ags of
51.38 [(1, [1], "#Given", Const ("Descript.equalities", _), _),
52.1 --- a/test/Tools/isac/Interpret/ctree.sml Mon Aug 26 09:20:07 2019 +0200
52.2 +++ b/test/Tools/isac/Interpret/ctree.sml Mon Aug 26 17:40:27 2019 +0200
52.3 @@ -73,8 +73,8 @@
52.4 val pt = append_problem [] (e_istate, e_ctxt) e_fmz ([(*oris*)], e_spec, e_term) pt;
52.5 val ctxt = get_obj g_ctxt pt [];
52.6 if is_e_ctxt ctxt then () else error "--- fun update_ctxt, fun g_ctxt: append_problem changed";
52.7 -val pt = update_ctxt pt [] (Proof_Context.init_global @{theory "Isac"});
52.8 -if (get_obj g_ctxt pt [] |> Proof_Context.theory_of |> Context.theory_name) = "Isac"
52.9 +val pt = update_ctxt pt [] (Proof_Context.init_global @{theory "Isac_Knowledge"});
52.10 +if (get_obj g_ctxt pt [] |> Proof_Context.theory_of |> Context.theory_name) = "Isac_Knowledge"
52.11 then () else error "--- fun update_ctxt, fun g_ctxt changed";
52.12
52.13 "-------------- check positions in miniscript --------------------";
53.1 --- a/test/Tools/isac/Interpret/generate.sml Mon Aug 26 09:20:07 2019 +0200
53.2 +++ b/test/Tools/isac/Interpret/generate.sml Mon Aug 26 17:40:27 2019 +0200
53.3 @@ -17,7 +17,7 @@
53.4 reset_states ();
53.5 CalcTree
53.6 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
53.7 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
53.8 + ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
53.9 Iterator 1;
53.10 moveActiveRoot 1;
53.11 autoCalculate 1 CompleteCalcHead;
54.1 --- a/test/Tools/isac/Interpret/inform.sml Mon Aug 26 09:20:07 2019 +0200
54.2 +++ b/test/Tools/isac/Interpret/inform.sml Mon Aug 26 17:40:27 2019 +0200
54.3 @@ -115,13 +115,13 @@
54.4 *)
54.5 "----------------------------------------------------------";
54.6
54.7 - val fod = make_deriv (@{theory "Isac"}) Atools_erls
54.8 + val fod = make_deriv (@{theory "Isac_Knowledge"}) Atools_erls
54.9 ((#rules o rep_rls) Test_simplify)
54.10 (sqrt_right false (@{theory "Pure"})) NONE
54.11 (str2term "x + 1 + -1 * 2 = 0");
54.12 (writeln o trtas2str) fod;
54.13
54.14 - val ifod = make_deriv (@{theory "Isac"}) Atools_erls
54.15 + val ifod = make_deriv (@{theory "Isac_Knowledge"}) Atools_erls
54.16 ((#rules o rep_rls) Test_simplify)
54.17 (sqrt_right false (@{theory "Pure"})) NONE
54.18 (str2term "-2 * 1 + (1 + x) = 0");
54.19 @@ -664,7 +664,7 @@
54.20 [], NONE,
54.21 ??.empty, Sundef, false)*)
54.22 (*default_print_depth 5;*) spec; (*default_print_depth 3;*)
54.23 -(*("Isac",
54.24 +(*("Isac_Knowledge",
54.25 ["derivative_of", "function"],
54.26 ["diff", "differentiate_on_R"]) : spec*)
54.27 writeln (itms2str_ ctxt probl);
54.28 @@ -694,7 +694,7 @@
54.29 (*the following input is copied from BridgeLog Java <==> SML,
54.30 omitting unnecessary inputs*)
54.31 (*1>*)reset_states ();
54.32 -(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac",["derivative_of","function"],["diff","differentiate_on_R"]))];
54.33 +(*2>*)CalcTree [(["functionTerm (x^2 + x + 1)", "differentiateFor x", "derivative f_'_f"],("Isac_Knowledge",["derivative_of","function"],["diff","differentiate_on_R"]))];
54.34 (*3>*)Iterator 1; moveActiveRoot 1;
54.35
54.36 (*6>*)(*completeCalcHead*)autoCalculate 1 CompleteCalcHead;
54.37 @@ -708,7 +708,7 @@
54.38 [], NONE,
54.39 ??.empty, Sundef, false)*)
54.40 (*default_print_depth 5;*) spec; (*default_print_depth 3;*)
54.41 -(*("Isac",
54.42 +(*("Isac_Knowledge",
54.43 ["derivative_of", "function"],
54.44 ["diff", "differentiate_on_R"]) : spec*)
54.45 writeln (itms2str_ ctxt probl);
54.46 @@ -998,7 +998,7 @@
54.47 reset_states ();
54.48 CalcTree
54.49 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
54.50 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
54.51 + ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
54.52 Iterator 1;
54.53 moveActiveRoot 1;
54.54 autoCalculate 1 CompleteCalcHead;
54.55 @@ -1016,7 +1016,7 @@
54.56 "~~~~~ fun inform , args:"; val (((*next_*)cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
54.57 = (cs', (encode ifo));
54.58 val ctxt = get_ctxt pt pos (*see TODO.thy*)
54.59 - val SOME f_in = (*case*) TermC.parse (Celem.assoc_thy "Isac") istr (*of*);
54.60 + val SOME f_in = (*case*) TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr (*of*);
54.61 val f_in = Thm.term_of f_in
54.62 val pos_pred = lev_back' pos
54.63 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
54.64 @@ -1058,7 +1058,7 @@
54.65 reset_states ();
54.66 CalcTree
54.67 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
54.68 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
54.69 + ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
54.70 Iterator 1;
54.71 moveActiveRoot 1;
54.72 autoCalculate 1 CompleteCalcHead;
54.73 @@ -1141,7 +1141,7 @@
54.74 reset_states ();
54.75 CalcTree
54.76 [(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
54.77 - ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
54.78 + ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
54.79 Iterator 1;
54.80 moveActiveRoot 1;
54.81 autoCalculate 1 CompleteCalcHead;
54.82 @@ -1204,7 +1204,7 @@
54.83 val pos = get_pos cI 1;
54.84
54.85 "~~~~~ fun is_exactly_equal, args:"; val ((pt, pos as (p, p_)), istr) = ((pt, pos), ifo);
54.86 - val SOME ifo = parseNEW (assoc_thy "Isac" |> thy2ctxt) istr
54.87 + val SOME ifo = parseNEW (assoc_thy "Isac_Knowledge" |> thy2ctxt) istr
54.88 val p' = lev_on p;
54.89 val tac = get_obj g_tac pt p';
54.90 val Rewrite_Inst ([bbb as "(''bdv'', x)"], ("diff_sin_chain", ttt)) = tac;
55.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Aug 26 09:20:07 2019 +0200
55.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Aug 26 17:40:27 2019 +0200
55.3 @@ -103,7 +103,7 @@
55.4 (*case*) inform cs' (encode ifo) (*of*);
55.5 "~~~~~ fun inform , args:"; val ((cs as (_, _, (pt, pos as (p, _))): Chead.calcstate'), istr)
55.6 = (cs', (encode ifo));
55.7 -val SOME f_in = (*case*) TermC.parse (Celem.assoc_thy "Isac") istr (*of*);
55.8 +val SOME f_in = (*case*) TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr (*of*);
55.9 (* NONE \<longrightarrow> ("syntax error in '" ^ istr ^ "'", cs )*)
55.10 val f_in = Thm.term_of f_in
55.11 val f_succ = Ctree.get_curr_formula (pt, pos);
56.1 --- a/test/Tools/isac/Interpret/mathengine.sml Mon Aug 26 09:20:07 2019 +0200
56.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Mon Aug 26 17:40:27 2019 +0200
56.3 @@ -473,7 +473,7 @@
56.4 "--------- search for Or_to_List ------------------------";
56.5 "--------- search for Or_to_List ------------------------";
56.6 val fmz = ["equality (x^^^2 + 4*x + 5 = (2::real))", "solveFor x","solutions L"];
56.7 -val (dI',pI',mI') = ("Isac", ["univariate","equation"], ["no_met"])
56.8 +val (dI',pI',mI') = ("Isac_Knowledge", ["univariate","equation"], ["no_met"])
56.9 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
56.10 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
56.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
56.12 @@ -521,13 +521,13 @@
56.13 "we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
56.14 "Below there are the steps which found out the reason: \n" ^
56.15 "store_pbt mistakenly stored that theory.";
56.16 -val ctxt = Proof_Context.init_global @{theory Isac};
56.17 +val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
56.18 val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
56.19 val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
56.20
56.21 val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", "boundVariable z",
56.22 "stepResponse (x[n::real]::bool)"];
56.23 -val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
56.24 +val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
56.25 ["SignalProcessing","Z_Transform","Inverse"]);
56.26
56.27 val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
56.28 @@ -596,7 +596,7 @@
56.29 is wrong for simpl, but working ?!? *)
56.30 val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
56.31 val pos' = ((lev_on o lev_dn) p, Frm)
56.32 - val thy = assoc_thy "Isac"
56.33 + val thy = assoc_thy "Isac_Knowledge"
56.34 val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ (is, ctxt) pos' pt;
56.35 (*val (_,_,(pt'',_)) = *)complete_solve CompleteSubpbl [] (pt',pos');
56.36 (* ^^^^^^^^^^^^^^ in test/../mathengine.sml*)
56.37 @@ -635,11 +635,11 @@
56.38 (p, Met) => ((lev_on o lev_dn) p, Frm)(*begin script*)
56.39 | (p, Res) => (lev_on p,Res) (*somewhere in script*)
56.40 | _ => pos;
56.41 -generate1 (assoc_thy "Isac") tac_ is pos pt;
56.42 +generate1 (assoc_thy "Isac_Knowledge") tac_ is pos pt;
56.43 (* tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
56.44 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
56.45 "~~~~~ fun generate1, args:"; val (thy, (Rewrite' (thy',ord',rls',pa,thm',f,(f',asm))),
56.46 - (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac"), tac_, is, pos, pt);
56.47 + (is, ctxt), (p,p_), pt) = ((assoc_thy "Isac_Knowledge"), tac_, is, pos, pt);
56.48 val (pt,c) = cappend_atomic pt p (is, insert_assumptions asm ctxt) f
56.49 (Rewrite thm') (f',asm) Complete;
56.50 (* in pt: tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
56.51 @@ -717,7 +717,7 @@
56.52 (*val ("ok", (_, c, ptp as (_,p))) = *)inform cs' (encode ifo);
56.53 "~~~~~ fun inform , args:"; val (cs as (_, _, ptp as (pt, pos as (p, p_))), istr) =
56.54 (cs', (encode ifo));
56.55 -val SOME f_in = parse (assoc_thy "Isac") istr
56.56 +val SOME f_in = parse (assoc_thy "Isac_Knowledge") istr
56.57 val f_in = Thm.term_of f_in
56.58 val f_succ = get_curr_formula (pt, pos);
56.59 f_succ = f_in = false;
57.1 --- a/test/Tools/isac/Interpret/mstools.sml Mon Aug 26 09:20:07 2019 +0200
57.2 +++ b/test/Tools/isac/Interpret/mstools.sml Mon Aug 26 17:40:27 2019 +0200
57.3 @@ -322,13 +322,13 @@
57.4 then () else error "common_subthy 2";
57.5
57.6 val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory PolyEq});
57.7 -if Context.theory_name (common_subthy (thy1, thy2)) = "Isac" then () else error "common_subthy 3";
57.8 +if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 3";
57.9
57.10 -val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Isac});
57.11 -if Context.theory_name (common_subthy (thy1, thy2)) = "Isac" then () else error "common_subthy 4";
57.12 +val (thy1, thy2) = (@{theory Partial_Fractions}, @{theory Isac_Knowledge});
57.13 +if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 4";
57.14
57.15 val (thy1, thy2) = (@{theory PolyEq}, @{theory Partial_Fractions});
57.16 -if Context.theory_name (common_subthy (thy1, thy2)) = "Isac" then () else error "common_subthy 5";
57.17 +if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 5";
57.18
57.19 -val (thy1, thy2) = (@{theory Isac}, @{theory Partial_Fractions});
57.20 -if Context.theory_name (common_subthy (thy1, thy2)) = "Isac" then () else error "common_subthy 6";
57.21 +val (thy1, thy2) = (@{theory Isac_Knowledge}, @{theory Partial_Fractions});
57.22 +if Context.theory_name (common_subthy (thy1, thy2)) = "Isac_Knowledge" then () else error "common_subthy 6";
58.1 --- a/test/Tools/isac/Interpret/ptyps.sml Mon Aug 26 09:20:07 2019 +0200
58.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Mon Aug 26 17:40:27 2019 +0200
58.3 @@ -30,8 +30,8 @@
58.4 "----------- testdata for refin, refine_ori ----------------------";
58.5 "----------- testdata for refin, refine_ori ----------------------";
58.6 show_ptyps();
58.7 -val thy = @{theory "Isac"};
58.8 -val ctxt = Proof_Context.init_global @{theory "Isac"};
58.9 +val thy = @{theory "Isac_Knowledge"};
58.10 +val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"};
58.11
58.12 (*case 1: no refinement *)
58.13 val (d1,ts1) = split_dts ((Thm.term_of o the o (parse thy)) "fixedValues [aaa = 0]");
59.1 --- a/test/Tools/isac/Interpret/script.sml Mon Aug 26 09:20:07 2019 +0200
59.2 +++ b/test/Tools/isac/Interpret/script.sml Mon Aug 26 17:40:27 2019 +0200
59.3 @@ -20,7 +20,7 @@
59.4 "-----------------------------------------------------------------";
59.5 "-----------------------------------------------------------------";
59.6
59.7 -val thy = @{theory Isac};
59.8 +val thy = @{theory Isac_Knowledge};
59.9
59.10 "----------- fun sel_appl_atomic_tacs ----------------------------";
59.11 "----------- fun sel_appl_atomic_tacs ----------------------------";
60.1 --- a/test/Tools/isac/Interpret/solve.sml Mon Aug 26 09:20:07 2019 +0200
60.2 +++ b/test/Tools/isac/Interpret/solve.sml Mon Aug 26 17:40:27 2019 +0200
60.3 @@ -36,7 +36,7 @@
60.4 "-----------------------------------------------------------------";
60.5 "-----------------------------------------------------------------";
60.6
60.7 -val thy= @{theory Isac};
60.8 +val thy= @{theory Isac_Knowledge};
60.9 "--------- interSteps on norm_Rational ---------------------------";
60.10 "--------- interSteps on norm_Rational ---------------------------";
60.11 "--------- interSteps on norm_Rational ---------------------------";
61.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Mon Aug 26 09:20:07 2019 +0200
61.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Mon Aug 26 17:40:27 2019 +0200
61.3 @@ -24,18 +24,18 @@
61.4 (* the ONLY Test_Isac, which uses Rewrite !!! *)
61.5 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
61.6 "functionName X_z", "stepResponse (x[n::real]::bool)"];
61.7 -val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
61.8 +val (dI, pI, mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
61.9 ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
61.10 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; (*Model_Problem*)
61.11 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = ...*)
61.12 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "stepResponse (x [n])")*)
61.13 -(*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory "Isac"*)
61.14 +(*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Theory "Isac_Knowledge"*)
61.15 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Problem ["Inverse_sub", "Z_Transform", "SignalProcessing"]*)
61.16 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Specify_Method ["SignalProcessing", "Z_Transform", "Inverse_sub"]*)
61.17 (*[], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "boundVariable X_z"*)
61.18 (*[], Met*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Apply_Me["SignalProcessing","Z_Transform","Inverse_sub"]*)
61.19 (*[1], Frm*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Rewrite ("ruleZY", "Inverse_Z_Transform.ruleZY")*)
61.20 -(*[1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["partial_fraction", "rational..*)
61.21 +(*[1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac_Knowledge", ["partial_fraction", "rational..*)
61.22 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Model_Problem*)
61.23 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "functionTerm (X' z)"*)
61.24 (*[2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "solveFor z"*)
61.25 @@ -49,7 +49,7 @@
61.26 if p = ([2, 1], Frm) andalso f2str fb = "3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))"
61.27 then () else error "Z_Transform,inverse_sub] me 1"; (*Rewrite_Set "norm_Rational"*)
61.28
61.29 -(*[2,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["abcFormula", "degree_2", "po...a*)
61.30 +(*[2,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac_Knowledge", ["abcFormula", "degree_2", "po...a*)
61.31 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
61.32 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
61.33 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
61.34 @@ -183,7 +183,7 @@
61.35 reset_states ();
61.36 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
61.37 "functionName X_z", "stepResponse (x[n::real]::bool)"];
61.38 -val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
61.39 +val (dI, pI, mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
61.40 ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
61.41 CalcTree [(fmz, (dI,pI,mI))];
61.42 Iterator 1;
62.1 --- a/test/Tools/isac/Knowledge/algein.sml Mon Aug 26 09:20:07 2019 +0200
62.2 +++ b/test/Tools/isac/Knowledge/algein.sml Mon Aug 26 17:40:27 2019 +0200
62.3 @@ -43,7 +43,7 @@
62.4 "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
62.5 "GesamtLaenge L"];
62.6 val (dI',pI',mI') =
62.7 - ("Isac",["numerischSymbolische", "Berechnung"],
62.8 + ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],
62.9 ["Berechnung","erstNumerisch"]);
62.10 val p = e_pos'; val c = [];
62.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))](*nxt = ("Model_Pr*);
62.12 @@ -88,7 +88,7 @@
62.13 "KantenSenkrecht [v1 = (k::real), v2 = (k::real), v3 = (k::real), v4 = (k::real)]",
62.14 "KantenOben [t1 = k - 2*(q::real), t2 = k - 2*(q::real), t3 = k - 2*(q::real), t4 = k - 2*(q::real) ]",
62.15 "GesamtLaenge L"],
62.16 - ("Isac",["numerischSymbolische", "Berechnung"],
62.17 + ("Isac_Knowledge",["numerischSymbolische", "Berechnung"],
62.18 ["Berechnung","erstSymbolisch"]))];
62.19 Iterator 1;
62.20 moveActiveRoot 1;
62.21 @@ -100,7 +100,7 @@
62.22 "----------- Widerspruch 3 = 777 ---------------------------------";
62.23 "----------- Widerspruch 3 = 777 ---------------------------------";
62.24 "----------- Widerspruch 3 = 777 ---------------------------------";
62.25 -val thy = @{theory "Isac"};
62.26 +val thy = @{theory "Isac_Knowledge"};
62.27 val rew_ord = dummy_ord;
62.28 val erls = Erls;
62.29 val thm = assoc_thm' thy ("sym_mult_zero_right","");
63.1 --- a/test/Tools/isac/Knowledge/atools.sml Mon Aug 26 09:20:07 2019 +0200
63.2 +++ b/test/Tools/isac/Knowledge/atools.sml Mon Aug 26 17:40:27 2019 +0200
63.3 @@ -368,7 +368,7 @@
63.4 Termorder.thy BITTE NUR HIERHER SCHREIBEN (...WN03)
63.5
63.6 get_thm Termorder.thy "bdv_n_collect";
63.7 - get_thm (theory "Isac") "bdv_n_collect";
63.8 + get_thm (theory "Isac_Knowledge") "bdv_n_collect";
63.9 *)
63.10 val t = (Thm.term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
63.11 val SOME (t,_) =
64.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Mon Aug 26 09:20:07 2019 +0200
64.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Mon Aug 26 17:40:27 2019 +0200
64.3 @@ -44,12 +44,12 @@
64.4 val allthys = Theory.ancestors_of @{theory};
64.5 val allthys = filter_out (member Context.eq_thy (* thys for isac bootstrap *)
64.6 [(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory xmlsrc},
64.7 - @{theory Frontend}, knowledge_parent]) allthys (*["Isac", ..., "Pure"]*)
64.8 + @{theory Frontend}, knowledge_parent]) allthys (*["Isac_Knowledge", ..., "Pure"]*)
64.9 val isabthys' = (*["Complex_Main", "Taylor", .., "Pure"]*)
64.10 drop ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
64.11 - val isacthys' = (*["Isac", "Inverse_Z_Transform", .., "KEStore"]*)
64.12 + val isacthys' = (*["Isac_Knowledge", "Inverse_Z_Transform", .., "KEStore"]*)
64.13 take ((find_index (curry Context.eq_thy @{theory Complex_Main}) allthys), allthys);
64.14 - val knowthys' = (*["Isac", .., "Descript", "Delete"]*)
64.15 + val knowthys' = (*["Isac_Knowledge", .., "Descript", "Delete"]*)
64.16 take ((find_index (curry Context.eq_thy proglang_parent) isacthys'), isacthys');
64.17 val progthys' = (*["Program", "Tools", "ListC", "KEStore"]*)
64.18 drop ((find_index (curry Context.eq_thy proglang_parent) isacthys') + 1(*ProgLang*), isacthys');
64.19 @@ -77,7 +77,7 @@
64.20
64.21 (*/----- save time in Test_Isac.thy ----------------------------------------------------------
64.22 (* rls are stored cumulatively vvv we try them by bisection *)
64.23 -(*KEStore_Elems.get_rlss @{theory Isac} (* NOT terminating *)*)
64.24 +(*KEStore_Elems.get_rlss @{theory Isac_Knowledge} (* NOT terminating *)*)
64.25 (*KEStore_Elems.get_rlss @{theory Inverse_Z_Transform} (* NOT terminating *)*)
64.26 KEStore_Elems.get_rlss @{theory Biegelinie}; (* very very very slow *)
64.27 KEStore_Elems.get_rlss @{theory PolyEq}; (* OK, very very slow *)
65.1 --- a/test/Tools/isac/Knowledge/diff.sml Mon Aug 26 09:20:07 2019 +0200
65.2 +++ b/test/Tools/isac/Knowledge/diff.sml Mon Aug 26 17:40:27 2019 +0200
65.3 @@ -229,7 +229,7 @@
65.4 term2str screxp1;
65.5 atomty screxp1;
65.6
65.7 -val SOME (f'_,_) = rewrite_set_ (@{theory "Isac"}) false srls_diff screxp1;
65.8 +val SOME (f'_,_) = rewrite_set_ (@{theory "Isac_Knowledge"}) false srls_diff screxp1;
65.9 if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then ()
65.10 else error "diff.sml: diff.behav. in 'primed'";
65.11 atomty f'_;
65.12 @@ -315,7 +315,7 @@
65.13 [(["functionTerm (x^2 + x+ 1/x + 2/x^2)",
65.14 (*"functionTerm ((x^3)^5)",*)
65.15 "differentiateFor x", "derivative f_f'"],
65.16 - ("Isac", ["derivative_of","function"],
65.17 + ("Isac_Knowledge", ["derivative_of","function"],
65.18 ["diff","differentiate_on_R"]))];
65.19 Iterator 1;
65.20 moveActiveRoot 1;
65.21 @@ -330,7 +330,7 @@
65.22 CalcTree
65.23 [(["functionTerm (x^3 * x^5)",
65.24 "differentiateFor x", "derivative f_f'"],
65.25 - ("Isac", ["derivative_of","function"],
65.26 + ("Isac_Knowledge", ["derivative_of","function"],
65.27 ["diff","differentiate_on_R"]))];
65.28 Iterator 1;
65.29 moveActiveRoot 1;
65.30 @@ -354,7 +354,7 @@
65.31 CalcTree
65.32 [(["functionTerm (x^3 * x^5)",
65.33 "differentiateFor x", "derivative f_f'"],
65.34 - ("Isac", ["derivative_of","function"],
65.35 + ("Isac_Knowledge", ["derivative_of","function"],
65.36 ["diff","after_simplification"]))];
65.37 Iterator 1;
65.38 moveActiveRoot 1;
65.39 @@ -374,7 +374,7 @@
65.40 CalcTree
65.41 [(["functionTerm ((x^3)^5)",
65.42 "differentiateFor x", "derivative f_f'"],
65.43 - ("Isac", ["derivative_of","function"],
65.44 + ("Isac_Knowledge", ["derivative_of","function"],
65.45 ["diff","after_simplification"]))];
65.46 Iterator 1;
65.47 moveActiveRoot 1;
65.48 @@ -389,7 +389,7 @@
65.49 reset_states ();
65.50 CalcTree
65.51 [(["functionEq (A = s * (a - (s::real)))", "differentiateFor s", "derivativeEq f_f'"],
65.52 - ("Isac", ["named","derivative_of","function"],
65.53 + ("Isac_Knowledge", ["named","derivative_of","function"],
65.54 ["diff","differentiate_equality"]))];
65.55 Iterator 1;
65.56 moveActiveRoot 1;
65.57 @@ -416,7 +416,7 @@
65.58 CalcTree
65.59 [(["functionTerm (x^2 + x + 1)",
65.60 "differentiateFor x", "derivative f_f'"],
65.61 - ("Isac", ["derivative_of","function"],
65.62 + ("Isac_Knowledge", ["derivative_of","function"],
65.63 ["diff","differentiate_on_R"]))];
65.64 Iterator 1;
65.65 moveActiveRoot 1;
66.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml Mon Aug 26 09:20:07 2019 +0200
66.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml Mon Aug 26 17:40:27 2019 +0200
66.3 @@ -18,7 +18,7 @@
66.4 (*there seemed to be no way to do these tests within DiophantEq.thy:
66.5 val thy = @{theory};(**** ME_Isa: thy 'DiophantEq' not in system
66.6 from CalcTreeTest*)
66.7 -(*val thy = @{theory "Isac"};toplevel error from store_met?!?*)
66.8 +(*val thy = @{theory "Isac_Knowledge"};toplevel error from store_met?!?*)
66.9 *)
66.10 val thy = @{theory "DiophantEq"};
66.11 val ctxt = Proof_Context.init_global thy;
67.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Mon Aug 26 09:20:07 2019 +0200
67.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Mon Aug 26 17:40:27 2019 +0200
67.3 @@ -172,7 +172,7 @@
67.4 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
67.5 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
67.6 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
67.7 -val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*);
67.8 +val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
67.9 val t =
67.10 str2term"[0 = c_2 + c * 0 + 1 / EI * (L * q_0 / 12 * 0 ^^^ 3 + \
67.11 \ -1 * q_0 / 24 * 0 ^^^ 4),\
67.12 @@ -463,7 +463,7 @@
67.13 =========================================================================/
67.14
67.15 -----fun refin' ff:
67.16 -> (writeln o (itms2str_ (thy2ctxt @{theory Isac}))) itms;
67.17 +> (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) itms;
67.18 [
67.19 (1 ,[1] ,true ,#Given ,Cor equalities
67.20 [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,
67.21 @@ -478,7 +478,7 @@
67.22 (true, length_ [c, c_2] = 2)]
67.23
67.24 ----- fun match_oris':
67.25 -> (writeln o (itms2str_ (thy2ctxt @{theory Isac}))) itms;
67.26 +> (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) itms;
67.27 > (writeln o pres2str) pre';
67.28 ..as in refin'
67.29
67.30 @@ -545,7 +545,7 @@
67.31
67.32 val (p,_,f,nxt,_,pt) = me nxt p c pt;
67.33 val PblObj {probl,...} = get_obj I pt [5];
67.34 - (writeln o (itms2str_ (thy2ctxt @{theory Isac}))) probl;
67.35 + (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) probl;
67.36 (*[
67.37 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
67.38 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
67.39 @@ -613,7 +613,7 @@
67.40
67.41 val (p,_,f,nxt,_,pt) = me nxt p c pt;
67.42 val PblObj {probl,...} = get_obj I pt [5];
67.43 - (writeln o (itms2str_ (thy2ctxt @{theory Isac}))) probl;
67.44 + (writeln o (itms2str_ (thy2ctxt @{theory Isac_Knowledge}))) probl;
67.45 (*[
67.46 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]])),
67.47 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])),
67.48 @@ -643,7 +643,7 @@
67.49 "----------- all systems from Biegelinie -------------------------";
67.50 "----------- all systems from Biegelinie -------------------------";
67.51 "----------- all systems from Biegelinie -------------------------";
67.52 -val thy = @{theory Isac}
67.53 +val thy = @{theory Isac_Knowledge}
67.54 val subst =
67.55 [(str2term "bdv_1", str2term "c"), (str2term "bdv_2", str2term "c_2"),
67.56 (str2term "bdv_3", str2term "c_3"), (str2term "bdv_4", str2term "c_4")];
68.1 --- a/test/Tools/isac/Knowledge/gcd_poly.thy Mon Aug 26 09:20:07 2019 +0200
68.2 +++ b/test/Tools/isac/Knowledge/gcd_poly.thy Mon Aug 26 17:40:27 2019 +0200
68.3 @@ -1,5 +1,5 @@
68.4 theory gcd_poly
68.5 -imports (*"~~/src/Tools/isac/Knowledge/GCD_Poly"*) Isac.Isac
68.6 +imports (*"~~/src/Tools/isac/Knowledge/GCD_Poly"*) Isac.Isac_Knowledge
68.7 begin
68.8
68.9 (*here come the tests from GCD_Poly.thy*)
69.1 --- a/test/Tools/isac/Knowledge/integrate.sml Mon Aug 26 09:20:07 2019 +0200
69.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Mon Aug 26 17:40:27 2019 +0200
69.3 @@ -176,7 +176,7 @@
69.4 "----------- simplify by ruleset reducing make_ratpoly_in";
69.5 "----------- simplify by ruleset reducing make_ratpoly_in";
69.6 "----------- simplify by ruleset reducing make_ratpoly_in";
69.7 -val thy = @{theory "Isac"};
69.8 +val thy = @{theory "Isac_Knowledge"};
69.9 "===== test 1";
69.10 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
69.11
69.12 @@ -311,7 +311,7 @@
69.13 "----------- rewrite 3rd integration in 7.27 ------------";
69.14 "----------- rewrite 3rd integration in 7.27 ------------";
69.15 "----------- rewrite 3rd integration in 7.27 ------------";
69.16 -val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*);
69.17 +val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
69.18 val t = str2t "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
69.19 val SOME(t,_)= rewrite_set_inst_ thy true subs simplify_Integral t;
69.20 if term2str t =
70.1 --- a/test/Tools/isac/Knowledge/integrate.thy Mon Aug 26 09:20:07 2019 +0200
70.2 +++ b/test/Tools/isac/Knowledge/integrate.thy Mon Aug 26 17:40:27 2019 +0200
70.3 @@ -15,7 +15,7 @@
70.4 (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False) @@
70.5 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))"
70.6 setup \<open>KEStore_Elems.add_mets
70.7 - [Specify.prep_met @{theory "Isac"} "met_testint" [] Celem.e_metID
70.8 + [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Celem.e_metID
70.9 (["diff","integration","test"],
70.10 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],
70.11 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
71.1 --- a/test/Tools/isac/Knowledge/isac.sml Mon Aug 26 09:20:07 2019 +0200
71.2 +++ b/test/Tools/isac/Knowledge/isac.sml Mon Aug 26 17:40:27 2019 +0200
71.3 @@ -8,6 +8,6 @@
71.4 val allthys = @{theory} :: Theory.ancestors_of @{theory};
71.5
71.6 @{theory} is NOT Isac.thy, but some predecessor, which causes
71.7 -the error 'ME_Isac "Isac" not in system'.
71.8 +the error 'ME_Isac "Isac_Knowledge" not in system'.
71.9 *)
71.10
72.1 --- a/test/Tools/isac/Knowledge/logexp.sml Mon Aug 26 09:20:07 2019 +0200
72.2 +++ b/test/Tools/isac/Knowledge/logexp.sml Mon Aug 26 17:40:27 2019 +0200
72.3 @@ -24,7 +24,7 @@
72.4
72.5 equality_power;
72.6 exp_invers_log;
72.7 -(* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac") works ?
72.8 +(* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac_Knowledge") works ?
72.9 refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"]
72.10 ["equation","test"]; *)
72.11 *)
72.12 @@ -37,7 +37,7 @@
72.13
72.14 val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"];
72.15 val (dI',pI',mI') =
72.16 - ("Isac",["logarithmic","univariate","equation","test"],
72.17 + ("Isac_Knowledge",["logarithmic","univariate","equation","test"],
72.18 ["Test","solve_log"]);
72.19 val p = e_pos'; val c = [];
72.20 (*============ inhibit exn 110726 ==============================================
73.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Mon Aug 26 09:20:07 2019 +0200
73.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Mon Aug 26 17:40:27 2019 +0200
73.3 @@ -28,7 +28,7 @@
73.4 "----------- why helpless here ? ------------------------";
73.5 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
73.6 "functionName X_z", "stepResponse (x[n::real]::bool)"];
73.7 -val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
73.8 +val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
73.9 ["SignalProcessing","Z_Transform","Inverse"]);
73.10 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
73.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
73.12 @@ -77,7 +77,7 @@
73.13 "----------- fun factors_from_solution ------------------";
73.14 "----------- fun factors_from_solution ------------------";
73.15 "----------- fun factors_from_solution ------------------";
73.16 -val ctxt = Proof_Context.init_global @{theory Isac};
73.17 +val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
73.18 val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
73.19 val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
73.20 if term2str t' =
73.21 @@ -150,13 +150,13 @@
73.22 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)"*)
73.23 (*[5], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["z = 1 / 2"])*)
73.24 (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*nxt = Rewrite_Set "norm_Rational"*)
73.25 -(*[6], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt;(*nxt = Subproblem ("Isac", ["normalise", "polynomial", "univariate", "equation"]*)
73.26 +(*[6], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt;(*nxt = Subproblem ("Isac_Knowledge", ["normalise", "polynomial", "univariate", "equation"]*)
73.27 (*30+1*)
73.28 (*[7], Pbl*)val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' [] pt'''; (*nxt = Model_Problem*)
73.29 (*[7], Pbl*)val (p'v,_,f,nxt'v,_,pt'v) = me nxt'''' p'''' [] pt''''; (*nxt = Add_Given "equality (3 = 3 * AA / 4)")*)
73.30 (*[7], Pbl*)val (p'v',_,f,nxt'v',_,pt'v') = me nxt'v p'v [] pt'v; (*nxt = Add_Given "solveFor AA")*)
73.31 (*[7], Pbl*)val (p'v'',_,f,nxt'v'',_,pt'v'') = me nxt'v' p'v' [] pt'v'; (*nxt = Add_Find "solutions AA_i")*)
73.32 -(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt'v'' p'v'' [] pt'v''; (*nxt = Specify_Theory "Isac"*)
73.33 +(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt'v'' p'v'' [] pt'v''; (*nxt = Specify_Theory "Isac_Knowledge"*)
73.34 (*35*)
73.35 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*)
73.36 (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "normalise_poly"])*)
73.37 @@ -165,7 +165,7 @@
73.38 (*[7, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', AA)"], "make_ratpoly_in")*)
73.39 (*40*)
73.40 (*[7, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify"*)
73.41 -(*[7, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Isac", ["degree_1", "polynomial", "univariate", "equation"])*)
73.42 +(*[7, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Isac_Knowledge", ["degree_1", "polynomial", "univariate", "equation"])*)
73.43 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
73.44 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (3 + -3 / 4 * AA = 0)"*)
73.45 (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor AA"*)
73.46 @@ -431,14 +431,14 @@
73.47 "----------- progr.vers.2: check erls for multiply_ansatz";
73.48 (*test for outcommented 3 lines in script: is norm_Rational strong enough?*)
73.49 val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))";
73.50 -val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t;
73.51 +val SOME (t', _) = rewrite_set_ @{theory Isac_Knowledge} true ansatz_rls t;
73.52 term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
73.53
73.54 -val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*)
73.55 +val SOME (t'', _) = rewrite_set_ @{theory Isac_Knowledge} true multiply_ansatz t'; (*true*)
73.56 term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
73.57 "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
73.58
73.59 -val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
73.60 +val SOME (t''', _) = rewrite_set_ @{theory Isac_Knowledge} true norm_Rational t'';
73.61 if term2str t''' = "3 = (AA + -2 * BB + 4 * z * AA + 4 * z * BB) / 4" then ()
73.62 else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
73.63
73.64 @@ -510,7 +510,7 @@
73.65 val fmz_from_Subproblem_of_Inverse_sub = (*see --- test [SignalProcessing,Z_Transform,Inverse_s.."*)
73.66 (["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))", "solveFor z",
73.67 "decomposedFunction p_p'''"],
73.68 - ("Isac", ["partial_fraction", "rational", "simplification"],
73.69 + ("Isac_Knowledge", ["partial_fraction", "rational", "simplification"],
73.70 ["simplification", "of_rationals", "to_partial_fraction"]))
73.71 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz_from_Subproblem_of_Inverse_sub)];
73.72 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
73.73 @@ -574,7 +574,7 @@
73.74 val fmz_from_Subproblem_of_Inverse_sub = (*see --- test [SignalProcessing,Z_Transform,Inverse_s.."*)
73.75 (["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))", "solveFor z",
73.76 "decomposedFunction p_p'''"],
73.77 - ("Isac", ["partial_fraction", "rational", "simplification"],
73.78 + ("Isac_Knowledge", ["partial_fraction", "rational", "simplification"],
73.79 ["simplification", "of_rationals", "to_partial_fraction"]));
73.80 CalcTree [fmz_from_Subproblem_of_Inverse_sub];
73.81 Iterator 1;
74.1 --- a/test/Tools/isac/Knowledge/poly.sml Mon Aug 26 09:20:07 2019 +0200
74.2 +++ b/test/Tools/isac/Knowledge/poly.sml Mon Aug 26 17:40:27 2019 +0200
74.3 @@ -334,7 +334,7 @@
74.4 "-------- fun is_multUnordered --------------------------";
74.5 "-------- fun is_multUnordered --------------------------";
74.6 "-------- fun is_multUnordered --------------------------";
74.7 -val thy = @{theory "Isac"};
74.8 +val thy = @{theory "Isac_Knowledge"};
74.9 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
74.10 val t = str2term "x^^^2 * x";
74.11 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
74.12 @@ -671,7 +671,7 @@
74.13
74.14 (*WN071202: ^^^ why then is there no rewriting ...*)
74.15 val term = str2term "2*b + (3*a + 3*b)";
74.16 -val NONE = rewrite_set_ (@{theory "Isac"}) false order_add_mult term;
74.17 +val NONE = rewrite_set_ (@{theory "Isac_Knowledge"}) false order_add_mult term;
74.18
74.19 (*or why is there no rewriting this way...*)
74.20 val t1 = str2term "2 * b + (3 * a + 3 * b)";
75.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Mon Aug 26 09:20:07 2019 +0200
75.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Mon Aug 26 17:40:27 2019 +0200
75.3 @@ -151,7 +151,7 @@
75.4 "----- d2_pqformula1 ------!!!!";
75.5 val fmz = ["equality (-1/8 + (-1/4)*z + z^^^2 = (0::real))", "solveFor z","solutions L"];
75.6 val (dI',pI',mI') =
75.7 - ("Isac", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
75.8 + ("Isac_Knowledge", ["pqFormula","degree_2","polynomial","univariate","equation"], ["no_met"]);
75.9 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
75.10 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
75.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
76.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Aug 26 09:20:07 2019 +0200
76.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Aug 26 17:40:27 2019 +0200
76.3 @@ -423,16 +423,16 @@
76.4 val erls = erls_ordne_alphabetisch;
76.5 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
76.6 val SOME (t',_) =
76.7 - rewrite_ (@{theory "Isac"}) e_rew_ord erls false @{thm tausche_minus} t;
76.8 + rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus} t;
76.9 term2str t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";
76.10
76.11 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
76.12 val NONE =
76.13 - rewrite_ (@{theory "Isac"}) e_rew_ord erls false @{thm tausche_minus_plus} t;
76.14 + rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus_plus} t;
76.15
76.16 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
76.17 val SOME (t',_) =
76.18 - rewrite_set_ (@{theory "Isac"}) false ordne_alphabetisch t;
76.19 + rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
76.20 term2str t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
76.21 trace_rewrite := false;
76.22
77.1 --- a/test/Tools/isac/Knowledge/rational.sml Mon Aug 26 09:20:07 2019 +0200
77.2 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Aug 26 17:40:27 2019 +0200
77.3 @@ -205,7 +205,7 @@
77.4 (again) get prepat = [] changed to <>[]. *)
77.5 val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)";
77.6
77.7 -(*rewrite_set_ @{theory Isac} true cancel t = NONE; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
77.8 +(*rewrite_set_ @{theory Isac_Knowledge} true cancel t = NONE; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
77.9 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, cancel_p, t);
77.10 "~~~~~ fun rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
77.11 (thy, 1, bool, [], rls, term);
77.12 @@ -289,7 +289,7 @@
77.13 val t = str2term "(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";
77.14 (* "-------- example 187c": doesn't terminate...
77.15 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)
77.16 -"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (@{theory Isac}, false, cancel_p, t);
77.17 +"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (@{theory Isac_Knowledge}, false, cancel_p, t);
77.18 (* WN130827: exception Div raised...
77.19 rewrite__set_ thy 1 bool [] rls term
77.20 *)
77.21 @@ -367,7 +367,7 @@
77.22 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
77.23 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
77.24 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
77.25 -val thy = @{theory Isac};
77.26 +val thy = @{theory Isac_Knowledge};
77.27 "----- SK060904-2a non-termination of add_fraction_p_";
77.28 val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^
77.29 " (-1 * a + b * x) / (a + b * x) ");
77.30 @@ -376,7 +376,7 @@
77.31 (* rewrite_set_ thy false add_fractions_p t;
77.32 exception Div raised*)
77.33 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) =
77.34 - (@{theory Isac}, false, add_fractions_p, t);
77.35 + (@{theory Isac_Knowledge}, false, add_fractions_p, t);
77.36 "~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
77.37 (thy, 1, bool, [], rls, term);
77.38 (* app_rev thy (i+1) rrls t;
77.39 @@ -430,7 +430,7 @@
77.40 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
77.41 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
77.42 "----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
77.43 -val thy = @{theory Isac(*Partial_Fractions*)}
77.44 +val thy = @{theory Isac_Knowledge(*Partial_Fractions*)}
77.45 val ctxt = Proof_Context.init_global thy;
77.46
77.47 (*---------- (1) with Free A, B ----------------------------------------------------------------*)
77.48 @@ -840,7 +840,7 @@
77.49 ### Isabelle2009-2 for cancel_ (not cancel_p_):
77.50 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
77.51 andalso string_of_thm thm =
77.52 - (string_of_thm o Thm.make_thm o (Thm.global_cterm_of (@{theory "Isac"})))
77.53 + (string_of_thm o Thm.make_thm o (Thm.global_cterm_of (@{theory "Isac_Knowledge"})))
77.54 (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
77.55 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
77.56 \---------------------------------------------------------------------------------------/*)
77.57 @@ -859,7 +859,7 @@
77.58 (* find the next rule to apply *)
77.59 val SOME (r as (Thm (str, thm))) = nex revsets t;
77.60 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
77.61 - string_of_thm thm = (string_of_thm o Thm.make_thm o (Thm.global_cterm_of (@{theory "Isac"})))
77.62 + string_of_thm thm = (string_of_thm o Thm.make_thm o (Thm.global_cterm_of (@{theory "Isac_Knowledge"})))
77.63 (Trueprop $ (Thm.term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
77.64 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
77.65
77.66 @@ -1724,7 +1724,7 @@
77.67 "-------- fun eval_get_denominator -------------------------------------------";
77.68 "-------- fun eval_get_denominator -------------------------------------------";
77.69 "-------- fun eval_get_denominator -------------------------------------------";
77.70 -val thy = @{theory Isac};
77.71 +val thy = @{theory Isac_Knowledge};
77.72 val t = Thm.term_of (the (parse thy "get_denominator ((a +x)/b)"));
77.73 val SOME (_, t') = eval_get_denominator "" 0 t thy;
77.74 if term2str t' = "get_denominator ((a + x) / b) = b"
78.1 --- a/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Aug 26 09:20:07 2019 +0200
78.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl.sml Mon Aug 26 17:40:27 2019 +0200
78.3 @@ -8,7 +8,7 @@
78.4 "----------- Minisubplb/100-init-rootpbl.sml ---------------------";
78.5 val fmz = ["equality (AA+1=(2::real))", "solveFor AA","solutions L"];
78.6 val (dI',pI',mI') =
78.7 - ("Isac", ["sqroot-test","univariate","equation","test"],
78.8 + ("Isac_Knowledge", ["sqroot-test","univariate","equation","test"],
78.9 ["Test","squ-equ-test-subpbl1"]);
78.10 "~~~~~ fun CalcTreeTEST, args:"; val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
78.11 "~~~~~ fun nxt_specify_init_calc, args:"; val (fmz : fmz_, (dI, pI, mI) : spec) = (fmz, sp);
79.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon Aug 26 09:20:07 2019 +0200
79.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl.sml Mon Aug 26 17:40:27 2019 +0200
79.3 @@ -98,9 +98,9 @@
79.4 "~~~~~ fun assy , args:"; val ((ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss:step list), t)
79.5 = (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
79.6
79.7 -(*val (a', LTool.STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac" sr E a v t (*of*);
79.8 +(*val (a', LTool.STac stac) = ( *case*) Lucin.handle_leaf "locate" "Isac_Knowledge" sr E a v t (*of*);
79.9 "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, E, a, v, t)
79.10 - = ("locate", "Isac", sr, E, a, v, t);
79.11 + = ("locate", "Isac_Knowledge", sr, E, a, v, t);
79.12
79.13 val (a', LTool.STac stac) = (*case*) LTool.subst_stacexpr E a v t (*of*);
79.14 "~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Program.SubProblem", _) $ _ $ _)))
79.15 @@ -121,7 +121,7 @@
79.16 | _ => error ("assy: call by " ^ pos'2str (p,p_));
79.17 (**)val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*);
79.18 val (p'',c',f',pt') =
79.19 - Generate.generate1 (Celem.assoc_thy "Isac") m (Istate.Pstate (E,l,a',v',S,true), ctxt) (p',p_) pt;
79.20 + Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") m (Istate.Pstate (E,l,a',v',S,true), ctxt) (p',p_) pt;
79.21
79.22 (*+*)if is_e_ctxt ctxt then error "ERROR: assy returns e_ctxt" else ();
79.23 (*\\--1 end step into relevant call ----------------------------------------------------------//*)
80.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Aug 26 09:20:07 2019 +0200
80.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Aug 26 17:40:27 2019 +0200
80.3 @@ -94,7 +94,7 @@
80.4 val is = Generate.init_istate tac t
80.5 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
80.6 val pos' = ((lev_on o lev_dn) p, Frm)
80.7 - val thy = Celem.assoc_thy "Isac"
80.8 + val thy = Celem.assoc_thy "Isac_Knowledge"
80.9 val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *);
80.10
80.11 show_pt pt'; (* cut ctree after ([3,1,1], Frm) *)
81.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Mon Aug 26 09:20:07 2019 +0200
81.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Mon Aug 26 17:40:27 2019 +0200
81.3 @@ -103,7 +103,7 @@
81.4 "bound_variable x","error_bound 0"(*,
81.5 "solutions L::real set" ,
81.6 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
81.7 -val thy = (theory "Isac");
81.8 +val thy = (theory "Isac_Knowledge");
81.9 val formals = map (the o (parse thy)) origin;
81.10
81.11 val given = ["equation (l=(r::real))",
82.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Mon Aug 26 09:20:07 2019 +0200
82.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Mon Aug 26 17:40:27 2019 +0200
82.3 @@ -8,7 +8,7 @@
82.4
82.5 (*---------------- 25.7.02 ---------------------*)
82.6
82.7 -val thy = (theory "Isac");
82.8 +val thy = (theory "Isac_Knowledge");
82.9 val t = (Thm.term_of o the o (parse thy)) "contains_root (sqrt(x)=1)";
82.10 val SOME(ss,tt) = eval_contains_root "xxx" 1 t thy;
82.11
82.12 @@ -37,26 +37,26 @@
82.13 val t = (Thm.term_of o the o (parse Test.thy))
82.14 "is_rootequation_in (sqrt(x)=1) x";
82.15 atomty t;
82.16 -val t = (Thm.term_of o the o (parse (theory "Isac")))
82.17 +val t = (Thm.term_of o the o (parse (theory "Isac_Knowledge")))
82.18 "is_rootequation_in (sqrt(x)=1) x";
82.19 atomty t;
82.20
82.21 (*
82.22 val SOME(tt,_) = rewrite_set_ Test.thytrue tval_rls t;
82.23 *)
82.24 -val SOME(tt,_) = rewrite_set_ (theory "Isac") true tval_rls t;
82.25 +val SOME(tt,_) = rewrite_set_ (theory "Isac_Knowledge") true tval_rls t;
82.26
82.27 -rewrite_set "Isac" true
82.28 +rewrite_set "Isac_Knowledge" true
82.29 "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
82.30 rewrite_set "Test" true
82.31 "tval_rls" "is_rootequation_in (sqrt(x)=1) x";
82.32
82.33
82.34 -(*WN: ^^^--- bitte nimm vorerst immer (theory "Isac"), damit wird richtig gematcht,
82.35 +(*WN: ^^^--- bitte nimm vorerst immer (theory "Isac_Knowledge"), damit wird richtig gematcht,
82.36 siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*)
82.37
82.38 KEStore_Elems.add_pbts
82.39 - [prep_pbt (*Test.thy*) (theory "Isac")
82.40 + [prep_pbt (*Test.thy*) (theory "Isac_Knowledge")
82.41 (["rootX","univariate","equation","test"],
82.42 [("#Given" ,["equality e_e","solveFor v_v"]),
82.43 ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),
82.44 @@ -68,7 +68,7 @@
82.45 match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["rootX","univariate","equation","test"]);
82.46
82.47 KEStore_Elems.add_pbts
82.48 - [prep_pbt (theory "Isac")
82.49 + [prep_pbt (theory "Isac_Knowledge")
82.50 (["approximate","univariate","equation","test"],
82.51 [("#Given", ["equality e_e","solveFor v_v","errorBound err_"]),
82.52 ("#Where", ["matches (?a = ?b) e_e"]),
82.53 @@ -79,7 +79,7 @@
82.54 methods:= overwritel (!methods,
82.55 [
82.56 prep_met
82.57 - (("Isac","solve_univar_err"):metID,
82.58 + (("Isac_Knowledge","solve_univar_err"):metID,
82.59 [("#Given" ,["equality e_e","solveFor v_v","errorBound err_"]),
82.60 ("#Find" ,["solutions v_i_"])
82.61 ],
82.62 @@ -96,8 +96,8 @@
82.63 val fmz = ["equality (1+2*x=0)","solveFor x","errorBound (eps=0)",
82.64 "solutions L"];
82.65 val (dI',pI',mI') =
82.66 - ("Isac",["approximate","univariate","equation","test"],
82.67 - ("Isac","solve_univar_err"));
82.68 + ("Isac_Knowledge",["approximate","univariate","equation","test"],
82.69 + ("Isac_Knowledge","solve_univar_err"));
82.70 val p = e_pos'; val c = [];
82.71 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
82.72 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
82.73 @@ -108,7 +108,7 @@
82.74 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82.75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82.76 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82.77 -(*val nxt = ("Apply_Method",Apply_Method ("Isac","solve_univar_err"))*)
82.78 +(*val nxt = ("Apply_Method",Apply_Method ("Isac_Knowledge","solve_univar_err"))*)
82.79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82.80 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;
82.81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82.82 @@ -135,8 +135,8 @@
82.83 val fmz = ["equality (sqrt(x) - 1 = 0)","solveFor x","errorBound (eps=0)",
82.84 "solutions L"];
82.85 val (dI',pI',mI') =
82.86 - ("Isac",["approximate","univariate","equation","test"],
82.87 - ("Isac","solve_univar_err"));
82.88 + ("Isac_Knowledge",["approximate","univariate","equation","test"],
82.89 + ("Isac_Knowledge","solve_univar_err"));
82.90 val p = e_pos'; val c = [];
82.91 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
82.92 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
82.93 @@ -147,7 +147,7 @@
82.94 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82.95 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82.96 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82.97 -(*val nxt = ("Apply_Method",Apply_Method ("Isac","solve_univar_err"))*)
82.98 +(*val nxt = ("Apply_Method",Apply_Method ("Isac_Knowledge","solve_univar_err"))*)
82.99 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82.100 val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e;
82.101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
83.1 --- a/test/Tools/isac/ProgLang/calculate.sml Mon Aug 26 09:20:07 2019 +0200
83.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Mon Aug 26 17:40:27 2019 +0200
83.3 @@ -146,7 +146,7 @@
83.4 (*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
83.5
83.6 val t = str2term "2 * x is_const";
83.7 - val SOME (str,t') = eval_const "" "" t (@{theory "Isac"});
83.8 + val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
83.9 term2str t';
83.10
83.11
84.1 --- a/test/Tools/isac/ProgLang/contextC.sml Mon Aug 26 09:20:07 2019 +0200
84.2 +++ b/test/Tools/isac/ProgLang/contextC.sml Mon Aug 26 17:40:27 2019 +0200
84.3 @@ -59,7 +59,7 @@
84.4 "----------- fun transfer_asms_from_to ---------------------------------------------------------";
84.5 "----------- fun transfer_asms_from_to ---------------------------------------------------------";
84.6 "----------- fun transfer_asms_from_to ---------------------------------------------------------";
84.7 -val ctxt = Proof_Context.init_global @{theory "Isac"}
84.8 +val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
84.9 val from_ctxt = insert_assumptions
84.10 [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
84.11 val to_ctxt = insert_assumptions
84.12 @@ -71,7 +71,7 @@
84.13 "----------- fun from_subpbl_to_caller ---------------------------------------------------------";
84.14 "----------- fun from_subpbl_to_caller ---------------------------------------------------------";
84.15 "----------- fun from_subpbl_to_caller ---------------------------------------------------------";
84.16 -val ctxt = Proof_Context.init_global @{theory "Isac"}
84.17 +val ctxt = Proof_Context.init_global @{theory "Isac_Knowledge"}
84.18 val sub_ctxt = insert_assumptions
84.19 [str2term "a < (fro::int)", str2term "b < (fro::int)"] ctxt
84.20 val caller_ctxt = insert_assumptions
85.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Mon Aug 26 09:20:07 2019 +0200
85.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml Mon Aug 26 17:40:27 2019 +0200
85.3 @@ -301,7 +301,7 @@
85.4 ----- 2009 -------------------------------------------------------------------*)
85.5
85.6 (*the situation as was before repair (asm without Trueprop) is outcommented*)
85.7 -val thy = @{theory "Isac"};
85.8 +val thy = @{theory "Isac_Knowledge"};
85.9 "===== example which raised the problem =================";
85.10 val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
85.11 "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
85.12 @@ -349,7 +349,7 @@
85.13 "----------- compare all prepat's existing 2010 ---------";
85.14 "----------- compare all prepat's existing 2010 ---------";
85.15 "----------- compare all prepat's existing 2010 ---------";
85.16 -val thy = @{theory "Isac"};
85.17 +val thy = @{theory "Isac_Knowledge"};
85.18 val t = @{term "a + b * x = (0 ::real)"};
85.19 val pat = parse_patt thy "?l = (?r ::real)";
85.20 val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
85.21 @@ -511,7 +511,7 @@
85.22 val t = str2term "(2*x)/1"; (*Type real*)
85.23
85.24 val (thy, ro, er, inst) =
85.25 - (@{theory "Isac"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
85.26 + (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
85.27 val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
85.28
85.29 "----------- repair NO asms from rls RatEq_eliminate ----";
85.30 @@ -593,7 +593,7 @@
85.31 "----------- fun mk_thm ------------------------------------------------------------------------";
85.32 "----------- fun mk_thm ------------------------------------------------------------------------";
85.33 "----------- fun mk_thm ------------------------------------------------------------------------";
85.34 -val thy = @{theory Isac}
85.35 +val thy = @{theory Isac_Knowledge}
85.36
85.37 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
85.38 val thm = @{thm realpow_twoI};
86.1 --- a/test/Tools/isac/ProgLang/termC.sml Mon Aug 26 09:20:07 2019 +0200
86.2 +++ b/test/Tools/isac/ProgLang/termC.sml Mon Aug 26 17:40:27 2019 +0200
86.3 @@ -235,7 +235,7 @@
86.4 val t = (Thm.term_of o the o (parse thy)) "3 * x^^^2 = (1::real)";
86.5 val pat = (free2var o Thm.term_of o the o (parse thy)) "a * b^^^2 = (c::real)";
86.6 (* !^^^^^^^^!... necessary for Pattern.match, see Logic.varify_global below*)
86.7 - val insts = Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty);
86.8 + val insts = Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty);
86.9 (*default_print_depth 3; 999*) insts;
86.10 (*val insts =
86.11 ({},
86.12 @@ -245,7 +245,7 @@
86.13
86.14 "----- throws exn MATCH...";
86.15 (* val t = str2term "x";
86.16 - (Pattern.match @{theory "Isac"} (pat, t) (Vartab.empty, Vartab.empty))
86.17 + (Pattern.match @{theory "Isac_Knowledge"} (pat, t) (Vartab.empty, Vartab.empty))
86.18 handle MATCH => ???; *)
86.19
86.20 val thy = @{theory "Complex_Main"};
86.21 @@ -488,8 +488,8 @@
86.22 "----------- check writeln, tracing for string markup ---";
86.23 val t = @{term "x + 1"};
86.24 val str_markup = (Syntax.string_of_term
86.25 - (Proof_Context.init_global (Thy_Info_get_theory "Isac"))) t;
86.26 - val str = term_to_string'' "Isac" t;
86.27 + (Proof_Context.init_global (Thy_Info_get_theory "Isac_Knowledge"))) t;
86.28 + val str = term_to_string'' "Isac_Knowledge" t;
86.29
86.30 writeln "----------------writeln str_markup---";
86.31 writeln str_markup;
86.32 @@ -526,8 +526,8 @@
86.33 "----------- check writeln, tracing for string markup ---";
86.34 val t = @{term "x + 1"};
86.35 val str_markup = (Syntax.string_of_term
86.36 - (Proof_Context.init_global (Thy_Info_get_theory "Isac"))) t;
86.37 - val str = term_to_string'' "Isac" t;
86.38 + (Proof_Context.init_global (Thy_Info_get_theory "Isac_Knowledge"))) t;
86.39 + val str = term_to_string'' "Isac_Knowledge" t;
86.40
86.41 writeln "----------------writeln str_markup---";
86.42 writeln str_markup;
87.1 --- a/test/Tools/isac/Test_Some.thy Mon Aug 26 09:20:07 2019 +0200
87.2 +++ b/test/Tools/isac/Test_Some.thy Mon Aug 26 17:40:27 2019 +0200
87.3 @@ -71,34 +71,6 @@
87.4 "~~~~~ fun xxx , args:"; val () = ();
87.5 \<close>
87.6
87.7 -section \<open>===================================================================================\<close>
87.8 -ML \<open>
87.9 -"~~~~~ fun xxx , args:"; val () = ();
87.10 -\<close> ML \<open>
87.11 -"----------- fun revert_sym --------------------------------------";
87.12 -"----------- fun revert_sym --------------------------------------";
87.13 -"----------- fun revert_sym --------------------------------------";
87.14 -val thy = @{theory Isac}
87.15 -val (Thm (thmID, thm)) =
87.16 - revert_sym thy (Thm ("sym_real_mult_minus1", num_str (@{thm real_mult_minus1} RS @{thm sym})))
87.17 -;
87.18 -\<close> ML \<open>
87.19 -thmID
87.20 -\<close> ML \<open>
87.21 -if thmID = "Poly.real_mult_minus1" andalso string_of_thmI thm = "-1 * ?z = - ?z"
87.22 -then () else error "fun revert_sym changed 1";
87.23 -
87.24 -val (Thm (thmID, thm)) =
87.25 - revert_sym thy (Thm ("real_diff_minus", num_str @{thm real_diff_minus}))
87.26 -;
87.27 -if thmID = "Root.real_diff_minus" andalso string_of_thmI thm = "?a - ?b = ?a + -1 * ?b"
87.28 -then () else error "fun revert_sym changed 2"
87.29 -
87.30 -\<close> ML \<open>
87.31 -\<close> ML \<open>
87.32 -"~~~~~ fun xxx , args:"; val () = ();
87.33 -\<close>
87.34 -
87.35 section \<open>===========--- x / (x ^ 2 - 6 * x + 9) - 1 / (x ^ 2 - 3 * x) = 1 /x"===============\<close>
87.36 ML \<open>
87.37 "~~~~~ fun xxx , args:"; val () = ();
88.1 --- a/test/Tools/isac/kestore.sml Mon Aug 26 09:20:07 2019 +0200
88.2 +++ b/test/Tools/isac/kestore.sml Mon Aug 26 17:40:27 2019 +0200
88.3 @@ -1,10 +1,6 @@
88.4 (* Title: tests for KEStore.thy
88.5 Author: Walther Neuper
88.6 Use is subject to license terms.
88.7 -
88.8 -theory Test_Some imports Isac.Isac begin
88.9 -ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
88.10 -ML_file "kestore.sml"
88.11 *)
88.12
88.13 "-----------------------------------------------------------------------------";
88.14 @@ -23,7 +19,7 @@
88.15 "(e_rls, (KEStore, Rls {#calc = 0, #rules = 0, ...))"
88.16 then () else error "check_kestore_rls changed"
88.17 ;
88.18 -Test_KEStore_Elems.get_rlss @{theory Isac}
88.19 +Test_KEStore_Elems.get_rlss @{theory Isac_Knowledge}
88.20 |> map check_kestore_rls
88.21 |> enumerate_strings
88.22 |> sort string_ord
89.1 --- a/test/Tools/isac/xmlsrc/mathml.sml Mon Aug 26 09:20:07 2019 +0200
89.2 +++ b/test/Tools/isac/xmlsrc/mathml.sml Mon Aug 26 17:40:27 2019 +0200
89.3 @@ -48,21 +48,21 @@
89.4 (*str2term str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
89.5 Failed to parse term*)*)
89.6 "~~~~~ fun str2term, args:"; val (str) = (str);
89.7 -Thy_Info_get_theory "Isac";
89.8 +Thy_Info_get_theory "Isac_Knowledge";
89.9
89.10 parse_patt;
89.11 -parse_patt (Thy_Info_get_theory "Isac");
89.12 -(*parse_patt (Thy_Info_get_theory "Isac") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
89.13 +parse_patt (Thy_Info_get_theory "Isac_Knowledge");
89.14 +(*parse_patt (Thy_Info_get_theory "Isac_Knowledge") str; (* ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
89.15 Failed to parse term*)*)
89.16
89.17 -"~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info_get_theory "Isac"), str);
89.18 +"~~~~~ fun parse_patt, args:"; val (thy, str) = ((Thy_Info_get_theory "Isac_Knowledge"), str);
89.19 (thy, str)
89.20 |>> thy2ctxt
89.21 (*|-> Proof_Context.read_term_pattern (*ERROR: Inner syntax error at "; 0 < ?n |] ==> ?a / ?b ^ ?n = ?a * ?b ^ - ?n"
89.22 Failed to parse term*)*)
89.23
89.24 Proof_Context.read_term_pattern;
89.25 -(@{theory "Isac"}, str) |>> thy2ctxt;
89.26 +(@{theory "Isac_Knowledge"}, str) |>> thy2ctxt;
89.27 "~~~~~ fun Proof_Context.read_term_pattern, args:"; val () = ();
89.28 (*AK110725 To be continued...*)
89.29 *)
90.1 --- a/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Mon Aug 26 09:20:07 2019 +0200
90.2 +++ b/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Mon Aug 26 17:40:27 2019 +0200
90.3 @@ -8,7 +8,7 @@
90.4 CAUTION with testing *2file functions -- they are actually writing !!!
90.5 *)
90.6
90.7 -val thy = @{theory "Isac"};
90.8 +val thy = @{theory "Isac_Knowledge"};
90.9
90.10 "-----------------------------------------------------------------";
90.11 "table of contents -----------------------------------------------";
90.12 @@ -144,8 +144,8 @@
90.13 "----- fun pbl2term ----------------------------------------------";
90.14 "----- fun pbl2term ----------------------------------------------";
90.15 (*see WN120405a.TODO.txt*)
90.16 -if term2str (pbl2term (Thy_Info_get_theory "Isac") ["equations","univariate","normalise"]) =
90.17 - "Problem (Isac', [normalise, univariate, equations])"
90.18 +if term2str (pbl2term (Thy_Info_get_theory "Isac_Knowledge") ["equations","univariate","normalise"]) =
90.19 + "Problem (Isac_Knowledge', [normalise, univariate, equations])"
90.20 then () else error "fun pbl2term changed";
90.21
90.22 "----- fun insert_errpats ----------------------------------------";
91.1 --- a/test/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Aug 26 09:20:07 2019 +0200
91.2 +++ b/test/Tools/isac/xmlsrc/thy-hierarchy.sml Mon Aug 26 17:40:27 2019 +0200
91.3 @@ -10,7 +10,7 @@
91.4 CAUTION with testing *2file functions -- they are actually writing to ~/tmp
91.5 *)
91.6
91.7 -val thy = @{theory "Isac"};
91.8 +val thy = @{theory "Isac_Knowledge"};
91.9
91.10 "-----------------------------------------------------------------";
91.11 "table of contents -----------------------------------------------";
91.12 @@ -184,7 +184,7 @@
91.13 "----------- fun revert_sym --------------------------------------";
91.14 "----------- fun revert_sym --------------------------------------";
91.15 "----------- fun revert_sym --------------------------------------";
91.16 -val thy = @{theory Isac}
91.17 +val thy = @{theory Isac_Knowledge}
91.18 val (Thm (thmID, thm)) =
91.19 revert_sym thy (Thm ("sym_real_mult_minus1", num_str (@{thm real_mult_minus1} RS @{thm sym})))
91.20 ;
91.21 @@ -210,7 +210,7 @@
91.22 then () else error "thms_of_rlss changed"
91.23 *)
91.24 ;
91.25 -"~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac}, rlss);
91.26 +"~~~~~ fun thms_of_rlss, args:"; val (thy, rlss) = (@{theory Isac_Knowledge}, rlss);
91.27 val rlss' = (rlss : (rls' * (theory' * rls)) list)
91.28 |> map (thms_of_rls o #2 o #2)
91.29 (* = [[], [Thm ("real_diff_minus", "?a - ?b = ?a + -1 * ?b"),