tuned specifications;
authorwenzelm
Tue Nov 07 19:40:13 2006 +0100 (2006-11-07)
changeset 212335a5c8ea5f66a
parent 21232 faacfd4392b5
child 21234 fb84ab52f23b
tuned specifications;
src/HOL/NumberTheory/Gauss.thy
src/HOL/NumberTheory/Quadratic_Reciprocity.thy
src/ZF/Constructible/AC_in_L.thy
src/ZF/Constructible/DPow_absolute.thy
src/ZF/Constructible/Datatype_absolute.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/Internalize.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/MetaExists.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/Rank.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/Relative.thy
src/ZF/Constructible/Satisfies_absolute.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
src/ZF/Constructible/Wellorderings.thy
src/ZF/ex/Commutation.thy
src/ZF/ex/Group.thy
src/ZF/ex/Ramsey.thy
src/ZF/ex/Ring.thy
     1.1 --- a/src/HOL/NumberTheory/Gauss.thy	Tue Nov 07 19:39:54 2006 +0100
     1.2 +++ b/src/HOL/NumberTheory/Gauss.thy	Tue Nov 07 19:40:13 2006 +0100
     1.3 @@ -10,37 +10,45 @@
     1.4  locale GAUSS =
     1.5    fixes p :: "int"
     1.6    fixes a :: "int"
     1.7 -  fixes A :: "int set"
     1.8 -  fixes B :: "int set"
     1.9 -  fixes C :: "int set"
    1.10 -  fixes D :: "int set"
    1.11 -  fixes E :: "int set"
    1.12 -  fixes F :: "int set"
    1.13  
    1.14    assumes p_prime: "zprime p"
    1.15    assumes p_g_2: "2 < p"
    1.16    assumes p_a_relprime: "~[a = 0](mod p)"
    1.17    assumes a_nonzero:    "0 < a"
    1.18 +begin
    1.19  
    1.20 -  defines A_def: "A == {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
    1.21 -  defines B_def: "B == (%x. x * a) ` A"
    1.22 -  defines C_def: "C == (StandardRes p) ` B"
    1.23 -  defines D_def: "D == C \<inter> {x. x \<le> ((p - 1) div 2)}"
    1.24 -  defines E_def: "E == C \<inter> {x. ((p - 1) div 2) < x}"
    1.25 -  defines F_def: "F == (%x. (p - x)) ` E"
    1.26 +definition
    1.27 +  A :: "int set"
    1.28 +  "A = {(x::int). 0 < x & x \<le> ((p - 1) div 2)}"
    1.29 +
    1.30 +  B :: "int set"
    1.31 +  "B = (%x. x * a) ` A"
    1.32 +
    1.33 +  C :: "int set"
    1.34 +  "C = StandardRes p ` B"
    1.35 +
    1.36 +  D :: "int set"
    1.37 +  "D = C \<inter> {x. x \<le> ((p - 1) div 2)}"
    1.38 +
    1.39 +  E :: "int set"
    1.40 +  "E = C \<inter> {x. ((p - 1) div 2) < x}"
    1.41 +
    1.42 +  F :: "int set"
    1.43 +  "F = (%x. (p - x)) ` E"
    1.44 +
    1.45  
    1.46  subsection {* Basic properties of p *}
    1.47  
    1.48 -lemma (in GAUSS) p_odd: "p \<in> zOdd"
    1.49 +lemma p_odd: "p \<in> zOdd"
    1.50    by (auto simp add: p_prime p_g_2 zprime_zOdd_eq_grt_2)
    1.51  
    1.52 -lemma (in GAUSS) p_g_0: "0 < p"
    1.53 +lemma p_g_0: "0 < p"
    1.54    using p_g_2 by auto
    1.55  
    1.56 -lemma (in GAUSS) int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
    1.57 +lemma int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
    1.58    using insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
    1.59  
    1.60 -lemma (in GAUSS) p_minus_one_l: "(p - 1) div 2 < p"
    1.61 +lemma p_minus_one_l: "(p - 1) div 2 < p"
    1.62  proof -
    1.63    have "(p - 1) div 2 \<le> (p - 1) div 1"
    1.64      by (rule zdiv_mono2) (auto simp add: p_g_0)
    1.65 @@ -48,9 +56,11 @@
    1.66    finally show ?thesis by simp
    1.67  qed
    1.68  
    1.69 -lemma (in GAUSS) p_eq: "p = (2 * (p - 1) div 2) + 1"
    1.70 +lemma p_eq: "p = (2 * (p - 1) div 2) + 1"
    1.71    using zdiv_zmult_self2 [of 2 "p - 1"] by auto
    1.72  
    1.73 +end
    1.74 +
    1.75  lemma zodd_imp_zdiv_eq: "x \<in> zOdd ==> 2 * (x - 1) div 2 = 2 * ((x - 1) div 2)"
    1.76    apply (frule odd_minus_one_even)
    1.77    apply (simp add: zEven_def)
    1.78 @@ -59,54 +69,58 @@
    1.79    apply (auto simp add: even_div_2_prop2)
    1.80    done
    1.81  
    1.82 -lemma (in GAUSS) p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
    1.83 +context GAUSS
    1.84 +begin
    1.85 +
    1.86 +lemma p_eq2: "p = (2 * ((p - 1) div 2)) + 1"
    1.87    apply (insert p_eq p_prime p_g_2 zprime_zOdd_eq_grt_2 [of p], auto)
    1.88    apply (frule zodd_imp_zdiv_eq, auto)
    1.89    done
    1.90  
    1.91 +
    1.92  subsection {* Basic Properties of the Gauss Sets *}
    1.93  
    1.94 -lemma (in GAUSS) finite_A: "finite (A)"
    1.95 +lemma finite_A: "finite (A)"
    1.96    apply (auto simp add: A_def)
    1.97    apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}")
    1.98    apply (auto simp add: bdd_int_set_l_finite finite_subset)
    1.99    done
   1.100  
   1.101 -lemma (in GAUSS) finite_B: "finite (B)"
   1.102 +lemma finite_B: "finite (B)"
   1.103    by (auto simp add: B_def finite_A finite_imageI)
   1.104  
   1.105 -lemma (in GAUSS) finite_C: "finite (C)"
   1.106 +lemma finite_C: "finite (C)"
   1.107    by (auto simp add: C_def finite_B finite_imageI)
   1.108  
   1.109 -lemma (in GAUSS) finite_D: "finite (D)"
   1.110 +lemma finite_D: "finite (D)"
   1.111    by (auto simp add: D_def finite_Int finite_C)
   1.112  
   1.113 -lemma (in GAUSS) finite_E: "finite (E)"
   1.114 +lemma finite_E: "finite (E)"
   1.115    by (auto simp add: E_def finite_Int finite_C)
   1.116  
   1.117 -lemma (in GAUSS) finite_F: "finite (F)"
   1.118 +lemma finite_F: "finite (F)"
   1.119    by (auto simp add: F_def finite_E finite_imageI)
   1.120  
   1.121 -lemma (in GAUSS) C_eq: "C = D \<union> E"
   1.122 +lemma C_eq: "C = D \<union> E"
   1.123    by (auto simp add: C_def D_def E_def)
   1.124  
   1.125 -lemma (in GAUSS) A_card_eq: "card A = nat ((p - 1) div 2)"
   1.126 +lemma A_card_eq: "card A = nat ((p - 1) div 2)"
   1.127    apply (auto simp add: A_def)
   1.128    apply (insert int_nat)
   1.129    apply (erule subst)
   1.130    apply (auto simp add: card_bdd_int_set_l_le)
   1.131    done
   1.132  
   1.133 -lemma (in GAUSS) inj_on_xa_A: "inj_on (%x. x * a) A"
   1.134 +lemma inj_on_xa_A: "inj_on (%x. x * a) A"
   1.135    using a_nonzero by (simp add: A_def inj_on_def)
   1.136  
   1.137 -lemma (in GAUSS) A_res: "ResSet p A"
   1.138 +lemma A_res: "ResSet p A"
   1.139    apply (auto simp add: A_def ResSet_def)
   1.140    apply (rule_tac m = p in zcong_less_eq)
   1.141    apply (insert p_g_2, auto)
   1.142    done
   1.143  
   1.144 -lemma (in GAUSS) B_res: "ResSet p B"
   1.145 +lemma B_res: "ResSet p B"
   1.146    apply (insert p_g_2 p_a_relprime p_minus_one_l)
   1.147    apply (auto simp add: B_def)
   1.148    apply (rule ResSet_image)
   1.149 @@ -128,7 +142,7 @@
   1.150      by (simp add: prems p_minus_one_l p_g_0)
   1.151  qed
   1.152  
   1.153 -lemma (in GAUSS) SR_B_inj: "inj_on (StandardRes p) B"
   1.154 +lemma SR_B_inj: "inj_on (StandardRes p) B"
   1.155    apply (auto simp add: B_def StandardRes_def inj_on_def A_def prems)
   1.156  proof -
   1.157    fix x fix y
   1.158 @@ -153,23 +167,23 @@
   1.159      by simp
   1.160  qed
   1.161  
   1.162 -lemma (in GAUSS) inj_on_pminusx_E: "inj_on (%x. p - x) E"
   1.163 +lemma inj_on_pminusx_E: "inj_on (%x. p - x) E"
   1.164    apply (auto simp add: E_def C_def B_def A_def)
   1.165    apply (rule_tac g = "%x. -1 * (x - p)" in inj_on_inverseI)
   1.166    apply auto
   1.167    done
   1.168  
   1.169 -lemma (in GAUSS) A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)"
   1.170 +lemma A_ncong_p: "x \<in> A ==> ~[x = 0](mod p)"
   1.171    apply (auto simp add: A_def)
   1.172    apply (frule_tac m = p in zcong_not_zero)
   1.173    apply (insert p_minus_one_l)
   1.174    apply auto
   1.175    done
   1.176  
   1.177 -lemma (in GAUSS) A_greater_zero: "x \<in> A ==> 0 < x"
   1.178 +lemma A_greater_zero: "x \<in> A ==> 0 < x"
   1.179    by (auto simp add: A_def)
   1.180  
   1.181 -lemma (in GAUSS) B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)"
   1.182 +lemma B_ncong_p: "x \<in> B ==> ~[x = 0](mod p)"
   1.183    apply (auto simp add: B_def)
   1.184    apply (frule A_ncong_p)
   1.185    apply (insert p_a_relprime p_prime a_nonzero)
   1.186 @@ -177,10 +191,10 @@
   1.187    apply (auto simp add: A_greater_zero)
   1.188    done
   1.189  
   1.190 -lemma (in GAUSS) B_greater_zero: "x \<in> B ==> 0 < x"
   1.191 +lemma B_greater_zero: "x \<in> B ==> 0 < x"
   1.192    using a_nonzero by (auto simp add: B_def mult_pos_pos A_greater_zero)
   1.193  
   1.194 -lemma (in GAUSS) C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)"
   1.195 +lemma C_ncong_p: "x \<in> C ==>  ~[x = 0](mod p)"
   1.196    apply (auto simp add: C_def)
   1.197    apply (frule B_ncong_p)
   1.198    apply (subgoal_tac "[x = StandardRes p x](mod p)")
   1.199 @@ -189,7 +203,7 @@
   1.200    apply auto
   1.201    done
   1.202  
   1.203 -lemma (in GAUSS) C_greater_zero: "y \<in> C ==> 0 < y"
   1.204 +lemma C_greater_zero: "y \<in> C ==> 0 < y"
   1.205    apply (auto simp add: C_def)
   1.206  proof -
   1.207    fix x
   1.208 @@ -204,13 +218,13 @@
   1.209      by (simp add: order_le_less)
   1.210  qed
   1.211  
   1.212 -lemma (in GAUSS) D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)"
   1.213 +lemma D_ncong_p: "x \<in> D ==> ~[x = 0](mod p)"
   1.214    by (auto simp add: D_def C_ncong_p)
   1.215  
   1.216 -lemma (in GAUSS) E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)"
   1.217 +lemma E_ncong_p: "x \<in> E ==> ~[x = 0](mod p)"
   1.218    by (auto simp add: E_def C_ncong_p)
   1.219  
   1.220 -lemma (in GAUSS) F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)"
   1.221 +lemma F_ncong_p: "x \<in> F ==> ~[x = 0](mod p)"
   1.222    apply (auto simp add: F_def)
   1.223  proof -
   1.224    fix x assume a: "x \<in> E" assume b: "[p - x = 0] (mod p)"
   1.225 @@ -225,7 +239,7 @@
   1.226    from this show False by (simp add: b)
   1.227  qed
   1.228  
   1.229 -lemma (in GAUSS) F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   1.230 +lemma F_subset: "F \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   1.231    apply (auto simp add: F_def E_def)
   1.232    apply (insert p_g_0)
   1.233    apply (frule_tac x = xa in StandardRes_ubound)
   1.234 @@ -241,19 +255,19 @@
   1.235      by simp
   1.236  qed
   1.237  
   1.238 -lemma (in GAUSS) D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   1.239 +lemma D_subset: "D \<subseteq> {x. 0 < x & x \<le> ((p - 1) div 2)}"
   1.240    by (auto simp add: D_def C_greater_zero)
   1.241  
   1.242 -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))}"
   1.243 +lemma F_eq: "F = {x. \<exists>y \<in> A. ( x = p - (StandardRes p (y*a)) & (p - 1) div 2 < StandardRes p (y*a))}"
   1.244    by (auto simp add: F_def E_def D_def C_def B_def A_def)
   1.245  
   1.246 -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)}"
   1.247 +lemma D_eq: "D = {x. \<exists>y \<in> A. ( x = StandardRes p (y*a) & StandardRes p (y*a) \<le> (p - 1) div 2)}"
   1.248    by (auto simp add: D_def C_def B_def A_def)
   1.249  
   1.250 -lemma (in GAUSS) D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
   1.251 +lemma D_leq: "x \<in> D ==> x \<le> (p - 1) div 2"
   1.252    by (auto simp add: D_eq)
   1.253  
   1.254 -lemma (in GAUSS) F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
   1.255 +lemma F_ge: "x \<in> F ==> x \<le> (p - 1) div 2"
   1.256    apply (auto simp add: F_eq A_def)
   1.257  proof -
   1.258    fix y
   1.259 @@ -268,24 +282,25 @@
   1.260      using zless_add1_eq [of "p - StandardRes p (y * a)" "(p - 1) div 2"] by auto
   1.261  qed
   1.262  
   1.263 -lemma (in GAUSS) all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
   1.264 +lemma all_A_relprime: "\<forall>x \<in> A. zgcd(x, p) = 1"
   1.265    using p_prime p_minus_one_l by (auto simp add: A_def zless_zprime_imp_zrelprime)
   1.266  
   1.267 -lemma (in GAUSS) A_prod_relprime: "zgcd((setprod id A),p) = 1"
   1.268 +lemma A_prod_relprime: "zgcd((setprod id A),p) = 1"
   1.269    using all_A_relprime finite_A by (simp add: all_relprime_prod_relprime)
   1.270  
   1.271 +
   1.272  subsection {* Relationships Between Gauss Sets *}
   1.273  
   1.274 -lemma (in GAUSS) B_card_eq_A: "card B = card A"
   1.275 +lemma B_card_eq_A: "card B = card A"
   1.276    using finite_A by (simp add: finite_A B_def inj_on_xa_A card_image)
   1.277  
   1.278 -lemma (in GAUSS) B_card_eq: "card B = nat ((p - 1) div 2)"
   1.279 +lemma B_card_eq: "card B = nat ((p - 1) div 2)"
   1.280    by (simp add: B_card_eq_A A_card_eq)
   1.281  
   1.282 -lemma (in GAUSS) F_card_eq_E: "card F = card E"
   1.283 +lemma F_card_eq_E: "card F = card E"
   1.284    using finite_E by (simp add: F_def inj_on_pminusx_E card_image)
   1.285  
   1.286 -lemma (in GAUSS) C_card_eq_B: "card C = card B"
   1.287 +lemma C_card_eq_B: "card C = card B"
   1.288    apply (insert finite_B)
   1.289    apply (subgoal_tac "inj_on (StandardRes p) B")
   1.290    apply (simp add: B_def C_def card_image)
   1.291 @@ -293,19 +308,19 @@
   1.292    apply (simp add: B_res)
   1.293    done
   1.294  
   1.295 -lemma (in GAUSS) D_E_disj: "D \<inter> E = {}"
   1.296 +lemma D_E_disj: "D \<inter> E = {}"
   1.297    by (auto simp add: D_def E_def)
   1.298  
   1.299 -lemma (in GAUSS) C_card_eq_D_plus_E: "card C = card D + card E"
   1.300 +lemma C_card_eq_D_plus_E: "card C = card D + card E"
   1.301    by (auto simp add: C_eq card_Un_disjoint D_E_disj finite_D finite_E)
   1.302  
   1.303 -lemma (in GAUSS) C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
   1.304 +lemma C_prod_eq_D_times_E: "setprod id E * setprod id D = setprod id C"
   1.305    apply (insert D_E_disj finite_D finite_E C_eq)
   1.306    apply (frule setprod_Un_disjoint [of D E id])
   1.307    apply auto
   1.308    done
   1.309  
   1.310 -lemma (in GAUSS) C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
   1.311 +lemma C_B_zcong_prod: "[setprod id C = setprod id B] (mod p)"
   1.312    apply (auto simp add: C_def)
   1.313    apply (insert finite_B SR_B_inj)
   1.314    apply (frule_tac f = "StandardRes p" in setprod_reindex_id [symmetric], auto)
   1.315 @@ -313,15 +328,12 @@
   1.316    apply (auto simp add: StandardRes_prop1 zcong_sym p_g_0)
   1.317    done
   1.318  
   1.319 -lemma (in GAUSS) F_Un_D_subset: "(F \<union> D) \<subseteq> A"
   1.320 +lemma F_Un_D_subset: "(F \<union> D) \<subseteq> A"
   1.321    apply (rule Un_least)
   1.322    apply (auto simp add: A_def F_subset D_subset)
   1.323    done
   1.324  
   1.325 -lemma two_eq: "2 * (x::int) = x + x"
   1.326 -  by arith
   1.327 -
   1.328 -lemma (in GAUSS) F_D_disj: "(F \<inter> D) = {}"
   1.329 +lemma F_D_disj: "(F \<inter> D) = {}"
   1.330    apply (simp add: F_eq D_eq)
   1.331    apply (auto simp add: F_eq D_eq)
   1.332  proof -
   1.333 @@ -366,8 +378,7 @@
   1.334      done
   1.335  qed
   1.336  
   1.337 -lemma (in GAUSS) F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
   1.338 -  apply (insert F_D_disj finite_F finite_D)
   1.339 +lemma F_Un_D_card: "card (F \<union> D) = nat ((p - 1) div 2)"
   1.340  proof -
   1.341    have "card (F \<union> D) = card E + card D"
   1.342      by (auto simp add: finite_F finite_D F_D_disj
   1.343 @@ -378,17 +389,17 @@
   1.344      by (simp add: C_card_eq_B B_card_eq)
   1.345  qed
   1.346  
   1.347 -lemma (in GAUSS) F_Un_D_eq_A: "F \<union> D = A"
   1.348 +lemma F_Un_D_eq_A: "F \<union> D = A"
   1.349    using finite_A F_Un_D_subset A_card_eq F_Un_D_card by (auto simp add: card_seteq)
   1.350  
   1.351 -lemma (in GAUSS) prod_D_F_eq_prod_A:
   1.352 +lemma prod_D_F_eq_prod_A:
   1.353      "(setprod id D) * (setprod id F) = setprod id A"
   1.354    apply (insert F_D_disj finite_D finite_F)
   1.355    apply (frule setprod_Un_disjoint [of F D id])
   1.356    apply (auto simp add: F_Un_D_eq_A)
   1.357    done
   1.358  
   1.359 -lemma (in GAUSS) prod_F_zcong:
   1.360 +lemma prod_F_zcong:
   1.361    "[setprod id F = ((-1) ^ (card E)) * (setprod id E)] (mod p)"
   1.362  proof -
   1.363    have "setprod id F = setprod id (op - p ` E)"
   1.364 @@ -438,12 +449,13 @@
   1.365      by simp
   1.366  qed
   1.367  
   1.368 +
   1.369  subsection {* Gauss' Lemma *}
   1.370  
   1.371 -lemma (in GAUSS) aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
   1.372 +lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
   1.373    by (auto simp add: finite_E neg_one_special)
   1.374  
   1.375 -theorem (in GAUSS) pre_gauss_lemma:
   1.376 +theorem pre_gauss_lemma:
   1.377    "[a ^ nat((p - 1) div 2) = (-1) ^ (card E)] (mod p)"
   1.378  proof -
   1.379    have "[setprod id A = setprod id F * setprod id D](mod p)"
   1.380 @@ -499,7 +511,7 @@
   1.381      by (simp add: A_card_eq zcong_sym)
   1.382  qed
   1.383  
   1.384 -theorem (in GAUSS) gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
   1.385 +theorem gauss_lemma: "(Legendre a p) = (-1) ^ (card E)"
   1.386  proof -
   1.387    from Euler_Criterion p_prime p_g_2 have
   1.388        "[(Legendre a p) = a^(nat (((p) - 1) div 2))] (mod p)"
   1.389 @@ -516,3 +528,5 @@
   1.390  qed
   1.391  
   1.392  end
   1.393 +
   1.394 +end
     2.1 --- a/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Tue Nov 07 19:39:54 2006 +0100
     2.2 +++ b/src/HOL/NumberTheory/Quadratic_Reciprocity.thy	Tue Nov 07 19:40:13 2006 +0100
     2.3 @@ -14,7 +14,10 @@
     2.4    Zuckerman's presentation.
     2.5  *}
     2.6  
     2.7 -lemma (in GAUSS) QRLemma1: "a * setsum id A =
     2.8 +context GAUSS
     2.9 +begin
    2.10 +
    2.11 +lemma QRLemma1: "a * setsum id A =
    2.12    p * setsum (%x. ((x * a) div p)) A + setsum id D + setsum id E"
    2.13  proof -
    2.14    from finite_A have "a * setsum id A = setsum (%x. a * x) A"
    2.15 @@ -44,7 +47,7 @@
    2.16    finally show ?thesis by arith
    2.17  qed
    2.18  
    2.19 -lemma (in GAUSS) QRLemma2: "setsum id A = p * int (card E) - setsum id E +
    2.20 +lemma QRLemma2: "setsum id A = p * int (card E) - setsum id E +
    2.21    setsum id D"
    2.22  proof -
    2.23    from F_Un_D_eq_A have "setsum id A = setsum id (D \<union> F)"
    2.24 @@ -65,7 +68,7 @@
    2.25      by arith
    2.26  qed
    2.27  
    2.28 -lemma (in GAUSS) QRLemma3: "(a - 1) * setsum id A =
    2.29 +lemma QRLemma3: "(a - 1) * setsum id A =
    2.30      p * (setsum (%x. ((x * a) div p)) A - int(card E)) + 2 * setsum id E"
    2.31  proof -
    2.32    have "(a - 1) * setsum id A = a * setsum id A - setsum id A"
    2.33 @@ -83,7 +86,7 @@
    2.34      by (auto simp only: zdiff_zmult_distrib2)
    2.35  qed
    2.36  
    2.37 -lemma (in GAUSS) QRLemma4: "a \<in> zOdd ==>
    2.38 +lemma QRLemma4: "a \<in> zOdd ==>
    2.39      (setsum (%x. ((x * a) div p)) A \<in> zEven) = (int(card E): zEven)"
    2.40  proof -
    2.41    assume a_odd: "a \<in> zOdd"
    2.42 @@ -108,7 +111,7 @@
    2.43      by (auto simp only: even_diff [symmetric])
    2.44  qed
    2.45  
    2.46 -lemma (in GAUSS) QRLemma5: "a \<in> zOdd ==>
    2.47 +lemma QRLemma5: "a \<in> zOdd ==>
    2.48     (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
    2.49  proof -
    2.50    assume "a \<in> zOdd"
    2.51 @@ -138,6 +141,8 @@
    2.52    finally show ?thesis .
    2.53  qed
    2.54  
    2.55 +end
    2.56 +
    2.57  lemma MainQRLemma: "[| a \<in> zOdd; 0 < a; ~([a = 0] (mod p)); zprime p; 2 < p;
    2.58    A = {x. 0 < x & x \<le> (p - 1) div 2} |] ==>
    2.59    (Legendre a p) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
    2.60 @@ -145,6 +150,7 @@
    2.61    apply (auto simp add: GAUSS_def)
    2.62    apply (subst GAUSS.QRLemma5)
    2.63    apply (auto simp add: GAUSS_def)
    2.64 +  apply (simp add: GAUSS.A_def [OF GAUSS.intro] GAUSS_def)
    2.65    done
    2.66  
    2.67  
    2.68 @@ -153,47 +159,51 @@
    2.69  locale QRTEMP =
    2.70    fixes p     :: "int"
    2.71    fixes q     :: "int"
    2.72 -  fixes P_set :: "int set"
    2.73 -  fixes Q_set :: "int set"
    2.74 -  fixes S     :: "(int * int) set"
    2.75 -  fixes S1    :: "(int * int) set"
    2.76 -  fixes S2    :: "(int * int) set"
    2.77 -  fixes f1    :: "int => (int * int) set"
    2.78 -  fixes f2    :: "int => (int * int) set"
    2.79  
    2.80    assumes p_prime: "zprime p"
    2.81    assumes p_g_2: "2 < p"
    2.82    assumes q_prime: "zprime q"
    2.83    assumes q_g_2: "2 < q"
    2.84    assumes p_neq_q:      "p \<noteq> q"
    2.85 +begin
    2.86  
    2.87 -  defines P_set_def: "P_set == {x. 0 < x & x \<le> ((p - 1) div 2) }"
    2.88 -  defines Q_set_def: "Q_set == {x. 0 < x & x \<le> ((q - 1) div 2) }"
    2.89 -  defines S_def:     "S     == P_set <*> Q_set"
    2.90 -  defines S1_def:    "S1    == { (x, y). (x, y):S & ((p * y) < (q * x)) }"
    2.91 -  defines S2_def:    "S2    == { (x, y). (x, y):S & ((q * x) < (p * y)) }"
    2.92 -  defines f1_def:    "f1 j  == { (j1, y). (j1, y):S & j1 = j &
    2.93 -                                 (y \<le> (q * j) div p) }"
    2.94 -  defines f2_def:    "f2 j  == { (x, j1). (x, j1):S & j1 = j &
    2.95 -                                 (x \<le> (p * j) div q) }"
    2.96 +definition
    2.97 +  P_set :: "int set"
    2.98 +  "P_set = {x. 0 < x & x \<le> ((p - 1) div 2) }"
    2.99 +
   2.100 +  Q_set :: "int set"
   2.101 +  "Q_set = {x. 0 < x & x \<le> ((q - 1) div 2) }"
   2.102 +  
   2.103 +  S :: "(int * int) set"
   2.104 +  "S = P_set <*> Q_set"
   2.105 +
   2.106 +  S1 :: "(int * int) set"
   2.107 +  "S1 = { (x, y). (x, y):S & ((p * y) < (q * x)) }"
   2.108  
   2.109 -lemma (in QRTEMP) p_fact: "0 < (p - 1) div 2"
   2.110 +  S2 :: "(int * int) set"
   2.111 +  "S2 = { (x, y). (x, y):S & ((q * x) < (p * y)) }"
   2.112 +
   2.113 +  f1 :: "int => (int * int) set"
   2.114 +  "f1 j = { (j1, y). (j1, y):S & j1 = j & (y \<le> (q * j) div p) }"
   2.115 +
   2.116 +  f2 :: "int => (int * int) set"
   2.117 +  "f2 j = { (x, j1). (x, j1):S & j1 = j & (x \<le> (p * j) div q) }"
   2.118 +
   2.119 +lemma p_fact: "0 < (p - 1) div 2"
   2.120  proof -
   2.121 -  from prems have "2 < p" by (simp add: QRTEMP_def)
   2.122 -  then have "2 \<le> p - 1" by arith
   2.123 +  from p_g_2 have "2 \<le> p - 1" by arith
   2.124    then have "2 div 2 \<le> (p - 1) div 2" by (rule zdiv_mono1, auto)
   2.125    then show ?thesis by auto
   2.126  qed
   2.127  
   2.128 -lemma (in QRTEMP) q_fact: "0 < (q - 1) div 2"
   2.129 +lemma q_fact: "0 < (q - 1) div 2"
   2.130  proof -
   2.131 -  from prems have "2 < q" by (simp add: QRTEMP_def)
   2.132 -  then have "2 \<le> q - 1" by arith
   2.133 +  from q_g_2 have "2 \<le> q - 1" by arith
   2.134    then have "2 div 2 \<le> (q - 1) div 2" by (rule zdiv_mono1, auto)
   2.135    then show ?thesis by auto
   2.136  qed
   2.137  
   2.138 -lemma (in QRTEMP) pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
   2.139 +lemma pb_neq_qa: "[|1 \<le> b; b \<le> (q - 1) div 2 |] ==>
   2.140      (p * b \<noteq> q * a)"
   2.141  proof
   2.142    assume "p * b = q * a" and "1 \<le> b" and "b \<le> (q - 1) div 2"
   2.143 @@ -234,43 +244,43 @@
   2.144    with q_g_2 show False by auto
   2.145  qed
   2.146  
   2.147 -lemma (in QRTEMP) P_set_finite: "finite (P_set)"
   2.148 +lemma P_set_finite: "finite (P_set)"
   2.149    using p_fact by (auto simp add: P_set_def bdd_int_set_l_le_finite)
   2.150  
   2.151 -lemma (in QRTEMP) Q_set_finite: "finite (Q_set)"
   2.152 +lemma Q_set_finite: "finite (Q_set)"
   2.153    using q_fact by (auto simp add: Q_set_def bdd_int_set_l_le_finite)
   2.154  
   2.155 -lemma (in QRTEMP) S_finite: "finite S"
   2.156 +lemma S_finite: "finite S"
   2.157    by (auto simp add: S_def  P_set_finite Q_set_finite finite_cartesian_product)
   2.158  
   2.159 -lemma (in QRTEMP) S1_finite: "finite S1"
   2.160 +lemma S1_finite: "finite S1"
   2.161  proof -
   2.162    have "finite S" by (auto simp add: S_finite)
   2.163    moreover have "S1 \<subseteq> S" by (auto simp add: S1_def S_def)
   2.164    ultimately show ?thesis by (auto simp add: finite_subset)
   2.165  qed
   2.166  
   2.167 -lemma (in QRTEMP) S2_finite: "finite S2"
   2.168 +lemma S2_finite: "finite S2"
   2.169  proof -
   2.170    have "finite S" by (auto simp add: S_finite)
   2.171    moreover have "S2 \<subseteq> S" by (auto simp add: S2_def S_def)
   2.172    ultimately show ?thesis by (auto simp add: finite_subset)
   2.173  qed
   2.174  
   2.175 -lemma (in QRTEMP) P_set_card: "(p - 1) div 2 = int (card (P_set))"
   2.176 +lemma P_set_card: "(p - 1) div 2 = int (card (P_set))"
   2.177    using p_fact by (auto simp add: P_set_def card_bdd_int_set_l_le)
   2.178  
   2.179 -lemma (in QRTEMP) Q_set_card: "(q - 1) div 2 = int (card (Q_set))"
   2.180 +lemma Q_set_card: "(q - 1) div 2 = int (card (Q_set))"
   2.181    using q_fact by (auto simp add: Q_set_def card_bdd_int_set_l_le)
   2.182  
   2.183 -lemma (in QRTEMP) S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
   2.184 +lemma S_card: "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
   2.185    using P_set_card Q_set_card P_set_finite Q_set_finite
   2.186    by (auto simp add: S_def zmult_int setsum_constant)
   2.187  
   2.188 -lemma (in QRTEMP) S1_Int_S2_prop: "S1 \<inter> S2 = {}"
   2.189 +lemma S1_Int_S2_prop: "S1 \<inter> S2 = {}"
   2.190    by (auto simp add: S1_def S2_def)
   2.191  
   2.192 -lemma (in QRTEMP) S1_Union_S2_prop: "S = S1 \<union> S2"
   2.193 +lemma S1_Union_S2_prop: "S = S1 \<union> S2"
   2.194    apply (auto simp add: S_def P_set_def Q_set_def S1_def S2_def)
   2.195  proof -
   2.196    fix a and b
   2.197 @@ -280,7 +290,7 @@
   2.198    ultimately show "p * b < q * a" by auto
   2.199  qed
   2.200  
   2.201 -lemma (in QRTEMP) card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
   2.202 +lemma card_sum_S1_S2: "((p - 1) div 2) * ((q - 1) div 2) =
   2.203      int(card(S1)) + int(card(S2))"
   2.204  proof -
   2.205    have "((p - 1) div 2) * ((q - 1) div 2) = int (card(S))"
   2.206 @@ -293,7 +303,7 @@
   2.207    finally show ?thesis .
   2.208  qed
   2.209  
   2.210 -lemma (in QRTEMP) aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
   2.211 +lemma aux1a: "[| 0 < a; a \<le> (p - 1) div 2;
   2.212                               0 < b; b \<le> (q - 1) div 2 |] ==>
   2.213                            (p * b < q * a) = (b \<le> q * a div p)"
   2.214  proof -
   2.215 @@ -327,7 +337,7 @@
   2.216    ultimately show ?thesis ..
   2.217  qed
   2.218  
   2.219 -lemma (in QRTEMP) aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
   2.220 +lemma aux1b: "[| 0 < a; a \<le> (p - 1) div 2;
   2.221                               0 < b; b \<le> (q - 1) div 2 |] ==>
   2.222                            (q * a < p * b) = (a \<le> p * b div q)"
   2.223  proof -
   2.224 @@ -361,6 +371,8 @@
   2.225    ultimately show ?thesis ..
   2.226  qed
   2.227  
   2.228 +end
   2.229 +
   2.230  lemma aux2: "[| zprime p; zprime q; 2 < p; 2 < q |] ==>
   2.231               (q * ((p - 1) div 2)) div p \<le> (q - 1) div 2"
   2.232  proof-
   2.233 @@ -390,7 +402,10 @@
   2.234      using prems by auto
   2.235  qed
   2.236  
   2.237 -lemma (in QRTEMP) aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
   2.238 +context QRTEMP
   2.239 +begin
   2.240 +
   2.241 +lemma aux3a: "\<forall>j \<in> P_set. int (card (f1 j)) = (q * j) div p"
   2.242  proof
   2.243    fix j
   2.244    assume j_fact: "j \<in> P_set"
   2.245 @@ -422,7 +437,7 @@
   2.246          by (auto simp add: mult_le_cancel_left)
   2.247        with p_g_2 have "q * j div p \<le> q * ((p - 1) div 2) div p"
   2.248          by (auto simp add: zdiv_mono1)
   2.249 -      also from prems have "... \<le> (q - 1) div 2"
   2.250 +      also from prems P_set_def have "... \<le> (q - 1) div 2"
   2.251          apply simp
   2.252          apply (insert aux2)
   2.253          apply (simp add: QRTEMP_def)
   2.254 @@ -446,7 +461,7 @@
   2.255    finally show "int (card (f1 j)) = q * j div p" .
   2.256  qed
   2.257  
   2.258 -lemma (in QRTEMP) aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q"
   2.259 +lemma aux3b: "\<forall>j \<in> Q_set. int (card (f2 j)) = (p * j) div q"
   2.260  proof
   2.261    fix j
   2.262    assume j_fact: "j \<in> Q_set"
   2.263 @@ -499,7 +514,7 @@
   2.264    finally show "int (card (f2 j)) = p * j div q" .
   2.265  qed
   2.266  
   2.267 -lemma (in QRTEMP) S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set"
   2.268 +lemma S1_card: "int (card(S1)) = setsum (%j. (q * j) div p) P_set"
   2.269  proof -
   2.270    have "\<forall>x \<in> P_set. finite (f1 x)"
   2.271    proof
   2.272 @@ -522,7 +537,7 @@
   2.273    finally show ?thesis .
   2.274  qed
   2.275  
   2.276 -lemma (in QRTEMP) S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set"
   2.277 +lemma S2_card: "int (card(S2)) = setsum (%j. (p * j) div q) Q_set"
   2.278  proof -
   2.279    have "\<forall>x \<in> Q_set. finite (f2 x)"
   2.280    proof
   2.281 @@ -546,15 +561,15 @@
   2.282    finally show ?thesis .
   2.283  qed
   2.284  
   2.285 -lemma (in QRTEMP) S1_carda: "int (card(S1)) =
   2.286 +lemma S1_carda: "int (card(S1)) =
   2.287      setsum (%j. (j * q) div p) P_set"
   2.288    by (auto simp add: S1_card zmult_ac)
   2.289  
   2.290 -lemma (in QRTEMP) S2_carda: "int (card(S2)) =
   2.291 +lemma S2_carda: "int (card(S2)) =
   2.292      setsum (%j. (j * p) div q) Q_set"
   2.293    by (auto simp add: S2_card zmult_ac)
   2.294  
   2.295 -lemma (in QRTEMP) pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
   2.296 +lemma pq_sum_prop: "(setsum (%j. (j * p) div q) Q_set) +
   2.297      (setsum (%j. (j * q) div p) P_set) = ((p - 1) div 2) * ((q - 1) div 2)"
   2.298  proof -
   2.299    have "(setsum (%j. (j * p) div q) Q_set) +
   2.300 @@ -567,6 +582,8 @@
   2.301    finally show ?thesis .
   2.302  qed
   2.303  
   2.304 +end
   2.305 +
   2.306  lemma pq_prime_neq: "[| zprime p; zprime q; p \<noteq> q |] ==> (~[p = 0] (mod q))"
   2.307    apply (auto simp add: zcong_eq_zdvd_prop zprime_def)
   2.308    apply (drule_tac x = q in allE)
   2.309 @@ -574,12 +591,15 @@
   2.310    apply auto
   2.311    done
   2.312  
   2.313 -lemma (in QRTEMP) QR_short: "(Legendre p q) * (Legendre q p) =
   2.314 +context QRTEMP
   2.315 +begin
   2.316 +
   2.317 +lemma QR_short: "(Legendre p q) * (Legendre q p) =
   2.318      (-1::int)^nat(((p - 1) div 2)*((q - 1) div 2))"
   2.319  proof -
   2.320    from prems have "~([p = 0] (mod q))"
   2.321      by (auto simp add: pq_prime_neq QRTEMP_def)
   2.322 -  with prems have a1: "(Legendre p q) = (-1::int) ^
   2.323 +  with prems Q_set_def have a1: "(Legendre p q) = (-1::int) ^
   2.324        nat(setsum (%x. ((x * p) div q)) Q_set)"
   2.325      apply (rule_tac p = q in  MainQRLemma)
   2.326      apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   2.327 @@ -588,7 +608,7 @@
   2.328      apply (rule_tac p = q and q = p in pq_prime_neq)
   2.329      apply (simp add: QRTEMP_def)+
   2.330      done
   2.331 -  with prems have a2: "(Legendre q p) =
   2.332 +  with prems P_set_def have a2: "(Legendre q p) =
   2.333        (-1::int) ^ nat(setsum (%x. ((x * q) div p)) P_set)"
   2.334      apply (rule_tac p = p in  MainQRLemma)
   2.335      apply (auto simp add: zprime_zOdd_eq_grt_2 QRTEMP_def)
   2.336 @@ -613,6 +633,8 @@
   2.337    finally show ?thesis .
   2.338  qed
   2.339  
   2.340 +end
   2.341 +
   2.342  theorem Quadratic_Reciprocity:
   2.343       "[| p \<in> zOdd; zprime p; q \<in> zOdd; zprime q;
   2.344           p \<noteq> q |]
     3.1 --- a/src/ZF/Constructible/AC_in_L.thy	Tue Nov 07 19:39:54 2006 +0100
     3.2 +++ b/src/ZF/Constructible/AC_in_L.thy	Tue Nov 07 19:40:13 2006 +0100
     3.3 @@ -222,7 +222,7 @@
     3.4  (environment, formula) pairs into the ordinals.  For each member of @{term
     3.5  "DPow(A)"}, we take the minimum such ordinal.*}
     3.6  
     3.7 -constdefs
     3.8 +definition
     3.9    env_form_r :: "[i,i,i]=>i"
    3.10      --{*wellordering on (environment, formula) pairs*}
    3.11     "env_form_r(f,r,A) ==
    3.12 @@ -317,7 +317,7 @@
    3.13  @{term "Lset(i)"}.  We assume as an inductive hypothesis that there is a family
    3.14  of wellorderings for smaller ordinals.*}
    3.15  
    3.16 -constdefs
    3.17 +definition
    3.18    rlimit :: "[i,i=>i]=>i"
    3.19    --{*Expresses the wellordering at limit ordinals.  The conditional
    3.20        lets us remove the premise @{term "Limit(i)"} from some theorems.*}
    3.21 @@ -400,7 +400,7 @@
    3.22  
    3.23  subsection{*Transfinite Definition of the Wellordering on @{term "L"}*}
    3.24  
    3.25 -constdefs
    3.26 +definition
    3.27   L_r :: "[i, i] => i"
    3.28    "L_r(f) == %i.
    3.29        transrec3(i, 0, \<lambda>x r. DPow_r(f, r, Lset(x)), 
     4.1 --- a/src/ZF/Constructible/DPow_absolute.thy	Tue Nov 07 19:39:54 2006 +0100
     4.2 +++ b/src/ZF/Constructible/DPow_absolute.thy	Tue Nov 07 19:40:13 2006 +0100
     4.3 @@ -23,7 +23,7 @@
     4.4               successor(M,dp,i) & fun_apply(M,f,p,z) & is_transrec(M,MH,i,f)"
     4.5  *)
     4.6  
     4.7 -constdefs formula_rec_fm :: "[i, i, i]=>i"
     4.8 +definition formula_rec_fm :: "[i, i, i]=>i"
     4.9   "formula_rec_fm(mh,p,z) == 
    4.10      Exists(Exists(Exists(
    4.11        And(finite_ordinal_fm(2),
    4.12 @@ -80,7 +80,7 @@
    4.13  subsubsection{*The Operator @{term is_satisfies}*}
    4.14  
    4.15  (* is_satisfies(M,A,p,z) == is_formula_rec (M, satisfies_MH(M,A), p, z) *)
    4.16 -constdefs satisfies_fm :: "[i,i,i]=>i"
    4.17 +definition satisfies_fm :: "[i,i,i]=>i"
    4.18      "satisfies_fm(x) == formula_rec_fm (satisfies_MH_fm(x#+5#+6, 2, 1, 0))"
    4.19  
    4.20  lemma is_satisfies_type [TC]:
    4.21 @@ -119,7 +119,7 @@
    4.22  
    4.23  text{*Relativize the use of @{term sats} within @{term DPow'}
    4.24  (the comprehension).*}
    4.25 -constdefs
    4.26 +definition
    4.27    is_DPow_sats :: "[i=>o,i,i,i,i] => o"
    4.28     "is_DPow_sats(M,A,env,p,x) ==
    4.29        \<forall>n1[M]. \<forall>e[M]. \<forall>sp[M]. 
    4.30 @@ -148,7 +148,7 @@
    4.31               is_satisfies(M,A,p,sp) --> is_Cons(M,x,env,e) --> 
    4.32               fun_apply(M, sp, e, n1) --> number1(M, n1) *)
    4.33  
    4.34 -constdefs DPow_sats_fm :: "[i,i,i,i]=>i"
    4.35 +definition DPow_sats_fm :: "[i,i,i,i]=>i"
    4.36   "DPow_sats_fm(A,env,p,x) ==
    4.37     Forall(Forall(Forall(
    4.38       Implies(satisfies_fm(A#+3,p#+3,0), 
    4.39 @@ -218,7 +218,7 @@
    4.40  done
    4.41  
    4.42  text{*Relativization of the Operator @{term DPow'}*}
    4.43 -constdefs 
    4.44 +definition 
    4.45    is_DPow' :: "[i=>o,i,i] => o"
    4.46      "is_DPow'(M,A,Z) == 
    4.47         \<forall>X[M]. X \<in> Z <-> 
    4.48 @@ -310,7 +310,7 @@
    4.49  (* is_Collect :: "[i=>o,i,i=>o,i] => o"
    4.50      "is_Collect(M,A,P,z) == \<forall>x[M]. x \<in> z <-> x \<in> A & P(x)" *)
    4.51  
    4.52 -constdefs Collect_fm :: "[i, i, i]=>i"
    4.53 +definition Collect_fm :: "[i, i, i]=>i"
    4.54   "Collect_fm(A,is_P,z) == 
    4.55          Forall(Iff(Member(0,succ(z)),
    4.56                     And(Member(0,succ(A)), is_P)))"
    4.57 @@ -360,7 +360,7 @@
    4.58  (*  is_Replace :: "[i=>o,i,[i,i]=>o,i] => o"
    4.59      "is_Replace(M,A,P,z) == \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & P(x,u))" *)
    4.60  
    4.61 -constdefs Replace_fm :: "[i, i, i]=>i"
    4.62 +definition Replace_fm :: "[i, i, i]=>i"
    4.63   "Replace_fm(A,is_P,z) == 
    4.64          Forall(Iff(Member(0,succ(z)),
    4.65                     Exists(And(Member(0,A#+2), is_P))))"
    4.66 @@ -413,7 +413,7 @@
    4.67             (\<exists>env[M]. \<exists>p[M]. mem_formula(M,p) & mem_list(M,A,env) &
    4.68                      is_Collect(M, A, is_DPow_sats(M,A,env,p), X))" *)
    4.69  
    4.70 -constdefs DPow'_fm :: "[i,i]=>i"
    4.71 +definition DPow'_fm :: "[i,i]=>i"
    4.72      "DPow'_fm(A,Z) == 
    4.73        Forall(
    4.74         Iff(Member(0,succ(Z)),
    4.75 @@ -451,7 +451,7 @@
    4.76  
    4.77  subsection{*A Locale for Relativizing the Operator @{term Lset}*}
    4.78  
    4.79 -constdefs
    4.80 +definition
    4.81    transrec_body :: "[i=>o,i,i,i,i] => o"
    4.82      "transrec_body(M,g,x) ==
    4.83        \<lambda>y z. \<exists>gy[M]. y \<in> x & fun_apply(M,g,y,gy) & is_DPow'(M,gy,z)"
    4.84 @@ -503,7 +503,7 @@
    4.85  
    4.86  text{*Relativization of the Operator @{term Lset}*}
    4.87  
    4.88 -constdefs
    4.89 +definition
    4.90    is_Lset :: "[i=>o, i, i] => o"
    4.91     --{*We can use the term language below because @{term is_Lset} will
    4.92         not have to be internalized: it isn't used in any instance of
    4.93 @@ -609,7 +609,7 @@
    4.94  subsection{*The Notion of Constructible Set*}
    4.95  
    4.96  
    4.97 -constdefs
    4.98 +definition
    4.99    constructible :: "[i=>o,i] => o"
   4.100      "constructible(M,x) ==
   4.101         \<exists>i[M]. \<exists>Li[M]. ordinal(M,i) & is_Lset(M,i,Li) & x \<in> Li"
     5.1 --- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Nov 07 19:39:54 2006 +0100
     5.2 +++ b/src/ZF/Constructible/Datatype_absolute.thy	Tue Nov 07 19:40:13 2006 +0100
     5.3 @@ -10,7 +10,7 @@
     5.4  
     5.5  subsection{*The lfp of a continuous function can be expressed as a union*}
     5.6  
     5.7 -constdefs
     5.8 +definition
     5.9    directed :: "i=>o"
    5.10     "directed(A) == A\<noteq>0 & (\<forall>x\<in>A. \<forall>y\<in>A. x \<union> y \<in> A)"
    5.11  
    5.12 @@ -113,7 +113,7 @@
    5.13  
    5.14  subsection {*Absoluteness for "Iterates"*}
    5.15  
    5.16 -constdefs
    5.17 +definition
    5.18  
    5.19    iterates_MH :: "[i=>o, [i,i]=>o, i, i, i, i] => o"
    5.20     "iterates_MH(M,isF,v,n,g,z) ==
    5.21 @@ -207,7 +207,7 @@
    5.22  by (simp add: list_eq_lfp2 lfp_eq_Union list_fun_bnd_mono list_fun_contin)
    5.23  
    5.24  
    5.25 -constdefs
    5.26 +definition
    5.27    is_list_functor :: "[i=>o,i,i,i] => o"
    5.28      "is_list_functor(M,A,X,Z) == 
    5.29          \<exists>n1[M]. \<exists>AX[M]. 
    5.30 @@ -260,7 +260,7 @@
    5.31                formula_fun_contin)
    5.32  
    5.33  
    5.34 -constdefs
    5.35 +definition
    5.36    is_formula_functor :: "[i=>o,i,i] => o"
    5.37      "is_formula_functor(M,X,Z) == 
    5.38          \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M]. 
    5.39 @@ -278,7 +278,7 @@
    5.40  
    5.41  subsection{*@{term M} Contains the List and Formula Datatypes*}
    5.42  
    5.43 -constdefs
    5.44 +definition
    5.45    list_N :: "[i,i] => i"
    5.46      "list_N(A,n) == (\<lambda>X. {0} + A * X)^n (0)"
    5.47  
    5.48 @@ -339,7 +339,7 @@
    5.49  apply (simp add: list_imp_list_N) 
    5.50  done
    5.51  
    5.52 -constdefs
    5.53 +definition
    5.54    is_list_N :: "[i=>o,i,i,i] => o"
    5.55      "is_list_N(M,A,n,Z) == 
    5.56        \<exists>zero[M]. empty(M,zero) & 
    5.57 @@ -366,7 +366,7 @@
    5.58  by (induct_tac p, simp_all) 
    5.59  
    5.60  
    5.61 -constdefs
    5.62 +definition
    5.63    formula_N :: "i => i"
    5.64      "formula_N(n) == (\<lambda>X. ((nat*nat) + (nat*nat)) + (X*X + X)) ^ n (0)"
    5.65  
    5.66 @@ -441,14 +441,14 @@
    5.67                       le_imp_subset formula_N_mono)
    5.68  done
    5.69  
    5.70 -constdefs
    5.71 +definition
    5.72    is_formula_N :: "[i=>o,i,i] => o"
    5.73      "is_formula_N(M,n,Z) == 
    5.74        \<exists>zero[M]. empty(M,zero) & 
    5.75                  is_iterates(M, is_formula_functor(M), zero, n, Z)"
    5.76  
    5.77  
    5.78 -constdefs
    5.79 +definition
    5.80    
    5.81    mem_formula :: "[i=>o,i] => o"
    5.82      "mem_formula(M,p) == 
    5.83 @@ -584,7 +584,7 @@
    5.84  apply (simp add: nat_rec_succ)
    5.85  done
    5.86  
    5.87 -constdefs
    5.88 +definition
    5.89    is_eclose_n :: "[i=>o,i,i,i] => o"
    5.90      "is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z)"
    5.91  
    5.92 @@ -643,7 +643,7 @@
    5.93  subsection {*Absoluteness for @{term transrec}*}
    5.94  
    5.95  text{* @{term "transrec(a,H) \<equiv> wfrec(Memrel(eclose({a})), a, H)"} *}
    5.96 -constdefs
    5.97 +definition
    5.98  
    5.99    is_transrec :: "[i=>o, [i,i,i]=>o, i, i] => o"
   5.100     "is_transrec(M,MH,a,z) ==
   5.101 @@ -691,7 +691,7 @@
   5.102  subsection{*Absoluteness for the List Operator @{term length}*}
   5.103  text{*But it is never used.*}
   5.104  
   5.105 -constdefs
   5.106 +definition
   5.107    is_length :: "[i=>o,i,i,i] => o"
   5.108      "is_length(M,A,l,n) ==
   5.109         \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M].
   5.110 @@ -739,7 +739,7 @@
   5.111  apply (simp add: not_lt_iff_le nth_eq_0)
   5.112  done
   5.113  
   5.114 -constdefs
   5.115 +definition
   5.116    is_nth :: "[i=>o,i,i,i] => o"
   5.117      "is_nth(M,n,l,Z) ==
   5.118        \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)"
   5.119 @@ -757,7 +757,7 @@
   5.120  
   5.121  subsection{*Relativization and Absoluteness for the @{term formula} Constructors*}
   5.122  
   5.123 -constdefs
   5.124 +definition
   5.125    is_Member :: "[i=>o,i,i,i] => o"
   5.126       --{* because @{term "Member(x,y) \<equiv> Inl(Inl(\<langle>x,y\<rangle>))"}*}
   5.127      "is_Member(M,x,y,Z) ==
   5.128 @@ -771,7 +771,7 @@
   5.129       "M(Member(x,y)) <-> M(x) & M(y)"
   5.130  by (simp add: Member_def)
   5.131  
   5.132 -constdefs
   5.133 +definition
   5.134    is_Equal :: "[i=>o,i,i,i] => o"
   5.135       --{* because @{term "Equal(x,y) \<equiv> Inl(Inr(\<langle>x,y\<rangle>))"}*}
   5.136      "is_Equal(M,x,y,Z) ==
   5.137 @@ -784,7 +784,7 @@
   5.138  lemma (in M_trivial) Equal_in_M_iff [iff]: "M(Equal(x,y)) <-> M(x) & M(y)"
   5.139  by (simp add: Equal_def)
   5.140  
   5.141 -constdefs
   5.142 +definition
   5.143    is_Nand :: "[i=>o,i,i,i] => o"
   5.144       --{* because @{term "Nand(x,y) \<equiv> Inr(Inl(\<langle>x,y\<rangle>))"}*}
   5.145      "is_Nand(M,x,y,Z) ==
   5.146 @@ -797,7 +797,7 @@
   5.147  lemma (in M_trivial) Nand_in_M_iff [iff]: "M(Nand(x,y)) <-> M(x) & M(y)"
   5.148  by (simp add: Nand_def)
   5.149  
   5.150 -constdefs
   5.151 +definition
   5.152    is_Forall :: "[i=>o,i,i] => o"
   5.153       --{* because @{term "Forall(x) \<equiv> Inr(Inr(p))"}*}
   5.154      "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)"
   5.155 @@ -813,7 +813,7 @@
   5.156  
   5.157  subsection {*Absoluteness for @{term formula_rec}*}
   5.158  
   5.159 -constdefs
   5.160 +definition
   5.161  
   5.162    formula_rec_case :: "[[i,i]=>i, [i,i]=>i, [i,i,i,i]=>i, [i,i]=>i, i, i] => i"
   5.163      --{* the instance of @{term formula_case} in @{term formula_rec}*}
   5.164 @@ -847,7 +847,7 @@
   5.165  
   5.166  
   5.167  subsubsection{*Absoluteness for the Formula Operator @{term depth}*}
   5.168 -constdefs
   5.169 +definition
   5.170  
   5.171    is_depth :: "[i=>o,i,i] => o"
   5.172      "is_depth(M,p,n) ==
   5.173 @@ -873,7 +873,7 @@
   5.174  
   5.175  subsubsection{*@{term is_formula_case}: relativization of @{term formula_case}*}
   5.176  
   5.177 -constdefs
   5.178 +definition
   5.179  
   5.180   is_formula_case ::
   5.181      "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
   5.182 @@ -909,7 +909,7 @@
   5.183  
   5.184  subsubsection {*Absoluteness for @{term formula_rec}: Final Results*}
   5.185  
   5.186 -constdefs
   5.187 +definition
   5.188    is_formula_rec :: "[i=>o, [i,i,i]=>o, i, i] => o"
   5.189      --{* predicate to relativize the functional @{term formula_rec}*}
   5.190     "is_formula_rec(M,MH,p,z)  ==
     6.1 --- a/src/ZF/Constructible/Formula.thy	Tue Nov 07 19:39:54 2006 +0100
     6.2 +++ b/src/ZF/Constructible/Formula.thy	Tue Nov 07 19:40:13 2006 +0100
     6.3 @@ -21,22 +21,22 @@
     6.4  
     6.5  declare formula.intros [TC]
     6.6  
     6.7 -constdefs Neg :: "i=>i"
     6.8 +definition Neg :: "i=>i"
     6.9      "Neg(p) == Nand(p,p)"
    6.10  
    6.11 -constdefs And :: "[i,i]=>i"
    6.12 +definition And :: "[i,i]=>i"
    6.13      "And(p,q) == Neg(Nand(p,q))"
    6.14  
    6.15 -constdefs Or :: "[i,i]=>i"
    6.16 +definition Or :: "[i,i]=>i"
    6.17      "Or(p,q) == Nand(Neg(p),Neg(q))"
    6.18  
    6.19 -constdefs Implies :: "[i,i]=>i"
    6.20 +definition Implies :: "[i,i]=>i"
    6.21      "Implies(p,q) == Nand(p,Neg(q))"
    6.22  
    6.23 -constdefs Iff :: "[i,i]=>i"
    6.24 +definition Iff :: "[i,i]=>i"
    6.25      "Iff(p,q) == And(Implies(p,q), Implies(q,p))"
    6.26  
    6.27 -constdefs Exists :: "i=>i"
    6.28 +definition Exists :: "i=>i"
    6.29      "Exists(p) == Neg(Forall(Neg(p)))";
    6.30  
    6.31  lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula"
    6.32 @@ -76,10 +76,11 @@
    6.33  
    6.34  
    6.35  lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool"
    6.36 -by (induct_tac p, simp_all) 
    6.37 +by (induct set: formula) simp_all
    6.38  
    6.39 -syntax sats :: "[i,i,i] => o"
    6.40 -translations "sats(A,p,env)" == "satisfies(A,p)`env = 1"
    6.41 +abbreviation
    6.42 +  sats :: "[i,i,i] => o"
    6.43 +  "sats(A,p,env) == satisfies(A,p)`env = 1"
    6.44  
    6.45  lemma [simp]:
    6.46    "env \<in> list(A) 
    6.47 @@ -245,7 +246,7 @@
    6.48  
    6.49  subsection{*Renaming Some de Bruijn Variables*}
    6.50  
    6.51 -constdefs incr_var :: "[i,i]=>i"
    6.52 +definition incr_var :: "[i,i]=>i"
    6.53      "incr_var(x,nq) == if x<nq then x else succ(x)"
    6.54  
    6.55  lemma incr_var_lt: "x<nq ==> incr_var(x,nq) = x"
    6.56 @@ -333,7 +334,7 @@
    6.57  
    6.58  subsection{*Renaming all but the First de Bruijn Variable*}
    6.59  
    6.60 -constdefs incr_bv1 :: "i => i"
    6.61 +definition incr_bv1 :: "i => i"
    6.62      "incr_bv1(p) == incr_bv(p)`1"
    6.63  
    6.64  
    6.65 @@ -384,7 +385,7 @@
    6.66  subsection{*Definable Powerset*}
    6.67  
    6.68  text{*The definable powerset operation: Kunen's definition VI 1.1, page 165.*}
    6.69 -constdefs DPow :: "i => i"
    6.70 +definition DPow :: "i => i"
    6.71    "DPow(A) == {X \<in> Pow(A). 
    6.72                 \<exists>env \<in> list(A). \<exists>p \<in> formula. 
    6.73                   arity(p) \<le> succ(length(env)) & 
    6.74 @@ -506,7 +507,7 @@
    6.75  
    6.76  subsubsection{*The subset relation*}
    6.77  
    6.78 -constdefs subset_fm :: "[i,i]=>i"
    6.79 +definition subset_fm :: "[i,i]=>i"
    6.80      "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
    6.81  
    6.82  lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
    6.83 @@ -526,7 +527,7 @@
    6.84  
    6.85  subsubsection{*Transitive sets*}
    6.86  
    6.87 -constdefs transset_fm :: "i=>i"
    6.88 +definition transset_fm :: "i=>i"
    6.89     "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
    6.90  
    6.91  lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
    6.92 @@ -546,7 +547,7 @@
    6.93  
    6.94  subsubsection{*Ordinals*}
    6.95  
    6.96 -constdefs ordinal_fm :: "i=>i"
    6.97 +definition ordinal_fm :: "i=>i"
    6.98     "ordinal_fm(x) == 
    6.99        And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
   6.100  
   6.101 @@ -577,7 +578,7 @@
   6.102  
   6.103  subsection{* Constant Lset: Levels of the Constructible Universe *}
   6.104  
   6.105 -constdefs
   6.106 +definition
   6.107    Lset :: "i=>i"
   6.108      "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
   6.109  
   6.110 @@ -823,7 +824,7 @@
   6.111  
   6.112  
   6.113  text{*The rank function for the constructible universe*}
   6.114 -constdefs
   6.115 +definition
   6.116    lrank :: "i=>i" --{*Kunen's definition VI 1.7*}
   6.117      "lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
   6.118  
   6.119 @@ -983,7 +984,7 @@
   6.120  
   6.121  
   6.122  text{*A simpler version of @{term DPow}: no arity check!*}
   6.123 -constdefs DPow' :: "i => i"
   6.124 +definition DPow' :: "i => i"
   6.125    "DPow'(A) == {X \<in> Pow(A). 
   6.126                  \<exists>env \<in> list(A). \<exists>p \<in> formula. 
   6.127                      X = {x\<in>A. sats(A, p, Cons(x,env))}}"
     7.1 --- a/src/ZF/Constructible/Internalize.thy	Tue Nov 07 19:39:54 2006 +0100
     7.2 +++ b/src/ZF/Constructible/Internalize.thy	Tue Nov 07 19:40:13 2006 +0100
     7.3 @@ -10,7 +10,7 @@
     7.4  subsubsection{*The Formula @{term is_Inl}, Internalized*}
     7.5  
     7.6  (*  is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z) *)
     7.7 -constdefs Inl_fm :: "[i,i]=>i"
     7.8 +definition Inl_fm :: "[i,i]=>i"
     7.9      "Inl_fm(a,z) == Exists(And(empty_fm(0), pair_fm(0,succ(a),succ(z))))"
    7.10  
    7.11  lemma Inl_type [TC]:
    7.12 @@ -39,7 +39,7 @@
    7.13  subsubsection{*The Formula @{term is_Inr}, Internalized*}
    7.14  
    7.15  (*  is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z) *)
    7.16 -constdefs Inr_fm :: "[i,i]=>i"
    7.17 +definition Inr_fm :: "[i,i]=>i"
    7.18      "Inr_fm(a,z) == Exists(And(number1_fm(0), pair_fm(0,succ(a),succ(z))))"
    7.19  
    7.20  lemma Inr_type [TC]:
    7.21 @@ -69,7 +69,7 @@
    7.22  
    7.23  (* is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs) *)
    7.24  
    7.25 -constdefs Nil_fm :: "i=>i"
    7.26 +definition Nil_fm :: "i=>i"
    7.27      "Nil_fm(x) == Exists(And(empty_fm(0), Inl_fm(0,succ(x))))"
    7.28  
    7.29  lemma Nil_type [TC]: "x \<in> nat ==> Nil_fm(x) \<in> formula"
    7.30 @@ -97,7 +97,7 @@
    7.31  
    7.32  
    7.33  (*  "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)" *)
    7.34 -constdefs Cons_fm :: "[i,i,i]=>i"
    7.35 +definition Cons_fm :: "[i,i,i]=>i"
    7.36      "Cons_fm(a,l,Z) ==
    7.37         Exists(And(pair_fm(succ(a),succ(l),0), Inr_fm(0,succ(Z))))"
    7.38  
    7.39 @@ -128,7 +128,7 @@
    7.40  
    7.41  (* is_quasilist(M,xs) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))" *)
    7.42  
    7.43 -constdefs quasilist_fm :: "i=>i"
    7.44 +definition quasilist_fm :: "i=>i"
    7.45      "quasilist_fm(x) ==
    7.46         Or(Nil_fm(x), Exists(Exists(Cons_fm(1,0,succ(succ(x))))))"
    7.47  
    7.48 @@ -162,7 +162,7 @@
    7.49         (is_Nil(M,xs) --> empty(M,H)) &
    7.50         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
    7.51         (is_quasilist(M,xs) | empty(M,H))" *)
    7.52 -constdefs hd_fm :: "[i,i]=>i"
    7.53 +definition hd_fm :: "[i,i]=>i"
    7.54      "hd_fm(xs,H) == 
    7.55         And(Implies(Nil_fm(xs), empty_fm(H)),
    7.56             And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(H#+2,1)))),
    7.57 @@ -198,7 +198,7 @@
    7.58         (is_Nil(M,xs) --> T=xs) &
    7.59         (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
    7.60         (is_quasilist(M,xs) | empty(M,T))" *)
    7.61 -constdefs tl_fm :: "[i,i]=>i"
    7.62 +definition tl_fm :: "[i,i]=>i"
    7.63      "tl_fm(xs,T) ==
    7.64         And(Implies(Nil_fm(xs), Equal(T,xs)),
    7.65             And(Forall(Forall(Or(Neg(Cons_fm(1,0,xs#+2)), Equal(T#+2,0)))),
    7.66 @@ -234,7 +234,7 @@
    7.67     "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))" *)
    7.68  
    7.69  text{*The formula @{term p} has no free variables.*}
    7.70 -constdefs bool_of_o_fm :: "[i, i]=>i"
    7.71 +definition bool_of_o_fm :: "[i, i]=>i"
    7.72   "bool_of_o_fm(p,z) == 
    7.73      Or(And(p,number1_fm(z)),
    7.74         And(Neg(p),empty_fm(z)))"
    7.75 @@ -276,7 +276,7 @@
    7.76      "is_lambda(M, A, is_b, z) == 
    7.77         \<forall>p[M]. p \<in> z <->
    7.78          (\<exists>u[M]. \<exists>v[M]. u\<in>A & pair(M,u,v,p) & is_b(u,v))" *)
    7.79 -constdefs lambda_fm :: "[i, i, i]=>i"
    7.80 +definition lambda_fm :: "[i, i, i]=>i"
    7.81   "lambda_fm(p,A,z) == 
    7.82      Forall(Iff(Member(0,succ(z)),
    7.83              Exists(Exists(And(Member(1,A#+3),
    7.84 @@ -315,7 +315,7 @@
    7.85  
    7.86  (*    "is_Member(M,x,y,Z) ==
    7.87  	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" *)
    7.88 -constdefs Member_fm :: "[i,i,i]=>i"
    7.89 +definition Member_fm :: "[i,i,i]=>i"
    7.90      "Member_fm(x,y,Z) ==
    7.91         Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
    7.92                        And(Inl_fm(1,0), Inl_fm(0,Z#+2)))))"
    7.93 @@ -347,7 +347,7 @@
    7.94  
    7.95  (*    "is_Equal(M,x,y,Z) ==
    7.96  	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" *)
    7.97 -constdefs Equal_fm :: "[i,i,i]=>i"
    7.98 +definition Equal_fm :: "[i,i,i]=>i"
    7.99      "Equal_fm(x,y,Z) ==
   7.100         Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
   7.101                        And(Inr_fm(1,0), Inl_fm(0,Z#+2)))))"
   7.102 @@ -379,7 +379,7 @@
   7.103  
   7.104  (*    "is_Nand(M,x,y,Z) ==
   7.105  	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" *)
   7.106 -constdefs Nand_fm :: "[i,i,i]=>i"
   7.107 +definition Nand_fm :: "[i,i,i]=>i"
   7.108      "Nand_fm(x,y,Z) ==
   7.109         Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
   7.110                        And(Inl_fm(1,0), Inr_fm(0,Z#+2)))))"
   7.111 @@ -410,7 +410,7 @@
   7.112  subsubsection{*The Operator @{term is_Forall}, Internalized*}
   7.113  
   7.114  (* "is_Forall(M,p,Z) == \<exists>u[M]. is_Inr(M,p,u) & is_Inr(M,u,Z)" *)
   7.115 -constdefs Forall_fm :: "[i,i]=>i"
   7.116 +definition Forall_fm :: "[i,i]=>i"
   7.117      "Forall_fm(x,Z) ==
   7.118         Exists(And(Inr_fm(succ(x),0), Inr_fm(0,succ(Z))))"
   7.119  
   7.120 @@ -442,7 +442,7 @@
   7.121  
   7.122  (* is_and(M,a,b,z) == (number1(M,a)  & z=b) | 
   7.123                         (~number1(M,a) & empty(M,z)) *)
   7.124 -constdefs and_fm :: "[i,i,i]=>i"
   7.125 +definition and_fm :: "[i,i,i]=>i"
   7.126      "and_fm(a,b,z) ==
   7.127         Or(And(number1_fm(a), Equal(z,b)),
   7.128            And(Neg(number1_fm(a)),empty_fm(z)))"
   7.129 @@ -476,7 +476,7 @@
   7.130  (* is_or(M,a,b,z) == (number1(M,a)  & number1(M,z)) | 
   7.131                       (~number1(M,a) & z=b) *)
   7.132  
   7.133 -constdefs or_fm :: "[i,i,i]=>i"
   7.134 +definition or_fm :: "[i,i,i]=>i"
   7.135      "or_fm(a,b,z) ==
   7.136         Or(And(number1_fm(a), number1_fm(z)),
   7.137            And(Neg(number1_fm(a)), Equal(z,b)))"
   7.138 @@ -510,7 +510,7 @@
   7.139  
   7.140  (* is_not(M,a,z) == (number1(M,a)  & empty(M,z)) | 
   7.141                       (~number1(M,a) & number1(M,z)) *)
   7.142 -constdefs not_fm :: "[i,i]=>i"
   7.143 +definition not_fm :: "[i,i]=>i"
   7.144      "not_fm(a,z) ==
   7.145         Or(And(number1_fm(a), empty_fm(z)),
   7.146            And(Neg(number1_fm(a)), number1_fm(z)))"
   7.147 @@ -576,7 +576,7 @@
   7.148  *)
   7.149  
   7.150  text{*The three arguments of @{term p} are always 2, 1, 0 and z*}
   7.151 -constdefs is_recfun_fm :: "[i, i, i, i]=>i"
   7.152 +definition is_recfun_fm :: "[i, i, i, i]=>i"
   7.153   "is_recfun_fm(p,r,a,f) == 
   7.154     Forall(Iff(Member(0,succ(f)),
   7.155      Exists(Exists(Exists(
   7.156 @@ -638,7 +638,7 @@
   7.157  (* is_wfrec :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
   7.158      "is_wfrec(M,MH,r,a,z) == 
   7.159        \<exists>f[M]. M_is_recfun(M,MH,r,a,f) & MH(a,f,z)" *)
   7.160 -constdefs is_wfrec_fm :: "[i, i, i, i]=>i"
   7.161 +definition is_wfrec_fm :: "[i, i, i, i]=>i"
   7.162   "is_wfrec_fm(p,r,a,z) == 
   7.163      Exists(And(is_recfun_fm(p, succ(r), succ(a), 0),
   7.164             Exists(Exists(Exists(Exists(
   7.165 @@ -696,7 +696,7 @@
   7.166  
   7.167  subsubsection{*Binary Products, Internalized*}
   7.168  
   7.169 -constdefs cartprod_fm :: "[i,i,i]=>i"
   7.170 +definition cartprod_fm :: "[i,i,i]=>i"
   7.171  (* "cartprod(M,A,B,z) ==
   7.172          \<forall>u[M]. u \<in> z <-> (\<exists>x[M]. x\<in>A & (\<exists>y[M]. y\<in>B & pair(M,x,y,u)))" *)
   7.173      "cartprod_fm(A,B,z) ==
   7.174 @@ -736,7 +736,7 @@
   7.175           3      2       1        0
   7.176         number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
   7.177         cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"  *)
   7.178 -constdefs sum_fm :: "[i,i,i]=>i"
   7.179 +definition sum_fm :: "[i,i,i]=>i"
   7.180      "sum_fm(A,B,Z) ==
   7.181         Exists(Exists(Exists(Exists(
   7.182          And(number1_fm(2),
   7.183 @@ -771,7 +771,7 @@
   7.184  subsubsection{*The Operator @{term quasinat}*}
   7.185  
   7.186  (* "is_quasinat(M,z) == empty(M,z) | (\<exists>m[M]. successor(M,m,z))" *)
   7.187 -constdefs quasinat_fm :: "i=>i"
   7.188 +definition quasinat_fm :: "i=>i"
   7.189      "quasinat_fm(z) == Or(empty_fm(z), Exists(succ_fm(0,succ(z))))"
   7.190  
   7.191  lemma quasinat_type [TC]:
   7.192 @@ -808,7 +808,7 @@
   7.193         (\<forall>m[M]. successor(M,m,k) --> is_b(m,z)) &
   7.194         (is_quasinat(M,k) | empty(M,z))" *)
   7.195  text{*The formula @{term is_b} has free variables 1 and 0.*}
   7.196 -constdefs is_nat_case_fm :: "[i, i, i, i]=>i"
   7.197 +definition is_nat_case_fm :: "[i, i, i, i]=>i"
   7.198   "is_nat_case_fm(a,is_b,k,z) == 
   7.199      And(Implies(empty_fm(k), Equal(z,a)),
   7.200          And(Forall(Implies(succ_fm(0,succ(k)), 
   7.201 @@ -863,7 +863,7 @@
   7.202     "iterates_MH(M,isF,v,n,g,z) ==
   7.203          is_nat_case(M, v, \<lambda>m u. \<exists>gm[M]. fun_apply(M,g,m,gm) & isF(gm,u),
   7.204                      n, z)" *)
   7.205 -constdefs iterates_MH_fm :: "[i, i, i, i, i]=>i"
   7.206 +definition iterates_MH_fm :: "[i, i, i, i, i]=>i"
   7.207   "iterates_MH_fm(isF,v,n,g,z) == 
   7.208      is_nat_case_fm(v, 
   7.209        Exists(And(fun_apply_fm(succ(succ(succ(g))),2,0), 
   7.210 @@ -928,7 +928,7 @@
   7.211        \<exists>sn[M]. \<exists>msn[M]. successor(M,n,sn) & membership(M,sn,msn) &
   7.212         1       0       is_wfrec(M, iterates_MH(M,isF,v), msn, n, Z)"*)
   7.213  
   7.214 -constdefs is_iterates_fm :: "[i, i, i, i]=>i"
   7.215 +definition is_iterates_fm :: "[i, i, i, i]=>i"
   7.216   "is_iterates_fm(p,v,n,Z) == 
   7.217       Exists(Exists(
   7.218        And(succ_fm(n#+2,1),
   7.219 @@ -998,7 +998,7 @@
   7.220  
   7.221  (* is_eclose_n(M,A,n,Z) == is_iterates(M, big_union(M), A, n, Z) *)
   7.222  
   7.223 -constdefs eclose_n_fm :: "[i,i,i]=>i"
   7.224 +definition eclose_n_fm :: "[i,i,i]=>i"
   7.225    "eclose_n_fm(A,n,Z) == is_iterates_fm(big_union_fm(1,0), A, n, Z)"
   7.226  
   7.227  lemma eclose_n_fm_type [TC]:
   7.228 @@ -1034,7 +1034,7 @@
   7.229  (* mem_eclose(M,A,l) == 
   7.230        \<exists>n[M]. \<exists>eclosen[M]. 
   7.231         finite_ordinal(M,n) & is_eclose_n(M,A,n,eclosen) & l \<in> eclosen *)
   7.232 -constdefs mem_eclose_fm :: "[i,i]=>i"
   7.233 +definition mem_eclose_fm :: "[i,i]=>i"
   7.234      "mem_eclose_fm(x,y) ==
   7.235         Exists(Exists(
   7.236           And(finite_ordinal_fm(1),
   7.237 @@ -1066,7 +1066,7 @@
   7.238  subsubsection{*The Predicate ``Is @{term "eclose(A)"}''*}
   7.239  
   7.240  (* is_eclose(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_eclose(M,A,l) *)
   7.241 -constdefs is_eclose_fm :: "[i,i]=>i"
   7.242 +definition is_eclose_fm :: "[i,i]=>i"
   7.243      "is_eclose_fm(A,Z) ==
   7.244         Forall(Iff(Member(0,succ(Z)), mem_eclose_fm(succ(A),0)))"
   7.245  
   7.246 @@ -1095,7 +1095,7 @@
   7.247  
   7.248  subsubsection{*The List Functor, Internalized*}
   7.249  
   7.250 -constdefs list_functor_fm :: "[i,i,i]=>i"
   7.251 +definition list_functor_fm :: "[i,i,i]=>i"
   7.252  (* "is_list_functor(M,A,X,Z) ==
   7.253          \<exists>n1[M]. \<exists>AX[M].
   7.254           number1(M,n1) & cartprod(M,A,X,AX) & is_sum(M,n1,AX,Z)" *)
   7.255 @@ -1135,7 +1135,7 @@
   7.256        \<exists>zero[M]. empty(M,zero) & 
   7.257                  is_iterates(M, is_list_functor(M,A), zero, n, Z)" *)
   7.258  
   7.259 -constdefs list_N_fm :: "[i,i,i]=>i"
   7.260 +definition list_N_fm :: "[i,i,i]=>i"
   7.261    "list_N_fm(A,n,Z) == 
   7.262       Exists(
   7.263         And(empty_fm(0),
   7.264 @@ -1175,7 +1175,7 @@
   7.265  (* mem_list(M,A,l) == 
   7.266        \<exists>n[M]. \<exists>listn[M]. 
   7.267         finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> listn *)
   7.268 -constdefs mem_list_fm :: "[i,i]=>i"
   7.269 +definition mem_list_fm :: "[i,i]=>i"
   7.270      "mem_list_fm(x,y) ==
   7.271         Exists(Exists(
   7.272           And(finite_ordinal_fm(1),
   7.273 @@ -1207,7 +1207,7 @@
   7.274  subsubsection{*The Predicate ``Is @{term "list(A)"}''*}
   7.275  
   7.276  (* is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l) *)
   7.277 -constdefs is_list_fm :: "[i,i]=>i"
   7.278 +definition is_list_fm :: "[i,i]=>i"
   7.279      "is_list_fm(A,Z) ==
   7.280         Forall(Iff(Member(0,succ(Z)), mem_list_fm(succ(A),0)))"
   7.281  
   7.282 @@ -1236,7 +1236,7 @@
   7.283  
   7.284  subsubsection{*The Formula Functor, Internalized*}
   7.285  
   7.286 -constdefs formula_functor_fm :: "[i,i]=>i"
   7.287 +definition formula_functor_fm :: "[i,i]=>i"
   7.288  (*     "is_formula_functor(M,X,Z) ==
   7.289          \<exists>nat'[M]. \<exists>natnat[M]. \<exists>natnatsum[M]. \<exists>XX[M]. \<exists>X3[M].
   7.290             4           3               2       1       0
   7.291 @@ -1282,7 +1282,7 @@
   7.292  (*  "is_formula_N(M,n,Z) == 
   7.293        \<exists>zero[M]. empty(M,zero) & 
   7.294                  is_iterates(M, is_formula_functor(M), zero, n, Z)" *) 
   7.295 -constdefs formula_N_fm :: "[i,i]=>i"
   7.296 +definition formula_N_fm :: "[i,i]=>i"
   7.297    "formula_N_fm(n,Z) == 
   7.298       Exists(
   7.299         And(empty_fm(0),
   7.300 @@ -1322,7 +1322,7 @@
   7.301  (*  mem_formula(M,p) == 
   7.302        \<exists>n[M]. \<exists>formn[M]. 
   7.303         finite_ordinal(M,n) & is_formula_N(M,n,formn) & p \<in> formn *)
   7.304 -constdefs mem_formula_fm :: "i=>i"
   7.305 +definition mem_formula_fm :: "i=>i"
   7.306      "mem_formula_fm(x) ==
   7.307         Exists(Exists(
   7.308           And(finite_ordinal_fm(1),
   7.309 @@ -1354,7 +1354,7 @@
   7.310  subsubsection{*The Predicate ``Is @{term "formula"}''*}
   7.311  
   7.312  (* is_formula(M,Z) == \<forall>p[M]. p \<in> Z <-> mem_formula(M,p) *)
   7.313 -constdefs is_formula_fm :: "i=>i"
   7.314 +definition is_formula_fm :: "i=>i"
   7.315      "is_formula_fm(Z) == Forall(Iff(Member(0,succ(Z)), mem_formula_fm(0)))"
   7.316  
   7.317  lemma is_formula_type [TC]:
   7.318 @@ -1392,7 +1392,7 @@
   7.319         2       1         0
   7.320         upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
   7.321         is_wfrec(M,MH,mesa,a,z)" *)
   7.322 -constdefs is_transrec_fm :: "[i, i, i]=>i"
   7.323 +definition is_transrec_fm :: "[i, i, i]=>i"
   7.324   "is_transrec_fm(p,a,z) == 
   7.325      Exists(Exists(Exists(
   7.326        And(upair_fm(a#+3,a#+3,2),
     8.1 --- a/src/ZF/Constructible/L_axioms.thy	Tue Nov 07 19:39:54 2006 +0100
     8.2 +++ b/src/ZF/Constructible/L_axioms.thy	Tue Nov 07 19:40:13 2006 +0100
     8.3 @@ -114,7 +114,7 @@
     8.4  subsection{*Instantiation of the locale @{text reflection}*}
     8.5  
     8.6  text{*instances of locale constants*}
     8.7 -constdefs
     8.8 +definition
     8.9    L_F0 :: "[i=>o,i] => i"
    8.10      "L_F0(P,y) == \<mu> b. (\<exists>z. L(z) \<and> P(<y,z>)) --> (\<exists>z\<in>Lset(b). P(<y,z>))"
    8.11  
    8.12 @@ -127,7 +127,7 @@
    8.13  
    8.14  text{*We must use the meta-existential quantifier; otherwise the reflection
    8.15        terms become enormous!*}
    8.16 -constdefs
    8.17 +definition
    8.18    L_Reflects :: "[i=>o,[i,i]=>o] => prop"      ("(3REFLECTS/ [_,/ _])")
    8.19      "REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) &
    8.20                             (\<forall>a. Cl(a) --> (\<forall>x \<in> Lset(a). P(x) <-> Q(a,x))))"
    8.21 @@ -265,28 +265,26 @@
    8.22  
    8.23  subsubsection{*Some numbers to help write de Bruijn indices*}
    8.24  
    8.25 -syntax
    8.26 -    "3" :: i   ("3")
    8.27 -    "4" :: i   ("4")
    8.28 -    "5" :: i   ("5")
    8.29 -    "6" :: i   ("6")
    8.30 -    "7" :: i   ("7")
    8.31 -    "8" :: i   ("8")
    8.32 -    "9" :: i   ("9")
    8.33 -
    8.34 -translations
    8.35 -   "3"  == "succ(2)"
    8.36 -   "4"  == "succ(3)"
    8.37 -   "5"  == "succ(4)"
    8.38 -   "6"  == "succ(5)"
    8.39 -   "7"  == "succ(6)"
    8.40 -   "8"  == "succ(7)"
    8.41 -   "9"  == "succ(8)"
    8.42 +abbreviation
    8.43 +  digit3 :: i   ("3")
    8.44 +  "3 == succ(2)"
    8.45 +  digit4 :: i   ("4")
    8.46 +  "4 == succ(3)"
    8.47 +  digit5 :: i   ("5")
    8.48 +  "5 == succ(4)"
    8.49 +  digit6 :: i   ("6")
    8.50 +  "6 == succ(5)"
    8.51 +  digit7 :: i   ("7")
    8.52 +  "7 == succ(6)"
    8.53 +  digit8 :: i   ("8")
    8.54 +  "8 == succ(7)"
    8.55 +  digit9 :: i   ("9")
    8.56 +  "9 == succ(8)"
    8.57  
    8.58  
    8.59  subsubsection{*The Empty Set, Internalized*}
    8.60  
    8.61 -constdefs empty_fm :: "i=>i"
    8.62 +definition empty_fm :: "i=>i"
    8.63      "empty_fm(x) == Forall(Neg(Member(0,succ(x))))"
    8.64  
    8.65  lemma empty_type [TC]:
    8.66 @@ -324,7 +322,7 @@
    8.67  
    8.68  subsubsection{*Unordered Pairs, Internalized*}
    8.69  
    8.70 -constdefs upair_fm :: "[i,i,i]=>i"
    8.71 +definition upair_fm :: "[i,i,i]=>i"
    8.72      "upair_fm(x,y,z) ==
    8.73         And(Member(x,z),
    8.74             And(Member(y,z),
    8.75 @@ -366,7 +364,7 @@
    8.76  
    8.77  subsubsection{*Ordered pairs, Internalized*}
    8.78  
    8.79 -constdefs pair_fm :: "[i,i,i]=>i"
    8.80 +definition pair_fm :: "[i,i,i]=>i"
    8.81      "pair_fm(x,y,z) ==
    8.82         Exists(And(upair_fm(succ(x),succ(x),0),
    8.83                Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0),
    8.84 @@ -398,7 +396,7 @@
    8.85  
    8.86  subsubsection{*Binary Unions, Internalized*}
    8.87  
    8.88 -constdefs union_fm :: "[i,i,i]=>i"
    8.89 +definition union_fm :: "[i,i,i]=>i"
    8.90      "union_fm(x,y,z) ==
    8.91         Forall(Iff(Member(0,succ(z)),
    8.92                    Or(Member(0,succ(x)),Member(0,succ(y)))))"
    8.93 @@ -429,7 +427,7 @@
    8.94  
    8.95  subsubsection{*Set ``Cons,'' Internalized*}
    8.96  
    8.97 -constdefs cons_fm :: "[i,i,i]=>i"
    8.98 +definition cons_fm :: "[i,i,i]=>i"
    8.99      "cons_fm(x,y,z) ==
   8.100         Exists(And(upair_fm(succ(x),succ(x),0),
   8.101                    union_fm(0,succ(y),succ(z))))"
   8.102 @@ -461,7 +459,7 @@
   8.103  
   8.104  subsubsection{*Successor Function, Internalized*}
   8.105  
   8.106 -constdefs succ_fm :: "[i,i]=>i"
   8.107 +definition succ_fm :: "[i,i]=>i"
   8.108      "succ_fm(x,y) == cons_fm(x,x,y)"
   8.109  
   8.110  lemma succ_type [TC]:
   8.111 @@ -491,7 +489,7 @@
   8.112  subsubsection{*The Number 1, Internalized*}
   8.113  
   8.114  (* "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))" *)
   8.115 -constdefs number1_fm :: "i=>i"
   8.116 +definition number1_fm :: "i=>i"
   8.117      "number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))"
   8.118  
   8.119  lemma number1_type [TC]:
   8.120 @@ -520,7 +518,7 @@
   8.121  subsubsection{*Big Union, Internalized*}
   8.122  
   8.123  (*  "big_union(M,A,z) == \<forall>x[M]. x \<in> z <-> (\<exists>y[M]. y\<in>A & x \<in> y)" *)
   8.124 -constdefs big_union_fm :: "[i,i]=>i"
   8.125 +definition big_union_fm :: "[i,i]=>i"
   8.126      "big_union_fm(A,z) ==
   8.127         Forall(Iff(Member(0,succ(z)),
   8.128                    Exists(And(Member(0,succ(succ(A))), Member(1,0)))))"
   8.129 @@ -600,7 +598,7 @@
   8.130  
   8.131  subsubsection{*Membership Relation, Internalized*}
   8.132  
   8.133 -constdefs Memrel_fm :: "[i,i]=>i"
   8.134 +definition Memrel_fm :: "[i,i]=>i"
   8.135      "Memrel_fm(A,r) ==
   8.136         Forall(Iff(Member(0,succ(r)),
   8.137                    Exists(And(Member(0,succ(succ(A))),
   8.138 @@ -633,7 +631,7 @@
   8.139  
   8.140  subsubsection{*Predecessor Set, Internalized*}
   8.141  
   8.142 -constdefs pred_set_fm :: "[i,i,i,i]=>i"
   8.143 +definition pred_set_fm :: "[i,i,i,i]=>i"
   8.144      "pred_set_fm(A,x,r,B) ==
   8.145         Forall(Iff(Member(0,succ(B)),
   8.146                    Exists(And(Member(0,succ(succ(r))),
   8.147 @@ -671,7 +669,7 @@
   8.148  
   8.149  (* "is_domain(M,r,z) ==
   8.150          \<forall>x[M]. (x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *)
   8.151 -constdefs domain_fm :: "[i,i]=>i"
   8.152 +definition domain_fm :: "[i,i]=>i"
   8.153      "domain_fm(r,z) ==
   8.154         Forall(Iff(Member(0,succ(z)),
   8.155                    Exists(And(Member(0,succ(succ(r))),
   8.156 @@ -705,7 +703,7 @@
   8.157  
   8.158  (* "is_range(M,r,z) ==
   8.159          \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *)
   8.160 -constdefs range_fm :: "[i,i]=>i"
   8.161 +definition range_fm :: "[i,i]=>i"
   8.162      "range_fm(r,z) ==
   8.163         Forall(Iff(Member(0,succ(z)),
   8.164                    Exists(And(Member(0,succ(succ(r))),
   8.165 @@ -740,7 +738,7 @@
   8.166  (* "is_field(M,r,z) ==
   8.167          \<exists>dr[M]. is_domain(M,r,dr) &
   8.168              (\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *)
   8.169 -constdefs field_fm :: "[i,i]=>i"
   8.170 +definition field_fm :: "[i,i]=>i"
   8.171      "field_fm(r,z) ==
   8.172         Exists(And(domain_fm(succ(r),0),
   8.173                Exists(And(range_fm(succ(succ(r)),0),
   8.174 @@ -775,7 +773,7 @@
   8.175  
   8.176  (* "image(M,r,A,z) ==
   8.177          \<forall>y[M]. (y \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *)
   8.178 -constdefs image_fm :: "[i,i,i]=>i"
   8.179 +definition image_fm :: "[i,i,i]=>i"
   8.180      "image_fm(r,A,z) ==
   8.181         Forall(Iff(Member(0,succ(z)),
   8.182                    Exists(And(Member(0,succ(succ(r))),
   8.183 @@ -810,7 +808,7 @@
   8.184  
   8.185  (* "pre_image(M,r,A,z) ==
   8.186          \<forall>x[M]. x \<in> z <-> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *)
   8.187 -constdefs pre_image_fm :: "[i,i,i]=>i"
   8.188 +definition pre_image_fm :: "[i,i,i]=>i"
   8.189      "pre_image_fm(r,A,z) ==
   8.190         Forall(Iff(Member(0,succ(z)),
   8.191                    Exists(And(Member(0,succ(succ(r))),
   8.192 @@ -846,7 +844,7 @@
   8.193  (* "fun_apply(M,f,x,y) ==
   8.194          (\<exists>xs[M]. \<exists>fxs[M].
   8.195           upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *)
   8.196 -constdefs fun_apply_fm :: "[i,i,i]=>i"
   8.197 +definition fun_apply_fm :: "[i,i,i]=>i"
   8.198      "fun_apply_fm(f,x,y) ==
   8.199         Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1),
   8.200                           And(image_fm(succ(succ(f)), 1, 0),
   8.201 @@ -881,7 +879,7 @@
   8.202  
   8.203  (* "is_relation(M,r) ==
   8.204          (\<forall>z[M]. z\<in>r --> (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *)
   8.205 -constdefs relation_fm :: "i=>i"
   8.206 +definition relation_fm :: "i=>i"
   8.207      "relation_fm(r) ==
   8.208         Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))"
   8.209  
   8.210 @@ -913,7 +911,7 @@
   8.211  (* "is_function(M,r) ==
   8.212          \<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M].
   8.213             pair(M,x,y,p) --> pair(M,x,y',p') --> p\<in>r --> p'\<in>r --> y=y'" *)
   8.214 -constdefs function_fm :: "i=>i"
   8.215 +definition function_fm :: "i=>i"
   8.216      "function_fm(r) ==
   8.217         Forall(Forall(Forall(Forall(Forall(
   8.218           Implies(pair_fm(4,3,1),
   8.219 @@ -950,7 +948,7 @@
   8.220          is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &
   8.221          (\<forall>u[M]. u\<in>r --> (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) --> y\<in>B))" *)
   8.222  
   8.223 -constdefs typed_function_fm :: "[i,i,i]=>i"
   8.224 +definition typed_function_fm :: "[i,i,i]=>i"
   8.225      "typed_function_fm(A,B,r) ==
   8.226         And(function_fm(r),
   8.227           And(relation_fm(r),
   8.228 @@ -1009,7 +1007,7 @@
   8.229                 (\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M].
   8.230                  pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) &
   8.231                  xy \<in> s & yz \<in> r)" *)
   8.232 -constdefs composition_fm :: "[i,i,i]=>i"
   8.233 +definition composition_fm :: "[i,i,i]=>i"
   8.234    "composition_fm(r,s,t) ==
   8.235       Forall(Iff(Member(0,succ(t)),
   8.236               Exists(Exists(Exists(Exists(Exists(
   8.237 @@ -1048,7 +1046,7 @@
   8.238          typed_function(M,A,B,f) &
   8.239          (\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M].
   8.240            pair(M,x,y,p) --> pair(M,x',y,p') --> p\<in>f --> p'\<in>f --> x=x')" *)
   8.241 -constdefs injection_fm :: "[i,i,i]=>i"
   8.242 +definition injection_fm :: "[i,i,i]=>i"
   8.243   "injection_fm(A,B,f) ==
   8.244      And(typed_function_fm(A,B,f),
   8.245         Forall(Forall(Forall(Forall(Forall(
   8.246 @@ -1088,7 +1086,7 @@
   8.247      "surjection(M,A,B,f) ==
   8.248          typed_function(M,A,B,f) &
   8.249          (\<forall>y[M]. y\<in>B --> (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))" *)
   8.250 -constdefs surjection_fm :: "[i,i,i]=>i"
   8.251 +definition surjection_fm :: "[i,i,i]=>i"
   8.252   "surjection_fm(A,B,f) ==
   8.253      And(typed_function_fm(A,B,f),
   8.254         Forall(Implies(Member(0,succ(B)),
   8.255 @@ -1124,7 +1122,7 @@
   8.256  
   8.257  (*   bijection :: "[i=>o,i,i,i] => o"
   8.258      "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *)
   8.259 -constdefs bijection_fm :: "[i,i,i]=>i"
   8.260 +definition bijection_fm :: "[i,i,i]=>i"
   8.261   "bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))"
   8.262  
   8.263  lemma bijection_type [TC]:
   8.264 @@ -1156,7 +1154,7 @@
   8.265  
   8.266  (* "restriction(M,r,A,z) ==
   8.267          \<forall>x[M]. x \<in> z <-> (x \<in> r & (\<exists>u[M]. u\<in>A & (\<exists>v[M]. pair(M,u,v,x))))" *)
   8.268 -constdefs restriction_fm :: "[i,i,i]=>i"
   8.269 +definition restriction_fm :: "[i,i,i]=>i"
   8.270      "restriction_fm(r,A,z) ==
   8.271         Forall(Iff(Member(0,succ(z)),
   8.272                    And(Member(0,succ(r)),
   8.273 @@ -1197,7 +1195,7 @@
   8.274              pair(M,fx,fy,q) --> (p\<in>r <-> q\<in>s))))"
   8.275    *)
   8.276  
   8.277 -constdefs order_isomorphism_fm :: "[i,i,i,i,i]=>i"
   8.278 +definition order_isomorphism_fm :: "[i,i,i,i,i]=>i"
   8.279   "order_isomorphism_fm(A,r,B,s,f) ==
   8.280     And(bijection_fm(A,B,f),
   8.281       Forall(Implies(Member(0,succ(A)),
   8.282 @@ -1244,7 +1242,7 @@
   8.283          ordinal(M,a) & ~ empty(M,a) &
   8.284          (\<forall>x[M]. x\<in>a --> (\<exists>y[M]. y\<in>a & successor(M,x,y)))" *)
   8.285  
   8.286 -constdefs limit_ordinal_fm :: "i=>i"
   8.287 +definition limit_ordinal_fm :: "i=>i"
   8.288      "limit_ordinal_fm(x) ==
   8.289          And(ordinal_fm(x),
   8.290              And(Neg(empty_fm(x)),
   8.291 @@ -1280,7 +1278,7 @@
   8.292  (*     "finite_ordinal(M,a) == 
   8.293  	ordinal(M,a) & ~ limit_ordinal(M,a) & 
   8.294          (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x))" *)
   8.295 -constdefs finite_ordinal_fm :: "i=>i"
   8.296 +definition finite_ordinal_fm :: "i=>i"
   8.297      "finite_ordinal_fm(x) ==
   8.298         And(ordinal_fm(x),
   8.299            And(Neg(limit_ordinal_fm(x)),
   8.300 @@ -1313,7 +1311,7 @@
   8.301  subsubsection{*Omega: The Set of Natural Numbers*}
   8.302  
   8.303  (* omega(M,a) == limit_ordinal(M,a) & (\<forall>x[M]. x\<in>a --> ~ limit_ordinal(M,x)) *)
   8.304 -constdefs omega_fm :: "i=>i"
   8.305 +definition omega_fm :: "i=>i"
   8.306      "omega_fm(x) ==
   8.307         And(limit_ordinal_fm(x),
   8.308             Forall(Implies(Member(0,succ(x)),
     9.1 --- a/src/ZF/Constructible/MetaExists.thy	Tue Nov 07 19:39:54 2006 +0100
     9.2 +++ b/src/ZF/Constructible/MetaExists.thy	Tue Nov 07 19:40:13 2006 +0100
     9.3 @@ -10,12 +10,12 @@
     9.4  text{*Allows quantification over any term having sort @{text logic}.  Used to
     9.5  quantify over classes.  Yields a proposition rather than a FOL formula.*}
     9.6  
     9.7 -constdefs
     9.8 +definition
     9.9    ex :: "(('a::{}) => prop) => prop"            (binder "?? " 0)
    9.10    "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
    9.11  
    9.12 -syntax (xsymbols)
    9.13 -  "?? "        :: "[idts, o] => o"             ("(3\<Or>_./ _)" [0, 0] 0)
    9.14 +notation (xsymbols)
    9.15 +  ex  (binder "\<Or>" 0)
    9.16  
    9.17  lemma meta_exI: "PROP P(x) ==> (?? x. PROP P(x))"
    9.18  proof (unfold ex_def)
    10.1 --- a/src/ZF/Constructible/Normal.thy	Tue Nov 07 19:39:54 2006 +0100
    10.2 +++ b/src/ZF/Constructible/Normal.thy	Tue Nov 07 19:40:13 2006 +0100
    10.3 @@ -18,7 +18,7 @@
    10.4  
    10.5  subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}
    10.6  
    10.7 -constdefs
    10.8 +definition
    10.9    Closed :: "(i=>o) => o"
   10.10      "Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"
   10.11  
   10.12 @@ -200,7 +200,7 @@
   10.13  
   10.14  subsection {*Normal Functions*} 
   10.15  
   10.16 -constdefs
   10.17 +definition
   10.18    mono_le_subset :: "(i=>i) => o"
   10.19      "mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"
   10.20  
   10.21 @@ -372,7 +372,7 @@
   10.22        only if @{text F} is continuous: succ is not bounded above by any 
   10.23        normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
   10.24  *}
   10.25 -constdefs
   10.26 +definition
   10.27    normalize :: "[i=>i, i] => i"
   10.28      "normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"
   10.29  
   10.30 @@ -424,12 +424,12 @@
   10.31  text {*This is the well-known transfinite enumeration of the cardinal 
   10.32  numbers.*}
   10.33  
   10.34 -constdefs
   10.35 +definition
   10.36    Aleph :: "i => i"
   10.37      "Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
   10.38  
   10.39 -syntax (xsymbols)
   10.40 -  Aleph :: "i => i"   ("\<aleph>_" [90] 90)
   10.41 +notation (xsymbols)
   10.42 +  Aleph  ("\<aleph>_" [90] 90)
   10.43  
   10.44  lemma Card_Aleph [simp, intro]:
   10.45       "Ord(a) ==> Card(Aleph(a))"
   10.46 @@ -458,4 +458,3 @@
   10.47  done
   10.48  
   10.49  end
   10.50 -
    11.1 --- a/src/ZF/Constructible/Rank.thy	Tue Nov 07 19:39:54 2006 +0100
    11.2 +++ b/src/ZF/Constructible/Rank.thy	Tue Nov 07 19:40:13 2006 +0100
    11.3 @@ -136,7 +136,7 @@
    11.4  done
    11.5  
    11.6  
    11.7 -constdefs
    11.8 +definition
    11.9    
   11.10    obase :: "[i=>o,i,i] => i"
   11.11         --{*the domain of @{text om}, eventually shown to equal @{text A}*}
   11.12 @@ -414,7 +414,7 @@
   11.13  subsubsection{*Ordinal Addition*}
   11.14  
   11.15  (*FIXME: update to use new techniques!!*)
   11.16 -constdefs
   11.17 +definition
   11.18   (*This expresses ordinal addition in the language of ZF.  It also 
   11.19     provides an abbreviation that can be used in the instance of strong
   11.20     replacement below.  Here j is used to define the relation, namely
   11.21 @@ -725,7 +725,7 @@
   11.22  
   11.23  text{*This function, defined using replacement, is a rank function for
   11.24  well-founded relations within the class M.*}
   11.25 -constdefs
   11.26 +definition
   11.27   wellfoundedrank :: "[i=>o,i,i] => i"
   11.28      "wellfoundedrank(M,r,A) ==
   11.29          {p. x\<in>A, \<exists>y[M]. \<exists>f[M]. 
    12.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Tue Nov 07 19:39:54 2006 +0100
    12.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Tue Nov 07 19:40:13 2006 +0100
    12.3 @@ -30,7 +30,7 @@
    12.4            (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
    12.5              fun_apply(M,f,j,fj) & successor(M,j,sj) &
    12.6              fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
    12.7 -constdefs rtran_closure_mem_fm :: "[i,i,i]=>i"
    12.8 +definition rtran_closure_mem_fm :: "[i,i,i]=>i"
    12.9   "rtran_closure_mem_fm(A,r,p) ==
   12.10     Exists(Exists(Exists(
   12.11      And(omega_fm(2),
   12.12 @@ -87,7 +87,7 @@
   12.13  (*  "rtran_closure(M,r,s) ==
   12.14          \<forall>A[M]. is_field(M,r,A) -->
   12.15           (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))" *)
   12.16 -constdefs rtran_closure_fm :: "[i,i]=>i"
   12.17 +definition rtran_closure_fm :: "[i,i]=>i"
   12.18   "rtran_closure_fm(r,s) ==
   12.19     Forall(Implies(field_fm(succ(r),0),
   12.20                    Forall(Iff(Member(0,succ(succ(s))),
   12.21 @@ -121,7 +121,7 @@
   12.22  
   12.23  (*  "tran_closure(M,r,t) ==
   12.24           \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *)
   12.25 -constdefs tran_closure_fm :: "[i,i]=>i"
   12.26 +definition tran_closure_fm :: "[i,i]=>i"
   12.27   "tran_closure_fm(r,s) ==
   12.28     Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))"
   12.29  
   12.30 @@ -293,7 +293,7 @@
   12.31  
   12.32  (* "is_nth(M,n,l,Z) ==
   12.33        \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *)
   12.34 -constdefs nth_fm :: "[i,i,i]=>i"
   12.35 +definition nth_fm :: "[i,i,i]=>i"
   12.36      "nth_fm(n,l,Z) == 
   12.37         Exists(And(is_iterates_fm(tl_fm(1,0), succ(l), succ(n), 0), 
   12.38                hd_fm(0,succ(Z))))"
    13.1 --- a/src/ZF/Constructible/Relative.thy	Tue Nov 07 19:39:54 2006 +0100
    13.2 +++ b/src/ZF/Constructible/Relative.thy	Tue Nov 07 19:40:13 2006 +0100
    13.3 @@ -9,7 +9,7 @@
    13.4  
    13.5  subsection{* Relativized versions of standard set-theoretic concepts *}
    13.6  
    13.7 -constdefs
    13.8 +definition
    13.9    empty :: "[i=>o,i] => o"
   13.10      "empty(M,z) == \<forall>x[M]. x \<notin> z"
   13.11  
   13.12 @@ -236,7 +236,7 @@
   13.13  
   13.14  
   13.15  subsection {*The relativized ZF axioms*}
   13.16 -constdefs
   13.17 +definition
   13.18  
   13.19    extensionality :: "(i=>o) => o"
   13.20      "extensionality(M) ==
   13.21 @@ -441,7 +441,7 @@
   13.22  
   13.23  
   13.24  text{*More constants, for order types*}
   13.25 -constdefs
   13.26 +definition
   13.27  
   13.28    order_isomorphism :: "[i=>o,i,i,i,i,i] => o"
   13.29      "order_isomorphism(M,A,r,B,s,f) ==
   13.30 @@ -712,7 +712,7 @@
   13.31  
   13.32  subsubsection {*Absoluteness for @{term Lambda}*}
   13.33  
   13.34 -constdefs
   13.35 +definition
   13.36   is_lambda :: "[i=>o, i, [i,i]=>o, i] => o"
   13.37      "is_lambda(M, A, is_b, z) ==
   13.38         \<forall>p[M]. p \<in> z <->
   13.39 @@ -893,7 +893,7 @@
   13.40  	   (\<lambda>x\<in>nat. if (\<exists>y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x))
   13.41  		     then 1 else 0)"
   13.42  
   13.43 -  constdefs
   13.44 +  definition
   13.45      natnumber :: "[i=>o,i,i] => o"
   13.46        "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1"
   13.47  
   13.48 @@ -1312,7 +1312,7 @@
   13.49  
   13.50  subsection{*Relativization and Absoluteness for Boolean Operators*}
   13.51  
   13.52 -constdefs
   13.53 +definition
   13.54    is_bool_of_o :: "[i=>o, o, i] => o"
   13.55     "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))"
   13.56  
   13.57 @@ -1365,7 +1365,7 @@
   13.58  
   13.59  subsection{*Relativization and Absoluteness for List Operators*}
   13.60  
   13.61 -constdefs
   13.62 +definition
   13.63  
   13.64    is_Nil :: "[i=>o, i] => o"
   13.65       --{* because @{term "[] \<equiv> Inl(0)"}*}
   13.66 @@ -1390,7 +1390,7 @@
   13.67  by (simp add: is_Cons_def Cons_def)
   13.68  
   13.69  
   13.70 -constdefs
   13.71 +definition
   13.72  
   13.73    quasilist :: "i => o"
   13.74      "quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"
    14.1 --- a/src/ZF/Constructible/Satisfies_absolute.thy	Tue Nov 07 19:39:54 2006 +0100
    14.2 +++ b/src/ZF/Constructible/Satisfies_absolute.thy	Tue Nov 07 19:40:13 2006 +0100
    14.3 @@ -17,7 +17,7 @@
    14.4           2          1                0
    14.5          is_formula_N(M,n,formula_n) & p \<notin> formula_n &
    14.6          successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p \<in> formula_sn" *)
    14.7 -constdefs depth_fm :: "[i,i]=>i"
    14.8 +definition depth_fm :: "[i,i]=>i"
    14.9    "depth_fm(p,n) == 
   14.10       Exists(Exists(Exists(
   14.11         And(formula_N_fm(n#+3,1),
   14.12 @@ -66,7 +66,7 @@
   14.13                       is_Nand(M,x,y,v) --> is_c(x,y,z)) &
   14.14        (\<forall>x[M]. x\<in>formula --> is_Forall(M,x,v) --> is_d(x,z))" *)
   14.15  
   14.16 -constdefs formula_case_fm :: "[i, i, i, i, i, i]=>i"
   14.17 +definition formula_case_fm :: "[i, i, i, i, i, i]=>i"
   14.18   "formula_case_fm(is_a, is_b, is_c, is_d, v, z) == 
   14.19          And(Forall(Forall(Implies(finite_ordinal_fm(1), 
   14.20                             Implies(finite_ordinal_fm(0), 
   14.21 @@ -173,7 +173,7 @@
   14.22  
   14.23  subsection {*Absoluteness for the Function @{term satisfies}*}
   14.24  
   14.25 -constdefs
   14.26 +definition
   14.27    is_depth_apply :: "[i=>o,i,i,i] => o"
   14.28     --{*Merely a useful abbreviation for the sequel.*}
   14.29     "is_depth_apply(M,h,p,z) ==
   14.30 @@ -193,7 +193,7 @@
   14.31  
   14.32  text{*These constants let us instantiate the parameters @{term a}, @{term b},
   14.33        @{term c}, @{term d}, etc., of the locale @{text Formula_Rec}.*}
   14.34 -constdefs
   14.35 +definition
   14.36    satisfies_a :: "[i,i,i]=>i"
   14.37     "satisfies_a(A) == 
   14.38      \<lambda>x y. \<lambda>env \<in> list(A). bool_of_o (nth(x,env) \<in> nth(y,env))"
   14.39 @@ -504,7 +504,7 @@
   14.40        2        1         0
   14.41  	finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
   14.42  	fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z) *)
   14.43 -constdefs depth_apply_fm :: "[i,i,i]=>i"
   14.44 +definition depth_apply_fm :: "[i,i,i]=>i"
   14.45      "depth_apply_fm(h,p,z) ==
   14.46         Exists(Exists(Exists(
   14.47          And(finite_ordinal_fm(2),
   14.48 @@ -547,7 +547,7 @@
   14.49   		       is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx \<in> ny, z),
   14.50                  zz)  *)
   14.51  
   14.52 -constdefs satisfies_is_a_fm :: "[i,i,i,i]=>i"
   14.53 +definition satisfies_is_a_fm :: "[i,i,i,i]=>i"
   14.54   "satisfies_is_a_fm(A,x,y,z) ==
   14.55     Forall(
   14.56       Implies(is_list_fm(succ(A),0),
   14.57 @@ -598,7 +598,7 @@
   14.58                        \<exists>nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
   14.59                  zz) *)
   14.60  
   14.61 -constdefs satisfies_is_b_fm :: "[i,i,i,i]=>i"
   14.62 +definition satisfies_is_b_fm :: "[i,i,i,i]=>i"
   14.63   "satisfies_is_b_fm(A,x,y,z) ==
   14.64     Forall(
   14.65       Implies(is_list_fm(succ(A),0),
   14.66 @@ -647,7 +647,7 @@
   14.67                   (\<exists>pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
   14.68                  zz) *)
   14.69  
   14.70 -constdefs satisfies_is_c_fm :: "[i,i,i,i,i]=>i"
   14.71 +definition satisfies_is_c_fm :: "[i,i,i,i,i]=>i"
   14.72   "satisfies_is_c_fm(A,h,p,q,zz) ==
   14.73     Forall(
   14.74       Implies(is_list_fm(succ(A),0),
   14.75 @@ -700,7 +700,7 @@
   14.76                    z),
   14.77                 zz) *)
   14.78  
   14.79 -constdefs satisfies_is_d_fm :: "[i,i,i,i]=>i"
   14.80 +definition satisfies_is_d_fm :: "[i,i,i,i]=>i"
   14.81   "satisfies_is_d_fm(A,h,p,zz) ==
   14.82     Forall(
   14.83       Implies(is_list_fm(succ(A),0),
   14.84 @@ -754,7 +754,7 @@
   14.85                                  satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
   14.86                 zz) *)
   14.87  
   14.88 -constdefs satisfies_MH_fm :: "[i,i,i,i]=>i"
   14.89 +definition satisfies_MH_fm :: "[i,i,i,i]=>i"
   14.90   "satisfies_MH_fm(A,u,f,zz) ==
   14.91     Forall(
   14.92       Implies(is_formula_fm(0),
    15.1 --- a/src/ZF/Constructible/WF_absolute.thy	Tue Nov 07 19:39:54 2006 +0100
    15.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Tue Nov 07 19:40:13 2006 +0100
    15.3 @@ -9,7 +9,7 @@
    15.4  
    15.5  subsection{*Transitive closure without fixedpoints*}
    15.6  
    15.7 -constdefs
    15.8 +definition
    15.9    rtrancl_alt :: "[i,i]=>i"
   15.10      "rtrancl_alt(A,r) ==
   15.11         {p \<in> A*A. \<exists>n\<in>nat. \<exists>f \<in> succ(n) -> A.
   15.12 @@ -59,7 +59,7 @@
   15.13  	  intro: rtrancl_alt_subset_rtrancl rtrancl_subset_rtrancl_alt)
   15.14  
   15.15  
   15.16 -constdefs
   15.17 +definition
   15.18  
   15.19    rtran_closure_mem :: "[i=>o,i,i,i] => o"
   15.20      --{*The property of belonging to @{text "rtran_closure(r)"}*}
    16.1 --- a/src/ZF/Constructible/WFrec.thy	Tue Nov 07 19:39:54 2006 +0100
    16.2 +++ b/src/ZF/Constructible/WFrec.thy	Tue Nov 07 19:40:13 2006 +0100
    16.3 @@ -271,7 +271,7 @@
    16.4  
    16.5  subsection{*Relativization of the ZF Predicate @{term is_recfun}*}
    16.6  
    16.7 -constdefs
    16.8 +definition
    16.9    M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
   16.10     "M_is_recfun(M,MH,r,a,f) == 
   16.11       \<forall>z[M]. z \<in> f <-> 
    17.1 --- a/src/ZF/Constructible/Wellorderings.thy	Tue Nov 07 19:39:54 2006 +0100
    17.2 +++ b/src/ZF/Constructible/Wellorderings.thy	Tue Nov 07 19:40:13 2006 +0100
    17.3 @@ -16,7 +16,7 @@
    17.4  
    17.5  subsection{*Wellorderings*}
    17.6  
    17.7 -constdefs
    17.8 +definition
    17.9    irreflexive :: "[i=>o,i,i]=>o"
   17.10      "irreflexive(M,A,r) == \<forall>x[M]. x\<in>A --> <x,x> \<notin> r"
   17.11    
    18.1 --- a/src/ZF/ex/Commutation.thy	Tue Nov 07 19:39:54 2006 +0100
    18.2 +++ b/src/ZF/ex/Commutation.thy	Tue Nov 07 19:40:13 2006 +0100
    18.3 @@ -4,41 +4,41 @@
    18.4      Copyright   1995  TU Muenchen
    18.5  
    18.6  Commutation theory for proving the Church Rosser theorem
    18.7 -	ported from Isabelle/HOL  by Sidi Ould Ehmety
    18.8 +        ported from Isabelle/HOL  by Sidi Ould Ehmety
    18.9  *)
   18.10  
   18.11  theory Commutation imports Main begin
   18.12  
   18.13 -constdefs
   18.14 +definition
   18.15    square  :: "[i, i, i, i] => o"
   18.16 -   "square(r,s,t,u) ==
   18.17 -     (\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
   18.18 +  "square(r,s,t,u) ==
   18.19 +    (\<forall>a b. <a,b> \<in> r --> (\<forall>c. <a, c> \<in> s --> (\<exists>x. <b,x> \<in> t & <c,x> \<in> u)))"
   18.20  
   18.21    commute :: "[i, i] => o"
   18.22 -   "commute(r,s) == square(r,s,s,r)"
   18.23 +  "commute(r,s) == square(r,s,s,r)"
   18.24  
   18.25    diamond :: "i=>o"
   18.26 -   "diamond(r)   == commute(r, r)"
   18.27 +  "diamond(r)   == commute(r, r)"
   18.28  
   18.29    strip :: "i=>o"
   18.30 -   "strip(r) == commute(r^*, r)"
   18.31 +  "strip(r) == commute(r^*, r)"
   18.32  
   18.33    Church_Rosser :: "i => o"
   18.34 -   "Church_Rosser(r) == (\<forall>x y. <x,y> \<in>  (r Un converse(r))^* -->
   18.35 -	 	 	 (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
   18.36 +  "Church_Rosser(r) == (\<forall>x y. <x,y> \<in>  (r Un converse(r))^* -->
   18.37 +                        (\<exists>z. <x,z> \<in> r^* & <y,z> \<in> r^*))"
   18.38    confluent :: "i=>o"
   18.39 -   "confluent(r) == diamond(r^*)"
   18.40 +  "confluent(r) == diamond(r^*)"
   18.41  
   18.42  
   18.43  lemma square_sym: "square(r,s,t,u) ==> square(s,r,u,t)"
   18.44 -by (unfold square_def, blast)
   18.45 +  unfolding square_def by blast
   18.46  
   18.47  lemma square_subset: "[| square(r,s,t,u); t \<subseteq> t' |] ==> square(r,s,t',u)"
   18.48 -by (unfold square_def, blast)
   18.49 +  unfolding square_def by blast
   18.50  
   18.51  
   18.52 -lemma square_rtrancl [rule_format]: 
   18.53 -     "square(r,s,s,t) --> field(s)<=field(t) --> square(r^*,s,s,t^*)"
   18.54 +lemma square_rtrancl:
   18.55 +  "square(r,s,s,t) ==> field(s)<=field(t) ==> square(r^*,s,s,t^*)"
   18.56  apply (unfold square_def, clarify)
   18.57  apply (erule rtrancl_induct)
   18.58  apply (blast intro: rtrancl_refl)
   18.59 @@ -46,23 +46,22 @@
   18.60  done
   18.61  
   18.62  (* A special case of square_rtrancl_on *)
   18.63 -lemma diamond_strip: 
   18.64 - "diamond(r) ==> strip(r)"
   18.65 +lemma diamond_strip:
   18.66 +  "diamond(r) ==> strip(r)"
   18.67  apply (unfold diamond_def commute_def strip_def)
   18.68  apply (rule square_rtrancl, simp_all)
   18.69  done
   18.70  
   18.71  (*** commute ***)
   18.72  
   18.73 -lemma commute_sym: 
   18.74 -    "commute(r,s) ==> commute(s,r)"
   18.75 -by (unfold commute_def, blast intro: square_sym)
   18.76 +lemma commute_sym: "commute(r,s) ==> commute(s,r)"
   18.77 +  unfolding commute_def by (blast intro: square_sym)
   18.78  
   18.79 -lemma commute_rtrancl [rule_format]: 
   18.80 -    "commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)"
   18.81 -apply (unfold commute_def, clarify)
   18.82 +lemma commute_rtrancl:
   18.83 +  "commute(r,s) ==> field(r)=field(s) ==> commute(r^*,s^*)"
   18.84 +apply (unfold commute_def)
   18.85  apply (rule square_rtrancl)
   18.86 -apply (rule square_sym [THEN square_rtrancl, THEN square_sym]) 
   18.87 +apply (rule square_sym [THEN square_rtrancl, THEN square_sym])
   18.88  apply (simp_all add: rtrancl_field)
   18.89  done
   18.90  
   18.91 @@ -77,20 +76,20 @@
   18.92  done
   18.93  
   18.94  lemma commute_Un: "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)"
   18.95 -by (unfold commute_def square_def, blast)
   18.96 +  unfolding commute_def square_def by blast
   18.97  
   18.98 -lemma diamond_Un: 
   18.99 +lemma diamond_Un:
  18.100       "[| diamond(r); diamond(s); commute(r, s) |] ==> diamond(r Un s)"
  18.101 -by (unfold diamond_def, blast intro: commute_Un commute_sym) 
  18.102 +  unfolding diamond_def by (blast intro: commute_Un commute_sym)
  18.103  
  18.104 -lemma diamond_confluent: 
  18.105 +lemma diamond_confluent:
  18.106      "diamond(r) ==> confluent(r)"
  18.107  apply (unfold diamond_def confluent_def)
  18.108  apply (erule commute_rtrancl, simp)
  18.109  done
  18.110  
  18.111 -lemma confluent_Un: 
  18.112 - "[| confluent(r); confluent(s); commute(r^*, s^*); 
  18.113 +lemma confluent_Un:
  18.114 + "[| confluent(r); confluent(s); commute(r^*, s^*);
  18.115       relation(r); relation(s) |] ==> confluent(r Un s)"
  18.116  apply (unfold confluent_def)
  18.117  apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
  18.118 @@ -98,7 +97,7 @@
  18.119  done
  18.120  
  18.121  
  18.122 -lemma diamond_to_confluence: 
  18.123 +lemma diamond_to_confluence:
  18.124       "[| diamond(r); s \<subseteq> r; r<= s^* |] ==> confluent(s)"
  18.125  apply (drule rtrancl_subset [symmetric], assumption)
  18.126  apply (simp_all add: confluent_def)
  18.127 @@ -108,9 +107,9 @@
  18.128  
  18.129  (*** Church_Rosser ***)
  18.130  
  18.131 -lemma Church_Rosser1: 
  18.132 +lemma Church_Rosser1:
  18.133       "Church_Rosser(r) ==> confluent(r)"
  18.134 -apply (unfold confluent_def Church_Rosser_def square_def 
  18.135 +apply (unfold confluent_def Church_Rosser_def square_def
  18.136                commute_def diamond_def, auto)
  18.137  apply (drule converseI)
  18.138  apply (simp (no_asm_use) add: rtrancl_converse [symmetric])
  18.139 @@ -121,9 +120,9 @@
  18.140  done
  18.141  
  18.142  
  18.143 -lemma Church_Rosser2: 
  18.144 +lemma Church_Rosser2:
  18.145       "confluent(r) ==> Church_Rosser(r)"
  18.146 -apply (unfold confluent_def Church_Rosser_def square_def 
  18.147 +apply (unfold confluent_def Church_Rosser_def square_def
  18.148                commute_def diamond_def, auto)
  18.149  apply (frule fieldI1)
  18.150  apply (simp add: rtrancl_field)
  18.151 @@ -134,6 +133,6 @@
  18.152  
  18.153  
  18.154  lemma Church_Rosser: "Church_Rosser(r) <-> confluent(r)"
  18.155 -by (blast intro: Church_Rosser1 Church_Rosser2)
  18.156 +  by (blast intro: Church_Rosser1 Church_Rosser2)
  18.157  
  18.158 -end          
  18.159 +end
    19.1 --- a/src/ZF/ex/Group.thy	Tue Nov 07 19:39:54 2006 +0100
    19.2 +++ b/src/ZF/ex/Group.thy	Tue Nov 07 19:40:13 2006 +0100
    19.3 @@ -20,22 +20,22 @@
    19.4    one :: i ("\<one>\<index>")
    19.5  *)
    19.6  
    19.7 -constdefs
    19.8 +definition
    19.9    carrier :: "i => i"
   19.10 -   "carrier(M) == fst(M)"
   19.11 +  "carrier(M) == fst(M)"
   19.12  
   19.13    mmult :: "[i, i, i] => i" (infixl "\<cdot>\<index>" 70)
   19.14 -   "mmult(M,x,y) == fst(snd(M)) ` <x,y>"
   19.15 +  "mmult(M,x,y) == fst(snd(M)) ` <x,y>"
   19.16  
   19.17    one :: "i => i" ("\<one>\<index>")
   19.18 -   "one(M) == fst(snd(snd(M)))"
   19.19 +  "one(M) == fst(snd(snd(M)))"
   19.20  
   19.21    update_carrier :: "[i,i] => i"
   19.22 -   "update_carrier(M,A) == <A,snd(M)>"
   19.23 +  "update_carrier(M,A) == <A,snd(M)>"
   19.24  
   19.25 -constdefs (structure G)
   19.26 +definition
   19.27    m_inv :: "i => i => i" ("inv\<index> _" [81] 80)
   19.28 -  "inv x == (THE y. y \<in> carrier(G) & y \<cdot> x = \<one> & x \<cdot> y = \<one>)"
   19.29 +  "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>)"
   19.30  
   19.31  locale monoid = struct G +
   19.32    assumes m_closed [intro, simp]:
   19.33 @@ -294,7 +294,7 @@
   19.34  
   19.35  subsection {* Direct Products *}
   19.36  
   19.37 -constdefs
   19.38 +definition
   19.39    DirProdGroup :: "[i,i] => i"  (infixr "\<Otimes>" 80)
   19.40    "G \<Otimes> H == <carrier(G) \<times> carrier(H),
   19.41                (\<lambda><<g,h>, <g', h'>>
   19.42 @@ -332,7 +332,7 @@
   19.43  
   19.44  subsection {* Isomorphisms *}
   19.45  
   19.46 -constdefs
   19.47 +definition
   19.48    hom :: "[i,i] => i"
   19.49    "hom(G,H) ==
   19.50      {h \<in> carrier(G) -> carrier(H).
   19.51 @@ -358,7 +358,7 @@
   19.52  
   19.53  subsection {* Isomorphisms *}
   19.54  
   19.55 -constdefs
   19.56 +definition
   19.57    iso :: "[i,i] => i"  (infixr "\<cong>" 60)
   19.58    "G \<cong> H == hom(G,H) \<inter> bij(carrier(G), carrier(H))"
   19.59  
   19.60 @@ -478,7 +478,7 @@
   19.61  
   19.62  subsection {* Bijections of a Set, Permutation Groups, Automorphism Groups *}
   19.63  
   19.64 -constdefs
   19.65 +definition
   19.66    BijGroup :: "i=>i"
   19.67    "BijGroup(S) ==
   19.68      <bij(S,S),
   19.69 @@ -513,7 +513,7 @@
   19.70  by (simp add: iso_def)
   19.71  
   19.72  
   19.73 -constdefs
   19.74 +definition
   19.75    auto :: "i=>i"
   19.76    "auto(G) == iso(G,G)"
   19.77  
   19.78 @@ -551,32 +551,28 @@
   19.79  
   19.80  subsection{*Cosets and Quotient Groups*}
   19.81  
   19.82 -constdefs (structure G)
   19.83 +definition
   19.84    r_coset  :: "[i,i,i] => i"    (infixl "#>\<index>" 60)
   19.85 -   "H #> a == \<Union>h\<in>H. {h \<cdot> a}"
   19.86 +  "H #>\<^bsub>G\<^esub> a == \<Union>h\<in>H. {h \<cdot>\<^bsub>G\<^esub> a}"
   19.87  
   19.88    l_coset  :: "[i,i,i] => i"    (infixl "<#\<index>" 60)
   19.89 -   "a <# H == \<Union>h\<in>H. {a \<cdot> h}"
   19.90 +  "a <#\<^bsub>G\<^esub> H == \<Union>h\<in>H. {a \<cdot>\<^bsub>G\<^esub> h}"
   19.91  
   19.92    RCOSETS  :: "[i,i] => i"          ("rcosets\<index> _" [81] 80)
   19.93 -   "rcosets H == \<Union>a\<in>carrier(G). {H #> a}"
   19.94 +  "rcosets\<^bsub>G\<^esub> H == \<Union>a\<in>carrier(G). {H #>\<^bsub>G\<^esub> a}"
   19.95  
   19.96    set_mult :: "[i,i,i] => i"    (infixl "<#>\<index>" 60)
   19.97 -   "H <#> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot> k}"
   19.98 +  "H <#>\<^bsub>G\<^esub> K == \<Union>h\<in>H. \<Union>k\<in>K. {h \<cdot>\<^bsub>G\<^esub> k}"
   19.99  
  19.100    SET_INV  :: "[i,i] => i"  ("set'_inv\<index> _" [81] 80)
  19.101 -   "set_inv H == \<Union>h\<in>H. {inv h}"
  19.102 +  "set_inv\<^bsub>G\<^esub> H == \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
  19.103  
  19.104  
  19.105  locale normal = subgroup + group +
  19.106    assumes coset_eq: "(\<forall>x \<in> carrier(G). H #> x = x <# H)"
  19.107  
  19.108 -
  19.109 -syntax
  19.110 -  "@normal" :: "[i,i] => i"  (infixl "\<lhd>" 60)
  19.111 -
  19.112 -translations
  19.113 -  "H \<lhd> G" == "normal(H,G)"
  19.114 +notation
  19.115 +  normal  (infixl "\<lhd>" 60)
  19.116  
  19.117  
  19.118  subsection {*Basic Properties of Cosets*}
  19.119 @@ -836,9 +832,9 @@
  19.120  
  19.121  subsubsection{*Two distinct right cosets are disjoint*}
  19.122  
  19.123 -constdefs (structure G)
  19.124 +definition
  19.125    r_congruent :: "[i,i] => i" ("rcong\<index> _" [60] 60)
  19.126 -   "rcong H == {<x,y> \<in> carrier(G) * carrier(G). inv x \<cdot> y \<in> H}"
  19.127 +  "rcong\<^bsub>G\<^esub> H == {<x,y> \<in> carrier(G) * carrier(G). inv\<^bsub>G\<^esub> x \<cdot>\<^bsub>G\<^esub> y \<in> H}"
  19.128  
  19.129  
  19.130  lemma (in subgroup) equiv_rcong:
  19.131 @@ -903,7 +899,7 @@
  19.132  
  19.133  subsection {*Order of a Group and Lagrange's Theorem*}
  19.134  
  19.135 -constdefs
  19.136 +definition
  19.137    order :: "i => i"
  19.138    "order(S) == |carrier(S)|"
  19.139  
  19.140 @@ -975,11 +971,11 @@
  19.141  
  19.142  subsection {*Quotient Groups: Factorization of a Group*}
  19.143  
  19.144 -constdefs (structure G)
  19.145 +definition
  19.146    FactGroup :: "[i,i] => i" (infixl "Mod" 65)
  19.147      --{*Actually defined for groups rather than monoids*}
  19.148    "G Mod H == 
  19.149 -     <rcosets\<^bsub>G\<^esub> H, \<lambda><K1,K2> \<in> (rcosets\<^bsub>G\<^esub> H) \<times> (rcosets\<^bsub>G\<^esub> H). K1 <#> K2, H, 0>"
  19.150 +     <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>"
  19.151  
  19.152  lemma (in normal) setmult_closed:
  19.153       "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
  19.154 @@ -1038,7 +1034,7 @@
  19.155  text{*The quotient by the kernel of a homomorphism is isomorphic to the 
  19.156    range of that homomorphism.*}
  19.157  
  19.158 -constdefs
  19.159 +definition
  19.160    kernel :: "[i,i,i] => i" 
  19.161      --{*the kernel of a homomorphism*}
  19.162    "kernel(G,H,h) == {x \<in> carrier(G). h ` x = \<one>\<^bsub>H\<^esub>}";
    20.1 --- a/src/ZF/ex/Ramsey.thy	Tue Nov 07 19:39:54 2006 +0100
    20.2 +++ b/src/ZF/ex/Ramsey.thy	Tue Nov 07 19:40:13 2006 +0100
    20.3 @@ -27,7 +27,8 @@
    20.4  *)
    20.5  
    20.6  theory Ramsey imports Main begin
    20.7 -constdefs
    20.8 +
    20.9 +definition
   20.10    Symmetric :: "i=>o"
   20.11      "Symmetric(E) == (\<forall>x y. <x,y>:E --> <y,x>:E)"
   20.12  
    21.1 --- a/src/ZF/ex/Ring.thy	Tue Nov 07 19:39:54 2006 +0100
    21.2 +++ b/src/ZF/ex/Ring.thy	Tue Nov 07 19:40:13 2006 +0100
    21.3 @@ -13,15 +13,15 @@
    21.4    zero :: i ("\<zero>\<index>")
    21.5  *)
    21.6  
    21.7 -constdefs
    21.8 +definition
    21.9    add_field :: "i => i"
   21.10 -   "add_field(M) == fst(snd(snd(snd(M))))"
   21.11 +  "add_field(M) = fst(snd(snd(snd(M))))"
   21.12  
   21.13    ring_add :: "[i, i, i] => i" (infixl "\<oplus>\<index>" 65)
   21.14 -   "ring_add(M,x,y) == add_field(M) ` <x,y>"
   21.15 +  "ring_add(M,x,y) = add_field(M) ` <x,y>"
   21.16  
   21.17    zero :: "i => i" ("\<zero>\<index>")
   21.18 -   "zero(M) == fst(snd(snd(snd(snd(M)))))"
   21.19 +  "zero(M) = fst(snd(snd(snd(snd(M)))))"
   21.20  
   21.21  
   21.22  lemma add_field_eq [simp]: "add_field(<C,M,I,A,z>) = A"
   21.23 @@ -36,12 +36,12 @@
   21.24  
   21.25  text {* Derived operations. *}
   21.26  
   21.27 -constdefs (structure R)
   21.28 +definition
   21.29    a_inv :: "[i,i] => i" ("\<ominus>\<index> _" [81] 80)
   21.30    "a_inv(R) == m_inv (<carrier(R), add_field(R), zero(R), 0>)"
   21.31  
   21.32    minus :: "[i,i,i] => i" (infixl "\<ominus>\<index>" 65)
   21.33 -  "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y == x \<oplus> (\<ominus> y)"
   21.34 +  "\<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)"
   21.35  
   21.36  locale abelian_monoid = struct G +
   21.37    assumes a_comm_monoid: 
   21.38 @@ -170,8 +170,10 @@
   21.39    The following proofs are from Jacobson, Basic Algebra I, pp.~88--89
   21.40  *}
   21.41  
   21.42 -lemma (in ring) l_null [simp]:
   21.43 -  "x \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>"
   21.44 +context ring
   21.45 +begin
   21.46 +
   21.47 +lemma l_null [simp]: "x \<in> carrier(R) \<Longrightarrow> \<zero> \<cdot> x = \<zero>"
   21.48  proof -
   21.49    assume R: "x \<in> carrier(R)"
   21.50    then have "\<zero> \<cdot> x \<oplus> \<zero> \<cdot> x = (\<zero> \<oplus> \<zero>) \<cdot> x"
   21.51 @@ -181,8 +183,7 @@
   21.52    with R show ?thesis by (simp del: r_zero)
   21.53  qed
   21.54  
   21.55 -lemma (in ring) r_null [simp]:
   21.56 -  "x \<in> carrier(R) \<Longrightarrow> x \<cdot> \<zero> = \<zero>"
   21.57 +lemma r_null [simp]: "x \<in> carrier(R) \<Longrightarrow> x \<cdot> \<zero> = \<zero>"
   21.58  proof -
   21.59    assume R: "x \<in> carrier(R)"
   21.60    then have "x \<cdot> \<zero> \<oplus> x \<cdot> \<zero> = x \<cdot> (\<zero> \<oplus> \<zero>)"
   21.61 @@ -192,7 +193,7 @@
   21.62    with R show ?thesis by (simp del: r_zero)
   21.63  qed
   21.64  
   21.65 -lemma (in ring) l_minus:
   21.66 +lemma l_minus:
   21.67    "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> \<ominus> x \<cdot> y = \<ominus> (x \<cdot> y)"
   21.68  proof -
   21.69    assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
   21.70 @@ -203,7 +204,7 @@
   21.71    with R show ?thesis by (simp add: a_assoc r_neg)
   21.72  qed
   21.73  
   21.74 -lemma (in ring) r_minus:
   21.75 +lemma r_minus:
   21.76    "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<cdot> \<ominus> y = \<ominus> (x \<cdot> y)"
   21.77  proof -
   21.78    assume R: "x \<in> carrier(R)" "y \<in> carrier(R)"
   21.79 @@ -214,16 +215,18 @@
   21.80    with R show ?thesis by (simp add: a_assoc r_neg)
   21.81  qed
   21.82  
   21.83 -lemma (in ring) minus_eq:
   21.84 +lemma minus_eq:
   21.85    "\<lbrakk>x \<in> carrier(R); y \<in> carrier(R)\<rbrakk> \<Longrightarrow> x \<ominus> y = x \<oplus> \<ominus> y"
   21.86    by (simp only: minus_def)
   21.87  
   21.88 +end
   21.89 +
   21.90  
   21.91  subsection {* Morphisms *}
   21.92  
   21.93 -constdefs
   21.94 +definition
   21.95    ring_hom :: "[i,i] => i"
   21.96 -  "ring_hom(R,S) == 
   21.97 +  "ring_hom(R,S) ==
   21.98      {h \<in> carrier(R) -> carrier(S).
   21.99        (\<forall>x y. x \<in> carrier(R) & y \<in> carrier(R) -->
  21.100          h ` (x \<cdot>\<^bsub>R\<^esub> y) = (h ` x) \<cdot>\<^bsub>S\<^esub> (h ` y) &
  21.101 @@ -287,4 +290,3 @@
  21.102  done
  21.103  
  21.104  end
  21.105 -