--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Tue Oct 16 22:38:34 2012 +0200
@@ -0,0 +1,94 @@
+(* Title: HOL/BNF/Examples/Infinite_Derivation_Trees/DTree.thy
+ Author: Andrei Popescu, TU Muenchen
+ Copyright 2012
+
+Derivation trees with nonterminal internal nodes and terminal leaves.
+*)
+
+header {* Trees with Nonterminal Internal Nodes and Terminal Leaves *}
+
+theory DTree
+imports Prelim
+begin
+
+hide_fact (open) Quotient_Product.prod_rel_def
+
+typedecl N
+typedecl T
+
+codata dtree = NNode (root: N) (ccont: "(T + dtree) fset")
+
+subsection{* Transporting the Characteristic Lemmas from @{text "fset"} to @{text "set"} *}
+
+definition "Node n as \<equiv> NNode n (the_inv fset as)"
+definition "cont \<equiv> fset o ccont"
+definition "unfold rt ct \<equiv> dtree_unfold rt (the_inv fset o ct)"
+definition "corec rt qt ct dt \<equiv> dtree_corec rt qt (the_inv fset o ct) (the_inv fset o dt)"
+
+lemma finite_cont[simp]: "finite (cont tr)"
+unfolding cont_def by auto
+
+lemma Node_root_cont[simp]:
+"Node (root tr) (cont tr) = tr"
+using dtree.collapse unfolding Node_def cont_def
+by (metis cont_def finite_cont fset_cong fset_to_fset o_def)
+
+lemma dtree_simps[simp]:
+assumes "finite as" and "finite as'"
+shows "Node n as = Node n' as' \<longleftrightarrow> n = n' \<and> as = as'"
+using assms dtree.inject unfolding Node_def
+by (metis fset_to_fset)
+
+lemma dtree_cases[elim, case_names Node Choice]:
+assumes Node: "\<And> n as. \<lbrakk>finite as; tr = Node n as\<rbrakk> \<Longrightarrow> phi"
+shows phi
+apply(cases rule: dtree.exhaust[of tr])
+using Node unfolding Node_def
+by (metis Node Node_root_cont finite_cont)
+
+lemma dtree_sel_ctor[simp]:
+"root (Node n as) = n"
+"finite as \<Longrightarrow> cont (Node n as) = as"
+unfolding Node_def cont_def by auto
+
+lemmas root_Node = dtree_sel_ctor(1)
+lemmas cont_Node = dtree_sel_ctor(2)
+
+lemma dtree_cong:
+assumes "root tr = root tr'" and "cont tr = cont tr'"
+shows "tr = tr'"
+by (metis Node_root_cont assms)
+
+lemma set_rel_cont:
+"set_rel \<chi> (cont tr1) (cont tr2) = fset_rel \<chi> (ccont tr1) (ccont tr2)"
+unfolding cont_def comp_def fset_rel_fset ..
+
+lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]:
+assumes phi: "\<phi> tr1 tr2" and
+Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
+ root tr1 = root tr2 \<and> set_rel (sum_rel op = \<phi>) (cont tr1) (cont tr2)"
+shows "tr1 = tr2"
+using phi apply(elim dtree.coinduct)
+apply(rule Lift[unfolded set_rel_cont]) .
+
+lemma unfold:
+"root (unfold rt ct b) = rt b"
+"finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
+using dtree.sel_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def
+apply - apply metis
+unfolding cont_def comp_def
+by (metis (no_types) fset_to_fset map_fset_image)
+
+lemma corec:
+"root (corec rt qt ct dt b) = rt b"
+"\<lbrakk>finite (ct b); finite (dt b)\<rbrakk> \<Longrightarrow>
+ cont (corec rt qt ct dt b) =
+ (if qt b then ct b else image (id \<oplus> corec rt qt ct dt) (dt b))"
+using dtree.sel_corec[of rt qt "the_inv fset \<circ> ct" "the_inv fset \<circ> dt" b]
+unfolding corec_def
+apply -
+apply simp
+unfolding cont_def comp_def id_def
+by (metis (no_types) fset_to_fset map_fset_image)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy Tue Oct 16 22:38:34 2012 +0200
@@ -0,0 +1,1359 @@
+(* Title: HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy
+ Author: Andrei Popescu, TU Muenchen
+ Copyright 2012
+
+Language of a grammar.
+*)
+
+header {* Language of a Grammar *}
+
+theory Gram_Lang
+imports DTree
+begin
+
+
+(* We assume that the sets of terminals, and the left-hand sides of
+productions are finite and that the grammar has no unused nonterminals. *)
+consts P :: "(N \<times> (T + N) set) set"
+axiomatization where
+ finite_N: "finite (UNIV::N set)"
+and finite_in_P: "\<And> n tns. (n,tns) \<in> P \<longrightarrow> finite tns"
+and used: "\<And> n. \<exists> tns. (n,tns) \<in> P"
+
+
+subsection{* Tree Basics: frontier, interior, etc. *}
+
+
+(* Frontier *)
+
+inductive inFr :: "N set \<Rightarrow> dtree \<Rightarrow> T \<Rightarrow> bool" where
+Base: "\<lbrakk>root tr \<in> ns; Inl t \<in> cont tr\<rbrakk> \<Longrightarrow> inFr ns tr t"
+|
+Ind: "\<lbrakk>root tr \<in> ns; Inr tr1 \<in> cont tr; inFr ns tr1 t\<rbrakk> \<Longrightarrow> inFr ns tr t"
+
+definition "Fr ns tr \<equiv> {t. inFr ns tr t}"
+
+lemma inFr_root_in: "inFr ns tr t \<Longrightarrow> root tr \<in> ns"
+by (metis inFr.simps)
+
+lemma inFr_mono:
+assumes "inFr ns tr t" and "ns \<subseteq> ns'"
+shows "inFr ns' tr t"
+using assms apply(induct arbitrary: ns' rule: inFr.induct)
+using Base Ind by (metis inFr.simps set_mp)+
+
+lemma inFr_Ind_minus:
+assumes "inFr ns1 tr1 t" and "Inr tr1 \<in> cont tr"
+shows "inFr (insert (root tr) ns1) tr t"
+using assms apply(induct rule: inFr.induct)
+ apply (metis inFr.simps insert_iff)
+ by (metis inFr.simps inFr_mono insertI1 subset_insertI)
+
+(* alternative definition *)
+inductive inFr2 :: "N set \<Rightarrow> dtree \<Rightarrow> T \<Rightarrow> bool" where
+Base: "\<lbrakk>root tr \<in> ns; Inl t \<in> cont tr\<rbrakk> \<Longrightarrow> inFr2 ns tr t"
+|
+Ind: "\<lbrakk>Inr tr1 \<in> cont tr; inFr2 ns1 tr1 t\<rbrakk>
+ \<Longrightarrow> inFr2 (insert (root tr) ns1) tr t"
+
+lemma inFr2_root_in: "inFr2 ns tr t \<Longrightarrow> root tr \<in> ns"
+apply(induct rule: inFr2.induct) by auto
+
+lemma inFr2_mono:
+assumes "inFr2 ns tr t" and "ns \<subseteq> ns'"
+shows "inFr2 ns' tr t"
+using assms apply(induct arbitrary: ns' rule: inFr2.induct)
+using Base Ind
+apply (metis subsetD) by (metis inFr2.simps insert_absorb insert_subset)
+
+lemma inFr2_Ind:
+assumes "inFr2 ns tr1 t" and "root tr \<in> ns" and "Inr tr1 \<in> cont tr"
+shows "inFr2 ns tr t"
+using assms apply(induct rule: inFr2.induct)
+ apply (metis inFr2.simps insert_absorb)
+ by (metis inFr2.simps insert_absorb)
+
+lemma inFr_inFr2:
+"inFr = inFr2"
+apply (rule ext)+ apply(safe)
+ apply(erule inFr.induct)
+ apply (metis (lifting) inFr2.Base)
+ apply (metis (lifting) inFr2_Ind)
+ apply(erule inFr2.induct)
+ apply (metis (lifting) inFr.Base)
+ apply (metis (lifting) inFr_Ind_minus)
+done
+
+lemma not_root_inFr:
+assumes "root tr \<notin> ns"
+shows "\<not> inFr ns tr t"
+by (metis assms inFr_root_in)
+
+lemma not_root_Fr:
+assumes "root tr \<notin> ns"
+shows "Fr ns tr = {}"
+using not_root_inFr[OF assms] unfolding Fr_def by auto
+
+
+(* Interior *)
+
+inductive inItr :: "N set \<Rightarrow> dtree \<Rightarrow> N \<Rightarrow> bool" where
+Base: "root tr \<in> ns \<Longrightarrow> inItr ns tr (root tr)"
+|
+Ind: "\<lbrakk>root tr \<in> ns; Inr tr1 \<in> cont tr; inItr ns tr1 n\<rbrakk> \<Longrightarrow> inItr ns tr n"
+
+definition "Itr ns tr \<equiv> {n. inItr ns tr n}"
+
+lemma inItr_root_in: "inItr ns tr n \<Longrightarrow> root tr \<in> ns"
+by (metis inItr.simps)
+
+lemma inItr_mono:
+assumes "inItr ns tr n" and "ns \<subseteq> ns'"
+shows "inItr ns' tr n"
+using assms apply(induct arbitrary: ns' rule: inItr.induct)
+using Base Ind by (metis inItr.simps set_mp)+
+
+
+(* The subtree relation *)
+
+inductive subtr where
+Refl: "root tr \<in> ns \<Longrightarrow> subtr ns tr tr"
+|
+Step: "\<lbrakk>root tr3 \<in> ns; subtr ns tr1 tr2; Inr tr2 \<in> cont tr3\<rbrakk> \<Longrightarrow> subtr ns tr1 tr3"
+
+lemma subtr_rootL_in:
+assumes "subtr ns tr1 tr2"
+shows "root tr1 \<in> ns"
+using assms apply(induct rule: subtr.induct) by auto
+
+lemma subtr_rootR_in:
+assumes "subtr ns tr1 tr2"
+shows "root tr2 \<in> ns"
+using assms apply(induct rule: subtr.induct) by auto
+
+lemmas subtr_roots_in = subtr_rootL_in subtr_rootR_in
+
+lemma subtr_mono:
+assumes "subtr ns tr1 tr2" and "ns \<subseteq> ns'"
+shows "subtr ns' tr1 tr2"
+using assms apply(induct arbitrary: ns' rule: subtr.induct)
+using Refl Step by (metis subtr.simps set_mp)+
+
+lemma subtr_trans_Un:
+assumes "subtr ns12 tr1 tr2" and "subtr ns23 tr2 tr3"
+shows "subtr (ns12 \<union> ns23) tr1 tr3"
+proof-
+ have "subtr ns23 tr2 tr3 \<Longrightarrow>
+ (\<forall> ns12 tr1. subtr ns12 tr1 tr2 \<longrightarrow> subtr (ns12 \<union> ns23) tr1 tr3)"
+ apply(induct rule: subtr.induct, safe)
+ apply (metis subtr_mono sup_commute sup_ge2)
+ by (metis (lifting) Step UnI2)
+ thus ?thesis using assms by auto
+qed
+
+lemma subtr_trans:
+assumes "subtr ns tr1 tr2" and "subtr ns tr2 tr3"
+shows "subtr ns tr1 tr3"
+using subtr_trans_Un[OF assms] by simp
+
+lemma subtr_StepL:
+assumes r: "root tr1 \<in> ns" and tr12: "Inr tr1 \<in> cont tr2" and s: "subtr ns tr2 tr3"
+shows "subtr ns tr1 tr3"
+apply(rule subtr_trans[OF _ s])
+apply(rule Step[of tr2 ns tr1 tr1])
+apply(rule subtr_rootL_in[OF s])
+apply(rule Refl[OF r])
+apply(rule tr12)
+done
+
+(* alternative definition: *)
+inductive subtr2 where
+Refl: "root tr \<in> ns \<Longrightarrow> subtr2 ns tr tr"
+|
+Step: "\<lbrakk>root tr1 \<in> ns; Inr tr1 \<in> cont tr2; subtr2 ns tr2 tr3\<rbrakk> \<Longrightarrow> subtr2 ns tr1 tr3"
+
+lemma subtr2_rootL_in:
+assumes "subtr2 ns tr1 tr2"
+shows "root tr1 \<in> ns"
+using assms apply(induct rule: subtr2.induct) by auto
+
+lemma subtr2_rootR_in:
+assumes "subtr2 ns tr1 tr2"
+shows "root tr2 \<in> ns"
+using assms apply(induct rule: subtr2.induct) by auto
+
+lemmas subtr2_roots_in = subtr2_rootL_in subtr2_rootR_in
+
+lemma subtr2_mono:
+assumes "subtr2 ns tr1 tr2" and "ns \<subseteq> ns'"
+shows "subtr2 ns' tr1 tr2"
+using assms apply(induct arbitrary: ns' rule: subtr2.induct)
+using Refl Step by (metis subtr2.simps set_mp)+
+
+lemma subtr2_trans_Un:
+assumes "subtr2 ns12 tr1 tr2" and "subtr2 ns23 tr2 tr3"
+shows "subtr2 (ns12 \<union> ns23) tr1 tr3"
+proof-
+ have "subtr2 ns12 tr1 tr2 \<Longrightarrow>
+ (\<forall> ns23 tr3. subtr2 ns23 tr2 tr3 \<longrightarrow> subtr2 (ns12 \<union> ns23) tr1 tr3)"
+ apply(induct rule: subtr2.induct, safe)
+ apply (metis subtr2_mono sup_commute sup_ge2)
+ by (metis Un_iff subtr2.simps)
+ thus ?thesis using assms by auto
+qed
+
+lemma subtr2_trans:
+assumes "subtr2 ns tr1 tr2" and "subtr2 ns tr2 tr3"
+shows "subtr2 ns tr1 tr3"
+using subtr2_trans_Un[OF assms] by simp
+
+lemma subtr2_StepR:
+assumes r: "root tr3 \<in> ns" and tr23: "Inr tr2 \<in> cont tr3" and s: "subtr2 ns tr1 tr2"
+shows "subtr2 ns tr1 tr3"
+apply(rule subtr2_trans[OF s])
+apply(rule Step[of _ _ tr3])
+apply(rule subtr2_rootR_in[OF s])
+apply(rule tr23)
+apply(rule Refl[OF r])
+done
+
+lemma subtr_subtr2:
+"subtr = subtr2"
+apply (rule ext)+ apply(safe)
+ apply(erule subtr.induct)
+ apply (metis (lifting) subtr2.Refl)
+ apply (metis (lifting) subtr2_StepR)
+ apply(erule subtr2.induct)
+ apply (metis (lifting) subtr.Refl)
+ apply (metis (lifting) subtr_StepL)
+done
+
+lemma subtr_inductL[consumes 1, case_names Refl Step]:
+assumes s: "subtr ns tr1 tr2" and Refl: "\<And>ns tr. \<phi> ns tr tr"
+and Step:
+"\<And>ns tr1 tr2 tr3.
+ \<lbrakk>root tr1 \<in> ns; Inr tr1 \<in> cont tr2; subtr ns tr2 tr3; \<phi> ns tr2 tr3\<rbrakk> \<Longrightarrow> \<phi> ns tr1 tr3"
+shows "\<phi> ns tr1 tr2"
+using s unfolding subtr_subtr2 apply(rule subtr2.induct)
+using Refl Step unfolding subtr_subtr2 by auto
+
+lemma subtr_UNIV_inductL[consumes 1, case_names Refl Step]:
+assumes s: "subtr UNIV tr1 tr2" and Refl: "\<And>tr. \<phi> tr tr"
+and Step:
+"\<And>tr1 tr2 tr3.
+ \<lbrakk>Inr tr1 \<in> cont tr2; subtr UNIV tr2 tr3; \<phi> tr2 tr3\<rbrakk> \<Longrightarrow> \<phi> tr1 tr3"
+shows "\<phi> tr1 tr2"
+using s apply(induct rule: subtr_inductL)
+apply(rule Refl) using Step subtr_mono by (metis subset_UNIV)
+
+(* Subtree versus frontier: *)
+lemma subtr_inFr:
+assumes "inFr ns tr t" and "subtr ns tr tr1"
+shows "inFr ns tr1 t"
+proof-
+ have "subtr ns tr tr1 \<Longrightarrow> (\<forall> t. inFr ns tr t \<longrightarrow> inFr ns tr1 t)"
+ apply(induct rule: subtr.induct, safe) by (metis inFr.Ind)
+ thus ?thesis using assms by auto
+qed
+
+corollary Fr_subtr:
+"Fr ns tr = \<Union> {Fr ns tr' | tr'. subtr ns tr' tr}"
+unfolding Fr_def proof safe
+ fix t assume t: "inFr ns tr t" hence "root tr \<in> ns" by (rule inFr_root_in)
+ thus "t \<in> \<Union>{{t. inFr ns tr' t} |tr'. subtr ns tr' tr}"
+ apply(intro UnionI[of "{t. inFr ns tr t}" _ t]) using t subtr.Refl by auto
+qed(metis subtr_inFr)
+
+lemma inFr_subtr:
+assumes "inFr ns tr t"
+shows "\<exists> tr'. subtr ns tr' tr \<and> Inl t \<in> cont tr'"
+using assms apply(induct rule: inFr.induct) apply safe
+ apply (metis subtr.Refl)
+ by (metis (lifting) subtr.Step)
+
+corollary Fr_subtr_cont:
+"Fr ns tr = \<Union> {Inl -` cont tr' | tr'. subtr ns tr' tr}"
+unfolding Fr_def
+apply safe
+apply (frule inFr_subtr)
+apply auto
+by (metis inFr.Base subtr_inFr subtr_rootL_in)
+
+(* Subtree versus interior: *)
+lemma subtr_inItr:
+assumes "inItr ns tr n" and "subtr ns tr tr1"
+shows "inItr ns tr1 n"
+proof-
+ have "subtr ns tr tr1 \<Longrightarrow> (\<forall> t. inItr ns tr n \<longrightarrow> inItr ns tr1 n)"
+ apply(induct rule: subtr.induct, safe) by (metis inItr.Ind)
+ thus ?thesis using assms by auto
+qed
+
+corollary Itr_subtr:
+"Itr ns tr = \<Union> {Itr ns tr' | tr'. subtr ns tr' tr}"
+unfolding Itr_def apply safe
+apply (metis (lifting, mono_tags) UnionI inItr_root_in mem_Collect_eq subtr.Refl)
+by (metis subtr_inItr)
+
+lemma inItr_subtr:
+assumes "inItr ns tr n"
+shows "\<exists> tr'. subtr ns tr' tr \<and> root tr' = n"
+using assms apply(induct rule: inItr.induct) apply safe
+ apply (metis subtr.Refl)
+ by (metis (lifting) subtr.Step)
+
+corollary Itr_subtr_cont:
+"Itr ns tr = {root tr' | tr'. subtr ns tr' tr}"
+unfolding Itr_def apply safe
+ apply (metis (lifting, mono_tags) inItr_subtr)
+ by (metis inItr.Base subtr_inItr subtr_rootL_in)
+
+
+subsection{* The Immediate Subtree Function *}
+
+(* production of: *)
+abbreviation "prodOf tr \<equiv> (id \<oplus> root) ` (cont tr)"
+(* subtree of: *)
+definition "subtrOf tr n \<equiv> SOME tr'. Inr tr' \<in> cont tr \<and> root tr' = n"
+
+lemma subtrOf:
+assumes n: "Inr n \<in> prodOf tr"
+shows "Inr (subtrOf tr n) \<in> cont tr \<and> root (subtrOf tr n) = n"
+proof-
+ obtain tr' where "Inr tr' \<in> cont tr \<and> root tr' = n"
+ using n unfolding image_def by (metis (lifting) Inr_oplus_elim assms)
+ thus ?thesis unfolding subtrOf_def by(rule someI)
+qed
+
+lemmas Inr_subtrOf = subtrOf[THEN conjunct1]
+lemmas root_subtrOf[simp] = subtrOf[THEN conjunct2]
+
+lemma Inl_prodOf: "Inl -` (prodOf tr) = Inl -` (cont tr)"
+proof safe
+ fix t ttr assume "Inl t = (id \<oplus> root) ttr" and "ttr \<in> cont tr"
+ thus "t \<in> Inl -` cont tr" by(cases ttr, auto)
+next
+ fix t assume "Inl t \<in> cont tr" thus "t \<in> Inl -` prodOf tr"
+ by (metis (lifting) id_def image_iff sum_map.simps(1) vimageI2)
+qed
+
+lemma root_prodOf:
+assumes "Inr tr' \<in> cont tr"
+shows "Inr (root tr') \<in> prodOf tr"
+by (metis (lifting) assms image_iff sum_map.simps(2))
+
+
+subsection{* Well-Formed Derivation Trees *}
+
+hide_const wf
+
+coinductive wf where
+dtree: "\<lbrakk>(root tr, (id \<oplus> root) ` (cont tr)) \<in> P; inj_on root (Inr -` cont tr);
+ \<And> tr'. tr' \<in> Inr -` (cont tr) \<Longrightarrow> wf tr'\<rbrakk> \<Longrightarrow> wf tr"
+
+(* destruction rules: *)
+lemma wf_P:
+assumes "wf tr"
+shows "(root tr, (id \<oplus> root) ` (cont tr)) \<in> P"
+using assms wf.simps[of tr] by auto
+
+lemma wf_inj_on:
+assumes "wf tr"
+shows "inj_on root (Inr -` cont tr)"
+using assms wf.simps[of tr] by auto
+
+lemma wf_inj[simp]:
+assumes "wf tr" and "Inr tr1 \<in> cont tr" and "Inr tr2 \<in> cont tr"
+shows "root tr1 = root tr2 \<longleftrightarrow> tr1 = tr2"
+using assms wf_inj_on unfolding inj_on_def by auto
+
+lemma wf_cont:
+assumes "wf tr" and "Inr tr' \<in> cont tr"
+shows "wf tr'"
+using assms wf.simps[of tr] by auto
+
+
+(* coinduction:*)
+lemma wf_coind[elim, consumes 1, case_names Hyp]:
+assumes phi: "\<phi> tr"
+and Hyp:
+"\<And> tr. \<phi> tr \<Longrightarrow>
+ (root tr, image (id \<oplus> root) (cont tr)) \<in> P \<and>
+ inj_on root (Inr -` cont tr) \<and>
+ (\<forall> tr' \<in> Inr -` (cont tr). \<phi> tr' \<or> wf tr')"
+shows "wf tr"
+apply(rule wf.coinduct[of \<phi> tr, OF phi])
+using Hyp by blast
+
+lemma wf_raw_coind[elim, consumes 1, case_names Hyp]:
+assumes phi: "\<phi> tr"
+and Hyp:
+"\<And> tr. \<phi> tr \<Longrightarrow>
+ (root tr, image (id \<oplus> root) (cont tr)) \<in> P \<and>
+ inj_on root (Inr -` cont tr) \<and>
+ (\<forall> tr' \<in> Inr -` (cont tr). \<phi> tr')"
+shows "wf tr"
+using phi apply(induct rule: wf_coind)
+using Hyp by (metis (mono_tags))
+
+lemma wf_subtr_inj_on:
+assumes d: "wf tr1" and s: "subtr ns tr tr1"
+shows "inj_on root (Inr -` cont tr)"
+using s d apply(induct rule: subtr.induct)
+apply (metis (lifting) wf_inj_on) by (metis wf_cont)
+
+lemma wf_subtr_P:
+assumes d: "wf tr1" and s: "subtr ns tr tr1"
+shows "(root tr, (id \<oplus> root) ` cont tr) \<in> P"
+using s d apply(induct rule: subtr.induct)
+apply (metis (lifting) wf_P) by (metis wf_cont)
+
+lemma subtrOf_root[simp]:
+assumes tr: "wf tr" and cont: "Inr tr' \<in> cont tr"
+shows "subtrOf tr (root tr') = tr'"
+proof-
+ have 0: "Inr (subtrOf tr (root tr')) \<in> cont tr" using Inr_subtrOf
+ by (metis (lifting) cont root_prodOf)
+ have "root (subtrOf tr (root tr')) = root tr'"
+ using root_subtrOf by (metis (lifting) cont root_prodOf)
+ thus ?thesis unfolding wf_inj[OF tr 0 cont] .
+qed
+
+lemma surj_subtrOf:
+assumes "wf tr" and 0: "Inr tr' \<in> cont tr"
+shows "\<exists> n. Inr n \<in> prodOf tr \<and> subtrOf tr n = tr'"
+apply(rule exI[of _ "root tr'"])
+using root_prodOf[OF 0] subtrOf_root[OF assms] by simp
+
+lemma wf_subtr:
+assumes "wf tr1" and "subtr ns tr tr1"
+shows "wf tr"
+proof-
+ have "(\<exists> ns tr1. wf tr1 \<and> subtr ns tr tr1) \<Longrightarrow> wf tr"
+ proof (induct rule: wf_raw_coind)
+ case (Hyp tr)
+ then obtain ns tr1 where tr1: "wf tr1" and tr_tr1: "subtr ns tr tr1" by auto
+ show ?case proof safe
+ show "(root tr, (id \<oplus> root) ` cont tr) \<in> P" using wf_subtr_P[OF tr1 tr_tr1] .
+ next
+ show "inj_on root (Inr -` cont tr)" using wf_subtr_inj_on[OF tr1 tr_tr1] .
+ next
+ fix tr' assume tr': "Inr tr' \<in> cont tr"
+ have tr_tr1: "subtr (ns \<union> {root tr'}) tr tr1" using subtr_mono[OF tr_tr1] by auto
+ have "subtr (ns \<union> {root tr'}) tr' tr1" using subtr_StepL[OF _ tr' tr_tr1] by auto
+ thus "\<exists>ns' tr1. wf tr1 \<and> subtr ns' tr' tr1" using tr1 by blast
+ qed
+ qed
+ thus ?thesis using assms by auto
+qed
+
+
+subsection{* Default Trees *}
+
+(* Pick a left-hand side of a production for each nonterminal *)
+definition S where "S n \<equiv> SOME tns. (n,tns) \<in> P"
+
+lemma S_P: "(n, S n) \<in> P"
+using used unfolding S_def by(rule someI_ex)
+
+lemma finite_S: "finite (S n)"
+using S_P finite_in_P by auto
+
+
+(* The default tree of a nonterminal *)
+definition deftr :: "N \<Rightarrow> dtree" where
+"deftr \<equiv> unfold id S"
+
+lemma deftr_simps[simp]:
+"root (deftr n) = n"
+"cont (deftr n) = image (id \<oplus> deftr) (S n)"
+using unfold(1)[of id S n] unfold(2)[of S n id, OF finite_S]
+unfolding deftr_def by simp_all
+
+lemmas root_deftr = deftr_simps(1)
+lemmas cont_deftr = deftr_simps(2)
+
+lemma root_o_deftr[simp]: "root o deftr = id"
+by (rule ext, auto)
+
+lemma wf_deftr: "wf (deftr n)"
+proof-
+ {fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
+ apply(induct rule: wf_raw_coind) apply safe
+ unfolding deftr_simps image_compose[symmetric] sum_map.comp id_o
+ root_o_deftr sum_map.id image_id id_apply apply(rule S_P)
+ unfolding inj_on_def by auto
+ }
+ thus ?thesis by auto
+qed
+
+
+subsection{* Hereditary Substitution *}
+
+(* Auxiliary concept: The root-ommiting frontier: *)
+definition "inFrr ns tr t \<equiv> \<exists> tr'. Inr tr' \<in> cont tr \<and> inFr ns tr' t"
+definition "Frr ns tr \<equiv> {t. \<exists> tr'. Inr tr' \<in> cont tr \<and> t \<in> Fr ns tr'}"
+
+context
+fixes tr0 :: dtree
+begin
+
+definition "hsubst_r tr \<equiv> root tr"
+definition "hsubst_c tr \<equiv> if root tr = root tr0 then cont tr0 else cont tr"
+
+(* Hereditary substitution: *)
+definition hsubst :: "dtree \<Rightarrow> dtree" where
+"hsubst \<equiv> unfold hsubst_r hsubst_c"
+
+lemma finite_hsubst_c: "finite (hsubst_c n)"
+unfolding hsubst_c_def by (metis (full_types) finite_cont)
+
+lemma root_hsubst[simp]: "root (hsubst tr) = root tr"
+using unfold(1)[of hsubst_r hsubst_c tr] unfolding hsubst_def hsubst_r_def by simp
+
+lemma root_o_subst[simp]: "root o hsubst = root"
+unfolding comp_def root_hsubst ..
+
+lemma cont_hsubst_eq[simp]:
+assumes "root tr = root tr0"
+shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr0)"
+apply(subst id_o[symmetric, of id]) unfolding id_o
+using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
+unfolding hsubst_def hsubst_c_def using assms by simp
+
+lemma hsubst_eq:
+assumes "root tr = root tr0"
+shows "hsubst tr = hsubst tr0"
+apply(rule dtree_cong) using assms cont_hsubst_eq by auto
+
+lemma cont_hsubst_neq[simp]:
+assumes "root tr \<noteq> root tr0"
+shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr)"
+apply(subst id_o[symmetric, of id]) unfolding id_o
+using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
+unfolding hsubst_def hsubst_c_def using assms by simp
+
+lemma Inl_cont_hsubst_eq[simp]:
+assumes "root tr = root tr0"
+shows "Inl -` cont (hsubst tr) = Inl -` (cont tr0)"
+unfolding cont_hsubst_eq[OF assms] by simp
+
+lemma Inr_cont_hsubst_eq[simp]:
+assumes "root tr = root tr0"
+shows "Inr -` cont (hsubst tr) = hsubst ` Inr -` cont tr0"
+unfolding cont_hsubst_eq[OF assms] by simp
+
+lemma Inl_cont_hsubst_neq[simp]:
+assumes "root tr \<noteq> root tr0"
+shows "Inl -` cont (hsubst tr) = Inl -` (cont tr)"
+unfolding cont_hsubst_neq[OF assms] by simp
+
+lemma Inr_cont_hsubst_neq[simp]:
+assumes "root tr \<noteq> root tr0"
+shows "Inr -` cont (hsubst tr) = hsubst ` Inr -` cont tr"
+unfolding cont_hsubst_neq[OF assms] by simp
+
+lemma wf_hsubst:
+assumes tr0: "wf tr0" and tr: "wf tr"
+shows "wf (hsubst tr)"
+proof-
+ {fix tr1 have "(\<exists> tr. wf tr \<and> tr1 = hsubst tr) \<Longrightarrow> wf tr1"
+ proof (induct rule: wf_raw_coind)
+ case (Hyp tr1) then obtain tr
+ where dtr: "wf tr" and tr1: "tr1 = hsubst tr" by auto
+ show ?case unfolding tr1 proof safe
+ show "(root (hsubst tr), prodOf (hsubst tr)) \<in> P"
+ unfolding tr1 apply(cases "root tr = root tr0")
+ using wf_P[OF dtr] wf_P[OF tr0]
+ by (auto simp add: image_compose[symmetric] sum_map.comp)
+ show "inj_on root (Inr -` cont (hsubst tr))"
+ apply(cases "root tr = root tr0") using wf_inj_on[OF dtr] wf_inj_on[OF tr0]
+ unfolding inj_on_def by (auto, blast)
+ fix tr' assume "Inr tr' \<in> cont (hsubst tr)"
+ thus "\<exists>tra. wf tra \<and> tr' = hsubst tra"
+ apply(cases "root tr = root tr0", simp_all)
+ apply (metis wf_cont tr0)
+ by (metis dtr wf_cont)
+ qed
+ qed
+ }
+ thus ?thesis using assms by blast
+qed
+
+lemma Frr: "Frr ns tr = {t. inFrr ns tr t}"
+unfolding inFrr_def Frr_def Fr_def by auto
+
+lemma inFr_hsubst_imp:
+assumes "inFr ns (hsubst tr) t"
+shows "t \<in> Inl -` (cont tr0) \<or> inFrr (ns - {root tr0}) tr0 t \<or>
+ inFr (ns - {root tr0}) tr t"
+proof-
+ {fix tr1
+ have "inFr ns tr1 t \<Longrightarrow>
+ (\<And> tr. tr1 = hsubst tr \<Longrightarrow> (t \<in> Inl -` (cont tr0) \<or> inFrr (ns - {root tr0}) tr0 t \<or>
+ inFr (ns - {root tr0}) tr t))"
+ proof(induct rule: inFr.induct)
+ case (Base tr1 ns t tr)
+ hence rtr: "root tr1 \<in> ns" and t_tr1: "Inl t \<in> cont tr1" and tr1: "tr1 = hsubst tr"
+ by auto
+ show ?case
+ proof(cases "root tr1 = root tr0")
+ case True
+ hence "t \<in> Inl -` (cont tr0)" using t_tr1 unfolding tr1 by auto
+ thus ?thesis by simp
+ next
+ case False
+ hence "inFr (ns - {root tr0}) tr t" using t_tr1 unfolding tr1 apply simp
+ by (metis Base.prems Diff_iff root_hsubst inFr.Base rtr singletonE)
+ thus ?thesis by simp
+ qed
+ next
+ case (Ind tr1 ns tr1' t) note IH = Ind(4)
+ have rtr1: "root tr1 \<in> ns" and tr1'_tr1: "Inr tr1' \<in> cont tr1"
+ and t_tr1': "inFr ns tr1' t" and tr1: "tr1 = hsubst tr" using Ind by auto
+ have rtr1: "root tr1 = root tr" unfolding tr1 by simp
+ show ?case
+ proof(cases "root tr1 = root tr0")
+ case True
+ then obtain tr' where tr'_tr0: "Inr tr' \<in> cont tr0" and tr1': "tr1' = hsubst tr'"
+ using tr1'_tr1 unfolding tr1 by auto
+ show ?thesis using IH[OF tr1'] proof (elim disjE)
+ assume "inFr (ns - {root tr0}) tr' t"
+ thus ?thesis using tr'_tr0 unfolding inFrr_def by auto
+ qed auto
+ next
+ case False
+ then obtain tr' where tr'_tr: "Inr tr' \<in> cont tr" and tr1': "tr1' = hsubst tr'"
+ using tr1'_tr1 unfolding tr1 by auto
+ show ?thesis using IH[OF tr1'] proof (elim disjE)
+ assume "inFr (ns - {root tr0}) tr' t"
+ thus ?thesis using tr'_tr unfolding inFrr_def
+ by (metis Diff_iff False Ind(1) empty_iff inFr2_Ind inFr_inFr2 insert_iff rtr1)
+ qed auto
+ qed
+ qed
+ }
+ thus ?thesis using assms by auto
+qed
+
+lemma inFr_hsubst_notin:
+assumes "inFr ns tr t" and "root tr0 \<notin> ns"
+shows "inFr ns (hsubst tr) t"
+using assms apply(induct rule: inFr.induct)
+apply (metis Inl_cont_hsubst_neq inFr2.Base inFr_inFr2 root_hsubst vimageD vimageI2)
+by (metis (lifting) Inr_cont_hsubst_neq inFr.Ind rev_image_eqI root_hsubst vimageD vimageI2)
+
+lemma inFr_hsubst_minus:
+assumes "inFr (ns - {root tr0}) tr t"
+shows "inFr ns (hsubst tr) t"
+proof-
+ have 1: "inFr (ns - {root tr0}) (hsubst tr) t"
+ using inFr_hsubst_notin[OF assms] by simp
+ show ?thesis using inFr_mono[OF 1] by auto
+qed
+
+lemma inFr_self_hsubst:
+assumes "root tr0 \<in> ns"
+shows
+"inFr ns (hsubst tr0) t \<longleftrightarrow>
+ t \<in> Inl -` (cont tr0) \<or> inFrr (ns - {root tr0}) tr0 t"
+(is "?A \<longleftrightarrow> ?B \<or> ?C")
+apply(intro iffI)
+apply (metis inFr_hsubst_imp Diff_iff inFr_root_in insertI1) proof(elim disjE)
+ assume ?B thus ?A apply(intro inFr.Base) using assms by auto
+next
+ assume ?C then obtain tr where
+ tr_tr0: "Inr tr \<in> cont tr0" and t_tr: "inFr (ns - {root tr0}) tr t"
+ unfolding inFrr_def by auto
+ def tr1 \<equiv> "hsubst tr"
+ have 1: "inFr ns tr1 t" using t_tr unfolding tr1_def using inFr_hsubst_minus by auto
+ have "Inr tr1 \<in> cont (hsubst tr0)" unfolding tr1_def using tr_tr0 by auto
+ thus ?A using 1 inFr.Ind assms by (metis root_hsubst)
+qed
+
+lemma Fr_self_hsubst:
+assumes "root tr0 \<in> ns"
+shows "Fr ns (hsubst tr0) = Inl -` (cont tr0) \<union> Frr (ns - {root tr0}) tr0"
+using inFr_self_hsubst[OF assms] unfolding Frr Fr_def by auto
+
+end (* context *)
+
+
+subsection{* Regular Trees *}
+
+hide_const regular
+
+definition "reg f tr \<equiv> \<forall> tr'. subtr UNIV tr' tr \<longrightarrow> tr' = f (root tr')"
+definition "regular tr \<equiv> \<exists> f. reg f tr"
+
+lemma reg_def2: "reg f tr \<longleftrightarrow> (\<forall> ns tr'. subtr ns tr' tr \<longrightarrow> tr' = f (root tr'))"
+unfolding reg_def using subtr_mono by (metis subset_UNIV)
+
+lemma regular_def2: "regular tr \<longleftrightarrow> (\<exists> f. reg f tr \<and> (\<forall> n. root (f n) = n))"
+unfolding regular_def proof safe
+ fix f assume f: "reg f tr"
+ def g \<equiv> "\<lambda> n. if inItr UNIV tr n then f n else deftr n"
+ show "\<exists>g. reg g tr \<and> (\<forall>n. root (g n) = n)"
+ apply(rule exI[of _ g])
+ using f deftr_simps(1) unfolding g_def reg_def apply safe
+ apply (metis (lifting) inItr.Base subtr_inItr subtr_rootL_in)
+ by (metis (full_types) inItr_subtr)
+qed auto
+
+lemma reg_root:
+assumes "reg f tr"
+shows "f (root tr) = tr"
+using assms unfolding reg_def
+by (metis (lifting) iso_tuple_UNIV_I subtr.Refl)
+
+
+lemma reg_Inr_cont:
+assumes "reg f tr" and "Inr tr' \<in> cont tr"
+shows "reg f tr'"
+by (metis (lifting) assms iso_tuple_UNIV_I reg_def subtr.Step)
+
+lemma reg_subtr:
+assumes "reg f tr" and "subtr ns tr' tr"
+shows "reg f tr'"
+using assms unfolding reg_def using subtr_trans[of UNIV tr] UNIV_I
+by (metis UNIV_eq_I UnCI Un_upper1 iso_tuple_UNIV_I subtr_mono subtr_trans)
+
+lemma regular_subtr:
+assumes r: "regular tr" and s: "subtr ns tr' tr"
+shows "regular tr'"
+using r reg_subtr[OF _ s] unfolding regular_def by auto
+
+lemma subtr_deftr:
+assumes "subtr ns tr' (deftr n)"
+shows "tr' = deftr (root tr')"
+proof-
+ {fix tr have "subtr ns tr' tr \<Longrightarrow> (\<forall> n. tr = deftr n \<longrightarrow> tr' = deftr (root tr'))"
+ apply (induct rule: subtr.induct)
+ proof(metis (lifting) deftr_simps(1), safe)
+ fix tr3 ns tr1 tr2 n
+ assume 1: "root (deftr n) \<in> ns" and 2: "subtr ns tr1 tr2"
+ and IH: "\<forall>n. tr2 = deftr n \<longrightarrow> tr1 = deftr (root tr1)"
+ and 3: "Inr tr2 \<in> cont (deftr n)"
+ have "tr2 \<in> deftr ` UNIV"
+ using 3 unfolding deftr_simps image_def
+ by (metis (lifting, full_types) 3 CollectI Inr_oplus_iff cont_deftr
+ iso_tuple_UNIV_I)
+ then obtain n where "tr2 = deftr n" by auto
+ thus "tr1 = deftr (root tr1)" using IH by auto
+ qed
+ }
+ thus ?thesis using assms by auto
+qed
+
+lemma reg_deftr: "reg deftr (deftr n)"
+unfolding reg_def using subtr_deftr by auto
+
+lemma wf_subtrOf_Union:
+assumes "wf tr"
+shows "\<Union>{K tr' |tr'. Inr tr' \<in> cont tr} =
+ \<Union>{K (subtrOf tr n) |n. Inr n \<in> prodOf tr}"
+unfolding Union_eq Bex_def mem_Collect_eq proof safe
+ fix x xa tr'
+ assume x: "x \<in> K tr'" and tr'_tr: "Inr tr' \<in> cont tr"
+ show "\<exists>X. (\<exists>n. X = K (subtrOf tr n) \<and> Inr n \<in> prodOf tr) \<and> x \<in> X"
+ apply(rule exI[of _ "K (subtrOf tr (root tr'))"]) apply(intro conjI)
+ apply(rule exI[of _ "root tr'"]) apply (metis (lifting) root_prodOf tr'_tr)
+ by (metis (lifting) assms subtrOf_root tr'_tr x)
+next
+ fix x X n ttr
+ assume x: "x \<in> K (subtrOf tr n)" and n: "Inr n = (id \<oplus> root) ttr" and ttr: "ttr \<in> cont tr"
+ show "\<exists>X. (\<exists>tr'. X = K tr' \<and> Inr tr' \<in> cont tr) \<and> x \<in> X"
+ apply(rule exI[of _ "K (subtrOf tr n)"]) apply(intro conjI)
+ apply(rule exI[of _ "subtrOf tr n"]) apply (metis imageI n subtrOf ttr)
+ using x .
+qed
+
+
+
+
+subsection {* Paths in a Regular Tree *}
+
+inductive path :: "(N \<Rightarrow> dtree) \<Rightarrow> N list \<Rightarrow> bool" for f where
+Base: "path f [n]"
+|
+Ind: "\<lbrakk>path f (n1 # nl); Inr (f n1) \<in> cont (f n)\<rbrakk>
+ \<Longrightarrow> path f (n # n1 # nl)"
+
+lemma path_NE:
+assumes "path f nl"
+shows "nl \<noteq> Nil"
+using assms apply(induct rule: path.induct) by auto
+
+lemma path_post:
+assumes f: "path f (n # nl)" and nl: "nl \<noteq> []"
+shows "path f nl"
+proof-
+ obtain n1 nl1 where nl: "nl = n1 # nl1" using nl by (cases nl, auto)
+ show ?thesis using assms unfolding nl using path.simps by (metis (lifting) list.inject)
+qed
+
+lemma path_post_concat:
+assumes "path f (nl1 @ nl2)" and "nl2 \<noteq> Nil"
+shows "path f nl2"
+using assms apply (induct nl1)
+apply (metis append_Nil) by (metis Nil_is_append_conv append_Cons path_post)
+
+lemma path_concat:
+assumes "path f nl1" and "path f ((last nl1) # nl2)"
+shows "path f (nl1 @ nl2)"
+using assms apply(induct rule: path.induct) apply simp
+by (metis append_Cons last.simps list.simps(3) path.Ind)
+
+lemma path_distinct:
+assumes "path f nl"
+shows "\<exists> nl'. path f nl' \<and> hd nl' = hd nl \<and> last nl' = last nl \<and>
+ set nl' \<subseteq> set nl \<and> distinct nl'"
+using assms proof(induct rule: length_induct)
+ case (1 nl) hence p_nl: "path f nl" by simp
+ then obtain n nl1 where nl: "nl = n # nl1" by (metis list.exhaust path_NE)
+ show ?case
+ proof(cases nl1)
+ case Nil
+ show ?thesis apply(rule exI[of _ nl]) using path.Base unfolding nl Nil by simp
+ next
+ case (Cons n1 nl2)
+ hence p1: "path f nl1" by (metis list.simps(3) nl p_nl path_post)
+ show ?thesis
+ proof(cases "n \<in> set nl1")
+ case False
+ obtain nl1' where p1': "path f nl1'" and hd_nl1': "hd nl1' = hd nl1" and
+ l_nl1': "last nl1' = last nl1" and d_nl1': "distinct nl1'"
+ and s_nl1': "set nl1' \<subseteq> set nl1"
+ using 1(1)[THEN allE[of _ nl1]] p1 unfolding nl by auto
+ obtain nl2' where nl1': "nl1' = n1 # nl2'" using path_NE[OF p1'] hd_nl1'
+ unfolding Cons by(cases nl1', auto)
+ show ?thesis apply(intro exI[of _ "n # nl1'"]) unfolding nl proof safe
+ show "path f (n # nl1')" unfolding nl1'
+ apply(rule path.Ind, metis nl1' p1')
+ by (metis (lifting) Cons list.inject nl p1 p_nl path.simps path_NE)
+ qed(insert l_nl1' Cons nl1' s_nl1' d_nl1' False, auto)
+ next
+ case True
+ then obtain nl11 nl12 where nl1: "nl1 = nl11 @ n # nl12"
+ by (metis split_list)
+ have p12: "path f (n # nl12)"
+ apply(rule path_post_concat[of _ "n # nl11"]) using p_nl[unfolded nl nl1] by auto
+ obtain nl12' where p1': "path f nl12'" and hd_nl12': "hd nl12' = n" and
+ l_nl12': "last nl12' = last (n # nl12)" and d_nl12': "distinct nl12'"
+ and s_nl12': "set nl12' \<subseteq> {n} \<union> set nl12"
+ using 1(1)[THEN allE[of _ "n # nl12"]] p12 unfolding nl nl1 by auto
+ thus ?thesis apply(intro exI[of _ nl12']) unfolding nl nl1 by auto
+ qed
+ qed
+qed
+
+lemma path_subtr:
+assumes f: "\<And> n. root (f n) = n"
+and p: "path f nl"
+shows "subtr (set nl) (f (last nl)) (f (hd nl))"
+using p proof (induct rule: path.induct)
+ case (Ind n1 nl n) let ?ns1 = "insert n1 (set nl)"
+ have "path f (n1 # nl)"
+ and "subtr ?ns1 (f (last (n1 # nl))) (f n1)"
+ and fn1: "Inr (f n1) \<in> cont (f n)" using Ind by simp_all
+ hence fn1_flast: "subtr (insert n ?ns1) (f (last (n1 # nl))) (f n1)"
+ by (metis subset_insertI subtr_mono)
+ have 1: "last (n # n1 # nl) = last (n1 # nl)" by auto
+ have "subtr (insert n ?ns1) (f (last (n1 # nl))) (f n)"
+ using f subtr.Step[OF _ fn1_flast fn1] by auto
+ thus ?case unfolding 1 by simp
+qed (metis f hd.simps last_ConsL last_in_set not_Cons_self2 subtr.Refl)
+
+lemma reg_subtr_path_aux:
+assumes f: "reg f tr" and n: "subtr ns tr1 tr"
+shows "\<exists> nl. path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and> set nl \<subseteq> ns"
+using n f proof(induct rule: subtr.induct)
+ case (Refl tr ns)
+ thus ?case
+ apply(intro exI[of _ "[root tr]"]) apply simp by (metis (lifting) path.Base reg_root)
+next
+ case (Step tr ns tr2 tr1)
+ hence rtr: "root tr \<in> ns" and tr1_tr: "Inr tr1 \<in> cont tr"
+ and tr2_tr1: "subtr ns tr2 tr1" and tr: "reg f tr" by auto
+ have tr1: "reg f tr1" using reg_subtr[OF tr] rtr tr1_tr
+ by (metis (lifting) Step.prems iso_tuple_UNIV_I reg_def subtr.Step)
+ obtain nl where nl: "path f nl" and f_nl: "f (hd nl) = tr1"
+ and last_nl: "f (last nl) = tr2" and set: "set nl \<subseteq> ns" using Step(3)[OF tr1] by auto
+ have 0: "path f (root tr # nl)" apply (subst path.simps)
+ using f_nl nl reg_root tr tr1_tr by (metis hd.simps neq_Nil_conv)
+ show ?case apply(rule exI[of _ "(root tr) # nl"])
+ using 0 reg_root tr last_nl nl path_NE rtr set by auto
+qed
+
+lemma reg_subtr_path:
+assumes f: "reg f tr" and n: "subtr ns tr1 tr"
+shows "\<exists> nl. distinct nl \<and> path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and> set nl \<subseteq> ns"
+using reg_subtr_path_aux[OF assms] path_distinct[of f]
+by (metis (lifting) order_trans)
+
+lemma subtr_iff_path:
+assumes r: "reg f tr" and f: "\<And> n. root (f n) = n"
+shows "subtr ns tr1 tr \<longleftrightarrow>
+ (\<exists> nl. distinct nl \<and> path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and> set nl \<subseteq> ns)"
+proof safe
+ fix nl assume p: "path f nl" and nl: "set nl \<subseteq> ns"
+ have "subtr (set nl) (f (last nl)) (f (hd nl))"
+ apply(rule path_subtr) using p f by simp_all
+ thus "subtr ns (f (last nl)) (f (hd nl))"
+ using subtr_mono nl by auto
+qed(insert reg_subtr_path[OF r], auto)
+
+lemma inFr_iff_path:
+assumes r: "reg f tr" and f: "\<And> n. root (f n) = n"
+shows
+"inFr ns tr t \<longleftrightarrow>
+ (\<exists> nl tr1. distinct nl \<and> path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and>
+ set nl \<subseteq> ns \<and> Inl t \<in> cont tr1)"
+apply safe
+apply (metis (no_types) inFr_subtr r reg_subtr_path)
+by (metis f inFr.Base path_subtr subtr_inFr subtr_mono subtr_rootL_in)
+
+
+
+subsection{* The Regular Cut of a Tree *}
+
+context fixes tr0 :: dtree
+begin
+
+(* Picking a subtree of a certain root: *)
+definition "pick n \<equiv> SOME tr. subtr UNIV tr tr0 \<and> root tr = n"
+
+lemma pick:
+assumes "inItr UNIV tr0 n"
+shows "subtr UNIV (pick n) tr0 \<and> root (pick n) = n"
+proof-
+ have "\<exists> tr. subtr UNIV tr tr0 \<and> root tr = n"
+ using assms by (metis (lifting) inItr_subtr)
+ thus ?thesis unfolding pick_def by(rule someI_ex)
+qed
+
+lemmas subtr_pick = pick[THEN conjunct1]
+lemmas root_pick = pick[THEN conjunct2]
+
+lemma wf_pick:
+assumes tr0: "wf tr0" and n: "inItr UNIV tr0 n"
+shows "wf (pick n)"
+using wf_subtr[OF tr0 subtr_pick[OF n]] .
+
+definition "H_r n \<equiv> root (pick n)"
+definition "H_c n \<equiv> (id \<oplus> root) ` cont (pick n)"
+
+(* The regular tree of a function: *)
+definition H :: "N \<Rightarrow> dtree" where
+"H \<equiv> unfold H_r H_c"
+
+lemma finite_H_c: "finite (H_c n)"
+unfolding H_c_def by (metis finite_cont finite_imageI)
+
+lemma root_H_pick: "root (H n) = root (pick n)"
+using unfold(1)[of H_r H_c n] unfolding H_def H_r_def by simp
+
+lemma root_H[simp]:
+assumes "inItr UNIV tr0 n"
+shows "root (H n) = n"
+unfolding root_H_pick root_pick[OF assms] ..
+
+lemma cont_H[simp]:
+"cont (H n) = (id \<oplus> (H o root)) ` cont (pick n)"
+apply(subst id_o[symmetric, of id]) unfolding sum_map.comp[symmetric]
+unfolding image_compose unfolding H_c_def[symmetric]
+using unfold(2)[of H_c n H_r, OF finite_H_c]
+unfolding H_def ..
+
+lemma Inl_cont_H[simp]:
+"Inl -` (cont (H n)) = Inl -` (cont (pick n))"
+unfolding cont_H by simp
+
+lemma Inr_cont_H:
+"Inr -` (cont (H n)) = (H \<circ> root) ` (Inr -` cont (pick n))"
+unfolding cont_H by simp
+
+lemma subtr_H:
+assumes n: "inItr UNIV tr0 n" and "subtr UNIV tr1 (H n)"
+shows "\<exists> n1. inItr UNIV tr0 n1 \<and> tr1 = H n1"
+proof-
+ {fix tr ns assume "subtr UNIV tr1 tr"
+ hence "tr = H n \<longrightarrow> (\<exists> n1. inItr UNIV tr0 n1 \<and> tr1 = H n1)"
+ proof (induct rule: subtr_UNIV_inductL)
+ case (Step tr2 tr1 tr)
+ show ?case proof
+ assume "tr = H n"
+ then obtain n1 where tr2: "Inr tr2 \<in> cont tr1"
+ and tr1_tr: "subtr UNIV tr1 tr" and n1: "inItr UNIV tr0 n1" and tr1: "tr1 = H n1"
+ using Step by auto
+ obtain tr2' where tr2: "tr2 = H (root tr2')"
+ and tr2': "Inr tr2' \<in> cont (pick n1)"
+ using tr2 Inr_cont_H[of n1]
+ unfolding tr1 image_def o_def using vimage_eq by auto
+ have "inItr UNIV tr0 (root tr2')"
+ using inItr.Base inItr.Ind n1 pick subtr_inItr tr2' by (metis iso_tuple_UNIV_I)
+ thus "\<exists>n2. inItr UNIV tr0 n2 \<and> tr2 = H n2" using tr2 by blast
+ qed
+ qed(insert n, auto)
+ }
+ thus ?thesis using assms by auto
+qed
+
+lemma root_H_root:
+assumes n: "inItr UNIV tr0 n" and t_tr: "t_tr \<in> cont (pick n)"
+shows "(id \<oplus> (root \<circ> H \<circ> root)) t_tr = (id \<oplus> root) t_tr"
+using assms apply(cases t_tr)
+ apply (metis (lifting) sum_map.simps(1))
+ using pick H_def H_r_def unfold(1)
+ inItr.Base o_apply subtr_StepL subtr_inItr sum_map.simps(2)
+ by (metis UNIV_I)
+
+lemma H_P:
+assumes tr0: "wf tr0" and n: "inItr UNIV tr0 n"
+shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
+proof-
+ have "?L = (n, (id \<oplus> root) ` cont (pick n))"
+ unfolding cont_H image_compose[symmetric] sum_map.comp id_o o_assoc
+ unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
+ by(rule root_H_root[OF n])
+ moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
+ ultimately show ?thesis by simp
+qed
+
+lemma wf_H:
+assumes tr0: "wf tr0" and "inItr UNIV tr0 n"
+shows "wf (H n)"
+proof-
+ {fix tr have "\<exists> n. inItr UNIV tr0 n \<and> tr = H n \<Longrightarrow> wf tr"
+ proof (induct rule: wf_raw_coind)
+ case (Hyp tr)
+ then obtain n where n: "inItr UNIV tr0 n" and tr: "tr = H n" by auto
+ show ?case apply safe
+ apply (metis (lifting) H_P root_H n tr tr0)
+ unfolding tr Inr_cont_H unfolding inj_on_def apply clarsimp using root_H
+ apply (metis UNIV_I inItr.Base n pick subtr2.simps subtr_inItr subtr_subtr2)
+ by (metis n subtr.Refl subtr_StepL subtr_H tr UNIV_I)
+ qed
+ }
+ thus ?thesis using assms by blast
+qed
+
+(* The regular cut of a tree: *)
+definition "rcut \<equiv> H (root tr0)"
+
+lemma reg_rcut: "reg H rcut"
+unfolding reg_def rcut_def
+by (metis inItr.Base root_H subtr_H UNIV_I)
+
+lemma rcut_reg:
+assumes "reg H tr0"
+shows "rcut = tr0"
+using assms unfolding rcut_def reg_def by (metis subtr.Refl UNIV_I)
+
+lemma rcut_eq: "rcut = tr0 \<longleftrightarrow> reg H tr0"
+using reg_rcut rcut_reg by metis
+
+lemma regular_rcut: "regular rcut"
+using reg_rcut unfolding regular_def by blast
+
+lemma Fr_rcut: "Fr UNIV rcut \<subseteq> Fr UNIV tr0"
+proof safe
+ fix t assume "t \<in> Fr UNIV rcut"
+ then obtain tr where t: "Inl t \<in> cont tr" and tr: "subtr UNIV tr (H (root tr0))"
+ using Fr_subtr[of UNIV "H (root tr0)"] unfolding rcut_def
+ by (metis (full_types) Fr_def inFr_subtr mem_Collect_eq)
+ obtain n where n: "inItr UNIV tr0 n" and tr: "tr = H n" using tr
+ by (metis (lifting) inItr.Base subtr_H UNIV_I)
+ have "Inl t \<in> cont (pick n)" using t using Inl_cont_H[of n] unfolding tr
+ by (metis (lifting) vimageD vimageI2)
+ moreover have "subtr UNIV (pick n) tr0" using subtr_pick[OF n] ..
+ ultimately show "t \<in> Fr UNIV tr0" unfolding Fr_subtr_cont by auto
+qed
+
+lemma wf_rcut:
+assumes "wf tr0"
+shows "wf rcut"
+unfolding rcut_def using wf_H[OF assms inItr.Base] by simp
+
+lemma root_rcut[simp]: "root rcut = root tr0"
+unfolding rcut_def
+by (metis (lifting) root_H inItr.Base reg_def reg_root subtr_rootR_in)
+
+end (* context *)
+
+
+subsection{* Recursive Description of the Regular Tree Frontiers *}
+
+lemma regular_inFr:
+assumes r: "regular tr" and In: "root tr \<in> ns"
+and t: "inFr ns tr t"
+shows "t \<in> Inl -` (cont tr) \<or>
+ (\<exists> tr'. Inr tr' \<in> cont tr \<and> inFr (ns - {root tr}) tr' t)"
+(is "?L \<or> ?R")
+proof-
+ obtain f where r: "reg f tr" and f: "\<And>n. root (f n) = n"
+ using r unfolding regular_def2 by auto
+ obtain nl tr1 where d_nl: "distinct nl" and p: "path f nl" and hd_nl: "f (hd nl) = tr"
+ and l_nl: "f (last nl) = tr1" and s_nl: "set nl \<subseteq> ns" and t_tr1: "Inl t \<in> cont tr1"
+ using t unfolding inFr_iff_path[OF r f] by auto
+ obtain n nl1 where nl: "nl = n # nl1" by (metis (lifting) p path.simps)
+ hence f_n: "f n = tr" using hd_nl by simp
+ have n_nl1: "n \<notin> set nl1" using d_nl unfolding nl by auto
+ show ?thesis
+ proof(cases nl1)
+ case Nil hence "tr = tr1" using f_n l_nl unfolding nl by simp
+ hence ?L using t_tr1 by simp thus ?thesis by simp
+ next
+ case (Cons n1 nl2) note nl1 = Cons
+ have 1: "last nl1 = last nl" "hd nl1 = n1" unfolding nl nl1 by simp_all
+ have p1: "path f nl1" and n1_tr: "Inr (f n1) \<in> cont tr"
+ using path.simps[of f nl] p f_n unfolding nl nl1 by auto
+ have r1: "reg f (f n1)" using reg_Inr_cont[OF r n1_tr] .
+ have 0: "inFr (set nl1) (f n1) t" unfolding inFr_iff_path[OF r1 f]
+ apply(intro exI[of _ nl1], intro exI[of _ tr1])
+ using d_nl unfolding 1 l_nl unfolding nl using p1 t_tr1 by auto
+ have root_tr: "root tr = n" by (metis f f_n)
+ have "inFr (ns - {root tr}) (f n1) t" apply(rule inFr_mono[OF 0])
+ using s_nl unfolding root_tr unfolding nl using n_nl1 by auto
+ thus ?thesis using n1_tr by auto
+ qed
+qed
+
+lemma regular_Fr:
+assumes r: "regular tr" and In: "root tr \<in> ns"
+shows "Fr ns tr =
+ Inl -` (cont tr) \<union>
+ \<Union> {Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
+unfolding Fr_def
+using In inFr.Base regular_inFr[OF assms] apply safe
+apply (simp, metis (full_types) mem_Collect_eq)
+apply simp
+by (simp, metis (lifting) inFr_Ind_minus insert_Diff)
+
+
+subsection{* The Generated Languages *}
+
+(* The (possibly inifinite tree) generated language *)
+definition "L ns n \<equiv> {Fr ns tr | tr. wf tr \<and> root tr = n}"
+
+(* The regular-tree generated language *)
+definition "Lr ns n \<equiv> {Fr ns tr | tr. wf tr \<and> root tr = n \<and> regular tr}"
+
+lemma L_rec_notin:
+assumes "n \<notin> ns"
+shows "L ns n = {{}}"
+using assms unfolding L_def apply safe
+ using not_root_Fr apply force
+ apply(rule exI[of _ "deftr n"])
+ by (metis (no_types) wf_deftr not_root_Fr root_deftr)
+
+lemma Lr_rec_notin:
+assumes "n \<notin> ns"
+shows "Lr ns n = {{}}"
+using assms unfolding Lr_def apply safe
+ using not_root_Fr apply force
+ apply(rule exI[of _ "deftr n"])
+ by (metis (no_types) regular_def wf_deftr not_root_Fr reg_deftr root_deftr)
+
+lemma wf_subtrOf:
+assumes "wf tr" and "Inr n \<in> prodOf tr"
+shows "wf (subtrOf tr n)"
+by (metis assms wf_cont subtrOf)
+
+lemma Lr_rec_in:
+assumes n: "n \<in> ns"
+shows "Lr ns n \<subseteq>
+{Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
+ (n,tns) \<in> P \<and>
+ (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> Lr (ns - {n}) n')}"
+(is "Lr ns n \<subseteq> {?F tns K | tns K. (n,tns) \<in> P \<and> ?\<phi> tns K}")
+proof safe
+ fix ts assume "ts \<in> Lr ns n"
+ then obtain tr where dtr: "wf tr" and r: "root tr = n" and tr: "regular tr"
+ and ts: "ts = Fr ns tr" unfolding Lr_def by auto
+ def tns \<equiv> "(id \<oplus> root) ` (cont tr)"
+ def K \<equiv> "\<lambda> n'. Fr (ns - {n}) (subtrOf tr n')"
+ show "\<exists>tns K. ts = ?F tns K \<and> (n, tns) \<in> P \<and> ?\<phi> tns K"
+ apply(rule exI[of _ tns], rule exI[of _ K]) proof(intro conjI allI impI)
+ show "ts = Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns}"
+ unfolding ts regular_Fr[OF tr n[unfolded r[symmetric]]]
+ unfolding tns_def K_def r[symmetric]
+ unfolding Inl_prodOf wf_subtrOf_Union[OF dtr] ..
+ show "(n, tns) \<in> P" unfolding tns_def r[symmetric] using wf_P[OF dtr] .
+ fix n' assume "Inr n' \<in> tns" thus "K n' \<in> Lr (ns - {n}) n'"
+ unfolding K_def Lr_def mem_Collect_eq apply(intro exI[of _ "subtrOf tr n'"])
+ using dtr tr apply(intro conjI refl) unfolding tns_def
+ apply(erule wf_subtrOf[OF dtr])
+ apply (metis subtrOf)
+ by (metis Inr_subtrOf UNIV_I regular_subtr subtr.simps)
+ qed
+qed
+
+lemma hsubst_aux:
+fixes n ftr tns
+assumes n: "n \<in> ns" and tns: "finite tns" and
+1: "\<And> n'. Inr n' \<in> tns \<Longrightarrow> wf (ftr n')"
+defines "tr \<equiv> Node n ((id \<oplus> ftr) ` tns)" defines "tr' \<equiv> hsubst tr tr"
+shows "Fr ns tr' = Inl -` tns \<union> \<Union>{Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns}"
+(is "_ = ?B") proof-
+ have rtr: "root tr = n" and ctr: "cont tr = (id \<oplus> ftr) ` tns"
+ unfolding tr_def using tns by auto
+ have Frr: "Frr (ns - {n}) tr = \<Union>{Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns}"
+ unfolding Frr_def ctr by auto
+ have "Fr ns tr' = Inl -` (cont tr) \<union> Frr (ns - {n}) tr"
+ using Fr_self_hsubst[OF n[unfolded rtr[symmetric]]] unfolding tr'_def rtr ..
+ also have "... = ?B" unfolding ctr Frr by simp
+ finally show ?thesis .
+qed
+
+lemma L_rec_in:
+assumes n: "n \<in> ns"
+shows "
+{Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
+ (n,tns) \<in> P \<and>
+ (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> L (ns - {n}) n')}
+ \<subseteq> L ns n"
+proof safe
+ fix tns K
+ assume P: "(n, tns) \<in> P" and 0: "\<forall>n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> L (ns - {n}) n'"
+ {fix n' assume "Inr n' \<in> tns"
+ hence "K n' \<in> L (ns - {n}) n'" using 0 by auto
+ hence "\<exists> tr'. K n' = Fr (ns - {n}) tr' \<and> wf tr' \<and> root tr' = n'"
+ unfolding L_def mem_Collect_eq by auto
+ }
+ then obtain ftr where 0: "\<And> n'. Inr n' \<in> tns \<Longrightarrow>
+ K n' = Fr (ns - {n}) (ftr n') \<and> wf (ftr n') \<and> root (ftr n') = n'"
+ by metis
+ def tr \<equiv> "Node n ((id \<oplus> ftr) ` tns)" def tr' \<equiv> "hsubst tr tr"
+ have rtr: "root tr = n" and ctr: "cont tr = (id \<oplus> ftr) ` tns"
+ unfolding tr_def by (simp, metis P cont_Node finite_imageI finite_in_P)
+ have prtr: "prodOf tr = tns" apply(rule Inl_Inr_image_cong)
+ unfolding ctr apply simp apply simp apply safe
+ using 0 unfolding image_def apply force apply simp by (metis 0 vimageI2)
+ have 1: "{K n' |n'. Inr n' \<in> tns} = {Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns}"
+ using 0 by auto
+ have dtr: "wf tr" apply(rule wf.dtree)
+ apply (metis (lifting) P prtr rtr)
+ unfolding inj_on_def ctr using 0 by auto
+ hence dtr': "wf tr'" unfolding tr'_def by (metis wf_hsubst)
+ have tns: "finite tns" using finite_in_P P by simp
+ have "Inl -` tns \<union> \<Union>{Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns} \<in> L ns n"
+ unfolding L_def mem_Collect_eq apply(intro exI[of _ tr'] conjI)
+ using dtr' 0 hsubst_aux[OF assms tns, of ftr] unfolding tr_def tr'_def by auto
+ thus "Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns} \<in> L ns n" unfolding 1 .
+qed
+
+lemma card_N: "(n::N) \<in> ns \<Longrightarrow> card (ns - {n}) < card ns"
+by (metis finite_N Diff_UNIV Diff_infinite_finite card_Diff1_less finite.emptyI)
+
+function LL where
+"LL ns n =
+ (if n \<notin> ns then {{}} else
+ {Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
+ (n,tns) \<in> P \<and>
+ (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> LL (ns - {n}) n')})"
+by(pat_completeness, auto)
+termination apply(relation "inv_image (measure card) fst")
+using card_N by auto
+
+declare LL.simps[code]
+declare LL.simps[simp del]
+
+lemma Lr_LL: "Lr ns n \<subseteq> LL ns n"
+proof (induct ns arbitrary: n rule: measure_induct[of card])
+ case (1 ns n) show ?case proof(cases "n \<in> ns")
+ case False thus ?thesis unfolding Lr_rec_notin[OF False] by (simp add: LL.simps)
+ next
+ case True show ?thesis apply(rule subset_trans)
+ using Lr_rec_in[OF True] apply assumption
+ unfolding LL.simps[of ns n] using True 1 card_N proof clarsimp
+ fix tns K
+ assume "n \<in> ns" hence c: "card (ns - {n}) < card ns" using card_N by blast
+ assume "(n, tns) \<in> P"
+ and "\<forall>n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> Lr (ns - {n}) n'"
+ thus "\<exists>tnsa Ka.
+ Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns} =
+ Inl -` tnsa \<union> \<Union>{Ka n' |n'. Inr n' \<in> tnsa} \<and>
+ (n, tnsa) \<in> P \<and> (\<forall>n'. Inr n' \<in> tnsa \<longrightarrow> Ka n' \<in> LL (ns - {n}) n')"
+ apply(intro exI[of _ tns] exI[of _ K]) using c 1 by auto
+ qed
+ qed
+qed
+
+lemma LL_L: "LL ns n \<subseteq> L ns n"
+proof (induct ns arbitrary: n rule: measure_induct[of card])
+ case (1 ns n) show ?case proof(cases "n \<in> ns")
+ case False thus ?thesis unfolding L_rec_notin[OF False] by (simp add: LL.simps)
+ next
+ case True show ?thesis apply(rule subset_trans)
+ prefer 2 using L_rec_in[OF True] apply assumption
+ unfolding LL.simps[of ns n] using True 1 card_N proof clarsimp
+ fix tns K
+ assume "n \<in> ns" hence c: "card (ns - {n}) < card ns" using card_N by blast
+ assume "(n, tns) \<in> P"
+ and "\<forall>n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> LL (ns - {n}) n'"
+ thus "\<exists>tnsa Ka.
+ Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns} =
+ Inl -` tnsa \<union> \<Union>{Ka n' |n'. Inr n' \<in> tnsa} \<and>
+ (n, tnsa) \<in> P \<and> (\<forall>n'. Inr n' \<in> tnsa \<longrightarrow> Ka n' \<in> L (ns - {n}) n')"
+ apply(intro exI[of _ tns] exI[of _ K]) using c 1 by auto
+ qed
+ qed
+qed
+
+(* The subsumpsion relation between languages *)
+definition "subs L1 L2 \<equiv> \<forall> ts2 \<in> L2. \<exists> ts1 \<in> L1. ts1 \<subseteq> ts2"
+
+lemma incl_subs[simp]: "L2 \<subseteq> L1 \<Longrightarrow> subs L1 L2"
+unfolding subs_def by auto
+
+lemma subs_refl[simp]: "subs L1 L1" unfolding subs_def by auto
+
+lemma subs_trans: "\<lbrakk>subs L1 L2; subs L2 L3\<rbrakk> \<Longrightarrow> subs L1 L3"
+unfolding subs_def by (metis subset_trans)
+
+(* Language equivalence *)
+definition "leqv L1 L2 \<equiv> subs L1 L2 \<and> subs L2 L1"
+
+lemma subs_leqv[simp]: "leqv L1 L2 \<Longrightarrow> subs L1 L2"
+unfolding leqv_def by auto
+
+lemma subs_leqv_sym[simp]: "leqv L1 L2 \<Longrightarrow> subs L2 L1"
+unfolding leqv_def by auto
+
+lemma leqv_refl[simp]: "leqv L1 L1" unfolding leqv_def by auto
+
+lemma leqv_trans:
+assumes 12: "leqv L1 L2" and 23: "leqv L2 L3"
+shows "leqv L1 L3"
+using assms unfolding leqv_def by (metis (lifting) subs_trans)
+
+lemma leqv_sym: "leqv L1 L2 \<Longrightarrow> leqv L2 L1"
+unfolding leqv_def by auto
+
+lemma leqv_Sym: "leqv L1 L2 \<longleftrightarrow> leqv L2 L1"
+unfolding leqv_def by auto
+
+lemma Lr_incl_L: "Lr ns ts \<subseteq> L ns ts"
+unfolding Lr_def L_def by auto
+
+lemma Lr_subs_L: "subs (Lr UNIV ts) (L UNIV ts)"
+unfolding subs_def proof safe
+ fix ts2 assume "ts2 \<in> L UNIV ts"
+ then obtain tr where ts2: "ts2 = Fr UNIV tr" and dtr: "wf tr" and rtr: "root tr = ts"
+ unfolding L_def by auto
+ thus "\<exists>ts1\<in>Lr UNIV ts. ts1 \<subseteq> ts2"
+ apply(intro bexI[of _ "Fr UNIV (rcut tr)"])
+ unfolding Lr_def L_def using Fr_rcut wf_rcut root_rcut regular_rcut by auto
+qed
+
+lemma Lr_leqv_L: "leqv (Lr UNIV ts) (L UNIV ts)"
+using Lr_subs_L unfolding leqv_def by (metis (lifting) Lr_incl_L incl_subs)
+
+lemma LL_leqv_L: "leqv (LL UNIV ts) (L UNIV ts)"
+by (metis (lifting) LL_L Lr_LL Lr_subs_L incl_subs leqv_def subs_trans)
+
+lemma LL_leqv_Lr: "leqv (LL UNIV ts) (Lr UNIV ts)"
+using Lr_leqv_L LL_leqv_L by (metis leqv_Sym leqv_trans)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Parallel.thy Tue Oct 16 22:38:34 2012 +0200
@@ -0,0 +1,148 @@
+(* Title: HOL/BNF/Examples/Derivation_Trees/Parallel.thy
+ Author: Andrei Popescu, TU Muenchen
+ Copyright 2012
+
+Parallel composition.
+*)
+
+header {* Parallel Composition *}
+
+theory Parallel
+imports DTree
+begin
+
+no_notation plus_class.plus (infixl "+" 65)
+no_notation Sublist.parallel (infixl "\<parallel>" 50)
+
+consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60)
+
+axiomatization where
+ Nplus_comm: "(a::N) + b = b + (a::N)"
+and Nplus_assoc: "((a::N) + b) + c = a + (b + c)"
+
+subsection{* Corecursive Definition of Parallel Composition *}
+
+fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2"
+fun par_c where
+"par_c (tr1,tr2) =
+ Inl ` (Inl -` (cont tr1 \<union> cont tr2)) \<union>
+ Inr ` (Inr -` cont tr1 \<times> Inr -` cont tr2)"
+
+declare par_r.simps[simp del] declare par_c.simps[simp del]
+
+definition par :: "dtree \<times> dtree \<Rightarrow> dtree" where
+"par \<equiv> unfold par_r par_c"
+
+abbreviation par_abbr (infixr "\<parallel>" 80) where "tr1 \<parallel> tr2 \<equiv> par (tr1, tr2)"
+
+lemma finite_par_c: "finite (par_c (tr1, tr2))"
+unfolding par_c.simps apply(rule finite_UnI)
+ apply (metis finite_Un finite_cont finite_imageI finite_vimageI inj_Inl)
+ apply(intro finite_imageI finite_cartesian_product finite_vimageI)
+ using finite_cont by auto
+
+lemma root_par: "root (tr1 \<parallel> tr2) = root tr1 + root tr2"
+using unfold(1)[of par_r par_c "(tr1,tr2)"] unfolding par_def par_r.simps by simp
+
+lemma cont_par:
+"cont (tr1 \<parallel> tr2) = (id \<oplus> par) ` par_c (tr1,tr2)"
+using unfold(2)[of par_c "(tr1,tr2)" par_r, OF finite_par_c]
+unfolding par_def ..
+
+lemma Inl_cont_par[simp]:
+"Inl -` (cont (tr1 \<parallel> tr2)) = Inl -` (cont tr1 \<union> cont tr2)"
+unfolding cont_par par_c.simps by auto
+
+lemma Inr_cont_par[simp]:
+"Inr -` (cont (tr1 \<parallel> tr2)) = par ` (Inr -` cont tr1 \<times> Inr -` cont tr2)"
+unfolding cont_par par_c.simps by auto
+
+lemma Inl_in_cont_par:
+"Inl t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (Inl t \<in> cont tr1 \<or> Inl t \<in> cont tr2)"
+using Inl_cont_par[of tr1 tr2] unfolding vimage_def by auto
+
+lemma Inr_in_cont_par:
+"Inr t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (t \<in> par ` (Inr -` cont tr1 \<times> Inr -` cont tr2))"
+using Inr_cont_par[of tr1 tr2] unfolding vimage_def by auto
+
+
+subsection{* Structural Coinduction Proofs *}
+
+lemma set_rel_sum_rel_eq[simp]:
+"set_rel (sum_rel (op =) \<phi>) A1 A2 \<longleftrightarrow>
+ Inl -` A1 = Inl -` A2 \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
+unfolding set_rel_sum_rel set_rel_eq ..
+
+(* Detailed proofs of commutativity and associativity: *)
+theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1"
+proof-
+ let ?\<theta> = "\<lambda> trA trB. \<exists> tr1 tr2. trA = tr1 \<parallel> tr2 \<and> trB = tr2 \<parallel> tr1"
+ {fix trA trB
+ assume "?\<theta> trA trB" hence "trA = trB"
+ apply (induct rule: dtree_coinduct)
+ unfolding set_rel_sum_rel set_rel_eq unfolding set_rel_def proof safe
+ fix tr1 tr2 show "root (tr1 \<parallel> tr2) = root (tr2 \<parallel> tr1)"
+ unfolding root_par by (rule Nplus_comm)
+ next
+ fix n tr1 tr2 assume "Inl n \<in> cont (tr1 \<parallel> tr2)" thus "n \<in> Inl -` (cont (tr2 \<parallel> tr1))"
+ unfolding Inl_in_cont_par by auto
+ next
+ fix n tr1 tr2 assume "Inl n \<in> cont (tr2 \<parallel> tr1)" thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2))"
+ unfolding Inl_in_cont_par by auto
+ next
+ fix tr1 tr2 trA' assume "Inr trA' \<in> cont (tr1 \<parallel> tr2)"
+ then obtain tr1' tr2' where "trA' = tr1' \<parallel> tr2'"
+ and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
+ unfolding Inr_in_cont_par by auto
+ thus "\<exists> trB' \<in> Inr -` (cont (tr2 \<parallel> tr1)). ?\<theta> trA' trB'"
+ apply(intro bexI[of _ "tr2' \<parallel> tr1'"]) unfolding Inr_in_cont_par by auto
+ next
+ fix tr1 tr2 trB' assume "Inr trB' \<in> cont (tr2 \<parallel> tr1)"
+ then obtain tr1' tr2' where "trB' = tr2' \<parallel> tr1'"
+ and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
+ unfolding Inr_in_cont_par by auto
+ thus "\<exists> trA' \<in> Inr -` (cont (tr1 \<parallel> tr2)). ?\<theta> trA' trB'"
+ apply(intro bexI[of _ "tr1' \<parallel> tr2'"]) unfolding Inr_in_cont_par by auto
+ qed
+ }
+ thus ?thesis by blast
+qed
+
+lemma par_assoc: "(tr1 \<parallel> tr2) \<parallel> tr3 = tr1 \<parallel> (tr2 \<parallel> tr3)"
+proof-
+ let ?\<theta> =
+ "\<lambda> trA trB. \<exists> tr1 tr2 tr3. trA = (tr1 \<parallel> tr2) \<parallel> tr3 \<and> trB = tr1 \<parallel> (tr2 \<parallel> tr3)"
+ {fix trA trB
+ assume "?\<theta> trA trB" hence "trA = trB"
+ apply (induct rule: dtree_coinduct)
+ unfolding set_rel_sum_rel set_rel_eq unfolding set_rel_def proof safe
+ fix tr1 tr2 tr3 show "root ((tr1 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))"
+ unfolding root_par by (rule Nplus_assoc)
+ next
+ fix n tr1 tr2 tr3 assume "Inl n \<in> (cont ((tr1 \<parallel> tr2) \<parallel> tr3))"
+ thus "n \<in> Inl -` (cont (tr1 \<parallel> tr2 \<parallel> tr3))" unfolding Inl_in_cont_par by simp
+ next
+ fix n tr1 tr2 tr3 assume "Inl n \<in> (cont (tr1 \<parallel> tr2 \<parallel> tr3))"
+ thus "n \<in> Inl -` (cont ((tr1 \<parallel> tr2) \<parallel> tr3))" unfolding Inl_in_cont_par by simp
+ next
+ fix trA' tr1 tr2 tr3 assume "Inr trA' \<in> cont ((tr1 \<parallel> tr2) \<parallel> tr3)"
+ then obtain tr1' tr2' tr3' where "trA' = (tr1' \<parallel> tr2') \<parallel> tr3'"
+ and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
+ and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto
+ thus "\<exists> trB' \<in> Inr -` (cont (tr1 \<parallel> tr2 \<parallel> tr3)). ?\<theta> trA' trB'"
+ apply(intro bexI[of _ "tr1' \<parallel> tr2' \<parallel> tr3'"])
+ unfolding Inr_in_cont_par by auto
+ next
+ fix trB' tr1 tr2 tr3 assume "Inr trB' \<in> cont (tr1 \<parallel> tr2 \<parallel> tr3)"
+ then obtain tr1' tr2' tr3' where "trB' = tr1' \<parallel> (tr2' \<parallel> tr3')"
+ and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
+ and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto
+ thus "\<exists> trA' \<in> Inr -` cont ((tr1 \<parallel> tr2) \<parallel> tr3). ?\<theta> trA' trB'"
+ apply(intro bexI[of _ "(tr1' \<parallel> tr2') \<parallel> tr3'"])
+ unfolding Inr_in_cont_par by auto
+ qed
+ }
+ thus ?thesis by blast
+qed
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Prelim.thy Tue Oct 16 22:38:34 2012 +0200
@@ -0,0 +1,65 @@
+(* Title: HOL/BNF/Examples/Derivation_Trees/Prelim.thy
+ Author: Andrei Popescu, TU Muenchen
+ Copyright 2012
+
+Preliminaries.
+*)
+
+header {* Preliminaries *}
+
+theory Prelim
+imports "../../BNF" "../../More_BNFs"
+begin
+
+declare fset_to_fset[simp]
+
+lemma fst_snd_convol_o[simp]: "<fst o s, snd o s> = s"
+apply(rule ext) by (simp add: convol_def)
+
+abbreviation sm_abbrev (infix "\<oplus>" 60)
+where "f \<oplus> g \<equiv> Sum_Type.sum_map f g"
+
+lemma sum_map_InlD: "(f \<oplus> g) z = Inl x \<Longrightarrow> \<exists>y. z = Inl y \<and> f y = x"
+by (cases z) auto
+
+lemma sum_map_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
+by (cases z) auto
+
+abbreviation sum_case_abbrev ("[[_,_]]" 800)
+where "[[f,g]] \<equiv> Sum_Type.sum_case f g"
+
+lemma inj_Inl[simp]: "inj Inl" unfolding inj_on_def by auto
+lemma inj_Inr[simp]: "inj Inr" unfolding inj_on_def by auto
+
+lemma Inl_oplus_elim:
+assumes "Inl tr \<in> (id \<oplus> f) ` tns"
+shows "Inl tr \<in> tns"
+using assms apply clarify by (case_tac x, auto)
+
+lemma Inl_oplus_iff[simp]: "Inl tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> Inl tr \<in> tns"
+using Inl_oplus_elim
+by (metis id_def image_iff sum_map.simps(1))
+
+lemma Inl_m_oplus[simp]: "Inl -` (id \<oplus> f) ` tns = Inl -` tns"
+using Inl_oplus_iff unfolding vimage_def by auto
+
+lemma Inr_oplus_elim:
+assumes "Inr tr \<in> (id \<oplus> f) ` tns"
+shows "\<exists> n. Inr n \<in> tns \<and> f n = tr"
+using assms apply clarify by (case_tac x, auto)
+
+lemma Inr_oplus_iff[simp]:
+"Inr tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> (\<exists> n. Inr n \<in> tns \<and> f n = tr)"
+apply (rule iffI)
+ apply (metis Inr_oplus_elim)
+by (metis image_iff sum_map.simps(2))
+
+lemma Inr_m_oplus[simp]: "Inr -` (id \<oplus> f) ` tns = f ` (Inr -` tns)"
+using Inr_oplus_iff unfolding vimage_def by auto
+
+lemma Inl_Inr_image_cong:
+assumes "Inl -` A = Inl -` B" and "Inr -` A = Inr -` B"
+shows "A = B"
+apply safe using assms apply(case_tac x, auto) by(case_tac x, auto)
+
+end
\ No newline at end of file
--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Gram_Lang.thy Tue Oct 16 22:13:46 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1374 +0,0 @@
-(* Title: HOL/BNF/Examples/Infinite_Derivation_Trees/Gram_Lang.thy
- Author: Andrei Popescu, TU Muenchen
- Copyright 2012
-
-Language of a grammar.
-*)
-
-header {* Language of a Grammar *}
-
-theory Gram_Lang
-imports Tree
-begin
-
-
-consts P :: "(N \<times> (T + N) set) set"
-axiomatization where
- finite_N: "finite (UNIV::N set)"
-and finite_in_P: "\<And> n tns. (n,tns) \<in> P \<longrightarrow> finite tns"
-and used: "\<And> n. \<exists> tns. (n,tns) \<in> P"
-
-
-subsection{* Tree basics: frontier, interior, etc. *}
-
-lemma Tree_cong:
-assumes "root tr = root tr'" and "cont tr = cont tr'"
-shows "tr = tr'"
-by (metis Node_root_cont assms)
-
-inductive finiteT where
-Node: "\<lbrakk>finite as; (finiteT^#) as\<rbrakk> \<Longrightarrow> finiteT (Node a as)"
-monos lift_mono
-
-lemma finiteT_induct[consumes 1, case_names Node, induct pred: finiteT]:
-assumes 1: "finiteT tr"
-and IH: "\<And>as n. \<lbrakk>finite as; (\<phi>^#) as\<rbrakk> \<Longrightarrow> \<phi> (Node n as)"
-shows "\<phi> tr"
-using 1 apply(induct rule: finiteT.induct)
-apply(rule IH) apply assumption apply(elim mono_lift) by simp
-
-
-(* Frontier *)
-
-inductive inFr :: "N set \<Rightarrow> Tree \<Rightarrow> T \<Rightarrow> bool" where
-Base: "\<lbrakk>root tr \<in> ns; Inl t \<in> cont tr\<rbrakk> \<Longrightarrow> inFr ns tr t"
-|
-Ind: "\<lbrakk>root tr \<in> ns; Inr tr1 \<in> cont tr; inFr ns tr1 t\<rbrakk> \<Longrightarrow> inFr ns tr t"
-
-definition "Fr ns tr \<equiv> {t. inFr ns tr t}"
-
-lemma inFr_root_in: "inFr ns tr t \<Longrightarrow> root tr \<in> ns"
-by (metis inFr.simps)
-
-lemma inFr_mono:
-assumes "inFr ns tr t" and "ns \<subseteq> ns'"
-shows "inFr ns' tr t"
-using assms apply(induct arbitrary: ns' rule: inFr.induct)
-using Base Ind by (metis inFr.simps set_mp)+
-
-lemma inFr_Ind_minus:
-assumes "inFr ns1 tr1 t" and "Inr tr1 \<in> cont tr"
-shows "inFr (insert (root tr) ns1) tr t"
-using assms apply(induct rule: inFr.induct)
- apply (metis inFr.simps insert_iff)
- by (metis inFr.simps inFr_mono insertI1 subset_insertI)
-
-(* alternative definition *)
-inductive inFr2 :: "N set \<Rightarrow> Tree \<Rightarrow> T \<Rightarrow> bool" where
-Base: "\<lbrakk>root tr \<in> ns; Inl t \<in> cont tr\<rbrakk> \<Longrightarrow> inFr2 ns tr t"
-|
-Ind: "\<lbrakk>Inr tr1 \<in> cont tr; inFr2 ns1 tr1 t\<rbrakk>
- \<Longrightarrow> inFr2 (insert (root tr) ns1) tr t"
-
-lemma inFr2_root_in: "inFr2 ns tr t \<Longrightarrow> root tr \<in> ns"
-apply(induct rule: inFr2.induct) by auto
-
-lemma inFr2_mono:
-assumes "inFr2 ns tr t" and "ns \<subseteq> ns'"
-shows "inFr2 ns' tr t"
-using assms apply(induct arbitrary: ns' rule: inFr2.induct)
-using Base Ind
-apply (metis subsetD) by (metis inFr2.simps insert_absorb insert_subset)
-
-lemma inFr2_Ind:
-assumes "inFr2 ns tr1 t" and "root tr \<in> ns" and "Inr tr1 \<in> cont tr"
-shows "inFr2 ns tr t"
-using assms apply(induct rule: inFr2.induct)
- apply (metis inFr2.simps insert_absorb)
- by (metis inFr2.simps insert_absorb)
-
-lemma inFr_inFr2:
-"inFr = inFr2"
-apply (rule ext)+ apply(safe)
- apply(erule inFr.induct)
- apply (metis (lifting) inFr2.Base)
- apply (metis (lifting) inFr2_Ind)
- apply(erule inFr2.induct)
- apply (metis (lifting) inFr.Base)
- apply (metis (lifting) inFr_Ind_minus)
-done
-
-lemma not_root_inFr:
-assumes "root tr \<notin> ns"
-shows "\<not> inFr ns tr t"
-by (metis assms inFr_root_in)
-
-theorem not_root_Fr:
-assumes "root tr \<notin> ns"
-shows "Fr ns tr = {}"
-using not_root_inFr[OF assms] unfolding Fr_def by auto
-
-
-(* Interior *)
-
-inductive inItr :: "N set \<Rightarrow> Tree \<Rightarrow> N \<Rightarrow> bool" where
-Base: "root tr \<in> ns \<Longrightarrow> inItr ns tr (root tr)"
-|
-Ind: "\<lbrakk>root tr \<in> ns; Inr tr1 \<in> cont tr; inItr ns tr1 n\<rbrakk> \<Longrightarrow> inItr ns tr n"
-
-definition "Itr ns tr \<equiv> {n. inItr ns tr n}"
-
-lemma inItr_root_in: "inItr ns tr n \<Longrightarrow> root tr \<in> ns"
-by (metis inItr.simps)
-
-lemma inItr_mono:
-assumes "inItr ns tr n" and "ns \<subseteq> ns'"
-shows "inItr ns' tr n"
-using assms apply(induct arbitrary: ns' rule: inItr.induct)
-using Base Ind by (metis inItr.simps set_mp)+
-
-
-(* The subtree relation *)
-
-inductive subtr where
-Refl: "root tr \<in> ns \<Longrightarrow> subtr ns tr tr"
-|
-Step: "\<lbrakk>root tr3 \<in> ns; subtr ns tr1 tr2; Inr tr2 \<in> cont tr3\<rbrakk> \<Longrightarrow> subtr ns tr1 tr3"
-
-lemma subtr_rootL_in:
-assumes "subtr ns tr1 tr2"
-shows "root tr1 \<in> ns"
-using assms apply(induct rule: subtr.induct) by auto
-
-lemma subtr_rootR_in:
-assumes "subtr ns tr1 tr2"
-shows "root tr2 \<in> ns"
-using assms apply(induct rule: subtr.induct) by auto
-
-lemmas subtr_roots_in = subtr_rootL_in subtr_rootR_in
-
-lemma subtr_mono:
-assumes "subtr ns tr1 tr2" and "ns \<subseteq> ns'"
-shows "subtr ns' tr1 tr2"
-using assms apply(induct arbitrary: ns' rule: subtr.induct)
-using Refl Step by (metis subtr.simps set_mp)+
-
-lemma subtr_trans_Un:
-assumes "subtr ns12 tr1 tr2" and "subtr ns23 tr2 tr3"
-shows "subtr (ns12 \<union> ns23) tr1 tr3"
-proof-
- have "subtr ns23 tr2 tr3 \<Longrightarrow>
- (\<forall> ns12 tr1. subtr ns12 tr1 tr2 \<longrightarrow> subtr (ns12 \<union> ns23) tr1 tr3)"
- apply(induct rule: subtr.induct, safe)
- apply (metis subtr_mono sup_commute sup_ge2)
- by (metis (lifting) Step UnI2)
- thus ?thesis using assms by auto
-qed
-
-lemma subtr_trans:
-assumes "subtr ns tr1 tr2" and "subtr ns tr2 tr3"
-shows "subtr ns tr1 tr3"
-using subtr_trans_Un[OF assms] by simp
-
-lemma subtr_StepL:
-assumes r: "root tr1 \<in> ns" and tr12: "Inr tr1 \<in> cont tr2" and s: "subtr ns tr2 tr3"
-shows "subtr ns tr1 tr3"
-apply(rule subtr_trans[OF _ s])
-apply(rule Step[of tr2 ns tr1 tr1])
-apply(rule subtr_rootL_in[OF s])
-apply(rule Refl[OF r])
-apply(rule tr12)
-done
-
-(* alternative definition: *)
-inductive subtr2 where
-Refl: "root tr \<in> ns \<Longrightarrow> subtr2 ns tr tr"
-|
-Step: "\<lbrakk>root tr1 \<in> ns; Inr tr1 \<in> cont tr2; subtr2 ns tr2 tr3\<rbrakk> \<Longrightarrow> subtr2 ns tr1 tr3"
-
-lemma subtr2_rootL_in:
-assumes "subtr2 ns tr1 tr2"
-shows "root tr1 \<in> ns"
-using assms apply(induct rule: subtr2.induct) by auto
-
-lemma subtr2_rootR_in:
-assumes "subtr2 ns tr1 tr2"
-shows "root tr2 \<in> ns"
-using assms apply(induct rule: subtr2.induct) by auto
-
-lemmas subtr2_roots_in = subtr2_rootL_in subtr2_rootR_in
-
-lemma subtr2_mono:
-assumes "subtr2 ns tr1 tr2" and "ns \<subseteq> ns'"
-shows "subtr2 ns' tr1 tr2"
-using assms apply(induct arbitrary: ns' rule: subtr2.induct)
-using Refl Step by (metis subtr2.simps set_mp)+
-
-lemma subtr2_trans_Un:
-assumes "subtr2 ns12 tr1 tr2" and "subtr2 ns23 tr2 tr3"
-shows "subtr2 (ns12 \<union> ns23) tr1 tr3"
-proof-
- have "subtr2 ns12 tr1 tr2 \<Longrightarrow>
- (\<forall> ns23 tr3. subtr2 ns23 tr2 tr3 \<longrightarrow> subtr2 (ns12 \<union> ns23) tr1 tr3)"
- apply(induct rule: subtr2.induct, safe)
- apply (metis subtr2_mono sup_commute sup_ge2)
- by (metis Un_iff subtr2.simps)
- thus ?thesis using assms by auto
-qed
-
-lemma subtr2_trans:
-assumes "subtr2 ns tr1 tr2" and "subtr2 ns tr2 tr3"
-shows "subtr2 ns tr1 tr3"
-using subtr2_trans_Un[OF assms] by simp
-
-lemma subtr2_StepR:
-assumes r: "root tr3 \<in> ns" and tr23: "Inr tr2 \<in> cont tr3" and s: "subtr2 ns tr1 tr2"
-shows "subtr2 ns tr1 tr3"
-apply(rule subtr2_trans[OF s])
-apply(rule Step[of _ _ tr3])
-apply(rule subtr2_rootR_in[OF s])
-apply(rule tr23)
-apply(rule Refl[OF r])
-done
-
-lemma subtr_subtr2:
-"subtr = subtr2"
-apply (rule ext)+ apply(safe)
- apply(erule subtr.induct)
- apply (metis (lifting) subtr2.Refl)
- apply (metis (lifting) subtr2_StepR)
- apply(erule subtr2.induct)
- apply (metis (lifting) subtr.Refl)
- apply (metis (lifting) subtr_StepL)
-done
-
-lemma subtr_inductL[consumes 1, case_names Refl Step]:
-assumes s: "subtr ns tr1 tr2" and Refl: "\<And>ns tr. \<phi> ns tr tr"
-and Step:
-"\<And>ns tr1 tr2 tr3.
- \<lbrakk>root tr1 \<in> ns; Inr tr1 \<in> cont tr2; subtr ns tr2 tr3; \<phi> ns tr2 tr3\<rbrakk> \<Longrightarrow> \<phi> ns tr1 tr3"
-shows "\<phi> ns tr1 tr2"
-using s unfolding subtr_subtr2 apply(rule subtr2.induct)
-using Refl Step unfolding subtr_subtr2 by auto
-
-lemma subtr_UNIV_inductL[consumes 1, case_names Refl Step]:
-assumes s: "subtr UNIV tr1 tr2" and Refl: "\<And>tr. \<phi> tr tr"
-and Step:
-"\<And>tr1 tr2 tr3.
- \<lbrakk>Inr tr1 \<in> cont tr2; subtr UNIV tr2 tr3; \<phi> tr2 tr3\<rbrakk> \<Longrightarrow> \<phi> tr1 tr3"
-shows "\<phi> tr1 tr2"
-using s apply(induct rule: subtr_inductL)
-apply(rule Refl) using Step subtr_mono by (metis subset_UNIV)
-
-(* Subtree versus frontier: *)
-lemma subtr_inFr:
-assumes "inFr ns tr t" and "subtr ns tr tr1"
-shows "inFr ns tr1 t"
-proof-
- have "subtr ns tr tr1 \<Longrightarrow> (\<forall> t. inFr ns tr t \<longrightarrow> inFr ns tr1 t)"
- apply(induct rule: subtr.induct, safe) by (metis inFr.Ind)
- thus ?thesis using assms by auto
-qed
-
-corollary Fr_subtr:
-"Fr ns tr = \<Union> {Fr ns tr' | tr'. subtr ns tr' tr}"
-unfolding Fr_def proof safe
- fix t assume t: "inFr ns tr t" hence "root tr \<in> ns" by (rule inFr_root_in)
- thus "t \<in> \<Union>{{t. inFr ns tr' t} |tr'. subtr ns tr' tr}"
- apply(intro UnionI[of "{t. inFr ns tr t}" _ t]) using t subtr.Refl by auto
-qed(metis subtr_inFr)
-
-lemma inFr_subtr:
-assumes "inFr ns tr t"
-shows "\<exists> tr'. subtr ns tr' tr \<and> Inl t \<in> cont tr'"
-using assms apply(induct rule: inFr.induct) apply safe
- apply (metis subtr.Refl)
- by (metis (lifting) subtr.Step)
-
-corollary Fr_subtr_cont:
-"Fr ns tr = \<Union> {Inl -` cont tr' | tr'. subtr ns tr' tr}"
-unfolding Fr_def
-apply safe
-apply (frule inFr_subtr)
-apply auto
-by (metis inFr.Base subtr_inFr subtr_rootL_in)
-
-(* Subtree versus interior: *)
-lemma subtr_inItr:
-assumes "inItr ns tr n" and "subtr ns tr tr1"
-shows "inItr ns tr1 n"
-proof-
- have "subtr ns tr tr1 \<Longrightarrow> (\<forall> t. inItr ns tr n \<longrightarrow> inItr ns tr1 n)"
- apply(induct rule: subtr.induct, safe) by (metis inItr.Ind)
- thus ?thesis using assms by auto
-qed
-
-corollary Itr_subtr:
-"Itr ns tr = \<Union> {Itr ns tr' | tr'. subtr ns tr' tr}"
-unfolding Itr_def apply safe
-apply (metis (lifting, mono_tags) UnionI inItr_root_in mem_Collect_eq subtr.Refl)
-by (metis subtr_inItr)
-
-lemma inItr_subtr:
-assumes "inItr ns tr n"
-shows "\<exists> tr'. subtr ns tr' tr \<and> root tr' = n"
-using assms apply(induct rule: inItr.induct) apply safe
- apply (metis subtr.Refl)
- by (metis (lifting) subtr.Step)
-
-corollary Itr_subtr_cont:
-"Itr ns tr = {root tr' | tr'. subtr ns tr' tr}"
-unfolding Itr_def apply safe
- apply (metis (lifting, mono_tags) inItr_subtr)
- by (metis inItr.Base subtr_inItr subtr_rootL_in)
-
-
-subsection{* The immediate subtree function *}
-
-(* production of: *)
-abbreviation "prodOf tr \<equiv> (id \<oplus> root) ` (cont tr)"
-(* subtree of: *)
-definition "subtrOf tr n \<equiv> SOME tr'. Inr tr' \<in> cont tr \<and> root tr' = n"
-
-lemma subtrOf:
-assumes n: "Inr n \<in> prodOf tr"
-shows "Inr (subtrOf tr n) \<in> cont tr \<and> root (subtrOf tr n) = n"
-proof-
- obtain tr' where "Inr tr' \<in> cont tr \<and> root tr' = n"
- using n unfolding image_def by (metis (lifting) Inr_oplus_elim assms)
- thus ?thesis unfolding subtrOf_def by(rule someI)
-qed
-
-lemmas Inr_subtrOf = subtrOf[THEN conjunct1]
-lemmas root_subtrOf[simp] = subtrOf[THEN conjunct2]
-
-lemma Inl_prodOf: "Inl -` (prodOf tr) = Inl -` (cont tr)"
-proof safe
- fix t ttr assume "Inl t = (id \<oplus> root) ttr" and "ttr \<in> cont tr"
- thus "t \<in> Inl -` cont tr" by(cases ttr, auto)
-next
- fix t assume "Inl t \<in> cont tr" thus "t \<in> Inl -` prodOf tr"
- by (metis (lifting) id_def image_iff sum_map.simps(1) vimageI2)
-qed
-
-lemma root_prodOf:
-assumes "Inr tr' \<in> cont tr"
-shows "Inr (root tr') \<in> prodOf tr"
-by (metis (lifting) assms image_iff sum_map.simps(2))
-
-
-subsection{* Derivation trees *}
-
-coinductive dtree where
-Tree: "\<lbrakk>(root tr, (id \<oplus> root) ` (cont tr)) \<in> P; inj_on root (Inr -` cont tr);
- lift dtree (cont tr)\<rbrakk> \<Longrightarrow> dtree tr"
-monos lift_mono
-
-(* destruction rules: *)
-lemma dtree_P:
-assumes "dtree tr"
-shows "(root tr, (id \<oplus> root) ` (cont tr)) \<in> P"
-using assms unfolding dtree.simps by auto
-
-lemma dtree_inj_on:
-assumes "dtree tr"
-shows "inj_on root (Inr -` cont tr)"
-using assms unfolding dtree.simps by auto
-
-lemma dtree_inj[simp]:
-assumes "dtree tr" and "Inr tr1 \<in> cont tr" and "Inr tr2 \<in> cont tr"
-shows "root tr1 = root tr2 \<longleftrightarrow> tr1 = tr2"
-using assms dtree_inj_on unfolding inj_on_def by auto
-
-lemma dtree_lift:
-assumes "dtree tr"
-shows "lift dtree (cont tr)"
-using assms unfolding dtree.simps by auto
-
-
-(* coinduction:*)
-lemma dtree_coind[elim, consumes 1, case_names Hyp]:
-assumes phi: "\<phi> tr"
-and Hyp:
-"\<And> tr. \<phi> tr \<Longrightarrow>
- (root tr, image (id \<oplus> root) (cont tr)) \<in> P \<and>
- inj_on root (Inr -` cont tr) \<and>
- lift (\<lambda> tr. \<phi> tr \<or> dtree tr) (cont tr)"
-shows "dtree tr"
-apply(rule dtree.coinduct[of \<phi> tr, OF phi])
-using Hyp by blast
-
-lemma dtree_raw_coind[elim, consumes 1, case_names Hyp]:
-assumes phi: "\<phi> tr"
-and Hyp:
-"\<And> tr. \<phi> tr \<Longrightarrow>
- (root tr, image (id \<oplus> root) (cont tr)) \<in> P \<and>
- inj_on root (Inr -` cont tr) \<and>
- lift \<phi> (cont tr)"
-shows "dtree tr"
-using phi apply(induct rule: dtree_coind)
-using Hyp mono_lift
-by (metis (mono_tags) mono_lift)
-
-lemma dtree_subtr_inj_on:
-assumes d: "dtree tr1" and s: "subtr ns tr tr1"
-shows "inj_on root (Inr -` cont tr)"
-using s d apply(induct rule: subtr.induct)
-apply (metis (lifting) dtree_inj_on) by (metis dtree_lift lift_def)
-
-lemma dtree_subtr_P:
-assumes d: "dtree tr1" and s: "subtr ns tr tr1"
-shows "(root tr, (id \<oplus> root) ` cont tr) \<in> P"
-using s d apply(induct rule: subtr.induct)
-apply (metis (lifting) dtree_P) by (metis dtree_lift lift_def)
-
-lemma subtrOf_root[simp]:
-assumes tr: "dtree tr" and cont: "Inr tr' \<in> cont tr"
-shows "subtrOf tr (root tr') = tr'"
-proof-
- have 0: "Inr (subtrOf tr (root tr')) \<in> cont tr" using Inr_subtrOf
- by (metis (lifting) cont root_prodOf)
- have "root (subtrOf tr (root tr')) = root tr'"
- using root_subtrOf by (metis (lifting) cont root_prodOf)
- thus ?thesis unfolding dtree_inj[OF tr 0 cont] .
-qed
-
-lemma surj_subtrOf:
-assumes "dtree tr" and 0: "Inr tr' \<in> cont tr"
-shows "\<exists> n. Inr n \<in> prodOf tr \<and> subtrOf tr n = tr'"
-apply(rule exI[of _ "root tr'"])
-using root_prodOf[OF 0] subtrOf_root[OF assms] by simp
-
-lemma dtree_subtr:
-assumes "dtree tr1" and "subtr ns tr tr1"
-shows "dtree tr"
-proof-
- have "(\<exists> ns tr1. dtree tr1 \<and> subtr ns tr tr1) \<Longrightarrow> dtree tr"
- proof (induct rule: dtree_raw_coind)
- case (Hyp tr)
- then obtain ns tr1 where tr1: "dtree tr1" and tr_tr1: "subtr ns tr tr1" by auto
- show ?case unfolding lift_def proof safe
- show "(root tr, (id \<oplus> root) ` cont tr) \<in> P" using dtree_subtr_P[OF tr1 tr_tr1] .
- next
- show "inj_on root (Inr -` cont tr)" using dtree_subtr_inj_on[OF tr1 tr_tr1] .
- next
- fix tr' assume tr': "Inr tr' \<in> cont tr"
- have tr_tr1: "subtr (ns \<union> {root tr'}) tr tr1" using subtr_mono[OF tr_tr1] by auto
- have "subtr (ns \<union> {root tr'}) tr' tr1" using subtr_StepL[OF _ tr' tr_tr1] by auto
- thus "\<exists>ns' tr1. dtree tr1 \<and> subtr ns' tr' tr1" using tr1 by blast
- qed
- qed
- thus ?thesis using assms by auto
-qed
-
-
-subsection{* Default trees *}
-
-(* Pick a left-hand side of a production for each nonterminal *)
-definition S where "S n \<equiv> SOME tns. (n,tns) \<in> P"
-
-lemma S_P: "(n, S n) \<in> P"
-using used unfolding S_def by(rule someI_ex)
-
-lemma finite_S: "finite (S n)"
-using S_P finite_in_P by auto
-
-
-(* The default tree of a nonterminal *)
-definition deftr :: "N \<Rightarrow> Tree" where
-"deftr \<equiv> unfold id S"
-
-lemma deftr_simps[simp]:
-"root (deftr n) = n"
-"cont (deftr n) = image (id \<oplus> deftr) (S n)"
-using unfold(1)[of id S n] unfold(2)[of S n id, OF finite_S]
-unfolding deftr_def by simp_all
-
-lemmas root_deftr = deftr_simps(1)
-lemmas cont_deftr = deftr_simps(2)
-
-lemma root_o_deftr[simp]: "root o deftr = id"
-by (rule ext, auto)
-
-lemma dtree_deftr: "dtree (deftr n)"
-proof-
- {fix tr assume "\<exists> n. tr = deftr n" hence "dtree tr"
- apply(induct rule: dtree_raw_coind) apply safe
- unfolding deftr_simps image_compose[symmetric] sum_map.comp id_o
- root_o_deftr sum_map.id image_id id_apply apply(rule S_P)
- unfolding inj_on_def lift_def by auto
- }
- thus ?thesis by auto
-qed
-
-
-subsection{* Hereditary substitution *}
-
-(* Auxiliary concept: The root-ommiting frontier: *)
-definition "inFrr ns tr t \<equiv> \<exists> tr'. Inr tr' \<in> cont tr \<and> inFr ns tr' t"
-definition "Frr ns tr \<equiv> {t. \<exists> tr'. Inr tr' \<in> cont tr \<and> t \<in> Fr ns tr'}"
-
-context
-fixes tr0 :: Tree
-begin
-
-definition "hsubst_r tr \<equiv> root tr"
-definition "hsubst_c tr \<equiv> if root tr = root tr0 then cont tr0 else cont tr"
-
-(* Hereditary substitution: *)
-definition hsubst :: "Tree \<Rightarrow> Tree" where
-"hsubst \<equiv> unfold hsubst_r hsubst_c"
-
-lemma finite_hsubst_c: "finite (hsubst_c n)"
-unfolding hsubst_c_def by (metis (full_types) finite_cont)
-
-lemma root_hsubst[simp]: "root (hsubst tr) = root tr"
-using unfold(1)[of hsubst_r hsubst_c tr] unfolding hsubst_def hsubst_r_def by simp
-
-lemma root_o_subst[simp]: "root o hsubst = root"
-unfolding comp_def root_hsubst ..
-
-lemma cont_hsubst_eq[simp]:
-assumes "root tr = root tr0"
-shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr0)"
-apply(subst id_o[symmetric, of id]) unfolding id_o
-using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
-unfolding hsubst_def hsubst_c_def using assms by simp
-
-lemma hsubst_eq:
-assumes "root tr = root tr0"
-shows "hsubst tr = hsubst tr0"
-apply(rule Tree_cong) using assms cont_hsubst_eq by auto
-
-lemma cont_hsubst_neq[simp]:
-assumes "root tr \<noteq> root tr0"
-shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr)"
-apply(subst id_o[symmetric, of id]) unfolding id_o
-using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
-unfolding hsubst_def hsubst_c_def using assms by simp
-
-lemma Inl_cont_hsubst_eq[simp]:
-assumes "root tr = root tr0"
-shows "Inl -` cont (hsubst tr) = Inl -` (cont tr0)"
-unfolding cont_hsubst_eq[OF assms] by simp
-
-lemma Inr_cont_hsubst_eq[simp]:
-assumes "root tr = root tr0"
-shows "Inr -` cont (hsubst tr) = hsubst ` Inr -` cont tr0"
-unfolding cont_hsubst_eq[OF assms] by simp
-
-lemma Inl_cont_hsubst_neq[simp]:
-assumes "root tr \<noteq> root tr0"
-shows "Inl -` cont (hsubst tr) = Inl -` (cont tr)"
-unfolding cont_hsubst_neq[OF assms] by simp
-
-lemma Inr_cont_hsubst_neq[simp]:
-assumes "root tr \<noteq> root tr0"
-shows "Inr -` cont (hsubst tr) = hsubst ` Inr -` cont tr"
-unfolding cont_hsubst_neq[OF assms] by simp
-
-lemma dtree_hsubst:
-assumes tr0: "dtree tr0" and tr: "dtree tr"
-shows "dtree (hsubst tr)"
-proof-
- {fix tr1 have "(\<exists> tr. dtree tr \<and> tr1 = hsubst tr) \<Longrightarrow> dtree tr1"
- proof (induct rule: dtree_raw_coind)
- case (Hyp tr1) then obtain tr
- where dtr: "dtree tr" and tr1: "tr1 = hsubst tr" by auto
- show ?case unfolding lift_def tr1 proof safe
- show "(root (hsubst tr), prodOf (hsubst tr)) \<in> P"
- unfolding tr1 apply(cases "root tr = root tr0")
- using dtree_P[OF dtr] dtree_P[OF tr0]
- by (auto simp add: image_compose[symmetric] sum_map.comp)
- show "inj_on root (Inr -` cont (hsubst tr))"
- apply(cases "root tr = root tr0") using dtree_inj_on[OF dtr] dtree_inj_on[OF tr0]
- unfolding inj_on_def by (auto, blast)
- fix tr' assume "Inr tr' \<in> cont (hsubst tr)"
- thus "\<exists>tra. dtree tra \<and> tr' = hsubst tra"
- apply(cases "root tr = root tr0", simp_all)
- apply (metis dtree_lift lift_def tr0)
- by (metis dtr dtree_lift lift_def)
- qed
- qed
- }
- thus ?thesis using assms by blast
-qed
-
-lemma Frr: "Frr ns tr = {t. inFrr ns tr t}"
-unfolding inFrr_def Frr_def Fr_def by auto
-
-lemma inFr_hsubst_imp:
-assumes "inFr ns (hsubst tr) t"
-shows "t \<in> Inl -` (cont tr0) \<or> inFrr (ns - {root tr0}) tr0 t \<or>
- inFr (ns - {root tr0}) tr t"
-proof-
- {fix tr1
- have "inFr ns tr1 t \<Longrightarrow>
- (\<And> tr. tr1 = hsubst tr \<Longrightarrow> (t \<in> Inl -` (cont tr0) \<or> inFrr (ns - {root tr0}) tr0 t \<or>
- inFr (ns - {root tr0}) tr t))"
- proof(induct rule: inFr.induct)
- case (Base tr1 ns t tr)
- hence rtr: "root tr1 \<in> ns" and t_tr1: "Inl t \<in> cont tr1" and tr1: "tr1 = hsubst tr"
- by auto
- show ?case
- proof(cases "root tr1 = root tr0")
- case True
- hence "t \<in> Inl -` (cont tr0)" using t_tr1 unfolding tr1 by auto
- thus ?thesis by simp
- next
- case False
- hence "inFr (ns - {root tr0}) tr t" using t_tr1 unfolding tr1 apply simp
- by (metis Base.prems Diff_iff root_hsubst inFr.Base rtr singletonE)
- thus ?thesis by simp
- qed
- next
- case (Ind tr1 ns tr1' t) note IH = Ind(4)
- have rtr1: "root tr1 \<in> ns" and tr1'_tr1: "Inr tr1' \<in> cont tr1"
- and t_tr1': "inFr ns tr1' t" and tr1: "tr1 = hsubst tr" using Ind by auto
- have rtr1: "root tr1 = root tr" unfolding tr1 by simp
- show ?case
- proof(cases "root tr1 = root tr0")
- case True
- then obtain tr' where tr'_tr0: "Inr tr' \<in> cont tr0" and tr1': "tr1' = hsubst tr'"
- using tr1'_tr1 unfolding tr1 by auto
- show ?thesis using IH[OF tr1'] proof (elim disjE)
- assume "inFr (ns - {root tr0}) tr' t"
- thus ?thesis using tr'_tr0 unfolding inFrr_def by auto
- qed auto
- next
- case False
- then obtain tr' where tr'_tr: "Inr tr' \<in> cont tr" and tr1': "tr1' = hsubst tr'"
- using tr1'_tr1 unfolding tr1 by auto
- show ?thesis using IH[OF tr1'] proof (elim disjE)
- assume "inFr (ns - {root tr0}) tr' t"
- thus ?thesis using tr'_tr unfolding inFrr_def
- by (metis Diff_iff False Ind(1) empty_iff inFr2_Ind inFr_inFr2 insert_iff rtr1)
- qed auto
- qed
- qed
- }
- thus ?thesis using assms by auto
-qed
-
-lemma inFr_hsubst_notin:
-assumes "inFr ns tr t" and "root tr0 \<notin> ns"
-shows "inFr ns (hsubst tr) t"
-using assms apply(induct rule: inFr.induct)
-apply (metis Inl_cont_hsubst_neq inFr2.Base inFr_inFr2 root_hsubst vimageD vimageI2)
-by (metis (lifting) Inr_cont_hsubst_neq inFr.Ind rev_image_eqI root_hsubst vimageD vimageI2)
-
-lemma inFr_hsubst_minus:
-assumes "inFr (ns - {root tr0}) tr t"
-shows "inFr ns (hsubst tr) t"
-proof-
- have 1: "inFr (ns - {root tr0}) (hsubst tr) t"
- using inFr_hsubst_notin[OF assms] by simp
- show ?thesis using inFr_mono[OF 1] by auto
-qed
-
-lemma inFr_self_hsubst:
-assumes "root tr0 \<in> ns"
-shows
-"inFr ns (hsubst tr0) t \<longleftrightarrow>
- t \<in> Inl -` (cont tr0) \<or> inFrr (ns - {root tr0}) tr0 t"
-(is "?A \<longleftrightarrow> ?B \<or> ?C")
-apply(intro iffI)
-apply (metis inFr_hsubst_imp Diff_iff inFr_root_in insertI1) proof(elim disjE)
- assume ?B thus ?A apply(intro inFr.Base) using assms by auto
-next
- assume ?C then obtain tr where
- tr_tr0: "Inr tr \<in> cont tr0" and t_tr: "inFr (ns - {root tr0}) tr t"
- unfolding inFrr_def by auto
- def tr1 \<equiv> "hsubst tr"
- have 1: "inFr ns tr1 t" using t_tr unfolding tr1_def using inFr_hsubst_minus by auto
- have "Inr tr1 \<in> cont (hsubst tr0)" unfolding tr1_def using tr_tr0 by auto
- thus ?A using 1 inFr.Ind assms by (metis root_hsubst)
-qed
-
-theorem Fr_self_hsubst:
-assumes "root tr0 \<in> ns"
-shows "Fr ns (hsubst tr0) = Inl -` (cont tr0) \<union> Frr (ns - {root tr0}) tr0"
-using inFr_self_hsubst[OF assms] unfolding Frr Fr_def by auto
-
-end (* context *)
-
-
-subsection{* Regular trees *}
-
-hide_const regular
-
-definition "reg f tr \<equiv> \<forall> tr'. subtr UNIV tr' tr \<longrightarrow> tr' = f (root tr')"
-definition "regular tr \<equiv> \<exists> f. reg f tr"
-
-lemma reg_def2: "reg f tr \<longleftrightarrow> (\<forall> ns tr'. subtr ns tr' tr \<longrightarrow> tr' = f (root tr'))"
-unfolding reg_def using subtr_mono by (metis subset_UNIV)
-
-lemma regular_def2: "regular tr \<longleftrightarrow> (\<exists> f. reg f tr \<and> (\<forall> n. root (f n) = n))"
-unfolding regular_def proof safe
- fix f assume f: "reg f tr"
- def g \<equiv> "\<lambda> n. if inItr UNIV tr n then f n else deftr n"
- show "\<exists>g. reg g tr \<and> (\<forall>n. root (g n) = n)"
- apply(rule exI[of _ g])
- using f deftr_simps(1) unfolding g_def reg_def apply safe
- apply (metis (lifting) inItr.Base subtr_inItr subtr_rootL_in)
- by (metis (full_types) inItr_subtr)
-qed auto
-
-lemma reg_root:
-assumes "reg f tr"
-shows "f (root tr) = tr"
-using assms unfolding reg_def
-by (metis (lifting) iso_tuple_UNIV_I subtr.Refl)
-
-
-lemma reg_Inr_cont:
-assumes "reg f tr" and "Inr tr' \<in> cont tr"
-shows "reg f tr'"
-by (metis (lifting) assms iso_tuple_UNIV_I reg_def subtr.Step)
-
-lemma reg_subtr:
-assumes "reg f tr" and "subtr ns tr' tr"
-shows "reg f tr'"
-using assms unfolding reg_def using subtr_trans[of UNIV tr] UNIV_I
-by (metis UNIV_eq_I UnCI Un_upper1 iso_tuple_UNIV_I subtr_mono subtr_trans)
-
-lemma regular_subtr:
-assumes r: "regular tr" and s: "subtr ns tr' tr"
-shows "regular tr'"
-using r reg_subtr[OF _ s] unfolding regular_def by auto
-
-lemma subtr_deftr:
-assumes "subtr ns tr' (deftr n)"
-shows "tr' = deftr (root tr')"
-proof-
- {fix tr have "subtr ns tr' tr \<Longrightarrow> (\<forall> n. tr = deftr n \<longrightarrow> tr' = deftr (root tr'))"
- apply (induct rule: subtr.induct)
- proof(metis (lifting) deftr_simps(1), safe)
- fix tr3 ns tr1 tr2 n
- assume 1: "root (deftr n) \<in> ns" and 2: "subtr ns tr1 tr2"
- and IH: "\<forall>n. tr2 = deftr n \<longrightarrow> tr1 = deftr (root tr1)"
- and 3: "Inr tr2 \<in> cont (deftr n)"
- have "tr2 \<in> deftr ` UNIV"
- using 3 unfolding deftr_simps image_def
- by (metis (lifting, full_types) 3 CollectI Inr_oplus_iff cont_deftr
- iso_tuple_UNIV_I)
- then obtain n where "tr2 = deftr n" by auto
- thus "tr1 = deftr (root tr1)" using IH by auto
- qed
- }
- thus ?thesis using assms by auto
-qed
-
-lemma reg_deftr: "reg deftr (deftr n)"
-unfolding reg_def using subtr_deftr by auto
-
-lemma dtree_subtrOf_Union:
-assumes "dtree tr"
-shows "\<Union>{K tr' |tr'. Inr tr' \<in> cont tr} =
- \<Union>{K (subtrOf tr n) |n. Inr n \<in> prodOf tr}"
-unfolding Union_eq Bex_def mem_Collect_eq proof safe
- fix x xa tr'
- assume x: "x \<in> K tr'" and tr'_tr: "Inr tr' \<in> cont tr"
- show "\<exists>X. (\<exists>n. X = K (subtrOf tr n) \<and> Inr n \<in> prodOf tr) \<and> x \<in> X"
- apply(rule exI[of _ "K (subtrOf tr (root tr'))"]) apply(intro conjI)
- apply(rule exI[of _ "root tr'"]) apply (metis (lifting) root_prodOf tr'_tr)
- by (metis (lifting) assms subtrOf_root tr'_tr x)
-next
- fix x X n ttr
- assume x: "x \<in> K (subtrOf tr n)" and n: "Inr n = (id \<oplus> root) ttr" and ttr: "ttr \<in> cont tr"
- show "\<exists>X. (\<exists>tr'. X = K tr' \<and> Inr tr' \<in> cont tr) \<and> x \<in> X"
- apply(rule exI[of _ "K (subtrOf tr n)"]) apply(intro conjI)
- apply(rule exI[of _ "subtrOf tr n"]) apply (metis imageI n subtrOf ttr)
- using x .
-qed
-
-
-
-
-subsection {* Paths in a regular tree *}
-
-inductive path :: "(N \<Rightarrow> Tree) \<Rightarrow> N list \<Rightarrow> bool" for f where
-Base: "path f [n]"
-|
-Ind: "\<lbrakk>path f (n1 # nl); Inr (f n1) \<in> cont (f n)\<rbrakk>
- \<Longrightarrow> path f (n # n1 # nl)"
-
-lemma path_NE:
-assumes "path f nl"
-shows "nl \<noteq> Nil"
-using assms apply(induct rule: path.induct) by auto
-
-lemma path_post:
-assumes f: "path f (n # nl)" and nl: "nl \<noteq> []"
-shows "path f nl"
-proof-
- obtain n1 nl1 where nl: "nl = n1 # nl1" using nl by (cases nl, auto)
- show ?thesis using assms unfolding nl using path.simps by (metis (lifting) list.inject)
-qed
-
-lemma path_post_concat:
-assumes "path f (nl1 @ nl2)" and "nl2 \<noteq> Nil"
-shows "path f nl2"
-using assms apply (induct nl1)
-apply (metis append_Nil) by (metis Nil_is_append_conv append_Cons path_post)
-
-lemma path_concat:
-assumes "path f nl1" and "path f ((last nl1) # nl2)"
-shows "path f (nl1 @ nl2)"
-using assms apply(induct rule: path.induct) apply simp
-by (metis append_Cons last.simps list.simps(3) path.Ind)
-
-lemma path_distinct:
-assumes "path f nl"
-shows "\<exists> nl'. path f nl' \<and> hd nl' = hd nl \<and> last nl' = last nl \<and>
- set nl' \<subseteq> set nl \<and> distinct nl'"
-using assms proof(induct rule: length_induct)
- case (1 nl) hence p_nl: "path f nl" by simp
- then obtain n nl1 where nl: "nl = n # nl1" by (metis list.exhaust path_NE)
- show ?case
- proof(cases nl1)
- case Nil
- show ?thesis apply(rule exI[of _ nl]) using path.Base unfolding nl Nil by simp
- next
- case (Cons n1 nl2)
- hence p1: "path f nl1" by (metis list.simps(3) nl p_nl path_post)
- show ?thesis
- proof(cases "n \<in> set nl1")
- case False
- obtain nl1' where p1': "path f nl1'" and hd_nl1': "hd nl1' = hd nl1" and
- l_nl1': "last nl1' = last nl1" and d_nl1': "distinct nl1'"
- and s_nl1': "set nl1' \<subseteq> set nl1"
- using 1(1)[THEN allE[of _ nl1]] p1 unfolding nl by auto
- obtain nl2' where nl1': "nl1' = n1 # nl2'" using path_NE[OF p1'] hd_nl1'
- unfolding Cons by(cases nl1', auto)
- show ?thesis apply(intro exI[of _ "n # nl1'"]) unfolding nl proof safe
- show "path f (n # nl1')" unfolding nl1'
- apply(rule path.Ind, metis nl1' p1')
- by (metis (lifting) Cons list.inject nl p1 p_nl path.simps path_NE)
- qed(insert l_nl1' Cons nl1' s_nl1' d_nl1' False, auto)
- next
- case True
- then obtain nl11 nl12 where nl1: "nl1 = nl11 @ n # nl12"
- by (metis split_list)
- have p12: "path f (n # nl12)"
- apply(rule path_post_concat[of _ "n # nl11"]) using p_nl[unfolded nl nl1] by auto
- obtain nl12' where p1': "path f nl12'" and hd_nl12': "hd nl12' = n" and
- l_nl12': "last nl12' = last (n # nl12)" and d_nl12': "distinct nl12'"
- and s_nl12': "set nl12' \<subseteq> {n} \<union> set nl12"
- using 1(1)[THEN allE[of _ "n # nl12"]] p12 unfolding nl nl1 by auto
- thus ?thesis apply(intro exI[of _ nl12']) unfolding nl nl1 by auto
- qed
- qed
-qed
-
-lemma path_subtr:
-assumes f: "\<And> n. root (f n) = n"
-and p: "path f nl"
-shows "subtr (set nl) (f (last nl)) (f (hd nl))"
-using p proof (induct rule: path.induct)
- case (Ind n1 nl n) let ?ns1 = "insert n1 (set nl)"
- have "path f (n1 # nl)"
- and "subtr ?ns1 (f (last (n1 # nl))) (f n1)"
- and fn1: "Inr (f n1) \<in> cont (f n)" using Ind by simp_all
- hence fn1_flast: "subtr (insert n ?ns1) (f (last (n1 # nl))) (f n1)"
- by (metis subset_insertI subtr_mono)
- have 1: "last (n # n1 # nl) = last (n1 # nl)" by auto
- have "subtr (insert n ?ns1) (f (last (n1 # nl))) (f n)"
- using f subtr.Step[OF _ fn1_flast fn1] by auto
- thus ?case unfolding 1 by simp
-qed (metis f hd.simps last_ConsL last_in_set not_Cons_self2 subtr.Refl)
-
-lemma reg_subtr_path_aux:
-assumes f: "reg f tr" and n: "subtr ns tr1 tr"
-shows "\<exists> nl. path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and> set nl \<subseteq> ns"
-using n f proof(induct rule: subtr.induct)
- case (Refl tr ns)
- thus ?case
- apply(intro exI[of _ "[root tr]"]) apply simp by (metis (lifting) path.Base reg_root)
-next
- case (Step tr ns tr2 tr1)
- hence rtr: "root tr \<in> ns" and tr1_tr: "Inr tr1 \<in> cont tr"
- and tr2_tr1: "subtr ns tr2 tr1" and tr: "reg f tr" by auto
- have tr1: "reg f tr1" using reg_subtr[OF tr] rtr tr1_tr
- by (metis (lifting) Step.prems iso_tuple_UNIV_I reg_def subtr.Step)
- obtain nl where nl: "path f nl" and f_nl: "f (hd nl) = tr1"
- and last_nl: "f (last nl) = tr2" and set: "set nl \<subseteq> ns" using Step(3)[OF tr1] by auto
- have 0: "path f (root tr # nl)" apply (subst path.simps)
- using f_nl nl reg_root tr tr1_tr by (metis hd.simps neq_Nil_conv)
- show ?case apply(rule exI[of _ "(root tr) # nl"])
- using 0 reg_root tr last_nl nl path_NE rtr set by auto
-qed
-
-lemma reg_subtr_path:
-assumes f: "reg f tr" and n: "subtr ns tr1 tr"
-shows "\<exists> nl. distinct nl \<and> path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and> set nl \<subseteq> ns"
-using reg_subtr_path_aux[OF assms] path_distinct[of f]
-by (metis (lifting) order_trans)
-
-lemma subtr_iff_path:
-assumes r: "reg f tr" and f: "\<And> n. root (f n) = n"
-shows "subtr ns tr1 tr \<longleftrightarrow>
- (\<exists> nl. distinct nl \<and> path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and> set nl \<subseteq> ns)"
-proof safe
- fix nl assume p: "path f nl" and nl: "set nl \<subseteq> ns"
- have "subtr (set nl) (f (last nl)) (f (hd nl))"
- apply(rule path_subtr) using p f by simp_all
- thus "subtr ns (f (last nl)) (f (hd nl))"
- using subtr_mono nl by auto
-qed(insert reg_subtr_path[OF r], auto)
-
-lemma inFr_iff_path:
-assumes r: "reg f tr" and f: "\<And> n. root (f n) = n"
-shows
-"inFr ns tr t \<longleftrightarrow>
- (\<exists> nl tr1. distinct nl \<and> path f nl \<and> f (hd nl) = tr \<and> f (last nl) = tr1 \<and>
- set nl \<subseteq> ns \<and> Inl t \<in> cont tr1)"
-apply safe
-apply (metis (no_types) inFr_subtr r reg_subtr_path)
-by (metis f inFr.Base path_subtr subtr_inFr subtr_mono subtr_rootL_in)
-
-
-
-subsection{* The regular cut of a tree *}
-
-context fixes tr0 :: Tree
-begin
-
-(* Picking a subtree of a certain root: *)
-definition "pick n \<equiv> SOME tr. subtr UNIV tr tr0 \<and> root tr = n"
-
-lemma pick:
-assumes "inItr UNIV tr0 n"
-shows "subtr UNIV (pick n) tr0 \<and> root (pick n) = n"
-proof-
- have "\<exists> tr. subtr UNIV tr tr0 \<and> root tr = n"
- using assms by (metis (lifting) inItr_subtr)
- thus ?thesis unfolding pick_def by(rule someI_ex)
-qed
-
-lemmas subtr_pick = pick[THEN conjunct1]
-lemmas root_pick = pick[THEN conjunct2]
-
-lemma dtree_pick:
-assumes tr0: "dtree tr0" and n: "inItr UNIV tr0 n"
-shows "dtree (pick n)"
-using dtree_subtr[OF tr0 subtr_pick[OF n]] .
-
-definition "regOf_r n \<equiv> root (pick n)"
-definition "regOf_c n \<equiv> (id \<oplus> root) ` cont (pick n)"
-
-(* The regular tree of a function: *)
-definition regOf :: "N \<Rightarrow> Tree" where
-"regOf \<equiv> unfold regOf_r regOf_c"
-
-lemma finite_regOf_c: "finite (regOf_c n)"
-unfolding regOf_c_def by (metis finite_cont finite_imageI)
-
-lemma root_regOf_pick: "root (regOf n) = root (pick n)"
-using unfold(1)[of regOf_r regOf_c n] unfolding regOf_def regOf_r_def by simp
-
-lemma root_regOf[simp]:
-assumes "inItr UNIV tr0 n"
-shows "root (regOf n) = n"
-unfolding root_regOf_pick root_pick[OF assms] ..
-
-lemma cont_regOf[simp]:
-"cont (regOf n) = (id \<oplus> (regOf o root)) ` cont (pick n)"
-apply(subst id_o[symmetric, of id]) unfolding sum_map.comp[symmetric]
-unfolding image_compose unfolding regOf_c_def[symmetric]
-using unfold(2)[of regOf_c n regOf_r, OF finite_regOf_c]
-unfolding regOf_def ..
-
-lemma Inl_cont_regOf[simp]:
-"Inl -` (cont (regOf n)) = Inl -` (cont (pick n))"
-unfolding cont_regOf by simp
-
-lemma Inr_cont_regOf:
-"Inr -` (cont (regOf n)) = (regOf \<circ> root) ` (Inr -` cont (pick n))"
-unfolding cont_regOf by simp
-
-lemma subtr_regOf:
-assumes n: "inItr UNIV tr0 n" and "subtr UNIV tr1 (regOf n)"
-shows "\<exists> n1. inItr UNIV tr0 n1 \<and> tr1 = regOf n1"
-proof-
- {fix tr ns assume "subtr UNIV tr1 tr"
- hence "tr = regOf n \<longrightarrow> (\<exists> n1. inItr UNIV tr0 n1 \<and> tr1 = regOf n1)"
- proof (induct rule: subtr_UNIV_inductL)
- case (Step tr2 tr1 tr)
- show ?case proof
- assume "tr = regOf n"
- then obtain n1 where tr2: "Inr tr2 \<in> cont tr1"
- and tr1_tr: "subtr UNIV tr1 tr" and n1: "inItr UNIV tr0 n1" and tr1: "tr1 = regOf n1"
- using Step by auto
- obtain tr2' where tr2: "tr2 = regOf (root tr2')"
- and tr2': "Inr tr2' \<in> cont (pick n1)"
- using tr2 Inr_cont_regOf[of n1]
- unfolding tr1 image_def o_def using vimage_eq by auto
- have "inItr UNIV tr0 (root tr2')"
- using inItr.Base inItr.Ind n1 pick subtr_inItr tr2' by (metis iso_tuple_UNIV_I)
- thus "\<exists>n2. inItr UNIV tr0 n2 \<and> tr2 = regOf n2" using tr2 by blast
- qed
- qed(insert n, auto)
- }
- thus ?thesis using assms by auto
-qed
-
-lemma root_regOf_root:
-assumes n: "inItr UNIV tr0 n" and t_tr: "t_tr \<in> cont (pick n)"
-shows "(id \<oplus> (root \<circ> regOf \<circ> root)) t_tr = (id \<oplus> root) t_tr"
-using assms apply(cases t_tr)
- apply (metis (lifting) sum_map.simps(1))
- using pick regOf_def regOf_r_def unfold(1)
- inItr.Base o_apply subtr_StepL subtr_inItr sum_map.simps(2)
- by (metis UNIV_I)
-
-lemma regOf_P:
-assumes tr0: "dtree tr0" and n: "inItr UNIV tr0 n"
-shows "(n, (id \<oplus> root) ` cont (regOf n)) \<in> P" (is "?L \<in> P")
-proof-
- have "?L = (n, (id \<oplus> root) ` cont (pick n))"
- unfolding cont_regOf image_compose[symmetric] sum_map.comp id_o o_assoc
- unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
- by(rule root_regOf_root[OF n])
- moreover have "... \<in> P" by (metis (lifting) dtree_pick root_pick dtree_P n tr0)
- ultimately show ?thesis by simp
-qed
-
-lemma dtree_regOf:
-assumes tr0: "dtree tr0" and "inItr UNIV tr0 n"
-shows "dtree (regOf n)"
-proof-
- {fix tr have "\<exists> n. inItr UNIV tr0 n \<and> tr = regOf n \<Longrightarrow> dtree tr"
- proof (induct rule: dtree_raw_coind)
- case (Hyp tr)
- then obtain n where n: "inItr UNIV tr0 n" and tr: "tr = regOf n" by auto
- show ?case unfolding lift_def apply safe
- apply (metis (lifting) regOf_P root_regOf n tr tr0)
- unfolding tr Inr_cont_regOf unfolding inj_on_def apply clarsimp using root_regOf
- apply (metis UNIV_I inItr.Base n pick subtr2.simps subtr_inItr subtr_subtr2)
- by (metis n subtr.Refl subtr_StepL subtr_regOf tr UNIV_I)
- qed
- }
- thus ?thesis using assms by blast
-qed
-
-(* The regular cut of a tree: *)
-definition "rcut \<equiv> regOf (root tr0)"
-
-theorem reg_rcut: "reg regOf rcut"
-unfolding reg_def rcut_def
-by (metis inItr.Base root_regOf subtr_regOf UNIV_I)
-
-lemma rcut_reg:
-assumes "reg regOf tr0"
-shows "rcut = tr0"
-using assms unfolding rcut_def reg_def by (metis subtr.Refl UNIV_I)
-
-theorem rcut_eq: "rcut = tr0 \<longleftrightarrow> reg regOf tr0"
-using reg_rcut rcut_reg by metis
-
-theorem regular_rcut: "regular rcut"
-using reg_rcut unfolding regular_def by blast
-
-theorem Fr_rcut: "Fr UNIV rcut \<subseteq> Fr UNIV tr0"
-proof safe
- fix t assume "t \<in> Fr UNIV rcut"
- then obtain tr where t: "Inl t \<in> cont tr" and tr: "subtr UNIV tr (regOf (root tr0))"
- using Fr_subtr[of UNIV "regOf (root tr0)"] unfolding rcut_def
- by (metis (full_types) Fr_def inFr_subtr mem_Collect_eq)
- obtain n where n: "inItr UNIV tr0 n" and tr: "tr = regOf n" using tr
- by (metis (lifting) inItr.Base subtr_regOf UNIV_I)
- have "Inl t \<in> cont (pick n)" using t using Inl_cont_regOf[of n] unfolding tr
- by (metis (lifting) vimageD vimageI2)
- moreover have "subtr UNIV (pick n) tr0" using subtr_pick[OF n] ..
- ultimately show "t \<in> Fr UNIV tr0" unfolding Fr_subtr_cont by auto
-qed
-
-theorem dtree_rcut:
-assumes "dtree tr0"
-shows "dtree rcut"
-unfolding rcut_def using dtree_regOf[OF assms inItr.Base] by simp
-
-theorem root_rcut[simp]: "root rcut = root tr0"
-unfolding rcut_def
-by (metis (lifting) root_regOf inItr.Base reg_def reg_root subtr_rootR_in)
-
-end (* context *)
-
-
-subsection{* Recursive description of the regular tree frontiers *}
-
-lemma regular_inFr:
-assumes r: "regular tr" and In: "root tr \<in> ns"
-and t: "inFr ns tr t"
-shows "t \<in> Inl -` (cont tr) \<or>
- (\<exists> tr'. Inr tr' \<in> cont tr \<and> inFr (ns - {root tr}) tr' t)"
-(is "?L \<or> ?R")
-proof-
- obtain f where r: "reg f tr" and f: "\<And>n. root (f n) = n"
- using r unfolding regular_def2 by auto
- obtain nl tr1 where d_nl: "distinct nl" and p: "path f nl" and hd_nl: "f (hd nl) = tr"
- and l_nl: "f (last nl) = tr1" and s_nl: "set nl \<subseteq> ns" and t_tr1: "Inl t \<in> cont tr1"
- using t unfolding inFr_iff_path[OF r f] by auto
- obtain n nl1 where nl: "nl = n # nl1" by (metis (lifting) p path.simps)
- hence f_n: "f n = tr" using hd_nl by simp
- have n_nl1: "n \<notin> set nl1" using d_nl unfolding nl by auto
- show ?thesis
- proof(cases nl1)
- case Nil hence "tr = tr1" using f_n l_nl unfolding nl by simp
- hence ?L using t_tr1 by simp thus ?thesis by simp
- next
- case (Cons n1 nl2) note nl1 = Cons
- have 1: "last nl1 = last nl" "hd nl1 = n1" unfolding nl nl1 by simp_all
- have p1: "path f nl1" and n1_tr: "Inr (f n1) \<in> cont tr"
- using path.simps[of f nl] p f_n unfolding nl nl1 by auto
- have r1: "reg f (f n1)" using reg_Inr_cont[OF r n1_tr] .
- have 0: "inFr (set nl1) (f n1) t" unfolding inFr_iff_path[OF r1 f]
- apply(intro exI[of _ nl1], intro exI[of _ tr1])
- using d_nl unfolding 1 l_nl unfolding nl using p1 t_tr1 by auto
- have root_tr: "root tr = n" by (metis f f_n)
- have "inFr (ns - {root tr}) (f n1) t" apply(rule inFr_mono[OF 0])
- using s_nl unfolding root_tr unfolding nl using n_nl1 by auto
- thus ?thesis using n1_tr by auto
- qed
-qed
-
-theorem regular_Fr:
-assumes r: "regular tr" and In: "root tr \<in> ns"
-shows "Fr ns tr =
- Inl -` (cont tr) \<union>
- \<Union> {Fr (ns - {root tr}) tr' | tr'. Inr tr' \<in> cont tr}"
-unfolding Fr_def
-using In inFr.Base regular_inFr[OF assms] apply safe
-apply (simp, metis (full_types) mem_Collect_eq)
-apply simp
-by (simp, metis (lifting) inFr_Ind_minus insert_Diff)
-
-
-subsection{* The generated languages *}
-
-(* The (possibly inifinite tree) generated language *)
-definition "L ns n \<equiv> {Fr ns tr | tr. dtree tr \<and> root tr = n}"
-
-(* The regular-tree generated language *)
-definition "Lr ns n \<equiv> {Fr ns tr | tr. dtree tr \<and> root tr = n \<and> regular tr}"
-
-theorem L_rec_notin:
-assumes "n \<notin> ns"
-shows "L ns n = {{}}"
-using assms unfolding L_def apply safe
- using not_root_Fr apply force
- apply(rule exI[of _ "deftr n"])
- by (metis (no_types) dtree_deftr not_root_Fr root_deftr)
-
-theorem Lr_rec_notin:
-assumes "n \<notin> ns"
-shows "Lr ns n = {{}}"
-using assms unfolding Lr_def apply safe
- using not_root_Fr apply force
- apply(rule exI[of _ "deftr n"])
- by (metis (no_types) regular_def dtree_deftr not_root_Fr reg_deftr root_deftr)
-
-lemma dtree_subtrOf:
-assumes "dtree tr" and "Inr n \<in> prodOf tr"
-shows "dtree (subtrOf tr n)"
-by (metis assms dtree_lift lift_def subtrOf)
-
-theorem Lr_rec_in:
-assumes n: "n \<in> ns"
-shows "Lr ns n \<subseteq>
-{Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
- (n,tns) \<in> P \<and>
- (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> Lr (ns - {n}) n')}"
-(is "Lr ns n \<subseteq> {?F tns K | tns K. (n,tns) \<in> P \<and> ?\<phi> tns K}")
-proof safe
- fix ts assume "ts \<in> Lr ns n"
- then obtain tr where dtr: "dtree tr" and r: "root tr = n" and tr: "regular tr"
- and ts: "ts = Fr ns tr" unfolding Lr_def by auto
- def tns \<equiv> "(id \<oplus> root) ` (cont tr)"
- def K \<equiv> "\<lambda> n'. Fr (ns - {n}) (subtrOf tr n')"
- show "\<exists>tns K. ts = ?F tns K \<and> (n, tns) \<in> P \<and> ?\<phi> tns K"
- apply(rule exI[of _ tns], rule exI[of _ K]) proof(intro conjI allI impI)
- show "ts = Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns}"
- unfolding ts regular_Fr[OF tr n[unfolded r[symmetric]]]
- unfolding tns_def K_def r[symmetric]
- unfolding Inl_prodOf dtree_subtrOf_Union[OF dtr] ..
- show "(n, tns) \<in> P" unfolding tns_def r[symmetric] using dtree_P[OF dtr] .
- fix n' assume "Inr n' \<in> tns" thus "K n' \<in> Lr (ns - {n}) n'"
- unfolding K_def Lr_def mem_Collect_eq apply(intro exI[of _ "subtrOf tr n'"])
- using dtr tr apply(intro conjI refl) unfolding tns_def
- apply(erule dtree_subtrOf[OF dtr])
- apply (metis subtrOf)
- by (metis Inr_subtrOf UNIV_I regular_subtr subtr.simps)
- qed
-qed
-
-lemma hsubst_aux:
-fixes n ftr tns
-assumes n: "n \<in> ns" and tns: "finite tns" and
-1: "\<And> n'. Inr n' \<in> tns \<Longrightarrow> dtree (ftr n')"
-defines "tr \<equiv> Node n ((id \<oplus> ftr) ` tns)" defines "tr' \<equiv> hsubst tr tr"
-shows "Fr ns tr' = Inl -` tns \<union> \<Union>{Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns}"
-(is "_ = ?B") proof-
- have rtr: "root tr = n" and ctr: "cont tr = (id \<oplus> ftr) ` tns"
- unfolding tr_def using tns by auto
- have Frr: "Frr (ns - {n}) tr = \<Union>{Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns}"
- unfolding Frr_def ctr by auto
- have "Fr ns tr' = Inl -` (cont tr) \<union> Frr (ns - {n}) tr"
- using Fr_self_hsubst[OF n[unfolded rtr[symmetric]]] unfolding tr'_def rtr ..
- also have "... = ?B" unfolding ctr Frr by simp
- finally show ?thesis .
-qed
-
-theorem L_rec_in:
-assumes n: "n \<in> ns"
-shows "
-{Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
- (n,tns) \<in> P \<and>
- (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> L (ns - {n}) n')}
- \<subseteq> L ns n"
-proof safe
- fix tns K
- assume P: "(n, tns) \<in> P" and 0: "\<forall>n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> L (ns - {n}) n'"
- {fix n' assume "Inr n' \<in> tns"
- hence "K n' \<in> L (ns - {n}) n'" using 0 by auto
- hence "\<exists> tr'. K n' = Fr (ns - {n}) tr' \<and> dtree tr' \<and> root tr' = n'"
- unfolding L_def mem_Collect_eq by auto
- }
- then obtain ftr where 0: "\<And> n'. Inr n' \<in> tns \<Longrightarrow>
- K n' = Fr (ns - {n}) (ftr n') \<and> dtree (ftr n') \<and> root (ftr n') = n'"
- by metis
- def tr \<equiv> "Node n ((id \<oplus> ftr) ` tns)" def tr' \<equiv> "hsubst tr tr"
- have rtr: "root tr = n" and ctr: "cont tr = (id \<oplus> ftr) ` tns"
- unfolding tr_def by (simp, metis P cont_Node finite_imageI finite_in_P)
- have prtr: "prodOf tr = tns" apply(rule Inl_Inr_image_cong)
- unfolding ctr apply simp apply simp apply safe
- using 0 unfolding image_def apply force apply simp by (metis 0 vimageI2)
- have 1: "{K n' |n'. Inr n' \<in> tns} = {Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns}"
- using 0 by auto
- have dtr: "dtree tr" apply(rule dtree.Tree)
- apply (metis (lifting) P prtr rtr)
- unfolding inj_on_def ctr lift_def using 0 by auto
- hence dtr': "dtree tr'" unfolding tr'_def by (metis dtree_hsubst)
- have tns: "finite tns" using finite_in_P P by simp
- have "Inl -` tns \<union> \<Union>{Fr (ns - {n}) (ftr n') |n'. Inr n' \<in> tns} \<in> L ns n"
- unfolding L_def mem_Collect_eq apply(intro exI[of _ tr'] conjI)
- using dtr' 0 hsubst_aux[OF assms tns, of ftr] unfolding tr_def tr'_def by auto
- thus "Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns} \<in> L ns n" unfolding 1 .
-qed
-
-lemma card_N: "(n::N) \<in> ns \<Longrightarrow> card (ns - {n}) < card ns"
-by (metis finite_N Diff_UNIV Diff_infinite_finite card_Diff1_less finite.emptyI)
-
-function LL where
-"LL ns n =
- (if n \<notin> ns then {{}} else
- {Inl -` tns \<union> (\<Union> {K n' | n'. Inr n' \<in> tns}) | tns K.
- (n,tns) \<in> P \<and>
- (\<forall> n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> LL (ns - {n}) n')})"
-by(pat_completeness, auto)
-termination apply(relation "inv_image (measure card) fst")
-using card_N by auto
-
-declare LL.simps[code] (* TODO: Does code generation for LL work? *)
-declare LL.simps[simp del]
-
-theorem Lr_LL: "Lr ns n \<subseteq> LL ns n"
-proof (induct ns arbitrary: n rule: measure_induct[of card])
- case (1 ns n) show ?case proof(cases "n \<in> ns")
- case False thus ?thesis unfolding Lr_rec_notin[OF False] by (simp add: LL.simps)
- next
- case True show ?thesis apply(rule subset_trans)
- using Lr_rec_in[OF True] apply assumption
- unfolding LL.simps[of ns n] using True 1 card_N proof clarsimp
- fix tns K
- assume "n \<in> ns" hence c: "card (ns - {n}) < card ns" using card_N by blast
- assume "(n, tns) \<in> P"
- and "\<forall>n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> Lr (ns - {n}) n'"
- thus "\<exists>tnsa Ka.
- Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns} =
- Inl -` tnsa \<union> \<Union>{Ka n' |n'. Inr n' \<in> tnsa} \<and>
- (n, tnsa) \<in> P \<and> (\<forall>n'. Inr n' \<in> tnsa \<longrightarrow> Ka n' \<in> LL (ns - {n}) n')"
- apply(intro exI[of _ tns] exI[of _ K]) using c 1 by auto
- qed
- qed
-qed
-
-theorem LL_L: "LL ns n \<subseteq> L ns n"
-proof (induct ns arbitrary: n rule: measure_induct[of card])
- case (1 ns n) show ?case proof(cases "n \<in> ns")
- case False thus ?thesis unfolding L_rec_notin[OF False] by (simp add: LL.simps)
- next
- case True show ?thesis apply(rule subset_trans)
- prefer 2 using L_rec_in[OF True] apply assumption
- unfolding LL.simps[of ns n] using True 1 card_N proof clarsimp
- fix tns K
- assume "n \<in> ns" hence c: "card (ns - {n}) < card ns" using card_N by blast
- assume "(n, tns) \<in> P"
- and "\<forall>n'. Inr n' \<in> tns \<longrightarrow> K n' \<in> LL (ns - {n}) n'"
- thus "\<exists>tnsa Ka.
- Inl -` tns \<union> \<Union>{K n' |n'. Inr n' \<in> tns} =
- Inl -` tnsa \<union> \<Union>{Ka n' |n'. Inr n' \<in> tnsa} \<and>
- (n, tnsa) \<in> P \<and> (\<forall>n'. Inr n' \<in> tnsa \<longrightarrow> Ka n' \<in> L (ns - {n}) n')"
- apply(intro exI[of _ tns] exI[of _ K]) using c 1 by auto
- qed
- qed
-qed
-
-(* The subsumpsion relation between languages *)
-definition "subs L1 L2 \<equiv> \<forall> ts2 \<in> L2. \<exists> ts1 \<in> L1. ts1 \<subseteq> ts2"
-
-lemma incl_subs[simp]: "L2 \<subseteq> L1 \<Longrightarrow> subs L1 L2"
-unfolding subs_def by auto
-
-lemma subs_refl[simp]: "subs L1 L1" unfolding subs_def by auto
-
-lemma subs_trans: "\<lbrakk>subs L1 L2; subs L2 L3\<rbrakk> \<Longrightarrow> subs L1 L3"
-unfolding subs_def by (metis subset_trans)
-
-(* Language equivalence *)
-definition "leqv L1 L2 \<equiv> subs L1 L2 \<and> subs L2 L1"
-
-lemma subs_leqv[simp]: "leqv L1 L2 \<Longrightarrow> subs L1 L2"
-unfolding leqv_def by auto
-
-lemma subs_leqv_sym[simp]: "leqv L1 L2 \<Longrightarrow> subs L2 L1"
-unfolding leqv_def by auto
-
-lemma leqv_refl[simp]: "leqv L1 L1" unfolding leqv_def by auto
-
-lemma leqv_trans:
-assumes 12: "leqv L1 L2" and 23: "leqv L2 L3"
-shows "leqv L1 L3"
-using assms unfolding leqv_def by (metis (lifting) subs_trans)
-
-lemma leqv_sym: "leqv L1 L2 \<Longrightarrow> leqv L2 L1"
-unfolding leqv_def by auto
-
-lemma leqv_Sym: "leqv L1 L2 \<longleftrightarrow> leqv L2 L1"
-unfolding leqv_def by auto
-
-lemma Lr_incl_L: "Lr ns ts \<subseteq> L ns ts"
-unfolding Lr_def L_def by auto
-
-lemma Lr_subs_L: "subs (Lr UNIV ts) (L UNIV ts)"
-unfolding subs_def proof safe
- fix ts2 assume "ts2 \<in> L UNIV ts"
- then obtain tr where ts2: "ts2 = Fr UNIV tr" and dtr: "dtree tr" and rtr: "root tr = ts"
- unfolding L_def by auto
- thus "\<exists>ts1\<in>Lr UNIV ts. ts1 \<subseteq> ts2"
- apply(intro bexI[of _ "Fr UNIV (rcut tr)"])
- unfolding Lr_def L_def using Fr_rcut dtree_rcut root_rcut regular_rcut by auto
-qed
-
-theorem Lr_leqv_L: "leqv (Lr UNIV ts) (L UNIV ts)"
-using Lr_subs_L unfolding leqv_def by (metis (lifting) Lr_incl_L incl_subs)
-
-theorem LL_leqv_L: "leqv (LL UNIV ts) (L UNIV ts)"
-by (metis (lifting) LL_L Lr_LL Lr_subs_L incl_subs leqv_def subs_trans)
-
-theorem LL_leqv_Lr: "leqv (LL UNIV ts) (Lr UNIV ts)"
-using Lr_leqv_L LL_leqv_L by (metis leqv_Sym leqv_trans)
-
-
-end
--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy Tue Oct 16 22:13:46 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,152 +0,0 @@
-(* Title: HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy
- Author: Andrei Popescu, TU Muenchen
- Copyright 2012
-
-Parallel composition.
-*)
-
-header {* Parallel Composition *}
-
-theory Parallel
-imports Tree
-begin
-
-no_notation plus_class.plus (infixl "+" 65)
-no_notation Sublist.parallel (infixl "\<parallel>" 50)
-
-consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60)
-
-axiomatization where
- Nplus_comm: "(a::N) + b = b + (a::N)"
-and Nplus_assoc: "((a::N) + b) + c = a + (b + c)"
-
-section{* Parallel composition *}
-
-fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2"
-fun par_c where
-"par_c (tr1,tr2) =
- Inl ` (Inl -` (cont tr1 \<union> cont tr2)) \<union>
- Inr ` (Inr -` cont tr1 \<times> Inr -` cont tr2)"
-
-declare par_r.simps[simp del] declare par_c.simps[simp del]
-
-definition par :: "Tree \<times> Tree \<Rightarrow> Tree" where
-"par \<equiv> unfold par_r par_c"
-
-abbreviation par_abbr (infixr "\<parallel>" 80) where "tr1 \<parallel> tr2 \<equiv> par (tr1, tr2)"
-
-lemma finite_par_c: "finite (par_c (tr1, tr2))"
-unfolding par_c.simps apply(rule finite_UnI)
- apply (metis finite_Un finite_cont finite_imageI finite_vimageI inj_Inl)
- apply(intro finite_imageI finite_cartesian_product finite_vimageI)
- using finite_cont by auto
-
-lemma root_par: "root (tr1 \<parallel> tr2) = root tr1 + root tr2"
-using unfold(1)[of par_r par_c "(tr1,tr2)"] unfolding par_def par_r.simps by simp
-
-lemma cont_par:
-"cont (tr1 \<parallel> tr2) = (id \<oplus> par) ` par_c (tr1,tr2)"
-using unfold(2)[of par_c "(tr1,tr2)" par_r, OF finite_par_c]
-unfolding par_def ..
-
-lemma Inl_cont_par[simp]:
-"Inl -` (cont (tr1 \<parallel> tr2)) = Inl -` (cont tr1 \<union> cont tr2)"
-unfolding cont_par par_c.simps by auto
-
-lemma Inr_cont_par[simp]:
-"Inr -` (cont (tr1 \<parallel> tr2)) = par ` (Inr -` cont tr1 \<times> Inr -` cont tr2)"
-unfolding cont_par par_c.simps by auto
-
-lemma Inl_in_cont_par:
-"Inl t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (Inl t \<in> cont tr1 \<or> Inl t \<in> cont tr2)"
-using Inl_cont_par[of tr1 tr2] unfolding vimage_def by auto
-
-lemma Inr_in_cont_par:
-"Inr t \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> (t \<in> par ` (Inr -` cont tr1 \<times> Inr -` cont tr2))"
-using Inr_cont_par[of tr1 tr2] unfolding vimage_def by auto
-
-
-section{* =-coinductive proofs *}
-
-(* Detailed proofs of commutativity and associativity: *)
-theorem par_com: "tr1 \<parallel> tr2 = tr2 \<parallel> tr1"
-proof-
- let ?\<phi> = "\<lambda> trA trB. \<exists> tr1 tr2. trA = tr1 \<parallel> tr2 \<and> trB = tr2 \<parallel> tr1"
- {fix trA trB
- assume "?\<phi> trA trB" hence "trA = trB"
- proof (induct rule: Tree_coind, safe)
- fix tr1 tr2
- show "root (tr1 \<parallel> tr2) = root (tr2 \<parallel> tr1)"
- unfolding root_par by (rule Nplus_comm)
- next
- fix tr1 tr2 :: Tree
- let ?trA = "tr1 \<parallel> tr2" let ?trB = "tr2 \<parallel> tr1"
- show "(?\<phi> ^#2) (cont ?trA) (cont ?trB)"
- unfolding lift2_def proof(intro conjI allI impI)
- fix n show "Inl n \<in> cont (tr1 \<parallel> tr2) \<longleftrightarrow> Inl n \<in> cont (tr2 \<parallel> tr1)"
- unfolding Inl_in_cont_par by auto
- next
- fix trA' assume "Inr trA' \<in> cont ?trA"
- then obtain tr1' tr2' where "trA' = tr1' \<parallel> tr2'"
- and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
- unfolding Inr_in_cont_par by auto
- thus "\<exists> trB'. Inr trB' \<in> cont ?trB \<and> ?\<phi> trA' trB'"
- apply(intro exI[of _ "tr2' \<parallel> tr1'"]) unfolding Inr_in_cont_par by auto
- next
- fix trB' assume "Inr trB' \<in> cont ?trB"
- then obtain tr1' tr2' where "trB' = tr2' \<parallel> tr1'"
- and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
- unfolding Inr_in_cont_par by auto
- thus "\<exists> trA'. Inr trA' \<in> cont ?trA \<and> ?\<phi> trA' trB'"
- apply(intro exI[of _ "tr1' \<parallel> tr2'"]) unfolding Inr_in_cont_par by auto
- qed
- qed
- }
- thus ?thesis by blast
-qed
-
-theorem par_assoc: "(tr1 \<parallel> tr2) \<parallel> tr3 = tr1 \<parallel> (tr2 \<parallel> tr3)"
-proof-
- let ?\<phi> =
- "\<lambda> trA trB. \<exists> tr1 tr2 tr3. trA = (tr1 \<parallel> tr2) \<parallel> tr3 \<and>
- trB = tr1 \<parallel> (tr2 \<parallel> tr3)"
- {fix trA trB
- assume "?\<phi> trA trB" hence "trA = trB"
- proof (induct rule: Tree_coind, safe)
- fix tr1 tr2 tr3
- show "root ((tr1 \<parallel> tr2) \<parallel> tr3) = root (tr1 \<parallel> (tr2 \<parallel> tr3))"
- unfolding root_par by (rule Nplus_assoc)
- next
- fix tr1 tr2 tr3
- let ?trA = "(tr1 \<parallel> tr2) \<parallel> tr3" let ?trB = "tr1 \<parallel> (tr2 \<parallel> tr3)"
- show "(?\<phi> ^#2) (cont ?trA) (cont ?trB)"
- unfolding lift2_def proof(intro conjI allI impI)
- fix n show "Inl n \<in> (cont ?trA) \<longleftrightarrow> Inl n \<in> (cont ?trB)"
- unfolding Inl_in_cont_par by simp
- next
- fix trA' assume "Inr trA' \<in> cont ?trA"
- then obtain tr1' tr2' tr3' where "trA' = (tr1' \<parallel> tr2') \<parallel> tr3'"
- and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
- and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto
- thus "\<exists> trB'. Inr trB' \<in> cont ?trB \<and> ?\<phi> trA' trB'"
- apply(intro exI[of _ "tr1' \<parallel> (tr2' \<parallel> tr3')"])
- unfolding Inr_in_cont_par by auto
- next
- fix trB' assume "Inr trB' \<in> cont ?trB"
- then obtain tr1' tr2' tr3' where "trB' = tr1' \<parallel> (tr2' \<parallel> tr3')"
- and "Inr tr1' \<in> cont tr1" and "Inr tr2' \<in> cont tr2"
- and "Inr tr3' \<in> cont tr3" unfolding Inr_in_cont_par by auto
- thus "\<exists> trA'. Inr trA' \<in> cont ?trA \<and> ?\<phi> trA' trB'"
- apply(intro exI[of _ "(tr1' \<parallel> tr2') \<parallel> tr3'"])
- unfolding Inr_in_cont_par by auto
- qed
- qed
- }
- thus ?thesis by blast
-qed
-
-
-
-
-
-end
\ No newline at end of file
--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Prelim.thy Tue Oct 16 22:13:46 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,67 +0,0 @@
-(* Title: HOL/BNF/Examples/Infinite_Derivation_Trees/Prelim.thy
- Author: Andrei Popescu, TU Muenchen
- Copyright 2012
-
-Preliminaries.
-*)
-
-header {* Preliminaries *}
-
-theory Prelim
-imports "../../BNF"
-begin
-
-declare fset_to_fset[simp]
-
-lemma fst_snd_convol_o[simp]: "<fst o s, snd o s> = s"
-apply(rule ext) by (simp add: convol_def)
-
-abbreviation sm_abbrev (infix "\<oplus>" 60)
-where "f \<oplus> g \<equiv> Sum_Type.sum_map f g"
-
-lemma sum_map_InlD: "(f \<oplus> g) z = Inl x \<Longrightarrow> \<exists>y. z = Inl y \<and> f y = x"
-by (cases z) auto
-
-lemma sum_map_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
-by (cases z) auto
-
-abbreviation sum_case_abbrev ("[[_,_]]" 800)
-where "[[f,g]] \<equiv> Sum_Type.sum_case f g"
-
-lemma inj_Inl[simp]: "inj Inl" unfolding inj_on_def by auto
-lemma inj_Inr[simp]: "inj Inr" unfolding inj_on_def by auto
-
-lemma Inl_oplus_elim:
-assumes "Inl tr \<in> (id \<oplus> f) ` tns"
-shows "Inl tr \<in> tns"
-using assms apply clarify by (case_tac x, auto)
-
-lemma Inl_oplus_iff[simp]: "Inl tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> Inl tr \<in> tns"
-using Inl_oplus_elim
-by (metis id_def image_iff sum_map.simps(1))
-
-lemma Inl_m_oplus[simp]: "Inl -` (id \<oplus> f) ` tns = Inl -` tns"
-using Inl_oplus_iff unfolding vimage_def by auto
-
-lemma Inr_oplus_elim:
-assumes "Inr tr \<in> (id \<oplus> f) ` tns"
-shows "\<exists> n. Inr n \<in> tns \<and> f n = tr"
-using assms apply clarify by (case_tac x, auto)
-
-lemma Inr_oplus_iff[simp]:
-"Inr tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> (\<exists> n. Inr n \<in> tns \<and> f n = tr)"
-apply (rule iffI)
- apply (metis Inr_oplus_elim)
-by (metis image_iff sum_map.simps(2))
-
-lemma Inr_m_oplus[simp]: "Inr -` (id \<oplus> f) ` tns = f ` (Inr -` tns)"
-using Inr_oplus_iff unfolding vimage_def by auto
-
-lemma Inl_Inr_image_cong:
-assumes "Inl -` A = Inl -` B" and "Inr -` A = Inr -` B"
-shows "A = B"
-apply safe using assms apply(case_tac x, auto) by(case_tac x, auto)
-
-
-
-end
\ No newline at end of file
--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy Tue Oct 16 22:13:46 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,192 +0,0 @@
-(* Title: HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy
- Author: Andrei Popescu, TU Muenchen
- Copyright 2012
-
-Trees with nonterminal internal nodes and terminal leaves.
-*)
-
-header {* Trees with Nonterminal Internal Nodes and Terminal Leaves *}
-
-theory Tree
-imports Prelim
-begin
-
-hide_fact (open) Quotient_Product.prod_rel_def
-
-typedecl N
-typedecl T
-
-codata Tree = NNode (root: N) (ccont: "(T + Tree) fset")
-
-
-section {* Sugar notations for Tree *}
-
-definition
-"llift2 \<phi> as1 as2 \<longleftrightarrow>
- (\<forall> n. Inl n \<in> fset as1 \<longleftrightarrow> Inl n \<in> fset as2) \<and>
- (\<forall> tr1. Inr tr1 \<in> fset as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> fset as2 \<and> \<phi> tr1 tr2)) \<and>
- (\<forall> tr2. Inr tr2 \<in> fset as2 \<longrightarrow> (\<exists> tr1. Inr tr1 \<in> fset as1 \<and> \<phi> tr1 tr2))"
-
-lemma pre_Tree_rel: "pre_Tree_rel \<phi> (n1,as1) (n2,as2) \<longleftrightarrow> n1 = n2 \<and> llift2 \<phi> as1 as2"
-unfolding llift2_def pre_Tree_rel_def sum_rel_def[abs_def] prod_rel_def fset_rel_def split_conv
-apply (auto split: sum.splits)
-apply (metis sumE)
-apply (metis sumE)
-apply (metis sumE)
-apply (metis sumE)
-apply (metis sumE sum.simps(1,2,4))
-apply (metis sumE sum.simps(1,2,4))
-done
-
-
-subsection{* Coinduction *}
-
-theorem Tree_coind_NNode[elim, consumes 1, case_names NNode, induct pred: "HOL.eq"]:
-assumes phi: "\<phi> tr1 tr2" and
-NNode: "\<And> n1 n2 as1 as2.
- \<lbrakk>\<phi> (NNode n1 as1) (NNode n2 as2)\<rbrakk> \<Longrightarrow>
- n1 = n2 \<and> llift2 \<phi> as1 as2"
-shows "tr1 = tr2"
-apply(rule mp[OF Tree.dtor_coinduct[of \<phi> tr1 tr2] phi]) proof clarify
- fix tr1 tr2 assume \<phi>: "\<phi> tr1 tr2"
- show "pre_Tree_rel \<phi> (Tree_dtor tr1) (Tree_dtor tr2)"
- apply(cases rule: Tree.ctor_exhaust[of tr1], cases rule: Tree.ctor_exhaust[of tr2])
- apply (simp add: Tree.dtor_ctor)
- apply(case_tac x, case_tac xa, simp)
- unfolding pre_Tree_rel apply(rule NNode) using \<phi> unfolding NNode_def by simp
-qed
-
-theorem TTree_coind[elim, consumes 1, case_names LLift]:
-assumes phi: "\<phi> tr1 tr2" and
-LLift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow> root tr1 = root tr2 \<and> llift2 \<phi> (ccont tr1) (ccont tr2)"
-shows "tr1 = tr2"
-using phi apply(induct rule: Tree_coind_NNode)
-using LLift by (metis Tree.sels)
-
-
-subsection{* The characteristic theorems transported from fset to set *}
-
-definition "Node n as \<equiv> NNode n (the_inv fset as)"
-definition "cont \<equiv> fset o ccont"
-definition "unfold rt ct \<equiv> Tree_unfold rt (the_inv fset o ct)"
-definition "corec rt qt ct dt \<equiv> Tree_corec rt qt (the_inv fset o ct) (the_inv fset o dt)"
-
-definition lift ("_ ^#" 200) where
-"lift \<phi> as \<longleftrightarrow> (\<forall> tr. Inr tr \<in> as \<longrightarrow> \<phi> tr)"
-
-definition lift2 ("_ ^#2" 200) where
-"lift2 \<phi> as1 as2 \<longleftrightarrow>
- (\<forall> n. Inl n \<in> as1 \<longleftrightarrow> Inl n \<in> as2) \<and>
- (\<forall> tr1. Inr tr1 \<in> as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> as2 \<and> \<phi> tr1 tr2)) \<and>
- (\<forall> tr2. Inr tr2 \<in> as2 \<longrightarrow> (\<exists> tr1. Inr tr1 \<in> as1 \<and> \<phi> tr1 tr2))"
-
-definition liftS ("_ ^#s" 200) where
-"liftS trs = {as. Inr -` as \<subseteq> trs}"
-
-lemma lift2_llift2:
-"\<lbrakk>finite as1; finite as2\<rbrakk> \<Longrightarrow>
- lift2 \<phi> as1 as2 \<longleftrightarrow> llift2 \<phi> (the_inv fset as1) (the_inv fset as2)"
-unfolding lift2_def llift2_def by auto
-
-lemma llift2_lift2:
-"llift2 \<phi> as1 as2 \<longleftrightarrow> lift2 \<phi> (fset as1) (fset as2)"
-using lift2_llift2 by (metis finite_fset fset_cong fset_to_fset)
-
-lemma mono_lift:
-assumes "(\<phi>^#) as"
-and "\<And> tr. \<phi> tr \<Longrightarrow> \<phi>' tr"
-shows "(\<phi>'^#) as"
-using assms unfolding lift_def[abs_def] by blast
-
-lemma mono_liftS:
-assumes "trs1 \<subseteq> trs2 "
-shows "(trs1 ^#s) \<subseteq> (trs2 ^#s)"
-using assms unfolding liftS_def[abs_def] by blast
-
-lemma lift_mono:
-assumes "\<phi> \<le> \<phi>'"
-shows "(\<phi>^#) \<le> (\<phi>'^#)"
-using assms unfolding lift_def[abs_def] by blast
-
-lemma mono_lift2:
-assumes "(\<phi>^#2) as1 as2"
-and "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow> \<phi>' tr1 tr2"
-shows "(\<phi>'^#2) as1 as2"
-using assms unfolding lift2_def[abs_def] by blast
-
-lemma lift2_mono:
-assumes "\<phi> \<le> \<phi>'"
-shows "(\<phi>^#2) \<le> (\<phi>'^#2)"
-using assms unfolding lift2_def[abs_def] by blast
-
-lemma finite_cont[simp]: "finite (cont tr)"
-unfolding cont_def by auto
-
-theorem Node_root_cont[simp]:
-"Node (root tr) (cont tr) = tr"
-using Tree.collapse unfolding Node_def cont_def
-by (metis cont_def finite_cont fset_cong fset_to_fset o_def)
-
-theorem Tree_simps[simp]:
-assumes "finite as" and "finite as'"
-shows "Node n as = Node n' as' \<longleftrightarrow> n = n' \<and> as = as'"
-using assms Tree.inject unfolding Node_def
-by (metis fset_to_fset)
-
-theorem Tree_cases[elim, case_names Node Choice]:
-assumes Node: "\<And> n as. \<lbrakk>finite as; tr = Node n as\<rbrakk> \<Longrightarrow> phi"
-shows phi
-apply(cases rule: Tree.exhaust[of tr])
-using Node unfolding Node_def
-by (metis Node Node_root_cont finite_cont)
-
-theorem Tree_sel_ctor[simp]:
-"root (Node n as) = n"
-"finite as \<Longrightarrow> cont (Node n as) = as"
-unfolding Node_def cont_def by auto
-
-theorems root_Node = Tree_sel_ctor(1)
-theorems cont_Node = Tree_sel_ctor(2)
-
-theorem Tree_coind_Node[elim, consumes 1, case_names Node]:
-assumes phi: "\<phi> tr1 tr2" and
-Node:
-"\<And> n1 n2 as1 as2.
- \<lbrakk>finite as1; finite as2; \<phi> (Node n1 as1) (Node n2 as2)\<rbrakk>
- \<Longrightarrow> n1 = n2 \<and> (\<phi>^#2) as1 as2"
-shows "tr1 = tr2"
-using phi apply(induct rule: Tree_coind_NNode)
-unfolding llift2_lift2 apply(rule Node)
-unfolding Node_def
-apply (metis finite_fset)
-apply (metis finite_fset)
-by (metis finite_fset fset_cong fset_to_fset)
-
-theorem Tree_coind[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]:
-assumes phi: "\<phi> tr1 tr2" and
-Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
- root tr1 = root tr2 \<and> (\<phi>^#2) (cont tr1) (cont tr2)"
-shows "tr1 = tr2"
-using phi apply(induct rule: TTree_coind)
-unfolding llift2_lift2 apply(rule Lift[unfolded cont_def comp_def]) .
-
-theorem unfold:
-"root (unfold rt ct b) = rt b"
-"finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
-using Tree.sel_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def
-apply - apply metis
-unfolding cont_def comp_def
-by (metis (no_types) fset_to_fset map_fset_image)
-
-theorem corec:
-"root (corec rt qt ct dt b) = rt b"
-"\<lbrakk>finite (ct b); finite (dt b)\<rbrakk> \<Longrightarrow>
- cont (corec rt qt ct dt b) =
- (if qt b then ct b else image (id \<oplus> corec rt qt ct dt) (dt b))"
-using Tree.sel_corec[of rt qt "the_inv fset \<circ> ct" "the_inv fset \<circ> dt" b] unfolding corec_def
-apply -
-apply simp
-unfolding cont_def comp_def id_def
-by (metis (no_types) fset_to_fset map_fset_image)
-
-end
--- a/src/HOL/BNF/More_BNFs.thy Tue Oct 16 22:13:46 2012 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Tue Oct 16 22:38:34 2012 +0200
@@ -470,6 +470,9 @@
unfolding fset_rel_def fset_rel_aux by simp
qed auto
+lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
+unfolding fset_rel_def set_rel_def by auto
+
(* Countable sets *)
lemma card_of_countable_sets_range:
@@ -1508,4 +1511,74 @@
theorems multiset_rel_induct[case_names empty add, induct pred: multiset_rel] =
multiset_rel'.induct[unfolded multiset_rel_multiset_rel'[symmetric]]
+
+
+(* Advanced relator customization *)
+
+(* Set vs. sum relators: *)
+(* FIXME: All such facts should be declared as simps: *)
+declare sum_rel_simps[simp]
+
+lemma set_rel_sum_rel[simp]:
+"set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow>
+ set_rel \<chi> (Inl -` A1) (Inl -` A2) \<and> set_rel \<phi> (Inr -` A1) (Inr -` A2)"
+(is "?L \<longleftrightarrow> ?Rl \<and> ?Rr")
+proof safe
+ assume L: "?L"
+ show ?Rl unfolding set_rel_def Bex_def vimage_eq proof safe
+ fix l1 assume "Inl l1 \<in> A1"
+ then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inl l1) a2"
+ using L unfolding set_rel_def by auto
+ then obtain l2 where "a2 = Inl l2 \<and> \<chi> l1 l2" by (cases a2, auto)
+ thus "\<exists> l2. Inl l2 \<in> A2 \<and> \<chi> l1 l2" using a2 by auto
+ next
+ fix l2 assume "Inl l2 \<in> A2"
+ then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inl l2)"
+ using L unfolding set_rel_def by auto
+ then obtain l1 where "a1 = Inl l1 \<and> \<chi> l1 l2" by (cases a1, auto)
+ thus "\<exists> l1. Inl l1 \<in> A1 \<and> \<chi> l1 l2" using a1 by auto
+ qed
+ show ?Rr unfolding set_rel_def Bex_def vimage_eq proof safe
+ fix r1 assume "Inr r1 \<in> A1"
+ then obtain a2 where a2: "a2 \<in> A2" and "sum_rel \<chi> \<phi> (Inr r1) a2"
+ using L unfolding set_rel_def by auto
+ then obtain r2 where "a2 = Inr r2 \<and> \<phi> r1 r2" by (cases a2, auto)
+ thus "\<exists> r2. Inr r2 \<in> A2 \<and> \<phi> r1 r2" using a2 by auto
+ next
+ fix r2 assume "Inr r2 \<in> A2"
+ then obtain a1 where a1: "a1 \<in> A1" and "sum_rel \<chi> \<phi> a1 (Inr r2)"
+ using L unfolding set_rel_def by auto
+ then obtain r1 where "a1 = Inr r1 \<and> \<phi> r1 r2" by (cases a1, auto)
+ thus "\<exists> r1. Inr r1 \<in> A1 \<and> \<phi> r1 r2" using a1 by auto
+ qed
+next
+ assume Rl: "?Rl" and Rr: "?Rr"
+ show ?L unfolding set_rel_def Bex_def vimage_eq proof safe
+ fix a1 assume a1: "a1 \<in> A1"
+ show "\<exists> a2. a2 \<in> A2 \<and> sum_rel \<chi> \<phi> a1 a2"
+ proof(cases a1)
+ case (Inl l1) then obtain l2 where "Inl l2 \<in> A2 \<and> \<chi> l1 l2"
+ using Rl a1 unfolding set_rel_def by blast
+ thus ?thesis unfolding Inl by auto
+ next
+ case (Inr r1) then obtain r2 where "Inr r2 \<in> A2 \<and> \<phi> r1 r2"
+ using Rr a1 unfolding set_rel_def by blast
+ thus ?thesis unfolding Inr by auto
+ qed
+ next
+ fix a2 assume a2: "a2 \<in> A2"
+ show "\<exists> a1. a1 \<in> A1 \<and> sum_rel \<chi> \<phi> a1 a2"
+ proof(cases a2)
+ case (Inl l2) then obtain l1 where "Inl l1 \<in> A1 \<and> \<chi> l1 l2"
+ using Rl a2 unfolding set_rel_def by blast
+ thus ?thesis unfolding Inl by auto
+ next
+ case (Inr r2) then obtain r1 where "Inr r1 \<in> A1 \<and> \<phi> r1 r2"
+ using Rr a2 unfolding set_rel_def by blast
+ thus ?thesis unfolding Inr by auto
+ qed
+ qed
+qed
+
+
end
--- a/src/HOL/ROOT Tue Oct 16 22:13:46 2012 +0200
+++ b/src/HOL/ROOT Tue Oct 16 22:38:34 2012 +0200
@@ -628,8 +628,8 @@
Lambda_Term
Process
TreeFsetI
- "Infinite_Derivation_Trees/Gram_Lang"
- "Infinite_Derivation_Trees/Parallel"
+ "Derivation_Trees/Gram_Lang"
+ "Derivation_Trees/Parallel"
Stream
theories [condition = ISABELLE_FULL_TEST]
Misc_Codata
--- a/src/HOL/Sledgehammer.thy Tue Oct 16 22:13:46 2012 +0200
+++ b/src/HOL/Sledgehammer.thy Tue Oct 16 22:38:34 2012 +0200
@@ -14,6 +14,7 @@
ML_file "Tools/Sledgehammer/async_manager.ML"
ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
ML_file "Tools/Sledgehammer/sledgehammer_provers.ML"
ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Oct 16 22:13:46 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Oct 16 22:38:34 2012 +0200
@@ -13,6 +13,8 @@
type 'a proof = 'a ATP_Proof.proof
type stature = ATP_Problem_Generate.stature
+ structure String_Redirect : ATP_PROOF_REDIRECT
+
datatype reconstructor =
Metis of string * string |
SMT
@@ -61,10 +63,50 @@
val prop_from_atp :
Proof.context -> bool -> int Symtab.table
-> (string, string, (string, string) ho_term, string) formula -> term
- val isar_proof_text :
- Proof.context -> bool -> isar_params -> one_line_params -> string
- val proof_text :
- Proof.context -> bool -> isar_params -> int -> one_line_params -> string
+
+ type label
+ type facts = label list * string list
+
+ datatype isar_qualifier = Show | Then | Moreover | Ultimately
+
+ datatype isar_step =
+ Fix of (string * typ) list |
+ Let of term * term |
+ Assume of label * term |
+ Prove of isar_qualifier list * label * term * byline
+ and byline =
+ By_Metis of facts |
+ Case_Split of isar_step list list * facts
+
+ val string_for_label : label -> string
+ val decode_lines :
+ Proof.context -> int Symtab.table
+ -> (string, string, (string, string) ATP_Problem.ho_term, string)
+ ATP_Problem.formula ATP_Proof.step list -> term ATP_Proof.step list
+ val add_line :
+ (string * 'a) list vector -> term ATP_Proof.step
+ -> term ATP_Proof.step list -> term ATP_Proof.step list
+ val repair_waldmeister_endgame : term ATP_Proof.step list -> term ATP_Proof.step list
+ val add_desired_line :
+ int -> (string * 'a) list vector -> (string * typ) list -> term ATP_Proof.step
+ -> int * term ATP_Proof.step list -> int * term ATP_Proof.step list
+ val add_nontrivial_line :
+ term ATP_Proof.step -> term ATP_Proof.step list -> term ATP_Proof.step list
+ val forall_of : term -> term -> term
+ val raw_label_for_name : string * string list -> string * int
+
+ val no_label : label
+ val indent_size : int
+ val reconstructor_command :
+ reconstructor -> int -> int -> string list -> int
+ -> (string * int) list * string list -> string
+ val repair_name : string -> string
+ val add_fact_from_dependency :
+ (string * 'a) list vector -> string * string list
+ -> (string * int) list * string list -> (string * int) list * string list
+ val kill_duplicate_assumptions_in_proof : isar_step list -> isar_step list
+ val kill_useless_labels_in_proof : isar_step list -> isar_step list
+ val relabel_proof : isar_step list -> isar_step list
end;
structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT =
@@ -833,313 +875,4 @@
step :: aux subst depth nextp proof
in aux [] 0 (1, 1) end
-
-(** Type annotations **)
-
-fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
- | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
- | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
- | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
- | post_traverse_term_type' f env (Abs (x, T1, b)) s =
- let
- val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
- in f (Abs (x, T1, b')) (T1 --> T2) s' end
- | post_traverse_term_type' f env (u $ v) s =
- let
- val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
- val ((v', s''), _) = post_traverse_term_type' f env v s'
- in f (u' $ v') T s'' end
-
-fun post_traverse_term_type f s t =
- post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
-fun post_fold_term_type f s t =
- post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
-
-(* Data structures, orders *)
-val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
-
-structure Var_Set_Tab = Table(
- type key = indexname list
- val ord = list_ord Term_Ord.fast_indexname_ord)
-
-(* (1) Generalize Types *)
-fun generalize_types ctxt t =
- t |> map_types (fn _ => dummyT)
- |> Syntax.check_term
- (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
-
-(* (2) Typing-spot Table *)
-local
-fun key_of_atype (TVar (idxn, _)) =
- Ord_List.insert Term_Ord.fast_indexname_ord idxn
- | key_of_atype _ = I
-fun key_of_type T = fold_atyps key_of_atype T []
-fun update_tab t T (tab, pos) =
- (case key_of_type T of
- [] => tab
- | key =>
- let val cost = (size_of_typ T, (size_of_term t, pos)) in
- case Var_Set_Tab.lookup tab key of
- NONE => Var_Set_Tab.update_new (key, cost) tab
- | SOME old_cost =>
- (case cost_ord (cost, old_cost) of
- LESS => Var_Set_Tab.update (key, cost) tab
- | _ => tab)
- end,
- pos + 1)
-in
-val typing_spot_table =
- post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
-end
-
-(* (3) Reverse-Greedy *)
-fun reverse_greedy typing_spot_tab =
- let
- fun update_count z =
- fold (fn tvar => fn tab =>
- let val c = Vartab.lookup tab tvar |> the_default 0 in
- Vartab.update (tvar, c + z) tab
- end)
- fun superfluous tcount =
- forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
- fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
- if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
- else (spot :: spots, tcount)
- val (typing_spots, tvar_count_tab) =
- Var_Set_Tab.fold
- (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
- typing_spot_tab ([], Vartab.empty)
- |>> sort_distinct (rev_order o cost_ord o pairself snd)
- in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
-
-(* (4) Introduce Annotations *)
-fun introduce_annotations thy spots t t' =
- let
- val get_types = post_fold_term_type (K cons) []
- fun match_types tp =
- fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty
- fun unica' b x [] = if b then [x] else []
- | unica' b x (y :: ys) =
- if x = y then unica' false x ys
- else unica' true y ys |> b ? cons x
- fun unica ord xs =
- case sort ord xs of x :: ys => unica' true x ys | [] => []
- val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I)
- fun erase_unica_tfrees env =
- let
- val unica =
- Vartab.fold (add_all_tfree_namesT o snd o snd) env []
- |> unica fast_string_ord
- val erase_unica = map_atyps
- (fn T as TFree (s, _) =>
- if Ord_List.member fast_string_ord unica s then dummyT else T
- | T => T)
- in Vartab.map (K (apsnd erase_unica)) env end
- val env = match_types (t', t) |> erase_unica_tfrees
- fun get_annot env (TFree _) = (false, (env, dummyT))
- | get_annot env (T as TVar (v, S)) =
- let val T' = Envir.subst_type env T in
- if T' = dummyT then (false, (env, dummyT))
- else (true, (Vartab.update (v, (S, dummyT)) env, T'))
- end
- | get_annot env (Type (S, Ts)) =
- (case fold_rev (fn T => fn (b, (env, Ts)) =>
- let
- val (b', (env', T)) = get_annot env T
- in (b orelse b', (env', T :: Ts)) end)
- Ts (false, (env, [])) of
- (true, (env', Ts)) => (true, (env', Type (S, Ts)))
- | (false, (env', _)) => (false, (env', dummyT)))
- fun post1 _ T (env, cp, ps as p :: ps', annots) =
- if p <> cp then
- (env, cp + 1, ps, annots)
- else
- let val (_, (env', T')) = get_annot env T in
- (env', cp + 1, ps', (p, T') :: annots)
- end
- | post1 _ _ accum = accum
- val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'
- fun post2 t _ (cp, annots as (p, T) :: annots') =
- if p <> cp then (t, (cp + 1, annots))
- else (Type.constraint T t, (cp + 1, annots'))
- | post2 t _ x = (t, x)
- in post_traverse_term_type post2 (0, rev annots) t |> fst end
-
-(* (5) Annotate *)
-fun annotate_types ctxt t =
- let
- val thy = Proof_Context.theory_of ctxt
- val t' = generalize_types ctxt t
- val typing_spots =
- t' |> typing_spot_table
- |> reverse_greedy
- |> sort int_ord
- in introduce_annotations thy typing_spots t t' end
-
-fun string_for_proof ctxt type_enc lam_trans i n =
- let
- fun fix_print_mode f x =
- Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ())) f x
- fun do_indent ind = replicate_string (ind * indent_size) " "
- fun do_free (s, T) =
- maybe_quote s ^ " :: " ^
- maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
- fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
- fun do_have qs =
- (if member (op =) qs Moreover then "moreover " else "") ^
- (if member (op =) qs Ultimately then "ultimately " else "") ^
- (if member (op =) qs Then then
- if member (op =) qs Show then "thus" else "hence"
- else
- if member (op =) qs Show then "show" else "have")
- val do_term =
- maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
- o annotate_types ctxt
- val reconstr = Metis (type_enc, lam_trans)
- fun do_facts (ls, ss) =
- reconstructor_command reconstr 1 1 [] 0
- (ls |> sort_distinct (prod_ord string_ord int_ord),
- ss |> sort_distinct string_ord)
- and do_step ind (Fix xs) =
- do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
- | do_step ind (Let (t1, t2)) =
- do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
- | do_step ind (Assume (l, t)) =
- do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
- | do_step ind (Prove (qs, l, t, By_Metis facts)) =
- do_indent ind ^ do_have qs ^ " " ^
- do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
- | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
- implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
- proofs) ^
- do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
- do_facts facts ^ "\n"
- and do_steps prefix suffix ind steps =
- let val s = implode (map (do_step ind) steps) in
- replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
- String.extract (s, ind * indent_size,
- SOME (size s - ind * indent_size - 1)) ^
- suffix ^ "\n"
- end
- and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
- (* One-step proofs are pointless; better use the Metis one-liner
- directly. *)
- and do_proof [Prove (_, _, _, By_Metis _)] = ""
- | do_proof proof =
- (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
- do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
- (if n <> 1 then "next" else "qed")
- in do_proof end
-
-fun isar_proof_text ctxt isar_proof_requested
- (debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal)
- (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
- let
- val isar_shrink_factor =
- (if isar_proof_requested then 1 else 2) * isar_shrink_factor
- val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
- val frees = fold Term.add_frees (concl_t :: hyp_ts) []
- val one_line_proof = one_line_proof_text 0 one_line_params
- val type_enc =
- if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
- else partial_typesN
- val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
-
- fun isar_proof_of () =
- let
- val atp_proof =
- atp_proof
- |> clean_up_atp_proof_dependencies
- |> nasty_atp_proof pool
- |> map_term_names_in_atp_proof repair_name
- |> decode_lines ctxt sym_tab
- |> rpair [] |-> fold_rev (add_line fact_names)
- |> repair_waldmeister_endgame
- |> rpair [] |-> fold_rev add_nontrivial_line
- |> rpair (0, [])
- |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
- |> snd
- val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
- val conjs =
- atp_proof
- |> map_filter (fn Inference_Step (name as (_, ss), _, _, []) =>
- if member (op =) ss conj_name then SOME name else NONE
- | _ => NONE)
- fun dep_of_step (Definition_Step _) = NONE
- | dep_of_step (Inference_Step (name, _, _, from)) = SOME (from, name)
- val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
- val axioms = axioms_of_ref_graph ref_graph conjs
- val tainted = tainted_atoms_of_ref_graph ref_graph conjs
- val props =
- Symtab.empty
- |> fold (fn Definition_Step _ => I (* FIXME *)
- | Inference_Step ((s, _), t, _, _) =>
- Symtab.update_new (s,
- t |> fold forall_of (map Var (Term.add_vars t []))
- |> member (op = o apsnd fst) tainted s ? s_not))
- atp_proof
- fun prop_of_clause c =
- fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
- @{term False}
- fun label_of_clause [name] = raw_label_for_name name
- | label_of_clause c = (space_implode "___" (map fst c), 0)
- fun maybe_show outer c =
- (outer andalso length c = 1 andalso subset (op =) (c, conjs))
- ? cons Show
- fun do_have outer qs (gamma, c) =
- Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
- By_Metis (fold (add_fact_from_dependency fact_names
- o the_single) gamma ([], [])))
- fun do_inf outer (Have z) = do_have outer [] z
- | do_inf outer (Hence z) = do_have outer [Then] z
- | do_inf outer (Cases cases) =
- let val c = succedent_of_cases cases in
- Prove (maybe_show outer c [Ultimately], label_of_clause c,
- prop_of_clause c,
- Case_Split (map (do_case false) cases, ([], [])))
- end
- and do_case outer (c, infs) =
- Assume (label_of_clause c, prop_of_clause c) ::
- map (do_inf outer) infs
- val isar_proof =
- (if null params then [] else [Fix params]) @
- (ref_graph
- |> redirect_graph axioms tainted
- |> chain_direct_proof
- |> map (do_inf true)
- |> kill_duplicate_assumptions_in_proof
- |> kill_useless_labels_in_proof
- |> relabel_proof)
- |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
- in
- case isar_proof of
- "" =>
- if isar_proof_requested then
- "\nNo structured proof available (proof too short)."
- else
- ""
- | _ =>
- "\n\n" ^ (if isar_proof_requested then "Structured proof"
- else "Perhaps this will work") ^
- ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_proof
- end
- val isar_proof =
- if debug then
- isar_proof_of ()
- else case try isar_proof_of () of
- SOME s => s
- | NONE => if isar_proof_requested then
- "\nWarning: The Isar proof construction failed."
- else
- ""
- in one_line_proof ^ isar_proof end
-
-fun proof_text ctxt isar_proof isar_params num_chained
- (one_line_params as (preplay, _, _, _, _, _)) =
- (if case preplay of Failed_to_Play _ => true | _ => isar_proof then
- isar_proof_text ctxt isar_proof isar_params
- else
- one_line_proof_text num_chained) one_line_params
-
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Oct 16 22:13:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Oct 16 22:38:34 2012 +0200
@@ -149,6 +149,7 @@
open ATP_Proof_Reconstruct
open Metis_Tactic
open Sledgehammer_Util
+open Sledgehammer_Reconstruct
(** The Sledgehammer **)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Oct 16 22:38:34 2012 +0200
@@ -0,0 +1,414 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+*)
+
+signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
+sig
+ type isar_params = ATP_Proof_Reconstruct.isar_params
+ type one_line_params = ATP_Proof_Reconstruct.one_line_params
+ val isar_proof_text :
+ Proof.context -> bool -> isar_params ->
+ one_line_params -> string
+ val proof_text :
+ Proof.context -> bool -> isar_params ->
+ int -> one_line_params -> string
+end;
+
+structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
+struct
+
+open ATP_Util
+open ATP_Proof
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open String_Redirect
+
+(** Type annotations **)
+
+fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
+ | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
+ | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
+ | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
+ | post_traverse_term_type' f env (Abs (x, T1, b)) s =
+ let
+ val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
+ in f (Abs (x, T1, b')) (T1 --> T2) s' end
+ | post_traverse_term_type' f env (u $ v) s =
+ let
+ val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
+ val ((v', s''), _) = post_traverse_term_type' f env v s'
+ in f (u' $ v') T s'' end
+
+fun post_traverse_term_type f s t =
+ post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
+fun post_fold_term_type f s t =
+ post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
+
+(* Data structures, orders *)
+val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
+
+structure Var_Set_Tab = Table(
+ type key = indexname list
+ val ord = list_ord Term_Ord.fast_indexname_ord)
+
+(* (1) Generalize Types *)
+fun generalize_types ctxt t =
+ t |> map_types (fn _ => dummyT)
+ |> Syntax.check_term
+ (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
+
+(* (2) Typing-spot Table *)
+local
+fun key_of_atype (TVar (idxn, _)) =
+ Ord_List.insert Term_Ord.fast_indexname_ord idxn
+ | key_of_atype _ = I
+fun key_of_type T = fold_atyps key_of_atype T []
+fun update_tab t T (tab, pos) =
+ (case key_of_type T of
+ [] => tab
+ | key =>
+ let val cost = (size_of_typ T, (size_of_term t, pos)) in
+ case Var_Set_Tab.lookup tab key of
+ NONE => Var_Set_Tab.update_new (key, cost) tab
+ | SOME old_cost =>
+ (case cost_ord (cost, old_cost) of
+ LESS => Var_Set_Tab.update (key, cost) tab
+ | _ => tab)
+ end,
+ pos + 1)
+in
+val typing_spot_table =
+ post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
+end
+
+(* (3) Reverse-Greedy *)
+fun reverse_greedy typing_spot_tab =
+ let
+ fun update_count z =
+ fold (fn tvar => fn tab =>
+ let val c = Vartab.lookup tab tvar |> the_default 0 in
+ Vartab.update (tvar, c + z) tab
+ end)
+ fun superfluous tcount =
+ forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
+ fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
+ if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
+ else (spot :: spots, tcount)
+ val (typing_spots, tvar_count_tab) =
+ Var_Set_Tab.fold
+ (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
+ typing_spot_tab ([], Vartab.empty)
+ |>> sort_distinct (rev_order o cost_ord o pairself snd)
+ in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
+
+(* (4) Introduce Annotations *)
+fun introduce_annotations thy spots t t' =
+ let
+ val get_types = post_fold_term_type (K cons) []
+ fun match_types tp =
+ fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty
+ fun unica' b x [] = if b then [x] else []
+ | unica' b x (y :: ys) =
+ if x = y then unica' false x ys
+ else unica' true y ys |> b ? cons x
+ fun unica ord xs =
+ case sort ord xs of x :: ys => unica' true x ys | [] => []
+ val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x | _ => I)
+ fun erase_unica_tfrees env =
+ let
+ val unica =
+ Vartab.fold (add_all_tfree_namesT o snd o snd) env []
+ |> unica fast_string_ord
+ val erase_unica = map_atyps
+ (fn T as TFree (s, _) =>
+ if Ord_List.member fast_string_ord unica s then dummyT else T
+ | T => T)
+ in Vartab.map (K (apsnd erase_unica)) env end
+ val env = match_types (t', t) |> erase_unica_tfrees
+ fun get_annot env (TFree _) = (false, (env, dummyT))
+ | get_annot env (T as TVar (v, S)) =
+ let val T' = Envir.subst_type env T in
+ if T' = dummyT then (false, (env, dummyT))
+ else (true, (Vartab.update (v, (S, dummyT)) env, T'))
+ end
+ | get_annot env (Type (S, Ts)) =
+ (case fold_rev (fn T => fn (b, (env, Ts)) =>
+ let
+ val (b', (env', T)) = get_annot env T
+ in (b orelse b', (env', T :: Ts)) end)
+ Ts (false, (env, [])) of
+ (true, (env', Ts)) => (true, (env', Type (S, Ts)))
+ | (false, (env', _)) => (false, (env', dummyT)))
+ fun post1 _ T (env, cp, ps as p :: ps', annots) =
+ if p <> cp then
+ (env, cp + 1, ps, annots)
+ else
+ let val (_, (env', T')) = get_annot env T in
+ (env', cp + 1, ps', (p, T') :: annots)
+ end
+ | post1 _ _ accum = accum
+ val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t'
+ fun post2 t _ (cp, annots as (p, T) :: annots') =
+ if p <> cp then (t, (cp + 1, annots))
+ else (Type.constraint T t, (cp + 1, annots'))
+ | post2 t _ x = (t, x)
+ in post_traverse_term_type post2 (0, rev annots) t |> fst end
+
+(* (5) Annotate *)
+fun annotate_types ctxt t =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val t' = generalize_types ctxt t
+ val typing_spots =
+ t' |> typing_spot_table
+ |> reverse_greedy
+ |> sort int_ord
+ in introduce_annotations thy typing_spots t t' end
+
+fun string_for_proof ctxt type_enc lam_trans i n =
+ let
+ fun fix_print_mode f x =
+ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ())) f x
+ fun do_indent ind = replicate_string (ind * indent_size) " "
+ fun do_free (s, T) =
+ maybe_quote s ^ " :: " ^
+ maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
+ fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
+ fun do_have qs =
+ (if member (op =) qs Moreover then "moreover " else "") ^
+ (if member (op =) qs Ultimately then "ultimately " else "") ^
+ (if member (op =) qs Then then
+ if member (op =) qs Show then "thus" else "hence"
+ else
+ if member (op =) qs Show then "show" else "have")
+ val do_term =
+ maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
+ o annotate_types ctxt
+ val reconstr = Metis (type_enc, lam_trans)
+ fun do_facts (ls, ss) =
+ reconstructor_command reconstr 1 1 [] 0
+ (ls |> sort_distinct (prod_ord string_ord int_ord),
+ ss |> sort_distinct string_ord)
+ and do_step ind (Fix xs) =
+ do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
+ | do_step ind (Let (t1, t2)) =
+ do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
+ | do_step ind (Assume (l, t)) =
+ do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
+ | do_step ind (Prove (qs, l, t, By_Metis facts)) =
+ do_indent ind ^ do_have qs ^ " " ^
+ do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
+ | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) =
+ implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind)
+ proofs) ^
+ do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
+ do_facts facts ^ "\n"
+ and do_steps prefix suffix ind steps =
+ let val s = implode (map (do_step ind) steps) in
+ replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
+ String.extract (s, ind * indent_size,
+ SOME (size s - ind * indent_size - 1)) ^
+ suffix ^ "\n"
+ end
+ and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
+ (* One-step proofs are pointless; better use the Metis one-liner
+ directly. *)
+ and do_proof [Prove (_, _, _, By_Metis _)] = ""
+ | do_proof proof =
+ (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
+ do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
+ (if n <> 1 then "next" else "qed")
+ in do_proof end
+
+fun min_local ctxt type_enc lam_trans proof =
+ let
+ (* Merging spots, greedy algorithm *)
+ fun cost (Prove (_, _ , t, _)) = Term.size_of_term t
+ | cost _ = ~1
+ fun can_merge (Prove (_, lbl, _, By_Metis _)) (Prove (_, _, _, By_Metis _)) =
+ (lbl = no_label)
+ | can_merge _ _ = false
+ val merge_spots =
+ fold_index
+ (fn (i, s2) => fn (s1, pile) => (s2, pile |> can_merge s1 s2 ? cons (i, cost s1)))
+ (tl proof) (hd proof, [])
+ |> snd |> sort (rev_order o int_ord o pairself snd) |> map fst
+
+ (* Enrich context with facts *)
+ val thy = Proof_Context.theory_of ctxt
+ fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *)
+ fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt =
+ if lbl = no_label then ctxt
+ else Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t]) ctxt
+ | enrich_ctxt' _ ctxt = ctxt
+ val rich_ctxt = fold enrich_ctxt' proof ctxt
+
+ (* Timing *)
+ fun take_time tac arg =
+ let
+ val t_start = Timing.start ()
+ in
+ (tac arg ; Timing.result t_start |> #cpu)
+ end
+ fun try_metis (Prove (qs, _, t, By_Metis fact_names)) s0 =
+ let
+ fun thmify (Prove (_, _, t, _)) = sorry t
+ val facts = fact_names |>> map string_for_label
+ |> op@
+ |> map (Proof_Context.get_thm rich_ctxt)
+ |> (if member op= qs Then
+ then cons (the s0 |> thmify)
+ else I)
+ val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) (* FIXME: mk_Trueprop always ok? *)
+ fun tac {context = ctxt, prems = _} =
+ Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1
+ in
+ take_time (fn () => goal tac)
+ end
+
+ (* Merging *)
+ fun merge (Prove (qs1, _, _, By_Metis (ls1, ss1)))
+ (Prove (qs2, lbl , t, By_Metis (ls2, ss2))) =
+ let
+ val qs = (inter op= qs1 qs2) (* FIXME: Is this correct? *)
+ |> member op= (union op= qs1 qs2) Ultimately ? cons Ultimately
+ |> member op= qs2 Show ? cons Show
+ in Prove (qs, lbl, t, By_Metis (ls1@ls2, ss1@ss2)) end
+ fun try_merge proof i =
+ let
+ val (front, s0, s1, s2, tail) =
+ case (proof, i) of
+ ((s1::s2::proof), 0) => ([], NONE, s1, s2, proof)
+ | _ => let val (front, s0::s1::s2::tail) = chop (i-1) proof
+ in (front, SOME s0, s1, s2, tail) end
+ val s12 = merge s1 s2
+ val t1 = try_metis s1 s0 ()
+ val t2 = try_metis s2 (SOME s1) ()
+ val tlimit = t1 + t2 |> Time.toReal |> curry Real.* 1.2 |> Time.fromReal
+ in
+ (TimeLimit.timeLimit tlimit (try_metis s12 s0) ();
+ SOME (front @ (case s0 of NONE => s12::tail | SOME s => s::s12::tail)))
+ handle _ => NONE
+ end
+ fun merge_steps proof [] = proof
+ | merge_steps proof (i::is) =
+ case try_merge proof i of
+ NONE => merge_steps proof is
+ | SOME proof' => merge_steps proof' (map (fn j => if j>i then j-1 else j) is)
+ in merge_steps proof merge_spots end
+
+fun isar_proof_text ctxt isar_proof_requested
+ (debug, isar_shrink_factor, pool, fact_names, sym_tab, atp_proof, goal)
+ (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
+ let
+ val isar_shrink_factor =
+ (if isar_proof_requested then 1 else 2) * isar_shrink_factor
+ val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
+ val frees = fold Term.add_frees (concl_t :: hyp_ts) []
+ val one_line_proof = one_line_proof_text 0 one_line_params
+ val type_enc =
+ if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
+ else partial_typesN
+ val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
+
+ fun isar_proof_of () =
+ let
+ val atp_proof =
+ atp_proof
+ |> clean_up_atp_proof_dependencies
+ |> nasty_atp_proof pool
+ |> map_term_names_in_atp_proof repair_name
+ |> decode_lines ctxt sym_tab
+ |> rpair [] |-> fold_rev (add_line fact_names)
+ |> repair_waldmeister_endgame
+ |> rpair [] |-> fold_rev add_nontrivial_line
+ |> rpair (0, [])
+ |-> fold_rev (add_desired_line isar_shrink_factor fact_names frees)
+ |> snd
+ val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts)
+ val conjs =
+ atp_proof
+ |> map_filter (fn Inference_Step (name as (_, ss), _, _, []) =>
+ if member (op =) ss conj_name then SOME name else NONE
+ | _ => NONE)
+ fun dep_of_step (Definition_Step _) = NONE
+ | dep_of_step (Inference_Step (name, _, _, from)) = SOME (from, name)
+ val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph
+ val axioms = axioms_of_ref_graph ref_graph conjs
+ val tainted = tainted_atoms_of_ref_graph ref_graph conjs
+ val props =
+ Symtab.empty
+ |> fold (fn Definition_Step _ => I (* FIXME *)
+ | Inference_Step ((s, _), t, _, _) =>
+ Symtab.update_new (s,
+ t |> fold forall_of (map Var (Term.add_vars t []))
+ |> member (op = o apsnd fst) tainted s ? s_not))
+ atp_proof
+ fun prop_of_clause c =
+ fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
+ @{term False}
+ fun label_of_clause [name] = raw_label_for_name name
+ | label_of_clause c = (space_implode "___" (map fst c), 0)
+ fun maybe_show outer c =
+ (outer andalso length c = 1 andalso subset (op =) (c, conjs))
+ ? cons Show
+ fun do_have outer qs (gamma, c) =
+ Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
+ By_Metis (fold (add_fact_from_dependency fact_names
+ o the_single) gamma ([], [])))
+ fun do_inf outer (Have z) = do_have outer [] z
+ | do_inf outer (Hence z) = do_have outer [Then] z
+ | do_inf outer (Cases cases) =
+ let val c = succedent_of_cases cases in
+ Prove (maybe_show outer c [Ultimately], label_of_clause c,
+ prop_of_clause c,
+ Case_Split (map (do_case false) cases, ([], [])))
+ end
+ and do_case outer (c, infs) =
+ Assume (label_of_clause c, prop_of_clause c) ::
+ map (do_inf outer) infs
+ val isar_proof =
+ (if null params then [] else [Fix params]) @
+ (ref_graph
+ |> redirect_graph axioms tainted
+ |> chain_direct_proof
+ |> map (do_inf true)
+ |> kill_duplicate_assumptions_in_proof
+ |> kill_useless_labels_in_proof
+ |> relabel_proof
+ |> min_local ctxt type_enc lam_trans)
+ |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
+ in
+ case isar_proof of
+ "" =>
+ if isar_proof_requested then
+ "\nNo structured proof available (proof too short)."
+ else
+ ""
+ | _ =>
+ "\n\n" ^ (if isar_proof_requested then "Structured proof"
+ else "Perhaps this will work") ^
+ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_proof
+ end
+ val isar_proof =
+ if debug then
+ isar_proof_of ()
+ else case try isar_proof_of () of
+ SOME s => s
+ | NONE => if isar_proof_requested then
+ "\nWarning: The Isar proof construction failed."
+ else
+ ""
+ in one_line_proof ^ isar_proof end
+
+fun proof_text ctxt isar_proof isar_params num_chained
+ (one_line_params as (preplay, _, _, _, _, _)) =
+ (if case preplay of Failed_to_Play _ => true | _ => isar_proof then
+ isar_proof_text ctxt isar_proof isar_params
+ else
+ one_line_proof_text num_chained) one_line_params
+
+end;
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Tue Oct 16 22:13:46 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Tue Oct 16 22:38:34 2012 +0200
@@ -58,6 +58,13 @@
T1 --> (setT --> T2) --> resT) $ t1 $ absdummy setT t2
end;
+fun mk_vimage f s =
+ let
+ val T as Type (@{type_name fun}, [T1, T2]) = fastype_of f
+ in
+ Const (@{const_name vimage}, T --> HOLogic.mk_setT T2 --> HOLogic.mk_setT T1) $ f $ s
+ end;
+
fun dest_Collect (Const (@{const_name Collect}, _) $ Abs (x, T, t)) = ((x, T), t)
| dest_Collect t = raise TERM ("dest_Collect", [t])
@@ -77,6 +84,11 @@
HOLogic.pair_const T1 T2 $ t1 $ t2
end;
+fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end
+ | mk_split_abs vs (Const ("Product_Type.Pair", _) $ u $ v) t =
+ HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t))
+ | mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]);
+
(* patterns *)
@@ -107,8 +119,25 @@
datatype formula = Atom of (pattern * term) | Int of formula * formula | Un of formula * formula
-fun mk_atom (Const (@{const_name "Set.member"}, _) $ x $ s) = (mk_pattern x, Atom (mk_pattern x, s))
- | mk_atom (Const (@{const_name "HOL.Not"}, _) $ (Const (@{const_name "Set.member"}, _) $ x $ s)) =
+fun mk_atom vs (Const (@{const_name "Set.member"}, _) $ x $ s) =
+ (case try mk_pattern x of
+ SOME pat => (pat, Atom (pat, s))
+ | NONE =>
+ let
+ val bs = loose_bnos x
+ val vs' = map (nth (rev vs)) bs
+ val x' = subst_atomic (map_index (fn (i, j) => (Bound j, Bound i)) (rev bs)) x
+ val tuple = foldr1 TPair (map TBound bs)
+ val rT = HOLogic.dest_setT (fastype_of s)
+ fun mk_split [(x, T)] t = (T, Abs (x, T, t))
+ | mk_split ((x, T) :: vs) t =
+ let
+ val (T', t') = mk_split vs t
+ val t'' = HOLogic.split_const (T, T', rT) $ (Abs (x, T, t'))
+ in (domain_type (fastype_of t''), t'') end
+ val (_, f) = mk_split vs' x'
+ in (tuple, Atom (tuple, mk_vimage f s)) end)
+ | mk_atom _ (Const (@{const_name "HOL.Not"}, _) $ (Const (@{const_name "Set.member"}, _) $ x $ s)) =
(mk_pattern x, Atom (mk_pattern x, mk_Compl s))
fun can_merge (pats1, pats2) =
@@ -126,9 +155,9 @@
fun merge oper (pats1, sp1) (pats2, sp2) = (merge_patterns (pats1, pats2), oper (sp1, sp2))
-fun mk_formula (@{const HOL.conj} $ t1 $ t2) = merge Int (mk_formula t1) (mk_formula t2)
- | mk_formula (@{const HOL.disj} $ t1 $ t2) = merge Un (mk_formula t1) (mk_formula t2)
- | mk_formula t = apfst single (mk_atom t)
+fun mk_formula vs (@{const HOL.conj} $ t1 $ t2) = merge Int (mk_formula vs t1) (mk_formula vs t2)
+ | mk_formula vs (@{const HOL.disj} $ t1 $ t2) = merge Un (mk_formula vs t1) (mk_formula vs t2)
+ | mk_formula vs t = apfst single (mk_atom vs t)
fun strip_Int (Int (fm1, fm2)) = fm1 :: (strip_Int fm2)
| strip_Int fm = [fm]
@@ -144,11 +173,6 @@
subst_bounds (map Bound bperm, t)
end;
-fun mk_split_abs vs (Bound i) t = let val (x, T) = nth vs i in Abs (x, T, t) end
- | mk_split_abs vs (Const ("Product_Type.Pair", _) $ u $ v) t =
- HOLogic.mk_split (mk_split_abs vs u (mk_split_abs vs v t))
- | mk_split_abs _ t _ = raise TERM ("mk_split_abs: bad term", [t]);
-
fun mk_pointfree_expr t =
let
val ((x, T), (vs, t'')) = apsnd strip_ex (dest_Collect t)
@@ -165,7 +189,7 @@
val unused_bounds = subtract (op =) (distinct (op =) (maps loose_bnos conjs'))
(0 upto (length vs - 1))
val (pats, fm) =
- mk_formula (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
+ mk_formula vs (foldr1 HOLogic.mk_conj (conjs' @ map mk_mem_UNIV unused_bounds))
fun mk_set (Atom pt) = (case map (lookup pt) pats of [t'] => t' | ts => foldr1 mk_sigma ts)
| mk_set (Un (f1, f2)) = mk_sup (mk_set f1, mk_set f2)
| mk_set (Int (f1, f2)) = mk_inf (mk_set f1, mk_set f2)
@@ -222,10 +246,12 @@
THEN' rtac @{thm UnI2}
THEN' tac1_of_formula fm2
| tac1_of_formula (Atom _) =
- (REPEAT_DETERM1 o (rtac @{thm SigmaI}
+ REPEAT_DETERM1 o (rtac @{thm SigmaI}
+ ORELSE' (rtac @{thm vimageI2} THEN'
+ TRY o Simplifier.simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}]))
ORELSE' rtac @{thm UNIV_I}
ORELSE' rtac @{thm iffD2[OF Compl_iff]}
- ORELSE' atac))
+ ORELSE' atac)
fun tac2_of_formula (Int (fm1, fm2)) =
TRY o etac @{thm IntE}
@@ -241,6 +267,9 @@
TRY o REPEAT_DETERM1 o
(dtac @{thm iffD1[OF mem_Sigma_iff]}
ORELSE' etac @{thm conjE}
+ ORELSE' (etac @{thm vimageE}
+ THEN' TRY o Simplifier.full_simp_tac (HOL_basic_ss addsimps [@{thm prod.cases}])
+ THEN' TRY o hyp_subst_tac)
ORELSE' etac @{thm ComplE}
ORELSE' atac)
@@ -265,6 +294,8 @@
(* main simprocs *)
+val prep_thms = map mk_meta_eq [@{thm Bex_def}, @{thm Pow_iff[symmetric]}]
+
val post_thms =
map mk_meta_eq [@{thm Times_Un_distrib1[symmetric]},
@{lemma "A \<times> B \<union> A \<times> C = A \<times> (B \<union> C)" by auto},
@@ -273,12 +304,11 @@
fun conv ctxt t =
let
val ct = cterm_of (Proof_Context.theory_of ctxt) t
- val Bex_def = mk_meta_eq @{thm Bex_def}
- val unfold_eq = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv Bex_def))) ctxt ct
- val t' = term_of (Thm.rhs_of unfold_eq)
+ val prep_eq = Raw_Simplifier.rewrite true prep_thms ct
+ val t' = term_of (Thm.rhs_of prep_eq)
fun mk_thm (fm, t'') = Goal.prove ctxt [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (t', t''))) (fn {context, ...} => tac context fm 1)
- fun unfold th = th RS ((unfold_eq RS meta_eq_to_obj_eq) RS @{thm trans})
+ fun unfold th = th RS ((prep_eq RS meta_eq_to_obj_eq) RS @{thm trans})
fun post th = Conv.fconv_rule (Trueprop_conv (eq_conv Conv.all_conv
(Raw_Simplifier.rewrite true post_thms))) th
in
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Tue Oct 16 22:13:46 2012 +0200
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy Tue Oct 16 22:38:34 2012 +0200
@@ -91,6 +91,20 @@
"finite A ==> finite B ==> finite {f a * g b |a b. a : A & b : B}"
by simp
+lemma
+ "finite S ==> inj (%(x, y). g x y) ==> finite {f x y| x y. g x y : S}"
+ by (auto intro: finite_vimageI)
+
+lemma
+ "finite A ==> finite S ==> inj (%(x, y). g x y) ==> finite {f x y z | x y z. g x y : S & z : A}"
+ by (auto intro: finite_vimageI)
+
+lemma
+ "finite S ==> finite A ==> inj (%(x, y). g x y) ==> inj (%(x, y). h x y)
+ ==> finite {f a b c d | a b c d. g a c : S & h b d : A}"
+ by (auto intro: finite_vimageI)
+
+
schematic_lemma (* check interaction with schematics *)
"finite {x :: ?'A \<Rightarrow> ?'B \<Rightarrow> bool. \<exists>a b. x = Pair_Rep a b}
= finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
@@ -106,4 +120,18 @@
(* to be automated with further rules and automation *)
qed
+section {* Testing simproc in code generation *}
+
+definition union :: "nat set => nat set => nat set"
+where
+ "union A B = {x. x : A \<or> x : B}"
+
+definition common_subsets :: "nat set => nat set => nat set set"
+where
+ "common_subsets S1 S2 = {S. S \<subseteq> S1 \<and> S \<subseteq> S2}"
+
+export_code union common_subsets in Haskell file -
+
+
+
end