# HG changeset patch
# User huffman
# Date 1337075434 -7200
# Node ID 4e951258204b599a3178b20d1dcb48a830abe29d
# Parent  ba9df9685e7c2d59ebd40836fc41e89748c6ddc2
add transfer rules for nat_rec and funpow

diff -r ba9df9685e7c -r 4e951258204b src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Mon May 14 17:28:07 2012 +0200
+++ b/src/HOL/Transfer.thy	Tue May 15 11:50:34 2012 +0200
@@ -279,6 +279,14 @@
   "(A ===> (op = ===> A) ===> op = ===> A) nat_case nat_case"
   unfolding fun_rel_def by (simp split: nat.split)
 
+lemma nat_rec_transfer [transfer_rule]:
+  "(A ===> (op = ===> A ===> A) ===> op = ===> A) nat_rec nat_rec"
+  unfolding fun_rel_def by (clarsimp, rename_tac n, induct_tac n, simp_all)
+
+lemma funpow_transfer [transfer_rule]:
+  "(op = ===> (A ===> A) ===> (A ===> A)) compow compow"
+  unfolding funpow_def by transfer_prover
+
 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). *}