1.1 --- a/src/Tools/isac/Build_Isac.thy Tue Aug 31 11:10:30 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Tue Aug 31 15:36:57 2010 +0200
1.3 @@ -27,8 +27,9 @@
1.4 use "ProgLang/term.sml"
1.5 use "ProgLang/calculate.sml"
1.6 use "ProgLang/rewrite.sml"
1.7 -use_thy"ProgLang/Script"
1.8 +use_thy"ProgLang/Script" (*ListC, Tools, Script*)
1.9 use "ProgLang/scrtools.sml"
1.10 +use_thy"ProgLang/Language"
1.11
1.12 use "Interpret/mstools.sml"
1.13 use "Interpret/ctree.sml"
1.14 @@ -56,13 +57,14 @@
1.15 ML {* writeln "**** build math-engine complete **************************" *}
1.16
1.17 ML {* writeln "**** build the Knowledge *********************************" *}
1.18 -(*use_thy "Knowledge/Typefix" FIXXXMEWN100827*)
1.19 +(*use_thy "Knowledge/Typefix"*)
1.20 +use_thy "Knowledge/Delete"
1.21 use_thy "Knowledge/Descript"
1.22 -
1.23 -(*
1.24 use_thy "Knowledge/Atools"
1.25
1.26
1.27 +text {*------------------------------------------*}
1.28 +(*
1.29 use_thy "Knowledge/Simplify"
1.30 use_thy "Knowledge/Poly"
1.31 use_thy "Knowledge/Rational"
2.1 --- a/src/Tools/isac/Knowledge/Atools.thy Tue Aug 31 11:10:30 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Tue Aug 31 15:36:57 2010 +0200
2.3 @@ -44,34 +44,33 @@
2.4
2.5 axioms (*for evaluating the assumptions of conditional rules*)
2.6
2.7 - last_thmI "lastI (x#xs) = (if xs =!= [] then x else lastI xs)"
2.8 - real_unari_minus "- a = (-1) * a" (*Isa!*)
2.9 + last_thmI: "lastI (x#xs) = (if xs =!= [] then x else lastI xs)"
2.10 + real_unari_minus: "- a = (-1) * a"
2.11
2.12 - rle_refl "(n::real) <= n"
2.13 -(*reflI "(t = t) = True"*)
2.14 - radd_left_cancel_le "((k::real) + m <= k + n) = (m <= n)"
2.15 - not_true "(~ True) = False"
2.16 - not_false "(~ False) = True"
2.17 - and_true "(a & True) = a"
2.18 - and_false "(a & False) = False"
2.19 - or_true "(a | True) = True"
2.20 - or_false "(a | False) = a"
2.21 - and_commute "(a & b) = (b & a)"
2.22 - or_commute "(a | b) = (b | a)"
2.23 + rle_refl: "(n::real) <= n"
2.24 + radd_left_cancel_le:"((k::real) + m <= k + n) = (m <= n)"
2.25 + not_true: "(~ True) = False"
2.26 + not_false: "(~ False) = True"
2.27 + and_true: "(a & True) = a"
2.28 + and_false: "(a & False) = False"
2.29 + or_true: "(a | True) = True"
2.30 + or_false: "(a | False) = a"
2.31 + and_commute: "(a & b) = (b & a)"
2.32 + or_commute: "(a | b) = (b | a)"
2.33
2.34 (*.should be in Rational.thy, but:
2.35 needed for asms in e.g. d2_pqformula1 in PolyEq.ML, RootEq.ML.*)
2.36 - rat_leq1 "[| b ~= 0; d ~= 0 |] ==>
2.37 + rat_leq1: "[| b ~= 0; d ~= 0 |] ==>
2.38 ((a / b) <= (c / d)) = ((a*d) <= (b*c))"(*Isa?*)
2.39 - rat_leq2 "d ~= 0 ==>
2.40 + rat_leq2: "d ~= 0 ==>
2.41 ( a <= (c / d)) = ((a*d) <= c )"(*Isa?*)
2.42 - rat_leq3 "b ~= 0 ==>
2.43 + rat_leq3: "b ~= 0 ==>
2.44 ((a / b) <= c ) = ( a <= (b*c))"(*Isa?*)
2.45
2.46 +
2.47 text {*copy from doc/math-eng.tex WN.28.3.03
2.48 WN071228 extended *}
2.49
2.50 -
2.51 section {*Coding standards*}
2.52 subsection {*Identifiers*}
2.53 text {*Naming is particularily crucial, because Isabelles name space is global, and isac does not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc. However, all the cases (1)..(4) require different typing for one and the same identifier {\tt probe} which is impossible, and actually leads to strange errors (for instance (1) is used as string, except in a script addressing a Subproblem).
2.54 @@ -518,8 +517,8 @@
2.55 open Term;
2.56
2.57 in
2.58 -fun termlessI (_:subst) uv = termless uv;
2.59 -fun term_ordI (_:subst) uv = term_ord uv;
2.60 +fun termlessI (_:subst) uv = Term_Ord.termless uv;
2.61 +fun term_ordI (_:subst) uv = Term_Ord.term_ord uv;
2.62 end;
2.63
2.64
2.65 @@ -537,11 +536,11 @@
2.66
2.67 Calc ("Tools.Vars",eval_var "#Vars_"),
2.68
2.69 - Thm ("if_True",num_str @{thm HOL.if_True}),
2.70 - Thm ("if_False",num_str @{thm HOL.if_False})
2.71 + Thm ("if_True",num_str @{thm if_True}),
2.72 + Thm ("if_False",num_str @{thm if_False})
2.73 ];
2.74
2.75 -ruleset' := overwritelthy thy (!ruleset',
2.76 +ruleset' := overwritelthy @{theory} (!ruleset',
2.77 [("list_rls",list_rls)
2.78 ]);
2.79
2.80 @@ -558,7 +557,7 @@
2.81 Calc ("op <=",eval_equ "#less_equal_"),
2.82 Calc ("op =",eval_equal "#equal_"),
2.83
2.84 - Thm ("real_unari_minus",num_str real_unari_minus),
2.85 + Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
2.86 Calc ("op +",eval_binop "#add_"),
2.87 Calc ("op -",eval_binop "#sub_"),
2.88 Calc ("op *",eval_binop "#mult_")
2.89 @@ -567,25 +566,25 @@
2.90 val Atools_erls =
2.91 append_rls "Atools_erls" e_rls
2.92 [Calc ("op =",eval_equal "#equal_"),
2.93 - Thm ("not_true",num_str not_true),
2.94 + Thm ("not_true",num_str @{thm not_true}),
2.95 (*"(~ True) = False"*)
2.96 - Thm ("not_false",num_str not_false),
2.97 + Thm ("not_false",num_str @{thm not_false}),
2.98 (*"(~ False) = True"*)
2.99 - Thm ("and_true",and_true),
2.100 + Thm ("and_true",num_str @{thm and_true}),
2.101 (*"(?a & True) = ?a"*)
2.102 - Thm ("and_false",and_false),
2.103 + Thm ("and_false",num_str @{thm and_false}),
2.104 (*"(?a & False) = False"*)
2.105 - Thm ("or_true",or_true),
2.106 + Thm ("or_true",num_str @{thm or_true}),
2.107 (*"(?a | True) = True"*)
2.108 - Thm ("or_false",or_false),
2.109 + Thm ("or_false",num_str @{thm or_false}),
2.110 (*"(?a | False) = ?a"*)
2.111
2.112 - Thm ("rat_leq1",rat_leq1),
2.113 - Thm ("rat_leq2",rat_leq2),
2.114 - Thm ("rat_leq3",rat_leq3),
2.115 - Thm ("refl",num_str refl),
2.116 - Thm ("le_refl",num_str le_refl),
2.117 - Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
2.118 + Thm ("rat_leq1",num_str @{thm rat_leq1}),
2.119 + Thm ("rat_leq2",num_str @{thm rat_leq2}),
2.120 + Thm ("rat_leq3",num_str @{thm rat_leq3}),
2.121 + Thm ("refl",num_str @{thm refl}),
2.122 + Thm ("real_le_refl",num_str @{thm real_le_refl}),
2.123 + Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
2.124
2.125 Calc ("op <",eval_equ "#less_"),
2.126 Calc ("op <=",eval_equ "#less_equal_"),
2.127 @@ -599,19 +598,19 @@
2.128 val Atools_crls =
2.129 append_rls "Atools_crls" e_rls
2.130 [Calc ("op =",eval_equal "#equal_"),
2.131 - Thm ("not_true",num_str not_true),
2.132 - Thm ("not_false",num_str not_false),
2.133 - Thm ("and_true",and_true),
2.134 - Thm ("and_false",and_false),
2.135 - Thm ("or_true",or_true),
2.136 - Thm ("or_false",or_false),
2.137 + Thm ("not_true",num_str @{thm not_true}),
2.138 + Thm ("not_false",num_str @{thm not_false}),
2.139 + Thm ("and_true",num_str @{thm and_true}),
2.140 + Thm ("and_false",num_str @{thm and_false}),
2.141 + Thm ("or_true",num_str @{thm or_true}),
2.142 + Thm ("or_false",num_str @{thm or_false}),
2.143
2.144 - Thm ("rat_leq1",rat_leq1),
2.145 - Thm ("rat_leq2",rat_leq2),
2.146 - Thm ("rat_leq3",rat_leq3),
2.147 - Thm ("refl",num_str refl),
2.148 - Thm ("le_refl",num_str le_refl),
2.149 - Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
2.150 + Thm ("rat_leq1",num_str @{thm rat_leq1}),
2.151 + Thm ("rat_leq2",num_str @{thm rat_leq2}),
2.152 + Thm ("rat_leq3",num_str @{thm rat_leq3}),
2.153 + Thm ("refl",num_str @{thm refl}),
2.154 + Thm ("real_le_refl",num_str @{thm real_le_refl}),
2.155 + Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
2.156
2.157 Calc ("op <",eval_equ "#less_"),
2.158 Calc ("op <=",eval_equ "#less_equal_"),
2.159 @@ -635,17 +634,17 @@
2.160 (* val atools_erls = prep_rls(
2.161 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI),
2.162 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
2.163 - rules = [Thm ("refl",num_str refl),
2.164 - Thm ("le_refl",num_str le_refl),
2.165 - Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
2.166 - Thm ("not_true",num_str not_true),
2.167 - Thm ("not_false",num_str not_false),
2.168 - Thm ("and_true",and_true),
2.169 - Thm ("and_false",and_false),
2.170 - Thm ("or_true",or_true),
2.171 - Thm ("or_false",or_false),
2.172 - Thm ("and_commute",num_str and_commute),
2.173 - Thm ("or_commute",num_str or_commute),
2.174 + rules = [Thm ("refl",num_str @{thm refl}),
2.175 + Thm ("real_le_refl",num_str @{thm real_le_refl}),
2.176 + Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
2.177 + Thm ("not_true",num_str @{thm not_true}),
2.178 + Thm ("not_false",num_str @{thm not_false}),
2.179 + Thm ("and_true",num_str @{thm and_true}),
2.180 + Thm ("and_false",num_str @{thm and_false}),
2.181 + Thm ("or_true",num_str @{thm or_true}),
2.182 + Thm ("or_false",num_str @{thm or_false}),
2.183 + Thm ("and_commute",num_str @{thm and_commute}),
2.184 + Thm ("or_commute",num_str @{thm or_commute}),
2.185
2.186 Calc ("op <",eval_equ "#less_"),
2.187 Calc ("op <=",eval_equ "#less_equal_"),
2.188 @@ -701,7 +700,7 @@
2.189 srls = Erls, calc = [], (*asm_thm = [], *)
2.190 rules = [], scr = EmptyScr})
2.191 list_rls);
2.192 -ruleset' := overwritelthy thy (!ruleset', [("list_rls", list_rls)]);
2.193 +ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]);
2.194 *}
2.195
2.196 end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Tools/isac/Knowledge/Delete.thy Tue Aug 31 15:36:57 2010 +0200
3.3 @@ -0,0 +1,102 @@
3.4 +(* Title: quick and dirty for quick update Isabelle2002 --> Isabelle2009-2
3.5 + Author: Walther Neuper 000301
3.6 + (c) due to copyright terms
3.7 +*)
3.8 +
3.9 +theory Delete imports "../ProgLang/Language" begin
3.10 +
3.11 +axioms (* theorems which are available only with long names,
3.12 + which can not yet be handled in isac's scripts *)
3.13 +
3.14 + real_mult_left_commute "z1 * (z2 * z3) = z2 * (z1 * z3)"
3.15 + (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*)
3.16 +
3.17 +
3.18 +ML {*
3.19 +(* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var:
3.20 + Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *)
3.21 +
3.22 +(*.used for calculating built in binary operations in Isabelle2002.
3.23 + integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*)
3.24 +fun calc "op +" ((a, b), _:int * int) ((c, d), _:int * int) = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*)
3.25 + if b < d
3.26 + then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
3.27 + else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
3.28 + | calc "op -" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
3.29 + ((a - c,0),(0,0))
3.30 + | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
3.31 + ((a * c, b + d), (0, 0))
3.32 + | calc "HOL.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
3.33 + ((a div c, 0), (0, 0))
3.34 + | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
3.35 + ((power a c, 0), (0, 0))
3.36 + | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
3.37 + raise error ("calc: not impl. for Float (("^
3.38 + (string_of_int a )^","^(string_of_int b )^"), ("^
3.39 + (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
3.40 + (string_of_int c )^","^(string_of_int d )^"), ("^
3.41 + (string_of_int p21)^","^(string_of_int p22)^"))");
3.42 +(*> calc "op +" ((~1,0),(0,0)) ((2,0),(0,0));
3.43 +val it = ((1,0),(0,0))*)
3.44 +
3.45 +(*.convert internal floatingpoint prepresentation to int and float.*)
3.46 +fun term_of_float T ((val1, 0), ( 0, 0)) =
3.47 + term_of_num T val1
3.48 + | term_of_float T ((val1, val2), (precision1, precision2)) =
3.49 + let val pT = pairT T T
3.50 + in Const ("Float.Float", (pairT pT pT) --> T)
3.51 + $ (pairt (pairt (Free (str_of_int val1, T))
3.52 + (Free (str_of_int val2, T)))
3.53 + (pairt (Free (str_of_int precision1, T))
3.54 + (Free (str_of_int precision2, T))))
3.55 + end;
3.56 +(*> val t = str2term "Float ((1,2),(0,0))";
3.57 +> val Const ("Float.Float", fT) $ _ = t;
3.58 +> atomtyp fT;
3.59 +> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT)
3.60 +> (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
3.61 +> atomtyp ffT;
3.62 +> fT = ffT;
3.63 +val it = true : bool
3.64 +
3.65 +t = float_term_of_num HOLogic.realT ((1,2),(0,0));
3.66 +val it = true : bool*)
3.67 +
3.68 +(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
3.69 +fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
3.70 + var_op_num v op_ optype ntyp v1
3.71 + | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
3.72 + let val pT = pairT T T
3.73 + in Const (op_, optype) $ v $
3.74 + (Const ("Float.Float", (pairT pT pT) --> T)
3.75 + $ (pairt (pairt (Free (str_of_int v1, T))
3.76 + (Free (str_of_int v2, T)))
3.77 + (pairt (Free (str_of_int p1, T))
3.78 + (Free (str_of_int p2, T)))))
3.79 + end;
3.80 +(*> val t = str2term "a + b";
3.81 +> val Const ("op +", optype) $ _ $ _ = t;
3.82 +> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
3.83 +> t = var_op_float v "op +" optype HOLogic.realT ((11,~1),(0,0));
3.84 +val it = true : bool*)
3.85 +
3.86 +(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
3.87 +fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
3.88 + num_op_var v op_ optype ntyp v1
3.89 + | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
3.90 + let val pT = pairT T T
3.91 + in Const (op_,optype) $
3.92 + (Const ("Float.Float", (pairT pT pT) --> T)
3.93 + $ (pairt (pairt (Free (str_of_int v1, T))
3.94 + (Free (str_of_int v2, T)))
3.95 + (pairt (Free (str_of_int p1, T))
3.96 + (Free (str_of_int p2, T))))) $ v
3.97 + end;
3.98 +(*> val t = str2term "a + b";
3.99 +> val Const ("op +", optype) $ _ $ _ = t;
3.100 +> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
3.101 +> t = float_op_var v "op +" optype HOLogic.realT ((11,~1),(0,0));
3.102 +val it = true : bool*)
3.103 +*}
3.104 +
3.105 +end
3.106 \ No newline at end of file
4.1 --- a/src/Tools/isac/Knowledge/Descript.thy Tue Aug 31 11:10:30 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Descript.thy Tue Aug 31 15:36:57 2010 +0200
4.3 @@ -5,7 +5,7 @@
4.4 + see WN, Reactive User-Guidance ... Vers. Oct.2000 p.48 ff
4.5 *)
4.6
4.7 -theory Descript imports "../ProgLang/Script" begin
4.8 +theory Descript imports Delete begin
4.9
4.10 consts
4.11
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue Aug 31 11:10:30 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Aug 31 15:36:57 2010 +0200
5.3 @@ -132,9 +132,9 @@
5.4 Calc ("op *", eval_binop "#mult_"),
5.5 Thm ("rat_mult",num_str rat_mult),
5.6 (*a / b * (c / d) = a * c / (b * d)*)
5.7 - Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
5.8 + Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
5.9 (*?x * (?y / ?z) = ?x * ?y / ?z*)
5.10 - Thm ("real_times_divide2_eq",num_str real_times_divide2_eq)
5.11 + Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left})
5.12 (*?y / ?z * ?x = ?y * ?x / ?z*)
5.13 (*
5.14 Thm ("", num_str ),*)
5.15 @@ -158,9 +158,9 @@
5.16 (*- ?z = "-1 * ?z"*)
5.17 Thm ("rat_mult",num_str rat_mult),
5.18 (*a / b * (c / d) = a * c / (b * d)*)
5.19 - Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
5.20 + Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
5.21 (*?x * (?y / ?z) = ?x * ?y / ?z*)
5.22 - Thm ("real_times_divide2_eq",num_str real_times_divide2_eq),
5.23 + Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
5.24 (*?y / ?z * ?x = ?y * ?x / ?z*)
5.25 Calc ("op *", eval_binop "#mult_")
5.26 ],
6.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Tue Aug 31 11:10:30 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Aug 31 15:36:57 2010 +0200
6.3 @@ -52,7 +52,7 @@
6.4 Rls {id="eval_rls",preconds = [], rew_ord = ("termlessI",termlessI),
6.5 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
6.6 rules = [Thm ("refl",num_str refl),
6.7 - Thm ("le_refl",num_str le_refl),
6.8 + Thm ("real_le_refl",num_str @{thm real_le_refl}),
6.9 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
6.10 Thm ("not_true",num_str not_true),
6.11 Thm ("not_false",num_str not_false),
7.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Aug 31 11:10:30 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Aug 31 15:36:57 2010 +0200
7.3 @@ -192,11 +192,11 @@
7.4 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
7.5 Thm ("real_mult_assoc",num_str real_mult_assoc),
7.6 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
7.7 - Thm ("real_add_commute",num_str real_add_commute),
7.8 + Thm ("add_commute",num_str @{thm add_commute}),
7.9 (*z + w = w + z*)
7.10 - Thm ("real_add_left_commute",num_str real_add_left_commute),
7.11 + Thm ("add_left_commute",num_str @{thm add_left_commute}),
7.12 (*x + (y + z) = y + (x + z)*)
7.13 - Thm ("real_add_assoc",num_str real_add_assoc)
7.14 + Thm ("add_assoc",num_str @{thm add_assoc})
7.15 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
7.16 ],
7.17 scr = EmptyScr}:rls;
7.18 @@ -256,9 +256,9 @@
7.19 Seq {id = "simplify_System_parenthesized", preconds = []:term list,
7.20 rew_ord = ("dummy_ord", dummy_ord),
7.21 erls = Atools_erls, srls = Erls, calc = [],
7.22 - rules = [Thm ("real_add_mult_distrib",num_str real_add_mult_distrib),
7.23 + rules = [Thm ("left_distrib",num_str @{thm left_distrib}),
7.24 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
7.25 - Thm ("real_add_divide_distrib",num_str real_add_divide_distrib),
7.26 + Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}),
7.27 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
7.28 (*^^^^^ *0* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
7.29 Rls_ norm_Rational_noadd_fractions(**2**),
8.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Tue Aug 31 11:10:30 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Tue Aug 31 15:36:57 2010 +0200
8.3 @@ -187,9 +187,9 @@
8.4
8.5 Thm ("real_divide_divide1_mg", real_divide_divide1_mg),
8.6 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
8.7 - Thm ("real_divide_divide1_eq", real_divide_divide1_eq),
8.8 + Thm ("divide_divide_eq_right", real_divide_divide1_eq),
8.9 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
8.10 - Thm ("real_divide_divide2_eq", real_divide_divide2_eq),
8.11 + Thm ("divide_divide_eq_left", real_divide_divide2_eq),
8.12 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
8.13 Calc ("HOL.divide" ,eval_cancel "#divide_"),
8.14
8.15 @@ -236,8 +236,8 @@
8.16 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
8.17 Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
8.18 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
8.19 - *****Thm ("real_add_divide_distrib",
8.20 - *****num_str real_add_divide_distrib)
8.21 + *****Thm ("nadd_divide_distrib",
8.22 + *****num_str @{thm nadd_divide_distrib})
8.23 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)----------*)
8.24 ];
8.25 val simplify_Integral =
8.26 @@ -245,9 +245,9 @@
8.27 rew_ord = ("dummy_ord", dummy_ord),
8.28 erls = Atools_erls, srls = Erls,
8.29 calc = [], (*asm_thm = [],*)
8.30 - rules = [Thm ("real_add_mult_distrib",num_str real_add_mult_distrib),
8.31 + rules = [Thm ("left_distrib",num_str @{thm left_distrib}),
8.32 (*"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"*)
8.33 - Thm ("real_add_divide_distrib",num_str real_add_divide_distrib),
8.34 + Thm ("nadd_divide_distrib",num_str @{thm nadd_divide_distrib}),
8.35 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)
8.36 (*^^^^^ *1* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
8.37 Rls_ norm_Rational_noadd_fractions,
8.38 @@ -289,8 +289,8 @@
8.39 * (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
8.40 * Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)(*,
8.41 * (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
8.42 -* Thm ("real_add_divide_distrib",
8.43 -* num_str real_add_divide_distrib)
8.44 +* Thm ("nadd_divide_distrib",
8.45 +* num_str @{thm nadd_divide_distrib})
8.46 * (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"*)*)
8.47 * ]),
8.48 * Calc ("HOL.divide" ,eval_cancel "#divide_")
9.1 --- a/src/Tools/isac/Knowledge/Isac.thy Tue Aug 31 11:10:30 2010 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Isac.thy Tue Aug 31 15:36:57 2010 +0200
9.3 @@ -27,7 +27,7 @@
9.4 (map (thms_of_rls o #2 o #2))) (!ruleset');
9.5 val isacthms = (flat o (map (PureThy.all_thms_of o #2)))
9.6 (*WN100827 TODOOOOO*)(!theory');
9.7 -in
9.8 +in (*TODO.WN1008 filter_out "sym_..." *)
9.9 val rlsthmsNOTisac = gen_diff eq_thmI (isacrlsthms, isacthms);
9.10 end;
9.11
10.1 --- a/src/Tools/isac/Knowledge/Poly.thy Tue Aug 31 11:10:30 2010 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Tue Aug 31 15:36:57 2010 +0200
10.3 @@ -489,9 +489,9 @@
10.4 erls = e_rls,srls = Erls,
10.5 calc = [],
10.6 (*asm_thm = [],*)
10.7 - rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
10.8 + rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
10.9 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
10.10 - Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2)
10.11 + Thm ("left_distrib2",num_str @{thm left_distrib}2)
10.12 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
10.13 ], scr = EmptyScr}:rls;
10.14
10.15 @@ -536,9 +536,9 @@
10.16 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
10.17 (*WN071229 changed/removed for Schaerding -----^^^*)
10.18
10.19 - Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
10.20 + Thm ("left_distrib" ,num_str @{thm left_distrib}),
10.21 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
10.22 - Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
10.23 + Thm ("left_distrib2",num_str @{thm left_distrib}2),
10.24 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
10.25
10.26 Thm ("realpow_multI", num_str realpow_multI),
10.27 @@ -601,9 +601,9 @@
10.28 Thm ("real_plus_minus_binom2_p_p",num_str real_plus_minus_binom2_p_p),
10.29 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
10.30
10.31 - Thm ("real_add_mult_distrib_poly" ,num_str real_add_mult_distrib_poly),
10.32 + Thm ("left_distrib_poly" ,num_str @{thm left_distrib}_poly),
10.33 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
10.34 - Thm("real_add_mult_distrib2_poly",num_str real_add_mult_distrib2_poly),
10.35 + Thm("left_distrib2_poly",num_str @{thm left_distrib}2_poly),
10.36 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
10.37
10.38 Thm ("realpow_multI_poly", num_str realpow_multI_poly),
10.39 @@ -666,7 +666,7 @@
10.40 calc = [],
10.41 (*asm_thm = [],*)
10.42 rules = [(* MG: folgende Thm müssen hier stehen bleiben: *)
10.43 - Thm ("real_mult_1_right",num_str real_mult_1_right),
10.44 + Thm ("mult_1_right",num_str @{thm mult_1_right}),
10.45 (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
10.46 Thm ("realpow_zeroI",num_str realpow_zeroI),
10.47 (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
10.48 @@ -709,20 +709,20 @@
10.49 erls = e_rls,srls = Erls,
10.50 calc = [],
10.51 (*asm_thm = [],*)
10.52 - rules = [Thm ("real_mult_1",num_str real_mult_1),
10.53 + rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
10.54 (*"1 * z = z"*)
10.55 - Thm ("real_mult_0",num_str real_mult_0),
10.56 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
10.57 (*"0 * z = 0"*)
10.58 - Thm ("real_mult_0_right",num_str real_mult_0_right),
10.59 + Thm ("mult_zero_left_right",num_str @{thm mult_zero_left}_right),
10.60 (*"z * 0 = 0"*)
10.61 - Thm ("real_add_zero_left",num_str real_add_zero_left),
10.62 + Thm ("add_0_left",num_str @{thm add_0_left}),
10.63 (*"0 + z = z"*)
10.64 - Thm ("real_add_zero_right",num_str real_add_zero_right),
10.65 + Thm ("add_0_right",num_str @{thm add_0_right}),
10.66 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
10.67
10.68 (*Thm ("realpow_oneI",num_str realpow_oneI)*)
10.69 (*"?r ^^^ 1 = ?r"*)
10.70 - Thm ("real_0_divide",num_str real_0_divide)(*WN060914*)
10.71 + Thm ("divide_zero_left",num_str @{thm divide_zero_left})(*WN060914*)
10.72 (*"0 / ?x = 0"*)
10.73 ], scr = EmptyScr}:rls;
10.74
10.75 @@ -772,11 +772,11 @@
10.76 erls = e_rls,srls = Erls,
10.77 calc = [],
10.78 (*asm_thm = [],*)
10.79 - rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
10.80 + rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
10.81 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
10.82 - Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
10.83 + Thm ("left_distrib2",num_str @{thm left_distrib}2),
10.84 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
10.85 - (*Thm ("real_add_mult_distrib1",num_str real_add_mult_distrib1),
10.86 + (*Thm ("left_distrib1",num_str @{thm left_distrib}1),
10.87 ....... 18.3.03 undefined???*)
10.88
10.89 Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),
10.90 @@ -790,7 +790,7 @@
10.91 num_str real_plus_minus_binom2_p),
10.92 (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
10.93
10.94 - Thm ("real_minus_minus",num_str real_minus_minus),
10.95 + Thm ("minus_minus",num_str @{thm minus_minus}),
10.96 (*"- (- ?z) = ?z"*)
10.97 Thm ("real_diff_minus",num_str real_diff_minus),
10.98 (*"a - b = a + -1 * b"*)
10.99 @@ -843,11 +843,11 @@
10.100 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
10.101 Thm ("real_mult_assoc",num_str real_mult_assoc),
10.102 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
10.103 - Thm ("real_add_commute",num_str real_add_commute),
10.104 + Thm ("add_commute",num_str @{thm add_commute}),
10.105 (*z + w = w + z*)
10.106 - Thm ("real_add_left_commute",num_str real_add_left_commute),
10.107 + Thm ("add_left_commute",num_str @{thm add_left_commute}),
10.108 (*x + (y + z) = y + (x + z)*)
10.109 - Thm ("real_add_assoc",num_str real_add_assoc)
10.110 + Thm ("add_assoc",num_str @{thm add_assoc})
10.111 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
10.112 ], scr = EmptyScr}:rls;
10.113 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
10.114 @@ -893,20 +893,20 @@
10.115 erls = e_rls,srls = Erls,
10.116 calc = [],
10.117 (*asm_thm = [],*)
10.118 - rules = [Thm ("real_mult_1",num_str real_mult_1),
10.119 + rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
10.120 (*"1 * z = z"*)
10.121 (*Thm ("real_mult_minus1",num_str real_mult_minus1),14.3.03*)
10.122 (*"-1 * z = - z"*)
10.123 - Thm ("sym_real_mult_minus_eq1",
10.124 + Thm ("minus_mult_left",
10.125 num_str (real_mult_minus_eq1 RS sym)),
10.126 (*- (?x * ?y) = "- ?x * ?y"*)
10.127 (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel),
10.128 (*"- ?x * - ?y = ?x * ?y"*)---*)
10.129 - Thm ("real_mult_0",num_str real_mult_0),
10.130 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
10.131 (*"0 * z = 0"*)
10.132 - Thm ("real_add_zero_left",num_str real_add_zero_left),
10.133 + Thm ("add_0_left",num_str @{thm add_0_left}),
10.134 (*"0 + z = z"*)
10.135 - Thm ("real_add_minus",num_str real_add_minus),
10.136 + Thm ("right_minus",num_str @{thm right_minus}),
10.137 (*"?z + - ?z = 0"*)
10.138 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
10.139 (*"z1 + z1 = 2 * z1"*)
10.140 @@ -1044,19 +1044,19 @@
10.141 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
10.142
10.143
10.144 - (* Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
10.145 + (* Thm ("left_distrib" ,num_str @{thm left_distrib}),
10.146 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
10.147 - Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
10.148 + Thm ("left_distrib2",num_str @{thm left_distrib}2),
10.149 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
10.150 - Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
10.151 + Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
10.152 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
10.153 - Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
10.154 + Thm ("left_diff_distrib2",num_str @{thm left_diff_distrib}2),
10.155 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
10.156 *)
10.157
10.158 - Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
10.159 - Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
10.160 - Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*)
10.161 + Thm ("mult_1_left",num_str @{thm mult_1_left}), (*"1 * z = z"*)
10.162 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}), (*"0 * z = 0"*)
10.163 + Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
10.164
10.165 Calc ("op +", eval_binop "#add_"),
10.166 Calc ("op *", eval_binop "#mult_"),
10.167 @@ -1065,9 +1065,9 @@
10.168 Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
10.169 Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
10.170 Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
10.171 - Thm ("real_add_commute",num_str real_add_commute), (**)
10.172 - Thm ("real_add_left_commute",num_str real_add_left_commute), (**)
10.173 - Thm ("real_add_assoc",num_str real_add_assoc), (**)
10.174 + Thm ("add_commute",num_str @{thm add_commute}), (**)
10.175 + Thm ("add_left_commute",num_str @{thm add_left_commute}), (**)
10.176 + Thm ("add_assoc",num_str @{thm add_assoc}), (**)
10.177 *)
10.178
10.179 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
10.180 @@ -1482,11 +1482,11 @@
10.181 Thm ("real_plus_binom_times2" ,num_str real_plus_binom_times2),
10.182 (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
10.183
10.184 - Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*)
10.185 + Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
10.186
10.187 - Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
10.188 + Thm ("left_distrib" ,num_str @{thm left_distrib}),
10.189 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
10.190 - Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
10.191 + Thm ("left_distrib2",num_str @{thm left_distrib}2),
10.192 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
10.193
10.194 Thm ("real_mult_assoc", num_str real_mult_assoc),
10.195 @@ -1522,9 +1522,9 @@
10.196 Calc ("op *", eval_binop "#mult_"),
10.197 Calc ("Atools.pow", eval_binop "#power_"),
10.198
10.199 - Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*)
10.200 - Thm ("real_mult_0",num_str real_mult_0),(*"0 * z = 0"*)
10.201 - Thm ("real_add_zero_left",num_str real_add_zero_left)(*0 + z = z*)
10.202 + Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
10.203 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}),(*"0 * z = 0"*)
10.204 + Thm ("add_0_left",num_str @{thm add_0_left})(*0 + z = z*)
10.205
10.206 (*Rls_ order_add_rls_*)
10.207 ],
11.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Tue Aug 31 11:10:30 2010 +0200
11.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Tue Aug 31 15:36:57 2010 +0200
11.3 @@ -1349,11 +1349,11 @@
11.4 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
11.5 Thm ("real_mult_assoc",num_str real_mult_assoc),
11.6 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
11.7 - Thm ("real_add_commute",num_str real_add_commute),
11.8 + Thm ("add_commute",num_str @{thm add_commute}),
11.9 (*z + w = w + z*)
11.10 - Thm ("real_add_left_commute",num_str real_add_left_commute),
11.11 + Thm ("add_left_commute",num_str @{thm add_left_commute}),
11.12 (*x + (y + z) = y + (x + z)*)
11.13 - Thm ("real_add_assoc",num_str real_add_assoc)
11.14 + Thm ("add_assoc",num_str @{thm add_assoc})
11.15 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
11.16 ], scr = EmptyScr}:rls);
11.17
11.18 @@ -1418,8 +1418,8 @@
11.19 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
11.20 Thm ("separate_1_bdv_n", num_str separate_1_bdv_n),
11.21 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
11.22 - Thm ("real_add_divide_distrib",
11.23 - num_str real_add_divide_distrib)
11.24 + Thm ("nadd_divide_distrib",
11.25 + num_str @{thm nadd_divide_distrib})
11.26 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
11.27 WN051031 DOES NOT BELONG TO HERE*)
11.28 ];
12.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Tue Aug 31 11:10:30 2010 +0200
12.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Tue Aug 31 15:36:57 2010 +0200
12.3 @@ -297,11 +297,11 @@
12.4
12.5 Calc ("op *", eval_binop "#mult_"),
12.6
12.7 - Thm ("real_mult_0",num_str real_mult_0),
12.8 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
12.9 (*"0 * z = 0"*)
12.10 - Thm ("real_mult_1",num_str real_mult_1),
12.11 + Thm ("mult_1_left",num_str @{thm mult_1_left}),
12.12 (*"1 * z = z"*)
12.13 - Thm ("real_add_zero_left",num_str real_add_zero_left),
12.14 + Thm ("add_0_left",num_str @{thm add_0_left}),
12.15 (*"0 + z = z"*)
12.16 Thm ("null_minus",num_str null_minus),
12.17 (*"0 - a = -a"*)
12.18 @@ -328,9 +328,9 @@
12.19 val klammern_ausmultiplizieren =
12.20 Rls{id = "klammern_ausmultiplizieren", preconds = [],
12.21 rew_ord = ("dummy_ord", dummy_ord), srls = Erls, calc = [], erls = Erls,
12.22 - rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
12.23 + rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
12.24 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
12.25 - Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
12.26 + Thm ("left_distrib2",num_str @{thm left_distrib}2),
12.27 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
12.28
12.29 Thm ("klammer_mult_minus",num_str klammer_mult_minus),
13.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Aug 31 11:10:30 2010 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Aug 31 15:36:57 2010 +0200
13.3 @@ -2781,7 +2781,7 @@
13.4 rules =
13.5 [Calc ("HOL.divide" ,eval_cancel "#divide_"),
13.6
13.7 - Thm ("sym_real_minus_divide_eq",
13.8 + Thm ("minus_divide_left",
13.9 num_str (real_minus_divide_eq RS sym)),
13.10 (*SYM - ?x / ?y = - (?x / ?y) may come from subst*)
13.11
13.12 @@ -2801,14 +2801,14 @@
13.13
13.14 Thm ("rat_mult",num_str rat_mult),
13.15 (*a / b * (c / d) = a * c / (b * d)*)
13.16 - Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
13.17 + Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
13.18 (*?x * (?y / ?z) = ?x * ?y / ?z*)
13.19 - Thm ("real_times_divide2_eq",num_str real_times_divide2_eq),
13.20 + Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
13.21 (*?y / ?z * ?x = ?y * ?x / ?z*)
13.22
13.23 Thm ("real_divide_divide1",num_str real_divide_divide1),
13.24 (*"?y ~= 0 ==> ?u / ?v / (?y / ?z) = ?u / ?v * (?z / ?y)"*)
13.25 - Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq),
13.26 + Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left}),
13.27 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
13.28
13.29 Thm ("rat_power", num_str rat_power),
13.30 @@ -3520,16 +3520,16 @@
13.31 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
13.32 rules = [Thm ("rat_mult",num_str rat_mult),
13.33 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
13.34 - Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
13.35 + Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
13.36 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
13.37 otherwise inv.to a / b / c = ...*)
13.38 - Thm ("real_times_divide2_eq",num_str real_times_divide2_eq),
13.39 + Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
13.40 (*"?a / ?b * ?c = ?a * ?c / ?b" order weights x^^^n too much
13.41 and does not commute a / b * c ^^^ 2 !*)
13.42
13.43 - Thm ("real_divide_divide1_eq", real_divide_divide1_eq),
13.44 + Thm ("divide_divide_eq_right", real_divide_divide1_eq),
13.45 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
13.46 - Thm ("real_divide_divide2_eq", real_divide_divide2_eq),
13.47 + Thm ("divide_divide_eq_left", real_divide_divide2_eq),
13.48 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
13.49 Calc ("HOL.divide" ,eval_cancel "#divide_")
13.50 ],
13.51 @@ -3539,20 +3539,20 @@
13.52 val reduce_0_1_2 = prep_rls(
13.53 Rls{id = "reduce_0_1_2", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
13.54 erls = e_rls,srls = Erls,calc = [],(*asm_thm = [],*)
13.55 - rules = [(*Thm ("real_divide_1",num_str real_divide_1),
13.56 + rules = [(*Thm ("divide_1",num_str @{thm divide_1}),
13.57 "?x / 1 = ?x" unnecess.for normalform*)
13.58 - Thm ("real_mult_1",num_str real_mult_1),
13.59 + Thm ("mult_1_left",num_str @{thm mult_1_left}),
13.60 (*"1 * z = z"*)
13.61 (*Thm ("real_mult_minus1",num_str real_mult_minus1),
13.62 "-1 * z = - z"*)
13.63 (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel),
13.64 "- ?x * - ?y = ?x * ?y"*)
13.65
13.66 - Thm ("real_mult_0",num_str real_mult_0),
13.67 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
13.68 (*"0 * z = 0"*)
13.69 - Thm ("real_add_zero_left",num_str real_add_zero_left),
13.70 + Thm ("add_0_left",num_str @{thm add_0_left}),
13.71 (*"0 + z = z"*)
13.72 - (*Thm ("real_add_minus",num_str real_add_minus),
13.73 + (*Thm ("right_minus",num_str @{thm right_minus}),
13.74 "?z + - ?z = 0"*)
13.75
13.76 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)),
13.77 @@ -3560,7 +3560,7 @@
13.78 Thm ("real_mult_2_assoc",num_str real_mult_2_assoc),
13.79 (*"z1 + (z1 + k) = 2 * z1 + k"*)
13.80
13.81 - Thm ("real_0_divide",num_str real_0_divide)
13.82 + Thm ("divide_zero_left",num_str @{thm divide_zero_left})
13.83 (*"0 / ?x = 0"*)
13.84 ], scr = EmptyScr}:rls);
13.85
13.86 @@ -3615,14 +3615,14 @@
13.87 val simplify_rational =
13.88 merge_rls "simplify_rational" expand_binoms
13.89 (append_rls "divide" calculate_Rational
13.90 - [Thm ("real_divide_1",num_str real_divide_1),
13.91 + [Thm ("divide_1",num_str @{thm divide_1}),
13.92 (*"?x / 1 = ?x"*)
13.93 Thm ("rat_mult",num_str rat_mult),
13.94 (*(1)"?a / ?b * (?c / ?d) = ?a * ?c / (?b * ?d)"*)
13.95 - Thm ("real_times_divide1_eq",num_str real_times_divide1_eq),
13.96 + Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
13.97 (*(2)"?a * (?c / ?d) = ?a * ?c / ?d" must be [2],
13.98 otherwise inv.to a / b / c = ...*)
13.99 - Thm ("real_times_divide2_eq",num_str real_times_divide2_eq),
13.100 + Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
13.101 (*"?a / ?b * ?c = ?a * ?c / ?b"*)
13.102 Thm ("add_minus",num_str add_minus),
13.103 (*"?a + ?b - ?b = ?a"*)
13.104 @@ -3705,9 +3705,9 @@
13.105
13.106 Thm ("real_divide_divide1_mg", real_divide_divide1_mg),
13.107 (*"y ~= 0 ==> (u / v) / (y / z) = (u * z) / (y * v)"*)
13.108 - Thm ("real_divide_divide1_eq", real_divide_divide1_eq),
13.109 + Thm ("divide_divide_eq_right", real_divide_divide1_eq),
13.110 (*"?x / (?y / ?z) = ?x * ?z / ?y"*)
13.111 - Thm ("real_divide_divide2_eq", real_divide_divide2_eq),
13.112 + Thm ("divide_divide_eq_left", real_divide_divide2_eq),
13.113 (*"?x / ?y / ?z = ?x / (?y * ?z)"*)
13.114 Calc ("HOL.divide" ,eval_cancel "#divide_"),
13.115
13.116 @@ -3721,9 +3721,9 @@
13.117 Rls {id = "rat_reduce_1", preconds = [],
13.118 rew_ord = ("dummy_ord",dummy_ord),
13.119 erls = e_rls, srls = Erls, calc = [],
13.120 - rules = [Thm ("real_divide_1",num_str real_divide_1),
13.121 + rules = [Thm ("divide_1",num_str @{thm divide_1}),
13.122 (*"?x / 1 = ?x"*)
13.123 - Thm ("real_mult_1",num_str real_mult_1)
13.124 + Thm ("mult_1_left",num_str @{thm mult_1_left})
13.125 (*"1 * z = z"*)
13.126 ],
13.127 scr = Script ((term_of o the o (parse thy)) "empty_script")
14.1 --- a/src/Tools/isac/Knowledge/Root.thy Tue Aug 31 11:10:30 2010 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Root.thy Tue Aug 31 15:36:57 2010 +0200
14.3 @@ -198,20 +198,20 @@
14.4 rules = [Thm ("real_diff_minus",num_str real_diff_minus),
14.5 (*"a - b = a + (-1) * b"*)
14.6
14.7 - Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
14.8 + Thm ("left_distrib" ,num_str @{thm left_distrib}),
14.9 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
14.10 - Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
14.11 + Thm ("left_distrib2",num_str @{thm left_distrib}2),
14.12 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
14.13 - Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
14.14 + Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
14.15 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
14.16 - Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
14.17 + Thm ("left_diff_distrib2",num_str @{thm left_diff_distrib}2),
14.18 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
14.19
14.20 - Thm ("real_mult_1",num_str real_mult_1),
14.21 + Thm ("mult_1_left",num_str @{thm mult_1_left}),
14.22 (*"1 * z = z"*)
14.23 - Thm ("real_mult_0",num_str real_mult_0),
14.24 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
14.25 (*"0 * z = 0"*)
14.26 - Thm ("real_add_zero_left",num_str real_add_zero_left),
14.27 + Thm ("add_0_left",num_str @{thm add_0_left}),
14.28 (*"0 + z = z"*)
14.29
14.30 Thm ("real_mult_commute",num_str real_mult_commute),
14.31 @@ -220,11 +220,11 @@
14.32 (**)
14.33 Thm ("real_mult_assoc",num_str real_mult_assoc),
14.34 (**)
14.35 - Thm ("real_add_commute",num_str real_add_commute),
14.36 + Thm ("add_commute",num_str @{thm add_commute}),
14.37 (**)
14.38 - Thm ("real_add_left_commute",num_str real_add_left_commute),
14.39 + Thm ("add_left_commute",num_str @{thm add_left_commute}),
14.40 (**)
14.41 - Thm ("real_add_assoc",num_str real_add_assoc),
14.42 + Thm ("add_assoc",num_str @{thm add_assoc}),
14.43 (**)
14.44
14.45 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
14.46 @@ -286,9 +286,9 @@
14.47 Thm ("realpow_mul",num_str realpow_mul),
14.48 (*(a*b)^^^n = a^^^n * b^^^n*)
14.49
14.50 - Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
14.51 - Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
14.52 - Thm ("real_add_zero_left",num_str real_add_zero_left),
14.53 + Thm ("mult_1_left",num_str @{thm mult_1_left}), (*"1 * z = z"*)
14.54 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}), (*"0 * z = 0"*)
14.55 + Thm ("add_0_left",num_str @{thm add_0_left}),
14.56 (*"0 + z = z"*)
14.57
14.58 Calc ("op +", eval_binop "#add_"),
15.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Tue Aug 31 11:10:30 2010 +0200
15.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Tue Aug 31 15:36:57 2010 +0200
15.3 @@ -214,12 +214,12 @@
15.4
15.5 val RootEq_erls =
15.6 append_rls "RootEq_erls" Root_erls
15.7 - [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)
15.8 + [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
15.9 ];
15.10
15.11 val RootEq_crls =
15.12 append_rls "RootEq_crls" Root_crls
15.13 - [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)
15.14 + [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
15.15 ];
15.16
15.17 val rooteq_srls =
16.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Tue Aug 31 11:10:30 2010 +0200
16.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Tue Aug 31 15:36:57 2010 +0200
16.3 @@ -23,9 +23,9 @@
16.4 (*.calculate numeral groundterms.*)
16.5 val calculate_RootRat =
16.6 append_rls "calculate_RootRat" calculate_Rational
16.7 - [Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
16.8 + [Thm ("left_distrib2",num_str @{thm left_distrib}2),
16.9 (* w*(z1.0 + z2.0) = w * z1.0 + w * z2.0 *)
16.10 - Thm ("real_mult_1",num_str real_mult_1),
16.11 + Thm ("mult_1_left",num_str @{thm mult_1_left}),
16.12 (* 1 * z = z *)
16.13 Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym)),
16.14 (* "- z1 = -1 * z1" *)
17.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Aug 31 11:10:30 2010 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Aug 31 15:36:57 2010 +0200
17.3 @@ -210,7 +210,7 @@
17.4 erls = e_rls, srls = Erls,
17.5 calc = [],
17.6 rules = [Thm ("refl",num_str refl),
17.7 - Thm ("le_refl",num_str le_refl),
17.8 + Thm ("real_le_refl",num_str @{thm real_le_refl}),
17.9 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
17.10 Thm ("not_true",num_str not_true),
17.11 Thm ("not_false",num_str not_false),
17.12 @@ -244,7 +244,7 @@
17.13 erls=testerls,srls = e_rls,
17.14 calc=[],
17.15 rules = [Thm ("refl",num_str refl),
17.16 - Thm ("le_refl",num_str le_refl),
17.17 + Thm ("real_le_refl",num_str @{thm real_le_refl}),
17.18 Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
17.19 Thm ("not_true",num_str not_true),
17.20 Thm ("not_false",num_str not_false),
17.21 @@ -1263,19 +1263,19 @@
17.22 (*asm_thm = [],*)
17.23 rules = [Thm ("real_diff_minus",num_str real_diff_minus),
17.24 (*"a - b = a + (-1) * b"*)
17.25 - Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
17.26 + Thm ("left_distrib" ,num_str @{thm left_distrib}),
17.27 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
17.28 - Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
17.29 + Thm ("left_distrib2",num_str @{thm left_distrib}2),
17.30 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
17.31 - Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
17.32 + Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
17.33 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
17.34 - Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
17.35 + Thm ("left_diff_distrib2",num_str @{thm left_diff_distrib}2),
17.36 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
17.37 - Thm ("real_mult_1",num_str real_mult_1),
17.38 + Thm ("mult_1_left",num_str @{thm mult_1_left}),
17.39 (*"1 * z = z"*)
17.40 - Thm ("real_mult_0",num_str real_mult_0),
17.41 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
17.42 (*"0 * z = 0"*)
17.43 - Thm ("real_add_zero_left",num_str real_add_zero_left),
17.44 + Thm ("add_0_left",num_str @{thm add_0_left}),
17.45 (*"0 + z = z"*)
17.46
17.47 (*AC-rewriting*)
17.48 @@ -1285,11 +1285,11 @@
17.49 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
17.50 Thm ("real_mult_assoc",num_str real_mult_assoc),
17.51 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
17.52 - Thm ("real_add_commute",num_str real_add_commute),
17.53 + Thm ("add_commute",num_str @{thm add_commute}),
17.54 (*z + w = w + z*)
17.55 - Thm ("real_add_left_commute",num_str real_add_left_commute),
17.56 + Thm ("add_left_commute",num_str @{thm add_left_commute}),
17.57 (*x + (y + z) = y + (x + z)*)
17.58 - Thm ("real_add_assoc",num_str real_add_assoc),
17.59 + Thm ("add_assoc",num_str @{thm add_assoc}),
17.60 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
17.61
17.62 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
17.63 @@ -1392,19 +1392,19 @@
17.64 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
17.65
17.66
17.67 - (* Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib),
17.68 + (* Thm ("left_distrib" ,num_str @{thm left_distrib}),
17.69 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
17.70 - Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2),
17.71 + Thm ("left_distrib2",num_str @{thm left_distrib}2),
17.72 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
17.73 - Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib),
17.74 + Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
17.75 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
17.76 - Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2),
17.77 + Thm ("left_diff_distrib2",num_str @{thm left_diff_distrib}2),
17.78 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
17.79 *)
17.80
17.81 - Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*)
17.82 - Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*)
17.83 - Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*)
17.84 + Thm ("mult_1_left",num_str @{thm mult_1_left}), (*"1 * z = z"*)
17.85 + Thm ("mult_zero_left",num_str @{thm mult_zero_left}), (*"0 * z = 0"*)
17.86 + Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
17.87
17.88 Calc ("op +", eval_binop "#add_"),
17.89 Calc ("op *", eval_binop "#mult_"),
17.90 @@ -1413,9 +1413,9 @@
17.91 Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*)
17.92 Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**)
17.93 Thm ("real_mult_assoc",num_str real_mult_assoc), (**)
17.94 - Thm ("real_add_commute",num_str real_add_commute), (**)
17.95 - Thm ("real_add_left_commute",num_str real_add_left_commute), (**)
17.96 - Thm ("real_add_assoc",num_str real_add_assoc), (**)
17.97 + Thm ("add_commute",num_str @{thm add_commute}), (**)
17.98 + Thm ("add_left_commute",num_str @{thm add_left_commute}), (**)
17.99 + Thm ("add_assoc",num_str @{thm add_assoc}), (**)
17.100 *)
17.101
17.102 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)),
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/Tools/isac/ProgLang/Language.thy Tue Aug 31 15:36:57 2010 +0200
18.3 @@ -0,0 +1,12 @@
18.4 +(* Title: collect all defitions for the program language
18.5 + Author: Walther Neuper 100831
18.6 + (c) due to copyright terms
18.7 + *)
18.8 +
18.9 +theory Language imports Script
18.10 +uses ("scrtools.sml")
18.11 +begin
18.12 +
18.13 +use "scrtools.sml"
18.14 +
18.15 +end
18.16 \ No newline at end of file
19.1 --- a/src/Tools/isac/ProgLang/ListC.thy Tue Aug 31 11:10:30 2010 +0200
19.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Tue Aug 31 15:36:57 2010 +0200
19.3 @@ -1,13 +1,6 @@
19.4 -(* use_thy_only"../ProgLang/ListC";
19.5 - use_thy_only"ProgLang/ListC";
19.6 - use_thy"ProgLang/ListC";
19.7 -
19.8 - use_thy_only"ListC";
19.9 - W.N. 8.01
19.10 - attaches identifiers to definition of listfuns,
19.11 - for storing them in list_rls
19.12 -
19.13 -WN.29.4.03:
19.14 +(* Title: functions on lists for Scripts
19.15 + Author: Walther Neuper 0108
19.16 + (c) due to copyright terms
19.17 *)
19.18
19.19 theory ListC imports Complex_Main
20.1 --- a/src/Tools/isac/ProgLang/Real2002-theorems.sml Tue Aug 31 11:10:30 2010 +0200
20.2 +++ b/src/Tools/isac/ProgLang/Real2002-theorems.sml Tue Aug 31 15:36:57 2010 +0200
20.3 @@ -443,7 +443,7 @@
20.4 "real_minus_congruent";
20.5 "real_minus";
20.6 "- Abs_REAL (realrel `` {(?x, ?y)}) = Abs_REAL (realrel `` {(?y, ?x)})"
20.7 - "real_minus_minus"; (**)"- (- (?z::real)) = ?z"
20.8 + "minus_minus"; (**)"- (- (?z::real)) = ?z"
20.9 "inj_real_minus"; "inj uminus"
20.10 "real_minus_zero"; (**)"- 0 = 0"
20.11 "real_minus_zero_iff"; (**)"(- ?x = 0) = (?x = 0)"
20.12 @@ -454,19 +454,19 @@
20.13 "Abs_REAL (realrel `` {(?x1.0, ?y1.0)}) +
20.14 Abs_REAL (realrel `` {(?x2.0, ?y2.0)}) =
20.15 Abs_REAL (realrel `` {(?x1.0 + ?x2.0, ?y1.0 + ?y2.0)})"
20.16 - "real_add_commute"; (**)"(?z::real) + (?w::real) = ?w + ?z"
20.17 - "real_add_assoc"; (**)
20.18 - "real_add_left_commute"; (**)
20.19 - "real_add_zero_left"; (**)"0 + ?z = ?z"
20.20 - "real_add_zero_right"; (**)
20.21 - "real_add_minus"; (**)"?z + - ?z = 0"
20.22 - "real_add_minus_left"; (**)
20.23 - "real_add_minus_cancel"; (**)"?z + (- ?z + ?w) = ?w"
20.24 + "add_commute"; (**)"(?z::real) + (?w::real) = ?w + ?z"
20.25 + "add_assoc"; (**)
20.26 + "add_left_commute"; (**)
20.27 + "add_0_left"; (**)"0 + ?z = ?z"
20.28 + "add_0_right"; (**)
20.29 + "right_minus"; (**)"?z + - ?z = 0"
20.30 + "right_minus_left"; (**)
20.31 + "right_minus_cancel"; (**)"?z + (- ?z + ?w) = ?w"
20.32 "real_minus_add_cancel"; (**)"- ?z + (?z + ?w) = ?w"
20.33 "real_minus_ex"; "EX y. ?x + y = 0"
20.34 "real_minus_ex1";
20.35 "real_minus_left_ex1"; "EX! y. y + ?x = 0"
20.36 - "real_add_minus_eq_minus";"?x + ?y = 0 ==> ?x = - ?y"
20.37 + "right_minus_eq_minus";"?x + ?y = 0 ==> ?x = - ?y"
20.38 "real_as_add_inverse_ex"; "EX y. ?x = - y"
20.39 "real_minus_add_distrib"; (**)"- (?x + ?y) = - ?x + - ?y"
20.40 "real_add_left_cancel"; "(?x + ?y = ?x + ?z) = (?y = ?z)"
20.41 @@ -491,23 +491,23 @@
20.42 "real_mult_assoc"; (**)
20.43 "real_mult_left_commute";
20.44 (**)"?z1.0 * (?z2.0 * ?z3.0) = ?z2.0 * (?z1.0 * ?z3.0)"
20.45 - "real_mult_1"; (**)"1 * ?z = ?z"
20.46 - "real_mult_1_right"; (**)"?z * 1 = ?z"
20.47 - "real_mult_0"; (**)
20.48 - "real_mult_0_right"; (**)"?z * 0 = 0"
20.49 + "mult_1_left"; (**)"1 * ?z = ?z"
20.50 + "mult_1_right"; (**)"?z * 1 = ?z"
20.51 + "mult_zero_left"; (**)
20.52 + "mult_zero_left_right"; (**)"?z * 0 = 0"
20.53 "real_mult_minus_eq1"; (**)"- ?x * ?y = - (?x * ?y)"
20.54 "real_mult_minus_eq2"; (**)"?x * - ?y = - (?x * ?y)"
20.55 "real_mult_minus_1"; (**)"- 1 * ?z = - ?z"
20.56 "real_mult_minus_1_right";(**)"?z * - 1 = - ?z"
20.57 "real_minus_mult_cancel"; (**)"- ?x * - ?y = ?x * ?y"
20.58 "real_minus_mult_commute";(**)"- ?x * ?y = ?x * - ?y"
20.59 - "real_add_assoc_cong";
20.60 + "add_assoc_cong";
20.61 "?z + ?v = ?z' + ?v' ==> ?z + (?v + ?w) = ?z' + (?v' + ?w)"
20.62 - "real_add_assoc_swap"; (**)"?z + (?v + ?w) = ?v + (?z + ?w)"
20.63 - "real_add_mult_distrib"; (**)"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"
20.64 - "real_add_mult_distrib2"; (**)"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"
20.65 - "real_diff_mult_distrib"; (**)"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"
20.66 - "real_diff_mult_distrib2";(**)"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"
20.67 + "add_assoc_swap"; (**)"?z + (?v + ?w) = ?v + (?z + ?w)"
20.68 + "left_distrib"; (**)"(?z1.0 + ?z2.0) * ?w = ?z1.0 * ?w + ?z2.0 * ?w"
20.69 + "left_distrib2"; (**)"?w * (?z1.0 + ?z2.0) = ?w * ?z1.0 + ?w * ?z2.0"
20.70 + "left_diff_distrib"; (**)"(?z1.0 - ?z2.0) * ?w = ?z1.0 * ?w - ?z2.0 * ?w"
20.71 + "left_diff_distrib2";(**)"?w * (?z1.0 - ?z2.0) = ?w * ?z1.0 - ?w * ?z2.0"
20.72 "real_zero_not_eq_one";
20.73 "real_zero_iff"; "0 = Abs_REAL (realrel `` {(?x, ?x)})"
20.74 "real_mult_inv_right_ex"; "?x ~= 0 ==> EX y. ?x * y = 1"
20.75 @@ -526,13 +526,13 @@
20.76 "real_inverse_1"; "inverse 1 = 1"
20.77 "real_minus_inverse"; "inverse (- ?x) = - inverse ?x"
20.78 "real_inverse_distrib"; "inverse (?x * ?y) = inverse ?x * inverse ?y"
20.79 - "real_times_divide1_eq"; (**)"?x * (?y / ?z) = ?x * ?y / ?z"
20.80 - "real_times_divide2_eq"; (**)"?y / ?z * ?x = ?y * ?x / ?z"
20.81 - "real_divide_divide1_eq"; (**)"?x / (?y / ?z) = ?x * ?z / ?y"
20.82 - "real_divide_divide2_eq"; (**)"?x / ?y / ?z = ?x / (?y * ?z)"
20.83 + "times_divide_eq_right"; (**)"?x * (?y / ?z) = ?x * ?y / ?z"
20.84 + "times_divide_eq_left"; (**)"?y / ?z * ?x = ?y * ?x / ?z"
20.85 + "divide_divide_eq_right"; (**)"?x / (?y / ?z) = ?x * ?z / ?y"
20.86 + "divide_divide_eq_left"; (**)"?x / ?y / ?z = ?x / (?y * ?z)"
20.87 "real_minus_divide_eq"; (**)"- ?x / ?y = - (?x / ?y)"
20.88 "real_divide_minus_eq"; (**)"?x / - ?y = - (?x / ?y)"
20.89 - "real_add_divide_distrib"; (**)"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
20.90 + "nadd_divide_distrib"; (**)"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
20.91 "preal_lemma_eq_rev_sum";
20.92 "[| ?x = ?y; ?x1.0 = ?y1.0 |] ==> ?x + ?y1.0 = ?x1.0 + ?y"
20.93 "preal_add_left_commute_cancel";
20.94 @@ -560,7 +560,7 @@
20.95 "real_of_preal_not_minus_gt_zero";
20.96 "real_of_preal_zero_less";
20.97 "real_of_preal_not_less_zero";
20.98 - "real_minus_minus_zero_less";
20.99 + "minus_minus_zero_less";
20.100 "real_of_preal_sum_zero_less";
20.101 "real_of_preal_minus_less_all";
20.102 "real_of_preal_not_minus_gt_all";
20.103 @@ -640,7 +640,7 @@
20.104 "real_add_left_le_mono1";
20.105 "real_add_le_mono";
20.106 "real_less_Ex";
20.107 - "real_add_minus_positive_less_self"; "0 < ?r ==> ?u + - ?r < ?u"
20.108 + "right_minus_positive_less_self"; "0 < ?r ==> ?u + - ?r < ?u"
20.109 "real_le_minus_iff"; "(- ?s <= - ?r) = (?r <= ?s)"
20.110 "real_le_square";
20.111 "real_of_posnat_one";
20.112 @@ -760,7 +760,7 @@
20.113 "[| ?i <= ?j; ?k <= ?l; 0 <= ?j; 0 <= ?k |] ==> ?i * ?k <= ?j * ?l"
20.114 RealArith0.ML:qed ------------------------------------------------------------
20.115 "real_diff_minus_eq"; (**)"?x - - ?y = ?x + ?y"
20.116 - "real_0_divide"; (**)"0 / ?x = 0"
20.117 + "divide_zero_left"; (**)"0 / ?x = 0"
20.118 "real_0_less_inverse_iff"; "(0 < inverse ?x) = (0 < ?x)"
20.119 "real_inverse_less_0_iff";
20.120 "real_0_le_inverse_iff";
20.121 @@ -803,7 +803,7 @@
20.122 "real_divide_eq_cancel1"; "(?k / ?m = ?k / ?n) = (?k = 0 | ?m = ?n)"
20.123 "real_inverse_less_iff";
20.124 "real_inverse_le_iff";
20.125 - "real_divide_1"; (**)"?x / 1 = ?x"
20.126 + "divide_1"; (**)"?x / 1 = ?x"
20.127 "real_divide_minus1"; (**)"?x / -1 = - ?x"
20.128 "real_minus1_divide"; (**)"-1 / ?x = - (1 / ?x)"
20.129 "real_lbound_gt_zero";
20.130 @@ -816,7 +816,7 @@
20.131 "real_minus_le"; "(- ?x <= ?y) = (- ?y <= ?x)"
20.132 "real_equation_minus"; (**)"(?x = - ?y) = (?y = - ?x)"
20.133 "real_minus_equation"; (**)"(- ?x = ?y) = (- ?y = ?x)"
20.134 - "real_add_minus_iff"; (**)"(?x + - ?a = 0) = (?x = ?a)"
20.135 + "right_minus_iff"; (**)"(?x + - ?a = 0) = (?x = ?a)"
20.136 "real_minus_eq_cancel"; (**)"(- ?b = - ?a) = (?b = ?a)"
20.137 "real_add_eq_0_iff"; (**)"(?x + ?y = 0) = (?y = - ?x)"
20.138 "real_add_less_0_iff"; "(?x + ?y < 0) = (?y < - ?x)"
20.139 @@ -874,7 +874,7 @@
20.140 "abs_add_less"; "[| abs ?x < ?r; abs ?y < ?s |] ==> abs (?x + ?y) < ?r + ?s"
20.141 RealAbs.ML:qed
20.142 "abs_add_minus_less";
20.143 - "real_mult_0_less"; "(0 * ?x < ?r) = (0 < ?r)"
20.144 + "mult_zero_left_less"; "(0 * ?x < ?r) = (0 < ?r)"
20.145 "real_mult_less_trans";
20.146 "real_mult_le_less_trans";
20.147 "abs_mult_less";
21.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Tue Aug 31 11:10:30 2010 +0200
21.2 +++ b/src/Tools/isac/ProgLang/rewrite.sml Tue Aug 31 15:36:57 2010 +0200
21.3 @@ -451,14 +451,14 @@
21.4 (*> assoc_thm' Isac.thy ("sym_#mult_2_3","6 = 2 * 3");
21.5 val it = "6 = 2 * 3" : thm
21.6
21.7 -> assoc_thm' Isac.thy ("real_add_zero_left","");
21.8 +> assoc_thm' Isac.thy ("add_0_left","");
21.9 val it = "0 + ?z = ?z" : thm
21.10
21.11 > assoc_thm' Isac.thy ("sym_real_add_zero_left","");
21.12 val it = "?t = 0 + ?t" [.] : thm
21.13
21.14 > assoc_thm' HOL.thy ("sym_real_add_zero_left","");
21.15 -*** Unknown theorem(s) "real_add_zero_left"
21.16 +*** Unknown theorem(s) "add_0_left"
21.17 *** assoc_thm': 'sym_real_add_zero_left' not in 'HOL.thy' (and parents)
21.18 uncaught exception ERROR*)
21.19
22.1 --- a/test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_Know111.thy Tue Aug 31 11:10:30 2010 +0200
22.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/3knowledge/Foo_Know111.thy Tue Aug 31 15:36:57 2010 +0200
22.3 @@ -1,11 +1,11 @@
22.4 -theory Foo_Know111 imports "../1language/Foo_Language" begin
22.5 +theory Foo_Know111 imports "../1language/Foo_Language" Complex_Main begin
22.6
22.7 consts foo111 :: "'a"
22.8 bar111 :: "'a"
22.9 axioms code111 : "foo111 = bar111"
22.10
22.11 ML {*
22.12 -(* there is an error when de-commenting *) 111
22.13 +@{thm code111};
22.14 *}
22.15
22.16 end
22.17 \ No newline at end of file
23.1 --- a/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Tue Aug 31 11:10:30 2010 +0200
23.2 +++ b/test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy Tue Aug 31 15:36:57 2010 +0200
23.3 @@ -1,4 +1,10 @@
23.4 -theory Build_Test imports Main begin
23.5 +(*
23.6 +$ cd /usr/local/isabisac/test/Tools/isac/ADDTESTS/file-depend
23.7 +$ /usr/local/isabisac/bin/isabelle emacs Build_Test.thy &
23.8 +
23.9 +*)
23.10 +
23.11 +theory Build_Test imports Complex_Main begin
23.12
23.13 use "0foolibrary.ML"
23.14 use_thy "1language/Foo_Language"