--- a/src/ZF/Constructible/Formula.thy Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/Constructible/Formula.thy Tue Sep 27 16:51:35 2022 +0100
@@ -22,46 +22,46 @@
definition
Neg :: "i=>i" where
- "Neg(p) == Nand(p,p)"
+ "Neg(p) \<equiv> Nand(p,p)"
definition
And :: "[i,i]=>i" where
- "And(p,q) == Neg(Nand(p,q))"
+ "And(p,q) \<equiv> Neg(Nand(p,q))"
definition
Or :: "[i,i]=>i" where
- "Or(p,q) == Nand(Neg(p),Neg(q))"
+ "Or(p,q) \<equiv> Nand(Neg(p),Neg(q))"
definition
Implies :: "[i,i]=>i" where
- "Implies(p,q) == Nand(p,Neg(q))"
+ "Implies(p,q) \<equiv> Nand(p,Neg(q))"
definition
Iff :: "[i,i]=>i" where
- "Iff(p,q) == And(Implies(p,q), Implies(q,p))"
+ "Iff(p,q) \<equiv> And(Implies(p,q), Implies(q,p))"
definition
Exists :: "i=>i" where
- "Exists(p) == Neg(Forall(Neg(p)))"
+ "Exists(p) \<equiv> Neg(Forall(Neg(p)))"
-lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula"
+lemma Neg_type [TC]: "p \<in> formula \<Longrightarrow> Neg(p) \<in> formula"
by (simp add: Neg_def)
-lemma And_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> And(p,q) \<in> formula"
+lemma And_type [TC]: "\<lbrakk>p \<in> formula; q \<in> formula\<rbrakk> \<Longrightarrow> And(p,q) \<in> formula"
by (simp add: And_def)
-lemma Or_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> Or(p,q) \<in> formula"
+lemma Or_type [TC]: "\<lbrakk>p \<in> formula; q \<in> formula\<rbrakk> \<Longrightarrow> Or(p,q) \<in> formula"
by (simp add: Or_def)
lemma Implies_type [TC]:
- "[| p \<in> formula; q \<in> formula |] ==> Implies(p,q) \<in> formula"
+ "\<lbrakk>p \<in> formula; q \<in> formula\<rbrakk> \<Longrightarrow> Implies(p,q) \<in> formula"
by (simp add: Implies_def)
lemma Iff_type [TC]:
- "[| p \<in> formula; q \<in> formula |] ==> Iff(p,q) \<in> formula"
+ "\<lbrakk>p \<in> formula; q \<in> formula\<rbrakk> \<Longrightarrow> Iff(p,q) \<in> formula"
by (simp add: Iff_def)
-lemma Exists_type [TC]: "p \<in> formula ==> Exists(p) \<in> formula"
+lemma Exists_type [TC]: "p \<in> formula \<Longrightarrow> Exists(p) \<in> formula"
by (simp add: Exists_def)
@@ -85,7 +85,7 @@
abbreviation
sats :: "[i,i,i] => o" where
- "sats(A,p,env) == satisfies(A,p)`env = 1"
+ "sats(A,p,env) \<equiv> satisfies(A,p)`env = 1"
lemma sats_Member_iff [simp]:
"env \<in> list(A) \<Longrightarrow> sats(A, Member(x,y), env) \<longleftrightarrow> nth(x,env) \<in> nth(y,env)"
@@ -97,12 +97,12 @@
lemma sats_Nand_iff [simp]:
"env \<in> list(A)
- ==> (sats(A, Nand(p,q), env)) \<longleftrightarrow> ~ (sats(A,p,env) & sats(A,q,env))"
+ \<Longrightarrow> (sats(A, Nand(p,q), env)) \<longleftrightarrow> \<not> (sats(A,p,env) & sats(A,q,env))"
by (simp add: Bool.and_def Bool.not_def cond_def)
lemma sats_Forall_iff [simp]:
"env \<in> list(A)
- ==> sats(A, Forall(p), env) \<longleftrightarrow> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"
+ \<Longrightarrow> sats(A, Forall(p), env) \<longleftrightarrow> (\<forall>x\<in>A. sats(A, p, Cons(x,env)))"
by simp
declare satisfies.simps [simp del]
@@ -111,80 +111,80 @@
lemma sats_Neg_iff [simp]:
"env \<in> list(A)
- ==> sats(A, Neg(p), env) \<longleftrightarrow> ~ sats(A,p,env)"
+ \<Longrightarrow> sats(A, Neg(p), env) \<longleftrightarrow> \<not> sats(A,p,env)"
by (simp add: Neg_def)
lemma sats_And_iff [simp]:
"env \<in> list(A)
- ==> (sats(A, And(p,q), env)) \<longleftrightarrow> sats(A,p,env) & sats(A,q,env)"
+ \<Longrightarrow> (sats(A, And(p,q), env)) \<longleftrightarrow> sats(A,p,env) & sats(A,q,env)"
by (simp add: And_def)
lemma sats_Or_iff [simp]:
"env \<in> list(A)
- ==> (sats(A, Or(p,q), env)) \<longleftrightarrow> sats(A,p,env) | sats(A,q,env)"
+ \<Longrightarrow> (sats(A, Or(p,q), env)) \<longleftrightarrow> sats(A,p,env) | sats(A,q,env)"
by (simp add: Or_def)
lemma sats_Implies_iff [simp]:
"env \<in> list(A)
- ==> (sats(A, Implies(p,q), env)) \<longleftrightarrow> (sats(A,p,env) \<longrightarrow> sats(A,q,env))"
+ \<Longrightarrow> (sats(A, Implies(p,q), env)) \<longleftrightarrow> (sats(A,p,env) \<longrightarrow> sats(A,q,env))"
by (simp add: Implies_def, blast)
lemma sats_Iff_iff [simp]:
"env \<in> list(A)
- ==> (sats(A, Iff(p,q), env)) \<longleftrightarrow> (sats(A,p,env) \<longleftrightarrow> sats(A,q,env))"
+ \<Longrightarrow> (sats(A, Iff(p,q), env)) \<longleftrightarrow> (sats(A,p,env) \<longleftrightarrow> sats(A,q,env))"
by (simp add: Iff_def, blast)
lemma sats_Exists_iff [simp]:
"env \<in> list(A)
- ==> sats(A, Exists(p), env) \<longleftrightarrow> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))"
+ \<Longrightarrow> sats(A, Exists(p), env) \<longleftrightarrow> (\<exists>x\<in>A. sats(A, p, Cons(x,env)))"
by (simp add: Exists_def)
subsubsection\<open>Derived rules to help build up formulas\<close>
lemma mem_iff_sats:
- "[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
- ==> (x\<in>y) \<longleftrightarrow> sats(A, Member(i,j), env)"
+ "\<lbrakk>nth(i,env) = x; nth(j,env) = y; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> (x\<in>y) \<longleftrightarrow> sats(A, Member(i,j), env)"
by (simp add: satisfies.simps)
lemma equal_iff_sats:
- "[| nth(i,env) = x; nth(j,env) = y; env \<in> list(A)|]
- ==> (x=y) \<longleftrightarrow> sats(A, Equal(i,j), env)"
+ "\<lbrakk>nth(i,env) = x; nth(j,env) = y; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> (x=y) \<longleftrightarrow> sats(A, Equal(i,j), env)"
by (simp add: satisfies.simps)
lemma not_iff_sats:
- "[| P \<longleftrightarrow> sats(A,p,env); env \<in> list(A)|]
- ==> (~P) \<longleftrightarrow> sats(A, Neg(p), env)"
+ "\<lbrakk>P \<longleftrightarrow> sats(A,p,env); env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> (\<not>P) \<longleftrightarrow> sats(A, Neg(p), env)"
by simp
lemma conj_iff_sats:
- "[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
- ==> (P & Q) \<longleftrightarrow> sats(A, And(p,q), env)"
+ "\<lbrakk>P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> (P & Q) \<longleftrightarrow> sats(A, And(p,q), env)"
by (simp)
lemma disj_iff_sats:
- "[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
- ==> (P | Q) \<longleftrightarrow> sats(A, Or(p,q), env)"
+ "\<lbrakk>P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> (P | Q) \<longleftrightarrow> sats(A, Or(p,q), env)"
by (simp)
lemma iff_iff_sats:
- "[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
- ==> (P \<longleftrightarrow> Q) \<longleftrightarrow> sats(A, Iff(p,q), env)"
+ "\<lbrakk>P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> (P \<longleftrightarrow> Q) \<longleftrightarrow> sats(A, Iff(p,q), env)"
by (simp)
lemma imp_iff_sats:
- "[| P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)|]
- ==> (P \<longrightarrow> Q) \<longleftrightarrow> sats(A, Implies(p,q), env)"
+ "\<lbrakk>P \<longleftrightarrow> sats(A,p,env); Q \<longleftrightarrow> sats(A,q,env); env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> (P \<longrightarrow> Q) \<longleftrightarrow> sats(A, Implies(p,q), env)"
by (simp)
lemma ball_iff_sats:
- "[| !!x. x\<in>A ==> P(x) \<longleftrightarrow> sats(A, p, Cons(x, env)); env \<in> list(A)|]
- ==> (\<forall>x\<in>A. P(x)) \<longleftrightarrow> sats(A, Forall(p), env)"
+ "\<lbrakk>\<And>x. x\<in>A \<Longrightarrow> P(x) \<longleftrightarrow> sats(A, p, Cons(x, env)); env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> (\<forall>x\<in>A. P(x)) \<longleftrightarrow> sats(A, Forall(p), env)"
by (simp)
lemma bex_iff_sats:
- "[| !!x. x\<in>A ==> P(x) \<longleftrightarrow> sats(A, p, Cons(x, env)); env \<in> list(A)|]
- ==> (\<exists>x\<in>A. P(x)) \<longleftrightarrow> sats(A, Exists(p), env)"
+ "\<lbrakk>\<And>x. x\<in>A \<Longrightarrow> P(x) \<longleftrightarrow> sats(A, p, Cons(x, env)); env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> (\<exists>x\<in>A. P(x)) \<longleftrightarrow> sats(A, Exists(p), env)"
by (simp)
lemmas FOL_iff_sats =
@@ -206,7 +206,7 @@
"arity(Forall(p)) = Arith.pred(arity(p))"
-lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
+lemma arity_type [TC]: "p \<in> formula \<Longrightarrow> arity(p) \<in> nat"
by (induct_tac p, simp_all)
lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)"
@@ -229,8 +229,8 @@
lemma arity_sats_iff [rule_format]:
- "[| p \<in> formula; extra \<in> list(A) |]
- ==> \<forall>env \<in> list(A).
+ "\<lbrakk>p \<in> formula; extra \<in> list(A)\<rbrakk>
+ \<Longrightarrow> \<forall>env \<in> list(A).
arity(p) \<le> length(env) \<longrightarrow>
sats(A, p, env @ extra) \<longleftrightarrow> sats(A, p, env)"
apply (induct_tac p)
@@ -239,9 +239,9 @@
done
lemma arity_sats1_iff:
- "[| arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A);
- extra \<in> list(A) |]
- ==> sats(A, p, Cons(x, env @ extra)) \<longleftrightarrow> sats(A, p, Cons(x, env))"
+ "\<lbrakk>arity(p) \<le> succ(length(env)); p \<in> formula; x \<in> A; env \<in> list(A);
+ extra \<in> list(A)\<rbrakk>
+ \<Longrightarrow> sats(A, p, Cons(x, env @ extra)) \<longleftrightarrow> sats(A, p, Cons(x, env))"
apply (insert arity_sats_iff [of p extra A "Cons(x,env)"])
apply simp
done
@@ -251,12 +251,12 @@
definition
incr_var :: "[i,i]=>i" where
- "incr_var(x,nq) == if x<nq then x else succ(x)"
+ "incr_var(x,nq) \<equiv> if x<nq then x else succ(x)"
-lemma incr_var_lt: "x<nq ==> incr_var(x,nq) = x"
+lemma incr_var_lt: "x<nq \<Longrightarrow> incr_var(x,nq) = x"
by (simp add: incr_var_def)
-lemma incr_var_le: "nq\<le>x ==> incr_var(x,nq) = succ(x)"
+lemma incr_var_le: "nq\<le>x \<Longrightarrow> incr_var(x,nq) = succ(x)"
apply (simp add: incr_var_def)
apply (blast dest: lt_trans1)
done
@@ -276,10 +276,10 @@
(\<lambda>nq \<in> nat. Forall (incr_bv(p) ` succ(nq)))"
-lemma [TC]: "x \<in> nat ==> incr_var(x,nq) \<in> nat"
+lemma [TC]: "x \<in> nat \<Longrightarrow> incr_var(x,nq) \<in> nat"
by (simp add: incr_var_def)
-lemma incr_bv_type [TC]: "p \<in> formula ==> incr_bv(p) \<in> nat -> formula"
+lemma incr_bv_type [TC]: "p \<in> formula \<Longrightarrow> incr_bv(p) \<in> nat -> formula"
by (induct_tac p, simp_all)
text\<open>Obviously, \<^term>\<open>DPow\<close> is closed under complements and finite
@@ -287,8 +287,8 @@
parameters to be combined.\<close>
lemma sats_incr_bv_iff [rule_format]:
- "[| p \<in> formula; env \<in> list(A); x \<in> A |]
- ==> \<forall>bvs \<in> list(A).
+ "\<lbrakk>p \<in> formula; env \<in> list(A); x \<in> A\<rbrakk>
+ \<Longrightarrow> \<forall>bvs \<in> list(A).
sats(A, incr_bv(p) ` length(bvs), bvs @ Cons(x,env)) \<longleftrightarrow>
sats(A, p, bvs@env)"
apply (induct_tac p)
@@ -299,8 +299,8 @@
(*the following two lemmas prevent huge case splits in arity_incr_bv_lemma*)
lemma incr_var_lemma:
- "[| x \<in> nat; y \<in> nat; nq \<le> x |]
- ==> succ(x) \<union> incr_var(y,nq) = succ(x \<union> y)"
+ "\<lbrakk>x \<in> nat; y \<in> nat; nq \<le> x\<rbrakk>
+ \<Longrightarrow> succ(x) \<union> incr_var(y,nq) = succ(x \<union> y)"
apply (simp add: incr_var_def Ord_Un_if, auto)
apply (blast intro: leI)
apply (simp add: not_lt_iff_le)
@@ -309,14 +309,14 @@
done
lemma incr_And_lemma:
- "y < x ==> y \<union> succ(x) = succ(x \<union> y)"
+ "y < x \<Longrightarrow> y \<union> succ(x) = succ(x \<union> y)"
apply (simp add: Ord_Un_if lt_Ord lt_Ord2 succ_lt_iff)
apply (blast dest: lt_asym)
done
lemma arity_incr_bv_lemma [rule_format]:
"p \<in> formula
- ==> \<forall>n \<in> nat. arity (incr_bv(p) ` n) =
+ \<Longrightarrow> \<forall>n \<in> nat. arity (incr_bv(p) ` n) =
(if n < arity(p) then succ(arity(p)) else arity(p))"
apply (induct_tac p)
apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
@@ -340,24 +340,24 @@
definition
incr_bv1 :: "i => i" where
- "incr_bv1(p) == incr_bv(p)`1"
+ "incr_bv1(p) \<equiv> incr_bv(p)`1"
-lemma incr_bv1_type [TC]: "p \<in> formula ==> incr_bv1(p) \<in> formula"
+lemma incr_bv1_type [TC]: "p \<in> formula \<Longrightarrow> incr_bv1(p) \<in> formula"
by (simp add: incr_bv1_def)
(*For renaming all but the bound variable at level 0*)
lemma sats_incr_bv1_iff:
- "[| p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A |]
- ==> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) \<longleftrightarrow>
+ "\<lbrakk>p \<in> formula; env \<in> list(A); x \<in> A; y \<in> A\<rbrakk>
+ \<Longrightarrow> sats(A, incr_bv1(p), Cons(x, Cons(y, env))) \<longleftrightarrow>
sats(A, p, Cons(x,env))"
apply (insert sats_incr_bv_iff [of p env A y "Cons(x,Nil)"])
apply (simp add: incr_bv1_def)
done
lemma formula_add_params1 [rule_format]:
- "[| p \<in> formula; n \<in> nat; x \<in> A |]
- ==> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).
+ "\<lbrakk>p \<in> formula; n \<in> nat; x \<in> A\<rbrakk>
+ \<Longrightarrow> \<forall>bvs \<in> list(A). \<forall>env \<in> list(A).
length(bvs) = n \<longrightarrow>
sats(A, iterates(incr_bv1, n, p), Cons(x, bvs@env)) \<longleftrightarrow>
sats(A, p, Cons(x,env))"
@@ -369,15 +369,15 @@
lemma arity_incr_bv1_eq:
"p \<in> formula
- ==> arity(incr_bv1(p)) =
+ \<Longrightarrow> arity(incr_bv1(p)) =
(if 1 < arity(p) then succ(arity(p)) else arity(p))"
apply (insert arity_incr_bv_lemma [of p 1])
apply (simp add: incr_bv1_def)
done
lemma arity_iterates_incr_bv1_eq:
- "[| p \<in> formula; n \<in> nat |]
- ==> arity(incr_bv1^n(p)) =
+ "\<lbrakk>p \<in> formula; n \<in> nat\<rbrakk>
+ \<Longrightarrow> arity(incr_bv1^n(p)) =
(if 1 < arity(p) then n #+ arity(p) else arity(p))"
apply (induct_tac n)
apply (simp_all add: arity_incr_bv1_eq)
@@ -392,26 +392,26 @@
text\<open>The definable powerset operation: Kunen's definition VI 1.1, page 165.\<close>
definition
DPow :: "i => i" where
- "DPow(A) == {X \<in> Pow(A).
+ "DPow(A) \<equiv> {X \<in> Pow(A).
\<exists>env \<in> list(A). \<exists>p \<in> formula.
arity(p) \<le> succ(length(env)) &
X = {x\<in>A. sats(A, p, Cons(x,env))}}"
lemma DPowI:
- "[|env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))|]
- ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
+ "\<lbrakk>env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))\<rbrakk>
+ \<Longrightarrow> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
by (simp add: DPow_def, blast)
text\<open>With this rule we can specify \<^term>\<open>p\<close> later.\<close>
lemma DPowI2 [rule_format]:
- "[|\<forall>x\<in>A. P(x) \<longleftrightarrow> sats(A, p, Cons(x,env));
- env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))|]
- ==> {x\<in>A. P(x)} \<in> DPow(A)"
+ "\<lbrakk>\<forall>x\<in>A. P(x) \<longleftrightarrow> sats(A, p, Cons(x,env));
+ env \<in> list(A); p \<in> formula; arity(p) \<le> succ(length(env))\<rbrakk>
+ \<Longrightarrow> {x\<in>A. P(x)} \<in> DPow(A)"
by (simp add: DPow_def, blast)
lemma DPowD:
"X \<in> DPow(A)
- ==> X \<subseteq> A &
+ \<Longrightarrow> X \<subseteq> A &
(\<exists>env \<in> list(A).
\<exists>p \<in> formula. arity(p) \<le> succ(length(env)) &
X = {x\<in>A. sats(A, p, Cons(x,env))})"
@@ -420,8 +420,8 @@
lemmas DPow_imp_subset = DPowD [THEN conjunct1]
(*Kunen's Lemma VI 1.2*)
-lemma "[| p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env)) |]
- ==> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
+lemma "\<lbrakk>p \<in> formula; env \<in> list(A); arity(p) \<le> succ(length(env))\<rbrakk>
+ \<Longrightarrow> {x\<in>A. sats(A, p, Cons(x,env))} \<in> DPow(A)"
by (blast intro: DPowI)
lemma DPow_subset_Pow: "DPow(A) \<subseteq> Pow(A)"
@@ -434,14 +434,14 @@
apply (auto simp add: Un_least_lt_iff)
done
-lemma Compl_in_DPow: "X \<in> DPow(A) ==> (A-X) \<in> DPow(A)"
+lemma Compl_in_DPow: "X \<in> DPow(A) \<Longrightarrow> (A-X) \<in> DPow(A)"
apply (simp add: DPow_def, clarify, auto)
apply (rule bexI)
apply (rule_tac x="Neg(p)" in bexI)
apply auto
done
-lemma Int_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X \<inter> Y \<in> DPow(A)"
+lemma Int_in_DPow: "\<lbrakk>X \<in> DPow(A); Y \<in> DPow(A)\<rbrakk> \<Longrightarrow> X \<inter> Y \<in> DPow(A)"
apply (simp add: DPow_def, auto)
apply (rename_tac envp p envq q)
apply (rule_tac x="envp@envq" in bexI)
@@ -454,13 +454,13 @@
apply (simp add: arity_sats1_iff formula_add_params1, blast)
done
-lemma Un_in_DPow: "[| X \<in> DPow(A); Y \<in> DPow(A) |] ==> X \<union> Y \<in> DPow(A)"
+lemma Un_in_DPow: "\<lbrakk>X \<in> DPow(A); Y \<in> DPow(A)\<rbrakk> \<Longrightarrow> X \<union> Y \<in> DPow(A)"
apply (subgoal_tac "X \<union> Y = A - ((A-X) \<inter> (A-Y))")
apply (simp add: Int_in_DPow Compl_in_DPow)
apply (simp add: DPow_def, blast)
done
-lemma singleton_in_DPow: "a \<in> A ==> {a} \<in> DPow(A)"
+lemma singleton_in_DPow: "a \<in> A \<Longrightarrow> {a} \<in> DPow(A)"
apply (simp add: DPow_def)
apply (rule_tac x="Cons(a,Nil)" in bexI)
apply (rule_tac x="Equal(0,1)" in bexI)
@@ -468,13 +468,13 @@
apply (force simp add: succ_Un_distrib [symmetric])
done
-lemma cons_in_DPow: "[| a \<in> A; X \<in> DPow(A) |] ==> cons(a,X) \<in> DPow(A)"
+lemma cons_in_DPow: "\<lbrakk>a \<in> A; X \<in> DPow(A)\<rbrakk> \<Longrightarrow> cons(a,X) \<in> DPow(A)"
apply (rule cons_eq [THEN subst])
apply (blast intro: singleton_in_DPow Un_in_DPow)
done
(*Part of Lemma 1.3*)
-lemma Fin_into_DPow: "X \<in> Fin(A) ==> X \<in> DPow(A)"
+lemma Fin_into_DPow: "X \<in> Fin(A) \<Longrightarrow> X \<in> DPow(A)"
apply (erule Fin.induct)
apply (rule empty_in_DPow)
apply (blast intro: cons_in_DPow)
@@ -491,10 +491,10 @@
oops
*)
-lemma Finite_Pow_subset_Pow: "Finite(A) ==> Pow(A) \<subseteq> DPow(A)"
+lemma Finite_Pow_subset_Pow: "Finite(A) \<Longrightarrow> Pow(A) \<subseteq> DPow(A)"
by (blast intro: Fin_into_DPow Finite_into_Fin Fin_subset)
-lemma Finite_DPow_eq_Pow: "Finite(A) ==> DPow(A) = Pow(A)"
+lemma Finite_DPow_eq_Pow: "Finite(A) \<Longrightarrow> DPow(A) = Pow(A)"
apply (rule equalityI)
apply (rule DPow_subset_Pow)
apply (erule Finite_Pow_subset_Pow)
@@ -515,18 +515,18 @@
definition
subset_fm :: "[i,i]=>i" where
- "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
+ "subset_fm(x,y) \<equiv> Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
-lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
+lemma subset_type [TC]: "\<lbrakk>x \<in> nat; y \<in> nat\<rbrakk> \<Longrightarrow> subset_fm(x,y) \<in> formula"
by (simp add: subset_fm_def)
lemma arity_subset_fm [simp]:
- "[| x \<in> nat; y \<in> nat |] ==> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
+ "\<lbrakk>x \<in> nat; y \<in> nat\<rbrakk> \<Longrightarrow> arity(subset_fm(x,y)) = succ(x) \<union> succ(y)"
by (simp add: subset_fm_def succ_Un_distrib [symmetric])
lemma sats_subset_fm [simp]:
- "[|x < length(env); y \<in> nat; env \<in> list(A); Transset(A)|]
- ==> sats(A, subset_fm(x,y), env) \<longleftrightarrow> nth(x,env) \<subseteq> nth(y,env)"
+ "\<lbrakk>x < length(env); y \<in> nat; env \<in> list(A); Transset(A)\<rbrakk>
+ \<Longrightarrow> sats(A, subset_fm(x,y), env) \<longleftrightarrow> nth(x,env) \<subseteq> nth(y,env)"
apply (frule lt_length_in_nat, assumption)
apply (simp add: subset_fm_def Transset_def)
apply (blast intro: nth_type)
@@ -536,18 +536,18 @@
definition
transset_fm :: "i=>i" where
- "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
+ "transset_fm(x) \<equiv> Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
-lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
+lemma transset_type [TC]: "x \<in> nat \<Longrightarrow> transset_fm(x) \<in> formula"
by (simp add: transset_fm_def)
lemma arity_transset_fm [simp]:
- "x \<in> nat ==> arity(transset_fm(x)) = succ(x)"
+ "x \<in> nat \<Longrightarrow> arity(transset_fm(x)) = succ(x)"
by (simp add: transset_fm_def succ_Un_distrib [symmetric])
lemma sats_transset_fm [simp]:
- "[|x < length(env); env \<in> list(A); Transset(A)|]
- ==> sats(A, transset_fm(x), env) \<longleftrightarrow> Transset(nth(x,env))"
+ "\<lbrakk>x < length(env); env \<in> list(A); Transset(A)\<rbrakk>
+ \<Longrightarrow> sats(A, transset_fm(x), env) \<longleftrightarrow> Transset(nth(x,env))"
apply (frule lt_nat_in_nat, erule length_type)
apply (simp add: transset_fm_def Transset_def)
apply (blast intro: nth_type)
@@ -557,19 +557,19 @@
definition
ordinal_fm :: "i=>i" where
- "ordinal_fm(x) ==
+ "ordinal_fm(x) \<equiv>
And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
-lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
+lemma ordinal_type [TC]: "x \<in> nat \<Longrightarrow> ordinal_fm(x) \<in> formula"
by (simp add: ordinal_fm_def)
lemma arity_ordinal_fm [simp]:
- "x \<in> nat ==> arity(ordinal_fm(x)) = succ(x)"
+ "x \<in> nat \<Longrightarrow> arity(ordinal_fm(x)) = succ(x)"
by (simp add: ordinal_fm_def succ_Un_distrib [symmetric])
lemma sats_ordinal_fm:
- "[|x < length(env); env \<in> list(A); Transset(A)|]
- ==> sats(A, ordinal_fm(x), env) \<longleftrightarrow> Ord(nth(x,env))"
+ "\<lbrakk>x < length(env); env \<in> list(A); Transset(A)\<rbrakk>
+ \<Longrightarrow> sats(A, ordinal_fm(x), env) \<longleftrightarrow> Ord(nth(x,env))"
apply (frule lt_nat_in_nat, erule length_type)
apply (simp add: ordinal_fm_def Ord_def Transset_def)
apply (blast intro: nth_type)
@@ -577,7 +577,7 @@
text\<open>The subset consisting of the ordinals is definable. Essential lemma for
\<open>Ord_in_Lset\<close>. This result is the objective of the present subsection.\<close>
-theorem Ords_in_DPow: "Transset(A) ==> {x \<in> A. Ord(x)} \<in> DPow(A)"
+theorem Ords_in_DPow: "Transset(A) \<Longrightarrow> {x \<in> A. Ord(x)} \<in> DPow(A)"
apply (simp add: DPow_def Collect_subset)
apply (rule_tac x=Nil in bexI)
apply (rule_tac x="ordinal_fm(0)" in bexI)
@@ -589,40 +589,40 @@
definition
Lset :: "i=>i" where
- "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
+ "Lset(i) \<equiv> transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
definition
L :: "i=>o" where \<comment> \<open>Kunen's definition VI 1.5, page 167\<close>
- "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
+ "L(x) \<equiv> \<exists>i. Ord(i) & x \<in> Lset(i)"
text\<open>NOT SUITABLE FOR REWRITING -- RECURSIVE!\<close>
lemma Lset: "Lset(i) = (\<Union>j\<in>i. DPow(Lset(j)))"
by (subst Lset_def [THEN def_transrec], simp)
-lemma LsetI: "[|y\<in>x; A \<in> DPow(Lset(y))|] ==> A \<in> Lset(x)"
+lemma LsetI: "\<lbrakk>y\<in>x; A \<in> DPow(Lset(y))\<rbrakk> \<Longrightarrow> A \<in> Lset(x)"
by (subst Lset, blast)
-lemma LsetD: "A \<in> Lset(x) ==> \<exists>y\<in>x. A \<in> DPow(Lset(y))"
+lemma LsetD: "A \<in> Lset(x) \<Longrightarrow> \<exists>y\<in>x. A \<in> DPow(Lset(y))"
apply (insert Lset [of x])
apply (blast intro: elim: equalityE)
done
subsubsection\<open>Transitivity\<close>
-lemma elem_subset_in_DPow: "[|X \<in> A; X \<subseteq> A|] ==> X \<in> DPow(A)"
+lemma elem_subset_in_DPow: "\<lbrakk>X \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> X \<in> DPow(A)"
apply (simp add: Transset_def DPow_def)
apply (rule_tac x="[X]" in bexI)
apply (rule_tac x="Member(0,1)" in bexI)
apply (auto simp add: Un_least_lt_iff)
done
-lemma Transset_subset_DPow: "Transset(A) ==> A \<subseteq> DPow(A)"
+lemma Transset_subset_DPow: "Transset(A) \<Longrightarrow> A \<subseteq> DPow(A)"
apply clarify
apply (simp add: Transset_def)
apply (blast intro: elem_subset_in_DPow)
done
-lemma Transset_DPow: "Transset(A) ==> Transset(DPow(A))"
+lemma Transset_DPow: "Transset(A) \<Longrightarrow> Transset(DPow(A))"
apply (simp add: Transset_def)
apply (blast intro: elem_subset_in_DPow dest: DPowD)
done
@@ -634,7 +634,7 @@
apply (blast intro!: Transset_Union_family Transset_Un Transset_DPow)
done
-lemma mem_Lset_imp_subset_Lset: "a \<in> Lset(i) ==> a \<subseteq> Lset(i)"
+lemma mem_Lset_imp_subset_Lset: "a \<in> Lset(i) \<Longrightarrow> a \<subseteq> Lset(i)"
apply (insert Transset_Lset)
apply (simp add: Transset_def)
done
@@ -666,7 +666,7 @@
text\<open>Useful with Reflection to bump up the ordinal\<close>
-lemma subset_Lset_ltD: "[|A \<subseteq> Lset(i); i < j|] ==> A \<subseteq> Lset(j)"
+lemma subset_Lset_ltD: "\<lbrakk>A \<subseteq> Lset(i); i < j\<rbrakk> \<Longrightarrow> A \<subseteq> Lset(j)"
by (blast dest: ltD [THEN Lset_mono_mem])
subsubsection\<open>0, successor and limit equations for Lset\<close>
@@ -707,16 +707,16 @@
subsubsection\<open>Lset applied to Limit ordinals\<close>
lemma Limit_Lset_eq:
- "Limit(i) ==> Lset(i) = (\<Union>y\<in>i. Lset(y))"
+ "Limit(i) \<Longrightarrow> Lset(i) = (\<Union>y\<in>i. Lset(y))"
by (simp add: Lset_Union [symmetric] Limit_Union_eq)
-lemma lt_LsetI: "[| a \<in> Lset(j); j<i |] ==> a \<in> Lset(i)"
+lemma lt_LsetI: "\<lbrakk>a \<in> Lset(j); j<i\<rbrakk> \<Longrightarrow> a \<in> Lset(i)"
by (blast dest: Lset_mono [OF le_imp_subset [OF leI]])
lemma Limit_LsetE:
- "[| a \<in> Lset(i); ~R ==> Limit(i);
- !!x. [| x<i; a \<in> Lset(x) |] ==> R
- |] ==> R"
+ "\<lbrakk>a \<in> Lset(i); \<not>R \<Longrightarrow> Limit(i);
+ \<And>x. \<lbrakk>x<i; a \<in> Lset(x)\<rbrakk> \<Longrightarrow> R
+\<rbrakk> \<Longrightarrow> R"
apply (rule classical)
apply (rule Limit_Lset_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
prefer 2 apply assumption
@@ -726,7 +726,7 @@
subsubsection\<open>Basic closure properties\<close>
-lemma zero_in_Lset: "y \<in> x ==> 0 \<in> Lset(x)"
+lemma zero_in_Lset: "y \<in> x \<Longrightarrow> 0 \<in> Lset(x)"
by (subst Lset, blast intro: empty_in_DPow)
lemma notin_Lset: "x \<notin> Lset(x)"
@@ -738,7 +738,7 @@
subsection\<open>Constructible Ordinals: Kunen's VI 1.9 (b)\<close>
-lemma Ords_of_Lset_eq: "Ord(i) ==> {x\<in>Lset(i). Ord(x)} = i"
+lemma Ords_of_Lset_eq: "Ord(i) \<Longrightarrow> {x\<in>Lset(i). Ord(x)} = i"
apply (erule trans_induct3)
apply (simp_all add: Lset_succ Limit_Lset_eq Limit_Union_eq)
txt\<open>The successor case remains.\<close>
@@ -758,22 +758,22 @@
done
-lemma Ord_subset_Lset: "Ord(i) ==> i \<subseteq> Lset(i)"
+lemma Ord_subset_Lset: "Ord(i) \<Longrightarrow> i \<subseteq> Lset(i)"
by (subst Ords_of_Lset_eq [symmetric], assumption, fast)
-lemma Ord_in_Lset: "Ord(i) ==> i \<in> Lset(succ(i))"
+lemma Ord_in_Lset: "Ord(i) \<Longrightarrow> i \<in> Lset(succ(i))"
apply (simp add: Lset_succ)
apply (subst Ords_of_Lset_eq [symmetric], assumption,
rule Ords_in_DPow [OF Transset_Lset])
done
-lemma Ord_in_L: "Ord(i) ==> L(i)"
+lemma Ord_in_L: "Ord(i) \<Longrightarrow> L(i)"
by (simp add: L_def, blast intro: Ord_in_Lset)
subsubsection\<open>Unions\<close>
lemma Union_in_Lset:
- "X \<in> Lset(i) ==> \<Union>(X) \<in> Lset(succ(i))"
+ "X \<in> Lset(i) \<Longrightarrow> \<Union>(X) \<in> Lset(succ(i))"
apply (insert Transset_Lset)
apply (rule LsetI [OF succI1])
apply (simp add: Transset_def DPow_def)
@@ -785,20 +785,20 @@
apply (simp add: succ_Un_distrib [symmetric], blast)
done
-theorem Union_in_L: "L(X) ==> L(\<Union>(X))"
+theorem Union_in_L: "L(X) \<Longrightarrow> L(\<Union>(X))"
by (simp add: L_def, blast dest: Union_in_Lset)
subsubsection\<open>Finite sets and ordered pairs\<close>
-lemma singleton_in_Lset: "a \<in> Lset(i) ==> {a} \<in> Lset(succ(i))"
+lemma singleton_in_Lset: "a \<in> Lset(i) \<Longrightarrow> {a} \<in> Lset(succ(i))"
by (simp add: Lset_succ singleton_in_DPow)
lemma doubleton_in_Lset:
- "[| a \<in> Lset(i); b \<in> Lset(i) |] ==> {a,b} \<in> Lset(succ(i))"
+ "\<lbrakk>a \<in> Lset(i); b \<in> Lset(i)\<rbrakk> \<Longrightarrow> {a,b} \<in> Lset(succ(i))"
by (simp add: Lset_succ empty_in_DPow cons_in_DPow)
lemma Pair_in_Lset:
- "[| a \<in> Lset(i); b \<in> Lset(i); Ord(i) |] ==> <a,b> \<in> Lset(succ(succ(i)))"
+ "\<lbrakk>a \<in> Lset(i); b \<in> Lset(i); Ord(i)\<rbrakk> \<Longrightarrow> <a,b> \<in> Lset(succ(succ(i)))"
apply (unfold Pair_def)
apply (blast intro: doubleton_in_Lset)
done
@@ -808,21 +808,21 @@
text\<open>Hard work is finding a single \<^term>\<open>j \<in> i\<close> such that \<^term>\<open>{a,b} \<subseteq> Lset(j)\<close>\<close>
lemma doubleton_in_LLimit:
- "[| a \<in> Lset(i); b \<in> Lset(i); Limit(i) |] ==> {a,b} \<in> Lset(i)"
+ "\<lbrakk>a \<in> Lset(i); b \<in> Lset(i); Limit(i)\<rbrakk> \<Longrightarrow> {a,b} \<in> Lset(i)"
apply (erule Limit_LsetE, assumption)
apply (erule Limit_LsetE, assumption)
apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
done
-theorem doubleton_in_L: "[| L(a); L(b) |] ==> L({a, b})"
+theorem doubleton_in_L: "\<lbrakk>L(a); L(b)\<rbrakk> \<Longrightarrow> L({a, b})"
apply (simp add: L_def, clarify)
apply (drule Ord2_imp_greater_Limit, assumption)
apply (blast intro: lt_LsetI doubleton_in_LLimit Limit_is_Ord)
done
lemma Pair_in_LLimit:
- "[| a \<in> Lset(i); b \<in> Lset(i); Limit(i) |] ==> <a,b> \<in> Lset(i)"
+ "\<lbrakk>a \<in> Lset(i); b \<in> Lset(i); Limit(i)\<rbrakk> \<Longrightarrow> <a,b> \<in> Lset(i)"
txt\<open>Infer that a, b occur at ordinals x,xa < i.\<close>
apply (erule Limit_LsetE, assumption)
apply (erule Limit_LsetE, assumption)
@@ -836,18 +836,18 @@
text\<open>The rank function for the constructible universe\<close>
definition
lrank :: "i=>i" where \<comment> \<open>Kunen's definition VI 1.7\<close>
- "lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
+ "lrank(x) \<equiv> \<mu> i. x \<in> Lset(succ(i))"
-lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
+lemma L_I: "\<lbrakk>x \<in> Lset(i); Ord(i)\<rbrakk> \<Longrightarrow> L(x)"
by (simp add: L_def, blast)
-lemma L_D: "L(x) ==> \<exists>i. Ord(i) & x \<in> Lset(i)"
+lemma L_D: "L(x) \<Longrightarrow> \<exists>i. Ord(i) & x \<in> Lset(i)"
by (simp add: L_def)
lemma Ord_lrank [simp]: "Ord(lrank(a))"
by (simp add: lrank_def)
-lemma Lset_lrank_lt [rule_format]: "Ord(i) ==> x \<in> Lset(i) \<longrightarrow> lrank(x) < i"
+lemma Lset_lrank_lt [rule_format]: "Ord(i) \<Longrightarrow> x \<in> Lset(i) \<longrightarrow> lrank(x) < i"
apply (erule trans_induct3)
apply simp
apply (simp only: lrank_def)
@@ -859,7 +859,7 @@
text\<open>Kunen's VI 1.8. The proof is much harder than the text would
suggest. For a start, it needs the previous lemma, which is proved by
induction.\<close>
-lemma Lset_iff_lrank_lt: "Ord(i) ==> x \<in> Lset(i) \<longleftrightarrow> L(x) & lrank(x) < i"
+lemma Lset_iff_lrank_lt: "Ord(i) \<Longrightarrow> x \<in> Lset(i) \<longleftrightarrow> L(x) & lrank(x) < i"
apply (simp add: L_def, auto)
apply (blast intro: Lset_lrank_lt)
apply (unfold lrank_def)
@@ -872,7 +872,7 @@
by (simp add: Lset_iff_lrank_lt)
text\<open>Kunen's VI 1.9 (a)\<close>
-lemma lrank_of_Ord: "Ord(i) ==> lrank(i) = i"
+lemma lrank_of_Ord: "Ord(i) \<Longrightarrow> lrank(i) = i"
apply (unfold lrank_def)
apply (rule Least_equality)
apply (erule Ord_in_Lset)
@@ -893,7 +893,7 @@
apply auto
done
-lemma lrank_Lset: "Ord(i) ==> lrank(Lset(i)) = i"
+lemma lrank_Lset: "Ord(i) \<Longrightarrow> lrank(Lset(i)) = i"
apply (unfold lrank_def)
apply (rule Least_equality)
apply (rule Lset_in_Lset_succ)
@@ -905,7 +905,7 @@
done
text\<open>Kunen's VI 1.11\<close>
-lemma Lset_subset_Vset: "Ord(i) ==> Lset(i) \<subseteq> Vset(i)"
+lemma Lset_subset_Vset: "Ord(i) \<Longrightarrow> Lset(i) \<subseteq> Vset(i)"
apply (erule trans_induct)
apply (subst Lset)
apply (subst Vset)
@@ -915,7 +915,7 @@
done
text\<open>Kunen's VI 1.12\<close>
-lemma Lset_subset_Vset': "i \<in> nat ==> Lset(i) = Vset(i)"
+lemma Lset_subset_Vset': "i \<in> nat \<Longrightarrow> Lset(i) = Vset(i)"
apply (erule nat_induct)
apply (simp add: Vfrom_0)
apply (simp add: Lset_succ Vset_succ Finite_Vset Finite_DPow_eq_Pow)
@@ -923,24 +923,24 @@
text\<open>Every set of constructible sets is included in some \<^term>\<open>Lset\<close>\<close>
lemma subset_Lset:
- "(\<forall>x\<in>A. L(x)) ==> \<exists>i. Ord(i) & A \<subseteq> Lset(i)"
+ "(\<forall>x\<in>A. L(x)) \<Longrightarrow> \<exists>i. Ord(i) & A \<subseteq> Lset(i)"
by (rule_tac x = "\<Union>x\<in>A. succ(lrank(x))" in exI, force)
lemma subset_LsetE:
- "[|\<forall>x\<in>A. L(x);
- !!i. [|Ord(i); A \<subseteq> Lset(i)|] ==> P|]
- ==> P"
+ "\<lbrakk>\<forall>x\<in>A. L(x);
+ \<And>i. \<lbrakk>Ord(i); A \<subseteq> Lset(i)\<rbrakk> \<Longrightarrow> P\<rbrakk>
+ \<Longrightarrow> P"
by (blast dest: subset_Lset)
subsubsection\<open>For L to satisfy the Powerset axiom\<close>
lemma LPow_env_typing:
- "[| y \<in> Lset(i); Ord(i); y \<subseteq> X |]
- ==> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))"
+ "\<lbrakk>y \<in> Lset(i); Ord(i); y \<subseteq> X\<rbrakk>
+ \<Longrightarrow> \<exists>z \<in> Pow(X). y \<in> Lset(succ(lrank(z)))"
by (auto intro: L_I iff: Lset_succ_lrank_iff)
lemma LPow_in_Lset:
- "[|X \<in> Lset(i); Ord(i)|] ==> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)"
+ "\<lbrakk>X \<in> Lset(i); Ord(i)\<rbrakk> \<Longrightarrow> \<exists>j. Ord(j) & {y \<in> Pow(X). L(y)} \<in> Lset(j)"
apply (rule_tac x="succ(\<Union>y \<in> Pow(X). succ(lrank(y)))" in exI)
apply simp
apply (rule LsetI [OF succI1])
@@ -958,34 +958,34 @@
apply (auto intro: L_I iff: Lset_succ_lrank_iff)
done
-theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
+theorem LPow_in_L: "L(X) \<Longrightarrow> L({y \<in> Pow(X). L(y)})"
by (blast intro: L_I dest: L_D LPow_in_Lset)
subsection\<open>Eliminating \<^term>\<open>arity\<close> from the Definition of \<^term>\<open>Lset\<close>\<close>
-lemma nth_zero_eq_0: "n \<in> nat ==> nth(n,[0]) = 0"
+lemma nth_zero_eq_0: "n \<in> nat \<Longrightarrow> nth(n,[0]) = 0"
by (induct_tac n, auto)
lemma sats_app_0_iff [rule_format]:
- "[| p \<in> formula; 0 \<in> A |]
- ==> \<forall>env \<in> list(A). sats(A,p, env@[0]) \<longleftrightarrow> sats(A,p,env)"
+ "\<lbrakk>p \<in> formula; 0 \<in> A\<rbrakk>
+ \<Longrightarrow> \<forall>env \<in> list(A). sats(A,p, env@[0]) \<longleftrightarrow> sats(A,p,env)"
apply (induct_tac p)
apply (simp_all del: app_Cons add: app_Cons [symmetric]
add: nth_zero_eq_0 nth_append not_lt_iff_le nth_eq_0)
done
lemma sats_app_zeroes_iff:
- "[| p \<in> formula; 0 \<in> A; env \<in> list(A); n \<in> nat |]
- ==> sats(A,p,env @ repeat(0,n)) \<longleftrightarrow> sats(A,p,env)"
+ "\<lbrakk>p \<in> formula; 0 \<in> A; env \<in> list(A); n \<in> nat\<rbrakk>
+ \<Longrightarrow> sats(A,p,env @ repeat(0,n)) \<longleftrightarrow> sats(A,p,env)"
apply (induct_tac n, simp)
apply (simp del: repeat.simps
add: repeat_succ_app sats_app_0_iff app_assoc [symmetric])
done
lemma exists_bigger_env:
- "[| p \<in> formula; 0 \<in> A; env \<in> list(A) |]
- ==> \<exists>env' \<in> list(A). arity(p) \<le> succ(length(env')) &
+ "\<lbrakk>p \<in> formula; 0 \<in> A; env \<in> list(A)\<rbrakk>
+ \<Longrightarrow> \<exists>env' \<in> list(A). arity(p) \<le> succ(length(env')) &
(\<forall>a\<in>A. sats(A,p,Cons(a,env')) \<longleftrightarrow> sats(A,p,Cons(a,env)))"
apply (rule_tac x="env @ repeat(0,arity(p))" in bexI)
apply (simp del: app_Cons add: app_Cons [symmetric]
@@ -996,7 +996,7 @@
text\<open>A simpler version of \<^term>\<open>DPow\<close>: no arity check!\<close>
definition
DPow' :: "i => i" where
- "DPow'(A) == {X \<in> Pow(A).
+ "DPow'(A) \<equiv> {X \<in> Pow(A).
\<exists>env \<in> list(A). \<exists>p \<in> formula.
X = {x\<in>A. sats(A, p, Cons(x,env))}}"
@@ -1006,12 +1006,12 @@
lemma DPow'_0: "DPow'(0) = {0}"
by (auto simp add: DPow'_def)
-lemma DPow'_subset_DPow: "0 \<in> A ==> DPow'(A) \<subseteq> DPow(A)"
+lemma DPow'_subset_DPow: "0 \<in> A \<Longrightarrow> DPow'(A) \<subseteq> DPow(A)"
apply (auto simp add: DPow'_def DPow_def)
apply (frule exists_bigger_env, assumption+, force)
done
-lemma DPow_eq_DPow': "Transset(A) ==> DPow(A) = DPow'(A)"
+lemma DPow_eq_DPow': "Transset(A) \<Longrightarrow> DPow(A) = DPow'(A)"
apply (drule Transset_0_disj)
apply (erule disjE)
apply (simp add: DPow'_0 Finite_DPow_eq_Pow)
@@ -1032,9 +1032,9 @@
text\<open>With this rule we can specify \<^term>\<open>p\<close> later and don't worry about
arities at all!\<close>
lemma DPow_LsetI [rule_format]:
- "[|\<forall>x\<in>Lset(i). P(x) \<longleftrightarrow> sats(Lset(i), p, Cons(x,env));
- env \<in> list(Lset(i)); p \<in> formula|]
- ==> {x\<in>Lset(i). P(x)} \<in> DPow(Lset(i))"
+ "\<lbrakk>\<forall>x\<in>Lset(i). P(x) \<longleftrightarrow> sats(Lset(i), p, Cons(x,env));
+ env \<in> list(Lset(i)); p \<in> formula\<rbrakk>
+ \<Longrightarrow> {x\<in>Lset(i). P(x)} \<in> DPow(Lset(i))"
by (simp add: DPow_eq_DPow' [OF Transset_Lset] DPow'_def, blast)
end