1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Mon Sep 13 16:01:48 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Tue Sep 14 12:22:57 2021 +0200
     1.3 @@ -300,41 +300,21 @@
     1.4  "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
     1.5  "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
     1.6  "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
     1.7 -val (t1, t2) = (@{term 3}, @{term "2::real"});
     1.8 +val t = @{term "2 + 3 ::real"};
     1.9  
    1.10 -"~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2));
    1.11 -    val (Const (\<^const_name>\<open>numeral\<close>, _) $ n1) = t1;
    1.12 -    val (Const (\<^const_name>\<open>numeral\<close>, _) $ n2) = t2;
    1.13 -    val (T, _) = HOLogic.dest_number t1
    1.14 -    val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2)
    1.15 -    val result =
    1.16 -      case op_ of
    1.17 -        "Groups.plus_class.plus" => i1 + i2
    1.18 -      | "Groups.minus_class.minus" => i1 - i2
    1.19 -      | "Groups.times_class.times" => i1 * i2
    1.20 -      | "Transcendental.powr" => power i1 i2
    1.21 -      | str => raise ERROR ("calcul not impl.for op_ " ^ str)
    1.22 -  (*in*)
    1.23 -    val xxx = HOLogic.mk_number T result;
    1.24 -  (*end*)
    1.25 -case HOLogic.dest_number xxx of
    1.26 -  (_, 5) => ()
    1.27 -| _ => error "calcul + 2 3 CHANGED";
    1.28 +"~~~~~ fun calcul , args:"; val (thy, lhs) = (@{theory}, t);
    1.29 +    val simp_ctxt =
    1.30 +      Proof_Context.init_global thy
    1.31 +      |> put_simpset (Simplifier.simpset_of @{theory_context Complex_Main});
    1.32 +    val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs);
    1.33  
    1.34 -case HOLogic.dest_number (calcul "Groups.minus_class.minus" (t1, t2)) of
    1.35 -  (_, 1) => xxx
    1.36 -| _ => error "calcul - 2 3 CHANGED";
    1.37 +if ThmC.string_of_thm eq = "2 + 3 \<equiv> 5" then () else error "calcul 1";
    1.38  
    1.39 -case HOLogic.dest_number (calcul "Groups.times_class.times" (t1, t2)) of
    1.40 -  (_, 6) => xxx
    1.41 -| _ => error "calcul - 2 3 CHANGED";
    1.42 +    val rhs = Thm.term_of (Thm.rhs_of eq);
    1.43 +    val _ = \<^assert> (is_num rhs);
    1.44  
    1.45 -(*                       (calcul "Rings.divide_class.divide" (t1, t2)
    1.46 -ERROR: calcul not impl.for op_ Rings.divide_class.divide*)
    1.47 -
    1.48 -case HOLogic.dest_number (calcul "Transcendental.powr" (t1, t2)) of
    1.49 -  (_, 9) => xxx
    1.50 -| _ => error "calcul - 2 3 CHANGED";
    1.51 +(*return value*) rhs;
    1.52 +if TermC.to_string rhs = "5" then () else error "calcul 2";
    1.53  
    1.54  
    1.55  "----------- get_pair with 3 args --------------------------------";