File: wordn_ints.th

package info (click to toggle)

hol88 2.02.19940316-35.1

links: PTS
area: main
in suites: bullseye
size: 66,004 kB
sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,095; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5

file content (2 lines) | stat: -rw-r--r-- 6,897 bytes

parent folder | download | duplicates (9)

1
2

(setq %theorydata '((parents more_integers wordn_num integer more_gp HOL) (types) (nametypes) (operators (TWOS_COMPLEMENT fun (list (bool)) (list (bool))) (TWOS_COMP fun (list (bool)) (prod (bool) (list (bool)))) (iVal fun (list (bool)) (integer))) (paired-infixes) (curried-infixes) (predicates) (version . "2.01 (Franz: pre-release)") (stamp . 716732443)))
(setq %theorems '((sharetypes 2 (|,%1| prod (bool) (list (bool))) (l%0 list (bool))) (axiom (TWOS_COMPLEMENT pred HOL_ASSERT comb ((const HOL_DEFINITION) comb ((const !) abs ((var l %t . l%0) comb ((comb ((const =) comb ((const TWOS_COMPLEMENT) var l))) comb ((const SND) comb ((const TWOS_COMP) var l)) %t . l%0) bool)))) (TWOS_COMP pred HOL_ASSERT comb ((const HOL_DEFINITION) comb ((comb ((const |/\\|) comb ((comb ((const =) comb ((const TWOS_COMP) const NIL))) comb ((comb ((const |,|) const T)) const NIL %t . l%0) %t . |,%1|))) comb ((const !) abs ((var x bool) comb ((const !) abs ((var xs %t . l%0) comb ((comb ((const =) comb ((const TWOS_COMP) comb ((comb ((const CONS) var x bool)) var xs %t . l%0)))) comb ((comb ((const LET) abs ((var xp %t . |,%1|) comb ((comb ((const |,|) comb ((comb ((const |/\\|) comb ((const ~) var x))) comb ((const FST) var xp %t . |,%1|)))) comb ((comb ((const CONS) comb ((comb ((const =) var x bool)) comb ((const FST) var xp %t . |,%1|) bool) bool)) comb ((const SND) var xp %t . |,%1|) %t . l%0) %t . l%0) %t . |,%1|))) comb ((const TWOS_COMP) var xs)) %t . |,%1|) bool)) bool))))) (iVal pred HOL_ASSERT comb ((const HOL_DEFINITION) comb ((const !) abs ((var l %t . l%0) comb ((comb ((const =) comb ((const iVal) var l))) comb ((comb ((comb ((const COND) comb ((const NULL) var l %t . l%0) bool)) comb ((const INT) const |0|))) comb ((comb ((const plus) comb ((const neg) comb ((const INT) comb ((comb ((const *) comb ((const BV) comb ((const HD) var l %t . l%0)))) comb ((comb ((const EXP) const |2|)) comb ((const LENGTH) comb ((const TL) var l %t . l%0) %t . l%0))))))) comb ((const INT) comb ((const VAL) comb ((const TL) var l %t . l%0))))) integer) bool))))) (fact (LSHIFT_n_iVal pred HOL_ASSERT comb ((const !) abs ((var l1 %t . l%0) comb ((comb ((const ==>) comb ((comb ((const =) comb ((const VAL) var l1))) const |0|))) comb ((const !) abs ((var l2 %t . l%0) comb ((comb ((const =) comb ((const iVal) comb ((comb ((const APPEND) var l2 %t . l%0)) var l1 %t . l%0)))) comb ((comb ((const times) comb ((const INT) comb ((comb ((const EXP) const |2|)) comb ((const LENGTH) var l1 %t . l%0))))) comb ((const iVal) var l2))) bool))))) bool) (LSHIFT_n_VAL pred HOL_ASSERT comb ((const !) abs ((var l1 %t . l%0) comb ((comb ((const ==>) comb ((comb ((const =) comb ((const VAL) var l1))) const |0|))) comb ((const !) abs ((var l2 %t . l%0) comb ((comb ((const =) comb ((const VAL) comb ((comb ((const APPEND) var l2 %t . l%0)) var l1 %t . l%0)))) comb ((comb ((const *) comb ((comb ((const EXP) const |2|)) comb ((const LENGTH) var l1 %t . l%0)))) comb ((const VAL) var l2))) bool))))) bool) (LSHIFT_iVal pred HOL_ASSERT comb ((const !) abs ((var l %t . l%0) comb ((comb ((const =) comb ((const iVal) comb ((comb ((const APPEND) var l %t . l%0)) comb ((comb ((const CONS) const F)) const NIL %t . l%0) %t . l%0)))) comb ((comb ((const times) comb ((const INT) const |2|))) comb ((const iVal) var l))) bool)) bool) (LSHIFT_VAL pred HOL_ASSERT comb ((const !) abs ((var l %t . l%0) comb ((comb ((const =) comb ((const VAL) comb ((comb ((const APPEND) var l %t . l%0)) comb ((comb ((const CONS) const F)) const NIL %t . l%0) %t . l%0)))) comb ((comb ((const *) const |2|)) comb ((const VAL) var l))) bool)) bool) (TWOS_COMP_iVal pred HOL_ASSERT comb ((const !) abs ((var ll %t . l%0) comb ((const !) abs ((var l bool) comb ((comb ((const ==>) comb ((const ~) comb ((comb ((const =) comb ((const iVal) comb ((comb ((const CONS) var l bool)) var ll %t . l%0)))) comb ((const neg) comb ((const INT) comb ((comb ((const EXP) const |2|)) comb ((const LENGTH) var ll %t . l%0)))))))) comb ((comb ((const =) comb ((const iVal) comb ((const TWOS_COMPLEMENT) comb ((comb ((const CONS) var l bool)) var ll %t . l%0))))) comb ((const neg) comb ((const iVal) comb ((comb ((const CONS) var l bool)) var ll %t . l%0))))))) bool)) bool) (TWOS_COMP_MOST_NEG_iVal pred HOL_ASSERT comb ((const !) abs ((var ll %t . l%0) comb ((const !) abs ((var l bool) comb ((comb ((const ==>) comb ((comb ((const =) comb ((const iVal) comb ((comb ((const CONS) var l bool)) var ll %t . l%0)))) comb ((const neg) comb ((const INT) comb ((comb ((const EXP) const |2|)) comb ((const LENGTH) var ll %t . l%0))))))) comb ((comb ((const =) comb ((const iVal) comb ((const TWOS_COMPLEMENT) comb ((comb ((const CONS) var l bool)) var ll %t . l%0))))) comb ((const iVal) comb ((comb ((const CONS) var l bool)) var ll %t . l%0)))))) bool)) bool) (MOST_NEG_LEMMA pred HOL_ASSERT comb ((const !) abs ((var ll %t . l%0) comb ((const !) abs ((var l bool) comb ((comb ((const =) comb ((comb ((const =) comb ((const iVal) comb ((comb ((const CONS) var l bool)) var ll %t . l%0)))) comb ((const neg) comb ((const INT) comb ((comb ((const EXP) const |2|)) comb ((const LENGTH) var ll %t . l%0))))) bool)) comb ((comb ((const |/\\|) var l)) comb ((comb ((const =) comb ((const VAL) var ll))) const |0|))) bool)) bool)) bool) (iVal_ONTO_LEMMA pred HOL_ASSERT comb ((const !) abs ((var n integer) comb ((const !) abs ((var m num) comb ((comb ((const ==>) comb ((comb ((const |/\\|) comb ((comb ((const below_eq) comb ((const neg) comb ((const INT) comb ((comb ((const EXP) const |2|)) var m))))) var n))) comb ((comb ((const below) var n)) comb ((const INT) comb ((comb ((const EXP) const |2|)) var m)))))) comb ((const ?) abs ((var l %t . l%0) comb ((comb ((const |/\\|) comb ((comb ((const =) comb ((const LENGTH) var l %t . l%0) num)) comb ((const SUC) var m)))) comb ((comb ((const =) var n integer)) comb ((const iVal) var l)))))))) bool)) bool) (iVal_ONE_ONE pred HOL_ASSERT comb ((const !) abs ((var l1 %t . l%0) comb ((const !) abs ((var l2 %t . l%0) comb ((comb ((const ==>) comb ((comb ((const =) comb ((const LENGTH) var l1 %t . l%0) num)) comb ((const LENGTH) var l2 %t . l%0) num))) comb ((comb ((const ==>) comb ((comb ((const =) comb ((const iVal) var l1))) comb ((const iVal) var l2)))) comb ((comb ((const =) var l1 %t . l%0)) var l2 %t . l%0))))) bool)) bool) (iVal_BOUNDS pred HOL_ASSERT comb ((const !) abs ((var l %t . l%0) comb ((const !) abs ((var a bool) comb ((comb ((const |/\\|) comb ((comb ((const below_eq) comb ((const neg) comb ((const INT) comb ((comb ((const EXP) const |2|)) comb ((const LENGTH) var l %t . l%0)))))) comb ((const iVal) comb ((comb ((const CONS) var a bool)) var l %t . l%0))))) comb ((comb ((const below) comb ((const iVal) comb ((comb ((const CONS) var a bool)) var l %t . l%0)))) comb ((const INT) comb ((comb ((const EXP) const |2|)) comb ((const LENGTH) var l %t . l%0))))))) bool)) bool))))