summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Transfer.thy

changeset 47637 | 7a34395441ff |

parent 47636 | b786388b4b3a |

child 47658 | 7631f6f7873d |

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