author paulson Tue, 09 Jul 2002 17:25:42 +0200 changeset 13324 39d1b3a4c6f4 parent 13323 2c287f50c9f3 child 13325 5b5e12f0aee0
more and simpler separation proofs
```--- a/src/ZF/Constructible/Separation.thy	Tue Jul 09 15:39:44 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy	Tue Jul 09 17:25:42 2002 +0200
@@ -2,7 +2,7 @@

(*This theory proves all instances needed for locale M_axioms*)

-theory Separation = L_axioms + WFrec:
+theory Separation = L_axioms + WF_absolute:

text{*Helps us solve for de Bruijn indices!*}
lemma nth_ConsI: "[|nth(n,l) = x; n \<in> nat|] ==> nth(succ(n), Cons(a,l)) = x"
@@ -633,56 +633,80 @@

subsection{*Separation for Reflexive/Transitive Closure*}

-lemma rtrancl_reflects:
-  "REFLECTS[\<lambda>p.
-    \<exists>nnat[L]. \<exists>n[L]. \<exists>n'[L]. omega(L,nnat) & n\<in>nnat & successor(L,n,n') &
-     (\<exists>f[L].
-      typed_function(L,n',A,f) &
-      (\<exists>x[L]. \<exists>y[L]. \<exists>zero[L]. pair(L,x,y,p) & empty(L,zero) &
-	fun_apply(L,f,zero,x) & fun_apply(L,f,n,y)) &
-	(\<forall>j[L]. j\<in>n -->
-	  (\<exists>fj[L]. \<exists>sj[L]. \<exists>fsj[L]. \<exists>ffp[L].
-	    fun_apply(L,f,j,fj) & successor(L,j,sj) &
-	    fun_apply(L,f,sj,fsj) & pair(L,fj,fsj,ffp) & ffp \<in> r))),
-\<lambda>i p.
-    \<exists>nnat \<in> Lset(i). \<exists>n \<in> Lset(i). \<exists>n' \<in> Lset(i).
-     omega(**Lset(i),nnat) & n\<in>nnat & successor(**Lset(i),n,n') &
-     (\<exists>f \<in> Lset(i).
-      typed_function(**Lset(i),n',A,f) &
-      (\<exists>x \<in> Lset(i). \<exists>y \<in> Lset(i). \<exists>zero \<in> Lset(i). pair(**Lset(i),x,y,p) & empty(**Lset(i),zero) &
-	fun_apply(**Lset(i),f,zero,x) & fun_apply(**Lset(i),f,n,y)) &
-	(\<forall>j \<in> Lset(i). j\<in>n -->
-	  (\<exists>fj \<in> Lset(i). \<exists>sj \<in> Lset(i). \<exists>fsj \<in> Lset(i). \<exists>ffp \<in> Lset(i).
-	    fun_apply(**Lset(i),f,j,fj) & successor(**Lset(i),j,sj) &
-	    fun_apply(**Lset(i),f,sj,fsj) & pair(**Lset(i),fj,fsj,ffp) & ffp \<in> r)))]"
-by (intro FOL_reflections function_reflections fun_plus_reflections)
+subsubsection{*First, The Defining Formula*}
+
+(* "rtran_closure_mem(M,A,r,p) ==
+      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
+       omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
+       (\<exists>f[M]. typed_function(M,n',A,f) &
+	(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
+	  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
+	(\<forall>j[M]. j\<in>n -->
+	  (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
+	    fun_apply(M,f,j,fj) & successor(M,j,sj) &
+	    fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"*)
+constdefs rtran_closure_mem_fm :: "[i,i,i]=>i"
+ "rtran_closure_mem_fm(A,r,p) ==
+   Exists(Exists(Exists(
+    And(omega_fm(2),
+     And(Member(1,2),
+      And(succ_fm(1,0),
+       Exists(And(typed_function_fm(1, A#+4, 0),
+	And(Exists(Exists(Exists(
+	      And(pair_fm(2,1,p#+7),
+	       And(empty_fm(0),
+		And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))),
+	    Forall(Implies(Member(0,3),
+	     Exists(Exists(Exists(Exists(
+	      And(fun_apply_fm(5,4,3),
+	       And(succ_fm(4,2),
+		And(fun_apply_fm(5,2,1),
+		 And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))"
+
+
+lemma rtran_closure_mem_type [TC]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula"
+
+lemma arity_rtran_closure_mem_fm [simp]:
+     "[| x \<in> nat; y \<in> nat; z \<in> nat |]
+      ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"
+by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac)
+
+lemma sats_rtran_closure_mem_fm [simp]:
+   "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|]
+    ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <->
+        rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))"
+
+lemma rtran_closure_mem_iff_sats:
+      "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
+          i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)|]
+       ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)"
+
+theorem rtran_closure_mem_reflection:
+     "REFLECTS[\<lambda>x. rtran_closure_mem(L,f(x),g(x),h(x)),
+               \<lambda>i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]"
+apply (simp only: rtran_closure_mem_def setclass_simps)
+apply (intro FOL_reflections function_reflections fun_plus_reflections)
+done
+
+subsubsection{*Then, the Instance of Separation*}

text{*This formula describes @{term "rtrancl(r)"}.*}
lemma rtrancl_separation:
-     "[| L(r); L(A) |] ==>
-      separation (L, \<lambda>p.
-	  \<exists>nnat[L]. \<exists>n[L]. \<exists>n'[L].
-           omega(L,nnat) & n\<in>nnat & successor(L,n,n') &
-	   (\<exists>f[L].
-	    typed_function(L,n',A,f) &
-	    (\<exists>x[L]. \<exists>y[L]. \<exists>zero[L]. pair(L,x,y,p) & empty(L,zero) &
-	      fun_apply(L,f,zero,x) & fun_apply(L,f,n,y)) &
-	      (\<forall>j[L]. j\<in>n -->
-		(\<exists>fj[L]. \<exists>sj[L]. \<exists>fsj[L]. \<exists>ffp[L].
-		  fun_apply(L,f,j,fj) & successor(L,j,sj) &
-		  fun_apply(L,f,sj,fsj) & pair(L,fj,fsj,ffp) & ffp \<in> r))))"
+     "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
apply (rule separation_CollectI)
apply (rule_tac A="{r,A,z}" in subset_LsetE, blast )
-apply (rule ReflectsE [OF rtrancl_reflects], assumption)
+apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption)
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
apply (rule DPowI2)
-apply (rename_tac u)
-apply (rule bex_iff_sats conj_iff_sats)+
-apply (rule_tac env = "[x,u,r,A]" in omega_iff_sats)
-txt{*SLOW, maybe just due to the formula's size*}
+apply (rename_tac u)
+apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats)
apply (rule sep_rules | simp)+
done```
```--- a/src/ZF/Constructible/WF_absolute.thy	Tue Jul 09 15:39:44 2002 +0200
+++ b/src/ZF/Constructible/WF_absolute.thy	Tue Jul 09 17:25:42 2002 +0200
@@ -111,41 +111,43 @@

constdefs

+  rtran_closure_mem :: "[i=>o,i,i,i] => o"
+    --{*The property of belonging to @{text "rtran_closure(r)"}*}
+    "rtran_closure_mem(M,A,r,p) ==
+	      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
+               omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
+	       (\<exists>f[M]. typed_function(M,n',A,f) &
+		(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
+		  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
+		  (\<forall>j[M]. j\<in>n -->
+		    (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
+		      fun_apply(M,f,j,fj) & successor(M,j,sj) &
+		      fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r)))"
+
rtran_closure :: "[i=>o,i,i] => o"
-    "rtran_closure(M,r,s) ==
-        \<forall>A. M(A) --> is_field(M,r,A) -->
- 	 (\<forall>p. M(p) -->
-          (p \<in> s <->
-           (\<exists>n\<in>nat. M(n) &
-            (\<exists>n'. M(n') & successor(M,n,n') &
-             (\<exists>f. M(f) & typed_function(M,n',A,f) &
-              (\<exists>x\<in>A. M(x) & (\<exists>y\<in>A. M(y) & pair(M,x,y,p) &
-                   fun_apply(M,f,0,x) & fun_apply(M,f,n,y))) &
-              (\<forall>i\<in>n. M(i) -->
-                (\<forall>i'. M(i') --> successor(M,i,i') -->
-                 (\<forall>fi. M(fi) --> fun_apply(M,f,i,fi) -->
-                  (\<forall>fi'. M(fi') --> fun_apply(M,f,i',fi') -->
-                   (\<forall>q. M(q) --> pair(M,fi,fi',q) --> q \<in> r))))))))))"
+    "rtran_closure(M,r,s) ==
+        \<forall>A[M]. is_field(M,r,A) -->
+ 	 (\<forall>p[M]. p \<in> s <-> rtran_closure_mem(M,A,r,p))"

tran_closure :: "[i=>o,i,i] => o"
"tran_closure(M,r,t) ==
\<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)"

+lemma (in M_axioms) rtran_closure_mem_iff:
+     "[|M(A); M(r); M(p)|]
+      ==> rtran_closure_mem(M,A,r,p) <->
+          (\<exists>n[M]. n\<in>nat &
+           (\<exists>f[M]. f \<in> succ(n) -> A &
+            (\<exists>x[M]. \<exists>y[M]. p = <x,y> & f`0 = x & f`n = y) &
+                           (\<forall>i\<in>n. <f`i, f`succ(i)> \<in> r)))"
+                 Ord_succ_mem_iff nat_0_le [THEN ltD])
+apply (blast intro: elim:);
+done

locale M_trancl = M_axioms +
assumes rtrancl_separation:
-	 "[| M(r); M(A) |] ==>
-	  separation (M, \<lambda>p.
-	      \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
-               omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
-	       (\<exists>f[M].
-		typed_function(M,n',A,f) &
-		(\<exists>x[M]. \<exists>y[M]. \<exists>zero[M]. pair(M,x,y,p) & empty(M,zero) &
-		  fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) &
-		  (\<forall>j[M]. j\<in>n -->
-		    (\<exists>fj[M]. \<exists>sj[M]. \<exists>fsj[M]. \<exists>ffp[M].
-		      fun_apply(M,f,j,fj) & successor(M,j,sj) &
-		      fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \<in> r))))"
+	 "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))"
and wellfounded_trancl_separation:
"[| M(r); M(Z) |] ==>
separation (M, \<lambda>x.
@@ -155,29 +157,16 @@

lemma (in M_trancl) rtran_closure_rtrancl:
"M(r) ==> rtran_closure(M,r,rtrancl(r))"
-apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
-                 rtrancl_alt_def field_closed typed_apply_abs apply_closed
-                 Ord_succ_mem_iff M_nat  nat_0_le [THEN ltD], clarify)
-apply (rule iffI)
- apply clarify
- apply simp
- apply (rename_tac n f)
- apply (rule_tac x=n in bexI)
-  apply (rule_tac x=f in exI)
-  apply simp
-  apply (blast dest: finite_fun_closed dest: transM)
- apply assumption
-apply clarify
-apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast)
+                 rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def)
+apply (auto simp add: nat_0_le [THEN ltD] apply_funtype);
done

lemma (in M_trancl) rtrancl_closed [intro,simp]:
"M(r) ==> M(rtrancl(r))"
apply (insert rtrancl_separation [of r "field(r)"])
-                 rtrancl_alt_def field_closed typed_apply_abs apply_closed
-                 Ord_succ_mem_iff M_nat nat_into_M
-                 nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
+                 rtrancl_alt_def rtran_closure_mem_iff)
done

lemma (in M_trancl) rtrancl_abs [simp]:
@@ -187,20 +176,10 @@
prefer 2 apply (blast intro: rtran_closure_rtrancl)
apply (rule M_equalityI)
apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric]
-                 rtrancl_alt_def field_closed typed_apply_abs apply_closed
-                 Ord_succ_mem_iff M_nat
-                 nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype)
- prefer 2 apply assumption
- prefer 2 apply blast
-apply (rule iffI, clarify)
-apply (simp add: nat_0_le [THEN ltD]  apply_funtype, blast, clarify, simp)
- apply (rename_tac n f)
- apply (rule_tac x=n in bexI)
-  apply (rule_tac x=f in exI)
-  apply (blast dest!: finite_fun_closed, assumption)
+                 rtrancl_alt_def rtran_closure_mem_iff)
+apply (auto simp add: nat_0_le [THEN ltD] apply_funtype);
done

-
lemma (in M_trancl) trancl_closed [intro,simp]:
"M(r) ==> M(trancl(r))"
by (simp add: trancl_def comp_closed rtrancl_closed)```