src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy

     finite_N: "finite (UNIV::N set)"
 and finite_in_P: "\<And> n tns. (n,tns) \<in> P \<longrightarrow> finite tns"
 and used: "\<And> n. \<exists> tns. (n,tns) \<in> P"
 
 
-subsection{* Tree basics: frontier, interior, etc. *}
+subsection{* Tree Basics: frontier, interior, etc. *}
 
 
 (* Frontier *)
 
 inductive inFr :: "N set \<Rightarrow> dtree \<Rightarrow> T \<Rightarrow> bool" where

 unfolding Itr_def apply safe
   apply (metis (lifting, mono_tags) inItr_subtr)
   by (metis inItr.Base subtr_inItr subtr_rootL_in)
 
 
-subsection{* The immediate subtree function *}
+subsection{* The Immediate Subtree Function *}
 
 (* production of: *)
 abbreviation "prodOf tr \<equiv> (id \<oplus> root) ` (cont tr)"
 (* subtree of: *)
 definition "subtrOf tr n \<equiv> SOME tr'. Inr tr' \<in> cont tr \<and> root tr' = n"

 assumes "Inr tr' \<in> cont tr"
 shows "Inr (root tr') \<in> prodOf tr"
 by (metis (lifting) assms image_iff sum_map.simps(2))
 
 
-subsection{* Well-formed derivation trees *}
+subsection{* Well-Formed Derivation Trees *}
 
 hide_const wf
 
 coinductive wf where
 dtree: "\<lbrakk>(root tr, (id \<oplus> root) ` (cont tr)) \<in> P; inj_on root (Inr -` cont tr);

   qed
   thus ?thesis using assms by auto
 qed
 
 
-subsection{* Default trees *}
+subsection{* Default Trees *}
 
 (* Pick a left-hand side of a production for each nonterminal *)
 definition S where "S n \<equiv> SOME tns. (n,tns) \<in> P"
 
 lemma S_P: "(n, S n) \<in> P"

   }
   thus ?thesis by auto
 qed
 
 
-subsection{* Hereditary substitution *}
+subsection{* Hereditary Substitution *}
 
 (* Auxiliary concept: The root-ommiting frontier: *)
 definition "inFrr ns tr t \<equiv> \<exists> tr'. Inr tr' \<in> cont tr \<and> inFr ns tr' t"
 definition "Frr ns tr \<equiv> {t. \<exists> tr'. Inr tr' \<in> cont tr \<and> t \<in> Fr ns tr'}"
 

 using inFr_self_hsubst[OF assms] unfolding Frr Fr_def by auto
 
 end (* context *)
 
 
-subsection{* Regular trees *}
+subsection{* Regular Trees *}
 
 hide_const regular
 
 definition "reg f tr \<equiv> \<forall> tr'. subtr UNIV tr' tr \<longrightarrow> tr' = f (root tr')"
 definition "regular tr \<equiv> \<exists> f. reg f tr"

 qed
 
 
 
 
-subsection {* Paths in a regular tree *}
+subsection {* Paths in a Regular Tree *}
 
 inductive path :: "(N \<Rightarrow> dtree) \<Rightarrow> N list \<Rightarrow> bool" for f where
 Base: "path f [n]"
 |
 Ind: "\<lbrakk>path f (n1 # nl); Inr (f n1) \<in> cont (f n)\<rbrakk>

 apply (metis (no_types) inFr_subtr r reg_subtr_path)
 by (metis f inFr.Base path_subtr subtr_inFr subtr_mono subtr_rootL_in)
 
 
 
-subsection{* The regular cut of a tree *}
+subsection{* The Regular Cut of a Tree *}
 
 context fixes tr0 :: dtree
 begin
 
 (* Picking a subtree of a certain root: *)

 by (metis (lifting) root_H inItr.Base reg_def reg_root subtr_rootR_in)
 
 end (* context *)
 
 
-subsection{* Recursive description of the regular tree frontiers *}
+subsection{* Recursive Description of the Regular Tree Frontiers *}
 
 lemma regular_inFr:
 assumes r: "regular tr" and In: "root tr \<in> ns"
 and t: "inFr ns tr t"
 shows "t \<in> Inl -` (cont tr) \<or>

 apply (simp, metis (full_types) mem_Collect_eq)
 apply simp
 by (simp, metis (lifting) inFr_Ind_minus insert_Diff)
 
 
-subsection{* The generated languages *}
+subsection{* The Generated Languages *}
 
 (* The (possibly inifinite tree) generated language *)
 definition "L ns n \<equiv> {Fr ns tr | tr. wf tr \<and> root tr = n}"
 
 (* The regular-tree generated language *)