1.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Aug 03 18:17:27 2022 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Aug 04 12:48:37 2022 +0200
1.3 @@ -439,7 +439,7 @@
1.4 val rearrange_assoc =
1.5 Rule_Def.Repeat{
1.6 id = "rearrange_assoc", preconds = [],
1.7 - rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
1.8 + rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.9 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [],
1.10 rules = [
1.11 \<^rule_thm_sym>\<open>add.assoc\<close>,
1.12 @@ -461,7 +461,7 @@
1.13
1.14 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*)
1.15 val norm_equation =
1.16 - Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
1.17 + Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.18 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [],
1.19 rules = [
1.20 \<^rule_thm>\<open>rnorm_equation_add\<close>],
1.21 @@ -525,7 +525,7 @@
1.22 ML \<open>
1.23 (*isolate the root in a root-equation*)
1.24 val isolate_root =
1.25 - Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
1.26 + Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.27 erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [],
1.28 rules = [
1.29 \<^rule_thm>\<open>rroot_to_lhs\<close>,
1.30 @@ -539,7 +539,7 @@
1.31 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*)
1.32 val isolate_bdv =
1.33 Rule_Def.Repeat{
1.34 - id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord),
1.35 + id = "isolate_bdv", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty),
1.36 erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [],
1.37 rules = [
1.38 \<^rule_thm>\<open>risolate_bdv_add\<close>,
1.39 @@ -777,7 +777,7 @@
1.40 in
1.41 [e_e])"
1.42 method met_test_solvelin : "Test/solve_linear" =
1.43 - \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
1.44 + \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
1.45 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
1.46 nrls = Test_simplify}\<close>
1.47 Program: solve_linear.simps
1.48 @@ -808,7 +808,7 @@
1.49
1.50 method met_test_sqrt : "Test/sqrt-equ-test" =
1.51 (*root-equation, version for tests before 8.01.01*)
1.52 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
1.53 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
1.54 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
1.55 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")],
1.56 prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty
1.57 @@ -834,7 +834,7 @@
1.58
1.59 method met_test_squ_sub : "Test/squ-equ-test-subpbl1" =
1.60 (*tests subproblem fixed linear*)
1.61 - \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty,
1.62 + \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
1.63 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty
1.64 [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")],
1.65 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}\<close>
1.66 @@ -864,7 +864,7 @@
1.67
1.68 method met_test_eq1 : "Test/square_equation1" =
1.69 (*root-equation1:*)
1.70 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
1.71 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
1.72 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
1.73 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
1.74 prls=Rule_Set.empty, calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
1.75 @@ -894,7 +894,7 @@
1.76
1.77 method met_test_squ2 : "Test/square_equation2" =
1.78 (*root-equation2*)
1.79 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
1.80 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
1.81 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
1.82 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
1.83 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
1.84 @@ -924,7 +924,7 @@
1.85
1.86 method met_test_squeq : "Test/square_equation" =
1.87 (*root-equation*)
1.88 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,
1.89 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,
1.90 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty
1.91 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")],
1.92 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close>
1.93 @@ -947,7 +947,7 @@
1.94
1.95 method met_test_eq_plain : "Test/solve_plain_square" =
1.96 (*solve_plain_square*)
1.97 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
1.98 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
1.99 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
1.100 asm_rls=[],asm_thm=[]*)}\<close>
1.101 Program: solve_plain_square.simps
1.102 @@ -974,7 +974,7 @@
1.103 [''no_met'']) [BOOL e_e, REAL v_v])"
1.104
1.105 method met_test_norm_univ : "Test/norm_univar_equation" =
1.106 - \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
1.107 + \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls,
1.108 errpats = [], nrls = Rule_Set.empty}\<close>
1.109 Program: norm_univariate_equ.simps
1.110 Given: "equality e_e" "solveFor v_v"
1.111 @@ -992,7 +992,7 @@
1.112 (Try (Calculate ''TIMES''))) t_t)"
1.113
1.114 method met_test_intsimp : "Test/intsimp" =
1.115 - \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
1.116 + \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [],
1.117 crls = tval_rls, errpats = [], nrls = Test_simplify}\<close>
1.118 Program: test_simplify.simps
1.119 Given: "intTestGiven t_t"