--- a/src/ZF/Constructible/Relative.thy Tue Feb 04 16:36:49 2020 +0100
+++ b/src/ZF/Constructible/Relative.thy Tue Feb 04 16:19:15 2020 +0000
@@ -1,5 +1,7 @@
(* Title: ZF/Constructible/Relative.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ With modifications by E. Gunther, M. Pagano,
+ and P. Sánchez Terraf
*)
section \<open>Relativization and Absoluteness\<close>
@@ -404,7 +406,7 @@
lemma Collect_in_univ:
"[| X \<in> univ(A); Transset(A) |] ==> Collect(X,P) \<in> univ(A)"
-by (simp add: univ_def Collect_in_VLimit Limit_nat)
+by (simp add: univ_def Collect_in_VLimit)
lemma "separation(\<lambda>x. x \<in> univ(0), P)"
apply (simp add: separation_def, clarify)
@@ -430,7 +432,7 @@
lemma Pow_in_univ:
"[| X \<in> univ(A); Transset(A) |] ==> Pow(X) \<in> univ(A)"
-apply (simp add: univ_def Pow_in_VLimit Limit_nat)
+apply (simp add: univ_def Pow_in_VLimit)
done
lemma "power_ax(\<lambda>x. x \<in> univ(0))"
@@ -522,32 +524,52 @@
subsection\<open>Introducing a Transitive Class Model\<close>
+text\<open>The class M is assumed to be transitive and inhabited\<close>
+locale M_trans =
+ fixes M
+ assumes transM: "[| y\<in>x; M(x) |] ==> M(y)"
+ and M_inhabited: "\<exists>x . M(x)"
+
+lemma (in M_trans) nonempty [simp]: "M(0)"
+proof -
+ have "M(x) \<longrightarrow> M(0)" for x
+ proof (rule_tac P="\<lambda>w. M(w) \<longrightarrow> M(0)" in eps_induct)
+ {
+ fix x
+ assume "\<forall>y\<in>x. M(y) \<longrightarrow> M(0)" "M(x)"
+ consider (a) "\<exists>y. y\<in>x" | (b) "x=0" by auto
+ then
+ have "M(x) \<longrightarrow> M(0)"
+ proof cases
+ case a
+ then show ?thesis using \<open>\<forall>y\<in>x._\<close> \<open>M(x)\<close> transM by auto
+ next
+ case b
+ then show ?thesis by simp
+ qed
+ }
+ then show "M(x) \<longrightarrow> M(0)" if "\<forall>y\<in>x. M(y) \<longrightarrow> M(0)" for x
+ using that by auto
+ qed
+ with M_inhabited
+ show "M(0)" using M_inhabited by blast
+qed
+
text\<open>The class M is assumed to be transitive and to satisfy some
relativized ZF axioms\<close>
-locale M_trivial =
- fixes M
- assumes transM: "[| y\<in>x; M(x) |] ==> M(y)"
- and upair_ax: "upair_ax(M)"
+locale M_trivial = M_trans +
+ assumes upair_ax: "upair_ax(M)"
and Union_ax: "Union_ax(M)"
- and power_ax: "power_ax(M)"
- and replacement: "replacement(M,P)"
- and M_nat [iff]: "M(nat)" (*i.e. the axiom of infinity*)
-
-text\<open>Automatically discovers the proof using \<open>transM\<close>, \<open>nat_0I\<close>
-and \<open>M_nat\<close>.\<close>
-lemma (in M_trivial) nonempty [simp]: "M(0)"
-by (blast intro: transM)
-
-lemma (in M_trivial) rall_abs [simp]:
+lemma (in M_trans) rall_abs [simp]:
"M(A) ==> (\<forall>x[M]. x\<in>A \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x\<in>A. P(x))"
by (blast intro: transM)
-lemma (in M_trivial) rex_abs [simp]:
+lemma (in M_trans) rex_abs [simp]:
"M(A) ==> (\<exists>x[M]. x\<in>A & P(x)) \<longleftrightarrow> (\<exists>x\<in>A. P(x))"
by (blast intro: transM)
-lemma (in M_trivial) ball_iff_equiv:
+lemma (in M_trans) ball_iff_equiv:
"M(A) ==> (\<forall>x[M]. (x\<in>A \<longleftrightarrow> P(x))) \<longleftrightarrow>
(\<forall>x\<in>A. P(x)) & (\<forall>x. P(x) \<longrightarrow> M(x) \<longrightarrow> x\<in>A)"
by (blast intro: transM)
@@ -556,56 +578,76 @@
available for rewriting, universally quantified over M.
But it's not the only way to prove such equalities: its
premises \<^term>\<open>M(A)\<close> and \<^term>\<open>M(B)\<close> can be too strong.\<close>
-lemma (in M_trivial) M_equalityI:
+lemma (in M_trans) M_equalityI:
"[| !!x. M(x) ==> x\<in>A \<longleftrightarrow> x\<in>B; M(A); M(B) |] ==> A=B"
-by (blast intro!: equalityI dest: transM)
+by (blast dest: transM)
subsubsection\<open>Trivial Absoluteness Proofs: Empty Set, Pairs, etc.\<close>
-lemma (in M_trivial) empty_abs [simp]:
+lemma (in M_trans) empty_abs [simp]:
"M(z) ==> empty(M,z) \<longleftrightarrow> z=0"
apply (simp add: empty_def)
apply (blast intro: transM)
done
-lemma (in M_trivial) subset_abs [simp]:
+lemma (in M_trans) subset_abs [simp]:
"M(A) ==> subset(M,A,B) \<longleftrightarrow> A \<subseteq> B"
apply (simp add: subset_def)
apply (blast intro: transM)
done
-lemma (in M_trivial) upair_abs [simp]:
+lemma (in M_trans) upair_abs [simp]:
"M(z) ==> upair(M,a,b,z) \<longleftrightarrow> z={a,b}"
apply (simp add: upair_def)
apply (blast intro: transM)
done
-lemma (in M_trivial) upair_in_M_iff [iff]:
- "M({a,b}) \<longleftrightarrow> M(a) & M(b)"
-apply (insert upair_ax, simp add: upair_ax_def)
-apply (blast intro: transM)
-done
+lemma (in M_trivial) upair_in_MI [intro!]:
+ " M(a) & M(b) \<Longrightarrow> M({a,b})"
+by (insert upair_ax, simp add: upair_ax_def)
+
+lemma (in M_trans) upair_in_MD [dest!]:
+ "M({a,b}) \<Longrightarrow> M(a) & M(b)"
+ by (blast intro: transM)
+
+lemma (in M_trivial) upair_in_M_iff [simp]:
+ "M({a,b}) \<longleftrightarrow> M(a) & M(b)"
+ by blast
-lemma (in M_trivial) singleton_in_M_iff [iff]:
+lemma (in M_trivial) singleton_in_MI [intro!]:
+ "M(a) \<Longrightarrow> M({a})"
+ by (insert upair_in_M_iff [of a a], simp)
+
+lemma (in M_trans) singleton_in_MD [dest!]:
+ "M({a}) \<Longrightarrow> M(a)"
+ by (insert upair_in_MD [of a a], simp)
+
+lemma (in M_trivial) singleton_in_M_iff [simp]:
"M({a}) \<longleftrightarrow> M(a)"
-by (insert upair_in_M_iff [of a a], simp)
+ by blast
-lemma (in M_trivial) pair_abs [simp]:
+lemma (in M_trans) pair_abs [simp]:
"M(z) ==> pair(M,a,b,z) \<longleftrightarrow> z=<a,b>"
apply (simp add: pair_def Pair_def)
apply (blast intro: transM)
done
-lemma (in M_trivial) pair_in_M_iff [iff]:
- "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
-by (simp add: Pair_def)
+lemma (in M_trans) pair_in_MD [dest!]:
+ "M(<a,b>) \<Longrightarrow> M(a) & M(b)"
+ by (simp add: Pair_def, blast intro: transM)
+
+lemma (in M_trivial) pair_in_MI [intro!]:
+ "M(a) & M(b) \<Longrightarrow> M(<a,b>)"
+ by (simp add: Pair_def)
-lemma (in M_trivial) pair_components_in_M:
+lemma (in M_trivial) pair_in_M_iff [simp]:
+ "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
+ by blast
+
+lemma (in M_trans) pair_components_in_M:
"[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
-apply (simp add: Pair_def)
-apply (blast dest: transM)
-done
+ by (blast dest: transM)
lemma (in M_trivial) cartprod_abs [simp]:
"[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) \<longleftrightarrow> z = A*B"
@@ -617,29 +659,25 @@
subsubsection\<open>Absoluteness for Unions and Intersections\<close>
-lemma (in M_trivial) union_abs [simp]:
+lemma (in M_trans) union_abs [simp]:
"[| M(a); M(b); M(z) |] ==> union(M,a,b,z) \<longleftrightarrow> z = a \<union> b"
-apply (simp add: union_def)
-apply (blast intro: transM)
-done
+ unfolding union_def
+ by (blast intro: transM )
-lemma (in M_trivial) inter_abs [simp]:
+lemma (in M_trans) inter_abs [simp]:
"[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) \<longleftrightarrow> z = a \<inter> b"
-apply (simp add: inter_def)
-apply (blast intro: transM)
-done
+ unfolding inter_def
+ by (blast intro: transM)
-lemma (in M_trivial) setdiff_abs [simp]:
+lemma (in M_trans) setdiff_abs [simp]:
"[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) \<longleftrightarrow> z = a-b"
-apply (simp add: setdiff_def)
-apply (blast intro: transM)
-done
+ unfolding setdiff_def
+ by (blast intro: transM)
-lemma (in M_trivial) Union_abs [simp]:
+lemma (in M_trans) Union_abs [simp]:
"[| M(A); M(z) |] ==> big_union(M,A,z) \<longleftrightarrow> z = \<Union>(A)"
-apply (simp add: big_union_def)
-apply (blast intro!: equalityI dest: transM)
-done
+ unfolding big_union_def
+ by (blast dest: transM)
lemma (in M_trivial) Union_closed [intro,simp]:
"M(A) ==> M(\<Union>(A))"
@@ -661,15 +699,23 @@
"[| M(a); M(z) |] ==> successor(M,a,z) \<longleftrightarrow> z = succ(a)"
by (simp add: successor_def, blast)
-lemma (in M_trivial) succ_in_M_iff [iff]:
+lemma (in M_trans) succ_in_MD [dest!]:
+ "M(succ(a)) \<Longrightarrow> M(a)"
+ unfolding succ_def
+ by (blast intro: transM)
+
+lemma (in M_trivial) succ_in_MI [intro!]:
+ "M(a) \<Longrightarrow> M(succ(a))"
+ unfolding succ_def
+ by (blast intro: transM)
+
+lemma (in M_trivial) succ_in_M_iff [simp]:
"M(succ(a)) \<longleftrightarrow> M(a)"
-apply (simp add: succ_def)
-apply (blast intro: transM)
-done
+ by blast
subsubsection\<open>Absoluteness for Separation and Replacement\<close>
-lemma (in M_trivial) separation_closed [intro,simp]:
+lemma (in M_trans) separation_closed [intro,simp]:
"[| separation(M,P); M(A) |] ==> M(Collect(A,P))"
apply (insert separation, simp add: separation_def)
apply (drule rspec, assumption, clarify)
@@ -681,22 +727,10 @@
"separation(M,P) \<longleftrightarrow> (\<forall>z[M]. \<exists>y[M]. is_Collect(M,z,P,y))"
by (simp add: separation_def is_Collect_def)
-lemma (in M_trivial) Collect_abs [simp]:
+lemma (in M_trans) Collect_abs [simp]:
"[| M(A); M(z) |] ==> is_Collect(M,A,P,z) \<longleftrightarrow> z = Collect(A,P)"
-apply (simp add: is_Collect_def)
-apply (blast intro!: equalityI dest: transM)
-done
-
-text\<open>Probably the premise and conclusion are equivalent\<close>
-lemma (in M_trivial) strong_replacementI [rule_format]:
- "[| \<forall>B[M]. separation(M, %u. \<exists>x[M]. x\<in>B & P(x,u)) |]
- ==> strong_replacement(M,P)"
-apply (simp add: strong_replacement_def, clarify)
-apply (frule replacementD [OF replacement], assumption, clarify)
-apply (drule_tac x=A in rspec, clarify)
-apply (drule_tac z=Y in separationD, assumption, clarify)
-apply (rule_tac x=y in rexI, force, assumption)
-done
+ unfolding is_Collect_def
+ by (blast dest: transM)
subsubsection\<open>The Operator \<^term>\<open>is_Replace\<close>\<close>
@@ -709,16 +743,15 @@
is_Replace(M, A', %x y. P'(x,y), z')"
by (simp add: is_Replace_def)
-lemma (in M_trivial) univalent_Replace_iff:
+lemma (in M_trans) univalent_Replace_iff:
"[| M(A); univalent(M,A,P);
!!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
==> u \<in> Replace(A,P) \<longleftrightarrow> (\<exists>x. x\<in>A & P(x,u))"
-apply (simp add: Replace_iff univalent_def)
-apply (blast dest: transM)
-done
+ unfolding Replace_iff univalent_def
+ by (blast dest: transM)
(*The last premise expresses that P takes M to M*)
-lemma (in M_trivial) strong_replacement_closed [intro,simp]:
+lemma (in M_trans) strong_replacement_closed [intro,simp]:
"[| strong_replacement(M,P); M(A); univalent(M,A,P);
!!x y. [| x\<in>A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))"
apply (simp add: strong_replacement_def)
@@ -730,7 +763,7 @@
apply (blast dest: transM)
done
-lemma (in M_trivial) Replace_abs:
+lemma (in M_trans) Replace_abs:
"[| M(A); M(z); univalent(M,A,P);
!!x y. [| x\<in>A; P(x,y) |] ==> M(y) |]
==> is_Replace(M,A,P,z) \<longleftrightarrow> z = Replace(A,P)"
@@ -749,7 +782,7 @@
nonconstructible set. So we cannot assume that M(X) implies M(RepFun(X,f))
even for f \<in> M -> M.
*)
-lemma (in M_trivial) RepFun_closed:
+lemma (in M_trans) RepFun_closed:
"[| strong_replacement(M, \<lambda>x y. y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
==> M(RepFun(A,f))"
apply (simp add: RepFun_def)
@@ -760,7 +793,7 @@
text\<open>Better than \<open>RepFun_closed\<close> when having the formula \<^term>\<open>x\<in>A\<close>
makes relativization easier.\<close>
-lemma (in M_trivial) RepFun_closed2:
+lemma (in M_trans) RepFun_closed2:
"[| strong_replacement(M, \<lambda>x y. x\<in>A & y = f(x)); M(A); \<forall>x\<in>A. M(f(x)) |]
==> M(RepFun(A, %x. f(x)))"
apply (simp add: RepFun_def)
@@ -809,35 +842,60 @@
is_lambda(M, A', %x y. is_b'(x,y), z')"
by (simp add: is_lambda_def)
-lemma (in M_trivial) image_abs [simp]:
+lemma (in M_trans) image_abs [simp]:
"[| M(r); M(A); M(z) |] ==> image(M,r,A,z) \<longleftrightarrow> z = r``A"
apply (simp add: image_def)
apply (rule iffI)
apply (blast intro!: equalityI dest: transM, blast)
done
+subsubsection\<open>Relativization of Powerset\<close>
+
text\<open>What about \<open>Pow_abs\<close>? Powerset is NOT absolute!
This result is one direction of absoluteness.\<close>
-lemma (in M_trivial) powerset_Pow:
+lemma (in M_trans) powerset_Pow:
"powerset(M, x, Pow(x))"
by (simp add: powerset_def)
text\<open>But we can't prove that the powerset in \<open>M\<close> includes the
real powerset.\<close>
-lemma (in M_trivial) powerset_imp_subset_Pow:
+
+lemma (in M_trans) powerset_imp_subset_Pow:
"[| powerset(M,x,y); M(y) |] ==> y \<subseteq> Pow(x)"
apply (simp add: powerset_def)
apply (blast dest: transM)
done
+lemma (in M_trans) powerset_abs:
+ assumes
+ "M(y)"
+ shows
+ "powerset(M,x,y) \<longleftrightarrow> y = {a\<in>Pow(x) . M(a)}"
+proof (intro iffI equalityI)
+ (* First show the converse implication by double inclusion *)
+ assume "powerset(M,x,y)"
+ with \<open>M(y)\<close>
+ show "y \<subseteq> {a\<in>Pow(x) . M(a)}"
+ using powerset_imp_subset_Pow transM by blast
+ from \<open>powerset(M,x,y)\<close>
+ show "{a\<in>Pow(x) . M(a)} \<subseteq> y"
+ using transM unfolding powerset_def by auto
+next (* we show the direct implication *)
+ assume
+ "y = {a \<in> Pow(x) . M(a)}"
+ then
+ show "powerset(M, x, y)"
+ unfolding powerset_def subset_def using transM by blast
+qed
+
subsubsection\<open>Absoluteness for the Natural Numbers\<close>
lemma (in M_trivial) nat_into_M [intro]:
"n \<in> nat ==> M(n)"
by (induct n rule: nat_induct, simp_all)
-lemma (in M_trivial) nat_case_closed [intro,simp]:
+lemma (in M_trans) nat_case_closed [intro,simp]:
"[|M(k); M(a); \<forall>m[M]. M(b(m))|] ==> M(nat_case(a,b,k))"
apply (case_tac "k=0", simp)
apply (case_tac "\<exists>m. k = succ(m)", force)
@@ -873,15 +931,15 @@
subsection\<open>Absoluteness for Ordinals\<close>
text\<open>These results constitute Theorem IV 5.1 of Kunen (page 126).\<close>
-lemma (in M_trivial) lt_closed:
+lemma (in M_trans) lt_closed:
"[| j<i; M(i) |] ==> M(j)"
by (blast dest: ltD intro: transM)
-lemma (in M_trivial) transitive_set_abs [simp]:
+lemma (in M_trans) transitive_set_abs [simp]:
"M(a) ==> transitive_set(M,a) \<longleftrightarrow> Transset(a)"
by (simp add: transitive_set_def Transset_def)
-lemma (in M_trivial) ordinal_abs [simp]:
+lemma (in M_trans) ordinal_abs [simp]:
"M(a) ==> ordinal(M,a) \<longleftrightarrow> Ord(a)"
by (simp add: ordinal_def Ord_def)
@@ -999,8 +1057,9 @@
pair(M,x,a,xa) & xa \<in> r & pair(M,x,b,xb) & xb \<in> r &
(\<exists>fx[M]. \<exists>gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) &
fx \<noteq> gx))"
+ and power_ax: "power_ax(M)"
-lemma (in M_basic) cartprod_iff_lemma:
+lemma (in M_trivial) cartprod_iff_lemma:
"[| M(C); \<forall>u[M]. u \<in> C \<longleftrightarrow> (\<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}});
powerset(M, A \<union> B, p1); powerset(M, p1, p2); M(p2) |]
==> C = {u \<in> p2 . \<exists>x\<in>A. \<exists>y\<in>B. u = {{x}, {x,y}}}"
@@ -1125,7 +1184,7 @@
subsubsection\<open>Domain, range and field\<close>
-lemma (in M_basic) domain_abs [simp]:
+lemma (in M_trans) domain_abs [simp]:
"[| M(r); M(z) |] ==> is_domain(M,r,z) \<longleftrightarrow> z = domain(r)"
apply (simp add: is_domain_def)
apply (blast intro!: equalityI dest: transM)
@@ -1136,7 +1195,7 @@
apply (simp add: domain_eq_vimage)
done
-lemma (in M_basic) range_abs [simp]:
+lemma (in M_trans) range_abs [simp]:
"[| M(r); M(z) |] ==> is_range(M,r,z) \<longleftrightarrow> z = range(r)"
apply (simp add: is_range_def)
apply (blast intro!: equalityI dest: transM)
@@ -1149,22 +1208,22 @@
lemma (in M_basic) field_abs [simp]:
"[| M(r); M(z) |] ==> is_field(M,r,z) \<longleftrightarrow> z = field(r)"
-by (simp add: domain_closed range_closed is_field_def field_def)
+by (simp add: is_field_def field_def)
lemma (in M_basic) field_closed [intro,simp]:
"M(r) ==> M(field(r))"
-by (simp add: domain_closed range_closed Un_closed field_def)
+by (simp add: field_def)
subsubsection\<open>Relations, functions and application\<close>
-lemma (in M_basic) relation_abs [simp]:
+lemma (in M_trans) relation_abs [simp]:
"M(r) ==> is_relation(M,r) \<longleftrightarrow> relation(r)"
apply (simp add: is_relation_def relation_def)
apply (blast dest!: bspec dest: pair_components_in_M)+
done
-lemma (in M_basic) function_abs [simp]:
+lemma (in M_trivial) function_abs [simp]:
"M(r) ==> is_function(M,r) \<longleftrightarrow> function(r)"
apply (simp add: is_function_def function_def, safe)
apply (frule transM, assumption)
@@ -1180,7 +1239,7 @@
apply (simp add: fun_apply_def apply_def, blast)
done
-lemma (in M_basic) typed_function_abs [simp]:
+lemma (in M_trivial) typed_function_abs [simp]:
"[| M(A); M(f) |] ==> typed_function(M,A,B,f) \<longleftrightarrow> f \<in> A -> B"
apply (auto simp add: typed_function_def relation_def Pi_iff)
apply (blast dest: pair_components_in_M)+
@@ -1188,7 +1247,7 @@
lemma (in M_basic) injection_abs [simp]:
"[| M(A); M(f) |] ==> injection(M,A,B,f) \<longleftrightarrow> f \<in> inj(A,B)"
-apply (simp add: injection_def apply_iff inj_def apply_closed)
+apply (simp add: injection_def apply_iff inj_def)
apply (blast dest: transM [of _ A])
done
@@ -1242,7 +1301,7 @@
apply (unfold function_def, blast)
done
-lemma (in M_basic) restriction_abs [simp]:
+lemma (in M_trans) restriction_abs [simp]:
"[| M(f); M(A); M(z) |]
==> restriction(M,f,A,z) \<longleftrightarrow> z = restrict(f,A)"
apply (simp add: ball_iff_equiv restriction_def restrict_def)
@@ -1250,7 +1309,7 @@
done
-lemma (in M_basic) M_restrict_iff:
+lemma (in M_trans) M_restrict_iff:
"M(r) ==> restrict(r,A) = {z \<in> r . \<exists>x\<in>A. \<exists>y[M]. z = \<langle>x, y\<rangle>}"
by (simp add: restrict_def, blast dest: transM)
@@ -1260,7 +1319,7 @@
apply (insert restrict_separation [of A], simp)
done
-lemma (in M_basic) Inter_abs [simp]:
+lemma (in M_trans) Inter_abs [simp]:
"[| M(A); M(z) |] ==> big_inter(M,A,z) \<longleftrightarrow> z = \<Inter>(A)"
apply (simp add: big_inter_def Inter_def)
apply (blast intro!: equalityI dest: transM)
@@ -1296,12 +1355,11 @@
"A - Collect(A,P) = Collect(A, %x. ~ P(x))"
by blast
-lemma (in M_trivial) Collect_rall_eq:
+lemma (in M_trans) Collect_rall_eq:
"M(Y) ==> Collect(A, %x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y)) =
(if Y=0 then A else (\<Inter>y \<in> Y. {x \<in> A. P(x,y)}))"
-apply simp
-apply (blast intro!: equalityI dest: transM)
-done
+ by (simp,blast dest: transM)
+
lemma (in M_basic) separation_disj:
"[|separation(M,P); separation(M,Q)|] ==> separation(M, \<lambda>z. P(z) | Q(z))"
@@ -1327,7 +1385,7 @@
==> separation(M, \<lambda>x. \<forall>y[M]. y\<in>Y \<longrightarrow> P(x,y))"
apply (simp del: separation_closed rall_abs
add: separation_iff Collect_rall_eq)
-apply (blast intro!: Inter_closed RepFun_closed dest: transM)
+apply (blast intro!: RepFun_closed dest: transM)
done
@@ -1335,7 +1393,7 @@
text\<open>The assumption \<^term>\<open>M(A->B)\<close> is unusual, but essential: in
all but trivial cases, A->B cannot be expected to belong to \<^term>\<open>M\<close>.\<close>
-lemma (in M_basic) is_funspace_abs [simp]:
+lemma (in M_trivial) is_funspace_abs [simp]:
"[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) \<longleftrightarrow> F = A->B"
apply (simp add: is_funspace_def)
apply (rule iffI)