(* Title:  "Interpret/lucas-interpreter.sml"

    Author: Walther Neuper

    (c) due to copyright terms

 *)

 "-----------------------------------------------------------------------------------------------";

 "table of contents -----------------------------------------------------------------------------";

 "-----------------------------------------------------------------------------------------------";

 "----------- note on new realpow ------- -------------------------------------------------------";

 "-----------------------------------------------------------------------------------------------";

 "-----------------------------------------------------------------------------------------------";

 "-----------------------------------------------------------------------------------------------";

 "----------- note on new realpow ------- -------------------------------------------------------";

 "----------- note on new realpow ------- -------------------------------------------------------";

 "----------- note on new realpow ------- -------------------------------------------------------";

 (* these and other numeral calculations have been accomplished by Simplifier.rewrite so far *)

 val t = Calc_Binop.simplify @{context} @{term "4 * - 1 * 4 ::real"};

 if UnparseC.term @{context} t =    "- 16"

 then () else error "calcul  4 * - 1 * 4 \<longrightarrow> - 16";

 (*

   guess: simp_ctxt is not sufficient for simplifying the conditions in the definition -- RIGHT.

   note: missing cases, defined in lemma realpow_uminus_simps, go via [simp] into simp_ctxt.

 *)

 val t = Calc_Binop.simplify @{context} @{term "4 \<up> 2 ::real"};

 if UnparseC.term @{context} t = "16"

 then () else error    "calcul  4 \<up> 2 \<longrightarrow> 16";

 val t = Calc_Binop.simplify @{context} @{term "(- 1) \<up> 2"};

 if UnparseC.term @{context} t =  "1"

 then () else error "calcul  (- 1) \<up> 2 \<longrightarrow> 1";

 val t = Calc_Binop.simplify @{context} @{term "3 \<up> (- 2)"};

 if UnparseC.term @{context} t =  "1 / 9"

 then () else error "calcul  3 \<up> (- 2) \<longrightarrow> 1 / 9";

 val t = Calc_Binop.simplify @{context} @{term "3 \<up> - 1"};

 if UnparseC.term @{context} t = "1 / 3"

 then () else error  "calcul  3 \<up> - 1 \<longrightarrow> 1 / 3";

 (* note on example "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" *)

 (*

   fun Calc_Binop.simplify should simplify both sides of the inequality. 

   Afterwards the inequality  - 64 \<le> 8  should evaluate to True.

   But we get the error:

     rew_once: 

     Eval.get_pair for "BaseDefinitions.realpow" \<longrightarrow> SOME (_, "4 \<up> 2 = 4 \<up> 2")

     but rewrite__ on "4 * - 1 * 4 \<up> 2 \<le> 8 * (- 1) \<up> 2" \<longrightarrow> NONE

   The error occurs while rewriting and expecting \<longrightarrow> SOME (_, "4 \<up> 2 = 16");

   the rewriter takes the rhs 4 \<up> 2, the same as the lhs, 

   and assumes to be able to simplify, but we have lhs = rhs \<longrightarrow> NONE, 

   which is recognised by the rewriter as an error.

   Eval.get_pair ensures, that only pairs of numerals are passed to fun Calc_Binop.simplify,

   such that single-stepping is realised, although Simplifier.rewrite could do all at once.

   \<le> is a binary operator, too, but has another signature as algebraic operations.

   So \<le> is handled separately and not by fun Calc_Binop.simplify.

 *)