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