author | paulson <lp15@cam.ac.uk> |
Tue, 27 Sep 2022 17:46:52 +0100 | |
changeset 76215 | a642599ffdea |
parent 76213 | e44d86131648 |
child 76216 | 9fc34f76b4e8 |
permissions | -rw-r--r-- |
12610 | 1 |
(* Title: ZF/Induct/Rmap.thy |
12088 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1994 University of Cambridge |
|
12610 | 4 |
*) |
12088 | 5 |
|
60770 | 6 |
section \<open>An operator to ``map'' a relation over a list\<close> |
12088 | 7 |
|
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
61798
diff
changeset
|
8 |
theory Rmap imports ZF begin |
12088 | 9 |
|
10 |
consts |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76213
diff
changeset
|
11 |
rmap :: "i\<Rightarrow>i" |
12088 | 12 |
|
13 |
inductive |
|
12610 | 14 |
domains "rmap(r)" \<subseteq> "list(domain(r)) \<times> list(range(r))" |
12560 | 15 |
intros |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76213
diff
changeset
|
16 |
NilI: "\<langle>Nil,Nil\<rangle> \<in> rmap(r)" |
12560 | 17 |
|
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76213
diff
changeset
|
18 |
ConsI: "\<lbrakk>\<langle>x,y\<rangle>: r; \<langle>xs,ys\<rangle> \<in> rmap(r)\<rbrakk> |
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
19 |
\<Longrightarrow> <Cons(x,xs), Cons(y,ys)> \<in> rmap(r)" |
12560 | 20 |
|
21 |
type_intros domainI rangeI list.intros |
|
22 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
23 |
lemma rmap_mono: "r \<subseteq> s \<Longrightarrow> rmap(r) \<subseteq> rmap(s)" |
12610 | 24 |
apply (unfold rmap.defs) |
25 |
apply (rule lfp_mono) |
|
26 |
apply (rule rmap.bnd_mono)+ |
|
27 |
apply (assumption | rule Sigma_mono list_mono domain_mono range_mono basic_monos)+ |
|
28 |
done |
|
12560 | 29 |
|
12610 | 30 |
inductive_cases |
76215
a642599ffdea
More syntactic cleanup. LaTeX markup working
paulson <lp15@cam.ac.uk>
parents:
76213
diff
changeset
|
31 |
Nil_rmap_case [elim!]: "\<langle>Nil,zs\<rangle> \<in> rmap(r)" |
12610 | 32 |
and Cons_rmap_case [elim!]: "<Cons(x,xs),zs> \<in> rmap(r)" |
12560 | 33 |
|
34 |
declare rmap.intros [intro] |
|
35 |
||
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
36 |
lemma rmap_rel_type: "r \<subseteq> A \<times> B \<Longrightarrow> rmap(r) \<subseteq> list(A) \<times> list(B)" |
12610 | 37 |
apply (rule rmap.dom_subset [THEN subset_trans]) |
38 |
apply (assumption | |
|
39 |
rule domain_rel_subset range_rel_subset Sigma_mono list_mono)+ |
|
40 |
done |
|
12088 | 41 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
42 |
lemma rmap_total: "A \<subseteq> domain(r) \<Longrightarrow> list(A) \<subseteq> domain(rmap(r))" |
12610 | 43 |
apply (rule subsetI) |
44 |
apply (erule list.induct) |
|
45 |
apply blast+ |
|
46 |
done |
|
12560 | 47 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
48 |
lemma rmap_functional: "function(r) \<Longrightarrow> function(rmap(r))" |
12610 | 49 |
apply (unfold function_def) |
50 |
apply (rule impI [THEN allI, THEN allI]) |
|
51 |
apply (erule rmap.induct) |
|
52 |
apply blast+ |
|
53 |
done |
|
12088 | 54 |
|
60770 | 55 |
text \<open> |
61798 | 56 |
\medskip If \<open>f\<close> is a function then \<open>rmap(f)\<close> behaves |
12610 | 57 |
as expected. |
60770 | 58 |
\<close> |
12560 | 59 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
60 |
lemma rmap_fun_type: "f \<in> A->B \<Longrightarrow> rmap(f): list(A)->list(B)" |
12610 | 61 |
by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total) |
12560 | 62 |
|
63 |
lemma rmap_Nil: "rmap(f)`Nil = Nil" |
|
12610 | 64 |
by (unfold apply_def) blast |
12560 | 65 |
|
76213
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
66 |
lemma rmap_Cons: "\<lbrakk>f \<in> A->B; x \<in> A; xs: list(A)\<rbrakk> |
e44d86131648
Removal of obsolete ASCII syntax
paulson <lp15@cam.ac.uk>
parents:
65449
diff
changeset
|
67 |
\<Longrightarrow> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)" |
12610 | 68 |
by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros) |
12088 | 69 |
|
70 |
end |