src/ZF/Constructible/Rec_Separation.thy

 (*  Title:      ZF/Constructible/Rec_Separation.thy
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-section {*Separation for Facts About Recursion*}
+section \<open>Separation for Facts About Recursion\<close>
 
 theory Rec_Separation imports Separation Internalize begin
 
-text{*This theory proves all instances needed for locales @{text
-"M_trancl"} and @{text "M_datatypes"}*}
+text\<open>This theory proves all instances needed for locales @{text
+"M_trancl"} and @{text "M_datatypes"}\<close>
 
 lemma eq_succ_imp_lt: "[|i = succ(j); Ord(i)|] ==> j<i"
 by simp
 
 
-subsection{*The Locale @{text "M_trancl"}*}
-
-subsubsection{*Separation for Reflexive/Transitive Closure*}
-
-text{*First, The Defining Formula*}
+subsection\<open>The Locale @{text "M_trancl"}\<close>
+
+subsubsection\<open>Separation for Reflexive/Transitive Closure\<close>
+
+text\<open>First, The Defining Formula\<close>
 
 (* "rtran_closure_mem(M,A,r,p) ==
       \<exists>nnat[M]. \<exists>n[M]. \<exists>n'[M].
        omega(M,nnat) & n\<in>nnat & successor(M,n,n') &
        (\<exists>f[M]. typed_function(M,n',A,f) &

                \<lambda>i x. rtran_closure_mem(##Lset(i),f(x),g(x),h(x))]"
 apply (simp only: rtran_closure_mem_def)
 apply (intro FOL_reflections function_reflections fun_plus_reflections)
 done
 
-text{*Separation for @{term "rtrancl(r)"}.*}
+text\<open>Separation for @{term "rtrancl(r)"}.\<close>
 lemma rtrancl_separation:
      "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))"
 apply (rule gen_separation_multi [OF rtran_closure_mem_reflection, of "{r,A}"],
        auto)
 apply (rule_tac env="[r,A]" in DPow_LsetI)
 apply (rule rtran_closure_mem_iff_sats sep_rules | simp)+
 done
 
 
-subsubsection{*Reflexive/Transitive Closure, Internalized*}
+subsubsection\<open>Reflexive/Transitive Closure, Internalized\<close>
 
 (*  "rtran_closure(M,r,s) ==
         \<forall>A[M]. is_field(M,r,A) \<longrightarrow>
          (\<forall>p[M]. p \<in> s \<longleftrightarrow> rtran_closure_mem(M,A,r,p))" *)
 definition

 apply (simp only: rtran_closure_def)
 apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection)
 done
 
 
-subsubsection{*Transitive Closure of a Relation, Internalized*}
+subsubsection\<open>Transitive Closure of a Relation, Internalized\<close>
 
 (*  "tran_closure(M,r,t) ==
          \<exists>s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *)
 definition
   tran_closure_fm :: "[i,i]=>i" where

 apply (intro FOL_reflections function_reflections
              rtran_closure_reflection composition_reflection)
 done
 
 
-subsubsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*}
+subsubsection\<open>Separation for the Proof of @{text "wellfounded_on_trancl"}\<close>
 
 lemma wellfounded_trancl_reflects:
   "REFLECTS[\<lambda>x. \<exists>w[L]. \<exists>wx[L]. \<exists>rp[L].
                  w \<in> Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \<in> rp,
    \<lambda>i x. \<exists>w \<in> Lset(i). \<exists>wx \<in> Lset(i). \<exists>rp \<in> Lset(i).

 apply (rule_tac env="[r,Z]" in DPow_LsetI)
 apply (rule sep_rules tran_closure_iff_sats | simp)+
 done
 
 
-subsubsection{*Instantiating the locale @{text M_trancl}*}
+subsubsection\<open>Instantiating the locale @{text M_trancl}\<close>
 
 lemma M_trancl_axioms_L: "M_trancl_axioms(L)"
   apply (rule M_trancl_axioms.intro)
    apply (assumption | rule rtrancl_separation wellfounded_trancl_separation)+
   done

 by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
 
 interpretation L?: M_trancl L by (rule M_trancl_L)
 
 
-subsection{*@{term L} is Closed Under the Operator @{term list}*}
-
-subsubsection{*Instances of Replacement for Lists*}
+subsection\<open>@{term L} is Closed Under the Operator @{term list}\<close>
+
+subsubsection\<open>Instances of Replacement for Lists\<close>
 
 lemma list_replacement1_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B \<and> (\<exists>y[L]. pair(L,u,y,x) \<and>
          is_wfrec(L, iterates_MH(L, is_list_functor(L,A), 0), memsn, u, y)),

 apply (rule_tac env="[A,B,0,nat]" in DPow_LsetI)
 apply (rule sep_rules list_functor_iff_sats is_iterates_iff_sats | simp)+
 done
 
 
-subsection{*@{term L} is Closed Under the Operator @{term formula}*}
-
-subsubsection{*Instances of Replacement for Formulas*}
+subsection\<open>@{term L} is Closed Under the Operator @{term formula}\<close>
+
+subsubsection\<open>Instances of Replacement for Formulas\<close>
 
 (*FIXME: could prove a lemma iterates_replacementI to eliminate the 
 need to expand iterates_replacement and wfrec_replacement*)
 lemma formula_replacement1_Reflects:
  "REFLECTS

        auto simp add: nonempty L_nat)
 apply (rule_tac env="[B,0,nat]" in DPow_LsetI)
 apply (rule sep_rules formula_functor_iff_sats is_iterates_iff_sats | simp)+
 done
 
-text{*NB The proofs for type @{term formula} are virtually identical to those
-for @{term "list(A)"}.  It was a cut-and-paste job! *}
-
-
-subsubsection{*The Formula @{term is_nth}, Internalized*}
+text\<open>NB The proofs for type @{term formula} are virtually identical to those
+for @{term "list(A)"}.  It was a cut-and-paste job!\<close>
+
+
+subsubsection\<open>The Formula @{term is_nth}, Internalized\<close>
 
 (* "is_nth(M,n,l,Z) ==
       \<exists>X[M]. is_iterates(M, is_tl(M), l, n, X) & is_hd(M,X,Z)" *)
 definition
   nth_fm :: "[i,i,i]=>i" where

 apply (intro FOL_reflections is_iterates_reflection
              hd_reflection tl_reflection) 
 done
 
 
-subsubsection{*An Instance of Replacement for @{term nth}*}
+subsubsection\<open>An Instance of Replacement for @{term nth}\<close>
 
 (*FIXME: could prove a lemma iterates_replacementI to eliminate the 
 need to expand iterates_replacement and wfrec_replacement*)
 lemma nth_replacement_Reflects:
  "REFLECTS

 apply (rule sep_rules is_nat_case_iff_sats tl_iff_sats
             is_wfrec_iff_sats iterates_MH_iff_sats quasinat_iff_sats | simp)+
 done
 
 
-subsubsection{*Instantiating the locale @{text M_datatypes}*}
+subsubsection\<open>Instantiating the locale @{text M_datatypes}\<close>
 
 lemma M_datatypes_axioms_L: "M_datatypes_axioms(L)"
   apply (rule M_datatypes_axioms.intro)
       apply (assumption | rule
         list_replacement1 list_replacement2

   done
 
 interpretation L?: M_datatypes L by (rule M_datatypes_L)
 
 
-subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
-
-subsubsection{*Instances of Replacement for @{term eclose}*}
+subsection\<open>@{term L} is Closed Under the Operator @{term eclose}\<close>
+
+subsubsection\<open>Instances of Replacement for @{term eclose}\<close>
 
 lemma eclose_replacement1_Reflects:
  "REFLECTS
    [\<lambda>x. \<exists>u[L]. u \<in> B & (\<exists>y[L]. pair(L,u,y,x) &
          is_wfrec(L, iterates_MH(L, big_union(L), A), memsn, u, y)),

 apply (rule_tac env="[A,B,nat]" in DPow_LsetI)
 apply (rule sep_rules is_iterates_iff_sats big_union_iff_sats | simp)+
 done
 
 
-subsubsection{*Instantiating the locale @{text M_eclose}*}
+subsubsection\<open>Instantiating the locale @{text M_eclose}\<close>
 
 lemma M_eclose_axioms_L: "M_eclose_axioms(L)"
   apply (rule M_eclose_axioms.intro)
    apply (assumption | rule eclose_replacement1 eclose_replacement2)+
   done