| COM | combin_begin | ************ COMBIN ************ |
| COM | combin_ancestors | bool |
| COM | combin_Nuprl_defs | -------------- |
| COM | combin_Nuprl_aux | -------------- |
| COM | combin_HOL_type_defs | -------------- |
| COM | combin_HOL_const_defs | -------------- |
| ABS | ho | o ==  f:'a   'b. g:'a 'b. f o g |
| ML | ho_ml | add_to_simpset `hol_to_nuprl` (hdef_to_simp "ho");; add_info `direct_
old_hdef` `ho`;; |
| ABS | hk | k == x:'a. y:'b. x |
| ML | hk_ml | add_to_simpset `hol_to_nuprl` (hdef_to_simp "hk");; add_info `direct_
old_hdef` `hk`;; |
| ABS | hs | s == f:'a 'b 'c. g:'a 'b. x:'a. f x (g x) |
| ML | hs_ml | add_to_simpset `hol_to_nuprl` (hdef_to_simp "hs");; add_info `direct_
old_hdef` `hs`;; |
| ABS | hi | i == x:'a. x |
| ML | hi_ml | add_to_simpset `hol_to_nuprl` (hdef_to_simp "hi");; add_info `direct_
old_hdef` `hi`;; |
| COM | combin_HOL_obligations | -------------- |
| THM | ho_wf |  'b,'c,'a:stype. o  ('b 'c) ('a 'b) 'a 'c |
| THM | hk_wf | 'a,'b:stype. k 'a 'b 'a |
| THM | hs_wf | 'a,'b,'c:stype. s ('a 'b 'c) ('a 'b) 'a 'c |
| THM | hi_wf | 'a:stype. i 'a 'a |
| THM | ho_def | 'c,'b,'a:stype.
 (all
(f:'b 'c. all (g:'a 'b. equal (o f g) (x:'a. f (g x))))) |
| THM | hk_def | 'a,'b:stype. (equal k (x:'a. y:'b. x)) |
| THM | hs_def | 'c,'b,'a:stype.
(equal s (f:'a 'b 'c. g:'a 'b. x:'a. f x (g x))) |
| THM | hi_def | 'a:stype. (equal i (s k k)) |
| COM | combin_HOL_theorems | -------------- |
| THM | ho_thm | 'b,'c,'a:stype.
(all
(f:'b 'c. all
(g:'a 'b. all (x:'a. equal (o f g x) (f (g x)))))) |
| THM | ho_assoc | 'a,'c,'d,'b:stype.
(all
(f:'c 'd. all
(g:'b 'c. all
(h:'a 'b. equal (o f (o g h)) (o (o f g) h))))) |
| THM | hk_thm | 'a,'b:stype. (all (x:'a. all (y:'b. equal (k x y) x))) |
| THM | hs_thm | 'a,'b,'c:stype.
(all
(f:'a 'b 'c. all
(g:'a 'b. all (x:'a. equal (s f g x) (f x (g x)))))) |
| THM | hi_thm | 'a:stype. (all (x:'a. equal (i x) x)) |
| THM | hi_o_id | 'b,'a:stype.
(all (f:'a 'b. and (equal (o i f) f) (equal (o f i) f))) |
| COM | combin_Nuprl_theorems | -------------- |
| THM | o_thm | 'b,'c,'a:stype. x:'b 'c. x@0:'a 'b. x@1:'a.
(x o x@0) x@1 = x (x@0 x@1) |
| THM | o_assoc | 'a,'c,'d,'b:stype. x:'c 'd. x@0:'b 'c. x@1:'a 'b.
x o (x@0 o x@1) = (x o x@0) o x@1 |
| THM | k_thm | 'a,'b:stype. x:'a. x@0:'b. x = x |
| THM | s_thm | 'a,'b,'c:stype. x:'a 'b 'c. x@0:'a 'b. x@1:'a.
x x@1 (x@0 x@1) = x x@1 (x@0 x@1) |
| THM | i_thm | 'a:stype. x:'a. x = x |
| THM | i_o_id | 'b,'a:stype. x:'a 'b. (x:'b. x) o x = x  x o (x:'a. x) = x |
| ML | combin_simpset | map (add_to_simpset `combin`)
(
[pattern_unfold_op `compose_unfold` `compose` [ (x o x@0) x@1 ]
;lemma_to_simp `o_assoc`
]
@ lemma_simps `i_o_id`
)
;; |
| COM | combin_end | ******************************** |