theory GTT_RRn imports GTT RRn_Automata begin abbreviation ggtt_lang where "ggtt_lang F G ≡ map_both gterm_of_term ` (Restr (gtt_lang G) {t. funas_term t ⊆ F})" lemma ground_mctxt_map_vars_mctxt [simp]: "ground_mctxt (map_vars_mctxt f C) = ground_mctxt C" by (induct C) auto definition parallel_closure_automaton :: "('f × nat) set ⇒ ('q, 'f option × 'f option) ta ⇒ (_, 'f option × 'f option) ta" where "parallel_closure_automaton F A = ta.make {None} (map_ta_rule Some id ` ta_rules A ∪ {(Some f, Some f) (replicate n None) → None |f n. (f, n) ∈ F}) (map_both Some ` ta_eps A ∪ {(Some q, None) |q. q ∈ ta_final A})" definition gfill_holes :: "(_, unit) mctxt ⇒ _ ⇒ _" where "gfill_holes C ts = gterm_of_term (fill_holes C (map term_of_gterm ts))" lemma gpair_context1: assumes "length ts = length us" shows "gpair (GFun f ts) (GFun f us) = GFun (Some f, Some f) (map (case_prod gpair) (zip ts us))" using assms unfolding gpair_code by (auto intro!: nth_equalityI simp: zip_fill_def) lemma gpair_inject [simp]: "gpair s t = gpair s' t' ⟷ s = s' ∧ t = t'" by (metis gfst_gpair gsnd_gpair) lemma parallel_closure_automaton: assumes "RR2_spec A R" shows "RR2_spec (parallel_closure_automaton F A) {(gfill_holes C ts, gfill_holes C us) |C ts us. ground_mctxt C ∧ funas_mctxt C ⊆ F ∧ length ts = num_holes C ∧ length us = num_holes C ∧ (∀i < num_holes C. (ts ! i, us ! i) ∈ R)}" proof - have [simp]: "(t, u) ∈ R ⟷ gpair t u ∈ gta_lang A" for t u using assms by (auto simp: RR2_spec_def) { fix s assume "s ∈ gta_lang (parallel_closure_automaton F A)" then have "None ∈ ta_res (parallel_closure_automaton F A) (term_of_gterm s)" by (auto simp: gta_lang_def parallel_closure_automaton_def elim!: ta_langE2) then have "∃t u C ts us. s = gpair t u ∧ t = gfill_holes C ts ∧ u = gfill_holes C us ∧ ground_mctxt C ∧ funas_mctxt C ⊆ F ∧ length ts = num_holes C ∧ length us = num_holes C ∧ (∀i<num_holes C. gpair (ts ! i) (us ! i) ∈ gta_lang A)" proof (induct s) case (GFun f ss) obtain q' qs where q: "f qs → q' ∈ ta_rules (parallel_closure_automaton F A)" "(q', None) ∈ (ta_eps (parallel_closure_automaton F A))⇧*" "length qs = length ss" "⋀i. i<length qs ⟹ qs ! i ∈ ta_res (parallel_closure_automaton F A) (term_of_gterm (ss ! i))" using GFun(2) by auto have "map_ta_rule g h r = case_ta_rule (λf qs q. map_ta_rule g h (f qs → q)) r" for g h r by (cases r) auto note * = this[unfolded ta_rule.simps] show ?case proof (cases q') case None obtain f' where f': "qs = replicate (length ss) None" "f = (Some f', Some f')" "(f', length ss) ∈ F" using q(1) None by (auto simp: parallel_closure_automaton_def * q(3)[symmetric] split: ta_rule.splits) { fix i assume "i < length ss" then have "∃C ts us. ground_mctxt C ∧ funas_mctxt C ⊆ F ∧ length ts = num_holes C ∧ length us = num_holes C ∧ ss ! i = gpair (gfill_holes C ts) (gfill_holes C us) ∧ (∀i<num_holes C. gpair (ts ! i) (us ! i) ∈ gta_lang A)" using GFun(1)[OF nth_mem, of i] q(4)[of i] by (auto simp: f'(1)) } then obtain Cs tss uss where "⋀i. i < length ss ⟹ ground_mctxt (Cs i) ∧ funas_mctxt (Cs i) ⊆ F ∧ length (tss i) = num_holes (Cs i) ∧ length (uss i) = num_holes (Cs i) ∧ ss ! i = gpair (gfill_holes (Cs i) (tss i)) (gfill_holes (Cs i) (uss i)) ∧ (∀j<num_holes (Cs i). gpair ((tss i) ! j) ((uss i) ! j) ∈ gta_lang A)" by metis note Cs = conjunct1[OF this] conjunct1[OF conjunct2[OF conjunct2[OF this]]] conjunct1[OF conjunct2[OF conjunct2[OF conjunct2[OF this]]]] conjunct1[OF conjunct2[OF conjunct2[OF conjunct2[OF conjunct2[OF this]]]]] conjunct2[OF conjunct2[OF conjunct2[OF conjunct2[OF conjunct2[OF this]]]]] conjunct1[OF conjunct2[OF this]] have l: "length (concat (map tss [0..<length ss])) = sum_list (map (num_holes ∘ Cs) [0..<length ss])" "length (concat (map uss [0..<length ss])) = sum_list (map (num_holes ∘ Cs) [0..<length ss])" by (auto simp: Cs(2,3) length_concat cong: list.map_cong_simp) have p: "partition_by (map term_of_gterm (concat (map tss [0..<length ss]))) (map (num_holes ∘ Cs) [0..<length ss]) = map (map term_of_gterm ∘ tss) [0..<length ss]" "partition_by (map term_of_gterm (concat (map uss [0..<length ss]))) (map (num_holes ∘ Cs) [0..<length ss]) = map (map term_of_gterm ∘ uss) [0..<length ss]" unfolding map_concat by (subst partition_by_concat_id; simp add: Cs(2,3))+ have g: "gpair (concat (map tss [0..<length ss]) ! i) (concat (map uss [0..<length ss]) ! i) ∈ gta_lang A" if "i < sum_list (map (num_holes ∘ Cs) [0..<length ss])" for i using nth_concat_two_lists[of i "map tss [0..<length ss]" "map uss [0..<length ss]"] by (auto simp: that l Cs(2,3,5)) show ?thesis using Cs(1,4) subsetD[OF Cs(6)] f'(3) by (auto simp: gpair_context1 f'(2) gfill_holes_def l p g intro!: exI[of _ "GFun f' (map (λi. gfill_holes (Cs i) (tss i)) [0..<length ss])", OF exI[of _ "GFun f' (map (λi. gfill_holes (Cs i) (uss i)) [0..<length ss])"]] exI[of _ "MFun f' (map Cs [0..<length ss])"] exI[of _ "concat (map tss [0..<length ss])", OF conjI[OF _ exI[of _ "concat (map uss [0..<length ss])"]]] nth_equalityI) next case (Some p') obtain p where p: "(Some p', Some p) ∈ (ta_eps (parallel_closure_automaton F A))⇧*" "p ∈ ta_final A" using q(2) by (cases rule: rtrancl.cases) (auto simp: parallel_closure_automaton_def Some) have "Some p ∈ ta_res (parallel_closure_automaton F A) (term_of_gterm (GFun f ss))" using q(1,3,4) p(1) by (auto simp: Some) then have "p ∈ ta_res A (term_of_gterm (GFun f ss))" proof (induct ("GFun f ss") arbitrary: p) case (GFun f ss) obtain q' qs where q': "f qs → q' ∈ ta_rules (parallel_closure_automaton F A)" "(q', Some p) ∈ (ta_eps (parallel_closure_automaton F A))⇧*" "length qs = length ss" "⋀i. i < length ss ⟹ qs ! i ∈ ta_res (parallel_closure_automaton F A) (term_of_gterm (ss ! i))" using GFun(2) by auto obtain p' where p': "q' = Some p'" "(p', p) ∈ (ta_eps A)⇧*" using q'(2) proof (induct "Some p" arbitrary: thesis p) case (step q'') obtain p'' where p'': "q'' = Some p''" "(p'', p) ∈ ta_eps A" using step(2) by (cases q'') (auto simp: parallel_closure_automaton_def) obtain p' where "q' = Some p'" "(p', p'') ∈ (ta_eps A)⇧*" using step(3)[OF p''(1)] . then show ?case using p''(2) by (auto simp: parallel_closure_automaton_def intro: step(4)) qed auto then obtain ps where "qs = map Some ps" "f ps → p' ∈ ta_rules A" using q'(1) by (auto simp: parallel_closure_automaton_def * split: ta_rule.splits) then show ?case using p'(2) q'(3,4) GFun(1)[OF nth_mem, of i "ps ! i" for i] by (auto intro!: exI[of _ p'] exI[of _ ps]) qed then have "GFun f ss ∈ gta_lang A" using p(2) by (auto 0 3 simp: gta_lang_def image_def comp_def adapt_vars_def gterm.map_ident simp del: ta_res.simps intro!: bexI[of _ "term_of_gterm _"] ta_langI2) then show ?thesis unfolding assms[unfolded RR2_spec_def] by (auto simp: gfst_gpair gsnd_gpair gfill_holes_def intro!: exI[of _ "gfst (GFun f ss)", OF exI[of _ "gsnd (GFun f ss)"]] exI[of _ MHole] exI[of _ "[_]"]) qed qed } note [dest!] = this { fix C :: "('b, unit) mctxt" and ts us assume C: "ground_mctxt C" "length ts = num_holes C" "length us = num_holes C" "⋀i. i<num_holes C ⟹ gpair (ts ! i) (us ! i) ∈ gta_lang A" "funas_mctxt C ⊆ F" have "None ∈ ta_res (parallel_closure_automaton F A) (term_of_gterm (gpair (gfill_holes C ts) (gfill_holes C us)))" using C(2,3)[symmetric] C(1,4,5) proof (induct C ts us rule: fill_holes_induct2) case (MHole t u) obtain q where q: "q ∈ ta_final A" "q ∈ ta_res A (term_of_gterm (gpair t u))" using MHole(2)[of 0] by (auto simp: gta_lang_def elim!: ta_langE2) have "Some q ∈ ta_res (parallel_closure_automaton F A) (term_of_gterm (gpair t u))" by (rule subsetD[OF ta_res_mono' ta_res_fmap_states_ta[OF q(2), of Some], of "parallel_closure_automaton F A", unfolded map_term_of_gterm gterm.map_ident]) (auto simp: fmap_states_ta_def' parallel_closure_automaton_def) note * = ta_res_eps[OF this] have "None ∈ ta_res (parallel_closure_automaton F A) (term_of_gterm (gpair t u))" using q(1) by (intro *) (auto simp: parallel_closure_automaton_def) then show ?case by (auto simp: gta_lang_def gfill_holes_def elim!: ta_langE2 dest!: ground_term_to_gtermD) next case (MFun f Cs ts us) have "funas_mctxt (Cs ! i) ⊆ F" if "i < length Cs" for i using MFun(6) that by (auto simp: set_conv_nth) then show ?case using MFun(1,2)[symmetric] MFun(3,4) MFun(5)[of "partition_holes_idx (sum_list (map num_holes Cs)) Cs _ _", unfolded num_holes.simps, OF partition_by_nth_nth(2)[OF MFun(1), unfolded MFun(1)[symmetric]]] MFun(6) by (auto simp: gfill_holes_def gpair_context1 partition_by_nth_nth(1) parallel_closure_automaton_def intro!: exI[of _ "replicate _ None"] exI[of _ None]) qed auto then have "gpair (gfill_holes C ts) (gfill_holes C us) ∈ gta_lang (parallel_closure_automaton F A)" by (auto simp: gta_lang_def image_def parallel_closure_automaton_def intro!: bexI[of _ "term_of_gterm _"] ta_langI2) } note [intro!] = this show ?thesis by (force simp: RR2_spec_def) qed definition GTT_to_RR2_root :: "('q, 'f) gtt ⇒ (_, 'f option × 'f option) ta" where "GTT_to_RR2_root 𝒢 = (pair_automaton (fst 𝒢) (snd 𝒢))⦇ ta_final := {(Some q, Some q) |q. q ∈ gtt_states 𝒢} ⦈" lemma GTT_to_RR2_root: "RR2_spec (GTT_to_RR2_root 𝒢) {(t, u) |t u q. q ∈ ta_res (fst 𝒢) (term_of_gterm t) ∧ q ∈ ta_res (snd 𝒢) (term_of_gterm u)}" proof - { fix s assume "s ∈ gta_lang (GTT_to_RR2_root 𝒢)" then obtain q where q: "q ∈ ta_final (GTT_to_RR2_root 𝒢)" "q ∈ ta_res (GTT_to_RR2_root 𝒢) (term_of_gterm s)" by (auto simp: gta_lang_def elim: ta_langE2) then obtain q' where [simp]: "q = (Some q', Some q')" using q(1) by (auto simp: GTT_to_RR2_root_def) have "∃t u q. s = gpair t u ∧ q ∈ ta_res (fst 𝒢) (term_of_gterm t) ∧ q ∈ ta_res (snd 𝒢) (term_of_gterm u)" using subsetD[OF ta_res_mono' q(2), of "pair_automaton (fst 𝒢) (snd 𝒢)"] by (auto simp: GTT_to_RR2_root_def dest!: from_ta_res_pair_automaton(4)) } moreover { fix t u q assume q: "q ∈ ta_res (fst 𝒢) (term_of_gterm t)" "q ∈ ta_res (snd 𝒢) (term_of_gterm u)" then have "gpair t u ∈ gta_lang (GTT_to_RR2_root 𝒢)" using subsetD[OF ta_res_mono' to_ta_res_pair_automaton(3)[OF q], of "GTT_to_RR2_root 𝒢"] q[THEN subsetD[OF ta_res_states[OF ground_term_of_gterm]]] by (auto simp: GTT_to_RR2_root_def gta_lang_def image_def intro!: ta_langI2 bexI[of _ "term_of_gterm _"]) } ultimately show ?thesis by (auto simp: RR2_spec_def) qed lemma swap_GTT_to_RR2_root: "gpair s t ∈ gta_lang (GTT_to_RR2_root (prod.swap 𝒢)) ⟷ gpair t s ∈ gta_lang (GTT_to_RR2_root 𝒢)" by (auto simp: GTT_to_RR2_root[unfolded RR2_spec_def]) lemma funas_mctxt_map_vars_mctxt [simp]: "funas_mctxt (map_vars_mctxt f C) = funas_mctxt C" by (induct C) auto lemma funas_term_GTT_to_RR2_root: assumes "gpair s t ∈ gta_lang (GTT_to_RR2_root 𝒢)" shows "funas_gterm s ⊆ ta_syms (fst 𝒢)" using assms by (auto dest!: ta_syms_res simp: GTT_to_RR2_root[unfolded RR2_spec_def] funas_term_of_gterm_conv) definition GTT_to_RR2 :: "('f × nat) set ⇒ ('q, 'f) gtt ⇒ (_, 'f option × 'f option) ta" where "GTT_to_RR2 F G = parallel_closure_automaton F (GTT_to_RR2_root G)" lemma GTT_to_RR2: assumes "gtt_syms 𝒢 ⊆ F" shows "RR2_spec (GTT_to_RR2 F 𝒢) (ggtt_lang F 𝒢)" proof - note rr2 = parallel_closure_automaton[OF GTT_to_RR2_root, unfolded RR2_spec_def, folded GTT_to_RR2_def] note [simp] = funas_term_of_gterm_conv { fix C :: "('a, unit) mctxt" and ts us assume C: "ground_mctxt C" "funas_mctxt C ⊆ F" "length ts = num_holes C" "length us = num_holes C" "∀i<num_holes C. ∃q. q ∈ ta_res (fst 𝒢) (term_of_gterm (ts ! i)) ∧ q ∈ ta_res (snd 𝒢) (term_of_gterm (us ! i))" have [simp]: "ground (fill_holes C (map term_of_gterm ts))" "ground (fill_holes C (map term_of_gterm us))" using C(1,3,4,5) by (simp_all add: ground_fill_holes) have *: "funas_gterm (ts ! i) ⊆ F" "funas_gterm (us ! i) ⊆ F" if "i < num_holes C" for i using that spec[OF C(5), of i] assms by (auto dest!: ta_syms_res) have "(gfill_holes C ts, gfill_holes C us) ∈ map_both gterm_of_term ` (Restr (gtt_lang 𝒢) {t. funas_term t ⊆ F})" using C by (auto intro!: exI[of _ "gfill_holes _ _"] bexI[of _ "(term_of_gterm _, term_of_gterm _)"] arg_cong[where f = gterm_of_term] simp: gtt_accept_equiv gfill_holes_def map_prod_def image_def split: prod.splits) (auto simp: funas_mctxt_fill_holes in_set_conv_nth *[THEN subsetD] funas_gterm_gterm_of_term gterm_of_term_inv' ground_fill_holes adapt_vars_def map_vars_term_fill_holes gterm.map_ident) } note * = this[simplified] { fix C ts us assume "ground (fill_holes C ts)" "funas_mctxt C ⊆ F" "ground (fill_holes C us)" "length ts = length us" "num_holes C = length us" "∀i < length us. ∃q. q ∈ ta_res (fst 𝒢) (ts ! i) ∧ q ∈ ta_res (snd 𝒢) (us ! i)" then have "gpair (gterm_of_term (fill_holes C ts)) (gterm_of_term (fill_holes C us)) ∈ gta_lang (GTT_to_RR2 F 𝒢)" by (auto intro!: exI[of _ "gterm_of_term (fill_holes C ts)", OF exI[of _ "gterm_of_term (fill_holes C us)"]] exI[of _ "map_vars_mctxt undefined C"] exI[of _ "map gterm_of_term ts", OF conjI[OF _ exI[of _ "map gterm_of_term us"]]] simp: rr2 gfill_holes_def comp_def gterm_of_term_inv' ground_fill_holes adapt_vars_def map_vars_term_fill_holes[symmetric] gterm.map_ident cong: map_cong) } note ** = this[unfolded rr2, simplified] show ?thesis unfolding RR2_spec_def rr2 by (auto simp: funas_mctxt_fill_holes gtt_accept_equiv GTT_to_RR2_def RR2_spec_def ** elim!: gtt_accept'.cases intro: *) qed lemma GTT_to_RR2': shows "RR2_spec (GTT_to_RR2 UNIV 𝒢) (map_both gterm_of_term ` (gtt_lang 𝒢))" using GTT_to_RR2[of 𝒢 UNIV] by simp end