src/ZF/Constructible/AC_in_L.thy
author paulson
Tue Oct 01 13:26:10 2002 +0200 (2002-10-01)
changeset 13615 449a70d88b38
parent 13546 f76237c2be75
child 13634 99a593b49b04
permissions -rw-r--r--
Numerous cosmetic changes, prompted by the new simplifier
paulson@13543
     1
(*  Title:      ZF/Constructible/AC_in_L.thy
paulson@13543
     2
    ID: $Id$
paulson@13543
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13543
     4
    Copyright   2002  University of Cambridge
paulson@13543
     5
*)
paulson@13543
     6
paulson@13543
     7
header {* The Axiom of Choice Holds in L! *}
paulson@13543
     8
paulson@13543
     9
theory AC_in_L = Formula:
paulson@13543
    10
paulson@13543
    11
subsection{*Extending a Wellordering over a List -- Lexicographic Power*}
paulson@13543
    12
paulson@13543
    13
text{*This could be moved into a library.*}
paulson@13543
    14
paulson@13543
    15
consts
paulson@13543
    16
  rlist   :: "[i,i]=>i"
paulson@13543
    17
paulson@13543
    18
inductive
paulson@13543
    19
  domains "rlist(A,r)" \<subseteq> "list(A) * list(A)"
paulson@13543
    20
  intros
paulson@13543
    21
    shorterI:
paulson@13543
    22
      "[| length(l') < length(l); l' \<in> list(A); l \<in> list(A) |] 
paulson@13543
    23
       ==> <l', l> \<in> rlist(A,r)"
paulson@13543
    24
paulson@13543
    25
    sameI:
paulson@13543
    26
      "[| <l',l> \<in> rlist(A,r); a \<in> A |] 
paulson@13543
    27
       ==> <Cons(a,l'), Cons(a,l)> \<in> rlist(A,r)"
paulson@13543
    28
paulson@13543
    29
    diffI:
paulson@13543
    30
      "[| length(l') = length(l); <a',a> \<in> r; 
paulson@13543
    31
          l' \<in> list(A); l \<in> list(A); a' \<in> A; a \<in> A |] 
paulson@13543
    32
       ==> <Cons(a',l'), Cons(a,l)> \<in> rlist(A,r)"
paulson@13543
    33
  type_intros list.intros
paulson@13543
    34
paulson@13543
    35
paulson@13543
    36
subsubsection{*Type checking*}
paulson@13543
    37
paulson@13543
    38
lemmas rlist_type = rlist.dom_subset
paulson@13543
    39
paulson@13543
    40
lemmas field_rlist = rlist_type [THEN field_rel_subset]
paulson@13543
    41
paulson@13543
    42
subsubsection{*Linearity*}
paulson@13543
    43
paulson@13543
    44
lemma rlist_Nil_Cons [intro]:
paulson@13543
    45
    "[|a \<in> A; l \<in> list(A)|] ==> <[], Cons(a,l)> \<in> rlist(A, r)"
paulson@13543
    46
by (simp add: shorterI) 
paulson@13543
    47
paulson@13543
    48
lemma linear_rlist:
paulson@13543
    49
    "linear(A,r) ==> linear(list(A),rlist(A,r))"
paulson@13543
    50
apply (simp (no_asm_simp) add: linear_def)
paulson@13543
    51
apply (rule ballI)  
paulson@13543
    52
apply (induct_tac x) 
paulson@13543
    53
 apply (rule ballI)  
paulson@13543
    54
 apply (induct_tac y)  
paulson@13543
    55
  apply (simp_all add: shorterI) 
paulson@13543
    56
apply (rule ballI)  
paulson@13543
    57
apply (erule_tac a=y in list.cases) 
paulson@13543
    58
 apply (rename_tac [2] a2 l2) 
paulson@13543
    59
 apply (rule_tac [2] i = "length(l)" and j = "length(l2)" in Ord_linear_lt)
paulson@13543
    60
     apply (simp_all add: shorterI) 
paulson@13543
    61
apply (erule_tac x=a and y=a2 in linearE) 
paulson@13543
    62
    apply (simp_all add: diffI) 
paulson@13543
    63
apply (blast intro: sameI) 
paulson@13543
    64
done
paulson@13543
    65
paulson@13543
    66
paulson@13543
    67
subsubsection{*Well-foundedness*}
paulson@13543
    68
paulson@13543
    69
text{*Nothing preceeds Nil in this ordering.*}
paulson@13543
    70
inductive_cases rlist_NilE: " <l,[]> \<in> rlist(A,r)"
paulson@13543
    71
paulson@13543
    72
inductive_cases rlist_ConsE: " <l', Cons(x,l)> \<in> rlist(A,r)"
paulson@13543
    73
paulson@13543
    74
lemma not_rlist_Nil [simp]: " <l,[]> \<notin> rlist(A,r)"
paulson@13543
    75
by (blast intro: elim: rlist_NilE)
paulson@13543
    76
paulson@13543
    77
lemma rlist_imp_length_le: "<l',l> \<in> rlist(A,r) ==> length(l') \<le> length(l)"
paulson@13543
    78
apply (erule rlist.induct)
paulson@13543
    79
apply (simp_all add: leI)  
paulson@13543
    80
done
paulson@13543
    81
paulson@13543
    82
lemma wf_on_rlist_n:
paulson@13543
    83
  "[| n \<in> nat; wf[A](r) |] ==> wf[{l \<in> list(A). length(l) = n}](rlist(A,r))"
paulson@13543
    84
apply (induct_tac n) 
paulson@13543
    85
 apply (rule wf_onI2, simp) 
paulson@13543
    86
apply (rule wf_onI2, clarify) 
paulson@13543
    87
apply (erule_tac a=y in list.cases, clarify) 
paulson@13543
    88
 apply (simp (no_asm_use))
paulson@13543
    89
apply clarify 
paulson@13543
    90
apply (simp (no_asm_use))
paulson@13543
    91
apply (subgoal_tac "\<forall>l2 \<in> list(A). length(l2) = x --> Cons(a,l2) \<in> B", blast)
paulson@13543
    92
apply (erule_tac a=a in wf_on_induct, assumption)
paulson@13543
    93
apply (rule ballI)
paulson@13543
    94
apply (rule impI) 
paulson@13543
    95
apply (erule_tac a=l2 in wf_on_induct, blast, clarify)
paulson@13543
    96
apply (rename_tac a' l2 l') 
paulson@13543
    97
apply (drule_tac x="Cons(a',l')" in bspec, typecheck) 
paulson@13543
    98
apply simp 
paulson@13543
    99
apply (erule mp, clarify) 
paulson@13543
   100
apply (erule rlist_ConsE, auto)
paulson@13543
   101
done
paulson@13543
   102
paulson@13543
   103
lemma list_eq_UN_length: "list(A) = (\<Union>n\<in>nat. {l \<in> list(A). length(l) = n})"
paulson@13543
   104
by (blast intro: length_type)
paulson@13543
   105
paulson@13543
   106
paulson@13543
   107
lemma wf_on_rlist: "wf[A](r) ==> wf[list(A)](rlist(A,r))"
paulson@13543
   108
apply (subst list_eq_UN_length) 
paulson@13543
   109
apply (rule wf_on_Union) 
paulson@13543
   110
  apply (rule wf_imp_wf_on [OF wf_Memrel [of nat]])
paulson@13543
   111
 apply (simp add: wf_on_rlist_n)
paulson@13543
   112
apply (frule rlist_type [THEN subsetD]) 
paulson@13543
   113
apply (simp add: length_type)   
paulson@13543
   114
apply (drule rlist_imp_length_le)
paulson@13543
   115
apply (erule leE) 
paulson@13543
   116
apply (simp_all add: lt_def) 
paulson@13543
   117
done
paulson@13543
   118
paulson@13543
   119
paulson@13543
   120
lemma wf_rlist: "wf(r) ==> wf(rlist(field(r),r))"
paulson@13543
   121
apply (simp add: wf_iff_wf_on_field)
paulson@13543
   122
apply (rule wf_on_subset_A [OF _ field_rlist])
paulson@13543
   123
apply (blast intro: wf_on_rlist) 
paulson@13543
   124
done
paulson@13543
   125
paulson@13543
   126
lemma well_ord_rlist:
paulson@13543
   127
     "well_ord(A,r) ==> well_ord(list(A), rlist(A,r))"
paulson@13543
   128
apply (rule well_ordI)
paulson@13543
   129
apply (simp add: well_ord_def wf_on_rlist)
paulson@13543
   130
apply (simp add: well_ord_def tot_ord_def linear_rlist)
paulson@13543
   131
done
paulson@13543
   132
paulson@13543
   133
paulson@13543
   134
subsection{*An Injection from Formulas into the Natural Numbers*}
paulson@13543
   135
paulson@13543
   136
text{*There is a well-known bijection between @{term "nat*nat"} and @{term
paulson@13543
   137
nat} given by the expression f(m,n) = triangle(m+n) + m, where triangle(k)
paulson@13543
   138
enumerates the triangular numbers and can be defined by triangle(0)=0,
paulson@13543
   139
triangle(succ(k)) = succ(k + triangle(k)).  Some small amount of effort is
paulson@13543
   140
needed to show that f is a bijection.  We already know (by the theorem @{text
paulson@13543
   141
InfCard_square_eqpoll}) that such a bijection exists, but as we have no direct
paulson@13543
   142
way to refer to it, we must use a locale.*}
paulson@13543
   143
paulson@13543
   144
text{*Locale for any arbitrary injection between @{term "nat*nat"} 
paulson@13543
   145
      and @{term nat}*}
paulson@13543
   146
locale Nat_Times_Nat =
paulson@13543
   147
  fixes fn
paulson@13543
   148
  assumes fn_inj: "fn \<in> inj(nat*nat, nat)"
paulson@13543
   149
paulson@13543
   150
paulson@13543
   151
consts   enum :: "[i,i]=>i"
paulson@13543
   152
primrec
paulson@13543
   153
  "enum(f, Member(x,y)) = f ` <0, f ` <x,y>>"
paulson@13543
   154
  "enum(f, Equal(x,y)) = f ` <1, f ` <x,y>>"
paulson@13543
   155
  "enum(f, Nand(p,q)) = f ` <2, f ` <enum(f,p), enum(f,q)>>"
paulson@13543
   156
  "enum(f, Forall(p)) = f ` <succ(2), enum(f,p)>"
paulson@13543
   157
paulson@13543
   158
lemma (in Nat_Times_Nat) fn_type [TC,simp]:
paulson@13543
   159
    "[|x \<in> nat; y \<in> nat|] ==> fn`<x,y> \<in> nat"
paulson@13543
   160
by (blast intro: inj_is_fun [OF fn_inj] apply_funtype) 
paulson@13543
   161
paulson@13543
   162
lemma (in Nat_Times_Nat) fn_iff:
paulson@13543
   163
    "[|x \<in> nat; y \<in> nat; u \<in> nat; v \<in> nat|] 
paulson@13543
   164
     ==> (fn`<x,y> = fn`<u,v>) <-> (x=u & y=v)"
paulson@13543
   165
by (blast dest: inj_apply_equality [OF fn_inj]) 
paulson@13543
   166
paulson@13543
   167
lemma (in Nat_Times_Nat) enum_type [TC,simp]:
paulson@13543
   168
    "p \<in> formula ==> enum(fn,p) \<in> nat"
paulson@13543
   169
by (induct_tac p, simp_all) 
paulson@13543
   170
paulson@13543
   171
lemma (in Nat_Times_Nat) enum_inject [rule_format]:
paulson@13543
   172
    "p \<in> formula ==> \<forall>q\<in>formula. enum(fn,p) = enum(fn,q) --> p=q"
paulson@13543
   173
apply (induct_tac p, simp_all) 
paulson@13543
   174
   apply (rule ballI) 
paulson@13543
   175
   apply (erule formula.cases) 
paulson@13543
   176
   apply (simp_all add: fn_iff) 
paulson@13543
   177
  apply (rule ballI) 
paulson@13543
   178
  apply (erule formula.cases) 
paulson@13543
   179
  apply (simp_all add: fn_iff) 
paulson@13543
   180
 apply (rule ballI) 
paulson@13543
   181
 apply (erule_tac a=qa in formula.cases) 
paulson@13543
   182
 apply (simp_all add: fn_iff) 
paulson@13543
   183
 apply blast 
paulson@13543
   184
apply (rule ballI) 
paulson@13543
   185
apply (erule_tac a=q in formula.cases) 
paulson@13543
   186
apply (simp_all add: fn_iff, blast) 
paulson@13543
   187
done
paulson@13543
   188
paulson@13543
   189
lemma (in Nat_Times_Nat) inj_formula_nat:
paulson@13543
   190
    "(\<lambda>p \<in> formula. enum(fn,p)) \<in> inj(formula, nat)"
paulson@13543
   191
apply (simp add: inj_def lam_type) 
paulson@13543
   192
apply (blast intro: enum_inject) 
paulson@13543
   193
done
paulson@13543
   194
paulson@13543
   195
lemma (in Nat_Times_Nat) well_ord_formula:
paulson@13543
   196
    "well_ord(formula, measure(formula, enum(fn)))"
paulson@13543
   197
apply (rule well_ord_measure, simp)
paulson@13543
   198
apply (blast intro: enum_inject)   
paulson@13543
   199
done
paulson@13543
   200
paulson@13543
   201
lemmas nat_times_nat_lepoll_nat =
paulson@13543
   202
    InfCard_nat [THEN InfCard_square_eqpoll, THEN eqpoll_imp_lepoll]
paulson@13543
   203
paulson@13543
   204
paulson@13543
   205
text{*Not needed--but interesting?*}
paulson@13543
   206
theorem formula_lepoll_nat: "formula \<lesssim> nat"
paulson@13543
   207
apply (insert nat_times_nat_lepoll_nat)
paulson@13543
   208
apply (unfold lepoll_def)
paulson@13543
   209
apply (blast intro: exI Nat_Times_Nat.inj_formula_nat Nat_Times_Nat.intro)
paulson@13543
   210
done
paulson@13543
   211
paulson@13543
   212
paulson@13543
   213
subsection{*Limit Construction for Well-Orderings*}
paulson@13543
   214
paulson@13543
   215
text{*Now we work towards the transfinite definition of wellorderings for
paulson@13543
   216
@{term "Lset(i)"}.  We assume as an inductive hypothesis that there is a family
paulson@13543
   217
of wellorderings for smaller ordinals.*}
paulson@13543
   218
paulson@13543
   219
text{*This constant denotes the set of elements introduced at level
paulson@13543
   220
@{term "succ(i)"}*}
paulson@13543
   221
constdefs
paulson@13543
   222
  Lset_new :: "i=>i"
paulson@13543
   223
    "Lset_new(i) == {x \<in> Lset(succ(i)). lrank(x) = i}"
paulson@13543
   224
paulson@13543
   225
lemma Lset_new_iff_lrank_eq:
paulson@13543
   226
     "Ord(i) ==> x \<in> Lset_new(i) <-> L(x) & lrank(x) = i"
paulson@13543
   227
by (auto simp add: Lset_new_def Lset_iff_lrank_lt) 
paulson@13543
   228
paulson@13543
   229
lemma Lset_new_eq:
paulson@13543
   230
     "Ord(i) ==> Lset_new(i) = Lset(succ(i)) - Lset(i)"
paulson@13543
   231
apply (rule equality_iffI)
paulson@13543
   232
apply (simp add: Lset_new_iff_lrank_eq Lset_iff_lrank_lt, auto) 
paulson@13543
   233
apply (blast elim: leE) 
paulson@13543
   234
done
paulson@13543
   235
paulson@13543
   236
lemma Limit_Lset_eq2:
paulson@13543
   237
    "Limit(i) ==> Lset(i) = (\<Union>j\<in>i. Lset_new(j))"
paulson@13543
   238
apply (simp add: Limit_Lset_eq) 
paulson@13543
   239
apply (rule equalityI)
paulson@13543
   240
 apply safe
paulson@13543
   241
 apply (subgoal_tac "Ord(y)")
paulson@13543
   242
  prefer 2 apply (blast intro: Ord_in_Ord Limit_is_Ord)
paulson@13543
   243
 apply (simp_all add: Limit_is_Ord Lset_iff_lrank_lt Lset_new_def 
paulson@13543
   244
                      Ord_mem_iff_lt) 
paulson@13543
   245
 apply (blast intro: lt_trans) 
paulson@13543
   246
apply (rule_tac x = "succ(lrank(x))" in bexI)
paulson@13543
   247
 apply (simp add: Lset_succ_lrank_iff) 
paulson@13543
   248
apply (blast intro: Limit_has_succ ltD) 
paulson@13543
   249
done
paulson@13543
   250
paulson@13543
   251
text{*This constant expresses the wellordering at limit ordinals.*}
paulson@13543
   252
constdefs
paulson@13543
   253
  rlimit :: "[i,i=>i]=>i"
paulson@13543
   254
    "rlimit(i,r) == 
paulson@13543
   255
       {z: Lset(i) * Lset(i).
paulson@13543
   256
        \<exists>x' x. z = <x',x> &         
paulson@13543
   257
               (lrank(x') < lrank(x) | 
paulson@13543
   258
                (lrank(x') = lrank(x) & <x',x> \<in> r(succ(lrank(x)))))}"
paulson@13543
   259
paulson@13543
   260
lemma rlimit_eqI:
paulson@13543
   261
     "[|Limit(i); \<forall>j<i. r'(j) = r(j)|] ==> rlimit(i,r) = rlimit(i,r')"
paulson@13543
   262
apply (simp add: rlimit_def) 
paulson@13543
   263
apply (rule refl iff_refl Collect_cong ex_cong conj_cong)+
paulson@13543
   264
apply (simp add: Limit_is_Ord Lset_lrank_lt)  
paulson@13543
   265
done
paulson@13543
   266
paulson@13543
   267
lemma wf_on_Lset:
paulson@13543
   268
    "wf[Lset(succ(j))](r(succ(j))) ==> wf[Lset_new(j)](rlimit(i,r))"
paulson@13543
   269
apply (simp add: wf_on_def Lset_new_def) 
paulson@13543
   270
apply (erule wf_subset) 
paulson@13543
   271
apply (force simp add: rlimit_def) 
paulson@13543
   272
done
paulson@13543
   273
paulson@13543
   274
lemma wf_on_rlimit:
paulson@13543
   275
    "[|Limit(i); \<forall>j<i. wf[Lset(j)](r(j)) |] ==> wf[Lset(i)](rlimit(i,r))"
paulson@13543
   276
apply (simp add: Limit_Lset_eq2)
paulson@13543
   277
apply (rule wf_on_Union)
paulson@13543
   278
  apply (rule wf_imp_wf_on [OF wf_Memrel [of i]]) 
paulson@13543
   279
 apply (blast intro: wf_on_Lset Limit_has_succ Limit_is_Ord ltI) 
paulson@13543
   280
apply (force simp add: rlimit_def Limit_is_Ord Lset_iff_lrank_lt Lset_new_def
paulson@13543
   281
                       Ord_mem_iff_lt)
paulson@13543
   282
paulson@13543
   283
done
paulson@13543
   284
paulson@13543
   285
lemma linear_rlimit:
paulson@13543
   286
    "[|Limit(i); \<forall>j<i. linear(Lset(j), r(j)) |]
paulson@13543
   287
     ==> linear(Lset(i), rlimit(i,r))"
paulson@13543
   288
apply (frule Limit_is_Ord) 
paulson@13543
   289
apply (simp add: Limit_Lset_eq2)
paulson@13543
   290
apply (simp add: linear_def Lset_new_def rlimit_def Ball_def) 
paulson@13543
   291
apply (simp add: lt_Ord Lset_iff_lrank_lt) 
paulson@13543
   292
apply (simp add: ltI, clarify) 
paulson@13543
   293
apply (rename_tac u v) 
paulson@13543
   294
apply (rule_tac i="lrank(u)" and j="lrank(v)" in Ord_linear_lt) 
paulson@13543
   295
apply simp_all
paulson@13543
   296
apply (drule_tac x="succ(lrank(u) Un lrank(v))" in ospec) 
paulson@13543
   297
apply (simp add: ltI)
paulson@13543
   298
apply (drule_tac x=u in spec, simp) 
paulson@13543
   299
apply (drule_tac x=v in spec, simp) 
paulson@13543
   300
done
paulson@13543
   301
paulson@13543
   302
paulson@13543
   303
lemma well_ord_rlimit:
paulson@13543
   304
    "[|Limit(i); \<forall>j<i. well_ord(Lset(j), r(j)) |]
paulson@13543
   305
     ==> well_ord(Lset(i), rlimit(i,r))"
paulson@13543
   306
by (blast intro: well_ordI wf_on_rlimit well_ord_is_wf 
paulson@13543
   307
                           linear_rlimit well_ord_is_linear) 
paulson@13543
   308
paulson@13543
   309
paulson@13543
   310
subsection{*Defining the Wellordering on @{term "Lset(succ(i))"}*}
paulson@13543
   311
paulson@13543
   312
text{*We introduce wellorderings for environments, which are lists built over
paulson@13543
   313
@{term "Lset(succ(i))"}.  We combine it with the enumeration of formulas.  The
paulson@13543
   314
order type of the resulting wellordering gives us a map from (environment,
paulson@13543
   315
formula) pairs into the ordinals.  For each member of @{term "DPow(Lset(i))"},
paulson@13543
   316
we take the minimum such ordinal.  This yields a wellordering of
paulson@13543
   317
@{term "DPow(Lset(i))"}, which we then extend to @{term "Lset(succ(i))"}*}
paulson@13543
   318
paulson@13543
   319
constdefs
paulson@13543
   320
  env_form_r :: "[i,i,i]=>i"
paulson@13543
   321
    --{*wellordering on (environment, formula) pairs*}
paulson@13543
   322
   "env_form_r(f,r,i) ==
paulson@13543
   323
      rmult(list(Lset(i)), rlist(Lset(i), r),
paulson@13543
   324
	    formula, measure(formula, enum(f)))"
paulson@13543
   325
paulson@13543
   326
  env_form_map :: "[i,i,i,i]=>i"
paulson@13543
   327
    --{*map from (environment, formula) pairs to ordinals*}
paulson@13543
   328
   "env_form_map(f,r,i,z) 
paulson@13543
   329
      == ordermap(list(Lset(i)) * formula, env_form_r(f,r,i)) ` z"
paulson@13543
   330
paulson@13543
   331
  L_new_ord :: "[i,i,i,i,i]=>o"
paulson@13543
   332
    --{*predicate that holds if @{term k} is a valid index for @{term X}*}
paulson@13543
   333
   "L_new_ord(f,r,i,X,k) ==  
paulson@13543
   334
           \<exists>env \<in> list(Lset(i)). \<exists>p \<in> formula. 
paulson@13543
   335
             arity(p) \<le> succ(length(env)) & 
paulson@13543
   336
             X = {x\<in>Lset(i). sats(Lset(i), p, Cons(x,env))} &
paulson@13543
   337
             env_form_map(f,r,i,<env,p>) = k"
paulson@13543
   338
paulson@13543
   339
  L_new_least :: "[i,i,i,i]=>i"
paulson@13543
   340
    --{*function yielding the smallest index for @{term X}*}
paulson@13543
   341
   "L_new_least(f,r,i,X) == \<mu>k. L_new_ord(f,r,i,X,k)"
paulson@13543
   342
paulson@13543
   343
  L_new_r :: "[i,i,i]=>i"
paulson@13543
   344
    --{*a wellordering on @{term "DPow(Lset(i))"}*}
paulson@13543
   345
   "L_new_r(f,r,i) == measure(Lset_new(i), L_new_least(f,r,i))"
paulson@13543
   346
paulson@13543
   347
  L_succ_r :: "[i,i,i]=>i"
paulson@13543
   348
    --{*a wellordering on @{term "Lset(succ(i))"}*}
paulson@13543
   349
   "L_succ_r(f,r,i) == (L_new_r(f,r,i) Un (Lset(i) * Lset_new(i))) Un r"
paulson@13543
   350
paulson@13543
   351
paulson@13543
   352
lemma (in Nat_Times_Nat) well_ord_env_form_r:
paulson@13543
   353
    "well_ord(Lset(i), r) 
paulson@13543
   354
     ==> well_ord(list(Lset(i)) * formula, env_form_r(fn,r,i))"
paulson@13543
   355
by (simp add: env_form_r_def well_ord_rmult well_ord_rlist well_ord_formula) 
paulson@13543
   356
paulson@13543
   357
lemma (in Nat_Times_Nat) Ord_env_form_map:
paulson@13543
   358
    "[|well_ord(Lset(i), r); z \<in> list(Lset(i)) * formula|]
paulson@13543
   359
     ==> Ord(env_form_map(fn,r,i,z))"
paulson@13543
   360
by (simp add: env_form_map_def Ord_ordermap well_ord_env_form_r) 
paulson@13543
   361
paulson@13543
   362
paulson@13543
   363
lemma DPow_imp_ex_L_new_ord:
paulson@13543
   364
    "X \<in> DPow(Lset(i)) ==> \<exists>k. L_new_ord(fn,r,i,X,k)"
paulson@13543
   365
apply (simp add: L_new_ord_def) 
paulson@13543
   366
apply (blast dest!: DPowD) 
paulson@13543
   367
done
paulson@13543
   368
paulson@13543
   369
lemma (in Nat_Times_Nat) L_new_ord_imp_Ord:
paulson@13543
   370
     "[|L_new_ord(fn,r,i,X,k); well_ord(Lset(i), r)|] ==> Ord(k)"
paulson@13543
   371
apply (simp add: L_new_ord_def, clarify)
paulson@13543
   372
apply (simp add: Ord_env_form_map)  
paulson@13543
   373
done
paulson@13543
   374
paulson@13543
   375
lemma (in Nat_Times_Nat) DPow_imp_L_new_least:
paulson@13543
   376
    "[|X \<in> DPow(Lset(i)); well_ord(Lset(i), r)|] 
paulson@13543
   377
     ==> L_new_ord(fn, r, i, X, L_new_least(fn,r,i,X))"
paulson@13543
   378
apply (simp add: L_new_least_def)
paulson@13543
   379
apply (blast dest!: DPow_imp_ex_L_new_ord intro: L_new_ord_imp_Ord LeastI)  
paulson@13543
   380
done
paulson@13543
   381
paulson@13543
   382
lemma (in Nat_Times_Nat) env_form_map_inject:
paulson@13543
   383
    "[|env_form_map(fn,r,i,u) = env_form_map(fn,r,i,v); well_ord(Lset(i), r);  
paulson@13543
   384
       u \<in> list(Lset(i)) * formula;  v \<in> list(Lset(i)) * formula|] 
paulson@13543
   385
     ==> u=v"
paulson@13543
   386
apply (simp add: env_form_map_def) 
paulson@13543
   387
apply (rule inj_apply_equality [OF bij_is_inj, OF ordermap_bij, 
paulson@13543
   388
                                OF well_ord_env_form_r], assumption+)
paulson@13543
   389
done
paulson@13543
   390
paulson@13543
   391
paulson@13543
   392
lemma (in Nat_Times_Nat) L_new_ord_unique:
paulson@13543
   393
    "[|L_new_ord(fn,r,i,X,k); L_new_ord(fn,r,i,Y,k); well_ord(Lset(i), r)|] 
paulson@13543
   394
     ==> X=Y"
paulson@13543
   395
apply (simp add: L_new_ord_def, clarify)
paulson@13543
   396
apply (drule env_form_map_inject, auto) 
paulson@13543
   397
done
paulson@13543
   398
paulson@13543
   399
lemma (in Nat_Times_Nat) well_ord_L_new_r:
paulson@13543
   400
    "[|Ord(i); well_ord(Lset(i), r)|]
paulson@13543
   401
     ==> well_ord(Lset_new(i), L_new_r(fn,r,i))"
paulson@13543
   402
apply (simp add: L_new_r_def) 
paulson@13543
   403
apply (rule well_ord_measure) 
paulson@13543
   404
 apply (simp add: L_new_least_def Ord_Least)
paulson@13543
   405
apply (simp add: Lset_new_eq Lset_succ, clarify) 
paulson@13543
   406
apply (drule DPow_imp_L_new_least, assumption)+
paulson@13543
   407
apply simp 
paulson@13543
   408
apply (blast intro: L_new_ord_unique) 
paulson@13543
   409
done
paulson@13543
   410
paulson@13543
   411
lemma L_new_r_subset: "L_new_r(f,r,i) <= Lset_new(i) * Lset_new(i)"
paulson@13543
   412
by (simp add: L_new_r_def measure_type)
paulson@13543
   413
paulson@13543
   414
lemma Lset_Lset_new_disjoint: "Ord(i) ==> Lset(i) \<inter> Lset_new(i) = 0"
paulson@13543
   415
by (simp add: Lset_new_eq, blast)
paulson@13543
   416
paulson@13543
   417
lemma (in Nat_Times_Nat) linear_L_succ_r:
paulson@13543
   418
    "[|Ord(i); well_ord(Lset(i), r)|]
paulson@13543
   419
     ==> linear(Lset(succ(i)), L_succ_r(fn, r, i))"
paulson@13543
   420
apply (frule well_ord_L_new_r, assumption) 
paulson@13543
   421
apply (drule well_ord_is_linear)+
paulson@13543
   422
apply (simp add: linear_def L_succ_r_def Lset_new_eq, auto) 
paulson@13543
   423
done
paulson@13543
   424
paulson@13543
   425
paulson@13543
   426
lemma (in Nat_Times_Nat) wf_L_new_r:
paulson@13543
   427
    "[|Ord(i); well_ord(Lset(i), r)|] ==> wf(L_new_r(fn,r,i))"
paulson@13543
   428
apply (rule well_ord_L_new_r [THEN well_ord_is_wf, THEN wf_on_imp_wf], 
paulson@13543
   429
       assumption+)
paulson@13543
   430
apply (rule L_new_r_subset)
paulson@13543
   431
done
paulson@13543
   432
paulson@13543
   433
paulson@13546
   434
lemma (in Nat_Times_Nat) well_ord_L_succ_r:
paulson@13543
   435
    "[|Ord(i); well_ord(Lset(i), r); r \<subseteq> Lset(i) * Lset(i)|]
paulson@13543
   436
     ==> well_ord(Lset(succ(i)), L_succ_r(fn,r,i))"
paulson@13543
   437
apply (rule well_ordI [OF wf_imp_wf_on])
paulson@13543
   438
 prefer 2 apply (blast intro: linear_L_succ_r) 
paulson@13543
   439
apply (simp add: L_succ_r_def)
paulson@13543
   440
apply (rule wf_Un)
paulson@13543
   441
  apply (cut_tac L_new_r_subset [of fn r i], simp add: Lset_new_eq, blast)
paulson@13543
   442
 apply (rule wf_Un)  
paulson@13543
   443
   apply (cut_tac L_new_r_subset [of fn r i], simp add: Lset_new_eq, blast)
paulson@13543
   444
  apply (blast intro: wf_L_new_r) 
paulson@13543
   445
 apply (simp add: wf_times Lset_Lset_new_disjoint)
paulson@13543
   446
apply (blast intro: well_ord_is_wf wf_on_imp_wf)
paulson@13543
   447
done
paulson@13543
   448
paulson@13543
   449
paulson@13543
   450
lemma (in Nat_Times_Nat) L_succ_r_type:
paulson@13543
   451
    "[|Ord(i); r \<subseteq> Lset(i) * Lset(i)|]
paulson@13543
   452
     ==> L_succ_r(fn,r,i) \<subseteq> Lset(succ(i)) * Lset(succ(i))"
paulson@13543
   453
apply (simp add: L_succ_r_def L_new_r_def measure_def Lset_new_eq) 
paulson@13543
   454
apply (blast intro: Lset_mono_mem [OF succI1, THEN subsetD] ) 
paulson@13543
   455
done				   
paulson@13543
   456
paulson@13543
   457
paulson@13543
   458
subsection{*Transfinite Definition of the Wellordering on @{term "L"}*}
paulson@13543
   459
paulson@13543
   460
constdefs
paulson@13543
   461
 L_r :: "[i, i] => i"
paulson@13543
   462
  "L_r(f,i) == 
paulson@13543
   463
      transrec(i, \<lambda>x r. 
paulson@13543
   464
         if x=0 then 0
paulson@13543
   465
         else if Limit(x) then rlimit(x, \<lambda>y. r`y)
paulson@13543
   466
         else L_succ_r(f, r ` Arith.pred(x), Arith.pred(x)))"
paulson@13543
   467
paulson@13543
   468
subsubsection{*The Corresponding Recursion Equations*}
paulson@13543
   469
lemma [simp]: "L_r(f,0) = 0"
paulson@13543
   470
by (simp add: def_transrec [OF L_r_def])
paulson@13543
   471
paulson@13543
   472
lemma [simp]: "Ord(i) ==> L_r(f, succ(i)) = L_succ_r(f, L_r(f,i), i)"
paulson@13543
   473
by (simp add: def_transrec [OF L_r_def])
paulson@13543
   474
paulson@13543
   475
text{*Needed to handle the limit case*}
paulson@13543
   476
lemma L_r_eq:
paulson@13543
   477
     "Ord(i) ==> 
paulson@13543
   478
      L_r(f, i) =
paulson@13543
   479
      (if i = 0 then 0
paulson@13543
   480
       else if Limit(i) then rlimit(i, op `(Lambda(i, L_r(f))))
paulson@13543
   481
       else L_succ_r (f, Lambda(i, L_r(f)) ` Arith.pred(i), Arith.pred(i)))"
paulson@13543
   482
apply (induct i rule: trans_induct3_rule)
paulson@13543
   483
apply (simp_all add: def_transrec [OF L_r_def])
paulson@13543
   484
done
paulson@13543
   485
paulson@13543
   486
text{*I don't know why the limit case is so complicated.*}
paulson@13543
   487
lemma [simp]: "Limit(i) ==> L_r(f,i) = rlimit(i, L_r(f))"
paulson@13543
   488
apply (simp add: Limit_nonzero def_transrec [OF L_r_def])
paulson@13543
   489
apply (rule rlimit_eqI, assumption)
paulson@13543
   490
apply (rule oallI)
paulson@13543
   491
apply (frule lt_Ord) 
paulson@13543
   492
apply (simp only: beta ltD L_r_eq [symmetric])  
paulson@13543
   493
done
paulson@13543
   494
paulson@13543
   495
lemma (in Nat_Times_Nat) L_r_type:
paulson@13543
   496
    "Ord(i) ==> L_r(fn,i) \<subseteq> Lset(i) * Lset(i)"
paulson@13543
   497
apply (induct i rule: trans_induct3_rule)
paulson@13546
   498
  apply (simp_all add: L_succ_r_type well_ord_L_succ_r rlimit_def, blast) 
paulson@13543
   499
done
paulson@13543
   500
paulson@13543
   501
lemma (in Nat_Times_Nat) well_ord_L_r:
paulson@13543
   502
    "Ord(i) ==> well_ord(Lset(i), L_r(fn,i))"
paulson@13543
   503
apply (induct i rule: trans_induct3_rule)
paulson@13546
   504
apply (simp_all add: well_ord0 L_r_type well_ord_L_succ_r well_ord_rlimit ltD)
paulson@13543
   505
done
paulson@13543
   506
paulson@13543
   507
lemma well_ord_L_r:
paulson@13543
   508
    "Ord(i) ==> \<exists>r. well_ord(Lset(i), r)"
paulson@13543
   509
apply (insert nat_times_nat_lepoll_nat)
paulson@13543
   510
apply (unfold lepoll_def)
paulson@13543
   511
apply (blast intro: exI Nat_Times_Nat.well_ord_L_r Nat_Times_Nat.intro)
paulson@13543
   512
done
paulson@13543
   513
paulson@13543
   514
paulson@13543
   515
text{*Locale for proving results under the assumption @{text "V=L"}*}
paulson@13543
   516
locale V_equals_L =
paulson@13543
   517
  assumes VL: "L(x)"
paulson@13543
   518
paulson@13543
   519
text{*The Axiom of Choice holds in @{term L}!  Or, to be precise, the
paulson@13543
   520
Wellordering Theorem.*}
paulson@13543
   521
theorem (in V_equals_L) AC: "\<exists>r. well_ord(x,r)"
paulson@13543
   522
apply (insert Transset_Lset VL [of x]) 
paulson@13543
   523
apply (simp add: Transset_def L_def)
paulson@13543
   524
apply (blast dest!: well_ord_L_r intro: well_ord_subset) 
paulson@13543
   525
done
paulson@13543
   526
paulson@13543
   527
end