src/HOL/Code_Setup.thy
 changeset 28740 22a8125d66fa parent 28699 32b6a8f12c1c child 28856 5e009a80fe6d
```     1.1 --- a/src/HOL/Code_Setup.thy	Thu Nov 13 14:19:10 2008 +0100
1.2 +++ b/src/HOL/Code_Setup.thy	Thu Nov 13 15:58:37 2008 +0100
1.3 @@ -22,6 +22,12 @@
1.4  text {* Code equations *}
1.5
1.6  lemma [code]:
1.7 +  shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P"
1.8 +    and "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
1.9 +    and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True"
1.10 +    and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
1.11 +
1.12 +lemma [code]:
1.13    shows "False \<and> x \<longleftrightarrow> False"
1.14      and "True \<and> x \<longleftrightarrow> x"
1.15      and "x \<and> False \<longleftrightarrow> False"
1.16 @@ -206,35 +212,30 @@
1.17    let
1.18      val thy = Thm.theory_of_cterm ct;
1.19      val t = Thm.term_of ct;
1.20 -  in
1.21 -    if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
1.22 -      (HOLogic.dest_Trueprop t) []
1.23 -    then ct
1.24 -    else @{cprop True} (*dummy*)
1.25 +    val dummy = @{cprop True};
1.26 +  in case try HOLogic.dest_Trueprop t
1.27 +   of SOME t' => if Code_ML.eval_term
1.28 +         ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' []
1.29 +       then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
1.30 +       else dummy
1.31 +    | NONE => dummy
1.32    end
1.33  *}
1.34
1.35 -method_setup eval = {*
1.36 -let
1.37 -  fun eval_tac thy =
1.38 -    CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
1.39 -in
1.40 -  Method.ctxt_args (fn ctxt =>
1.41 -    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
1.42 -end
1.43 -*} "solve goal by evaluation"
1.44 -
1.45 +ML {*
1.46 +fun gen_eval_method conv = Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD'
1.47 +  (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
1.48 +    THEN' rtac TrueI))
1.49 +*}
1.50
1.51 -method_setup evaluation = {*
1.52 -  Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
1.53 -*} "solve goal by evaluation"
1.54 -
1.55 +method_setup eval = {* gen_eval_method eval_oracle *}
1.56 +  "solve goal by evaluation"
1.57
1.58 -method_setup normalization = {*
1.59 -  Method.no_args (Method.SIMPLE_METHOD'
1.60 -    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
1.61 -    THEN' (fn k => TRY (rtac TrueI k))
1.62 -  ))
1.63 +method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
1.64 +  "solve goal by evaluation"
1.65 +
1.66 +method_setup normalization = {* (Method.no_args o Method.SIMPLE_METHOD')
1.67 +  (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
1.68  *} "solve goal by normalization"
1.69
1.70
```