src/HOL/Fun.thy
 changeset 44277 bcb696533579 parent 43991 f4a7697011c5 child 44744 bdf8eb8f126b
equal 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 `
`    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 `
`    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)"`