src/ZF/Constructible/Formula.thy
changeset 13398 1cadd412da48
parent 13385 31df66ca0780
child 13505 52a16cb7fefb
     1.1 --- a/src/ZF/Constructible/Formula.thy	Fri Jul 19 13:29:22 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Formula.thy	Fri Jul 19 18:06:31 2002 +0200
     1.3 @@ -11,17 +11,22 @@
     1.4  datatype
     1.5    "formula" = Member ("x: nat", "y: nat")
     1.6              | Equal  ("x: nat", "y: nat")
     1.7 -            | Neg ("p: formula")
     1.8 -            | And ("p: formula", "q: formula")
     1.9 +            | Nand ("p: formula", "q: formula")
    1.10              | Forall ("p: formula")
    1.11  
    1.12  declare formula.intros [TC]
    1.13  
    1.14 +constdefs Neg :: "i=>i"
    1.15 +    "Neg(p) == Nand(p,p)"
    1.16 +
    1.17 +constdefs And :: "[i,i]=>i"
    1.18 +    "And(p,q) == Neg(Nand(p,q))"
    1.19 +
    1.20  constdefs Or :: "[i,i]=>i"
    1.21 -    "Or(p,q) == Neg(And(Neg(p),Neg(q)))"
    1.22 +    "Or(p,q) == Nand(Neg(p),Neg(q))"
    1.23  
    1.24  constdefs Implies :: "[i,i]=>i"
    1.25 -    "Implies(p,q) == Neg(And(p,Neg(q)))"
    1.26 +    "Implies(p,q) == Nand(p,Neg(q))"
    1.27  
    1.28  constdefs Iff :: "[i,i]=>i"
    1.29      "Iff(p,q) == And(Implies(p,q), Implies(q,p))"
    1.30 @@ -29,6 +34,12 @@
    1.31  constdefs Exists :: "i=>i"
    1.32      "Exists(p) == Neg(Forall(Neg(p)))";
    1.33  
    1.34 +lemma Neg_type [TC]: "p \<in> formula ==> Neg(p) \<in> formula"
    1.35 +by (simp add: Neg_def) 
    1.36 +
    1.37 +lemma And_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> And(p,q) \<in> formula"
    1.38 +by (simp add: And_def) 
    1.39 +
    1.40  lemma Or_type [TC]: "[| p \<in> formula; q \<in> formula |] ==> Or(p,q) \<in> formula"
    1.41  by (simp add: Or_def) 
    1.42  
    1.43 @@ -52,11 +63,8 @@
    1.44    "satisfies(A,Equal(x,y)) = 
    1.45        (\<lambda>env \<in> list(A). bool_of_o (nth(x,env) = nth(y,env)))"
    1.46  
    1.47 -  "satisfies(A,Neg(p)) = 
    1.48 -      (\<lambda>env \<in> list(A). not(satisfies(A,p)`env))"
    1.49 -
    1.50 -  "satisfies(A,And(p,q)) =
    1.51 -      (\<lambda>env \<in> list(A). (satisfies(A,p)`env) and (satisfies(A,q)`env))"
    1.52 +  "satisfies(A,Nand(p,q)) =
    1.53 +      (\<lambda>env \<in> list(A). not ((satisfies(A,p)`env) and (satisfies(A,q)`env)))"
    1.54  
    1.55    "satisfies(A,Forall(p)) = 
    1.56        (\<lambda>env \<in> list(A). bool_of_o (\<forall>x\<in>A. satisfies(A,p) ` (Cons(x,env)) = 1))"
    1.57 @@ -78,15 +86,10 @@
    1.58     ==> sats(A, Equal(x,y), env) <-> nth(x,env) = nth(y,env)"
    1.59  by simp
    1.60  
    1.61 -lemma sats_Neg_iff [simp]:
    1.62 +lemma sats_Nand_iff [simp]:
    1.63    "env \<in> list(A) 
    1.64 -   ==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)"
    1.65 -by (simp add: Bool.not_def cond_def) 
    1.66 -
    1.67 -lemma sats_And_iff [simp]:
    1.68 -  "env \<in> list(A) 
    1.69 -   ==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)"
    1.70 -by (simp add: Bool.and_def cond_def) 
    1.71 +   ==> (sats(A, Nand(p,q), env)) <-> ~ (sats(A,p,env) & sats(A,q,env))" 
    1.72 +by (simp add: Bool.and_def Bool.not_def cond_def) 
    1.73  
    1.74  lemma sats_Forall_iff [simp]:
    1.75    "env \<in> list(A) 
    1.76 @@ -97,6 +100,16 @@
    1.77  
    1.78  subsection{*Dividing line between primitive and derived connectives*}
    1.79  
    1.80 +lemma sats_Neg_iff [simp]:
    1.81 +  "env \<in> list(A) 
    1.82 +   ==> sats(A, Neg(p), env) <-> ~ sats(A,p,env)"
    1.83 +by (simp add: Neg_def) 
    1.84 +
    1.85 +lemma sats_And_iff [simp]:
    1.86 +  "env \<in> list(A) 
    1.87 +   ==> (sats(A, And(p,q), env)) <-> sats(A,p,env) & sats(A,q,env)"
    1.88 +by (simp add: And_def) 
    1.89 +
    1.90  lemma sats_Or_iff [simp]:
    1.91    "env \<in> list(A) 
    1.92     ==> (sats(A, Or(p,q), env)) <-> sats(A,p,env) | sats(A,q,env)"
    1.93 @@ -194,11 +207,8 @@
    1.94    "incr_bv(Equal(x,y)) = 
    1.95        (\<lambda>lev \<in> nat. Equal (incr_var(x,lev), incr_var(y,lev)))"
    1.96  
    1.97 -  "incr_bv(Neg(p)) = 
    1.98 -      (\<lambda>lev \<in> nat. Neg(incr_bv(p)`lev))"
    1.99 -
   1.100 -  "incr_bv(And(p,q)) =
   1.101 -      (\<lambda>lev \<in> nat. And (incr_bv(p)`lev, incr_bv(q)`lev))"
   1.102 +  "incr_bv(Nand(p,q)) =
   1.103 +      (\<lambda>lev \<in> nat. Nand (incr_bv(p)`lev, incr_bv(q)`lev))"
   1.104  
   1.105    "incr_bv(Forall(p)) = 
   1.106        (\<lambda>lev \<in> nat. Forall (incr_bv(p) ` succ(lev)))"
   1.107 @@ -257,9 +267,7 @@
   1.108  
   1.109    "arity(Equal(x,y)) = succ(x) \<union> succ(y)"
   1.110  
   1.111 -  "arity(Neg(p)) = arity(p)"
   1.112 -
   1.113 -  "arity(And(p,q)) = arity(p) \<union> arity(q)"
   1.114 +  "arity(Nand(p,q)) = arity(p) \<union> arity(q)"
   1.115  
   1.116    "arity(Forall(p)) = nat_case(0, %x. x, arity(p))"
   1.117  
   1.118 @@ -267,6 +275,12 @@
   1.119  lemma arity_type [TC]: "p \<in> formula ==> arity(p) \<in> nat"
   1.120  by (induct_tac p, simp_all) 
   1.121  
   1.122 +lemma arity_Neg [simp]: "arity(Neg(p)) = arity(p)"
   1.123 +by (simp add: Neg_def) 
   1.124 +
   1.125 +lemma arity_And [simp]: "arity(And(p,q)) = arity(p) \<union> arity(q)"
   1.126 +by (simp add: And_def) 
   1.127 +
   1.128  lemma arity_Or [simp]: "arity(Or(p,q)) = arity(p) \<union> arity(q)"
   1.129  by (simp add: Or_def) 
   1.130