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 =)