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.22 +by (simp add: Inl_def) 
    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.30 +by (simp add: Inr_def) 
    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.57 +by (simp add: Nil_def)
    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.63 +by (simp add: Cons_def) 
    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.116 +by (simp add: quasilist_def)
   1.117 +
   1.118 +lemma [iff]: "quasilist(Cons(x,l))"
   1.119 +by (simp add: quasilist_def)
   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.143 +apply (simp add: non_list_case) 
   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.174 +apply (simp add: hd'_def)
   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.190 +apply (simp add: tl'_def)
   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.198 +by (simp add: relativize1_def)
   1.199 +
   1.200 +lemma hd'_Nil: "hd'([]) = 0"
   1.201 +by (simp add: hd'_def)
   1.202 +
   1.203 +lemma hd'_Cons: "hd'(Cons(a,l)) = a"
   1.204 +by (simp add: hd'_def)
   1.205 +
   1.206 +lemma tl'_Nil: "tl'([]) = []"
   1.207 +by (simp add: tl'_def)
   1.208 +
   1.209 +lemma tl'_Cons: "tl'(Cons(a,l)) = l"
   1.210 +by (simp add: tl'_def)
   1.211 +
   1.212 +lemma iterates_tl_Nil: "n \<in> nat ==> tl'^n ([]) = []"
   1.213 +apply (induct_tac n) 
   1.214 +apply (simp_all add: tl'_Nil) 
   1.215 +done
   1.216 +
   1.217 +lemma (in M_axioms) tl'_closed: "M(x) ==> M(tl'(x))"
   1.218 +apply (simp add: tl'_def)
   1.219 +apply (force simp add: quasilist_def)
   1.220 +done
   1.221 +
   1.222 +
   1.223  end