1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Aug 29 13:52:47 2019 +0200
1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Sep 03 12:40:27 2019 +0200
1.3 @@ -60,7 +60,7 @@
1.4 t: the term under consideration
1.5 *)
1.6 fun occur_exactly_in vs all t =
1.7 - let fun occurs_in' a b = occurs_in b a
1.8 + let fun occurs_in' a b = Prog_Expr.occurs_in b a
1.9 in foldl and_ (true, map (occurs_in' t) vs)
1.10 andalso not (foldl or_ (false, map (occurs_in' t)
1.11 (subtract op = vs all)))
1.12 @@ -258,7 +258,7 @@
1.13 (*Rule.Rls_ discard_parentheses *3**),
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" ,eval_cancel "#divide_e")
1.17 + Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.18 ],
1.19 scr = Rule.EmptyScr};
1.20 \<close>
1.21 @@ -276,7 +276,7 @@
1.22 Rule.Rls_ discard_parentheses,
1.23 Rule.Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
1.24 Rule.Rls_ separate_bdv2,
1.25 - Rule.Calc ("Rings.divide_class.divide" ,eval_cancel "#divide_e")
1.26 + Rule.Calc ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")
1.27 ],
1.28 scr = Rule.EmptyScr};
1.29 (*
1.30 @@ -310,10 +310,9 @@
1.31 "erls_isolate_bdvs_4x4" Rule.e_rls
1.32 [Rule.Calc ("EqSystem.occur'_exactly'_in",
1.33 eval_occur_exactly_in "#eval_occur_exactly_in_"),
1.34 - Rule.Calc ("Atools.ident",eval_ident "#ident_"),
1.35 - Rule.Calc ("Atools.some'_occur'_in",
1.36 - eval_some_occur_in "#some_occur_in_"),
1.37 - Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.38 + Rule.Calc ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
1.39 + Rule.Calc ("Prog_Expr.some'_occur'_in", Prog_Expr.eval_some_occur_in "#some_occur_in_"),
1.40 + Rule.Thm ("not_true",TermC.num_str @{thm not_true}),
1.41 Rule.Thm ("not_false",TermC.num_str @{thm not_false})
1.42 ],
1.43 srls = Rule.Erls, calc = [], errpatts = [],
1.44 @@ -345,15 +344,15 @@
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",eval_equ "#less_"),
1.49 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_")
1.50 + Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.51 + Rule.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.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 @@ -374,15 +373,15 @@
1.64 rew_ord = ("e_rew_ord", Rule.e_rew_ord),
1.65 erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
1.66 rules = [(*for precond NTH_CONS ...*)
1.67 - Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.68 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_")
1.69 + Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.70 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_")
1.71 (*immediately repeated rewrite pushes
1.72 '+' into precondition !*)
1.73 ],
1.74 scr = Rule.EmptyScr},
1.75 srls = Rule.Erls, calc = [], errpatts = [],
1.76 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.77 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.78 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.79 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL}),
1.80 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}),
1.81 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil}),
1.82 @@ -427,8 +426,8 @@
1.83 Rule.append_rls "prls_2x2_linear_system" Rule.e_rls
1.84 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.85 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.86 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.87 - Rule.Calc ("HOL.eq",eval_equal "#equal_")],
1.88 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.89 + Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.90 SOME "solveSystem e_s v_s", [])),
1.91 (Specify.prep_pbt thy "pbl_equsys_lin_2x2_tri" [] Celem.e_pblID
1.92 (["triangular", "2x2", "LINEAR", "system"],
1.93 @@ -454,8 +453,8 @@
1.94 Rule.append_rls "prls_3x3_linear_system" Rule.e_rls
1.95 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.96 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.97 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.98 - Rule.Calc ("HOL.eq",eval_equal "#equal_")],
1.99 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.100 + Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.101 SOME "solveSystem e_s v_s", [])),
1.102 (Specify.prep_pbt thy "pbl_equsys_lin_4x4" [] Celem.e_pblID
1.103 (["4x4", "LINEAR", "system"],
1.104 @@ -466,8 +465,8 @@
1.105 Rule.append_rls "prls_4x4_linear_system" Rule.e_rls
1.106 [Rule.Thm ("LENGTH_CONS",TermC.num_str @{thm LENGTH_CONS}),
1.107 Rule.Thm ("LENGTH_NIL",TermC.num_str @{thm LENGTH_NIL}),
1.108 - Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.109 - Rule.Calc ("HOL.eq",eval_equal "#equal_")],
1.110 + Rule.Calc ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.111 + Rule.Calc ("HOL.eq", Prog_Expr.eval_equal "#equal_")],
1.112 SOME "solveSystem e_s v_s", [])),
1.113 (Specify.prep_pbt thy "pbl_equsys_lin_4x4_tri" [] Celem.e_pblID
1.114 (["triangular", "4x4", "LINEAR", "system"],
1.115 @@ -479,7 +478,7 @@
1.116 "(NTH 4 (v_s::real list)) occurs_in (NTH 4 (e_s::bool list))"]),
1.117 ("#Find" ,["solution ss'''"])],
1.118 Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.119 - [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.120 + [Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.121 SOME "solveSystem e_s v_s",
1.122 [["EqSystem","top_down_substitution","4x4"]])),
1.123 (Specify.prep_pbt thy "pbl_equsys_lin_4x4_norm" [] Celem.e_pblID
1.124 @@ -498,13 +497,13 @@
1.125 rew_ord = ("termlessI",termlessI),
1.126 erls = Rule.append_rls "erls_in_srls_IntegrierenUnd.." Rule.e_rls
1.127 [(*for asm in NTH_CONS ...*)
1.128 - Rule.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.129 + Rule.Calc ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
1.130 (*2nd NTH_CONS pushes n+-1 into asms*)
1.131 - Rule.Calc("Groups.plus_class.plus", eval_binop "#add_")
1.132 + Rule.Calc("Groups.plus_class.plus", (**)eval_binop "#add_")
1.133 ],
1.134 srls = Rule.Erls, calc = [], errpatts = [],
1.135 rules = [Rule.Thm ("NTH_CONS",TermC.num_str @{thm NTH_CONS}),
1.136 - Rule.Calc("Groups.plus_class.plus", eval_binop "#add_"),
1.137 + Rule.Calc("Groups.plus_class.plus", (**)eval_binop "#add_"),
1.138 Rule.Thm ("NTH_NIL",TermC.num_str @{thm NTH_NIL})],
1.139 scr = Rule.EmptyScr};
1.140 \<close>
1.141 @@ -654,7 +653,7 @@
1.142 {rew_ord'="ord_simplify_System", rls' = Rule.Erls, calc = [],
1.143 srls = Rule.append_rls "srls_top_down_4x4" srls [],
1.144 prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular
1.145 - [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")],
1.146 + [Rule.Calc ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in "")],
1.147 crls = Rule.Erls, errpats = [], nrls = Rule.Erls},
1.148 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*)
1.149 @{thm solve_system4.simps})]