1.1 --- a/src/Tools/isac/Build_Isac.thy Tue Aug 31 15:36:57 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Aug 31 16:00:13 2010 +0200
1.3 @@ -12,7 +12,7 @@
1.4 header {* Loading the isac mathengine *}
1.5
1.6 theory Build_Isac
1.7 -imports Complex_Main "ProgLang/Script" (*ListC, Tools, Script*)
1.8 +imports Complex_Main "ProgLang/Script" "ProgLang/Language"
1.9 begin
1.10
1.11 ML {*
1.12 @@ -61,11 +61,11 @@
1.13 use_thy "Knowledge/Delete"
1.14 use_thy "Knowledge/Descript"
1.15 use_thy "Knowledge/Atools"
1.16 +use_thy "Knowledge/Simplify"
1.17
1.18
1.19 text {*------------------------------------------*}
1.20 (*
1.21 -use_thy "Knowledge/Simplify"
1.22 use_thy "Knowledge/Poly"
1.23 use_thy "Knowledge/Rational"
1.24 use_thy "Knowledge/PolyMinus"
2.1 --- a/src/Tools/isac/Interpret/rewtools.sml Tue Aug 31 15:36:57 2010 +0200
2.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Tue Aug 31 16:00:13 2010 +0200
2.3 @@ -217,7 +217,7 @@
2.4 | sym_Thm (Rls_ rls) = Rls_ (*WN060825?!?*) (sym_rls rls)
2.5 | sym_Thm r = raise error ("sym_Thm: not for "^(rule2str r));
2.6 (*
2.7 - val th = Thm ("real_one_collect",num_str real_one_collect);
2.8 + val th = Thm ("real_one_collect",num_str @{real_one_collect);
2.9 sym_Thm th;
2.10 val th =
2.11 Thm ("real_one_collect","?m is_const ==> ?n + ?m * ?n = (1 + ?m) * ?n")
3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Tue Aug 31 15:36:57 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue Aug 31 16:00:13 2010 +0200
3.3 @@ -185,9 +185,9 @@
3.4 Calc("op +", eval_binop "#add_")
3.5 ],
3.6 srls = Erls, calc = [],
3.7 - rules = [Thm ("nth_Cons_",num_str nth_Cons_),
3.8 + rules = [Thm ("nth_Cons_",num_str @{nth_Cons_),
3.9 Calc("op +", eval_binop "#add_"),
3.10 - Thm ("nth_Nil_",num_str nth_Nil_),
3.11 + Thm ("nth_Nil_",num_str @{nth_Nil_),
3.12 Calc("Tools.lhs", eval_lhs"eval_lhs_"),
3.13 Calc("Tools.rhs", eval_rhs"eval_rhs_"),
3.14 Calc("Atools.argument'_in",
3.15 @@ -206,19 +206,19 @@
3.16 Calc("op +", eval_binop "#add_")
3.17 ],
3.18 srls = Erls, calc = [],
3.19 - rules = [Thm ("nth_Cons_",num_str nth_Cons_),
3.20 + rules = [Thm ("nth_Cons_",num_str @{nth_Cons_),
3.21 Calc("op +", eval_binop "#add_"),
3.22 - Thm ("nth_Nil_", num_str nth_Nil_),
3.23 + Thm ("nth_Nil_", num_str @{nth_Nil_),
3.24 Calc("Tools.lhs", eval_lhs "eval_lhs_"),
3.25 Calc("Atools.filter'_sameFunId",
3.26 eval_filter_sameFunId "Atools.filter'_sameFunId"),
3.27 (*WN070514 just for smltest/../biegelinie.sml ...*)
3.28 Calc("Atools.sameFunId", eval_sameFunId "Atools.sameFunId"),
3.29 - Thm ("filter_Cons", num_str filter_Cons),
3.30 - Thm ("filter_Nil", num_str filter_Nil),
3.31 - Thm ("if_True", num_str if_True),
3.32 - Thm ("if_False", num_str if_False),
3.33 - Thm ("hd_thm", num_str hd_thm)
3.34 + Thm ("filter_Cons", num_str @{filter_Cons),
3.35 + Thm ("filter_Nil", num_str @{filter_Nil),
3.36 + Thm ("if_True", num_str @{if_True),
3.37 + Thm ("if_False", num_str @{if_False),
3.38 + Thm ("hd_thm", num_str @{hd_thm)
3.39 ],
3.40 scr = EmptyScr};
3.41
3.42 @@ -235,8 +235,8 @@
3.43 {rew_ord'="tless_true",
3.44 rls' = append_rls "erls_IntegrierenUndK.." e_rls
3.45 [Calc ("Atools.ident",eval_ident "#ident_"),
3.46 - Thm ("not_true",num_str not_true),
3.47 - Thm ("not_false",num_str not_false)],
3.48 + Thm ("not_true",num_str @{not_true),
3.49 + Thm ("not_false",num_str @{not_false)],
3.50 calc = [], srls = srls, prls = Erls,
3.51 crls = Atools_erls, nrls = Erls},
3.52 "Script BiegelinieScript " ^
3.53 @@ -312,15 +312,15 @@
3.54 {rew_ord'="tless_true",
3.55 rls' = append_rls "erls_IntegrierenUndK.." e_rls
3.56 [Calc ("Atools.ident",eval_ident "#ident_"),
3.57 - Thm ("not_true",num_str not_true),
3.58 - Thm ("not_false",num_str not_false)],
3.59 + Thm ("not_true",num_str @{not_true),
3.60 + Thm ("not_false",num_str @{not_false)],
3.61 calc = [],
3.62 srls = append_rls "erls_IntegrierenUndK.." e_rls
3.63 [Calc("Tools.rhs", eval_rhs"eval_rhs_"),
3.64 Calc ("Atools.ident",eval_ident "#ident_"),
3.65 - Thm ("last_thmI",num_str last_thmI),
3.66 - Thm ("if_True",num_str if_True),
3.67 - Thm ("if_False",num_str if_False)
3.68 + Thm ("last_thmI",num_str @{last_thmI),
3.69 + Thm ("if_True",num_str @{if_True),
3.70 + Thm ("if_False",num_str @{if_False)
3.71 ],
3.72 prls = Erls, crls = Atools_erls, nrls = Erls},
3.73 "Script Biegelinie2Script " ^
3.74 @@ -395,8 +395,8 @@
3.75 {rew_ord'="tless_true",
3.76 rls' = append_rls "erls_ausBelastung" e_rls
3.77 [Calc ("Atools.ident",eval_ident "#ident_"),
3.78 - Thm ("not_true",num_str not_true),
3.79 - Thm ("not_false",num_str not_false)],
3.80 + Thm ("not_true",num_str @{not_true),
3.81 + Thm ("not_false",num_str @{not_false)],
3.82 calc = [],
3.83 srls = append_rls "srls_ausBelastung" e_rls
3.84 [Calc("Tools.rhs", eval_rhs"eval_rhs_")],
4.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue Aug 31 15:36:57 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Aug 31 16:00:13 2010 +0200
4.3 @@ -116,28 +116,28 @@
4.4 rew_ord = ("termlessI",termlessI),
4.5 erls = append_rls "erls_diff_conv" e_rls
4.6 [Calc ("Atools.occurs'_in", eval_occurs_in ""),
4.7 - Thm ("not_true",num_str not_true),
4.8 - Thm ("not_false",num_str not_false),
4.9 + Thm ("not_true",num_str @{not_true),
4.10 + Thm ("not_false",num_str @{not_false),
4.11 Calc ("op <",eval_equ "#less_"),
4.12 - Thm ("and_true",num_str and_true),
4.13 - Thm ("and_false",num_str and_false)
4.14 + Thm ("and_true",num_str @{and_true),
4.15 + Thm ("and_false",num_str @{and_false)
4.16 ],
4.17 srls = Erls, calc = [],
4.18 - rules = [Thm ("frac_conv", num_str frac_conv),
4.19 - Thm ("sqrt_conv_bdv", num_str sqrt_conv_bdv),
4.20 - Thm ("sqrt_conv_bdv_n", num_str sqrt_conv_bdv_n),
4.21 - Thm ("sqrt_conv", num_str sqrt_conv),
4.22 - Thm ("root_conv", num_str root_conv),
4.23 - Thm ("realpow_pow_bdv", num_str realpow_pow_bdv),
4.24 + rules = [Thm ("frac_conv", num_str @{frac_conv),
4.25 + Thm ("sqrt_conv_bdv", num_str @{sqrt_conv_bdv),
4.26 + Thm ("sqrt_conv_bdv_n", num_str @{sqrt_conv_bdv_n),
4.27 + Thm ("sqrt_conv", num_str @{sqrt_conv),
4.28 + Thm ("root_conv", num_str @{root_conv),
4.29 + Thm ("realpow_pow_bdv", num_str @{realpow_pow_bdv),
4.30 Calc ("op *", eval_binop "#mult_"),
4.31 - Thm ("rat_mult",num_str rat_mult),
4.32 + Thm ("rat_mult",num_str @{rat_mult),
4.33 (*a / b * (c / d) = a * c / (b * d)*)
4.34 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
4.35 (*?x * (?y / ?z) = ?x * ?y / ?z*)
4.36 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left})
4.37 (*?y / ?z * ?x = ?y * ?x / ?z*)
4.38 (*
4.39 - Thm ("", num_str ),*)
4.40 + Thm ("", num_str @{),*)
4.41 ],
4.42 scr = EmptyScr};
4.43
4.44 @@ -150,13 +150,13 @@
4.45 [Calc ("op <",eval_equ "#less_")
4.46 ],
4.47 srls = Erls, calc = [],
4.48 - rules = [Thm ("frac_sym_conv", num_str frac_sym_conv),
4.49 - Thm ("sqrt_sym_conv", num_str sqrt_sym_conv),
4.50 - Thm ("root_sym_conv", num_str root_sym_conv),
4.51 + rules = [Thm ("frac_sym_conv", num_str @{frac_sym_conv),
4.52 + Thm ("sqrt_sym_conv", num_str @{sqrt_sym_conv),
4.53 + Thm ("root_sym_conv", num_str @{root_sym_conv),
4.54 Thm ("sym_real_mult_minus1",
4.55 - num_str (real_mult_minus1 RS sym)),
4.56 + num_str @{(real_mult_minus1 RS sym)),
4.57 (*- ?z = "-1 * ?z"*)
4.58 - Thm ("rat_mult",num_str rat_mult),
4.59 + Thm ("rat_mult",num_str @{rat_mult),
4.60 (*a / b * (c / d) = a * c / (b * d)*)
4.61 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
4.62 (*?x * (?y / ?z) = ?x * ?y / ?z*)
4.63 @@ -182,8 +182,8 @@
4.64 (*..*)
4.65 val erls_diff =
4.66 append_rls "erls_differentiate.." e_rls
4.67 - [Thm ("not_true",num_str not_true),
4.68 - Thm ("not_false",num_str not_false),
4.69 + [Thm ("not_true",num_str @{not_true),
4.70 + Thm ("not_false",num_str @{not_false),
4.71
4.72 Calc ("Atools.ident",eval_ident "#ident_"),
4.73 Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
4.74 @@ -195,27 +195,27 @@
4.75 val diff_rules =
4.76 Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
4.77 erls = erls_diff, srls = Erls, calc = [],
4.78 - rules = [Thm ("diff_sum",num_str diff_sum),
4.79 - Thm ("diff_dif",num_str diff_dif),
4.80 - Thm ("diff_prod_const",num_str diff_prod_const),
4.81 - Thm ("diff_prod",num_str diff_prod),
4.82 - Thm ("diff_quot",num_str diff_quot),
4.83 - Thm ("diff_sin",num_str diff_sin),
4.84 - Thm ("diff_sin_chain",num_str diff_sin_chain),
4.85 - Thm ("diff_cos",num_str diff_cos),
4.86 - Thm ("diff_cos_chain",num_str diff_cos_chain),
4.87 - Thm ("diff_pow",num_str diff_pow),
4.88 - Thm ("diff_pow_chain",num_str diff_pow_chain),
4.89 - Thm ("diff_ln",num_str diff_ln),
4.90 - Thm ("diff_ln_chain",num_str diff_ln_chain),
4.91 - Thm ("diff_exp",num_str diff_exp),
4.92 - Thm ("diff_exp_chain",num_str diff_exp_chain),
4.93 + rules = [Thm ("diff_sum",num_str @{diff_sum),
4.94 + Thm ("diff_dif",num_str @{diff_dif),
4.95 + Thm ("diff_prod_const",num_str @{diff_prod_const),
4.96 + Thm ("diff_prod",num_str @{diff_prod),
4.97 + Thm ("diff_quot",num_str @{diff_quot),
4.98 + Thm ("diff_sin",num_str @{diff_sin),
4.99 + Thm ("diff_sin_chain",num_str @{diff_sin_chain),
4.100 + Thm ("diff_cos",num_str @{diff_cos),
4.101 + Thm ("diff_cos_chain",num_str @{diff_cos_chain),
4.102 + Thm ("diff_pow",num_str @{diff_pow),
4.103 + Thm ("diff_pow_chain",num_str @{diff_pow_chain),
4.104 + Thm ("diff_ln",num_str @{diff_ln),
4.105 + Thm ("diff_ln_chain",num_str @{diff_ln_chain),
4.106 + Thm ("diff_exp",num_str @{diff_exp),
4.107 + Thm ("diff_exp_chain",num_str @{diff_exp_chain),
4.108 (*
4.109 - Thm ("diff_sqrt",num_str diff_sqrt),
4.110 - Thm ("diff_sqrt_chain",num_str diff_sqrt_chain),
4.111 + Thm ("diff_sqrt",num_str @{diff_sqrt),
4.112 + Thm ("diff_sqrt_chain",num_str @{diff_sqrt_chain),
4.113 *)
4.114 - Thm ("diff_const",num_str diff_const),
4.115 - Thm ("diff_var",num_str diff_var)
4.116 + Thm ("diff_const",num_str @{diff_const),
4.117 + Thm ("diff_var",num_str @{diff_var)
4.118 ],
4.119 scr = EmptyScr};
4.120
5.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Tue Aug 31 15:36:57 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Aug 31 16:00:13 2010 +0200
5.3 @@ -51,17 +51,17 @@
5.4 val eval_rls = prep_rls(
5.5 Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI),
5.6 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
5.7 - rules = [Thm ("refl",num_str refl),
5.8 + rules = [Thm ("refl",num_str @{refl),
5.9 Thm ("real_le_refl",num_str @{thm real_le_refl}),
5.10 - Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
5.11 - Thm ("not_true",num_str not_true),
5.12 - Thm ("not_false",num_str not_false),
5.13 + Thm ("radd_left_cancel_le",num_str @{radd_left_cancel_le),
5.14 + Thm ("not_true",num_str @{not_true),
5.15 + Thm ("not_false",num_str @{not_false),
5.16 Thm ("and_true",and_true),
5.17 Thm ("and_false",and_false),
5.18 Thm ("or_true",or_true),
5.19 Thm ("or_false",or_false),
5.20 - Thm ("and_commute",num_str and_commute),
5.21 - Thm ("or_commute",num_str or_commute),
5.22 + Thm ("and_commute",num_str @{and_commute),
5.23 + Thm ("or_commute",num_str @{or_commute),
5.24
5.25 Calc ("op <",eval_equ "#less_"),
5.26 Calc ("op <=",eval_equ "#less_equal_"),
5.27 @@ -241,8 +241,8 @@
5.28 "empty_script"));
5.29
5.30 val list_rls = append_rls "list_rls" list_rls
5.31 - [Thm ("filterVar_Const", num_str filterVar_Const),
5.32 - Thm ("filterVar_Nil", num_str filterVar_Nil)
5.33 + [Thm ("filterVar_Const", num_str @{filterVar_Const),
5.34 + Thm ("filterVar_Nil", num_str @{filterVar_Nil)
5.35 ];
5.36 ruleset' := overwritelthy thy (!ruleset',
5.37 [("list_rls",list_rls)
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Aug 31 15:36:57 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Aug 31 16:00:13 2010 +0200
6.3 @@ -186,11 +186,11 @@
6.4 rew_ord = ("ord_simplify_System",
6.5 ord_simplify_System false (theory "Integrate")),
6.6 erls = e_rls,srls = Erls, calc = [],
6.7 - rules = [Thm ("real_mult_commute",num_str real_mult_commute),
6.8 + rules = [Thm ("real_mult_commute",num_str @{real_mult_commute),
6.9 (* z * w = w * z *)
6.10 - Thm ("real_mult_left_commute",num_str real_mult_left_commute),
6.11 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute),
6.12 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
6.13 - Thm ("real_mult_assoc",num_str real_mult_assoc),
6.14 + Thm ("real_mult_assoc",num_str @{real_mult_assoc),
6.15 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
6.16 Thm ("add_commute",num_str @{thm add_commute}),
6.17 (*z + w = w + z*)
6.18 @@ -263,7 +263,7 @@
6.19 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
6.20 Rls_ norm_Rational_noadd_fractions(**2**),
6.21 Rls_ (*order_add_mult_in*) norm_System_noadd_fractions (**1**),
6.22 - Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym))
6.23 + Thm ("sym_real_mult_assoc", num_str @{(real_mult_assoc RS sym))
6.24 (*Rls_ discard_parentheses *3**),
6.25 Rls_ collect_bdv, (*from make_polynomial_in WN051031 welldone?*)
6.26 Rls_ separate_bdv2,
6.27 @@ -290,7 +290,7 @@
6.28 (*
6.29 val simplify_System =
6.30 append_rls "simplify_System" simplify_System_parenthesized
6.31 - [Thm ("sym_real_add_assoc", num_str (real_add_assoc RS sym))];
6.32 + [Thm ("sym_real_add_assoc", num_str @{(real_add_assoc RS sym))];
6.33 *)
6.34
6.35 val isolate_bdvs =
6.36 @@ -303,9 +303,9 @@
6.37 ],
6.38 srls = Erls, calc = [],
6.39 rules = [Thm ("commute_0_equality",
6.40 - num_str commute_0_equality),
6.41 - Thm ("separate_bdvs_add", num_str separate_bdvs_add),
6.42 - Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)],
6.43 + num_str @{commute_0_equality),
6.44 + Thm ("separate_bdvs_add", num_str @{separate_bdvs_add),
6.45 + Thm ("separate_bdvs_mult", num_str @{separate_bdvs_mult)],
6.46 scr = EmptyScr};
6.47 val isolate_bdvs_4x4 =
6.48 Rls {id="isolate_bdvs_4x4", preconds = [],
6.49 @@ -317,16 +317,16 @@
6.50 Calc ("Atools.ident",eval_ident "#ident_"),
6.51 Calc ("Atools.some'_occur'_in",
6.52 eval_some_occur_in "#some_occur_in_"),
6.53 - Thm ("not_true",num_str not_true),
6.54 - Thm ("not_false",num_str not_false)
6.55 + Thm ("not_true",num_str @{not_true),
6.56 + Thm ("not_false",num_str @{not_false)
6.57 ],
6.58 srls = Erls, calc = [],
6.59 rules = [Thm ("commute_0_equality",
6.60 - num_str commute_0_equality),
6.61 - Thm ("separate_bdvs0", num_str separate_bdvs0),
6.62 - Thm ("separate_bdvs_add1", num_str separate_bdvs_add1),
6.63 - Thm ("separate_bdvs_add1", num_str separate_bdvs_add2),
6.64 - Thm ("separate_bdvs_mult", num_str separate_bdvs_mult)],
6.65 + num_str @{commute_0_equality),
6.66 + Thm ("separate_bdvs0", num_str @{separate_bdvs0),
6.67 + Thm ("separate_bdvs_add1", num_str @{separate_bdvs_add1),
6.68 + Thm ("separate_bdvs_add1", num_str @{separate_bdvs_add2),
6.69 + Thm ("separate_bdvs_mult", num_str @{separate_bdvs_mult)],
6.70 scr = EmptyScr};
6.71
6.72 (*.order the equations in a system such, that a triangular system (if any)
6.73 @@ -336,7 +336,7 @@
6.74 rew_ord = ("ord_simplify_System",
6.75 ord_simplify_System false thy),
6.76 erls = Erls, srls = Erls, calc = [],
6.77 - rules = [Thm ("order_system_NxN", num_str order_system_NxN)
6.78 + rules = [Thm ("order_system_NxN", num_str @{order_system_NxN)
6.79 ],
6.80 scr = EmptyScr};
6.81
6.82 @@ -354,11 +354,11 @@
6.83 ],
6.84 scr = EmptyScr},
6.85 srls = Erls, calc = [],
6.86 - rules = [Thm ("nth_Cons_",num_str nth_Cons_),
6.87 + rules = [Thm ("nth_Cons_",num_str @{nth_Cons_),
6.88 Calc ("op +", eval_binop "#add_"),
6.89 - Thm ("nth_Nil_",num_str nth_Nil_),
6.90 - Thm ("tl_Cons",num_str tl_Cons),
6.91 - Thm ("tl_Nil",num_str tl_Nil),
6.92 + Thm ("nth_Nil_",num_str @{nth_Nil_),
6.93 + Thm ("tl_Cons",num_str @{tl_Cons),
6.94 + Thm ("tl_Nil",num_str @{tl_Nil),
6.95 Calc ("EqSystem.occur'_exactly'_in",
6.96 eval_occur_exactly_in
6.97 "#eval_occur_exactly_in_")
6.98 @@ -381,11 +381,11 @@
6.99 ],
6.100 scr = EmptyScr},
6.101 srls = Erls, calc = [],
6.102 - rules = [Thm ("nth_Cons_",num_str nth_Cons_),
6.103 + rules = [Thm ("nth_Cons_",num_str @{nth_Cons_),
6.104 Calc ("op +", eval_binop "#add_"),
6.105 - Thm ("nth_Nil_",num_str nth_Nil_),
6.106 - Thm ("tl_Cons",num_str tl_Cons),
6.107 - Thm ("tl_Nil",num_str tl_Nil),
6.108 + Thm ("nth_Nil_",num_str @{nth_Nil_),
6.109 + Thm ("tl_Cons",num_str @{tl_Cons),
6.110 + Thm ("tl_Nil",num_str @{tl_Nil),
6.111 Calc ("EqSystem.occur'_exactly'_in",
6.112 eval_occur_exactly_in
6.113 "#eval_occur_exactly_in_")
6.114 @@ -436,8 +436,8 @@
6.115 ("#Find" ,["solution ss___"])
6.116 ],
6.117 append_rls "prls_2x2_linear_system" e_rls
6.118 - [Thm ("length_Cons_",num_str length_Cons_),
6.119 - Thm ("length_Nil_",num_str length_Nil_),
6.120 + [Thm ("length_Cons_",num_str @{length_Cons_),
6.121 + Thm ("length_Nil_",num_str @{length_Nil_),
6.122 Calc ("op +", eval_binop "#add_"),
6.123 Calc ("op =",eval_equal "#equal_")
6.124 ],
6.125 @@ -473,8 +473,8 @@
6.126 ("#Find" ,["solution ss___"])
6.127 ],
6.128 append_rls "prls_3x3_linear_system" e_rls
6.129 - [Thm ("length_Cons_",num_str length_Cons_),
6.130 - Thm ("length_Nil_",num_str length_Nil_),
6.131 + [Thm ("length_Cons_",num_str @{length_Cons_),
6.132 + Thm ("length_Nil_",num_str @{length_Nil_),
6.133 Calc ("op +", eval_binop "#add_"),
6.134 Calc ("op =",eval_equal "#equal_")
6.135 ],
6.136 @@ -489,8 +489,8 @@
6.137 ("#Find" ,["solution ss___"])
6.138 ],
6.139 append_rls "prls_4x4_linear_system" e_rls
6.140 - [Thm ("length_Cons_",num_str length_Cons_),
6.141 - Thm ("length_Nil_",num_str length_Nil_),
6.142 + [Thm ("length_Cons_",num_str @{length_Cons_),
6.143 + Thm ("length_Nil_",num_str @{length_Nil_),
6.144 Calc ("op +", eval_binop "#add_"),
6.145 Calc ("op =",eval_equal "#equal_")
6.146 ],
6.147 @@ -557,9 +557,9 @@
6.148 ],
6.149 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [],
6.150 srls = append_rls "srls_top_down_2x2" e_rls
6.151 - [Thm ("hd_thm",num_str hd_thm),
6.152 - Thm ("tl_Cons",num_str tl_Cons),
6.153 - Thm ("tl_Nil",num_str tl_Nil)
6.154 + [Thm ("hd_thm",num_str @{hd_thm),
6.155 + Thm ("tl_Cons",num_str @{tl_Cons),
6.156 + Thm ("tl_Nil",num_str @{tl_Nil)
6.157 ],
6.158 prls = prls_triangular, crls = Erls, nrls = Erls},
6.159 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
6.160 @@ -611,9 +611,9 @@
6.161 ("#Find" ,["solution ss___"])],
6.162 {rew_ord'="tless_true", rls' = Erls, calc = [],
6.163 srls = append_rls "srls_normalize_2x2" e_rls
6.164 - [Thm ("hd_thm",num_str hd_thm),
6.165 - Thm ("tl_Cons",num_str tl_Cons),
6.166 - Thm ("tl_Nil",num_str tl_Nil)
6.167 + [Thm ("hd_thm",num_str @{hd_thm),
6.168 + Thm ("tl_Cons",num_str @{tl_Cons),
6.169 + Thm ("tl_Nil",num_str @{tl_Nil)
6.170 ],
6.171 prls = Erls, crls = Erls, nrls = Erls},
6.172 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^
6.173 @@ -640,9 +640,9 @@
6.174 Calc("op +", eval_binop "#add_")
6.175 ],
6.176 srls = Erls, calc = [],
6.177 - rules = [Thm ("nth_Cons_",num_str nth_Cons_),
6.178 + rules = [Thm ("nth_Cons_",num_str @{nth_Cons_),
6.179 Calc("op +", eval_binop "#add_"),
6.180 - Thm ("nth_Nil_",num_str nth_Nil_)],
6.181 + Thm ("nth_Nil_",num_str @{nth_Nil_)],
6.182 scr = EmptyScr};
6.183 store_met
6.184 (prep_met (theory "EqSystem") "met_eqsys_norm_4x4" [] e_metID
6.185 @@ -651,9 +651,9 @@
6.186 ("#Find" ,["solution ss___"])],
6.187 {rew_ord'="tless_true", rls' = Erls, calc = [],
6.188 srls = append_rls "srls_normalize_4x4" srls
6.189 - [Thm ("hd_thm",num_str hd_thm),
6.190 - Thm ("tl_Cons",num_str tl_Cons),
6.191 - Thm ("tl_Nil",num_str tl_Nil)
6.192 + [Thm ("hd_thm",num_str @{hd_thm),
6.193 + Thm ("tl_Cons",num_str @{tl_Cons),
6.194 + Thm ("tl_Nil",num_str @{tl_Nil)
6.195 ],
6.196 prls = Erls, crls = Erls, nrls = Erls},
6.197 (*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*)
7.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Tue Aug 31 15:36:57 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Aug 31 16:00:13 2010 +0200
7.3 @@ -127,17 +127,17 @@
7.4 rules = [(*for rewriting conditions in Thm's*)
7.5 Calc ("Atools.occurs'_in",
7.6 eval_occurs_in "#occurs_in_"),
7.7 - Thm ("not_true",num_str not_true),
7.8 + Thm ("not_true",num_str @{not_true),
7.9 Thm ("not_false",not_false)
7.10 ],
7.11 scr = EmptyScr},
7.12 srls = Erls, calc = [],
7.13 rules = [
7.14 - Thm ("integral_const",num_str integral_const),
7.15 - Thm ("integral_var",num_str integral_var),
7.16 - Thm ("integral_add",num_str integral_add),
7.17 - Thm ("integral_mult",num_str integral_mult),
7.18 - Thm ("integral_pow",num_str integral_pow),
7.19 + Thm ("integral_const",num_str @{integral_const),
7.20 + Thm ("integral_var",num_str @{integral_var),
7.21 + Thm ("integral_add",num_str @{integral_add),
7.22 + Thm ("integral_mult",num_str @{integral_mult),
7.23 + Thm ("integral_pow",num_str @{integral_pow),
7.24 Calc ("op +", eval_binop "#add_")(*for n+1*)
7.25 ],
7.26 scr = EmptyScr};
7.27 @@ -152,12 +152,12 @@
7.28 rules = [Calc ("Tools.matches", eval_matches""),
7.29 Calc ("Integrate.is'_f'_x",
7.30 eval_is_f_x "is_f_x_"),
7.31 - Thm ("not_true",num_str not_true),
7.32 - Thm ("not_false",num_str not_false)
7.33 + Thm ("not_true",num_str @{not_true),
7.34 + Thm ("not_false",num_str @{not_false)
7.35 ],
7.36 scr = EmptyScr},
7.37 srls = Erls, calc = [],
7.38 - rules = [ (*Thm ("call_for_new_c", num_str call_for_new_c),*)
7.39 + rules = [ (*Thm ("call_for_new_c", num_str @{call_for_new_c),*)
7.40 Cal1 ("Integrate.add'_new'_c", eval_add_new_c "new_c_")
7.41 ],
7.42 scr = EmptyScr};
7.43 @@ -178,11 +178,11 @@
7.44 [Calc ("Poly.is'_polyexp",
7.45 eval_is_polyexp "")],
7.46 srls = Erls, calc = [],
7.47 - rules = [Thm ("rat_mult",num_str rat_mult),
7.48 + rules = [Thm ("rat_mult",num_str @{rat_mult),
7.49 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
7.50 - Thm ("rat_mult_poly_l",num_str rat_mult_poly_l),
7.51 + Thm ("rat_mult_poly_l",num_str @{rat_mult_poly_l),
7.52 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
7.53 - Thm ("rat_mult_poly_r",num_str rat_mult_poly_r),
7.54 + Thm ("rat_mult_poly_r",num_str @{rat_mult_poly_r),
7.55 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
7.56
7.57 Thm ("real_divide_divide1_mg", real_divide_divide1_mg),
7.58 @@ -193,7 +193,7 @@
7.59 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
7.60 Calc ("HOL.divide" ,eval_cancel "#divide_"),
7.61
7.62 - Thm ("rat_power", num_str rat_power)
7.63 + Thm ("rat_power", num_str @{rat_power)
7.64 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
7.65 ],
7.66 scr = Script ((term_of o the o (parse thy)) "empty_script")
7.67 @@ -229,12 +229,12 @@
7.68 val separate_bdv2 =
7.69 append_rls "separate_bdv2"
7.70 collect_bdv
7.71 - [Thm ("separate_bdv", num_str separate_bdv),
7.72 + [Thm ("separate_bdv", num_str @{separate_bdv),
7.73 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
7.74 - Thm ("separate_bdv_n", num_str separate_bdv_n),
7.75 - Thm ("separate_1_bdv", num_str separate_1_bdv),
7.76 + Thm ("separate_bdv_n", num_str @{separate_bdv_n),
7.77 + Thm ("separate_1_bdv", num_str @{separate_1_bdv),
7.78 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
7.79 - Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
7.80 + Thm ("separate_1_bdv_n", num_str @{separate_1_bdv_n)(*,
7.81 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
7.82 *****Thm ("nadd_divide_distrib",
7.83 *****num_str @{thm nadd_divide_distrib})
7.84 @@ -276,18 +276,18 @@
7.85 * Rls_ simplify_power,
7.86 * Rls_ collect_numerals,
7.87 * Rls_ reduce_012,
7.88 -* Thm ("realpow_oneI",num_str realpow_oneI),
7.89 +* Thm ("realpow_oneI",num_str @{realpow_oneI),
7.90 * Rls_ discard_parentheses,
7.91 * Rls_ collect_bdv,
7.92 * (*below inserted from 'make_ratpoly_in'*)
7.93 * Rls_ (append_rls "separate_bdv"
7.94 * collect_bdv
7.95 -* [Thm ("separate_bdv", num_str separate_bdv),
7.96 +* [Thm ("separate_bdv", num_str @{separate_bdv),
7.97 * (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
7.98 -* Thm ("separate_bdv_n", num_str separate_bdv_n),
7.99 -* Thm ("separate_1_bdv", num_str separate_1_bdv),
7.100 +* Thm ("separate_bdv_n", num_str @{separate_bdv_n),
7.101 +* Thm ("separate_1_bdv", num_str @{separate_1_bdv),
7.102 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
7.103 -* Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
7.104 +* Thm ("separate_1_bdv_n", num_str @{separate_1_bdv_n)(*,
7.105 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
7.106 * Thm ("nadd_divide_distrib",
7.107 * num_str @{thm nadd_divide_distrib})
8.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Tue Aug 31 15:36:57 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Tue Aug 31 16:00:13 2010 +0200
8.3 @@ -40,17 +40,17 @@
8.4 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
8.5 Calc ("Atools.occurs'_in",eval_occurs_in ""),
8.6 Calc ("Atools.ident",eval_ident "#ident_"),
8.7 - Thm ("not_true",num_str not_true),
8.8 - Thm ("not_false",num_str not_false),
8.9 - Thm ("and_true",num_str and_true),
8.10 - Thm ("and_false",num_str and_false),
8.11 - Thm ("or_true",num_str or_true),
8.12 - Thm ("or_false",num_str or_false)
8.13 + Thm ("not_true",num_str @{not_true),
8.14 + Thm ("not_false",num_str @{not_false),
8.15 + Thm ("and_true",num_str @{and_true),
8.16 + Thm ("and_false",num_str @{and_false),
8.17 + Thm ("or_true",num_str @{or_true),
8.18 + Thm ("or_false",num_str @{or_false)
8.19 ];
8.20 (* ----- erls ----- *)
8.21 val LinEq_crls =
8.22 append_rls "LinEq_crls" poly_crls
8.23 - [Thm ("real_assoc_1",num_str real_assoc_1)
8.24 + [Thm ("real_assoc_1",num_str @{real_assoc_1)
8.25 (*
8.26 Don't use
8.27 Calc ("HOL.divide", eval_cancel "#divide_"),
8.28 @@ -61,7 +61,7 @@
8.29 (* ----- crls ----- *)
8.30 val LinEq_erls =
8.31 append_rls "LinEq_erls" Poly_erls
8.32 - [Thm ("real_assoc_1",num_str real_assoc_1)
8.33 + [Thm ("real_assoc_1",num_str @{real_assoc_1)
8.34 (*
8.35 Don't use
8.36 Calc ("HOL.divide", eval_cancel "#divide_"),
8.37 @@ -81,7 +81,7 @@
8.38 calc = [],
8.39 (*asm_thm = [],*)
8.40 rules = [
8.41 - Thm ("real_assoc_1",num_str real_assoc_1),
8.42 + Thm ("real_assoc_1",num_str @{real_assoc_1),
8.43 Calc ("op +",eval_binop "#add_"),
8.44 Calc ("op -",eval_binop "#sub_"),
8.45 Calc ("op *",eval_binop "#mult_"),
8.46 @@ -105,11 +105,11 @@
8.47 calc = [],
8.48 (*asm_thm = [("lin_isolate_div","")],*)
8.49 rules = [
8.50 - Thm("lin_isolate_add1",num_str lin_isolate_add1),
8.51 + Thm("lin_isolate_add1",num_str @{lin_isolate_add1),
8.52 (* a+bx=0 -> bx=-a *)
8.53 - Thm("lin_isolate_add2",num_str lin_isolate_add2),
8.54 + Thm("lin_isolate_add2",num_str @{lin_isolate_add2),
8.55 (* a+ x=0 -> x=-a *)
8.56 - Thm("lin_isolate_div",num_str lin_isolate_div)
8.57 + Thm("lin_isolate_div",num_str @{lin_isolate_div)
8.58 (* bx=c -> x=c/b *)
8.59 ],
8.60 scr = Script ((term_of o the o (parse thy)) "empty_script")
9.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Aug 31 15:36:57 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Aug 31 16:00:13 2010 +0200
9.3 @@ -391,7 +391,7 @@
9.4 val Poly_erls =
9.5 append_rls "Poly_erls" Atools_erls
9.6 [ Calc ("op =",eval_equal "#equal_"),
9.7 - Thm ("real_unari_minus",num_str real_unari_minus),
9.8 + Thm ("real_unari_minus",num_str @{real_unari_minus),
9.9 Calc ("op +",eval_binop "#add_"),
9.10 Calc ("op -",eval_binop "#sub_"),
9.11 Calc ("op *",eval_binop "#mult_"),
9.12 @@ -401,7 +401,7 @@
9.13 val poly_crls =
9.14 append_rls "poly_crls" Atools_crls
9.15 [ Calc ("op =",eval_equal "#equal_"),
9.16 - Thm ("real_unari_minus",num_str real_unari_minus),
9.17 + Thm ("real_unari_minus",num_str @{real_unari_minus),
9.18 Calc ("op +",eval_binop "#add_"),
9.19 Calc ("op -",eval_binop "#sub_"),
9.20 Calc ("op *",eval_binop "#mult_"),
9.21 @@ -505,9 +505,9 @@
9.22 erls = e_rls,srls = Erls,
9.23 calc = [],
9.24 (*asm_thm = [],*)
9.25 - rules = [Thm ("real_diff_minus",num_str real_diff_minus),
9.26 + rules = [Thm ("real_diff_minus",num_str @{real_diff_minus),
9.27 (*"a - b = a + -1 * b"*)
9.28 - Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
9.29 + Thm ("sym_real_mult_minus1",num_str @{(real_mult_minus1 RS sym))
9.30 (*- ?z = "-1 * ?z"*)
9.31 ], scr = EmptyScr}:rls;
9.32 val expand_poly_ =
9.33 @@ -516,23 +516,23 @@
9.34 erls = e_rls,srls = Erls,
9.35 calc = [],
9.36 (*asm_thm = [],*)
9.37 - rules = [Thm ("real_plus_binom_pow4",num_str real_plus_binom_pow4),
9.38 + rules = [Thm ("real_plus_binom_pow4",num_str @{real_plus_binom_pow4),
9.39 (*"(a + b)^^^4 = ... "*)
9.40 - Thm ("real_plus_binom_pow5",num_str real_plus_binom_pow5),
9.41 + Thm ("real_plus_binom_pow5",num_str @{real_plus_binom_pow5),
9.42 (*"(a + b)^^^5 = ... "*)
9.43 - Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
9.44 + Thm ("real_plus_binom_pow3",num_str @{real_plus_binom_pow3),
9.45 (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
9.46
9.47 (*WN071229 changed/removed for Schaerding -----vvv*)
9.48 - (*Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),*)
9.49 + (*Thm ("real_plus_binom_pow2",num_str @{real_plus_binom_pow2),*)
9.50 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
9.51 - Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
9.52 + Thm ("real_plus_binom_pow2",num_str @{real_plus_binom_pow2),
9.53 (*"(a + b)^^^2 = (a + b) * (a + b)"*)
9.54 (*Thm ("real_plus_minus_binom1_p_p",
9.55 - num_str real_plus_minus_binom1_p_p),*)
9.56 + num_str @{real_plus_minus_binom1_p_p),*)
9.57 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
9.58 (*Thm ("real_plus_minus_binom2_p_p",
9.59 - num_str real_plus_minus_binom2_p_p),*)
9.60 + num_str @{real_plus_minus_binom2_p_p),*)
9.61 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
9.62 (*WN071229 changed/removed for Schaerding -----^^^*)
9.63
9.64 @@ -541,9 +541,9 @@
9.65 Thm ("left_distrib2",num_str @{thm left_distrib}2),
9.66 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
9.67
9.68 - Thm ("realpow_multI", num_str realpow_multI),
9.69 + Thm ("realpow_multI", num_str @{realpow_multI),
9.70 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
9.71 - Thm ("realpow_pow",num_str realpow_pow)
9.72 + Thm ("realpow_pow",num_str @{realpow_pow)
9.73 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
9.74 ], scr = EmptyScr}:rls;
9.75
9.76 @@ -586,19 +586,19 @@
9.77 calc = [],
9.78 (*asm_thm = [],*)
9.79 rules =
9.80 - [Thm ("real_plus_binom_pow4_poly", num_str real_plus_binom_pow4_poly),
9.81 + [Thm ("real_plus_binom_pow4_poly", num_str @{real_plus_binom_pow4_poly),
9.82 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
9.83 - Thm ("real_plus_binom_pow5_poly", num_str real_plus_binom_pow5_poly),
9.84 + Thm ("real_plus_binom_pow5_poly", num_str @{real_plus_binom_pow5_poly),
9.85 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
9.86 - Thm ("real_plus_binom_pow2_poly",num_str real_plus_binom_pow2_poly),
9.87 + Thm ("real_plus_binom_pow2_poly",num_str @{real_plus_binom_pow2_poly),
9.88 (*"[| a is_polyexp; b is_polyexp |] ==>
9.89 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
9.90 - Thm ("real_plus_binom_pow3_poly",num_str real_plus_binom_pow3_poly),
9.91 + Thm ("real_plus_binom_pow3_poly",num_str @{real_plus_binom_pow3_poly),
9.92 (*"[| a is_polyexp; b is_polyexp |] ==>
9.93 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
9.94 - Thm ("real_plus_minus_binom1_p_p",num_str real_plus_minus_binom1_p_p),
9.95 + Thm ("real_plus_minus_binom1_p_p",num_str @{real_plus_minus_binom1_p_p),
9.96 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
9.97 - Thm ("real_plus_minus_binom2_p_p",num_str real_plus_minus_binom2_p_p),
9.98 + Thm ("real_plus_minus_binom2_p_p",num_str @{real_plus_minus_binom2_p_p),
9.99 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
9.100
9.101 Thm ("left_distrib_poly" ,num_str @{thm left_distrib}_poly),
9.102 @@ -606,10 +606,10 @@
9.103 Thm("left_distrib2_poly",num_str @{thm left_distrib}2_poly),
9.104 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
9.105
9.106 - Thm ("realpow_multI_poly", num_str realpow_multI_poly),
9.107 + Thm ("realpow_multI_poly", num_str @{realpow_multI_poly),
9.108 (*"[| r is_polyexp; s is_polyexp |] ==>
9.109 (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
9.110 - Thm ("realpow_pow",num_str realpow_pow)
9.111 + Thm ("realpow_pow",num_str @{realpow_pow)
9.112 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
9.113 ], scr = EmptyScr}:rls;
9.114
9.115 @@ -621,27 +621,27 @@
9.116 (*asm_thm = [],*)
9.117 rules = [(*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
9.118 a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
9.119 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
9.120 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
9.121 (*"r * r = r ^^^ 2"*)
9.122 - Thm ("realpow_twoI_assoc_l",num_str realpow_twoI_assoc_l),
9.123 + Thm ("realpow_twoI_assoc_l",num_str @{realpow_twoI_assoc_l),
9.124 (*"r * (r * s) = r ^^^ 2 * s"*)
9.125
9.126 - Thm ("realpow_plus_1",num_str realpow_plus_1),
9.127 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
9.128 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
9.129 - Thm ("realpow_plus_1_assoc_l", num_str realpow_plus_1_assoc_l),
9.130 + Thm ("realpow_plus_1_assoc_l", num_str @{realpow_plus_1_assoc_l),
9.131 (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
9.132 (*MG 9.7.03: neues Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
9.133 - Thm ("realpow_plus_1_assoc_l2", num_str realpow_plus_1_assoc_l2),
9.134 + Thm ("realpow_plus_1_assoc_l2", num_str @{realpow_plus_1_assoc_l2),
9.135 (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
9.136
9.137 - Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)),
9.138 + Thm ("sym_realpow_addI",num_str @{(realpow_addI RS sym)),
9.139 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
9.140 - Thm ("realpow_addI_assoc_l", num_str realpow_addI_assoc_l),
9.141 + Thm ("realpow_addI_assoc_l", num_str @{realpow_addI_assoc_l),
9.142 (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
9.143
9.144 (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
9.145 "r * r = r ^^^ 2" wenn r=a^^^b*)
9.146 - Thm ("realpow_pow",num_str realpow_pow)
9.147 + Thm ("realpow_pow",num_str @{realpow_pow)
9.148 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
9.149 ], scr = EmptyScr}:rls;
9.150
9.151 @@ -668,11 +668,11 @@
9.152 rules = [(* MG: folgende Thm müssen hier stehen bleiben: *)
9.153 Thm ("mult_1_right",num_str @{thm mult_1_right}),
9.154 (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
9.155 - Thm ("realpow_zeroI",num_str realpow_zeroI),
9.156 + Thm ("realpow_zeroI",num_str @{realpow_zeroI),
9.157 (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
9.158 - Thm ("realpow_oneI",num_str realpow_oneI),
9.159 + Thm ("realpow_oneI",num_str @{realpow_oneI),
9.160 (*"r ^^^ 1 = r"*)
9.161 - Thm ("realpow_eq_oneI",num_str realpow_eq_oneI)
9.162 + Thm ("realpow_eq_oneI",num_str @{realpow_eq_oneI)
9.163 (*"1 ^^^ n = 1"*)
9.164 ], scr = EmptyScr}:rls;
9.165
9.166 @@ -683,23 +683,23 @@
9.167 calc = [("PLUS" , ("op +", eval_binop "#add_"))
9.168 ],
9.169 rules =
9.170 - [Thm ("real_num_collect",num_str real_num_collect),
9.171 + [Thm ("real_num_collect",num_str @{real_num_collect),
9.172 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
9.173 - Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
9.174 + Thm ("real_num_collect_assoc_r",num_str @{real_num_collect_assoc_r),
9.175 (*"[| l is_const; m is_const |] ==> \
9.176 \(k + m * n) + l * n = k + (l + m)*n"*)
9.177 - Thm ("real_one_collect",num_str real_one_collect),
9.178 + Thm ("real_one_collect",num_str @{real_one_collect),
9.179 (*"m is_const ==> n + m * n = (1 + m) * n"*)
9.180 - Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
9.181 + Thm ("real_one_collect_assoc_r",num_str @{real_one_collect_assoc_r),
9.182 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
9.183
9.184 Calc ("op +", eval_binop "#add_"),
9.185
9.186 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
9.187 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
9.188 - Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
9.189 + Thm ("real_mult_2_assoc_r",num_str @{real_mult_2_assoc_r),
9.190 (*"(k + z1) + z1 = k + 2 * z1"*)
9.191 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym))
9.192 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym))
9.193 (*"z1 + z1 = 2 * z1"*)
9.194 ], scr = EmptyScr}:rls;
9.195
9.196 @@ -720,7 +720,7 @@
9.197 Thm ("add_0_right",num_str @{thm add_0_right}),
9.198 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
9.199
9.200 - (*Thm ("realpow_oneI",num_str realpow_oneI)*)
9.201 + (*Thm ("realpow_oneI",num_str @{realpow_oneI)*)
9.202 (*"?r ^^^ 1 = ?r"*)
9.203 Thm ("divide_zero_left",num_str @{thm divide_zero_left})(*WN060914*)
9.204 (*"0 / ?x = 0"*)
9.205 @@ -729,9 +729,9 @@
9.206 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
9.207 val discard_parentheses_ =
9.208 append_rls "discard_parentheses_" e_rls
9.209 - [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym))
9.210 + [Thm ("sym_real_mult_assoc", num_str @{(real_mult_assoc RS sym))
9.211 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
9.212 - (*Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))*)
9.213 + (*Thm ("sym_real_add_assoc",num_str @{(real_add_assoc RS sym))*)
9.214 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
9.215 ];
9.216
9.217 @@ -747,22 +747,22 @@
9.218 ("POWER", ("Atools.pow", eval_binop "#power_"))
9.219 ],
9.220 (*asm_thm = [],*)
9.221 - rules = [Thm ("real_num_collect",num_str real_num_collect),
9.222 + rules = [Thm ("real_num_collect",num_str @{real_num_collect),
9.223 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
9.224 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
9.225 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
9.226 (*"[| l is_const; m is_const |] ==>
9.227 l * n + (m * n + k) = (l + m) * n + k"*)
9.228 - Thm ("real_one_collect",num_str real_one_collect),
9.229 + Thm ("real_one_collect",num_str @{real_one_collect),
9.230 (*"m is_const ==> n + m * n = (1 + m) * n"*)
9.231 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
9.232 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
9.233 (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
9.234
9.235 Calc ("op +", eval_binop "#add_"),
9.236
9.237 (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
9.238 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
9.239 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
9.240 (*"z1 + z1 = 2 * z1"*)
9.241 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc)
9.242 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc)
9.243 (*"z1 + (z1 + k) = 2 * z1 + k"*)
9.244 ], scr = EmptyScr}:rls;*)
9.245
9.246 @@ -779,31 +779,31 @@
9.247 (*Thm ("left_distrib1",num_str @{thm left_distrib}1),
9.248 ....... 18.3.03 undefined???*)
9.249
9.250 - Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
9.251 + Thm ("real_plus_binom_pow2",num_str @{real_plus_binom_pow2),
9.252 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
9.253 - Thm ("real_minus_binom_pow2_p",num_str real_minus_binom_pow2_p),
9.254 + Thm ("real_minus_binom_pow2_p",num_str @{real_minus_binom_pow2_p),
9.255 (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
9.256 Thm ("real_plus_minus_binom1_p",
9.257 - num_str real_plus_minus_binom1_p),
9.258 + num_str @{real_plus_minus_binom1_p),
9.259 (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
9.260 Thm ("real_plus_minus_binom2_p",
9.261 - num_str real_plus_minus_binom2_p),
9.262 + num_str @{real_plus_minus_binom2_p),
9.263 (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
9.264
9.265 Thm ("minus_minus",num_str @{thm minus_minus}),
9.266 (*"- (- ?z) = ?z"*)
9.267 - Thm ("real_diff_minus",num_str real_diff_minus),
9.268 + Thm ("real_diff_minus",num_str @{real_diff_minus),
9.269 (*"a - b = a + -1 * b"*)
9.270 - Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
9.271 + Thm ("sym_real_mult_minus1",num_str @{(real_mult_minus1 RS sym))
9.272 (*- ?z = "-1 * ?z"*)
9.273
9.274 - (*Thm ("",num_str ),
9.275 - Thm ("",num_str ),
9.276 - Thm ("",num_str ),*)
9.277 + (*Thm ("",num_str @{),
9.278 + Thm ("",num_str @{),
9.279 + Thm ("",num_str @{),*)
9.280 (*Thm ("real_minus_add_distrib",
9.281 - num_str real_minus_add_distrib),*)
9.282 + num_str @{real_minus_add_distrib),*)
9.283 (*"- (?x + ?y) = - ?x + - ?y"*)
9.284 - (*Thm ("real_diff_plus",num_str real_diff_plus)*)
9.285 + (*Thm ("real_diff_plus",num_str @{real_diff_plus)*)
9.286 (*"a - b = a + -b"*)
9.287 ], scr = EmptyScr}:rls;
9.288
9.289 @@ -813,20 +813,20 @@
9.290 erls = e_rls, srls = Erls,
9.291 calc = [],
9.292 (*asm_thm = [],*)
9.293 - rules = [Thm ("realpow_multI", num_str realpow_multI),
9.294 + rules = [Thm ("realpow_multI", num_str @{realpow_multI),
9.295 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
9.296
9.297 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
9.298 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
9.299 (*"r1 * r1 = r1 ^^^ 2"*)
9.300 - Thm ("realpow_plus_1",num_str realpow_plus_1),
9.301 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
9.302 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
9.303 - Thm ("realpow_pow",num_str realpow_pow),
9.304 + Thm ("realpow_pow",num_str @{realpow_pow),
9.305 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
9.306 - Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)),
9.307 + Thm ("sym_realpow_addI",num_str @{(realpow_addI RS sym)),
9.308 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
9.309 - Thm ("realpow_oneI",num_str realpow_oneI),
9.310 + Thm ("realpow_oneI",num_str @{realpow_oneI),
9.311 (*"r ^^^ 1 = r"*)
9.312 - Thm ("realpow_eq_oneI",num_str realpow_eq_oneI)
9.313 + Thm ("realpow_eq_oneI",num_str @{realpow_eq_oneI)
9.314 (*"1 ^^^ n = 1"*)
9.315 ], scr = EmptyScr}:rls;
9.316 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
9.317 @@ -837,11 +837,11 @@
9.318 erls = e_rls,srls = Erls,
9.319 calc = [],
9.320 (*asm_thm = [],*)
9.321 - rules = [Thm ("real_mult_commute",num_str real_mult_commute),
9.322 + rules = [Thm ("real_mult_commute",num_str @{real_mult_commute),
9.323 (* z * w = w * z *)
9.324 - Thm ("real_mult_left_commute",num_str real_mult_left_commute),
9.325 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute),
9.326 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
9.327 - Thm ("real_mult_assoc",num_str real_mult_assoc),
9.328 + Thm ("real_mult_assoc",num_str @{real_mult_assoc),
9.329 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
9.330 Thm ("add_commute",num_str @{thm add_commute}),
9.331 (*z + w = w + z*)
9.332 @@ -858,11 +858,11 @@
9.333 erls = e_rls,srls = Erls,
9.334 calc = [],
9.335 (*asm_thm = [],*)
9.336 - rules = [Thm ("real_mult_commute",num_str real_mult_commute),
9.337 + rules = [Thm ("real_mult_commute",num_str @{real_mult_commute),
9.338 (* z * w = w * z *)
9.339 - Thm ("real_mult_left_commute",num_str real_mult_left_commute),
9.340 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute),
9.341 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
9.342 - Thm ("real_mult_assoc",num_str real_mult_assoc)
9.343 + Thm ("real_mult_assoc",num_str @{real_mult_assoc)
9.344 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
9.345 ], scr = EmptyScr}:rls;
9.346 val collect_numerals =
9.347 @@ -874,14 +874,14 @@
9.348 ("POWER", ("Atools.pow", eval_binop "#power_"))
9.349 ],
9.350 (*asm_thm = [],*)
9.351 - rules = [Thm ("real_num_collect",num_str real_num_collect),
9.352 + rules = [Thm ("real_num_collect",num_str @{real_num_collect),
9.353 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
9.354 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
9.355 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
9.356 (*"[| l is_const; m is_const |] ==>
9.357 l * n + (m * n + k) = (l + m) * n + k"*)
9.358 - Thm ("real_one_collect",num_str real_one_collect),
9.359 + Thm ("real_one_collect",num_str @{real_one_collect),
9.360 (*"m is_const ==> n + m * n = (1 + m) * n"*)
9.361 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
9.362 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
9.363 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
9.364 Calc ("op +", eval_binop "#add_"),
9.365 Calc ("op *", eval_binop "#mult_"),
9.366 @@ -895,12 +895,12 @@
9.367 (*asm_thm = [],*)
9.368 rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
9.369 (*"1 * z = z"*)
9.370 - (*Thm ("real_mult_minus1",num_str real_mult_minus1),14.3.03*)
9.371 + (*Thm ("real_mult_minus1",num_str @{real_mult_minus1),14.3.03*)
9.372 (*"-1 * z = - z"*)
9.373 Thm ("minus_mult_left",
9.374 - num_str (real_mult_minus_eq1 RS sym)),
9.375 + num_str @{(real_mult_minus_eq1 RS sym)),
9.376 (*- (?x * ?y) = "- ?x * ?y"*)
9.377 - (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel),
9.378 + (*Thm ("real_minus_mult_cancel",num_str @{real_minus_mult_cancel),
9.379 (*"- ?x * - ?y = ?x * ?y"*)---*)
9.380 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
9.381 (*"0 * z = 0"*)
9.382 @@ -908,16 +908,16 @@
9.383 (*"0 + z = z"*)
9.384 Thm ("right_minus",num_str @{thm right_minus}),
9.385 (*"?z + - ?z = 0"*)
9.386 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
9.387 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
9.388 (*"z1 + z1 = 2 * z1"*)
9.389 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc)
9.390 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc)
9.391 (*"z1 + (z1 + k) = 2 * z1 + k"*)
9.392 ], scr = EmptyScr}:rls;
9.393 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
9.394 val discard_parentheses =
9.395 append_rls "discard_parentheses" e_rls
9.396 - [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym)),
9.397 - Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))];
9.398 + [Thm ("sym_real_mult_assoc", num_str @{(real_mult_assoc RS sym)),
9.399 + Thm ("sym_real_add_assoc",num_str @{(real_add_assoc RS sym))];
9.400
9.401 val scr_make_polynomial =
9.402 "Script Expand_binoms t_ = " ^
9.403 @@ -967,7 +967,7 @@
9.404 Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
9.405 Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
9.406 Rls_ reduce_012,
9.407 - Thm ("realpow_oneI",num_str realpow_oneI),(*in --^*)
9.408 + Thm ("realpow_oneI",num_str @{realpow_oneI),(*in --^*)
9.409 Rls_ discard_parentheses
9.410 ],
9.411 scr = EmptyScr
9.412 @@ -1015,32 +1015,32 @@
9.413 ("POWER", ("Atools.pow", eval_binop "#power_"))
9.414 ],
9.415 (*asm_thm = [],*)
9.416 - rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
9.417 + rules = [Thm ("real_plus_binom_pow2" ,num_str @{real_plus_binom_pow2),
9.418 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
9.419 - Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
9.420 + Thm ("real_plus_binom_times" ,num_str @{real_plus_binom_times),
9.421 (*"(a + b)*(a + b) = ...*)
9.422 - Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
9.423 + Thm ("real_minus_binom_pow2" ,num_str @{real_minus_binom_pow2),
9.424 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
9.425 - Thm ("real_minus_binom_times",num_str real_minus_binom_times),
9.426 + Thm ("real_minus_binom_times",num_str @{real_minus_binom_times),
9.427 (*"(a - b)*(a - b) = ...*)
9.428 - Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
9.429 + Thm ("real_plus_minus_binom1",num_str @{real_plus_minus_binom1),
9.430 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
9.431 - Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
9.432 + Thm ("real_plus_minus_binom2",num_str @{real_plus_minus_binom2),
9.433 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
9.434 (*RL 020915*)
9.435 - Thm ("real_pp_binom_times",num_str real_pp_binom_times),
9.436 + Thm ("real_pp_binom_times",num_str @{real_pp_binom_times),
9.437 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
9.438 - Thm ("real_pm_binom_times",num_str real_pm_binom_times),
9.439 + Thm ("real_pm_binom_times",num_str @{real_pm_binom_times),
9.440 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
9.441 - Thm ("real_mp_binom_times",num_str real_mp_binom_times),
9.442 + Thm ("real_mp_binom_times",num_str @{real_mp_binom_times),
9.443 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
9.444 - Thm ("real_mm_binom_times",num_str real_mm_binom_times),
9.445 + Thm ("real_mm_binom_times",num_str @{real_mm_binom_times),
9.446 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
9.447 - Thm ("realpow_multI",num_str realpow_multI),
9.448 + Thm ("realpow_multI",num_str @{realpow_multI),
9.449 (*(a*b)^^^n = a^^^n * b^^^n*)
9.450 - Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
9.451 + Thm ("real_plus_binom_pow3",num_str @{real_plus_binom_pow3),
9.452 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
9.453 - Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),
9.454 + Thm ("real_minus_binom_pow3",num_str @{real_minus_binom_pow3),
9.455 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
9.456
9.457
9.458 @@ -1062,30 +1062,30 @@
9.459 Calc ("op *", eval_binop "#mult_"),
9.460 Calc ("Atools.pow", eval_binop "#power_"),
9.461 (*
9.462 - Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
9.463 - Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
9.464 - Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
9.465 + Thm ("real_mult_commute",num_str @{real_mult_commute), (*AC-rewriting*)
9.466 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute), (**)
9.467 + Thm ("real_mult_assoc",num_str @{real_mult_assoc), (**)
9.468 Thm ("add_commute",num_str @{thm add_commute}), (**)
9.469 Thm ("add_left_commute",num_str @{thm add_left_commute}), (**)
9.470 Thm ("add_assoc",num_str @{thm add_assoc}), (**)
9.471 *)
9.472
9.473 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
9.474 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
9.475 (*"r1 * r1 = r1 ^^^ 2"*)
9.476 - Thm ("realpow_plus_1",num_str realpow_plus_1),
9.477 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
9.478 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
9.479 - (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
9.480 + (*Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
9.481 (*"z1 + z1 = 2 * z1"*)*)
9.482 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
9.483 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
9.484 (*"z1 + (z1 + k) = 2 * z1 + k"*)
9.485
9.486 - Thm ("real_num_collect",num_str real_num_collect),
9.487 + Thm ("real_num_collect",num_str @{real_num_collect),
9.488 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
9.489 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
9.490 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
9.491 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
9.492 - Thm ("real_one_collect",num_str real_one_collect),
9.493 + Thm ("real_one_collect",num_str @{real_one_collect),
9.494 (*"m is_const ==> n + m * n = (1 + m) * n"*)
9.495 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
9.496 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
9.497 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
9.498
9.499 Calc ("op +", eval_binop "#add_"),
9.500 @@ -1475,11 +1475,11 @@
9.501 ("TIMES" , ("op *", eval_binop "#mult_")),
9.502 ("POWER", ("Atools.pow", eval_binop "#power_"))*)
9.503 ],
9.504 - rules = [Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
9.505 + rules = [Thm ("real_plus_binom_times" ,num_str @{real_plus_binom_times),
9.506 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
9.507 - Thm ("real_plus_binom_times1" ,num_str real_plus_binom_times1),
9.508 + Thm ("real_plus_binom_times1" ,num_str @{real_plus_binom_times1),
9.509 (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
9.510 - Thm ("real_plus_binom_times2" ,num_str real_plus_binom_times2),
9.511 + Thm ("real_plus_binom_times2" ,num_str @{real_plus_binom_times2),
9.512 (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
9.513
9.514 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
9.515 @@ -1489,7 +1489,7 @@
9.516 Thm ("left_distrib2",num_str @{thm left_distrib}2),
9.517 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
9.518
9.519 - Thm ("real_mult_assoc", num_str real_mult_assoc),
9.520 + Thm ("real_mult_assoc", num_str @{real_mult_assoc),
9.521 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
9.522 Rls_ order_mult_rls_,
9.523 (*Rls_ order_add_rls_,*)
9.524 @@ -1498,24 +1498,24 @@
9.525 Calc ("op *", eval_binop "#mult_"),
9.526 Calc ("Atools.pow", eval_binop "#power_"),
9.527
9.528 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
9.529 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
9.530 (*"r1 * r1 = r1 ^^^ 2"*)
9.531 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
9.532 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
9.533 (*"z1 + z1 = 2 * z1"*)
9.534 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
9.535 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
9.536 (*"z1 + (z1 + k) = 2 * z1 + k"*)
9.537
9.538 - Thm ("real_num_collect",num_str real_num_collect),
9.539 + Thm ("real_num_collect",num_str @{real_num_collect),
9.540 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
9.541 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
9.542 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
9.543 (*"[| l is_const; m is_const |] ==>
9.544 l * n + (m * n + k) = (l + m) * n + k"*)
9.545 - Thm ("real_one_collect",num_str real_one_collect),
9.546 + Thm ("real_one_collect",num_str @{real_one_collect),
9.547 (*"m is_const ==> n + m * n = (1 + m) * n"*)
9.548 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
9.549 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
9.550 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
9.551
9.552 - Thm ("realpow_multI", num_str realpow_multI),
9.553 + Thm ("realpow_multI", num_str @{realpow_multI),
9.554 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
9.555
9.556 Calc ("op +", eval_binop "#add_"),
10.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Aug 31 15:36:57 2010 +0200
10.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Aug 31 16:00:13 2010 +0200
10.3 @@ -378,53 +378,53 @@
10.4 Calc ("op =",eval_equal "#equal_"),
10.5 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
10.6 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
10.7 - Thm ("not_true",num_str not_true),
10.8 - Thm ("not_false",num_str not_false),
10.9 - Thm ("and_true",num_str and_true),
10.10 - Thm ("and_false",num_str and_false),
10.11 - Thm ("or_true",num_str or_true),
10.12 - Thm ("or_false",num_str or_false)
10.13 + Thm ("not_true",num_str @{not_true),
10.14 + Thm ("not_false",num_str @{not_false),
10.15 + Thm ("and_true",num_str @{and_true),
10.16 + Thm ("and_false",num_str @{and_false),
10.17 + Thm ("or_true",num_str @{or_true),
10.18 + Thm ("or_false",num_str @{or_false)
10.19 ];
10.20
10.21 val PolyEq_erls =
10.22 merge_rls "PolyEq_erls" LinEq_erls
10.23 (append_rls "ops_preds" calculate_Rational
10.24 [Calc ("op =",eval_equal "#equal_"),
10.25 - Thm ("plus_leq", num_str plus_leq),
10.26 - Thm ("minus_leq", num_str minus_leq),
10.27 - Thm ("rat_leq1", num_str rat_leq1),
10.28 - Thm ("rat_leq2", num_str rat_leq2),
10.29 - Thm ("rat_leq3", num_str rat_leq3)
10.30 + Thm ("plus_leq", num_str @{plus_leq),
10.31 + Thm ("minus_leq", num_str @{minus_leq),
10.32 + Thm ("rat_leq1", num_str @{rat_leq1),
10.33 + Thm ("rat_leq2", num_str @{rat_leq2),
10.34 + Thm ("rat_leq3", num_str @{rat_leq3)
10.35 ]);
10.36
10.37 val PolyEq_crls =
10.38 merge_rls "PolyEq_crls" LinEq_crls
10.39 (append_rls "ops_preds" calculate_Rational
10.40 [Calc ("op =",eval_equal "#equal_"),
10.41 - Thm ("plus_leq", num_str plus_leq),
10.42 - Thm ("minus_leq", num_str minus_leq),
10.43 - Thm ("rat_leq1", num_str rat_leq1),
10.44 - Thm ("rat_leq2", num_str rat_leq2),
10.45 - Thm ("rat_leq3", num_str rat_leq3)
10.46 + Thm ("plus_leq", num_str @{plus_leq),
10.47 + Thm ("minus_leq", num_str @{minus_leq),
10.48 + Thm ("rat_leq1", num_str @{rat_leq1),
10.49 + Thm ("rat_leq2", num_str @{rat_leq2),
10.50 + Thm ("rat_leq3", num_str @{rat_leq3)
10.51 ]);
10.52
10.53 val cancel_leading_coeff = prep_rls(
10.54 Rls {id = "cancel_leading_coeff", preconds = [],
10.55 rew_ord = ("e_rew_ord",e_rew_ord),
10.56 erls = PolyEq_erls, srls = Erls, calc = [], (*asm_thm = [],*)
10.57 - rules = [Thm ("cancel_leading_coeff1",num_str cancel_leading_coeff1),
10.58 - Thm ("cancel_leading_coeff2",num_str cancel_leading_coeff2),
10.59 - Thm ("cancel_leading_coeff3",num_str cancel_leading_coeff3),
10.60 - Thm ("cancel_leading_coeff4",num_str cancel_leading_coeff4),
10.61 - Thm ("cancel_leading_coeff5",num_str cancel_leading_coeff5),
10.62 - Thm ("cancel_leading_coeff6",num_str cancel_leading_coeff6),
10.63 - Thm ("cancel_leading_coeff7",num_str cancel_leading_coeff7),
10.64 - Thm ("cancel_leading_coeff8",num_str cancel_leading_coeff8),
10.65 - Thm ("cancel_leading_coeff9",num_str cancel_leading_coeff9),
10.66 - Thm ("cancel_leading_coeff10",num_str cancel_leading_coeff10),
10.67 - Thm ("cancel_leading_coeff11",num_str cancel_leading_coeff11),
10.68 - Thm ("cancel_leading_coeff12",num_str cancel_leading_coeff12),
10.69 - Thm ("cancel_leading_coeff13",num_str cancel_leading_coeff13)
10.70 + rules = [Thm ("cancel_leading_coeff1",num_str @{cancel_leading_coeff1),
10.71 + Thm ("cancel_leading_coeff2",num_str @{cancel_leading_coeff2),
10.72 + Thm ("cancel_leading_coeff3",num_str @{cancel_leading_coeff3),
10.73 + Thm ("cancel_leading_coeff4",num_str @{cancel_leading_coeff4),
10.74 + Thm ("cancel_leading_coeff5",num_str @{cancel_leading_coeff5),
10.75 + Thm ("cancel_leading_coeff6",num_str @{cancel_leading_coeff6),
10.76 + Thm ("cancel_leading_coeff7",num_str @{cancel_leading_coeff7),
10.77 + Thm ("cancel_leading_coeff8",num_str @{cancel_leading_coeff8),
10.78 + Thm ("cancel_leading_coeff9",num_str @{cancel_leading_coeff9),
10.79 + Thm ("cancel_leading_coeff10",num_str @{cancel_leading_coeff10),
10.80 + Thm ("cancel_leading_coeff11",num_str @{cancel_leading_coeff11),
10.81 + Thm ("cancel_leading_coeff12",num_str @{cancel_leading_coeff12),
10.82 + Thm ("cancel_leading_coeff13",num_str @{cancel_leading_coeff13)
10.83 ],
10.84 scr = Script ((term_of o the o (parse thy))
10.85 "empty_script")
10.86 @@ -434,11 +434,11 @@
10.87 Rls {id = "complete_square", preconds = [],
10.88 rew_ord = ("e_rew_ord",e_rew_ord),
10.89 erls = PolyEq_erls, srls = Erls, calc = [], (*asm_thm = [],*)
10.90 - rules = [Thm ("complete_square1",num_str complete_square1),
10.91 - Thm ("complete_square2",num_str complete_square2),
10.92 - Thm ("complete_square3",num_str complete_square3),
10.93 - Thm ("complete_square4",num_str complete_square4),
10.94 - Thm ("complete_square5",num_str complete_square5)
10.95 + rules = [Thm ("complete_square1",num_str @{complete_square1),
10.96 + Thm ("complete_square2",num_str @{complete_square2),
10.97 + Thm ("complete_square3",num_str @{complete_square3),
10.98 + Thm ("complete_square4",num_str @{complete_square4),
10.99 + Thm ("complete_square5",num_str @{complete_square5)
10.100 ],
10.101 scr = Script ((term_of o the o (parse thy))
10.102 "empty_script")
10.103 @@ -451,11 +451,11 @@
10.104 srls = Erls,
10.105 calc = [],
10.106 (*asm_thm = [],*)
10.107 - rules = [Thm ("real_assoc_1",num_str real_assoc_1),
10.108 - Thm ("real_assoc_2",num_str real_assoc_2),
10.109 - Thm ("real_diff_minus",num_str real_diff_minus),
10.110 - Thm ("real_unari_minus",num_str real_unari_minus),
10.111 - Thm ("realpow_multI",num_str realpow_multI),
10.112 + rules = [Thm ("real_assoc_1",num_str @{real_assoc_1),
10.113 + Thm ("real_assoc_2",num_str @{real_assoc_2),
10.114 + Thm ("real_diff_minus",num_str @{real_diff_minus),
10.115 + Thm ("real_unari_minus",num_str @{real_unari_minus),
10.116 + Thm ("realpow_multI",num_str @{realpow_multI),
10.117 Calc ("op +",eval_binop "#add_"),
10.118 Calc ("op -",eval_binop "#sub_"),
10.119 Calc ("op *",eval_binop "#mult_"),
10.120 @@ -484,8 +484,8 @@
10.121 srls = Erls,
10.122 calc = [],
10.123 (*asm_thm = [],*)
10.124 - rules = [Thm("d0_true",num_str d0_true),
10.125 - Thm("d0_false",num_str d0_false)
10.126 + rules = [Thm("d0_true",num_str @{d0_true),
10.127 + Thm("d0_false",num_str @{d0_false)
10.128 ],
10.129 scr = Script ((term_of o the o (parse thy)) "empty_script")
10.130 }:rls);
10.131 @@ -500,11 +500,11 @@
10.132 calc = [],
10.133 (*asm_thm = [("d1_isolate_div","")],*)
10.134 rules = [
10.135 - Thm("d1_isolate_add1",num_str d1_isolate_add1),
10.136 + Thm("d1_isolate_add1",num_str @{d1_isolate_add1),
10.137 (* a+bx=0 -> bx=-a *)
10.138 - Thm("d1_isolate_add2",num_str d1_isolate_add2),
10.139 + Thm("d1_isolate_add2",num_str @{d1_isolate_add2),
10.140 (* a+ x=0 -> x=-a *)
10.141 - Thm("d1_isolate_div",num_str d1_isolate_div)
10.142 + Thm("d1_isolate_div",num_str @{d1_isolate_div)
10.143 (* bx=c -> x=c/b *)
10.144 ],
10.145 scr = Script ((term_of o the o (parse thy)) "empty_script")
10.146 @@ -521,25 +521,25 @@
10.147 calc = [],
10.148 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
10.149 ("d2_isolate_div","")],*)
10.150 - rules = [Thm("d2_prescind1",num_str d2_prescind1),
10.151 + rules = [Thm("d2_prescind1",num_str @{d2_prescind1),
10.152 (* ax+bx^2=0 -> x(a+bx)=0 *)
10.153 - Thm("d2_prescind2",num_str d2_prescind2),
10.154 + Thm("d2_prescind2",num_str @{d2_prescind2),
10.155 (* ax+ x^2=0 -> x(a+ x)=0 *)
10.156 - Thm("d2_prescind3",num_str d2_prescind3),
10.157 + Thm("d2_prescind3",num_str @{d2_prescind3),
10.158 (* x+bx^2=0 -> x(1+bx)=0 *)
10.159 - Thm("d2_prescind4",num_str d2_prescind4),
10.160 + Thm("d2_prescind4",num_str @{d2_prescind4),
10.161 (* x+ x^2=0 -> x(1+ x)=0 *)
10.162 - Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1),
10.163 + Thm("d2_sqrt_equation1",num_str @{d2_sqrt_equation1),
10.164 (* x^2=c -> x=+-sqrt(c)*)
10.165 - Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),
10.166 + Thm("d2_sqrt_equation1_neg",num_str @{d2_sqrt_equation1_neg),
10.167 (* [0<c] x^2=c -> [] *)
10.168 - Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
10.169 + Thm("d2_sqrt_equation2",num_str @{d2_sqrt_equation2),
10.170 (* x^2=0 -> x=0 *)
10.171 - Thm("d2_reduce_equation1",num_str d2_reduce_equation1),
10.172 + Thm("d2_reduce_equation1",num_str @{d2_reduce_equation1),
10.173 (* x(a+bx)=0 -> x=0 | a+bx=0*)
10.174 - Thm("d2_reduce_equation2",num_str d2_reduce_equation2),
10.175 + Thm("d2_reduce_equation2",num_str @{d2_reduce_equation2),
10.176 (* x(a+ x)=0 -> x=0 | a+ x=0*)
10.177 - Thm("d2_isolate_div",num_str d2_isolate_div)
10.178 + Thm("d2_isolate_div",num_str @{d2_isolate_div)
10.179 (* bx^2=c -> x^2=c/b*)
10.180 ],
10.181 scr = Script ((term_of o the o (parse thy)) "empty_script")
10.182 @@ -555,17 +555,17 @@
10.183 calc = [],
10.184 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
10.185 ("d2_isolate_div","")],*)
10.186 - rules = [Thm("d2_isolate_add1",num_str d2_isolate_add1),
10.187 + rules = [Thm("d2_isolate_add1",num_str @{d2_isolate_add1),
10.188 (* a+ bx^2=0 -> bx^2=(-1)a*)
10.189 - Thm("d2_isolate_add2",num_str d2_isolate_add2),
10.190 + Thm("d2_isolate_add2",num_str @{d2_isolate_add2),
10.191 (* a+ x^2=0 -> x^2=(-1)a*)
10.192 - Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
10.193 + Thm("d2_sqrt_equation2",num_str @{d2_sqrt_equation2),
10.194 (* x^2=0 -> x=0 *)
10.195 - Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1),
10.196 + Thm("d2_sqrt_equation1",num_str @{d2_sqrt_equation1),
10.197 (* x^2=c -> x=+-sqrt(c)*)
10.198 - Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),
10.199 + Thm("d2_sqrt_equation1_neg",num_str @{d2_sqrt_equation1_neg),
10.200 (* [c<0] x^2=c -> x=[] *)
10.201 - Thm("d2_isolate_div",num_str d2_isolate_div)
10.202 + Thm("d2_isolate_div",num_str @{d2_isolate_div)
10.203 (* bx^2=c -> x^2=c/b*)
10.204 ],
10.205 scr = Script ((term_of o the o (parse thy)) "empty_script")
10.206 @@ -577,41 +577,41 @@
10.207 Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
10.208 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
10.209 srls = Erls, calc = [],
10.210 - rules = [Thm("d2_pqformula1",num_str d2_pqformula1),
10.211 + rules = [Thm("d2_pqformula1",num_str @{d2_pqformula1),
10.212 (* q+px+ x^2=0 *)
10.213 - Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg),
10.214 + Thm("d2_pqformula1_neg",num_str @{d2_pqformula1_neg),
10.215 (* q+px+ x^2=0 *)
10.216 - Thm("d2_pqformula2",num_str d2_pqformula2),
10.217 + Thm("d2_pqformula2",num_str @{d2_pqformula2),
10.218 (* q+px+1x^2=0 *)
10.219 - Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg),
10.220 + Thm("d2_pqformula2_neg",num_str @{d2_pqformula2_neg),
10.221 (* q+px+1x^2=0 *)
10.222 - Thm("d2_pqformula3",num_str d2_pqformula3),
10.223 + Thm("d2_pqformula3",num_str @{d2_pqformula3),
10.224 (* q+ x+ x^2=0 *)
10.225 - Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg),
10.226 + Thm("d2_pqformula3_neg",num_str @{d2_pqformula3_neg),
10.227 (* q+ x+ x^2=0 *)
10.228 - Thm("d2_pqformula4",num_str d2_pqformula4),
10.229 + Thm("d2_pqformula4",num_str @{d2_pqformula4),
10.230 (* q+ x+1x^2=0 *)
10.231 - Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg),
10.232 + Thm("d2_pqformula4_neg",num_str @{d2_pqformula4_neg),
10.233 (* q+ x+1x^2=0 *)
10.234 - Thm("d2_pqformula5",num_str d2_pqformula5),
10.235 + Thm("d2_pqformula5",num_str @{d2_pqformula5),
10.236 (* qx+ x^2=0 *)
10.237 - Thm("d2_pqformula6",num_str d2_pqformula6),
10.238 + Thm("d2_pqformula6",num_str @{d2_pqformula6),
10.239 (* qx+1x^2=0 *)
10.240 - Thm("d2_pqformula7",num_str d2_pqformula7),
10.241 + Thm("d2_pqformula7",num_str @{d2_pqformula7),
10.242 (* x+ x^2=0 *)
10.243 - Thm("d2_pqformula8",num_str d2_pqformula8),
10.244 + Thm("d2_pqformula8",num_str @{d2_pqformula8),
10.245 (* x+1x^2=0 *)
10.246 - Thm("d2_pqformula9",num_str d2_pqformula9),
10.247 + Thm("d2_pqformula9",num_str @{d2_pqformula9),
10.248 (* q +1x^2=0 *)
10.249 - Thm("d2_pqformula9_neg",num_str d2_pqformula9_neg),
10.250 + Thm("d2_pqformula9_neg",num_str @{d2_pqformula9_neg),
10.251 (* q +1x^2=0 *)
10.252 - Thm("d2_pqformula10",num_str d2_pqformula10),
10.253 + Thm("d2_pqformula10",num_str @{d2_pqformula10),
10.254 (* q + x^2=0 *)
10.255 - Thm("d2_pqformula10_neg",num_str d2_pqformula10_neg),
10.256 + Thm("d2_pqformula10_neg",num_str @{d2_pqformula10_neg),
10.257 (* q + x^2=0 *)
10.258 - Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
10.259 + Thm("d2_sqrt_equation2",num_str @{d2_sqrt_equation2),
10.260 (* x^2=0 *)
10.261 - Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3)
10.262 + Thm("d2_sqrt_equation3",num_str @{d2_sqrt_equation3)
10.263 (* 1x^2=0 *)
10.264 ],
10.265 scr = Script ((term_of o the o (parse thy)) "empty_script")
10.266 @@ -623,41 +623,41 @@
10.267 Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
10.268 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
10.269 srls = Erls, calc = [],
10.270 - rules = [Thm("d2_abcformula1",num_str d2_abcformula1),
10.271 + rules = [Thm("d2_abcformula1",num_str @{d2_abcformula1),
10.272 (*c+bx+cx^2=0 *)
10.273 - Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg),
10.274 + Thm("d2_abcformula1_neg",num_str @{d2_abcformula1_neg),
10.275 (*c+bx+cx^2=0 *)
10.276 - Thm("d2_abcformula2",num_str d2_abcformula2),
10.277 + Thm("d2_abcformula2",num_str @{d2_abcformula2),
10.278 (*c+ x+cx^2=0 *)
10.279 - Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg),
10.280 + Thm("d2_abcformula2_neg",num_str @{d2_abcformula2_neg),
10.281 (*c+ x+cx^2=0 *)
10.282 - Thm("d2_abcformula3",num_str d2_abcformula3),
10.283 + Thm("d2_abcformula3",num_str @{d2_abcformula3),
10.284 (*c+bx+ x^2=0 *)
10.285 - Thm("d2_abcformula3_neg",num_str d2_abcformula3_neg),
10.286 + Thm("d2_abcformula3_neg",num_str @{d2_abcformula3_neg),
10.287 (*c+bx+ x^2=0 *)
10.288 - Thm("d2_abcformula4",num_str d2_abcformula4),
10.289 + Thm("d2_abcformula4",num_str @{d2_abcformula4),
10.290 (*c+ x+ x^2=0 *)
10.291 - Thm("d2_abcformula4_neg",num_str d2_abcformula4_neg),
10.292 + Thm("d2_abcformula4_neg",num_str @{d2_abcformula4_neg),
10.293 (*c+ x+ x^2=0 *)
10.294 - Thm("d2_abcformula5",num_str d2_abcformula5),
10.295 + Thm("d2_abcformula5",num_str @{d2_abcformula5),
10.296 (*c+ cx^2=0 *)
10.297 - Thm("d2_abcformula5_neg",num_str d2_abcformula5_neg),
10.298 + Thm("d2_abcformula5_neg",num_str @{d2_abcformula5_neg),
10.299 (*c+ cx^2=0 *)
10.300 - Thm("d2_abcformula6",num_str d2_abcformula6),
10.301 + Thm("d2_abcformula6",num_str @{d2_abcformula6),
10.302 (*c+ x^2=0 *)
10.303 - Thm("d2_abcformula6_neg",num_str d2_abcformula6_neg),
10.304 + Thm("d2_abcformula6_neg",num_str @{d2_abcformula6_neg),
10.305 (*c+ x^2=0 *)
10.306 - Thm("d2_abcformula7",num_str d2_abcformula7),
10.307 + Thm("d2_abcformula7",num_str @{d2_abcformula7),
10.308 (* bx+ax^2=0 *)
10.309 - Thm("d2_abcformula8",num_str d2_abcformula8),
10.310 + Thm("d2_abcformula8",num_str @{d2_abcformula8),
10.311 (* bx+ x^2=0 *)
10.312 - Thm("d2_abcformula9",num_str d2_abcformula9),
10.313 + Thm("d2_abcformula9",num_str @{d2_abcformula9),
10.314 (* x+ax^2=0 *)
10.315 - Thm("d2_abcformula10",num_str d2_abcformula10),
10.316 + Thm("d2_abcformula10",num_str @{d2_abcformula10),
10.317 (* x+ x^2=0 *)
10.318 - Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
10.319 + Thm("d2_sqrt_equation2",num_str @{d2_sqrt_equation2),
10.320 (* x^2=0 *)
10.321 - Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3)
10.322 + Thm("d2_sqrt_equation3",num_str @{d2_sqrt_equation3)
10.323 (* bx^2=0 *)
10.324 ],
10.325 scr = Script ((term_of o the o (parse thy)) "empty_script")
10.326 @@ -669,53 +669,53 @@
10.327 Rls {id = "d2_polyeq_simplify", preconds = [],
10.328 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
10.329 srls = Erls, calc = [],
10.330 - rules = [Thm("d2_pqformula1",num_str d2_pqformula1),
10.331 + rules = [Thm("d2_pqformula1",num_str @{d2_pqformula1),
10.332 (* p+qx+ x^2=0 *)
10.333 - Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg),
10.334 + Thm("d2_pqformula1_neg",num_str @{d2_pqformula1_neg),
10.335 (* p+qx+ x^2=0 *)
10.336 - Thm("d2_pqformula2",num_str d2_pqformula2),
10.337 + Thm("d2_pqformula2",num_str @{d2_pqformula2),
10.338 (* p+qx+1x^2=0 *)
10.339 - Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg),
10.340 + Thm("d2_pqformula2_neg",num_str @{d2_pqformula2_neg),
10.341 (* p+qx+1x^2=0 *)
10.342 - Thm("d2_pqformula3",num_str d2_pqformula3),
10.343 + Thm("d2_pqformula3",num_str @{d2_pqformula3),
10.344 (* p+ x+ x^2=0 *)
10.345 - Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg),
10.346 + Thm("d2_pqformula3_neg",num_str @{d2_pqformula3_neg),
10.347 (* p+ x+ x^2=0 *)
10.348 - Thm("d2_pqformula4",num_str d2_pqformula4),
10.349 + Thm("d2_pqformula4",num_str @{d2_pqformula4),
10.350 (* p+ x+1x^2=0 *)
10.351 - Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg),
10.352 + Thm("d2_pqformula4_neg",num_str @{d2_pqformula4_neg),
10.353 (* p+ x+1x^2=0 *)
10.354 - Thm("d2_abcformula1",num_str d2_abcformula1),
10.355 + Thm("d2_abcformula1",num_str @{d2_abcformula1),
10.356 (* c+bx+cx^2=0 *)
10.357 - Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg),
10.358 + Thm("d2_abcformula1_neg",num_str @{d2_abcformula1_neg),
10.359 (* c+bx+cx^2=0 *)
10.360 - Thm("d2_abcformula2",num_str d2_abcformula2),
10.361 + Thm("d2_abcformula2",num_str @{d2_abcformula2),
10.362 (* c+ x+cx^2=0 *)
10.363 - Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg),
10.364 + Thm("d2_abcformula2_neg",num_str @{d2_abcformula2_neg),
10.365 (* c+ x+cx^2=0 *)
10.366 - Thm("d2_prescind1",num_str d2_prescind1),
10.367 + Thm("d2_prescind1",num_str @{d2_prescind1),
10.368 (* ax+bx^2=0 -> x(a+bx)=0 *)
10.369 - Thm("d2_prescind2",num_str d2_prescind2),
10.370 + Thm("d2_prescind2",num_str @{d2_prescind2),
10.371 (* ax+ x^2=0 -> x(a+ x)=0 *)
10.372 - Thm("d2_prescind3",num_str d2_prescind3),
10.373 + Thm("d2_prescind3",num_str @{d2_prescind3),
10.374 (* x+bx^2=0 -> x(1+bx)=0 *)
10.375 - Thm("d2_prescind4",num_str d2_prescind4),
10.376 + Thm("d2_prescind4",num_str @{d2_prescind4),
10.377 (* x+ x^2=0 -> x(1+ x)=0 *)
10.378 - Thm("d2_isolate_add1",num_str d2_isolate_add1),
10.379 + Thm("d2_isolate_add1",num_str @{d2_isolate_add1),
10.380 (* a+ bx^2=0 -> bx^2=(-1)a*)
10.381 - Thm("d2_isolate_add2",num_str d2_isolate_add2),
10.382 + Thm("d2_isolate_add2",num_str @{d2_isolate_add2),
10.383 (* a+ x^2=0 -> x^2=(-1)a*)
10.384 - Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1),
10.385 + Thm("d2_sqrt_equation1",num_str @{d2_sqrt_equation1),
10.386 (* x^2=c -> x=+-sqrt(c)*)
10.387 - Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),
10.388 + Thm("d2_sqrt_equation1_neg",num_str @{d2_sqrt_equation1_neg),
10.389 (* [c<0] x^2=c -> x=[]*)
10.390 - Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
10.391 + Thm("d2_sqrt_equation2",num_str @{d2_sqrt_equation2),
10.392 (* x^2=0 -> x=0 *)
10.393 - Thm("d2_reduce_equation1",num_str d2_reduce_equation1),
10.394 + Thm("d2_reduce_equation1",num_str @{d2_reduce_equation1),
10.395 (* x(a+bx)=0 -> x=0 | a+bx=0*)
10.396 - Thm("d2_reduce_equation2",num_str d2_reduce_equation2),
10.397 + Thm("d2_reduce_equation2",num_str @{d2_reduce_equation2),
10.398 (* x(a+ x)=0 -> x=0 | a+ x=0*)
10.399 - Thm("d2_isolate_div",num_str d2_isolate_div)
10.400 + Thm("d2_isolate_div",num_str @{d2_isolate_div)
10.401 (* bx^2=c -> x^2=c/b*)
10.402 ],
10.403 scr = Script ((term_of o the o (parse thy)) "empty_script")
10.404 @@ -728,65 +728,65 @@
10.405 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
10.406 srls = Erls, calc = [],
10.407 rules =
10.408 - [Thm("d3_reduce_equation1",num_str d3_reduce_equation1),
10.409 + [Thm("d3_reduce_equation1",num_str @{d3_reduce_equation1),
10.410 (*a*bdv + b*bdv^^^2 + c*bdv^^^3=0) =
10.411 (bdv=0 | (a + b*bdv + c*bdv^^^2=0)*)
10.412 - Thm("d3_reduce_equation2",num_str d3_reduce_equation2),
10.413 + Thm("d3_reduce_equation2",num_str @{d3_reduce_equation2),
10.414 (* bdv + b*bdv^^^2 + c*bdv^^^3=0) =
10.415 (bdv=0 | (1 + b*bdv + c*bdv^^^2=0)*)
10.416 - Thm("d3_reduce_equation3",num_str d3_reduce_equation3),
10.417 + Thm("d3_reduce_equation3",num_str @{d3_reduce_equation3),
10.418 (*a*bdv + bdv^^^2 + c*bdv^^^3=0) =
10.419 (bdv=0 | (a + bdv + c*bdv^^^2=0)*)
10.420 - Thm("d3_reduce_equation4",num_str d3_reduce_equation4),
10.421 + Thm("d3_reduce_equation4",num_str @{d3_reduce_equation4),
10.422 (* bdv + bdv^^^2 + c*bdv^^^3=0) =
10.423 (bdv=0 | (1 + bdv + c*bdv^^^2=0)*)
10.424 - Thm("d3_reduce_equation5",num_str d3_reduce_equation5),
10.425 + Thm("d3_reduce_equation5",num_str @{d3_reduce_equation5),
10.426 (*a*bdv + b*bdv^^^2 + bdv^^^3=0) =
10.427 (bdv=0 | (a + b*bdv + bdv^^^2=0)*)
10.428 - Thm("d3_reduce_equation6",num_str d3_reduce_equation6),
10.429 + Thm("d3_reduce_equation6",num_str @{d3_reduce_equation6),
10.430 (* bdv + b*bdv^^^2 + bdv^^^3=0) =
10.431 (bdv=0 | (1 + b*bdv + bdv^^^2=0)*)
10.432 - Thm("d3_reduce_equation7",num_str d3_reduce_equation7),
10.433 + Thm("d3_reduce_equation7",num_str @{d3_reduce_equation7),
10.434 (*a*bdv + bdv^^^2 + bdv^^^3=0) =
10.435 (bdv=0 | (1 + bdv + bdv^^^2=0)*)
10.436 - Thm("d3_reduce_equation8",num_str d3_reduce_equation8),
10.437 + Thm("d3_reduce_equation8",num_str @{d3_reduce_equation8),
10.438 (* bdv + bdv^^^2 + bdv^^^3=0) =
10.439 (bdv=0 | (1 + bdv + bdv^^^2=0)*)
10.440 - Thm("d3_reduce_equation9",num_str d3_reduce_equation9),
10.441 + Thm("d3_reduce_equation9",num_str @{d3_reduce_equation9),
10.442 (*a*bdv + c*bdv^^^3=0) =
10.443 (bdv=0 | (a + c*bdv^^^2=0)*)
10.444 - Thm("d3_reduce_equation10",num_str d3_reduce_equation10),
10.445 + Thm("d3_reduce_equation10",num_str @{d3_reduce_equation10),
10.446 (* bdv + c*bdv^^^3=0) =
10.447 (bdv=0 | (1 + c*bdv^^^2=0)*)
10.448 - Thm("d3_reduce_equation11",num_str d3_reduce_equation11),
10.449 + Thm("d3_reduce_equation11",num_str @{d3_reduce_equation11),
10.450 (*a*bdv + bdv^^^3=0) =
10.451 (bdv=0 | (a + bdv^^^2=0)*)
10.452 - Thm("d3_reduce_equation12",num_str d3_reduce_equation12),
10.453 + Thm("d3_reduce_equation12",num_str @{d3_reduce_equation12),
10.454 (* bdv + bdv^^^3=0) =
10.455 (bdv=0 | (1 + bdv^^^2=0)*)
10.456 - Thm("d3_reduce_equation13",num_str d3_reduce_equation13),
10.457 + Thm("d3_reduce_equation13",num_str @{d3_reduce_equation13),
10.458 (* b*bdv^^^2 + c*bdv^^^3=0) =
10.459 (bdv=0 | ( b*bdv + c*bdv^^^2=0)*)
10.460 - Thm("d3_reduce_equation14",num_str d3_reduce_equation14),
10.461 + Thm("d3_reduce_equation14",num_str @{d3_reduce_equation14),
10.462 (* bdv^^^2 + c*bdv^^^3=0) =
10.463 (bdv=0 | ( bdv + c*bdv^^^2=0)*)
10.464 - Thm("d3_reduce_equation15",num_str d3_reduce_equation15),
10.465 + Thm("d3_reduce_equation15",num_str @{d3_reduce_equation15),
10.466 (* b*bdv^^^2 + bdv^^^3=0) =
10.467 (bdv=0 | ( b*bdv + bdv^^^2=0)*)
10.468 - Thm("d3_reduce_equation16",num_str d3_reduce_equation16),
10.469 + Thm("d3_reduce_equation16",num_str @{d3_reduce_equation16),
10.470 (* bdv^^^2 + bdv^^^3=0) =
10.471 (bdv=0 | ( bdv + bdv^^^2=0)*)
10.472 - Thm("d3_isolate_add1",num_str d3_isolate_add1),
10.473 + Thm("d3_isolate_add1",num_str @{d3_isolate_add1),
10.474 (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) =
10.475 (bdv=0 | (b*bdv^^^3=a)*)
10.476 - Thm("d3_isolate_add2",num_str d3_isolate_add2),
10.477 + Thm("d3_isolate_add2",num_str @{d3_isolate_add2),
10.478 (*[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) =
10.479 (bdv=0 | ( bdv^^^3=a)*)
10.480 - Thm("d3_isolate_div",num_str d3_isolate_div),
10.481 + Thm("d3_isolate_div",num_str @{d3_isolate_div),
10.482 (*[|Not(b=0)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b*)
10.483 - Thm("d3_root_equation2",num_str d3_root_equation2),
10.484 + Thm("d3_root_equation2",num_str @{d3_root_equation2),
10.485 (*(bdv^^^3=0) = (bdv=0) *)
10.486 - Thm("d3_root_equation1",num_str d3_root_equation1)
10.487 + Thm("d3_root_equation1",num_str @{d3_root_equation1)
10.488 (*bdv^^^3=c) = (bdv = nroot 3 c*)
10.489 ],
10.490 scr = Script ((term_of o the o (parse thy)) "empty_script")
10.491 @@ -799,7 +799,7 @@
10.492 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
10.493 srls = Erls, calc = [],
10.494 rules =
10.495 - [Thm("d4_sub_u1",num_str d4_sub_u1)
10.496 + [Thm("d4_sub_u1",num_str @{d4_sub_u1)
10.497 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
10.498 ],
10.499 scr = Script ((term_of o the o (parse thy)) "empty_script")
10.500 @@ -1343,11 +1343,11 @@
10.501 erls = e_rls,srls = Erls,
10.502 calc = [],
10.503 (*asm_thm = [],*)
10.504 - rules = [Thm ("real_mult_commute",num_str real_mult_commute),
10.505 + rules = [Thm ("real_mult_commute",num_str @{real_mult_commute),
10.506 (* z * w = w * z *)
10.507 - Thm ("real_mult_left_commute",num_str real_mult_left_commute),
10.508 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute),
10.509 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
10.510 - Thm ("real_mult_assoc",num_str real_mult_assoc),
10.511 + Thm ("real_mult_assoc",num_str @{real_mult_assoc),
10.512 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
10.513 Thm ("add_commute",num_str @{thm add_commute}),
10.514 (*z + w = w + z*)
10.515 @@ -1363,30 +1363,30 @@
10.516 erls = e_rls,srls = Erls,
10.517 calc = [],
10.518 (*asm_thm = [],*)
10.519 - rules = [Thm ("bdv_collect_1",num_str bdv_collect_1),
10.520 - Thm ("bdv_collect_2",num_str bdv_collect_2),
10.521 - Thm ("bdv_collect_3",num_str bdv_collect_3),
10.522 + rules = [Thm ("bdv_collect_1",num_str @{bdv_collect_1),
10.523 + Thm ("bdv_collect_2",num_str @{bdv_collect_2),
10.524 + Thm ("bdv_collect_3",num_str @{bdv_collect_3),
10.525
10.526 - Thm ("bdv_collect_assoc1_1",num_str bdv_collect_assoc1_1),
10.527 - Thm ("bdv_collect_assoc1_2",num_str bdv_collect_assoc1_2),
10.528 - Thm ("bdv_collect_assoc1_3",num_str bdv_collect_assoc1_3),
10.529 + Thm ("bdv_collect_assoc1_1",num_str @{bdv_collect_assoc1_1),
10.530 + Thm ("bdv_collect_assoc1_2",num_str @{bdv_collect_assoc1_2),
10.531 + Thm ("bdv_collect_assoc1_3",num_str @{bdv_collect_assoc1_3),
10.532
10.533 - Thm ("bdv_collect_assoc2_1",num_str bdv_collect_assoc2_1),
10.534 - Thm ("bdv_collect_assoc2_2",num_str bdv_collect_assoc2_2),
10.535 - Thm ("bdv_collect_assoc2_3",num_str bdv_collect_assoc2_3),
10.536 + Thm ("bdv_collect_assoc2_1",num_str @{bdv_collect_assoc2_1),
10.537 + Thm ("bdv_collect_assoc2_2",num_str @{bdv_collect_assoc2_2),
10.538 + Thm ("bdv_collect_assoc2_3",num_str @{bdv_collect_assoc2_3),
10.539
10.540
10.541 - Thm ("bdv_n_collect_1",num_str bdv_n_collect_1),
10.542 - Thm ("bdv_n_collect_2",num_str bdv_n_collect_2),
10.543 - Thm ("bdv_n_collect_3",num_str bdv_n_collect_3),
10.544 + Thm ("bdv_n_collect_1",num_str @{bdv_n_collect_1),
10.545 + Thm ("bdv_n_collect_2",num_str @{bdv_n_collect_2),
10.546 + Thm ("bdv_n_collect_3",num_str @{bdv_n_collect_3),
10.547
10.548 - Thm ("bdv_n_collect_assoc1_1",num_str bdv_n_collect_assoc1_1),
10.549 - Thm ("bdv_n_collect_assoc1_2",num_str bdv_n_collect_assoc1_2),
10.550 - Thm ("bdv_n_collect_assoc1_3",num_str bdv_n_collect_assoc1_3),
10.551 + Thm ("bdv_n_collect_assoc1_1",num_str @{bdv_n_collect_assoc1_1),
10.552 + Thm ("bdv_n_collect_assoc1_2",num_str @{bdv_n_collect_assoc1_2),
10.553 + Thm ("bdv_n_collect_assoc1_3",num_str @{bdv_n_collect_assoc1_3),
10.554
10.555 - Thm ("bdv_n_collect_assoc2_1",num_str bdv_n_collect_assoc2_1),
10.556 - Thm ("bdv_n_collect_assoc2_2",num_str bdv_n_collect_assoc2_2),
10.557 - Thm ("bdv_n_collect_assoc2_3",num_str bdv_n_collect_assoc2_3)
10.558 + Thm ("bdv_n_collect_assoc2_1",num_str @{bdv_n_collect_assoc2_1),
10.559 + Thm ("bdv_n_collect_assoc2_2",num_str @{bdv_n_collect_assoc2_2),
10.560 + Thm ("bdv_n_collect_assoc2_3",num_str @{bdv_n_collect_assoc2_3)
10.561 ], scr = EmptyScr}:rls);
10.562
10.563 (*.transforms an arbitrary term without roots to a polynomial [4]
10.564 @@ -1401,7 +1401,7 @@
10.565 Rls_ simplify_power,
10.566 Rls_ collect_numerals,
10.567 Rls_ reduce_012,
10.568 - Thm ("realpow_oneI",num_str realpow_oneI),
10.569 + Thm ("realpow_oneI",num_str @{realpow_oneI),
10.570 Rls_ discard_parentheses,
10.571 Rls_ collect_bdv
10.572 ],
10.573 @@ -1411,12 +1411,12 @@
10.574 val separate_bdvs =
10.575 append_rls "separate_bdvs"
10.576 collect_bdv
10.577 - [Thm ("separate_bdv", num_str separate_bdv),
10.578 + [Thm ("separate_bdv", num_str @{separate_bdv),
10.579 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
10.580 - Thm ("separate_bdv_n", num_str separate_bdv_n),
10.581 - Thm ("separate_1_bdv", num_str separate_1_bdv),
10.582 + Thm ("separate_bdv_n", num_str @{separate_bdv_n),
10.583 + Thm ("separate_1_bdv", num_str @{separate_1_bdv),
10.584 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
10.585 - Thm ("separate_1_bdv_n", num_str separate_1_bdv_n),
10.586 + Thm ("separate_1_bdv_n", num_str @{separate_1_bdv_n),
10.587 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
10.588 Thm ("nadd_divide_distrib",
10.589 num_str @{thm nadd_divide_distrib})
11.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue Aug 31 15:36:57 2010 +0200
11.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Aug 31 16:00:13 2010 +0200
11.3 @@ -197,21 +197,21 @@
11.4 Rls{id = "ordne_alphabetisch", preconds = [],
11.5 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
11.6 erls = erls_ordne_alphabetisch,
11.7 - rules = [Thm ("tausche_plus",num_str tausche_plus),
11.8 + rules = [Thm ("tausche_plus",num_str @{tausche_plus),
11.9 (*"b kleiner a ==> (b + a) = (a + b)"*)
11.10 - Thm ("tausche_minus",num_str tausche_minus),
11.11 + Thm ("tausche_minus",num_str @{tausche_minus),
11.12 (*"b kleiner a ==> (b - a) = (-a + b)"*)
11.13 - Thm ("tausche_vor_plus",num_str tausche_vor_plus),
11.14 + Thm ("tausche_vor_plus",num_str @{tausche_vor_plus),
11.15 (*"[| b ist_monom; a kleiner b |] ==> (- b + a) = (a - b)"*)
11.16 - Thm ("tausche_vor_minus",num_str tausche_vor_minus),
11.17 + Thm ("tausche_vor_minus",num_str @{tausche_vor_minus),
11.18 (*"[| b ist_monom; a kleiner b |] ==> (- b - a) = (-a - b)"*)
11.19 - Thm ("tausche_plus_plus",num_str tausche_plus_plus),
11.20 + Thm ("tausche_plus_plus",num_str @{tausche_plus_plus),
11.21 (*"c kleiner b ==> (a + c + b) = (a + b + c)"*)
11.22 - Thm ("tausche_plus_minus",num_str tausche_plus_minus),
11.23 + Thm ("tausche_plus_minus",num_str @{tausche_plus_minus),
11.24 (*"c kleiner b ==> (a + c - b) = (a - b + c)"*)
11.25 - Thm ("tausche_minus_plus",num_str tausche_minus_plus),
11.26 + Thm ("tausche_minus_plus",num_str @{tausche_minus_plus),
11.27 (*"c kleiner b ==> (a - c + b) = (a + b - c)"*)
11.28 - Thm ("tausche_minus_minus",num_str tausche_minus_minus)
11.29 + Thm ("tausche_minus_minus",num_str @{tausche_minus_minus)
11.30 (*"c kleiner b ==> (a - c - b) = (a - b - c)"*)
11.31 ], scr = EmptyScr}:rls;
11.32
11.33 @@ -222,42 +222,42 @@
11.34 [Calc ("Atools.is'_const",eval_const "#is_const_")],
11.35 srls = Erls, calc = [],
11.36 rules =
11.37 - [Thm ("real_num_collect",num_str real_num_collect),
11.38 + [Thm ("real_num_collect",num_str @{real_num_collect),
11.39 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
11.40 - Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r),
11.41 + Thm ("real_num_collect_assoc_r",num_str @{real_num_collect_assoc_r),
11.42 (*"[| l is_const; m..|] ==> (k + m * n) + l * n = k + (l + m)*n"*)
11.43 - Thm ("real_one_collect",num_str real_one_collect),
11.44 + Thm ("real_one_collect",num_str @{real_one_collect),
11.45 (*"m is_const ==> n + m * n = (1 + m) * n"*)
11.46 - Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r),
11.47 + Thm ("real_one_collect_assoc_r",num_str @{real_one_collect_assoc_r),
11.48 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
11.49
11.50
11.51 - Thm ("subtrahiere",num_str subtrahiere),
11.52 + Thm ("subtrahiere",num_str @{subtrahiere),
11.53 (*"[| l is_const; m is_const |] ==> m * v - l * v = (m - l) * v"*)
11.54 - Thm ("subtrahiere_von_1",num_str subtrahiere_von_1),
11.55 + Thm ("subtrahiere_von_1",num_str @{subtrahiere_von_1),
11.56 (*"[| l is_const |] ==> v - l * v = (1 - l) * v"*)
11.57 - Thm ("subtrahiere_1",num_str subtrahiere_1),
11.58 + Thm ("subtrahiere_1",num_str @{subtrahiere_1),
11.59 (*"[| l is_const; m is_const |] ==> m * v - v = (m - 1) * v"*)
11.60
11.61 - Thm ("subtrahiere_x_plus_minus",num_str subtrahiere_x_plus_minus),
11.62 + Thm ("subtrahiere_x_plus_minus",num_str @{subtrahiere_x_plus_minus),
11.63 (*"[| l is_const; m..|] ==> (k + m * n) - l * n = k + ( m - l) * n"*)
11.64 - Thm ("subtrahiere_x_plus1_minus",num_str subtrahiere_x_plus1_minus),
11.65 + Thm ("subtrahiere_x_plus1_minus",num_str @{subtrahiere_x_plus1_minus),
11.66 (*"[| l is_const |] ==> (x + v) - l * v = x + (1 - l) * v"*)
11.67 - Thm ("subtrahiere_x_plus_minus1",num_str subtrahiere_x_plus_minus1),
11.68 + Thm ("subtrahiere_x_plus_minus1",num_str @{subtrahiere_x_plus_minus1),
11.69 (*"[| m is_const |] ==> (x + m * v) - v = x + (m - 1) * v"*)
11.70
11.71 - Thm ("subtrahiere_x_minus_plus",num_str subtrahiere_x_minus_plus),
11.72 + Thm ("subtrahiere_x_minus_plus",num_str @{subtrahiere_x_minus_plus),
11.73 (*"[| l is_const; m..|] ==> (k - m * n) + l * n = k + (-m + l) * n"*)
11.74 - Thm ("subtrahiere_x_minus1_plus",num_str subtrahiere_x_minus1_plus),
11.75 + Thm ("subtrahiere_x_minus1_plus",num_str @{subtrahiere_x_minus1_plus),
11.76 (*"[| l is_const |] ==> (x - v) + l * v = x + (-1 + l) * v"*)
11.77 - Thm ("subtrahiere_x_minus_plus1",num_str subtrahiere_x_minus_plus1),
11.78 + Thm ("subtrahiere_x_minus_plus1",num_str @{subtrahiere_x_minus_plus1),
11.79 (*"[| m is_const |] ==> (x - m * v) + v = x + (-m + 1) * v"*)
11.80
11.81 - Thm ("subtrahiere_x_minus_minus",num_str subtrahiere_x_minus_minus),
11.82 + Thm ("subtrahiere_x_minus_minus",num_str @{subtrahiere_x_minus_minus),
11.83 (*"[| l is_const; m..|] ==> (k - m * n) - l * n = k + (-m - l) * n"*)
11.84 - Thm ("subtrahiere_x_minus1_minus",num_str subtrahiere_x_minus1_minus),
11.85 + Thm ("subtrahiere_x_minus1_minus",num_str @{subtrahiere_x_minus1_minus),
11.86 (*"[| l is_const |] ==> (x - v) - l * v = x + (-1 - l) * v"*)
11.87 - Thm ("subtrahiere_x_minus_minus1",num_str subtrahiere_x_minus_minus1),
11.88 + Thm ("subtrahiere_x_minus_minus1",num_str @{subtrahiere_x_minus_minus1),
11.89 (*"[| m is_const |] ==> (x - m * v) - v = x + (-m - 1) * v"*)
11.90
11.91 Calc ("op +", eval_binop "#add_"),
11.92 @@ -265,18 +265,18 @@
11.93
11.94 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
11.95 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
11.96 - Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r),
11.97 + Thm ("real_mult_2_assoc_r",num_str @{real_mult_2_assoc_r),
11.98 (*"(k + z1) + z1 = k + 2 * z1"*)
11.99 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
11.100 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
11.101 (*"z1 + z1 = 2 * z1"*)
11.102
11.103 - Thm ("addiere_vor_minus",num_str addiere_vor_minus),
11.104 + Thm ("addiere_vor_minus",num_str @{addiere_vor_minus),
11.105 (*"[| l is_const; m is_const |] ==> -(l * v) + m * v = (-l + m) *v"*)
11.106 - Thm ("addiere_eins_vor_minus",num_str addiere_eins_vor_minus),
11.107 + Thm ("addiere_eins_vor_minus",num_str @{addiere_eins_vor_minus),
11.108 (*"[| m is_const |] ==> - v + m * v = (-1 + m) * v"*)
11.109 - Thm ("subtrahiere_vor_minus",num_str subtrahiere_vor_minus),
11.110 + Thm ("subtrahiere_vor_minus",num_str @{subtrahiere_vor_minus),
11.111 (*"[| l is_const; m is_const |] ==> -(l * v) - m * v = (-l - m) *v"*)
11.112 - Thm ("subtrahiere_eins_vor_minus",num_str subtrahiere_eins_vor_minus)
11.113 + Thm ("subtrahiere_eins_vor_minus",num_str @{subtrahiere_eins_vor_minus)
11.114 (*"[| m is_const |] ==> - v - m * v = (-1 - m) * v"*)
11.115
11.116 ], scr = EmptyScr}:rls;
11.117 @@ -286,13 +286,13 @@
11.118 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [],
11.119 erls = append_rls "erls_verschoenere" e_rls
11.120 [Calc ("PolyMinus.kleiner", eval_kleiner "")],
11.121 - rules = [Thm ("vorzeichen_minus_weg1",num_str vorzeichen_minus_weg1),
11.122 + rules = [Thm ("vorzeichen_minus_weg1",num_str @{vorzeichen_minus_weg1),
11.123 (*"l kleiner 0 ==> a + l * b = a - -l * b"*)
11.124 - Thm ("vorzeichen_minus_weg2",num_str vorzeichen_minus_weg2),
11.125 + Thm ("vorzeichen_minus_weg2",num_str @{vorzeichen_minus_weg2),
11.126 (*"l kleiner 0 ==> a - l * b = a + -l * b"*)
11.127 - Thm ("vorzeichen_minus_weg3",num_str vorzeichen_minus_weg3),
11.128 + Thm ("vorzeichen_minus_weg3",num_str @{vorzeichen_minus_weg3),
11.129 (*"l kleiner 0 ==> k + a - l * b = k + a + -l * b"*)
11.130 - Thm ("vorzeichen_minus_weg4",num_str vorzeichen_minus_weg4),
11.131 + Thm ("vorzeichen_minus_weg4",num_str @{vorzeichen_minus_weg4),
11.132 (*"l kleiner 0 ==> k - a - l * b = k - a + -l * b"*)
11.133
11.134 Calc ("op *", eval_binop "#mult_"),
11.135 @@ -303,25 +303,25 @@
11.136 (*"1 * z = z"*)
11.137 Thm ("add_0_left",num_str @{thm add_0_left}),
11.138 (*"0 + z = z"*)
11.139 - Thm ("null_minus",num_str null_minus),
11.140 + Thm ("null_minus",num_str @{null_minus),
11.141 (*"0 - a = -a"*)
11.142 - Thm ("vor_minus_mal",num_str vor_minus_mal)
11.143 + Thm ("vor_minus_mal",num_str @{vor_minus_mal)
11.144 (*"- a * b = (-a) * b"*)
11.145
11.146 - (*Thm ("",num_str ),*)
11.147 + (*Thm ("",num_str @{),*)
11.148 (**)
11.149 ], scr = EmptyScr}:rls (*end verschoenere*);
11.150
11.151 val klammern_aufloesen =
11.152 Rls{id = "klammern_aufloesen", preconds = [],
11.153 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
11.154 - rules = [Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym)),
11.155 + rules = [Thm ("sym_real_add_assoc",num_str @{(real_add_assoc RS sym)),
11.156 (*"a + (b + c) = (a + b) + c"*)
11.157 - Thm ("klammer_plus_minus",num_str klammer_plus_minus),
11.158 + Thm ("klammer_plus_minus",num_str @{klammer_plus_minus),
11.159 (*"a + (b - c) = (a + b) - c"*)
11.160 - Thm ("klammer_minus_plus",num_str klammer_minus_plus),
11.161 + Thm ("klammer_minus_plus",num_str @{klammer_minus_plus),
11.162 (*"a - (b + c) = (a - b) - c"*)
11.163 - Thm ("klammer_minus_minus",num_str klammer_minus_minus)
11.164 + Thm ("klammer_minus_minus",num_str @{klammer_minus_minus)
11.165 (*"a - (b - c) = (a - b) + c"*)
11.166 ], scr = EmptyScr}:rls;
11.167
11.168 @@ -333,12 +333,12 @@
11.169 Thm ("left_distrib2",num_str @{thm left_distrib}2),
11.170 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
11.171
11.172 - Thm ("klammer_mult_minus",num_str klammer_mult_minus),
11.173 + Thm ("klammer_mult_minus",num_str @{klammer_mult_minus),
11.174 (*"a * (b - c) = a * b - a * c"*)
11.175 - Thm ("klammer_minus_mult",num_str klammer_minus_mult)
11.176 + Thm ("klammer_minus_mult",num_str @{klammer_minus_mult)
11.177 (*"(b - c) * a = b * a - c * a"*)
11.178
11.179 - (*Thm ("",num_str ),
11.180 + (*Thm ("",num_str @{),
11.181 (*""*)*)
11.182 ], scr = EmptyScr}:rls;
11.183
11.184 @@ -349,16 +349,16 @@
11.185 [Calc ("PolyMinus.kleiner", eval_kleiner ""),
11.186 Calc ("Atools.is'_atom", eval_is_atom "")
11.187 ],
11.188 - rules = [Thm ("tausche_mal",num_str tausche_mal),
11.189 + rules = [Thm ("tausche_mal",num_str @{tausche_mal),
11.190 (*"[| b is_atom; a kleiner b |] ==> (b * a) = (a * b)"*)
11.191 - Thm ("tausche_vor_mal",num_str tausche_vor_mal),
11.192 + Thm ("tausche_vor_mal",num_str @{tausche_vor_mal),
11.193 (*"[| b is_atom; a kleiner b |] ==> (-b * a) = (-a * b)"*)
11.194 - Thm ("tausche_mal_mal",num_str tausche_mal_mal),
11.195 + Thm ("tausche_mal_mal",num_str @{tausche_mal_mal),
11.196 (*"[| c is_atom; b kleiner c |] ==> (a * c * b) = (a * b *c)"*)
11.197 - Thm ("x_quadrat",num_str x_quadrat)
11.198 + Thm ("x_quadrat",num_str @{x_quadrat)
11.199 (*"(x * a) * a = x * a ^^^ 2"*)
11.200
11.201 - (*Thm ("",num_str ),
11.202 + (*Thm ("",num_str @{),
11.203 (*""*)*)
11.204 ], scr = EmptyScr}:rls;
11.205
11.206 @@ -423,9 +423,9 @@
11.207 (*"(?a | True) = True"*)
11.208 Thm ("or_false",or_false),
11.209 (*"(?a | False) = ?a"*)
11.210 - Thm ("not_true",num_str not_true),
11.211 + Thm ("not_true",num_str @{not_true),
11.212 (*"(~ True) = False"*)
11.213 - Thm ("not_false",num_str not_false)
11.214 + Thm ("not_false",num_str @{not_false)
11.215 (*"(~ False) = True"*)],
11.216 SOME "Vereinfache t_",
11.217 [["simplification","for_polynomials","with_minus"]]));
11.218 @@ -447,9 +447,9 @@
11.219 (*"(?a | True) = True"*)
11.220 Thm ("or_false",or_false),
11.221 (*"(?a | False) = ?a"*)
11.222 - Thm ("not_true",num_str not_true),
11.223 + Thm ("not_true",num_str @{not_true),
11.224 (*"(~ True) = False"*)
11.225 - Thm ("not_false",num_str not_false)
11.226 + Thm ("not_false",num_str @{not_false)
11.227 (*"(~ False) = True"*)],
11.228 SOME "Vereinfache t_",
11.229 [["simplification","for_polynomials","with_parentheses"]]));
11.230 @@ -519,9 +519,9 @@
11.231 (*"(?a & True) = ?a"*)
11.232 Thm ("and_false",and_false),
11.233 (*"(?a & False) = False"*)
11.234 - Thm ("not_true",num_str not_true),
11.235 + Thm ("not_true",num_str @{not_true),
11.236 (*"(~ True) = False"*)
11.237 - Thm ("not_false",num_str not_false)
11.238 + Thm ("not_false",num_str @{not_false)
11.239 (*"(~ False) = True"*)],
11.240 crls = e_rls, nrls = rls_p_33},
11.241 "Script SimplifyScript (t_::real) = " ^
12.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Tue Aug 31 15:36:57 2010 +0200
12.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Tue Aug 31 16:00:13 2010 +0200
12.3 @@ -83,12 +83,12 @@
12.4 Calc ("Tools.rhs" ,eval_rhs ""),
12.5 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
12.6 Calc ("op =",eval_equal "#equal_"),
12.7 - Thm ("not_true",num_str not_true),
12.8 - Thm ("not_false",num_str not_false),
12.9 - Thm ("and_true",num_str and_true),
12.10 - Thm ("and_false",num_str and_false),
12.11 - Thm ("or_true",num_str or_true),
12.12 - Thm ("or_false",num_str or_false)
12.13 + Thm ("not_true",num_str @{not_true),
12.14 + Thm ("not_false",num_str @{not_false),
12.15 + Thm ("and_true",num_str @{and_true),
12.16 + Thm ("and_false",num_str @{and_false),
12.17 + Thm ("or_true",num_str @{or_true),
12.18 + Thm ("or_false",num_str @{or_false)
12.19 ];
12.20
12.21
12.22 @@ -103,8 +103,8 @@
12.23 eval_is_ratequation_in "")
12.24
12.25 ]))
12.26 - [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*)
12.27 - Thm ("or_commute",num_str or_commute) (*WN: ein Hack*)
12.28 + [Thm ("and_commute",num_str @{and_commute), (*WN: ein Hack*)
12.29 + Thm ("or_commute",num_str @{or_commute) (*WN: ein Hack*)
12.30 ];
12.31 ruleset' := overwritelthy thy (!ruleset',
12.32 [("rateq_erls",rateq_erls)(*FIXXXME:del with rls.rls'*)
12.33 @@ -120,8 +120,8 @@
12.34 Calc ("RatEq.is'_ratequation'_in",
12.35 eval_is_ratequation_in "")
12.36 ]))
12.37 - [Thm ("and_commute",num_str and_commute), (*WN: ein Hack*)
12.38 - Thm ("or_commute",num_str or_commute) (*WN: ein Hack*)
12.39 + [Thm ("and_commute",num_str @{and_commute), (*WN: ein Hack*)
12.40 + Thm ("or_commute",num_str @{or_commute) (*WN: ein Hack*)
12.41 ];
12.42
12.43 val RatEq_eliminate = prep_rls(
12.44 @@ -129,11 +129,11 @@
12.45 rew_ord = ("termlessI", termlessI), erls = rateq_erls, srls = Erls,
12.46 calc = [],
12.47 rules = [
12.48 - Thm("rat_mult_denominator_both",num_str rat_mult_denominator_both),
12.49 + Thm("rat_mult_denominator_both",num_str @{rat_mult_denominator_both),
12.50 (* a/b=c/d -> ad=cb *)
12.51 - Thm("rat_mult_denominator_left",num_str rat_mult_denominator_left),
12.52 + Thm("rat_mult_denominator_left",num_str @{rat_mult_denominator_left),
12.53 (* a =c/d -> ad=c *)
12.54 - Thm("rat_mult_denominator_right",num_str rat_mult_denominator_right)
12.55 + Thm("rat_mult_denominator_right",num_str @{rat_mult_denominator_right)
12.56 (* a/b=c -> a=cb *)
12.57 ],
12.58 scr = Script ((term_of o the o (parse thy)) "empty_script")
12.59 @@ -146,21 +146,21 @@
12.60 Rls {id = "RatEq_simplify", preconds = [], rew_ord = ("termlessI", termlessI),
12.61 erls = rateq_erls, srls = Erls, calc = [],
12.62 rules = [
12.63 - Thm("real_rat_mult_1",num_str real_rat_mult_1),
12.64 + Thm("real_rat_mult_1",num_str @{real_rat_mult_1),
12.65 (*a*(b/c) = (a*b)/c*)
12.66 - Thm("real_rat_mult_2",num_str real_rat_mult_2),
12.67 + Thm("real_rat_mult_2",num_str @{real_rat_mult_2),
12.68 (*(a/b)*(c/d) = (a*c)/(b*d)*)
12.69 - Thm("real_rat_mult_3",num_str real_rat_mult_3),
12.70 + Thm("real_rat_mult_3",num_str @{real_rat_mult_3),
12.71 (* (a/b)*c = (a*c)/b*)
12.72 - Thm("real_rat_pow",num_str real_rat_pow),
12.73 + Thm("real_rat_pow",num_str @{real_rat_pow),
12.74 (*(a/b)^^^2 = a^^^2/b^^^2*)
12.75 - Thm("real_diff_minus",num_str real_diff_minus),
12.76 + Thm("real_diff_minus",num_str @{real_diff_minus),
12.77 (* a - b = a + (-1) * b *)
12.78 - Thm("rat_double_rat_1",num_str rat_double_rat_1),
12.79 + Thm("rat_double_rat_1",num_str @{rat_double_rat_1),
12.80 (* (a / (c/d) = (a*d) / c) *)
12.81 - Thm("rat_double_rat_2",num_str rat_double_rat_2),
12.82 + Thm("rat_double_rat_2",num_str @{rat_double_rat_2),
12.83 (* ((a/b) / (c/d) = (a*d) / (b*c)) *)
12.84 - Thm("rat_double_rat_3",num_str rat_double_rat_3)
12.85 + Thm("rat_double_rat_3",num_str @{rat_double_rat_3)
12.86 (* ((a/b) / c = a / (b*c) ) *)
12.87 ],
12.88 scr = Script ((term_of o the o (parse thy)) "empty_script")
13.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Aug 31 15:36:57 2010 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Aug 31 16:00:13 2010 +0200
13.3 @@ -2764,8 +2764,8 @@
13.4 rules =
13.5 [Calc ("op =",eval_equal "#equal_"),
13.6 Calc ("Atools.is'_const",eval_const "#is_const_"),
13.7 - Thm ("not_true",num_str not_true),
13.8 - Thm ("not_false",num_str not_false)
13.9 + Thm ("not_true",num_str @{not_true),
13.10 + Thm ("not_false",num_str @{not_false)
13.11 ],
13.12 scr = EmptyScr});
13.13
13.14 @@ -2782,43 +2782,43 @@
13.15 [Calc ("HOL.divide" ,eval_cancel "#divide_"),
13.16
13.17 Thm ("minus_divide_left",
13.18 - num_str (real_minus_divide_eq RS sym)),
13.19 + num_str @{(real_minus_divide_eq RS sym)),
13.20 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
13.21
13.22 - Thm ("rat_add",num_str rat_add),
13.23 + Thm ("rat_add",num_str @{rat_add),
13.24 (*"[| a is_const; b is_const; c is_const; d is_const |] ==> \
13.25 \"a / c + b / d = (a * d) / (c * d) + (b * c ) / (d * c)"*)
13.26 - Thm ("rat_add1",num_str rat_add1),
13.27 + Thm ("rat_add1",num_str @{rat_add1),
13.28 (*"[| a is_const; b is_const; c is_const |] ==> \
13.29 \"a / c + b / c = (a + b) / c"*)
13.30 - Thm ("rat_add2",num_str rat_add2),
13.31 + Thm ("rat_add2",num_str @{rat_add2),
13.32 (*"[| ?a is_const; ?b is_const; ?c is_const |] ==> \
13.33 \?a / ?c + ?b = (?a + ?b * ?c) / ?c"*)
13.34 - Thm ("rat_add3",num_str rat_add3),
13.35 + Thm ("rat_add3",num_str @{rat_add3),
13.36 (*"[| a is_const; b is_const; c is_const |] ==> \
13.37 \"a + b / c = (a * c) / c + b / c"\
13.38 \.... is_const to be omitted here FIXME*)
13.39
13.40 - Thm ("rat_mult",num_str rat_mult),
13.41 + Thm ("rat_mult",num_str @{rat_mult),
13.42 (*a / b * (c / d) = a * c / (b * d)*)
13.43 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
13.44 (*?x * (?y / ?z) = ?x * ?y / ?z*)
13.45 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
13.46 (*?y / ?z * ?x = ?y * ?x / ?z*)
13.47
13.48 - Thm ("real_divide_divide1",num_str real_divide_divide1),
13.49 + Thm ("real_divide_divide1",num_str @{real_divide_divide1),
13.50 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
13.51 Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left}),
13.52 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
13.53
13.54 - Thm ("rat_power", num_str rat_power),
13.55 + Thm ("rat_power", num_str @{rat_power),
13.56 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
13.57
13.58 - Thm ("mult_cross",num_str mult_cross),
13.59 + Thm ("mult_cross",num_str @{mult_cross),
13.60 (*"[| b ~= 0; d ~= 0 |] ==> (a / b = c / d) = (a * d = b * c)*)
13.61 - Thm ("mult_cross1",num_str mult_cross1),
13.62 + Thm ("mult_cross1",num_str @{mult_cross1),
13.63 (*" b ~= 0 ==> (a / b = c ) = (a = b * c)*)
13.64 - Thm ("mult_cross2",num_str mult_cross2)
13.65 + Thm ("mult_cross2",num_str @{mult_cross2)
13.66 (*" d ~= 0 ==> (a = c / d) = (a * d = c)*)
13.67 ], scr = EmptyScr})
13.68 calculate_Poly);
13.69 @@ -2912,7 +2912,7 @@
13.70 val SOME (t'',asm) = cancel_p_ thy t
13.71 val der = reverse_deriv thy eval_rls rules ro NONE t'
13.72 val der = der @ [(Thm ("real_mult_div_cancel2",
13.73 - num_str real_mult_div_cancel2),
13.74 + num_str @{real_mult_div_cancel2),
13.75 (t'',asm))]
13.76 val rs = (distinct_Thm o (map #1)) der
13.77 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
13.78 @@ -3043,7 +3043,7 @@
13.79 val SOME (t'',asm) = cancel_ thy t;
13.80 val der = reverse_deriv thy eval_rls rules ro NONE t';
13.81 val der = der @ [(Thm ("real_mult_div_cancel2",
13.82 - num_str real_mult_div_cancel2),
13.83 + num_str @{real_mult_div_cancel2),
13.84 (t'',asm))]
13.85 val rs = map #1 der;
13.86 in (t,t'',[rs],der) end;
13.87 @@ -3137,7 +3137,7 @@
13.88 val SOME (t'',asm) = add_fraction_p_ thy t;
13.89 val der = reverse_deriv thy eval_rls rules ro NONE t';
13.90 val der = der @ [(Thm ("real_mult_div_cancel2",
13.91 - num_str real_mult_div_cancel2),
13.92 + num_str @{real_mult_div_cancel2),
13.93 (t'',asm))]
13.94 val rs = (distinct_Thm o (map #1)) der;
13.95 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
13.96 @@ -3286,7 +3286,7 @@
13.97 val SOME (t'',asm) = add_fraction_ thy t;
13.98 val der = reverse_deriv thy eval_rls rules ro NONE t';
13.99 val der = der @ [(Thm ("real_mult_div_cancel2",
13.100 - num_str real_mult_div_cancel2),
13.101 + num_str @{real_mult_div_cancel2),
13.102 (t'',asm))]
13.103 val rs = (distinct_Thm o (map #1)) der;
13.104 val rs = filter_out (eq_Thms ["sym_real_add_zero_left",
13.105 @@ -3457,9 +3457,9 @@
13.106 val discard_minus = prep_rls(
13.107 Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
13.108 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
13.109 - rules = [Thm ("real_diff_minus", num_str real_diff_minus),
13.110 + rules = [Thm ("real_diff_minus", num_str @{real_diff_minus),
13.111 (*"a - b = a + -1 * b"*)
13.112 - Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym))
13.113 + Thm ("sym_real_mult_minus1",num_str @{(real_mult_minus1 RS sym))
13.114 (*- ?z = "-1 * ?z"*)
13.115 ],
13.116 scr = Script ((term_of o the o (parse thy))
13.117 @@ -3484,29 +3484,29 @@
13.118 val powers = prep_rls(
13.119 Rls {id = "powers", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
13.120 erls = powers_erls, srls = Erls, calc = [], (*asm_thm = [],*)
13.121 - rules = [Thm ("realpow_multI", num_str realpow_multI),
13.122 + rules = [Thm ("realpow_multI", num_str @{realpow_multI),
13.123 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
13.124 - Thm ("realpow_pow",num_str realpow_pow),
13.125 + Thm ("realpow_pow",num_str @{realpow_pow),
13.126 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
13.127 - Thm ("realpow_oneI",num_str realpow_oneI),
13.128 + Thm ("realpow_oneI",num_str @{realpow_oneI),
13.129 (*"r ^^^ 1 = r"*)
13.130 - Thm ("realpow_minus_even",num_str realpow_minus_even),
13.131 + Thm ("realpow_minus_even",num_str @{realpow_minus_even),
13.132 (*"n is_even ==> (- r) ^^^ n = r ^^^ n" ?-->discard_minus?*)
13.133 - Thm ("realpow_minus_odd",num_str realpow_minus_odd),
13.134 + Thm ("realpow_minus_odd",num_str @{realpow_minus_odd),
13.135 (*"Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"*)
13.136
13.137 (*----- collect atoms over * -----*)
13.138 - Thm ("realpow_two_atom",num_str realpow_two_atom),
13.139 + Thm ("realpow_two_atom",num_str @{realpow_two_atom),
13.140 (*"r is_atom ==> r * r = r ^^^ 2"*)
13.141 - Thm ("realpow_plus_1",num_str realpow_plus_1),
13.142 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
13.143 (*"r is_atom ==> r * r ^^^ n = r ^^^ (n + 1)"*)
13.144 - Thm ("realpow_addI_atom",num_str realpow_addI_atom),
13.145 + Thm ("realpow_addI_atom",num_str @{realpow_addI_atom),
13.146 (*"r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
13.147
13.148 (*----- distribute none-atoms -----*)
13.149 - Thm ("realpow_def_atom",num_str realpow_def_atom),
13.150 + Thm ("realpow_def_atom",num_str @{realpow_def_atom),
13.151 (*"[| 1 < n; not(r is_atom) |]==>r ^^^ n = r * r ^^^ (n + -1)"*)
13.152 - Thm ("realpow_eq_oneI",num_str realpow_eq_oneI),
13.153 + Thm ("realpow_eq_oneI",num_str @{realpow_eq_oneI),
13.154 (*"1 ^^^ n = 1"*)
13.155 Calc ("op +",eval_binop "#add_")
13.156 ],
13.157 @@ -3518,7 +3518,7 @@
13.158 Rls {id = "rat_mult_divide", preconds = [],
13.159 rew_ord = ("dummy_ord",dummy_ord),
13.160 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
13.161 - rules = [Thm ("rat_mult",num_str rat_mult),
13.162 + rules = [Thm ("rat_mult",num_str @{rat_mult),
13.163 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
13.164 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
13.165 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
13.166 @@ -3543,9 +3543,9 @@
13.167 "?x / 1 = ?x" unnecess.for normalform*)
13.168 Thm ("mult_1_left",num_str @{thm mult_1_left}),
13.169 (*"1 * z = z"*)
13.170 - (*Thm ("real_mult_minus1",num_str real_mult_minus1),
13.171 + (*Thm ("real_mult_minus1",num_str @{real_mult_minus1),
13.172 "-1 * z = - z"*)
13.173 - (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel),
13.174 + (*Thm ("real_minus_mult_cancel",num_str @{real_minus_mult_cancel),
13.175 "- ?x * - ?y = ?x * ?y"*)
13.176
13.177 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
13.178 @@ -3555,9 +3555,9 @@
13.179 (*Thm ("right_minus",num_str @{thm right_minus}),
13.180 "?z + - ?z = 0"*)
13.181
13.182 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
13.183 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
13.184 (*"z1 + z1 = 2 * z1"*)
13.185 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
13.186 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
13.187 (*"z1 + (z1 + k) = 2 * z1 + k"*)
13.188
13.189 Thm ("divide_zero_left",num_str @{thm divide_zero_left})
13.190 @@ -3617,22 +3617,22 @@
13.191 (append_rls "divide" calculate_Rational
13.192 [Thm ("divide_1",num_str @{thm divide_1}),
13.193 (*"?x / 1 = ?x"*)
13.194 - Thm ("rat_mult",num_str rat_mult),
13.195 + Thm ("rat_mult",num_str @{rat_mult),
13.196 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
13.197 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
13.198 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
13.199 otherwise inv.to a / b / c = ...*)
13.200 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
13.201 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
13.202 - Thm ("add_minus",num_str add_minus),
13.203 + Thm ("add_minus",num_str @{add_minus),
13.204 (*"?a + ?b - ?b = ?a"*)
13.205 - Thm ("add_minus1",num_str add_minus1),
13.206 + Thm ("add_minus1",num_str @{add_minus1),
13.207 (*"?a - ?b + ?b = ?a"*)
13.208 - Thm ("real_divide_minus1",num_str real_divide_minus1)
13.209 + Thm ("real_divide_minus1",num_str @{real_divide_minus1)
13.210 (*"?x / -1 = - ?x"*)
13.211 (*
13.212 ,
13.213 - Thm ("",num_str )
13.214 + Thm ("",num_str @{)
13.215 *)
13.216 ]);
13.217
13.218 @@ -3674,9 +3674,9 @@
13.219 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
13.220 srls = Erls, calc = [],
13.221 rules =
13.222 - [Thm ("rat_mult_poly_l",num_str rat_mult_poly_l),
13.223 + [Thm ("rat_mult_poly_l",num_str @{rat_mult_poly_l),
13.224 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
13.225 - Thm ("rat_mult_poly_r",num_str rat_mult_poly_r)
13.226 + Thm ("rat_mult_poly_r",num_str @{rat_mult_poly_r)
13.227 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
13.228 ],
13.229 scr = EmptyScr});
13.230 @@ -3696,11 +3696,11 @@
13.231 error "rational.sml.sml: diff.behav. in norm_Rational_mg 29" etc.
13.232 thus we decided to go on with this flaw*)
13.233 srls = Erls, calc = [],
13.234 - rules = [Thm ("rat_mult",num_str rat_mult),
13.235 + rules = [Thm ("rat_mult",num_str @{rat_mult),
13.236 (*"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
13.237 - Thm ("rat_mult_poly_l",num_str rat_mult_poly_l),
13.238 + Thm ("rat_mult_poly_l",num_str @{rat_mult_poly_l),
13.239 (*"?c is_polyexp ==> ?c * (?a / ?b) = ?c * ?a / ?b"*)
13.240 - Thm ("rat_mult_poly_r",num_str rat_mult_poly_r),
13.241 + Thm ("rat_mult_poly_r",num_str @{rat_mult_poly_r),
13.242 (*"?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"*)
13.243
13.244 Thm ("real_divide_divide1_mg", real_divide_divide1_mg),
13.245 @@ -3711,7 +3711,7 @@
13.246 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
13.247 Calc ("HOL.divide" ,eval_cancel "#divide_"),
13.248
13.249 - Thm ("rat_power", num_str rat_power)
13.250 + Thm ("rat_power", num_str @{rat_power)
13.251 (*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
13.252 ],
13.253 scr = Script ((term_of o the o (parse thy)) "empty_script")
14.1 --- a/src/Tools/isac/Knowledge/Root.thy Tue Aug 31 15:36:57 2010 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Root.thy Tue Aug 31 16:00:13 2010 +0200
14.3 @@ -163,7 +163,7 @@
14.4 (*-------------------------rulse-------------------------*)
14.5 val Root_crls =
14.6 append_rls "Root_crls" Atools_erls
14.7 - [Thm ("real_unari_minus",num_str real_unari_minus),
14.8 + [Thm ("real_unari_minus",num_str @{real_unari_minus),
14.9 Calc ("Root.sqrt" ,eval_sqrt "#sqrt_"),
14.10 Calc ("HOL.divide",eval_cancel "#divide_"),
14.11 Calc ("Atools.pow" ,eval_binop "#power_"),
14.12 @@ -175,7 +175,7 @@
14.13
14.14 val Root_erls =
14.15 append_rls "Root_erls" Atools_erls
14.16 - [Thm ("real_unari_minus",num_str real_unari_minus),
14.17 + [Thm ("real_unari_minus",num_str @{real_unari_minus),
14.18 Calc ("Root.sqrt" ,eval_sqrt "#sqrt_"),
14.19 Calc ("HOL.divide",eval_cancel "#divide_"),
14.20 Calc ("Atools.pow" ,eval_binop "#power_"),
14.21 @@ -195,7 +195,7 @@
14.22 erls = Atools_erls, srls = Erls,
14.23 calc = [],
14.24 (*asm_thm = [],*)
14.25 - rules = [Thm ("real_diff_minus",num_str real_diff_minus),
14.26 + rules = [Thm ("real_diff_minus",num_str @{real_diff_minus),
14.27 (*"a - b = a + (-1) * b"*)
14.28
14.29 Thm ("left_distrib" ,num_str @{thm left_distrib}),
14.30 @@ -214,11 +214,11 @@
14.31 Thm ("add_0_left",num_str @{thm add_0_left}),
14.32 (*"0 + z = z"*)
14.33
14.34 - Thm ("real_mult_commute",num_str real_mult_commute),
14.35 + Thm ("real_mult_commute",num_str @{real_mult_commute),
14.36 (*AC-rewriting*)
14.37 - Thm ("real_mult_left_commute",num_str real_mult_left_commute),
14.38 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute),
14.39 (**)
14.40 - Thm ("real_mult_assoc",num_str real_mult_assoc),
14.41 + Thm ("real_mult_assoc",num_str @{real_mult_assoc),
14.42 (**)
14.43 Thm ("add_commute",num_str @{thm add_commute}),
14.44 (**)
14.45 @@ -227,23 +227,23 @@
14.46 Thm ("add_assoc",num_str @{thm add_assoc}),
14.47 (**)
14.48
14.49 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
14.50 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
14.51 (*"r1 * r1 = r1 ^^^ 2"*)
14.52 - Thm ("realpow_plus_1",num_str realpow_plus_1),
14.53 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
14.54 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
14.55 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
14.56 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
14.57 (*"z1 + z1 = 2 * z1"*)
14.58 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
14.59 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
14.60 (*"z1 + (z1 + k) = 2 * z1 + k"*)
14.61
14.62 - Thm ("real_num_collect",num_str real_num_collect),
14.63 + Thm ("real_num_collect",num_str @{real_num_collect),
14.64 (*"[| l is_const; m is_const |]==> l * n + m * n = (l + m) * n"*)
14.65 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
14.66 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
14.67 (*"[| l is_const; m is_const |] ==>
14.68 l * n + (m * n + k) = (l + m) * n + k"*)
14.69 - Thm ("real_one_collect",num_str real_one_collect),
14.70 + Thm ("real_one_collect",num_str @{real_one_collect),
14.71 (*"m is_const ==> n + m * n = (1 + m) * n"*)
14.72 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
14.73 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
14.74 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
14.75
14.76 Calc ("op +", eval_binop "#add_"),
14.77 @@ -262,28 +262,28 @@
14.78 erls = Atools_erls, srls = Erls,
14.79 calc = [],
14.80 (*asm_thm = [],*)
14.81 - rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
14.82 + rules = [Thm ("real_plus_binom_pow2" ,num_str @{real_plus_binom_pow2),
14.83 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
14.84 - Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
14.85 + Thm ("real_plus_binom_times" ,num_str @{real_plus_binom_times),
14.86 (*"(a + b)*(a + b) = ...*)
14.87 - Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
14.88 + Thm ("real_minus_binom_pow2" ,num_str @{real_minus_binom_pow2),
14.89 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
14.90 - Thm ("real_minus_binom_times",num_str real_minus_binom_times),
14.91 + Thm ("real_minus_binom_times",num_str @{real_minus_binom_times),
14.92 (*"(a - b)*(a - b) = ...*)
14.93 - Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
14.94 + Thm ("real_plus_minus_binom1",num_str @{real_plus_minus_binom1),
14.95 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
14.96 - Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
14.97 + Thm ("real_plus_minus_binom2",num_str @{real_plus_minus_binom2),
14.98 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
14.99 (*RL 020915*)
14.100 - Thm ("real_pp_binom_times",num_str real_pp_binom_times),
14.101 + Thm ("real_pp_binom_times",num_str @{real_pp_binom_times),
14.102 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
14.103 - Thm ("real_pm_binom_times",num_str real_pm_binom_times),
14.104 + Thm ("real_pm_binom_times",num_str @{real_pm_binom_times),
14.105 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
14.106 - Thm ("real_mp_binom_times",num_str real_mp_binom_times),
14.107 + Thm ("real_mp_binom_times",num_str @{real_mp_binom_times),
14.108 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
14.109 - Thm ("real_mm_binom_times",num_str real_mm_binom_times),
14.110 + Thm ("real_mm_binom_times",num_str @{real_mm_binom_times),
14.111 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
14.112 - Thm ("realpow_mul",num_str realpow_mul),
14.113 + Thm ("realpow_mul",num_str @{realpow_mul),
14.114 (*(a*b)^^^n = a^^^n * b^^^n*)
14.115
14.116 Thm ("mult_1_left",num_str @{thm mult_1_left}), (*"1 * z = z"*)
14.117 @@ -298,21 +298,21 @@
14.118 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
14.119 Calc ("Atools.pow", eval_binop "#power_"),
14.120
14.121 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
14.122 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
14.123 (*"r1 * r1 = r1 ^^^ 2"*)
14.124 - Thm ("realpow_plus_1",num_str realpow_plus_1),
14.125 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
14.126 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
14.127 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
14.128 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
14.129 (*"z1 + (z1 + k) = 2 * z1 + k"*)
14.130
14.131 - Thm ("real_num_collect",num_str real_num_collect),
14.132 + Thm ("real_num_collect",num_str @{real_num_collect),
14.133 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
14.134 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
14.135 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
14.136 (*"[| l is_const; m is_const |] ==>
14.137 l * n + (m * n + k) = (l + m) * n + k"*)
14.138 - Thm ("real_one_collect",num_str real_one_collect),
14.139 + Thm ("real_one_collect",num_str @{real_one_collect),
14.140 (*"m is_const ==> n + m * n = (1 + m) * n"*)
14.141 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
14.142 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
14.143 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
14.144
14.145 Calc ("op +", eval_binop "#add_"),
15.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Aug 31 15:36:57 2010 +0200
15.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Aug 31 16:00:13 2010 +0200
15.3 @@ -204,12 +204,12 @@
15.4 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
15.5 Calc ("RootEq.is'_normSqrtTerm'_in",eval_is_normSqrtTerm_in ""),
15.6 Calc ("op =",eval_equal "#equal_"),
15.7 - Thm ("not_true",num_str not_true),
15.8 - Thm ("not_false",num_str not_false),
15.9 - Thm ("and_true",num_str and_true),
15.10 - Thm ("and_false",num_str and_false),
15.11 - Thm ("or_true",num_str or_true),
15.12 - Thm ("or_false",num_str or_false)
15.13 + Thm ("not_true",num_str @{not_true),
15.14 + Thm ("not_false",num_str @{not_false),
15.15 + Thm ("and_true",num_str @{and_true),
15.16 + Thm ("and_false",num_str @{and_false),
15.17 + Thm ("or_true",num_str @{or_true),
15.18 + Thm ("or_false",num_str @{or_false)
15.19 ];
15.20
15.21 val RootEq_erls =
15.22 @@ -240,95 +240,95 @@
15.23 Rls {id = "sqrt_isolate", preconds = [], rew_ord = ("termlessI",termlessI),
15.24 erls = RootEq_erls, srls = Erls, calc = [],
15.25 rules = [
15.26 - Thm("sqrt_square_1",num_str sqrt_square_1),
15.27 + Thm("sqrt_square_1",num_str @{sqrt_square_1),
15.28 (* (sqrt a)^^^2 -> a *)
15.29 - Thm("sqrt_square_2",num_str sqrt_square_2),
15.30 + Thm("sqrt_square_2",num_str @{sqrt_square_2),
15.31 (* sqrt (a^^^2) -> a *)
15.32 - Thm("sqrt_times_root_1",num_str sqrt_times_root_1),
15.33 + Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1),
15.34 (* sqrt a sqrt b -> sqrt(ab) *)
15.35 - Thm("sqrt_times_root_2",num_str sqrt_times_root_2),
15.36 + Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2),
15.37 (* a sqrt b sqrt c -> a sqrt(bc) *)
15.38 Thm("sqrt_square_equation_both_1",
15.39 - num_str sqrt_square_equation_both_1),
15.40 + num_str @{sqrt_square_equation_both_1),
15.41 (* (sqrt a + sqrt b = sqrt c + sqrt d) ->
15.42 (a+2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
15.43 Thm("sqrt_square_equation_both_2",
15.44 - num_str sqrt_square_equation_both_2),
15.45 + num_str @{sqrt_square_equation_both_2),
15.46 (* (sqrt a - sqrt b = sqrt c + sqrt d) ->
15.47 (a-2*sqrt(a)*sqrt(b)+b) = c+2*sqrt(c)*sqrt(d)+d) *)
15.48 Thm("sqrt_square_equation_both_3",
15.49 - num_str sqrt_square_equation_both_3),
15.50 + num_str @{sqrt_square_equation_both_3),
15.51 (* (sqrt a + sqrt b = sqrt c - sqrt d) ->
15.52 (a+2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
15.53 Thm("sqrt_square_equation_both_4",
15.54 - num_str sqrt_square_equation_both_4),
15.55 + num_str @{sqrt_square_equation_both_4),
15.56 (* (sqrt a - sqrt b = sqrt c - sqrt d) ->
15.57 (a-2*sqrt(a)*sqrt(b)+b) = c-2*sqrt(c)*sqrt(d)+d) *)
15.58 Thm("sqrt_isolate_l_add1",
15.59 - num_str sqrt_isolate_l_add1),
15.60 + num_str @{sqrt_isolate_l_add1),
15.61 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
15.62 Thm("sqrt_isolate_l_add2",
15.63 - num_str sqrt_isolate_l_add2),
15.64 + num_str @{sqrt_isolate_l_add2),
15.65 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
15.66 Thm("sqrt_isolate_l_add3",
15.67 - num_str sqrt_isolate_l_add3),
15.68 + num_str @{sqrt_isolate_l_add3),
15.69 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
15.70 Thm("sqrt_isolate_l_add4",
15.71 - num_str sqrt_isolate_l_add4),
15.72 + num_str @{sqrt_isolate_l_add4),
15.73 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
15.74 Thm("sqrt_isolate_l_add5",
15.75 - num_str sqrt_isolate_l_add5),
15.76 + num_str @{sqrt_isolate_l_add5),
15.77 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
15.78 Thm("sqrt_isolate_l_add6",
15.79 - num_str sqrt_isolate_l_add6),
15.80 + num_str @{sqrt_isolate_l_add6),
15.81 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
15.82 - (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*)
15.83 + (*Thm("sqrt_isolate_l_div",num_str @{sqrt_isolate_l_div),*)
15.84 (* b*sqrt(x) = d sqrt(x) d/b *)
15.85 Thm("sqrt_isolate_r_add1",
15.86 - num_str sqrt_isolate_r_add1),
15.87 + num_str @{sqrt_isolate_r_add1),
15.88 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
15.89 Thm("sqrt_isolate_r_add2",
15.90 - num_str sqrt_isolate_r_add2),
15.91 + num_str @{sqrt_isolate_r_add2),
15.92 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
15.93 Thm("sqrt_isolate_r_add3",
15.94 - num_str sqrt_isolate_r_add3),
15.95 + num_str @{sqrt_isolate_r_add3),
15.96 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
15.97 Thm("sqrt_isolate_r_add4",
15.98 - num_str sqrt_isolate_r_add4),
15.99 + num_str @{sqrt_isolate_r_add4),
15.100 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
15.101 Thm("sqrt_isolate_r_add5",
15.102 - num_str sqrt_isolate_r_add5),
15.103 + num_str @{sqrt_isolate_r_add5),
15.104 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
15.105 Thm("sqrt_isolate_r_add6",
15.106 - num_str sqrt_isolate_r_add6),
15.107 + num_str @{sqrt_isolate_r_add6),
15.108 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
15.109 - (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*)
15.110 + (*Thm("sqrt_isolate_r_div",num_str @{sqrt_isolate_r_div),*)
15.111 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
15.112 Thm("sqrt_square_equation_left_1",
15.113 - num_str sqrt_square_equation_left_1),
15.114 + num_str @{sqrt_square_equation_left_1),
15.115 (* sqrt(x)=b -> x=b^2 *)
15.116 Thm("sqrt_square_equation_left_2",
15.117 - num_str sqrt_square_equation_left_2),
15.118 + num_str @{sqrt_square_equation_left_2),
15.119 (* c*sqrt(x)=b -> c^2*x=b^2 *)
15.120 - Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3),
15.121 + Thm("sqrt_square_equation_left_3",num_str @{sqrt_square_equation_left_3),
15.122 (* c/sqrt(x)=b -> c^2/x=b^2 *)
15.123 - Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4),
15.124 + Thm("sqrt_square_equation_left_4",num_str @{sqrt_square_equation_left_4),
15.125 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
15.126 - Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5),
15.127 + Thm("sqrt_square_equation_left_5",num_str @{sqrt_square_equation_left_5),
15.128 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
15.129 - Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6),
15.130 + Thm("sqrt_square_equation_left_6",num_str @{sqrt_square_equation_left_6),
15.131 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
15.132 - Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1),
15.133 + Thm("sqrt_square_equation_right_1",num_str @{sqrt_square_equation_right_1),
15.134 (* a=sqrt(x) ->a^2=x *)
15.135 - Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2),
15.136 + Thm("sqrt_square_equation_right_2",num_str @{sqrt_square_equation_right_2),
15.137 (* a=c*sqrt(x) ->a^2=c^2*x *)
15.138 - Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3),
15.139 + Thm("sqrt_square_equation_right_3",num_str @{sqrt_square_equation_right_3),
15.140 (* a=c/sqrt(x) ->a^2=c^2/x *)
15.141 - Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4),
15.142 + Thm("sqrt_square_equation_right_4",num_str @{sqrt_square_equation_right_4),
15.143 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
15.144 - Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5),
15.145 + Thm("sqrt_square_equation_right_5",num_str @{sqrt_square_equation_right_5),
15.146 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
15.147 - Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6)
15.148 + Thm("sqrt_square_equation_right_6",num_str @{sqrt_square_equation_right_6)
15.149 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
15.150 ],scr = Script ((term_of o the o (parse thy)) "empty_script")
15.151 }:rls);
15.152 @@ -343,39 +343,39 @@
15.153 rew_ord = ("termlessI",termlessI),
15.154 erls = RootEq_erls, srls = Erls, calc = [],
15.155 rules = [
15.156 - Thm("sqrt_square_1",num_str sqrt_square_1),
15.157 + Thm("sqrt_square_1",num_str @{sqrt_square_1),
15.158 (* (sqrt a)^^^2 -> a *)
15.159 - Thm("sqrt_square_2",num_str sqrt_square_2),
15.160 + Thm("sqrt_square_2",num_str @{sqrt_square_2),
15.161 (* sqrt (a^^^2) -> a *)
15.162 - Thm("sqrt_times_root_1",num_str sqrt_times_root_1),
15.163 + Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1),
15.164 (* sqrt a sqrt b -> sqrt(ab) *)
15.165 - Thm("sqrt_times_root_2",num_str sqrt_times_root_2),
15.166 + Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2),
15.167 (* a sqrt b sqrt c -> a sqrt(bc) *)
15.168 - Thm("sqrt_isolate_l_add1",num_str sqrt_isolate_l_add1),
15.169 + Thm("sqrt_isolate_l_add1",num_str @{sqrt_isolate_l_add1),
15.170 (* a+b*sqrt(x)=d -> b*sqrt(x) = d-a *)
15.171 - Thm("sqrt_isolate_l_add2",num_str sqrt_isolate_l_add2),
15.172 + Thm("sqrt_isolate_l_add2",num_str @{sqrt_isolate_l_add2),
15.173 (* a+ sqrt(x)=d -> sqrt(x) = d-a *)
15.174 - Thm("sqrt_isolate_l_add3",num_str sqrt_isolate_l_add3),
15.175 + Thm("sqrt_isolate_l_add3",num_str @{sqrt_isolate_l_add3),
15.176 (* a+b*c/sqrt(x)=d->b*c/sqrt(x)=d-a *)
15.177 - Thm("sqrt_isolate_l_add4",num_str sqrt_isolate_l_add4),
15.178 + Thm("sqrt_isolate_l_add4",num_str @{sqrt_isolate_l_add4),
15.179 (* a+c/sqrt(x)=d -> c/sqrt(x) = d-a *)
15.180 - Thm("sqrt_isolate_l_add5",num_str sqrt_isolate_l_add5),
15.181 + Thm("sqrt_isolate_l_add5",num_str @{sqrt_isolate_l_add5),
15.182 (* a+b*c/f*sqrt(x)=d->b*c/f*sqrt(x)=d-a *)
15.183 - Thm("sqrt_isolate_l_add6",num_str sqrt_isolate_l_add6),
15.184 + Thm("sqrt_isolate_l_add6",num_str @{sqrt_isolate_l_add6),
15.185 (* a+c/f*sqrt(x)=d -> c/f*sqrt(x) = d-a *)
15.186 - (*Thm("sqrt_isolate_l_div",num_str sqrt_isolate_l_div),*)
15.187 + (*Thm("sqrt_isolate_l_div",num_str @{sqrt_isolate_l_div),*)
15.188 (* b*sqrt(x) = d sqrt(x) d/b *)
15.189 - Thm("sqrt_square_equation_left_1",num_str sqrt_square_equation_left_1),
15.190 + Thm("sqrt_square_equation_left_1",num_str @{sqrt_square_equation_left_1),
15.191 (* sqrt(x)=b -> x=b^2 *)
15.192 - Thm("sqrt_square_equation_left_2",num_str sqrt_square_equation_left_2),
15.193 + Thm("sqrt_square_equation_left_2",num_str @{sqrt_square_equation_left_2),
15.194 (* a*sqrt(x)=b -> a^2*x=b^2*)
15.195 - Thm("sqrt_square_equation_left_3",num_str sqrt_square_equation_left_3),
15.196 + Thm("sqrt_square_equation_left_3",num_str @{sqrt_square_equation_left_3),
15.197 (* c/sqrt(x)=b -> c^2/x=b^2 *)
15.198 - Thm("sqrt_square_equation_left_4",num_str sqrt_square_equation_left_4),
15.199 + Thm("sqrt_square_equation_left_4",num_str @{sqrt_square_equation_left_4),
15.200 (* c*d/sqrt(x)=b -> c^2*d^2/x=b^2 *)
15.201 - Thm("sqrt_square_equation_left_5",num_str sqrt_square_equation_left_5),
15.202 + Thm("sqrt_square_equation_left_5",num_str @{sqrt_square_equation_left_5),
15.203 (* c/d*sqrt(x)=b -> c^2/d^2x=b^2 *)
15.204 - Thm("sqrt_square_equation_left_6",num_str sqrt_square_equation_left_6)
15.205 + Thm("sqrt_square_equation_left_6",num_str @{sqrt_square_equation_left_6)
15.206 (* c*d/g*sqrt(x)=b -> c^2*d^2/g^2x=b^2 *)
15.207 ],
15.208 scr = Script ((term_of o the o (parse thy)) "empty_script")
15.209 @@ -392,39 +392,39 @@
15.210 rew_ord = ("termlessI",termlessI),
15.211 erls = RootEq_erls, srls = Erls, calc = [],
15.212 rules = [
15.213 - Thm("sqrt_square_1",num_str sqrt_square_1),
15.214 + Thm("sqrt_square_1",num_str @{sqrt_square_1),
15.215 (* (sqrt a)^^^2 -> a *)
15.216 - Thm("sqrt_square_2",num_str sqrt_square_2),
15.217 + Thm("sqrt_square_2",num_str @{sqrt_square_2),
15.218 (* sqrt (a^^^2) -> a *)
15.219 - Thm("sqrt_times_root_1",num_str sqrt_times_root_1),
15.220 + Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1),
15.221 (* sqrt a sqrt b -> sqrt(ab) *)
15.222 - Thm("sqrt_times_root_2",num_str sqrt_times_root_2),
15.223 + Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2),
15.224 (* a sqrt b sqrt c -> a sqrt(bc) *)
15.225 - Thm("sqrt_isolate_r_add1",num_str sqrt_isolate_r_add1),
15.226 + Thm("sqrt_isolate_r_add1",num_str @{sqrt_isolate_r_add1),
15.227 (* a= d+e*sqrt(x) -> a-d=e*sqrt(x) *)
15.228 - Thm("sqrt_isolate_r_add2",num_str sqrt_isolate_r_add2),
15.229 + Thm("sqrt_isolate_r_add2",num_str @{sqrt_isolate_r_add2),
15.230 (* a= d+ sqrt(x) -> a-d= sqrt(x) *)
15.231 - Thm("sqrt_isolate_r_add3",num_str sqrt_isolate_r_add3),
15.232 + Thm("sqrt_isolate_r_add3",num_str @{sqrt_isolate_r_add3),
15.233 (* a=d+e*g/sqrt(x)->a-d=e*g/sqrt(x)*)
15.234 - Thm("sqrt_isolate_r_add4",num_str sqrt_isolate_r_add4),
15.235 + Thm("sqrt_isolate_r_add4",num_str @{sqrt_isolate_r_add4),
15.236 (* a= d+g/sqrt(x) -> a-d=g/sqrt(x) *)
15.237 - Thm("sqrt_isolate_r_add5",num_str sqrt_isolate_r_add5),
15.238 + Thm("sqrt_isolate_r_add5",num_str @{sqrt_isolate_r_add5),
15.239 (* a=d+e*g/h*sqrt(x)->a-d=e*g/h*sqrt(x)*)
15.240 - Thm("sqrt_isolate_r_add6",num_str sqrt_isolate_r_add6),
15.241 + Thm("sqrt_isolate_r_add6",num_str @{sqrt_isolate_r_add6),
15.242 (* a= d+g/h*sqrt(x) -> a-d=g/h*sqrt(x) *)
15.243 - (*Thm("sqrt_isolate_r_div",num_str sqrt_isolate_r_div),*)
15.244 + (*Thm("sqrt_isolate_r_div",num_str @{sqrt_isolate_r_div),*)
15.245 (* a=e*sqrt(x) -> a/e = sqrt(x) *)
15.246 - Thm("sqrt_square_equation_right_1",num_str sqrt_square_equation_right_1),
15.247 + Thm("sqrt_square_equation_right_1",num_str @{sqrt_square_equation_right_1),
15.248 (* a=sqrt(x) ->a^2=x *)
15.249 - Thm("sqrt_square_equation_right_2",num_str sqrt_square_equation_right_2),
15.250 + Thm("sqrt_square_equation_right_2",num_str @{sqrt_square_equation_right_2),
15.251 (* a=c*sqrt(x) ->a^2=c^2*x *)
15.252 - Thm("sqrt_square_equation_right_3",num_str sqrt_square_equation_right_3),
15.253 + Thm("sqrt_square_equation_right_3",num_str @{sqrt_square_equation_right_3),
15.254 (* a=c/sqrt(x) ->a^2=c^2/x *)
15.255 - Thm("sqrt_square_equation_right_4",num_str sqrt_square_equation_right_4),
15.256 + Thm("sqrt_square_equation_right_4",num_str @{sqrt_square_equation_right_4),
15.257 (* a=c*d/sqrt(x) ->a^2=c^2*d^2/x *)
15.258 - Thm("sqrt_square_equation_right_5",num_str sqrt_square_equation_right_5),
15.259 + Thm("sqrt_square_equation_right_5",num_str @{sqrt_square_equation_right_5),
15.260 (* a=c/e*sqrt(x) ->a^2=c^2/e^2x *)
15.261 - Thm("sqrt_square_equation_right_6",num_str sqrt_square_equation_right_6)
15.262 + Thm("sqrt_square_equation_right_6",num_str @{sqrt_square_equation_right_6)
15.263 (* a=c*d/g*sqrt(x) ->a^2=c^2*d^2/g^2*x *)
15.264 ],
15.265 scr = Script ((term_of o the o (parse thy)) "empty_script")
15.266 @@ -439,9 +439,9 @@
15.267 preconds = [], rew_ord = ("termlessI",termlessI),
15.268 erls = RootEq_erls, srls = Erls, calc = [],
15.269 (*asm_thm = [("sqrt_square_1","")],*)
15.270 - rules = [Thm ("real_assoc_1",num_str real_assoc_1),
15.271 + rules = [Thm ("real_assoc_1",num_str @{real_assoc_1),
15.272 (* a+(b+c) = a+b+c *)
15.273 - Thm ("real_assoc_2",num_str real_assoc_2),
15.274 + Thm ("real_assoc_2",num_str @{real_assoc_2),
15.275 (* a*(b*c) = a*b*c *)
15.276 Calc ("op +",eval_binop "#add_"),
15.277 Calc ("op -",eval_binop "#sub_"),
15.278 @@ -449,17 +449,17 @@
15.279 Calc ("HOL.divide", eval_cancel "#divide_"),
15.280 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
15.281 Calc ("Atools.pow" ,eval_binop "#power_"),
15.282 - Thm("real_plus_binom_pow2",num_str real_plus_binom_pow2),
15.283 - Thm("real_minus_binom_pow2",num_str real_minus_binom_pow2),
15.284 - Thm("realpow_mul",num_str realpow_mul),
15.285 + Thm("real_plus_binom_pow2",num_str @{real_plus_binom_pow2),
15.286 + Thm("real_minus_binom_pow2",num_str @{real_minus_binom_pow2),
15.287 + Thm("realpow_mul",num_str @{realpow_mul),
15.288 (* (a * b)^n = a^n * b^n*)
15.289 - Thm("sqrt_times_root_1",num_str sqrt_times_root_1),
15.290 + Thm("sqrt_times_root_1",num_str @{sqrt_times_root_1),
15.291 (* sqrt b * sqrt c = sqrt(b*c) *)
15.292 - Thm("sqrt_times_root_2",num_str sqrt_times_root_2),
15.293 + Thm("sqrt_times_root_2",num_str @{sqrt_times_root_2),
15.294 (* a * sqrt a * sqrt b = a * sqrt(a*b) *)
15.295 - Thm("sqrt_square_2",num_str sqrt_square_2),
15.296 + Thm("sqrt_square_2",num_str @{sqrt_square_2),
15.297 (* sqrt (a^^^2) = a *)
15.298 - Thm("sqrt_square_1",num_str sqrt_square_1)
15.299 + Thm("sqrt_square_1",num_str @{sqrt_square_1)
15.300 (* sqrt a ^^^ 2 = a *)
15.301 ],
15.302 scr = Script ((term_of o the o (parse thy)) "empty_script")
16.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Tue Aug 31 15:36:57 2010 +0200
16.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Tue Aug 31 16:00:13 2010 +0200
16.3 @@ -27,7 +27,7 @@
16.4 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
16.5 Thm ("mult_1_left",num_str @{thm mult_1_left}),
16.6 (* 1 * z = z *)
16.7 - Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym)),
16.8 + Thm ("sym_real_mult_minus1",num_str @{(real_mult_minus1 RS sym)),
16.9 (* "- z1 = -1 * z1" *)
16.10 Calc ("Root.sqrt",eval_sqrt "#sqrt_")
16.11 ];
17.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Tue Aug 31 15:36:57 2010 +0200
17.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Tue Aug 31 16:00:13 2010 +0200
17.3 @@ -78,12 +78,12 @@
17.4 Calc ("RootRatEq.is'_rootRatAddTerm'_in",
17.5 eval_is_rootRatAddTerm_in ""),
17.6 Calc ("op =",eval_equal "#equal_"),
17.7 - Thm ("not_true",num_str not_true),
17.8 - Thm ("not_false",num_str not_false),
17.9 - Thm ("and_true",num_str and_true),
17.10 - Thm ("and_false",num_str and_false),
17.11 - Thm ("or_true",num_str or_true),
17.12 - Thm ("or_false",num_str or_false)
17.13 + Thm ("not_true",num_str @{not_true),
17.14 + Thm ("not_false",num_str @{not_false),
17.15 + Thm ("and_true",num_str @{and_true),
17.16 + Thm ("and_false",num_str @{and_false),
17.17 + Thm ("or_true",num_str @{or_true),
17.18 + Thm ("or_false",num_str @{or_false)
17.19 ];
17.20
17.21 val RooRatEq_erls =
17.22 @@ -108,15 +108,15 @@
17.23 Rls {id = "rootrat_solve", preconds = [],
17.24 rew_ord = ("termlessI",termlessI),
17.25 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
17.26 - rules = [Thm("rootrat_equation_left_1", num_str rootrat_equation_left_1),
17.27 + rules = [Thm("rootrat_equation_left_1", num_str @{rootrat_equation_left_1),
17.28 (* [|c is_rootTerm_in bdv|] ==>
17.29 ( (a + b/c = d) = ( b = (d - a) * c )) *)
17.30 - Thm("rootrat_equation_left_2",num_str rootrat_equation_left_2),
17.31 + Thm("rootrat_equation_left_2",num_str @{rootrat_equation_left_2),
17.32 (* [|c is_rootTerm_in bdv|] ==> ( (b/c = d) = ( b = d * c )) *)
17.33 - Thm("rootrat_equation_right_1",num_str rootrat_equation_right_1),
17.34 + Thm("rootrat_equation_right_1",num_str @{rootrat_equation_right_1),
17.35 (* [|f is_rootTerm_in bdv|] ==>
17.36 ( (a = d + e/f) = ( (a - d) * f = e )) *)
17.37 - Thm("rootrat_equation_right_2",num_str rootrat_equation_right_2)
17.38 + Thm("rootrat_equation_right_2",num_str @{rootrat_equation_right_2)
17.39 (* [|f is_rootTerm_in bdv|] ==> ( (a = e/f) = ( a * f = e ))*)
17.40 ],
17.41 scr = Script ((term_of o the o (parse thy)) "empty_script")
18.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Aug 31 15:36:57 2010 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Aug 31 16:00:13 2010 +0200
18.3 @@ -209,17 +209,17 @@
18.4 Rls {id = "testerls", preconds = [], rew_ord = ("termlessI",termlessI),
18.5 erls = e_rls, srls = Erls,
18.6 calc = [],
18.7 - rules = [Thm ("refl",num_str refl),
18.8 + rules = [Thm ("refl",num_str @{refl),
18.9 Thm ("real_le_refl",num_str @{thm real_le_refl}),
18.10 - Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
18.11 - Thm ("not_true",num_str not_true),
18.12 - Thm ("not_false",num_str not_false),
18.13 + Thm ("radd_left_cancel_le",num_str @{radd_left_cancel_le),
18.14 + Thm ("not_true",num_str @{not_true),
18.15 + Thm ("not_false",num_str @{not_false),
18.16 Thm ("and_true",and_true),
18.17 Thm ("and_false",and_false),
18.18 Thm ("or_true",or_true),
18.19 Thm ("or_false",or_false),
18.20 - Thm ("and_commute",num_str and_commute),
18.21 - Thm ("or_commute",num_str or_commute),
18.22 + Thm ("and_commute",num_str @{and_commute),
18.23 + Thm ("or_commute",num_str @{or_commute),
18.24
18.25 Calc ("Atools.is'_const",eval_const "#is_const_"),
18.26 Calc ("Tools.matches",eval_matches ""),
18.27 @@ -243,24 +243,24 @@
18.28 rew_ord = ("sqrt_right",sqrt_right false (theory "Pure")),
18.29 erls=testerls,srls = e_rls,
18.30 calc=[],
18.31 - rules = [Thm ("refl",num_str refl),
18.32 + rules = [Thm ("refl",num_str @{refl),
18.33 Thm ("real_le_refl",num_str @{thm real_le_refl}),
18.34 - Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
18.35 - Thm ("not_true",num_str not_true),
18.36 - Thm ("not_false",num_str not_false),
18.37 + Thm ("radd_left_cancel_le",num_str @{radd_left_cancel_le),
18.38 + Thm ("not_true",num_str @{not_true),
18.39 + Thm ("not_false",num_str @{not_false),
18.40 Thm ("and_true",and_true),
18.41 Thm ("and_false",and_false),
18.42 Thm ("or_true",or_true),
18.43 Thm ("or_false",or_false),
18.44 - Thm ("and_commute",num_str and_commute),
18.45 - Thm ("or_commute",num_str or_commute),
18.46 + Thm ("and_commute",num_str @{and_commute),
18.47 + Thm ("or_commute",num_str @{or_commute),
18.48
18.49 - Thm ("real_diff_minus",num_str real_diff_minus),
18.50 + Thm ("real_diff_minus",num_str @{real_diff_minus),
18.51
18.52 - Thm ("root_ge0",num_str root_ge0),
18.53 - Thm ("root_add_ge0",num_str root_add_ge0),
18.54 - Thm ("root_ge0_1",num_str root_ge0_1),
18.55 - Thm ("root_ge0_2",num_str root_ge0_2),
18.56 + Thm ("root_ge0",num_str @{root_ge0),
18.57 + Thm ("root_add_ge0",num_str @{root_add_ge0),
18.58 + Thm ("root_ge0_1",num_str @{root_ge0_1),
18.59 + Thm ("root_ge0_2",num_str @{root_ge0_2),
18.60
18.61 Calc ("Atools.is'_const",eval_const "#is_const_"),
18.62 Calc ("Test.is'_root'_free",eval_root_free "#is_root_free_"),
18.63 @@ -293,8 +293,8 @@
18.64 rew_ord = ("e_rew_ord",e_rew_ord),
18.65 erls = e_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
18.66 rules =
18.67 - [Thm ("sym_radd_assoc",num_str (radd_assoc RS sym)),
18.68 - Thm ("sym_rmult_assoc",num_str (rmult_assoc RS sym))],
18.69 + [Thm ("sym_radd_assoc",num_str @{(radd_assoc RS sym)),
18.70 + Thm ("sym_rmult_assoc",num_str @{(rmult_assoc RS sym))],
18.71 scr = Script ((term_of o the o (parse thy))
18.72 "empty_script")
18.73 }:rls;
18.74 @@ -313,11 +313,11 @@
18.75 "empty_script")
18.76 }:rls;
18.77
18.78 -(*todo: replace by Rewrite("rnorm_equation_add",num_str rnorm_equation_add)*)
18.79 +(*todo: replace by Rewrite("rnorm_equation_add",num_str @{rnorm_equation_add)*)
18.80 val norm_equation =
18.81 Rls{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
18.82 erls = tval_rls, srls = e_rls, calc = [], (*asm_thm=[],*)
18.83 - rules = [Thm ("rnorm_equation_add",num_str rnorm_equation_add)
18.84 + rules = [Thm ("rnorm_equation_add",num_str @{rnorm_equation_add)
18.85 ],
18.86 scr = Script ((term_of o the o (parse thy))
18.87 "empty_script")
18.88 @@ -381,22 +381,22 @@
18.89 calc=[(*since 040209 filled by prep_rls*)],
18.90 (*asm_thm = [],*)
18.91 rules = [
18.92 - Thm ("real_diff_minus",num_str real_diff_minus),
18.93 - Thm ("radd_mult_distrib2",num_str radd_mult_distrib2),
18.94 - Thm ("rdistr_right_assoc",num_str rdistr_right_assoc),
18.95 - Thm ("rdistr_right_assoc_p",num_str rdistr_right_assoc_p),
18.96 - Thm ("rdistr_div_right",num_str rdistr_div_right),
18.97 - Thm ("rbinom_power_2",num_str rbinom_power_2),
18.98 + Thm ("real_diff_minus",num_str @{real_diff_minus),
18.99 + Thm ("radd_mult_distrib2",num_str @{radd_mult_distrib2),
18.100 + Thm ("rdistr_right_assoc",num_str @{rdistr_right_assoc),
18.101 + Thm ("rdistr_right_assoc_p",num_str @{rdistr_right_assoc_p),
18.102 + Thm ("rdistr_div_right",num_str @{rdistr_div_right),
18.103 + Thm ("rbinom_power_2",num_str @{rbinom_power_2),
18.104
18.105 - Thm ("radd_commute",num_str radd_commute),
18.106 - Thm ("radd_left_commute",num_str radd_left_commute),
18.107 - Thm ("radd_assoc",num_str radd_assoc),
18.108 - Thm ("rmult_commute",num_str rmult_commute),
18.109 - Thm ("rmult_left_commute",num_str rmult_left_commute),
18.110 - Thm ("rmult_assoc",num_str rmult_assoc),
18.111 + Thm ("radd_commute",num_str @{radd_commute),
18.112 + Thm ("radd_left_commute",num_str @{radd_left_commute),
18.113 + Thm ("radd_assoc",num_str @{radd_assoc),
18.114 + Thm ("rmult_commute",num_str @{rmult_commute),
18.115 + Thm ("rmult_left_commute",num_str @{rmult_left_commute),
18.116 + Thm ("rmult_assoc",num_str @{rmult_assoc),
18.117
18.118 - Thm ("radd_real_const_eq",num_str radd_real_const_eq),
18.119 - Thm ("radd_real_const",num_str radd_real_const),
18.120 + Thm ("radd_real_const_eq",num_str @{radd_real_const_eq),
18.121 + Thm ("radd_real_const",num_str @{radd_real_const),
18.122 (* these 2 rules are invers to distr_div_right wrt. termination.
18.123 thus they MUST be done IMMEDIATELY before calc *)
18.124 Calc ("op +", eval_binop "#add_"),
18.125 @@ -404,27 +404,27 @@
18.126 Calc ("HOL.divide", eval_cancel "#divide_"),
18.127 Calc ("Atools.pow", eval_binop "#power_"),
18.128
18.129 - Thm ("rcollect_right",num_str rcollect_right),
18.130 - Thm ("rcollect_one_left",num_str rcollect_one_left),
18.131 - Thm ("rcollect_one_left_assoc",num_str rcollect_one_left_assoc),
18.132 - Thm ("rcollect_one_left_assoc_p",num_str rcollect_one_left_assoc_p),
18.133 + Thm ("rcollect_right",num_str @{rcollect_right),
18.134 + Thm ("rcollect_one_left",num_str @{rcollect_one_left),
18.135 + Thm ("rcollect_one_left_assoc",num_str @{rcollect_one_left_assoc),
18.136 + Thm ("rcollect_one_left_assoc_p",num_str @{rcollect_one_left_assoc_p),
18.137
18.138 - Thm ("rshift_nominator",num_str rshift_nominator),
18.139 - Thm ("rcancel_den",num_str rcancel_den),
18.140 - Thm ("rroot_square_inv",num_str rroot_square_inv),
18.141 - Thm ("rroot_times_root",num_str rroot_times_root),
18.142 - Thm ("rroot_times_root_assoc_p",num_str rroot_times_root_assoc_p),
18.143 - Thm ("rsqare",num_str rsqare),
18.144 - Thm ("power_1",num_str power_1),
18.145 - Thm ("rtwo_of_the_same",num_str rtwo_of_the_same),
18.146 - Thm ("rtwo_of_the_same_assoc_p",num_str rtwo_of_the_same_assoc_p),
18.147 + Thm ("rshift_nominator",num_str @{rshift_nominator),
18.148 + Thm ("rcancel_den",num_str @{rcancel_den),
18.149 + Thm ("rroot_square_inv",num_str @{rroot_square_inv),
18.150 + Thm ("rroot_times_root",num_str @{rroot_times_root),
18.151 + Thm ("rroot_times_root_assoc_p",num_str @{rroot_times_root_assoc_p),
18.152 + Thm ("rsqare",num_str @{rsqare),
18.153 + Thm ("power_1",num_str @{power_1),
18.154 + Thm ("rtwo_of_the_same",num_str @{rtwo_of_the_same),
18.155 + Thm ("rtwo_of_the_same_assoc_p",num_str @{rtwo_of_the_same_assoc_p),
18.156
18.157 - Thm ("rmult_1",num_str rmult_1),
18.158 - Thm ("rmult_1_right",num_str rmult_1_right),
18.159 - Thm ("rmult_0",num_str rmult_0),
18.160 - Thm ("rmult_0_right",num_str rmult_0_right),
18.161 - Thm ("radd_0",num_str radd_0),
18.162 - Thm ("radd_0_right",num_str radd_0_right)
18.163 + Thm ("rmult_1",num_str @{rmult_1),
18.164 + Thm ("rmult_1_right",num_str @{rmult_1_right),
18.165 + Thm ("rmult_0",num_str @{rmult_0),
18.166 + Thm ("rmult_0_right",num_str @{rmult_0_right),
18.167 + Thm ("radd_0",num_str @{radd_0),
18.168 + Thm ("radd_0_right",num_str @{radd_0_right)
18.169 ],
18.170 scr = Script ((term_of o the o (parse thy)) "empty_script")
18.171 (*since 040209 filled by prep_rls: STest_simplify*)
18.172 @@ -442,12 +442,12 @@
18.173 val isolate_root =
18.174 Rls{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
18.175 erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
18.176 - rules = [Thm ("rroot_to_lhs",num_str rroot_to_lhs),
18.177 - Thm ("rroot_to_lhs_mult",num_str rroot_to_lhs_mult),
18.178 - Thm ("rroot_to_lhs_add_mult",num_str rroot_to_lhs_add_mult),
18.179 - Thm ("risolate_root_add",num_str risolate_root_add),
18.180 - Thm ("risolate_root_mult",num_str risolate_root_mult),
18.181 - Thm ("risolate_root_div",num_str risolate_root_div) ],
18.182 + rules = [Thm ("rroot_to_lhs",num_str @{rroot_to_lhs),
18.183 + Thm ("rroot_to_lhs_mult",num_str @{rroot_to_lhs_mult),
18.184 + Thm ("rroot_to_lhs_add_mult",num_str @{rroot_to_lhs_add_mult),
18.185 + Thm ("risolate_root_add",num_str @{risolate_root_add),
18.186 + Thm ("risolate_root_mult",num_str @{risolate_root_mult),
18.187 + Thm ("risolate_root_div",num_str @{risolate_root_div) ],
18.188 scr = Script ((term_of o the o (parse thy))
18.189 "empty_script")
18.190 }:rls;
18.191 @@ -457,12 +457,12 @@
18.192 Rls{id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",e_rew_ord),
18.193 erls=tval_rls,srls = e_rls, calc=[],(*asm_thm = [], *)
18.194 rules =
18.195 - [Thm ("risolate_bdv_add",num_str risolate_bdv_add),
18.196 - Thm ("risolate_bdv_mult_add",num_str risolate_bdv_mult_add),
18.197 - Thm ("risolate_bdv_mult",num_str risolate_bdv_mult),
18.198 - Thm ("mult_square",num_str mult_square),
18.199 - Thm ("constant_square",num_str constant_square),
18.200 - Thm ("constant_mult_square",num_str constant_mult_square)
18.201 + [Thm ("risolate_bdv_add",num_str @{risolate_bdv_add),
18.202 + Thm ("risolate_bdv_mult_add",num_str @{risolate_bdv_mult_add),
18.203 + Thm ("risolate_bdv_mult",num_str @{risolate_bdv_mult),
18.204 + Thm ("mult_square",num_str @{mult_square),
18.205 + Thm ("constant_square",num_str @{constant_square),
18.206 + Thm ("constant_mult_square",num_str @{constant_mult_square)
18.207 ],
18.208 scr = Script ((term_of o the o (parse thy))
18.209 "empty_script")
18.210 @@ -1261,7 +1261,7 @@
18.211 ("POWER", ("Atools.pow", eval_binop "#power_"))
18.212 ],
18.213 (*asm_thm = [],*)
18.214 - rules = [Thm ("real_diff_minus",num_str real_diff_minus),
18.215 + rules = [Thm ("real_diff_minus",num_str @{real_diff_minus),
18.216 (*"a - b = a + (-1) * b"*)
18.217 Thm ("left_distrib" ,num_str @{thm left_distrib}),
18.218 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
18.219 @@ -1279,11 +1279,11 @@
18.220 (*"0 + z = z"*)
18.221
18.222 (*AC-rewriting*)
18.223 - Thm ("real_mult_commute",num_str real_mult_commute),
18.224 + Thm ("real_mult_commute",num_str @{real_mult_commute),
18.225 (* z * w = w * z *)
18.226 - Thm ("real_mult_left_commute",num_str real_mult_left_commute),
18.227 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute),
18.228 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
18.229 - Thm ("real_mult_assoc",num_str real_mult_assoc),
18.230 + Thm ("real_mult_assoc",num_str @{real_mult_assoc),
18.231 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
18.232 Thm ("add_commute",num_str @{thm add_commute}),
18.233 (*z + w = w + z*)
18.234 @@ -1292,23 +1292,23 @@
18.235 Thm ("add_assoc",num_str @{thm add_assoc}),
18.236 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
18.237
18.238 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
18.239 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
18.240 (*"r1 * r1 = r1 ^^^ 2"*)
18.241 - Thm ("realpow_plus_1",num_str realpow_plus_1),
18.242 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
18.243 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
18.244 - Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
18.245 + Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
18.246 (*"z1 + z1 = 2 * z1"*)
18.247 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
18.248 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
18.249 (*"z1 + (z1 + k) = 2 * z1 + k"*)
18.250
18.251 - Thm ("real_num_collect",num_str real_num_collect),
18.252 + Thm ("real_num_collect",num_str @{real_num_collect),
18.253 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
18.254 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
18.255 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
18.256 (*"[| l is_const; m is_const |] ==>
18.257 l * n + (m * n + k) = (l + m) * n + k"*)
18.258 - Thm ("real_one_collect",num_str real_one_collect),
18.259 + Thm ("real_one_collect",num_str @{real_one_collect),
18.260 (*"m is_const ==> n + m * n = (1 + m) * n"*)
18.261 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
18.262 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
18.263 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
18.264
18.265 Calc ("op +", eval_binop "#add_"),
18.266 @@ -1363,32 +1363,32 @@
18.267 ("POWER", ("Atools.pow", eval_binop "#power_"))
18.268 ],
18.269 (*asm_thm = [],*)
18.270 - rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2),
18.271 + rules = [Thm ("real_plus_binom_pow2" ,num_str @{real_plus_binom_pow2),
18.272 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
18.273 - Thm ("real_plus_binom_times" ,num_str real_plus_binom_times),
18.274 + Thm ("real_plus_binom_times" ,num_str @{real_plus_binom_times),
18.275 (*"(a + b)*(a + b) = ...*)
18.276 - Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2),
18.277 + Thm ("real_minus_binom_pow2" ,num_str @{real_minus_binom_pow2),
18.278 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
18.279 - Thm ("real_minus_binom_times",num_str real_minus_binom_times),
18.280 + Thm ("real_minus_binom_times",num_str @{real_minus_binom_times),
18.281 (*"(a - b)*(a - b) = ...*)
18.282 - Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1),
18.283 + Thm ("real_plus_minus_binom1",num_str @{real_plus_minus_binom1),
18.284 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
18.285 - Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2),
18.286 + Thm ("real_plus_minus_binom2",num_str @{real_plus_minus_binom2),
18.287 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
18.288 (*RL 020915*)
18.289 - Thm ("real_pp_binom_times",num_str real_pp_binom_times),
18.290 + Thm ("real_pp_binom_times",num_str @{real_pp_binom_times),
18.291 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
18.292 - Thm ("real_pm_binom_times",num_str real_pm_binom_times),
18.293 + Thm ("real_pm_binom_times",num_str @{real_pm_binom_times),
18.294 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
18.295 - Thm ("real_mp_binom_times",num_str real_mp_binom_times),
18.296 + Thm ("real_mp_binom_times",num_str @{real_mp_binom_times),
18.297 (*(a - b)*(c p d) = a*c + a*d - b*c - b*d*)
18.298 - Thm ("real_mm_binom_times",num_str real_mm_binom_times),
18.299 + Thm ("real_mm_binom_times",num_str @{real_mm_binom_times),
18.300 (*(a - b)*(c p d) = a*c - a*d - b*c + b*d*)
18.301 - Thm ("realpow_multI",num_str realpow_multI),
18.302 + Thm ("realpow_multI",num_str @{realpow_multI),
18.303 (*(a*b)^^^n = a^^^n * b^^^n*)
18.304 - Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3),
18.305 + Thm ("real_plus_binom_pow3",num_str @{real_plus_binom_pow3),
18.306 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
18.307 - Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3),
18.308 + Thm ("real_minus_binom_pow3",num_str @{real_minus_binom_pow3),
18.309 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
18.310
18.311
18.312 @@ -1410,30 +1410,30 @@
18.313 Calc ("op *", eval_binop "#mult_"),
18.314 Calc ("Atools.pow", eval_binop "#power_"),
18.315 (*
18.316 - Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
18.317 - Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
18.318 - Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
18.319 + Thm ("real_mult_commute",num_str @{real_mult_commute), (*AC-rewriting*)
18.320 + Thm ("real_mult_left_commute",num_str @{real_mult_left_commute), (**)
18.321 + Thm ("real_mult_assoc",num_str @{real_mult_assoc), (**)
18.322 Thm ("add_commute",num_str @{thm add_commute}), (**)
18.323 Thm ("add_left_commute",num_str @{thm add_left_commute}), (**)
18.324 Thm ("add_assoc",num_str @{thm add_assoc}), (**)
18.325 *)
18.326
18.327 - Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
18.328 + Thm ("sym_realpow_twoI",num_str @{(realpow_twoI RS sym)),
18.329 (*"r1 * r1 = r1 ^^^ 2"*)
18.330 - Thm ("realpow_plus_1",num_str realpow_plus_1),
18.331 + Thm ("realpow_plus_1",num_str @{realpow_plus_1),
18.332 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
18.333 - (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
18.334 + (*Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym)),
18.335 (*"z1 + z1 = 2 * z1"*)*)
18.336 - Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
18.337 + Thm ("real_mult_2_assoc",num_str @{real_mult_2_assoc),
18.338 (*"z1 + (z1 + k) = 2 * z1 + k"*)
18.339
18.340 - Thm ("real_num_collect",num_str real_num_collect),
18.341 + Thm ("real_num_collect",num_str @{real_num_collect),
18.342 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
18.343 - Thm ("real_num_collect_assoc",num_str real_num_collect_assoc),
18.344 + Thm ("real_num_collect_assoc",num_str @{real_num_collect_assoc),
18.345 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
18.346 - Thm ("real_one_collect",num_str real_one_collect),
18.347 + Thm ("real_one_collect",num_str @{real_one_collect),
18.348 (*"m is_const ==> n + m * n = (1 + m) * n"*)
18.349 - Thm ("real_one_collect_assoc",num_str real_one_collect_assoc),
18.350 + Thm ("real_one_collect_assoc",num_str @{real_one_collect_assoc),
18.351 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
18.352
18.353 Calc ("op +", eval_binop "#add_"),
19.1 --- a/src/Tools/isac/ProgLang/Language.thy Tue Aug 31 15:36:57 2010 +0200
19.2 +++ b/src/Tools/isac/ProgLang/Language.thy Tue Aug 31 16:00:13 2010 +0200
19.3 @@ -4,9 +4,9 @@
19.4 *)
19.5
19.6 theory Language imports Script
19.7 -uses ("scrtools.sml")
19.8 +uses ("../ProgLang/scrtools.sml")
19.9 begin
19.10
19.11 -use "scrtools.sml"
19.12 +use "../ProgLang/scrtools.sml"
19.13
19.14 end
19.15 \ No newline at end of file
20.1 --- a/src/Tools/isac/ProgLang/ListC.thy Tue Aug 31 15:36:57 2010 +0200
20.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Aug 31 16:00:13 2010 +0200
20.3 @@ -143,7 +143,7 @@
20.4 Rls{id="list_rls",preconds = [], rew_ord = ("dummy_ord",dummy_ord),
20.5 erls = e_rls, srls = Erls, calc = [], (*asm_thm=[],*)
20.6 rules = (*8.01: copied from*)
20.7 - [Thm ("refl", num_str refl), (*'a<>b -> FALSE' by fun eval_equal*)
20.8 + [Thm ("refl", num_str @{thm refl}), (*'a<>b -> FALSE' by fun eval_equal*)
20.9 Thm ("o_apply", num_str @{thm o_apply}),
20.10
20.11 Thm ("NTH_CONS",num_str @{thm NTH_CONS}),(*erls for cond. in Atools.ML*)
21.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Tue Aug 31 15:36:57 2010 +0200
21.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Tue Aug 31 16:00:13 2010 +0200
21.3 @@ -387,7 +387,7 @@
21.4 Try $ (Repeat $ (Ca1 $ Free (assoc_calc (calc ,c), IDtype)))
21.5 | rule2stac _ (Rls_ rls) =
21.6 Try $ (Rew_Set $ Free (id_rls rls, IDtype) $ HOLogic.false_const);
21.7 -(*val t = rule2stac [] (Thm ("real_diff_minus", num_str real_diff_minus));
21.8 +(*val t = rule2stac [] (Thm ("real_diff_minus", num_str @{real_diff_minus));
21.9 atomt t; term2str t;
21.10 val t = rule2stac calclist (Calc ("op +", eval_binop "#add_"));
21.11 atomt t; term2str t;
21.12 @@ -404,7 +404,7 @@
21.13 | rule2stac_inst _ (Rls_ rls) =
21.14 Try $ (Rew_Set_Inst $ Subs $ Free (id_rls rls, IDtype) $
21.15 HOLogic.false_const);
21.16 -(*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str real_diff_minus));
21.17 +(*val t = rule2stac_inst [] (Thm ("real_diff_minus", num_str @{real_diff_minus));
21.18 atomt t; term2str t;
21.19 val t = rule2stac_inst calclist (Calc ("op +", eval_binop "#add_"));
21.20 atomt t; term2str t;