Converted Fun to Isar style.
authorpaulson
Thu Sep 26 10:51:29 2002 +0200 (2002-09-26)
changeset 13585db4005b40cc6
parent 13584 3736cf381e15
child 13586 0f339348df0e
Converted Fun to Isar style.
Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy.
Renamed constant "Fun.op o" to "Fun.comp"
src/HOL/Bali/AxSem.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Table.thy
src/HOL/Fun.ML
src/HOL/Fun.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Hilbert_Choice_lemmas.ML
src/HOL/Induct/LList.thy
src/HOL/IsaMakefile
src/HOL/List.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/Nat.thy
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/ex/Tarski.thy
     1.1 --- a/src/HOL/Bali/AxSem.thy	Thu Sep 26 10:43:43 2002 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Thu Sep 26 10:51:29 2002 +0200
     1.3 @@ -413,7 +413,7 @@
     1.4    "{P} .c. {Q}" == "{P} In1r c\<succ> {Q}"
     1.5  
     1.6  lemma inj_triple: "inj (\<lambda>(P,t,Q). {P} t\<succ> {Q})"
     1.7 -apply (rule injI)
     1.8 +apply (rule inj_onI)
     1.9  apply auto
    1.10  done
    1.11  
     2.1 --- a/src/HOL/Bali/DeclConcepts.thy	Thu Sep 26 10:43:43 2002 +0200
     2.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Thu Sep 26 10:51:29 2002 +0200
     2.3 @@ -2369,9 +2369,8 @@
     2.4        unique (fields G C)" 
     2.5  apply (rule ws_subcls1_induct, assumption, assumption)
     2.6  apply (subst fields_rec, assumption)            
     2.7 -apply (auto intro!: unique_map_inj injI 
     2.8 -            elim!: unique_append ws_unique_fields_lemma fields_norec
     2.9 -            )
    2.10 +apply (auto intro!: unique_map_inj inj_onI 
    2.11 +            elim!: unique_append ws_unique_fields_lemma fields_norec)
    2.12  done
    2.13  
    2.14  
     3.1 --- a/src/HOL/Bali/Table.thy	Thu Sep 26 10:43:43 2002 +0200
     3.2 +++ b/src/HOL/Bali/Table.thy	Thu Sep 26 10:51:29 2002 +0200
     3.3 @@ -213,7 +213,7 @@
     3.4  done
     3.5  
     3.6  lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
     3.7 -apply (rule injI)
     3.8 +apply (rule inj_onI)
     3.9  apply auto
    3.10  done
    3.11  
     4.1 --- a/src/HOL/Fun.ML	Thu Sep 26 10:43:43 2002 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,507 +0,0 @@
     4.4 -(*  Title:      HOL/Fun
     4.5 -    ID:         $Id$
     4.6 -    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     4.7 -    Copyright   1993  University of Cambridge
     4.8 -
     4.9 -Lemmas about functions.
    4.10 -*)
    4.11 -
    4.12 -Goal "(f = g) = (! x. f(x)=g(x))";
    4.13 -by (rtac iffI 1);
    4.14 -by (Asm_simp_tac 1);
    4.15 -by (rtac ext 1 THEN Asm_simp_tac 1);
    4.16 -qed "expand_fun_eq";
    4.17 -
    4.18 -val prems = Goal
    4.19 -    "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)";
    4.20 -by (rtac (arg_cong RS box_equals) 1);
    4.21 -by (REPEAT (resolve_tac (prems@[refl]) 1));
    4.22 -qed "apply_inverse";
    4.23 -
    4.24 -
    4.25 -section "id";
    4.26 -
    4.27 -Goalw [id_def] "id x = x";
    4.28 -by (rtac refl 1);
    4.29 -qed "id_apply";
    4.30 -Addsimps [id_apply];
    4.31 -
    4.32 -
    4.33 -section "o";
    4.34 -
    4.35 -Goalw [o_def] "(f o g) x = f (g x)";
    4.36 -by (rtac refl 1);
    4.37 -qed "o_apply";
    4.38 -Addsimps [o_apply];
    4.39 -
    4.40 -Goalw [o_def] "f o (g o h) = f o g o h";
    4.41 -by (rtac ext 1);
    4.42 -by (rtac refl 1);
    4.43 -qed "o_assoc";
    4.44 -
    4.45 -Goalw [id_def] "id o g = g";
    4.46 -by (rtac ext 1);
    4.47 -by (Simp_tac 1);
    4.48 -qed "id_o";
    4.49 -Addsimps [id_o];
    4.50 -
    4.51 -Goalw [id_def] "f o id = f";
    4.52 -by (rtac ext 1);
    4.53 -by (Simp_tac 1);
    4.54 -qed "o_id";
    4.55 -Addsimps [o_id];
    4.56 -
    4.57 -Goalw [o_def] "(f o g)`r = f`(g`r)";
    4.58 -by (Blast_tac 1);
    4.59 -qed "image_compose";
    4.60 -
    4.61 -Goal "f`A = (UN x:A. {f x})";
    4.62 -by (Blast_tac 1);
    4.63 -qed "image_eq_UN";
    4.64 -
    4.65 -Goalw [o_def] "UNION A (g o f) = UNION (f`A) g";
    4.66 -by (Blast_tac 1);
    4.67 -qed "UN_o";
    4.68 -
    4.69 -(** lemma for proving injectivity of representation functions for **)
    4.70 -(** datatypes involving function types                            **)
    4.71 -
    4.72 -Goalw [o_def]
    4.73 -  "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa";
    4.74 -by (rtac ext 1);
    4.75 -by (etac allE 1);
    4.76 -by (etac allE 1);
    4.77 -by (etac mp 1);
    4.78 -by (etac fun_cong 1);
    4.79 -qed "inj_fun_lemma";
    4.80 -
    4.81 -
    4.82 -section "inj";
    4.83 -(**NB: inj now just translates to inj_on**)
    4.84 -
    4.85 -(*** inj(f): f is a one-to-one function ***)
    4.86 -
    4.87 -(*for Tools/datatype_rep_proofs*)
    4.88 -val [prem] = Goalw [inj_on_def]
    4.89 -    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)";
    4.90 -by (blast_tac (claset() addIs [prem RS spec RS mp]) 1);
    4.91 -qed "datatype_injI";
    4.92 -
    4.93 -Goalw [inj_on_def] "[| inj(f); f(x) = f(y) |] ==> x=y";
    4.94 -by (Blast_tac 1);
    4.95 -qed "injD";
    4.96 -
    4.97 -(*Useful with the simplifier*)
    4.98 -Goal "inj(f) ==> (f(x) = f(y)) = (x=y)";
    4.99 -by (rtac iffI 1);
   4.100 -by (etac arg_cong 2);
   4.101 -by (etac injD 1);
   4.102 -by (assume_tac 1);
   4.103 -qed "inj_eq";
   4.104 -
   4.105 -Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
   4.106 -by (rtac ext 1);
   4.107 -by (etac injD 1);
   4.108 -by (etac fun_cong 1);
   4.109 -qed "inj_o";
   4.110 -
   4.111 -(*** inj_on f A: f is one-to-one over A ***)
   4.112 -
   4.113 -val prems = Goalw [inj_on_def]
   4.114 -    "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A";
   4.115 -by (blast_tac (claset() addIs prems) 1);
   4.116 -qed "inj_onI";
   4.117 -bind_thm ("injI", inj_onI);                  (*for compatibility*)
   4.118 -
   4.119 -val [major] = Goal 
   4.120 -    "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
   4.121 -by (rtac inj_onI 1);
   4.122 -by (etac (apply_inverse RS trans) 1);
   4.123 -by (REPEAT (eresolve_tac [asm_rl,major] 1));
   4.124 -qed "inj_on_inverseI";
   4.125 -bind_thm ("inj_inverseI", inj_on_inverseI);   (*for compatibility*)
   4.126 -
   4.127 -Goalw [inj_on_def] "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
   4.128 -by (Blast_tac 1);
   4.129 -qed "inj_onD";
   4.130 -
   4.131 -Goal "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
   4.132 -by (blast_tac (claset() addSDs [inj_onD]) 1);
   4.133 -qed "inj_on_iff";
   4.134 -
   4.135 -Goalw [o_def, inj_on_def]
   4.136 -     "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A";
   4.137 -by (Blast_tac 1);
   4.138 -qed "comp_inj_on";
   4.139 -
   4.140 -Goalw [inj_on_def] "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
   4.141 -by (Blast_tac 1);
   4.142 -qed "inj_on_contraD";
   4.143 -
   4.144 -Goal "inj (%s. {s})";
   4.145 -by (rtac injI 1);
   4.146 -by (etac singleton_inject 1);
   4.147 -qed "inj_singleton";
   4.148 -
   4.149 -Goalw [inj_on_def] "[| A<=B; inj_on f B |] ==> inj_on f A";
   4.150 -by (Blast_tac 1);
   4.151 -qed "subset_inj_on";
   4.152 -
   4.153 -
   4.154 -(** surj **)
   4.155 -
   4.156 -val [prem] = Goalw [surj_def] "(!! x. g(f x) = x) ==> surj g";
   4.157 -by (blast_tac (claset() addIs [prem RS sym]) 1);
   4.158 -qed "surjI";
   4.159 -
   4.160 -Goalw [surj_def] "surj f ==> range f = UNIV";
   4.161 -by Auto_tac;
   4.162 -qed "surj_range";
   4.163 -
   4.164 -Goalw [surj_def] "surj f ==> EX x. y = f x";
   4.165 -by (Blast_tac 1);
   4.166 -qed "surjD";
   4.167 -
   4.168 -val [p1, p2] = Goal "surj f ==> (!!x. y = f x ==> C) ==> C";
   4.169 -by (cut_facts_tac [p1 RS surjD] 1);
   4.170 -by (etac exE 1);
   4.171 -by (rtac p2 1);
   4.172 -by (atac 1);
   4.173 -qed "surjE";
   4.174 -
   4.175 -Goalw [o_def, surj_def] "[| surj f;  surj g |] ==> surj (g o f)";
   4.176 -by (Clarify_tac 1); 
   4.177 -by (dres_inst_tac [("x","y")] spec 1); 
   4.178 -by (Clarify_tac 1); 
   4.179 -by (dres_inst_tac [("x","x")] spec 1); 
   4.180 -by (Blast_tac 1); 
   4.181 -qed "comp_surj";
   4.182 -
   4.183 -
   4.184 -(** Bijections **)
   4.185 -
   4.186 -Goalw [bij_def] "[| inj f; surj f |] ==> bij f";
   4.187 -by (Blast_tac 1);
   4.188 -qed "bijI";
   4.189 -
   4.190 -Goalw [bij_def] "bij f ==> inj f";
   4.191 -by (Blast_tac 1);
   4.192 -qed "bij_is_inj";
   4.193 -
   4.194 -Goalw [bij_def] "bij f ==> surj f";
   4.195 -by (Blast_tac 1);
   4.196 -qed "bij_is_surj";
   4.197 -
   4.198 -
   4.199 -(** We seem to need both the id-forms and the (%x. x) forms; the latter can
   4.200 -    arise by rewriting, while id may be used explicitly. **)
   4.201 -
   4.202 -Goal "(%x. x) ` Y = Y";
   4.203 -by (Blast_tac 1);
   4.204 -qed "image_ident";
   4.205 -
   4.206 -Goalw [id_def] "id ` Y = Y";
   4.207 -by (Blast_tac 1);
   4.208 -qed "image_id";
   4.209 -Addsimps [image_ident, image_id];
   4.210 -
   4.211 -Goal "(%x. x) -` Y = Y";
   4.212 -by (Blast_tac 1);
   4.213 -qed "vimage_ident";
   4.214 -
   4.215 -Goalw [id_def] "id -` A = A";
   4.216 -by Auto_tac;
   4.217 -qed "vimage_id";
   4.218 -Addsimps [vimage_ident, vimage_id];
   4.219 -
   4.220 -Goal "f -` (f ` A) = {y. EX x:A. f x = f y}";
   4.221 -by (blast_tac (claset() addIs [sym]) 1);
   4.222 -qed "vimage_image_eq";
   4.223 -
   4.224 -Goal "f ` (f -` A) <= A";
   4.225 -by (Blast_tac 1);
   4.226 -qed "image_vimage_subset";
   4.227 -
   4.228 -Goal "f ` (f -` A) = A Int range f";
   4.229 -by (Blast_tac 1);
   4.230 -qed "image_vimage_eq";
   4.231 -Addsimps [image_vimage_eq];
   4.232 -
   4.233 -Goal "surj f ==> f ` (f -` A) = A";
   4.234 -by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
   4.235 -qed "surj_image_vimage_eq";
   4.236 -
   4.237 -Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A";
   4.238 -by (Blast_tac 1);
   4.239 -qed "inj_vimage_image_eq";
   4.240 -
   4.241 -Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A";
   4.242 -by (blast_tac (claset() addIs [sym]) 1);
   4.243 -qed "vimage_subsetD";
   4.244 -
   4.245 -Goalw [inj_on_def] "inj f ==> B <= f ` A ==> f -` B <= A";
   4.246 -by (Blast_tac 1);
   4.247 -qed "vimage_subsetI";
   4.248 -
   4.249 -Goalw [bij_def] "bij f ==> (f -` B <= A) = (B <= f ` A)";
   4.250 -by (blast_tac (claset() delrules [subsetI]
   4.251 -			addIs [vimage_subsetI, vimage_subsetD]) 1);
   4.252 -qed "vimage_subset_eq";
   4.253 -
   4.254 -Goal "f`(A Int B) <= f`A Int f`B";
   4.255 -by (Blast_tac 1);
   4.256 -qed "image_Int_subset";
   4.257 -
   4.258 -Goal "f`A - f`B <= f`(A - B)";
   4.259 -by (Blast_tac 1);
   4.260 -qed "image_diff_subset";
   4.261 -
   4.262 -Goalw [inj_on_def]
   4.263 -   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B";
   4.264 -by (Blast_tac 1);
   4.265 -qed "inj_on_image_Int";
   4.266 -
   4.267 -Goalw [inj_on_def]
   4.268 -   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A-B) = f`A - f`B";
   4.269 -by (Blast_tac 1);
   4.270 -qed "inj_on_image_set_diff";
   4.271 -
   4.272 -Goalw [inj_on_def] "inj f ==> f`(A Int B) = f`A Int f`B";
   4.273 -by (Blast_tac 1);
   4.274 -qed "image_Int";
   4.275 -
   4.276 -Goalw [inj_on_def] "inj f ==> f`(A-B) = f`A - f`B";
   4.277 -by (Blast_tac 1);
   4.278 -qed "image_set_diff";
   4.279 -
   4.280 -Goal "inj f ==> (f a : f`A) = (a : A)";
   4.281 -by (blast_tac (claset() addDs [injD]) 1);
   4.282 -qed "inj_image_mem_iff";
   4.283 -
   4.284 -Goalw [inj_on_def] "inj f ==> (f`A <= f`B) = (A<=B)";
   4.285 -by (Blast_tac 1);
   4.286 -qed "inj_image_subset_iff";
   4.287 -
   4.288 -Goal "inj f ==> (f`A = f`B) = (A = B)";
   4.289 -by (blast_tac (claset() addDs [injD]) 1);
   4.290 -qed "inj_image_eq_iff";
   4.291 -
   4.292 -Goal  "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))";
   4.293 -by (Blast_tac 1);
   4.294 -qed "image_UN";
   4.295 -
   4.296 -(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
   4.297 -Goalw [inj_on_def]
   4.298 -   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |] \
   4.299 -\   ==> f ` (INTER A B) = (INT x:A. f ` B x)";
   4.300 -by (Blast_tac 1);
   4.301 -qed "image_INT";
   4.302 -
   4.303 -(*Compare with image_INT: no use of inj_on, and if f is surjective then
   4.304 -  it doesn't matter whether A is empty*)
   4.305 -Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)";
   4.306 -by (asm_full_simp_tac (simpset() addsimps [inj_on_def, surj_def]) 1);
   4.307 -by (Blast_tac 1);  
   4.308 -qed "bij_image_INT";
   4.309 -
   4.310 -Goal "surj f ==> -(f`A) <= f`(-A)";
   4.311 -by (auto_tac (claset(), simpset() addsimps [surj_def]));  
   4.312 -qed "surj_Compl_image_subset";
   4.313 -
   4.314 -Goal "inj f ==> f`(-A) <= -(f`A)";
   4.315 -by (auto_tac (claset(), simpset() addsimps [inj_on_def]));  
   4.316 -qed "inj_image_Compl_subset";
   4.317 -
   4.318 -Goalw [bij_def] "bij f ==> f`(-A) = -(f`A)";
   4.319 -by (rtac equalityI 1); 
   4.320 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [inj_image_Compl_subset, 
   4.321 -                                                surj_Compl_image_subset]))); 
   4.322 -qed "bij_image_Compl_eq";
   4.323 -
   4.324 -val set_cs = claset() delrules [equalityI];
   4.325 -
   4.326 -
   4.327 -section "fun_upd";
   4.328 -
   4.329 -Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
   4.330 -by Safe_tac;
   4.331 -by (etac subst 1);
   4.332 -by (rtac ext 2);
   4.333 -by Auto_tac;
   4.334 -qed "fun_upd_idem_iff";
   4.335 -
   4.336 -(* f x = y ==> f(x:=y) = f *)
   4.337 -bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
   4.338 -
   4.339 -(* f(x := f x) = f *)
   4.340 -AddIffs [refl RS fun_upd_idem];
   4.341 -
   4.342 -Goal "(f(x:=y))z = (if z=x then y else f z)";
   4.343 -by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
   4.344 -qed "fun_upd_apply";
   4.345 -Addsimps [fun_upd_apply];
   4.346 -
   4.347 -(* fun_upd_apply supersedes these two,   but they are useful 
   4.348 -   if fun_upd_apply is intentionally removed from the simpset *)
   4.349 -Goal "(f(x:=y)) x = y";
   4.350 -by (Simp_tac 1);
   4.351 -qed "fun_upd_same";
   4.352 -
   4.353 -Goal "z~=x ==> (f(x:=y)) z = f z";
   4.354 -by (Asm_simp_tac 1);
   4.355 -qed "fun_upd_other";
   4.356 -
   4.357 -Goal "f(x:=y,x:=z) = f(x:=z)";
   4.358 -by (rtac ext 1);
   4.359 -by (Simp_tac 1);
   4.360 -qed "fun_upd_upd";
   4.361 -Addsimps [fun_upd_upd];
   4.362 -
   4.363 -(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
   4.364 -local 
   4.365 -  fun gen_fun_upd None T _ _ = None
   4.366 -    | gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y);
   4.367 -  fun dest_fun_T1 (Type (_, T :: Ts)) = T;
   4.368 -  fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) =
   4.369 -    let
   4.370 -      fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) =
   4.371 -            if v aconv x then Some g else gen_fun_upd (find g) T v w
   4.372 -        | find t = None;
   4.373 -    in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end;
   4.374 -
   4.375 -  val ss = simpset ();
   4.376 -  val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1);
   4.377 -in 
   4.378 -  val fun_upd2_simproc =
   4.379 -    Simplifier.simproc (Theory.sign_of (the_context ()))
   4.380 -      "fun_upd2" ["f(v := w, x := y)"]
   4.381 -      (fn sg => fn _ => fn t =>
   4.382 -        case find_double t of (T, None) => None
   4.383 -        | (T, Some rhs) => Some (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover));
   4.384 -end;
   4.385 -Addsimprocs[fun_upd2_simproc];
   4.386 -
   4.387 -Goal "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)";
   4.388 -by (rtac ext 1);
   4.389 -by Auto_tac;
   4.390 -qed "fun_upd_twist";
   4.391 -
   4.392 -
   4.393 -(*** -> and Pi, by Florian Kammueller and LCP ***)
   4.394 -
   4.395 -val prems = Goalw [Pi_def]
   4.396 -"[| !!x. x: A ==> f x: B x; !!x. x ~: A  ==> f(x) = arbitrary|] \
   4.397 -\    ==> f: Pi A B";
   4.398 -by (auto_tac (claset(), simpset() addsimps prems));
   4.399 -qed "Pi_I";
   4.400 -
   4.401 -val prems = Goal 
   4.402 -"[| !!x. x: A ==> f x: B; !!x. x ~: A  ==> f(x) = arbitrary|] ==> f: A funcset B";
   4.403 -by (blast_tac (claset() addIs Pi_I::prems) 1);
   4.404 -qed "funcsetI";
   4.405 -
   4.406 -Goalw [Pi_def] "[|f: Pi A B; x: A|] ==> f x: B x";
   4.407 -by Auto_tac;
   4.408 -qed "Pi_mem";
   4.409 -
   4.410 -Goalw [Pi_def] "[|f: A funcset B; x: A|] ==> f x: B";
   4.411 -by Auto_tac;
   4.412 -qed "funcset_mem";
   4.413 -
   4.414 -Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = arbitrary";
   4.415 -by Auto_tac;
   4.416 -qed "apply_arb";
   4.417 -
   4.418 -Goalw [Pi_def] "[| f: Pi A B; g: Pi A B; ! x: A. f x = g x |] ==> f = g";
   4.419 -by (rtac ext 1);
   4.420 -by Auto_tac;
   4.421 -bind_thm ("Pi_extensionality", ballI RSN (3, result()));
   4.422 -
   4.423 -
   4.424 -(*** compose ***)
   4.425 -
   4.426 -Goalw [Pi_def, compose_def, restrict_def]
   4.427 -     "[| f: A funcset B; g: B funcset C |]==> compose A g f: A funcset C";
   4.428 -by Auto_tac;
   4.429 -qed "funcset_compose";
   4.430 -
   4.431 -Goal "[| f: A funcset B; g: B funcset C; h: C funcset D |]\
   4.432 -\     ==> compose A h (compose A g f) = compose A (compose B h g) f";
   4.433 -by (res_inst_tac [("A","A")] Pi_extensionality 1);
   4.434 -by (blast_tac (claset() addIs [funcset_compose]) 1);
   4.435 -by (blast_tac (claset() addIs [funcset_compose]) 1);
   4.436 -by (rewrite_goals_tac [Pi_def, compose_def, restrict_def]);  
   4.437 -by Auto_tac;
   4.438 -qed "compose_assoc";
   4.439 -
   4.440 -Goal "x : A ==> compose A g f x = g(f(x))";
   4.441 -by (asm_simp_tac (simpset() addsimps [compose_def, restrict_def]) 1);
   4.442 -qed "compose_eq";
   4.443 -
   4.444 -Goal "[| f ` A = B; g ` B = C |] ==> compose A g f ` A = C";
   4.445 -by (auto_tac (claset(), simpset() addsimps [image_def, compose_eq]));
   4.446 -qed "surj_compose";
   4.447 -
   4.448 -Goal "[| f ` A = B; inj_on f A; inj_on g B |] ==> inj_on (compose A g f) A";
   4.449 -by (auto_tac (claset(), simpset() addsimps [inj_on_def, compose_eq]));
   4.450 -qed "inj_on_compose";
   4.451 -
   4.452 -
   4.453 -(*** restrict / bounded abstraction ***)
   4.454 -
   4.455 -Goal "f`A <= B ==> (%x:A. f x) : A funcset B";
   4.456 -by (auto_tac (claset(),
   4.457 -	      simpset() addsimps [restrict_def, Pi_def]));
   4.458 -qed "restrict_in_funcset";
   4.459 -
   4.460 -val prems = Goalw [restrict_def, Pi_def]
   4.461 -     "(!!x. x: A ==> f x: B x) ==> (%x:A. f x) : Pi A B";
   4.462 -by (asm_simp_tac (simpset() addsimps prems) 1);
   4.463 -qed "restrictI";
   4.464 -
   4.465 -Goal "(%y:A. f y) x = (if x : A then f x else arbitrary)";
   4.466 -by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
   4.467 -qed "restrict_apply";
   4.468 -Addsimps [restrict_apply];
   4.469 -
   4.470 -val prems = Goal
   4.471 -    "(!!x. x: A ==> f x = g x) ==> (%x:A. f x) = (%x:A. g x)";
   4.472 -by (rtac ext 1);
   4.473 -by (auto_tac (claset(),
   4.474 -	      simpset() addsimps prems@[restrict_def, Pi_def]));
   4.475 -qed "restrict_ext";
   4.476 -
   4.477 -Goalw [inj_on_def, restrict_def] "inj_on (restrict f A) A = inj_on f A";
   4.478 -by Auto_tac;
   4.479 -qed "inj_on_restrict_eq";
   4.480 -
   4.481 -
   4.482 -Goal "f : A funcset B ==> compose A (%y:B. y) f = f";
   4.483 -by (rtac ext 1); 
   4.484 -by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 
   4.485 -qed "Id_compose";
   4.486 -
   4.487 -Goal "g : A funcset B ==> compose A g (%x:A. x) = g";
   4.488 -by (rtac ext 1); 
   4.489 -by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def])); 
   4.490 -qed "compose_Id";
   4.491 -
   4.492 -
   4.493 -(*** Pi ***)
   4.494 -
   4.495 -Goalw [Pi_def] "[| B(x) = {};  x: A |] ==> (PI x: A. B x) = {}";
   4.496 -by Auto_tac;
   4.497 -qed "Pi_eq_empty";
   4.498 -
   4.499 -Goal "[| (PI x: A. B x) ~= {};  x: A |] ==> B(x) ~= {}";
   4.500 -by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
   4.501 -qed "Pi_total1";
   4.502 -
   4.503 -Goal "Pi {} B = { %x. arbitrary }";
   4.504 -by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
   4.505 -qed "Pi_empty";
   4.506 -
   4.507 -val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
   4.508 -by (auto_tac (claset(),
   4.509 -	      simpset() addsimps [impOfSubs major]));
   4.510 -qed "Pi_mono";
     5.1 --- a/src/HOL/Fun.thy	Thu Sep 26 10:43:43 2002 +0200
     5.2 +++ b/src/HOL/Fun.thy	Thu Sep 26 10:51:29 2002 +0200
     5.3 @@ -6,94 +6,447 @@
     5.4  Notions about functions.
     5.5  *)
     5.6  
     5.7 -Fun = Typedef +
     5.8 +theory Fun = Typedef:
     5.9  
    5.10  instance set :: (type) order
    5.11 -                       (subset_refl,subset_trans,subset_antisym,psubset_eq)
    5.12 -consts
    5.13 -  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    5.14 +  by (intro_classes,
    5.15 +      (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
    5.16 +
    5.17 +constdefs
    5.18 +  fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    5.19 +   "fun_upd f a b == % x. if x=a then b else f x"
    5.20  
    5.21  nonterminals
    5.22    updbinds updbind
    5.23  syntax
    5.24 -  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
    5.25 -  ""               :: updbind => updbinds             ("_")
    5.26 -  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    5.27 -  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [1000,0] 900)
    5.28 +  "_updbind" :: "['a, 'a] => updbind"             ("(2_ :=/ _)")
    5.29 +  ""         :: "updbind => updbinds"             ("_")
    5.30 +  "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _")
    5.31 +  "_Update"  :: "['a, updbinds] => 'a"            ("_/'((_)')" [1000,0] 900)
    5.32  
    5.33  translations
    5.34    "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
    5.35    "f(x:=y)"                     == "fun_upd f x y"
    5.36  
    5.37 -defs
    5.38 -  fun_upd_def "f(a:=b) == % x. if x=a then b else f x"
    5.39 -
    5.40  (* Hint: to define the sum of two functions (or maps), use sum_case.
    5.41           A nice infix syntax could be defined (in Datatype.thy or below) by
    5.42  consts
    5.43    fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80)
    5.44  translations
    5.45 - "fun_sum" == "sum_case"
    5.46 + "fun_sum" == sum_case
    5.47  *)
    5.48  
    5.49  constdefs
    5.50 -  id ::  'a => 'a
    5.51 +  id :: "'a => 'a"
    5.52      "id == %x. x"
    5.53  
    5.54 -  o  :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
    5.55 +  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"   (infixl "o" 55)
    5.56      "f o g == %x. f(g(x))"
    5.57  
    5.58 -  inj_on :: ['a => 'b, 'a set] => bool
    5.59 -    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    5.60 +text{*compatibility*}
    5.61 +lemmas o_def = comp_def
    5.62  
    5.63  syntax (xsymbols)
    5.64 -  "op o"        :: "['b => 'c, 'a => 'b, 'a] => 'c"      (infixl "\\<circ>" 55)
    5.65 +  comp :: "['b => 'c, 'a => 'b, 'a] => 'c"        (infixl "\<circ>" 55)
    5.66 +
    5.67  
    5.68 -syntax
    5.69 -  inj   :: ('a => 'b) => bool                   (*injective*)
    5.70 +constdefs
    5.71 +  inj_on :: "['a => 'b, 'a set] => bool"         (*injective*)
    5.72 +    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    5.73  
    5.74 +text{*A common special case: functions injective over the entire domain type.*}
    5.75 +syntax inj   :: "('a => 'b) => bool"
    5.76  translations
    5.77    "inj f" == "inj_on f UNIV"
    5.78  
    5.79  constdefs
    5.80 -  surj :: ('a => 'b) => bool                   (*surjective*)
    5.81 +  surj :: "('a => 'b) => bool"                   (*surjective*)
    5.82      "surj f == ! y. ? x. y=f(x)"
    5.83  
    5.84 -  bij :: ('a => 'b) => bool                    (*bijective*)
    5.85 +  bij :: "('a => 'b) => bool"                    (*bijective*)
    5.86      "bij f == inj f & surj f"
    5.87  
    5.88  
    5.89 -(*The Pi-operator, by Florian Kammueller*)
    5.90 +
    5.91 +text{*As a simplification rule, it replaces all function equalities by
    5.92 +  first-order equalities.*}
    5.93 +lemma expand_fun_eq: "(f = g) = (! x. f(x)=g(x))"
    5.94 +apply (rule iffI)
    5.95 +apply (simp (no_asm_simp))
    5.96 +apply (rule ext, simp (no_asm_simp))
    5.97 +done
    5.98 +
    5.99 +lemma apply_inverse:
   5.100 +    "[| f(x)=u;  !!x. P(x) ==> g(f(x)) = x;  P(x) |] ==> x=g(u)"
   5.101 +by auto
   5.102 +
   5.103 +
   5.104 +text{*The Identity Function: @{term id}*}
   5.105 +lemma id_apply [simp]: "id x = x"
   5.106 +by (simp add: id_def)
   5.107 +
   5.108 +
   5.109 +subsection{*The Composition Operator: @{term "f \<circ> g"}*}
   5.110 +
   5.111 +lemma o_apply [simp]: "(f o g) x = f (g x)"
   5.112 +by (simp add: comp_def)
   5.113 +
   5.114 +lemma o_assoc: "f o (g o h) = f o g o h"
   5.115 +by (simp add: comp_def)
   5.116 +
   5.117 +lemma id_o [simp]: "id o g = g"
   5.118 +by (simp add: comp_def)
   5.119 +
   5.120 +lemma o_id [simp]: "f o id = f"
   5.121 +by (simp add: comp_def)
   5.122 +
   5.123 +lemma image_compose: "(f o g) ` r = f`(g`r)"
   5.124 +by (simp add: comp_def, blast)
   5.125 +
   5.126 +lemma image_eq_UN: "f`A = (UN x:A. {f x})"
   5.127 +by blast
   5.128 +
   5.129 +lemma UN_o: "UNION A (g o f) = UNION (f`A) g"
   5.130 +by (unfold comp_def, blast)
   5.131 +
   5.132 +text{*Lemma for proving injectivity of representation functions for
   5.133 +datatypes involving function types*}
   5.134 +lemma inj_fun_lemma:
   5.135 +  "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa"
   5.136 +by (simp add: comp_def expand_fun_eq)
   5.137 +
   5.138 +
   5.139 +subsection{*The Injectivity Predicate, @{term inj}*}
   5.140 +
   5.141 +text{*NB: @{term inj} now just translates to @{term inj_on}*}
   5.142 +
   5.143 +
   5.144 +text{*For Proofs in @{text "Tools/datatype_rep_proofs"}*}
   5.145 +lemma datatype_injI:
   5.146 +    "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)"
   5.147 +by (simp add: inj_on_def)
   5.148 +
   5.149 +lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
   5.150 +by (simp add: inj_on_def)
   5.151 +
   5.152 +(*Useful with the simplifier*)
   5.153 +lemma inj_eq: "inj(f) ==> (f(x) = f(y)) = (x=y)"
   5.154 +by (force simp add: inj_on_def)
   5.155 +
   5.156 +lemma inj_o: "[| inj f; f o g = f o h |] ==> g = h"
   5.157 +by (simp add: comp_def inj_on_def expand_fun_eq)
   5.158 +
   5.159 +
   5.160 +subsection{*The Predicate @{term inj_on}: Injectivity On A Restricted Domain*}
   5.161 +
   5.162 +lemma inj_onI:
   5.163 +    "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A"
   5.164 +by (simp add: inj_on_def)
   5.165 +
   5.166 +lemma inj_on_inverseI: "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A"
   5.167 +by (auto dest:  arg_cong [of concl: g] simp add: inj_on_def)
   5.168 +
   5.169 +lemma inj_onD: "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y"
   5.170 +by (unfold inj_on_def, blast)
   5.171 +
   5.172 +lemma inj_on_iff: "[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)"
   5.173 +by (blast dest!: inj_onD)
   5.174 +
   5.175 +lemma comp_inj_on:
   5.176 +     "[| inj_on f A;  inj_on g (f`A) |] ==> inj_on (g o f) A"
   5.177 +by (simp add: comp_def inj_on_def)
   5.178 +
   5.179 +lemma inj_on_contraD: "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)"
   5.180 +by (unfold inj_on_def, blast)
   5.181  
   5.182 -constdefs
   5.183 -  Pi      :: "['a set, 'a => 'b set] => ('a => 'b) set"
   5.184 -    "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = arbitrary}"
   5.185 +lemma inj_singleton: "inj (%s. {s})"
   5.186 +by (simp add: inj_on_def)
   5.187 +
   5.188 +lemma subset_inj_on: "[| A<=B; inj_on f B |] ==> inj_on f A"
   5.189 +by (unfold inj_on_def, blast)
   5.190 +
   5.191 +
   5.192 +subsection{*The Predicate @{term surj}: Surjectivity*}
   5.193 +
   5.194 +lemma surjI: "(!! x. g(f x) = x) ==> surj g"
   5.195 +apply (simp add: surj_def)
   5.196 +apply (blast intro: sym)
   5.197 +done
   5.198 +
   5.199 +lemma surj_range: "surj f ==> range f = UNIV"
   5.200 +by (auto simp add: surj_def)
   5.201 +
   5.202 +lemma surjD: "surj f ==> EX x. y = f x"
   5.203 +by (simp add: surj_def)
   5.204 +
   5.205 +lemma surjE: "surj f ==> (!!x. y = f x ==> C) ==> C"
   5.206 +by (simp add: surj_def, blast)
   5.207 +
   5.208 +lemma comp_surj: "[| surj f;  surj g |] ==> surj (g o f)"
   5.209 +apply (simp add: comp_def surj_def, clarify)
   5.210 +apply (drule_tac x = y in spec, clarify)
   5.211 +apply (drule_tac x = x in spec, blast)
   5.212 +done
   5.213 +
   5.214 +
   5.215 +
   5.216 +subsection{*The Predicate @{term bij}: Bijectivity*}
   5.217 +
   5.218 +lemma bijI: "[| inj f; surj f |] ==> bij f"
   5.219 +by (simp add: bij_def)
   5.220 +
   5.221 +lemma bij_is_inj: "bij f ==> inj f"
   5.222 +by (simp add: bij_def)
   5.223 +
   5.224 +lemma bij_is_surj: "bij f ==> surj f"
   5.225 +by (simp add: bij_def)
   5.226 +
   5.227 +
   5.228 +subsection{*Facts About the Identity Function*}
   5.229  
   5.230 -  restrict :: "['a => 'b, 'a set] => ('a => 'b)"
   5.231 -    "restrict f A == (%x. if x : A then f x else arbitrary)"
   5.232 +text{*We seem to need both the @{term id} forms and the @{term "\<lambda>x. x"}
   5.233 +forms. The latter can arise by rewriting, while @{term id} may be used
   5.234 +explicitly.*}
   5.235 +
   5.236 +lemma image_ident [simp]: "(%x. x) ` Y = Y"
   5.237 +by blast
   5.238 +
   5.239 +lemma image_id [simp]: "id ` Y = Y"
   5.240 +by (simp add: id_def)
   5.241 +
   5.242 +lemma vimage_ident [simp]: "(%x. x) -` Y = Y"
   5.243 +by blast
   5.244 +
   5.245 +lemma vimage_id [simp]: "id -` A = A"
   5.246 +by (simp add: id_def)
   5.247 +
   5.248 +lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}"
   5.249 +by (blast intro: sym)
   5.250 +
   5.251 +lemma image_vimage_subset: "f ` (f -` A) <= A"
   5.252 +by blast
   5.253 +
   5.254 +lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f"
   5.255 +by blast
   5.256 +
   5.257 +lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
   5.258 +by (simp add: surj_range)
   5.259 +
   5.260 +lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
   5.261 +by (simp add: inj_on_def, blast)
   5.262 +
   5.263 +lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A"
   5.264 +apply (unfold surj_def)
   5.265 +apply (blast intro: sym)
   5.266 +done
   5.267 +
   5.268 +lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A"
   5.269 +by (unfold inj_on_def, blast)
   5.270 +
   5.271 +lemma vimage_subset_eq: "bij f ==> (f -` B <= A) = (B <= f ` A)"
   5.272 +apply (unfold bij_def)
   5.273 +apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD)
   5.274 +done
   5.275 +
   5.276 +lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B"
   5.277 +by blast
   5.278 +
   5.279 +lemma image_diff_subset: "f`A - f`B <= f`(A - B)"
   5.280 +by blast
   5.281  
   5.282 -syntax
   5.283 -  "@Pi"  :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3PI _:_./ _)" 10)
   5.284 -  funcset :: "['a set, 'b set] => ('a => 'b) set"      (infixr 60)
   5.285 -  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3%_:_./ _)" [0, 0, 3] 3)
   5.286 -syntax (xsymbols)
   5.287 -  "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)"  ("(3\\<lambda>_\\<in>_./ _)" [0, 0, 3] 3)
   5.288 +lemma inj_on_image_Int:
   5.289 +   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A Int B) = f`A Int f`B"
   5.290 +apply (simp add: inj_on_def, blast)
   5.291 +done
   5.292 +
   5.293 +lemma inj_on_image_set_diff:
   5.294 +   "[| inj_on f C;  A<=C;  B<=C |] ==> f`(A-B) = f`A - f`B"
   5.295 +apply (simp add: inj_on_def, blast)
   5.296 +done
   5.297 +
   5.298 +lemma image_Int: "inj f ==> f`(A Int B) = f`A Int f`B"
   5.299 +by (simp add: inj_on_def, blast)
   5.300 +
   5.301 +lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B"
   5.302 +by (simp add: inj_on_def, blast)
   5.303 +
   5.304 +lemma inj_image_mem_iff: "inj f ==> (f a : f`A) = (a : A)"
   5.305 +by (blast dest: injD)
   5.306 +
   5.307 +lemma inj_image_subset_iff: "inj f ==> (f`A <= f`B) = (A<=B)"
   5.308 +by (simp add: inj_on_def, blast)
   5.309 +
   5.310 +lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)"
   5.311 +by (blast dest: injD)
   5.312 +
   5.313 +lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))"
   5.314 +by blast
   5.315 +
   5.316 +(*injectivity's required.  Left-to-right inclusion holds even if A is empty*)
   5.317 +lemma image_INT:
   5.318 +   "[| inj_on f C;  ALL x:A. B x <= C;  j:A |]
   5.319 +    ==> f ` (INTER A B) = (INT x:A. f ` B x)"
   5.320 +apply (simp add: inj_on_def, blast)
   5.321 +done
   5.322 +
   5.323 +(*Compare with image_INT: no use of inj_on, and if f is surjective then
   5.324 +  it doesn't matter whether A is empty*)
   5.325 +lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)"
   5.326 +apply (simp add: bij_def)
   5.327 +apply (simp add: inj_on_def surj_def, blast)
   5.328 +done
   5.329 +
   5.330 +lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
   5.331 +by (auto simp add: surj_def)
   5.332 +
   5.333 +lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)"
   5.334 +by (auto simp add: inj_on_def)
   5.335  
   5.336 -  (*Giving funcset an arrow syntax (-> or =>) clashes with many existing theories*)
   5.337 +lemma bij_image_Compl_eq: "bij f ==> f`(-A) = -(f`A)"
   5.338 +apply (simp add: bij_def)
   5.339 +apply (rule equalityI)
   5.340 +apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset)
   5.341 +done
   5.342 +
   5.343 +
   5.344 +subsection{*Function Updating*}
   5.345 +
   5.346 +lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)"
   5.347 +apply (simp add: fun_upd_def, safe)
   5.348 +apply (erule subst)
   5.349 +apply (rule_tac [2] ext, auto)
   5.350 +done
   5.351 +
   5.352 +(* f x = y ==> f(x:=y) = f *)
   5.353 +lemmas fun_upd_idem = fun_upd_idem_iff [THEN iffD2, standard]
   5.354 +
   5.355 +(* f(x := f x) = f *)
   5.356 +declare refl [THEN fun_upd_idem, iff]
   5.357 +
   5.358 +lemma fun_upd_apply [simp]: "(f(x:=y))z = (if z=x then y else f z)"
   5.359 +apply (simp (no_asm) add: fun_upd_def)
   5.360 +done
   5.361 +
   5.362 +(* fun_upd_apply supersedes these two,   but they are useful
   5.363 +   if fun_upd_apply is intentionally removed from the simpset *)
   5.364 +lemma fun_upd_same: "(f(x:=y)) x = y"
   5.365 +by simp
   5.366 +
   5.367 +lemma fun_upd_other: "z~=x ==> (f(x:=y)) z = f z"
   5.368 +by simp
   5.369 +
   5.370 +lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)"
   5.371 +by (simp add: expand_fun_eq)
   5.372 +
   5.373 +lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)"
   5.374 +by (rule ext, auto)
   5.375 +
   5.376 +text{*The ML section includes some compatibility bindings and a simproc
   5.377 +for function updates, in addition to the usual ML-bindings of theorems.*}
   5.378 +ML
   5.379 +{*
   5.380 +val id_def = thm "id_def";
   5.381 +val inj_on_def = thm "inj_on_def";
   5.382 +val surj_def = thm "surj_def";
   5.383 +val bij_def = thm "bij_def";
   5.384 +val fun_upd_def = thm "fun_upd_def";
   5.385  
   5.386 -syntax (xsymbols)
   5.387 -  "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set"  ("(3\\<Pi> _\\<in>_./ _)"   10)
   5.388 +val o_def = thm "comp_def";
   5.389 +val injI = thm "inj_onI";
   5.390 +val inj_inverseI = thm "inj_on_inverseI";
   5.391 +val set_cs = claset() delrules [equalityI];
   5.392 +
   5.393 +val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];
   5.394 +
   5.395 +(* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *)
   5.396 +local
   5.397 +  fun gen_fun_upd None T _ _ = None
   5.398 +    | gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y)
   5.399 +  fun dest_fun_T1 (Type (_, T :: Ts)) = T
   5.400 +  fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) =
   5.401 +    let
   5.402 +      fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) =
   5.403 +            if v aconv x then Some g else gen_fun_upd (find g) T v w
   5.404 +        | find t = None
   5.405 +    in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
   5.406 +
   5.407 +  val ss = simpset ()
   5.408 +  val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1)
   5.409 +in
   5.410 +  val fun_upd2_simproc =
   5.411 +    Simplifier.simproc (Theory.sign_of (the_context ()))
   5.412 +      "fun_upd2" ["f(v := w, x := y)"]
   5.413 +      (fn sg => fn _ => fn t =>
   5.414 +        case find_double t of (T, None) => None
   5.415 +        | (T, Some rhs) => Some (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover))
   5.416 +end;
   5.417 +Addsimprocs[fun_upd2_simproc];
   5.418  
   5.419 -translations
   5.420 -  "PI x:A. B" => "Pi A (%x. B)"
   5.421 -  "A funcset B"    => "Pi A (_K B)"
   5.422 -  "%x:A. f"  == "restrict (%x. f) A"
   5.423 -
   5.424 -constdefs
   5.425 -  compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
   5.426 -  "compose A g f == %x:A. g (f x)"
   5.427 +val expand_fun_eq = thm "expand_fun_eq";
   5.428 +val apply_inverse = thm "apply_inverse";
   5.429 +val id_apply = thm "id_apply";
   5.430 +val o_apply = thm "o_apply";
   5.431 +val o_assoc = thm "o_assoc";
   5.432 +val id_o = thm "id_o";
   5.433 +val o_id = thm "o_id";
   5.434 +val image_compose = thm "image_compose";
   5.435 +val image_eq_UN = thm "image_eq_UN";
   5.436 +val UN_o = thm "UN_o";
   5.437 +val inj_fun_lemma = thm "inj_fun_lemma";
   5.438 +val datatype_injI = thm "datatype_injI";
   5.439 +val injD = thm "injD";
   5.440 +val inj_eq = thm "inj_eq";
   5.441 +val inj_o = thm "inj_o";
   5.442 +val inj_onI = thm "inj_onI";
   5.443 +val inj_on_inverseI = thm "inj_on_inverseI";
   5.444 +val inj_onD = thm "inj_onD";
   5.445 +val inj_on_iff = thm "inj_on_iff";
   5.446 +val comp_inj_on = thm "comp_inj_on";
   5.447 +val inj_on_contraD = thm "inj_on_contraD";
   5.448 +val inj_singleton = thm "inj_singleton";
   5.449 +val subset_inj_on = thm "subset_inj_on";
   5.450 +val surjI = thm "surjI";
   5.451 +val surj_range = thm "surj_range";
   5.452 +val surjD = thm "surjD";
   5.453 +val surjE = thm "surjE";
   5.454 +val comp_surj = thm "comp_surj";
   5.455 +val bijI = thm "bijI";
   5.456 +val bij_is_inj = thm "bij_is_inj";
   5.457 +val bij_is_surj = thm "bij_is_surj";
   5.458 +val image_ident = thm "image_ident";
   5.459 +val image_id = thm "image_id";
   5.460 +val vimage_ident = thm "vimage_ident";
   5.461 +val vimage_id = thm "vimage_id";
   5.462 +val vimage_image_eq = thm "vimage_image_eq";
   5.463 +val image_vimage_subset = thm "image_vimage_subset";
   5.464 +val image_vimage_eq = thm "image_vimage_eq";
   5.465 +val surj_image_vimage_eq = thm "surj_image_vimage_eq";
   5.466 +val inj_vimage_image_eq = thm "inj_vimage_image_eq";
   5.467 +val vimage_subsetD = thm "vimage_subsetD";
   5.468 +val vimage_subsetI = thm "vimage_subsetI";
   5.469 +val vimage_subset_eq = thm "vimage_subset_eq";
   5.470 +val image_Int_subset = thm "image_Int_subset";
   5.471 +val image_diff_subset = thm "image_diff_subset";
   5.472 +val inj_on_image_Int = thm "inj_on_image_Int";
   5.473 +val inj_on_image_set_diff = thm "inj_on_image_set_diff";
   5.474 +val image_Int = thm "image_Int";
   5.475 +val image_set_diff = thm "image_set_diff";
   5.476 +val inj_image_mem_iff = thm "inj_image_mem_iff";
   5.477 +val inj_image_subset_iff = thm "inj_image_subset_iff";
   5.478 +val inj_image_eq_iff = thm "inj_image_eq_iff";
   5.479 +val image_UN = thm "image_UN";
   5.480 +val image_INT = thm "image_INT";
   5.481 +val bij_image_INT = thm "bij_image_INT";
   5.482 +val surj_Compl_image_subset = thm "surj_Compl_image_subset";
   5.483 +val inj_image_Compl_subset = thm "inj_image_Compl_subset";
   5.484 +val bij_image_Compl_eq = thm "bij_image_Compl_eq";
   5.485 +val fun_upd_idem_iff = thm "fun_upd_idem_iff";
   5.486 +val fun_upd_idem = thm "fun_upd_idem";
   5.487 +val fun_upd_apply = thm "fun_upd_apply";
   5.488 +val fun_upd_same = thm "fun_upd_same";
   5.489 +val fun_upd_other = thm "fun_upd_other";
   5.490 +val fun_upd_upd = thm "fun_upd_upd";
   5.491 +val fun_upd_twist = thm "fun_upd_twist";
   5.492 +*}
   5.493  
   5.494  end
   5.495 -
   5.496 -ML
   5.497 -val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))];
     6.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Sep 26 10:43:43 2002 +0200
     6.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 26 10:51:29 2002 +0200
     6.3 @@ -39,6 +39,10 @@
     6.4  use "Hilbert_Choice_lemmas.ML"
     6.5  declare someI_ex [elim?];
     6.6  
     6.7 +lemma Inv_mem: "[| f ` A = B;  x \<in> B |] ==> Inv A f x \<in> A"
     6.8 +apply (unfold Inv_def)
     6.9 +apply (fast intro: someI2)
    6.10 +done
    6.11  
    6.12  lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    6.13    -- {* dynamically-scoped fact for TFL *}
     7.1 --- a/src/HOL/Hilbert_Choice_lemmas.ML	Thu Sep 26 10:43:43 2002 +0200
     7.2 +++ b/src/HOL/Hilbert_Choice_lemmas.ML	Thu Sep 26 10:51:29 2002 +0200
     7.3 @@ -212,10 +212,6 @@
     7.4  
     7.5  section "Inverse of a PI-function (restricted domain)";
     7.6  
     7.7 -Goalw [Inv_def] "f ` A = B ==> (%x:B. (Inv A f) x) : B funcset A";
     7.8 -by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
     7.9 -qed "Inv_funcset";
    7.10 -
    7.11  Goal "[| inj_on f A;  x : A |] ==> Inv A f (f x) = x";
    7.12  by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
    7.13  by (blast_tac (claset() addIs [someI2]) 1); 
    7.14 @@ -236,15 +232,6 @@
    7.15  by (blast_tac (claset() addIs [inj_onI] addDs [Inv_injective, injD]) 1);
    7.16  qed "inj_on_Inv";
    7.17  
    7.18 -Goal "[| inj_on f A;  f ` A = B |] \
    7.19 -\     ==> compose A (%y:B. (Inv A f) y) f = (%x:A. x)";
    7.20 -by (asm_simp_tac (simpset() addsimps [compose_def]) 1);
    7.21 -by (rtac restrict_ext 1); 
    7.22 -by Auto_tac; 
    7.23 -by (etac subst 1); 
    7.24 -by (asm_full_simp_tac (simpset() addsimps [Inv_f_f]) 1);
    7.25 -qed "compose_Inv_id";
    7.26 -
    7.27  
    7.28  
    7.29  section "split and SOME";
     8.1 --- a/src/HOL/Induct/LList.thy	Thu Sep 26 10:43:43 2002 +0200
     8.2 +++ b/src/HOL/Induct/LList.thy	Thu Sep 26 10:51:29 2002 +0200
     8.3 @@ -1,7 +1,6 @@
     8.4  (*  Title:      HOL/Induct/LList.thy
     8.5      ID:         $Id$
     8.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1994  University of Cambridge
     8.8  
     8.9  Shares NIL, CONS, List_case with List.thy
    8.10  
    8.11 @@ -445,7 +444,7 @@
    8.12  subsection{* Isomorphisms *}
    8.13  
    8.14  lemma inj_Rep_LList: "inj Rep_LList"
    8.15 -apply (rule inj_inverseI)
    8.16 +apply (rule inj_on_inverseI)
    8.17  apply (rule Rep_LList_inverse)
    8.18  done
    8.19  
     9.1 --- a/src/HOL/IsaMakefile	Thu Sep 26 10:43:43 2002 +0200
     9.2 +++ b/src/HOL/IsaMakefile	Thu Sep 26 10:51:29 2002 +0200
     9.3 @@ -83,7 +83,7 @@
     9.4    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
     9.5    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \
     9.6    Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
     9.7 -  Fun.ML Fun.thy Gfp.ML Gfp.thy \
     9.8 +  Fun.thy Gfp.ML Gfp.thy \
     9.9    Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
    9.10    HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
    9.11    Integ/Equiv.ML Integ/Equiv.thy Integ/int.ML Integ/Int.thy \
    9.12 @@ -197,7 +197,8 @@
    9.13  HOL-Library: HOL $(LOG)/HOL-Library.gz
    9.14  
    9.15  $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
    9.16 -  Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
    9.17 +  Library/FuncSet.thy Library/Library.thy \
    9.18 +  Library/List_Prefix.thy Library/Multiset.thy \
    9.19    Library/Permutation.thy Library/Primes.thy \
    9.20    Library/Quotient.thy Library/Ring_and_Field.thy \
    9.21    Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \
    9.22 @@ -275,20 +276,16 @@
    9.23  HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz
    9.24  
    9.25  $(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \
    9.26 -  Library/Primes.thy \
    9.27 -  GroupTheory/Bij.thy GroupTheory/Bij.ML\
    9.28 -  GroupTheory/Coset.thy GroupTheory/Coset.ML\
    9.29 -  GroupTheory/DirProd.thy GroupTheory/DirProd.ML\
    9.30 -  GroupTheory/Exponent.thy GroupTheory/Exponent.ML\
    9.31 -  GroupTheory/FactGroup.thy GroupTheory/FactGroup.ML\
    9.32 -  GroupTheory/Group.thy GroupTheory/Group.ML\
    9.33 -  GroupTheory/Homomorphism.thy GroupTheory/Homomorphism.ML\
    9.34 -  GroupTheory/PiSets.ML GroupTheory/PiSets.thy \
    9.35 -  GroupTheory/Ring.thy GroupTheory/Ring.ML\
    9.36 -  GroupTheory/RingConstr.thy GroupTheory/RingConstr.ML\
    9.37 -  GroupTheory/Sylow.thy GroupTheory/Sylow.ML\
    9.38 -  GroupTheory/ROOT.ML
    9.39 -	@$(ISATOOL) usedir $(OUT)/HOL GroupTheory
    9.40 +  Library/Primes.thy Library/FuncSet.thy \
    9.41 +  GroupTheory/Bij.thy \
    9.42 +  GroupTheory/Coset.thy \
    9.43 +  GroupTheory/Exponent.thy \
    9.44 +  GroupTheory/Group.thy \
    9.45 +  GroupTheory/Ring.thy \
    9.46 +  GroupTheory/Sylow.thy \
    9.47 +  GroupTheory/ROOT.ML \
    9.48 +  GroupTheory/document/root.tex
    9.49 +	@$(ISATOOL) usedir -g true $(OUT)/HOL GroupTheory
    9.50  
    9.51  
    9.52  ## HOL-Hoare
    10.1 --- a/src/HOL/List.thy	Thu Sep 26 10:43:43 2002 +0200
    10.2 +++ b/src/HOL/List.thy	Thu Sep 26 10:51:29 2002 +0200
    10.3 @@ -451,7 +451,7 @@
    10.4  by (induct ys) (auto simp add: map_eq_Cons)
    10.5  
    10.6  lemma inj_mapI: "inj f ==> inj (map f)"
    10.7 -by (rules dest: map_injective injD intro: injI)
    10.8 +by (rules dest: map_injective injD intro: inj_onI)
    10.9  
   10.10  lemma inj_mapD: "inj (map f) ==> inj f"
   10.11  apply (unfold inj_on_def)
   10.12 @@ -1241,7 +1241,7 @@
   10.13  apply(rule wf_subset)
   10.14   prefer 2 apply (rule Int_lower1)
   10.15  apply(rule wf_prod_fun_image)
   10.16 - prefer 2 apply (rule injI)
   10.17 + prefer 2 apply (rule inj_onI)
   10.18  apply auto
   10.19  done
   10.20  
    11.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Thu Sep 26 10:43:43 2002 +0200
    11.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Sep 26 10:51:29 2002 +0200
    11.3 @@ -230,7 +230,7 @@
    11.4  apply(  simp add: wf_cdecl_def)
    11.5  apply(  rule unique_map_inj)
    11.6  apply(   simp)
    11.7 -apply(  rule injI)
    11.8 +apply(  rule inj_onI)
    11.9  apply(  simp)
   11.10  apply( safe dest!: wf_cdecl_supD)
   11.11  apply( drule subcls1_wfD)
   11.12 @@ -244,7 +244,7 @@
   11.13  apply( erule unique_append)
   11.14  apply(  rule unique_map_inj)
   11.15  apply(   clarsimp)
   11.16 -apply  (rule injI)
   11.17 +apply  (rule inj_onI)
   11.18  apply(  simp)
   11.19  apply(auto dest!: widen_fields_defpl)
   11.20  done
    12.1 --- a/src/HOL/Nat.thy	Thu Sep 26 10:43:43 2002 +0200
    12.2 +++ b/src/HOL/Nat.thy	Thu Sep 26 10:51:29 2002 +0200
    12.3 @@ -80,7 +80,7 @@
    12.4  text {* Isomorphisms: @{text Abs_Nat} and @{text Rep_Nat} *}
    12.5  
    12.6  lemma inj_Rep_Nat: "inj Rep_Nat"
    12.7 -  apply (rule inj_inverseI)
    12.8 +  apply (rule inj_on_inverseI)
    12.9    apply (rule Rep_Nat_inverse)
   12.10    done
   12.11  
   12.12 @@ -111,7 +111,7 @@
   12.13  
   12.14  lemma inj_Suc: "inj Suc"
   12.15    apply (unfold Suc_def)
   12.16 -  apply (rule injI)
   12.17 +  apply (rule inj_onI)
   12.18    apply (drule inj_on_Abs_Nat [THEN inj_onD])
   12.19    apply (rule Rep_Nat Nat.Suc_RepI)+
   12.20    apply (drule inj_Suc_Rep [THEN injD])
    13.1 --- a/src/HOL/Tools/datatype_prop.ML	Thu Sep 26 10:43:43 2002 +0200
    13.2 +++ b/src/HOL/Tools/datatype_prop.ML	Thu Sep 26 10:51:29 2002 +0200
    13.3 @@ -168,7 +168,7 @@
    13.4  
    13.5  fun make_primrecs new_type_names descr sorts thy =
    13.6    let
    13.7 -    val o_name = "Fun.op o";
    13.8 +    val o_name = "Fun.comp";
    13.9  
   13.10      val sign = Theory.sign_of thy;
   13.11  
    14.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 26 10:43:43 2002 +0200
    14.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 26 10:51:29 2002 +0200
    14.3 @@ -55,7 +55,7 @@
    14.4      val Numb_name = "Datatype_Universe.Numb";
    14.5      val Lim_name = "Datatype_Universe.Lim";
    14.6      val Funs_name = "Datatype_Universe.Funs";
    14.7 -    val o_name = "Fun.op o";
    14.8 +    val o_name = "Fun.comp";
    14.9      val sum_case_name = "Datatype.sum.sum_case";
   14.10  
   14.11      val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
    15.1 --- a/src/HOL/ex/Tarski.thy	Thu Sep 26 10:43:43 2002 +0200
    15.2 +++ b/src/HOL/ex/Tarski.thy	Thu Sep 26 10:51:29 2002 +0200
    15.3 @@ -1,12 +1,11 @@
    15.4  (*  Title:      HOL/ex/Tarski.thy
    15.5      ID:         $Id$
    15.6      Author:     Florian Kammüller, Cambridge University Computer Laboratory
    15.7 -    Copyright   1999  University of Cambridge
    15.8  *)
    15.9  
   15.10 -header {* The full theorem of Tarski *}
   15.11 +header {* The Full Theorem of Tarski *}
   15.12  
   15.13 -theory Tarski = Main:
   15.14 +theory Tarski = Main + FuncSet:
   15.15  
   15.16  text {*
   15.17    Minimal version of lattice theory plus the full theorem of Tarski:
   15.18 @@ -21,39 +20,31 @@
   15.19    pset  :: "'a set"
   15.20    order :: "('a * 'a) set"
   15.21  
   15.22 -syntax
   15.23 -  "@pset"  :: "'a potype => 'a set"            ("_ .<A>"  [90] 90)
   15.24 -  "@order" :: "'a potype => ('a *'a)set"       ("_ .<r>"  [90] 90)
   15.25 -
   15.26 -translations
   15.27 -  "po.<A>" == "pset po"
   15.28 -  "po.<r>" == "order po"
   15.29 -
   15.30  constdefs
   15.31    monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
   15.32    "monotone f A r == \<forall>x\<in>A. \<forall>y\<in>A. (x, y): r --> ((f x), (f y)) : r"
   15.33  
   15.34    least :: "['a => bool, 'a potype] => 'a"
   15.35 -  "least P po == @ x. x: po.<A> & P x &
   15.36 -                       (\<forall>y \<in> po.<A>. P y --> (x,y): po.<r>)"
   15.37 +  "least P po == @ x. x: pset po & P x &
   15.38 +                       (\<forall>y \<in> pset po. P y --> (x,y): order po)"
   15.39  
   15.40    greatest :: "['a => bool, 'a potype] => 'a"
   15.41 -  "greatest P po == @ x. x: po.<A> & P x &
   15.42 -                          (\<forall>y \<in> po.<A>. P y --> (y,x): po.<r>)"
   15.43 +  "greatest P po == @ x. x: pset po & P x &
   15.44 +                          (\<forall>y \<in> pset po. P y --> (y,x): order po)"
   15.45  
   15.46    lub  :: "['a set, 'a potype] => 'a"
   15.47 -  "lub S po == least (%x. \<forall>y\<in>S. (y,x): po.<r>) po"
   15.48 +  "lub S po == least (%x. \<forall>y\<in>S. (y,x): order po) po"
   15.49  
   15.50    glb  :: "['a set, 'a potype] => 'a"
   15.51 -  "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): po.<r>) po"
   15.52 +  "glb S po == greatest (%x. \<forall>y\<in>S. (x,y): order po) po"
   15.53  
   15.54    isLub :: "['a set, 'a potype, 'a] => bool"
   15.55 -  "isLub S po == %L. (L: po.<A> & (\<forall>y\<in>S. (y,L): po.<r>) &
   15.56 -                     (\<forall>z\<in>po.<A>. (\<forall>y\<in>S. (y,z): po.<r>) --> (L,z): po.<r>))"
   15.57 +  "isLub S po == %L. (L: pset po & (\<forall>y\<in>S. (y,L): order po) &
   15.58 +                   (\<forall>z\<in>pset po. (\<forall>y\<in>S. (y,z): order po) --> (L,z): order po))"
   15.59  
   15.60    isGlb :: "['a set, 'a potype, 'a] => bool"
   15.61 -  "isGlb S po == %G. (G: po.<A> & (\<forall>y\<in>S. (G,y): po.<r>) &
   15.62 -                     (\<forall>z \<in> po.<A>. (\<forall>y\<in>S. (z,y): po.<r>) --> (z,G): po.<r>))"
   15.63 +  "isGlb S po == %G. (G: pset po & (\<forall>y\<in>S. (G,y): order po) &
   15.64 +                 (\<forall>z \<in> pset po. (\<forall>y\<in>S. (z,y): order po) --> (z,G): order po))"
   15.65  
   15.66    "fix"    :: "[('a => 'a), 'a set] => 'a set"
   15.67    "fix f A  == {x. x: A & f x = x}"
   15.68 @@ -70,17 +61,17 @@
   15.69    "Top po == greatest (%x. True) po"
   15.70  
   15.71    PartialOrder :: "('a potype) set"
   15.72 -  "PartialOrder == {P. refl (P.<A>) (P.<r>) & antisym (P.<r>) &
   15.73 -                       trans (P.<r>)}"
   15.74 +  "PartialOrder == {P. refl (pset P) (order P) & antisym (order P) &
   15.75 +                       trans (order P)}"
   15.76  
   15.77    CompleteLattice :: "('a potype) set"
   15.78    "CompleteLattice == {cl. cl: PartialOrder &
   15.79 -                        (\<forall>S. S <= cl.<A> --> (\<exists>L. isLub S cl L)) &
   15.80 -                        (\<forall>S. S <= cl.<A> --> (\<exists>G. isGlb S cl G))}"
   15.81 +                        (\<forall>S. S <= pset cl --> (\<exists>L. isLub S cl L)) &
   15.82 +                        (\<forall>S. S <= pset cl --> (\<exists>G. isGlb S cl G))}"
   15.83  
   15.84    CLF :: "('a potype * ('a => 'a)) set"
   15.85    "CLF == SIGMA cl: CompleteLattice.
   15.86 -            {f. f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)}"
   15.87 +            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)}"
   15.88  
   15.89    induced :: "['a set, ('a * 'a) set] => ('a *'a)set"
   15.90    "induced A r == {(a,b). a : A & b: A & (a,b): r}"
   15.91 @@ -90,8 +81,8 @@
   15.92    sublattice :: "('a potype * 'a set)set"
   15.93    "sublattice ==
   15.94        SIGMA cl: CompleteLattice.
   15.95 -          {S. S <= cl.<A> &
   15.96 -           (| pset = S, order = induced S (cl.<r>) |): CompleteLattice }"
   15.97 +          {S. S <= pset cl &
   15.98 +           (| pset = S, order = induced S (order cl) |): CompleteLattice }"
   15.99  
  15.100  syntax
  15.101    "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
  15.102 @@ -101,15 +92,15 @@
  15.103  
  15.104  constdefs
  15.105    dual :: "'a potype => 'a potype"
  15.106 -  "dual po == (| pset = po.<A>, order = converse (po.<r>) |)"
  15.107 +  "dual po == (| pset = pset po, order = converse (order po) |)"
  15.108  
  15.109  locale (open) PO =
  15.110    fixes cl :: "'a potype"
  15.111      and A  :: "'a set"
  15.112      and r  :: "('a * 'a) set"
  15.113    assumes cl_po:  "cl : PartialOrder"
  15.114 -  defines A_def: "A == cl.<A>"
  15.115 -     and  r_def: "r == cl.<r>"
  15.116 +  defines A_def: "A == pset cl"
  15.117 +     and  r_def: "r == order cl"
  15.118  
  15.119  locale (open) CL = PO +
  15.120    assumes cl_co:  "cl : CompleteLattice"
  15.121 @@ -254,8 +245,8 @@
  15.122  by (rule PO_imp_trans)
  15.123  
  15.124  lemma CompleteLatticeI:
  15.125 -     "[| po \<in> PartialOrder; (\<forall>S. S <= po.<A> --> (\<exists>L. isLub S po L));
  15.126 -         (\<forall>S. S <= po.<A> --> (\<exists>G. isGlb S po G))|]
  15.127 +     "[| po \<in> PartialOrder; (\<forall>S. S <= pset po --> (\<exists>L. isLub S po L));
  15.128 +         (\<forall>S. S <= pset po --> (\<exists>G. isGlb S po G))|]
  15.129        ==> po \<in> CompleteLattice"
  15.130  apply (unfold CompleteLattice_def, blast)
  15.131  done
  15.132 @@ -268,19 +259,19 @@
  15.133                   dualPO)
  15.134  done
  15.135  
  15.136 -lemma (in PO) dualA_iff: "(dual cl.<A>) = cl.<A>"
  15.137 +lemma (in PO) dualA_iff: "pset (dual cl) = pset cl"
  15.138  by (simp add: dual_def)
  15.139  
  15.140 -lemma (in PO) dualr_iff: "((x, y) \<in> (dual cl.<r>)) = ((y, x) \<in> cl.<r>)"
  15.141 +lemma (in PO) dualr_iff: "((x, y) \<in> (order(dual cl))) = ((y, x) \<in> order cl)"
  15.142  by (simp add: dual_def)
  15.143  
  15.144  lemma (in PO) monotone_dual:
  15.145 -     "monotone f (cl.<A>) (cl.<r>) ==> monotone f (dual cl.<A>) (dual cl.<r>)"
  15.146 -apply (simp add: monotone_def dualA_iff dualr_iff)
  15.147 -done
  15.148 +     "monotone f (pset cl) (order cl) 
  15.149 +     ==> monotone f (pset (dual cl)) (order(dual cl))"
  15.150 +by (simp add: monotone_def dualA_iff dualr_iff)
  15.151  
  15.152  lemma (in PO) interval_dual:
  15.153 -     "[| x \<in> A; y \<in> A|] ==> interval r x y = interval (dual cl.<r>) y x"
  15.154 +     "[| x \<in> A; y \<in> A|] ==> interval r x y = interval (order(dual cl)) y x"
  15.155  apply (simp add: interval_def dualr_iff)
  15.156  apply (fold r_def, fast)
  15.157  done
  15.158 @@ -416,7 +407,7 @@
  15.159  *}
  15.160  
  15.161  lemma (in CLF) [simp]:
  15.162 -    "f: cl.<A> funcset cl.<A> & monotone f (cl.<A>) (cl.<r>)"
  15.163 +    "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
  15.164  apply (insert f_cl)
  15.165  apply (simp add: CLF_def)
  15.166  done
  15.167 @@ -424,7 +415,7 @@
  15.168  declare (in CLF) f_cl [simp]
  15.169  
  15.170  
  15.171 -lemma (in CLF) f_in_funcset: "f \<in> A funcset A"
  15.172 +lemma (in CLF) f_in_funcset: "f \<in> A -> A"
  15.173  by (simp add: A_def)
  15.174  
  15.175  lemma (in CLF) monotone_f: "monotone f A r"
  15.176 @@ -460,7 +451,7 @@
  15.177  apply (rule ballI)
  15.178  apply (rule transE)
  15.179  apply (rule CO_trans)
  15.180 --- {* instantiates @{text "(x, ???z) \<in> cl.<r> to (x, f x)"}, *}
  15.181 +-- {* instantiates @{text "(x, ???z) \<in> order cl to (x, f x)"}, *}
  15.182  -- {* because of the def of @{text H} *}
  15.183  apply fast
  15.184  -- {* so it remains to show @{text "(f x, f (lub H cl)) \<in> r"} *}
  15.185 @@ -807,7 +798,7 @@
  15.186  apply (simp add: intY1_def interval_def  intY1_elem)
  15.187  done
  15.188  
  15.189 -lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 funcset intY1"
  15.190 +lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
  15.191  apply (rule restrictI)
  15.192  apply (erule intY1_f_closed)
  15.193  done