moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
authorhaftmann
Thu Aug 18 13:25:17 2011 +0200 (2011-08-18)
changeset 44277bcb696533579
parent 44276 fe769a0fcc96
child 44278 1220ecb81e8f
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
src/HOL/Fun.thy
src/HOL/HOL.thy
     1.1 --- a/src/HOL/Fun.thy	Thu Aug 18 13:10:24 2011 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Aug 18 13:25:17 2011 +0200
     1.3 @@ -10,15 +10,6 @@
     1.4  uses ("Tools/enriched_type.ML")
     1.5  begin
     1.6  
     1.7 -text{*As a simplification rule, it replaces all function equalities by
     1.8 -  first-order equalities.*}
     1.9 -lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
    1.10 -apply (rule iffI)
    1.11 -apply (simp (no_asm_simp))
    1.12 -apply (rule ext)
    1.13 -apply (simp (no_asm_simp))
    1.14 -done
    1.15 -
    1.16  lemma apply_inverse:
    1.17    "f x = u \<Longrightarrow> (\<And>x. P x \<Longrightarrow> g (f x) = x) \<Longrightarrow> P x \<Longrightarrow> x = g u"
    1.18    by auto
    1.19 @@ -26,26 +17,22 @@
    1.20  
    1.21  subsection {* The Identity Function @{text id} *}
    1.22  
    1.23 -definition
    1.24 -  id :: "'a \<Rightarrow> 'a"
    1.25 -where
    1.26 +definition id :: "'a \<Rightarrow> 'a" where
    1.27    "id = (\<lambda>x. x)"
    1.28  
    1.29  lemma id_apply [simp]: "id x = x"
    1.30    by (simp add: id_def)
    1.31  
    1.32  lemma image_id [simp]: "id ` Y = Y"
    1.33 -by (simp add: id_def)
    1.34 +  by (simp add: id_def)
    1.35  
    1.36  lemma vimage_id [simp]: "id -` A = A"
    1.37 -by (simp add: id_def)
    1.38 +  by (simp add: id_def)
    1.39  
    1.40  
    1.41  subsection {* The Composition Operator @{text "f \<circ> g"} *}
    1.42  
    1.43 -definition
    1.44 -  comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55)
    1.45 -where
    1.46 +definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
    1.47    "f o g = (\<lambda>x. f (g x))"
    1.48  
    1.49  notation (xsymbols)
    1.50 @@ -54,9 +41,6 @@
    1.51  notation (HTML output)
    1.52    comp  (infixl "\<circ>" 55)
    1.53  
    1.54 -text{*compatibility*}
    1.55 -lemmas o_def = comp_def
    1.56 -
    1.57  lemma o_apply [simp]: "(f o g) x = f (g x)"
    1.58  by (simp add: comp_def)
    1.59  
    1.60 @@ -71,7 +55,7 @@
    1.61  
    1.62  lemma o_eq_dest:
    1.63    "a o b = c o d \<Longrightarrow> a (b v) = c (d v)"
    1.64 -  by (simp only: o_def) (fact fun_cong)
    1.65 +  by (simp only: comp_def) (fact fun_cong)
    1.66  
    1.67  lemma o_eq_elim:
    1.68    "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
    1.69 @@ -89,9 +73,7 @@
    1.70  
    1.71  subsection {* The Forward Composition Operator @{text fcomp} *}
    1.72  
    1.73 -definition
    1.74 -  fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60)
    1.75 -where
    1.76 +definition fcomp :: "('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "\<circ>>" 60) where
    1.77    "f \<circ>> g = (\<lambda>x. g (f x))"
    1.78  
    1.79  lemma fcomp_apply [simp]:  "(f \<circ>> g) x = g (f x)"
    1.80 @@ -569,8 +551,7 @@
    1.81  
    1.82  subsection{*Function Updating*}
    1.83  
    1.84 -definition
    1.85 -  fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
    1.86 +definition fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" where
    1.87    "fun_upd f a b == % x. if x=a then b else f x"
    1.88  
    1.89  nonterminal updbinds and updbind
    1.90 @@ -634,9 +615,7 @@
    1.91  
    1.92  subsection {* @{text override_on} *}
    1.93  
    1.94 -definition
    1.95 -  override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
    1.96 -where
    1.97 +definition override_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b" where
    1.98    "override_on f g A = (\<lambda>a. if a \<in> A then g a else f a)"
    1.99  
   1.100  lemma override_on_emptyset[simp]: "override_on f g {} = f"
   1.101 @@ -651,9 +630,7 @@
   1.102  
   1.103  subsection {* @{text swap} *}
   1.104  
   1.105 -definition
   1.106 -  swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"
   1.107 -where
   1.108 +definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)" where
   1.109    "swap a b f = f (a := f b, b:= f a)"
   1.110  
   1.111  lemma swap_self [simp]: "swap a a f = f"
   1.112 @@ -716,7 +693,7 @@
   1.113  subsection {* Inversion of injective functions *}
   1.114  
   1.115  definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
   1.116 -"the_inv_into A f == %x. THE y. y : A & f y = x"
   1.117 +  "the_inv_into A f == %x. THE y. y : A & f y = x"
   1.118  
   1.119  lemma the_inv_into_f_f:
   1.120    "[| inj_on f A;  x : A |] ==> the_inv_into A f (f x) = x"
   1.121 @@ -775,6 +752,11 @@
   1.122    shows "the_inv f (f x) = x" using assms UNIV_I
   1.123    by (rule the_inv_into_f_f)
   1.124  
   1.125 +
   1.126 +text{*compatibility*}
   1.127 +lemmas o_def = comp_def
   1.128 +
   1.129 +
   1.130  subsection {* Cantor's Paradox *}
   1.131  
   1.132  lemma Cantors_paradox [no_atp]:
     2.1 --- a/src/HOL/HOL.thy	Thu Aug 18 13:10:24 2011 +0200
     2.2 +++ b/src/HOL/HOL.thy	Thu Aug 18 13:25:17 2011 +0200
     2.3 @@ -1394,6 +1394,11 @@
     2.4    "f (if c then x else y) = (if c then f x else f y)"
     2.5    by simp
     2.6  
     2.7 +text{*As a simplification rule, it replaces all function equalities by
     2.8 +  first-order equalities.*}
     2.9 +lemma fun_eq_iff: "f = g \<longleftrightarrow> (\<forall>x. f x = g x)"
    2.10 +  by auto
    2.11 +
    2.12  
    2.13  subsubsection {* Generic cases and induction *}
    2.14