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