# HG changeset patch # User wenzelm # Date 1162924813 -3600 # Node ID 5a5c8ea5f66a731128f4af7c028420d374cba591 # Parent faacfd4392b57fac5974f0ea4f65a45a4911b9a5 tuned specifications; diff -r faacfd4392b5 -r 5a5c8ea5f66a src/HOL/NumberTheory/Gauss.thy --- 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 \ ((p - 1) div 2)}" - defines B_def: "B == (%x. x * a) ` A" - defines C_def: "C == (StandardRes p) ` B" - defines D_def: "D == C \ {x. x \ ((p - 1) div 2)}" - defines E_def: "E == C \ {x. ((p - 1) div 2) < x}" - defines F_def: "F == (%x. (p - x)) ` E" +definition + A :: "int set" + "A = {(x::int). 0 < x & x \ ((p - 1) div 2)}" + + B :: "int set" + "B = (%x. x * a) ` A" + + C :: "int set" + "C = StandardRes p ` B" + + D :: "int set" + "D = C \ {x. x \ ((p - 1) div 2)}" + + E :: "int set" + "E = C \ {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 \ zOdd" +lemma p_odd: "p \ 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 \ (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 \ 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 \ (p - 1) div 2} \ {x. 0 \ 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 \ E" +lemma C_eq: "C = D \ 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 \ A ==> ~[x = 0](mod p)" +lemma A_ncong_p: "x \ 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 \ A ==> 0 < x" +lemma A_greater_zero: "x \ A ==> 0 < x" by (auto simp add: A_def) -lemma (in GAUSS) B_ncong_p: "x \ B ==> ~[x = 0](mod p)" +lemma B_ncong_p: "x \ 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 \ B ==> 0 < x" +lemma B_greater_zero: "x \ 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 \ C ==> ~[x = 0](mod p)" +lemma C_ncong_p: "x \ 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 \ C ==> 0 < y" +lemma C_greater_zero: "y \ 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 \ D ==> ~[x = 0](mod p)" +lemma D_ncong_p: "x \ D ==> ~[x = 0](mod p)" by (auto simp add: D_def C_ncong_p) -lemma (in GAUSS) E_ncong_p: "x \ E ==> ~[x = 0](mod p)" +lemma E_ncong_p: "x \ E ==> ~[x = 0](mod p)" by (auto simp add: E_def C_ncong_p) -lemma (in GAUSS) F_ncong_p: "x \ F ==> ~[x = 0](mod p)" +lemma F_ncong_p: "x \ F ==> ~[x = 0](mod p)" apply (auto simp add: F_def) proof - fix x assume a: "x \ 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 \ {x. 0 < x & x \ ((p - 1) div 2)}" +lemma F_subset: "F \ {x. 0 < x & x \ ((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 \ {x. 0 < x & x \ ((p - 1) div 2)}" +lemma D_subset: "D \ {x. 0 < x & x \ ((p - 1) div 2)}" by (auto simp add: D_def C_greater_zero) -lemma (in GAUSS) F_eq: "F = {x. \y \ A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}" +lemma F_eq: "F = {x. \y \ 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. \y \ A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \ (p - 1) div 2)}" +lemma D_eq: "D = {x. \y \ A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \ (p - 1) div 2)}" by (auto simp add: D_def C_def B_def A_def) -lemma (in GAUSS) D_leq: "x \ D ==> x \ (p - 1) div 2" +lemma D_leq: "x \ D ==> x \ (p - 1) div 2" by (auto simp add: D_eq) -lemma (in GAUSS) F_ge: "x \ F ==> x \ (p - 1) div 2" +lemma F_ge: "x \ F ==> x \ (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: "\x \ A. zgcd(x, p) = 1" +lemma all_A_relprime: "\x \ 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 \ E = {}" +lemma D_E_disj: "D \ 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 \ D) \ A" +lemma F_Un_D_subset: "(F \ D) \ 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 \ D) = {}" +lemma F_D_disj: "(F \ 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 \ D) = nat ((p - 1) div 2)" - apply (insert F_D_disj finite_F finite_D) +lemma F_Un_D_card: "card (F \ D) = nat ((p - 1) div 2)" proof - have "card (F \ 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 \ D = A" +lemma F_Un_D_eq_A: "F \ 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 diff -r faacfd4392b5 -r 5a5c8ea5f66a src/HOL/NumberTheory/Quadratic_Reciprocity.thy --- 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 \ 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 \ zOdd ==> +lemma QRLemma4: "a \ zOdd ==> (setsum (%x. ((x * a) div p)) A \ zEven) = (int(card E): zEven)" proof - assume a_odd: "a \ zOdd" @@ -108,7 +111,7 @@ by (auto simp only: even_diff [symmetric]) qed -lemma (in GAUSS) QRLemma5: "a \ zOdd ==> +lemma QRLemma5: "a \ zOdd ==> (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))" proof - assume "a \ zOdd" @@ -138,6 +141,8 @@ finally show ?thesis . qed +end + lemma MainQRLemma: "[| a \ zOdd; 0 < a; ~([a = 0] (mod p)); zprime p; 2 < p; A = {x. 0 < x & x \ (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 \ q" +begin - defines P_set_def: "P_set == {x. 0 < x & x \ ((p - 1) div 2) }" - defines Q_set_def: "Q_set == {x. 0 < x & x \ ((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 \ (q * j) div p) }" - defines f2_def: "f2 j == { (x, j1). (x, j1):S & j1 = j & - (x \ (p * j) div q) }" +definition + P_set :: "int set" + "P_set = {x. 0 < x & x \ ((p - 1) div 2) }" + + Q_set :: "int set" + "Q_set = {x. 0 < x & x \ ((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 \ (q * j) div p) }" + + f2 :: "int => (int * int) set" + "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \ (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 \ p - 1" by arith + from p_g_2 have "2 \ p - 1" by arith then have "2 div 2 \ (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 \ q - 1" by arith + from q_g_2 have "2 \ q - 1" by arith then have "2 div 2 \ (q - 1) div 2" by (rule zdiv_mono1, auto) then show ?thesis by auto qed -lemma (in QRTEMP) pb_neq_qa: "[|1 \ b; b \ (q - 1) div 2 |] ==> +lemma pb_neq_qa: "[|1 \ b; b \ (q - 1) div 2 |] ==> (p * b \ q * a)" proof assume "p * b = q * a" and "1 \ b" and "b \ (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 \ 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 \ 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 \ S2 = {}" +lemma S1_Int_S2_prop: "S1 \ S2 = {}" by (auto simp add: S1_def S2_def) -lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \ S2" +lemma S1_Union_S2_prop: "S = S1 \ 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 \ (p - 1) div 2; +lemma aux1a: "[| 0 < a; a \ (p - 1) div 2; 0 < b; b \ (q - 1) div 2 |] ==> (p * b < q * a) = (b \ q * a div p)" proof - @@ -327,7 +337,7 @@ ultimately show ?thesis .. qed -lemma (in QRTEMP) aux1b: "[| 0 < a; a \ (p - 1) div 2; +lemma aux1b: "[| 0 < a; a \ (p - 1) div 2; 0 < b; b \ (q - 1) div 2 |] ==> (q * a < p * b) = (a \ 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 \ (q - 1) div 2" proof- @@ -390,7 +402,10 @@ using prems by auto qed -lemma (in QRTEMP) aux3a: "\j \ P_set. int (card (f1 j)) = (q * j) div p" +context QRTEMP +begin + +lemma aux3a: "\j \ P_set. int (card (f1 j)) = (q * j) div p" proof fix j assume j_fact: "j \ P_set" @@ -422,7 +437,7 @@ by (auto simp add: mult_le_cancel_left) with p_g_2 have "q * j div p \ q * ((p - 1) div 2) div p" by (auto simp add: zdiv_mono1) - also from prems have "... \ (q - 1) div 2" + also from prems P_set_def have "... \ (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: "\j \ Q_set. int (card (f2 j)) = (p * j) div q" +lemma aux3b: "\j \ Q_set. int (card (f2 j)) = (p * j) div q" proof fix j assume j_fact: "j \ 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 "\x \ 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 "\x \ 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 \ 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 \ zOdd; zprime p; q \ zOdd; zprime q; p \ q |] diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/AC_in_L.thy --- 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, \x r. DPow_r(f, r, Lset(x)), diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/DPow_absolute.thy --- 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) == \n1[M]. \e[M]. \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) == \X[M]. X \ Z <-> @@ -310,7 +310,7 @@ (* is_Collect :: "[i=>o,i,i=>o,i] => o" "is_Collect(M,A,P,z) == \x[M]. x \ z <-> x \ 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) == \u[M]. u \ z <-> (\x[M]. x\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 @@ (\env[M]. \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) == \y z. \gy[M]. y \ 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) == \i[M]. \Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \ Li" diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/Datatype_absolute.thy --- 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\0 & (\x\A. \y\A. x \ y \ 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) == \n1[M]. \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) == \nat'[M]. \natnat[M]. \natnatsum[M]. \XX[M]. \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) == (\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) == \zero[M]. empty(M,zero) & @@ -366,7 +366,7 @@ by (induct_tac p, simp_all) -constdefs +definition formula_N :: "i => i" "formula_N(n) == (\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) == \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) \ 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) == \sn[M]. \list_n[M]. \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) == \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) \ Inl(Inl(\x,y\))"}*} "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) \ Inl(Inr(\x,y\))"}*} "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) \ Inr(Inl(\x,y\))"}*} "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) \ Inr(Inr(p))"}*} "is_Forall(M,p,Z) == \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) == diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/Formula.thy --- 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 \ formula ==> Neg(p) \ formula" @@ -76,10 +76,11 @@ lemma "p \ formula ==> satisfies(A,p) \ 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 \ 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 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 \ Pow(A). \env \ list(A). \p \ formula. arity(p) \ 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 \ nat; y \ nat |] ==> subset_fm(x,y) \ 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 \ nat ==> transset_fm(x) \ 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. \y\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) == \ i. x \ 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 \ Pow(A). \env \ list(A). \p \ formula. X = {x\A. sats(A, p, Cons(x,env))}}" diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/Internalize.thy --- 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) == \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) == \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) == \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 \ nat ==> Nil_fm(x) \ formula" @@ -97,7 +97,7 @@ (* "is_Cons(M,a,l,Z) == \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) | (\x[M]. \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)) & (\x[M]. \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) & (\x[M]. \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) == \p[M]. p \ z <-> (\u[M]. \v[M]. u\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) == \p[M]. \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) == \p[M]. \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) == \p[M]. \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) == \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) == \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) == \u[M]. u \ z <-> (\x[M]. x\A & (\y[M]. y\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) | (\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 @@ (\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, \m u. \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 @@ \sn[M]. \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) == \n[M]. \eclosen[M]. finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \ 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) == \l[M]. l \ 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) == \n1[M]. \AX[M]. number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *) @@ -1135,7 +1135,7 @@ \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) == \n[M]. \listn[M]. finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \ 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) == \l[M]. l \ 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) == \nat'[M]. \natnat[M]. \natnatsum[M]. \XX[M]. \X3[M]. 4 3 2 1 0 @@ -1282,7 +1282,7 @@ (* "is_formula_N(M,n,Z) == \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) == \n[M]. \formn[M]. finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \ 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) == \p[M]. p \ 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), diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/L_axioms.thy --- 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) == \ b. (\z. L(z) \ P()) --> (\z\Lset(b). P())" @@ -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) & (\a. Cl(a) --> (\x \ 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) == (\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) == \x[M]. x \ z <-> (\y[M]. y\A & x \ 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) == \x[M]. (x \ z <-> (\w[M]. w\r & (\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) == \y[M]. (y \ z <-> (\w[M]. w\r & (\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) == \dr[M]. is_domain(M,r,dr) & (\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) == \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. x\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) == \x[M]. x \ z <-> (\w[M]. w\r & (\y[M]. y\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) == (\xs[M]. \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) == (\z[M]. z\r --> (\x[M]. \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) == \x[M]. \y[M]. \y'[M]. \p[M]. \p'[M]. pair(M,x,y,p) --> pair(M,x,y',p') --> p\r --> p'\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) & (\u[M]. u\r --> (\x[M]. \y[M]. pair(M,x,y,u) --> y\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 @@ (\x[M]. \y[M]. \z[M]. \xy[M]. \yz[M]. pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & xy \ s & yz \ 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) & (\x[M]. \x'[M]. \y[M]. \p[M]. \p'[M]. pair(M,x,y,p) --> pair(M,x',y,p') --> p\f --> p'\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) & (\y[M]. y\B --> (\x[M]. x\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) == \x[M]. x \ z <-> (x \ r & (\u[M]. u\A & (\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\r <-> q\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) & (\x[M]. x\a --> (\y[M]. y\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) & (\x[M]. x\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) & (\x[M]. x\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)), diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/MetaExists.thy --- 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\_./ _)" [0, 0] 0) +notation (xsymbols) + ex (binder "\" 0) lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))" proof (unfold ex_def) diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/Normal.thy --- 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) == \I. I \ 0 --> (\i\I. Ord(i) \ P(i)) --> P(\(I))" @@ -200,7 +200,7 @@ subsection {*Normal Functions*} -constdefs +definition mono_le_subset :: "(i=>i) => o" "mono_le_subset(M) == \i j. i\j --> M(i) \ 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), \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, \x r. csucc(r))" -syntax (xsymbols) - Aleph :: "i => i" ("\_" [90] 90) +notation (xsymbols) + Aleph ("\_" [90] 90) lemma Card_Aleph [simp, intro]: "Ord(a) ==> Card(Aleph(a))" @@ -458,4 +458,3 @@ done end - diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/Rank.thy --- 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\A, \y[M]. \f[M]. diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/Rec_Separation.thy --- 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 @@ (\fj[M]. \sj[M]. \fsj[M]. \ffp[M]. fun_apply(M,f,j,fj) & successor(M,j,sj) & fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \ 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) == \A[M]. is_field(M,r,A) --> (\p[M]. p \ 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) == \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) == \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))))" diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/Relative.thy --- 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) == \x[M]. x \ 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) == \p[M]. p \ z <-> @@ -893,7 +893,7 @@ (\x\nat. if (\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 "[] \ Inl(0)"}*} @@ -1390,7 +1390,7 @@ by (simp add: is_Cons_def Cons_def) -constdefs +definition quasilist :: "i => o" "quasilist(xs) == xs=Nil | (\x l. xs = Cons(x,l))" diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/Satisfies_absolute.thy --- 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 \ formula_n & successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \ 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)) & (\x[M]. x\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) == \x y. \env \ list(A). bool_of_o (nth(x,env) \ 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 \ 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 @@ \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 @@ (\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), diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/WF_absolute.thy --- 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 \ A*A. \n\nat. \f \ 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)"}*} diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/WFrec.thy --- 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) == \z[M]. z \ f <-> diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/Constructible/Wellorderings.thy --- 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) == \x[M]. x\A --> \ r" diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/ex/Commutation.thy --- 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) == - (\a b. \ r --> (\c. \ s --> (\x. \ t & \ u)))" + "square(r,s,t,u) == + (\a b. \ r --> (\c. \ s --> (\x. \ t & \ 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) == (\x y. \ (r Un converse(r))^* --> - (\z. \ r^* & \ r^*))" + "Church_Rosser(r) == (\x y. \ (r Un converse(r))^* --> + (\z. \ r^* & \ 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 \ 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 \ 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 diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/ex/Group.thy --- 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 ("\\") *) -constdefs +definition carrier :: "i => i" - "carrier(M) == fst(M)" + "carrier(M) == fst(M)" mmult :: "[i, i, i] => i" (infixl "\\" 70) - "mmult(M,x,y) == fst(snd(M)) ` " + "mmult(M,x,y) == fst(snd(M)) ` " one :: "i => i" ("\\") - "one(M) == fst(snd(snd(M)))" + "one(M) == fst(snd(snd(M)))" update_carrier :: "[i,i] => i" - "update_carrier(M,A) == " + "update_carrier(M,A) == " -constdefs (structure G) +definition m_inv :: "i => i => i" ("inv\ _" [81] 80) - "inv x == (THE y. y \ carrier(G) & y \ x = \ & x \ y = \)" + "inv\<^bsub>G\<^esub> x == (THE y. y \ carrier(G) & y \\<^bsub>G\<^esub> x = \\<^bsub>G\<^esub> & x \\<^bsub>G\<^esub> y = \\<^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 "\" 80) "G \ H == carrier(H), (\<, > @@ -332,7 +332,7 @@ subsection {* Isomorphisms *} -constdefs +definition hom :: "[i,i] => i" "hom(G,H) == {h \ carrier(G) -> carrier(H). @@ -358,7 +358,7 @@ subsection {* Isomorphisms *} -constdefs +definition iso :: "[i,i] => i" (infixr "\" 60) "G \ H == hom(G,H) \ 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) == 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 "#>\" 60) - "H #> a == \h\H. {h \ a}" + "H #>\<^bsub>G\<^esub> a == \h\H. {h \\<^bsub>G\<^esub> a}" l_coset :: "[i,i,i] => i" (infixl "<#\" 60) - "a <# H == \h\H. {a \ h}" + "a <#\<^bsub>G\<^esub> H == \h\H. {a \\<^bsub>G\<^esub> h}" RCOSETS :: "[i,i] => i" ("rcosets\ _" [81] 80) - "rcosets H == \a\carrier(G). {H #> a}" + "rcosets\<^bsub>G\<^esub> H == \a\carrier(G). {H #>\<^bsub>G\<^esub> a}" set_mult :: "[i,i,i] => i" (infixl "<#>\" 60) - "H <#> K == \h\H. \k\K. {h \ k}" + "H <#>\<^bsub>G\<^esub> K == \h\H. \k\K. {h \\<^bsub>G\<^esub> k}" SET_INV :: "[i,i] => i" ("set'_inv\ _" [81] 80) - "set_inv H == \h\H. {inv h}" + "set_inv\<^bsub>G\<^esub> H == \h\H. {inv\<^bsub>G\<^esub> h}" locale normal = subgroup + group + assumes coset_eq: "(\x \ carrier(G). H #> x = x <# H)" - -syntax - "@normal" :: "[i,i] => i" (infixl "\" 60) - -translations - "H \ G" == "normal(H,G)" +notation + normal (infixl "\" 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\ _" [60] 60) - "rcong H == { \ carrier(G) * carrier(G). inv x \ y \ H}" + "rcong\<^bsub>G\<^esub> H == { \ carrier(G) * carrier(G). inv\<^bsub>G\<^esub> x \\<^bsub>G\<^esub> y \ 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 == - G\<^esub> H, \ \ (rcosets\<^bsub>G\<^esub> H) \ (rcosets\<^bsub>G\<^esub> H). K1 <#> K2, H, 0>" + G\<^esub> H, \ \ (rcosets\<^bsub>G\<^esub> H) \ (rcosets\<^bsub>G\<^esub> H). K1 <#>\<^bsub>G\<^esub> K2, H, 0>" lemma (in normal) setmult_closed: "\K1 \ rcosets H; K2 \ rcosets H\ \ K1 <#> K2 \ 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 \ carrier(G). h ` x = \\<^bsub>H\<^esub>}"; diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/ex/Ramsey.thy --- 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) == (\x y. :E --> :E)" diff -r faacfd4392b5 -r 5a5c8ea5f66a src/ZF/ex/Ring.thy --- 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 ("\\") *) -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 "\\" 65) - "ring_add(M,x,y) == add_field(M) ` " + "ring_add(M,x,y) = add_field(M) ` " zero :: "i => i" ("\\") - "zero(M) == fst(snd(snd(snd(snd(M)))))" + "zero(M) = fst(snd(snd(snd(snd(M)))))" lemma add_field_eq [simp]: "add_field() = A" @@ -36,12 +36,12 @@ text {* Derived operations. *} -constdefs (structure R) +definition a_inv :: "[i,i] => i" ("\\ _" [81] 80) "a_inv(R) == m_inv ()" minus :: "[i,i,i] => i" (infixl "\\" 65) - "\x \ carrier(R); y \ carrier(R)\ \ x \ y == x \ (\ y)" + "\x \ carrier(R); y \ carrier(R)\ \ x \\<^bsub>R\<^esub> y = x \\<^bsub>R\<^esub> (\\<^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 \ carrier(R) \ \ \ x = \" +context ring +begin + +lemma l_null [simp]: "x \ carrier(R) \ \ \ x = \" proof - assume R: "x \ carrier(R)" then have "\ \ x \ \ \ x = (\ \ \) \ x" @@ -181,8 +183,7 @@ with R show ?thesis by (simp del: r_zero) qed -lemma (in ring) r_null [simp]: - "x \ carrier(R) \ x \ \ = \" +lemma r_null [simp]: "x \ carrier(R) \ x \ \ = \" proof - assume R: "x \ carrier(R)" then have "x \ \ \ x \ \ = x \ (\ \ \)" @@ -192,7 +193,7 @@ with R show ?thesis by (simp del: r_zero) qed -lemma (in ring) l_minus: +lemma l_minus: "\x \ carrier(R); y \ carrier(R)\ \ \ x \ y = \ (x \ y)" proof - assume R: "x \ carrier(R)" "y \ 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: "\x \ carrier(R); y \ carrier(R)\ \ x \ \ y = \ (x \ y)" proof - assume R: "x \ carrier(R)" "y \ 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: "\x \ carrier(R); y \ carrier(R)\ \ x \ y = x \ \ 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 \ carrier(R) -> carrier(S). (\x y. x \ carrier(R) & y \ carrier(R) --> h ` (x \\<^bsub>R\<^esub> y) = (h ` x) \\<^bsub>S\<^esub> (h ` y) & @@ -287,4 +290,3 @@ done end -