equal
deleted
inserted
replaced
34 |
34 |
35 val comp_numeral = @{computation "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" :: nat} |
35 val comp_numeral = @{computation "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" :: nat} |
36 (fn post => post o HOLogic.mk_nat o int_of_nat o the); |
36 (fn post => post o HOLogic.mk_nat o int_of_nat o the); |
37 |
37 |
38 val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies |
38 val comp_bool = @{computation True False HOL.conj HOL.disj HOL.implies |
39 HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool } |
39 HOL.iff even "less_eq :: nat \<Rightarrow> _" "less :: nat \<Rightarrow> _" "HOL.eq :: nat \<Rightarrow> _" :: bool} |
40 (K the); |
40 (K the); |
|
41 |
|
42 val comp_check = @{computation_check Trueprop}; |
41 |
43 |
42 end |
44 end |
43 \<close> |
45 \<close> |
44 |
46 |
45 declare [[ML_source_trace = false]] |
47 declare [[ML_source_trace = false]] |
53 ML_val \<open> |
55 ML_val \<open> |
54 comp_bool @{context} @{term "fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 < fib (Suc (Suc 0))"} |
56 comp_bool @{context} @{term "fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 < fib (Suc (Suc 0))"} |
55 \<close> |
57 \<close> |
56 |
58 |
57 ML_val \<open> |
59 ML_val \<open> |
|
60 comp_check @{context} @{cprop "fib (Suc (Suc (Suc 0)) * Suc (Suc (Suc 0))) + Suc 0 > fib (Suc (Suc 0))"} |
|
61 \<close> |
|
62 |
|
63 ML_val \<open> |
58 comp_numeral @{context} @{term "Suc 42 + 7"} |
64 comp_numeral @{context} @{term "Suc 42 + 7"} |
59 |> Syntax.string_of_term @{context} |
65 |> Syntax.string_of_term @{context} |
60 |> writeln |
66 |> writeln |
61 \<close> |
67 \<close> |
62 |
68 |