author paulson Wed, 17 Jul 2002 15:48:54 +0200 changeset 13385 31df66ca0780 parent 13384 a34e38154413 child 13386 f3e9e8b21aba
Expressing Lset and L without using length and arity; simplifies Separation proofs
 src/ZF/Constructible/Datatype_absolute.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/Formula.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/L_axioms.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/Rec_Separation.thy file | annotate | diff | comparison | revisions src/ZF/Constructible/Separation.thy file | annotate | diff | comparison | revisions
```--- 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)
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 (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))"
+    "[|bnd_mono(D, h); contin(h)|]
+     ==> h(\<Union>n\<in>nat. h^n (0)) = (\<Union>n\<in>nat. h^n (0))"
apply (rule trans)
apply (rule equalityI)
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 (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))"
+
+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 (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)"
+
+lemma id_contin: "contin(\<lambda>X. X)"
+
+
+
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 (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]
+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}"
+
+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)
+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 (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)+
done

@@ -189,12 +188,11 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -348,12 +346,11 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -390,12 +387,11 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -430,12 +426,11 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
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 (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 (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 (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 (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)+
done

subsection{*Separation for Image*}
@@ -111,12 +110,11 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -137,13 +135,12 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -162,13 +159,12 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -194,14 +190,13 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
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 (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)+
done

@@ -244,12 +238,11 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -278,13 +271,12 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -307,12 +299,11 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -339,13 +330,12 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -375,12 +365,11 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -412,12 +401,11 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)
-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)+
done

@@ -448,12 +436,11 @@
apply (drule subset_Lset_ltD, assumption)
apply (erule reflection_imp_L_separation)