equal
deleted
inserted
replaced
884 |
884 |
885 text {* tyRel takes a type and builds a relation that a quantifier over this |
885 text {* tyRel takes a type and builds a relation that a quantifier over this |
886 type needs to respect. *} |
886 type needs to respect. *} |
887 ML {* |
887 ML {* |
888 fun tyRel ty rty rel lthy = |
888 fun tyRel ty rty rel lthy = |
889 if ty = rty then rel |
889 if ty = rty |
|
890 then rel |
890 else (case ty of |
891 else (case ty of |
891 Type (s, tys) => |
892 Type (s, tys) => |
892 let |
893 let |
893 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
894 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
894 val ty_out = ty --> ty --> @{typ bool}; |
895 val ty_out = ty --> ty --> @{typ bool}; |
895 val tys_out = tys_rel ---> ty_out; |
896 val tys_out = tys_rel ---> ty_out; |
896 in |
897 in |
897 (case (lookup (ProofContext.theory_of lthy) s) of |
898 (case (lookup (ProofContext.theory_of lthy) s) of |
898 SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys) |
899 SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys) |
899 | NONE => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}) |
900 | NONE => HOLogic.eq_const ty |
900 ) |
901 ) |
901 end |
902 end |
902 | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})) |
903 | _ => HOLogic.eq_const ty) |
903 *} |
904 *} |
904 |
905 |
905 ML {* |
906 ML {* |
906 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
907 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
907 *} |
908 *} |