author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 68660 | 4ce18f389f53 |
permissions | -rw-r--r-- |
64959 | 1 |
(* Title: HOL/ex/Computations.thy |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
section \<open>Simple example for computations generated by the code generator\<close> |
|
6 |
||
7 |
theory Computations |
|
68660 | 8 |
imports Main |
64959 | 9 |
begin |
10 |
||
11 |
fun 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 |
||
16 |
fun 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 |
||
21 |
declare [[ML_source_trace]] |
|
22 |
||
23 |
ML \<open> |
|
24 |
local |
|
25 |
||
26 |
fun int_of_nat @{code "0 :: nat"} = 0 |
|
27 |
| int_of_nat (@{code Suc} n) = int_of_nat n + 1; |
|
28 |
||
29 |
in |
|
30 |
||
64992
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
31 |
val comp_nat = @{computation nat |
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
32 |
terms: "plus :: nat \<Rightarrow>_" "times :: nat \<Rightarrow> _" fib |
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
33 |
datatypes: nat} |
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
34 |
(fn post => post o HOLogic.mk_nat o int_of_nat o the); |
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
35 |
|
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
36 |
val comp_numeral = @{computation nat |
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
37 |
terms: "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat"} |
64988 | 38 |
(fn post => post o HOLogic.mk_nat o int_of_nat o the); |
64959 | 39 |
|
64992
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
40 |
val comp_bool = @{computation bool |
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
41 |
terms: HOL.conj HOL.disj HOL.implies |
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
42 |
HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" |
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
43 |
datatypes: bool} |
64988 | 44 |
(K the); |
64959 | 45 |
|
64992
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
46 |
val comp_check = @{computation_check terms: Trueprop}; |
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
47 |
|
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
48 |
val comp_dummy = @{computation "(nat \<times> unit) option" |
41e2c3617582
extended syntax allows to include datatype constructors directly in computations
haftmann
parents:
64989
diff
changeset
|
49 |
datatypes: "(nat \<times> unit) option"} |
64989 | 50 |
|
64959 | 51 |
end |
52 |
\<close> |
|
53 |
||
54 |
declare [[ML_source_trace = false]] |
|
55 |
||
56 |
ML_val \<open> |
|
69597 | 57 |
comp_nat \<^context> \<^term>\<open>fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0\<close> |
58 |
|> Syntax.string_of_term \<^context> |
|
64959 | 59 |
|> writeln |
60 |
\<close> |
|
61 |
||
62 |
ML_val \<open> |
|
69597 | 63 |
comp_bool \<^context> \<^term>\<open>fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 < fib (Suc (Suc 0))\<close> |
64959 | 64 |
\<close> |
65 |
||
66 |
ML_val \<open> |
|
69597 | 67 |
comp_check \<^context> \<^cprop>\<open>fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 > fib (Suc (Suc 0))\<close> |
64989 | 68 |
\<close> |
69 |
||
70 |
ML_val \<open> |
|
69597 | 71 |
comp_numeral \<^context> \<^term>\<open>Suc 42 + 7\<close> |
72 |
|> Syntax.string_of_term \<^context> |
|
64959 | 73 |
|> writeln |
74 |
\<close> |
|
75 |
||
76 |
end |