# HG changeset patch # User berghofe # Date 1138817972 -3600 # Node ID 6ad81e3fa4782ee71ab21fdc1aeb41190d35490e # Parent 9f27383426dbbf43cac20cf59775ff3e03883ba8 Added "evaluation" method and oracle. diff -r 9f27383426db -r 6ad81e3fa478 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Feb 01 15:22:02 2006 +0100 +++ b/src/HOL/HOL.thy Wed Feb 01 19:19:32 2006 +0100 @@ -1202,8 +1202,14 @@ attach (test) {* fun gen_bool i = one_of [false, true]; *} + "prop" ("bool") +attach (term_of) {* +fun term_of_prop b = + HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const); +*} consts_code + "Trueprop" ("(_)") "True" ("true") "False" ("false") "Not" ("not") @@ -1230,14 +1236,34 @@ thy defs dep thyname b (gr, Codegen.eta_expand t ts 2)) | _ => NONE); +exception Evaluation of term; + +fun evaluation_oracle (thy, Evaluation t) = + Logic.mk_equals (t, Codegen.eval_term thy t); + +fun evaluation_conv ct = + let val {sign, t, ...} = rep_cterm ct + in Thm.invoke_oracle_i sign "HOL.Evaluation" (sign, Evaluation t) end; + +fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule + (Drule.goals_conv (equal i) evaluation_conv)); + +val evaluation_meth = + Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac TrueI 1)); + in val eq_codegen_setup = Codegen.add_codegen "eq_codegen" eq_codegen; +val evaluation_oracle_setup = + Theory.add_oracle ("Evaluation", evaluation_oracle) #> + Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation"); + end; *} setup eq_codegen_setup +setup evaluation_oracle_setup subsection {* Other simple lemmas *}