# HG changeset patch # User wenzelm # Date 1491763475 -7200 # Node ID c82e63b11b8b2f413ade6f2b6278f2db2e95d704 # Parent 9bc3b57c1fa7979a404139e8ea7006233a3ac6ca clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy; diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/Doc/Logics_ZF/ZF_Isar.thy --- a/src/Doc/Logics_ZF/ZF_Isar.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/Doc/Logics_ZF/ZF_Isar.thy Sun Apr 09 20:44:35 2017 +0200 @@ -1,5 +1,5 @@ theory ZF_Isar -imports Main +imports ZF begin (*<*) diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/Doc/Logics_ZF/ZF_examples.thy --- a/src/Doc/Logics_ZF/ZF_examples.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/Doc/Logics_ZF/ZF_examples.thy Sun Apr 09 20:44:35 2017 +0200 @@ -1,6 +1,6 @@ section{*Examples of Reasoning in ZF Set Theory*} -theory ZF_examples imports Main_ZFC begin +theory ZF_examples imports ZFC begin subsection {* Binary Trees *} diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/AC.thy --- a/src/ZF/AC.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/AC.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section\The Axiom of Choice\ -theory AC imports Main_ZF begin +theory AC imports ZF begin text\This definition comes from Halmos (1960), page 59.\ axiomatization where diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/AC/AC_Equiv.thy --- a/src/ZF/AC/AC_Equiv.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/AC/AC_Equiv.thy Sun Apr 09 20:44:35 2017 +0200 @@ -12,8 +12,8 @@ *) theory AC_Equiv -imports Main -begin (*obviously not Main_ZFC*) +imports ZF +begin (*obviously not ZFC*) (* Well Ordering Theorems *) diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Coind/Language.thy --- a/src/ZF/Coind/Language.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Coind/Language.thy Sun Apr 09 20:44:35 2017 +0200 @@ -3,7 +3,7 @@ Copyright 1995 University of Cambridge *) -theory Language imports Main begin +theory Language imports ZF begin text\these really can't be definitions without losing the abstraction\ diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Coind/Map.thy --- a/src/ZF/Coind/Map.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Coind/Map.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ Some sample proofs of inclusions for the final coalgebra "U" (by lcp). *) -theory Map imports Main begin +theory Map imports ZF begin definition TMap :: "[i,i] => i" where diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Constructible/Formula.thy --- a/src/ZF/Constructible/Formula.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Constructible/Formula.thy Sun Apr 09 20:44:35 2017 +0200 @@ -4,7 +4,7 @@ section \First-Order Formulas and the Definition of the Class L\ -theory Formula imports Main begin +theory Formula imports ZF begin subsection\Internalized formulas of FOL\ diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Constructible/MetaExists.thy --- a/src/ZF/Constructible/MetaExists.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Constructible/MetaExists.thy Sun Apr 09 20:44:35 2017 +0200 @@ -4,7 +4,7 @@ section\The meta-existential quantifier\ -theory MetaExists imports Main begin +theory MetaExists imports ZF begin text\Allows quantification over any term. Used to quantify over classes. Yields a proposition rather than a FOL formula.\ diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Constructible/Normal.thy --- a/src/ZF/Constructible/Normal.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Constructible/Normal.thy Sun Apr 09 20:44:35 2017 +0200 @@ -4,7 +4,7 @@ section \Closed Unbounded Classes and Normal Functions\ -theory Normal imports Main begin +theory Normal imports ZF begin text\ One source is the book diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Constructible/Relative.thy Sun Apr 09 20:44:35 2017 +0200 @@ -4,7 +4,7 @@ section \Relativization and Absoluteness\ -theory Relative imports Main begin +theory Relative imports ZF begin subsection\Relativized versions of standard set-theoretic concepts\ @@ -593,13 +593,13 @@ lemma (in M_trivial) pair_abs [simp]: "M(z) ==> pair(M,a,b,z) \ z=" -apply (simp add: pair_def ZF.Pair_def) +apply (simp add: pair_def Pair_def) apply (blast intro: transM) done lemma (in M_trivial) pair_in_M_iff [iff]: "M() \ M(a) & M(b)" -by (simp add: ZF.Pair_def) +by (simp add: Pair_def) lemma (in M_trivial) pair_components_in_M: "[| \ A; M(A) |] ==> M(x) & M(y)" diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/IMP/Com.thy --- a/src/ZF/IMP/Com.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/IMP/Com.thy Sun Apr 09 20:44:35 2017 +0200 @@ -4,7 +4,7 @@ section \Arithmetic expressions, boolean expressions, commands\ -theory Com imports Main begin +theory Com imports ZF begin subsection \Arithmetic expressions\ diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Acc.thy --- a/src/ZF/Induct/Acc.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Acc.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \The accessible part of a relation\ -theory Acc imports Main begin +theory Acc imports ZF begin text \ Inductive definition of \acc(r)\; see @{cite "paulin-tlca"}. diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Binary_Trees.thy --- a/src/ZF/Induct/Binary_Trees.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Binary_Trees.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \Binary trees\ -theory Binary_Trees imports Main begin +theory Binary_Trees imports ZF begin subsection \Datatype definition\ diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Brouwer.thy --- a/src/ZF/Induct/Brouwer.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Brouwer.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \Infinite branching datatype definitions\ -theory Brouwer imports Main_ZFC begin +theory Brouwer imports ZFC begin subsection \The Brouwer ordinals\ diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Comb.thy --- a/src/ZF/Induct/Comb.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Comb.thy Sun Apr 09 20:44:35 2017 +0200 @@ -6,7 +6,7 @@ section \Combinatory Logic example: the Church-Rosser Theorem\ theory Comb -imports Main +imports ZF begin text \ diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Datatypes.thy --- a/src/ZF/Induct/Datatypes.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Datatypes.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \Sample datatype definitions\ -theory Datatypes imports Main begin +theory Datatypes imports ZF begin subsection \A type with four constructors\ diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/FoldSet.thy --- a/src/ZF/Induct/FoldSet.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/FoldSet.thy Sun Apr 09 20:44:35 2017 +0200 @@ -6,7 +6,7 @@ least left-commutative. *) -theory FoldSet imports Main begin +theory FoldSet imports ZF begin consts fold_set :: "[i, i, [i,i]=>i, i] => i" diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/ListN.thy --- a/src/ZF/Induct/ListN.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/ListN.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \Lists of n elements\ -theory ListN imports Main begin +theory ListN imports ZF begin text \ Inductive definition of lists of \n\ elements; see diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Mutil.thy --- a/src/ZF/Induct/Mutil.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Mutil.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \The Mutilated Chess Board Problem, formalized inductively\ -theory Mutil imports Main begin +theory Mutil imports ZF begin text \ Originator is Max Black, according to J A Robinson. Popularized as diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Ntree.thy --- a/src/ZF/Induct/Ntree.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Ntree.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \Datatype definition n-ary branching trees\ -theory Ntree imports Main begin +theory Ntree imports ZF begin text \ Demonstrates a simple use of function space in a datatype diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Primrec.thy --- a/src/ZF/Induct/Primrec.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Primrec.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \Primitive Recursive Functions: the inductive definition\ -theory Primrec imports Main begin +theory Primrec imports ZF begin text \ Proof adopted from @{cite szasz93}. diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/PropLog.thy --- a/src/ZF/Induct/PropLog.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/PropLog.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \Meta-theory of propositional logic\ -theory PropLog imports Main begin +theory PropLog imports ZF begin text \ Datatype definition of propositional logic formulae and inductive diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Rmap.thy --- a/src/ZF/Induct/Rmap.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Rmap.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \An operator to ``map'' a relation over a list\ -theory Rmap imports Main begin +theory Rmap imports ZF begin consts rmap :: "i=>i" diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Term.thy --- a/src/ZF/Induct/Term.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Term.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \Terms over an alphabet\ -theory Term imports Main begin +theory Term imports ZF begin text \ Illustrates the list functor (essentially the same type as in \Trees_Forest\). diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Induct/Tree_Forest.thy --- a/src/ZF/Induct/Tree_Forest.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Induct/Tree_Forest.thy Sun Apr 09 20:44:35 2017 +0200 @@ -5,7 +5,7 @@ section \Trees and forests, a mutually recursive type definition\ -theory Tree_Forest imports Main begin +theory Tree_Forest imports ZF begin subsection \Datatype definition\ diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Main.thy --- a/src/ZF/Main.thy Sun Apr 09 20:17:00 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -theory Main -imports Main_ZF -begin - -end diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Main_ZF.thy --- a/src/ZF/Main_ZF.thy Sun Apr 09 20:17:00 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,73 +0,0 @@ -section\Theory Main: Everything Except AC\ - -theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin - -(*The theory of "iterates" logically belongs to Nat, but can't go there because - primrec isn't available into after Datatype.*) - -subsection\Iteration of the function @{term F}\ - -consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60) - -primrec - "F^0 (x) = x" - "F^(succ(n)) (x) = F(F^n (x))" - -definition - iterates_omega :: "[i=>i,i] => i" ("(_^\ '(_'))" [60,1000] 60) where - "F^\ (x) == \n\nat. F^n (x)" - -lemma iterates_triv: - "[| n\nat; F(x) = x |] ==> F^n (x) = x" -by (induct n rule: nat_induct, simp_all) - -lemma iterates_type [TC]: - "[| n \ nat; a \ A; !!x. x \ A ==> F(x) \ A |] - ==> F^n (a) \ A" -by (induct n rule: nat_induct, simp_all) - -lemma iterates_omega_triv: - "F(x) = x ==> F^\ (x) = x" -by (simp add: iterates_omega_def iterates_triv) - -lemma Ord_iterates [simp]: - "[| n\nat; !!i. Ord(i) ==> Ord(F(i)); Ord(x) |] - ==> Ord(F^n (x))" -by (induct n rule: nat_induct, simp_all) - -lemma iterates_commute: "n \ nat ==> F(F^n (x)) = F^n (F(x))" -by (induct_tac n, simp_all) - - -subsection\Transfinite Recursion\ - -text\Transfinite recursion for definitions based on the - three cases of ordinals\ - -definition - transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where - "transrec3(k, a, b, c) == - transrec(k, \x r. - if x=0 then a - else if Limit(x) then c(x, \y\x. r`y) - else b(Arith.pred(x), r ` Arith.pred(x)))" - -lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a" -by (rule transrec3_def [THEN def_transrec, THEN trans], simp) - -lemma transrec3_succ [simp]: - "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))" -by (rule transrec3_def [THEN def_transrec, THEN trans], simp) - -lemma transrec3_Limit: - "Limit(i) ==> - transrec3(i,a,b,c) = c(i, \j\i. transrec3(j,a,b,c))" -by (rule transrec3_def [THEN def_transrec, THEN trans], force) - - -declaration \fn _ => - Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt => - map mk_eq o Ord_atomize o Variable.gen_all ctxt)) -\ - -end diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Main_ZFC.thy --- a/src/ZF/Main_ZFC.thy Sun Apr 09 20:17:00 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -theory Main_ZFC imports Main_ZF InfDatatype -begin - -end diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/ROOT --- a/src/ZF/ROOT Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/ROOT Sun Apr 09 20:44:35 2017 +0200 @@ -43,8 +43,7 @@ (North-Holland, 1980) *} theories - Main - Main_ZFC + ZFC document_files "root.tex" session "ZF-AC" (ZF) in AC = ZF + diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/Resid/Redex.thy --- a/src/ZF/Resid/Redex.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/Resid/Redex.thy Sun Apr 09 20:44:35 2017 +0200 @@ -2,7 +2,7 @@ Author: Ole Rasmussen, University of Cambridge *) -theory Redex imports Main begin +theory Redex imports ZF begin consts redexes :: i diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/UNITY/GenPrefix.thy --- a/src/ZF/UNITY/GenPrefix.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/UNITY/GenPrefix.thy Sun Apr 09 20:44:35 2017 +0200 @@ -12,7 +12,7 @@ section\Charpentier's Generalized Prefix Relation\ theory GenPrefix -imports Main +imports ZF begin definition (*really belongs in ZF/Trancl*) diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/UNITY/State.thy --- a/src/ZF/UNITY/State.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/UNITY/State.thy Sun Apr 09 20:44:35 2017 +0200 @@ -10,7 +10,7 @@ section\UNITY Program States\ -theory State imports Main begin +theory State imports ZF begin consts var :: i datatype var = Var("i \ list(nat)") diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/UNITY/WFair.thy --- a/src/ZF/UNITY/WFair.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/UNITY/WFair.thy Sun Apr 09 20:44:35 2017 +0200 @@ -6,7 +6,7 @@ section\Progress under Weak Fairness\ theory WFair -imports UNITY Main_ZFC +imports UNITY ZFC begin text\This theory defines the operators transient, ensures and leadsTo, diff -r 9bc3b57c1fa7 -r c82e63b11b8b src/ZF/ZF.thy --- a/src/ZF/ZF.thy Sun Apr 09 20:17:00 2017 +0200 +++ b/src/ZF/ZF.thy Sun Apr 09 20:44:35 2017 +0200 @@ -1,650 +1,73 @@ -(* Title: ZF/ZF.thy - Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory - Copyright 1993 University of Cambridge -*) - -section \Zermelo-Fraenkel Set Theory\ - -theory ZF -imports "~~/src/FOL/FOL" -begin - -subsection \Signature\ - -declare [[eta_contract = false]] +section\Theory Main: Everything Except AC\ -typedecl i -instance i :: "term" .. - -axiomatization mem :: "[i, i] \ o" (infixl "\" 50) \ \membership relation\ - and zero :: "i" ("0") \ \the empty set\ - and Pow :: "i \ i" \ \power sets\ - and Inf :: "i" \ \infinite set\ - and Union :: "i \ i" ("\_" [90] 90) - and PrimReplace :: "[i, [i, i] \ o] \ i" - -abbreviation not_mem :: "[i, i] \ o" (infixl "\" 50) \ \negated membership relation\ - where "x \ y \ \ (x \ y)" - - -subsection \Bounded Quantifiers\ - -definition Ball :: "[i, i \ o] \ o" - where "Ball(A, P) \ \x. x\A \ P(x)" +theory ZF imports List_ZF IntDiv_ZF CardinalArith begin -definition Bex :: "[i, i \ o] \ o" - where "Bex(A, P) \ \x. x\A \ P(x)" - -syntax - "_Ball" :: "[pttrn, i, o] \ o" ("(3\_\_./ _)" 10) - "_Bex" :: "[pttrn, i, o] \ o" ("(3\_\_./ _)" 10) -translations - "\x\A. P" \ "CONST Ball(A, \x. P)" - "\x\A. P" \ "CONST Bex(A, \x. P)" - - -subsection \Variations on Replacement\ +(*The theory of "iterates" logically belongs to Nat, but can't go there because + primrec isn't available into after Datatype.*) -(* Derived form of replacement, restricting P to its functional part. - The resulting set (for functional P) is the same as with - PrimReplace, but the rules are simpler. *) -definition Replace :: "[i, [i, i] \ o] \ i" - where "Replace(A,P) == PrimReplace(A, %x y. (\!z. P(x,z)) & P(x,y))" - -syntax - "_Replace" :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \ _, _})") -translations - "{y. x\A, Q}" \ "CONST Replace(A, \x y. Q)" - - -(* Functional form of replacement -- analgous to ML's map functional *) - -definition RepFun :: "[i, i \ i] \ i" - where "RepFun(A,f) == {y . x\A, y=f(x)}" - -syntax - "_RepFun" :: "[i, pttrn, i] => i" ("(1{_ ./ _ \ _})" [51,0,51]) -translations - "{b. x\A}" \ "CONST RepFun(A, \x. b)" - +subsection\Iteration of the function @{term F}\ -(* Separation and Pairing can be derived from the Replacement - and Powerset Axioms using the following definitions. *) -definition Collect :: "[i, i \ o] \ i" - where "Collect(A,P) == {y . x\A, x=y & P(x)}" - -syntax - "_Collect" :: "[pttrn, i, o] \ i" ("(1{_ \ _ ./ _})") -translations - "{x\A. P}" \ "CONST Collect(A, \x. P)" - - -subsection \General union and intersection\ - -definition Inter :: "i => i" ("\_" [90] 90) - where "\(A) == { x\\(A) . \y\A. x\y}" - -syntax - "_UNION" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) - "_INTER" :: "[pttrn, i, i] => i" ("(3\_\_./ _)" 10) -translations - "\x\A. B" == "CONST Union({B. x\A})" - "\x\A. B" == "CONST Inter({B. x\A})" - - -subsection \Finite sets and binary operations\ - -(*Unordered pairs (Upair) express binary union/intersection and cons; - set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*) - -definition Upair :: "[i, i] => i" - where "Upair(a,b) == {y. x\Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}" - -definition Subset :: "[i, i] \ o" (infixl "\" 50) \ \subset relation\ - where subset_def: "A \ B \ \x\A. x\B" +consts iterates :: "[i=>i,i,i] => i" ("(_^_ '(_'))" [60,1000,1000] 60) -definition Diff :: "[i, i] \ i" (infixl "-" 65) \ \set difference\ - where "A - B == { x\A . ~(x\B) }" - -definition Un :: "[i, i] \ i" (infixl "\" 65) \ \binary union\ - where "A \ B == \(Upair(A,B))" - -definition Int :: "[i, i] \ i" (infixl "\" 70) \ \binary intersection\ - where "A \ B == \(Upair(A,B))" - -definition cons :: "[i, i] => i" - where "cons(a,A) == Upair(a,a) \ A" - -definition succ :: "i => i" - where "succ(i) == cons(i, i)" +primrec + "F^0 (x) = x" + "F^(succ(n)) (x) = F(F^n (x))" -nonterminal "is" -syntax - "" :: "i \ is" ("_") - "_Enum" :: "[i, is] \ is" ("_,/ _") - "_Finset" :: "is \ i" ("{(_)}") -translations - "{x, xs}" == "CONST cons(x, {xs})" - "{x}" == "CONST cons(x, 0)" - - -subsection \Axioms\ - -(* ZF axioms -- see Suppes p.238 - Axioms for Union, Pow and Replace state existence only, - uniqueness is derivable using extensionality. *) - -axiomatization -where - extension: "A = B \ A \ B \ B \ A" and - Union_iff: "A \ \(C) \ (\B\C. A\B)" and - Pow_iff: "A \ Pow(B) \ A \ B" and - - (*We may name this set, though it is not uniquely defined.*) - infinity: "0 \ Inf \ (\y\Inf. succ(y) \ Inf)" and +definition + iterates_omega :: "[i=>i,i] => i" ("(_^\ '(_'))" [60,1000] 60) where + "F^\ (x) == \n\nat. F^n (x)" - (*This formulation facilitates case analysis on A.*) - foundation: "A = 0 \ (\x\A. \y\x. y\A)" and - - (*Schema axiom since predicate P is a higher-order variable*) - replacement: "(\x\A. \y z. P(x,y) \ P(x,z) \ y = z) \ - b \ PrimReplace(A,P) \ (\x\A. P(x,b))" - - -subsection \Definite descriptions -- via Replace over the set "1"\ - -definition The :: "(i \ o) \ i" (binder "THE " 10) - where the_def: "The(P) == \({y . x \ {0}, P(y)})" - -definition If :: "[o, i, i] \ i" ("(if (_)/ then (_)/ else (_))" [10] 10) - where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b" - -abbreviation (input) - old_if :: "[o, i, i] => i" ("if '(_,_,_')") - where "if(P,a,b) == If(P,a,b)" - - -subsection \Ordered Pairing\ - -(* this "symmetric" definition works better than {{a}, {a,b}} *) -definition Pair :: "[i, i] => i" - where "Pair(a,b) == {{a,a}, {a,b}}" - -definition fst :: "i \ i" - where "fst(p) == THE a. \b. p = Pair(a, b)" - -definition snd :: "i \ i" - where "snd(p) == THE b. \a. p = Pair(a, b)" +lemma iterates_triv: + "[| n\nat; F(x) = x |] ==> F^n (x) = x" +by (induct n rule: nat_induct, simp_all) -definition split :: "[[i, i] \ 'a, i] \ 'a::{}" \ \for pattern-matching\ - where "split(c) == \p. c(fst(p), snd(p))" - -(* Patterns -- extends pre-defined type "pttrn" used in abstractions *) -nonterminal patterns -syntax - "_pattern" :: "patterns => pttrn" ("\_\") - "" :: "pttrn => patterns" ("_") - "_patterns" :: "[pttrn, patterns] => patterns" ("_,/_") - "_Tuple" :: "[i, is] => i" ("\(_,/ _)\") -translations - "\x, y, z\" == "\x, \y, z\\" - "\x, y\" == "CONST Pair(x, y)" - "\\x,y,zs\.b" == "CONST split(\x \y,zs\.b)" - "\\x,y\.b" == "CONST split(\x y. b)" - -definition Sigma :: "[i, i \ i] \ i" - where "Sigma(A,B) == \x\A. \y\B(x). {\x,y\}" - -abbreviation cart_prod :: "[i, i] => i" (infixr "\" 80) \ \Cartesian product\ - where "A \ B \ Sigma(A, \_. B)" - - -subsection \Relations and Functions\ - -(*converse of relation r, inverse of function*) -definition converse :: "i \ i" - where "converse(r) == {z. w\r, \x y. w=\x,y\ \ z=\y,x\}" - -definition domain :: "i \ i" - where "domain(r) == {x. w\r, \y. w=\x,y\}" - -definition range :: "i \ i" - where "range(r) == domain(converse(r))" - -definition field :: "i \ i" - where "field(r) == domain(r) \ range(r)" +lemma iterates_type [TC]: + "[| n \ nat; a \ A; !!x. x \ A ==> F(x) \ A |] + ==> F^n (a) \ A" +by (induct n rule: nat_induct, simp_all) -definition relation :: "i \ o" \ \recognizes sets of pairs\ - where "relation(r) == \z\r. \x y. z = \x,y\" - -definition "function" :: "i \ o" \ \recognizes functions; can have non-pairs\ - where "function(r) == \x y. \x,y\ \ r \ (\y'. \x,y'\ \