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.44  by (simp add: Neg_def) 
    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.65  by (simp add: incr_var_def)
    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.99  by (simp add: subset_fm_def) 
   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.111  by (simp add: transset_fm_def) 
   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.125  by (simp add: ordinal_fm_def) 
   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))}}"