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