1.1 --- a/src/Tools/isac/Knowledge/Atools.thy Tue Oct 05 14:41:16 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Tue Oct 05 15:28:32 2010 +0200
1.3 @@ -325,8 +325,8 @@
1.4
1.5
1.6 (*.evaluate < and <= for numerals.*)
1.7 -(*("le" ,("op <" ,eval_equ "#less_")),
1.8 - ("leq" ,("op <=" ,eval_equ "#less_equal_"))*)
1.9 +(*("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
1.10 + ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_"))*)
1.11 fun eval_equ (thmid:string) (op_:string) (t as
1.12 (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) thy =
1.13 (case (int_of_str n1, int_of_str n2) of
1.14 @@ -562,8 +562,8 @@
1.15 append_rls "list_rls" list_rls
1.16 [Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.17 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.18 - Calc ("op <",eval_equ "#less_"),
1.19 - Calc ("op <=",eval_equ "#less_equal_"),
1.20 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.21 + Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.22 Calc ("Atools.ident",eval_ident "#ident_"),
1.23 Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*)
1.24
1.25 @@ -586,8 +586,8 @@
1.26
1.27 val calculate_Atools =
1.28 append_rls "calculate_Atools" e_rls
1.29 - [Calc ("op <",eval_equ "#less_"),
1.30 - Calc ("op <=",eval_equ "#less_equal_"),
1.31 + [Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.32 + Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.33 Calc ("op =",eval_equal "#equal_"),
1.34
1.35 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
1.36 @@ -619,8 +619,8 @@
1.37 Thm ("real_le_refl",num_str @{thm real_le_refl}),
1.38 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
1.39
1.40 - Calc ("op <",eval_equ "#less_"),
1.41 - Calc ("op <=",eval_equ "#less_equal_"),
1.42 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.43 + Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.44
1.45 Calc ("Atools.ident",eval_ident "#ident_"),
1.46 Calc ("Atools.is'_const",eval_const "#is_const_"),
1.47 @@ -645,8 +645,8 @@
1.48 Thm ("real_le_refl",num_str @{thm real_le_refl}),
1.49 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}),
1.50
1.51 - Calc ("op <",eval_equ "#less_"),
1.52 - Calc ("op <=",eval_equ "#less_equal_"),
1.53 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.54 + Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.55
1.56 Calc ("Atools.ident",eval_ident "#ident_"),
1.57 Calc ("Atools.is'_const",eval_const "#is_const_"),
1.58 @@ -679,8 +679,8 @@
1.59 Thm ("and_commute",num_str @{thm and_commute}),
1.60 Thm ("or_commute",num_str @{thm or_commute}),
1.61
1.62 - Calc ("op <",eval_equ "#less_"),
1.63 - Calc ("op <=",eval_equ "#less_equal_"),
1.64 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
1.65 + Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
1.66
1.67 Calc ("Atools.ident",eval_ident "#ident_"),
1.68 Calc ("Atools.is'_const",eval_const "#is_const_"),
1.69 @@ -704,8 +704,8 @@
1.70 ("is_atom" ,("Atools.is'_atom",eval_is_atom "#is_atom_")),
1.71 ("is_even" ,("Atools.is'_even",eval_is_even "#is_even_")),
1.72 ("is_const" ,("Atools.is'_const",eval_const "#is_const_")),
1.73 - ("le" ,("op <" ,eval_equ "#less_")),
1.74 - ("leq" ,("op <=" ,eval_equ "#less_equal_")),
1.75 + ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
1.76 + ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")),
1.77 ("ident" ,("Atools.ident",eval_ident "#ident_")),
1.78 ("equal" ,("op =",eval_equal "#equal_")),
1.79 ("PLUS" ,("Groups.plus_class.plus" ,eval_binop "#add_")),
1.80 @@ -725,7 +725,7 @@
1.81 erls = e_rls,
1.82 srls = Erls, calc = [], (*asm_thm = [],*)
1.83 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1.84 - Calc ("op <",eval_equ "#less_")
1.85 + Calc ("Orderings.ord_class.less",eval_equ "#less_")
1.86 (* ~~~~~~ for nth_Cons_*)
1.87 ],
1.88 scr = EmptyScr},
2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Tue Oct 05 14:41:16 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Tue Oct 05 15:28:32 2010 +0200
2.3 @@ -183,7 +183,7 @@
2.4 rew_ord = ("termlessI",termlessI),
2.5 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
2.6 [(*for asm in NTH_CONS ...*)
2.7 - Calc ("op <",eval_equ "#less_"),
2.8 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
2.9 (*2nd NTH_CONS pushes n+-1 into asms*)
2.10 Calc("Groups.plus_class.plus", eval_binop "#add_")
2.11 ],
2.12 @@ -204,7 +204,7 @@
2.13 rew_ord = ("termlessI",termlessI),
2.14 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
2.15 [(*for asm in NTH_CONS ...*)
2.16 - Calc ("op <",eval_equ "#less_"),
2.17 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
2.18 (*2nd NTH_CONS pushes n+-1 into asms*)
2.19 Calc("Groups.plus_class.plus", eval_binop "#add_")
2.20 ],
3.1 --- a/src/Tools/isac/Knowledge/Diff.thy Tue Oct 05 14:41:16 2010 +0200
3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Tue Oct 05 15:28:32 2010 +0200
3.3 @@ -124,7 +124,7 @@
3.4 [Calc ("Atools.occurs'_in", eval_occurs_in ""),
3.5 Thm ("not_true",num_str @{thm not_true}),
3.6 Thm ("not_false",num_str @{thm not_false}),
3.7 - Calc ("op <",eval_equ "#less_"),
3.8 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
3.9 Thm ("and_true",num_str @{thm and_true}),
3.10 Thm ("and_false",num_str @{thm and_false})
3.11 ],
3.12 @@ -152,7 +152,7 @@
3.13 preconds = [],
3.14 rew_ord = ("termlessI",termlessI),
3.15 erls = append_rls "erls_diff_sym_conv" e_rls
3.16 - [Calc ("op <",eval_equ "#less_")
3.17 + [Calc ("Orderings.ord_class.less",eval_equ "#less_")
3.18 ],
3.19 srls = Erls, calc = [],
3.20 rules = [Thm ("frac_sym_conv", num_str @{thm frac_sym_conv}),
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Tue Oct 05 14:41:16 2010 +0200
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Tue Oct 05 15:28:32 2010 +0200
4.3 @@ -65,8 +65,8 @@
4.4 Thm ("and_commute",num_str @{thm and_commute}),
4.5 Thm ("or_commute",num_str @{thm or_commute}),
4.6
4.7 - Calc ("op <",eval_equ "#less_"),
4.8 - Calc ("op <=",eval_equ "#less_equal_"),
4.9 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
4.10 + Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
4.11
4.12 Calc ("Atools.ident",eval_ident "#ident_"),
4.13 Calc ("Atools.is'_const",eval_const "#is_const_"),
5.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Tue Oct 05 14:41:16 2010 +0200
5.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Tue Oct 05 15:28:32 2010 +0200
5.3 @@ -361,7 +361,7 @@
5.4 rew_ord = ("e_rew_ord", e_rew_ord),
5.5 erls = Erls, srls = Erls, calc = [],
5.6 rules = [(*for precond NTH_CONS ...*)
5.7 - Calc ("op <",eval_equ "#less_"),
5.8 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
5.9 Calc ("Groups.plus_class.plus", eval_binop "#add_")
5.10 (*immediately repeated rewrite pushes
5.11 '+' into precondition !*)
5.12 @@ -390,7 +390,7 @@
5.13 rew_ord = ("e_rew_ord", e_rew_ord),
5.14 erls = Erls, srls = Erls, calc = [],
5.15 rules = [(*for precond NTH_CONS ...*)
5.16 - Calc ("op <",eval_equ "#less_"),
5.17 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
5.18 Calc ("Groups.plus_class.plus", eval_binop "#add_")
5.19 (*immediately repeated rewrite pushes
5.20 '+' into precondition !*)
5.21 @@ -670,7 +670,7 @@
5.22 rew_ord = ("termlessI",termlessI),
5.23 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
5.24 [(*for asm in NTH_CONS ...*)
5.25 - Calc ("op <",eval_equ "#less_"),
5.26 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
5.27 (*2nd NTH_CONS pushes n+-1 into asms*)
5.28 Calc("Groups.plus_class.plus", eval_binop "#add_")
5.29 ],
6.1 --- a/src/Tools/isac/Knowledge/InsSort.sml Tue Oct 05 14:41:16 2010 +0200
6.2 +++ b/src/Tools/isac/Knowledge/InsSort.sml Tue Oct 05 15:28:32 2010 +0200
6.3 @@ -30,7 +30,7 @@
6.4 Thm ("ins_rec",ins_rec),
6.5 Thm ("sort_def",sort_def),
6.6
6.7 - Calc ("op <",eval_equ "#less_"),
6.8 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
6.9 Thm ("if_True", if_True),
6.10 Thm ("if_False", if_False)
6.11 ],
7.1 --- a/src/Tools/isac/Knowledge/Rational.thy Tue Oct 05 14:41:16 2010 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Tue Oct 05 15:28:32 2010 +0200
7.3 @@ -3470,7 +3470,7 @@
7.4 erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
7.5 rules = [Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
7.6 Calc ("Atools.is'_even",eval_is_even "#is_even_"),
7.7 - Calc ("op <",eval_equ "#less_"),
7.8 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
7.9 Thm ("not_false", num_str @{thm not_false}),
7.10 Thm ("not_true", num_str @{thm not_true}),
7.11 Calc ("Groups.plus_class.plus",eval_binop "#add_")
8.1 --- a/src/Tools/isac/Knowledge/Test.thy Tue Oct 05 14:41:16 2010 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Test.thy Tue Oct 05 15:28:32 2010 +0200
8.3 @@ -231,8 +231,8 @@
8.4 Calc ("Groups.times_class.times",eval_binop "#mult_"),
8.5 Calc ("Atools.pow" ,eval_binop "#power_"),
8.6
8.7 - Calc ("op <",eval_equ "#less_"),
8.8 - Calc ("op <=",eval_equ "#less_equal_"),
8.9 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
8.10 + Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
8.11
8.12 Calc ("Atools.ident",eval_ident "#ident_")],
8.13 scr = Script ((term_of o the o (parse thy))
8.14 @@ -277,8 +277,8 @@
8.15 Calc ("NthRoot.sqrt",eval_sqrt "#sqrt_"),
8.16 Calc ("Atools.pow" ,eval_binop "#power_"),
8.17
8.18 - Calc ("op <",eval_equ "#less_"),
8.19 - Calc ("op <=",eval_equ "#less_equal_"),
8.20 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
8.21 + Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
8.22
8.23 Calc ("Atools.ident",eval_ident "#ident_")],
8.24 scr = Script ((term_of o the o (parse thy))
8.25 @@ -489,8 +489,8 @@
8.26 ("DIVIDE" ,("Rings.inverse_class.divide" ,eval_cancel "#divide_e")),
8.27 ("POWER" ,("Atools.pow" ,eval_binop "#power_")),
8.28 ("is_const",("Atools.is'_const",eval_const "#is_const_")),
8.29 - ("le" ,("op <" ,eval_equ "#less_")),
8.30 - ("leq" ,("op <=" ,eval_equ "#less_equal_")),
8.31 + ("le" ,("Orderings.ord_class.less" ,eval_equ "#less_")),
8.32 + ("leq" ,("Orderings.ord_class.less_eq" ,eval_equ "#less_equal_")),
8.33 ("ident" ,("Atools.ident",eval_ident "#ident_")),
8.34 (*von hier (ehem.SqRoot*)
8.35 ("sqrt" ,("NthRoot.sqrt" ,eval_sqrt "#sqrt_")),
9.1 --- a/src/Tools/isac/ProgLang/calculate.sml Tue Oct 05 14:41:16 2010 +0200
9.2 +++ b/src/Tools/isac/ProgLang/calculate.sml Tue Oct 05 15:28:32 2010 +0200
9.3 @@ -178,11 +178,11 @@
9.4 > Syntax.string_of_term (thy2ctxt thy) t';
9.5 >
9.6 > val t = (term_of o the o (parse thy)) "#0 < #4";
9.7 -> val eval_fn = the (assoc (!eval_list, "op <"));
9.8 -> val (SOME (id,t')) = get_pair thy "op <" eval_fn t;
9.9 +> val eval_fn = the (assoc (!eval_list, "Orderings.ord_class.less"));
9.10 +> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
9.11 > Syntax.string_of_term (thy2ctxt thy) t';
9.12 > val t = (term_of o the o (parse thy)) "#0 < #-4";
9.13 -> val (SOME (id,t')) = get_pair thy "op <" eval_fn t;
9.14 +> val (SOME (id,t')) = get_pair thy "Orderings.ord_class.less" eval_fn t;
9.15 > Syntax.string_of_term (thy2ctxt thy) t';
9.16 >
9.17 > val t = (term_of o the o (parse thy)) "#3 is_const";
9.18 @@ -240,16 +240,16 @@
9.19 val it = SOME ("sqrt_9_","sqrt 9 = 3 [sqrt 9 = 3]") : (string * thm) option
9.20
9.21 > val ct = (the o (parse thy)) "#4<#4";
9.22 -> get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;fun is_no str = (hd o explode) str = "#";
9.23 +> get_calculation_ thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;fun is_no str = (hd o explode) str = "#";
9.24
9.25 val it = SOME ("less_5_4","(5 < 4) = False [(5 < 4) = False]")
9.26
9.27 > val ct = (the o (parse thy)) "a<#4";
9.28 -> get_calculation_ thy ("op <",the (assoc(!eval_list,"op <"))) ct;
9.29 +> get_calculation_ thy ("Orderings.ord_class.less",the (assoc(!eval_list,"Orderings.ord_class.less"))) ct;
9.30 val it = NONE : (string * thm) option
9.31
9.32 > val ct = (the o (parse thy)) "#5<=#4";
9.33 -> get_calculation_ thy ("op <=",the (assoc(!eval_list,"op <="))) ct;
9.34 +> get_calculation_ thy ("Orderings.ord_class.less_eq",the (assoc(!eval_list,"Orderings.ord_class.less_eq"))) ct;
9.35 val it = SOME ("less_equal_5_4","(5 <= 4) = False [(5 <= 4) = False]")
9.36
9.37 -------------------------------------------------------------------6.8.02:
10.1 --- a/src/Tools/isac/ProgLang/termC.sml Tue Oct 05 14:41:16 2010 +0200
10.2 +++ b/src/Tools/isac/ProgLang/termC.sml Tue Oct 05 15:28:32 2010 +0200
10.3 @@ -612,8 +612,8 @@
10.4 | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
10.5 | calc "Atools.pow"(n1, n2) = power n1 n2
10.6 | calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*)
10.7 -fun calc_equ "op <" (n1, n2) = n1 < n2
10.8 - | calc_equ "op <=" (n1, n2) = n1 <= n2
10.9 +fun calc_equ "Orderings.ord_class.less" (n1, n2) = n1 < n2
10.10 + | calc_equ "Orderings.ord_class.less_eq" (n1, n2) = n1 <= n2
10.11 | calc_equ op_ _ =
10.12 error ("calc_equ: operator = "^op_^" not defined");
10.13 fun sqrt (n:int) = if n < 0 then 0
11.1 --- a/src/Tools/isac/Test_Isac.thy Tue Oct 05 14:41:16 2010 +0200
11.2 +++ b/src/Tools/isac/Test_Isac.thy Tue Oct 05 15:28:32 2010 +0200
11.3 @@ -93,7 +93,11 @@
11.4 *}
11.5
11.6 ML {*
11.7 +str2term "1 = (2 :: real)";
11.8 str2term "1 < (2 :: real)";
11.9 +str2term "1 <= (2 :: real)";
11.10 +str2term "a & b";
11.11 +str2term "a | b";
11.12 *}
11.13
11.14 use"../../../test/Tools/isac/Knowledge/rational.sml"
12.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml Tue Oct 05 14:41:16 2010 +0200
12.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml Tue Oct 05 15:28:32 2010 +0200
12.3 @@ -140,7 +140,7 @@
12.4 rew_ord = ("termlessI",termlessI),
12.5 erls = append_rls "erls_in_srls_IntegrierenUnd.." e_rls
12.6 [(*for asm in nth_Cons_ ...*)
12.7 - Calc ("op <",eval_equ "#less_"),
12.8 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
12.9 (*2nd nth_Cons_ pushes n+-1 into asms*)
12.10 Calc("Groups.plus_class.plus", eval_binop "#add_")
12.11 ],
13.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue Oct 05 14:41:16 2010 +0200
13.2 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Oct 05 15:28:32 2010 +0200
13.3 @@ -73,8 +73,8 @@
13.4 Calc ("Groups.times_class.times",eval_binop "#mult_"),
13.5 Calc ("Atools.pow" ,eval_binop "#power_"),
13.6
13.7 - Calc ("op <",eval_equ "#less_"),
13.8 - Calc ("op <=",eval_equ "#less_equal_"),
13.9 + Calc ("Orderings.ord_class.less",eval_equ "#less_"),
13.10 + Calc ("Orderings.ord_class.less_eq",eval_equ "#less_equal_"),
13.11
13.12 Calc ("Atools.ident",eval_ident "#ident_")],
13.13 scr = Script ((term_of o the o (parse thy))