1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Mon Apr 27 16:40:11 2020 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Tue Apr 28 15:31:49 2020 +0200
1.3 @@ -14,6 +14,7 @@
1.4
1.5 ML \<open>
1.6 \<close> ML \<open>
1.7 +Library.distinct: ('a * 'a -> bool) -> 'a list -> 'a list
1.8 \<close> ML \<open>
1.9 \<close>
1.10 end
1.11 \ No newline at end of file
2.1 --- a/src/Tools/isac/BaseDefinitions/cas-def.sml Mon Apr 27 16:40:11 2020 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/cas-def.sml Tue Apr 28 15:31:49 2020 +0200
2.3 @@ -22,7 +22,6 @@
2.4 struct
2.5 (**)
2.6
2.7 -(*/------- to Celem7 -------\*)
2.8 (* association list with cas-commands, for generating a complete calc-head *)
2.9 type generate_fn =
2.10 (term list -> (* the arguments of the cas-command, eg. (x+1=2, x) *)
2.11 @@ -34,6 +33,5 @@
2.12 (Spec.T * (* theory, problem, method *)
2.13 generate_fn))
2.14 fun equal ((t1, (_, _)) : T, (t2, (_, _)) : T) = t1 = t2
2.15 -(*\------- to Celem7 -------/*)
2.16
2.17 (**)end(**)
3.1 --- a/src/Tools/isac/BaseDefinitions/celem-4.sml Mon Apr 27 16:40:11 2020 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/celem-4.sml Tue Apr 28 15:31:49 2020 +0200
3.3 @@ -4,15 +4,11 @@
3.4
3.5 *)
3.6 signature CALCELEMENT_4 =
3.7 -(*/------- to Celem4 -------\*)
3.8 -(*\------- to Celem4 -------/*)
3.9 sig
3.10 -(*/------- to Celem4 -------\*)
3.11 type pat
3.12 val pats2str: pat list -> string
3.13 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.14 val pats2str' : pat list -> string
3.15 -(*\------- to Celem4 -------/*)
3.16 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
3.17 (*NONE*)
3.18 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.19 @@ -25,7 +21,6 @@
3.20 struct
3.21 (**)
3.22
3.23 -(*/------- to Celem4 -------\*)
3.24 (* the pattern for an item of a problems model or a methods guard *)
3.25 type pat =
3.26 (string * (* field *)
3.27 @@ -37,6 +32,5 @@
3.28 fun pat2str' ((field, (dsc, id)) : pat) =
3.29 pair2str (field, pair2str (UnparseC.term dsc, UnparseC.term id)) ^ "\n"
3.30 fun pats2str' pats = (strs2str o (map pat2str')) pats
3.31 -(*\------- to Celem4 -------/*)
3.32
3.33 (**)end(**)
4.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Mon Apr 27 16:40:11 2020 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Tue Apr 28 15:31:49 2020 +0200
4.3 @@ -67,7 +67,6 @@
4.4 val empty_store = Store.Node ("empty_meth_id", [empty],[]);
4.5
4.6 type store = (T Store.node) list;
4.7 -(*\------- to Celem6 -------/*)
4.8
4.9 val check_unique =
4.10 Check_Unique.message (Check_Unique.collect (#guh: T -> Check_Unique.id));
5.1 --- a/src/Tools/isac/BaseDefinitions/problem-def.sml Mon Apr 27 16:40:11 2020 +0200
5.2 +++ b/src/Tools/isac/BaseDefinitions/problem-def.sml Tue Apr 28 15:31:49 2020 +0200
5.3 @@ -65,11 +65,9 @@
5.4 ^ (Rule_Set.id prls' |> quote) ^ ", thy = {" ^ Context.theory_name thy' ^ "}, where_ = "
5.5 ^ (UnparseC.terms w') ^ "}" |> linefeed;
5.6 fun s_to_string pbts = map pbt2str pbts |> list2str;
5.7 -(*\------- to Celem5 -------/*)
5.8 -(*/------- to Celem5 -------\*)
5.9 +
5.10 val empty_store = Store.Node ("empty_probl_id", [empty], [])
5.11 type store = (T Store.node) list
5.12 -(*\------- to Celem5 -------/*)
5.13
5.14 val check_unique =
5.15 Check_Unique.message (Check_Unique.collect (#guh : T -> Check_Unique.id));
6.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml Mon Apr 27 16:40:11 2020 +0200
6.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml Tue Apr 28 15:31:49 2020 +0200
6.3 @@ -17,8 +17,9 @@
6.4 val keep_unique_rules: string -> T -> Rule_Def.rule list -> T
6.5 val merge: string -> T -> T -> T
6.6 val get_rules: T -> Rule_Def.rule list
6.7 -(*val rule2rls' : Rule.rule -> string*)
6.8 - val id_from_rule : Rule.rule -> string
6.9 +(*val rule2rls': Rule.rule -> string*)
6.10 + val id_from_rule: Rule.rule -> string
6.11 + val contains: Rule.rule -> T -> bool
6.12
6.13 type for_kestore
6.14 val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
6.15 @@ -156,6 +157,18 @@
6.16 fun id_from_rule (Rule.Rls_ rls) = id rls
6.17 | id_from_rule r = raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string r);
6.18
6.19 +(* check if a rule is contained in a rule-set (recursivley down in Rls_);
6.20 + this rule can even be a rule-set itself *)
6.21 +fun contains r rls =
6.22 + let
6.23 + fun (*find (_, Rls_ rls) = finds (get_rules rls)
6.24 + | find r12 = equal r12
6.25 + and*) finds [] = false
6.26 + | finds (r1 :: rs) = if Rule.equal (r, r1) then true else finds rs
6.27 + in
6.28 + finds (get_rules rls)
6.29 + end
6.30 +
6.31 (*/------- this will disappear eventually -----------\*)
6.32 type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
6.33 (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
7.1 --- a/src/Tools/isac/BaseDefinitions/rule.sml Mon Apr 27 16:40:11 2020 +0200
7.2 +++ b/src/Tools/isac/BaseDefinitions/rule.sml Tue Apr 28 15:31:49 2020 +0200
7.3 @@ -18,6 +18,8 @@
7.4 val to_string_short: Rule_Def.rule -> string
7.5
7.6 val thm: rule -> thm
7.7 + val distinct : rule list -> rule list
7.8 +
7.9 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.10 val thm_id: rule -> string
7.11 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
7.12 @@ -52,6 +54,7 @@
7.13 | equal (Rule_Def.Eval (id1, _), Rule_Def.Eval (id2, _)) = id1 = id2
7.14 | equal (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = set_id rls1 = set_id rls2
7.15 | equal _ = false;
7.16 +fun distinct rs = Library.distinct equal rs
7.17
7.18 fun to_string Rule_Def.Erule = "Erule"
7.19 | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thm thm ^ ")"
8.1 --- a/src/Tools/isac/BaseDefinitions/store.sml Mon Apr 27 16:40:11 2020 +0200
8.2 +++ b/src/Tools/isac/BaseDefinitions/store.sml Tue Apr 28 15:31:49 2020 +0200
8.3 @@ -35,7 +35,7 @@
8.4 (**)
8.5
8.6 type key = string list; (*will become pblID, methID, theID*)
8.7 -(*/------- to Store -------\*)
8.8 +
8.9 (* A tree for storing data defined in different theories
8.10 for access from the Interpreter and from dialogue authoring
8.11 using a string list as key.
8.12 @@ -104,6 +104,5 @@
8.13 then ((Node (key, d, update ID is data pys)) :: pyss)
8.14 else (py :: (update ID (i :: is) data pyss))
8.15 | update _ _ _ _ = raise ERROR "update called with undef pattern.";
8.16 -(*\------- to Store -------/*)
8.17
8.18 (**)end(**)
9.1 --- a/src/Tools/isac/BaseDefinitions/thy-html.sml Mon Apr 27 16:40:11 2020 +0200
9.2 +++ b/src/Tools/isac/BaseDefinitions/thy-html.sml Tue Apr 28 15:31:49 2020 +0200
9.3 @@ -42,7 +42,6 @@
9.4 struct
9.5 (**)
9.6
9.7 -(*/------- to Celem8 -------\*)
9.8 (*the key into the hierarchy ob theory elements*)
9.9 type theID = string list;
9.10 val theID2str = strs2str; (*theID eg. is ["IsacKnowledge", "Test", "Rulesets", "ac_plus_times"]*)
9.11 @@ -66,9 +65,7 @@
9.12 | the2str (Hcal {guh, ...}) = guh
9.13 | the2str (Hord {guh, ...}) = guh
9.14 fun thes2str thes = map the2str thes |> list2str;
9.15 -(*\------- to Celem8 -------/*)
9.16
9.17 -(*/------- to Celem8 -------\*)
9.18 (* notes on thehier concerning sym_thmID theorems (created in derivations, reverse rewriting)
9.19 (a): thehier does not contain sym_thmID theorems
9.20 (b): lookup for sym_thmID directly from Isabelle using sym_thm
9.21 @@ -164,9 +161,7 @@
9.22 | "Orders" => ord2guh (isa, thyID) elemID
9.23 | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
9.24 | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
9.25 -(*\------- to Celem8 -------/*)
9.26
9.27 -(*/------- to Celem8 -------\*)
9.28 (* not only for thydata, but also for thy's etc *)
9.29 fun theID2guh [] = raise ERROR ("theID2guh: called with []")
9.30 | theID2guh [str] = part2guh [str]
9.31 @@ -179,8 +174,7 @@
9.32 | "Orders" => ord2guh (isa, thyID) elemID
9.33 | _ => raise ERROR ("theID2guh: called with theID = " ^ strs2str' strs))
9.34 | theID2guh strs = raise ERROR ("theID2guh called with theID = " ^ strs2str' strs);
9.35 -(*\------- to Celem8 -------/*)
9.36 -(*/------- to Celem8 -------\*)
9.37 +
9.38 fun Html_default exist = (Html {guh = theID2guh exist,
9.39 coursedesign = ["isac team 2006"], mathauthors = [], html = ""})
9.40
9.41 @@ -207,6 +201,5 @@
9.42 Hthm {guh = guh, coursedesign = coursedesign, mathauthors = mathauthors,
9.43 fillpats = fillpats', thm = thm}
9.44 | update_hthm _ _ = raise ERROR "update_hthm: wrong arguments";
9.45 -(*\------- to Celem8 -------/*)
9.46
9.47 (**)end(**)
10.1 --- a/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Mon Apr 27 16:40:11 2020 +0200
10.2 +++ b/src/Tools/isac/BridgeLibisabelle/BridgeLibisabelle.thy Tue Apr 28 15:31:49 2020 +0200
10.3 @@ -15,6 +15,7 @@
10.4
10.5 ML \<open>
10.6 \<close> ML \<open>
10.7 +ThmC.string_of_thm_in_thy @{theory} @{thm refl}
10.8 \<close> ML \<open>
10.9 \<close>
10.10 end
10.11 \ No newline at end of file
11.1 --- a/src/Tools/isac/Interpret/li-tool.sml Mon Apr 27 16:40:11 2020 +0200
11.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Tue Apr 28 15:31:49 2020 +0200
11.3 @@ -124,7 +124,7 @@
11.4 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
11.5 else Not_Associated
11.6 | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
11.7 - if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
11.8 + if Rule_Set.contains (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
11.9 if f = f_ then
11.10 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
11.11 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
11.12 @@ -139,7 +139,7 @@
11.13 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
11.14 else Not_Associated
11.15 | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
11.16 - if Rtools.contains_rule (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
11.17 + if Rule_Set.contains (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
11.18 if f = f_ then
11.19 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
11.20 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
11.21 @@ -180,12 +180,12 @@
11.22 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
11.23 else Not_Associated
11.24 | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
11.25 - if Rtools.contains_rule (Rule.Eval (assoc_calc' (ThyC.get_theory "Isac_Knowledge")
11.26 + if Rule_Set.contains (Rule.Eval (assoc_calc' (ThyC.get_theory "Isac_Knowledge")
11.27 op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
11.28 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
11.29 else Not_Associated
11.30 | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
11.31 - if Rtools.contains_rule (Rule.Eval (assoc_calc' ( ThyC.get_theory "Isac_Knowledge")
11.32 + if Rule_Set.contains (Rule.Eval (assoc_calc' ( ThyC.get_theory "Isac_Knowledge")
11.33 op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
11.34 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
11.35 else Not_Associated
12.1 --- a/src/Tools/isac/Interpret/rewtools.sml Mon Apr 27 16:40:11 2020 +0200
12.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Apr 28 15:31:49 2020 +0200
12.3 @@ -8,19 +8,11 @@
12.4 signature REWRITE_TOOLS =
12.5 sig
12.6
12.7 -(*/------- for error-fill-pattern -------\*)
12.8 +(*/------- to error-fill-pattern from Rtools -------\*)
12.9 val thy_containing_thm : string -> string * string
12.10 val thy_containing_rls : ThyC.id -> Rule_Set.id -> string * ThyC.id
12.11 val thy_containing_cal : ThyC.id -> Exec_Def.prog_calcID -> string * string
12.12 -(*\------- for error-fill-pattern -------/*)
12.13 -
12.14 -(*/------- for Fetch_Tacs ONLY -------\*)
12.15 - val atomic_appl_tacs : theory -> string -> Rule_Set.T -> term -> Tactic.input -> Tactic.input list
12.16 -(*\------- for Fetch_Tacs ONLY -------/*)
12.17 -
12.18 -(*/------- to Rule_Set from Rtools -------\*)
12.19 - val contains_rule : Rule.rule -> Rule_Set.T -> bool
12.20 -(*\------- to Rule_Set from Rtools -------/*)
12.21 +(*\------- to error-fill-pattern from Rtools -------/*)
12.22
12.23 datatype contthy
12.24 = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id}
12.25 @@ -42,12 +34,6 @@
12.26 val guh2rewtac : Check_Unique.id -> Subst.input -> Tactic.input
12.27 val get_tac_checked : Ctree.ctree -> Pos.pos' -> Tactic.input
12.28 val context_thy : Calc.T -> Tactic.input -> contthy
12.29 - val distinct_Thm : Rule.rule list -> Rule.rule list
12.30 - val eq_Thms : string list -> Rule.rule -> bool
12.31 -(*/------- to ThmC -------\*)
12.32 - val eq_Thm : Rule.rule * Rule.rule -> bool
12.33 - val deriv_of_thm'' : ThmC.T -> string
12.34 -(*\------- to ThmC -------/*)
12.35 val guh2theID : Check_Unique.id -> Thy_Html.theID
12.36
12.37 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.38 @@ -73,16 +59,6 @@
12.39 | SOME cs => TermC.ins_concl cs (TermC.mk_equality (rhs, lhs))
12.40 in trm' end
12.41
12.42 -fun eq_Thm (Rule.Thm (id1, _), Rule.Thm (id2,_)) = id1 = id2
12.43 - | eq_Thm (Rule.Thm (_, _), _) = false
12.44 - | eq_Thm (Rule.Rls_ r1, Rule.Rls_ r2) = Rule_Set.id r1 = Rule_Set.id r2
12.45 - | eq_Thm (Rule.Rls_ _, _) = false
12.46 - | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule.to_string r1 ^ "' '" ^ Rule.to_string r2 ^ "'")
12.47 -fun distinct_Thm r = gen_distinct eq_Thm r
12.48 -
12.49 -fun eq_Thms thmIDs thm = (member op = thmIDs (Rule.thm_id thm))
12.50 - handle ERROR _ => false
12.51 -
12.52 fun thy_containing_thm thmDeriv =
12.53 let
12.54 val isabthys' = map Context.theory_name (Celem.isabthys ());
12.55 @@ -181,16 +157,13 @@
12.56 pass other tacs unchanged.*)
12.57 fun get_tac_checked pt ((p, _) : Pos.pos') = Ctree.get_obj Ctree.g_tac pt p;
12.58
12.59 -(* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)
12.60 -fun deriv_of_thm'' (thmID, _) =
12.61 - thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint
12.62 -
12.63 (* get the formula f at ptp rewritten by the Rewrite_* already applied to f *)
12.64 -fun context_thy (pt, pos as (p,p_)) (tac as Tactic.Rewrite thm'') =
12.65 - let val thm_deriv = deriv_of_thm'' thm''
12.66 +fun context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite thm'') =
12.67 + let
12.68 + val thm_deriv = ThmC.long_id thm''
12.69 in
12.70 (case Applicable.applicable_in pos pt tac of
12.71 - Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
12.72 + Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =>
12.73 ContThm
12.74 {thyID = thy',
12.75 thm = Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv),
12.76 @@ -281,60 +254,6 @@
12.77 | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map thm_of_rule)) rules
12.78 | thms_of_rls (Rule_Set.Rrls _) = []
12.79
12.80 -(* check if a rule is contained in a rule-set (recursivley down in Rls_);
12.81 - this rule can even be a rule-set itself *)
12.82 -fun contains_rule r rls =
12.83 - let
12.84 - fun (*find (_, Rls_ rls) = finds (get_rules rls)
12.85 - | find r12 = equal r12
12.86 - and*) finds [] = false
12.87 - | finds (r1 :: rs) = if Rule.equal (r, r1) then true else finds rs
12.88 - in
12.89 - finds (Rule_Set.get_rules rls)
12.90 - end
12.91 -
12.92 -(* try if a rewrite-rule is applicable to a given formula;
12.93 - in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
12.94 -fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
12.95 - if Auto_Prog.contains_bdv thm
12.96 - then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
12.97 - SOME _ => [Tactic.rule2tac thy subst thm']
12.98 - | NONE => []
12.99 - else (case Rewrite.rewrite_ thy ro erls false thm f of
12.100 - SOME _ => [Tactic.rule2tac thy [] thm']
12.101 - | NONE => [])
12.102 - | try_rew thy _ _ _ f (cal as Rule.Eval c) =
12.103 - (case Eval.adhoc_thm thy c f of
12.104 - SOME _ => [Tactic.rule2tac thy [] cal]
12.105 - | NONE => [])
12.106 - | try_rew thy _ _ _ f (cal as Rule.Cal1 c) =
12.107 - (case Eval.adhoc_thm thy c f of
12.108 - SOME _ => [Tactic.rule2tac thy [] cal]
12.109 - | NONE => [])
12.110 - | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
12.111 - | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
12.112 -and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) =
12.113 - gen_distinct Tactic.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
12.114 - | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) =
12.115 - gen_distinct Tactic.eq_tac (flat (map (try_rew thy ro erls subst f) rules))
12.116 - | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
12.117 - | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
12.118 -
12.119 -(* decide if a tactic is applicable to a given formula;
12.120 - in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
12.121 -fun atomic_appl_tacs thy _ _ f (Tactic.Calculate scrID) =
12.122 - try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd))
12.123 - | atomic_appl_tacs thy ro erls f (Tactic.Rewrite thm'') =
12.124 - try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
12.125 - | atomic_appl_tacs thy ro erls f (Tactic.Rewrite_Inst (subs, thm'')) =
12.126 - try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input thy subs) f (Rule.Thm thm'')
12.127 -
12.128 - | atomic_appl_tacs thy _ _ f (Tactic.Rewrite_Set rls') =
12.129 - filter_appl_rews thy [] f (assoc_rls rls')
12.130 - | atomic_appl_tacs thy _ _ f (Tactic.Rewrite_Set_Inst (subs, rls')) =
12.131 - filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls')
12.132 - | atomic_appl_tacs _ _ _ _ tac =
12.133 - (tracing ("### atomic_appl_tacs: not impl. for tac = '" ^ Tactic.input_to_string tac ^ "'"); []);
12.134
12.135 (* filenames not only for thydata, but also for thy's etc *)
12.136 fun theID2filename theID = Thy_Html.theID2guh theID ^ ".xml"
13.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Apr 27 16:40:11 2020 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Apr 28 15:31:49 2020 +0200
13.3 @@ -479,8 +479,8 @@
13.4 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
13.5 val der = der @
13.6 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'', asm))]
13.7 - val rs = (Rtools.distinct_Thm o (map #1)) der
13.8 - val rs = filter_out (Rtools.eq_Thms
13.9 + val rs = (Rule.distinct o (map #1)) der
13.10 + val rs = filter_out (ThmC.member
13.11 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs
13.12 in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
13.13
13.14 @@ -540,8 +540,8 @@
13.15 val der = Derive.steps_reverse thy eval_rls rules ro NONE t';
13.16 val der = der @
13.17 [(Rule.Thm ("real_mult_div_cancel2", ThmC.numerals_to_Free @{thm real_mult_div_cancel2}), (t'',asm))]
13.18 - val rs = (Rtools.distinct_Thm o (map #1)) der;
13.19 - val rs = filter_out (Rtools.eq_Thms
13.20 + val rs = (Rule.distinct o (map #1)) der;
13.21 + val rs = filter_out (ThmC.member
13.22 ["sym_real_add_zero_left", "sym_real_mult_0", "sym_real_mult_1"]) rs;
13.23 in (t, t'', [rs(*here only _ONE_*)], der) end;
13.24
14.1 --- a/src/Tools/isac/MathEngBasic/state-steps.sml Mon Apr 27 16:40:11 2020 +0200
14.2 +++ b/src/Tools/isac/MathEngBasic/state-steps.sml Tue Apr 28 15:31:49 2020 +0200
14.3 @@ -27,7 +27,6 @@
14.4 struct
14.5 (**)
14.6
14.7 -(*/------- to State_Steps from Generate -------\*)
14.8 (* a single holds alle information required to build a node in the calc-tree;
14.9 a single is assumed to be used efficiently such that the calc-tree
14.10 resulting from applying a single need not be stored separately;
14.11 @@ -53,8 +52,7 @@
14.12 fun result (_, Tactic.Rewrite' (_, _, _, _, _, _,(res, asm)), _) = (res, asm)
14.13 | result (_, Tactic.Rewrite_Set' (_, _, _, _, (res, asm)), _) = (res, asm)
14.14 | result (_, tac_, _) = error ("result: called with" ^ Tactic.string_of tac_)
14.15 -(*\------- to State_Steps from Generate -------/*)
14.16 -(*/------- to State_Steps from Error_Pattern -------\*)
14.17 +
14.18 fun make_single ro erls (t, r as Rule.Thm (id, thm), (t', a)) =
14.19 (Tactic.Rewrite (id, thm),
14.20 Tactic.Rewrite' ("Isac_Knowledge", fst ro, erls, false, ThmC.from_rule r, t, (t', a)),
14.21 @@ -64,7 +62,6 @@
14.22 Tactic.Rewrite_Set' ("Isac_Knowledge", false, rls, t, (t', a)),
14.23 (Pos.e_pos'(*to be updated before generate tacis!!!*), (Istate_Def.Uistate, ContextC.empty)))
14.24 | make_single _ _ (t, r, _) = error ("make_single: not impl. for " ^ Rule.to_string r ^ " at " ^ UnparseC.term t)
14.25 -(*\------- to State_Steps from Error_Pattern -------/*)
14.26
14.27 (* update pos in tacis for embedding by generate *)
14.28 fun insert_pos (_: Pos.pos) [] = []
15.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Mon Apr 27 16:40:11 2020 +0200
15.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Tue Apr 28 15:31:49 2020 +0200
15.3 @@ -113,11 +113,13 @@
15.4 val is_rewset : input -> bool
15.5 val rls_of : input -> Rule_Set.id
15.6 val rule2tac : theory -> (term * term) list -> Rule.rule -> input
15.7 + val applicable : theory -> string -> Rule_Set.T -> term -> input ->input list
15.8 + val for_specify: input -> bool
15.9 +
15.10 val input_from_T : T -> input
15.11 val result : T -> term
15.12 val creates_assms: T -> term list
15.13 val insert_assumptions: T -> Proof.context -> Proof.context
15.14 - val for_specify: input -> bool
15.15 val for_specify': T -> bool
15.16
15.17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15.18 @@ -135,6 +137,8 @@
15.19 struct
15.20 (**)
15.21
15.22 +(** tactics for user at front-end **)
15.23 +
15.24 (* tactics for user at front-end.
15.25 input propagates the construction of the calc-tree;
15.26 there are
15.27 @@ -321,6 +325,52 @@
15.28 | rule2tac _ _ rule =
15.29 error ("rule2tac: called with \"" ^ Rule.to_string rule ^ "\"");
15.30
15.31 +(* try if a rewrite-rule is applicable to a given formula;
15.32 + in case of rule-sets (recursivley) collect all _atomic_ rewrites *)
15.33 +fun try_rew thy ((_, ro) : Rewrite_Ord.rew_ord) erls (subst : subst) f (thm' as Rule.Thm (_, thm)) =
15.34 + if Auto_Prog.contains_bdv thm
15.35 + then case Rewrite.rewrite_inst_ thy ro erls false subst thm f of
15.36 + SOME _ => [rule2tac thy subst thm']
15.37 + | NONE => []
15.38 + else (case Rewrite.rewrite_ thy ro erls false thm f of
15.39 + SOME _ => [rule2tac thy [] thm']
15.40 + | NONE => [])
15.41 + | try_rew thy _ _ _ f (cal as Rule.Eval c) =
15.42 + (case Eval.adhoc_thm thy c f of
15.43 + SOME _ => [rule2tac thy [] cal]
15.44 + | NONE => [])
15.45 + | try_rew thy _ _ _ f (cal as Rule.Cal1 c) =
15.46 + (case Eval.adhoc_thm thy c f of
15.47 + SOME _ => [rule2tac thy [] cal]
15.48 + | NONE => [])
15.49 + | try_rew thy _ _ subst f (Rule.Rls_ rls) = filter_appl_rews thy subst f rls
15.50 + | try_rew _ _ _ _ _ _ = error "try_rew: uncovered case"
15.51 +and filter_appl_rews thy subst f (Rule_Def.Repeat {rew_ord = ro, erls, rules, ...}) =
15.52 + gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
15.53 + | filter_appl_rews thy subst f (Rule_Set.Sequence {rew_ord = ro, erls, rules,...}) =
15.54 + gen_distinct eq_tac (flat (map (try_rew thy ro erls subst f) rules))
15.55 + | filter_appl_rews _ _ _ (Rule_Set.Rrls _) = []
15.56 + | filter_appl_rews _ _ _ _ = error "filter_appl_rews: uncovered case"
15.57 +
15.58 +(* decide if a tactic is applicable to a given formula;
15.59 + in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
15.60 +fun applicable thy _ _ f (Calculate scrID) =
15.61 + try_rew thy Rewrite_Ord.e_rew_ordX Rule_Set.empty [] f (Rule.Eval (assoc_calc' thy scrID |> snd))
15.62 + | applicable thy ro erls f (Rewrite thm'') =
15.63 + try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls [] f (Rule.Thm thm'')
15.64 + | applicable thy ro erls f (Rewrite_Inst (subs, thm'')) =
15.65 + try_rew thy (ro, Rewrite_Ord.assoc_rew_ord ro) erls (Subst.T_from_input thy subs) f (Rule.Thm thm'')
15.66 +
15.67 + | applicable thy _ _ f (Rewrite_Set rls') =
15.68 + filter_appl_rews thy [] f (assoc_rls rls')
15.69 + | applicable thy _ _ f (Rewrite_Set_Inst (subs, rls')) =
15.70 + filter_appl_rews thy (Subst.T_from_input thy subs) f (assoc_rls rls')
15.71 + | applicable _ _ _ _ tac =
15.72 + (tracing ("### applicable: not impl. for tac = '" ^ input_to_string tac ^ "'"); []);
15.73 +
15.74 +
15.75 +(** tactics for internal use **)
15.76 +
15.77 (* tactics for for internal use, compare "input" for user at the front-end.
15.78 tac_ contains results from check in 'fun applicable_in'.
15.79 This is useful for costly results, e.g. from rewriting;
16.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Mon Apr 27 16:40:11 2020 +0200
16.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Tue Apr 28 15:31:49 2020 +0200
16.3 @@ -8,7 +8,13 @@
16.4 signature THEOREM_ISAC =
16.5 sig
16.6 type T = ThmC_Def.T
16.7 - type id = ThmC_Def.id;
16.8 + type id = ThmC_Def.id (* shortest possible *)
16.9 + type long_id (* e.g. "Test.radd_left_commute"*)
16.10 +
16.11 +(*/------- to ThmC from Rtools -------\*)
16.12 + val member: id list -> Rule.rule -> bool
16.13 + val long_id: T -> long_id
16.14 +(*\------- to ThmC from Rtools -------/*)
16.15
16.16 val numerals_to_Free: thm -> thm
16.17 val thm_from_thy: theory -> ThmC_Def.id -> thm
16.18 @@ -16,8 +22,8 @@
16.19 val string_of_thm: thm -> string
16.20 val string_of_thms: thm list -> string
16.21
16.22 - val cut_id: string -> string
16.23 - val id_of_thm: thm -> string
16.24 + val cut_id: string -> id
16.25 + val id_of_thm: thm -> id
16.26 val of_thm: thm -> T
16.27 val from_rule : Rule.rule -> T
16.28
16.29 @@ -42,6 +48,7 @@
16.30
16.31 type T = ThmC_Def.T;
16.32 type id = ThmC_Def.id;
16.33 +type long_id = string;
16.34
16.35 val string_of_thm = ThmC_Def.string_of_thm;
16.36 val string_of_thms = ThmC_Def.string_of_thms;
16.37 @@ -52,6 +59,13 @@
16.38
16.39 fun string_of_thm_in_thy thy thm = UnparseC.term_in_ctxt (ThyC.to_ctxt thy) (Thm.prop_of thm);
16.40
16.41 +(*/------- to ThmC from Rtools -------\*)
16.42 +fun member thmIDs thm = (Library.member op = thmIDs (Rule.thm_id thm))
16.43 + handle ERROR _ => false
16.44 +(* create a derivation-name, eg. ("refl", _) --> "HOL.refl"*)
16.45 +
16.46 +fun long_id (thmID, _) = thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint
16.47 +(*\------- ThmC from Rtools -------/*)
16.48
16.49 (** convert Isabelle's numerals to ISAC's specific format, LEGACY **)
16.50
17.1 --- a/src/Tools/isac/MathEngine/fetch-tactics.sml Mon Apr 27 16:40:11 2020 +0200
17.2 +++ b/src/Tools/isac/MathEngine/fetch-tactics.sml Tue Apr 28 15:31:49 2020 +0200
17.3 @@ -62,13 +62,15 @@
17.4 val (env, (a, v)) = (case get_istate_LI pt (p, p_) of
17.5 Istate.Pstate pst => (Istate.get_subst pst) | _ => error "specific_from_prog 2")
17.6 val ctxt = get_ctxt pt (p, p_)
17.7 - val alltacs = (*we expect at least 1 stac in a script*)
17.8 + val alltacs = (*we expect at least 1 Prog_Tac in a program*)
17.9 map ((LItool.tac_from_prog pt thy) o Program.rep_stacexpr o #1 o
17.10 (LItool.check_leaf "selrul" ctxt srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
17.11 val f =
17.12 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
17.13 | _ => raise ERROR "specific_from_prog 2")
17.14 (*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
17.15 - in ((gen_distinct Tactic.eq_tac) o flat o (map (Rtools.atomic_appl_tacs thy ro erls f))) alltacs end;
17.16 + in
17.17 + ((gen_distinct Tactic.eq_tac) o flat o (map (Tactic.applicable thy ro erls f))) alltacs
17.18 + end;
17.19
17.20 (**)end(**)
17.21 \ No newline at end of file
18.1 --- a/src/Tools/isac/TODO.thy Mon Apr 27 16:40:11 2020 +0200
18.2 +++ b/src/Tools/isac/TODO.thy Tue Apr 28 15:31:49 2020 +0200
18.3 @@ -41,6 +41,12 @@
18.4 rename Specify -> Specify_Etc
18.5 rename SpecifyNEW -> Specify
18.6 \item xxx
18.7 + \item specific_from_prog in..end: replace o by |> (Test_Isac or Test_Some!)
18.8 + \item xxx
18.9 + \item cleanup ThmC in MathEngBasic
18.10 + \item xxx
18.11 + \item xxx
18.12 + \item xxx
18.13 \item xxx
18.14 \item xxx
18.15 \item xxx
19.1 --- a/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML2_Functions.thy Mon Apr 27 16:40:11 2020 +0200
19.2 +++ b/test/Tools/isac/ADDTESTS/course/ml_quickstart/ML2_Functions.thy Tue Apr 28 15:31:49 2020 +0200
19.3 @@ -78,14 +78,14 @@
19.4 \<close>
19.5 section \<open>see src/Pure/library.ML, lists as sets\<close>
19.6 ML \<open>
19.7 -member;
19.8 -member op = [1,2,3,4,5] 3;
19.9 -member op = [1,2,3,4,5] 7;
19.10 +Library.member;
19.11 +Library.member op = [1,2,3,4,5] 3;
19.12 +Library.member op = [1,2,3,4,5] 7;
19.13 \<close>
19.14 ML \<open>
19.15 insert;
19.16 Library.insert;
19.17 -fun insert eq x xs = if member eq xs x then xs else x :: xs;
19.18 +fun insert eq x xs = if Library.member eq xs x then xs else x :: xs;
19.19 \<close>
19.20 ML \<open>
19.21 insert op = 1 [1,2,3];
19.22 @@ -95,7 +95,7 @@
19.23 insert;
19.24 Library.insert;
19.25 fun insert eq x xs =
19.26 - if member eq xs x
19.27 + if Library.member eq xs x
19.28 then (writeln "then"; xs)
19.29 else (writeln "else"; x :: xs);
19.30 insert op = 1 [1,2,3];
20.1 --- a/test/Tools/isac/BaseDefinitions/check-unique.sml Mon Apr 27 16:40:11 2020 +0200
20.2 +++ b/test/Tools/isac/BaseDefinitions/check-unique.sml Tue Apr 28 15:31:49 2020 +0200
20.3 @@ -43,7 +43,7 @@
20.4 collect met_select_guh: Method.T Store.T -> Check_Unique.id list;
20.5
20.6 fun message select store guh =
20.7 - if member op = (select store) guh
20.8 + if Library.member op = (select store) guh
20.9 then error ("Check_Unique failed with \"" ^ guh ^ "\";\n" ^
20.10 "use \"sort_guhs()\" for a list of guhs;\n" ^
20.11 "consider setting \"Check_Unique.on := false\"")
21.1 --- a/test/Tools/isac/BaseDefinitions/contextC.sml Mon Apr 27 16:40:11 2020 +0200
21.2 +++ b/test/Tools/isac/BaseDefinitions/contextC.sml Tue Apr 28 15:31:49 2020 +0200
21.3 @@ -45,7 +45,7 @@
21.4 initialise' thy fmz;
21.5
21.6 val ctxt = thy |> Proof_Context.init_global
21.7 - val ts = (map (TermC.parseNEW' ctxt) fmz) |> map TermC.vars |> flat |> distinct
21.8 + val ts = (map (TermC.parseNEW' ctxt) fmz) |> map TermC.vars |> flat |> Library.distinct op =
21.9 val _ = TermC.raise_type_conflicts ts;
21.10
21.11 "----------- fun get_assumptions, fun insert_assumptions----------------------------------------";
22.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Mon Apr 27 16:40:11 2020 +0200
22.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Tue Apr 28 15:31:49 2020 +0200
22.3 @@ -287,7 +287,7 @@
22.4
22.5 val rlsthmsNOTisac = isacrlsthms (*length = 2*)
22.6 |> filter (fn (deriv, _) =>
22.7 - member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
22.8 + Library.member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
22.9 ;
22.10 val (knowthys', progthys') = ([@{theory Test_Build_Thydata}], [@{theory Test_Build_Thydata}])
22.11 ;
23.1 --- a/test/Tools/isac/Interpret/li-tool.sml Mon Apr 27 16:40:11 2020 +0200
23.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Tue Apr 28 15:31:49 2020 +0200
23.3 @@ -192,8 +192,8 @@
23.4 (*WAS:
23.5 specific_from_prog pt p;
23.6 ...
23.7 -### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
23.8 -### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
23.9 +### Tactic.applicable: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
23.10 +### Tactic.applicable: not impl. for tac = 'Check_elementwise "Assumptions"'
23.11 *)
23.12
23.13 "~~~~~ fun specific_from_prog , args:"; val (pt, (p, p_)) = (pt, p);
23.14 @@ -216,10 +216,10 @@
23.15 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
23.16 | _ => error "");
23.17 (*WN120611 stopped and took version 1 again for fetchApplicableTactics !
23.18 -(distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
23.19 +(Library.distinct op = o flat o (map (Tactic.applicable thy ro erls f))) alltacs
23.20 ...
23.21 -### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
23.22 -### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
23.23 +### Tactic.applicable: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
23.24 +### Tactic.applicable: not impl. for tac = 'Check_elementwise "Assumptions"'
23.25 *)
23.26
23.27 "----------- fun de_esc_underscore -------------------------------";
24.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Apr 27 16:40:11 2020 +0200
24.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Apr 28 15:31:49 2020 +0200
24.3 @@ -362,7 +362,7 @@
24.4 (*if*) ip = ([], Res) (*else*);
24.5 val _ = (*case*) tacis (*of*);
24.6 val SOME _ = (*case*) pIopt (*of*);
24.7 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
24.8 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] p_ (*else*);
24.9
24.10 val ("ok", ([(Rewrite_Set "norm_Poly", _, _)], _, (_, ([1], Res)))) =
24.11 Step_Solve.do_next (pt, ip);
24.12 @@ -413,7 +413,7 @@
24.13 (*if*) ip = ([], Res) (*else*);
24.14 val _ = (*case*) tacis (*of*);
24.15 val SOME _ = (*case*) pIopt (*of*);
24.16 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
24.17 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] p_ (*else*);
24.18
24.19 val ("ok", ([(Check_Postcond ["polynomial", "simplification"], _, _)], _, (_, ([], Res)))) =
24.20 Step_Solve.do_next (pt, ip);
25.1 --- a/test/Tools/isac/Interpret/rewtools.sml Mon Apr 27 16:40:11 2020 +0200
25.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Tue Apr 28 15:31:49 2020 +0200
25.3 @@ -56,7 +56,7 @@
25.4 knowthys ()
25.5 ;
25.6 "~~~~~ fun knowthys , args:"; val () = ();
25.7 - val allthys = filter_out (member Context.eq_thy
25.8 + val allthys = filter_out (Library.member Context.eq_thy
25.9 [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret",
25.10 ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
25.11 (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"));
25.12 @@ -125,7 +125,7 @@
25.13
25.14 val p = ([2,4], Res);
25.15 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
25.16 - member op = [Pbl,Met] p_ = false;
25.17 + Library.member op = [Pbl,Met] p_ = false;
25.18 pos = ([],Res) = false;
25.19 val cs as (ptp as (pt,_),_) = get_calc cI;
25.20 exist_lev_on' pt pos = true;
25.21 @@ -147,7 +147,7 @@
25.22
25.23 val p = ([3,1,1], Frm);
25.24 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
25.25 - member op = [Pbl,Met] p_ = false;
25.26 + Library.member op = [Pbl,Met] p_ = false;
25.27 pos = ([],Res) = false;
25.28 val cs as (ptp as (pt,_),_) = get_calc cI;
25.29 exist_lev_on' pt pos = true;
25.30 @@ -169,7 +169,7 @@
25.31
25.32 val p = ([2,5], Res);
25.33 "~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
25.34 - member op = [Pbl,Met] p_ = false;
25.35 + Library.member op = [Pbl,Met] p_ = false;
25.36 pos = ([],Res) = false;
25.37 val cs as (ptp as (pt,_),_) = get_calc cI;
25.38 exist_lev_on' pt pos = true;
25.39 @@ -349,13 +349,13 @@
25.40 "----------- fun is_contained_in ------------------------";
25.41 "----------- fun is_contained_in ------------------------";
25.42 val r1 = Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus});
25.43 -if Rtools.contains_rule r1 Test_simplify then ()
25.44 -else error "rewtools.sml Rtools.contains_rule Thm";
25.45 +if Rule_Set.contains r1 Test_simplify then ()
25.46 +else error "rewtools.sml Rule_Set.contains Thm";
25.47
25.48 val r1 = Eval ("Groups.plus_class.plus", eval_binop "#add_");
25.49 -if Rtools.contains_rule r1 Test_simplify then ()
25.50 -else error "rewtools.sml Rtools.contains_rule Eval";
25.51 +if Rule_Set.contains r1 Test_simplify then ()
25.52 +else error "rewtools.sml Rule_Set.contains Eval";
25.53
25.54 val r1 = Eval ("Groups.minus_class.minus", eval_binop "#add_");
25.55 -if not (Rtools.contains_rule r1 Test_simplify) then ()
25.56 -else error "rewtools.sml Rtools.contains_rule Eval";
25.57 +if not (Rule_Set.contains r1 Test_simplify) then ()
25.58 +else error "rewtools.sml Rule_Set.contains Eval";
26.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Mon Apr 27 16:40:11 2020 +0200
26.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Tue Apr 28 15:31:49 2020 +0200
26.3 @@ -144,7 +144,7 @@
26.4 *)
26.5 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
26.6 val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
26.7 -(*if*) member op = Solve.specsteps mI = false; (*else*)
26.8 +(*if*) Library.member op = Solve.specsteps mI = false; (*else*)
26.9
26.10 loc_solve_ (mI,m) ptp;
26.11 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
26.12 @@ -225,7 +225,7 @@
26.13 ;
26.14 "~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
26.15 val Applicable.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
26.16 -(*if*) member op = Solve.specsteps mI = true; (*then*)
26.17 +(*if*) Library.member op = Solve.specsteps mI = true; (*then*)
26.18
26.19 (*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
26.20 "~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);
27.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Mon Apr 27 16:40:11 2020 +0200
27.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Tue Apr 28 15:31:49 2020 +0200
27.3 @@ -42,7 +42,7 @@
27.4 here = {Pure, .., Inverse_Z_Transform, Isac, Test_Build_Thydata, Test_Theory:111} *)
27.5 val proglang_parent = @{theory ProgLang}
27.6 val allthys = Theory.ancestors_of @{theory};
27.7 - val allthys = filter_out (member Context.eq_thy (* thys for isac bootstrap *)
27.8 + val allthys = filter_out (Library.member Context.eq_thy (* thys for isac bootstrap *)
27.9 [(*@{theory ProgLang}: required in isacthys' below*) @{theory Interpret}, @{theory MathEngine},
27.10 @{theory BridgeLibisabelle}, knowledge_parent]) allthys (*["Isac_Knowledge", ..., "Pure"]*)
27.11 val isabthys' = (*["Complex_Main", "Taylor", .., "Pure"]*)
27.12 @@ -57,7 +57,7 @@
27.13 thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC.id * thm) list
27.14 val rlsthmsNOTisac = isacrlsthms (*length = 36*)
27.15 |> filter (fn (deriv, _) =>
27.16 - member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
27.17 + Library.member op= (map Context.theory_name isabthys') (ThyC.cut_id deriv))
27.18 : (ThmC.id * thm) list
27.19 ;
27.20 (*\----- cp from Build_Thydata.thy -----------------------------------------------------------/*)
28.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Mon Apr 27 16:40:11 2020 +0200
28.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Tue Apr 28 15:31:49 2020 +0200
28.3 @@ -48,7 +48,7 @@
28.4 ip = ([],Res); "false";
28.5 tacis; " = []";
28.6 pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
28.7 -member op = [Pbl,Met] p_ ; "false";
28.8 +Library.member op = [Pbl,Met] p_ ; "false";
28.9 (*Step_Solve.do_next (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
28.10 THIS MEANS: replace no_meth by [no_meth] in Program.*)
28.11 (*WAS val ("helpless",_) = Step.do_next p ((pt, e_pos'),[]) *)
28.12 @@ -67,7 +67,7 @@
28.13 ip = ([],Res); " = false";
28.14 tacis; " = []";
28.15 pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);
28.16 -member op = [Pbl,Met] p_; " = false";
28.17 +Library.member op = [Pbl,Met] p_; " = false";
28.18 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
28.19 Step_Solve.do_next, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
28.20 This ERROR seems to be introduced together with ctxt, concerns Apply_Method without implicit_take.
29.1 --- a/test/Tools/isac/Knowledge/rateq.sml Mon Apr 27 16:40:11 2020 +0200
29.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Tue Apr 28 15:31:49 2020 +0200
29.3 @@ -100,7 +100,7 @@
29.4 val pIopt = get_pblID (pt,ip); (*= SOME ["rational", "univariate", "equation"]
29.5 1-1 associated to metID ["RatEq", "solve_rat_equation"]*)
29.6 tacis; (*= []*)
29.7 -member op = [Pbl,Met] p_; (*= false*)
29.8 +Library.member op = [Pbl,Met] p_; (*= false*)
29.9 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
29.10 val thy' = get_obj g_domID pt (par_pblobj pt p);
29.11 val (is, sc) = resume_prog thy' (p,p_) pt; (*is: which ctxt?*)
29.12 @@ -134,7 +134,7 @@
29.13 case m of Check_elementwise "Assumptions" => () | _ => (); (*m' = Empty_Tac_ ???!??? *);
29.14 val (p''''', pt''''', m''''') = (p, pt, m);
29.15 "~~~~~ fun applicable_in, args:"; val ((p,p_), pt, (m as Check_elementwise pred)) = (p, pt, m);
29.16 -member op = [Pbl,Met] p_; (* = false*)
29.17 +Library.member op = [Pbl,Met] p_; (* = false*)
29.18 val pp = par_pblobj pt p;
29.19 val thy' = (get_obj g_domID pt pp):theory';
29.20 val thy = ThyC.get_theory thy'
30.1 --- a/test/Tools/isac/Knowledge/rational-old.sml Mon Apr 27 16:40:11 2020 +0200
30.2 +++ b/test/Tools/isac/Knowledge/rational-old.sml Tue Apr 28 15:31:49 2020 +0200
30.3 @@ -688,7 +688,7 @@
30.4 val (t,_,revsets,_) = ini t;
30.5 (*
30.6 val [rs] = revsets;
30.7 - filter_out (eq_Thms ["sym_real_add_zero_left",
30.8 + filter_out (ThmC.Library.member ["sym_real_add_zero_left",
30.9 "sym_real_mult_0",
30.10 "sym_real_mult_1"]) rs;
30.11
31.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml Mon Apr 27 16:40:11 2020 +0200
31.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Tue Apr 28 15:31:49 2020 +0200
31.3 @@ -108,7 +108,7 @@
31.4 ip; (*= ([3, 2], Res)*)
31.5 tacis; (*= []*)
31.6 pIopt; (*= SOME ["sq", "rootX", "univariate", "equation"]*)
31.7 -member op = [Pbl,Met] p_; (*= false*)
31.8 +Library.member op = [Pbl,Met] p_; (*= false*)
31.9 "~~~~~ fun do_next, args:"; (*stopped due to strange exn
31.10 "check_elementwise: no set 1 = 2 + -2 * sqrt x"*)
31.11
31.12 @@ -332,7 +332,7 @@
31.13
31.14 switch_specify_solve p_ (pt, ip);
31.15 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
31.16 - (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
31.17 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
31.18
31.19 LI.do_next (pt, input_pos);
31.20 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
32.1 --- a/test/Tools/isac/MathEngBasic/ctree-navi.sml Mon Apr 27 16:40:11 2020 +0200
32.2 +++ b/test/Tools/isac/MathEngBasic/ctree-navi.sml Tue Apr 28 15:31:49 2020 +0200
32.3 @@ -53,7 +53,7 @@
32.4 val pIopt = get_pblID (pt,ip);
32.5 tacis; (*= []*)
32.6 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
32.7 -member op = [Pbl,Met] p_; (*= true*)
32.8 +Library.member op = [Pbl,Met] p_; (*= true*)
32.9 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt, ip);
32.10 val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
32.11 probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
32.12 @@ -77,8 +77,8 @@
32.13 is_known ctxt sel oris t;
32.14 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);
32.15 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t);
32.16 -val ots = (distinct o flat o (map #5)) (ori:ori list);
32.17 -val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots;
32.18 +val ots = (Library.distinct op = o flat o (map #5)) (ori:ori list);
32.19 +val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots;
32.20 val (d, ts) = split_dts t;
32.21 "~~~~~ fun split_dts, args:"; val (t as d $ arg) = t;
32.22 (*if is_dsc d then () else error "TODO";*)
33.1 --- a/test/Tools/isac/MathEngBasic/mstools.sml Mon Apr 27 16:40:11 2020 +0200
33.2 +++ b/test/Tools/isac/MathEngBasic/mstools.sml Tue Apr 28 15:31:49 2020 +0200
33.3 @@ -53,7 +53,7 @@
33.4 val pIopt = get_pblID (pt,ip);
33.5 tacis; (*= []*)
33.6 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
33.7 -member op = [Pbl,Met] p_; (*= true*)
33.8 +Library.member op = [Pbl,Met] p_; (*= true*)
33.9 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt, ip);
33.10 val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
33.11 probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
33.12 @@ -77,8 +77,8 @@
33.13 is_known ctxt sel oris t;
33.14 "~~~~~ fun is_known, args:"; val (ctxt, sel, ori, t) = (ctxt, sel, oris, t);
33.15 val _ = tracing ("RM is_known: t=" ^ UnparseC.term t);
33.16 -val ots = (distinct o flat o (map #5)) (ori:ori list);
33.17 -val oids = ((map (fst o dest_Free)) o distinct o flat o (map vars)) ots;
33.18 +val ots = (Library.distinct op = o flat o (map #5)) (ori:ori list);
33.19 +val oids = ((map (fst o dest_Free)) o Library.distinct op = o flat o (map vars)) ots;
33.20 val (d, ts) = split_dts t;
33.21 "~~~~~ fun split_dts, args:"; val (t as d $ arg) = t;
33.22 (*if is_dsc d then () else error "TODO";*)
34.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Mon Apr 27 16:40:11 2020 +0200
34.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Tue Apr 28 15:31:49 2020 +0200
34.3 @@ -114,7 +114,7 @@
34.4 val pIopt = get_pblID (pt,ip);
34.5 ip = ([],Res); (*false*)
34.6 ip = p; (*false*)
34.7 -member op = [Pbl,Met] p_; (*false*)
34.8 +Library.member op = [Pbl,Met] p_; (*false*)
34.9 "~~~~~ fun do_next, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
34.10 Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
34.11 val thy' = get_obj g_domID pt (par_pblobj pt p);
34.12 @@ -215,7 +215,7 @@
34.13 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_,p_)): ctree * pos')) =
34.14 (CompleteSubpbl, [], (pt',pos'));
34.15 p = ([], Res) = false;
34.16 -member op = [Pbl,Met] p_ = false;
34.17 +Library.member op = [Pbl,Met] p_ = false;
34.18 val (_, (_, c', ptp')) = Step_Solve.do_next ptp;
34.19 (* in pt': tac = Rewrite ("rnorm_equation_add", "Test.rnorm_equation_add")},
34.20 ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
35.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Mon Apr 27 16:40:11 2020 +0200
35.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Tue Apr 28 15:31:49 2020 +0200
35.3 @@ -26,7 +26,7 @@
35.4 (*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
35.5 switch_specify_solve p_ (pt, ip);
35.6 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
35.7 - (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*then*);
35.8 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] state_pos (*then*);
35.9
35.10 (*rewrite__set_ called with 'Rule_Set.Empty' for 'precond_rootpbl x'*)
35.11 specify_do_next (pt, input_pos);
36.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Mon Apr 27 16:40:11 2020 +0200
36.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Apr 28 15:31:49 2020 +0200
36.3 @@ -33,7 +33,7 @@
36.4 ip = ([],Res) (*= false*);
36.5 tacis (* = []*);
36.6 val SOME pI = pIopt;
36.7 -member op = [Pbl,Met] p_ (*= true*);
36.8 +Library.member op = [Pbl,Met] p_ (*= true*);
36.9 (*nxt_specify_ (pt, ip) ..ERROR in creating the environment..*);
36.10
36.11 val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
37.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Mon Apr 27 16:40:11 2020 +0200
37.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Tue Apr 28 15:31:49 2020 +0200
37.3 @@ -93,7 +93,7 @@
37.4 (*if*) ip = ([], Pos.Res) = false;
37.5 val _ = (*case*) tacis (*of*);
37.6 (*if*) ip = p = false;
37.7 -(*if*) member op = [Pbl, Met] p_ = false;
37.8 +(*if*) Library.member op = [Pbl, Met] p_ = false;
37.9
37.10 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
37.11 Method.id_empty = get_obj g_metID pt (par_pblobj pt p) = false;
37.12 @@ -146,7 +146,7 @@
37.13 (*if*) ip = ([], Pos.Res) (*else*);
37.14 val _ = (*case*) tacis (*of*);
37.15 val SOME _ = (*case*) pIopt (*of*);
37.16 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (**else*);
37.17 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] p_ (**else*);
37.18
37.19 Step_Solve.do_next (pt, ip);
37.20 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
37.21 @@ -230,7 +230,7 @@
37.22 val {cas,ppc,thy,...} = Specify.get_pbt pI
37.23 val dI = Context.theory_name thy (*.take dI from _refined_ pbl.*)
37.24 val dI = Context.theory_name (Stool.common_subthy (ThyC.get_theory dI, rootthy pt));
37.25 - val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> distinct);
37.26 + val ctxt = ContextC.initialise dI (map TermC.vars vals |> flat |> Library.distinct op =);
37.27 (*\\--2 end step into relevant call ----------------------------------------------------------//*)
37.28
37.29 if p = ([2], Res) andalso f2str f = "-1 + x = 0" then
38.1 --- a/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Mon Apr 27 16:40:11 2020 +0200
38.2 +++ b/test/Tools/isac/Minisubpbl/300-init-subpbl-NEXT_STEP.sml Tue Apr 28 15:31:49 2020 +0200
38.3 @@ -23,7 +23,7 @@
38.4 (*if*) ip = ([], Pos.Res) (*else*);
38.5 val _ = (*case*) tacis (*of*);
38.6 val SOME _ = (*case*) pIopt (*of*);
38.7 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*then*);
38.8 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] p_ (*then*);
38.9
38.10 (*+*)val (_, ([_], _, (pt''''', p'''''))) =
38.11 Step.specify_do_next (pt, ip);
39.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Mon Apr 27 16:40:11 2020 +0200
39.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Tue Apr 28 15:31:49 2020 +0200
39.3 @@ -67,7 +67,7 @@
39.4 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p'''', ((pt'''', e_pos'), []))
39.5 val pIopt = get_pblID (pt,ip);
39.6 tacis; (*= []*)
39.7 -member op = [Pbl,Met] p_ (*= false*);
39.8 +Library.member op = [Pbl,Met] p_ (*= false*);
39.9
39.10 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
39.11 val thy' = get_obj g_domID pt (par_pblobj pt p);
40.1 --- a/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Mon Apr 27 16:40:11 2020 +0200
40.2 +++ b/test/Tools/isac/Minisubpbl/470-Check_elementwise-NEXT_STEP.sml Tue Apr 28 15:31:49 2020 +0200
40.3 @@ -48,7 +48,7 @@
40.4 (*if*) ip = ([], Pos.Res) (*else*);
40.5 val _ = (*case*) tacis (*of*);
40.6 (*if*) ip = p (*else*);
40.7 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
40.8 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] p_ (*else*);
40.9
40.10 LI.do_next (pt, ip);
40.11 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = ((pt, ip));
41.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Mon Apr 27 16:40:11 2020 +0200
41.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Tue Apr 28 15:31:49 2020 +0200
41.3 @@ -41,7 +41,7 @@
41.4 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
41.5 (*if*) tacis; (*= []*)
41.6 val SOME pI = pIopt;
41.7 - (*if*) member op = [Pbl,Met] p_; (*= false*)
41.8 + (*if*) Library.member op = [Pbl,Met] p_; (*= false*)
41.9
41.10 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
41.11 (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p); (*false*)
42.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Mon Apr 27 16:40:11 2020 +0200
42.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Tue Apr 28 15:31:49 2020 +0200
42.3 @@ -51,7 +51,7 @@
42.4 "~~~~~ fun do_next, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
42.5 val pIopt = get_pblID (pt,ip); (*= SOME ["sqroot-test", "univariate", ...]*)
42.6 tacis; (*= []*)
42.7 -member op = [Pbl,Met] p_; (*= false*)
42.8 +Library.member op = [Pbl,Met] p_; (*= false*)
42.9 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
42.10 (*if*) Method.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
42.11 val thy' = get_obj g_domID pt (par_pblobj pt p);
43.1 --- a/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Mon Apr 27 16:40:11 2020 +0200
43.2 +++ b/test/Tools/isac/Minisubpbl/600-postcond-NEXT_STEP.sml Tue Apr 28 15:31:49 2020 +0200
43.3 @@ -102,7 +102,7 @@
43.4 (*if*) ip = ([], Pos.Res) (*else*);
43.5 val _ = (*case*) tacis (*of*);
43.6 val SOME _ = (*case*) pIopt (*of*);
43.7 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*else*);
43.8 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] p_ (*else*);
43.9
43.10 Step_Solve.do_next (pt, ip);
43.11 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
44.1 --- a/test/Tools/isac/Minisubpbl/700-interSteps.sml Mon Apr 27 16:40:11 2020 +0200
44.2 +++ b/test/Tools/isac/Minisubpbl/700-interSteps.sml Tue Apr 28 15:31:49 2020 +0200
44.3 @@ -101,7 +101,7 @@
44.4 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
44.5 = (CompleteSubpbl, [], (pt', pos'));
44.6 (*if*) p = ([], Res) (*else*);
44.7 - (*if*) member op = [Pbl,Met] p_ (*else*);
44.8 + (*if*) Library.member op = [Pbl,Met] p_ (*else*);
44.9
44.10 val (_, ([(Rewrite ("radd_commute", _), _, _)], c', ptp')) =
44.11 (*case*) Step_Solve.do_next ptp (*of*);
44.12 @@ -126,13 +126,13 @@
44.13 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
44.14 = (auto, (c @ c'), ptp');
44.15 (*if*) p = ([], Res) (*else*);
44.16 - (*if*) member op = [Pbl,Met] p_ (*else*);
44.17 + (*if*) Library.member op = [Pbl,Met] p_ (*else*);
44.18
44.19 val (_, ([(Rewrite ("add.assoc", _), _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
44.20 "~~~~~ fun complete_solve , args:"; val (auto, c, (ptp as (_, p as (_, p_))))
44.21 = (auto, (c @ c'), ptp');
44.22 (*if*) p = ([], Res) (*else*);
44.23 - (*if*) member op = [Pbl,Met] p_ (*else*);
44.24 + (*if*) Library.member op = [Pbl,Met] p_ (*else*);
44.25 val (_, ([(Calculate "TIMES", _, _)], c', ptp')) = (*case*)Step_Solve.do_next ptp (*of*);
44.26
44.27 show_pt (fst ptp'); (* added [2,1]..[2,3], more to come *)
45.1 --- a/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Mon Apr 27 16:40:11 2020 +0200
45.2 +++ b/test/Tools/isac/Minisubpbl/800-append-on-Frm.sml Tue Apr 28 15:31:49 2020 +0200
45.3 @@ -45,7 +45,7 @@
45.4
45.5 Step.switch_specify_solve p_ (pt, ip);
45.6 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
45.7 - (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
45.8 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] state_pos (*else*);
45.9
45.10 LI.do_next (pt, input_pos);
45.11 "~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);
46.1 --- a/test/Tools/isac/Specify/appl.sml Mon Apr 27 16:40:11 2020 +0200
46.2 +++ b/test/Tools/isac/Specify/appl.sml Tue Apr 28 15:31:49 2020 +0200
46.3 @@ -51,7 +51,7 @@
46.4 val pIopt = get_pblID (pt,ip);
46.5 tacis; (*= []*)
46.6 pIopt; (*= SOME ["sqroot-test", "univariate", ...]*)
46.7 -member op = [Pbl,Met] p_; (*= true*)
46.8 +Library.member op = [Pbl,Met] p_; (*= true*)
46.9 "~~~~~ fun nxt_specify_, args:"; val (ptp as (pt, pos as (p,p_))) = (pt,ip);
46.10 (*============ inhibit exn AK110726 ==============================================
46.11 (* ERROR: Exception Bind raised and subsequent errors (not declared...)*)
47.1 --- a/test/Tools/isac/Specify/step-specify.sml Mon Apr 27 16:40:11 2020 +0200
47.2 +++ b/test/Tools/isac/Specify/step-specify.sml Tue Apr 28 15:31:49 2020 +0200
47.3 @@ -45,7 +45,7 @@
47.4 (*if*) ip = ([], Pos.Res) (*else*);
47.5 val [] = (*case*) tacis (*of*);
47.6 val SOME _ = (*case*) pIopt (*of*);
47.7 - (*if*) member op = [Pos.Pbl, Pos.Met] p_ (*then*);
47.8 + (*if*) Library.member op = [Pos.Pbl, Pos.Met] p_ (*then*);
47.9
47.10 val ("dummy", ([(Specify_Theory "Integrate", _, _)], _, _)) =
47.11 Step.specify_do_next (pt, ip);
48.1 --- a/test/Tools/isac/Test_Isac.thy Mon Apr 27 16:40:11 2020 +0200
48.2 +++ b/test/Tools/isac/Test_Isac.thy Tue Apr 28 15:31:49 2020 +0200
48.3 @@ -610,7 +610,7 @@
48.4 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
48.5 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
48.6 --------------------------------------------------------------------------------
48.7 - WN120409.TODO replace "op mem" (2002) with member (2011) ...
48.8 + WN120409.TODO replace "op mem" (2002) with Library.member (2011) ...
48.9 ... an exercise interesting for beginners !
48.10 --------------------------------------------------------------------------------
48.11 WN120411 scanning html representation of newly generated knowledge:
49.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Apr 27 16:40:11 2020 +0200
49.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Tue Apr 28 15:31:49 2020 +0200
49.3 @@ -610,7 +610,7 @@
49.4 !!add mutual crossreferences to ?fun headline??? where the same has to be done:
49.5 !!OR BETTER: use only 2 functions for adding/removing "'" to/from thy!!
49.6 --------------------------------------------------------------------------------
49.7 - WN120409.TODO replace "op mem" (2002) with member (2011) ...
49.8 + WN120409.TODO replace "op mem" (2002) with Library.member (2011) ...
49.9 ... an exercise interesting for beginners !
49.10 --------------------------------------------------------------------------------
49.11 WN120411 scanning html representation of newly generated knowledge:
50.1 --- a/test/Tools/isac/Test_Some.thy Mon Apr 27 16:40:11 2020 +0200
50.2 +++ b/test/Tools/isac/Test_Some.thy Tue Apr 28 15:31:49 2020 +0200
50.3 @@ -96,6 +96,418 @@
50.4 section \<open>===================================================================================\<close>
50.5 ML \<open>
50.6 \<close> ML \<open>
50.7 +(* Title: test for rewtools.sml
50.8 + authors: Walther Neuper 2000, 2006
50.9 +
50.10 +theory Test_Some imports Isac.Build_Thydata begin
50.11 +ML_file "~~/test/Tools/isac/ADDTESTS/accumulate-val/lucas_interpreter.sml"
50.12 +ML {* KEStore_Elems.set_ref_thy @{theory};
50.13 + fun autoCalculate' cI auto = autoCalculate cI auto |> Future.join *}
50.14 +ML_file "Interpret/rewtools.sml"
50.15 +*)
50.16 +
50.17 +"--------------------------------------------------------";
50.18 +"--------------------------------------------------------";
50.19 +"table of contents --------------------------------------";
50.20 +"--------------------------------------------------------";
50.21 +"----------- fun thy_containing_rls ---------------------";
50.22 +"----------- apply thy_containing_rls -------------------";
50.23 +"----------- fun thy_containing_cal ---------------------";
50.24 +"----------- initContext Thy_ Integration-demo ----------";
50.25 +"----------- initContext..Thy_, fun context_thm ---------";
50.26 +"----------- initContext..Thy_, fun context_rls ---------";
50.27 +"----------- checkContext..Thy_, fun context_thy --------";
50.28 +"----------- checkContext..Thy_, fun context_rls --------";
50.29 +"----------- checkContext..Thy_ on last formula ---------";
50.30 +"----------- fun guh2theID ------------------------------";
50.31 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
50.32 +"--------------------------------------------------------";
50.33 +(*============ inhibit exn WN120321 ==============================================
50.34 +"--------------------------------------------------------";
50.35 +"----------- fun filter_appl_rews -----------------------";
50.36 +============ inhibit exn WN120321 ==============================================*)
50.37 +"----------- fun is_contained_in ------------------------";
50.38 +"--------------------------------------------------------";
50.39 +"--------------------------------------------------------";
50.40 +
50.41 +\<close> ML \<open>
50.42 +"----------- fun thy_containing_rls ---------------------";
50.43 +"----------- fun thy_containing_rls ---------------------";
50.44 +"----------- fun thy_containing_rls ---------------------";
50.45 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
50.46 +if thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
50.47 +else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
50.48 +;
50.49 +"~~~~~ fun thy_containing_rls, args:"; val (thy', rls') = ("Biegelinie", "norm_Poly");
50.50 + val thy = ThyC.get_theory thy'; (*.., EqSystem, Isac.Biegelinie}*)
50.51 +val xxx = AList.lookup op= (KEStore_Elems.get_rlss thy) rls';
50.52 +val SOME (thy'', _) = xxx;
50.53 +val SOME ("Poly", _) = xxx;
50.54 +if thy'' = "Poly" then () else error "--- fun thy_containing_rls: changed";
50.55 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main" *)
50.56 +if partID' thy'' = "IsacKnowledge" then () else error "fun partID': changed"
50.57 +;
50.58 +"~~~~~ fun partID', args:"; val (thy') = (thy');
50.59 +ThyC.get_theory thy' (*.., EqSystem, Isac.Biegelinie}*)
50.60 +;
50.61 +"~~~~~ fun partID, args:"; val (thy) = (ThyC.get_theory thy');
50.62 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"*)
50.63 +knowthys ()
50.64 +;
50.65 +"~~~~~ fun knowthys , args:"; val () = ();
50.66 + val allthys = filter_out (Library.member Context.eq_thy
50.67 + [(*ThyC.get_theory "ProgLang",*) ThyC.get_theory "Interpret",
50.68 + ThyC.get_theory "MathEngine", ThyC.get_theory "BridgeLibisabelle"])
50.69 + (Theory.ancestors_of (ThyC.get_theory "Build_Thydata"));
50.70 +length allthys = 152; (*in Isabelle2015/Isac*)
50.71 +(*ERROR WAS: Theory loader: undefined entry for theory "Isac.Complex_Main"
50.72 +ThyC.get_theory "Complex_Main";*)
50.73 +Thy_Info.get_theory "Complex_Main";;
50.74 +
50.75 +\<close> ML \<open>
50.76 +"----------- apply thy_containing_rls -------------------";
50.77 +"----------- apply thy_containing_rls -------------------";
50.78 +"----------- apply thy_containing_rls -------------------";
50.79 +if thy_containing_rls "Biegelinie" "norm_Poly" = ("IsacKnowledge", "Poly") then ()
50.80 +else error ("thy_containing_rls changed for 'Biegelinie', 'norm_Poly'")
50.81 +;
50.82 +if thy_containing_rls "Biegelinie" "empty" = ("IsacScripts", "Know_Store") then ()
50.83 +else error ("thy_containing_rls changed for 'Biegelinie', 'e_rls'")
50.84 +;
50.85 +if thy_containing_rls "Build_Thydata" "prog_expr" = (*FIXME: handle redifinition in several thys*)
50.86 + ("IsacKnowledge", "Base_Tools") then ()
50.87 +else error ("thy_containing_rls changed for 'Biegelinie', 'prog_expr'")
50.88 +
50.89 +\<close> ML \<open>
50.90 +"----------- fun thy_containing_cal ---------------------";
50.91 +"----------- fun thy_containing_cal ---------------------";
50.92 +"----------- fun thy_containing_cal ---------------------";
50.93 +(* ATTENTION: both, "IsacKnowledge" and "Prog_Expr" are fixed as results for any input*)
50.94 +if thy_containing_cal "Biegelinie" "PLUS" = ("IsacKnowledge", "Base_Tools")
50.95 +then () else error "(wrong) thy_containing_cal 'Biegelinie' 'PLUS' changed"
50.96 +
50.97 +\<close> ML \<open>
50.98 +"----------- initContext Thy_ Integration-demo ----------";
50.99 +"----------- initContext Thy_ Integration-demo ----------";
50.100 +"----------- initContext Thy_ Integration-demo ----------";
50.101 +reset_states ();
50.102 +CalcTree
50.103 +[(["functionTerm (2 * x)","integrateBy x","antiDerivative FF"],
50.104 + ("Integrate",["integrate","function"],
50.105 + ["diff","integration"]))];
50.106 +Iterator 1;
50.107 +moveActiveRoot 1;
50.108 +autoCalculate 1 CompleteCalc;
50.109 +interSteps 1 ([1],Res);
50.110 +interSteps 1 ([1,1],Res);
50.111 +val ((pt,p),_) = get_calc 1; show_pt pt;
50.112 +if existpt' ([1,1,1], Frm) pt then ()
50.113 +else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
50.114 +initContext 1 Thy_ ([1,1,1], Frm);
50.115 +
50.116 +\<close> ML \<open>
50.117 +"----------- initContext..Thy_, fun context_thm ---------";
50.118 +"----------- initContext..Thy_, fun context_thm ---------";
50.119 +"----------- initContext..Thy_, fun context_thm ---------";
50.120 +reset_states (); (*start of calculation, return No.1*)
50.121 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
50.122 + ("Test", ["sqroot-test","univariate","equation","test"],
50.123 + ["Test","squ-equ-test-subpbl1"]))];
50.124 +Iterator 1; moveActiveRoot 1;
50.125 +autoCalculate 1 CompleteCalc;
50.126 +
50.127 +"----- no thy-context at result -----";
50.128 +val p = ([], Res);
50.129 +initContext 1 Thy_ p;
50.130 +val ((pt,_),_) = get_calc 1; show_pt pt; (* 11 lines with subpbl *)
50.131 +
50.132 +interSteps 1 ([2], Res);
50.133 +val ((pt,_),_) = get_calc 1; show_pt pt; (* added [2,1]..[2,6] *)
50.134 +interSteps 1 ([3,1], Res);
50.135 +val ((pt,_),_) = get_calc 1; show_pt pt; (* added [3,1,1] Frm + Res *)
50.136 +
50.137 +val p = ([2,4], Res);
50.138 +"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
50.139 + Library.member op = [Pbl,Met] p_ = false;
50.140 + pos = ([],Res) = false;
50.141 + val cs as (ptp as (pt,_),_) = get_calc cI;
50.142 + exist_lev_on' pt pos = true;
50.143 + val pos' = lev_on' pt pos
50.144 + val tac = get_tac_checked pt pos';
50.145 + is_rewtac tac = true;
50.146 +"~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite (thmID,_))) =
50.147 + ((pt, pos), tac);
50.148 + val Appl (Rewrite' (thy', ord', erls, _, (thmID,thm), f, (res,asm))) = applicable_in pos pt tac
50.149 + val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
50.150 + val thm_deriv = Thm.get_name_hint thm;
50.151 +
50.152 +if Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv)
50.153 + = "thy_isac_Test-thm-radd_left_commute" then ()
50.154 +else error "context_thy mini-subpbl ([2,4], Res) changed";
50.155 +(*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-radd_left_commute*
50.156 +-rw-rw-r-- 1 wneuper wneuper 638 Aug 8 16:04 thy_isac_Test-thm-radd_left_commute.html*)
50.157 +
50.158 +
50.159 +val p = ([3,1,1], Frm);
50.160 +"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
50.161 + Library.member op = [Pbl,Met] p_ = false;
50.162 + pos = ([],Res) = false;
50.163 + val cs as (ptp as (pt,_),_) = get_calc cI;
50.164 + exist_lev_on' pt pos = true;
50.165 + val pos' = lev_on' pt pos
50.166 + val tac = get_tac_checked pt pos';
50.167 + is_rewtac tac = true;
50.168 +"~~~~~ fun context_thy, args:"; val ((pt, pos as (p,p_)), (tac as Rewrite_Inst (subs, (thmID,_))))=
50.169 + ((pt, pos), tac);
50.170 +val Appl (Rewrite_Inst' (thy', ord', erls, _, subst, (thmID,_), f, (res, asm))) =
50.171 + applicable_in pos pt tac
50.172 + val thm = Global_Theory.get_thm (Isac ()(*WN141021 ThyC.get_theory thy' ERROR*)) thmID
50.173 + val thm_deriv = Thm.get_name_hint thm;
50.174 +if Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv) =
50.175 + "thy_isac_Test-thm-risolate_bdv_add" then ()
50.176 +else error "context_thy mini-subpbl ([3,1,1], Frm) changed";
50.177 +(*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-risolate_bdv_add*
50.178 +-rw-rw-r-- 1 wneuper wneuper 646 Aug 8 16:04 thy_isac_Test-thm-risolate_bdv_add.html*)
50.179 +
50.180 +
50.181 +val p = ([2,5], Res);
50.182 +"~~~~~ fun initContext, args:"; val ((cI:calcID), Thy_, (pos as (p,p_):pos')) = (1, Thy_, p);
50.183 + Library.member op = [Pbl,Met] p_ = false;
50.184 + pos = ([],Res) = false;
50.185 + val cs as (ptp as (pt,_),_) = get_calc cI;
50.186 + exist_lev_on' pt pos = true;
50.187 + val pos' = lev_on' pt pos
50.188 + val tac = get_tac_checked pt pos';
50.189 +if is_rewtac tac = false then ()
50.190 +else error "initContext: context_thy .. Calculate PLUS .. TO BE IMPLEMENTED"
50.191 +
50.192 +\<close> ML \<open>
50.193 +"----------- initContext..Thy_, fun context_rls ---------";
50.194 +"----------- initContext..Thy_, fun context_rls ---------";
50.195 +"----------- initContext..Thy_, fun context_rls ---------";
50.196 +(*using pt from above*)
50.197 +val p = ([1], Res);
50.198 +val tac = Rewrite_Set "Test_simplify";
50.199 +initContext 1 Thy_ p;
50.200 +(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
50.201 + --- in initContext..Thy_ ---*)
50.202 +val ContRls {rls,result,...} = context_thy (pt,p) tac;
50.203 +if rls = "thy_isac_Test-rls-Test_simplify"
50.204 + andalso UnparseC.term result = "-1 + x = 0" then ()
50.205 +else error "rewtools.sml initContext..Th_ thy_isac_Test-rls-Test_simplify";
50.206 +
50.207 +val p = ([3,1], Frm);
50.208 +val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");
50.209 +initContext 1 Thy_ p;
50.210 +(*Frm->Res, Rewrite_Set_Inst "isolate_bdv" -1 + x = 0 -> x = 0 + -1 * -1
50.211 + --- in initContext..Thy_ ---*)
50.212 +val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
50.213 +if rls = "thy_isac_Test-rls-isolate_bdv"
50.214 + andalso UnparseC.term result = "x = 0 + -1 * -1" then ()
50.215 +else error "rewtools.sml initContext..Th_ thy_Test-thm-risolate_bdv_add";
50.216 +
50.217 +\<close> ML \<open>
50.218 +"----------- checkContext..Thy_, fun context_thy --------";
50.219 +"----------- checkContext..Thy_, fun context_thy --------";
50.220 +"----------- checkContext..Thy_, fun context_thy --------";
50.221 +(*using pt from above*)
50.222 +val p = ([2,4], Res);
50.223 +val tac = Rewrite ("radd_left_commute", @{thm radd_left_commute});
50.224 +checkContext 1 p "thy_Test-thm-radd_left_commute";
50.225 +(* radd_left_commute: 1 + (-2 + x) = 0 -> -2 + (1 + x) = 0
50.226 + --- in checkContext..Thy_ ---*)
50.227 +val ContThm {thm,result,...} = context_thy (pt,p) tac;
50.228 +\<close> ML \<open>
50.229 +(*+*)val Rewrite ("radd_left_commute", _) = tac
50.230 +\<close> ML \<open>
50.231 +(*+*)thm = ("thy_isac_radd_left_commute-thm-radd_left_commute": ThmC.id);
50.232 +\<close> ML \<open>
50.233 +(*+*)UnparseC.term result = "-2 + (1 + x) = 0";
50.234 +\<close> ML \<open>
50.235 +"~~~~~ fun context_thy , args:"; val ((pt, pos as (p,p_)), (tac as Tactic.Rewrite thm'')) =
50.236 + ((pt,p), tac);
50.237 +\<close> ML \<open>
50.238 + val thm_deriv = ThmC.deriv_of_thm'' thm''
50.239 +\<close> ML \<open>
50.240 +"~~~~~ fun deriv_of_thm'' , args:"; val (thmID, _) = (thm'');
50.241 +\<close> ML \<open>
50.242 +(*+*)(thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint) = "Test.radd_left_commute";
50.243 +\<close> ML \<open>
50.244 + val id = thmID |> Global_Theory.get_thm (ThyC.Isac ()) |> Thm.get_name_hint |> cut_id
50.245 +\<close> ML \<open>
50.246 + (*if*) thmID = id
50.247 +\<close> ML \<open>
50.248 +"~~~~~ from fun deriv_of_thm'' \<longrightarrow>fun context_thy, return:"; val (thm_deriv) = (id);
50.249 +\<close> ML \<open>
50.250 + val Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) =
50.251 + (*case*) Applicable.applicable_in pos pt tac (*of*);
50.252 +\<close> ML \<open>
50.253 +(*+*)(ThmC.cut_id thm_deriv) = "radd_left_commute";
50.254 +\<close> ML \<open>
50.255 +(*+*)(thy_containing_thm thm_deriv) = ("IsacKnowledge", "radd_left_commute");
50.256 +\<close> ML \<open>
50.257 +Thy_Html.thm2guh (thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv)
50.258 +\<close> ML \<open>
50.259 +\<close> ML \<open>
50.260 +\<close> ML \<open>
50.261 +\<close> ML \<open>
50.262 +\<close> ML \<open>
50.263 +\<close> ML \<open>
50.264 +thm = "thy_isac_radd_left_commute-thm-radd_left_commute";
50.265 +\<close> ML \<open>(*\------- end new code -------/*)
50.266 +if thm = "thy_isac_Test-thm-radd_left_commute"
50.267 + andalso UnparseC.term result = "-2 + (1 + x) = 0" then ()
50.268 +else error "rewtools.sml checkContext.._ thy_Test-thm-radd_left_commute";
50.269 +
50.270 +\<close> ML \<open>
50.271 +val p = ([3,1,1], Frm);
50.272 +val tac = Rewrite_Inst (["(''bdv'',x)"],("risolate_bdv_add", @{thm "risolate_bdv_add"}));
50.273 +checkContext 1 p "thy_Test-thm-risolate_bdv_add";
50.274 +(* risolate_bdv_add: -1 + x = 0 -> x = 0 + -1 * -1
50.275 + --- in checkContext..Thy_ ---*)
50.276 +val ContThmInst {thm,result,...} = context_thy (pt,p) tac;
50.277 +if thm = "thy_isac_Test-thm-risolate_bdv_add"
50.278 + andalso UnparseC.term result = "x = 0 + - 1 * -1" then ()
50.279 +else error "rewtools.sml checkContext..T_ thy_Test-thm-risolate_bdv_add";
50.280 +
50.281 +val p = ([2,5], Res);
50.282 +val tac = Calculate "plus";
50.283 +(*checkContext..Thy_ 1 ([2,5], Res);*)
50.284 +(*FIXXXME #######################vvvvv kestoreID !!!!!!!!!!!!!!!!*)
50.285 +checkContext 1 p ;
50.286 +(* Calculate "plus" -2 + (1 + x) = 0 -> -1 + x = 0
50.287 + --- in checkContext..Thy_ ---*)
50.288 +
50.289 +\<close> ML \<open>
50.290 +"----------- checkContext..Thy_, fun context_rls --------";
50.291 +"----------- checkContext..Thy_, fun context_rls --------";
50.292 +"----------- checkContext..Thy_, fun context_rls --------";
50.293 +(*using pt from above*)
50.294 +val p = ([1], Res);
50.295 +val tac = Rewrite_Set "Test_simplify";
50.296 +checkContext 1 p "thy_isac_Test-rls-Test_simplify";
50.297 +(*Res->Res, Rewrite_Set "Test_simplify" x + 1 + -1 * 2 = 0 -> -1 + x = 0
50.298 + --- in checkContext..Thy_ ---*)
50.299 +val ContRls {rls,result,...} = context_thy (pt,p) tac;
50.300 +if rls = "thy_isac_Test-rls-Test_simplify"
50.301 + andalso UnparseC.term result = "-1 + x = 0" then ()
50.302 +else error "rewtools.sml checkContext..Thy_ thy_Test-rls-Test_simplify";
50.303 +
50.304 +val p = ([3,1], Frm);
50.305 +val tac = Rewrite_Set_Inst (["(''bdv'', x)"],"isolate_bdv");
50.306 +checkContext 1 p "thy_Test-rls-isolate_bdv";
50.307 +val ContRlsInst {rls,result,...} = context_thy (pt,p) tac;
50.308 +if rls = "thy_isac_Test-rls-isolate_bdv"
50.309 + andalso UnparseC.term result = "x = 0 + -1 * -1" then ()
50.310 +else error "rewtools.sml checkContext..Thy_ thy_Test-thm-isolate_bdv";
50.311 +
50.312 +\<close> ML \<open>
50.313 +"----------- checkContext..Thy_ on last formula ---------";
50.314 +"----------- checkContext..Thy_ on last formula ---------";
50.315 +"----------- checkContext..Thy_ on last formula ---------";
50.316 +reset_states (); (*start of calculation, return No.1*)
50.317 +CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
50.318 + ("Test", ["sqroot-test","univariate","equation","test"],
50.319 + ["Test","squ-equ-test-subpbl1"]))];
50.320 +Iterator 1; moveActiveRoot 1;
50.321 +
50.322 +autoCalculate 1 CompleteCalcHead;
50.323 +autoCalculate 1 (Steps 1);
50.324 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
50.325 +initContext 1 Thy_ ([1], Frm);
50.326 +checkContext 1 ([1], Frm) "thy_isac_Test-thm-radd_left_commute";
50.327 +
50.328 +autoCalculate 1 (Steps 1);
50.329 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
50.330 +initContext 1 Thy_ ([1], Res);
50.331 +checkContext 1 ([1], Res) "thy_isac_Test-rls-Test_simplify";
50.332 +
50.333 +\<close> ML \<open>
50.334 +"----------- fun guh2theID ------------------------------";
50.335 +"----------- fun guh2theID ------------------------------";
50.336 +"----------- fun guh2theID ------------------------------";
50.337 +val guh = "thy_scri_ListG-thm-zip_Nil";
50.338 +(*default_print_depth 3; 999*)
50.339 +take_fromto 1 4 (Symbol.explode guh);
50.340 +take_fromto 5 9 (Symbol.explode guh);
50.341 +val rest = takerest (9,(Symbol.explode guh));
50.342 +
50.343 +separate "-" rest;
50.344 +space_implode "-" rest;
50.345 +commas rest;
50.346 +
50.347 +val delim = "-";
50.348 +val thyID = takewhile [] (not o (curry op= delim)) rest;
50.349 +val rest' = dropuntil (curry op= delim) rest;
50.350 +val setc = take_fromto 1 5 rest';
50.351 +val xstr = takerest (5, rest');
50.352 +
50.353 +if guh2theID guh = ["IsacScripts", "ListG", "Theorems", "zip_Nil"] then ()
50.354 +else error "rewtools.sml: guh2theID thy_scri_ListG-thm-zip_Nil changed";
50.355 +
50.356 +
50.357 +\<close> ML \<open>
50.358 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
50.359 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
50.360 +"----------- debugging on Tests/solve_linear_as_rootpbl -";
50.361 +"----- initContext -----";
50.362 +reset_states ();
50.363 +CalcTree
50.364 + [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
50.365 + ("Test",
50.366 + ["LINEAR","univariate","equation","test"],
50.367 + ["Test","solve_linear"]))];
50.368 +Iterator 1; moveActiveRoot 1;
50.369 +autoCalculate 1 CompleteCalcHead;
50.370 +
50.371 +autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
50.372 +if is_curr_endof_calc pt ([1],Frm) then ()
50.373 +else error "rewtools.sml is_curr_endof_calc ([1],Frm)";
50.374 +
50.375 +autoCalculate 1 (Steps 1); val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
50.376 +
50.377 +if not (is_curr_endof_calc pt ([1],Frm)) then ()
50.378 +else error "rewtools.sml is_curr_endof_calc ([1],Frm) not";
50.379 +if is_curr_endof_calc pt ([1],Res) then ()
50.380 +else error "rewtools.sml is_curr_endof_calc ([1],Res)";
50.381 +
50.382 +initContext 1 Thy_ ([1],Res);
50.383 +
50.384 +"----- checkContext -----";
50.385 +reset_states ();
50.386 +CalcTree
50.387 + [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
50.388 + ("Test",
50.389 + ["LINEAR","univariate","equation","test"],
50.390 + ["Test","solve_linear"]))];
50.391 +Iterator 1; moveActiveRoot 1;
50.392 +autoCalculate 1 CompleteCalc;
50.393 +interSteps 1 ([1],Res);
50.394 +
50.395 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
50.396 +checkContext 1 ([1],Res) "thy_isac_Test-rls-Test_simplify";
50.397 +
50.398 +interSteps 1 ([2],Res);
50.399 +val (ptp as (pt,p), tacis) = get_calc 1; show_pt pt;
50.400 +
50.401 +checkContext 1 ([2,1],Res) "thy_isac_Test-rls-Test_simplify";
50.402 +checkContext 1 ([2,2],Res) "thy_isac_Test-rls-Test_simplify";
50.403 +
50.404 +\<close> ML \<open>
50.405 +"----------- fun is_contained_in ------------------------";
50.406 +"----------- fun is_contained_in ------------------------";
50.407 +"----------- fun is_contained_in ------------------------";
50.408 +val r1 = Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus});
50.409 +if Rule_Set.contains r1 Test_simplify then ()
50.410 +else error "rewtools.sml Rule_Set.contains Thm";
50.411 +
50.412 +val r1 = Eval ("Groups.plus_class.plus", eval_binop "#add_");
50.413 +if Rule_Set.contains r1 Test_simplify then ()
50.414 +else error "rewtools.sml Rule_Set.contains Eval";
50.415 +
50.416 +val r1 = Eval ("Groups.minus_class.minus", eval_binop "#add_");
50.417 +if not (Rule_Set.contains r1 Test_simplify) then ()
50.418 +else error "rewtools.sml Rule_Set.contains Eval";
50.419 \<close> ML \<open>
50.420 \<close>
50.421