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.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.31  end