1.1 --- a/TODO.md Fri May 07 13:23:24 2021 +0200
1.2 +++ b/TODO.md Fri May 07 18:12:51 2021 +0200
1.3 @@ -36,6 +36,4 @@
1.4 Left ^^^ in doc-isac (old master-theses, etc: "x^^^#2 + #8" ... # are left, too)
1.5 Left "ASCII art" in case of indicating comments pointing at facts ABOVE.
1.6
1.7 -* WN: simplify const names like "is'_expanded": no need to imitate the escape of mixfix syntax;
1.8 -
1.9 * WN: "fun pr_ord" is not required if used with @{make_string}, @{print}, @{print tracing};
2.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Fri May 07 13:23:24 2021 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Fri May 07 18:12:51 2021 +0200
2.3 @@ -531,12 +531,6 @@
2.4 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
2.5
2.6 fun is_atom (Const ("Float.Float",_) $ _) = true
2.7 - | is_atom (Const ("ComplexI.I'_'_",_)) = true
2.8 - | is_atom (Const ("Groups.times_class.times",_) $ t $ Const ("ComplexI.I'_'_",_)) = is_atom t
2.9 - | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $ Const ("ComplexI.I'_'_",_)) = is_atom t1
2.10 - | is_atom (Const ("Groups.plus_class.plus",_) $ t1 $
2.11 - (Const ("Groups.times_class.times",_) $ t2 $ Const ("ComplexI.I'_'_",_))) =
2.12 - is_atom t1 andalso is_atom t2
2.13 | is_atom (Const _) = true
2.14 | is_atom (Free _) = true
2.15 | is_atom (Var _) = true
3.1 --- a/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy Fri May 07 13:23:24 2021 +0200
3.2 +++ b/src/Tools/isac/Doc/Lucas_Interpreter/Lucas_Interpreter.thy Fri May 07 18:12:51 2021 +0200
3.3 @@ -235,14 +235,14 @@
3.4 \label{fig:fun-pack-diff}
3.5 \end{figure}
3.6
3.7 -The program executes the tactic @{const Rewrite'_Set}\footnote{Isabelle's
3.8 +The program executes the tactic @{const Rewrite_Set}\footnote{Isabelle's
3.9 document preparation system preserves the apostroph from the definition, while
3.10 Isabelle's pretty printer drops it in the presentation of the program as
3.11 above.}
3.12 with different canonical term rewriting systems (called ``rule sets'' in
3.13 \sisac) guided by tacticals. The output (disregarding user interaction) is a
3.14 calculation with steps of simplification, where the steps are created by
3.15 -@{const Rewrite'_Set}.
3.16 +@{const Rewrite_Set}.
3.17
3.18 Chained functions (by \texttt{\small \#>}) %TODO which antiquot?
3.19 are applied curried to @{ML_type term}. The initial part of the chain, from
3.20 @@ -251,7 +251,7 @@
3.21 \texttt{\small ''discard\_minus''} for reducing
3.22 the number of theorems to be used in simplification.
3.23 %
3.24 -The second chain of @{const Rewrite'_Set} is @{const Repeat}ed until no
3.25 +The second chain of @{const Rewrite_Set} is @{const Repeat}ed until no
3.26 further rewrites are possible; this is necessary in case of nested fractions.
3.27
3.28 In cases like the one above, a confluent and terminating term rewrite system,
3.29 @@ -280,10 +280,10 @@
3.30 consts
3.31 Calculate :: "[char list, 'a] => 'a"
3.32 Rewrite :: "[char list, 'a] => 'a"
3.33 - Rewrite'_Inst :: "[(char list * 'a) list, char list, 'a] => 'a"
3.34 - Rewrite'_Set :: "[char list, 'a] => 'a"
3.35 - Rewrite'_Set'_Inst :: "[((char list) * 'a) list, char list, 'a] => 'a"
3.36 - Or'_to'_List :: "bool => 'a list"
3.37 + Rewrite_Inst :: "[(char list * 'a) list, char list, 'a] => 'a"
3.38 + Rewrite_Set :: "[char list, 'a] => 'a"
3.39 + Rewrite_Set_Inst :: "[((char list) * 'a) list, char list, 'a] => 'a"
3.40 + Or_to_List :: "bool => 'a list"
3.41 SubProblem ::
3.42 "[char list * char list list * char list list, arg list] => 'a"
3.43 Substitute :: "[bool list, 'a] => 'a"
3.44 @@ -300,7 +300,7 @@
3.45 respective constants before rewriting (this is due to the user requirement,
3.46 that terms in calculations are close to traditional notation, which excludes
3.47 $\lambda$-terms), for instance modelling bound variables in equation solving.
3.48 -@{const[names_short] Or'_to'_List} is due to a similar requirement: logically
3.49 +@{const[names_short] Or_to_List} is due to a similar requirement: logically
3.50 appropriate for describing solution sets in equation solving are equalities
3.51 connected by $\land,\lor$, but traditional notation uses sets (and these are
3.52 still lists for convenience). @{const[names_short] SubProblem}s not only take
4.1 --- a/src/Tools/isac/Interpret/li-tool.sml Fri May 07 13:23:24 2021 +0200
4.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Fri May 07 18:12:51 2021 +0200
4.3 @@ -72,23 +72,23 @@
4.4 let
4.5 val tid = HOLogic.dest_string thmID
4.6 in (Tactic.Rewrite (tid, ThmC.thm_from_thy thy tid)) end
4.7 - | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite'_Inst", _) $ sub $ thmID $ _) =
4.8 + | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite_Inst", _) $ sub $ thmID $ _) =
4.9 let
4.10 val tid = HOLogic.dest_string thmID
4.11 in (Tactic.Rewrite_Inst (Subst.program_to_input sub, (tid, ThmC.thm_from_thy thy tid))) end
4.12 - | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _) =
4.13 + | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite_Set",_) $ rls $ _) =
4.14 (Tactic.Rewrite_Set (HOLogic.dest_string rls))
4.15 - | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ sub $ rls $ _) =
4.16 + | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite_Set_Inst", _) $ sub $ rls $ _) =
4.17 (Tactic.Rewrite_Set_Inst (Subst.program_to_input sub, HOLogic.dest_string rls))
4.18 | tac_from_prog _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
4.19 (Tactic.Calculate (HOLogic.dest_string op_))
4.20 | tac_from_prog _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (UnparseC.term t))
4.21 | tac_from_prog _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
4.22 (Tactic.Substitute ((Subst.eqs_to_input o TermC.isalist2list) isasub))
4.23 - | tac_from_prog _ thy (Const("Prog_Tac.Check'_elementwise", _) $ _ $
4.24 + | tac_from_prog _ thy (Const("Prog_Tac.Check_elementwise", _) $ _ $
4.25 (Const ("Set.Collect", _) $ Abs (_, _, pred))) =
4.26 (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred))
4.27 - | tac_from_prog _ _ (Const("Prog_Tac.Or'_to'_List", _) $ _ ) = Tactic.Or_to_List
4.28 + | tac_from_prog _ _ (Const("Prog_Tac.Or_to_List", _) $ _ ) = Tactic.Or_to_List
4.29 | tac_from_prog pt _ (ptac as Const ("Prog_Tac.SubProblem", _) $ _ $ _) =
4.30 fst (Sub_Problem.tac_from_prog pt ptac) (*might involve problem refinement etc*)
4.31 | tac_from_prog _ thy t = raise ERROR ("stac2tac_ TODO: no match for " ^ UnparseC.term_in_thy thy t);
4.32 @@ -114,13 +114,13 @@
4.33 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
4.34 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
4.35 (case stac of
4.36 - (Const ("Prog_Tac.Rewrite'_Inst", _) $ _ $ thmID_ $ f_) =>
4.37 + (Const ("Prog_Tac.Rewrite_Inst", _) $ _ $ thmID_ $ f_) =>
4.38 if thmID = HOLogic.dest_string thmID_ then
4.39 if f = f_ then
4.40 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.41 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
4.42 else Not_Associated
4.43 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ rls_ $ f_) =>
4.44 + | (Const ("Prog_Tac.Rewrite_Set_Inst",_) $ _ $ rls_ $ f_) =>
4.45 if Rule_Set.contains (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
4.46 if f = f_ then
4.47 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.48 @@ -135,7 +135,7 @@
4.49 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.50 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
4.51 else Not_Associated
4.52 - | (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_) =>
4.53 + | (Const ("Prog_Tac.Rewrite_Set", _) $ rls_ $ f_) =>
4.54 if Rule_Set.contains (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
4.55 if f = f_ then
4.56 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.57 @@ -143,14 +143,14 @@
4.58 else Not_Associated
4.59 | _ => Not_Associated)
4.60 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
4.61 - (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_)) =
4.62 + (Const ("Prog_Tac.Rewrite_Set_Inst", _) $ _ $ rls_ $ f_)) =
4.63 if Rule_Set.id rls = HOLogic.dest_string rls_ then
4.64 if f = f_ then
4.65 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.66 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
4.67 else Not_Associated
4.68 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
4.69 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) =
4.70 + (Const ("Prog_Tac.Rewrite_Set", _) $ rls_ $ f_)) =
4.71 if Rule_Set.id rls = HOLogic.dest_string rls_ then
4.72 if f = f_ then
4.73 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
4.74 @@ -162,21 +162,21 @@
4.75 if op_ = HOLogic.dest_string op__ then
4.76 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
4.77 else Not_Associated
4.78 - | (Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $ _ $ rls_ $ f_) =>
4.79 + | (Const ("Prog_Tac.Rewrite_Set_Inst", _) $ _ $ rls_ $ f_) =>
4.80 if Rule_Set.contains (Rule.Eval (assoc_calc' (ThyC.get_theory "Isac_Knowledge")
4.81 op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
4.82 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
4.83 else Not_Associated
4.84 - | (Const ("Prog_Tac.Rewrite'_Set",_) $ rls_ $ f_) =>
4.85 + | (Const ("Prog_Tac.Rewrite_Set",_) $ rls_ $ f_) =>
4.86 if Rule_Set.contains (Rule.Eval (assoc_calc' ( ThyC.get_theory "Isac_Knowledge")
4.87 op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
4.88 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
4.89 else Not_Associated
4.90 | _ => Not_Associated)
4.91 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
4.92 - (Const ("Prog_Tac.Check'_elementwise",_) $ consts' $ _)) =
4.93 + (Const ("Prog_Tac.Check_elementwise",_) $ consts' $ _)) =
4.94 if consts = consts' then Associated (m, consts_chkd, ctxt) else Not_Associated
4.95 - | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or'_to'_List", _) $ _)) =
4.96 + | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or_to_List", _) $ _)) =
4.97 Associated (m, list, ctxt)
4.98 | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) =
4.99 Associated (m, term, ctxt)
5.1 --- a/src/Tools/isac/Knowledge/AlgEin.thy Fri May 07 13:23:24 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/AlgEin.thy Fri May 07 18:12:51 2021 +0200
5.3 @@ -112,6 +112,7 @@
5.4 [Rule.Eval ("Prog_Expr.boollist2sum", Prog_Expr.eval_boollist2sum "")],
5.5 prls = Rule_Set.empty, crls =Rule_Set.empty , errpats = [], nrls = norm_Rational},
5.6 @{thm symbolisch_rechnen.simps})]
5.7 +\<close> ML \<open>
5.8 +\<close> ML \<open>
5.9 \<close>
5.10 -
5.11 end
6.1 --- a/src/Tools/isac/Knowledge/Base_Tools.thy Fri May 07 13:23:24 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Base_Tools.thy Fri May 07 18:12:51 2021 +0200
6.3 @@ -25,11 +25,11 @@
6.4 subsection \<open>setup for ML-functions\<close>
6.5 text \<open>required by "eval_binop" below\<close>
6.6 setup \<open>KEStore_Elems.add_calcs
6.7 - [ ("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_")),
6.8 - ("some_occur_in", ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_")),
6.9 - ("is_atom", ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_")),
6.10 - ("is_even", ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_")),
6.11 - ("is_const", ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")),
6.12 + [ ("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "#occurs_in_")),
6.13 + ("some_occur_in", ("Prog_Expr.some_occur_in", Prog_Expr.eval_some_occur_in "#some_occur_in_")),
6.14 + ("is_atom", ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_")),
6.15 + ("is_even", ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_")),
6.16 + ("is_const", ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")),
6.17 ("le", ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")),
6.18 ("leq", ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_")),
6.19 ("ident", ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_")),
6.20 @@ -88,8 +88,8 @@
6.21 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
6.22
6.23 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
6.24 - Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
6.25 - Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
6.26 + Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
6.27 + Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
6.28 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
6.29 \<close>
6.30
6.31 @@ -114,8 +114,8 @@
6.32 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
6.33
6.34 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
6.35 - Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
6.36 - Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
6.37 + Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
6.38 + Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
6.39 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")];
6.40 \<close>
6.41
6.42 @@ -151,4 +151,8 @@
6.43 setup \<open>KEStore_Elems.add_rlss
6.44 [("prog_expr", (Context.theory_name @{theory}, Auto_Prog.prep_rls @{theory} prog_expr))]\<close>
6.45
6.46 +ML \<open>
6.47 +\<close> ML \<open>
6.48 +\<close> ML \<open>
6.49 +\<close>
6.50 end
7.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Fri May 07 13:23:24 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Fri May 07 18:12:51 2021 +0200
7.3 @@ -12,19 +12,19 @@
7.4 qq :: "real => real" (* Streckenlast *)
7.5 Q :: "real => real" (* Querkraft *)
7.6 Q' :: "real => real" (* Ableitung der Querkraft *)
7.7 - M'_b :: "real => real" ("M'_b") (* Biegemoment *)
7.8 -(*M'_b' :: "real => real" ("M'_b' ") ( * Ableitung des Biegemoments
7.9 - Isabelle2020: new handling of quotes in mixfix in, so the parser cannot distinguish M'_b M'_b'
7.10 + M_b :: "real => real" ("M'_b") (* Biegemoment *)
7.11 +(*M_b' :: "real => real" ("M_b' ") ( * Ableitung des Biegemoments
7.12 + Isabelle2020: new handling of quotes in mixfix in, so the parser cannot distinguish M_b M_b'
7.13
7.14 Outcommenting causes error at Neigung_Moment: "y'' x = -M_b x/ EI" below:
7.15 Ambiguous input\<^here> produces 2 parse trees:
7.16 ("\<^const>HOL.Trueprop"
7.17 ("\<^const>HOL.eq" ("_applC" ("_position" y'') ("_position" x))
7.18 - ("\<^const>Fields.inverse_class.inverse_divide" ("\<^const>Groups.uminus_class.uminus" ("_applC" ("\<^const>Biegelinie_Test.M'_b") ("_position" x)))
7.19 + ("\<^const>Fields.inverse_class.inverse_divide" ("\<^const>Groups.uminus_class.uminus" ("_applC" ("\<^const>Biegelinie_Test.M_b") ("_position" x)))
7.20 ("_position" EI))))
7.21 ("\<^const>HOL.Trueprop"
7.22 ("\<^const>HOL.eq" ("_applC" ("_position" y'') ("_position" x))
7.23 - ("\<^const>Fields.inverse_class.inverse_divide" ("\<^const>Groups.uminus_class.uminus" ("_applC" ("\<^const>Biegelinie_Test.M'_b'") ("_position" x)))
7.24 + ("\<^const>Fields.inverse_class.inverse_divide" ("\<^const>Groups.uminus_class.uminus" ("_applC" ("\<^const>Biegelinie_Test.M_b'") ("_position" x)))
7.25 ("_position" EI))))
7.26 Ambiguous input -------------------------------------------------------------------------------------------------------^^^^^^
7.27 2 terms are type correct:
7.28 @@ -71,7 +71,7 @@
7.29 Moment_Neigung: "(M_b x) = -EI * y'' x" and
7.30
7.31 (*according to rls 'simplify_Integral': .. = 1/a * .. instead .. = ../ a*)
7.32 - make_fun_explicit: "Not (a =!= 0) ==> (a * (f x) = b) = (f x = 1/a * b)"
7.33 + make_fun_explicit: "~ (a =!= 0) ==> (a * (f x) = bb) = (f x = 1/a * bb)"
7.34
7.35
7.36 section \<open>Acknowledgements shown in browsers of Isac_Knowledge\<close>
7.37 @@ -160,7 +160,7 @@
7.38 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
7.39 Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs"eval_lhs_"),
7.40 Rule.Eval("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
7.41 - Rule.Eval("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in")
7.42 + Rule.Eval("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in")
7.43 ],
7.44 scr = Rule.Empty_Prog};
7.45
7.46 @@ -179,7 +179,7 @@
7.47 Rule.Eval("Groups.plus_class.plus", (**)eval_binop "#add_"),
7.48 Rule.Thm ("NTH_NIL", ThmC.numerals_to_Free @{thm NTH_NIL}),
7.49 Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
7.50 - Rule.Eval("Prog_Expr.filter'_sameFunId", Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"),
7.51 + Rule.Eval("Prog_Expr.filter_sameFunId", Prog_Expr.eval_filter_sameFunId "Prog_Expr.filter_sameFunId"),
7.52 (*WN070514 just for smltest/../biegelinie.sml ...*)
7.53 Rule.Eval("Prog_Expr.sameFunId", Prog_Expr.eval_sameFunId "Prog_Expr.sameFunId"),
7.54 Rule.Thm ("filter_Cons", ThmC.numerals_to_Free @{thm filter_Cons}),
7.55 @@ -393,7 +393,7 @@
7.56 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [],
7.57 srls = Rule_Set.append_rules "srls_in_EquationfromFunc" Rule_Set.empty
7.58 [Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
7.59 - Rule.Eval("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in")],
7.60 + Rule.Eval("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in")],
7.61 prls=Rule_Set.empty, crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
7.62 (*(M_b x = c_2 + c * x + -1 * q_0 / 2 * x \<up> 2) (M_b L = 0) -->
7.63 0 = c_2 + c * L + -1 * q_0 / 2 * L \<up> 2*)
7.64 @@ -401,7 +401,7 @@
7.65 \<close>
7.66 ML \<open>
7.67 \<close> ML \<open>
7.68 +\<close> ML \<open>
7.69 \<close>
7.70 -
7.71 end
7.72
8.1 --- a/src/Tools/isac/Knowledge/Calculus.thy Fri May 07 13:23:24 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Calculus.thy Fri May 07 18:12:51 2021 +0200
8.3 @@ -1,3 +1,7 @@
8.4 theory Calculus imports Base_Tools begin
8.5
8.6 -end
8.7 \ No newline at end of file
8.8 +ML \<open>
8.9 +\<close> ML \<open>
8.10 +\<close> ML \<open>
8.11 +\<close>
8.12 +end
9.1 --- a/src/Tools/isac/Knowledge/Diff.thy Fri May 07 13:23:24 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Fri May 07 18:12:51 2021 +0200
9.3 @@ -112,7 +112,7 @@
9.4 preconds = [],
9.5 rew_ord = ("termlessI",termlessI),
9.6 erls = Rule_Set.append_rules "erls_diff_conv" Rule_Set.empty
9.7 - [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
9.8 + [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
9.9 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
9.10 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
9.11 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
9.12 @@ -190,9 +190,9 @@
9.13 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
9.14
9.15 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
9.16 - Rule.Eval ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),
9.17 - Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
9.18 - Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")
9.19 + Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
9.20 + Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
9.21 + Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")
9.22 ];
9.23
9.24 (*.rules for differentiation, _no_ simplification.*)
9.25 @@ -432,6 +432,8 @@
9.26 \<close>
9.27 setup \<open>KEStore_Elems.add_cas
9.28 [((Thm.term_of o the o (TermC.parse thy)) "Differentiate",
9.29 - (("Isac_Knowledge", ["named", "derivative_of", "function"], ["no_met"]), argl2dtss))]\<close>
9.30 -
9.31 + (("Isac_Knowledge", ["named", "derivative_of", "function"], ["no_met"]), argl2dtss))]
9.32 +\<close> ML \<open>
9.33 +\<close> ML \<open>
9.34 +\<close>
9.35 end
10.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Fri May 07 13:23:24 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Fri May 07 18:12:51 2021 +0200
10.3 @@ -53,8 +53,8 @@
10.4 Rule.Eval ("Orderings.ord_class.less_eq", Prog_Expr.eval_equ "#less_equal_"),
10.5
10.6 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
10.7 - Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
10.8 - Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
10.9 + Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
10.10 + Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
10.11 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "")],
10.12 scr = Rule.Empty_Prog
10.13 });
10.14 @@ -199,6 +199,9 @@
10.15 [Rule.Thm ("filterVar_Const", ThmC.numerals_to_Free @{thm filterVar_Const}),
10.16 Rule.Thm ("filterVar_Nil", ThmC.numerals_to_Free @{thm filterVar_Nil})];
10.17 \<close>
10.18 -setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>
10.19 -
10.20 +setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]
10.21 +\<close> ML \<open>
10.22 +\<close> ML \<open>
10.23 +\<close> ML \<open>
10.24 +\<close>
10.25 end
11.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy Fri May 07 13:23:24 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy Fri May 07 18:12:51 2021 +0200
11.3 @@ -42,6 +42,8 @@
11.4 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
11.5 crls = tval_rls, errpats = [], nrls = Test_simplify},
11.6 @{thm diophant_equation.simps})]
11.7 +\<close> ML \<open>
11.8 +\<close> ML \<open>
11.9 \<close>
11.10
11.11 -end
11.12 \ No newline at end of file
11.13 +end
12.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Fri May 07 13:23:24 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri May 07 18:12:51 2021 +0200
12.3 @@ -8,7 +8,7 @@
12.4
12.5 consts
12.6
12.7 - occur'_exactly'_in ::
12.8 + occur_exactly_in ::
12.9 "[real list, real list, 'a] => bool" ("_ from _ occur'_exactly'_in _")
12.10
12.11 (*descriptions in the related problems*)
12.12 @@ -66,10 +66,10 @@
12.13 (subtract op = vs all)))
12.14 end;
12.15
12.16 -(*("occur_exactly_in", ("EqSystem.occur'_exactly'_in",
12.17 +(*("occur_exactly_in", ("EqSystem.occur_exactly_in",
12.18 eval_occur_exactly_in "#eval_occur_exactly_in_"))*)
12.19 -fun eval_occur_exactly_in _ "EqSystem.occur'_exactly'_in"
12.20 - (p as (Const ("EqSystem.occur'_exactly'_in",_)
12.21 +fun eval_occur_exactly_in _ "EqSystem.occur_exactly_in"
12.22 + (p as (Const ("EqSystem.occur_exactly_in",_)
12.23 $ vs $ all $ t)) _ =
12.24 if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t
12.25 then SOME ((UnparseC.term p) ^ " = True",
12.26 @@ -80,7 +80,7 @@
12.27 \<close>
12.28 setup \<open>KEStore_Elems.add_calcs
12.29 [("occur_exactly_in",
12.30 - ("EqSystem.occur'_exactly'_in",
12.31 + ("EqSystem.occur_exactly_in",
12.32 eval_occur_exactly_in "#eval_occur_exactly_in_"))]\<close>
12.33 ML \<open>
12.34 (** rewrite order 'ord_simplify_System' **)
12.35 @@ -292,7 +292,7 @@
12.36 Rule_Def.Repeat {id="isolate_bdvs", preconds = [],
12.37 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
12.38 erls = Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
12.39 - [(Rule.Eval ("EqSystem.occur'_exactly'_in",
12.40 + [(Rule.Eval ("EqSystem.occur_exactly_in",
12.41 eval_occur_exactly_in
12.42 "#eval_occur_exactly_in_"))
12.43 ],
12.44 @@ -309,10 +309,10 @@
12.45 rew_ord = ("e_rew_ord", Rewrite_Ord.e_rew_ord),
12.46 erls = Rule_Set.append_rules
12.47 "erls_isolate_bdvs_4x4" Rule_Set.empty
12.48 - [Rule.Eval ("EqSystem.occur'_exactly'_in",
12.49 + [Rule.Eval ("EqSystem.occur_exactly_in",
12.50 eval_occur_exactly_in "#eval_occur_exactly_in_"),
12.51 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
12.52 - Rule.Eval ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
12.53 + Rule.Eval ("Prog_Expr.some_occur_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
12.54 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
12.55 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
12.56 ],
12.57 @@ -357,7 +357,7 @@
12.58 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
12.59 Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
12.60 Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
12.61 - Rule.Eval ("EqSystem.occur'_exactly'_in",
12.62 + Rule.Eval ("EqSystem.occur_exactly_in",
12.63 eval_occur_exactly_in
12.64 "#eval_occur_exactly_in_")
12.65 ],
12.66 @@ -386,7 +386,7 @@
12.67 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
12.68 Rule.Thm ("tl_Cons",ThmC.numerals_to_Free @{thm tl_Cons}),
12.69 Rule.Thm ("tl_Nil",ThmC.numerals_to_Free @{thm tl_Nil}),
12.70 - Rule.Eval ("EqSystem.occur'_exactly'_in",
12.71 + Rule.Eval ("EqSystem.occur_exactly_in",
12.72 eval_occur_exactly_in
12.73 "#eval_occur_exactly_in_")
12.74 ],
12.75 @@ -481,7 +481,7 @@
12.76 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
12.77 ("#Find" ,["solution ss'''"])],
12.78 Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
12.79 - [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
12.80 + [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "")],
12.81 SOME "solveSystem e_s v_s",
12.82 [["EqSystem", "top_down_substitution", "4x4"]])),
12.83 (Problem.prep_input thy "pbl_equsys_lin_4x4_norm" [] Problem.id_empty
12.84 @@ -660,10 +660,12 @@
12.85 {rew_ord'="ord_simplify_System", rls' = Rule_Set.Empty, calc = [],
12.86 srls = Rule_Set.append_rules "srls_top_down_4x4" srls [],
12.87 prls = Rule_Set.append_rules "prls_tri_4x4_lin_sys" prls_triangular
12.88 - [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
12.89 + [Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "")],
12.90 crls = Rule_Set.Empty, errpats = [], nrls = Rule_Set.Empty},
12.91 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
12.92 @{thm solve_system4.simps})]
12.93 +\<close> ML \<open>
12.94 +\<close> ML \<open>
12.95 +\<close> ML \<open>
12.96 \<close>
12.97 -
12.98 -end
12.99 \ No newline at end of file
12.100 +end
13.1 --- a/src/Tools/isac/Knowledge/Equation.thy Fri May 07 13:23:24 2021 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Equation.thy Fri May 07 18:12:51 2021 +0200
13.3 @@ -86,6 +86,7 @@
13.4 {rew_ord'="tless_true", rls'=Rule_Set.Empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, crls = Atools_erls,
13.5 errpats = [], nrls = Rule_Set.empty},
13.6 @{thm refl})]
13.7 +\<close> ML \<open>
13.8 +\<close> ML \<open>
13.9 \<close>
13.10 -
13.11 end
13.12 \ No newline at end of file
14.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Fri May 07 13:23:24 2021 +0200
14.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Fri May 07 18:12:51 2021 +0200
14.3 @@ -236,7 +236,7 @@
14.4
14.5 yields p is_prime \<and> n1 < p \<and> \<not> p dvd n2 \<and> (* smallest with these properties... *)
14.6 (\<forall> p'. (p' is_prime \<and> n1 < p' \<and> \<not> p' dvd n2) \<longrightarrow> p \<le> p') *)
14.7 -function next_prime_not_dvd :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "next'_prime'_not'_dvd" 70) where
14.8 +function next_prime_not_dvd :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "next_prime_not_dvd" 70) where
14.9 "n1 next_prime_not_dvd n2 =
14.10 (let
14.11 ps = primes_upto (n1 + 1);
14.12 @@ -462,7 +462,7 @@
14.13 assume m > 0
14.14 yields up = [p1 mod m, p2 mod m, ..., pk mod m]*)
14.15 definition mod' :: "nat \<Rightarrow> int \<Rightarrow> int" where "mod' m i = i mod (int m)"
14.16 -definition mod_up :: "unipoly \<Rightarrow> nat \<Rightarrow> unipoly" (infixl "mod'_up" 70) where
14.17 +definition mod_up :: "unipoly \<Rightarrow> nat \<Rightarrow> unipoly" (infixl "mod_up" 70) where
14.18 "p mod_up m = map (mod' m) p"
14.19
14.20 value "[5, 4, 7, 8, 1] mod_up 5 = [0, 4, 2, 3, 1]"
15.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Fri May 07 13:23:24 2021 +0200
15.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Fri May 07 18:12:51 2021 +0200
15.3 @@ -159,6 +159,7 @@
15.4 (("InsSort", ["insertion", "SORT", "Programming"], ["no_met"]), argl2dtss)
15.5 )
15.6 ]
15.7 +\<close> ML \<open>
15.8 +\<close> ML \<open>
15.9 \<close>
15.10 -
15.11 end
16.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Fri May 07 13:23:24 2021 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Fri May 07 18:12:51 2021 +0200
16.3 @@ -9,8 +9,8 @@
16.4 consts
16.5
16.6 Integral :: "[real, real]=> real" ("Integral _ D _" 91)
16.7 -(*new'_c :: "real => real" ("new'_c _" 66)*)
16.8 - is'_f'_x :: "real => bool" ("_ is'_f'_x" 10)
16.9 +(*new_c :: "real => real" ("new_c _" 66)*)
16.10 + is_f_x :: "real => bool" ("_ is'_f'_x" 10)
16.11
16.12 (*descriptions in the related problems*)
16.13 integrateBy :: "real => una"
16.14 @@ -72,18 +72,18 @@
16.15 end;
16.16
16.17 (*WN080222
16.18 -(*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*)
16.19 -fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =
16.20 +(*("new_c", ("Integrate.new_c", eval_new_c "#new_c_"))*)
16.21 +fun eval_new_c _ _ (p as (Const ("Integrate.new_c",_) $ t)) _ =
16.22 SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (new_c p),
16.23 Trueprop $ (mk_equality (p, new_c p)))
16.24 | eval_new_c _ _ _ _ = NONE;
16.25 *)
16.26
16.27 (*WN080222:*)
16.28 -(*("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "#add_new_c_"))
16.29 +(*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_"))
16.30 add a new c to a term or a fun-equation;
16.31 this is _not in_ the term, because only applied to _whole_ term*)
16.32 -fun eval_add_new_c (_:string) "Integrate.add'_new'_c" p (_:theory) =
16.33 +fun eval_add_new_c (_:string) "Integrate.add_new_c" p (_:theory) =
16.34 let val p' = case p of
16.35 Const ("HOL.eq", T) $ lh $ rh =>
16.36 Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh)
16.37 @@ -94,8 +94,8 @@
16.38 | eval_add_new_c _ _ _ _ = NONE;
16.39
16.40
16.41 -(*("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_x_"))*)
16.42 -fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
16.43 +(*("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_x_"))*)
16.44 +fun eval_is_f_x _ _(p as (Const ("Integrate.is_f_x", _)
16.45 $ arg)) _ =
16.46 if TermC.is_f_x arg
16.47 then SOME ((UnparseC.term p) ^ " = True",
16.48 @@ -105,8 +105,8 @@
16.49 | eval_is_f_x _ _ _ _ = NONE;
16.50 \<close>
16.51 setup \<open>KEStore_Elems.add_calcs
16.52 - [("add_new_c", ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_")),
16.53 - ("is_f_x", ("Integrate.is'_f'_x", eval_is_f_x "is_f_idextifier_"))]\<close>
16.54 + [("add_new_c", ("Integrate.add_new_c", eval_add_new_c "add_new_c_")),
16.55 + ("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_idextifier_"))]\<close>
16.56 ML \<open>
16.57 (** rulesets **)
16.58
16.59 @@ -120,7 +120,7 @@
16.60 erls = Rule_Set.Empty,
16.61 srls = Rule_Set.Empty, calc = [], errpatts = [],
16.62 rules = [(*for rewriting conditions in Thm's*)
16.63 - Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
16.64 + Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in "#occurs_in_"),
16.65 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
16.66 Rule.Thm ("not_false",@{thm not_false})
16.67 ],
16.68 @@ -146,7 +146,7 @@
16.69 erls = Rule_Set.Empty,
16.70 srls = Rule_Set.Empty, calc = [], errpatts = [],
16.71 rules = [Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches""),
16.72 - Rule.Eval ("Integrate.is'_f'_x",
16.73 + Rule.Eval ("Integrate.is_f_x",
16.74 eval_is_f_x "is_f_x_"),
16.75 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
16.76 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})
16.77 @@ -154,7 +154,7 @@
16.78 scr = Rule.Empty_Prog},
16.79 srls = Rule_Set.Empty, calc = [], errpatts = [],
16.80 rules = [ (*Rule.Thm ("call_for_new_c", ThmC.numerals_to_Free @{thm call_for_new_c}),*)
16.81 - Rule.Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
16.82 + Rule.Cal1 ("Integrate.add_new_c", eval_add_new_c "new_c_")
16.83 ],
16.84 scr = Rule.Empty_Prog};
16.85 \<close>
16.86 @@ -173,7 +173,7 @@
16.87 rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
16.88 erls = (*FIXME.WN051028 Rule_Set.empty,*)
16.89 Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
16.90 - [Rule.Eval ("Poly.is'_polyexp",
16.91 + [Rule.Eval ("Poly.is_polyexp",
16.92 eval_is_polyexp "")],
16.93 srls = Rule_Set.Empty, calc = [], errpatts = [],
16.94 rules = [Rule.Thm ("rat_mult", ThmC.numerals_to_Free @{thm rat_mult}),
16.95 @@ -384,6 +384,8 @@
16.96 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
16.97 crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
16.98 @{thm intergrate_named.simps})]
16.99 +\<close> ML \<open>
16.100 +\<close> ML \<open>
16.101 \<close>
16.102
16.103 end
16.104 \ No newline at end of file
17.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri May 07 13:23:24 2021 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Fri May 07 18:12:51 2021 +0200
17.3 @@ -102,14 +102,14 @@
17.4 let
17.5 X = Take X_eq;
17.6 X' = Rewrite ''ruleZY'' X;
17.7 - X'_z = lhs X';
17.8 - zzz = argument_in X'_z;
17.9 + X_z = lhs X';
17.10 + zzz = argument_in X_z;
17.11 funterm = rhs X';
17.12 pbz = SubProblem (''Isac_Knowledge'',
17.13 [''partial_fraction'',''rational'',''simplification''],
17.14 [''simplification'',''of_rationals'',''to_partial_fraction''])
17.15 [REAL funterm, REAL zzz];
17.16 - pbz_eq = Take (X'_z = pbz);
17.17 + pbz_eq = Take (X_z = pbz);
17.18 pbz_eq = Rewrite ''ruleYZ'' pbz_eq;
17.19 X_zeq = Take (X_z = rhs pbz_eq);
17.20 n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
17.21 @@ -133,7 +133,7 @@
17.22 Rule.Thm ("NTH_NIL", @{thm NTH_NIL}),
17.23 Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
17.24 Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
17.25 - Rule.Eval ("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"),
17.26 + Rule.Eval ("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
17.27 Rule.Eval ("Rational.get_denominator", eval_get_denominator "#get_denominator"),
17.28 Rule.Eval ("Rational.get_numerator", eval_get_numerator "#get_numerator"),
17.29 Rule.Eval ("Partial_Fractions.factors_from_solution",
17.30 @@ -144,6 +144,7 @@
17.31 \<close>
17.32 ML \<open>
17.33 \<close> ML \<open>
17.34 +\<close> ML \<open>
17.35 \<close>
17.36
17.37 end
18.1 --- a/src/Tools/isac/Knowledge/Isac_Knowledge.thy Fri May 07 13:23:24 2021 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Isac_Knowledge.thy Fri May 07 18:12:51 2021 +0200
18.3 @@ -23,10 +23,9 @@
18.4 RatPolyEq RatRootEq etc.
18.5 \<close>
18.6
18.7 -ML \<open>val version_isac = "isac version 120504 15:33";\<close>
18.8 ML \<open>
18.9 + val version_isac = "isac version 120504 15:33";
18.10 \<close> ML \<open>
18.11 \<close> ML \<open>
18.12 \<close>
18.13 -
18.14 end
19.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Fri May 07 13:23:24 2021 +0200
19.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Fri May 07 18:12:51 2021 +0200
19.3 @@ -31,9 +31,9 @@
19.4 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
19.5 Rule.Eval ("Prog_Expr.lhs" , Prog_Expr.eval_lhs ""),
19.6 Rule.Eval ("Prog_Expr.rhs" , Prog_Expr.eval_rhs ""),
19.7 - Rule.Eval ("Poly.has'_degree'_in", eval_has_degree_in ""),
19.8 - Rule.Eval ("Poly.is'_polyrat'_in", eval_is_polyrat_in ""),
19.9 - Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
19.10 + Rule.Eval ("Poly.has_degree_in", eval_has_degree_in ""),
19.11 + Rule.Eval ("Poly.is_polyrat_in", eval_is_polyrat_in ""),
19.12 + Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""),
19.13 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
19.14 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
19.15 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
19.16 @@ -160,7 +160,11 @@
19.17 crls = LinEq_crls, errpats = [], nrls = norm_Poly},
19.18 @{thm solve_linear_equation.simps})]
19.19 \<close>
19.20 -ML \<open>MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];\<close>
19.21 +ML \<open>
19.22 + MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];
19.23 +\<close> ML \<open>
19.24 +\<close> ML \<open>
19.25 +\<close>
19.26
19.27 end
19.28
20.1 --- a/src/Tools/isac/Knowledge/LogExp.thy Fri May 07 13:23:24 2021 +0200
20.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy Fri May 07 18:12:51 2021 +0200
20.3 @@ -7,7 +7,6 @@
20.4 consts
20.5
20.6 ln :: "real => real"
20.7 - exp :: "real => real" ("E'_ \<up> _" 80)
20.8 alog :: "[real, real] => real" ("_ log _" 90)
20.9
20.10 axiomatization where
20.11 @@ -52,6 +51,7 @@
20.12 {rew_ord' = "termlessI", rls' = PolyEq_erls, srls = Rule_Set.empty, prls = PolyEq_prls, calc = [],
20.13 crls = PolyEq_crls, errpats = [], nrls = norm_Rational},
20.14 @{thm solve_log.simps})]
20.15 +\<close> ML \<open>
20.16 +\<close> ML \<open>
20.17 \<close>
20.18 -
20.19 end
20.20 \ No newline at end of file
21.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri May 07 13:23:24 2021 +0200
21.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Fri May 07 18:12:51 2021 +0200
21.3 @@ -178,7 +178,7 @@
21.4 Rule.Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
21.5 Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
21.6 Rule.Eval("Prog_Expr.rhs", Prog_Expr.eval_rhs"eval_rhs_"),
21.7 - Rule.Eval("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"),
21.8 + Rule.Eval("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"),
21.9 Rule.Eval("Rational.get_denominator", eval_get_denominator "#get_denominator"),
21.10 Rule.Eval("Rational.get_numerator", eval_get_numerator "#get_numerator"),
21.11 Rule.Eval("Partial_Fractions.factors_from_solution",
21.12 @@ -251,6 +251,7 @@
21.13 ["simplification", "of_rationals", "to_partial_fraction"]);
21.14 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
21.15 *)
21.16 +\<close>ML \<open>
21.17 +\<close> ML \<open>
21.18 \<close>
21.19 -
21.20 end
21.21 \ No newline at end of file
22.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri May 07 13:23:24 2021 +0200
22.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri May 07 18:12:51 2021 +0200
22.3 @@ -52,14 +52,14 @@
22.4 subsection \<open>consts definition for predicates in specifications\<close>
22.5 consts
22.6
22.7 - is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _")
22.8 - is'_poly'_in :: "[real, real] => bool" ("_ is'_poly'_in _") (*RL DA *)
22.9 - has'_degree'_in :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *)
22.10 - is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*)
22.11 + is_expanded_in :: "[real, real] => bool" ("_ is'_expanded'_in _")
22.12 + is_poly_in :: "[real, real] => bool" ("_ is'_poly'_in _") (*RL DA *)
22.13 + has_degree_in :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *)
22.14 + is_polyrat_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*)
22.15
22.16 - is'_multUnordered:: "real => bool" ("_ is'_multUnordered")
22.17 - is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)
22.18 - is'_polyexp :: "real => bool" ("_ is'_polyexp")
22.19 + is_multUnordered:: "real => bool" ("_ is'_multUnordered")
22.20 + is_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)
22.21 + is_polyexp :: "real => bool" ("_ is'_polyexp")
22.22
22.23 subsection \<open>theorems not yet adopted from Isabelle\<close>
22.24 axiomatization where (*.not contained in Isabelle2002,
22.25 @@ -94,7 +94,7 @@
22.26 realpow_addI_atom: "r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)" and
22.27
22.28
22.29 - realpow_minus_even: "n is_even ==> (- r) \<up> n = r \<up> n" and
22.30 + realpow_minus_even: "n is_even ==> (- r) \<up> n = r \<up> n" and
22.31 realpow_minus_odd: "Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n" and
22.32
22.33
22.34 @@ -174,6 +174,7 @@
22.35 real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
22.36 real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
22.37
22.38 +
22.39 subsection \<open>auxiliary functions\<close>
22.40 ML \<open>
22.41 val thy = @{theory};
22.42 @@ -563,7 +564,7 @@
22.43 subsection \<open>evaluations functions\<close>
22.44 subsubsection \<open>for predicates\<close>
22.45 ML \<open>
22.46 -fun eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ =
22.47 +fun eval_is_polyrat_in _ _(p as (Const ("Poly.is_polyrat_in",_) $ t $ v)) _ =
22.48 if is_polyrat_in t v
22.49 then SOME ((UnparseC.term p) ^ " = True",
22.50 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
22.51 @@ -571,9 +572,9 @@
22.52 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
22.53 | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
22.54
22.55 -(*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
22.56 +(*("is_expanded_in", ("Poly.is_expanded_in", eval_is_expanded_in ""))*)
22.57 fun eval_is_expanded_in _ _
22.58 - (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
22.59 + (p as (Const ("Poly.is_expanded_in",_) $ t $ v)) _ =
22.60 if is_expanded_in t v
22.61 then SOME ((UnparseC.term p) ^ " = True",
22.62 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
22.63 @@ -581,9 +582,9 @@
22.64 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
22.65 | eval_is_expanded_in _ _ _ _ = NONE;
22.66
22.67 -(*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
22.68 +(*("is_poly_in", ("Poly.is_poly_in", eval_is_poly_in ""))*)
22.69 fun eval_is_poly_in _ _
22.70 - (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
22.71 + (p as (Const ("Poly.is_poly_in",_) $ t $ v)) _ =
22.72 if is_poly_in t v
22.73 then SOME ((UnparseC.term p) ^ " = True",
22.74 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
22.75 @@ -591,9 +592,9 @@
22.76 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
22.77 | eval_is_poly_in _ _ _ _ = NONE;
22.78
22.79 -(*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
22.80 +(*("has_degree_in", ("Poly.has_degree_in", eval_has_degree_in ""))*)
22.81 fun eval_has_degree_in _ _
22.82 - (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
22.83 + (p as (Const ("Poly.has_degree_in",_) $ t $ v)) _ =
22.84 let val d = has_degree_in t v
22.85 val d' = TermC.term_of_num HOLogic.realT d
22.86 in SOME ((UnparseC.term p) ^ " = " ^ (string_of_int d),
22.87 @@ -601,9 +602,9 @@
22.88 end
22.89 | eval_has_degree_in _ _ _ _ = NONE;
22.90
22.91 -(*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
22.92 +(*("is_polyexp", ("Poly.is_polyexp", eval_is_polyexp ""))*)
22.93 fun eval_is_polyexp (thmid:string) _
22.94 - (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
22.95 + (t as (Const("Poly.is_polyexp", _) $ arg)) thy =
22.96 if is_polyexp arg
22.97 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
22.98 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
22.99 @@ -615,9 +616,9 @@
22.100 subsubsection \<open>for hard-coded AC rewriting\<close>
22.101 ML \<open>
22.102 (*WN.18.6.03 *)
22.103 -(*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
22.104 +(*("is_addUnordered", ("Poly.is_addUnordered", eval_is_addUnordered ""))*)
22.105 fun eval_is_addUnordered (thmid:string) _
22.106 - (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
22.107 + (t as (Const("Poly.is_addUnordered", _) $ arg)) thy =
22.108 if is_addUnordered arg
22.109 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
22.110 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
22.111 @@ -626,7 +627,7 @@
22.112 | eval_is_addUnordered _ _ _ _ = NONE;
22.113
22.114 fun eval_is_multUnordered (thmid:string) _
22.115 - (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
22.116 + (t as (Const("Poly.is_multUnordered", _) $ arg)) thy =
22.117 if is_multUnordered arg
22.118 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
22.119 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
22.120 @@ -635,14 +636,14 @@
22.121 | eval_is_multUnordered _ _ _ _ = NONE;
22.122 \<close>
22.123 setup \<open>KEStore_Elems.add_calcs
22.124 - [("is_polyrat_in", ("Poly.is'_polyrat'_in",
22.125 + [("is_polyrat_in", ("Poly.is_polyrat_in",
22.126 eval_is_polyrat_in "#eval_is_polyrat_in")),
22.127 - ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
22.128 - ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
22.129 - ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
22.130 - ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
22.131 - ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
22.132 - ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))]\<close>
22.133 + ("is_expanded_in", ("Poly.is_expanded_in", eval_is_expanded_in "")),
22.134 + ("is_poly_in", ("Poly.is_poly_in", eval_is_poly_in "")),
22.135 + ("has_degree_in", ("Poly.has_degree_in", eval_has_degree_in "")),
22.136 + ("is_polyexp", ("Poly.is_polyexp", eval_is_polyexp "")),
22.137 + ("is_multUnordered", ("Poly.is_multUnordered", eval_is_multUnordered"")),
22.138 + ("is_addUnordered", ("Poly.is_addUnordered", eval_is_addUnordered ""))]\<close>
22.139
22.140 subsection \<open>rule-sets\<close>
22.141 subsubsection \<open>without specific order\<close>
22.142 @@ -654,18 +655,18 @@
22.143 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls
22.144 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
22.145 Rule.Thm ("real_unari_minus", ThmC.numerals_to_Free @{thm real_unari_minus}),
22.146 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
22.147 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
22.148 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.149 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")];
22.150 + Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
22.151 + Rule.Eval ("Groups.minus_class.minus", eval_binop "#sub_"),
22.152 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.153 + Rule.Eval ("Transcendental.powr", eval_binop "#power_")];
22.154
22.155 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls
22.156 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
22.157 Rule.Thm ("real_unari_minus", ThmC.numerals_to_Free @{thm real_unari_minus}),
22.158 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
22.159 - Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
22.160 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.161 - Rule.Eval ("Transcendental.powr" , (**)eval_binop "#power_")];
22.162 + Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
22.163 + Rule.Eval ("Groups.minus_class.minus", eval_binop "#sub_"),
22.164 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.165 + Rule.Eval ("Transcendental.powr" , eval_binop "#power_")];
22.166 \<close>
22.167 ML \<open>
22.168 val expand =
22.169 @@ -725,7 +726,7 @@
22.170 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [],
22.171 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.172 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
22.173 - [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")
22.174 + [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")
22.175 ],
22.176 srls = Rule_Set.Empty,
22.177 calc = [], errpatts = [],
22.178 @@ -798,14 +799,14 @@
22.179 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [],
22.180 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.181 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
22.182 - calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
22.183 - ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
22.184 - ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))
22.185 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
22.186 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
22.187 + ("POWER", ("Transcendental.powr", eval_binop "#power_"))
22.188 ],
22.189 errpatts = [],
22.190 - rules = [Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
22.191 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.192 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
22.193 + rules = [Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
22.194 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.195 + Rule.Eval ("Transcendental.powr", eval_binop "#power_")
22.196 ], scr = Rule.Empty_Prog};
22.197
22.198 val reduce_012_mult_ =
22.199 @@ -828,7 +829,7 @@
22.200 Rule_Def.Repeat{id = "collect_numerals_", preconds = [],
22.201 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.202 erls = Atools_erls, srls = Rule_Set.Empty,
22.203 - calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_"))
22.204 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
22.205 ], errpatts = [],
22.206 rules =
22.207 [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
22.208 @@ -841,7 +842,7 @@
22.209 Rule.Thm ("real_one_collect_assoc_r",ThmC.numerals_to_Free @{thm real_one_collect_assoc_r}),
22.210 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
22.211
22.212 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
22.213 + Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
22.214
22.215 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
22.216 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
22.217 @@ -949,9 +950,9 @@
22.218 Rule_Def.Repeat{id = "collect_numerals", preconds = [],
22.219 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.220 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
22.221 - calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
22.222 - ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
22.223 - ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))
22.224 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
22.225 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
22.226 + ("POWER", ("Transcendental.powr", eval_binop "#power_"))
22.227 ], errpatts = [],
22.228 rules = [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
22.229 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
22.230 @@ -962,9 +963,9 @@
22.231 (*"m is_const ==> n + m * n = (1 + m) * n"*)
22.232 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
22.233 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
22.234 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
22.235 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.236 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
22.237 + Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
22.238 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.239 + Rule.Eval ("Transcendental.powr", eval_binop "#power_")
22.240 ], scr = Rule.Empty_Prog};
22.241 val reduce_012 =
22.242 Rule_Def.Repeat{id = "reduce_012", preconds = [],
22.243 @@ -1057,12 +1058,12 @@
22.244 TermC.parse_patt thy "?p :: real")],
22.245 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.246 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
22.247 - [Rule.Eval ("Poly.is'_multUnordered",
22.248 + [Rule.Eval ("Poly.is_multUnordered",
22.249 eval_is_multUnordered "")],
22.250 - calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
22.251 - ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
22.252 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
22.253 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
22.254 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
22.255 - ("POWER" , ("Transcendental.powr", (**)eval_binop "#power_"))],
22.256 + ("POWER" , ("Transcendental.powr", eval_binop "#power_"))],
22.257 errpatts = [],
22.258 scr = Rule.Rfuns {init_state = init_state,
22.259 normal_form = normal_form,
22.260 @@ -1097,11 +1098,11 @@
22.261 fuer die Evaluation der Precondition "p is_addUnordered"*))],
22.262 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
22.263 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
22.264 - [Rule.Eval ("Poly.is'_addUnordered", eval_is_addUnordered "")],
22.265 - calc = [("PLUS" ,("Groups.plus_class.plus", (**)eval_binop "#add_")),
22.266 - ("TIMES" ,("Groups.times_class.times", (**)eval_binop "#mult_")),
22.267 + [Rule.Eval ("Poly.is_addUnordered", eval_is_addUnordered "")],
22.268 + calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
22.269 + ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
22.270 ("DIVIDE",("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
22.271 - ("POWER" ,("Transcendental.powr" , (**)eval_binop "#power_"))],
22.272 + ("POWER" ,("Transcendental.powr" , eval_binop "#power_"))],
22.273 errpatts = [],
22.274 scr = Rule.Rfuns {init_state = init_state,
22.275 normal_form = normal_form,
22.276 @@ -1135,7 +1136,7 @@
22.277 erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [],
22.278 rules = [Rule.Rls_ discard_minus,
22.279 Rule.Rls_ expand_poly_,
22.280 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.281 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.282 Rule.Rls_ order_mult_rls_,
22.283 Rule.Rls_ simplify_power_,
22.284 Rule.Rls_ calc_add_mult_pow_,
22.285 @@ -1155,7 +1156,7 @@
22.286 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.287 rules = [Rule.Rls_ discard_minus,
22.288 Rule.Rls_ expand_poly_,
22.289 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.290 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.291 Rule.Rls_ order_mult_rls_,
22.292 Rule.Rls_ simplify_power_,
22.293 Rule.Rls_ calc_add_mult_pow_,
22.294 @@ -1178,7 +1179,7 @@
22.295 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
22.296 rules = [Rule.Rls_ discard_minus,
22.297 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
22.298 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.299 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.300 Rule.Rls_ order_mult_rls_,
22.301 Rule.Rls_ simplify_power_,
22.302 Rule.Rls_ calc_add_mult_pow_,
22.303 @@ -1197,9 +1198,9 @@
22.304 val rev_rew_p =
22.305 Rule_Set.Sequence{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
22.306 erls = Atools_erls, srls = Rule_Set.Empty,
22.307 - calc = [(*("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
22.308 - ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
22.309 - ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))*)
22.310 + calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
22.311 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
22.312 + ("POWER", ("Transcendental.powr", eval_binop "#power_"))*)
22.313 ], errpatts = [],
22.314 rules = [Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
22.315 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
22.316 @@ -1220,9 +1221,9 @@
22.317 Rule.Rls_ order_mult_rls_,
22.318 (*Rule.Rls_ order_add_rls_,*)
22.319
22.320 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
22.321 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.322 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
22.323 + Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
22.324 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.325 + Rule.Eval ("Transcendental.powr", eval_binop "#power_"),
22.326
22.327 Rule.Thm ("sym_realpow_twoI",
22.328 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
22.329 @@ -1246,9 +1247,9 @@
22.330 Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
22.331 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
22.332
22.333 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
22.334 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.335 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
22.336 + Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
22.337 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.338 + Rule.Eval ("Transcendental.powr", eval_binop "#power_"),
22.339
22.340 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),(*"1 * z = z"*)
22.341 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),(*"0 * z = 0"*)
22.342 @@ -1299,9 +1300,9 @@
22.343 val expand_binoms =
22.344 Rule_Def.Repeat{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
22.345 erls = Atools_erls, srls = Rule_Set.Empty,
22.346 - calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
22.347 - ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
22.348 - ("POWER", ("Transcendental.powr", (**)eval_binop "#power_"))
22.349 + calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
22.350 + ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
22.351 + ("POWER", ("Transcendental.powr", eval_binop "#power_"))
22.352 ], errpatts = [],
22.353 rules = [Rule.Thm ("real_plus_binom_pow2",
22.354 ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
22.355 @@ -1354,9 +1355,9 @@
22.356 (*"0 * z = 0"*)
22.357 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),(*"0 + z = z"*)
22.358
22.359 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
22.360 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.361 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_"),
22.362 + Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
22.363 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.364 + Rule.Eval ("Transcendental.powr", eval_binop "#power_"),
22.365 (*Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
22.366 (*AC-rewriting*)
22.367 Rule.Thm ("real_mult_left_commute",
22.368 @@ -1389,9 +1390,9 @@
22.369 ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
22.370 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
22.371
22.372 - Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
22.373 - Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
22.374 - Rule.Eval ("Transcendental.powr", (**)eval_binop "#power_")
22.375 + Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
22.376 + Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
22.377 + Rule.Eval ("Transcendental.powr", eval_binop "#power_")
22.378 ],
22.379 scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})
22.380 };
22.381 @@ -1440,7 +1441,7 @@
22.382 ("#Where" ,["t_t is_polyexp"]),
22.383 ("#Find" ,["normalform n_n"])],
22.384 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
22.385 - Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
22.386 + Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
22.387 SOME "Simplify t_t",
22.388 [["simplification", "for_polynomials"]]))]\<close>
22.389
22.390 @@ -1458,7 +1459,7 @@
22.391 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
22.392 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
22.393 [(*for preds in where_*)
22.394 - Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp"")],
22.395 + Rule.Eval ("Poly.is_polyexp", eval_is_polyexp"")],
22.396 crls = Rule_Set.empty, errpats = [], nrls = norm_Poly},
22.397 @{thm simplify.simps})]
22.398 \<close>
23.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Fri May 07 13:23:24 2021 +0200
23.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Fri May 07 18:12:51 2021 +0200
23.3 @@ -328,15 +328,15 @@
23.4 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
23.5 Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs ""),
23.6 Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),
23.7 - Rule.Eval ("Poly.is'_expanded'_in", eval_is_expanded_in ""),
23.8 - Rule.Eval ("Poly.is'_poly'_in", eval_is_poly_in ""),
23.9 - Rule.Eval ("Poly.has'_degree'_in", eval_has_degree_in ""),
23.10 - Rule.Eval ("Poly.is'_polyrat'_in", eval_is_polyrat_in ""),
23.11 - (*Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""), *)
23.12 - (*Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),*)
23.13 + Rule.Eval ("Poly.is_expanded_in", eval_is_expanded_in ""),
23.14 + Rule.Eval ("Poly.is_poly_in", eval_is_poly_in ""),
23.15 + Rule.Eval ("Poly.has_degree_in", eval_has_degree_in ""),
23.16 + Rule.Eval ("Poly.is_polyrat_in", eval_is_polyrat_in ""),
23.17 + (*Rule.Eval ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""), *)
23.18 + (*Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),*)
23.19 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
23.20 - Rule.Eval ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in ""),
23.21 - Rule.Eval ("RatEq.is'_ratequation'_in", eval_is_ratequation_in ""),
23.22 + Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""),
23.23 + Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in ""),
23.24 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
23.25 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
23.26 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
23.27 @@ -1336,8 +1336,11 @@
23.28 ("collect_bdv", (Context.theory_name @{theory}, collect_bdv)),
23.29 ("make_polynomial_in", (Context.theory_name @{theory}, make_polynomial_in)),
23.30 ("make_ratpoly_in", (Context.theory_name @{theory}, make_ratpoly_in)),
23.31 - ("separate_bdvs", (Context.theory_name @{theory}, separate_bdvs))]\<close>
23.32 -
23.33 + ("separate_bdvs", (Context.theory_name @{theory}, separate_bdvs))]
23.34 +\<close> ML \<open>
23.35 +\<close> ML \<open>
23.36 +\<close> ML \<open>
23.37 +\<close>
23.38 end
23.39
23.40
24.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Fri May 07 13:23:24 2021 +0200
24.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Fri May 07 18:12:51 2021 +0200
24.3 @@ -9,7 +9,7 @@
24.4
24.5 (*predicates for conditions in rewriting*)
24.6 kleiner :: "['a, 'a] => bool" ("_ kleiner _")
24.7 - ist'_monom :: "'a => bool" ("_ ist'_monom")
24.8 + ist_monom :: "'a => bool" ("_ ist'_monom")
24.9
24.10 (*the CAS-command*)
24.11 Probe :: "[bool, bool list] => bool"
24.12 @@ -178,8 +178,8 @@
24.13 | ist_monom _ = false;
24.14
24.15 (* is this a univariate monomial ? *)
24.16 -(*("ist_monom", ("PolyMinus.ist'_monom", eval_ist_monom ""))*)
24.17 -fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist'_monom",_) $ a)) _ =
24.18 +(*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*)
24.19 +fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist_monom",_) $ a)) _ =
24.20 if ist_monom a then
24.21 SOME ((UnparseC.term p) ^ " = True",
24.22 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
24.23 @@ -195,7 +195,7 @@
24.24 val erls_ordne_alphabetisch =
24.25 Rule_Set.append_rules "erls_ordne_alphabetisch" Rule_Set.empty
24.26 [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""),
24.27 - Rule.Eval ("PolyMinus.ist'_monom", eval_ist_monom "")
24.28 + Rule.Eval ("PolyMinus.ist_monom", eval_ist_monom "")
24.29 ];
24.30
24.31 val ordne_alphabetisch =
24.32 @@ -224,7 +224,7 @@
24.33 Rule_Def.Repeat{id = "fasse_zusammen", preconds = [],
24.34 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
24.35 erls = Rule_Set.append_rules "erls_fasse_zusammen" Rule_Set.empty
24.36 - [Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")],
24.37 + [Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")],
24.38 srls = Rule_Set.Empty, calc = [], errpatts = [],
24.39 rules =
24.40 [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
24.41 @@ -353,7 +353,7 @@
24.42 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord), srls = Rule_Set.Empty, calc = [], errpatts = [],
24.43 erls = Rule_Set.append_rules "erls_ordne_monome" Rule_Set.empty
24.44 [Rule.Eval ("PolyMinus.kleiner", eval_kleiner ""),
24.45 - Rule.Eval ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "")
24.46 + Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "")
24.47 ],
24.48 rules = [Rule.Thm ("tausche_mal",ThmC.numerals_to_Free @{thm tausche_mal}),
24.49 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
24.50 @@ -416,7 +416,7 @@
24.51 " matchsub ((?b - ?c) * ?a) t_t )"]),
24.52 ("#Find", ["normalform n_n"])],
24.53 Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty
24.54 - [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp ""),
24.55 + [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
24.56 Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
24.57 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
24.58 (*"(?a | True) = True"*)
24.59 @@ -437,7 +437,7 @@
24.60 " matchsub ((?b - ?c) * ?a) t_t )"]),
24.61 ("#Find" ,["normalform n_n"])],
24.62 Rule_Set.append_rules "prls_pbl_vereinf_poly_klammer" Rule_Set.empty
24.63 - [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp ""),
24.64 + [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
24.65 Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
24.66 Rule.Thm ("or_true", ThmC.numerals_to_Free @{thm or_true}),
24.67 (*"(?a | True) = True"*)
24.68 @@ -455,7 +455,7 @@
24.69 ("#Where", ["t_t is_polyexp"]),
24.70 ("#Find", ["normalform n_n"])],
24.71 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
24.72 - Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
24.73 + Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
24.74 SOME "Vereinfache t_t",
24.75 [["simplification", "for_polynomials", "with_parentheses_mult"]])),
24.76 (Problem.prep_input thy "pbl_probe" [] Problem.id_empty (["probe"], [], Rule_Set.Empty, NONE, [])),
24.77 @@ -465,7 +465,7 @@
24.78 ("#Where", ["e_e is_polyexp"]),
24.79 ("#Find", ["Geprueft p_p"])],
24.80 Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
24.81 - Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
24.82 + Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
24.83 SOME "Probe e_e w_w",
24.84 [["probe", "fuer_polynom"]])),
24.85 (Problem.prep_input thy "pbl_probe_bruch" [] Problem.id_empty
24.86 @@ -474,7 +474,7 @@
24.87 ("#Where" ,["e_e is_ratpolyexp"]),
24.88 ("#Find" ,["Geprueft p_p"])],
24.89 Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
24.90 - Rule.Eval ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
24.91 + Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
24.92 SOME "Probe e_e w_w", [["probe", "fuer_bruch"]]))]\<close>
24.93
24.94 (** methods **)
24.95 @@ -499,7 +499,7 @@
24.96 ("#Find" ,["normalform n_n"])],
24.97 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
24.98 prls = Rule_Set.append_rules "prls_met_simp_poly_minus" Rule_Set.empty
24.99 - [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp ""),
24.100 + [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp ""),
24.101 Rule.Eval ("Prog_Expr.matchsub", Prog_Expr.eval_matchsub ""),
24.102 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
24.103 (*"(?a & True) = ?a"*)
24.104 @@ -530,7 +530,7 @@
24.105 ("#Find" ,["normalform n_n"])],
24.106 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
24.107 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
24.108 - [(*for preds in where_*) Rule.Eval("Poly.is'_polyexp", eval_is_polyexp"")],
24.109 + [(*for preds in where_*) Rule.Eval("Poly.is_polyexp", eval_is_polyexp"")],
24.110 crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
24.111 @{thm simplify2.simps})]
24.112 \<close>
24.113 @@ -553,7 +553,7 @@
24.114 [("#Given" ,["Term t_t"]), ("#Where" ,["t_t is_polyexp"]), ("#Find" ,["normalform n_n"])],
24.115 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
24.116 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
24.117 - [(*for preds in where_*) Rule.Eval("Poly.is'_polyexp", eval_is_polyexp"")],
24.118 + [(*for preds in where_*) Rule.Eval("Poly.is_polyexp", eval_is_polyexp"")],
24.119 crls = Rule_Set.empty, errpats = [], nrls = rls_p_34},
24.120 @{thm simplify3.simps})]
24.121 \<close>
24.122 @@ -585,7 +585,7 @@
24.123 ("#Find" ,["Geprueft p_p"])],
24.124 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
24.125 prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
24.126 - [(*for preds in where_*) Rule.Eval ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
24.127 + [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
24.128 crls = Rule_Set.empty, errpats = [], nrls = rechnen},
24.129 @{thm mache_probe.simps})]
24.130 \<close>
24.131 @@ -597,9 +597,11 @@
24.132 ("#Find" ,["Geprueft p_p"])],
24.133 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
24.134 prls = Rule_Set.append_rules "prls_met_probe_bruch" Rule_Set.empty
24.135 - [(*for preds in where_*) Rule.Eval ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
24.136 + [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
24.137 crls = Rule_Set.empty, errpats = [], nrls = Rule_Set.Empty},
24.138 @{thm refl})]
24.139 +\<close> ML \<open>
24.140 +\<close> ML \<open>
24.141 \<close>
24.142
24.143 end
25.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Fri May 07 13:23:24 2021 +0200
25.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Fri May 07 18:12:51 2021 +0200
25.3 @@ -23,7 +23,7 @@
25.4
25.5 subsection \<open>consts definition for predicates in specifications\<close>
25.6 consts
25.7 - is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")
25.8 + is_ratequation_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")
25.9
25.10 subsection \<open>theorems not yet adopted from Isabelle\<close>
25.11 axiomatization where
25.12 @@ -69,7 +69,7 @@
25.13
25.14 subsection \<open>evaluations functions\<close>
25.15 ML \<open>
25.16 -fun eval_is_ratequation_in _ _ (p as (Const ("RatEq.is'_ratequation'_in",_) $ t $ v)) _ =
25.17 +fun eval_is_ratequation_in _ _ (p as (Const ("RatEq.is_ratequation_in",_) $ t $ v)) _ =
25.18 if is_rateqation_in t v
25.19 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
25.20 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
25.21 @@ -86,7 +86,7 @@
25.22 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
25.23 Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs ""),
25.24 Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),
25.25 - Rule.Eval ("RatEq.is'_ratequation'_in", eval_is_ratequation_in ""),
25.26 + Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in ""),
25.27 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
25.28 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
25.29 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
25.30 @@ -103,7 +103,7 @@
25.31 (Rule_Set.merge "is_ratequation_in" calculate_Rational
25.32 (Rule_Set.append_rules "is_ratequation_in"
25.33 Poly_erls [(*Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),*)
25.34 - Rule.Eval ("RatEq.is'_ratequation'_in", eval_is_ratequation_in "")]))
25.35 + Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in "")]))
25.36 [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)
25.37 Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})]; (*WN: ein Hack*)
25.38
25.39 @@ -113,7 +113,7 @@
25.40 (Rule_Set.merge "is_ratequation_in" calculate_Rational
25.41 (Rule_Set.append_rules "is_ratequation_in"
25.42 Poly_erls [(*Rule.Eval ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e"),*)
25.43 - Rule.Eval ("RatEq.is'_ratequation'_in", eval_is_ratequation_in "")]))
25.44 + Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in "")]))
25.45 [Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}), (*WN: ein Hack*)
25.46 Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute})]; (*WN: ein Hack*)
25.47
26.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri May 07 13:23:24 2021 +0200
26.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri May 07 18:12:51 2021 +0200
26.3 @@ -14,8 +14,8 @@
26.4 section \<open>Constants for evaluation by "Rule.Eval"\<close>
26.5 consts
26.6
26.7 - is'_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
26.8 - is'_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")
26.9 + is_expanded :: "real => bool" ("_ is'_expanded") (*RL->Poly.thy*)
26.10 + is_ratpolyexp :: "real => bool" ("_ is'_ratpolyexp")
26.11 get_denominator :: "real => real"
26.12 get_numerator :: "real => real"
26.13
26.14 @@ -39,9 +39,9 @@
26.15 ((is_ratpolyexp t1) andalso (is_ratpolyexp t2))
26.16 | is_ratpolyexp _ = false;
26.17
26.18 -(*("is_ratpolyexp", ("Rational.is'_ratpolyexp", eval_is_ratpolyexp ""))*)
26.19 +(*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
26.20 fun eval_is_ratpolyexp (thmid:string) _
26.21 - (t as (Const("Rational.is'_ratpolyexp", _) $ arg)) thy =
26.22 + (t as (Const("Rational.is_ratpolyexp", _) $ arg)) thy =
26.23 if is_ratpolyexp arg
26.24 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
26.25 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
26.26 @@ -395,7 +395,7 @@
26.27 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
26.28 rules =
26.29 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
26.30 - Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
26.31 + Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
26.32 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
26.33 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false})],
26.34 scr = Rule.Empty_Prog});
26.35 @@ -448,9 +448,9 @@
26.36 scr = Rule.Empty_Prog})
26.37 calculate_Poly);
26.38
26.39 -(*("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))*)
26.40 +(*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
26.41 fun eval_is_expanded (thmid:string) _
26.42 - (t as (Const("Rational.is'_expanded", _) $ arg)) thy =
26.43 + (t as (Const("Rational.is_expanded", _) $ arg)) thy =
26.44 if is_expanded arg
26.45 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
26.46 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
26.47 @@ -459,12 +459,12 @@
26.48 | eval_is_expanded _ _ _ _ = NONE;
26.49 \<close>
26.50 setup \<open>KEStore_Elems.add_calcs
26.51 - [("is_expanded", ("Rational.is'_expanded", eval_is_expanded ""))]\<close>
26.52 + [("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))]\<close>
26.53 ML \<open>
26.54 val rational_erls =
26.55 Rule_Set.merge "rational_erls" calculate_Rational
26.56 (Rule_Set.append_rules "is_expanded" Atools_erls
26.57 - [Rule.Eval ("Rational.is'_expanded", eval_is_expanded "")]);
26.58 + [Rule.Eval ("Rational.is_expanded", eval_is_expanded "")]);
26.59 \<close>
26.60
26.61 subsection \<open>Embed cancellation into rewriting\<close>
26.62 @@ -604,8 +604,8 @@
26.63 val powers_erls = prep_rls'(
26.64 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
26.65 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
26.66 - rules = [Rule.Eval ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),
26.67 - Rule.Eval ("Prog_Expr.is'_even", Prog_Expr.eval_is_even "#is_even_"),
26.68 + rules = [Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
26.69 + Rule.Eval ("Prog_Expr.is_even", Prog_Expr.eval_is_even "#is_even_"),
26.70 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
26.71 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
26.72 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
26.73 @@ -706,7 +706,7 @@
26.74 val norm_rat_erls = prep_rls'(
26.75 Rule_Def.Repeat {id = "norm_rat_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
26.76 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
26.77 - rules = [Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")
26.78 + rules = [Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_")
26.79 ], scr = Rule.Empty_Prog});
26.80
26.81 (* consists of rls containing the absolute minimum of thms *)
26.82 @@ -778,7 +778,7 @@
26.83 used in initial part norm_Rational_mg, see example DA-M02-main.p.60.*)
26.84 val rat_mult_poly = prep_rls'(
26.85 Rule_Def.Repeat {id = "rat_mult_poly", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
26.86 - erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
26.87 + erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
26.88 srls = Rule_Set.Empty, calc = [], errpatts = [],
26.89 rules =
26.90 [Rule.Thm ("rat_mult_poly_l",ThmC.numerals_to_Free @{thm rat_mult_poly_l}),
26.91 @@ -913,9 +913,10 @@
26.92 ("#Find" ,["normalform n_n"])],
26.93 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
26.94 prls = Rule_Set.append_rules "simplification_of_rationals_prls" Rule_Set.empty
26.95 - [(*for preds in where_*) Rule.Eval ("Rational.is'_ratpolyexp", eval_is_ratpolyexp "")],
26.96 + [(*for preds in where_*) Rule.Eval ("Rational.is_ratpolyexp", eval_is_ratpolyexp "")],
26.97 crls = Rule_Set.empty, errpats = [], nrls = norm_Rational_rls},
26.98 @{thm simplify.simps})]
26.99 +\<close> ML \<open>
26.100 +\<close> ML \<open>
26.101 \<close>
26.102 -
26.103 end
27.1 --- a/src/Tools/isac/Knowledge/Root.thy Fri May 07 13:23:24 2021 +0200
27.2 +++ b/src/Tools/isac/Knowledge/Root.thy Fri May 07 18:12:51 2021 +0200
27.3 @@ -330,6 +330,8 @@
27.4 \<close>
27.5 setup \<open>KEStore_Elems.add_rlss
27.6 [("expand_rootbinoms", (Context.theory_name @{theory}, expand_rootbinoms))]\<close>
27.7 -
27.8 -
27.9 +ML \<open>
27.10 +\<close> ML \<open>
27.11 +\<close> ML \<open>
27.12 +\<close>
27.13 end
28.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Fri May 07 13:23:24 2021 +0200
28.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Fri May 07 18:12:51 2021 +0200
28.3 @@ -21,9 +21,9 @@
28.4
28.5 subsection \<open>consts definition for predicates\<close>
28.6 consts
28.7 - is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _")
28.8 - is'_sqrtTerm'_in :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _")
28.9 - is'_normSqrtTerm'_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _")
28.10 + is_rootTerm_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _")
28.11 + is_sqrtTerm_in :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _")
28.12 + is_normSqrtTerm_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _")
28.13
28.14 subsection \<open>theorems not yet adopted from Isabelle\<close>
28.15 axiomatization where
28.16 @@ -153,27 +153,27 @@
28.17 isnorm t v
28.18 end;
28.19
28.20 -fun eval_is_rootTerm_in _ _ (p as (Const ("RootEq.is'_rootTerm'_in",_) $ t $ v)) _ =
28.21 +fun eval_is_rootTerm_in _ _ (p as (Const ("RootEq.is_rootTerm_in",_) $ t $ v)) _ =
28.22 if is_rootTerm_in t v
28.23 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
28.24 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
28.25 | eval_is_rootTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
28.26
28.27 -fun eval_is_sqrtTerm_in _ _ (p as (Const ("RootEq.is'_sqrtTerm'_in",_) $ t $ v)) _ =
28.28 +fun eval_is_sqrtTerm_in _ _ (p as (Const ("RootEq.is_sqrtTerm_in",_) $ t $ v)) _ =
28.29 if is_sqrtTerm_in t v
28.30 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
28.31 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
28.32 | eval_is_sqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
28.33
28.34 -fun eval_is_normSqrtTerm_in _ _ (p as (Const ("RootEq.is'_normSqrtTerm'_in",_) $ t $ v)) _ =
28.35 +fun eval_is_normSqrtTerm_in _ _ (p as (Const ("RootEq.is_normSqrtTerm_in",_) $ t $ v)) _ =
28.36 if is_normSqrtTerm_in t v
28.37 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
28.38 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
28.39 | eval_is_normSqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
28.40 \<close>
28.41 setup \<open>KEStore_Elems.add_calcs
28.42 - [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in"")),
28.43 - ("is_sqrtTerm_in", ("RootEq.is'_sqrtTerm'_in", eval_is_sqrtTerm_in"")),
28.44 + [("is_rootTerm_in", ("RootEq.is_rootTerm_in", eval_is_rootTerm_in"")),
28.45 + ("is_sqrtTerm_in", ("RootEq.is_sqrtTerm_in", eval_is_sqrtTerm_in"")),
28.46 ("is_normSqrtTerm_in", ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in""))]\<close>
28.47
28.48 subsection \<open>rule-sets\<close>
28.49 @@ -184,9 +184,9 @@
28.50 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
28.51 Rule.Eval ("Prog_Expr.lhs" , Prog_Expr.eval_lhs ""),
28.52 Rule.Eval ("Prog_Expr.rhs" , Prog_Expr.eval_rhs ""),
28.53 - Rule.Eval ("RootEq.is'_sqrtTerm'_in", eval_is_sqrtTerm_in ""),
28.54 - Rule.Eval ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in ""),
28.55 - Rule.Eval ("RootEq.is'_normSqrtTerm'_in", eval_is_normSqrtTerm_in ""),
28.56 + Rule.Eval ("RootEq.is_sqrtTerm_in", eval_is_sqrtTerm_in ""),
28.57 + Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""),
28.58 + Rule.Eval ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in ""),
28.59 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
28.60 Rule.Thm ("not_true", ThmC.numerals_to_Free @{thm not_true}),
28.61 Rule.Thm ("not_false", ThmC.numerals_to_Free @{thm not_false}),
28.62 @@ -206,9 +206,9 @@
28.63
28.64 val rooteq_srls =
28.65 Rule_Set.append_rules "rooteq_srls" Rule_Set.empty
28.66 - [Rule.Eval ("RootEq.is'_sqrtTerm'_in", eval_is_sqrtTerm_in ""),
28.67 - Rule.Eval ("RootEq.is'_normSqrtTerm'_in", eval_is_normSqrtTerm_in""),
28.68 - Rule.Eval ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in "")];
28.69 + [Rule.Eval ("RootEq.is_sqrtTerm_in", eval_is_sqrtTerm_in ""),
28.70 + Rule.Eval ("RootEq.is_normSqrtTerm_in", eval_is_normSqrtTerm_in""),
28.71 + Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in "")];
28.72 \<close>
28.73 ML \<open>
28.74
29.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Fri May 07 13:23:24 2021 +0200
29.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Fri May 07 18:12:51 2021 +0200
29.3 @@ -30,5 +30,8 @@
29.4 setup \<open>KEStore_Elems.add_rlss
29.5 [("rootrat_erls", (Context.theory_name @{theory}, prep_rls' rootrat_erls)),
29.6 ("calculate_RootRat", (Context.theory_name @{theory}, prep_rls' calculate_RootRat))]\<close>
29.7 -
29.8 +ML \<open>
29.9 +\<close> ML \<open>
29.10 +\<close> ML \<open>
29.11 +\<close>
29.12 end
30.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Fri May 07 13:23:24 2021 +0200
30.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Fri May 07 18:12:51 2021 +0200
30.3 @@ -17,8 +17,7 @@
30.4
30.5 subsection \<open>consts definition for predicates\<close>
30.6 consts
30.7 - is'_rootRatAddTerm'_in :: "[real, real] => bool"
30.8 - ("_ is'_rootRatAddTerm'_in _") (*RL*)
30.9 + is_rootRatAddTerm_in :: "[real, real] => bool" ("_ is'_rootRatAddTerm'_in _") (*RL*)
30.10
30.11 subsection \<open>theorems not yet adopted from Isabelle\<close>
30.12 axiomatization where
30.13 @@ -58,7 +57,7 @@
30.14 findrootrat t v
30.15 end;
30.16
30.17 -fun eval_is_rootRatAddTerm_in _ _ (p as (Const ("RootRatEq.is'_rootRatAddTerm'_in",_) $ t $ v)) _ =
30.18 +fun eval_is_rootRatAddTerm_in _ _ (p as (Const ("RootRatEq.is_rootRatAddTerm_in",_) $ t $ v)) _ =
30.19 if is_rootRatAddTerm_in t v
30.20 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
30.21 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
30.22 @@ -75,8 +74,8 @@
30.23 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
30.24 Rule.Eval ("Prog_Expr.lhs", Prog_Expr.eval_lhs ""),
30.25 Rule.Eval ("Prog_Expr.rhs", Prog_Expr.eval_rhs ""),
30.26 - Rule.Eval ("RootEq.is'_rootTerm'_in", eval_is_rootTerm_in ""),
30.27 - Rule.Eval ("RootRatEq.is'_rootRatAddTerm'_in", eval_is_rootRatAddTerm_in ""),
30.28 + Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""),
30.29 + Rule.Eval ("RootRatEq.is_rootRatAddTerm_in", eval_is_rootRatAddTerm_in ""),
30.30 Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
30.31 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
30.32 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
30.33 @@ -161,5 +160,7 @@
30.34 {rew_ord'="termlessI", rls'=RooRatEq_erls, srls=Rule_Set.empty, prls=RootRatEq_prls, calc=[],
30.35 crls=RootRatEq_crls, errpats = [], nrls = norm_Rational},
30.36 @{thm solve_rootrat_equ.simps})]
30.37 +\<close> ML \<open>
30.38 +\<close> ML \<open>
30.39 \<close>
30.40 end
31.1 --- a/src/Tools/isac/Knowledge/Test.thy Fri May 07 13:23:24 2021 +0200
31.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri May 07 18:12:51 2021 +0200
31.3 @@ -16,13 +16,13 @@
31.4
31.5 section \<open>consts for problems\<close>
31.6 consts
31.7 - "is'_root'_free" :: "'a => bool" ("is'_root'_free _" 10)
31.8 - "contains'_root" :: "'a => bool" ("contains'_root _" 10)
31.9 + "is_root_free" :: "'a => bool" ("is'_root'_free _" 10)
31.10 + "contains_root" :: "'a => bool" ("contains'_root _" 10)
31.11
31.12 - "precond'_rootmet" :: "'a => bool" ("precond'_rootmet _" 10)
31.13 - "precond'_rootpbl" :: "'a => bool" ("precond'_rootpbl _" 10)
31.14 - "precond'_submet" :: "'a => bool" ("precond'_submet _" 10)
31.15 - "precond'_subpbl" :: "'a => bool" ("precond'_subpbl _" 10)
31.16 + "precond_rootmet" :: "'a => bool" ("precond'_rootmet _" 10)
31.17 + "precond_rootpbl" :: "'a => bool" ("precond'_rootpbl _" 10)
31.18 + "precond_submet" :: "'a => bool" ("precond'_submet _" 10)
31.19 + "precond_subpbl" :: "'a => bool" ("precond'_subpbl _" 10)
31.20
31.21
31.22 section \<open>functions\<close>
31.23 @@ -254,7 +254,7 @@
31.24
31.25 (*does a term contain a root ?*)
31.26 fun eval_contains_root (thmid:string) _
31.27 - (t as (Const("Test.contains'_root", _) $ arg)) thy =
31.28 + (t as (Const("Test.contains_root", _) $ arg)) thy =
31.29 if member op = (ids_of arg) "sqrt"
31.30 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
31.31 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
31.32 @@ -263,21 +263,21 @@
31.33 | eval_contains_root _ _ _ _ = NONE;
31.34
31.35 (*dummy precondition for root-met of x+1=2*)
31.36 -fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond'_rootmet", _) $ arg)) thy =
31.37 +fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond_rootmet", _) $ arg)) thy =
31.38 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
31.39 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
31.40 | eval_precond_rootmet _ _ _ _ = NONE;
31.41
31.42 (*dummy precondition for root-pbl of x+1=2*)
31.43 -fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond'_rootpbl", _) $ arg)) thy =
31.44 +fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond_rootpbl", _) $ arg)) thy =
31.45 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
31.46 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
31.47 | eval_precond_rootpbl _ _ _ _ = NONE;
31.48 \<close>
31.49 setup \<open>KEStore_Elems.add_calcs
31.50 - [("contains_root", ("Test.contains'_root", eval_contains_root"#contains_root_")),
31.51 - ("Test.precond'_rootmet", ("Test.precond'_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),
31.52 - ("Test.precond'_rootpbl", ("Test.precond'_rootpbl",
31.53 + [("contains_root", ("Test.contains_root", eval_contains_root"#contains_root_")),
31.54 + ("Test.precond_rootmet", ("Test.precond_rootmet", eval_precond_rootmet"#Test.precond_rootmet_")),
31.55 + ("Test.precond_rootpbl", ("Test.precond_rootpbl",
31.56 eval_precond_rootpbl"#Test.precond_rootpbl_"))]
31.57 \<close>
31.58 ML \<open>
31.59 @@ -377,7 +377,7 @@
31.60 Rule.Thm ("and_commute",ThmC.numerals_to_Free @{thm and_commute}),
31.61 Rule.Thm ("or_commute",ThmC.numerals_to_Free @{thm or_commute}),
31.62
31.63 - Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
31.64 + Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
31.65 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
31.66
31.67 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
31.68 @@ -418,10 +418,10 @@
31.69 Rule.Thm ("root_ge0_1",ThmC.numerals_to_Free @{thm root_ge0_1}),
31.70 Rule.Thm ("root_ge0_2",ThmC.numerals_to_Free @{thm root_ge0_2}),
31.71
31.72 - Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"),
31.73 - Rule.Eval ("Test.contains'_root", eval_contains_root "#eval_contains_root"),
31.74 + Rule.Eval ("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"),
31.75 + Rule.Eval ("Test.contains_root", eval_contains_root "#eval_contains_root"),
31.76 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches ""),
31.77 - Rule.Eval ("Test.contains'_root",
31.78 + Rule.Eval ("Test.contains_root",
31.79 eval_contains_root"#contains_root_"),
31.80
31.81 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
31.82 @@ -811,7 +811,7 @@
31.83 [("#Given" ,["equality e_e", "solveFor v_v"]),
31.84 ("#Where" ,["precond_rootpbl v_v"]),
31.85 ("#Find" ,["solutions v_v'i'"])],
31.86 - Rule_Set.append_rules "contains_root" Rule_Set.empty [Rule.Eval ("Test.contains'_root",
31.87 + Rule_Set.append_rules "contains_root" Rule_Set.empty [Rule.Eval ("Test.contains_root",
31.88 eval_contains_root "#contains_root_")],
31.89 SOME "solve (e_e::bool, v_v)", [["Test", "square_equation"]])),
31.90 (Problem.prep_input thy "pbl_test_uni_norm" [] Problem.id_empty
31.91 @@ -891,9 +891,9 @@
31.92 ("#Find" ,["solutions v_v'i'"])],
31.93 {rew_ord'="e_rew_ord",rls'=tval_rls,
31.94 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
31.95 - [Rule.Eval ("Test.contains'_root", eval_contains_root "")],
31.96 + [Rule.Eval ("Test.contains_root", eval_contains_root "")],
31.97 prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
31.98 - [Rule.Eval ("Test.contains'_root", eval_contains_root "")],
31.99 + [Rule.Eval ("Test.contains_root", eval_contains_root "")],
31.100 calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
31.101 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
31.102 @{thm solve_root_equ.simps})]
31.103 @@ -919,7 +919,7 @@
31.104 ("#Find" ,["solutions v_v'i'"])],
31.105 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
31.106 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
31.107 - [Rule.Eval ("Test.precond'_rootmet", eval_precond_rootmet "")],
31.108 + [Rule.Eval ("Test.precond_rootmet", eval_precond_rootmet "")],
31.109 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify},
31.110 @{thm minisubpbl.simps})]
31.111 \<close>
31.112 @@ -950,7 +950,7 @@
31.113 ("#Find" ,["solutions v_v'i'"])],
31.114 {rew_ord'="e_rew_ord",rls'=tval_rls,
31.115 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
31.116 - [Rule.Eval ("Test.contains'_root", eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls,
31.117 + [Rule.Eval ("Test.contains_root", eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls,
31.118 errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], asm_thm=[("square_equation_left", ""),
31.119 ("square_equation_right", "")]*)},
31.120 @{thm solve_root_equ2.simps})]
31.121 @@ -983,7 +983,7 @@
31.122 ("#Find" ,["solutions v_v'i'"])],
31.123 {rew_ord'="e_rew_ord",rls'=tval_rls,
31.124 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
31.125 - [Rule.Eval ("Test.contains'_root", eval_contains_root"")],
31.126 + [Rule.Eval ("Test.contains_root", eval_contains_root"")],
31.127 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,asm_rls=[],
31.128 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
31.129 @{thm solve_root_equ3.simps})]
31.130 @@ -1016,7 +1016,7 @@
31.131 ("#Find" ,["solutions v_v'i'"])],
31.132 {rew_ord'="e_rew_ord",rls'=tval_rls,
31.133 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
31.134 - [Rule.Eval ("Test.contains'_root", eval_contains_root"")],
31.135 + [Rule.Eval ("Test.contains_root", eval_contains_root"")],
31.136 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[],
31.137 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)},
31.138 @{thm solve_root_equ4.simps})]
31.139 @@ -1088,6 +1088,7 @@
31.140 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
31.141 crls = tval_rls, errpats = [], nrls = Test_simplify},
31.142 @{thm test_simplify.simps})]
31.143 +\<close> ML \<open>
31.144 \<close>
31.145
31.146 end
32.1 --- a/src/Tools/isac/Knowledge/Trig.thy Fri May 07 13:23:24 2021 +0200
32.2 +++ b/src/Tools/isac/Knowledge/Trig.thy Fri May 07 18:12:51 2021 +0200
32.3 @@ -1,3 +1,6 @@
32.4 theory Trig imports Base_Tools begin
32.5 -ML \<open>"test"\<close>
32.6 +ML \<open>
32.7 +\<close> ML \<open>
32.8 +\<close> ML \<open>
32.9 +\<close>
32.10 end
32.11 \ No newline at end of file
33.1 --- a/src/Tools/isac/Knowledge/Vect.thy Fri May 07 13:23:24 2021 +0200
33.2 +++ b/src/Tools/isac/Knowledge/Vect.thy Fri May 07 18:12:51 2021 +0200
33.3 @@ -1,3 +1,7 @@
33.4 theory Vect imports Base_Tools begin
33.5
33.6 +ML \<open>
33.7 +\<close> ML \<open>
33.8 +\<close> ML \<open>
33.9 +\<close>
33.10 end
34.1 --- a/src/Tools/isac/MathEngBasic/ctree-basic.sml Fri May 07 13:23:24 2021 +0200
34.2 +++ b/src/Tools/isac/MathEngBasic/ctree-basic.sml Fri May 07 18:12:51 2021 +0200
34.3 @@ -94,7 +94,7 @@
34.4 val get_allpos's : Pos.pos * Pos.posel -> ctree list -> (Pos.pos * Pos.pos_) list
34.5 val cut_bottom : Pos.pos * Pos.posel -> ctree -> (ctree * Pos.pos' list) * bool
34.6 val cut_level : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list
34.7 - val cut_level_'_ : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list
34.8 + val cut_level__ : Pos.pos' list -> Pos.pos -> ctree -> int list * Pos.pos_ -> ctree * Pos.pos' list
34.9 val get_trace : ctree -> int list -> int list -> int list list
34.10 val branch2str : branch -> string
34.11 \<close>
34.12 @@ -586,18 +586,18 @@
34.13 (get_allpos' (p @ [i], i) pt) @ (get_allpos's (p, i + 1) pts);
34.14
34.15 (*WN050106 like cut_level, but deletes exactly 1 node *)
34.16 -fun cut_level_'_ _ _ EmptyPtree _ =raise PTREE "cut_level_'_ Empty _" (* for tests ONLY *)
34.17 - | cut_level_'_ _ _ (Nd ( _, _)) ([], _) = raise PTREE "cut_level_'_ _ []"
34.18 - | cut_level_'_ cuts P (Nd (b, bs)) (p :: [], p_) =
34.19 +fun cut_level__ _ _ EmptyPtree _ =raise PTREE "cut_level__ Empty _" (* for tests ONLY *)
34.20 + | cut_level__ _ _ (Nd ( _, _)) ([], _) = raise PTREE "cut_level__ _ []"
34.21 + | cut_level__ cuts P (Nd (b, bs)) (p :: [], p_) =
34.22 if test_trans b
34.23 then
34.24 (Nd (b, drop_nth [] (p:Pos.posel, bs)),
34.25 cuts @ (if p_ = Frm then [(P @ [p], Res)] else []) @
34.26 (get_allpos's (P, p + 1) (drop_nth [] (p, bs))))
34.27 else (Nd (b, bs), cuts)
34.28 - | cut_level_'_ cuts P (Nd (b, bs)) ((p :: ps), p_) =
34.29 + | cut_level__ cuts P (Nd (b, bs)) ((p :: ps), p_) =
34.30 let
34.31 - val (bs', cuts') = cut_level_'_ cuts P (nth p bs) (ps, p_)
34.32 + val (bs', cuts') = cut_level__ cuts P (nth p bs) (ps, p_)
34.33 in (Nd (b, repl_app bs p bs'), cuts @ cuts') end;
34.34
34.35 fun cut_level _ _ EmptyPtree _ = raise PTREE "cut_level EmptyPtree _"
35.1 --- a/src/Tools/isac/ProgLang/ListC.thy Fri May 07 13:23:24 2021 +0200
35.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Fri May 07 18:12:51 2021 +0200
35.3 @@ -180,4 +180,8 @@
35.4 \<close>
35.5 setup \<open>KEStore_Elems.add_rlss [("prog_expr", (Context.theory_name @{theory}, prog_expr))]\<close>
35.6
35.7 +ML \<open>
35.8 +\<close> ML \<open>
35.9 +\<close> ML \<open>
35.10 +\<close>
35.11 end
36.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Fri May 07 13:23:24 2021 +0200
36.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Fri May 07 18:12:51 2021 +0200
36.3 @@ -25,25 +25,24 @@
36.4 Vars :: "'a => real list" (*get the variables of a term *)
36.5 matches :: "['a, 'a] => bool"
36.6 matchsub :: "['a, 'a] => bool"
36.7 - some'_occur'_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
36.8 - occurs'_in :: "[real , 'a] => bool" ("_ occurs'_in _")
36.9 + some_occur_in :: "[real list, 'a] => bool" ("some'_of _ occur'_in _")
36.10 + occurs_in :: "[real , 'a] => bool" ("_ occurs'_in _")
36.11
36.12 abs :: "real => real" ("(|| _ ||)")
36.13 (* ~~~ FIXXXME Isabelle2002 has abs already !!!*)
36.14 absset :: "real set => real" ("(||| _ |||)")
36.15 (*is numeral constant ?*)
36.16 - is'_const :: "real => bool" ("_ is'_const" 10)
36.17 + is_const :: "real => bool" ("_ is'_const" 10)
36.18 (*is_const rename to is_num FIXXXME.WN.16.5.03 *)
36.19 - is'_atom :: "real => bool" ("_ is'_atom" 10)
36.20 - is'_even :: "real => bool" ("_ is'_even" 10)
36.21 + is_atom :: "real => bool" ("_ is'_atom" 10)
36.22 + is_even :: "real => bool" ("_ is'_even" 10)
36.23
36.24 (* identity on term level*)
36.25 ident :: "['a, 'a] => bool" ("(_ =!=/ _)" [51, 51] 50)
36.26 - argument'_in :: "real => real" ("argument'_in _" 10)
36.27 - sameFunId :: "[real, bool] => bool" (* "same'_funid _ _" 10
36.28 + argument_in :: "real => real" ("argument'_in _" 10)
36.29 + sameFunId :: "[real, bool] => bool" (* "same_funid _ _" 10
36.30 WN0609 changed the id, because ".. _ _" inhibits currying *)
36.31 - filter'_sameFunId:: "[real, bool list] => bool list"
36.32 - ("filter'_sameFunId _ _" 10)
36.33 + filter_sameFunId:: "[real, bool list] => bool list" ("filter'_sameFunId _ _" 10)
36.34 boollist2sum :: "bool list => real"
36.35 lastI :: "'a list \<Rightarrow> 'a"
36.36
36.37 @@ -252,8 +251,8 @@
36.38 (*//------------------------- from Atools.thy------------------------------------------------\\*)
36.39 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
36.40
36.41 -(*("occurs_in", ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""))*)
36.42 -fun eval_occurs_in _ "Prog_Expr.occurs'_in" (p as (Const ("Prog_Expr.occurs'_in",_) $ v $ t)) _ =
36.43 +(*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
36.44 +fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const ("Prog_Expr.occurs_in",_) $ v $ t)) _ =
36.45 ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v));
36.46 tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*)
36.47 if occurs_in v t
36.48 @@ -268,10 +267,10 @@
36.49 let fun occurs_in' a b = occurs_in b a
36.50 in foldl or_ (false, map (occurs_in' t) vs) end;
36.51
36.52 -(*("some_occur_in", ("Prog_Expr.some'_occur'_in",
36.53 +(*("some_occur_in", ("Prog_Expr.some_occur_in",
36.54 eval_some_occur_in "#eval_some_occur_in_"))*)
36.55 -fun eval_some_occur_in _ "Prog_Expr.some'_occur'_in"
36.56 - (p as (Const ("Prog_Expr.some'_occur'_in",_) $ vs $ t)) _ =
36.57 +fun eval_some_occur_in _ "Prog_Expr.some_occur_in"
36.58 + (p as (Const ("Prog_Expr.some_occur_in",_) $ vs $ t)) _ =
36.59 if some_occur_in (TermC.isalist2list vs) t
36.60 then SOME ((UnparseC.term p) ^ " = True",
36.61 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
36.62 @@ -279,8 +278,8 @@
36.63 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
36.64 | eval_some_occur_in _ _ _ _ = NONE;
36.65
36.66 -(*("is_atom",("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
36.67 -fun eval_is_atom (thmid:string) "Prog_Expr.is'_atom"
36.68 +(*("is_atom",("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"))*)
36.69 +fun eval_is_atom (thmid:string) "Prog_Expr.is_atom"
36.70 (t as (Const _ $ arg)) _ =
36.71 (case arg of
36.72 Free (n,_) => SOME (TermC.mk_thmid thmid n "",
36.73 @@ -290,8 +289,8 @@
36.74 | eval_is_atom _ _ _ _ = NONE;
36.75
36.76 fun even i = (i div 2) * 2 = i;
36.77 -(*("is_even",("Prog_Expr.is'_even", eval_is_even "#is_even_"))*)
36.78 -fun eval_is_even (thmid:string) "Prog_Expr.is'_even"
36.79 +(*("is_even",("Prog_Expr.is_even", eval_is_even "#is_even_"))*)
36.80 +fun eval_is_even (thmid:string) "Prog_Expr.is_even"
36.81 (t as (Const _ $ arg)) _ =
36.82 (case arg of
36.83 Free (n,_) =>
36.84 @@ -306,7 +305,7 @@
36.85 | eval_is_even _ _ _ _ = NONE;
36.86
36.87 (*evaluate 'is_const'*)
36.88 -(*("is_const",("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"))*)
36.89 +(*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
36.90 fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ =
36.91 (case arg of
36.92 Const (n1, _) =>
36.93 @@ -452,9 +451,9 @@
36.94 | eval_cancel _ _ _ _ = NONE;
36.95
36.96 (* get the argument from a function-definition *)
36.97 -(*("argument_in" ,("Prog_Expr.argument'_in", Prog_Expr.eval_argument_in "Prog_Expr.argument'_in"))*)
36.98 -fun eval_argument_in _ "Prog_Expr.argument'_in"
36.99 - (t as (Const ("Prog_Expr.argument'_in", _) $ (_(*f*) $ arg))) _ =
36.100 +(*("argument_in" ,("Prog_Expr.argument_in", Prog_Expr.eval_argument_in "Prog_Expr.argument_in"))*)
36.101 +fun eval_argument_in _ "Prog_Expr.argument_in"
36.102 + (t as (Const ("Prog_Expr.argument_in", _) $ (_(*f*) $ arg))) _ =
36.103 if is_Free arg (*could be something to be simplified before*)
36.104 then
36.105 SOME (UnparseC.term t ^ " = " ^ UnparseC.term arg,
36.106 @@ -482,10 +481,10 @@
36.107 fun same_funid f1 (Const ("HOL.eq", _) $ (f2 $ _) $ _) = f1 = f2
36.108 | same_funid f1 t = raise ERROR ("same_funid called with t = ("
36.109 ^ UnparseC.term f1 ^ ") (" ^ UnparseC.term t ^ ")");
36.110 -(*("filter_sameFunId" ,("Prog_Expr.filter'_sameFunId",
36.111 - eval_filter_sameFunId "Prog_Expr.filter'_sameFunId"))*)
36.112 -fun eval_filter_sameFunId _ "Prog_Expr.filter'_sameFunId"
36.113 - (p as Const ("Prog_Expr.filter'_sameFunId",_) $
36.114 +(*("filter_sameFunId" ,("Prog_Expr.filter_sameFunId",
36.115 + eval_filter_sameFunId "Prog_Expr.filter_sameFunId"))*)
36.116 +fun eval_filter_sameFunId _ "Prog_Expr.filter_sameFunId"
36.117 + (p as Const ("Prog_Expr.filter_sameFunId",_) $
36.118 (fid $ _) $ fs) _ =
36.119 let val fs' = ((TermC.list2isalist HOLogic.boolT) o
36.120 (filter (same_funid fid))) (TermC.isalist2list fs)
37.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Fri May 07 13:23:24 2021 +0200
37.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Fri May 07 18:12:51 2021 +0200
37.3 @@ -36,19 +36,19 @@
37.4 consts
37.5 Calculate :: "[char list, 'a] => 'a"
37.6 Rewrite :: "[char list, 'a] => 'a"
37.7 - Rewrite'_Inst:: "[(char list * 'b) list, char list, 'a] => 'a"
37.8 + Rewrite_Inst:: "[(char list * 'b) list, char list, 'a] => 'a"
37.9 ("(Rewrite'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
37.10 - Rewrite'_Set :: "[char list, 'a] => 'a" ("(Rewrite'_Set (_))" 11)
37.11 - Rewrite'_Set'_Inst
37.12 + Rewrite_Set :: "[char list, 'a] => 'a" ("(Rewrite'_Set (_))" 11)
37.13 + Rewrite_Set_Inst
37.14 :: "[((char list) * 'b) list, char list, 'a] => 'a"
37.15 ("(Rewrite'_Set'_Inst (_ _))" 11) (*without last argument ^^ for #>*)
37.16 - Or'_to'_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
37.17 + Or_to_List :: "bool => 'a list" ("Or'_to'_List (_)" 11)
37.18 SubProblem :: "[char list * char list list * char list list, arg list] => 'a"
37.19 Substitute :: "[bool list, 'a] => 'a"
37.20 Take :: "'a => 'a"
37.21
37.22 (* legacy.. *)
37.23 - Check'_elementwise :: (* TODO: is idle, retained for test purposes in Minisubpbl *)
37.24 + Check_elementwise :: (* TODO: is idle, retained for test purposes in Minisubpbl *)
37.25 "['a list, 'b set] => 'a list" ("Check'_elementwise (_ _)" 11)
37.26 Assumptions :: bool (* TODO: remove with making ^^^ idle *)
37.27
37.28 @@ -100,12 +100,12 @@
37.29
37.30 | get_t (Const ("Prog_Tac.Rewrite",_) $ _ $ a) _ = SOME a
37.31 | get_t (Const ("Prog_Tac.Rewrite",_) $ _ ) a = SOME a
37.32 - | get_t (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ $ a) _ = SOME a
37.33 - | get_t (Const ("Prog_Tac.Rewrite'_Inst",_) $ _ $ _ ) a = SOME a
37.34 - | get_t (Const ("Prog_Tac.Rewrite'_Set",_) $ _ $ a) _ = SOME a
37.35 - | get_t (Const ("Prog_Tac.Rewrite'_Set",_) $ _ ) a = SOME a
37.36 - | get_t (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ $a)_ =SOME a
37.37 - | get_t (Const ("Prog_Tac.Rewrite'_Set'_Inst",_) $ _ $ _ ) a =SOME a
37.38 + | get_t (Const ("Prog_Tac.Rewrite_Inst",_) $ _ $ _ $ a) _ = SOME a
37.39 + | get_t (Const ("Prog_Tac.Rewrite_Inst",_) $ _ $ _ ) a = SOME a
37.40 + | get_t (Const ("Prog_Tac.Rewrite_Set",_) $ _ $ a) _ = SOME a
37.41 + | get_t (Const ("Prog_Tac.Rewrite_Set",_) $ _ ) a = SOME a
37.42 + | get_t (Const ("Prog_Tac.Rewrite_Set_Inst",_) $ _ $ _ $a)_ =SOME a
37.43 + | get_t (Const ("Prog_Tac.Rewrite_Set_Inst",_) $ _ $ _ ) a =SOME a
37.44 | get_t (Const ("Prog_Tac.Calculate",_) $ _ $ a) _ = SOME a
37.45 | get_t (Const ("Prog_Tac.Calculate",_) $ _ ) a = SOME a
37.46 | get_t (Const ("Prog_Tac.Substitute",_) $ _ $ a) _ = SOME a
37.47 @@ -130,23 +130,23 @@
37.48 case a of SOME a' => (subst_atomic E (t $ a'))
37.49 | NONE => ((subst_atomic E t) $ v)),
37.50 a)
37.51 - | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Inst"(*1*), _) $ _ $ _ $ _)) =
37.52 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Inst"(*1*), _) $ _ $ _ $ _)) =
37.53 (Program.Tac (subst_atomic E t), NONE)
37.54 - | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Inst"(*2*), _) $ _ $ _)) =
37.55 + | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Inst"(*2*), _) $ _ $ _)) =
37.56 (Program.Tac (
37.57 case a of SOME a' => subst_atomic E (t $ a')
37.58 | NONE => ((subst_atomic E t) $ v)),
37.59 a)
37.60 - | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set"(*1*), _) $ _ $ _)) =
37.61 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Set"(*1*), _) $ _ $ _)) =
37.62 (Program.Tac (subst_atomic E t), NONE)
37.63 - | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Set"(*2*), _) $ _)) =
37.64 + | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Set"(*2*), _) $ _)) =
37.65 (Program.Tac (
37.66 case a of SOME a' => subst_atomic E (t $ a')
37.67 | NONE => ((subst_atomic E t) $ v)),
37.68 a)
37.69 - | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*1*), _) $ _ $ _ $ _)) =
37.70 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Rewrite_Set_Inst"(*1*), _) $ _ $ _ $ _)) =
37.71 (Program.Tac (subst_atomic E t), NONE)
37.72 - | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite'_Set'_Inst"(*2*), _) $ _ $ _)) =
37.73 + | eval_leaf E a v (t as (Const ("Prog_Tac.Rewrite_Set_Inst"(*2*), _) $ _ $ _)) =
37.74 (Program.Tac (
37.75 case a of SOME a' => subst_atomic E (t $ a')
37.76 | NONE => ((subst_atomic E t) $ v)),
37.77 @@ -158,16 +158,16 @@
37.78 case a of SOME a' => subst_atomic E (t $ a')
37.79 | NONE => ((subst_atomic E t) $ v)),
37.80 a)
37.81 - | eval_leaf E _ _ (t as (Const ("Prog_Tac.Check'_elementwise"(*1*),_) $ _ $ _)) =
37.82 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Check_elementwise"(*1*),_) $ _ $ _)) =
37.83 (Program.Tac (subst_atomic E t), NONE)
37.84 - | eval_leaf E a v (t as (Const ("Prog_Tac.Check'_elementwise"(*2*), _) $ _)) =
37.85 + | eval_leaf E a v (t as (Const ("Prog_Tac.Check_elementwise"(*2*), _) $ _)) =
37.86 (Program.Tac (
37.87 case a of SOME a' => subst_atomic E (t $ a')
37.88 | NONE => ((subst_atomic E t) $ v)),
37.89 a)
37.90 - | eval_leaf E _ _ (t as (Const ("Prog_Tac.Or'_to'_List"(*1*), _) $ _)) =
37.91 + | eval_leaf E _ _ (t as (Const ("Prog_Tac.Or_to_List"(*1*), _) $ _)) =
37.92 (Program.Tac (subst_atomic E t), NONE)
37.93 - | eval_leaf E a v (t as (Const ("Prog_Tac.Or'_to'_List"(*2*), _))) = (*t $ v*)
37.94 + | eval_leaf E a v (t as (Const ("Prog_Tac.Or_to_List"(*2*), _))) = (*t $ v*)
37.95 (Program.Tac (
37.96 case a of SOME a' => subst_atomic E (t $ a')
37.97 | NONE => ((subst_atomic E t) $ v)),
38.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri May 07 13:23:24 2021 +0200
38.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri May 07 18:12:51 2021 +0200
38.3 @@ -73,19 +73,22 @@
38.4 text\<open>\noindent We try to apply the rules to a given expression.\<close>
38.5
38.6 ML \<open>
38.7 - val inverse_Z = Rule_Set.append_rules "inverse_Z" Rule_Set.empty
38.8 - [ Thm ("rule3",ThmC.numerals_to_Free @{thm rule3}),
38.9 - Thm ("rule4",ThmC.numerals_to_Free @{thm rule4}),
38.10 - Thm ("rule1",ThmC.numerals_to_Free @{thm rule1})
38.11 + val inverse_Z = Rule_Set.append_rules "inverse_Z" Atools_erls
38.12 + [ Rule.Thm ("rule3",ThmC.numerals_to_Free @{thm rule3}),
38.13 + Rule.Thm ("rule4",ThmC.numerals_to_Free @{thm rule4}),
38.14 + Rule.Thm ("rule1",ThmC.numerals_to_Free @{thm rule1})
38.15 ];
38.16
38.17 +\<close> ML \<open>
38.18 val t = TermC.str2term "z / (z - 1) + z / (z - \<alpha>) + 1";
38.19 +\<close> ML \<open>
38.20 val SOME (t', asm) = Rewrite.rewrite_set_ thy true inverse_Z t;
38.21 UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
38.22 (*
38.23 * Attention rule1 is applied before the expression is
38.24 * checked for rule4 which would be correct!!!
38.25 *)
38.26 +\<close> ML \<open>
38.27 \<close>
38.28
38.29 ML \<open>val (thy, ro, er) = (@{theory}, tless_true, eval_rls);\<close>
39.1 --- a/test/Tools/isac/BaseDefinitions/libraryC.sml Fri May 07 13:23:24 2021 +0200
39.2 +++ b/test/Tools/isac/BaseDefinitions/libraryC.sml Fri May 07 18:12:51 2021 +0200
39.3 @@ -81,7 +81,7 @@
39.4 > val t = (Thm.term_of o the o (TermC.parse thy))
39.5 "solve_univar (R, [univar, equation], no_met) (a = b + #1) a";
39.6 > ids_of t;
39.7 -["solve'_univar", "Product_Type.Pair", "R", "Cons", "univar", "equation", "Nil",...]*)
39.8 +["solve_univar", "Product_Type.Pair", "R", "Cons", "univar", "equation", "Nil",...]*)
39.9
39.10 "----------- fun overwritel --------------------------------------------------------------------";
39.11 "----------- fun overwritel --------------------------------------------------------------------";
40.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Fri May 07 13:23:24 2021 +0200
40.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Fri May 07 18:12:51 2021 +0200
40.3 @@ -331,13 +331,6 @@
40.4 if TermC.matches thy tm pa then error "termC.sml diff.behav. in TermC.matches false 4"
40.5 else ();
40.6
40.7 -"----------- fun TermC.matches, repair 'Handler catches all exceptions' ------------------------------";
40.8 -"----------- fun TermC.matches, repair 'Handler catches all exceptions' ------------------------------";
40.9 -"----------- fun TermC.matches, repair 'Handler catches all exceptions' ------------------------------";
40.10 -
40.11 -
40.12 -
40.13 -
40.14 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------";
40.15 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------";
40.16 "----------- fun TermC.parse, fun TermC.parse_patt, fun T_a2real -------------------------------------------";
41.1 --- a/test/Tools/isac/BridgeLibisabelle/interface.sml Fri May 07 13:23:24 2021 +0200
41.2 +++ b/test/Tools/isac/BridgeLibisabelle/interface.sml Fri May 07 18:12:51 2021 +0200
41.3 @@ -85,7 +85,7 @@
41.4 writeln(pr_ctree pr_short pt);
41.5 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
41.6 ###########################################################################*)
41.7 -val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm); (*#*)
41.8 +val (pt, _) = cut_level__ [] [] pt ([4,1],Frm); (*#*)
41.9 (*##########################################################################*)
41.10 writeln(pr_ctree pr_short pt);
41.11 (*##########################################################################
42.1 --- a/test/Tools/isac/Interpret/error-pattern.sml Fri May 07 13:23:24 2021 +0200
42.2 +++ b/test/Tools/isac/Interpret/error-pattern.sml Fri May 07 18:12:51 2021 +0200
42.3 @@ -1044,7 +1044,7 @@
42.4 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
42.5 | _ => error "inform: uncovered case of MethodC.from_store"
42.6 ;
42.7 -(*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)\", \"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\", \"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\", \"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\", \"d_d ?bdv (E_ \<up> ?u) = E_ \<up> ?u * d_d ?x ?u\"]]"
42.8 +(*+*)if Error_Pattern.s_to_string errpats = "[(\"chain-rule-diff-both\",\n[\"d_d ?bdv (sin ?u) = cos (d_d ?bdv ?u)\", \"d_d ?bdv (cos ?u) = - sin (d_d ?bdv ?u)\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1)\", \"d_d ?bdv (LogExp.ln ?u) = 1 / ?u\", \"d_d ?bdv (LogExp.ln ?u) = 1 / d_d ?bdv ?u\"],\n[\"d_d ?bdv (sin ?u) = cos ?u * d_d ?bdv ?u\", \"d_d ?bdv (cos ?u) = - sin ?u * d_d ?bdv ?u\", \"d_d ?bdv (?u \<up> ?n) = ?n * ?u \<up> (?n - 1) * d_d ?bdv ?u\", \"d_d ?bdv (LogExp.ln ?u) = d_d ?bdv ?u / ?u\", \"d_d ?bdv (exp ?u) = exp ?u * d_d ?x ?u\"]]"
42.9 (*+*)then () else error "inform with (positive) Error_Pattern.check_for broken 3";
42.10
42.11 val {env, ...} = Ctree.get_istate_LI pt pos |> Istate.the_pstate
43.1 --- a/test/Tools/isac/Interpret/li-tool.sml Fri May 07 13:23:24 2021 +0200
43.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Fri May 07 18:12:51 2021 +0200
43.3 @@ -160,7 +160,7 @@
43.4 (*
43.5 > val str = "Rewrite_Set_Inst";
43.6 > val esc = esc_underscore str;
43.7 -val it = "Rewrite'_Set'_Inst" : string
43.8 +val it = "Rewrite_Set_Inst" : string
43.9 > val des = de_esc_underscore esc;
43.10 val des = de_esc_underscore esc;*)
43.11
44.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Fri May 07 13:23:24 2021 +0200
44.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Fri May 07 18:12:51 2021 +0200
44.3 @@ -67,7 +67,7 @@
44.4 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
44.5 Eval("Prog_Expr.lhs", eval_lhs "eval_lhs_"),
44.6 Eval("Prog_Expr.rhs", eval_rhs "eval_rhs_"),
44.7 - Eval("Prog_Expr.argument'_in", eval_argument_in "Prog_Expr.argument'_in")
44.8 + Eval("Prog_Expr.argument_in", eval_argument_in "Prog_Expr.argument_in")
44.9 ],
44.10 scr = Empty_Prog};
44.11 val rm_ = TermC.str2term"[M_b 0 = 0, M_b L = 0]";
45.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Fri May 07 13:23:24 2021 +0200
45.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Fri May 07 18:12:51 2021 +0200
45.3 @@ -44,35 +44,35 @@
45.4 then () else error "eqsystem.sml occur_exactly_in 3";
45.5
45.6 val t = TermC.str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
45.7 -eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
45.8 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
45.9 +eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
45.10 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
45.11 if str = "[c, c_2] from [c, c_2,\n" ^
45.12 " c_3] occur_exactly_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = True"
45.13 then () else error "eval_occur_exactly_in [c, c_2]";
45.14
45.15 val t = TermC.str2term ("[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in " ^
45.16 "-1 * q_0 * L \<up> 2 / 2 + L * c + c_2");
45.17 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
45.18 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
45.19 if str = "[c, c_2,\n c_3] from [c, c_2,\n" ^
45.20 " c_3] occur_exactly_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
45.21 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
45.22
45.23 val t = TermC.str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
45.24 \-1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
45.25 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
45.26 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
45.27 if str = "[c_2] from [c, c_2,\n" ^
45.28 " c_3] occur_exactly_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False"
45.29 then () else error "eval_occur_exactly_in [c, c_2, c_3]";
45.30
45.31 val t = TermC.str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
45.32 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
45.33 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
45.34 if str = "[] from [c, c_2, c_3] occur_exactly_in 0 = True" then ()
45.35 else error "eval_occur_exactly_in [c, c_2, c_3]";
45.36
45.37 val t =
45.38 TermC.str2term
45.39 "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) /2";
45.40 -val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
45.41 +val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur_exactly_in" t 0;
45.42 if str = "[] from [c, c_2, c_3, c_4] occur_exactly_in \
45.43 \-1 * (q_0 * L \<up> 2) / 2 = True" then ()
45.44 else error "eval_occur_exactly_in [c, c_2, c_3, c_4]";
45.45 @@ -112,7 +112,7 @@
45.46 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
45.47 Thm ("TL_CONS",ThmC.numerals_to_Free @{thm tl_Cons}),
45.48 Thm ("TL_NIL",ThmC.numerals_to_Free @{thm tl_Nil}),
45.49 - Eval ("EqSystem.occur'_exactly'_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
45.50 + Eval ("EqSystem.occur_exactly_in", eval_occur_exactly_in "#eval_occur_exactly_in_")
45.51 ]) t;
45.52 if t = @{term True} then ()
45.53 else error "eqsystem.sml ..occur_exactly_in (nth_ 1 [c_4..";
45.54 @@ -802,7 +802,7 @@
45.55
45.56 "----- outcommented before Isabelle2002 --> 2011 -------------------------";
45.57 (*-----------------------------------vvvWN080102 Exception- Match raised
45.58 - since associate Rewrite .. Rewrite'_Set
45.59 + since associate Rewrite .. Rewrite_Set
45.60 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
45.61
45.62 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
45.63 @@ -937,7 +937,7 @@
45.64 \ 0 = c_2, \
45.65 \ 0 = (2 * c_2 + 2 * L * c + -1 * L \<up> 2 * q_0) / 2]";
45.66 (*vvvWN080102 Exception- Match raised
45.67 - since associate Rewrite .. Rewrite'_Set
45.68 + since associate Rewrite .. Rewrite_Set
45.69 "------------------------------------------- simplify_System_parenthesized...";
45.70 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
45.71 "[0 = c_4, \
46.1 --- a/test/Tools/isac/Knowledge/integrate.sml Fri May 07 13:23:24 2021 +0200
46.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Fri May 07 18:12:51 2021 +0200
46.3 @@ -36,7 +36,7 @@
46.4 erls = Rule_Set.Empty,
46.5 srls = Rule_Set.Empty, calc = [], errpatts = [],
46.6 rules = [(*for rewriting conditions in Thm's*)
46.7 - Eval ("Prog_Expr.occurs'_in",
46.8 + Eval ("Prog_Expr.occurs_in",
46.9 eval_occurs_in "#occurs_in_"),
46.10 Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
46.11 Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})],
46.12 @@ -59,7 +59,7 @@
46.13 | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";
46.14
46.15 val t = str2t "ff x is_f_x";
46.16 -case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
46.17 +case t of Const ("Integrate.is_f_x", _) $ _ => ()
46.18 | _ => error "integrate.sml: parsing: ff x is_f_x";
46.19
46.20
46.21 @@ -97,11 +97,11 @@
46.22 val cc = new_c term;
46.23 if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
46.24
46.25 -val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
46.26 +val SOME (id,t') = eval_add_new_c "" "Integrate.add_new_c" term thy;
46.27 if UnparseC.term t' = "x \<up> 2 * c + c_2 = x \<up> 2 * c + c_2 + c_3" then ()
46.28 else error "intergrate.sml: diff. eval_add_new_c";
46.29
46.30 -val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
46.31 +val cc = ("Integrate.add_new_c", eval_add_new_c "add_new_c_");
46.32 val SOME (thmstr, thm) = adhoc_thm1_ thy cc term;
46.33
46.34 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
46.35 @@ -147,7 +147,7 @@
46.36 erls = Rule_Set.Empty,
46.37 srls = Rule_Set.Empty, calc = [], errpatts = [],
46.38 rules = [Eval ("Prog_Expr.matches",eval_matches ""),
46.39 - Eval ("Integrate.is'_f'_x",
46.40 + Eval ("Integrate.is_f_x",
46.41 eval_is_f_x "is_f_x_"),
46.42 Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
46.43 Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
47.1 --- a/test/Tools/isac/Knowledge/poly.sml Fri May 07 13:23:24 2021 +0200
47.2 +++ b/test/Tools/isac/Knowledge/poly.sml Fri May 07 18:12:51 2021 +0200
47.3 @@ -339,13 +339,13 @@
47.4 val t = TermC.str2term "x \<up> 2 * x";
47.5 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
47.6 if UnparseC.term t' = "x * x \<up> 2" then ()
47.7 -else error "poly.sml Poly.is'_multUnordered doesn't work";
47.8 +else error "poly.sml Poly.is_multUnordered doesn't work";
47.9
47.10 (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
47.11 ### rls: order_mult_ on: 5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +
47.12 (-48 * x \<up> 4 + 8))
47.13 ###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
47.14 -####### try calc: Poly.is'_multUnordered'
47.15 +####### try calc: Poly.is_multUnordered'
47.16 ======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
47.17 *)
47.18 val t = TermC.str2term "5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) + (-48 * x \<up> 4 + 8))";
47.19 @@ -363,7 +363,7 @@
47.20 case eval_is_multUnordered "testid" "" tm thy of
47.21 SOME (_, Const ("HOL.Trueprop", _) $
47.22 (Const ("HOL.eq", _) $
47.23 - (Const ("Poly.is'_multUnordered", _) $ _) $
47.24 + (Const ("Poly.is_multUnordered", _) $ _) $
47.25 Const ("HOL.True", _))) => ()
47.26 | _ => error "poly.sml diff. eval_is_multUnordered";
47.27
48.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Fri May 07 13:23:24 2021 +0200
48.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Fri May 07 18:12:51 2021 +0200
48.3 @@ -567,7 +567,7 @@
48.4
48.5 "--- does the respective prls rewrite ?";
48.6 val prls = Rule_Set.append_rules "prls_pbl_vereinf_poly" Rule_Set.empty
48.7 - [Eval ("Poly.is'_polyexp", eval_is_polyexp ""),
48.8 + [Eval ("Poly.is_polyexp", eval_is_polyexp ""),
48.9 Eval ("Prog_Expr.matchsub", eval_matchsub ""),
48.10 Thm ("or_true",@{thm or_true}),
48.11 (*"(?a | True) = True"*)
49.1 --- a/test/Tools/isac/Knowledge/rateq.sml Fri May 07 13:23:24 2021 +0200
49.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Fri May 07 18:12:51 2021 +0200
49.3 @@ -122,7 +122,7 @@
49.4 (thy, ptp, E, (up@[R,D]), body, a, v);
49.5 "~~~~~ fun check_leaf, args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t);
49.6 "~~~~~ fun eval_leaf, args:"; val (E, a, v,
49.7 - (t as (Const ("Prog_Tac.Check'_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
49.8 + (t as (Const ("Prog_Tac.Check_elementwise",_) $ _ $ _ ))) = (E, a, v, t);
49.9 val Program.Tac tm = Program.Tac (subst_atomic E t);
49.10 UnparseC.term tm = "Check_elementwise [x = 1 / 5] {v_v. Assumptions}";
49.11 (* ------ \<up> ----- ? "x" ?*)
50.1 --- a/test/Tools/isac/MathEngBasic/ctree.sml Fri May 07 13:23:24 2021 +0200
50.2 +++ b/test/Tools/isac/MathEngBasic/ctree.sml Fri May 07 18:12:51 2021 +0200
50.3 @@ -731,7 +731,7 @@
50.4 writeln(pr_ctree pr_short pt);
50.5 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]:
50.6 ###########################################################################*)
50.7 -val (pt, ppp) = cut_level_'_ [] [] pt ([4,1],Frm);
50.8 +val (pt, ppp) = cut_level__ [] [] pt ([4,1],Frm);
50.9 writeln(pr_ctree pr_short pt);
50.10
50.11
51.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml Fri May 07 13:23:24 2021 +0200
51.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Fri May 07 18:12:51 2021 +0200
51.3 @@ -287,7 +287,7 @@
51.4 val SOME (t,_) =
51.5 rewrite_inst_ thy e_rew_ord
51.6 (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
51.7 - [(Eval ("EqSystem.occur'_exactly'_in",
51.8 + [(Eval ("EqSystem.occur_exactly_in",
51.9 eval_occur_exactly_in
51.10 "#eval_occur_exactly_in_"))
51.11 ])
51.12 @@ -353,7 +353,7 @@
51.13 val pres = [TermC.parse_patt thy "?p is_multUnordered"];
51.14 val prepat = [(pres, pat)];
51.15 val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
51.16 - [Eval ("Poly.is'_multUnordered",
51.17 + [Eval ("Poly.is_multUnordered",
51.18 eval_is_multUnordered "")];
51.19
51.20 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
51.21 @@ -376,7 +376,7 @@
51.22 case eval_is_multUnordered "testid" "" tm thy of
51.23 SOME (_, Const ("HOL.Trueprop", _) $
51.24 (Const ("HOL.eq", _) $
51.25 - (Const ("Poly.is'_multUnordered", _) $ _) $
51.26 + (Const ("Poly.is_multUnordered", _) $ _) $
51.27 Const ("HOL.True", _))) => ()
51.28 | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
51.29
51.30 @@ -384,7 +384,7 @@
51.31 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
51.32 tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
51.33 if UnparseC.term t' = "x * x \<up> 2" then ()
51.34 -else error "rewrite.sml Poly.is'_multUnordered doesn't work";
51.35 +else error "rewrite.sml Poly.is_multUnordered doesn't work";
51.36
51.37 (* for achieving the previous result, the following code was taken apart *)
51.38 "----- rewrite__set_ ---";
51.39 @@ -607,7 +607,7 @@
51.40 (*+*) Thm ("not_false", "(\<not> False) = True"),
51.41 (*+*) :
51.42 (*+*) Eval ("Transcendental.powr", fn),
51.43 -(*+*) Eval ("RatEq.is'_ratequation'_in", fn)]:
51.44 +(*+*) Eval ("RatEq.is_ratequation_in", fn)]:
51.45 (*+*) rule list*)
51.46 (*+*)chk: term list -> term list -> term list * bool
51.47
52.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Fri May 07 13:23:24 2021 +0200
52.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method.sml Fri May 07 18:12:51 2021 +0200
52.3 @@ -76,7 +76,7 @@
52.4 val Associated (Rewrite_Set' _, _, _) = (*case*)
52.5 associate pt ctxt (m, stac) (*of*);
52.6 "~~~~~ fun associate, args:"; val (_, ctxt, (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', _))),
52.7 - (Const ("Prog_Tac.Rewrite'_Set", _) $ rls_ $ f_)) = (pt, ctxt, m, stac);
52.8 + (Const ("Prog_Tac.Rewrite_Set", _) $ rls_ $ f_)) = (pt, ctxt, m, stac);
52.9
52.10 (*+*)if Rule_Set.id rls = HOLogic.dest_string rls_ then () else error "Prog_Tac.associate changed";
52.11
53.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Fri May 07 13:23:24 2021 +0200
53.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Fri May 07 18:12:51 2021 +0200
53.3 @@ -89,7 +89,7 @@
53.4
53.5 val Check_elementwise "Assumptions" =
53.6 LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) stac;
53.7 -"~~~~~ fun tac_from_prog , args:"; val (pt, thy, (Const("Prog_Tac.Check'_elementwise",_) $ _ $
53.8 +"~~~~~ fun tac_from_prog , args:"; val (pt, thy, (Const("Prog_Tac.Check_elementwise",_) $ _ $
53.9 (set as Const ("Set.Collect",_) $ Abs (_,_,pred))))
53.10 = (pt, (Proof_Context.theory_of ctxt), stac);
53.11
54.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Fri May 07 13:23:24 2021 +0200
54.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Fri May 07 18:12:51 2021 +0200
54.3 @@ -61,7 +61,7 @@
54.4 [("#Given" ,["equality e_e", "solveFor v_v"]),
54.5 ("#Where" ,["is_rootequation_in (e_e::bool) (v_::real)"]),
54.6 ("#Find" ,["solutions v_i_"])],
54.7 - Rule_Set.append_rules Rule_Set.empty [Eval ("Test.is'_rootequation'_in", eval_is_rootequation_in "")],
54.8 + Rule_Set.append_rules Rule_Set.empty [Eval ("Test.is_rootequation_in", eval_is_rootequation_in "")],
54.9 [("Test", "methode")])]
54.10 thy;
54.11
55.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Fri May 07 13:23:24 2021 +0200
55.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
55.3 @@ -1,481 +0,0 @@
55.4 -(* use"../systest/scriptnew.sml";
55.5 - use"systest/scriptnew.sml";
55.6 - use"scriptnew.sml";
55.7 - *)
55.8 -
55.9 -(*contents*)
55.10 -" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
55.11 -" --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
55.12 -" --- test 11.5.02 Testeq: let e_e =... in [e_] ------------------ ";
55.13 -" _________________ me + nxt_step from script ___________________ ";
55.14 -" _________________ me + sqrt-equ-test: 1.norm_equation ________ ";
55.15 -" _________________ equation with x =(-12)/5, but L ={} ------- ";
55.16 -"------------------ script with Map, Subst (biquadr.equ.)---------";
55.17 -(*contents*)
55.18 -
55.19 -
55.20 -
55.21 -
55.22 -" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
55.23 -" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
55.24 -" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
55.25 -KEStore_Elems.add_pbts
55.26 - [Problem.prep_input Test.thy "pbl_testss" [] Problem.id_empty
55.27 - (["tests"], []:(string * string list) list, Rule_Set.empty, NONE, []),
55.28 - Problem.prep_input Test.thy "pbl_testss_term" [] Problem.id_empty
55.29 - (["met_testterm", "tests"],
55.30 - [("#Given" ,["realTestGiven g_"]),
55.31 - ("#Find" ,["realTestFind f_"])],
55.32 - Rule_Set.empty, NONE, [])]
55.33 - thy;
55.34 -
55.35 -store_met
55.36 - (MethodC.prep_input Test.thy "met_test_simp" [] e_metID
55.37 - (*test for simplification*)
55.38 - (["Test", "met_testterm"]:metID,
55.39 - [("#Given" ,["realTestGiven g_"]),
55.40 - ("#Find" ,["realTestFind f_"])
55.41 - ],
55.42 - {rew_ord'="tless_true",rls'=tval_rls,srls=Rule_Set.empty,prls=Rule_Set.empty,calc=[],
55.43 - crls=tval_rls, errpats = [], nrls=Rule_Set.empty(*,
55.44 - asm_rls=[],asm_thm=[]*)},
55.45 - "Program Testterm (g_::real) = \
55.46 - \Repeat\
55.47 - \ ((Repeat (Rewrite rmult_1)) Or\
55.48 - \ (Repeat (Rewrite rmult_0)) Or\
55.49 - \ (Repeat (Rewrite radd_0))) g_"
55.50 - ));
55.51 -val fmz = ["realTestGiven ((0+0)*(1*(1*a)))", "realTestFind F"];
55.52 -val (dI',pI',mI') = ("Test",["met_testterm", "tests"],
55.53 - ["Test", "met_testterm"]);
55.54 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
55.55 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.56 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.57 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.58 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.59 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.60 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.61 -(*val nxt = ("Apply_Method",Apply_Method ("Test", "met_testterm"))*)
55.62 -(*----script 111 ------------------------------------------------*)
55.63 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.64 -(*"(#0 + #0) * (#1 * (#1 * a))" nxt= Rewrite ("rmult_1",*)
55.65 -(*----script 222 ------------------------------------------------*)
55.66 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.67 -(*"(#0 + #0) * (#1 * a)" nxt= Rewrite ("rmult_1",*)
55.68 -(*----script 333 ------------------------------------------------*)
55.69 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.70 -(*"(#0 + #0) * a" nxt= Rewrite ("radd_0",*)
55.71 -(*----script 444 ------------------------------------------------*)
55.72 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.73 -(*"#0 * a"*)
55.74 -(*----script 555 ------------------------------------------------*)
55.75 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.76 -(*"#0"*)
55.77 -if p=([4],Res) then ()
55.78 -else error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p));
55.79 -(*----script 666 ------------------------------------------------*)
55.80 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.81 -(*"#0"*)
55.82 -if nxt=("End_Proof'",End_Proof') then ()
55.83 -else error "new behaviour in 30.4.02 Testterm: End_Proof";
55.84 -
55.85 -
55.86 -
55.87 -
55.88 -
55.89 -" --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
55.90 -" --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
55.91 -" --- test 9.5.02 Testeq: While Try Repeat #> ------------------ ";
55.92 -KEStore_Elems.add_pbts
55.93 - [Problem.prep_input Test.thy "pbl_testss_eq" [] Problem.id_empty
55.94 - (["met_testeq", "tests"],
55.95 - [("#Given" ,["boolTestGiven e_e"]),
55.96 - ("#Find" ,["boolTestFind v_i_"])],
55.97 - Rule_Set.empty, NONE, [])]
55.98 - thy;
55.99 -
55.100 -store_met
55.101 - (MethodC.prep_input Test.thy "met_test_eq1" [] e_metID
55.102 - (["Test", "testeq1"]:metID,
55.103 - [("#Given",["boolTestGiven e_e"]),
55.104 - ("#Where" ,[]),
55.105 - ("#Find" ,["boolTestFind v_i_"])
55.106 - ],
55.107 - {rew_ord'="tless_true",rls'=tval_rls,
55.108 - srls=Rule_Set.append_rules "testeq1_srls" Rule_Set.empty
55.109 - [Eval ("Test.contains'_root", eval_contains_root"")],
55.110 - prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls=Rule_Set.empty
55.111 - (*,asm_rls=[],asm_thm=[("square_equation_left", "")]*)},
55.112 - "Program Testeq (e_e::bool) = \
55.113 - \(While (contains_root e_e) Do \
55.114 - \((Try (Repeat (Rewrite rroot_square_inv))) #> \
55.115 - \ (Try (Repeat (Rewrite square_equation_left))) #> \
55.116 - \ (Try (Repeat (Rewrite radd_0)))))\
55.117 - \ e_e"
55.118 - ));
55.119 -
55.120 -val fmz = ["boolTestGiven (0+(sqrt(sqrt(sqrt a)) \<up> 2) \<up> 2=0)",
55.121 - "boolTestFind v_i_"];
55.122 -val (dI',pI',mI') = ("Test",["met_testeq", "tests"],
55.123 - ["Test", "testeq1"]);
55.124 -val Prog sc = (#scr o MethodC.from_store) ["Test", "testeq1"];
55.125 -atomt sc;
55.126 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
55.127 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.128 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.129 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.130 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.131 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.132 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.133 -(*val nxt = ("Apply_Method",Apply_Method ("Test", "testeq1")) *)
55.134 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.135 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.136 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.137 -(*val f = Form' (Test_Out.FormKF (~1,EdUndef,1,Nundef,"#0 + sqrt a = #0"))
55.138 -val nxt = ("Rewrite",Rewrite ("radd_0", "#0 + ?k = ?k"))*)
55.139 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.140 -
55.141 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.142 -(*** No such constant: "Test.contains'_root" *)
55.143 -
55.144 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.145 -if f=(Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"a = 0 \<up> 2"))) andalso
55.146 - nxt=("End_Proof'",End_Proof') then ()
55.147 -else error "different behaviour test 9.5.02 Testeq: While Try Repeat #>";
55.148 -
55.149 -
55.150 -
55.151 -
55.152 -" --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";
55.153 -" --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";
55.154 -" --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";
55.155 -store_met
55.156 - (MethodC.prep_input Test.thy "met_test_let" [] e_metID
55.157 - (["Test", "testlet"]:metID,
55.158 - [("#Given",["boolTestGiven e_e"]),
55.159 - ("#Where" ,[]),
55.160 - ("#Find" ,["boolTestFind v_i_"])
55.161 - ],
55.162 - {rew_ord'="tless_true",rls'=tval_rls,
55.163 - srls=Rule_Set.append_rules "testlet_srls" Rule_Set.empty
55.164 - [Eval ("Test.contains'_root",eval_contains_root"")],
55.165 - prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls=Rule_Set.empty
55.166 - (*,asm_rls=[],asm_thm=[("square_equation_left", "")]*)},
55.167 - "Program Testeq2 (e_e::bool) = \
55.168 - \(let e_e =\
55.169 - \ ((While (contains_root e_e) Do \
55.170 - \ (Rewrite square_equation_left True))\
55.171 - \ e_e)\
55.172 - \in [e_::bool])"
55.173 - ));
55.174 -val Prog sc = (#scr o MethodC.from_store) ["Test", "testlet"];
55.175 -writeln(UnparseC.term sc);
55.176 -val fmz = ["boolTestGiven (sqrt a = 0)",
55.177 - "boolTestFind v_i_"];
55.178 -val (dI',pI',mI') = ("Test",["met_testeq", "tests"],
55.179 - ["Test", "testlet"]);
55.180 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
55.181 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.182 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.183 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.184 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.185 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.186 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.187 -(*val nxt = ("Apply_Method",Apply_Method ("Test", "testlet"))*)
55.188 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.189 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.190 -val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
55.191 -if f=(Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[a = 0 \<up> 2]"))) andalso
55.192 - nxt=("End_Proof'",End_Proof') then ()
55.193 -else error "different behaviour in test 11.5.02 Testeq: let e_e =... in [e_]";
55.194 -
55.195 -
55.196 -
55.197 -
55.198 -" _________________ me + nxt_step from script _________________ ";
55.199 -" _________________ me + nxt_step from script _________________ ";
55.200 -" _________________ me + nxt_step from script _________________ ";
55.201 -val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
55.202 - "solveFor x", "solutions L"];
55.203 -val (dI',pI',mI') =
55.204 - ("Test",["sqroot-test", "univariate", "equation", "test"],
55.205 - ["Test", "sqrt-equ-test"]);
55.206 -val Prog sc = (#scr o MethodC.from_store) ["Test", "sqrt-equ-test"];
55.207 -writeln(UnparseC.term sc);
55.208 -
55.209 -"--- s1 ---";
55.210 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
55.211 -"--- s2 ---";
55.212 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.213 -(* val nxt =
55.214 - ("Add_Given",
55.215 - Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)
55.216 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.217 -"--- s3 ---";
55.218 -(* val nxt = ("Add_Given",Add_Given "solveFor x");*)
55.219 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.220 -"--- s4 ---";
55.221 -(* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)
55.222 -"--- s5 ---";
55.223 -(* val nxt = ("Add_Find",Add_Find "solutions L");*)
55.224 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.225 -"--- s6 ---";
55.226 -(* val nxt = ("Specify_Theory",Specify_Theory "Test");*)
55.227 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.228 -"--- s7 ---";
55.229 -(* val nxt =
55.230 - ("Specify_Problem",
55.231 - Specify_Problem ["sqroot-test", "univariate", "equation", "test"]);*)
55.232 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.233 -"--- s8 ---";
55.234 -(* val nxt = ("Specify_Method",Specify_Method ("Test", "sqrt-equ-test"));*)
55.235 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.236 -"--- s9 ---";
55.237 -(* val nxt = ("Apply_Method",Apply_Method ("Test", "sqrt-equ-test"));*)
55.238 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.239 -"--- 1 ---";
55.240 -(* val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));*)
55.241 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.242 -"--- 2 ---";
55.243 -(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
55.244 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.245 -"--- 3 ---";
55.246 -(* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)
55.247 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.248 -"--- 4 ---";
55.249 -(* val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");*)
55.250 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.251 -"--- 5 ---";
55.252 -(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
55.253 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.254 -"--- 6 ---";
55.255 -(* val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));*)
55.256 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.257 -"--- 7 ---";
55.258 -(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
55.259 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.260 -"--- 8<> ---";
55.261 -(* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)
55.262 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.263 -"--- 9<> ---";
55.264 -(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
55.265 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.266 -"--- 10<> ---";
55.267 -(* val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");*)
55.268 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.269 -"--- 11<> ---";
55.270 -(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
55.271 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.272 -"--- 12<> ---.";
55.273 -(* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv"));*)
55.274 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.275 -"--- 13<> ---";
55.276 -(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
55.277 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.278 -"--- 14<> ---";
55.279 -(* nxt = ("Check_Postcond",Check_Postcond ("Test", "sqrt-equ-test"));*)
55.280 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.281 -if f<>(Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
55.282 -then error "scriptnew.sml 1: me + tacs from script: new behaviour"
55.283 -else ();
55.284 -"--- 15<> ---";
55.285 -(* val nxt = ("End_Proof'",End_Proof');*)
55.286 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.287 -
55.288 -writeln (pr_ctree pr_short pt);
55.289 -writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^
55.290 -"\n=============================================================");
55.291 -(*get_obj g_asm pt [];
55.292 -val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*)
55.293 -
55.294 -
55.295 -
55.296 -
55.297 -
55.298 -" _________________ me + sqrt-equ-test: 1.norm_equation _________________ ";
55.299 -" _________________ me + sqrt-equ-test: 1.norm_equation _________________ ";
55.300 -" _________________ me + sqrt-equ-test: 1.norm_equation _________________ ";
55.301 -val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
55.302 - "solveFor x", "errorBound (eps=0)",
55.303 - "solutions L"];
55.304 -val (dI',pI',mI') =
55.305 - ("Test",["sqroot-test", "univariate", "equation", "test"],
55.306 - ["Test", "sqrt-equ-test"]);
55.307 - val Prog sc = (#scr o MethodC.from_store) ["Test", "sqrt-equ-test"];
55.308 - (writeln o UnparseC.term) sc;
55.309 -"--- s1 ---";
55.310 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
55.311 -"--- s2 ---";
55.312 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.313 -(* val nxt = ("Add_Given",
55.314 - Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)
55.315 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.316 -"--- s3 ---";
55.317 -(* val nxt = ("Add_Given",Add_Given "solveFor x");*)
55.318 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.319 -"--- s4 ---";
55.320 -(* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)
55.321 -(*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;*)
55.322 -"--- s5 ---";
55.323 -(* val nxt = ("Add_Find",Add_Find "solutions L");*)
55.324 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.325 -"--- s6 ---";
55.326 -(* val nxt = ("Specify_Theory",Specify_Theory "Test");*)
55.327 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.328 -"--- s7 ---";
55.329 -(* val nxt = ("Specify_Problem",
55.330 - Specify_Problem ["sqroot-test", "univariate", "equation", "test"]);*)
55.331 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.332 -"--- s8 ---";
55.333 -(* val nxt = ("Specify_Method",Specify_Method ("Test", "sqrt-equ-test"));*)
55.334 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.335 -"--- s9 ---";
55.336 -(* val nxt = ("Apply_Method",Apply_Method ("Test", "sqrt-equ-test"));*)
55.337 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.338 -(*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"*)
55.339 -"--- !!! x1 --- 1.norm_equation";
55.340 -(*###*)val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
55.341 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.342 -"--- !!! x2 --- 1.norm_equation";
55.343 -(*me-NEW: "9 + 4 * x = (sqrt x + sqrt (5 + x)) \<up> 2" -- NICHT norm_equation!!*)
55.344 -(*me-OLD: "sqrt (9 + 4 * x) + -1 * (sqrt x + sqrt (5 + x)) = 0"*)
55.345 -(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
55.346 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.347 -(*"-1 * sqrt x + (-1 * sqrt (5 + x) + sqrt (9 + 4 * x)) = 0"*)
55.348 -(*(me nxt p [1] pt) handle e => print_exn_G e;*)
55.349 -"--- !!! x3 --- 1.norm_equation";
55.350 -(*val nxt = ("Empty_Tac",Empty_Tac) ### helpless*)
55.351 -(*###*)val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
55.352 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.353 -"--- !!! x4 --- 1.norm_equation";
55.354 -(*"-1 * sqrt x + -1 * sqrt (5 + x) + sqrt (9 + 4 * x) = 0"*)
55.355 -(*val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root")*)
55.356 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.357 -"--- !!! x5 --- 1.norm_equation";
55.358 -(*"sqrt (9 + 4 * x) = 0 + -1 * (-1 * sqrt x + -1 * sqrt (5 + x))"*)
55.359 -(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
55.360 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.361 -
55.362 -(*FIXXXXXXXXXXXXXXXXXXXXXXXME reestablish check:
55.363 -if f= Form'(Test_Out.FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"))
55.364 -then() else error "new behaviour in test-example 1.norm sqrt-equ-test";
55.365 -#################################################*)
55.366 -
55.367 -(* use"../tests/scriptnew.sml";
55.368 - *)
55.369 -
55.370 -" _________________ equation with x =(-12)/5, but L ={} ------- ";
55.371 -
55.372 -val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",
55.373 - "solveFor x", "errorBound (eps=0)",
55.374 - "solutions L"];
55.375 -val (dI',pI',mI') =
55.376 - ("Test",["sqroot-test", "univariate", "equation", "test"],
55.377 - ["Test", "square_equation"]);
55.378 -
55.379 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
55.380 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55.381 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.382 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.383 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.384 -(*val nxt = ("Apply_Method",Apply_Method ["Test", "square_equation"])*)
55.385 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.386 -(*val nxt = "square_equation_left",
55.387 - "[| 0 <= ?a; 0 <= ?b |] ==> (sqrt ?a = ?b) = (?a = ?b \<up> 2)"))*)
55.388 -Ctree.get_assumptions pt p;
55.389 -(*it = [] : string list;*)
55.390 -Rewrite.trace_on := false;
55.391 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.392 -Rewrite.trace_on := false;
55.393 -val asms = Ctree.get_assumptions pt p;
55.394 -if asms = [(TermC.str2term "0 <= 9 + 4 * x",[1]),
55.395 - (TermC.str2term "0 <= x",[1]),
55.396 - (TermC.str2term "0 <= -3 + x",[1])] then ()
55.397 -else error "scriptnew.sml diff.behav. in sqrt assumptions 1";
55.398 -
55.399 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.400 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.401 -(*val nxt = Rewrite ("square_equation_left", *)
55.402 -val asms = Ctree.get_assumptions pt p;
55.403 -[("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1])];
55.404 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.405 -val asms = Ctree.get_assumptions pt p;
55.406 -if asms = [(TermC.str2term "0 <= 9 + 4 * x",[1]),
55.407 - (TermC.str2term "0 <= x",[1]),
55.408 - (TermC.str2term "0 <= -3 + x",[1]),
55.409 - (TermC.str2term "0 <= x \<up> 2 + -3 * x",[6]),
55.410 - (TermC.str2term "0 <= 6 + x",[6])] then ()
55.411 -else error "scriptnew.sml diff.behav. in sqrt assumptions 2";
55.412 -
55.413 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.414 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.415 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.416 -(*val nxt = Subproblem ("Test",["LINEAR", "univariate", "equation", "test"*)
55.417 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.418 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.419 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.420 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.421 -(*val nxt = ("Apply_Method",Apply_Method ["Test", "solve_linear"])*)
55.422 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.423 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.424 -(*val nxt =
55.425 - ("Check_Postcond",Check_Postcond ["LINEAR", "univariate", "equation", "test"])*)
55.426 -val asms = Ctree.get_assumptions pt p;
55.427 -if asms = [] then ()
55.428 -else error "scriptnew.sml diff.behav. in sqrt assumptions 3";
55.429 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.430 -(*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
55.431 -
55.432 -val asms = Ctree.get_assumptions pt p;
55.433 -if asms = [(TermC.str2term "0 <= 9 + 4 * x",[1]),
55.434 - (TermC.str2term "0 <= x",[1]),
55.435 - (TermC.str2term "0 <= -3 + x",[1]),
55.436 - (TermC.str2term "0 <= x \<up> 2 + -3 * x",[6]),
55.437 - (TermC.str2term "0 <= 6 + x",[6])] then ()
55.438 -else raise
55.439 - error "scriptnew.sml: diff.behav. at Check_elementwise [x = -12 / 5]";
55.440 -
55.441 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.442 -(*val nxt = Check_Postcond ["sqroot-test", "univariate", "equation", "test"])*)
55.443 -val asms = Ctree.get_assumptions pt p;
55.444 -[("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1]),
55.445 - ("0 <= x \<up> 2 + -3 * x",[6]),("0 <= 6 + x",[6]),
55.446 - ("0 <= 6 + -12 / 5 &\n0 <= (-12 / 5) \<up> 2 + -3 * (-12 / 5) &\n0 <= -3 + -12 / 5 & 0 <= -12 / 5 & 0 <= 9 + 4 * (-12 / 5)",
55.447 - [13])];
55.448 -
55.449 -
55.450 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
55.451 -val Form' (Test_Out.FormKF (_,_,_,_,ff)) = f;
55.452 -if ff="[x = -12 / 5]"
55.453 -then writeln("there should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\n")
55.454 -else error "diff.behav. in scriptnew.sml; root-eq: L = []";
55.455 -
55.456 -val asms = Ctree.get_assumptions pt p;
55.457 -if asms = [(TermC.str2term "0 <= 9 + 4 * (-12 / 5)",[]),
55.458 - (TermC.str2term "0 <= -12 / 5", []),
55.459 - (TermC.str2term "0 <= -3 + -12 / 5", []),
55.460 - (TermC.str2term "0 <= (-12 / 5) \<up> 2 + -3 * (-12 / 5)", []),
55.461 - (TermC.str2term "0 <= 6 + -12 / 5", [])] then ()
55.462 -else error "scriptnew.sml diff.behav. in sqrt assumptions 4";
55.463 -
55.464 -
55.465 -"------------------ script with Map, Subst (biquadr.equ.)---------";
55.466 -"------------------ script with Map, Subst (biquadr.equ.)---------";
55.467 -"------------------ script with Map, Subst (biquadr.equ.)---------";
55.468 -
55.469 -
55.470 -(*GoOn.5.03. script with Map, Subst (biquadr.equ.)
55.471 -val scr = Prog ((inst_abs o Thm.term_of o the o (TermC.parse thy))
55.472 - "Program Biquadrat_poly (e_e::bool) (v_::real) = \
55.473 - \(let e_e = Substitute [(v_ \<up> 4, v_0_ \<up> 2),(v_ \<up> 2, v_0_)] e_; \
55.474 - \ L_0_ = (SubProblem (PolyEqX,[univariate,equation], [no_met]) \
55.475 - \ [BOOL e_e, REAL v_0_]); \
55.476 - \ L_i_ = Map (((Substitute [(v_0_, v_ \<up> 2)]) #> \
55.477 - \ ((Rewrite real_root_positive) Or \
55.478 - \ (Rewrite real_root_negative)) #> \
55.479 - \ OrToList) L_0_ \
55.480 - \ in (flat ....))"
55.481 -);
55.482 -
55.483 -*)
55.484 -
56.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Fri May 07 13:23:24 2021 +0200
56.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Fri May 07 18:12:51 2021 +0200
56.3 @@ -154,26 +154,26 @@
56.4 *** . Free (t_t, 'z)
56.5 *** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
56.6 *** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
56.7 -*** . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
56.8 +*** . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
56.9 *** . . . . Free (discard_minus, ID)
56.10 *** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
56.11 *** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
56.12 -*** . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
56.13 +*** . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
56.14 *** . . . . . Free (rat_mult_poly, ID)
56.15 *** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
56.16 *** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
56.17 -*** . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
56.18 +*** . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
56.19 *** . . . . . . Free (make_rat_poly_with_parentheses, ID)
56.20 *** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
56.21 *** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
56.22 -*** . . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
56.23 +*** . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
56.24 *** . . . . . . . Free (cancel_p_rls, ID)
56.25 *** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
56.26 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
56.27 -*** . . . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
56.28 +*** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
56.29 *** . . . . . . . . Free (norm_Rational_rls, ID)
56.30 *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
56.31 -*** . . . . . . . Const (Program.Rewrite'_Set, ID => 'a => 'a)
56.32 +*** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
56.33 *** . . . . . . . . Free (discard_parentheses1, ID)
56.34 *** . . Const (empty, 'a)
56.35 ***)
56.36 @@ -259,7 +259,7 @@
56.37 case t of
56.38 (Const ("Tactical.Try", _) $
56.39 (Const ("Tactical.Repeat", _) $
56.40 - (Const ("Prog_Tac.Rewrite'_Inst", _) $
56.41 + (Const ("Prog_Tac.Rewrite_Inst", _) $
56.42 (Const ("List.list.Cons", _) $
56.43 (Const ("Product_Type.Pair", _) $
56.44 bdv $
56.45 @@ -278,11 +278,11 @@
56.46 val {scr, ...} = MethodC.from_store ["Test", "sqrt-equ-test"]; val Prog sc = scr; val ts = stacpbls sc;
56.47 case stacpbls sc of
56.48 [Const ("Prog_Tac.Rewrite", _) $ square_equation_left,
56.49 - Const ("Prog_Tac.Rewrite'_Set", _) $ Test_simplify,
56.50 - Const ("Prog_Tac.Rewrite'_Set", _) $ rearrange_assoc,
56.51 - Const ("Prog_Tac.Rewrite'_Set", _) $ isolate_root,
56.52 - Const ("Prog_Tac.Rewrite'_Set", _) $ norm_equation,
56.53 - Const ("Prog_Tac.Rewrite'_Set'_Inst", _) $
56.54 + Const ("Prog_Tac.Rewrite_Set", _) $ Test_simplify,
56.55 + Const ("Prog_Tac.Rewrite_Set", _) $ rearrange_assoc,
56.56 + Const ("Prog_Tac.Rewrite_Set", _) $ isolate_root,
56.57 + Const ("Prog_Tac.Rewrite_Set", _) $ norm_equation,
56.58 + Const ("Prog_Tac.Rewrite_Set_Inst", _) $
56.59 (Const ("List.list.Cons", _) $ (Const ("Product_Type.Pair", _) $ bdv $ Free ("v_v", _)) $
56.60 Const ("List.list.Nil", _)) $ isolate_bdv] =>
56.61 if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
57.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Fri May 07 13:23:24 2021 +0200
57.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Fri May 07 18:12:51 2021 +0200
57.3 @@ -300,7 +300,7 @@
57.4 "----------- get_pair with 3 args --------------------------------";
57.5 "----------- get_pair with 3 args --------------------------------";
57.6 val (thy, op_, ef, arg) =
57.7 - (thy, "EqSystem.occur'_exactly'_in",
57.8 + (thy, "EqSystem.occur_exactly_in",
57.9 assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
57.10 TermC.str2term
57.11 "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) / 2"
58.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Fri May 07 13:23:24 2021 +0200
58.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Fri May 07 18:12:51 2021 +0200
58.3 @@ -57,7 +57,7 @@
58.4 if occurs_in t t then "OK" else error "occurs_in x x -> f ..changed";
58.5
58.6 val t = TermC.str2term "x occurs_in x";
58.7 -val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs'_in" t 0;
58.8 +val SOME (str, t') = eval_occurs_in 0 "Prog_Expr.occurs_in" t 0;
58.9 if UnparseC.term t' = "x occurs_in x = True" then ()
58.10 else error "x occurs_in x = True ..changed";
58.11
58.12 @@ -65,14 +65,14 @@
58.13 some_occur_in [str2t"c",str2t"c_2"] (str2t"a + b + c");
58.14 val t = str2t "some_of [c, c_2, c_3, c_4] occur_in \
58.15 \-1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
58.16 -val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some'_occur'_in" t 0;
58.17 +val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;
58.18 if UnparseC.term t' =
58.19 "some_of [c, c_2, c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2 =\nTrue" then ()
58.20 else error "atools.sml: some_occur_in true";
58.21
58.22 val t = str2t "some_of [c_3, c_4] occur_in \
58.23 \-1 * q_0 * L \<up> 2 / 2 + L * c + c_2";
58.24 -val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some'_occur'_in" t 0;
58.25 +val SOME (str,t') = eval_some_occur_in 0 "Prog_Expr.some_occur_in" t 0;
58.26 if UnparseC.term t' =
58.27 "some_of [c_3, c_4] occur_in -1 * q_0 * L \<up> 2 / 2 + L * c + c_2 = False" then ()
58.28 else error "atools.sml: some_occur_in false";
58.29 @@ -166,7 +166,7 @@
58.30 "---------fun eval_argument_of -----------------------------------------------------------------";
58.31 "---------fun eval_argument_of -----------------------------------------------------------------";
58.32 val t = TermC.str2term "argument_in (M_b x)";
58.33 -val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument'_in" t 0;
58.34 +val SOME (str, t') = eval_argument_in "0" "Prog_Expr.argument_in" t 0;
58.35 if UnparseC.term t' = "(argument_in M_b x) = x" then ()
58.36 else error "atools.sml:(argument_in M_b x) = x ???";
58.37
58.38 @@ -200,10 +200,10 @@
58.39 "---------fun eval_filter_sameFunId ------------------------------------------------------------";
58.40 val flhs as (fid $ _) = str2t "y' L";
58.41 val fs = str2t "[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
58.42 -val (p as Const ("Prog_Expr.filter'_sameFunId",_) $ (fid $ _) $ fs) =
58.43 +val (p as Const ("Prog_Expr.filter_sameFunId",_) $ (fid $ _) $ fs) =
58.44 str2t "filter_sameFunId (y' L) \
58.45 \[M_b x = c + L*x, y' x = c + L*x, y x = c + L*x]";
58.46 -val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter'_sameFunId" p "";
58.47 +val SOME (str, es) = eval_filter_sameFunId "" "Prog_Expr.filter_sameFunId" p "";
58.48 if UnparseC.term es = "(filter_sameFunId y' L [M_b x = c + L * x, y' x = c + L * x,\n y x = c + L * x]) =\n[y' x = c + L * x]" then ()
58.49 else error "atools.slm diff.behav. in filter_sameFunId";
58.50
59.1 --- a/test/Tools/isac/Specify/o-model.sml Fri May 07 13:23:24 2021 +0200
59.2 +++ b/test/Tools/isac/Specify/o-model.sml Fri May 07 18:12:51 2021 +0200
59.3 @@ -62,9 +62,9 @@
59.4 Const ("List.list.Nil", _),
59.5 Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Free ("y", _) $ Free ("L", _)) $ Free ("0", _)) $
59.6 Const ("List.list.Nil", _),
59.7 - Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Const ("Biegelinie.M'_b", _) $ Free ("0", _)) $ Free ("0", _)) $
59.8 + Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Const ("Biegelinie.M_b", _) $ Free ("0", _)) $ Free ("0", _)) $
59.9 Const ("List.list.Nil", _),
59.10 - Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Const ("Biegelinie.M'_b", _) $ Free ("L", _)) $ Free ("0", _)) $
59.11 + Const ("List.list.Cons", _) $ (Const ("HOL.eq", _) $ (Const ("Biegelinie.M_b", _) $ Free ("L", _)) $ Free ("0", _)) $
59.12 Const ("List.list.Nil", _)]),
59.13 ("#undef", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]),
59.14 _, _] =