src/ZF/Epsilon.thy
 author wenzelm Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago) changeset 49566 66cbf8bb4693 parent 46953 2b6e55924af3 child 58860 fee7cfa69c50 permissions -rw-r--r--
basic integration of graphview into document model;
updated Isabelle/jEdit authors and dependencies etc.;
```     1 (*  Title:      ZF/Epsilon.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1993  University of Cambridge
```
```     4 *)
```
```     5
```
```     6 header{*Epsilon Induction and Recursion*}
```
```     7
```
```     8 theory Epsilon imports Nat_ZF begin
```
```     9
```
```    10 definition
```
```    11   eclose    :: "i=>i"  where
```
```    12     "eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. \<Union>(r))"
```
```    13
```
```    14 definition
```
```    15   transrec  :: "[i, [i,i]=>i] =>i"  where
```
```    16     "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
```
```    17
```
```    18 definition
```
```    19   rank      :: "i=>i"  where
```
```    20     "rank(a) == transrec(a, %x f. \<Union>y\<in>x. succ(f`y))"
```
```    21
```
```    22 definition
```
```    23   transrec2 :: "[i, i, [i,i]=>i] =>i"  where
```
```    24     "transrec2(k, a, b) ==
```
```    25        transrec(k,
```
```    26                 %i r. if(i=0, a,
```
```    27                         if(\<exists>j. i=succ(j),
```
```    28                            b(THE j. i=succ(j), r`(THE j. i=succ(j))),
```
```    29                            \<Union>j<i. r`j)))"
```
```    30
```
```    31 definition
```
```    32   recursor  :: "[i, [i,i]=>i, i]=>i"  where
```
```    33     "recursor(a,b,k) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
```
```    34
```
```    35 definition
```
```    36   rec  :: "[i, i, [i,i]=>i]=>i"  where
```
```    37     "rec(k,a,b) == recursor(a,b,k)"
```
```    38
```
```    39
```
```    40 subsection{*Basic Closure Properties*}
```
```    41
```
```    42 lemma arg_subset_eclose: "A \<subseteq> eclose(A)"
```
```    43 apply (unfold eclose_def)
```
```    44 apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans])
```
```    45 apply (rule nat_0I [THEN UN_upper])
```
```    46 done
```
```    47
```
```    48 lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD]
```
```    49
```
```    50 lemma Transset_eclose: "Transset(eclose(A))"
```
```    51 apply (unfold eclose_def Transset_def)
```
```    52 apply (rule subsetI [THEN ballI])
```
```    53 apply (erule UN_E)
```
```    54 apply (rule nat_succI [THEN UN_I], assumption)
```
```    55 apply (erule nat_rec_succ [THEN ssubst])
```
```    56 apply (erule UnionI, assumption)
```
```    57 done
```
```    58
```
```    59 (* @{term"x \<in> eclose(A) ==> x \<subseteq> eclose(A)"} *)
```
```    60 lemmas eclose_subset =
```
```    61        Transset_eclose [unfolded Transset_def, THEN bspec]
```
```    62
```
```    63 (* @{term"[| A \<in> eclose(B); c \<in> A |] ==> c \<in> eclose(B)"} *)
```
```    64 lemmas ecloseD = eclose_subset [THEN subsetD]
```
```    65
```
```    66 lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD]
```
```    67 lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD]
```
```    68
```
```    69 (* This is epsilon-induction for eclose(A); see also eclose_induct_down...
```
```    70    [| a \<in> eclose(A);  !!x. [| x \<in> eclose(A); \<forall>y\<in>x. P(y) |] ==> P(x)
```
```    71    |] ==> P(a)
```
```    72 *)
```
```    73 lemmas eclose_induct =
```
```    74      Transset_induct [OF _ Transset_eclose, induct set: eclose]
```
```    75
```
```    76
```
```    77 (*Epsilon induction*)
```
```    78 lemma eps_induct:
```
```    79     "[| !!x. \<forall>y\<in>x. P(y) ==> P(x) |]  ==>  P(a)"
```
```    80 by (rule arg_in_eclose_sing [THEN eclose_induct], blast)
```
```    81
```
```    82
```
```    83 subsection{*Leastness of @{term eclose}*}
```
```    84
```
```    85 (** eclose(A) is the least transitive set including A as a subset. **)
```
```    86
```
```    87 lemma eclose_least_lemma:
```
```    88     "[| Transset(X);  A<=X;  n \<in> nat |] ==> nat_rec(n, A, %m r. \<Union>(r)) \<subseteq> X"
```
```    89 apply (unfold Transset_def)
```
```    90 apply (erule nat_induct)
```
```    91 apply (simp add: nat_rec_0)
```
```    92 apply (simp add: nat_rec_succ, blast)
```
```    93 done
```
```    94
```
```    95 lemma eclose_least:
```
```    96      "[| Transset(X);  A<=X |] ==> eclose(A) \<subseteq> X"
```
```    97 apply (unfold eclose_def)
```
```    98 apply (rule eclose_least_lemma [THEN UN_least], assumption+)
```
```    99 done
```
```   100
```
```   101 (*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
```
```   102 lemma eclose_induct_down [consumes 1]:
```
```   103     "[| a \<in> eclose(b);
```
```   104         !!y.   [| y \<in> b |] ==> P(y);
```
```   105         !!y z. [| y \<in> eclose(b);  P(y);  z \<in> y |] ==> P(z)
```
```   106      |] ==> P(a)"
```
```   107 apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"])
```
```   108   prefer 3 apply assumption
```
```   109  apply (unfold Transset_def)
```
```   110  apply (blast intro: ecloseD)
```
```   111 apply (blast intro: arg_subset_eclose [THEN subsetD])
```
```   112 done
```
```   113
```
```   114 lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
```
```   115 apply (erule equalityI [OF eclose_least arg_subset_eclose])
```
```   116 apply (rule subset_refl)
```
```   117 done
```
```   118
```
```   119 text{*A transitive set either is empty or contains the empty set.*}
```
```   120 lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A \<longrightarrow> 0\<in>A";
```
```   121 apply (simp add: Transset_def)
```
```   122 apply (rule_tac a=x in eps_induct, clarify)
```
```   123 apply (drule bspec, assumption)
```
```   124 apply (case_tac "x=0", auto)
```
```   125 done
```
```   126
```
```   127 lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A";
```
```   128 by (blast dest: Transset_0_lemma)
```
```   129
```
```   130
```
```   131 subsection{*Epsilon Recursion*}
```
```   132
```
```   133 (*Unused...*)
```
```   134 lemma mem_eclose_trans: "[| A \<in> eclose(B);  B \<in> eclose(C) |] ==> A \<in> eclose(C)"
```
```   135 by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD],
```
```   136     assumption+)
```
```   137
```
```   138 (*Variant of the previous lemma in a useable form for the sequel*)
```
```   139 lemma mem_eclose_sing_trans:
```
```   140      "[| A \<in> eclose({B});  B \<in> eclose({C}) |] ==> A \<in> eclose({C})"
```
```   141 by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD],
```
```   142     assumption+)
```
```   143
```
```   144 lemma under_Memrel: "[| Transset(i);  j \<in> i |] ==> Memrel(i)-``{j} = j"
```
```   145 by (unfold Transset_def, blast)
```
```   146
```
```   147 lemma lt_Memrel: "j < i ==> Memrel(i) -`` {j} = j"
```
```   148 by (simp add: lt_def Ord_def under_Memrel)
```
```   149
```
```   150 (* @{term"j \<in> eclose(A) ==> Memrel(eclose(A)) -`` j = j"} *)
```
```   151 lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel]
```
```   152
```
```   153 lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst]
```
```   154
```
```   155 lemma wfrec_eclose_eq:
```
```   156     "[| k \<in> eclose({j});  j \<in> eclose({i}) |] ==>
```
```   157      wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)"
```
```   158 apply (erule eclose_induct)
```
```   159 apply (rule wfrec_ssubst)
```
```   160 apply (rule wfrec_ssubst)
```
```   161 apply (simp add: under_Memrel_eclose mem_eclose_sing_trans [of _ j i])
```
```   162 done
```
```   163
```
```   164 lemma wfrec_eclose_eq2:
```
```   165     "k \<in> i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)"
```
```   166 apply (rule arg_in_eclose_sing [THEN wfrec_eclose_eq])
```
```   167 apply (erule arg_into_eclose_sing)
```
```   168 done
```
```   169
```
```   170 lemma transrec: "transrec(a,H) = H(a, \<lambda>x\<in>a. transrec(x,H))"
```
```   171 apply (unfold transrec_def)
```
```   172 apply (rule wfrec_ssubst)
```
```   173 apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose)
```
```   174 done
```
```   175
```
```   176 (*Avoids explosions in proofs; resolve it with a meta-level definition.*)
```
```   177 lemma def_transrec:
```
```   178     "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, \<lambda>x\<in>a. f(x))"
```
```   179 apply simp
```
```   180 apply (rule transrec)
```
```   181 done
```
```   182
```
```   183 lemma transrec_type:
```
```   184     "[| !!x u. [| x \<in> eclose({a});  u \<in> Pi(x,B) |] ==> H(x,u) \<in> B(x) |]
```
```   185      ==> transrec(a,H) \<in> B(a)"
```
```   186 apply (rule_tac i = a in arg_in_eclose_sing [THEN eclose_induct])
```
```   187 apply (subst transrec)
```
```   188 apply (simp add: lam_type)
```
```   189 done
```
```   190
```
```   191 lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) \<subseteq> succ(i)"
```
```   192 apply (erule Ord_is_Transset [THEN Transset_succ, THEN eclose_least])
```
```   193 apply (rule succI1 [THEN singleton_subsetI])
```
```   194 done
```
```   195
```
```   196 lemma succ_subset_eclose_sing: "succ(i) \<subseteq> eclose({i})"
```
```   197 apply (insert arg_subset_eclose [of "{i}"], simp)
```
```   198 apply (frule eclose_subset, blast)
```
```   199 done
```
```   200
```
```   201 lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
```
```   202 apply (rule equalityI)
```
```   203 apply (erule eclose_sing_Ord)
```
```   204 apply (rule succ_subset_eclose_sing)
```
```   205 done
```
```   206
```
```   207 lemma Ord_transrec_type:
```
```   208   assumes jini: "j \<in> i"
```
```   209       and ordi: "Ord(i)"
```
```   210       and minor: " !!x u. [| x \<in> i;  u \<in> Pi(x,B) |] ==> H(x,u) \<in> B(x)"
```
```   211   shows "transrec(j,H) \<in> B(j)"
```
```   212 apply (rule transrec_type)
```
```   213 apply (insert jini ordi)
```
```   214 apply (blast intro!: minor
```
```   215              intro: Ord_trans
```
```   216              dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD])
```
```   217 done
```
```   218
```
```   219 subsection{*Rank*}
```
```   220
```
```   221 (*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
```
```   222 lemma rank: "rank(a) = (\<Union>y\<in>a. succ(rank(y)))"
```
```   223 by (subst rank_def [THEN def_transrec], simp)
```
```   224
```
```   225 lemma Ord_rank [simp]: "Ord(rank(a))"
```
```   226 apply (rule_tac a=a in eps_induct)
```
```   227 apply (subst rank)
```
```   228 apply (rule Ord_succ [THEN Ord_UN])
```
```   229 apply (erule bspec, assumption)
```
```   230 done
```
```   231
```
```   232 lemma rank_of_Ord: "Ord(i) ==> rank(i) = i"
```
```   233 apply (erule trans_induct)
```
```   234 apply (subst rank)
```
```   235 apply (simp add: Ord_equality)
```
```   236 done
```
```   237
```
```   238 lemma rank_lt: "a \<in> b ==> rank(a) < rank(b)"
```
```   239 apply (rule_tac a1 = b in rank [THEN ssubst])
```
```   240 apply (erule UN_I [THEN ltI])
```
```   241 apply (rule_tac [2] Ord_UN, auto)
```
```   242 done
```
```   243
```
```   244 lemma eclose_rank_lt: "a \<in> eclose(b) ==> rank(a) < rank(b)"
```
```   245 apply (erule eclose_induct_down)
```
```   246 apply (erule rank_lt)
```
```   247 apply (erule rank_lt [THEN lt_trans], assumption)
```
```   248 done
```
```   249
```
```   250 lemma rank_mono: "a<=b ==> rank(a) \<le> rank(b)"
```
```   251 apply (rule subset_imp_le)
```
```   252 apply (auto simp add: rank [of a] rank [of b])
```
```   253 done
```
```   254
```
```   255 lemma rank_Pow: "rank(Pow(a)) = succ(rank(a))"
```
```   256 apply (rule rank [THEN trans])
```
```   257 apply (rule le_anti_sym)
```
```   258 apply (rule_tac [2] UN_upper_le)
```
```   259 apply (rule UN_least_le)
```
```   260 apply (auto intro: rank_mono simp add: Ord_UN)
```
```   261 done
```
```   262
```
```   263 lemma rank_0 [simp]: "rank(0) = 0"
```
```   264 by (rule rank [THEN trans], blast)
```
```   265
```
```   266 lemma rank_succ [simp]: "rank(succ(x)) = succ(rank(x))"
```
```   267 apply (rule rank [THEN trans])
```
```   268 apply (rule equalityI [OF UN_least succI1 [THEN UN_upper]])
```
```   269 apply (erule succE, blast)
```
```   270 apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset])
```
```   271 done
```
```   272
```
```   273 lemma rank_Union: "rank(\<Union>(A)) = (\<Union>x\<in>A. rank(x))"
```
```   274 apply (rule equalityI)
```
```   275 apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least])
```
```   276 apply (erule_tac [2] Union_upper)
```
```   277 apply (subst rank)
```
```   278 apply (rule UN_least)
```
```   279 apply (erule UnionE)
```
```   280 apply (rule subset_trans)
```
```   281 apply (erule_tac [2] RepFunI [THEN Union_upper])
```
```   282 apply (erule rank_lt [THEN succ_leI, THEN le_imp_subset])
```
```   283 done
```
```   284
```
```   285 lemma rank_eclose: "rank(eclose(a)) = rank(a)"
```
```   286 apply (rule le_anti_sym)
```
```   287 apply (rule_tac [2] arg_subset_eclose [THEN rank_mono])
```
```   288 apply (rule_tac a1 = "eclose (a) " in rank [THEN ssubst])
```
```   289 apply (rule Ord_rank [THEN UN_least_le])
```
```   290 apply (erule eclose_rank_lt [THEN succ_leI])
```
```   291 done
```
```   292
```
```   293 lemma rank_pair1: "rank(a) < rank(<a,b>)"
```
```   294 apply (unfold Pair_def)
```
```   295 apply (rule consI1 [THEN rank_lt, THEN lt_trans])
```
```   296 apply (rule consI1 [THEN consI2, THEN rank_lt])
```
```   297 done
```
```   298
```
```   299 lemma rank_pair2: "rank(b) < rank(<a,b>)"
```
```   300 apply (unfold Pair_def)
```
```   301 apply (rule consI1 [THEN consI2, THEN rank_lt, THEN lt_trans])
```
```   302 apply (rule consI1 [THEN consI2, THEN rank_lt])
```
```   303 done
```
```   304
```
```   305 (*Not clear how to remove the P(a) condition, since the "then" part
```
```   306   must refer to "a"*)
```
```   307 lemma the_equality_if:
```
```   308      "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
```
```   309 by (simp add: the_0 the_equality2)
```
```   310
```
```   311 (*The first premise not only fixs i but ensures @{term"f\<noteq>0"}.
```
```   312   The second premise is now essential.  Consider otherwise the relation
```
```   313   r = {<0,0>,<0,1>,<0,2>,...}.  Then f`0 = \<Union>(f``{0}) = \<Union>(nat) = nat,
```
```   314   whose rank equals that of r.*)
```
```   315 lemma rank_apply: "[|i \<in> domain(f); function(f)|] ==> rank(f`i) < rank(f)"
```
```   316 apply clarify
```
```   317 apply (simp add: function_apply_equality)
```
```   318 apply (blast intro: lt_trans rank_lt rank_pair2)
```
```   319 done
```
```   320
```
```   321
```
```   322 subsection{*Corollaries of Leastness*}
```
```   323
```
```   324 lemma mem_eclose_subset: "A \<in> B ==> eclose(A)<=eclose(B)"
```
```   325 apply (rule Transset_eclose [THEN eclose_least])
```
```   326 apply (erule arg_into_eclose [THEN eclose_subset])
```
```   327 done
```
```   328
```
```   329 lemma eclose_mono: "A<=B ==> eclose(A) \<subseteq> eclose(B)"
```
```   330 apply (rule Transset_eclose [THEN eclose_least])
```
```   331 apply (erule subset_trans)
```
```   332 apply (rule arg_subset_eclose)
```
```   333 done
```
```   334
```
```   335 (** Idempotence of eclose **)
```
```   336
```
```   337 lemma eclose_idem: "eclose(eclose(A)) = eclose(A)"
```
```   338 apply (rule equalityI)
```
```   339 apply (rule eclose_least [OF Transset_eclose subset_refl])
```
```   340 apply (rule arg_subset_eclose)
```
```   341 done
```
```   342
```
```   343 (** Transfinite recursion for definitions based on the
```
```   344     three cases of ordinals **)
```
```   345
```
```   346 lemma transrec2_0 [simp]: "transrec2(0,a,b) = a"
```
```   347 by (rule transrec2_def [THEN def_transrec, THEN trans], simp)
```
```   348
```
```   349 lemma transrec2_succ [simp]: "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"
```
```   350 apply (rule transrec2_def [THEN def_transrec, THEN trans])
```
```   351 apply (simp add: the_equality if_P)
```
```   352 done
```
```   353
```
```   354 lemma transrec2_Limit:
```
```   355      "Limit(i) ==> transrec2(i,a,b) = (\<Union>j<i. transrec2(j,a,b))"
```
```   356 apply (rule transrec2_def [THEN def_transrec, THEN trans])
```
```   357 apply (auto simp add: OUnion_def)
```
```   358 done
```
```   359
```
```   360 lemma def_transrec2:
```
```   361      "(!!x. f(x)==transrec2(x,a,b))
```
```   362       ==> f(0) = a &
```
```   363           f(succ(i)) = b(i, f(i)) &
```
```   364           (Limit(K) \<longrightarrow> f(K) = (\<Union>j<K. f(j)))"
```
```   365 by (simp add: transrec2_Limit)
```
```   366
```
```   367
```
```   368 (** recursor -- better than nat_rec; the succ case has no type requirement! **)
```
```   369
```
```   370 (*NOT suitable for rewriting*)
```
```   371 lemmas recursor_lemma = recursor_def [THEN def_transrec, THEN trans]
```
```   372
```
```   373 lemma recursor_0: "recursor(a,b,0) = a"
```
```   374 by (rule nat_case_0 [THEN recursor_lemma])
```
```   375
```
```   376 lemma recursor_succ: "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))"
```
```   377 by (rule recursor_lemma, simp)
```
```   378
```
```   379
```
```   380 (** rec: old version for compatibility **)
```
```   381
```
```   382 lemma rec_0 [simp]: "rec(0,a,b) = a"
```
```   383 apply (unfold rec_def)
```
```   384 apply (rule recursor_0)
```
```   385 done
```
```   386
```
```   387 lemma rec_succ [simp]: "rec(succ(m),a,b) = b(m, rec(m,a,b))"
```
```   388 apply (unfold rec_def)
```
```   389 apply (rule recursor_succ)
```
```   390 done
```
```   391
```
```   392 lemma rec_type:
```
```   393     "[| n \<in> nat;
```
```   394         a \<in> C(0);
```
```   395         !!m z. [| m \<in> nat;  z \<in> C(m) |] ==> b(m,z): C(succ(m)) |]
```
```   396      ==> rec(n,a,b) \<in> C(n)"
```
```   397 by (erule nat_induct, auto)
```
```   398
```
```   399 end
```