diff options
| -rw-r--r-- | backends/hol4/divDefLib.sml | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml index 08c8b91a..3ecb32df 100644 --- a/backends/hol4/divDefLib.sml +++ b/backends/hol4/divDefLib.sml @@ -1213,6 +1213,32 @@ val def_qt = ‘ val even_def = DefineDiv def_qt +(* Complexigying the above definition *) +val def_qt = ‘ + (even (i : int) : bool result = + if i = 0 then + do + b <- Return T; + Return b + od + else do + b <- odd (i - 1); + Return b + od + ) /\ + (odd (i : int) : bool result = + if i = 0 then + do + b <- Return F; + Return b + od + else do + b <- even (i - 1); + Return b + od) +’ + +val even_def = DefineDiv def_qt Datatype: list_t = |