author paulson Fri, 19 Jul 2002 13:29:22 +0200 changeset 13397 6e5f4d911435 parent 13396 11219ca224ab child 13398 1cadd412da48
Absoluteness of the function "nth"
--- a/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 19 13:28:19 2002 +0200
+++ b/src/ZF/Constructible/Datatype_absolute.thy	Fri Jul 19 13:29:22 2002 +0200
@@ -270,8 +270,69 @@
subsection{*@{term M} Contains the List and Formula Datatypes*}

constdefs
-  is_list_n :: "[i=>o,i,i,i] => o"
-    "is_list_n(M,A,n,Z) ==
+  list_N :: "[i,i] => i"
+    "list_N(A,n) == (\<lambda>X. {0} + A * X)^n (0)"
+
+lemma Nil_in_list_N [simp]: "[] \<in> list_N(A,succ(n))"
+
+lemma Cons_in_list_N [simp]:
+     "Cons(a,l) \<in> list_N(A,succ(n)) <-> a\<in>A & l \<in> list_N(A,n)"
+
+text{*These two aren't simprules because they reveal the underlying
+list representation.*}
+lemma list_N_0: "list_N(A,0) = 0"
+
+lemma list_N_succ: "list_N(A,succ(n)) = {0} + A * (list_N(A,n))"
+
+lemma list_N_imp_list:
+  "[| l \<in> list_N(A,n); n \<in> nat |] ==> l \<in> list(A)"
+by (force simp add: list_eq_Union list_N_def)
+
+lemma list_N_imp_length_lt [rule_format]:
+     "n \<in> nat ==> \<forall>l \<in> list_N(A,n). length(l) < n"
+apply (induct_tac n)
+apply (auto simp add: list_N_0 list_N_succ
+                      Nil_def [symmetric] Cons_def [symmetric])
+done
+
+lemma list_imp_list_N [rule_format]:
+     "l \<in> list(A) ==> \<forall>n\<in>nat. length(l) < n --> l \<in> list_N(A, n)"
+apply (induct_tac l)
+apply (force elim: natE)+
+done
+
+lemma list_N_imp_eq_length:
+      "[|n \<in> nat; l \<notin> list_N(A, n); l \<in> list_N(A, succ(n))|]
+       ==> n = length(l)"
+apply (rule le_anti_sym)
+ prefer 2 apply (simp add: list_N_imp_length_lt)
+apply (frule list_N_imp_list, simp)
+apply (blast intro: list_imp_list_N)
+done
+
+text{*Express @{term list_rec} without using @{term rank} or @{term Vset},
+neither of which is absolute.*}
+lemma (in M_triv_axioms) list_rec_eq:
+  "l \<in> list(A) ==>
+   list_rec(a,g,l) =
+   transrec (succ(length(l)),
+      \<lambda>x h. Lambda (list_N(A,x),
+             list_case' (a,
+                \<lambda>a l. g(a, l, h ` succ(length(l)) ` l)))) ` l"
+apply (induct_tac l)
+apply (subst transrec, simp)
+apply (subst transrec)
+done
+
+constdefs
+  is_list_N :: "[i=>o,i,i,i] => o"
+    "is_list_N(M,A,n,Z) ==
\<exists>zero[M]. \<exists>sn[M]. \<exists>msn[M].
empty(M,zero) &
successor(M,n,sn) & membership(M,sn,msn) &
@@ -280,7 +341,7 @@
mem_list :: "[i=>o,i,i] => o"
"mem_list(M,A,l) ==
\<exists>n[M]. \<exists>listn[M].
-       finite_ordinal(M,n) & is_list_n(M,A,n,listn) & l \<in> listn"
+       finite_ordinal(M,n) & is_list_N(M,A,n,listn) & l \<in> listn"

is_list :: "[i=>o,i,i] => o"
"is_list(M,A,Z) == \<forall>l[M]. l \<in> Z <-> mem_list(M,A,l)"
@@ -336,18 +397,26 @@
list_replacement2' relativize1_def
iterates_closed [of "is_list_functor(M,A)"])
-lemma (in M_datatypes) is_list_n_abs [simp]:
+
+lemma (in M_datatypes) list_N_abs [simp]:
"[|M(A); n\<in>nat; M(Z)|]
-      ==> is_list_n(M,A,n,Z) <-> Z = (\<lambda>X. {0} + A * X)^n (0)"
+      ==> is_list_N(M,A,n,Z) <-> Z = list_N(A,n)"
apply (insert list_replacement1)
-apply (simp add: is_list_n_def relativize1_def nat_into_M
+apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M
iterates_abs [of "is_list_functor(M,A)" _ "\<lambda>X. {0} + A*X"])
done

+lemma (in M_datatypes) list_N_closed [intro,simp]:
+     "[|M(A); n\<in>nat|] ==> M(list_N(A,n))"
+apply (insert list_replacement1)
+apply (simp add: is_list_N_def list_N_def relativize1_def nat_into_M
+                 iterates_closed [of "is_list_functor(M,A)"])
+done
+
lemma (in M_datatypes) mem_list_abs [simp]:
"M(A) ==> mem_list(M,A,l) <-> l \<in> list(A)"
apply (insert list_replacement1)
-apply (simp add: mem_list_def relativize1_def list_eq_Union
+apply (simp add: mem_list_def list_N_def relativize1_def list_eq_Union
iterates_closed [of "is_list_functor(M,A)"])
done

@@ -399,6 +468,8 @@
done

+subsection{*Absoluteness for Some List Operators*}
+
subsection{*Absoluteness for @{text \<epsilon>}-Closure: the @{term eclose} Operator*}

text{*Re-expresses eclose using "iterates"*}
@@ -494,11 +565,6 @@
upair(M,a,a,sa) & is_eclose(M,sa,esa) & membership(M,esa,mesa) &
wfrec_replacement(M,MH,mesa)"

-(*????????????????Ordinal.thy*)
-lemma Transset_trans_Memrel:
-    "\<forall>j\<in>i. Transset(j) ==> trans(Memrel(i))"
-by (unfold Transset_def trans_def, blast)
-
text{*The condition @{term "Ord(i)"} lets us use the simpler
@{text "trans_wfrec_abs"} rather than @{text "trans_wfrec_abs"},
which I haven't even proved yet. *}
@@ -521,5 +587,78 @@

+subsection{*Absoluteness for the List Operator @{term length}*}
+constdefs
+
+  is_length :: "[i=>o,i,i,i] => o"
+    "is_length(M,A,l,n) ==
+       \<exists>sn[M]. \<exists>list_n[M]. \<exists>list_sn[M].
+        is_list_N(M,A,n,list_n) & l \<notin> list_n &
+        successor(M,n,sn) & is_list_N(M,A,sn,list_sn) & l \<in> list_sn"
+
+
+lemma (in M_datatypes) length_abs [simp]:
+     "[|M(A); l \<in> list(A); n \<in> nat|] ==> is_length(M,A,l,n) <-> n = length(l)"
+apply (subgoal_tac "M(l) & M(n)")
+ prefer 2 apply (blast dest: transM)
+apply (blast intro: list_imp_list_N nat_into_Ord list_N_imp_eq_length
+             dest: list_N_imp_length_lt)
+done
+
+text{*Proof is trivial since @{term length} returns natural numbers.*}
+lemma (in M_triv_axioms) length_closed [intro,simp]:
+     "l \<in> list(A) ==> M(length(l))"
+
+
+subsection {*Absoluteness for @{term nth}*}
+
+lemma nth_eq_hd_iterates_tl [rule_format]:
+     "xs \<in> list(A) ==> \<forall>n \<in> nat. nth(n,xs) = hd' (tl'^n (xs))"
+apply (induct_tac xs)
+apply (simp add: iterates_tl_Nil hd'_Nil, clarify)
+apply (erule natE)
+done
+
+lemma (in M_axioms) iterates_tl'_closed:
+     "[|n \<in> nat; M(x)|] ==> M(tl'^n (x))"
+apply (induct_tac n, simp)
+done
+
+locale (open) M_nth = M_datatypes +
+ assumes nth_replacement1:
+   "M(xs) ==> iterates_replacement(M, %l t. is_tl(M,l,t), xs)"
+
+text{*Immediate by type-checking*}
+lemma (in M_datatypes) nth_closed [intro,simp]:
+     "[|xs \<in> list(A); n \<in> nat; M(A)|] ==> M(nth(n,xs))"
+apply (case_tac "n < length(xs)")
+ apply (blast intro: nth_type transM)
+done
+
+constdefs
+  is_nth :: "[i=>o,i,i,i] => o"
+    "is_nth(M,n,l,Z) ==
+      \<exists>X[M]. \<exists>sn[M]. \<exists>msn[M].
+       successor(M,n,sn) & membership(M,sn,msn) &
+       is_wfrec(M, iterates_MH(M, is_tl(M), l), msn, n, X) &
+       is_hd(M,X,Z)"
+
+lemma (in M_nth) nth_abs [simp]:
+     "[|M(A); n \<in> nat; l \<in> list(A); M(Z)|]
+      ==> is_nth(M,n,l,Z) <-> Z = nth(n,l)"
+apply (subgoal_tac "M(l)")
+ prefer 2 apply (blast intro: transM)
+apply (insert nth_replacement1)
+apply (simp add: is_nth_def nth_eq_hd_iterates_tl nat_into_M
+                 tl'_closed iterates_tl'_closed
+                 iterates_abs [OF _ relativize1_tl])
+done
+

end
--- a/src/ZF/Constructible/Relative.thy	Fri Jul 19 13:28:19 2002 +0200
+++ b/src/ZF/Constructible/Relative.thy	Fri Jul 19 13:29:22 2002 +0200
@@ -64,6 +64,12 @@
number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"

+  is_Inl :: "[i=>o,i,i] => o"
+    "is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z)"
+
+  is_Inr :: "[i=>o,i,i] => o"
+    "is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z)"
+
is_converse :: "[i=>o,i,i] => o"
"is_converse(M,r,z) ==
\<forall>x[M]. x \<in> z <->
@@ -899,6 +905,22 @@
"[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
by (simp add: is_sum_def sum_def singleton_0 nat_into_M)

+lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
+     "M(Inl(a)) <-> M(a)"
+
+lemma (in M_triv_axioms) Inl_abs [simp]:
+     "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
+
+lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
+     "M(Inr(a)) <-> M(a)"
+
+lemma (in M_triv_axioms) Inr_abs [simp]:
+     "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
+

subsubsection {*converse of a relation*}

@@ -1158,4 +1180,184 @@
done

+subsection{*Relativization and Absoluteness for List Operators*}
+
+constdefs
+
+  is_Nil :: "[i=>o, i] => o"
+     --{* because @{term "[] \<equiv> Inl(0)"}*}
+    "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
+
+  is_Cons :: "[i=>o,i,i,i] => o"
+     --{* because @{term "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
+    "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
+
+
+lemma (in M_triv_axioms) Nil_in_M [intro,simp]: "M(Nil)"
+
+lemma (in M_triv_axioms) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
+
+lemma (in M_triv_axioms) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
+
+lemma (in M_triv_axioms) Cons_abs [simp]:
+     "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
+
+
+constdefs
+
+  quasilist :: "i => o"
+    "quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"
+
+  is_quasilist :: "[i=>o,i] => o"
+    "is_quasilist(M,z) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))"
+
+  list_case' :: "[i, [i,i]=>i, i] => i"
+    --{*A version of @{term list_case} that's always defined.*}
+    "list_case'(a,b,xs) ==
+       if quasilist(xs) then list_case(a,b,xs) else 0"
+
+  is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
+    --{*Returns 0 for non-lists*}
+    "is_list_case(M, a, is_b, xs, z) ==
+       (is_Nil(M,xs) --> z=a) &
+       (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
+       (is_quasilist(M,xs) | empty(M,z))"
+
+  hd' :: "i => i"
+    --{*A version of @{term hd} that's always defined.*}
+    "hd'(xs) == if quasilist(xs) then hd(xs) else 0"
+
+  tl' :: "i => i"
+    --{*A version of @{term tl} that's always defined.*}
+    "tl'(xs) == if quasilist(xs) then tl(xs) else 0"
+
+  is_hd :: "[i=>o,i,i] => o"
+     --{* @{term "hd([]) = 0"} no constraints if not a list.
+          Avoiding implication prevents the simplifier's looping.*}
+    "is_hd(M,xs,H) ==
+       (is_Nil(M,xs) --> empty(M,H)) &
+       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
+       (is_quasilist(M,xs) | empty(M,H))"
+
+  is_tl :: "[i=>o,i,i] => o"
+    "is_tl(M,xs,T) ==
+       (is_Nil(M,xs) --> T=xs) &
+       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
+       (is_quasilist(M,xs) | empty(M,T))"
+
+subsubsection{*@{term quasilist}: For Case-Splitting with @{term list_case'}*}
+
+lemma [iff]: "quasilist(Nil)"
+
+lemma [iff]: "quasilist(Cons(x,l))"
+
+lemma list_imp_quasilist: "l \<in> list(A) ==> quasilist(l)"
+by (erule list.cases, simp_all)
+
+subsubsection{*@{term list_case'}, the Modified Version of @{term list_case}*}
+
+lemma list_case'_Nil [simp]: "list_case'(a,b,Nil) = a"
+
+lemma list_case'_Cons [simp]: "list_case'(a,b,Cons(x,l)) = b(x,l)"
+
+lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0"
+
+lemma list_case'_eq_list_case [simp]:
+     "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
+by (erule list.cases, simp_all)
+
+lemma (in M_axioms) list_case'_closed [intro,simp]:
+  "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
+apply (case_tac "quasilist(k)")
+ apply (simp add: quasilist_def, force)
+done
+
+lemma (in M_triv_axioms) quasilist_abs [simp]:
+     "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
+by (auto simp add: is_quasilist_def quasilist_def)
+
+lemma (in M_triv_axioms) list_case_abs [simp]:
+     "[| relativize2(M,is_b,b); M(k); M(z) |]
+      ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
+apply (case_tac "quasilist(k)")
+ prefer 2
+ apply (simp add: is_list_case_def non_list_case)
+ apply (force simp add: quasilist_def)
+apply (elim disjE exE)
+done
+
+
+subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
+
+lemma (in M_triv_axioms) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
+
+lemma (in M_triv_axioms) is_hd_Cons:
+     "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
+by (force simp add: is_hd_def )
+
+lemma (in M_triv_axioms) hd_abs [simp]:
+     "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
+apply (intro impI conjI)
+ prefer 2 apply (force simp add: is_hd_def)
+apply (simp add: quasilist_def is_hd_def )
+apply (elim disjE exE, auto)
+done
+
+lemma (in M_triv_axioms) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
+
+lemma (in M_triv_axioms) is_tl_Cons:
+     "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
+by (force simp add: is_tl_def )
+
+lemma (in M_triv_axioms) tl_abs [simp]:
+     "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
+apply (intro impI conjI)
+ prefer 2 apply (force simp add: is_tl_def)
+apply (simp add: quasilist_def is_tl_def )
+apply (elim disjE exE, auto)
+done
+
+lemma (in M_triv_axioms) relativize1_tl: "relativize1(M, is_tl(M), tl')"
+
+lemma hd'_Nil: "hd'([]) = 0"
+
+lemma hd'_Cons: "hd'(Cons(a,l)) = a"
+
+lemma tl'_Nil: "tl'([]) = []"
+
+lemma tl'_Cons: "tl'(Cons(a,l)) = l"