src/ZF/Constructible/Formula.thy
 changeset 21404 eb85850d3eb7 parent 21233 5a5c8ea5f66a child 32960 69916a850301
```     1.1 --- a/src/ZF/Constructible/Formula.thy	Fri Nov 17 02:19:55 2006 +0100
1.2 +++ b/src/ZF/Constructible/Formula.thy	Fri Nov 17 02:20:03 2006 +0100
1.3 @@ -21,23 +21,29 @@
1.4
1.5  declare formula.intros [TC]
1.6
1.7 -definition Neg :: "i=>i"
1.8 -    "Neg(p) == Nand(p,p)"
1.9 +definition
1.10 +  Neg :: "i=>i" where
1.11 +  "Neg(p) == Nand(p,p)"
1.12
1.13 -definition And :: "[i,i]=>i"
1.14 -    "And(p,q) == Neg(Nand(p,q))"
1.15 +definition
1.16 +  And :: "[i,i]=>i" where
1.17 +  "And(p,q) == Neg(Nand(p,q))"
1.18
1.19 -definition Or :: "[i,i]=>i"
1.20 -    "Or(p,q) == Nand(Neg(p),Neg(q))"
1.21 +definition
1.22 +  Or :: "[i,i]=>i" where
1.23 +  "Or(p,q) == Nand(Neg(p),Neg(q))"
1.24
1.25 -definition Implies :: "[i,i]=>i"
1.26 -    "Implies(p,q) == Nand(p,Neg(q))"
1.27 +definition
1.28 +  Implies :: "[i,i]=>i" where
1.29 +  "Implies(p,q) == Nand(p,Neg(q))"
1.30
1.31 -definition Iff :: "[i,i]=>i"
1.32 -    "Iff(p,q) == And(Implies(p,q), Implies(q,p))"
1.33 +definition
1.34 +  Iff :: "[i,i]=>i" where
1.35 +  "Iff(p,q) == And(Implies(p,q), Implies(q,p))"
1.36
1.37 -definition Exists :: "i=>i"
1.38 -    "Exists(p) == Neg(Forall(Neg(p)))";
1.39 +definition
1.40 +  Exists :: "i=>i" where
1.41 +  "Exists(p) == Neg(Forall(Neg(p)))";
1.42
1.43  lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula"
1.45 @@ -79,7 +85,7 @@
1.46  by (induct set: formula) simp_all
1.47
1.48  abbreviation
1.49 -  sats :: "[i,i,i] => o"
1.50 +  sats :: "[i,i,i] => o" where
1.51    "sats(A,p,env) == satisfies(A,p)`env = 1"
1.52
1.53  lemma [simp]:
1.54 @@ -246,8 +252,9 @@
1.55
1.56  subsection{*Renaming Some de Bruijn Variables*}
1.57
1.58 -definition incr_var :: "[i,i]=>i"
1.59 -    "incr_var(x,nq) == if x<nq then x else succ(x)"
1.60 +definition
1.61 +  incr_var :: "[i,i]=>i" where
1.62 +  "incr_var(x,nq) == if x<nq then x else succ(x)"
1.63
1.64  lemma incr_var_lt: "x<nq ==> incr_var(x,nq) = x"
1.66 @@ -334,8 +341,9 @@
1.67
1.68  subsection{*Renaming all but the First de Bruijn Variable*}
1.69
1.70 -definition incr_bv1 :: "i => i"
1.71 -    "incr_bv1(p) == incr_bv(p)`1"
1.72 +definition
1.73 +  incr_bv1 :: "i => i" where
1.74 +  "incr_bv1(p) == incr_bv(p)`1"
1.75
1.76
1.77  lemma incr_bv1_type [TC]: "p \<in> formula ==> incr_bv1(p) \<in> formula"
1.78 @@ -385,7 +393,8 @@
1.79  subsection{*Definable Powerset*}
1.80
1.81  text{*The definable powerset operation: Kunen's definition VI 1.1, page 165.*}
1.82 -definition DPow :: "i => i"
1.83 +definition
1.84 +  DPow :: "i => i" where
1.85    "DPow(A) == {X \<in> Pow(A).
1.86                 \<exists>env \<in> list(A). \<exists>p \<in> formula.
1.87                   arity(p) \<le> succ(length(env)) &
1.88 @@ -507,8 +516,9 @@
1.89
1.90  subsubsection{*The subset relation*}
1.91
1.92 -definition subset_fm :: "[i,i]=>i"
1.93 -    "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
1.94 +definition
1.95 +  subset_fm :: "[i,i]=>i" where
1.96 +  "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
1.97
1.98  lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
1.100 @@ -527,8 +537,9 @@
1.101
1.102  subsubsection{*Transitive sets*}
1.103
1.104 -definition transset_fm :: "i=>i"
1.105 -   "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
1.106 +definition
1.107 +  transset_fm :: "i=>i" where
1.108 +  "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
1.109
1.110  lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
1.112 @@ -547,9 +558,10 @@
1.113
1.114  subsubsection{*Ordinals*}
1.115
1.116 -definition ordinal_fm :: "i=>i"
1.117 -   "ordinal_fm(x) ==
1.118 -      And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
1.119 +definition
1.120 +  ordinal_fm :: "i=>i" where
1.121 +  "ordinal_fm(x) ==
1.122 +    And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
1.123
1.124  lemma ordinal_type [TC]: "x \<in> nat ==> ordinal_fm(x) \<in> formula"
1.126 @@ -579,11 +591,12 @@
1.127  subsection{* Constant Lset: Levels of the Constructible Universe *}
1.128
1.129  definition
1.130 -  Lset :: "i=>i"
1.131 -    "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
1.132 +  Lset :: "i=>i" where
1.133 +  "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
1.134
1.135 -  L :: "i=>o" --{*Kunen's definition VI 1.5, page 167*}
1.136 -    "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
1.137 +definition
1.138 +  L :: "i=>o" where --{*Kunen's definition VI 1.5, page 167*}
1.139 +  "L(x) == \<exists>i. Ord(i) & x \<in> Lset(i)"
1.140
1.141  text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
1.142  lemma Lset: "Lset(i) = (UN j:i. DPow(Lset(j)))"
1.143 @@ -825,8 +838,8 @@
1.144
1.145  text{*The rank function for the constructible universe*}
1.146  definition
1.147 -  lrank :: "i=>i" --{*Kunen's definition VI 1.7*}
1.148 -    "lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
1.149 +  lrank :: "i=>i" where --{*Kunen's definition VI 1.7*}
1.150 +  "lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
1.151
1.152  lemma L_I: "[|x \<in> Lset(i); Ord(i)|] ==> L(x)"
1.153  by (simp add: L_def, blast)
1.154 @@ -984,7 +997,8 @@
1.155
1.156
1.157  text{*A simpler version of @{term DPow}: no arity check!*}
1.158 -definition DPow' :: "i => i"
1.159 +definition
1.160 +  DPow' :: "i => i" where
1.161    "DPow'(A) == {X \<in> Pow(A).
1.162                  \<exists>env \<in> list(A). \<exists>p \<in> formula.
1.163                      X = {x\<in>A. sats(A, p, Cons(x,env))}}"
```