src/HOL/Fun.thy
changeset 44277 bcb696533579
parent 43991 f4a7697011c5
child 44744 bdf8eb8f126b
equal deleted inserted replaced
44276:fe769a0fcc96 44277:bcb696533579
     8 theory Fun
     8 theory Fun
     9 imports Complete_Lattice
     9 imports Complete_Lattice
    10 uses ("Tools/enriched_type.ML")
    10 uses ("Tools/enriched_type.ML")
    11 begin
    11 begin
    12 
    12 
    13 text{*As a simplification rule, it replaces all function equalities by
       
    14   first-order equalities.*}
       
    15 lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
       
    16 apply (rule iffI)
       
    17 apply (simp (no_asm_simp))
       
    18 apply (rule ext)
       
    19 apply (simp (no_asm_simp))
       
    20 done
       
    21 
       
    22 lemma apply_inverse:
    13 lemma apply_inverse:
    23   "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
    14   "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
    24   by auto
    15   by auto
    25 
    16 
    26 
    17 
    27 subsection {* The Identity Function @{text id} *}
    18 subsection {* The Identity Function @{text id} *}
    28 
    19 
    29 definition
    20 definition id :: "'a \<Rightarrow> 'a" where
    30   id :: "'a \<Rightarrow> 'a"
       
    31 where
       
    32   "id = (\<lambda>x. x)"
    21   "id = (\<lambda>x. x)"
    33 
    22 
    34 lemma id_apply [simp]: "id x = x"
    23 lemma id_apply [simp]: "id x = x"
    35   by (simp add: id_def)
    24   by (simp add: id_def)
    36 
    25 
    37 lemma image_id [simp]: "id ` Y = Y"
    26 lemma image_id [simp]: "id ` Y = Y"
    38 by (simp add: id_def)
    27   by (simp add: id_def)
    39 
    28 
    40 lemma vimage_id [simp]: "id -` A = A"
    29 lemma vimage_id [simp]: "id -` A = A"
    41 by (simp add: id_def)
    30   by (simp add: id_def)
    42 
    31 
    43 
    32 
    44 subsection {* The Composition Operator @{text "f \<circ> g"} *}
    33 subsection {* The Composition Operator @{text "f \<circ> g"} *}
    45 
    34 
    46 definition
    35 definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
    47   comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55)
       
    48 where
       
    49   "f o g = (\<lambda>x. f (g x))"
    36   "f o g = (\<lambda>x. f (g x))"
    50 
    37 
    51 notation (xsymbols)
    38 notation (xsymbols)
    52   comp  (infixl "\<circ>" 55)
    39   comp  (infixl "\<circ>" 55)
    53 
    40 
    54 notation (HTML output)
    41 notation (HTML output)
    55   comp  (infixl "\<circ>" 55)
    42   comp  (infixl "\<circ>" 55)
    56 
    43 
    57 text{*compatibility*}
       
    58 lemmas o_def = comp_def
       
    59 
       
    60 lemma o_apply [simp]: "(f o g) x = f (g x)"
    44 lemma o_apply [simp]: "(f o g) x = f (g x)"
    61 by (simp add: comp_def)
    45 by (simp add: comp_def)
    62 
    46 
    63 lemma o_assoc: "f o (g o h) = f o g o h"
    47 lemma o_assoc: "f o (g o h) = f o g o h"
    64 by (simp add: comp_def)
    48 by (simp add: comp_def)
    69 lemma o_id [simp]: "f o id = f"
    53 lemma o_id [simp]: "f o id = f"
    70 by (simp add: comp_def)
    54 by (simp add: comp_def)
    71 
    55 
    72 lemma o_eq_dest:
    56 lemma o_eq_dest:
    73   "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
    57   "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
    74   by (simp only: o_def) (fact fun_cong)
    58   by (simp only: comp_def) (fact fun_cong)
    75 
    59 
    76 lemma o_eq_elim:
    60 lemma o_eq_elim:
    77   "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    61   "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    78   by (erule meta_mp) (fact o_eq_dest) 
    62   by (erule meta_mp) (fact o_eq_dest) 
    79 
    63 
    87 by (unfold comp_def, blast)
    71 by (unfold comp_def, blast)
    88 
    72 
    89 
    73 
    90 subsection {* The Forward Composition Operator @{text fcomp} *}
    74 subsection {* The Forward Composition Operator @{text fcomp} *}
    91 
    75 
    92 definition
    76 definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60) where
    93   fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
       
    94 where
       
    95   "f \<circ>> g = (\<lambda>x. g (f x))"
    77   "f \<circ>> g = (\<lambda>x. g (f x))"
    96 
    78 
    97 lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
    79 lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
    98   by (simp add: fcomp_def)
    80   by (simp add: fcomp_def)
    99 
    81 
   567   by (auto intro!: inj_onI dest: strict_mono_eq)
   549   by (auto intro!: inj_onI dest: strict_mono_eq)
   568 
   550 
   569 
   551 
   570 subsection{*Function Updating*}
   552 subsection{*Function Updating*}
   571 
   553 
   572 definition
   554 definition fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
   573   fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
       
   574   "fun_upd f a b == % x. if x=a then b else f x"
   555   "fun_upd f a b == % x. if x=a then b else f x"
   575 
   556 
   576 nonterminal updbinds and updbind
   557 nonterminal updbinds and updbind
   577 
   558 
   578 syntax
   559 syntax
   632 by (auto intro: ext)
   613 by (auto intro: ext)
   633 
   614 
   634 
   615 
   635 subsection {* @{text override_on} *}
   616 subsection {* @{text override_on} *}
   636 
   617 
   637 definition
   618 definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" where
   638   override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
       
   639 where
       
   640   "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
   619   "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
   641 
   620 
   642 lemma override_on_emptyset[simp]: "override_on f g {} = f"
   621 lemma override_on_emptyset[simp]: "override_on f g {} = f"
   643 by(simp add:override_on_def)
   622 by(simp add:override_on_def)
   644 
   623 
   649 by(simp add:override_on_def)
   628 by(simp add:override_on_def)
   650 
   629 
   651 
   630 
   652 subsection {* @{text swap} *}
   631 subsection {* @{text swap} *}
   653 
   632 
   654 definition
   633 definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where
   655   swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
       
   656 where
       
   657   "swap a b f = f (a := f b, b:= f a)"
   634   "swap a b f = f (a := f b, b:= f a)"
   658 
   635 
   659 lemma swap_self [simp]: "swap a a f = f"
   636 lemma swap_self [simp]: "swap a a f = f"
   660 by (simp add: swap_def)
   637 by (simp add: swap_def)
   661 
   638 
   714 hide_const (open) swap
   691 hide_const (open) swap
   715 
   692 
   716 subsection {* Inversion of injective functions *}
   693 subsection {* Inversion of injective functions *}
   717 
   694 
   718 definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
   695 definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
   719 "the_inv_into A f == %x. THE y. y : A & f y = x"
   696   "the_inv_into A f == %x. THE y. y : A & f y = x"
   720 
   697 
   721 lemma the_inv_into_f_f:
   698 lemma the_inv_into_f_f:
   722   "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
   699   "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
   723 apply (simp add: the_inv_into_def inj_on_def)
   700 apply (simp add: the_inv_into_def inj_on_def)
   724 apply blast
   701 apply blast
   772 
   749 
   773 lemma the_inv_f_f:
   750 lemma the_inv_f_f:
   774   assumes "inj f"
   751   assumes "inj f"
   775   shows "the_inv f (f x) = x" using assms UNIV_I
   752   shows "the_inv f (f x) = x" using assms UNIV_I
   776   by (rule the_inv_into_f_f)
   753   by (rule the_inv_into_f_f)
       
   754 
       
   755 
       
   756 text{*compatibility*}
       
   757 lemmas o_def = comp_def
       
   758 
   777 
   759 
   778 subsection {* Cantor's Paradox *}
   760 subsection {* Cantor's Paradox *}
   779 
   761 
   780 lemma Cantors_paradox [no_atp]:
   762 lemma Cantors_paradox [no_atp]:
   781   "\<not>(\<exists>f. f ` A = Pow A)"
   763   "\<not>(\<exists>f. f ` A = Pow A)"