equal
deleted
inserted
replaced
899 |
899 |
900 text {* tyRel takes a type and builds a relation that a quantifier over this |
900 text {* tyRel takes a type and builds a relation that a quantifier over this |
901 type needs to respect. *} |
901 type needs to respect. *} |
902 ML {* |
902 ML {* |
903 fun tyRel ty rty rel lthy = |
903 fun tyRel ty rty rel lthy = |
904 if ty = rty then rel |
904 if ty = rty |
|
905 then rel |
905 else (case ty of |
906 else (case ty of |
906 Type (s, tys) => |
907 Type (s, tys) => |
907 let |
908 let |
908 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
909 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
909 val ty_out = ty --> ty --> @{typ bool}; |
910 val ty_out = ty --> ty --> @{typ bool}; |
910 val tys_out = tys_rel ---> ty_out; |
911 val tys_out = tys_rel ---> ty_out; |
911 in |
912 in |
912 (case (lookup (ProofContext.theory_of lthy) s) of |
913 (case (lookup (ProofContext.theory_of lthy) s) of |
913 SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys) |
914 SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys) |
914 | NONE => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}) |
915 | NONE => HOLogic.eq_const ty |
915 ) |
916 ) |
916 end |
917 end |
917 | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})) |
918 | _ => HOLogic.eq_const ty) |
918 *} |
919 *} |
919 |
920 |
920 ML {* |
921 ML {* |
921 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
922 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
922 *} |
923 *} |