src/ZF/Constructible/Relative.thy
 changeset 13397 6e5f4d911435 parent 13382 b37764a46b16 child 13418 7c0ba9dba978
```     1.1 --- a/src/ZF/Constructible/Relative.thy	Fri Jul 19 13:28:19 2002 +0200
1.2 +++ b/src/ZF/Constructible/Relative.thy	Fri Jul 19 13:29:22 2002 +0200
1.3 @@ -64,6 +64,12 @@
1.4         number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) &
1.5         cartprod(M,s1,B,B1) & union(M,A0,B1,Z)"
1.6
1.7 +  is_Inl :: "[i=>o,i,i] => o"
1.8 +    "is_Inl(M,a,z) == \<exists>zero[M]. empty(M,zero) & pair(M,zero,a,z)"
1.9 +
1.10 +  is_Inr :: "[i=>o,i,i] => o"
1.11 +    "is_Inr(M,a,z) == \<exists>n1[M]. number1(M,n1) & pair(M,n1,a,z)"
1.12 +
1.13    is_converse :: "[i=>o,i,i] => o"
1.14      "is_converse(M,r,z) ==
1.15  	\<forall>x[M]. x \<in> z <->
1.16 @@ -899,6 +905,22 @@
1.17       "[| M(A); M(B); M(Z) |] ==> is_sum(M,A,B,Z) <-> (Z = A+B)"
1.18  by (simp add: is_sum_def sum_def singleton_0 nat_into_M)
1.19
1.20 +lemma (in M_triv_axioms) Inl_in_M_iff [iff]:
1.21 +     "M(Inl(a)) <-> M(a)"
1.23 +
1.24 +lemma (in M_triv_axioms) Inl_abs [simp]:
1.25 +     "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))"
1.26 +by (simp add: is_Inl_def Inl_def)
1.27 +
1.28 +lemma (in M_triv_axioms) Inr_in_M_iff [iff]:
1.29 +     "M(Inr(a)) <-> M(a)"
1.31 +
1.32 +lemma (in M_triv_axioms) Inr_abs [simp]:
1.33 +     "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))"
1.34 +by (simp add: is_Inr_def Inr_def)
1.35 +
1.36
1.37  subsubsection {*converse of a relation*}
1.38
1.39 @@ -1158,4 +1180,184 @@
1.40  done
1.41
1.42
1.43 +subsection{*Relativization and Absoluteness for List Operators*}
1.44 +
1.45 +constdefs
1.46 +
1.47 +  is_Nil :: "[i=>o, i] => o"
1.48 +     --{* because @{term "[] \<equiv> Inl(0)"}*}
1.49 +    "is_Nil(M,xs) == \<exists>zero[M]. empty(M,zero) & is_Inl(M,zero,xs)"
1.50 +
1.51 +  is_Cons :: "[i=>o,i,i,i] => o"
1.52 +     --{* because @{term "Cons(a, l) \<equiv> Inr(\<langle>a,l\<rangle>)"}*}
1.53 +    "is_Cons(M,a,l,Z) == \<exists>p[M]. pair(M,a,l,p) & is_Inr(M,p,Z)"
1.54 +
1.55 +
1.56 +lemma (in M_triv_axioms) Nil_in_M [intro,simp]: "M(Nil)"
1.58 +
1.59 +lemma (in M_triv_axioms) Nil_abs [simp]: "M(Z) ==> is_Nil(M,Z) <-> (Z = Nil)"
1.60 +by (simp add: is_Nil_def Nil_def)
1.61 +
1.62 +lemma (in M_triv_axioms) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)"
1.64 +
1.65 +lemma (in M_triv_axioms) Cons_abs [simp]:
1.66 +     "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))"
1.67 +by (simp add: is_Cons_def Cons_def)
1.68 +
1.69 +
1.70 +constdefs
1.71 +
1.72 +  quasilist :: "i => o"
1.73 +    "quasilist(xs) == xs=Nil | (\<exists>x l. xs = Cons(x,l))"
1.74 +
1.75 +  is_quasilist :: "[i=>o,i] => o"
1.76 +    "is_quasilist(M,z) == is_Nil(M,z) | (\<exists>x[M]. \<exists>l[M]. is_Cons(M,x,l,z))"
1.77 +
1.78 +  list_case' :: "[i, [i,i]=>i, i] => i"
1.79 +    --{*A version of @{term list_case} that's always defined.*}
1.80 +    "list_case'(a,b,xs) ==
1.81 +       if quasilist(xs) then list_case(a,b,xs) else 0"
1.82 +
1.83 +  is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o"
1.84 +    --{*Returns 0 for non-lists*}
1.85 +    "is_list_case(M, a, is_b, xs, z) ==
1.86 +       (is_Nil(M,xs) --> z=a) &
1.87 +       (\<forall>x[M]. \<forall>l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) &
1.88 +       (is_quasilist(M,xs) | empty(M,z))"
1.89 +
1.90 +  hd' :: "i => i"
1.91 +    --{*A version of @{term hd} that's always defined.*}
1.92 +    "hd'(xs) == if quasilist(xs) then hd(xs) else 0"
1.93 +
1.94 +  tl' :: "i => i"
1.95 +    --{*A version of @{term tl} that's always defined.*}
1.96 +    "tl'(xs) == if quasilist(xs) then tl(xs) else 0"
1.97 +
1.98 +  is_hd :: "[i=>o,i,i] => o"
1.99 +     --{* @{term "hd([]) = 0"} no constraints if not a list.
1.100 +          Avoiding implication prevents the simplifier's looping.*}
1.101 +    "is_hd(M,xs,H) ==
1.102 +       (is_Nil(M,xs) --> empty(M,H)) &
1.103 +       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | H=x) &
1.104 +       (is_quasilist(M,xs) | empty(M,H))"
1.105 +
1.106 +  is_tl :: "[i=>o,i,i] => o"
1.107 +     --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*}
1.108 +    "is_tl(M,xs,T) ==
1.109 +       (is_Nil(M,xs) --> T=xs) &
1.110 +       (\<forall>x[M]. \<forall>l[M]. ~ is_Cons(M,x,l,xs) | T=l) &
1.111 +       (is_quasilist(M,xs) | empty(M,T))"
1.112 +
1.113 +subsubsection{*@{term quasilist}: For Case-Splitting with @{term list_case'}*}
1.114 +
1.115 +lemma [iff]: "quasilist(Nil)"
1.117 +
1.118 +lemma [iff]: "quasilist(Cons(x,l))"
1.120 +
1.121 +lemma list_imp_quasilist: "l \<in> list(A) ==> quasilist(l)"
1.122 +by (erule list.cases, simp_all)
1.123 +
1.124 +subsubsection{*@{term list_case'}, the Modified Version of @{term list_case}*}
1.125 +
1.126 +lemma list_case'_Nil [simp]: "list_case'(a,b,Nil) = a"
1.127 +by (simp add: list_case'_def quasilist_def)
1.128 +
1.129 +lemma list_case'_Cons [simp]: "list_case'(a,b,Cons(x,l)) = b(x,l)"
1.130 +by (simp add: list_case'_def quasilist_def)
1.131 +
1.132 +lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0"
1.133 +by (simp add: quasilist_def list_case'_def)
1.134 +
1.135 +lemma list_case'_eq_list_case [simp]:
1.136 +     "xs \<in> list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)"
1.137 +by (erule list.cases, simp_all)
1.138 +
1.139 +lemma (in M_axioms) list_case'_closed [intro,simp]:
1.140 +  "[|M(k); M(a); \<forall>x[M]. \<forall>y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))"
1.141 +apply (case_tac "quasilist(k)")
1.142 + apply (simp add: quasilist_def, force)
1.144 +done
1.145 +
1.146 +lemma (in M_triv_axioms) quasilist_abs [simp]:
1.147 +     "M(z) ==> is_quasilist(M,z) <-> quasilist(z)"
1.148 +by (auto simp add: is_quasilist_def quasilist_def)
1.149 +
1.150 +lemma (in M_triv_axioms) list_case_abs [simp]:
1.151 +     "[| relativize2(M,is_b,b); M(k); M(z) |]
1.152 +      ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)"
1.153 +apply (case_tac "quasilist(k)")
1.154 + prefer 2
1.155 + apply (simp add: is_list_case_def non_list_case)
1.156 + apply (force simp add: quasilist_def)
1.157 +apply (simp add: quasilist_def is_list_case_def)
1.158 +apply (elim disjE exE)
1.159 + apply (simp_all add: relativize2_def)
1.160 +done
1.161 +
1.162 +
1.163 +subsubsection{*The Modified Operators @{term hd'} and @{term tl'}*}
1.164 +
1.165 +lemma (in M_triv_axioms) is_hd_Nil: "is_hd(M,[],Z) <-> empty(M,Z)"
1.166 +by (simp add: is_hd_def )
1.167 +
1.168 +lemma (in M_triv_axioms) is_hd_Cons:
1.169 +     "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a"
1.170 +by (force simp add: is_hd_def )
1.171 +
1.172 +lemma (in M_triv_axioms) hd_abs [simp]:
1.173 +     "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)"
1.175 +apply (intro impI conjI)
1.176 + prefer 2 apply (force simp add: is_hd_def)
1.177 +apply (simp add: quasilist_def is_hd_def )
1.178 +apply (elim disjE exE, auto)
1.179 +done
1.180 +
1.181 +lemma (in M_triv_axioms) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []"
1.182 +by (simp add: is_tl_def )
1.183 +
1.184 +lemma (in M_triv_axioms) is_tl_Cons:
1.185 +     "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l"
1.186 +by (force simp add: is_tl_def )
1.187 +
1.188 +lemma (in M_triv_axioms) tl_abs [simp]:
1.189 +     "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)"
1.191 +apply (intro impI conjI)
1.192 + prefer 2 apply (force simp add: is_tl_def)
1.193 +apply (simp add: quasilist_def is_tl_def )
1.194 +apply (elim disjE exE, auto)
1.195 +done
1.196 +
1.197 +lemma (in M_triv_axioms) relativize1_tl: "relativize1(M, is_tl(M), tl')"
1.199 +
1.200 +lemma hd'_Nil: "hd'([]) = 0"
1.202 +
1.203 +lemma hd'_Cons: "hd'(Cons(a,l)) = a"
1.205 +
1.206 +lemma tl'_Nil: "tl'([]) = []"
1.208 +
1.209 +lemma tl'_Cons: "tl'(Cons(a,l)) = l"
1.211 +
1.212 +lemma iterates_tl_Nil: "n \<in> nat ==> tl'^n ([]) = []"
1.213 +apply (induct_tac n)