summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Fri, 20 Apr 2012 22:05:07 +0200 | |

changeset 47637 | 7a34395441ff |

parent 47636 | b786388b4b3a |

child 47638 | 4923b8ba0f49 |

add transfer rule for nat_case

--- a/src/HOL/Transfer.thy Fri Apr 20 22:54:13 2012 +0200 +++ b/src/HOL/Transfer.thy Fri Apr 20 22:05:07 2012 +0200 @@ -252,13 +252,17 @@ shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" unfolding fun_upd_def [abs_def] by transfer_prover -lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)" - by auto +lemma nat_case_transfer [transfer_rule]: + "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case" + unfolding fun_rel_def by (simp split: nat.split) text {* Fallback rule for transferring universal quantifiers over correspondence relations that are not bi-total, and do not have custom transfer rules (e.g. relations between function types). *} +lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)" + by auto + lemma Domainp_forall_transfer [transfer_rule]: assumes "right_total A" shows "((A ===> op =) ===> op =)