1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Fri Jul 16 07:45:06 2021 +0200
1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Sat Jul 17 14:05:28 2021 +0200
1.3 @@ -15,13 +15,13 @@
1.4 "----------- calculate check test-root-equ --------------";
1.5 "----------- check calculate bottom up -----------------";
1.6 "----------- Prog_Expr.pow Power.power_class.power ---------";
1.7 -" ================= evaluate.sml: calculate_ 2002 ======";
1.8 "----------- fun cancel_int --------------------------------------------------------------------";
1.9 "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
1.10 "----------- get_pair with 3 args -----------------------";
1.11 "----------- calculate (2 * x is_const) -----------------";
1.12 "----------- fun get_pair: examples ------------------------------------------------------------";
1.13 "----------- fun adhoc_thm: examples -----------------------------------------------------------";
1.14 +"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
1.15 "----------- fun power -------------------------------------------------------------------------";
1.16 "----------- fun divisors ----------------------------------------------------------------------";
1.17 "----------- fun doubles, fun squfact ----------------------------------------------------------";
1.18 @@ -108,23 +108,23 @@
1.19 "----------- calculate check test-root-equ --------------";
1.20 (*(1): 2nd Test_simplify didn't work:
1.21 val ct =
1.22 - "sqrt (x \<up> 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
1.23 + "sqrt (x \<up> 2 + -3 * x) = (-3 + 2 * x + - 1 * (9 + 4 * x)) / (- 1 * 2)"
1.24 > val rls = ("Test_simplify");
1.25 > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
1.26 val ct = "sqrt (x \<up> 2 + -3 * x) =
1.27 -(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
1.28 +(-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))";
1.29 ie. cancel does not work properly
1.30 *)
1.31 val thy = @{theory "Test"};
1.32 val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
1.33 val ct = ThmC_Def.num_to_Free @{term
1.34 - "sqrt (x \<up> 2 + -3 * x) = (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"};
1.35 + "sqrt (x \<up> 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"};
1.36 case calculate_ thy op_ ct of
1.37 SOME _ => ()
1.38 | NONE => error "calculate_ test-root-equ changed";
1.39 (*
1.40 sqrt (x \<up> 2 + -3 * x) =\
1.41 - \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))
1.42 + \(-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))
1.43 ............... does not work *)
1.44
1.45 (*--------------(2): does divide work in Test_simplify ?: ------*)
1.46 @@ -173,11 +173,11 @@
1.47 Rewrite.trace_on:=false; (*=true3.6.03*)
1.48
1.49 (*--- Rewrite.trace_on before correction of ... --------------------
1.50 - val ct = "(-3 + 2 * x + -1) / 2";
1.51 + val ct = "(-3 + 2 * x + - 1) / 2";
1.52 val (ct,_) = the (rewrite_set thy' false rls ct);
1.53 :
1.54 ### trying thm 'root_ge0_2'
1.55 -### rewrite_set_: x + (-1 + -3) / 2
1.56 +### rewrite_set_: x + (- 1 + -3) / 2
1.57 ### trying thm 'radd_real_const_eq'
1.58 ### trying thm 'radd_real_const'
1.59 ### rewrite_set_: x + (-4) / 2
1.60 @@ -185,27 +185,27 @@
1.61 :
1.62 "x + (-4) / 2"
1.63 -------------------------------------while before Isabelle20002:
1.64 - val ct = "(#-3 + #2 * x + #-1) // #2";
1.65 + val ct = "(#-3 + #2 * x + #- 1) // #2";
1.66 val (ct,_) = the (rewrite_set thy' false rls ct);
1.67 :
1.68 ### trying thm 'root_ge0_2'
1.69 -### rewrite_set_: x + (#-1 + #-3) // #2
1.70 +### rewrite_set_: x + (#- 1 + #-3) // #2
1.71 ### trying thm 'radd_real_const_eq'
1.72 ### trying thm 'radd_real_const'
1.73 ### rewrite_set_: x + #-4 // #2
1.74 -### rewrite_set_: x + #-2
1.75 +### rewrite_set_: x + #- 2
1.76 ### trying thm 'rcollect_right'
1.77 :
1.78 -"#-2 + x"
1.79 +"#- 2 + x"
1.80 -----------------------------------------------------------------*)
1.81
1.82
1.83 (*===================*)
1.84 Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
1.85 - val t = (Thm.term_of o the o (TermC.parse thy)) "x + (-1 + -3) / 2";
1.86 + val t = (Thm.term_of o the o (TermC.parse thy)) "x + (- 1 + -3) / 2";
1.87 val SOME (res, []) = rewrite_set_ thy false rls t;
1.88 (*WAS "x + - 2" WITH OLD numerals TOODOO?*)
1.89 -if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (-1 + -3) / 2 changed";
1.90 +if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_ x + (- 1 + -3) / 2 changed";
1.91 "x + (-4) / 2";
1.92 (*
1.93 ### trying calc. 'cancel'
1.94 @@ -344,7 +344,7 @@
1.95 (thy, "EqSystem.occur_exactly_in",
1.96 assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
1.97 TermC.str2term
1.98 - "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L \<up> 2) / 2"
1.99 + "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2"
1.100 );
1.101 val SOME (str, simpl) = get_pair thy op_ ef arg;
1.102 if str =
1.103 @@ -393,10 +393,10 @@
1.104
1.105 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
1.106
1.107 -val t = @{term "-4 / -2 :: real"};
1.108 +val t = @{term "-4 / - 2 :: real"};
1.109 val SOME (str, term) = get_pair thy isa_str eval_fn t;
1.110 if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2"
1.111 -then () else error "get_pair -4 / -2 changed";
1.112 +then () else error "get_pair -4 / - 2 changed";
1.113
1.114 val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
1.115
1.116 @@ -455,6 +455,27 @@
1.117 if str = "#ident_(4 + (4 * x + x \<up> 2))_(0)" andalso ThmC_Def.string_of_thm thm = "(4 + (4 * x + x \<up> 2) =!= 0) = False"
1.118 then () else error "adhoc_thm (\<not> (4 + (4 * x + x ^ 2) =!= 0)) changed";
1.119
1.120 +"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
1.121 +"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
1.122 +"----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
1.123 +val t = TermC.str2term "sqrt 4";
1.124 +
1.125 +(* TODO.ThmC.numerals_to_Free 1 * )
1.126 + exception TYPE raised (line 169 of "consts.ML"): Illegal type
1.127 + for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
1.128 + Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t
1.129 +( **)
1.130 +"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
1.131 + ((ThyC.get_theory "Isac_Knowledge"),
1.132 + ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> theory -> (string * term) option), t);
1.133 +val SOME (thmid, t) =
1.134 + (*case*) get_pair thy op_ eval_fn ct (*of*);
1.135 +(** )
1.136 + exception TYPE raised (line 169 of "consts.ML"): Illegal type
1.137 + for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
1.138 + Skip_Proof.make_thm thy t
1.139 +( **)
1.140 +
1.141 "----------- fun power -------------------------------------------------------------------------";
1.142 "----------- fun power -------------------------------------------------------------------------";
1.143 "----------- fun power -------------------------------------------------------------------------";