Theory GTT_RRn

theory GTT_RRn
imports GTT TA_Clousure_Const Context_RR2
theory GTT_RRn
  imports RR.GTT TA_Clousure_Const Context_RR2
begin                                    
                                        
abbreviation ggtt_lang where
  "ggtt_lang F G ≡ map_both gterm_of_term ` (Restr (gtt_lang_terms G) {t. funas_term t ⊆ fset F})"

lemma ground_mctxt_map_vars_mctxt [simp]:
  "ground_mctxt (map_vars_mctxt f C) = ground_mctxt C"
  by (induct C) auto

lemma root_single_automaton:
  assumes "RR2_spec 𝒜 R"
  shows "RR2_spec 𝒜 (lift_root_step ℱ PRoot ESingle R)"
  using assms unfolding RR2_spec_def
  by (auto simp: lift_root_step.simps)

lemma root_strictparallel_automaton:
  assumes "RR2_spec 𝒜 R"
  shows "RR2_spec 𝒜 (lift_root_step ℱ PRoot EStrictParallel R)"
  using assms unfolding RR2_spec_def
  by (auto simp: lift_root_step.simps)

lemma reflcl_automaton:
  assumes "RR2_spec 𝒜 R"
  shows "RR2_spec (reflcl_reg (lift_sig_RR2 |`| ℱ) 𝒜) (lift_root_step (fset ℱ) PRoot EParallel R)"
   unfolding RR2_spec_def ℒ_reflcl_reg
   unfolding lift_root_step.simps 𝒯G_equivalent_def assms[unfolded RR2_spec_def]
   by (auto simp flip: 𝒯G_equivalent_def)

lemma parallel_closure_automaton:
  assumes "RR2_spec 𝒜 R"
  shows "RR2_spec (parallel_closure_reg (lift_sig_RR2 |`| ℱ) 𝒜) (lift_root_step (fset ℱ) PAny EParallel R)"
  unfolding RR2_spec_def parallelcl_gmctxt_lang lift_root_step.simps
  unfolding gmctxtex_onp_gpair_set_conv assms[unfolded RR2_spec_def]
  by (intro RR2_gmctxt_cl_to_gmctxt) auto

lemma ctxt_closure_automaton:
  assumes "RR2_spec 𝒜 R"
  shows "RR2_spec (ctxt_closure_reg (lift_sig_RR2 |`| ℱ) 𝒜) (lift_root_step (fset ℱ) PAny ESingle R)"
  unfolding RR2_spec_def gctxt_closure_lang lift_root_step.simps
  unfolding gctxtex_onp_gpair_set_conv assms[unfolded RR2_spec_def]
  by (intro RR2_gctxt_cl_to_gctxt) auto

lemma mctxt_closure_automaton:
  assumes "RR2_spec 𝒜 R"
  shows "RR2_spec (mctxt_closure_reg (lift_sig_RR2 |`| ℱ) 𝒜) (lift_root_step (fset ℱ) PAny EStrictParallel R)"
  unfolding RR2_spec_def gmctxt_closure_lang lift_root_step.simps
  unfolding gmctxtex_onp_gpair_set_conv assms[unfolded RR2_spec_def] conj_assoc
  by (intro RR2_gmctxt_cl_to_gmctxt[where ?P = "λ C. 0 < num_gholes C ∧ funas_gmctxt C ⊆ fset (lift_sig_RR2 |`| ℱ)" and
       ?R = "λ C. 0 < num_gholes C ∧ funas_gmctxt C ⊆ fset ℱ", unfolded conj_assoc]) auto

lemma nhole_ctxt_closure_automaton:
  assumes "RR2_spec 𝒜 R"
  shows "RR2_spec (nhole_ctxt_closure_reg (lift_sig_RR2 |`| ℱ) 𝒜) (lift_root_step (fset ℱ) PNonRoot ESingle R)"
  unfolding RR2_spec_def nhole_ctxtcl_lang lift_root_step.simps
  unfolding gctxtex_onp_gpair_set_conv assms[unfolded RR2_spec_def]
  by (intro RR2_gctxt_cl_to_gctxt[where
    ?P = "λ C. C ≠ □G ∧ funas_gctxt C ⊆ fset (lift_sig_RR2 |`| ℱ)", unfolded conj_assoc]) auto

lemma nhole_mctxt_closure_automaton:
  assumes "RR2_spec 𝒜 R"
  shows "RR2_spec (nhole_mctxt_closure_reg (lift_sig_RR2 |`| ℱ) 𝒜) (lift_root_step (fset ℱ) PNonRoot EStrictParallel R)"
  unfolding RR2_spec_def nhole_gmctxt_closure_lang lift_root_step.simps
  unfolding gmctxtex_onp_gpair_set_conv assms[unfolded RR2_spec_def]
  by (intro RR2_gmctxt_cl_to_gmctxt[where
    ?P = "λ C. 0 < num_gholes C ∧ C ≠ GMHole ∧ funas_gmctxt C ⊆ fset (lift_sig_RR2 |`| ℱ)", unfolded conj_assoc])
    auto

lemma nhole_mctxt_reflcl_automaton:
  assumes "RR2_spec 𝒜 R"
  shows "RR2_spec (nhole_mctxt_reflcl_reg (lift_sig_RR2 |`| ℱ) 𝒜) (lift_root_step (fset ℱ) PNonRoot EParallel R)"
  using nhole_mctxt_closure_automaton[OF assms, of ℱ]
  unfolding RR2_spec_def lift_root_step_Parallel_conv nhole_mctxt_reflcl_lang
  by (auto simp flip: 𝒯G_equivalent_def)

definition GTT_to_RR2_root :: "('q, 'f) gtt ⇒ (_, 'f option × 'f option) ta" where
  "GTT_to_RR2_root 𝒢 = pair_automaton (fst 𝒢) (snd 𝒢)"

definition GTT_to_RR2_root_reg where
  "GTT_to_RR2_root_reg 𝒢 = Reg (map_both Some |`| fId_on (gtt_states 𝒢)) (GTT_to_RR2_root 𝒢)"

lemma GTT_to_RR2_root:
  "RR2_spec (GTT_to_RR2_root_reg 𝒢) (agtt_lang 𝒢)"
proof -
  { fix s assume "s ∈ ℒ (GTT_to_RR2_root_reg 𝒢)"
    then obtain q where q: "q |∈| fin (GTT_to_RR2_root_reg 𝒢)" "q |∈| ta_der (GTT_to_RR2_root 𝒢) (term_of_gterm s)"
      by (auto simp: ℒ_def gta_lang_def GTT_to_RR2_root_reg_def gta_der_def)
    then obtain q' where [simp]: "q = (Some q', Some q')" using q(1) by (auto simp: GTT_to_RR2_root_reg_def)
    have "∃t u q. s = gpair t u ∧ q |∈| ta_der (fst 𝒢) (term_of_gterm t) ∧ q |∈| ta_der (snd 𝒢) (term_of_gterm u)"
      using fsubsetD[OF ta_der_mono' q(2), of "pair_automaton (fst 𝒢) (snd 𝒢)"]
      by (auto simp: GTT_to_RR2_root_def dest!: from_ta_der_pair_automaton(4))
  } moreover
  { fix t u q assume q: "q |∈| ta_der (fst 𝒢) (term_of_gterm t)" "q |∈| ta_der (snd 𝒢) (term_of_gterm u)"
    have "lift_fun q |∈| map_both Some |`| fId_on (𝒬 (fst 𝒢) |∪| 𝒬 (snd 𝒢))"
      using q[THEN fsubsetD[OF ground_ta_der_states[OF  ground_term_of_gterm]]]
      by (auto simp: fimage_iff fBex_def)
    then have "gpair t u ∈ ℒ (GTT_to_RR2_root_reg 𝒢)" using q
      using fsubsetD[OF ta_der_mono to_ta_der_pair_automaton(3)[OF q], of "GTT_to_RR2_root 𝒢"]
      by (auto simp: ℒ_def GTT_to_RR2_root_def gta_lang_def image_def gtt_states_def
        gta_der_def GTT_to_RR2_root_reg_def)
  } ultimately show ?thesis by (auto simp: RR2_spec_def agtt_lang_def ℒ_def gta_der_def)
qed

lemma swap_GTT_to_RR2_root:
  "gpair s t ∈ ℒ (GTT_to_RR2_root_reg (prod.swap 𝒢)) ⟷
   gpair t s ∈ ℒ (GTT_to_RR2_root_reg 𝒢)"
  by (auto simp: GTT_to_RR2_root[unfolded RR2_spec_def] agtt_lang_def)

lemma funas_mctxt_map_vars_mctxt [simp]:
  "funas_mctxt (map_vars_mctxt f C) = funas_mctxt C"
  by (induct C) auto

definition GTT_to_RR2_reg  :: "('f × nat) fset ⇒ ('q, 'f) gtt ⇒ (_, 'f option × 'f option) reg" where
  "GTT_to_RR2_reg F G = parallel_closure_reg (lift_sig_RR2 |`| F) (GTT_to_RR2_root_reg G)"

lemma agtt_lang_syms:
  "gtt_syms 𝒢 |⊆| ℱ ⟹ agtt_lang 𝒢 ⊆ {t. funas_gterm t ⊆ fset ℱ} × {t. funas_gterm t ⊆ fset ℱ}"
  by (auto simp: agtt_lang_def gta_der_def funas_term_of_gterm_conv)
     (metis ffunas_gterm.rep_eq fin_mono notin_fset ta_der_gterm_sig)+

lemma GTT_to_RR2:
  assumes "gtt_syms 𝒢 |⊆| ℱ"
  shows "RR2_spec (GTT_to_RR2_reg ℱ 𝒢) (ggtt_lang ℱ 𝒢)"
proof -
  have *: "snd ` (X × X) = X" for X by auto
  show ?thesis unfolding gtt_lang_from_agtt_lang GTT_to_RR2_reg_def RR2_spec_def
    parallel_closure_automaton[OF GTT_to_RR2_root, of ℱ 𝒢, unfolded RR2_spec_def]
  proof (intro arg_cong[where f = "λX. {gpair t u |t u. (t,u) ∈ X}"] equalityI subrelI, goal_cases)
    case (1 s t) then show ?case
      using subsetD[OF equalityD2[OF gtt_lang_from_agtt_lang], of "(s, t)" 𝒢]
      by (intro rev_image_eqI[of "(term_of_gterm s, term_of_gterm t)"])
         (auto simp: funas_term_of_gterm_conv subsetD[OF lift_root_step_mono]
           dest: subsetD[OF lift_root_step_sig[unfolded 𝒯G_equivalent_def, OF agtt_lang_syms[OF assms]]])
  next
    case (2 s t)
    from image_mono[OF agtt_lang_syms[OF assms], of snd, unfolded *]
    have *: "snd ` agtt_lang 𝒢 ⊆ gterms UNIV" by auto
    show ?case using 2
      by (auto intro!: lift_root_step_sig_transfer[unfolded 𝒯G_equivalent_def, OF _ *, of _ _ _ "fset ℱ"]
        simp: funas_gterm_gterm_of_term funas_term_of_gterm_conv)
         (metis case_prodI gtt_lang_from_agtt_lang mem_Collect_eq)
  qed
qed


end