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

src/HOL/Transfer.thy

changeset 47627 | 2b1d3eda59eb |

parent 47625 | 10cfaf771687 |

child 47635 | ebb79474262c |

1.1 --- a/src/HOL/Transfer.thy Fri Apr 20 15:34:33 2012 +0200 1.2 +++ b/src/HOL/Transfer.thy Fri Apr 20 15:49:45 2012 +0200 1.3 @@ -252,7 +252,26 @@ 1.4 shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" 1.5 unfolding fun_upd_def [abs_def] by correspondence 1.6 1.7 -lemmas transfer_forall_parametric [transfer_rule] 1.8 - = All_parametric [folded transfer_forall_def] 1.9 +lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)" 1.10 + by auto 1.11 + 1.12 +text {* Fallback rule for transferring universal quantifiers over 1.13 + correspondence relations that are not bi-total, and do not have 1.14 + custom transfer rules (e.g. relations between function types). *} 1.15 + 1.16 +lemma Domainp_forall_transfer [transfer_rule]: 1.17 + assumes "right_total A" 1.18 + shows "((A ===> op =) ===> op =) 1.19 + (transfer_bforall (Domainp A)) transfer_forall" 1.20 + using assms unfolding right_total_def 1.21 + unfolding transfer_forall_def transfer_bforall_def fun_rel_def Domainp_iff 1.22 + by metis 1.23 + 1.24 +text {* Preferred rule for transferring universal quantifiers over 1.25 + bi-total correspondence relations (later rules are tried first). *} 1.26 + 1.27 +lemma transfer_forall_parametric [transfer_rule]: 1.28 + "bi_total A \<Longrightarrow> ((A ===> op =) ===> op =) transfer_forall transfer_forall" 1.29 + unfolding transfer_forall_def by (rule All_parametric) 1.30 1.31 end