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