add transfer rule for 'id'
authorhuffman
Fri, 20 Apr 2012 15:30:13 +0200
changeset 47625 10cfaf771687
parent 47624 16d433895d2e
child 47626 f7b1034cb9ce
add transfer rule for 'id'
src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Fri Apr 20 14:57:19 2012 +0200
+++ b/src/HOL/Transfer.thy	Fri Apr 20 15:30:13 2012 +0200
@@ -240,6 +240,9 @@
 lemma Let_parametric [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
   unfolding fun_rel_def by simp
 
+lemma id_parametric [transfer_rule]: "(A ===> A) id id"
+  unfolding fun_rel_def by simp
+
 lemma comp_parametric [transfer_rule]:
   "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
   unfolding fun_rel_def by simp