src/ZF/OrdQuant.thy
changeset 24893 b8ef7afe3a6b
parent 18324 d1c4b1112e33
child 26339 7825c83c9eff
     1.1 --- a/src/ZF/OrdQuant.thy	Sun Oct 07 15:49:25 2007 +0200
     1.2 +++ b/src/ZF/OrdQuant.thy	Sun Oct 07 21:19:31 2007 +0200
     1.3 @@ -9,17 +9,18 @@
     1.4  
     1.5  subsection {*Quantifiers and union operator for ordinals*}
     1.6  
     1.7 -constdefs
     1.8 -
     1.9 +definition
    1.10    (* Ordinal Quantifiers *)
    1.11 -  oall :: "[i, i => o] => o"
    1.12 +  oall :: "[i, i => o] => o"  where
    1.13      "oall(A, P) == ALL x. x<A --> P(x)"
    1.14  
    1.15 -  oex :: "[i, i => o] => o"
    1.16 +definition
    1.17 +  oex :: "[i, i => o] => o"  where
    1.18      "oex(A, P)  == EX x. x<A & P(x)"
    1.19  
    1.20 +definition
    1.21    (* Ordinal Union *)
    1.22 -  OUnion :: "[i, i => i] => i"
    1.23 +  OUnion :: "[i, i => i] => i"  where
    1.24      "OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
    1.25  
    1.26  syntax
    1.27 @@ -28,9 +29,9 @@
    1.28    "@OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
    1.29  
    1.30  translations
    1.31 -  "ALL x<a. P"  == "oall(a, %x. P)"
    1.32 -  "EX x<a. P"   == "oex(a, %x. P)"
    1.33 -  "UN x<a. B"   == "OUnion(a, %x. B)"
    1.34 +  "ALL x<a. P"  == "CONST oall(a, %x. P)"
    1.35 +  "EX x<a. P"   == "CONST oex(a, %x. P)"
    1.36 +  "UN x<a. B"   == "CONST OUnion(a, %x. B)"
    1.37  
    1.38  syntax (xsymbols)
    1.39    "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
    1.40 @@ -194,11 +195,12 @@
    1.41  
    1.42  subsection {*Quantification over a class*}
    1.43  
    1.44 -constdefs
    1.45 -  "rall"     :: "[i=>o, i=>o] => o"
    1.46 +definition
    1.47 +  "rall"     :: "[i=>o, i=>o] => o"  where
    1.48      "rall(M, P) == ALL x. M(x) --> P(x)"
    1.49  
    1.50 -  "rex"      :: "[i=>o, i=>o] => o"
    1.51 +definition
    1.52 +  "rex"      :: "[i=>o, i=>o] => o"  where
    1.53      "rex(M, P) == EX x. M(x) & P(x)"
    1.54  
    1.55  syntax
    1.56 @@ -213,8 +215,8 @@
    1.57    "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
    1.58  
    1.59  translations
    1.60 -  "ALL x[M]. P"  == "rall(M, %x. P)"
    1.61 -  "EX x[M]. P"   == "rex(M, %x. P)"
    1.62 +  "ALL x[M]. P"  == "CONST rall(M, %x. P)"
    1.63 +  "EX x[M]. P"   == "CONST rex(M, %x. P)"
    1.64  
    1.65  
    1.66  subsubsection{*Relativized universal quantifier*}
    1.67 @@ -340,7 +342,8 @@
    1.68  
    1.69  subsubsection{*Sets as Classes*}
    1.70  
    1.71 -constdefs setclass :: "[i,i] => o"       ("##_" [40] 40)
    1.72 +definition
    1.73 +  setclass :: "[i,i] => o"       ("##_" [40] 40)  where
    1.74     "setclass(A) == %x. x : A"
    1.75  
    1.76  lemma setclass_iff [simp]: "setclass(A,x) <-> x : A"
    1.77 @@ -355,41 +358,8 @@
    1.78  
    1.79  ML
    1.80  {*
    1.81 -val oall_def = thm "oall_def"
    1.82 -val oex_def = thm "oex_def"
    1.83 -val OUnion_def = thm "OUnion_def"
    1.84 -
    1.85 -val oallI = thm "oallI";
    1.86 -val ospec = thm "ospec";
    1.87 -val oallE = thm "oallE";
    1.88 -val rev_oallE = thm "rev_oallE";
    1.89 -val oall_simp = thm "oall_simp";
    1.90 -val oall_cong = thm "oall_cong";
    1.91 -val oexI = thm "oexI";
    1.92 -val oexCI = thm "oexCI";
    1.93 -val oexE = thm "oexE";
    1.94 -val oex_cong = thm "oex_cong";
    1.95 -val OUN_I = thm "OUN_I";
    1.96 -val OUN_E = thm "OUN_E";
    1.97 -val OUN_iff = thm "OUN_iff";
    1.98 -val OUN_cong = thm "OUN_cong";
    1.99 -val lt_induct = thm "lt_induct";
   1.100 -
   1.101 -val rall_def = thm "rall_def"
   1.102 -val rex_def = thm "rex_def"
   1.103 -
   1.104 -val rallI = thm "rallI";
   1.105 -val rspec = thm "rspec";
   1.106 -val rallE = thm "rallE";
   1.107 -val rev_oallE = thm "rev_oallE";
   1.108 -val rall_cong = thm "rall_cong";
   1.109 -val rexI = thm "rexI";
   1.110 -val rexCI = thm "rexCI";
   1.111 -val rexE = thm "rexE";
   1.112 -val rex_cong = thm "rex_cong";
   1.113 -
   1.114  val Ord_atomize =
   1.115 -    atomize ([("OrdQuant.oall", [ospec]),("OrdQuant.rall", [rspec])]@
   1.116 +    atomize ([("OrdQuant.oall", [@{thm ospec}]),("OrdQuant.rall", [@{thm rspec}])]@
   1.117                   ZF_conn_pairs,
   1.118               ZF_mem_pairs);
   1.119  change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
   1.120 @@ -400,19 +370,19 @@
   1.121  ML_setup {*
   1.122  local
   1.123  
   1.124 -val unfold_rex_tac = unfold_tac [rex_def];
   1.125 +val unfold_rex_tac = unfold_tac [@{thm rex_def}];
   1.126  fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
   1.127  val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
   1.128  
   1.129 -val unfold_rall_tac = unfold_tac [rall_def];
   1.130 +val unfold_rall_tac = unfold_tac [@{thm rall_def}];
   1.131  fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;
   1.132  val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
   1.133  
   1.134  in
   1.135  
   1.136 -val defREX_regroup = Simplifier.simproc (the_context ())
   1.137 +val defREX_regroup = Simplifier.simproc @{theory}
   1.138    "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
   1.139 -val defRALL_regroup = Simplifier.simproc (the_context ())
   1.140 +val defRALL_regroup = Simplifier.simproc @{theory}
   1.141    "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
   1.142  
   1.143  end;