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