Expressing Lset and L without using length and arity; simplifies Separation
proofs

--- a/src/ZF/Constructible/Datatype_absolute.thy	Tue Jul 16 20:25:21 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Wed Jul 17 15:48:54 2002 +0200
@@ -6,21 +6,43 @@
 subsection{*The lfp of a continuous function can be expressed as a union*}
 
 constdefs
-  contin :: "[i=>i]=>o"
-   "contin(h) == (\<forall>A. A\<noteq>0 --> h(\<Union>A) = (\<Union>X\<in>A. h(X)))"
+  directed :: "i=>o"
+   "directed(A) == A\<noteq>0 & (\<forall>x\<in>A. \<forall>y\<in>A. x \<union> y \<in> A)"
+
+  contin :: "(i=>i) => o"
+   "contin(h) == (\<forall>A. directed(A) --> h(\<Union>A) = (\<Union>X\<in>A. h(X)))"
 
 lemma bnd_mono_iterates_subset: "[|bnd_mono(D, h); n \<in> nat|] ==> h^n (0) <= D"
 apply (induct_tac n) 
  apply (simp_all add: bnd_mono_def, blast) 
 done
 
+lemma bnd_mono_increasing [rule_format]:
+     "[|i \<in> nat; j \<in> nat; bnd_mono(D,h)|] ==> i \<le> j --> h^i(0) \<subseteq> h^j(0)"
+apply (rule_tac m=i and n=j in diff_induct, simp_all)
+apply (blast del: subsetI
+	     intro: bnd_mono_iterates_subset bnd_monoD2 [of concl: h] ) 
+done
+
+lemma directed_iterates: "bnd_mono(D,h) ==> directed({h^n (0). n\<in>nat})"
+apply (simp add: directed_def, clarify) 
+apply (rename_tac i j)
+apply (rule_tac x="i \<union> j" in bexI) 
+apply (rule_tac i = i and j = j in Ord_linear_le)
+apply (simp_all add: subset_Un_iff [THEN iffD1] le_imp_subset
+                     subset_Un_iff2 [THEN iffD1])
+apply (simp_all add: subset_Un_iff [THEN iff_sym] bnd_mono_increasing
+                     subset_Un_iff2 [THEN iff_sym])
+done
+
 
 lemma contin_iterates_eq: 
-    "contin(h) \<Longrightarrow> h(\<Union>n\<in>nat. h^n (0)) = (\<Union>n\<in>nat. h^n (0))"
-apply (simp add: contin_def) 
+    "[|bnd_mono(D, h); contin(h)|] 
+     ==> h(\<Union>n\<in>nat. h^n (0)) = (\<Union>n\<in>nat. h^n (0))"
+apply (simp add: contin_def directed_iterates) 
 apply (rule trans) 
 apply (rule equalityI) 
- apply (simp_all add: UN_subset_iff) 
+ apply (simp_all add: UN_subset_iff)
  apply safe
  apply (erule_tac [2] natE) 
   apply (rule_tac a="succ(x)" in UN_I) 
@@ -51,20 +73,53 @@
           intro: lfp_subset_Union Union_subset_lfp)
 
 
+subsubsection{*Some Standard Datatype Constructions Preserve Continuity*}
+
+lemma contin_imp_mono: "[|X\<subseteq>Y; contin(F)|] ==> F(X) \<subseteq> F(Y)"
+apply (simp add: contin_def) 
+apply (drule_tac x="{X,Y}" in spec) 
+apply (simp add: directed_def subset_Un_iff2 Un_commute) 
+done
+
+lemma sum_contin: "[|contin(F); contin(G)|] ==> contin(\<lambda>X. F(X) + G(X))"
+by (simp add: contin_def, blast)
+
+lemma prod_contin: "[|contin(F); contin(G)|] ==> contin(\<lambda>X. F(X) * G(X))" 
+apply (subgoal_tac "\<forall>B C. F(B) \<subseteq> F(B \<union> C)")
+ prefer 2 apply (simp add: Un_upper1 contin_imp_mono) 
+apply (subgoal_tac "\<forall>B C. G(C) \<subseteq> G(B \<union> C)")
+ prefer 2 apply (simp add: Un_upper2 contin_imp_mono) 
+apply (simp add: contin_def, clarify) 
+apply (rule equalityI) 
+ prefer 2 apply blast 
+apply clarify 
+apply (rename_tac B C) 
+apply (rule_tac a="B \<union> C" in UN_I) 
+ apply (simp add: directed_def, blast)  
+done
+
+lemma const_contin: "contin(\<lambda>X. A)"
+by (simp add: contin_def directed_def)
+
+lemma id_contin: "contin(\<lambda>X. X)"
+by (simp add: contin_def)
+
+
+
 subsection {*lists without univ*}
 
-lemmas datatype_univs = A_into_univ Inl_in_univ Inr_in_univ 
-                        Pair_in_univ zero_in_univ
+lemmas datatype_univs = Inl_in_univ Inr_in_univ 
+                        Pair_in_univ nat_into_univ A_into_univ 
 
 lemma list_fun_bnd_mono: "bnd_mono(univ(A), \<lambda>X. {0} + A*X)"
 apply (rule bnd_monoI)
  apply (intro subset_refl zero_subset_univ A_subset_univ 
 	      sum_subset_univ Sigma_subset_univ) 
- apply (blast intro!: subset_refl sum_mono Sigma_mono del: subsetI)
+apply (rule subset_refl sum_mono Sigma_mono | assumption)+
 done
 
 lemma list_fun_contin: "contin(\<lambda>X. {0} + A*X)"
-by (simp add: contin_def, blast)
+by (intro sum_contin prod_contin id_contin const_contin) 
 
 text{*Re-expresses lists using sum and product*}
 lemma list_eq_lfp2: "list(A) = lfp(univ(A), \<lambda>X. {0} + A*X)"

--- a/src/ZF/Constructible/Formula.thy	Tue Jul 16 20:25:21 2002 +0200
+++ b/src/ZF/Constructible/Formula.thy	Wed Jul 17 15:48:54 2002 +0200
@@ -1013,4 +1013,80 @@
 theorem LPow_in_L: "L(X) ==> L({y \<in> Pow(X). L(y)})"
 by (blast intro: L_I dest: L_D LPow_in_Lset)
 
+
+subsection{*Eliminating @{term arity} from the Definition of @{term Lset}*}
+
+
+lemma nth_zero_eq_0: "n \<in> nat ==> nth(n,[0]) = 0"
+by (induct_tac n, auto)
+
+lemma sats_app_0_iff [rule_format]:
+  "[| p \<in> formula; 0 \<in> A |]
+   ==> \<forall>env \<in> list(A). sats(A,p, env@[0]) <-> sats(A,p,env)"
+apply (induct_tac p)
+apply (simp_all del: app_Cons add: app_Cons [symmetric]
+		add: nth_zero_eq_0 nth_append not_lt_iff_le nth_eq_0)
+done
+
+lemma sats_app_zeroes_iff:
+  "[| p \<in> formula; 0 \<in> A; env \<in> list(A); n \<in> nat |]
+   ==> sats(A,p,env @ repeat(0,n)) <-> sats(A,p,env)"
+apply (induct_tac n, simp) 
+apply (simp del: repeat.simps
+            add: repeat_succ_app sats_app_0_iff app_assoc [symmetric]) 
+done
+
+lemma exists_bigger_env:
+  "[| p \<in> formula; 0 \<in> A; env \<in> list(A) |]
+   ==> \<exists>env' \<in> list(A). arity(p) \<le> succ(length(env')) & 
+              (\<forall>a\<in>A. sats(A,p,Cons(a,env')) <-> sats(A,p,Cons(a,env)))"
+apply (rule_tac x="env @ repeat(0,arity(p))" in bexI) 
+apply (simp del: app_Cons add: app_Cons [symmetric]
+	    add: length_repeat sats_app_zeroes_iff, typecheck)
+done
+
+
+text{*A simpler version of @{term DPow}: no arity check!*}
+constdefs DPow' :: "i => i"
+  "DPow'(A) == {X \<in> Pow(A). 
+                \<exists>env \<in> list(A). \<exists>p \<in> formula. 
+                    X = {x\<in>A. sats(A, p, Cons(x,env))}}"
+
+lemma DPow_subset_DPow': "DPow(A) <= DPow'(A)";
+by (simp add: DPow_def DPow'_def, blast)
+
+lemma DPow'_0: "DPow'(0) = {0}"
+by (auto simp add: DPow'_def)
+
+lemma DPow'_subset_DPow: "0 \<in> A ==> DPow'(A) \<subseteq> DPow(A)"
+apply (auto simp add: DPow'_def DPow_def) 
+apply (frule exists_bigger_env, assumption+, force)  
+done
+
+lemma DPow_eq_DPow': "Transset(A) ==> DPow(A) = DPow'(A)"
+apply (drule Transset_0_disj) 
+apply (erule disjE) 
+ apply (simp add: DPow'_0 DPow_0) 
+apply (rule equalityI)
+ apply (rule DPow_subset_DPow') 
+apply (erule DPow'_subset_DPow) 
+done
+
+text{*And thus we can relativize @{term Lset} without bothering with
+      @{term arity} and @{term length}*}
+lemma Lset_eq_transrec_DPow': "Lset(i) = transrec(i, %x f. \<Union>y\<in>x. DPow'(f`y))"
+apply (rule_tac a=i in eps_induct)
+apply (subst Lset)
+apply (subst transrec)
+apply (simp only: DPow_eq_DPow' [OF Transset_Lset], simp) 
+done
+
+text{*With this rule we can specify @{term p} later and don't worry about
+      arities at all!*}
+lemma DPow_LsetI [rule_format]:
+  "[|\<forall>x\<in>Lset(i). P(x) <-> sats(Lset(i), p, Cons(x,env));
+     env \<in> list(Lset(i));  p \<in> formula|]
+   ==> {x\<in>Lset(i). P(x)} \<in> DPow(Lset(i))"
+by (simp add: DPow_eq_DPow' [OF Transset_Lset] DPow'_def, blast) 
+
 end

--- a/src/ZF/Constructible/L_axioms.thy	Tue Jul 16 20:25:21 2002 +0200
+++ b/src/ZF/Constructible/L_axioms.thy	Wed Jul 17 15:48:54 2002 +0200
@@ -372,6 +372,16 @@
 apply (intro FOL_reflections)  
 done
 
+text{*Not used.  But maybe useful?*}
+lemma Transset_sats_empty_fm_eq_0:
+   "[| n \<in> nat; env \<in> list(A); Transset(A)|]
+    ==> sats(A, empty_fm(n), env) <-> nth(n,env) = 0"
+apply (simp add: empty_fm_def empty_def Transset_def, auto)
+apply (case_tac "n < length(env)") 
+apply (frule nth_type, assumption+, blast)  
+apply (simp_all add: not_lt_iff_le nth_eq_0) 
+done
+
 
 subsubsection{*Unordered Pairs, Internalized*}
 

--- a/src/ZF/Constructible/Rec_Separation.thy	Tue Jul 16 20:25:21 2002 +0200
+++ b/src/ZF/Constructible/Rec_Separation.thy	Wed Jul 17 15:48:54 2002 +0200
@@ -80,11 +80,10 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u)
 apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats)
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -189,12 +188,11 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats conj_iff_sats)+
 apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats) 
 apply (rule sep_rules tran_closure_iff_sats | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -348,12 +346,11 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u)  
 apply (rule ball_iff_sats imp_iff_sats)+
 apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
 apply (rule sep_rules is_recfun_iff_sats | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -390,12 +387,11 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+
 apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats) 
 apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -430,12 +426,11 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u)  
 apply (rule ball_iff_sats imp_iff_sats)+
 apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats)
 apply (rule sep_rules is_recfun_iff_sats | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -790,7 +785,6 @@
 
 subsection{*@{term L} is Closed Under the Operator @{term list}*} 
 
-
 lemma list_replacement1_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
@@ -816,7 +810,7 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac v) 
 apply (rule bex_iff_sats conj_iff_sats)+
 apply (rule_tac env = "[u,v,A,n,B,0,Memrel(succ(n))]" in mem_iff_sats)
@@ -861,16 +855,13 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac v) 
 apply (rule bex_iff_sats conj_iff_sats)+
 apply (rule_tac env = "[u,v,A,B,0,nat]" in mem_iff_sats)
 apply (rule sep_rules | simp)+
 apply (simp add: is_wfrec_def M_is_recfun_def iterates_MH_def is_nat_case_def)
 apply (rule sep_rules list_functor_iff_sats quasinat_iff_sats | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric] Memrel_closed)
 done
 
-
-
 end

--- a/src/ZF/Constructible/Separation.thy	Tue Jul 16 20:25:21 2002 +0200
+++ b/src/ZF/Constructible/Separation.thy	Wed Jul 17 15:48:54 2002 +0200
@@ -61,7 +61,7 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify)
-apply (rule DPowI2) 
+apply (rule DPow_LsetI) 
 apply (rule ball_iff_sats) 
 apply (rule imp_iff_sats)
 apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats)
@@ -86,13 +86,12 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify) 
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u)  
 apply (rule bex_iff_sats) 
 apply (rule conj_iff_sats)
 apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all)
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 subsection{*Separation for Image*}
@@ -111,12 +110,11 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rule bex_iff_sats) 
 apply (rule conj_iff_sats)
 apply (rule_tac env="[p,y,A,r]" in mem_iff_sats)
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -137,13 +135,12 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats) 
 apply (rule conj_iff_sats)
 apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all)
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -162,13 +159,12 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats) 
 apply (rule conj_iff_sats)
 apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all)
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -194,14 +190,13 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats)+
 apply (rename_tac x y z)  
 apply (rule conj_iff_sats)
 apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats)
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 subsection{*Separation for Predecessors in an Order*}
@@ -219,13 +214,12 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2, clarify)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats)
 apply (rule conj_iff_sats)
 apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats) 
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -244,12 +238,11 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats conj_iff_sats)+
 apply (rule_tac env = "[y,x,u]" in pair_iff_sats) 
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -278,13 +271,12 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats)
 apply (rule conj_iff_sats)
 apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats) 
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -307,12 +299,11 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule imp_iff_sats)
 apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats) 
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -339,13 +330,12 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats)
 apply (rule conj_iff_sats)
 apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats) 
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -375,12 +365,11 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+
 apply (rule_tac env = "[u,A,r]" in mem_iff_sats) 
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -412,12 +401,11 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats conj_iff_sats)+
 apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats) 
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done
 
 
@@ -448,12 +436,11 @@
 apply (drule subset_Lset_ltD, assumption) 
 apply (erule reflection_imp_L_separation)
   apply (simp_all add: lt_Ord2)
-apply (rule DPowI2)
+apply (rule DPow_LsetI)
 apply (rename_tac u) 
 apply (rule bex_iff_sats conj_iff_sats)+
 apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats) 
 apply (rule sep_rules | simp)+
-apply (simp_all add: succ_Un_distrib [symmetric])
 done