equal
deleted
inserted
replaced
433 lemma finfun_default_update_const: |
433 lemma finfun_default_update_const: |
434 "finfun_default (f(a $:= b)) = finfun_default f" |
434 "finfun_default (f(a $:= b)) = finfun_default f" |
435 by transfer (simp add: finfun_default_aux_update_const) |
435 by transfer (simp add: finfun_default_aux_update_const) |
436 |
436 |
437 lemma finfun_default_const_code [code]: |
437 lemma finfun_default_const_code [code]: |
438 "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)" |
438 "finfun_default ((K$ c) :: 'a :: card_UNIV \<Rightarrow>f 'b) = (if CARD('a) = 0 then c else undefined)" |
439 by(simp add: finfun_default_const) |
439 by(simp add: finfun_default_const) |
440 |
440 |
441 lemma finfun_default_update_code [code]: |
441 lemma finfun_default_update_code [code]: |
442 "finfun_default (finfun_update_code f a b) = finfun_default f" |
442 "finfun_default (finfun_update_code f a b) = finfun_default f" |
443 by(simp add: finfun_default_update_const) |
443 by(simp add: finfun_default_update_const) |