Quelle  Computations.thy   Sprache: Isabelle

(*  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 🍋 🍋‹fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0›
  |> Syntax.string_of_term 🍋
  |> writeln
›
  
ML_val ‹
  comp_bool 🍋 🍋‹fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 < fib (Suc (Suc 0))›
›

ML_val ‹
  comp_check 🍋 🍋‹fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 > fib (Suc (Suc 0))›
›
  
ML_val ‹
  comp_numeral 🍋 🍋‹Suc 42 + 7›
  |> Syntax.string_of_term 🍋
  |> writeln
›

end