--- a/src/HOL/NumberTheory/Gauss.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy Tue Nov 07 19:40:13 2006 +0100
@@ -10,37 +10,45 @@
locale GAUSS =
fixes p :: "int"
fixes a :: "int"
- fixes A :: "int set"
- fixes B :: "int set"
- fixes C :: "int set"
- fixes D :: "int set"
- fixes E :: "int set"
- fixes F :: "int set"
assumes p_prime: "zprime p"
assumes p_g_2: "2 < p"
assumes p_a_relprime: "~[a = 0](mod p)"
assumes a_nonzero: "0 < a"
+begin
- defines A_def: "A == {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
- defines B_def: "B == (%x. x * a) ` A"
- defines C_def: "C == (StandardRes p) ` B"
- defines D_def: "D == C \<inter> {x. x \<le> ((p - 1) div 2)}"
- defines E_def: "E == C \<inter> {x. ((p - 1) div 2) < x}"
- defines F_def: "F == (%x. (p - x)) ` E"
+definition
+ A :: "int set"
+ "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
+
+ B :: "int set"
+ "B = (%x. x * a) ` A"
+
+ C :: "int set"
+ "C = StandardRes p ` B"
+
+ D :: "int set"
+ "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
+
+ E :: "int set"
+ "E = C \<inter> {x. ((p - 1) div 2) < x}"
+
+ F :: "int set"
+ "F = (%x. (p - x)) ` E"
+
subsection {* Basic properties of p *}
-lemma (in GAUSS) p_odd: "p \<in> zOdd"
+lemma p_odd: "p \<in> zOdd"
by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
-lemma (in GAUSS) p_g_0: "0 < p"
+lemma p_g_0: "0 < p"
using p_g_2 by auto
-lemma (in GAUSS) int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
+lemma int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
using insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
-lemma (in GAUSS) p_minus_one_l: "(p - 1) div 2 < p"
+lemma p_minus_one_l: "(p - 1) div 2 < p"
proof -
have "(p - 1) div 2 \<le> (p - 1) div 1"
by (rule zdiv_mono2) (auto simp add: p_g_0)
@@ -48,9 +56,11 @@
finally show ?thesis by simp
qed
-lemma (in GAUSS) p_eq: "p = (2 * (p - 1) div 2) + 1"
+lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
using zdiv_zmult_self2 [of 2 "p - 1"] by auto
+end
+
lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
apply (frule odd_minus_one_even)
apply (simp add: zEven_def)
@@ -59,54 +69,58 @@
apply (auto simp add: even_div_2_prop2)
done
-lemma (in GAUSS) p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
+context GAUSS
+begin
+
+lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
apply (frule zodd_imp_zdiv_eq, auto)
done
+
subsection {* Basic Properties of the Gauss Sets *}
-lemma (in GAUSS) finite_A: "finite (A)"
+lemma finite_A: "finite (A)"
apply (auto simp add: A_def)
apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}")
apply (auto simp add: bdd_int_set_l_finite finite_subset)
done
-lemma (in GAUSS) finite_B: "finite (B)"
+lemma finite_B: "finite (B)"
by (auto simp add: B_def finite_A finite_imageI)
-lemma (in GAUSS) finite_C: "finite (C)"
+lemma finite_C: "finite (C)"
by (auto simp add: C_def finite_B finite_imageI)
-lemma (in GAUSS) finite_D: "finite (D)"
+lemma finite_D: "finite (D)"
by (auto simp add: D_def finite_Int finite_C)
-lemma (in GAUSS) finite_E: "finite (E)"
+lemma finite_E: "finite (E)"
by (auto simp add: E_def finite_Int finite_C)
-lemma (in GAUSS) finite_F: "finite (F)"
+lemma finite_F: "finite (F)"
by (auto simp add: F_def finite_E finite_imageI)
-lemma (in GAUSS) C_eq: "C = D \<union> E"
+lemma C_eq: "C = D \<union> E"
by (auto simp add: C_def D_def E_def)
-lemma (in GAUSS) A_card_eq: "card A = nat ((p - 1) div 2)"
+lemma A_card_eq: "card A = nat ((p - 1) div 2)"
apply (auto simp add: A_def)
apply (insert int_nat)
apply (erule subst)
apply (auto simp add: card_bdd_int_set_l_le)
done
-lemma (in GAUSS) inj_on_xa_A: "inj_on (%x. x * a) A"
+lemma inj_on_xa_A: "inj_on (%x. x * a) A"
using a_nonzero by (simp add: A_def inj_on_def)
-lemma (in GAUSS) A_res: "ResSet p A"
+lemma A_res: "ResSet p A"
apply (auto simp add: A_def ResSet_def)
apply (rule_tac m = p in zcong_less_eq)
apply (insert p_g_2, auto)
done
-lemma (in GAUSS) B_res: "ResSet p B"
+lemma B_res: "ResSet p B"
apply (insert p_g_2 p_a_relprime p_minus_one_l)
apply (auto simp add: B_def)
apply (rule ResSet_image)
@@ -128,7 +142,7 @@
by (simp add: prems p_minus_one_l p_g_0)
qed
-lemma (in GAUSS) SR_B_inj: "inj_on (StandardRes p) B"
+lemma SR_B_inj: "inj_on (StandardRes p) B"
apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems)
proof -
fix x fix y
@@ -153,23 +167,23 @@
by simp
qed
-lemma (in GAUSS) inj_on_pminusx_E: "inj_on (%x. p - x) E"
+lemma inj_on_pminusx_E: "inj_on (%x. p - x) E"
apply (auto simp add: E_def C_def B_def A_def)
apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI)
apply auto
done
-lemma (in GAUSS) A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)"
+lemma A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)"
apply (auto simp add: A_def)
apply (frule_tac m = p in zcong_not_zero)
apply (insert p_minus_one_l)
apply auto
done
-lemma (in GAUSS) A_greater_zero: "x \<in> A ==> 0 < x"
+lemma A_greater_zero: "x \<in> A ==> 0 < x"
by (auto simp add: A_def)
-lemma (in GAUSS) B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)"
+lemma B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)"
apply (auto simp add: B_def)
apply (frule A_ncong_p)
apply (insert p_a_relprime p_prime a_nonzero)
@@ -177,10 +191,10 @@
apply (auto simp add: A_greater_zero)
done
-lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x"
+lemma B_greater_zero: "x \<in> B ==> 0 < x"
using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
-lemma (in GAUSS) C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)"
+lemma C_ncong_p: "x \<in> C ==> ~[x = 0](mod p)"
apply (auto simp add: C_def)
apply (frule B_ncong_p)
apply (subgoal_tac "[x = StandardRes p x](mod p)")
@@ -189,7 +203,7 @@
apply auto
done
-lemma (in GAUSS) C_greater_zero: "y \<in> C ==> 0 < y"
+lemma C_greater_zero: "y \<in> C ==> 0 < y"
apply (auto simp add: C_def)
proof -
fix x
@@ -204,13 +218,13 @@
by (simp add: order_le_less)
qed
-lemma (in GAUSS) D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)"
+lemma D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)"
by (auto simp add: D_def C_ncong_p)
-lemma (in GAUSS) E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)"
+lemma E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)"
by (auto simp add: E_def C_ncong_p)
-lemma (in GAUSS) F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)"
+lemma F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)"
apply (auto simp add: F_def)
proof -
fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
@@ -225,7 +239,7 @@
from this show False by (simp add: b)
qed
-lemma (in GAUSS) F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
+lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
apply (auto simp add: F_def E_def)
apply (insert p_g_0)
apply (frule_tac x = xa in StandardRes_ubound)
@@ -241,19 +255,19 @@
by simp
qed
-lemma (in GAUSS) D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
+lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
by (auto simp add: D_def C_greater_zero)
-lemma (in GAUSS) F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}"
+lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}"
by (auto simp add: F_def E_def D_def C_def B_def A_def)
-lemma (in GAUSS) D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}"
+lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}"
by (auto simp add: D_def C_def B_def A_def)
-lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
+lemma D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
by (auto simp add: D_eq)
-lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
+lemma F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
apply (auto simp add: F_eq A_def)
proof -
fix y
@@ -268,24 +282,25 @@
using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
qed
-lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
+lemma all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
-lemma (in GAUSS) A_prod_relprime: "zgcd((setprod id A),p) = 1"
+lemma A_prod_relprime: "zgcd((setprod id A),p) = 1"
using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
+
subsection {* Relationships Between Gauss Sets *}
-lemma (in GAUSS) B_card_eq_A: "card B = card A"
+lemma B_card_eq_A: "card B = card A"
using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
-lemma (in GAUSS) B_card_eq: "card B = nat ((p - 1) div 2)"
+lemma B_card_eq: "card B = nat ((p - 1) div 2)"
by (simp add: B_card_eq_A A_card_eq)
-lemma (in GAUSS) F_card_eq_E: "card F = card E"
+lemma F_card_eq_E: "card F = card E"
using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
-lemma (in GAUSS) C_card_eq_B: "card C = card B"
+lemma C_card_eq_B: "card C = card B"
apply (insert finite_B)
apply (subgoal_tac "inj_on (StandardRes p) B")
apply (simp add: B_def C_def card_image)
@@ -293,19 +308,19 @@
apply (simp add: B_res)
done
-lemma (in GAUSS) D_E_disj: "D \<inter> E = {}"
+lemma D_E_disj: "D \<inter> E = {}"
by (auto simp add: D_def E_def)
-lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E"
+lemma C_card_eq_D_plus_E: "card C = card D + card E"
by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
-lemma (in GAUSS) C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
+lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
apply (insert D_E_disj finite_D finite_E C_eq)
apply (frule setprod_Un_disjoint [of D E id])
apply auto
done
-lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
+lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
apply (auto simp add: C_def)
apply (insert finite_B SR_B_inj)
apply (frule_tac f = "StandardRes p" in setprod_reindex_id [symmetric], auto)
@@ -313,15 +328,12 @@
apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
done
-lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A"
+lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
apply (rule Un_least)
apply (auto simp add: A_def F_subset D_subset)
done
-lemma two_eq: "2 * (x::int) = x + x"
- by arith
-
-lemma (in GAUSS) F_D_disj: "(F \<inter> D) = {}"
+lemma F_D_disj: "(F \<inter> D) = {}"
apply (simp add: F_eq D_eq)
apply (auto simp add: F_eq D_eq)
proof -
@@ -366,8 +378,7 @@
done
qed
-lemma (in GAUSS) F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
- apply (insert F_D_disj finite_F finite_D)
+lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
proof -
have "card (F \<union> D) = card E + card D"
by (auto simp add: finite_F finite_D F_D_disj
@@ -378,17 +389,17 @@
by (simp add: C_card_eq_B B_card_eq)
qed
-lemma (in GAUSS) F_Un_D_eq_A: "F \<union> D = A"
+lemma F_Un_D_eq_A: "F \<union> D = A"
using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq)
-lemma (in GAUSS) prod_D_F_eq_prod_A:
+lemma prod_D_F_eq_prod_A:
"(setprod id D) * (setprod id F) = setprod id A"
apply (insert F_D_disj finite_D finite_F)
apply (frule setprod_Un_disjoint [of F D id])
apply (auto simp add: F_Un_D_eq_A)
done
-lemma (in GAUSS) prod_F_zcong:
+lemma prod_F_zcong:
"[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
proof -
have "setprod id F = setprod id (op - p ` E)"
@@ -438,12 +449,13 @@
by simp
qed
+
subsection {* Gauss' Lemma *}
-lemma (in GAUSS) aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
+lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
by (auto simp add: finite_E neg_one_special)
-theorem (in GAUSS) pre_gauss_lemma:
+theorem pre_gauss_lemma:
"[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
have "[setprod id A = setprod id F * setprod id D](mod p)"
@@ -499,7 +511,7 @@
by (simp add: A_card_eq zcong_sym)
qed
-theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
+theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
proof -
from Euler_Criterion p_prime p_g_2 have
"[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
@@ -516,3 +528,5 @@
qed
end
+
+end
--- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy Tue Nov 07 19:40:13 2006 +0100
@@ -14,7 +14,10 @@
Zuckerman's presentation.
*}
-lemma (in GAUSS) QRLemma1: "a * setsum id A =
+context GAUSS
+begin
+
+lemma QRLemma1: "a * setsum id A =
p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
proof -
from finite_A have "a * setsum id A = setsum (%x. a * x) A"
@@ -44,7 +47,7 @@
finally show ?thesis by arith
qed
-lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E +
+lemma QRLemma2: "setsum id A = p * int (card E) - setsum id E +
setsum id D"
proof -
from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)"
@@ -65,7 +68,7 @@
by arith
qed
-lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A =
+lemma QRLemma3: "(a - 1) * setsum id A =
p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E"
proof -
have "(a - 1) * setsum id A = a * setsum id A - setsum id A"
@@ -83,7 +86,7 @@
by (auto simp only: zdiff_zmult_distrib2)
qed
-lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==>
+lemma QRLemma4: "a \<in> zOdd ==>
(setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)"
proof -
assume a_odd: "a \<in> zOdd"
@@ -108,7 +111,7 @@
by (auto simp only: even_diff [symmetric])
qed
-lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==>
+lemma QRLemma5: "a \<in> zOdd ==>
(-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
proof -
assume "a \<in> zOdd"
@@ -138,6 +141,8 @@
finally show ?thesis .
qed
+end
+
lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p)); zprime p; 2 < p;
A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==>
(Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
@@ -145,6 +150,7 @@
apply (auto simp add: GAUSS_def)
apply (subst GAUSS.QRLemma5)
apply (auto simp add: GAUSS_def)
+ apply (simp add: GAUSS.A_def [OF GAUSS.intro] GAUSS_def)
done
@@ -153,47 +159,51 @@
locale QRTEMP =
fixes p :: "int"
fixes q :: "int"
- fixes P_set :: "int set"
- fixes Q_set :: "int set"
- fixes S :: "(int * int) set"
- fixes S1 :: "(int * int) set"
- fixes S2 :: "(int * int) set"
- fixes f1 :: "int => (int * int) set"
- fixes f2 :: "int => (int * int) set"
assumes p_prime: "zprime p"
assumes p_g_2: "2 < p"
assumes q_prime: "zprime q"
assumes q_g_2: "2 < q"
assumes p_neq_q: "p \<noteq> q"
+begin
- defines P_set_def: "P_set == {x. 0 < x & x \<le> ((p - 1) div 2) }"
- defines Q_set_def: "Q_set == {x. 0 < x & x \<le> ((q - 1) div 2) }"
- defines S_def: "S == P_set <*> Q_set"
- defines S1_def: "S1 == { (x, y). (x, y):S & ((p * y) < (q * x)) }"
- defines S2_def: "S2 == { (x, y). (x, y):S & ((q * x) < (p * y)) }"
- defines f1_def: "f1 j == { (j1, y). (j1, y):S & j1 = j &
- (y \<le> (q * j) div p) }"
- defines f2_def: "f2 j == { (x, j1). (x, j1):S & j1 = j &
- (x \<le> (p * j) div q) }"
+definition
+ P_set :: "int set"
+ "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
+
+ Q_set :: "int set"
+ "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
+
+ S :: "(int * int) set"
+ "S = P_set <*> Q_set"
+
+ S1 :: "(int * int) set"
+ "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
-lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2"
+ S2 :: "(int * int) set"
+ "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
+
+ f1 :: "int => (int * int) set"
+ "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
+
+ f2 :: "int => (int * int) set"
+ "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
+
+lemma p_fact: "0 < (p - 1) div 2"
proof -
- from prems have "2 < p" by (simp add: QRTEMP_def)
- then have "2 \<le> p - 1" by arith
+ from p_g_2 have "2 \<le> p - 1" by arith
then have "2 div 2 \<le> (p - 1) div 2" by (rule zdiv_mono1, auto)
then show ?thesis by auto
qed
-lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2"
+lemma q_fact: "0 < (q - 1) div 2"
proof -
- from prems have "2 < q" by (simp add: QRTEMP_def)
- then have "2 \<le> q - 1" by arith
+ from q_g_2 have "2 \<le> q - 1" by arith
then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto)
then show ?thesis by auto
qed
-lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
+lemma pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
(p * b \<noteq> q * a)"
proof
assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
@@ -234,43 +244,43 @@
with q_g_2 show False by auto
qed
-lemma (in QRTEMP) P_set_finite: "finite (P_set)"
+lemma P_set_finite: "finite (P_set)"
using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)
-lemma (in QRTEMP) Q_set_finite: "finite (Q_set)"
+lemma Q_set_finite: "finite (Q_set)"
using q_fact by (auto simp add: Q_set_def bdd_int_set_l_le_finite)
-lemma (in QRTEMP) S_finite: "finite S"
+lemma S_finite: "finite S"
by (auto simp add: S_def P_set_finite Q_set_finite finite_cartesian_product)
-lemma (in QRTEMP) S1_finite: "finite S1"
+lemma S1_finite: "finite S1"
proof -
have "finite S" by (auto simp add: S_finite)
moreover have "S1 \<subseteq> S" by (auto simp add: S1_def S_def)
ultimately show ?thesis by (auto simp add: finite_subset)
qed
-lemma (in QRTEMP) S2_finite: "finite S2"
+lemma S2_finite: "finite S2"
proof -
have "finite S" by (auto simp add: S_finite)
moreover have "S2 \<subseteq> S" by (auto simp add: S2_def S_def)
ultimately show ?thesis by (auto simp add: finite_subset)
qed
-lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))"
+lemma P_set_card: "(p - 1) div 2 = int (card (P_set))"
using p_fact by (auto simp add: P_set_def card_bdd_int_set_l_le)
-lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))"
+lemma Q_set_card: "(q - 1) div 2 = int (card (Q_set))"
using q_fact by (auto simp add: Q_set_def card_bdd_int_set_l_le)
-lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
+lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
using P_set_card Q_set_card P_set_finite Q_set_finite
by (auto simp add: S_def zmult_int setsum_constant)
-lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}"
+lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
by (auto simp add: S1_def S2_def)
-lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2"
+lemma S1_Union_S2_prop: "S = S1 \<union> S2"
apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
proof -
fix a and b
@@ -280,7 +290,7 @@
ultimately show "p * b < q * a" by auto
qed
-lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
+lemma card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
int(card(S1)) + int(card(S2))"
proof -
have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
@@ -293,7 +303,7 @@
finally show ?thesis .
qed
-lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
+lemma aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
0 < b; b \<le> (q - 1) div 2 |] ==>
(p * b < q * a) = (b \<le> q * a div p)"
proof -
@@ -327,7 +337,7 @@
ultimately show ?thesis ..
qed
-lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
+lemma aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
0 < b; b \<le> (q - 1) div 2 |] ==>
(q * a < p * b) = (a \<le> p * b div q)"
proof -
@@ -361,6 +371,8 @@
ultimately show ?thesis ..
qed
+end
+
lemma aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
(q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
proof-
@@ -390,7 +402,10 @@
using prems by auto
qed
-lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
+context QRTEMP
+begin
+
+lemma aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
proof
fix j
assume j_fact: "j \<in> P_set"
@@ -422,7 +437,7 @@
by (auto simp add: mult_le_cancel_left)
with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
by (auto simp add: zdiv_mono1)
- also from prems have "... \<le> (q - 1) div 2"
+ also from prems P_set_def have "... \<le> (q - 1) div 2"
apply simp
apply (insert aux2)
apply (simp add: QRTEMP_def)
@@ -446,7 +461,7 @@
finally show "int (card (f1 j)) = q * j div p" .
qed
-lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q"
+lemma aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q"
proof
fix j
assume j_fact: "j \<in> Q_set"
@@ -499,7 +514,7 @@
finally show "int (card (f2 j)) = p * j div q" .
qed
-lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set"
+lemma S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set"
proof -
have "\<forall>x \<in> P_set. finite (f1 x)"
proof
@@ -522,7 +537,7 @@
finally show ?thesis .
qed
-lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set"
+lemma S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set"
proof -
have "\<forall>x \<in> Q_set. finite (f2 x)"
proof
@@ -546,15 +561,15 @@
finally show ?thesis .
qed
-lemma (in QRTEMP) S1_carda: "int (card(S1)) =
+lemma S1_carda: "int (card(S1)) =
setsum (%j. (j * q) div p) P_set"
by (auto simp add: S1_card zmult_ac)
-lemma (in QRTEMP) S2_carda: "int (card(S2)) =
+lemma S2_carda: "int (card(S2)) =
setsum (%j. (j * p) div q) Q_set"
by (auto simp add: S2_card zmult_ac)
-lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
+lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
(setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
proof -
have "(setsum (%j. (j * p) div q) Q_set) +
@@ -567,6 +582,8 @@
finally show ?thesis .
qed
+end
+
lemma pq_prime_neq: "[| zprime p; zprime q; p \<noteq> q |] ==> (~[p = 0] (mod q))"
apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
apply (drule_tac x = q in allE)
@@ -574,12 +591,15 @@
apply auto
done
-lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) =
+context QRTEMP
+begin
+
+lemma QR_short: "(Legendre p q) * (Legendre q p) =
(-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
proof -
from prems have "~([p = 0] (mod q))"
by (auto simp add: pq_prime_neq QRTEMP_def)
- with prems have a1: "(Legendre p q) = (-1::int) ^
+ with prems Q_set_def have a1: "(Legendre p q) = (-1::int) ^
nat(setsum (%x. ((x * p) div q)) Q_set)"
apply (rule_tac p = q in MainQRLemma)
apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
@@ -588,7 +608,7 @@
apply (rule_tac p = q and q = p in pq_prime_neq)
apply (simp add: QRTEMP_def)+
done
- with prems have a2: "(Legendre q p) =
+ with prems P_set_def have a2: "(Legendre q p) =
(-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
apply (rule_tac p = p in MainQRLemma)
apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
@@ -613,6 +633,8 @@
finally show ?thesis .
qed
+end
+
theorem Quadratic_Reciprocity:
"[| p \<in> zOdd; zprime p; q \<in> zOdd; zprime q;
p \<noteq> q |]
--- a/src/ZF/Constructible/AC_in_L.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/AC_in_L.thy Tue Nov 07 19:40:13 2006 +0100
@@ -222,7 +222,7 @@
(environment, formula) pairs into the ordinals. For each member of @{term
"DPow(A)"}, we take the minimum such ordinal.*}
-constdefs
+definition
env_form_r :: "[i,i,i]=>i"
--{*wellordering on (environment, formula) pairs*}
"env_form_r(f,r,A) ==
@@ -317,7 +317,7 @@
@{term "Lset(i)"}. We assume as an inductive hypothesis that there is a family
of wellorderings for smaller ordinals.*}
-constdefs
+definition
rlimit :: "[i,i=>i]=>i"
--{*Expresses the wellordering at limit ordinals. The conditional
lets us remove the premise @{term "Limit(i)"} from some theorems.*}
@@ -400,7 +400,7 @@
subsection{*Transfinite Definition of the Wellordering on @{term "L"}*}
-constdefs
+definition
L_r :: "[i, i] => i"
"L_r(f) == %i.
transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)),
--- a/src/ZF/Constructible/DPow_absolute.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/DPow_absolute.thy Tue Nov 07 19:40:13 2006 +0100
@@ -23,7 +23,7 @@
successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
*)
-constdefs formula_rec_fm :: "[i, i, i]=>i"
+definition formula_rec_fm :: "[i, i, i]=>i"
"formula_rec_fm(mh,p,z) ==
Exists(Exists(Exists(
And(finite_ordinal_fm(2),
@@ -80,7 +80,7 @@
subsubsection{*The Operator @{term is_satisfies}*}
(* is_satisfies(M,A,p,z) == is_formula_rec (M, satisfies_MH(M,A), p, z) *)
-constdefs satisfies_fm :: "[i,i,i]=>i"
+definition satisfies_fm :: "[i,i,i]=>i"
"satisfies_fm(x) == formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))"
lemma is_satisfies_type [TC]:
@@ -119,7 +119,7 @@
text{*Relativize the use of @{term sats} within @{term DPow'}
(the comprehension).*}
-constdefs
+definition
is_DPow_sats :: "[i=>o,i,i,i,i] => o"
"is_DPow_sats(M,A,env,p,x) ==
\<forall>n1[M]. \<forall>e[M]. \<forall>sp[M].
@@ -148,7 +148,7 @@
is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) -->
fun_apply(M, sp, e, n1) --> number1(M, n1) *)
-constdefs DPow_sats_fm :: "[i,i,i,i]=>i"
+definition DPow_sats_fm :: "[i,i,i,i]=>i"
"DPow_sats_fm(A,env,p,x) ==
Forall(Forall(Forall(
Implies(satisfies_fm(A#+3,p#+3,0),
@@ -218,7 +218,7 @@
done
text{*Relativization of the Operator @{term DPow'}*}
-constdefs
+definition
is_DPow' :: "[i=>o,i,i] => o"
"is_DPow'(M,A,Z) ==
\<forall>X[M]. X \<in> Z <->
@@ -310,7 +310,7 @@
(* is_Collect :: "[i=>o,i,i=>o,i] => o"
"is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)" *)
-constdefs Collect_fm :: "[i, i, i]=>i"
+definition Collect_fm :: "[i, i, i]=>i"
"Collect_fm(A,is_P,z) ==
Forall(Iff(Member(0,succ(z)),
And(Member(0,succ(A)), is_P)))"
@@ -360,7 +360,7 @@
(* is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
"is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))" *)
-constdefs Replace_fm :: "[i, i, i]=>i"
+definition Replace_fm :: "[i, i, i]=>i"
"Replace_fm(A,is_P,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,A#+2), is_P))))"
@@ -413,7 +413,7 @@
(\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" *)
-constdefs DPow'_fm :: "[i,i]=>i"
+definition DPow'_fm :: "[i,i]=>i"
"DPow'_fm(A,Z) ==
Forall(
Iff(Member(0,succ(Z)),
@@ -451,7 +451,7 @@
subsection{*A Locale for Relativizing the Operator @{term Lset}*}
-constdefs
+definition
transrec_body :: "[i=>o,i,i,i,i] => o"
"transrec_body(M,g,x) ==
\<lambda>y z. \<exists>gy[M]. y \<in> x & fun_apply(M,g,y,gy) & is_DPow'(M,gy,z)"
@@ -503,7 +503,7 @@
text{*Relativization of the Operator @{term Lset}*}
-constdefs
+definition
is_Lset :: "[i=>o, i, i] => o"
--{*We can use the term language below because @{term is_Lset} will
not have to be internalized: it isn't used in any instance of
@@ -609,7 +609,7 @@
subsection{*The Notion of Constructible Set*}
-constdefs
+definition
constructible :: "[i=>o,i] => o"
"constructible(M,x) ==
\<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
--- a/src/ZF/Constructible/Datatype_absolute.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Datatype_absolute.thy Tue Nov 07 19:40:13 2006 +0100
@@ -10,7 +10,7 @@
subsection{*The lfp of a continuous function can be expressed as a union*}
-constdefs
+definition
directed :: "i=>o"
"directed(A) == A\<noteq>0 & (\<forall>x\<in>A. \<forall>y\<in>A. x \<union> y \<in> A)"
@@ -113,7 +113,7 @@
subsection {*Absoluteness for "Iterates"*}
-constdefs
+definition
iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
"iterates_MH(M,isF,v,n,g,z) ==
@@ -207,7 +207,7 @@
by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
-constdefs
+definition
is_list_functor :: "[i=>o,i,i,i] => o"
"is_list_functor(M,A,X,Z) ==
\<exists>n1[M]. \<exists>AX[M].
@@ -260,7 +260,7 @@
formula_fun_contin)
-constdefs
+definition
is_formula_functor :: "[i=>o,i,i] => o"
"is_formula_functor(M,X,Z) ==
\<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M].
@@ -278,7 +278,7 @@
subsection{*@{term M} Contains the List and Formula Datatypes*}
-constdefs
+definition
list_N :: "[i,i] => i"
"list_N(A,n) == (\<lambda>X. {0} + A * X)^n (0)"
@@ -339,7 +339,7 @@
apply (simp add: list_imp_list_N)
done
-constdefs
+definition
is_list_N :: "[i=>o,i,i,i] => o"
"is_list_N(M,A,n,Z) ==
\<exists>zero[M]. empty(M,zero) &
@@ -366,7 +366,7 @@
by (induct_tac p, simp_all)
-constdefs
+definition
formula_N :: "i => i"
"formula_N(n) == (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0)"
@@ -441,14 +441,14 @@
le_imp_subset formula_N_mono)
done
-constdefs
+definition
is_formula_N :: "[i=>o,i,i] => o"
"is_formula_N(M,n,Z) ==
\<exists>zero[M]. empty(M,zero) &
is_iterates(M, is_formula_functor(M), zero, n, Z)"
-constdefs
+definition
mem_formula :: "[i=>o,i] => o"
"mem_formula(M,p) ==
@@ -584,7 +584,7 @@
apply (simp add: nat_rec_succ)
done
-constdefs
+definition
is_eclose_n :: "[i=>o,i,i,i] => o"
"is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z)"
@@ -643,7 +643,7 @@
subsection {*Absoluteness for @{term transrec}*}
text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
-constdefs
+definition
is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
"is_transrec(M,MH,a,z) ==
@@ -691,7 +691,7 @@
subsection{*Absoluteness for the List Operator @{term length}*}
text{*But it is never used.*}
-constdefs
+definition
is_length :: "[i=>o,i,i,i] => o"
"is_length(M,A,l,n) ==
\<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M].
@@ -739,7 +739,7 @@
apply (simp add: not_lt_iff_le nth_eq_0)
done
-constdefs
+definition
is_nth :: "[i=>o,i,i,i] => o"
"is_nth(M,n,l,Z) ==
\<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)"
@@ -757,7 +757,7 @@
subsection{*Relativization and Absoluteness for the @{term formula} Constructors*}
-constdefs
+definition
is_Member :: "[i=>o,i,i,i] => o"
--{* because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}*}
"is_Member(M,x,y,Z) ==
@@ -771,7 +771,7 @@
"M(Member(x,y)) <-> M(x) & M(y)"
by (simp add: Member_def)
-constdefs
+definition
is_Equal :: "[i=>o,i,i,i] => o"
--{* because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}*}
"is_Equal(M,x,y,Z) ==
@@ -784,7 +784,7 @@
lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
by (simp add: Equal_def)
-constdefs
+definition
is_Nand :: "[i=>o,i,i,i] => o"
--{* because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}*}
"is_Nand(M,x,y,Z) ==
@@ -797,7 +797,7 @@
lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
by (simp add: Nand_def)
-constdefs
+definition
is_Forall :: "[i=>o,i,i] => o"
--{* because @{term "Forall(x) \<equiv> Inr(Inr(p))"}*}
"is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)"
@@ -813,7 +813,7 @@
subsection {*Absoluteness for @{term formula_rec}*}
-constdefs
+definition
formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
--{* the instance of @{term formula_case} in @{term formula_rec}*}
@@ -847,7 +847,7 @@
subsubsection{*Absoluteness for the Formula Operator @{term depth}*}
-constdefs
+definition
is_depth :: "[i=>o,i,i] => o"
"is_depth(M,p,n) ==
@@ -873,7 +873,7 @@
subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
-constdefs
+definition
is_formula_case ::
"[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
@@ -909,7 +909,7 @@
subsubsection {*Absoluteness for @{term formula_rec}: Final Results*}
-constdefs
+definition
is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
--{* predicate to relativize the functional @{term formula_rec}*}
"is_formula_rec(M,MH,p,z) ==
--- a/src/ZF/Constructible/Formula.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Formula.thy Tue Nov 07 19:40:13 2006 +0100
@@ -21,22 +21,22 @@
declare formula.intros [TC]
-constdefs Neg :: "i=>i"
+definition Neg :: "i=>i"
"Neg(p) == Nand(p,p)"
-constdefs And :: "[i,i]=>i"
+definition And :: "[i,i]=>i"
"And(p,q) == Neg(Nand(p,q))"
-constdefs Or :: "[i,i]=>i"
+definition Or :: "[i,i]=>i"
"Or(p,q) == Nand(Neg(p),Neg(q))"
-constdefs Implies :: "[i,i]=>i"
+definition Implies :: "[i,i]=>i"
"Implies(p,q) == Nand(p,Neg(q))"
-constdefs Iff :: "[i,i]=>i"
+definition Iff :: "[i,i]=>i"
"Iff(p,q) == And(Implies(p,q), Implies(q,p))"
-constdefs Exists :: "i=>i"
+definition Exists :: "i=>i"
"Exists(p) == Neg(Forall(Neg(p)))";
lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula"
@@ -76,10 +76,11 @@
lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool"
-by (induct_tac p, simp_all)
+by (induct set: formula) simp_all
-syntax sats :: "[i,i,i] => o"
-translations "sats(A,p,env)" == "satisfies(A,p)`env = 1"
+abbreviation
+ sats :: "[i,i,i] => o"
+ "sats(A,p,env) == satisfies(A,p)`env = 1"
lemma [simp]:
"env \<in> list(A)
@@ -245,7 +246,7 @@
subsection{*Renaming Some de Bruijn Variables*}
-constdefs incr_var :: "[i,i]=>i"
+definition incr_var :: "[i,i]=>i"
"incr_var(x,nq) == if x<nq then x else succ(x)"
lemma incr_var_lt: "x<nq ==> incr_var(x,nq) = x"
@@ -333,7 +334,7 @@
subsection{*Renaming all but the First de Bruijn Variable*}
-constdefs incr_bv1 :: "i => i"
+definition incr_bv1 :: "i => i"
"incr_bv1(p) == incr_bv(p)`1"
@@ -384,7 +385,7 @@
subsection{*Definable Powerset*}
text{*The definable powerset operation: Kunen's definition VI 1.1, page 165.*}
-constdefs DPow :: "i => i"
+definition DPow :: "i => i"
"DPow(A) == {X \<in> Pow(A).
\<exists>env \<in> list(A). \<exists>p \<in> formula.
arity(p) \<le> succ(length(env)) &
@@ -506,7 +507,7 @@
subsubsection{*The subset relation*}
-constdefs subset_fm :: "[i,i]=>i"
+definition subset_fm :: "[i,i]=>i"
"subset_fm(x,y) == 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"
@@ -526,7 +527,7 @@
subsubsection{*Transitive sets*}
-constdefs transset_fm :: "i=>i"
+definition transset_fm :: "i=>i"
"transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
@@ -546,7 +547,7 @@
subsubsection{*Ordinals*}
-constdefs ordinal_fm :: "i=>i"
+definition ordinal_fm :: "i=>i"
"ordinal_fm(x) ==
And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
@@ -577,7 +578,7 @@
subsection{* Constant Lset: Levels of the Constructible Universe *}
-constdefs
+definition
Lset :: "i=>i"
"Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
@@ -823,7 +824,7 @@
text{*The rank function for the constructible universe*}
-constdefs
+definition
lrank :: "i=>i" --{*Kunen's definition VI 1.7*}
"lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
@@ -983,7 +984,7 @@
text{*A simpler version of @{term DPow}: no arity check!*}
-constdefs DPow' :: "i => i"
+definition DPow' :: "i => i"
"DPow'(A) == {X \<in> Pow(A).
\<exists>env \<in> list(A). \<exists>p \<in> formula.
X = {x\<in>A. sats(A, p, Cons(x,env))}}"
--- a/src/ZF/Constructible/Internalize.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Internalize.thy Tue Nov 07 19:40:13 2006 +0100
@@ -10,7 +10,7 @@
subsubsection{*The Formula @{term is_Inl}, Internalized*}
(* is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z) *)
-constdefs Inl_fm :: "[i,i]=>i"
+definition Inl_fm :: "[i,i]=>i"
"Inl_fm(a,z) == Exists(And(empty_fm(0), pair_fm(0,succ(a),succ(z))))"
lemma Inl_type [TC]:
@@ -39,7 +39,7 @@
subsubsection{*The Formula @{term is_Inr}, Internalized*}
(* is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z) *)
-constdefs Inr_fm :: "[i,i]=>i"
+definition Inr_fm :: "[i,i]=>i"
"Inr_fm(a,z) == Exists(And(number1_fm(0), pair_fm(0,succ(a),succ(z))))"
lemma Inr_type [TC]:
@@ -69,7 +69,7 @@
(* is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs) *)
-constdefs Nil_fm :: "i=>i"
+definition Nil_fm :: "i=>i"
"Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
@@ -97,7 +97,7 @@
(* "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
-constdefs Cons_fm :: "[i,i,i]=>i"
+definition Cons_fm :: "[i,i,i]=>i"
"Cons_fm(a,l,Z) ==
Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
@@ -128,7 +128,7 @@
(* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
-constdefs quasilist_fm :: "i=>i"
+definition quasilist_fm :: "i=>i"
"quasilist_fm(x) ==
Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
@@ -162,7 +162,7 @@
(is_Nil(M,xs) --> empty(M,H)) &
(\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
(is_quasilist(M,xs) | empty(M,H))" *)
-constdefs hd_fm :: "[i,i]=>i"
+definition hd_fm :: "[i,i]=>i"
"hd_fm(xs,H) ==
And(Implies(Nil_fm(xs), empty_fm(H)),
And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(H#+2,1)))),
@@ -198,7 +198,7 @@
(is_Nil(M,xs) --> T=xs) &
(\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
(is_quasilist(M,xs) | empty(M,T))" *)
-constdefs tl_fm :: "[i,i]=>i"
+definition tl_fm :: "[i,i]=>i"
"tl_fm(xs,T) ==
And(Implies(Nil_fm(xs), Equal(T,xs)),
And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
@@ -234,7 +234,7 @@
"is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))" *)
text{*The formula @{term p} has no free variables.*}
-constdefs bool_of_o_fm :: "[i, i]=>i"
+definition bool_of_o_fm :: "[i, i]=>i"
"bool_of_o_fm(p,z) ==
Or(And(p,number1_fm(z)),
And(Neg(p),empty_fm(z)))"
@@ -276,7 +276,7 @@
"is_lambda(M, A, is_b, z) ==
\<forall>p[M]. p \<in> z <->
(\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))" *)
-constdefs lambda_fm :: "[i, i, i]=>i"
+definition lambda_fm :: "[i, i, i]=>i"
"lambda_fm(p,A,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(Exists(And(Member(1,A#+3),
@@ -315,7 +315,7 @@
(* "is_Member(M,x,y,Z) ==
\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" *)
-constdefs Member_fm :: "[i,i,i]=>i"
+definition Member_fm :: "[i,i,i]=>i"
"Member_fm(x,y,Z) ==
Exists(Exists(And(pair_fm(x#+2,y#+2,1),
And(Inl_fm(1,0), Inl_fm(0,Z#+2)))))"
@@ -347,7 +347,7 @@
(* "is_Equal(M,x,y,Z) ==
\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" *)
-constdefs Equal_fm :: "[i,i,i]=>i"
+definition Equal_fm :: "[i,i,i]=>i"
"Equal_fm(x,y,Z) ==
Exists(Exists(And(pair_fm(x#+2,y#+2,1),
And(Inr_fm(1,0), Inl_fm(0,Z#+2)))))"
@@ -379,7 +379,7 @@
(* "is_Nand(M,x,y,Z) ==
\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" *)
-constdefs Nand_fm :: "[i,i,i]=>i"
+definition Nand_fm :: "[i,i,i]=>i"
"Nand_fm(x,y,Z) ==
Exists(Exists(And(pair_fm(x#+2,y#+2,1),
And(Inl_fm(1,0), Inr_fm(0,Z#+2)))))"
@@ -410,7 +410,7 @@
subsubsection{*The Operator @{term is_Forall}, Internalized*}
(* "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" *)
-constdefs Forall_fm :: "[i,i]=>i"
+definition Forall_fm :: "[i,i]=>i"
"Forall_fm(x,Z) ==
Exists(And(Inr_fm(succ(x),0), Inr_fm(0,succ(Z))))"
@@ -442,7 +442,7 @@
(* is_and(M,a,b,z) == (number1(M,a) & z=b) |
(~number1(M,a) & empty(M,z)) *)
-constdefs and_fm :: "[i,i,i]=>i"
+definition and_fm :: "[i,i,i]=>i"
"and_fm(a,b,z) ==
Or(And(number1_fm(a), Equal(z,b)),
And(Neg(number1_fm(a)),empty_fm(z)))"
@@ -476,7 +476,7 @@
(* is_or(M,a,b,z) == (number1(M,a) & number1(M,z)) |
(~number1(M,a) & z=b) *)
-constdefs or_fm :: "[i,i,i]=>i"
+definition or_fm :: "[i,i,i]=>i"
"or_fm(a,b,z) ==
Or(And(number1_fm(a), number1_fm(z)),
And(Neg(number1_fm(a)), Equal(z,b)))"
@@ -510,7 +510,7 @@
(* is_not(M,a,z) == (number1(M,a) & empty(M,z)) |
(~number1(M,a) & number1(M,z)) *)
-constdefs not_fm :: "[i,i]=>i"
+definition not_fm :: "[i,i]=>i"
"not_fm(a,z) ==
Or(And(number1_fm(a), empty_fm(z)),
And(Neg(number1_fm(a)), number1_fm(z)))"
@@ -576,7 +576,7 @@
*)
text{*The three arguments of @{term p} are always 2, 1, 0 and z*}
-constdefs is_recfun_fm :: "[i, i, i, i]=>i"
+definition is_recfun_fm :: "[i, i, i, i]=>i"
"is_recfun_fm(p,r,a,f) ==
Forall(Iff(Member(0,succ(f)),
Exists(Exists(Exists(
@@ -638,7 +638,7 @@
(* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
"is_wfrec(M,MH,r,a,z) ==
\<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *)
-constdefs is_wfrec_fm :: "[i, i, i, i]=>i"
+definition is_wfrec_fm :: "[i, i, i, i]=>i"
"is_wfrec_fm(p,r,a,z) ==
Exists(And(is_recfun_fm(p, succ(r), succ(a), 0),
Exists(Exists(Exists(Exists(
@@ -696,7 +696,7 @@
subsubsection{*Binary Products, Internalized*}
-constdefs cartprod_fm :: "[i,i,i]=>i"
+definition cartprod_fm :: "[i,i,i]=>i"
(* "cartprod(M,A,B,z) ==
\<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
"cartprod_fm(A,B,z) ==
@@ -736,7 +736,7 @@
3 2 1 0
number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
cartprod(M,s1,B,B1) & union(M,A0,B1,Z)" *)
-constdefs sum_fm :: "[i,i,i]=>i"
+definition sum_fm :: "[i,i,i]=>i"
"sum_fm(A,B,Z) ==
Exists(Exists(Exists(Exists(
And(number1_fm(2),
@@ -771,7 +771,7 @@
subsubsection{*The Operator @{term quasinat}*}
(* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *)
-constdefs quasinat_fm :: "i=>i"
+definition quasinat_fm :: "i=>i"
"quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))"
lemma quasinat_type [TC]:
@@ -808,7 +808,7 @@
(\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
(is_quasinat(M,k) | empty(M,z))" *)
text{*The formula @{term is_b} has free variables 1 and 0.*}
-constdefs is_nat_case_fm :: "[i, i, i, i]=>i"
+definition is_nat_case_fm :: "[i, i, i, i]=>i"
"is_nat_case_fm(a,is_b,k,z) ==
And(Implies(empty_fm(k), Equal(z,a)),
And(Forall(Implies(succ_fm(0,succ(k)),
@@ -863,7 +863,7 @@
"iterates_MH(M,isF,v,n,g,z) ==
is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
n, z)" *)
-constdefs iterates_MH_fm :: "[i, i, i, i, i]=>i"
+definition iterates_MH_fm :: "[i, i, i, i, i]=>i"
"iterates_MH_fm(isF,v,n,g,z) ==
is_nat_case_fm(v,
Exists(And(fun_apply_fm(succ(succ(succ(g))),2,0),
@@ -928,7 +928,7 @@
\<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
1 0 is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"*)
-constdefs is_iterates_fm :: "[i, i, i, i]=>i"
+definition is_iterates_fm :: "[i, i, i, i]=>i"
"is_iterates_fm(p,v,n,Z) ==
Exists(Exists(
And(succ_fm(n#+2,1),
@@ -998,7 +998,7 @@
(* is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z) *)
-constdefs eclose_n_fm :: "[i,i,i]=>i"
+definition eclose_n_fm :: "[i,i,i]=>i"
"eclose_n_fm(A,n,Z) == is_iterates_fm(big_union_fm(1,0), A, n, Z)"
lemma eclose_n_fm_type [TC]:
@@ -1034,7 +1034,7 @@
(* mem_eclose(M,A,l) ==
\<exists>n[M]. \<exists>eclosen[M].
finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen *)
-constdefs mem_eclose_fm :: "[i,i]=>i"
+definition mem_eclose_fm :: "[i,i]=>i"
"mem_eclose_fm(x,y) ==
Exists(Exists(
And(finite_ordinal_fm(1),
@@ -1066,7 +1066,7 @@
subsubsection{*The Predicate ``Is @{term "eclose(A)"}''*}
(* is_eclose(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_eclose(M,A,l) *)
-constdefs is_eclose_fm :: "[i,i]=>i"
+definition is_eclose_fm :: "[i,i]=>i"
"is_eclose_fm(A,Z) ==
Forall(Iff(Member(0,succ(Z)), mem_eclose_fm(succ(A),0)))"
@@ -1095,7 +1095,7 @@
subsubsection{*The List Functor, Internalized*}
-constdefs list_functor_fm :: "[i,i,i]=>i"
+definition list_functor_fm :: "[i,i,i]=>i"
(* "is_list_functor(M,A,X,Z) ==
\<exists>n1[M]. \<exists>AX[M].
number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
@@ -1135,7 +1135,7 @@
\<exists>zero[M]. empty(M,zero) &
is_iterates(M, is_list_functor(M,A), zero, n, Z)" *)
-constdefs list_N_fm :: "[i,i,i]=>i"
+definition list_N_fm :: "[i,i,i]=>i"
"list_N_fm(A,n,Z) ==
Exists(
And(empty_fm(0),
@@ -1175,7 +1175,7 @@
(* mem_list(M,A,l) ==
\<exists>n[M]. \<exists>listn[M].
finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> listn *)
-constdefs mem_list_fm :: "[i,i]=>i"
+definition mem_list_fm :: "[i,i]=>i"
"mem_list_fm(x,y) ==
Exists(Exists(
And(finite_ordinal_fm(1),
@@ -1207,7 +1207,7 @@
subsubsection{*The Predicate ``Is @{term "list(A)"}''*}
(* is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l) *)
-constdefs is_list_fm :: "[i,i]=>i"
+definition is_list_fm :: "[i,i]=>i"
"is_list_fm(A,Z) ==
Forall(Iff(Member(0,succ(Z)), mem_list_fm(succ(A),0)))"
@@ -1236,7 +1236,7 @@
subsubsection{*The Formula Functor, Internalized*}
-constdefs formula_functor_fm :: "[i,i]=>i"
+definition formula_functor_fm :: "[i,i]=>i"
(* "is_formula_functor(M,X,Z) ==
\<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M].
4 3 2 1 0
@@ -1282,7 +1282,7 @@
(* "is_formula_N(M,n,Z) ==
\<exists>zero[M]. empty(M,zero) &
is_iterates(M, is_formula_functor(M), zero, n, Z)" *)
-constdefs formula_N_fm :: "[i,i]=>i"
+definition formula_N_fm :: "[i,i]=>i"
"formula_N_fm(n,Z) ==
Exists(
And(empty_fm(0),
@@ -1322,7 +1322,7 @@
(* mem_formula(M,p) ==
\<exists>n[M]. \<exists>formn[M].
finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> formn *)
-constdefs mem_formula_fm :: "i=>i"
+definition mem_formula_fm :: "i=>i"
"mem_formula_fm(x) ==
Exists(Exists(
And(finite_ordinal_fm(1),
@@ -1354,7 +1354,7 @@
subsubsection{*The Predicate ``Is @{term "formula"}''*}
(* is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p) *)
-constdefs is_formula_fm :: "i=>i"
+definition is_formula_fm :: "i=>i"
"is_formula_fm(Z) == Forall(Iff(Member(0,succ(Z)), mem_formula_fm(0)))"
lemma is_formula_type [TC]:
@@ -1392,7 +1392,7 @@
2 1 0
upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
is_wfrec(M,MH,mesa,a,z)" *)
-constdefs is_transrec_fm :: "[i, i, i]=>i"
+definition is_transrec_fm :: "[i, i, i]=>i"
"is_transrec_fm(p,a,z) ==
Exists(Exists(Exists(
And(upair_fm(a#+3,a#+3,2),
--- a/src/ZF/Constructible/L_axioms.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/L_axioms.thy Tue Nov 07 19:40:13 2006 +0100
@@ -114,7 +114,7 @@
subsection{*Instantiation of the locale @{text reflection}*}
text{*instances of locale constants*}
-constdefs
+definition
L_F0 :: "[i=>o,i] => i"
"L_F0(P,y) == \<mu> b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
@@ -127,7 +127,7 @@
text{*We must use the meta-existential quantifier; otherwise the reflection
terms become enormous!*}
-constdefs
+definition
L_Reflects :: "[i=>o,[i,i]=>o] => prop" ("(3REFLECTS/ [_,/ _])")
"REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) &
(\<forall>a. Cl(a) --> (\<forall>x \<in> Lset(a). P(x) <-> Q(a,x))))"
@@ -265,28 +265,26 @@
subsubsection{*Some numbers to help write de Bruijn indices*}
-syntax
- "3" :: i ("3")
- "4" :: i ("4")
- "5" :: i ("5")
- "6" :: i ("6")
- "7" :: i ("7")
- "8" :: i ("8")
- "9" :: i ("9")
-
-translations
- "3" == "succ(2)"
- "4" == "succ(3)"
- "5" == "succ(4)"
- "6" == "succ(5)"
- "7" == "succ(6)"
- "8" == "succ(7)"
- "9" == "succ(8)"
+abbreviation
+ digit3 :: i ("3")
+ "3 == succ(2)"
+ digit4 :: i ("4")
+ "4 == succ(3)"
+ digit5 :: i ("5")
+ "5 == succ(4)"
+ digit6 :: i ("6")
+ "6 == succ(5)"
+ digit7 :: i ("7")
+ "7 == succ(6)"
+ digit8 :: i ("8")
+ "8 == succ(7)"
+ digit9 :: i ("9")
+ "9 == succ(8)"
subsubsection{*The Empty Set, Internalized*}
-constdefs empty_fm :: "i=>i"
+definition empty_fm :: "i=>i"
"empty_fm(x) == Forall(Neg(Member(0,succ(x))))"
lemma empty_type [TC]:
@@ -324,7 +322,7 @@
subsubsection{*Unordered Pairs, Internalized*}
-constdefs upair_fm :: "[i,i,i]=>i"
+definition upair_fm :: "[i,i,i]=>i"
"upair_fm(x,y,z) ==
And(Member(x,z),
And(Member(y,z),
@@ -366,7 +364,7 @@
subsubsection{*Ordered pairs, Internalized*}
-constdefs pair_fm :: "[i,i,i]=>i"
+definition pair_fm :: "[i,i,i]=>i"
"pair_fm(x,y,z) ==
Exists(And(upair_fm(succ(x),succ(x),0),
Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0),
@@ -398,7 +396,7 @@
subsubsection{*Binary Unions, Internalized*}
-constdefs union_fm :: "[i,i,i]=>i"
+definition union_fm :: "[i,i,i]=>i"
"union_fm(x,y,z) ==
Forall(Iff(Member(0,succ(z)),
Or(Member(0,succ(x)),Member(0,succ(y)))))"
@@ -429,7 +427,7 @@
subsubsection{*Set ``Cons,'' Internalized*}
-constdefs cons_fm :: "[i,i,i]=>i"
+definition cons_fm :: "[i,i,i]=>i"
"cons_fm(x,y,z) ==
Exists(And(upair_fm(succ(x),succ(x),0),
union_fm(0,succ(y),succ(z))))"
@@ -461,7 +459,7 @@
subsubsection{*Successor Function, Internalized*}
-constdefs succ_fm :: "[i,i]=>i"
+definition succ_fm :: "[i,i]=>i"
"succ_fm(x,y) == cons_fm(x,x,y)"
lemma succ_type [TC]:
@@ -491,7 +489,7 @@
subsubsection{*The Number 1, Internalized*}
(* "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))" *)
-constdefs number1_fm :: "i=>i"
+definition number1_fm :: "i=>i"
"number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))"
lemma number1_type [TC]:
@@ -520,7 +518,7 @@
subsubsection{*Big Union, Internalized*}
(* "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
-constdefs big_union_fm :: "[i,i]=>i"
+definition big_union_fm :: "[i,i]=>i"
"big_union_fm(A,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,succ(succ(A))), Member(1,0)))))"
@@ -600,7 +598,7 @@
subsubsection{*Membership Relation, Internalized*}
-constdefs Memrel_fm :: "[i,i]=>i"
+definition Memrel_fm :: "[i,i]=>i"
"Memrel_fm(A,r) ==
Forall(Iff(Member(0,succ(r)),
Exists(And(Member(0,succ(succ(A))),
@@ -633,7 +631,7 @@
subsubsection{*Predecessor Set, Internalized*}
-constdefs pred_set_fm :: "[i,i,i,i]=>i"
+definition pred_set_fm :: "[i,i,i,i]=>i"
"pred_set_fm(A,x,r,B) ==
Forall(Iff(Member(0,succ(B)),
Exists(And(Member(0,succ(succ(r))),
@@ -671,7 +669,7 @@
(* "is_domain(M,r,z) ==
\<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *)
-constdefs domain_fm :: "[i,i]=>i"
+definition domain_fm :: "[i,i]=>i"
"domain_fm(r,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,succ(succ(r))),
@@ -705,7 +703,7 @@
(* "is_range(M,r,z) ==
\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *)
-constdefs range_fm :: "[i,i]=>i"
+definition range_fm :: "[i,i]=>i"
"range_fm(r,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,succ(succ(r))),
@@ -740,7 +738,7 @@
(* "is_field(M,r,z) ==
\<exists>dr[M]. is_domain(M,r,dr) &
(\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *)
-constdefs field_fm :: "[i,i]=>i"
+definition field_fm :: "[i,i]=>i"
"field_fm(r,z) ==
Exists(And(domain_fm(succ(r),0),
Exists(And(range_fm(succ(succ(r)),0),
@@ -775,7 +773,7 @@
(* "image(M,r,A,z) ==
\<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *)
-constdefs image_fm :: "[i,i,i]=>i"
+definition image_fm :: "[i,i,i]=>i"
"image_fm(r,A,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,succ(succ(r))),
@@ -810,7 +808,7 @@
(* "pre_image(M,r,A,z) ==
\<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *)
-constdefs pre_image_fm :: "[i,i,i]=>i"
+definition pre_image_fm :: "[i,i,i]=>i"
"pre_image_fm(r,A,z) ==
Forall(Iff(Member(0,succ(z)),
Exists(And(Member(0,succ(succ(r))),
@@ -846,7 +844,7 @@
(* "fun_apply(M,f,x,y) ==
(\<exists>xs[M]. \<exists>fxs[M].
upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *)
-constdefs fun_apply_fm :: "[i,i,i]=>i"
+definition fun_apply_fm :: "[i,i,i]=>i"
"fun_apply_fm(f,x,y) ==
Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1),
And(image_fm(succ(succ(f)), 1, 0),
@@ -881,7 +879,7 @@
(* "is_relation(M,r) ==
(\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *)
-constdefs relation_fm :: "i=>i"
+definition relation_fm :: "i=>i"
"relation_fm(r) ==
Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))"
@@ -913,7 +911,7 @@
(* "is_function(M,r) ==
\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'" *)
-constdefs function_fm :: "i=>i"
+definition function_fm :: "i=>i"
"function_fm(r) ==
Forall(Forall(Forall(Forall(Forall(
Implies(pair_fm(4,3,1),
@@ -950,7 +948,7 @@
is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
(\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))" *)
-constdefs typed_function_fm :: "[i,i,i]=>i"
+definition typed_function_fm :: "[i,i,i]=>i"
"typed_function_fm(A,B,r) ==
And(function_fm(r),
And(relation_fm(r),
@@ -1009,7 +1007,7 @@
(\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
xy \<in> s & yz \<in> r)" *)
-constdefs composition_fm :: "[i,i,i]=>i"
+definition composition_fm :: "[i,i,i]=>i"
"composition_fm(r,s,t) ==
Forall(Iff(Member(0,succ(t)),
Exists(Exists(Exists(Exists(Exists(
@@ -1048,7 +1046,7 @@
typed_function(M,A,B,f) &
(\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')" *)
-constdefs injection_fm :: "[i,i,i]=>i"
+definition injection_fm :: "[i,i,i]=>i"
"injection_fm(A,B,f) ==
And(typed_function_fm(A,B,f),
Forall(Forall(Forall(Forall(Forall(
@@ -1088,7 +1086,7 @@
"surjection(M,A,B,f) ==
typed_function(M,A,B,f) &
(\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))" *)
-constdefs surjection_fm :: "[i,i,i]=>i"
+definition surjection_fm :: "[i,i,i]=>i"
"surjection_fm(A,B,f) ==
And(typed_function_fm(A,B,f),
Forall(Implies(Member(0,succ(B)),
@@ -1124,7 +1122,7 @@
(* bijection :: "[i=>o,i,i,i] => o"
"bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *)
-constdefs bijection_fm :: "[i,i,i]=>i"
+definition bijection_fm :: "[i,i,i]=>i"
"bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))"
lemma bijection_type [TC]:
@@ -1156,7 +1154,7 @@
(* "restriction(M,r,A,z) ==
\<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" *)
-constdefs restriction_fm :: "[i,i,i]=>i"
+definition restriction_fm :: "[i,i,i]=>i"
"restriction_fm(r,A,z) ==
Forall(Iff(Member(0,succ(z)),
And(Member(0,succ(r)),
@@ -1197,7 +1195,7 @@
pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
*)
-constdefs order_isomorphism_fm :: "[i,i,i,i,i]=>i"
+definition order_isomorphism_fm :: "[i,i,i,i,i]=>i"
"order_isomorphism_fm(A,r,B,s,f) ==
And(bijection_fm(A,B,f),
Forall(Implies(Member(0,succ(A)),
@@ -1244,7 +1242,7 @@
ordinal(M,a) & ~ empty(M,a) &
(\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))" *)
-constdefs limit_ordinal_fm :: "i=>i"
+definition limit_ordinal_fm :: "i=>i"
"limit_ordinal_fm(x) ==
And(ordinal_fm(x),
And(Neg(empty_fm(x)),
@@ -1280,7 +1278,7 @@
(* "finite_ordinal(M,a) ==
ordinal(M,a) & ~ limit_ordinal(M,a) &
(\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))" *)
-constdefs finite_ordinal_fm :: "i=>i"
+definition finite_ordinal_fm :: "i=>i"
"finite_ordinal_fm(x) ==
And(ordinal_fm(x),
And(Neg(limit_ordinal_fm(x)),
@@ -1313,7 +1311,7 @@
subsubsection{*Omega: The Set of Natural Numbers*}
(* omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x)) *)
-constdefs omega_fm :: "i=>i"
+definition omega_fm :: "i=>i"
"omega_fm(x) ==
And(limit_ordinal_fm(x),
Forall(Implies(Member(0,succ(x)),
--- a/src/ZF/Constructible/MetaExists.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/MetaExists.thy Tue Nov 07 19:40:13 2006 +0100
@@ -10,12 +10,12 @@
text{*Allows quantification over any term having sort @{text logic}. Used to
quantify over classes. Yields a proposition rather than a FOL formula.*}
-constdefs
+definition
ex :: "(('a::{}) => prop) => prop" (binder "?? " 0)
"ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
-syntax (xsymbols)
- "?? " :: "[idts, o] => o" ("(3\<Or>_./ _)" [0, 0] 0)
+notation (xsymbols)
+ ex (binder "\<Or>" 0)
lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
proof (unfold ex_def)
--- a/src/ZF/Constructible/Normal.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Normal.thy Tue Nov 07 19:40:13 2006 +0100
@@ -18,7 +18,7 @@
subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}
-constdefs
+definition
Closed :: "(i=>o) => o"
"Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"
@@ -200,7 +200,7 @@
subsection {*Normal Functions*}
-constdefs
+definition
mono_le_subset :: "(i=>i) => o"
"mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"
@@ -372,7 +372,7 @@
only if @{text F} is continuous: succ is not bounded above by any
normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
*}
-constdefs
+definition
normalize :: "[i=>i, i] => i"
"normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"
@@ -424,12 +424,12 @@
text {*This is the well-known transfinite enumeration of the cardinal
numbers.*}
-constdefs
+definition
Aleph :: "i => i"
"Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
-syntax (xsymbols)
- Aleph :: "i => i" ("\<aleph>_" [90] 90)
+notation (xsymbols)
+ Aleph ("\<aleph>_" [90] 90)
lemma Card_Aleph [simp, intro]:
"Ord(a) ==> Card(Aleph(a))"
@@ -458,4 +458,3 @@
done
end
-
--- a/src/ZF/Constructible/Rank.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Rank.thy Tue Nov 07 19:40:13 2006 +0100
@@ -136,7 +136,7 @@
done
-constdefs
+definition
obase :: "[i=>o,i,i] => i"
--{*the domain of @{text om}, eventually shown to equal @{text A}*}
@@ -414,7 +414,7 @@
subsubsection{*Ordinal Addition*}
(*FIXME: update to use new techniques!!*)
-constdefs
+definition
(*This expresses ordinal addition in the language of ZF. It also
provides an abbreviation that can be used in the instance of strong
replacement below. Here j is used to define the relation, namely
@@ -725,7 +725,7 @@
text{*This function, defined using replacement, is a rank function for
well-founded relations within the class M.*}
-constdefs
+definition
wellfoundedrank :: "[i=>o,i,i] => i"
"wellfoundedrank(M,r,A) ==
{p. x\<in>A, \<exists>y[M]. \<exists>f[M].
--- a/src/ZF/Constructible/Rec_Separation.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Rec_Separation.thy Tue Nov 07 19:40:13 2006 +0100
@@ -30,7 +30,7 @@
(\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
fun_apply(M,f,j,fj) & successor(M,j,sj) &
fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
-constdefs rtran_closure_mem_fm :: "[i,i,i]=>i"
+definition rtran_closure_mem_fm :: "[i,i,i]=>i"
"rtran_closure_mem_fm(A,r,p) ==
Exists(Exists(Exists(
And(omega_fm(2),
@@ -87,7 +87,7 @@
(* "rtran_closure(M,r,s) ==
\<forall>A[M]. is_field(M,r,A) -->
(\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *)
-constdefs rtran_closure_fm :: "[i,i]=>i"
+definition rtran_closure_fm :: "[i,i]=>i"
"rtran_closure_fm(r,s) ==
Forall(Implies(field_fm(succ(r),0),
Forall(Iff(Member(0,succ(succ(s))),
@@ -121,7 +121,7 @@
(* "tran_closure(M,r,t) ==
\<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *)
-constdefs tran_closure_fm :: "[i,i]=>i"
+definition tran_closure_fm :: "[i,i]=>i"
"tran_closure_fm(r,s) ==
Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))"
@@ -293,7 +293,7 @@
(* "is_nth(M,n,l,Z) ==
\<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *)
-constdefs nth_fm :: "[i,i,i]=>i"
+definition nth_fm :: "[i,i,i]=>i"
"nth_fm(n,l,Z) ==
Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0),
hd_fm(0,succ(Z))))"
--- a/src/ZF/Constructible/Relative.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Relative.thy Tue Nov 07 19:40:13 2006 +0100
@@ -9,7 +9,7 @@
subsection{* Relativized versions of standard set-theoretic concepts *}
-constdefs
+definition
empty :: "[i=>o,i] => o"
"empty(M,z) == \<forall>x[M]. x \<notin> z"
@@ -236,7 +236,7 @@
subsection {*The relativized ZF axioms*}
-constdefs
+definition
extensionality :: "(i=>o) => o"
"extensionality(M) ==
@@ -441,7 +441,7 @@
text{*More constants, for order types*}
-constdefs
+definition
order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
"order_isomorphism(M,A,r,B,s,f) ==
@@ -712,7 +712,7 @@
subsubsection {*Absoluteness for @{term Lambda}*}
-constdefs
+definition
is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
"is_lambda(M, A, is_b, z) ==
\<forall>p[M]. p \<in> z <->
@@ -893,7 +893,7 @@
(\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x))
then 1 else 0)"
- constdefs
+ definition
natnumber :: "[i=>o,i,i] => o"
"natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
@@ -1312,7 +1312,7 @@
subsection{*Relativization and Absoluteness for Boolean Operators*}
-constdefs
+definition
is_bool_of_o :: "[i=>o, o, i] => o"
"is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))"
@@ -1365,7 +1365,7 @@
subsection{*Relativization and Absoluteness for List Operators*}
-constdefs
+definition
is_Nil :: "[i=>o, i] => o"
--{* because @{term "[] \<equiv> Inl(0)"}*}
@@ -1390,7 +1390,7 @@
by (simp add: is_Cons_def Cons_def)
-constdefs
+definition
quasilist :: "i => o"
"quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"
--- a/src/ZF/Constructible/Satisfies_absolute.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Satisfies_absolute.thy Tue Nov 07 19:40:13 2006 +0100
@@ -17,7 +17,7 @@
2 1 0
is_formula_N(M,n,formula_n) & p \<notin> formula_n &
successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn" *)
-constdefs depth_fm :: "[i,i]=>i"
+definition depth_fm :: "[i,i]=>i"
"depth_fm(p,n) ==
Exists(Exists(Exists(
And(formula_N_fm(n#+3,1),
@@ -66,7 +66,7 @@
is_Nand(M,x,y,v) --> is_c(x,y,z)) &
(\<forall>x[M]. x\<in>formula --> is_Forall(M,x,v) --> is_d(x,z))" *)
-constdefs formula_case_fm :: "[i, i, i, i, i, i]=>i"
+definition formula_case_fm :: "[i, i, i, i, i, i]=>i"
"formula_case_fm(is_a, is_b, is_c, is_d, v, z) ==
And(Forall(Forall(Implies(finite_ordinal_fm(1),
Implies(finite_ordinal_fm(0),
@@ -173,7 +173,7 @@
subsection {*Absoluteness for the Function @{term satisfies}*}
-constdefs
+definition
is_depth_apply :: "[i=>o,i,i,i] => o"
--{*Merely a useful abbreviation for the sequel.*}
"is_depth_apply(M,h,p,z) ==
@@ -193,7 +193,7 @@
text{*These constants let us instantiate the parameters @{term a}, @{term b},
@{term c}, @{term d}, etc., of the locale @{text Formula_Rec}.*}
-constdefs
+definition
satisfies_a :: "[i,i,i]=>i"
"satisfies_a(A) ==
\<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env))"
@@ -504,7 +504,7 @@
2 1 0
finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z) *)
-constdefs depth_apply_fm :: "[i,i,i]=>i"
+definition depth_apply_fm :: "[i,i,i]=>i"
"depth_apply_fm(h,p,z) ==
Exists(Exists(Exists(
And(finite_ordinal_fm(2),
@@ -547,7 +547,7 @@
is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z),
zz) *)
-constdefs satisfies_is_a_fm :: "[i,i,i,i]=>i"
+definition satisfies_is_a_fm :: "[i,i,i,i]=>i"
"satisfies_is_a_fm(A,x,y,z) ==
Forall(
Implies(is_list_fm(succ(A),0),
@@ -598,7 +598,7 @@
\<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
zz) *)
-constdefs satisfies_is_b_fm :: "[i,i,i,i]=>i"
+definition satisfies_is_b_fm :: "[i,i,i,i]=>i"
"satisfies_is_b_fm(A,x,y,z) ==
Forall(
Implies(is_list_fm(succ(A),0),
@@ -647,7 +647,7 @@
(\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
zz) *)
-constdefs satisfies_is_c_fm :: "[i,i,i,i,i]=>i"
+definition satisfies_is_c_fm :: "[i,i,i,i,i]=>i"
"satisfies_is_c_fm(A,h,p,q,zz) ==
Forall(
Implies(is_list_fm(succ(A),0),
@@ -700,7 +700,7 @@
z),
zz) *)
-constdefs satisfies_is_d_fm :: "[i,i,i,i]=>i"
+definition satisfies_is_d_fm :: "[i,i,i,i]=>i"
"satisfies_is_d_fm(A,h,p,zz) ==
Forall(
Implies(is_list_fm(succ(A),0),
@@ -754,7 +754,7 @@
satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
zz) *)
-constdefs satisfies_MH_fm :: "[i,i,i,i]=>i"
+definition satisfies_MH_fm :: "[i,i,i,i]=>i"
"satisfies_MH_fm(A,u,f,zz) ==
Forall(
Implies(is_formula_fm(0),
--- a/src/ZF/Constructible/WF_absolute.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/WF_absolute.thy Tue Nov 07 19:40:13 2006 +0100
@@ -9,7 +9,7 @@
subsection{*Transitive closure without fixedpoints*}
-constdefs
+definition
rtrancl_alt :: "[i,i]=>i"
"rtrancl_alt(A,r) ==
{p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
@@ -59,7 +59,7 @@
intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt)
-constdefs
+definition
rtran_closure_mem :: "[i=>o,i,i,i] => o"
--{*The property of belonging to @{text "rtran_closure(r)"}*}
--- a/src/ZF/Constructible/WFrec.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/WFrec.thy Tue Nov 07 19:40:13 2006 +0100
@@ -271,7 +271,7 @@
subsection{*Relativization of the ZF Predicate @{term is_recfun}*}
-constdefs
+definition
M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
"M_is_recfun(M,MH,r,a,f) ==
\<forall>z[M]. z \<in> f <->
--- a/src/ZF/Constructible/Wellorderings.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Wellorderings.thy Tue Nov 07 19:40:13 2006 +0100
@@ -16,7 +16,7 @@
subsection{*Wellorderings*}
-constdefs
+definition
irreflexive :: "[i=>o,i,i]=>o"
"irreflexive(M,A,r) == \<forall>x[M]. x\<in>A --> <x,x> \<notin> r"
--- a/src/ZF/ex/Commutation.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/ex/Commutation.thy Tue Nov 07 19:40:13 2006 +0100
@@ -4,41 +4,41 @@
Copyright 1995 TU Muenchen
Commutation theory for proving the Church Rosser theorem
- ported from Isabelle/HOL by Sidi Ould Ehmety
+ ported from Isabelle/HOL by Sidi Ould Ehmety
*)
theory Commutation imports Main begin
-constdefs
+definition
square :: "[i, i, i, i] => o"
- "square(r,s,t,u) ==
- (\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
+ "square(r,s,t,u) ==
+ (\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
commute :: "[i, i] => o"
- "commute(r,s) == square(r,s,s,r)"
+ "commute(r,s) == square(r,s,s,r)"
diamond :: "i=>o"
- "diamond(r) == commute(r, r)"
+ "diamond(r) == commute(r, r)"
strip :: "i=>o"
- "strip(r) == commute(r^*, r)"
+ "strip(r) == commute(r^*, r)"
Church_Rosser :: "i => o"
- "Church_Rosser(r) == (\<forall>x y. <x,y> \<in> (r Un converse(r))^* -->
- (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
+ "Church_Rosser(r) == (\<forall>x y. <x,y> \<in> (r Un converse(r))^* -->
+ (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
confluent :: "i=>o"
- "confluent(r) == diamond(r^*)"
+ "confluent(r) == diamond(r^*)"
lemma square_sym: "square(r,s,t,u) ==> square(s,r,u,t)"
-by (unfold square_def, blast)
+ unfolding square_def by blast
lemma square_subset: "[| square(r,s,t,u); t \<subseteq> t' |] ==> square(r,s,t',u)"
-by (unfold square_def, blast)
+ unfolding square_def by blast
-lemma square_rtrancl [rule_format]:
- "square(r,s,s,t) --> field(s)<=field(t) --> square(r^*,s,s,t^*)"
+lemma square_rtrancl:
+ "square(r,s,s,t) ==> field(s)<=field(t) ==> square(r^*,s,s,t^*)"
apply (unfold square_def, clarify)
apply (erule rtrancl_induct)
apply (blast intro: rtrancl_refl)
@@ -46,23 +46,22 @@
done
(* A special case of square_rtrancl_on *)
-lemma diamond_strip:
- "diamond(r) ==> strip(r)"
+lemma diamond_strip:
+ "diamond(r) ==> strip(r)"
apply (unfold diamond_def commute_def strip_def)
apply (rule square_rtrancl, simp_all)
done
(*** commute ***)
-lemma commute_sym:
- "commute(r,s) ==> commute(s,r)"
-by (unfold commute_def, blast intro: square_sym)
+lemma commute_sym: "commute(r,s) ==> commute(s,r)"
+ unfolding commute_def by (blast intro: square_sym)
-lemma commute_rtrancl [rule_format]:
- "commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)"
-apply (unfold commute_def, clarify)
+lemma commute_rtrancl:
+ "commute(r,s) ==> field(r)=field(s) ==> commute(r^*,s^*)"
+apply (unfold commute_def)
apply (rule square_rtrancl)
-apply (rule square_sym [THEN square_rtrancl, THEN square_sym])
+apply (rule square_sym [THEN square_rtrancl, THEN square_sym])
apply (simp_all add: rtrancl_field)
done
@@ -77,20 +76,20 @@
done
lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)"
-by (unfold commute_def square_def, blast)
+ unfolding commute_def square_def by blast
-lemma diamond_Un:
+lemma diamond_Un:
"[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r Un s)"
-by (unfold diamond_def, blast intro: commute_Un commute_sym)
+ unfolding diamond_def by (blast intro: commute_Un commute_sym)
-lemma diamond_confluent:
+lemma diamond_confluent:
"diamond(r) ==> confluent(r)"
apply (unfold diamond_def confluent_def)
apply (erule commute_rtrancl, simp)
done
-lemma confluent_Un:
- "[| confluent(r); confluent(s); commute(r^*, s^*);
+lemma confluent_Un:
+ "[| confluent(r); confluent(s); commute(r^*, s^*);
relation(r); relation(s) |] ==> confluent(r Un s)"
apply (unfold confluent_def)
apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
@@ -98,7 +97,7 @@
done
-lemma diamond_to_confluence:
+lemma diamond_to_confluence:
"[| diamond(r); s \<subseteq> r; r<= s^* |] ==> confluent(s)"
apply (drule rtrancl_subset [symmetric], assumption)
apply (simp_all add: confluent_def)
@@ -108,9 +107,9 @@
(*** Church_Rosser ***)
-lemma Church_Rosser1:
+lemma Church_Rosser1:
"Church_Rosser(r) ==> confluent(r)"
-apply (unfold confluent_def Church_Rosser_def square_def
+apply (unfold confluent_def Church_Rosser_def square_def
commute_def diamond_def, auto)
apply (drule converseI)
apply (simp (no_asm_use) add: rtrancl_converse [symmetric])
@@ -121,9 +120,9 @@
done
-lemma Church_Rosser2:
+lemma Church_Rosser2:
"confluent(r) ==> Church_Rosser(r)"
-apply (unfold confluent_def Church_Rosser_def square_def
+apply (unfold confluent_def Church_Rosser_def square_def
commute_def diamond_def, auto)
apply (frule fieldI1)
apply (simp add: rtrancl_field)
@@ -134,6 +133,6 @@
lemma Church_Rosser: "Church_Rosser(r) <-> confluent(r)"
-by (blast intro: Church_Rosser1 Church_Rosser2)
+ by (blast intro: Church_Rosser1 Church_Rosser2)
-end
+end
--- a/src/ZF/ex/Group.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/ex/Group.thy Tue Nov 07 19:40:13 2006 +0100
@@ -20,22 +20,22 @@
one :: i ("\<one>\<index>")
*)
-constdefs
+definition
carrier :: "i => i"
- "carrier(M) == fst(M)"
+ "carrier(M) == fst(M)"
mmult :: "[i, i, i] => i" (infixl "\<cdot>\<index>" 70)
- "mmult(M,x,y) == fst(snd(M)) ` <x,y>"
+ "mmult(M,x,y) == fst(snd(M)) ` <x,y>"
one :: "i => i" ("\<one>\<index>")
- "one(M) == fst(snd(snd(M)))"
+ "one(M) == fst(snd(snd(M)))"
update_carrier :: "[i,i] => i"
- "update_carrier(M,A) == <A,snd(M)>"
+ "update_carrier(M,A) == <A,snd(M)>"
-constdefs (structure G)
+definition
m_inv :: "i => i => i" ("inv\<index> _" [81] 80)
- "inv x == (THE y. y \<in> carrier(G) & y \<cdot> x = \<one> & x \<cdot> y = \<one>)"
+ "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier(G) & y \<cdot>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub> & x \<cdot>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub>)"
locale monoid = struct G +
assumes m_closed [intro, simp]:
@@ -294,7 +294,7 @@
subsection {* Direct Products *}
-constdefs
+definition
DirProdGroup :: "[i,i] => i" (infixr "\<Otimes>" 80)
"G \<Otimes> H == <carrier(G) \<times> carrier(H),
(\<lambda><<g,h>, <g', h'>>
@@ -332,7 +332,7 @@
subsection {* Isomorphisms *}
-constdefs
+definition
hom :: "[i,i] => i"
"hom(G,H) ==
{h \<in> carrier(G) -> carrier(H).
@@ -358,7 +358,7 @@
subsection {* Isomorphisms *}
-constdefs
+definition
iso :: "[i,i] => i" (infixr "\<cong>" 60)
"G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
@@ -478,7 +478,7 @@
subsection {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
-constdefs
+definition
BijGroup :: "i=>i"
"BijGroup(S) ==
<bij(S,S),
@@ -513,7 +513,7 @@
by (simp add: iso_def)
-constdefs
+definition
auto :: "i=>i"
"auto(G) == iso(G,G)"
@@ -551,32 +551,28 @@
subsection{*Cosets and Quotient Groups*}
-constdefs (structure G)
+definition
r_coset :: "[i,i,i] => i" (infixl "#>\<index>" 60)
- "H #> a == \<Union>h\<in>H. {h \<cdot> a}"
+ "H #>\<^bsub>G\<^esub> a == \<Union>h\<in>H. {h \<cdot>\<^bsub>G\<^esub> a}"
l_coset :: "[i,i,i] => i" (infixl "<#\<index>" 60)
- "a <# H == \<Union>h\<in>H. {a \<cdot> h}"
+ "a <#\<^bsub>G\<^esub> H == \<Union>h\<in>H. {a \<cdot>\<^bsub>G\<^esub> h}"
RCOSETS :: "[i,i] => i" ("rcosets\<index> _" [81] 80)
- "rcosets H == \<Union>a\<in>carrier(G). {H #> a}"
+ "rcosets\<^bsub>G\<^esub> H == \<Union>a\<in>carrier(G). {H #>\<^bsub>G\<^esub> a}"
set_mult :: "[i,i,i] => i" (infixl "<#>\<index>" 60)
- "H <#> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot> k}"
+ "H <#>\<^bsub>G\<^esub> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot>\<^bsub>G\<^esub> k}"
SET_INV :: "[i,i] => i" ("set'_inv\<index> _" [81] 80)
- "set_inv H == \<Union>h\<in>H. {inv h}"
+ "set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
locale normal = subgroup + group +
assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
-
-syntax
- "@normal" :: "[i,i] => i" (infixl "\<lhd>" 60)
-
-translations
- "H \<lhd> G" == "normal(H,G)"
+notation
+ normal (infixl "\<lhd>" 60)
subsection {*Basic Properties of Cosets*}
@@ -836,9 +832,9 @@
subsubsection{*Two distinct right cosets are disjoint*}
-constdefs (structure G)
+definition
r_congruent :: "[i,i] => i" ("rcong\<index> _" [60] 60)
- "rcong H == {<x,y> \<in> carrier(G) * carrier(G). inv x \<cdot> y \<in> H}"
+ "rcong\<^bsub>G\<^esub> H == {<x,y> \<in> carrier(G) * carrier(G). inv\<^bsub>G\<^esub> x \<cdot>\<^bsub>G\<^esub> y \<in> H}"
lemma (in subgroup) equiv_rcong:
@@ -903,7 +899,7 @@
subsection {*Order of a Group and Lagrange's Theorem*}
-constdefs
+definition
order :: "i => i"
"order(S) == |carrier(S)|"
@@ -975,11 +971,11 @@
subsection {*Quotient Groups: Factorization of a Group*}
-constdefs (structure G)
+definition
FactGroup :: "[i,i] => i" (infixl "Mod" 65)
--{*Actually defined for groups rather than monoids*}
"G Mod H ==
- <rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#> K2, H, 0>"
+ <rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>"
lemma (in normal) setmult_closed:
"\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
@@ -1038,7 +1034,7 @@
text{*The quotient by the kernel of a homomorphism is isomorphic to the
range of that homomorphism.*}
-constdefs
+definition
kernel :: "[i,i,i] => i"
--{*the kernel of a homomorphism*}
"kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}";
--- a/src/ZF/ex/Ramsey.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/ex/Ramsey.thy Tue Nov 07 19:40:13 2006 +0100
@@ -27,7 +27,8 @@
*)
theory Ramsey imports Main begin
-constdefs
+
+definition
Symmetric :: "i=>o"
"Symmetric(E) == (\<forall>x y. <x,y>:E --> <y,x>:E)"
--- a/src/ZF/ex/Ring.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/ex/Ring.thy Tue Nov 07 19:40:13 2006 +0100
@@ -13,15 +13,15 @@
zero :: i ("\<zero>\<index>")
*)
-constdefs
+definition
add_field :: "i => i"
- "add_field(M) == fst(snd(snd(snd(M))))"
+ "add_field(M) = fst(snd(snd(snd(M))))"
ring_add :: "[i, i, i] => i" (infixl "\<oplus>\<index>" 65)
- "ring_add(M,x,y) == add_field(M) ` <x,y>"
+ "ring_add(M,x,y) = add_field(M) ` <x,y>"
zero :: "i => i" ("\<zero>\<index>")
- "zero(M) == fst(snd(snd(snd(snd(M)))))"
+ "zero(M) = fst(snd(snd(snd(snd(M)))))"
lemma add_field_eq [simp]: "add_field(<C,M,I,A,z>) = A"
@@ -36,12 +36,12 @@
text {* Derived operations. *}
-constdefs (structure R)
+definition
a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80)
"a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65)
- "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y == x \<oplus> (\<ominus> y)"
+ "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus>\<^bsub>R\<^esub> y = x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
locale abelian_monoid = struct G +
assumes a_comm_monoid:
@@ -170,8 +170,10 @@
The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
*}
-lemma (in ring) l_null [simp]:
- "x \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>"
+context ring
+begin
+
+lemma l_null [simp]: "x \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>"
proof -
assume R: "x \<in> carrier(R)"
then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x"
@@ -181,8 +183,7 @@
with R show ?thesis by (simp del: r_zero)
qed
-lemma (in ring) r_null [simp]:
- "x \<in> carrier(R) \<Longrightarrow> x \<cdot> \<zero> = \<zero>"
+lemma r_null [simp]: "x \<in> carrier(R) \<Longrightarrow> x \<cdot> \<zero> = \<zero>"
proof -
assume R: "x \<in> carrier(R)"
then have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> (\<zero> \<oplus> \<zero>)"
@@ -192,7 +193,7 @@
with R show ?thesis by (simp del: r_zero)
qed
-lemma (in ring) l_minus:
+lemma l_minus:
"\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> \<ominus> x \<cdot> y = \<ominus> (x \<cdot> y)"
proof -
assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
@@ -203,7 +204,7 @@
with R show ?thesis by (simp add: a_assoc r_neg)
qed
-lemma (in ring) r_minus:
+lemma r_minus:
"\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<cdot> \<ominus> y = \<ominus> (x \<cdot> y)"
proof -
assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
@@ -214,16 +215,18 @@
with R show ?thesis by (simp add: a_assoc r_neg)
qed
-lemma (in ring) minus_eq:
+lemma minus_eq:
"\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y = x \<oplus> \<ominus> y"
by (simp only: minus_def)
+end
+
subsection {* Morphisms *}
-constdefs
+definition
ring_hom :: "[i,i] => i"
- "ring_hom(R,S) ==
+ "ring_hom(R,S) ==
{h \<in> carrier(R) -> carrier(S).
(\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) -->
h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) &
@@ -287,4 +290,3 @@
done
end
-