neuper@38022: (* Title:  test calculation of values for function constants
neuper@38022:    Author: Walther Neuper 2000
neuper@38022:    (c) copyright due to lincense terms.
neuper@37906: 
neuper@38022: 12345678901234567890123456789012345678901234567890123456789012345678901234567890
neuper@38022:         10        20        30        40        50        60        70        80
neuper@37906: *)
neuper@37906: 
neuper@38022: "--------------------------------------------------------";
neuper@38022: "table of contents --------------------------------------";
neuper@38022: "--------------------------------------------------------";
neuper@41924: "----------- fun norm -----------------------------------";
neuper@38022: "----------- check return value of get_calculation_  ----";
neuper@38032: "----------- fun calculate_ -----------------------------";
neuper@38032: "----------- fun calculate_ -----------------------------";
neuper@38032: "----------- calculate from script ----------------------";
neuper@38032: "----------- calculate check test-root-equ --------------";
neuper@38032: "----------- check calculate bottom up ------------------";
neuper@42223: "----------- Atools.pow Power.power_class.power ---------";
neuper@41934: " ================= calculate.sml: calculate_ 2002 ======";
neuper@38032: "----------- get_pair with 3 args -----------------------";
neuper@38032: "----------- calculate (2 * x is_const) -----------------";
neuper@38022: "--------------------------------------------------------";
neuper@38022: "--------------------------------------------------------";
neuper@38022: "--------------------------------------------------------";
neuper@37906: 
neuper@38022: "----------- check return value of get_calculation_  ----";
neuper@38022: "----------- check return value of get_calculation_  ----";
neuper@38022: "----------- check return value of get_calculation_  ----";
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"};
neuper@38022: val SOME (thmID, thm) = get_calculation_ thy cal t;
neuper@38022: (HOLogic.dest_Trueprop (prop_of thm); writeln "all thms wrapped by Trueprop")
neuper@38022: handle TERM _ => 
neuper@38031:        error "calculate.sml: get_calculation_ must return Trueprop";
neuper@38022: 
neuper@38033: "----------- fun calculate_ -----------------------------";
neuper@38033: "----------- fun calculate_ -----------------------------";
neuper@38033: "----------- fun calculate_ -----------------------------";
neuper@41924: val thy = @{theory "Test"};
neuper@38033: "===== test 1";
neuper@38033: val t = (term_of o the o (parse thy)) "1+2";
neuper@38033: val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
neuper@38033: term2str (prop_of thm) = "1 + 2 = 3";
neuper@38033: 
neuper@38033: "===== test 2";
neuper@38033: val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
neuper@38033: val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
neuper@38033: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@41931: if term2str t = "(3 * 4 / 3) ^^^ 2" then ()
neuper@41931: else error "calculate.sml: ((1+2)*4/3)^^^2 --> (3 * 4 / 3) ^^^ 2";
neuper@38033: 
neuper@38033: "===== test 3b -- 2 contiued";
neuper@38033: val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t;
neuper@38033: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@38033: term2str t;
neuper@38033: (*val it = "(#12 // #3) ^^^ #2" : string*)
neuper@37906: 
neuper@38033: "===== test 4";
neuper@38033: val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
neuper@38032: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@38033: term2str t;
neuper@38033: (*it = "#4 ^^^ #2" : string*)
neuper@38033: 
neuper@38033: "===== test 5";
neuper@38033: val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;
neuper@38032: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@41931: (*show_types := false;*)
neuper@38037: if term2str t <> "16" then error "calculate.sml: new behaviour in calculate_"
neuper@37906: else ();
neuper@37906: 
neuper@38032: "----------- calculate from script ----------------------";
neuper@38032: "----------- calculate from script ----------------------";
neuper@38032: "----------- calculate from script ----------------------";
neuper@37906: store_pbt
neuper@41924:  (prep_pbt (@{theory "Test"}) "pbl_ttest" [] e_pblID
neuper@37906:  (["test"],
neuper@37906:   [],
neuper@38032:   e_rls, NONE, []));
neuper@37906: store_pbt
neuper@41924:  (prep_pbt (@{theory "Test"}) "pbl_ttest_calc" [] e_pblID
neuper@37906:  (["calculate","test"],
neuper@38035:   [("#Given" ,["realTestGiven t_t"]),
neuper@38035:    ("#Find"  ,["realTestFind s_s"])
neuper@37906:    ],
neuper@38032:   e_rls, NONE, [["Test","test_calculate"]]));
neuper@37906: 
neuper@37906: store_met
neuper@41924:  (prep_met (@{theory "Test"}) "met_testcal" [] e_metID
neuper@37906:  (["Test","test_calculate"]:metID,
neuper@38035:   [("#Given" ,["realTestGiven t_t"]),
neuper@38035:    ("#Find"  ,["realTestFind s_s"])
neuper@37906:    ],
neuper@37906:   {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls,
neuper@38033:    calc=[("PLUS"    ,("op +"        ,eval_binop "#add_")),
neuper@38034: 	 ("TIMES"   ,("Groups.times_class.times"        ,eval_binop "#mult_")),
neuper@38033: 	 ("DIVIDE" ,("HOL.divide"  ,eval_cancel "#divide_")),
neuper@38033: 	 ("POWER"  ,("Atools.pow"  ,eval_binop "#power_"))],
neuper@42425:    crls=tval_rls, errpats = [], nrls=e_rls(*,
neuper@37906:    asm_rls=[],asm_thm=[]*)},
neuper@38035:   "Script STest_simplify (t_t::real) =          \
neuper@37906:   \(Repeat                                        \
neuper@38035:   \ ((Try (Repeat (Calculate PLUS))) @@   \
neuper@38035:   \  (Try (Repeat (Calculate TIMES))) @@  \
neuper@38035:   \  (Try (Repeat (Calculate DIVIDE))) @@ \
neuper@38035:   \  (Try (Repeat (Calculate POWER))))) t_t"
neuper@37906:    ));
neuper@37906: 
neuper@37906: val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"];
neuper@37906: val (dI',pI',mI') =
neuper@38035:   ("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;
neuper@37906: (*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#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;
neuper@37906: (*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38035: (*nxt = ("Specify_Method",Specify_Method ("Test","test_calculate"))*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38035: (*nxt = ("Apply_Method",Apply_Method ("Test","test_calculate"))*)
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38033: (*nxt = ("Calculate",Calculate "PLUS")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38033: (*nxt = ("Calculate",Calculate "TIMES")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38033: (*nxt = ("Calculate",Calculate "DIVIDE")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38033: (*nxt = ("Calculate",Calculate "POWER")*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*nxt = ("End_Proof'",End_Proof')*)
neuper@37906: if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then ()
neuper@38031: else error "calculate.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 =
neuper@37906:   "sqrt (x ^^^ 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);
neuper@37906: val ct = "sqrt (x ^^^ 2 + -3 * x) =
neuper@37906: (-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
neuper@37906: ie. cancel does not work properly
neuper@37906: *)
neuper@38035:  val thy = "Test";
neuper@38033:  val op_ = "DIVIDE";
neuper@37906:  val ct = "sqrt (x ^^^ 2 + -3 * x) =\
neuper@37906:  \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))";
neuper@38032:  val SOME (ct,_) = calculate thy (the(assoc(calclist,op_))) ct;
neuper@37906:  writeln ct;
neuper@37906: (*
neuper@37906:            sqrt (x ^^^ 2 + -3 * x) =\
neuper@37906:  \(-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};
neuper@37906:  val t = (term_of o the o (parse thy)) "6 / 2";
neuper@37906:  val rls = Test_simplify;
neuper@37906:  val (t,_) = the (rewrite_set_ thy false rls t);
neuper@37906: (*val t = Free ("3","RealDef.real") : term*)
neuper@37906: 
neuper@38035:  val thy = "Test";
neuper@37906:  val t = "6 / 2";
neuper@37906:  val rls = "Test_simplify";
neuper@37906:  val (t,_) = the (rewrite_set thy false rls t);
neuper@37906: (*val t = "3" : string
neuper@37906:       ....... works, thus: which rule in SqRoot_simplify works differently ?*)
neuper@37906: 
neuper@37906: 
neuper@37906: (*--------------(3): is_const works ?: -------------------------------------*)
akargl@42188:  val t = (term_of o the o (parse @{theory Test})) "2 is_const";
neuper@37906:  atomty t;
akargl@42188:  rewrite_set_ @{theory Test} false tval_rls t;
neuper@41928: (*val it = SOME (Const ("HOL.True","bool"),[]) ... works*)
neuper@37906: 
neuper@37906:  val t = str2term "2 * x is_const";
akargl@42188:  val SOME (str,t') = eval_const "" "" t (@{theory "Isac"});
neuper@37906:  term2str 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: *)
neuper@52070:  trace_rewrite:=false;
akargl@42188:  val thy = @{theory Test};
neuper@37906:  val t = (term_of o the o (parse thy)) "(-4) / 2";
akargl@42188: 
neuper@48789: val SOME (_, t) = eval_cancel "xxx" "Fields.inverse_class.divide" t thy;
akargl@42188: 
neuper@37906:  term2str t;
neuper@37906: "-4 / 2 = (-2)";
neuper@37906: (*-------------- but ... *)
neuper@37906:  val ct = "x + (-4) / 2";
akargl@42188: 
akargl@42218: val thy' = "Test"; (* added AK110727 *)
neuper@37906:  val (ct,_) = the (rewrite_set thy' false rls ct);
akargl@42188: 
neuper@37906: "(-2) + x";
neuper@37906: (*-------------- while ... *)
neuper@37906:  val ct = "(-4) / 2";
akargl@42202: 
neuper@37906:  val (ct,_) = the (rewrite_set thy'  false rls ct);
akargl@42202: 
neuper@37906: "-2";
neuper@37906: 
neuper@37906: (*--------------(5): reproduce (1) with simpler term: ------------*)
neuper@38035:  val thy = "Test";
neuper@37906:  val t = "(3+5)/2";
neuper@37906:  val (t,_) = the (rewrite_set thy false rls t);
neuper@37906: (*val t = "4" ... works*)
neuper@37906: 
neuper@37906:  val t = "(3+1+2*x)/2";
neuper@37906:  val (t,_) = the (rewrite_set thy false rls t);
neuper@37906: (*val t = "2 + x" ... works*)
neuper@37906: 
neuper@52070:  trace_rewrite:=false; (*=true3.6.03*)
akargl@42218: 
neuper@38035:  val thy = "Test";
neuper@37906:  val rls = "Test_simplify";
neuper@37906:  val t = "(3+(1+2*x))/2";
neuper@37906:  val (t,_) = the (rewrite_set thy false rls t);
neuper@37906: (*val t = "2 + x" ... works: give up----------------------------------------*)
neuper@37906:  trace_rewrite:=false; 
neuper@37906: 
neuper@52070:  trace_rewrite:=false; (*=true3.6.03*)
akargl@42188:  val thy = @{theory Test};
neuper@37906:  val rls = Test_simplify;
neuper@37906:  val t = str2term "(3+(1+2*x))/2";
neuper@38032:  val SOME (t',asm) = rewrite_set_ thy false rls t;
neuper@37906:  term2str t';
neuper@37906: (*val t = "2 + x" ... works: give up----------------------------------------*)
neuper@37906:  trace_rewrite:=false; 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*--- trace_rewrite before correction of ... --------------------
neuper@37906:  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'
neuper@37906: ### 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:
neuper@37906:  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'
neuper@37906: ### 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: ### rewrite_set_: x + #-2
neuper@37906: ### trying thm 'rcollect_right'
neuper@37906: :
neuper@37906: "#-2 + x"
neuper@37906: -----------------------------------------------------------------*)
neuper@37906: 
neuper@37906: 
neuper@37906: (*===================*)
neuper@52070:  trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
neuper@38035:  val thy' = "Test";
neuper@37906:  val rls = "Test_simplify";		
neuper@37906:  val ct = "x + (-1 + -3) / 2";
neuper@37906:  val (ct,_) = the (rewrite_set thy'  false rls ct);	
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
neuper@38032: @@@ get_calculation: NONE
neuper@37906: ### trying calc. 'pow'
neuper@37906: *)
neuper@37906: 
neuper@52070:  trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
neuper@38035:  val thy' = "Test";
neuper@37906:  val rls = "Test_simplify";		
neuper@37906:  val ct = "x + (-4) / 2";
neuper@37906:  val (ct,_) = the (rewrite_set thy'  false rls ct);	
neuper@37906: "(-2) + x";
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_calculation: SOME #cancel_-4_2
neuper@37906: ### calc. to: x + (-2)
neuper@37906: ### trying calc. 'cancel'
neuper@37906: *)
neuper@37906:  trace_rewrite:=false;
neuper@37906: 
neuper@42223: "----------- Atools.pow Power.power_class.power ---------";
neuper@42223: "----------- Atools.pow Power.power_class.power ---------";
neuper@42223: "----------- Atools.pow Power.power_class.power ---------";
neuper@42223: val t = (term_of o the o (parseold thy)) "1 ^ aaa";
neuper@42223: atomty t;
neuper@37906: (*** -------------
neuper@37906: *** Const ( Nat.power, ['a, nat] => 'a)
neuper@37906: *** . Free ( 1, 'a)
neuper@37906: *** . Free ( aaa, nat) *)
akargl@42218: 
neuper@42223: val t = str2term "1 ^^^ aaa";
neuper@42223: atomty t;
neuper@42223: (**** 
neuper@42223: *** Const (Atools.pow, real => real => real)
neuper@42223: *** . Free (1, real)
neuper@42223: *** . Free (aaa, real)
neuper@42223: *** *);
neuper@37906: 
neuper@37906: " ================= calculate.sml: calculate_ 2002 =================== ";
neuper@37906: " ================= calculate.sml: calculate_ 2002 =================== ";
neuper@37906: " ================= calculate.sml: calculate_ 2002 =================== ";
neuper@37906: 
akargl@42188: val thy = @{theory Test};
neuper@37906: val t = (term_of o the o (parse thy)) "12 / 3";
neuper@38033: val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"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};
neuper@37906: val t = (term_of o the o (parse thy)) "4 ^^^ 2";
neuper@38033: val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER"))) t;
neuper@38032: val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@37906: "4 ^ 2 = 16";
neuper@37906: 
neuper@37906:  val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2";
neuper@38033:  val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"PLUS"))) t;
neuper@37906: "1 + 2 = 3";
neuper@38032:  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@38033:  term2str t;
neuper@37906: "(3 * 4 / 3) ^^^ 2";
neuper@38033:  val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES")))t;
neuper@37906: "3 * 4 = 12";
neuper@38032:  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@38033:  term2str t;
neuper@37906: "(12 / 3) ^^^ 2";
neuper@38033:  val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"DIVIDE")))t;
neuper@37906: "12 / 3 = 4";
neuper@38032:  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@38033:  term2str t;
neuper@37906: "4 ^^^ 2";
neuper@38033:  val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"POWER")))t;
neuper@37906: "4 ^^^ 2 = 16";
neuper@38032:  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
neuper@38033:  term2str t;
neuper@37906: "16";
neuper@38031:  if it <> "16" then error "calculate.sml: new behaviour in calculate_"
neuper@37906:  else ();
neuper@37906: 
neuper@37906: (*13.9.02 *** calc: operator = pow not defined*)
neuper@37906:   val t = (term_of o the o (parse thy)) "3^^^2";
neuper@38032:   val SOME (thmID,thm) = 
neuper@38033:       get_calculation_ thy (the(assoc(calclist,"POWER"))) t;
neuper@37906: (*** calc: operator = pow not defined*)
neuper@37906: 
neuper@38033:   val (op_, eval_fn) = the (assoc(calclist,"POWER"));
neuper@37906:   (*
neuper@37906: val op_ = "Atools.pow" : 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: 
neuper@37906:   val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t);
neuper@38032:   val SOME (id,t') = eval_binop thmid op_ t thy;
neuper@37906: (*** calc: operator = pow not defined*)
neuper@37906: 
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) =
neuper@37906:     (thy, "EqSystem.occur'_exactly'_in", 
neuper@37906:      snd (the (assoc(!calclist',"occur_exactly_in"))),
neuper@37906:      str2term
akargl@42188:       "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
neuper@37906:       );
neuper@38032: val SOME (str, simpl) = get_pair thy op_ ef arg;
neuper@37906: if str = 
akargl@42188: "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2 = True"
neuper@38031: then () else error "calculate.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) -----------------";
neuper@37906: val t = str2term "2 * x is_const";
akargl@42188: val SOME (str, t') = eval_const "" "" t @{theory Test};
neuper@37906: term2str t';
neuper@37906: "(2 * x is_const) = False";
neuper@37906: 
akargl@42188: val SOME (t',_) = rewrite_set_ @{theory Test} false tval_rls t;
neuper@37906: term2str t';
neuper@41928: "HOL.False";