1(* Title: HOL/ex/Computations.thy 2 Author: Florian Haftmann, TU Muenchen 3*) 4 5section \<open>Simple example for computations generated by the code generator\<close> 6 7theory Computations 8 imports Main 9begin 10 11fun even :: "nat \<Rightarrow> bool" 12 where "even 0 \<longleftrightarrow> True" 13 | "even (Suc 0) \<longleftrightarrow> False" 14 | "even (Suc (Suc n)) \<longleftrightarrow> even n" 15 16fun fib :: "nat \<Rightarrow> nat" 17 where "fib 0 = 0" 18 | "fib (Suc 0) = Suc 0" 19 | "fib (Suc (Suc n)) = fib (Suc n) + fib n" 20 21declare [[ML_source_trace]] 22 23ML \<open> 24local 25 26fun int_of_nat @{code "0 :: nat"} = 0 27 | int_of_nat (@{code Suc} n) = int_of_nat n + 1; 28 29in 30 31val comp_nat = @{computation nat 32 terms: "plus :: nat \<Rightarrow>_" "times :: nat \<Rightarrow> _" fib 33 datatypes: nat} 34 (fn post => post o HOLogic.mk_nat o int_of_nat o the); 35 36val comp_numeral = @{computation nat 37 terms: "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat"} 38 (fn post => post o HOLogic.mk_nat o int_of_nat o the); 39 40val comp_bool = @{computation bool 41 terms: HOL.conj HOL.disj HOL.implies 42 HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" 43 datatypes: bool} 44 (K the); 45 46val comp_check = @{computation_check terms: Trueprop}; 47 48val comp_dummy = @{computation "(nat \<times> unit) option" 49 datatypes: "(nat \<times> unit) option"} 50 51end 52\<close> 53 54declare [[ML_source_trace = false]] 55 56ML_val \<open> 57 comp_nat \<^context> \<^term>\<open>fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0\<close> 58 |> Syntax.string_of_term \<^context> 59 |> writeln 60\<close> 61 62ML_val \<open> 63 comp_bool \<^context> \<^term>\<open>fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 < fib (Suc (Suc 0))\<close> 64\<close> 65 66ML_val \<open> 67 comp_check \<^context> \<^cprop>\<open>fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 > fib (Suc (Suc 0))\<close> 68\<close> 69 70ML_val \<open> 71 comp_numeral \<^context> \<^term>\<open>Suc 42 + 7\<close> 72 |> Syntax.string_of_term \<^context> 73 |> writeln 74\<close> 75 76end 77