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