src/ZF/Constructible/Formula.thy
 changeset 21233 5a5c8ea5f66a parent 16417 9bc16273c2d4 child 21404 eb85850d3eb7
```     1.1 --- a/src/ZF/Constructible/Formula.thy	Tue Nov 07 19:39:54 2006 +0100
1.2 +++ b/src/ZF/Constructible/Formula.thy	Tue Nov 07 19:40:13 2006 +0100
1.3 @@ -21,22 +21,22 @@
1.4
1.5  declare formula.intros [TC]
1.6
1.7 -constdefs Neg :: "i=>i"
1.8 +definition Neg :: "i=>i"
1.9      "Neg(p) == Nand(p,p)"
1.10
1.11 -constdefs And :: "[i,i]=>i"
1.12 +definition And :: "[i,i]=>i"
1.13      "And(p,q) == Neg(Nand(p,q))"
1.14
1.15 -constdefs Or :: "[i,i]=>i"
1.16 +definition Or :: "[i,i]=>i"
1.17      "Or(p,q) == Nand(Neg(p),Neg(q))"
1.18
1.19 -constdefs Implies :: "[i,i]=>i"
1.20 +definition Implies :: "[i,i]=>i"
1.21      "Implies(p,q) == Nand(p,Neg(q))"
1.22
1.23 -constdefs Iff :: "[i,i]=>i"
1.24 +definition Iff :: "[i,i]=>i"
1.25      "Iff(p,q) == And(Implies(p,q), Implies(q,p))"
1.26
1.27 -constdefs Exists :: "i=>i"
1.28 +definition Exists :: "i=>i"
1.29      "Exists(p) == Neg(Forall(Neg(p)))";
1.30
1.31  lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula"
1.32 @@ -76,10 +76,11 @@
1.33
1.34
1.35  lemma "p \<in> formula ==> satisfies(A,p) \<in> list(A) -> bool"
1.36 -by (induct_tac p, simp_all)
1.37 +by (induct set: formula) simp_all
1.38
1.39 -syntax sats :: "[i,i,i] => o"
1.40 -translations "sats(A,p,env)" == "satisfies(A,p)`env = 1"
1.41 +abbreviation
1.42 +  sats :: "[i,i,i] => o"
1.43 +  "sats(A,p,env) == satisfies(A,p)`env = 1"
1.44
1.45  lemma [simp]:
1.46    "env \<in> list(A)
1.47 @@ -245,7 +246,7 @@
1.48
1.49  subsection{*Renaming Some de Bruijn Variables*}
1.50
1.51 -constdefs incr_var :: "[i,i]=>i"
1.52 +definition incr_var :: "[i,i]=>i"
1.53      "incr_var(x,nq) == if x<nq then x else succ(x)"
1.54
1.55  lemma incr_var_lt: "x<nq ==> incr_var(x,nq) = x"
1.56 @@ -333,7 +334,7 @@
1.57
1.58  subsection{*Renaming all but the First de Bruijn Variable*}
1.59
1.60 -constdefs incr_bv1 :: "i => i"
1.61 +definition incr_bv1 :: "i => i"
1.62      "incr_bv1(p) == incr_bv(p)`1"
1.63
1.64
1.65 @@ -384,7 +385,7 @@
1.66  subsection{*Definable Powerset*}
1.67
1.68  text{*The definable powerset operation: Kunen's definition VI 1.1, page 165.*}
1.69 -constdefs DPow :: "i => i"
1.70 +definition DPow :: "i => i"
1.71    "DPow(A) == {X \<in> Pow(A).
1.72                 \<exists>env \<in> list(A). \<exists>p \<in> formula.
1.73                   arity(p) \<le> succ(length(env)) &
1.74 @@ -506,7 +507,7 @@
1.75
1.76  subsubsection{*The subset relation*}
1.77
1.78 -constdefs subset_fm :: "[i,i]=>i"
1.79 +definition subset_fm :: "[i,i]=>i"
1.80      "subset_fm(x,y) == Forall(Implies(Member(0,succ(x)), Member(0,succ(y))))"
1.81
1.82  lemma subset_type [TC]: "[| x \<in> nat; y \<in> nat |] ==> subset_fm(x,y) \<in> formula"
1.83 @@ -526,7 +527,7 @@
1.84
1.85  subsubsection{*Transitive sets*}
1.86
1.87 -constdefs transset_fm :: "i=>i"
1.88 +definition transset_fm :: "i=>i"
1.89     "transset_fm(x) == Forall(Implies(Member(0,succ(x)), subset_fm(0,succ(x))))"
1.90
1.91  lemma transset_type [TC]: "x \<in> nat ==> transset_fm(x) \<in> formula"
1.92 @@ -546,7 +547,7 @@
1.93
1.94  subsubsection{*Ordinals*}
1.95
1.96 -constdefs ordinal_fm :: "i=>i"
1.97 +definition ordinal_fm :: "i=>i"
1.98     "ordinal_fm(x) ==
1.99        And(transset_fm(x), Forall(Implies(Member(0,succ(x)), transset_fm(0))))"
1.100
1.101 @@ -577,7 +578,7 @@
1.102
1.103  subsection{* Constant Lset: Levels of the Constructible Universe *}
1.104
1.105 -constdefs
1.106 +definition
1.107    Lset :: "i=>i"
1.108      "Lset(i) == transrec(i, %x f. \<Union>y\<in>x. DPow(f`y))"
1.109
1.110 @@ -823,7 +824,7 @@
1.111
1.112
1.113  text{*The rank function for the constructible universe*}
1.114 -constdefs
1.115 +definition
1.116    lrank :: "i=>i" --{*Kunen's definition VI 1.7*}
1.117      "lrank(x) == \<mu> i. x \<in> Lset(succ(i))"
1.118
1.119 @@ -983,7 +984,7 @@
1.120
1.121
1.122  text{*A simpler version of @{term DPow}: no arity check!*}
1.123 -constdefs DPow' :: "i => i"
1.124 +definition DPow' :: "i => i"
1.125    "DPow'(A) == {X \<in> Pow(A).
1.126                  \<exists>env \<in> list(A). \<exists>p \<in> formula.
1.127                      X = {x\<in>A. sats(A, p, Cons(x,env))}}"
```