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@60516: "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------"; neuper@38032: "----------- get_pair with 3 args -----------------------"; walther@60387: "----------- calculate (2 * x is_num) -------------------"; wneuper@59387: "----------- fun get_pair: examples ------------------------------------------------------------"; wneuper@59387: "----------- fun adhoc_thm: examples -----------------------------------------------------------"; walther@60391: "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------"; walther@60357: "----------- fun adhoc_thm \ exception TYPE --------------------------------------------------"; 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"}; Walther@60550: val ctxt = Proof_Context.init_global thy; Walther@60550: val cal = snd (get_calc ctxt "is_polyexp"); neuper@38022: val t = @{term "(x / x) is_polyexp"}; Walther@60519: val SOME (thmID, thm) = adhoc_thm ctxt 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_ \ fun rew_once works the same way *) Walther@60565: val t = TermC.parse_test @{context} "((1+2)*4/3) \ 2"; wneuper@59411: val thy = @{theory}; Walther@60500: val ctxt = Proof_Context.init_global @{theory} Walther@60539: val times = ("Groups.times_class.times", Calc_Binop.numeric "#mult_") : string * Eval.ml_fun; Walther@60539: val plus = ("Groups.plus_class.plus", Calc_Binop.numeric "#add_") : string * Eval.ml_fun; Walther@60539: val divide = ("Rings.divide_class.divide", eval_cancel "#divide_e") : string * Eval.ml_fun; Walther@60539: val pow = (\<^const_name>\realpow\, Calc_Binop.numeric "#power_") : string * Eval.ml_fun; wneuper@59411: walther@60317: "~~~~~ fun calculate_ , args:"; val (thy, isa_fn, t) = (thy, plus, t); Walther@60519: val SOME ("#: 1 + 2 = 3", adh_thm) = adhoc_thm @{context} isa_fn t; Walther@60509: val SOME (t', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; walther@60242: if UnparseC.term t' = "(3 * 4 / 3) \ 2" then () else error "calculate_ 1 + 2 = 3 changed"; wneuper@59411: wneuper@59411: "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, times, t'); Walther@60519: val SOME ("#: 3 * 4 = 12", adh_thm) = adhoc_thm @{context} isa_fn t'; Walther@60509: val SOME (t'', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; walther@60242: if UnparseC.term t'' = "(12 / 3) \ 2" then () else error "calculate_ 3 * 4 = 12 changed"; wneuper@59411: wneuper@59411: "~~~~~ fun calculate_, args:"; val (thy, isa_fn, t) = (thy, divide, t''); Walther@60519: val SOME ("#divide_e12_3", adh_thm) = adhoc_thm @{context} isa_fn t; Walther@60509: val SOME (t''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty Rule_Set.empty true adh_thm t; walther@60242: if UnparseC.term t''' = "4 \ 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@60519: val SOME ("#: 4 \ 2 = 16", adh_thm) = adhoc_thm @{context} isa_fn t; Walther@60509: val SOME (t'''', []) = rewrite__ ctxt 0 [] Rewrite_Ord.function_empty 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) \ 2)", "realTestFind s"]; neuper@37906: val (dI',pI',mI') = walther@60317: ("Test", ["calculate", "test"], ["Test", "test_calculate"]); neuper@38035: Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(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) \ #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 \ 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 \ 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@60588: val op_ = the (LibraryC.assoc (Know_Store.get_calcs @{theory}, "DIVIDE")); walther@60337: val ct = @{term walther@60329: "sqrt (x \ 2 + -3 * x) = (-9) / (- 2) + (-3 / (- 2) + (x * ((-4) / (- 2)) + x * (2 / (- 2))))"}; Walther@60500: case calculate_ ctxt op_ ct of wneuper@59382: SOME _ => () wneuper@59382: | NONE => error "calculate_ test-root-equ changed"; neuper@37906: (* walther@60242: sqrt (x \ 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@60424: val ctxt = (ThyC.id_to_ctxt "Test") Walther@60424: val t = TermC.parseNEW' ctxt "6 / 2"; neuper@37906: val rls = Test_simplify; Walther@60500: val (t,_) = the (rewrite_set_ ctxt false rls t); walther@59997: (*val t = Free ("3", "Real.real") : term*) neuper@37906: walther@60387: (*--------------(3): is_num works ?: -------------------------------------*) Walther@60424: val t = TermC.parseNEW' ctxt "2 is_num"; Walther@60650: TermC.atom_trace_detail @{context} t; Walther@60500: rewrite_set_ ctxt false tval_rls t; wenzelm@60309: (*val it = SOME (Const (\<^const_name>\True\, "bool"),[]) ... works*) neuper@37906: Walther@60565: val t = TermC.parse_test @{context} "2 * x is_num"; walther@60387: val NONE = eval_is_num "" "" t (@{theory "Isac_Knowledge"}); 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: *) akargl@42188: val thy = @{theory Test}; wneuper@59384: val rls = Test_simplify; Walther@60424: val t = TermC.parseNEW' ctxt "(-4) / 2"; akargl@42188: wenzelm@60309: val SOME (_, t) = eval_cancel "xxx" \<^const_name>\divide\ t thy; akargl@42188: neuper@37906: (*--------------(5): reproduce (1) with simpler term: ------------*) Walther@60424: val t = TermC.parseNEW' ctxt "(3+5)/(2::real)"; Walther@60500: case rewrite_set_ ctxt 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@60424: val t = TermC.parseNEW' ctxt "(3+1+2*x)/(2::real)"; Walther@60500: case rewrite_set_ ctxt 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@60500: (*--- trace_rewrite 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@60424: val t = TermC.parseNEW' ctxt "x + (- 1 + -3) / (2::real)"; Walther@60500: val SOME (res, []) = rewrite_set_ ctxt 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@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@60424: val t = TermC.parseNEW' ctxt "12 / 3"; Walther@60588: val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(Know_Store.get_calcs @{theory},"DIVIDE")))t; Walther@60500: val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; neuper@37906: "12 / 3 = 4"; akargl@42188: val thy = @{theory Test}; Walther@60424: val t = TermC.parseNEW' ctxt "4 \ 2"; Walther@60588: val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(Know_Store.get_calcs @{theory},"POWER"))) t; Walther@60500: val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; neuper@37906: "4 ^ 2 = 16"; neuper@37906: Walther@60424: val t = TermC.parseNEW' ctxt "((1 + 2) * 4 / 3) \ 2"; Walther@60588: val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"PLUS"))) t; neuper@37906: "1 + 2 = 3"; Walther@60500: val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; walther@59868: UnparseC.term t; walther@60242: "(3 * 4 / 3) \ 2"; Walther@60588: val SOME (thmID,thm) = adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"TIMES")))t; neuper@37906: "3 * 4 = 12"; Walther@60500: val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; walther@59868: UnparseC.term t; walther@60242: "(12 / 3) \ 2"; Walther@60588: val SOME (thmID,thm) =adhoc_thm ctxt(the(LibraryC.assoc(Know_Store.get_calcs @{theory},"DIVIDE")))t; neuper@37906: "12 / 3 = 4"; Walther@60500: val SOME (t,_) = rewrite_ ctxt tless_true tval_rls true thm t; walther@59868: UnparseC.term t; walther@60242: "4 \ 2"; Walther@60588: val SOME (thmID,thm) = adhoc_thm ctxt(the(LibraryC.assoc(Know_Store.get_calcs @{theory},"POWER")))t; walther@60242: "4 \ 2 = 16"; Walther@60500: val SOME (t,_) = rewrite_ ctxt 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@60424: val t = TermC.parseNEW' ctxt "3 \ 2"; neuper@38032: val SOME (thmID,thm) = Walther@60588: adhoc_thm ctxt (the(LibraryC.assoc(Know_Store.get_calcs @{theory},"POWER"))) t; neuper@37906: (*** calc: operator = pow not defined*) neuper@37906: Walther@60588: val (op_, eval_fn) = the (LibraryC.assoc(Know_Store.get_calcs @{theory},"POWER")); neuper@37906: (* wenzelm@60405: val op_ = \<^const_name>\realpow\ : string neuper@37906: val eval_fn = fn : string -> term -> theory -> (string * term) option*) neuper@37906: Walther@60504: val SOME (thmid,t') = get_pair ctxt op_ eval_fn t; neuper@37906: (*** calc: operator = pow not defined*) neuper@37906: Walther@60504: val SOME (id,t') = eval_fn op_ t ctxt; neuper@37906: (*** calc: operator = pow not defined*) neuper@37906: walther@60317: case (op_, t) of wenzelm@60405: (\<^const_name>\realpow\, wenzelm@60405: Const (\<^const_name>\realpow\, _) $ (Const (\<^const_name>\numeral\, _) $ (Const (\<^const_name>\num.Bit1\, _) $ Const (\<^const_name>\num.One\, _))) $ walther@60336: (Const (\<^const_name>\numeral\, _) $ (Const (\<^const_name>\num.Bit0\, _) $ Const (\<^const_name>\num.One\, _)))) => () walther@60317: | _ => error "3 \ 2 CHANGED"; Walther@60516: val SOME (id, t') = Calc_Binop.numeric thmid op_ t ctxt; neuper@37906: (*** calc: operator = pow not defined*) neuper@37906: walther@60317: if UnparseC.term t' = "3 \ 2 = 9" then () else error "eval_binop 3 \ 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@60516: "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------"; Walther@60516: "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------"; Walther@60516: "----------- RE-BUILD fun Calc_Binop.simplify ---------------------------------------------------------------"; walther@60401: val t = @{term "2 + 3 ::real"}; walther@60317: Walther@60516: "~~~~~ fun Calc_Binop.simplify , args:"; val (thy, lhs) = (@{theory}, t); walther@60401: val simp_ctxt = walther@60401: Proof_Context.init_global thy wenzelm@60407: |> put_simpset (Simplifier.simpset_of @{theory_context BaseDefinitions}); walther@60401: val eq = Simplifier.rewrite simp_ctxt (Thm.global_cterm_of thy lhs); walther@60317: Walther@60648: if ThmC.string_of_thm ctxt eq = "2 + 3 \ 5" then () else error "calcul 1"; walther@60317: walther@60401: val rhs = Thm.term_of (Thm.rhs_of eq); walther@60401: val _ = \<^assert> (is_num rhs); walther@60317: walther@60401: (*return value*) rhs; walther@60401: if TermC.to_string rhs = "5" then () else error "calcul 2"; 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", Walther@60550: get_calc (@{theory "EqSystem"} |> Proof_Context.init_global) "occur_exactly_in" |> snd |> snd, Walther@60565: TermC.parse_test @{context} walther@60329: "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \ 2) / 2" neuper@37906: ); Walther@60504: val SOME (str, simpl) = get_pair ctxt op_ ef arg; neuper@37906: if str = walther@60317: "[] from [c, c_2, c_3, c_4] occur_exactly_in - 1 * (q_0 * L \ 2) / 2 = True" walther@59902: then () else error "evaluate.sml get_pair with 3 args:occur_exactly_in"; neuper@37906: neuper@37906: walther@60387: "----------- calculate (2 * x is_num) -------------------"; walther@60387: "----------- calculate (2 * x is_num) -------------------"; walther@60387: "----------- calculate (2 * x is_num) -------------------"; Walther@60565: val t = TermC.parse_test @{context} "(2::real) * x is_num"; walther@60387: walther@60387: val SOME (str, t') = eval_is_num "" "Prog_Expr.is_num" t @{theory Test}; walther@60387: if UnparseC.term t' = "(2 * x is_num) = False" then () walther@60387: else error "is_num 2 * x is_num CHANGED"; neuper@37906: Walther@60500: val SOME (t',_) = rewrite_set_ ctxt false tval_rls t; walther@60317: if UnparseC.term t' = "False" then () walther@60387: else error "rewrite_set_ 2 * x is_num 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@60550: val ctxt = @{context}; Walther@60588: val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.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"}; Walther@60504: val SOME (str, term) = get_pair ctxt 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"}; Walther@60504: val SOME (str, term) = get_pair ctxt 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"}; Walther@60504: val SOME (str, term) = get_pair ctxt 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)"}; Walther@60504: val SOME (str, term) = get_pair ctxt 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@60588: val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "DIVIDE"); wneuper@59388: walther@60329: val t = @{term "-4 / - 2 :: real"}; Walther@60504: val SOME (str, term) = get_pair ctxt 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@60588: val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "POWER"); wneuper@59388: walther@60317: val t = @{term "2 \ 3 :: real"}; Walther@60504: val SOME (str, term) = get_pair ctxt isa_str eval_fn t; walther@60242: if str = "#: 2 \ 3 = 8" andalso UnparseC.term term = "2 \ 3 = 8" walther@60242: then () else error "get_pair 2 \ 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@60588: val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "is_num"); walther@60387: val t = @{term "9 is_num"}; Walther@60519: val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t; Walther@60648: if str = "#is_num_9_" andalso ThmC.string_of_thm ctxt thm = "(9 is_num) = True" walther@60387: then () else error "adhoc_thm 9 is_num changed"; wneuper@59387: Walther@60550: case get_calc_prog_id ctxt \<^const_name>\less\ of wneuper@59388: "le" => () | _ => error "Orderings.ord_class.less <-> le changed"; Walther@60588: val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.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)"}; Walther@60519: val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t; Walther@60648: if str = "#less_4_4" andalso ThmC.string_of_thm ctxt 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"; Walther@60519: case adhoc_thm ctxt (isa_str, eval_fn) t of wneuper@59388: NONE => () | _ => error "adhoc_thm a < 4 does NOT result in NONE"; wneuper@59387: Walther@60588: val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "PLUS"); walther@60317: val SOME t = parseNEW @{context} "1 + (2::real)"; Walther@60519: val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t; Walther@60648: if str = "#: 1 + 2 = 3" andalso ThmC.string_of_thm ctxt thm = "1 + 2 = 3" wneuper@59388: then () else error "adhoc_thm 1 + 2 changed"; wneuper@59387: Walther@60588: val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "DIVIDE"); walther@60317: val t = @{term "6 / -8 :: real"}; Walther@60519: val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t; Walther@60648: if str = "#divide_e6_~8" andalso ThmC.string_of_thm ctxt thm = "6 / - 8 = - 3 / 4" walther@60317: then () else error "adhoc_thm 6 / -8 = - 3 / 4 changed"; wneuper@59387: Walther@60550: case get_calc_prog_id ctxt "Prog_Expr.ident" of walther@59603: "ident" => () | _ => error "Prog_Expr.ident <-> ident changed"; Walther@60588: val SOME (isa_str, eval_fn) = LibraryC.assoc (Know_Store.get_calcs @{theory}, "ident"); wneuper@59387: walther@60317: val t = @{term "3 =!= (3 :: real)"}; Walther@60519: val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t; Walther@60648: if str = "#ident_(3)_(3)" andalso ThmC.string_of_thm ctxt thm = "(3 =!= 3) = True" wneuper@59388: then () else error "adhoc_thm (3 =!= 3) changed"; wneuper@59387: walther@60317: val t = @{term "\ ((4 :: real) + (4 * x + x \ 2) =!= 0)"}; Walther@60519: val SOME (str, thm) = adhoc_thm ctxt (isa_str, eval_fn) t; Walther@60648: if str = "#ident_(4 + (4 * x + x \ 2))_(0)" andalso ThmC.string_of_thm ctxt thm = "(4 + (4 * x + x \ 2) =!= 0) = False" wneuper@59388: then () else error "adhoc_thm (\ (4 + (4 * x + x ^ 2) =!= 0)) changed"; wneuper@59403: walther@60391: "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------"; walther@60391: "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------"; walther@60391: "----------- fun adhoc_thm + fun eval_cancel ---------------------------------------------------"; Walther@60538: val eval_ = ("Rings.divide_class.divide", eval_cancel "#divide_e" : Eval.ml_fun): Eval.ml; walther@60391: val t = @{term "- 1 / 2 ::real"}; walther@60391: (* walther@60391: ML\Eval.adhoc_thm\ is called while searching terms for adjacent numerals walther@60391: given a certain ML_type\eval_fn\ and a certain ML\term\ .. walther@60391: walther@60391: THE ERROR WAS: walther@60391: rew_once: walther@60391: Eval.get_pair for \<^const_name>\divide\ \ SOME (_, "- 1 / 2 = - 1 / 2") walther@60391: but rewrite__ on "x = - 0 \ x = - 1 / 2" \ NONE walther@60391: walther@60391: STEP-INTO BEVORE REMOVING THE ERROR: walther@60391: val SOME ("#divide_e~1_2", adhoc_thm) = Walther@60519: Eval.adhoc_thm @{context} eval_ t; walther@60391: "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t); walther@60391: val SOME walther@60391: ("#divide_e~1_2", t'') = Walther@60504: (*case*) get_pair ctxt op_ eval_fn t (*of*); walther@60391: (* walther@60391: get_pair finds two adjacent numerals and does NOT distinguish between different kinds of walther@60391: \<^ML_type>\eval_fn\. In case of \<^ML>\eval_cancel\ the return value WAS the same as the input.. walther@60391: *) walther@60391: (*+*)ThmC.string_of_thm adhoc_thm = "- 1 / 2 = - 1 / 2" walther@60391: *) walther@60391: Walther@60519: val NONE = adhoc_thm @{context} eval_ t; walther@60393: "~~~~~ fun adhoc_thm , args:"; val (thy, (op_, eval_fn), t) = (@{theory}, eval_, t); walther@60391: val NONE = Walther@60504: (*case*) get_pair ctxt op_ eval_fn t (*of*); walther@60391: walther@60391: walther@60329: "----------- fun adhoc_thm \ exception TYPE --------------------------------------------------"; walther@60329: "----------- fun adhoc_thm \ exception TYPE --------------------------------------------------"; walther@60329: "----------- fun adhoc_thm \ exception TYPE --------------------------------------------------"; Walther@60565: val t = TermC.parse_test @{context} "sqrt 4"; Walther@60519: Eval.adhoc_thm @{context} ("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@60504: ("NthRoot.sqrt", eval_sqrt "#sqrt_": string -> term -> Proof.context -> (string * term) option), t); walther@60356: walther@60329: val SOME (thmid, t) = Walther@60504: (*case*) get_pair ctxt 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 \ (num \ real) \ 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>\ power 3 ~2 \ 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";