src/ZF/Epsilon.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46953 2b6e55924af3
child 58860 fee7cfa69c50
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35762
af3ff2ba4c54 removed old CVS Ids;
wenzelm
parents: 26056
diff changeset
     1
(*  Title:      ZF/Epsilon.thy
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
13328
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     6
header{*Epsilon Induction and Recursion*}
703de709a64b better document preparation
paulson
parents: 13269
diff changeset
     7
26056
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents: 24893
diff changeset
     8
theory Epsilon imports Nat_ZF begin
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
     9
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    10
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    11
  eclose    :: "i=>i"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    12
    "eclose(A) == \<Union>n\<in>nat. nat_rec(n, A, %m r. \<Union>(r))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    14
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    15
  transrec  :: "[i, [i,i]=>i] =>i"  where
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)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    17
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    18
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    19
  rank      :: "i=>i"  where
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13524
diff changeset
    20
    "rank(a) == transrec(a, %x f. \<Union>y\<in>x. succ(f`y))"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1478
diff changeset
    21
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    22
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    23
  transrec2 :: "[i, i, [i,i]=>i] =>i"  where
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    24
    "transrec2(k, a, b) ==
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    25
       transrec(k,
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    26
                %i r. if(i=0, a,
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    27
                        if(\<exists>j. i=succ(j),
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    28
                           b(THE j. i=succ(j), r`(THE j. i=succ(j))),
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13524
diff changeset
    29
                           \<Union>j<i. r`j)))"
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1478
diff changeset
    30
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    31
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    32
  recursor  :: "[i, [i,i]=>i, i]=>i"  where
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    33
    "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
    34
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    35
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    36
  rec  :: "[i, i, [i,i]=>i]=>i"  where
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    37
    "rec(k,a,b) == recursor(a,b,k)"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    38
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    39
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
    40
subsection{*Basic Closure Properties*}
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    41
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    42
lemma arg_subset_eclose: "A \<subseteq> eclose(A)"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    43
apply (unfold eclose_def)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    44
apply (rule nat_rec_0 [THEN equalityD2, THEN subset_trans])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    45
apply (rule nat_0I [THEN UN_upper])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    46
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    47
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
    48
lemmas arg_into_eclose = arg_subset_eclose [THEN subsetD]
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    49
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    50
lemma Transset_eclose: "Transset(eclose(A))"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    51
apply (unfold eclose_def Transset_def)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    52
apply (rule subsetI [THEN ballI])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    53
apply (erule UN_E)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    54
apply (rule nat_succI [THEN UN_I], assumption)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    55
apply (erule nat_rec_succ [THEN ssubst])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    56
apply (erule UnionI, assumption)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    57
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    58
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    59
(* @{term"x \<in> eclose(A) ==> x \<subseteq> eclose(A)"} *)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    60
lemmas eclose_subset =
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
    61
       Transset_eclose [unfolded Transset_def, THEN bspec]
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    62
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    63
(* @{term"[| A \<in> eclose(B); c \<in> A |] ==> c \<in> eclose(B)"} *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
    64
lemmas ecloseD = eclose_subset [THEN subsetD]
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    65
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    66
lemmas arg_in_eclose_sing = arg_subset_eclose [THEN singleton_subsetD]
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
    67
lemmas arg_into_eclose_sing = arg_in_eclose_sing [THEN ecloseD]
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    68
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    69
(* This is epsilon-induction for eclose(A); see also eclose_induct_down...
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
    70
   [| a \<in> eclose(A);  !!x. [| x \<in> eclose(A); \<forall>y\<in>x. P(y) |] ==> P(x)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    71
   |] ==> P(a)
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    72
*)
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
    73
lemmas eclose_induct =
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
    74
     Transset_induct [OF _ Transset_eclose, induct set: eclose]
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
    75
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    76
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    77
(*Epsilon induction*)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    78
lemma eps_induct:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    79
    "[| !!x. \<forall>y\<in>x. P(y) ==> P(x) |]  ==>  P(a)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    80
by (rule arg_in_eclose_sing [THEN eclose_induct], blast)
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    81
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    82
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
    83
subsection{*Leastness of @{term eclose}*}
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    84
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    85
(** eclose(A) is the least transitive set including A as a subset. **)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    86
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    87
lemma eclose_least_lemma:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
    88
    "[| Transset(X);  A<=X;  n \<in> nat |] ==> nat_rec(n, A, %m r. \<Union>(r)) \<subseteq> X"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    89
apply (unfold Transset_def)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    90
apply (erule nat_induct)
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    91
apply (simp add: nat_rec_0)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    92
apply (simp add: nat_rec_succ, blast)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    93
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    94
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    95
lemma eclose_least:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
    96
     "[| Transset(X);  A<=X |] ==> eclose(A) \<subseteq> X"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    97
apply (unfold eclose_def)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    98
apply (rule eclose_least_lemma [THEN UN_least], assumption+)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
    99
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   100
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   101
(*COMPLETELY DIFFERENT induction principle from eclose_induct!!*)
13524
604d0f3622d6 *** empty log message ***
wenzelm
parents: 13387
diff changeset
   102
lemma eclose_induct_down [consumes 1]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   103
    "[| a \<in> eclose(b);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   104
        !!y.   [| y \<in> b |] ==> P(y);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   105
        !!y z. [| y \<in> eclose(b);  P(y);  z \<in> y |] ==> P(z)
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   106
     |] ==> P(a)"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   107
apply (rule eclose_least [THEN subsetD, THEN CollectD2, of "eclose(b)"])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   108
  prefer 3 apply assumption
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   109
 apply (unfold Transset_def)
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   110
 apply (blast intro: ecloseD)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   111
apply (blast intro: arg_subset_eclose [THEN subsetD])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   112
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   113
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   114
lemma Transset_eclose_eq_arg: "Transset(X) ==> eclose(X) = X"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   115
apply (erule equalityI [OF eclose_least arg_subset_eclose])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   116
apply (rule subset_refl)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   117
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   118
13387
b7464ca2ebbb new theorems to support Constructible proofs
paulson
parents: 13357
diff changeset
   119
text{*A transitive set either is empty or contains the empty set.*}
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   120
lemma Transset_0_lemma [rule_format]: "Transset(A) ==> x\<in>A \<longrightarrow> 0\<in>A";
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   121
apply (simp add: Transset_def)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   122
apply (rule_tac a=x in eps_induct, clarify)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   123
apply (drule bspec, assumption)
14153
76a6ba67bd15 new case_tac
paulson
parents: 13784
diff changeset
   124
apply (case_tac "x=0", auto)
13387
b7464ca2ebbb new theorems to support Constructible proofs
paulson
parents: 13357
diff changeset
   125
done
b7464ca2ebbb new theorems to support Constructible proofs
paulson
parents: 13357
diff changeset
   126
b7464ca2ebbb new theorems to support Constructible proofs
paulson
parents: 13357
diff changeset
   127
lemma Transset_0_disj: "Transset(A) ==> A=0 | 0\<in>A";
b7464ca2ebbb new theorems to support Constructible proofs
paulson
parents: 13357
diff changeset
   128
by (blast dest: Transset_0_lemma)
b7464ca2ebbb new theorems to support Constructible proofs
paulson
parents: 13357
diff changeset
   129
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   130
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   131
subsection{*Epsilon Recursion*}
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   132
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   133
(*Unused...*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   134
lemma mem_eclose_trans: "[| A \<in> eclose(B);  B \<in> eclose(C) |] ==> A \<in> eclose(C)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   135
by (rule eclose_least [OF Transset_eclose eclose_subset, THEN subsetD],
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   136
    assumption+)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   137
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   138
(*Variant of the previous lemma in a useable form for the sequel*)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   139
lemma mem_eclose_sing_trans:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   140
     "[| A \<in> eclose({B});  B \<in> eclose({C}) |] ==> A \<in> eclose({C})"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   141
by (rule eclose_least [OF Transset_eclose singleton_subsetI, THEN subsetD],
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   142
    assumption+)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   143
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   144
lemma under_Memrel: "[| Transset(i);  j \<in> i |] ==> Memrel(i)-``{j} = j"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   145
by (unfold Transset_def, blast)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   146
13217
bc5dc2392578 new theorems
paulson
parents: 13203
diff changeset
   147
lemma lt_Memrel: "j < i ==> Memrel(i) -`` {j} = j"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   148
by (simp add: lt_def Ord_def under_Memrel)
13217
bc5dc2392578 new theorems
paulson
parents: 13203
diff changeset
   149
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   150
(* @{term"j \<in> eclose(A) ==> Memrel(eclose(A)) -`` j = j"} *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 39159
diff changeset
   151
lemmas under_Memrel_eclose = Transset_eclose [THEN under_Memrel]
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   152
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   153
lemmas wfrec_ssubst = wf_Memrel [THEN wfrec, THEN ssubst]
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   154
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   155
lemma wfrec_eclose_eq:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   156
    "[| k \<in> eclose({j});  j \<in> eclose({i}) |] ==>
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   157
     wfrec(Memrel(eclose({i})), k, H) = wfrec(Memrel(eclose({j})), k, H)"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   158
apply (erule eclose_induct)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   159
apply (rule wfrec_ssubst)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   160
apply (rule wfrec_ssubst)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   161
apply (simp add: under_Memrel_eclose mem_eclose_sing_trans [of _ j i])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   162
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   163
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   164
lemma wfrec_eclose_eq2:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   165
    "k \<in> i ==> wfrec(Memrel(eclose({i})),k,H) = wfrec(Memrel(eclose({k})),k,H)"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   166
apply (rule arg_in_eclose_sing [THEN wfrec_eclose_eq])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   167
apply (erule arg_into_eclose_sing)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   168
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   169
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   170
lemma transrec: "transrec(a,H) = H(a, \<lambda>x\<in>a. transrec(x,H))"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   171
apply (unfold transrec_def)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   172
apply (rule wfrec_ssubst)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   173
apply (simp add: wfrec_eclose_eq2 arg_in_eclose_sing under_Memrel_eclose)
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
(*Avoids explosions in proofs; resolve it with a meta-level definition.*)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   177
lemma def_transrec:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   178
    "[| !!x. f(x)==transrec(x,H) |] ==> f(a) = H(a, \<lambda>x\<in>a. f(x))"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   179
apply simp
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   180
apply (rule transrec)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   181
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   182
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   183
lemma transrec_type:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   184
    "[| !!x u. [| x \<in> eclose({a});  u \<in> Pi(x,B) |] ==> H(x,u) \<in> B(x) |]
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   185
     ==> transrec(a,H) \<in> B(a)"
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13615
diff changeset
   186
apply (rule_tac i = a in arg_in_eclose_sing [THEN eclose_induct])
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   187
apply (subst transrec)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   188
apply (simp add: lam_type)
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   189
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   190
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   191
lemma eclose_sing_Ord: "Ord(i) ==> eclose({i}) \<subseteq> succ(i)"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   192
apply (erule Ord_is_Transset [THEN Transset_succ, THEN eclose_least])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   193
apply (rule succI1 [THEN singleton_subsetI])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   194
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   195
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   196
lemma succ_subset_eclose_sing: "succ(i) \<subseteq> eclose({i})"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   197
apply (insert arg_subset_eclose [of "{i}"], simp)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   198
apply (frule eclose_subset, blast)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13217
diff changeset
   199
done
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13217
diff changeset
   200
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13217
diff changeset
   201
lemma eclose_sing_Ord_eq: "Ord(i) ==> eclose({i}) = succ(i)"
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13217
diff changeset
   202
apply (rule equalityI)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   203
apply (erule eclose_sing_Ord)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   204
apply (rule succ_subset_eclose_sing)
13269
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13217
diff changeset
   205
done
3ba9be497c33 Tidying and introduction of various new theorems
paulson
parents: 13217
diff changeset
   206
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   207
lemma Ord_transrec_type:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   208
  assumes jini: "j \<in> i"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   209
      and ordi: "Ord(i)"
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   210
      and minor: " !!x u. [| x \<in> i;  u \<in> Pi(x,B) |] ==> H(x,u) \<in> B(x)"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   211
  shows "transrec(j,H) \<in> B(j)"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   212
apply (rule transrec_type)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   213
apply (insert jini ordi)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   214
apply (blast intro!: minor
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   215
             intro: Ord_trans
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   216
             dest: Ord_in_Ord [THEN eclose_sing_Ord, THEN subsetD])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   217
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   218
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   219
subsection{*Rank*}
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   220
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   221
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13524
diff changeset
   222
lemma rank: "rank(a) = (\<Union>y\<in>a. succ(rank(y)))"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   223
by (subst rank_def [THEN def_transrec], simp)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   224
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   225
lemma Ord_rank [simp]: "Ord(rank(a))"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   226
apply (rule_tac a=a in eps_induct)
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   227
apply (subst rank)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   228
apply (rule Ord_succ [THEN Ord_UN])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   229
apply (erule bspec, assumption)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   230
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   231
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   232
lemma rank_of_Ord: "Ord(i) ==> rank(i) = i"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   233
apply (erule trans_induct)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   234
apply (subst rank)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   235
apply (simp add: Ord_equality)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   236
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   237
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   238
lemma rank_lt: "a \<in> b ==> rank(a) < rank(b)"
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13615
diff changeset
   239
apply (rule_tac a1 = b in rank [THEN ssubst])
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   240
apply (erule UN_I [THEN ltI])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   241
apply (rule_tac [2] Ord_UN, auto)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   242
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   243
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   244
lemma eclose_rank_lt: "a \<in> eclose(b) ==> rank(a) < rank(b)"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   245
apply (erule eclose_induct_down)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   246
apply (erule rank_lt)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   247
apply (erule rank_lt [THEN lt_trans], assumption)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   248
done
6070
032babd0120b ZF: the natural numbers as a datatype
paulson
parents: 2469
diff changeset
   249
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   250
lemma rank_mono: "a<=b ==> rank(a) \<le> rank(b)"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   251
apply (rule subset_imp_le)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   252
apply (auto simp add: rank [of a] rank [of b])
13164
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_Pow: "rank(Pow(a)) = succ(rank(a))"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   256
apply (rule rank [THEN trans])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   257
apply (rule le_anti_sym)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   258
apply (rule_tac [2] UN_upper_le)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   259
apply (rule UN_least_le)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   260
apply (auto intro: rank_mono simp add: Ord_UN)
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_0 [simp]: "rank(0) = 0"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   264
by (rule rank [THEN trans], blast)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   265
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   266
lemma rank_succ [simp]: "rank(succ(x)) = succ(rank(x))"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   267
apply (rule rank [THEN trans])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   268
apply (rule equalityI [OF UN_least succI1 [THEN UN_upper]])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   269
apply (erule succE, blast)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   270
apply (erule rank_lt [THEN leI, THEN succ_leI, THEN le_imp_subset])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   271
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   272
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   273
lemma rank_Union: "rank(\<Union>(A)) = (\<Union>x\<in>A. rank(x))"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   274
apply (rule equalityI)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   275
apply (rule_tac [2] rank_mono [THEN le_imp_subset, THEN UN_least])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   276
apply (erule_tac [2] Union_upper)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   277
apply (subst rank)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   278
apply (rule UN_least)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   279
apply (erule UnionE)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   280
apply (rule subset_trans)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   281
apply (erule_tac [2] RepFunI [THEN Union_upper])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   282
apply (erule rank_lt [THEN succ_leI, THEN le_imp_subset])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   283
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   284
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   285
lemma rank_eclose: "rank(eclose(a)) = rank(a)"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   286
apply (rule le_anti_sym)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   287
apply (rule_tac [2] arg_subset_eclose [THEN rank_mono])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   288
apply (rule_tac a1 = "eclose (a) " in rank [THEN ssubst])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   289
apply (rule Ord_rank [THEN UN_least_le])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   290
apply (erule eclose_rank_lt [THEN succ_leI])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   291
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   292
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   293
lemma rank_pair1: "rank(a) < rank(<a,b>)"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   294
apply (unfold Pair_def)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   295
apply (rule consI1 [THEN rank_lt, THEN lt_trans])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   296
apply (rule consI1 [THEN consI2, THEN rank_lt])
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 rank_pair2: "rank(b) < rank(<a,b>)"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   300
apply (unfold Pair_def)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   301
apply (rule consI1 [THEN consI2, THEN rank_lt, THEN lt_trans])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   302
apply (rule consI1 [THEN consI2, THEN rank_lt])
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
(*Not clear how to remove the P(a) condition, since the "then" part
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   306
  must refer to "a"*)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   307
lemma the_equality_if:
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   308
     "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
   309
by (simp add: the_0 the_equality2)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   310
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   311
(*The first premise not only fixs i but ensures @{term"f\<noteq>0"}.
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   312
  The second premise is now essential.  Consider otherwise the relation
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   313
  r = {<0,0>,<0,1>,<0,2>,...}.  Then f`0 = \<Union>(f``{0}) = \<Union>(nat) = nat,
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13164
diff changeset
   314
  whose rank equals that of r.*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   315
lemma rank_apply: "[|i \<in> domain(f); function(f)|] ==> rank(f`i) < rank(f)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   316
apply clarify
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   317
apply (simp add: function_apply_equality)
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13164
diff changeset
   318
apply (blast intro: lt_trans rank_lt rank_pair2)
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   319
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   320
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   321
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13328
diff changeset
   322
subsection{*Corollaries of Leastness*}
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   323
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   324
lemma mem_eclose_subset: "A \<in> B ==> eclose(A)<=eclose(B)"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   325
apply (rule Transset_eclose [THEN eclose_least])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   326
apply (erule arg_into_eclose [THEN eclose_subset])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   327
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   328
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   329
lemma eclose_mono: "A<=B ==> eclose(A) \<subseteq> eclose(B)"
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   330
apply (rule Transset_eclose [THEN eclose_least])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   331
apply (erule subset_trans)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   332
apply (rule arg_subset_eclose)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   333
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   334
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   335
(** Idempotence of eclose **)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   336
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   337
lemma eclose_idem: "eclose(eclose(A)) = eclose(A)"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   338
apply (rule equalityI)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   339
apply (rule eclose_least [OF Transset_eclose subset_refl])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   340
apply (rule arg_subset_eclose)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   341
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   342
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   343
(** Transfinite recursion for definitions based on the
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   344
    three cases of ordinals **)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   345
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   346
lemma transrec2_0 [simp]: "transrec2(0,a,b) = a"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   347
by (rule transrec2_def [THEN def_transrec, THEN trans], simp)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   348
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   349
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
   350
apply (rule transrec2_def [THEN def_transrec, THEN trans])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   351
apply (simp add: the_equality if_P)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   352
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   353
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   354
lemma transrec2_Limit:
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13524
diff changeset
   355
     "Limit(i) ==> transrec2(i,a,b) = (\<Union>j<i. transrec2(j,a,b))"
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13164
diff changeset
   356
apply (rule transrec2_def [THEN def_transrec, THEN trans])
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   357
apply (auto simp add: OUnion_def)
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   358
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   359
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   360
lemma def_transrec2:
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   361
     "(!!x. f(x)==transrec2(x,a,b))
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   362
      ==> f(0) = a &
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   363
          f(succ(i)) = b(i, f(i)) &
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   364
          (Limit(K) \<longrightarrow> f(K) = (\<Union>j<K. f(j)))"
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   365
by (simp add: transrec2_Limit)
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   366
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   367
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   368
(** recursor -- better than nat_rec; the succ case has no type requirement! **)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   369
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   370
(*NOT suitable for rewriting*)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   371
lemmas recursor_lemma = recursor_def [THEN def_transrec, THEN trans]
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   372
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   373
lemma recursor_0: "recursor(a,b,0) = a"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   374
by (rule nat_case_0 [THEN recursor_lemma])
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   375
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   376
lemma recursor_succ: "recursor(a,b,succ(m)) = b(m, recursor(a,b,m))"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   377
by (rule recursor_lemma, simp)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   378
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   379
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   380
(** rec: old version for compatibility **)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   381
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   382
lemma rec_0 [simp]: "rec(0,a,b) = a"
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   383
apply (unfold rec_def)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   384
apply (rule recursor_0)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   385
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   386
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   387
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
   388
apply (unfold rec_def)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   389
apply (rule recursor_succ)
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   390
done
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   391
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   392
lemma rec_type:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   393
    "[| n \<in> nat;
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   394
        a \<in> C(0);
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46820
diff changeset
   395
        !!m z. [| m \<in> nat;  z \<in> C(m) |] ==> b(m,z): C(succ(m)) |]
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 46751
diff changeset
   396
     ==> rec(n,a,b) \<in> C(n)"
13185
da61bfa0a391 deleted some useless ML bindings
paulson
parents: 13175
diff changeset
   397
by (erule nat_induct, auto)
13164
dfc399c684e4 converted Epsilon to Isar
paulson
parents: 6070
diff changeset
   398
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   399
end