1.1 --- a/test/Tools/isac/ProgLang/evaluate.sml	Sun Aug 22 11:42:55 2021 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/evaluate.sml	Sun Aug 22 14:28:38 2021 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  "----------- calculate (2 * x is_num) -------------------";
     1.5  "----------- fun get_pair: examples ------------------------------------------------------------";
     1.6  "----------- fun adhoc_thm: examples -----------------------------------------------------------";
     1.7 +"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
     1.8  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
     1.9  "----------- fun power -------------------------------------------------------------------------";
    1.10  "----------- fun divisors ----------------------------------------------------------------------";
    1.11 @@ -455,6 +456,47 @@
    1.12  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.13  then () else error "adhoc_thm  (\<not> (4 + (4 * x + x ^ 2) =!= 0))  changed";
    1.14  
    1.15 +"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
    1.16 +"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
    1.17 +"----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------";
    1.18 +val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : eval_fn);
    1.19 +val t = @{term "- 1 / 2 ::real"};
    1.20 +(* 
    1.21 +  ML\<open>Eval.adhoc_thm\<close> is called while searching terms for adjacent numerals 
    1.22 +  given a certain ML_type\<open>eval_fn\<close> and a certain  ML\<open>term\<close> ..
    1.23 +
    1.24 +  THE ERROR WAS:
    1.25 +    rew_once:
    1.26 +    Eval.get_pair for \<^const_name>\<open>divide\<close> \<longrightarrow> SOME (_, "- 1 / 2 = - 1 / 2")
    1.27 +    but rewrite__ on "x = - 0 \<or> x = - 1 / 2" \<longrightarrow> NONE
    1.28 +
    1.29 +  STEP-INTO BEVORE REMOVING THE ERROR:
    1.30 +val SOME ("#divide_e~1_2", adhoc_thm) =
    1.31 +      Eval.adhoc_thm @{theory} eval_ t;
    1.32 +"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
    1.33 +val SOME
    1.34 +    ("#divide_e~1_2", t'') =
    1.35 +  (*case*) get_pair thy op_ eval_fn t (*of*);
    1.36 +(*
    1.37 +  get_pair finds two adjacent numerals and does NOT distinguish between different kinds of 
    1.38 +  \<^ML_type>\<open>eval_fn\<close>. In case of \<^ML>\<open>eval_cancel\<close> the return value WAS the same as the input..
    1.39 +*)
    1.40 +(*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2"
    1.41 +*)
    1.42 +
    1.43 +val NONE =
    1.44 +           adhoc_thm @{theory} eval_ t;
    1.45 +"~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t);
    1.46 +val SOME ("#divide_e~1_2", t') =
    1.47 +  (*case*) get_pair thy op_ eval_fn t (*of*);
    1.48 +
    1.49 +(*+*)UnparseC.term t = "- 1 / 2";
    1.50 +(*+*)UnparseC.term t' = "- 1 / 2 = - 1 / 2"; "HOL.Trueprop";
    1.51 +
    1.52 +if t = (TermC.rhs o HOLogic.dest_Trueprop) t' 
    1.53 +then () else error "fun adhoc_thm + fun eval_cancel CHANGED";
    1.54 +
    1.55 +
    1.56  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
    1.57  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
    1.58  "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";