equal
deleted
inserted
replaced
24 val strip_args: int -> term -> term |
24 val strip_args: int -> term -> term |
25 val all_args_conv: conv -> conv |
25 val all_args_conv: conv -> conv |
26 val is_Type: typ -> bool |
26 val is_Type: typ -> bool |
27 val is_fun_rel: term -> bool |
27 val is_fun_rel: term -> bool |
28 val relation_types: typ -> typ * typ |
28 val relation_types: typ -> typ * typ |
29 val bottom_rewr_conv: thm list -> conv |
|
30 val mk_HOL_eq: thm -> thm |
29 val mk_HOL_eq: thm -> thm |
31 val safe_HOL_meta_eq: thm -> thm |
30 val safe_HOL_meta_eq: thm -> thm |
32 end; |
31 end; |
33 |
32 |
34 |
33 |
105 fun relation_types typ = |
104 fun relation_types typ = |
106 case strip_type typ of |
105 case strip_type typ of |
107 ([typ1, typ2], @{typ bool}) => (typ1, typ2) |
106 ([typ1, typ2], @{typ bool}) => (typ1, typ2) |
108 | _ => error "relation_types: not a relation" |
107 | _ => error "relation_types: not a relation" |
109 |
108 |
110 fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context} |
|
111 |
|
112 fun mk_HOL_eq r = r RS @{thm meta_eq_to_obj_eq} |
109 fun mk_HOL_eq r = r RS @{thm meta_eq_to_obj_eq} |
113 |
110 |
114 fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r |
111 fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r |
115 |
112 |
116 end; |
113 end; |