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;
```