src/ZF/QUniv.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 46821 ff6b0c1087f2
child 58871 c399ae4b836f
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6093
87bf8c03b169 eliminated global/local names;
wenzelm
parents: 3940
diff changeset
     1
(*  Title:      ZF/QUniv.thy
1478
2b8c2a7547ab expanded tabs
clasohm
parents: 1401
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Copyright   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
     6
header{*A Small Universe for Lazy Recursive Types*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13615
diff changeset
     8
theory QUniv imports Univ QPair begin
3923
c257b82a1200 global;
wenzelm
parents: 2469
diff changeset
     9
6112
5e4871c5136b datatype package improvements
paulson
parents: 6093
diff changeset
    10
(*Disjoint sums as a datatype*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    11
rep_datatype
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
    12
  elimination   sumE
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
    13
  induction     TrueI
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
    14
  case_eqns     case_Inl case_Inr
6112
5e4871c5136b datatype package improvements
paulson
parents: 6093
diff changeset
    15
5e4871c5136b datatype package improvements
paulson
parents: 6093
diff changeset
    16
(*Variant disjoint sums as a datatype*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    17
rep_datatype
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
    18
  elimination   qsumE
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
    19
  induction     TrueI
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 24893
diff changeset
    20
  case_eqns     qcase_QInl qcase_QInr
6112
5e4871c5136b datatype package improvements
paulson
parents: 6093
diff changeset
    21
24893
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    22
definition
b8ef7afe3a6b modernized specifications;
wenzelm
parents: 16417
diff changeset
    23
  quniv :: "i => i"  where
6112
5e4871c5136b datatype package improvements
paulson
parents: 6093
diff changeset
    24
   "quniv(A) == Pow(univ(eclose(A)))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    26
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
    27
subsection{*Properties involving Transset and Sum*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
    28
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    29
lemma Transset_includes_summands:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    30
     "[| Transset(C); A+B \<subseteq> C |] ==> A \<subseteq> C & B \<subseteq> C"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    31
apply (simp add: sum_def Un_subset_iff)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    32
apply (blast dest: Transset_includes_range)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    33
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    34
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    35
lemma Transset_sum_Int_subset:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    36
     "Transset(C) ==> (A+B) \<inter> C \<subseteq> (A \<inter> C) + (B \<inter> C)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    37
apply (simp add: sum_def Int_Un_distrib2)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    38
apply (blast dest: Transset_Pair_D)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    39
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    40
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
    41
subsection{*Introduction and Elimination Rules*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    42
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    43
lemma qunivI: "X \<subseteq> univ(eclose(A)) ==> X \<in> quniv(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    44
by (simp add: quniv_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    45
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    46
lemma qunivD: "X \<in> quniv(A) ==> X \<subseteq> univ(eclose(A))"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    47
by (simp add: quniv_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    48
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    49
lemma quniv_mono: "A<=B ==> quniv(A) \<subseteq> quniv(B)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    50
apply (unfold quniv_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    51
apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    52
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    53
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
    54
subsection{*Closure Properties*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    55
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    56
lemma univ_eclose_subset_quniv: "univ(eclose(A)) \<subseteq> quniv(A)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    57
apply (simp add: quniv_def Transset_iff_Pow [symmetric])
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    58
apply (rule Transset_eclose [THEN Transset_univ])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    59
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    60
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    61
(*Key property for proving A_subset_quniv; requires eclose in def of quniv*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    62
lemma univ_subset_quniv: "univ(A) \<subseteq> quniv(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    63
apply (rule arg_subset_eclose [THEN univ_mono, THEN subset_trans])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    64
apply (rule univ_eclose_subset_quniv)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    65
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    66
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
    67
lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD]
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    68
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    69
lemma Pow_univ_subset_quniv: "Pow(univ(A)) \<subseteq> quniv(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    70
apply (unfold quniv_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    71
apply (rule arg_subset_eclose [THEN univ_mono, THEN Pow_mono])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    72
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    73
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    74
lemmas univ_subset_into_quniv =
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
    75
    PowI [THEN Pow_univ_subset_quniv [THEN subsetD]]
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    76
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
    77
lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
    78
lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv]
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
    79
lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv]
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    80
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    81
lemmas A_subset_quniv =  subset_trans [OF A_subset_univ univ_subset_quniv]
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    82
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
    83
lemmas A_into_quniv = A_subset_quniv [THEN subsetD]
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    84
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    85
(*** univ(A) closure for Quine-inspired pairs and injections ***)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    86
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    87
(*Quine ordered pairs*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    88
lemma QPair_subset_univ:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    89
    "[| a \<subseteq> univ(A);  b \<subseteq> univ(A) |] ==> <a;b> \<subseteq> univ(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    90
by (simp add: QPair_def sum_subset_univ)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    91
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
    92
subsection{*Quine Disjoint Sum*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    93
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    94
lemma QInl_subset_univ: "a \<subseteq> univ(A) ==> QInl(a) \<subseteq> univ(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    95
apply (unfold QInl_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    96
apply (erule empty_subsetI [THEN QPair_subset_univ])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    97
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
    98
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
    99
lemmas naturals_subset_nat =
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   100
    Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec]
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   101
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   102
lemmas naturals_subset_univ =
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   103
    subset_trans [OF naturals_subset_nat nat_subset_univ]
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   104
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   105
lemma QInr_subset_univ: "a \<subseteq> univ(A) ==> QInr(a) \<subseteq> univ(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   106
apply (unfold QInr_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   107
apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   108
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   109
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   110
subsection{*Closure for Quine-Inspired Products and Sums*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   111
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   112
(*Quine ordered pairs*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   113
lemma QPair_in_quniv:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   114
    "[| a: quniv(A);  b: quniv(A) |] ==> <a;b> \<in> quniv(A)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   115
by (simp add: quniv_def QPair_def sum_subset_univ)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   116
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   117
lemma QSigma_quniv: "quniv(A) <*> quniv(A) \<subseteq> quniv(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   118
by (blast intro: QPair_in_quniv)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   119
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   120
lemmas QSigma_subset_quniv =  subset_trans [OF QSigma_mono QSigma_quniv]
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   121
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   122
(*The opposite inclusion*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   123
lemma quniv_QPair_D:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   124
    "<a;b> \<in> quniv(A) ==> a: quniv(A) & b: quniv(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   125
apply (unfold quniv_def QPair_def)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   126
apply (rule Transset_includes_summands [THEN conjE])
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   127
apply (rule Transset_eclose [THEN Transset_univ])
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   128
apply (erule PowD, blast)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   129
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   130
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   131
lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE]
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   132
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   133
lemma quniv_QPair_iff: "<a;b> \<in> quniv(A) \<longleftrightarrow> a: quniv(A) & b: quniv(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   134
by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   135
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   136
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   137
subsection{*Quine Disjoint Sum*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   138
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   139
lemma QInl_in_quniv: "a: quniv(A) ==> QInl(a) \<in> quniv(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   140
by (simp add: QInl_def zero_in_quniv QPair_in_quniv)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   141
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   142
lemma QInr_in_quniv: "b: quniv(A) ==> QInr(b) \<in> quniv(A)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   143
by (simp add: QInr_def one_in_quniv QPair_in_quniv)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   144
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   145
lemma qsum_quniv: "quniv(C) <+> quniv(C) \<subseteq> quniv(C)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   146
by (blast intro: QInl_in_quniv QInr_in_quniv)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   147
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   148
lemmas qsum_subset_quniv = subset_trans [OF qsum_mono qsum_quniv]
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   149
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   150
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   151
subsection{*The Natural Numbers*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   152
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   153
lemmas nat_subset_quniv =  subset_trans [OF nat_subset_univ univ_subset_quniv]
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   154
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   155
(* n:nat ==> n:quniv(A) *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   156
lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD]
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   157
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   158
lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv]
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   159
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   160
lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD]
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   161
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   162
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   163
(*Intersecting <a;b> with Vfrom...*)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   164
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   165
lemma QPair_Int_Vfrom_succ_subset:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   166
 "Transset(X) ==>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   167
       <a;b> \<inter> Vfrom(X, succ(i))  \<subseteq>  <a \<inter> Vfrom(X,i);  b \<inter> Vfrom(X,i)>"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   168
by (simp add: QPair_def sum_def Int_Un_distrib2 Un_mono
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   169
              product_Int_Vfrom_subset [THEN subset_trans]
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   170
              Sigma_mono [OF Int_lower1 subset_refl])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   171
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   172
subsection{*"Take-Lemma" Rules*}
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   173
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   174
(*for proving a=b by coinduction and c: quniv(A)*)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   175
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   176
(*Rule for level i -- preserving the level, not decreasing it*)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   177
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   178
lemma QPair_Int_Vfrom_subset:
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   179
 "Transset(X) ==>
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   180
       <a;b> \<inter> Vfrom(X,i)  \<subseteq>  <a \<inter> Vfrom(X,i);  b \<inter> Vfrom(X,i)>"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   181
apply (unfold QPair_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   182
apply (erule Transset_Vfrom [THEN Transset_sum_Int_subset])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   183
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   184
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   185
(*@{term"[| a \<inter> Vset(i) \<subseteq> c; b \<inter> Vset(i) \<subseteq> d |] ==> <a;b> \<inter> Vset(i) \<subseteq> <c;d>"}*)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   186
lemmas QPair_Int_Vset_subset_trans =
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   187
     subset_trans [OF Transset_0 [THEN QPair_Int_Vfrom_subset] QPair_mono]
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   188
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   189
lemma QPair_Int_Vset_subset_UN:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   190
     "Ord(i) ==> <a;b> \<inter> Vset(i) \<subseteq> (\<Union>j\<in>i. <a \<inter> Vset(j); b \<inter> Vset(j)>)"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   191
apply (erule Ord_cases)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   192
(*0 case*)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   193
apply (simp add: Vfrom_0)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   194
(*succ(j) case*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   195
apply (erule ssubst)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   196
apply (rule Transset_0 [THEN QPair_Int_Vfrom_succ_subset, THEN subset_trans])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   197
apply (rule succI1 [THEN UN_upper])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   198
(*Limit(i) case*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45602
diff changeset
   199
apply (simp del: UN_simps
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   200
        add: Limit_Vfrom_eq Int_UN_distrib UN_mono QPair_Int_Vset_subset_trans)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   201
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13220
diff changeset
   202
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
end