Various tweaks of the presentation
authorpaulson
Fri Aug 16 17:19:43 2002 +0200 (2002-08-16)
changeset 13506acc18a5d2b1a
parent 13505 52a16cb7fefb
child 13507 febb8e5d2a9d
Various tweaks of the presentation
src/ZF/Constructible/Internalize.thy
src/ZF/Constructible/L_axioms.thy
src/ZF/Constructible/Rec_Separation.thy
src/ZF/Constructible/WF_absolute.thy
src/ZF/Constructible/WFrec.thy
     1.1 --- a/src/ZF/Constructible/Internalize.thy	Fri Aug 16 16:41:48 2002 +0200
     1.2 +++ b/src/ZF/Constructible/Internalize.thy	Fri Aug 16 17:19:43 2002 +0200
     1.3 @@ -565,6 +565,7 @@
     1.4  
     1.5  subsection{*Well-Founded Recursion!*}
     1.6  
     1.7 +subsubsection{*The Operator @{term M_is_recfun}*}
     1.8  
     1.9  text{*Alternative definition, minimizing nesting of quantifiers around MH*}
    1.10  lemma M_is_recfun_iff:
     2.1 --- a/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 16:41:48 2002 +0200
     2.2 +++ b/src/ZF/Constructible/L_axioms.thy	Fri Aug 16 17:19:43 2002 +0200
     2.3 @@ -40,7 +40,7 @@
     2.4  apply (blast intro: transL)
     2.5  done
     2.6  
     2.7 -subsubsection{*For L to satisfy Replacement *}
     2.8 +subsection{*For L to satisfy Replacement *}
     2.9  
    2.10  (*Can't move these to Formula unless the definition of univalent is moved
    2.11  there too!*)
     3.1 --- a/src/ZF/Constructible/Rec_Separation.thy	Fri Aug 16 16:41:48 2002 +0200
     3.2 +++ b/src/ZF/Constructible/Rec_Separation.thy	Fri Aug 16 17:19:43 2002 +0200
     3.3 @@ -172,7 +172,7 @@
     3.4  done
     3.5  
     3.6  
     3.7 -subsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
     3.8 +subsubsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
     3.9  
    3.10  lemma wellfounded_trancl_reflects:
    3.11    "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
     4.1 --- a/src/ZF/Constructible/WF_absolute.thy	Fri Aug 16 16:41:48 2002 +0200
     4.2 +++ b/src/ZF/Constructible/WF_absolute.thy	Fri Aug 16 17:19:43 2002 +0200
     4.3 @@ -601,7 +601,7 @@
     4.4  apply (simp_all add: wfrec_replacement_iff trans_eq_pair_wfrec_iff) 
     4.5  done
     4.6  
     4.7 -section{*Absoluteness without assuming transitivity*}
     4.8 +subsection{*Absoluteness without assuming transitivity*}
     4.9  lemma (in M_trancl) eq_pair_wfrec_iff:
    4.10    "[|wf(r);  M(r);  M(y); 
    4.11       strong_replacement(M, \<lambda>x z. \<exists>y[M]. \<exists>g[M].
     5.1 --- a/src/ZF/Constructible/WFrec.thy	Fri Aug 16 16:41:48 2002 +0200
     5.2 +++ b/src/ZF/Constructible/WFrec.thy	Fri Aug 16 17:19:43 2002 +0200
     5.3 @@ -9,6 +9,8 @@
     5.4  theory WFrec = Wellorderings:
     5.5  
     5.6  
     5.7 +subsection{*General Lemmas*}
     5.8 +
     5.9  (*Many of these might be useful in WF.thy*)
    5.10  
    5.11  lemma apply_recfun2:
    5.12 @@ -70,6 +72,8 @@
    5.13  apply (blast intro: sym)+
    5.14  done
    5.15  
    5.16 +subsection{*Reworking of the Recursion Theory Within @{term M}*}
    5.17 +
    5.18  lemma (in M_axioms) is_recfun_separation':
    5.19      "[| f \<in> r -`` {a} \<rightarrow> range(f); g \<in> r -`` {b} \<rightarrow> range(g);
    5.20          M(r); M(f); M(g); M(a); M(b) |] 
    5.21 @@ -150,20 +154,6 @@
    5.22  apply (simp add: is_recfun_imp_function function_restrictI) 
    5.23  done
    5.24  
    5.25 -(* ideas for further weaking the H-closure premise:
    5.26 -apply (drule spec [THEN spec]) 
    5.27 -apply (erule mp)
    5.28 -apply (intro conjI)
    5.29 -apply (blast dest!: pair_components_in_M)
    5.30 -apply (blast intro!: function_restrictI dest!: pair_components_in_M)
    5.31 -apply (blast intro!: function_restrictI dest!: pair_components_in_M)
    5.32 -apply (simp only: subset_iff domain_iff restrict_iff vimage_iff) 
    5.33 -apply (simp add: vimage_singleton_iff) 
    5.34 -apply (intro allI impI conjI)
    5.35 -apply (blast intro: transM dest!: pair_components_in_M)
    5.36 -prefer 4;apply blast 
    5.37 -*)
    5.38 -
    5.39  lemma (in M_axioms) is_recfun_restrict:
    5.40       "[| wellfounded(M,r); trans(r); is_recfun(r,x,H,f); \<langle>y,x\<rangle> \<in> r; 
    5.41         M(r); M(f); 
    5.42 @@ -280,6 +270,9 @@
    5.43        apply (blast dest: transM del: rev_rallE, assumption+)
    5.44  done
    5.45  
    5.46 +
    5.47 +subsection{*Relativization of the ZF Predicate @{term is_recfun}*}
    5.48 +
    5.49  constdefs
    5.50    M_is_recfun :: "[i=>o, [i,i,i]=>o, i, i, i] => o"
    5.51     "M_is_recfun(M,MH,r,a,f) == 
    5.52 @@ -339,6 +332,10 @@
    5.53  by (simp add: is_wfrec_def wfrec_replacement_def) 
    5.54  
    5.55  
    5.56 +subsection{*Ordinal Arithmetic: Two Examples of Recursion*}
    5.57 +
    5.58 +subsubsection{*Ordinal Addition*}
    5.59 +
    5.60  (*FIXME: update to use new techniques!!*)
    5.61  constdefs
    5.62   (*This expresses ordinal addition in the language of ZF.  It also 
    5.63 @@ -485,7 +482,7 @@
    5.64  done
    5.65  
    5.66  
    5.67 -text{*Ordinal Multiplication*}
    5.68 +subsubsection{*Ordinal Multiplication*}
    5.69  
    5.70  lemma omult_eqns_unique:
    5.71       "[| omult_eqns(i,x,g,z); omult_eqns(i,x,g,z') |] ==> z=z'";