src/HOL/HOL.thy
changeset 30929 d9343c0aac11
parent 30927 bc51b343f80d
child 30947 dd551284a300
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 15 15:38:30 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 15 15:52:37 2009 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* The basis of Higher-Order Logic *}
     1.5  
     1.6  theory HOL
     1.7 -imports Pure
     1.8 +imports Pure "~~/src/Tools/Code_Generator"
     1.9  uses
    1.10    ("Tools/hologic.ML")
    1.11    "~~/src/Tools/IsaPlanner/zipper.ML"
    1.12 @@ -27,15 +27,6 @@
    1.13    "~~/src/Tools/atomize_elim.ML"
    1.14    "~~/src/Tools/induct.ML"
    1.15    ("~~/src/Tools/induct_tacs.ML")
    1.16 -  "~~/src/Tools/value.ML"
    1.17 -  "~~/src/Tools/code/code_name.ML"
    1.18 -  "~~/src/Tools/code/code_wellsorted.ML" 
    1.19 -  "~~/src/Tools/code/code_thingol.ML"
    1.20 -  "~~/src/Tools/code/code_printer.ML"
    1.21 -  "~~/src/Tools/code/code_target.ML"
    1.22 -  "~~/src/Tools/code/code_ml.ML"
    1.23 -  "~~/src/Tools/code/code_haskell.ML"
    1.24 -  "~~/src/Tools/nbe.ML"
    1.25    ("Tools/recfun_codegen.ML")
    1.26  begin
    1.27  
    1.28 @@ -1673,35 +1664,259 @@
    1.29  *}
    1.30  
    1.31  
    1.32 -subsection {* Code generator basics -- see further theory @{text "Code_Setup"} *}
    1.33 +subsection {* Code generator setup *}
    1.34 +
    1.35 +subsubsection {* SML code generator setup *}
    1.36 +
    1.37 +use "Tools/recfun_codegen.ML"
    1.38 +
    1.39 +setup {*
    1.40 +  Codegen.setup
    1.41 +  #> RecfunCodegen.setup
    1.42 +*}
    1.43 +
    1.44 +types_code
    1.45 +  "bool"  ("bool")
    1.46 +attach (term_of) {*
    1.47 +fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.48 +*}
    1.49 +attach (test) {*
    1.50 +fun gen_bool i =
    1.51 +  let val b = one_of [false, true]
    1.52 +  in (b, fn () => term_of_bool b) end;
    1.53 +*}
    1.54 +  "prop"  ("bool")
    1.55 +attach (term_of) {*
    1.56 +fun term_of_prop b =
    1.57 +  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    1.58 +*}
    1.59  
    1.60 -text {* Equality *}
    1.61 +consts_code
    1.62 +  "Trueprop" ("(_)")
    1.63 +  "True"    ("true")
    1.64 +  "False"   ("false")
    1.65 +  "Not"     ("Bool.not")
    1.66 +  "op |"    ("(_ orelse/ _)")
    1.67 +  "op &"    ("(_ andalso/ _)")
    1.68 +  "If"      ("(if _/ then _/ else _)")
    1.69 +
    1.70 +setup {*
    1.71 +let
    1.72 +
    1.73 +fun eq_codegen thy defs dep thyname b t gr =
    1.74 +    (case strip_comb t of
    1.75 +       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    1.76 +     | (Const ("op =", _), [t, u]) =>
    1.77 +          let
    1.78 +            val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
    1.79 +            val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
    1.80 +            val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
    1.81 +          in
    1.82 +            SOME (Codegen.parens
    1.83 +              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
    1.84 +          end
    1.85 +     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    1.86 +         thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    1.87 +     | _ => NONE);
    1.88 +
    1.89 +in
    1.90 +  Codegen.add_codegen "eq_codegen" eq_codegen
    1.91 +end
    1.92 +*}
    1.93 +
    1.94 +subsubsection {* Equality *}
    1.95  
    1.96  class eq =
    1.97    fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.98    assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
    1.99  begin
   1.100  
   1.101 -lemma eq: "eq = (op =)"
   1.102 +lemma eq [code unfold, code inline del]: "eq = (op =)"
   1.103    by (rule ext eq_equals)+
   1.104  
   1.105  lemma eq_refl: "eq x x \<longleftrightarrow> True"
   1.106    unfolding eq by rule+
   1.107  
   1.108 +lemma equals_eq [code inline, code]: "(op =) \<equiv> eq"
   1.109 +  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
   1.110 +
   1.111 +declare equals_eq [symmetric, code post]
   1.112 +
   1.113  end
   1.114  
   1.115 -text {* Module setup *}
   1.116 +subsubsection {* Generic code generator foundation *}
   1.117 +
   1.118 +text {* Datatypes *}
   1.119 +
   1.120 +code_datatype True False
   1.121 +
   1.122 +code_datatype "TYPE('a\<Colon>{})"
   1.123 +
   1.124 +code_datatype Trueprop "prop"
   1.125 +
   1.126 +text {* Code equations *}
   1.127 +
   1.128 +lemma [code]:
   1.129 +  shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 
   1.130 +    and "(False \<Longrightarrow> Q) \<equiv> Trueprop True" 
   1.131 +    and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" 
   1.132 +    and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)
   1.133 +
   1.134 +lemma [code]:
   1.135 +  shows "False \<and> x \<longleftrightarrow> False"
   1.136 +    and "True \<and> x \<longleftrightarrow> x"
   1.137 +    and "x \<and> False \<longleftrightarrow> False"
   1.138 +    and "x \<and> True \<longleftrightarrow> x" by simp_all
   1.139 +
   1.140 +lemma [code]:
   1.141 +  shows "False \<or> x \<longleftrightarrow> x"
   1.142 +    and "True \<or> x \<longleftrightarrow> True"
   1.143 +    and "x \<or> False \<longleftrightarrow> x"
   1.144 +    and "x \<or> True \<longleftrightarrow> True" by simp_all
   1.145 +
   1.146 +lemma [code]:
   1.147 +  shows "\<not> True \<longleftrightarrow> False"
   1.148 +    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
   1.149  
   1.150 -use "Tools/recfun_codegen.ML"
   1.151 +lemmas [code] = Let_def if_True if_False
   1.152 +
   1.153 +lemmas [code, code unfold, symmetric, code post] = imp_conv_disj
   1.154 +
   1.155 +text {* Equality *}
   1.156 +
   1.157 +declare simp_thms(6) [code nbe]
   1.158 +
   1.159 +hide (open) const eq
   1.160 +hide const eq
   1.161 +
   1.162 +setup {*
   1.163 +  Code_Unit.add_const_alias @{thm equals_eq}
   1.164 +*}
   1.165 +
   1.166 +text {* Cases *}
   1.167 +
   1.168 +lemma Let_case_cert:
   1.169 +  assumes "CASE \<equiv> (\<lambda>x. Let x f)"
   1.170 +  shows "CASE x \<equiv> f x"
   1.171 +  using assms by simp_all
   1.172 +
   1.173 +lemma If_case_cert:
   1.174 +  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
   1.175 +  shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
   1.176 +  using assms by simp_all
   1.177 +
   1.178 +setup {*
   1.179 +  Code.add_case @{thm Let_case_cert}
   1.180 +  #> Code.add_case @{thm If_case_cert}
   1.181 +  #> Code.add_undefined @{const_name undefined}
   1.182 +*}
   1.183 +
   1.184 +code_abort undefined
   1.185 +
   1.186 +subsubsection {* Generic code generator preprocessor *}
   1.187  
   1.188  setup {*
   1.189 -  Code_ML.setup
   1.190 -  #> Code_Haskell.setup
   1.191 -  #> Nbe.setup
   1.192 -  #> Codegen.setup
   1.193 -  #> RecfunCodegen.setup
   1.194 +  Code.map_pre (K HOL_basic_ss)
   1.195 +  #> Code.map_post (K HOL_basic_ss)
   1.196  *}
   1.197  
   1.198 +subsubsection {* Generic code generator target languages *}
   1.199 +
   1.200 +text {* type bool *}
   1.201 +
   1.202 +code_type bool
   1.203 +  (SML "bool")
   1.204 +  (OCaml "bool")
   1.205 +  (Haskell "Bool")
   1.206 +
   1.207 +code_const True and False and Not and "op &" and "op |" and If
   1.208 +  (SML "true" and "false" and "not"
   1.209 +    and infixl 1 "andalso" and infixl 0 "orelse"
   1.210 +    and "!(if (_)/ then (_)/ else (_))")
   1.211 +  (OCaml "true" and "false" and "not"
   1.212 +    and infixl 4 "&&" and infixl 2 "||"
   1.213 +    and "!(if (_)/ then (_)/ else (_))")
   1.214 +  (Haskell "True" and "False" and "not"
   1.215 +    and infixl 3 "&&" and infixl 2 "||"
   1.216 +    and "!(if (_)/ then (_)/ else (_))")
   1.217 +
   1.218 +code_reserved SML
   1.219 +  bool true false not
   1.220 +
   1.221 +code_reserved OCaml
   1.222 +  bool not
   1.223 +
   1.224 +text {* using built-in Haskell equality *}
   1.225 +
   1.226 +code_class eq
   1.227 +  (Haskell "Eq")
   1.228 +
   1.229 +code_const "eq_class.eq"
   1.230 +  (Haskell infixl 4 "==")
   1.231 +
   1.232 +code_const "op ="
   1.233 +  (Haskell infixl 4 "==")
   1.234 +
   1.235 +text {* undefined *}
   1.236 +
   1.237 +code_const undefined
   1.238 +  (SML "!(raise/ Fail/ \"undefined\")")
   1.239 +  (OCaml "failwith/ \"undefined\"")
   1.240 +  (Haskell "error/ \"undefined\"")
   1.241 +
   1.242 +subsubsection {* Evaluation and normalization by evaluation *}
   1.243 +
   1.244 +setup {*
   1.245 +  Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
   1.246 +*}
   1.247 +
   1.248 +ML {*
   1.249 +structure Eval_Method =
   1.250 +struct
   1.251 +
   1.252 +val eval_ref : (unit -> bool) option ref = ref NONE;
   1.253 +
   1.254 +end;
   1.255 +*}
   1.256 +
   1.257 +oracle eval_oracle = {* fn ct =>
   1.258 +  let
   1.259 +    val thy = Thm.theory_of_cterm ct;
   1.260 +    val t = Thm.term_of ct;
   1.261 +    val dummy = @{cprop True};
   1.262 +  in case try HOLogic.dest_Trueprop t
   1.263 +   of SOME t' => if Code_ML.eval_term
   1.264 +         ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
   1.265 +       then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
   1.266 +       else dummy
   1.267 +    | NONE => dummy
   1.268 +  end
   1.269 +*}
   1.270 +
   1.271 +ML {*
   1.272 +fun gen_eval_method conv ctxt = SIMPLE_METHOD'
   1.273 +  (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
   1.274 +    THEN' rtac TrueI)
   1.275 +*}
   1.276 +
   1.277 +method_setup eval = {* Scan.succeed (gen_eval_method eval_oracle) *}
   1.278 +  "solve goal by evaluation"
   1.279 +
   1.280 +method_setup evaluation = {* Scan.succeed (gen_eval_method Codegen.evaluation_conv) *}
   1.281 +  "solve goal by evaluation"
   1.282 +
   1.283 +method_setup normalization = {*
   1.284 +  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
   1.285 +*} "solve goal by normalization"
   1.286 +
   1.287 +subsubsection {* Quickcheck *}
   1.288 +
   1.289 +setup {*
   1.290 +  Quickcheck.add_generator ("SML", Codegen.test_term)
   1.291 +*}
   1.292 +
   1.293 +quickcheck_params [size = 5, iterations = 50]
   1.294 +
   1.295  
   1.296  subsection {* Nitpick hooks *}
   1.297