src/ZF/Univ.thy
author paulson
Tue, 18 Jun 2002 18:45:07 +0200
changeset 13220 62c899c77151
parent 13203 fac77a839aa2
child 13255 407ad9c3036d
permissions -rw-r--r--
tidying
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     1
(*  Title:      ZF/univ.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   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
The cumulative hierarchy and a small universe for recursive types
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Standard notation for Vset(i) is V(i), but users might want V for a variable
516
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 490
diff changeset
     9
1957113f0d7d installation of new inductive/datatype sections
lcp
parents: 490
diff changeset
    10
NOTE: univ(A) could be a translation; would simplify many proofs!
6093
87bf8c03b169 eliminated global/local names;
wenzelm
parents: 6053
diff changeset
    11
  But Ind_Syntax.univ refers to the constant "Univ.univ"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    14
theory Univ = Epsilon + Sum + Finite + mono:
3923
c257b82a1200 global;
wenzelm
parents: 2469
diff changeset
    15
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    16
constdefs
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    17
  Vfrom       :: "[i,i]=>i"
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
    18
    "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
    20
syntax   Vset :: "i=>i"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
translations
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
    22
    "Vset(x)"   ==      "Vfrom(0,x)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
3923
c257b82a1200 global;
wenzelm
parents: 2469
diff changeset
    24
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    25
constdefs
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    26
  Vrec        :: "[i, [i,i]=>i] =>i"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    27
    "Vrec(a,H) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    28
 		 	   H(z, lam w:Vset(x). g`rank(w)`w)) ` a"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    29
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    30
  Vrecursor   :: "[[i,i]=>i, i] =>i"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    31
    "Vrecursor(H,a) == transrec(rank(a), %x g. lam z: Vset(succ(x)).
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    32
				H(lam w:Vset(x). g`rank(w)`w, z)) ` a"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    33
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    34
  univ        :: "i=>i"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    35
    "univ(A) == Vfrom(A,nat)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    36
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    37
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    38
text{*NOT SUITABLE FOR REWRITING -- RECURSIVE!*}
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
    39
lemma Vfrom: "Vfrom(A,i) = A Un (\<Union>j\<in>i. Pow(Vfrom(A,j)))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    40
apply (subst Vfrom_def [THEN def_transrec])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    41
apply simp
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    42
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    43
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    44
subsubsection{* Monotonicity *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    45
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    46
lemma Vfrom_mono [rule_format]:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
    47
     "A<=B ==> \<forall>j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    48
apply (rule_tac a=i in eps_induct)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    49
apply (rule impI [THEN allI])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    50
apply (subst Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    51
apply (subst Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    52
apply (erule Un_mono)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    53
apply (erule UN_mono, blast) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    54
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    55
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
    56
lemma VfromI: "[| a \<in> Vfrom(A,j);  j<i |] ==> a \<in> Vfrom(A,i)"
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
    57
by (blast dest: Vfrom_mono [OF subset_refl le_imp_subset [OF leI]]) 
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
    58
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    59
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    60
subsubsection{* A fundamental equality: Vfrom does not require ordinals! *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    61
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    62
lemma Vfrom_rank_subset1: "Vfrom(A,x) <= Vfrom(A,rank(x))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    63
apply (rule_tac a=x in eps_induct)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    64
apply (subst Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    65
apply (subst Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    66
apply (blast intro!: rank_lt [THEN ltD])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    67
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    68
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    69
lemma Vfrom_rank_subset2: "Vfrom(A,rank(x)) <= Vfrom(A,x)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    70
apply (rule_tac a=x in eps_induct)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    71
apply (subst Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    72
apply (subst Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    73
apply (rule subset_refl [THEN Un_mono])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    74
apply (rule UN_least)
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
    75
txt{*expand rank(x1) = (\<Union>y\<in>x1. succ(rank(y))) in assumptions*}
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    76
apply (erule rank [THEN equalityD1, THEN subsetD, THEN UN_E])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    77
apply (rule subset_trans)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    78
apply (erule_tac [2] UN_upper)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    79
apply (rule subset_refl [THEN Vfrom_mono, THEN subset_trans, THEN Pow_mono])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    80
apply (erule ltI [THEN le_imp_subset])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    81
apply (rule Ord_rank [THEN Ord_succ])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    82
apply (erule bspec, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    83
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    84
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    85
lemma Vfrom_rank_eq: "Vfrom(A,rank(x)) = Vfrom(A,x)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    86
apply (rule equalityI)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    87
apply (rule Vfrom_rank_subset2)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    88
apply (rule Vfrom_rank_subset1)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    89
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    90
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    91
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    92
subsection{* Basic closure properties *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    93
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
    94
lemma zero_in_Vfrom: "y:x ==> 0 \<in> Vfrom(A,x)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    95
by (subst Vfrom, blast)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    96
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    97
lemma i_subset_Vfrom: "i <= Vfrom(A,i)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    98
apply (rule_tac a=i in eps_induct)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
    99
apply (subst Vfrom, blast)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   100
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   101
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   102
lemma A_subset_Vfrom: "A <= Vfrom(A,i)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   103
apply (subst Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   104
apply (rule Un_upper1)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   105
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   106
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   107
lemmas A_into_Vfrom = A_subset_Vfrom [THEN subsetD]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   108
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   109
lemma subset_mem_Vfrom: "a <= Vfrom(A,i) ==> a \<in> Vfrom(A,succ(i))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   110
by (subst Vfrom, blast)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   111
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   112
subsubsection{* Finite sets and ordered pairs *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   113
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   114
lemma singleton_in_Vfrom: "a \<in> Vfrom(A,i) ==> {a} \<in> Vfrom(A,succ(i))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   115
by (rule subset_mem_Vfrom, safe)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   116
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   117
lemma doubleton_in_Vfrom:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   118
     "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i) |] ==> {a,b} \<in> Vfrom(A,succ(i))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   119
by (rule subset_mem_Vfrom, safe)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   120
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   121
lemma Pair_in_Vfrom:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   122
    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i) |] ==> <a,b> \<in> Vfrom(A,succ(succ(i)))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   123
apply (unfold Pair_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   124
apply (blast intro: doubleton_in_Vfrom) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   125
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   126
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   127
lemma succ_in_Vfrom: "a <= Vfrom(A,i) ==> succ(a) \<in> Vfrom(A,succ(succ(i)))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   128
apply (intro subset_mem_Vfrom succ_subsetI, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   129
apply (erule subset_trans) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   130
apply (rule Vfrom_mono [OF subset_refl subset_succI]) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   131
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   132
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   133
subsection{* 0, successor and limit equations fof Vfrom *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   134
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   135
lemma Vfrom_0: "Vfrom(A,0) = A"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   136
by (subst Vfrom, blast)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   137
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   138
lemma Vfrom_succ_lemma: "Ord(i) ==> Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   139
apply (rule Vfrom [THEN trans])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   140
apply (rule equalityI [THEN subst_context, 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   141
                       OF _ succI1 [THEN RepFunI, THEN Union_upper]])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   142
apply (rule UN_least)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   143
apply (rule subset_refl [THEN Vfrom_mono, THEN Pow_mono])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   144
apply (erule ltI [THEN le_imp_subset])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   145
apply (erule Ord_succ)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   146
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   147
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   148
lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   149
apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   150
apply (rule_tac x1 = "i" in Vfrom_rank_eq [THEN subst])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   151
apply (subst rank_succ)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   152
apply (rule Ord_rank [THEN Vfrom_succ_lemma])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   153
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   154
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   155
(*The premise distinguishes this from Vfrom(A,0);  allowing X=0 forces
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   156
  the conclusion to be Vfrom(A,Union(X)) = A Un (\<Union>y\<in>X. Vfrom(A,y)) *)
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   157
lemma Vfrom_Union: "y:X ==> Vfrom(A,Union(X)) = (\<Union>y\<in>X. Vfrom(A,y))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   158
apply (subst Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   159
apply (rule equalityI)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   160
txt{*first inclusion*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   161
apply (rule Un_least)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   162
apply (rule A_subset_Vfrom [THEN subset_trans])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   163
apply (rule UN_upper, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   164
apply (rule UN_least)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   165
apply (erule UnionE)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   166
apply (rule subset_trans)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   167
apply (erule_tac [2] UN_upper,
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   168
       subst Vfrom, erule subset_trans [OF UN_upper Un_upper2])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   169
txt{*opposite inclusion*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   170
apply (rule UN_least)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   171
apply (subst Vfrom, blast)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   172
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   173
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   174
subsection{* Vfrom applied to Limit ordinals *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   175
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   176
(*NB. limit ordinals are non-empty:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   177
      Vfrom(A,0) = A = A Un (\<Union>y\<in>0. Vfrom(A,y)) *)
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   178
lemma Limit_Vfrom_eq:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   179
    "Limit(i) ==> Vfrom(A,i) = (\<Union>y\<in>i. Vfrom(A,y))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   180
apply (rule Limit_has_0 [THEN ltD, THEN Vfrom_Union, THEN subst], assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   181
apply (simp add: Limit_Union_eq) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   182
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   183
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   184
lemma Limit_VfromE:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   185
    "[| a \<in> Vfrom(A,i);  ~R ==> Limit(i);
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   186
        !!x. [| x<i;  a \<in> Vfrom(A,x) |] ==> R
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   187
     |] ==> R"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   188
apply (rule classical)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   189
apply (rule Limit_Vfrom_eq [THEN equalityD1, THEN subsetD, THEN UN_E])
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   190
  prefer 2 apply assumption
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   191
 apply blast 
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   192
apply (blast intro: ltI Limit_is_Ord)
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   193
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   194
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   195
lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   196
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   197
lemma singleton_in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   198
    "[| a \<in> Vfrom(A,i);  Limit(i) |] ==> {a} \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   199
apply (erule Limit_VfromE, assumption)
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   200
apply (erule singleton_in_Vfrom [THEN VfromI])
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   201
apply (blast intro: Limit_has_succ) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   202
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   203
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   204
lemmas Vfrom_UnI1 = 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   205
    Un_upper1 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   206
lemmas Vfrom_UnI2 = 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   207
    Un_upper2 [THEN subset_refl [THEN Vfrom_mono, THEN subsetD], standard]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   208
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   209
text{*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   210
lemma doubleton_in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   211
    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i) |] ==> {a,b} \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   212
apply (erule Limit_VfromE, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   213
apply (erule Limit_VfromE, assumption)
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   214
apply (blast intro:  VfromI [OF doubleton_in_Vfrom]
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   215
                     Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   216
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   217
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   218
lemma Pair_in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   219
    "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i) |] ==> <a,b> \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   220
txt{*Infer that a, b occur at ordinals x,xa < i.*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   221
apply (erule Limit_VfromE, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   222
apply (erule Limit_VfromE, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   223
txt{*Infer that succ(succ(x Un xa)) < i *}
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   224
apply (blast intro: VfromI [OF Pair_in_Vfrom]
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   225
                    Vfrom_UnI1 Vfrom_UnI2 Limit_has_succ Un_least_lt)
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   226
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   227
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   228
lemma product_VLimit: "Limit(i) ==> Vfrom(A,i) * Vfrom(A,i) <= Vfrom(A,i)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   229
by (blast intro: Pair_in_VLimit)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   230
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   231
lemmas Sigma_subset_VLimit =
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   232
     subset_trans [OF Sigma_mono product_VLimit]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   233
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   234
lemmas nat_subset_VLimit =
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   235
     subset_trans [OF nat_le_Limit [THEN le_imp_subset] i_subset_Vfrom]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   236
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   237
lemma nat_into_VLimit: "[| n: nat;  Limit(i) |] ==> n \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   238
by (blast intro: nat_subset_VLimit [THEN subsetD])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   239
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   240
subsubsection{* Closure under disjoint union *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   241
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   242
lemmas zero_in_VLimit = Limit_has_0 [THEN ltD, THEN zero_in_Vfrom, standard]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   243
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   244
lemma one_in_VLimit: "Limit(i) ==> 1 \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   245
by (blast intro: nat_into_VLimit)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   246
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   247
lemma Inl_in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   248
    "[| a \<in> Vfrom(A,i); Limit(i) |] ==> Inl(a) \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   249
apply (unfold Inl_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   250
apply (blast intro: zero_in_VLimit Pair_in_VLimit)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   251
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   252
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   253
lemma Inr_in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   254
    "[| b \<in> Vfrom(A,i); Limit(i) |] ==> Inr(b) \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   255
apply (unfold Inr_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   256
apply (blast intro: one_in_VLimit Pair_in_VLimit)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   257
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   258
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   259
lemma sum_VLimit: "Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   260
by (blast intro!: Inl_in_VLimit Inr_in_VLimit)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   261
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   262
lemmas sum_subset_VLimit = subset_trans [OF sum_mono sum_VLimit]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   263
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   264
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   265
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   266
subsection{* Properties assuming Transset(A) *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   267
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   268
lemma Transset_Vfrom: "Transset(A) ==> Transset(Vfrom(A,i))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   269
apply (rule_tac a=i in eps_induct)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   270
apply (subst Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   271
apply (blast intro!: Transset_Union_family Transset_Un Transset_Pow)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   272
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   273
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   274
lemma Transset_Vfrom_succ:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   275
     "Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   276
apply (rule Vfrom_succ [THEN trans])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   277
apply (rule equalityI [OF _ Un_upper2])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   278
apply (rule Un_least [OF _ subset_refl])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   279
apply (rule A_subset_Vfrom [THEN subset_trans])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   280
apply (erule Transset_Vfrom [THEN Transset_iff_Pow [THEN iffD1]])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   281
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   282
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   283
lemma Transset_Pair_subset: "[| <a,b> <= C; Transset(C) |] ==> a: C & b: C"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   284
by (unfold Pair_def Transset_def, blast)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   285
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   286
lemma Transset_Pair_subset_VLimit:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   287
     "[| <a,b> <= Vfrom(A,i);  Transset(A);  Limit(i) |]
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   288
      ==> <a,b> \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   289
apply (erule Transset_Pair_subset [THEN conjE])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   290
apply (erule Transset_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   291
apply (blast intro: Pair_in_VLimit)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   292
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   293
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   294
lemma Union_in_Vfrom:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   295
     "[| X \<in> Vfrom(A,j);  Transset(A) |] ==> Union(X) \<in> Vfrom(A, succ(j))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   296
apply (drule Transset_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   297
apply (rule subset_mem_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   298
apply (unfold Transset_def, blast)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   299
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   300
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   301
lemma Union_in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   302
     "[| X \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Union(X) \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   303
apply (rule Limit_VfromE, assumption+)
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   304
apply (blast intro: Limit_has_succ VfromI Union_in_Vfrom)
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   305
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   306
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   307
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   308
(*** Closure under product/sum applied to elements -- thus Vfrom(A,i)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   309
     is a model of simple type theory provided A is a transitive set
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   310
     and i is a limit ordinal
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   311
***)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   312
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   313
text{*General theorem for membership in Vfrom(A,i) when i is a limit ordinal*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   314
lemma in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   315
  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   316
      !!x y j. [| j<i; 1:j; x \<in> Vfrom(A,j); y \<in> Vfrom(A,j) |]
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   317
               ==> EX k. h(x,y) \<in> Vfrom(A,k) & k<i |]
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   318
   ==> h(a,b) \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   319
txt{*Infer that a, b occur at ordinals x,xa < i.*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   320
apply (erule Limit_VfromE, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   321
apply (erule Limit_VfromE, assumption, atomize)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   322
apply (drule_tac x=a in spec) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   323
apply (drule_tac x=b in spec) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   324
apply (drule_tac x="x Un xa Un 2" in spec) 
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   325
apply (simp add: Un_least_lt_iff lt_Ord Vfrom_UnI1 Vfrom_UnI2) 
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   326
apply (blast intro: Limit_has_0 Limit_has_succ VfromI)
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   327
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   328
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   329
subsubsection{* products *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   330
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   331
lemma prod_in_Vfrom:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   332
    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |]
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   333
     ==> a*b \<in> Vfrom(A, succ(succ(succ(j))))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   334
apply (drule Transset_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   335
apply (rule subset_mem_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   336
apply (unfold Transset_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   337
apply (blast intro: Pair_in_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   338
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   339
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   340
lemma prod_in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   341
  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   342
   ==> a*b \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   343
apply (erule in_VLimit, assumption+)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   344
apply (blast intro: prod_in_Vfrom Limit_has_succ)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   345
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   346
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   347
subsubsection{* Disjoint sums, aka Quine ordered pairs *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   348
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   349
lemma sum_in_Vfrom:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   350
    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A);  1:j |]
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   351
     ==> a+b \<in> Vfrom(A, succ(succ(succ(j))))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   352
apply (unfold sum_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   353
apply (drule Transset_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   354
apply (rule subset_mem_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   355
apply (unfold Transset_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   356
apply (blast intro: zero_in_Vfrom Pair_in_Vfrom i_subset_Vfrom [THEN subsetD])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   357
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   358
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   359
lemma sum_in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   360
  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   361
   ==> a+b \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   362
apply (erule in_VLimit, assumption+)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   363
apply (blast intro: sum_in_Vfrom Limit_has_succ)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   364
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   365
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   366
subsubsection{* function space! *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   367
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   368
lemma fun_in_Vfrom:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   369
    "[| a \<in> Vfrom(A,j);  b \<in> Vfrom(A,j);  Transset(A) |] ==>
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   370
          a->b \<in> Vfrom(A, succ(succ(succ(succ(j)))))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   371
apply (unfold Pi_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   372
apply (drule Transset_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   373
apply (rule subset_mem_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   374
apply (rule Collect_subset [THEN subset_trans])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   375
apply (subst Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   376
apply (rule subset_trans [THEN subset_trans])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   377
apply (rule_tac [3] Un_upper2)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   378
apply (rule_tac [2] succI1 [THEN UN_upper])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   379
apply (rule Pow_mono)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   380
apply (unfold Transset_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   381
apply (blast intro: Pair_in_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   382
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   383
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   384
lemma fun_in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   385
  "[| a \<in> Vfrom(A,i);  b \<in> Vfrom(A,i);  Limit(i);  Transset(A) |]
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   386
   ==> a->b \<in> Vfrom(A,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   387
apply (erule in_VLimit, assumption+)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   388
apply (blast intro: fun_in_Vfrom Limit_has_succ)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   389
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   390
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   391
lemma Pow_in_Vfrom:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   392
    "[| a \<in> Vfrom(A,j);  Transset(A) |] ==> Pow(a) \<in> Vfrom(A, succ(succ(j)))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   393
apply (drule Transset_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   394
apply (rule subset_mem_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   395
apply (unfold Transset_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   396
apply (subst Vfrom, blast)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   397
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   398
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   399
lemma Pow_in_VLimit:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   400
     "[| a \<in> Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) \<in> Vfrom(A,i)"
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   401
by (blast elim: Limit_VfromE intro: Limit_has_succ Pow_in_Vfrom VfromI)
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   402
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   403
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   404
subsection{* The set Vset(i) *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   405
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   406
lemma Vset: "Vset(i) = (\<Union>j\<in>i. Pow(Vset(j)))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   407
by (subst Vfrom, blast)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   408
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   409
lemmas Vset_succ = Transset_0 [THEN Transset_Vfrom_succ, standard]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   410
lemmas Transset_Vset = Transset_0 [THEN Transset_Vfrom, standard]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   411
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   412
subsubsection{* Characterisation of the elements of Vset(i) *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   413
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   414
lemma VsetD [rule_format]: "Ord(i) ==> \<forall>b. b \<in> Vset(i) --> rank(b) < i"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   415
apply (erule trans_induct)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   416
apply (subst Vset, safe)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   417
apply (subst rank)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   418
apply (blast intro: ltI UN_succ_least_lt) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   419
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   420
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   421
lemma VsetI_lemma [rule_format]:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   422
     "Ord(i) ==> \<forall>b. rank(b) \<in> i --> b \<in> Vset(i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   423
apply (erule trans_induct)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   424
apply (rule allI)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   425
apply (subst Vset)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   426
apply (blast intro!: rank_lt [THEN ltD])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   427
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   428
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   429
lemma VsetI: "rank(x)<i ==> x \<in> Vset(i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   430
by (blast intro: VsetI_lemma elim: ltE)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   431
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   432
text{*Merely a lemma for the next result*}
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   433
lemma Vset_Ord_rank_iff: "Ord(i) ==> b \<in> Vset(i) <-> rank(b) < i"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   434
by (blast intro: VsetD VsetI)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   435
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   436
lemma Vset_rank_iff [simp]: "b \<in> Vset(a) <-> rank(b) < rank(a)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   437
apply (rule Vfrom_rank_eq [THEN subst])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   438
apply (rule Ord_rank [THEN Vset_Ord_rank_iff])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   439
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   440
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   441
text{*This is rank(rank(a)) = rank(a) *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   442
declare Ord_rank [THEN rank_of_Ord, simp]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   443
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   444
lemma rank_Vset: "Ord(i) ==> rank(Vset(i)) = i"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   445
apply (subst rank)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   446
apply (rule equalityI, safe)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   447
apply (blast intro: VsetD [THEN ltD]) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   448
apply (blast intro: VsetD [THEN ltD] Ord_trans) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   449
apply (blast intro: i_subset_Vfrom [THEN subsetD]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   450
                    Ord_in_Ord [THEN rank_of_Ord, THEN ssubst])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   451
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   452
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   453
subsubsection{* Reasoning about sets in terms of their elements' ranks *}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   455
lemma arg_subset_Vset_rank: "a <= Vset(rank(a))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   456
apply (rule subsetI)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   457
apply (erule rank_lt [THEN VsetI])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   458
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   459
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   460
lemma Int_Vset_subset:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   461
    "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   462
apply (rule subset_trans) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   463
apply (rule Int_greatest [OF subset_refl arg_subset_Vset_rank])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   464
apply (blast intro: Ord_rank) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   465
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   466
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   467
subsubsection{* Set up an environment for simplification *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   468
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   469
lemma rank_Inl: "rank(a) < rank(Inl(a))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   470
apply (unfold Inl_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   471
apply (rule rank_pair2)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   472
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   473
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   474
lemma rank_Inr: "rank(a) < rank(Inr(a))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   475
apply (unfold Inr_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   476
apply (rule rank_pair2)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   477
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   478
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   479
lemmas rank_rls = rank_Inl rank_Inr rank_pair1 rank_pair2
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   480
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   481
subsubsection{* Recursion over Vset levels! *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   482
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   483
text{*NOT SUITABLE FOR REWRITING: recursive!*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   484
lemma Vrec: "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   485
apply (unfold Vrec_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   486
apply (subst transrec)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   487
apply simp
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13163
diff changeset
   488
apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   489
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   490
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   491
text{*This form avoids giant explosions in proofs.  NOTE USE OF == *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   492
lemma def_Vrec:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   493
    "[| !!x. h(x)==Vrec(x,H) |] ==>
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   494
     h(a) = H(a, lam x: Vset(rank(a)). h(x))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   495
apply simp 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   496
apply (rule Vrec)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   497
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   498
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   499
text{*NOT SUITABLE FOR REWRITING: recursive!*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   500
lemma Vrecursor:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   501
     "Vrecursor(H,a) = H(lam x:Vset(rank(a)). Vrecursor(H,x),  a)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   502
apply (unfold Vrecursor_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   503
apply (subst transrec, simp)
13175
81082cfa5618 new definition of "apply" and new simprule "beta_if"
paulson
parents: 13163
diff changeset
   504
apply (rule refl [THEN lam_cong, THEN subst_context], simp add: lt_def)
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   505
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   506
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   507
text{*This form avoids giant explosions in proofs.  NOTE USE OF == *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   508
lemma def_Vrecursor:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   509
     "h == Vrecursor(H) ==> h(a) = H(lam x: Vset(rank(a)). h(x),  a)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   510
apply simp
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   511
apply (rule Vrecursor)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   512
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   513
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   514
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   515
subsection{* univ(A) *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   516
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   517
lemma univ_mono: "A<=B ==> univ(A) <= univ(B)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   518
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   519
apply (erule Vfrom_mono)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   520
apply (rule subset_refl)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   521
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   522
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   523
lemma Transset_univ: "Transset(A) ==> Transset(univ(A))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   524
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   525
apply (erule Transset_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   526
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   527
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   528
subsubsection{* univ(A) as a limit *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   529
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   530
lemma univ_eq_UN: "univ(A) = (\<Union>i\<in>nat. Vfrom(A,i))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   531
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   532
apply (rule Limit_nat [THEN Limit_Vfrom_eq])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   533
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   534
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   535
lemma subset_univ_eq_Int: "c <= univ(A) ==> c = (\<Union>i\<in>nat. c Int Vfrom(A,i))"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   536
apply (rule subset_UN_iff_eq [THEN iffD1])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   537
apply (erule univ_eq_UN [THEN subst])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   538
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   539
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   540
lemma univ_Int_Vfrom_subset:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   541
    "[| a <= univ(X);
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   542
        !!i. i:nat ==> a Int Vfrom(X,i) <= b |]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   543
     ==> a <= b"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   544
apply (subst subset_univ_eq_Int, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   545
apply (rule UN_least, simp) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   546
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   547
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   548
lemma univ_Int_Vfrom_eq:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   549
    "[| a <= univ(X);   b <= univ(X);
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   550
        !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   551
     |] ==> a = b"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   552
apply (rule equalityI)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   553
apply (rule univ_Int_Vfrom_subset, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   554
apply (blast elim: equalityCE) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   555
apply (rule univ_Int_Vfrom_subset, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   556
apply (blast elim: equalityCE) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   557
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   558
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   559
subsubsection{* Closure properties *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   560
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   561
lemma zero_in_univ: "0 \<in> univ(A)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   562
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   563
apply (rule nat_0I [THEN zero_in_Vfrom])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   564
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   565
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   566
lemma A_subset_univ: "A <= univ(A)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   567
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   568
apply (rule A_subset_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   569
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   570
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   571
lemmas A_into_univ = A_subset_univ [THEN subsetD, standard]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   572
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   573
subsubsection{* Closure under unordered and ordered pairs *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   574
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   575
lemma singleton_in_univ: "a: univ(A) ==> {a} \<in> univ(A)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   576
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   577
apply (blast intro: singleton_in_VLimit Limit_nat)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   578
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   579
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   580
lemma doubleton_in_univ:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   581
    "[| a: univ(A);  b: univ(A) |] ==> {a,b} \<in> univ(A)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   582
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   583
apply (blast intro: doubleton_in_VLimit Limit_nat)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   584
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   585
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   586
lemma Pair_in_univ:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   587
    "[| a: univ(A);  b: univ(A) |] ==> <a,b> \<in> univ(A)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   588
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   589
apply (blast intro: Pair_in_VLimit Limit_nat)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   590
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   591
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   592
lemma Union_in_univ:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   593
     "[| X: univ(A);  Transset(A) |] ==> Union(X) \<in> univ(A)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   594
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   595
apply (blast intro: Union_in_VLimit Limit_nat)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   596
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   597
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   598
lemma product_univ: "univ(A)*univ(A) <= univ(A)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   599
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   600
apply (rule Limit_nat [THEN product_VLimit])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   601
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   602
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   603
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   604
subsubsection{* The natural numbers *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   605
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   606
lemma nat_subset_univ: "nat <= univ(A)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   607
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   608
apply (rule i_subset_Vfrom)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   609
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   610
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   611
text{* n:nat ==> n:univ(A) *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   612
lemmas nat_into_univ = nat_subset_univ [THEN subsetD, standard]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   613
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   614
subsubsection{* instances for 1 and 2 *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   615
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   616
lemma one_in_univ: "1 \<in> univ(A)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   617
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   618
apply (rule Limit_nat [THEN one_in_VLimit])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   619
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   620
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   621
text{*unused!*}
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   622
lemma two_in_univ: "2 \<in> univ(A)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   623
by (blast intro: nat_into_univ)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   624
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   625
lemma bool_subset_univ: "bool <= univ(A)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   626
apply (unfold bool_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   627
apply (blast intro!: zero_in_univ one_in_univ)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   628
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   629
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   630
lemmas bool_into_univ = bool_subset_univ [THEN subsetD, standard]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   631
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   632
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   633
subsubsection{* Closure under disjoint union *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   634
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   635
lemma Inl_in_univ: "a: univ(A) ==> Inl(a) \<in> univ(A)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   636
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   637
apply (erule Inl_in_VLimit [OF _ Limit_nat])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   638
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   639
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   640
lemma Inr_in_univ: "b: univ(A) ==> Inr(b) \<in> univ(A)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   641
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   642
apply (erule Inr_in_VLimit [OF _ Limit_nat])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   643
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   644
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   645
lemma sum_univ: "univ(C)+univ(C) <= univ(C)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   646
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   647
apply (rule Limit_nat [THEN sum_VLimit])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   648
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   649
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   650
lemmas sum_subset_univ = subset_trans [OF sum_mono sum_univ]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   651
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   652
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   653
subsubsection{* Closure under binary union -- use Un_least *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   654
subsubsection{* Closure under Collect -- use  (Collect_subset RS subset_trans)  *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   655
subsubsection{* Closure under RepFun -- use   RepFun_subset  *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   656
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   657
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   658
subsection{* Finite Branching Closure Properties *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   659
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   660
subsubsection{* Closure under finite powerset *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   661
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   662
lemma Fin_Vfrom_lemma:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   663
     "[| b: Fin(Vfrom(A,i));  Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j<i"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   664
apply (erule Fin_induct)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   665
apply (blast dest!: Limit_has_0, safe)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   666
apply (erule Limit_VfromE, assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   667
apply (blast intro!: Un_least_lt intro: Vfrom_UnI1 Vfrom_UnI2)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   668
done
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   669
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   670
lemma Fin_VLimit: "Limit(i) ==> Fin(Vfrom(A,i)) <= Vfrom(A,i)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   671
apply (rule subsetI)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   672
apply (drule Fin_Vfrom_lemma, safe)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   673
apply (rule Vfrom [THEN ssubst])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   674
apply (blast dest!: ltD)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   675
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   676
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   677
lemmas Fin_subset_VLimit = subset_trans [OF Fin_mono Fin_VLimit]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   678
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   679
lemma Fin_univ: "Fin(univ(A)) <= univ(A)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   680
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   681
apply (rule Limit_nat [THEN Fin_VLimit])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   682
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   683
13203
fac77a839aa2 Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents: 13185
diff changeset
   684
subsubsection{* Closure under finite powers: functions from a natural number *}
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   685
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   686
lemma nat_fun_VLimit:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   687
     "[| n: nat;  Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   688
apply (erule nat_fun_subset_Fin [THEN subset_trans])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   689
apply (blast del: subsetI
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   690
    intro: subset_refl Fin_subset_VLimit Sigma_subset_VLimit nat_subset_VLimit)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   691
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   692
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   693
lemmas nat_fun_subset_VLimit = subset_trans [OF Pi_mono nat_fun_VLimit]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   694
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   695
lemma nat_fun_univ: "n: nat ==> n -> univ(A) <= univ(A)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   696
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   697
apply (erule nat_fun_VLimit [OF _ Limit_nat])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   698
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   699
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   700
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   701
subsubsection{* Closure under finite function space *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   702
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   703
text{*General but seldom-used version; normally the domain is fixed*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   704
lemma FiniteFun_VLimit1:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   705
     "Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   706
apply (rule FiniteFun.dom_subset [THEN subset_trans])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   707
apply (blast del: subsetI
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   708
             intro: Fin_subset_VLimit Sigma_subset_VLimit subset_refl)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   709
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   710
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   711
lemma FiniteFun_univ1: "univ(A) -||> univ(A) <= univ(A)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   712
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   713
apply (rule Limit_nat [THEN FiniteFun_VLimit1])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   714
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   715
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   716
text{*Version for a fixed domain*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   717
lemma FiniteFun_VLimit:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   718
     "[| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   719
apply (rule subset_trans) 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   720
apply (erule FiniteFun_mono [OF _ subset_refl])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   721
apply (erule FiniteFun_VLimit1)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   722
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   723
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   724
lemma FiniteFun_univ:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   725
    "W <= univ(A) ==> W -||> univ(A) <= univ(A)"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   726
apply (unfold univ_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   727
apply (erule FiniteFun_VLimit [OF _ Limit_nat])
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   728
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   729
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   730
lemma FiniteFun_in_univ:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   731
     "[| f: W -||> univ(A);  W <= univ(A) |] ==> f \<in> univ(A)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   732
by (erule FiniteFun_univ [THEN subsetD], assumption)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   733
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   734
text{*Remove <= from the rule above*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   735
lemmas FiniteFun_in_univ' = FiniteFun_in_univ [OF _ subsetI]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   736
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   737
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   738
subsection{** For QUniv.  Properties of Vfrom analogous to the "take-lemma" **}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   739
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   740
subsection{* Intersecting a*b with Vfrom... *}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   741
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   742
text{*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   743
lemma doubleton_in_Vfrom_D:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   744
     "[| {a,b} \<in> Vfrom(X,succ(i));  Transset(X) |]
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   745
      ==> a \<in> Vfrom(X,i)  &  b \<in> Vfrom(X,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   746
by (drule Transset_Vfrom_succ [THEN equalityD1, THEN subsetD, THEN PowD], 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   747
    assumption, fast)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   748
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   749
text{*This weaker version says a, b exist at the same level*}
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   750
lemmas Vfrom_doubleton_D = Transset_Vfrom [THEN Transset_doubleton_D, standard]
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   751
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   752
(** Using only the weaker theorem would prove <a,b> \<in> Vfrom(X,i)
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   753
      implies a, b \<in> Vfrom(X,i), which is useless for induction.
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   754
    Using only the stronger theorem would prove <a,b> \<in> Vfrom(X,succ(succ(i)))
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   755
      implies a, b \<in> Vfrom(X,i), leaving the succ(i) case untreated.
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   756
    The combination gives a reduction by precisely one level, which is
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   757
      most convenient for proofs.
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   758
**)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   759
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   760
lemma Pair_in_Vfrom_D:
13220
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   761
    "[| <a,b> \<in> Vfrom(X,succ(i));  Transset(X) |]
62c899c77151 tidying
paulson
parents: 13203
diff changeset
   762
     ==> a \<in> Vfrom(X,i)  &  b \<in> Vfrom(X,i)"
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   763
apply (unfold Pair_def)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   764
apply (blast dest!: doubleton_in_Vfrom_D Vfrom_doubleton_D)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   765
done
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   766
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   767
lemma product_Int_Vfrom_subset:
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   768
     "Transset(X) ==>
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   769
      (a*b) Int Vfrom(X, succ(i)) <= (a Int Vfrom(X,i)) * (b Int Vfrom(X,i))"
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   770
by (blast dest!: Pair_in_Vfrom_D)
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   771
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   772
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   773
ML
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   774
{*
6053
8a1059aa01f0 new inductive, datatype and primrec packages, etc.
paulson
parents: 3940
diff changeset
   775
13163
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   776
val Vfrom = thm "Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   777
val Vfrom_mono = thm "Vfrom_mono";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   778
val Vfrom_rank_subset1 = thm "Vfrom_rank_subset1";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   779
val Vfrom_rank_subset2 = thm "Vfrom_rank_subset2";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   780
val Vfrom_rank_eq = thm "Vfrom_rank_eq";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   781
val zero_in_Vfrom = thm "zero_in_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   782
val i_subset_Vfrom = thm "i_subset_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   783
val A_subset_Vfrom = thm "A_subset_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   784
val subset_mem_Vfrom = thm "subset_mem_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   785
val singleton_in_Vfrom = thm "singleton_in_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   786
val doubleton_in_Vfrom = thm "doubleton_in_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   787
val Pair_in_Vfrom = thm "Pair_in_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   788
val succ_in_Vfrom = thm "succ_in_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   789
val Vfrom_0 = thm "Vfrom_0";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   790
val Vfrom_succ = thm "Vfrom_succ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   791
val Vfrom_Union = thm "Vfrom_Union";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   792
val Limit_Vfrom_eq = thm "Limit_Vfrom_eq";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   793
val zero_in_VLimit = thm "zero_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   794
val singleton_in_VLimit = thm "singleton_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   795
val Vfrom_UnI1 = thm "Vfrom_UnI1";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   796
val Vfrom_UnI2 = thm "Vfrom_UnI2";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   797
val doubleton_in_VLimit = thm "doubleton_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   798
val Pair_in_VLimit = thm "Pair_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   799
val product_VLimit = thm "product_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   800
val Sigma_subset_VLimit = thm "Sigma_subset_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   801
val nat_subset_VLimit = thm "nat_subset_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   802
val nat_into_VLimit = thm "nat_into_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   803
val zero_in_VLimit = thm "zero_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   804
val one_in_VLimit = thm "one_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   805
val Inl_in_VLimit = thm "Inl_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   806
val Inr_in_VLimit = thm "Inr_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   807
val sum_VLimit = thm "sum_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   808
val sum_subset_VLimit = thm "sum_subset_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   809
val Transset_Vfrom = thm "Transset_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   810
val Transset_Vfrom_succ = thm "Transset_Vfrom_succ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   811
val Transset_Pair_subset = thm "Transset_Pair_subset";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   812
val Union_in_Vfrom = thm "Union_in_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   813
val Union_in_VLimit = thm "Union_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   814
val in_VLimit = thm "in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   815
val prod_in_Vfrom = thm "prod_in_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   816
val prod_in_VLimit = thm "prod_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   817
val sum_in_Vfrom = thm "sum_in_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   818
val sum_in_VLimit = thm "sum_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   819
val fun_in_Vfrom = thm "fun_in_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   820
val fun_in_VLimit = thm "fun_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   821
val Pow_in_Vfrom = thm "Pow_in_Vfrom";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   822
val Pow_in_VLimit = thm "Pow_in_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   823
val Vset = thm "Vset";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   824
val Vset_succ = thm "Vset_succ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   825
val Transset_Vset = thm "Transset_Vset";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   826
val VsetD = thm "VsetD";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   827
val VsetI = thm "VsetI";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   828
val Vset_Ord_rank_iff = thm "Vset_Ord_rank_iff";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   829
val Vset_rank_iff = thm "Vset_rank_iff";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   830
val rank_Vset = thm "rank_Vset";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   831
val arg_subset_Vset_rank = thm "arg_subset_Vset_rank";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   832
val Int_Vset_subset = thm "Int_Vset_subset";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   833
val rank_Inl = thm "rank_Inl";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   834
val rank_Inr = thm "rank_Inr";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   835
val Vrec = thm "Vrec";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   836
val def_Vrec = thm "def_Vrec";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   837
val Vrecursor = thm "Vrecursor";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   838
val def_Vrecursor = thm "def_Vrecursor";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   839
val univ_mono = thm "univ_mono";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   840
val Transset_univ = thm "Transset_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   841
val univ_eq_UN = thm "univ_eq_UN";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   842
val subset_univ_eq_Int = thm "subset_univ_eq_Int";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   843
val univ_Int_Vfrom_subset = thm "univ_Int_Vfrom_subset";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   844
val univ_Int_Vfrom_eq = thm "univ_Int_Vfrom_eq";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   845
val zero_in_univ = thm "zero_in_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   846
val A_subset_univ = thm "A_subset_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   847
val A_into_univ = thm "A_into_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   848
val singleton_in_univ = thm "singleton_in_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   849
val doubleton_in_univ = thm "doubleton_in_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   850
val Pair_in_univ = thm "Pair_in_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   851
val Union_in_univ = thm "Union_in_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   852
val product_univ = thm "product_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   853
val nat_subset_univ = thm "nat_subset_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   854
val nat_into_univ = thm "nat_into_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   855
val one_in_univ = thm "one_in_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   856
val two_in_univ = thm "two_in_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   857
val bool_subset_univ = thm "bool_subset_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   858
val bool_into_univ = thm "bool_into_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   859
val Inl_in_univ = thm "Inl_in_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   860
val Inr_in_univ = thm "Inr_in_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   861
val sum_univ = thm "sum_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   862
val sum_subset_univ = thm "sum_subset_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   863
val Fin_VLimit = thm "Fin_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   864
val Fin_subset_VLimit = thm "Fin_subset_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   865
val Fin_univ = thm "Fin_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   866
val nat_fun_VLimit = thm "nat_fun_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   867
val nat_fun_subset_VLimit = thm "nat_fun_subset_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   868
val nat_fun_univ = thm "nat_fun_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   869
val FiniteFun_VLimit1 = thm "FiniteFun_VLimit1";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   870
val FiniteFun_univ1 = thm "FiniteFun_univ1";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   871
val FiniteFun_VLimit = thm "FiniteFun_VLimit";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   872
val FiniteFun_univ = thm "FiniteFun_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   873
val FiniteFun_in_univ = thm "FiniteFun_in_univ";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   874
val FiniteFun_in_univ' = thm "FiniteFun_in_univ'";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   875
val doubleton_in_Vfrom_D = thm "doubleton_in_Vfrom_D";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   876
val Vfrom_doubleton_D = thm "Vfrom_doubleton_D";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   877
val Pair_in_Vfrom_D = thm "Pair_in_Vfrom_D";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   878
val product_Int_Vfrom_subset = thm "product_Int_Vfrom_subset";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   879
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   880
val rank_rls = thms "rank_rls";
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   881
val rank_ss = simpset() addsimps [VsetI] 
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   882
              addsimps rank_rls @ (rank_rls RLN (2, [lt_trans]));
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   883
e320a52ff711 converted Arith, Univ, func to Isar format!
paulson
parents: 9395
diff changeset
   884
*}
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   885
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   886
end