tuned proofs
authorAndreas Lochbihler
Tue May 29 17:17:57 2012 +0200 (2012-05-29)
changeset 48031bbf95f3595ab
parent 48030 ac43c8a7dcb5
child 48032 ba9e0f5b686d
tuned proofs
src/HOL/Library/FinFun.thy
     1.1 --- a/src/HOL/Library/FinFun.thy	Tue May 29 16:41:00 2012 +0200
     1.2 +++ b/src/HOL/Library/FinFun.thy	Tue May 29 17:17:57 2012 +0200
     1.3 @@ -417,15 +417,15 @@
     1.4  lift_definition finfun_default :: "'a \<Rightarrow>\<^isub>f 'b \<Rightarrow> 'b"
     1.5  is "finfun_default_aux" ..
     1.6  
     1.7 +lemma finfun_apply_transfer [transfer_rule]: 
     1.8 +  "(fun_rel cr_finfun (fun_rel op = op =)) (\<lambda>f. f) finfun_apply"
     1.9 +unfolding Rel_def fun_rel_def cr_finfun_def by simp
    1.10 +
    1.11  lemma finite_finfun_default: "finite {a. finfun_apply f a \<noteq> finfun_default f}"
    1.12 -apply transfer apply (erule finite_finfun_default_aux)
    1.13 -unfolding Rel_def fun_rel_def cr_finfun_def by simp
    1.14 +by transfer (erule finite_finfun_default_aux)
    1.15  
    1.16  lemma finfun_default_const: "finfun_default ((\<lambda>\<^isup>f b) :: 'a \<Rightarrow>\<^isub>f 'b) = (if finite (UNIV :: 'a set) then undefined else b)"
    1.17 -apply(transfer)
    1.18 -apply(auto simp add: finfun_default_aux_infinite)
    1.19 -apply(simp add: finfun_default_aux_def)
    1.20 -done
    1.21 +by(transfer)(auto simp add: finfun_default_aux_infinite finfun_default_aux_def)
    1.22  
    1.23  lemma finfun_default_update_const:
    1.24    "finfun_default (f(\<^sup>f a := b)) = finfun_default f"