src/HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy
 author wenzelm Sun Nov 02 18:21:45 2014 +0100 (2014-11-02) changeset 58889 5b7a9633cfa8 parent 58309 a09ec6daaa19 child 60585 48fdff264eb2 permissions -rw-r--r--
```     1 (*  Title:      HOL/Datatype_Examples/Derivation_Trees/Gram_Lang.thy
```
```     2     Author:     Andrei Popescu, TU Muenchen
```
```     3     Copyright   2012
```
```     4
```
```     5 Language of a grammar.
```
```     6 *)
```
```     7
```
```     8 section {* Language of a Grammar *}
```
```     9
```
```    10 theory Gram_Lang
```
```    11 imports DTree "~~/src/HOL/Library/Infinite_Set"
```
```    12 begin
```
```    13
```
```    14
```
```    15 (* We assume that the sets of terminals, and the left-hand sides of
```
```    16 productions are finite and that the grammar has no unused nonterminals. *)
```
```    17 consts P :: "(N \<times> (T + N) set) set"
```
```    18 axiomatization where
```
```    19     finite_N: "finite (UNIV::N set)"
```
```    20 and finite_in_P: "\<And> n tns. (n,tns) \<in> P \<longrightarrow> finite tns"
```
```    21 and used: "\<And> n. \<exists> tns. (n,tns) \<in> P"
```
```    22
```
```    23
```
```    24 subsection{* Tree Basics: frontier, interior, etc. *}
```
```    25
```
```    26
```
```    27 (* Frontier *)
```
```    28
```
```    29 inductive inFr :: "N set \<Rightarrow> dtree \<Rightarrow> T \<Rightarrow> bool" where
```
```    30 Base: "\<lbrakk>root tr \<in> ns; Inl t \<in> cont tr\<rbrakk> \<Longrightarrow> inFr ns tr t"
```
```    31 |
```
```    32 Ind: "\<lbrakk>root tr \<in> ns; Inr tr1 \<in> cont tr; inFr ns tr1 t\<rbrakk> \<Longrightarrow> inFr ns tr t"
```
```    33
```
```    34 definition "Fr ns tr \<equiv> {t. inFr ns tr t}"
```
```    35
```
```    36 lemma inFr_root_in: "inFr ns tr t \<Longrightarrow> root tr \<in> ns"
```
```    37 by (metis inFr.simps)
```
```    38
```
```    39 lemma inFr_mono:
```
```    40 assumes "inFr ns tr t" and "ns \<subseteq> ns'"
```
```    41 shows "inFr ns' tr t"
```
```    42 using assms apply(induct arbitrary: ns' rule: inFr.induct)
```
```    43 using Base Ind by (metis inFr.simps set_mp)+
```
```    44
```
```    45 lemma inFr_Ind_minus:
```
```    46 assumes "inFr ns1 tr1 t" and "Inr tr1 \<in> cont tr"
```
```    47 shows "inFr (insert (root tr) ns1) tr t"
```
```    48 using assms apply(induct rule: inFr.induct)
```
```    49   apply (metis inFr.simps insert_iff)
```
```    50   by (metis inFr.simps inFr_mono insertI1 subset_insertI)
```
```    51
```
```    52 (* alternative definition *)
```
```    53 inductive inFr2 :: "N set \<Rightarrow> dtree \<Rightarrow> T \<Rightarrow> bool" where
```
```    54 Base: "\<lbrakk>root tr \<in> ns; Inl t \<in> cont tr\<rbrakk> \<Longrightarrow> inFr2 ns tr t"
```
```    55 |
```
```    56 Ind: "\<lbrakk>Inr tr1 \<in> cont tr; inFr2 ns1 tr1 t\<rbrakk>
```
```    57       \<Longrightarrow> inFr2 (insert (root tr) ns1) tr t"
```
```    58
```
```    59 lemma inFr2_root_in: "inFr2 ns tr t \<Longrightarrow> root tr \<in> ns"
```
```    60 apply(induct rule: inFr2.induct) by auto
```
```    61
```
```    62 lemma inFr2_mono:
```
```    63 assumes "inFr2 ns tr t" and "ns \<subseteq> ns'"
```
```    64 shows "inFr2 ns' tr t"
```
```    65 using assms apply(induct arbitrary: ns' rule: inFr2.induct)
```
```    66 using Base Ind
```
```    67 apply (metis subsetD) by (metis inFr2.simps insert_absorb insert_subset)
```
```    68
```
```    69 lemma inFr2_Ind:
```
```    70 assumes "inFr2 ns tr1 t" and "root tr \<in> ns" and "Inr tr1 \<in> cont tr"
```
```    71 shows "inFr2 ns tr t"
```
```    72 using assms apply(induct rule: inFr2.induct)
```
```    73   apply (metis inFr2.simps insert_absorb)
```
```    74   by (metis inFr2.simps insert_absorb)
```
```    75
```
```    76 lemma inFr_inFr2:
```
```    77 "inFr = inFr2"
```
```    78 apply (rule ext)+  apply(safe)
```
```    79   apply(erule inFr.induct)
```
```    80     apply (metis (lifting) inFr2.Base)
```
```    81     apply (metis (lifting) inFr2_Ind)
```
```    82   apply(erule inFr2.induct)
```
```    83     apply (metis (lifting) inFr.Base)
```
```    84     apply (metis (lifting) inFr_Ind_minus)
```
```    85 done
```
```    86
```
```    87 lemma not_root_inFr:
```
```    88 assumes "root tr \<notin> ns"
```
```    89 shows "\<not> inFr ns tr t"
```
```    90 by (metis assms inFr_root_in)
```
```    91
```
```    92 lemma not_root_Fr:
```
```    93 assumes "root tr \<notin> ns"
```
```    94 shows "Fr ns tr = {}"
```
```    95 using not_root_inFr[OF assms] unfolding Fr_def by auto
```
```    96
```
```    97
```
```    98 (* Interior *)
```
```    99
```
```   100 inductive inItr :: "N set \<Rightarrow> dtree \<Rightarrow> N \<Rightarrow> bool" where
```
```   101 Base: "root tr \<in> ns \<Longrightarrow> inItr ns tr (root tr)"
```
```   102 |
```
```   103 Ind: "\<lbrakk>root tr \<in> ns; Inr tr1 \<in> cont tr; inItr ns tr1 n\<rbrakk> \<Longrightarrow> inItr ns tr n"
```
```   104
```
```   105 definition "Itr ns tr \<equiv> {n. inItr ns tr n}"
```
```   106
```
```   107 lemma inItr_root_in: "inItr ns tr n \<Longrightarrow> root tr \<in> ns"
```
```   108 by (metis inItr.simps)
```
```   109
```
```   110 lemma inItr_mono:
```
```   111 assumes "inItr ns tr n" and "ns \<subseteq> ns'"
```
```   112 shows "inItr ns' tr n"
```
```   113 using assms apply(induct arbitrary: ns' rule: inItr.induct)
```
```   114 using Base Ind by (metis inItr.simps set_mp)+
```
```   115
```
```   116
```
```   117 (* The subtree relation *)
```
```   118
```
```   119 inductive subtr where
```
```   120 Refl: "root tr \<in> ns \<Longrightarrow> subtr ns tr tr"
```
```   121 |
```
```   122 Step: "\<lbrakk>root tr3 \<in> ns; subtr ns tr1 tr2; Inr tr2 \<in> cont tr3\<rbrakk> \<Longrightarrow> subtr ns tr1 tr3"
```
```   123
```
```   124 lemma subtr_rootL_in:
```
```   125 assumes "subtr ns tr1 tr2"
```
```   126 shows "root tr1 \<in> ns"
```
```   127 using assms apply(induct rule: subtr.induct) by auto
```
```   128
```
```   129 lemma subtr_rootR_in:
```
```   130 assumes "subtr ns tr1 tr2"
```
```   131 shows "root tr2 \<in> ns"
```
```   132 using assms apply(induct rule: subtr.induct) by auto
```
```   133
```
```   134 lemmas subtr_roots_in = subtr_rootL_in subtr_rootR_in
```
```   135
```
```   136 lemma subtr_mono:
```
```   137 assumes "subtr ns tr1 tr2" and "ns \<subseteq> ns'"
```
```   138 shows "subtr ns' tr1 tr2"
```
```   139 using assms apply(induct arbitrary: ns' rule: subtr.induct)
```
```   140 using Refl Step by (metis subtr.simps set_mp)+
```
```   141
```
```   142 lemma subtr_trans_Un:
```
```   143 assumes "subtr ns12 tr1 tr2" and "subtr ns23 tr2 tr3"
```
```   144 shows "subtr (ns12 \<union> ns23) tr1 tr3"
```
```   145 proof-
```
```   146   have "subtr ns23 tr2 tr3  \<Longrightarrow>
```
```   147         (\<forall> ns12 tr1. subtr ns12 tr1 tr2 \<longrightarrow> subtr (ns12 \<union> ns23) tr1 tr3)"
```
```   148   apply(induct  rule: subtr.induct, safe)
```
```   149     apply (metis subtr_mono sup_commute sup_ge2)
```
```   150     by (metis (lifting) Step UnI2)
```
```   151   thus ?thesis using assms by auto
```
```   152 qed
```
```   153
```
```   154 lemma subtr_trans:
```
```   155 assumes "subtr ns tr1 tr2" and "subtr ns tr2 tr3"
```
```   156 shows "subtr ns tr1 tr3"
```
```   157 using subtr_trans_Un[OF assms] by simp
```
```   158
```
```   159 lemma subtr_StepL:
```
```   160 assumes r: "root tr1 \<in> ns" and tr12: "Inr tr1 \<in> cont tr2" and s: "subtr ns tr2 tr3"
```
```   161 shows "subtr ns tr1 tr3"
```
```   162 apply(rule subtr_trans[OF _ s])
```
```   163 apply(rule Step[of tr2 ns tr1 tr1])
```
```   164 apply(rule subtr_rootL_in[OF s])
```
```   165 apply(rule Refl[OF r])
```
```   166 apply(rule tr12)
```
```   167 done
```
```   168
```
```   169 (* alternative definition: *)
```
```   170 inductive subtr2 where
```
```   171 Refl: "root tr \<in> ns \<Longrightarrow> subtr2 ns tr tr"
```
```   172 |
```
```   173 Step: "\<lbrakk>root tr1 \<in> ns; Inr tr1 \<in> cont tr2; subtr2 ns tr2 tr3\<rbrakk> \<Longrightarrow> subtr2 ns tr1 tr3"
```
```   174
```
```   175 lemma subtr2_rootL_in:
```
```   176 assumes "subtr2 ns tr1 tr2"
```
```   177 shows "root tr1 \<in> ns"
```
```   178 using assms apply(induct rule: subtr2.induct) by auto
```
```   179
```
```   180 lemma subtr2_rootR_in:
```
```   181 assumes "subtr2 ns tr1 tr2"
```
```   182 shows "root tr2 \<in> ns"
```
```   183 using assms apply(induct rule: subtr2.induct) by auto
```
```   184
```
```   185 lemmas subtr2_roots_in = subtr2_rootL_in subtr2_rootR_in
```
```   186
```
```   187 lemma subtr2_mono:
```
```   188 assumes "subtr2 ns tr1 tr2" and "ns \<subseteq> ns'"
```
```   189 shows "subtr2 ns' tr1 tr2"
```
```   190 using assms apply(induct arbitrary: ns' rule: subtr2.induct)
```
```   191 using Refl Step by (metis subtr2.simps set_mp)+
```
```   192
```
```   193 lemma subtr2_trans_Un:
```
```   194 assumes "subtr2 ns12 tr1 tr2" and "subtr2 ns23 tr2 tr3"
```
```   195 shows "subtr2 (ns12 \<union> ns23) tr1 tr3"
```
```   196 proof-
```
```   197   have "subtr2 ns12 tr1 tr2  \<Longrightarrow>
```
```   198         (\<forall> ns23 tr3. subtr2 ns23 tr2 tr3 \<longrightarrow> subtr2 (ns12 \<union> ns23) tr1 tr3)"
```
```   199   apply(induct  rule: subtr2.induct, safe)
```
```   200     apply (metis subtr2_mono sup_commute sup_ge2)
```
```   201     by (metis Un_iff subtr2.simps)
```
```   202   thus ?thesis using assms by auto
```
```   203 qed
```
```   204
```
```   205 lemma subtr2_trans:
```
```   206 assumes "subtr2 ns tr1 tr2" and "subtr2 ns tr2 tr3"
```
```   207 shows "subtr2 ns tr1 tr3"
```
```   208 using subtr2_trans_Un[OF assms] by simp
```
```   209
```
```   210 lemma subtr2_StepR:
```
```   211 assumes r: "root tr3 \<in> ns" and tr23: "Inr tr2 \<in> cont tr3" and s: "subtr2 ns tr1 tr2"
```
```   212 shows "subtr2 ns tr1 tr3"
```
```   213 apply(rule subtr2_trans[OF s])
```
```   214 apply(rule Step[of _ _ tr3])
```
```   215 apply(rule subtr2_rootR_in[OF s])
```
```   216 apply(rule tr23)
```
```   217 apply(rule Refl[OF r])
```
```   218 done
```
```   219
```
```   220 lemma subtr_subtr2:
```
```   221 "subtr = subtr2"
```
```   222 apply (rule ext)+  apply(safe)
```
```   223   apply(erule subtr.induct)
```
```   224     apply (metis (lifting) subtr2.Refl)
```
```   225     apply (metis (lifting) subtr2_StepR)
```
```   226   apply(erule subtr2.induct)
```
```   227     apply (metis (lifting) subtr.Refl)
```
```   228     apply (metis (lifting) subtr_StepL)
```
```   229 done
```
```   230
```
```   231 lemma subtr_inductL[consumes 1, case_names Refl Step]:
```
```   232 assumes s: "subtr ns tr1 tr2" and Refl: "\<And>ns tr. \<phi> ns tr tr"
```
```   233 and Step:
```
```   234 "\<And>ns tr1 tr2 tr3.
```
```   235    \<lbrakk>root tr1 \<in> ns; Inr tr1 \<in> cont tr2; subtr ns tr2 tr3; \<phi> ns tr2 tr3\<rbrakk> \<Longrightarrow> \<phi> ns tr1 tr3"
```
```   236 shows "\<phi> ns tr1 tr2"
```
```   237 using s unfolding subtr_subtr2 apply(rule subtr2.induct)
```
```   238 using Refl Step unfolding subtr_subtr2 by auto
```
```   239
```
```   240 lemma subtr_UNIV_inductL[consumes 1, case_names Refl Step]:
```
```   241 assumes s: "subtr UNIV tr1 tr2" and Refl: "\<And>tr. \<phi> tr tr"
```
```   242 and Step:
```
```   243 "\<And>tr1 tr2 tr3.
```
```   244    \<lbrakk>Inr tr1 \<in> cont tr2; subtr UNIV tr2 tr3; \<phi> tr2 tr3\<rbrakk> \<Longrightarrow> \<phi> tr1 tr3"
```
```   245 shows "\<phi> tr1 tr2"
```
```   246 using s apply(induct rule: subtr_inductL)
```
```   247 apply(rule Refl) using Step subtr_mono by (metis subset_UNIV)
```
```   248
```
```   249 (* Subtree versus frontier: *)
```
```   250 lemma subtr_inFr:
```
```   251 assumes "inFr ns tr t" and "subtr ns tr tr1"
```
```   252 shows "inFr ns tr1 t"
```
```   253 proof-
```
```   254   have "subtr ns tr tr1 \<Longrightarrow> (\<forall> t. inFr ns tr t \<longrightarrow> inFr ns tr1 t)"
```
```   255   apply(induct rule: subtr.induct, safe) by (metis inFr.Ind)
```
```   256   thus ?thesis using assms by auto
```
```   257 qed
```
```   258
```
```   259 corollary Fr_subtr:
```
```   260 "Fr ns tr = \<Union> {Fr ns tr' | tr'. subtr ns tr' tr}"
```
```   261 unfolding Fr_def proof safe
```
```   262   fix t assume t: "inFr ns tr t"  hence "root tr \<in> ns" by (rule inFr_root_in)
```
```   263   thus "t \<in> \<Union>{{t. inFr ns tr' t} |tr'. subtr ns tr' tr}"
```
```   264   apply(intro UnionI[of "{t. inFr ns tr t}" _ t]) using t subtr.Refl by auto
```
```   265 qed(metis subtr_inFr)
```
```   266
```
```   267 lemma inFr_subtr:
```
```   268 assumes "inFr ns tr t"
```
```   269 shows "\<exists> tr'. subtr ns tr' tr \<and> Inl t \<in> cont tr'"
```
```   270 using assms apply(induct rule: inFr.induct) apply safe
```
```   271   apply (metis subtr.Refl)
```
```   272   by (metis (lifting) subtr.Step)
```
```   273
```
```   274 corollary Fr_subtr_cont:
```
```   275 "Fr ns tr = \<Union> {Inl -` cont tr' | tr'. subtr ns tr' tr}"
```
```   276 unfolding Fr_def
```
```   277 apply safe
```
```   278 apply (frule inFr_subtr)
```
```   279 apply auto
```
```   280 by (metis inFr.Base subtr_inFr subtr_rootL_in)
```
```   281
```
```   282 (* Subtree versus interior: *)
```
```   283 lemma subtr_inItr:
```
```   284 assumes "inItr ns tr n" and "subtr ns tr tr1"
```
```   285 shows "inItr ns tr1 n"
```
```   286 proof-
```
```   287   have "subtr ns tr tr1 \<Longrightarrow> (\<forall> t. inItr ns tr n \<longrightarrow> inItr ns tr1 n)"
```
```   288   apply(induct rule: subtr.induct, safe) by (metis inItr.Ind)
```
```   289   thus ?thesis using assms by auto
```
```   290 qed
```
```   291
```
```   292 corollary Itr_subtr:
```
```   293 "Itr ns tr = \<Union> {Itr ns tr' | tr'. subtr ns tr' tr}"
```
```   294 unfolding Itr_def apply safe
```
```   295 apply (metis (lifting, mono_tags) UnionI inItr_root_in mem_Collect_eq subtr.Refl)
```
```   296 by (metis subtr_inItr)
```
```   297
```
```   298 lemma inItr_subtr:
```
```   299 assumes "inItr ns tr n"
```
```   300 shows "\<exists> tr'. subtr ns tr' tr \<and> root tr' = n"
```
```   301 using assms apply(induct rule: inItr.induct) apply safe
```
```   302   apply (metis subtr.Refl)
```
```   303   by (metis (lifting) subtr.Step)
```
```   304
```
```   305 corollary Itr_subtr_cont:
```
```   306 "Itr ns tr = {root tr' | tr'. subtr ns tr' tr}"
```
```   307 unfolding Itr_def apply safe
```
```   308   apply (metis (lifting, mono_tags) inItr_subtr)
```
```   309   by (metis inItr.Base subtr_inItr subtr_rootL_in)
```
```   310
```
```   311
```
```   312 subsection{* The Immediate Subtree Function *}
```
```   313
```
```   314 (* production of: *)
```
```   315 abbreviation "prodOf tr \<equiv> (id \<oplus> root) ` (cont tr)"
```
```   316 (* subtree of: *)
```
```   317 definition "subtrOf tr n \<equiv> SOME tr'. Inr tr' \<in> cont tr \<and> root tr' = n"
```
```   318
```
```   319 lemma subtrOf:
```
```   320 assumes n: "Inr n \<in> prodOf tr"
```
```   321 shows "Inr (subtrOf tr n) \<in> cont tr \<and> root (subtrOf tr n) = n"
```
```   322 proof-
```
```   323   obtain tr' where "Inr tr' \<in> cont tr \<and> root tr' = n"
```
```   324   using n unfolding image_def by (metis (lifting) Inr_oplus_elim assms)
```
```   325   thus ?thesis unfolding subtrOf_def by(rule someI)
```
```   326 qed
```
```   327
```
```   328 lemmas Inr_subtrOf = subtrOf[THEN conjunct1]
```
```   329 lemmas root_subtrOf[simp] = subtrOf[THEN conjunct2]
```
```   330
```
```   331 lemma Inl_prodOf: "Inl -` (prodOf tr) = Inl -` (cont tr)"
```
```   332 proof safe
```
```   333   fix t ttr assume "Inl t = (id \<oplus> root) ttr" and "ttr \<in> cont tr"
```
```   334   thus "t \<in> Inl -` cont tr" by(cases ttr, auto)
```
```   335 next
```
```   336   fix t assume "Inl t \<in> cont tr" thus "t \<in> Inl -` prodOf tr"
```
```   337   by (metis (lifting) id_def image_iff map_sum.simps(1) vimageI2)
```
```   338 qed
```
```   339
```
```   340 lemma root_prodOf:
```
```   341 assumes "Inr tr' \<in> cont tr"
```
```   342 shows "Inr (root tr') \<in> prodOf tr"
```
```   343 by (metis (lifting) assms image_iff map_sum.simps(2))
```
```   344
```
```   345
```
```   346 subsection{* Well-Formed Derivation Trees *}
```
```   347
```
```   348 hide_const wf
```
```   349
```
```   350 coinductive wf where
```
```   351 dtree: "\<lbrakk>(root tr, (id \<oplus> root) ` (cont tr)) \<in> P; inj_on root (Inr -` cont tr);
```
```   352         \<And> tr'. tr' \<in> Inr -` (cont tr) \<Longrightarrow> wf tr'\<rbrakk> \<Longrightarrow> wf tr"
```
```   353
```
```   354 (* destruction rules: *)
```
```   355 lemma wf_P:
```
```   356 assumes "wf tr"
```
```   357 shows "(root tr, (id \<oplus> root) ` (cont tr)) \<in> P"
```
```   358 using assms wf.simps[of tr] by auto
```
```   359
```
```   360 lemma wf_inj_on:
```
```   361 assumes "wf tr"
```
```   362 shows "inj_on root (Inr -` cont tr)"
```
```   363 using assms wf.simps[of tr] by auto
```
```   364
```
```   365 lemma wf_inj[simp]:
```
```   366 assumes "wf tr" and "Inr tr1 \<in> cont tr" and "Inr tr2 \<in> cont tr"
```
```   367 shows "root tr1 = root tr2 \<longleftrightarrow> tr1 = tr2"
```
```   368 using assms wf_inj_on unfolding inj_on_def by auto
```
```   369
```
```   370 lemma wf_cont:
```
```   371 assumes "wf tr" and "Inr tr' \<in> cont tr"
```
```   372 shows "wf tr'"
```
```   373 using assms wf.simps[of tr] by auto
```
```   374
```
```   375
```
```   376 (* coinduction:*)
```
```   377 lemma wf_coind[elim, consumes 1, case_names Hyp]:
```
```   378 assumes phi: "\<phi> tr"
```
```   379 and Hyp:
```
```   380 "\<And> tr. \<phi> tr \<Longrightarrow>
```
```   381        (root tr, image (id \<oplus> root) (cont tr)) \<in> P \<and>
```
```   382        inj_on root (Inr -` cont tr) \<and>
```
```   383        (\<forall> tr' \<in> Inr -` (cont tr). \<phi> tr' \<or> wf tr')"
```
```   384 shows "wf tr"
```
```   385 apply(rule wf.coinduct[of \<phi> tr, OF phi])
```
```   386 using Hyp by blast
```
```   387
```
```   388 lemma wf_raw_coind[elim, consumes 1, case_names Hyp]:
```
```   389 assumes phi: "\<phi> tr"
```
```   390 and Hyp:
```
```   391 "\<And> tr. \<phi> tr \<Longrightarrow>
```
```   392        (root tr, image (id \<oplus> root) (cont tr)) \<in> P \<and>
```
```   393        inj_on root (Inr -` cont tr) \<and>
```
```   394        (\<forall> tr' \<in> Inr -` (cont tr). \<phi> tr')"
```
```   395 shows "wf tr"
```
```   396 using phi apply(induct rule: wf_coind)
```
```   397 using Hyp by (metis (mono_tags))
```
```   398
```
```   399 lemma wf_subtr_inj_on:
```
```   400 assumes d: "wf tr1" and s: "subtr ns tr tr1"
```
```   401 shows "inj_on root (Inr -` cont tr)"
```
```   402 using s d apply(induct rule: subtr.induct)
```
```   403 apply (metis (lifting) wf_inj_on) by (metis wf_cont)
```
```   404
```
```   405 lemma wf_subtr_P:
```
```   406 assumes d: "wf tr1" and s: "subtr ns tr tr1"
```
```   407 shows "(root tr, (id \<oplus> root) ` cont tr) \<in> P"
```
```   408 using s d apply(induct rule: subtr.induct)
```
```   409 apply (metis (lifting) wf_P) by (metis wf_cont)
```
```   410
```
```   411 lemma subtrOf_root[simp]:
```
```   412 assumes tr: "wf tr" and cont: "Inr tr' \<in> cont tr"
```
```   413 shows "subtrOf tr (root tr') = tr'"
```
```   414 proof-
```
```   415   have 0: "Inr (subtrOf tr (root tr')) \<in> cont tr" using Inr_subtrOf
```
```   416   by (metis (lifting) cont root_prodOf)
```
```   417   have "root (subtrOf tr (root tr')) = root tr'"
```
```   418   using root_subtrOf by (metis (lifting) cont root_prodOf)
```
```   419   thus ?thesis unfolding wf_inj[OF tr 0 cont] .
```
```   420 qed
```
```   421
```
```   422 lemma surj_subtrOf:
```
```   423 assumes "wf tr" and 0: "Inr tr' \<in> cont tr"
```
```   424 shows "\<exists> n. Inr n \<in> prodOf tr \<and> subtrOf tr n = tr'"
```
```   425 apply(rule exI[of _ "root tr'"])
```
```   426 using root_prodOf[OF 0] subtrOf_root[OF assms] by simp
```
```   427
```
```   428 lemma wf_subtr:
```
```   429 assumes "wf tr1" and "subtr ns tr tr1"
```
```   430 shows "wf tr"
```
```   431 proof-
```
```   432   have "(\<exists> ns tr1. wf tr1 \<and> subtr ns tr tr1) \<Longrightarrow> wf tr"
```
```   433   proof (induct rule: wf_raw_coind)
```
```   434     case (Hyp tr)
```
```   435     then obtain ns tr1 where tr1: "wf tr1" and tr_tr1: "subtr ns tr tr1" by auto
```
```   436     show ?case proof safe
```
```   437       show "(root tr, (id \<oplus> root) ` cont tr) \<in> P" using wf_subtr_P[OF tr1 tr_tr1] .
```
```   438     next
```
```   439       show "inj_on root (Inr -` cont tr)" using wf_subtr_inj_on[OF tr1 tr_tr1] .
```
```   440     next
```
```   441       fix tr' assume tr': "Inr tr' \<in> cont tr"
```
```   442       have tr_tr1: "subtr (ns \<union> {root tr'}) tr tr1" using subtr_mono[OF tr_tr1] by auto
```
```   443       have "subtr (ns \<union> {root tr'}) tr' tr1" using subtr_StepL[OF _ tr' tr_tr1] by auto
```
```   444       thus "\<exists>ns' tr1. wf tr1 \<and> subtr ns' tr' tr1" using tr1 by blast
```
```   445     qed
```
```   446   qed
```
```   447   thus ?thesis using assms by auto
```
```   448 qed
```
```   449
```
```   450
```
```   451 subsection{* Default Trees *}
```
```   452
```
```   453 (* Pick a left-hand side of a production for each nonterminal *)
```
```   454 definition S where "S n \<equiv> SOME tns. (n,tns) \<in> P"
```
```   455
```
```   456 lemma S_P: "(n, S n) \<in> P"
```
```   457 using used unfolding S_def by(rule someI_ex)
```
```   458
```
```   459 lemma finite_S: "finite (S n)"
```
```   460 using S_P finite_in_P by auto
```
```   461
```
```   462
```
```   463 (* The default tree of a nonterminal *)
```
```   464 definition deftr :: "N \<Rightarrow> dtree" where
```
```   465 "deftr \<equiv> unfold id S"
```
```   466
```
```   467 lemma deftr_simps[simp]:
```
```   468 "root (deftr n) = n"
```
```   469 "cont (deftr n) = image (id \<oplus> deftr) (S n)"
```
```   470 using unfold(1)[of id S n] unfold(2)[of S n id, OF finite_S]
```
```   471 unfolding deftr_def by simp_all
```
```   472
```
```   473 lemmas root_deftr = deftr_simps(1)
```
```   474 lemmas cont_deftr = deftr_simps(2)
```
```   475
```
```   476 lemma root_o_deftr[simp]: "root o deftr = id"
```
```   477 by (rule ext, auto)
```
```   478
```
```   479 lemma wf_deftr: "wf (deftr n)"
```
```   480 proof-
```
```   481   {fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
```
```   482    apply(induct rule: wf_raw_coind) apply safe
```
```   483    unfolding deftr_simps image_comp map_sum.comp id_comp
```
```   484    root_o_deftr map_sum.id image_id id_apply apply(rule S_P)
```
```   485    unfolding inj_on_def by auto
```
```   486   }
```
```   487   thus ?thesis by auto
```
```   488 qed
```
```   489
```
```   490
```
```   491 subsection{* Hereditary Substitution *}
```
```   492
```
```   493 (* Auxiliary concept: The root-ommiting frontier: *)
```
```   494 definition "inFrr ns tr t \<equiv> \<exists> tr'. Inr tr' \<in> cont tr \<and> inFr ns tr' t"
```
```   495 definition "Frr ns tr \<equiv> {t. \<exists> tr'. Inr tr' \<in> cont tr \<and> t \<in> Fr ns tr'}"
```
```   496
```
```   497 context
```
```   498 fixes tr0 :: dtree
```
```   499 begin
```
```   500
```
```   501 definition "hsubst_r tr \<equiv> root tr"
```
```   502 definition "hsubst_c tr \<equiv> if root tr = root tr0 then cont tr0 else cont tr"
```
```   503
```
```   504 (* Hereditary substitution: *)
```
```   505 definition hsubst :: "dtree \<Rightarrow> dtree" where
```
```   506 "hsubst \<equiv> unfold hsubst_r hsubst_c"
```
```   507
```
```   508 lemma finite_hsubst_c: "finite (hsubst_c n)"
```
```   509 unfolding hsubst_c_def by (metis (full_types) finite_cont)
```
```   510
```
```   511 lemma root_hsubst[simp]: "root (hsubst tr) = root tr"
```
```   512 using unfold(1)[of hsubst_r hsubst_c tr] unfolding hsubst_def hsubst_r_def by simp
```
```   513
```
```   514 lemma root_o_subst[simp]: "root o hsubst = root"
```
```   515 unfolding comp_def root_hsubst ..
```
```   516
```
```   517 lemma cont_hsubst_eq[simp]:
```
```   518 assumes "root tr = root tr0"
```
```   519 shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr0)"
```
```   520 apply(subst id_comp[symmetric, of id]) unfolding id_comp
```
```   521 using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
```
```   522 unfolding hsubst_def hsubst_c_def using assms by simp
```
```   523
```
```   524 lemma hsubst_eq:
```
```   525 assumes "root tr = root tr0"
```
```   526 shows "hsubst tr = hsubst tr0"
```
```   527 apply(rule dtree_cong) using assms cont_hsubst_eq by auto
```
```   528
```
```   529 lemma cont_hsubst_neq[simp]:
```
```   530 assumes "root tr \<noteq> root tr0"
```
```   531 shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr)"
```
```   532 apply(subst id_comp[symmetric, of id]) unfolding id_comp
```
```   533 using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
```
```   534 unfolding hsubst_def hsubst_c_def using assms by simp
```
```   535
```
```   536 lemma Inl_cont_hsubst_eq[simp]:
```
```   537 assumes "root tr = root tr0"
```
```   538 shows "Inl -` cont (hsubst tr) = Inl -` (cont tr0)"
```
```   539 unfolding cont_hsubst_eq[OF assms] by simp
```
```   540
```
```   541 lemma Inr_cont_hsubst_eq[simp]:
```
```   542 assumes "root tr = root tr0"
```
```   543 shows "Inr -` cont (hsubst tr) = hsubst ` Inr -` cont tr0"
```
```   544 unfolding cont_hsubst_eq[OF assms] by simp
```
```   545
```
```   546 lemma Inl_cont_hsubst_neq[simp]:
```
```   547 assumes "root tr \<noteq> root tr0"
```
```   548 shows "Inl -` cont (hsubst tr) = Inl -` (cont tr)"
```
```   549 unfolding cont_hsubst_neq[OF assms] by simp
```
```   550
```
```   551 lemma Inr_cont_hsubst_neq[simp]:
```
```   552 assumes "root tr \<noteq> root tr0"
```
```   553 shows "Inr -` cont (hsubst tr) = hsubst ` Inr -` cont tr"
```
```   554 unfolding cont_hsubst_neq[OF assms] by simp
```
```   555
```
```   556 lemma wf_hsubst:
```
```   557 assumes tr0: "wf tr0" and tr: "wf tr"
```
```   558 shows "wf (hsubst tr)"
```
```   559 proof-
```
```   560   {fix tr1 have "(\<exists> tr. wf tr \<and> tr1 = hsubst tr) \<Longrightarrow> wf tr1"
```
```   561    proof (induct rule: wf_raw_coind)
```
```   562      case (Hyp tr1) then obtain tr
```
```   563      where dtr: "wf tr" and tr1: "tr1 = hsubst tr" by auto
```
```   564      show ?case unfolding tr1 proof safe
```
```   565        show "(root (hsubst tr), prodOf (hsubst tr)) \<in> P"
```
```   566        unfolding tr1 apply(cases "root tr = root tr0")
```
```   567        using  wf_P[OF dtr] wf_P[OF tr0]
```
```   568        by (auto simp add: image_comp map_sum.comp)
```
```   569        show "inj_on root (Inr -` cont (hsubst tr))"
```
```   570        apply(cases "root tr = root tr0") using wf_inj_on[OF dtr] wf_inj_on[OF tr0]
```
```   571        unfolding inj_on_def by (auto, blast)
```
```   572        fix tr' assume "Inr tr' \<in> cont (hsubst tr)"
```
```   573        thus "\<exists>tra. wf tra \<and> tr' = hsubst tra"
```
```   574        apply(cases "root tr = root tr0", simp_all)
```
```   575          apply (metis wf_cont tr0)
```
```   576          by (metis dtr wf_cont)
```
```   577      qed
```
```   578    qed
```
```   579   }
```
```   580   thus ?thesis using assms by blast
```
```   581 qed
```
```   582
```
```   583 lemma Frr: "Frr ns tr = {t. inFrr ns tr t}"
```
```   584 unfolding inFrr_def Frr_def Fr_def by auto
```
```   585
```
```   586 lemma inFr_hsubst_imp:
```
```   587 assumes "inFr ns (hsubst tr) t"
```
```   588 shows "t \<in> Inl -` (cont tr0) \<or> inFrr (ns - {root tr0}) tr0 t \<or>
```
```   589        inFr (ns - {root tr0}) tr t"
```
```   590 proof-
```
```   591   {fix tr1
```
```   592    have "inFr ns tr1 t \<Longrightarrow>
```
```   593    (\<And> tr. tr1 = hsubst tr \<Longrightarrow> (t \<in> Inl -` (cont tr0) \<or> inFrr (ns - {root tr0}) tr0 t \<or>
```
```   594                               inFr (ns - {root tr0}) tr t))"
```
```   595    proof(induct rule: inFr.induct)
```
```   596      case (Base tr1 ns t tr)
```
```   597      hence rtr: "root tr1 \<in> ns" and t_tr1: "Inl t \<in> cont tr1" and tr1: "tr1 = hsubst tr"
```
```   598      by auto
```
```   599      show ?case
```
```   600      proof(cases "root tr1 = root tr0")
```
```   601        case True
```
```   602        hence "t \<in> Inl -` (cont tr0)" using t_tr1 unfolding tr1 by auto
```
```   603        thus ?thesis by simp
```
```   604      next
```
```   605        case False
```
```   606        hence "inFr (ns - {root tr0}) tr t" using t_tr1 unfolding tr1 apply simp
```
```   607        by (metis Base.prems Diff_iff root_hsubst inFr.Base rtr singletonE)
```
```   608        thus ?thesis by simp
```
```   609      qed
```
```   610    next
```
```   611      case (Ind tr1 ns tr1' t) note IH = Ind(4)
```
```   612      have rtr1: "root tr1 \<in> ns" and tr1'_tr1: "Inr tr1' \<in> cont tr1"
```
```   613      and t_tr1': "inFr ns tr1' t" and tr1: "tr1 = hsubst tr" using Ind by auto
```
```   614      have rtr1: "root tr1 = root tr" unfolding tr1 by simp
```
```   615      show ?case
```
```   616      proof(cases "root tr1 = root tr0")
```
```   617        case True
```
```   618        then obtain tr' where tr'_tr0: "Inr tr' \<in> cont tr0" and tr1': "tr1' = hsubst tr'"
```
```   619        using tr1'_tr1 unfolding tr1 by auto
```
```   620        show ?thesis using IH[OF tr1'] proof (elim disjE)
```
```   621          assume "inFr (ns - {root tr0}) tr' t"
```
```   622          thus ?thesis using tr'_tr0 unfolding inFrr_def by auto
```
```   623        qed auto
```
```   624      next
```
```   625        case False
```
```   626        then obtain tr' where tr'_tr: "Inr tr' \<in> cont tr" and tr1': "tr1' = hsubst tr'"
```
```   627        using tr1'_tr1 unfolding tr1 by auto
```
```   628        show ?thesis using IH[OF tr1'] proof (elim disjE)
```
```   629          assume "inFr (ns - {root tr0}) tr' t"
```
```   630          thus ?thesis using tr'_tr unfolding inFrr_def
```
```   631          by (metis Diff_iff False Ind(1) empty_iff inFr2_Ind inFr_inFr2 insert_iff rtr1)
```
```   632        qed auto
```
```   633      qed
```
```   634    qed
```
```   635   }
```
```   636   thus ?thesis using assms by auto
```
```   637 qed
```
```   638
```
```   639 lemma inFr_hsubst_notin:
```
```   640 assumes "inFr ns tr t" and "root tr0 \<notin> ns"
```
```   641 shows "inFr ns (hsubst tr) t"
```
```   642 using assms apply(induct rule: inFr.induct)
```
```   643 apply (metis Inl_cont_hsubst_neq inFr2.Base inFr_inFr2 root_hsubst vimageD vimageI2)
```
```   644 by (metis (lifting) Inr_cont_hsubst_neq inFr.Ind rev_image_eqI root_hsubst vimageD vimageI2)
```
```   645
```
```   646 lemma inFr_hsubst_minus:
```
```   647 assumes "inFr (ns - {root tr0}) tr t"
```
```   648 shows "inFr ns (hsubst tr) t"
```
```   649 proof-
```
```   650   have 1: "inFr (ns - {root tr0}) (hsubst tr) t"
```
```   651   using inFr_hsubst_notin[OF assms] by simp
```
```   652   show ?thesis using inFr_mono[OF 1] by auto
```
```   653 qed
```
```   654
```
```   655 lemma inFr_self_hsubst:
```
```   656 assumes "root tr0 \<in> ns"
```
```   657 shows
```
```   658 "inFr ns (hsubst tr0) t \<longleftrightarrow>
```
```   659  t \<in> Inl -` (cont tr0) \<or> inFrr (ns - {root tr0}) tr0 t"
```
```   660 (is "?A \<longleftrightarrow> ?B \<or> ?C")
```
```   661 apply(intro iffI)
```
```   662 apply (metis inFr_hsubst_imp Diff_iff inFr_root_in insertI1) proof(elim disjE)
```
```   663   assume ?B thus ?A apply(intro inFr.Base) using assms by auto
```
```   664 next
```
```   665   assume ?C then obtain tr where
```
```   666   tr_tr0: "Inr tr \<in> cont tr0" and t_tr: "inFr (ns - {root tr0}) tr t"
```
```   667   unfolding inFrr_def by auto
```
```   668   def tr1 \<equiv> "hsubst tr"
```
```   669   have 1: "inFr ns tr1 t" using t_tr unfolding tr1_def using inFr_hsubst_minus by auto
```
```   670   have "Inr tr1 \<in> cont (hsubst tr0)" unfolding tr1_def using tr_tr0 by auto
```
```   671   thus ?A using 1 inFr.Ind assms by (metis root_hsubst)
```
```   672 qed
```
```   673
```
```   674 lemma Fr_self_hsubst:
```
```   675 assumes "root tr0 \<in> ns"
```
```   676 shows "Fr ns (hsubst tr0) = Inl -` (cont tr0) \<union> Frr (ns - {root tr0}) tr0"
```
```   677 using inFr_self_hsubst[OF assms] unfolding Frr Fr_def by auto
```
```   678
```
```   679 end (* context *)
```
```   680
```
```   681
```
```   682 subsection{* Regular Trees *}
```
```   683
```
```   684 definition "reg f tr \<equiv> \<forall> tr'. subtr UNIV tr' tr \<longrightarrow> tr' = f (root tr')"
```
```   685 definition "regular tr \<equiv> \<exists> f. reg f tr"
```
```   686
```
```   687 lemma reg_def2: "reg f tr \<longleftrightarrow> (\<forall> ns tr'. subtr ns tr' tr \<longrightarrow> tr' = f (root tr'))"
```
```   688 unfolding reg_def using subtr_mono by (metis subset_UNIV)
```
```   689
```
```   690 lemma regular_def2: "regular tr \<longleftrightarrow> (\<exists> f. reg f tr \<and> (\<forall> n. root (f n) = n))"
```
```   691 unfolding regular_def proof safe
```
```   692   fix f assume f: "reg f tr"
```
```   693   def g \<equiv> "\<lambda> n. if inItr UNIV tr n then f n else deftr n"
```
```   694   show "\<exists>g. reg g tr \<and> (\<forall>n. root (g n) = n)"
```
```   695   apply(rule exI[of _ g])
```
```   696   using f deftr_simps(1) unfolding g_def reg_def apply safe
```
```   697     apply (metis (lifting) inItr.Base subtr_inItr subtr_rootL_in)
```
```   698     by (metis (full_types) inItr_subtr)
```
```   699 qed auto
```
```   700
```
```   701 lemma reg_root:
```
```   702 assumes "reg f tr"
```
```   703 shows "f (root tr) = tr"
```
```   704 using assms unfolding reg_def
```
```   705 by (metis (lifting) iso_tuple_UNIV_I subtr.Refl)
```
```   706
```
```   707
```
```   708 lemma reg_Inr_cont:
```
```   709 assumes "reg f tr" and "Inr tr' \<in> cont tr"
```
```   710 shows "reg f tr'"
```
```   711 by (metis (lifting) assms iso_tuple_UNIV_I reg_def subtr.Step)
```
```   712
```
```   713 lemma reg_subtr:
```
```   714 assumes "reg f tr" and "subtr ns tr' tr"
```
```   715 shows "reg f tr'"
```
```   716 using assms unfolding reg_def using subtr_trans[of UNIV tr] UNIV_I
```
```   717 by (metis UNIV_eq_I UnCI Un_upper1 iso_tuple_UNIV_I subtr_mono subtr_trans)
```
```   718
```
```   719 lemma regular_subtr:
```
```   720 assumes r: "regular tr" and s: "subtr ns tr' tr"
```
```   721 shows "regular tr'"
```
```   722 using r reg_subtr[OF _ s] unfolding regular_def by auto
```
```   723
```
```   724 lemma subtr_deftr:
```
```   725 assumes "subtr ns tr' (deftr n)"
```
```   726 shows "tr' = deftr (root tr')"
```
```   727 proof-
```
```   728   {fix tr have "subtr ns tr' tr \<Longrightarrow> (\<forall> n. tr = deftr n \<longrightarrow> tr' = deftr (root tr'))"
```
```   729    apply (induct rule: subtr.induct)
```
```   730    proof(metis (lifting) deftr_simps(1), safe)
```
```   731      fix tr3 ns tr1 tr2 n
```
```   732      assume 1: "root (deftr n) \<in> ns" and 2: "subtr ns tr1 tr2"
```
```   733      and IH: "\<forall>n. tr2 = deftr n \<longrightarrow> tr1 = deftr (root tr1)"
```
```   734      and 3: "Inr tr2 \<in> cont (deftr n)"
```
```   735      have "tr2 \<in> deftr ` UNIV"
```
```   736      using 3 unfolding deftr_simps image_def
```
```   737      by (metis (lifting, full_types) 3 CollectI Inr_oplus_iff cont_deftr
```
```   738          iso_tuple_UNIV_I)
```
```   739      then obtain n where "tr2 = deftr n" by auto
```
```   740      thus "tr1 = deftr (root tr1)" using IH by auto
```
```   741    qed
```
```   742   }
```
```   743   thus ?thesis using assms by auto
```
```   744 qed
```
```   745
```
```   746 lemma reg_deftr: "reg deftr (deftr n)"
```
```   747 unfolding reg_def using subtr_deftr by auto
```
```   748
```
```   749 lemma wf_subtrOf_Union:
```
```   750 assumes "wf tr"
```
```   751 shows "\<Union>{K tr' |tr'. Inr tr' \<in> cont tr} =
```
```   752        \<Union>{K (subtrOf tr n) |n. Inr n \<in> prodOf tr}"
```
```   753 unfolding Union_eq Bex_def mem_Collect_eq proof safe
```
```   754   fix x xa tr'
```
```   755   assume x: "x \<in> K tr'" and tr'_tr: "Inr tr' \<in> cont tr"
```
```   756   show "\<exists>X. (\<exists>n. X = K (subtrOf tr n) \<and> Inr n \<in> prodOf tr) \<and> x \<in> X"
```
```   757   apply(rule exI[of _ "K (subtrOf tr (root tr'))"]) apply(intro conjI)
```
```   758     apply(rule exI[of _ "root tr'"]) apply (metis (lifting) root_prodOf tr'_tr)
```
```   759     by (metis (lifting) assms subtrOf_root tr'_tr x)
```
```   760 next
```
```   761   fix x X n ttr
```
```   762   assume x: "x \<in> K (subtrOf tr n)" and n: "Inr n = (id \<oplus> root) ttr" and ttr: "ttr \<in> cont tr"
```
```   763   show "\<exists>X. (\<exists>tr'. X = K tr' \<and> Inr tr' \<in> cont tr) \<and> x \<in> X"
```
```   764   apply(rule exI[of _ "K (subtrOf tr n)"]) apply(intro conjI)
```
```   765     apply(rule exI[of _ "subtrOf tr n"]) apply (metis imageI n subtrOf ttr)
```
```   766     using x .
```
```   767 qed
```
```   768
```
```   769
```
```   770
```
```   771
```
```   772 subsection {* Paths in a Regular Tree *}
```
```   773
```
```   774 inductive path :: "(N \<Rightarrow> dtree) \<Rightarrow> N list \<Rightarrow> bool" for f where
```
```   775 Base: "path f [n]"
```
```   776 |
```
```   777 Ind: "\<lbrakk>path f (n1 # nl); Inr (f n1) \<in> cont (f n)\<rbrakk>
```
```   778       \<Longrightarrow> path f (n # n1 # nl)"
```
```   779
```
```   780 lemma path_NE:
```
```   781 assumes "path f nl"
```
```   782 shows "nl \<noteq> Nil"
```
```   783 using assms apply(induct rule: path.induct) by auto
```
```   784
```
```   785 lemma path_post:
```
```   786 assumes f: "path f (n # nl)" and nl: "nl \<noteq> []"
```
```   787 shows "path f nl"
```
```   788 proof-
```
```   789   obtain n1 nl1 where nl: "nl = n1 # nl1" using nl by (cases nl, auto)
```
```   790   show ?thesis using assms unfolding nl using path.simps by (metis (lifting) list.inject)
```
```   791 qed
```
```   792
```
```   793 lemma path_post_concat:
```
```   794 assumes "path f (nl1 @ nl2)" and "nl2 \<noteq> Nil"
```
```   795 shows "path f nl2"
```
```   796 using assms apply (induct nl1)
```
```   797 apply (metis append_Nil) by (metis Nil_is_append_conv append_Cons path_post)
```
```   798
```
```   799 lemma path_concat:
```
```   800 assumes "path f nl1" and "path f ((last nl1) # nl2)"
```
```   801 shows "path f (nl1 @ nl2)"
```
```   802 using assms apply(induct rule: path.induct) apply simp
```
```   803 by (metis append_Cons last.simps list.simps(3) path.Ind)
```
```   804
```
```   805 lemma path_distinct:
```
```   806 assumes "path f nl"
```
```   807 shows "\<exists> nl'. path f nl' \<and> hd nl' = hd nl \<and> last nl' = last nl \<and>
```
```   808               set nl' \<subseteq> set nl \<and> distinct nl'"
```
```   809 using assms proof(induct rule: length_induct)
```
```   810   case (1 nl)  hence p_nl: "path f nl" by simp
```
```   811   then obtain n nl1 where nl: "nl = n # nl1" by (metis list.exhaust path_NE)
```
```   812   show ?case
```
```   813   proof(cases nl1)
```
```   814     case Nil
```
```   815     show ?thesis apply(rule exI[of _ nl]) using path.Base unfolding nl Nil by simp
```
```   816   next
```
```   817     case (Cons n1 nl2)
```
```   818     hence p1: "path f nl1" by (metis list.simps(3) nl p_nl path_post)
```
```   819     show ?thesis
```
```   820     proof(cases "n \<in> set nl1")
```
```   821       case False
```
```   822       obtain nl1' where p1': "path f nl1'" and hd_nl1': "hd nl1' = hd nl1" and
```
```   823       l_nl1': "last nl1' = last nl1" and d_nl1': "distinct nl1'"
```
```   824       and s_nl1': "set nl1' \<subseteq> set nl1"
```
```   825       using 1(1)[THEN allE[of _ nl1]] p1 unfolding nl by auto
```
```   826       obtain nl2' where nl1': "nl1' = n1 # nl2'" using path_NE[OF p1'] hd_nl1'
```
```   827       unfolding Cons by(cases nl1', auto)
```
```   828       show ?thesis apply(intro exI[of _ "n # nl1'"]) unfolding nl proof safe
```
```   829         show "path f (n # nl1')" unfolding nl1'
```
```   830         apply(rule path.Ind, metis nl1' p1')
```
```   831         by (metis (lifting) Cons list.inject nl p1 p_nl path.simps path_NE)
```
```   832       qed(insert l_nl1' Cons nl1' s_nl1' d_nl1' False, auto)
```
```   833     next
```
```   834       case True
```
```   835       then obtain nl11 nl12 where nl1: "nl1 = nl11 @ n # nl12"
```
```   836       by (metis split_list)
```
```   837       have p12: "path f (n # nl12)"
```
```   838       apply(rule path_post_concat[of _ "n # nl11"]) using p_nl[unfolded nl nl1] by auto
```
```   839       obtain nl12' where p1': "path f nl12'" and hd_nl12': "hd nl12' = n" and
```
```   840       l_nl12': "last nl12' = last (n # nl12)" and d_nl12': "distinct nl12'"
```
```   841       and s_nl12': "set nl12' \<subseteq> {n} \<union> set nl12"
```
```   842       using 1(1)[THEN allE[of _ "n # nl12"]] p12 unfolding nl nl1 by auto
```
```   843       thus ?thesis apply(intro exI[of _ nl12']) unfolding nl nl1 by auto
```
```   844     qed
```
```   845   qed
```
```   846 qed
```
```   847
```
```   848 lemma path_subtr:
```
```   849 assumes f: "\<And> n. root (f n) = n"
```
```   850 and p: "path f nl"
```
```   851 shows "subtr (set nl) (f (last nl)) (f (hd nl))"
```
```   852 using p proof (induct rule: path.induct)
```
```   853   case (Ind n1 nl n)  let ?ns1 = "insert n1 (set nl)"
```
```   854   have "path f (n1 # nl)"
```
```   855   and "subtr ?ns1 (f (last (n1 # nl))) (f n1)"
```
```   856   and fn1: "Inr (f n1) \<in> cont (f n)" using Ind by simp_all
```
```   857   hence fn1_flast:  "subtr (insert n ?ns1) (f (last (n1 # nl))) (f n1)"
```
```   858   by (metis subset_insertI subtr_mono)
```
```   859   have 1: "last (n # n1 # nl) = last (n1 # nl)" by auto
```
```   860   have "subtr (insert n ?ns1) (f (last (n1 # nl))) (f n)"
```
```   861   using f subtr.Step[OF _ fn1_flast fn1] by auto
```
```   862   thus ?case unfolding 1 by simp
```
```   863 qed (metis f list.sel(1) last_ConsL last_in_set not_Cons_self2 subtr.Refl)
```
```   864
```
```   865 lemma reg_subtr_path_aux:
```
```   866 assumes f: "reg f tr" and n: "subtr ns tr1 tr"
```
```   867 shows "\<exists> nl. path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and> set nl \<subseteq> ns"
```
```   868 using n f proof(induct rule: subtr.induct)
```
```   869   case (Refl tr ns)
```
```   870   thus ?case
```
```   871   apply(intro exI[of _ "[root tr]"]) apply simp by (metis (lifting) path.Base reg_root)
```
```   872 next
```
```   873   case (Step tr ns tr2 tr1)
```
```   874   hence rtr: "root tr \<in> ns" and tr1_tr: "Inr tr1 \<in> cont tr"
```
```   875   and tr2_tr1: "subtr ns tr2 tr1" and tr: "reg f tr" by auto
```
```   876   have tr1: "reg f tr1" using reg_subtr[OF tr] rtr tr1_tr
```
```   877   by (metis (lifting) Step.prems iso_tuple_UNIV_I reg_def subtr.Step)
```
```   878   obtain nl where nl: "path f nl" and f_nl: "f (hd nl) = tr1"
```
```   879   and last_nl: "f (last nl) = tr2" and set: "set nl \<subseteq> ns" using Step(3)[OF tr1] by auto
```
```   880   have 0: "path f (root tr # nl)" apply (subst path.simps)
```
```   881   using f_nl nl reg_root tr tr1_tr by (metis list.sel(1) neq_Nil_conv)
```
```   882   show ?case apply(rule exI[of _ "(root tr) # nl"])
```
```   883   using 0 reg_root tr last_nl nl path_NE rtr set by auto
```
```   884 qed
```
```   885
```
```   886 lemma reg_subtr_path:
```
```   887 assumes f: "reg f tr" and n: "subtr ns tr1 tr"
```
```   888 shows "\<exists> nl. distinct nl \<and> path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and> set nl \<subseteq> ns"
```
```   889 using reg_subtr_path_aux[OF assms] path_distinct[of f]
```
```   890 by (metis (lifting) order_trans)
```
```   891
```
```   892 lemma subtr_iff_path:
```
```   893 assumes r: "reg f tr" and f: "\<And> n. root (f n) = n"
```
```   894 shows "subtr ns tr1 tr \<longleftrightarrow>
```
```   895        (\<exists> nl. distinct nl \<and> path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and> set nl \<subseteq> ns)"
```
```   896 proof safe
```
```   897   fix nl assume p: "path f nl" and nl: "set nl \<subseteq> ns"
```
```   898   have "subtr (set nl) (f (last nl)) (f (hd nl))"
```
```   899   apply(rule path_subtr) using p f by simp_all
```
```   900   thus "subtr ns (f (last nl)) (f (hd nl))"
```
```   901   using subtr_mono nl by auto
```
```   902 qed(insert reg_subtr_path[OF r], auto)
```
```   903
```
```   904 lemma inFr_iff_path:
```
```   905 assumes r: "reg f tr" and f: "\<And> n. root (f n) = n"
```
```   906 shows
```
```   907 "inFr ns tr t \<longleftrightarrow>
```
```   908  (\<exists> nl tr1. distinct nl \<and> path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and>
```
```   909             set nl \<subseteq> ns \<and> Inl t \<in> cont tr1)"
```
```   910 apply safe
```
```   911 apply (metis (no_types) inFr_subtr r reg_subtr_path)
```
```   912 by (metis f inFr.Base path_subtr subtr_inFr subtr_mono subtr_rootL_in)
```
```   913
```
```   914
```
```   915
```
```   916 subsection{* The Regular Cut of a Tree *}
```
```   917
```
```   918 context fixes tr0 :: dtree
```
```   919 begin
```
```   920
```
```   921 (* Picking a subtree of a certain root: *)
```
```   922 definition "pick n \<equiv> SOME tr. subtr UNIV tr tr0 \<and> root tr = n"
```
```   923
```
```   924 lemma pick:
```
```   925 assumes "inItr UNIV tr0 n"
```
```   926 shows "subtr UNIV (pick n) tr0 \<and> root (pick n) = n"
```
```   927 proof-
```
```   928   have "\<exists> tr. subtr UNIV tr tr0 \<and> root tr = n"
```
```   929   using assms by (metis (lifting) inItr_subtr)
```
```   930   thus ?thesis unfolding pick_def by(rule someI_ex)
```
```   931 qed
```
```   932
```
```   933 lemmas subtr_pick = pick[THEN conjunct1]
```
```   934 lemmas root_pick = pick[THEN conjunct2]
```
```   935
```
```   936 lemma wf_pick:
```
```   937 assumes tr0: "wf tr0" and n: "inItr UNIV tr0 n"
```
```   938 shows "wf (pick n)"
```
```   939 using wf_subtr[OF tr0 subtr_pick[OF n]] .
```
```   940
```
```   941 definition "H_r n \<equiv> root (pick n)"
```
```   942 definition "H_c n \<equiv> (id \<oplus> root) ` cont (pick n)"
```
```   943
```
```   944 (* The regular tree of a function: *)
```
```   945 definition H :: "N \<Rightarrow> dtree" where
```
```   946 "H \<equiv> unfold H_r H_c"
```
```   947
```
```   948 lemma finite_H_c: "finite (H_c n)"
```
```   949 unfolding H_c_def by (metis finite_cont finite_imageI)
```
```   950
```
```   951 lemma root_H_pick: "root (H n) = root (pick n)"
```
```   952 using unfold(1)[of H_r H_c n] unfolding H_def H_r_def by simp
```
```   953
```
```   954 lemma root_H[simp]:
```
```   955 assumes "inItr UNIV tr0 n"
```
```   956 shows "root (H n) = n"
```
```   957 unfolding root_H_pick root_pick[OF assms] ..
```
```   958
```
```   959 lemma cont_H[simp]:
```
```   960 "cont (H n) = (id \<oplus> (H o root)) ` cont (pick n)"
```
```   961 apply(subst id_comp[symmetric, of id]) unfolding map_sum.comp[symmetric]
```
```   962 unfolding image_comp [symmetric] H_c_def [symmetric]
```
```   963 using unfold(2) [of H_c n H_r, OF finite_H_c]
```
```   964 unfolding H_def ..
```
```   965
```
```   966 lemma Inl_cont_H[simp]:
```
```   967 "Inl -` (cont (H n)) = Inl -` (cont (pick n))"
```
```   968 unfolding cont_H by simp
```
```   969
```
```   970 lemma Inr_cont_H:
```
```   971 "Inr -` (cont (H n)) = (H \<circ> root) ` (Inr -` cont (pick n))"
```
```   972 unfolding cont_H by simp
```
```   973
```
```   974 lemma subtr_H:
```
```   975 assumes n: "inItr UNIV tr0 n" and "subtr UNIV tr1 (H n)"
```
```   976 shows "\<exists> n1. inItr UNIV tr0 n1 \<and> tr1 = H n1"
```
```   977 proof-
```
```   978   {fix tr ns assume "subtr UNIV tr1 tr"
```
```   979    hence "tr = H n \<longrightarrow> (\<exists> n1. inItr UNIV tr0 n1 \<and> tr1 = H n1)"
```
```   980    proof (induct rule: subtr_UNIV_inductL)
```
```   981      case (Step tr2 tr1 tr)
```
```   982      show ?case proof
```
```   983        assume "tr = H n"
```
```   984        then obtain n1 where tr2: "Inr tr2 \<in> cont tr1"
```
```   985        and tr1_tr: "subtr UNIV tr1 tr" and n1: "inItr UNIV tr0 n1" and tr1: "tr1 = H n1"
```
```   986        using Step by auto
```
```   987        obtain tr2' where tr2: "tr2 = H (root tr2')"
```
```   988        and tr2': "Inr tr2' \<in> cont (pick n1)"
```
```   989        using tr2 Inr_cont_H[of n1]
```
```   990        unfolding tr1 image_def comp_def using vimage_eq by auto
```
```   991        have "inItr UNIV tr0 (root tr2')"
```
```   992        using inItr.Base inItr.Ind n1 pick subtr_inItr tr2' by (metis iso_tuple_UNIV_I)
```
```   993        thus "\<exists>n2. inItr UNIV tr0 n2 \<and> tr2 = H n2" using tr2 by blast
```
```   994      qed
```
```   995    qed(insert n, auto)
```
```   996   }
```
```   997   thus ?thesis using assms by auto
```
```   998 qed
```
```   999
```
```  1000 lemma root_H_root:
```
```  1001 assumes n: "inItr UNIV tr0 n" and t_tr: "t_tr \<in> cont (pick n)"
```
```  1002 shows "(id \<oplus> (root \<circ> H \<circ> root)) t_tr = (id \<oplus> root) t_tr"
```
```  1003 using assms apply(cases t_tr)
```
```  1004   apply (metis (lifting) map_sum.simps(1))
```
```  1005   using pick H_def H_r_def unfold(1)
```
```  1006       inItr.Base comp_apply subtr_StepL subtr_inItr map_sum.simps(2)
```
```  1007   by (metis UNIV_I)
```
```  1008
```
```  1009 lemma H_P:
```
```  1010 assumes tr0: "wf tr0" and n: "inItr UNIV tr0 n"
```
```  1011 shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
```
```  1012 proof-
```
```  1013   have "?L = (n, (id \<oplus> root) ` cont (pick n))"
```
```  1014   unfolding cont_H image_comp map_sum.comp id_comp comp_assoc[symmetric]
```
```  1015   unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
```
```  1016   by (rule root_H_root[OF n])
```
```  1017   moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
```
```  1018   ultimately show ?thesis by simp
```
```  1019 qed
```
```  1020
```
```  1021 lemma wf_H:
```
```  1022 assumes tr0: "wf tr0" and "inItr UNIV tr0 n"
```
```  1023 shows "wf (H n)"
```
```  1024 proof-
```
```  1025   {fix tr have "\<exists> n. inItr UNIV tr0 n \<and> tr = H n \<Longrightarrow> wf tr"
```
```  1026    proof (induct rule: wf_raw_coind)
```
```  1027      case (Hyp tr)
```
```  1028      then obtain n where n: "inItr UNIV tr0 n" and tr: "tr = H n" by auto
```
```  1029      show ?case apply safe
```
```  1030      apply (metis (lifting) H_P root_H n tr tr0)
```
```  1031      unfolding tr Inr_cont_H unfolding inj_on_def apply clarsimp using root_H
```
```  1032      apply (metis UNIV_I inItr.Base n pick subtr2.simps subtr_inItr subtr_subtr2)
```
```  1033      by (metis n subtr.Refl subtr_StepL subtr_H tr UNIV_I)
```
```  1034    qed
```
```  1035   }
```
```  1036   thus ?thesis using assms by blast
```
```  1037 qed
```
```  1038
```
```  1039 (* The regular cut of a tree: *)
```
```  1040 definition "rcut \<equiv> H (root tr0)"
```
```  1041
```
```  1042 lemma reg_rcut: "reg H rcut"
```
```  1043 unfolding reg_def rcut_def
```
```  1044 by (metis inItr.Base root_H subtr_H UNIV_I)
```
```  1045
```
```  1046 lemma rcut_reg:
```
```  1047 assumes "reg H tr0"
```
```  1048 shows "rcut = tr0"
```
```  1049 using assms unfolding rcut_def reg_def by (metis subtr.Refl UNIV_I)
```
```  1050
```
```  1051 lemma rcut_eq: "rcut = tr0 \<longleftrightarrow> reg H tr0"
```
```  1052 using reg_rcut rcut_reg by metis
```
```  1053
```
```  1054 lemma regular_rcut: "regular rcut"
```
```  1055 using reg_rcut unfolding regular_def by blast
```
```  1056
```
```  1057 lemma Fr_rcut: "Fr UNIV rcut \<subseteq> Fr UNIV tr0"
```
```  1058 proof safe
```
```  1059   fix t assume "t \<in> Fr UNIV rcut"
```
```  1060   then obtain tr where t: "Inl t \<in> cont tr" and tr: "subtr UNIV tr (H (root tr0))"
```
```  1061   using Fr_subtr[of UNIV "H (root tr0)"] unfolding rcut_def
```
```  1062   by (metis (full_types) Fr_def inFr_subtr mem_Collect_eq)
```
```  1063   obtain n where n: "inItr UNIV tr0 n" and tr: "tr = H n" using tr
```
```  1064   by (metis (lifting) inItr.Base subtr_H UNIV_I)
```
```  1065   have "Inl t \<in> cont (pick n)" using t using Inl_cont_H[of n] unfolding tr
```
```  1066   by (metis (lifting) vimageD vimageI2)
```
```  1067   moreover have "subtr UNIV (pick n) tr0" using subtr_pick[OF n] ..
```
```  1068   ultimately show "t \<in> Fr UNIV tr0" unfolding Fr_subtr_cont by auto
```
```  1069 qed
```
```  1070
```
```  1071 lemma wf_rcut:
```
```  1072 assumes "wf tr0"
```
```  1073 shows "wf rcut"
```
```  1074 unfolding rcut_def using wf_H[OF assms inItr.Base] by simp
```
```  1075
```
```  1076 lemma root_rcut[simp]: "root rcut = root tr0"
```
```  1077 unfolding rcut_def
```
```  1078 by (metis (lifting) root_H inItr.Base reg_def reg_root subtr_rootR_in)
```
```  1079
```
```  1080 end (* context *)
```
```  1081
```
```  1082
```
```  1083 subsection{* Recursive Description of the Regular Tree Frontiers *}
```
```  1084
```
```  1085 lemma regular_inFr:
```
```  1086 assumes r: "regular tr" and In: "root tr \<in> ns"
```
```  1087 and t: "inFr ns tr t"
```
```  1088 shows "t \<in> Inl -` (cont tr) \<or>
```
```  1089        (\<exists> tr'. Inr tr' \<in> cont tr \<and> inFr (ns - {root tr}) tr' t)"
```
```  1090 (is "?L \<or> ?R")
```
```  1091 proof-
```
```  1092   obtain f where r: "reg f tr" and f: "\<And>n. root (f n) = n"
```
```  1093   using r unfolding regular_def2 by auto
```
```  1094   obtain nl tr1 where d_nl: "distinct nl" and p: "path f nl" and hd_nl: "f (hd nl) = tr"
```
```  1095   and l_nl: "f (last nl) = tr1" and s_nl: "set nl \<subseteq> ns" and t_tr1: "Inl t \<in> cont tr1"
```
```  1096   using t unfolding inFr_iff_path[OF r f] by auto
```
```  1097   obtain n nl1 where nl: "nl = n # nl1" by (metis (lifting) p path.simps)
```
```  1098   hence f_n: "f n = tr" using hd_nl by simp
```
```  1099   have n_nl1: "n \<notin> set nl1" using d_nl unfolding nl by auto
```
```  1100   show ?thesis
```
```  1101   proof(cases nl1)
```
```  1102     case Nil hence "tr = tr1" using f_n l_nl unfolding nl by simp
```
```  1103     hence ?L using t_tr1 by simp thus ?thesis by simp
```
```  1104   next
```
```  1105     case (Cons n1 nl2) note nl1 = Cons
```
```  1106     have 1: "last nl1 = last nl" "hd nl1 = n1" unfolding nl nl1 by simp_all
```
```  1107     have p1: "path f nl1" and n1_tr: "Inr (f n1) \<in> cont tr"
```
```  1108     using path.simps[of f nl] p f_n unfolding nl nl1 by auto
```
```  1109     have r1: "reg f (f n1)" using reg_Inr_cont[OF r n1_tr] .
```
```  1110     have 0: "inFr (set nl1) (f n1) t" unfolding inFr_iff_path[OF r1 f]
```
```  1111     apply(intro exI[of _ nl1], intro exI[of _ tr1])
```
```  1112     using d_nl unfolding 1 l_nl unfolding nl using p1 t_tr1 by auto
```
```  1113     have root_tr: "root tr = n" by (metis f f_n)
```
```  1114     have "inFr (ns - {root tr}) (f n1) t" apply(rule inFr_mono[OF 0])
```
```  1115     using s_nl unfolding root_tr unfolding nl using n_nl1 by auto
```
```  1116     thus ?thesis using n1_tr by auto
```
```  1117   qed
```
```  1118 qed
```
```  1119
```
```  1120 lemma regular_Fr:
```
```  1121 assumes r: "regular tr" and In: "root tr \<in> ns"
```
```  1122 shows "Fr ns tr =
```
```  1123        Inl -` (cont tr) \<union>
```
```  1124        \<Union> {Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
```
```  1125 unfolding Fr_def
```
```  1126 using In inFr.Base regular_inFr[OF assms] apply safe
```
```  1127 apply (simp, metis (full_types) mem_Collect_eq)
```
```  1128 apply simp
```
```  1129 by (simp, metis (lifting) inFr_Ind_minus insert_Diff)
```
```  1130
```
```  1131
```
```  1132 subsection{* The Generated Languages *}
```
```  1133
```
```  1134 (* The (possibly inifinite tree) generated language *)
```
```  1135 definition "L ns n \<equiv> {Fr ns tr | tr. wf tr \<and> root tr = n}"
```
```  1136
```
```  1137 (* The regular-tree generated language *)
```
```  1138 definition "Lr ns n \<equiv> {Fr ns tr | tr. wf tr \<and> root tr = n \<and> regular tr}"
```
```  1139
```
```  1140 lemma L_rec_notin:
```
```  1141 assumes "n \<notin> ns"
```
```  1142 shows "L ns n = {{}}"
```
```  1143 using assms unfolding L_def apply safe
```
```  1144   using not_root_Fr apply force
```
```  1145   apply(rule exI[of _ "deftr n"])
```
```  1146   by (metis (no_types) wf_deftr not_root_Fr root_deftr)
```
```  1147
```
```  1148 lemma Lr_rec_notin:
```
```  1149 assumes "n \<notin> ns"
```
```  1150 shows "Lr ns n = {{}}"
```
```  1151 using assms unfolding Lr_def apply safe
```
```  1152   using not_root_Fr apply force
```
```  1153   apply(rule exI[of _ "deftr n"])
```
```  1154   by (metis (no_types) regular_def wf_deftr not_root_Fr reg_deftr root_deftr)
```
```  1155
```
```  1156 lemma wf_subtrOf:
```
```  1157 assumes "wf tr" and "Inr n \<in> prodOf tr"
```
```  1158 shows "wf (subtrOf tr n)"
```
```  1159 by (metis assms wf_cont subtrOf)
```
```  1160
```
```  1161 lemma Lr_rec_in:
```
```  1162 assumes n: "n \<in> ns"
```
```  1163 shows "Lr ns n \<subseteq>
```
```  1164 {Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
```
```  1165     (n,tns) \<in> P \<and>
```
```  1166     (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> Lr (ns - {n}) n')}"
```
```  1167 (is "Lr ns n \<subseteq> {?F tns K | tns K. (n,tns) \<in> P \<and> ?\<phi> tns K}")
```
```  1168 proof safe
```
```  1169   fix ts assume "ts \<in> Lr ns n"
```
```  1170   then obtain tr where dtr: "wf tr" and r: "root tr = n" and tr: "regular tr"
```
```  1171   and ts: "ts = Fr ns tr" unfolding Lr_def by auto
```
```  1172   def tns \<equiv> "(id \<oplus> root) ` (cont tr)"
```
```  1173   def K \<equiv> "\<lambda> n'. Fr (ns - {n}) (subtrOf tr n')"
```
```  1174   show "\<exists>tns K. ts = ?F tns K \<and> (n, tns) \<in> P \<and> ?\<phi> tns K"
```
```  1175   apply(rule exI[of _ tns], rule exI[of _ K]) proof(intro conjI allI impI)
```
```  1176     show "ts = Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns}"
```
```  1177     unfolding ts regular_Fr[OF tr n[unfolded r[symmetric]]]
```
```  1178     unfolding tns_def K_def r[symmetric]
```
```  1179     unfolding Inl_prodOf wf_subtrOf_Union[OF dtr] ..
```
```  1180     show "(n, tns) \<in> P" unfolding tns_def r[symmetric] using wf_P[OF dtr] .
```
```  1181     fix n' assume "Inr n' \<in> tns" thus "K n' \<in> Lr (ns - {n}) n'"
```
```  1182     unfolding K_def Lr_def mem_Collect_eq apply(intro exI[of _ "subtrOf tr n'"])
```
```  1183     using dtr tr apply(intro conjI refl)  unfolding tns_def
```
```  1184       apply(erule wf_subtrOf[OF dtr])
```
```  1185       apply (metis subtrOf)
```
```  1186       by (metis Inr_subtrOf UNIV_I regular_subtr subtr.simps)
```
```  1187   qed
```
```  1188 qed
```
```  1189
```
```  1190 lemma hsubst_aux:
```
```  1191 fixes n ftr tns
```
```  1192 assumes n: "n \<in> ns" and tns: "finite tns" and
```
```  1193 1: "\<And> n'. Inr n' \<in> tns \<Longrightarrow> wf (ftr n')"
```
```  1194 defines "tr \<equiv> Node n ((id \<oplus> ftr) ` tns)"  defines "tr' \<equiv> hsubst tr tr"
```
```  1195 shows "Fr ns tr' = Inl -` tns \<union> \<Union>{Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns}"
```
```  1196 (is "_ = ?B") proof-
```
```  1197   have rtr: "root tr = n" and ctr: "cont tr = (id \<oplus> ftr) ` tns"
```
```  1198   unfolding tr_def using tns by auto
```
```  1199   have Frr: "Frr (ns - {n}) tr = \<Union>{Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns}"
```
```  1200   unfolding Frr_def ctr by auto
```
```  1201   have "Fr ns tr' = Inl -` (cont tr) \<union> Frr (ns - {n}) tr"
```
```  1202   using Fr_self_hsubst[OF n[unfolded rtr[symmetric]]] unfolding tr'_def rtr ..
```
```  1203   also have "... = ?B" unfolding ctr Frr by simp
```
```  1204   finally show ?thesis .
```
```  1205 qed
```
```  1206
```
```  1207 lemma L_rec_in:
```
```  1208 assumes n: "n \<in> ns"
```
```  1209 shows "
```
```  1210 {Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
```
```  1211     (n,tns) \<in> P \<and>
```
```  1212     (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> L (ns - {n}) n')}
```
```  1213  \<subseteq> L ns n"
```
```  1214 proof safe
```
```  1215   fix tns K
```
```  1216   assume P: "(n, tns) \<in> P" and 0: "\<forall>n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> L (ns - {n}) n'"
```
```  1217   {fix n' assume "Inr n' \<in> tns"
```
```  1218    hence "K n' \<in> L (ns - {n}) n'" using 0 by auto
```
```  1219    hence "\<exists> tr'. K n' = Fr (ns - {n}) tr' \<and> wf tr' \<and> root tr' = n'"
```
```  1220    unfolding L_def mem_Collect_eq by auto
```
```  1221   }
```
```  1222   then obtain ftr where 0: "\<And> n'. Inr n' \<in> tns \<Longrightarrow>
```
```  1223   K n' = Fr (ns - {n}) (ftr n') \<and> wf (ftr n') \<and> root (ftr n') = n'"
```
```  1224   by metis
```
```  1225   def tr \<equiv> "Node n ((id \<oplus> ftr) ` tns)"  def tr' \<equiv> "hsubst tr tr"
```
```  1226   have rtr: "root tr = n" and ctr: "cont tr = (id \<oplus> ftr) ` tns"
```
```  1227   unfolding tr_def by (simp, metis P cont_Node finite_imageI finite_in_P)
```
```  1228   have prtr: "prodOf tr = tns" apply(rule Inl_Inr_image_cong)
```
```  1229   unfolding ctr apply simp apply simp apply safe
```
```  1230   using 0 unfolding image_def apply force apply simp by (metis 0 vimageI2)
```
```  1231   have 1: "{K n' |n'. Inr n' \<in> tns} = {Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns}"
```
```  1232   using 0 by auto
```
```  1233   have dtr: "wf tr" apply(rule wf.dtree)
```
```  1234     apply (metis (lifting) P prtr rtr)
```
```  1235     unfolding inj_on_def ctr using 0 by auto
```
```  1236   hence dtr': "wf tr'" unfolding tr'_def by (metis wf_hsubst)
```
```  1237   have tns: "finite tns" using finite_in_P P by simp
```
```  1238   have "Inl -` tns \<union> \<Union>{Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns} \<in> L ns n"
```
```  1239   unfolding L_def mem_Collect_eq apply(intro exI[of _ tr'] conjI)
```
```  1240   using dtr' 0 hsubst_aux[OF assms tns, of ftr] unfolding tr_def tr'_def by auto
```
```  1241   thus "Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns} \<in> L ns n" unfolding 1 .
```
```  1242 qed
```
```  1243
```
```  1244 lemma card_N: "(n::N) \<in> ns \<Longrightarrow> card (ns - {n}) < card ns"
```
```  1245 by (metis finite_N Diff_UNIV Diff_infinite_finite card_Diff1_less finite.emptyI)
```
```  1246
```
```  1247 function LL where
```
```  1248 "LL ns n =
```
```  1249  (if n \<notin> ns then {{}} else
```
```  1250  {Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
```
```  1251     (n,tns) \<in> P \<and>
```
```  1252     (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> LL (ns - {n}) n')})"
```
```  1253 by(pat_completeness, auto)
```
```  1254 termination apply(relation "inv_image (measure card) fst")
```
```  1255 using card_N by auto
```
```  1256
```
```  1257 declare LL.simps[code]
```
```  1258 declare LL.simps[simp del]
```
```  1259
```
```  1260 lemma Lr_LL: "Lr ns n \<subseteq> LL ns n"
```
```  1261 proof (induct ns arbitrary: n rule: measure_induct[of card])
```
```  1262   case (1 ns n) show ?case proof(cases "n \<in> ns")
```
```  1263     case False thus ?thesis unfolding Lr_rec_notin[OF False] by (simp add: LL.simps)
```
```  1264   next
```
```  1265     case True show ?thesis apply(rule subset_trans)
```
```  1266     using Lr_rec_in[OF True] apply assumption
```
```  1267     unfolding LL.simps[of ns n] using True 1 card_N proof clarsimp
```
```  1268       fix tns K
```
```  1269       assume "n \<in> ns" hence c: "card (ns - {n}) < card ns" using card_N by blast
```
```  1270       assume "(n, tns) \<in> P"
```
```  1271       and "\<forall>n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> Lr (ns - {n}) n'"
```
```  1272       thus "\<exists>tnsa Ka.
```
```  1273              Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns} =
```
```  1274              Inl -` tnsa \<union> \<Union>{Ka n' |n'. Inr n' \<in> tnsa} \<and>
```
```  1275              (n, tnsa) \<in> P \<and> (\<forall>n'. Inr n' \<in> tnsa \<longrightarrow> Ka n' \<in> LL (ns - {n}) n')"
```
```  1276       apply(intro exI[of _ tns] exI[of _ K]) using c 1 by auto
```
```  1277     qed
```
```  1278   qed
```
```  1279 qed
```
```  1280
```
```  1281 lemma LL_L: "LL ns n \<subseteq> L ns n"
```
```  1282 proof (induct ns arbitrary: n rule: measure_induct[of card])
```
```  1283   case (1 ns n) show ?case proof(cases "n \<in> ns")
```
```  1284     case False thus ?thesis unfolding L_rec_notin[OF False] by (simp add: LL.simps)
```
```  1285   next
```
```  1286     case True show ?thesis apply(rule subset_trans)
```
```  1287     prefer 2 using L_rec_in[OF True] apply assumption
```
```  1288     unfolding LL.simps[of ns n] using True 1 card_N proof clarsimp
```
```  1289       fix tns K
```
```  1290       assume "n \<in> ns" hence c: "card (ns - {n}) < card ns" using card_N by blast
```
```  1291       assume "(n, tns) \<in> P"
```
```  1292       and "\<forall>n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> LL (ns - {n}) n'"
```
```  1293       thus "\<exists>tnsa Ka.
```
```  1294              Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns} =
```
```  1295              Inl -` tnsa \<union> \<Union>{Ka n' |n'. Inr n' \<in> tnsa} \<and>
```
```  1296              (n, tnsa) \<in> P \<and> (\<forall>n'. Inr n' \<in> tnsa \<longrightarrow> Ka n' \<in> L (ns - {n}) n')"
```
```  1297       apply(intro exI[of _ tns] exI[of _ K]) using c 1 by auto
```
```  1298     qed
```
```  1299   qed
```
```  1300 qed
```
```  1301
```
```  1302 (* The subsumpsion relation between languages *)
```
```  1303 definition "subs L1 L2 \<equiv> \<forall> ts2 \<in> L2. \<exists> ts1 \<in> L1. ts1 \<subseteq> ts2"
```
```  1304
```
```  1305 lemma incl_subs[simp]: "L2 \<subseteq> L1 \<Longrightarrow> subs L1 L2"
```
```  1306 unfolding subs_def by auto
```
```  1307
```
```  1308 lemma subs_refl[simp]: "subs L1 L1" unfolding subs_def by auto
```
```  1309
```
```  1310 lemma subs_trans: "\<lbrakk>subs L1 L2; subs L2 L3\<rbrakk> \<Longrightarrow> subs L1 L3"
```
```  1311 unfolding subs_def by (metis subset_trans)
```
```  1312
```
```  1313 (* Language equivalence *)
```
```  1314 definition "leqv L1 L2 \<equiv> subs L1 L2 \<and> subs L2 L1"
```
```  1315
```
```  1316 lemma subs_leqv[simp]: "leqv L1 L2 \<Longrightarrow> subs L1 L2"
```
```  1317 unfolding leqv_def by auto
```
```  1318
```
```  1319 lemma subs_leqv_sym[simp]: "leqv L1 L2 \<Longrightarrow> subs L2 L1"
```
```  1320 unfolding leqv_def by auto
```
```  1321
```
```  1322 lemma leqv_refl[simp]: "leqv L1 L1" unfolding leqv_def by auto
```
```  1323
```
```  1324 lemma leqv_trans:
```
```  1325 assumes 12: "leqv L1 L2" and 23: "leqv L2 L3"
```
```  1326 shows "leqv L1 L3"
```
```  1327 using assms unfolding leqv_def by (metis (lifting) subs_trans)
```
```  1328
```
```  1329 lemma leqv_sym: "leqv L1 L2 \<Longrightarrow> leqv L2 L1"
```
```  1330 unfolding leqv_def by auto
```
```  1331
```
```  1332 lemma leqv_Sym: "leqv L1 L2 \<longleftrightarrow> leqv L2 L1"
```
```  1333 unfolding leqv_def by auto
```
```  1334
```
```  1335 lemma Lr_incl_L: "Lr ns ts \<subseteq> L ns ts"
```
```  1336 unfolding Lr_def L_def by auto
```
```  1337
```
```  1338 lemma Lr_subs_L: "subs (Lr UNIV ts) (L UNIV ts)"
```
```  1339 unfolding subs_def proof safe
```
```  1340   fix ts2 assume "ts2 \<in> L UNIV ts"
```
```  1341   then obtain tr where ts2: "ts2 = Fr UNIV tr" and dtr: "wf tr" and rtr: "root tr = ts"
```
```  1342   unfolding L_def by auto
```
```  1343   thus "\<exists>ts1\<in>Lr UNIV ts. ts1 \<subseteq> ts2"
```
```  1344   apply(intro bexI[of _ "Fr UNIV (rcut tr)"])
```
```  1345   unfolding Lr_def L_def using Fr_rcut wf_rcut root_rcut regular_rcut by auto
```
```  1346 qed
```
```  1347
```
```  1348 lemma Lr_leqv_L: "leqv (Lr UNIV ts) (L UNIV ts)"
```
```  1349 using Lr_subs_L unfolding leqv_def by (metis (lifting) Lr_incl_L incl_subs)
```
```  1350
```
```  1351 lemma LL_leqv_L: "leqv (LL UNIV ts) (L UNIV ts)"
```
```  1352 by (metis (lifting) LL_L Lr_LL Lr_subs_L incl_subs leqv_def subs_trans)
```
```  1353
```
```  1354 lemma LL_leqv_Lr: "leqv (LL UNIV ts) (Lr UNIV ts)"
```
```  1355 using Lr_leqv_L LL_leqv_L by (metis leqv_Sym leqv_trans)
```
```  1356
```
```  1357 end
```