1.1 --- a/TODO.md Thu Aug 04 16:48:37 2022 +0200
1.2 +++ b/TODO.md Fri Aug 05 08:45:37 2022 +0200
1.3 @@ -67,7 +67,6 @@
1.4
1.5 ***** priority of WN items is top down, most urgent/simple on top
1.6
1.7 -* WN: add signature EXAMPLE
1.8 * WN: MethodC.from_store throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument
1.9
1.10 * WN: rewriting with ctxt not complete (cause errors hard to indentify later)
2.1 --- a/src/Tools/isac/BaseDefinitions/example.sml Thu Aug 04 16:48:37 2022 +0200
2.2 +++ b/src/Tools/isac/BaseDefinitions/example.sml Fri Aug 05 08:45:37 2022 +0200
2.3 @@ -7,10 +7,22 @@
2.4 and re-uses Store.
2.5 *)
2.6
2.7 +signature EXAMPLE =
2.8 +sig
2.9 + type description
2.10 + type T
2.11 + val empty: T
2.12
2.13 -
2.14 + type id = References_Def.id
2.15 + val id_empty: id
2.16 + val id_to_string: id -> string
2.17 +
2.18 + type store = T Store.node list
2.19 + val empty_store: (string * Formalise.T) Store.node
2.20 +end
2.21 +
2.22 (**)
2.23 -structure Example(** ): REWRITE_ORDER( **) =
2.24 +structure Example(** ): EXAMPLE( **) =
2.25 struct
2.26 (**)
2.27
3.1 --- a/src/Tools/isac/BaseDefinitions/rule-def.sml Thu Aug 04 16:48:37 2022 +0200
3.2 +++ b/src/Tools/isac/BaseDefinitions/rule-def.sml Fri Aug 05 08:45:37 2022 +0200
3.3 @@ -114,7 +114,7 @@
3.4 rew_ord: rew_ord_T,(* for rules *)
3.5 erls: rule_set, (* for the conditions in rules *)
3.6 srls: rule_set, (* for evaluation of Prog_Expr *)
3.7 - calc: calc list, (* for Calculate in program, set by prep_rls' *)
3.8 + calc: calc list, (* for calculation in program, set by prep_rls' *)
3.9 rules: rule list,
3.10 errpatts: errpatID list,(* by dialog-authoring in Build_Thydata.thy *)
3.11 scr: program} (* DEPRECATED: intersteps are created on the fly now *)
4.1 --- a/src/Tools/isac/BaseDefinitions/theoryC.sml Thu Aug 04 16:48:37 2022 +0200
4.2 +++ b/src/Tools/isac/BaseDefinitions/theoryC.sml Fri Aug 05 08:45:37 2022 +0200
4.3 @@ -35,7 +35,7 @@
4.4
4.5 val last_isabelle_thy = @{theory Complex_Main}
4.6 val session_specify_names = ["Specify", "MathEngBasic", "Input_Descript",
4.7 - "ProgLang", "Auto_Prog", "Prog_Expr", "Tactical", "Prog_Tac", "Program", "ListC", "Calculate",
4.8 + "ProgLang", "Auto_Prog", "Prog_Expr", "Tactical", "Prog_Tac", "Program", "ListC", "Calc_Binop",
4.9 "BaseDefinitions", "Know_Store"]
4.10 val session_interpret_names = ["Interpret"]
4.11 (*this is troublesome since the introduction of sessions*)
5.1 --- a/src/Tools/isac/Build_Isac.thy Thu Aug 04 16:48:37 2022 +0200
5.2 +++ b/src/Tools/isac/Build_Isac.thy Fri Aug 05 08:45:37 2022 +0200
5.3 @@ -42,12 +42,12 @@
5.4 ML_file environment.sml
5.5 ( ** ) "BaseDefinitions/BaseDefinitions"( **)
5.6 (*
5.7 - theory Calculate imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.8 + theory Calc_Binop imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.9 at $ISABELLE_ISAC/ProgLang
5.10 ML_file evaluate.sml
5.11 theory ListC imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.12 theory Program imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.13 - theory Prog_Expr imports Calculate ListC Program
5.14 + theory Prog_Expr imports Calc_Binop ListC Program
5.15 theory Prog_Tac imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.16 theory Tactical imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
5.17 theory Auto_Prog imports Prog_Tac Tactical
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Tools/isac/ProgLang/Calc_Binop.thy Fri Aug 05 08:45:37 2022 +0200
6.3 @@ -0,0 +1,87 @@
6.4 +(* Title: ProgLang/Calc_Binop.thy
6.5 + Author: Walther Neuper 000301
6.6 + (c) copyright due to lincense terms.
6.7 +*)
6.8 +
6.9 +theory Calc_Binop
6.10 + imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
6.11 +begin
6.12 +
6.13 +text \<open>Abstract:
6.14 + The Isac project required floating point numbers and complex numbers in early 2000,
6.15 + before these numbers were available in Isabelle.
6.16 + Since that time numeral calculations are done by ML functions, all named eval_
6.17 + and integrated into rewriting. eval_binop below is not bound to a specific constant
6.18 + (like in Prog_Expr.thy), rather calculates results of Isabelle's binary operations + - * / ^.
6.19 +
6.20 + A specialty are the ad-hoc theorems for numeral calculations created in order to provide
6.21 + the rewrite engine with theorems as done in general.
6.22 +\<close>
6.23 +
6.24 +ML_file evaluate.sml
6.25 +
6.26 +ML \<open>
6.27 +signature CALCULATE_BINARY_OPERATION =
6.28 +sig
6.29 + val numeric: string -> string -> term -> Proof.context -> (string * term) option
6.30 +\<^isac_test>\<open>
6.31 + val is: string -> bool
6.32 + val simplify: Proof.context -> term -> term
6.33 +\<close>
6.34 +end
6.35 +
6.36 +(**)
6.37 +structure Calc_Binop(**): CALCULATE_BINARY_OPERATION(**) =
6.38 +struct
6.39 +(**)
6.40 +
6.41 +(*** evaluate binary associative operations ***)
6.42 +
6.43 +val is =
6.44 + member (op =) [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>, \<^const_name>\<open>times\<close>, \<^const_name>\<open>realpow\<close>];
6.45 +
6.46 +fun simplify ctxt lhs =
6.47 + let
6.48 + val simp_ctxt =
6.49 + ctxt |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
6.50 + val eq = Simplifier.rewrite simp_ctxt (Thm.cterm_of ctxt lhs);
6.51 + val rhs = Thm.term_of (Thm.rhs_of eq);
6.52 + in rhs end;
6.53 +
6.54 +fun numeric (_: string) (_: string) t ctxt =
6.55 + (case t of
6.56 + (opp as Const (c1, T)) $ (Const (c2, _) $ v $ t1) $ t2 => (* binary \<circ> (v \<circ> n1) \<circ> n2 *)
6.57 + if c1 = c2 andalso is c1 andalso Eval.is_num t1 andalso Eval.is_num t2 then
6.58 + let
6.59 + val opp' = Const (if c1 = \<^const_name>\<open>minus\<close> then \<^const_name>\<open>plus\<close> else c1, T);
6.60 + val res = simplify ctxt (opp' $ t1 $ t2);
6.61 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ v $ res));
6.62 + in SOME ("#: " ^ UnparseC.term prop, prop) end
6.63 + else NONE
6.64 + | (opp as Const (c1, _)) $ t1 $ (Const (c2, _) $ t2 $ v) => (* binary \<circ> n1 \<circ> (n2 \<circ> v) *)
6.65 + if c1 = c2 andalso is c1 andalso c1 <> \<^const_name>\<open>minus\<close>
6.66 + andalso Eval.is_num t1 andalso Eval.is_num t2
6.67 + then
6.68 + let
6.69 + val res = simplify ctxt (opp $ t1 $ t2);
6.70 + val prop = HOLogic.Trueprop $ HOLogic.mk_eq (t, opp $ res $ v);
6.71 + in
6.72 + SOME ("#: " ^ UnparseC.term prop, prop)
6.73 + end
6.74 + else NONE
6.75 + | Const (c, _) $ t1 $ t2 => (* binary \<circ> n1 \<circ> n2 *)
6.76 + if is c andalso Eval.is_num t1 andalso Eval.is_num t2 then
6.77 + let
6.78 + val res = simplify ctxt t;
6.79 + val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
6.80 + in
6.81 + SOME ("#: " ^ UnparseC.term prop, prop)
6.82 + end
6.83 + else NONE
6.84 + | _ => NONE);
6.85 +(**)end(**)
6.86 +\<close> ML \<open>
6.87 +\<close> ML \<open>
6.88 +\<close>
6.89 +
6.90 +end
7.1 --- a/src/Tools/isac/ProgLang/Calculate.thy Thu Aug 04 16:48:37 2022 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,87 +0,0 @@
7.4 -(* Title: ProgLang/Calculate.thy
7.5 - Author: Walther Neuper 000301
7.6 - (c) copyright due to lincense terms.
7.7 -*)
7.8 -
7.9 -theory Calculate
7.10 - imports "$ISABELLE_ISAC/BaseDefinitions/BaseDefinitions"
7.11 -begin
7.12 -
7.13 -text \<open>Abstract:
7.14 - The Isac project required floating point numbers and complex numbers in early 2000,
7.15 - before these numbers were available in Isabelle.
7.16 - Since that time numeral calculations are done by ML functions, all named eval_
7.17 - and integrated into rewriting. eval_binop below is not bound to a specific constant
7.18 - (like in Prog_Expr.thy), rather calculates results of Isabelle's binary operations + - * / ^.
7.19 -
7.20 - A specialty are the ad-hoc theorems for numeral calculations created in order to provide
7.21 - the rewrite engine with theorems as done in general.
7.22 -\<close>
7.23 -
7.24 -ML_file evaluate.sml
7.25 -
7.26 -ML \<open>
7.27 -signature CALCULATE_BINARY_OPERATION =
7.28 -sig
7.29 - val numeric: string -> string -> term -> Proof.context -> (string * term) option
7.30 -\<^isac_test>\<open>
7.31 - val is_calcul_op: string -> bool
7.32 - val calcul: Proof.context -> term -> term
7.33 -\<close>
7.34 -end
7.35 -
7.36 -(**)
7.37 -structure Calc_Binop(**): CALCULATE_BINARY_OPERATION(**) =
7.38 -struct
7.39 -(**)
7.40 -
7.41 -(*** evaluate binary associative operations ***)
7.42 -
7.43 -val is_calcul_op =
7.44 - member (op =) [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>, \<^const_name>\<open>times\<close>, \<^const_name>\<open>realpow\<close>];
7.45 -
7.46 -fun calcul ctxt lhs =
7.47 - let
7.48 - val simp_ctxt =
7.49 - ctxt |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
7.50 - val eq = Simplifier.rewrite simp_ctxt (Thm.cterm_of ctxt lhs);
7.51 - val rhs = Thm.term_of (Thm.rhs_of eq);
7.52 - in rhs end;
7.53 -
7.54 -fun numeric (_: string) (_: string) t ctxt =
7.55 - (case t of
7.56 - (opp as Const (c1, T)) $ (Const (c2, _) $ v $ t1) $ t2 => (* binary \<circ> (v \<circ> n1) \<circ> n2 *)
7.57 - if c1 = c2 andalso is_calcul_op c1 andalso Eval.is_num t1 andalso Eval.is_num t2 then
7.58 - let
7.59 - val opp' = Const (if c1 = \<^const_name>\<open>minus\<close> then \<^const_name>\<open>plus\<close> else c1, T);
7.60 - val res = calcul ctxt (opp' $ t1 $ t2);
7.61 - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, opp $ v $ res));
7.62 - in SOME ("#: " ^ UnparseC.term prop, prop) end
7.63 - else NONE
7.64 - | (opp as Const (c1, _)) $ t1 $ (Const (c2, _) $ t2 $ v) => (* binary \<circ> n1 \<circ> (n2 \<circ> v) *)
7.65 - if c1 = c2 andalso is_calcul_op c1 andalso c1 <> \<^const_name>\<open>minus\<close>
7.66 - andalso Eval.is_num t1 andalso Eval.is_num t2
7.67 - then
7.68 - let
7.69 - val res = calcul ctxt (opp $ t1 $ t2);
7.70 - val prop = HOLogic.Trueprop $ HOLogic.mk_eq (t, opp $ res $ v);
7.71 - in
7.72 - SOME ("#: " ^ UnparseC.term prop, prop)
7.73 - end
7.74 - else NONE
7.75 - | Const (c, _) $ t1 $ t2 => (* binary \<circ> n1 \<circ> n2 *)
7.76 - if is_calcul_op c andalso Eval.is_num t1 andalso Eval.is_num t2 then
7.77 - let
7.78 - val res = calcul ctxt t;
7.79 - val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
7.80 - in
7.81 - SOME ("#: " ^ UnparseC.term prop, prop)
7.82 - end
7.83 - else NONE
7.84 - | _ => NONE);
7.85 -(**)end(**)
7.86 -\<close> ML \<open>
7.87 -\<close> ML \<open>
7.88 -\<close>
7.89 -
7.90 -end
8.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Thu Aug 04 16:48:37 2022 +0200
8.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Fri Aug 05 08:45:37 2022 +0200
8.3 @@ -5,7 +5,7 @@
8.4 *)
8.5
8.6 theory Prog_Expr
8.7 - imports Calculate ListC Program
8.8 + imports Calc_Binop ListC Program
8.9 begin
8.10
8.11 text \<open>Abstract:
9.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Aug 04 16:48:37 2022 +0200
9.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Aug 05 08:45:37 2022 +0200
9.3 @@ -1096,12 +1096,12 @@
9.4 [(*for asm in NTH_CONS ...*)
9.5 Eval (\<^const_name>\<open>less\<close>,eval_equ "#less_"),
9.6 (*2nd NTH_CONS pushes n+-1 into asms*)
9.7 - Eval(\<^const_name>\<open>plus\<close>, eval_binop "#add_")
9.8 + Eval(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")
9.9 ],
9.10 srls = Rule_Set.Empty, calc = [], errpatts = [],
9.11 rules = [
9.12 Thm ("NTH_CONS",ThmC.numerals_to_Free @{thm NTH_CONS}),
9.13 - Eval(\<^const_name>\<open>plus\<close>, eval_binop "#add_"),
9.14 + Eval(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
9.15 Thm ("NTH_NIL",ThmC.numerals_to_Free @{thm NTH_NIL}),
9.16 Eval("Prog_Expr.lhs", eval_lhs"eval_lhs_"),
9.17 Eval("Prog_Expr.rhs", eval_rhs"eval_rhs_"),
10.1 --- a/test/Tools/isac/BaseDefinitions/base-definitions.sml Thu Aug 04 16:48:37 2022 +0200
10.2 +++ b/test/Tools/isac/BaseDefinitions/base-definitions.sml Fri Aug 05 08:45:37 2022 +0200
10.3 @@ -17,7 +17,7 @@
10.4
10.5 (* these and other numeral calculations have been accomplished by Simplifier.rewrite so far *)
10.6
10.7 -val t = calcul @{context} @{term "4 * - 1 * 4 ::real"};
10.8 +val t = Calc_Binop.simplify @{context} @{term "4 * - 1 * 4 ::real"};
10.9 if UnparseC.term_in_ctxt @{context} t = "- 16"
10.10 then () else error "calcul 4 * - 1 * 4 \<longrightarrow> - 16";
10.11
10.12 @@ -25,25 +25,25 @@
10.13 guess: simp_ctxt is not sufficient for simplifying the conditions in the definition -- RIGHT.
10.14 note: missing cases, defined in lemma realpow_uminus_simps, go via [simp] into simp_ctxt.
10.15 *)
10.16 -val t = calcul @{context} @{term "4 \<up> 2 ::real"};
10.17 +val t = Calc_Binop.simplify @{context} @{term "4 \<up> 2 ::real"};
10.18 if UnparseC.term_in_ctxt @{context} t = "16"
10.19 then () else error "calcul 4 \<up> 2 \<longrightarrow> 16";
10.20
10.21 -val t = calcul @{context} @{term "(- 1) \<up> 2"};
10.22 +val t = Calc_Binop.simplify @{context} @{term "(- 1) \<up> 2"};
10.23 if UnparseC.term_in_ctxt @{context} t = "1"
10.24 then () else error "calcul (- 1) \<up> 2 \<longrightarrow> 1";
10.25
10.26 -val t = calcul @{context} @{term "3 \<up> (- 2)"};
10.27 +val t = Calc_Binop.simplify @{context} @{term "3 \<up> (- 2)"};
10.28 if UnparseC.term_in_ctxt @{context} t = "1 / 9"
10.29 then () else error "calcul 3 \<up> (- 2) \<longrightarrow> 1 / 9";
10.30
10.31 -val t = calcul @{context} @{term "3 \<up> - 1"};
10.32 +val t = Calc_Binop.simplify @{context} @{term "3 \<up> - 1"};
10.33 if UnparseC.term_in_ctxt @{context} t = "1 / 3"
10.34 then () else error "calcul 3 \<up> - 1 \<longrightarrow> 1 / 3";
10.35
10.36 (* note on example "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" *)
10.37 (*
10.38 - fun calcul should simplify both sides of the inequality.
10.39 + fun Calc_Binop.simplify should simplify both sides of the inequality.
10.40 Afterwards the inequality - 64 \<le> 8 should evaluate to True.
10.41
10.42 But we get the error:
10.43 @@ -56,9 +56,9 @@
10.44 and assumes to be able to simplify, but we have lhs = rhs \<longrightarrow> NONE,
10.45 which is recognised by the rewriter as an error.
10.46
10.47 - Eval.get_pair ensures, that only pairs of numerals are passed to fun calcul,
10.48 + Eval.get_pair ensures, that only pairs of numerals are passed to fun Calc_Binop.simplify,
10.49 such that single-stepping is realised, although Simplifier.rewrite could do all at once.
10.50
10.51 \<le> is a binary operator, too, but has another signature as algebraic operations.
10.52 - So \<le> is handled separately and not by fun calcul.
10.53 + So \<le> is handled separately and not by fun Calc_Binop.simplify.
10.54 *)
11.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-present.sml Thu Aug 04 16:48:37 2022 +0200
11.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-present.sml Fri Aug 05 08:45:37 2022 +0200
11.3 @@ -130,10 +130,10 @@
11.4 if Rule_Set.contains r1 Test_simplify then ()
11.5 else error "rewtools.sml Rule_Set.contains Thm";
11.6
11.7 -val r1 = Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_");
11.8 +val r1 = Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_");
11.9 if Rule_Set.contains r1 Test_simplify then ()
11.10 else error "rewtools.sml Rule_Set.contains Eval";
11.11
11.12 -val r1 = Eval (\<^const_name>\<open>minus\<close>, eval_binop "#add_");
11.13 +val r1 = Eval (\<^const_name>\<open>minus\<close>, Calc_Binop.numeric "#add_");
11.14 if not (Rule_Set.contains r1 Test_simplify) then ()
11.15 else error "rewtools.sml Rule_Set.contains Eval";
12.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml Thu Aug 04 16:48:37 2022 +0200
12.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml Fri Aug 05 08:45:37 2022 +0200
12.3 @@ -60,11 +60,11 @@
12.4 [(*for asm in NTH_CONS ...*)
12.5 Eval ("Orderings.ord_class.less",eval_equ "#less_"),
12.6 (*2nd NTH_CONS pushes n+- 1 into asms*)
12.7 - Eval("Groups.plus_class.plus", eval_binop "#add_")
12.8 + Eval("Groups.plus_class.plus", Calc_Binop.numeric "#add_")
12.9 ],
12.10 srls = Rule_Set.Empty, calc = [], errpatts = [],
12.11 rules = [Thm ("NTH_CONS", @{thm NTH_CONS}),
12.12 - Eval("Groups.plus_class.plus", eval_binop "#add_"),
12.13 + Eval("Groups.plus_class.plus", Calc_Binop.numeric "#add_"),
12.14 Thm ("NTH_NIL", @{thm NTH_NIL}),
12.15 Eval("Prog_Expr.lhs", eval_lhs "eval_lhs_"),
12.16 Eval("Prog_Expr.rhs", eval_rhs "eval_rhs_"),
13.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Thu Aug 04 16:48:37 2022 +0200
13.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Fri Aug 05 08:45:37 2022 +0200
13.3 @@ -34,7 +34,7 @@
13.4 if p = ([], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term) =
13.5 "[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 + - 24 * L * c_3 + 12 * L \<up> 2 * c_2 + 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n - 24,\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
13.6 (*"[0 = - 1 * c_4 / - 1,\n 0 =\n (- 24 * c_4 * EI + - 24 * L * c_3 * EI + 12 * L \<up> 2 * c_2 +\n 4 * L \<up> 3 * c +\n - 1 * L \<up> 4 * q_0) /\n (- 24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + - 1 * L \<up> 2 * q_0) / 2]"
13.7 - ^^^ BEFORE fun calcul IS EVALUATEDO BY Simplifier.rewrite *)
13.8 + ^^^ BEFORE fun Calc_Binop.simplify IS EVALUATEDO BY Simplifier.rewrite *)
13.9 then () else error "auto method [Biegelinien,setzeRandbedingungenEin] changed";
13.10
13.11
13.12 @@ -83,7 +83,7 @@
13.13 case nxt of Check_Postcond ["makeFunctionTo", "equation"] => ()
13.14 | _ => error "biegelinie.sml met2 gg";
13.15
13.16 -(*========== inhibit exn WN210927 exception size SINCE BEFORE fun calcul WITH Simplifier.rewrite
13.17 +(*========== inhibit exn WN210927 exception size SINCE BEFORE fun Calc_Binop.simplify WITH Simplifier.rewrite
13.18 "--- before 2.subpbl [Equation, fromFunction]";
13.19 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_4 + 0 / (- 1 * EI)" ;
13.20 case nxt of Subproblem (_, ["makeFunctionTo", "equation"]) => ()
13.21 @@ -117,13 +117,13 @@
13.22
13.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.24 if f2str f = "0 = - 1 * c_4 / - 1"
13.25 - (*"M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2" BEFORE fun calcul WITH Simplifier.rewrite*)
13.26 + (*"M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2" BEFORE fun Calc_Binop.simplify WITH Simplifier.rewrite*)
13.27 then () else error "Method fromFunction CHANGED 1";
13.28
13.29 val (p,_,f,nxt,_,pt) = me nxt p c pt;
13.30 val Test_Out.PpcKF (Test_Out.Problem [], {Find = [], Given = [], Relate = [],
13.31 Where = [], With = []}) = f;
13.32 -( *========== inhibit exn WN210927 BEFORE fun calcul WITH Simplifier.rewrite ========
13.33 +( *========== inhibit exn WN210927 BEFORE fun Calc_Binop.simplify WITH Simplifier.rewrite ========
13.34 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
13.35 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f = "0 = c_2";
13.36 val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.1 --- a/test/Tools/isac/Knowledge/eqsystem-1.sml Thu Aug 04 16:48:37 2022 +0200
14.2 +++ b/test/Tools/isac/Knowledge/eqsystem-1.sml Fri Aug 05 08:45:37 2022 +0200
14.3 @@ -86,7 +86,7 @@
14.4 val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty
14.5 [(Thm ("LENGTH_NIL", @{thm LENGTH_NIL})),
14.6 (Thm ("LENGTH_CONS", @{thm LENGTH_CONS})),
14.7 - Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_"),
14.8 + Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"),
14.9 Eval (\<^const_name>\<open>HOL.eq\<close>,eval_equal "#equal_")
14.10 ];
14.11 val SOME (t',_) = rewrite_set_ ctxt false testrls t;
14.12 @@ -382,7 +382,7 @@
14.13 ##### try calc: op <'
14.14 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + - 1"]
14.15
14.16 -... i.e Eval ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
14.17 +... i.e Eval ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") was missing in erls_prls_triangular*)
14.18 (*--------------------------------------------------------------------------------------------//*)
14.19
14.20
15.1 --- a/test/Tools/isac/ProgLang/auto_prog.sml Thu Aug 04 16:48:37 2022 +0200
15.2 +++ b/test/Tools/isac/ProgLang/auto_prog.sml Fri Aug 05 08:45:37 2022 +0200
15.3 @@ -246,7 +246,7 @@
15.4 if UnparseC.term t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
15.5 else error "rule2stac Thm.. changed";
15.6
15.7 -val t = rule2stac @{theory} (Eval (\<^const_name>\<open>plus\<close>, eval_binop "#add_"));
15.8 +val t = rule2stac @{theory} (Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"));
15.9 if UnparseC.term t = "Try (Repeat (Calculate ''PLUS''))" then ()
15.10 else error "rule2stac Eval.. changed";
15.11
16.1 --- a/test/Tools/isac/ProgLang/calculate.sml Thu Aug 04 16:48:37 2022 +0200
16.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Fri Aug 05 08:45:37 2022 +0200
16.3 @@ -6,17 +6,17 @@
16.4 "-----------------------------------------------------------------------------------------------";
16.5 "table of contents -----------------------------------------------------------------------------";
16.6 "-----------------------------------------------------------------------------------------------";
16.7 -"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
16.8 +"----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";
16.9 "-----------------------------------------------------------------------------------------------";
16.10 "-----------------------------------------------------------------------------------------------";
16.11 "-----------------------------------------------------------------------------------------------";
16.12
16.13 -"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
16.14 -"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
16.15 -"----------- RE-BUILD fun eval_binop -----------------------------------------------------------";
16.16 +"----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";
16.17 +"----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";
16.18 +"----------- RE-BUILD fun Calc_Binop.numeric -----------------------------------------------------------";
16.19
16.20 fun test thy t =
16.21 - writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, calcul @{context} t)));
16.22 + writeln (Syntax.string_of_term_global thy (Logic.mk_equals (t, Calc_Binop.simplify @{context} t)));
16.23
16.24 test \<^theory> \<^term>\<open>10 + 20 :: real\<close>;
16.25 test \<^theory> \<^term>\<open>10 - 20 :: real\<close>;
17.1 --- a/test/Tools/isac/ProgLang/calculate.thy Thu Aug 04 16:48:37 2022 +0200
17.2 +++ b/test/Tools/isac/ProgLang/calculate.thy Fri Aug 05 08:45:37 2022 +0200
17.3 @@ -38,10 +38,10 @@
17.4 (["Test", "test_calculate"],
17.5 [("#Given" , ["realTestGiven t_t"]), ("#Find", ["realTestFind s_s"])],
17.6 {rew_ord'="sqrt_right",rls'=tval_rls,srls = Rule_Set.empty, prls = Rule_Set.empty,
17.7 - calc=[("PLUS", (\<^const_name>\<open>plus\<close>, eval_binop "#add_")),
17.8 - ("TIMES", (\<^const_name>\<open>times\<close>, eval_binop "#mult_")),
17.9 + calc=[("PLUS", (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
17.10 + ("TIMES", (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
17.11 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_")),
17.12 - ("POWER", (\<^const_name>\<open>realpow\<close>, eval_binop "#power_"))],
17.13 + ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))],
17.14 crls=tval_rls, errpats = [], nrls= Rule_Set.empty (*, asm_rls=[],asm_thm=[]*)},
17.15 @{thm calc_test.simps})]
17.16 \<close>
18.1 --- a/test/Tools/isac/ProgLang/evaluate.sml Thu Aug 04 16:48:37 2022 +0200
18.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml Fri Aug 05 08:45:37 2022 +0200
18.3 @@ -17,7 +17,7 @@
18.4 "----------- check calculate bottom up -----------------";
18.5 "----------- Prog_Expr.pow Power.power_class.power ---------";
18.6 "----------- fun cancel_int --------------------------------------------------------------------";
18.7 -"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
18.8 +"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
18.9 "----------- get_pair with 3 args -----------------------";
18.10 "----------- calculate (2 * x is_num) -------------------";
18.11 "----------- fun get_pair: examples ------------------------------------------------------------";
18.12 @@ -49,10 +49,10 @@
18.13 val t = TermC.str2term "((1+2)*4/3) \<up> 2";
18.14 val thy = @{theory};
18.15 val ctxt = Proof_Context.init_global @{theory}
18.16 -val times = ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
18.17 -val plus = ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn;
18.18 +val times = ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval_Def.eval_fn;
18.19 +val plus = ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval_Def.eval_fn;
18.20 val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
18.21 -val pow = (\<^const_name>\<open>realpow\<close>, eval_binop "#power_") : string * Eval_Def.eval_fn;
18.22 +val pow = (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_") : string * Eval_Def.eval_fn;
18.23
18.24 "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
18.25 val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
18.26 @@ -279,7 +279,7 @@
18.27 Const (\<^const_name>\<open>realpow\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
18.28 (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
18.29 | _ => error "3 \<up> 2 CHANGED";
18.30 - val SOME (id, t') = eval_binop thmid op_ t ctxt;
18.31 + val SOME (id, t') = Calc_Binop.numeric thmid op_ t ctxt;
18.32 (*** calc: operator = pow not defined*)
18.33
18.34 if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop 3 \<up> 2 = 9 CHANGED";
18.35 @@ -293,12 +293,12 @@
18.36 if cancel_int (6, 4) = (1, (3, 2)) then () else error "cancel_int (6, 4)CHANGED";
18.37
18.38
18.39 -"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
18.40 -"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
18.41 -"----------- RE-BUILD fun calcul ---------------------------------------------------------------";
18.42 +"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
18.43 +"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
18.44 +"----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------";
18.45 val t = @{term "2 + 3 ::real"};
18.46
18.47 -"~~~~~ fun calcul , args:"; val (thy, lhs) = (@{theory}, t);
18.48 +"~~~~~ fun Calc_Binop.simplify , args:"; val (thy, lhs) = (@{theory}, t);
18.49 val simp_ctxt =
18.50 Proof_Context.init_global thy
18.51 |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions});
19.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml Thu Aug 04 16:48:37 2022 +0200
19.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml Fri Aug 05 08:45:37 2022 +0200
19.3 @@ -19,7 +19,7 @@
19.4 "-------- fun eval_sameFunId -------------------------------------------------------------------";
19.5 "-------- fun eval_filter_sameFunId ------------------------------------------------------------";
19.6 "-------- fun eval_boollist2sum ----------------------------------------------------------------";
19.7 -"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
19.8 +"-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
19.9 "-------- fun matchsub -------------------------------------------------------------------------";
19.10 "-------- fun or2list: HOL.disj HOL.eq HOL.True HOL.False etc ----------------------------------";
19.11 "-----------------------------------------------------------------------------------------------";
19.12 @@ -417,9 +417,9 @@
19.13 | _ => error "atools.sml diff.rewrite boollist2sum";
19.14
19.15
19.16 -"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
19.17 -"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
19.18 -"-------- REBUILD fun eval_binop FOR Isabelle's NUMERALS ---------------------------------------";
19.19 +"-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
19.20 +"-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
19.21 +"-------- REBUILD fun Calc_Binop.numeric FOR Isabelle's NUMERALS ---------------------------------------";
19.22 val (op_, ef) = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "TIMES"));
19.23 val t = TermC.parseNEW' ctxt "2 * (3::real)";
19.24 (*val SOME (thmid,t') = *)get_pair ctxt op_ ef t;
19.25 @@ -429,20 +429,20 @@
19.26 (*if*) op_ = op0; (*then*)
19.27 val popt =
19.28 ef op_ t ctxt;
19.29 -"~~~~~ fun eval_binop , args:"; val ((_ : string), (_: string),
19.30 +"~~~~~ fun Calc_Binop.numeric , args:"; val ((_ : string), (_: string),
19.31 (t as (Const (op0, _) $ t1 $ t2)), thy) =
19.32 ("#mult_", op_, t, thy);
19.33 val Const (c, _) $ t1 $ t2 = (* binary \<circ> n1 \<circ> n2 *)
19.34 (*case*) t (*of*);
19.35 - (*if*) is_calcul_op c andalso is_num t1 andalso is_num t2 (*then*);
19.36 - val res = calcul ctxt t;
19.37 + (*if*) Calc_Binop.is c andalso is_num t1 andalso is_num t2 (*then*);
19.38 + val res = Calc_Binop.simplify ctxt t;
19.39 val prop = HOLogic.Trueprop $ (HOLogic.mk_eq (t, res));
19.40 SOME ("#: " ^ UnparseC.term prop, prop) (*return value*);
19.41 ;
19.42 if "#: " ^ UnparseC.term prop = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
19.43 else error "eval_binop changed"
19.44 ;
19.45 -val SOME (thmid, tm) = eval_binop "#mult_" op_ t ctxt;
19.46 +val SOME (thmid, tm) = Calc_Binop.numeric "#mult_" op_ t ctxt;
19.47 if thmid = "#: 2 * 3 = 6" andalso UnparseC.term prop = "2 * 3 = 6" then ()
19.48 else error "eval_binop changed 2"
19.49