# HG changeset patch
# User huffman
# Date 1334952307 -7200
# Node ID 7a34395441ff63abe74afa8421c48d615033f156
# Parent  b786388b4b3ad7927daf13f6646b7fd859bf01e5
add transfer rule for nat_case

diff -r b786388b4b3a -r 7a34395441ff src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Fri Apr 20 22:54:13 2012 +0200
+++ b/src/HOL/Transfer.thy	Fri Apr 20 22:05:07 2012 +0200
@@ -252,13 +252,17 @@
   shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd"
   unfolding fun_upd_def [abs_def] by transfer_prover
 
-lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
-  by auto
+lemma nat_case_transfer [transfer_rule]:
+  "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case"
+  unfolding fun_rel_def by (simp split: nat.split)
 
 text {* Fallback rule for transferring universal quantifiers over
   correspondence relations that are not bi-total, and do not have
   custom transfer rules (e.g. relations between function types). *}
 
+lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
+  by auto
+
 lemma Domainp_forall_transfer [transfer_rule]:
   assumes "right_total A"
   shows "((A ===> op =) ===> op =)