clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
authorwenzelm
Sun Apr 09 20:44:35 2017 +0200 (2017-04-09)
changeset 65449c82e63b11b8b
parent 65448 9bc3b57c1fa7
child 65450 b0a73039ddaa
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
src/Doc/Logics_ZF/ZF_Isar.thy
src/Doc/Logics_ZF/ZF_examples.thy
src/ZF/AC.thy
src/ZF/AC/AC_Equiv.thy
src/ZF/Coind/Language.thy
src/ZF/Coind/Map.thy
src/ZF/Constructible/Formula.thy
src/ZF/Constructible/MetaExists.thy
src/ZF/Constructible/Normal.thy
src/ZF/Constructible/Relative.thy
src/ZF/IMP/Com.thy
src/ZF/Induct/Acc.thy
src/ZF/Induct/Binary_Trees.thy
src/ZF/Induct/Brouwer.thy
src/ZF/Induct/Comb.thy
src/ZF/Induct/Datatypes.thy
src/ZF/Induct/FoldSet.thy
src/ZF/Induct/ListN.thy
src/ZF/Induct/Mutil.thy
src/ZF/Induct/Ntree.thy
src/ZF/Induct/Primrec.thy
src/ZF/Induct/PropLog.thy
src/ZF/Induct/Rmap.thy
src/ZF/Induct/Term.thy
src/ZF/Induct/Tree_Forest.thy
src/ZF/Main.thy
src/ZF/Main_ZF.thy
src/ZF/Main_ZFC.thy
src/ZF/ROOT
src/ZF/Resid/Redex.thy
src/ZF/UNITY/GenPrefix.thy
src/ZF/UNITY/State.thy
src/ZF/UNITY/WFair.thy
src/ZF/ZF.thy
src/ZF/ZFC.thy
src/ZF/ZF_Base.thy
src/ZF/ex/BinEx.thy
src/ZF/ex/CoUnit.thy
src/ZF/ex/Commutation.thy
src/ZF/ex/Group.thy
src/ZF/ex/LList.thy
src/ZF/ex/Limit.thy
src/ZF/ex/NatSum.thy
src/ZF/ex/Primes.thy
src/ZF/ex/Ramsey.thy
src/ZF/ex/misc.thy
src/ZF/upair.thy
     1.1 --- a/src/Doc/Logics_ZF/ZF_Isar.thy	Sun Apr 09 20:17:00 2017 +0200
     1.2 +++ b/src/Doc/Logics_ZF/ZF_Isar.thy	Sun Apr 09 20:44:35 2017 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  theory ZF_Isar
     1.5 -imports Main
     1.6 +imports ZF
     1.7  begin
     1.8  
     1.9  (*<*)
     2.1 --- a/src/Doc/Logics_ZF/ZF_examples.thy	Sun Apr 09 20:17:00 2017 +0200
     2.2 +++ b/src/Doc/Logics_ZF/ZF_examples.thy	Sun Apr 09 20:44:35 2017 +0200
     2.3 @@ -1,6 +1,6 @@
     2.4  section{*Examples of Reasoning in ZF Set Theory*}
     2.5  
     2.6 -theory ZF_examples imports Main_ZFC begin
     2.7 +theory ZF_examples imports ZFC begin
     2.8  
     2.9  subsection {* Binary Trees *}
    2.10  
     3.1 --- a/src/ZF/AC.thy	Sun Apr 09 20:17:00 2017 +0200
     3.2 +++ b/src/ZF/AC.thy	Sun Apr 09 20:44:35 2017 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  
     3.5  section\<open>The Axiom of Choice\<close>
     3.6  
     3.7 -theory AC imports Main_ZF begin
     3.8 +theory AC imports ZF begin
     3.9  
    3.10  text\<open>This definition comes from Halmos (1960), page 59.\<close>
    3.11  axiomatization where
     4.1 --- a/src/ZF/AC/AC_Equiv.thy	Sun Apr 09 20:17:00 2017 +0200
     4.2 +++ b/src/ZF/AC/AC_Equiv.thy	Sun Apr 09 20:44:35 2017 +0200
     4.3 @@ -12,8 +12,8 @@
     4.4  *)
     4.5  
     4.6  theory AC_Equiv
     4.7 -imports Main
     4.8 -begin (*obviously not Main_ZFC*)
     4.9 +imports ZF
    4.10 +begin (*obviously not ZFC*)
    4.11  
    4.12  (* Well Ordering Theorems *)
    4.13  
     5.1 --- a/src/ZF/Coind/Language.thy	Sun Apr 09 20:17:00 2017 +0200
     5.2 +++ b/src/ZF/Coind/Language.thy	Sun Apr 09 20:44:35 2017 +0200
     5.3 @@ -3,7 +3,7 @@
     5.4      Copyright   1995  University of Cambridge
     5.5  *)
     5.6  
     5.7 -theory Language imports Main begin
     5.8 +theory Language imports ZF begin
     5.9  
    5.10  
    5.11  text\<open>these really can't be definitions without losing the abstraction\<close>
     6.1 --- a/src/ZF/Coind/Map.thy	Sun Apr 09 20:17:00 2017 +0200
     6.2 +++ b/src/ZF/Coind/Map.thy	Sun Apr 09 20:44:35 2017 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  Some sample proofs of inclusions for the final coalgebra "U" (by lcp).
     6.5  *)
     6.6  
     6.7 -theory Map imports Main begin
     6.8 +theory Map imports ZF begin
     6.9  
    6.10  definition
    6.11    TMap :: "[i,i] => i"  where
     7.1 --- a/src/ZF/Constructible/Formula.thy	Sun Apr 09 20:17:00 2017 +0200
     7.2 +++ b/src/ZF/Constructible/Formula.thy	Sun Apr 09 20:44:35 2017 +0200
     7.3 @@ -4,7 +4,7 @@
     7.4  
     7.5  section \<open>First-Order Formulas and the Definition of the Class L\<close>
     7.6  
     7.7 -theory Formula imports Main begin
     7.8 +theory Formula imports ZF begin
     7.9  
    7.10  subsection\<open>Internalized formulas of FOL\<close>
    7.11  
     8.1 --- a/src/ZF/Constructible/MetaExists.thy	Sun Apr 09 20:17:00 2017 +0200
     8.2 +++ b/src/ZF/Constructible/MetaExists.thy	Sun Apr 09 20:44:35 2017 +0200
     8.3 @@ -4,7 +4,7 @@
     8.4  
     8.5  section\<open>The meta-existential quantifier\<close>
     8.6  
     8.7 -theory MetaExists imports Main begin
     8.8 +theory MetaExists imports ZF begin
     8.9  
    8.10  text\<open>Allows quantification over any term.  Used to quantify over classes.
    8.11  Yields a proposition rather than a FOL formula.\<close>
     9.1 --- a/src/ZF/Constructible/Normal.thy	Sun Apr 09 20:17:00 2017 +0200
     9.2 +++ b/src/ZF/Constructible/Normal.thy	Sun Apr 09 20:44:35 2017 +0200
     9.3 @@ -4,7 +4,7 @@
     9.4  
     9.5  section \<open>Closed Unbounded Classes and Normal Functions\<close>
     9.6  
     9.7 -theory Normal imports Main begin
     9.8 +theory Normal imports ZF begin
     9.9  
    9.10  text\<open>
    9.11  One source is the book
    10.1 --- a/src/ZF/Constructible/Relative.thy	Sun Apr 09 20:17:00 2017 +0200
    10.2 +++ b/src/ZF/Constructible/Relative.thy	Sun Apr 09 20:44:35 2017 +0200
    10.3 @@ -4,7 +4,7 @@
    10.4  
    10.5  section \<open>Relativization and Absoluteness\<close>
    10.6  
    10.7 -theory Relative imports Main begin
    10.8 +theory Relative imports ZF begin
    10.9  
   10.10  subsection\<open>Relativized versions of standard set-theoretic concepts\<close>
   10.11  
   10.12 @@ -593,13 +593,13 @@
   10.13  
   10.14  lemma (in M_trivial) pair_abs [simp]:
   10.15       "M(z) ==> pair(M,a,b,z) \<longleftrightarrow> z=<a,b>"
   10.16 -apply (simp add: pair_def ZF.Pair_def)
   10.17 +apply (simp add: pair_def Pair_def)
   10.18  apply (blast intro: transM)
   10.19  done
   10.20  
   10.21  lemma (in M_trivial) pair_in_M_iff [iff]:
   10.22       "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
   10.23 -by (simp add: ZF.Pair_def)
   10.24 +by (simp add: Pair_def)
   10.25  
   10.26  lemma (in M_trivial) pair_components_in_M:
   10.27       "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
    11.1 --- a/src/ZF/IMP/Com.thy	Sun Apr 09 20:17:00 2017 +0200
    11.2 +++ b/src/ZF/IMP/Com.thy	Sun Apr 09 20:44:35 2017 +0200
    11.3 @@ -4,7 +4,7 @@
    11.4  
    11.5  section \<open>Arithmetic expressions, boolean expressions, commands\<close>
    11.6  
    11.7 -theory Com imports Main begin
    11.8 +theory Com imports ZF begin
    11.9  
   11.10  
   11.11  subsection \<open>Arithmetic expressions\<close>
    12.1 --- a/src/ZF/Induct/Acc.thy	Sun Apr 09 20:17:00 2017 +0200
    12.2 +++ b/src/ZF/Induct/Acc.thy	Sun Apr 09 20:44:35 2017 +0200
    12.3 @@ -5,7 +5,7 @@
    12.4  
    12.5  section \<open>The accessible part of a relation\<close>
    12.6  
    12.7 -theory Acc imports Main begin
    12.8 +theory Acc imports ZF begin
    12.9  
   12.10  text \<open>
   12.11    Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}.
    13.1 --- a/src/ZF/Induct/Binary_Trees.thy	Sun Apr 09 20:17:00 2017 +0200
    13.2 +++ b/src/ZF/Induct/Binary_Trees.thy	Sun Apr 09 20:44:35 2017 +0200
    13.3 @@ -5,7 +5,7 @@
    13.4  
    13.5  section \<open>Binary trees\<close>
    13.6  
    13.7 -theory Binary_Trees imports Main begin
    13.8 +theory Binary_Trees imports ZF begin
    13.9  
   13.10  subsection \<open>Datatype definition\<close>
   13.11  
    14.1 --- a/src/ZF/Induct/Brouwer.thy	Sun Apr 09 20:17:00 2017 +0200
    14.2 +++ b/src/ZF/Induct/Brouwer.thy	Sun Apr 09 20:44:35 2017 +0200
    14.3 @@ -5,7 +5,7 @@
    14.4  
    14.5  section \<open>Infinite branching datatype definitions\<close>
    14.6  
    14.7 -theory Brouwer imports Main_ZFC begin
    14.8 +theory Brouwer imports ZFC begin
    14.9  
   14.10  subsection \<open>The Brouwer ordinals\<close>
   14.11  
    15.1 --- a/src/ZF/Induct/Comb.thy	Sun Apr 09 20:17:00 2017 +0200
    15.2 +++ b/src/ZF/Induct/Comb.thy	Sun Apr 09 20:44:35 2017 +0200
    15.3 @@ -6,7 +6,7 @@
    15.4  section \<open>Combinatory Logic example: the Church-Rosser Theorem\<close>
    15.5  
    15.6  theory Comb
    15.7 -imports Main
    15.8 +imports ZF
    15.9  begin
   15.10  
   15.11  text \<open>
    16.1 --- a/src/ZF/Induct/Datatypes.thy	Sun Apr 09 20:17:00 2017 +0200
    16.2 +++ b/src/ZF/Induct/Datatypes.thy	Sun Apr 09 20:44:35 2017 +0200
    16.3 @@ -5,7 +5,7 @@
    16.4  
    16.5  section \<open>Sample datatype definitions\<close>
    16.6  
    16.7 -theory Datatypes imports Main begin
    16.8 +theory Datatypes imports ZF begin
    16.9  
   16.10  subsection \<open>A type with four constructors\<close>
   16.11  
    17.1 --- a/src/ZF/Induct/FoldSet.thy	Sun Apr 09 20:17:00 2017 +0200
    17.2 +++ b/src/ZF/Induct/FoldSet.thy	Sun Apr 09 20:44:35 2017 +0200
    17.3 @@ -6,7 +6,7 @@
    17.4  least left-commutative.  
    17.5  *)
    17.6  
    17.7 -theory FoldSet imports Main begin
    17.8 +theory FoldSet imports ZF begin
    17.9  
   17.10  consts fold_set :: "[i, i, [i,i]=>i, i] => i"
   17.11  
    18.1 --- a/src/ZF/Induct/ListN.thy	Sun Apr 09 20:17:00 2017 +0200
    18.2 +++ b/src/ZF/Induct/ListN.thy	Sun Apr 09 20:44:35 2017 +0200
    18.3 @@ -5,7 +5,7 @@
    18.4  
    18.5  section \<open>Lists of n elements\<close>
    18.6  
    18.7 -theory ListN imports Main begin
    18.8 +theory ListN imports ZF begin
    18.9  
   18.10  text \<open>
   18.11    Inductive definition of lists of \<open>n\<close> elements; see
    19.1 --- a/src/ZF/Induct/Mutil.thy	Sun Apr 09 20:17:00 2017 +0200
    19.2 +++ b/src/ZF/Induct/Mutil.thy	Sun Apr 09 20:44:35 2017 +0200
    19.3 @@ -5,7 +5,7 @@
    19.4  
    19.5  section \<open>The Mutilated Chess Board Problem, formalized inductively\<close>
    19.6  
    19.7 -theory Mutil imports Main begin
    19.8 +theory Mutil imports ZF begin
    19.9  
   19.10  text \<open>
   19.11    Originator is Max Black, according to J A Robinson.  Popularized as
    20.1 --- a/src/ZF/Induct/Ntree.thy	Sun Apr 09 20:17:00 2017 +0200
    20.2 +++ b/src/ZF/Induct/Ntree.thy	Sun Apr 09 20:44:35 2017 +0200
    20.3 @@ -5,7 +5,7 @@
    20.4  
    20.5  section \<open>Datatype definition n-ary branching trees\<close>
    20.6  
    20.7 -theory Ntree imports Main begin
    20.8 +theory Ntree imports ZF begin
    20.9  
   20.10  text \<open>
   20.11    Demonstrates a simple use of function space in a datatype
    21.1 --- a/src/ZF/Induct/Primrec.thy	Sun Apr 09 20:17:00 2017 +0200
    21.2 +++ b/src/ZF/Induct/Primrec.thy	Sun Apr 09 20:44:35 2017 +0200
    21.3 @@ -5,7 +5,7 @@
    21.4  
    21.5  section \<open>Primitive Recursive Functions: the inductive definition\<close>
    21.6  
    21.7 -theory Primrec imports Main begin
    21.8 +theory Primrec imports ZF begin
    21.9  
   21.10  text \<open>
   21.11    Proof adopted from @{cite szasz93}.
    22.1 --- a/src/ZF/Induct/PropLog.thy	Sun Apr 09 20:17:00 2017 +0200
    22.2 +++ b/src/ZF/Induct/PropLog.thy	Sun Apr 09 20:44:35 2017 +0200
    22.3 @@ -5,7 +5,7 @@
    22.4  
    22.5  section \<open>Meta-theory of propositional logic\<close>
    22.6  
    22.7 -theory PropLog imports Main begin
    22.8 +theory PropLog imports ZF begin
    22.9  
   22.10  text \<open>
   22.11    Datatype definition of propositional logic formulae and inductive
    23.1 --- a/src/ZF/Induct/Rmap.thy	Sun Apr 09 20:17:00 2017 +0200
    23.2 +++ b/src/ZF/Induct/Rmap.thy	Sun Apr 09 20:44:35 2017 +0200
    23.3 @@ -5,7 +5,7 @@
    23.4  
    23.5  section \<open>An operator to ``map'' a relation over a list\<close>
    23.6  
    23.7 -theory Rmap imports Main begin
    23.8 +theory Rmap imports ZF begin
    23.9  
   23.10  consts
   23.11    rmap :: "i=>i"
    24.1 --- a/src/ZF/Induct/Term.thy	Sun Apr 09 20:17:00 2017 +0200
    24.2 +++ b/src/ZF/Induct/Term.thy	Sun Apr 09 20:44:35 2017 +0200
    24.3 @@ -5,7 +5,7 @@
    24.4  
    24.5  section \<open>Terms over an alphabet\<close>
    24.6  
    24.7 -theory Term imports Main begin
    24.8 +theory Term imports ZF begin
    24.9  
   24.10  text \<open>
   24.11    Illustrates the list functor (essentially the same type as in \<open>Trees_Forest\<close>).
    25.1 --- a/src/ZF/Induct/Tree_Forest.thy	Sun Apr 09 20:17:00 2017 +0200
    25.2 +++ b/src/ZF/Induct/Tree_Forest.thy	Sun Apr 09 20:44:35 2017 +0200
    25.3 @@ -5,7 +5,7 @@
    25.4  
    25.5  section \<open>Trees and forests, a mutually recursive type definition\<close>
    25.6  
    25.7 -theory Tree_Forest imports Main begin
    25.8 +theory Tree_Forest imports ZF begin
    25.9  
   25.10  subsection \<open>Datatype definition\<close>
   25.11  
    26.1 --- a/src/ZF/Main.thy	Sun Apr 09 20:17:00 2017 +0200
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,5 +0,0 @@
    26.4 -theory Main 
    26.5 -imports Main_ZF
    26.6 -begin
    26.7 -
    26.8 -end
    27.1 --- a/src/ZF/Main_ZF.thy	Sun Apr 09 20:17:00 2017 +0200
    27.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.3 @@ -1,73 +0,0 @@
    27.4 -section\<open>Theory Main: Everything Except AC\<close>
    27.5 -
    27.6 -theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin
    27.7 -
    27.8 -(*The theory of "iterates" logically belongs to Nat, but can't go there because
    27.9 -  primrec isn't available into after Datatype.*)
   27.10 -
   27.11 -subsection\<open>Iteration of the function @{term F}\<close>
   27.12 -
   27.13 -consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
   27.14 -
   27.15 -primrec
   27.16 -    "F^0 (x) = x"
   27.17 -    "F^(succ(n)) (x) = F(F^n (x))"
   27.18 -
   27.19 -definition
   27.20 -  iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) where
   27.21 -    "F^\<omega> (x) == \<Union>n\<in>nat. F^n (x)"
   27.22 -
   27.23 -lemma iterates_triv:
   27.24 -     "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"
   27.25 -by (induct n rule: nat_induct, simp_all)
   27.26 -
   27.27 -lemma iterates_type [TC]:
   27.28 -     "[| n \<in> nat;  a \<in> A; !!x. x \<in> A ==> F(x) \<in> A |]
   27.29 -      ==> F^n (a) \<in> A"
   27.30 -by (induct n rule: nat_induct, simp_all)
   27.31 -
   27.32 -lemma iterates_omega_triv:
   27.33 -    "F(x) = x ==> F^\<omega> (x) = x"
   27.34 -by (simp add: iterates_omega_def iterates_triv)
   27.35 -
   27.36 -lemma Ord_iterates [simp]:
   27.37 -     "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |]
   27.38 -      ==> Ord(F^n (x))"
   27.39 -by (induct n rule: nat_induct, simp_all)
   27.40 -
   27.41 -lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
   27.42 -by (induct_tac n, simp_all)
   27.43 -
   27.44 -
   27.45 -subsection\<open>Transfinite Recursion\<close>
   27.46 -
   27.47 -text\<open>Transfinite recursion for definitions based on the
   27.48 -    three cases of ordinals\<close>
   27.49 -
   27.50 -definition
   27.51 -  transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where
   27.52 -    "transrec3(k, a, b, c) ==
   27.53 -       transrec(k, \<lambda>x r.
   27.54 -         if x=0 then a
   27.55 -         else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
   27.56 -         else b(Arith.pred(x), r ` Arith.pred(x)))"
   27.57 -
   27.58 -lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
   27.59 -by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
   27.60 -
   27.61 -lemma transrec3_succ [simp]:
   27.62 -     "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
   27.63 -by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
   27.64 -
   27.65 -lemma transrec3_Limit:
   27.66 -     "Limit(i) ==>
   27.67 -      transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
   27.68 -by (rule transrec3_def [THEN def_transrec, THEN trans], force)
   27.69 -
   27.70 -
   27.71 -declaration \<open>fn _ =>
   27.72 -  Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
   27.73 -    map mk_eq o Ord_atomize o Variable.gen_all ctxt))
   27.74 -\<close>
   27.75 -
   27.76 -end
    28.1 --- a/src/ZF/Main_ZFC.thy	Sun Apr 09 20:17:00 2017 +0200
    28.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.3 @@ -1,4 +0,0 @@
    28.4 -theory Main_ZFC imports Main_ZF InfDatatype
    28.5 -begin
    28.6 -
    28.7 -end
    29.1 --- a/src/ZF/ROOT	Sun Apr 09 20:17:00 2017 +0200
    29.2 +++ b/src/ZF/ROOT	Sun Apr 09 20:44:35 2017 +0200
    29.3 @@ -43,8 +43,7 @@
    29.4      (North-Holland, 1980)
    29.5    *}
    29.6    theories
    29.7 -    Main
    29.8 -    Main_ZFC
    29.9 +    ZFC
   29.10    document_files "root.tex"
   29.11  
   29.12  session "ZF-AC" (ZF) in AC = ZF +
    30.1 --- a/src/ZF/Resid/Redex.thy	Sun Apr 09 20:17:00 2017 +0200
    30.2 +++ b/src/ZF/Resid/Redex.thy	Sun Apr 09 20:44:35 2017 +0200
    30.3 @@ -2,7 +2,7 @@
    30.4      Author:     Ole Rasmussen, University of Cambridge
    30.5  *)
    30.6  
    30.7 -theory Redex imports Main begin
    30.8 +theory Redex imports ZF begin
    30.9  consts
   30.10    redexes     :: i
   30.11  
    31.1 --- a/src/ZF/UNITY/GenPrefix.thy	Sun Apr 09 20:17:00 2017 +0200
    31.2 +++ b/src/ZF/UNITY/GenPrefix.thy	Sun Apr 09 20:44:35 2017 +0200
    31.3 @@ -12,7 +12,7 @@
    31.4  section\<open>Charpentier's Generalized Prefix Relation\<close>
    31.5  
    31.6  theory GenPrefix
    31.7 -imports Main
    31.8 +imports ZF
    31.9  begin
   31.10  
   31.11  definition (*really belongs in ZF/Trancl*)
    32.1 --- a/src/ZF/UNITY/State.thy	Sun Apr 09 20:17:00 2017 +0200
    32.2 +++ b/src/ZF/UNITY/State.thy	Sun Apr 09 20:44:35 2017 +0200
    32.3 @@ -10,7 +10,7 @@
    32.4  
    32.5  section\<open>UNITY Program States\<close>
    32.6  
    32.7 -theory State imports Main begin
    32.8 +theory State imports ZF begin
    32.9  
   32.10  consts var :: i
   32.11  datatype var = Var("i \<in> list(nat)")
    33.1 --- a/src/ZF/UNITY/WFair.thy	Sun Apr 09 20:17:00 2017 +0200
    33.2 +++ b/src/ZF/UNITY/WFair.thy	Sun Apr 09 20:44:35 2017 +0200
    33.3 @@ -6,7 +6,7 @@
    33.4  section\<open>Progress under Weak Fairness\<close>
    33.5  
    33.6  theory WFair
    33.7 -imports UNITY Main_ZFC
    33.8 +imports UNITY ZFC
    33.9  begin
   33.10  
   33.11  text\<open>This theory defines the operators transient, ensures and leadsTo,
    34.1 --- a/src/ZF/ZF.thy	Sun Apr 09 20:17:00 2017 +0200
    34.2 +++ b/src/ZF/ZF.thy	Sun Apr 09 20:44:35 2017 +0200
    34.3 @@ -1,650 +1,73 @@
    34.4 -(*  Title:      ZF/ZF.thy
    34.5 -    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
    34.6 -    Copyright   1993  University of Cambridge
    34.7 -*)
    34.8 -
    34.9 -section \<open>Zermelo-Fraenkel Set Theory\<close>
   34.10 -
   34.11 -theory ZF
   34.12 -imports "~~/src/FOL/FOL"
   34.13 -begin
   34.14 -
   34.15 -subsection \<open>Signature\<close>
   34.16 -
   34.17 -declare [[eta_contract = false]]
   34.18 +section\<open>Theory Main: Everything Except AC\<close>
   34.19  
   34.20 -typedecl i
   34.21 -instance i :: "term" ..
   34.22 -
   34.23 -axiomatization mem :: "[i, i] \<Rightarrow> o"  (infixl "\<in>" 50)  \<comment> \<open>membership relation\<close>
   34.24 -  and zero :: "i"  ("0")  \<comment> \<open>the empty set\<close>
   34.25 -  and Pow :: "i \<Rightarrow> i"  \<comment> \<open>power sets\<close>
   34.26 -  and Inf :: "i"  \<comment> \<open>infinite set\<close>
   34.27 -  and Union :: "i \<Rightarrow> i"  ("\<Union>_" [90] 90)
   34.28 -  and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
   34.29 -
   34.30 -abbreviation not_mem :: "[i, i] \<Rightarrow> o"  (infixl "\<notin>" 50)  \<comment> \<open>negated membership relation\<close>
   34.31 -  where "x \<notin> y \<equiv> \<not> (x \<in> y)"
   34.32 -
   34.33 -
   34.34 -subsection \<open>Bounded Quantifiers\<close>
   34.35 -
   34.36 -definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
   34.37 -  where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)"
   34.38 +theory ZF imports List_ZF IntDiv_ZF CardinalArith begin
   34.39  
   34.40 -definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
   34.41 -  where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
   34.42 -
   34.43 -syntax
   34.44 -  "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<forall>_\<in>_./ _)" 10)
   34.45 -  "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<exists>_\<in>_./ _)" 10)
   34.46 -translations
   34.47 -  "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
   34.48 -  "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
   34.49 -
   34.50 -
   34.51 -subsection \<open>Variations on Replacement\<close>
   34.52 +(*The theory of "iterates" logically belongs to Nat, but can't go there because
   34.53 +  primrec isn't available into after Datatype.*)
   34.54  
   34.55 -(* Derived form of replacement, restricting P to its functional part.
   34.56 -   The resulting set (for functional P) is the same as with
   34.57 -   PrimReplace, but the rules are simpler. *)
   34.58 -definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
   34.59 -  where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
   34.60 -
   34.61 -syntax
   34.62 -  "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
   34.63 -translations
   34.64 -  "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
   34.65 -
   34.66 -
   34.67 -(* Functional form of replacement -- analgous to ML's map functional *)
   34.68 -
   34.69 -definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
   34.70 -  where "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
   34.71 -
   34.72 -syntax
   34.73 -  "_RepFun" :: "[i, pttrn, i] => i"  ("(1{_ ./ _ \<in> _})" [51,0,51])
   34.74 -translations
   34.75 -  "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
   34.76 -
   34.77 +subsection\<open>Iteration of the function @{term F}\<close>
   34.78  
   34.79 -(* Separation and Pairing can be derived from the Replacement
   34.80 -   and Powerset Axioms using the following definitions. *)
   34.81 -definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i"
   34.82 -  where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
   34.83 -
   34.84 -syntax
   34.85 -  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  ("(1{_ \<in> _ ./ _})")
   34.86 -translations
   34.87 -  "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
   34.88 -
   34.89 -
   34.90 -subsection \<open>General union and intersection\<close>
   34.91 -
   34.92 -definition Inter :: "i => i"  ("\<Inter>_" [90] 90)
   34.93 -  where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
   34.94 -
   34.95 -syntax
   34.96 -  "_UNION" :: "[pttrn, i, i] => i"  ("(3\<Union>_\<in>_./ _)" 10)
   34.97 -  "_INTER" :: "[pttrn, i, i] => i"  ("(3\<Inter>_\<in>_./ _)" 10)
   34.98 -translations
   34.99 -  "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
  34.100 -  "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
  34.101 -
  34.102 -
  34.103 -subsection \<open>Finite sets and binary operations\<close>
  34.104 -
  34.105 -(*Unordered pairs (Upair) express binary union/intersection and cons;
  34.106 -  set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
  34.107 -
  34.108 -definition Upair :: "[i, i] => i"
  34.109 -  where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
  34.110 -
  34.111 -definition Subset :: "[i, i] \<Rightarrow> o"  (infixl "\<subseteq>" 50)  \<comment> \<open>subset relation\<close>
  34.112 -  where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B"
  34.113 +consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
  34.114  
  34.115 -definition Diff :: "[i, i] \<Rightarrow> i"  (infixl "-" 65)  \<comment> \<open>set difference\<close>
  34.116 -  where "A - B == { x\<in>A . ~(x\<in>B) }"
  34.117 -
  34.118 -definition Un :: "[i, i] \<Rightarrow> i"  (infixl "\<union>" 65)  \<comment> \<open>binary union\<close>
  34.119 -  where "A \<union> B == \<Union>(Upair(A,B))"
  34.120 -
  34.121 -definition Int :: "[i, i] \<Rightarrow> i"  (infixl "\<inter>" 70)  \<comment> \<open>binary intersection\<close>
  34.122 -  where "A \<inter> B == \<Inter>(Upair(A,B))"
  34.123 -
  34.124 -definition cons :: "[i, i] => i"
  34.125 -  where "cons(a,A) == Upair(a,a) \<union> A"
  34.126 -
  34.127 -definition succ :: "i => i"
  34.128 -  where "succ(i) == cons(i, i)"
  34.129 +primrec
  34.130 +    "F^0 (x) = x"
  34.131 +    "F^(succ(n)) (x) = F(F^n (x))"
  34.132  
  34.133 -nonterminal "is"
  34.134 -syntax
  34.135 -  "" :: "i \<Rightarrow> is"  ("_")
  34.136 -  "_Enum" :: "[i, is] \<Rightarrow> is"  ("_,/ _")
  34.137 -  "_Finset" :: "is \<Rightarrow> i"  ("{(_)}")
  34.138 -translations
  34.139 -  "{x, xs}" == "CONST cons(x, {xs})"
  34.140 -  "{x}" == "CONST cons(x, 0)"
  34.141 -
  34.142 -
  34.143 -subsection \<open>Axioms\<close>
  34.144 -
  34.145 -(* ZF axioms -- see Suppes p.238
  34.146 -   Axioms for Union, Pow and Replace state existence only,
  34.147 -   uniqueness is derivable using extensionality. *)
  34.148 -
  34.149 -axiomatization
  34.150 -where
  34.151 -  extension:     "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and
  34.152 -  Union_iff:     "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and
  34.153 -  Pow_iff:       "A \<in> Pow(B) \<longleftrightarrow> A \<subseteq> B" and
  34.154 -
  34.155 -  (*We may name this set, though it is not uniquely defined.*)
  34.156 -  infinity:      "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and
  34.157 +definition
  34.158 +  iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) where
  34.159 +    "F^\<omega> (x) == \<Union>n\<in>nat. F^n (x)"
  34.160  
  34.161 -  (*This formulation facilitates case analysis on A.*)
  34.162 -  foundation:    "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and
  34.163 -
  34.164 -  (*Schema axiom since predicate P is a higher-order variable*)
  34.165 -  replacement:   "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow>
  34.166 -                         b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))"
  34.167 -
  34.168 -
  34.169 -subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>
  34.170 -
  34.171 -definition The :: "(i \<Rightarrow> o) \<Rightarrow> i"  (binder "THE " 10)
  34.172 -  where the_def: "The(P)    == \<Union>({y . x \<in> {0}, P(y)})"
  34.173 -
  34.174 -definition If :: "[o, i, i] \<Rightarrow> i"  ("(if (_)/ then (_)/ else (_))" [10] 10)
  34.175 -  where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b"
  34.176 -
  34.177 -abbreviation (input)
  34.178 -  old_if :: "[o, i, i] => i"  ("if '(_,_,_')")
  34.179 -  where "if(P,a,b) == If(P,a,b)"
  34.180 -
  34.181 -
  34.182 -subsection \<open>Ordered Pairing\<close>
  34.183 -
  34.184 -(* this "symmetric" definition works better than {{a}, {a,b}} *)
  34.185 -definition Pair :: "[i, i] => i"
  34.186 -  where "Pair(a,b) == {{a,a}, {a,b}}"
  34.187 -
  34.188 -definition fst :: "i \<Rightarrow> i"
  34.189 -  where "fst(p) == THE a. \<exists>b. p = Pair(a, b)"
  34.190 -
  34.191 -definition snd :: "i \<Rightarrow> i"
  34.192 -  where "snd(p) == THE b. \<exists>a. p = Pair(a, b)"
  34.193 +lemma iterates_triv:
  34.194 +     "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"
  34.195 +by (induct n rule: nat_induct, simp_all)
  34.196  
  34.197 -definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>
  34.198 -  where "split(c) == \<lambda>p. c(fst(p), snd(p))"
  34.199 -
  34.200 -(* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
  34.201 -nonterminal patterns
  34.202 -syntax
  34.203 -  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
  34.204 -  ""          :: "pttrn => patterns"         ("_")
  34.205 -  "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
  34.206 -  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
  34.207 -translations
  34.208 -  "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
  34.209 -  "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
  34.210 -  "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
  34.211 -  "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"
  34.212 -
  34.213 -definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
  34.214 -  where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
  34.215 -
  34.216 -abbreviation cart_prod :: "[i, i] => i"  (infixr "\<times>" 80)  \<comment> \<open>Cartesian product\<close>
  34.217 -  where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
  34.218 -
  34.219 -
  34.220 -subsection \<open>Relations and Functions\<close>
  34.221 -
  34.222 -(*converse of relation r, inverse of function*)
  34.223 -definition converse :: "i \<Rightarrow> i"
  34.224 -  where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}"
  34.225 -
  34.226 -definition domain :: "i \<Rightarrow> i"
  34.227 -  where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}"
  34.228 -
  34.229 -definition range :: "i \<Rightarrow> i"
  34.230 -  where "range(r) == domain(converse(r))"
  34.231 -
  34.232 -definition field :: "i \<Rightarrow> i"
  34.233 -  where "field(r) == domain(r) \<union> range(r)"
  34.234 +lemma iterates_type [TC]:
  34.235 +     "[| n \<in> nat;  a \<in> A; !!x. x \<in> A ==> F(x) \<in> A |]
  34.236 +      ==> F^n (a) \<in> A"
  34.237 +by (induct n rule: nat_induct, simp_all)
  34.238  
  34.239 -definition relation :: "i \<Rightarrow> o"  \<comment> \<open>recognizes sets of pairs\<close>
  34.240 -  where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>"
  34.241 -
  34.242 -definition "function" :: "i \<Rightarrow> o"  \<comment> \<open>recognizes functions; can have non-pairs\<close>
  34.243 -  where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
  34.244 -
  34.245 -definition Image :: "[i, i] \<Rightarrow> i"  (infixl "``" 90)  \<comment> \<open>image\<close>
  34.246 -  where image_def: "r `` A  == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}"
  34.247 -
  34.248 -definition vimage :: "[i, i] \<Rightarrow> i"  (infixl "-``" 90)  \<comment> \<open>inverse image\<close>
  34.249 -  where vimage_def: "r -`` A == converse(r)``A"
  34.250 -
  34.251 -(* Restrict the relation r to the domain A *)
  34.252 -definition restrict :: "[i, i] \<Rightarrow> i"
  34.253 -  where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}"
  34.254 -
  34.255 -
  34.256 -(* Abstraction, application and Cartesian product of a family of sets *)
  34.257 -
  34.258 -definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
  34.259 -  where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}"
  34.260 -
  34.261 -definition "apply" :: "[i, i] \<Rightarrow> i"  (infixl "`" 90)  \<comment> \<open>function application\<close>
  34.262 -  where "f`a == \<Union>(f``{a})"
  34.263 -
  34.264 -definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
  34.265 -  where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}"
  34.266 -
  34.267 -abbreviation function_space :: "[i, i] \<Rightarrow> i"  (infixr "->" 60)  \<comment> \<open>function space\<close>
  34.268 -  where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
  34.269 -
  34.270 -
  34.271 -(* binder syntax *)
  34.272 +lemma iterates_omega_triv:
  34.273 +    "F(x) = x ==> F^\<omega> (x) = x"
  34.274 +by (simp add: iterates_omega_def iterates_triv)
  34.275  
  34.276 -syntax
  34.277 -  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Prod>_\<in>_./ _)" 10)
  34.278 -  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sum>_\<in>_./ _)" 10)
  34.279 -  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
  34.280 -translations
  34.281 -  "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
  34.282 -  "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
  34.283 -  "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"
  34.284 -
  34.285 -
  34.286 -subsection \<open>ASCII syntax\<close>
  34.287 -
  34.288 -notation (ASCII)
  34.289 -  cart_prod       (infixr "*" 80) and
  34.290 -  Int             (infixl "Int" 70) and
  34.291 -  Un              (infixl "Un" 65) and
  34.292 -  function_space  (infixr "\<rightarrow>" 60) and
  34.293 -  Subset          (infixl "<=" 50) and
  34.294 -  mem             (infixl ":" 50) and
  34.295 -  not_mem         (infixl "~:" 50)
  34.296 +lemma Ord_iterates [simp]:
  34.297 +     "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |]
  34.298 +      ==> Ord(F^n (x))"
  34.299 +by (induct n rule: nat_induct, simp_all)
  34.300  
  34.301 -syntax (ASCII)
  34.302 -  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
  34.303 -  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
  34.304 -  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
  34.305 -  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
  34.306 -  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
  34.307 -  "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
  34.308 -  "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
  34.309 -  "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
  34.310 -  "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
  34.311 -  "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
  34.312 -  "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
  34.313 -  "_pattern"  :: "patterns => pttrn"         ("<_>")
  34.314 -
  34.315 -
  34.316 -subsection \<open>Substitution\<close>
  34.317 -
  34.318 -(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
  34.319 -lemma subst_elem: "[| b\<in>A;  a=b |] ==> a\<in>A"
  34.320 -by (erule ssubst, assumption)
  34.321 +lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
  34.322 +by (induct_tac n, simp_all)
  34.323  
  34.324  
  34.325 -subsection\<open>Bounded universal quantifier\<close>
  34.326 -
  34.327 -lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)"
  34.328 -by (simp add: Ball_def)
  34.329 -
  34.330 -lemmas strip = impI allI ballI
  34.331 -
  34.332 -lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x);  x: A |] ==> P(x)"
  34.333 -by (simp add: Ball_def)
  34.334 -
  34.335 -(*Instantiates x first: better for automatic theorem proving?*)
  34.336 -lemma rev_ballE [elim]:
  34.337 -    "[| \<forall>x\<in>A. P(x);  x\<notin>A ==> Q;  P(x) ==> Q |] ==> Q"
  34.338 -by (simp add: Ball_def, blast)
  34.339 -
  34.340 -lemma ballE: "[| \<forall>x\<in>A. P(x);  P(x) ==> Q;  x\<notin>A ==> Q |] ==> Q"
  34.341 -by blast
  34.342 -
  34.343 -(*Used in the datatype package*)
  34.344 -lemma rev_bspec: "[| x: A;  \<forall>x\<in>A. P(x) |] ==> P(x)"
  34.345 -by (simp add: Ball_def)
  34.346 -
  34.347 -(*Trival rewrite rule;   @{term"(\<forall>x\<in>A.P)<->P"} holds only if A is nonempty!*)
  34.348 -lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<longrightarrow> P)"
  34.349 -by (simp add: Ball_def)
  34.350 -
  34.351 -(*Congruence rule for rewriting*)
  34.352 -lemma ball_cong [cong]:
  34.353 -    "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))"
  34.354 -by (simp add: Ball_def)
  34.355 -
  34.356 -lemma atomize_ball:
  34.357 -    "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"
  34.358 -  by (simp only: Ball_def atomize_all atomize_imp)
  34.359 -
  34.360 -lemmas [symmetric, rulify] = atomize_ball
  34.361 -  and [symmetric, defn] = atomize_ball
  34.362 -
  34.363 -
  34.364 -subsection\<open>Bounded existential quantifier\<close>
  34.365 +subsection\<open>Transfinite Recursion\<close>
  34.366  
  34.367 -lemma bexI [intro]: "[| P(x);  x: A |] ==> \<exists>x\<in>A. P(x)"
  34.368 -by (simp add: Bex_def, blast)
  34.369 -
  34.370 -(*The best argument order when there is only one @{term"x\<in>A"}*)
  34.371 -lemma rev_bexI: "[| x\<in>A;  P(x) |] ==> \<exists>x\<in>A. P(x)"
  34.372 -by blast
  34.373 -
  34.374 -(*Not of the general form for such rules. The existential quanitifer becomes universal. *)
  34.375 -lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a);  a: A |] ==> \<exists>x\<in>A. P(x)"
  34.376 -by blast
  34.377 -
  34.378 -lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x);  !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q"
  34.379 -by (simp add: Bex_def, blast)
  34.380 -
  34.381 -(*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty!!*)
  34.382 -lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)"
  34.383 -by (simp add: Bex_def)
  34.384 -
  34.385 -lemma bex_cong [cong]:
  34.386 -    "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |]
  34.387 -     ==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))"
  34.388 -by (simp add: Bex_def cong: conj_cong)
  34.389 -
  34.390 -
  34.391 -
  34.392 -subsection\<open>Rules for subsets\<close>
  34.393 -
  34.394 -lemma subsetI [intro!]:
  34.395 -    "(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B"
  34.396 -by (simp add: subset_def)
  34.397 -
  34.398 -(*Rule in Modus Ponens style [was called subsetE] *)
  34.399 -lemma subsetD [elim]: "[| A \<subseteq> B;  c\<in>A |] ==> c\<in>B"
  34.400 -apply (unfold subset_def)
  34.401 -apply (erule bspec, assumption)
  34.402 -done
  34.403 -
  34.404 -(*Classical elimination rule*)
  34.405 -lemma subsetCE [elim]:
  34.406 -    "[| A \<subseteq> B;  c\<notin>A ==> P;  c\<in>B ==> P |] ==> P"
  34.407 -by (simp add: subset_def, blast)
  34.408 +text\<open>Transfinite recursion for definitions based on the
  34.409 +    three cases of ordinals\<close>
  34.410  
  34.411 -(*Sometimes useful with premises in this order*)
  34.412 -lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B"
  34.413 -by blast
  34.414 -
  34.415 -lemma contra_subsetD: "[| A \<subseteq> B; c \<notin> B |] ==> c \<notin> A"
  34.416 -by blast
  34.417 -
  34.418 -lemma rev_contra_subsetD: "[| c \<notin> B;  A \<subseteq> B |] ==> c \<notin> A"
  34.419 -by blast
  34.420 -
  34.421 -lemma subset_refl [simp]: "A \<subseteq> A"
  34.422 -by blast
  34.423 -
  34.424 -lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"
  34.425 -by blast
  34.426 -
  34.427 -(*Useful for proving A<=B by rewriting in some cases*)
  34.428 -lemma subset_iff:
  34.429 -     "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
  34.430 -apply (unfold subset_def Ball_def)
  34.431 -apply (rule iff_refl)
  34.432 -done
  34.433 -
  34.434 -text\<open>For calculations\<close>
  34.435 -declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]
  34.436 -
  34.437 -
  34.438 -subsection\<open>Rules for equality\<close>
  34.439 -
  34.440 -(*Anti-symmetry of the subset relation*)
  34.441 -lemma equalityI [intro]: "[| A \<subseteq> B;  B \<subseteq> A |] ==> A = B"
  34.442 -by (rule extension [THEN iffD2], rule conjI)
  34.443 -
  34.444 -
  34.445 -lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B"
  34.446 -by (rule equalityI, blast+)
  34.447 -
  34.448 -lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1]
  34.449 -lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]
  34.450 -
  34.451 -lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
  34.452 -by (blast dest: equalityD1 equalityD2)
  34.453 +definition
  34.454 +  transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where
  34.455 +    "transrec3(k, a, b, c) ==
  34.456 +       transrec(k, \<lambda>x r.
  34.457 +         if x=0 then a
  34.458 +         else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
  34.459 +         else b(Arith.pred(x), r ` Arith.pred(x)))"
  34.460  
  34.461 -lemma equalityCE:
  34.462 -    "[| A = B;  [| c\<in>A; c\<in>B |] ==> P;  [| c\<notin>A; c\<notin>B |] ==> P |]  ==>  P"
  34.463 -by (erule equalityE, blast)
  34.464 -
  34.465 -lemma equality_iffD:
  34.466 -  "A = B ==> (!!x. x \<in> A <-> x \<in> B)"
  34.467 -  by auto
  34.468 -
  34.469 -
  34.470 -subsection\<open>Rules for Replace -- the derived form of replacement\<close>
  34.471 -
  34.472 -lemma Replace_iff:
  34.473 -    "b \<in> {y. x\<in>A, P(x,y)}  <->  (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) \<longrightarrow> y=b))"
  34.474 -apply (unfold Replace_def)
  34.475 -apply (rule replacement [THEN iff_trans], blast+)
  34.476 -done
  34.477 +lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
  34.478 +by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
  34.479  
  34.480 -(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
  34.481 -lemma ReplaceI [intro]:
  34.482 -    "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==>
  34.483 -     b \<in> {y. x\<in>A, P(x,y)}"
  34.484 -by (rule Replace_iff [THEN iffD2], blast)
  34.485 -
  34.486 -(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
  34.487 -lemma ReplaceE:
  34.488 -    "[| b \<in> {y. x\<in>A, P(x,y)};
  34.489 -        !!x. [| x: A;  P(x,b);  \<forall>y. P(x,y)\<longrightarrow>y=b |] ==> R
  34.490 -     |] ==> R"
  34.491 -by (rule Replace_iff [THEN iffD1, THEN bexE], simp+)
  34.492 +lemma transrec3_succ [simp]:
  34.493 +     "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
  34.494 +by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
  34.495  
  34.496 -(*As above but without the (generally useless) 3rd assumption*)
  34.497 -lemma ReplaceE2 [elim!]:
  34.498 -    "[| b \<in> {y. x\<in>A, P(x,y)};
  34.499 -        !!x. [| x: A;  P(x,b) |] ==> R
  34.500 -     |] ==> R"
  34.501 -by (erule ReplaceE, blast)
  34.502 -
  34.503 -lemma Replace_cong [cong]:
  34.504 -    "[| A=B;  !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==>
  34.505 -     Replace(A,P) = Replace(B,Q)"
  34.506 -apply (rule equality_iffI)
  34.507 -apply (simp add: Replace_iff)
  34.508 -done
  34.509 +lemma transrec3_Limit:
  34.510 +     "Limit(i) ==>
  34.511 +      transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
  34.512 +by (rule transrec3_def [THEN def_transrec, THEN trans], force)
  34.513  
  34.514  
  34.515 -subsection\<open>Rules for RepFun\<close>
  34.516 -
  34.517 -lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}"
  34.518 -by (simp add: RepFun_def Replace_iff, blast)
  34.519 -
  34.520 -(*Useful for coinduction proofs*)
  34.521 -lemma RepFun_eqI [intro]: "[| b=f(a);  a \<in> A |] ==> b \<in> {f(x). x\<in>A}"
  34.522 -apply (erule ssubst)
  34.523 -apply (erule RepFunI)
  34.524 -done
  34.525 -
  34.526 -lemma RepFunE [elim!]:
  34.527 -    "[| b \<in> {f(x). x\<in>A};
  34.528 -        !!x.[| x\<in>A;  b=f(x) |] ==> P |] ==>
  34.529 -     P"
  34.530 -by (simp add: RepFun_def Replace_iff, blast)
  34.531 -
  34.532 -lemma RepFun_cong [cong]:
  34.533 -    "[| A=B;  !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
  34.534 -by (simp add: RepFun_def)
  34.535 -
  34.536 -lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))"
  34.537 -by (unfold Bex_def, blast)
  34.538 -
  34.539 -lemma triv_RepFun [simp]: "{x. x\<in>A} = A"
  34.540 -by blast
  34.541 -
  34.542 -
  34.543 -subsection\<open>Rules for Collect -- forming a subset by separation\<close>
  34.544 -
  34.545 -(*Separation is derivable from Replacement*)
  34.546 -lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A & P(a)"
  34.547 -by (unfold Collect_def, blast)
  34.548 -
  34.549 -lemma CollectI [intro!]: "[| a\<in>A;  P(a) |] ==> a \<in> {x\<in>A. P(x)}"
  34.550 -by simp
  34.551 -
  34.552 -lemma CollectE [elim!]: "[| a \<in> {x\<in>A. P(x)};  [| a\<in>A; P(a) |] ==> R |] ==> R"
  34.553 -by simp
  34.554 -
  34.555 -lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A"
  34.556 -by (erule CollectE, assumption)
  34.557 -
  34.558 -lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)"
  34.559 -by (erule CollectE, assumption)
  34.560 -
  34.561 -lemma Collect_cong [cong]:
  34.562 -    "[| A=B;  !!x. x\<in>B ==> P(x) <-> Q(x) |]
  34.563 -     ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))"
  34.564 -by (simp add: Collect_def)
  34.565 -
  34.566 -
  34.567 -subsection\<open>Rules for Unions\<close>
  34.568 -
  34.569 -declare Union_iff [simp]
  34.570 -
  34.571 -(*The order of the premises presupposes that C is rigid; A may be flexible*)
  34.572 -lemma UnionI [intro]: "[| B: C;  A: B |] ==> A: \<Union>(C)"
  34.573 -by (simp, blast)
  34.574 -
  34.575 -lemma UnionE [elim!]: "[| A \<in> \<Union>(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
  34.576 -by (simp, blast)
  34.577 -
  34.578 -
  34.579 -subsection\<open>Rules for Unions of families\<close>
  34.580 -(* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *)
  34.581 -
  34.582 -lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))"
  34.583 -by (simp add: Bex_def, blast)
  34.584 -
  34.585 -(*The order of the premises presupposes that A is rigid; b may be flexible*)
  34.586 -lemma UN_I: "[| a: A;  b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))"
  34.587 -by (simp, blast)
  34.588 -
  34.589 -
  34.590 -lemma UN_E [elim!]:
  34.591 -    "[| b \<in> (\<Union>x\<in>A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
  34.592 -by blast
  34.593 -
  34.594 -lemma UN_cong:
  34.595 -    "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))"
  34.596 -by simp
  34.597 -
  34.598 -
  34.599 -(*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*)
  34.600 -
  34.601 -(* UN_E appears before UnionE so that it is tried first, to avoid expensive
  34.602 -  calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: would enlarge
  34.603 -  the search space.*)
  34.604 -
  34.605 -
  34.606 -subsection\<open>Rules for the empty set\<close>
  34.607 -
  34.608 -(*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0
  34.609 -  See Suppes, page 21.*)
  34.610 -lemma not_mem_empty [simp]: "a \<notin> 0"
  34.611 -apply (cut_tac foundation)
  34.612 -apply (best dest: equalityD2)
  34.613 -done
  34.614 -
  34.615 -lemmas emptyE [elim!] = not_mem_empty [THEN notE]
  34.616 -
  34.617 -
  34.618 -lemma empty_subsetI [simp]: "0 \<subseteq> A"
  34.619 -by blast
  34.620 -
  34.621 -lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0"
  34.622 -by blast
  34.623 -
  34.624 -lemma equals0D [dest]: "A=0 ==> a \<notin> A"
  34.625 -by blast
  34.626 -
  34.627 -declare sym [THEN equals0D, dest]
  34.628 -
  34.629 -lemma not_emptyI: "a\<in>A ==> A \<noteq> 0"
  34.630 -by blast
  34.631 -
  34.632 -lemma not_emptyE:  "[| A \<noteq> 0;  !!x. x\<in>A ==> R |] ==> R"
  34.633 -by blast
  34.634 -
  34.635 -
  34.636 -subsection\<open>Rules for Inter\<close>
  34.637 -
  34.638 -(*Not obviously useful for proving InterI, InterD, InterE*)
  34.639 -lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0"
  34.640 -by (simp add: Inter_def Ball_def, blast)
  34.641 -
  34.642 -(* Intersection is well-behaved only if the family is non-empty! *)
  34.643 -lemma InterI [intro!]:
  34.644 -    "[| !!x. x: C ==> A: x;  C\<noteq>0 |] ==> A \<in> \<Inter>(C)"
  34.645 -by (simp add: Inter_iff)
  34.646 -
  34.647 -(*A "destruct" rule -- every B in C contains A as an element, but
  34.648 -  A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)
  34.649 -lemma InterD [elim, Pure.elim]: "[| A \<in> \<Inter>(C);  B \<in> C |] ==> A \<in> B"
  34.650 -by (unfold Inter_def, blast)
  34.651 -
  34.652 -(*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *)
  34.653 -lemma InterE [elim]:
  34.654 -    "[| A \<in> \<Inter>(C);  B\<notin>C ==> R;  A\<in>B ==> R |] ==> R"
  34.655 -by (simp add: Inter_def, blast)
  34.656 -
  34.657 -
  34.658 -subsection\<open>Rules for Intersections of families\<close>
  34.659 -
  34.660 -(* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *)
  34.661 -
  34.662 -lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0"
  34.663 -by (force simp add: Inter_def)
  34.664 -
  34.665 -lemma INT_I: "[| !!x. x: A ==> b: B(x);  A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))"
  34.666 -by blast
  34.667 -
  34.668 -lemma INT_E: "[| b \<in> (\<Inter>x\<in>A. B(x));  a: A |] ==> b \<in> B(a)"
  34.669 -by blast
  34.670 -
  34.671 -lemma INT_cong:
  34.672 -    "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))"
  34.673 -by simp
  34.674 -
  34.675 -(*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*)
  34.676 -
  34.677 -
  34.678 -subsection\<open>Rules for Powersets\<close>
  34.679 -
  34.680 -lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)"
  34.681 -by (erule Pow_iff [THEN iffD2])
  34.682 -
  34.683 -lemma PowD: "A \<in> Pow(B)  ==>  A<=B"
  34.684 -by (erule Pow_iff [THEN iffD1])
  34.685 -
  34.686 -declare Pow_iff [iff]
  34.687 -
  34.688 -lemmas Pow_bottom = empty_subsetI [THEN PowI]    \<comment>\<open>@{term"0 \<in> Pow(B)"}\<close>
  34.689 -lemmas Pow_top = subset_refl [THEN PowI]         \<comment>\<open>@{term"A \<in> Pow(A)"}\<close>
  34.690 -
  34.691 -
  34.692 -subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close>
  34.693 -
  34.694 -(*The search is undirected.  Allowing redundant introduction rules may
  34.695 -  make it diverge.  Variable b represents ANY map, such as
  34.696 -  (lam x\<in>A.b(x)): A->Pow(A). *)
  34.697 -lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S"
  34.698 -by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
  34.699 +declaration \<open>fn _ =>
  34.700 +  Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
  34.701 +    map mk_eq o Ord_atomize o Variable.gen_all ctxt))
  34.702 +\<close>
  34.703  
  34.704  end
    35.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    35.2 +++ b/src/ZF/ZFC.thy	Sun Apr 09 20:44:35 2017 +0200
    35.3 @@ -0,0 +1,4 @@
    35.4 +theory ZFC imports ZF InfDatatype
    35.5 +begin
    35.6 +
    35.7 +end
    36.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    36.2 +++ b/src/ZF/ZF_Base.thy	Sun Apr 09 20:44:35 2017 +0200
    36.3 @@ -0,0 +1,650 @@
    36.4 +(*  Title:      ZF/ZF_Base.thy
    36.5 +    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
    36.6 +    Copyright   1993  University of Cambridge
    36.7 +*)
    36.8 +
    36.9 +section \<open>Base of Zermelo-Fraenkel Set Theory\<close>
   36.10 +
   36.11 +theory ZF_Base
   36.12 +imports "~~/src/FOL/FOL"
   36.13 +begin
   36.14 +
   36.15 +subsection \<open>Signature\<close>
   36.16 +
   36.17 +declare [[eta_contract = false]]
   36.18 +
   36.19 +typedecl i
   36.20 +instance i :: "term" ..
   36.21 +
   36.22 +axiomatization mem :: "[i, i] \<Rightarrow> o"  (infixl "\<in>" 50)  \<comment> \<open>membership relation\<close>
   36.23 +  and zero :: "i"  ("0")  \<comment> \<open>the empty set\<close>
   36.24 +  and Pow :: "i \<Rightarrow> i"  \<comment> \<open>power sets\<close>
   36.25 +  and Inf :: "i"  \<comment> \<open>infinite set\<close>
   36.26 +  and Union :: "i \<Rightarrow> i"  ("\<Union>_" [90] 90)
   36.27 +  and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
   36.28 +
   36.29 +abbreviation not_mem :: "[i, i] \<Rightarrow> o"  (infixl "\<notin>" 50)  \<comment> \<open>negated membership relation\<close>
   36.30 +  where "x \<notin> y \<equiv> \<not> (x \<in> y)"
   36.31 +
   36.32 +
   36.33 +subsection \<open>Bounded Quantifiers\<close>
   36.34 +
   36.35 +definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
   36.36 +  where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)"
   36.37 +
   36.38 +definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
   36.39 +  where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
   36.40 +
   36.41 +syntax
   36.42 +  "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<forall>_\<in>_./ _)" 10)
   36.43 +  "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<exists>_\<in>_./ _)" 10)
   36.44 +translations
   36.45 +  "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
   36.46 +  "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
   36.47 +
   36.48 +
   36.49 +subsection \<open>Variations on Replacement\<close>
   36.50 +
   36.51 +(* Derived form of replacement, restricting P to its functional part.
   36.52 +   The resulting set (for functional P) is the same as with
   36.53 +   PrimReplace, but the rules are simpler. *)
   36.54 +definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
   36.55 +  where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
   36.56 +
   36.57 +syntax
   36.58 +  "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
   36.59 +translations
   36.60 +  "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
   36.61 +
   36.62 +
   36.63 +(* Functional form of replacement -- analgous to ML's map functional *)
   36.64 +
   36.65 +definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
   36.66 +  where "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
   36.67 +
   36.68 +syntax
   36.69 +  "_RepFun" :: "[i, pttrn, i] => i"  ("(1{_ ./ _ \<in> _})" [51,0,51])
   36.70 +translations
   36.71 +  "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
   36.72 +
   36.73 +
   36.74 +(* Separation and Pairing can be derived from the Replacement
   36.75 +   and Powerset Axioms using the following definitions. *)
   36.76 +definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i"
   36.77 +  where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
   36.78 +
   36.79 +syntax
   36.80 +  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  ("(1{_ \<in> _ ./ _})")
   36.81 +translations
   36.82 +  "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
   36.83 +
   36.84 +
   36.85 +subsection \<open>General union and intersection\<close>
   36.86 +
   36.87 +definition Inter :: "i => i"  ("\<Inter>_" [90] 90)
   36.88 +  where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
   36.89 +
   36.90 +syntax
   36.91 +  "_UNION" :: "[pttrn, i, i] => i"  ("(3\<Union>_\<in>_./ _)" 10)
   36.92 +  "_INTER" :: "[pttrn, i, i] => i"  ("(3\<Inter>_\<in>_./ _)" 10)
   36.93 +translations
   36.94 +  "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
   36.95 +  "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
   36.96 +
   36.97 +
   36.98 +subsection \<open>Finite sets and binary operations\<close>
   36.99 +
  36.100 +(*Unordered pairs (Upair) express binary union/intersection and cons;
  36.101 +  set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
  36.102 +
  36.103 +definition Upair :: "[i, i] => i"
  36.104 +  where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
  36.105 +
  36.106 +definition Subset :: "[i, i] \<Rightarrow> o"  (infixl "\<subseteq>" 50)  \<comment> \<open>subset relation\<close>
  36.107 +  where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B"
  36.108 +
  36.109 +definition Diff :: "[i, i] \<Rightarrow> i"  (infixl "-" 65)  \<comment> \<open>set difference\<close>
  36.110 +  where "A - B == { x\<in>A . ~(x\<in>B) }"
  36.111 +
  36.112 +definition Un :: "[i, i] \<Rightarrow> i"  (infixl "\<union>" 65)  \<comment> \<open>binary union\<close>
  36.113 +  where "A \<union> B == \<Union>(Upair(A,B))"
  36.114 +
  36.115 +definition Int :: "[i, i] \<Rightarrow> i"  (infixl "\<inter>" 70)  \<comment> \<open>binary intersection\<close>
  36.116 +  where "A \<inter> B == \<Inter>(Upair(A,B))"
  36.117 +
  36.118 +definition cons :: "[i, i] => i"
  36.119 +  where "cons(a,A) == Upair(a,a) \<union> A"
  36.120 +
  36.121 +definition succ :: "i => i"
  36.122 +  where "succ(i) == cons(i, i)"
  36.123 +
  36.124 +nonterminal "is"
  36.125 +syntax
  36.126 +  "" :: "i \<Rightarrow> is"  ("_")
  36.127 +  "_Enum" :: "[i, is] \<Rightarrow> is"  ("_,/ _")
  36.128 +  "_Finset" :: "is \<Rightarrow> i"  ("{(_)}")
  36.129 +translations
  36.130 +  "{x, xs}" == "CONST cons(x, {xs})"
  36.131 +  "{x}" == "CONST cons(x, 0)"
  36.132 +
  36.133 +
  36.134 +subsection \<open>Axioms\<close>
  36.135 +
  36.136 +(* ZF axioms -- see Suppes p.238
  36.137 +   Axioms for Union, Pow and Replace state existence only,
  36.138 +   uniqueness is derivable using extensionality. *)
  36.139 +
  36.140 +axiomatization
  36.141 +where
  36.142 +  extension:     "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and
  36.143 +  Union_iff:     "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and
  36.144 +  Pow_iff:       "A \<in> Pow(B) \<longleftrightarrow> A \<subseteq> B" and
  36.145 +
  36.146 +  (*We may name this set, though it is not uniquely defined.*)
  36.147 +  infinity:      "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and
  36.148 +
  36.149 +  (*This formulation facilitates case analysis on A.*)
  36.150 +  foundation:    "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and
  36.151 +
  36.152 +  (*Schema axiom since predicate P is a higher-order variable*)
  36.153 +  replacement:   "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow>
  36.154 +                         b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))"
  36.155 +
  36.156 +
  36.157 +subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>
  36.158 +
  36.159 +definition The :: "(i \<Rightarrow> o) \<Rightarrow> i"  (binder "THE " 10)
  36.160 +  where the_def: "The(P)    == \<Union>({y . x \<in> {0}, P(y)})"
  36.161 +
  36.162 +definition If :: "[o, i, i] \<Rightarrow> i"  ("(if (_)/ then (_)/ else (_))" [10] 10)
  36.163 +  where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b"
  36.164 +
  36.165 +abbreviation (input)
  36.166 +  old_if :: "[o, i, i] => i"  ("if '(_,_,_')")
  36.167 +  where "if(P,a,b) == If(P,a,b)"
  36.168 +
  36.169 +
  36.170 +subsection \<open>Ordered Pairing\<close>
  36.171 +
  36.172 +(* this "symmetric" definition works better than {{a}, {a,b}} *)
  36.173 +definition Pair :: "[i, i] => i"
  36.174 +  where "Pair(a,b) == {{a,a}, {a,b}}"
  36.175 +
  36.176 +definition fst :: "i \<Rightarrow> i"
  36.177 +  where "fst(p) == THE a. \<exists>b. p = Pair(a, b)"
  36.178 +
  36.179 +definition snd :: "i \<Rightarrow> i"
  36.180 +  where "snd(p) == THE b. \<exists>a. p = Pair(a, b)"
  36.181 +
  36.182 +definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>
  36.183 +  where "split(c) == \<lambda>p. c(fst(p), snd(p))"
  36.184 +
  36.185 +(* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
  36.186 +nonterminal patterns
  36.187 +syntax
  36.188 +  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
  36.189 +  ""          :: "pttrn => patterns"         ("_")
  36.190 +  "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
  36.191 +  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
  36.192 +translations
  36.193 +  "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
  36.194 +  "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
  36.195 +  "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
  36.196 +  "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"
  36.197 +
  36.198 +definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
  36.199 +  where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
  36.200 +
  36.201 +abbreviation cart_prod :: "[i, i] => i"  (infixr "\<times>" 80)  \<comment> \<open>Cartesian product\<close>
  36.202 +  where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
  36.203 +
  36.204 +
  36.205 +subsection \<open>Relations and Functions\<close>
  36.206 +
  36.207 +(*converse of relation r, inverse of function*)
  36.208 +definition converse :: "i \<Rightarrow> i"
  36.209 +  where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}"
  36.210 +
  36.211 +definition domain :: "i \<Rightarrow> i"
  36.212 +  where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}"
  36.213 +
  36.214 +definition range :: "i \<Rightarrow> i"
  36.215 +  where "range(r) == domain(converse(r))"
  36.216 +
  36.217 +definition field :: "i \<Rightarrow> i"
  36.218 +  where "field(r) == domain(r) \<union> range(r)"
  36.219 +
  36.220 +definition relation :: "i \<Rightarrow> o"  \<comment> \<open>recognizes sets of pairs\<close>
  36.221 +  where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>"
  36.222 +
  36.223 +definition "function" :: "i \<Rightarrow> o"  \<comment> \<open>recognizes functions; can have non-pairs\<close>
  36.224 +  where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
  36.225 +
  36.226 +definition Image :: "[i, i] \<Rightarrow> i"  (infixl "``" 90)  \<comment> \<open>image\<close>
  36.227 +  where image_def: "r `` A  == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}"
  36.228 +
  36.229 +definition vimage :: "[i, i] \<Rightarrow> i"  (infixl "-``" 90)  \<comment> \<open>inverse image\<close>
  36.230 +  where vimage_def: "r -`` A == converse(r)``A"
  36.231 +
  36.232 +(* Restrict the relation r to the domain A *)
  36.233 +definition restrict :: "[i, i] \<Rightarrow> i"
  36.234 +  where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}"
  36.235 +
  36.236 +
  36.237 +(* Abstraction, application and Cartesian product of a family of sets *)
  36.238 +
  36.239 +definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
  36.240 +  where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}"
  36.241 +
  36.242 +definition "apply" :: "[i, i] \<Rightarrow> i"  (infixl "`" 90)  \<comment> \<open>function application\<close>
  36.243 +  where "f`a == \<Union>(f``{a})"
  36.244 +
  36.245 +definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
  36.246 +  where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}"
  36.247 +
  36.248 +abbreviation function_space :: "[i, i] \<Rightarrow> i"  (infixr "->" 60)  \<comment> \<open>function space\<close>
  36.249 +  where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
  36.250 +
  36.251 +
  36.252 +(* binder syntax *)
  36.253 +
  36.254 +syntax
  36.255 +  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Prod>_\<in>_./ _)" 10)
  36.256 +  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sum>_\<in>_./ _)" 10)
  36.257 +  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
  36.258 +translations
  36.259 +  "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
  36.260 +  "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
  36.261 +  "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"
  36.262 +
  36.263 +
  36.264 +subsection \<open>ASCII syntax\<close>
  36.265 +
  36.266 +notation (ASCII)
  36.267 +  cart_prod       (infixr "*" 80) and
  36.268 +  Int             (infixl "Int" 70) and
  36.269 +  Un              (infixl "Un" 65) and
  36.270 +  function_space  (infixr "\<rightarrow>" 60) and
  36.271 +  Subset          (infixl "<=" 50) and
  36.272 +  mem             (infixl ":" 50) and
  36.273 +  not_mem         (infixl "~:" 50)
  36.274 +
  36.275 +syntax (ASCII)
  36.276 +  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
  36.277 +  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
  36.278 +  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
  36.279 +  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
  36.280 +  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
  36.281 +  "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
  36.282 +  "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
  36.283 +  "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
  36.284 +  "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
  36.285 +  "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
  36.286 +  "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
  36.287 +  "_pattern"  :: "patterns => pttrn"         ("<_>")
  36.288 +
  36.289 +
  36.290 +subsection \<open>Substitution\<close>
  36.291 +
  36.292 +(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
  36.293 +lemma subst_elem: "[| b\<in>A;  a=b |] ==> a\<in>A"
  36.294 +by (erule ssubst, assumption)
  36.295 +
  36.296 +
  36.297 +subsection\<open>Bounded universal quantifier\<close>
  36.298 +
  36.299 +lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)"
  36.300 +by (simp add: Ball_def)
  36.301 +
  36.302 +lemmas strip = impI allI ballI
  36.303 +
  36.304 +lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x);  x: A |] ==> P(x)"
  36.305 +by (simp add: Ball_def)
  36.306 +
  36.307 +(*Instantiates x first: better for automatic theorem proving?*)
  36.308 +lemma rev_ballE [elim]:
  36.309 +    "[| \<forall>x\<in>A. P(x);  x\<notin>A ==> Q;  P(x) ==> Q |] ==> Q"
  36.310 +by (simp add: Ball_def, blast)
  36.311 +
  36.312 +lemma ballE: "[| \<forall>x\<in>A. P(x);  P(x) ==> Q;  x\<notin>A ==> Q |] ==> Q"
  36.313 +by blast
  36.314 +
  36.315 +(*Used in the datatype package*)
  36.316 +lemma rev_bspec: "[| x: A;  \<forall>x\<in>A. P(x) |] ==> P(x)"
  36.317 +by (simp add: Ball_def)
  36.318 +
  36.319 +(*Trival rewrite rule;   @{term"(\<forall>x\<in>A.P)<->P"} holds only if A is nonempty!*)
  36.320 +lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<longrightarrow> P)"
  36.321 +by (simp add: Ball_def)
  36.322 +
  36.323 +(*Congruence rule for rewriting*)
  36.324 +lemma ball_cong [cong]:
  36.325 +    "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))"
  36.326 +by (simp add: Ball_def)
  36.327 +
  36.328 +lemma atomize_ball:
  36.329 +    "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"
  36.330 +  by (simp only: Ball_def atomize_all atomize_imp)
  36.331 +
  36.332 +lemmas [symmetric, rulify] = atomize_ball
  36.333 +  and [symmetric, defn] = atomize_ball
  36.334 +
  36.335 +
  36.336 +subsection\<open>Bounded existential quantifier\<close>
  36.337 +
  36.338 +lemma bexI [intro]: "[| P(x);  x: A |] ==> \<exists>x\<in>A. P(x)"
  36.339 +by (simp add: Bex_def, blast)
  36.340 +
  36.341 +(*The best argument order when there is only one @{term"x\<in>A"}*)
  36.342 +lemma rev_bexI: "[| x\<in>A;  P(x) |] ==> \<exists>x\<in>A. P(x)"
  36.343 +by blast
  36.344 +
  36.345 +(*Not of the general form for such rules. The existential quanitifer becomes universal. *)
  36.346 +lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a);  a: A |] ==> \<exists>x\<in>A. P(x)"
  36.347 +by blast
  36.348 +
  36.349 +lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x);  !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q"
  36.350 +by (simp add: Bex_def, blast)
  36.351 +
  36.352 +(*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty!!*)
  36.353 +lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)"
  36.354 +by (simp add: Bex_def)
  36.355 +
  36.356 +lemma bex_cong [cong]:
  36.357 +    "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |]
  36.358 +     ==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))"
  36.359 +by (simp add: Bex_def cong: conj_cong)
  36.360 +
  36.361 +
  36.362 +
  36.363 +subsection\<open>Rules for subsets\<close>
  36.364 +
  36.365 +lemma subsetI [intro!]:
  36.366 +    "(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B"
  36.367 +by (simp add: subset_def)
  36.368 +
  36.369 +(*Rule in Modus Ponens style [was called subsetE] *)
  36.370 +lemma subsetD [elim]: "[| A \<subseteq> B;  c\<in>A |] ==> c\<in>B"
  36.371 +apply (unfold subset_def)
  36.372 +apply (erule bspec, assumption)
  36.373 +done
  36.374 +
  36.375 +(*Classical elimination rule*)
  36.376 +lemma subsetCE [elim]:
  36.377 +    "[| A \<subseteq> B;  c\<notin>A ==> P;  c\<in>B ==> P |] ==> P"
  36.378 +by (simp add: subset_def, blast)
  36.379 +
  36.380 +(*Sometimes useful with premises in this order*)
  36.381 +lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B"
  36.382 +by blast
  36.383 +
  36.384 +lemma contra_subsetD: "[| A \<subseteq> B; c \<notin> B |] ==> c \<notin> A"
  36.385 +by blast
  36.386 +
  36.387 +lemma rev_contra_subsetD: "[| c \<notin> B;  A \<subseteq> B |] ==> c \<notin> A"
  36.388 +by blast
  36.389 +
  36.390 +lemma subset_refl [simp]: "A \<subseteq> A"
  36.391 +by blast
  36.392 +
  36.393 +lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"
  36.394 +by blast
  36.395 +
  36.396 +(*Useful for proving A<=B by rewriting in some cases*)
  36.397 +lemma subset_iff:
  36.398 +     "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
  36.399 +apply (unfold subset_def Ball_def)
  36.400 +apply (rule iff_refl)
  36.401 +done
  36.402 +
  36.403 +text\<open>For calculations\<close>
  36.404 +declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]
  36.405 +
  36.406 +
  36.407 +subsection\<open>Rules for equality\<close>
  36.408 +
  36.409 +(*Anti-symmetry of the subset relation*)
  36.410 +lemma equalityI [intro]: "[| A \<subseteq> B;  B \<subseteq> A |] ==> A = B"
  36.411 +by (rule extension [THEN iffD2], rule conjI)
  36.412 +
  36.413 +
  36.414 +lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B"
  36.415 +by (rule equalityI, blast+)
  36.416 +
  36.417 +lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1]
  36.418 +lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]
  36.419 +
  36.420 +lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
  36.421 +by (blast dest: equalityD1 equalityD2)
  36.422 +
  36.423 +lemma equalityCE:
  36.424 +    "[| A = B;  [| c\<in>A; c\<in>B |] ==> P;  [| c\<notin>A; c\<notin>B |] ==> P |]  ==>  P"
  36.425 +by (erule equalityE, blast)
  36.426 +
  36.427 +lemma equality_iffD:
  36.428 +  "A = B ==> (!!x. x \<in> A <-> x \<in> B)"
  36.429 +  by auto
  36.430 +
  36.431 +
  36.432 +subsection\<open>Rules for Replace -- the derived form of replacement\<close>
  36.433 +
  36.434 +lemma Replace_iff:
  36.435 +    "b \<in> {y. x\<in>A, P(x,y)}  <->  (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) \<longrightarrow> y=b))"
  36.436 +apply (unfold Replace_def)
  36.437 +apply (rule replacement [THEN iff_trans], blast+)
  36.438 +done
  36.439 +
  36.440 +(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
  36.441 +lemma ReplaceI [intro]:
  36.442 +    "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==>
  36.443 +     b \<in> {y. x\<in>A, P(x,y)}"
  36.444 +by (rule Replace_iff [THEN iffD2], blast)
  36.445 +
  36.446 +(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
  36.447 +lemma ReplaceE:
  36.448 +    "[| b \<in> {y. x\<in>A, P(x,y)};
  36.449 +        !!x. [| x: A;  P(x,b);  \<forall>y. P(x,y)\<longrightarrow>y=b |] ==> R
  36.450 +     |] ==> R"
  36.451 +by (rule Replace_iff [THEN iffD1, THEN bexE], simp+)
  36.452 +
  36.453 +(*As above but without the (generally useless) 3rd assumption*)
  36.454 +lemma ReplaceE2 [elim!]:
  36.455 +    "[| b \<in> {y. x\<in>A, P(x,y)};
  36.456 +        !!x. [| x: A;  P(x,b) |] ==> R
  36.457 +     |] ==> R"
  36.458 +by (erule ReplaceE, blast)
  36.459 +
  36.460 +lemma Replace_cong [cong]:
  36.461 +    "[| A=B;  !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==>
  36.462 +     Replace(A,P) = Replace(B,Q)"
  36.463 +apply (rule equality_iffI)
  36.464 +apply (simp add: Replace_iff)
  36.465 +done
  36.466 +
  36.467 +
  36.468 +subsection\<open>Rules for RepFun\<close>
  36.469 +
  36.470 +lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}"
  36.471 +by (simp add: RepFun_def Replace_iff, blast)
  36.472 +
  36.473 +(*Useful for coinduction proofs*)
  36.474 +lemma RepFun_eqI [intro]: "[| b=f(a);  a \<in> A |] ==> b \<in> {f(x). x\<in>A}"
  36.475 +apply (erule ssubst)
  36.476 +apply (erule RepFunI)
  36.477 +done
  36.478 +
  36.479 +lemma RepFunE [elim!]:
  36.480 +    "[| b \<in> {f(x). x\<in>A};
  36.481 +        !!x.[| x\<in>A;  b=f(x) |] ==> P |] ==>
  36.482 +     P"
  36.483 +by (simp add: RepFun_def Replace_iff, blast)
  36.484 +
  36.485 +lemma RepFun_cong [cong]:
  36.486 +    "[| A=B;  !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
  36.487 +by (simp add: RepFun_def)
  36.488 +
  36.489 +lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))"
  36.490 +by (unfold Bex_def, blast)
  36.491 +
  36.492 +lemma triv_RepFun [simp]: "{x. x\<in>A} = A"
  36.493 +by blast
  36.494 +
  36.495 +
  36.496 +subsection\<open>Rules for Collect -- forming a subset by separation\<close>
  36.497 +
  36.498 +(*Separation is derivable from Replacement*)
  36.499 +lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A & P(a)"
  36.500 +by (unfold Collect_def, blast)
  36.501 +
  36.502 +lemma CollectI [intro!]: "[| a\<in>A;  P(a) |] ==> a \<in> {x\<in>A. P(x)}"
  36.503 +by simp
  36.504 +
  36.505 +lemma CollectE [elim!]: "[| a \<in> {x\<in>A. P(x)};  [| a\<in>A; P(a) |] ==> R |] ==> R"
  36.506 +by simp
  36.507 +
  36.508 +lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A"
  36.509 +by (erule CollectE, assumption)
  36.510 +
  36.511 +lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)"
  36.512 +by (erule CollectE, assumption)
  36.513 +
  36.514 +lemma Collect_cong [cong]:
  36.515 +    "[| A=B;  !!x. x\<in>B ==> P(x) <-> Q(x) |]
  36.516 +     ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))"
  36.517 +by (simp add: Collect_def)
  36.518 +
  36.519 +
  36.520 +subsection\<open>Rules for Unions\<close>
  36.521 +
  36.522 +declare Union_iff [simp]
  36.523 +
  36.524 +(*The order of the premises presupposes that C is rigid; A may be flexible*)
  36.525 +lemma UnionI [intro]: "[| B: C;  A: B |] ==> A: \<Union>(C)"
  36.526 +by (simp, blast)
  36.527 +
  36.528 +lemma UnionE [elim!]: "[| A \<in> \<Union>(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
  36.529 +by (simp, blast)
  36.530 +
  36.531 +
  36.532 +subsection\<open>Rules for Unions of families\<close>
  36.533 +(* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *)
  36.534 +
  36.535 +lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))"
  36.536 +by (simp add: Bex_def, blast)
  36.537 +
  36.538 +(*The order of the premises presupposes that A is rigid; b may be flexible*)
  36.539 +lemma UN_I: "[| a: A;  b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))"
  36.540 +by (simp, blast)
  36.541 +
  36.542 +
  36.543 +lemma UN_E [elim!]:
  36.544 +    "[| b \<in> (\<Union>x\<in>A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
  36.545 +by blast
  36.546 +
  36.547 +lemma UN_cong:
  36.548 +    "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))"
  36.549 +by simp
  36.550 +
  36.551 +
  36.552 +(*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*)
  36.553 +
  36.554 +(* UN_E appears before UnionE so that it is tried first, to avoid expensive
  36.555 +  calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: would enlarge
  36.556 +  the search space.*)
  36.557 +
  36.558 +
  36.559 +subsection\<open>Rules for the empty set\<close>
  36.560 +
  36.561 +(*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0
  36.562 +  See Suppes, page 21.*)
  36.563 +lemma not_mem_empty [simp]: "a \<notin> 0"
  36.564 +apply (cut_tac foundation)
  36.565 +apply (best dest: equalityD2)
  36.566 +done
  36.567 +
  36.568 +lemmas emptyE [elim!] = not_mem_empty [THEN notE]
  36.569 +
  36.570 +
  36.571 +lemma empty_subsetI [simp]: "0 \<subseteq> A"
  36.572 +by blast
  36.573 +
  36.574 +lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0"
  36.575 +by blast
  36.576 +
  36.577 +lemma equals0D [dest]: "A=0 ==> a \<notin> A"
  36.578 +by blast
  36.579 +
  36.580 +declare sym [THEN equals0D, dest]
  36.581 +
  36.582 +lemma not_emptyI: "a\<in>A ==> A \<noteq> 0"
  36.583 +by blast
  36.584 +
  36.585 +lemma not_emptyE:  "[| A \<noteq> 0;  !!x. x\<in>A ==> R |] ==> R"
  36.586 +by blast
  36.587 +
  36.588 +
  36.589 +subsection\<open>Rules for Inter\<close>
  36.590 +
  36.591 +(*Not obviously useful for proving InterI, InterD, InterE*)
  36.592 +lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0"
  36.593 +by (simp add: Inter_def Ball_def, blast)
  36.594 +
  36.595 +(* Intersection is well-behaved only if the family is non-empty! *)
  36.596 +lemma InterI [intro!]:
  36.597 +    "[| !!x. x: C ==> A: x;  C\<noteq>0 |] ==> A \<in> \<Inter>(C)"
  36.598 +by (simp add: Inter_iff)
  36.599 +
  36.600 +(*A "destruct" rule -- every B in C contains A as an element, but
  36.601 +  A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)
  36.602 +lemma InterD [elim, Pure.elim]: "[| A \<in> \<Inter>(C);  B \<in> C |] ==> A \<in> B"
  36.603 +by (unfold Inter_def, blast)
  36.604 +
  36.605 +(*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *)
  36.606 +lemma InterE [elim]:
  36.607 +    "[| A \<in> \<Inter>(C);  B\<notin>C ==> R;  A\<in>B ==> R |] ==> R"
  36.608 +by (simp add: Inter_def, blast)
  36.609 +
  36.610 +
  36.611 +subsection\<open>Rules for Intersections of families\<close>
  36.612 +
  36.613 +(* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *)
  36.614 +
  36.615 +lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0"
  36.616 +by (force simp add: Inter_def)
  36.617 +
  36.618 +lemma INT_I: "[| !!x. x: A ==> b: B(x);  A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))"
  36.619 +by blast
  36.620 +
  36.621 +lemma INT_E: "[| b \<in> (\<Inter>x\<in>A. B(x));  a: A |] ==> b \<in> B(a)"
  36.622 +by blast
  36.623 +
  36.624 +lemma INT_cong:
  36.625 +    "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))"
  36.626 +by simp
  36.627 +
  36.628 +(*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*)
  36.629 +
  36.630 +
  36.631 +subsection\<open>Rules for Powersets\<close>
  36.632 +
  36.633 +lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)"
  36.634 +by (erule Pow_iff [THEN iffD2])
  36.635 +
  36.636 +lemma PowD: "A \<in> Pow(B)  ==>  A<=B"
  36.637 +by (erule Pow_iff [THEN iffD1])
  36.638 +
  36.639 +declare Pow_iff [iff]
  36.640 +
  36.641 +lemmas Pow_bottom = empty_subsetI [THEN PowI]    \<comment>\<open>@{term"0 \<in> Pow(B)"}\<close>
  36.642 +lemmas Pow_top = subset_refl [THEN PowI]         \<comment>\<open>@{term"A \<in> Pow(A)"}\<close>
  36.643 +
  36.644 +
  36.645 +subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close>
  36.646 +
  36.647 +(*The search is undirected.  Allowing redundant introduction rules may
  36.648 +  make it diverge.  Variable b represents ANY map, such as
  36.649 +  (lam x\<in>A.b(x)): A->Pow(A). *)
  36.650 +lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S"
  36.651 +by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
  36.652 +
  36.653 +end
    37.1 --- a/src/ZF/ex/BinEx.thy	Sun Apr 09 20:17:00 2017 +0200
    37.2 +++ b/src/ZF/ex/BinEx.thy	Sun Apr 09 20:44:35 2017 +0200
    37.3 @@ -5,7 +5,7 @@
    37.4  Examples of performing binary arithmetic by simplification.
    37.5  *)
    37.6  
    37.7 -theory BinEx imports Main begin
    37.8 +theory BinEx imports ZF begin
    37.9  (*All runtimes below are on a 300MHz Pentium*)
   37.10  
   37.11  lemma "#13  $+  #19 = #32"
    38.1 --- a/src/ZF/ex/CoUnit.thy	Sun Apr 09 20:17:00 2017 +0200
    38.2 +++ b/src/ZF/ex/CoUnit.thy	Sun Apr 09 20:44:35 2017 +0200
    38.3 @@ -5,7 +5,7 @@
    38.4  
    38.5  section \<open>Trivial codatatype definitions, one of which goes wrong!\<close>
    38.6  
    38.7 -theory CoUnit imports Main begin
    38.8 +theory CoUnit imports ZF begin
    38.9  
   38.10  text \<open>
   38.11    See discussion in: L C Paulson.  A Concrete Final Coalgebra Theorem
    39.1 --- a/src/ZF/ex/Commutation.thy	Sun Apr 09 20:17:00 2017 +0200
    39.2 +++ b/src/ZF/ex/Commutation.thy	Sun Apr 09 20:44:35 2017 +0200
    39.3 @@ -5,7 +5,7 @@
    39.4  Commutation theory for proving the Church Rosser theorem.
    39.5  *)
    39.6  
    39.7 -theory Commutation imports Main begin
    39.8 +theory Commutation imports ZF begin
    39.9  
   39.10  definition
   39.11    square  :: "[i, i, i, i] => o" where
    40.1 --- a/src/ZF/ex/Group.thy	Sun Apr 09 20:17:00 2017 +0200
    40.2 +++ b/src/ZF/ex/Group.thy	Sun Apr 09 20:44:35 2017 +0200
    40.3 @@ -2,7 +2,7 @@
    40.4  
    40.5  section \<open>Groups\<close>
    40.6  
    40.7 -theory Group imports Main begin
    40.8 +theory Group imports ZF begin
    40.9  
   40.10  text\<open>Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and
   40.11  Markus Wenzel.\<close>
    41.1 --- a/src/ZF/ex/LList.thy	Sun Apr 09 20:17:00 2017 +0200
    41.2 +++ b/src/ZF/ex/LList.thy	Sun Apr 09 20:44:35 2017 +0200
    41.3 @@ -13,7 +13,7 @@
    41.4  a typing rule for it, based on some notion of "productivity..."
    41.5  *)
    41.6  
    41.7 -theory LList imports Main begin
    41.8 +theory LList imports ZF begin
    41.9  
   41.10  consts
   41.11    llist  :: "i=>i"
    42.1 --- a/src/ZF/ex/Limit.thy	Sun Apr 09 20:17:00 2017 +0200
    42.2 +++ b/src/ZF/ex/Limit.thy	Sun Apr 09 20:44:35 2017 +0200
    42.3 @@ -17,7 +17,7 @@
    42.4  Laboratory, 1995.
    42.5  *)
    42.6  
    42.7 -theory Limit  imports  Main begin
    42.8 +theory Limit  imports  ZF begin
    42.9  
   42.10  definition
   42.11    rel :: "[i,i,i]=>o"  where
    43.1 --- a/src/ZF/ex/NatSum.thy	Sun Apr 09 20:17:00 2017 +0200
    43.2 +++ b/src/ZF/ex/NatSum.thy	Sun Apr 09 20:44:35 2017 +0200
    43.3 @@ -16,7 +16,7 @@
    43.4  *)
    43.5  
    43.6  
    43.7 -theory NatSum imports Main begin
    43.8 +theory NatSum imports ZF begin
    43.9  
   43.10  consts sum :: "[i=>i, i] => i"
   43.11  primrec 
    44.1 --- a/src/ZF/ex/Primes.thy	Sun Apr 09 20:17:00 2017 +0200
    44.2 +++ b/src/ZF/ex/Primes.thy	Sun Apr 09 20:44:35 2017 +0200
    44.3 @@ -5,7 +5,7 @@
    44.4  
    44.5  section\<open>The Divides Relation and Euclid's algorithm for the GCD\<close>
    44.6  
    44.7 -theory Primes imports Main begin
    44.8 +theory Primes imports ZF begin
    44.9  
   44.10  definition
   44.11    divides :: "[i,i]=>o"              (infixl "dvd" 50)  where
    45.1 --- a/src/ZF/ex/Ramsey.thy	Sun Apr 09 20:17:00 2017 +0200
    45.2 +++ b/src/ZF/ex/Ramsey.thy	Sun Apr 09 20:44:35 2017 +0200
    45.3 @@ -24,7 +24,7 @@
    45.4    | ram i j = ram (i-1) j + ram i (j-1)
    45.5  *)
    45.6  
    45.7 -theory Ramsey imports Main begin
    45.8 +theory Ramsey imports ZF begin
    45.9  
   45.10  definition
   45.11    Symmetric :: "i=>o" where
    46.1 --- a/src/ZF/ex/misc.thy	Sun Apr 09 20:17:00 2017 +0200
    46.2 +++ b/src/ZF/ex/misc.thy	Sun Apr 09 20:44:35 2017 +0200
    46.3 @@ -7,7 +7,7 @@
    46.4  
    46.5  section\<open>Miscellaneous ZF Examples\<close>
    46.6  
    46.7 -theory misc imports Main begin
    46.8 +theory misc imports ZF begin
    46.9  
   46.10  
   46.11  subsection\<open>Various Small Problems\<close>
    47.1 --- a/src/ZF/upair.thy	Sun Apr 09 20:17:00 2017 +0200
    47.2 +++ b/src/ZF/upair.thy	Sun Apr 09 20:44:35 2017 +0200
    47.3 @@ -12,7 +12,7 @@
    47.4  section\<open>Unordered Pairs\<close>
    47.5  
    47.6  theory upair
    47.7 -imports ZF
    47.8 +imports ZF_Base
    47.9  keywords "print_tcset" :: diag
   47.10  begin
   47.11