equal
deleted
inserted
replaced
41 text{* |
41 text{* |
42 Note that the premise is executable once we have defined |
42 Note that the premise is executable once we have defined |
43 @{const factor}. Here is a trivial definition in ML: |
43 @{const factor}. Here is a trivial definition in ML: |
44 *} |
44 *} |
45 |
45 |
46 ML{*fun factor n = if n = 4 then 2 else 1*} |
46 ML %grayML{*fun factor n = if n = 4 then 2 else 1*} |
47 |
47 |
48 text{* |
48 text{* |
49 Of course this trivial definition of @{const factor} could have been given |
49 Of course this trivial definition of @{const factor} could have been given |
50 directly in HOL rather than ML. But by going to the ML level, all of ML is |
50 directly in HOL rather than ML. But by going to the ML level, all of ML is |
51 at our disposal, including arrays and references, features that are less |
51 at our disposal, including arrays and references, features that are less |
96 @{text list} by the corresponding ML-type. Thus the following variation |
96 @{text list} by the corresponding ML-type. Thus the following variation |
97 on @{const factor} also works: |
97 on @{const factor} also works: |
98 *} |
98 *} |
99 |
99 |
100 consts factor2 :: "nat \<Rightarrow> nat list" (*<*)(*>*) |
100 consts factor2 :: "nat \<Rightarrow> nat list" (*<*)(*>*) |
101 ML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*) |
101 ML %grayML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*) |
102 code_const factor2 (SML "factor2") |
102 code_const factor2 (SML "factor2") |
103 |
103 |
104 value "factor2 4" |
104 value "factor2 4" |
105 |
105 |
106 text{* |
106 text{* |
134 arbitrarily chosen) that contains the datatype @{typ result}. The list |
134 arbitrarily chosen) that contains the datatype @{typ result}. The list |
135 of constructors (but not their types) needs to be given. Now we can |
135 of constructors (but not their types) needs to be given. Now we can |
136 write ML-code that uses this datatype: |
136 write ML-code that uses this datatype: |
137 *} |
137 *} |
138 |
138 |
139 ML{*fun factor' n = if n = 4 then Result.Factor 2 else Result.Prime*} |
139 ML %grayML{*fun factor' n = if n = 4 then Result.Factor 2 else Result.Prime*} |
140 |
140 |
141 text{* |
141 text{* |
142 Finally we can link the HOL and ML version of @{const factor'} as |
142 Finally we can link the HOL and ML version of @{const factor'} as |
143 before: |
143 before: |
144 *} |
144 *} |