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