# 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 *}