|
(* Title: HOL/ex/Computations.thy
Author: Florian Haftmann, TU Muenchen
*)
section \<open>Simple example for computations generated by the code generator\<close>
theory Computations
imports Main
begin
fun even :: "nat \ bool"
where "even 0 \ True"
| "even (Suc 0) \ False"
| "even (Suc (Suc n)) \ even n"
fun fib :: "nat \ nat"
where "fib 0 = 0"
| "fib (Suc 0) = Suc 0"
| "fib (Suc (Suc n)) = fib (Suc n) + fib n"
declare [[ML_source_trace]]
ML \<open>
local
fun int_of_nat @{code "0 :: nat"} = 0
| int_of_nat (@{code Suc} n) = int_of_nat n + 1;
in
val comp_nat = @{computation nat
terms: "plus :: nat \_" "times :: nat \ _" fib
datatypes: nat}
(fn post => post o HOLogic.mk_nat o int_of_nat o the);
val comp_numeral = @{computation nat
terms: "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat"}
(fn post => post o HOLogic.mk_nat o int_of_nat o the);
val comp_bool = @{computation bool
terms: HOL.conj HOL.disj HOL.implies
HOL.iff even "less_eq :: nat \ _" "less :: nat \ _" "HOL.eq :: nat \ _"
datatypes: bool}
(K the);
val comp_check = @{computation_check terms: Trueprop};
val comp_dummy = @{computation "(nat \ unit) option"
datatypes: "(nat \ unit) option"}
end
\<close>
declare [[ML_source_trace = false]]
ML_val \<open>
comp_nat \<^context> \<^term>\<open>fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0\<close>
|> Syntax.string_of_term \<^context>
|> writeln
\<close>
ML_val \<open>
comp_bool \<^context> \<^term>\<open>fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 < fib (Suc (Suc 0))\<close>
\<close>
ML_val \<open>
comp_check \<^context> \<^cprop>\<open>fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 > fib (Suc (Suc 0))\<close>
\<close>
ML_val \<open>
comp_numeral \<^context> \<^term>\<open>Suc 42 + 7\<close>
|> Syntax.string_of_term \<^context>
|> writeln
\<close>
end
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
