src/ZF/Constructible/Internalize.thy

 (*  Title:      ZF/Constructible/Internalize.thy
-    ID: $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
 theory Internalize imports L_axioms Datatype_absolute begin
 

 done
 
 subsubsection{*The Operator @{term is_Member}, Internalized*}
 
 (*    "is_Member(M,x,y,Z) ==
-	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" *)
+        \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inl(M,u,Z)" *)
 definition
   Member_fm :: "[i,i,i]=>i" where
     "Member_fm(x,y,Z) ==
        Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
                       And(Inl_fm(1,0), Inl_fm(0,Z#+2)))))"

 done
 
 subsubsection{*The Operator @{term is_Equal}, Internalized*}
 
 (*    "is_Equal(M,x,y,Z) ==
-	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" *)
+        \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inr(M,p,u) & is_Inl(M,u,Z)" *)
 definition
   Equal_fm :: "[i,i,i]=>i" where
     "Equal_fm(x,y,Z) ==
        Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
                       And(Inr_fm(1,0), Inl_fm(0,Z#+2)))))"

 done
 
 subsubsection{*The Operator @{term is_Nand}, Internalized*}
 
 (*    "is_Nand(M,x,y,Z) ==
-	\<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" *)
+        \<exists>p[M]. \<exists>u[M]. pair(M,x,y,p) & is_Inl(M,p,u) & is_Inr(M,u,Z)" *)
 definition
   Nand_fm :: "[i,i,i]=>i" where
     "Nand_fm(x,y,Z) ==
        Exists(Exists(And(pair_fm(x#+2,y#+2,1), 
                       And(Inl_fm(1,0), Inr_fm(0,Z#+2)))))"

    Forall(Iff(Member(0,succ(f)),
     Exists(Exists(Exists(
      And(p, 
       And(pair_fm(2,0,3),
        Exists(Exists(Exists(
-	And(pair_fm(5,a#+7,2),
-	 And(upair_fm(5,5,1),
-	  And(pre_image_fm(r#+7,1,0),
-	   And(restriction_fm(f#+7,0,4), Member(2,r#+7)))))))))))))))"
+        And(pair_fm(5,a#+7,2),
+         And(upair_fm(5,5,1),
+          And(pre_image_fm(r#+7,1,0),
+           And(restriction_fm(f#+7,0,4), Member(2,r#+7)))))))))))))))"
 
 lemma is_recfun_type [TC]:
      "[| p \<in> formula; x \<in> nat; y \<in> nat; z \<in> nat |] 
       ==> is_recfun_fm(p,x,y,z) \<in> formula"
 by (simp add: is_recfun_fm_def)