walther@59902: (* Title:  "ProgLang/evaluate.sml"
walther@60278:            test calculation of values for function constants
neuper@38022:    Author: Walther Neuper 2000
neuper@38022:    (c) copyright due to lincense terms.
neuper@37906: *)
neuper@37906: 
neuper@38022: "--------------------------------------------------------";
neuper@38022: "table of contents --------------------------------------";
neuper@38022: "--------------------------------------------------------";
neuper@55366: "-calculate.thy: provides 'setup' -----------------------";
neuper@41924: "----------- fun norm -----------------------------------";
wneuper@59255: "----------- check return value of adhoc_thm  ----";
wneuper@59411: "----------- fun calculate_ --------------------------------------------------------------------";
wneuper@59411: "----------- calculate from Prog --------------------------------- -----------------------------";
neuper@55366: "----------- calculate from script --requires 'setup'----";
neuper@38032: "----------- calculate check test-root-equ --------------";
walther@60317: "----------- check calculate bottom up -----------------";
walther@59603: "----------- Prog_Expr.pow Power.power_class.power ---------";
walther@60317: "----------- fun cancel_int --------------------------------------------------------------------";
walther@60317: "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
neuper@38032: "----------- get_pair with 3 args -----------------------";
neuper@38032: "----------- calculate (2 * x is_const) -----------------";
wneuper@59387: "----------- fun get_pair: examples ------------------------------------------------------------";
wneuper@59387: "----------- fun adhoc_thm: examples -----------------------------------------------------------";
wneuper@59403: "----------- fun power -------------------------------------------------------------------------";
wneuper@59403: "----------- fun divisors ----------------------------------------------------------------------";
wneuper@59403: "----------- fun doubles, fun squfact ----------------------------------------------------------";
neuper@38022: "--------------------------------------------------------";
neuper@38022: "--------------------------------------------------------";
neuper@38022: "--------------------------------------------------------";
neuper@37906: 
wneuper@59255: "----------- check return value of adhoc_thm  ----";
wneuper@59255: "----------- check return value of adhoc_thm  ----";
wneuper@59255: "----------- check return value of adhoc_thm  ----";
neuper@41924: val thy = @{theory "Poly"};
s1210629013@52153: val cal = snd (assoc_calc' thy "is_polyexp");
neuper@38022: val t = @{term "(x / x) is_polyexp"};
wneuper@59255: val SOME (thmID, thm) = adhoc_thm thy cal t;
wneuper@59188: (HOLogic.dest_Trueprop (Thm.prop_of thm); writeln "all thms wrapped by Trueprop")
neuper@38022: handle TERM _ => 
walther@59902:        error "evaluate.sml: adhoc_thm must return Trueprop";
neuper@38022: 
wneuper@59411: "----------- fun calculate_ --------------------------------------------------------------------";
wneuper@59411: "----------- fun calculate_ --------------------------------------------------------------------";
wneuper@59411: "----------- fun calculate_ --------------------------------------------------------------------";
wneuper@59411: (* fun rewrite__set_ \<longrightarrow> fun rew_once works the same way *)
walther@60242: val t = TermC.str2term "((1+2)*4/3) \<up> 2";
wneuper@59411: val thy = @{theory};
walther@59919: val times =  ("Groups.times_class.times", eval_binop "#mult_") : string * Eval_Def.eval_fn;
walther@60317: val plus =   ("Groups.plus_class.plus", eval_binop "#add_") : string * Eval_Def.eval_fn;
walther@60317: val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval_Def.eval_fn;
walther@60317: val pow =    ("Transcendental.powr", eval_binop "#power_") : string * Eval_Def.eval_fn;
wneuper@59411: 
walther@60317: "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t);
wneuper@59411: val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{theory} isa_fn t;
walther@59852: val SOME (t', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
walther@60242: if UnparseC.term t' = "(3 * 4 / 3) \<up> 2" then () else error "calculate_  1 + 2 = 3  changed";
wneuper@59411: 
wneuper@59411: "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t');
wneuper@59411: val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{theory} isa_fn t';
walther@59852: val SOME (t'', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
walther@60242: if UnparseC.term t'' = "(12 / 3) \<up> 2" then () else error "calculate_  3 * 4 = 12  changed";
wneuper@59411: 
wneuper@59411: "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t'');
wneuper@59411: val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{theory} isa_fn t;
walther@59852: val SOME (t''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
walther@60242: if UnparseC.term t''' = "4 \<up> 2" then () else error "calculate_  12 / 3 = 4  changed";
wneuper@59411: 
wneuper@59411: "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, pow, t''');
walther@60242: val SOME ("#: 4 \<up> 2 = 16", adh_thm) = adhoc_thm @{theory} isa_fn t;
walther@59852: val SOME (t'''', []) = rewrite__ thy 0 [] e_rew_ord Rule_Set.empty true adh_thm t;
walther@59868: if UnparseC.term t'''' = "16" then () else error "calculate_  12 / 3 = 4  changed";
wneuper@59411: 
wneuper@59411: "----------- calculate from Prog --------------------------------- -----------------------------";
wneuper@59411: "----------- calculate from Prog --------------------------------- -----------------------------";
wneuper@59411: "----------- calculate from Prog --------------------------------- -----------------------------";
neuper@41924: val thy = @{theory "Test"};
walther@60242: val fmz = ["realTestGiven (((1+2)*4/3) \<up> 2)", "realTestFind s"];
neuper@37906: val (dI',pI',mI') =
walther@60317:   ("Test", ["calculate", "test"], ["Test", "test_calculate"]);
neuper@38035: 
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@60242: (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3)  \<up> #2)")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*nxt = ("Add_Find",Add_Find "realTestFind s") : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38035: (*nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*nxt = ("Specify_Problem",Specify_Problem ["calculate", "test"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*nxt = ("Specify_Method",Specify_Method ("Test", "test_calculate"))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
walther@59997: (*nxt = ("Apply_Method",Apply_Method ("Test", "test_calculate"))*)
neuper@37906: 
walther@59713: (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "PLUS")*)
walther@59713: (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "TIMES")*)
walther@59713: (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "DIVIDE")*)
walther@59713: (*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Calculate",Calculate "POWER")*)
walther@59997: (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("Check_Postcond",Check_Postcond ["calculate", "test"])*)
walther@59713: (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [1] pt; (*nxt = ("End_Proof'",End_Proof')*)
walther@59959: case f of Test_Out.FormKF "16" => () | _ =>
walther@59902: error "evaluate.sml: script test_calculate changed behaviour";
neuper@37906: 
neuper@37906: 
neuper@38032: "----------- calculate check test-root-equ --------------";
neuper@38032: "----------- calculate check test-root-equ --------------";
neuper@38032: "----------- calculate check test-root-equ --------------";
neuper@37906: (*(1): 2nd Test_simplify didn't work:
neuper@37906: val ct =
walther@60329:   "sqrt (x \<up> 2 + -3 * x) = (-3 + 2 * x + - 1 * (9 + 4 * x)) / (- 1 * 2)"
neuper@37906: > val rls = ("Test_simplify");
neuper@37906: > val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct);
walther@60242: val ct = "sqrt (x \<up> 2 + -3 * x) =
walther@60329: (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))";
neuper@37906: ie. cancel does not work properly
neuper@37906: *)
wneuper@59382:  val thy = @{theory "Test"};
walther@59686:  val op_ = the (LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE"));
walther@60337:  val ct = @{term
walther@60329:    "sqrt (x \<up> 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"};
wneuper@59382: case calculate_ thy op_ ct of
wneuper@59382:   SOME _ => ()
wneuper@59382: | NONE => error "calculate_ test-root-equ changed";
neuper@37906: (*
walther@60242:            sqrt (x \<up> 2 + -3 * x) =\
walther@60329:  \(-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))
neuper@37906: ............... does not work *)
neuper@37906: 
neuper@37906: (*--------------(2): does divide work in Test_simplify ?: ------*)
akargl@42188:  val thy = @{theory Test};
walther@60340:  val t = (Thm.term_of o the o (TermC.parse thy)) "6 / 2";
neuper@37906:  val rls = Test_simplify;
neuper@37906:  val (t,_) = the (rewrite_set_ thy false rls t);
walther@59997: (*val t = Free ("3", "Real.real") : term*)
neuper@37906: 
neuper@37906: (*--------------(3): is_const works ?: -------------------------------------*)
walther@60340:  val t = (Thm.term_of o the o (TermC.parse @{theory Test})) "2 is_const";
walther@60230:  TermC.atomty t;
akargl@42188:  rewrite_set_ @{theory Test} false tval_rls t;
wenzelm@60309: (*val it = SOME (Const (\<^const_name>\<open>True\<close>, "bool"),[]) ... works*)
neuper@37906: 
walther@60230:  val t = TermC.str2term "2 * x is_const";
wneuper@59592:  val SOME (str,t') = eval_const "" "" t (@{theory "Isac_Knowledge"});
walther@59868:  UnparseC.term t';
neuper@37906:  
neuper@37906: 
neuper@38032: "----------- check calculate bottom up ------------------";
neuper@38032: "----------- check calculate bottom up ------------------";
neuper@38032: "----------- check calculate bottom up ------------------";
neuper@37906: (*-------------- eval_cancel works: *)
walther@60330:  Rewrite.trace_on := false; (*true false*)
akargl@42188:  val thy = @{theory Test};
wneuper@59384:  val rls = Test_simplify;
walther@60340:  val t = (Thm.term_of o the o (TermC.parse thy)) "(-4) / 2";
akargl@42188: 
wenzelm@60309: val SOME (_, t) = eval_cancel "xxx" \<^const_name>\<open>divide\<close> t thy;
akargl@42188: 
neuper@37906: (*--------------(5): reproduce (1) with simpler term: ------------*)
walther@60340:  val t = (Thm.term_of o the o (TermC.parse thy)) "(3+5)/2";
wneuper@59384: case rewrite_set_ thy false rls t of
walther@60317:   SOME (t', []) =>
walther@60317:     if UnparseC.term t' = "4" then ()
walther@60317:     else error "rewrite_set_ (3+5)/2 changed 1"
walther@60317: | _ => error "rewrite_set_ (3+5)/2 changed 2";
neuper@37906: 
walther@60340:  val t = (Thm.term_of o the o (TermC.parse thy)) "(3+1+2*x)/2";
wneuper@59384: case rewrite_set_ thy false rls t of
walther@60356:   SOME (t', _) =>
walther@60324:     if UnparseC.term t' = "2 + x" then () else error "rewrite_set_ (3+1+2*x)/2 changed 1"
walther@60317: | _ => error "rewrite_set_ (3+1+2*x)/2 changed 2";
neuper@37906: 
walther@60330:  Rewrite.trace_on := false; (*true false*)
akargl@42218: 
walther@59901: (*--- Rewrite.trace_on before correction of ... --------------------
walther@60329:  val ct = "(-3 + 2 * x + - 1) / 2";
neuper@37906:  val (ct,_) = the (rewrite_set thy'  false rls ct);
neuper@37906: :
neuper@37906: ### trying thm 'root_ge0_2'
walther@60329: ### rewrite_set_: x + (- 1 + -3) / 2
neuper@37906: ### trying thm 'radd_real_const_eq'
neuper@37906: ### trying thm 'radd_real_const'
neuper@37906: ### rewrite_set_: x + (-4) / 2
neuper@37906: ### trying thm 'rcollect_right'
neuper@37906: :
neuper@37906: "x + (-4) / 2"
neuper@37906: -------------------------------------while before Isabelle20002:
walther@60329:  val ct = "(#-3 + #2 * x + #- 1) // #2";
neuper@37906:  val (ct,_) = the (rewrite_set thy'  false rls ct);
neuper@37906: :
neuper@37906: ### trying thm 'root_ge0_2'
walther@60329: ### rewrite_set_: x + (#- 1 + #-3) // #2
neuper@37906: ### trying thm 'radd_real_const_eq'
neuper@37906: ### trying thm 'radd_real_const'
neuper@37906: ### rewrite_set_: x + #-4 // #2
walther@60329: ### rewrite_set_: x + #- 2
neuper@37906: ### trying thm 'rcollect_right'
neuper@37906: :
walther@60329: "#- 2 + x"
neuper@37906: -----------------------------------------------------------------*)
neuper@37906: 
neuper@37906: 
neuper@37906: (*===================*)
walther@59901:  Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
walther@60340:  val t = (Thm.term_of o the o (TermC.parse thy))  "x + (- 1 + -3) / 2";
wneuper@59384: val SOME (res, []) = rewrite_set_ thy false rls t;
walther@60329: if UnparseC.term res = "- 2 + x" then () else error "rewrite_set_  x + (- 1 + -3) / 2  changed";
neuper@37906: "x + (-4) / 2";						
neuper@37906: (*
neuper@37906: ### trying calc. 'cancel'
neuper@37906: @@@ get_pair: binop, t = x + (-4) / 2
neuper@37906: @@@ get_pair: t else
neuper@38032: @@@ get_pair: t else -> NONE
neuper@37906: @@@ get_pair: binop, t = (-4) / 2
neuper@37906: @@@ get_pair: then 1
neuper@38032: @@@ get_pair: t -> NONE
neuper@38032: @@@ get_pair: t1 -> NONE
wneuper@59255: @@@ adhoc_thm': NONE
neuper@37906: ### trying calc. 'pow'
neuper@37906: *)
neuper@37906: 
walther@59901:  Rewrite.trace_on:=false; (*WN130722: =true stopped Test_Isac.thy*)
neuper@37906: 
walther@59902: " ================= evaluate.sml: calculate_ 2002 =================== ";
walther@59902: " ================= evaluate.sml: calculate_ 2002 =================== ";
walther@59902: " ================= evaluate.sml: calculate_ 2002 =================== ";
neuper@37906: 
akargl@42188: val thy = @{theory Test};
walther@60340: val t = (Thm.term_of o the o (TermC.parse thy)) "12 / 3";
walther@59686: val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
neuper@38032: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@37906: "12 / 3 = 4";
akargl@42188: val thy = @{theory Test};
walther@60340: val t = (Thm.term_of o the o (TermC.parse thy)) "4 \<up> 2";
walther@59686: val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
neuper@38032: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@37906: "4 ^ 2 = 16";
neuper@37906: 
walther@60340:  val t = (Thm.term_of o the o (TermC.parse thy)) "((1 + 2) * 4 / 3) \<up> 2";
walther@59686:  val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"PLUS"))) t;
neuper@37906: "1 + 2 = 3";
neuper@38032:  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
walther@59868:  UnparseC.term t;
walther@60242: "(3 * 4 / 3) \<up> 2";
walther@59686:  val SOME (thmID,thm) = adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"TIMES")))t;
neuper@37906: "3 * 4 = 12";
neuper@38032:  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
walther@59868:  UnparseC.term t;
walther@60242: "(12 / 3) \<up> 2";
walther@59686:  val SOME (thmID,thm) =adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"DIVIDE")))t;
neuper@37906: "12 / 3 = 4";
neuper@38032:  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
walther@59868:  UnparseC.term t;
walther@60242: "4 \<up> 2";
walther@59686:  val SOME (thmID,thm) = adhoc_thm thy(the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER")))t;
walther@60242: "4 \<up> 2 = 16";
neuper@38032:  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
walther@59868:  UnparseC.term t;
neuper@37906: "16";
walther@59902:  if it <> "16" then error "evaluate.sml: new behaviour in calculate_"
neuper@37906:  else ();
neuper@37906: 
neuper@37906: (*13.9.02 *** calc: operator = pow not defined*)
walther@60340:   val t = (Thm.term_of o the o (TermC.parse thy)) "3 \<up> 2";
neuper@38032:   val SOME (thmID,thm) = 
walther@59686:       adhoc_thm thy (the(LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"))) t;
neuper@37906: (*** calc: operator = pow not defined*)
neuper@37906: 
walther@59686:   val (op_, eval_fn) = the (LibraryC.assoc(KEStore_Elems.get_calcs @{theory},"POWER"));
neuper@37906:   (*
wenzelm@60309: val op_ = \<^const_name>\<open>powr\<close> : string
neuper@37906: val eval_fn = fn : string -> term -> theory -> (string * term) option*)
neuper@37906: 
neuper@38032:   val SOME (thmid,t') = get_pair thy op_ eval_fn t;
neuper@37906: (*** calc: operator = pow not defined*)
neuper@37906: 
neuper@38032:   val SOME (id,t') = eval_fn op_ t thy;
neuper@37906: (*** calc: operator = pow not defined*)
neuper@37906: 
walther@60317: case (op_, t) of
walther@60317:   ("Transcendental.powr",
walther@60336:     Const (\<^const_name>\<open>powr\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _))) $
walther@60336:       (Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
walther@60317: | _ => error "3 \<up> 2 CHANGED";
walther@60317:   val SOME (id, t') = eval_binop thmid op_ t thy;
neuper@37906: (*** calc: operator = pow not defined*)
neuper@37906: 
walther@60317: if UnparseC.term t' = "3 \<up> 2 = 9" then () else error "eval_binop  3 \<up> 2 = 9  CHANGED";
walther@60317: 
walther@60317: 
walther@60317: "----------- fun cancel_int --------------------------------------------------------------------";
walther@60317: "----------- fun cancel_int --------------------------------------------------------------------";
walther@60317: "----------- fun cancel_int --------------------------------------------------------------------";
walther@60317: if cancel_int (~4, 2) = (~1, (2, 1)) then () else error "cancel_int (~4, 2) CHANGED";
walther@60317: if cancel_int (4, ~8) = (~1, (1, 2)) then () else error "cancel_int (4, ~8) CHANGED";
walther@60317: if cancel_int (6, 4) = (1, (3, 2)) then () else error "cancel_int (6, 4)CHANGED";
walther@60317: 
walther@60317: 
walther@60317: "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
walther@60317: "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
walther@60317: "----------- RE-BUILD fun calcul ---------------------------------------------------------------";
walther@60317: val (t1, t2) = (@{term 3}, @{term "2::real"});
walther@60317: 
walther@60317: "~~~~~ fun calcul , args:"; val (op_, (t1, t2)) = ("Groups.plus_class.plus", (t1, t2));
walther@60336:     val (Const (\<^const_name>\<open>numeral\<close>, _) $ n1) = t1;
walther@60336:     val (Const (\<^const_name>\<open>numeral\<close>, _) $ n2) = t2;
walther@60317:     val (T, _) = HOLogic.dest_number t1
walther@60317:     val (i1, i2) = (HOLogic.dest_numeral n1, HOLogic.dest_numeral n2)
walther@60317:     val result =
walther@60317:       case op_ of
walther@60317:         "Groups.plus_class.plus" => i1 + i2
walther@60317:       | "Groups.minus_class.minus" => i1 - i2
walther@60317:       | "Groups.times_class.times" => i1 * i2
walther@60317:       | "Transcendental.powr" => power i1 i2
walther@60317:       | str => raise ERROR ("calcul not impl.for op_ " ^ str)
walther@60317:   (*in*)
walther@60317:     val xxx = HOLogic.mk_number T result;
walther@60317:   (*end*)
walther@60317: case HOLogic.dest_number xxx of
walther@60317:   (_, 5) => ()
walther@60317: | _ => error "calcul + 2 3 CHANGED";
walther@60317: 
walther@60317: case HOLogic.dest_number (calcul "Groups.minus_class.minus" (t1, t2)) of
walther@60317:   (_, 1) => xxx
walther@60317: | _ => error "calcul - 2 3 CHANGED";
walther@60317: 
walther@60317: case HOLogic.dest_number (calcul "Groups.times_class.times" (t1, t2)) of
walther@60317:   (_, 6) => xxx
walther@60317: | _ => error "calcul - 2 3 CHANGED";
walther@60317: 
walther@60317: (*                       (calcul "Rings.divide_class.divide" (t1, t2)
walther@60317: ERROR: calcul not impl.for op_ Rings.divide_class.divide*)
walther@60317: 
walther@60317: case HOLogic.dest_number (calcul "Transcendental.powr" (t1, t2)) of
walther@60317:   (_, 9) => xxx
walther@60317: | _ => error "calcul - 2 3 CHANGED";
walther@60317: 
akargl@42188: 
neuper@37906: "----------- get_pair with 3 args --------------------------------";
neuper@37906: "----------- get_pair with 3 args --------------------------------";
neuper@37906: "----------- get_pair with 3 args --------------------------------";
neuper@37906: val (thy, op_, ef, arg) =
walther@60278:     (thy, "EqSystem.occur_exactly_in", 
wneuper@59462:      assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
walther@60230:      TermC.str2term
walther@60329:       "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2"
neuper@37906:       );
neuper@38032: val SOME (str, simpl) = get_pair thy op_ ef arg;
neuper@37906: if str = 
walther@60317: "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \<up> 2) / 2 = True"
walther@59902: then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in";
neuper@37906: 
neuper@37906: 
neuper@38032: "----------- calculate (2 * x is_const) -----------------";
neuper@38032: "----------- calculate (2 * x is_const) -----------------";
neuper@38032: "----------- calculate (2 * x is_const) -----------------";
walther@60230: val t = TermC.str2term "2 * x is_const";
akargl@42188: val SOME (str, t') = eval_const "" "" t @{theory Test};
walther@60317: if UnparseC.term t' = "(2 * x is_const) = False" then ()
walther@60317: else error "eval_const 2 * x is_const CHANGED";
neuper@37906: 
akargl@42188: val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
walther@60317: if UnparseC.term t' = "False" then ()
walther@60317: else error "rewrite_set_ 2 * x is_const CHANGED";
wneuper@59387: 
wneuper@59387: "----------- fun get_pair: examples ------------------------------------------------------------";
wneuper@59387: "----------- fun get_pair: examples ------------------------------------------------------------";
wneuper@59387: "----------- fun get_pair: examples ------------------------------------------------------------";
wneuper@59388: val thy = @{theory};
walther@59686: val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
walther@60317: if isa_str = "Groups.plus_class.plus" then () else error "eval_fn PLUS changed";
wneuper@59388: 
walther@60317: val t = @{term "3 + 4 :: real"};
wneuper@59388: val SOME (str, term) = get_pair thy isa_str eval_fn t;
walther@60317: (*+*)if str =  "#: 3 + 4 = 7" andalso UnparseC.term term = "3 + 4 = 7"
walther@60317: (*+*)then () else error "get_pair  3 + 4  changed";
wneuper@59388: 
walther@60317: val t = @{term "(a + 3) + 4 :: real"};
wneuper@59388: val SOME (str, term) = get_pair thy isa_str eval_fn t;
walther@59868: if str =  "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
wneuper@59388: then () else error "get_pair  (a + 3) + 4  changed";
wneuper@59388: 
walther@60317: val t = @{term "(a + 3) + 4 :: real"};
wneuper@59388: val SOME (str, term) = get_pair thy isa_str eval_fn t;
walther@59868: if str =  "#: a + 3 + 4 = a + 7" andalso UnparseC.term term = "a + 3 + 4 = a + 7"
wneuper@59388: then () else error "get_pair  (a + 3) + 4  changed";
wneuper@59388: 
walther@60317: val t = @{term "x = 5 * (3 + (4 + a) :: real)"};
wneuper@59388: val SOME (str, term) = get_pair thy isa_str eval_fn t;
walther@59868: if str =  "#: 3 + (4 + a) = 7 + a" andalso UnparseC.term term = "3 + (4 + a) = 7 + a"
wneuper@59388: then ((* !!! gets subterm !!!*)) else error "get_pair  x = 5 * (3 + (4 + a))  (subterm) changed";
wneuper@59388: 
walther@59686: val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
wneuper@59388: 
walther@60329: val t = @{term "-4 / - 2 :: real"};
wneuper@59388: val SOME (str, term) = get_pair thy isa_str eval_fn t;
walther@60317: if str = "#divide_e~4_~2" andalso UnparseC.term term = "- 4 / - 2 = 2"
walther@60329: then () else error "get_pair  -4 / - 2   changed";
wneuper@59388: 
walther@59686: val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "POWER");
wneuper@59388: 
walther@60317: val t = @{term "2 \<up> 3 :: real"};
wneuper@59388: val SOME (str, term) = get_pair thy isa_str eval_fn t;
walther@60242: if str =  "#: 2 \<up> 3 = 8" andalso UnparseC.term term = "2 \<up> 3 = 8"
walther@60242: then () else error "get_pair  2 \<up> 3   changed";
wneuper@59388: 
wneuper@59387: "----------- fun adhoc_thm: examples -----------------------------------------------------------";
wneuper@59387: "----------- fun adhoc_thm: examples -----------------------------------------------------------";
wneuper@59387: "----------- fun adhoc_thm: examples -----------------------------------------------------------";
wneuper@59388: (*--------------------------------------------------------------------vvvvvvvvvv*)
walther@59686: val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "is_const");
walther@60317: val t = @{term "9 is_const"};
wneuper@59388: val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
walther@59876: if str = "#is_const_9_" andalso ThmC_Def.string_of_thm thm = "(9 is_const) = True"
wneuper@59388: then () else error "adhoc_thm  9 is_const  changed";
wneuper@59387: 
wenzelm@60309: case assoc_calc thy \<^const_name>\<open>less\<close> of
wneuper@59388:   "le" => () | _ => error "Orderings.ord_class.less <-> le changed";
walther@59686: val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "le");
walther@60317: if isa_str = "Orderings.ord_class.less" then () else error "adhoc_thm (4 < 4) = False CHANGED";
wneuper@59387: 
walther@60317: val t = @{term "4 < (4 :: real)"};
wneuper@59388: val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
walther@59876: if str = "#less_4_4" andalso ThmC_Def.string_of_thm thm = "(4 < 4) = False"
wneuper@59388: then () else error "adhoc_thm  4 < 4  changed";
wneuper@59387: 
wneuper@59388: val SOME t = parseNEW @{context} "a < 4";
wneuper@59388: case adhoc_thm thy (isa_str, eval_fn) t of
wneuper@59388: NONE => () | _ => error "adhoc_thm  a < 4  does NOT result in NONE";
wneuper@59387: 
walther@59686: val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "PLUS");
walther@60317: val SOME t = parseNEW @{context} "1 + (2::real)";
wneuper@59388: val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
walther@59876: if str = "#: 1 + 2 = 3" andalso ThmC_Def.string_of_thm thm = "1 + 2 = 3"
wneuper@59388: then () else error "adhoc_thm  1 + 2  changed";
wneuper@59387: 
walther@59686: val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "DIVIDE");
walther@60317: val t = @{term "6 / -8 :: real"};
wneuper@59388: val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
walther@60317: if str = "#divide_e6_~8" andalso ThmC_Def.string_of_thm thm = "6 / - 8 = - 3 / 4"
walther@60317: then () else error "adhoc_thm  6 / -8 = - 3 / 4  changed";
wneuper@59387: 
walther@59603: case assoc_calc thy "Prog_Expr.ident" of
walther@59603:   "ident" => () | _ => error "Prog_Expr.ident <-> ident  changed";
walther@59686: val SOME (isa_str, eval_fn) = LibraryC.assoc (KEStore_Elems.get_calcs @{theory}, "ident");
wneuper@59387: 
walther@60317: val t = @{term "3 =!= (3 :: real)"};
wneuper@59388: val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
walther@59876: if str = "#ident_(3)_(3)" andalso ThmC_Def.string_of_thm thm = "(3 =!= 3) = True"
wneuper@59388: then () else error "adhoc_thm  (3 =!= 3)  changed";
wneuper@59387: 
walther@60317: val t = @{term "\<not> ((4 :: real) + (4 * x + x \<up> 2) =!= 0)"};
wneuper@59388: val SOME (str, thm) = adhoc_thm thy (isa_str, eval_fn) t;
walther@60317: 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"
wneuper@59388: then () else error "adhoc_thm  (\<not> (4 + (4 * x + x ^ 2) =!= 0))  changed";
wneuper@59403: 
walther@60329: "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
walther@60329: "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
walther@60329: "----------- fun adhoc_thm \<longrightarrow> exception TYPE --------------------------------------------------";
walther@60329: val t = TermC.str2term "sqrt 4";
walther@60329: 
walther@60330: (* TOODOO.1: exception TYPE raised by Skip_Proof.make_thm * )
walther@60329:   exception TYPE raised (line 169 of "consts.ML"): Illegal type
walther@60329:    for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
walther@60329:       Eval.adhoc_thm (ThyC.get_theory "Isac_Knowledge") ("NthRoot.sqrt", eval_sqrt "#sqrt_") t
walther@60329: ( **)
walther@60329: "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), ct) =
walther@60329:   ((ThyC.get_theory "Isac_Knowledge"),
walther@60329:     ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> theory -> (string * term) option), t);
walther@60356: 
walther@60329: val SOME (thmid, t) =
walther@60329:   (*case*) get_pair thy op_ eval_fn ct (*of*);
walther@60356: (*+*)val "sqrt 4 = 2" = UnparseC.term t;
walther@60356: 
walther@60329: (** )
walther@60356:       Skip_Proof.make_thm thy t;
walther@60356: 
walther@60329:   exception TYPE raised (line 169 of "consts.ML"): Illegal type
walther@60329:    for constant "HOL.eq" :: real \<Rightarrow> (num \<Rightarrow> real) \<Rightarrow> bool (**)
walther@60329: ( **)
walther@60329: 
wneuper@59403: "----------- fun power -------------------------------------------------------------------------";
wneuper@59403: "----------- fun power -------------------------------------------------------------------------";
wneuper@59403: "----------- fun power -------------------------------------------------------------------------";
wneuper@59403: if power 2 3 = 8 then () else error "power 2 3 = 8";
wneuper@59403: if power ~2 3 = ~8 then () else error "power ~2 3 = ~8";
wneuper@59403: if power ~3 2 = 9 then () else error "power ~3 2 = 9";
walther@60270: case \<^try>\<open> power 3 ~2 \<close> of
walther@60270:   SOME _ => raise error "power 3 ~2: should raise an exn 1"
walther@60271: | NONE => ();
wneuper@59403: 
wneuper@59403: "----------- fun divisors ----------------------------------------------------------------------";
wneuper@59403: "----------- fun divisors ----------------------------------------------------------------------";
wneuper@59403: "----------- fun divisors ----------------------------------------------------------------------";
wneuper@59403: if divisors 30 = [5, 3, 2] then () else error "divisors 30 = [5, 3, 2]";
wneuper@59403: if divisors 32 = [2, 2, 2, 2, 2] then () else error "divisors 32 = [2, 2, 2, 2, 2]";
wneuper@59403: if divisors 60 = [5, 3, 2, 2] then () else error "divisors 60 = [5, 3, 2, 2]";
wneuper@59403: if divisors 11 = [11] then () else error "divisors 11 = [11]";
wneuper@59403: 
wneuper@59403: "----------- fun doubles, fun squfact ----------------------------------------------------------";
wneuper@59403: "----------- fun doubles, fun squfact ----------------------------------------------------------";
wneuper@59403: "----------- fun doubles, fun squfact ----------------------------------------------------------";
wneuper@59403: if doubles [2,3,4] = [] then () else error "doubles [2,3,4] changed";
wneuper@59403: if doubles [2,3,3,5,5,7] = [5, 3] then () else error "doubles [2,3,3,5,5,7] changed";
wneuper@59403: 
wneuper@59403: if squfact 30 = 1 then () else error "squfact  30  changed";
wneuper@59403: if squfact 32 = 4 then () else error "squfact  32  changed";
wneuper@59403: if squfact 60 = 2 then () else error "squfact  60  changed";
wneuper@59403: if squfact 11 = 1 then () else error "squfact  11  changed";