1.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Sat Jun 22 14:34:06 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Sun Jun 23 14:23:09 2019 +0200
1.3 @@ -56,7 +56,7 @@
1.4 Rule.Calc ("Atools.is'_const", eval_const "#is_const_"),
1.5 Rule.Calc ("Atools.occurs'_in", eval_occurs_in ""),
1.6 Rule.Calc ("Tools.matches", Tools.eval_matches "")],
1.7 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
1.8 + scr = Rule.EmptyScr
1.9 });
1.10 \<close>
1.11 setup \<open>KEStore_Elems.add_rlss [("eval_rls", (Context.theory_name @{theory}, eval_rls))]\<close>
2.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sat Jun 22 14:34:06 2019 +0200
2.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Sun Jun 23 14:23:09 2019 +0200
2.3 @@ -208,7 +208,7 @@
2.4 (*Rule.Rls_ add_fractions_p, #2*)
2.5 Rule.Rls_ cancel_p
2.6 ],
2.7 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
2.8 + scr = Rule.EmptyScr
2.9 };
2.10 \<close>
2.11 ML \<open>
2.12 @@ -229,7 +229,7 @@
2.13 Rule.Rls_ add_fractions_p,
2.14 Rule.Rls_ cancel_p
2.15 ],
2.16 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
2.17 + scr = Rule.EmptyScr
2.18 };
2.19 \<close>
2.20 ML \<open>
3.1 --- a/src/Tools/isac/Knowledge/InsSort.thy Sat Jun 22 14:34:06 2019 +0200
3.2 +++ b/src/Tools/isac/Knowledge/InsSort.thy Sun Jun 23 14:23:09 2019 +0200
3.3 @@ -66,7 +66,7 @@
3.4 Rule.Thm ("If_def", @{thm If_def} (* if ?P then ?x else ?y \<equiv> THE z. (?P = True \<longrightarrow> z = ?x) \<and> (?P = False \<longrightarrow> z = ?y) *)),
3.5 Rule.Thm ("if_True", @{thm if_True} (* "(if True then x else y) = x" *)),
3.6 Rule.Thm ("if_False", @{thm if_False} (* "(if False then x else y) = y" *))],
3.7 - errpatts = [], scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")};
3.8 + errpatts = [], scr = Rule.EmptyScr};
3.9 \<close>
3.10 setup \<open>KEStore_Elems.add_rlss [("ins_sort", (Context.theory_name @{theory}, ins_sort))]\<close>
3.11
4.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sat Jun 22 14:34:06 2019 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sun Jun 23 14:23:09 2019 +0200
4.3 @@ -196,13 +196,13 @@
4.4 Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})
4.5 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
4.6 ],
4.7 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
4.8 + scr = Rule.EmptyScr
4.9 }),
4.10 Rule.Rls_ make_rat_poly_with_parentheses,
4.11 Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
4.12 Rule.Rls_ rat_reduce_1
4.13 ],
4.14 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
4.15 + scr = Rule.EmptyScr
4.16 };
4.17
4.18 (*.for simplify_Integral adapted from 'norm_Rational'.*)
4.19 @@ -217,7 +217,7 @@
4.20 Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#) *)
4.21 Rule.Rls_ discard_parentheses1 (* mult only *)
4.22 ],
4.23 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
4.24 + scr = Rule.EmptyScr
4.25 };
4.26
4.27 (*.simplify terms before and after Integration such that
5.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sat Jun 22 14:34:06 2019 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Sun Jun 23 14:23:09 2019 +0200
5.3 @@ -1259,108 +1259,9 @@
5.4 \<close>
5.5
5.6 subsection \<open>rule-sets with explicit program for intermediate steps\<close>
5.7 -text \<open>such rule-sets are generated automatically in general\<close>
5.8 -(* probably perfectly replaced by auto-generated version *)
5.9 -(*ok
5.10 -partial_function (tailrec) expand_binoms :: "real \<Rightarrow> real"
5.11 - where
5.12 -"expand_binoms term =
5.13 -(Repeat
5.14 -((Try (Repeat (Rewrite ''real_diff_minus'' False))) @@
5.15 -
5.16 - (Try (Repeat (Rewrite ''distrib_right'' False))) @@
5.17 - (Try (Repeat (Rewrite ''distrib_left'' False))) @@
5.18 - (Try (Repeat (Rewrite ''left_diff_distrib'' False))) @@
5.19 - (Try (Repeat (Rewrite ''right_diff_distrib'' False))) @@
5.20 -
5.21 - (Try (Repeat (Rewrite ''mult_1_left'' False))) @@
5.22 - (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@
5.23 - (Try (Repeat (Rewrite ''add_0_left'' False))) @@
5.24 -
5.25 - (Try (Repeat (Rewrite ''mult_commute'' False))) @@
5.26 - (Try (Repeat (Rewrite ''real_mult_left_commute'' False))) @@
5.27 - (Try (Repeat (Rewrite ''mult_assoc'' False))) @@
5.28 - (Try (Repeat (Rewrite ''add_commute'' False))) @@
5.29 - (Try (Repeat (Rewrite ''add_left_commute'' False))) @@
5.30 - (Try (Repeat (Rewrite ''add_assoc'' False))) @@
5.31 -
5.32 - (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@
5.33 - (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@
5.34 - (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@
5.35 - (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@
5.36 -
5.37 - (Try (Repeat (Rewrite ''real_num_collect'' False))) @@
5.38 - (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@
5.39 -
5.40 - (Try (Repeat (Rewrite ''real_one_collect'' False))) @@
5.41 - (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@
5.42 -
5.43 - (Try (Repeat (Calculate ''PLUS'' ))) @@
5.44 - (Try (Repeat (Calculate ''TIMES'' ))) @@
5.45 - (Try (Repeat (Calculate ''POWER''))))
5.46 - term)"
5.47 -*)
5.48 -ML \<open>
5.49 -val scr_make_polynomial =
5.50 -"Script Expand_binoms t_t = " ^
5.51 -"(Repeat " ^
5.52 -"((Try (Repeat (Rewrite ''real_diff_minus'' False))) @@ " ^
5.53 -
5.54 -" (Try (Repeat (Rewrite ''distrib_right'' False))) @@ " ^
5.55 -" (Try (Repeat (Rewrite ''distrib_left'' False))) @@ " ^
5.56 -" (Try (Repeat (Rewrite ''left_diff_distrib'' False))) @@ " ^
5.57 -" (Try (Repeat (Rewrite ''right_diff_distrib'' False))) @@ " ^
5.58 -
5.59 -" (Try (Repeat (Rewrite ''mult_1_left'' False))) @@ " ^
5.60 -" (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@ " ^
5.61 -" (Try (Repeat (Rewrite ''add_0_left'' False))) @@ " ^
5.62 -
5.63 -" (Try (Repeat (Rewrite ''mult_commute'' False))) @@ " ^
5.64 -" (Try (Repeat (Rewrite ''real_mult_left_commute'' False))) @@ " ^
5.65 -" (Try (Repeat (Rewrite ''mult_assoc'' False))) @@ " ^
5.66 -" (Try (Repeat (Rewrite ''add_commute'' False))) @@ " ^
5.67 -" (Try (Repeat (Rewrite ''add_left_commute'' False))) @@ " ^
5.68 -" (Try (Repeat (Rewrite ''add_assoc'' False))) @@ " ^
5.69 -
5.70 -" (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@ " ^
5.71 -" (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@ " ^
5.72 -" (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@ " ^
5.73 -" (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@ " ^
5.74 -
5.75 -" (Try (Repeat (Rewrite ''real_num_collect'' False))) @@ " ^
5.76 -" (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@ " ^
5.77 -
5.78 -" (Try (Repeat (Rewrite ''real_one_collect'' False))) @@ " ^
5.79 -" (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@ " ^
5.80 -
5.81 -" (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
5.82 -" (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
5.83 -" (Try (Repeat (Calculate ''POWER'')))) " ^
5.84 -" t_t) ";
5.85 -
5.86 -(*version used by MG.02/03, overwritten by version AG in 04 below
5.87 -val make_polynomial = prep_rls'(
5.88 - Rule.Seq{id = "make_polynomial", preconds = []:term list,
5.89 - rew_ord = ("dummy_ord", Rule.dummy_ord),
5.90 - erls = Atools_erls, srls = Rule.Erls,
5.91 - calc = [], errpatts = [],
5.92 - rules = [Rule.Rls_ expand_poly,
5.93 - Rule.Rls_ order_add_mult,
5.94 - Rule.Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
5.95 - Rule.Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
5.96 - Rule.Rls_ reduce_012,
5.97 - Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),(*in --^*)
5.98 - Rule.Rls_ discard_parentheses
5.99 - ],
5.100 - scr = Rule.EmptyScr
5.101 - }); *)
5.102 -\<close>
5.103 -
5.104 -(* replacement by auto-generated version seemed to cause ERROR in algein.sml *)
5.105 -(*ok
5.106 partial_function (tailrec) expand_binoms_2 :: "real \<Rightarrow> real"
5.107 where
5.108 -"expand_binoms term =
5.109 +"expand_binoms_2 term =
5.110 (Repeat
5.111 ((Try (Repeat (Rewrite ''real_plus_binom_pow2'' False))) @@
5.112 (Try (Repeat (Rewrite ''real_plus_binom_times'' False))) @@
5.113 @@ -1392,42 +1293,7 @@
5.114 (Try (Repeat (Calculate ''TIMES'' ))) @@
5.115 (Try (Repeat (Calculate ''POWER''))))
5.116 term) "
5.117 -*)
5.118 ML \<open>
5.119 -val scr_expand_binoms =
5.120 -"Script Expand_binoms t_t = " ^
5.121 -"(Repeat " ^
5.122 -"((Try (Repeat (Rewrite ''real_plus_binom_pow2'' False))) @@ " ^
5.123 -" (Try (Repeat (Rewrite ''real_plus_binom_times'' False))) @@ " ^
5.124 -" (Try (Repeat (Rewrite ''real_minus_binom_pow2'' False))) @@ " ^
5.125 -" (Try (Repeat (Rewrite ''real_minus_binom_times'' False))) @@ " ^
5.126 -" (Try (Repeat (Rewrite ''real_plus_minus_binom1'' False))) @@ " ^
5.127 -" (Try (Repeat (Rewrite ''real_plus_minus_binom2'' False))) @@ " ^
5.128 -
5.129 -" (Try (Repeat (Rewrite ''mult_1_left'' False))) @@ " ^
5.130 -" (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@ " ^
5.131 -" (Try (Repeat (Rewrite ''add_0_left'' False))) @@ " ^
5.132 -
5.133 -" (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
5.134 -" (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
5.135 -" (Try (Repeat (Calculate ''POWER''))) @@ " ^
5.136 -
5.137 -" (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@ " ^
5.138 -" (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@ " ^
5.139 -" (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@ " ^
5.140 -" (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@ " ^
5.141 -
5.142 -" (Try (Repeat (Rewrite ''real_num_collect'' False))) @@ " ^
5.143 -" (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@ " ^
5.144 -
5.145 -" (Try (Repeat (Rewrite ''real_one_collect'' False))) @@ " ^
5.146 -" (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@ " ^
5.147 -
5.148 -" (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
5.149 -" (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
5.150 -" (Try (Repeat (Calculate ''POWER'')))) " ^
5.151 -" t_t) ";
5.152 -
5.153 val expand_binoms =
5.154 Rule.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
5.155 erls = Atools_erls, srls = Rule.Erls,
5.156 @@ -1525,7 +1391,7 @@
5.157 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
5.158 Rule.Calc ("Atools.pow", eval_binop "#power_")
5.159 ],
5.160 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) scr_expand_binoms)
5.161 + scr = Rule.Prog (LTool.prep_program @{thm expand_binoms_2.simps})
5.162 };
5.163 \<close>
5.164
5.165 @@ -1592,9 +1458,7 @@
5.166 [(*for preds in where_*)
5.167 Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
5.168 crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
5.169 - @{thm simplify.simps}
5.170 - (*"Script SimplifyScript (t_t::real) = " ^
5.171 - " ((Rewrite_Set ''norm_Poly'' False) t_t)"*))]
5.172 + @{thm simplify.simps})]
5.173 \<close>
5.174 ML \<open>
5.175 \<close> ML \<open>
6.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sat Jun 22 14:34:06 2019 +0200
6.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Sun Jun 23 14:23:09 2019 +0200
6.3 @@ -385,7 +385,7 @@
6.4 Rule.Thm ("cancel_leading_coeff11",TermC.num_str @{thm cancel_leading_coeff11}),
6.5 Rule.Thm ("cancel_leading_coeff12",TermC.num_str @{thm cancel_leading_coeff12}),
6.6 Rule.Thm ("cancel_leading_coeff13",TermC.num_str @{thm cancel_leading_coeff13})
6.7 - ],scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")});
6.8 + ],scr = Rule.EmptyScr});
6.9
6.10 val prep_rls' = LTool.prep_rls @{theory};
6.11 \<close>
6.12 @@ -400,7 +400,7 @@
6.13 Rule.Thm ("complete_square4",TermC.num_str @{thm complete_square4}),
6.14 Rule.Thm ("complete_square5",TermC.num_str @{thm complete_square5})
6.15 ],
6.16 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.17 + scr = Rule.EmptyScr
6.18 });
6.19
6.20 val polyeq_simplify = prep_rls'(
6.21 @@ -422,7 +422,7 @@
6.22 Rule.Calc ("Atools.pow" ,eval_binop "#power_"),
6.23 Rule.Rls_ reduce_012
6.24 ],
6.25 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.26 + scr = Rule.EmptyScr
6.27 });
6.28 \<close>
6.29 setup \<open>KEStore_Elems.add_rlss
6.30 @@ -444,7 +444,7 @@
6.31 rules = [Rule.Thm("d0_true",TermC.num_str @{thm d0_true}),
6.32 Rule.Thm("d0_false",TermC.num_str @{thm d0_false})
6.33 ],
6.34 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.35 + scr = Rule.EmptyScr
6.36 });
6.37
6.38 (* -- d1 -- *)
6.39 @@ -463,7 +463,7 @@
6.40 Rule.Thm("d1_isolate_div",TermC.num_str @{thm d1_isolate_div})
6.41 (* bx=c -> x=c/b *)
6.42 ],
6.43 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.44 + scr = Rule.EmptyScr
6.45 });
6.46
6.47 \<close>
6.48 @@ -486,7 +486,7 @@
6.49 Rule.Thm ("d2_reduce_equation2", TermC.num_str @{thm d2_reduce_equation2}),(* x(a+ x)=0 -> x=0 |a+ x=0*)
6.50 Rule.Thm ("d2_isolate_div", TermC.num_str @{thm d2_isolate_div}) (* bx^2=c -> x^2=c/b *)
6.51 ],
6.52 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.53 + scr = Rule.EmptyScr
6.54 });
6.55 \<close>
6.56 ML\<open>
6.57 @@ -513,7 +513,7 @@
6.58 Rule.Thm("d2_isolate_div",TermC.num_str @{thm d2_isolate_div})
6.59 (* bx^2=c -> x^2=c/b*)
6.60 ],
6.61 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.62 + scr = Rule.EmptyScr
6.63 });
6.64 \<close>
6.65 ML\<open>
6.66 @@ -559,7 +559,7 @@
6.67 (* x^2=0 *)
6.68 Rule.Thm("d2_sqrt_equation3",TermC.num_str @{thm d2_sqrt_equation3})
6.69 (* 1x^2=0 *)
6.70 - ],scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.71 + ],scr = Rule.EmptyScr
6.72 });
6.73 \<close>
6.74 ML\<open>
6.75 @@ -606,7 +606,7 @@
6.76 Rule.Thm("d2_sqrt_equation3",TermC.num_str @{thm d2_sqrt_equation3})
6.77 (* bx^2=0 *)
6.78 ],
6.79 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.80 + scr = Rule.EmptyScr
6.81 });
6.82 \<close>
6.83 ML\<open>
6.84 @@ -666,7 +666,7 @@
6.85 Rule.Thm("d2_isolate_div",TermC.num_str @{thm d2_isolate_div})
6.86 (* bx^2=c -> x^2=c/b*)
6.87 ],
6.88 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.89 + scr = Rule.EmptyScr
6.90 });
6.91 \<close>
6.92 ML\<open>
6.93 @@ -739,7 +739,7 @@
6.94 Rule.Thm("d3_root_equation1",TermC.num_str @{thm d3_root_equation1})
6.95 (*bdv^^^3=c) = (bdv = nroot 3 c*)
6.96 ],
6.97 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.98 + scr = Rule.EmptyScr
6.99 });
6.100 \<close>
6.101 ML\<open>
6.102 @@ -754,7 +754,7 @@
6.103 [Rule.Thm("d4_sub_u1",TermC.num_str @{thm d4_sub_u1})
6.104 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
6.105 ],
6.106 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
6.107 + scr = Rule.EmptyScr
6.108 });
6.109 \<close>
6.110 setup \<open>KEStore_Elems.add_rlss
7.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sat Jun 22 14:34:06 2019 +0200
7.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Sun Jun 23 14:23:09 2019 +0200
7.3 @@ -128,7 +128,7 @@
7.4 Rule.Thm("rat_mult_denominator_right",TermC.num_str @{thm rat_mult_denominator_right})
7.5 (* a/b=c -> a=cb *)
7.6 ],
7.7 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")});
7.8 + scr = Rule.EmptyScr});
7.9
7.10 \<close> ML \<open>
7.11 val RatEq_simplify = prep_rls'(
7.12 @@ -152,7 +152,7 @@
7.13 (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
7.14 Rule.Thm("rat_double_rat_3",TermC.num_str @{thm rat_double_rat_3})
7.15 (* ((a/b) / c = a / (b*c) ) *)],
7.16 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")});
7.17 + scr = Rule.EmptyScr});
7.18 \<close>
7.19 setup \<open>KEStore_Elems.add_rlss [("rateq_erls", (Context.theory_name @{theory}, rateq_erls))]\<close>
7.20 setup \<open>KEStore_Elems.add_rlss [("RatEq_eliminate", (Context.theory_name @{theory}, RatEq_eliminate))]\<close>
8.1 --- a/src/Tools/isac/Knowledge/Root.thy Sat Jun 22 14:34:06 2019 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Root.thy Sun Jun 23 14:23:09 2019 +0200
8.3 @@ -250,7 +250,7 @@
8.4 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
8.5 Rule.Calc ("Atools.pow", eval_binop "#power_")
8.6 ],
8.7 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
8.8 + scr = Rule.EmptyScr
8.9 });
8.10 \<close>
8.11 setup \<open>KEStore_Elems.add_rlss [("make_rooteq", (Context.theory_name @{theory}, make_rooteq))]\<close>
8.12 @@ -324,7 +324,7 @@
8.13 Rule.Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
8.14 Rule.Calc ("Atools.pow", eval_binop "#power_")
8.15 ],
8.16 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
8.17 + scr = Rule.EmptyScr
8.18 });
8.19 \<close>
8.20 setup \<open>KEStore_Elems.add_rlss
9.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sat Jun 22 14:34:06 2019 +0200
9.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Sun Jun 23 14:23:09 2019 +0200
9.3 @@ -307,7 +307,7 @@
9.4 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
9.5 Rule.Thm("sqrt_square_equation_right_6",TermC.num_str @{thm sqrt_square_equation_right_6})
9.6 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
9.7 - ],scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
9.8 + ],scr = Rule.EmptyScr
9.9 });
9.10
9.11 \<close> ML \<open>
9.12 @@ -352,7 +352,7 @@
9.13 Rule.Thm("sqrt_square_equation_left_6",TermC.num_str @{thm sqrt_square_equation_left_6})
9.14 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
9.15 ],
9.16 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
9.17 + scr = Rule.EmptyScr
9.18 });
9.19
9.20 \<close> ML \<open>
9.21 @@ -398,7 +398,7 @@
9.22 Rule.Thm("sqrt_square_equation_right_6",TermC.num_str @{thm sqrt_square_equation_right_6})
9.23 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
9.24 ],
9.25 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
9.26 + scr = Rule.EmptyScr
9.27 });
9.28
9.29 \<close> ML \<open>
9.30 @@ -430,7 +430,7 @@
9.31 Rule.Thm("sqrt_square_1",TermC.num_str @{thm sqrt_square_1})
9.32 (* sqrt a ^^^ 2 = a *)
9.33 ],
9.34 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
9.35 + scr = Rule.EmptyScr
9.36 });
9.37 \<close>
9.38 setup \<open>KEStore_Elems.add_rlss
10.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sat Jun 22 14:34:06 2019 +0200
10.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Sun Jun 23 14:23:09 2019 +0200
10.3 @@ -115,7 +115,7 @@
10.4 ( (a = d + e/f) = ( (a - d) * f = e )) *)
10.5 Rule.Thm("rootrat_equation_right_2",TermC.num_str @{thm rootrat_equation_right_2})
10.6 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
10.7 - ], scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")});
10.8 + ], scr = Rule.EmptyScr});
10.9 \<close>
10.10 setup \<open>KEStore_Elems.add_rlss
10.11 [("RooRatEq_erls", (Context.theory_name @{theory}, RooRatEq_erls)),
11.1 --- a/src/Tools/isac/Knowledge/Test.sml Sat Jun 22 14:34:06 2019 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,158 +0,0 @@
11.4 -val ttt = (Thm.term_of o the o (parse thy))
11.5 -"(Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) e_e";
11.6 -val ttt = (Thm.term_of o the o (parse thy))
11.7 -"(Try (Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) e_e)";
11.8 -
11.9 -val ttt = (Thm.term_of o the o (parse thy))
11.10 - "(Rewrite_Set SqRoot_simplify False) e_e ";
11.11 -val ttt = (Thm.term_of o the o (parseold thy))
11.12 - "%e_. (Rewrite_Set SqRoot_simplify False) e_e";
11.13 -val ttt = (Thm.term_of o the o (parseold thy))
11.14 - "Repeat (%e_. (Rewrite_Set SqRoot_simplify False)) e_e";
11.15 -
11.16 -val ttt = (Thm.term_of o the o (parse thy))
11.17 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.18 - \[e_e]";
11.19 -val ttt = (Thm.term_of o the o (parse thy))
11.20 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.21 - \((%e_. [e_e]) e_e)";
11.22 -val ttt = (Thm.term_of o the o (parse thy))
11.23 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.24 - \((%e_. (let e_e = e_e in [e_e])) e_e)";
11.25 -val ttt = (Thm.term_of o the o (parse thy))
11.26 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.27 - \((%e_. \
11.28 - \ (let e_e = ((Rewrite_Set SqRoot_simplify False) e_e)\
11.29 - \ in [e_e]))\
11.30 - \ e_e)";
11.31 -val ttt = (Thm.term_of o the o (parse thy))
11.32 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.33 - \((%ee_. (let e_e = ((Rewrite_Set SqRoot_simplify False) ee_) in [e_e])) e_e)";
11.34 -
11.35 -val ttt = (Thm.term_of o the o (parse thy))
11.36 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.37 - \(let e_e = \
11.38 - \ (Repeat ((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False)) e_e)\
11.39 - \ in [e_e])";
11.40 -(*----*)
11.41 -val ttt = (Thm.term_of o the o (parse thy))
11.42 -
11.43 -(*----*)
11.44 -val ttt = (Thm.term_of o the o (parse thy))
11.45 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.46 - \(let e_e = \
11.47 - \ (Repeat\
11.48 - \ ((%ee_. (Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) ee_)\
11.49 - \ e_e)\
11.50 - \ e_e)\
11.51 - \ in [e_e])";
11.52 -val ttt = (Thm.term_of o the o (parse thy))
11.53 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.54 - \(let e_e = \
11.55 - \ (Repeat\
11.56 - \ ((%ee_.\
11.57 - \ ((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) ee_))\
11.58 - \ e_e)\
11.59 - \ e_e)\
11.60 - \ in [e_e])";
11.61 -val ttt = (Thm.term_of o the o (parse thy))
11.62 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.63 - \(let e_e = \
11.64 - \ (Repeat\
11.65 - \ ((%ee_.\
11.66 - \ (let e_e = ((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) ee_)\
11.67 - \ in ((Rewrite_Set SqRoot_simplify False) e_e)) )\
11.68 - \ e_e)\
11.69 - \ e_e)\
11.70 - \ in [e_e])";
11.71 -atomty ttt;
11.72 -atomt ttt;
11.73 -
11.74 -val ttt = (Thm.term_of o the o (parse thy))
11.75 - "Script Testterm (g_::real) = \
11.76 - \Repeat\
11.77 - \ (Rewrite rmult_1 False) g_";
11.78 -val ttt = (Thm.term_of o the o (parse thy))
11.79 - "Script Testterm (g_::real) = \
11.80 - \Repeat\
11.81 - \ (((Rewrite rmult_1 False)) Or ((Rewrite rmult_0 False))) g_";
11.82 -val ttt = (Thm.term_of o the o (parse thy))
11.83 - "Script Testterm (g_::real) = \
11.84 - \Repeat\
11.85 - \ ((Repeat (Rewrite rmult_1 False)) Or (Repeat (Rewrite rmult_0 False))) g_";
11.86 -val ttt = (Thm.term_of o the o (parse thy))
11.87 - "Script Testterm (g_::real) = \
11.88 - \Repeat\
11.89 - \ ((Repeat (Rewrite rmult_1 False)) Or\
11.90 - \ (Repeat (Rewrite rmult_0 False))) g_";
11.91 -val ttt = (Thm.term_of o the o (parse thy))
11.92 - "Script Testterm (g_::real) = \
11.93 - \Repeat\
11.94 - \ ((Repeat (Rewrite rmult_1 False)) Or\
11.95 - \ (Repeat (Rewrite rmult_0 False)) Or\
11.96 - \ (Repeat (Rewrite rmult_0 False))) g_";
11.97 -val ttt = (Thm.term_of o the o (parse thy))
11.98 - "Script Testterm (g_::real) = \
11.99 - \Repeat\
11.100 - \ ((Try Repeat (Rewrite rmult_1 False)) Or\
11.101 - \ (Try Repeat (Rewrite rmult_0 False)) Or\
11.102 - \ (Try Repeat (Rewrite rmult_0 False))) g_";
11.103 -
11.104 -
11.105 -
11.106 -
11.107 -
11.108 -
11.109 -
11.110 -
11.111 -
11.112 -
11.113 -
11.114 -
11.115 -
11.116 -(*################### 29.4.02: Rewrite o Rewrite o ...###############*)
11.117 -(*################### 29.4.02: Rewrite o Rewrite o ...###############*)
11.118 -(*################### 29.4.02: Rewrite o Rewrite o ...###############*)
11.119 -
11.120 -
11.121 -
11.122 -atomt ttt;
11.123 -val ttt = (Thm.term_of o the o (parse thy))
11.124 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.125 - \(let e_e = \
11.126 - \ ((Repeat\
11.127 - \ (((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) @@\
11.128 - \ (Rewrite_Set SqRoot_simplify False)))) e_e)\
11.129 - \ in [e_e])";
11.130 -atomty ttt;
11.131 -
11.132 -
11.133 -val ttt = (Thm.term_of o the o (parse thy))
11.134 -"(Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) @@ yyy";
11.135 -atomty ttt;
11.136 -val ttt = (Thm.term_of o the o (parse thy))
11.137 - "(Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) @@\
11.138 - \ (Rewrite_Set SqRoot_simplify False)";
11.139 -atomty ttt;
11.140 -val ttt = (Thm.term_of o the o (parse thy))
11.141 - "(Repeat\
11.142 - \ ((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) @@\
11.143 - \ (Rewrite_Set SqRoot_simplify False))) e_e";
11.144 -atomty ttt;
11.145 -val ttt = (Thm.term_of o the o (parseold thy))
11.146 -"(let e_e = Repeat xxx e_e in [e_::bool])";
11.147 -atomty ttt;
11.148 -val ttt = (Thm.term_of o the o (parseold thy))
11.149 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.150 - \(let e_e = Repeat (xxx) e_e in [e_::bool])";
11.151 -atomty ttt;
11.152 -val ttt = (Thm.term_of o the o (parseold thy))
11.153 - "Script Solve_linear (e_e::bool) (v_v::real)= \
11.154 - \(let e_e =\
11.155 - \ Repeat\
11.156 - \ (((Rewrite_Set_Inst [(''bdv'',v_v::real)] isolate_bdv False) @@\
11.157 - \ (Rewrite_Set SqRoot_simplify False))) e_\
11.158 - \ in [e_::bool])"
11.159 -;
11.160 -atomty ttt;
11.161 -
12.1 --- a/src/Tools/isac/Knowledge/Test.thy Sat Jun 22 14:34:06 2019 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sun Jun 23 14:23:09 2019 +0200
12.3 @@ -385,7 +385,7 @@
12.4 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
12.5
12.6 Rule.Calc ("Atools.ident",eval_ident "#ident_")],
12.7 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
12.8 + scr = Rule.EmptyScr
12.9 };
12.10 \<close>
12.11 ML \<open>
12.12 @@ -430,7 +430,7 @@
12.13 Rule.Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
12.14
12.15 Rule.Calc ("Atools.ident",eval_ident "#ident_")],
12.16 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
12.17 + scr = Rule.EmptyScr
12.18 };
12.19 \<close>
12.20 setup \<open>KEStore_Elems.add_rlss [("testerls", (Context.theory_name @{theory}, prep_rls' testerls))]\<close>
12.21 @@ -444,7 +444,7 @@
12.22 rules =
12.23 [Rule.Thm ("sym_add_assoc",TermC.num_str (@{thm add.assoc} RS @{thm sym})),
12.24 Rule.Thm ("sym_rmult_assoc",TermC.num_str (@{thm rmult_assoc} RS @{thm sym}))],
12.25 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
12.26 + scr = Rule.EmptyScr
12.27 };
12.28
12.29 val ac_plus_times =
12.30 @@ -457,7 +457,7 @@
12.31 Rule.Thm ("rmult_commute",TermC.num_str @{thm rmult_commute}),
12.32 Rule.Thm ("rmult_left_commute",TermC.num_str @{thm rmult_left_commute}),
12.33 Rule.Thm ("rmult_assoc",TermC.num_str @{thm rmult_assoc})],
12.34 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
12.35 + scr = Rule.EmptyScr
12.36 };
12.37
12.38 (*todo: replace by Rewrite("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add)*)
12.39 @@ -466,7 +466,7 @@
12.40 erls = tval_rls, srls = Rule.e_rls, calc = [], errpatts = [],
12.41 rules = [Rule.Thm ("rnorm_equation_add",TermC.num_str @{thm rnorm_equation_add})
12.42 ],
12.43 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
12.44 + scr = Rule.EmptyScr
12.45 };
12.46 \<close>
12.47 ML \<open>
12.48 @@ -522,7 +522,7 @@
12.49 Rule.Thm ("radd_0",TermC.num_str @{thm radd_0}),
12.50 Rule.Thm ("radd_0_right",TermC.num_str @{thm radd_0_right})
12.51 ],
12.52 - scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
12.53 + scr = Rule.EmptyScr
12.54 (*since 040209 filled by prep_rls': STest_simplify*)
12.55 };
12.56 \<close>