# Theory Computations

theory Computations
imports Main
```(*  Title:      HOL/ex/Computations.thy
Author:     Florian Haftmann, TU Muenchen
*)

section ‹Simple example for computations generated by the code generator›

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 ‹
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
›

declare [[ML_source_trace = false]]

ML_val ‹
comp_nat @{context} @{term "fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0"}
|> Syntax.string_of_term @{context}
|> writeln
›

ML_val ‹
comp_bool @{context} @{term "fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 < fib (Suc (Suc 0))"}
›

ML_val ‹
comp_check @{context} @{cprop "fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 > fib (Suc (Suc 0))"}
›

ML_val ‹
comp_numeral @{context} @{term "Suc 42 + 7"}
|> Syntax.string_of_term @{context}
|> writeln
›

end
```