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))}}"