src/ZF/func.thy

 (*  Title:      ZF/func.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 *)
 
-section{*Functions, Function Spaces, Lambda-Abstraction*}
+section\<open>Functions, Function Spaces, Lambda-Abstraction\<close>
 
 theory func imports equalities Sum begin
 
-subsection{*The Pi Operator: Dependent Function Space*}
+subsection\<open>The Pi Operator: Dependent Function Space\<close>
 
 lemma subset_Sigma_imp_relation: "r \<subseteq> Sigma(A,B) ==> relation(r)"
 by (simp add: relation_def, blast)
 
 lemma relation_converse_converse [simp]:

 
 (*Weakening one function type to another; see also Pi_type*)
 lemma fun_weaken_type: "[| f \<in> A->B;  B<=D |] ==> f \<in> A->D"
 by (unfold Pi_def, best)
 
-subsection{*Function Application*}
+subsection\<open>Function Application\<close>
 
 lemma apply_equality2: "[| <a,b>: f;  <a,c>: f;  f \<in> Pi(A,B) |] ==> b=c"
 by (unfold Pi_def function_def, blast)
 
 lemma function_apply_equality: "[| <a,b>: f;  function(f) |] ==> f`a = b"

 by (blast dest: fun_is_rel)
 
 lemma Pair_mem_PiD: "[| <a,b>: f;  f \<in> Pi(A,B) |] ==> a \<in> A & b \<in> B(a) & f`a = b"
 by (blast intro: domain_type range_type apply_equality)
 
-subsection{*Lambda Abstraction*}
+subsection\<open>Lambda Abstraction\<close>
 
 lemma lamI: "a \<in> A ==> <a,b(a)> \<in> (\<lambda>x\<in>A. b(x))"
 apply (unfold lam_def)
 apply (erule RepFunI)
 done

 apply auto
 apply (fast intro!: equals0I intro: lam_type)
 done
 
 
-subsection{*Extensionality*}
+subsection\<open>Extensionality\<close>
 
 (*Semi-extensionality!*)
 
 lemma fun_subset:
     "[| f \<in> Pi(A,B);  g \<in> Pi(C,D);  A<=C;

 apply (rule_tac [2] eta [symmetric])
 apply (blast intro: major apply_type)+
 done
 
 
-subsection{*Images of Functions*}
+subsection\<open>Images of Functions\<close>
 
 lemma image_lam: "C \<subseteq> A ==> (\<lambda>x\<in>A. b(x)) `` C = {b(x). x \<in> C}"
 by (unfold lam_def, blast)
 
 lemma Repfun_function_if:

 lemma Pi_image_cons:
      "[| f \<in> Pi(A,B);  x \<in> A |] ==> f `` cons(x,y) = cons(f`x, f``y)"
 by (blast dest: apply_equality apply_Pair)
 
 
-subsection{*Properties of @{term "restrict(f,A)"}*}
+subsection\<open>Properties of @{term "restrict(f,A)"}\<close>
 
 lemma restrict_subset: "restrict(f,A) \<subseteq> f"
 by (unfold restrict_def, blast)
 
 lemma function_restrictI:

  prefer 2 apply (blast intro: apply_Pair restrict_subset [THEN subsetD])
 apply (auto dest!: Pi_memberD simp add: restrict_def lam_def)
 done
 
 
-subsection{*Unions of Functions*}
+subsection\<open>Unions of Functions\<close>
 
 (** The Union of a set of COMPATIBLE functions is a function **)
 
 lemma function_Union:
     "[| \<forall>x\<in>S. function(x);

 by (simp add: apply_def, blast)
 
 lemma fun_disjoint_apply2: "c \<notin> domain(f) ==> (f \<union> g)`c = g`c"
 by (simp add: apply_def, blast)
 
-subsection{*Domain and Range of a Function or Relation*}
+subsection\<open>Domain and Range of a Function or Relation\<close>
 
 lemma domain_of_fun: "f \<in> Pi(A,B) ==> domain(f)=A"
 by (unfold Pi_def, blast)
 
 lemma apply_rangeI: "[| f \<in> Pi(A,B);  a \<in> A |] ==> f`a \<in> range(f)"
 by (erule apply_Pair [THEN rangeI], assumption)
 
 lemma range_of_fun: "f \<in> Pi(A,B) ==> f \<in> A->range(f)"
 by (blast intro: Pi_type apply_rangeI)
 
-subsection{*Extensions of Functions*}
+subsection\<open>Extensions of Functions\<close>
 
 lemma fun_extend:
      "[| f \<in> A->B;  c\<notin>A |] ==> cons(<c,b>,f) \<in> cons(c,A) -> cons(b,B)"
 apply (frule singleton_fun [THEN fun_disjoint_Un], blast)
 apply (simp add: cons_eq)

 
 lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
 by (simp add: succ_def mem_not_refl cons_fun_eq)
 
 
-subsection{*Function Updates*}
+subsection\<open>Function Updates\<close>
 
 definition
   update  :: "[i,i,i] => i"  where
    "update(f,a,b) == \<lambda>x\<in>cons(a, domain(f)). if(x=a, b, f`x)"
 

 apply (unfold update_def)
 apply (simp add: domain_of_fun cons_absorb apply_funtype lam_type)
 done
 
 
-subsection{*Monotonicity Theorems*}
-
-subsubsection{*Replacement in its Various Forms*}
+subsection\<open>Monotonicity Theorems\<close>
+
+subsubsection\<open>Replacement in its Various Forms\<close>
 
 (*Not easy to express monotonicity in P, since any "bigger" predicate
   would have to be single-valued*)
 lemma Replace_mono: "A<=B ==> Replace(A,P) \<subseteq> Replace(B,P)"
 by (blast elim!: ReplaceE)

 by blast
 
 lemma Diff_mono: "[| A<=C;  D<=B |] ==> A-B \<subseteq> C-D"
 by blast
 
-subsubsection{*Standard Products, Sums and Function Spaces *}
+subsubsection\<open>Standard Products, Sums and Function Spaces\<close>
 
 lemma Sigma_mono [rule_format]:
      "[| A<=C;  !!x. x \<in> A \<longrightarrow> B(x) \<subseteq> D(x) |] ==> Sigma(A,B) \<subseteq> Sigma(C,D)"
 by blast
 

 lemma lam_mono: "A<=B ==> Lambda(A,c) \<subseteq> Lambda(B,c)"
 apply (unfold lam_def)
 apply (erule RepFun_mono)
 done
 
-subsubsection{*Converse, Domain, Range, Field*}
+subsubsection\<open>Converse, Domain, Range, Field\<close>
 
 lemma converse_mono: "r<=s ==> converse(r) \<subseteq> converse(s)"
 by blast
 
 lemma domain_mono: "r<=s ==> domain(r)<=domain(s)"

 
 lemma field_rel_subset: "r \<subseteq> A*A ==> field(r) \<subseteq> A"
 by (erule field_mono [THEN subset_trans], blast)
 
 
-subsubsection{*Images*}
+subsubsection\<open>Images\<close>
 
 lemma image_pair_mono:
     "[| !! x y. <x,y>:r ==> <x,y>:s;  A<=B |] ==> r``A \<subseteq> s``B"
 by blast