1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Fri Jan 17 12:37:21 2020 +0100
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Fri Jan 17 13:14:11 2020 +0100
1.3 @@ -258,7 +258,7 @@
1.4 (*Rule.Rls_ discard_parentheses *3**),
1.5 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.6 Rule.Rls_ separate_bdv2,
1.7 - Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.8 + Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.9 ],
1.10 scr = Rule.EmptyScr};
1.11 \<close>
1.12 @@ -276,7 +276,7 @@
1.13 Rule.Rls_ discard_parentheses,
1.14 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.15 Rule.Rls_ separate_bdv2,
1.16 - Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.17 + Rule.Num_Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.18 ],
1.19 scr = Rule.EmptyScr};
1.20 (*
1.21 @@ -291,7 +291,7 @@
1.22 Rule.Rls {id="isolate_bdvs", preconds = [],
1.23 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.24 erls = Rule.append_rls "erls_isolate_bdvs" Rule.e_rls
1.25 - [(Rule.Calc ("EqSystem.occur'_exactly'_in",
1.26 + [(Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.27 eval_occur_exactly_in
1.28 "#eval_occur_exactly_in_"))
1.29 ],
1.30 @@ -308,10 +308,10 @@
1.31 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.32 erls = Rule.append_rls
1.33 "erls_isolate_bdvs_4x4" Rule.e_rls
1.34 - [Rule.Calc ("EqSystem.occur'_exactly'_in",
1.35 + [Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.36 eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.37 - Rule.Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.38 - Rule.Calc ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.39 + Rule.Num_Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.40 + Rule.Num_Calc ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.41 Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.42 Rule.Thm ("not_false",TermC.num_str @{thm not_false})
1.43 ],
1.44 @@ -344,19 +344,19 @@
1.45 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.46 erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.47 rules = [(*for precond NTH_CONS ...*)
1.48 - Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.49 - Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.50 + Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.51 + Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.52 (*immediately repeated rewrite pushes
1.53 '+' into precondition !*)
1.54 ],
1.55 scr = Rule.EmptyScr},
1.56 srls = Rule.Erls, calc = [], errpatts = [],
1.57 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.58 - Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.59 + Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.60 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.61 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.62 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.63 - Rule.Calc ("EqSystem.occur'_exactly'_in",
1.64 + Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.65 eval_occur_exactly_in
1.66 "#eval_occur_exactly_in_")
1.67 ],
1.68 @@ -373,19 +373,19 @@
1.69 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.70 erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.71 rules = [(*for precond NTH_CONS ...*)
1.72 - Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.73 - Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.74 + Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.75 + Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.76 (*immediately repeated rewrite pushes
1.77 '+' into precondition !*)
1.78 ],
1.79 scr = Rule.EmptyScr},
1.80 srls = Rule.Erls, calc = [], errpatts = [],
1.81 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.82 - Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.83 + Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.84 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.85 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.86 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.87 - Rule.Calc ("EqSystem.occur'_exactly'_in",
1.88 + Rule.Num_Calc ("EqSystem.occur'_exactly'_in",
1.89 eval_occur_exactly_in
1.90 "#eval_occur_exactly_in_")
1.91 ],
1.92 @@ -426,8 +426,8 @@
1.93 Rule.append_rls "prls_2x2_linear_system" Rule.e_rls
1.94 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.95 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.96 - Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.97 - Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.98 + Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.99 + Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.100 SOME "solveSystem e_s v_s", [])),
1.101 (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Celem.e_pblID
1.102 (["triangular", "2x2", "LINEAR", "system"],
1.103 @@ -453,8 +453,8 @@
1.104 Rule.append_rls "prls_3x3_linear_system" Rule.e_rls
1.105 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.106 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.107 - Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.108 - Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.109 + Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.110 + Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.111 SOME "solveSystem e_s v_s", [])),
1.112 (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Celem.e_pblID
1.113 (["4x4", "LINEAR", "system"],
1.114 @@ -465,8 +465,8 @@
1.115 Rule.append_rls "prls_4x4_linear_system" Rule.e_rls
1.116 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.117 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.118 - Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.119 - Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.120 + Rule.Num_Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.121 + Rule.Num_Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.122 SOME "solveSystem e_s v_s", [])),
1.123 (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Celem.e_pblID
1.124 (["triangular", "4x4", "LINEAR", "system"],
1.125 @@ -478,7 +478,7 @@
1.126 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.127 ("#Find" ,["solution ss'''"])],
1.128 Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.129 - [Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.130 + [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.131 SOME "solveSystem e_s v_s",
1.132 [["EqSystem","top_down_substitution","4x4"]])),
1.133 (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Celem.e_pblID
1.134 @@ -497,13 +497,13 @@
1.135 rew_ord = ("termlessI",termlessI),
1.136 erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls
1.137 [(*for asm in NTH_CONS ...*)
1.138 - Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.139 + Rule.Num_Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.140 (*2nd NTH_CONS pushes n+-1 into asms*)
1.141 - Rule.Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
1.142 + Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
1.143 ],
1.144 srls = Rule.Erls, calc = [], errpatts = [],
1.145 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.146 - Rule.Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.147 + Rule.Num_Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.148 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
1.149 scr = Rule.EmptyScr};
1.150 \<close>
1.151 @@ -656,7 +656,7 @@
1.152 {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [],
1.153 srls = Rule.append_rls "srls_top_down_4x4" srls [],
1.154 prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.155 - [Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.156 + [Rule.Num_Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.157 crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.158 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 #>#>#>#>#>#>#>#>#>#>*)
1.159 @{thm solve_system4.simps})]