src/ZF/Constructible/Rank.thy
changeset 61798 27f3c10b0b50
parent 60770 240563fbf41d
child 67399 eab6ce8368fa
     1.1 --- a/src/ZF/Constructible/Rank.thy	Mon Dec 07 10:19:30 2015 +0100
     1.2 +++ b/src/ZF/Constructible/Rank.thy	Mon Dec 07 10:23:50 2015 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4        ==> separation (M, \<lambda>x. x\<in>A \<longrightarrow> (\<exists>y[M]. (\<exists>p[M].
     1.5                       fun_apply(M,f,x,y) & pair(M,y,x,p) & p \<in> r)))"
     1.6    and obase_separation:
     1.7 -     --\<open>part of the order type formalization\<close>
     1.8 +     \<comment>\<open>part of the order type formalization\<close>
     1.9       "[| M(A); M(r) |]
    1.10        ==> separation(M, \<lambda>a. \<exists>x[M]. \<exists>g[M]. \<exists>mx[M]. \<exists>par[M].
    1.11               ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) &
    1.12 @@ -92,7 +92,7 @@
    1.13  text\<open>Following Kunen's Theorem I 7.6, page 17.  Note that this material is
    1.14  not required elsewhere.\<close>
    1.15  
    1.16 -text\<open>Can't use @{text well_ord_iso_preserving} because it needs the
    1.17 +text\<open>Can't use \<open>well_ord_iso_preserving\<close> because it needs the
    1.18  strong premise @{term "well_ord(A,r)"}\<close>
    1.19  lemma (in M_ordertype) ord_iso_pred_imp_lt:
    1.20       "[| f \<in> ord_iso(Order.pred(A,x,r), r, i, Memrel(i));
    1.21 @@ -114,7 +114,7 @@
    1.22  apply (frule restrict_ord_iso2, assumption+) 
    1.23  apply (frule ord_iso_sym [THEN ord_iso_is_bij, THEN bij_is_fun]) 
    1.24  apply (frule apply_type, blast intro: ltD) 
    1.25 -  --\<open>thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}\<close>
    1.26 +  \<comment>\<open>thus @{term "converse(f)`j \<in> Order.pred(A,x,r)"}\<close>
    1.27  apply (simp add: pred_iff) 
    1.28  apply (subgoal_tac
    1.29         "\<exists>h[M]. h \<in> ord_iso(Order.pred(A,y,r), r, 
    1.30 @@ -137,26 +137,26 @@
    1.31  
    1.32  definition  
    1.33    obase :: "[i=>o,i,i] => i" where
    1.34 -       --\<open>the domain of @{text om}, eventually shown to equal @{text A}\<close>
    1.35 +       \<comment>\<open>the domain of \<open>om\<close>, eventually shown to equal \<open>A\<close>\<close>
    1.36     "obase(M,A,r) == {a\<in>A. \<exists>x[M]. \<exists>g[M]. Ord(x) & 
    1.37                            g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x))}"
    1.38  
    1.39  definition
    1.40    omap :: "[i=>o,i,i,i] => o" where
    1.41 -    --\<open>the function that maps wosets to order types\<close>
    1.42 +    \<comment>\<open>the function that maps wosets to order types\<close>
    1.43     "omap(M,A,r,f) == 
    1.44          \<forall>z[M].
    1.45           z \<in> f \<longleftrightarrow> (\<exists>a\<in>A. \<exists>x[M]. \<exists>g[M]. z = <a,x> & Ord(x) & 
    1.46                          g \<in> ord_iso(Order.pred(A,a,r),r,x,Memrel(x)))"
    1.47  
    1.48  definition
    1.49 -  otype :: "[i=>o,i,i,i] => o" where --\<open>the order types themselves\<close>
    1.50 +  otype :: "[i=>o,i,i,i] => o" where \<comment>\<open>the order types themselves\<close>
    1.51     "otype(M,A,r,i) == \<exists>f[M]. omap(M,A,r,f) & is_range(M,f,i)"
    1.52  
    1.53  
    1.54  text\<open>Can also be proved with the premise @{term "M(z)"} instead of
    1.55        @{term "M(f)"}, but that version is less useful.  This lemma
    1.56 -      is also more useful than the definition, @{text omap_def}.\<close>
    1.57 +      is also more useful than the definition, \<open>omap_def\<close>.\<close>
    1.58  lemma (in M_ordertype) omap_iff:
    1.59       "[| omap(M,A,r,f); M(A); M(f) |] 
    1.60        ==> z \<in> f \<longleftrightarrow>
    1.61 @@ -478,7 +478,7 @@
    1.62  
    1.63  
    1.64  
    1.65 -text\<open>@{text is_oadd_fun}: Relating the pure "language of set theory" to Isabelle/ZF\<close>
    1.66 +text\<open>\<open>is_oadd_fun\<close>: Relating the pure "language of set theory" to Isabelle/ZF\<close>
    1.67  lemma (in M_ord_arith) is_oadd_fun_iff:
    1.68     "[| a\<le>j; M(i); M(j); M(a); M(f) |] 
    1.69      ==> is_oadd_fun(M,i,j,a,f) \<longleftrightarrow>
    1.70 @@ -602,7 +602,7 @@
    1.71      "[| M(i); M(x); M(g); function(g) |] 
    1.72       ==> M(THE z. omult_eqns(i, x, g, z))"
    1.73  apply (case_tac "Ord(x)")
    1.74 - prefer 2 apply (simp add: omult_eqns_Not) --\<open>trivial, non-Ord case\<close>
    1.75 + prefer 2 apply (simp add: omult_eqns_Not) \<comment>\<open>trivial, non-Ord case\<close>
    1.76  apply (erule Ord_cases) 
    1.77    apply (simp add: omult_eqns_0)
    1.78   apply (simp add: omult_eqns_succ apply_closed oadd_closed) 
    1.79 @@ -897,12 +897,12 @@
    1.80  apply (frule is_recfun_restrict [of concl: "r^+" a])
    1.81      apply (rule trans_trancl, assumption)
    1.82     apply (simp_all add: r_into_trancl trancl_subset_times)
    1.83 -txt\<open>Still the same goal, but with new @{text is_recfun} assumptions.\<close>
    1.84 +txt\<open>Still the same goal, but with new \<open>is_recfun\<close> assumptions.\<close>
    1.85  apply (simp add: wellfoundedrank_eq)
    1.86  apply (frule_tac a=a in wellfoundedrank_eq, assumption+)
    1.87     apply (simp_all add: transM [of a])
    1.88  txt\<open>We have used equations for wellfoundedrank and now must use some
    1.89 -    for  @{text is_recfun}.\<close>
    1.90 +    for  \<open>is_recfun\<close>.\<close>
    1.91  apply (rule_tac a=a in rangeI)
    1.92  apply (simp add: is_recfun_type [THEN apply_iff] vimage_singleton_iff
    1.93                   r_into_trancl apply_recfun r_into_trancl)