--- a/src/ZF/AC.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/AC.thy Tue Jul 02 13:28:08 2002 +0200
@@ -23,27 +23,22 @@
(*Using dtac, this has the advantage of DELETING the universal quantifier*)
lemma AC_ball_Pi: "\<forall>x \<in> A. \<exists>y. y \<in> B(x) ==> \<exists>y. y \<in> Pi(A,B)"
apply (rule AC_Pi)
-apply (erule bspec)
-apply assumption
+apply (erule bspec, assumption)
done
lemma AC_Pi_Pow: "\<exists>f. f \<in> (\<Pi>X \<in> Pow(C)-{0}. X)"
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
-apply (erule_tac [2] exI)
-apply blast
+apply (erule_tac [2] exI, blast)
done
lemma AC_func:
"[| !!x. x \<in> A ==> (\<exists>y. y \<in> x) |] ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
apply (rule_tac B1 = "%x. x" in AC_Pi [THEN exE])
-prefer 2 apply (blast dest: apply_type intro: Pi_type)
-apply (blast intro: elim:);
+prefer 2 apply (blast dest: apply_type intro: Pi_type, blast)
done
lemma non_empty_family: "[| 0 \<notin> A; x \<in> A |] ==> \<exists>y. y \<in> x"
-apply (subgoal_tac "x \<noteq> 0")
-apply blast+
-done
+by (subgoal_tac "x \<noteq> 0", blast+)
lemma AC_func0: "0 \<notin> A ==> \<exists>f \<in> A->Union(A). \<forall>x \<in> A. f`x \<in> x"
apply (rule AC_func)
@@ -53,9 +48,8 @@
lemma AC_func_Pow: "\<exists>f \<in> (Pow(C)-{0}) -> C. \<forall>x \<in> Pow(C)-{0}. f`x \<in> x"
apply (rule AC_func0 [THEN bexE])
apply (rule_tac [2] bexI)
-prefer 2 apply (assumption)
-apply (erule_tac [2] fun_weaken_type)
-apply blast+
+prefer 2 apply assumption
+apply (erule_tac [2] fun_weaken_type, blast+)
done
lemma AC_Pi0: "0 \<notin> A ==> \<exists>f. f \<in> (\<Pi>x \<in> A. x)"
--- a/src/ZF/Bool.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Bool.thy Tue Jul 02 13:28:08 2002 +0200
@@ -72,7 +72,7 @@
by (simp add: bool_defs )
lemma cond_type [TC]: "[| b: bool; c: A(1); d: A(0) |] ==> cond(b,c,d): A(b)"
-by (simp add: bool_defs , blast)
+by (simp add: bool_defs, blast)
(*For Simp_tac and Blast_tac*)
lemma cond_simple_type: "[| b: bool; c: A; d: A |] ==> cond(b,c,d): A"
@@ -137,7 +137,7 @@
(a or b) and c = (a and c) or (b and c)"
by (elim boolE, auto)
-(** binary orion **)
+(** binary 'or' **)
lemma or_absorb [simp]: "a: bool ==> a or a = a"
by (elim boolE, auto)
@@ -152,6 +152,25 @@
(a and b) or c = (a or c) and (b or c)"
by (elim boolE, auto)
+
+constdefs bool_of_o :: "o=>i"
+ "bool_of_o(P) == (if P then 1 else 0)"
+
+lemma [simp]: "bool_of_o(True) = 1"
+by (simp add: bool_of_o_def)
+
+lemma [simp]: "bool_of_o(False) = 0"
+by (simp add: bool_of_o_def)
+
+lemma [simp,TC]: "bool_of_o(P) \<in> bool"
+by (simp add: bool_of_o_def)
+
+lemma [simp]: "(bool_of_o(P) = 1) <-> P"
+by (simp add: bool_of_o_def)
+
+lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
+by (simp add: bool_of_o_def)
+
ML
{*
val bool_def = thm "bool_def";
--- a/src/ZF/Cardinal.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Cardinal.thy Tue Jul 02 13:28:08 2002 +0200
@@ -432,8 +432,7 @@
by (blast intro: Card_lt_imp_lt Ord_cardinal_le [THEN lt_trans1])
lemma Card_le_iff: "[| Ord(i); Card(K) |] ==> (K le |i|) <-> (K le i)"
-apply (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
-done
+by (simp add: Card_lt_iff Card_is_Ord Ord_cardinal not_lt_iff_le [THEN iff_sym])
(*Can use AC or finiteness to discharge first premise*)
lemma well_ord_lepoll_imp_Card_le:
@@ -805,10 +804,10 @@
apply (erule Finite_cons)
done
-lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
+lemma Finite_cons_iff [iff]: "Finite(cons(y,x)) <-> Finite(x)"
by (blast intro: Finite_cons subset_Finite)
-lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
+lemma Finite_succ_iff [iff]: "Finite(succ(x)) <-> Finite(x)"
by (simp add: succ_def)
lemma nat_le_infinite_Ord:
--- a/src/ZF/CardinalArith.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/CardinalArith.thy Tue Jul 02 13:28:08 2002 +0200
@@ -467,7 +467,7 @@
(*A general fact about ordermap*)
lemma ordermap_eqpoll_pred:
- "[| well_ord(A,r); x:A |] ==> ordermap(A,r)`x \<approx> pred(A,x,r)"
+ "[| well_ord(A,r); x:A |] ==> ordermap(A,r)`x \<approx> Order.pred(A,x,r)"
apply (unfold eqpoll_def)
apply (rule exI)
apply (simp add: ordermap_eq_image well_ord_is_wf)
@@ -503,7 +503,7 @@
done
lemma pred_csquare_subset:
- "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"
+ "z<K ==> Order.pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)"
apply (unfold Order.pred_def)
apply (safe del: SigmaI succCI)
apply (erule csquareD [THEN conjE])
--- a/src/ZF/Cardinal_AC.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Cardinal_AC.thy Tue Jul 02 13:28:08 2002 +0200
@@ -22,13 +22,11 @@
lemma cardinal_eqE: "|X| = |Y| ==> X eqpoll Y"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
-apply (rule well_ord_cardinal_eqE)
-apply assumption+
+apply (rule well_ord_cardinal_eqE, assumption+)
done
lemma cardinal_eqpoll_iff: "|X| = |Y| <-> X eqpoll Y"
-apply (blast intro: cardinal_cong cardinal_eqE)
-done
+by (blast intro: cardinal_cong cardinal_eqE)
lemma cardinal_disjoint_Un: "[| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==>
|A Un C| = |B Un D|"
@@ -37,38 +35,33 @@
lemma lepoll_imp_Card_le: "A lepoll B ==> |A| le |B|"
apply (rule AC_well_ord [THEN exE])
-apply (erule well_ord_lepoll_imp_Card_le)
-apply assumption
+apply (erule well_ord_lepoll_imp_Card_le, assumption)
done
lemma cadd_assoc: "(i |+| j) |+| k = i |+| (j |+| k)"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
-apply (rule well_ord_cadd_assoc)
-apply assumption+
+apply (rule well_ord_cadd_assoc, assumption+)
done
lemma cmult_assoc: "(i |*| j) |*| k = i |*| (j |*| k)"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
-apply (rule well_ord_cmult_assoc)
-apply assumption+
+apply (rule well_ord_cmult_assoc, assumption+)
done
lemma cadd_cmult_distrib: "(i |+| j) |*| k = (i |*| k) |+| (j |*| k)"
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
apply (rule AC_well_ord [THEN exE])
-apply (rule well_ord_cadd_cmult_distrib)
-apply assumption+
+apply (rule well_ord_cadd_cmult_distrib, assumption+)
done
lemma InfCard_square_eq: "InfCard(|A|) ==> A*A eqpoll A"
apply (rule AC_well_ord [THEN exE])
-apply (erule well_ord_InfCard_square_eq)
-apply assumption
+apply (erule well_ord_InfCard_square_eq, assumption)
done
@@ -83,7 +76,7 @@
lemma le_Card_iff: "Card(K) ==> |A| le K <-> A lepoll K"
apply (erule Card_cardinal_eq [THEN subst], rule iffI,
- erule Card_le_imp_lepoll);
+ erule Card_le_imp_lepoll)
apply (erule lepoll_imp_Card_le)
done
@@ -119,12 +112,10 @@
prefer 2
apply (fast intro!: Least_le [THEN lt_trans1, THEN ltD] ltI
elim!: LeastI Ord_in_Ord)
-apply (rule_tac c = "%z. <LEAST i. z:X (i) , f ` (LEAST i. z:X (i)) ` z>"
+apply (rule_tac c = "%z. <LEAST i. z:X (i), f ` (LEAST i. z:X (i)) ` z>"
and d = "%<i,j>. converse (f`i) ` j" in lam_injective)
(*Instantiate the lemma proved above*)
-apply (blast intro: inj_is_fun [THEN apply_type] dest: apply_type)
-apply (force );
-done
+by (blast intro: inj_is_fun [THEN apply_type] dest: apply_type, force)
(*The same again, using csucc*)
@@ -139,8 +130,7 @@
lemma cardinal_UN_Ord_lt_csucc:
"[| InfCard(K); ALL i:K. j(i) < csucc(K) |]
==> (UN i:K. j(i)) < csucc(K)"
-apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt])
-apply assumption
+apply (rule cardinal_UN_lt_csucc [THEN Card_lt_imp_lt], assumption)
apply (blast intro: Ord_cardinal_le [THEN lt_trans1] elim: ltE)
apply (blast intro!: Ord_UN elim: ltE)
apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN Card_csucc])
@@ -172,9 +162,8 @@
Card_is_Ord Ord_0_lt_csucc)
apply (simp add: InfCard_is_Card le_Card_iff lepoll_def)
apply (safe intro!: equalityI)
-apply (erule swap);
-apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc])
-apply assumption+
+apply (erule swap)
+apply (rule lt_subset_trans [OF inj_UN_subset cardinal_UN_Ord_lt_csucc], assumption+)
apply (simp add: inj_converse_fun [THEN apply_type])
apply (blast intro!: Ord_UN elim: ltE)
done
--- a/src/ZF/Constructible/Datatype_absolute.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy Tue Jul 02 13:28:08 2002 +0200
@@ -1,28 +1,4 @@
-theory Datatype_absolute = WF_absolute:
-
-(*Epsilon.thy*)
-lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
-apply (insert arg_subset_eclose [of "{i}"], simp)
-apply (frule eclose_subset, blast)
-done
-
-lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
-apply (rule equalityI)
-apply (erule eclose_sing_Ord)
-apply (rule succ_subset_eclose_sing)
-done
-
-(*Ordinal.thy*)
-lemma relation_Memrel: "relation(Memrel(A))"
-by (simp add: relation_def Memrel_def, blast)
-
-lemma (in M_axioms) nat_case_closed:
- "[|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)")
-apply force
-apply (simp add: nat_case_def)
-done
+theory Datatype_absolute = Formula + WF_absolute:
subsection{*The lfp of a continuous function can be expressed as a union*}
@@ -143,13 +119,16 @@
wf_Memrel trans_Memrel relation_Memrel nat_case_closed)
+
locale M_datatypes = M_wfrank +
(*THEY NEED RELATIVIZATION*)
assumes list_replacement1:
"[|M(A); n \<in> nat|] ==>
strong_replacement(M,
- \<lambda>x z. \<exists>y[M]. \<exists>g[M]. pair(M, x, y, z) &
- is_recfun (Memrel(succ(n)), x,
+ \<lambda>x z. \<exists>y[M]. \<exists>g[M]. \<exists>sucn[M]. \<exists>memr[M].
+ pair(M,x,y,z) & successor(M,n,sucn) &
+ membership(M,sucn,memr) &
+ is_recfun (memr, x,
\<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
y = nat_case(0, \<lambda>m. {0} + A \<times> g`m, x))"
and list_replacement2':
@@ -159,11 +138,11 @@
lemma (in M_datatypes) list_replacement1':
"[|M(A); n \<in> nat|]
==> strong_replacement
- (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x, z\<rangle> &
+ (M, \<lambda>x y. \<exists>z[M]. \<exists>g[M]. y = \<langle>x,z\<rangle> &
is_recfun (Memrel(succ(n)), x,
- \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f ` m, n), g) &
+ \<lambda>n f. nat_case(0, \<lambda>m. {0} + A \<times> f`m, n), g) &
z = nat_case(0, \<lambda>m. {0} + A \<times> g ` m, x))"
-by (insert list_replacement1, simp)
+by (insert list_replacement1, simp add: nat_into_M)
lemma (in M_datatypes) list_closed [intro,simp]:
--- a/src/ZF/Constructible/Formula.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy Tue Jul 02 13:28:08 2002 +0200
@@ -2,48 +2,6 @@
theory Formula = Main:
-
-(*??for Bool.thy**)
-constdefs bool_of_o :: "o=>i"
- "bool_of_o(P) == (if P then 1 else 0)"
-
-lemma [simp]: "bool_of_o(True) = 1"
-by (simp add: bool_of_o_def)
-
-lemma [simp]: "bool_of_o(False) = 0"
-by (simp add: bool_of_o_def)
-
-lemma [simp,TC]: "bool_of_o(P) \<in> bool"
-by (simp add: bool_of_o_def)
-
-lemma [simp]: "(bool_of_o(P) = 1) <-> P"
-by (simp add: bool_of_o_def)
-
-lemma [simp]: "(bool_of_o(P) = 0) <-> ~P"
-by (simp add: bool_of_o_def)
-
-(*????????????????CardinalArith *)
-
-lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
-apply (erule nat_induct)
- apply (simp add: Vfrom_0)
-apply (simp add: Vset_succ)
-done
-
-(*???Ordinal maybe, but some lemmas seem to be in CardinalArith??*)
-text{*Every ordinal is exceeded by some limit ordinal.*}
-lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
-apply (rule_tac x="i ++ nat" in exI)
-apply (blast intro: oadd_LimitI oadd_lt_self Limit_nat [THEN Limit_has_0])
-done
-
-lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
-apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])
-apply (simp add: Un_least_lt_iff)
-done
-
-
-
(*Internalized formulas of FOL. De Bruijn representation.
Unbound variables get their denotations from an environment.*)
@@ -250,7 +208,7 @@
"arity(And(p,q)) = arity(p) \<union> arity(q)"
- "arity(Forall(p)) = nat_case3(0, %x. x, arity(p))"
+ "arity(Forall(p)) = nat_case(0, %x. x, arity(p))"
lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
@@ -262,7 +220,7 @@
lemma arity_Implies [simp]: "arity(Implies(p,q)) = arity(p) \<union> arity(q)"
by (simp add: Implies_def)
-lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case3(0, %x. x, arity(p))"
+lemma arity_Exists [simp]: "arity(Exists(p)) = nat_case(0, %x. x, arity(p))"
by (simp add: Exists_def)
@@ -272,8 +230,8 @@
arity(p) \<le> length(env) -->
sats(A, p, env @ extra) <-> sats(A, p, env)"
apply (induct_tac p)
-apply (simp_all add: nth_append Un_least_lt_iff arity_type
- split: split_nat_case3, auto)
+apply (simp_all add: nth_append Un_least_lt_iff arity_type nat_imp_quasinat
+ split: split_nat_case, auto)
done
lemma arity_sats1_iff:
@@ -308,14 +266,18 @@
apply (induct_tac p)
apply (simp_all add: imp_disj not_lt_iff_le Un_least_lt_iff lt_Un_iff le_Un_iff
succ_Un_distrib [symmetric] incr_var_lt incr_var_le
- Un_commute incr_var_lemma arity_type
- split: split_nat_case3)
-(*left with the And case*)
+ Un_commute incr_var_lemma arity_type nat_imp_quasinat
+ split: split_nat_case)
+ txt{*the Forall case reduces to linear arithmetic*}
+ prefer 2
+ apply clarify
+ apply (blast dest: lt_trans1)
+txt{*left with the And case*}
apply safe
apply (blast intro: incr_And_lemma lt_trans1)
apply (subst incr_And_lemma)
- apply (blast intro: lt_trans1)
-apply (simp add: Un_commute)
+ apply (blast intro: lt_trans1)
+apply (simp add: Un_commute)
done
lemma arity_incr_boundvars_eq:
@@ -774,8 +736,8 @@
"[| a: Lset(i); b: Lset(i); Limit(i) |] ==> {a,b} : 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)
+apply (blast intro: lt_LsetI [OF doubleton_in_Lset]
+ Lset_UnI1 Lset_UnI2 Limit_has_succ Un_least_lt)
done
lemma Pair_in_LLimit:
--- a/src/ZF/Constructible/L_axioms.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy Tue Jul 02 13:28:08 2002 +0200
@@ -1,6 +1,6 @@
header {* The class L satisfies the axioms of ZF*}
-theory L_axioms = Formula + Relative:
+theory L_axioms = Formula + Relative + Reflection:
text {* The class L satisfies the premises of locale @{text M_axioms} *}
@@ -72,57 +72,57 @@
(*
and Inter_separation:
- "L(A) ==> separation(M, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
+ "L(A) ==> separation(L, \<lambda>x. \<forall>y\<in>A. L(y) --> x\<in>y)"
and cartprod_separation:
"[| L(A); L(B) |]
- ==> separation(M, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(M,x,y,z))"
+ ==> separation(L, \<lambda>z. \<exists>x\<in>A. \<exists>y\<in>B. L(x) & L(y) & pair(L,x,y,z))"
and image_separation:
"[| L(A); L(r) |]
- ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(M,x,y,p)))"
+ ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & (\<exists>x\<in>A. L(x) & pair(L,x,y,p)))"
and vimage_separation:
"[| L(A); L(r) |]
- ==> separation(M, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(M,x,y,p)))"
+ ==> separation(L, \<lambda>x. \<exists>p\<in>r. L(p) & (\<exists>y\<in>A. L(x) & pair(L,x,y,p)))"
and converse_separation:
- "L(r) ==> separation(M, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) &
- pair(M,x,y,p) & pair(M,y,x,z)))"
+ "L(r) ==> separation(L, \<lambda>z. \<exists>p\<in>r. L(p) & (\<exists>x y. L(x) & L(y) &
+ pair(L,x,y,p) & pair(L,y,x,z)))"
and restrict_separation:
"L(A)
- ==> separation(M, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(M,x,y,z)))"
+ ==> separation(L, \<lambda>z. \<exists>x\<in>A. L(x) & (\<exists>y. L(y) & pair(L,x,y,z)))"
and comp_separation:
"[| L(r); L(s) |]
- ==> separation(M, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
+ ==> separation(L, \<lambda>xz. \<exists>x y z. L(x) & L(y) & L(z) &
(\<exists>xy\<in>s. \<exists>yz\<in>r. L(xy) & L(yz) &
- pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz)))"
+ pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz)))"
and pred_separation:
- "[| L(r); L(x) |] ==> separation(M, \<lambda>y. \<exists>p\<in>r. L(p) & pair(M,y,x,p))"
+ "[| L(r); L(x) |] ==> separation(L, \<lambda>y. \<exists>p\<in>r. L(p) & pair(L,y,x,p))"
and Memrel_separation:
- "separation(M, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(M,x,y,z) \<and> x \<in> y)"
+ "separation(L, \<lambda>z. \<exists>x y. L(x) & L(y) & pair(L,x,y,z) \<and> x \<in> y)"
and obase_separation:
--{*part of the order type formalization*}
"[| L(A); L(r) |]
- ==> separation(M, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
- ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
- order_isomorphism(M,par,r,x,mx,g))"
+ ==> separation(L, \<lambda>a. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
+ ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) &
+ order_isomorphism(L,par,r,x,mx,g))"
and well_ord_iso_separation:
"[| L(A); L(f); L(r) |]
- ==> separation (M, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and>
- fun_apply(M,f,x,y) \<and> pair(M,y,x,p) \<and> p \<in> r)))"
+ ==> separation (L, \<lambda>x. x\<in>A --> (\<exists>y. L(y) \<and> (\<exists>p. L(p) \<and>
+ fun_apply(L,f,x,y) \<and> pair(L,y,x,p) \<and> p \<in> r)))"
and obase_equals_separation:
"[| L(A); L(r) |]
==> separation
- (M, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
- ordinal(M,y) & (\<exists>my pxr. L(my) & L(pxr) &
- membership(M,y,my) & pred_set(M,A,x,r,pxr) &
- order_isomorphism(M,pxr,r,y,my,g)))))"
+ (L, \<lambda>x. x\<in>A --> ~(\<exists>y. L(y) & (\<exists>g. L(g) &
+ ordinal(L,y) & (\<exists>my pxr. L(my) & L(pxr) &
+ membership(L,y,my) & pred_set(L,A,x,r,pxr) &
+ order_isomorphism(L,pxr,r,y,my,g)))))"
and is_recfun_separation:
--{*for well-founded recursion. NEEDS RELATIVIZATION*}
"[| L(A); L(f); L(g); L(a); L(b) |]
- ==> separation(M, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
+ ==> separation(L, \<lambda>x. x \<in> A --> \<langle>x,a\<rangle> \<in> r \<and> \<langle>x,b\<rangle> \<in> r \<and> f`x \<noteq> g`x)"
and omap_replacement:
"[| L(A); L(r) |]
- ==> strong_replacement(M,
+ ==> strong_replacement(L,
\<lambda>a z. \<exists>x g mx par. L(x) & L(g) & L(mx) & L(par) &
- ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) &
- pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))"
+ ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) &
+ pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))"
*)
\ No newline at end of file
--- a/src/ZF/Constructible/Relative.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy Tue Jul 02 13:28:08 2002 +0200
@@ -2,11 +2,6 @@
theory Relative = Main:
-(*func.thy*)
-lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
-by (simp add: succ_def mem_not_refl cons_fun_eq)
-
-
subsection{* Relativized versions of standard set-theoretic concepts *}
constdefs
@@ -899,6 +894,13 @@
"n \<in> nat ==> M(n)"
by (induct n rule: nat_induct, simp_all)
+lemma (in M_axioms) nat_case_closed:
+ "[|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)
+apply (simp add: nat_case_def)
+done
+
lemma (in M_axioms) Inl_in_M_iff [iff]:
"M(Inl(a)) <-> M(a)"
by (simp add: Inl_def)
--- a/src/ZF/Constructible/WF_absolute.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy Tue Jul 02 13:28:08 2002 +0200
@@ -1,20 +1,5 @@
theory WF_absolute = WFrec:
-(*????move to Wellorderings.thy*)
-lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
- "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
-by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
-
-lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
- "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
-by (blast intro: wellfounded_imp_wellfounded_on
- wellfounded_on_field_imp_wellfounded)
-
-lemma (in M_axioms) wellfounded_on_subset_A:
- "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)"
-by (simp add: wellfounded_on_def, blast)
-
-
subsection{*Every well-founded relation is a subset of some inverse image of
an ordinal*}
--- a/src/ZF/Constructible/WFrec.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/WFrec.thy Tue Jul 02 13:28:08 2002 +0200
@@ -3,14 +3,11 @@
(*Many of these might be useful in WF.thy*)
-lemma is_recfunI:
- "f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))) ==> is_recfun(r,a,H,f)"
-by (simp add: is_recfun_def)
-
-lemma is_recfun_imp_function: "is_recfun(r,a,H,f) ==> function(f)"
-apply (simp add: is_recfun_def)
-apply (erule ssubst)
-apply (rule function_lam)
+lemma apply_recfun2:
+ "[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))"
+apply (frule apply_recfun)
+ apply (blast dest: is_recfun_type fun_is_rel)
+apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
done
text{*Expresses @{text is_recfun} as a recursion equation*}
@@ -28,14 +25,7 @@
done
lemma is_recfun_imp_in_r: "[|is_recfun(r,a,H,f); \<langle>x,i\<rangle> \<in> f|] ==> \<langle>x, a\<rangle> \<in> r"
-by (blast dest: is_recfun_type fun_is_rel)
-
-lemma apply_recfun2:
- "[| is_recfun(r,a,H,f); <x,i>:f |] ==> i = H(x, restrict(f,r-``{x}))"
-apply (frule apply_recfun)
- apply (blast dest: is_recfun_type fun_is_rel)
-apply (simp add: function_apply_equality [OF _ is_recfun_imp_function])
-done
+by (blast dest: is_recfun_type fun_is_rel)
lemma trans_Int_eq:
"[| trans(r); <y,x> \<in> r |] ==> r -`` {x} \<inter> r -`` {y} = r -`` {y}"
@@ -153,7 +143,7 @@
apply (blast intro!: function_restrictI dest!: pair_components_in_M)
apply (blast intro!: function_restrictI dest!: pair_components_in_M)
apply (simp only: subset_iff domain_iff restrict_iff vimage_iff)
-apply (simp add: vimage_singleton_iff)
+apply (simp add: vimage_singleton_iff)
apply (intro allI impI conjI)
apply (blast intro: transM dest!: pair_components_in_M)
prefer 4;apply blast
--- a/src/ZF/Constructible/Wellorderings.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Constructible/Wellorderings.thy Tue Jul 02 13:28:08 2002 +0200
@@ -71,6 +71,10 @@
"[| wellfounded(M,r); M(A) |] ==> wellfounded_on(M,A,r)"
by (auto simp add: wellfounded_def wellfounded_on_def)
+lemma (in M_axioms) wellfounded_on_subset_A:
+ "[| wellfounded_on(M,A,r); B<=A |] ==> wellfounded_on(M,B,r)"
+by (simp add: wellfounded_on_def, blast)
+
subsubsection {*Well-founded relations*}
@@ -85,6 +89,15 @@
"[|wellfounded_on(M,A,r); r \<subseteq> A*A|] ==> wellfounded(M,r)"
by (simp add: wellfounded_on_iff_wellfounded subset_Int_iff)
+lemma (in M_axioms) wellfounded_on_field_imp_wellfounded:
+ "wellfounded_on(M, field(r), r) ==> wellfounded(M,r)"
+by (simp add: wellfounded_def wellfounded_on_iff_wellfounded, fast)
+
+lemma (in M_axioms) wellfounded_iff_wellfounded_on_field:
+ "M(r) ==> wellfounded(M,r) <-> wellfounded_on(M, field(r), r)"
+by (blast intro: wellfounded_imp_wellfounded_on
+ wellfounded_on_field_imp_wellfounded)
+
(*Consider the least z in domain(r) such that P(z) does not hold...*)
lemma (in M_axioms) wellfounded_induct:
"[| wellfounded(M,r); M(a); M(r); separation(M, \<lambda>x. ~P(x));
--- a/src/ZF/Epsilon.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Epsilon.thy Tue Jul 02 13:28:08 2002 +0200
@@ -181,6 +181,17 @@
apply (rule succI1 [THEN singleton_subsetI])
done
+lemma succ_subset_eclose_sing: "succ(i) <= eclose({i})"
+apply (insert arg_subset_eclose [of "{i}"], simp)
+apply (frule eclose_subset, blast)
+done
+
+lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
+apply (rule equalityI)
+apply (erule eclose_sing_Ord)
+apply (rule succ_subset_eclose_sing)
+done
+
lemma Ord_transrec_type:
assumes jini: "j: i"
and ordi: "Ord(i)"
@@ -291,8 +302,8 @@
r = {<0,0>,<0,1>,<0,2>,...}. Then f`0 = Union(f``{0}) = Union(nat) = nat,
whose rank equals that of r.*)
lemma rank_apply: "[|i : domain(f); function(f)|] ==> rank(f`i) < rank(f)"
-apply (clarify );
-apply (simp add: function_apply_equality);
+apply clarify
+apply (simp add: function_apply_equality)
apply (blast intro: lt_trans rank_lt rank_pair2)
done
@@ -332,7 +343,7 @@
lemma transrec2_Limit:
"Limit(i) ==> transrec2(i,a,b) = (UN j<i. transrec2(j,a,b))"
apply (rule transrec2_def [THEN def_transrec, THEN trans])
-apply (auto simp add: OUnion_def);
+apply (auto simp add: OUnion_def)
done
lemma def_transrec2:
--- a/src/ZF/Finite.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Finite.thy Tue Jul 02 13:28:08 2002 +0200
@@ -151,9 +151,7 @@
done
lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)"
-apply (erule FiniteFun.induct, simp)
-apply simp
-done
+by (erule FiniteFun.induct, simp, simp)
lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard]
@@ -175,8 +173,7 @@
lemma fun_FiniteFunI [rule_format]: "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B"
apply (erule Fin.induct)
- apply (simp add: FiniteFun.intros)
-apply clarify
+ apply (simp add: FiniteFun.intros, clarify)
apply (case_tac "a:b")
apply (rotate_tac -1)
apply (simp add: cons_absorb)
--- a/src/ZF/InfDatatype.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/InfDatatype.thy Tue Jul 02 13:28:08 2002 +0200
@@ -17,8 +17,7 @@
apply (rule_tac x = "UN d:D. LEAST i. f`d : Vfrom (A,i) " in exI)
apply (rule conjI)
apply (rule_tac [2] le_UN_Ord_lt_csucc)
-apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE)
-apply (simp_all add: )
+apply (rule_tac [4] ballI, erule_tac [4] fun_Limit_VfromE, simp_all)
prefer 2 apply (fast elim: Least_le [THEN lt_trans1] ltE)
apply (rule Pi_type)
apply (rename_tac [2] d)
@@ -44,7 +43,7 @@
(*This level includes the function, and is below csucc(K)*)
apply (rule_tac a1 = "succ (succ (j Un ja))" in UN_I [THEN UnI2])
apply (blast intro: ltD InfCard_csucc InfCard_is_Limit Limit_has_succ
- Un_least_lt);
+ Un_least_lt)
apply (erule subset_trans [THEN PowI])
apply (fast intro: Pair_in_Vfrom Vfrom_UnI1 Vfrom_UnI2)
done
--- a/src/ZF/Nat.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Nat.thy Tue Jul 02 13:28:08 2002 +0200
@@ -12,15 +12,13 @@
nat :: i
"nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
+ quasinat :: "i => o"
+ "quasinat(n) == n=0 | (\<exists>m. n = succ(m))"
+
(*Has an unconditional succ case, which is used in "recursor" below.*)
nat_case :: "[i, i=>i, i]=>i"
"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
- (*Slightly different from the version above. Requires k to be a
- natural number, but it has a splitting rule.*)
- nat_case3 :: "[i, i=>i, i]=>i"
- "nat_case3(a,b,k) == THE y. k=0 & y=a | (EX x:nat. k=succ(x) & y=b(x))"
-
nat_rec :: "[i, i, [i,i]=>i]=>i"
"nat_rec(k,a,b) ==
wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
@@ -47,8 +45,7 @@
lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"
apply (rule bnd_monoI)
-apply (cut_tac infinity, blast)
-apply blast
+apply (cut_tac infinity, blast, blast)
done
(* nat = {0} Un {succ(x). x:nat} *)
@@ -135,8 +132,7 @@
lemma lt_nat_in_nat: "[| m<n; n: nat |] ==> m: nat"
apply (erule ltE)
-apply (erule Ord_trans, assumption)
-apply simp
+apply (erule Ord_trans, assumption, simp)
done
lemma le_in_nat: "[| m le n; n:nat |] ==> m:nat"
@@ -205,6 +201,34 @@
==> P(m,n)"
by (blast intro: succ_lt_induct_lemma lt_nat_in_nat)
+subsection{*quasinat: to allow a case-split rule for @{term nat_case}*}
+
+text{*True if the argument is zero or any successor*}
+lemma [iff]: "quasinat(0)"
+by (simp add: quasinat_def)
+
+lemma [iff]: "quasinat(succ(x))"
+by (simp add: quasinat_def)
+
+lemma nat_imp_quasinat: "n \<in> nat ==> quasinat(n)"
+by (erule natE, simp_all)
+
+lemma non_nat_case: "~ quasinat(x) ==> nat_case(a,b,x) = 0"
+by (simp add: quasinat_def nat_case_def)
+
+lemma nat_cases_disj: "k=0 | (\<exists>y. k = succ(y)) | ~ quasinat(k)"
+txt{*The @{text case_tac} method is not yet available.*}
+apply (rule_tac P = "k=0" in case_split_thm, simp)
+apply (rule_tac P = "\<exists>m. k = succ(m)" in case_split_thm, simp)
+apply simp
+apply (simp add: quasinat_def)
+done
+
+lemma nat_cases:
+ "[|k=0 ==> P; !!y. k = succ(y) ==> P; ~ quasinat(k) ==> P|] ==> P"
+apply (insert nat_cases_disj [of k], blast)
+done
+
(** nat_case **)
lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
@@ -218,32 +242,13 @@
==> nat_case(a,b,n) : C(n)";
by (erule nat_induct, auto)
-(** nat_case3 **)
-
-lemma nat_case3_0 [simp]: "nat_case3(a,b,0) = a"
-by (simp add: nat_case3_def)
-
-lemma nat_case3_succ [simp]: "n\<in>nat \<Longrightarrow> nat_case3(a,b,succ(n)) = b(n)"
-by (simp add: nat_case3_def)
-
-lemma non_nat_case3: "x\<notin>nat \<Longrightarrow> nat_case3(a,b,x) = 0"
-apply (simp add: nat_case3_def)
-apply (blast intro: the_0)
+lemma split_nat_case:
+ "P(nat_case(a,b,k)) <->
+ ((k=0 --> P(a)) & (\<forall>x. k=succ(x) --> P(b(x))) & (~ quasinat(k) \<longrightarrow> P(0)))"
+apply (rule nat_cases [of k])
+apply (auto simp add: non_nat_case)
done
-lemma split_nat_case3:
- "P(nat_case3(a,b,k)) <->
- ((k=0 --> P(a)) & (\<forall>x\<in>nat. k=succ(x) --> P(b(x))) & (k \<notin> nat \<longrightarrow> P(0)))"
-apply (rule_tac P="k\<in>nat" in case_split_thm)
- (*case_tac method not available yet; needs "inductive"*)
-apply (erule natE)
-apply (auto simp add: non_nat_case3)
-done
-
-lemma nat_case3_type [TC]:
- "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |]
- ==> nat_case3(a,b,n) : C(n)";
-by (erule nat_induct, auto)
(** nat_rec -- used to define eclose and transrec, then obsolete
--- a/src/ZF/OrderArith.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/OrderArith.thy Tue Jul 02 13:28:08 2002 +0200
@@ -38,26 +38,22 @@
lemma radd_Inl_Inr_iff [iff]:
"<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B"
-apply (unfold radd_def)
-apply blast
+apply (unfold radd_def, blast)
done
lemma radd_Inl_iff [iff]:
"<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> a':A & a:A & <a',a>:r"
-apply (unfold radd_def)
-apply blast
+apply (unfold radd_def, blast)
done
lemma radd_Inr_iff [iff]:
"<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s"
-apply (unfold radd_def)
-apply blast
+apply (unfold radd_def, blast)
done
lemma radd_Inr_Inl_iff [iff]:
"<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"
-apply (unfold radd_def)
-apply blast
+apply (unfold radd_def, blast)
done
(** Elimination Rule **)
@@ -68,8 +64,7 @@
!!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q;
!!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q
|] ==> Q"
-apply (unfold radd_def)
-apply (blast intro: elim:);
+apply (unfold radd_def, blast)
done
(** Type checking **)
@@ -85,8 +80,7 @@
lemma linear_radd:
"[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
-apply (unfold linear_def)
-apply (blast intro: elim:);
+apply (unfold linear_def, blast)
done
@@ -100,12 +94,11 @@
apply (erule_tac V = "y : A + B" in thin_rl)
apply (rule_tac ballI)
apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
- apply (blast intro: elim:);
+ apply blast
(*Returning to main part of proof*)
apply safe
apply blast
-apply (erule_tac r = "s" and a = "ya" in wf_on_induct , assumption)
-apply (blast intro: elim:);
+apply (erule_tac r = "s" and a = "ya" in wf_on_induct, assumption, blast)
done
lemma wf_radd: "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))"
@@ -126,7 +119,7 @@
lemma sum_bij:
"[| f: bij(A,C); g: bij(B,D) |]
==> (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)"
-apply (rule_tac d = "case (%x. Inl (converse (f) `x) , %y. Inr (converse (g) `y))" in lam_bijective)
+apply (rule_tac d = "case (%x. Inl (converse (f) `x), %y. Inr (converse (g) `y))" in lam_bijective)
apply (typecheck add: bij_is_inj inj_is_fun)
apply (auto simp add: left_inverse_bij right_inverse_bij)
done
@@ -163,8 +156,7 @@
"(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))
: ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),
A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"
-apply (rule sum_assoc_bij [THEN ord_isoI])
-apply auto
+apply (rule sum_assoc_bij [THEN ord_isoI], auto)
done
@@ -177,8 +169,7 @@
(<a',a>: r & a':A & a:A & b': B & b: B) |
(<b',b>: s & a'=a & a:A & b': B & b: B)"
-apply (unfold rmult_def)
-apply blast
+apply (unfold rmult_def, blast)
done
lemma rmultE:
@@ -186,7 +177,7 @@
[| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q;
[| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q
|] ==> Q"
-apply (blast intro: elim:);
+apply blast
done
(** Type checking **)
@@ -202,8 +193,7 @@
lemma linear_rmult:
"[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
-apply (simp add: linear_def);
-apply (blast intro: elim:);
+apply (simp add: linear_def, blast)
done
(** Well-foundedness **)
@@ -212,11 +202,10 @@
apply (rule wf_onI2)
apply (erule SigmaE)
apply (erule ssubst)
-apply (subgoal_tac "ALL b:B. <x,b>: Ba")
-apply blast
-apply (erule_tac a = "x" in wf_on_induct , assumption)
+apply (subgoal_tac "ALL b:B. <x,b>: Ba", blast)
+apply (erule_tac a = "x" in wf_on_induct, assumption)
apply (rule ballI)
-apply (erule_tac a = "b" in wf_on_induct , assumption)
+apply (erule_tac a = "b" in wf_on_induct, assumption)
apply (best elim!: rmultE bspec [THEN mp])
done
@@ -257,9 +246,7 @@
done
lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)"
-apply (rule_tac d = "snd" in lam_bijective)
-apply auto
-done
+by (rule_tac d = "snd" in lam_bijective, auto)
(*Used??*)
lemma singleton_prod_ord_iso:
@@ -279,8 +266,7 @@
apply (rule subst_elem)
apply (rule id_bij [THEN sum_bij, THEN comp_bij])
apply (rule singleton_prod_bij)
-apply (rule sum_disjoint_bij)
-apply blast
+apply (rule sum_disjoint_bij, blast)
apply (simp (no_asm_simp) cong add: case_cong)
apply (rule comp_lam [THEN trans, symmetric])
apply (fast elim!: case_type)
@@ -303,7 +289,7 @@
lemma sum_prod_distrib_bij:
"(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
: bij((A+B)*C, (A*C)+(B*C))"
-apply (rule_tac d = "case (%<x,y>.<Inl (x) ,y>, %<x,y>.<Inr (x) ,y>) "
+apply (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) "
in lam_bijective)
apply auto
done
@@ -312,24 +298,21 @@
"(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))
: ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t),
(A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
-apply (rule sum_prod_distrib_bij [THEN ord_isoI])
-apply auto
+apply (rule sum_prod_distrib_bij [THEN ord_isoI], auto)
done
(** Associativity **)
lemma prod_assoc_bij:
"(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"
-apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective)
-apply auto
+apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto)
done
lemma prod_assoc_ord_iso:
"(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)
: ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),
A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"
-apply (rule prod_assoc_bij [THEN ord_isoI])
-apply auto
+apply (rule prod_assoc_bij [THEN ord_isoI], auto)
done
(**** Inverse image of a relation ****)
@@ -337,9 +320,7 @@
(** Rewrite rule **)
lemma rvimage_iff: "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A"
-apply (unfold rvimage_def)
-apply blast
-done
+by (unfold rvimage_def, blast)
(** Type checking **)
@@ -351,9 +332,7 @@
lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
lemma rvimage_converse: "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))"
-apply (unfold rvimage_def)
-apply blast
-done
+by (unfold rvimage_def, blast)
(** Partial Ordering Properties **)
@@ -381,7 +360,7 @@
lemma linear_rvimage:
"[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))"
apply (simp add: inj_def linear_def rvimage_iff)
-apply (blast intro: apply_funtype);
+apply (blast intro: apply_funtype)
done
lemma tot_ord_rvimage:
@@ -400,9 +379,9 @@
apply (subgoal_tac "EX w. w : {w: {f`x. x:Q}. EX x. x: Q & (f`x = w) }")
apply (erule allE)
apply (erule impE)
- apply assumption;
+ apply assumption
apply blast
-apply (blast intro: elim:);
+apply blast
done
lemma wf_on_rvimage: "[| f: A->B; wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
@@ -431,8 +410,7 @@
lemma ord_iso_rvimage_eq:
"f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"
-apply (unfold ord_iso_def rvimage_def)
-apply blast
+apply (unfold ord_iso_def rvimage_def, blast)
done
@@ -441,8 +419,7 @@
lemma measure_eq_rvimage_Memrel:
"measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))"
apply (simp (no_asm) add: measure_def rvimage_def Memrel_iff)
-apply (rule equalityI)
-apply auto
+apply (rule equalityI, auto)
apply (auto intro: Ord_in_Ord simp add: lt_def)
done
--- a/src/ZF/OrderType.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/OrderType.thy Tue Jul 02 13:28:08 2002 +0200
@@ -11,7 +11,7 @@
But a definition by transfinite recursion would be much simpler!
*)
-theory OrderType = OrderArith + OrdQuant:
+theory OrderType = OrderArith + OrdQuant + Nat:
constdefs
@@ -52,7 +52,7 @@
"op **" :: "[i,i] => i" (infixl "\<times>\<times>" 70)
-(**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
+subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*}
lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"
apply (rule well_ordI)
@@ -99,7 +99,7 @@
done
-(**** Ordermap and ordertype ****)
+subsection{*Ordermap and ordertype*}
lemma ordermap_type:
"ordermap(A,r) : A -> ordertype(A,r)"
@@ -310,7 +310,7 @@
done
-(**** Alternative definition of ordinal ****)
+subsection{*Alternative definition of ordinal*}
(*proof by Krzysztof Grabczewski*)
lemma Ord_is_Ord_alt: "Ord(i) ==> Ord_alt(i)"
@@ -330,7 +330,7 @@
done
-(**** Ordinal Addition ****)
+subsection{*Ordinal Addition*}
(*** Order Type calculations for radd ***)
@@ -666,6 +666,17 @@
apply (blast intro: succ_leI oadd_le_mono)
done
+text{*Every ordinal is exceeded by some limit ordinal.*}
+lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
+apply (rule_tac x="i ++ nat" in exI)
+apply (blast intro: oadd_LimitI oadd_lt_self Limit_nat [THEN Limit_has_0])
+done
+
+lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
+apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])
+apply (simp add: Un_least_lt_iff)
+done
+
(** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)).
Probably simpler to define the difference recursively!
@@ -733,7 +744,7 @@
done
-(**** Ordinal Multiplication ****)
+subsection{*Ordinal Multiplication*}
lemma Ord_omult [simp,TC]:
"[| Ord(i); Ord(j) |] ==> Ord(i**j)"
--- a/src/ZF/Ordinal.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Ordinal.thy Tue Jul 02 13:28:08 2002 +0200
@@ -290,6 +290,9 @@
lemma Memrel_1 [simp]: "Memrel(1) = 0"
by (unfold Memrel_def, blast)
+lemma relation_Memrel: "relation(Memrel(A))"
+by (simp add: relation_def Memrel_def, blast)
+
(*The membership relation (as a set) is well-founded.
Proof idea: show A<=B by applying the foundation axiom to A-B *)
lemma wf_Memrel: "wf(Memrel(A))"
@@ -316,8 +319,7 @@
!!x.[| x: k; ALL y:x. P(y) |] ==> P(x) |]
==> P(i)"
apply (simp add: Transset_def)
-apply (erule wf_Memrel [THEN wf_induct2], blast)
-apply blast
+apply (erule wf_Memrel [THEN wf_induct2], blast+)
done
(*Induction over an ordinal*)
@@ -404,8 +406,7 @@
by (blast intro: Ord_0_le elim: ltE)
lemma subset_imp_le: "[| j<=i; Ord(i); Ord(j) |] ==> j le i"
-apply (rule not_lt_iff_le [THEN iffD1], assumption)
-apply assumption
+apply (rule not_lt_iff_le [THEN iffD1], assumption+)
apply (blast elim: ltE mem_irrefl)
done
--- a/src/ZF/Perm.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Perm.thy Tue Jul 02 13:28:08 2002 +0200
@@ -380,8 +380,7 @@
"[| (f O g): inj(A,C); g: surj(A,B); f: B->C |] ==> f: inj(B,C)"
apply (unfold inj_def surj_def, safe)
apply (rule_tac x1 = "x" in bspec [THEN bexE])
-apply (erule_tac [3] x1 = "w" in bspec [THEN bexE], assumption+)
-apply safe
+apply (erule_tac [3] x1 = "w" in bspec [THEN bexE], assumption+, safe)
apply (rule_tac t = "op ` (g) " in subst_context)
apply (erule asm_rl bspec [THEN bspec, THEN mp])+
apply (simp (no_asm_simp))
@@ -518,8 +517,7 @@
lemma inj_succ_restrict:
"[| f: inj(succ(m), A) |] ==> restrict(f,m) : inj(m, A-{f`m})"
-apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption)
-apply blast
+apply (rule restrict_bij [THEN bij_is_inj, THEN inj_weaken_type], assumption, blast)
apply (unfold inj_def)
apply (fast elim: range_type mem_irrefl dest: apply_equality)
done
--- a/src/ZF/Trancl.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Trancl.thy Tue Jul 02 13:28:08 2002 +0200
@@ -124,8 +124,7 @@
(*Closure under composition with r *)
lemma rtrancl_into_rtrancl: "[| <a,b> : r^*; <b,c> : r |] ==> <a,c> : r^*"
apply (rule rtrancl_unfold [THEN ssubst])
-apply (rule compI [THEN UnI2], assumption)
-apply assumption
+apply (rule compI [THEN UnI2], assumption, assumption)
done
(*rtrancl of r contains all pairs in r *)
@@ -301,8 +300,7 @@
lemma rtrancl_subset: "[| R <= S; S <= R^* |] ==> S^* = R^*"
apply (drule rtrancl_mono)
-apply (drule rtrancl_mono, simp_all)
-apply blast
+apply (drule rtrancl_mono, simp_all, blast)
done
lemma rtrancl_Un_rtrancl:
--- a/src/ZF/Univ.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Univ.thy Tue Jul 02 13:28:08 2002 +0200
@@ -11,7 +11,7 @@
But Ind_Syntax.univ refers to the constant "Univ.univ"
*)
-theory Univ = Epsilon + Sum + Finite + mono:
+theory Univ = Epsilon + Cardinal:
constdefs
Vfrom :: "[i,i]=>i"
@@ -37,9 +37,7 @@
text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
-apply (subst Vfrom_def [THEN def_transrec])
-apply simp
-done
+by (subst Vfrom_def [THEN def_transrec], simp)
subsubsection{* Monotonicity *}
@@ -450,6 +448,12 @@
Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
done
+lemma Finite_Vset: "i \<in> nat ==> Finite(Vset(i))";
+apply (erule nat_induct)
+ apply (simp add: Vfrom_0)
+apply (simp add: Vset_succ)
+done
+
subsubsection{* Reasoning about sets in terms of their elements' ranks *}
lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
@@ -483,8 +487,7 @@
text{*NOT SUITABLE FOR REWRITING: recursive!*}
lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
apply (unfold Vrec_def)
-apply (subst transrec)
-apply simp
+apply (subst transrec, simp)
apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
done
--- a/src/ZF/Update.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Update.thy Tue Jul 02 13:28:08 2002 +0200
@@ -39,8 +39,7 @@
apply (unfold update_def)
apply (simp add: domain_of_fun cons_absorb)
apply (rule fun_extension)
-apply (best intro: apply_type if_type lam_type, assumption)
-apply simp
+apply (best intro: apply_type if_type lam_type, assumption, simp)
done
--- a/src/ZF/WF.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/WF.thy Tue Jul 02 13:28:08 2002 +0200
@@ -165,20 +165,17 @@
lemmas wf_asym = wf_not_sym [THEN swap, standard]
lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r"
-apply (erule_tac a=a in wf_on_induct, assumption)
-apply blast
-done
+by (erule_tac a=a in wf_on_induct, assumption, blast)
lemma wf_on_not_sym [rule_format]:
"[| wf[A](r); a:A |] ==> ALL b:A. <a,b>:r --> <b,a>~:r"
-apply (erule_tac a=a in wf_on_induct, assumption)
-apply blast
+apply (erule_tac a=a in wf_on_induct, assumption, blast)
done
lemma wf_on_asym:
"[| wf[A](r); ~Z ==> <a,b> : r;
<b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z"
-by (blast dest: wf_on_not_sym);
+by (blast dest: wf_on_not_sym)
(*Needed to prove well_ordI. Could also reason that wf[A](r) means
@@ -187,8 +184,7 @@
"[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P"
apply (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P",
blast)
-apply (erule_tac a=a in wf_on_induct, assumption)
-apply blast
+apply (erule_tac a=a in wf_on_induct, assumption, blast)
done
@@ -226,12 +222,14 @@
apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
done
+lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function]
+
lemma apply_recfun:
"[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
apply (unfold is_recfun_def)
txt{*replace f only on the left-hand side*}
apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
-apply (simp add: underI);
+apply (simp add: underI)
done
lemma is_recfun_equal [rule_format]:
@@ -311,7 +309,7 @@
lemma the_recfun_cut:
"[| wf(r); trans(r); <b,a>:r |]
==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
-by (blast intro: is_recfun_cut unfold_the_recfun);
+by (blast intro: is_recfun_cut unfold_the_recfun)
(*NOT SUITABLE FOR REWRITING: it is recursive!*)
lemma wftrec:
--- a/src/ZF/Zorn.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/Zorn.thy Tue Jul 02 13:28:08 2002 +0200
@@ -55,12 +55,10 @@
(*** Section 1. Mathematical Preamble ***)
lemma Union_lemma0: "(ALL x:C. x<=A | B<=x) ==> Union(C)<=A | B<=Union(C)"
-apply blast
-done
+by blast
lemma Inter_lemma0: "[| c:C; ALL x:C. A<=x | x<=B |] ==> A<=Inter(C) | Inter(C)<=B"
-apply blast
-done
+by blast
(*** Section 2. The Transfinite Construction ***)
@@ -71,9 +69,7 @@
done
lemma increasingD2: "[| f: increasing(A); x<=A |] ==> x <= f`x"
-apply (unfold increasing_def)
-apply (blast intro: elim:);
-done
+by (unfold increasing_def, blast)
lemmas TFin_UnionI = PowI [THEN TFin.Pow_UnionI, standard]
@@ -87,8 +83,7 @@
!!x. [| x : TFin(S,next); P(x); next: increasing(S) |] ==> P(next`x);
!!Y. [| Y <= TFin(S,next); ALL y:Y. P(y) |] ==> P(Union(Y))
|] ==> P(n)"
-apply (erule TFin.induct)
-apply blast+
+apply (erule TFin.induct, blast+)
done
@@ -119,19 +114,17 @@
apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
assumption+)
apply (blast del: subsetI
- intro: increasing_trans subsetI)
-apply (blast intro: elim:);
+ intro: increasing_trans subsetI, blast)
(*second induction step*)
apply (rule impI [THEN ballI])
apply (rule Union_lemma0 [THEN disjE])
apply (erule_tac [3] disjI2)
-prefer 2 apply (blast intro: elim:);
+prefer 2 apply blast
apply (rule ballI)
apply (drule bspec, assumption)
apply (drule subsetD, assumption)
apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
- assumption+)
-apply (blast intro: elim:);
+ assumption+, blast)
apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
apply (blast dest: TFin_is_subset)+
done
@@ -159,9 +152,8 @@
"[| n: TFin(S,next); m: TFin(S,next); m = next`m |] ==> n<=m"
apply (erule TFin_induct)
apply (drule TFin_subsetD)
-apply (assumption+)
-apply (force );
-apply (blast)
+apply (assumption+, force)
+apply blast
done
(*Property 3.3 of section 3.3*)
@@ -172,7 +164,7 @@
apply (rule_tac [2] equal_next_upper [THEN Union_least])
apply (assumption+)
apply (erule ssubst)
-apply (rule increasingD2 [THEN equalityI] , assumption)
+apply (rule increasingD2 [THEN equalityI], assumption)
apply (blast del: subsetI
intro: subsetI TFin_UnionI TFin.nextI TFin_is_subset)+
done
@@ -202,8 +194,7 @@
X : chain(S); X ~: maxchain(S) |]
==> ch ` super(S,X) : super(S,X)"
apply (erule apply_type)
-apply (unfold super_def maxchain_def)
-apply blast
+apply (unfold super_def maxchain_def, blast)
done
lemma choice_not_equals:
@@ -211,8 +202,7 @@
X : chain(S); X ~: maxchain(S) |]
==> ch ` super(S,X) ~= X"
apply (rule notI)
-apply (drule choice_super)
-apply assumption
+apply (drule choice_super, assumption)
apply assumption
apply (simp add: super_def)
done
@@ -225,7 +215,7 @@
apply (rule_tac x="\<lambda>X\<in>Pow(S).
if X \<in> chain(S) - maxchain(S) then ch ` super(S, X) else X"
in bexI)
-apply (force );
+apply force
apply (unfold increasing_def)
apply (rule CollectI)
apply (rule lam_type)
@@ -236,8 +226,7 @@
apply safe
apply (drule choice_super)
apply (assumption+)
-apply (simp add: super_def)
-apply blast
+apply (simp add: super_def, blast)
done
(*Lemma 4*)
@@ -252,16 +241,13 @@
apply (simp (no_asm_simp) add: chain_subset_Pow [THEN subsetD, THEN PowD]
choice_super [THEN super_subset_chain [THEN subsetD]])
apply (unfold chain_def)
-apply (rule CollectI , blast)
-apply safe
-apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE])
-apply fast+ (*Blast_tac's slow*)
+apply (rule CollectI, blast, safe)
+apply (rule_tac m1 = "B" and n1 = "Ba" in TFin_subset_linear [THEN disjE], fast+) (*Blast_tac's slow*)
done
lemma Hausdorff: "EX c. c : maxchain(S)"
apply (rule AC_Pi_Pow [THEN exE])
-apply (rule Hausdorff_next_exists [THEN bexE])
-apply assumption
+apply (rule Hausdorff_next_exists [THEN bexE], assumption)
apply (rename_tac ch "next")
apply (subgoal_tac "Union (TFin (S,next)) : chain (S) ")
prefer 2
@@ -271,7 +257,7 @@
apply (subgoal_tac "next ` Union (TFin (S,next)) = Union (TFin (S,next))")
apply (rule_tac [2] equal_next_Union [THEN iffD2, symmetric])
apply (rule_tac [2] subset_refl [THEN TFin_UnionI])
-prefer 2 apply (assumption)
+prefer 2 apply assumption
apply (rule_tac [2] refl)
apply (simp add: subset_refl [THEN TFin_UnionI,
THEN TFin.dom_subset [THEN subsetD, THEN PowD]])
@@ -286,8 +272,7 @@
(*Used in the proof of Zorn's Lemma*)
lemma chain_extend:
"[| c: chain(A); z: A; ALL x:c. x<=z |] ==> cons(z,c) : chain(A)"
-apply (unfold chain_def)
-apply blast
+apply (unfold chain_def, blast)
done
lemma Zorn: "ALL c: chain(S). Union(c) : S ==> EX y:S. ALL z:S. y<=z --> y=z"
@@ -295,14 +280,13 @@
apply (simp add: maxchain_def)
apply (rename_tac c)
apply (rule_tac x = "Union (c)" in bexI)
-prefer 2 apply (blast)
+prefer 2 apply blast
apply safe
apply (rename_tac z)
apply (rule classical)
apply (subgoal_tac "cons (z,c) : super (S,c) ")
apply (blast elim: equalityE)
-apply (unfold super_def)
-apply safe
+apply (unfold super_def, safe)
apply (fast elim: chain_extend)
apply (fast elim: equalityE)
done
@@ -315,10 +299,9 @@
"[| n: TFin(S,next); Z <= TFin(S,next); z:Z; ~ Inter(Z) : Z |]
==> ALL m:Z. n<=m"
apply (erule TFin_induct)
-prefer 2 apply (blast) (*second induction step is easy*)
+prefer 2 apply blast (*second induction step is easy*)
apply (rule ballI)
-apply (rule bspec [THEN TFin_subsetD, THEN disjE])
-apply (auto );
+apply (rule bspec [THEN TFin_subsetD, THEN disjE], auto)
apply (subgoal_tac "m = Inter (Z) ")
apply blast+
done
@@ -330,8 +313,7 @@
apply (simp (no_asm_simp) add: Inter_singleton)
apply (erule equal_singleton)
apply (rule Union_upper [THEN equalityI])
-apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec])
-apply (blast intro: elim:)+
+apply (rule_tac [2] subset_refl [THEN TFin_UnionI, THEN TFin_well_lemma5, THEN bspec], blast+)
done
(*This theorem just packages the previous result*)
@@ -341,17 +323,16 @@
apply (unfold Subset_rel_def linear_def)
(*Prove the well-foundedness goal*)
apply (rule wf_onI)
-apply (frule well_ord_TFin_lemma , assumption)
-apply (drule_tac x = "Inter (Z) " in bspec , assumption)
+apply (frule well_ord_TFin_lemma, assumption)
+apply (drule_tac x = "Inter (Z) " in bspec, assumption)
apply blast
(*Now prove the linearity goal*)
apply (intro ballI)
apply (case_tac "x=y")
- apply (blast)
+ apply blast
(*The x~=y case remains*)
apply (rule_tac n1=x and m1=y in TFin_subset_linear [THEN disjE],
- assumption+)
-apply (blast intro: elim:)+
+ assumption+, blast+)
done
(** Defining the "next" operation for Zermelo's Theorem **)
@@ -369,7 +350,7 @@
next`X = (if X=S then S else cons(ch`(S-X), X))"
apply (rule_tac x="\<lambda>X\<in>Pow(S). if X=S then S else cons(ch`(S-X), X)"
in bexI)
-apply (force );
+apply force
apply (unfold increasing_def)
apply (rule CollectI)
apply (rule lam_type)
@@ -414,13 +395,11 @@
(*The wellordering theorem*)
lemma AC_well_ord: "EX r. well_ord(S,r)"
apply (rule AC_Pi_Pow [THEN exE])
-apply (rule Zermelo_next_exists [THEN bexE])
-apply assumption
+apply (rule Zermelo_next_exists [THEN bexE], assumption)
apply (rule exI)
apply (rule well_ord_rvimage)
apply (erule_tac [2] well_ord_TFin)
-apply (rule choice_imp_injection [THEN inj_weaken_type])
-apply (blast intro: elim:)+
+apply (rule choice_imp_injection [THEN inj_weaken_type], blast+)
done
end
--- a/src/ZF/func.thy Mon Jul 01 18:16:18 2002 +0200
+++ b/src/ZF/func.thy Tue Jul 02 13:28:08 2002 +0200
@@ -415,7 +415,7 @@
(*For Finite.ML. Inclusion of right into left is easy*)
lemma cons_fun_eq:
- "c ~: A ==> cons(c,A) -> B = (UN f: A->B. UN b:B. {cons(<c,b>, f)})"
+ "c ~: A ==> cons(c,A) -> B = (\<Union>f \<in> A->B. \<Union>b\<in>B. {cons(<c,b>, f)})"
apply (rule equalityI)
apply (safe elim!: fun_extend3)
(*Inclusion of left into right*)
@@ -432,6 +432,9 @@
apply (erule consE, simp_all)
done
+lemma succ_fun_eq: "succ(n) -> B = (\<Union>f \<in> n->B. \<Union>b\<in>B. {cons(<n,b>, f)})"
+by (simp add: succ_def mem_not_refl cons_fun_eq)
+
ML
{*
val Pi_iff = thm "Pi_iff";